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