Herbrand theorem works only with clauses I read that Herbrand's theorem is valid only for a set of clauses. I already know how to convert every formula in a clause.
But, what I haven't understood is why Herbrand's theorem doesn't work with a formula that's not a clause.
Can you show me ?
 A: See: Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), page 180:

Herbrand’s Theorem: A set of clauses $S$ is unsatisfiable if and only if a finite set of ground instances of clauses of $S$ is unsatisfiable.

From this we have that: a set of clauses $S$ is unsatisfiable iff $S$ has no 
Herbrand models. 
The restriction that $S$ be a set of clauses is unavoidable, i.e. if $S$ is a set of arbitrary closed formulas, it is not possible, in general, to show that $S$ is unsatisfiable considering only to Herbrand interpretations. 
Let $S = \{ \ p(a), \ \exists x \lnot p(x) \ \}$, where the second formula is not a 
clause. 
Obviously, $S$ has a model: let $D = \{ 0, 1 \}$ and assign $0$ to $a$. Then, interpret $p$ with the function which maps $0$ to TRUE and $1$ to FALSE.
The only Herbrand interpretations for $S$ are $\emptyset$ and $\{ p(a) \}$ (there are no function symbols in $S$), but neither of these is a model for $S$.
Conclusion: $S$ does not have an Herbrand model. 
