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.
Best Answer
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) $$