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