Consider the following premises. p_1 -> s. ~R(c). forall x_12: R(x_12) <-> S_12(x_12). s -> S_12(c). Can we infer ~p_1 from them? If possible, name the inference rules being used at each step.
 From forall x_12: R(x_12) <-> S_12(x_12) we can infer R(c) <-> S_12(c) via universal instantiation. From R(c) <-> S_12(c), ~R(c) we can infer ~S_12(c) via biconditional elimination. From p_1 -> s, s -> S_12(c) we can infer p_1 -> S_12(c) via transitivity. Finally, from p_1 -> S_12(c), ~S_12(c) we can infer ~p_1 via modus tollens. Therefore, the answer is yes.