Consider a clause (disjunction of literals) obtained from those of a first-order logic formula in Skolemized form
Then an atomic statement obtained from those of by replacing all variables by elements of the Herbrand universe of is called a ground atom. The set of all ground atoms that can be formed from predicate symbols from and terms from is called the Herbrand base.