The lion chases the tiger. The tiger needs the lion. If the tiger eats the lion and the lion does not eat the tiger then the tiger does not need the lion. If the tiger eats the lion and the tiger is blue then the tiger is not big. If the lion eats the tiger and the tiger needs the lion then the lion is red.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If the tiger eats the lion and the lion does not eat the tiger then the tiger does not need the lion.
((("tiger" "eats" "lion" "+") ("lion" "eats" "tiger" "~")) -> ("tiger" "needs" "lion" "-"))
If the tiger eats the lion and the tiger is blue then the tiger is not big.
((("tiger" "eats" "lion" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "is" "big" "-"))
If the lion eats the tiger and the tiger needs the lion then the lion is red.
((("lion" "eats" "tiger" "+") ("tiger" "needs" "lion" "+")) -> ("lion" "is" "red" "+"))
The lion chases the tiger.
True
1
proof
[(triple1)]
("lion" "chases" "tiger" "+")
triple1
The tiger does not need the lion.
False
1
inv-proof
[(triple2)]
("tiger" "needs" "lion" "-")
triple2
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "red" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The lion chases the tiger.[(triple1)] The tiger needs the lion.[(triple2)]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple2