The cat likes the squirrel. The lion visits the squirrel. The squirrel visits the cat. The tiger visits the squirrel. If the tiger likes the cat and the cat needs the squirrel then the cat is round.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the tiger likes the cat and the cat needs the squirrel then the cat is round.
((("tiger" "likes" "cat" "+") ("cat" "needs" "squirrel" "+")) -> ("cat" "is" "round" "+"))
The cat likes the squirrel.
True
1
proof
[(triple1)]
("cat" "likes" "squirrel" "+")
triple1
The squirrel does not visit the cat.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "cat" "-")
triple3
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "round" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat likes the squirrel.[(triple1)] The lion visits the squirrel.[(triple2)] The squirrel visits the cat.[(triple3)] The tiger visits the squirrel.[(triple4)]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple4