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