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