Solution (source code)

= Solution

Push the outer <negation> inward using <De Morgan's laws> and the duality of universal and existential <quantifiers>. Negating the outer universal <quantifier> first gives an existential $x$. Negating its conjunction produces either $\forall y\,\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a <negation normal form> is
$$
\boxed{\exists x\left(
(\forall y\,\neg P(x,y))\lor
\exists z\left(\neg Q(z)\land
\left(\neg P(x,z)\lor\forall t\,\neg P(z,t)\right)\right)
\right).}
$$
All <negations> now apply directly to <atomic formulas>. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.