The bear chases the cat. The bear eats the cat. The cat likes the squirrel. The lion eats the cat. The lion eats the squirrel. The lion likes the cat. The squirrel is not blue. If someone is big then they like the squirrel. If someone eats the lion and they do not eat the cat then the cat eats the squirrel. If someone likes the squirrel and they are rough then the squirrel is big. If someone is rough then they like the lion. If someone likes the squirrel and the squirrel is not blue then they are rough. If the bear does not like the squirrel then the squirrel likes the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
If someone is big then they like the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone eats the lion and they do not eat the cat then the cat eats the squirrel.
((("someone" "eats" "lion" "+") ("someone" "eats" "cat" "~")) -> ("cat" "eats" "squirrel" "+"))
If someone likes the squirrel and they are rough then the squirrel is big.
((("someone" "likes" "squirrel" "+") ("someone" "is" "rough" "+")) -> ("squirrel" "is" "big" "+"))
If someone is rough then they like the lion.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the squirrel and the squirrel is not blue then they are rough.
((("someone" "likes" "squirrel" "+") ("squirrel" "is" "blue" "~")) -> ("someone" "is" "rough" "+"))
If the bear does not like the squirrel then the squirrel likes the cat.
((("bear" "likes" "squirrel" "~")) -> ("squirrel" "likes" "cat" "+"))
The lion eats the cat.
True
1
proof
[(triple4)]
("lion" "eats" "cat" "+")
triple4
The squirrel is blue.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "blue" "+")
triple7
The cat is rough.
True
3
proof
[(((triple3 triple7) -> rule5))]
("cat" "is" "rough" "+")
((triple3 triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
3
inv-proof
[(((triple3 triple7) -> rule5))]
("cat" "is" "rough" "-")
((triple3 triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the lion.
True
4
proof
[(((((triple3 triple7) -> rule5)) -> rule4))]
("cat" "likes" "lion" "+")
((((triple3 triple7) -> (rule5 % int2))) -> (rule4 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel is not big.
False
5
inv-proof
[(((triple3 ((triple3 triple7) -> rule5)) -> rule3))]
("squirrel" "is" "big" "-")
((triple3 ((triple3 triple7) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel likes the squirrel.
True
6
proof
[(((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((((triple3 ((triple3 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The squirrel does not like the squirrel.
False
6
inv-proof
[(((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((((triple3 ((triple3 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The squirrel is rough.
True
8
proof
[(((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5))]
("squirrel" "is" "rough" "+")
((((((triple3 ((triple3 triple7) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The squirrel is not rough.
False
8
inv-proof
[(((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5))]
("squirrel" "is" "rough" "-")
((((((triple3 ((triple3 triple7) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The squirrel likes the lion.
True
9
proof
[(((((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5)) -> rule4))]
("squirrel" "likes" "lion" "+")
((((((((triple3 ((triple3 triple7) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5
The squirrel does not like the lion.
False
9
inv-proof
[(((((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5)) -> rule4))]
("squirrel" "likes" "lion" "-")
((((((((triple3 ((triple3 triple7) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5
The lion does not like the lion.
Unknown
inv-rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("lion" "likes" "lion" "-")
The bear likes the lion.
Unknown
rconc
[@2: The bear likes the lion.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("bear" "likes" "lion" "+")
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The lion likes the squirrel.
Unknown
rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "squirrel" "+")
The squirrel does not like the cat.
Unknown
inv-rconc
[@1: The squirrel likes the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "cat" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The lion does not eat the bear.
Unknown
inv-random
[@0: The lion eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The bear does not chase the squirrel.
Unknown
inv-random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "-")
The squirrel eats the bear.
Unknown
random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "+")
@0: The bear chases the cat.[(triple1)] The bear eats the cat.[(triple2)] The cat likes the squirrel.[(triple3)] The lion eats the cat.[(triple4)] The lion eats the squirrel.[(triple5)] The lion likes the cat.[(triple6)] The squirrel is not blue.[(triple7)] @1: The cat is rough.[(((triple3 triple7) -> rule5))] @2: The cat likes the lion.[(((((triple3 triple7) -> rule5)) -> rule4))] The squirrel is big.[(((triple3 ((triple3 triple7) -> rule5)) -> rule3))] @3: The squirrel likes the squirrel.[(((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1))] @4: The squirrel is rough.[(((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5))] @5: The squirrel likes the lion.[(((((((((triple3 ((triple3 triple7) -> rule5)) -> rule3)) -> rule1) triple7) -> rule5)) -> rule4))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear eats the cat.
("bear" "eats" "cat" "+")
triple2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple3
The lion eats the cat.
("lion" "eats" "cat" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion likes the cat.
("lion" "likes" "cat" "+")
triple6
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple7
The cat is rough.
("cat" "is" "rough" "+")
((triple3 triple7) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
((((triple3 triple7) -> (rule5 % int2))) -> (rule4 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((triple3 ((triple3 triple7) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple3 ((triple3 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((((triple3 ((triple3 triple7) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((((((((triple3 ((triple3 triple7) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5