The bald eagle sees the tiger. The bear sees the tiger. The lion sees the bald eagle. The tiger visits the bald eagle. If the tiger likes the lion then the tiger is kind. If something sees the bald eagle then the bald eagle visits the tiger. If something is young then it likes the bear. If something visits the lion then the lion is young. If something visits the bald eagle then it likes the bear. If something sees the bald eagle then it visits the tiger. If something likes the tiger and the tiger is round then it visits the tiger. If something likes the bear then the bear visits the bald eagle.
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
If the tiger likes the lion then the tiger is kind.
((("tiger" "likes" "lion" "+")) -> ("tiger" "is" "kind" "+"))
If something sees the bald eagle then the bald eagle visits the tiger.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "visits" "tiger" "+"))
If something is young then it likes the bear.
((("something" "is" "young" "+")) -> ("something" "likes" "bear" "+"))
If something visits the lion then the lion is young.
((("something" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
If something visits the bald eagle then it likes the bear.
((("something" "visits" "bald eagle" "+")) -> ("something" "likes" "bear" "+"))
If something sees the bald eagle then it visits the tiger.
((("something" "sees" "bald eagle" "+")) -> ("something" "visits" "tiger" "+"))
If something likes the tiger and the tiger is round then it visits the tiger.
((("something" "likes" "tiger" "+") ("tiger" "is" "round" "+")) -> ("something" "visits" "tiger" "+"))
If something likes the bear then the bear visits the bald eagle.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "bald eagle" "+"))
The tiger visits the bald eagle.
True
1
proof
[(triple4)]
("tiger" "visits" "bald eagle" "+")
triple4
The lion does not see the bald eagle.
False
1
inv-proof
[(triple3)]
("lion" "sees" "bald eagle" "-")
triple3
The tiger likes the bear.
True
2
proof
[(((triple4) -> rule5))]
("tiger" "likes" "bear" "+")
((triple4) -> (rule5 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bald eagle does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("bald eagle" "visits" "tiger" "-")
((triple3) -> (rule2 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bear visits the bald eagle.
True
3
proof
[(((((triple4) -> rule5)) -> rule8))]
("bear" "visits" "bald eagle" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear does not visit the bald eagle.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule8))]
("bear" "visits" "bald eagle" "-")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear likes the bear.
True
4
proof
[(((((((triple4) -> rule5)) -> rule8)) -> rule5))]
("bear" "likes" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The bear does not like the bear.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule8)) -> rule5))]
("bear" "likes" "bear" "-")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The lion does not like the bear.
Unknown
inv-rconc
[@2: The lion likes the bear.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("lion" "likes" "bear" "-")
The bear visits the tiger.
Unknown
rconc
[@1: The bear visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "tiger" "+")
The bald eagle does not like the bear.
Unknown
inv-rconc
[@1: The bald eagle likes the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "likes" "bear" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The lion visits the bald eagle.
Unknown
random
[@0: The lion visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bald eagle" "+")
@0: The bald eagle sees the tiger.[(triple1)] The bear sees the tiger.[(triple2)] The lion sees the bald eagle.[(triple3)] The tiger visits the bald eagle.[(triple4)] @1: The bald eagle visits the tiger.[(((triple3) -> rule2))] The lion visits the tiger.[(((triple3) -> rule6))] The tiger likes the bear.[(((triple4) -> rule5))] @2: The bear visits the bald eagle.[(((((triple4) -> rule5)) -> rule8))] @3: The bear likes the bear.[(((((((triple4) -> rule5)) -> rule8)) -> rule5))]
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
triple4
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
((triple3) -> (rule2 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple3) -> (rule6 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple4) -> (rule5 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3