The bear is green. The bear is red. The bear likes the cow. The bear likes the squirrel. The bear needs the cow. The bear sees the squirrel. The cow does not like the squirrel. The cow needs the bear. The cow sees the bear. The cow sees the squirrel. The squirrel is green. The squirrel sees the bear. If the bear is not kind then the bear needs the squirrel. If the squirrel likes the bear then the squirrel needs the bear. If the bear needs the cow and the bear does not see the squirrel then the squirrel does not need the bear. If someone sees the bear then they need the bear. If someone likes the cow and the cow needs the bear then the cow is not green. If the cow sees the bear and the squirrel does not see the cow then the bear likes the cow. If the cow likes the bear then the bear needs the cow. If someone needs the bear then they like the cow.
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
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 sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow does not like the squirrel.
("cow" "likes" "squirrel" "-")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If the bear is not kind then the bear needs the squirrel.
((("bear" "is" "kind" "~")) -> ("bear" "needs" "squirrel" "+"))
If the squirrel likes the bear then the squirrel needs the bear.
((("squirrel" "likes" "bear" "+")) -> ("squirrel" "needs" "bear" "+"))
If the bear needs the cow and the bear does not see the squirrel then the squirrel does not need the bear.
((("bear" "needs" "cow" "+") ("bear" "sees" "squirrel" "~")) -> ("squirrel" "needs" "bear" "-"))
If someone sees the bear then they need the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone likes the cow and the cow needs the bear then the cow is not green.
((("someone" "likes" "cow" "+") ("cow" "needs" "bear" "+")) -> ("cow" "is" "green" "-"))
If the cow sees the bear and the squirrel does not see the cow then the bear likes the cow.
((("cow" "sees" "bear" "+") ("squirrel" "sees" "cow" "~")) -> ("bear" "likes" "cow" "+"))
If the cow likes the bear then the bear needs the cow.
((("cow" "likes" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If someone needs the bear then they like the cow.
((("someone" "needs" "bear" "+")) -> ("someone" "likes" "cow" "+"))
The bear is green.
True
1
proof
[(triple1)]
("bear" "is" "green" "+")
triple1
The bear does not need the cow.
False
1
inv-proof
[(triple5)]
("bear" "needs" "cow" "-")
triple5
The squirrel needs the bear.
True
2
proof
[(((triple12) -> rule4))]
("squirrel" "needs" "bear" "+")
((triple12) -> (rule4 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple8) -> rule8) OR ((((triple9) -> rule4)) -> rule8))]
("cow" "likes" "cow" "-")
((triple8) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The squirrel likes the cow.
True
3
proof
[(((((triple12) -> rule4)) -> rule8))]
("squirrel" "likes" "cow" "+")
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel does not like the cow.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule8))]
("squirrel" "likes" "cow" "-")
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear needs the squirrel.
Unknown
rconc
[@1: The bear needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "squirrel" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
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 likes the bear.
Unknown
random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "+")
@0: The bear is green.[(triple1)] The bear is red.[(triple2)] The bear likes the cow.[(triple3)] The bear likes the squirrel.[(triple4)] The bear needs the cow.[(triple5)] The bear sees the squirrel.[(triple6)] The cow does not like the squirrel.[(triple7)] The cow needs the bear.[(triple8 OR ((triple9) -> rule4))] The cow sees the bear.[(triple9)] The cow sees the squirrel.[(triple10)] The squirrel is green.[(triple11)] The squirrel sees the bear.[(triple12)] @1: The cow is not green.[(((triple3 triple8) -> rule5) OR ((triple3 ((triple9) -> rule4)) -> rule5) OR ((((triple8) -> rule8) triple8) -> rule5) OR ((((triple8) -> rule8) ((triple9) -> rule4)) -> rule5) OR ((((((triple12) -> rule4)) -> rule8) triple8) -> rule5) OR ((((((triple9) -> rule4)) -> rule8) triple8) -> rule5) OR ((((((triple12) -> rule4)) -> rule8) ((triple9) -> rule4)) -> rule5) OR ((((((triple9) -> rule4)) -> rule8) ((triple9) -> rule4)) -> rule5))] The cow likes the cow.[(((triple8) -> rule8) OR ((((triple9) -> rule4)) -> rule8))] The squirrel needs the bear.[(((triple12) -> rule4))] @2: The squirrel likes the cow.[(((((triple12) -> rule4)) -> rule8))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
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 sees the squirrel.
("bear" "sees" "squirrel" "+")
triple6
The cow does not like the squirrel.
("cow" "likes" "squirrel" "-")
triple7
The cow needs the bear.
("cow" "needs" "bear" "+")
triple8
((triple9) -> (rule4 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple9
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple12
The cow is not green.
("cow" "is" "green" "-")
((triple3 triple8) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
((triple3 ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
((((triple8) -> (rule8 % int2)) triple8) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((((triple8) -> (rule8 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
((((((triple12) -> (rule4 % int3))) -> (rule8 % int2)) triple8) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule8 % int2)) triple8) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
((((((triple12) -> (rule4 % int4))) -> (rule8 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int3))) -> (rule8 % int2)) ((triple9) -> (rule4 % int3))) -> (rule5 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple8) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple12) -> (rule4 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2