Consider the following premises. S_12(a_1) <-> R_1(a_1). forall x_12: R_1(x_12) -> S_12(x_12). Can we infer ~(S_12(a_1) -> R_1(a_1)) from them?
That contradicts the premises. Therefore the answer is no.