Consider the following premises. w or ~r. q_4 or r. w <-> q_4. Can we infer w 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 w <-> q_4 we can infer q_4 -> w via biconditional elimination. Finally, from q_4 -> w, r -> w, q_4 or r we can infer w via disjunction elimination. Therefore, the answer is yes.