The bear eats the cat. The cat eats the bear. The cat visits the bear. If something is kind and it does not eat the bear then it does not visit the cat. If the cat does not see the bear then the bear eats the cat.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If something is kind and it does not eat the bear then it does not visit the cat.
((("something" "is" "kind" "+") ("something" "eats" "bear" "~")) -> ("something" "visits" "cat" "-"))
If the cat does not see the bear then the bear eats the cat.
((("cat" "sees" "bear" "~")) -> ("bear" "eats" "cat" "+"))
The bear eats the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "+")
triple1
The cat does not eat the bear.
False
1
inv-proof
[(triple2)]
("cat" "eats" "bear" "-")
triple2
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The bear eats the cat.[(triple1)] The cat eats the bear.[(triple2)] The cat visits the bear.[(triple3)]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The cat visits the bear.
("cat" "visits" "bear" "+")
triple3