The bear eats the squirrel. The bear eats the tiger. The cat is not kind. The cat visits the tiger. The squirrel is green. The tiger chases the squirrel. The tiger visits the cat. If the tiger eats the bear and the bear is not kind then the bear is not green.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the tiger eats the bear and the bear is not kind then the bear is not green.
((("tiger" "eats" "bear" "+") ("bear" "is" "kind" "~")) -> ("bear" "is" "green" "-"))
The bear eats the squirrel.
True
1
proof
[(triple1)]
("bear" "eats" "squirrel" "+")
triple1
The cat does not visit the tiger.
False
1
inv-proof
[(triple4)]
("cat" "visits" "tiger" "-")
triple4
The squirrel does not chase the bear.
Unknown
inv-random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "-")
The cat visits the bear.
Unknown
random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "+")
@0: The bear eats the squirrel.[(triple1)] The bear eats the tiger.[(triple2)] The cat is not kind.[(triple3)] The cat visits the tiger.[(triple4)] The squirrel is green.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger visits the cat.[(triple7)]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The cat is not kind.
("cat" "is" "kind" "-")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple7