The bald eagle visits the cat. The bear eats the bald eagle. The cat needs the bald eagle. The tiger visits the bear. If something eats the bear then the bear needs the cat. If the bear eats the bald eagle and the bald eagle visits the tiger then the bear is kind. If something needs the bald eagle then the bald eagle visits the tiger. All kind things are nice. If something eats the cat and the cat eats the bald eagle then the cat needs the tiger. If something needs the cat then it eats the bear.
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something eats the bear then the bear needs the cat.
((("something" "eats" "bear" "+")) -> ("bear" "needs" "cat" "+"))
If the bear eats the bald eagle and the bald eagle visits the tiger then the bear is kind.
((("bear" "eats" "bald eagle" "+") ("bald eagle" "visits" "tiger" "+")) -> ("bear" "is" "kind" "+"))
If something needs the bald eagle then the bald eagle visits the tiger.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "visits" "tiger" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something eats the cat and the cat eats the bald eagle then the cat needs the tiger.
((("something" "eats" "cat" "+") ("cat" "eats" "bald eagle" "+")) -> ("cat" "needs" "tiger" "+"))
If something needs the cat then it eats the bear.
((("something" "needs" "cat" "+")) -> ("something" "eats" "bear" "+"))
The bald eagle visits the cat.
True
1
proof
[(triple1)]
("bald eagle" "visits" "cat" "+")
triple1
The bald eagle does not visit the cat.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "cat" "-")
triple1
The bald eagle visits the tiger.
True
2
proof
[(((triple3) -> rule3))]
("bald eagle" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bald eagle does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("bald eagle" "visits" "tiger" "-")
((triple3) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bear is kind.
True
4
proof
[(((triple2 ((triple3) -> rule3)) -> rule2))]
("bear" "is" "kind" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bear is not kind.
False
4
inv-proof
[(((triple2 ((triple3) -> rule3)) -> rule2))]
("bear" "is" "kind" "-")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bear is nice.
True
5
proof
[(((((triple2 ((triple3) -> rule3)) -> rule2)) -> rule4))]
("bear" "is" "nice" "+")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3
The bear is not nice.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule3)) -> rule2)) -> rule4))]
("bear" "is" "nice" "-")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3
The bald eagle does not eat the bear.
Unknown
inv-rconc
[@1: The bald eagle eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "eats" "bear" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "nice" "+")
The bald eagle is not nice.
Unknown
inv-rconc
[@1: The bald eagle is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "nice" "-")
The bear eats the bear.
Unknown
rconc
[@2: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("bear" "eats" "bear" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat eats the bald eagle.
Unknown
random
[@0: The cat eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bald eagle" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The tiger eats the cat.
Unknown
random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "+")
@0: The bald eagle visits the cat.[(triple1)] The bear eats the bald eagle.[(triple2)] The cat needs the bald eagle.[(triple3)] The tiger visits the bear.[(triple4)] @1: The bald eagle visits the tiger.[(((triple3) -> rule3))] @2: The bear is kind.[(((triple2 ((triple3) -> rule3)) -> rule2))] @3: The bear is nice.[(((((triple2 ((triple3) -> rule3)) -> rule2)) -> rule4))]
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple1
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
triple2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple3
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple4
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3