Formulas with only Finite Models but Infinite Set of Ground Terms


    P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)

Is this formula satisfiable?

What are possible cardinalities for models?

What are ground terms for this formula?

Cardinality is

By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model?