Consider the following premises. s_2. p_8 <-> t. u_4 -> p_8. t -> ~s_2. Can we infer u_4 from them? If possible, name the inference rules being used at each step.
 From t -> ~s_2, s_2 we can infer ~t via modus tollens. From p_8 <-> t, ~t we can infer ~p_8 via biconditional elimination. Finally, from u_4 -> p_8, ~p_8 we can infer ~u_4 via modus tollens, which contradicts u_4. Therefore, the answer is no.