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