Consider the following premises. forall z: ~P(z). forall x_12: T_3(x_12) <-> S_12(x_12). S_12(a_12) -> P(b). Can we infer T_3(a_12) from them?
 From forall x_12: T_3(x_12) <-> S_12(x_12) we can infer T_3(a_12) <-> S_12(a_12). From forall z: ~P(z) we can infer ~P(b). From S_12(a_12) -> P(b), ~P(b) we can infer ~S_12(a_12). Finally, from T_3(a_12) <-> S_12(a_12), ~S_12(a_12) we can infer ~T_3(a_12), which contradicts T_3(a_12). Therefore, the answer is no.