The cow is red. The squirrel needs the cow. The squirrel sees the cow. If the squirrel sees the cow then the cow needs the squirrel. If the cow sees the squirrel and the cow is big then the squirrel is red. If something sees the cow then it eats the cow. If something is red then it eats the cow. If the cow sees the squirrel then the cow eats the squirrel. If something eats the cow then it sees the squirrel.
The cow is red.
("cow" "is" "red" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If the squirrel sees the cow then the cow needs the squirrel.
((("squirrel" "sees" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
If the cow sees the squirrel and the cow is big then the squirrel is red.
((("cow" "sees" "squirrel" "+") ("cow" "is" "big" "+")) -> ("squirrel" "is" "red" "+"))
If something sees the cow then it eats the cow.
((("something" "sees" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something is red then it eats the cow.
((("something" "is" "red" "+")) -> ("something" "eats" "cow" "+"))
If the cow sees the squirrel then the cow eats the squirrel.
((("cow" "sees" "squirrel" "+")) -> ("cow" "eats" "squirrel" "+"))
If something eats the cow then it sees the squirrel.
((("something" "eats" "cow" "+")) -> ("something" "sees" "squirrel" "+"))
The squirrel needs the cow.
True
1
proof
[(triple2)]
("squirrel" "needs" "cow" "+")
triple2
The squirrel does not need the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "needs" "cow" "-")
triple2
The squirrel eats the cow.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "eats" "cow" "+")
((triple3) -> (rule3 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "eats" "cow" "-")
((triple1) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow sees the squirrel.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "sees" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not see the squirrel.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "sees" "squirrel" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the squirrel.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5))]
("cow" "eats" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow does not eat the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5))]
("cow" "eats" "squirrel" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow is red.[(triple1)] The squirrel needs the cow.[(triple2)] The squirrel sees the cow.[(triple3)] @1: The cow eats the cow.[(((triple1) -> rule4))] The cow needs the squirrel.[(((triple3) -> rule1))] The squirrel eats the cow.[(((triple3) -> rule3))] @2: The cow sees the squirrel.[(((((triple1) -> rule4)) -> rule6))] The squirrel sees the squirrel.[(((((triple3) -> rule3)) -> rule6))] @3: The cow eats the squirrel.[(((((((triple1) -> rule4)) -> rule6)) -> rule5))]
The cow is red.
("cow" "is" "red" "+")
triple1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple3
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((triple3) -> (rule3 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3