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