What happens to uninterpreted predicates in Ackermann's reduction?
Essentially, you can treat uninterpreted predicates as boolean-valued functions (adding a new boolean sort if necessary) and replace them with boolean variables as you would other functions. For the given example:

Getting rid of $F$ and $G$ first: 

$$\begin{align*}
p(z,f_1)&amp;\wedge f_2=g_1\to p(x_1,y)\wedge x_1=f_1\to f_1=f_2\\
  &amp;\wedge x_1=x_2\to f_1=f_3\wedge f_1=x_2\to f_2=f_3\\
  &amp;\wedge (x_1=x_2\wedge g_2=x_3\wedge f_3=x_4)\to g_1=g_2
\end{align*}$$

Introduce boolean variables $b_1,b_2$ for $p(z,f_1)$ and $p(x_1,y)$, respectively, and add a condition that they are equivalent when the arguments agree:

$$\begin{align*}
b_1 &amp;\wedge f_2=g_1\to b_2\wedge x_1=f_1\to f_1=f_2\\
  &amp;\wedge x_1=x_2\to f_1=f_3\wedge f_1=x_2\to f_2=f_3\\
  &amp;\wedge (x_1=x_2\wedge g_2=x_3\wedge f_3=x_4)\to g_1=g_2\wedge (z=x_1\wedge f_1=y)\to(b_1\leftrightarrow b_2)
\end{align*}$$