The dog eats the mouse. The dog is green. The dog is nice. The dog likes the mouse. The dog visits the mouse. The mouse is big. The mouse visits the dog. If the dog is nice then the dog visits the mouse. If something visits the mouse then it likes the dog. If something is nice and it likes the mouse then it likes the dog. If something eats the dog and the dog visits the mouse then it visits the mouse. If something likes the mouse then the mouse eats the dog. If something eats the dog and it is green then it is nice.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If the dog is nice then the dog visits the mouse.
((("dog" "is" "nice" "+")) -> ("dog" "visits" "mouse" "+"))
If something visits the mouse then it likes the dog.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "dog" "+"))
If something is nice and it likes the mouse then it likes the dog.
((("something" "is" "nice" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "dog" "+"))
If something eats the dog and the dog visits the mouse then it visits the mouse.
((("something" "eats" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something likes the mouse then the mouse eats the dog.
((("something" "likes" "mouse" "+")) -> ("mouse" "eats" "dog" "+"))
If something eats the dog and it is green then it is nice.
((("something" "eats" "dog" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The dog does not like the mouse.
False
1
inv-proof
[(triple4)]
("dog" "likes" "mouse" "-")
triple4
The mouse eats the dog.
True
2
proof
[(((triple4) -> rule5))]
("mouse" "eats" "dog" "+")
((triple4) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse does not eat the dog.
False
2
inv-proof
[(((triple4) -> rule5))]
("mouse" "eats" "dog" "-")
((triple4) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the mouse.
True
4
proof
[(((((triple4) -> rule5) triple5) -> rule4) OR ((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4))]
("mouse" "visits" "mouse" "+")
((((triple4) -> (rule5 % int2)) triple5) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
((((triple4) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The mouse does not visit the mouse.
False
4
inv-proof
[(((((triple4) -> rule5) triple5) -> rule4) OR ((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4))]
("mouse" "visits" "mouse" "-")
((((triple4) -> (rule5 % int2)) triple5) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
((((triple4) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The mouse likes the dog.
True
5
proof
[(((((((triple4) -> rule5) triple5) -> rule4)) -> rule2) OR ((((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4)) -> rule2))]
("mouse" "likes" "dog" "+")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
((((((triple4) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int4
The mouse does not like the dog.
False
5
inv-proof
[(((((((triple4) -> rule5) triple5) -> rule4)) -> rule2) OR ((((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4)) -> rule2))]
("mouse" "likes" "dog" "-")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
((((((triple4) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int4
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "nice" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The dog eats the mouse.[(triple1)] The dog is green.[(triple2)] The dog is nice.[(triple3)] The dog likes the mouse.[(triple4)] The dog visits the mouse.[(triple5 OR ((triple3) -> rule1))] The mouse is big.[(triple6)] The mouse visits the dog.[(triple7)] @1: The dog likes the dog.[(((triple5) -> rule2) OR ((triple3 triple4) -> rule3) OR ((((triple3) -> rule1)) -> rule2))] The mouse eats the dog.[(((triple4) -> rule5))] @2: The mouse visits the mouse.[(((((triple4) -> rule5) triple5) -> rule4) OR ((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4))] @3: The mouse likes the dog.[(((((((triple4) -> rule5) triple5) -> rule4)) -> rule2) OR ((((((triple4) -> rule5) ((triple3) -> rule1)) -> rule4)) -> rule2))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple5
((triple3) -> (rule1 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple5) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
((triple3 triple4) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple4) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple4) -> (rule5 % int2)) triple5) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
((((triple4) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
((((((triple4) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int4