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