Consider the following premises. p_6 -> r_6. q_6 -> r_6. ~q. q <-> p. p_6 or q_6. Can we infer ~r_6 from them? If possible, name the inference rules being used at each step.
 From q <-> p, ~q we can infer ~p via biconditional elimination. Finally, from p_6 -> r_6, q_6 -> r_6, p_6 or q_6 we can infer r_6 via disjunction elimination, which contradicts ~r_6. Therefore, the answer is no.