Consider the following premises. ~w_1. ~w_3 or w. q. w_3 or w_1. Can we infer w and q from them? If possible, name the inference rules being used at each step.
 From w_3 or w_1, ~w_3 or w we can infer w_1 or w via resolution. From w_1 or w, ~w_1 we can infer w via disjunctive syllogism. Finally, from w, q we can infer w and q via conjunction. Therefore, the answer is yes.