diff --git a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
index 80dabce6..1c75ea99 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
@@ -50,12 +50,6 @@ public class MartelliMontanariUnify implements IUnify {
 			TypeParams rhsTypeParams = rhsType.getTypeParams();
 			TypeParams lhsTypeParams = lhsType.getTypeParams();
 			
-			// DELETE - Rule
-			if(pair.getRhsType().equals(pair.getLhsType())) {
-				termsList.remove(idx);
-				continue; 
-			}
-			
 			// REDUCE - Rule
 			if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
 				Set<UnifyPair> result = new HashSet<>();
@@ -78,6 +72,12 @@ public class MartelliMontanariUnify implements IUnify {
 				termsList.addAll(result);
 				continue;
 			}
+			
+			// DELETE - Rule
+			if(pair.getRhsType().equals(pair.getLhsType())) {
+				termsList.remove(idx);
+				continue; 
+			}
 
 			// SWAP - Rule
 			if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
index 805d461c..2e0d70fd 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
@@ -3,6 +3,7 @@ package de.dhbwstuttgart.typeinference.unify;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.LinkedHashSet;
 import java.util.LinkedList;
@@ -10,6 +11,7 @@ import java.util.List;
 import java.util.Map.Entry;
 import java.util.Optional;
 import java.util.Set;
+import java.util.function.Function;
 import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
@@ -47,6 +49,8 @@ public class TypeUnify {
 	 */
 	protected IRuleSet rules = new RuleSet();
 	
+	protected boolean parallel = true;
+	
 	/**
 	 * Computes all principal type unifiers for a set of constraints.
 	 * @param eq The set of constraints
@@ -58,7 +62,7 @@ public class TypeUnify {
 		 * Step 1: Repeated application of reduce, adapt, erase, swap 
 		 */
 		Set<UnifyPair> eq0 = applyTypeUnificationRules(eq, fc);
-		
+		 
 		/*
 		 * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs
 		 */
@@ -110,7 +114,7 @@ public class TypeUnify {
 		
 		// Sub cartesian products of the second level (pattern matched) sets
 		// "the big (x)"
-		// TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich
+		// TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich (scheint sich nicht zu lohnen)
 		for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
 			List<Set<Set<UnifyPair>>> secondLevelSetList = new ArrayList<>(secondLevelSet);
 			Set<List<Set<UnifyPair>>> cartResult = setOps.cartesianProduct(secondLevelSetList);
@@ -133,7 +137,7 @@ public class TypeUnify {
 		//System.out.println(result);
 
 		// Flatten the cartesian product
-		// TODO parallelisierung möglich
+		// TODO parallelisierung möglich (scheint sich nicht zu lohnen)
 		Set<Set<UnifyPair>> eqPrimeSetFlat = new HashSet<>();
 		for(Set<Set<UnifyPair>> setToFlatten : eqPrimeSet) {
 			Set<UnifyPair> buffer = new HashSet<>();
@@ -148,15 +152,33 @@ public class TypeUnify {
 		Set<Set<UnifyPair>> restartSet = new HashSet<>();
 		Set<Set<UnifyPair>> eqPrimePrimeSet = new HashSet<>();
 		
-		for(Set<UnifyPair> eqPrime : eqPrimeSetFlat) {
-			Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
+		
+		if(parallel) {
+	        Set<Set<UnifyPair>> restartSetSync = Collections.synchronizedSet(restartSet);
+	        Set<Set<UnifyPair>> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet);
 			
-			if (eqPrime.equals(eq))
-				eqPrimePrimeSet.add(eqPrime);
-			else if(eqPrimePrime.isPresent())
-				restartSet.add(eqPrimePrime.get());
-			else
-				restartSet.add(eqPrime);
+	        eqPrimeSetFlat.parallelStream().forEach(eqPrime -> {
+				Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
+				
+				if (eqPrime.equals(eq))
+					eqPrimePrimeSetSync.add(eqPrime);
+				else if(eqPrimePrime.isPresent())
+					restartSetSync.add(eqPrimePrime.get());
+				else
+					restartSetSync.add(eqPrime);
+			});
+		}
+		else {
+			for(Set<UnifyPair> eqPrime : eqPrimeSetFlat) {
+				Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
+				
+				if (eqPrime.equals(eq))
+					eqPrimePrimeSet.add(eqPrime);
+				else if(eqPrimePrime.isPresent())
+					restartSet.add(eqPrimePrime.get());
+				else
+					restartSet.add(eqPrime);
+			}
 		}
 
 		/*
@@ -164,10 +186,16 @@ public class TypeUnify {
 		 * 		  b) Build the union over everything
 		 */
 		// TODO parallelisierung möglich (lohnt sich vermutlich)
-		for(Set<UnifyPair> eqss : restartSet)
-			eqPrimePrimeSet.addAll(this.unify(eqss, fc));
-		/*restartSet.parallelStream().forEach( 
-				x -> eqPrimePrimeSet.addAll(unify(x, fc)));*/
+		
+		if(parallel) {
+	        Set<Set<UnifyPair>> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet);
+			restartSet.parallelStream().forEach( x -> eqPrimePrimeSetSync.addAll(unify(x, fc)));
+		} 
+		else {
+			for(Set<UnifyPair> eqss : restartSet)
+				eqPrimePrimeSet.addAll(this.unify(eqss, fc));
+		}
+
 		 /*
 		  * Step 7: Filter empty sets;
 		  */
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
index 17fbb240..ac0862cc 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
@@ -106,10 +106,10 @@ public class FiniteClosure implements IFiniteClosure {
 	    
 	    // Permute all params with values that are in smArg() of that type.
 	    // This corresponds to Case 3 in the definition of the subtyping relation.
-		{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+		/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
 		for (UnifyType param : type.getTypeParams())
 				paramCandidates.add(smArg(param));
-		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}
+		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
 		
 		// This is case 2 of the definition of the subtyping relation.
 		Set<UnifyType> result2 = new HashSet<>();
@@ -117,23 +117,24 @@ public class FiniteClosure implements IFiniteClosure {
 			HashSet<UnifyType> candidates = new HashSet<>();
 			// All types with the same name
 			strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
-			for(UnifyType typePrime : result1) {
-				for (UnifyType theta2 : candidates) {
-					// Find the substitution
-					Optional<Unifier> sigma2Opt = unify.unify(typePrime, theta2);
-					if (!sigma2Opt.isPresent())
-						continue;
-					Unifier sigma2 = sigma2Opt.get();
-					sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams());
-					if(type.equals(theta2))
-						continue;
-					Set<UnifyType> theta1s = smaller(theta2);
-					for (UnifyType theta1 : theta1s) {
-						// Because only the most general type is calculated, sigma1 = sigma2
-						UnifyType sigma1Theta1 = sigma2.apply(theta1);
-						result2.add(sigma1Theta1);
-					}
-				}
+			//for(UnifyType typePrime : result1) {
+			for (UnifyType theta2 : candidates) {
+				// Find the substitution
+				Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
+				if (!sigma2Opt.isPresent())
+					continue;
+				Unifier sigma2 = sigma2Opt.get();
+				if(sigma2.size() == 0)
+					continue;
+				sigma2.swapPlaceholderSubstitutions(type.getTypeParams());
+				//if(type.equals(theta2))
+				//	continue;
+				Set<UnifyType> theta1s = smaller(theta2);
+				for (UnifyType theta1 : theta1s) {
+					// Because only the most general type is calculated, sigma1 = sigma2
+					UnifyType sigma1Theta1 = sigma2.apply(theta1);
+					result2.add(sigma1Theta1);	
+			     }
 			}
 		}
 		else
@@ -210,10 +211,10 @@ public class FiniteClosure implements IFiniteClosure {
 	    
 	    // Permute all params with values that are in smArg() of that type.
 	    // This corresponds to Case 3 in the definition of the subtyping relation.
-		{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+		/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
 		for (UnifyType param : type.getTypeParams())
 				paramCandidates.add(grArg(param));
-		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}
+		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
 		
 		// This is case 2 of the definition of the subtyping relation.
 		Set<UnifyType> result2 = new HashSet<>();
@@ -221,24 +222,27 @@ public class FiniteClosure implements IFiniteClosure {
 			HashSet<UnifyType> candidates = new HashSet<>();
 			// All types with the same name
 			strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
-			
-			for(UnifyType typePrime : result1) {
-				for (UnifyType theta2 : candidates) {
-					// Find the substitution
-					Optional<Unifier> sigma2Opt = unify.unify(typePrime, theta2);
-					if (!sigma2Opt.isPresent())
-						continue;
-					if(type.equals(theta2))
-						continue;
-					Unifier sigma2 = sigma2Opt.get();
-					sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams());
-					Set<UnifyType> theta1s = greater(theta2);
-					for (UnifyType theta1 : theta1s) {
-						// Because only the most general type is calculated, sigma1 = sigma2
-						UnifyType sigma1Theta1 = sigma2.apply(theta1);
-						result2.add(sigma1Theta1);
-					}
+
+			// for(UnifyType typePrime : result1)
+			for (UnifyType theta2 : candidates) {
+				// Find the substitution
+				Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
+				if (!sigma2Opt.isPresent())
+					continue;
+				//if (type.equals(theta2))
+				//	continue;
+				Unifier sigma2 = sigma2Opt.get();
+				if(sigma2.size() == 0) // type.equals(theta2)
+					continue;
+				sigma2.swapPlaceholderSubstitutions(type.getTypeParams());
+				Set<UnifyType> theta1s = greater(theta2);
+				for (UnifyType theta1 : theta1s) {
+					// Because only the most general type is calculated, sigma1
+					// = sigma2
+					UnifyType sigma1Theta1 = sigma2.apply(theta1);
+					result2.add(sigma1Theta1);
 				}
+			// }
 			}
 		}
 		
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java
index aa534b60..7ce251d9 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java
@@ -15,6 +15,11 @@ public final class TypeParams implements Iterable<UnifyType>{
 	 */
 	private final UnifyType[] typeParams;
 
+	/**
+	 * Hashcode calculation is expensive and must be cached.
+	 */
+	private final int hashCode;
+	
 	/**
 	 * Creates a new set of type parameters.
 	 * @param types The type parameters.
@@ -23,6 +28,9 @@ public final class TypeParams implements Iterable<UnifyType>{
 		typeParams = new UnifyType[types.size()];
 		for(int i=0;i<types.size();i++)
 			typeParams[i] = types.get(i);
+		
+		// Hashcode calculation is expensive and must be cached.
+		hashCode = Arrays.hashCode(typeParams);
 	}
 	
 	/**
@@ -31,6 +39,9 @@ public final class TypeParams implements Iterable<UnifyType>{
 	 */
 	public TypeParams(UnifyType... types) {
 		typeParams = types;
+		
+		// Hashcode calculation is expensive and must be cached.
+		hashCode = Arrays.hashCode(typeParams);
 	}
 	
 	/**
@@ -108,7 +119,7 @@ public final class TypeParams implements Iterable<UnifyType>{
 	
 	@Override
 	public int hashCode() {
-		return Arrays.hashCode(typeParams);
+		return hashCode;
 	}
 	
 	@Override
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
index 1a3988db..dbcc9b39 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
@@ -81,6 +81,13 @@ public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<P
 		return substitutions.get(t);
 	}
 
+	/**
+	 * The number of substitutions in the unifier. If zero, this is the identity function.
+	 */
+	public int size() {
+		return substitutions.size();
+	}
+	
 	/**
 	 * Garantuees that if there is a substitutions (a -> b) in this unifier,
 	 * a is not an element of the targetParams. Substitutions that do not
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
index ed2c95ef..62de0c96 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
@@ -9,18 +9,20 @@ public class UnifyPair {
 	/**
 	 * The type on the left hand side of the pair.
 	 */
-	private UnifyType lhs;
+	private final UnifyType lhs;
 	
 	/**
 	 * The type on the right hand side of the pair.
 	 */
-	private UnifyType rhs;
+	private final UnifyType rhs;
 	
 	/**
 	 * The operator that determines the relation between the left and right hand side type.
 	 */
 	private PairOperator pairOp;
 	
+	private final int hashCode;
+	
 	/**
 	 * Creates a new instance of the pair.
 	 * @param lhs The type on the left hand side of the pair.
@@ -31,6 +33,9 @@ public class UnifyPair {
 		this.lhs = lhs;
 		this.rhs = rhs;
 		pairOp = op;
+		
+		// Caching hashcode
+		hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode();
 	}	
 	
 	/**
@@ -68,7 +73,7 @@ public class UnifyPair {
 
 	@Override
 	public int hashCode() {
-		return 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode();
+		return hashCode;
 	}
 	
 	@Override