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