Consider the following premises. u. ~r_4. u -> q_12. r_4 or p. Can we infer p from them? If possible, name the inference rules being used at each step.
 From u -> q_12, u we can infer q_12 via modus ponens. Finally, from r_4 or p, ~r_4 we can infer p via disjunctive syllogism. Therefore, the answer is yes.