The bald eagle eats the lion. The bald eagle is round. The bald eagle sees the tiger. The lion is blue. The lion sees the bald eagle. The squirrel is blue. The squirrel is kind. The squirrel likes the tiger. The tiger is nice. The tiger sees the lion. If someone is kind then they see the lion.
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone is kind then they see the lion.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "lion" "+"))
The tiger sees the lion.
True
1
proof
[(triple10)]
("tiger" "sees" "lion" "+")
triple10
The tiger does not see the lion.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "lion" "-")
triple10
The squirrel sees the lion.
True
2
proof
[(((triple7) -> rule1))]
("squirrel" "sees" "lion" "+")
((triple7) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel does not see the lion.
False
2
inv-proof
[(((triple7) -> rule1))]
("squirrel" "sees" "lion" "-")
((triple7) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The bald eagle does not see the lion.
Unknown
inv-rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The bald eagle eats the lion.[(triple1)] The bald eagle is round.[(triple2)] The bald eagle sees the tiger.[(triple3)] The lion is blue.[(triple4)] The lion sees the bald eagle.[(triple5)] The squirrel is blue.[(triple6)] The squirrel is kind.[(triple7)] The squirrel likes the tiger.[(triple8)] The tiger is nice.[(triple9)] The tiger sees the lion.[(triple10)] @1: The squirrel sees the lion.[(((triple7) -> rule1))]
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
triple1
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple5
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple7) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1