The bald eagle likes the squirrel. The cow eats the bald eagle. The squirrel is round. If someone likes the squirrel then they eat the squirrel. If someone is round then they do not like the bald eagle. If someone needs the cow and the cow is green then the cow does not eat the squirrel. If the squirrel does not like the bald eagle then the bald eagle does not need the cow. If someone needs the cow then they need the bald eagle. If the bald eagle does not need the cow then the bald eagle likes the cow.
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone likes the squirrel then they eat the squirrel.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is round then they do not like the bald eagle.
((("someone" "is" "round" "+")) -> ("someone" "likes" "bald eagle" "-"))
If someone needs the cow and the cow is green then the cow does not eat the squirrel.
((("someone" "needs" "cow" "+") ("cow" "is" "green" "+")) -> ("cow" "eats" "squirrel" "-"))
If the squirrel does not like the bald eagle then the bald eagle does not need the cow.
((("squirrel" "likes" "bald eagle" "~")) -> ("bald eagle" "needs" "cow" "-"))
If someone needs the cow then they need the bald eagle.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "bald eagle" "+"))
If the bald eagle does not need the cow then the bald eagle likes the cow.
((("bald eagle" "needs" "cow" "~")) -> ("bald eagle" "likes" "cow" "+"))
The cow eats the bald eagle.
True
1
proof
[(triple2)]
("cow" "eats" "bald eagle" "+")
triple2
The bald eagle does not like the squirrel.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "squirrel" "-")
triple1
The bald eagle eats the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int1
The squirrel likes the bald eagle.
False
2
inv-proof
[(((triple3) -> rule2))]
("squirrel" "likes" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int1
The bald eagle does not need the cow.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("bald eagle" "needs" "cow" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int1
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int2
The bald eagle needs the cow.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("bald eagle" "needs" "cow" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int1
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int2
The bald eagle likes the cow.
True
4
proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
("bald eagle" "likes" "cow" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int2
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int3
The bald eagle does not like the cow.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
("bald eagle" "likes" "cow" "-")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int2
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int3
The bald eagle does not need the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The cow needs the bald eagle.
Unknown
rconc
[@1: The cow needs the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "bald eagle" "+")
The cow does not eat the squirrel.
Unknown
inv-rconc
[@1: The cow eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
The bald eagle does not eat the cow.
Unknown
inv-random
[@0: The bald eagle eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "cow" "-")
The cow likes the squirrel.
Unknown
random
[@0: The cow likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "squirrel" "+")
@0: The bald eagle likes the squirrel.[(triple1)] The cow eats the bald eagle.[(triple2)] The squirrel is round.[(triple3)] @1: The bald eagle eats the squirrel.[(((triple1) -> rule1))] The squirrel does not like the bald eagle.[(((triple3) -> rule2))] @2: The bald eagle does not need the cow.[(((((triple3) -> rule2)) -> rule4))] @3: The bald eagle likes the cow.[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The bald eagle eats the squirrel.
("bald eagle" "eats" "squirrel" "+")
int1
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
((triple3) -> (rule2 % int1))
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int1
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int1
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
int2
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
int3