The cat eats the cow. The cat is not nice. The cat needs the squirrel. The cat does not see the squirrel. The cow is kind. The cow is nice. The cow needs the cat. The cow sees the cat. The cow sees the squirrel. The rabbit is nice. The squirrel eats the cow. The squirrel sees the cat. If the cat is red then the cat is nice. If something is cold and kind then it eats the cow. If the cow is nice and the cow eats the rabbit then the cow sees the rabbit. If the cat sees the rabbit then the rabbit sees the cat. If something needs the cat and the cat eats the cow then it eats the rabbit. If something sees the rabbit and the rabbit is blue then it is nice. If something eats the cow then it needs the cow. If something sees the rabbit then it sees the cow. If something sees the cow then it is cold.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the cat is red then the cat is nice.
((("cat" "is" "red" "+")) -> ("cat" "is" "nice" "+"))
If something is cold and kind then it eats the cow.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "eats" "cow" "+"))
If the cow is nice and the cow eats the rabbit then the cow sees the rabbit.
((("cow" "is" "nice" "+") ("cow" "eats" "rabbit" "+")) -> ("cow" "sees" "rabbit" "+"))
If the cat sees the rabbit then the rabbit sees the cat.
((("cat" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something needs the cat and the cat eats the cow then it eats the rabbit.
((("something" "needs" "cat" "+") ("cat" "eats" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the rabbit and the rabbit is blue then it is nice.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something eats the cow then it needs the cow.
((("something" "eats" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something sees the rabbit then it sees the cow.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it is cold.
((("something" "sees" "cow" "+")) -> ("something" "is" "cold" "+"))
The cat needs the squirrel.
True
1
proof
[(triple3)]
("cat" "needs" "squirrel" "+")
triple3
The rabbit is not nice.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "nice" "-")
triple10
The cow eats the rabbit.
True
3
proof
[(((triple7 triple1) -> rule5))]
("cow" "eats" "rabbit" "+")
((triple7 triple1) -> (rule5 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The squirrel does not need the cow.
False
2
inv-proof
[(((triple11) -> rule7))]
("squirrel" "needs" "cow" "-")
((triple11) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow sees the rabbit.
True
5
proof
[(((triple6 ((triple7 triple1) -> rule5)) -> rule3))]
("cow" "sees" "rabbit" "+")
((triple6 ((triple7 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow does not see the rabbit.
False
5
inv-proof
[(((triple6 ((triple7 triple1) -> rule5)) -> rule3))]
("cow" "sees" "rabbit" "-")
((triple6 ((triple7 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow sees the cow.
True
6
proof
[(((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8))]
("cow" "sees" "cow" "+")
((((triple6 ((triple7 triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow does not see the cow.
False
6
inv-proof
[(((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8))]
("cow" "sees" "cow" "-")
((((triple6 ((triple7 triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow is cold.
True
7
proof
[(((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9))]
("cow" "is" "cold" "+")
((((((triple6 ((triple7 triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4
The cow is not cold.
False
7
inv-proof
[(((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9))]
("cow" "is" "cold" "-")
((((((triple6 ((triple7 triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4
The cow eats the cow.
True
9
proof
[(((((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9) triple5) -> rule2))]
("cow" "eats" "cow" "+")
((((((((triple6 ((triple7 triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) triple5) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int5
The cow does not eat the cow.
False
9
inv-proof
[(((((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9) triple5) -> rule2))]
("cow" "eats" "cow" "-")
((((((((triple6 ((triple7 triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) triple5) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int5
The squirrel does not see the cow.
Unknown
inv-rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "sees" "cow" "-")
The squirrel is cold.
Unknown
rconc
[@2: The squirrel is cold.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("squirrel" "is" "cold" "+")
The cat is not cold.
Unknown
inv-rconc
[@2: The cat is cold.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("cat" "is" "cold" "-")
The squirrel eats the rabbit.
Unknown
rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "rabbit" "+")
The rabbit does not need the cow.
Unknown
inv-rconc
[@2: The rabbit needs the cow.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("rabbit" "needs" "cow" "-")
The cat sees the cow.
Unknown
rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "sees" "cow" "+")
The rabbit does not need the cat.
Unknown
inv-random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "-")
The squirrel needs the cat.
Unknown
random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "+")
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 sees the rabbit.
Unknown
random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The cat does not see the squirrel.[(triple4)] The cat eats the cow.[(triple1)] The cat is not nice.[(triple2)] The cat needs the squirrel.[(triple3)] The cow is kind.[(triple5)] The cow is nice.[(triple6)] The cow needs the cat.[(triple7)] The cow sees the cat.[(triple8)] The cow sees the squirrel.[(triple9)] The rabbit is nice.[(triple10)] The squirrel eats the cow.[(triple11)] The squirrel sees the cat.[(triple12)] @1: The cat needs the cow.[(((triple1) -> rule7))] The cow eats the rabbit.[(((triple7 triple1) -> rule5))] The squirrel needs the cow.[(((triple11) -> rule7))] @2: The cow sees the rabbit.[(((triple6 ((triple7 triple1) -> rule5)) -> rule3))] @3: The cow sees the cow.[(((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8))] @4: The cow is cold.[(((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9))] @5: The cow eats the cow.[(((((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9) triple5) -> rule2))] @6: The cow needs the cow.[(((((((((((triple6 ((triple7 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule9) triple5) -> rule2)) -> rule7))]
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple4
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow is nice.
("cow" "is" "nice" "+")
triple6
The cow needs the cat.
("cow" "needs" "cat" "+")
triple7
The cow sees the cat.
("cow" "sees" "cat" "+")
triple8
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple11
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple12
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple1) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple7 triple1) -> (rule5 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple11) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple6 ((triple7 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple6 ((triple7 triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
((((((triple6 ((triple7 triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((((triple6 ((triple7 triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) triple5) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int5
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((((((triple6 ((triple7 triple1) -> (rule5 % int6))) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule9 % int3)) triple5) -> (rule2 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int5
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int6