The bear is nice. The bear sees the lion. The lion is cold. The lion is nice. The lion needs the bear. The lion sees the bear. The squirrel is blue. The squirrel is nice. The squirrel sees the lion. The squirrel visits the lion. If something is blue then it sees the squirrel.
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is blue then it sees the squirrel.
((("something" "is" "blue" "+")) -> ("something" "sees" "squirrel" "+"))
The lion needs the bear.
True
1
proof
[(triple5)]
("lion" "needs" "bear" "+")
triple5
The squirrel is not blue.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "blue" "-")
triple7
The squirrel sees the squirrel.
True
2
proof
[(((triple7) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple7) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((triple7) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
Unknown
inv-rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The bear is nice.[(triple1)] The bear sees the lion.[(triple2)] The lion is cold.[(triple3)] The lion is nice.[(triple4)] The lion needs the bear.[(triple5)] The lion sees the bear.[(triple6)] The squirrel is blue.[(triple7)] The squirrel is nice.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel visits the lion.[(triple10)] @1: The squirrel sees the squirrel.[(((triple7) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion needs the bear.
("lion" "needs" "bear" "+")
triple5
The lion sees the bear.
("lion" "sees" "bear" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1