Consider the following premises. p_14 or q_14. ~q_14. ~p_14 or p_1. ~p_1 or u. Can we infer w_2 or u from them? If possible, name the inference rules being used at each step.
 From p_14 or q_14, ~p_14 or p_1 we can infer q_14 or p_1 via resolution. From q_14 or p_1, ~q_14 we can infer p_1 via disjunctive syllogism. From p_1 we can infer p_1 or w_2 via addition. Finally, from p_1 or w_2, ~p_1 or u we can infer w_2 or u via resolution. Therefore, the answer is yes.