Consider the following premises. u <-> t_4. w_1 -> t_4. w_1 or ~t. Can we infer ~(t -> u) from them?
 From w_1 or ~t we can infer t -> w_1. From u <-> t_4 we can infer t_4 -> u. From t -> w_1, w_1 -> t_4 we can infer t -> t_4. Finally, from t -> t_4, t_4 -> u we can infer t -> u, which contradicts ~(t -> u). Therefore, the answer is no.