Complexity of two-variable logic with counting

Let C-k(2) denote the class of first order sentences with two variables and with additional quantifiers ''there exists exactly (at most, at least) m'', for m less than or equal to k, and let C-2 be the union of C-k(2) taken over all integers k. We prove that the problem of satisfiability of sentences of C-1(2) is NEXPTIME-complete. This strengthens a recent result off. Gradel, Ph. Kolaitis and M. Vardi [4] who proved that the satisfiability problem for the first order two-variable logic L-2 is NEXPTIME-complete and a very recent result by E. Gradel M. Otto and E. Rosen [5] who proved the decidability of C-2. Our result easily implies that the satisfiability problem for C-2 is in nondeterministic, doubly exponential time. It is interesting that C-1(2) is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size.