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