path: root/test/spass/proofcheck.c

/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *             PROOF CHECKING                             * */
/* *                                                        * */
/* *  Copyright (C) 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 "proofcheck.h"


/* options */
int        pcheck_Timelimit;
const char *pcheck_ProofFileSuffix;
BOOL       pcheck_Quiet;

/* options for graph generation */
BOOL        pcheck_ClauseCg;
BOOL        pcheck_GenNamedCg, pcheck_GenRedCg;
const char  *pcheck_CgName, *pcheck_RedCgName;
GRAPHFORMAT pcheck_GraphFormat;


static int pcheck_MaxSplitLevel(LIST Clauses)
/**************************************************************
  INPUT:   A list of clauses.
  RETURNS: The maximum split level of a clause.
***************************************************************/
{
  int Max;
  int Act;
  
  Max = 0;
  while (!list_Empty(Clauses)) {
    Act = clause_SplitLevel(list_Car(Clauses));
    if (Act > Max) 
      Max = Act;
    Clauses = list_Cdr(Clauses);
  }
  return Max;
}


static __inline__ int pcheck_MaxParentSplitLevel(CLAUSE Clause) 
/**************************************************************
  INPUT:   A clause
  RETURNS: The max split level of the parent clauses
***************************************************************/
{
  return pcheck_MaxSplitLevel(clause_ParentClauses(Clause));
}


static BOOL pcheck_ClauseIsFromLeftSplit(CLAUSE Clause)
/**************************************************************
  INPUT  : A Clause                                                      
  RETURNS: TRUE iff the clause is the left half of a split
  CAUTION: This works also for clauses without parents, since
           pcheck_MaxParentSplitLevel returns 0 in that case.
***************************************************************/
{
  return (clause_SplitLevel(Clause) > pcheck_MaxParentSplitLevel(Clause));
}


static BOOL pcheck_ClauseIsFromRightSplit(CLAUSE Clause)
/**************************************************************
  INPUT:   A clause
  RETURNS: TRUE iff the clause is from the right half of a split
***************************************************************/
{
  if (list_Empty(clause_ParentClauses(Clause)))
    return FALSE;

  return clause_IsEmptyClause(list_Car(clause_ParentClauses(Clause)));
}

static BOOL pcheck_ClauseIsFromSplit(CLAUSE Clause)
/**************************************************************
 INPUT  : A clause
 RETURNS: TRUE iff the clause is from a split
***************************************************************/
{
  return (pcheck_ClauseIsFromRightSplit(Clause) ||
	  pcheck_ClauseIsFromLeftSplit(Clause));
}


static int pcheck_LabelToNumber(const char* Label)
/**************************************************************
  INPUT:   A clause label
  RETURNS: The label converted to a number.
  EFFECT:  If the conversion fails an error message is printed
           and the program exits.
***************************************************************/
{
  int Number;

  if (!string_StringToInt(Label, FALSE, &Number)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n In pcheck_LabelToNumber:");
    misc_UserErrorReport(" Could not convert clause");
    misc_UserErrorReport(" label %s to a number.\n", Label);
    misc_FinishUserErrorReport();
  }

  return Number;
}


static int pcheck_CompareNumberAndClause(const void* Number, const void* ClausePtr)
/**************************************************************
  INPUT:   A number and a pointer to a CLAUSE.
  RETURNS: 1) a negative number if <number> is < number of <Clause>
           2) 0 if <Number> is equal to the number of <Clause>
           3) a positive number if <Number> is > number of <Clause>
  EFFECT:  This function is used as parameter to the bsearch function.
***************************************************************/
{
  return (int)Number - clause_Number(*(const CLAUSE*)ClausePtr);
}


static void pcheck_ParentNumbersToPointersInVector(CLAUSE* ClauseVector, int Size)
/**************************************************************
  INPUT:   A clause vector without duplicate clauses and the maximal
           number of elements in the vector
  EFFECTS: All clause parent numbers are replaced by pointers
           to the parents.
  CAUTION: The clause vector has to be sorted by increasing
           clause numbers, since this function performs a binary search
           on the vector.
***************************************************************/
{
  int     Position;
  LIST    NewParents, OldParents;
  LIST    ScanParents;
  int     ParentNum;
  CLAUSE* Parent;
  
  for (Position = 0; Position < Size; Position++)  {
    OldParents = clause_ParentClauses(ClauseVector[Position]);
    NewParents = list_Copy(OldParents);
    
    for (ScanParents = NewParents; !list_Empty(ScanParents); ScanParents = list_Cdr(ScanParents)) {     
      ParentNum = (int)list_Car(ScanParents);
      /* Binary search for parent clause with number <ParentNum>. */
      Parent = bsearch((const void*)ParentNum, ClauseVector, Size,
		       sizeof(CLAUSE), pcheck_CompareNumberAndClause);
      if (Parent != NULL)
	list_Rplaca(ScanParents, *Parent);  
      else {
	misc_StartUserErrorReport();
	misc_UserErrorReport("\n Error: Missing parent clause %d of clause %d.\n", 
			     ParentNum, clause_Number(ClauseVector[Position]));
	misc_FinishUserErrorReport();
      }
    }    
    clause_SetParentClauses(ClauseVector[Position], NewParents);
    list_Delete(OldParents); 
  }
}


static LIST pcheck_ForceParentNumbersToPointersInVector(CLAUSE* ClauseVector,
							int Size)
/**************************************************************
  INPUT:   A clause vector, possibly with duplicates
  RETURNS: All numbers of clauses <c> that are missing a parent clause
           from the transitive hull of parent clauses of <c>.
  EFFECTS: All MARKED and HIDDEN flags of the clauses are changed.
           All parent numbers are converted to pointers, if the
           parents exist, otherwise the parent number is deleted
           from the list.
           The parent literal list is changed accordingly.
           A clause <c> is marked as HIDDEN, if any clause
           from the transitive hull of parent clauses of <c>
           was missing in <ClauseVector>.
***************************************************************/
{
  int     Position;
  LIST    NewParents, NewPLits, Parents, PLits, Missing;
  int     ParentNum, PLitNum;
  CLAUSE  *Parent, Clause;

  Missing = list_Nil();

  for (Position = 0; Position < Size; Position++) {
    clause_RemoveFlag(ClauseVector[Position], MARKED); 
    clause_RemoveFlag(ClauseVector[Position], HIDDEN);
  }

  for (Position = 0; Position < Size; Position++)  {
    Clause = ClauseVector[Position];
    if (!clause_GetFlag(Clause, MARKED)) { 
      clause_SetFlag(Clause, MARKED);
      Parents    = clause_ParentClauses(Clause);
      PLits      = clause_ParentLiterals(Clause);
      NewParents = list_Nil();
      NewPLits   = list_Nil();

      while (!list_Empty(Parents)) {
	ParentNum = (int)list_Car(Parents);
	PLitNum   = (int)list_Car(PLits);
	/* Binary search for parent clause with number <ParentNum>. */
	Parent = bsearch((const void*)ParentNum, ClauseVector, Size,
			 sizeof(CLAUSE), pcheck_CompareNumberAndClause);
	if (Parent == NULL) {
	  Missing = list_Cons((POINTER)ParentNum, Missing); 
	  clause_SetFlag(Clause, HIDDEN);
	} else {
	  if (clause_GetFlag(*Parent, HIDDEN))
	    clause_SetFlag(Clause, HIDDEN);
	  NewParents  = list_Cons((POINTER)*Parent, NewParents);
	  NewPLits    = list_Cons((POINTER)PLitNum, NewPLits);
	}
	Parents = list_Cdr(Parents); 
	PLits   = list_Cdr(PLits);
      }
      list_Delete(clause_ParentClauses(Clause));
      list_Delete(clause_ParentLiterals(Clause));
      NewParents = list_NReverse(NewParents);
      NewPLits   = list_NReverse(NewPLits);
      clause_SetParentClauses(Clause, NewParents);
      clause_SetParentLiterals(Clause, NewPLits);
    } /* if clause is not marked */
  } /* for all clauses */
 
  return Missing;
}


static int pcheck_CompareClauseNumber(const void* C1, const void* C2)
/**************************************************************
  INPUT  : Two pointers to CLAUSEs.
  RETURNS: 1) a negative number if the number of C1 is < number of C2.
           2) 0 if C1 and C2 have the same clause number
              (that means a possible bug in SPASS)
           3) a positive number if number of C1 > number of C2
  EFFECT:  This function is used as parameter to the qsort function.
************************************************************/
{
  return clause_Number(*(const CLAUSE*)C1) - clause_Number(*(const CLAUSE*)C2);
}


static LIST pcheck_ConvertParentsInList(LIST List)
/**************************************************************
  INPUT:   A list of clauses.
  RETURNS: The list of missing parent clause numbers from the list 
  EFFECTS: Parent numbers are converted to pointers
***************************************************************/
{
  int     Size, Index;
  CLAUSE* ClauseVector;
  LIST    Missing;

  Size = list_Length(List);
  if (Size == 0)
    return list_Nil();

  /* convert list into vector for binary search */
  ClauseVector = (CLAUSE*)memory_Malloc(sizeof(CLAUSE) * Size);
  for (Index = 0; !list_Empty(List); List = list_Cdr(List), Index++)
    ClauseVector[Index] = list_Car(List);

  /* sort the clauses in vector by increasing clause number */
  qsort(ClauseVector, Size, sizeof(CLAUSE), pcheck_CompareClauseNumber);

  /* convert parent lists */
  Missing = pcheck_ForceParentNumbersToPointersInVector(ClauseVector, Size);
  
  memory_Free(ClauseVector, sizeof(CLAUSE) * Size);
  return Missing;
}


LIST pcheck_ConvertParentsInSPASSProof(PROOFSEARCH Search, LIST EmptyClauses) 
/**************************************************************
  INPUT  : A proofsearch object with clauses sorted by weight
           and an unsorted list <EmptyClauses>
  RETURNS: The lists, where the clauses in <EmptyClauses> are
           now sorted by weight, and parent numbers
           in the clauses are replaced by parent pointers
***************************************************************/
{
  LIST    AllLists; 
  LIST    Missing;

  AllLists = list_Nconc(list_Copy(prfs_DocProofClauses(Search)),
			list_Copy(EmptyClauses));
  AllLists = list_Nconc(list_Copy(prfs_UsableClauses(Search)), AllLists);
  AllLists = list_Nconc(list_Copy(prfs_WorkedOffClauses(Search)), AllLists);
  
  AllLists = pcheck_ClauseNumberMergeSort(AllLists);
  Missing  = pcheck_ConvertParentsInList(AllLists);
  list_Delete(AllLists);

  return Missing;
}


static LIST pcheck_ParentNumbersToParents(LIST Proof)
/**************************************************************
  INPUT:   A list of clauses, representing a proof.
  RETURNS: The list, where parent numbers in the
           parent list of clauses are replaced
           by the parents (pointers).
  CAUTION: For finding the clause corresponding to a
           a clause number, the <Proof> list is searched
	   with binary search. This is correct only if
	   the clause numbers in <Proof> are increasing.
************************************************************/
{
  LIST    ScanClauses;
  int     ProofLength, Position;
  CLAUSE* ClauseVector;

  if (list_Empty(Proof))
    return list_Nil();

  /* convert list into vector for binary search */
  ProofLength  = list_Length(Proof);
  ClauseVector = (CLAUSE*) memory_Malloc(ProofLength * sizeof(CLAUSE));

  for (ScanClauses = Proof, Position = 0; !list_Empty(ScanClauses);
       ScanClauses = list_Cdr(ScanClauses), Position++) {
    ClauseVector[Position] = list_Car(ScanClauses);
  }

  /* sort the clauses in vector by increasing clause number */
  qsort(ClauseVector, ProofLength, sizeof(CLAUSE), pcheck_CompareClauseNumber);
 
  /* convert parent lists */
  pcheck_ParentNumbersToPointersInVector(ClauseVector, ProofLength);
 
  memory_Free(ClauseVector, ProofLength * sizeof(CLAUSE));

  return Proof;
}


LIST pcheck_ParentPointersToParentNumbers(LIST Clauses)
/**************************************************************
 INPUT  : A list of clauses                                                      
 RETURNS: The list with parent pointers replaced by
          parent numbers
 EFFECTS: Sets marks on all clauses.                            
***************************************************************/
{
  LIST ScanClauses;
  LIST ScanParents;

  pcheck_ClauseListRemoveFlag(Clauses, MARKED);

  for (ScanClauses = Clauses; !list_Empty(ScanClauses); ScanClauses = list_Cdr(ScanClauses)) {
    if (!clause_GetFlag(list_Car(ScanClauses), MARKED)) {
      for (ScanParents = clause_ParentClauses(list_Car(ScanClauses)); !list_Empty(ScanParents);
	   ScanParents = list_Cdr(ScanParents))
	list_Rplaca(ScanParents, (POINTER)clause_Number(list_Car(ScanParents))); 
      clause_SetFlag(list_Car(ScanClauses), MARKED);
    }
  }
  return Clauses;
}


LIST pcheck_ConvertTermListToClauseList(LIST ProofRest, FLAGSTORE Flags,
					PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A list of quintupels (lists) representing a proof,
           a flag store, and a precedence.
  RETURNS: The conversion of this list into the internal clause
           structure. For each clause, the numbers of parent
	   clauses are replaced by pointers to the parents.
***************************************************************/
{
  LIST    Clauses;
  LIST    ProofLine;
  TERM    ClauseTerm;
  CLAUSE  Clause;
  int     Level;
  int     ClauseNumber;
  LIST    ParentLabels;
  LIST    ParentIds;     
  LIST    ParentLits;    /* this is a dummy list; parent lits are not yet specified in a SPASS proof */
  RULE    Origin;
  char*   ClauseLabel;

  Clauses = list_Nil();  /* result */

  while (!list_Empty(ProofRest)) {    
    /* break proof line into components */
    ProofLine     = list_Car(ProofRest);
    
    ClauseLabel   = list_First(ProofLine);
    ClauseTerm    = list_Second(ProofLine);    
    /* replace by NULL clause, since dfg_CreateClauseFromTerm deletes clause ! */
    list_Rplaca(list_Cdr(ProofLine), clause_Null()); 
    ParentLabels  = (LIST)list_Third(ProofLine);
    Level         = (int)list_Fourth(ProofLine);
    Origin        = (RULE)list_Fifth(ProofLine);

    /* Conversion */
    Clause       = dfg_CreateClauseFromTerm(ClauseTerm, TRUE, Flags,Precedence);
    /* It's necessary to update the weight since dfg_CreateClauseFromTerm */
    /* doesn't set it. */
    clause_UpdateWeight(Clause, Flags);
    ClauseNumber = pcheck_LabelToNumber(ClauseLabel);
    ParentIds    = list_Nil();
    ParentLits   = list_Nil();

    while (!list_Empty(ParentLabels)) {
      ParentIds  = list_Cons((POINTER)pcheck_LabelToNumber(list_Car(ParentLabels)), ParentIds); 
      ParentLits = list_Cons(0, ParentLits);
      ParentLabels   = list_Cdr(ParentLabels);
    }
    
    /* set all data */
    clause_SetNumber(Clause, ClauseNumber);
    ParentIds = list_NReverse(ParentIds);
    clause_SetParentClauses(Clause, ParentIds);
    clause_SetParentLiterals(Clause, ParentLits);
    Clause->origin = Origin;

    clause_SetSplitLevel(Clause, Level); 
    if (Level > 0) {
      clause_ClearSplitField(Clause);
      clause_SetSplitFieldBit(Clause, Level);
    } else 
      clause_SetSplitField(Clause, (SPLITFIELD)NULL,0);

    clause_RemoveFlag(Clause, MARKED);
    Clauses   = list_Cons(Clause, Clauses);
    ProofRest = list_Cdr(ProofRest);  
  }
  Clauses = list_NReverse(Clauses);
  
  /* convert parent numbers to pointers */
  Clauses = pcheck_ParentNumbersToParents(Clauses);
  
  return Clauses;
}


static BOOL pcheck_ClauseIsUnmarked(CLAUSE C)
/**************************************************************
  INPUT:   A clause
  RETURNS: The value of the clauses MARKED flag
***************************************************************/
{
  return !clause_GetFlag(C, MARKED);
}


static void pcheck_RemoveUnmarkedFromTableau(TABLEAU T)
/**************************************************************
  INPUT:   A tableau
  RETURNS: Nothing.
  EFFECTS: Delete all clauses that have the MARKED flag
           set from tableau.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  tab_SetClauses(T, list_DeleteElementIf(tab_Clauses(T),
					 (BOOL (*)(POINTER))pcheck_ClauseIsUnmarked));
  
  pcheck_RemoveUnmarkedFromTableau(tab_LeftBranch(T));
  pcheck_RemoveUnmarkedFromTableau(tab_RightBranch(T));
}


static void pcheck_CollectUnmarkedSplits(TABLEAU T, LIST* Splits)
/**************************************************************
  INPUT:   A tableau, a list of clauses by reference
  RETURNS: Nothing.
  EFFECTS: Add all split clauses in the tableau that are not
           marked to the <Splits> list.
***************************************************************/
{
  LIST Scan;

  if (tab_IsEmpty(T))
    return;

  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (!clause_GetFlag(list_Car(Scan), MARKED) && clause_IsFromSplitting(list_Car(Scan))) 
      (*Splits) = list_Cons(list_Car(Scan), *Splits);
  }
  
  pcheck_CollectUnmarkedSplits(tab_LeftBranch(T), Splits);
  pcheck_CollectUnmarkedSplits(tab_RightBranch(T), Splits);
}


/* EK: unused, only recursive */
static void pcheck_TableauSplitsComplete(TABLEAU T)
/**************************************************************
  INPUT  : A tableau
  RETURNS: Checks that every split has exactly two or no
           successors. This condition must be true after
           tab_RemoveRedundantSplits has been called.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  if (tab_RightBranchIsEmpty(T) && !tab_LeftBranchIsEmpty(T)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Split of clause %d has no right branch.\n", 
			 clause_Number(tab_SplitClause(T)));
    misc_FinishUserErrorReport();
  }
 
  if (!tab_RightBranchIsEmpty(T) && tab_LeftBranchIsEmpty(T)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Split of clause %d has no left branch.\n", 
			 clause_Number(tab_SplitClause(T)));
    misc_FinishUserErrorReport();
  }
  
  pcheck_TableauSplitsComplete(tab_LeftBranch(T));
  pcheck_TableauSplitsComplete(tab_RightBranch(T));
}


static void pcheck_RightSplitParents(CLAUSE SplitClause, CLAUSE RightSplitClause,
				     CLAUSE LeftSplitClause)
/**************************************************************
  INPUT:   A split clause, and its left and right successors
  EFFECTS: Prints an error message if the split is not correctly
           closed.
***************************************************************/
{
  LIST Scan;
  BOOL HasEmpty, ContainsSplitClause;

  HasEmpty = ContainsSplitClause = FALSE;

  for (Scan = clause_ParentClauses(RightSplitClause);
       !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (clause_IsEmptyClause(list_Car(Scan)))
      HasEmpty = TRUE;
    if (clause_Number(list_Car(Scan)) == clause_Number(SplitClause)) 
      ContainsSplitClause = TRUE; 
  }
  
  if (!HasEmpty) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Right split clause %d has no empty clause as parent.\n", 
			 clause_Number(SplitClause));
    misc_FinishUserErrorReport();
  }

  if (!ContainsSplitClause) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Right split clause %d", clause_Number(SplitClause));
    misc_UserErrorReport(" does not have its split parent as parent clause.\n");
    misc_FinishUserErrorReport();
  }
}



/* EK: unused, only recursive */
static void pcheck_SplitFormats(TABLEAU T)
/**************************************************************
  INPUT  : A tableau
  RETURNS: TRUE iff all splits:
           - have generated negations of the left split clause
 	     if the left split clause is ground
	   - the conditions for right split clauses are
             as demanded in pcheck_RightSplitParents
***************************************************************/
{
  LIST Scan;

  if (tab_IsEmpty(T))
    return;

  /* for right splits, check that parents have an empty clause */
  /* and the split clause as a parent */

  for (Scan = tab_RightSplitClauses(T); !list_Empty(Scan);
       Scan = list_Cdr(Scan)) {
    pcheck_RightSplitParents(tab_SplitClause(T), list_Car(Scan),
			     tab_LeftSplitClause(T));
  }
    
  pcheck_SplitFormats(tab_RightBranch(T));
  pcheck_SplitFormats(tab_LeftBranch(T));
}


static void pcheck_SplitLevels(TABLEAU T)
/**************************************************************
  INPUT  : A Tableau
  RETURNS: TRUE iff all clauses in the tableau that
           are not splitting clauses have the max split
    	   level of their parents.
  CAUTION: We assume that <T> has correct and complete split
           entries. See pcheck_SplitToProblems.
***************************************************************/
{
  LIST   Scan;
  CLAUSE Clause;
  int    CorrectLevel;

  if (tab_IsEmpty(T))
    return;

  /* check split levels */
  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    Clause = list_Car(Scan);
    if (!list_Empty(clause_ParentClauses(Clause))
	&& !clause_IsFromSplitting(Clause)) {
 
     CorrectLevel = pcheck_MaxParentSplitLevel(Clause);
     if (clause_SplitLevel(Clause) != CorrectLevel) {
       misc_StartUserErrorReport();
       misc_UserErrorReport("\n Error: Split level of clause %d should be %d.\n",
			    clause_Number(Clause), CorrectLevel);
       misc_FinishUserErrorReport();
     }
    }
  }

  pcheck_SplitLevels(tab_RightBranch(T));
  pcheck_SplitLevels(tab_LeftBranch(T));
}


/* EK: unused, only recursive */
static void pcheck_SplitPrecheck(TABLEAU T)
/**************************************************************
  INPUT  : A tableau.
  EFFECTS: Stops and prints an error message if a left half
           of a split does not subsume its parents, or
	   if negations have been generated for a non-ground
	   left split clause.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  if (!subs_Subsumes(tab_LeftSplitClause(T), tab_SplitClause(T), -1, -1)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Incorrect split of %d,", tab_SplitClause(T));
    misc_UserErrorReport(" left half of split does not subsume splitted clause.\n");			 
    misc_FinishUserErrorReport();
  }

  if (list_Length(tab_RightSplitClauses(T)) > 1 &&
      !clause_IsGround(tab_LeftSplitClause(T))) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Incorrect split of %d,", tab_SplitClause(T));
    misc_UserErrorReport(" non-ground split generated more than two clause.\n");
    misc_FinishUserErrorReport();
  }

  pcheck_SplitPrecheck(tab_LeftBranch(T));
  pcheck_SplitPrecheck(tab_RightBranch(T));
}


BOOL pcheck_BuildTableauFromProof(LIST Proof, TABLEAU* Tableau)
/**************************************************************
  INPUT  : A list of clauses representing a proof, and a pointer
           to a tableau used as return value.
  RETURNS: TRUE iff no errors occurred, FALSE otherwise.
           If TRUE is returned <Tableau> is set to a tableau
	   representing the proof.
  EFFECTS: Errors are commented when they occur.
***************************************************************/
{
  LIST     ProofRest;
  TABLEAU  SplitPos;
  TABPATH  Path;
  CLAUSE   Clause;
  int      ClauseLevel, SplitLevel;
  int      ProofDepth;

  if (list_Empty(Proof)) {
    *Tableau = tab_EmptyTableau();
    return TRUE;
  }

  ProofDepth = pcheck_MaxSplitLevel(Proof);
  *Tableau   = tab_CreateNode();
  Path       = tab_PathCreate(ProofDepth, *Tableau);

  ProofRest = Proof;
  while (!list_Empty(ProofRest)) {

    SplitLevel  = tab_PathLength(Path);
    Clause      = list_Car(ProofRest);
    ClauseLevel = clause_SplitLevel(Clause); 

    /* Special treatment for clauses that result from a splitting step */
    if (pcheck_ClauseIsFromSplit(Clause)) {

      if (ClauseLevel == 0) {
	misc_StartUserErrorReport();
	misc_UserErrorReport("\n Error: Split level of split clause %d is 0.\n", clause_Number(Clause));
	misc_FinishUserErrorReport();
      }

      if (ClauseLevel > SplitLevel+1) {
	misc_StartUserErrorReport();
	misc_UserErrorReport("\n Error: Split level of split clause %d", clause_Number(Clause));
	misc_UserErrorReport(" is not increment of current split level.\n");
	misc_FinishUserErrorReport();
      }

      SplitPos = tab_PathNthNode(Path, ClauseLevel-1);

      if (pcheck_ClauseIsFromLeftSplit(Clause)) {
	/* Left branch of a splitting step */
	if (!tab_LeftBranchIsEmpty(SplitPos)) {
	  misc_StartUserErrorReport();
	  misc_UserErrorReport("\n Error: Multiple left splits for clause %d.\n", 
			       clause_Number(tab_SplitClause(SplitPos)));
	  misc_FinishUserErrorReport();
	}

	Path = tab_PathPrefix(ClauseLevel-1, Path);
	tab_SetSplitClause(SplitPos, list_Car(clause_ParentClauses(Clause)));
	tab_SetLeftSplitClause(SplitPos, Clause);
	tab_AddSplitAtCursor(Path, TRUE);
      } else {
	/* Right branch of a splitting step */
	if (tab_RightBranchIsEmpty(SplitPos)) {
	  
	  if (tab_LeftBranchIsEmpty(SplitPos)) {
	    misc_StartUserErrorReport();
	    misc_UserErrorReport("\n Error: Right split with incorrect split level, clause %d.\n", 
				 clause_Number(Clause));
	    misc_FinishUserErrorReport();
	  }

	  Path = tab_PathPrefix(ClauseLevel-1, Path);
	  tab_AddSplitAtCursor(Path, FALSE);
	}
	tab_AddRightSplitClause(SplitPos, Clause); 
      } /* clause from right split */
    } /* clause from split */
      
    if (ClauseLevel > tab_PathLength(Path)) {
      misc_StartUserErrorReport();
      misc_UserErrorReport("\n Error: Split level of clause %d greater than current level.\n", 
			   clause_Number(Clause));
      misc_FinishUserErrorReport();
    }
    tab_AddClauseOnItsLevel(Clause, Path); 
    
    ProofRest = list_Cdr(ProofRest);   
  } /* while proof is not empty */


  tab_PathDelete(Path);

  return TRUE;
}


static BOOL pcheck_TableauJustificationsRec(TABLEAU T, TABPATH Path)
/**************************************************************
  INPUT  : A Tableau <T>, a <Path> in the tableau
  RETURNS: TRUE iff all clauses in the last node of the
           path are correctly justified.
***************************************************************/
{
  CLAUSE  Clause;
  LIST    ScanClauses;
  LIST    ScanParents;
  LIST    Parents;
  CLAUSE  Parent;
  BOOL    Ok, RightSplit;

  if (tab_IsEmpty(T))
    return TRUE;

  Ok = TRUE; 

  /* for each clause, check that its parents have been justified */

  for (ScanClauses = tab_Clauses(tab_PathTop(Path));
       !list_Empty(ScanClauses); ScanClauses = list_Cdr(ScanClauses)) {

    Clause  = list_Car(ScanClauses);
    Parents = clause_ParentClauses(Clause);
    
    RightSplit = pcheck_ClauseIsFromRightSplit(Clause); 
    
    /* check all parents */
    
    for (ScanParents = Parents; !list_Empty(ScanParents); 
	 ScanParents = list_Cdr(ScanParents)) {
      
      Parent = list_Car(ScanParents);
      
      if ((!(RightSplit && clause_IsEmptyClause(Parent)) &&
	  !(RightSplit && pcheck_ClauseIsFromLeftSplit(Parent))) ||
	  (clause_Number(Parent) > clause_Number(Clause)) ) {
	if (!tab_PathContainsClause(Path, Parent)) {
	  misc_StartUserErrorReport();
	  misc_UserErrorReport("\n Error: Parent clause with number %d is not yet justified.\n", 
			       clause_Number(Parent));
	  misc_FinishUserErrorReport();
	}
      }
    }
  }  /* for all clauses in current node */
  
  
  /* Recursion */
  
  if (!tab_LeftBranchIsEmpty(T)) {
    Path = tab_PathPush(tab_LeftBranch(T), Path);
    Ok   = Ok && pcheck_TableauJustificationsRec(tab_LeftBranch(T), Path);
    Path = tab_PathPop(Path);
  }
  
  if (!tab_RightBranchIsEmpty(T)) {
    Path = tab_PathPush(tab_RightBranch(T), Path);
    Ok   = Ok && pcheck_TableauJustificationsRec(tab_RightBranch(T), Path);
    Path = tab_PathPop(Path);
  }

  return Ok;
}

static BOOL pcheck_TableauJustifications(TABLEAU T)
/**************************************************************
  INPUT  : A Tableau
  RETURNS: TRUE iff for each clause in tableau, all its parent
           clauses have been derived in a split on the same level
	   or below.
***************************************************************/
{
  TABPATH Path;
  BOOL    Ok;

  Path = tab_PathCreate(tab_Depth(T),T);
  Ok   = pcheck_TableauJustificationsRec(T,Path); 
  tab_PathDelete(Path);
  
  return Ok;
}

BOOL pcheck_TableauProof(TABLEAU* Tableau, LIST Proof)
/**************************************************************
  INPUT: 
  RETURNS:                                                      
***************************************************************/
{
  LIST RedundantClauses;
  LIST EmptyClauses;
  LIST UnmarkedSplits;

  tab_LabelNodes(*Tableau);
  /* print out current tableau */
  if (pcheck_GenNamedCg) 
    tab_WriteTableau(*Tableau, pcheck_CgName, pcheck_GraphFormat);
  
  RedundantClauses = list_Nil();
  if (!pcheck_Quiet) {
    fputs("pruning closed branches...", stdout);
    fflush(stdout);
  }
  (*Tableau) = tab_PruneClosedBranches(*Tableau, &RedundantClauses);   /* delete descendants of already closed branches */
  if (!pcheck_Quiet)
    puts("finished.");

  if (!pcheck_Quiet) {
    fputs("removing incomplete splits...", stdout);
    fflush(stdout);
  }
  (*Tableau) = tab_RemoveIncompleteSplits(*Tableau, &RedundantClauses);  /* reduce open node redundancies */
  if (!pcheck_Quiet)
    puts("finished.");
  
  list_Delete(RedundantClauses);

  /* remove all clauses that are not needed for the empty clauses */
  /* of the proof or for the tableau structure (splits) */

  EmptyClauses = list_Nil();
  tab_GetEarliestEmptyClauses(*Tableau, &EmptyClauses);
  pcheck_ClauseListRemoveFlag(Proof, MARKED);
  pcheck_MarkRecursive(EmptyClauses);
  UnmarkedSplits = list_Nil();
  pcheck_CollectUnmarkedSplits(*Tableau, &UnmarkedSplits);
  pcheck_MarkRecursive(UnmarkedSplits);
  pcheck_RemoveUnmarkedFromTableau(*Tableau); 
  list_Delete(UnmarkedSplits);
  list_Delete(EmptyClauses);

  /* print reduced graph */
  if (pcheck_GenRedCg) 
    tab_WriteTableau(*Tableau, pcheck_RedCgName, pcheck_GraphFormat);

  tab_SetSplitLevels(*Tableau);
  pcheck_SplitLevels(*Tableau);
  tab_CheckEmpties(*Tableau);

 if (!tab_IsClosed(*Tableau)) {
    puts("\nerror: tableau is not closed.");  
    return FALSE;
 }

  /* check justifications */
  if (!pcheck_Quiet) {
    fputs("checking justifications...", stdout);
    fflush(stdout);
  }
  if (!pcheck_TableauJustifications(*Tableau))
    return FALSE;
  if (!pcheck_Quiet)
    puts("finished.");
 
  return TRUE;
}


void pcheck_MarkRecursive(LIST Clauses)
/**************************************************************
  INPUT:   A list of clauses 
  RETURNS: Nothing.                                                      
  EFFECTS: Marks all <Clauses> and its ancestors with the
           MARKED clause flag.
***************************************************************/
{
  CLAUSE Clause;

  for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses)) {
    Clause = list_Car(Clauses);
    if (!clause_GetFlag(Clause, MARKED)) {
      pcheck_MarkRecursive(clause_ParentClauses(Clause)); 
      clause_SetFlag(Clause, MARKED);
    }
  }
}


static LIST pcheck_CollectTermVariables(TERM Term)
/**************************************************************
  INPUT:   A term.
  RETURNS: A list of terms. For each variable in <Term> the list
           contains exactly one term representing the variable.
  EFFECT:  Memory is allocated for the terms.
***************************************************************/
{
  LIST Result, Scan;

  Result = term_VariableSymbols(Term);
  for (Scan = Result; !list_Empty(Scan); Scan = list_Cdr(Scan))
    list_Rplaca(Scan, term_Create((SYMBOL)list_Car(Scan), list_Nil()));

  return Result;
}


static BOOL pcheck_IsRightSplitHalf(CLAUSE C)
/**************************************************************
  INPUT  : A clause.
  RETURNS: TRUE iff the following conditions are fulfilled:
           - the first parent clause is an empty clause
	   - the clause subsumes its second parent
***************************************************************/
{
  LIST Parents;
  BOOL Ok;

  Parents = list_Copy(clause_ParentClauses(C));
  Parents = list_PointerDeleteDuplicates(Parents);

  Ok = FALSE;
  if (list_Length(Parents) == 2 && clause_IsEmptyClause(list_First(Parents)))
    Ok = subs_Subsumes(C, list_Second(Parents), -1, -1);

  list_Delete(Parents);

  return Ok;
}


static TERM pcheck_UnivClosure(TERM T)
/**************************************************************
  INPUT:   A term, representing a formula.
  RETURNS: The universal closure of the term.
  EFFECTS: <T> is part of the returned term!
***************************************************************/
{
  LIST Vars;

  Vars = pcheck_CollectTermVariables(T);
  
  if (list_Empty(Vars))
    return T;
  return fol_CreateQuantifier(fol_All(), Vars, list_List(T));
}


static TERM pcheck_ClauseToTerm(CLAUSE Clause)
/**************************************************************
  INPUT:   A clause.
  RETURNS: The clause represented as a TERM.
***************************************************************/
{
  int  LitScan;
  LIST Args;
  TERM Lit;
  TERM ClauseTerm;

  Args = list_Nil();

  for (LitScan = clause_FirstLitIndex(); LitScan <= clause_LastLitIndex(Clause);
       LitScan++) {
    Lit  = clause_LiteralSignedAtom(clause_GetLiteral(Clause, LitScan));
    Args = list_Cons(term_Copy(Lit), Args);
  }

  if (list_Empty(Args))
    Args = list_List(term_Create(fol_False(), list_Nil()));
  
  /* Build the disjunction of the literals */
  if (list_Empty(list_Cdr(Args))) {   /* only one arg */
    ClauseTerm = list_Car(Args);
    list_Delete(Args);
  } else
    ClauseTerm = term_Create(fol_Or(), Args);
  ClauseTerm = pcheck_UnivClosure(ClauseTerm);

  return ClauseTerm;
}


static LIST pcheck_ClauseListToTermList(LIST Clauses)
/**************************************************************
  INPUT  : A list of clauses.
  RETURNS: A new list containing the clauses represented as TERMs.
***************************************************************/
{
  LIST Terms;

  Terms = list_Nil();
  for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses))
    Terms = list_Cons(pcheck_ClauseToTerm(list_Car(Clauses)), Terms);
  
  return Terms;
}


static void pcheck_SaveNumberedDFGProblem(int Number, LIST Axioms,
					  LIST Conjectures,
					  const char* ProofFileName,
					  const char* DestPrefix)
/**************************************************************
  INPUT  : A (clause) number, a list of axioms and conjectures,
           and a filename (of the proof file of the currently
	   checked proof)
  RETURNS: Nothing.
  EFFECTS: Saves a DFG file containing <Axioms> and <Conjectures>
           under the name "<DestPrefix><Number>_<ProofFileName>"
***************************************************************/
{
  char *Filename, *Tmp, *NumStr;
  FILE *File;

  NumStr   = string_IntToString(Number);
  Tmp      = pcheck_GenericFilename(ProofFileName, NumStr);
  Filename = string_Conc(DestPrefix, Tmp);
    
  File = misc_OpenFile(Filename, "w");
  fol_FPrintDFGProblem(File, "{*Sub Proof*}", "{* Proof Checker *}",
		       "unsatisfiable",
		       "{* The problem is the correctness test for a single proof line *}",
		       Axioms, Conjectures);
  misc_CloseFile(File, Filename);

  string_StringFree(NumStr);
  string_StringFree(Tmp);
  string_StringFree(Filename);
}


static void pcheck_SplitToProblems(TABLEAU T, const char* ProofFileName,
				   const char* DestPrefix)
/**************************************************************
  INPUT:   A tableau, which isn't a leaf of the tableau tree,
           the name of a proof file and a file name prefix used for
	   generating files.
  RETURNS: Nothing.
  EFFECT:  This function generates proof check tasks for clauses
           resulting from splitting steps and writes them to
	   output files.
  CAUTION: We assume that we get non-null clauses when calling
           tab_SplitClause and tab_LeftSplitClause.
***************************************************************/
{
  TERM SplitClauseTerm, LeftClauseTerm, RightClauseTerm;
  TERM Equiv, Disj, Tmp;
  LIST Conj, Args, Negations;

#ifdef CHECK
  if (tab_IsLeaf(T)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In pcheck_SplitToProblems: Tableau is a leaf of the ");
    misc_ErrorReport("tableau tree.");
    misc_FinishErrorReport();
  }
#endif

  SplitClauseTerm = pcheck_ClauseToTerm(tab_SplitClause(T));
  LeftClauseTerm  = pcheck_ClauseToTerm(tab_LeftSplitClause(T));
  
  /* by default, take all right split clauses as negations       */
  /* if the first clause is the second half of a split clause,   */
  /* take only the rest of the right split clauses as negations. */

  Negations = tab_RightSplitClauses(T);
  if (!list_Empty(Negations) && pcheck_IsRightSplitHalf(list_Car(Negations))) {
    /* EK: Meiner Meinung nach ist es eine Invariante, daß die erste */
    /* Elternklausel die rechte Hälfte eines Splittings ist???  */
    Negations = list_Cdr(Negations);
    /* build C <=> C' v C''  */
    RightClauseTerm = pcheck_ClauseToTerm(list_Car(tab_RightSplitClauses(T)));
    Disj  = term_Create(fol_Or(), list_Cons(LeftClauseTerm, list_List(RightClauseTerm)));
    Equiv = term_Create(fol_Equiv(), list_Cons(SplitClauseTerm, list_List(Disj)));
    Conj  = list_List(Equiv);
    
    pcheck_SaveNumberedDFGProblem(clause_Number(tab_LeftSplitClause(T)),
				  list_Nil(), Conj, ProofFileName, DestPrefix);
    term_DeleteTermList(Conj);
  }
  
  Args = list_Nil();

  /* build conjunction of negations, if there are any. */
  if (!list_Empty(Negations)) {
    LeftClauseTerm = pcheck_ClauseToTerm(tab_LeftSplitClause(T));
    Args  = pcheck_ClauseListToTermList(Negations);
    /* Build the conjunction */
    if (list_Empty(list_Cdr(Args))) {  /* only one arg */
      Tmp = list_Car(Args);
      list_Delete(Args);
    } else
      Tmp = term_Create(fol_And(), Args);
    Tmp   = term_Create(fol_Not(), list_List(Tmp));
    Equiv = term_Create(fol_Implies(),list_Cons(Tmp,list_List(LeftClauseTerm)));
    Conj  = list_List(Equiv);
    
    /* problem id is number of right part of split clause, if it exists,
       number of first negation otherwise */
    pcheck_SaveNumberedDFGProblem(clause_Number(list_Car(tab_RightSplitClauses(T))), 
				  list_Nil(), Conj, ProofFileName, DestPrefix);
    term_DeleteTermList(Conj);
  }
}


void pcheck_TableauToProofTask(TABLEAU T, const char* ProofFileName,
			       const char* DestPrefix)
/**************************************************************
  INPUT:   A Tableau, two strings for filename generation.
  RETURNS: Nothing.
  EFFECTS: Generates DFG problem files for each clause in the tableau.
           The problem asserts that the clause follows from
	   its parents. For splits, see pcheck_SplitToProblems
***************************************************************/
{
  LIST   Scan;
  LIST   Axioms, Conj, Help;
  CLAUSE Clause;

  if (tab_IsEmpty(T))
    return;

  /* treat the splitting clauses at inner nodes of the tableau tree */
  if (!tab_IsLeaf(T))
    pcheck_SplitToProblems(T, ProofFileName, DestPrefix);
 
  /* treat derived clauses that don't result from splitting */
  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    Clause = list_Car(Scan);
    if (!clause_IsFromSplitting(Clause) &&
	!list_Empty(clause_ParentClauses(Clause))) {
      Axioms = list_Copy(clause_ParentClauses(Clause));
      Axioms = list_PointerDeleteDuplicates(Axioms);
      Help   = Axioms;
      Axioms = pcheck_ClauseListToTermList(Axioms);
      list_Delete(Help);
      Conj   = list_List(pcheck_ClauseToTerm(Clause));
      pcheck_SaveNumberedDFGProblem(clause_Number(Clause), Axioms, Conj,
				    ProofFileName, DestPrefix);
      term_DeleteTermList(Axioms);
      term_DeleteTermList(Conj);
    }
  }
  
  /* recursion */
  pcheck_TableauToProofTask(tab_RightBranch(T), ProofFileName, DestPrefix);
  pcheck_TableauToProofTask(tab_LeftBranch(T), ProofFileName, DestPrefix);
}


int pcheck_SeqProofDepth(LIST Proof)
/**************************************************************
  INPUT  : A sequential proof (list of clauses)
  RETURNS: The maximum clause depth in the proof
***************************************************************/ 
{
  int Max;

  Max = 0;
  for ( ; !list_Empty(Proof); Proof = list_Cdr(Proof)) 
    if (clause_Depth(list_Car(Proof)) > Max)
      Max = clause_Depth(list_Car(Proof));
  
  return Max;
}


LIST pcheck_ReduceSPASSProof(LIST Proof)
/**************************************************************
  INPUT:   A list of clauses representing a SPASS proof.
           Parents are pointers.
  RETURNS: A list of clauses were incomplete splits
           and closed branches with descendants have been
	   removed.
***************************************************************/  
{
  LIST    EmptyClauses, RedundantClauses;
  LIST    ReducedProof;
  TABLEAU Tableau;
  LIST    UnmarkedSplits;

  if (!pcheck_BuildTableauFromProof(Proof, &Tableau)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\n Error: Proof could not be translated into a closed tableau.\n");
    misc_FinishUserErrorReport();
  }

  RedundantClauses = list_Nil();
  Tableau = tab_PruneClosedBranches(Tableau, &RedundantClauses);
  Tableau = tab_RemoveIncompleteSplits(Tableau, &RedundantClauses);
  list_Delete(RedundantClauses);
  
  tab_SetSplitLevels(Tableau);
  
  /* 
   *  get minimal proof: First find earliest derived empty clauses,
   *  then recursively mark ancestors of these clauses. Put
   *  only marked clauses in <ReducedProof>.
   */

  EmptyClauses = list_Nil();
  tab_GetEarliestEmptyClauses(Tableau, &EmptyClauses);
  pcheck_ClauseListRemoveFlag(Proof, MARKED);
  pcheck_MarkRecursive(EmptyClauses);
  UnmarkedSplits = list_Nil();
  pcheck_CollectUnmarkedSplits(Tableau, &UnmarkedSplits);
  pcheck_MarkRecursive(UnmarkedSplits);
  pcheck_RemoveUnmarkedFromTableau(Tableau); 
  list_Delete(UnmarkedSplits);

  ReducedProof = list_Nil(); 
  tab_ToClauseList(Tableau, &ReducedProof);
  ReducedProof = pcheck_ClauseNumberMergeSort(ReducedProof);

  tab_Delete(Tableau);
  list_Delete(EmptyClauses); 

  return ReducedProof;
}


void pcheck_DeleteProof(LIST Proof)
/**************************************************************
  INPUT:   A Proof
  RETURNS: Nothing.
  EFFECTS: Frees memory associated with proof
**************************************************************/
{
  LIST Line, Scan2, Scan1;
  
  Scan1 = Proof;
  while (!list_Empty(Scan1)) {
    Line = list_Car(Scan1);
    
    string_StringFree(list_Car(Line));
    if (list_Second(Line) != clause_Null())                /* clause */
      term_Delete(list_Second(Line));

    /* delete labels in justification list and list itself */

    for (Scan2 = list_Third(Line); !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) 
      string_StringFree(list_Car(Scan2));
    list_Delete(list_Third(Line));     

    /* now contents of line are deleted. Delete line. */
    list_Delete(Line);     
    Scan1 = list_Cdr(Scan1);
  }
  list_Delete(Proof);
}


char* pcheck_GenericFilename(const char* Filename, const char* Id)
/**************************************************************
  INPUT:   Two strings.
  RETURNS: A string with Suffix as new extension to Filename
           (Filename = name.ext -> name_<Id>.prf)
  EFFECTS: Memory is allocated for the returned string.
**************************************************************/
{	
  char *Help1, *Help2;
  int  i;

  Help1 = string_Conc("_", Id); 
  Help2 = string_Conc(Help1, pcheck_ProofFileSuffix); 
  string_StringFree(Help1);
  
  /* remove filename extension */
  for (i = 0; Filename[i] != '.' && i < strlen(Filename); i++)
    /* empty */;
  Help1 = string_Prefix(Filename, i);

  return string_Nconc(Help1, Help2);  /* Help1 and Help2 are freed, too */
}


void pcheck_ClauseListRemoveFlag(LIST Clauses, CLAUSE_FLAGS Flag)
/**************************************************************
  INPUT:   A list of clauses and a clause flag
  RETURNS: Nothing.
  EFFECTS: Removes the <Flag> in all clauses in the list
**************************************************************/
{
  for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses)) 
    clause_RemoveFlag(list_Car(Clauses), Flag);
}


LIST pcheck_ClauseNumberMergeSort(LIST L)
/**************************************************************
  INPUT:   A list of clauses  
  RETURNS: The sorted list: clause_Number(L[i]) < clause_Number(L[i+1])
  EFFECTS: Destructive
***************************************************************/
{
  return clause_NumberSort(L);
}