The cow eats the squirrel. The squirrel sees the cow. If the squirrel eats the cow then the squirrel chases the cow. If someone eats the squirrel then they chase the cow. If someone sees the squirrel then the squirrel is green. If someone sees the cow then they eat the cow. If someone eats the cow and the cow sees the squirrel then the squirrel chases the cow. If someone sees the squirrel then they are young. If someone eats the squirrel and the squirrel chases the cow then the cow is nice. If someone eats the cow then they eat the squirrel.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If the squirrel eats the cow then the squirrel chases the cow.
((("squirrel" "eats" "cow" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone eats the squirrel then they chase the cow.
((("someone" "eats" "squirrel" "+")) -> ("someone" "chases" "cow" "+"))
If someone sees the squirrel then the squirrel is green.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If someone sees the cow then they eat the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the cow and the cow sees the squirrel then the squirrel chases the cow.
((("someone" "eats" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone sees the squirrel then they are young.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "young" "+"))
If someone eats the squirrel and the squirrel chases the cow then the cow is nice.
((("someone" "eats" "squirrel" "+") ("squirrel" "chases" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone eats the cow then they eat the squirrel.
((("someone" "eats" "cow" "+")) -> ("someone" "eats" "squirrel" "+"))
The cow eats the squirrel.
True
1
proof
[(triple1)]
("cow" "eats" "squirrel" "+")
triple1
The cow does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "eats" "squirrel" "-")
triple1
The squirrel eats the cow.
True
2
proof
[(((triple2) -> rule4))]
("squirrel" "eats" "cow" "+")
((triple2) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule4))]
("squirrel" "eats" "cow" "-")
((triple2) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the squirrel.
True
3
proof
[(((((triple2) -> rule4)) -> rule8))]
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel does not eat the squirrel.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule8))]
("squirrel" "eats" "squirrel" "-")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The cow is nice.
True
5
proof
[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((triple1 ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7))]
("cow" "is" "nice" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple2) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((triple1 ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The cow is not nice.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((triple1 ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7))]
("cow" "is" "nice" "-")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple2) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((triple1 ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "young" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "green" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "young" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The cow does not chase the squirrel.
Unknown
inv-random
[@0: The cow chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "squirrel" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow eats the squirrel.[(triple1)] The squirrel sees the cow.[(triple2)] @1: The cow chases the cow.[(((triple1) -> rule2))] The squirrel eats the cow.[(((triple2) -> rule4))] @2: The squirrel chases the cow.[(((((triple2) -> rule4)) -> rule1) OR ((((((triple2) -> rule4)) -> rule8)) -> rule2))] The squirrel eats the squirrel.[(((((triple2) -> rule4)) -> rule8))] @3: The cow is nice.[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((triple2) -> rule4)) -> rule1)) -> rule7) OR ((triple1 ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7) OR ((((((triple2) -> rule4)) -> rule8) ((((((triple2) -> rule4)) -> rule8)) -> rule2)) -> rule7))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple1) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((triple2) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple2) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((triple1 ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
((((((triple2) -> (rule4 % int4))) -> (rule8 % int3)) ((((((triple2) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4