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