Consider the following premises. t_4 -> P(d). forall x: T_2(x) <-> P(x). ~T_2(d). Can we infer t_4 from them?
 From forall x: T_2(x) <-> P(x) we can infer T_2(d) <-> P(d). From T_2(d) <-> P(d), ~T_2(d) we can infer ~P(d). Finally, from t_4 -> P(d), ~P(d) we can infer ~t_4, which contradicts t_4. Therefore, the answer is no.