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