The bear sees the squirrel. The cat eats the lion. The lion sees the cat. The squirrel is round. If someone eats the cat then the cat is not nice.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone eats the cat then the cat is not nice.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "nice" "-"))
The lion sees the cat.
True
1
proof
[(triple3)]
("lion" "sees" "cat" "+")
triple3
The squirrel is not round.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "round" "-")
triple4
The lion does not eat the cat.
Unknown
inv-random
[@0: The lion eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The bear sees the squirrel.[(triple1)] The cat eats the lion.[(triple2)] The lion sees the cat.[(triple3)] The squirrel is round.[(triple4)]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The lion sees the cat.
("lion" "sees" "cat" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
triple4