The cat chases the squirrel. The cat eats the squirrel. The cat is cold. The cat is green. The cat is kind. The cat is rough. The cat is young. The cat likes the squirrel. The squirrel chases the cat. The squirrel eats the cat. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is rough. The squirrel is young. The squirrel likes the cat. If someone is young and kind then they like the cat. If someone likes the squirrel and the squirrel likes the cat then they like the cat. If someone is kind and they eat the squirrel then they are cold. If someone likes the cat and they like the squirrel then they are green. If the cat chases the squirrel then the cat likes the squirrel. If someone likes the cat and they chase the squirrel then they chase the cat.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If someone is young and kind then they like the cat.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the squirrel and the squirrel likes the cat then they like the cat.
((("someone" "likes" "squirrel" "+") ("squirrel" "likes" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If someone is kind and they eat the squirrel then they are cold.
((("someone" "is" "kind" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the cat and they like the squirrel then they are green.
((("someone" "likes" "cat" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If the cat chases the squirrel then the cat likes the squirrel.
((("cat" "chases" "squirrel" "+")) -> ("cat" "likes" "squirrel" "+"))
If someone likes the cat and they chase the squirrel then they chase the cat.
((("someone" "likes" "cat" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "cat" "+"))
The squirrel is young.
True
1
proof
[(triple15)]
("squirrel" "is" "young" "+")
triple15
The cat is not rough.
False
1
inv-proof
[(triple6)]
("cat" "is" "rough" "-")
triple6
The cat likes the cat.
True
3
proof
[(((triple7 triple5) -> rule1) OR ((triple8 triple16) -> rule2) OR ((triple8 ((triple15 triple13) -> rule1)) -> rule2) OR ((((triple1) -> rule5) triple16) -> rule2) OR ((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2))]
("cat" "likes" "cat" "+")
((triple7 triple5) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple1) -> (rule5 % int2)) triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
The cat does not like the cat.
False
3
inv-proof
[(((triple7 triple5) -> rule1) OR ((triple8 triple16) -> rule2) OR ((triple8 ((triple15 triple13) -> rule1)) -> rule2) OR ((((triple1) -> rule5) triple16) -> rule2) OR ((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2))]
("cat" "likes" "cat" "-")
((triple7 triple5) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple1) -> (rule5 % int2)) triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
The cat chases the cat.
True
5
proof
[(((((triple7 triple5) -> rule1) triple1) -> rule6) OR ((((triple8 triple16) -> rule2) triple1) -> rule6) OR ((((triple8 ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) triple16) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6))]
("cat" "chases" "cat" "+")
((((triple7 triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple1) -> (rule5 % int3)) triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int4
The cat does not chase the cat.
False
5
inv-proof
[(((((triple7 triple5) -> rule1) triple1) -> rule6) OR ((((triple8 triple16) -> rule2) triple1) -> rule6) OR ((((triple8 ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) triple16) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6))]
("cat" "chases" "cat" "-")
((((triple7 triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple1) -> (rule5 % int3)) triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int4
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat chases the squirrel.[(triple1)] The cat eats the squirrel.[(triple2)] The cat is cold.[(triple3 OR ((triple5 triple2) -> rule3))] The cat is green.[(triple4 OR ((((triple7 triple5) -> rule1) triple8) -> rule4) OR ((((triple8 triple16) -> rule2) triple8) -> rule4) OR ((((triple7 triple5) -> rule1) ((triple1) -> rule5)) -> rule4) OR ((((triple8 triple16) -> rule2) ((triple1) -> rule5)) -> rule4) OR ((((triple8 ((triple15 triple13) -> rule1)) -> rule2) triple8) -> rule4) OR ((((((triple1) -> rule5) triple16) -> rule2) triple8) -> rule4) OR ((((triple8 ((triple15 triple13) -> rule1)) -> rule2) ((triple1) -> rule5)) -> rule4) OR ((((((triple1) -> rule5) triple16) -> rule2) ((triple1) -> rule5)) -> rule4) OR ((((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2) triple8) -> rule4) OR ((((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2) ((triple1) -> rule5)) -> rule4))] The cat is kind.[(triple5)] The cat is rough.[(triple6)] The cat is young.[(triple7)] The cat likes the squirrel.[(triple8 OR ((triple1) -> rule5))] The squirrel chases the cat.[(triple9)] The squirrel eats the cat.[(triple10)] The squirrel is cold.[(triple11)] The squirrel is green.[(triple12)] The squirrel is kind.[(triple13)] The squirrel is rough.[(triple14)] The squirrel is young.[(triple15)] The squirrel likes the cat.[(triple16 OR ((triple15 triple13) -> rule1))] @1: The cat likes the cat.[(((triple7 triple5) -> rule1) OR ((triple8 triple16) -> rule2) OR ((triple8 ((triple15 triple13) -> rule1)) -> rule2) OR ((((triple1) -> rule5) triple16) -> rule2) OR ((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2))] @2: The cat chases the cat.[(((((triple7 triple5) -> rule1) triple1) -> rule6) OR ((((triple8 triple16) -> rule2) triple1) -> rule6) OR ((((triple8 ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) triple16) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule5) ((triple15 triple13) -> rule1)) -> rule2) triple1) -> rule6))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
((triple5 triple2) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
triple4
((((triple7 triple5) -> (rule1 % int2)) triple8) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 triple16) -> (rule2 % int2)) triple8) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple7 triple5) -> (rule1 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
((((triple8 triple16) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
((((triple8 ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple1) -> (rule5 % int3)) triple16) -> (rule2 % int2)) triple8) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
((((triple8 ((triple15 triple13) -> (rule1 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int4
((((((triple1) -> (rule5 % int3)) triple16) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int4
((((((triple1) -> (rule5 % int4)) ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int4))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple8
((triple1) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple9
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel is green.
("squirrel" "is" "green" "+")
triple12
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel is young.
("squirrel" "is" "young" "+")
triple15
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple16
((triple15 triple13) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple7 triple5) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple8 ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((triple1) -> (rule5 % int2)) triple16) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple15 triple13) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple7 triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple8 ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
((((((triple1) -> (rule5 % int3)) triple16) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple15 triple13) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int4