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