Consider the following premises. forall x: ~S(x). u_1 <-> S(h_3). ~u_1 -> t. Can we infer ~t from them?
 From forall x: ~S(x) we can infer ~S(h_3). From u_1 <-> S(h_3), ~S(h_3) we can infer ~u_1. Finally, from ~u_1 -> t, ~u_1 we can infer t, which contradicts ~t. Therefore, the answer is no.