Consider the following premises. ~q_10 or t. ~w_1. p_1 <-> w_1. ~p_10 or p_1. p_10 or q_10. Can we infer t from them? If possible, name the inference rules being used at each step.
 From p_10 or q_10, ~p_10 or p_1 we can infer q_10 or p_1 via resolution. From q_10 or p_1, ~q_10 or t we can infer p_1 or t via resolution. From p_1 <-> w_1, ~w_1 we can infer ~p_1 via biconditional elimination. Finally, from p_1 or t, ~p_1 we can infer t via disjunctive syllogism. Therefore, the answer is yes.