\item \applyAckermann{
    \begin{equation*}
    \varphi_{EUF}  :=   f(x)=y \land x=g(x) \lor \\
    x \neq f(x) \land g(x)=f(g(x)) \lor \\
    y \neq g(x) \land x=f(y) \land g(y)=f(g(x))
    \end{equation*}
  }