The cat visits the squirrel. The mouse sees the cat. The rabbit visits the squirrel. The squirrel needs the rabbit. If the squirrel is kind then the squirrel sees the mouse.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If the squirrel is kind then the squirrel sees the mouse.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "sees" "mouse" "+"))
The squirrel needs the rabbit.
True
1
proof
[(triple4)]
("squirrel" "needs" "rabbit" "+")
triple4
The mouse does not see the cat.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "cat" "-")
triple2
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The cat visits the squirrel.[(triple1)] The mouse sees the cat.[(triple2)] The rabbit visits the squirrel.[(triple3)] The squirrel needs the rabbit.[(triple4)]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple4