Consider the following premises. forall z: W_3(z). forall z: S(z). u_1 -> ~W_3(g). Can we infer ~u_1 from them?
 From forall z: W_3(z), forall z: S(z) we can infer forall z: W_3(z) and S(z). From forall z: W_3(z) and S(z) we can infer forall z: W_3(z). From forall z: W_3(z) we can infer W_3(g). Finally, from u_1 -> ~W_3(g), W_3(g) we can infer ~u_1. Therefore, the answer is yes.