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