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