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