Consider the following premises. u_1 -> w. q_7 or w_3. u_1 or ~q_7. w_3 -> w. Can we infer w from them? If possible, name the inference rules being used at each step.
 From u_1 or ~q_7 we can infer q_7 -> u_1 via rewriting. From q_7 -> u_1, u_1 -> w we can infer q_7 -> w via transitivity. Finally, from q_7 -> w, w_3 -> w, q_7 or w_3 we can infer w via disjunction elimination. Therefore, the answer is yes.