The mouse eats the squirrel. The mouse is cold. The mouse is rough. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel eats the mouse. The squirrel is cold. The squirrel is rough. The squirrel is round. The squirrel is young. The squirrel needs the mouse. The squirrel sees the mouse. If someone is cold then they need the mouse.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone is cold then they need the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "mouse" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple12)]
("squirrel" "sees" "mouse" "+")
triple12
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple6)]
("squirrel" "eats" "mouse" "-")
triple6
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse is cold.[(triple2)] The mouse is rough.[(triple3)] The mouse needs the squirrel.[(triple4)] The mouse sees the squirrel.[(triple5)] The squirrel eats the mouse.[(triple6)] The squirrel is cold.[(triple7)] The squirrel is rough.[(triple8)] The squirrel is round.[(triple9)] The squirrel is young.[(triple10)] The squirrel needs the mouse.[(triple11 OR ((triple7) -> rule1))] The squirrel sees the mouse.[(triple12)] @1: The mouse needs the mouse.[(((triple2) -> rule1))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple11
((triple7) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple12
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1