On the complexity of Maslov's class $\overline{\text{K}}$

Maslov's class $\overline{\text{K}}$ is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that $\overline{\text{K}}$ has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to $\overline{\text{K}}$ and a novel application of paradoxical tournament graphs.
Comment: This is an extended version of the LICS'24 paper