The cow chases the squirrel. The cow is cold. The cow sees the squirrel. The squirrel is big. The squirrel is cold. The squirrel needs the cow. The squirrel sees the cow. If something sees the cow and it is not kind then it needs the cow. If something needs the squirrel and it is cold then the squirrel chases the cow. All blue things are rough. If something chases the squirrel then the squirrel needs the cow. If something needs the cow then the cow needs the squirrel. If something chases the squirrel then the squirrel is rough. If something chases the cow and it sees the squirrel then the cow sees the squirrel. If something needs the cow and the cow is not rough then it sees the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If something sees the cow and it is not kind then it needs the cow.
((("something" "sees" "cow" "+") ("something" "is" "kind" "~")) -> ("something" "needs" "cow" "+"))
If something needs the squirrel and it is cold then the squirrel chases the cow.
((("something" "needs" "squirrel" "+") ("something" "is" "cold" "+")) -> ("squirrel" "chases" "cow" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something chases the squirrel then the squirrel needs the cow.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If something needs the cow then the cow needs the squirrel.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
If something chases the squirrel then the squirrel is rough.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If something chases the cow and it sees the squirrel then the cow sees the squirrel.
((("something" "chases" "cow" "+") ("something" "sees" "squirrel" "+")) -> ("cow" "sees" "squirrel" "+"))
If something needs the cow and the cow is not rough then it sees the squirrel.
((("something" "needs" "cow" "+") ("cow" "is" "rough" "~")) -> ("something" "sees" "squirrel" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The cow is not cold.
False
1
inv-proof
[(triple2)]
("cow" "is" "cold" "-")
triple2
The squirrel is rough.
True
2
proof
[(((triple1) -> rule6))]
("squirrel" "is" "rough" "+")
((triple1) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "is" "rough" "-")
((triple1) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the cow.
True
4
proof
[(((((triple6) -> rule5) triple2) -> rule2) OR ((((((triple1) -> rule4)) -> rule5) triple2) -> rule2))]
("squirrel" "chases" "cow" "+")
((((triple6) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The squirrel does not chase the cow.
False
4
inv-proof
[(((((triple6) -> rule5) triple2) -> rule2) OR ((((((triple1) -> rule4)) -> rule5) triple2) -> rule2))]
("squirrel" "chases" "cow" "-")
((((triple6) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "needs" "cow" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is cold.[(triple2)] The cow sees the squirrel.[(triple3)] The squirrel is big.[(triple4)] The squirrel is cold.[(triple5)] The squirrel needs the cow.[(triple6 OR ((triple1) -> rule4))] The squirrel sees the cow.[(triple7)] @1: The cow needs the squirrel.[(((triple6) -> rule5) OR ((((triple1) -> rule4)) -> rule5))] The squirrel is rough.[(((triple1) -> rule6))] @2: The squirrel chases the cow.[(((((triple6) -> rule5) triple2) -> rule2) OR ((((((triple1) -> rule4)) -> rule5) triple2) -> rule2))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple6
((triple1) -> (rule4 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple7
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple6) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple1) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
((((triple6) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3