Consider the following premises. t_4 -> ~S_16(a_16). R_16(a_16) or q_6. q_6 -> S_16(a_16). forall x_16: R_16(x_16) <-> S_16(x_16). Can we infer ~t_4 from them?
 From forall x_16: R_16(x_16) <-> S_16(x_16) we can infer R_16(a_16) <-> S_16(a_16). From R_16(a_16) <-> S_16(a_16) we can infer R_16(a_16) -> S_16(a_16). From R_16(a_16) -> S_16(a_16), q_6 -> S_16(a_16), R_16(a_16) or q_6 we can infer S_16(a_16). Finally, from t_4 -> ~S_16(a_16), S_16(a_16) we can infer ~t_4. Therefore, the answer is yes.