Consider the following premises. p_16 or w. ~w or p. t_2. ~r_4. ~p_16 or r_4. Can we infer p from them? If possible, name the inference rules being used at each step.
 From p_16 or w, ~p_16 or r_4 we can infer w or r_4 via resolution. From w or r_4, ~w or p we can infer r_4 or p via resolution. Finally, from r_4 or p, ~r_4 we can infer p via disjunctive syllogism. Therefore, the answer is yes.