The bear eats the squirrel. The bear is blue. The bear is cold. The bear is not green. The bear is rough. The bear needs the squirrel. The bear does not see the squirrel. The squirrel eats the bear. The squirrel is cold. The squirrel is red. The squirrel is rough. The squirrel needs the bear. If someone is rough and they eat the squirrel then the squirrel is not green. If someone sees the squirrel then they need the squirrel. If someone eats the bear then the bear does not see the squirrel. If someone needs the squirrel and they do not see the squirrel then they do not see the bear. If someone sees the bear then the bear does not need the squirrel. If someone needs the squirrel and they do not see the bear then they do not need the bear. If the bear eats the squirrel and the squirrel does not see the bear then the squirrel needs the bear. If someone needs the bear and the bear is not cold then they are not green.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is not green.
("bear" "is" "green" "-")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If someone is rough and they eat the squirrel then the squirrel is not green.
((("someone" "is" "rough" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "green" "-"))
If someone sees the squirrel then they need the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone eats the bear then the bear does not see the squirrel.
((("someone" "eats" "bear" "+")) -> ("bear" "sees" "squirrel" "-"))
If someone needs the squirrel and they do not see the squirrel then they do not see the bear.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "squirrel" "~")) -> ("someone" "sees" "bear" "-"))
If someone sees the bear then the bear does not need the squirrel.
((("someone" "sees" "bear" "+")) -> ("bear" "needs" "squirrel" "-"))
If someone needs the squirrel and they do not see the bear then they do not need the bear.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "bear" "~")) -> ("someone" "needs" "bear" "-"))
If the bear eats the squirrel and the squirrel does not see the bear then the squirrel needs the bear.
((("bear" "eats" "squirrel" "+") ("squirrel" "sees" "bear" "~")) -> ("squirrel" "needs" "bear" "+"))
If someone needs the bear and the bear is not cold then they are not green.
((("someone" "needs" "bear" "+") ("bear" "is" "cold" "~")) -> ("someone" "is" "green" "-"))
The squirrel needs the bear.
True
1
proof
[(triple12)]
("squirrel" "needs" "bear" "+")
triple12
The squirrel does not eat the bear.
False
1
inv-proof
[(triple8)]
("squirrel" "eats" "bear" "-")
triple8
The bear does not see the bear.
True
3
proof
[(((triple6 triple7) -> rule4) OR ((triple6 ((triple8) -> rule3)) -> rule4))]
("bear" "sees" "bear" "-")
((triple6 triple7) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
((triple6 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int2
The bear sees the bear.
False
3
inv-proof
[(((triple6 triple7) -> rule4) OR ((triple6 ((triple8) -> rule3)) -> rule4))]
("bear" "sees" "bear" "+")
((triple6 triple7) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
((triple6 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int2
The bear does not need the bear.
True
5
proof
[(((triple6 ((triple6 triple7) -> rule4)) -> rule6) OR ((triple6 ((triple6 ((triple8) -> rule3)) -> rule4)) -> rule6))]
("bear" "needs" "bear" "-")
((triple6 ((triple6 triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
((triple6 ((triple6 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int3
The bear needs the bear.
False
5
inv-proof
[(((triple6 ((triple6 triple7) -> rule4)) -> rule6) OR ((triple6 ((triple6 ((triple8) -> rule3)) -> rule4)) -> rule6))]
("bear" "needs" "bear" "+")
((triple6 ((triple6 triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
((triple6 ((triple6 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear does not see the squirrel.[(triple7 OR ((triple8) -> rule3))] The bear eats the squirrel.[(triple1)] The bear is blue.[(triple2)] The bear is cold.[(triple3)] The bear is not green.[(triple4)] The bear is rough.[(triple5)] The bear needs the squirrel.[(triple6)] The squirrel eats the bear.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is red.[(triple10)] The squirrel is rough.[(triple11)] The squirrel needs the bear.[(triple12)] @1: The bear does not see the bear.[(((triple6 triple7) -> rule4) OR ((triple6 ((triple8) -> rule3)) -> rule4))] The squirrel is not green.[(((triple5 triple1) -> rule1))] @2: The bear does not need the bear.[(((triple6 ((triple6 triple7) -> rule4)) -> rule6) OR ((triple6 ((triple6 ((triple8) -> rule3)) -> rule4)) -> rule6))]
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
triple7
((triple8) -> (rule3 % int1))
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is not green.
("bear" "is" "green" "-")
triple4
The bear is rough.
("bear" "is" "rough" "+")
triple5
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple6
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple12
The bear does not see the bear.
("bear" "sees" "bear" "-")
((triple6 triple7) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
((triple6 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int2
The squirrel is not green.
("squirrel" "is" "green" "-")
((triple5 triple1) -> (rule1 % int1))
The squirrel is not green.
("squirrel" "is" "green" "-")
int1
The bear does not need the bear.
("bear" "needs" "bear" "-")
((triple6 ((triple6 triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
((triple6 ((triple6 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
int3