given an if formula formula_23, we first define its skolemization relativized to a finite set formula_159 of variables. for every existential quantifier formula_1 occurring in formula_23, let formula_162 be a new function symbol (a "skolem function"). we write formula_163 for the formula which is obtained substituting, in formula_23, all free occurrences of the variable formula_5 with the term formula_166. the skolemization of formula_23 relative to formula_168, formula_169, is defined by the following inductive clauses: