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