diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
index 42cd4835..7864ece1 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
@@ -23,6 +23,7 @@ import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
 import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
+import de.dhbwstuttgart.typeinference.unify.model.FunNType;
 import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
 import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
 import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
@@ -84,7 +85,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	Integer noAllErasedElements = 0;
 	
-	Integer noBacktracking = 0;
+	static int noBacktracking;
 	
 	public TypeUnifyTask() { 
 		rules = new RuleSet();
@@ -587,7 +588,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					//	ret = ret || x.stream().map(b -> b.getLhsType().equals(var)).reduce((c,d) -> c || d).get();
 					//}
 					return (!x.containsAll(durchschnitt));
-				})//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10
+				})//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) //fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10
 							.collect(Collectors.toCollection(ArrayList::new));
 				nofstred = nextSetasList.size();
 				//NOCH NICHT korrekt PL 2018-10-12
@@ -637,29 +638,74 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				if (((checkPair.getLhsType() instanceof PlaceholderType) || (checkPair.getRhsType() instanceof PlaceholderType)) 
 					&& (checkPair.getPairOp() == PairOperator.SMALLERDOT || checkPair.getPairOp() == PairOperator.SMALLERDOTWC))	
 				{
-					Set<UnifyPair> up = new HashSet<>();
-					up.add(checkPair);
-					Set<UnifyPair> undef = new HashSet<>();
-					calculatePairSets(up, fc, undef);
-					if (undef.isEmpty()) {
-						return true;
-					}
-					else {
-						writeLog("Second erase:" +checkPair.toString());
-						return false;
-					}
-				} else {
-				if 	((checkPair.getLhsType() instanceof ReferenceType) && (checkPair.getRhsType() instanceof ReferenceType)) 
-				//		&& (checkPair.getPairOp() == PairOperator.SMALLERDOT || checkPair.getPairOp() == PairOperator.SMALLERDOTWC)	
-				{
+					/*
 					Set<UnifyPair> setCheckPair = new HashSet<>();
 					setCheckPair.add(checkPair);
-					return isUndefinedPairSet(applyTypeUnificationRules(setCheckPair, fc));
+					Set<UnifyPair> setReturnCheckPair = applyTypeUnificationRules(setCheckPair, fc);
+					UnifyPair checkPair1 = setReturnCheckPair.iterator().next();
+					Set<UnifyPair> up = new HashSet<>();
+					up.add(checkPair1);
+					Set<UnifyPair> undef = new HashSet<>();
+					 */
+				PairOperator pairOp = checkPair.getPairOp();
+				UnifyType lhsType =  checkPair.getLhsType();
+				UnifyType rhsType =  checkPair.getRhsType();
+				///* Case 1: (a <. Theta')
+				if ((((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.SMALLERNEQDOT))  && lhsType instanceof PlaceholderType) 
+					// Case 2: (a <.? ? ext Theta')
+					|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)					
+					// Case 3: (a <.? ? sup Theta')
+					|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
+
+					// Case 4 was replaced by an inference rule
+					// Case 4: (a <.? Theta')
+					|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
+					// Case 5: (Theta <. a)
+					|| ((pairOp == PairOperator.SMALLERDOT) && rhsType instanceof PlaceholderType)
+					// Case 6 was replaced by an inference rule.
+					// Case 6: (? ext Theta <.? a)
+					|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
+					// Case 7 was replaced by an inference rule
+					// Case 7: (? sup Theta <.? a)
+					|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
+					// Case 8: (Theta <.? a)
+					|| (pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
+					//reduceWildcardLow
+					|| (pairOp == PairOperator.SMALLERDOTWC && (lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType))
+					//reduceWildcardLowRight
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof ExtendsType))
+					//reduceWildcardUp 
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && (rhsType instanceof SuperType))
+					//reduceWildcardUpRight
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof SuperType))
+					//reduceFunN
+					|| (((pairOp == PairOperator.SMALLERDOT)  || (pairOp == PairOperator.EQUALSDOT)) 
+				                                                               //PL 2017-10-03 hinzugefuegt  
+						                                                       //da Regel auch fuer EQUALSDOT anwendbar 
+						&& (lhsType instanceof FunNType) && (rhsType instanceof FunNType))
+					//greaterFunN
+					|| ((pairOp== PairOperator.SMALLERDOT) && (lhsType instanceof FunNType) && (rhsType instanceof PlaceholderType))
+					//smallerFunN
+					|| ((pairOp == PairOperator.SMALLERDOT) && (lhsType instanceof PlaceholderType && rhsType instanceof FunNType))
+					//reduceTph
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof PlaceholderType && rhsType instanceof ReferenceType))
+					//reduceTphExt
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ExtendsType) && rhsType instanceof PlaceholderType)
+					//reduceTphSup
+					|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && rhsType instanceof PlaceholderType)) {
+					return true;	
+				}
+				// Case unknown: If a pair fits no other case, then the type unification has failed.
+				// Through application of the rules, every pair should have one of the above forms.
+				// Pairs that do not have one of the aboves form are contradictory.
+				else {
+					writeLog("Second erase:" +checkPair.toString());
+					return false;
+				}
+				//*/
 				} else {
 					//Pair type <. ? extends ? extends type betrachten TODO PL 2018-10-09		
-				}
-				}
-			}
+				}}
 			return true;}).reduce((xx, yy) -> xx || yy).get();
 	}