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