The cat eats the squirrel. The cat is cold. The cat is red. The cat is young. The cat likes the squirrel. The cat does not see the squirrel. The squirrel likes the cat. If the cat does not see the squirrel then the cat likes the squirrel. If something likes the cat and the cat eats the squirrel then the squirrel is big.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If the cat does not see the squirrel then the cat likes the squirrel.
((("cat" "sees" "squirrel" "~")) -> ("cat" "likes" "squirrel" "+"))
If something likes the cat and the cat eats the squirrel then the squirrel is big.
((("something" "likes" "cat" "+") ("cat" "eats" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The squirrel does not like the cat.
False
1
inv-proof
[(triple7)]
("squirrel" "likes" "cat" "-")
triple7
The squirrel is big.
True
3
proof
[(((triple7 triple1) -> rule2))]
("squirrel" "is" "big" "+")
((triple7 triple1) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
3
inv-proof
[(((triple7 triple1) -> rule2))]
("squirrel" "is" "big" "-")
((triple7 triple1) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The cat does not see the squirrel.[(triple6)] The cat eats the squirrel.[(triple1)] The cat is cold.[(triple2)] The cat is red.[(triple3)] The cat is young.[(triple4)] The cat likes the squirrel.[(triple5 OR ((triple6) -> rule1))] The squirrel likes the cat.[(triple7)] @1: The squirrel is big.[(((triple7 triple1) -> rule2))]
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple6
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
((triple6) -> (rule1 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
((triple7 triple1) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1