Conversion to Clausal Form I want to convert this formula to clausal form:
$\lnot \forall  \exists  \lnot(((, ) \land ()) \to (\exists  (,) \land ∃ ()))$
First I removed $\to$:
$\lnot \forall  \exists  \lnot(\lnot ((, ) \land ()) \land (∃ (,) \land \exists  ()))$
Then I wanted to reduce the scope of the negations:
$\lnot\forall  \exists  (((, ) \land ()) \land (∀\lnot (,) \lor \forall  \lnot ()))$
Now my problem is, how can I eliminate the negation of the Quantifier $\lnot \forall $?
Would $\exists  \exists  ((\lnot (, ) \land ()) \land (\forall (,) \lor \forall \lnot ()))$ be the right solution?
 A: As Mauro Allegranza said in his first comment, a first error is in your second formula: since $(A \to B) \equiv (\lnot A \lor B)$, your second formula should be
\begin{align}
\lnot \forall  \exists  \lnot(\lnot ((, ) \land ()) \lor (∃ (,) \land \exists  ()))
\end{align} 
Concerning your question about $\lnot \forall x$, you have to consider that $\lnot \forall x A \equiv \exists x \lnot A$. Therefore, a correct conversion of your starting formula is the following:
\begin{align}
 & \lnot \forall  \exists  \lnot(((, ) \land ()) \to (\exists  (,) \land ∃ ())) \\
\equiv \ &\lnot \forall  \exists  \lnot(\lnot ((, ) \land ()) \lor (∃ (,) \land \exists  ())) \\
\equiv \ & \lnot \forall  \exists  \lnot(\lnot (, ) \lor \lnot () \lor (∃ (,) \land \exists  ())) \\
\equiv \ & \exists  \lnot \exists  \lnot(\lnot (, ) \lor \lnot () \lor (∃ (,) \land \exists  ())) \\
\equiv \ & \exists  \forall  \, \lnot \lnot(\lnot (, ) \lor \lnot () \lor (∃ (,) \land \exists  ())) \\
\equiv \ & \exists  \forall   \,(\lnot (, ) \lor \lnot () \lor (\exists  (,) \land \exists  ())) \\
\equiv \ & \exists  \forall   \,(\lnot (, ) \lor \lnot () \lor (\exists  (,) \land \exists w (w))) \\
\end{align}
Pay attention: according to Wikipedia's definition, the last formula is not a clausal form yet because of the existential quantifier in $\exists  (,) \land \exists w (w)$. To eliminate them (and the initial $\exists x$), you have to skolemize them. 
After skolemization, you have to (drop all universal quantifiers and)
distribute $\lor$'s inwards over $\land$'s, i.e. repeatedly replace $A \lor ( B \land C )$ with $(A \lor B) \land (A \lor C)$.
