Consider the following premises. ~q_24. forall z_2: U(z_2). s <-> u. s <-> q_24. Can we infer ~u from them?
 From s <-> q_24, ~q_24 we can infer ~s. Finally, from s <-> u, ~s we can infer ~u. Therefore, the answer is yes.