Skolem Constants and Functions Can Handle "exists"
Existentially quantified variables are handled by a technique called
skolemization, which replaces the variable with a new constant.
For example, the formula
∃ y ∀ x .
loves(x, y)
would be encoded as a formula such as loves(X, sk1), where
sk1 is a new constant that stands for the object that is
asserted to exist.
