The rabbit sees the squirrel. The squirrel is blue. The squirrel is nice. The squirrel is red. The squirrel likes the rabbit. The squirrel sees the rabbit. The squirrel visits the rabbit. If someone visits the rabbit and they are kind then they visit the squirrel. If someone sees the rabbit then they see the squirrel. If the rabbit sees the squirrel then the squirrel likes the rabbit. If someone visits the squirrel and they are blue then the squirrel likes the rabbit. If the rabbit is big and the rabbit visits the squirrel then the rabbit likes the squirrel. If someone sees the squirrel and the squirrel visits the rabbit then they are red.
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone visits the rabbit and they are kind then they visit the squirrel.
((("someone" "visits" "rabbit" "+") ("someone" "is" "kind" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone sees the rabbit then they see the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "squirrel" "+"))
If the rabbit sees the squirrel then the squirrel likes the rabbit.
((("rabbit" "sees" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone visits the squirrel and they are blue then the squirrel likes the rabbit.
((("someone" "visits" "squirrel" "+") ("someone" "is" "blue" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If the rabbit is big and the rabbit visits the squirrel then the rabbit likes the squirrel.
((("rabbit" "is" "big" "+") ("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If someone sees the squirrel and the squirrel visits the rabbit then they are red.
((("someone" "sees" "squirrel" "+") ("squirrel" "visits" "rabbit" "+")) -> ("someone" "is" "red" "+"))
The squirrel is blue.
True
1
proof
[(triple2)]
("squirrel" "is" "blue" "+")
triple2
The rabbit does not see the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "sees" "squirrel" "-")
triple1
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The rabbit sees the squirrel.[(triple1)] The squirrel is blue.[(triple2)] The squirrel is nice.[(triple3)] The squirrel is red.[(triple4 OR ((((triple6) -> rule2) triple7) -> rule6))] The squirrel likes the rabbit.[(triple5 OR ((triple1) -> rule3))] The squirrel sees the rabbit.[(triple6)] The squirrel visits the rabbit.[(triple7)] @1: The rabbit is red.[(((triple1 triple7) -> rule6))] The squirrel sees the squirrel.[(((triple6) -> rule2))]
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
((((triple6) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple5
((triple1) -> (rule3 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple6
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1 triple7) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1