The cat likes the squirrel. The cow eats the cat. The cow is nice. The cow likes the cat. The cow needs the cat. The squirrel eats the cat. The squirrel is red. The squirrel likes the cow. The squirrel needs the cat. The squirrel needs the cow. If the squirrel eats the cat and the squirrel likes the cow then the squirrel likes the cat. If someone likes the cat then the cat eats the squirrel. If someone likes the cat then the cat is red. If someone is nice and they need the cow then the cow is red. If someone eats the squirrel and the squirrel is red then they like the squirrel. If someone is nice and they like the cow then they need the cow. If the squirrel needs the cat and the squirrel is red then the squirrel likes the cow. If someone is red then they like the squirrel.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If the squirrel eats the cat and the squirrel likes the cow then the squirrel likes the cat.
((("squirrel" "eats" "cat" "+") ("squirrel" "likes" "cow" "+")) -> ("squirrel" "likes" "cat" "+"))
If someone likes the cat then the cat eats the squirrel.
((("someone" "likes" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If someone likes the cat then the cat is red.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is nice and they need the cow then the cow is red.
((("someone" "is" "nice" "+") ("someone" "needs" "cow" "+")) -> ("cow" "is" "red" "+"))
If someone eats the squirrel and the squirrel is red then they like the squirrel.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is nice and they like the cow then they need the cow.
((("someone" "is" "nice" "+") ("someone" "likes" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If the squirrel needs the cat and the squirrel is red then the squirrel likes the cow.
((("squirrel" "needs" "cat" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone is red then they like the squirrel.
((("someone" "is" "red" "+")) -> ("someone" "likes" "squirrel" "+"))
The squirrel needs the cow.
True
1
proof
[(triple10)]
("squirrel" "needs" "cow" "+")
triple10
The cow is not nice.
False
1
inv-proof
[(triple3)]
("cow" "is" "nice" "-")
triple3
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "cow" "-")
The cat eats the cow.
Unknown
random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "+")
@0: The cat likes the squirrel.[(triple1 OR ((((triple4) -> rule3)) -> rule8) OR ((((triple4) -> rule2) triple7) -> rule5) OR ((((((triple6 triple8) -> rule1)) -> rule3)) -> rule8) OR ((((((triple6 triple8) -> rule1)) -> rule2) triple7) -> rule5) OR ((((((triple6 ((triple9 triple7) -> rule7)) -> rule1)) -> rule3)) -> rule8) OR ((((((triple6 ((triple9 triple7) -> rule7)) -> rule1)) -> rule2) triple7) -> rule5))] The cow eats the cat.[(triple2)] The cow is nice.[(triple3)] The cow likes the cat.[(triple4)] The cow needs the cat.[(triple5)] The squirrel eats the cat.[(triple6)] The squirrel is red.[(triple7)] The squirrel likes the cow.[(triple8 OR ((triple9 triple7) -> rule7))] The squirrel needs the cat.[(triple9)] The squirrel needs the cow.[(triple10)] @1: The cat eats the squirrel.[(((triple4) -> rule2) OR ((((triple6 triple8) -> rule1)) -> rule2) OR ((((triple6 ((triple9 triple7) -> rule7)) -> rule1)) -> rule2))] The cat is red.[(((triple4) -> rule3) OR ((((triple6 triple8) -> rule1)) -> rule3) OR ((((triple6 ((triple9 triple7) -> rule7)) -> rule1)) -> rule3))] The squirrel likes the cat.[(((triple6 triple8) -> rule1) OR ((triple6 ((triple9 triple7) -> rule7)) -> rule1))] The squirrel likes the squirrel.[(((triple7) -> rule8))]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple4) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
((((((triple6 triple8) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple6 triple8) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple6 ((triple9 triple7) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int4
((((((triple6 ((triple9 triple7) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow likes the cat.
("cow" "likes" "cat" "+")
triple4
The cow needs the cat.
("cow" "needs" "cat" "+")
triple5
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple8
((triple9 triple7) -> (rule7 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((triple4) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
((((triple6 triple8) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple6 ((triple9 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int3
The cat is red.
("cat" "is" "red" "+")
((triple4) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple6 triple8) -> (rule1 % int2))) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple6 ((triple9 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int3
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((triple6 triple8) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
((triple6 ((triple9 triple7) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple7) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1