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