The bear is big. The squirrel sees the bear. If someone sees the squirrel then the squirrel needs the bear. If someone needs the bear then they are green. If someone is big then they need the bear.
The bear is big.
("bear" "is" "big" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the squirrel then the squirrel needs the bear.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
If someone needs the bear then they are green.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they need the bear.
((("someone" "is" "big" "+")) -> ("someone" "needs" "bear" "+"))
The bear is big.
True
1
proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear needs the bear.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "bear" "-")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("bear" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("bear" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The squirrel does not need the bear.
Unknown
inv-rconc
[@1: The squirrel needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "bear" "-")
The squirrel is green.
Unknown
rconc
[@2: The squirrel is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("squirrel" "is" "green" "+")
The bear does not chase the squirrel.
Unknown
inv-random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The bear is big.[(triple1)] The squirrel sees the bear.[(triple2)] @1: The bear needs the bear.[(((triple1) -> rule3))] @2: The bear is green.[(((((triple1) -> rule3)) -> rule2))]
The bear is big.
("bear" "is" "big" "+")
triple1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple2
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2