Consider the following premises. forall x_12: R(x_12) or S_12(x_12). s -> ~S_12(c_2). ~R(c_2). Can we infer ~s from them?
 From forall x_12: R(x_12) or S_12(x_12) we can infer R(c_2) or S_12(c_2). From R(c_2) or S_12(c_2), ~R(c_2) we can infer S_12(c_2). Finally, from s -> ~S_12(c_2), S_12(c_2) we can infer ~s. Therefore, the answer is yes.