$|\varphi|$.

Let $\varphi$ be an ${\ensuremath{\mathrm{ESO}^2}\xspace}$-sentence. Without loss of generality we can assume, by Lemma \[lemma:scottnormalform\], that $\varphi = \exists \bar R \, \xi$ where $\xi$ is of the form $\forall x \forall y \psi(x,y) \wedge \bigwedge_i \forall x \exists y \psi_i(x,y)$ with quantifier-free $\psi$ and $\psi_i$. Let $T$ be the signature of the ${\ensuremath{\mathrm{FO}^2}\xspace}$-formula $\xi$. Further let $\Sigma$ and $\Gamma$ be the sets of unary and binary $T$-types.

A ${{\cal K}\xspace}$-satisfiability equivalent constraint problem for $\varphi$ is now constructed by translating $\forall x \forall y \psi(x,y)$ and $\forall x \exists y \psi_i(x,y)$ into universal and existential constraints, respectively.

Observe that, for a quantifier-free formula in disjunctive normal form $\bigvee_i \psi_i$, an equivalent quantifier-free formula in disjunctive normal form can be constructed, where (1) each disjunct is of the form $\sigma(x) \wedge \tau(y) \wedge \gamma(x,y)$ where $\sigma$ and $\tau$ are unary types and $\gamma$ is a conjunction of binary literals that use variables $x$ and $y$, and (2) for all unary types $\sigma$ and $\tau$ there is such a disjunct.

Thus the first conjunct of $\xi$ is equivalent to a formula $$\chi = \forall x \forall y \bigvee_{\sigma, \tau \in \Sigma} \Big(\sigma(x) \wedge \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)\Big)$$ The formula $\chi$ 