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