The lion needs the rabbit. The mouse needs the lion. The rabbit sees the lion. The squirrel needs the lion. If something sees the squirrel and it eats the rabbit then the squirrel is cold. If the squirrel eats the lion and the lion is not cold then the squirrel sees the lion.
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If something sees the squirrel and it eats the rabbit then the squirrel is cold.
((("something" "sees" "squirrel" "+") ("something" "eats" "rabbit" "+")) -> ("squirrel" "is" "cold" "+"))
If the squirrel eats the lion and the lion is not cold then the squirrel sees the lion.
((("squirrel" "eats" "lion" "+") ("lion" "is" "cold" "~")) -> ("squirrel" "sees" "lion" "+"))
The lion needs the rabbit.
True
1
proof
[(triple1)]
("lion" "needs" "rabbit" "+")
triple1
The lion does not need the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "needs" "rabbit" "-")
triple1
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "lion" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
@0: The lion needs the rabbit.[(triple1)] The mouse needs the lion.[(triple2)] The rabbit sees the lion.[(triple3)] The squirrel needs the lion.[(triple4)]
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple4