approach is used to solve the ${\ensuremath{\mathrm{ESO}^2}\xspace}$-satisfiability problem on $({\ensuremath{{S}}}_1, {\ensuremath{{S}}}_2, <_2)$-structures in Section \[section:twosuccessors\].

To decide whether an ${\ensuremath{\mathrm{ESO}^2}\xspace}$-sentence $\varphi$ has a model which is a finite $({\ensuremath{{S}}},<)$-structure, $\varphi$ is converted into a satisfiability equivalent constraint problem $C$ whose size is exponential in the size of $\varphi$ using Lemma \[lemma:formulaToConstraint\]. We show, in Lemma \[lemma:succordfinitemodel\], that if $C$ has a finite $({\ensuremath{{S}}},<)$-solution then it has a $({\ensuremath{{S}}},<)$-solution of size at most $N$ where $N$ is polynomial in the size of $C$. Hence, a non-deterministic exponential time algorithm can guess a structure of size at most $N$ and verify that it is indeed a solution of $C$. This proves Theorem \[theorem:successorandorder\]. In the automata-based approach the satisfiability of $C$ is checked by a finite state automaton, see Lemma \[lemma:succorder\].

The following notion will be useful in both approaches. Let $w$ be a word. A position $a$ of $w$ is called *$(\sigma, \tau, k)$-rich* if there are at least $k$ $\sigma$-labeled positions (strictly) before $a$ and at least $k$ $\tau$-labeled positions (strictly) after $a$. A position $a$ of $w$ is *$(\sigma, \tau, k)$-poor* if there are at most $k$ $\sigma$-labeled positions (strictly) before $a$ and at most $k$ $\tau$ labeled positions 