Consider the following premises. S_9(a_9) -> q_1. q_1 -> S_9(a_9). forall x_9: R_9(x_9) <-> S_9(x_9). ~R_9(a_9). Can we infer ~q_1 from them?
 From forall x_9: R_9(x_9) <-> S_9(x_9) we can infer R_9(a_9) <-> S_9(a_9). From R_9(a_9) <-> S_9(a_9), ~R_9(a_9) we can infer ~S_9(a_9). From S_9(a_9) -> q_1, q_1 -> S_9(a_9) we can infer S_9(a_9) <-> q_1. Finally, from S_9(a_9) <-> q_1, ~S_9(a_9) we can infer ~q_1. Therefore, the answer is yes.