The mouse is big. The mouse is blue. The mouse is green. The mouse is not young. The mouse does not like the squirrel. The mouse needs the squirrel. The mouse visits the squirrel. The squirrel is big. The squirrel is not blue. The squirrel is green. The squirrel is round. The squirrel is young. The squirrel likes the mouse. The squirrel needs the mouse. The squirrel visits the mouse. If the mouse likes the squirrel then the squirrel is not young. If the mouse is not young and the mouse does not need the squirrel then the mouse does not visit the squirrel. If something visits the squirrel and the squirrel needs the mouse then it visits the mouse. If something is blue then it is round. If the mouse visits the squirrel and the squirrel is blue then the mouse likes the squirrel. If something likes the mouse then it likes the squirrel.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If the mouse likes the squirrel then the squirrel is not young.
((("mouse" "likes" "squirrel" "+")) -> ("squirrel" "is" "young" "-"))
If the mouse is not young and the mouse does not need the squirrel then the mouse does not visit the squirrel.
((("mouse" "is" "young" "~") ("mouse" "needs" "squirrel" "~")) -> ("mouse" "visits" "squirrel" "-"))
If something visits the squirrel and the squirrel needs the mouse then it visits the mouse.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If the mouse visits the squirrel and the squirrel is blue then the mouse likes the squirrel.
((("mouse" "visits" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something likes the mouse then it likes the squirrel.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "squirrel" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple7)]
("mouse" "visits" "squirrel" "+")
triple7
The squirrel does not need the mouse.
False
1
inv-proof
[(triple14)]
("squirrel" "needs" "mouse" "-")
triple14
The squirrel likes the squirrel.
True
2
proof
[(((triple13) -> rule6))]
("squirrel" "likes" "squirrel" "+")
((triple13) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The mouse does not visit the mouse.
False
3
inv-proof
[(((triple7 triple14) -> rule3))]
("mouse" "visits" "mouse" "-")
((triple7 triple14) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
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 mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse does not like the squirrel.[(triple5)] The mouse is big.[(triple1)] The mouse is blue.[(triple2)] The mouse is green.[(triple3)] The mouse is not young.[(triple4)] The mouse needs the squirrel.[(triple6)] The mouse visits the squirrel.[(triple7)] The squirrel is big.[(triple8)] The squirrel is green.[(triple10)] The squirrel is not blue.[(triple9)] The squirrel is round.[(triple11)] The squirrel is young.[(triple12)] The squirrel likes the mouse.[(triple13)] The squirrel needs the mouse.[(triple14)] The squirrel visits the mouse.[(triple15)] @1: The mouse is round.[(((triple2) -> rule4))] The mouse visits the mouse.[(((triple7 triple14) -> rule3))] The squirrel likes the squirrel.[(((triple13) -> rule6))]
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is not young.
("mouse" "is" "young" "-")
triple4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple6
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel is young.
("squirrel" "is" "young" "+")
triple12
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple14
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple15
The mouse is round.
("mouse" "is" "round" "+")
((triple2) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple7 triple14) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple13) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1