The bear sees the mouse. The cat likes the squirrel. The mouse visits the squirrel. The squirrel sees the cat. If someone visits the squirrel then they see the mouse. If someone is green and they see the mouse then they see the bear.
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone visits the squirrel then they see the mouse.
((("someone" "visits" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is green and they see the mouse then they see the bear.
((("someone" "is" "green" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "sees" "bear" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple3)]
("mouse" "visits" "squirrel" "+")
triple3
The mouse does not visit the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "squirrel" "-")
triple3
The cat does not see the mouse.
Unknown
inv-rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "mouse" "-")
The cat visits the mouse.
Unknown
random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "+")
@0: The bear sees the mouse.[(triple1)] The cat likes the squirrel.[(triple2)] The mouse visits the squirrel.[(triple3)] The squirrel sees the cat.[(triple4)] @1: The mouse sees the mouse.[(((triple3) -> rule1))]
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1