//PL 2018-12-19: Merge checken
package de.dhbwstuttgart.typeinference.unify;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
import java.util.Optional;
import java.util.Set;
import java.util.concurrent.RecursiveTask;
import java.util.function.BiFunction;
import java.util.function.BinaryOperator;
import java.util.stream.Collectors;
import java.util.stream.Stream;

import org.apache.commons.io.output.NullOutputStream;

import de.dhbwstuttgart.exceptions.TypeinferenceException;
import de.dhbwstuttgart.parser.NullToken;
import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory;
import de.dhbwstuttgart.typeinference.constraints.Constraint;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.result.ResultSet;
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
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;
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
import de.dhbwstuttgart.typeinference.unify.model.WildcardType;
import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.Pair;

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.OutputStreamWriter;
import java.io.Writer;

import com.google.common.collect.Ordering;


/**
 * Implementation of the type unification algorithm
 * @author Florian Steurer
 */
public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {

	private static final long serialVersionUID = 1L;
	private static int i = 0;
	private boolean printtag = false;
	Boolean log = true; //gibt an ob ein Log-File nach System.getProperty("user.dir")+"/test/logFiles/log" geschrieben werden soll?
	
	/**
	 * Element, das aus dem nextSet den Gleichunen dieses Threads hinzugefuegt wurde
	 */
	Set<UnifyPair> nextSetElement;
	
	/**
	 * Fuer die Threads
	 */
	UnifyResultModel urm;
	protected static int noOfThread = 0;
	private static int totalnoOfThread = 0;
	int thNo;
	protected boolean one = false;
	Integer MaxNoOfThreads = 8;

	public static final String rootDirectory = System.getProperty("user.dir")+"/test/logFiles/";
	Writer logFile;

	/**
	 * The implementation of setOps that will be used during the unification
	 */
	protected ISetOperations setOps = new GuavaSetOperations();
	
	/**
	 * The implementation of the standard unify that will be used during the unification
	 */
	protected IUnify stdUnify = new MartelliMontanariUnify();
	
	/**
	 * The implementation of the rules that will be used during the unification.
	 */
	protected IRuleSet rules;
	
	protected Set<UnifyPair> eq; //und-constraints
	
	protected List<Set<Set<UnifyPair>>> oderConstraintsField;
	
	protected IFiniteClosure fc;
	
	protected Ordering<Set<UnifyPair>> oup;
	
	protected boolean parallel;
	
	int rekTiefeField;
	
	Integer nOfUnify = 0;
	
	Integer noUndefPair = 0;
	
	Integer noAllErasedElements = 0;
	
	static Integer noou = 0;
	
	static int noBacktracking;
	
	static Integer  noShortendElements = 0;
	
	Boolean myIsCanceled = false;
	
	volatile UnifyTaskModel usedTasks;
	
	public TypeUnifyTask() { 
		rules = new RuleSet();
	}
	
	/*
	public TypeUnifyTask(Set<UnifyPair> eq, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log) {
		this.eq = eq;
		this.fc = fc;
		this.oup = new OrderingUnifyPair(fc);
		this.parallel = parallel;
		this.logFile = logFile;
		this.log = log;
		rules = new RuleSet(logFile);
		noOfThread++;
		thNo = noOfThread;
	}
	*/
	

	public TypeUnifyTask(Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks) {
		synchronized (this) { 
			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.oderConstraintsField = oderConstraints; /*.stream().map(x -> {
			Set<Set<UnifyPair>> ret = new HashSet<>();
			for (Constraint<UnifyPair> y : x) {
				ret.add(new HashSet<>(y));
			}
			return ret;
			}).collect(Collectors.toCollection(ArrayList::new));
			 */
		
			//x.stream().map(y -> new HashSet<>(y)).collect(Collectors.toSet(HashSet::new))).collect(Collectors.toList(ArrayList::new));
			this.nextSetElement = nextSetElement;
			this.fc = fc;
			this.oup = new OrderingUnifyPair(fc);
			this.parallel = parallel;
			this.logFile = logFile;
			this.log = log;
			
			noOfThread++; 
			totalnoOfThread++;
			//writeLog("thNo1 " + thNo);
			thNo = totalnoOfThread;
			writeLog("thNo2 " + thNo);
			try {
				this.logFile = //new OutputStreamWriter(new NullOutputStream());
				//new FileWriter(new File(System.getProperty("user.dir")+"/src/test/resources/logFiles/"+"Thread_"+thNo));
				new FileWriter(new File(System.getProperty("user.dir")+"/logFiles/"+"Thread_"+thNo));
				logFile.write("");
			}
			catch (IOException e) { 
				System.err.println("log-File nicht vorhanden");
			}
			/*Abbruchtest
			if (thNo > 10) {
				System.out.println("cancel");
				usedTasks.cancel();
				writeLog(nOfUnify.toString() + "cancel");
				System.out.println("cancel");
			}
			*/
			rules = new RuleSet(logFile);
			this.rekTiefeField = rekTiefe;
			this.urm = urm;
			this.usedTasks = usedTasks;
			this.usedTasks.add(this);
		}
	}
	
	/**
	 * Vererbt alle Variancen
	 * @param eq The set of constraints
	 */
	/* PL 2018-05- 17 verschoben nach JavaTXCompiler
	private void varianceInheritance(Set<UnifyPair> eq) {
		Set<PlaceholderType> usedTPH = new HashSet<>();
		Set<PlaceholderType> phSet = eq.stream().map(x -> { 
			Set<PlaceholderType> pair = new HashSet<>();
			if (x.getLhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getLhsType());
			if (x.getRhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getRhsType());
			return pair;
		}).reduce(new HashSet<>(), (a,b) -> { a.addAll(b); return a;} , (c,d) -> { c.addAll(d); return c;});
		
		ArrayList<PlaceholderType> phSetVariance =  new ArrayList<>(phSet);
		phSetVariance.removeIf(x -> (x.getVariance() == 0));
		while(!phSetVariance.isEmpty()) {
			PlaceholderType a = phSetVariance.remove(0);
			usedTPH.add(a);
			//HashMap<PlaceholderType,Integer> ht = new HashMap<>();
			//ht.put(a, a.getVariance());
			Set<UnifyPair> eq1 = new HashSet<>(eq); 
			eq1.removeIf(x -> !(x.getLhsType() instanceof PlaceholderType && ((PlaceholderType)x.getLhsType()).equals(a)));
			eq1.stream().forEach(x -> { x.getRhsType().accept(new distributeVariance(), a.getVariance());});
			eq1 = new HashSet<>(eq); 
			eq1.removeIf(x -> !(x.getRhsType() instanceof PlaceholderType && ((PlaceholderType)x.getRhsType()).equals(a)));
			eq1.stream().forEach(x -> { x.getLhsType().accept(new distributeVariance(), a.getVariance());});
			phSetVariance =  new ArrayList<>(phSet);
			phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x)));
		}		
}
*/
	void myCancel(Boolean b) {
		myIsCanceled = true;
	}
	
	public boolean myIsCancelled() {
		return myIsCanceled;
	}
	
	protected Set<Set<UnifyPair>> compute() {
		if (one) {
			System.out.println("two");
		}
		one = true;
		Set<UnifyPair> neweq = new HashSet<>(eq);
		/* 1-elementige Oder-Constraints werden in und-Constraints umgewandelt */
		oderConstraintsField.stream()
        	.filter(x -> x.size()==1)
        	.map(y -> y.stream().findFirst().get()).forEach(x -> neweq.addAll(x));
		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, rekTiefeField, true);
		noOfThread--;
		try {
			logFile.close();
		}
		catch (IOException ioE) {
			System.err.println("no log-File");
		}
		if (isUndefinedPairSetSet(res)) { 
				throw new TypeinferenceException("Unresolved constraints: " + res.toString(), new NullToken()); //return new HashSet<>(); 
			}
		else {
			synchronized (usedTasks) {
				if (this.myIsCancelled()) {
					return new HashSet<>();
				}
				else {
					return res;
				}
			}
		}
	}
/*	
	@Override
	protected Set<Set<UnifyPair>> compute() {
		Set<Set<UnifyPair>> fstElems = new HashSet<>();
		fstElems.add(eq);
		Set<Set<UnifyPair>> res = computeCartesianRecursiveOderConstraints(fstElems, oderConstraints, fc, parallel);
		if (isUndefinedPairSetSet(res)) { return new HashSet<>(); }
		else return res;
	}
*/	



	
	/**
	 * Computes all principal type unifiers for a set of constraints.
	 * @param eq The set of constraints
	 * @param fc The finite closure
	 * @return The set of all principal type unifiers
	 */
	protected Set<Set<UnifyPair>> unify(final Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult)  {
		//Set<UnifyPair> aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT)
		//		).collect(Collectors.toCollection(HashSet::new));
		//writeLog(nOfUnify.toString() + " AA: " + aas.toString());
		//if (aas.isEmpty()) {
		//	System.out.println("");
		//}

                //.collect(Collectors.toCollection(HashSet::new)));
		/*
		 * Step 1: Repeated application of reduce, adapt, erase, swap 
		 */
		
		rekTiefe++;
		nOfUnify++;
        writeLog(nOfUnify.toString() + " Unifikation: " + eq.toString());
        writeLog(nOfUnify.toString() + " Oderconstraints: " + oderConstraints.toString());
		//eq = eq.stream().map(x -> {x.setVariance((byte)-1); return x;}).collect(Collectors.toCollection(HashSet::new));
		
		/*
		 * Variancen auf alle Gleichungen vererben
		 */
		//PL 2018-05-17 nach JavaTXCompiler verschoben
		//varianceInheritance(eq);
		
		/*
		 * ? extends ? extends Theta rausfiltern
		 */
		Set<UnifyPair> doubleExt = eq.stream().filter(x -> (x.wrongWildcard())).map(x -> { x.setUndefinedPair(); return x;})
				.collect(Collectors.toCollection(HashSet::new));
		if (doubleExt.size() > 0) {
			Set<Set<UnifyPair>> ret = new HashSet<>();
			ret.add(doubleExt);
			return ret;
		}
		
		Set<UnifyPair> eq0; 
		Set<UnifyPair> eq0Prime;
		Optional<Set<UnifyPair>> eqSubst = Optional.of(eq);
		do {
			eq0Prime = eqSubst.get();
			eq0 = applyTypeUnificationRules(eq0Prime, fc);
			eqSubst = rules.subst(eq0, oderConstraints);	
		} 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
		 */
		Set<UnifyPair> eq1s = new HashSet<>();
		Set<UnifyPair> eq2s = new HashSet<>();
		splitEq(eq0, eq1s, eq2s);
		
		/*
		 * Step 4: Create possible typings
		 * 
		 * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) 
		 * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
		 */
		
		// 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<UnifyPair>>> topLevelSets = new ArrayList<>();
		
		//System.out.println(eq2s);
		
		if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
			Set<Set<UnifyPair>> wrap = new HashSet<>();
			wrap.add(eq1s);
			topLevelSets.add(wrap); // Add Eq1'
		}

		// Add the set of [a =. Theta | (a=. Theta) in Eq2']
		//TODO: Occurscheck anwenden als Fehler identifizieren
		Set<UnifyPair> bufferSet = eq2s.stream() 
				.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
				.collect(Collectors.toSet());
		
		if(bufferSet.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
			Set<Set<UnifyPair>> wrap = new HashSet<>();
			wrap.add(bufferSet);
			topLevelSets.add(wrap);
			eq2s.removeAll(bufferSet);
		}
		
		// Sets that originate from pair pattern matching
		// Sets of the "second level"
		Set<UnifyPair> undefinedPairs = new HashSet<>();
		if (printtag) System.out.println("eq2s " + eq2s);
		//writeLog("BufferSet: " + bufferSet.toString()+"\n");
		List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>();//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
		                                                //Typen getestet werden.
		writeLog(nOfUnify.toString() + " Oderconstraints2: " + oderConstraintsOutput.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()) {
			noUndefPair++;
			for (UnifyPair up : undefinedPairs) {
				writeLog(noUndefPair.toString() + " UndefinedPairs; " + up);
				writeLog("BasePair; " + up.getBasePair());
			}
			Set<Set<UnifyPair>> error = new HashSet<>();
			undefinedPairs = undefinedPairs.stream().map(x -> { x.setUndefinedPair(); return x;}).collect(Collectors.toCollection(HashSet::new));
			error.add(undefinedPairs);
			undefinedPairs.forEach(x -> writeLog("AllSubst: " +x.getAllSubstitutions().toString()));
			return error;
		}
		
		/* Up to here, no cartesian products are calculated.
		 * filters for pairs and sets can be applied here */
		
		// Alternative: Sub cartesian products of the second level (pattern matched) sets
		// "the big (x)"
		/* for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
			//System.out.println("secondLevelSet "+secondLevelSet.size());
			List<Set<Set<UnifyPair>>> secondLevelSetList = new ArrayList<>(secondLevelSet);
			Set<List<Set<UnifyPair>>> cartResult = setOps.cartesianProduct(secondLevelSetList);
			//System.out.println("CardResult: "+cartResult.size());
			// Flatten and add to top level sets
			Set<Set<UnifyPair>> flat = new HashSet<>();
			int j = 0;
			for(List<Set<UnifyPair>> s : cartResult) {
				j++;
				//System.out.println("s from CardResult: "+cartResult.size() + " " + j);
				Set<UnifyPair> flat1 = new HashSet<>();
				for(Set<UnifyPair> s1 : s)
					flat1.addAll(s1);
				flat.add(flat1);
			}
			//topLevelSets.add(flat);
		}
		*/
		
		//Alternative KEIN KARTESISCHES PRODUKT der secondlevel Ebene bilden
		for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
			for (Set<Set<UnifyPair>> secondlevelelem : secondLevelSet) {
				topLevelSets.add(secondlevelelem);
			}
		}
		//System.out.println(topLevelSets);
		//System.out.println();
		
		
		//Aufruf von computeCartesianRecursive ANFANG
		//writeLog("topLevelSets: " + topLevelSets.toString());
		return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult);
	
	}
	
	
	Set<Set<UnifyPair>> unify2(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) {
		//Aufruf von computeCartesianRecursive ENDE
		
		//keine Ahnung woher das kommt
		//Set<Set<UnifyPair>> setToFlatten = topLevelSets.stream().map(x -> x.iterator().next()).collect(Collectors.toCollection(HashSet::new));
		
		//Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG
		// Cartesian product over all (up to 10) top level sets 
		//Set<Set<Set<UnifyPair>>> eqPrimeSet = setOps.cartesianProduct(topLevelSets)
		//		.stream().map(x -> new HashSet<>(x))
		//		.collect(Collectors.toCollection(HashSet::new));
		//Muss auskommentiert werden, wenn computeCartesianRecursive ENDE
		

		
		Set<Set<UnifyPair>> eqPrimePrimeSet = new HashSet<>();
		
		Set<TypeUnifyTask> forks = new HashSet<>();
		
		//Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG
		//for(Set<Set<UnifyPair>> setToFlatten : eqPrimeSet) {
			// Flatten the cartesian product
		//Muss auskommentiert werden, wenn computeCartesianRecursive ENDE
			Set<UnifyPair> eqPrime = new HashSet<>();
			setToFlatten.stream().forEach(x -> eqPrime.addAll(x));

			/*
			 * Step 5: Substitution
			 */
			//writeLog("vor Subst: " + eqPrime);
			writeLog("vor Subst: " + oderConstraints);
			String ocString = oderConstraints.toString();
			List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
			Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime, newOderConstraints);
			Set<Set<UnifyPair>> unifyres1 = null;
			Set<Set<UnifyPair>> unifyres2 = null;
			if (!ocString.equals(newOderConstraints.toString())) writeLog("nach Subst: " + newOderConstraints);
			//writeLog("nach Subst: " + eqPrimePrime);
			/*
			 * Step 6 a) Restart (fork) for pairs where subst was applied
			 */
			/*
			if(parallel) {
				if (eqPrime.equals(eq) && !eqPrimePrime.isPresent()
				    && oderConstraints.isEmpty())         				    //PL 2017-09-29 //(!eqPrimePrime.isPresent()) auskommentiert und durch 
				                              								//PL 2017-09-29 dies ersetzt //(!eqPrimePrime.isPresent()) 
																			//PL 2018-05-18 beide Bedingungen muessen gelten, da eqPrime Veränderungen in allem ausser subst
																			//eqPrimePrime Veraenderungen in subst repraesentieren.
					eqPrimePrimeSet.add(eqPrime);
				else if(eqPrimePrime.isPresent()) {
					//System.out.println("nextStep: " + eqPrimePrime.get());
					TypeUnifyTask fork = new TypeUnifyTask(eqPrimePrime.get(), fc, true, logFile, log);
					forks.add(fork);
					fork.fork();
				}
				else {
					//System.out.println("nextStep: " + eqPrime);
					TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc, true, logFile, log);
					forks.add(fork);
					fork.fork();
				}
			}
			else */
			{// sequentiell (Step 6b is included)
				if (printtag) System.out.println("nextStep: " + eqPrimePrime);
				if (eqPrime.equals(eq) && !eqPrimePrime.isPresent()
					&& oderConstraints.isEmpty()) {        					  //PL 2017-09-29 //(!eqPrimePrime.isPresent()) auskommentiert und durch 
																			  //PL 2017-09-29 dies ersetzt //(!eqPrimePrime.isPresent()) 
																			  //PL 2018-05-18 beide Bedingungen muessen gelten, da eqPrime Veränderungen in allem ausser subst
																			  //eqPrimePrime Veraenderungen in subst repraesentieren.
					//try {
						//if (isSolvedForm(eqPrime)) {
						//	writeLog("eqPrime:" + eqPrime.toString()+"\n");
						//}
					//}
					//catch (IOException e) { 
					//	System.err.println("log-File nicht vorhanden");
					//}
					eqPrimePrimeSet.add(eqPrime);
					if (finalresult && isSolvedForm(eqPrime)) { 
						writeLog("eqPrime:" + eqPrime.toString()+"\n");
						urm.notify(eqPrimePrimeSet);
					}
				}
				else if(eqPrimePrime.isPresent()) {
					Set<Set<UnifyPair>> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe, finalresult);
					
					eqPrimePrimeSet.addAll(unifyres);
				}
				else {
					Set<Set<UnifyPair>> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe, finalresult);
					
					
					eqPrimePrimeSet.addAll(unifyres);
				}
			}
		//Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG
		//}
		//Muss auskommentiert werden, wenn computeCartesianRecursive ENDE
		
		/*
		 * 	Step 6 b) Build the union over everything.
		 */
		/*
		 * PL 2019-01-22: geloescht
		
		if(parallel)
			for(TypeUnifyTask fork : forks) 
				eqPrimePrimeSet.addAll(fork.join());
		*/
		 /*
		  * Step 7: Filter empty sets;
		  */
		eqPrimePrimeSet = eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x) || this.isUndefinedPairSet(x)).collect(Collectors.toCollection(HashSet::new));
		if (!eqPrimePrimeSet.isEmpty() && !isUndefinedPairSetSet(eqPrimePrimeSet)) {
			writeLog("Result1 " + eqPrimePrimeSet.toString());
		}
		return eqPrimePrimeSet;
	}
	
	
	
	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)
				                    .map(y -> y.stream().findFirst().get())
				                    .collect(Collectors.toCollection(HashSet::new)));
		ArrayList<Set<Set<UnifyPair>>> remainingSets = topLevelSets.stream()
				                                                   .filter(x -> x.size()>1)
				                                                   .collect(Collectors.toCollection(ArrayList::new));
		if (remainingSets.isEmpty()) {//Alle Elemente sind 1-elementig
			Set<Set<UnifyPair>> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe, finalresult);
			return result;
		}
		Set<Set<UnifyPair>> nextSet = remainingSets.remove(0);
		writeLog("nextSet: " + nextSet.toString());
		List<Set<UnifyPair>> nextSetasList =new ArrayList<>(nextSet);
		try {
		//List<Set<UnifyPair>> 
			//nextSetasList = oup.sortedCopy(nextSet);//new ArrayList<>(nextSet);
		}
		catch (java.lang.IllegalArgumentException e) {
			System.out.print("");
		}
		Set<Set<UnifyPair>> result = new HashSet<>(); 
		int variance = 0;
		
		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++) {
		//		al.add(0,nextSetasList.get(ii));
		//	}
		//	nextSetasList = al;
		//}
		//Set<UnifyPair> a = nextSetasListIt.next();
		/*if (nextSetasList.size()>1) {zu loeschen
			if (nextSetasList.iterator().next().iterator().next().getLhsType().getName().equals("D")) 
				System.out.print("");
			if (variance == 1) {
				a_next = oup.max(nextSetasList.iterator());
			}
			else if (variance == -1) {
				a_next = oup.min(nextSetasList.iterator());
			}
			else if (variance == 0) {
				a_next = nextSetasList.iterator().next();
			}
		}
		else {
			a_next = nextSetasList.iterator().next();
		}
		*/
		if (!nextSetasList.iterator().hasNext())
			System.out.print("");
		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 */
		Set<UnifyPair> sameEqSet = new HashSet<>();
		if (variance != 2) {
			Optional<UnifyPair> optOrigPair = nextSetElem.stream().filter(x -> (
					//x.getBasePair() != null && ist gegeben wenn variance != 2
					//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())
                */		
                ))).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();
			writeLog("optOrigPair: " + optOrigPair);
			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() instanceof PlaceholderType)) 
							|| (x.getRhsType().equals(tyVarEF) && !(x.getLhsType() instanceof PlaceholderType)))))
					.collect(Collectors.toCollection(HashSet::new));
			}
		}
		/* sameEqSet-Bestimmung Ende */
		
		Set<UnifyPair> a = null;
		while (nextSetasList.size() > 0) {  //(nextSetasList.size() != 0) {
			Set<UnifyPair> a_last = a;
			List<Set<UnifyPair>> nextSetasListRest = new ArrayList<>();
			//List<Set<UnifyPair>> nextSetasListRestMin = new ArrayList<>();
			//List<Set<UnifyPair>> nextSetasListRestOder = new ArrayList<>();
			if (variance == 1) {
				a = oup.max(nextSetasList.iterator());
				nextSetasList.remove(a);
				nextSetasListRest = new ArrayList<>(nextSetasList);
				Iterator<Set<UnifyPair>> nextSetasListItRest = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
				while (nextSetasListItRest.hasNext()) {
					Set<UnifyPair> a_next = nextSetasListItRest.next();
					if (//a.equals(a_next) || 
							(oup.compare(a, a_next) == 1)) {
						nextSetasListRest.remove(a_next);
					}
				}
				//Alle maximale Elemente in  nextSetasListRest bestimmen
				List<Set<UnifyPair>> nextSetasListRestTest;
				do {
					nextSetasListRestTest = new ArrayList<Set<UnifyPair>>(nextSetasListRest);
					if (!nextSetasListRest.isEmpty()) {
						Set<UnifyPair> max = oup.max(nextSetasListRest.iterator());
						Iterator<Set<UnifyPair>> nextSetasListItRest2 = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
						while (nextSetasListItRest2.hasNext()) {
							Set<UnifyPair> a_nextRest = nextSetasListItRest2.next();
							if (//a.equals(a_next) || 
									(oup.compare(max, a_nextRest) == 1)) {
								nextSetasListRest.remove(a_nextRest);
							}
						
						}}
				} while(!nextSetasListRestTest.equals(nextSetasListRest));
				
			}
			else if (variance == -1) {
				a = oup.min(nextSetasList.iterator());
				nextSetasList.remove(a);
				nextSetasListRest = new ArrayList<>(nextSetasList);
				Iterator<Set<UnifyPair>> nextSetasListItRest = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
				while (nextSetasListItRest.hasNext()) {
					Set<UnifyPair> a_next = nextSetasListItRest.next();
					if (//a.equals(a_next) || 
							(oup.compare(a, a_next) == -1)) {
						nextSetasListRest.remove(a_next);
					}
				}
				//Alle minimalen Elemente in  nextSetasListRest bestimmen
				
					List<Set<UnifyPair>> nextSetasListRestTest;
					do {
						nextSetasListRestTest = new ArrayList<Set<UnifyPair>>(nextSetasListRest);
						if (!nextSetasListRest.isEmpty()) {
							Set<UnifyPair> min = oup.min(nextSetasListRest.iterator());
							Iterator<Set<UnifyPair>> nextSetasListItRest2 = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
							while (nextSetasListItRest2.hasNext()) {
								Set<UnifyPair> a_nextRest = nextSetasListItRest2.next();
								if (//a.equals(a_next) || 
										(oup.compare(min, a_nextRest) == -1)) {
									nextSetasListRest.remove(a_nextRest);
								}
						
							}}
					} while(!nextSetasListRestTest.equals(nextSetasListRest));
			}
			else if (variance == 2) {
				a = nextSetasList.remove(0);
				nextSetasListRest = new ArrayList<>(nextSetasList);
			} 
			else if (variance == 0) {
				a = nextSetasList.remove(0);
			}
			//writeLog("nextSet: " + nextSetasList.toString()+ "\n");
			//nextSetasList.remove(a);
			/* zu loeschen
			if (nextSetasList.size() > 0) {
				if (nextSetasList.size()>1) {
					if (variance == 1) {
						a_next = oup.max(nextSetasList.iterator());
					}
					else if (variance == -1) {
						a_next = oup.min(nextSetasList.iterator());
					}
					else {
						a_next = nextSetasList.iterator().next();
					}
				}
				else {
					a_next = nextSetasList.iterator().next();
				}
			}
			*/
			//PL 2018-03-01
			//TODO: 1. Maximum und Minimum unterscheiden
			//TODO: 2. compare noch für alle Elmemente die nicht X =. ty sind erweitern 
		//for(Set<UnifyPair> a : newSet) {
			i++;
			Set<Set<UnifyPair>> elems = new HashSet<Set<UnifyPair>>(fstElems);
			writeLog("a1: " + rekTiefe + "  "+ "variance:  "+ variance + " " + a.toString()+ "\n");
			//elems.add(a); PL 2019-01-20 Muss weg, weil das in jeweiligen Thread erfolgen muss. Fuer den sequentiellen Fall 
			//im else-Zweig
			//if (remainingSets.isEmpty()) {//muss immer gegeben sein, weil nur 1 Element der topLevelSets mehr als ein Elemet enthaelt
				//writeLog("Vor unify2 Aufruf: " + elems.toString());
			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 */
			if (variance != 2 && !sameEqSet.isEmpty()) {
				Optional<UnifyPair> optAPair = a.stream().filter(x -> (
						//x.getBasePair() != null && ist gegeben wenn variance != 2
						//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())
	                */		
	                ))).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("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
					if (!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);
				Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
				List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
				newElemsOrig.add(a);
				
				/* FORK ANFANG */
				TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
				//forks.add(forkOrig);
				synchronized(usedTasks) {
					if (this.myIsCancelled()) {
						return new HashSet<>();
					}
					forkOrig.fork();
				}
				/* FORK ENDE */
				
				synchronized (this) {
					writeLog("a in " + variance + " "+ a);
					writeLog("nextSetasListRest: " + nextSetasListRest.toString());
				}
				while (!nextSetasListRest.isEmpty()) {
					Set<UnifyPair> nSaL = nextSetasListRest.remove(0);
					synchronized (this) { nextSetasList.remove(nSaL);
						writeLog("1 RM" + nSaL.toString());
					}
					
					/* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
					Optional<UnifyPair> optAPair = nSaL.stream().filter(x -> (
							//x.getBasePair() != null && ist gegeben wenn variance != 2
							//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())
		                */		
		                ))).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("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
						if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
							nSaL = null;
							noShortendElements++;
							continue;
						}
					}
					/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
					
					Set<UnifyPair> newEq = new HashSet<>(eq);
					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
					newElems.add(nSaL);
					TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
					forks.add(fork);
					synchronized(usedTasks) {
						if (this.myIsCancelled()) {
							return new HashSet<>();
						}
						fork.fork();
					}
				}
				//res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe);
				
				/* FORK ANFANG */
				synchronized (this) {
					noOfThread--;
					writeLog("wait "+ forkOrig.thNo);
					res = forkOrig.join();
					forkOrig.writeLog("final Orig 1");
					forkOrig.closeLogFile();
					//Set<Set<UnifyPair>> fork_res = forkOrig.join();
					writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString());
					//noOfThread--; an das Ende von compute verschoben 
					//add_res.add(fork_res);
				};
				/* FORK ENDE */
				
				forks.forEach(x -> writeLog("wait: " + x.thNo));
				for(TypeUnify2Task fork : forks) {
					synchronized (this) {
						Set<Set<UnifyPair>> fork_res = fork.join();
						writeLog("Join " + new Integer(fork.thNo).toString());
						//noOfThread--; an das Ende von compute verschoben
						writeLog("fork_res: " + fork_res.toString());
						writeLog(new Boolean((isUndefinedPairSetSet(fork_res))).toString());
						add_res.add(fork_res);
						if (!isUndefinedPairSetSet(fork_res)) {
							aParDef.add(fork.getNextSetElement());
						}
						fork.writeLog("final 1");
						fork.closeLogFile();
					};
				}
				noOfThread++;
			} else {
			if(parallel && (variance == -1) && noOfThread <= MaxNoOfThreads) {
				Set<TypeUnify2Task> forks = new HashSet<>();
				Set<UnifyPair> newEqOrig = new HashSet<>(eq);
				Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
				List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
				newElemsOrig.add(a);
				
				/* FORK ANFANG */
				TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
				//forks.add(forkOrig);
				synchronized(usedTasks) {
					if (this.myIsCancelled()) {
						return new HashSet<>();
					}
					forkOrig.fork();
				}
				/* FORK ENDE */
				
				synchronized (this) {
					writeLog("a in " + variance + " "+ a);
					writeLog("nextSetasListRest: " + nextSetasListRest.toString());
				}
				while (!nextSetasListRest.isEmpty()) {
					Set<UnifyPair> nSaL = nextSetasListRest.remove(0);
					synchronized (this) { nextSetasList.remove(nSaL);
						writeLog("-1 RM" + nSaL.toString());
					}
					
					/* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
					Optional<UnifyPair> optAPair = nSaL.stream().filter(x -> (
							//x.getBasePair() != null && ist gegeben wenn variance != 2
							//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())
		                */		
		                ))).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("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
						if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
							nSaL = null;
							noShortendElements++;
							continue;
						}
					}
					/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
					
					Set<UnifyPair> newEq = new HashSet<>(eq);
					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
					newElems.add(nSaL);
					TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
					forks.add(fork);
					synchronized(usedTasks) {
						if (this.myIsCancelled()) {
							return new HashSet<>();
						}
						fork.fork();
					}
				}
				//res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe);
				
				/* FORK ANFANG */
				synchronized (this) {
					noOfThread--;
					writeLog("wait "+ forkOrig.thNo);
					res = forkOrig.join();
					forkOrig.writeLog("final Orig -1");
					forkOrig.closeLogFile();
					//Set<Set<UnifyPair>> fork_res = forkOrig.join();
					writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString());
					//noOfThread--; an das Ende von compute verschoben 
					//add_res.add(fork_res);
				};
				/* FORK ENDE */
				
				forks.forEach(x -> writeLog("wait: " + x.thNo));
				for(TypeUnify2Task fork : forks) {
					synchronized (this) {
						Set<Set<UnifyPair>> fork_res = fork.join();
						writeLog("Join " + new Integer(fork.thNo).toString());
						//noOfThread--; an das Ende von compute verschoben 
						writeLog("fork_res: " + fork_res.toString());
						writeLog(new Boolean((isUndefinedPairSetSet(fork_res))).toString());
						add_res.add(fork_res);
						if (!isUndefinedPairSetSet(fork_res)) {
							aParDef.add(fork.getNextSetElement());
						}
						fork.writeLog("final -1");
						fork.closeLogFile();
					};
				}
				noOfThread++;
		    } else {
		    if(parallel && (variance == 2) && noOfThread <= MaxNoOfThreads) {
		    	writeLog("var2einstieg");
		    	Set<TypeUnify2Task> forks = new HashSet<>();
		    	Set<UnifyPair> newEqOrig = new HashSet<>(eq);
		    	Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
		    	List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
		    	newElemsOrig.add(a);
				
				/* FORK ANFANG */
		    	TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
		    	//forks.add(forkOrig);
		    	synchronized(usedTasks) {
					if (this.myIsCancelled()) {
						return new HashSet<>();
					}
					forkOrig.fork();
		    	}
		    	/* FORK ENDE */
		    	
		    	synchronized (this) {
					writeLog("a in " + variance + " "+ a);
					writeLog("nextSetasListRest: " + nextSetasListRest.toString());
				}
		    	while (!nextSetasListRest.isEmpty()) {
		    		Set<UnifyPair> nSaL = nextSetasListRest.remove(0);
		    		//nextSetasList.remove(nSaL);
		    		Set<UnifyPair> newEq = new HashSet<>(eq);
		    		Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
		    		List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
		    		newElems.add(nSaL);
		    		TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
		    		forks.add(fork);
		    		synchronized(usedTasks) {
						if (this.myIsCancelled()) {
							return new HashSet<>();
						}
						fork.fork();
		    		}
		    	}
		    	//res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe);
		    	
		    	/* FORK ANFANG */
		    	synchronized (this) {
		    		noOfThread--;
		    		writeLog("wait "+ forkOrig.thNo);
					res = forkOrig.join();
					forkOrig.writeLog("final Orig 2");
					forkOrig.closeLogFile();
					//Set<Set<UnifyPair>> fork_res = forkOrig.join();
					writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString());
					//noOfThread--; an das Ende von compute verschoben 
					//add_res.add(fork_res); //vermutlich falsch
				};
				/* FORK ENDE */
		    	forks.forEach(x -> writeLog("wait: " + x.thNo));
		    	for(TypeUnify2Task fork : forks) {
		    		synchronized (this) {
						Set<Set<UnifyPair>> fork_res = fork.join();
						writeLog("Join " + new Integer(fork.thNo).toString());
						//noOfThread--; an das Ende von compute verschoben 
						add_res.add(fork_res);
						fork.writeLog("final 2");
						fork.closeLogFile();
					};
				} 
		    	noOfThread++;	
		    } else {
		    	//parallel = false; //Wenn MaxNoOfThreads erreicht ist, 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, finalresult);
			}}}
				if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) {
					//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
					result = res;
				}
				else { 
					if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result))
					    || (!isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result))
					    || result.isEmpty()) {
						
						if ((!result.isEmpty() && !res.isEmpty() && !isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result)) //korrekte Loesungen aus und-constraints
							&& (a.stream().map(x-> (x.getBasePair() != null)).reduce(true, (x, y) -> (x && y)))) //bei oder-Constraints nicht ausfuehren
						{
							//TODO: PL 2019-01-15: Bug 129: Im Moment wird nur das Maximum und das Minimum des aktuellen Elements betrachtet.
							//Die zu vereinigenden Mengen können mehrere Elemente enthalten. Das ist bisher nicht berücksichtigt
							
							//Alle Variablen bestimmen die nicht hinzugefügt wurden in a
							//PL 2018-12-28: Hier gab es eine ClassCastException, war nicht reproduzierbar
							System.out.println("");
							List<PlaceholderType> vars_a = 
									a.stream().filter(x -> ((x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName())
															&& (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getLhsType() instanceof PlaceholderType))
														|| ((x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName()))
															&& (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getRhsType() instanceof PlaceholderType)))
											)
									.map(y -> (PlaceholderType)y.getLhsType()).collect(Collectors.toCollection(ArrayList::new));
							Set<UnifyPair> fstElemRes = res.iterator().next();
							Set<UnifyPair> compRes = fstElemRes.stream().filter(x -> vars_a.contains(((PlaceholderType)x.getLhsType()))).collect(Collectors.toCollection(HashSet::new));
						
							//Alle Variablen bestimmen die nicht hinzugefügt wurden in a_last
							//System.out.println(a_last);
							
							try {//PL eingefuegt 2019-03-06 da bei map mmer wieder Nullpointer kamen
							a_last.forEach(x -> {writeLog("a_last_elem:" + x + " basepair: " + x.getBasePair());});//PL 2019-05-13 ins try hinzugefuegt Nullpointer-Exception ist in der Zeile aufgetaucht.
							List<PlaceholderType> varsLast_a = 
									a_last.stream().filter(x -> ((x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName())
																 && (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getLhsType() instanceof PlaceholderType))
															|| ((x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())))
																&& (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getRhsType() instanceof PlaceholderType)))
									.map(y -> (PlaceholderType)y.getLhsType()).collect(Collectors.toCollection(ArrayList::new));
							//[(java.util.Vector<java.lang.Integer> <. gen_aq, , 1), (CEK =. ? extends gen_aq, 1)] KANN VORKOMMEN
							//erstes Element genügt, da vars immer auf die gleichen Elemente zugeordnet werden muessen
							Set<UnifyPair> fstElemResult = result.iterator().next();
							Set<UnifyPair> compResult = fstElemResult.stream().filter(x -> varsLast_a.contains(((PlaceholderType)x.getLhsType()))).collect(Collectors.toCollection(HashSet::new));; 
							if (variance == 1) {
								writeLog("a_last:" + a_last + " a: " + a);
								writeLog("varsLast_a:" + varsLast_a + " vars_a: " + vars_a);
								writeLog("compResult:" + compResult + " compRes: " + compRes);
								int resOfCompare = oup.compare(compResult, compRes);
								if (resOfCompare == -1) {
									writeLog("Geloescht result: " + result);
									result = res;
								} else { 
								if  (resOfCompare == 0) {
									result.addAll(res);
							    } //else { 
								if  (resOfCompare == 1) {
									writeLog("Geloescht res: " + res);	
									//result = result;
								}}}
							else { if (variance == -1) {
								writeLog("a_last:" + a_last + " a: " + a);
								writeLog("varsLast_a:" + varsLast_a + " vars_a: " + vars_a);
								writeLog("compResult:" + compResult + " compRes: " + compRes);
								int resOfCompare = oup.compare(compResult, compRes);
								if (resOfCompare == 1) {
									writeLog("Geloescht result: " + result);
									result = res;
								} else { 
								if  (resOfCompare == 0) {
									result.addAll(res);
								} else { 
								if  (resOfCompare == -1) {
									writeLog("Geloescht res: " + res);	
									//result = result;
								}}}}
							else { if (variance == 0) {
								writeLog("RES var=1 ADD:" + result.toString() + " " + res.toString());
								result.addAll(res);
							}}}	
							}
							catch (NullPointerException e) {
								writeLog("NullPointerException: " + a_last.toString());
							}
						}
						else {
							//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
							writeLog("RES Fst: reuslt: " + result.toString() + " res: " + res.toString());
							result.addAll(res);
						}
						}
					//else {
					  //wenn Korrekte Ergebnisse da und Feherfälle dazukommen Fehlerfälle ignorieren
					//	if (isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result)) {
					//		result = result;
					//	}
					//}
				}
				
			//}
			//else {//duerfte gar nicht mehr vorkommen PL 2018-04-03
				//result.addAll(computeCartesianRecursive(elems, remainingSets, eq, fc, parallel)); 
			//}
				if (parallel) {
					for (Set<Set<UnifyPair>> par_res : add_res) {
						if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) {
							//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
							result = par_res;
							if (par_res.iterator().next() instanceof WildcardType) {
								System.out.println("");
							}
						}
						else { 
							if ((isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result))
									|| (!isUndefinedPairSetSet(par_res) && !isUndefinedPairSetSet(result))
									|| result.isEmpty()) {
								//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
								writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString());
								result.addAll(par_res);
							}
						}
					}
					//break;
				}
				
			/* auskommentiert um alle Max und min Betrachtung auszuschalten ANFANG */
			if (!result.isEmpty() && (!isUndefinedPairSetSet(res) || !aParDef.isEmpty())) {
				if (nextSetasList.iterator().hasNext() && nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("B")).findFirst().isPresent() && nextSetasList.size()>1) 
					System.out.print("");
				Iterator<Set<UnifyPair>> nextSetasListIt = new ArrayList<Set<UnifyPair>>(nextSetasList).iterator();
				if (variance == 1) {
					/* vorgezogen vor das if
					if (parallel) {
						for (Set<Set<UnifyPair>> par_res : add_res) {
							if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) {
								//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
								result = par_res;
								if (par_res.iterator().next() instanceof WildcardType) {
									System.out.println("");
								}
							}
							else { 
								if ((isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result))
										|| (!isUndefinedPairSetSet(par_res) && !isUndefinedPairSetSet(result))
										|| result.isEmpty()) {
									//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
									writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString());
									result.addAll(par_res);
								}
							}
						}
						//break;
						*/
					
					/* nextSetasList = nextSetasListRest; */
					/* wird bereits vor den unify2-Aufruf durchgefuehrt und nextSetasListRest zugeordnet
					*/

					System.out.println("");
					writeLog("a: " + rekTiefe + " variance: " + variance + a.toString());
					writeLog("aParDef: " + aParDef.toString());
					aParDef.add(a);
					Iterator<Set<UnifyPair>> aParDefIt = aParDef.iterator();
					while(aParDefIt.hasNext()) {
						Set<UnifyPair> a_new = aParDefIt.next();
						while (nextSetasListIt.hasNext()) {
							Set<UnifyPair> a_next = nextSetasListIt.next();
							if (a_new.equals(a_next) || 
									(oup.compare(a_new, a_next) == 1)) {
								writeLog("Removed: " + a_next.toString());
								nextSetasList.remove(a_next);
							}
							else { 
								writeLog("Not Removed: " + a_next.toString());
								System.out.println("");
							}
						}
					}	
				}
				else { if (variance == -1) {
					/* vorgezogen vor das if
					if (parallel) {
						for (Set<Set<UnifyPair>> par_res : add_res) {
							if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) {
								//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
								result = par_res;
								if (par_res.iterator().next() instanceof WildcardType) {
									System.out.println("");
								}
							}
							else { 
								if ((isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result))
										|| (!isUndefinedPairSetSet(par_res) && !isUndefinedPairSetSet(result))
										|| result.isEmpty()) {
									//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
									writeLog("RES var-1 ADD:" + result.toString() + " " + par_res.toString());
									result.addAll(par_res);
								}
							}
						}
						//break;	
					}
				
				}
				*/	
					
					System.out.println("");
					writeLog("a: " + rekTiefe + " variance: " + variance + a.toString());
					writeLog("aParDef: " + aParDef.toString());
					aParDef.add(a);
					Iterator<Set<UnifyPair>> aParDefIt = aParDef.iterator();
					while(aParDefIt.hasNext()) {
						Set<UnifyPair> a_new = aParDefIt.next();
						while (nextSetasListIt.hasNext()) {
							Set<UnifyPair> a_next = nextSetasListIt.next();
							if (a_new.equals(a_next) || 
									(oup.compare(a_new, a_next) == -1)) {
								writeLog("Removed: " + a_next.toString());
								nextSetasList.remove(a_next); //PL geaendert 2019-01-09
							}
							else { 
								System.out.println("");
								writeLog("Not Removed: " + a_next.toString());
						}
					}
				}
				}
				else { if (variance == 0) {
					writeLog("a: " + rekTiefe + " variance: " + variance + a.toString());
					break; } 
				else { if (variance == 2) {
					/* vorgezogen vor das if
					if (parallel) {
						for (Set<Set<UnifyPair>> par_res : add_res) {
							if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) {
								//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
								result = par_res;
								if (par_res.iterator().next() instanceof WildcardType) {
									System.out.println("");
								}
							}
							else { 
								if ((isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result))
										|| (!isUndefinedPairSetSet(par_res) && !isUndefinedPairSetSet(result))
										|| result.isEmpty()) {
									//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
									writeLog("RES var2 ADD:" + result.toString() + " " + par_res.toString());
									result.addAll(par_res);
								}
							}
						}
						//break;
					}
					*/
				}}}
				writeLog("a: " + rekTiefe + " variance: " + variance + a.toString());
				}
			}
			 /* auskommentiert um alle Max und min Betrachtung auszuschalten ENDE */ 
			
			if (isUndefinedPairSetSet(res) && aParDef.isEmpty()) {
				int nofstred= 0;
				Set<UnifyPair> abhSubst = res.stream()
							   .map(b -> 
							    b.stream()
							   .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))
						                              //.filter(y -> abhSubst.contains(y))
						                              .collect(Collectors.toCollection(HashSet::new));
				//Set<PlaceholderType> vars = durchschnitt.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new));
				int len = nextSetasList.size();
				Set<UnifyPair> undefRes = res.stream().reduce((y,z) -> { y.addAll(z); return y;}).get(); //flatten aller undef results
				Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair = undefRes.stream()
						.map(x -> { Set<UnifyPair> su = x.getAllSubstitutions(); //alle benutzten Substitutionen
									su.add(x.getGroundBasePair());  // urspruengliches Paar
									su.removeAll(durchschnitt); //alle aktuell genänderten Paare entfernen
									return new Pair<>(su, x.getGroundBasePair());})
						.collect(Collectors.toCollection(HashSet::new));
				if (res.size() > 1) {
					System.out.println();
				}
				nextSetasList = nextSetasList.stream().filter(x -> {
					//Boolean ret = false;
					//for (PlaceholderType var : vars) {
					//	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
							.collect(Collectors.toCollection(ArrayList::new));
				nofstred = nextSetasList.size();
				//NOCH NICHT korrekt PL 2018-10-12
				//nextSetasList = nextSetasList.stream().filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y))
				//			.collect(Collectors.toCollection(ArrayList::new));
				writeLog("res (undef): " + res.toString());
				writeLog("abhSubst: " + abhSubst.toString());
				writeLog("a2: " + rekTiefe + " " + a.toString());
				writeLog("Durchschnitt: " + durchschnitt.toString());
				writeLog("nextSet: " + nextSet.toString());
				writeLog("nextSetasList: " + nextSetasList.toString());
				writeLog("Number first erased Elements (undef): " + (len - nofstred));
				writeLog("Number second erased Elements (undef): " + (nofstred- nextSetasList.size()));
				writeLog("Number erased Elements (undef): " + (len - nextSetasList.size()));
				noAllErasedElements = noAllErasedElements + (len - nextSetasList.size());
				writeLog("Number of all erased Elements (undef): " + noAllErasedElements.toString());
				noBacktracking++;
				writeLog("Number of Backtracking: " + noBacktracking);
				System.out.println("");
			}
			//if (nextSetasList.size() == 0 && isUndefinedPairSetSet(result) && nextSet.size() > 1) { 
			//	return result;
			//}
			//else {
			//	result.removeIf(y -> isUndefinedPairSet(y));
			//}
			//else result.stream().filter(y -> !isUndefinedPairSet(y));
			writeLog("res: " + res.toString());
		}
		
		writeLog("Return computeCR: " + result.toString());
		return result;
	}
	
	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) {
				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));
					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
					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));
					Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
					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;
	}
	
	protected boolean couldBecorrect(Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set<UnifyPair> nextElem) {
		return reducedUndefResSubstGroundedBasePair.stream()
		.map(pair -> {
			Set<UnifyPair> reducedAbhSubst = pair.getKey();
			reducedAbhSubst.addAll(nextElem);
			Optional<Set<UnifyPair>> substRes = rules.subst(reducedAbhSubst);
			if (!substRes.isPresent()) {
				return true;
			}
			//PL 2018-10-12
			//Evtl. zurest applyTypeUnification aufrufen
			//evtl auch unify aufrufen
			else {
				UnifyPair checkPair = substRes.get().stream()
									  .filter(x -> x.getGroundBasePair().equals(pair.getValue().get())).findFirst().get();
				if (((checkPair.getLhsType() instanceof PlaceholderType) || (checkPair.getRhsType() instanceof PlaceholderType)) 
					&& (checkPair.getPairOp() == PairOperator.SMALLERDOT || checkPair.getPairOp() == PairOperator.SMALLERDOTWC))	
				{
					/*
					Set<UnifyPair> setCheckPair = new HashSet<>();
					setCheckPair.add(checkPair);
					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();
	}
	
	protected boolean isUndefinedPairSet(Set<UnifyPair> s) {
		if (s.size() >= 1 ) {
			Boolean ret = s.stream().map(x -> x.isUndefinedPair()).reduce(true, (x,y)-> (x && y));
			return ret;
		}
		else { 
			return false;
		}
	}
	
	protected boolean isUndefinedPairSetSet(Set<Set<UnifyPair>> s) {
		if (s.size() >= 1) {
			Boolean ret = s.stream(). map(x -> isUndefinedPairSet(x)).reduce(true, (x,y)-> (x && y));
			return ret;
		}
		return false;

	}
	/**
	 * Checks whether a set of pairs is in solved form.
	 * @param eqPrimePrime The set of pair
	 * @return True if in solved form,  false otherwise.
	 */
	protected boolean isSolvedForm(Set<UnifyPair> eqPrimePrime) {
		for(UnifyPair pair : eqPrimePrime) {
			UnifyType lhsType = pair.getLhsType();
			UnifyType rhsType = pair.getRhsType();
			
			if(!(lhsType instanceof PlaceholderType))
				return false;
			
			// If operator is not equals, both sides must be placeholders
			if(pair.getPairOp() != PairOperator.EQUALSDOT && !(rhsType instanceof PlaceholderType))
				return false;
		}
		return true;
	}
	
	/**
	 * Repeatedly applies type unification rules to a set of equations. 
	 * This is step one of the unification algorithm.
	 * @return The set of pairs that results from repeated application of the inference rules.
	 */
	public Set<UnifyPair> applyTypeUnificationRules(Set<UnifyPair> eq, IFiniteClosure fc) {
		
		/*
		 * Rule Application Strategy:
		 * 
		 * 1. 	Swap all pairs and erase all erasable pairs
		 * 2. 	Apply all possible rules to a single pair, then move it to the result set.
		 *    	Iterating over pairs first, then iterating over rules prevents the application
		 *    	of rules to a "finished" pair over and over.
		 * 2.1 	Apply all rules repeatedly except for erase rules. If
		 * 		the application of a rule creates new pairs, check immediately
		 * 		against the erase rules.
		 */
		
		
		LinkedHashSet<UnifyPair> targetSet = new LinkedHashSet<UnifyPair>();
		LinkedList<UnifyPair> eqQueue = new LinkedList<>();
		
		/*
		 * Swap all pairs and erase all erasable pairs
		 */
		eq.forEach(x -> swapAddOrErase(x, fc, eqQueue));
		
		/*
		 * Apply rules until the queue is empty
		 */
		while(!eqQueue.isEmpty()) {
			UnifyPair pair = eqQueue.pollFirst();

			// ReduceUp, ReduceLow, ReduceUpLow
			Optional<UnifyPair> opt = rules.reduceUpLow(pair);
			opt = opt.isPresent() ? opt : rules.reduceLow(pair);
			opt = opt.isPresent() ? opt : rules.reduceUp(pair);
			opt = opt.isPresent() ? opt : rules.reduceWildcardLow(pair);
			opt = opt.isPresent() ? opt : rules.reduceWildcardLowRight(pair);
			opt = opt.isPresent() ? opt : rules.reduceWildcardUp(pair);
			opt = opt.isPresent() ? opt : rules.reduceWildcardUpRight(pair);
			//PL 2018-03-06 auskommentiert muesste falsch sein vgl. JAVA_BSP/Wildcard6.java
			//opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair);
			//opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair);
			//opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair);
			
			// Reduce TPH
			opt = opt.isPresent() ? opt : rules.reduceTph(pair);
			
			// One of the rules has been applied
			if(opt.isPresent()) {
				swapAddOrErase(opt.get(), fc, eqQueue);
				continue;
			}
			
			// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
			//try {
			//	logFile.write("PAIR1 " + pair + "\n");
			//	logFile.flush();
			//}
			//catch (IOException e) { }
			
			Optional<Set<UnifyPair>> optSet = rules.reduce1(pair, fc);
			optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
			optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc);
			optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc);
			optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair);
			
			// ReduceTphExt, ReduceTphSup
			optSet = optSet.isPresent() ? optSet : rules.reduceTphExt(pair);
			optSet = optSet.isPresent() ? optSet : rules.reduceTphSup(pair);

			
			// FunN Rules
			optSet = optSet.isPresent() ? optSet : rules.reduceFunN(pair);
			optSet = optSet.isPresent() ? optSet : rules.greaterFunN(pair);
			optSet = optSet.isPresent() ? optSet : rules.smallerFunN(pair);
			
			// One of the rules has been applied
			if(optSet.isPresent()) {
				optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue));
				continue;
			}
			
			// Adapt, AdaptExt, AdaptSup
			//try {
			//	logFile.write("PAIR2 " + pair + "\n");
			//	logFile.flush();
			//}
			//catch (IOException e) { }
			opt = rules.adapt(pair, fc);
			opt = opt.isPresent() ? opt : rules.adaptExt(pair,  fc);
			opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc);
			
			// One of the rules has been applied
			if(opt.isPresent()) {
				swapAddOrErase(opt.get(), fc, eqQueue);
				continue;
			}
			
			// None of the rules has been applied
			targetSet.add(pair);
		}
		
		return targetSet;
	}
	
	/**
	 * Applies the rule swap to a pair if possible. Then adds the pair to the set if no erase rule applies.
	 * If an erase rule applies, the pair is not added (erased).
	 * @param pair The pair to swap and add or erase.
	 * @param collection The collection to which the pairs are added.
	 */
	protected void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection<UnifyPair> collection) {
		Optional<UnifyPair> opt = rules.swap(pair);
		UnifyPair pair2 = opt.isPresent() ? opt.get() : pair;
		
		if(rules.erase1(pair2, fc) || rules.erase3(pair2) || rules.erase2(pair2, fc))
			return;
		
		collection.add(pair2);
	}
	
	/**
	 * Splits the equation eq into a set eq1s where both terms are type variables,
	 * and a set eq2s where one of both terms is not a type variable.
	 * @param eq Set of pairs to be splitted.
	 * @param eq1s Subset of eq where both terms are type variables.
	 * @param eq2s eq/eq1s.
	 */
	protected void splitEq(Set<UnifyPair> eq, Set<UnifyPair> eq1s, Set<UnifyPair> eq2s) {
		for(UnifyPair pair : eq) 
			if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType)
				eq1s.add(pair);
			else
				eq2s.add(pair);
	}
	
	/**
	 * Creates sets of pairs specified in the fourth step. Does not calculate cartesian products.
	 * @param undefined All pairs that did not match one of the 8 cases are added to this set.
	 * @return The set of the eight cases (without empty sets). Each case is a set, containing sets generated
	 * 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) {
		oderConstraintsOutput.addAll(oderConstraintsInput);
		List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9);

		// Init all 8 cases + 9. Case: oderConstraints
		for(int i = 0; i < 9; i++)
			result.add(new HashSet<>());
		
		ArrayList<UnifyPair> eq2sprime = new ArrayList<>(eq2s);
		Iterator<UnifyPair> eq2sprimeit = eq2sprime.iterator();
		ArrayList<UnifyPair> eq2sAsList = new ArrayList<>();
		Boolean first = true;
		while(eq2sprimeit.hasNext()) {// alle mit Variance != 0 nach vorne schieben
			UnifyPair up = eq2sprimeit.next();
			if ((up.getLhsType() instanceof PlaceholderType && ((PlaceholderType)up.getLhsType()).getVariance() != 0)
					|| (up.getRhsType() instanceof PlaceholderType && ((PlaceholderType)up.getRhsType()).getVariance() != 0)) {
				eq2sAsList.add(up);
				eq2s.remove(up);
			}
		}
		if (eq2sAsList.isEmpty()) {
			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) 
								         && (((PlaceholderType)(z.getLhsType())).getVariance() != 0))
								     || ((z.getRhsType() instanceof PlaceholderType) 
										 && (((PlaceholderType)(z.getRhsType())).getVariance() != 0))
								     ).findFirst().isPresent()
					).findFirst().isPresent()).collect(Collectors.toList());
			if (!oderConstraintsVariance.isEmpty()) {
				Set<Set<UnifyPair>> ret = oderConstraintsVariance.get(0);
				oderConstraintsOutput.remove(ret);
				//Set<UnifyPair> retFlat = new HashSet<>(); 
			    //ret.stream().forEach(x -> retFlat.addAll(x)); 
				ret.stream().forEach(x -> x.stream().forEach(y -> y.addSubstitutions(x))); 
				result.get(8).add(ret);
				first = false;
			}
		}
		
		eq2sAsList.addAll(eq2s);
		
		if (eq2sAsList.isEmpty() && first) {//Alle eq2s sind empty und alle oderConstraints mit Variance != 0 sind bearbeitet 
			if (!oderConstraintsOutput.isEmpty()) {
				Set<Set<UnifyPair>> ret = oderConstraintsOutput.remove(0);
				//if (ret.iterator().next().iterator().next().getLhsType().getName().equals("M"))
				//	System.out.println("M");
				//Set<UnifyPair> retFlat = new HashSet<>(); 
			    //ret.stream().forEach(x -> retFlat.addAll(x)); 
				ret.stream().forEach(x -> x.stream().forEach(y -> y.addSubstitutions(x))); 				
				result.get(8).add(ret);
				first = false;
			}
		}
		/*
		Bei allen die Abhaengigkeit der Elemente aus eq2sAsList als evtl. als Substitution 
		  hinzufuegen 
		*/
		Set<UnifyPair> consideredElements = new HashSet<>();
		for(UnifyPair pair : eq2sAsList) {
			if (consideredElements.contains(pair)) {
				continue;
			}
			PairOperator pairOp = pair.getPairOp();
			UnifyType lhsType = pair.getLhsType();
			UnifyType rhsType = pair.getRhsType();
	
			// Case 1: (a <. Theta')
			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<>();
						remElem.add(new UnifyPair(pair.getLhsType(), pair.getRhsType(), PairOperator.EQUALSDOT));
						x1.remove(remElem);
						remElem = new HashSet<>();
						remElem.add(new UnifyPair(pair.getLhsType(), new ExtendsType(pair.getRhsType()), PairOperator.EQUALSDOT));
						x1.remove(remElem);
						remElem = new HashSet<>();
						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)))
							  .collect(Collectors.toCollection(HashSet::new));
					consideredElements.addAll(sameEqSet);
					Set<Set<UnifyPair>> x2 = x1;
					Set<Set<UnifyPair>> x1Res = new HashSet<>(); 
					writeLog("pair:\n" + pair.toString());
					writeLog("x1 Start:\n" + x1.toString());
					writeLog("sameEqSet:\n" + sameEqSet.toString());
					for (UnifyPair sameEq : sameEqSet) {
						writeLog("x1 Original:\n" + x1.toString());
						if (sameEq.getLhsType() instanceof PlaceholderType) {
							x1 = x1.stream().filter(y -> {
								UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
								Set<UnifyPair> localEq = new HashSet<>(); 
								Set<UnifyPair> unitedSubst = new HashSet<>(type.getSubstitution());
								unitedSubst.addAll(sameEq.getSubstitution());
								localEq.add(new UnifyPair(type.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
								Boolean localCorr = !isUndefinedPairSetSet(localRes);
								if (!localCorr) {
									collectErr.addAll(localRes);
								}
								else {
									localRes.forEach(z -> z.addAll(y));
									x1Res.addAll(localRes);
								}
								return localCorr;
							}
							).collect(Collectors.toCollection(HashSet::new));
						}
						else {
							x1 = x1.stream().filter(y -> {
								UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
								Set<UnifyPair> localEq = new HashSet<>(); 
								Set<UnifyPair> unitedSubst = new HashSet<>(type.getSubstitution());
								unitedSubst.addAll(sameEq.getSubstitution());
								localEq.add(new UnifyPair(sameEq.getLhsType(), type.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
								Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
								Boolean localCorr = !isUndefinedPairSetSet(localRes);
								if (!localCorr) {
									collectErr.addAll(localRes);
								}
								else {
									localRes.forEach(z -> z.addAll(y));
									x1Res.addAll(localRes);
								}
								return localCorr;
							}
							).collect(Collectors.toCollection(HashSet::new));
						}
						writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
					}
					Set<Set<UnifyPair>> x1ResPrime;
					if (sameEqSet.isEmpty()) {
						x1ResPrime = x1;
					}
					else {
						x1ResPrime = x1Res;
					}
					result.get(0).add(x1ResPrime);
					ZU LOESCHEN ENDE */
					result.get(0).add(x1);
					if (x1.isEmpty()) {
						undefined.add(pair); //Theta ist nicht im FC => Abbruch
					}
				}
				else {
					Set<UnifyPair> s1 = new HashSet<>();
					s1.add(pair);
					Set<Set<UnifyPair>> s2 = new HashSet<>();
					s2.add(s1);
					result.get(0).add(s2);
				}
						
			}
			// Case 2: (a <.? ? ext Theta')
			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
				if (first) { //writeLog(pair.toString()+"\n");
					Set<Set<UnifyPair>> x1 = unifyCase2(pair, fc);
					result.get(1).add(x1);
					if (x1.isEmpty()) {
						undefined.add(pair); //Theta ist nicht im FC
					}
				}	
				else {
					Set<UnifyPair> s1 = new HashSet<>();
					s1.add(pair);
					Set<Set<UnifyPair>> s2 = new HashSet<>();
					s2.add(s1);
					result.get(1).add(s2);
				}
			
			// Case 3: (a <.? ? sup Theta')
			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
				if (first) { //writeLog(pair.toString()+"\n");
					Set<Set<UnifyPair>> x1 = unifyCase3(pair, fc);
					result.get(2).add(x1);
					if (x1.isEmpty()) {
						undefined.add(pair); //Theta ist nicht im FC
					}
				}
				else {
					Set<UnifyPair> s1 = new HashSet<>();
					s1.add(pair);
					Set<Set<UnifyPair>> s2 = new HashSet<>();
					s2.add(s1);
					result.get(2).add(s2);
				}
			
			// Case 4 was replaced by an inference rule
			// Case 4: (a <.? Theta')
			//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)
				if (first) { //writeLog(pair.toString()+"\n");
					Set<Set<UnifyPair>> x1 = unifyCase5(pair, fc);
					result.get(4).add(x1);
					if (x1.isEmpty()) {
						undefined.add(pair); //Theta ist nicht im FC
					}
				}
				else {
					Set<UnifyPair> s1 = new HashSet<>();
					s1.add(pair);
					Set<Set<UnifyPair>> s2 = new HashSet<>();
					s2.add(s1);
					result.get(4).add(s2);
				}
			
			// Case 6 was replaced by an inference rule.
			// Case 6: (? ext Theta <.? a)
			//else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
			//	result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));

			// Case 7 was replaced by an inference rule
			// Case 7: (? sup Theta <.? a)
			//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)
				if (first) { //writeLog(pair.toString()+"\n");
					Set<Set<UnifyPair>> x1 = unifyCase8(pair, fc);
					result.get(7).add(x1);
					if (x1.isEmpty()) {
						undefined.add(pair); //Theta ist nicht im FC
					}
				}
				else {
					Set<UnifyPair> s1 = new HashSet<>();
					s1.add(pair);
					Set<Set<UnifyPair>> s2 = new HashSet<>();
					s2.add(s1);
					result.get(7).add(s2);
				}
			// 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 {
				// If a pair is not defined, the unificiation will fail, so the loop can be stopped here.
				undefined.add(pair); 
				break;
			}
			first = false;
		}
		
		// Filter empty sets or sets that only contain an empty set.
		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));
	}
	
	//TODO: Wenn Theta' nicht im FC muss ein Fehler produziert werden PL 18-04-20
	/**
	 * Cartesian product Case 1: (a <. Theta') 
	 */
	protected Set<Set<UnifyPair>> unifyCase1(UnifyPair pair, IFiniteClosure fc) {
		PlaceholderType a = (PlaceholderType)pair.getLhsType(); 
		UnifyType thetaPrime = pair.getRhsType(); 
		byte variance = pair.getVariance();
		
		Set<Set<UnifyPair>> result = new HashSet<>();
		
		boolean allGen = thetaPrime.getTypeParams().size() > 0;
		for(UnifyType t : thetaPrime.getTypeParams())
			if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
				allGen = false;
				break;
			}
		//if (thetaPrime.getName().equals("java.util.Vector") //Fuer Bug 127
		//		&& thetaPrime instanceof ReferenceType 
		//		&& ((ReferenceType)thetaPrime).getTypeParams().iterator().next() instanceof PlaceholderType) //.getName().equals("java.util.Vector"))
		//		&& ((ReferenceType)((ReferenceType)thetaPrime).getTypeParams().iterator().next()).getTypeParams().iterator().next().getName().equals("java.lang.Integer")) {
		//		{
		//		System.out.println("");
		//}
		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());//cs= [java.util.Vector<NP>, java.util.Vector<java.util.Vector<java.lang.Integer>>, ????java.util.Vector<gen_hv>???]
		
		
		//PL 18-02-06 entfernt, kommt durch unify wieder rein
		//cs.add(thetaPrime);
		//PL 18-02-06 entfernt
		
		//cs muessen fresh Typvars gesetzt werden PL 2018-03-18
		Set<UnifyType> csPHRenamed = cs.stream().map(x -> {
			BinaryOperator<HashMap<PlaceholderType,PlaceholderType>> combiner = (aa,b) -> { aa.putAll(b); return aa;};
			HashMap<PlaceholderType,PlaceholderType> hm = x.getInvolvedPlaceholderTypes().stream()
					.reduce(new HashMap<PlaceholderType,PlaceholderType>(), 
							(aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner);
			return x.accept(new freshPlaceholder(), hm);
		}).collect(Collectors.toCollection(HashSet::new));
				
				
		for(UnifyType c : csPHRenamed) {
			//PL 18-02-05 getChildren durch smaller ersetzt in getChildren werden die Varianlen nicht ersetzt.
			Set<UnifyType> thetaQs = new HashSet<>();
			//TODO smaller wieder reinnehmen? 
			//thetaQs.add(c);//
			thetaQs = fc.smaller(c, new HashSet<>()).stream().collect(Collectors.toCollection(HashSet::new));
			//Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
		    //thetaQs.add(thetaPrime); //PL 18-02-05 wieder geloescht
			                           //PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert, 
		                               //da children offensichtlich ein echtes kleiner und kein kleinergleich ist
			
			//PL 18-02-06: eingefuegt, thetaQs der Form V<V<...>> <. V'<V<...>> werden entfernt
			//TODO PL 19-01-14 wieder reinnehmen kurzfristig auskommentiert 
			thetaQs = thetaQs.stream().filter(ut -> ut.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
			//PL 18-02-06: eingefuegt
			
			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, new HashSet<>()));
			
				for(TypeParams tp : permuteParams(candidateParams))
					thetaQPrimes.add(c.setTypeParams(tp));
			}
			
			for(UnifyType tqp : thetaQPrimes) {
				Collection<PlaceholderType> tphs = tqp.getInvolvedPlaceholderTypes();
				Optional<Unifier> opt = stdUnify.unify(tqp, thetaPrime);
				if (!opt.isPresent()) {                     
					continue;
				}
				Unifier unifier = opt.get();
				unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams());
				Set<UnifyPair> substitutionSet = new HashSet<>();
				for (Entry<PlaceholderType, UnifyType> sigma : unifier) {
					if (!tphs.contains(sigma.getKey())) {//eingefuegt PL 2019-02-02 Bug 127 
						substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT, 
							//TODO: nochmals ueberlegen ob hier pair.getSubstitution() korrekt ist, oder ob leere Menge hin müsste
							//alle folgenden New UnifyPair ebenfalls ueberpruefen PL 2018-04-19
							pair.getSubstitution(), pair));
					}
				}
				//List<UnifyType> freshTphs = new ArrayList<>(); PL 18-02-06 in die For-Schleife verschoben
				for (UnifyType tq : thetaQs) {
					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq), new HashSet<>()); 
					//eingefuegt PL 2018-03-29 Anfang ? ext. theta hinzufuegen
					if (a.isWildcardable()) {
						Set<UnifyType> smaller_ext = smaller.stream().filter(x -> !(x instanceof ExtendsType) && !(x instanceof SuperType)) 
								.map(x -> {
									//BinaryOperator<HashMap<PlaceholderType,PlaceholderType>> combiner = (aa,b) -> { aa.putAll(b); return aa;}; //Variablenumbenennung rausgenommen
									//HashMap<PlaceholderType,PlaceholderType> hm = x.getInvolvedPlaceholderTypes().stream()                   //Variablen muessen wahrscheinlich erhalten bleiben
									//		.reduce(new HashMap<PlaceholderType,PlaceholderType>(), 
									//				(aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner);
									return new ExtendsType (x);})//.accept(new freshPlaceholder(), hm));}
								.collect(Collectors.toCollection(HashSet::new));
						smaller.addAll(smaller_ext);
					}
					//eingefuegt PL 2018-03-29 Ende ? ext. theta hinzufuegen
					for(UnifyType theta : smaller) {
						List<UnifyType> freshTphs = new ArrayList<>();
						Set<UnifyPair> resultPrime = new HashSet<>();
						
						for(int i = 0; !allGen && i < theta.getTypeParams().size(); i++) {
							if(freshTphs.size()-1 < i)//IST DAS RICHTIG??? PL 2018-12-12
								freshTphs.add(PlaceholderType.freshPlaceholder());
							freshTphs.forEach(x -> ((PlaceholderType)x).setInnerType(true));
							resultPrime.add(new UnifyPair(freshTphs.get(i), theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair));
						}
						
						if(allGen) {
							UnifyPair up = new UnifyPair(a, theta, PairOperator.EQUALSDOT, pair.getSubstitution(), pair);
							Iterator<UnifyType> upit = up.getRhsType().getTypeParams().iterator();
							//TODO PL 2019-01-24: upit.next() ist nicht unbedingt ein PlaceholderType -> Visitor erledigt
							while (upit.hasNext()) upit.next().accept(new distributeVariance(), a.getVariance());//((PlaceholderType)upit.next()).setVariance(a.getVariance());
							resultPrime.add(up);
						}
						else {
							UnifyPair up = new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT, pair.getSubstitution(), pair);
							Iterator<UnifyType> upit = up.getRhsType().getTypeParams().iterator();
							distributeVariance dv = new distributeVariance();
							//TODO PL 2019-01-24: upit.next() ist nicht unbedingt ein PlaceholderType -> Visitor erledigt
							while (upit.hasNext()) upit.next().accept(new distributeVariance(), a.getVariance()); //((PlaceholderType)upit.next()).setVariance(a.getVariance());
							resultPrime.add(up);
						}
						resultPrime.addAll(substitutionSet);
						//writeLog("Substitution: " + substitutionSet.toString());
						resultPrime = resultPrime.stream().map(x -> { x.setVariance(variance); return x;}).collect(Collectors.toCollection(HashSet::new));
						result.add(resultPrime);
						//writeLog("Result: " + resultPrime.toString());
						//writeLog("MAX: " + oup.max(resultPrime.iterator()).toString());
					}
				}

			}
		}
		
		return result;
	}
	
	/**
	 * Cartesian Product Case 2: (a <.? ? ext Theta')
	 */
	private Set<Set<UnifyPair>> unifyCase2(UnifyPair pair, IFiniteClosure fc) {
		PlaceholderType a = (PlaceholderType) pair.getLhsType();
		ExtendsType extThetaPrime = (ExtendsType) pair.getRhsType();
		byte variance = pair.getVariance();
		Set<Set<UnifyPair>> result = new HashSet<>();
		
		UnifyType aPrime = PlaceholderType.freshPlaceholder();
		((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance());
		((PlaceholderType)aPrime).disableWildcardtable();
		UnifyType extAPrime = new ExtendsType(aPrime);
		UnifyType thetaPrime = extThetaPrime.getExtendedType();
		Set<UnifyPair> resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair));
		result.add(resultPrime);
			
		resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
		resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair));
		resultPrime = resultPrime.stream().map(x -> { x.setVariance(variance); return x;}).collect(Collectors.toCollection(HashSet::new));
		result.add(resultPrime);
		//writeLog("Result: " + resultPrime.toString());
		return result;
	}
	
	/**
	 * Cartesian Product Case 3: (a <.? ? sup Theta')
	 */
	private Set<Set<UnifyPair>> unifyCase3(UnifyPair pair, IFiniteClosure fc) {
		PlaceholderType a = (PlaceholderType) pair.getLhsType();
		a.reversVariance();
		SuperType subThetaPrime = (SuperType) pair.getRhsType();
		byte variance = pair.getVariance();
		Set<Set<UnifyPair>> result = new HashSet<>();
		
		UnifyType aPrime = PlaceholderType.freshPlaceholder();
		((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance());
		((PlaceholderType)aPrime).disableWildcardtable();
		UnifyType supAPrime = new SuperType(aPrime);
		UnifyType thetaPrime = subThetaPrime.getSuperedType();
		Set<UnifyPair> resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT, pair.getSubstitution(), pair, pair.getfBounded()));
		result.add(resultPrime);
		//writeLog(resultPrime.toString());
			
		resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
		resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair));
		resultPrime = resultPrime.stream().map(x -> { x.setVariance(variance); return x;}).collect(Collectors.toCollection(HashSet::new));
		result.add(resultPrime);
		//writeLog(resultPrime.toString());
		
		return result;
	}
	
	/**
	 * Cartesian Product Case 5: (Theta <. a)
	 */
	private Set<Set<UnifyPair>> unifyCase5(UnifyPair pair, IFiniteClosure fc) {
		UnifyType theta = pair.getLhsType();
		PlaceholderType a = (PlaceholderType) pair.getRhsType();
		byte variance = pair.getVariance();
		Set<Set<UnifyPair>> result = new HashSet<>();
		
		boolean allGen = theta.getTypeParams().size() > 0;
		for(UnifyType t : theta.getTypeParams())
			if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
				allGen = false;
				break;
			}
		
		//eingefuegt PL 2019-01-03 ANFANG
		//fc.setLogTrue();
		//writeLog("FBOUNDED: " + pair.getfBounded());
		//writeLog("Pair: " + pair);
		Set<UnifyType> greater = fc.greater(theta, pair.getfBounded());
		//writeLog("GREATER: " + greater + pair + "THETA: " + theta + "FBOUNDED: " + pair.getfBounded() + " ");
		if (a.isWildcardable()) {
			Set<UnifyType> greater_ext = greater.stream().filter(x -> !(x instanceof ExtendsType) && !(x instanceof SuperType)) 
					.map(x -> {
						//BinaryOperator<HashMap<PlaceholderType,PlaceholderType>> combiner = (aa,b) -> { aa.putAll(b); return aa;}; //Variablenumbenennung rausgenommen
						//HashMap<PlaceholderType,PlaceholderType> hm = x.getInvolvedPlaceholderTypes().stream()                   //Variablen muessen wahrscheinlich erhalten bleiben
						//		.reduce(new HashMap<PlaceholderType,PlaceholderType>(), 
						//				(aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner);
						return new SuperType (x);})//.accept(new freshPlaceholder(), hm));}
					.collect(Collectors.toCollection(HashSet::new));
			greater.addAll(greater_ext);
		}
		//eingefuegt PL 2019-01-03 ENDE
		
		//for(UnifyType thetaS : fc.greater(theta, pair.getfBounded())) {
		for(UnifyType thetaS : greater) {
			Set<UnifyPair> resultPrime = new HashSet<>();
			Match match = new Match();
			
			UnifyType[] freshTphs = new UnifyType[thetaS.getTypeParams().size()];
			for(int i = 0; !allGen && i < freshTphs.length; i++) {
				freshTphs[i] = PlaceholderType.freshPlaceholder();
				((PlaceholderType)freshTphs[i]).setVariance(((PlaceholderType)a).getVariance());
				Set<UnifyType> fBounded = new HashSet<>(pair.getfBounded()); //PL 2019-01-09 new HashSet eingefuegt
			
				int i_ef = i;
				BiFunction<Boolean,UnifyType,Boolean> f = (x,y) -> 
				{
					ArrayList<UnifyPair> termList = new ArrayList<UnifyPair>();
				    termList.add(new UnifyPair(y,thetaS.getTypeParams().get(i_ef), PairOperator.EQUALSDOT));
				    return ((match.match(termList).isPresent()) || x);
				};
				//if (parai.getName().equals("java.lang.Integer")) {
				//	System.out.println("");
				//}
				BinaryOperator<Boolean> bo = (x,y) -> (x || y);
				if (fBounded.stream().reduce(false,f,bo)) {
					resultPrime.add(new UnifyPair(freshTphs[i], thetaS.getTypeParams().get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
				}
				else {
					fBounded.add(thetaS.getTypeParams().get(i));
					resultPrime.add(new UnifyPair(thetaS.getTypeParams().get(i), freshTphs[i], PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair, fBounded));
				}	
			}
			
			if(allGen)
				resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
			else
				resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
			resultPrime = resultPrime.stream().map(x -> { x.setVariance(variance); return x;}).collect(Collectors.toCollection(HashSet::new));
			result.add(resultPrime);
			//writeLog("FBOUNDED2: " + pair.getfBounded());
			//writeLog("resultPrime Theta < a: " + greater + pair + "THETA: " + theta + "FBOUNDED: " + pair.getfBounded() + " " + resultPrime.toString());
		}
	
		return result;
	}

	/**
	 * Cartesian Product Case 8: (Theta <.? a)
	 */
	private Set<Set<UnifyPair>> unifyCase8(UnifyPair pair, IFiniteClosure fc) {
		UnifyType theta = pair.getLhsType();
	    PlaceholderType a = (PlaceholderType) pair.getRhsType();
	    byte variance = pair.getVariance();
		Set<Set<UnifyPair>> result = new HashSet<>();
		//for(UnifyType thetaS : fc.grArg(theta)) {
		Set<UnifyPair> resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
		result.add(resultPrime);
		//writeLog(resultPrime.toString());
		
		UnifyType freshTph = PlaceholderType.freshPlaceholder();
		
		((PlaceholderType)freshTph).setVariance(a.getVariance());
		((PlaceholderType)freshTph).disableWildcardtable();
		resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
		resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair, pair.getfBounded()));
		result.add(resultPrime);
		//writeLog("resultPrime: " + resultPrime.toString());

		resultPrime = new HashSet<>();
		resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair));
		resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT, pair.getSubstitution(), pair));
		resultPrime = resultPrime.stream().map(x -> { x.setVariance(variance); return x;}).collect(Collectors.toCollection(HashSet::new));
		result.add(resultPrime);
		//writeLog(resultPrime.toString());
		//}
	
		return result;
	}
	
	/**
	 * Takes a set of candidates for each position and computes all possible permutations.
	 * @param candidates The length of the list determines the number of type params. Each set
	 * contains the candidates for the corresponding position.
	 */
	protected Set<TypeParams> permuteParams(ArrayList<Set<UnifyType>> candidates) {
		Set<TypeParams> result = new HashSet<>();
		permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
		return result;
	}
	
	/**
	 * Takes a set of candidates for each position and computes all possible permutations.
	 * @param candidates The length of the list determines the number of type params. Each set
	 * contains the candidates for the corresponding position.
	 * @param idx Idx for the current permutatiton.
	 * @param result Set of all permutations found so far
	 * @param current The permutation of type params that is currently explored
	 */
	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;
		}
		
		Set<UnifyType> localCandidates = candidates.get(idx);
		
		for(UnifyType t : localCandidates) {
			current[idx] = t;
			permuteParams(candidates, idx+1, result, current);
		}
	}
	
	void writeLog(String str) {
		synchronized ( this ) { 
		if (log) {
			try {
				logFile.write("Thread no.:" + thNo + "\n");
				logFile.write("noOfThread:" + noOfThread + "\n");
				logFile.write("parallel:" + parallel + "\n");
				logFile.write(str+"\n\n");
				logFile.flush();
			
			}
			catch (IOException e) { 
				System.err.println("kein LogFile");
			}
			}
	}
	}
}
