Consider the following premises. ~P(a_12). forall x: P(x) -> T(x). P(a_12) <-> T(a_12). Can we infer ~T(a_12) from them?
 From forall x: P(x) -> T(x) we can infer P(a_12) -> T(a_12). From P(a_12) <-> T(a_12) we can infer T(a_12) -> P(a_12). From P(a_12) -> T(a_12), T(a_12) -> P(a_12) we can infer P(a_12) <-> T(a_12). Finally, from P(a_12) <-> T(a_12), ~P(a_12) we can infer ~T(a_12). Therefore, the answer is yes.