diff --git a/natural_deduction_predicate_logic/1004_sol.tex b/natural_deduction_predicate_logic/1004_sol.tex
index 28ca00c..ae6604f 100644
--- a/natural_deduction_predicate_logic/1004_sol.tex
+++ b/natural_deduction_predicate_logic/1004_sol.tex
@@ -1,18 +1,15 @@
+This sequent is not provable.
 
-\begin{logicproof}{2}
-  \exists x \; (Q(x) \imp R(x))                   &\prem \\
-  \exists x \; (P(x)\land Q(x))                   &\prem \\
-  \begin{subproof}
-    Q(x_0) \imp R(x_0)              &\assum~\freshVar{$x_0$} \\
-    \begin{subproof}
-      P(x_0) \land Q(x_0)             &\assum~\freshVar{$x_0$}\\
-      P(x_0)                          &\ande{1} 4\\
-      Q(x_0)                          &\ande{2} 4\\
-      R(x_0)                          &\impe 5,3\\
-      P(x_0) \land R(x_0) & \andi 5,7\\
-      \exists x (P(x) \land R(x)) & \existi 8
-    \end{subproof}
-    \exists x \; (P(x) \land R(x)) & \existe 2,4-9
-  \end{subproof}
-  \exists x \; (P(x) \land R(x)) & \existe 1,3-10
-\end{logicproof}
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ a, b \}\\
+  P^\mathcal{M} =& \; \{ a\} \\
+  Q^\mathcal{M} =& \; \{ a\} \\
+  R^\mathcal{M} =& \; \{ \}
+  \end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \exists x (Q(x) \imp R(x))$\\
+$\mathcal{M} \models \exists x (P(x) \land Q(x))$\\
+$\mathcal{M} \nmodels \exists x (P(x) \land R(x))$