The question is actually summarised in the title. I have a FOL language with a fixed number of variables, with only relational symbols, containing a set of $n$ constants $\Delta$. The domain of interpretations is also $\Delta$, the logic is described as Herbrand Logic in this paper.,
Given an FOL sentence in this language, what is the computational complexity (w.r.t $n$) of finding a model which is true on $n$ domain elements, assuming all the other things fixed.