The bald eagle eats the cow. The cow likes the bald eagle. The cow needs the bald eagle. If the cow likes the bald eagle and the cow needs the bald eagle then the cow is big. If someone needs the cow then the cow is kind. If someone is big then they need the bald eagle. If someone needs the cow then they need the bald eagle. If someone is big then they eat the cow. If someone eats the cow and the cow likes the bald eagle then they are red.
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
If the cow likes the bald eagle and the cow needs the bald eagle then the cow is big.
((("cow" "likes" "bald eagle" "+") ("cow" "needs" "bald eagle" "+")) -> ("cow" "is" "big" "+"))
If someone needs the cow then the cow is kind.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone is big then they need the bald eagle.
((("someone" "is" "big" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone needs the cow then they need the bald eagle.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone is big then they eat the cow.
((("someone" "is" "big" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the cow and the cow likes the bald eagle then they are red.
((("someone" "eats" "cow" "+") ("cow" "likes" "bald eagle" "+")) -> ("someone" "is" "red" "+"))
The bald eagle eats the cow.
True
1
proof
[(triple1)]
("bald eagle" "eats" "cow" "+")
triple1
The cow does not need the bald eagle.
False
1
inv-proof
[(triple3)]
("cow" "needs" "bald eagle" "-")
triple3
The bald eagle is red.
True
3
proof
[(((triple1 triple2) -> rule6))]
("bald eagle" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle is not red.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("bald eagle" "is" "red" "-")
((triple1 triple2) -> (rule6 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The cow eats the cow.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule5))]
("cow" "eats" "cow" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow does not eat the cow.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule5))]
("cow" "eats" "cow" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is red.
True
6
proof
[(((((((triple2 triple3) -> rule1)) -> rule5) triple2) -> rule6))]
("cow" "is" "red" "+")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is not red.
False
6
inv-proof
[(((((((triple2 triple3) -> rule1)) -> rule5) triple2) -> rule6))]
("cow" "is" "red" "-")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
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 = (rule3 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "kind" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The bald eagle is round.
Unknown
random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The bald eagle is not kind.
Unknown
inv-random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "-")
The bald eagle is nice.
Unknown
random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "+")
@0: The bald eagle eats the cow.[(triple1)] The cow likes the bald eagle.[(triple2)] The cow needs the bald eagle.[(triple3)] @1: The bald eagle is red.[(((triple1 triple2) -> rule6))] The cow is big.[(((triple2 triple3) -> rule1))] @2: The cow eats the cow.[(((((triple2 triple3) -> rule1)) -> rule5))] @3: The cow is red.[(((((((triple2 triple3) -> rule1)) -> rule5) triple2) -> rule6))]
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
triple1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple2
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple3
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple2 triple3) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3