diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java
index fa640eb8..1f9b4fb4 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java
@@ -48,7 +48,8 @@ public interface IFiniteClosure {
 	
 	public Set<UnifyType> grArg(PlaceholderType type);
 	public Set<UnifyType> smArg(PlaceholderType type);
-	
+	
 	public Optional<UnifyType> getGenericType(String typeName);
-	public Set<UnifyType> getAllTypes(String typeName);
+	public Set<UnifyType> getAllTypesByName(String typeName);
+
 }
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
index 35fae6cb..757e53d1 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
@@ -1,5 +1,7 @@
 package de.dhbwstuttgart.typeinference.unify.model;
 
+import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Optional;
@@ -7,13 +9,19 @@ import java.util.Set;
 import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
+import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify;
 
 public class FiniteClosure implements IFiniteClosure {
 	
 	private HashMap<UnifyType, Node<UnifyType>> inheritanceGraph;
 	private HashMap<String, HashSet<Node<UnifyType>>> strInheritanceGraph;
 	
+	public FiniteClosure() {
+		
+	}
+	
 	public FiniteClosure(Set<MPair> pairs) {
 		
 		inheritanceGraph = new HashMap<UnifyType, Node<UnifyType>>();
@@ -50,33 +58,120 @@ public class FiniteClosure implements IFiniteClosure {
 			strInheritanceGraph.get(key.getName()).add(inheritanceGraph.get(key));
 		}
 	}
-	
+
 	/**
 	 * Returns all types of the finite closure that are subtypes of the argument.
 	 * @return The set of subtypes of the argument.
 	 */
-	@Override
+	@Override
 	public Set<UnifyType> smaller(UnifyType type) {
-		if(!inheritanceGraph.containsKey(type))
-			return new HashSet<>();
-		
-		Set<UnifyType> result = inheritanceGraph.get(type).getContentOfDescendants();
+		// - if(T < T') then T <=* T'
+		Set<UnifyType> result = inheritanceGraph.containsKey(type) ? inheritanceGraph.get(type).getContentOfDescendants() : new HashSet<>();
+
 		result.add(type);
 		
+		// if T1 <=* T2 then sigma1(T1)  <=* sigma1(T2)
+		// where foreach type var a in T2:
+		// sigma1(T1) <=* sigma2(T2)
+		/*if(strInheritanceGraph.containsKey(type.getName())) {
+			IUnify unify = new MartelliMontanariUnify();
+			HashSet<Node<Type>> candidateNodes = strInheritanceGraph.get(type.getName());
+			for(Node<Type> candidateNode : candidateNodes) {
+				Type theta2 = candidateNode.getContent();
+				Optional<Unifier> sigma2 = unify.unify(theta2, type);
+				if(!sigma2.isPresent())
+					continue;
+				for(Type sigma1theta1 : candidateNode.getContentOfDescendants()) {
+					Type theta1 = sigma2.get().apply(sigma1theta1);
+				}
+			}
+		}*/
+		
+		if(type.getTypeParams().size() == 0)
+			return result;
+		
+		ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+		for(UnifyType param : type.getTypeParams()) {
+			if(param instanceof ExtendsType || param instanceof SuperType) {
+				Set<UnifyType> pc = param.smArg(this);
+				paramCandidates.add(pc);
+			} else {
+				HashSet<UnifyType> pc = new HashSet<>();
+				pc.add(param);
+				paramCandidates.add(pc);
+			}
+		}
+		
+		Set<TypeParams> permResult = new HashSet<>();
+		permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]);
+		
+		for(TypeParams newParams : permResult)
+			result.add(type.setTypeParams(newParams));
+		
 		return result;
 	}
 	
+	/**
+	 * @param t1
+	 * @param t2
+	 * @return
+	 */
+	protected Optional<Unifier> match(UnifyType t1, UnifyType t2) {
+		if(!t1.getName().equals(t2.getName()))
+			return Optional.empty();
+		
+		TypeParams t1Params = t1.getTypeParams();
+		TypeParams t2Params = t2.getTypeParams();
+	
+		if(t1Params.size() != t2Params.size())
+			return Optional.empty();
+		
+		Unifier result = new Unifier();
+		for(int i = 0; i < t1Params.size(); i++) {
+			UnifyType t1i = t1Params.get(i);
+			UnifyType t2i = t2Params.get(i);
+			
+			boolean equal = t1i.equals(t2i);
+			if(!equal && !(t2i instanceof PlaceholderType))
+				return Optional.empty();
+			
+			if(!equal && t2i instanceof PlaceholderType)
+				result.Add((PlaceholderType) t2i, t1i);
+		}
+		
+		return Optional.of(result);
+	}
+	
 	/**
 	 * Returns all types of the finite closure that are supertypes of the argument.
 	 * @return The set of supertypes of the argument.
 	 */
-	@Override
+	@Override
 	public Set<UnifyType> greater(UnifyType type) {
-		if(!inheritanceGraph.containsKey(type))
-			return new HashSet<>();
-		
-		Set<UnifyType> result = inheritanceGraph.get(type).getContentOfPredecessors();
+		Set<UnifyType> result = inheritanceGraph.containsKey(type) ? inheritanceGraph.get(type).getContentOfPredecessors() : new HashSet<>();
 		result.add(type);
+
+		if(type.getTypeParams().size() == 0)
+			return result;
+		
+		ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+		for(UnifyType param : type.getTypeParams()) {
+			if(param instanceof ExtendsType || param instanceof SuperType) {
+				Set<UnifyType> pc = param.grArg(this);
+				paramCandidates.add(pc);
+			} else {
+				HashSet<UnifyType> pc = new HashSet<>();
+				pc.add(param);
+				paramCandidates.add(pc);
+			}
+		}
+		
+		Set<TypeParams> permResult = new HashSet<>();
+		permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]);
+		
+		for(TypeParams newParams : permResult)
+			result.add(type.setTypeParams(newParams));
+		
 		return result;
 	}
 	
@@ -103,8 +198,9 @@ public class FiniteClosure implements IFiniteClosure {
 	public Set<UnifyType> grArg(ExtendsType type) {
 		if(!inheritanceGraph.containsKey(type.getExtendedType()))
 			return new HashSet<UnifyType>();
-		
+	
 		Set<UnifyType> result = new HashSet<UnifyType>();
+		result.add(type);
 		
 		UnifyType t = type.getExtendedType();
 		
@@ -117,8 +213,9 @@ public class FiniteClosure implements IFiniteClosure {
 	public Set<UnifyType> grArg(SuperType type) {
 		if(!inheritanceGraph.containsKey(type.getSuperedType()))
 			return new HashSet<UnifyType>();
-		
+
 		Set<UnifyType> result = new HashSet<UnifyType>();
+		result.add(type);
 		
 		UnifyType t = type.getSuperedType();
 		
@@ -127,9 +224,13 @@ public class FiniteClosure implements IFiniteClosure {
 		return result;
 	}
 	
-	@Override
+	@Override
 	public Set<UnifyType> grArg(PlaceholderType type) {
-		return new HashSet<>();
+		HashSet<UnifyType> result = new HashSet<>();
+		result.add(type);
+		result.add(new SuperType(type));
+		result.add(new ExtendsType(type));
+		return result;
 	}
 
 	@Override	
@@ -153,8 +254,9 @@ public class FiniteClosure implements IFiniteClosure {
 	public Set<UnifyType> smArg(ExtendsType type) {
 		if(!inheritanceGraph.containsKey(type.getExtendedType()))
 			return new HashSet<UnifyType>();
-		
+		
 		Set<UnifyType> result = new HashSet<UnifyType>();
+		result.add(type);
 		
 		UnifyType t = type.getExtendedType();
 		
@@ -172,8 +274,9 @@ public class FiniteClosure implements IFiniteClosure {
 	public Set<UnifyType> smArg(SuperType type) {
 		if(!inheritanceGraph.containsKey(type.getSuperedType()))
 			return new HashSet<UnifyType>();
-		
+		
 		Set<UnifyType> result = new HashSet<UnifyType>();
+		result.add(type);
 		
 		UnifyType t = type.getSuperedType();
 		
@@ -186,9 +289,13 @@ public class FiniteClosure implements IFiniteClosure {
 		return result;
 	}
 	
-	@Override
+	@Override
 	public Set<UnifyType> smArg(PlaceholderType type) {
-		return new HashSet<>();
+		HashSet<UnifyType> result = new HashSet<>();
+		result.add(type);
+		result.add(new SuperType(type));
+		result.add(new ExtendsType(type));
+		return result;
 	}
 
 	@Override
@@ -207,10 +314,24 @@ public class FiniteClosure implements IFiniteClosure {
 		return Optional.empty();
 	}
 	
-	@Override
-	public Set<UnifyType> getAllTypes(String typeName) {
+	@Override
+	public Set<UnifyType> getAllTypesByName(String typeName) {
 		if(!strInheritanceGraph.containsKey(typeName))
 			return new HashSet<>();
 		return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new));
 	}
+	
+	protected void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
+		if(candidates.size() == idx) {
+			result.add(new TypeParams(Arrays.copyOf(current, current.length)));
+			return;
+		}
+		
+		Set<UnifyType> localCandidates = candidates.get(idx);
+		
+		for(UnifyType t : localCandidates) {
+			current[idx] = t;
+			permuteParams(candidates, idx+1, result, current);
+		}
+	}
 }
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
index c277f8fc..aab24276 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
@@ -5,8 +5,10 @@ import java.util.Map.Entry;
 import java.util.Set;
 import java.util.function.Function;
 
-public class Unifier implements Function<UnifyType, UnifyType> {
+
+public class Unifier implements Function<UnifyType, UnifyType> /*, Set<MPair>*/ { // TODO set implementieren
 	private HashMap<PlaceholderType, UnifyType> substitutions = new HashMap<>();
+
 	
 	public static Unifier IDENTITY = new Unifier();
 	
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java
index 4409ae7f..858fd80a 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java
+++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java
@@ -101,12 +101,12 @@ public class MartelliMontanariUnify implements IUnify {
 		TypeParams rhsTypeParams = rhs.getTypeParams();
 		TypeParams lhsTypeParams = lhs.getTypeParams();
 		
+		if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size())
+			return null; // conflict
+		
 		if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
 			return Optional.empty();
 		
-		if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size())
-			return null; // conflict
-			
 		for(int i = 0; i < rhsTypeParams.size(); i++)
 			result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
 
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
index 6fa2eda1..1023c852 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
+++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
@@ -57,33 +57,48 @@ public class Unify {
 		 * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
 		 */
 		
-		// All Sets
-		List<Set<MPair>> sets = new ArrayList<Set<MPair>>();
+		// There are up to 10 toplevel set. 8 of 10 are the result of the 
+		// cartesian product of the sets created by pattern matching.
+		List<Set<Set<MPair>>> topLevelSets = new ArrayList<>();
 		
-		if(eq1s.size() != 0)
-			sets.add(eq1s); // Add Eq1'
+		if(eq1s.size() != 0) {
+			Set<Set<MPair>> wrap = new HashSet<>();
+			wrap.add(eq1s);
+			topLevelSets.add(wrap); // Add Eq1'
+		}
 
 		// Add the set of [a =. Theta | (a=. Theta) in Eq2']
 		Set<MPair> bufferSet = eq2s.stream()
 				.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
 				.collect(Collectors.toSet());
 		
-		if(bufferSet.size() != 0)
-			sets.add(bufferSet);
+		if(bufferSet.size() != 0) {
+			Set<Set<MPair>> wrap = new HashSet<>();
+			wrap.add(bufferSet);
+			topLevelSets.add(wrap);
+		}
 		
 		// Sets that originate from pair pattern matching
 		// Sets of the "second level"
-
-		sets.addAll(calculatePairSets(eq2s, fc));
+		Set<Set<Set<MPair>>> secondLevelSets = calculatePairSets(eq2s, fc);
 		
 		/* Up to here, no cartesian products are calculated.
-		 * Around here, filters for pairs and sets can be applied */
+		 * filters for pairs and sets can be applied here */
 		
 		ISetOperations setOps = new GuavaSetOperations();
 		
-		// Calculate the cartesian products
-		Set<Set<MPair>> result = setOps.cartesianProduct(sets).stream()
-				.map(x -> new HashSet<MPair>(x)).collect(Collectors.toCollection(HashSet::new));
+		// Sub cartesian products of the second level (pattern matched) sets
+		for(Set<Set<MPair>> secondLevelSet : secondLevelSets) {
+			List<Set<MPair>> secondLevelSetList = new ArrayList<>(secondLevelSet);
+			topLevelSets.add(setOps.cartesianProduct(secondLevelSetList)
+					.stream().map(x -> new HashSet<>(x))
+					.collect(Collectors.toCollection(HashSet::new)));
+		}
+		
+		// Cartesian product over all (up to 10) top level sets 
+		Set<Set<Set<MPair>>> eqPrimeSet = setOps.cartesianProduct(topLevelSets)
+				.stream().map(x -> new HashSet<>(x))
+				.collect(Collectors.toCollection(HashSet::new));
 		//System.out.println(result);
 
 		/*
@@ -91,38 +106,41 @@ public class Unify {
 		 */
 		
 		/*
-		 * TODO 
-		 * Im Paper wird Eq'' genannt, es wird also von einer Menge in einer Menge in einer Menge ausgegangen.
-		 * Durch das flache Kartesische Produkt gibt es hier aber nur Mengen in Mengen.
-		 * Richtig so?
+		 * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht)
 		 */
+		Set<Set<MPair>> eqPrimeSetFlat = new HashSet<>();
+		for(Set<Set<MPair>> setToFlatten : eqPrimeSet) {
+			Set<MPair> buffer = new HashSet<>();
+			setToFlatten.stream().forEach(x -> buffer.addAll(x));
+			eqPrimeSetFlat.add(buffer);
+		}
 		
 		IRuleSet rules = new RuleSet(fc);
 		Set<Set<MPair>> changed = new HashSet<>();
-		Set<Set<MPair>> unchanged = new HashSet<>();
+		Set<Set<MPair>> eqPrimePrimeSet = new HashSet<>();
 		
-		for(Set<MPair> eqss : result) {
-			Optional<Set<MPair>> newEqss = rules.subst(eqss);
-			if(newEqss.isPresent()) 
-				changed.add(newEqss.get());
-			else 
-				unchanged.add(eqss);
+		for(Set<MPair> eqPrime : eqPrimeSetFlat) {
+			Optional<Set<MPair>> eqPrimePrime = rules.subst(eqPrime);
+			
+			if(eqPrimePrime.isPresent())
+				changed.add(eqPrimePrime.get());
+			else
+				eqPrimePrimeSet.add(eqPrime);
 		}
 
-		
 		/*
 		 * Step 6 a) Restart for pairs where subst was applied
 		 * 		  b) Build the union over everything
 		 */
 		
-		for(Set<MPair> eqss : changed)
-			unchanged.addAll(this.unify(eqss, fc));
+		for(Set<MPair> eqss : changed) {
+			eqPrimePrimeSet.addAll(this.unify(eqss, fc));
+		}
 		
 		 /*
-		  * Step 7: Filter result for solved pairs TODO wie?
+		  * Step 7: Filter result for solved pairs
 		  */
-		
-		return unchanged;
+		return eqPrimePrimeSet;
 		
 	}
 	
@@ -217,8 +235,12 @@ public class Unify {
 	}
 	
 	
-	protected List<Set<MPair>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
-		List<Set<MPair>> result = new ArrayList<Set<MPair>>();
+	protected Set<Set<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
+		List<Set<Set<MPair>>> result = new ArrayList<>();
+		
+		// Init all 8 cases
+		for(int i = 0; i < 8; i++)
+			result.add(new HashSet<>());
 		
 		for(MPair pair : eq2s) {
 			
@@ -226,105 +248,223 @@ public class Unify {
 			UnifyType lhsType = pair.getLhsType();
 			UnifyType rhsType = pair.getRhsType();
 	
-			// Case 1: (a <. Theta')
-			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
-				UnifyType thetaPrime = pair.getRhsType();
-				Set<MPair> set = new HashSet<>();
-				IUnify unify = new MartelliMontanariUnify();
-				
-				//Set<Type> cs = fc.getAllTypes(rhsType.getName());
-				UnifyType c = rhsType;
-				
-				//Set<Type> thetaQs = cs.stream().flatMap(x -> fc.smaller(x).stream()).collect(Collectors.toCollection(HashSet::new));
-				Set<UnifyType> thetaQs = fc.smaller(c);
-				
-				Set<UnifyType> thetaQPrimes = new HashSet<>();
-				
-				TypeParams cParams = c.getTypeParams();
-				if(cParams.size() == 0)
-					thetaQPrimes.add(c);
-				else {
-					ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
-					for(UnifyType param : cParams)
-						candidateParams.add(fc.grArg(param));
-					Set<TypeParams> permutations = new HashSet<TypeParams>();
-					permuteParams(candidateParams, 0, permutations, new UnifyType[candidateParams.size()]);
-					
-					for(TypeParams tp : permutations)
-						thetaQPrimes.add(c.setTypeParams(tp));
-				}
-				
-				for(UnifyType tqp : thetaQPrimes) {
-					Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
-					if(opt.isPresent()) {
-						Unifier unifier = opt.get();
-						Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
-						for(Entry<PlaceholderType, UnifyType> sigma : substitutions)
-							set.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
-						for(UnifyType tq : thetaQs) {
-							Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
-							smaller.stream().map(x -> new MPair(lhsType, x, PairOperator.EQUALSDOT)).forEach(x -> set.add(x));
-						}
-					}
-				}
-				
-				result.add(set);
-			}
+			// Case 1: (a <. Theta')
+			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
+				result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
 			
 			// Case 2: (a <.? ? ext Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){
-				throw new NotImplementedException(); // TODO
-			}
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
+				result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
 			
-			// Case 3: (a <.? ? sup Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) {
-				Set<MPair> set = new HashSet<>();
-				for(UnifyType theta : fc.smArg(rhsType))
-					set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT));
-				result.add(set);
-			}
+			// Case 3: (a <.? ? sup Theta')
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
+				result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
 			
 			// Case 4: (a <.? Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) {
-				Set<MPair> set = new HashSet<>();
-				set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT));
-				result.add(set);
-			}
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
+				result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc));
 				
-			// Case 5: (Theta <. a)
-			else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) {
-				Set<MPair> set = new HashSet<>();
-				for(UnifyType thetaS : fc.greater(lhsType))
-					set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
-				result.add(set);
-			}
+			// Case 5: (Theta <. a)
+			else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
+				result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
 			
 			// Case 6: (? ext Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) {
-				Set<MPair> set = new HashSet<>();
-				for(UnifyType thetaS : fc.grArg(lhsType))
-					set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
-				result.add(set);
-			}
-			
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
+				result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));
+
 			// Case 7: (? sup Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) {
-				throw new NotImplementedException(); // TODO
-			}
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
+				result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc));
 			
 			// Case 8: (Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) {
-				Set<MPair> set = new HashSet<>();
-				for(UnifyType thetaS : fc.grArg(lhsType))
-					set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
-				result.add(set);
+			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
+				result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
+		}
+		
+		return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
+	}
+	
+	protected Set<MPair> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
+					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+
 			}
 		}
 		
 		return result;
 	}
 	
-	protected void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
+	protected Set<MPair> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		UnifyType thetaPrime = extThetaPrime.getExtendedType();
+		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					ExtendsType extTq = new ExtendsType(tq);
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(extTq));
+					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+			}
+		}
+		
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType theta : fc.smArg(subThetaPrime))
+			result.add(new MPair(a, theta, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		result.add(new MPair(a, thetaPrime, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.greater(theta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.grArg(extTheta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		UnifyType theta = supTheta.getSuperedType();
+		Set<UnifyType> cs = fc.getAllTypesByName(theta.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, theta);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
+					smaller.stream().map(x -> new MPair(a, new SuperType(x), PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+
+			}
+		}
+		
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.grArg(theta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<TypeParams> permuteParams(ArrayList<Set<UnifyType>> candidates) {
+		Set<TypeParams> result = new HashSet<>();
+		permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
+		return result;
+	}
+	
+	private void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
 		if(candidates.size() == idx) {
 			result.add(new TypeParams(Arrays.copyOf(current, current.length)));
 			return;
@@ -336,14 +476,5 @@ public class Unify {
 			current[idx] = t;
 			permuteParams(candidates, idx+1, result, current);
 		}
-	}
-	
-	private Set<UnifyType> getAllInstantiations(UnifyType t, IFiniteClosure fc) {
-		Set<UnifyType> result = new HashSet<>();
-		result.add(t);
-		return result;
-		
-		// TODO
-	}
-
+	}
 }
diff --git a/test/bytecode/types/AutoOverloading.jav b/test/bytecode/types/AutoOverloading.jav
index 314a7f48..8d97f705 100644
--- a/test/bytecode/types/AutoOverloading.jav
+++ b/test/bytecode/types/AutoOverloading.jav
@@ -1,15 +1,20 @@
 class AutoOverloading{
 
         method2(String p){
-
+			return p;
         }
         
         method2(Integer p){
-
+			return p;
         }
         
 
         method(p){
-                method2(p);
+                return method2(p);
+        }
+        
+        public static void main(String[] args){
+        	System.out.println(methode("hallo"));
+        	System.out.println(methode(2));
         }
 }
\ No newline at end of file
diff --git a/test/bytecode/types/SuperType.java b/test/bytecode/types/SuperType.java
index 5b2e2e12..42a8d77b 100644
--- a/test/bytecode/types/SuperType.java
+++ b/test/bytecode/types/SuperType.java
@@ -17,6 +17,7 @@ import bytecode.SourceFileBytecodeTest;
 
 
 public class SuperType extends SourceFileBytecodeTest{
+
 	@Override
 	protected void init() {
 		testName = "ExtendsType";
diff --git a/test/unify/FiniteClosureTest.java b/test/unify/FiniteClosureTest.java
index 1b19969c..314bed58 100644
--- a/test/unify/FiniteClosureTest.java
+++ b/test/unify/FiniteClosureTest.java
@@ -1,16 +1,38 @@
 package unify;
 
-import java.util.HashSet;
-import java.util.Set;
-
+import org.junit.Assert;
 import org.junit.Test;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
-import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
-import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
+import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
+import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 
-public class FiniteClosureTest {
+public class FiniteClosureTest extends FiniteClosure {
+	
+	@Test
+	public void testMatch() {
+		TypeFactory tf = new TypeFactory();
+		
+		UnifyType a = tf.getPlaceholderType("a");
+		UnifyType b = tf.getPlaceholderType("b");
+		UnifyType c = tf.getPlaceholderType("c");
+		
+		UnifyType A = tf.getSimpleType("A");
+		UnifyType B = tf.getSimpleType("B");
+		UnifyType C1 = tf.getSimpleType("C", a, b, c);
+		UnifyType C2 = tf.getSimpleType("C", a, A, b);
+		UnifyType C3 = tf.getSimpleType("C", A, B, A);
+		UnifyType D1 = tf.getSimpleType("D", C1, a, b, c);
+		UnifyType D2 = tf.getSimpleType("D", C3, A, B, A);
+		
+		System.out.println(match(C2, C1));
+		System.out.println(match(C3, C1));
+		System.out.println(match(D2, D1));
+		Assert.assertFalse(match(C3, C2).isPresent());
+		Assert.assertFalse(match(C1, C2).isPresent());
+	}
 	
 	@Test
 	public void testGreater() {
@@ -36,10 +58,14 @@ public class FiniteClosureTest {
 	
 	@Test
 	public void testSmaller() {
-		IFiniteClosure fc = new FiniteClosureBuilder().getCollectionExample();
+		FiniteClosureBuilder fcb = new FiniteClosureBuilder();
 		TypeFactory tf = new TypeFactory();
 		
+		fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number"));
+		IFiniteClosure fc = fcb.getCollectionExample();
+		
 		System.out.println("\n\n----- Smaller Test -----");
+		System.out.println("Smaller(List<? extends Number>) = " + fc.smaller(tf.getSimpleType("List", tf.getExtendsType(tf.getSimpleType("Number")))));
 		System.out.println("Smaller(List<T>) = " + fc.smaller(tf.getSimpleType("List", "T")));
 		System.out.println("Smaller(TreeSet<T>) = " + fc.smaller(tf.getSimpleType("TreeSet", "T")));
 		System.out.println("Smaller(Collection) = " + fc.smaller(tf.getSimpleType("Collection")));
diff --git a/test/unify/GenerateFiniteClosure.java b/test/unify/GenerateFiniteClosure.java
index b13cdc76..42a5e862 100644
--- a/test/unify/GenerateFiniteClosure.java
+++ b/test/unify/GenerateFiniteClosure.java
@@ -16,7 +16,7 @@ import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
 import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 
-public class GenerateFiniteClosure {
+public class GenerateFiniteClosure{
 
 	private TypeAssumptions generateAssumptionsFromImport(String importClass){
 		SourceFile sf = new SourceFile();
@@ -44,7 +44,7 @@ public class GenerateFiniteClosure {
 		String importClass = "java.util.Vector";
 		TypeAssumptions ass = generateAssumptionsFromImport(importClass);
 		FiniteClosure fc = UnifyTypeFactory.generateFC(ass);
-		Set<UnifyType> test = fc.getAllTypes(importClass);
+		Set<UnifyType> test = fc.getAllTypesByName(importClass);
 		assertTrue(test.size()>0);
 	}
 
diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java
index 60486017..e9bed425 100644
--- a/test/unify/UnifyTest.java
+++ b/test/unify/UnifyTest.java
@@ -24,6 +24,7 @@ public class UnifyTest extends Unify {
 		//fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object"));
 		fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number"));
 		fcb.add(tf.getSimpleType("Double"), tf.getSimpleType("Number"));
+		fcb.add(tf.getSimpleType("MyList"), tf.getSimpleType("List", tf.getSimpleType("Integer")));
 		//fcb.add(tf.getSimpleType("List", "T"));
 		
 		IFiniteClosure fc = fcb.getCollectionExample();
@@ -35,9 +36,9 @@ public class UnifyTest extends Unify {
 		// Double <. B
 		// B <. Object
 		eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
-		//eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
+		eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT));
-		eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", tf.getSimpleType("Number")), PairOperator.SMALLERDOT));
+		//eq.add(new MPair(tf.getPlaceholderType("A"),  tf.getSimpleType("List", "A"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT));
@@ -78,9 +79,8 @@ public class UnifyTest extends Unify {
 		candidates.add(p1);
 		candidates.add(p2);
 		candidates.add(p3);
-		
-		Set<TypeParams> result = new HashSet<>();
-		permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
+		
+		Set<TypeParams> result = permuteParams(candidates);
 		
 		System.out.println(result);
 	}