The bald eagle chases the cow. The cow chases the squirrel. The cow eats the squirrel. The lion chases the cow. The lion eats the squirrel. The squirrel eats the bald eagle. The squirrel is cold. If something chases the squirrel then it eats the lion. If something chases the squirrel and the squirrel sees the cow then the squirrel is rough. If something eats the bald eagle then it sees the squirrel. If something chases the cow then it chases the bald eagle. If something eats the bald eagle then the bald eagle eats the lion. If the cow is cold and the cow eats the lion then the lion eats the squirrel. If something sees the cow then it eats the cow. If something sees the lion then the lion eats the bald eagle. If something sees the squirrel then it sees the lion.
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If something chases the squirrel then it eats the lion.
((("something" "chases" "squirrel" "+")) -> ("something" "eats" "lion" "+"))
If something chases the squirrel and the squirrel sees the cow then the squirrel is rough.
((("something" "chases" "squirrel" "+") ("squirrel" "sees" "cow" "+")) -> ("squirrel" "is" "rough" "+"))
If something eats the bald eagle then it sees the squirrel.
((("something" "eats" "bald eagle" "+")) -> ("something" "sees" "squirrel" "+"))
If something chases the cow then it chases the bald eagle.
((("something" "chases" "cow" "+")) -> ("something" "chases" "bald eagle" "+"))
If something eats the bald eagle then the bald eagle eats the lion.
((("something" "eats" "bald eagle" "+")) -> ("bald eagle" "eats" "lion" "+"))
If the cow is cold and the cow eats the lion then the lion eats the squirrel.
((("cow" "is" "cold" "+") ("cow" "eats" "lion" "+")) -> ("lion" "eats" "squirrel" "+"))
If something sees the cow then it eats the cow.
((("something" "sees" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something sees the lion then the lion eats the bald eagle.
((("something" "sees" "lion" "+")) -> ("lion" "eats" "bald eagle" "+"))
If something sees the squirrel then it sees the lion.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "lion" "+"))
The cow chases the squirrel.
True
1
proof
[(triple2)]
("cow" "chases" "squirrel" "+")
triple2
The bald eagle does not chase the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "cow" "-")
triple1
The squirrel sees the squirrel.
True
2
proof
[(((triple6) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The bald eagle does not chase the bald eagle.
False
2
inv-proof
[(((triple1) -> rule4))]
("bald eagle" "chases" "bald eagle" "-")
((triple1) -> (rule4 % int1))
The bald eagle chases the bald eagle.
("bald eagle" "chases" "bald eagle" "+")
int1
The squirrel sees the lion.
True
3
proof
[(((((triple6) -> rule3)) -> rule9))]
("squirrel" "sees" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel does not see the lion.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule9))]
("squirrel" "sees" "lion" "-")
((((triple6) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The lion eats the bald eagle.
True
4
proof
[(((((((triple6) -> rule3)) -> rule9)) -> rule8))]
("lion" "eats" "bald eagle" "+")
((((((triple6) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The lion does not eat the bald eagle.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule9)) -> rule8))]
("lion" "eats" "bald eagle" "-")
((((((triple6) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The lion sees the squirrel.
True
5
proof
[(((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3))]
("lion" "sees" "squirrel" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The lion does not see the squirrel.
False
5
inv-proof
[(((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3))]
("lion" "sees" "squirrel" "-")
((((((((triple6) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The lion sees the lion.
True
6
proof
[(((((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3)) -> rule9))]
("lion" "sees" "lion" "+")
((((((((((triple6) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5
The lion does not see the lion.
False
6
inv-proof
[(((((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3)) -> rule9))]
("lion" "sees" "lion" "-")
((((((((((triple6) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "-")
The squirrel eats the lion.
Unknown
rconc
[@1: The squirrel eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "lion" "+")
The cow does not see the squirrel.
Unknown
inv-rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "squirrel" "-")
The squirrel chases the bald eagle.
Unknown
rconc
[@1: The squirrel chases the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "bald eagle" "+")
The bald eagle does not see the lion.
Unknown
inv-rconc
[@2: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("bald eagle" "sees" "lion" "-")
The cow chases the bald eagle.
Unknown
rconc
[@1: The cow chases the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "bald eagle" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The bald eagle is rough.
Unknown
random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The squirrel chases the cow.
Unknown
random
[@0: The squirrel chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cow" "+")
The bald eagle is not young.
Unknown
inv-random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "-")
The bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
@0: The bald eagle chases the cow.[(triple1)] The cow chases the squirrel.[(triple2)] The cow eats the squirrel.[(triple3)] The lion chases the cow.[(triple4)] The lion eats the squirrel.[(triple5)] The squirrel eats the bald eagle.[(triple6)] The squirrel is cold.[(triple7)] @1: The bald eagle chases the bald eagle.[(((triple1) -> rule4))] The bald eagle eats the lion.[(((triple6) -> rule5) OR ((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule5))] The cow eats the lion.[(((triple2) -> rule1))] The lion chases the bald eagle.[(((triple4) -> rule4))] The squirrel sees the squirrel.[(((triple6) -> rule3))] @2: The squirrel sees the lion.[(((((triple6) -> rule3)) -> rule9))] @3: The lion eats the bald eagle.[(((((((triple6) -> rule3)) -> rule9)) -> rule8))] @4: The lion sees the squirrel.[(((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3))] @5: The lion sees the lion.[(((((((((((triple6) -> rule3)) -> rule9)) -> rule8)) -> rule3)) -> rule9))]
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
triple1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The bald eagle chases the bald eagle.
("bald eagle" "chases" "bald eagle" "+")
((triple1) -> (rule4 % int1))
The bald eagle chases the bald eagle.
("bald eagle" "chases" "bald eagle" "+")
int1
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
((triple6) -> (rule5 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
((((((((triple6) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The cow eats the lion.
("cow" "eats" "lion" "+")
((triple2) -> (rule1 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
((triple4) -> (rule4 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
((((((triple6) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((((((triple6) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5