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