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