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