Consider the following premises. U(g) -> u. forall z: W_3(z) or U(z). W_3(g) -> u. Can we infer ~u from them?
 From forall z: W_3(z) or U(z) we can infer W_3(g) or U(g). Finally, from W_3(g) -> u, U(g) -> u, W_3(g) or U(g) we can infer u, which contradicts ~u. Therefore, the answer is no.