The bear sees the lion. The lion eats the squirrel. The squirrel sees the bear. If something eats the squirrel then the squirrel sees the lion. If something is nice and it sees the lion then it sees the bear. If something eats the lion then it is big. If something is nice then it sees the squirrel. If the lion eats the bear and the lion sees the bear then the bear visits the lion. If something eats the lion then the lion is big.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something eats the squirrel then the squirrel sees the lion.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If something is nice and it sees the lion then it sees the bear.
((("something" "is" "nice" "+") ("something" "sees" "lion" "+")) -> ("something" "sees" "bear" "+"))
If something eats the lion then it is big.
((("something" "eats" "lion" "+")) -> ("something" "is" "big" "+"))
If something is nice then it sees the squirrel.
((("something" "is" "nice" "+")) -> ("something" "sees" "squirrel" "+"))
If the lion eats the bear and the lion sees the bear then the bear visits the lion.
((("lion" "eats" "bear" "+") ("lion" "sees" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If something eats the lion then the lion is big.
((("something" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
The squirrel sees the bear.
True
1
proof
[(triple3)]
("squirrel" "sees" "bear" "+")
triple3
The lion does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "eats" "squirrel" "-")
triple2
The squirrel sees the lion.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "sees" "lion" "+")
((triple2) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel does not see the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "sees" "lion" "-")
((triple2) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion does not see the squirrel.
Unknown
inv-rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "squirrel" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "big" "+")
The bear does not eat the squirrel.
Unknown
inv-random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
@0: The bear sees the lion.[(triple1)] The lion eats the squirrel.[(triple2)] The squirrel sees the bear.[(triple3)] @1: The squirrel sees the lion.[(((triple2) -> rule1))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple2) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1