$({\ensuremath{{S}}}, <)$-solution then it has such a solution of size polynomial in $|C|$.

Assume that $C {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}(C_\exists, C_\forall)$ is a constraint problem over a signature $T \cup \{{\ensuremath{{S}}}, <\}$. Let $\Sigma {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}\Sigma_T$ and $\Gamma {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}\Gamma_T$. Let $k {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}3 |\Gamma|$.

We show that if $C$ has a finite $({\ensuremath{{S}}},<)$-solution ${\ensuremath{\mathfrak{A}}}$ with at least $N$ elements then it also has a $({\ensuremath{{S}}},<)$-solution ${\ensuremath{\mathfrak{B}}}$ with $|{\ensuremath{\mathfrak{B}}}| < N$. The number $N$ is polynomial in $|C|$ and will be specified later.

For each element $a$ of ${\ensuremath{\mathfrak{A}}}$ denote by $W(a)$ a set containing witnesses for $a$ for each existential constraint. An element $b \in W(a)$ is a *local witness* if ${\ensuremath{{S}}}(a,b)$, $a=b$, or ${\ensuremath{{S}}}(b,a)$. Otherwise it is a *non-local witness*.

We first construct, from ${\ensuremath{\mathfrak{A}}}$, a solution ${\ensuremath{\mathfrak{A}}}'$ of $C$ whose domain and unary types coincide with the domain and unary types of ${\ensuremath{\mathfrak{A}}}$ but whose set of non-local witnesses is small. Afterwards we argue that a smaller solution ${\ensuremath{\mathfrak{B}}}$ can be obtained from ${\ensuremath{\mathfrak{A}}}'$ by removing some elements.

Towards constructing ${\ensuremath{\mathfrak{A}}}'$ let $Z_1$ be the set that contains, for every $\sigma \in \Sigma$, the first $k+1$ $\sigma$-positions and the last $k+1$ $\sigma$-positions of ${\ensuremath{\mathfrak{A}}}$ (if 