The bald eagle is green. The cow eats the lion. The lion likes the squirrel. The squirrel sees the cow. If someone likes the bald eagle then the bald eagle likes the cow. If someone likes the cow then the cow does not eat the bald eagle. If someone eats the bald eagle then they see the squirrel. If the squirrel likes the lion then the squirrel does not see the lion. If someone sees the cow then they eat the bald eagle. If someone sees the bald eagle then the bald eagle is kind. If someone sees the cow and they see the squirrel then the cow does not see the squirrel. If someone is green and they eat the lion then the lion does not like the cow.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone likes the bald eagle then the bald eagle likes the cow.
((("someone" "likes" "bald eagle" "+")) -> ("bald eagle" "likes" "cow" "+"))
If someone likes the cow then the cow does not eat the bald eagle.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "bald eagle" "-"))
If someone eats the bald eagle then they see the squirrel.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "sees" "squirrel" "+"))
If the squirrel likes the lion then the squirrel does not see the lion.
((("squirrel" "likes" "lion" "+")) -> ("squirrel" "sees" "lion" "-"))
If someone sees the cow then they eat the bald eagle.
((("someone" "sees" "cow" "+")) -> ("someone" "eats" "bald eagle" "+"))
If someone sees the bald eagle then the bald eagle is kind.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "+"))
If someone sees the cow and they see the squirrel then the cow does not see the squirrel.
((("someone" "sees" "cow" "+") ("someone" "sees" "squirrel" "+")) -> ("cow" "sees" "squirrel" "-"))
If someone is green and they eat the lion then the lion does not like the cow.
((("someone" "is" "green" "+") ("someone" "eats" "lion" "+")) -> ("lion" "likes" "cow" "-"))
The lion likes the squirrel.
True
1
proof
[(triple3)]
("lion" "likes" "squirrel" "+")
triple3
The cow does not eat the lion.
False
1
inv-proof
[(triple2)]
("cow" "eats" "lion" "-")
triple2
The squirrel eats the bald eagle.
True
2
proof
[(((triple4) -> rule5))]
("squirrel" "eats" "bald eagle" "+")
((triple4) -> (rule5 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel does not eat the bald eagle.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "eats" "bald eagle" "-")
((triple4) -> (rule5 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel sees the squirrel.
True
3
proof
[(((((triple4) -> rule5)) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int2
The cow does not see the squirrel.
True
5
proof
[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
("cow" "sees" "squirrel" "-")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int3
The cow sees the squirrel.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
("cow" "sees" "squirrel" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int3
The lion does not eat the bald eagle.
Unknown
inv-rconc
[@1: The lion eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "bald eagle" "-")
The bald eagle is kind.
Unknown
rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "kind" "+")
The bald eagle does not see the squirrel.
Unknown
inv-rconc
[@2: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("bald eagle" "sees" "squirrel" "-")
The cow eats the bald eagle.
Unknown
rconc
[@1: The cow eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "bald eagle" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The bald eagle sees the lion.
Unknown
random
[@0: The bald eagle sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "lion" "+")
@0: The bald eagle is green.[(triple1)] The cow eats the lion.[(triple2)] The lion likes the squirrel.[(triple3)] The squirrel sees the cow.[(triple4)] @1: The squirrel eats the bald eagle.[(((triple4) -> rule5))] @2: The squirrel sees the squirrel.[(((((triple4) -> rule5)) -> rule3))] @3: The cow does not see the squirrel.[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The cow eats the lion.
("cow" "eats" "lion" "+")
triple2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple3
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple4
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
((triple4) -> (rule5 % int1))
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int2
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
int3