has a model ${\ensuremath{\mathfrak{A}}}\in {{\cal K}\xspace}$. We will also say that a sentence is *${{\cal K}\xspace}$-satisfiable*.

Every ${\ensuremath{\mathrm{ESO}^2}\xspace}$-formula can be translated into a formula of a very simple shape which is ${{\cal K}\xspace}$-equivalent (see e.g. [@Scott1962] and [@GraedelO1999 page 17]). In this article ${{\cal K}\xspace}$ will always be a class of ordered $O$-structures.

\[lemma:scottnormalform\] For every ${\ensuremath{\mathrm{ESO}^2}\xspace}$-formula $\varphi = \exists \bar R\, \xi$ there is a ${{\cal K}\xspace}$-equivalent ${\ensuremath{\mathrm{ESO}^2}\xspace}$-formula $\varphi' = \exists \bar R'\, \xi'$ such that the formula $\xi'$ is of the form $$\forall x \forall y \psi(x,y) \wedge \bigwedge_i \forall x \exists y \psi_i(x, y)$$ where $\psi$ and all $\psi_i$ are quantifier-free formulas. Moreover, $\varphi'$ can be computed in polynomial time.

Note that this lemma is slightly stronger than the usual Scott normal form lemma because interpretations for some relation symbols are restricted by ${{\cal K}\xspace}$. The usual proof carries over since interpretations of symbols that occur in $\varphi$ are preserved while going from a model of $\varphi$ to a model of $\varphi'$ and vice versa.

In this work it will be convenient to use an even stronger normal form. Our plan is to rephrase the satisfiability problem for ${\ensuremath{\mathrm{ESO}^2}\xspace}$ into the satisfiability of a set of existential 