Questionnaire-2024/smt/3000_sol.tex

We start by computing $\skel$:
\begin{compactItemize}
	\item $e_{0}\Leftrightarrow(x=y)$
	\item $e_{1}\Leftrightarrow(y=f(y))$
	\item $e_{2}\Leftrightarrow(y=f(x))$
	\item $e_{3}\Leftrightarrow(z=f(z))$
	\item $e_{4}\Leftrightarrow(f(z)=f(x))$
\end{compactItemize}


$$ \skel = e_{0} \land e_{1} \land \neg e_{2} \land e_{3} \land e_{4}$$

\hspace{-0.09cm}\scalebox{0.85}{
	\begin{dplltabular}{6}
		\dpllStep{1|2|3|4|5|6}
		\dpllDecL{0|0|0|0|0|0}
		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{1}$|$e_{0}, e_{1}, \lnot e_{2}$|\makecell{$e_{0}, e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|\makecell{$e_{0}, e_{1}, \lnot e_{2}, $ \\ $e_{3}, e_{4}$}}
		\dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done|\done}
		\dpllClause{2}{$e_{1}$}{$e_{1}$|$e_{1}$|\done|\done|\done|\done}
		\dpllClause{3}{$\lnot e_{2}$}{$\lnot e_{2}$|$\lnot e_{2}$|$\lnot e_{2}$|\done|\done|\done}
		\dpllClause{4}{$e_{3}$}{$e_{3}$|$e_{3}$|$e_{3}$|$e_{3}$|\done|\done}
		\dpllClause{5}{$e_{4}$}{$e_{4}$|$e_{4}$|$e_{4}$|$e_{4}$|$e_{4}$|\done}
		\dpllBCP{$e_{0}$|$e_{1}$|$\lnot e_{2}$|$e_{3}$|$e_{4}$| - }
		\dpllPL{ - | - | - | - | - | - }
		\dpllDeci{ - | - | - | - | - |SAT}
	\end{dplltabular}
}

\vspace{0.5em}
The SAT solver has computed that $\skel$ is satisfiable, we are therefore going to check for consistency with the theory:
\begin{align*}
	&\{x, y\}, \{y, f(y)\}, \{z, f(z)\}, \{f(z), f(x)\}\\
	&\{f(y), x, y\}, \{f(x), f(z), z\}
\end{align*}
The $\EUF$-Solver returned SAT, therefore $\varphi$ is satisfiable.