The dog sees the squirrel. The mouse is red. The mouse sees the dog. The mouse visits the dog. The rabbit sees the squirrel. The rabbit visits the dog. The rabbit visits the squirrel. The squirrel is red. The squirrel needs the dog. The squirrel visits the dog. If someone needs the dog then they visit the mouse. If someone visits the rabbit then the rabbit visits the dog. If someone visits the squirrel and the squirrel is blue then they see the mouse.
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone needs the dog then they visit the mouse.
((("someone" "needs" "dog" "+")) -> ("someone" "visits" "mouse" "+"))
If someone visits the rabbit then the rabbit visits the dog.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If someone visits the squirrel and the squirrel is blue then they see the mouse.
((("someone" "visits" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("someone" "sees" "mouse" "+"))
The squirrel visits the dog.
True
1
proof
[(triple10)]
("squirrel" "visits" "dog" "+")
triple10
The rabbit does not visit the dog.
False
1
inv-proof
[(triple6)]
("rabbit" "visits" "dog" "-")
triple6
The squirrel visits the mouse.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel does not visit the mouse.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "visits" "mouse" "-")
((triple9) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The dog visits the mouse.
Unknown
rconc
[@1: The dog visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "mouse" "+")
The dog does not need the rabbit.
Unknown
inv-random
[@0: The dog needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "rabbit" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
@0: The dog sees the squirrel.[(triple1)] The mouse is red.[(triple2)] The mouse sees the dog.[(triple3)] The mouse visits the dog.[(triple4)] The rabbit sees the squirrel.[(triple5)] The rabbit visits the dog.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel is red.[(triple8)] The squirrel needs the dog.[(triple9)] The squirrel visits the dog.[(triple10)] @1: The squirrel visits the mouse.[(((triple9) -> rule1))]
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple5
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple9
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple10
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1