diff --git a/smt/2001.tex b/smt/2001.tex
index a2ea042..f6edba8 100644
--- a/smt/2001.tex
+++ b/smt/2001.tex
@@ -1,3 +1,3 @@
 \item \ifassignmentsheet \points{2} \fi \applyAckermann{
-        $$f(x)=g(x) \lor z=f(y) \imp f(z) \neq g(y) \land x=z$$
+        $$f(x)=g(x) \lor z=f(y) \imp f(z) \neq g(y) \land x=z.$$
 }
diff --git a/smt/2004.tex b/smt/2004.tex
index 4fe8045..208acb0 100644
--- a/smt/2004.tex
+++ b/smt/2004.tex
@@ -1,3 +1,3 @@
 \item \ifassignmentsheet \points{2} \fi \applyAckermann{
-$$ \varphi_{EUF} := f(a,b)=x \land f(x,y)\neq g(a) \lor f(m,n)=b \lor f(g(a),y) \neq a$$
+$$ \varphi_{EUF} := f(a,b)=x \land f(x,y)\neq g(a) \lor f(m,n)=b \lor f(g(a),y) \neq a.$$
 }
diff --git a/smt/3013.tex b/smt/3013.tex
new file mode 100644
index 0000000..3043538
--- /dev/null
+++ b/smt/3013.tex
@@ -0,0 +1,8 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+\varphi = &(\clause{(f(a)=b); (f(a)=c); \lnot (b=c)}) \land (\clause{(b=c); (a=b); (f(a)=b)})~\land\\
+          &(\clause{\lnot (f(a)=b); (a=b)}) \land (\clause{(b=c); \lnot (a=b); \lnot (f(a)=b)})~\land\\
+          &(\clause{\lnot (f(a)=c); (b=c)}) \land (\clause{\lnot (f(a)=c); (b=c); \lnot (a=b)})~\land\\
+          &(\clause{(f(a)=b); (f(a)=c)})
+  \end{align*}
diff --git a/smt/3013_sol.tex b/smt/3013_sol.tex
new file mode 100644
index 0000000..763ca88
--- /dev/null
+++ b/smt/3013_sol.tex
@@ -0,0 +1,61 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(f(a)=b)$
+	\item $e_{1}\Leftrightarrow(f(a)=c)$
+	\item $e_{2}\Leftrightarrow(b=c)$
+	\item $e_{3}\Leftrightarrow(a=b)$
+\end{itemize}
+
+$\hat{\varphi} = (\clause{e_{0}; e_{1}; \lnot e_{2}}) \land (\clause{e_{2}; e_{3}; e_{0}}) \land (\clause{\lnot e_{0}; e_{3}}) \land (\clause{e_{2}; \lnot e_{3}; \lnot e_{0}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{\lnot e_{1}; e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; e_{1}}) $
+
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{1|2|3|4}
+		\dpllDecL{0|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$}
+		\dpllClause{1}{$e_{0}, e_{1}, \lnot e_{2}$}{$e_{0}, e_{1}, \lnot e_{2}$|$e_{1}, \lnot e_{2}$|\done|\done}
+		\dpllClause{2}{$e_{2}, e_{3}, e_{0}$}{$e_{2}, e_{3}, e_{0}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done}
+		\dpllClause{3}{$\lnot e_{0}, e_{3}$}{$\lnot e_{0}, e_{3}$|\done|\done|\done}
+		\dpllClause{4}{$e_{2}, \lnot e_{3}, \lnot e_{0}$}{$e_{2}, \lnot e_{3}, \lnot e_{0}$|\done|\done|\done}
+		\dpllClause{5}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done}
+		\dpllClause{6}{$\lnot e_{1}, e_{2}, \lnot e_{3}$}{$\lnot e_{1}, e_{2}, \lnot e_{3}$|$\lnot e_{1}, e_{2}, \lnot e_{3}$|$e_{2}, \lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done}
+		\dpllBCP{ - |$e_{1}$|$e_{2}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - }
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := \{(f(a) \neq b), (f(a) = c), (b = c)\} $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{f(a), c\}, \{b, c\}\\
+	&\{b, c, f(a)\}
+\end{align*}
+
+$\Model_{\EUF}$ is not consistent with the theory, because of: $(f(a) \neq b) $\\
+$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}$:
+
+$BC_8 := e_0 \lor \neg e_1 \lor \neg e_2 $ \\
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{5|6|7|8}
+		\dpllDecL{0|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, \lnot e_{2}$}
+		\dpllClause{1}{$e_{0}, e_{1}, \lnot e_{2}$}{$e_{0}, e_{1}, \lnot e_{2}$|$e_{1}, \lnot e_{2}$|\done|\done}
+		\dpllClause{2}{$e_{2}, e_{3}, e_{0}$}{$e_{2}, e_{3}, e_{0}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$}
+		\dpllClause{3}{$\lnot e_{0}, e_{3}$}{$\lnot e_{0}, e_{3}$|\done|\done|\done}
+		\dpllClause{4}{$e_{2}, \lnot e_{3}, \lnot e_{0}$}{$e_{2}, \lnot e_{3}, \lnot e_{0}$|\done|\done|\done}
+		\dpllClause{5}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\conflict}
+		\dpllClause{6}{$\lnot e_{1}, e_{2}, \lnot e_{3}$}{$\lnot e_{1}, e_{2}, \lnot e_{3}$|$\lnot e_{1}, e_{2}, \lnot e_{3}$|$e_{2}, \lnot e_{3}$|$\lnot e_{3}$}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done}
+		\blockingClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}$}{$e_{0}, \lnot e_{1}, \lnot e_{2}$|$\lnot e_{1}, \lnot e_{2}$|$\lnot e_{2}$|\done}
+		\dpllBCP{ - |$e_{1}$|$\lnot e_{2}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - }
+	\end{dplltabular}
+}
+
diff --git a/smt/3013_sol_second_part.tex b/smt/3013_sol_second_part.tex
new file mode 100644
index 0000000..513ae42
--- /dev/null
+++ b/smt/3013_sol_second_part.tex
@@ -0,0 +1,98 @@
+Conflict in step 8\\
+\scalebox{0.75}{
+
+\begin{tikzpicture}[>=latex,line join=bevel,]
+  \pgfsetlinewidth{1bp}
+%%
+\pgfsetcolor{black}
+  % Edge: 1 -> 4
+  \draw [->] (22.3bp,31.0bp) .. controls (35.47bp,31.0bp) and (58.583bp,31.0bp)  .. (85.878bp,31.0bp);
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (54.0bp,38.5bp) node {$$7$$};
+  % Edge: 3 -> 2
+  \draw [->] (193.67bp,47.438bp) .. controls (201.41bp,44.585bp) and (212.51bp,40.495bp)  .. (231.47bp,33.51bp);
+  % Edge: 4 -> 3
+  \draw [->] (107.97bp,33.373bp) .. controls (121.23bp,36.53bp) and (144.98bp,42.186bp)  .. (172.05bp,48.63bp);
+  \draw (140.0bp,50.5bp) node {$$5$$};
+  % Edge: 4 -> 5
+  \draw [->] (107.11bp,26.371bp) .. controls (112.48bp,23.828bp) and (119.48bp,20.828bp)  .. (126.0bp,19.0bp) .. controls (137.65bp,15.733bp) and (151.06bp,13.758bp)  .. (171.92bp,11.639bp);
+  \draw (140.0bp,26.5bp) node {$$8$$};
+  % Edge: 5 -> 2
+  \draw [->] (193.67bp,14.223bp) .. controls (201.24bp,16.746bp) and (212.02bp,20.339bp)  .. (231.09bp,26.697bp);
+  % Node: 1
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,31.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,31.0bp) node {$\lnot e_{0}$};
+\end{scope}
+  % Node: 4
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,31.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,31.0bp) node {$e_{1}$};
+\end{scope}
+  % Node: 2
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (242.0bp,30.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (242.0bp,30.0bp) node {$\bot$};
+\end{scope}
+  % Node: 3
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (183.0bp,51.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (183.0bp,51.0bp) node {$e_{2}$};
+\end{scope}
+  % Node: 5
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (183.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (183.0bp,11.0bp) node {$\lnot e_{2}$};
+\end{scope}
+%
+\end{tikzpicture}
+
+
+}
+\begin{prooftree}
+	\AxiomC{$5. \; \lnot e_{1} \lor e_{2}$}
+	\AxiomC{$8. \; e_{0} \lor \lnot e_{1} \lor \lnot e_{2}$}
+	\BinaryInfC{$\lnot e_{1} \lor e_{0}$}
+	\AxiomC{$7. \; e_{0} \lor e_{1}$}
+	\BinaryInfC{$e_{0}$}
+\end{prooftree}
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{9|10|11|12}
+		\dpllDecL{0|0|0|0}
+		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{3}$|$e_{0}, e_{3}, e_{2}$}
+		\dpllClause{1}{$e_{0}, e_{1}, \lnot e_{2}$}{$e_{0}, e_{1}, \lnot e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$e_{2}, e_{3}, e_{0}$}{$e_{2}, e_{3}, e_{0}$|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{0}, e_{3}$}{$\lnot e_{0}, e_{3}$|$e_{3}$|\done|\done}
+		\dpllClause{4}{$e_{2}, \lnot e_{3}, \lnot e_{0}$}{$e_{2}, \lnot e_{3}, \lnot e_{0}$|$e_{2}, \lnot e_{3}$|$e_{2}$|\done}
+		\dpllClause{5}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done}
+		\dpllClause{6}{$\lnot e_{1}, e_{2}, \lnot e_{3}$}{$\lnot e_{1}, e_{2}, \lnot e_{3}$|$\lnot e_{1}, e_{2}, \lnot e_{3}$|$\lnot e_{1}, e_{2}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|\done|\done|\done}
+		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}$}{$e_{0}, \lnot e_{1}, \lnot e_{2}$|\done|\done|\done}
+		\dpllClause{9}{$e_{0}$}{$e_{0}$|\done|\done|\done}
+		\dpllBCP{$e_{0}$|$e_{3}$|$e_{2}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{ - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (f(a) = b) \land (b = c) \land (a = b) $ \\
+Check if the assignment is consistent with the theory:
+\begin{align*}
+	&\{f(a), b\}, \{b, c\}, \{a, b\}\\
+	&\{a, b, c, f(a)\}
+\end{align*}
+$\Model_{\EUF}$ is consistent with the theory, \\
+$\Rightarrow$ $\Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3014.tex b/smt/3014.tex
new file mode 100644
index 0000000..daaa711
--- /dev/null
+++ b/smt/3014.tex
@@ -0,0 +1,9 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+    \varphi =& (\clause{\lnot (f(a)=f(b)); (f(a)=c); (a=b)}) \land (\clause{\lnot (f(a)=c); (a=b); \lnot (f(c)=a)})~\land\\
+             & (\clause{(f(a)=f(b)); \lnot (f(a)=c)}) \land (\clause{\lnot (f(a)=f(b)); (a=b)})~\land \\
+             & (\clause{\lnot (a=b); \lnot (f(c)=a)}) \land (\clause{(f(a)=f(b)); (a=b)})~\land \\
+             & (\clause{\lnot (a=b); \lnot (f(a)=c)})
+  \end{align*}
+
diff --git a/smt/3014_sol.tex b/smt/3014_sol.tex
new file mode 100644
index 0000000..28e810e
--- /dev/null
+++ b/smt/3014_sol.tex
@@ -0,0 +1,37 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(f(a)=f(b))$
+	\item $e_{1}\Leftrightarrow(f(a)=c)$
+	\item $e_{2}\Leftrightarrow(a=b)$
+	\item $e_{3}\Leftrightarrow(f(c)=a)$
+\end{itemize}
+
+$\hat{\varphi} = (\clause{\lnot e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{1}; e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; \lnot e_{1}}) \land (\clause{\lnot e_{0}; e_{2}}) \land (\clause{\lnot e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; e_{2}}) \land (\clause{\lnot e_{2}; \lnot e_{1}}) $
+
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{1|2|3|4|5}
+		\dpllDecL{0|0|1|1|1}
+		\dpllAssi{ - |$\lnot e_{3}$|$\lnot e_{3}, \lnot e_{0}$|$\lnot e_{3}, \lnot e_{0}, \lnot e_{1}$|\makecell{$\lnot e_{3}, \lnot e_{0}, \lnot e_{1}, $ \\ $e_{2}$}}
+		\dpllClause{1}{$\lnot e_{0}, e_{1}, e_{2}$}{$\lnot e_{0}, e_{1}, e_{2}$|$\lnot e_{0}, e_{1}, e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{1}, e_{2}, \lnot e_{3}$}{$\lnot e_{1}, e_{2}, \lnot e_{3}$|\done|\done|\done|\done}
+		\dpllClause{3}{$e_{0}, \lnot e_{1}$}{$e_{0}, \lnot e_{1}$|$e_{0}, \lnot e_{1}$|$\lnot e_{1}$|\done|\done}
+		\dpllClause{4}{$\lnot e_{0}, e_{2}$}{$\lnot e_{0}, e_{2}$|$\lnot e_{0}, e_{2}$|\done|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, \lnot e_{3}$}{$\lnot e_{2}, \lnot e_{3}$|\done|\done|\done|\done}
+		\dpllClause{6}{$e_{0}, e_{2}$}{$e_{0}, e_{2}$|$e_{0}, e_{2}$|$e_{2}$|$e_{2}$|\done}
+		\dpllClause{7}{$\lnot e_{2}, \lnot e_{1}$}{$\lnot e_{2}, \lnot e_{1}$|$\lnot e_{2}, \lnot e_{1}$|$\lnot e_{2}, \lnot e_{1}$|\done|\done}
+		\dpllBCP{ - | - |$\lnot e_{1}$|$e_{2}$| - }
+		\dpllPL{$\lnot e_{3}$| - | - | - | - }
+		\dpllDeci{ - |$\lnot e_{0}$| - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (f(a) \neq f(b)) \land (f(a) \neq c) \land (a = b) \land (f(c) \neq a) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{a, b\}, \{f(a)\}, \{f(b)\}, \{c\}, \{f(c)\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3015.tex b/smt/3015.tex
new file mode 100644
index 0000000..aed0c04
--- /dev/null
+++ b/smt/3015.tex
@@ -0,0 +1,9 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+  \varphi =& (\clause{(a=x); (a=y); (x=y)})\land (\clause{\lnot (a=x); (a=y)})~\land \\
+           & (\clause{\lnot (a=y); (x=y)})\land (\clause{(x=y); (z=a)})~\land \\
+           & (\clause{\lnot (x=y); (b=z)})\land (\clause{\lnot (z=a); \lnot (b=z)})
+  \end{align*}
+
+
diff --git a/smt/3015_sol.tex b/smt/3015_sol.tex
new file mode 100644
index 0000000..0857f21
--- /dev/null
+++ b/smt/3015_sol.tex
@@ -0,0 +1,36 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(a=x)$
+	\item $e_{1}\Leftrightarrow(a=y)$
+	\item $e_{2}\Leftrightarrow(x=y)$
+	\item $e_{3}\Leftrightarrow(z=a)$
+	\item $e_{4}\Leftrightarrow(b=z)$
+\end{itemize}
+
+$\hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}})\land (\clause{\lnot e_{0}; e_{1}})\land (\clause{\lnot e_{1}; e_{2}})\land (\clause{e_{2}; e_{3}})\land (\clause{\lnot e_{2}; e_{4}})\land (\clause{\lnot e_{3}; \lnot e_{4}})$
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{6}
+		\dpllStep{1|2|3|4|5|6}
+		\dpllDecL{0|1|2|2|2|2}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, e_{2}$|\makecell{$\lnot e_{0}, \lnot e_{1}, e_{2}, $ \\ $e_{4}$}|\makecell{$\lnot e_{0}, \lnot e_{1}, e_{2}, $ \\ $e_{4}, \lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{4}$}{$\lnot e_{2}, e_{4}$|$\lnot e_{2}, e_{4}$|$\lnot e_{2}, e_{4}$|$e_{4}$|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{4}$}{$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}$|\done}
+		\dpllBCP{ - | - |$e_{2}$|$e_{4}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (a \neq x) \land (a \neq y) \land (x = y) \land (z \neq a) \land (b = z) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{x, y\}, \{b, z\}, \{a\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3016.tex b/smt/3016.tex
new file mode 100644
index 0000000..dfed612
--- /dev/null
+++ b/smt/3016.tex
@@ -0,0 +1,8 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+\begin{align*}
+  \varphi =&(\clause{(f(x)=x); (f(x)=y); (x=y)}) \land (\clause{\lnot (f(x)=x); (f(x)=y)})~\land \\
+           &(\clause{\lnot (f(x)=y); (x=y)}) \land (\clause{(x=y); (z=f(x))})~\land \\
+           &(\clause{\lnot (x=y); (f(x)=y)}) \land (\clause{\lnot (z=f(x)); \lnot (f(x)=y)})
+\end{align*}
+
diff --git a/smt/3016_sol.tex b/smt/3016_sol.tex
new file mode 100644
index 0000000..63c6517
--- /dev/null
+++ b/smt/3016_sol.tex
@@ -0,0 +1,126 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(f(x)=x)$
+	\item $e_{1}\Leftrightarrow(f(x)=y)$
+	\item $e_{2}\Leftrightarrow(x=y)$
+	\item $e_{3}\Leftrightarrow(z=f(x))$
+\end{itemize}
+
+
+$\hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{0}; e_{1}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{e_{2}; e_{3}}) \land (\clause{\lnot e_{2}; e_{1}}) \land (\clause{\lnot e_{3}; \lnot e_{1}}) $
+
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{1|2|3|4}
+		\dpllDecL{0|1|2|2}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, \lnot e_{2}$}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\conflict}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|$\lnot e_{2}$|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|\done|\done}
+		\dpllBCP{ - | - |$\lnot e_{2}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - }
+	\end{dplltabular}
+}
+
+Conflict in step 4\\
+\scalebox{0.75}{
+
+\begin{tikzpicture}[>=latex,line join=bevel,]
+  \pgfsetlinewidth{1bp}
+%%
+\pgfsetcolor{black}
+  % Edge: 1 -> 4
+  \draw [->] (21.08bp,83.506bp) .. controls (26.44bp,80.758bp) and (33.44bp,77.508bp)  .. (40.0bp,75.5bp) .. controls (51.601bp,71.949bp) and (65.006bp,69.732bp)  .. (85.898bp,67.281bp);
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (54.0bp,83.0bp) node {$$1$$};
+  % Edge: 1 -> 5
+  \draw [->] (21.966bp,90.636bp) .. controls (35.227bp,93.477bp) and (58.98bp,98.567bp)  .. (86.047bp,104.37bp);
+  \draw (54.0bp,107.0bp) node {$$5$$};
+  % Edge: 2 -> 4
+  \draw [->] (21.717bp,33.396bp) .. controls (33.05bp,36.904bp) and (52.243bp,43.253bp)  .. (68.0bp,50.5bp) .. controls (71.462bp,52.092bp) and (75.062bp,53.969bp)  .. (87.382bp,61.048bp);
+  \draw (54.0bp,58.0bp) node {$$1$$};
+  % Edge: 4 -> 3
+  \draw [->] (107.67bp,69.723bp) .. controls (115.24bp,72.246bp) and (126.02bp,75.839bp)  .. (145.09bp,82.197bp);
+  % Edge: 5 -> 3
+  \draw [->] (107.67bp,102.94bp) .. controls (115.41bp,100.08bp) and (126.51bp,95.995bp)  .. (145.47bp,89.01bp);
+  % Node: 1
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,88.5bp) node {$\lnot e_{1}$};
+\end{scope}
+  % Node: 4
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,66.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,66.5bp) node {$e_{2}$};
+\end{scope}
+  % Node: 5
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,106.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,106.5bp) node {$\lnot e_{2}$};
+\end{scope}
+  % Node: 2
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,30.5bp) node {$\lnot e_{0}$};
+\end{scope}
+  % Node: 3
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (156.0bp,85.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (156.0bp,85.5bp) node {$\bot$};
+\end{scope}
+%
+\end{tikzpicture}
+
+
+}
+\begin{prooftree}
+	\AxiomC{$1. \; e_{0} \lor e_{1} \lor e_{2}$}
+	\AxiomC{$5. \; \lnot e_{2} \lor e_{1}$}
+	\BinaryInfC{$e_{0} \lor e_{1}$}
+\end{prooftree}
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{5|6|7|8}
+		\dpllDecL{1|1|1|1}
+		\dpllAssi{$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{1}, e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{1}$|\done|\done|\done}
+		\dpllBCP{$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{ - | - | - | - }
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (f(x) \neq x) \land (f(x) = y) \land (x = y) \land (z \neq f(x)) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{f(x), y\}, \{x, y\}, \{z\}\\
+	&\{z\}, \{f(x), x, y\}
+\end{align*}
+
+$\Model_{\EUF}$ is not consistent with the theory, because of: $(f(x) \neq x) $\\
+$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
+$BC :=e_{0} \lor \neg e_{1} \lor \neg e_{2} \lor e_{3}$\\
diff --git a/smt/3016_sol_second_part.tex b/smt/3016_sol_second_part.tex
new file mode 100644
index 0000000..e1bac5b
--- /dev/null
+++ b/smt/3016_sol_second_part.tex
@@ -0,0 +1,133 @@
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{9|10|11|12|13}
+		\dpllDecL{0|1|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
+		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|$\lnot e_{1}, \lnot e_{2}, e_{3}$|$\lnot e_{2}, e_{3}$|$e_{3}$|\conflict}
+		\dpllBCP{ - |$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - | - }
+	\end{dplltabular}
+}
+
+Conflict in step 13\\
+\scalebox{0.75}{
+
+\begin{tikzpicture}[>=latex,line join=bevel,]
+  \pgfsetlinewidth{1bp}
+%%
+\pgfsetcolor{black}
+  % Edge: 1 -> 5
+  \draw [->] (22.3bp,50.0bp) .. controls (35.47bp,50.0bp) and (58.583bp,50.0bp)  .. (85.878bp,50.0bp);
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (54.0bp,57.5bp) node {$$7$$};
+  % Edge: 3 -> 6
+  \draw [->] (197.32bp,50.0bp) .. controls (211.2bp,50.0bp) and (236.16bp,50.0bp)  .. (263.96bp,50.0bp);
+  \draw (232.0bp,57.5bp) node {$$8$$};
+  % Edge: 4 -> 2
+  \draw [->] (242.95bp,12.194bp) .. controls (259.12bp,14.134bp) and (291.4bp,18.008bp)  .. (322.79bp,21.775bp);
+  % Edge: 5 -> 3
+  \draw [->] (108.32bp,50.0bp) .. controls (122.2bp,50.0bp) and (147.16bp,50.0bp)  .. (174.96bp,50.0bp);
+  \draw (140.0bp,57.5bp) node {$$3$$};
+  % Edge: 5 -> 4
+  \draw [->] (105.82bp,43.402bp) .. controls (111.18bp,39.225bp) and (118.62bp,34.054bp)  .. (126.0bp,31.0bp) .. controls (154.04bp,19.403bp) and (189.09bp,14.461bp)  .. (220.77bp,11.572bp);
+  \draw (140.0bp,38.5bp) node {$$6$$};
+  % Edge: 5 -> 6
+  \draw [->] (105.67bp,57.009bp) .. controls (110.96bp,61.36bp) and (118.39bp,66.571bp)  .. (126.0bp,69.0bp) .. controls (176.81bp,85.217bp) and (195.19bp,85.217bp)  .. (246.0bp,69.0bp) .. controls (250.16bp,67.671bp) and (254.27bp,65.511bp)  .. (266.33bp,57.009bp);
+  \draw (186.0bp,89.5bp) node {$$8$$};
+  % Edge: 6 -> 2
+  \draw [->] (285.16bp,45.662bp) .. controls (293.01bp,41.945bp) and (304.56bp,36.472bp)  .. (323.68bp,27.417bp);
+  % Node: 1
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,50.0bp) node {$\lnot e_{0}$};
+\end{scope}
+  % Node: 5
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,50.0bp) node {$e_{1}$};
+\end{scope}
+  % Node: 2
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (334.0bp,23.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (334.0bp,23.0bp) node {$\bot$};
+\end{scope}
+  % Node: 3
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (186.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (186.0bp,50.0bp) node {$e_{2}$};
+\end{scope}
+  % Node: 6
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (275.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (275.0bp,50.0bp) node {$e_{3}$};
+\end{scope}
+  % Node: 4
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (232.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (232.0bp,11.0bp) node {$\lnot e_{3}$};
+\end{scope}
+%
+\end{tikzpicture}
+
+
+}
+\begin{prooftree}
+	\AxiomC{$8. \; e_{0} \lor \lnot e_{1} \lor \lnot e_{2} \lor e_{3}$}
+	\AxiomC{$3. \; \lnot e_{1} \lor e_{2}$}
+	\BinaryInfC{$e_{0} \lor \lnot e_{1} \lor e_{3}$}
+	\AxiomC{$6. \; \lnot e_{3} \lor \lnot e_{1}$}
+	\BinaryInfC{$e_{0} \lor \lnot e_{1}$}
+	\AxiomC{$7. \; e_{0} \lor e_{1}$}
+	\BinaryInfC{$e_{0}$}
+\end{prooftree}
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{14|15|16|17|18}
+		\dpllDecL{0|0|0|0|0}
+		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{1}$|$e_{0}, e_{1}, e_{2}$|\makecell{$e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|\done|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|\done|\done|\done|\done}
+		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|\done|\done|\done|\done}
+		\dpllClause{9}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done}
+		\dpllBCP{$e_{0}$|$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - | - }
+		\dpllDeci{ - | - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (f(x) = x) \land (f(x) = y) \land (x = y) \land (z \neq f(x)) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{f(x), x\}, \{f(x), y\}, \{x, y\}, \{z\}\\
+	&\{z\}, \{f(x), x, y\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3017.tex b/smt/3017.tex
new file mode 100644
index 0000000..7bf5908
--- /dev/null
+++ b/smt/3017.tex
@@ -0,0 +1,7 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+	\varphi= 	& (\clause{(a=b); (a=f(a)); (b=f(a))}) \land (\clause{\lnot (a=b); (a=f(a))})~\land \\
+		        & (\clause{\lnot (a=f(a)); (b=f(a))}) \land (\clause{(b=f(a)); (d=a)})~\land \\
+		        & (\clause{\lnot (b=f(a)); (a=f(a))}) \land (\clause{\lnot (d=a); \lnot (a=f(a))})
+  \end{align*}
diff --git a/smt/3017_sol.tex b/smt/3017_sol.tex
new file mode 100644
index 0000000..1641e62
--- /dev/null
+++ b/smt/3017_sol.tex
@@ -0,0 +1,125 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(a=b)$
+	\item $e_{1}\Leftrightarrow(a=f(a))$
+	\item $e_{2}\Leftrightarrow(b=f(a))$
+	\item $e_{3}\Leftrightarrow(d=a)$
+\end{itemize}
+
+$ \hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{0}; e_{1}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{e_{2}; e_{3}}) \land (\clause{\lnot e_{2}; e_{1}}) \land (\clause{\lnot e_{3}; \lnot e_{1}}) $
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{1|2|3|4}
+		\dpllDecL{0|1|2|2}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, \lnot e_{2}$}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\conflict}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|$\lnot e_{2}$|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|\done|\done}
+		\dpllBCP{ - | - |$\lnot e_{2}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - }
+	\end{dplltabular}
+}
+
+Conflict in step 4\\
+\scalebox{0.75}{
+
+\begin{tikzpicture}[>=latex,line join=bevel,]
+  \pgfsetlinewidth{1bp}
+%%
+\pgfsetcolor{black}
+  % Edge: 1 -> 4
+  \draw [->] (21.08bp,83.506bp) .. controls (26.44bp,80.758bp) and (33.44bp,77.508bp)  .. (40.0bp,75.5bp) .. controls (51.601bp,71.949bp) and (65.006bp,69.732bp)  .. (85.898bp,67.281bp);
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (54.0bp,83.0bp) node {$$1$$};
+  % Edge: 1 -> 5
+  \draw [->] (21.966bp,90.636bp) .. controls (35.227bp,93.477bp) and (58.98bp,98.567bp)  .. (86.047bp,104.37bp);
+  \draw (54.0bp,107.0bp) node {$$5$$};
+  % Edge: 2 -> 4
+  \draw [->] (21.717bp,33.396bp) .. controls (33.05bp,36.904bp) and (52.243bp,43.253bp)  .. (68.0bp,50.5bp) .. controls (71.462bp,52.092bp) and (75.062bp,53.969bp)  .. (87.382bp,61.048bp);
+  \draw (54.0bp,58.0bp) node {$$1$$};
+  % Edge: 4 -> 3
+  \draw [->] (107.67bp,69.723bp) .. controls (115.24bp,72.246bp) and (126.02bp,75.839bp)  .. (145.09bp,82.197bp);
+  % Edge: 5 -> 3
+  \draw [->] (107.67bp,102.94bp) .. controls (115.41bp,100.08bp) and (126.51bp,95.995bp)  .. (145.47bp,89.01bp);
+  % Node: 1
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,88.5bp) node {$\lnot e_{1}$};
+\end{scope}
+  % Node: 4
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,66.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,66.5bp) node {$e_{2}$};
+\end{scope}
+  % Node: 5
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,106.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,106.5bp) node {$\lnot e_{2}$};
+\end{scope}
+  % Node: 2
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,30.5bp) node {$\lnot e_{0}$};
+\end{scope}
+  % Node: 3
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (156.0bp,85.5bp) ellipse (11.0bp and 11.0bp);
+  \draw (156.0bp,85.5bp) node {$\bot$};
+\end{scope}
+%
+\end{tikzpicture}
+
+
+}
+\begin{prooftree}
+	\AxiomC{$1. \; e_{0} \lor e_{1} \lor e_{2}$}
+	\AxiomC{$5. \; \lnot e_{2} \lor e_{1}$}
+	\BinaryInfC{$e_{0} \lor e_{1}$}
+\end{prooftree}
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{4}
+		\dpllStep{5|6|7|8}
+		\dpllDecL{1|1|1|1}
+		\dpllAssi{$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{1}, e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{1}$|\done|\done|\done}
+		\dpllBCP{$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - }
+		\dpllDeci{ - | - | - | - }
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (b = f(a)) \land (d \neq a) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{a, f(a)\}, \{b, f(a)\}, \{d\}\\
+	&\{d\}, \{a, b, f(a)\}
+\end{align*}
+
+$\Model_{\EUF}$ is not consistent with the theory, because of: $(a \neq b) $\\
+$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
+$BC :=e_{0} \lor \neg e_{1} \lor \neg e_{2} \lor e_{3}$\\
+
diff --git a/smt/3017_sol_second_part.tex b/smt/3017_sol_second_part.tex
new file mode 100644
index 0000000..7c71598
--- /dev/null
+++ b/smt/3017_sol_second_part.tex
@@ -0,0 +1,133 @@
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{9|10|11|12|13}
+		\dpllDecL{0|1|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
+		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|$\lnot e_{1}, \lnot e_{2}, e_{3}$|$\lnot e_{2}, e_{3}$|$e_{3}$|\conflict}
+		\dpllBCP{ - |$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - | - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - | - }
+	\end{dplltabular}
+}
+
+Conflict in step 13\\
+\scalebox{0.75}{
+
+\begin{tikzpicture}[>=latex,line join=bevel,]
+  \pgfsetlinewidth{1bp}
+%%
+\pgfsetcolor{black}
+  % Edge: 1 -> 5
+  \draw [->] (22.3bp,50.0bp) .. controls (35.47bp,50.0bp) and (58.583bp,50.0bp)  .. (85.878bp,50.0bp);
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (54.0bp,57.5bp) node {$$7$$};
+  % Edge: 3 -> 6
+  \draw [->] (197.32bp,50.0bp) .. controls (211.2bp,50.0bp) and (236.16bp,50.0bp)  .. (263.96bp,50.0bp);
+  \draw (232.0bp,57.5bp) node {$$8$$};
+  % Edge: 4 -> 2
+  \draw [->] (242.95bp,12.194bp) .. controls (259.12bp,14.134bp) and (291.4bp,18.008bp)  .. (322.79bp,21.775bp);
+  % Edge: 5 -> 3
+  \draw [->] (108.32bp,50.0bp) .. controls (122.2bp,50.0bp) and (147.16bp,50.0bp)  .. (174.96bp,50.0bp);
+  \draw (140.0bp,57.5bp) node {$$3$$};
+  % Edge: 5 -> 4
+  \draw [->] (105.82bp,43.402bp) .. controls (111.18bp,39.225bp) and (118.62bp,34.054bp)  .. (126.0bp,31.0bp) .. controls (154.04bp,19.403bp) and (189.09bp,14.461bp)  .. (220.77bp,11.572bp);
+  \draw (140.0bp,38.5bp) node {$$6$$};
+  % Edge: 5 -> 6
+  \draw [->] (105.67bp,57.009bp) .. controls (110.96bp,61.36bp) and (118.39bp,66.571bp)  .. (126.0bp,69.0bp) .. controls (176.81bp,85.217bp) and (195.19bp,85.217bp)  .. (246.0bp,69.0bp) .. controls (250.16bp,67.671bp) and (254.27bp,65.511bp)  .. (266.33bp,57.009bp);
+  \draw (186.0bp,89.5bp) node {$$8$$};
+  % Edge: 6 -> 2
+  \draw [->] (285.16bp,45.662bp) .. controls (293.01bp,41.945bp) and (304.56bp,36.472bp)  .. (323.68bp,27.417bp);
+  % Node: 1
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (11.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (11.0bp,50.0bp) node {$\lnot e_{0}$};
+\end{scope}
+  % Node: 5
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (97.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (97.0bp,50.0bp) node {$e_{1}$};
+\end{scope}
+  % Node: 2
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (334.0bp,23.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (334.0bp,23.0bp) node {$\bot$};
+\end{scope}
+  % Node: 3
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (186.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (186.0bp,50.0bp) node {$e_{2}$};
+\end{scope}
+  % Node: 6
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (275.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (275.0bp,50.0bp) node {$e_{3}$};
+\end{scope}
+  % Node: 4
+\begin{scope}
+  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+  \pgfsetstrokecolor{strokecol}
+  \draw (232.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
+  \draw (232.0bp,11.0bp) node {$\lnot e_{3}$};
+\end{scope}
+%
+\end{tikzpicture}
+
+
+}
+\begin{prooftree}
+	\AxiomC{$8. \; e_{0} \lor \lnot e_{1} \lor \lnot e_{2} \lor e_{3}$}
+	\AxiomC{$3. \; \lnot e_{1} \lor e_{2}$}
+	\BinaryInfC{$e_{0} \lor \lnot e_{1} \lor e_{3}$}
+	\AxiomC{$6. \; \lnot e_{3} \lor \lnot e_{1}$}
+	\BinaryInfC{$e_{0} \lor \lnot e_{1}$}
+	\AxiomC{$7. \; e_{0} \lor e_{1}$}
+	\BinaryInfC{$e_{0}$}
+\end{prooftree}
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{14|15|16|17|18}
+		\dpllDecL{0|0|0|0|0}
+		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{1}$|$e_{0}, e_{1}, e_{2}$|\makecell{$e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
+		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|\done|\done|\done|\done}
+		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
+		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
+		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
+		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|\done|\done|\done|\done}
+		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|\done|\done|\done|\done}
+		\dpllClause{9}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done}
+		\dpllBCP{$e_{0}$|$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
+		\dpllPL{ - | - | - | - | - }
+		\dpllDeci{ - | - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (a = b) \land (a = f(a)) \land (b = f(a)) \land (d \neq a) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{a, b\}, \{a, f(a)\}, \{b, f(a)\}, \{d\}\\
+	&\{d\}, \{a, b, f(a)\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3018.tex b/smt/3018.tex
new file mode 100644
index 0000000..9a1a2a9
--- /dev/null
+++ b/smt/3018.tex
@@ -0,0 +1,7 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+\varphi = & (\clause{(a=b); (a=f(a))}) \land (\clause{(f(a)=b); (c=b); (f(a)=c)})~\land \\
+           & (\clause{(f(b)=c); \lnot (f(a)=b); \lnot (f(a)=c)}) \land (\clause{\lnot (a=b); \lnot (a=f(a))})~\land \\
+           & (\clause{(a=f(a)); \lnot (c=b)})
+  \end{align*}
diff --git a/smt/3018_sol.tex b/smt/3018_sol.tex
new file mode 100644
index 0000000..a29845d
--- /dev/null
+++ b/smt/3018_sol.tex
@@ -0,0 +1,39 @@
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(a=b)$
+	\item $e_{1}\Leftrightarrow(a=f(a))$
+	\item $e_{2}\Leftrightarrow(f(a)=b)$
+	\item $e_{3}\Leftrightarrow(c=b)$
+	\item $e_{4}\Leftrightarrow(f(a)=c)$
+	\item $e_{5}\Leftrightarrow(f(b)=c)$
+\end{itemize}
+
+$\hat{\varphi} = (\clause{e_{0}; e_{1}}) \land (\clause{e_{2}; e_{3}; e_{4}}) \land (\clause{e_{5}; \lnot e_{2}; \lnot e_{4}}) \land (\clause{\lnot e_{0}; \lnot e_{1}}) \land (\clause{e_{1}; \lnot e_{3}}) $
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{6}
+		\dpllStep{1|2|3|4|5|6}
+		\dpllDecL{0|0|0|0|1|1}
+		\dpllAssi{ - |$e_{5}$|$e_{5}, e_{2}$|$e_{5}, e_{2}, \lnot e_{3}$|\makecell{$e_{5}, e_{2}, \lnot e_{3}, $ \\ $\lnot e_{0}$}|\makecell{$e_{5}, e_{2}, \lnot e_{3}, $ \\ $\lnot e_{0}, e_{1}$}}
+		\dpllClause{1}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{1}$|\done}
+		\dpllClause{2}{$e_{2}, e_{3}, e_{4}$}{$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|\done|\done|\done|\done}
+		\dpllClause{3}{$e_{5}, \lnot e_{2}, \lnot e_{4}$}{$e_{5}, \lnot e_{2}, \lnot e_{4}$|\done|\done|\done|\done|\done}
+		\dpllClause{4}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|\done|\done}
+		\dpllClause{5}{$e_{1}, \lnot e_{3}$}{$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|\done|\done|\done}
+		\dpllBCP{ - | - | - | - |$e_{1}$| - }
+		\dpllPL{$e_{5}$|$e_{2}$|$\lnot e_{3}$| - | - | - }
+		\dpllDeci{ - | - | - |$\lnot e_{0}$| - | - }
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (f(a) = b) \land (c \neq b) \land (f(b) = c) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{a, f(a)\}, \{f(a), b\}, \{f(b), c\}\\
+	&\{f(b), c\}, \{a, b, f(a)\}
+\end{align*}
+
+$\Model_{\EUF}$ is not consistent with the theory, because of: $(a \neq b) $\\
+$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
+$BC :=\neg e_{5} \lor \neg e_{2} \lor e_{3} \lor e_{0} \lor \neg e_{1}$\\
diff --git a/smt/3018_sol_second_part.tex b/smt/3018_sol_second_part.tex
new file mode 100644
index 0000000..ce93c12
--- /dev/null
+++ b/smt/3018_sol_second_part.tex
@@ -0,0 +1,26 @@
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{5}
+		\dpllStep{7|8|9|10|11}
+		\dpllDecL{0|1|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{3}$|\makecell{$\lnot e_{0}, e_{1}, e_{3}, $ \\ $\lnot e_{2}$}}
+		\dpllClause{1}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
+		\dpllClause{2}{$e_{2}, e_{3}, e_{4}$}{$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|\done|\done}
+		\dpllClause{3}{$e_{5}, \lnot e_{2}, \lnot e_{4}$}{$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|\done}
+		\dpllClause{4}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done|\done}
+		\dpllClause{5}{$e_{1}, \lnot e_{3}$}{$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|\done|\done|\done}
+		\dpllClause{6}{$\lnot e_{5}, \lnot e_{2}, e_{3}, e_{0}, \lnot e_{1}$}{\makecell{$\lnot e_{5}, \lnot e_{2}, e_{3}, $ \\ $e_{0}, \lnot e_{1}$}|\makecell{$\lnot e_{5}, \lnot e_{2}, e_{3}, $ \\ $\lnot e_{1}$}|$\lnot e_{5}, \lnot e_{2}, e_{3}$|\done|\done}
+		\dpllBCP{ - |$e_{1}$| - | - | - }
+		\dpllPL{ - | - |$e_{3}$|$\lnot e_{2}$| - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (f(a) \neq b) \land (c = b) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{a, f(a)\}, \{c, b\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/3019.tex b/smt/3019.tex
new file mode 100644
index 0000000..d3555b8
--- /dev/null
+++ b/smt/3019.tex
@@ -0,0 +1,7 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  \begin{align*}
+	\varphi = &(\clause{\lnot (y=f(x)); \lnot (y=f(y))}) \land (\clause{(y=f(x)); (y=f(y))})~\land\\
+	&(\clause{(f(x)=z); (f(y)=x); \lnot (f(y)=z)}) \land (\clause{(y=f(y)); \lnot (z=x)})~\land\\
+	&(\clause{(f(y)=x); (z=x); (f(y)=z)}) \land (\clause{(y=f(x)); (z=x)})
+  \end{align*}
diff --git a/smt/3019_sol.tex b/smt/3019_sol.tex
new file mode 100644
index 0000000..1d394a6
--- /dev/null
+++ b/smt/3019_sol.tex
@@ -0,0 +1,41 @@
+
+We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
+\begin{itemize}
+	\item $e_{0}\Leftrightarrow(y=f(x))$
+	\item $e_{1}\Leftrightarrow(y=f(y))$
+	\item $e_{2}\Leftrightarrow(f(x)=z)$
+	\item $e_{3}\Leftrightarrow(f(y)=x)$
+	\item $e_{4}\Leftrightarrow(f(y)=z)$
+	\item $e_{5}\Leftrightarrow(z=x)$
+\end{itemize}
+
+$\hat{\varphi} = (\clause{\lnot e_{0}; \lnot e_{1}}) \land (\clause{e_{0}; e_{1}}) \land (\clause{e_{2}; e_{3}; \lnot e_{4}}) \land (\clause{e_{1}; \lnot e_{5}}) \land (\clause{e_{3}; e_{5}; e_{4}}) \land (\clause{e_{0}; e_{5}})$
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{6}
+		\dpllStep{1|2|3|4|5|6}
+		\dpllDecL{0|0|0|1|1|1}
+		\dpllAssi{ - |$e_{2}$|$e_{2}, e_{3}$|$e_{2}, e_{3}, \lnot e_{0}$|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}$}|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}, e_{5}$}}
+		\dpllClause{1}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done}
+		\dpllClause{2}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{1}$|\done|\done}
+		\dpllClause{3}{$e_{2}, e_{3}, \lnot e_{4}$}{$e_{2}, e_{3}, \lnot e_{4}$|\done|\done|\done|\done|\done}
+		\dpllClause{4}{$e_{1}, \lnot e_{5}$}{$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|\done|\done}
+		\dpllClause{5}{$e_{3}, e_{5}, e_{4}$}{$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|\done|\done|\done|\done}
+		\dpllClause{6}{$e_{0}, e_{5}$}{$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{5}$|$e_{5}$|\done}
+		\dpllBCP{ - | - | - |$e_{1}$|$e_{5}$| - }
+		\dpllPL{$e_{2}$|$e_{3}$| - | - | - | - }
+		\dpllDeci{ - | - |$\lnot e_{0}$| - | - | - }
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (y \neq f(x)) \land (y = f(y)) \land (f(x) = z) \land (f(y) = x) \land (z = x) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{y, f(y)\}, \{f(x), z\}, \{f(y), x\}, \{z, x\}\\
+	&\{f(x), f(y), x, y, z\}
+\end{align*}
+
+$\Model_{\EUF}$ is not consistent with the theory, because of: $(y \neq f(x)) $\\
+$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
+$BC :=\neg e_{2} \lor \neg e_{3} \lor e_{0} \lor \neg e_{1} \lor \neg e_{5}$\\
diff --git a/smt/3019_sol_second_part.tex b/smt/3019_sol_second_part.tex
new file mode 100644
index 0000000..70e1a34
--- /dev/null
+++ b/smt/3019_sol_second_part.tex
@@ -0,0 +1,26 @@
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{6}
+		\dpllStep{7|8|9|10|11|12}
+		\dpllDecL{0|1|1|1|1|1}
+		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{5}$|\makecell{$\lnot e_{0}, e_{1}, e_{5}, $ \\ $\lnot e_{4}$}|\makecell{$\lnot e_{0}, e_{1}, e_{5}, $ \\ $\lnot e_{4}, \lnot e_{2}$}}
+		\dpllClause{1}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done|\done|\done}
+		\dpllClause{2}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done|\done}
+		\dpllClause{3}{$e_{2}, e_{3}, \lnot e_{4}$}{$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|\done|\done}
+		\dpllClause{4}{$e_{1}, \lnot e_{5}$}{$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|\done|\done|\done|\done}
+		\dpllClause{5}{$e_{3}, e_{5}, e_{4}$}{$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|\done|\done|\done}
+		\dpllClause{6}{$e_{0}, e_{5}$}{$e_{0}, e_{5}$|$e_{5}$|$e_{5}$|\done|\done|\done}
+		\dpllClause{7}{$\lnot e_{2}, \lnot e_{3}, e_{0}, \lnot e_{1}, \lnot e_{5}$}{\makecell{$\lnot e_{2}, \lnot e_{3}, e_{0}, $ \\ $\lnot e_{1}, \lnot e_{5}$}|\makecell{$\lnot e_{2}, \lnot e_{3}, \lnot e_{1}, $ \\ $\lnot e_{5}$}|$\lnot e_{2}, \lnot e_{3}, \lnot e_{5}$|$\lnot e_{2}, \lnot e_{3}$|$\lnot e_{2}, \lnot e_{3}$|\done}
+		\dpllBCP{ - |$e_{1}$|$e_{5}$| - | - | - }
+		\dpllPL{ - | - | - |$\lnot e_{4}$|$\lnot e_{2}$| - }
+		\dpllDeci{$\lnot e_{0}$| - | - | - | - |SAT}
+	\end{dplltabular}
+}
+
+$\Model_{\EUF} := (y \neq f(x)) \land (y = f(y)) \land (f(x) \neq z) \land (f(y) \neq z) \land (z = x) $ \\
+Check if the assignment is consistent with the theory:
+
+\begin{align*}
+	&\{y, f(y)\}, \{z, x\}, \{f(x)\}
+\end{align*}
+
+$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.
diff --git a/smt/smt.tex b/smt/smt.tex
index cf6e91d..275a72d 100644
--- a/smt/smt.tex
+++ b/smt/smt.tex
@@ -194,7 +194,46 @@
 \question{smt/3000.tex}
          {smt/3000_sol.tex}
          {3cm}
-\question{smt/3001.tex}
-         {smt/3001_sol.tex}
-         {3cm}
+\question{smt/3013.tex}
+         {smt/3013_sol.tex}
+         {3cm}
+          \ifsolution
+          \leavevmode \newline \vspace{1mm} \noindent \\
+          \widefbox{\input{smt/3013_sol_second_part.tex}}
+          \fi
+\question{smt/3014.tex}
+         {smt/3014_sol.tex}
+         {3cm}
+\question{smt/3015.tex}
+         {smt/3015_sol.tex}
+         {3cm}
+\question{smt/3016.tex}
+         {smt/3016_sol.tex}
+         {3cm}
+          \ifsolution
+          \leavevmode \newline \vspace{1mm} \noindent \\
+          \widefbox{\input{smt/3016_sol_second_part.tex}}
+          \fi
+
+\question{smt/3017.tex}
+         {smt/3017_sol.tex}
+         {3cm}
+          \ifsolution
+          \leavevmode \newline \vspace{1mm} \noindent \\
+          \widefbox{\input{smt/3017_sol_second_part.tex}}
+          \fi
+\question{smt/3018.tex}
+         {smt/3018_sol.tex}
+         {3cm}
+          \ifsolution
+          \leavevmode \newline \vspace{1mm} \noindent \\
+          \widefbox{\input{smt/3018_sol_second_part.tex}}
+          \fi
+\question{smt/3019.tex}
+         {smt/3019_sol.tex}
+         {3cm}
+          \ifsolution
+          \leavevmode \newline \vspace{1mm} \noindent \\
+          \widefbox{\input{smt/3019_sol_second_part.tex}}
+          \fi
 \end{questionSection}
diff --git a/util/math_macros.tex b/util/math_macros.tex
index 0503b47..19568c3 100644
--- a/util/math_macros.tex
+++ b/util/math_macros.tex
@@ -137,6 +137,16 @@
   \def\CLAUSE{#2}%
   Cl. \ITEM: \CLAUSE & \dpllrow{#3}
 }
+\newcommand{\learnedClause}[3]{
+  \def\ITEM{#1}%
+  \def\CLAUSE{#2}%
+  Cl. \ITEM: \CLAUSE & \dpllrow{#3}
+}
+\newcommand{\blockingClause}[3]{
+  \def\ITEM{#1}%
+  \def\CLAUSE{#2}%
+  Blocking Cl. \ITEM: \CLAUSE & \dpllrow{#3}
+}
 
 \ExplSyntaxOn
 \NewDocumentCommand{\clause}{m}