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