diff --git a/aspUnify.tex b/aspUnify.tex
index 330ceef..4c6acfb 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -64,50 +64,43 @@ In this paper we translate the type inference algorithm for Featherweight Generi
 Answer Set Program.
 Answer Set Programming (ASP) promises to solve complex computational search problems
 as long as they are finite domain.
-This paper shows that it is possible to implement global type inference for FGJ as an ASP program.
+This paper shows that it is possible to implement global type inference for Featherweight Generic Java (FGJ) as an ASP program.
+Afterwards we compared the ASP implementation with our own implementation in Java
+exposing promising results.
 % We also show soundness, completeness and termination for our ASP implementation.
 Another advantage is that the specification of the algorithm can be translated one on one to ASP code
 leading to less errors in the respective implementation.
+Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types.
 %TODO: Is this correct?
 \end{abstract}
 %
 %
 %
-\section{Type Inference}
-Every major typed programming language uses some form of type inference.
-Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
-Type inference adds alot of value to a programming language.
-\begin{itemize}
-\item Code is more readable.
-\item Type inference usually does a better job at finding types than a programmer.
-\item Type inference can use types that are not denotable by the programmer.
-\item Better reusability.
-\item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
-\end{itemize}
+\section{Global Type Inference}
+% Every major typed programming language uses some form of type inference.
+% Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
+% Type inference adds alot of value to a programming language.
+% \begin{itemize}
+% \item Code is more readable.
+% \item Type inference usually does a better job at finding types than a programmer.
+% \item Type inference can use types that are not denotable by the programmer.
+% \item Better reusability.
+% \item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
+% \end{itemize}
 
-Java has adopted more and more type inference features over time.
-%TODO: list type inference additions
-Currently Java only has local type inference.
-We want to bring type inference for Java to the next level.
+% Java has adopted more and more type inference features over time.
+% %TODO: list type inference additions
+% Currently Java only has local type inference.
+% We want to bring type inference for Java to the next level.
 
-Our type inference algorithms for Java are described in a formal manner in
-\cite{MartinUnify}, \cite{TIforGFJ}.
-The first prototype implementation put the focus on a correct implementation rather than
-fast execution times.
-These programs tend to be in exponential time upper bounded by the amount of ambiguous method calls and subtype relations.
-%TODO: Example with multiple calls to m.toString(). All possibilities are checked in a naive implementation!
+Java is a strictly typed programming language.
+The current versions come with a local type inference feature that allows the programmer to omit
+type annotations in some places like argument types of lambda expressions for example.
+But methods still have to be fully typed including argument and return types.
+We work at a global type inference algorithm for Java which is able to compute correct types
+for a Java program with no type annotations at all.
 
-\section{Motivation}
-The nature of the global type inference algorithm causes the search space of the unification algorithm to
-increase exponentially.
-Java allows overloaded methods causing our type inference algorithm to create so called Or-Constraints.
-This can also happen if multiple classes implement a method with the same name and the same amount of parameters.
-Given the following input program we do not know, which method \texttt{self} is meant for the method call
-\texttt{var.self()}, because there is no type annotation for \texttt{var}.
-
-
-%\begin{figure}[h]
-%\begin{minipage}{0.49\textwidth}
+\begin{figure}[h]
 \begin{lstlisting}
 class C1 {
     C1 self(){
@@ -121,10 +114,45 @@ class C2 {
 }
 class Example {
     untypedMethod(var){
-        return var.self();      (*@$\implies \set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$@*)
+        return var.self();   //  (*@$\implies \set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$@*)
     }
 }
 \end{lstlisting}
+\caption{Java program missing type annotations}\label{fig:introExample}
+\end{figure}
+
+A possible input for our algorithm is shonw in figure \ref{fig:introExample}.
+Here the method \texttt{untypedMethod} is missing its argument type for \texttt{var} and its return type.
+Global type inference works in two steps.
+First we generate a set of subtype constraints, which are later unified resulting in a type solution consisting of type unifiers $\sigma$.
+Every missing type is replaced by a type placeholder.
+In this example the type placeholder $\tv{var}$ is a placeholder for the type of the \texttt{var} variable.
+The $\tv{ret}$ placeholder represents the return type of the \texttt{untypedMethod} method.
+Also shown as a comment behind the respective method call.
+There are two types of type constraints.
+A subtype constraint like $\tv{var} \lessdot \type{C1}$ meaning that the unification algorithm has to find
+a type replacement for $\tv{var}$ which is a subtype of $\type{C1}$.
+Due to the Java type system being reflexive one possible solution would be $\sigma(\tv{var}) = \type{C1}$.
+A constraint $\tv{var} \doteq \type{C1}$ directly results in $\sigma(\tv{ret}) = \type{C1}$.
+
+Our type inference algorithms for Java are described in a formal manner in
+\cite{MartinUnify}, \cite{TIforGFJ}.
+The first prototype implementation put the focus on a correct implementation rather than
+fast execution times.
+Depending on the input it currently takes upto several minutes or even days to compute all or even one possible type solution.
+To make them usable in practice we now focus on decreasing the runtime to a feasible level.
+
+\section{Motivation}
+The nature of the global type inference algorithm causes the search space of the unification algorithm to
+increase exponentially with every ambiguous method call.
+Java allows overloaded methods causing our type inference algorithm to create so called Or-Constraints.
+This happens if multiple classes implement a method with the same name and the same amount of parameters.
+Given the input program in figure \ref{fig:introExample} we do not know, which method \texttt{self} is meant for the method call
+\texttt{var.self()}, because there is no type annotation for \texttt{var}.
+
+
+%\begin{figure}[h]
+%\begin{minipage}{0.49\textwidth}
 %     \end{minipage}%
 %     \hfill
 %     \begin{minipage}{0.49\textwidth}
@@ -138,8 +166,6 @@ class Example {
 An Or-Constraint like $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$
 means that either the the constraint set $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }$
 or $\set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$ has to be satisfied.
-In this example the type placeholder $\tv{var}$ is a placeholder for the type of the \texttt{var} variable.
-The $\tv{ret}$ placeholder represents the return type of the \texttt{untypedMethod} method.
 If we set the type of \texttt{var} to \texttt{C1}, then the return type of the method will be \texttt{C1} aswell.
 If we set it to \texttt{C2} then also the return type will be \texttt{C2}.
 There are two possibilities therefore the Or-Constraint.
@@ -149,11 +175,14 @@ The type unification algorithm \unify{} only sees the supplied constraints and h
 This is proven in \cite{TIforGFJ} and is the reason why type inference for Featherweight Generic Java is NP-hard.
 Let's have a look at the following alternation of our example:
 
+\begin{figure}[h]
 \begin{lstlisting}
     untypedMethod(var){
         return var.self().self().self().self();
     }
 \end{lstlisting}
+\caption{Stacked ambiguous method calls}\label{fig:benchmark}
+\end{figure}
 
 Now there are four chained method calls leading to four Or-Constraints:
 \begin{align*}
@@ -184,8 +213,29 @@ Answer Set programming promises to solve complex search problems in a highly opt
 The idea in this paper is to implement the algorithm presented in \cite{TIforGFJ}
 as an ASP program and see how well it handles our type unification problem.
 
+\section{ASP Implementation}
 
-\section{Subtyping}
+Our ASP implementation replaces the unification step of the type inference algorithm.
+So the input is a set of constraints $c$ and the output is a set of unifiers $\sigma$.
+An ASP program consists of implication rules and facts.
+Here the facts are the input constraints and the rules are the ones depicted in chapter \ref{sec:implicationRules}.
+After running the resulting program through an interpreter the output
+holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
+
+\begin{figure}[h]
+  \center
+\begin{tabular}{lcll}
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
+    $\type{T} $ & $::=$ & $\tv{a} \mid \type{N}$ & Type placeholder or Type \\
+    $\ntype{N}$ & $::=$ & $\exptype{C}{\ol{T}}$ & Class Type containing type placeholders\\
+    $\gtype{G}$ & $::=$ & $\exptype{C}{\ol{G}}$ & Class Type not containing type placeholders \\
+\end{tabular}
+  \caption{Syntax of types and constraints}
+  \label{fig:syntax-constraints}
+\end{figure}
+
+%\subsection{Subtyping}
+\begin{figure}[h]
 \begin{mathpar}
 \inferrule[S-Refl]{}{
 \type{T} <: \type{T}
@@ -201,7 +251,6 @@ as an ASP program and see how well it handles our type unification problem.
 \exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
 }
 \end{mathpar}
-
 \begin{mathpar}
 \inferrule[N-Refl]{}{
 \type{C} << \type{C}
@@ -215,19 +264,21 @@ as an ASP program and see how well it handles our type unification problem.
 \type{C} << \type{D}
 }
 \end{mathpar}
+\caption{Subtyping}\label{fig:subtyping}
+\end{figure}
+
 
 %Subtyping has no bounds for generic type parameters.
 % but this is propably not needed
 
-\section{Unify}
-Input: Every type placeholder must have an upper bound.
-Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a 
+\subsection{Unification Algorithm}\label{sec:implicationRules}
 
 The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
 The need to have an upper bound to every type placeholder.
 
-We have to formulate the unification algorithm with implication rules.
-Those can be directly translated to ASP.
+All the implication rules depicted in this chapter can be translated to ASP statements
+described in chapter \ref{sec:translation}.
+
 \label{sec:implicationRules}
 \begin{mathpar}
 \inferrule[Subst-L]{
@@ -432,16 +483,18 @@ Fail:
 
 The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
 
-\section{ASP Encoding}
-The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program.
-
-\begin{tabular}{l | r}
-    $\tv{a}$ & \texttt{tph("a")}\\
-    $\exptype{C}{}$ & \texttt{type("C", null)}\\
-    $\exptype{C}{\ol{X}}$ & \texttt{type("C", params(\ldots))}\\
-
-\end{tabular}
+\section{ASP Encoding}\label{sec:translation}
 \newcommand{\aspify}{\nabla}
+The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program
+(see figure \ref{fig:aspTransformationRules}).
+
+% \begin{tabular}{l | r}
+%     $\tv{a}$ & \texttt{tph("a")}\\
+%     $\exptype{C}{}$ & \texttt{type("C", null)}\\
+%     $\exptype{C}{\ol{X}}$ & \texttt{type("C", params(\ldots))}\\
+% \end{tabular}
+
+\begin{figure}[h]
 \begin{align*}
    \aspify(\tv{a}) =& \texttt{tph("a")}\\
    \exptype{C}{} =& \texttt{type("C", null)}\\
@@ -454,186 +507,207 @@ The implication rules defined in chapter \ref{sec:implicationRules} can be trans
     c
 }\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2)
 \end{align*}
+\caption{Transformation to ASP code}\label{fig:aspTransformationRules}
+\end{figure}
 
-The S-Class rule contains a substitution and has to be encoded with variables.
+%The $\aspify{}$ function converts our formal specification of the algorithm to ASP code.
+
+This also has to be done for the subtype rules in figure \ref{fig:subtyping}.
+There the S-Class rule needs special handling because it contains a substitution.
+It has to be encoded using variables.
 Given a extends relation $\texttt{class}\ \exptype{C}{\type{X}} \triangleleft \exptype{D}{\type{X}}$
 we generate the ASP code:\\
 {\small{\texttt{subtype(type("C", params(X)), type("D", params(X))) :- subtype(type("C", params(X))).}}}
 
 Capital letters like \texttt{X} are variables in ASP and the former statement causes any
-literal like \texttt{subtype(type("C", params(tph("a"))))} leads to the literal
+literal like \texttt{subtype(type("C", params(tph("a"))))} to imply the literal
 \texttt{subtype(type("C", params(tph("a"))), type("D", params(tph("a"))))}.
 
 
-\section{Proofs}
-\begin{lemma}{Substitution:}
-For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
-there also exists a constraint $[\type{T}/\tv{a}]c$.
+% \section{Proofs}
+% \begin{lemma}{Substitution:}
+% For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
+% there also exists a constraint $[\type{T}/\tv{a}]c$.
 
-\noindent
-\normalfont
-This lemma proofs that equal constraints lead to a substitution in every other constraint.
-For exmaple $\tv{b} \doteq \type{String}$ and $\tv{b} \lessdot \exptype{Comparable}{\tv{b}}$
-lead to a constraint $\type{String} \lessdot \exptype{Comparable}{\type{String}}$
-\end{lemma}
-\textit{Proof:}
-%TODO
+% \noindent
+% \normalfont
+% This lemma proofs that equal constraints lead to a substitution in every other constraint.
+% For exmaple $\tv{b} \doteq \type{String}$ and $\tv{b} \lessdot \exptype{Comparable}{\tv{b}}$
+% lead to a constraint $\type{String} \lessdot \exptype{Comparable}{\type{String}}$
+% \end{lemma}
+% \textit{Proof:}
+% %TODO
 
-\section{Termination}
+% \section{Termination}
 
-The amount of different constraints is limited by the maximum amount of encapsulated generics.
-The only part that is able to add an additional nesting is the Subst-Param rule.
-Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
-another layer of nesting but it also removes one type placeholder.
+% The amount of different constraints is limited by the maximum amount of encapsulated generics.
+% The only part that is able to add an additional nesting is the Subst-Param rule.
+% Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
+% another layer of nesting but it also removes one type placeholder.
 
-There must be one substitution that does not add another type placeholder.
-Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
+% There must be one substitution that does not add another type placeholder.
+% Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
 
-The Subst-Param rule can only be applied a finite number of times.
-Due to the substitution lemma and the Sigma-Fail rule the Subst-Param rule can only be applied once per type placeholder.
+% The Subst-Param rule can only be applied a finite number of times.
+% Due to the substitution lemma and the Sigma-Fail rule the Subst-Param rule can only be applied once per type placeholder.
 
-The Subst-Param rule can only be applied once per type placeholder.
-If $\type{T} \doteq \exptype{C}{\tv{a}}$ is substituted to $\type{T} \doteq \exptype{C}{\type{N}}$
-then there is no $\tv{a} \in \type{N}$.
+% The Subst-Param rule can only be applied once per type placeholder.
+% If $\type{T} \doteq \exptype{C}{\tv{a}}$ is substituted to $\type{T} \doteq \exptype{C}{\type{N}}$
+% then there is no $\tv{a} \in \type{N}$.
 
-\section{Completeness}
-To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
+% \section{Completeness}
+% To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
 
-Completeness -> we never exclude a solution
-Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
-Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
-Proof:
-%Induction over every possible constraint variation:
-a =. T -> induction start
-a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
-in latter case: a <. T, a <. T'
+% Completeness -> we never exclude a solution
+% Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
+% Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
+% Proof:
+% %Induction over every possible constraint variation:
+% a =. T -> induction start
+% a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
+% in latter case: a <. T, a <. T'
 
-Proof that every type can be replaced by a Type Placeholder.
-% Whats with a =. T, can T be replaced by a Type Placeholder?
-% What is our finish condition? a <. T constraints stay, a =. b constraints stay.
-% Algorithm does not fail -> \emptyset if a solution exists
-% Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
-% by: a <. T -> a =.T
-%     a =. b, b =. T -> use the solution generation from other paper
-% TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
+% Proof that every type can be replaced by a Type Placeholder.
+% % Whats with a =. T, can T be replaced by a Type Placeholder?
+% % What is our finish condition? a <. T constraints stay, a =. b constraints stay.
+% % Algorithm does not fail -> \emptyset if a solution exists
+% % Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
+% % by: a <. T -> a =.T
+% %     a =. b, b =. T -> use the solution generation from other paper
+% % TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
 
-Soundness -> we never make a wrong implication
-%$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
-If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
-constraints in the original constraint set and
-there exists a typing for the remaining type placeholders 
-so that the constraint set is satisfied.
+% Soundness -> we never make a wrong implication
+% %$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
+% If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
+% constraints in the original constraint set and
+% there exists a typing for the remaining type placeholders 
+% so that the constraint set is satisfied.
 
-\begin{theorem}{Soundness}\label{lemma:soundness}
-if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
-then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
-\end{theorem}
+% \begin{theorem}{Soundness}\label{lemma:soundness}
+% if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
+% then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
+% \end{theorem}
 
-\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
-\newcommand*\ncasesmakelabel[1]{Case #1}
+% \SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
+% \newcommand*\ncasesmakelabel[1]{Case #1}
 
-\newenvironment{subproof}
-  {\def\proofname{Subproof}%
-   \def\qedsymbol{$\triangleleft$}%
-   \proof}
-  {\endproof}
-Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
-\begin{proof}
-  \begin{enumerate}[ncases]
-    \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
-        Solution-Sub
-    Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
-    \item $\tv{a} \doteq \type{N}$.
-    Solution
-    \item $\tv{a} \lessdot \tv{b}$.
-    There must be a $\tv{a} \lessdot \type{N}$
-    \begin{subproof}
-    $\sigma(\tv{a}) = \type{Object}$, 
-    $\sigma(\tv{b}) = \type{Object}$.
-    \end{subproof}
-    \item $\type{N} \lessdot \tv{a}$.
-    \begin{subproof}
-    $2$
-    \end{subproof}
-  \end{enumerate}
-  And more text.
-\end{proof}
+% \newenvironment{subproof}
+%   {\def\proofname{Subproof}%
+%    \def\qedsymbol{$\triangleleft$}%
+%    \proof}
+%   {\endproof}
+% Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
+% \begin{proof}
+%   \begin{enumerate}[ncases]
+%     \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
+%         Solution-Sub
+%     Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
+%     \item $\tv{a} \doteq \type{N}$.
+%     Solution
+%     \item $\tv{a} \lessdot \tv{b}$.
+%     There must be a $\tv{a} \lessdot \type{N}$
+%     \begin{subproof}
+%     $\sigma(\tv{a}) = \type{Object}$, 
+%     $\sigma(\tv{b}) = \type{Object}$.
+%     \end{subproof}
+%     \item $\type{N} \lessdot \tv{a}$.
+%     \begin{subproof}
+%     $2$
+%     \end{subproof}
+%   \end{enumerate}
+%   And more text.
+% \end{proof}
 
-\begin{lemma}{Substitution}
-    \begin{description}
-        \item[If] $\tv{a} \doteq \type{N}$ with $\tv{a} \neq \type{N}$
-        \item[Then] for every $\type{T} \doteq \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \doteq [\type{N}/\tv{a}]\type{T}$
-        \item[Then] for every $\type{T} \lessdot \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \lessdot [\type{N}/\tv{a}]\type{T}$
-    \end{description}
-\end{lemma}
-\textit{Proof:}
-TODO
+% \begin{lemma}{Substitution}
+%     \begin{description}
+%         \item[If] $\tv{a} \doteq \type{N}$ with $\tv{a} \neq \type{N}$
+%         \item[Then] for every $\type{T} \doteq \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \doteq [\type{N}/\tv{a}]\type{T}$
+%         \item[Then] for every $\type{T} \lessdot \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \lessdot [\type{N}/\tv{a}]\type{T}$
+%     \end{description}
+% \end{lemma}
+% \textit{Proof:}
+% TODO
 
-\begin{lemma} \label{lemma:subtypeOnly}
-If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
-\end{lemma}
-Proof:
-Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
-Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
+% \begin{lemma} \label{lemma:subtypeOnly}
+% If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
+% \end{lemma}
+% Proof:
+% Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
+% Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
 
-The Solution-Sub rule is always correct.
+% The Solution-Sub rule is always correct.
 
-Proof:
+% Proof:
 
-\begin{theorem}{Termination}
-    %jede nichtendliche Menge von Constraints bleibt endlich. Die Regeln können nicht unendlich oft angewendet werden
-%Trivial. The only possibility would be if we allow a =. C<a> constraints!
-\end{theorem}
+% \begin{theorem}{Termination}
+%     %jede nichtendliche Menge von Constraints bleibt endlich. Die Regeln können nicht unendlich oft angewendet werden
+% %Trivial. The only possibility would be if we allow a =. C<a> constraints!
+% \end{theorem}
 
-TODO: For completeness we have to proof that not $\tv{a} \doteq \type{N}$ only is the case if $\tv{a}$ only appears on the left side of $\tv{a} \lessdot \type{T}$ constraints.
-Problem: a <. List<a>
-        a <. List<b>
-        then a =. b
-Solution: Keep the a <. N constraints and apply the Step 6 from the GTFGJ paper.
-Then we have to proof that only a <. N constraints remain with sigma(a) = empty. Or Fail
+% TODO: For completeness we have to proof that not $\tv{a} \doteq \type{N}$ only is the case if $\tv{a}$ only appears on the left side of $\tv{a} \lessdot \type{T}$ constraints.
+% Problem: a <. List<a>
+%         a <. List<b>
+%         then a =. b
+% Solution: Keep the a <. N constraints and apply the Step 6 from the GTFGJ paper.
+% Then we have to proof that only a <. N constraints remain with sigma(a) = empty. Or Fail
 
-\begin{theorem}{Completeness}
-$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
-and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
-\end{theorem}
-%Problem: We do not support multiple inheritance
-\begin{proof}
-  \begin{enumerate}[ncases]
-    \item $\tv{a} \lessdot \type{N}$.
-        Solution-Sub
-    \item $\tv{a} \doteq \type{N}$.
-    Solution
-    \item $\tv{a} \lessdot \tv{b}$.
-    There must be a $\tv{a} \lessdot \type{N}$
-    \begin{subproof}
-    $\sigma(\tv{a}) = \type{Object}$, 
-    $\sigma(\tv{b}) = \type{Object}$.
-    \end{subproof}
-    \item $\type{N} \lessdot \tv{a}$.
-    \begin{subproof}
-    $2$
-    \end{subproof}
-  \end{enumerate}
-  And more text.
-\end{proof}
+% \begin{theorem}{Completeness}
+% $\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
+% and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
+% \end{theorem}
+% %Problem: We do not support multiple inheritance
+% \begin{proof}
+%   \begin{enumerate}[ncases]
+%     \item $\tv{a} \lessdot \type{N}$.
+%         Solution-Sub
+%     \item $\tv{a} \doteq \type{N}$.
+%     Solution
+%     \item $\tv{a} \lessdot \tv{b}$.
+%     There must be a $\tv{a} \lessdot \type{N}$
+%     \begin{subproof}
+%     $\sigma(\tv{a}) = \type{Object}$, 
+%     $\sigma(\tv{b}) = \type{Object}$.
+%     \end{subproof}
+%     \item $\type{N} \lessdot \tv{a}$.
+%     \begin{subproof}
+%     $2$
+%     \end{subproof}
+%   \end{enumerate}
+%   And more text.
+% \end{proof}
 
 
-\section{Discussion}
+%\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.
+We tested our ASP implementation of the unification algorithm with the constraints originating from the program in
+figure \ref{fig:benchmark}.
+We compared it with the current implementation of the Unification algorithm in Java
+\footnote{\url{https://gitea.hb.dhbw-stuttgart.de/JavaTX/JavaCompilerCore}}.
+We increased the complexity by adding more stacked method calls up to ten stacked calls and the interpreter clingo \footnote{\url{https://potassco.org/clingo/}}
+was still able to handle it easily and finish computation in under 50 milliseconds.
+By contrast our Java implementation already takes multiple seconds processing time for the same input.
 
-\section{Future Work}
+We are using this example for a fair comparision between the two implementations because it does not include generic type parameters causing the unification algorithm
+not to consider wildcard types.
+The Java implementation also supports Java wildcard types whereas the ASP implementation does not.
+%It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
+It is unfortunately not possible to implement the unification algorithm including wildcard support with Answer Set Programming.
+The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
+The grounding process of the ASP interpreter clingo would not terminate if the problem is turing complete
+\cite{kaufmann2016grounding}.
+The Java implementation is still able to spawn atleast one solution in most cases and only never terminates for specific inputs,
+whereas the ASP program never terminates as soon as wildcards are involved.
+
+
+%\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