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