Consider the following premises. s <-> Q(a_20). forall z: U(z) -> Q(z). s -> u_2. u_2 -> U(a_20). Can we infer ~(U(a_20) <-> Q(a_20)) from them?
 From forall z: U(z) -> Q(z) we can infer U(a_20) -> Q(a_20). From s -> u_2, u_2 -> U(a_20) we can infer s -> U(a_20). From s <-> Q(a_20) we can infer Q(a_20) -> s. From Q(a_20) -> s, s -> U(a_20) we can infer Q(a_20) -> U(a_20). Finally, from U(a_20) -> Q(a_20), Q(a_20) -> U(a_20) we can infer U(a_20) <-> Q(a_20), which contradicts ~(U(a_20) <-> Q(a_20)). Therefore, the answer is no.