The lion needs the rabbit. The lion sees the rabbit. The rabbit sees the lion. If the rabbit chases the lion and the lion is kind then the rabbit is nice. If someone needs the lion then the lion is kind.
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the rabbit chases the lion and the lion is kind then the rabbit is nice.
((("rabbit" "chases" "lion" "+") ("lion" "is" "kind" "+")) -> ("rabbit" "is" "nice" "+"))
If someone needs the lion then the lion is kind.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "kind" "+"))
The lion needs the rabbit.
True
1
proof
[(triple1)]
("lion" "needs" "rabbit" "+")
triple1
The rabbit does not see the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "lion" "-")
triple3
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "kind" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The lion needs the rabbit.[(triple1)] The lion sees the rabbit.[(triple2)] The rabbit sees the lion.[(triple3)]
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3