The bear is green. The bear needs the cow. The cow eats the bear. The cow eats the squirrel. The cow eats the tiger. The cow needs the squirrel. The squirrel is young. The squirrel needs the bear. The tiger needs the cow. The tiger sees the cow. If someone eats the squirrel then they see the tiger. If the cow eats the squirrel and the cow sees the tiger then the squirrel needs the cow.
The bear is green.
("bear" "is" "green" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone eats the squirrel then they see the tiger.
((("someone" "eats" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If the cow eats the squirrel and the cow sees the tiger then the squirrel needs the cow.
((("cow" "eats" "squirrel" "+") ("cow" "sees" "tiger" "+")) -> ("squirrel" "needs" "cow" "+"))
The bear needs the cow.
True
1
proof
[(triple2)]
("bear" "needs" "cow" "+")
triple2
The squirrel does not need the bear.
False
1
inv-proof
[(triple8)]
("squirrel" "needs" "bear" "-")
triple8
The cow sees the tiger.
True
2
proof
[(((triple4) -> rule1))]
("cow" "sees" "tiger" "+")
((triple4) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "sees" "tiger" "-")
((triple4) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The squirrel needs the cow.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("squirrel" "needs" "cow" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The squirrel does not need the cow.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("squirrel" "needs" "cow" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The squirrel does not see the tiger.
Unknown
inv-rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "tiger" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The bear is green.[(triple1)] The bear needs the cow.[(triple2)] The cow eats the bear.[(triple3)] The cow eats the squirrel.[(triple4)] The cow eats the tiger.[(triple5)] The cow needs the squirrel.[(triple6)] The squirrel is young.[(triple7)] The squirrel needs the bear.[(triple8)] The tiger needs the cow.[(triple9)] The tiger sees the cow.[(triple10)] @1: The cow sees the tiger.[(((triple4) -> rule1))] @2: The squirrel needs the cow.[(((triple4 ((triple4) -> rule1)) -> rule2))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple4
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple5
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple6
The squirrel is young.
("squirrel" "is" "young" "+")
triple7
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple8
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple4) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2