The bald eagle needs the bear. The bear needs the lion. The cat needs the bald eagle. The lion eats the cat. If something is rough and it eats the bald eagle then it needs the bald eagle. If something chases the bear then the bear needs the bald eagle. If something chases the bear and the bear needs the lion then the bear needs the bald eagle. If something chases the bear then it needs the lion. If something needs the lion then it is red. If something eats the cat then the cat chases the bear.
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
If something is rough and it eats the bald eagle then it needs the bald eagle.
((("something" "is" "rough" "+") ("something" "eats" "bald eagle" "+")) -> ("something" "needs" "bald eagle" "+"))
If something chases the bear then the bear needs the bald eagle.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "bald eagle" "+"))
If something chases the bear and the bear needs the lion then the bear needs the bald eagle.
((("something" "chases" "bear" "+") ("bear" "needs" "lion" "+")) -> ("bear" "needs" "bald eagle" "+"))
If something chases the bear then it needs the lion.
((("something" "chases" "bear" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion then it is red.
((("something" "needs" "lion" "+")) -> ("something" "is" "red" "+"))
If something eats the cat then the cat chases the bear.
((("something" "eats" "cat" "+")) -> ("cat" "chases" "bear" "+"))
The bear needs the lion.
True
1
proof
[(triple2)]
("bear" "needs" "lion" "+")
triple2
The cat does not need the bald eagle.
False
1
inv-proof
[(triple3)]
("cat" "needs" "bald eagle" "-")
triple3
The cat chases the bear.
True
2
proof
[(((triple4) -> rule6))]
("cat" "chases" "bear" "+")
((triple4) -> (rule6 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The bear is not red.
False
2
inv-proof
[(((triple2) -> rule5))]
("bear" "is" "red" "-")
((triple2) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat needs the lion.
True
3
proof
[(((((triple4) -> rule6)) -> rule4))]
("cat" "needs" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat does not need the lion.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4))]
("cat" "needs" "lion" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is red.
True
4
proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule5))]
("cat" "is" "red" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The cat is not red.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule5))]
("cat" "is" "red" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The lion does not need the bald eagle.
Unknown
inv-rconc
[@1: The lion needs the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "bald eagle" "-")
The lion is red.
Unknown
rconc
[@2: The lion is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("lion" "is" "red" "+")
The bald eagle is not red.
Unknown
inv-rconc
[@2: The bald eagle is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("bald eagle" "is" "red" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion does not chase the bear.
Unknown
inv-random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The bald eagle needs the bear.[(triple1)] The bear needs the lion.[(triple2)] The cat needs the bald eagle.[(triple3)] The lion eats the cat.[(triple4)] @1: The bear is red.[(((triple2) -> rule5))] The cat chases the bear.[(((triple4) -> rule6))] @2: The bear needs the bald eagle.[(((((triple4) -> rule6)) -> rule2) OR ((((triple4) -> rule6) triple2) -> rule3))] The cat needs the lion.[(((((triple4) -> rule6)) -> rule4))] @3: The cat is red.[(((((((triple4) -> rule6)) -> rule4)) -> rule5))]
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
triple1
The bear needs the lion.
("bear" "needs" "lion" "+")
triple2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple3
The lion eats the cat.
("lion" "eats" "cat" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
((triple2) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
((triple4) -> (rule6 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3