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