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