Consider the following premises. r -> p_2. p or t_2. p_2 or ~t_2. ~p or r. Can we infer ~p_2 from them? If possible, name the inference rules being used at each step.
 From p or t_2, ~p or r we can infer t_2 or r via resolution. From p_2 or ~t_2 we can infer t_2 -> p_2 via rewriting. Finally, from t_2 -> p_2, r -> p_2, t_2 or r we can infer p_2 via disjunction elimination, which contradicts ~p_2. Therefore, the answer is no.