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