The cat chases the mouse. The cat eats the mouse. The cat eats the squirrel. The cat is big. The cat needs the squirrel. The mouse chases the squirrel. The mouse eats the cat. The mouse is cold. The mouse needs the cat. The mouse needs the squirrel. The squirrel chases the cat. The squirrel chases the mouse. The squirrel is red. The squirrel is young. The squirrel needs the mouse. If someone chases the cat then the cat chases the mouse. If someone chases the cat then the cat is cold. If the squirrel chases the cat and the cat eats the mouse then the mouse is cold.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is big.
("cat" "is" "big" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone chases the cat then the cat chases the mouse.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If someone chases the cat then the cat is cold.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "cold" "+"))
If the squirrel chases the cat and the cat eats the mouse then the mouse is cold.
((("squirrel" "chases" "cat" "+") ("cat" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The cat eats the mouse.
True
1
proof
[(triple2)]
("cat" "eats" "mouse" "+")
triple2
The mouse is not cold.
False
1
inv-proof
[(triple8 OR ((triple11 triple2) -> rule3))]
("mouse" "is" "cold" "-")
triple8
((triple11 triple2) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat does not chase the squirrel.
Unknown
inv-random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the mouse.[(triple1 OR ((triple11) -> rule1))] The cat eats the mouse.[(triple2)] The cat eats the squirrel.[(triple3)] The cat is big.[(triple4)] The cat needs the squirrel.[(triple5)] The mouse chases the squirrel.[(triple6)] The mouse eats the cat.[(triple7)] The mouse is cold.[(triple8 OR ((triple11 triple2) -> rule3))] The mouse needs the cat.[(triple9)] The mouse needs the squirrel.[(triple10)] The squirrel chases the cat.[(triple11)] The squirrel chases the mouse.[(triple12)] The squirrel is red.[(triple13)] The squirrel is young.[(triple14)] The squirrel needs the mouse.[(triple15)] @1: The cat is cold.[(((triple11) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
((triple11) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple3
The cat is big.
("cat" "is" "big" "+")
triple4
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple5
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple6
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
((triple11 triple2) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple9
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple10
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple11
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple15
The cat is cold.
("cat" "is" "cold" "+")
((triple11) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1