The bald eagle chases the squirrel. The bald eagle chases the tiger. The bald eagle is cold. The bald eagle needs the lion. The bald eagle sees the tiger. The lion chases the bald eagle. The lion chases the tiger. The lion needs the squirrel. The lion sees the squirrel. The squirrel does not chase the lion. The squirrel sees the bald eagle. The tiger chases the lion. The tiger is big. The tiger sees the bald eagle. The tiger sees the lion. If the lion is blue then the lion does not see the bald eagle. If something chases the lion then it needs the bald eagle. If something needs the bald eagle then the bald eagle chases the lion.
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the lion is blue then the lion does not see the bald eagle.
((("lion" "is" "blue" "+")) -> ("lion" "sees" "bald eagle" "-"))
If something chases the lion then it needs the bald eagle.
((("something" "chases" "lion" "+")) -> ("something" "needs" "bald eagle" "+"))
If something needs the bald eagle then the bald eagle chases the lion.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "chases" "lion" "+"))
The tiger is big.
True
1
proof
[(triple13)]
("tiger" "is" "big" "+")
triple13
The tiger does not see the bald eagle.
False
1
inv-proof
[(triple14)]
("tiger" "sees" "bald eagle" "-")
triple14
The tiger needs the bald eagle.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "needs" "bald eagle" "+")
((triple12) -> (rule2 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The tiger does not need the bald eagle.
False
2
inv-proof
[(((triple12) -> rule2))]
("tiger" "needs" "bald eagle" "-")
((triple12) -> (rule2 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The bald eagle chases the lion.
True
3
proof
[(((((triple12) -> rule2)) -> rule3))]
("bald eagle" "chases" "lion" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle does not chase the lion.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule3))]
("bald eagle" "chases" "lion" "-")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle needs the bald eagle.
True
4
proof
[(((((((triple12) -> rule2)) -> rule3)) -> rule2))]
("bald eagle" "needs" "bald eagle" "+")
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3
The bald eagle does not need the bald eagle.
False
4
inv-proof
[(((((((triple12) -> rule2)) -> rule3)) -> rule2))]
("bald eagle" "needs" "bald eagle" "-")
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3
The lion does not need the bald eagle.
Unknown
inv-rconc
[@1: The lion needs the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "bald eagle" "-")
The squirrel needs the bald eagle.
Unknown
rconc
[@1: The squirrel needs the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "bald eagle" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
The bald eagle is not green.
Unknown
inv-random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "-")
The lion sees the bald eagle.
Unknown
random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "+")
@0: The bald eagle chases the squirrel.[(triple1)] The bald eagle chases the tiger.[(triple2)] The bald eagle is cold.[(triple3)] The bald eagle needs the lion.[(triple4)] The bald eagle sees the tiger.[(triple5)] The lion chases the bald eagle.[(triple6)] The lion chases the tiger.[(triple7)] The lion needs the squirrel.[(triple8)] The lion sees the squirrel.[(triple9)] The squirrel does not chase the lion.[(triple10)] The squirrel sees the bald eagle.[(triple11)] The tiger chases the lion.[(triple12)] The tiger is big.[(triple13)] The tiger sees the bald eagle.[(triple14)] The tiger sees the lion.[(triple15)] @1: The tiger needs the bald eagle.[(((triple12) -> rule2))] @2: The bald eagle chases the lion.[(((((triple12) -> rule2)) -> rule3))] @3: The bald eagle needs the bald eagle.[(((((((triple12) -> rule2)) -> rule3)) -> rule2))]
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
triple1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
triple2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple4
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple5
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple6
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple7
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple8
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple9
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
triple10
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
triple11
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple14
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple15
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
((triple12) -> (rule2 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3