The cow eats the mouse. The cow eats the squirrel. The cow is big. The cow is blue. The cow is cold. The cow likes the mouse. The cow likes the squirrel. The cow needs the squirrel. The mouse eats the squirrel. The mouse likes the cow. The mouse needs the squirrel. The squirrel eats the cow. The squirrel is cold. The squirrel likes the mouse. The squirrel needs the mouse. If something likes the squirrel and it needs the squirrel then the squirrel is rough. If something eats the squirrel then it needs the squirrel.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something likes the squirrel and it needs the squirrel then the squirrel is rough.
((("something" "likes" "squirrel" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If something eats the squirrel then it needs the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "needs" "squirrel" "+"))
The cow needs the squirrel.
True
1
proof
[(triple8 OR ((triple2) -> rule2))]
("cow" "needs" "squirrel" "+")
triple8
((triple2) -> (rule2 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel does not like the mouse.
False
1
inv-proof
[(triple14)]
("squirrel" "likes" "mouse" "-")
triple14
The squirrel is rough.
True
3
proof
[(((triple7 triple8) -> rule1) OR ((triple7 ((triple2) -> rule2)) -> rule1))]
("squirrel" "is" "rough" "+")
((triple7 triple8) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple7 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel is not rough.
False
3
inv-proof
[(((triple7 triple8) -> rule1) OR ((triple7 ((triple2) -> rule2)) -> rule1))]
("squirrel" "is" "rough" "-")
((triple7 triple8) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple7 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cow needs the mouse.
Unknown
random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The cow eats the mouse.[(triple1)] The cow eats the squirrel.[(triple2)] The cow is big.[(triple3)] The cow is blue.[(triple4)] The cow is cold.[(triple5)] The cow likes the mouse.[(triple6)] The cow likes the squirrel.[(triple7)] The cow needs the squirrel.[(triple8 OR ((triple2) -> rule2))] The mouse eats the squirrel.[(triple9)] The mouse likes the cow.[(triple10)] The mouse needs the squirrel.[(triple11 OR ((triple9) -> rule2))] The squirrel eats the cow.[(triple12)] The squirrel is cold.[(triple13)] The squirrel likes the mouse.[(triple14)] The squirrel needs the mouse.[(triple15)] @1: The squirrel is rough.[(((triple7 triple8) -> rule1) OR ((triple7 ((triple2) -> rule2)) -> rule1))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is blue.
("cow" "is" "blue" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple6
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple7
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple8
((triple2) -> (rule2 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple11
((triple9) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple14
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple15
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple7 triple8) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple7 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2