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