Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as Emil Jeřábek suggested) by some very old works by Behmann and Loewenheim.
Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book).