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