Consider the following premises. q -> r_15. p_15 or q. u_1. u_4 -> ~u_1. p_15 -> r_15. Can we infer u_4 from them? If possible, name the inference rules being used at each step.
 From p_15 -> r_15, q -> r_15, p_15 or q we can infer r_15 via disjunction elimination. Finally, from u_4 -> ~u_1, u_1 we can infer ~u_4 via modus tollens, which contradicts u_4. Therefore, the answer is no.