Consider the following premises. ~p. t. ~t or p_1. Can we infer ~p_1 from them? If possible, name the inference rules being used at each step.
 From t we can infer t or p via addition. From t or p, ~t or p_1 we can infer p or p_1 via resolution. Finally, from p or p_1, ~p we can infer p_1 via disjunctive syllogism, which contradicts ~p_1. Therefore, the answer is no.