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