diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
index aa2e25a0..8377edd6 100644
--- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
+++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
@@ -624,7 +624,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	 */
 	Set<Set<UnifyPair>> computeCartesianRecursive(ArrayList<Set<? extends Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
 		
-		//fstElems: Alle 1-elementigen Mengen, die nur ein Paar 
+		//oneElems: Alle 1-elementigen Mengen, die nur ein Paar 
 		//a <. theta, theta <. a oder a =. theta enthalten 
 		Set<Set<UnifyPair>> oneElems = new HashSet<>();
 		oneElems.addAll(topLevelSets.stream()
@@ -846,11 +846,19 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			i++;
 			Set<Set<UnifyPair>> elems = new HashSet<Set<UnifyPair>>(oneElems);
 			writeLog("a1: " + rekTiefe + "  "+ "variance:  "+ variance + " " + a.toString()+ "\n");
+			
+			//Ergebnisvariable für den aktuelle Thread
 			Set<Set<UnifyPair>> res = new HashSet<>();
+			
+			//Menge der Ergebnisse der geforkten Threads
 			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 */
+			/* Wenn bei (a \in theta) \in a zu Widerspruch in oneElems wird
+			 * a verworfen und zu nächstem Element von nextSetasList gegangen  
+			 */
 			if (!oderConstraint && !sameEqSet.isEmpty()) {
 				//optAPair enthaelt ggf. das Paar a = ty' \in a
 				//unterscheidet sich von optOrigPair, da dort a = ty
@@ -873,15 +881,20 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					UnifyPair aPair = optAPair.get();
 					//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
 					writeLog("variance: " + variance + "sameEqSet:" + sameEqSet);
+					boolean newCheckA = newCheckA(a, sameEqSet, result);
 					if (!checkA(aPair, sameEqSet, elems, result)) {
+						writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
 						a = null;
 						noShortendElements++;
 						continue;
 					}
+					else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
 				}
 			}
-			/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
 			
+			/* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread
+			 * gestartet, der parallel weiterarbeitet.
+			 */
 			if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) {
 				Set<TypeUnify2Task> forks = new HashSet<>();
 				Set<UnifyPair> newEqOrig = new HashSet<>(eq);
@@ -931,11 +944,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 							UnifyPair aPair = optAPair.get();
 							//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
 							writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
+							boolean newCheckA = newCheckA(nSaL, sameEqSet, result);
 							if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
+								writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
 								nSaL = null;
 								noShortendElements++;
 								continue;
 							}
+							else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
 						}
 					}
 					/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
@@ -1051,11 +1067,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 							UnifyPair aPair = optAPair.get();
 							//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
 							writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
+							boolean newCheckA = newCheckA(nSaL, sameEqSet, result);
 							if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
+								writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
 								nSaL = null;
 								noShortendElements++;
 								continue;
 							}
+							else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
 						}
 					}
 					/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
@@ -1201,11 +1220,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					};
 				} 
 		    	//noOfThread++;	
-		    } else {
-		    	//parallel = false; //Wenn MaxNoOfThreads erreicht ist, sequentiell weiterarbeiten
+		    } else {//parallel = false oder MaxNoOfThreads ist erreicht, sequentiell weiterarbeiten
 				elems.add(a); //PL 2019-01-16 muss das wirklich hin steht schon in Zeile 859 ja braucht man siehe Zeile 859
 				res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe);
 		    }}}
+			
+			//Ab hier alle parallele Berechnungen wieder zusammengeführt.
 				if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) {
 					//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
 					result = res;
@@ -1540,6 +1560,66 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		return result;
 	}
 	
+	protected Boolean newCheckA(Set<UnifyPair> a, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> result) {
+		
+			//optAPair enthaelt ggf. das Paar a = ty' \in a
+			//unterscheidet sich von optOrigPair, da dort a = ty
+			Optional<UnifyPair> optAPair = 
+				a.stream().filter(x -> (x.getPairOp().equals(PairOperator.EQUALSDOT)))
+				          .filter(x -> //Sicherstellen, dass bei a = ty a auch wirklich die gesuchte Typvariable ist 
+            	                  x.getLhsType().equals(x.getBasePair().getLhsType()) || 
+            	                  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("checkA: " + aPair + "sameEqSet: " + sameEqSet);
+			for (UnifyPair sameEq : sameEqSet) {
+				if (sameEq.getLhsType() instanceof PlaceholderType) {
+					Set<UnifyPair> localEq = new HashSet<>(); 
+					Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getAllSubstitutions());
+					unitedSubst.addAll(aPair.getAllBases());
+					unitedSubst.addAll(sameEq.getAllSubstitutions());
+					unitedSubst.addAll(sameEq.getAllBases());
+					localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+					finalresult = false;
+					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0);
+					finalresult = true;
+					if (isUndefinedPairSetSet(localRes)) {
+						if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+							result.addAll(localRes);
+						}
+						writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet);
+						return false;
+					}
+				}
+				else {
+					Set<UnifyPair> localEq = new HashSet<>(); 
+					Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getAllSubstitutions());
+					unitedSubst.addAll(aPair.getAllBases());
+					unitedSubst.addAll(sameEq.getAllSubstitutions());
+					unitedSubst.addAll(sameEq.getAllBases());
+					localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
+					finalresult = false;
+					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0);
+					finalresult = true;
+					if (isUndefinedPairSetSet(localRes)) {
+						if (result.isEmpty() || isUndefinedPairSetSet(result)) {
+							result.addAll(localRes);
+						}
+						writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet);
+						return false;
+					}
+				}	
+			} 
+			writeLog("TRUE: " + aPair + "sameEqSet: " + sameEqSet);
+			return true;
+		}
+		return true;
+	}
+	
 	protected Boolean checkA (UnifyPair aPair, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> elems, Set<Set<UnifyPair>> result) {
 			writeLog("checkA: " + aPair + "sameEqSet: " + sameEqSet);
 			for (UnifyPair sameEq : sameEqSet) {