Consider the following premises. w_4 -> ~q_3. q -> r_15. w -> r_15. w or q. q_3. Can we infer r_15 and ~w_4 from them? If possible, name the inference rules being used at each step.
 From w -> r_15, q -> r_15, w or q we can infer r_15 via disjunction elimination. From w_4 -> ~q_3, q_3 we can infer ~w_4 via modus tollens. Finally, from r_15, ~w_4 we can infer r_15 and ~w_4 via conjunction. Therefore, the answer is yes.