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