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