Consider the following premises. q or u_2. u_2 <-> q_13. ~q_13. Can we infer q from them? If possible, name the inference rules being used at each step.
 From u_2 <-> q_13, ~q_13 we can infer ~u_2 via biconditional elimination. From q or u_2 we can infer ~u_2 -> q via rewriting. Finally, from ~u_2 -> q, ~u_2 we can infer q via modus ponens. Therefore, the answer is yes.