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