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