The bald eagle likes the cat. The cat likes the tiger. The tiger is rough. If someone likes the bald eagle and the bald eagle is rough then the bald eagle likes the cat. If someone likes the tiger then the tiger eats the bald eagle. If the tiger likes the bald eagle then the tiger eats the bald eagle. If someone sees the tiger and the tiger eats the bald eagle then the tiger eats the cat. If someone eats the bald eagle then they see the tiger. If someone is rough then they see the cat. If someone eats the bald eagle and they do not eat the tiger then the tiger likes the cat. If the bald eagle eats the cat and the bald eagle does not eat the tiger then the bald eagle sees the tiger.
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone likes the bald eagle and the bald eagle is rough then the bald eagle likes the cat.
((("someone" "likes" "bald eagle" "+") ("bald eagle" "is" "rough" "+")) -> ("bald eagle" "likes" "cat" "+"))
If someone likes the tiger then the tiger eats the bald eagle.
((("someone" "likes" "tiger" "+")) -> ("tiger" "eats" "bald eagle" "+"))
If the tiger likes the bald eagle then the tiger eats the bald eagle.
((("tiger" "likes" "bald eagle" "+")) -> ("tiger" "eats" "bald eagle" "+"))
If someone sees the tiger and the tiger eats the bald eagle then the tiger eats the cat.
((("someone" "sees" "tiger" "+") ("tiger" "eats" "bald eagle" "+")) -> ("tiger" "eats" "cat" "+"))
If someone eats the bald eagle then they see the tiger.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is rough then they see the cat.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "+"))
If someone eats the bald eagle and they do not eat the tiger then the tiger likes the cat.
((("someone" "eats" "bald eagle" "+") ("someone" "eats" "tiger" "~")) -> ("tiger" "likes" "cat" "+"))
If the bald eagle eats the cat and the bald eagle does not eat the tiger then the bald eagle sees the tiger.
((("bald eagle" "eats" "cat" "+") ("bald eagle" "eats" "tiger" "~")) -> ("bald eagle" "sees" "tiger" "+"))
The bald eagle likes the cat.
True
1
proof
[(triple1)]
("bald eagle" "likes" "cat" "+")
triple1
The bald eagle does not like the cat.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "cat" "-")
triple1
The tiger sees the cat.
True
2
proof
[(((triple3) -> rule6))]
("tiger" "sees" "cat" "+")
((triple3) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger does not eat the bald eagle.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "eats" "bald eagle" "-")
((triple2) -> (rule2 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("tiger" "sees" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("tiger" "sees" "tiger" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int2
The tiger eats the cat.
True
6
proof
[(((((((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule4))]
("tiger" "eats" "cat" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int3
The tiger does not eat the cat.
False
6
inv-proof
[(((((((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule4))]
("tiger" "eats" "cat" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int3
The tiger does not like the cat.
Unknown
inv-rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "likes" "cat" "-")
The bald eagle sees the tiger.
Unknown
rconc
[@1: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "sees" "tiger" "+")
The bald eagle does not see the cat.
Unknown
inv-rconc
[@1: The bald eagle sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "sees" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The bald eagle does not eat the cat.
Unknown
inv-random
[@0: The bald eagle eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "cat" "-")
The tiger sees the bald eagle.
Unknown
random
[@0: The tiger sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bald eagle" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle likes the cat.[(triple1)] The cat likes the tiger.[(triple2)] The tiger is rough.[(triple3)] @1: The tiger eats the bald eagle.[(((triple2) -> rule2))] The tiger sees the cat.[(((triple3) -> rule6))] @2: The tiger sees the tiger.[(((((triple2) -> rule2)) -> rule5))] @3: The tiger eats the cat.[(((((((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule4))]
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((triple3) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int3