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