Consider the following premises. p_13 <-> t_4. u_2 -> t_4. ~p_13. s <-> p_1. p_1 -> u_2. Can we infer ~s from them? If possible, name the inference rules being used at each step.
 From p_13 <-> t_4, ~p_13 we can infer ~t_4 via biconditional elimination. From u_2 -> t_4, ~t_4 we can infer ~u_2 via modus tollens. From p_1 -> u_2, ~u_2 we can infer ~p_1 via modus tollens. Finally, from s <-> p_1, ~p_1 we can infer ~s via biconditional elimination. Therefore, the answer is yes.