Consider the following premises. ~t or r_4. w -> p_4. p_4 <-> r_4. t or w. Can we infer p_4 from them? If possible, name the inference rules being used at each step.
 From t or w, ~t or r_4 we can infer w or r_4 via resolution. From p_4 <-> r_4 we can infer r_4 -> p_4 via biconditional elimination. Finally, from w -> p_4, r_4 -> p_4, w or r_4 we can infer p_4 via disjunction elimination. Therefore, the answer is yes.