Consider the following premises. w <-> s_4. s_4 -> t_2. t_2 -> ~q_12. p_1 -> w. q_12. Can we infer ~p_1 from them? If possible, name the inference rules being used at each step.
 From w <-> s_4 we can infer w -> s_4 via biconditional elimination. From t_2 -> ~q_12, q_12 we can infer ~t_2 via modus tollens. From s_4 -> t_2, ~t_2 we can infer ~s_4 via modus tollens. From p_1 -> w, w -> s_4 we can infer p_1 -> s_4 via transitivity. Finally, from p_1 -> s_4, ~s_4 we can infer ~p_1 via modus tollens. Therefore, the answer is yes.