The cat eats the squirrel. The cat is rough. The cat visits the squirrel. The lion eats the cat. The lion is rough. The lion needs the cat. The squirrel is green. The squirrel is kind. The squirrel needs the lion. The squirrel visits the lion. If the squirrel is big and the squirrel eats the cat then the cat needs the lion. If someone visits the squirrel then the squirrel needs the cat. If someone visits the lion then the lion needs the squirrel.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the squirrel is big and the squirrel eats the cat then the cat needs the lion.
((("squirrel" "is" "big" "+") ("squirrel" "eats" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If someone visits the squirrel then the squirrel needs the cat.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "needs" "cat" "+"))
If someone visits the lion then the lion needs the squirrel.
((("someone" "visits" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
The squirrel is green.
True
1
proof
[(triple7)]
("squirrel" "is" "green" "+")
triple7
The squirrel does not visit the lion.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "lion" "-")
triple10
The squirrel needs the cat.
True
2
proof
[(((triple3) -> rule2))]
("squirrel" "needs" "cat" "+")
((triple3) -> (rule2 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The lion does not need the squirrel.
False
2
inv-proof
[(((triple10) -> rule3))]
("lion" "needs" "squirrel" "-")
((triple10) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The cat does not need the lion.
Unknown
inv-rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "lion" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
The squirrel does not eat the cat.
Unknown
inv-random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "-")
The cat eats the lion.
Unknown
random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "+")
@0: The cat eats the squirrel.[(triple1)] The cat is rough.[(triple2)] The cat visits the squirrel.[(triple3)] The lion eats the cat.[(triple4)] The lion is rough.[(triple5)] The lion needs the cat.[(triple6)] The squirrel is green.[(triple7)] The squirrel is kind.[(triple8)] The squirrel needs the lion.[(triple9)] The squirrel visits the lion.[(triple10)] @1: The lion needs the squirrel.[(((triple10) -> rule3))] The squirrel needs the cat.[(((triple3) -> rule2))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The lion eats the cat.
("lion" "eats" "cat" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((triple10) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple3) -> (rule2 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1