Consider the following premises. ~q_22. w <-> s_2. u_4 <-> q_22. s_2 -> u_4. Can we infer ~w or q from them? If possible, name the inference rules being used at each step.
 From u_4 <-> q_22, ~q_22 we can infer ~u_4 via biconditional elimination. From s_2 -> u_4, ~u_4 we can infer ~s_2 via modus tollens. From w <-> s_2, ~s_2 we can infer ~w via biconditional elimination. Finally, from ~w we can infer ~w or q via addition. Therefore, the answer is yes.