The cat likes the tiger. The tiger sees the cat. If something eats the tiger then it is not red. If something is cold then it does not see the tiger.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something eats the tiger then it is not red.
((("something" "eats" "tiger" "+")) -> ("something" "is" "red" "-"))
If something is cold then it does not see the tiger.
((("something" "is" "cold" "+")) -> ("something" "sees" "tiger" "-"))
The cat likes the tiger.
True
1
proof
[(triple1)]
("cat" "likes" "tiger" "+")
triple1
The tiger does not see the cat.
False
1
inv-proof
[(triple2)]
("tiger" "sees" "cat" "-")
triple2
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat likes the tiger.[(triple1)] The tiger sees the cat.[(triple2)]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple2