The bear sees the lion. The lion is red. The rabbit needs the lion. The squirrel sees the rabbit. If someone sees the rabbit then they see the bear. If the squirrel sees the rabbit then the squirrel is rough.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the rabbit then they see the bear.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "bear" "+"))
If the squirrel sees the rabbit then the squirrel is rough.
((("squirrel" "sees" "rabbit" "+")) -> ("squirrel" "is" "rough" "+"))
The bear sees the lion.
True
1
proof
[(triple1)]
("bear" "sees" "lion" "+")
triple1
The bear does not see the lion.
False
1
inv-proof
[(triple1)]
("bear" "sees" "lion" "-")
triple1
The squirrel sees the bear.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "sees" "bear" "+")
((triple4) -> (rule1 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel does not see the bear.
False
2
inv-proof
[(((triple4) -> rule1))]
("squirrel" "sees" "bear" "-")
((triple4) -> (rule1 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "bear" "-")
The rabbit sees the bear.
Unknown
rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "bear" "+")
The lion does not need the squirrel.
Unknown
inv-random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The bear sees the lion.[(triple1)] The lion is red.[(triple2)] The rabbit needs the lion.[(triple3)] The squirrel sees the rabbit.[(triple4)] @1: The squirrel is rough.[(((triple4) -> rule2))] The squirrel sees the bear.[(((triple4) -> rule1))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple4
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple4) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple4) -> (rule1 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1