diff --git a/src/de/dhbwstuttgart/core/JavaTXCompiler.java b/src/de/dhbwstuttgart/core/JavaTXCompiler.java
index 212dafad..5387e2a1 100644
--- a/src/de/dhbwstuttgart/core/JavaTXCompiler.java
+++ b/src/de/dhbwstuttgart/core/JavaTXCompiler.java
@@ -318,6 +318,9 @@ public class JavaTXCompiler {
 			});
 			Set<PlaceholderType> varianceTPHold;
 			Set<PlaceholderType> varianceTPH = new HashSet<>();
+			varianceTPH = varianceInheritanceConstraintSet(unifyCons);
+			
+			/* PL 2018-11-07 wird in varianceInheritanceConstraintSet erledigt
 			do { //PL 2018-11-05 Huellenbildung Variance auf alle TPHs der Terme auf der jeweiligen
 				 //anderen Seite übertragen
 				varianceTPHold = new HashSet<>(varianceTPH);
@@ -332,7 +335,9 @@ public class JavaTXCompiler {
 						} 
 					}
 					return y; } ); }	
-			while (!varianceTPHold.equals(varianceTPH));	
+			while (!varianceTPHold.equals(varianceTPH));
+			*/
+			
 			//Set<Set<UnifyPair>> result = unify.unifySequential(xConsSet, finiteClosure, logFile, log);
 			//Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure);
 			Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), unifyCons.getOderConstraints(), finiteClosure, logFile, log);
@@ -400,8 +405,8 @@ public class JavaTXCompiler {
 					x.getLhsType().accept(new distributeVariance(), a.getVariance());
 				}	
 				});
-			//phSetVariance =  new ArrayList<>(phSet); macht vermutlich keinen Sinn PL 2018-10-18
-			//phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x)));
+			phSetVariance =  new ArrayList<>(phSet); //macht vermutlich keinen Sinn PL 2018-10-18, doch, es koennen neue TPHs mit Variancen dazugekommen sein PL 2018-11-07
+			phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x)));
 		}
 		return usedTPH;
 	}
diff --git a/src/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java b/src/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java
index df57fa5e..e0666950 100644
--- a/src/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java
+++ b/src/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java
@@ -228,8 +228,14 @@ public class TYPEStmt implements StatementVisitor{
                 binary.operation.equals(BinaryExpr.Operator.ADD)||
                 binary.operation.equals(BinaryExpr.Operator.SUB)){
             Set<Constraint<Pair>> numericAdditionOrStringConcatenation = new HashSet<>();
-         - Auf importierte Typen einschraenken
-         - pruefen, ob die Typen richtig bestimmt werden.
+
+// TODO PL 2018-11-06
+            
+            //            Auf importierte Typen einschraenken
+            //         	 pruefen, ob  Typen richtig bestimmt werden.
+            
+
+            
             //Zuerst der Fall für Numerische AusdrücPairOpnumericeratorke, das sind Mul, Mod und Div immer:
             //see: https://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.17
             //Expression muss zu Numeric Convertierbar sein. also von Numeric erben
diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
index 5ee0a27d..aabd2792 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
@@ -74,7 +74,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	protected Set<UnifyPair> eq; //und-constraints
 	
-	protected List<Set<Set<UnifyPair>>> oderConstraints;
+	protected List<Set<Set<UnifyPair>>> oderConstraintsField;
 	
 	protected IFiniteClosure fc;
 	
@@ -109,7 +109,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	public TypeUnifyTask(Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log) {
 		this.eq = eq;
 		//this.oderConstraints = oderConstraints.stream().map(x -> x.stream().map(y -> new HashSet<>(y)).collect(Collectors.toSet(HashSet::new))).collect(Collectors.toList(ArrayList::new));
-		this.oderConstraints = oderConstraints.stream().map(x -> {
+		this.oderConstraintsField = oderConstraints.stream().map(x -> {
 			Set<Set<UnifyPair>> ret = new HashSet<>();
 			for (Constraint<UnifyPair> y : x) {
 				ret.add(new HashSet<>(y));
@@ -162,10 +162,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	protected Set<Set<UnifyPair>> compute() {
 		Set<UnifyPair> neweq = new HashSet<>(eq);
 		/* 1-elementige Oder-Constraints werden in und-Constraints umgewandelt */
-		oderConstraints.stream()
+		oderConstraintsField.stream()
         	.filter(x -> x.size()==1)
         	.map(y -> y.stream().findFirst().get()).forEach(x -> neweq.addAll(x));
-		ArrayList<Set<Set<UnifyPair>>> remainingOderconstraints = oderConstraints.stream()
+		ArrayList<Set<Set<UnifyPair>>> remainingOderconstraints = oderConstraintsField.stream()
 				.filter(x -> x.size()>1)
 				.collect(Collectors.toCollection(ArrayList::new));
 		Set<Set<UnifyPair>> res = unify(neweq, remainingOderconstraints, fc, parallel);
@@ -518,7 +518,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		Set<UnifyPair> undefinedPairs = new HashSet<>();
 		if (printtag) System.out.println("eq2s " + eq2s);
 		//writeLog("BufferSet: " + bufferSet.toString()+"\n");
-		Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs);
+		List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>(oderConstraints);
+		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
@@ -574,7 +575,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		
 		
 		//Aufruf von computeCartesianRecursive ANFANG
-		return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraints, fc, parallel);
+		return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel);
 	
 	}
 	
@@ -859,6 +860,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 							   .map(x -> x.getAllSubstitutions())
 							   .reduce((y,z) -> { y.addAll(z); return y;}).get())
 							   .reduce((y,z) -> { y.addAll(z); return y;}).get();
+				abhSubst.addAll(
+						res.stream()
+						   .map(b -> 
+						    b.stream()
+						   .map(x -> x.getAllBases())
+						   .reduce((y,z) -> { y.addAll(z); return y;}).get())
+						   .reduce((y,z) -> { y.addAll(z); return y;}).get()
+						);
 				Set<UnifyPair> b = a;//effective final a
 				Set<UnifyPair> durchschnitt = abhSubst.stream()
 						                              .filter(x -> b.contains(x))
@@ -1187,7 +1196,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>>> oderConstraints, IFiniteClosure fc, Set<UnifyPair> undefined) {
+	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) {
 		List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9);
 
 		// Init all 8 cases + 9. Case: oderConstraints
@@ -1207,7 +1216,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			}
 		}
 		if (eq2sAsList.isEmpty()) {
-			List<Set<Set<UnifyPair>>> oderConstraintsVariance = oderConstraints.stream() //Alle Elemente rauswerfen, die Variance 0 haben oder keine TPH in LHS oder RHS sind
+			List<Set<Set<UnifyPair>>> oderConstraintsVariance = oderConstraintsOutput.stream() //Alle Elemente rauswerfen, die Variance 0 haben oder keine TPH in LHS oder RHS sind
 			.filter(x -> x.stream()
 					.filter(y -> 
 						y.stream().filter(z -> ((z.getLhsType() instanceof PlaceholderType) 
@@ -1218,7 +1227,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					).findFirst().isPresent()).collect(Collectors.toList());
 			if (!oderConstraintsVariance.isEmpty()) {
 				Set<Set<UnifyPair>> ret = oderConstraintsVariance.get(0);
-				oderConstraints.remove(ret);
+				oderConstraintsOutput.remove(ret);
 				result.get(8).add(ret);
 				first = false;
 			}
@@ -1227,15 +1236,15 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		eq2sAsList.addAll(eq2s);
 		
 		if (eq2sAsList.isEmpty() && first) {//Alle eq2s sind empty und alle oderConstraints mit Variance != 0 sind bearbeitet 
-			if (!oderConstraints.isEmpty()) {
-				result.get(8).add(oderConstraints.remove(0));
+			if (!oderConstraintsOutput.isEmpty()) {
+				result.get(8).add(oderConstraintsOutput.remove(0));
 				first = false;
 			}
 		}
-		
-		- Bei allen die Abhaengigkeit der Elemente aus eq2sAsList als evtl. als Substitution 
+		/*
+		Bei allen die Abhaengigkeit der Elemente aus eq2sAsList als evtl. als Substitution 
 		  hinzufuegen 
-		
+		*/
 		for(UnifyPair pair : eq2sAsList) {
 			PairOperator pairOp = pair.getPairOp();
 			UnifyType lhsType = pair.getLhsType();
@@ -1245,6 +1254,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			if (((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.SMALLERNEQDOT))  && lhsType instanceof PlaceholderType) {
 				//System.out.println(pair);
 				if (first) { //writeLog(pair.toString()+"\n");
+					if (((PlaceholderType)(pair.getLhsType())).getName().equals("AR")) {
+						System.out.println("AR");
+					}
 					Set<Set<UnifyPair>> x1 = unifyCase1(pair, fc);
 					if (pairOp == PairOperator.SMALLERNEQDOT) {
 						Set<UnifyPair> remElem = new HashSet<>();
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
index d69138a7..729f7f4a 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
@@ -152,6 +152,15 @@ public class UnifyPair {
 		return ret;
 	}
 	
+	public Set<UnifyPair> getAllBases () {
+		Set<UnifyPair> ret = new HashSet<>();
+		if (basePair != null) {
+			ret.add(getBasePair());
+			ret.addAll(basePair.getAllBases());
+		}
+		return ret;
+	}
+	
 	public UnifyPair getGroundBasePair () {
 		if (basePair == null) {
 			return this;