Complexity of two-variable logic with counting

Let C_k² denote the class of first order sentences with two variables and with additional quantifiers “there exists exactly (at most, at least) m”, for m⩽k, and let C² be the union of C_k² taken over all integers k. We prove that the problem of satisfiability of sentences of C₁² is NEXPTIME-complete. This strengthens a recent result of E. Gradel, Ph. Kolaitis and M. Vardi (1997) who proved that the satisfiability problem for the first order two-variable logic L² is NEXPTIME-complete and a very recent result by E. Gradel, M. Otto and E. Rosen (1997) who proved the decidability of C². Our result easily implies that the satisfiability problem for C² is in non-deterministic, doubly exponential time. It is interesting that C₁² is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size