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