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