The cow chases the squirrel. The cow is blue. The cow is cold. The cow is green. The cow is round. The cow needs the squirrel. The cow sees the squirrel. The squirrel chases the cow. The squirrel is round. The squirrel needs the cow. If something sees the squirrel then it is blue. If something chases the cow and it chases the squirrel then it sees the cow. If something sees the cow then it is cold. If something needs the cow then it needs the squirrel. If something needs the cow then it chases the squirrel. If something sees the squirrel then the squirrel needs the cow. If something is rough and it does not need the cow then the cow needs the squirrel. If the squirrel sees the cow and the cow needs the squirrel then the squirrel is blue.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If something sees the squirrel then it is blue.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "blue" "+"))
If something chases the cow and it chases the squirrel then it sees the cow.
((("something" "chases" "cow" "+") ("something" "chases" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it is cold.
((("something" "sees" "cow" "+")) -> ("something" "is" "cold" "+"))
If something needs the cow then it needs the squirrel.
((("something" "needs" "cow" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the cow then it chases the squirrel.
((("something" "needs" "cow" "+")) -> ("something" "chases" "squirrel" "+"))
If something sees the squirrel then the squirrel needs the cow.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If something is rough and it does not need the cow then the cow needs the squirrel.
((("something" "is" "rough" "+") ("something" "needs" "cow" "~")) -> ("cow" "needs" "squirrel" "+"))
If the squirrel sees the cow and the cow needs the squirrel then the squirrel is blue.
((("squirrel" "sees" "cow" "+") ("cow" "needs" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
The cow needs the squirrel.
True
1
proof
[(triple6)]
("cow" "needs" "squirrel" "+")
triple6
The squirrel does not need the cow.
False
1
inv-proof
[(triple10 OR ((triple7) -> rule6))]
("squirrel" "needs" "cow" "-")
triple10
((triple7) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel chases the squirrel.
True
2
proof
[(((triple10) -> rule5) OR ((((triple7) -> rule6)) -> rule5))]
("squirrel" "chases" "squirrel" "+")
((triple10) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((triple7) -> rule6)) -> rule4))]
("squirrel" "needs" "squirrel" "-")
((triple10) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel sees the cow.
True
4
proof
[(((triple8 ((triple10) -> rule5)) -> rule2) OR ((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2))]
("squirrel" "sees" "cow" "+")
((triple8 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((triple8 ((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The squirrel does not see the cow.
False
4
inv-proof
[(((triple8 ((triple10) -> rule5)) -> rule2) OR ((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2))]
("squirrel" "sees" "cow" "-")
((triple8 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((triple8 ((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The squirrel is blue.
True
6
proof
[(((((triple8 ((triple10) -> rule5)) -> rule2) triple6) -> rule8) OR ((((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2) triple6) -> rule8))]
("squirrel" "is" "blue" "+")
((((triple8 ((triple10) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((((triple8 ((((triple7) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int4
The squirrel is not cold.
False
5
inv-proof
[(((((triple8 ((triple10) -> rule5)) -> rule2)) -> rule3) OR ((((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2)) -> rule3))]
("squirrel" "is" "cold" "-")
((((triple8 ((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((((triple8 ((((triple7) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int4
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cow" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
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 cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is blue.[(triple2 OR ((triple7) -> rule1))] The cow is cold.[(triple3)] The cow is green.[(triple4)] The cow is round.[(triple5)] The cow needs the squirrel.[(triple6)] The cow sees the squirrel.[(triple7)] The squirrel chases the cow.[(triple8)] The squirrel is round.[(triple9)] The squirrel needs the cow.[(triple10 OR ((triple7) -> rule6))] @1: The squirrel chases the squirrel.[(((triple10) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] The squirrel needs the squirrel.[(((triple10) -> rule4) OR ((((triple7) -> rule6)) -> rule4))] @2: The squirrel sees the cow.[(((triple8 ((triple10) -> rule5)) -> rule2) OR ((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2))] @3: The squirrel is blue.[(((((triple8 ((triple10) -> rule5)) -> rule2) triple6) -> rule8) OR ((((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2) triple6) -> rule8))] The squirrel is cold.[(((((triple8 ((triple10) -> rule5)) -> rule2)) -> rule3) OR ((((triple8 ((((triple7) -> rule6)) -> rule5)) -> rule2)) -> rule3))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
((triple7) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple6
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple7
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
((triple7) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple10) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple10) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple8 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((triple8 ((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple8 ((triple10) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((((triple8 ((((triple7) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int4
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple8 ((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((((triple8 ((((triple7) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int4