Consider the following premises. w_1 <-> R_7(a_7). ~S_7(a_7). forall x_7: R_7(x_7) <-> S_7(x_7). Can we infer ~w_1 from them?
 From forall x_7: R_7(x_7) <-> S_7(x_7) we can infer R_7(a_7) <-> S_7(a_7). From R_7(a_7) <-> S_7(a_7), ~S_7(a_7) we can infer ~R_7(a_7). Finally, from w_1 <-> R_7(a_7), ~R_7(a_7) we can infer ~w_1. Therefore, the answer is yes.