The bear sees the squirrel. The squirrel is rough. The squirrel sees the bear. If someone is green then they need the bear. If someone needs the bear then they are cold. If someone sees the squirrel then the squirrel likes the bear. If someone likes the bear then they need the bear. If someone likes the bear and they see the squirrel then they see the bear. If someone likes the squirrel and the squirrel needs the bear then they see the squirrel.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone is green then they need the bear.
((("someone" "is" "green" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear then they are cold.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the squirrel then the squirrel likes the bear.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "likes" "bear" "+"))
If someone likes the bear then they need the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone likes the bear and they see the squirrel then they see the bear.
((("someone" "likes" "bear" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "bear" "+"))
If someone likes the squirrel and the squirrel needs the bear then they see the squirrel.
((("someone" "likes" "squirrel" "+") ("squirrel" "needs" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple3)]
("squirrel" "sees" "bear" "+")
triple3
The bear does not see the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "sees" "squirrel" "-")
triple1
The squirrel likes the bear.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "likes" "bear" "+")
((triple1) -> (rule3 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel does not like the bear.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "likes" "bear" "-")
((triple1) -> (rule3 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel needs the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("squirrel" "needs" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel does not need the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("squirrel" "needs" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is cold.
True
4
proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule2))]
("squirrel" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The squirrel is not cold.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule2))]
("squirrel" "is" "cold" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear is not cold.
Unknown
inv-rconc
[@2: The bear is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bear" "is" "cold" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "bear" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "+")
The bear does not like the squirrel.
Unknown
inv-random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear sees the squirrel.[(triple1)] The squirrel is rough.[(triple2)] The squirrel sees the bear.[(triple3)] @1: The squirrel likes the bear.[(((triple1) -> rule3))] @2: The squirrel needs the bear.[(((((triple1) -> rule3)) -> rule4))] @3: The squirrel is cold.[(((((((triple1) -> rule3)) -> rule4)) -> rule2))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((triple1) -> (rule3 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3