Consider the following premises. forall x_13: T_1(x_13) <-> S_13(x_13). q_1. ~S_13(a_13). Can we infer T_1(a_13) from them?
 From forall x_13: T_1(x_13) <-> S_13(x_13) we can infer T_1(a_13) <-> S_13(a_13). Finally, from T_1(a_13) <-> S_13(a_13), ~S_13(a_13) we can infer ~T_1(a_13), which contradicts T_1(a_13). Therefore, the answer is no.