The cat eats the squirrel. The rabbit is blue. The rabbit is kind. The rabbit is red. The rabbit likes the squirrel. The squirrel is blue. The squirrel is nice. If something is kind then it eats the squirrel. If something needs the rabbit and the rabbit eats the squirrel then the rabbit likes the cat. If something is young and it needs the squirrel then the squirrel is kind. If the cat eats the squirrel and the squirrel likes the rabbit then the squirrel eats the rabbit. If something is blue and nice then it likes the squirrel. If the squirrel is blue then the squirrel is young. If something is kind then it eats the cat. If something eats the cat then the cat needs the rabbit.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something is kind then it eats the squirrel.
((("something" "is" "kind" "+")) -> ("something" "eats" "squirrel" "+"))
If something needs the rabbit and the rabbit eats the squirrel then the rabbit likes the cat.
((("something" "needs" "rabbit" "+") ("rabbit" "eats" "squirrel" "+")) -> ("rabbit" "likes" "cat" "+"))
If something is young and it needs the squirrel then the squirrel is kind.
((("something" "is" "young" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If the cat eats the squirrel and the squirrel likes the rabbit then the squirrel eats the rabbit.
((("cat" "eats" "squirrel" "+") ("squirrel" "likes" "rabbit" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If something is blue and nice then it likes the squirrel.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "likes" "squirrel" "+"))
If the squirrel is blue then the squirrel is young.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "is" "young" "+"))
If something is kind then it eats the cat.
((("something" "is" "kind" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat then the cat needs the rabbit.
((("something" "eats" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
The rabbit is red.
True
1
proof
[(triple4)]
("rabbit" "is" "red" "+")
triple4
The cat does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "eats" "squirrel" "-")
triple1
The rabbit eats the cat.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "eats" "cat" "+")
((triple3) -> (rule7 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "eats" "squirrel" "-")
((triple3) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The cat needs the rabbit.
True
3
proof
[(((((triple3) -> rule7)) -> rule8))]
("cat" "needs" "rabbit" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The cat does not need the rabbit.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule8))]
("cat" "needs" "rabbit" "-")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The rabbit likes the cat.
True
6
proof
[(((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule1)) -> rule2))]
("rabbit" "likes" "cat" "+")
((((((triple3) -> (rule7 % int4))) -> (rule8 % int3)) ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int4
The rabbit does not like the cat.
False
6
inv-proof
[(((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule1)) -> rule2))]
("rabbit" "likes" "cat" "-")
((((((triple3) -> (rule7 % int4))) -> (rule8 % int3)) ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int4
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "eats" "cat" "-")
The cat likes the squirrel.
Unknown
rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "squirrel" "+")
The squirrel does not eat the rabbit.
Unknown
inv-rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "rabbit" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The cat does not like the rabbit.
Unknown
inv-random
[@0: The cat likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "rabbit" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the squirrel.[(triple1)] The rabbit is blue.[(triple2)] The rabbit is kind.[(triple3)] The rabbit is red.[(triple4)] The rabbit likes the squirrel.[(triple5)] The squirrel is blue.[(triple6)] The squirrel is nice.[(triple7)] @1: The rabbit eats the cat.[(((triple3) -> rule7))] The rabbit eats the squirrel.[(((triple3) -> rule1))] The squirrel is young.[(((triple6) -> rule6))] The squirrel likes the squirrel.[(((triple6 triple7) -> rule5))] @2: The cat needs the rabbit.[(((((triple3) -> rule7)) -> rule8))] @3: The rabbit likes the cat.[(((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule1)) -> rule2))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple6
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((triple3) -> (rule7 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((triple6) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple6 triple7) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((((((triple3) -> (rule7 % int4))) -> (rule8 % int3)) ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int4