Consider the following premises. q_12 <-> u. Q(h) <-> q_12. forall y: ~Q(y). Can we infer ~u or p from them?
 From forall y: ~Q(y) we can infer ~Q(h). From Q(h) <-> q_12, ~Q(h) we can infer ~q_12. From q_12 <-> u, ~q_12 we can infer ~u. Finally, from ~u we can infer ~u or p. Therefore, the answer is yes.