File: cnf.c

package info (click to toggle)
spass 3.7-2
links: PTS
area: main
in suites: squeeze
size: 5,500 kB
ctags: 5,981
sloc: ansic: 50,634; yacc: 3,038; sh: 1,072; lex: 430; perl: 407; makefile: 394
file content (5126 lines) | stat: -rw-r--r-- 177,400 bytes
parent folder | download | duplicates (3)
/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *               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 FreeBSD    * */
/* *  Licence.                                              * */
/* *                                                        * */
/* *  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 LICENCE file       * */
/* *  for more details.                                     * */
/* *                                                        * */
/* *                                                        * */
/* $Revision: 1.10 $                                         * */
/* $State: Exp $                                            * */
/* $Date: 2010-02-22 14:09:57 $                             * */
/* $Author: weidenb $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: spass@mpi-inf.mpg.de                * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile: cnf.c,v $ */

#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_GetFlagIntValue(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_GetFlagIntValue(Flags, flag_CNFSTRSKOLEM)) {
    memory_Free(cnf_VARIABLEDEPTHARRAY, sizeof(int[symbol__MAXSTANDARDVAR + 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_GetFlagIntValue(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)) && !symbol_IsPredicate(term_TopSymbol(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));
}


BOOL cnf_FlattenToSimpleORTerm(TERM Term)
/**************************************************************
  INPUT:   A term
  RETURNS: Traverse the term tree using BFS, and flatten the cascated OR Term
			to flat ones. Return True if it is a flat OR Term after all, 
			returns FALSE if it contains any AND SubTerm
  EFFECTS: The input Term will be flattened on each level, 
           as long as it contains no AND subTerm. The sub Terms of the 
		   AND Terms are no more flattened, even if it might contains
		   cascated OR Terms as sub Terms.
  CAUTION: The term is changed. 
***************************************************************/
{
  LIST   Scan1,Scan2;
  BOOL   SimpleOrTerm, SimpleOrSubTerm;

  SimpleOrTerm = FALSE;
  if (symbol_Equal(term_TopSymbol(Term), fol_Or())) {
    TERM   Argterm;
    SimpleOrSubTerm = TRUE;
    Scan1 =term_ArgumentList(Term);
    while (!list_Empty(Scan1)) {
      Argterm = (TERM)list_Car(Scan1);
      Scan2   = list_Cdr(Scan1);
      if (symbol_Equal(term_TopSymbol(Argterm),fol_Or())) {
			SimpleOrSubTerm	= cnf_FlattenToSimpleORTerm(Argterm);
			if (!SimpleOrSubTerm) SimpleOrTerm = FALSE;
			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);
      }
      else if (symbol_Equal(term_TopSymbol(Argterm),fol_And())) {
			SimpleOrTerm = FALSE;
      }
      Scan1  = Scan2;
    }
  }
  return SimpleOrTerm;
}

TERM cnf_ScanTree(TERM Tree)
/**************************************************************
  INPUT:   The input complex Term, which need to be transformed to CNF
  RETURNS: Traverse the term tree using BFS, and put the "or" subtree pointer into the stacks.
  CAUTION: The term is not changed. 
***************************************************************/
{
	SYMBOL Symbol;
	LIST Temp;
	BOOL SimpleOrTerm;

	SimpleOrTerm = cnf_FlattenToSimpleORTerm(Tree);

	Symbol = term_TopSymbol(Tree);
	if (symbol_Equal(Symbol,fol_Or()) && (!SimpleOrTerm)) {
	  stack_Push(Tree);
	}

	for (Temp=term_ArgumentList(Tree);!list_Empty(Temp);Temp=list_Cdr(Temp)) {
	  cnf_ScanTree(list_Car(Temp));
	}
	return Tree;
}

TERM cnf_CombineORTerms(TERM Term1, TERM Term2)
/**********************************************************
  INPUT:   Two OR Terms
  RETURNS: A big "OR" Term. Both argument lists are combined
           to be the new argument list of Term1. Term1 will 
	   be returned.
  MEMORY:  Term2 will be freed.
***********************************************************/
{
  list_Nconc(term_ArgumentList(Term1), term_ArgumentList(Term2));
  term_Free(Term2);
  return Term1;
}

TERM cnf_AddAtomToORTerm(TERM AtomTerm, TERM OrTerm)
/**********************************************************
  INPUT:   First arg is an Atom Term, second arg is an OR Term
  RETURNS: Atom Term will be added into the argumentlist of OR Term
		   
  CAUTION: Atom Term is used, no copy or creation occured
***********************************************************/
{
  LIST ArgumentList;
  ArgumentList = list_Cons(AtomTerm, term_ArgumentList(OrTerm));
  term_RplacArgumentList(OrTerm, ArgumentList);
  return OrTerm;
}

TERM cnf_BuildORTermFromAtoms(TERM Atom1, TERM Atom2)
/**********************************************************
  INPUT:   Two atom Terms
  RETURNS: An OR Term containing the input atom Terms as subterms
		   
  MEMORY:  One new list created, one new Term created.
***********************************************************/
{
  LIST ArgumentList;
  ArgumentList =  list_List(Atom1);
  ArgumentList = list_Cons(Atom2, ArgumentList);
  return  term_Create(fol_Or(), ArgumentList);
}

LIST cnf_List_MultiCons(LIST TempResultList, LIST RightCNFAndArgument)
/**********************************************************
  INPUT:   Two list of CNF list.
  RETURNS: One big CNF list after "multiplications"
  CAUTION: Both input lists will be destructed and deleted afterwards
           The content of these lists are reused in the result.
	   New list is generated for the result
***********************************************************/
{
  LIST NewResult, Scan1, Scan2;     
  TERM NewTerm, Term1, Term2;    
  SYMBOL Symbol1, Symbol2;
  BOOL BreakOut;
  NewResult = list_Nil();
  BreakOut = FALSE;


  for (Scan1=TempResultList;!list_Empty(Scan1);Scan1=list_Cdr(Scan1))	{
    for (Scan2=RightCNFAndArgument;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) {

      Term1 = list_Car(Scan1);
      Term2 = list_Car(Scan2);

      if (!list_Empty(list_Cdr(Scan2))) {
	Term1 = term_Copy(Term1);
      }
      if (!list_Empty(list_Cdr(Scan1))) {
	Term2 = term_Copy(Term2);
      }
      Symbol1 = term_TopSymbol(Term1);
      Symbol2 = term_TopSymbol(Term2);
	      
      /*Case analysis:*/
      if (symbol_Equal(Symbol1,fol_Or()) && symbol_Equal(Symbol2,fol_Or())) {
			  
	if((!list_Empty(list_Cdr(Scan1))) && list_Empty(list_Cdr(Scan2))) {
	  NewTerm = cnf_CombineORTerms(Term2, Term1);
	}
	else {			  
	  NewTerm = cnf_CombineORTerms(Term1, Term2);
	}
      }
      else if ((symbol_Equal(Symbol1,fol_Or())) && (!symbol_Equal(Symbol2,fol_Or()))) {
	NewTerm = cnf_AddAtomToORTerm(Term2, Term1);
      }
      else if ((!symbol_Equal(Symbol1,fol_Or())) && (symbol_Equal(Symbol2,fol_Or()))) {
	NewTerm = cnf_AddAtomToORTerm(Term1, Term2);
      }
      else {
	NewTerm = cnf_BuildORTermFromAtoms(Term1, Term2);

      }
      NewResult = list_Cons( NewTerm, NewResult);
    }
  }


  /* The list is not  yet deleted*/

  list_Delete(RightCNFAndArgument);
  list_Delete(TempResultList);	

	
  NewResult = term_DestroyDuplicatesInList(NewResult);

  /*Debugging Code*/
  /*    
	printf("\nAfter multiplication, the new Result contains:");

	for (Scan1= NewResult; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) {

	printf("\n"); term_Print(list_Car(Scan1));fflush(stdout);
	}
  */
  return NewResult;
}


void cnf_SeparateAndTermsFromArgList(LIST* Input, LIST* AndList, 
				     LIST* AtomList, LIST* AndTail, LIST* AtomTail)
/**************************************************************
  INPUT:    A Pointer to Input Argument List
	    A Pointer to AndList, which will be filled with And subterms
	    A Pointer to AtomList,which will be filled with Atom subterms
	    A Pointer to AndTail, the last element of AndList
	    A Pointer to AtomTail, the last element of AtomList
  EFFECTS:  All the arguments will be initialised. The given 
	    Input List (Argumentst) will be separated to AndList
	    and AtomList.
  MEMORY:   No memory allocation occurs here. The input argumentlist
	    might become either AndList or AtomList, depending on the
	    head element of it.
***************************************************************/
{
  LIST Scan1,Scan2;

  Scan1=*Input;

  while(!list_Empty(Scan1)) {
    Scan2 = list_Cdr(Scan1);
    list_Rplacd(Scan1,list_Nil());

    if (symbol_Equal(term_TopSymbol(list_Car(Scan1)), fol_And())) {
      if (list_Empty(*AndList)){
	*AndList = Scan1;
      }
      else {
	list_Rplacd(*AndTail,Scan1);
      }	
      *AndTail = Scan1;
    }
    else {
      if (list_Empty(*AtomList)){
	*AtomList = Scan1;
      }
      else {
	list_Rplacd(*AtomTail,Scan1);
      }
      *AtomTail = Scan1;
    }

    Scan1=Scan2;

  }

  /*Debugging Code*/
  /*
    printf("\nAfter cnf_SeparateAtomOrAndTermsFrom:.");
    printf("\nAnd list:.");
    for (Scan1= *AndList; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) {

    printf("\n"); term_Print(list_Car(Scan1));fflush(stdout);
    }
    printf("\nAtom list:.");
    for (Scan1= *AtomList; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) {

    printf("\n"); term_Print(list_Car(Scan1));fflush(stdout);
    }
    printf("\nInput list:.");
    for (Scan1= *Input; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) {

    printf("\n"); term_Print(list_Car(Scan1));fflush(stdout);
    }
  */
}

LIST cnf_MakeBigAndList(LIST AndList)
/**************************************************************
  INPUT:   Build the list of OR SubTerms of a big AND Term
  RETURNS: The argumentlist of the big AND Term
  CAUTION: The content of the big AND list will be reused but the list
           itself is no more useful. The input list is deleted here.
***************************************************************/
{
  LIST Result, Scan;

  Result = term_ArgumentList(list_Car(AndList));
  for (Scan=list_Cdr(AndList);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
    Result = cnf_List_MultiCons(Result, term_ArgumentList(list_Car(Scan)));
    term_Free(list_Car(Scan));
  }
  term_Free(list_Car(AndList));
  list_Delete(AndList);
  return  Result;
}




void cnf_AttachAtomList(LIST* ResultCandidate, LIST AtomList)
/**************************************************************
  INPUT:   A candidate list containing either flattened OR Terms
           or atom Terms;
           A list containing only Atom Terms
  EFFECT:  The candidate list will be manipulated, so that all
           subTerms are extended with the AtomList. 
  CAUTION: Destructive on candidate list.
		   The AtomList is useful afterwards, i.e.
		   shouldn't be deleted.
***************************************************************/
{
  LIST Scan, Temp, AttachAtomList;

  for (Scan = *ResultCandidate;!list_Empty(Scan);Scan=list_Cdr(Scan)){
    if (!list_Empty(list_Cdr(Scan))) {
      AttachAtomList = term_CopyTermList(AtomList);

    }
    else {

      AttachAtomList = AtomList;
    }
    if(symbol_Equal(term_TopSymbol(list_Car(Scan)), fol_Or())) {/*OR subterm*/

      Temp = term_ArgumentList(list_Car(Scan));
      Temp = list_Nconc(Temp, AttachAtomList);
      Temp = term_DestroyDuplicatesInList(Temp);
      term_RplacArgumentList(list_Car(Scan), Temp);
    }
    else {/*single atom*/
      Temp = list_Cons(list_Car(Scan), AttachAtomList);
      Temp = term_DestroyDuplicatesInList(Temp);
      list_Rplaca(Scan, term_Create(fol_Or(), Temp));	
    }	
  }
}


void cnf_TransformTree(NAT StackBottom)
/**************************************************************
  INPUT:	The NAT flag of stack bottom.
  EFFECTS:	Go through the "or" subtrees bottom up by processing the 
			Stack and convert the poped out subtree to CNF subtree
  CAUTION:	The poped out subterm and the overall Term is distructively
			changed.
***************************************************************/
{
  TERM Term;
  LIST Result, Scan,  ArgList, AtomList,  AndList, AtomTail, AndTail; 

  while (!stack_Empty(StackBottom)) {
    Term = stack_PopResult();

    for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      cnf_Flatten(list_Car(Scan), fol_And());
    }
    
    AndList  = list_Nil();
    AtomList = list_Nil();
    AndTail  = list_Nil();
    AtomTail = list_Nil();
    ArgList  = term_ArgumentList(Term);
    cnf_SeparateAndTermsFromArgList(&ArgList , &AndList, &AtomList,&AndTail, &AtomTail ); 


    if (!list_Empty(AndList)) {/*The Term is not a simple OR Term, contains And subterms*/
      
      Result = cnf_MakeBigAndList(AndList);

      if (!list_Empty(AtomList)) {/*The Term contains both AND and Atom sub terms */
	
	cnf_AttachAtomList(&Result, AtomList);
      }
      term_RplacTop(Term, fol_And());
      term_RplacArgumentList(Term,Result);	      
    }

    /*
      printf("\nSubOrTerm-After-Transformation: \n"); 
      term_Print(Term);fflush(stdout);
    */
  }
}

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.
***************************************************************/
{ 
  NAT StackBottom;

  if (symbol_Equal(term_TopSymbol(Formula), fol_Or()) || symbol_Equal(term_TopSymbol(Formula), fol_And())) {  
    StackBottom = stack_Bottom();
    cnf_ScanTree(Formula);
    cnf_TransformTree(StackBottom);
    cnf_Flatten(Formula, fol_And());
  }

  return Formula;
}


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(FLAGSTORE Flags, LIST clauselist)
/**********************************************************
  INPUT:   A list of clauses.
  RETURNS: The list of clauses without subsumed clauses.
  EFFECT:  Checks the clock cnf_REDUCTION with respect to the value
           of flag_CNFREDTIME to permit subsumption reductions.
  CAUTION: The list is destructively changed.
***********************************************************/
{
  LIST     scan;
  st_INDEX stindex;
  CLAUSE   actclause;

  stindex = st_IndexCreate();

  for (scan = clauselist; !list_Empty(scan); scan=list_Cdr(scan))
    res_InsertClauseIndex(list_Car(scan),stindex);

  scan=clauselist;
  while (!list_Empty(scan)) {
    actclause     = list_Car(scan);
    res_DeleteClauseIndex(actclause,stindex);
    if (res_BackSubWithLength(actclause,stindex)) {
      clause_Delete(actclause);
      list_Rplaca(scan,(POINTER)NULL);
    }
    else 
      res_InsertClauseIndex(actclause,stindex);

    if (flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) != flag_CNFREDTIMELIMITUNLIMITED &&
	flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) <= ceil(clock_GetSeconds(clock_CNFREDUCTION)))
      scan = list_Nil();
    else
      scan = list_Cdr(scan);
  }

  clauselist = list_PointerDeleteElement(clauselist, (POINTER)NULL);

  st_IndexDelete(stindex);
  return clauselist;
}


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.
           Checks the clock cnf_REDUCTION with respect to the value
           of flag_CNFREDTIME to permit condesing and subsumption reductions.
***************************************************************/
{
  LIST   termlist,scan,clauselist,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;
  }

  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)) {
    clause = (CLAUSE)list_Car(scan);
    if (res_HasTautology(clause)) {
      clause_Delete(clause);
      list_Rplaca(scan, (POINTER)NULL);
    }
    else
      if (flag_GetFlagIntValue(Flags, flag_CNFCON) == flag_ON) {
	condlist = cond_CondFast(clause);
	if (!list_Empty(condlist))
	  clause_DeleteLiterals(clause, condlist, Flags, Precedence);
	list_Delete(condlist);
      }

    if (flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) != flag_CNFREDTIMELIMITUNLIMITED &&
	flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) <= ceil(clock_GetSeconds(clock_CNFREDUCTION))) {
      flag_SetFlagIntValue(Flags, flag_CNFCON, flag_OFF);
      flag_SetFlagIntValue(Flags, flag_CNFSUB, flag_OFF);
    }
  }

  clauselist = list_PointerDeleteElement(clauselist, (POINTER)NULL);

  if (flag_GetFlagIntValue(Flags, flag_CNFSUB) == flag_ON)
    clauselist    = cnf_SubsumeClauseList(Flags, clauselist);

  return clauselist;
}


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, FLAGSTORE Flags, 
	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, Flags, Precedence, Symblist);
    } 
    else {  /* exist quantifier */
      /* Implementation of the quantifier exchange operator of Ohlbach &
       * Schmidt for the functional translation of modal logics K, KD.  
       * Constants are introduced during Skolemisation */
      if (flag_GetFlagIntValue(Flags, flag_CNFQUANTEXCH)) {  
        Varlist = list_Nil();
        Arity   = 0;
      }
      else {
        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, Flags, 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), Flags, Precedence, Symblist);
  return Term;
}


static TERM cnf_Cnf(TERM Term, FLAGSTORE Flags, 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, flag_GetFlagIntValue(Flags, flag_CNFRENAMING));
  Term = cnf_RemoveEquivImplFromFormula(Term);
  Term = cnf_NegationNormalFormula(Term);
  Term = cnf_SkolemFormula(cnf_AntiPrenex(Term), Flags, 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, Flags, 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_GetFlagIntValue(Flags, flag_DOCPROOF)  || flag_GetFlagIntValue(Flags, flag_FLOTTER)) {
#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_GetFlagIntValue(Flags, flag_DOCPROOF) || flag_GetFlagIntValue(Flags, flag_FLOTTER))
      *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_GetFlagIntValue(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, Flags, 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, Flags, 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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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.
           Checks the clock cnf_REDUCTION with respect to the value
           of flag_CNFREDTIME to permit optimized Skolemization steps.
  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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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);
	      if (flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) != flag_CNFREDTIMELIMITUNLIMITED &&
		  flag_GetFlagIntValue(Flags,flag_CNFREDTIMELIMIT) <= ceil(clock_GetSeconds(clock_CNFREDUCTION)))
		flag_SetFlagIntValue(Flags, flag_CNFOPTSKOLEM, flag_OFF);
#ifdef CHECK_OPTSKOLEM
	      if (flag_GetFlagIntValue(Flags, flag_POPTSKOLEM)) {
		fputs("\nHaveProof result : ", stdout);
		if (result2)
		  fputs("TRUE", stdout);
		else
		  fputs("FALSE", stdout);
	      }
#endif
	    }
	  }
	    
	  if (Result1 || result2) {
	    optimized = TRUE;
	    if (flag_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(Flags, flag_CNFSTRSKOLEM)) {
    /* Initializing array */
    for (i = 1; i <= symbol__MAXSTANDARDVAR; i++)
      cnf_VARIABLEDEPTHARRAY[i] = -1;
  }

  if (flag_GetFlagIntValue(Flags, flag_POPTSKOLEM) ||
      flag_GetFlagIntValue(Flags, flag_PSTRSKOLEM)) {
    fputs("\nTerm before skolemization : \n ", stdout);
    fol_PrettyPrintDFG(Term);
  }

  if (!fol_IsLiteral(Term)) {
    if (flag_GetFlagIntValue(Flags, flag_CNFOPTSKOLEM) ||
	flag_GetFlagIntValue(Flags, flag_CNFSTRSKOLEM))  {
      if (flag_GetFlagIntValue(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, Flags, Precedence, &Symbols);
      list_Delete(Symbols);
    }
  }
  if (flag_GetFlagIntValue(Flags, flag_POPTSKOLEM) ||
      flag_GetFlagIntValue(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_SetFlagIntValue(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:  Initializes and checks the clock_CNFREDUCTION clock with respect
           to the flag_CNFREDTIME value for usable reduction time including
           optimized Skolemization, condensing and subsumption testing.
           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;

  clock_InitCounter(clock_CNFREDUCTION);
  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_GetFlagIntValue(Flags, flag_DOCPROOF))
    prfs_AddDocProofSharingIndex(Search);

  AxTerm           = (TERM)NULL;
  SkolemPredicates = list_Nil();
  Result           = FALSE;
  if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) || flag_GetFlagIntValue(Flags, flag_FLOTTER))
    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);
    AxTerm = fol_RemoveXorNorNand(AxTerm);	
    term_AddFatherLinks(AxTerm);
    fol_NormalizeVars(AxTerm);
    if (flag_GetFlagIntValue(Flags, flag_CNFFEQREDUCTIONS))
      cnf_PropagateSubstEquations(AxTerm);
    AxTerm = cnf_ObviousSimplifications(AxTerm);
    if (flag_GetFlagIntValue(Flags, flag_CNFRENAMING)) {
      term_AddFatherLinks(AxTerm);
      AxTerm = ren_Rename(AxTerm, Precedence, &SkolemPredicates,
			  flag_GetFlagIntValue(Flags, flag_CNFPRENAMING), 
			  flag_GetFlagIntValue(Flags, flag_CNFRENMATCH), 
			  flag_GetFlagIntValue(Flags, flag_CNFRENAMING));
    }
    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_GetFlagIntValue(Flags, flag_DOCPROOF)  || flag_GetFlagIntValue(Flags, flag_FLOTTER)) &&
	  flag_GetFlagIntValue(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);
    ConTerm = fol_RemoveXorNorNand(ConTerm);	
    term_AddFatherLinks(ConTerm);
    fol_NormalizeVars(ConTerm);  
    if (flag_GetFlagIntValue(Flags, flag_CNFFEQREDUCTIONS))
      cnf_PropagateSubstEquations(ConTerm);
    ConTerm  = cnf_ObviousSimplifications(ConTerm); 

    if (flag_GetFlagIntValue(Flags, flag_CNFRENAMING)) {
      term_AddFatherLinks(ConTerm);
      ConTerm = ren_Rename(ConTerm, Precedence, &SkolemPredicates,
			   flag_GetFlagIntValue(Flags, flag_CNFPRENAMING),
			   flag_GetFlagIntValue(Flags, flag_CNFRENMATCH), 
			   flag_GetFlagIntValue(Flags, flag_CNFRENAMING));
    }
    /* 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;
  clock_StartCounter(clock_CNFREDUCTION);

  if (flag_GetFlagIntValue(Flags, flag_CNFOPTSKOLEM) == flag_ON) {   
    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\n", (char*) list_PairFirst(list_Car(Scan)));
#endif 
    Formula            = cnf_SkolemFormula(Formula,Flags,Precedence,&SkolemFunctions);
    Formula            = cnf_DistributiveFormula(Formula);
    FormulaClausesTemp = cnf_MakeClauseList(Formula,FALSE,FALSE,Flags,Precedence);
    if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) || flag_GetFlagIntValue(Flags, flag_FLOTTER)) {
      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);
  }

    /* 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)) {
      /* Set now to FALSE because formula clause relationship for subsequent */
      /* optimized Skolemization steps is then not properly set. However, this */
      /* may cause performance problems */
      Result = FALSE;              
      /*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);
    clock_StopAddPassedTime(clock_CNFREDUCTION);
    /* 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_GetFlagIntValue(Flags, flag_DOCPROOF) || flag_GetFlagIntValue(Flags, flag_FLOTTER)) {
      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(Ax, *AxClauses);
    list_Delete(UsedTerms);
  }

  /* Transfer precedence of new skolem symbols into <InputPrecedence> */
  symbol_TransferPrecedence(Precedence, InputPrecedence);

  list_Delete(ConjectureList);
  if (flag_GetFlagIntValue(Flags, flag_DOCPROOF)  || flag_GetFlagIntValue(Flags, flag_FLOTTER))
    hsh_Delete(InputClauseToTermLabellist);
  if (!flag_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(Flags, flag_CNFRENAMING)) {
    term_AddFatherLinks(Term);
    Term = ren_Rename(Term, Precedence, &SkolemPredicates,
		      flag_GetFlagIntValue(Flags, flag_CNFPRENAMING), 
		      flag_GetFlagIntValue(Flags, flag_CNFRENMATCH),
		      flag_GetFlagIntValue(Flags, flag_CNFRENAMING));
  }
  Term = cnf_RemoveEquivImplFromFormula(Term);
  Term = cnf_NegationNormalFormula(Term);
  Term = cnf_AntiPrenex(Term);
  
  TermCopy = term_Copy(Term);
  TermCopy = cnf_SkolemFormula(TermCopy, Flags, 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_GetFlagIntValue(SubProofFlags, flag_DOCPROOF))
    Formulae2Clause = TRUE;
  else
    Formulae2Clause = FALSE;
  flag_SetFlagIntValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFOFF);
  ResultClauses = cnf_OptimizedSkolemization(cnf_SEARCHCOPY, term_Copy(Term),
					     NULL, &Dummy, Symblist, Result,
					     FALSE, NULL);

  if (Formulae2Clause)
    flag_SetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(Flags, flag_PAPPLYDEFS)) {
    puts("\nConverted to :");
    fol_PrettyPrint(Target);
  }

  targettoprove = cnf_NegationNormalFormula(targettoprove);
  
  if (flag_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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_GetFlagIntValue(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, Flags, Precedence, &symblist);
    result     = cnf_MakeClauseList(clauseterm,FALSE,FALSE,Flags,Precedence);
    list_Delete(symblist);
    term_Delete(clauseterm);
    if (flag_GetFlagIntValue(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;
}