The lion chases the tiger. The tiger chases the lion. The tiger is blue. If someone needs the tiger then they are not red.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If someone needs the tiger then they are not red.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "red" "-"))
The tiger chases the lion.
True
1
proof
[(triple2)]
("tiger" "chases" "lion" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple3)]
("tiger" "is" "blue" "-")
triple3
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The lion chases the tiger.[(triple1)] The tiger chases the lion.[(triple2)] The tiger is blue.[(triple3)]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3