The bear likes the lion. The lion does not eat the squirrel. The mouse eats the lion. The squirrel is kind. If something likes the lion and the lion is not young then the lion does not like the squirrel. If the squirrel eats the bear then the bear is not green.
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If something likes the lion and the lion is not young then the lion does not like the squirrel.
((("something" "likes" "lion" "+") ("lion" "is" "young" "~")) -> ("lion" "likes" "squirrel" "-"))
If the squirrel eats the bear then the bear is not green.
((("squirrel" "eats" "bear" "+")) -> ("bear" "is" "green" "-"))
The mouse eats the lion.
True
1
proof
[(triple3)]
("mouse" "eats" "lion" "+")
triple3
The squirrel is not kind.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "kind" "-")
triple4
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
@0: The bear likes the lion.[(triple1)] The lion does not eat the squirrel.[(triple2)] The mouse eats the lion.[(triple3)] The squirrel is kind.[(triple4)]
The bear likes the lion.
("bear" "likes" "lion" "+")
triple1
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple4