The rabbit sees the squirrel. The squirrel sees the rabbit. If someone sees the rabbit and the rabbit sees the squirrel then the rabbit visits the squirrel. If the rabbit sees the squirrel and the squirrel chases the rabbit then the squirrel sees the rabbit. If someone sees the rabbit then the rabbit visits the squirrel.
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the rabbit and the rabbit sees the squirrel then the rabbit visits the squirrel.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "squirrel" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If the rabbit sees the squirrel and the squirrel chases the rabbit then the squirrel sees the rabbit.
((("rabbit" "sees" "squirrel" "+") ("squirrel" "chases" "rabbit" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone sees the rabbit then the rabbit visits the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
The rabbit sees the squirrel.
True
1
proof
[(triple1)]
("rabbit" "sees" "squirrel" "+")
triple1
The rabbit does not see the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "sees" "squirrel" "-")
triple1
The rabbit visits the squirrel.
True
2
proof
[(((triple2) -> rule3) OR ((triple2 triple1) -> rule1))]
("rabbit" "visits" "squirrel" "+")
((triple2) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
((triple2 triple1) -> (rule1 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2 triple1) -> rule1))]
("rabbit" "visits" "squirrel" "-")
((triple2) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
((triple2 triple1) -> (rule1 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The rabbit sees the squirrel.[(triple1)] The squirrel sees the rabbit.[(triple2)] @1: The rabbit visits the squirrel.[(((triple2) -> rule3) OR ((triple2 triple1) -> rule1))]
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple2) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
((triple2 triple1) -> (rule1 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1