The cat chases the squirrel. The cat eats the squirrel. The cat is blue. The cat is kind. The cat is red. The cat needs the squirrel. The squirrel chases the cat. The squirrel is blue. The squirrel is red. The squirrel needs the cat. If something is blue then it chases the squirrel. If the cat chases the squirrel then the squirrel chases the cat. If the cat is kind and the cat is green then the cat needs the squirrel. If something eats the cat and the cat needs the squirrel then the cat chases the squirrel. If something chases the cat then it eats the cat. If something needs the squirrel and the squirrel chases the cat then the cat chases the squirrel. If the cat needs the squirrel and the squirrel is blue then the squirrel eats the cat. If something is red and it chases the squirrel then it is kind.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If something is blue then it chases the squirrel.
((("something" "is" "blue" "+")) -> ("something" "chases" "squirrel" "+"))
If the cat chases the squirrel then the squirrel chases the cat.
((("cat" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cat" "+"))
If the cat is kind and the cat is green then the cat needs the squirrel.
((("cat" "is" "kind" "+") ("cat" "is" "green" "+")) -> ("cat" "needs" "squirrel" "+"))
If something eats the cat and the cat needs the squirrel then the cat chases the squirrel.
((("something" "eats" "cat" "+") ("cat" "needs" "squirrel" "+")) -> ("cat" "chases" "squirrel" "+"))
If something chases the cat then it eats the cat.
((("something" "chases" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something needs the squirrel and the squirrel chases the cat then the cat chases the squirrel.
((("something" "needs" "squirrel" "+") ("squirrel" "chases" "cat" "+")) -> ("cat" "chases" "squirrel" "+"))
If the cat needs the squirrel and the squirrel is blue then the squirrel eats the cat.
((("cat" "needs" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "eats" "cat" "+"))
If something is red and it chases the squirrel then it is kind.
((("something" "is" "red" "+") ("something" "chases" "squirrel" "+")) -> ("something" "is" "kind" "+"))
The cat chases the squirrel.
True
1
proof
[(triple1 OR ((triple3) -> rule1) OR ((triple6 triple7) -> rule6) OR ((((triple7) -> rule5) triple6) -> rule4) OR ((((triple6 triple8) -> rule7) triple6) -> rule4))]
("cat" "chases" "squirrel" "+")
triple1
((triple3) -> (rule1 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((triple6 triple7) -> (rule6 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
((((triple6 triple8) -> (rule7 % int2)) triple6) -> (rule4 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The cat does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "eats" "squirrel" "-")
triple2
The squirrel eats the cat.
True
2
proof
[(((triple7) -> rule5) OR ((triple6 triple8) -> rule7) OR ((((triple1) -> rule2)) -> rule5) OR ((((((triple3) -> rule1)) -> rule2)) -> rule5))]
("squirrel" "eats" "cat" "+")
((triple7) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple6 triple8) -> (rule7 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int3
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple8) -> rule1))]
("squirrel" "chases" "squirrel" "-")
((triple8) -> (rule1 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is kind.
True
4
proof
[(((triple9 ((triple8) -> rule1)) -> rule8))]
("squirrel" "is" "kind" "+")
((triple9 ((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is not kind.
False
4
inv-proof
[(((triple9 ((triple8) -> rule1)) -> rule8))]
("squirrel" "is" "kind" "-")
((triple9 ((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "cat" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the squirrel.[(triple1 OR ((triple3) -> rule1) OR ((triple6 triple7) -> rule6) OR ((((triple7) -> rule5) triple6) -> rule4) OR ((((triple6 triple8) -> rule7) triple6) -> rule4))] The cat eats the squirrel.[(triple2)] The cat is blue.[(triple3)] The cat is kind.[(triple4 OR ((triple5 triple1) -> rule8) OR ((triple5 ((triple3) -> rule1)) -> rule8) OR ((triple5 ((triple6 triple7) -> rule6)) -> rule8) OR ((triple5 ((((triple7) -> rule5) triple6) -> rule4)) -> rule8) OR ((triple5 ((((triple6 triple8) -> rule7) triple6) -> rule4)) -> rule8))] The cat is red.[(triple5)] The cat needs the squirrel.[(triple6)] The squirrel chases the cat.[(triple7 OR ((triple1) -> rule2) OR ((((triple3) -> rule1)) -> rule2) OR ((((((triple6 triple8) -> rule7) triple6) -> rule4)) -> rule2))] The squirrel is blue.[(triple8)] The squirrel is red.[(triple9)] The squirrel needs the cat.[(triple10)] @1: The squirrel chases the squirrel.[(((triple8) -> rule1))] The squirrel eats the cat.[(((triple7) -> rule5) OR ((triple6 triple8) -> rule7) OR ((((triple1) -> rule2)) -> rule5) OR ((((((triple3) -> rule1)) -> rule2)) -> rule5))] @2: The squirrel is kind.[(((triple9 ((triple8) -> rule1)) -> rule8))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
((triple3) -> (rule1 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((triple6 triple7) -> (rule6 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
((((triple6 triple8) -> (rule7 % int2)) triple6) -> (rule4 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
((triple5 triple1) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple5 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
((triple5 ((triple6 triple7) -> (rule6 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3)) triple6) -> (rule4 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3
((triple5 ((((triple6 triple8) -> (rule7 % int3)) triple6) -> (rule4 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3
The cat is red.
("cat" "is" "red" "+")
triple5
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple6
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple7
((triple1) -> (rule2 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
((((((triple6 triple8) -> (rule7 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple8) -> (rule1 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple7) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple6 triple8) -> (rule7 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple9 ((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2