Consider the following premises. forall x_11: R_11(x_11) <-> S_11(x_11). ~S_11(a_1). p. Can we infer p and ~R_11(a_1) from them?
 From forall x_11: R_11(x_11) <-> S_11(x_11) we can infer R_11(a_1) <-> S_11(a_1). From R_11(a_1) <-> S_11(a_1), ~S_11(a_1) we can infer ~R_11(a_1). Finally, from p, ~R_11(a_1) we can infer p and ~R_11(a_1). Therefore, the answer is yes.