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