Q69,paper 3,J13. If we convert

∃u ∀v ∀x ∃y (P(f(u),v, x, y) ->Q(u,v,y)) to

∀v ∀x (P(f(a),v, x, g(v,x)) ->Q(a,v,g(v,x)))

This process is known as

(A) Simplification

(B) Unification

(C) Skolemization

(D) Resolution.

Answer C.