How do I reason with Skolem functions? Given the first-order sentence.
$\forall x \forall y : (Overlap(x,y) \iff  (\exists z Part(z,x) \land Part(z,y)))~~~~~~~~~~~~~~~~$  (1)
Here is an outline (partial) proof that $Overlap$ is symmetric:
Proof 1
\begin{align}
& \text{1}~~\forall x \forall y : (Overlap(x,y) \iff  (\exists z Part(z,x) \land Part(z,y))) & \tag{Axiom}\\
&  \text{2}~~~~~~~Overlap(a,b) \tag{Assume} \\
&  \text{3}~~~~~~~\exists z (Part(z,a) \land Part(z,b)) \tag{1,2}\\
&  \text{4}~~~~~~~\exists z (Part(z,b) \land Part(z,a)) \tag{3}\\
&  \text{5}~~~~~~~Overlap(b,a)  \tag{1,2,4}\\
&  \text{6}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{$\forall$-Intro 2-5} \\
\end{align}
Note in line 4 the same existential $z$ is used.
Now I wish write the  axiom (1) in an equisatisfiable form that can be proved using equational logic and term rewriting. This usually requires Skolemization.  Sentence (1) can be Skolemized as follows:
$\forall x \forall y : (Overlap(x,y) \iff   (Part(Sk(x,y),x) \land Part(Sk(x,y),y))~~~~~~~~~~~$ (2)
Now I try to prove symmetry using (2) with a similar approach as in Proof 1:
Proof Attempt 2
\begin{align}
& \text{1}~~\forall x \forall y : (Overlap(x,y) \iff   (Part(Sk(x,y),x) \land Part(Sk(x,y),y))& \tag{Axiom}\\
&  \text{2}~~~~~~~~Overlap(a,b) \tag{Assume} \\
&  \text{3}~~~~~~~~Part(Sk(a,b),a) \land Part(Sk(a,b),b)  \tag{1,2}\\
&  \text{4}~~~~~~~~Part(Sk(a,b),b) \land Part(Sk(a,b),a)  \tag{3}\\
&  \text{5}~~~~~~~~Overlap(b,a)\tag{XX}\\
&  \text{6}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{XX} \\
\end{align}
I am stuck at lines 4-5 in Proof Attempt 2.By following the approach of Proof 1 there is an issue with the order of arguments to Skolem functions.
 A: This is a sketch of the main idea. The axiom is the same if the  universal quantifiers are interchanged.
Skolemization of this gives
$$\exists Sk \forall y \forall x \; Overlap(x, y) \Leftrightarrow Part(Sk(y, x), x) \land Part(Sk(y, x), y) \tag{a}\label{eqa}$$
which is equivalent to
$$\exists Sk \forall x \forall y \; Overlap(y, x) \Leftrightarrow Part(Sk(x, y), y) \land Part(Sk(x, y), x) \tag{b}\label{eqb}$$
by changing the names of the variables.
We can also show similarly from the Axiom that
$$\exists S \forall x \forall y \; Overlap(x, y) \Leftrightarrow Part(S(x, y), y) \land Part(S(x, y), x) \tag{c}\label{eqc}$$
From (\ref{eqb}) and (\ref{eqc}) and the assumption on the Skolem functions that $\exists Sk \exists S \forall x \forall y \; Sk(x, y) = S(x, y)$, it follows
$$\forall x \forall y \;  Overlap(x,y) \Leftrightarrow Overlap(y, x) $$
A: We can translate the original bi-conditional axiom into three implications. Using the quantifier equivalence, $\exists x (Q(x) \implies P) \equiv \forall x Q(x) \implies P $, the existential in the original  (1) can be replaced by a universal $z$, so line 3 below does not need a Skolem function. I believe these 3 sentences and the FOL sentence (1) are equisatisfiable. I believe breaking  (1) into three parts makes the proof fairly straightforward.
Proof
\begin{align}
& \text{1}~~\forall x \forall y : (Overlap(x,y) \implies  Part(Sk(x,y),x)) & \tag{Axiom1}\\
& \text{2}~~\forall x \forall y : (Overlap(x,y) \implies  Part(Sk(x,y),y))& \tag{Axiom2}\\
& \text{3}~~\forall x \forall y \forall z : ((Part(z,x) \land Part(z,y)) \implies Overlap(x,y))& \tag{Axiom3}\\
&  \text{4 (a,b)}~~Overlap(a,b) \tag{Assume} \\
&  \text{5}~~~~~~~~~~~~~(Part(Sk(a,b) ,a) \land Part(Sk(a,b) ,b))  \implies Overlap(a,b)   \tag{$\forall$-Elim 3}\\
&  \text{6}~~~~~~~~~~~~~Overlap(a,b)  \implies  Part(Sk(a,b),a)   \tag{$\forall$-Elim 1}\\
&  \text{7}~~~~~~~~~~~~~Overlap(a,b)  \implies  Part(Sk(a,b),b)   \tag{$\forall$-Elim 2}\\
&  \text{8}~~~~~~~~~~~~~Part(Sk(a,b),a)  \tag{$\implies$-Elim 4,6}\\
&  \text{9}~~~~~~~~~~~~~Part(Sk(a,b),b)  \tag{$\implies$-Elim 4,7}\\
&  \text{10}~~~~~~~~~~~~~Part(Sk(a,b),b)  \land  Part(Sk(a,b),a)  \tag{$\land$-Intro 8,9}\\
&  \text{11}~~~~~~~~~~~~~(Part(Sk(a,b) ,b) \land Part(Sk(a,b) ,a))  \implies Overlap(b,a)   \tag{$\forall$-Elim 3}\\
&  \text{12}~~~~~~~~~~~~~Overlap(b,a) \tag{$\implies$-Elim 10,11}\\
&  \text{13}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{$\forall$-Intro 4-12} \\
\end{align}
