I guess I can't really edit this comment anymore, but it looks like I was wrong. That example is actually a perfectly valid clause, since it's equivalent to "fo

I guess I can't really edit this comment anymore, but it looks like I was wrong. That example is actually a perfectly valid clause, since it's equivalent to "forall x. ~(x = Santa Claus)". The only reason no model satisfies this clause is because we conventionally require equality to be reflexive, but for an arbitrary predicate the empty model would be a perfectly good model in the Herbrand universe.