On the complexity of Maslov's class K

Maslov's class 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 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 K and a novel application of paradoxical tournament graphs.