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