The bear chases the squirrel. The bear is nice. The bear likes the cow. The bear likes the squirrel. The bear needs the cow. The bear needs the squirrel. The cow is green. The squirrel is green. The tiger likes the cow. The tiger needs the squirrel. If someone likes the tiger and they need the squirrel then the squirrel likes the bear. If someone is green then they like the squirrel. If the bear is nice then the bear likes the tiger. If someone likes the bear and the bear needs the squirrel then the bear chases the cow. If the tiger needs the squirrel then the tiger likes the cow. If someone needs the cow then the cow chases the tiger.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cow is green.
("cow" "is" "green" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone likes the tiger and they need the squirrel then the squirrel likes the bear.
((("someone" "likes" "tiger" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "likes" "bear" "+"))
If someone is green then they like the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "likes" "squirrel" "+"))
If the bear is nice then the bear likes the tiger.
((("bear" "is" "nice" "+")) -> ("bear" "likes" "tiger" "+"))
If someone likes the bear and the bear needs the squirrel then the bear chases the cow.
((("someone" "likes" "bear" "+") ("bear" "needs" "squirrel" "+")) -> ("bear" "chases" "cow" "+"))
If the tiger needs the squirrel then the tiger likes the cow.
((("tiger" "needs" "squirrel" "+")) -> ("tiger" "likes" "cow" "+"))
If someone needs the cow then the cow chases the tiger.
((("someone" "needs" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
The tiger likes the cow.
True
1
proof
[(triple9 OR ((triple10) -> rule5))]
("tiger" "likes" "cow" "+")
triple9
((triple10) -> (rule5 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The bear does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "chases" "squirrel" "-")
triple1
The cow likes the squirrel.
True
2
proof
[(((triple7) -> rule2))]
("cow" "likes" "squirrel" "+")
((triple7) -> (rule2 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow does not chase the tiger.
False
2
inv-proof
[(((triple5) -> rule6))]
("cow" "chases" "tiger" "-")
((triple5) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The squirrel likes the bear.
True
4
proof
[(((((triple2) -> rule3) triple6) -> rule1))]
("squirrel" "likes" "bear" "+")
((((triple2) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The squirrel does not like the bear.
False
4
inv-proof
[(((((triple2) -> rule3) triple6) -> rule1))]
("squirrel" "likes" "bear" "-")
((((triple2) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear chases the cow.
True
6
proof
[(((((((triple2) -> rule3) triple6) -> rule1) triple6) -> rule4))]
("bear" "chases" "cow" "+")
((((((triple2) -> (rule3 % int3)) triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The bear does not chase the cow.
False
6
inv-proof
[(((((((triple2) -> rule3) triple6) -> rule1) triple6) -> rule4))]
("bear" "chases" "cow" "-")
((((((triple2) -> (rule3 % int3)) triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The tiger does not like the squirrel.
Unknown
inv-rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "squirrel" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
The squirrel does not need the bear.
Unknown
inv-random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The squirrel likes the tiger.
Unknown
random
[@0: The squirrel likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "tiger" "+")
@0: The bear chases the squirrel.[(triple1)] The bear is nice.[(triple2)] The bear likes the cow.[(triple3)] The bear likes the squirrel.[(triple4)] The bear needs the cow.[(triple5)] The bear needs the squirrel.[(triple6)] The cow is green.[(triple7)] The squirrel is green.[(triple8)] The tiger likes the cow.[(triple9 OR ((triple10) -> rule5))] The tiger needs the squirrel.[(triple10)] @1: The bear likes the tiger.[(((triple2) -> rule3))] The cow chases the tiger.[(((triple5) -> rule6))] The cow likes the squirrel.[(((triple7) -> rule2))] The squirrel likes the squirrel.[(((triple8) -> rule2))] @2: The squirrel likes the bear.[(((((triple2) -> rule3) triple6) -> rule1))] @3: The bear chases the cow.[(((((((triple2) -> rule3) triple6) -> rule1) triple6) -> rule4))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear likes the cow.
("bear" "likes" "cow" "+")
triple3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple4
The bear needs the cow.
("bear" "needs" "cow" "+")
triple5
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple6
The cow is green.
("cow" "is" "green" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple9
((triple10) -> (rule5 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple10
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple2) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple5) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((triple7) -> (rule2 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple8) -> (rule2 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((((triple2) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
((((((triple2) -> (rule3 % int3)) triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3