diff --git a/aspUnify.tex b/aspUnify.tex
index 6b9892e..330ceef 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -187,17 +187,17 @@ as an ASP program and see how well it handles our type unification problem.
 
 \section{Subtyping}
 \begin{mathpar}
-\inferrule[Refl]{}{
+\inferrule[S-Refl]{}{
 \type{T} <: \type{T}
 }
 \and
-\inferrule[Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
+\inferrule[S-Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
 \type{T}_1 <: \type{T}_3
 }
 \and
-\inferrule[Var]{}{\type{A} <: \Delta(\type{A})}
+\inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
 \and
-\inferrule[Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
+\inferrule[S-Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
 \exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
 }
 \end{mathpar}
@@ -617,6 +617,27 @@ and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
   And more text.
 \end{proof}
 
+
+\section{Discussion}
+% We cannot use Datalog, because it cannot solve NP-Hard problems.
+% See: E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov. Complexity and Expressive Power of Logic Programming.
+% ACM Computing Surveys, 33(3):374–425, 2001. Available at
+% http://www.kr.tuwien.ac.at/staff/eiter/et-archive/
+% Source: https://www.cs.ox.ac.uk/files/1018/gglecture7.pdf
+
+It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
+The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
+It is not possible to implement a type inference algorithm for Java in ASP, because the grounding process will not terminate
+\cite{kaufmann2016grounding}.
+
+\section{Outcome and Conclusion}
+ASP handles Or-Constraints surprisingly well.
+
+\section{Future Work}
+% Benchmarks
+% Integrating the ASP Unify implementation into existing Java-TX Compiler
+% Checking how many programs are abel to be build without wildcards
+
 \bibliographystyle{eptcs}
 \bibliography{martin}