The cow eats the squirrel. The mouse eats the cow. The mouse is red. The mouse visits the cow. The mouse visits the rabbit. The mouse visits the squirrel. The rabbit needs the mouse. The squirrel needs the mouse. The squirrel needs the rabbit. The squirrel visits the mouse. If something needs the rabbit then the rabbit eats the squirrel.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something needs the rabbit then the rabbit eats the squirrel.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple8)]
("squirrel" "needs" "mouse" "+")
triple8
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple5)]
("mouse" "visits" "rabbit" "-")
triple5
The cow does not eat the mouse.
Unknown
inv-random
[@0: The cow eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "mouse" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow eats the squirrel.[(triple1)] The mouse eats the cow.[(triple2)] The mouse is red.[(triple3)] The mouse visits the cow.[(triple4)] The mouse visits the rabbit.[(triple5)] The mouse visits the squirrel.[(triple6)] The rabbit needs the mouse.[(triple7)] The squirrel needs the mouse.[(triple8)] The squirrel needs the rabbit.[(triple9)] The squirrel visits the mouse.[(triple10)] @1: The rabbit eats the squirrel.[(((triple9) -> rule1))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple6
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple7
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple8
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple9
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple10
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((triple9) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1