 The variables formula_11 are the kind we consider for the second step, so we delete the quantifiers formula_12 and formula_13.Finally, we then replace formula_14 with a constant formula_15 (since there were no other quantifiers governing formula_14), and we replace formula_17 with a function symbol formula_18