The cat is nice. The cat likes the squirrel. The cat needs the squirrel. The cat visits the squirrel. The squirrel is big. The squirrel is blue. The squirrel is kind. The squirrel is red. The squirrel needs the cat. The squirrel visits the cat. If someone visits the squirrel and they need the cat then the squirrel likes the cat. If someone is big and blue then they visit the squirrel. If someone likes the cat and they are red then the cat visits the squirrel.
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone visits the squirrel and they need the cat then the squirrel likes the cat.
((("someone" "visits" "squirrel" "+") ("someone" "needs" "cat" "+")) -> ("squirrel" "likes" "cat" "+"))
If someone is big and blue then they visit the squirrel.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone likes the cat and they are red then the cat visits the squirrel.
((("someone" "likes" "cat" "+") ("someone" "is" "red" "+")) -> ("cat" "visits" "squirrel" "+"))
The squirrel is kind.
True
1
proof
[(triple7)]
("squirrel" "is" "kind" "+")
triple7
The cat does not like the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "likes" "squirrel" "-")
triple2
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is nice.[(triple1)] The cat likes the squirrel.[(triple2)] The cat needs the squirrel.[(triple3)] The cat visits the squirrel.[(triple4 OR ((((((triple5 triple6) -> rule2) triple9) -> rule1) triple8) -> rule3))] The squirrel is big.[(triple5)] The squirrel is blue.[(triple6)] The squirrel is kind.[(triple7)] The squirrel is red.[(triple8)] The squirrel needs the cat.[(triple9)] The squirrel visits the cat.[(triple10)] @1: The squirrel visits the squirrel.[(((triple5 triple6) -> rule2))] @2: The squirrel likes the cat.[(((((triple5 triple6) -> rule2) triple9) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple3
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple4
((((((triple5 triple6) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple8) -> (rule3 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple9
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple10
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple5 triple6) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((((triple5 triple6) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2