Consider the following premises. forall z: P(z) <-> U_2(z). forall z: ~U_2(z). forall z: P(z) -> Q_4(z). forall z: Q_4(z) -> P(z). s -> Q_4(d_4). Can we infer s from them?
 From forall z: P(z) <-> U_2(z), forall z: ~U_2(z) we can infer forall z: ~P(z). From forall z: Q_4(z) -> P(z), forall z: P(z) -> Q_4(z) we can infer forall z: Q_4(z) <-> P(z). From forall z: Q_4(z) <-> P(z), forall z: ~P(z) we can infer forall z: ~Q_4(z). From forall z: ~Q_4(z) we can infer ~Q_4(d_4). Finally, from s -> Q_4(d_4), ~Q_4(d_4) we can infer ~s, which contradicts s. Therefore, the answer is no.