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