Consider the following premises. t_3. p or ~t. t. Can we infer ~p from them? If possible, name the inference rules being used at each step.
 From p or ~t we can infer t -> p via rewriting. Finally, from t -> p, t we can infer p via modus ponens, which contradicts ~p. Therefore, the answer is no.