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