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