The mouse is not green. The mouse likes the squirrel. The mouse visits the squirrel. The squirrel is green. The squirrel is kind. The squirrel is round. The squirrel is young. The squirrel likes the mouse. The squirrel sees the mouse. The squirrel visits the mouse. If the squirrel visits the mouse and the mouse visits the squirrel then the mouse sees the squirrel. If the squirrel is young then the squirrel is big. If someone likes the squirrel and they see the squirrel then they like the mouse. If someone visits the squirrel then they are round. If someone sees the mouse and they are round then they see the squirrel. If someone sees the mouse then the mouse is kind.
The mouse is not green.
("mouse" "is" "green" "-")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If the squirrel visits the mouse and the mouse visits the squirrel then the mouse sees the squirrel.
((("squirrel" "visits" "mouse" "+") ("mouse" "visits" "squirrel" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the squirrel is young then the squirrel is big.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "big" "+"))
If someone likes the squirrel and they see the squirrel then they like the mouse.
((("someone" "likes" "squirrel" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "mouse" "+"))
If someone visits the squirrel then they are round.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If someone sees the mouse and they are round then they see the squirrel.
((("someone" "sees" "mouse" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the mouse then the mouse is kind.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
The squirrel likes the mouse.
True
1
proof
[(triple8)]
("squirrel" "likes" "mouse" "+")
triple8
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "mouse" "-")
triple10
The mouse is round.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "is" "round" "+")
((triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not see the squirrel.
False
3
inv-proof
[(((triple10 triple3) -> rule1))]
("mouse" "sees" "squirrel" "-")
((triple10 triple3) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse likes the mouse.
True
5
proof
[(((triple2 ((triple10 triple3) -> rule1)) -> rule3))]
("mouse" "likes" "mouse" "+")
((triple2 ((triple10 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse does not like the mouse.
False
5
inv-proof
[(((triple2 ((triple10 triple3) -> rule1)) -> rule3))]
("mouse" "likes" "mouse" "-")
((triple2 ((triple10 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "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 is not green.[(triple1)] The mouse likes the squirrel.[(triple2)] The mouse visits the squirrel.[(triple3)] The squirrel is green.[(triple4)] The squirrel is kind.[(triple5)] The squirrel is round.[(triple6)] The squirrel is young.[(triple7)] The squirrel likes the mouse.[(triple8)] The squirrel sees the mouse.[(triple9)] The squirrel visits the mouse.[(triple10)] @1: The mouse is kind.[(((triple9) -> rule6))] The mouse is round.[(((triple3) -> rule4))] The mouse sees the squirrel.[(((triple10 triple3) -> rule1))] The squirrel is big.[(((triple7) -> rule2))] The squirrel sees the squirrel.[(((triple9 triple6) -> rule5))] @2: The mouse likes the mouse.[(((triple2 ((triple10 triple3) -> rule1)) -> rule3))]
The mouse is not green.
("mouse" "is" "green" "-")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
triple4
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple5
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel is young.
("squirrel" "is" "young" "+")
triple7
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple8
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple9
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
((triple9) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple10 triple3) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple7) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple9 triple6) -> (rule5 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple2 ((triple10 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2