Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 4787 insertions, 0 deletions

diff --git a/test/spass/cnf.c b/test/spass/cnf.c
new file mode 100644
index 00000000..bf52a264
--- /dev/null
+++ b/test/spass/cnf.c
@@ -0,0 +1,4787 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *               CNF TRANSLATOR                           * */
+/* *                                                        * */
+/* *  $Module:   CNF                                        * */
+/* *                                                        * */
+/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
+/* *  MPI fuer Informatik                                   * */
+/* *                                                        * */
+/* *  This program is free software; you can redistribute   * */
+/* *  it and/or modify it under the terms of the GNU        * */
+/* *  General Public License as published by the Free       * */
+/* *  Software Foundation; either version 2 of the License, * */
+/* *  or (at your option) any later version.                * */
+/* *                                                        * */
+/* *  This program is distributed in the hope that it will  * */
+/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
+/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
+/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
+/* *  License for more details.                             * */
+/* *                                                        * */
+/* *  You should have received a copy of the GNU General    * */
+/* *  Public License along with this program; if not, write * */
+/* *  to the Free Software Foundation, Inc., 59 Temple      * */
+/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
+/* *                                                        * */
+/* *                                                        * */
+/* $Revision: 21527 $                                       * */
+/* $State$                                            * */
+/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
+/* $Author: duraid $                                       * */
+/* *                                                        * */
+/* *             Contact:                                   * */
+/* *             Christoph Weidenbach                       * */
+/* *             MPI fuer Informatik                        * */
+/* *             Stuhlsatzenhausweg 85                      * */
+/* *             66123 Saarbruecken                         * */
+/* *             Email: weidenb@mpi-sb.mpg.de               * */
+/* *             Germany                                    * */
+/* *                                                        * */
+/* ********************************************************** */
+/**************************************************************/
+
+
+/* $RCSfile$ */
+
+#include "cnf.h"
+#include "rules-inf.h"
+#include "rules-red.h"
+
+
+static TERM   cnf_AntiPrenexPath(TERM, TERM);
+static TERM   cnf_ApplyDefinitionInternOnce(TERM, TERM, TERM, TERM, BOOL*);
+
+static SYMBOL cnf_GetDualSymbol(SYMBOL symbol);
+
+static TERM   cnf_IsDefinition(TERM);
+
+static void   cnf_OptimizedSkolemFormula(PROOFSEARCH, TERM, char*, BOOL, TERM,
+					 LIST*, LIST*, BOOL, HASH, int);
+static int    cnf_PredicateOccurrences(TERM, SYMBOL);
+
+static void   cnf_RplacVar(TERM, LIST, LIST);
+
+static LIST   cnf_SatUnit(PROOFSEARCH, LIST);
+static LIST   cnf_SkolemFunctionFormula(TERM, LIST, LIST, PRECEDENCE);
+
+/* For every variable the depth in the current term, required for */
+/* strong skolemization */
+static int* cnf_VARIABLEDEPTHARRAY;
+/* Holds a copy of the ProofSearch--Object built by cnf_Flotter */
+/* during cnf_QueryFlotter */
+static PROOFSEARCH cnf_SEARCHCOPY;
+
+/* Proofsearch--Object for the function cnf_HaveProof. We need this */
+/* to reduce the number of term stamps required. */
+static PROOFSEARCH cnf_HAVEPROOFPS;
+
+
+void cnf_Init(FLAGSTORE Flags)
+/***************************************************************
+  INPUT:   A flag store.
+  RETURNS: None.
+  SUMMARY: Initializes the CNF Module.
+  EFFECTS: Initializes global variables.
+  CAUTION: MUST BE CALLED BEFORE ANY OTHER CNF-FUNCTION.
+***************************************************************/
+{
+  /* If strong skolemization is performed, allocate array for variable depth */
+  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))
+    cnf_VARIABLEDEPTHARRAY = (int*) memory_Malloc(sizeof(int[symbol__MAXSTANDARDVAR + 1]));
+  else
+    cnf_VARIABLEDEPTHARRAY = NULL;
+  cnf_SEARCHCOPY  = prfs_Create();
+  cnf_HAVEPROOFPS = prfs_Create();
+}
+
+
+void cnf_Free(FLAGSTORE Flags)
+/**************************************************************
+  INPUT:   A flag store.
+  RETURNS: None.
+  SUMMARY: Frees the CNF Module.
+***************************************************************/
+{
+  /* If strong skolemization is performed, free array for variable depth */
+  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
+    memory_Free(cnf_VARIABLEDEPTHARRAY, sizeof(int) * (symbol__NOOFSTANDARDVAR + 1));
+    cnf_VARIABLEDEPTHARRAY = NULL;
+  }
+  prfs_Delete(cnf_SEARCHCOPY);
+  cnf_SEARCHCOPY = NULL;
+  prfs_Delete(cnf_HAVEPROOFPS);
+  cnf_HAVEPROOFPS = NULL;
+}
+
+
+static int cnf_GetFormulaPolarity(TERM term, TERM subterm)
+/**********************************************************
+  INPUT:   Two terms term and subterm where subterm is a
+           subterm of term.
+  RETURNS: The polarity of subterm in term.
+********************************************************/
+{  
+  LIST   scan;
+  TERM   term1;
+  int    polterm1,bottom; 
+
+  bottom = vec_ActMax();
+  vec_Push((POINTER) 1);
+  vec_Push(term);
+
+  do {
+    term1    = (TERM)vec_PopResult();
+    polterm1 = (int)vec_PopResult();
+    if (term1 == subterm) {
+      vec_SetMax(bottom);
+      return polterm1;
+    }else
+      if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {
+	vec_Push((POINTER) (- polterm1));
+	vec_Push(list_Car(term_ArgumentList(term1)));
+      }
+    if (symbol_Equal(term_TopSymbol(term1),fol_Exist()) ||
+	symbol_Equal(term_TopSymbol(term1),fol_All())) {
+      vec_Push((POINTER)polterm1);
+      vec_Push(list_Second(term_ArgumentList(term1)));
+    }
+    else
+      if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
+	vec_Push((POINTER) (- polterm1));
+	vec_Push(list_Car(term_ArgumentList(term1)));
+	vec_Push((POINTER) polterm1);
+	vec_Push(list_Second(term_ArgumentList(term1)));
+      }
+      else
+	if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) {
+	  vec_Push(0);
+	  vec_Push(list_Car(term_ArgumentList(term1)));
+	  vec_Push(0);
+	  vec_Push(list_Second(term_ArgumentList(term1)));
+	}
+	else
+	  if (symbol_Equal(term_TopSymbol(term1),fol_And()) ||
+	      symbol_Equal(term_TopSymbol(term1),fol_Or())) {
+	    for (scan = term_ArgumentList(term1);
+		 !list_Empty(scan);
+		 scan = list_Cdr(scan)) {
+	      vec_Push((POINTER) polterm1);
+	      vec_Push(list_Car(scan));
+	    }
+	  }
+  } while (bottom != vec_ActMax());
+  vec_SetMax(bottom);
+  misc_StartErrorReport();
+  misc_ErrorReport("\n In cnf_GetFormulaPolarity: Wrong arguments !\n");
+  misc_FinishErrorReport();
+  return -2;
+}
+
+
+static BOOL cnf_ContainsDefinitionIntern(TERM TopDef, TERM Def, int Polarity,
+					 TERM* FoundPred)
+/**********************************************************
+  INPUT:   A term TopDef which is the top level term of the recursion.
+           A term Def which is searched for a definition.
+           A pointer to a term into which the predicate of the definition
+	   is stored if it is found.
+  RETURNS: TRUE if Def contains a definition that can be converted
+           to standard form.
+********************************************************/
+{
+  /* AND / OR */
+  /* In these cases Def cannot be converted to standard form */
+
+  if ((symbol_Equal(term_TopSymbol(Def),fol_And()) && (Polarity == 1)) ||
+      (symbol_Equal(term_TopSymbol(Def),fol_Or()) && (Polarity == -1)))
+    return FALSE;
+
+  if (symbol_Equal(term_TopSymbol(Def), fol_And()) ||
+     symbol_Equal(term_TopSymbol(Def),fol_Or())) {
+    /* Polarity is ok */
+    LIST l;
+    for (l=term_ArgumentList(Def); !list_Empty(l); l=list_Cdr(l))
+      if (cnf_ContainsDefinitionIntern(TopDef, list_Car(l), Polarity, FoundPred))
+	return TRUE;
+    return FALSE;
+  }
+
+  /* Quantifiers */
+  if (fol_IsQuantifier(term_TopSymbol(Def)))
+    return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
+  
+  /* Negation */
+  if (symbol_Equal(term_TopSymbol(Def),fol_Not()))
+    return cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred);
+  
+  /* Implication */
+  if (symbol_Equal(term_TopSymbol(Def),fol_Implies())) {
+    if (Polarity==1) {
+      if (cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred))
+	return TRUE;
+      return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
+    }
+    return FALSE;
+  }
+  
+  /* Equivalence */
+  if (symbol_Equal(term_TopSymbol(Def),fol_Equiv()) && (Polarity==1)) {
+    /* Check if equivalence itself is in correct form */
+    TERM defpredicate;
+
+    defpredicate = cnf_IsDefinition(Def);
+    if (defpredicate != (TERM) NULL) {
+      LIST predicate_vars, l, defpath;
+      BOOL allquantifierfound;
+      TERM super;
+      int pol;
+      /* Check if predicate occurs several times in TopDef */
+      /* if (cnf_PredicateOccurrences(TopDef, term_TopSymbol(defpredicate)) > 1) {}
+	 puts("\n Predicate occurs more than once.");
+	 return FALSE; */
+
+
+      /* Now make sure that the variables of the predicate are       */
+      /* all--quantified and not in the scope of an exist quantifier */
+      /*      predicate_vars = list_Copy(term_ArgumentList(defpredicate)); */
+      predicate_vars = term_ListOfVariables(defpredicate);
+      predicate_vars = term_DeleteDuplicatesFromList(predicate_vars);
+
+      /* So far (going bottom--up) no all-quantifier was found for */
+      /* a variable of the predicates' arguments */
+      allquantifierfound = FALSE;
+      
+      /* Build defpath here by going bottom up */
+      /* At first, list of superterms on path is top down */
+      defpath = list_Nil();
+      super = Def;
+      while (super != (TERM) NULL) {
+	defpath = list_Cons(super, defpath);
+	super = term_Superterm(super);
+      }
+      /* No go top down and add polarities */
+      pol = 1;
+      for (l=defpath; !list_Empty(l); l=list_Cdr(l)) {
+	list_Rplaca(l, list_PairCreate((TERM) list_Car(l), (LIST) pol));
+	if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Not()))
+	  pol = -pol;
+	else {
+	  if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Implies()) &&
+	      (term_FirstArgument((TERM) list_Car(l)) == (TERM) list_Car(list_Cdr(l))))
+	    pol = -pol;
+	  else 
+	    if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Equiv()))
+	      pol = 0;
+	}
+      }
+      /* <defpath> is now a list of pairs (term, polarity) */
+      for (l=defpath; !list_Empty(l) && !list_Empty(predicate_vars); l=list_Cdr(l)) {
+	LIST pair;
+	TERM t;
+	int p;
+	/* Pair Term t / Polarity p */
+	pair = (LIST) list_Car(l);
+	t = (TERM) list_PairFirst(pair);
+	p = (int) list_PairSecond(pair);
+
+	if (fol_IsQuantifier(term_TopSymbol(t))) {
+	  
+	  /* Variables of the predicate that are universally quantified are no problem */
+	  if ((symbol_Equal(term_TopSymbol(t), fol_All()) && (p==1)) ||
+	      (symbol_Equal(term_TopSymbol(t), fol_Exist()) && (p==-1))) {
+	    LIST scan;
+	    allquantifierfound = TRUE;
+	    for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan))
+	      predicate_vars = list_DeleteElement(predicate_vars,(TERM) list_Car(scan),
+						  (BOOL (*)(POINTER,POINTER))term_Equal);
+	  }
+	  else {
+	    /* Check if allquantified variables of the predicate are in scope of an exist--quantifier */
+	    /* We already found an all quantified variable */
+	    if (allquantifierfound) {
+	      list_Delete(predicate_vars);
+	      list_DeletePairList(defpath);
+	      return FALSE;
+	    }
+	    else {
+	      LIST scan;
+	      /* Check if a variable of the predicate is exist--quantified */
+	      for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan)) {
+		if (term_ListContainsTerm(predicate_vars, list_Car(scan))) {
+		  list_Delete(predicate_vars);
+		  list_DeletePairList(defpath);
+		  return FALSE;
+		}
+	      }
+	    }
+	  }
+	}
+      }
+      
+#ifdef CHECK
+      if (!list_Empty(predicate_vars)) {
+	list_Delete(predicate_vars);
+	misc_StartErrorReport();
+	misc_ErrorReport("\n In cnf_ContainsDefinitionIntern: Definition has free variables.\n");
+	misc_FinishErrorReport();
+      }
+#endif
+      list_DeletePairList(defpath);
+      *FoundPred = defpredicate;
+      return TRUE;
+    }
+  }
+  
+  return FALSE;
+}
+
+
+BOOL cnf_ContainsDefinition(TERM Def, TERM* FoundPred)
+/**********************************************************
+  INPUT:   A term Def which is searched for a definition of a predicate.
+           A pointer to a term into which the predicate of the definition
+	   is stored if it is found.
+  RETURNS: TRUE if Def contains a definition that can be converted to
+           standard form.
+***********************************************************/
+{
+  BOOL result;
+#ifdef CHECK
+  fol_CheckFatherLinks(Def);
+#endif
+  result = cnf_ContainsDefinitionIntern(Def, Def, 1, FoundPred);
+#ifdef CHECK
+  fol_CheckFatherLinks(Def);
+#endif
+  return result;
+}
+
+
+static TERM cnf_IsDefinition(TERM Def)
+/**********************************************************
+ INPUT:   A term Def.
+ RETURNS: The Def term where the arguments of the equivalence are exchanged
+          iff the first one is not a predicate.
+**********************************************************/
+{
+  LIST l,freevars, predicatevars;
+
+#ifdef CHECK
+  if (Def == NULL) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_IsDefinition: Empty formula.\n");
+    misc_FinishErrorReport();
+  }
+  if (!symbol_Equal(term_TopSymbol(Def),fol_Equiv())) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_IsDefinition: Formula is no equivalence.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+  
+  /* If the predicate is the second argument of the equivalence, exchange them */
+  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) {
+    TERM arg1;
+    arg1 = term_FirstArgument(Def);
+    term_RplacFirstArgument(Def, term_SecondArgument(Def));
+    term_RplacSecondArgument(Def, arg1);
+  }
+
+
+  /* Check if the first argument is a predicate */
+  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) 
+    return NULL;
+
+  /* Check if first argument is a predicate and not fol_Equality */
+  /*  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))
+      || symbol_Equal(term_TopSymbol(term_FirstArgument(Def)), fol_Equality()))) {
+      return NULL;
+      }*/
+
+
+  /* The free variables of the non-predicate term must occur in the predicate term */
+  
+  freevars = fol_FreeVariables(term_SecondArgument(Def));
+  freevars = term_DeleteDuplicatesFromList(freevars);
+  predicatevars = term_ListOfVariables(term_FirstArgument(Def));
+  predicatevars = term_DeleteDuplicatesFromList(predicatevars);
+
+  for (l=predicatevars; !list_Empty(l); l=list_Cdr(l))
+    freevars = list_DeleteElement(freevars, list_Car(l),
+				  (BOOL (*)(POINTER,POINTER))term_Equal);
+
+  if (!list_Empty(freevars)) {
+    list_Delete(freevars);
+    list_Delete(predicatevars);
+    return NULL;
+  }
+
+  list_Delete(predicatevars);
+  return term_FirstArgument(Def);
+}
+
+
+static BOOL cnf_ContainsPredicateIntern(TERM Target, SYMBOL Predicate, 
+					int Polarity, TERM* TargetPredicate,
+					TERM* ToTopLevel, LIST* TargetVars,
+					LIST* VarsForTopLevel)
+/**********************************************************
+  INPUT:   A term (sub--) Target
+           A symbol Predicate which is searched in the target term.
+           The polarity of the subterm.
+           A pointer to the term TargetPredicate into which the found
+	   predicate term is stored.
+           A pointer to the list TargetVars into which the variables found
+	   in the predicates' arguments are stored.
+           A pointer to a list VarsForTopLevel into which all variables are
+	   stored that are all--quantified and can be moved to top level.
+
+  RETURNS: TRUE if Formula contains the predicate for which a definition
+           was found.
+********************************************************/
+{
+  /* AND / OR */
+  /* In these cases the predicate (if it exists) can not be moved to a higher level */
+
+  if ((symbol_Equal(term_TopSymbol(Target),fol_And()) && Polarity == 1) ||
+      (symbol_Equal(term_TopSymbol(Target),fol_Or()) && Polarity == -1) ||
+      (symbol_Equal(term_TopSymbol(Target),fol_Implies()) && Polarity != 1) ||
+      symbol_Equal(term_TopSymbol(Target), fol_Equiv())) {
+    TERM s;
+    LIST l;
+    /* Try to find Predicate in Target */
+    s = term_FindSubterm(Target, Predicate);
+    if (s == NULL)
+      return FALSE;
+    
+    /* Store variables found in the predicates arguments */
+    for (l=term_ArgumentList(s); !list_Empty(l); l = list_Cdr(l))
+      *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars);
+    *TargetVars = term_DeleteDuplicatesFromList(*TargetVars);
+    /* Keep found predicate */
+    *TargetPredicate = s;
+    *ToTopLevel = Target;
+    return TRUE;
+  }
+  
+  /* AND / OR continued */
+  if (symbol_Equal(term_TopSymbol(Target),fol_And()) || symbol_Equal(term_TopSymbol(Target),fol_Or())) {
+    /* The polarity is ok here */
+    LIST l;
+    for (l=term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l))
+      if (cnf_ContainsPredicateIntern((TERM) list_Car(l), Predicate, Polarity,
+				      TargetPredicate, ToTopLevel, TargetVars,
+				      VarsForTopLevel))
+	return TRUE;
+    return FALSE;
+  }
+
+  /* Quantifiers */
+  if (fol_IsQuantifier(term_TopSymbol(Target))) {
+    if (cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate,
+				    Polarity, TargetPredicate, ToTopLevel,
+				    TargetVars, VarsForTopLevel)) {
+      /* Quantifiers for free variables of the predicate should be moved
+	 to top level to make the proof easier */
+      if ((symbol_Equal(term_TopSymbol(Target), fol_All()) && Polarity == 1) ||
+	  (symbol_Equal(term_TopSymbol(Target), fol_Exist()) && Polarity == -1)) {
+	LIST l;
+	/* Check for all variables found in the predicates arguments */
+	for (l = *TargetVars; !list_Empty(l); l=list_Cdr(l)) {
+	  if (term_ListContainsTerm(fol_QuantifierVariables(Target),list_Car(l)))
+	    *VarsForTopLevel = list_Cons(list_Car(l), *VarsForTopLevel);
+	}
+      }
+      return TRUE;
+    }
+    return FALSE;
+  }
+
+  /* Negation */
+  if (symbol_Equal(term_TopSymbol(Target),fol_Not()))
+    return cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate,
+				       -Polarity, TargetPredicate, ToTopLevel,
+				       TargetVars, VarsForTopLevel);
+  /* Implication */
+  if (symbol_Equal(term_TopSymbol(Target),fol_Implies())) {
+    /* In this case the predicate (if it exists) can be moved to a higher level */
+    if (cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate,
+				    -Polarity, TargetPredicate, ToTopLevel,
+				    TargetVars, VarsForTopLevel))
+      return TRUE;
+    return cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate,
+				       Polarity, TargetPredicate, ToTopLevel,
+				       TargetVars, VarsForTopLevel);
+  }
+
+  /* Found the predicate */
+  if (symbol_Equal(term_TopSymbol(Target), Predicate)) {
+    LIST l;
+    for (l = term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l))
+      *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars);
+    *TargetVars = term_DeleteDuplicatesFromList(*TargetVars);
+    
+    *TargetPredicate = Target;
+    *ToTopLevel      = Target;
+    return TRUE;
+  }
+  
+  /* In all other cases the predicate was not found */
+  return FALSE;
+}  
+
+  
+BOOL cnf_ContainsPredicate(TERM Target, SYMBOL Predicate,
+			   TERM* TargetPredicate, TERM* ToTopLevel,
+			   LIST* TargetVars, LIST* VarsForTopLevel)
+/**********************************************************
+  INPUT:   A term Target without implications.
+           A symbol Predicate which is searched in the target term.
+           A pointer to the predicate found in TargetTerm is recorded.
+           A pointer to the term TargetPredicate into which the found
+	   predicate term is stored.
+           A pointer to the list TargetVars into which the variables
+	   found in the predicates' arguments are stored.
+           A pointer to a list VarsForTopLevel into which all variables
+	   are stored that are all--quantified and can be moved to top level.
+  RETURNS: TRUE if Formula contains the predicate for which a definition
+           was found.
+********************************************************/
+{
+  BOOL result;
+#ifdef CHECK
+  fol_CheckFatherLinks(Target);
+#endif
+  result = cnf_ContainsPredicateIntern(Target, Predicate, 1, TargetPredicate,
+				       ToTopLevel, TargetVars, VarsForTopLevel);
+#ifdef CHECK
+  fol_CheckFatherLinks(Target);
+#endif
+  return result;
+}
+
+
+static int cnf_PredicateOccurrences(TERM Term, SYMBOL P)
+/****************************************************
+  INPUT:   A term and a predicate symbol.
+  RETURNS: The number of occurrences of the predicate symbol in Term
+**************************************************/			       
+{
+  /* Quantifiers */
+  if (fol_IsQuantifier(term_TopSymbol(Term)))
+    return cnf_PredicateOccurrences(term_SecondArgument(Term), P);
+
+  /* Junctors and NOT */
+  if (fol_IsJunctor(term_TopSymbol(Term)) ||
+      symbol_Equal(term_TopSymbol(Term),fol_Not())) {
+    LIST scan;
+    int count;
+    count = 0;
+    for (scan=term_ArgumentList(Term); !list_Empty(scan); scan=list_Cdr(scan)) {
+      count += cnf_PredicateOccurrences(list_Car(scan), P);
+      /* Only the cases count==1 and count>1 are important */
+      if (count > 1)
+	return count;
+    }
+    return count;
+  }
+  
+  if (symbol_Equal(term_TopSymbol(Term), P))
+    return 1;
+  return 0;
+} 
+  
+
+static TERM cnf_NegationNormalFormulaPath(TERM Term, TERM PredicateTerm)
+/**********************************************************
+  INPUT:   A term and a predicate term which is a subterm of term
+  RETURNS: The negation normal form of the term along the path.
+  CAUTION: The term is destructively changed.
+           This works only if the superterm member of Term and its subterms 
+	   are set.
+********************************************************/
+{
+  TERM   subterm, termL, term1;
+  LIST   scan;
+  SYMBOL symbol;
+  BOOL   set;
+
+  term1 = Term;
+  while (term1 != NULL) {
+    set = FALSE;
+    if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {	    
+      subterm = term_FirstArgument(term1);
+      if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) {
+	LIST l;
+	term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm)));
+	list_Delete(term_ArgumentList(term1));
+	term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm)));
+	term_Free(term_FirstArgument(subterm));
+	list_Delete(term_ArgumentList(subterm));
+	term_Free(subterm);
+	/* Set superterm member to new superterm */
+	for (l=term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l))
+	  term_RplacSuperterm(list_Car(l), term1);
+	/* term1 weiter betrachten */
+	set = TRUE;
+      }
+      else {
+	if (fol_IsQuantifier(term_TopSymbol(subterm))) {
+	  LIST l;
+	  symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
+	  termL  = term_CreateAddFather(fol_Not(),
+					list_List(term_SecondArgument(subterm)));
+	  list_RplacSecond(term_ArgumentList(subterm), termL);
+	  term_RplacSuperterm(termL, subterm);
+	  term_RplacTop(term1,symbol);
+	  list_Delete(term_ArgumentList(term1));
+	  term_RplacArgumentList(term1, term_ArgumentList(subterm));
+	  for (l=term_ArgumentList(term1); !list_Empty(l); l = list_Cdr(l))
+	    term_RplacSuperterm(list_Car(l), term1);
+	  term_RplacArgumentList(subterm, list_Nil());
+	  term_Delete(subterm);
+	  term1 = termL;
+	  /* Next term to check is not(subterm) */
+	  set = TRUE;
+	} 
+	else {
+	  if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || 
+	      (symbol_Equal(term_TopSymbol(subterm),fol_And()))) {
+	    LIST l;
+	    symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
+	    for (scan = term_ArgumentList(subterm); !list_Empty(scan);
+		 scan = list_Cdr(scan)) {
+	      TERM new;
+	      termL = list_Car(scan);
+	      new = term_CreateAddFather(fol_Not(),list_List(termL));
+	      list_Rplaca(scan, new);
+	      term_RplacSuperterm(new, subterm);
+	    }
+	    term_RplacTop(term1,symbol);
+	    list_Delete(term_ArgumentList(term1));
+	    term_RplacArgumentList(term1,term_ArgumentList(subterm));
+	    for (l = term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l))
+	      term_RplacSuperterm(list_Car(l), term1);
+	    term_RplacArgumentList(subterm, list_Nil());
+	    term_Delete(subterm);
+	  }
+	}
+      }
+    }
+    if (!set) {
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	  if (term_HasProperSuperterm(PredicateTerm, list_Car(scan))) {
+	    term1 = list_Car(scan);
+	    set = TRUE;
+	    break;
+	  }
+      if (!set)
+	term1 = NULL;
+    }
+  }
+  return Term;
+}
+
+
+TERM cnf_ApplyDefinitionOnce(TERM Predicate, TERM Formula, TERM TargetTerm,
+			     TERM TargetPredicate, FLAGSTORE Flags)
+/*********************************************************
+  INPUT:   A term Predicate which is a predicate found in a definition.
+           A term Formula which is a term equivalent to the predicate.
+           A term TargetTerm in which one occurrence of the predicate may be 
+           replaced by the Formula.
+           A term TargetPredicate which is the subterm of the TargetTerm
+           to be replaced.
+	   A flag store.
+  RETURNS: The changed TargetTerm.
+*************************************************************/
+{
+  SYMBOL maxvar, maxvar_temp;
+  LIST bound, scan;
+  BOOL success;
+  
+  /* Init varcounter */
+  maxvar = term_MaxVar(TargetTerm);
+  maxvar_temp = term_MaxVar(Formula);
+  if (maxvar_temp > maxvar)
+    maxvar = maxvar_temp;
+  symbol_SetStandardVarCounter(maxvar);
+
+  /* Find bound variables in formula for renaming them */
+  bound = fol_BoundVariables(Formula);
+  for (scan=bound; !list_Empty(scan); scan=list_Cdr(scan)) {
+    /* Bound variable in definition is already used in term */
+    if (term_ContainsSymbol(TargetTerm, term_TopSymbol(list_Car(scan))))
+      term_ExchangeVariable(Formula, term_TopSymbol(list_Car(scan)),
+			    symbol_CreateStandardVariable());
+  }
+  list_Delete(bound);
+  TargetTerm = cnf_ApplyDefinitionInternOnce(Predicate, Formula, TargetTerm, 
+					     TargetPredicate,&success);
+  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+    if (success) {
+      fputs("\nTarget after applying def:\n", stdout);
+      fol_PrettyPrint(TargetTerm);
+      puts("\n");
+    }
+  }
+  
+  return TargetTerm;
+}
+
+
+static TERM cnf_ApplyDefinitionInternOnce(TERM Predicate, TERM Formula, 
+					  TERM TargetTerm, TERM TargetPredicate,
+					  BOOL* Success)
+/**********************************************************
+  INPUT:   A term Predicate which is equivalence to
+           Formula and Term
+  RETURNS: The term in which all occurrences of P(..) are 
+           replaced by Formula modulo the proper bindings
+  CAUTION: Term is destructively changed!
+***********************************************************/
+{
+  /* Quantifiers */
+  if (fol_IsQuantifier(term_TopSymbol(TargetTerm))) {
+    term_RplacSecondArgument(TargetTerm, 
+      cnf_ApplyDefinitionInternOnce(Predicate, Formula, 
+				    term_SecondArgument(TargetTerm),
+				    TargetPredicate, Success));
+    term_RplacSuperterm(term_SecondArgument(TargetTerm), TargetTerm);
+    return TargetTerm;
+  }
+
+  /* Junctors and NOT */
+  if (fol_IsJunctor(term_TopSymbol(TargetTerm)) ||
+      symbol_Equal(term_TopSymbol(TargetTerm),fol_Not())) {
+    LIST scan;
+    for (scan=term_ArgumentList(TargetTerm); !list_Empty(scan); scan=list_Cdr(scan)) {
+      list_Rplaca(scan, cnf_ApplyDefinitionInternOnce(Predicate, Formula, 
+						      list_Car(scan), 
+						      TargetPredicate, Success));
+      term_RplacSuperterm((TERM) list_Car(scan), TargetTerm);
+    }
+    return TargetTerm;
+  }
+  
+  if (symbol_Equal(term_TopSymbol(TargetTerm), term_TopSymbol(Predicate))) {
+    if (TargetTerm == TargetPredicate) {
+      TERM result;
+      result = Formula;
+      cnf_RplacVar(result, term_ArgumentList(Predicate), 
+		   term_ArgumentList(TargetTerm));
+      term_AddFatherLinks(result);
+      term_Delete(TargetTerm);
+      *Success = TRUE;
+      return result;
+    }
+  }
+  
+  return TargetTerm;
+} 
+
+
+static TERM cnf_RemoveEquivImplFromFormula(TERM term)
+/**********************************************************
+  INPUT:   A term.
+  RETURNS: The term  with replaced implications and equivalences.
+  CAUTION: The term is destructively changed.
+********************************************************/
+{
+  TERM term1,termL,termR,termLneg,termRneg;
+  LIST scan;
+  int  bottom,pol;
+  
+  bottom = vec_ActMax();
+  vec_Push(term);
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
+      term_RplacTop(term1, fol_Or());
+      list_Rplaca(term_ArgumentList(term1),
+		  term_Create(fol_Not(), list_List(list_Car(term_ArgumentList(term1)))));
+    }else
+      if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) {
+	pol      = cnf_GetFormulaPolarity(term,term1);
+	termL    = (TERM)list_Car(term_ArgumentList(term1));
+	termR    = (TERM)list_Second(term_ArgumentList(term1));
+	termLneg = term_Create(fol_Not(),list_List(term_Copy(termL)));
+	termRneg = term_Create(fol_Not(),list_List(term_Copy(termR)));
+	if (pol == 1 || pol == 0) {
+	  term_RplacTop(term1, fol_And());
+	  list_Rplaca(term_ArgumentList(term1), term_Create(fol_Or(),list_Cons(termLneg,list_List(termR))));
+	  list_RplacSecond(term_ArgumentList(term1),term_Create(fol_Or(),list_Cons(termRneg,list_List(termL))));
+	}else
+	  if (pol == -1) {
+	    term_RplacTop(term1, fol_Or());
+	    list_Rplaca(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termLneg,list_List(termRneg))));
+	    list_RplacSecond(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termL,list_List(termR))));
+	  }
+      }  
+    if (!list_Empty(term_ArgumentList(term1)))
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	vec_Push(list_Car(scan));
+  }
+  vec_SetMax(bottom);
+  return term;
+}
+
+
+static TERM cnf_MovePredicateVariablesUp(TERM Term, TERM TargetPredicateTerm,
+					 LIST VarsForTopLevel)
+/**********************************************************
+  INPUT:   A term and a predicate term which is a subterm of term
+           an equivalence.
+  RETURNS: The term where the free variables of the equivalence, which
+           must be allquantified and not in the scope of an 
+	   exist quantifier, are moved to toplevel.
+  CAUTION: The term is destructively changed.
+********************************************************/
+{
+  TERM term1;
+  LIST scan;
+  int  bottom;
+
+  bottom = vec_ActMax();
+  vec_Push(Term);
+  
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (!list_Empty(term_ArgumentList(term1)))
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) {
+	TERM arg;
+	arg = (TERM) list_Car(scan);
+	if (term_HasProperSuperterm(TargetPredicateTerm, arg)) {
+	  if (symbol_Equal(term_TopSymbol(arg), fol_All())) {
+	    LIST predicatevarscan, quantifiervars;
+	    quantifiervars = fol_QuantifierVariables(arg);
+	    for (predicatevarscan=VarsForTopLevel; !list_Empty(predicatevarscan);
+		predicatevarscan = list_Cdr(predicatevarscan))
+	      quantifiervars = list_DeleteElementFree(quantifiervars, 
+						      (TERM) list_Car(predicatevarscan),
+						      (BOOL (*)(POINTER,POINTER))term_Equal,
+						      (void (*)(POINTER))term_Delete);
+	    if (!list_Empty(quantifiervars))
+	      term_RplacArgumentList(term_FirstArgument(arg), quantifiervars);
+	    else {
+	      TERM subterm;
+	      subterm = term_SecondArgument(arg);
+	      term_Free(term_FirstArgument(arg));
+	      list_Delete(term_ArgumentList(arg));
+	      term_Free(arg);
+	      list_Rplaca(scan, subterm);
+	      term_RplacSuperterm(subterm, term1);
+	    }
+	  }
+	  vec_Push((TERM) list_Car(scan));
+	}
+      }
+  }
+  
+  for (scan=VarsForTopLevel; !list_Empty(scan); scan = list_Cdr(scan))
+    list_Rplaca(scan, term_Copy((TERM) list_Car(scan)));
+  if (symbol_Equal(term_TopSymbol(Term), fol_All())) {
+    LIST vars;
+    vars = fol_QuantifierVariables(Term);
+    vars = list_Nconc(vars, list_Copy(VarsForTopLevel));
+    vars = term_DestroyDuplicatesInList(vars);
+    term_RplacArgumentList(term_FirstArgument(Term), vars);
+  }
+  else {
+    TERM newtop;
+    newtop = fol_CreateQuantifier(fol_All(), list_Copy(VarsForTopLevel), list_List(Term));
+    term_RplacSuperterm(Term, newtop);
+    Term = newtop;
+  }
+  vec_SetMax(bottom);
+  return Term;
+}
+
+
+static TERM cnf_RemoveImplFromFormulaPath(TERM Term, TERM PredicateTerm)
+/**********************************************************
+  INPUT:   A term and a predicate term which is a subterm of term
+  RETURNS: The term where implications along the path to PredicateTerm 
+           are replaced.
+  CAUTION: The term is destructively changed.
+           This works only if the superterm member of Term and its 
+	   subterms are set.
+********************************************************/
+{
+  TERM term1;
+  LIST scan;
+  int  bottom;
+  
+  bottom = vec_ActMax();
+  vec_Push(Term);
+  
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (term_HasProperSuperterm(PredicateTerm, term1)) {
+      if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
+	TERM newterm;
+	term_RplacTop(term1, fol_Or());
+	newterm = term_CreateAddFather(fol_Not(), list_List(list_Car(term_ArgumentList(term1))));
+	list_Rplaca(term_ArgumentList(term1), newterm);
+	term_RplacSuperterm(newterm, term1);
+      }
+      
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	  vec_Push(list_Car(scan));
+    }
+  }
+  vec_SetMax(bottom);
+  return Term;
+}
+
+
+static SYMBOL cnf_GetDualSymbol(SYMBOL symbol)
+/********************************************************
+  INPUT:   A predefined symbol.
+  RETURNS: The dual symbol.
+********************************************************/
+{
+  SYMBOL dual;
+
+  dual = symbol;
+  if (symbol_Equal(symbol,fol_All()))
+    dual = fol_Exist();
+  else
+    if (symbol_Equal(symbol,fol_Exist()))
+      dual = fol_All();
+    else
+      if (symbol_Equal(symbol,fol_Or()))
+	dual = fol_And();
+      else
+	if (symbol_Equal(symbol,fol_And()))
+	  dual =  fol_Or();
+  return dual;
+}
+
+
+TERM cnf_NegationNormalFormula(TERM term)
+/********************************************************
+  INPUT:   A term.
+  RETURNS: The negation normal form of the term.
+  CAUTION: The term is destructively changed.
+********************************************************/
+{
+  TERM   term1,subterm,termL;
+  LIST   scan;
+  SYMBOL symbol;
+  int    bottom;
+  
+  bottom = vec_ActMax();
+  vec_Push(term);
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {	    
+      subterm = (TERM)list_Car(term_ArgumentList(term1));
+      if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) {
+	term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm)));
+	list_Delete(term_ArgumentList(term1));
+	term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm)));
+	term_Free(term_FirstArgument(subterm));
+	list_Delete(term_ArgumentList(subterm));
+	term_Free(subterm);
+	vec_Push(term1);
+      }else 
+	if (fol_IsQuantifier(term_TopSymbol(subterm))) {
+	  symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
+	  termL  = term_Create(fol_Not(),
+			       list_List(term_SecondArgument(subterm)));
+	  list_RplacSecond(term_ArgumentList(subterm), termL);
+	  term_RplacTop(term1,symbol);
+	  list_Delete(term_ArgumentList(term1));
+	  term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm)));
+	  term_Delete(subterm);
+	} else
+	  if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || 
+	      symbol_Equal(term_TopSymbol(subterm),fol_And())) {
+	    symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
+	    for (scan = term_ArgumentList(subterm);
+		 !list_Empty(scan);
+		 scan = list_Cdr(scan)) {
+	      termL = (TERM)list_Car(scan);
+	      list_Rplaca(scan, term_Create(fol_Not(),list_List(termL)));
+	    }
+	    term_RplacTop(term1,symbol);
+	    list_Delete(term_ArgumentList(term1));
+	    term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm)));
+	    term_Delete(subterm); 
+	  }
+    }
+    if (!list_Empty(term_ArgumentList(term1)))
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	vec_Push(list_Car(scan));
+  }
+  vec_SetMax(bottom);
+  return term;
+}
+
+
+static TERM cnf_QuantMakeOneVar(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: The term where all quantifiers quantify over only one variable.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  TERM   term1,termL;
+  SYMBOL quantor;
+  LIST   scan,varlist;
+  int    bottom;
+  
+  bottom = vec_ActMax();
+  vec_Push(term);       
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (fol_IsQuantifier(term_TopSymbol(term1))) {
+      quantor = term_TopSymbol(term1);
+      if (list_Length(term_ArgumentList(term_FirstArgument(term1))) > 1) {
+	varlist =
+	  list_Copy(list_Cdr(term_ArgumentList(term_FirstArgument(term1))));
+	for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) {
+	  termL = term_SecondArgument(term1);
+	  term_RplacSecondArgument(term1, fol_CreateQuantifier(quantor,list_List(list_Car(scan)),list_List(termL)));
+	}
+	for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) {
+	  term_RplacArgumentList(term_FirstArgument(term1), 
+				 list_PointerDeleteElement(term_ArgumentList(term_FirstArgument(term1)),list_Car(scan)));
+	}
+	list_Delete(varlist);
+      }
+    }
+    if (!list_Empty(term_ArgumentList(term1)))
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	vec_Push(list_Car(scan));
+  }
+  vec_SetMax(bottom);
+  return term;
+}
+
+
+static LIST cnf_GetSymbolList(LIST varlist)
+/**************************************************************
+  INPUT:   A list of variables
+  RETURNS: The list of the symbols of the variables.
+***************************************************************/
+{
+  LIST scan,result;
+
+  result = list_Nil();
+  for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan))
+    result = list_Cons((POINTER)term_TopSymbol((TERM)list_Car(scan)),result);
+
+  return result;
+}
+
+
+static BOOL cnf_TopIsAnd(LIST termlist)
+/**************************************************************
+  INPUT:   A list of terms.
+  RETURNS: True if one term in termlist is a conjunction.
+***************************************************************/
+{
+  LIST scan;
+
+  for (scan=termlist;!list_Empty(scan);scan=list_Cdr(scan))
+    if (term_TopSymbol(list_Car(scan)) == fol_And())
+      return TRUE;
+  return FALSE;
+}
+
+
+static TERM cnf_MakeOneOr(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all arguments of an or together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+
+  LIST   scan;
+
+  if (symbol_Equal(term_TopSymbol(term),fol_Or())) {
+    TERM   argterm;
+    scan=term_ArgumentList(term);
+    while (!list_Empty(scan)) {
+      argterm = (TERM)list_Car(scan);
+      cnf_MakeOneOr(argterm);
+      if (symbol_Equal(term_TopSymbol(argterm),fol_Or())) {
+	scan = list_Cdr(scan);
+	term_RplacArgumentList(term,
+			       list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm)));
+	term_Free(argterm);
+      }
+      else
+	scan = list_Cdr(scan);
+    }
+  } else if (!symbol_IsPredicate(term_TopSymbol(term)))
+    for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan))
+      cnf_MakeOneOr(list_Car(scan));
+  
+  return term;
+}
+
+
+static TERM cnf_MakeOneOrPredicate(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all predicates and negated predicates as arguments 
+           of an or together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+
+  LIST   scan,scan1,predlist;
+
+  if (cnf_TopIsAnd(term_ArgumentList(term))) {
+    
+    for (scan1=term_ArgumentList(term);
+	 !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_And()));
+	 scan1=list_Cdr(scan1));
+
+    if (!list_Empty(scan1)) {
+      predlist = list_Nil();
+      for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) {
+	if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
+	    fol_IsNegativeLiteral(list_Car(scan))) {
+	  predlist = list_Cons(list_Car(scan),predlist);
+	}
+      }
+      for (scan=predlist;!list_Empty(scan);scan=list_Cdr(scan))
+	term_RplacArgumentList(term,
+			       list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan)));
+      
+      if (!list_Empty(predlist))
+	term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term)));
+    }
+  }
+  return term;
+}
+
+
+static TERM cnf_MakeOneOrTerm(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all predicates as arguments of an or together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  return cnf_MakeOneOrPredicate(cnf_MakeOneOr(term));
+}
+
+
+static TERM cnf_MakeOneAnd(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all arguments of an and together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   scan;
+
+  if (symbol_Equal(term_TopSymbol(term),fol_And())) {
+    TERM   argterm;
+    scan=term_ArgumentList(term);
+    while (!list_Empty(scan)) {
+      argterm = (TERM)list_Car(scan);
+      cnf_MakeOneAnd(argterm);
+      if (symbol_Equal(term_TopSymbol(argterm),fol_And())) {
+	scan = list_Cdr(scan);
+	term_RplacArgumentList(term,
+			       list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm)));
+	term_Free(argterm);
+      }
+      else
+	scan = list_Cdr(scan);
+    }
+  } else if (!symbol_IsPredicate(term_TopSymbol(term)))
+    for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan))
+      cnf_MakeOneAnd(list_Car(scan));
+
+  return term;
+}
+
+
+static TERM cnf_MakeOneAndPredicate(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all predicates as arguments of one or together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   scan,scan1,predlist;
+  
+  for (scan1=term_ArgumentList(term);
+       !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_Or()));
+       scan1=list_Cdr(scan1));
+  
+  if (!list_Empty(scan1)) {
+    /* The car of scan1 points to a term with topsymbol 'or' */
+    predlist = list_Nil();
+    for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) {
+      if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) &&
+	  fol_IsNegativeLiteral(list_Car(scan))) {
+	predlist = list_Cons(list_Car(scan),predlist);
+      }
+    }
+    for (scan=predlist; !list_Empty(scan); scan=list_Cdr(scan))
+      term_RplacArgumentList(term, list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan)));
+    
+    if (!list_Empty(predlist))
+      term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term)));
+  }
+  return term;
+}
+
+
+static TERM cnf_MakeOneAndTerm(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Takes all predicates as arguments of an or together.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  return cnf_MakeOneAndPredicate(cnf_MakeOneAnd(term));
+}
+
+
+LIST cnf_ComputeLiteralLists(TERM Term)
+/**********************************************************
+  INPUT:   A term in negation normal form without quantifiers.
+  RETURNS: The list of all literal lists corresponding to the
+           CNF of Term.
+***********************************************************/
+{
+  LIST   Scan, Scan1, Scan2, Help, Result, List1, List2, NewResult;
+  SYMBOL Symbol;
+
+  Symbol = term_TopSymbol(Term);
+  Result = list_Nil();
+
+  if (symbol_Equal(Symbol,fol_Or())) {
+    Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term)));
+    for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+      Help      = cnf_ComputeLiteralLists(list_Car(Scan));
+      NewResult = list_Nil();
+      for (Scan1=Help;!list_Empty(Scan1);Scan1=list_Cdr(Scan1))	    
+	for (Scan2=Result;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) {
+	  List1 = list_Car(Scan1);
+	  List2 = list_Car(Scan2);
+	  if (!list_Empty(list_Cdr(Scan2)))
+	    List1 = term_CopyTermList(List1);
+	  if (!list_Empty(list_Cdr(Scan1))) 
+	    List2 = term_CopyTermList(List2);
+	  NewResult = list_Cons(term_DestroyDuplicatesInList(list_Nconc(List1,List2)),
+				NewResult);
+	}
+      list_Delete(Help);
+      list_Delete(Result);
+      Result = NewResult;
+    }
+    return Result;
+  }
+
+  if (symbol_Equal(Symbol,fol_And())) {
+    Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term)));
+    for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+      Result = list_Nconc(cnf_ComputeLiteralLists(list_Car(Scan)), Result);
+    }
+    return Result;
+  }
+  
+  if (symbol_Equal(Symbol,fol_Not()) || symbol_IsPredicate(Symbol))
+    return list_List(list_List(term_Copy(Term)));
+  
+    
+  misc_StartErrorReport();
+  misc_ErrorReport("\n In cnf_ComputeLiteralLists: Unexpected junctor in input Formula!\n");
+  misc_FinishErrorReport();
+
+  return Result;
+}
+
+
+static TERM cnf_DistributiveFormula(TERM Formula)
+/**************************************************************
+  INPUT:   A Formula in NNF which consists only of disjunctions and
+           conjunctions.
+  RETURNS: The Formula where the distributivity rule is exhaustively applied
+           and all disjunctions and the top level conjunction are grouped.
+  CAUTION: The Formula is destructively changed.
+***************************************************************/
+{
+  TERM Result;
+  LIST Scan, Lists;
+
+  Lists = cnf_ComputeLiteralLists(Formula);
+  
+  for (Scan= Lists; !list_Empty(Scan); Scan=list_Cdr(Scan))
+    list_Rplaca(Scan,term_Create(fol_Or(), list_Car(Scan)));
+
+  Result = term_Create(fol_And(), Lists);
+  term_Delete(Formula);
+
+  return Result;
+}
+
+
+
+void cnf_FPrintClause(TERM term, FILE* file)
+/**************************************************************
+  INPUT:   A term and a file pointer.
+  RETURNS: Nothing.
+  EFFECT:  Print the term which contains only disjunctions to file.
+           The disjunctions represent a clause.
+***************************************************************/
+{
+    
+  TERM   term1;
+  LIST   scan;
+  int    bottom;
+  
+  bottom = vec_ActMax();
+  vec_Push(term);       
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (symbol_Equal(term_TopSymbol(term1),fol_Or())) {
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	vec_Push(list_Car(scan));
+    }else
+      term_FPrint(file,term1);
+  }
+  fputs(".\n", file);
+  vec_SetMax(bottom);
+}
+
+
+void cnf_FPrint(TERM term, FILE* file)
+/**************************************************************
+  INPUT:   A term and a file pointer.
+  RETURNS: Nothing.
+  EFFECT:  Print the term (in negation normal form)
+           which contains only conjunctions of 
+	   disjunctions to file. The conjunctions are interpreted 
+	   to represent different clauses.
+***************************************************************/
+{
+  TERM   term1;
+  LIST   scan;
+  int    bottom;
+  
+  bottom = vec_ActMax();
+  vec_Push(term);       
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (symbol_Equal(term_TopSymbol(term1),fol_And())) {
+      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	vec_Push(list_Car(scan));
+    }else
+      if (symbol_Equal(term_TopSymbol(term1),fol_Or()) ||
+	  symbol_IsPredicate(term_TopSymbol(term1)) ||
+	  symbol_Equal(term_TopSymbol(term1),fol_Not()))
+	cnf_FPrintClause(term1,file);
+  }
+  vec_SetMax(bottom);
+}
+
+
+void cnf_StdoutPrint(TERM term)
+/**************************************************************
+  INPUT:   A term.
+  RETURNS: Nothing.
+  EFFECT:  Print the term (in negation normal form)
+           which contains only conjunctions of 
+	   disjunctions to standard out. The conjunctions are interpreted 
+	   to represent different clauses.
+***************************************************************/
+{
+  LIST termlist,scan,scan1;
+
+  for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
+    termlist = list_Nil();
+    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
+	  fol_IsNegativeLiteral(list_Car(scan))))
+      termlist = term_ArgumentList(list_Car(scan));
+    
+    if (!list_Empty(termlist)) {
+      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1))
+	term_Print(list_Car(scan1));
+      puts(".");
+    }else{
+      term_Print(list_Car(scan));
+      puts(".");
+    }
+  }
+}
+
+
+void cnf_FilePrint(TERM term, FILE* file)
+/**************************************************************
+  INPUT:   A term and a file.
+  RETURNS: Nothing.
+  EFFECT:  Print the term (in negation normal form)
+           which contains only conjunctions of 
+	   disjunctions to file. The conjunctions are interpreted 
+	   to represent different clauses.
+***************************************************************/
+{
+  LIST termlist,scan,scan1;
+
+  for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
+    termlist = list_Nil();
+    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
+	  fol_IsNegativeLiteral(list_Car(scan))))
+      termlist = term_ArgumentList(list_Car(scan));
+    
+    if (!list_Empty(termlist)) {
+      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1))
+	term_FPrint(file,list_Car(scan1));
+      fputs(".\n", file);
+    }else{
+      term_FPrint(file,list_Car(scan));
+      fputs(".\n", file);
+    }
+  }
+  
+}
+
+
+void cnf_FilePrintPrefix(TERM term, FILE* file)
+/**************************************************************
+  INPUT:   A term and a file pointer.
+  RETURNS: Nothing.
+  EFFECT:  Prefix Print the term (in negation normal form)
+           which contains only conjunctions of 
+	   disjunctions to file. The conjunctions are interpreted 
+	   to represent different clauses.
+***************************************************************/
+{
+  LIST termlist,scan,scan1;
+
+  for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan)) {
+    termlist = list_Nil();
+    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
+	  fol_IsNegativeLiteral(list_Car(scan))))
+      termlist = term_ArgumentList(list_Car(scan));
+    
+    if (!list_Empty(termlist)) {
+      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1)) {
+	term_FPrintPrefix(file,list_Car(scan1));
+	if (!list_Empty(list_Cdr(scan1)))
+	  fputs(" | ", file);
+      }
+      fputs(".\n", file);
+    } else {
+      term_FPrintPrefix(file,list_Car(scan));
+      fputs(".\n", file);
+    }
+  }
+}
+
+
+static LIST cnf_SubsumeClauseList(LIST clauselist)
+/**********************************************************
+  INPUT:   A list of clauses.
+  RETURNS: The list of clauses without subsumed clauses.
+  CAUTION: The list is destructively changed.
+***********************************************************/
+{
+  LIST     scan,result;
+  st_INDEX stindex;
+  CLAUSE   actclause;
+
+  stindex = st_IndexCreate();
+  result  = list_Nil();
+
+  for (scan = clauselist; !list_Empty(scan); scan=list_Cdr(scan))
+    res_InsertClauseIndex(list_Car(scan),stindex);
+
+  for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
+    actclause     = list_Car(scan);
+    res_DeleteClauseIndex(actclause,stindex);
+    if (!res_BackSubWithLength(actclause,stindex)) {
+      res_InsertClauseIndex(actclause,stindex);
+      result = list_Cons(actclause,result);
+    }
+  }
+  if (list_Length(result) != list_Length(clauselist)) {
+    for (scan = result; !list_Empty(scan); scan=list_Cdr(scan))
+      clauselist = list_PointerDeleteElement(clauselist,list_Car(scan));
+    if (!list_Empty(result))
+      clause_DeleteClauseList(clauselist);
+  }else
+    list_Delete(clauselist);
+  st_IndexDelete(stindex);
+  return result;
+}
+
+
+static LIST cnf_MakeClauseList(TERM term, BOOL Sorts, BOOL Conclause,
+			       FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A term in cnf and two boolean values indicating
+           whether sorts should be generated and whether the
+	   generated clauses are Conclauses, a flag store and
+	   a precedence.
+  RETURNS: A list of clauses with respect to term. The terms 
+           in the new clauses are the copied subterms from term.
+  EFFECT:  The flag store and the precedence are not changed,
+           but they're needed for creating clauses.
+***************************************************************/
+{
+  LIST   termlist,scan,clauselist,newclauselist,delclauselist,condlist;
+  CLAUSE clause;
+  int    j;
+
+  termlist   = list_Nil();
+  clauselist = list_Nil();
+
+  if (fol_IsTrue(term))
+    return  clauselist;
+
+  if (fol_IsNegativeLiteral(term) || symbol_IsPredicate(term_TopSymbol(term))) {
+    termlist = list_List(term_Copy(term));
+    clause = clause_CreateFromLiterals(termlist, Sorts, Conclause,TRUE,
+				       Flags, Precedence);
+    clauselist = list_Nconc(clauselist,list_List(clause));
+    term_StartMinRenaming();
+    term_Rename(clause_GetLiteralTerm(clause,0));
+    list_Delete(termlist);
+    return clauselist;
+  }
+
+  delclauselist = list_Nil();
+  term          = cnf_MakeOneAndTerm(term);
+  if (symbol_Equal(term_TopSymbol(term), fol_And())) {
+    for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
+      list_Rplaca(scan, cnf_MakeOneOrTerm(list_Car(scan)));
+      termlist = list_Nil();
+      if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
+	    fol_IsNegativeLiteral(list_Car(scan)))) {
+	termlist = term_CopyTermList(term_ArgumentList(list_Car(scan)));
+	termlist = term_DestroyDuplicatesInList(termlist);
+      } else
+	termlist = list_List(term_Copy(list_Car(scan)));
+  
+      if (!list_Empty(termlist)) {
+	clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE,
+					   Flags, Precedence);
+	term_StartMinRenaming();
+	for (j = 0; j < clause_Length(clause); j++)
+	  term_Rename(clause_GetLiteralTerm(clause,j));
+	clauselist = list_Cons(clause,clauselist);
+	list_Delete(termlist);
+      }
+    }
+  } else {
+    /* Here the term is a disjunction, i.e. there is only one clause */
+    term = cnf_MakeOneOrTerm(term);
+    if (!(symbol_IsPredicate(term_TopSymbol(term)) ||
+	  fol_IsNegativeLiteral(term))) {
+      termlist = term_CopyTermList(term_ArgumentList(term));
+      termlist = term_DestroyDuplicatesInList(termlist);
+    } else
+      termlist = list_List(term_Copy(term));
+    
+    if (!list_Empty(termlist)) {
+      clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE,
+					 Flags, Precedence);
+      term_StartMinRenaming();
+      for (j = 0; j < clause_Length(clause); j++)
+	term_Rename(clause_GetLiteralTerm(clause,j));
+      clauselist = list_Cons(clause,clauselist);
+      list_Delete(termlist);
+    }
+  }
+
+  for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
+    condlist = cond_CondFast(list_Car(scan));
+    if (!list_Empty(condlist))
+      clause_DeleteLiterals(list_Car(scan), condlist, Flags, Precedence);
+    list_Delete(condlist);
+  }
+  clauselist    = cnf_SubsumeClauseList(clauselist);
+  newclauselist = list_Nil();
+  while (!list_Empty(clauselist)) {
+    clause = res_SelectLightestClause(clauselist);
+    newclauselist = list_Nconc(newclauselist,list_List(clause));
+    clauselist = list_PointerDeleteElement(clauselist,clause);
+  }
+  list_Delete(clauselist);
+  for (scan=newclauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
+    if (res_HasTautology(list_Car(scan)))
+      delclauselist = list_Cons(list_Car(scan),delclauselist);
+  }
+  for (scan=delclauselist; !list_Empty(scan); scan=list_Cdr(scan))
+    newclauselist = list_PointerDeleteElement(newclauselist,list_Car(scan));
+  clause_DeleteClauseList(delclauselist);
+    
+  return newclauselist;
+}
+
+
+TERM cnf_Flatten(TERM Term, SYMBOL Symbol)
+/**************************************************************
+  INPUT:   A <Term> and <Symbol> that is assumed to be associative.
+  RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
+           as long as it contains further direct subterms starting with <Symbol>
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   Scan1,Scan2;
+
+  if (symbol_Equal(term_TopSymbol(Term), Symbol)) {
+    TERM   Argterm;
+    Scan1 =term_ArgumentList(Term);
+    while (!list_Empty(Scan1)) {
+      Argterm = (TERM)list_Car(Scan1);
+      Scan2   = list_Cdr(Scan1);
+      if (symbol_Equal(term_TopSymbol(Argterm),Symbol)) {
+	cnf_Flatten(Argterm,Symbol);
+	list_NInsert(Scan1,list_Cdr(term_ArgumentList(Argterm)));   /* Be efficient ... */
+	list_Rplaca(Scan1,list_Car(term_ArgumentList(Argterm)));
+	list_Free(term_ArgumentList(Argterm));
+	term_Free(Argterm);
+      }
+      Scan1  = Scan2;
+    }
+  }
+  return Term;
+}
+
+
+static TERM cnf_FlattenPath(TERM Term, TERM PredicateTerm)
+/**************************************************************
+  INPUT:   A <Term> and <Symbol> that is assumed to be associative,
+           and a predicate term which is a subterm of term
+  RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
+           as long as it contains further direct subterms starting with <Symbol>
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  TERM   subterm;
+  
+  subterm = Term;
+  while (symbol_Equal(term_TopSymbol(subterm), fol_All()))
+    subterm = term_SecondArgument(subterm);
+
+  if (symbol_Equal(term_TopSymbol(subterm), fol_Or())) {
+    TERM Argterm;
+    LIST scan1;
+    scan1 = term_ArgumentList(subterm);
+    while (!list_Empty(scan1)) {
+      LIST scan2;
+      Argterm = (TERM)list_Car(scan1);
+      scan2   = list_Cdr(scan1);
+      if (term_HasProperSuperterm(PredicateTerm, Argterm)) {
+	if (symbol_Equal(term_TopSymbol(Argterm),fol_Or())) {
+	  LIST l;
+	  cnf_Flatten(Argterm,fol_Or());
+	  for (l=term_ArgumentList(Argterm); !list_Empty(l); l=list_Cdr(l))
+	    term_RplacSuperterm((TERM) list_Car(l), subterm);
+	  list_NInsert(scan1,list_Cdr(term_ArgumentList(Argterm)));   /* Be efficient ... */
+	  list_Rplaca(scan1,list_Car(term_ArgumentList(Argterm)));
+	  list_Free(term_ArgumentList(Argterm));
+	  term_Free(Argterm);
+	}
+      }
+      scan1  = scan2;
+    }
+  }
+  return Term;
+}
+
+
+static void cnf_DistrQuantorNoVarSub(TERM Term)
+/**************************************************************
+  INPUT:   A formula in negation normal form starting with a universal 
+           (existential) quantifier and a disjunction (conjunction) as argument.
+  EFFECT:  The Quantor is distributed if possible.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   Variables,Subformulas,Scan1,Scan2,Rest;
+  TERM   Subterm,Var,NewForm;
+  SYMBOL Subtop,Top;
+
+  Top       = term_TopSymbol(Term);
+  Variables = list_Copy(fol_QuantifierVariables(Term));
+  Subterm   = term_SecondArgument(Term);
+  Subtop    = term_TopSymbol(Subterm);
+  Subterm   = cnf_Flatten(Subterm,Subtop);
+
+  for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
+    Subformulas = list_Nil();
+    Var         = (TERM)list_Car(Scan1);
+    for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
+      if (!fol_VarOccursFreely(Var,list_Car(Scan2)))
+	Subformulas = list_Cons(list_Car(Scan2),Subformulas);
+    if (!list_Empty(Subformulas)) {
+      Rest     = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas);
+      if (list_Empty(list_Cdr(Rest))) { /* One subformula */
+	if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */
+	  NewForm = (TERM)list_Car(Rest);
+	  term_RplacArgumentList(term_FirstArgument(NewForm),
+				 list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm)));
+	  list_Delete(Rest);
+	}
+	else
+	  NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),Rest);
+      }
+      else
+	NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),list_List(term_Create(Subtop,Rest)));
+      term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas));
+      term_RplacArgumentList(term_FirstArgument(Term),
+			     list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var));
+    } 
+  }
+
+  if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */
+    term_Free(term_FirstArgument(Term));
+    list_Delete(term_ArgumentList(Term));
+    term_RplacTop(Term,Subtop);
+    term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+    term_Free(Subterm);
+  }
+  list_Delete(Variables);
+}
+
+
+static TERM cnf_AntiPrenex(TERM Term)
+/**************************************************************
+  INPUT:   A formula in negation normal form.
+  RETURNS: The term after application of anti-prenexing. Quantifiers
+           are moved inside as long as possible.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   Scan;
+  SYMBOL Top;
+
+  Top = term_TopSymbol(Term);
+
+  if (fol_IsQuantifier(Top)) {
+    TERM   Subterm,Actterm;
+    SYMBOL DistrSymb,Subtop;          /* The junctor the respective quantifier distributes over */
+    
+    Subterm = term_SecondArgument(Term);
+    Subtop  = term_TopSymbol(Subterm);
+
+    if (!symbol_IsPredicate(Subtop) && 
+	!symbol_Equal(Subtop,fol_Not())) { /* Formula in NNF: No Literals or Atoms */
+      if (symbol_Equal(Top,fol_All()))
+	DistrSymb = fol_And();
+      else
+	DistrSymb = fol_Or();
+      if (fol_IsQuantifier(Subtop)) {
+	cnf_AntiPrenex(Subterm);
+	Subtop = term_TopSymbol(Subterm);
+      }
+      if (symbol_Equal(Subtop,DistrSymb)) {
+	LIST Variables;	
+	LIST NewVars;
+	Variables = fol_QuantifierVariables(Term);
+	Subterm   = cnf_Flatten(Subterm,DistrSymb);
+	for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+	  Actterm = (TERM)list_Car(Scan);
+	  NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables,
+				    (BOOL (*)(POINTER,POINTER))term_Equal);
+	  if (!list_Empty(NewVars)) {
+	    if (symbol_Equal(Top,term_TopSymbol(Actterm))) {        /* Quantor already there */
+	      term_CopyTermsInList(NewVars);
+	      term_RplacArgumentList(term_FirstArgument(Actterm),
+				     list_Nconc(fol_QuantifierVariables(Actterm),
+						NewVars));
+	    }
+	    else {
+	      term_CopyTermsInList(NewVars);
+	      list_Rplaca(Scan,fol_CreateQuantifier(Top, NewVars, list_List(Actterm)));
+	    }
+	  }
+	}
+	term_Delete(term_FirstArgument(Term));   /* Delete old variable list */
+	list_Delete(term_ArgumentList(Term)); 
+	term_RplacTop(Term,DistrSymb);
+	term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+	term_Free(Subterm);
+	for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) 
+	  list_Rplaca(Scan,cnf_AntiPrenex(list_Car(Scan)));
+      }
+      else 
+	if (!fol_IsQuantifier(Subtop)) {
+	  cnf_DistrQuantorNoVarSub(Term);
+	  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
+	    cnf_AntiPrenex(list_Car(Scan));
+	}
+    }
+  }
+  else
+    if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top))
+      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
+	cnf_AntiPrenex(list_Car(Scan));
+
+  return Term;
+}
+
+
+static void cnf_DistrQuantorNoVarSubPath(TERM Term, TERM PredicateTerm)
+/**************************************************************
+  INPUT:   A formula in negation normal form starting with a universal 
+           (existential) quantifier and a disjunction (conjunction) as argument
+	   and a predicate term which is a subterm of term.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   Variables,Subformulas,Scan1,Scan2,Rest;
+  TERM   Subterm,Var,NewForm;
+  SYMBOL Subtop,Top;
+
+  /*fputs("\nAN0:\t",stdout);term_Print(Term);*/
+
+  Top       = term_TopSymbol(Term);
+  Variables = list_Copy(fol_QuantifierVariables(Term));
+  Subterm   = term_SecondArgument(Term);
+  Subtop    = term_TopSymbol(Subterm);
+  Subterm   = cnf_Flatten(Subterm,Subtop);
+
+  /*fputs("\nAN1:\t",stdout);term_Print(Subterm);*/
+
+  for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
+    Subformulas = list_Nil();
+    Var         = (TERM)list_Car(Scan1);
+    /* Find subterms in which the variable does not occur freely */
+    for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
+      if (!fol_VarOccursFreely(Var,list_Car(Scan2)))
+	Subformulas = list_Cons(list_Car(Scan2),Subformulas);
+    if (!list_Empty(Subformulas)) {
+      /* Rest is the list of those subterms where the variable does occur freely */
+      Rest     = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas);
+      if (list_Empty(list_Cdr(Rest))) { /* One subformula */
+	if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */
+	  NewForm = (TERM)list_Car(Rest);
+	  /* Move one variable down */
+	  term_RplacArgumentList(term_FirstArgument(NewForm),
+				 list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm)));
+	  list_Delete(Rest);
+	}
+	else {
+	  NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var),
+						  Rest);
+	}
+      }
+      else {
+	TERM t;
+	t = term_CreateAddFather(Subtop,Rest);
+	NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var),list_List(t));
+      }
+      if (term_HasProperSuperterm(PredicateTerm, NewForm))
+	NewForm = cnf_AntiPrenexPath(NewForm, PredicateTerm);
+      term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas));
+      term_RplacSuperterm(NewForm, Subterm);
+      term_RplacArgumentList(term_FirstArgument(Term),
+			     list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var));
+    } 
+  }
+
+  if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */
+    LIST l;
+    term_Free(term_FirstArgument(Term));
+    list_Delete(term_ArgumentList(Term));
+    term_RplacTop(Term,Subtop);
+    term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+    term_Free(Subterm);
+    for (l=term_ArgumentList(Term); !list_Empty(l); l=list_Cdr(l))
+      term_RplacSuperterm((TERM) list_Car(l), Term);
+  }
+  list_Delete(Variables);
+}
+
+
+static TERM cnf_AntiPrenexPath(TERM Term, TERM PredicateTerm)
+/**************************************************************
+  INPUT:   A formula in negation normal form and a predicate term
+           which is a subterm of term.
+  RETURNS: The term after application of anti-prenexing. Quantifiers
+           are moved inside along the path as long as possible.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  LIST   Scan;
+  SYMBOL Top;
+
+  Top = term_TopSymbol(Term);
+
+  if (fol_IsQuantifier(Top)) {
+    TERM   Subterm,Actterm;
+    SYMBOL DistrSymb,Subtop;          /* The junctor the respective quantifier distributes over */
+    
+    Subterm = term_SecondArgument(Term);
+    Subtop  = term_TopSymbol(Subterm);
+
+    if (!symbol_Equal(Subtop,fol_Not()) && !symbol_IsPredicate(Subtop)) { /* No Literals or Atoms */
+      if (symbol_Equal(Top,fol_All()))
+	DistrSymb = fol_And();
+      else
+	DistrSymb = fol_Or();
+      if (fol_IsQuantifier(Subtop)) {
+	cnf_AntiPrenexPath(Subterm, PredicateTerm);
+	Subtop = term_TopSymbol(Subterm);
+      }
+      if (symbol_Equal(Subtop,DistrSymb)) {
+	LIST Variables;	
+	LIST NewVars;
+	Variables = fol_QuantifierVariables(Term);
+	Subterm   = cnf_Flatten(Subterm,DistrSymb);
+	term_AddFatherLinks(Subterm);
+	/*
+	  for (l=term_ArgumentList(Subterm); !list_Empty(l); l=list_Cdr(l))
+	  term_RplacSuperterm((TERM) list_Car(l), Subterm);
+	*/
+	for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+	  Actterm = (TERM)list_Car(Scan);
+	  NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables,
+				    (BOOL (*)(POINTER,POINTER))term_Equal);
+	  if (!list_Empty(NewVars)) {
+	    if (symbol_Equal(Top,term_TopSymbol(Actterm))) {         /* Quantor already there */
+	      term_CopyTermsInList(NewVars);
+	      term_RplacArgumentList(term_FirstArgument(Actterm),
+				     list_Nconc(fol_QuantifierVariables(Actterm), NewVars));
+	    }
+	    else {
+	      term_CopyTermsInList(NewVars);
+	      list_Rplaca(Scan,fol_CreateQuantifierAddFather(Top, NewVars, list_List(Actterm)));
+	    }
+	  }
+	}
+	term_Delete(term_FirstArgument(Term));   /* Delete old variable list */
+	list_Delete(term_ArgumentList(Term)); 
+	term_RplacTop(Term,DistrSymb);
+	term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+	term_Free(Subterm);
+	term_AddFatherLinks(Term);
+	for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+	  term_RplacSuperterm((TERM) list_Car(Scan), Term);
+	  if (term_HasPointerSubterm((TERM) list_Car(Scan), PredicateTerm)) {
+	    puts("\ncheck1");
+	    list_Rplaca(Scan,cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm));
+	    term_RplacSuperterm((TERM) list_Car(Scan), Term);
+	  }
+	}
+      }
+      else
+	if (!fol_IsQuantifier(Subtop)) {
+	  cnf_DistrQuantorNoVarSubPath(Term, PredicateTerm);
+	  for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+	    if (term_HasPointerSubterm(list_Car(Scan), PredicateTerm))
+	      cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm);
+	  }
+	}
+    }
+  }
+  else
+    if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top))
+      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
+	if (term_HasProperSuperterm(PredicateTerm, (TERM) list_Car(Scan)))
+	  cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm);
+  
+  term_AddFatherLinks(Term);
+  return Term;
+}
+
+
+static TERM cnf_RemoveTrivialOperators(TERM Term)
+/**************************************************************
+  INPUT:   A formula.
+  RETURNS: The formula after
+           removal of "or" and "and" with only one argument
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  SYMBOL Top;
+  LIST   Scan;
+
+  Top = term_TopSymbol(Term);
+
+  if (symbol_IsPredicate(Top))
+    return Term;
+
+  if ((symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or())) &&
+      list_Empty(list_Cdr(term_ArgumentList(Term)))) {
+    TERM Result;
+    Result = term_FirstArgument(Term);
+    term_RplacSuperterm(Result, term_Superterm(Term));
+    list_Delete(term_ArgumentList(Term));
+    term_Free(Term);
+    return cnf_RemoveTrivialOperators(Result);
+  }
+
+  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+    list_Rplaca(Scan,cnf_RemoveTrivialOperators(list_Car(Scan)));
+    term_RplacSuperterm((TERM) list_Car(Scan), Term);
+  }
+  
+  return Term;
+}
+
+
+static TERM cnf_SimplifyQuantors(TERM Term)
+  /**************************************************************
+  INPUT:   A formula.
+  RETURNS: The formula after
+	   removal of bindings of variables that don't occur in the
+	   respective subformula and possible mergings of quantors
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  SYMBOL Top;
+  LIST   Scan;
+
+  Top = term_TopSymbol(Term);
+
+  if (symbol_IsPredicate(Top) || symbol_Equal(Top,fol_Varlist()))
+    return Term;
+
+  if (fol_IsQuantifier(Top)) {
+    LIST Vars;
+    TERM Var,Subterm,Aux;
+    Vars    = list_Nil();
+    Subterm = term_SecondArgument(Term);
+
+    while (symbol_Equal(term_TopSymbol(Subterm),Top)) {
+      term_RplacArgumentList(term_FirstArgument(Term),
+			     list_Nconc(fol_QuantifierVariables(Term),fol_QuantifierVariables(Subterm)));
+      term_Free(term_FirstArgument(Subterm));
+      Aux = term_SecondArgument(Subterm);
+      list_Delete(term_ArgumentList(Subterm));
+      term_Free(Subterm);
+      list_Rplaca(list_Cdr(term_ArgumentList(Term)),Aux);
+      Subterm = Aux;
+    }
+    
+    for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+      Var = (TERM)list_Car(Scan);
+      if (!fol_VarOccursFreely(Var,Subterm))
+	Vars = list_Cons(Var,Vars);
+    }
+    if (!list_Empty(Vars)) {
+      Subterm = term_FirstArgument(Term);
+      term_RplacArgumentList(Subterm,list_NPointerDifference(term_ArgumentList(Subterm),Vars));
+      term_DeleteTermList(Vars);
+      if (list_Empty(term_ArgumentList(Subterm))) {
+	Subterm = term_SecondArgument(Term);
+	term_Delete(term_FirstArgument(Term));
+	list_Delete(term_ArgumentList(Term));
+	term_Free(Term);
+	return cnf_SimplifyQuantors(Subterm);
+      }
+    }
+  }
+  
+  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
+    list_Rplaca(Scan,cnf_SimplifyQuantors(list_Car(Scan)));
+  
+  return Term; 
+}
+
+
+TERM cnf_RemoveTrivialAtoms(TERM Term)
+/**************************************************************
+  INPUT:   A formula.
+  RETURNS: The formula where occurrences of the atoms "true"
+           and "false" are propagated and eventually removed.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  SYMBOL Top,Subtop;
+  LIST   Scan;
+  TERM   Result;
+  BOOL   Update;
+
+
+  if (!term_IsComplex(Term))
+    return Term;
+  
+  Top    = term_TopSymbol(Term);
+  Update = FALSE;
+
+  if (symbol_Equal(Top,fol_And())) {
+    Scan  = term_ArgumentList(Term);
+    while (!list_Empty(Scan)) {
+      Result = cnf_RemoveTrivialAtoms(list_Car(Scan));
+      Subtop = term_TopSymbol(Result);
+      if (symbol_Equal(Subtop,fol_True()))
+	Update = TRUE;
+      else
+	if (symbol_Equal(Subtop,fol_False())) {
+	  term_RplacTop(Term,fol_False());
+	  term_DeleteTermList(term_ArgumentList(Term));
+	  term_RplacArgumentList(Term,list_Nil());
+	  return Term;
+	}
+      Scan = list_Cdr(Scan);
+    }
+    if (Update) {
+      term_RplacArgumentList(Term,fol_DeleteTrueTermFromList(term_ArgumentList(Term)));
+      if (list_Empty(term_ArgumentList(Term))) {
+	term_RplacTop(Term,fol_True());
+	return Term;
+      }
+    }
+  }
+  else if (symbol_Equal(Top,fol_Or())) {
+    Scan  = term_ArgumentList(Term);
+    while (!list_Empty(Scan)) {
+      Result = cnf_RemoveTrivialAtoms(list_Car(Scan));
+      Subtop = term_TopSymbol(Result);
+      if (symbol_Equal(Subtop,fol_False()))
+	Update = TRUE;
+      else
+	if (symbol_Equal(Subtop,fol_True())) {
+	  term_RplacTop(Term,fol_True());
+	  term_DeleteTermList(term_ArgumentList(Term));
+	  term_RplacArgumentList(Term,list_Nil());
+	  return Term;
+	}
+      Scan = list_Cdr(Scan);
+    }
+    if (Update) {
+      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
+      if (list_Empty(term_ArgumentList(Term))) {
+	term_RplacTop(Term,fol_False());
+	return Term;
+      }
+    }
+  }
+  else if (fol_IsQuantifier(Top) || symbol_Equal(Top,fol_Not())) {
+    if (fol_IsQuantifier(Top))
+      Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
+    else
+      Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
+    Subtop = term_TopSymbol(Result);
+    if ((symbol_Equal(Subtop,fol_False()) && symbol_Equal(Top,fol_Not())) ||
+	(symbol_Equal(Subtop,fol_True()) && fol_IsQuantifier(Top))) {
+      term_RplacTop(Term,fol_True());
+      term_DeleteTermList(term_ArgumentList(Term));
+      term_RplacArgumentList(Term,list_Nil());
+      return Term;
+    }
+    else
+      if ((symbol_Equal(Subtop,fol_True()) && symbol_Equal(Top,fol_Not())) ||
+	  (symbol_Equal(Subtop,fol_False()) && fol_IsQuantifier(Top))) {
+	term_RplacTop(Term,fol_False());
+	term_DeleteTermList(term_ArgumentList(Term));
+	term_RplacArgumentList(Term,list_Nil());
+	return Term;
+      }
+  }
+  else if (symbol_Equal(Top,fol_Implies())) {
+    Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
+    Subtop = term_TopSymbol(Result);
+    if (symbol_Equal(Subtop,fol_False())) {
+      term_RplacTop(Term,fol_True());
+      term_DeleteTermList(term_ArgumentList(Term));
+      term_RplacArgumentList(Term,list_Nil());
+      return Term;
+    }
+    else if (symbol_Equal(Subtop,fol_True())) {
+      term_Delete(Result);
+      Result = term_SecondArgument(Term);
+      list_Delete(term_ArgumentList(Term));
+      term_RplacTop(Term,term_TopSymbol(Result));
+      term_RplacArgumentList(Term,term_ArgumentList(Result));
+      term_Free(Result);
+      return cnf_RemoveTrivialAtoms(Term);
+    }
+    Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
+    Subtop = term_TopSymbol(Result);
+    if (symbol_Equal(Subtop,fol_True())) {
+      term_RplacTop(Term,fol_True());
+      term_DeleteTermList(term_ArgumentList(Term));
+      term_RplacArgumentList(Term,list_Nil());
+      return Term;
+    }
+    else if (symbol_Equal(Subtop,fol_False())) {
+      term_RplacTop(Term,fol_Not());
+      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
+    }
+  }
+  else if (symbol_Equal(Top,fol_Equiv())) {
+    Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
+    Subtop = term_TopSymbol(Result);
+    if (symbol_Equal(Subtop,fol_False())) {
+      term_RplacTop(Term,fol_Not());
+      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
+      if (list_Empty(term_ArgumentList(Term))) {
+	term_RplacTop(Term, fol_True());
+	return Term;
+      }
+      return cnf_RemoveTrivialAtoms(Term);
+    }
+    else if (symbol_Equal(Subtop,fol_True())) {
+      term_Delete(Result);
+      Result = term_SecondArgument(Term);
+      list_Delete(term_ArgumentList(Term));
+      term_RplacTop(Term,term_TopSymbol(Result));
+      term_RplacArgumentList(Term,term_ArgumentList(Result));
+      term_Free(Result);
+      return cnf_RemoveTrivialAtoms(Term);
+    }
+    Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
+    Subtop = term_TopSymbol(Result);
+    if (symbol_Equal(Subtop,fol_False())) {
+      term_RplacTop(Term,fol_Not());
+      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
+    }
+    else if (symbol_Equal(Subtop,fol_True())) {
+      term_Delete(Result);
+      Result = term_FirstArgument(Term);
+      list_Delete(term_ArgumentList(Term));
+      term_RplacTop(Term,term_TopSymbol(Result));
+      term_RplacArgumentList(Term,term_ArgumentList(Result));
+      term_Free(Result);
+    }
+  }
+
+  return Term;
+}
+
+
+TERM cnf_ObviousSimplifications(TERM Term)
+/**************************************************************
+  INPUT:   A formula.
+  RETURNS: The formula after performing the following simplifications:
+             - remove "or" and "and" with only one argument
+	     - remove bindings of variables that don't occur in the
+	       respective subformula
+	     - merge quantors
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  Term = cnf_RemoveTrivialAtoms(Term);
+  Term = cnf_RemoveTrivialOperators(Term);
+  Term = cnf_SimplifyQuantors(Term);
+
+  return Term;
+}
+
+
+/* EK: warum wird Term zurueckgegeben, wenn er destruktiv geaendert wird??? */
+static TERM cnf_SkolemFormula(TERM Term, PRECEDENCE Precedence, LIST* Symblist)
+/**************************************************************
+  INPUT:   A formula in negation normal form, a precedence and pointer
+           to a list used as return value.
+  RETURNS: The skolemized term and the list of introduced Skolem functions.
+  CAUTION: The term is destructively changed.
+           The precedence of the new Skolem functions is set in <Precedence>.
+***************************************************************/
+{
+  SYMBOL Top,SkolemSymbol;
+  TERM   Subterm,SkolemTerm;
+  LIST   Varlist,Scan;
+  NAT    Arity;
+
+  Top = term_TopSymbol(Term);
+    
+  if (fol_IsQuantifier(term_TopSymbol(Term))) {
+    if (symbol_Equal(Top,fol_All())) {
+      term_Delete(term_FirstArgument(Term));
+      Subterm = term_SecondArgument(Term);
+      list_Delete(term_ArgumentList(Term));
+      term_RplacTop(Term,term_TopSymbol(Subterm));
+      term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+      term_Free(Subterm);
+      return cnf_SkolemFormula(Term, Precedence, Symblist);
+    } 
+    else {  /* exist quantifier */
+      Varlist = fol_FreeVariables(Term);
+      Arity   = list_Length(Varlist);
+      for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
+	SkolemSymbol = symbol_CreateSkolemFunction(Arity, Precedence);
+	*Symblist  = list_Cons((POINTER)SkolemSymbol, *Symblist);
+	SkolemTerm = term_Create(SkolemSymbol,Varlist); /* Caution: Sharing of Varlist ! */
+	fol_ReplaceVariable(term_SecondArgument(Term),term_TopSymbol(list_Car(Scan)),SkolemTerm);
+	term_Free(SkolemTerm);
+      }
+      list_Delete(Varlist);
+      term_Delete(term_FirstArgument(Term));
+      Subterm = term_SecondArgument(Term);
+      list_Delete(term_ArgumentList(Term));
+      term_RplacTop(Term,term_TopSymbol(Subterm));
+      term_RplacArgumentList(Term,term_ArgumentList(Subterm));
+      term_Free(Subterm);
+      return cnf_SkolemFormula(Term, Precedence, Symblist);
+    } 
+  }
+  else
+    if (symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or()))
+      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
+	cnf_SkolemFormula(list_Car(Scan), Precedence, Symblist);
+  return Term;
+}
+
+
+static TERM cnf_Cnf(TERM Term, PRECEDENCE Precedence, LIST* Symblist)
+/**************************************************************
+  INPUT:   A formula, a precedence and a pointer to a list of symbols
+           used as return value.
+  RETURNS: The term is transformed to conjunctive normal form.
+  EFFECT:  The term is destructively changed and not normalized.
+           The precedence of new Skolem symbols is set in <Precedence>.
+***************************************************************/
+{
+  /* Necessary because ren_Rename crashes if a e.g. and() has only one argument */
+  Term = cnf_ObviousSimplifications(Term);
+  term_AddFatherLinks(Term);
+  Term = ren_Rename(Term, Precedence, Symblist, FALSE, FALSE);
+  Term = cnf_RemoveEquivImplFromFormula(Term);
+  Term = cnf_NegationNormalFormula(Term);
+  Term = cnf_SkolemFormula(cnf_AntiPrenex(Term), Precedence, Symblist);
+  Term = cnf_DistributiveFormula(Term);
+
+  return Term;
+}
+
+
+static LIST cnf_GetUsedTerms(CLAUSE C, PROOFSEARCH Search,
+			     HASH InputClauseToTermLabellist) 
+/**************************************************************
+  INPUT:   
+  RETURNS: 
+***************************************************************/
+{
+  LIST UsedTerms, Used2, Scan;
+  UsedTerms = list_Copy(hsh_Get(InputClauseToTermLabellist, C));
+  UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms);
+  if (!list_Empty(UsedTerms))
+    return UsedTerms;
+
+  for (Scan = clause_ParentClauses(C); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+    CLAUSE P;
+    int ClauseNumber;
+    ClauseNumber = (int) list_Car(Scan);
+    P = clause_GetNumberedCl(ClauseNumber, prfs_WorkedOffClauses(Search));
+    if (P == NULL) {
+      P = clause_GetNumberedCl(ClauseNumber, prfs_UsableClauses(Search));
+      if (P == NULL)
+	P = clause_GetNumberedCl(ClauseNumber, prfs_DocProofClauses(Search));
+    }
+    Used2 = cnf_GetUsedTerms(P, Search, InputClauseToTermLabellist);
+    UsedTerms = list_Nconc(UsedTerms, Used2);
+  }
+  return UsedTerms;
+}
+
+
+static BOOL cnf_HaveProofOptSkolem(PROOFSEARCH Search, TERM topterm,
+				   char* toplabel, TERM term2,
+				   LIST* UsedTerms, LIST* Symblist,
+				   HASH InputClauseToTermLabellist)
+/**************************************************************
+  INPUT:   
+  RETURNS: ??? EK
+***************************************************************/
+{
+  LIST       ConClauses, EmptyClauses;
+  LIST       scan;
+  BOOL       found;
+  LIST       Usables;
+  FLAGSTORE  Flags;
+  PRECEDENCE Precedence;
+
+  Flags      = prfs_Store(Search);
+  Precedence = prfs_Precedence(Search);
+  ConClauses = list_Nil();
+  found      = FALSE;
+  /* List of clauses from term2 */
+  term_AddFatherLinks(term2);
+  term2      = cnf_Cnf(term2, Precedence, Symblist);
+  Usables    = cnf_MakeClauseList(term2, FALSE, FALSE, Flags, Precedence);
+  term_Delete(term2);
+
+  for (scan=Usables; !list_Empty(scan); scan = list_Cdr(scan)) {
+    clause_SetFlag(list_Car(scan), CONCLAUSE);
+    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
+#ifdef CHECK
+      hsh_Check(InputClauseToTermLabellist);
+#endif
+      hsh_Put(InputClauseToTermLabellist, list_Car(scan), toplabel);
+#ifdef CHECK_CNF
+      fputs("\nUsable : ", stdout);
+      clause_Print(list_Car(scan));
+      printf(" Label %s", toplabel);
+#endif
+    }
+  }
+  EmptyClauses = cnf_SatUnit(Search, Usables);
+  if (!list_Empty(EmptyClauses)) {
+    found = TRUE;
+#ifdef CHECK_CNF
+    fputs("\nHaveProof : Empty Clause : ", stdout);
+    clause_Print((CLAUSE) list_Car(EmptyClauses));
+    putchar('\n');
+#endif
+    if (flag_GetFlagValue(Flags, flag_DOCPROOF))
+      *UsedTerms = list_Nconc(*UsedTerms, cnf_GetUsedTerms((CLAUSE) list_Car(EmptyClauses), Search, InputClauseToTermLabellist));
+    EmptyClauses = list_PointerDeleteDuplicates(EmptyClauses);
+    clause_DeleteClauseList(EmptyClauses);
+  }
+    
+  /* Removing ConClauses from UsablesIndex */
+  ConClauses = list_Copy(prfs_UsableClauses(Search));
+  for (scan = ConClauses; !list_Empty(scan); scan = list_Cdr(scan))
+    if (flag_GetFlagValue(Flags, flag_DOCPROOF))
+      prfs_MoveUsableDocProof(Search, (CLAUSE) list_Car(scan));
+    else
+      prfs_DeleteUsable(Search, (CLAUSE) list_Car(scan));
+  list_Delete(ConClauses); 
+	
+  return found;
+}
+
+
+BOOL cnf_HaveProof(LIST TermList, TERM ToProve, FLAGSTORE InputFlags,
+		   PRECEDENCE InputPrecedence)
+/**************************************************************
+  INPUT:   A list of terms, a term to prove, a flag store and a precedence.
+           The arguments are not changed.
+  RETURNS: True if the termlist implies ToProve
+  CAUTION: All terms are copied.
+***************************************************************/
+{
+  PROOFSEARCH search;
+  LIST        scan, usables, symblist, emptyclauses;
+  BOOL        found;
+  FLAGSTORE   Flags;
+  PRECEDENCE  Precedence;
+
+  /* Use global PROOFSEARCH object to avoid stamp overflow */
+  search  = cnf_HAVEPROOFPS;
+  usables = symblist = list_Nil();
+
+  /* Initialize search object's flag store */
+  Flags = prfs_Store(search);
+  flag_CleanStore(Flags);
+  flag_InitFlotterSubproofFlags(InputFlags, Flags);
+  /* Initialize search object's precedence */
+  Precedence = prfs_Precedence(search);
+  symbol_TransferPrecedence(InputPrecedence, Precedence);
+
+  /* Build list of clauses from the termlist */
+  for (scan=TermList; !list_Empty(scan); scan=list_Cdr(scan)) {
+    TERM t;
+    t = term_Copy(list_Car(scan));
+    t = cnf_Cnf(t, Precedence, &symblist);
+
+    usables = list_Nconc(cnf_MakeClauseList(t,FALSE,FALSE,Flags,Precedence),
+			 usables);
+    term_Delete(t); 
+  }
+
+  /* Build clauses from negated term to prove */
+  ToProve = term_Create(fol_Not(), list_List(term_Copy(ToProve)));
+  term_AddFatherLinks(ToProve);
+  ToProve = cnf_Cnf(ToProve, Precedence, &symblist);
+  usables = list_Nconc(cnf_MakeClauseList(ToProve,FALSE,FALSE,Flags,Precedence),
+		       usables);
+  term_Delete(ToProve);
+
+  /* SatUnit requires the CONCLAUSE flag */
+  for (scan=usables;!list_Empty(scan); scan = list_Cdr(scan))
+    clause_SetFlag(list_Car(scan), CONCLAUSE);
+
+  emptyclauses = cnf_SatUnit(search, usables);
+  
+  if (!list_Empty(emptyclauses)) {
+    found = TRUE;
+    emptyclauses = list_PointerDeleteDuplicates(emptyclauses);
+    clause_DeleteClauseList(emptyclauses);
+  }
+  else
+    found = FALSE;
+  prfs_Clean(search);
+  symbol_DeleteSymbolList(symblist);
+
+  return found;
+}
+
+
+static void cnf_RplacVarsymbFunction(TERM term, SYMBOL varsymb, TERM function)
+/**********************************************************
+  INPUT:   A term, a variable symbol and a function.
+  EFFECT:  The variable with the symbol  varsymb in the term 
+           is replaced by the function function.
+  CAUTION: The term is destructively changed.
+***********************************************************/
+{
+  int  bottom;
+  TERM term1;
+  LIST scan;
+
+  bottom = vec_ActMax();
+  vec_Push(term);
+
+  while (bottom != vec_ActMax()) {
+    term1 = (TERM)vec_PopResult();
+    if (symbol_Equal(term_TopSymbol(term1),varsymb)) {
+      term_RplacTop(term1,term_TopSymbol(function));
+      term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(function)));
+    }else
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	  vec_Push(list_Car(scan));
+  }
+  vec_SetMax(bottom);
+}
+
+
+static void cnf_RplacVar(TERM Term, LIST Varlist, LIST Termlist)
+/**********************************************************
+  INPUT:   A term,a variable symbol and a function.
+  RETURNS: The variable with the symbol  varsymb in the term 
+           is replaced by the function function.
+  CAUTION: The term is destructively changed.
+***********************************************************/
+{
+  int  bottom;
+  TERM term1;
+  LIST scan,scan2;
+
+  bottom = vec_ActMax();
+  vec_Push(Term);
+
+  while (bottom != vec_ActMax()) {
+    term1 = vec_PopResult();
+    if (symbol_IsVariable(term_TopSymbol(term1))) {
+      BOOL done;
+      done = FALSE;
+      for (scan=Varlist, scan2=Termlist; !list_Empty(scan) && !done; 
+	   scan = list_Cdr(scan), scan2 = list_Cdr(scan2)) {
+	if (symbol_Equal(term_TopSymbol(term1),term_TopSymbol(list_Car(scan)))) {
+	  term_RplacTop(term1,term_TopSymbol((TERM) list_Car(scan2)));
+	  term_RplacArgumentList(term1,
+				 term_CopyTermList(term_ArgumentList(list_Car(scan2))));
+	  done = TRUE;
+	}
+      }
+    }
+    else
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	  vec_Push(list_Car(scan));
+  }
+  vec_SetMax(bottom);
+}
+
+
+static TERM cnf_MakeSkolemFunction(LIST varlist, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A list of variables and a precedence.
+  RETURNS: The new term oskf... (oskc...) which is a function 
+           with varlist as arguments.
+  EFFECT:  The precedence of the new Skolem function is set in <Precedence>.
+***************************************************************/
+{
+  TERM   term;
+  SYMBOL skolem;
+  
+  skolem = symbol_CreateSkolemFunction(list_Length(varlist), Precedence);
+  term   = term_Create(skolem, term_CopyTermList(varlist));
+  return term;
+}
+
+
+static void cnf_PopAllQuantifier(TERM term)
+/********************************************************
+ INPUT:   A term whose top symbol is fol_all.
+ RETURNS: Nothing.
+ EFFECT:  Removes the quantifier
+********************************************************/
+{
+  TERM SubTerm;
+  LIST VarList;
+
+#ifdef CHECK
+  if (!symbol_Equal(term_TopSymbol(term), fol_All())) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_PopAllQuantifier: Top symbol is not fol_All !\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  VarList = term_ArgumentList(term_FirstArgument(term));
+  term_DeleteTermList(VarList);
+  term_Free(term_FirstArgument(term));
+  SubTerm = term_SecondArgument(term);
+  list_Delete(term_ArgumentList(term));
+  term_RplacTop(term,term_TopSymbol(SubTerm));
+  term_RplacArgumentList(term,term_ArgumentList(SubTerm));
+  term_Free(SubTerm);
+}
+
+
+static TERM cnf_QuantifyAndNegate(TERM term, LIST VarList, LIST FreeList)
+/****************************************************************
+  INPUT:   A term, a list of variables to be exist-quantified,
+           a list of variables to be all-quantified
+  RETURNS: not(forall[FreeList](exists[VarList](term)))
+  MEMORY:  The term, the lists and their arguments are copied.
+***************************************************************/
+{
+  TERM Result;
+  TERM TermCopy;
+  LIST VarListCopy;
+  LIST FreeListCopy;
+
+  TermCopy = term_Copy(term);
+  VarListCopy = term_CopyTermList(VarList);
+  Result = fol_CreateQuantifier(fol_Exist(),VarListCopy,list_List(TermCopy));
+  FreeListCopy = list_Nil();
+
+  FreeList = fol_FreeVariables(Result);
+  if (!list_Empty(FreeList)) {
+    FreeListCopy = term_CopyTermList(FreeList);
+    list_Delete(FreeList);
+    Result = fol_CreateQuantifier(fol_All(), FreeListCopy, list_List(Result));
+  }
+  Result = term_Create(fol_Not(), list_List(Result));
+  return Result;
+}
+
+
+static TERM cnf_MoveProvedTermToTopLevel(TERM Term, TERM Term1, TERM Proved,
+					 LIST VarList, LIST FreeList,
+					 PRECEDENCE Precedence)
+/********************************************************************
+  INPUT:   A top-level term, which must be a conjunction,
+           a subterm <Term1> of <Term>, a subterm <Proved> of <Term1>,
+	   a list of existence quantified variables <VarList>,
+	   a list of free variables <FreeList> and a precedence.
+           <Term1> is of the form
+	   exists[...](t1 and t2 and ... and Proved and ..)
+  RETURNS: A new term, where <Proved> is removed from the arguments
+           of <Term1>.
+  EFFECT:  The precedence of new Skolem functions is set in <Precedence>
+*******************************************************************/
+{
+  TERM termR;
+  TERM skolemfunction;
+  SYMBOL varsymb;
+  LIST scan;
+
+  termR = term_SecondArgument(Term1); /* t1 and t2 and ... and Proved ... */
+  term_RplacArgumentList(termR,
+			 list_PointerDeleteElement(term_ArgumentList(termR),
+						   Proved));
+  if (list_Length(term_ArgumentList(termR)) < 2) {
+    TERM termRL = term_FirstArgument(termR);     /* t1 */
+    list_Delete(term_ArgumentList(termR));
+    term_RplacTop(termR, term_TopSymbol(termRL));
+    term_RplacArgumentList(termR,term_ArgumentList(termRL));
+    term_Free(termRL);
+  }
+
+  for (scan = VarList; scan != list_Nil(); scan = list_Cdr(scan)) {
+    varsymb = term_TopSymbol(list_Car(scan));
+    skolemfunction = cnf_MakeSkolemFunction(FreeList, Precedence);
+    cnf_RplacVarsymbFunction(termR,varsymb,skolemfunction);
+    cnf_RplacVarsymbFunction(Proved,varsymb,skolemfunction); 
+    term_Delete(skolemfunction); 
+  }
+
+  if (!list_Empty(FreeList)) {
+    Proved = 
+      fol_CreateQuantifier(fol_All(), term_CopyTermList(FreeList),
+			   list_List(Proved));
+    if (list_Length(FreeList) > 1)
+      Proved = cnf_QuantMakeOneVar(Proved);
+  }
+ 
+  term_Delete(term_FirstArgument(Term1)); /* Variables of "exists" */
+  list_Delete(term_ArgumentList(Term1));
+  term_RplacTop(Term1,term_TopSymbol(termR));
+  term_RplacArgumentList(Term1,term_ArgumentList(termR));
+  term_Free(termR);
+    
+  term_RplacArgumentList(Term, list_Cons(Proved, term_ArgumentList(Term)));
+  return Proved;
+}
+
+
+static void cnf_Skolemize(TERM Term, LIST FreeList, PRECEDENCE Precedence)
+/********************************************************
+  INPUT:   A existence quantified term, the list of free variables
+           and a precedence.
+  RETURNS: Nothing.
+  EFFECT:  The term is destructively changed, i.e. the
+           existence quantifier is removed by skolemization.
+	   The precedence of new Skolem functions is set in <Precedence>.
+*********************************************************/
+{
+  LIST exlist;
+  TERM subterm;
+  LIST symblist;
+
+  symblist = list_Nil();
+  exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term)));
+  term_Delete(term_FirstArgument(Term));
+  subterm = term_SecondArgument(Term);
+  list_Delete(term_ArgumentList(Term));
+  term_RplacTop(Term,term_TopSymbol(subterm));
+  term_RplacArgumentList(Term,term_ArgumentList(subterm));
+  term_Free(subterm);
+  symblist = cnf_SkolemFunctionFormula(Term, FreeList, exlist, Precedence);
+  list_Delete(exlist);
+  list_Delete(symblist);
+}
+
+
+static LIST cnf_FreeVariablesBut(TERM Term, LIST Symbols)
+/********************************************************
+  INPUT:   A term and a list of symbols
+  RETURNS: A list of all free variable terms in Term whose symbols are 
+           not in Symbols
+*********************************************************/
+{
+  LIST follist, Scan;
+  follist = fol_FreeVariables(Term);
+  for (Scan = follist; !list_Empty(Scan); Scan = list_Cdr(Scan))
+    if (list_Member(Symbols, (POINTER)term_TopSymbol(list_Car(Scan)),
+		    (BOOL (*)(POINTER,POINTER))symbol_Equal))
+      list_Rplaca(Scan,NULL);
+  follist = list_PointerDeleteElement(follist,NULL);
+    
+  return follist;
+}
+
+
+static void cnf_SkolemFunctionFormulaMapped(TERM term, LIST allist, LIST map)
+/**************************************************************
+  INPUT:   A term  term and a  list allist of variables and a list map
+           of pairs (variable symbols, function symbol)
+  RETURNS: None.
+  CAUTION: The term is destructively changed. All variable symbols
+           in map which appear in term are replaced by the skolem functions
+	   with respect to allist which contains the universally quantified
+	   variables.
+***************************************************************/
+{
+  TERM   term1;
+  LIST   scan,scan1;
+  SYMBOL skolem, symbol;
+  int    bottom;
+
+  bottom = vec_ActMax();
+  
+  for (scan1=map; !list_Empty(scan1); scan1=list_Cdr(scan1)) {
+    vec_Push(term);
+    symbol = (SYMBOL) list_PairFirst((LIST) list_Car(scan1));
+    skolem = (SYMBOL) list_PairSecond((LIST) list_Car(scan1));
+
+#ifdef CHECK_STRSKOLEM
+    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+      fputs("\nVariable : ", stdout);
+      symbol_Print(symbol);
+      fputs("\nFunction : ", stdout);
+      symbol_Print(skolem);
+    }
+#endif
+    while (bottom != vec_ActMax()) {
+      term1 = (TERM)vec_PopResult();
+
+      if (symbol_Equal(term_TopSymbol(term1),symbol)) {
+	term_RplacTop(term1,skolem);
+	list_Delete(term_ArgumentList(term1));
+	term_RplacArgumentList(term1,term_CopyTermList(allist));
+      }
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) {
+	  vec_Push(list_Car(scan));
+	}
+    }
+  }
+  vec_SetMax(bottom);
+}
+
+
+static BOOL cnf_HasDeeperVariable(LIST List1, LIST List2)
+/******************************************************************
+   INPUT:   Two lists of variable terms
+   RETURNS: TRUE if a variable in the first list is deeper than all variables
+            in the second list, FALSE otherwise.
+   NOTE:    If cnf_VARIABLEDEPTHARRAY is not allocated this will crash
+            If new variables are introduced by strong skolemization, their
+            depth is -1.
+*******************************************************************/
+{
+  LIST scan;
+  int  maxdepth1;
+  
+  /* Determine maximum depth of variables in List1 */
+  maxdepth1 = 0;
+  for (scan=List1; !list_Empty(scan); scan=list_Cdr(scan)) {
+    int i;
+    i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))];
+#ifdef CHECK_STRSKOLEM
+    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+      fputs("\nFor variable ", stdout);
+      symbol_Print(term_TopSymbol((TERM) list_Car(scan)));
+      printf(" depth is %d.", i);
+    }
+#endif
+    if (i > maxdepth1)
+      maxdepth1 = i;
+  }
+
+  /* Compare with depth of variables in List2 */
+  for (scan=List2; !list_Empty(scan); scan=list_Cdr(scan)) {
+    int i;
+    i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))];
+#ifdef CHECK_STRSKOLEM
+    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+      fputs("\nFor variable ", stdout);
+      symbol_Print(term_TopSymbol((TERM) list_Car(scan)));
+      printf(" depth is %d.", i);
+    }
+#endif
+    if (i >= maxdepth1)
+      return FALSE;
+  }
+  return  TRUE;
+}
+
+
+static void cnf_StrongSkolemization(PROOFSEARCH Search, TERM Topterm,
+				    char* Toplabel, BOOL TopAnd, TERM Term, 
+				    LIST* UsedTerms, LIST* Symblist,
+				    BOOL Result1,
+				    HASH InputClauseToTermLabellist, int Depth)
+/******************************************************************
+  INPUT:   An existence quantified formula. ??? EK
+  RETURNS: Nothing.
+  EFFECT:  The existence quantifier is removed by strong skolemization.
+           The precedence of new Skolem symbols is set in the precedence
+	   of the search object.
+*******************************************************************/
+{
+  LIST       exlist;    /* Variable symbols bound by exists[]() */
+  LIST       pairlist;  /* List of pairs (Subterm of AND, free variable symbols
+			   not in exlist) */
+  LIST       allfreevariables;
+  LIST       newvariables;       /* w2..wn*/
+  LIST       mapping;           /* List of pairs */
+  int        numberofallfreevariables, acc_length, i;
+  LIST       pair, pairscan, pairscan_pred, scan, accumulatedvariables;
+  TERM       subterm, w;
+  BOOL       strskolemsuccess;  /* Indicates whether strong skolemization was
+				   possible */
+  FLAGSTORE  Flags;
+  PRECEDENCE Precedence;
+
+  Flags      = prfs_Store(Search);
+  Precedence = prfs_Precedence(Search);
+
+  /* Necessary so that new variables really are new ! */
+  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))
+    symbol_SetStandardVarCounter(term_MaxVar(Topterm));
+
+  /* Get list of quantified variable symbols x_k */
+  exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term)));
+  /* Pop quantifier */
+  term_Delete(term_FirstArgument(Term));
+  subterm = term_SecondArgument(Term);
+  list_Delete(term_ArgumentList(Term));
+  term_RplacTop(Term,term_TopSymbol(subterm));
+  term_RplacArgumentList(Term,term_ArgumentList(subterm));
+  term_Free(subterm);
+
+  /* Now for every argument get the list of free variables whose symbols
+     are not in exlist */
+  pairlist = list_Nil();
+  for (scan=term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) {
+    pair = list_PairCreate((TERM) list_Car(scan), 
+			   cnf_FreeVariablesBut((TERM) list_Car(scan), exlist));
+    if (list_Empty(pairlist)) 
+      pairlist = list_List(pair);
+    else {
+      /* First sort subterms by number of free variables */
+      int pairlength, currentlength;
+      pairlength = list_Length((LIST) list_PairSecond(pair));
+      pairscan = pairlist; 
+      pairscan_pred = list_Nil();
+      currentlength = 0;
+      while (!list_Empty(pairscan)) {
+	currentlength = list_Length((LIST) list_PairSecond((LIST) list_Car(pairscan)));
+	if (currentlength < pairlength) {
+	  pairscan_pred = pairscan;
+	  pairscan = list_Cdr(pairscan);
+	}
+	else if (currentlength == pairlength) {
+	  /* If both subterms have the same number of free variables compare depth of variables */
+	  if (cnf_HasDeeperVariable((LIST) list_PairSecond((LIST) list_Car(pairscan)), /* in list */
+				   (LIST) list_PairSecond(pair))) {                   /* new pair */
+#ifdef CHECK_STRSKOLEM
+	    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+	      fputs("\nTerm ", stdout);
+	      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
+	      fputs("\n has deeper variable than ", stdout);
+	      term_Print((TERM) list_PairFirst(pair));
+	    }
+#endif	    
+	    pairscan_pred = pairscan;
+	    pairscan = list_Cdr(pairscan);
+	  }
+	  else
+	    break;
+	}
+	else
+	  break;
+      }
+      
+      /* New pair has more variables than all others in list */
+      if (list_Empty(pairscan))
+	list_Rplacd(pairscan_pred, list_List(pair));
+      /* New pair is inserted between pairscan_pred and pairscan */
+      else if (currentlength >= pairlength) { 
+	/* Head of list */
+	if (list_Empty(pairscan_pred))
+	  pairlist = list_Cons(pair, pairlist);
+	else 
+	  list_InsertNext(pairscan_pred, pair);
+      }
+      /* The case for the same number of variables is not yet implemented */
+    }
+  }
+
+#ifdef CHECK_STRSKOLEM
+  if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+    for (pairscan=pairlist; !list_Empty(pairscan); pairscan = list_Cdr(pairscan)) {
+      LIST l;
+      fputs("\nSubterm ", stdout);
+      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
+      fputs("\n  has free variables ", stdout);
+      for (l=(LIST) list_PairSecond((LIST) list_Car(pairscan)); !list_Empty(l); l = list_Cdr(l)) {
+	term_Print((TERM) list_Car(l));
+	fputs(" ", stdout);
+      }
+    }
+  }
+#endif
+
+  /* Determine number of all free variablein and()--term whose symbols are not in exlist */
+  /* Create map from ex_variables tp skolem symbols */
+  allfreevariables = cnf_FreeVariablesBut(Term, exlist);
+  numberofallfreevariables = list_Length(allfreevariables);
+    
+  mapping  = list_Nil();
+
+  for (scan = exlist; !list_Empty(scan); scan = list_Cdr(scan)) {
+    SYMBOL skolem;
+    skolem = symbol_CreateSkolemFunction(numberofallfreevariables, Precedence);
+    *Symblist = list_Cons((POINTER)skolem,*Symblist);
+    mapping = list_Cons(list_PairCreate(list_Car(scan), (POINTER)skolem), 
+			mapping);
+  }
+  list_Delete(allfreevariables);
+
+  /* Create new variables */
+  newvariables = list_Nil();
+
+  for (i=0; i < numberofallfreevariables; i++) {
+    w = term_CreateStandardVariable();
+    newvariables = list_Cons(w, newvariables);
+  }
+
+#ifdef CHECK_STRSKOLEM
+  if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+    LIST l;
+    fputs("\nNew variables : ", stdout);
+    for (l=newvariables; !list_Empty(l); l = list_Cdr(l)) {
+      term_Print((TERM) list_Car(l));
+      fputs(" ", stdout);
+    }
+  }
+#endif
+  
+  /* Now do the replacing */
+  accumulatedvariables = list_Nil();
+  acc_length = 0;
+  strskolemsuccess = FALSE;
+  for (pairscan=pairlist; !list_Empty(pairscan); pairscan=list_Cdr(pairscan)) {
+    LIST allist;
+
+    /* Add bound variables for this subterm */
+    accumulatedvariables = list_Nconc(accumulatedvariables,
+				      (LIST) list_PairSecond((LIST) list_Car(pairscan)));
+    accumulatedvariables = term_DeleteDuplicatesFromList(accumulatedvariables);
+
+    /* Remove new variables not (no longer) needed */
+    for (i=0; i < list_Length(accumulatedvariables) - acc_length; i++) {
+      term_Delete((TERM) list_Top(newvariables));
+      newvariables = list_Pop(newvariables);
+    }
+    acc_length = list_Length(accumulatedvariables);
+
+#ifdef CHECK_STRSKOLEM
+    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+      LIST l;
+      fputs("\n\nSubterm is ", stdout);
+      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
+      fputs("\nFree variables : ", stdout);
+      for (l=accumulatedvariables; !list_Empty(l); l = list_Cdr(l)) {
+	term_Print((TERM) list_Car(l));
+	fputs(" ", stdout);
+      }
+    }
+#endif
+    if (!list_Empty(newvariables))
+      strskolemsuccess = TRUE;
+    allist = list_Nconc(list_Copy(accumulatedvariables), list_Copy(newvariables));
+
+    cnf_SkolemFunctionFormulaMapped((TERM) list_PairFirst((LIST) list_Car(pairscan)), allist,
+				    mapping);
+#ifdef CHECK_STRSKOLEM
+    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
+      fputs("\nSubterm after skolemization : ", stdout);
+      term_Print(list_PairFirst((LIST) list_Car(pairscan)));
+    }
+#endif
+
+    list_Delete(allist);
+    cnf_OptimizedSkolemFormula(Search, Topterm, Toplabel, TopAnd,
+			       (TERM) list_PairFirst((LIST) list_Car(pairscan)),
+			       UsedTerms, Symblist, Result1, 
+			       InputClauseToTermLabellist, Depth);
+  }
+  while (!list_Empty(newvariables)) {
+    term_Delete((TERM) list_Top(newvariables));
+    newvariables = list_Pop(newvariables);
+  }
+  list_Delete(accumulatedvariables); /* Only pairs and pairlist left */
+  list_DeletePairList(pairlist);
+  list_Delete(exlist);
+  list_DeletePairList(mapping);
+  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM) && strskolemsuccess) {
+    fputs("\nStrong skolemization applied", stdout);
+  }
+}
+    
+
+static void cnf_OptimizedSkolemFormula(PROOFSEARCH Search, TERM topterm,
+				       char* toplabel, BOOL TopAnd, TERM term, 
+				       LIST* UsedTerms, LIST* Symblist,
+				       BOOL Result1,
+				       HASH InputClauseToTermLabellist,
+				       int Depth)
+/**************************************************************
+  INPUT:   Two terms in negation normal form. ??? EK
+  RETURNS: The  skolemized term with the optimized skolemization
+           due to Ohlbach and Weidenbach of <term> and further improvements.
+	   <rest> is used as additional, conjunctively added information.
+  EFFECT:  The symbol precedence of the search  object is changed
+           because new Skolem symbols are defined.
+  CAUTION: The term is destructively changed.
+***************************************************************/
+{
+  TERM       termL2, provedterm;
+  LIST       freevariables, scan, varlist;
+  SYMBOL     top;
+  BOOL       result2;
+  BOOL       optimized;
+  FLAGSTORE  Flags;
+  PRECEDENCE Precedence;
+
+  result2       = FALSE;
+  freevariables = list_Nil();
+  Flags         = prfs_Store(Search);
+  Precedence    = prfs_Precedence(Search);
+  
+  top = term_TopSymbol(term);
+  if (fol_IsQuantifier(top)) {
+    if (symbol_Equal(top,fol_All())) {
+      /* For quantified variables store depth if strong skolemization is performed */
+      if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
+	LIST variables;
+	variables = term_ArgumentList(term_FirstArgument(term));
+	for (scan=variables; !list_Empty(scan); scan=list_Cdr(scan)) {
+#ifdef CHECK_STRSKOLEM
+	  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
+	    if (cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] != -1) {
+	      fputs("\nFor variable ", stderr);
+	      term_Print((TERM) list_Car(scan));
+	      printf(" depth is already set to %d, now setting it to %d", 
+		     cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))],Depth);
+	    }
+	  }
+#endif
+#ifdef CHECK_STRSKOLEM
+	  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
+	    fputs("\nVariable ", stdout);
+	    term_Print((TERM) list_Car(scan));
+	    printf(" has depth %d in term\n  ", Depth);
+	    term_Print(term);
+	  }
+#endif
+	  cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] = Depth;
+	}
+	Depth++;
+      }
+      cnf_PopAllQuantifier(term);
+      cnf_OptimizedSkolemFormula(Search,topterm, toplabel, TopAnd, term, 
+				 UsedTerms, Symblist, Result1,
+				 InputClauseToTermLabellist, Depth);
+      return;
+    }
+    freevariables = fol_FreeVariables(term);
+    optimized = FALSE;
+    if (symbol_Equal(term_TopSymbol(term_SecondArgument(term)), fol_And())) {
+      if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM)) {
+	scan = term_ArgumentList(term_SecondArgument(term));
+	varlist = term_ArgumentList(term_FirstArgument(term));
+	while (!list_Empty(scan) && !optimized) {
+	  if (!Result1) {
+	    if (TopAnd) {
+	      if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
+		fputs("\nHaveProof not necessary", stdout);
+	      }
+	      result2 = TRUE;
+	    }
+	    else {
+	      termL2 = cnf_QuantifyAndNegate((TERM) list_Car(scan), 
+					     varlist, freevariables);
+	      result2 = cnf_HaveProofOptSkolem(Search, topterm, toplabel, termL2,
+					       UsedTerms, Symblist, 
+					       InputClauseToTermLabellist);
+#ifdef CHECK_OPTSKOLEM
+	      if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
+		fputs("\nHaveProof result : ", stdout);
+		if (result2)
+		  fputs("TRUE", stdout);
+		else
+		  fputs("FALSE", stdout);
+	      }
+#endif
+	    }
+	  }
+	    
+	  if (Result1 || result2) {
+	    optimized = TRUE;
+	    if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
+	      fputs("\nIn term ", stdout);
+	      term_Print(topterm);
+	      fputs("\n subterm ", stdout);
+	      term_Print((TERM) list_Car(scan));
+	      puts(" is moved to toplevel.");
+	    }
+	    provedterm =
+	      cnf_MoveProvedTermToTopLevel(topterm, term, list_Car(scan), 
+					   varlist, freevariables, Precedence);
+	    if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
+	      fputs("Result : ", stdout);
+	      term_Print(topterm);
+	      putchar('\n');
+	    }
+	    /* provedterm is argument of top AND term */
+	    cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TRUE,
+				       provedterm,UsedTerms, Symblist, Result1, 
+				       InputClauseToTermLabellist, Depth);
+	  }
+	  else 
+	    scan = list_Cdr(scan);
+	}
+      }
+      if (!optimized) {
+	/* Optimized skolemization not enabled or not possible */
+	if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
+	  optimized = TRUE; /* Strong Skolemization is always possible after exists[..](and(..)) */
+	  cnf_StrongSkolemization(Search, topterm, toplabel, TopAnd, term,
+				  UsedTerms, Symblist, Result1, 
+				  InputClauseToTermLabellist, Depth);
+	}
+      }
+    }
+    else
+      TopAnd = FALSE;
+    if (!optimized) {
+      /* Optimized skolemization not enabled or not possible */
+      /* Strong skolemization not enabled or not possible */
+      cnf_Skolemize(term, freevariables, Precedence);
+    }
+    list_Delete(freevariables);
+    cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd, term,UsedTerms,
+			       Symblist,Result1,InputClauseToTermLabellist,Depth);
+    return;
+  } 
+  else {
+    if (symbol_Equal(top,fol_And()) || symbol_Equal(top,fol_Or())) {
+      if (symbol_Equal(top,fol_Or()))
+	TopAnd = FALSE;
+      for (scan=term_ArgumentList(term);!list_Empty(scan);
+	   scan=list_Cdr(scan))
+	cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd,
+				   (TERM) list_Car(scan),
+				   UsedTerms, Symblist,
+				   Result1, InputClauseToTermLabellist, Depth);
+    }
+  }
+  return;
+}
+
+
+static LIST cnf_SkolemFunctionFormula(TERM term, LIST allist, LIST exlist,
+				      PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A term <term>, a list <allist> of variables, a list <exlist>
+           of variable symbols and a precedence.
+  RETURNS: The list of new Skolem functions.
+  EFFECT:  The term is destructively changed. All variable symbols
+           in <exlist> which appear in <term> are replaced by skolem functions
+	   with respect to <allist> which contains the universally quantified
+	   variables.
+	   New Skolem functions are created and their precedence is set
+	   in <Precedence>.
+***************************************************************/
+{
+  TERM   term1;
+  LIST   scan, scan1, Result;
+  SYMBOL skolem;
+  int    bottom,n;
+
+  Result = list_Nil();
+  bottom = vec_ActMax();
+  n = list_Length(allist);
+  
+  for (scan1=exlist; !list_Empty(scan1); scan1=list_Cdr(scan1)) {
+    vec_Push(term);
+    skolem = symbol_CreateSkolemFunction(n, Precedence);
+    Result = list_Cons((POINTER)skolem, Result);
+    
+    while (bottom != vec_ActMax()) {
+      term1 = (TERM)vec_PopResult();
+      if (symbol_Equal(term_TopSymbol(term1),(SYMBOL)list_Car(scan1))) {
+	term_RplacTop(term1,skolem);
+	list_Delete(term_ArgumentList(term1));
+	term_RplacArgumentList(term1,term_CopyTermList(allist));
+      }
+      if (!list_Empty(term_ArgumentList(term1)))
+	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
+	  vec_Push(list_Car(scan));
+    }
+  }
+  vec_SetMax(bottom);
+  return Result;
+}
+
+
+static LIST cnf_OptimizedSkolemization(PROOFSEARCH Search, TERM Term,
+				       char* Label, LIST* UsedTerms, 
+				       LIST* Symblist, BOOL result,
+				       BOOL Conjecture, 
+				       HASH InputClauseToTermLabellist)
+/**************************************************************
+  INPUT:   A term, a shared index and a list of non-ConClauses. ??? EK
+  RETURNS: The list of clauses derived from Term.
+  EFFECT:  The term is skolemized using optimized skolemization wrt ShIndex.
+**************************************************************/
+{
+  LIST       Clauses;
+  TERM       FirstArg;
+  int        i;
+  FLAGSTORE  Flags;
+  PRECEDENCE Precedence;
+
+#ifdef CHECK
+  if (Term == NULL) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_OptimizedSkolemization: Input term is NULL.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  Flags      = prfs_Store(Search);
+  Precedence = prfs_Precedence(Search);
+  FirstArg   = Term;
+
+  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
+    /* Initializing array */
+    for (i = 1; i <= symbol__MAXSTANDARDVAR; i++)
+      cnf_VARIABLEDEPTHARRAY[i] = -1;
+  }
+
+  if (flag_GetFlagValue(Flags, flag_POPTSKOLEM) ||
+      flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
+    fputs("\nTerm before skolemization : \n ", stdout);
+    fol_PrettyPrintDFG(Term);
+  }
+
+  if (!fol_IsLiteral(Term)) {
+    if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM) ||
+	flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))  {
+      if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM))
+	Term = term_Create(fol_And(), list_List(Term)); /* CW hack: definitions are added on top level*/
+      cnf_OptimizedSkolemFormula(Search, Term, Label, TRUE, FirstArg, UsedTerms, 
+				 Symblist, result, InputClauseToTermLabellist, 0);
+    }
+    else {
+      LIST Symbols;
+      Symbols = list_Nil();
+      Term    = cnf_SkolemFormula(Term, Precedence, &Symbols);
+      list_Delete(Symbols);
+    }
+  }
+  if (flag_GetFlagValue(Flags, flag_POPTSKOLEM) ||
+      flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
+    fputs("\nTerm after skolemization : ", stdout);
+    term_Print(Term);
+  }
+  Term    = cnf_DistributiveFormula(Term);
+  Clauses = cnf_MakeClauseList(Term, FALSE, Conjecture, Flags, Precedence);
+  term_Delete(Term);
+
+  return Clauses;
+}
+
+
+LIST cnf_GetSkolemFunctions(TERM Term, LIST ArgList, LIST* SkolToExVar)
+/**************************************************************
+  INPUT:   A term, the argumentlist of a skolem function, a mapping from
+           a skolem function to a variable
+  RETURNS: The longest argumentlist of all skolem functions found so far.
+  EFFECT:  Computes information for renaming variables and replacing 
+           skolem functions during de-skolemization.
+**************************************************************/ 
+{
+  LIST Scan;
+  SYMBOL Top;
+    
+  Top = term_TopSymbol(Term);
+
+  if (fol_IsQuantifier(Top)) 
+    return cnf_GetSkolemFunctions(term_SecondArgument(Term), ArgList, 
+				  SkolToExVar);
+
+  if (symbol_IsFunction(Top) && symbol_HasProperty(Top, SKOLEM)) {
+    BOOL found;
+    SYMBOL Var = 0;
+    int Arity;
+    found = FALSE;
+      
+    /* Keep longest argument list of all skolem functions in the clause for renaming */
+    /* Delete all other argument lists */
+    Arity = list_Length(term_ArgumentList(Term));
+    if (Arity > list_Length(ArgList)) {
+      term_DeleteTermList(ArgList);
+      ArgList = term_ArgumentList(Term);
+    }
+    else 
+      term_DeleteTermList(term_ArgumentList(Term));
+    term_RplacArgumentList(Term, NULL);
+      
+    /* Replace skolem function by variable */
+    if (list_Length(*SkolToExVar) > Arity) {
+      NAT i;
+      LIST SkolScan = *SkolToExVar;
+      for (i = 0; i < Arity; i++)
+	SkolScan = list_Cdr(SkolScan);
+      for (SkolScan = (LIST) list_Car(SkolScan);
+	   (SkolScan != list_Nil()) && !found; SkolScan = list_Cdr(SkolScan)) {
+	SYMBOL Skol;
+	Skol = (SYMBOL) list_PairFirst((LIST) list_Car(SkolScan));
+	if (Skol == term_TopSymbol(Term)) {
+	  Var = (SYMBOL) list_PairSecond((LIST) list_Car(SkolScan));
+	  found = TRUE;
+	}
+      }
+    }
+    if (!found) {
+      LIST Pair;
+      NAT  i;
+      LIST SkolScan;
+
+      SkolScan = *SkolToExVar;
+      for (i = 0; i < Arity; i++) {
+	if (list_Cdr(SkolScan) == list_Nil())
+	  list_Rplacd(SkolScan, list_List(NULL));
+	SkolScan = list_Cdr(SkolScan);
+      }
+
+      Var = symbol_CreateStandardVariable();
+      Pair = list_PairCreate((POINTER) term_TopSymbol(Term), 
+			     (POINTER) Var);
+      if (list_Car(SkolScan) == list_Nil())
+	list_Rplaca(SkolScan, list_List(Pair));
+      else
+	list_Rplaca(SkolScan, list_Nconc((LIST) list_Car(SkolScan), 
+					 list_List(Pair)));
+    }
+    term_RplacTop(Term, Var);
+  }
+  else {
+    for (Scan = term_ArgumentList(Term); Scan != list_Nil(); 
+	Scan = list_Cdr(Scan))
+      ArgList = cnf_GetSkolemFunctions((TERM) list_Car(Scan), ArgList, 
+				       SkolToExVar);
+  }
+  return ArgList;
+}
+
+
+void cnf_ReplaceVariable(TERM Term, SYMBOL Old, SYMBOL New)
+/**************************************************************
+  INPUT:  A term, two symbols that are variables
+  EFFECT: In term every occurrence of Old is replaced by New
+**************************************************************/ 
+{
+  LIST Scan;
+
+#ifdef CHECK
+  if (!symbol_IsVariable(Old)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_ReplaceVariable: Illegal input symbol.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  if (symbol_Equal(term_TopSymbol(Term), Old))
+    term_RplacTop(Term, New);
+  else 
+    for (Scan = term_ArgumentList(Term); !list_Empty(Scan); 
+	 Scan = list_Cdr(Scan))
+      cnf_ReplaceVariable(list_Car(Scan), Old, New);
+}
+
+
+LIST cnf_RemoveSkolemFunctions(CLAUSE Clause, LIST* SkolToExVar, LIST Vars)
+/**************************************************************
+  INPUT:   A clause, a list which is a mapping from skolem functions to
+           variables and a list of variables for forall-quantification.
+  RETURNS: A list of terms derived from the clause using deskolemization
+  EFFECT:  Arguments of skolem functions are renamed consistently.
+           Skolemfunctions are replaced by variables.
+**************************************************************/
+{
+  LIST Scan;
+  LIST TermScan, TermList, ArgList;
+  TERM Term;
+  int i;
+
+  TermList = list_Nil();
+
+  ArgList = list_Nil();
+  for (i = 0; i < clause_Length(Clause); i++) {
+    Term = term_Copy(clause_GetLiteralTerm(Clause, i));
+    ArgList = cnf_GetSkolemFunctions(Term, ArgList, SkolToExVar);
+    TermList = list_Cons(Term, TermList);
+  }
+    
+  if (list_Empty(ArgList))
+    return TermList;
+    
+  /* Rename variables */
+  for (Scan = ArgList; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
+    for (TermScan = TermList; TermScan != list_Nil(); 
+	 TermScan = list_Cdr(TermScan)) {
+      Term = (TERM) list_Car(TermScan);
+      cnf_ReplaceVariable(Term,
+			  term_TopSymbol((TERM) list_Car(Scan)),
+			  (SYMBOL) list_Car(Vars));
+    }
+    if (list_Cdr(Vars) == list_Nil()) {
+      SYMBOL New = symbol_CreateStandardVariable();
+      Vars = list_Nconc(Vars, list_List((POINTER) New));
+    }
+    Vars = list_Cdr(Vars);
+  }
+  term_DeleteTermList(ArgList);
+  return TermList;
+}
+
+
+TERM cnf_DeSkolemFormula(LIST Clauses)
+/**************************************************************
+  INPUT:   A list of clauses.
+  RETURNS: A formula built from the clauses.
+  EFFECT:  All skolem functions are removed from the clauses.
+**************************************************************/
+{
+  LIST Scan, SkolToExVar, Vars, FreeVars, FreeVarsCopy, VarScan, TermList;
+  TERM VarListTerm, TopTerm, Term;
+  BOOL First;
+  
+  SkolToExVar = list_List(NULL);
+  Vars = list_List((POINTER) symbol_CreateStandardVariable());
+  
+  TopTerm = term_Create(fol_And(), NULL);
+  
+  for (Scan = Clauses; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
+    TermList =  cnf_RemoveSkolemFunctions((CLAUSE) list_Car(Scan),
+					  &SkolToExVar, Vars);
+    Term = term_Create(fol_Or(), TermList);
+    FreeVars = fol_FreeVariables(Term);
+    if (!list_Empty(FreeVars)) {
+      FreeVarsCopy = term_CopyTermList(FreeVars);
+      list_Delete(FreeVars);
+      Term = fol_CreateQuantifier(fol_All(), FreeVarsCopy, list_List(Term));
+    }
+    term_RplacArgumentList(TopTerm, list_Cons(Term, term_ArgumentList(TopTerm)));
+  }
+  
+  VarScan = Vars;
+  First = TRUE;
+  
+  for (Scan = SkolToExVar; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
+    if (list_Empty(list_Car(Scan))) {
+      if (term_TopSymbol(TopTerm) == fol_All())
+	term_RplacArgumentList(TopTerm, list_Cons(term_Create((SYMBOL) list_Car(VarScan), NULL),  
+						  term_ArgumentList(TopTerm)));
+      if (!First)
+	TopTerm = fol_CreateQuantifier(fol_All(),
+				       list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)),
+				       list_List(TopTerm)); 
+    }
+    else {
+      LIST ExVarScan;
+      LIST ExVars = list_Nil();
+      for (ExVarScan = list_Car(Scan); ExVarScan != list_Nil();
+	  ExVarScan = list_Cdr(ExVarScan)) {
+	if (ExVars == list_Nil())
+	  ExVars = list_List(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL));
+	else
+	  ExVars = list_Cons(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL), ExVars);
+	list_PairFree((LIST) list_Car(ExVarScan));
+      }
+      list_Delete((LIST) list_Car(Scan));
+      list_Rplaca(Scan, NULL);
+
+      if (term_TopSymbol(TopTerm) == fol_Exist()) {
+	VarListTerm = (TERM) list_Car(term_ArgumentList(TopTerm));
+	term_RplacArgumentList(VarListTerm,
+			       list_Nconc(term_ArgumentList(VarListTerm),
+					  ExVars));
+      }
+      else
+	TopTerm = fol_CreateQuantifier(fol_Exist(), ExVars, list_List(TopTerm));
+      ExVars = list_Nil();
+
+      if (!First) 
+	TopTerm = fol_CreateQuantifier(fol_All(), 
+				       list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)),
+				       list_List(TopTerm));
+    }
+    if (!First) 
+      VarScan = list_Cdr(VarScan);
+    else
+      First = FALSE;
+	
+  }
+  list_Delete(SkolToExVar);
+  list_Delete(Vars);
+
+  return TopTerm;
+}
+
+
+#ifdef OPTCHECK
+/* Currently unused */
+/*static */
+LIST cnf_CheckOptimizedSkolemization(LIST* AxClauses, LIST* ConClauses,
+				     TERM AxTerm, TERM ConTerm,
+				     LIST NonConClauses, LIST* SkolemPredicates,
+				     SHARED_INDEX ShIndex, BOOL result)
+/**********************************************************
+  EFFECT: Used to check the correctness of optimized skolemization
+***********************************************************/
+{
+  TERM DeSkolemizedAxOpt, DeSkolemizedConOpt, DeSkolemizedAx, DeSkolemizedCon;
+  TERM TopOpt, Top, ToProve;
+  LIST SkolemFunctions2;
+
+  if (*AxClauses != list_Nil()) {
+    DeSkolemizedAxOpt = cnf_DeSkolemFormula(*AxClauses);
+    if (*ConClauses != list_Nil()) {
+      DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses);
+      TopOpt = term_Create(fol_And(), 
+			   list_Cons(DeSkolemizedAxOpt, 
+				     list_List(DeSkolemizedConOpt)));
+    }
+    else 
+      TopOpt = DeSkolemizedAxOpt;
+  }
+  else {
+    DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses);     
+    TopOpt = DeSkolemizedConOpt;
+  }
+  
+  clause_DeleteClauseList(*AxClauses);
+  clause_DeleteClauseList(*ConClauses);
+  *AxClauses = list_Nil();
+  *ConClauses = list_Nil();
+  
+  flag_SetFlagValue(flag_CNFOPTSKOLEM, flag_CNFOPTSKOLEMOFF);  
+  if (AxTerm) {
+    *AxClauses = cnf_OptimizedSkolemization(term_Copy(AxTerm), ShIndex, NonConClauses, result,FALSE, ClauseToTermLabellist);
+  }
+  if (ConTerm) {
+    *ConClauses = cnf_OptimizedSkolemization(term_Copy(ConTerm), ShIndex, NonConClauses, result,TRUE, ClauseToTermLabellist);
+  }
+  
+  if (*AxClauses != list_Nil()) {
+    DeSkolemizedAx = cnf_DeSkolemFormula(*AxClauses);
+    if (*ConClauses != list_Nil()) {
+      DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses);
+      Top = term_Create(fol_And(), 
+			list_Cons(DeSkolemizedAx, 
+				  list_List(DeSkolemizedCon)));
+    }
+    else 
+      Top = DeSkolemizedAx;
+  }
+  else {
+    DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses);    
+    Top = DeSkolemizedCon;
+  }
+  
+  clause_DeleteClauseList(*AxClauses);
+  clause_DeleteClausList(*ConClauses);
+  *AxClauses = list_Nil();
+  *ConClauses = list_Nil();
+  
+  ToProve = term_Create(fol_Equiv(), list_Cons(TopOpt, list_List(Top)));
+  ToProve = term_Create(fol_Not(), list_List(ToProve));
+  fol_NormalizeVars(ToProve); 
+  ToProve  = cnf_ObviousSimplifications(ToProve);
+  term_AddFatherLinks(ToProve);
+  ToProve  = ren_Rename(ToProve,SkolemPredicates,FALSE);
+  ToProve  = cnf_RemoveEquivImplFromFormula(ToProve);
+  ToProve  = cnf_NegationNormalFormula(ToProve);
+  ToProve  = cnf_AntiPrenex(ToProve);
+  
+  SkolemFunctions2 = list_Nil();
+  ToProve     = cnf_SkolemFormula(ToProve, &SkolemFunctions2);
+  ToProve     = cnf_DistributiveFormula(ToProve);
+  *ConClauses = cnf_MakeClauseList(ToProve);
+  if (ToProve)
+    term_Delete(ToProve);
+  *AxClauses = list_Nil();
+  return SkolemFunctions2;
+}
+#endif
+
+
+PROOFSEARCH cnf_Flotter(LIST AxiomList, LIST ConjectureList, LIST* AxClauses, 
+			LIST* AllLabels, HASH TermLabelToClauselist, 
+			HASH ClauseToTermLabellist, FLAGSTORE InputFlags,
+			PRECEDENCE InputPrecedence, LIST* Symblist)
+/**************************************************************
+  INPUT:   A list of axiom formulae,
+           a list of conjecture formulae,
+	   a pointer to a list in which clauses derived from axiom formulae 
+	   are stored,
+	   a pointer to a list in which clauses derived from 
+	   conjecture formulae are stored, ???
+	   a pointer to a list of all termlabels,
+	   a hasharray in which for every term label the list of clauses 
+	   derived from the term is stored (if DocProof is set),
+	   a hasharray in which for every clause the list of labels 
+	   of the terms used for deriving the clause is stored (if DocProof 
+	   is set),
+	   a flag store,
+	   a precedence
+	   a pointer to a list of symbols which have to be deleted later if
+	   the ProofSearch object is kept.
+  RETURNS: If KeepProofSearch ??? is TRUE, then the ProofSearch object is not
+           freed but returned.
+	   Else, NULL is returned.
+  EFFECT:  ??? EK
+           The precedence of new skolem symbols is set in <InputPrecedence>.
+***************************************************************/
+{
+  LIST        Scan, Scan2, FormulaClauses,SkolemFunctions;
+  LIST        SkolemPredicates, EmptyClauses, AllFormulae;
+  LIST        UsedTerms;
+  TERM        AxTerm,Formula;
+  BOOL        Result;
+  PROOFSEARCH Search;
+  PRECEDENCE  Precedence;
+  FLAGSTORE   Flags;
+  NAT         Count;
+  HASH        InputClauseToTermLabellist;
+
+  Search = prfs_Create();
+
+  /* Initialize the flagstore for the CNF transformation */
+  Flags = prfs_Store(Search);
+  flag_CleanStore(Flags);
+  flag_InitFlotterFlags(InputFlags, Flags);
+  /* Initialize the precedence */
+  Precedence = prfs_Precedence(Search);
+  symbol_TransferPrecedence(InputPrecedence, Precedence);
+
+  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
+    prfs_AddDocProofSharingIndex(Search);
+
+  AxTerm           = (TERM)NULL;
+  SkolemPredicates = list_Nil();
+  Result           = FALSE;
+  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
+    InputClauseToTermLabellist = hsh_Create();
+  else 
+    InputClauseToTermLabellist = NULL;
+
+  symbol_ReinitGenericNameCounters();
+
+  for (Scan = AxiomList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+    LIST Pair;
+    Pair = list_Car(Scan);
+    AxTerm = (TERM) list_PairSecond(Pair);
+    fol_RemoveImplied(AxTerm);
+    term_AddFatherLinks(AxTerm);
+    fol_NormalizeVars(AxTerm);
+    if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS))
+      cnf_PropagateSubstEquations(AxTerm);
+    AxTerm = cnf_ObviousSimplifications(AxTerm);
+    if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
+      term_AddFatherLinks(AxTerm);
+      AxTerm = ren_Rename(AxTerm, Precedence, &SkolemPredicates,
+			  flag_GetFlagValue(Flags, flag_CNFPRENAMING), TRUE);
+    }
+    AxTerm = cnf_RemoveEquivImplFromFormula(AxTerm);
+    AxTerm = cnf_NegationNormalFormula(AxTerm);
+    AxTerm = cnf_AntiPrenex(AxTerm);
+    list_Rplacd(Pair, (LIST) AxTerm);
+  }
+  AllFormulae = AxiomList;
+  
+  /* At this point the list contains max. 1 element, which is a pair 
+     of the label NULL and the negated
+     conjunction of all conjecture formulae. */
+
+  Count = 0;
+  for (Scan = ConjectureList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+    TERM  ConTerm;
+    char* Label;
+    char  buf[100];
+    /* Add label */  
+    if (list_PairFirst(list_Car(Scan)) == NULL) {
+      sprintf(buf, "conjecture%d", Count);
+      Label = string_StringCopy(buf);
+      list_Rplaca((LIST) list_Car(Scan), Label);
+      if (flag_GetFlagValue(Flags, flag_DOCPROOF) &&
+	  flag_GetFlagValue(Flags, flag_PLABELS)) {
+	printf("\nAdded label %s for conjecture", Label);
+	fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan)));
+      }
+    }
+
+    ConTerm = (TERM) list_PairSecond((LIST) list_Car(Scan));
+    fol_RemoveImplied(ConTerm);
+    term_AddFatherLinks(ConTerm);
+    fol_NormalizeVars(ConTerm);  
+    if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS))
+      cnf_PropagateSubstEquations(ConTerm);
+    ConTerm  = cnf_ObviousSimplifications(ConTerm); 
+
+    if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
+      term_AddFatherLinks(ConTerm);
+      ConTerm = ren_Rename(ConTerm, Precedence, &SkolemPredicates,
+			   flag_GetFlagValue(Flags, flag_CNFPRENAMING),TRUE);
+    }
+    /* fputs("\nRen:\t",stdout);term_Print(ConTerm);putchar('\n'); */
+    ConTerm  = cnf_RemoveEquivImplFromFormula(ConTerm);
+    ConTerm  = cnf_NegationNormalFormula(ConTerm);
+    /* fputs("\nAn:\t",stdout);term_Print(ConTerm);putchar('\n'); */
+    ConTerm  = cnf_AntiPrenex(ConTerm);
+    /* fputs("\nPr:\t",stdout);term_Print(ConTerm);putchar('\n'); */
+    /* Insert changed term into pair */
+    list_Rplacd((LIST) list_Car(Scan), (LIST) ConTerm);
+
+    Count++;
+  } 
+
+  AllFormulae = list_Append(ConjectureList, AllFormulae);
+  for (Scan = ConjectureList;!list_Empty(Scan); Scan = list_Cdr(Scan))
+    list_Rplaca(Scan,list_PairSecond(list_Car(Scan)));
+
+  FormulaClauses = list_Nil();
+  SkolemFunctions = list_Nil();
+  Count = 0;
+  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan), Count++) {
+    LIST FormulaClausesTemp;
+    Formula            = term_Copy((TERM) list_PairSecond(list_Car(Scan)));
+#ifdef CHECK_CNF
+    fputs("\nInputFormula : ",stdout); term_Print(Formula); 
+    printf("\nLabel : %s", (char*) list_PairFirst(list_Car(Scan)));
+#endif
+    Formula            = cnf_SkolemFormula(Formula,Precedence,&SkolemFunctions);
+    Formula            = cnf_DistributiveFormula(Formula);
+    FormulaClausesTemp = cnf_MakeClauseList(Formula,FALSE,FALSE,Flags,Precedence);
+    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
+      for (Scan2 = FormulaClausesTemp; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) {
+	hsh_Put(InputClauseToTermLabellist, list_Car(Scan2), list_PairFirst(list_Car(Scan)));
+      }
+    }
+    FormulaClauses = list_Nconc(FormulaClauses, FormulaClausesTemp);
+    term_Delete(Formula);
+  }
+
+  /* Trage nun Formula Clauses modulo Reduktion in einen Index ein */
+ 
+  /* red_SatUnit works only on conclauses */
+  for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
+    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);
+  /* For FormulaClauses a full saturation */
+  /* List is deleted in red_SatUnit ! */
+  EmptyClauses = red_SatUnit(Search, FormulaClauses);
+  if (!list_Empty(EmptyClauses)) {
+    Result = TRUE;
+    /*puts("\nPROOF in FormulaClauses");*/
+    clause_DeleteClauseList(EmptyClauses);
+  }
+
+  /* Move all usables to workedoff */
+  FormulaClauses = list_Copy(prfs_UsableClauses(Search));
+  for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
+    prfs_MoveUsableWorkedOff(Search, (CLAUSE) list_Car(Scan));
+  list_Delete(FormulaClauses);
+  FormulaClauses = list_Nil();
+
+#ifdef CHECK
+  /*cnf_CheckClauseListsConsistency(ShIndex); */
+#endif     
+
+
+  *Symblist = list_Nil();
+  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+    LIST Ax, Pair;
+    UsedTerms = list_Nil();
+    Pair = list_Car(Scan);
+#ifdef CHECK_CNF
+    fputs("\nFormula : ", stdout);
+    term_Print((TERM) list_PairSecond(Pair)); 
+    printf("\nLabel : %s", (char*) list_PairFirst(Pair)); 
+#endif
+    Ax = cnf_OptimizedSkolemization(Search, term_Copy((TERM)list_PairSecond(Pair)), 
+				    (char*) list_PairFirst(Pair), &UsedTerms, 
+				    Symblist,Result,FALSE,InputClauseToTermLabellist);
+    /* Set CONCLAUSE flag for clauses derived from conjectures */
+    if (list_PointerMember(ConjectureList,list_PairSecond(Pair))) {
+      LIST l;
+      for (l = Ax; !list_Empty(l); l = list_Cdr(l))
+	clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE);
+    }
+    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
+      hsh_PutListWithCompareFunc(TermLabelToClauselist, list_PairFirst(Pair),
+				 list_Copy(Ax),
+				 (BOOL (*)(POINTER,POINTER))cnf_LabelEqual,
+				 (unsigned long (*)(POINTER))hsh_StringHashKey);
+      UsedTerms = list_Cons(list_PairFirst(Pair), UsedTerms);
+      UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms);
+      for (Scan2 = Ax; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) {
+	hsh_PutList(ClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms));
+	hsh_PutList(InputClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms));
+      } 
+    }
+    *AxClauses = list_Nconc(*AxClauses, Ax);
+    list_Delete(UsedTerms);
+  }
+
+  /* Transfer precedence of new skolem symbols into <InputPrecedence> */
+  symbol_TransferPrecedence(Precedence, InputPrecedence);
+
+  list_Delete(ConjectureList);
+  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
+    hsh_Delete(InputClauseToTermLabellist);
+  if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) { 
+    list_Delete(*Symblist);
+  }
+
+  *AllLabels = list_Nil();
+  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
+    LIST Pair;
+    Pair = list_Car(Scan);
+    term_Delete((TERM) list_PairSecond(Pair));
+    *AllLabels = list_Cons(list_PairFirst(Pair), *AllLabels);
+    list_PairFree(Pair);
+  }
+
+  list_Delete(AllFormulae);
+  list_Delete(SkolemFunctions);
+  list_Delete(SkolemPredicates);
+
+  if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) {
+    symbol_ResetSkolemIndex();
+    prfs_Delete(Search);
+    return NULL;
+  }
+  else {
+    /* Delete DocProof clauses */
+    prfs_DeleteDocProof(Search);
+    return Search;
+  }
+}
+
+LIST cnf_QueryFlotter(PROOFSEARCH Search, TERM Term, LIST* Symblist)
+/**************************************************************
+  INPUT:   A term to derive clauses from, using optimized skolemization,
+           and a ProofSearch object. 
+  RETURNS: A list of derived clauses.
+  EFFECT:  ??? EK
+           The precedence of new skolem symbols is set in <Search>.
+***************************************************************/
+{
+  LIST       SkolemPredicates, SkolemFunctions, IndexedClauses, Scan;
+  LIST       ResultClauses, Dummy, EmptyClauses;
+  TERM       TermCopy;
+  int        Formulae2Clause;
+  BOOL       Result;
+  FLAGSTORE  Flags, SubProofFlags;
+  PRECEDENCE Precedence;
+
+  Flags      = prfs_Store(Search);
+  Precedence = prfs_Precedence(Search);
+
+  /* Initialize the flagstore of the cnf_SEARCHCOPY object with default values */
+  /* and copy the value of flag_DOCPROOF from the global Proofserach object.   */
+  SubProofFlags = prfs_Store(cnf_SEARCHCOPY);
+  flag_InitStoreByDefaults(SubProofFlags);
+  flag_TransferFlag(Flags, SubProofFlags, flag_DOCPROOF);
+  /* Transfer the precedence into the local search object */
+  symbol_TransferPrecedence(Precedence, prfs_Precedence(cnf_SEARCHCOPY));
+
+  SkolemPredicates = SkolemFunctions = list_Nil();
+  Result = FALSE;
+  
+  prfs_CopyIndices(Search, cnf_SEARCHCOPY);
+
+  Term = term_Create(fol_Not(), list_List(Term));
+  fol_NormalizeVars(Term);
+  Term = cnf_ObviousSimplifications(Term);
+  if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
+    term_AddFatherLinks(Term);
+    Term = ren_Rename(Term, Precedence, &SkolemPredicates,
+		      flag_GetFlagValue(Flags,flag_CNFPRENAMING), TRUE);
+  }
+  Term = cnf_RemoveEquivImplFromFormula(Term);
+  Term = cnf_NegationNormalFormula(Term);
+  Term = cnf_AntiPrenex(Term);
+  
+  TermCopy = term_Copy(Term);
+  TermCopy = cnf_SkolemFormula(TermCopy, Precedence, &SkolemFunctions);
+  TermCopy = cnf_DistributiveFormula(TermCopy);
+
+  IndexedClauses = cnf_MakeClauseList(TermCopy,FALSE,FALSE,Flags,Precedence);
+  term_Delete(TermCopy);
+
+  /* red_SatUnit works only on conclauses */
+  for (Scan = IndexedClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
+    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);
+
+  EmptyClauses = red_SatUnit(cnf_SEARCHCOPY, IndexedClauses);
+
+  if (!list_Empty(EmptyClauses)) {
+    Result = TRUE;
+    clause_DeleteClauseList(EmptyClauses);
+  }
+
+  while (!list_Empty(prfs_UsableClauses(cnf_SEARCHCOPY))) {
+    prfs_MoveUsableWorkedOff(cnf_SEARCHCOPY, (CLAUSE) list_Car(prfs_UsableClauses(cnf_SEARCHCOPY)));
+  }
+  /* Works only if DOCPROOF is false. Otherwise we need labels */
+  Dummy = list_Nil();
+  if (flag_GetFlagValue(SubProofFlags, flag_DOCPROOF))
+    Formulae2Clause = TRUE;
+  else
+    Formulae2Clause = FALSE;
+  flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFOFF);
+  ResultClauses = cnf_OptimizedSkolemization(cnf_SEARCHCOPY, term_Copy(Term),
+					     NULL, &Dummy, Symblist, Result,
+					     FALSE, NULL);
+
+  if (Formulae2Clause)
+    flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFON);
+  
+  term_Delete(Term);
+  list_Delete(SkolemPredicates);
+  list_Delete(SkolemFunctions);
+  prfs_Clean(cnf_SEARCHCOPY);
+
+  /* All result clauses of queries are conjecture clauses */
+  for (Scan=ResultClauses; !list_Empty(Scan); Scan=list_Cdr(Scan))
+    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);
+
+  return ResultClauses;
+}
+
+
+#ifdef CHECK
+/* Currently unused */
+/*static*/ void cnf_CheckClauseListsConsistency(SHARED_INDEX ShIndex)
+/**************************************************************
+  INPUT: A shared index and a list of non-ConClauses.
+  EFFECT: When this function is called all clauses in the index must be
+       non-ConClauses, which must also be members of the list.
+**************************************************************/
+{
+  LIST AllClauses, scan;
+
+  AllClauses = clause_AllIndexedClauses(ShIndex);
+  for (scan = AllClauses; scan != list_Nil(); scan = list_Cdr(scan)) {
+    if (clause_GetFlag((CLAUSE) list_Car(scan), CONCLAUSE)) {
+      misc_StartErrorReport();
+      misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is a CONCLAUSE.\n");
+      misc_FinishErrorReport();
+    } 
+    if (clause_GetFlag((CLAUSE) list_Car(scan), BLOCKED)) {
+      misc_StartErrorReport();
+      misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is BLOCKED.\n");
+      misc_FinishErrorReport();
+    }
+  }
+  list_Delete(AllClauses);
+}
+#endif
+
+
+static LIST cnf_SatUnit(PROOFSEARCH Search, LIST ClauseList) 
+/*********************************************************
+  INPUT:   A list of unshared clauses, proof search object
+  RETURNS: A possibly empty list of empty clauses.
+**********************************************************/
+{
+  CLAUSE     Given;
+  LIST       Scan, Derivables, EmptyClauses, BackReduced;
+  NAT        n, Derived;
+  FLAGSTORE  Flags;
+  PRECEDENCE Precedence;
+
+  Flags        = prfs_Store(Search);
+  Precedence   = prfs_Precedence(Search);
+  Derived      = flag_GetFlagValue(Flags, flag_CNFPROOFSTEPS);
+  EmptyClauses = list_Nil();
+  ClauseList   = clause_ListSortWeighed(ClauseList);
+  
+  while (!list_Empty(ClauseList) && list_Empty(EmptyClauses)) {
+    Given = (CLAUSE)list_NCar(&ClauseList);
+    Given = red_CompleteReductionOnDerivedClause(Search, Given, red_ALL);
+    if (Given) {
+      if (clause_IsEmptyClause(Given))
+        EmptyClauses = list_List(Given);
+      else {
+        /*fputs("\n\nGiven: ",stdout);clause_Print(Given);*/
+	BackReduced = red_BackReduction(Search, Given, red_USABLE);
+	
+        if (Derived != 0) {
+	  Derivables =
+	    inf_BoundedDepthUnitResolution(Given, prfs_UsableSharingIndex(Search),
+					   FALSE, Flags, Precedence);
+	  Derivables =
+	    list_Nconc(Derivables,
+		       inf_BoundedDepthUnitResolution(Given,prfs_WorkedOffSharingIndex(Search),
+						      FALSE, Flags, Precedence));
+          n = list_Length(Derivables);
+          if (n > Derived)
+            Derived = 0;
+          else
+            Derived -= n;
+        }
+        else 
+          Derivables = list_Nil();
+	
+        Derivables  = list_Nconc(BackReduced,Derivables);
+        Derivables  = split_ExtractEmptyClauses(Derivables, &EmptyClauses);
+	
+	prfs_InsertUsableClause(Search, Given);
+	
+	for (Scan = Derivables; !list_Empty(Scan); Scan = list_Cdr(Scan))
+	  ClauseList = clause_InsertWeighed(list_Car(Scan), ClauseList, Flags,
+					    Precedence);
+	list_Delete(Derivables);
+      }
+    }
+  }
+  clause_DeleteClauseList(ClauseList);
+  return EmptyClauses;
+}
+
+
+TERM cnf_DefTargetConvert(TERM Target, TERM ToTopLevel, TERM ToProveDef, 
+			  LIST DefPredArgs, LIST TargetPredArgs,
+			  LIST TargetPredVars, LIST VarsForTopLevel,
+			  FLAGSTORE Flags, PRECEDENCE Precedence,
+			  BOOL* LocallyTrue)
+/**********************************************************
+  INPUT:   A term Target which contains a predicate that might be replaced
+           by its definition.
+	   A term ToTopLevel which is the highest level subterm in Target
+	   that contains the predicate and can be moved to top level or().
+	   A term ToProveDef which must hold if the definition is to be applied.
+	   (IS DESTROYED AND FREED)
+	   A list DefPredArgs of the arguments of the predicate in the
+	   Definition.
+	   A list TargetPredArgs of the arguments of the predicate in Target.
+	   A list TargetPredVars of the variables occurring in the arguments
+	   of the predicate in Target.
+	   A list VarsForTopLevel containing the variables that should be
+	   all-quantified at top level to make the proof easier.
+	   A flag store.
+	   A pointer to a boolean LocallyTrue which is set to TRUE iff
+	   the definition can be applied.
+  RETURNS: The Target term which is brought into standard form.
+**********************************************************/
+
+{
+  TERM orterm, targettoprove;
+  SYMBOL maxvar;                    /* For normalizing terms */
+  LIST l1, l2;
+  LIST freevars, vars;              /* Free variables in targettoprove */
+
+  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+    puts("\nTarget :");
+    fol_PrettyPrint(Target);
+  }
+#ifdef CHECK
+  fol_CheckFatherLinks(Target);
+#endif
+  /* No proof found yet */
+  *LocallyTrue = FALSE;
+
+  /* Remove implications from path */
+  Target = cnf_RemoveImplFromFormulaPath(Target, ToTopLevel);
+    
+  /* Move negations as far down as possible */
+  Target = cnf_NegationNormalFormulaPath(Target, ToTopLevel);
+    
+  /* Move quantifiers as far down as possible */
+  Target = cnf_AntiPrenexPath(Target, ToTopLevel);
+
+  /* Move all-quantified variables from the predicates' arguments to top level */
+  Target = cnf_MovePredicateVariablesUp(Target, ToTopLevel, VarsForTopLevel);
+
+  /* Flatten top or() */
+  Target = cnf_FlattenPath(Target, ToTopLevel);
+
+  /* Now make sure that all variables in the top forall quantifier are in TargetPredVars */
+  /* Not necessary, according to CW */
+  if (symbol_Equal(term_TopSymbol(Target), fol_All())) {
+    targettoprove = term_Copy(term_SecondArgument(Target));
+    orterm        = term_SecondArgument(Target);
+  }
+  else {
+    targettoprove = term_Copy(Target);
+    orterm        = Target;
+  }
+
+  /* Find argument of targettoprove that contains the predicate and remove it */
+  if (symbol_Equal(term_TopSymbol(targettoprove), fol_Or())) {
+    /* Find subterm that contains the predicate */
+    LIST arglist;
+    arglist = term_ArgumentList(targettoprove);
+    for (l1=arglist, l2=term_ArgumentList(orterm); !list_Empty(l1); 
+	l1 = list_Cdr(l1), l2 = list_Cdr(l2)) {
+      if (term_HasProperSuperterm(ToTopLevel, (TERM) list_Car(l2)) ||
+	  (ToTopLevel == (TERM) list_Car(l2))) {
+	arglist = list_PointerDeleteElementFree(arglist, list_Car(l1),
+						(void (*)(POINTER))term_Delete);
+	break;
+      }
+    }
+    term_RplacArgumentList(targettoprove, arglist);
+    /* Nothing left for the proof ? */
+    if (list_Empty(term_ArgumentList(targettoprove))) {
+      term_Delete(targettoprove);
+      term_Delete(ToProveDef);
+#ifdef CHECK
+      fol_CheckFatherLinks(Target);
+#endif
+      return Target;
+    }
+  }
+  else {
+    /* Nothing left for the proof */
+    term_Delete(targettoprove);
+    term_Delete(ToProveDef);
+#ifdef CHECK
+    fol_CheckFatherLinks(Target);
+#endif
+    return Target;
+  }
+
+  /* Normalize variables in ToProveDef with respect to targettoprove */
+  maxvar = term_MaxVar(targettoprove);
+  symbol_SetStandardVarCounter(maxvar);
+  vars = fol_BoundVariables(ToProveDef);
+  vars = term_DeleteDuplicatesFromList(vars);
+  for (l1=vars; !list_Empty(l1); l1=list_Cdr(l1))
+    term_ExchangeVariable(ToProveDef, term_TopSymbol(list_Car(l1)), symbol_CreateStandardVariable());
+  list_Delete(vars);
+  
+  /* Replace arguments of predicate in condition of definition by matching arguments
+     of predicate in target term */
+  for (l1=DefPredArgs, l2=TargetPredArgs; !list_Empty(l1); l1=list_Cdr(l1), l2=list_Cdr(l2)) 
+    term_ReplaceVariable(ToProveDef, term_TopSymbol((TERM) list_Car(l1)), (TERM) list_Car(l2));
+
+  targettoprove = term_Create(fol_Not(), list_List(targettoprove));
+  targettoprove = cnf_NegationNormalFormula(targettoprove);
+  targettoprove = term_Create(fol_Implies(), 
+			      list_Cons(targettoprove, list_List(ToProveDef)));
+
+  /* At this point ToProveDef must not be accessed again ! */
+  
+  /* Add all--quantifier to targettoprove */
+  freevars = fol_FreeVariables(targettoprove);
+  term_CopyTermsInList(freevars);
+  targettoprove = fol_CreateQuantifier(fol_All(), freevars, list_List(targettoprove));
+  
+  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+    puts("\nConverted to :");
+    fol_PrettyPrint(Target);
+  }
+
+  targettoprove = cnf_NegationNormalFormula(targettoprove);
+  
+  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+    puts("\nToProve for this target :");
+    fol_PrettyPrint(targettoprove);
+  }
+ 
+  *LocallyTrue = cnf_HaveProof(list_Nil(), targettoprove, Flags, Precedence);
+  
+  term_Delete(targettoprove);
+
+#ifdef CHECK
+  fol_CheckFatherLinks(Target);
+#endif
+
+  return Target;
+}
+
+
+static TERM cnf_RemoveQuantFromPathAndFlatten(TERM TopTerm, TERM SubTerm)
+/**********************************************************
+  INPUT:  Two terms, <SubTerm> must be a subterm of <TopTerm>.
+          Superterm of <SubTerm> must be an equivalence.
+	  Along the path to SubTerm there are only quantifiers or disjunctions.
+	  All free variables in the equivalence are free variables
+	  in <SubTerm>.
+	  All free variables in <SubTerm> are bound by a universal quantifier
+	  (with polarity 1).
+  RETURN: The destructively changed <TopTerm>.
+  EFFECT: Removes all quantifiers not binding a variable in <SubTerm>
+          from <subTerm>'s path.
+          Moves all universal quantifiers binding free variable
+	  in <SubTerm> up.
+	  <TopTerm> is transformed into the form
+	  forall([X1,...,Xn],or (equiv(<SubTerm>,psi),phi)).
+**********************************************************/
+{
+  TERM Term1, Term2, Flat, Variable;
+  LIST Scan1, Scan2, FreeVars;
+
+
+#ifdef CHECK
+  if (!fol_CheckFormula(TopTerm) || !term_HasPointerSubterm(TopTerm, SubTerm)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal input.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  TopTerm = cnf_SimplifyQuantors(TopTerm);
+  term_AddFatherLinks(TopTerm);
+  Term1   = term_Superterm(SubTerm);
+
+  while (Term1 != TopTerm) {
+
+    while (symbol_Equal(fol_Or(), term_TopSymbol(Term1)) && (TopTerm != Term1)) {
+      Term1 = term_Superterm(Term1);
+    }
+    if (fol_IsQuantifier(term_TopSymbol(Term1))) {
+      Flat  = term_SecondArgument(Term1);
+      Flat  = cnf_Flatten(Flat, fol_Or());
+      Scan1 = fol_QuantifierVariables(Term1);
+      while (!list_Empty(Scan1)) {
+	Variable = (TERM)list_Car(Scan1);
+	if (fol_VarOccursFreely(Variable, SubTerm)) {
+	  Scan2 = list_Cdr(Scan1);
+	  fol_DeleteQuantifierVariable(Term1, term_TopSymbol(list_Car(Scan1)));
+	  Scan1 = Scan2;
+	}
+	else {
+	  Scan1 = list_Cdr(Scan1);
+	}
+      }
+      if (fol_IsQuantifier(term_TopSymbol(Term1))) {
+	/* still variables, but not binding a variable in the equivalence term */
+	LIST ArgList;
+
+	term_RplacArgumentList(Flat, list_PointerDeleteOneElement(term_ArgumentList(Flat), SubTerm));
+	ArgList = term_ArgumentList(Term1);
+       	term_RplacArgumentList(Term1, list_Nil());
+	Term2 = term_Create(term_TopSymbol(Term1), ArgList);
+	term_RplacArgumentList(Term1, list_Cons(SubTerm, list_List(Term2)));
+	term_RplacTop(Term1, fol_Or());
+	Scan1 = term_ArgumentList(Term1); 
+	while (!list_Empty(Scan1)) {
+	  term_RplacSuperterm((TERM)list_Car(Scan1), Term1);
+	  Scan1 = list_Cdr(Scan1);
+	}
+      }
+    }
+    else {
+
+#ifdef CHECK
+      if (!symbol_Equal(term_TopSymbol(Term1), fol_Or())) {
+	misc_StartErrorReport();
+	misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal term Term1");
+	misc_FinishErrorReport();
+      }
+#endif
+
+      Term1 = cnf_Flatten(Term1, fol_Or());
+    }
+  }
+  FreeVars = fol_FreeVariables(Term1);
+  if (!list_Empty(FreeVars)) {
+    term_CopyTermsInList(FreeVars);
+    TopTerm = fol_CreateQuantifier(fol_All(), FreeVars, list_List(Term1));
+  }
+  return TopTerm;
+}
+
+
+TERM cnf_DefConvert(TERM Def, TERM FoundPredicate, TERM* ToProve)
+/*********************************************************
+  INPUT:   A term Def which is an equivalence (P(x1,..,xn) <=> Formula)
+           that can be converted to standard form.
+           The subterm that holds the defined predicate.
+           A pointer to a term ToProve into which a term is stored
+	   that has to be proved before applying the definition.
+  RETURNS: The converted definition : forall([..], or(equiv(..,..), ..))
+************************************************************/
+{
+  TERM orterm;
+
+#ifdef CHECK
+  fol_CheckFatherLinks(Def);
+#endif
+  
+  Def = cnf_RemoveImplFromFormulaPath(Def, FoundPredicate);   /* Remove implications along the path */
+  Def = cnf_NegationNormalFormulaPath(Def, FoundPredicate);   /* Move not's as far down as possible */
+
+#ifdef CHECK
+  if (!fol_CheckFormula(Def)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\nIn cnf_DefConvert: Illegal input Formula.\n");
+    misc_FinishErrorReport();
+  }
+  if (!term_HasPointerSubterm(Def, FoundPredicate)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\nIn cnf_DefConvert: Illegal input SubTerm.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  Def = cnf_RemoveQuantFromPathAndFlatten(Def, term_Superterm(FoundPredicate));
+  term_AddFatherLinks(Def);
+
+#ifdef CHECK
+  if (!fol_CheckFormula(Def)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\nIn cnf_DefConvert: Illegal term Def.");
+    misc_FinishErrorReport();
+  }
+  if (!term_HasPointerSubterm(Def, FoundPredicate)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\nIn cnf_DefConvert: Illegal term FoundPredicate.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  /* Find top level or() */
+  if (symbol_Equal(term_TopSymbol(Def), fol_All())) {
+    /* Make sure there are several arguments */
+    if (symbol_Equal(term_TopSymbol(term_SecondArgument(Def)), fol_Or()) &&
+	(list_Length(term_ArgumentList(term_SecondArgument(Def))) == 1)) {
+      TERM t;
+      t = term_SecondArgument(Def);
+      term_RplacSecondArgument(Def, term_FirstArgument(term_SecondArgument(Def)));
+      term_Free(t);
+      orterm = NULL;
+      term_RplacSuperterm(term_SecondArgument(Def), Def);
+    }
+    else 
+      orterm = term_SecondArgument(Def);
+  }
+  else {
+    /* Make sure there are several arguments */
+    if (symbol_Equal(term_TopSymbol(Def), fol_Or()) &&
+	(list_Length(term_ArgumentList(Def)) == 1)) {
+      TERM t;
+      t = Def;
+      Def = term_FirstArgument(Def);
+      term_Free(t);
+      orterm = NULL;
+      term_RplacSuperterm(term_SecondArgument(Def), Def);
+    }
+    else 
+      orterm = Def;
+  }
+
+  /* If there is something to prove */
+  if (orterm != (TERM) NULL) {
+    TERM equiv;
+    LIST args;
+
+    equiv = (TERM) NULL;
+
+    /* In pell 10 there are no conditions for the equivalence */
+    if (symbol_Equal(term_TopSymbol(orterm), fol_Equiv())) {
+      equiv = orterm;
+      *ToProve = NULL;
+    }
+    else {
+      TERM t;
+      /* First find equivalence term among arguments */
+      args  = term_ArgumentList(orterm);
+      equiv = term_Superterm(FoundPredicate);
+      
+      /* Delete equivalence from list */
+      args = list_PointerDeleteElement(args, equiv);
+      term_RplacArgumentList(orterm, args);
+      
+      /* ToProve consists of all the definitions arguments except the equivalence */
+      *ToProve = term_Copy(orterm);
+      
+      /* Now not(*ToProve) implies the equivalence */
+      /* Negate *ToProve */
+      *ToProve = term_Create(fol_Not(), list_List(*ToProve));
+      *ToProve = cnf_NegationNormalFormula(*ToProve);
+      term_AddFatherLinks(*ToProve);
+
+      /* Now convert definition to implication form */
+      term_RplacTop(orterm, fol_Implies());
+      t = term_Create(fol_Not(), 
+		      list_List(term_Create(fol_Or(), 
+					    term_ArgumentList(orterm))));
+      term_RplacArgumentList(orterm, list_Cons(t, list_List(equiv)));
+
+      Def = cnf_NegationNormalFormula(Def);
+      term_AddFatherLinks(Def);
+    }    
+  }
+  
+#ifdef CHECK
+  fol_CheckFatherLinks(Def);
+#endif
+  return Def;
+}
+
+
+LIST cnf_HandleDefinition(PROOFSEARCH Search, LIST Pair, LIST Axioms,
+			  LIST Sorts, LIST Conjectures)
+/*******************************************************************
+  INPUT:   A PROOFSEARCH object, a pair (label, term) and 3 lists of pairs.
+           If the term in pair is a definition, the defined predicate
+	   is expanded in all the lists
+           and added to the proofsearch object.
+  RETURNS: The pair with the converted definition:
+           forall([..], or(equiv(..,..), .......))
+********************************************************************/
+{
+  TERM definition, defpredicate, equivterm;
+  
+  BOOL alwaysapplicable;     /* Is set to TRUE iff the definition can always be applied */
+  FLAGSTORE Flags;
+  PRECEDENCE Precedence;
+
+  Flags      = prfs_Store(Search);
+  Precedence = prfs_Precedence(Search);
+
+  /* The axiomlist consists of (label, formula) pairs */
+  definition = list_PairSecond(Pair);
+  
+  /* Test if Definition contains a definition */
+  defpredicate = (TERM) NULL;
+  if (cnf_ContainsDefinition(definition, &defpredicate)) { 
+    TERM toprove;
+    LIST allformulae, scan;
+
+    /* Create list of all formula pairs */
+    /* Check if definition may be applied to each formula */
+    allformulae = list_Copy(Axioms);
+    allformulae = list_Nconc(allformulae, list_Copy(Sorts));
+    allformulae = list_Nconc(allformulae, list_Copy(Conjectures));
+#ifdef CHECK
+    for (scan=allformulae; !list_Empty(scan); scan=list_Cdr(scan)) {
+      if (!list_Empty((LIST) list_Car(scan))) {
+	if (!term_IsTerm((TERM) list_PairSecond((LIST) list_Car(scan))))
+	  fol_CheckFatherLinks((TERM) list_PairSecond((LIST) list_Car(scan)));
+      }
+    }
+#endif
+    
+    /* Convert definition to standard form */
+    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+      fputs("\nPredicate : ", stdout);
+      symbol_Print(term_TopSymbol(defpredicate));
+    }
+
+    definition = cnf_DefConvert(definition, defpredicate, &toprove);
+    if (toprove == NULL)
+      alwaysapplicable = TRUE;
+    else 
+      alwaysapplicable = FALSE;
+
+    prfs_SetDefinitions(Search, list_Cons(term_Copy(definition), 
+					  prfs_Definitions(Search)));
+    
+    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+      if (alwaysapplicable) {
+	fputs("\nAlways Applicable     : ", stdout);
+	fol_PrettyPrint(definition); 
+      } 
+    }
+
+    /* Definition is converted to a form where the equivalence is
+       the first argument of the disjunction */
+    equivterm     = term_SecondArgument(term_Superterm(defpredicate));
+    
+    
+    scan = allformulae;
+    while (!list_Empty(scan)) {
+      BOOL localfound;
+      LIST pair, targettermvars;
+      
+      /* Pair label / term */
+      pair = list_Car(scan);
+
+      /* Pair may be NULL if it is a definition that could be deleted */
+      if ((pair != NULL) && (definition != (TERM) list_PairSecond(pair))) {
+	TERM target, targetpredicate, totoplevel;
+	LIST varsfortoplevel;
+	target = (TERM) list_PairSecond(pair);
+	targettermvars = varsfortoplevel = list_Nil();
+	
+	/* If definition is not always applicable, check if it is applicable
+	   for this formula */
+	localfound = FALSE;
+	if (!alwaysapplicable) {
+	  if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate),
+				    &targetpredicate, &totoplevel,
+				    &targettermvars, &varsfortoplevel)) {
+	    TERM toprovecopy;
+	    toprovecopy = term_Copy(toprove);
+	    target = cnf_DefTargetConvert(target, totoplevel, toprovecopy,
+					  term_ArgumentList(defpredicate),
+					  term_ArgumentList(targetpredicate),
+					  targettermvars, varsfortoplevel,
+					  Flags, Precedence, &localfound);
+	    list_Delete(targettermvars);
+	    list_Delete(varsfortoplevel);
+	    targettermvars = varsfortoplevel = list_Nil();
+	    
+	    list_Rplacd(pair, (LIST) target);
+	    if (localfound)
+	      list_Rplacd(pair, 
+			  (LIST) cnf_ApplyDefinitionOnce(defpredicate, 
+							 equivterm,
+							 list_PairSecond(pair),
+							 targetpredicate,
+							 Flags));
+	  }
+	}
+	else {
+	  if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate), 
+				    &targetpredicate, &totoplevel,
+				    &targettermvars, &varsfortoplevel))
+	    list_Rplacd(pair, (LIST) cnf_ApplyDefinitionOnce(defpredicate, 
+							     equivterm,
+							     list_PairSecond(pair),
+							     targetpredicate,
+							     Flags));
+	  else
+	    scan = list_Cdr(scan);
+	  list_Delete(targettermvars);
+	  list_Delete(varsfortoplevel);
+	  targettermvars = varsfortoplevel = list_Nil();
+	}
+      }
+      else
+	scan = list_Cdr(scan);
+    }
+    list_Delete(allformulae);
+    /* toprove can be NULL if the definition can always be applied */
+    if (toprove != (TERM) NULL)
+      term_Delete(toprove);
+    list_Rplacd(Pair, (LIST) definition);
+  }
+ 
+  return Pair;
+}
+
+
+LIST cnf_ApplyDefinitionToClause(CLAUSE Clause, TERM Predicate, TERM Expansion,
+				 FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause, two terms and a flag store and a precedence.
+  RETURNS: The list of clauses where each occurrence of Predicate is 
+           replaced by Expansion.
+***************************************************************/
+{
+  NAT  i;
+  BOOL changed;
+  LIST args, scan, symblist;
+  TERM clauseterm, argument;
+
+  changed = FALSE;
+  
+  /* Build term from clause */
+  args = list_Nil();
+  for (i = 0; i < clause_Length(Clause); i++) {
+    argument = clause_GetLiteralTerm(Clause, i); /* with sign */
+    args     = list_Cons(term_Copy(argument), args);
+  }
+  clauseterm = term_Create(fol_Or(), args);
+
+  for (scan=term_ArgumentList(clauseterm); !list_Empty(scan); scan=list_Cdr(scan)) {
+    BOOL isneg;
+
+    argument = (TERM) list_Car(scan);
+    if (symbol_Equal(term_TopSymbol(argument), fol_Not())) {
+      argument = term_FirstArgument(argument);
+      isneg = TRUE;
+    }
+    else 
+      isneg = FALSE;
+      
+    /* Try to match with predicate */
+    cont_StartBinding();
+    if (unify_Match(cont_LeftContext(), Predicate, argument)) {
+      SUBST subst;
+      TERM  newargument;
+      subst = subst_ExtractMatcher();
+      newargument = subst_Apply(subst, term_Copy(Expansion));
+      subst_Free(subst);
+      if (isneg)
+	newargument = term_Create(fol_Not(), list_List(newargument));
+      term_Delete((TERM) list_Car(scan));
+      list_Rplaca(scan, newargument);
+      changed = TRUE;
+    }      
+    cont_BackTrack();
+  }
+
+  if (changed) {
+    /* Build term and derive list of clauses */
+    LIST result;
+    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+      puts("\nClause before applying def :");
+      clause_Print(Clause);
+      puts("\nPredicate :");
+      fol_PrettyPrint(Predicate);
+      puts("\nExpansion :");
+      fol_PrettyPrint(Expansion);
+    }
+    symblist   = list_Nil();
+    clauseterm = cnf_Cnf(clauseterm, Precedence, &symblist);
+    result     = cnf_MakeClauseList(clauseterm,FALSE,FALSE,Flags,Precedence);
+    list_Delete(symblist);
+    term_Delete(clauseterm);
+    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
+      LIST l;
+      puts("\nClauses derived by expanding definition :");
+      for (l = result; !list_Empty(l); l=list_Cdr(l)) {
+	clause_Print((CLAUSE) list_Car(l));
+	fputs("\n", stdout);
+      }
+    }
+    return result;
+  }
+  else {
+    term_Delete(clauseterm);
+    return list_Nil();
+  }
+}
+
+
+BOOL cnf_PropagateSubstEquations(TERM StartTerm)
+/*************************************************************
+  INPUT:   A term where we assume that father links are established and
+           that no variable is bound by more than one quantifier.
+  RETURNS: TRUE, if any substitutions were made, FALSE otherwise.
+  EFFECT:  Function looks for equations of the form x=t where x does not
+           occur in t. If x=t occurs negatively and disjunctively below
+	   a universal quantifier binding x or if x=t occurs positively and
+	   conjunctively below an existential quantifier binding x,
+           all occurrences of  x are replaced by t in <StartTerm>.
+**************************************************************/
+{
+  LIST   Subequ;
+  TERM   QuantorTerm, Equation, EquationTerm;
+  SYMBOL Variable;
+  BOOL   Hit, Substituted;
+
+#ifdef CHECK
+  if (fol_VarBoundTwice(StartTerm)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In cnf_PropagateSubstEquations: Variables of");
+    misc_ErrorReport("\n input term are not normalized.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  Substituted = FALSE;
+
+  Subequ = fol_GetSubstEquations(StartTerm);
+  for ( ; !list_Empty(Subequ); Subequ = list_Pop(Subequ)) {
+    Hit          = FALSE;
+    Equation     = list_Car(Subequ);
+    Variable     = symbol_Null();
+    QuantorTerm  = term_Null();
+    EquationTerm = term_Null();
+
+    if (term_IsVariable(term_FirstArgument(Equation)) &&
+	!term_ContainsVariable(term_SecondArgument(Equation),
+			       term_TopSymbol(term_FirstArgument(Equation)))) {
+
+      Variable     = term_TopSymbol(term_FirstArgument(Equation));
+      QuantorTerm  = fol_GetBindingQuantifier(Equation, Variable);
+      EquationTerm = term_SecondArgument(Equation);
+      Hit          = fol_PolarCheck(Equation, QuantorTerm);
+    }
+    if (!Hit && term_IsVariable(term_SecondArgument(Equation)) &&
+	!term_ContainsVariable(term_FirstArgument(Equation),
+			       term_TopSymbol(term_SecondArgument(Equation)))) {
+
+      Variable     = term_TopSymbol(term_SecondArgument(Equation));
+      QuantorTerm  = fol_GetBindingQuantifier(Equation, Variable);
+      EquationTerm = term_FirstArgument(Equation);
+      Hit          = fol_PolarCheck(Equation, QuantorTerm);
+    }
+    if (Hit) {
+      fol_DeleteQuantifierVariable(QuantorTerm,Variable);
+      term_ReplaceVariable(StartTerm, Variable, EquationTerm); /* We replace everythere ! */
+      term_AddFatherLinks(StartTerm);
+      if (symbol_Equal(term_TopSymbol(QuantorTerm),fol_Equality())) /* Trivial Formula */
+	fol_SetTrue(QuantorTerm);
+      else
+	fol_SetTrue(Equation);
+      Substituted = TRUE;
+    }   
+  }
+
+  /* <Subequ> was freed in the loop. */
+
+  return Substituted;
+}