The tiger is blue. The tiger is cold. The tiger is red. The tiger is rough. The tiger is young. If the tiger is not rough then the tiger is cold.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is not rough then the tiger is cold.
((("tiger" "is" "rough" "~")) -> ("tiger" "is" "cold" "+"))
The tiger is cold.
True
1
proof
[(triple2)]
("tiger" "is" "cold" "+")
triple2
The tiger is not young.
False
1
inv-proof
[(triple5)]
("tiger" "is" "young" "-")
triple5
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The tiger is blue.[(triple1)] The tiger is cold.[(triple2)] The tiger is red.[(triple3)] The tiger is rough.[(triple4)] The tiger is young.[(triple5)]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The tiger is young.
("tiger" "is" "young" "+")
triple5