The bear is big. The lion is cold. The mouse does not visit the lion. If someone visits the mouse then the mouse does not need the bear.
The bear is big.
("bear" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
If someone visits the mouse then the mouse does not need the bear.
((("someone" "visits" "mouse" "+")) -> ("mouse" "needs" "bear" "-"))
The mouse does not visit the lion.
True
1
proof
[(triple3)]
("mouse" "visits" "lion" "-")
triple3
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear does not eat the mouse.
Unknown
inv-random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
@0: The bear is big.[(triple1)] The lion is cold.[(triple2)] The mouse does not visit the lion.[(triple3)]
The bear is big.
("bear" "is" "big" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple3