The bear sees the lion. The lion does not chase the bear. The squirrel sees the bear. If the bear does not eat the squirrel then the squirrel sees the lion. If the lion does not chase the bear then the lion is young. If someone sees the bear then the bear eats the lion.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion does not chase the bear.
("lion" "chases" "bear" "-")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If the bear does not eat the squirrel then the squirrel sees the lion.
((("bear" "eats" "squirrel" "~")) -> ("squirrel" "sees" "lion" "+"))
If the lion does not chase the bear then the lion is young.
((("lion" "chases" "bear" "~")) -> ("lion" "is" "young" "+"))
If someone sees the bear then the bear eats the lion.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "lion" "+"))
The lion does not chase the bear.
True
1
proof
[(triple2)]
("lion" "chases" "bear" "-")
triple2
The bear does not see the lion.
False
1
inv-proof
[(triple1)]
("bear" "sees" "lion" "-")
triple1
The bear eats the lion.
True
2
proof
[(((triple3) -> rule3))]
("bear" "eats" "lion" "+")
((triple3) -> (rule3 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "is" "young" "-")
((triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The bear sees the lion.[(triple1)] The lion does not chase the bear.[(triple2)] The squirrel sees the bear.[(triple3)] @1: The bear eats the lion.[(((triple3) -> rule3))] The lion is young.[(((triple2) -> rule2))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion does not chase the bear.
("lion" "chases" "bear" "-")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The bear eats the lion.
("bear" "eats" "lion" "+")
((triple3) -> (rule3 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1