Solution (source code)

= Solution

Use the axioms for a strict <dense linear order without endpoints>:
$$
\forall x\,\neg(x<x),\qquad
\forall x\forall y\forall z\,((x<y\wedge y<z)\to x<z),
$$
$$
\forall x\forall y\,(x<y\vee x=y\vee y<x),\qquad
\forall x\forall y\,(x<y\to\exists z(x<z\wedge z<y)),
$$
$$
\forall x\exists y\,(y<x),\qquad\forall x\exists y\,(x<y).
$$
The first three give strict linear order; the next gives density; the final two exclude endpoints. Domains are nonempty under the adopted first-order semantics, and these axioms force them to be infinite.