The mouse eats the squirrel. The mouse is cold. The mouse is green. The mouse is kind. The mouse is rough. The mouse is young. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel eats the mouse. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is rough. The squirrel is young. The squirrel likes the mouse. The squirrel sees the mouse. If someone likes the mouse then the mouse eats the squirrel. If the squirrel is green then the squirrel eats the mouse. If someone is cold then they see the squirrel.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the squirrel.
("mouse" "likes" "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 green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone likes the mouse then the mouse eats the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the squirrel is green then the squirrel eats the mouse.
((("squirrel" "is" "green" "+")) -> ("squirrel" "eats" "mouse" "+"))
If someone is cold then they see the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "squirrel" "+"))
The mouse likes the squirrel.
True
1
proof
[(triple7)]
("mouse" "likes" "squirrel" "+")
triple7
The mouse does not eat the squirrel.
False
1
inv-proof
[(triple1 OR ((triple15) -> rule1))]
("mouse" "eats" "squirrel" "-")
triple1
((triple15) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel sees the squirrel.
True
2
proof
[(((triple10) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((triple10) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple10) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((triple10) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse eats the squirrel.[(triple1 OR ((triple15) -> rule1))] The mouse is cold.[(triple2)] The mouse is green.[(triple3)] The mouse is kind.[(triple4)] The mouse is rough.[(triple5)] The mouse is young.[(triple6)] The mouse likes the squirrel.[(triple7)] The mouse sees the squirrel.[(triple8 OR ((triple2) -> rule3))] The squirrel eats the mouse.[(triple9 OR ((triple11) -> rule2))] The squirrel is cold.[(triple10)] The squirrel is green.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is rough.[(triple13)] The squirrel is young.[(triple14)] The squirrel likes the mouse.[(triple15)] The squirrel sees the mouse.[(triple16)] @1: The squirrel sees the squirrel.[(((triple10) -> rule3))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
((triple15) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
((triple2) -> (rule3 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
((triple11) -> (rule2 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple15
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple16
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple10) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1