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