 The universal quantifiers can then be removed to obtain the final clause, R(x,f(x),v) ∨ ~K(x,z,g(x,z),v) in our example. The Skolemizing process may not preserve equivalence but maintains satisfiability, which is enough for clause-based automated reasoning.