The cat likes the rabbit. The lion is big. The lion likes the squirrel. The lion needs the cat. The rabbit needs the cat. The squirrel likes the rabbit. The squirrel needs the cat. If the lion needs the cat and the lion needs the rabbit then the cat sees the rabbit.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If the lion needs the cat and the lion needs the rabbit then the cat sees the rabbit.
((("lion" "needs" "cat" "+") ("lion" "needs" "rabbit" "+")) -> ("cat" "sees" "rabbit" "+"))
The lion likes the squirrel.
True
1
proof
[(triple3)]
("lion" "likes" "squirrel" "+")
triple3
The lion does not need the cat.
False
1
inv-proof
[(triple4)]
("lion" "needs" "cat" "-")
triple4
The cat does not see the rabbit.
Unknown
inv-rconc
[@1: The cat sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "rabbit" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat likes the rabbit.[(triple1)] The lion is big.[(triple2)] The lion likes the squirrel.[(triple3)] The lion needs the cat.[(triple4)] The rabbit needs the cat.[(triple5)] The squirrel likes the rabbit.[(triple6)] The squirrel needs the cat.[(triple7)]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple3
The lion needs the cat.
("lion" "needs" "cat" "+")
triple4
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple5
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple6
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple7