The dog needs the squirrel. The dog does not see the squirrel. The squirrel likes the dog. If the squirrel likes the dog and the squirrel is red then the squirrel does not need the dog.
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If the squirrel likes the dog and the squirrel is red then the squirrel does not need the dog.
((("squirrel" "likes" "dog" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "needs" "dog" "-"))
The dog does not see the squirrel.
True
1
proof
[(triple2)]
("dog" "sees" "squirrel" "-")
triple2
The dog does not need the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "needs" "squirrel" "-")
triple1
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The dog does not see the squirrel.[(triple2)] The dog needs the squirrel.[(triple1)] The squirrel likes the dog.[(triple3)]
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple2
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple3