\Gamma_O$, $\gamma \in \Gamma_{T}$ and $\tau \in \Sigma_{T}$. Similarly universal constraints are written as tuples $(\sigma, d, \gamma, \tau)$ where $\sigma, \tau \in \Sigma_{T}$, $\gamma \in \Gamma_{T}$ and $d \in \Gamma_O$.

Warm-Up: One Linear Order and One Successor {#section:warm-up}
===========================================

Before proving the main results we study the complexity of the ${\ensuremath{\mathrm{ESO}^2}\xspace}$-satisfiability problem on ordered $({\ensuremath{{S}}},<)$-structures. Decidability has been established in [@GradelR99]. Combining Lemma 2.4 in [@GradelR99] and a construction from [@EiterGG00 Corollary 9.2] yields at best a non-deterministic double-exponential upper bound. In this section we obtain an optimal non-deterministic exponential upper bound.

\[theorem:successorandorder\] ${\ensuremath{\mathrm{ESO}^2}\xspace}$-satisfiability on finite ordered $({\ensuremath{{S}}},<)$-structures is [[$\mbox{\sc NExpTime}$]{}]{}-complete.

This result should be compared with the known results that deciding on ordered $({\ensuremath{{S}}},<)$-structure and deciding ${\ensuremath{\mathrm{ESO}^2}\xspace}$ on ordered $<$-structures are ${{\ensuremath{\mbox{\sc NExpTime}}\xspace}}$-complete .

We present two different approaches for proving Theorem \[theorem:successorandorder\]; a small model property based approach and an automata-based approach. Only the former approach leads to a non-deterministic exponential time algorithm. Later both approaches will be generalized in different directions to obtain decidability for larger fragments. The small model approach, combined with a technique from [@SchwentickZ10; @SchwentickZ12], is used to obtain a decision algorithm for ${\ensuremath{\mathrm{ESO}^2}\xspace}$ on $({\ensuremath{{S}}}_1, <_1, <_2)$-structures in Section \[section:twoorders\]. The automata-based 