The cat needs the lion. The cat needs the mouse. The lion is green. The lion is round. The lion likes the cat. The mouse is green. The mouse needs the cat. If someone eats the lion and the lion eats the cat then the lion is round. If the cat is round then the cat likes the lion.
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If someone eats the lion and the lion eats the cat then the lion is round.
((("someone" "eats" "lion" "+") ("lion" "eats" "cat" "+")) -> ("lion" "is" "round" "+"))
If the cat is round then the cat likes the lion.
((("cat" "is" "round" "+")) -> ("cat" "likes" "lion" "+"))
The mouse needs the cat.
True
1
proof
[(triple7)]
("mouse" "needs" "cat" "+")
triple7
The lion is not green.
False
1
inv-proof
[(triple3)]
("lion" "is" "green" "-")
triple3
The cat does not like the lion.
Unknown
inv-rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cat needs the lion.[(triple1)] The cat needs the mouse.[(triple2)] The lion is green.[(triple3)] The lion is round.[(triple4)] The lion likes the cat.[(triple5)] The mouse is green.[(triple6)] The mouse needs the cat.[(triple7)]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion likes the cat.
("lion" "likes" "cat" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple7