Solution (source code)

= Solution

Suppose such a <first-order theory> $S$ existed. Add two new constants $c,d$ and consider
$$
T=S\cup\{\neg E(c,d)\}\cup
\{\theta_n(c),\theta_n(d):n\ge1\},
$$
where $\theta_n$ is the finite lower-bound <logical formula> from (iii).

Every finite <subset> of $T$ has a <first-order model>. Choose a <first-order structure> with exactly two equivalence classes: one countably infinite, and one finite of size at least the largest bound appearing in that <subset>. Interpret $c$ in the infinite class and $d$ in the finite class. The <first-order structure> satisfies all of $S$, by its assumed characterization, and meets the finite demands on both named classes.

<Compactness theorem> in the language with the two new constants gives a <first-order model> of all of $T$. Its classes of $c$ and $d$ are distinct and both infinite. Its reduct still satisfies $S$, which is impossible if $S$ characterizes exactly one infinite class. Hence
$$
\boxed{\text{Exactly one infinite equivalence class is not first-order axiomatizable}.}
$$
The finite approximations work because any finite list of <lower bounds> permits the second class to remain finite; the entire list prevents that escape.