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