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