On satisfiability for 2-variable FOL being NEXPTIME-complete

Question

Let $\mathbf{FO^2}$ be the fragment of first-order logic consisting of sentences with at most two variables and no function symbols. It is well known that satisfiability for $\mathbf{FO}^2$ is decidable (see [1], for instance). Furthermore, in that same paper, it is argued that $\mathbf{FO^2}$ satisfiability is $\mathbf{NEXPTIME}$-complete, and that this result follows from these two lemmas:

1. Satisfiability for $\mathbf{FO^2}$ is in $\mathbf{NTIME}(2^{O(n)})$.
2. Satisfiability for $\mathbf{FO^2}$ has a lower complexity bound of the form $\mathbf{NTIME}(2^{cn/\log{n}})$ for some positive constant $c$.

I don't have a lot of background in complexity theory, so this has left me with two questions:

1. Is it easy to see that these two lemmas imply $\mathbf{NEXPTIME}$-completeness?
2. Is this result not contradictory? By definition, $\mathbf{NEXPTIME} = \bigcup_{k \in \mathbb{N}}\mathbf{NTIME}(2^{n^k})$, and by the non-deterministic time hierarchy theorem we have for any $i, j \in \mathbb{N}$ that $\mathbf{NTIME}(2^{n^i}) \subsetneq \mathbf{NTIME}(2^{n^j})$ if $i < j$. So I'm wondering how a problem complete for the class can lie at the "lowest rung" of the ladder - is this because Karp-reductions can blow-up the size of an input polynomially?

---

REFERENCES

[1] On the Decision Problem for Two-Variable First-Order Logic - Grädel, Kolaitis and Vardi