Consider the following premises. ~u or u_4. u and w_4. Can we infer q_3 or u_4 from them? If possible, name the inference rules being used at each step.
 From u and w_4 we can infer u via simplification. From u we can infer u or q_3 via addition. Finally, from u or q_3, ~u or u_4 we can infer q_3 or u_4 via resolution. Therefore, the answer is yes.