Consider the following premises. ~q_9. ~p_14 or p. u -> q_9. u or ~q_9. p_14 or u. Can we infer p from them? If possible, name the inference rules being used at each step.
 From p_14 or u, ~p_14 or p we can infer u or p via resolution. From u or ~q_9 we can infer q_9 -> u via rewriting. From q_9 -> u, u -> q_9 we can infer q_9 <-> u via biconditional introduction. From q_9 <-> u, ~q_9 we can infer ~u via biconditional elimination. Finally, from u or p, ~u we can infer p via disjunctive syllogism. Therefore, the answer is yes.