Let us say I have a function-free first order logic language. And I can ground it on a domain $\Delta$ of size $n$. Grounding here means that $\forall x \Phi(x)$ translates to $\land_{a\in \Delta}\Phi(a)$. Similarly, grounding $\exists x \Phi(x)$ translates to $\lor_{a\in \Delta}\Phi(a)$. Now, can I someohow use gaifman locality theorem to ground any FOL formula to a DNF of size polynomial in $n$. My intuition emerges from one formulation of the theorem which says that every fol sentence can be written as $\exists^{*} \forall x$ -local sentence.
http://www.kurims.kyoto-u.ac.jp/EMIS/journals/DMTCS/pdfpapers/dm030303.pdf