Consider the following premises. t or s. s -> q_2. q_2 <-> p. w. ~t or p. Can we infer q_2 and w from them? If possible, name the inference rules being used at each step.
 From q_2 <-> p we can infer p -> q_2 via biconditional elimination. From t or s, ~t or p we can infer s or p via resolution. From s -> q_2, p -> q_2, s or p we can infer q_2 via disjunction elimination. Finally, from q_2, w we can infer q_2 and w via conjunction. Therefore, the answer is yes.