diff --git a/src/main/java/de/dhbwstuttgart/core/JavaTXCompiler.java b/src/main/java/de/dhbwstuttgart/core/JavaTXCompiler.java
index 03567487a..0be50fb5e 100644
--- a/src/main/java/de/dhbwstuttgart/core/JavaTXCompiler.java
+++ b/src/main/java/de/dhbwstuttgart/core/JavaTXCompiler.java
@@ -52,7 +52,7 @@ import org.antlr.v4.parse.ANTLRParser.throwsSpec_return;
 public class JavaTXCompiler {
 
     final CompilationEnvironment environment;
-    Boolean resultmodel = false;
+    Boolean resultmodel = true;
     public final Map<File, SourceFile> sourceFiles = new HashMap<>();
     Boolean log = true; //gibt an ob ein Log-File nach System.getProperty("user.dir")+"src/test/java/logFiles" geschrieben werden soll?
 
@@ -551,8 +551,8 @@ public class JavaTXCompiler {
 			}
 			/* UnifyResultModel End */
 			else {
-				//Set<Set<UnifyPair>> result = unify.unify(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
-				Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
+				Set<Set<UnifyPair>> result = unify.unify(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
+				//Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
 				System.out.println("RESULT: " + result);
 				logFile.write("RES: " + result.toString()+"\n");
 				logFile.flush();
diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
index 2cea2184c..ecef0e14e 100644
--- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
+++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
@@ -1,6 +1,7 @@
 package de.dhbwstuttgart.typeinference.unify;
 
 import java.io.FileWriter;
+import java.io.IOException;
 import java.io.Writer;
 import java.util.List;
 import java.util.Set;
@@ -30,6 +31,13 @@ public class TypeUnify {
 		ForkJoinPool pool = new ForkJoinPool();
 		pool.invoke(unifyTask);
 		Set<Set<UnifyPair>> res =  unifyTask.join();
+		try {
+			logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements + "\n");
+			logFile.flush();
+		}
+		catch (IOException e) {
+			System.err.println("no log-File");
+		}
 		return res;
 	}
 	
@@ -67,6 +75,13 @@ public class TypeUnify {
 		ForkJoinPool pool = new ForkJoinPool();
 		pool.invoke(unifyTask);
 		Set<Set<UnifyPair>> res =  unifyTask.join();
+		try {
+			logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
+			logFile.flush();
+		}
+		catch (IOException e) {
+			System.err.println("no log-File");
+		}
 		return ret;
 	}
 	
@@ -91,6 +106,13 @@ public class TypeUnify {
 	public Set<Set<UnifyPair>> unifyOderConstraints(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret) {
 		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, ret);
 		Set<Set<UnifyPair>> res = unifyTask.compute();
+		try {
+			logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
+			logFile.flush();
+		}
+		catch (IOException e) {
+			System.err.println("no log-File");
+		}
 		return res;
 	}
 
diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
index ea1c8410a..2cd36b41b 100644
--- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
+++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
@@ -115,6 +115,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	static int noBacktracking;
 	
+	Integer noShortendElements = 0;
+	
 	public TypeUnifyTask() { 
 		rules = new RuleSet();
 	}
@@ -293,6 +295,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		} while (eqSubst.isPresent());
 		
 		eq0.forEach(x -> x.disableCondWildcards());
+		
+		writeLog(nOfUnify.toString() + " Unifikation nach applyTypeUnificationRules: " + eq.toString());
+        writeLog(nOfUnify.toString() + " Oderconstraints nach applyTypeUnificationRules: " + oderConstraints.toString());
 
 		/*
 		 * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs
@@ -339,21 +344,16 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		if (printtag) System.out.println("eq2s " + eq2s);
 		//writeLog("BufferSet: " + bufferSet.toString()+"\n");
 		List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints);
-		Set<Set<UnifyPair>> collectErr = new HashSet<>();
-		Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput, collectErr);
+		Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput);
 		                                                //PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer 
 		                                                //nicht ausgewertet Faculty Beispiel im 1. Schritt
 		                                                //PL 2017-10-03 geloest, muesste noch mit FCs mit kleineren
 		                                                //Typen getestet werden.
 		writeLog(nOfUnify.toString() + " Oderconstraints2: " + oderConstraintsOutput.toString());
-		writeLog(nOfUnify.toString() + " collectErr: " + collectErr.toString());
 		if (printtag) System.out.println("secondLevelSets:" +secondLevelSets);
 		// If pairs occured that did not match one of the cartesian product cases,
 		// those pairs are contradictory and the unification is impossible.
 		if(!undefinedPairs.isEmpty()) {
-			Set<UnifyPair> flatCollectErr = new HashSet<>();
-			collectErr.forEach(x -> flatCollectErr.addAll(x));
-			undefinedPairs.addAll(flatCollectErr);
 			noUndefPair++;
 			for (UnifyPair up : undefinedPairs) {
 				writeLog(noUndefPair.toString() + " UndefinedPairs; " + up);
@@ -403,7 +403,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		
 		//Aufruf von computeCartesianRecursive ANFANG
 		//writeLog("topLevelSets: " + topLevelSets.toString());
-		return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, collectErr, finalresult);
+		return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult);
 	
 	}
 	
@@ -527,7 +527,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	
 	
-	Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<Set<Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set<Set<UnifyPair>> collectErr, Boolean finalresult) {
+	Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<Set<Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) {
 		//ArrayList<Set<Set<UnifyPair>>> remainingSets = new ArrayList<>(topLevelSets);
 		fstElems.addAll(topLevelSets.stream()
 				                    .filter(x -> x.size()==1)
@@ -552,16 +552,35 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		}
 		Set<Set<UnifyPair>> result = new HashSet<>(); 
 		int variance = 0;
-		Optional<Integer> xi = nextSetasList.stream().map(x -> x.stream().filter(y -> y.getLhsType() instanceof PlaceholderType)
-				                                  .filter(z -> ((PlaceholderType)z.getLhsType()).getVariance() != 0)
-				                                  .map(c -> ((PlaceholderType)c.getLhsType()).getVariance())
-				                                  .reduce((a,b)-> {if (a==b) return a; else return 2; })) //2 kommt insbesondere bei Oder-Constraints vor
-												  .filter(d -> d.isPresent())
-												  .map(e -> e.get())
-												  .findAny();
-		if (xi.isPresent()) {
-			variance = xi.get();
-		}		                                                  
+		
+		ArrayList<UnifyPair> zeroNextElem = new ArrayList<>(nextSetasList.get(0)); 
+		UnifyPair fstBasePair = zeroNextElem.remove(0).getBasePair();
+		
+		if (fstBasePair != null) {
+			Boolean sameBase = true;
+			for (UnifyPair ele : nextSetasList.get(0)) {//check ob a <. ty base oder ob Ueberladung
+				sameBase = sameBase && ele.getBasePair() != null && ele.getBasePair().equals(fstBasePair);
+			}
+			if (sameBase) {
+				Optional<Integer> xi = nextSetasList.stream().map(x -> x.stream().filter(y -> y.getLhsType() instanceof PlaceholderType)
+						.filter(z -> ((PlaceholderType)z.getLhsType()).getVariance() != 0)
+						.map(c -> ((PlaceholderType)c.getLhsType()).getVariance())
+						.reduce((a,b)-> {if (a==b) return a; else return 0; })) //2 kommt insbesondere bei Oder-Constraints vor
+						.filter(d -> d.isPresent())
+						.map(e -> e.get())
+						.findAny();
+				if (xi.isPresent()) {
+					variance = xi.get();
+				}
+			}
+			else {
+				variance = 2;
+			}
+
+		}
+		else {
+			variance = 2;
+		}
 		//if (variance == 1 && nextSetasList.size() > 1) {
 		//	List<Set<UnifyPair>> al = new ArrayList<>(nextSetasList.size());
 		//	for (int ii = 0; ii <  nextSetasList.size();ii++) {
@@ -592,6 +611,32 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		if (nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("D")).findFirst().isPresent() && nextSetasList.size()>1) 
 			System.out.print("");
 		writeLog("nextSetasList: " + nextSetasList.toString());
+		Set<UnifyPair> nextSetElem =  nextSetasList.get(0);
+		writeLog("BasePair1: " + nextSetElem + " " + nextSetElem.iterator().next().getBasePair());
+		
+		/* sameEqSet-Bestimmung: Wenn a = ty \in  nextSet dann enthaelt sameEqSet alle Paare a < ty1 oder ty2 < a aus fstElems */
+		Optional<UnifyPair> optOrigPair = nextSetElem.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
+                && (x.getPairOp().equals(PairOperator.EQUALSDOT))
+                	/*	(x.getBasePair().getLhsType() instanceof PlaceholderType 
+                     && x.getLhsType().equals(x.getBasePair().getLhsType()))
+                	|| (x.getBasePair().getRhsType() instanceof PlaceholderType 
+                		&& x.getLhsType().equals(x.getBasePair().getRhsType())))	
+                	*/	
+				)).findFirst();
+		Set<UnifyPair> sameEqSet = null;
+		if (optOrigPair.isPresent()) {
+			UnifyPair origPair = optOrigPair.get();
+			UnifyType tyVar;
+			if (!((tyVar = origPair.getLhsType()) instanceof PlaceholderType)) {
+				tyVar = origPair.getRhsType();
+			}
+			UnifyType tyVarEF = tyVar;
+			sameEqSet = fstElems.stream().map(xx -> xx.iterator().next())
+					.filter(x -> ((x.getLhsType().equals(tyVarEF) || x.getRhsType().equals(tyVarEF))))
+					.collect(Collectors.toCollection(HashSet::new));
+		}
+		/* sameEqSet-Bestimmung Ende */
+		
 		Set<UnifyPair> a = null;
 		while (nextSetasList.size() > 0) {  //(nextSetasList.size() != 0) {
 			Set<UnifyPair> a_last = a;
@@ -699,6 +744,30 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			Set<Set<UnifyPair>> res = new HashSet<>();
 			Set<Set<Set<UnifyPair>>> add_res = new HashSet<>();
 			Set<Set<UnifyPair>> aParDef = new HashSet<>();
+			
+			/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+			Optional<UnifyPair> optAPair = a.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
+	                && (x.getPairOp().equals(PairOperator.EQUALSDOT))
+	                	/*
+	                	(x.getBasePair().getLhsType() instanceof PlaceholderType 
+	                        && x.getLhsType().equals(x.getBasePair().getLhsType()))
+	                   	|| (x.getBasePair().getRhsType() instanceof PlaceholderType 
+	                   		&& x.getLhsType().equals(x.getBasePair().getRhsType())))
+	                   	*/	
+	                   		)).findFirst();
+			
+			if (optAPair.isPresent()) {//basepair ist entweder a <. Ty oder ty <. a
+				UnifyPair aPair = optAPair.get();
+				//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
+				writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
+				if (variance != 2 && !sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
+					a = null;
+					noShortendElements++;
+					continue;
+				}
+			}
+			/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+			
 			if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) {
 				Set<TypeUnify2Task> forks = new HashSet<>();
 				Set<UnifyPair> newEqOrig = new HashSet<>(eq);
@@ -721,6 +790,82 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					synchronized (this) { nextSetasList.remove(nSaL);
 						writeLog("1 RM" + nSaL.toString());
 					}
+					/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+					optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
+			                && ((x.getBasePair().getLhsType() instanceof PlaceholderType 
+			                        && x.getLhsType().equals(x.getBasePair().getLhsType()))
+			                   	|| (x.getBasePair().getRhsType() instanceof PlaceholderType 
+			                   		&& x.getLhsType().equals(x.getBasePair().getRhsType())))	
+			                   		)).findFirst();
+					
+					if (optAPair.isPresent()) {//basepair ist entweder a <. Ty oder ty <. a
+						UnifyPair aPair = optAPair.get();
+						//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
+						writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
+						if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
+							nSaL = null;
+							noShortendElements++;
+							continue;
+						}
+					}
+					/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+					
+					/* LOESCHEN, WENN KEINE FEHLER AUFTRETEN
+					optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null
+                            && x.getBasePair().getLhsType() instanceof PlaceholderType 
+                            && x.getLhsType().equals(x.getBasePair().getLhsType()))).findFirst();
+					if (optAPair.isPresent()) {
+						UnifyPair aPair = optAPair.get();
+					if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)) {
+						//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
+						//		.filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
+						//		.collect(Collectors.toCollection(HashSet::new));
+						//consideredElements.addAll(sameEqSet);
+						Boolean wrong = false;
+						writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
+						writeLog("nSaL: " + nSaL + " " + nSaL.iterator().next().getBasePair());
+						for (UnifyPair sameEq : sameEqSet) {
+							//writeLog("x1 Original:\n" + x1.toString());
+							if (sameEq.getLhsType() instanceof PlaceholderType) {
+								//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+								Set<UnifyPair> localEq = new HashSet<>(); 
+								Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+								unitedSubst.addAll(sameEq.getSubstitution());
+								localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+								if (isUndefinedPairSetSet(localRes)) {
+									if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+										result.addAll(localRes);
+									}
+									wrong = true;
+									break;
+								}
+							}
+							else {
+								//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+								Set<UnifyPair> localEq = new HashSet<>(); 
+								Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+								unitedSubst.addAll(sameEq.getSubstitution());
+								localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+								if (isUndefinedPairSetSet(localRes)) {
+									if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+										result.addAll(localRes);
+									}
+									wrong = true;
+									break;
+								}
+							}
+							//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
+						}
+						if (wrong) { 
+							nSaL = null;
+							noShortendElements++;
+							continue;
+						}
+					}}
+					*/
+					
 					Set<UnifyPair> newEq = new HashSet<>(eq);
 					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
 					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
@@ -785,6 +930,81 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					synchronized (this) { nextSetasList.remove(nSaL);
 						writeLog("-1 RM" + nSaL.toString());
 					}
+					
+					/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+					optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
+			                && ((x.getBasePair().getLhsType() instanceof PlaceholderType 
+			                        && x.getLhsType().equals(x.getBasePair().getLhsType()))
+			                   	|| (x.getBasePair().getRhsType() instanceof PlaceholderType 
+			                   		&& x.getLhsType().equals(x.getBasePair().getRhsType())))	
+			                   		)).findFirst();
+					
+					if (optAPair.isPresent()) {//basepair ist entweder a <. Ty oder ty <. a
+						UnifyPair aPair = optAPair.get();
+						//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
+						writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
+						if (variance != 2 && !sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
+							nSaL = null;
+							noShortendElements++;
+							continue;
+						}
+					}
+					/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
+					
+					/* LOESCHEN, WENN KEINE FEHLER AUFTRETEN
+					optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null
+                            && x.getBasePair().getLhsType() instanceof PlaceholderType 
+                            && x.getLhsType().equals(x.getBasePair().getLhsType()))).findFirst();
+					if (optAPair.isPresent()) {
+						UnifyPair aPair = optAPair.get();
+					if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)) {
+						//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
+						//		.filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
+						//		.collect(Collectors.toCollection(HashSet::new));
+						//consideredElements.addAll(sameEqSet);
+						Boolean wrong = false;
+						for (UnifyPair sameEq : sameEqSet) {
+							//writeLog("x1 Original:\n" + x1.toString());
+							if (sameEq.getLhsType() instanceof PlaceholderType) {
+								//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+								Set<UnifyPair> localEq = new HashSet<>(); 
+								Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+								unitedSubst.addAll(sameEq.getSubstitution());
+								localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+								if (isUndefinedPairSetSet(localRes)) {
+									if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+										result.addAll(localRes);
+									}
+									wrong = true;
+									break;
+								}
+							}
+							else {
+								//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+								Set<UnifyPair> localEq = new HashSet<>(); 
+								Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+								unitedSubst.addAll(sameEq.getSubstitution());
+								localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+								if (isUndefinedPairSetSet(localRes)) {
+									if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+										result.addAll(localRes);
+									}
+									wrong = true;
+									break;
+								}
+							}
+							//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
+						}
+						if (wrong) { 
+							nSaL = null;
+							noShortendElements++;
+							continue;
+						}
+					}}
+					*/
+					
 					Set<UnifyPair> newEq = new HashSet<>(eq);
 					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
 					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
@@ -976,10 +1196,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 						}
 						else {
 							//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
-							writeLog("RES Fst:" + result.toString() + " " + res.toString() + " " + collectErr.toString());
-							if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result))) {//Wenn Fehlerfall: dann die Fehler aus calculatePairSets hinzufuegen
-								result.addAll(collectErr);
-							}
+							writeLog("RES Fst:" + result.toString() + " " + res.toString());
 							result.addAll(res);
 						}
 						}
@@ -1010,9 +1227,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 									|| result.isEmpty()) {
 								//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
 								writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString());
-								if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result))) {//Wenn Fehlerfall: dann die Fehler aus calculatePairSets hinzufuegen
-									result.addAll(collectErr);
-								}
 								result.addAll(par_res);
 							}
 						}
@@ -1229,6 +1443,51 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		return result;
 	}
 	
+	protected Boolean checkA (UnifyPair aPair, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> elems, Set<Set<UnifyPair>> result) {
+		//if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)) 
+		//{
+			writeLog("checkA: " + aPair);
+			//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
+			//		.filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
+			//		.collect(Collectors.toCollection(HashSet::new));
+			//consideredElements.addAll(sameEqSet);
+			Boolean wrong = false;
+			for (UnifyPair sameEq : sameEqSet) {
+				//writeLog("x1 Original:\n" + x1.toString());
+				if (sameEq.getLhsType() instanceof PlaceholderType) {
+					//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+					Set<UnifyPair> localEq = new HashSet<>(); 
+					Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+					unitedSubst.addAll(sameEq.getSubstitution());
+					localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+					if (isUndefinedPairSetSet(localRes)) {
+						if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+							result.addAll(localRes);
+						}
+						return false;
+					}
+				}
+				else {
+					//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
+					Set<UnifyPair> localEq = new HashSet<>(); 
+					Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
+					unitedSubst.addAll(sameEq.getSubstitution());
+					localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
+					if (isUndefinedPairSetSet(localRes)) {
+						if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+							result.addAll(localRes);
+						}
+						return false;
+					}
+				}	
+				//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
+			} 
+		//}
+		return true;
+	}
+	
 	protected boolean couldBecorrect(Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set<UnifyPair> nextElem) {
 		return reducedUndefResSubstGroundedBasePair.stream()
 		.map(pair -> {
@@ -1502,7 +1761,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	 * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements
 	 * (as in case 1 where sigma is added to the innermost set).
 	 */
-	protected Set<Set<Set<Set<UnifyPair>>>> calculatePairSets(Set<UnifyPair> eq2s, List<Set<Set<UnifyPair>>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<Set<Set<UnifyPair>>> oderConstraintsOutput, Set<Set<UnifyPair>> collectErr) {
+	protected Set<Set<Set<Set<UnifyPair>>>> calculatePairSets(Set<UnifyPair> eq2s, List<Set<Set<UnifyPair>>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<Set<Set<UnifyPair>>> oderConstraintsOutput) {
 		oderConstraintsOutput.addAll(oderConstraintsInput);
 		List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9);
 
@@ -1589,6 +1848,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 						remElem.add(new UnifyPair(pair.getLhsType(), new SuperType(pair.getRhsType()), PairOperator.EQUALSDOT));
 						x1.remove(remElem);
 					}
+					/* ZU LOESCHEN ANFANG
 				//System.out.println(x1);
 					Set<UnifyPair> sameEqSet = eq2sAsList.stream()
 							  .filter(x -> ((x.getLhsType().equals(lhsType) || x.getRhsType().equals(lhsType)) && !x.equals(pair)))
@@ -1651,7 +1911,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 						x1ResPrime = x1Res;
 					}
 					result.get(0).add(x1ResPrime);
-					if (x1ResPrime.isEmpty()) {
+					ZU LOESCHEN ENDE */
+					result.get(0).add(x1);
+					if (x1.isEmpty()) {
 						undefined.add(pair); //Theta ist nicht im FC => Abbruch
 					}
 				}
@@ -1758,7 +2020,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		}
 		
 		// Filter empty sets or sets that only contain an empty set.
-		writeLog("collectErr: " + collectErr);
 		return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new)))
 				.filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
 	}
diff --git a/src/test/resources/bytecode/javFiles/MatrixOP.jav b/src/test/resources/bytecode/javFiles/MatrixOP.jav
index 638cff35a..8be24d17b 100644
--- a/src/test/resources/bytecode/javFiles/MatrixOP.jav
+++ b/src/test/resources/bytecode/javFiles/MatrixOP.jav
@@ -1,6 +1,6 @@
 import java.util.Vector;
 import java.lang.Integer;
-//import java.lang.Byte;
+import java.lang.Byte;
 import java.lang.Boolean;
 
 public class MatrixOP  extends Vector<Vector<Integer>> {