The bald eagle eats the cow. The cow eats the bald eagle. If someone eats the bald eagle then the bald eagle likes the cow. If someone likes the bald eagle then they need the cow. If someone is big then they need the cow. If someone likes the cow then the cow likes the bald eagle. If someone needs the cow and they do not eat the cow then the cow does not eat the bald eagle. If someone needs the cow then the cow eats the bald eagle. If someone likes the cow and they need the cow then they are cold. If someone likes the cow and they do not need the cow then they are blue.
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
If someone eats the bald eagle then the bald eagle likes the cow.
((("someone" "eats" "bald eagle" "+")) -> ("bald eagle" "likes" "cow" "+"))
If someone likes the bald eagle then they need the cow.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "needs" "cow" "+"))
If someone is big then they need the cow.
((("someone" "is" "big" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the cow then the cow likes the bald eagle.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "bald eagle" "+"))
If someone needs the cow and they do not eat the cow then the cow does not eat the bald eagle.
((("someone" "needs" "cow" "+") ("someone" "eats" "cow" "~")) -> ("cow" "eats" "bald eagle" "-"))
If someone needs the cow then the cow eats the bald eagle.
((("someone" "needs" "cow" "+")) -> ("cow" "eats" "bald eagle" "+"))
If someone likes the cow and they need the cow then they are cold.
((("someone" "likes" "cow" "+") ("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the cow and they do not need the cow then they are blue.
((("someone" "likes" "cow" "+") ("someone" "needs" "cow" "~")) -> ("someone" "is" "blue" "+"))
The cow eats the bald eagle.
True
1
proof
[(triple2)]
("cow" "eats" "bald eagle" "+")
triple2
The bald eagle does not eat the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "eats" "cow" "-")
triple1
The bald eagle likes the cow.
True
2
proof
[(((triple2) -> rule1))]
("bald eagle" "likes" "cow" "+")
((triple2) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The bald eagle does not like the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("bald eagle" "likes" "cow" "-")
((triple2) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cow likes the bald eagle.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("cow" "likes" "bald eagle" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow does not like the bald eagle.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("cow" "likes" "bald eagle" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow needs the cow.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule2))]
("cow" "needs" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The cow does not need the cow.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule2))]
("cow" "needs" "cow" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The bald eagle is not blue.
Unknown
inv-rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "blue" "-")
The bald eagle needs the cow.
Unknown
rconc
[@1: The bald eagle needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "needs" "cow" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "cold" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "blue" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
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 big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
@0: The bald eagle eats the cow.[(triple1)] The cow eats the bald eagle.[(triple2)] @1: The bald eagle likes the cow.[(((triple2) -> rule1))] @2: The cow likes the bald eagle.[(((((triple2) -> rule1)) -> rule4))] @3: The cow needs the cow.[(((((((triple2) -> rule1)) -> rule4)) -> rule2))]
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
triple1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
triple2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
((triple2) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3