path: root/test/spass/cnf.c

/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *               CNF TRANSLATOR                           * */
/* *                                                        * */
/* *  $Module:   CNF                                        * */
/* *                                                        * */
/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* *                                                        * */
/* $Revision: 21527 $                                       * */
/* $State$                                            * */
/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
/* $Author: duraid $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#include "cnf.h"
#include "rules-inf.h"
#include "rules-red.h"


static TERM   cnf_AntiPrenexPath(TERM, TERM);
static TERM   cnf_ApplyDefinitionInternOnce(TERM, TERM, TERM, TERM, BOOL*);

static SYMBOL cnf_GetDualSymbol(SYMBOL symbol);

static TERM   cnf_IsDefinition(TERM);

static void   cnf_OptimizedSkolemFormula(PROOFSEARCH, TERM, char*, BOOL, TERM,
					 LIST*, LIST*, BOOL, HASH, int);
static int    cnf_PredicateOccurrences(TERM, SYMBOL);

static void   cnf_RplacVar(TERM, LIST, LIST);

static LIST   cnf_SatUnit(PROOFSEARCH, LIST);
static LIST   cnf_SkolemFunctionFormula(TERM, LIST, LIST, PRECEDENCE);

/* For every variable the depth in the current term, required for */
/* strong skolemization */
static int* cnf_VARIABLEDEPTHARRAY;
/* Holds a copy of the ProofSearch--Object built by cnf_Flotter */
/* during cnf_QueryFlotter */
static PROOFSEARCH cnf_SEARCHCOPY;

/* Proofsearch--Object for the function cnf_HaveProof. We need this */
/* to reduce the number of term stamps required. */
static PROOFSEARCH cnf_HAVEPROOFPS;


void cnf_Init(FLAGSTORE Flags)
/***************************************************************
  INPUT:   A flag store.
  RETURNS: None.
  SUMMARY: Initializes the CNF Module.
  EFFECTS: Initializes global variables.
  CAUTION: MUST BE CALLED BEFORE ANY OTHER CNF-FUNCTION.
***************************************************************/
{
  /* If strong skolemization is performed, allocate array for variable depth */
  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))
    cnf_VARIABLEDEPTHARRAY = (int*) memory_Malloc(sizeof(int[symbol__MAXSTANDARDVAR + 1]));
  else
    cnf_VARIABLEDEPTHARRAY = NULL;
  cnf_SEARCHCOPY  = prfs_Create();
  cnf_HAVEPROOFPS = prfs_Create();
}


void cnf_Free(FLAGSTORE Flags)
/**************************************************************
  INPUT:   A flag store.
  RETURNS: None.
  SUMMARY: Frees the CNF Module.
***************************************************************/
{
  /* If strong skolemization is performed, free array for variable depth */
  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
    memory_Free(cnf_VARIABLEDEPTHARRAY, sizeof(int) * (symbol__NOOFSTANDARDVAR + 1));
    cnf_VARIABLEDEPTHARRAY = NULL;
  }
  prfs_Delete(cnf_SEARCHCOPY);
  cnf_SEARCHCOPY = NULL;
  prfs_Delete(cnf_HAVEPROOFPS);
  cnf_HAVEPROOFPS = NULL;
}


static int cnf_GetFormulaPolarity(TERM term, TERM subterm)
/**********************************************************
  INPUT:   Two terms term and subterm where subterm is a
           subterm of term.
  RETURNS: The polarity of subterm in term.
********************************************************/
{  
  LIST   scan;
  TERM   term1;
  int    polterm1,bottom; 

  bottom = vec_ActMax();
  vec_Push((POINTER) 1);
  vec_Push(term);

  do {
    term1    = (TERM)vec_PopResult();
    polterm1 = (int)vec_PopResult();
    if (term1 == subterm) {
      vec_SetMax(bottom);
      return polterm1;
    }else
      if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {
	vec_Push((POINTER) (- polterm1));
	vec_Push(list_Car(term_ArgumentList(term1)));
      }
    if (symbol_Equal(term_TopSymbol(term1),fol_Exist()) ||
	symbol_Equal(term_TopSymbol(term1),fol_All())) {
      vec_Push((POINTER)polterm1);
      vec_Push(list_Second(term_ArgumentList(term1)));
    }
    else
      if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
	vec_Push((POINTER) (- polterm1));
	vec_Push(list_Car(term_ArgumentList(term1)));
	vec_Push((POINTER) polterm1);
	vec_Push(list_Second(term_ArgumentList(term1)));
      }
      else
	if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) {
	  vec_Push(0);
	  vec_Push(list_Car(term_ArgumentList(term1)));
	  vec_Push(0);
	  vec_Push(list_Second(term_ArgumentList(term1)));
	}
	else
	  if (symbol_Equal(term_TopSymbol(term1),fol_And()) ||
	      symbol_Equal(term_TopSymbol(term1),fol_Or())) {
	    for (scan = term_ArgumentList(term1);
		 !list_Empty(scan);
		 scan = list_Cdr(scan)) {
	      vec_Push((POINTER) polterm1);
	      vec_Push(list_Car(scan));
	    }
	  }
  } while (bottom != vec_ActMax());
  vec_SetMax(bottom);
  misc_StartErrorReport();
  misc_ErrorReport("\n In cnf_GetFormulaPolarity: Wrong arguments !\n");
  misc_FinishErrorReport();
  return -2;
}


static BOOL cnf_ContainsDefinitionIntern(TERM TopDef, TERM Def, int Polarity,
					 TERM* FoundPred)
/**********************************************************
  INPUT:   A term TopDef which is the top level term of the recursion.
           A term Def which is searched for a definition.
           A pointer to a term into which the predicate of the definition
	   is stored if it is found.
  RETURNS: TRUE if Def contains a definition that can be converted
           to standard form.
********************************************************/
{
  /* AND / OR */
  /* In these cases Def cannot be converted to standard form */

  if ((symbol_Equal(term_TopSymbol(Def),fol_And()) && (Polarity == 1)) ||
      (symbol_Equal(term_TopSymbol(Def),fol_Or()) && (Polarity == -1)))
    return FALSE;

  if (symbol_Equal(term_TopSymbol(Def), fol_And()) ||
     symbol_Equal(term_TopSymbol(Def),fol_Or())) {
    /* Polarity is ok */
    LIST l;
    for (l=term_ArgumentList(Def); !list_Empty(l); l=list_Cdr(l))
      if (cnf_ContainsDefinitionIntern(TopDef, list_Car(l), Polarity, FoundPred))
	return TRUE;
    return FALSE;
  }

  /* Quantifiers */
  if (fol_IsQuantifier(term_TopSymbol(Def)))
    return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
  
  /* Negation */
  if (symbol_Equal(term_TopSymbol(Def),fol_Not()))
    return cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred);
  
  /* Implication */
  if (symbol_Equal(term_TopSymbol(Def),fol_Implies())) {
    if (Polarity==1) {
      if (cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred))
	return TRUE;
      return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
    }
    return FALSE;
  }
  
  /* Equivalence */
  if (symbol_Equal(term_TopSymbol(Def),fol_Equiv()) && (Polarity==1)) {
    /* Check if equivalence itself is in correct form */
    TERM defpredicate;

    defpredicate = cnf_IsDefinition(Def);
    if (defpredicate != (TERM) NULL) {
      LIST predicate_vars, l, defpath;
      BOOL allquantifierfound;
      TERM super;
      int pol;
      /* Check if predicate occurs several times in TopDef */
      /* if (cnf_PredicateOccurrences(TopDef, term_TopSymbol(defpredicate)) > 1) {}
	 puts("\n Predicate occurs more than once.");
	 return FALSE; */


      /* Now make sure that the variables of the predicate are       */
      /* all--quantified and not in the scope of an exist quantifier */
      /*      predicate_vars = list_Copy(term_ArgumentList(defpredicate)); */
      predicate_vars = term_ListOfVariables(defpredicate);
      predicate_vars = term_DeleteDuplicatesFromList(predicate_vars);

      /* So far (going bottom--up) no all-quantifier was found for */
      /* a variable of the predicates' arguments */
      allquantifierfound = FALSE;
      
      /* Build defpath here by going bottom up */
      /* At first, list of superterms on path is top down */
      defpath = list_Nil();
      super = Def;
      while (super != (TERM) NULL) {
	defpath = list_Cons(super, defpath);
	super = term_Superterm(super);
      }
      /* No go top down and add polarities */
      pol = 1;
      for (l=defpath; !list_Empty(l); l=list_Cdr(l)) {
	list_Rplaca(l, list_PairCreate((TERM) list_Car(l), (LIST) pol));
	if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Not()))
	  pol = -pol;
	else {
	  if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Implies()) &&
	      (term_FirstArgument((TERM) list_Car(l)) == (TERM) list_Car(list_Cdr(l))))
	    pol = -pol;
	  else 
	    if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Equiv()))
	      pol = 0;
	}
      }
      /* <defpath> is now a list of pairs (term, polarity) */
      for (l=defpath; !list_Empty(l) && !list_Empty(predicate_vars); l=list_Cdr(l)) {
	LIST pair;
	TERM t;
	int p;
	/* Pair Term t / Polarity p */
	pair = (LIST) list_Car(l);
	t = (TERM) list_PairFirst(pair);
	p = (int) list_PairSecond(pair);

	if (fol_IsQuantifier(term_TopSymbol(t))) {
	  
	  /* Variables of the predicate that are universally quantified are no problem */
	  if ((symbol_Equal(term_TopSymbol(t), fol_All()) && (p==1)) ||
	      (symbol_Equal(term_TopSymbol(t), fol_Exist()) && (p==-1))) {
	    LIST scan;
	    allquantifierfound = TRUE;
	    for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan))
	      predicate_vars = list_DeleteElement(predicate_vars,(TERM) list_Car(scan),
						  (BOOL (*)(POINTER,POINTER))term_Equal);
	  }
	  else {
	    /* Check if allquantified variables of the predicate are in scope of an exist--quantifier */
	    /* We already found an all quantified variable */
	    if (allquantifierfound) {
	      list_Delete(predicate_vars);
	      list_DeletePairList(defpath);
	      return FALSE;
	    }
	    else {
	      LIST scan;
	      /* Check if a variable of the predicate is exist--quantified */
	      for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan)) {
		if (term_ListContainsTerm(predicate_vars, list_Car(scan))) {
		  list_Delete(predicate_vars);
		  list_DeletePairList(defpath);
		  return FALSE;
		}
	      }
	    }
	  }
	}
      }
      
#ifdef CHECK
      if (!list_Empty(predicate_vars)) {
	list_Delete(predicate_vars);
	misc_StartErrorReport();
	misc_ErrorReport("\n In cnf_ContainsDefinitionIntern: Definition has free variables.\n");
	misc_FinishErrorReport();
      }
#endif
      list_DeletePairList(defpath);
      *FoundPred = defpredicate;
      return TRUE;
    }
  }
  
  return FALSE;
}


BOOL cnf_ContainsDefinition(TERM Def, TERM* FoundPred)
/**********************************************************
  INPUT:   A term Def which is searched for a definition of a predicate.
           A pointer to a term into which the predicate of the definition
	   is stored if it is found.
  RETURNS: TRUE if Def contains a definition that can be converted to
           standard form.
***********************************************************/
{
  BOOL result;
#ifdef CHECK
  fol_CheckFatherLinks(Def);
#endif
  result = cnf_ContainsDefinitionIntern(Def, Def, 1, FoundPred);
#ifdef CHECK
  fol_CheckFatherLinks(Def);
#endif
  return result;
}


static TERM cnf_IsDefinition(TERM Def)
/**********************************************************
 INPUT:   A term Def.
 RETURNS: The Def term where the arguments of the equivalence are exchanged
          iff the first one is not a predicate.
**********************************************************/
{
  LIST l,freevars, predicatevars;

#ifdef CHECK
  if (Def == NULL) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_IsDefinition: Empty formula.\n");
    misc_FinishErrorReport();
  }
  if (!symbol_Equal(term_TopSymbol(Def),fol_Equiv())) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_IsDefinition: Formula is no equivalence.\n");
    misc_FinishErrorReport();
  }
#endif
  
  /* If the predicate is the second argument of the equivalence, exchange them */
  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) {
    TERM arg1;
    arg1 = term_FirstArgument(Def);
    term_RplacFirstArgument(Def, term_SecondArgument(Def));
    term_RplacSecondArgument(Def, arg1);
  }


  /* Check if the first argument is a predicate */
  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) 
    return NULL;

  /* Check if first argument is a predicate and not fol_Equality */
  /*  if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))
      || symbol_Equal(term_TopSymbol(term_FirstArgument(Def)), fol_Equality()))) {
      return NULL;
      }*/


  /* The free variables of the non-predicate term must occur in the predicate term */
  
  freevars = fol_FreeVariables(term_SecondArgument(Def));
  freevars = term_DeleteDuplicatesFromList(freevars);
  predicatevars = term_ListOfVariables(term_FirstArgument(Def));
  predicatevars = term_DeleteDuplicatesFromList(predicatevars);

  for (l=predicatevars; !list_Empty(l); l=list_Cdr(l))
    freevars = list_DeleteElement(freevars, list_Car(l),
				  (BOOL (*)(POINTER,POINTER))term_Equal);

  if (!list_Empty(freevars)) {
    list_Delete(freevars);
    list_Delete(predicatevars);
    return NULL;
  }

  list_Delete(predicatevars);
  return term_FirstArgument(Def);
}


static BOOL cnf_ContainsPredicateIntern(TERM Target, SYMBOL Predicate, 
					int Polarity, TERM* TargetPredicate,
					TERM* ToTopLevel, LIST* TargetVars,
					LIST* VarsForTopLevel)
/**********************************************************
  INPUT:   A term (sub--) Target
           A symbol Predicate which is searched in the target term.
           The polarity of the subterm.
           A pointer to the term TargetPredicate into which the found
	   predicate term is stored.
           A pointer to the list TargetVars into which the variables found
	   in the predicates' arguments are stored.
           A pointer to a list VarsForTopLevel into which all variables are
	   stored that are all--quantified and can be moved to top level.

  RETURNS: TRUE if Formula contains the predicate for which a definition
           was found.
********************************************************/
{
  /* AND / OR */
  /* In these cases the predicate (if it exists) can not be moved to a higher level */

  if ((symbol_Equal(term_TopSymbol(Target),fol_And()) && Polarity == 1) ||
      (symbol_Equal(term_TopSymbol(Target),fol_Or()) && Polarity == -1) ||
      (symbol_Equal(term_TopSymbol(Target),fol_Implies()) && Polarity != 1) ||
      symbol_Equal(term_TopSymbol(Target), fol_Equiv())) {
    TERM s;
    LIST l;
    /* Try to find Predicate in Target */
    s = term_FindSubterm(Target, Predicate);
    if (s == NULL)
      return FALSE;
    
    /* Store variables found in the predicates arguments */
    for (l=term_ArgumentList(s); !list_Empty(l); l = list_Cdr(l))
      *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars);
    *TargetVars = term_DeleteDuplicatesFromList(*TargetVars);
    /* Keep found predicate */
    *TargetPredicate = s;
    *ToTopLevel = Target;
    return TRUE;
  }
  
  /* AND / OR continued */
  if (symbol_Equal(term_TopSymbol(Target),fol_And()) || symbol_Equal(term_TopSymbol(Target),fol_Or())) {
    /* The polarity is ok here */
    LIST l;
    for (l=term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l))
      if (cnf_ContainsPredicateIntern((TERM) list_Car(l), Predicate, Polarity,
				      TargetPredicate, ToTopLevel, TargetVars,
				      VarsForTopLevel))
	return TRUE;
    return FALSE;
  }

  /* Quantifiers */
  if (fol_IsQuantifier(term_TopSymbol(Target))) {
    if (cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate,
				    Polarity, TargetPredicate, ToTopLevel,
				    TargetVars, VarsForTopLevel)) {
      /* Quantifiers for free variables of the predicate should be moved
	 to top level to make the proof easier */
      if ((symbol_Equal(term_TopSymbol(Target), fol_All()) && Polarity == 1) ||
	  (symbol_Equal(term_TopSymbol(Target), fol_Exist()) && Polarity == -1)) {
	LIST l;
	/* Check for all variables found in the predicates arguments */
	for (l = *TargetVars; !list_Empty(l); l=list_Cdr(l)) {
	  if (term_ListContainsTerm(fol_QuantifierVariables(Target),list_Car(l)))
	    *VarsForTopLevel = list_Cons(list_Car(l), *VarsForTopLevel);
	}
      }
      return TRUE;
    }
    return FALSE;
  }

  /* Negation */
  if (symbol_Equal(term_TopSymbol(Target),fol_Not()))
    return cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate,
				       -Polarity, TargetPredicate, ToTopLevel,
				       TargetVars, VarsForTopLevel);
  /* Implication */
  if (symbol_Equal(term_TopSymbol(Target),fol_Implies())) {
    /* In this case the predicate (if it exists) can be moved to a higher level */
    if (cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate,
				    -Polarity, TargetPredicate, ToTopLevel,
				    TargetVars, VarsForTopLevel))
      return TRUE;
    return cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate,
				       Polarity, TargetPredicate, ToTopLevel,
				       TargetVars, VarsForTopLevel);
  }

  /* Found the predicate */
  if (symbol_Equal(term_TopSymbol(Target), Predicate)) {
    LIST l;
    for (l = term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l))
      *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars);
    *TargetVars = term_DeleteDuplicatesFromList(*TargetVars);
    
    *TargetPredicate = Target;
    *ToTopLevel      = Target;
    return TRUE;
  }
  
  /* In all other cases the predicate was not found */
  return FALSE;
}  

  
BOOL cnf_ContainsPredicate(TERM Target, SYMBOL Predicate,
			   TERM* TargetPredicate, TERM* ToTopLevel,
			   LIST* TargetVars, LIST* VarsForTopLevel)
/**********************************************************
  INPUT:   A term Target without implications.
           A symbol Predicate which is searched in the target term.
           A pointer to the predicate found in TargetTerm is recorded.
           A pointer to the term TargetPredicate into which the found
	   predicate term is stored.
           A pointer to the list TargetVars into which the variables
	   found in the predicates' arguments are stored.
           A pointer to a list VarsForTopLevel into which all variables
	   are stored that are all--quantified and can be moved to top level.
  RETURNS: TRUE if Formula contains the predicate for which a definition
           was found.
********************************************************/
{
  BOOL result;
#ifdef CHECK
  fol_CheckFatherLinks(Target);
#endif
  result = cnf_ContainsPredicateIntern(Target, Predicate, 1, TargetPredicate,
				       ToTopLevel, TargetVars, VarsForTopLevel);
#ifdef CHECK
  fol_CheckFatherLinks(Target);
#endif
  return result;
}


static int cnf_PredicateOccurrences(TERM Term, SYMBOL P)
/****************************************************
  INPUT:   A term and a predicate symbol.
  RETURNS: The number of occurrences of the predicate symbol in Term
**************************************************/			       
{
  /* Quantifiers */
  if (fol_IsQuantifier(term_TopSymbol(Term)))
    return cnf_PredicateOccurrences(term_SecondArgument(Term), P);

  /* Junctors and NOT */
  if (fol_IsJunctor(term_TopSymbol(Term)) ||
      symbol_Equal(term_TopSymbol(Term),fol_Not())) {
    LIST scan;
    int count;
    count = 0;
    for (scan=term_ArgumentList(Term); !list_Empty(scan); scan=list_Cdr(scan)) {
      count += cnf_PredicateOccurrences(list_Car(scan), P);
      /* Only the cases count==1 and count>1 are important */
      if (count > 1)
	return count;
    }
    return count;
  }
  
  if (symbol_Equal(term_TopSymbol(Term), P))
    return 1;
  return 0;
} 
  

static TERM cnf_NegationNormalFormulaPath(TERM Term, TERM PredicateTerm)
/**********************************************************
  INPUT:   A term and a predicate term which is a subterm of term
  RETURNS: The negation normal form of the term along the path.
  CAUTION: The term is destructively changed.
           This works only if the superterm member of Term and its subterms 
	   are set.
********************************************************/
{
  TERM   subterm, termL, term1;
  LIST   scan;
  SYMBOL symbol;
  BOOL   set;

  term1 = Term;
  while (term1 != NULL) {
    set = FALSE;
    if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {	    
      subterm = term_FirstArgument(term1);
      if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) {
	LIST l;
	term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm)));
	list_Delete(term_ArgumentList(term1));
	term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm)));
	term_Free(term_FirstArgument(subterm));
	list_Delete(term_ArgumentList(subterm));
	term_Free(subterm);
	/* Set superterm member to new superterm */
	for (l=term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l))
	  term_RplacSuperterm(list_Car(l), term1);
	/* term1 weiter betrachten */
	set = TRUE;
      }
      else {
	if (fol_IsQuantifier(term_TopSymbol(subterm))) {
	  LIST l;
	  symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
	  termL  = term_CreateAddFather(fol_Not(),
					list_List(term_SecondArgument(subterm)));
	  list_RplacSecond(term_ArgumentList(subterm), termL);
	  term_RplacSuperterm(termL, subterm);
	  term_RplacTop(term1,symbol);
	  list_Delete(term_ArgumentList(term1));
	  term_RplacArgumentList(term1, term_ArgumentList(subterm));
	  for (l=term_ArgumentList(term1); !list_Empty(l); l = list_Cdr(l))
	    term_RplacSuperterm(list_Car(l), term1);
	  term_RplacArgumentList(subterm, list_Nil());
	  term_Delete(subterm);
	  term1 = termL;
	  /* Next term to check is not(subterm) */
	  set = TRUE;
	} 
	else {
	  if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || 
	      (symbol_Equal(term_TopSymbol(subterm),fol_And()))) {
	    LIST l;
	    symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
	    for (scan = term_ArgumentList(subterm); !list_Empty(scan);
		 scan = list_Cdr(scan)) {
	      TERM new;
	      termL = list_Car(scan);
	      new = term_CreateAddFather(fol_Not(),list_List(termL));
	      list_Rplaca(scan, new);
	      term_RplacSuperterm(new, subterm);
	    }
	    term_RplacTop(term1,symbol);
	    list_Delete(term_ArgumentList(term1));
	    term_RplacArgumentList(term1,term_ArgumentList(subterm));
	    for (l = term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l))
	      term_RplacSuperterm(list_Car(l), term1);
	    term_RplacArgumentList(subterm, list_Nil());
	    term_Delete(subterm);
	  }
	}
      }
    }
    if (!set) {
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	  if (term_HasProperSuperterm(PredicateTerm, list_Car(scan))) {
	    term1 = list_Car(scan);
	    set = TRUE;
	    break;
	  }
      if (!set)
	term1 = NULL;
    }
  }
  return Term;
}


TERM cnf_ApplyDefinitionOnce(TERM Predicate, TERM Formula, TERM TargetTerm,
			     TERM TargetPredicate, FLAGSTORE Flags)
/*********************************************************
  INPUT:   A term Predicate which is a predicate found in a definition.
           A term Formula which is a term equivalent to the predicate.
           A term TargetTerm in which one occurrence of the predicate may be 
           replaced by the Formula.
           A term TargetPredicate which is the subterm of the TargetTerm
           to be replaced.
	   A flag store.
  RETURNS: The changed TargetTerm.
*************************************************************/
{
  SYMBOL maxvar, maxvar_temp;
  LIST bound, scan;
  BOOL success;
  
  /* Init varcounter */
  maxvar = term_MaxVar(TargetTerm);
  maxvar_temp = term_MaxVar(Formula);
  if (maxvar_temp > maxvar)
    maxvar = maxvar_temp;
  symbol_SetStandardVarCounter(maxvar);

  /* Find bound variables in formula for renaming them */
  bound = fol_BoundVariables(Formula);
  for (scan=bound; !list_Empty(scan); scan=list_Cdr(scan)) {
    /* Bound variable in definition is already used in term */
    if (term_ContainsSymbol(TargetTerm, term_TopSymbol(list_Car(scan))))
      term_ExchangeVariable(Formula, term_TopSymbol(list_Car(scan)),
			    symbol_CreateStandardVariable());
  }
  list_Delete(bound);
  TargetTerm = cnf_ApplyDefinitionInternOnce(Predicate, Formula, TargetTerm, 
					     TargetPredicate,&success);
  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
    if (success) {
      fputs("\nTarget after applying def:\n", stdout);
      fol_PrettyPrint(TargetTerm);
      puts("\n");
    }
  }
  
  return TargetTerm;
}


static TERM cnf_ApplyDefinitionInternOnce(TERM Predicate, TERM Formula, 
					  TERM TargetTerm, TERM TargetPredicate,
					  BOOL* Success)
/**********************************************************
  INPUT:   A term Predicate which is equivalence to
           Formula and Term
  RETURNS: The term in which all occurrences of P(..) are 
           replaced by Formula modulo the proper bindings
  CAUTION: Term is destructively changed!
***********************************************************/
{
  /* Quantifiers */
  if (fol_IsQuantifier(term_TopSymbol(TargetTerm))) {
    term_RplacSecondArgument(TargetTerm, 
      cnf_ApplyDefinitionInternOnce(Predicate, Formula, 
				    term_SecondArgument(TargetTerm),
				    TargetPredicate, Success));
    term_RplacSuperterm(term_SecondArgument(TargetTerm), TargetTerm);
    return TargetTerm;
  }

  /* Junctors and NOT */
  if (fol_IsJunctor(term_TopSymbol(TargetTerm)) ||
      symbol_Equal(term_TopSymbol(TargetTerm),fol_Not())) {
    LIST scan;
    for (scan=term_ArgumentList(TargetTerm); !list_Empty(scan); scan=list_Cdr(scan)) {
      list_Rplaca(scan, cnf_ApplyDefinitionInternOnce(Predicate, Formula, 
						      list_Car(scan), 
						      TargetPredicate, Success));
      term_RplacSuperterm((TERM) list_Car(scan), TargetTerm);
    }
    return TargetTerm;
  }
  
  if (symbol_Equal(term_TopSymbol(TargetTerm), term_TopSymbol(Predicate))) {
    if (TargetTerm == TargetPredicate) {
      TERM result;
      result = Formula;
      cnf_RplacVar(result, term_ArgumentList(Predicate), 
		   term_ArgumentList(TargetTerm));
      term_AddFatherLinks(result);
      term_Delete(TargetTerm);
      *Success = TRUE;
      return result;
    }
  }
  
  return TargetTerm;
} 


static TERM cnf_RemoveEquivImplFromFormula(TERM term)
/**********************************************************
  INPUT:   A term.
  RETURNS: The term  with replaced implications and equivalences.
  CAUTION: The term is destructively changed.
********************************************************/
{
  TERM term1,termL,termR,termLneg,termRneg;
  LIST scan;
  int  bottom,pol;
  
  bottom = vec_ActMax();
  vec_Push(term);

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
      term_RplacTop(term1, fol_Or());
      list_Rplaca(term_ArgumentList(term1),
		  term_Create(fol_Not(), list_List(list_Car(term_ArgumentList(term1)))));
    }else
      if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) {
	pol      = cnf_GetFormulaPolarity(term,term1);
	termL    = (TERM)list_Car(term_ArgumentList(term1));
	termR    = (TERM)list_Second(term_ArgumentList(term1));
	termLneg = term_Create(fol_Not(),list_List(term_Copy(termL)));
	termRneg = term_Create(fol_Not(),list_List(term_Copy(termR)));
	if (pol == 1 || pol == 0) {
	  term_RplacTop(term1, fol_And());
	  list_Rplaca(term_ArgumentList(term1), term_Create(fol_Or(),list_Cons(termLneg,list_List(termR))));
	  list_RplacSecond(term_ArgumentList(term1),term_Create(fol_Or(),list_Cons(termRneg,list_List(termL))));
	}else
	  if (pol == -1) {
	    term_RplacTop(term1, fol_Or());
	    list_Rplaca(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termLneg,list_List(termRneg))));
	    list_RplacSecond(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termL,list_List(termR))));
	  }
      }  
    if (!list_Empty(term_ArgumentList(term1)))
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	vec_Push(list_Car(scan));
  }
  vec_SetMax(bottom);
  return term;
}


static TERM cnf_MovePredicateVariablesUp(TERM Term, TERM TargetPredicateTerm,
					 LIST VarsForTopLevel)
/**********************************************************
  INPUT:   A term and a predicate term which is a subterm of term
           an equivalence.
  RETURNS: The term where the free variables of the equivalence, which
           must be allquantified and not in the scope of an 
	   exist quantifier, are moved to toplevel.
  CAUTION: The term is destructively changed.
********************************************************/
{
  TERM term1;
  LIST scan;
  int  bottom;

  bottom = vec_ActMax();
  vec_Push(Term);
  
  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (!list_Empty(term_ArgumentList(term1)))
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) {
	TERM arg;
	arg = (TERM) list_Car(scan);
	if (term_HasProperSuperterm(TargetPredicateTerm, arg)) {
	  if (symbol_Equal(term_TopSymbol(arg), fol_All())) {
	    LIST predicatevarscan, quantifiervars;
	    quantifiervars = fol_QuantifierVariables(arg);
	    for (predicatevarscan=VarsForTopLevel; !list_Empty(predicatevarscan);
		predicatevarscan = list_Cdr(predicatevarscan))
	      quantifiervars = list_DeleteElementFree(quantifiervars, 
						      (TERM) list_Car(predicatevarscan),
						      (BOOL (*)(POINTER,POINTER))term_Equal,
						      (void (*)(POINTER))term_Delete);
	    if (!list_Empty(quantifiervars))
	      term_RplacArgumentList(term_FirstArgument(arg), quantifiervars);
	    else {
	      TERM subterm;
	      subterm = term_SecondArgument(arg);
	      term_Free(term_FirstArgument(arg));
	      list_Delete(term_ArgumentList(arg));
	      term_Free(arg);
	      list_Rplaca(scan, subterm);
	      term_RplacSuperterm(subterm, term1);
	    }
	  }
	  vec_Push((TERM) list_Car(scan));
	}
      }
  }
  
  for (scan=VarsForTopLevel; !list_Empty(scan); scan = list_Cdr(scan))
    list_Rplaca(scan, term_Copy((TERM) list_Car(scan)));
  if (symbol_Equal(term_TopSymbol(Term), fol_All())) {
    LIST vars;
    vars = fol_QuantifierVariables(Term);
    vars = list_Nconc(vars, list_Copy(VarsForTopLevel));
    vars = term_DestroyDuplicatesInList(vars);
    term_RplacArgumentList(term_FirstArgument(Term), vars);
  }
  else {
    TERM newtop;
    newtop = fol_CreateQuantifier(fol_All(), list_Copy(VarsForTopLevel), list_List(Term));
    term_RplacSuperterm(Term, newtop);
    Term = newtop;
  }
  vec_SetMax(bottom);
  return Term;
}


static TERM cnf_RemoveImplFromFormulaPath(TERM Term, TERM PredicateTerm)
/**********************************************************
  INPUT:   A term and a predicate term which is a subterm of term
  RETURNS: The term where implications along the path to PredicateTerm 
           are replaced.
  CAUTION: The term is destructively changed.
           This works only if the superterm member of Term and its 
	   subterms are set.
********************************************************/
{
  TERM term1;
  LIST scan;
  int  bottom;
  
  bottom = vec_ActMax();
  vec_Push(Term);
  
  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (term_HasProperSuperterm(PredicateTerm, term1)) {
      if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
	TERM newterm;
	term_RplacTop(term1, fol_Or());
	newterm = term_CreateAddFather(fol_Not(), list_List(list_Car(term_ArgumentList(term1))));
	list_Rplaca(term_ArgumentList(term1), newterm);
	term_RplacSuperterm(newterm, term1);
      }
      
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	  vec_Push(list_Car(scan));
    }
  }
  vec_SetMax(bottom);
  return Term;
}


static SYMBOL cnf_GetDualSymbol(SYMBOL symbol)
/********************************************************
  INPUT:   A predefined symbol.
  RETURNS: The dual symbol.
********************************************************/
{
  SYMBOL dual;

  dual = symbol;
  if (symbol_Equal(symbol,fol_All()))
    dual = fol_Exist();
  else
    if (symbol_Equal(symbol,fol_Exist()))
      dual = fol_All();
    else
      if (symbol_Equal(symbol,fol_Or()))
	dual = fol_And();
      else
	if (symbol_Equal(symbol,fol_And()))
	  dual =  fol_Or();
  return dual;
}


TERM cnf_NegationNormalFormula(TERM term)
/********************************************************
  INPUT:   A term.
  RETURNS: The negation normal form of the term.
  CAUTION: The term is destructively changed.
********************************************************/
{
  TERM   term1,subterm,termL;
  LIST   scan;
  SYMBOL symbol;
  int    bottom;
  
  bottom = vec_ActMax();
  vec_Push(term);

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {	    
      subterm = (TERM)list_Car(term_ArgumentList(term1));
      if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) {
	term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm)));
	list_Delete(term_ArgumentList(term1));
	term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm)));
	term_Free(term_FirstArgument(subterm));
	list_Delete(term_ArgumentList(subterm));
	term_Free(subterm);
	vec_Push(term1);
      }else 
	if (fol_IsQuantifier(term_TopSymbol(subterm))) {
	  symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
	  termL  = term_Create(fol_Not(),
			       list_List(term_SecondArgument(subterm)));
	  list_RplacSecond(term_ArgumentList(subterm), termL);
	  term_RplacTop(term1,symbol);
	  list_Delete(term_ArgumentList(term1));
	  term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm)));
	  term_Delete(subterm);
	} else
	  if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || 
	      symbol_Equal(term_TopSymbol(subterm),fol_And())) {
	    symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm));
	    for (scan = term_ArgumentList(subterm);
		 !list_Empty(scan);
		 scan = list_Cdr(scan)) {
	      termL = (TERM)list_Car(scan);
	      list_Rplaca(scan, term_Create(fol_Not(),list_List(termL)));
	    }
	    term_RplacTop(term1,symbol);
	    list_Delete(term_ArgumentList(term1));
	    term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm)));
	    term_Delete(subterm); 
	  }
    }
    if (!list_Empty(term_ArgumentList(term1)))
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	vec_Push(list_Car(scan));
  }
  vec_SetMax(bottom);
  return term;
}


static TERM cnf_QuantMakeOneVar(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: The term where all quantifiers quantify over only one variable.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  TERM   term1,termL;
  SYMBOL quantor;
  LIST   scan,varlist;
  int    bottom;
  
  bottom = vec_ActMax();
  vec_Push(term);       

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (fol_IsQuantifier(term_TopSymbol(term1))) {
      quantor = term_TopSymbol(term1);
      if (list_Length(term_ArgumentList(term_FirstArgument(term1))) > 1) {
	varlist =
	  list_Copy(list_Cdr(term_ArgumentList(term_FirstArgument(term1))));
	for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) {
	  termL = term_SecondArgument(term1);
	  term_RplacSecondArgument(term1, fol_CreateQuantifier(quantor,list_List(list_Car(scan)),list_List(termL)));
	}
	for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) {
	  term_RplacArgumentList(term_FirstArgument(term1), 
				 list_PointerDeleteElement(term_ArgumentList(term_FirstArgument(term1)),list_Car(scan)));
	}
	list_Delete(varlist);
      }
    }
    if (!list_Empty(term_ArgumentList(term1)))
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	vec_Push(list_Car(scan));
  }
  vec_SetMax(bottom);
  return term;
}


static LIST cnf_GetSymbolList(LIST varlist)
/**************************************************************
  INPUT:   A list of variables
  RETURNS: The list of the symbols of the variables.
***************************************************************/
{
  LIST scan,result;

  result = list_Nil();
  for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan))
    result = list_Cons((POINTER)term_TopSymbol((TERM)list_Car(scan)),result);

  return result;
}


static BOOL cnf_TopIsAnd(LIST termlist)
/**************************************************************
  INPUT:   A list of terms.
  RETURNS: True if one term in termlist is a conjunction.
***************************************************************/
{
  LIST scan;

  for (scan=termlist;!list_Empty(scan);scan=list_Cdr(scan))
    if (term_TopSymbol(list_Car(scan)) == fol_And())
      return TRUE;
  return FALSE;
}


static TERM cnf_MakeOneOr(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all arguments of an or together.
  CAUTION: The term is destructively changed.
***************************************************************/
{

  LIST   scan;

  if (symbol_Equal(term_TopSymbol(term),fol_Or())) {
    TERM   argterm;
    scan=term_ArgumentList(term);
    while (!list_Empty(scan)) {
      argterm = (TERM)list_Car(scan);
      cnf_MakeOneOr(argterm);
      if (symbol_Equal(term_TopSymbol(argterm),fol_Or())) {
	scan = list_Cdr(scan);
	term_RplacArgumentList(term,
			       list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm)));
	term_Free(argterm);
      }
      else
	scan = list_Cdr(scan);
    }
  } else if (!symbol_IsPredicate(term_TopSymbol(term)))
    for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan))
      cnf_MakeOneOr(list_Car(scan));
  
  return term;
}


static TERM cnf_MakeOneOrPredicate(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all predicates and negated predicates as arguments 
           of an or together.
  CAUTION: The term is destructively changed.
***************************************************************/
{

  LIST   scan,scan1,predlist;

  if (cnf_TopIsAnd(term_ArgumentList(term))) {
    
    for (scan1=term_ArgumentList(term);
	 !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_And()));
	 scan1=list_Cdr(scan1));

    if (!list_Empty(scan1)) {
      predlist = list_Nil();
      for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) {
	if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
	    fol_IsNegativeLiteral(list_Car(scan))) {
	  predlist = list_Cons(list_Car(scan),predlist);
	}
      }
      for (scan=predlist;!list_Empty(scan);scan=list_Cdr(scan))
	term_RplacArgumentList(term,
			       list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan)));
      
      if (!list_Empty(predlist))
	term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term)));
    }
  }
  return term;
}


static TERM cnf_MakeOneOrTerm(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all predicates as arguments of an or together.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  return cnf_MakeOneOrPredicate(cnf_MakeOneOr(term));
}


static TERM cnf_MakeOneAnd(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all arguments of an and together.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   scan;

  if (symbol_Equal(term_TopSymbol(term),fol_And())) {
    TERM   argterm;
    scan=term_ArgumentList(term);
    while (!list_Empty(scan)) {
      argterm = (TERM)list_Car(scan);
      cnf_MakeOneAnd(argterm);
      if (symbol_Equal(term_TopSymbol(argterm),fol_And())) {
	scan = list_Cdr(scan);
	term_RplacArgumentList(term,
			       list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm)));
	term_Free(argterm);
      }
      else
	scan = list_Cdr(scan);
    }
  } else if (!symbol_IsPredicate(term_TopSymbol(term)))
    for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan))
      cnf_MakeOneAnd(list_Car(scan));

  return term;
}


static TERM cnf_MakeOneAndPredicate(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all predicates as arguments of one or together.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   scan,scan1,predlist;
  
  for (scan1=term_ArgumentList(term);
       !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_Or()));
       scan1=list_Cdr(scan1));
  
  if (!list_Empty(scan1)) {
    /* The car of scan1 points to a term with topsymbol 'or' */
    predlist = list_Nil();
    for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) {
      if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) &&
	  fol_IsNegativeLiteral(list_Car(scan))) {
	predlist = list_Cons(list_Car(scan),predlist);
      }
    }
    for (scan=predlist; !list_Empty(scan); scan=list_Cdr(scan))
      term_RplacArgumentList(term, list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan)));
    
    if (!list_Empty(predlist))
      term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term)));
  }
  return term;
}


static TERM cnf_MakeOneAndTerm(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Takes all predicates as arguments of an or together.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  return cnf_MakeOneAndPredicate(cnf_MakeOneAnd(term));
}


LIST cnf_ComputeLiteralLists(TERM Term)
/**********************************************************
  INPUT:   A term in negation normal form without quantifiers.
  RETURNS: The list of all literal lists corresponding to the
           CNF of Term.
***********************************************************/
{
  LIST   Scan, Scan1, Scan2, Help, Result, List1, List2, NewResult;
  SYMBOL Symbol;

  Symbol = term_TopSymbol(Term);
  Result = list_Nil();

  if (symbol_Equal(Symbol,fol_Or())) {
    Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term)));
    for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      Help      = cnf_ComputeLiteralLists(list_Car(Scan));
      NewResult = list_Nil();
      for (Scan1=Help;!list_Empty(Scan1);Scan1=list_Cdr(Scan1))	    
	for (Scan2=Result;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) {
	  List1 = list_Car(Scan1);
	  List2 = list_Car(Scan2);
	  if (!list_Empty(list_Cdr(Scan2)))
	    List1 = term_CopyTermList(List1);
	  if (!list_Empty(list_Cdr(Scan1))) 
	    List2 = term_CopyTermList(List2);
	  NewResult = list_Cons(term_DestroyDuplicatesInList(list_Nconc(List1,List2)),
				NewResult);
	}
      list_Delete(Help);
      list_Delete(Result);
      Result = NewResult;
    }
    return Result;
  }

  if (symbol_Equal(Symbol,fol_And())) {
    Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term)));
    for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      Result = list_Nconc(cnf_ComputeLiteralLists(list_Car(Scan)), Result);
    }
    return Result;
  }
  
  if (symbol_Equal(Symbol,fol_Not()) || symbol_IsPredicate(Symbol))
    return list_List(list_List(term_Copy(Term)));
  
    
  misc_StartErrorReport();
  misc_ErrorReport("\n In cnf_ComputeLiteralLists: Unexpected junctor in input Formula!\n");
  misc_FinishErrorReport();

  return Result;
}


static TERM cnf_DistributiveFormula(TERM Formula)
/**************************************************************
  INPUT:   A Formula in NNF which consists only of disjunctions and
           conjunctions.
  RETURNS: The Formula where the distributivity rule is exhaustively applied
           and all disjunctions and the top level conjunction are grouped.
  CAUTION: The Formula is destructively changed.
***************************************************************/
{
  TERM Result;
  LIST Scan, Lists;

  Lists = cnf_ComputeLiteralLists(Formula);
  
  for (Scan= Lists; !list_Empty(Scan); Scan=list_Cdr(Scan))
    list_Rplaca(Scan,term_Create(fol_Or(), list_Car(Scan)));

  Result = term_Create(fol_And(), Lists);
  term_Delete(Formula);

  return Result;
}



void cnf_FPrintClause(TERM term, FILE* file)
/**************************************************************
  INPUT:   A term and a file pointer.
  RETURNS: Nothing.
  EFFECT:  Print the term which contains only disjunctions to file.
           The disjunctions represent a clause.
***************************************************************/
{
    
  TERM   term1;
  LIST   scan;
  int    bottom;
  
  bottom = vec_ActMax();
  vec_Push(term);       

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (symbol_Equal(term_TopSymbol(term1),fol_Or())) {
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	vec_Push(list_Car(scan));
    }else
      term_FPrint(file,term1);
  }
  fputs(".\n", file);
  vec_SetMax(bottom);
}


void cnf_FPrint(TERM term, FILE* file)
/**************************************************************
  INPUT:   A term and a file pointer.
  RETURNS: Nothing.
  EFFECT:  Print the term (in negation normal form)
           which contains only conjunctions of 
	   disjunctions to file. The conjunctions are interpreted 
	   to represent different clauses.
***************************************************************/
{
  TERM   term1;
  LIST   scan;
  int    bottom;
  
  bottom = vec_ActMax();
  vec_Push(term);       

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (symbol_Equal(term_TopSymbol(term1),fol_And())) {
      for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	vec_Push(list_Car(scan));
    }else
      if (symbol_Equal(term_TopSymbol(term1),fol_Or()) ||
	  symbol_IsPredicate(term_TopSymbol(term1)) ||
	  symbol_Equal(term_TopSymbol(term1),fol_Not()))
	cnf_FPrintClause(term1,file);
  }
  vec_SetMax(bottom);
}


void cnf_StdoutPrint(TERM term)
/**************************************************************
  INPUT:   A term.
  RETURNS: Nothing.
  EFFECT:  Print the term (in negation normal form)
           which contains only conjunctions of 
	   disjunctions to standard out. The conjunctions are interpreted 
	   to represent different clauses.
***************************************************************/
{
  LIST termlist,scan,scan1;

  for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
    termlist = list_Nil();
    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
	  fol_IsNegativeLiteral(list_Car(scan))))
      termlist = term_ArgumentList(list_Car(scan));
    
    if (!list_Empty(termlist)) {
      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1))
	term_Print(list_Car(scan1));
      puts(".");
    }else{
      term_Print(list_Car(scan));
      puts(".");
    }
  }
}


void cnf_FilePrint(TERM term, FILE* file)
/**************************************************************
  INPUT:   A term and a file.
  RETURNS: Nothing.
  EFFECT:  Print the term (in negation normal form)
           which contains only conjunctions of 
	   disjunctions to file. The conjunctions are interpreted 
	   to represent different clauses.
***************************************************************/
{
  LIST termlist,scan,scan1;

  for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
    termlist = list_Nil();
    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
	  fol_IsNegativeLiteral(list_Car(scan))))
      termlist = term_ArgumentList(list_Car(scan));
    
    if (!list_Empty(termlist)) {
      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1))
	term_FPrint(file,list_Car(scan1));
      fputs(".\n", file);
    }else{
      term_FPrint(file,list_Car(scan));
      fputs(".\n", file);
    }
  }
  
}


void cnf_FilePrintPrefix(TERM term, FILE* file)
/**************************************************************
  INPUT:   A term and a file pointer.
  RETURNS: Nothing.
  EFFECT:  Prefix Print the term (in negation normal form)
           which contains only conjunctions of 
	   disjunctions to file. The conjunctions are interpreted 
	   to represent different clauses.
***************************************************************/
{
  LIST termlist,scan,scan1;

  for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan)) {
    termlist = list_Nil();
    if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
	  fol_IsNegativeLiteral(list_Car(scan))))
      termlist = term_ArgumentList(list_Car(scan));
    
    if (!list_Empty(termlist)) {
      for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1)) {
	term_FPrintPrefix(file,list_Car(scan1));
	if (!list_Empty(list_Cdr(scan1)))
	  fputs(" | ", file);
      }
      fputs(".\n", file);
    } else {
      term_FPrintPrefix(file,list_Car(scan));
      fputs(".\n", file);
    }
  }
}


static LIST cnf_SubsumeClauseList(LIST clauselist)
/**********************************************************
  INPUT:   A list of clauses.
  RETURNS: The list of clauses without subsumed clauses.
  CAUTION: The list is destructively changed.
***********************************************************/
{
  LIST     scan,result;
  st_INDEX stindex;
  CLAUSE   actclause;

  stindex = st_IndexCreate();
  result  = list_Nil();

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

  for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
    actclause     = list_Car(scan);
    res_DeleteClauseIndex(actclause,stindex);
    if (!res_BackSubWithLength(actclause,stindex)) {
      res_InsertClauseIndex(actclause,stindex);
      result = list_Cons(actclause,result);
    }
  }
  if (list_Length(result) != list_Length(clauselist)) {
    for (scan = result; !list_Empty(scan); scan=list_Cdr(scan))
      clauselist = list_PointerDeleteElement(clauselist,list_Car(scan));
    if (!list_Empty(result))
      clause_DeleteClauseList(clauselist);
  }else
    list_Delete(clauselist);
  st_IndexDelete(stindex);
  return result;
}


static LIST cnf_MakeClauseList(TERM term, BOOL Sorts, BOOL Conclause,
			       FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A term in cnf and two boolean values indicating
           whether sorts should be generated and whether the
	   generated clauses are Conclauses, a flag store and
	   a precedence.
  RETURNS: A list of clauses with respect to term. The terms 
           in the new clauses are the copied subterms from term.
  EFFECT:  The flag store and the precedence are not changed,
           but they're needed for creating clauses.
***************************************************************/
{
  LIST   termlist,scan,clauselist,newclauselist,delclauselist,condlist;
  CLAUSE clause;
  int    j;

  termlist   = list_Nil();
  clauselist = list_Nil();

  if (fol_IsTrue(term))
    return  clauselist;

  if (fol_IsNegativeLiteral(term) || symbol_IsPredicate(term_TopSymbol(term))) {
    termlist = list_List(term_Copy(term));
    clause = clause_CreateFromLiterals(termlist, Sorts, Conclause,TRUE,
				       Flags, Precedence);
    clauselist = list_Nconc(clauselist,list_List(clause));
    term_StartMinRenaming();
    term_Rename(clause_GetLiteralTerm(clause,0));
    list_Delete(termlist);
    return clauselist;
  }

  delclauselist = list_Nil();
  term          = cnf_MakeOneAndTerm(term);
  if (symbol_Equal(term_TopSymbol(term), fol_And())) {
    for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) {
      list_Rplaca(scan, cnf_MakeOneOrTerm(list_Car(scan)));
      termlist = list_Nil();
      if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) ||
	    fol_IsNegativeLiteral(list_Car(scan)))) {
	termlist = term_CopyTermList(term_ArgumentList(list_Car(scan)));
	termlist = term_DestroyDuplicatesInList(termlist);
      } else
	termlist = list_List(term_Copy(list_Car(scan)));
  
      if (!list_Empty(termlist)) {
	clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE,
					   Flags, Precedence);
	term_StartMinRenaming();
	for (j = 0; j < clause_Length(clause); j++)
	  term_Rename(clause_GetLiteralTerm(clause,j));
	clauselist = list_Cons(clause,clauselist);
	list_Delete(termlist);
      }
    }
  } else {
    /* Here the term is a disjunction, i.e. there is only one clause */
    term = cnf_MakeOneOrTerm(term);
    if (!(symbol_IsPredicate(term_TopSymbol(term)) ||
	  fol_IsNegativeLiteral(term))) {
      termlist = term_CopyTermList(term_ArgumentList(term));
      termlist = term_DestroyDuplicatesInList(termlist);
    } else
      termlist = list_List(term_Copy(term));
    
    if (!list_Empty(termlist)) {
      clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE,
					 Flags, Precedence);
      term_StartMinRenaming();
      for (j = 0; j < clause_Length(clause); j++)
	term_Rename(clause_GetLiteralTerm(clause,j));
      clauselist = list_Cons(clause,clauselist);
      list_Delete(termlist);
    }
  }

  for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
    condlist = cond_CondFast(list_Car(scan));
    if (!list_Empty(condlist))
      clause_DeleteLiterals(list_Car(scan), condlist, Flags, Precedence);
    list_Delete(condlist);
  }
  clauselist    = cnf_SubsumeClauseList(clauselist);
  newclauselist = list_Nil();
  while (!list_Empty(clauselist)) {
    clause = res_SelectLightestClause(clauselist);
    newclauselist = list_Nconc(newclauselist,list_List(clause));
    clauselist = list_PointerDeleteElement(clauselist,clause);
  }
  list_Delete(clauselist);
  for (scan=newclauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
    if (res_HasTautology(list_Car(scan)))
      delclauselist = list_Cons(list_Car(scan),delclauselist);
  }
  for (scan=delclauselist; !list_Empty(scan); scan=list_Cdr(scan))
    newclauselist = list_PointerDeleteElement(newclauselist,list_Car(scan));
  clause_DeleteClauseList(delclauselist);
    
  return newclauselist;
}


TERM cnf_Flatten(TERM Term, SYMBOL Symbol)
/**************************************************************
  INPUT:   A <Term> and <Symbol> that is assumed to be associative.
  RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
           as long as it contains further direct subterms starting with <Symbol>
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   Scan1,Scan2;

  if (symbol_Equal(term_TopSymbol(Term), Symbol)) {
    TERM   Argterm;
    Scan1 =term_ArgumentList(Term);
    while (!list_Empty(Scan1)) {
      Argterm = (TERM)list_Car(Scan1);
      Scan2   = list_Cdr(Scan1);
      if (symbol_Equal(term_TopSymbol(Argterm),Symbol)) {
	cnf_Flatten(Argterm,Symbol);
	list_NInsert(Scan1,list_Cdr(term_ArgumentList(Argterm)));   /* Be efficient ... */
	list_Rplaca(Scan1,list_Car(term_ArgumentList(Argterm)));
	list_Free(term_ArgumentList(Argterm));
	term_Free(Argterm);
      }
      Scan1  = Scan2;
    }
  }
  return Term;
}


static TERM cnf_FlattenPath(TERM Term, TERM PredicateTerm)
/**************************************************************
  INPUT:   A <Term> and <Symbol> that is assumed to be associative,
           and a predicate term which is a subterm of term
  RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
           as long as it contains further direct subterms starting with <Symbol>
  CAUTION: The term is destructively changed.
***************************************************************/
{
  TERM   subterm;
  
  subterm = Term;
  while (symbol_Equal(term_TopSymbol(subterm), fol_All()))
    subterm = term_SecondArgument(subterm);

  if (symbol_Equal(term_TopSymbol(subterm), fol_Or())) {
    TERM Argterm;
    LIST scan1;
    scan1 = term_ArgumentList(subterm);
    while (!list_Empty(scan1)) {
      LIST scan2;
      Argterm = (TERM)list_Car(scan1);
      scan2   = list_Cdr(scan1);
      if (term_HasProperSuperterm(PredicateTerm, Argterm)) {
	if (symbol_Equal(term_TopSymbol(Argterm),fol_Or())) {
	  LIST l;
	  cnf_Flatten(Argterm,fol_Or());
	  for (l=term_ArgumentList(Argterm); !list_Empty(l); l=list_Cdr(l))
	    term_RplacSuperterm((TERM) list_Car(l), subterm);
	  list_NInsert(scan1,list_Cdr(term_ArgumentList(Argterm)));   /* Be efficient ... */
	  list_Rplaca(scan1,list_Car(term_ArgumentList(Argterm)));
	  list_Free(term_ArgumentList(Argterm));
	  term_Free(Argterm);
	}
      }
      scan1  = scan2;
    }
  }
  return Term;
}


static void cnf_DistrQuantorNoVarSub(TERM Term)
/**************************************************************
  INPUT:   A formula in negation normal form starting with a universal 
           (existential) quantifier and a disjunction (conjunction) as argument.
  EFFECT:  The Quantor is distributed if possible.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   Variables,Subformulas,Scan1,Scan2,Rest;
  TERM   Subterm,Var,NewForm;
  SYMBOL Subtop,Top;

  Top       = term_TopSymbol(Term);
  Variables = list_Copy(fol_QuantifierVariables(Term));
  Subterm   = term_SecondArgument(Term);
  Subtop    = term_TopSymbol(Subterm);
  Subterm   = cnf_Flatten(Subterm,Subtop);

  for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
    Subformulas = list_Nil();
    Var         = (TERM)list_Car(Scan1);
    for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
      if (!fol_VarOccursFreely(Var,list_Car(Scan2)))
	Subformulas = list_Cons(list_Car(Scan2),Subformulas);
    if (!list_Empty(Subformulas)) {
      Rest     = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas);
      if (list_Empty(list_Cdr(Rest))) { /* One subformula */
	if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */
	  NewForm = (TERM)list_Car(Rest);
	  term_RplacArgumentList(term_FirstArgument(NewForm),
				 list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm)));
	  list_Delete(Rest);
	}
	else
	  NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),Rest);
      }
      else
	NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),list_List(term_Create(Subtop,Rest)));
      term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas));
      term_RplacArgumentList(term_FirstArgument(Term),
			     list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var));
    } 
  }

  if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */
    term_Free(term_FirstArgument(Term));
    list_Delete(term_ArgumentList(Term));
    term_RplacTop(Term,Subtop);
    term_RplacArgumentList(Term,term_ArgumentList(Subterm));
    term_Free(Subterm);
  }
  list_Delete(Variables);
}


static TERM cnf_AntiPrenex(TERM Term)
/**************************************************************
  INPUT:   A formula in negation normal form.
  RETURNS: The term after application of anti-prenexing. Quantifiers
           are moved inside as long as possible.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   Scan;
  SYMBOL Top;

  Top = term_TopSymbol(Term);

  if (fol_IsQuantifier(Top)) {
    TERM   Subterm,Actterm;
    SYMBOL DistrSymb,Subtop;          /* The junctor the respective quantifier distributes over */
    
    Subterm = term_SecondArgument(Term);
    Subtop  = term_TopSymbol(Subterm);

    if (!symbol_IsPredicate(Subtop) && 
	!symbol_Equal(Subtop,fol_Not())) { /* Formula in NNF: No Literals or Atoms */
      if (symbol_Equal(Top,fol_All()))
	DistrSymb = fol_And();
      else
	DistrSymb = fol_Or();
      if (fol_IsQuantifier(Subtop)) {
	cnf_AntiPrenex(Subterm);
	Subtop = term_TopSymbol(Subterm);
      }
      if (symbol_Equal(Subtop,DistrSymb)) {
	LIST Variables;	
	LIST NewVars;
	Variables = fol_QuantifierVariables(Term);
	Subterm   = cnf_Flatten(Subterm,DistrSymb);
	for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
	  Actterm = (TERM)list_Car(Scan);
	  NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables,
				    (BOOL (*)(POINTER,POINTER))term_Equal);
	  if (!list_Empty(NewVars)) {
	    if (symbol_Equal(Top,term_TopSymbol(Actterm))) {        /* Quantor already there */
	      term_CopyTermsInList(NewVars);
	      term_RplacArgumentList(term_FirstArgument(Actterm),
				     list_Nconc(fol_QuantifierVariables(Actterm),
						NewVars));
	    }
	    else {
	      term_CopyTermsInList(NewVars);
	      list_Rplaca(Scan,fol_CreateQuantifier(Top, NewVars, list_List(Actterm)));
	    }
	  }
	}
	term_Delete(term_FirstArgument(Term));   /* Delete old variable list */
	list_Delete(term_ArgumentList(Term)); 
	term_RplacTop(Term,DistrSymb);
	term_RplacArgumentList(Term,term_ArgumentList(Subterm));
	term_Free(Subterm);
	for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) 
	  list_Rplaca(Scan,cnf_AntiPrenex(list_Car(Scan)));
      }
      else 
	if (!fol_IsQuantifier(Subtop)) {
	  cnf_DistrQuantorNoVarSub(Term);
	  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
	    cnf_AntiPrenex(list_Car(Scan));
	}
    }
  }
  else
    if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top))
      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
	cnf_AntiPrenex(list_Car(Scan));

  return Term;
}


static void cnf_DistrQuantorNoVarSubPath(TERM Term, TERM PredicateTerm)
/**************************************************************
  INPUT:   A formula in negation normal form starting with a universal 
           (existential) quantifier and a disjunction (conjunction) as argument
	   and a predicate term which is a subterm of term.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   Variables,Subformulas,Scan1,Scan2,Rest;
  TERM   Subterm,Var,NewForm;
  SYMBOL Subtop,Top;

  /*fputs("\nAN0:\t",stdout);term_Print(Term);*/

  Top       = term_TopSymbol(Term);
  Variables = list_Copy(fol_QuantifierVariables(Term));
  Subterm   = term_SecondArgument(Term);
  Subtop    = term_TopSymbol(Subterm);
  Subterm   = cnf_Flatten(Subterm,Subtop);

  /*fputs("\nAN1:\t",stdout);term_Print(Subterm);*/

  for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
    Subformulas = list_Nil();
    Var         = (TERM)list_Car(Scan1);
    /* Find subterms in which the variable does not occur freely */
    for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
      if (!fol_VarOccursFreely(Var,list_Car(Scan2)))
	Subformulas = list_Cons(list_Car(Scan2),Subformulas);
    if (!list_Empty(Subformulas)) {
      /* Rest is the list of those subterms where the variable does occur freely */
      Rest     = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas);
      if (list_Empty(list_Cdr(Rest))) { /* One subformula */
	if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */
	  NewForm = (TERM)list_Car(Rest);
	  /* Move one variable down */
	  term_RplacArgumentList(term_FirstArgument(NewForm),
				 list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm)));
	  list_Delete(Rest);
	}
	else {
	  NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var),
						  Rest);
	}
      }
      else {
	TERM t;
	t = term_CreateAddFather(Subtop,Rest);
	NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var),list_List(t));
      }
      if (term_HasProperSuperterm(PredicateTerm, NewForm))
	NewForm = cnf_AntiPrenexPath(NewForm, PredicateTerm);
      term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas));
      term_RplacSuperterm(NewForm, Subterm);
      term_RplacArgumentList(term_FirstArgument(Term),
			     list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var));
    } 
  }

  if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */
    LIST l;
    term_Free(term_FirstArgument(Term));
    list_Delete(term_ArgumentList(Term));
    term_RplacTop(Term,Subtop);
    term_RplacArgumentList(Term,term_ArgumentList(Subterm));
    term_Free(Subterm);
    for (l=term_ArgumentList(Term); !list_Empty(l); l=list_Cdr(l))
      term_RplacSuperterm((TERM) list_Car(l), Term);
  }
  list_Delete(Variables);
}


static TERM cnf_AntiPrenexPath(TERM Term, TERM PredicateTerm)
/**************************************************************
  INPUT:   A formula in negation normal form and a predicate term
           which is a subterm of term.
  RETURNS: The term after application of anti-prenexing. Quantifiers
           are moved inside along the path as long as possible.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  LIST   Scan;
  SYMBOL Top;

  Top = term_TopSymbol(Term);

  if (fol_IsQuantifier(Top)) {
    TERM   Subterm,Actterm;
    SYMBOL DistrSymb,Subtop;          /* The junctor the respective quantifier distributes over */
    
    Subterm = term_SecondArgument(Term);
    Subtop  = term_TopSymbol(Subterm);

    if (!symbol_Equal(Subtop,fol_Not()) && !symbol_IsPredicate(Subtop)) { /* No Literals or Atoms */
      if (symbol_Equal(Top,fol_All()))
	DistrSymb = fol_And();
      else
	DistrSymb = fol_Or();
      if (fol_IsQuantifier(Subtop)) {
	cnf_AntiPrenexPath(Subterm, PredicateTerm);
	Subtop = term_TopSymbol(Subterm);
      }
      if (symbol_Equal(Subtop,DistrSymb)) {
	LIST Variables;	
	LIST NewVars;
	Variables = fol_QuantifierVariables(Term);
	Subterm   = cnf_Flatten(Subterm,DistrSymb);
	term_AddFatherLinks(Subterm);
	/*
	  for (l=term_ArgumentList(Subterm); !list_Empty(l); l=list_Cdr(l))
	  term_RplacSuperterm((TERM) list_Car(l), Subterm);
	*/
	for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
	  Actterm = (TERM)list_Car(Scan);
	  NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables,
				    (BOOL (*)(POINTER,POINTER))term_Equal);
	  if (!list_Empty(NewVars)) {
	    if (symbol_Equal(Top,term_TopSymbol(Actterm))) {         /* Quantor already there */
	      term_CopyTermsInList(NewVars);
	      term_RplacArgumentList(term_FirstArgument(Actterm),
				     list_Nconc(fol_QuantifierVariables(Actterm), NewVars));
	    }
	    else {
	      term_CopyTermsInList(NewVars);
	      list_Rplaca(Scan,fol_CreateQuantifierAddFather(Top, NewVars, list_List(Actterm)));
	    }
	  }
	}
	term_Delete(term_FirstArgument(Term));   /* Delete old variable list */
	list_Delete(term_ArgumentList(Term)); 
	term_RplacTop(Term,DistrSymb);
	term_RplacArgumentList(Term,term_ArgumentList(Subterm));
	term_Free(Subterm);
	term_AddFatherLinks(Term);
	for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
	  term_RplacSuperterm((TERM) list_Car(Scan), Term);
	  if (term_HasPointerSubterm((TERM) list_Car(Scan), PredicateTerm)) {
	    puts("\ncheck1");
	    list_Rplaca(Scan,cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm));
	    term_RplacSuperterm((TERM) list_Car(Scan), Term);
	  }
	}
      }
      else
	if (!fol_IsQuantifier(Subtop)) {
	  cnf_DistrQuantorNoVarSubPath(Term, PredicateTerm);
	  for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
	    if (term_HasPointerSubterm(list_Car(Scan), PredicateTerm))
	      cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm);
	  }
	}
    }
  }
  else
    if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top))
      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
	if (term_HasProperSuperterm(PredicateTerm, (TERM) list_Car(Scan)))
	  cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm);
  
  term_AddFatherLinks(Term);
  return Term;
}


static TERM cnf_RemoveTrivialOperators(TERM Term)
/**************************************************************
  INPUT:   A formula.
  RETURNS: The formula after
           removal of "or" and "and" with only one argument
  CAUTION: The term is destructively changed.
***************************************************************/
{
  SYMBOL Top;
  LIST   Scan;

  Top = term_TopSymbol(Term);

  if (symbol_IsPredicate(Top))
    return Term;

  if ((symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or())) &&
      list_Empty(list_Cdr(term_ArgumentList(Term)))) {
    TERM Result;
    Result = term_FirstArgument(Term);
    term_RplacSuperterm(Result, term_Superterm(Term));
    list_Delete(term_ArgumentList(Term));
    term_Free(Term);
    return cnf_RemoveTrivialOperators(Result);
  }

  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
    list_Rplaca(Scan,cnf_RemoveTrivialOperators(list_Car(Scan)));
    term_RplacSuperterm((TERM) list_Car(Scan), Term);
  }
  
  return Term;
}


static TERM cnf_SimplifyQuantors(TERM Term)
  /**************************************************************
  INPUT:   A formula.
  RETURNS: The formula after
	   removal of bindings of variables that don't occur in the
	   respective subformula and possible mergings of quantors
  CAUTION: The term is destructively changed.
***************************************************************/
{
  SYMBOL Top;
  LIST   Scan;

  Top = term_TopSymbol(Term);

  if (symbol_IsPredicate(Top) || symbol_Equal(Top,fol_Varlist()))
    return Term;

  if (fol_IsQuantifier(Top)) {
    LIST Vars;
    TERM Var,Subterm,Aux;
    Vars    = list_Nil();
    Subterm = term_SecondArgument(Term);

    while (symbol_Equal(term_TopSymbol(Subterm),Top)) {
      term_RplacArgumentList(term_FirstArgument(Term),
			     list_Nconc(fol_QuantifierVariables(Term),fol_QuantifierVariables(Subterm)));
      term_Free(term_FirstArgument(Subterm));
      Aux = term_SecondArgument(Subterm);
      list_Delete(term_ArgumentList(Subterm));
      term_Free(Subterm);
      list_Rplaca(list_Cdr(term_ArgumentList(Term)),Aux);
      Subterm = Aux;
    }
    
    for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      Var = (TERM)list_Car(Scan);
      if (!fol_VarOccursFreely(Var,Subterm))
	Vars = list_Cons(Var,Vars);
    }
    if (!list_Empty(Vars)) {
      Subterm = term_FirstArgument(Term);
      term_RplacArgumentList(Subterm,list_NPointerDifference(term_ArgumentList(Subterm),Vars));
      term_DeleteTermList(Vars);
      if (list_Empty(term_ArgumentList(Subterm))) {
	Subterm = term_SecondArgument(Term);
	term_Delete(term_FirstArgument(Term));
	list_Delete(term_ArgumentList(Term));
	term_Free(Term);
	return cnf_SimplifyQuantors(Subterm);
      }
    }
  }
  
  for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
    list_Rplaca(Scan,cnf_SimplifyQuantors(list_Car(Scan)));
  
  return Term; 
}


TERM cnf_RemoveTrivialAtoms(TERM Term)
/**************************************************************
  INPUT:   A formula.
  RETURNS: The formula where occurrences of the atoms "true"
           and "false" are propagated and eventually removed.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  SYMBOL Top,Subtop;
  LIST   Scan;
  TERM   Result;
  BOOL   Update;


  if (!term_IsComplex(Term))
    return Term;
  
  Top    = term_TopSymbol(Term);
  Update = FALSE;

  if (symbol_Equal(Top,fol_And())) {
    Scan  = term_ArgumentList(Term);
    while (!list_Empty(Scan)) {
      Result = cnf_RemoveTrivialAtoms(list_Car(Scan));
      Subtop = term_TopSymbol(Result);
      if (symbol_Equal(Subtop,fol_True()))
	Update = TRUE;
      else
	if (symbol_Equal(Subtop,fol_False())) {
	  term_RplacTop(Term,fol_False());
	  term_DeleteTermList(term_ArgumentList(Term));
	  term_RplacArgumentList(Term,list_Nil());
	  return Term;
	}
      Scan = list_Cdr(Scan);
    }
    if (Update) {
      term_RplacArgumentList(Term,fol_DeleteTrueTermFromList(term_ArgumentList(Term)));
      if (list_Empty(term_ArgumentList(Term))) {
	term_RplacTop(Term,fol_True());
	return Term;
      }
    }
  }
  else if (symbol_Equal(Top,fol_Or())) {
    Scan  = term_ArgumentList(Term);
    while (!list_Empty(Scan)) {
      Result = cnf_RemoveTrivialAtoms(list_Car(Scan));
      Subtop = term_TopSymbol(Result);
      if (symbol_Equal(Subtop,fol_False()))
	Update = TRUE;
      else
	if (symbol_Equal(Subtop,fol_True())) {
	  term_RplacTop(Term,fol_True());
	  term_DeleteTermList(term_ArgumentList(Term));
	  term_RplacArgumentList(Term,list_Nil());
	  return Term;
	}
      Scan = list_Cdr(Scan);
    }
    if (Update) {
      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
      if (list_Empty(term_ArgumentList(Term))) {
	term_RplacTop(Term,fol_False());
	return Term;
      }
    }
  }
  else if (fol_IsQuantifier(Top) || symbol_Equal(Top,fol_Not())) {
    if (fol_IsQuantifier(Top))
      Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
    else
      Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
    Subtop = term_TopSymbol(Result);
    if ((symbol_Equal(Subtop,fol_False()) && symbol_Equal(Top,fol_Not())) ||
	(symbol_Equal(Subtop,fol_True()) && fol_IsQuantifier(Top))) {
      term_RplacTop(Term,fol_True());
      term_DeleteTermList(term_ArgumentList(Term));
      term_RplacArgumentList(Term,list_Nil());
      return Term;
    }
    else
      if ((symbol_Equal(Subtop,fol_True()) && symbol_Equal(Top,fol_Not())) ||
	  (symbol_Equal(Subtop,fol_False()) && fol_IsQuantifier(Top))) {
	term_RplacTop(Term,fol_False());
	term_DeleteTermList(term_ArgumentList(Term));
	term_RplacArgumentList(Term,list_Nil());
	return Term;
      }
  }
  else if (symbol_Equal(Top,fol_Implies())) {
    Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
    Subtop = term_TopSymbol(Result);
    if (symbol_Equal(Subtop,fol_False())) {
      term_RplacTop(Term,fol_True());
      term_DeleteTermList(term_ArgumentList(Term));
      term_RplacArgumentList(Term,list_Nil());
      return Term;
    }
    else if (symbol_Equal(Subtop,fol_True())) {
      term_Delete(Result);
      Result = term_SecondArgument(Term);
      list_Delete(term_ArgumentList(Term));
      term_RplacTop(Term,term_TopSymbol(Result));
      term_RplacArgumentList(Term,term_ArgumentList(Result));
      term_Free(Result);
      return cnf_RemoveTrivialAtoms(Term);
    }
    Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
    Subtop = term_TopSymbol(Result);
    if (symbol_Equal(Subtop,fol_True())) {
      term_RplacTop(Term,fol_True());
      term_DeleteTermList(term_ArgumentList(Term));
      term_RplacArgumentList(Term,list_Nil());
      return Term;
    }
    else if (symbol_Equal(Subtop,fol_False())) {
      term_RplacTop(Term,fol_Not());
      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
    }
  }
  else if (symbol_Equal(Top,fol_Equiv())) {
    Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term));
    Subtop = term_TopSymbol(Result);
    if (symbol_Equal(Subtop,fol_False())) {
      term_RplacTop(Term,fol_Not());
      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
      if (list_Empty(term_ArgumentList(Term))) {
	term_RplacTop(Term, fol_True());
	return Term;
      }
      return cnf_RemoveTrivialAtoms(Term);
    }
    else if (symbol_Equal(Subtop,fol_True())) {
      term_Delete(Result);
      Result = term_SecondArgument(Term);
      list_Delete(term_ArgumentList(Term));
      term_RplacTop(Term,term_TopSymbol(Result));
      term_RplacArgumentList(Term,term_ArgumentList(Result));
      term_Free(Result);
      return cnf_RemoveTrivialAtoms(Term);
    }
    Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term));
    Subtop = term_TopSymbol(Result);
    if (symbol_Equal(Subtop,fol_False())) {
      term_RplacTop(Term,fol_Not());
      term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term)));
    }
    else if (symbol_Equal(Subtop,fol_True())) {
      term_Delete(Result);
      Result = term_FirstArgument(Term);
      list_Delete(term_ArgumentList(Term));
      term_RplacTop(Term,term_TopSymbol(Result));
      term_RplacArgumentList(Term,term_ArgumentList(Result));
      term_Free(Result);
    }
  }

  return Term;
}


TERM cnf_ObviousSimplifications(TERM Term)
/**************************************************************
  INPUT:   A formula.
  RETURNS: The formula after performing the following simplifications:
             - remove "or" and "and" with only one argument
	     - remove bindings of variables that don't occur in the
	       respective subformula
	     - merge quantors
  CAUTION: The term is destructively changed.
***************************************************************/
{
  Term = cnf_RemoveTrivialAtoms(Term);
  Term = cnf_RemoveTrivialOperators(Term);
  Term = cnf_SimplifyQuantors(Term);

  return Term;
}


/* EK: warum wird Term zurueckgegeben, wenn er destruktiv geaendert wird??? */
static TERM cnf_SkolemFormula(TERM Term, PRECEDENCE Precedence, LIST* Symblist)
/**************************************************************
  INPUT:   A formula in negation normal form, a precedence and pointer
           to a list used as return value.
  RETURNS: The skolemized term and the list of introduced Skolem functions.
  CAUTION: The term is destructively changed.
           The precedence of the new Skolem functions is set in <Precedence>.
***************************************************************/
{
  SYMBOL Top,SkolemSymbol;
  TERM   Subterm,SkolemTerm;
  LIST   Varlist,Scan;
  NAT    Arity;

  Top = term_TopSymbol(Term);
    
  if (fol_IsQuantifier(term_TopSymbol(Term))) {
    if (symbol_Equal(Top,fol_All())) {
      term_Delete(term_FirstArgument(Term));
      Subterm = term_SecondArgument(Term);
      list_Delete(term_ArgumentList(Term));
      term_RplacTop(Term,term_TopSymbol(Subterm));
      term_RplacArgumentList(Term,term_ArgumentList(Subterm));
      term_Free(Subterm);
      return cnf_SkolemFormula(Term, Precedence, Symblist);
    } 
    else {  /* exist quantifier */
      Varlist = fol_FreeVariables(Term);
      Arity   = list_Length(Varlist);
      for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
	SkolemSymbol = symbol_CreateSkolemFunction(Arity, Precedence);
	*Symblist  = list_Cons((POINTER)SkolemSymbol, *Symblist);
	SkolemTerm = term_Create(SkolemSymbol,Varlist); /* Caution: Sharing of Varlist ! */
	fol_ReplaceVariable(term_SecondArgument(Term),term_TopSymbol(list_Car(Scan)),SkolemTerm);
	term_Free(SkolemTerm);
      }
      list_Delete(Varlist);
      term_Delete(term_FirstArgument(Term));
      Subterm = term_SecondArgument(Term);
      list_Delete(term_ArgumentList(Term));
      term_RplacTop(Term,term_TopSymbol(Subterm));
      term_RplacArgumentList(Term,term_ArgumentList(Subterm));
      term_Free(Subterm);
      return cnf_SkolemFormula(Term, Precedence, Symblist);
    } 
  }
  else
    if (symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or()))
      for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))
	cnf_SkolemFormula(list_Car(Scan), Precedence, Symblist);
  return Term;
}


static TERM cnf_Cnf(TERM Term, PRECEDENCE Precedence, LIST* Symblist)
/**************************************************************
  INPUT:   A formula, a precedence and a pointer to a list of symbols
           used as return value.
  RETURNS: The term is transformed to conjunctive normal form.
  EFFECT:  The term is destructively changed and not normalized.
           The precedence of new Skolem symbols is set in <Precedence>.
***************************************************************/
{
  /* Necessary because ren_Rename crashes if a e.g. and() has only one argument */
  Term = cnf_ObviousSimplifications(Term);
  term_AddFatherLinks(Term);
  Term = ren_Rename(Term, Precedence, Symblist, FALSE, FALSE);
  Term = cnf_RemoveEquivImplFromFormula(Term);
  Term = cnf_NegationNormalFormula(Term);
  Term = cnf_SkolemFormula(cnf_AntiPrenex(Term), Precedence, Symblist);
  Term = cnf_DistributiveFormula(Term);

  return Term;
}


static LIST cnf_GetUsedTerms(CLAUSE C, PROOFSEARCH Search,
			     HASH InputClauseToTermLabellist) 
/**************************************************************
  INPUT:   
  RETURNS: 
***************************************************************/
{
  LIST UsedTerms, Used2, Scan;
  UsedTerms = list_Copy(hsh_Get(InputClauseToTermLabellist, C));
  UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms);
  if (!list_Empty(UsedTerms))
    return UsedTerms;

  for (Scan = clause_ParentClauses(C); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    CLAUSE P;
    int ClauseNumber;
    ClauseNumber = (int) list_Car(Scan);
    P = clause_GetNumberedCl(ClauseNumber, prfs_WorkedOffClauses(Search));
    if (P == NULL) {
      P = clause_GetNumberedCl(ClauseNumber, prfs_UsableClauses(Search));
      if (P == NULL)
	P = clause_GetNumberedCl(ClauseNumber, prfs_DocProofClauses(Search));
    }
    Used2 = cnf_GetUsedTerms(P, Search, InputClauseToTermLabellist);
    UsedTerms = list_Nconc(UsedTerms, Used2);
  }
  return UsedTerms;
}


static BOOL cnf_HaveProofOptSkolem(PROOFSEARCH Search, TERM topterm,
				   char* toplabel, TERM term2,
				   LIST* UsedTerms, LIST* Symblist,
				   HASH InputClauseToTermLabellist)
/**************************************************************
  INPUT:   
  RETURNS: ??? EK
***************************************************************/
{
  LIST       ConClauses, EmptyClauses;
  LIST       scan;
  BOOL       found;
  LIST       Usables;
  FLAGSTORE  Flags;
  PRECEDENCE Precedence;

  Flags      = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);
  ConClauses = list_Nil();
  found      = FALSE;
  /* List of clauses from term2 */
  term_AddFatherLinks(term2);
  term2      = cnf_Cnf(term2, Precedence, Symblist);
  Usables    = cnf_MakeClauseList(term2, FALSE, FALSE, Flags, Precedence);
  term_Delete(term2);

  for (scan=Usables; !list_Empty(scan); scan = list_Cdr(scan)) {
    clause_SetFlag(list_Car(scan), CONCLAUSE);
    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
#ifdef CHECK
      hsh_Check(InputClauseToTermLabellist);
#endif
      hsh_Put(InputClauseToTermLabellist, list_Car(scan), toplabel);
#ifdef CHECK_CNF
      fputs("\nUsable : ", stdout);
      clause_Print(list_Car(scan));
      printf(" Label %s", toplabel);
#endif
    }
  }
  EmptyClauses = cnf_SatUnit(Search, Usables);
  if (!list_Empty(EmptyClauses)) {
    found = TRUE;
#ifdef CHECK_CNF
    fputs("\nHaveProof : Empty Clause : ", stdout);
    clause_Print((CLAUSE) list_Car(EmptyClauses));
    putchar('\n');
#endif
    if (flag_GetFlagValue(Flags, flag_DOCPROOF))
      *UsedTerms = list_Nconc(*UsedTerms, cnf_GetUsedTerms((CLAUSE) list_Car(EmptyClauses), Search, InputClauseToTermLabellist));
    EmptyClauses = list_PointerDeleteDuplicates(EmptyClauses);
    clause_DeleteClauseList(EmptyClauses);
  }
    
  /* Removing ConClauses from UsablesIndex */
  ConClauses = list_Copy(prfs_UsableClauses(Search));
  for (scan = ConClauses; !list_Empty(scan); scan = list_Cdr(scan))
    if (flag_GetFlagValue(Flags, flag_DOCPROOF))
      prfs_MoveUsableDocProof(Search, (CLAUSE) list_Car(scan));
    else
      prfs_DeleteUsable(Search, (CLAUSE) list_Car(scan));
  list_Delete(ConClauses); 
	
  return found;
}


BOOL cnf_HaveProof(LIST TermList, TERM ToProve, FLAGSTORE InputFlags,
		   PRECEDENCE InputPrecedence)
/**************************************************************
  INPUT:   A list of terms, a term to prove, a flag store and a precedence.
           The arguments are not changed.
  RETURNS: True if the termlist implies ToProve
  CAUTION: All terms are copied.
***************************************************************/
{
  PROOFSEARCH search;
  LIST        scan, usables, symblist, emptyclauses;
  BOOL        found;
  FLAGSTORE   Flags;
  PRECEDENCE  Precedence;

  /* Use global PROOFSEARCH object to avoid stamp overflow */
  search  = cnf_HAVEPROOFPS;
  usables = symblist = list_Nil();

  /* Initialize search object's flag store */
  Flags = prfs_Store(search);
  flag_CleanStore(Flags);
  flag_InitFlotterSubproofFlags(InputFlags, Flags);
  /* Initialize search object's precedence */
  Precedence = prfs_Precedence(search);
  symbol_TransferPrecedence(InputPrecedence, Precedence);

  /* Build list of clauses from the termlist */
  for (scan=TermList; !list_Empty(scan); scan=list_Cdr(scan)) {
    TERM t;
    t = term_Copy(list_Car(scan));
    t = cnf_Cnf(t, Precedence, &symblist);

    usables = list_Nconc(cnf_MakeClauseList(t,FALSE,FALSE,Flags,Precedence),
			 usables);
    term_Delete(t); 
  }

  /* Build clauses from negated term to prove */
  ToProve = term_Create(fol_Not(), list_List(term_Copy(ToProve)));
  term_AddFatherLinks(ToProve);
  ToProve = cnf_Cnf(ToProve, Precedence, &symblist);
  usables = list_Nconc(cnf_MakeClauseList(ToProve,FALSE,FALSE,Flags,Precedence),
		       usables);
  term_Delete(ToProve);

  /* SatUnit requires the CONCLAUSE flag */
  for (scan=usables;!list_Empty(scan); scan = list_Cdr(scan))
    clause_SetFlag(list_Car(scan), CONCLAUSE);

  emptyclauses = cnf_SatUnit(search, usables);
  
  if (!list_Empty(emptyclauses)) {
    found = TRUE;
    emptyclauses = list_PointerDeleteDuplicates(emptyclauses);
    clause_DeleteClauseList(emptyclauses);
  }
  else
    found = FALSE;
  prfs_Clean(search);
  symbol_DeleteSymbolList(symblist);

  return found;
}


static void cnf_RplacVarsymbFunction(TERM term, SYMBOL varsymb, TERM function)
/**********************************************************
  INPUT:   A term, a variable symbol and a function.
  EFFECT:  The variable with the symbol  varsymb in the term 
           is replaced by the function function.
  CAUTION: The term is destructively changed.
***********************************************************/
{
  int  bottom;
  TERM term1;
  LIST scan;

  bottom = vec_ActMax();
  vec_Push(term);

  while (bottom != vec_ActMax()) {
    term1 = (TERM)vec_PopResult();
    if (symbol_Equal(term_TopSymbol(term1),varsymb)) {
      term_RplacTop(term1,term_TopSymbol(function));
      term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(function)));
    }else
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	  vec_Push(list_Car(scan));
  }
  vec_SetMax(bottom);
}


static void cnf_RplacVar(TERM Term, LIST Varlist, LIST Termlist)
/**********************************************************
  INPUT:   A term,a variable symbol and a function.
  RETURNS: The variable with the symbol  varsymb in the term 
           is replaced by the function function.
  CAUTION: The term is destructively changed.
***********************************************************/
{
  int  bottom;
  TERM term1;
  LIST scan,scan2;

  bottom = vec_ActMax();
  vec_Push(Term);

  while (bottom != vec_ActMax()) {
    term1 = vec_PopResult();
    if (symbol_IsVariable(term_TopSymbol(term1))) {
      BOOL done;
      done = FALSE;
      for (scan=Varlist, scan2=Termlist; !list_Empty(scan) && !done; 
	   scan = list_Cdr(scan), scan2 = list_Cdr(scan2)) {
	if (symbol_Equal(term_TopSymbol(term1),term_TopSymbol(list_Car(scan)))) {
	  term_RplacTop(term1,term_TopSymbol((TERM) list_Car(scan2)));
	  term_RplacArgumentList(term1,
				 term_CopyTermList(term_ArgumentList(list_Car(scan2))));
	  done = TRUE;
	}
      }
    }
    else
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	  vec_Push(list_Car(scan));
  }
  vec_SetMax(bottom);
}


static TERM cnf_MakeSkolemFunction(LIST varlist, PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A list of variables and a precedence.
  RETURNS: The new term oskf... (oskc...) which is a function 
           with varlist as arguments.
  EFFECT:  The precedence of the new Skolem function is set in <Precedence>.
***************************************************************/
{
  TERM   term;
  SYMBOL skolem;
  
  skolem = symbol_CreateSkolemFunction(list_Length(varlist), Precedence);
  term   = term_Create(skolem, term_CopyTermList(varlist));
  return term;
}


static void cnf_PopAllQuantifier(TERM term)
/********************************************************
 INPUT:   A term whose top symbol is fol_all.
 RETURNS: Nothing.
 EFFECT:  Removes the quantifier
********************************************************/
{
  TERM SubTerm;
  LIST VarList;

#ifdef CHECK
  if (!symbol_Equal(term_TopSymbol(term), fol_All())) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_PopAllQuantifier: Top symbol is not fol_All !\n");
    misc_FinishErrorReport();
  }
#endif

  VarList = term_ArgumentList(term_FirstArgument(term));
  term_DeleteTermList(VarList);
  term_Free(term_FirstArgument(term));
  SubTerm = term_SecondArgument(term);
  list_Delete(term_ArgumentList(term));
  term_RplacTop(term,term_TopSymbol(SubTerm));
  term_RplacArgumentList(term,term_ArgumentList(SubTerm));
  term_Free(SubTerm);
}


static TERM cnf_QuantifyAndNegate(TERM term, LIST VarList, LIST FreeList)
/****************************************************************
  INPUT:   A term, a list of variables to be exist-quantified,
           a list of variables to be all-quantified
  RETURNS: not(forall[FreeList](exists[VarList](term)))
  MEMORY:  The term, the lists and their arguments are copied.
***************************************************************/
{
  TERM Result;
  TERM TermCopy;
  LIST VarListCopy;
  LIST FreeListCopy;

  TermCopy = term_Copy(term);
  VarListCopy = term_CopyTermList(VarList);
  Result = fol_CreateQuantifier(fol_Exist(),VarListCopy,list_List(TermCopy));
  FreeListCopy = list_Nil();

  FreeList = fol_FreeVariables(Result);
  if (!list_Empty(FreeList)) {
    FreeListCopy = term_CopyTermList(FreeList);
    list_Delete(FreeList);
    Result = fol_CreateQuantifier(fol_All(), FreeListCopy, list_List(Result));
  }
  Result = term_Create(fol_Not(), list_List(Result));
  return Result;
}


static TERM cnf_MoveProvedTermToTopLevel(TERM Term, TERM Term1, TERM Proved,
					 LIST VarList, LIST FreeList,
					 PRECEDENCE Precedence)
/********************************************************************
  INPUT:   A top-level term, which must be a conjunction,
           a subterm <Term1> of <Term>, a subterm <Proved> of <Term1>,
	   a list of existence quantified variables <VarList>,
	   a list of free variables <FreeList> and a precedence.
           <Term1> is of the form
	   exists[...](t1 and t2 and ... and Proved and ..)
  RETURNS: A new term, where <Proved> is removed from the arguments
           of <Term1>.
  EFFECT:  The precedence of new Skolem functions is set in <Precedence>
*******************************************************************/
{
  TERM termR;
  TERM skolemfunction;
  SYMBOL varsymb;
  LIST scan;

  termR = term_SecondArgument(Term1); /* t1 and t2 and ... and Proved ... */
  term_RplacArgumentList(termR,
			 list_PointerDeleteElement(term_ArgumentList(termR),
						   Proved));
  if (list_Length(term_ArgumentList(termR)) < 2) {
    TERM termRL = term_FirstArgument(termR);     /* t1 */
    list_Delete(term_ArgumentList(termR));
    term_RplacTop(termR, term_TopSymbol(termRL));
    term_RplacArgumentList(termR,term_ArgumentList(termRL));
    term_Free(termRL);
  }

  for (scan = VarList; scan != list_Nil(); scan = list_Cdr(scan)) {
    varsymb = term_TopSymbol(list_Car(scan));
    skolemfunction = cnf_MakeSkolemFunction(FreeList, Precedence);
    cnf_RplacVarsymbFunction(termR,varsymb,skolemfunction);
    cnf_RplacVarsymbFunction(Proved,varsymb,skolemfunction); 
    term_Delete(skolemfunction); 
  }

  if (!list_Empty(FreeList)) {
    Proved = 
      fol_CreateQuantifier(fol_All(), term_CopyTermList(FreeList),
			   list_List(Proved));
    if (list_Length(FreeList) > 1)
      Proved = cnf_QuantMakeOneVar(Proved);
  }
 
  term_Delete(term_FirstArgument(Term1)); /* Variables of "exists" */
  list_Delete(term_ArgumentList(Term1));
  term_RplacTop(Term1,term_TopSymbol(termR));
  term_RplacArgumentList(Term1,term_ArgumentList(termR));
  term_Free(termR);
    
  term_RplacArgumentList(Term, list_Cons(Proved, term_ArgumentList(Term)));
  return Proved;
}


static void cnf_Skolemize(TERM Term, LIST FreeList, PRECEDENCE Precedence)
/********************************************************
  INPUT:   A existence quantified term, the list of free variables
           and a precedence.
  RETURNS: Nothing.
  EFFECT:  The term is destructively changed, i.e. the
           existence quantifier is removed by skolemization.
	   The precedence of new Skolem functions is set in <Precedence>.
*********************************************************/
{
  LIST exlist;
  TERM subterm;
  LIST symblist;

  symblist = list_Nil();
  exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term)));
  term_Delete(term_FirstArgument(Term));
  subterm = term_SecondArgument(Term);
  list_Delete(term_ArgumentList(Term));
  term_RplacTop(Term,term_TopSymbol(subterm));
  term_RplacArgumentList(Term,term_ArgumentList(subterm));
  term_Free(subterm);
  symblist = cnf_SkolemFunctionFormula(Term, FreeList, exlist, Precedence);
  list_Delete(exlist);
  list_Delete(symblist);
}


static LIST cnf_FreeVariablesBut(TERM Term, LIST Symbols)
/********************************************************
  INPUT:   A term and a list of symbols
  RETURNS: A list of all free variable terms in Term whose symbols are 
           not in Symbols
*********************************************************/
{
  LIST follist, Scan;
  follist = fol_FreeVariables(Term);
  for (Scan = follist; !list_Empty(Scan); Scan = list_Cdr(Scan))
    if (list_Member(Symbols, (POINTER)term_TopSymbol(list_Car(Scan)),
		    (BOOL (*)(POINTER,POINTER))symbol_Equal))
      list_Rplaca(Scan,NULL);
  follist = list_PointerDeleteElement(follist,NULL);
    
  return follist;
}


static void cnf_SkolemFunctionFormulaMapped(TERM term, LIST allist, LIST map)
/**************************************************************
  INPUT:   A term  term and a  list allist of variables and a list map
           of pairs (variable symbols, function symbol)
  RETURNS: None.
  CAUTION: The term is destructively changed. All variable symbols
           in map which appear in term are replaced by the skolem functions
	   with respect to allist which contains the universally quantified
	   variables.
***************************************************************/
{
  TERM   term1;
  LIST   scan,scan1;
  SYMBOL skolem, symbol;
  int    bottom;

  bottom = vec_ActMax();
  
  for (scan1=map; !list_Empty(scan1); scan1=list_Cdr(scan1)) {
    vec_Push(term);
    symbol = (SYMBOL) list_PairFirst((LIST) list_Car(scan1));
    skolem = (SYMBOL) list_PairSecond((LIST) list_Car(scan1));

#ifdef CHECK_STRSKOLEM
    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
      fputs("\nVariable : ", stdout);
      symbol_Print(symbol);
      fputs("\nFunction : ", stdout);
      symbol_Print(skolem);
    }
#endif
    while (bottom != vec_ActMax()) {
      term1 = (TERM)vec_PopResult();

      if (symbol_Equal(term_TopSymbol(term1),symbol)) {
	term_RplacTop(term1,skolem);
	list_Delete(term_ArgumentList(term1));
	term_RplacArgumentList(term1,term_CopyTermList(allist));
      }
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) {
	  vec_Push(list_Car(scan));
	}
    }
  }
  vec_SetMax(bottom);
}


static BOOL cnf_HasDeeperVariable(LIST List1, LIST List2)
/******************************************************************
   INPUT:   Two lists of variable terms
   RETURNS: TRUE if a variable in the first list is deeper than all variables
            in the second list, FALSE otherwise.
   NOTE:    If cnf_VARIABLEDEPTHARRAY is not allocated this will crash
            If new variables are introduced by strong skolemization, their
            depth is -1.
*******************************************************************/
{
  LIST scan;
  int  maxdepth1;
  
  /* Determine maximum depth of variables in List1 */
  maxdepth1 = 0;
  for (scan=List1; !list_Empty(scan); scan=list_Cdr(scan)) {
    int i;
    i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))];
#ifdef CHECK_STRSKOLEM
    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
      fputs("\nFor variable ", stdout);
      symbol_Print(term_TopSymbol((TERM) list_Car(scan)));
      printf(" depth is %d.", i);
    }
#endif
    if (i > maxdepth1)
      maxdepth1 = i;
  }

  /* Compare with depth of variables in List2 */
  for (scan=List2; !list_Empty(scan); scan=list_Cdr(scan)) {
    int i;
    i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))];
#ifdef CHECK_STRSKOLEM
    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
      fputs("\nFor variable ", stdout);
      symbol_Print(term_TopSymbol((TERM) list_Car(scan)));
      printf(" depth is %d.", i);
    }
#endif
    if (i >= maxdepth1)
      return FALSE;
  }
  return  TRUE;
}


static void cnf_StrongSkolemization(PROOFSEARCH Search, TERM Topterm,
				    char* Toplabel, BOOL TopAnd, TERM Term, 
				    LIST* UsedTerms, LIST* Symblist,
				    BOOL Result1,
				    HASH InputClauseToTermLabellist, int Depth)
/******************************************************************
  INPUT:   An existence quantified formula. ??? EK
  RETURNS: Nothing.
  EFFECT:  The existence quantifier is removed by strong skolemization.
           The precedence of new Skolem symbols is set in the precedence
	   of the search object.
*******************************************************************/
{
  LIST       exlist;    /* Variable symbols bound by exists[]() */
  LIST       pairlist;  /* List of pairs (Subterm of AND, free variable symbols
			   not in exlist) */
  LIST       allfreevariables;
  LIST       newvariables;       /* w2..wn*/
  LIST       mapping;           /* List of pairs */
  int        numberofallfreevariables, acc_length, i;
  LIST       pair, pairscan, pairscan_pred, scan, accumulatedvariables;
  TERM       subterm, w;
  BOOL       strskolemsuccess;  /* Indicates whether strong skolemization was
				   possible */
  FLAGSTORE  Flags;
  PRECEDENCE Precedence;

  Flags      = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  /* Necessary so that new variables really are new ! */
  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))
    symbol_SetStandardVarCounter(term_MaxVar(Topterm));

  /* Get list of quantified variable symbols x_k */
  exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term)));
  /* Pop quantifier */
  term_Delete(term_FirstArgument(Term));
  subterm = term_SecondArgument(Term);
  list_Delete(term_ArgumentList(Term));
  term_RplacTop(Term,term_TopSymbol(subterm));
  term_RplacArgumentList(Term,term_ArgumentList(subterm));
  term_Free(subterm);

  /* Now for every argument get the list of free variables whose symbols
     are not in exlist */
  pairlist = list_Nil();
  for (scan=term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) {
    pair = list_PairCreate((TERM) list_Car(scan), 
			   cnf_FreeVariablesBut((TERM) list_Car(scan), exlist));
    if (list_Empty(pairlist)) 
      pairlist = list_List(pair);
    else {
      /* First sort subterms by number of free variables */
      int pairlength, currentlength;
      pairlength = list_Length((LIST) list_PairSecond(pair));
      pairscan = pairlist; 
      pairscan_pred = list_Nil();
      currentlength = 0;
      while (!list_Empty(pairscan)) {
	currentlength = list_Length((LIST) list_PairSecond((LIST) list_Car(pairscan)));
	if (currentlength < pairlength) {
	  pairscan_pred = pairscan;
	  pairscan = list_Cdr(pairscan);
	}
	else if (currentlength == pairlength) {
	  /* If both subterms have the same number of free variables compare depth of variables */
	  if (cnf_HasDeeperVariable((LIST) list_PairSecond((LIST) list_Car(pairscan)), /* in list */
				   (LIST) list_PairSecond(pair))) {                   /* new pair */
#ifdef CHECK_STRSKOLEM
	    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
	      fputs("\nTerm ", stdout);
	      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
	      fputs("\n has deeper variable than ", stdout);
	      term_Print((TERM) list_PairFirst(pair));
	    }
#endif	    
	    pairscan_pred = pairscan;
	    pairscan = list_Cdr(pairscan);
	  }
	  else
	    break;
	}
	else
	  break;
      }
      
      /* New pair has more variables than all others in list */
      if (list_Empty(pairscan))
	list_Rplacd(pairscan_pred, list_List(pair));
      /* New pair is inserted between pairscan_pred and pairscan */
      else if (currentlength >= pairlength) { 
	/* Head of list */
	if (list_Empty(pairscan_pred))
	  pairlist = list_Cons(pair, pairlist);
	else 
	  list_InsertNext(pairscan_pred, pair);
      }
      /* The case for the same number of variables is not yet implemented */
    }
  }

#ifdef CHECK_STRSKOLEM
  if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
    for (pairscan=pairlist; !list_Empty(pairscan); pairscan = list_Cdr(pairscan)) {
      LIST l;
      fputs("\nSubterm ", stdout);
      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
      fputs("\n  has free variables ", stdout);
      for (l=(LIST) list_PairSecond((LIST) list_Car(pairscan)); !list_Empty(l); l = list_Cdr(l)) {
	term_Print((TERM) list_Car(l));
	fputs(" ", stdout);
      }
    }
  }
#endif

  /* Determine number of all free variablein and()--term whose symbols are not in exlist */
  /* Create map from ex_variables tp skolem symbols */
  allfreevariables = cnf_FreeVariablesBut(Term, exlist);
  numberofallfreevariables = list_Length(allfreevariables);
    
  mapping  = list_Nil();

  for (scan = exlist; !list_Empty(scan); scan = list_Cdr(scan)) {
    SYMBOL skolem;
    skolem = symbol_CreateSkolemFunction(numberofallfreevariables, Precedence);
    *Symblist = list_Cons((POINTER)skolem,*Symblist);
    mapping = list_Cons(list_PairCreate(list_Car(scan), (POINTER)skolem), 
			mapping);
  }
  list_Delete(allfreevariables);

  /* Create new variables */
  newvariables = list_Nil();

  for (i=0; i < numberofallfreevariables; i++) {
    w = term_CreateStandardVariable();
    newvariables = list_Cons(w, newvariables);
  }

#ifdef CHECK_STRSKOLEM
  if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
    LIST l;
    fputs("\nNew variables : ", stdout);
    for (l=newvariables; !list_Empty(l); l = list_Cdr(l)) {
      term_Print((TERM) list_Car(l));
      fputs(" ", stdout);
    }
  }
#endif
  
  /* Now do the replacing */
  accumulatedvariables = list_Nil();
  acc_length = 0;
  strskolemsuccess = FALSE;
  for (pairscan=pairlist; !list_Empty(pairscan); pairscan=list_Cdr(pairscan)) {
    LIST allist;

    /* Add bound variables for this subterm */
    accumulatedvariables = list_Nconc(accumulatedvariables,
				      (LIST) list_PairSecond((LIST) list_Car(pairscan)));
    accumulatedvariables = term_DeleteDuplicatesFromList(accumulatedvariables);

    /* Remove new variables not (no longer) needed */
    for (i=0; i < list_Length(accumulatedvariables) - acc_length; i++) {
      term_Delete((TERM) list_Top(newvariables));
      newvariables = list_Pop(newvariables);
    }
    acc_length = list_Length(accumulatedvariables);

#ifdef CHECK_STRSKOLEM
    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
      LIST l;
      fputs("\n\nSubterm is ", stdout);
      term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan)));
      fputs("\nFree variables : ", stdout);
      for (l=accumulatedvariables; !list_Empty(l); l = list_Cdr(l)) {
	term_Print((TERM) list_Car(l));
	fputs(" ", stdout);
      }
    }
#endif
    if (!list_Empty(newvariables))
      strskolemsuccess = TRUE;
    allist = list_Nconc(list_Copy(accumulatedvariables), list_Copy(newvariables));

    cnf_SkolemFunctionFormulaMapped((TERM) list_PairFirst((LIST) list_Car(pairscan)), allist,
				    mapping);
#ifdef CHECK_STRSKOLEM
    if (flag_GetFlagValue(flag_PSTRSKOLEM)) {
      fputs("\nSubterm after skolemization : ", stdout);
      term_Print(list_PairFirst((LIST) list_Car(pairscan)));
    }
#endif

    list_Delete(allist);
    cnf_OptimizedSkolemFormula(Search, Topterm, Toplabel, TopAnd,
			       (TERM) list_PairFirst((LIST) list_Car(pairscan)),
			       UsedTerms, Symblist, Result1, 
			       InputClauseToTermLabellist, Depth);
  }
  while (!list_Empty(newvariables)) {
    term_Delete((TERM) list_Top(newvariables));
    newvariables = list_Pop(newvariables);
  }
  list_Delete(accumulatedvariables); /* Only pairs and pairlist left */
  list_DeletePairList(pairlist);
  list_Delete(exlist);
  list_DeletePairList(mapping);
  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM) && strskolemsuccess) {
    fputs("\nStrong skolemization applied", stdout);
  }
}
    

static void cnf_OptimizedSkolemFormula(PROOFSEARCH Search, TERM topterm,
				       char* toplabel, BOOL TopAnd, TERM term, 
				       LIST* UsedTerms, LIST* Symblist,
				       BOOL Result1,
				       HASH InputClauseToTermLabellist,
				       int Depth)
/**************************************************************
  INPUT:   Two terms in negation normal form. ??? EK
  RETURNS: The  skolemized term with the optimized skolemization
           due to Ohlbach and Weidenbach of <term> and further improvements.
	   <rest> is used as additional, conjunctively added information.
  EFFECT:  The symbol precedence of the search  object is changed
           because new Skolem symbols are defined.
  CAUTION: The term is destructively changed.
***************************************************************/
{
  TERM       termL2, provedterm;
  LIST       freevariables, scan, varlist;
  SYMBOL     top;
  BOOL       result2;
  BOOL       optimized;
  FLAGSTORE  Flags;
  PRECEDENCE Precedence;

  result2       = FALSE;
  freevariables = list_Nil();
  Flags         = prfs_Store(Search);
  Precedence    = prfs_Precedence(Search);
  
  top = term_TopSymbol(term);
  if (fol_IsQuantifier(top)) {
    if (symbol_Equal(top,fol_All())) {
      /* For quantified variables store depth if strong skolemization is performed */
      if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
	LIST variables;
	variables = term_ArgumentList(term_FirstArgument(term));
	for (scan=variables; !list_Empty(scan); scan=list_Cdr(scan)) {
#ifdef CHECK_STRSKOLEM
	  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
	    if (cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] != -1) {
	      fputs("\nFor variable ", stderr);
	      term_Print((TERM) list_Car(scan));
	      printf(" depth is already set to %d, now setting it to %d", 
		     cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))],Depth);
	    }
	  }
#endif
#ifdef CHECK_STRSKOLEM
	  if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
	    fputs("\nVariable ", stdout);
	    term_Print((TERM) list_Car(scan));
	    printf(" has depth %d in term\n  ", Depth);
	    term_Print(term);
	  }
#endif
	  cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] = Depth;
	}
	Depth++;
      }
      cnf_PopAllQuantifier(term);
      cnf_OptimizedSkolemFormula(Search,topterm, toplabel, TopAnd, term, 
				 UsedTerms, Symblist, Result1,
				 InputClauseToTermLabellist, Depth);
      return;
    }
    freevariables = fol_FreeVariables(term);
    optimized = FALSE;
    if (symbol_Equal(term_TopSymbol(term_SecondArgument(term)), fol_And())) {
      if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM)) {
	scan = term_ArgumentList(term_SecondArgument(term));
	varlist = term_ArgumentList(term_FirstArgument(term));
	while (!list_Empty(scan) && !optimized) {
	  if (!Result1) {
	    if (TopAnd) {
	      if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
		fputs("\nHaveProof not necessary", stdout);
	      }
	      result2 = TRUE;
	    }
	    else {
	      termL2 = cnf_QuantifyAndNegate((TERM) list_Car(scan), 
					     varlist, freevariables);
	      result2 = cnf_HaveProofOptSkolem(Search, topterm, toplabel, termL2,
					       UsedTerms, Symblist, 
					       InputClauseToTermLabellist);
#ifdef CHECK_OPTSKOLEM
	      if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
		fputs("\nHaveProof result : ", stdout);
		if (result2)
		  fputs("TRUE", stdout);
		else
		  fputs("FALSE", stdout);
	      }
#endif
	    }
	  }
	    
	  if (Result1 || result2) {
	    optimized = TRUE;
	    if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
	      fputs("\nIn term ", stdout);
	      term_Print(topterm);
	      fputs("\n subterm ", stdout);
	      term_Print((TERM) list_Car(scan));
	      puts(" is moved to toplevel.");
	    }
	    provedterm =
	      cnf_MoveProvedTermToTopLevel(topterm, term, list_Car(scan), 
					   varlist, freevariables, Precedence);
	    if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) {
	      fputs("Result : ", stdout);
	      term_Print(topterm);
	      putchar('\n');
	    }
	    /* provedterm is argument of top AND term */
	    cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TRUE,
				       provedterm,UsedTerms, Symblist, Result1, 
				       InputClauseToTermLabellist, Depth);
	  }
	  else 
	    scan = list_Cdr(scan);
	}
      }
      if (!optimized) {
	/* Optimized skolemization not enabled or not possible */
	if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
	  optimized = TRUE; /* Strong Skolemization is always possible after exists[..](and(..)) */
	  cnf_StrongSkolemization(Search, topterm, toplabel, TopAnd, term,
				  UsedTerms, Symblist, Result1, 
				  InputClauseToTermLabellist, Depth);
	}
      }
    }
    else
      TopAnd = FALSE;
    if (!optimized) {
      /* Optimized skolemization not enabled or not possible */
      /* Strong skolemization not enabled or not possible */
      cnf_Skolemize(term, freevariables, Precedence);
    }
    list_Delete(freevariables);
    cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd, term,UsedTerms,
			       Symblist,Result1,InputClauseToTermLabellist,Depth);
    return;
  } 
  else {
    if (symbol_Equal(top,fol_And()) || symbol_Equal(top,fol_Or())) {
      if (symbol_Equal(top,fol_Or()))
	TopAnd = FALSE;
      for (scan=term_ArgumentList(term);!list_Empty(scan);
	   scan=list_Cdr(scan))
	cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd,
				   (TERM) list_Car(scan),
				   UsedTerms, Symblist,
				   Result1, InputClauseToTermLabellist, Depth);
    }
  }
  return;
}


static LIST cnf_SkolemFunctionFormula(TERM term, LIST allist, LIST exlist,
				      PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A term <term>, a list <allist> of variables, a list <exlist>
           of variable symbols and a precedence.
  RETURNS: The list of new Skolem functions.
  EFFECT:  The term is destructively changed. All variable symbols
           in <exlist> which appear in <term> are replaced by skolem functions
	   with respect to <allist> which contains the universally quantified
	   variables.
	   New Skolem functions are created and their precedence is set
	   in <Precedence>.
***************************************************************/
{
  TERM   term1;
  LIST   scan, scan1, Result;
  SYMBOL skolem;
  int    bottom,n;

  Result = list_Nil();
  bottom = vec_ActMax();
  n = list_Length(allist);
  
  for (scan1=exlist; !list_Empty(scan1); scan1=list_Cdr(scan1)) {
    vec_Push(term);
    skolem = symbol_CreateSkolemFunction(n, Precedence);
    Result = list_Cons((POINTER)skolem, Result);
    
    while (bottom != vec_ActMax()) {
      term1 = (TERM)vec_PopResult();
      if (symbol_Equal(term_TopSymbol(term1),(SYMBOL)list_Car(scan1))) {
	term_RplacTop(term1,skolem);
	list_Delete(term_ArgumentList(term1));
	term_RplacArgumentList(term1,term_CopyTermList(allist));
      }
      if (!list_Empty(term_ArgumentList(term1)))
	for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan))
	  vec_Push(list_Car(scan));
    }
  }
  vec_SetMax(bottom);
  return Result;
}


static LIST cnf_OptimizedSkolemization(PROOFSEARCH Search, TERM Term,
				       char* Label, LIST* UsedTerms, 
				       LIST* Symblist, BOOL result,
				       BOOL Conjecture, 
				       HASH InputClauseToTermLabellist)
/**************************************************************
  INPUT:   A term, a shared index and a list of non-ConClauses. ??? EK
  RETURNS: The list of clauses derived from Term.
  EFFECT:  The term is skolemized using optimized skolemization wrt ShIndex.
**************************************************************/
{
  LIST       Clauses;
  TERM       FirstArg;
  int        i;
  FLAGSTORE  Flags;
  PRECEDENCE Precedence;

#ifdef CHECK
  if (Term == NULL) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_OptimizedSkolemization: Input term is NULL.\n");
    misc_FinishErrorReport();
  }
#endif

  Flags      = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);
  FirstArg   = Term;

  if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
    /* Initializing array */
    for (i = 1; i <= symbol__MAXSTANDARDVAR; i++)
      cnf_VARIABLEDEPTHARRAY[i] = -1;
  }

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

  if (!fol_IsLiteral(Term)) {
    if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM) ||
	flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))  {
      if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM))
	Term = term_Create(fol_And(), list_List(Term)); /* CW hack: definitions are added on top level*/
      cnf_OptimizedSkolemFormula(Search, Term, Label, TRUE, FirstArg, UsedTerms, 
				 Symblist, result, InputClauseToTermLabellist, 0);
    }
    else {
      LIST Symbols;
      Symbols = list_Nil();
      Term    = cnf_SkolemFormula(Term, Precedence, &Symbols);
      list_Delete(Symbols);
    }
  }
  if (flag_GetFlagValue(Flags, flag_POPTSKOLEM) ||
      flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) {
    fputs("\nTerm after skolemization : ", stdout);
    term_Print(Term);
  }
  Term    = cnf_DistributiveFormula(Term);
  Clauses = cnf_MakeClauseList(Term, FALSE, Conjecture, Flags, Precedence);
  term_Delete(Term);

  return Clauses;
}


LIST cnf_GetSkolemFunctions(TERM Term, LIST ArgList, LIST* SkolToExVar)
/**************************************************************
  INPUT:   A term, the argumentlist of a skolem function, a mapping from
           a skolem function to a variable
  RETURNS: The longest argumentlist of all skolem functions found so far.
  EFFECT:  Computes information for renaming variables and replacing 
           skolem functions during de-skolemization.
**************************************************************/ 
{
  LIST Scan;
  SYMBOL Top;
    
  Top = term_TopSymbol(Term);

  if (fol_IsQuantifier(Top)) 
    return cnf_GetSkolemFunctions(term_SecondArgument(Term), ArgList, 
				  SkolToExVar);

  if (symbol_IsFunction(Top) && symbol_HasProperty(Top, SKOLEM)) {
    BOOL found;
    SYMBOL Var = 0;
    int Arity;
    found = FALSE;
      
    /* Keep longest argument list of all skolem functions in the clause for renaming */
    /* Delete all other argument lists */
    Arity = list_Length(term_ArgumentList(Term));
    if (Arity > list_Length(ArgList)) {
      term_DeleteTermList(ArgList);
      ArgList = term_ArgumentList(Term);
    }
    else 
      term_DeleteTermList(term_ArgumentList(Term));
    term_RplacArgumentList(Term, NULL);
      
    /* Replace skolem function by variable */
    if (list_Length(*SkolToExVar) > Arity) {
      NAT i;
      LIST SkolScan = *SkolToExVar;
      for (i = 0; i < Arity; i++)
	SkolScan = list_Cdr(SkolScan);
      for (SkolScan = (LIST) list_Car(SkolScan);
	   (SkolScan != list_Nil()) && !found; SkolScan = list_Cdr(SkolScan)) {
	SYMBOL Skol;
	Skol = (SYMBOL) list_PairFirst((LIST) list_Car(SkolScan));
	if (Skol == term_TopSymbol(Term)) {
	  Var = (SYMBOL) list_PairSecond((LIST) list_Car(SkolScan));
	  found = TRUE;
	}
      }
    }
    if (!found) {
      LIST Pair;
      NAT  i;
      LIST SkolScan;

      SkolScan = *SkolToExVar;
      for (i = 0; i < Arity; i++) {
	if (list_Cdr(SkolScan) == list_Nil())
	  list_Rplacd(SkolScan, list_List(NULL));
	SkolScan = list_Cdr(SkolScan);
      }

      Var = symbol_CreateStandardVariable();
      Pair = list_PairCreate((POINTER) term_TopSymbol(Term), 
			     (POINTER) Var);
      if (list_Car(SkolScan) == list_Nil())
	list_Rplaca(SkolScan, list_List(Pair));
      else
	list_Rplaca(SkolScan, list_Nconc((LIST) list_Car(SkolScan), 
					 list_List(Pair)));
    }
    term_RplacTop(Term, Var);
  }
  else {
    for (Scan = term_ArgumentList(Term); Scan != list_Nil(); 
	Scan = list_Cdr(Scan))
      ArgList = cnf_GetSkolemFunctions((TERM) list_Car(Scan), ArgList, 
				       SkolToExVar);
  }
  return ArgList;
}


void cnf_ReplaceVariable(TERM Term, SYMBOL Old, SYMBOL New)
/**************************************************************
  INPUT:  A term, two symbols that are variables
  EFFECT: In term every occurrence of Old is replaced by New
**************************************************************/ 
{
  LIST Scan;

#ifdef CHECK
  if (!symbol_IsVariable(Old)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_ReplaceVariable: Illegal input symbol.\n");
    misc_FinishErrorReport();
  }
#endif

  if (symbol_Equal(term_TopSymbol(Term), Old))
    term_RplacTop(Term, New);
  else 
    for (Scan = term_ArgumentList(Term); !list_Empty(Scan); 
	 Scan = list_Cdr(Scan))
      cnf_ReplaceVariable(list_Car(Scan), Old, New);
}


LIST cnf_RemoveSkolemFunctions(CLAUSE Clause, LIST* SkolToExVar, LIST Vars)
/**************************************************************
  INPUT:   A clause, a list which is a mapping from skolem functions to
           variables and a list of variables for forall-quantification.
  RETURNS: A list of terms derived from the clause using deskolemization
  EFFECT:  Arguments of skolem functions are renamed consistently.
           Skolemfunctions are replaced by variables.
**************************************************************/
{
  LIST Scan;
  LIST TermScan, TermList, ArgList;
  TERM Term;
  int i;

  TermList = list_Nil();

  ArgList = list_Nil();
  for (i = 0; i < clause_Length(Clause); i++) {
    Term = term_Copy(clause_GetLiteralTerm(Clause, i));
    ArgList = cnf_GetSkolemFunctions(Term, ArgList, SkolToExVar);
    TermList = list_Cons(Term, TermList);
  }
    
  if (list_Empty(ArgList))
    return TermList;
    
  /* Rename variables */
  for (Scan = ArgList; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
    for (TermScan = TermList; TermScan != list_Nil(); 
	 TermScan = list_Cdr(TermScan)) {
      Term = (TERM) list_Car(TermScan);
      cnf_ReplaceVariable(Term,
			  term_TopSymbol((TERM) list_Car(Scan)),
			  (SYMBOL) list_Car(Vars));
    }
    if (list_Cdr(Vars) == list_Nil()) {
      SYMBOL New = symbol_CreateStandardVariable();
      Vars = list_Nconc(Vars, list_List((POINTER) New));
    }
    Vars = list_Cdr(Vars);
  }
  term_DeleteTermList(ArgList);
  return TermList;
}


TERM cnf_DeSkolemFormula(LIST Clauses)
/**************************************************************
  INPUT:   A list of clauses.
  RETURNS: A formula built from the clauses.
  EFFECT:  All skolem functions are removed from the clauses.
**************************************************************/
{
  LIST Scan, SkolToExVar, Vars, FreeVars, FreeVarsCopy, VarScan, TermList;
  TERM VarListTerm, TopTerm, Term;
  BOOL First;
  
  SkolToExVar = list_List(NULL);
  Vars = list_List((POINTER) symbol_CreateStandardVariable());
  
  TopTerm = term_Create(fol_And(), NULL);
  
  for (Scan = Clauses; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
    TermList =  cnf_RemoveSkolemFunctions((CLAUSE) list_Car(Scan),
					  &SkolToExVar, Vars);
    Term = term_Create(fol_Or(), TermList);
    FreeVars = fol_FreeVariables(Term);
    if (!list_Empty(FreeVars)) {
      FreeVarsCopy = term_CopyTermList(FreeVars);
      list_Delete(FreeVars);
      Term = fol_CreateQuantifier(fol_All(), FreeVarsCopy, list_List(Term));
    }
    term_RplacArgumentList(TopTerm, list_Cons(Term, term_ArgumentList(TopTerm)));
  }
  
  VarScan = Vars;
  First = TRUE;
  
  for (Scan = SkolToExVar; Scan != list_Nil(); Scan = list_Cdr(Scan)) {
    if (list_Empty(list_Car(Scan))) {
      if (term_TopSymbol(TopTerm) == fol_All())
	term_RplacArgumentList(TopTerm, list_Cons(term_Create((SYMBOL) list_Car(VarScan), NULL),  
						  term_ArgumentList(TopTerm)));
      if (!First)
	TopTerm = fol_CreateQuantifier(fol_All(),
				       list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)),
				       list_List(TopTerm)); 
    }
    else {
      LIST ExVarScan;
      LIST ExVars = list_Nil();
      for (ExVarScan = list_Car(Scan); ExVarScan != list_Nil();
	  ExVarScan = list_Cdr(ExVarScan)) {
	if (ExVars == list_Nil())
	  ExVars = list_List(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL));
	else
	  ExVars = list_Cons(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL), ExVars);
	list_PairFree((LIST) list_Car(ExVarScan));
      }
      list_Delete((LIST) list_Car(Scan));
      list_Rplaca(Scan, NULL);

      if (term_TopSymbol(TopTerm) == fol_Exist()) {
	VarListTerm = (TERM) list_Car(term_ArgumentList(TopTerm));
	term_RplacArgumentList(VarListTerm,
			       list_Nconc(term_ArgumentList(VarListTerm),
					  ExVars));
      }
      else
	TopTerm = fol_CreateQuantifier(fol_Exist(), ExVars, list_List(TopTerm));
      ExVars = list_Nil();

      if (!First) 
	TopTerm = fol_CreateQuantifier(fol_All(), 
				       list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)),
				       list_List(TopTerm));
    }
    if (!First) 
      VarScan = list_Cdr(VarScan);
    else
      First = FALSE;
	
  }
  list_Delete(SkolToExVar);
  list_Delete(Vars);

  return TopTerm;
}


#ifdef OPTCHECK
/* Currently unused */
/*static */
LIST cnf_CheckOptimizedSkolemization(LIST* AxClauses, LIST* ConClauses,
				     TERM AxTerm, TERM ConTerm,
				     LIST NonConClauses, LIST* SkolemPredicates,
				     SHARED_INDEX ShIndex, BOOL result)
/**********************************************************
  EFFECT: Used to check the correctness of optimized skolemization
***********************************************************/
{
  TERM DeSkolemizedAxOpt, DeSkolemizedConOpt, DeSkolemizedAx, DeSkolemizedCon;
  TERM TopOpt, Top, ToProve;
  LIST SkolemFunctions2;

  if (*AxClauses != list_Nil()) {
    DeSkolemizedAxOpt = cnf_DeSkolemFormula(*AxClauses);
    if (*ConClauses != list_Nil()) {
      DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses);
      TopOpt = term_Create(fol_And(), 
			   list_Cons(DeSkolemizedAxOpt, 
				     list_List(DeSkolemizedConOpt)));
    }
    else 
      TopOpt = DeSkolemizedAxOpt;
  }
  else {
    DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses);     
    TopOpt = DeSkolemizedConOpt;
  }
  
  clause_DeleteClauseList(*AxClauses);
  clause_DeleteClauseList(*ConClauses);
  *AxClauses = list_Nil();
  *ConClauses = list_Nil();
  
  flag_SetFlagValue(flag_CNFOPTSKOLEM, flag_CNFOPTSKOLEMOFF);  
  if (AxTerm) {
    *AxClauses = cnf_OptimizedSkolemization(term_Copy(AxTerm), ShIndex, NonConClauses, result,FALSE, ClauseToTermLabellist);
  }
  if (ConTerm) {
    *ConClauses = cnf_OptimizedSkolemization(term_Copy(ConTerm), ShIndex, NonConClauses, result,TRUE, ClauseToTermLabellist);
  }
  
  if (*AxClauses != list_Nil()) {
    DeSkolemizedAx = cnf_DeSkolemFormula(*AxClauses);
    if (*ConClauses != list_Nil()) {
      DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses);
      Top = term_Create(fol_And(), 
			list_Cons(DeSkolemizedAx, 
				  list_List(DeSkolemizedCon)));
    }
    else 
      Top = DeSkolemizedAx;
  }
  else {
    DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses);    
    Top = DeSkolemizedCon;
  }
  
  clause_DeleteClauseList(*AxClauses);
  clause_DeleteClausList(*ConClauses);
  *AxClauses = list_Nil();
  *ConClauses = list_Nil();
  
  ToProve = term_Create(fol_Equiv(), list_Cons(TopOpt, list_List(Top)));
  ToProve = term_Create(fol_Not(), list_List(ToProve));
  fol_NormalizeVars(ToProve); 
  ToProve  = cnf_ObviousSimplifications(ToProve);
  term_AddFatherLinks(ToProve);
  ToProve  = ren_Rename(ToProve,SkolemPredicates,FALSE);
  ToProve  = cnf_RemoveEquivImplFromFormula(ToProve);
  ToProve  = cnf_NegationNormalFormula(ToProve);
  ToProve  = cnf_AntiPrenex(ToProve);
  
  SkolemFunctions2 = list_Nil();
  ToProve     = cnf_SkolemFormula(ToProve, &SkolemFunctions2);
  ToProve     = cnf_DistributiveFormula(ToProve);
  *ConClauses = cnf_MakeClauseList(ToProve);
  if (ToProve)
    term_Delete(ToProve);
  *AxClauses = list_Nil();
  return SkolemFunctions2;
}
#endif


PROOFSEARCH cnf_Flotter(LIST AxiomList, LIST ConjectureList, LIST* AxClauses, 
			LIST* AllLabels, HASH TermLabelToClauselist, 
			HASH ClauseToTermLabellist, FLAGSTORE InputFlags,
			PRECEDENCE InputPrecedence, LIST* Symblist)
/**************************************************************
  INPUT:   A list of axiom formulae,
           a list of conjecture formulae,
	   a pointer to a list in which clauses derived from axiom formulae 
	   are stored,
	   a pointer to a list in which clauses derived from 
	   conjecture formulae are stored, ???
	   a pointer to a list of all termlabels,
	   a hasharray in which for every term label the list of clauses 
	   derived from the term is stored (if DocProof is set),
	   a hasharray in which for every clause the list of labels 
	   of the terms used for deriving the clause is stored (if DocProof 
	   is set),
	   a flag store,
	   a precedence
	   a pointer to a list of symbols which have to be deleted later if
	   the ProofSearch object is kept.
  RETURNS: If KeepProofSearch ??? is TRUE, then the ProofSearch object is not
           freed but returned.
	   Else, NULL is returned.
  EFFECT:  ??? EK
           The precedence of new skolem symbols is set in <InputPrecedence>.
***************************************************************/
{
  LIST        Scan, Scan2, FormulaClauses,SkolemFunctions;
  LIST        SkolemPredicates, EmptyClauses, AllFormulae;
  LIST        UsedTerms;
  TERM        AxTerm,Formula;
  BOOL        Result;
  PROOFSEARCH Search;
  PRECEDENCE  Precedence;
  FLAGSTORE   Flags;
  NAT         Count;
  HASH        InputClauseToTermLabellist;

  Search = prfs_Create();

  /* Initialize the flagstore for the CNF transformation */
  Flags = prfs_Store(Search);
  flag_CleanStore(Flags);
  flag_InitFlotterFlags(InputFlags, Flags);
  /* Initialize the precedence */
  Precedence = prfs_Precedence(Search);
  symbol_TransferPrecedence(InputPrecedence, Precedence);

  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
    prfs_AddDocProofSharingIndex(Search);

  AxTerm           = (TERM)NULL;
  SkolemPredicates = list_Nil();
  Result           = FALSE;
  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
    InputClauseToTermLabellist = hsh_Create();
  else 
    InputClauseToTermLabellist = NULL;

  symbol_ReinitGenericNameCounters();

  for (Scan = AxiomList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    LIST Pair;
    Pair = list_Car(Scan);
    AxTerm = (TERM) list_PairSecond(Pair);
    fol_RemoveImplied(AxTerm);
    term_AddFatherLinks(AxTerm);
    fol_NormalizeVars(AxTerm);
    if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS))
      cnf_PropagateSubstEquations(AxTerm);
    AxTerm = cnf_ObviousSimplifications(AxTerm);
    if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
      term_AddFatherLinks(AxTerm);
      AxTerm = ren_Rename(AxTerm, Precedence, &SkolemPredicates,
			  flag_GetFlagValue(Flags, flag_CNFPRENAMING), TRUE);
    }
    AxTerm = cnf_RemoveEquivImplFromFormula(AxTerm);
    AxTerm = cnf_NegationNormalFormula(AxTerm);
    AxTerm = cnf_AntiPrenex(AxTerm);
    list_Rplacd(Pair, (LIST) AxTerm);
  }
  AllFormulae = AxiomList;
  
  /* At this point the list contains max. 1 element, which is a pair 
     of the label NULL and the negated
     conjunction of all conjecture formulae. */

  Count = 0;
  for (Scan = ConjectureList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    TERM  ConTerm;
    char* Label;
    char  buf[100];
    /* Add label */  
    if (list_PairFirst(list_Car(Scan)) == NULL) {
      sprintf(buf, "conjecture%d", Count);
      Label = string_StringCopy(buf);
      list_Rplaca((LIST) list_Car(Scan), Label);
      if (flag_GetFlagValue(Flags, flag_DOCPROOF) &&
	  flag_GetFlagValue(Flags, flag_PLABELS)) {
	printf("\nAdded label %s for conjecture", Label);
	fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan)));
      }
    }

    ConTerm = (TERM) list_PairSecond((LIST) list_Car(Scan));
    fol_RemoveImplied(ConTerm);
    term_AddFatherLinks(ConTerm);
    fol_NormalizeVars(ConTerm);  
    if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS))
      cnf_PropagateSubstEquations(ConTerm);
    ConTerm  = cnf_ObviousSimplifications(ConTerm); 

    if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
      term_AddFatherLinks(ConTerm);
      ConTerm = ren_Rename(ConTerm, Precedence, &SkolemPredicates,
			   flag_GetFlagValue(Flags, flag_CNFPRENAMING),TRUE);
    }
    /* fputs("\nRen:\t",stdout);term_Print(ConTerm);putchar('\n'); */
    ConTerm  = cnf_RemoveEquivImplFromFormula(ConTerm);
    ConTerm  = cnf_NegationNormalFormula(ConTerm);
    /* fputs("\nAn:\t",stdout);term_Print(ConTerm);putchar('\n'); */
    ConTerm  = cnf_AntiPrenex(ConTerm);
    /* fputs("\nPr:\t",stdout);term_Print(ConTerm);putchar('\n'); */
    /* Insert changed term into pair */
    list_Rplacd((LIST) list_Car(Scan), (LIST) ConTerm);

    Count++;
  } 

  AllFormulae = list_Append(ConjectureList, AllFormulae);
  for (Scan = ConjectureList;!list_Empty(Scan); Scan = list_Cdr(Scan))
    list_Rplaca(Scan,list_PairSecond(list_Car(Scan)));

  FormulaClauses = list_Nil();
  SkolemFunctions = list_Nil();
  Count = 0;
  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan), Count++) {
    LIST FormulaClausesTemp;
    Formula            = term_Copy((TERM) list_PairSecond(list_Car(Scan)));
#ifdef CHECK_CNF
    fputs("\nInputFormula : ",stdout); term_Print(Formula); 
    printf("\nLabel : %s", (char*) list_PairFirst(list_Car(Scan)));
#endif
    Formula            = cnf_SkolemFormula(Formula,Precedence,&SkolemFunctions);
    Formula            = cnf_DistributiveFormula(Formula);
    FormulaClausesTemp = cnf_MakeClauseList(Formula,FALSE,FALSE,Flags,Precedence);
    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
      for (Scan2 = FormulaClausesTemp; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) {
	hsh_Put(InputClauseToTermLabellist, list_Car(Scan2), list_PairFirst(list_Car(Scan)));
      }
    }
    FormulaClauses = list_Nconc(FormulaClauses, FormulaClausesTemp);
    term_Delete(Formula);
  }

  /* Trage nun Formula Clauses modulo Reduktion in einen Index ein */
 
  /* red_SatUnit works only on conclauses */
  for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);
  /* For FormulaClauses a full saturation */
  /* List is deleted in red_SatUnit ! */
  EmptyClauses = red_SatUnit(Search, FormulaClauses);
  if (!list_Empty(EmptyClauses)) {
    Result = TRUE;
    /*puts("\nPROOF in FormulaClauses");*/
    clause_DeleteClauseList(EmptyClauses);
  }

  /* Move all usables to workedoff */
  FormulaClauses = list_Copy(prfs_UsableClauses(Search));
  for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
    prfs_MoveUsableWorkedOff(Search, (CLAUSE) list_Car(Scan));
  list_Delete(FormulaClauses);
  FormulaClauses = list_Nil();

#ifdef CHECK
  /*cnf_CheckClauseListsConsistency(ShIndex); */
#endif     


  *Symblist = list_Nil();
  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    LIST Ax, Pair;
    UsedTerms = list_Nil();
    Pair = list_Car(Scan);
#ifdef CHECK_CNF
    fputs("\nFormula : ", stdout);
    term_Print((TERM) list_PairSecond(Pair)); 
    printf("\nLabel : %s", (char*) list_PairFirst(Pair)); 
#endif
    Ax = cnf_OptimizedSkolemization(Search, term_Copy((TERM)list_PairSecond(Pair)), 
				    (char*) list_PairFirst(Pair), &UsedTerms, 
				    Symblist,Result,FALSE,InputClauseToTermLabellist);
    /* Set CONCLAUSE flag for clauses derived from conjectures */
    if (list_PointerMember(ConjectureList,list_PairSecond(Pair))) {
      LIST l;
      for (l = Ax; !list_Empty(l); l = list_Cdr(l))
	clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE);
    }
    if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
      hsh_PutListWithCompareFunc(TermLabelToClauselist, list_PairFirst(Pair),
				 list_Copy(Ax),
				 (BOOL (*)(POINTER,POINTER))cnf_LabelEqual,
				 (unsigned long (*)(POINTER))hsh_StringHashKey);
      UsedTerms = list_Cons(list_PairFirst(Pair), UsedTerms);
      UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms);
      for (Scan2 = Ax; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) {
	hsh_PutList(ClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms));
	hsh_PutList(InputClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms));
      } 
    }
    *AxClauses = list_Nconc(*AxClauses, Ax);
    list_Delete(UsedTerms);
  }

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

  list_Delete(ConjectureList);
  if (flag_GetFlagValue(Flags, flag_DOCPROOF))
    hsh_Delete(InputClauseToTermLabellist);
  if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) { 
    list_Delete(*Symblist);
  }

  *AllLabels = list_Nil();
  for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    LIST Pair;
    Pair = list_Car(Scan);
    term_Delete((TERM) list_PairSecond(Pair));
    *AllLabels = list_Cons(list_PairFirst(Pair), *AllLabels);
    list_PairFree(Pair);
  }

  list_Delete(AllFormulae);
  list_Delete(SkolemFunctions);
  list_Delete(SkolemPredicates);

  if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) {
    symbol_ResetSkolemIndex();
    prfs_Delete(Search);
    return NULL;
  }
  else {
    /* Delete DocProof clauses */
    prfs_DeleteDocProof(Search);
    return Search;
  }
}

LIST cnf_QueryFlotter(PROOFSEARCH Search, TERM Term, LIST* Symblist)
/**************************************************************
  INPUT:   A term to derive clauses from, using optimized skolemization,
           and a ProofSearch object. 
  RETURNS: A list of derived clauses.
  EFFECT:  ??? EK
           The precedence of new skolem symbols is set in <Search>.
***************************************************************/
{
  LIST       SkolemPredicates, SkolemFunctions, IndexedClauses, Scan;
  LIST       ResultClauses, Dummy, EmptyClauses;
  TERM       TermCopy;
  int        Formulae2Clause;
  BOOL       Result;
  FLAGSTORE  Flags, SubProofFlags;
  PRECEDENCE Precedence;

  Flags      = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  /* Initialize the flagstore of the cnf_SEARCHCOPY object with default values */
  /* and copy the value of flag_DOCPROOF from the global Proofserach object.   */
  SubProofFlags = prfs_Store(cnf_SEARCHCOPY);
  flag_InitStoreByDefaults(SubProofFlags);
  flag_TransferFlag(Flags, SubProofFlags, flag_DOCPROOF);
  /* Transfer the precedence into the local search object */
  symbol_TransferPrecedence(Precedence, prfs_Precedence(cnf_SEARCHCOPY));

  SkolemPredicates = SkolemFunctions = list_Nil();
  Result = FALSE;
  
  prfs_CopyIndices(Search, cnf_SEARCHCOPY);

  Term = term_Create(fol_Not(), list_List(Term));
  fol_NormalizeVars(Term);
  Term = cnf_ObviousSimplifications(Term);
  if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) {
    term_AddFatherLinks(Term);
    Term = ren_Rename(Term, Precedence, &SkolemPredicates,
		      flag_GetFlagValue(Flags,flag_CNFPRENAMING), TRUE);
  }
  Term = cnf_RemoveEquivImplFromFormula(Term);
  Term = cnf_NegationNormalFormula(Term);
  Term = cnf_AntiPrenex(Term);
  
  TermCopy = term_Copy(Term);
  TermCopy = cnf_SkolemFormula(TermCopy, Precedence, &SkolemFunctions);
  TermCopy = cnf_DistributiveFormula(TermCopy);

  IndexedClauses = cnf_MakeClauseList(TermCopy,FALSE,FALSE,Flags,Precedence);
  term_Delete(TermCopy);

  /* red_SatUnit works only on conclauses */
  for (Scan = IndexedClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);

  EmptyClauses = red_SatUnit(cnf_SEARCHCOPY, IndexedClauses);

  if (!list_Empty(EmptyClauses)) {
    Result = TRUE;
    clause_DeleteClauseList(EmptyClauses);
  }

  while (!list_Empty(prfs_UsableClauses(cnf_SEARCHCOPY))) {
    prfs_MoveUsableWorkedOff(cnf_SEARCHCOPY, (CLAUSE) list_Car(prfs_UsableClauses(cnf_SEARCHCOPY)));
  }
  /* Works only if DOCPROOF is false. Otherwise we need labels */
  Dummy = list_Nil();
  if (flag_GetFlagValue(SubProofFlags, flag_DOCPROOF))
    Formulae2Clause = TRUE;
  else
    Formulae2Clause = FALSE;
  flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFOFF);
  ResultClauses = cnf_OptimizedSkolemization(cnf_SEARCHCOPY, term_Copy(Term),
					     NULL, &Dummy, Symblist, Result,
					     FALSE, NULL);

  if (Formulae2Clause)
    flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFON);
  
  term_Delete(Term);
  list_Delete(SkolemPredicates);
  list_Delete(SkolemFunctions);
  prfs_Clean(cnf_SEARCHCOPY);

  /* All result clauses of queries are conjecture clauses */
  for (Scan=ResultClauses; !list_Empty(Scan); Scan=list_Cdr(Scan))
    clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE);

  return ResultClauses;
}


#ifdef CHECK
/* Currently unused */
/*static*/ void cnf_CheckClauseListsConsistency(SHARED_INDEX ShIndex)
/**************************************************************
  INPUT: A shared index and a list of non-ConClauses.
  EFFECT: When this function is called all clauses in the index must be
       non-ConClauses, which must also be members of the list.
**************************************************************/
{
  LIST AllClauses, scan;

  AllClauses = clause_AllIndexedClauses(ShIndex);
  for (scan = AllClauses; scan != list_Nil(); scan = list_Cdr(scan)) {
    if (clause_GetFlag((CLAUSE) list_Car(scan), CONCLAUSE)) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is a CONCLAUSE.\n");
      misc_FinishErrorReport();
    } 
    if (clause_GetFlag((CLAUSE) list_Car(scan), BLOCKED)) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is BLOCKED.\n");
      misc_FinishErrorReport();
    }
  }
  list_Delete(AllClauses);
}
#endif


static LIST cnf_SatUnit(PROOFSEARCH Search, LIST ClauseList) 
/*********************************************************
  INPUT:   A list of unshared clauses, proof search object
  RETURNS: A possibly empty list of empty clauses.
**********************************************************/
{
  CLAUSE     Given;
  LIST       Scan, Derivables, EmptyClauses, BackReduced;
  NAT        n, Derived;
  FLAGSTORE  Flags;
  PRECEDENCE Precedence;

  Flags        = prfs_Store(Search);
  Precedence   = prfs_Precedence(Search);
  Derived      = flag_GetFlagValue(Flags, flag_CNFPROOFSTEPS);
  EmptyClauses = list_Nil();
  ClauseList   = clause_ListSortWeighed(ClauseList);
  
  while (!list_Empty(ClauseList) && list_Empty(EmptyClauses)) {
    Given = (CLAUSE)list_NCar(&ClauseList);
    Given = red_CompleteReductionOnDerivedClause(Search, Given, red_ALL);
    if (Given) {
      if (clause_IsEmptyClause(Given))
        EmptyClauses = list_List(Given);
      else {
        /*fputs("\n\nGiven: ",stdout);clause_Print(Given);*/
	BackReduced = red_BackReduction(Search, Given, red_USABLE);
	
        if (Derived != 0) {
	  Derivables =
	    inf_BoundedDepthUnitResolution(Given, prfs_UsableSharingIndex(Search),
					   FALSE, Flags, Precedence);
	  Derivables =
	    list_Nconc(Derivables,
		       inf_BoundedDepthUnitResolution(Given,prfs_WorkedOffSharingIndex(Search),
						      FALSE, Flags, Precedence));
          n = list_Length(Derivables);
          if (n > Derived)
            Derived = 0;
          else
            Derived -= n;
        }
        else 
          Derivables = list_Nil();
	
        Derivables  = list_Nconc(BackReduced,Derivables);
        Derivables  = split_ExtractEmptyClauses(Derivables, &EmptyClauses);
	
	prfs_InsertUsableClause(Search, Given);
	
	for (Scan = Derivables; !list_Empty(Scan); Scan = list_Cdr(Scan))
	  ClauseList = clause_InsertWeighed(list_Car(Scan), ClauseList, Flags,
					    Precedence);
	list_Delete(Derivables);
      }
    }
  }
  clause_DeleteClauseList(ClauseList);
  return EmptyClauses;
}


TERM cnf_DefTargetConvert(TERM Target, TERM ToTopLevel, TERM ToProveDef, 
			  LIST DefPredArgs, LIST TargetPredArgs,
			  LIST TargetPredVars, LIST VarsForTopLevel,
			  FLAGSTORE Flags, PRECEDENCE Precedence,
			  BOOL* LocallyTrue)
/**********************************************************
  INPUT:   A term Target which contains a predicate that might be replaced
           by its definition.
	   A term ToTopLevel which is the highest level subterm in Target
	   that contains the predicate and can be moved to top level or().
	   A term ToProveDef which must hold if the definition is to be applied.
	   (IS DESTROYED AND FREED)
	   A list DefPredArgs of the arguments of the predicate in the
	   Definition.
	   A list TargetPredArgs of the arguments of the predicate in Target.
	   A list TargetPredVars of the variables occurring in the arguments
	   of the predicate in Target.
	   A list VarsForTopLevel containing the variables that should be
	   all-quantified at top level to make the proof easier.
	   A flag store.
	   A pointer to a boolean LocallyTrue which is set to TRUE iff
	   the definition can be applied.
  RETURNS: The Target term which is brought into standard form.
**********************************************************/

{
  TERM orterm, targettoprove;
  SYMBOL maxvar;                    /* For normalizing terms */
  LIST l1, l2;
  LIST freevars, vars;              /* Free variables in targettoprove */

  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
    puts("\nTarget :");
    fol_PrettyPrint(Target);
  }
#ifdef CHECK
  fol_CheckFatherLinks(Target);
#endif
  /* No proof found yet */
  *LocallyTrue = FALSE;

  /* Remove implications from path */
  Target = cnf_RemoveImplFromFormulaPath(Target, ToTopLevel);
    
  /* Move negations as far down as possible */
  Target = cnf_NegationNormalFormulaPath(Target, ToTopLevel);
    
  /* Move quantifiers as far down as possible */
  Target = cnf_AntiPrenexPath(Target, ToTopLevel);

  /* Move all-quantified variables from the predicates' arguments to top level */
  Target = cnf_MovePredicateVariablesUp(Target, ToTopLevel, VarsForTopLevel);

  /* Flatten top or() */
  Target = cnf_FlattenPath(Target, ToTopLevel);

  /* Now make sure that all variables in the top forall quantifier are in TargetPredVars */
  /* Not necessary, according to CW */
  if (symbol_Equal(term_TopSymbol(Target), fol_All())) {
    targettoprove = term_Copy(term_SecondArgument(Target));
    orterm        = term_SecondArgument(Target);
  }
  else {
    targettoprove = term_Copy(Target);
    orterm        = Target;
  }

  /* Find argument of targettoprove that contains the predicate and remove it */
  if (symbol_Equal(term_TopSymbol(targettoprove), fol_Or())) {
    /* Find subterm that contains the predicate */
    LIST arglist;
    arglist = term_ArgumentList(targettoprove);
    for (l1=arglist, l2=term_ArgumentList(orterm); !list_Empty(l1); 
	l1 = list_Cdr(l1), l2 = list_Cdr(l2)) {
      if (term_HasProperSuperterm(ToTopLevel, (TERM) list_Car(l2)) ||
	  (ToTopLevel == (TERM) list_Car(l2))) {
	arglist = list_PointerDeleteElementFree(arglist, list_Car(l1),
						(void (*)(POINTER))term_Delete);
	break;
      }
    }
    term_RplacArgumentList(targettoprove, arglist);
    /* Nothing left for the proof ? */
    if (list_Empty(term_ArgumentList(targettoprove))) {
      term_Delete(targettoprove);
      term_Delete(ToProveDef);
#ifdef CHECK
      fol_CheckFatherLinks(Target);
#endif
      return Target;
    }
  }
  else {
    /* Nothing left for the proof */
    term_Delete(targettoprove);
    term_Delete(ToProveDef);
#ifdef CHECK
    fol_CheckFatherLinks(Target);
#endif
    return Target;
  }

  /* Normalize variables in ToProveDef with respect to targettoprove */
  maxvar = term_MaxVar(targettoprove);
  symbol_SetStandardVarCounter(maxvar);
  vars = fol_BoundVariables(ToProveDef);
  vars = term_DeleteDuplicatesFromList(vars);
  for (l1=vars; !list_Empty(l1); l1=list_Cdr(l1))
    term_ExchangeVariable(ToProveDef, term_TopSymbol(list_Car(l1)), symbol_CreateStandardVariable());
  list_Delete(vars);
  
  /* Replace arguments of predicate in condition of definition by matching arguments
     of predicate in target term */
  for (l1=DefPredArgs, l2=TargetPredArgs; !list_Empty(l1); l1=list_Cdr(l1), l2=list_Cdr(l2)) 
    term_ReplaceVariable(ToProveDef, term_TopSymbol((TERM) list_Car(l1)), (TERM) list_Car(l2));

  targettoprove = term_Create(fol_Not(), list_List(targettoprove));
  targettoprove = cnf_NegationNormalFormula(targettoprove);
  targettoprove = term_Create(fol_Implies(), 
			      list_Cons(targettoprove, list_List(ToProveDef)));

  /* At this point ToProveDef must not be accessed again ! */
  
  /* Add all--quantifier to targettoprove */
  freevars = fol_FreeVariables(targettoprove);
  term_CopyTermsInList(freevars);
  targettoprove = fol_CreateQuantifier(fol_All(), freevars, list_List(targettoprove));
  
  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
    puts("\nConverted to :");
    fol_PrettyPrint(Target);
  }

  targettoprove = cnf_NegationNormalFormula(targettoprove);
  
  if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
    puts("\nToProve for this target :");
    fol_PrettyPrint(targettoprove);
  }
 
  *LocallyTrue = cnf_HaveProof(list_Nil(), targettoprove, Flags, Precedence);
  
  term_Delete(targettoprove);

#ifdef CHECK
  fol_CheckFatherLinks(Target);
#endif

  return Target;
}


static TERM cnf_RemoveQuantFromPathAndFlatten(TERM TopTerm, TERM SubTerm)
/**********************************************************
  INPUT:  Two terms, <SubTerm> must be a subterm of <TopTerm>.
          Superterm of <SubTerm> must be an equivalence.
	  Along the path to SubTerm there are only quantifiers or disjunctions.
	  All free variables in the equivalence are free variables
	  in <SubTerm>.
	  All free variables in <SubTerm> are bound by a universal quantifier
	  (with polarity 1).
  RETURN: The destructively changed <TopTerm>.
  EFFECT: Removes all quantifiers not binding a variable in <SubTerm>
          from <subTerm>'s path.
          Moves all universal quantifiers binding free variable
	  in <SubTerm> up.
	  <TopTerm> is transformed into the form
	  forall([X1,...,Xn],or (equiv(<SubTerm>,psi),phi)).
**********************************************************/
{
  TERM Term1, Term2, Flat, Variable;
  LIST Scan1, Scan2, FreeVars;


#ifdef CHECK
  if (!fol_CheckFormula(TopTerm) || !term_HasPointerSubterm(TopTerm, SubTerm)) {
    misc_StartErrorReport();
    misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal input.");
    misc_FinishErrorReport();
  }
#endif

  TopTerm = cnf_SimplifyQuantors(TopTerm);
  term_AddFatherLinks(TopTerm);
  Term1   = term_Superterm(SubTerm);

  while (Term1 != TopTerm) {

    while (symbol_Equal(fol_Or(), term_TopSymbol(Term1)) && (TopTerm != Term1)) {
      Term1 = term_Superterm(Term1);
    }
    if (fol_IsQuantifier(term_TopSymbol(Term1))) {
      Flat  = term_SecondArgument(Term1);
      Flat  = cnf_Flatten(Flat, fol_Or());
      Scan1 = fol_QuantifierVariables(Term1);
      while (!list_Empty(Scan1)) {
	Variable = (TERM)list_Car(Scan1);
	if (fol_VarOccursFreely(Variable, SubTerm)) {
	  Scan2 = list_Cdr(Scan1);
	  fol_DeleteQuantifierVariable(Term1, term_TopSymbol(list_Car(Scan1)));
	  Scan1 = Scan2;
	}
	else {
	  Scan1 = list_Cdr(Scan1);
	}
      }
      if (fol_IsQuantifier(term_TopSymbol(Term1))) {
	/* still variables, but not binding a variable in the equivalence term */
	LIST ArgList;

	term_RplacArgumentList(Flat, list_PointerDeleteOneElement(term_ArgumentList(Flat), SubTerm));
	ArgList = term_ArgumentList(Term1);
       	term_RplacArgumentList(Term1, list_Nil());
	Term2 = term_Create(term_TopSymbol(Term1), ArgList);
	term_RplacArgumentList(Term1, list_Cons(SubTerm, list_List(Term2)));
	term_RplacTop(Term1, fol_Or());
	Scan1 = term_ArgumentList(Term1); 
	while (!list_Empty(Scan1)) {
	  term_RplacSuperterm((TERM)list_Car(Scan1), Term1);
	  Scan1 = list_Cdr(Scan1);
	}
      }
    }
    else {

#ifdef CHECK
      if (!symbol_Equal(term_TopSymbol(Term1), fol_Or())) {
	misc_StartErrorReport();
	misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal term Term1");
	misc_FinishErrorReport();
      }
#endif

      Term1 = cnf_Flatten(Term1, fol_Or());
    }
  }
  FreeVars = fol_FreeVariables(Term1);
  if (!list_Empty(FreeVars)) {
    term_CopyTermsInList(FreeVars);
    TopTerm = fol_CreateQuantifier(fol_All(), FreeVars, list_List(Term1));
  }
  return TopTerm;
}


TERM cnf_DefConvert(TERM Def, TERM FoundPredicate, TERM* ToProve)
/*********************************************************
  INPUT:   A term Def which is an equivalence (P(x1,..,xn) <=> Formula)
           that can be converted to standard form.
           The subterm that holds the defined predicate.
           A pointer to a term ToProve into which a term is stored
	   that has to be proved before applying the definition.
  RETURNS: The converted definition : forall([..], or(equiv(..,..), ..))
************************************************************/
{
  TERM orterm;

#ifdef CHECK
  fol_CheckFatherLinks(Def);
#endif
  
  Def = cnf_RemoveImplFromFormulaPath(Def, FoundPredicate);   /* Remove implications along the path */
  Def = cnf_NegationNormalFormulaPath(Def, FoundPredicate);   /* Move not's as far down as possible */

#ifdef CHECK
  if (!fol_CheckFormula(Def)) {
    misc_StartErrorReport();
    misc_ErrorReport("\nIn cnf_DefConvert: Illegal input Formula.\n");
    misc_FinishErrorReport();
  }
  if (!term_HasPointerSubterm(Def, FoundPredicate)) {
    misc_StartErrorReport();
    misc_ErrorReport("\nIn cnf_DefConvert: Illegal input SubTerm.\n");
    misc_FinishErrorReport();
  }
#endif

  Def = cnf_RemoveQuantFromPathAndFlatten(Def, term_Superterm(FoundPredicate));
  term_AddFatherLinks(Def);

#ifdef CHECK
  if (!fol_CheckFormula(Def)) {
    misc_StartErrorReport();
    misc_ErrorReport("\nIn cnf_DefConvert: Illegal term Def.");
    misc_FinishErrorReport();
  }
  if (!term_HasPointerSubterm(Def, FoundPredicate)) {
    misc_StartErrorReport();
    misc_ErrorReport("\nIn cnf_DefConvert: Illegal term FoundPredicate.");
    misc_FinishErrorReport();
  }
#endif

  /* Find top level or() */
  if (symbol_Equal(term_TopSymbol(Def), fol_All())) {
    /* Make sure there are several arguments */
    if (symbol_Equal(term_TopSymbol(term_SecondArgument(Def)), fol_Or()) &&
	(list_Length(term_ArgumentList(term_SecondArgument(Def))) == 1)) {
      TERM t;
      t = term_SecondArgument(Def);
      term_RplacSecondArgument(Def, term_FirstArgument(term_SecondArgument(Def)));
      term_Free(t);
      orterm = NULL;
      term_RplacSuperterm(term_SecondArgument(Def), Def);
    }
    else 
      orterm = term_SecondArgument(Def);
  }
  else {
    /* Make sure there are several arguments */
    if (symbol_Equal(term_TopSymbol(Def), fol_Or()) &&
	(list_Length(term_ArgumentList(Def)) == 1)) {
      TERM t;
      t = Def;
      Def = term_FirstArgument(Def);
      term_Free(t);
      orterm = NULL;
      term_RplacSuperterm(term_SecondArgument(Def), Def);
    }
    else 
      orterm = Def;
  }

  /* If there is something to prove */
  if (orterm != (TERM) NULL) {
    TERM equiv;
    LIST args;

    equiv = (TERM) NULL;

    /* In pell 10 there are no conditions for the equivalence */
    if (symbol_Equal(term_TopSymbol(orterm), fol_Equiv())) {
      equiv = orterm;
      *ToProve = NULL;
    }
    else {
      TERM t;
      /* First find equivalence term among arguments */
      args  = term_ArgumentList(orterm);
      equiv = term_Superterm(FoundPredicate);
      
      /* Delete equivalence from list */
      args = list_PointerDeleteElement(args, equiv);
      term_RplacArgumentList(orterm, args);
      
      /* ToProve consists of all the definitions arguments except the equivalence */
      *ToProve = term_Copy(orterm);
      
      /* Now not(*ToProve) implies the equivalence */
      /* Negate *ToProve */
      *ToProve = term_Create(fol_Not(), list_List(*ToProve));
      *ToProve = cnf_NegationNormalFormula(*ToProve);
      term_AddFatherLinks(*ToProve);

      /* Now convert definition to implication form */
      term_RplacTop(orterm, fol_Implies());
      t = term_Create(fol_Not(), 
		      list_List(term_Create(fol_Or(), 
					    term_ArgumentList(orterm))));
      term_RplacArgumentList(orterm, list_Cons(t, list_List(equiv)));

      Def = cnf_NegationNormalFormula(Def);
      term_AddFatherLinks(Def);
    }    
  }
  
#ifdef CHECK
  fol_CheckFatherLinks(Def);
#endif
  return Def;
}


LIST cnf_HandleDefinition(PROOFSEARCH Search, LIST Pair, LIST Axioms,
			  LIST Sorts, LIST Conjectures)
/*******************************************************************
  INPUT:   A PROOFSEARCH object, a pair (label, term) and 3 lists of pairs.
           If the term in pair is a definition, the defined predicate
	   is expanded in all the lists
           and added to the proofsearch object.
  RETURNS: The pair with the converted definition:
           forall([..], or(equiv(..,..), .......))
********************************************************************/
{
  TERM definition, defpredicate, equivterm;
  
  BOOL alwaysapplicable;     /* Is set to TRUE iff the definition can always be applied */
  FLAGSTORE Flags;
  PRECEDENCE Precedence;

  Flags      = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  /* The axiomlist consists of (label, formula) pairs */
  definition = list_PairSecond(Pair);
  
  /* Test if Definition contains a definition */
  defpredicate = (TERM) NULL;
  if (cnf_ContainsDefinition(definition, &defpredicate)) { 
    TERM toprove;
    LIST allformulae, scan;

    /* Create list of all formula pairs */
    /* Check if definition may be applied to each formula */
    allformulae = list_Copy(Axioms);
    allformulae = list_Nconc(allformulae, list_Copy(Sorts));
    allformulae = list_Nconc(allformulae, list_Copy(Conjectures));
#ifdef CHECK
    for (scan=allformulae; !list_Empty(scan); scan=list_Cdr(scan)) {
      if (!list_Empty((LIST) list_Car(scan))) {
	if (!term_IsTerm((TERM) list_PairSecond((LIST) list_Car(scan))))
	  fol_CheckFatherLinks((TERM) list_PairSecond((LIST) list_Car(scan)));
      }
    }
#endif
    
    /* Convert definition to standard form */
    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
      fputs("\nPredicate : ", stdout);
      symbol_Print(term_TopSymbol(defpredicate));
    }

    definition = cnf_DefConvert(definition, defpredicate, &toprove);
    if (toprove == NULL)
      alwaysapplicable = TRUE;
    else 
      alwaysapplicable = FALSE;

    prfs_SetDefinitions(Search, list_Cons(term_Copy(definition), 
					  prfs_Definitions(Search)));
    
    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
      if (alwaysapplicable) {
	fputs("\nAlways Applicable     : ", stdout);
	fol_PrettyPrint(definition); 
      } 
    }

    /* Definition is converted to a form where the equivalence is
       the first argument of the disjunction */
    equivterm     = term_SecondArgument(term_Superterm(defpredicate));
    
    
    scan = allformulae;
    while (!list_Empty(scan)) {
      BOOL localfound;
      LIST pair, targettermvars;
      
      /* Pair label / term */
      pair = list_Car(scan);

      /* Pair may be NULL if it is a definition that could be deleted */
      if ((pair != NULL) && (definition != (TERM) list_PairSecond(pair))) {
	TERM target, targetpredicate, totoplevel;
	LIST varsfortoplevel;
	target = (TERM) list_PairSecond(pair);
	targettermvars = varsfortoplevel = list_Nil();
	
	/* If definition is not always applicable, check if it is applicable
	   for this formula */
	localfound = FALSE;
	if (!alwaysapplicable) {
	  if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate),
				    &targetpredicate, &totoplevel,
				    &targettermvars, &varsfortoplevel)) {
	    TERM toprovecopy;
	    toprovecopy = term_Copy(toprove);
	    target = cnf_DefTargetConvert(target, totoplevel, toprovecopy,
					  term_ArgumentList(defpredicate),
					  term_ArgumentList(targetpredicate),
					  targettermvars, varsfortoplevel,
					  Flags, Precedence, &localfound);
	    list_Delete(targettermvars);
	    list_Delete(varsfortoplevel);
	    targettermvars = varsfortoplevel = list_Nil();
	    
	    list_Rplacd(pair, (LIST) target);
	    if (localfound)
	      list_Rplacd(pair, 
			  (LIST) cnf_ApplyDefinitionOnce(defpredicate, 
							 equivterm,
							 list_PairSecond(pair),
							 targetpredicate,
							 Flags));
	  }
	}
	else {
	  if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate), 
				    &targetpredicate, &totoplevel,
				    &targettermvars, &varsfortoplevel))
	    list_Rplacd(pair, (LIST) cnf_ApplyDefinitionOnce(defpredicate, 
							     equivterm,
							     list_PairSecond(pair),
							     targetpredicate,
							     Flags));
	  else
	    scan = list_Cdr(scan);
	  list_Delete(targettermvars);
	  list_Delete(varsfortoplevel);
	  targettermvars = varsfortoplevel = list_Nil();
	}
      }
      else
	scan = list_Cdr(scan);
    }
    list_Delete(allformulae);
    /* toprove can be NULL if the definition can always be applied */
    if (toprove != (TERM) NULL)
      term_Delete(toprove);
    list_Rplacd(Pair, (LIST) definition);
  }
 
  return Pair;
}


LIST cnf_ApplyDefinitionToClause(CLAUSE Clause, TERM Predicate, TERM Expansion,
				 FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A clause, two terms and a flag store and a precedence.
  RETURNS: The list of clauses where each occurrence of Predicate is 
           replaced by Expansion.
***************************************************************/
{
  NAT  i;
  BOOL changed;
  LIST args, scan, symblist;
  TERM clauseterm, argument;

  changed = FALSE;
  
  /* Build term from clause */
  args = list_Nil();
  for (i = 0; i < clause_Length(Clause); i++) {
    argument = clause_GetLiteralTerm(Clause, i); /* with sign */
    args     = list_Cons(term_Copy(argument), args);
  }
  clauseterm = term_Create(fol_Or(), args);

  for (scan=term_ArgumentList(clauseterm); !list_Empty(scan); scan=list_Cdr(scan)) {
    BOOL isneg;

    argument = (TERM) list_Car(scan);
    if (symbol_Equal(term_TopSymbol(argument), fol_Not())) {
      argument = term_FirstArgument(argument);
      isneg = TRUE;
    }
    else 
      isneg = FALSE;
      
    /* Try to match with predicate */
    cont_StartBinding();
    if (unify_Match(cont_LeftContext(), Predicate, argument)) {
      SUBST subst;
      TERM  newargument;
      subst = subst_ExtractMatcher();
      newargument = subst_Apply(subst, term_Copy(Expansion));
      subst_Free(subst);
      if (isneg)
	newargument = term_Create(fol_Not(), list_List(newargument));
      term_Delete((TERM) list_Car(scan));
      list_Rplaca(scan, newargument);
      changed = TRUE;
    }      
    cont_BackTrack();
  }

  if (changed) {
    /* Build term and derive list of clauses */
    LIST result;
    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
      puts("\nClause before applying def :");
      clause_Print(Clause);
      puts("\nPredicate :");
      fol_PrettyPrint(Predicate);
      puts("\nExpansion :");
      fol_PrettyPrint(Expansion);
    }
    symblist   = list_Nil();
    clauseterm = cnf_Cnf(clauseterm, Precedence, &symblist);
    result     = cnf_MakeClauseList(clauseterm,FALSE,FALSE,Flags,Precedence);
    list_Delete(symblist);
    term_Delete(clauseterm);
    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
      LIST l;
      puts("\nClauses derived by expanding definition :");
      for (l = result; !list_Empty(l); l=list_Cdr(l)) {
	clause_Print((CLAUSE) list_Car(l));
	fputs("\n", stdout);
      }
    }
    return result;
  }
  else {
    term_Delete(clauseterm);
    return list_Nil();
  }
}


BOOL cnf_PropagateSubstEquations(TERM StartTerm)
/*************************************************************
  INPUT:   A term where we assume that father links are established and
           that no variable is bound by more than one quantifier.
  RETURNS: TRUE, if any substitutions were made, FALSE otherwise.
  EFFECT:  Function looks for equations of the form x=t where x does not
           occur in t. If x=t occurs negatively and disjunctively below
	   a universal quantifier binding x or if x=t occurs positively and
	   conjunctively below an existential quantifier binding x,
           all occurrences of  x are replaced by t in <StartTerm>.
**************************************************************/
{
  LIST   Subequ;
  TERM   QuantorTerm, Equation, EquationTerm;
  SYMBOL Variable;
  BOOL   Hit, Substituted;

#ifdef CHECK
  if (fol_VarBoundTwice(StartTerm)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cnf_PropagateSubstEquations: Variables of");
    misc_ErrorReport("\n input term are not normalized.");
    misc_FinishErrorReport();
  }
#endif

  Substituted = FALSE;

  Subequ = fol_GetSubstEquations(StartTerm);
  for ( ; !list_Empty(Subequ); Subequ = list_Pop(Subequ)) {
    Hit          = FALSE;
    Equation     = list_Car(Subequ);
    Variable     = symbol_Null();
    QuantorTerm  = term_Null();
    EquationTerm = term_Null();

    if (term_IsVariable(term_FirstArgument(Equation)) &&
	!term_ContainsVariable(term_SecondArgument(Equation),
			       term_TopSymbol(term_FirstArgument(Equation)))) {

      Variable     = term_TopSymbol(term_FirstArgument(Equation));
      QuantorTerm  = fol_GetBindingQuantifier(Equation, Variable);
      EquationTerm = term_SecondArgument(Equation);
      Hit          = fol_PolarCheck(Equation, QuantorTerm);
    }
    if (!Hit && term_IsVariable(term_SecondArgument(Equation)) &&
	!term_ContainsVariable(term_FirstArgument(Equation),
			       term_TopSymbol(term_SecondArgument(Equation)))) {

      Variable     = term_TopSymbol(term_SecondArgument(Equation));
      QuantorTerm  = fol_GetBindingQuantifier(Equation, Variable);
      EquationTerm = term_FirstArgument(Equation);
      Hit          = fol_PolarCheck(Equation, QuantorTerm);
    }
    if (Hit) {
      fol_DeleteQuantifierVariable(QuantorTerm,Variable);
      term_ReplaceVariable(StartTerm, Variable, EquationTerm); /* We replace everythere ! */
      term_AddFatherLinks(StartTerm);
      if (symbol_Equal(term_TopSymbol(QuantorTerm),fol_Equality())) /* Trivial Formula */
	fol_SetTrue(QuantorTerm);
      else
	fol_SetTrue(Equation);
      Substituted = TRUE;
    }   
  }

  /* <Subequ> was freed in the loop. */

  return Substituted;
}