The lion is round. The mouse does not need the lion. If someone chases the lion and they do not chase the mouse then the mouse is red. If someone needs the mouse then they visit the lion. If the lion is not young then the lion needs the mouse.
The lion is round.
("lion" "is" "round" "+")
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
If someone chases the lion and they do not chase the mouse then the mouse is red.
((("someone" "chases" "lion" "+") ("someone" "chases" "mouse" "~")) -> ("mouse" "is" "red" "+"))
If someone needs the mouse then they visit the lion.
((("someone" "needs" "mouse" "+")) -> ("someone" "visits" "lion" "+"))
If the lion is not young then the lion needs the mouse.
((("lion" "is" "young" "~")) -> ("lion" "needs" "mouse" "+"))
The mouse does not need the lion.
True
1
proof
[(triple2)]
("mouse" "needs" "lion" "-")
triple2
The mouse needs the lion.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "lion" "+")
triple2
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "red" "-")
The mouse chases the lion.
Unknown
random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "+")
@0: The lion is round.[(triple1)] The mouse does not need the lion.[(triple2)]
The lion is round.
("lion" "is" "round" "+")
triple1
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
triple2