Updated raytracer test. Added SPASS test.

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

1 files changed, 1763 insertions, 0 deletions

diff --git a/test/spass/rules-sort.c b/test/spass/rules-sort.c
new file mode 100644
index 0000000..74f8c9f
--- /dev/null
+++ b/test/spass/rules-sort.c
@@ -0,0 +1,1763 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *           INFERENCE RULES FOR SORTS                    * */
+/* *                                                        * */
+/* *  $Module:   SORTRULES                                  * */ 
+/* *                                                        * */
+/* *  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$ */
+
+/**************************************************************/
+/* Includes                                                   */
+/**************************************************************/
+
+#include "rules-sort.h"
+
+     
+/**************************************************************/
+/* Functions                                                  */
+/**************************************************************/ 
+
+static LIST inf_GetForwardPartnerLits(LITERAL, st_INDEX);
+static SORT inf_GetSortFromLits(LIST, SORTTHEORY);
+
+
+static BOOL inf_SubsortPrecheck(CLAUSE Clause, LIST TLits, LITERAL Special,
+				st_INDEX Index, SORTTHEORY SortTheory)
+/**************************************************************
+  INPUT:   A clause, a list of constraint literal indices in
+           that clause, a special literal, an index of clauses,
+	   and the actual sort theory.
+  RETURNS: TRUE, if there exists any subsort of the <TLits> sort.
+***************************************************************/
+{
+  SORT tSort, unifierSort;
+  LIST unifiers;
+  BOOL result;
+
+  unifiers = inf_GetForwardPartnerLits(clause_GetLiteral(Clause,(int)list_Car(TLits)),
+				       Index);
+  unifierSort = inf_GetSortFromLits(unifiers, SortTheory);
+  list_Delete(unifiers);
+
+  tSort = sort_TopSort();
+  for (; !list_Empty(TLits); TLits = list_Cdr(TLits)) {
+    TERM actAtom = clause_GetLiteralAtom(Clause, (int)list_Car(TLits));
+    tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)),
+			   tSort);
+  }
+  tSort = list_PointerDeleteDuplicates(tSort);
+
+  if (Special == NULL)
+    result = sort_TheoryIsSubsortOf(SortTheory, unifierSort, tSort);
+  else {
+    SORT extraSort;
+    extraSort = sort_TheorySortOfSymbol(SortTheory, clause_LiteralPredicate(Special));
+    result    = sort_TheoryIsSubsortOfExtra(SortTheory, extraSort, unifierSort, tSort);
+    sort_Delete(extraSort);
+  }
+
+  sort_Delete(tSort);
+  sort_Delete(unifierSort);
+
+  return result;
+}
+     
+static LIST inf_GetSortResolutionPartnerLits(TERM Atom, st_INDEX Index)
+/**************************************************************
+  INPUT:   A clause, and an Index of clauses.
+  RETURNS: A list of literals with which sortresolution is possible.
+  MEMORY:  Allocates memory for the list.
+***************************************************************/
+{
+  LIST    Result, TermList, LitScan;
+  LITERAL NextLit;
+  CLAUSE  Clause;
+
+#ifdef CHECK  
+  if (!term_IsAtom(Atom)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_GetSortResolutionPartnerLits: Variable as atom input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  Result   = list_Nil();
+  TermList = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(), Atom);
+  
+  for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) {
+    
+    if (term_IsAtom(list_Car(TermList))) {
+      
+      for (LitScan = sharing_NAtomDataList(list_Car(TermList)); 
+	   !list_Empty(LitScan); 
+	   LitScan = list_Cdr(LitScan)){
+	NextLit = list_Car(LitScan);
+	Clause  = clause_LiteralOwningClause(NextLit);
+	
+	if (clause_LiteralIsPositive(NextLit) && 
+	    clause_LiteralGetFlag(NextLit,STRICTMAXIMAL) &&
+	    clause_GetFlag(Clause, WORKEDOFF) &&
+	    clause_HasSolvedConstraint(Clause) &&
+	    !list_PointerMember(Result, NextLit)) 
+	  Result = list_Cons(NextLit, Result);
+      }
+    }
+  }
+  
+  return Result;
+}
+
+
+static CLAUSE inf_BuildConstraintHyperResolvent(CLAUSE Clause, LIST Lits,
+						SUBST Subst, LIST Foundlits,
+						FLAGSTORE Flags,
+						PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A <Clause> where the sort constraint is resolved,
+           a list <Lits> of constraint indices in <Clause> where
+	   all corresponding constraints have the same term,
+	   the overall substitution <Subst>,
+	   a list <Foundlits> of literals of found partner clauses,
+	   a flag store and a precedence.
+  RETURNS: A clause, the resolvent of a resolution step.
+***************************************************************/
+{
+  CLAUSE NewClause, ClauseCopy;
+  LIST   Constraint, Antecedent, Succedent, ParentCls, ParentLits, Scan;
+  TERM   Atom;
+  SYMBOL MaxVar,MaxCand;
+  int    i,bound, depth;
+  BOOL   IsFromEmptySort;
+  LIST   Partners;
+  
+  ParentCls   = list_Nil();
+  ParentLits  = list_Nil();
+  Constraint  = list_Nil();
+  Antecedent  = list_Nil();
+  Succedent   = list_Nil();
+  Partners    = list_Nil();
+  depth       = clause_Depth(Clause);
+
+  for (Scan=Foundlits; !list_Empty(Scan); Scan=list_Cdr(Scan))
+    depth = misc_Max(depth,
+		     clause_Depth(clause_LiteralOwningClause(list_Car(Scan))));
+
+  ClauseCopy  = clause_Copy(Clause);
+  Partners    = list_Cons(ClauseCopy, Partners);
+  clause_SubstApply(Subst, ClauseCopy);
+
+  IsFromEmptySort = term_IsVariable(term_FirstArgument(
+    clause_GetLiteralAtom(Clause, (int)list_Car(Lits))));
+
+  bound = clause_LastConstraintLitIndex(ClauseCopy);
+
+  for (i = clause_FirstLitIndex(); i <= bound; i++)
+    if (!list_PointerMember(Lits, (POINTER)i)) {
+      Atom  = term_Copy(clause_GetLiteralAtom(ClauseCopy, i));
+      Constraint = list_Cons(Atom, Constraint);
+    } 
+    else {
+      ParentCls  = list_Cons((POINTER)clause_Number(ClauseCopy), ParentCls);
+      ParentLits = list_Cons((POINTER)i, ParentLits);
+    }
+
+  bound = clause_LastAntecedentLitIndex(ClauseCopy);
+  for ( ; i <= bound; i++) {
+    Atom = term_Copy(clause_GetLiteralAtom(ClauseCopy, i));
+    Antecedent = list_Cons(Atom, Antecedent);
+  }
+  bound = clause_LastSuccedentLitIndex(ClauseCopy);
+  for (; i <= bound; i++) {
+    Atom = term_Copy(clause_GetLiteralAtom(ClauseCopy, i));
+    Succedent = list_Cons(Atom, Succedent);
+  }
+  bound = clause_LastConstraintLitIndex(Clause);
+  for (i = clause_FirstLitIndex(); i <= bound; i++) {			
+    /* Hier sollen die gematchten Constraintliterale dazu fuehren, dass die */
+    /* c,a und s- literale der Partnerclauses in die Listen kommen...       */
+
+    if (list_PointerMember(Lits, (POINTER)i)) {
+      CLAUSE  PartnerCopy;
+      LITERAL PLit;
+      TERM    PAtom;
+      SUBST   NewSubst,RightSubst;
+      int     j,lc,la,n,PLitInd;
+
+      Atom      = clause_GetLiteralAtom(ClauseCopy, i);
+      NewClause = clause_CreateUnnormalized(Constraint, Antecedent, Succedent);
+
+      list_Delete(Constraint);
+      list_Delete(Antecedent);
+      list_Delete(Succedent);
+      Constraint  = list_Nil();
+      Antecedent  = list_Nil();
+      Succedent   = list_Nil();
+
+      /* Find corresponding Foundlit: */
+      for (Scan = Foundlits; 
+	   term_TopSymbol(Atom) !=
+	     term_TopSymbol(clause_LiteralAtom(list_Car(Scan))); 
+	   Scan = list_Cdr(Scan));
+      PLit        = list_Car(Scan);
+      PLitInd     = clause_LiteralGetIndex(PLit);
+      PartnerCopy = clause_Copy(clause_LiteralOwningClause(PLit));
+      Partners    = list_Cons(PartnerCopy, Partners);
+      ParentCls   = list_Cons((POINTER)clause_Number(PartnerCopy), ParentCls);
+      ParentLits  = list_Cons((POINTER)PLitInd, ParentLits);
+      MaxVar      = clause_SearchMaxVar(ClauseCopy);
+      MaxCand     = clause_SearchMaxVar(NewClause);
+      MaxVar      = ((MaxVar > MaxCand) ? MaxVar : MaxCand);   
+      /* MaxVar is the maximal variable in the new clause or the ClauseCopy, */
+      /* the latter to guarantee the stability of variable names.            */
+
+      clause_RenameVarsBiggerThan(PartnerCopy, MaxVar);
+      PLit  = clause_GetLiteral(PartnerCopy, PLitInd);
+      PAtom = clause_LiteralAtom(PLit);
+      
+      cont_Check();
+      if (!unify_UnifyNoOC(cont_LeftContext(), PAtom, cont_RightContext(), Atom)) {
+	misc_StartErrorReport();
+	misc_ErrorReport("\n In inf_BuildConstraintHyperResolvent: Unification failed.");
+	misc_FinishErrorReport();
+      }
+      subst_ExtractUnifier(cont_LeftContext(), &RightSubst, cont_RightContext(), &NewSubst);
+      cont_Reset();
+
+      clause_SubstApply(NewSubst, NewClause);
+      clause_SubstApply(NewSubst, ClauseCopy);
+      subst_Delete(NewSubst);
+      
+      n  = clause_Length(PartnerCopy);
+      lc = clause_LastConstraintLitIndex(PartnerCopy);
+      la = clause_LastAntecedentLitIndex(PartnerCopy);
+      for (j = clause_FirstLitIndex(); j < n; j++) {
+	if (j <= lc) 
+	  Constraint  = list_Cons(subst_Apply(RightSubst,
+	    term_Copy(clause_GetLiteralAtom(PartnerCopy, j))),
+	      Constraint);
+	else if (j <= la) 
+	  Antecedent  = list_Cons(subst_Apply(RightSubst,
+            term_Copy(clause_GetLiteralAtom(PartnerCopy, j))),
+               Antecedent);
+	else if (j != PLitInd)
+	  Succedent  = list_Cons(subst_Apply(RightSubst,
+            term_Copy(clause_GetLiteralAtom(PartnerCopy, j))),
+               Succedent);
+      }
+
+      subst_Delete(RightSubst);
+      
+      n  = clause_Length(NewClause);
+      lc = clause_LastConstraintLitIndex(NewClause);
+      la = clause_LastAntecedentLitIndex(NewClause);
+      
+      for (j = clause_FirstLitIndex(); j < n; j++) {
+	if (j <= lc) 
+	  Constraint  = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)),
+				  Constraint);
+	else if (j <= la) 
+	  Antecedent  = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)),
+				  Antecedent);
+	else 
+	  Succedent  = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)),
+				 Succedent);
+      }      
+      clause_Delete(NewClause);
+      clause_DecreaseCounter();
+    }
+  }
+  NewClause = clause_Create(Constraint, Antecedent, Succedent, Flags,Precedence);
+
+  list_Delete(Constraint); 
+  list_Delete(Antecedent); 
+  list_Delete(Succedent); 
+
+  if (IsFromEmptySort)
+    clause_SetFromEmptySort(NewClause);
+  else
+    clause_SetFromSortResolution(NewClause);
+
+  clause_SetDepth(NewClause, depth + 1);
+
+  clause_SetSplitDataFromList(NewClause, Partners);
+  clause_DeleteClauseList(Partners);
+
+  clause_SetParentClauses(NewClause, list_NReverse(ParentCls));
+  clause_SetParentLiterals(NewClause, list_NReverse(ParentLits));
+
+  return NewClause;
+}
+
+
+static LIST inf_ConstraintHyperResolvents(CLAUSE Clause, LIST Lits,
+					  SUBST Subst, LIST Restlits,
+					  LIST Foundlits, st_INDEX Index,
+					  FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A <Clause> where the sort constraint is resolved,
+           a list <Lits> of constraint indices in <Clause> where
+	   all corresponding constraints have the same term,
+	   the overall substitution <Subst>,
+	   a list <Restlits> of constraint indeces for which
+	   a partner clause is searched with respect to <Index>,
+	   a list <Foundlits> of literals of already found partner clauses,
+	   a flag store and a precedence.
+  RETURNS: The list of possible resolvents.
+***************************************************************/
+{
+  if (list_Empty(Restlits))
+    return list_List(inf_BuildConstraintHyperResolvent(Clause,Lits,Subst,
+						       Foundlits, Flags,
+						       Precedence));
+  else {
+    CLAUSE  PartnerCopy;
+    LITERAL Lit, PLit;
+    LIST    Result, NextLits;
+    TERM    AtomCopy;
+    SUBST   NewSubst, RightSubst, HelpSubst;
+    SYMBOL  MaxVar, MaxCand;
+    int     PLitInd;
+
+    Result   = list_Nil();
+    Lit      = clause_GetLiteral(Clause, (int) list_Car(Restlits));
+    AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit)));
+    NextLits = inf_GetSortResolutionPartnerLits(AtomCopy,Index);
+    MaxVar   = clause_MaxVar(Clause);
+    MaxCand  = clause_AtomMaxVar(AtomCopy);
+    MaxVar   = (symbol_GreaterVariable(MaxVar, MaxCand) ? MaxVar : MaxCand);
+      
+    for ( ; !list_Empty(NextLits); NextLits = list_Pop(NextLits)) {
+      PLit        = list_Car(NextLits);
+      PLitInd     = clause_LiteralGetIndex(PLit);
+      Foundlits   = list_Cons(PLit, Foundlits);
+      PartnerCopy = clause_Copy(clause_LiteralOwningClause(PLit));
+
+      clause_RenameVarsBiggerThan(PartnerCopy, MaxVar);
+      PLit        = clause_GetLiteral(PartnerCopy, PLitInd);
+
+      cont_Check();
+      unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
+		      cont_RightContext(), clause_LiteralAtom(PLit));
+      subst_ExtractUnifier(cont_LeftContext(), &NewSubst, cont_RightContext(), &RightSubst);
+      cont_Reset();
+
+      subst_Delete(RightSubst);
+      HelpSubst = NewSubst;
+      NewSubst  = subst_Compose(NewSubst, subst_Copy(Subst));
+
+      Result = list_Nconc(inf_ConstraintHyperResolvents(Clause, Lits, NewSubst,
+							list_Cdr(Restlits),
+							Foundlits, Index, Flags,
+							Precedence),
+			  Result);
+      subst_Delete(NewSubst);
+      subst_Delete(HelpSubst);
+      clause_Delete(PartnerCopy);
+
+      Foundlits = list_Pop(Foundlits);
+    }
+    term_Delete(AtomCopy);
+
+    return Result;
+  }
+}
+
+
+LIST inf_BackwardSortResolution(CLAUSE GivenClause, st_INDEX Index,
+				SORTTHEORY SortTheory, BOOL Precheck,
+				FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause with a solved sort constraint, an index of clauses,
+           a sort theory, a boolean flag indicating whether the subsort
+	   precheck can be applied, a flag store and a precedence.
+  RETURNS: A list of clauses inferred from the GivenClause by
+           SortResolution with the given clause.
+  MEMORY:  A list of clauses is produced, where memory for the list
+           and the clauses is allocated.
+***************************************************************/
+{
+  LIST     result;
+  int      i, ls;
+
+#ifdef CHECK
+  if (!clause_IsClause(GivenClause, Flags, Precedence) ||
+      !clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_BackwardSortResolution: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = list_Nil();
+  ls     = clause_LastSuccedentLitIndex(GivenClause);
+
+  for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) {
+    LITERAL pLit;
+    TERM    pAtom;
+
+    pLit  = clause_GetLiteral(GivenClause, i);
+    pAtom = clause_LiteralAtom(pLit);
+
+    if (clause_LiteralGetFlag(pLit,STRICTMAXIMAL) && 
+	clause_LiteralIsSort(pLit)) {
+      LIST termList;
+      termList = st_GetUnifier(cont_LeftContext(),Index,cont_RightContext(),pAtom);
+      
+      for ( ; !list_Empty(termList); termList = list_Pop(termList)){
+	if (term_IsAtom(list_Car(termList)) &&
+	    !term_IsVariable(term_FirstArgument(list_Car(termList)))) {
+
+	  LIST litScan;
+	  litScan = sharing_NAtomDataList(list_Car(termList));
+	  for ( ; !list_Empty(litScan); litScan = list_Cdr(litScan)) {
+	    LITERAL gLit;
+	    CLAUSE gClause;
+	    gLit    = list_Car(litScan);
+	    gClause = clause_LiteralOwningClause(gLit);
+	    if (clause_LiteralGetIndex(gLit) < clause_FirstAntecedentLitIndex(gClause) && 
+		clause_GetFlag(gClause,WORKEDOFF)) {
+	      TERM   gAtom;
+	      int    lc, gi, j;
+	      LIST   tLits, restLits;
+	      gAtom     = clause_LiteralAtom(gLit);
+	      lc        = clause_LastConstraintLitIndex(gClause);
+	      gi        = clause_LiteralGetIndex(gLit);
+	      tLits     = list_List((POINTER)gi);
+	      restLits  = list_Nil();
+	      for (j = clause_FirstLitIndex(); j <= lc; j++) {
+		LITERAL tCand;
+		tCand = clause_GetLiteral(gClause, j);
+		if (j != gi &&
+		    term_FirstArgument(clause_LiteralAtom(tCand))
+		    == term_FirstArgument(gAtom)) {
+		  tLits     = list_Cons((POINTER)j, tLits);
+		  restLits  = list_Cons((POINTER)j, restLits);
+		}
+	      }
+
+	      if (!Precheck ||
+		  inf_SubsortPrecheck(gClause,tLits,pLit,Index,SortTheory)) {
+		CLAUSE pClauseCopy;
+		SYMBOL minVar;
+		LIST   foundLits;
+		SUBST  leftSubst, rightSubst;
+		pClauseCopy = clause_Copy(GivenClause);
+		minVar      = clause_MaxVar(gClause);
+		foundLits   = list_List(pLit);
+
+		clause_RenameVarsBiggerThan(pClauseCopy, minVar);
+		pAtom = clause_GetLiteralAtom(pClauseCopy, i);
+		/* set, to unify correctly! */
+
+		cont_Check();
+		unify_UnifyNoOC(cont_LeftContext(), gAtom, cont_RightContext(), pAtom);
+		subst_ExtractUnifier(cont_LeftContext(), &leftSubst,
+				     cont_RightContext(), &rightSubst);
+		cont_Reset();
+
+		subst_Delete(rightSubst);
+
+		result =
+		  list_Nconc(inf_ConstraintHyperResolvents(gClause, tLits,
+							   leftSubst, restLits,
+							   foundLits, Index,
+							   Flags, Precedence),
+			     result);
+
+		pAtom = clause_LiteralAtom(pLit);
+
+		subst_Delete(leftSubst);
+		list_Delete(foundLits);
+		clause_Delete(pClauseCopy);
+	      } /* if Precheck */
+	      list_Delete(tLits);
+	      list_Delete(restLits);
+	    }
+	  }
+	}
+      }
+    }
+  }
+  return result;
+}
+
+
+LIST inf_ForwardSortResolution(CLAUSE GivenClause, st_INDEX Index,
+			       SORTTHEORY SortTheory, BOOL Precheck,
+			       FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause with an unsolved sort constraint, an index of clauses,
+           a sort theory, a boolean flag indicating whether the subsort
+	   precheck can be applied, a flag store and a precedence.
+  RETURNS: A list of clauses inferred from the GivenClause by
+           SortResolution on the given clause.
+  MEMORY:  A list of clauses is produced, where memory for the list
+           and the clauses is allocated.
+***************************************************************/
+{
+  LIST Result, TLits, RestLits;
+  int  i, j, lc;
+  BOOL Hit;
+  TERM TAtom;
+
+#ifdef CHECK
+  if (!clause_IsClause(GivenClause, Flags, Precedence) ||
+      !clause_HasTermSortConstraintLits(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_ForwardSortResolution: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  Result = list_Nil();
+  lc     = clause_LastConstraintLitIndex(GivenClause);
+  Hit    = FALSE;
+
+  i = clause_FirstLitIndex();
+  while (i <= lc && !Hit) {
+    TAtom = clause_GetLiteralAtom(GivenClause, i);
+    if (!term_IsVariable(term_FirstArgument(TAtom)))
+      Hit = TRUE;
+    else
+      i++;
+  }
+
+  if (!Hit)
+    return list_Nil();
+
+  /* added because of compiler warnings */
+  TAtom = clause_GetLiteralAtom(GivenClause, i);
+
+  /* Search the other T_i from <GivenClause> */
+  TLits    = list_List((POINTER)i);
+  for (j = i+1; j <= lc; j++) {
+    if (term_FirstArgument(clause_GetLiteralAtom(GivenClause, j))
+	== term_FirstArgument(TAtom))
+      TLits    = list_Cons((POINTER)j, TLits);
+  }
+  RestLits = list_Copy(TLits);
+  
+  if (!Precheck ||
+      inf_SubsortPrecheck(GivenClause, TLits, NULL, Index, SortTheory)) {
+
+    Result = inf_ConstraintHyperResolvents(GivenClause, TLits, subst_Nil(),
+					   RestLits, list_Nil(), Index, Flags,
+					   Precedence);
+
+  }
+  list_Delete(RestLits);
+  list_Delete(TLits);
+
+  return Result;
+}
+
+
+LIST inf_BackwardEmptySort(CLAUSE GivenClause, st_INDEX Index,
+			   SORTTHEORY SortTheory, BOOL Precheck,
+			   FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause with a solved sort constraint, an 'Index' of clauses,
+           a sort theory, a boolean flag indicating whether the subsort
+	   precheck can be applied, a flag store and a precedence.
+  RETURNS: A list of clauses inferred from the GivenClause by
+           EmptySort with the given clause.
+  MEMORY:  A list of clauses is produced, where memory for the list
+           and the clauses is allocated.
+***************************************************************/
+{
+  LIST result;
+  int  i, ls;
+
+#ifdef CHECK
+  if (!(clause_IsClause(GivenClause, Flags, Precedence)) ||
+      !clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_BackwardEmptySort: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = list_Nil();
+  
+  ls = clause_LastSuccedentLitIndex(GivenClause);
+
+  for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) {
+    LITERAL pLit  = clause_GetLiteral(GivenClause, i);
+    TERM    pAtom = clause_LiteralAtom(pLit);
+      
+    if (clause_LiteralGetFlag(pLit,STRICTMAXIMAL) && 
+	clause_LiteralIsSort(pLit)) {
+      LIST unifiers = st_GetUnifier(cont_LeftContext(),Index,cont_RightContext(),pAtom);
+	
+      for ( ; !list_Empty(unifiers); unifiers = list_Pop(unifiers)){
+	if (term_IsAtom(list_Car(unifiers)) &&
+	    term_IsVariable(term_FirstArgument(list_Car(unifiers)))) {
+	  LIST litScan = sharing_NAtomDataList(list_Car(unifiers));
+	    
+	  for ( ; !list_Empty(litScan); litScan = list_Cdr(litScan)){
+	    LITERAL gLit   = list_Car(litScan);
+	    CLAUSE gClause = clause_LiteralOwningClause(gLit);
+	      
+	    if (clause_LiteralGetIndex(gLit) < clause_FirstAntecedentLitIndex(gClause) &&
+		clause_GetFlag(gClause,WORKEDOFF) &&
+		clause_HasOnlyVarsInConstraint(gClause, Flags, Precedence)) {
+	      TERM   gAtom     = clause_LiteralAtom(gLit);
+	      SYMBOL var       = term_TopSymbol(term_FirstArgument(gAtom));
+	      int    lc        = clause_LastConstraintLitIndex(gClause);
+	      int    gi        = clause_LiteralGetIndex(gLit);
+	      BOOL   varOccursNoMore;
+	      int    j, bound;
+
+	      varOccursNoMore = TRUE;
+	      bound           = clause_LastSuccedentLitIndex(gClause);
+		
+	      for (j = clause_FirstAntecedentLitIndex(gClause);
+		   (j <= bound) && varOccursNoMore;
+		   j++) {
+		if (term_ContainsSymbol(clause_GetLiteralAtom(gClause, j), var))
+		  varOccursNoMore = FALSE;
+	      }
+		
+	      if (varOccursNoMore) {
+		LIST tLits, restLits;
+
+		/* Search the other T_i from <gClause> */
+		tLits     = list_List((POINTER)gi);
+		restLits  = list_Nil();		
+		for (j = clause_FirstLitIndex(); j <= lc; j++) {
+		  LITERAL tCand = clause_GetLiteral(gClause, j);
+
+		  if (j != gi &&
+		      term_FirstArgument(clause_LiteralAtom(tCand))
+		      == term_FirstArgument(gAtom)) {
+		    tLits     = list_Cons((POINTER)j, tLits);
+		    restLits  = list_Cons((POINTER)j, restLits);
+		  }
+		}
+
+		if (!Precheck ||
+		    inf_SubsortPrecheck(gClause,tLits,pLit,Index,SortTheory)) {
+		  CLAUSE pCopy     = clause_Copy(GivenClause);
+		  SYMBOL minVar    = clause_MaxVar(gClause);
+		  LIST   foundLits = list_List(pLit);
+		  SUBST  leftSubst, rightSubst;
+
+		  clause_RenameVarsBiggerThan(pCopy, minVar);
+		  pAtom = clause_GetLiteralAtom(pCopy, i);
+		  /* set, to adress the renamed term! */
+		  
+		  cont_Check();
+		  unify_UnifyNoOC(cont_LeftContext(), gAtom, cont_RightContext(), pAtom);
+		  subst_ExtractUnifier(cont_LeftContext(),  &leftSubst,
+				       cont_RightContext(), &rightSubst);
+		  cont_Reset();
+
+		  subst_Delete(rightSubst);
+		  
+		  result =
+		    list_Nconc(inf_ConstraintHyperResolvents(gClause, tLits,
+							     leftSubst,restLits,
+							     foundLits, Index,
+							     Flags, Precedence),
+			       result);
+
+		  list_Delete(foundLits);
+		  subst_Delete(leftSubst);
+		  clause_Delete(pCopy);
+		  
+		  pAtom = clause_LiteralAtom(pLit);
+		  /* reset to original clauses literal! */
+		} /* if Precheck */
+		list_Delete(tLits);
+		list_Delete(restLits);
+	      }
+	    }
+	  }
+	}
+      }
+    }
+  }
+  return result;
+}
+
+
+LIST inf_ForwardEmptySort(CLAUSE GivenClause, st_INDEX Index,
+			  SORTTHEORY SortTheory, BOOL Precheck, FLAGSTORE Flags,
+			  PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause, an index of clauses, a sort theory,
+           a boolean flag indicating whether the subsort
+	   precheck can be applied, a flag store and a precedence.
+	   The constraint of <GivenClause> is necessarily unsolved
+  RETURNS: A list of clauses inferred from the GivenClause by
+           EmptySort on the given clause.
+  MEMORY:  A list of clauses is produced, where memory for the list
+           and the clauses is allocated.
+***************************************************************/
+{
+  LIST   Result, TLits, RestLits;
+  int    i, j, lc, ls;
+  BOOL   Hit;
+  TERM   TAtom;
+  SYMBOL Var;
+
+#ifdef CHECK
+  if (clause_HasTermSortConstraintLits(GivenClause) ||
+      clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_ForwardEmptySort: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+  
+  Result = list_Nil();
+  lc     = clause_LastConstraintLitIndex(GivenClause);
+  Hit    = FALSE;
+  
+  i = clause_FirstLitIndex();
+  while (i <= lc && !Hit) {
+    TAtom = clause_GetLiteralAtom(GivenClause, i);
+
+    if (term_IsVariable(term_FirstArgument(TAtom))) {
+      Var   = term_TopSymbol(term_FirstArgument(TAtom));
+      ls    = clause_LastSuccedentLitIndex(GivenClause);
+      Hit = TRUE;
+      /* Check if the variable occurs in antecedent or succedent literals */
+      for (j = clause_FirstAntecedentLitIndex(GivenClause);
+	   j <= ls && Hit; j++) {
+	if (term_ContainsSymbol(clause_GetLiteralAtom(GivenClause,j), Var))
+	  Hit = FALSE; /* Variable occurs in antecedent/constraint literal */
+      }
+    }
+    if (!Hit)
+      i++;
+  }
+  
+  if (!Hit)
+    return list_Nil();
+
+  TAtom = clause_GetLiteralAtom(GivenClause, i);
+  Var   = term_TopSymbol(term_FirstArgument(TAtom));
+
+  /* Search the other T_i(t) literals */
+  TLits    = list_List((POINTER)i);
+  for (j = i+1; j <= lc; j++) {
+    TERM TCand;
+    
+    TCand = clause_GetLiteralAtom(GivenClause, j);
+    
+    if (symbol_Equal(term_TopSymbol(term_FirstArgument(TCand)), Var))
+      TLits    = list_Cons((POINTER)j, TLits);
+  }
+  RestLits = list_Copy(TLits);
+  
+  if (!Precheck ||
+      inf_SubsortPrecheck(GivenClause, TLits, NULL, Index, SortTheory)) {
+    
+    Result = inf_ConstraintHyperResolvents(GivenClause, TLits, subst_Nil(),
+					   RestLits, list_Nil(), Index, Flags,
+					   Precedence);
+
+  }
+  list_Delete(RestLits);
+  list_Delete(TLits);
+  
+  return Result;
+}
+
+static LIST inf_GetForwardPartnerLits(LITERAL Literal, st_INDEX Index)
+/**************************************************************
+  INPUT:   A monadic literal, and an index of clauses.
+  RETURNS: A list of monadic succedent literals whose subterm
+           is unifiable with the (one) subterm of <Literal>.
+	   The literals are strict maximal in their respective clauses,
+	   the clauses are "WORKEDOFF" and either the subterm
+	   is not a variable or the clause has an empty constraint.
+  MEMORY:  Allocates memory for the list.
+***************************************************************/
+{
+  LIST result, unifiers, atomScan, litScan;
+
+#ifdef CHECK
+  if (!clause_LiteralIsLiteral(Literal) || !clause_LiteralIsSort(Literal)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_GetForwardPartnerLits: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result   = list_Nil();
+  /* Search unifiers for the literal's subterm */
+  unifiers = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(),
+			   term_FirstArgument(clause_LiteralAtom(Literal)));
+  
+  for ( ; !list_Empty(unifiers); unifiers = list_Pop(unifiers)) {
+
+    if (!term_IsAtom(list_Car(unifiers))) { /* Can happen if arg is variable */
+      
+      for (atomScan = term_SupertermList(list_Car(unifiers)); 
+	   !list_Empty(atomScan); 
+	   atomScan = list_Cdr(atomScan)) {
+	TERM atomCand;
+	atomCand = (TERM) list_Car(atomScan);
+	if (term_IsDeclaration(atomCand)) {
+	  /* We are looking for an unary atom */
+
+	  for (litScan = sharing_NAtomDataList(atomCand);
+	       !list_Empty(litScan);
+	       litScan = list_Cdr(litScan)) {
+	    LITERAL nextLit;
+	    CLAUSE  nextClause;
+	    nextLit    = list_Car(litScan);
+	    nextClause = clause_LiteralOwningClause(nextLit);
+
+	    if (clause_LiteralIsPositive(nextLit) && 
+		clause_LiteralGetFlag(nextLit,STRICTMAXIMAL) &&
+		clause_GetFlag(nextClause, WORKEDOFF) &&
+		(!term_IsVariable(list_Car(unifiers)) ||
+		 clause_HasEmptyConstraint(nextClause)) &&
+		clause_HasSolvedConstraint(nextClause)) {
+	      /* Add the literal from the copied clause */
+	      result = list_Cons(nextLit, result);
+	    }
+	  }  /* litScan */
+	}    /* if IsAtom */
+      }      /* atomScan */
+    }        /* ! variable */
+  }          /* unifiers */
+  return result;
+}
+
+static BOOL inf_LiteralsHaveSameSubtermAndAreFromSameClause(LITERAL L1, LITERAL L2)
+/**************************************************************
+  INPUT:   Two literals.
+  RETURNS: TRUE, if both literals have the same term and are
+           from the same clause, FALSE otherwise.
+	   Since both literals are shared, pointer equality
+	   is used to detect this.
+	   This function is used by inf_GetBackwardPartnerLits().
+***************************************************************/
+{
+  return (term_FirstArgument(clause_LiteralAtom(L1))
+	  == term_FirstArgument(clause_LiteralAtom(L2)) &&
+	  clause_LiteralOwningClause(L1) == clause_LiteralOwningClause(L2));
+}
+
+static void inf_GetBackwardPartnerLits(LITERAL Literal, st_INDEX Index,
+				       LIST* ConstraintLits, LIST* Unifiers,
+				       BOOL IsFromEmptySort, FLAGSTORE Flags,
+				       PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A literal, an index of clauses, two pointers to lists,
+           a boolean value, a flag store and a precedence.
+  RETURNS:
+  MEMORY:  Allocates memory for the list.
+***************************************************************/
+{
+  LIST candidates, atomScan, litScan;
+  LITERAL nextLit;
+  CLAUSE  nextClause;
+
+#ifdef CHECK
+  if (!clause_LiteralIsLiteral(Literal) || !clause_LiteralIsSort(Literal)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_GetBackwardPartnerLits: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  candidates = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(),
+			     term_FirstArgument(clause_LiteralAtom(Literal)));
+
+  for ( ; !list_Empty(candidates); candidates = list_Pop(candidates)) {
+    if (!term_IsAtom(list_Car(candidates))) { /* May happen if arg is variable */
+      /* Consider variable unifiers only if called from BackwardEmptySort */
+      for (atomScan = term_SupertermList(list_Car(candidates)); 
+	   !list_Empty(atomScan); 
+	   atomScan = list_Cdr(atomScan)) {
+	TERM atomCand;
+	atomCand = (TERM) list_Car(atomScan);
+	if (term_IsDeclaration(atomCand)) {
+	  /* We are looking for unary atoms */
+
+	  for (litScan = sharing_NAtomDataList(atomCand);
+	       !list_Empty(litScan);
+	       litScan = list_Cdr(litScan)) {
+	    nextLit    = list_Car(litScan);
+	    nextClause = clause_LiteralOwningClause(nextLit);
+	    
+	    if (clause_GetFlag(nextClause, WORKEDOFF)) {
+	      if (clause_LiteralIsPositive(nextLit)) {
+		if (clause_LiteralGetFlag(nextLit,STRICTMAXIMAL) &&
+		    (!term_IsVariable(list_Car(candidates)) ||
+		     clause_HasEmptyConstraint(nextClause)) &&
+		    clause_HasSolvedConstraint(nextClause) &&
+		    !symbol_Equal(clause_LiteralPredicate(Literal),
+				  clause_LiteralPredicate(nextLit))) {
+		  /* Don't consider literals with same top symbol as given literal */
+		  /* since the given clause must be part of any inference */
+		  *Unifiers = list_Cons(nextLit, *Unifiers);
+		}
+	      } else if (clause_LiteralGetIndex(nextLit) < clause_FirstAntecedentLitIndex(nextClause) &&
+			 ((!term_IsVariable(list_Car(candidates)) && !IsFromEmptySort) ||
+			  (term_IsVariable(list_Car(candidates)) && IsFromEmptySort &&
+			   clause_HasOnlyVarsInConstraint(nextClause,Flags, Precedence)))) {
+		*ConstraintLits = list_Cons(nextLit, *ConstraintLits);
+	      }
+	    }
+	  } /* litScan */
+	}
+      }     /* atomScan */
+    }
+  }         /* candidates */
+
+  /* We have to avoid constraint literals from the same clause with the same
+     term or variable, since those would create the same result clause. */
+  *ConstraintLits =
+    list_DeleteDuplicates(*ConstraintLits,
+			  (BOOL (*)(POINTER,POINTER)) inf_LiteralsHaveSameSubtermAndAreFromSameClause);
+}
+
+static void inf_MakeClausesDisjoint(CLAUSE GClause, LIST Literals)
+/**************************************************************
+  INPUT:   A clause and a non-empty list of literals.
+  EFFECT:  All input clauses, those pointed to by the literals,
+           are variable disjointly renamed.
+***************************************************************/
+{
+  SYMBOL maxVar, maxCand;
+  CLAUSE lastClause;
+
+  maxVar     = clause_MaxVar(GClause);
+  lastClause = clause_LiteralOwningClause(list_Car(Literals));
+  clause_RenameVarsBiggerThan(lastClause, maxVar);
+  Literals   = list_Cdr(Literals);
+
+  for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) {
+    CLAUSE actClause;
+
+    clause_UpdateMaxVar(lastClause);
+    maxCand = clause_MaxVar(lastClause);    
+    maxVar = (symbol_GreaterVariable(maxVar,maxCand)? maxVar : maxCand);
+
+    actClause = clause_LiteralOwningClause(list_Car(Literals));
+    clause_RenameVarsBiggerThan(actClause, maxVar);
+  }
+}
+
+static void inf_CopyUnifierClauses(LIST Literals)
+/**************************************************************
+  INPUT:   A list of literals.
+  EFFECT:  Replaces all literals by pointers to literals of copies
+           of the respective clauses.
+***************************************************************/
+{
+  for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) {
+    CLAUSE actClause;
+    int    i;
+
+    actClause = clause_LiteralOwningClause(list_Car(Literals));
+    i         = clause_LiteralGetIndex(list_Car(Literals));
+    actClause = clause_Copy(actClause);
+    list_Rplaca(Literals, clause_GetLiteral(actClause, i)); /* Set to literal from copy */
+  }
+}
+
+static void inf_DeleteUnifierClauses(LIST Literals)
+/**************************************************************
+  INPUT:   A list of literals.
+  EFFECT:  Deletes all clauses the literals point to.
+***************************************************************/
+{
+  for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) {
+    clause_Delete(clause_LiteralOwningClause(list_Car(Literals)));
+    list_Rplaca(Literals, NULL);
+  }
+}
+
+static SORT inf_GetSortFromLits(LIST Literals, SORTTHEORY SortTheory)
+/**************************************************************
+  INPUT:   A list of literals and a sort theory.
+  RETURNS: The sort created from the literals' predicates.
+***************************************************************/
+{
+  SORT result = sort_TopSort();
+
+  for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) {
+    SORT newSort = sort_TheorySortOfSymbol(SortTheory,
+					   clause_LiteralPredicate(list_Car(Literals)));
+    
+    result = sort_Intersect(newSort, result);
+  }
+
+  list_PointerDeleteDuplicates(result);
+
+  return result;
+}
+
+static LIST inf_ApplyWeakening(CLAUSE Clause, LIST TLits, LIST Partners,
+			       CONDITION Condition, FLAGSTORE Flags,
+			       PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause, a list of constraint indices in <Clause>,
+           a list of maximal, monadic succedent literals,
+	   a subsort condition, a flag store and a precedence.
+  RETURNS: A one-element list with a clause derived from the
+           clause and the partner clauses by the Weakening or
+	   Empty Sort rule.
+           The flag store is needed to create the result clause.
+  MEMORY:  Memory is allocated for the returned list and the clause.
+***************************************************************/
+{
+  LIST   scan, parents;
+  LIST   constraint, antecedent, succedent;
+  LIST   parentClauses, parentLits;   /* clause numbers and literal indices */
+  int    i, bound, depth;
+  TERM   tSubterm;
+  CLAUSE newClause;
+
+#ifdef CHECK
+  if (!clause_IsClause(Clause, Flags, Precedence) || list_Empty(TLits) ||
+      list_Empty(Partners) || Condition == NULL) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_ApplyWeakening: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  constraint    = antecedent = succedent = list_Nil();
+  parentClauses = parentLits = list_Nil();
+  parents       = list_Nil();                      /* Used to set split data */
+  depth         = clause_Depth(Clause);
+  tSubterm      = term_FirstArgument(clause_GetLiteralAtom(Clause, (int)list_Car(TLits)));
+
+  /* Now collect the literals of the new clause */
+  /* First consider the condition atoms */
+  for (scan=sort_ConditionConstraint(Condition); !list_Empty(scan); scan=list_Cdr(scan)) {
+    TERM termCopy;
+
+    termCopy = term_Copy(list_Car(scan));
+    term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm);
+    constraint = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy),
+			   constraint);
+    term_Delete(termCopy);   /* constraint contains a copy */
+  }
+  for (scan=sort_ConditionAntecedent(Condition); !list_Empty(scan); scan=list_Cdr(scan)) {
+    TERM termCopy;
+
+    termCopy = term_Copy(list_Car(scan));
+    term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm);
+    antecedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy),
+			   antecedent);
+    term_Delete(termCopy);   /* antecedent contains a copy */ 
+  }
+  for (scan=sort_ConditionSuccedent(Condition); !list_Empty(scan); scan=list_Cdr(scan)) {
+    TERM termCopy;
+    
+    termCopy = term_Copy(list_Car(scan));
+    term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm);
+    succedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy),
+			  succedent);
+    term_Delete(termCopy);   /* succedent contains a copy */
+  }
+  /* update parents and depth from condition clauses */
+  for (scan=sort_ConditionClauses(Condition); !list_Empty(scan); scan=list_Cdr(scan)) {
+    CLAUSE condClause;
+
+    condClause    = list_Car(scan);
+    parents       = list_Cons(condClause, parents);
+    parentClauses = list_Cons((POINTER)clause_Number(condClause), parentClauses);
+    parentLits    = list_Cons((POINTER)clause_FirstSuccedentLitIndex(condClause), parentLits);
+    depth         = misc_Max(depth, clause_Depth(condClause));
+  }
+
+  /* Now we consider the partner clauses */
+  for (scan = Partners; !list_Empty(scan); scan = list_Cdr(scan)) {
+    LITERAL pLit;
+    CLAUSE  pClause;
+    int     pi;
+
+    pLit    = list_Car(scan);
+    pClause = clause_LiteralOwningClause(pLit);
+    pi      = clause_LiteralGetIndex(pLit);
+    bound   = clause_LastConstraintLitIndex(pClause);
+    for (i = clause_FirstLitIndex(); i <= bound; i++) {
+      constraint = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(),
+						       clause_GetLiteralAtom(pClause,i)),
+			     constraint);
+    }
+    bound = clause_LastAntecedentLitIndex(pClause);
+    for (i = clause_FirstAntecedentLitIndex(pClause); i <= bound; i++) {
+      antecedent = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(),
+						       clause_GetLiteralAtom(pClause,i)),
+			     antecedent);
+    }
+    bound = clause_LastSuccedentLitIndex(pClause);
+    for (i = clause_FirstSuccedentLitIndex(pClause); i <= bound; i++) {
+      if (i != pi)
+	succedent = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(),
+							clause_GetLiteralAtom(pClause,i)),
+			      succedent);
+    }
+
+    parents = list_Cons(pClause, parents);
+
+    parentClauses = list_Cons((POINTER)clause_Number(pClause), parentClauses);
+    parentLits    = list_Cons((POINTER) pi, parentLits);
+
+    depth = misc_Max(depth, clause_Depth(pClause));
+  }
+
+  /* Last but not least we consider the <Clause> itself */
+  bound = clause_LastConstraintLitIndex(Clause);
+  for (i = clause_FirstLitIndex(); i <= bound; i++) {
+    if (!list_PointerMember(TLits, (POINTER)i))
+	constraint = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(),
+							 clause_GetLiteralAtom(Clause,i)),
+			       constraint);
+    else {
+      parentClauses = list_Cons((POINTER)clause_Number(Clause), parentClauses);
+      parentLits    = list_Cons((POINTER)i, parentLits);
+    }
+  }
+  bound = clause_LastAntecedentLitIndex(Clause);
+  for (i = clause_FirstAntecedentLitIndex(Clause); i <= bound; i++) {
+    antecedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(),
+						     clause_GetLiteralAtom(Clause,i)),
+			   antecedent);
+  }
+  bound = clause_LastSuccedentLitIndex(Clause);
+  for (i = clause_FirstSuccedentLitIndex(Clause); i <= bound; i++) {
+    succedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(),
+						    clause_GetLiteralAtom(Clause,i)),
+			  succedent);
+  }
+
+  parents = list_Cons(Clause, parents);
+  
+  /* Now we've got all data we need */
+  newClause = clause_Create(constraint, antecedent, succedent, Flags,Precedence);
+  
+  list_Delete(constraint);
+  list_Delete(antecedent);
+  list_Delete(succedent);
+  
+  if (term_IsVariable(tSubterm))
+    clause_SetFromEmptySort(newClause);
+  else
+    clause_SetFromSortResolution(newClause);
+  
+  clause_SetDepth(newClause, depth+1);
+  clause_SetFlag(newClause, DOCCLAUSE);
+  
+  clause_SetSplitDataFromList(newClause, parents);
+  list_Delete(parents);
+  
+  clause_SetParentClauses(newClause, parentClauses);
+  clause_SetParentLiterals(newClause, parentLits);
+ 
+  return list_List(newClause);
+}
+
+static LIST inf_InternWeakening(CLAUSE Clause, LIST TLits, LIST Unifiers,
+				LITERAL Special, LIST SojuList, FLAGSTORE Flags,
+				PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A <Clause> with unsolved sort constraint,
+           a list <TLits> of constraint indices in <Clause> where
+	   all corresponding constraints have the same term,
+	   a list <Unifiers> of monadic succedent literals whose
+	   subterm is unifiable with the subterm of the <TLits>,
+	   and a flag store.
+	   If called from a backward rule the literal <Special>
+	   will be the succedent literal from the respective
+	   GivenClause, that must be part of every considered
+	   SOJU sort. If called from a forward rule <Special> is NULL.
+	   A list <SojuList> of sort pairs.
+	   A flag store and a precedence.
+  RETURNS: The list of possible resolvents.
+  EFFECT:  ATTENTION: <SojuList> is deleted.
+  MEMORY:  Memory is allocated for the returned list and the clauses.
+***************************************************************/
+{
+  LIST result, myUnifiers;
+  TERM searchTerm; 
+  int  stack;
+
+  LIST scan;
+#ifdef CHECK
+  if (!clause_IsClause(Clause, Flags, Precedence) || list_Empty(TLits) ||
+      list_Empty(Unifiers)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_InternWeakening: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  putchar('\n'); clause_Print(Clause);
+  fputs("\nT_k = ", stdout);
+  for (scan = TLits; !list_Empty(scan); scan = list_Cdr(scan)) {
+    clause_LiteralPrint(clause_GetLiteral(Clause, (int)list_Car(scan)));
+    putchar(' ');
+  }
+  fputs("\nS_k =", stdout);
+  for (scan = Unifiers; !list_Empty(scan); scan = list_Cdr(scan)) {
+    putchar('\n');
+    clause_LiteralPrint(list_Car(scan));
+    fputs(" in ", stdout);
+    clause_Print(clause_LiteralOwningClause(list_Car(scan)));
+  }
+  putchar('\n');
+
+  if (list_Empty(SojuList))
+    return list_Nil();
+
+  /*return list_Nil();*/
+  /* Und Schluss */
+
+  result = list_Nil();
+
+  myUnifiers = list_Copy(Unifiers);
+  inf_CopyUnifierClauses(myUnifiers);
+  inf_MakeClausesDisjoint(Clause, myUnifiers);
+
+  searchTerm =
+    term_FirstArgument(clause_GetLiteralAtom(Clause, (int)list_Car(TLits)));
+
+  stack  = stack_Bottom();
+
+  for ( ; !list_Empty(SojuList); SojuList = list_Pop(SojuList)) {
+    SOJU actSoju = list_Car(SojuList);
+
+    fputs("\nSOJU: ", stdout); sort_PairPrint(actSoju); fflush(stdout);
+
+    if (Special == NULL ||
+	sort_ContainsSymbol(sort_PairSort(actSoju),
+			    clause_LiteralPredicate(Special))) { 
+      LIST actSortSymbols, symbolScan, unifierScan, subset;
+
+      actSortSymbols = sort_GetSymbolsFromSort(sort_PairSort(actSoju));
+      subset         = list_Nil();
+
+      symbolScan  = actSortSymbols;
+      unifierScan = myUnifiers;
+
+      do {
+	while (!list_Empty(symbolScan) && !list_Empty(unifierScan)) {
+	  LITERAL actLit = list_Car(unifierScan);
+
+	  if (symbol_Equal(clause_LiteralPredicate(list_Car(unifierScan)),
+			   (SYMBOL)list_Car(symbolScan))) {
+	    cont_StartBinding();
+	    if (unify_UnifyNoOC(cont_LeftContext(), searchTerm, cont_RightContext(),
+				term_FirstArgument(clause_LiteralAtom(actLit)))) {
+	      /* Found corresponding literal for sort symbol */
+	      stack_Push(symbolScan);
+	      stack_Push(list_Cdr(unifierScan));
+	      subset = list_Cons(actLit, subset);
+	      /* Now search literals for the next sort symbol */
+	      symbolScan = list_Cdr(symbolScan);
+
+	      if (!list_Empty(symbolScan))
+		/* Start search for literal at the beginning of unifier list */
+		unifierScan = myUnifiers;
+	      else
+		unifierScan = list_Cdr(unifierScan);
+	    } else {
+	      cont_BackTrack();
+	      unifierScan = list_Cdr(unifierScan);
+	    }
+	  } else
+	    unifierScan = list_Cdr(unifierScan);
+	}
+
+	if (list_Empty(symbolScan)) {
+	  /*putchar('\n');
+	  clause_LiteralListPrint(subset);*/
+	  /* Found subset */
+	  result = list_Nconc(inf_ApplyWeakening(Clause, TLits, subset,
+						 sort_PairCondition(actSoju),
+						 Flags, Precedence),
+			      result);
+	}
+
+	while (!stack_Empty(stack) && list_Empty(stack_Top())) {
+	  /* No more literals */
+	  stack_NPop(2);
+	  cont_BackTrack();
+	  subset = list_Pop(subset);
+	}
+
+	if (!stack_Empty(stack)) {
+	  /* Implies that stack_Top is a non-empty list */
+	  unifierScan = stack_PopResult();
+	  symbolScan  = stack_PopResult();
+	  cont_BackTrack();
+	  subset = list_Pop(subset);
+	}
+      } while (!stack_Empty(stack) || !list_Empty(unifierScan));
+
+      list_Delete(actSortSymbols);
+    }
+    sort_PairDelete(actSoju);
+  } /* For all SOJUs */
+
+  inf_DeleteUnifierClauses(myUnifiers);
+  list_Delete(myUnifiers);
+
+  return result;
+}
+
+LIST inf_ForwardWeakening(CLAUSE GivenClause, st_INDEX Index,
+			  SORTTHEORY SortTheory, FLAGSTORE Flags,
+			  PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause, an index of clauses, a sort theory, a flag store
+           and a precedence.
+           The sort constraint of the clause must contain a non-variable term
+	   (this implies the sort constraint is unsolved). 
+  RETURNS: A list of clauses derived from the GivenClause by
+           the Weakening rule.
+  MEMORY:  Memory is allocated for the returned list and the clauses.
+***************************************************************/
+{
+  LIST    result;
+  int     i, lc;
+  BOOL    hit;
+
+#ifdef CHECK
+  if (!clause_HasTermSortConstraintLits(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_ForwardWeakening: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = list_Nil();
+  lc     = clause_LastConstraintLitIndex(GivenClause);
+  hit    = FALSE;
+
+  for (i = clause_FirstLitIndex(); i <= lc && !hit; i++) {
+    
+    if (!term_IsVariable(term_FirstArgument(clause_GetLiteralAtom(GivenClause, i)))) {
+      /* Condition implies that constraint is unsolved */
+      LITERAL tLit;
+      LIST    unifiers;
+      int     j;
+
+      tLit     = clause_GetLiteral(GivenClause, i);
+      hit      = TRUE; /* Try only the first appropriate constraint literal */
+      unifiers = inf_GetForwardPartnerLits(tLit, Index);
+
+      if (!list_Empty(unifiers)) {
+	TERM tAtom;
+	LIST tLits, sojuList;
+	SORT tSort, unifierSort;
+
+	tAtom = clause_GetLiteralAtom(GivenClause, i);
+
+	/* Search the other T_k(t) in GivenClause */
+	tLits = list_Nil();
+	tSort = sort_TopSort();
+	for (j = lc; j > i; j--) {
+	  TERM actAtom;
+	  actAtom = clause_GetLiteralAtom(GivenClause, j);
+	  if (term_FirstArgument(actAtom) == term_FirstArgument(tAtom)) {
+	    tLits = list_Cons((POINTER)j, tLits);
+	    tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)),
+				   tSort);
+	  }
+	}
+	tLits = list_Cons((POINTER)i, tLits);
+	tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)),
+			       tSort);
+	list_PointerDeleteDuplicates(tSort);
+	/* Necessary for Christoph's function */
+
+	unifierSort = inf_GetSortFromLits(unifiers, SortTheory);
+	sojuList    = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort);
+	sort_Delete(unifierSort);
+	sort_Delete(tSort);
+
+	result =
+	  list_Nconc(inf_InternWeakening(GivenClause, tLits, unifiers, NULL,
+					 sojuList, Flags, Precedence),
+		     result);
+
+	list_Delete(tLits);
+	list_Delete(unifiers);
+      }
+    }
+  }
+  return result;
+}
+
+LIST inf_BackwardWeakening(CLAUSE GivenClause, st_INDEX Index,
+			   SORTTHEORY SortTheory, FLAGSTORE Flags,
+			   PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause with solved sort constraint, an index of clauses,
+           a sort theory, a flag store and a precedence.
+  RETURNS: A list of clauses inferred from the GivenClause by
+           the Weakening rule.
+  MEMORY:  Memory is allocated for the list and the clauses.
+***************************************************************/
+{
+  LIST     result;
+  int      i, ls;
+
+#ifdef CHECK
+  if (!clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_BackwardWeakening: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = list_Nil();
+  ls     = clause_LastSuccedentLitIndex(GivenClause);
+
+  for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) {
+    LITERAL sLit;
+    TERM    sAtom;
+
+    sLit  = clause_GetLiteral(GivenClause, i);
+    sAtom = clause_LiteralAtom(sLit);
+    if (clause_LiteralGetFlag(sLit, STRICTMAXIMAL) && 
+	clause_LiteralIsSort(sLit) &&
+	(!term_IsVariable(term_FirstArgument(sAtom)) ||
+	 clause_HasEmptyConstraint(GivenClause))) {
+      LIST unifiers, partners;
+      SORT unifierSort;
+
+      unifiers = partners = list_Nil();
+      inf_GetBackwardPartnerLits(sLit,Index,&partners,&unifiers,FALSE,Flags,
+				 Precedence);
+      unifiers = list_Cons(sLit, unifiers);
+      /* <partners> holds monadic constraint literals */
+      /* <unifiers> holds monadic, maximal succedent literals */
+      unifierSort = inf_GetSortFromLits(unifiers, SortTheory);
+      
+      for ( ; !list_Empty(partners); partners = list_Pop(partners)) {
+	LITERAL tLit;
+	CLAUSE  tClause;
+	TERM    tAtom;
+	int     ti;
+	int     lc;
+	int     j;
+	LIST    tLits, sojuList;
+	SORT    tSort;
+
+	tLit    = list_Car(partners);
+	tClause = clause_LiteralOwningClause(tLit);
+	tAtom   = clause_LiteralAtom(tLit);
+	ti      = clause_LiteralGetIndex(tLit);
+	lc      = clause_LastConstraintLitIndex(tClause);
+
+	/* Search the other T_k(t) in GivenClause */
+	tLits = list_Nil();
+	tSort = sort_TopSort();
+	for (j = lc; j >= clause_FirstLitIndex(); j--) {
+	  TERM actAtom;
+
+	  actAtom = clause_GetLiteralAtom(tClause, j);
+	  if (j != ti &&
+	      term_FirstArgument(actAtom) == term_FirstArgument(tAtom)) {
+	    tLits = list_Cons((POINTER)j, tLits);
+	    tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)),
+				   tSort);
+	  }
+	}
+	tLits = list_Cons((POINTER)ti, tLits);
+	tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)),
+			       tSort);
+	list_PointerDeleteDuplicates(tSort);
+
+	sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort);
+	sort_Delete(tSort);
+
+	cont_StartBinding();
+	unify_UnifyNoOC(cont_LeftContext(), tAtom,
+			cont_RightContext(), sAtom);
+
+	result =
+	  list_Nconc(inf_InternWeakening(tClause, tLits, unifiers, sLit,
+					 sojuList, Flags, Precedence),
+		     result);
+
+	cont_BackTrack();
+
+	list_Delete(tLits);
+      }
+      sort_Delete(unifierSort);
+      list_Delete(unifiers);
+    }
+  }
+
+  return result;
+}
+
+LIST inf_ForwardEmptySortPlusPlus(CLAUSE GivenClause, st_INDEX Index,
+				  SORTTHEORY SortTheory, FLAGSTORE Flags,
+				  PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause,  an 'Index' of clauses, a sort theory, a flag store
+           and a precedence.
+           The sort constraint of the clause must not contain a
+	   non-variable term, but the sort constraint has to be unsolved.
+  RETURNS: A list of clauses derived from the GivenClause by
+           the Empty Sort rule.
+  MEMORY:  Memory is allocated for the returned list and the clauses.
+***************************************************************/
+{
+  LIST     result;
+  int      i, lc;
+  BOOL     hit;
+  
+#ifdef CHECK
+  if (clause_HasTermSortConstraintLits(GivenClause) ||
+      clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_ForwardEmptySortPlusPlus: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+  
+  result = list_Nil();
+  lc     = clause_LastConstraintLitIndex(GivenClause);
+  hit    = FALSE;
+  
+  for (i = clause_FirstLitIndex(); i <= lc && !hit; i++) {
+
+    if (term_IsVariable(term_FirstArgument(clause_GetLiteralAtom(GivenClause,i)))) {
+      LITERAL tLit;
+      TERM    var;
+      int     j, ls;
+      BOOL varOccursNoMore;
+
+      tLit            = clause_GetLiteral(GivenClause, i);
+      var             = term_FirstArgument(clause_LiteralAtom(tLit));
+      ls              = clause_LastSuccedentLitIndex(GivenClause);
+      varOccursNoMore = TRUE;
+      /* Check if the variable occurs in antecedent or succedent literals */
+      for (j = clause_FirstAntecedentLitIndex(GivenClause); 
+	   (j <= ls) && varOccursNoMore; j++) {
+	if (term_ContainsSymbol(clause_GetLiteralAtom(GivenClause,j),
+				term_TopSymbol(var)))
+	  varOccursNoMore = FALSE;
+      }
+		
+      if (varOccursNoMore) {
+	/* Condition implies that constraint is unsolved */
+	LIST unifiers;
+
+	unifiers = inf_GetForwardPartnerLits(tLit, Index);
+	hit      = TRUE;  /* We found the first appropriate constraint literal */
+
+	if (!list_Empty(unifiers)) {
+	  TERM tAtom = clause_LiteralAtom(tLit);
+	  LIST tLits, sojuList;
+	  SORT tSort, unifierSort;
+
+	  /* Search the other T_k(t) in GivenClause */
+	  tLits = list_Nil();
+	  tSort = sort_TopSort();
+	  for (j = lc; j > i; j--) {
+	    TERM actAtom;
+
+	    actAtom = clause_GetLiteralAtom(GivenClause, j);
+	    if (term_FirstArgument(actAtom) == var) {   /* tClause is shared */
+	      tLits = list_Cons((POINTER)j, tLits);
+	      tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory,
+							     term_TopSymbol(actAtom)),
+				     tSort);
+	    }
+	  }
+	  tLits = list_Cons((POINTER)i, tLits);
+	  tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory,
+							 term_TopSymbol(tAtom)),
+				 tSort);
+	  list_PointerDeleteDuplicates(tSort);
+
+	  unifierSort = inf_GetSortFromLits(unifiers, SortTheory);
+	  sojuList    = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort);
+
+	  sort_Delete(unifierSort);
+	  sort_Delete(tSort);
+
+	  result =
+	    list_Nconc(inf_InternWeakening(GivenClause, tLits, unifiers, NULL,
+					   sojuList, Flags, Precedence),
+		       result);
+
+	  list_Delete(tLits);
+	  list_Delete(unifiers);
+	}
+      }
+    }
+  }
+  return result;
+}
+
+LIST inf_BackwardEmptySortPlusPlus(CLAUSE GivenClause, st_INDEX Index,
+				   SORTTHEORY SortTheory, FLAGSTORE Flags,
+				   PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause with solved sort constraint, an index of clauses,
+           a sort theory, a flag store and a precedence.
+  RETURNS: A list of clauses inferred from the GivenClause by
+           the Empty Sort rule.
+  MEMORY:  Memory is allocated for the list and the clauses.
+***************************************************************/
+{
+  LIST     result;
+  int      i, ls;
+
+#ifdef CHECK
+  if (!clause_HasSolvedConstraint(GivenClause)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In inf_BackwardEmptySortPlusPlus: Illegal input.\n");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = list_Nil();  
+  ls     = clause_LastSuccedentLitIndex(GivenClause);
+
+  for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) {
+    LITERAL sLit;
+    TERM    sAtom;
+
+    sLit  = clause_GetLiteral(GivenClause, i);
+    sAtom = clause_LiteralAtom(sLit);
+    if (clause_LiteralGetFlag(sLit,STRICTMAXIMAL) && 
+	clause_LiteralIsSort(sLit) &&
+	(!term_IsVariable(term_FirstArgument(sAtom)) ||
+	 clause_HasEmptyConstraint(GivenClause))) {
+      LIST unifiers, partners;
+      SORT unifierSort;
+
+      unifiers = partners = list_Nil();
+      inf_GetBackwardPartnerLits(sLit, Index, &partners, &unifiers, TRUE, Flags,
+				 Precedence);
+      unifiers = list_Cons(sLit, unifiers);
+      /* <partners> holds monadic constraint literals */
+      /* <unifiers> holds monadic, maximal succedent literals */
+
+      unifierSort = inf_GetSortFromLits(unifiers, SortTheory);
+
+      for ( ; !list_Empty(partners); partners = list_Pop(partners)) {
+	LITERAL tLit;
+	CLAUSE  tClause;
+	TERM    tAtom;
+	int     ti;
+	int     li;
+	TERM    var;
+	BOOL    varOccursNoMore;
+	int     j;
+
+	tLit            = list_Car(partners);
+	tClause         = clause_LiteralOwningClause(tLit);
+	tAtom           = clause_LiteralAtom(tLit);
+	ti              = clause_LiteralGetIndex(tLit);
+	li              = clause_LastSuccedentLitIndex(tClause);
+	var             = term_FirstArgument(tAtom);
+	varOccursNoMore = TRUE;
+	for (j = clause_FirstAntecedentLitIndex(tClause);
+	     j <= li && varOccursNoMore;
+	     j++) {
+	  if (term_ContainsSymbol(clause_GetLiteralAtom(tClause,j),
+				  term_TopSymbol(var)))
+	    varOccursNoMore = FALSE;
+	}
+ 
+	if (varOccursNoMore) {
+	  /* Condition implies that constraint is unsolved */
+	  int  lc;
+	  LIST tLits, sojuList;
+	  SORT tSort;
+
+	  lc  = clause_LastConstraintLitIndex(tClause);
+
+	  /* Search the other T_k(t) in GivenClause */
+	  tLits = list_Nil();
+	  tSort = sort_TopSort();
+	  for (j = lc; j >= clause_FirstLitIndex(); j--) {
+	    TERM actAtom;
+	    
+	    actAtom = clause_GetLiteralAtom(tClause, j);
+	    if (j != ti &&
+		term_TopSymbol(term_FirstArgument(actAtom)) == term_TopSymbol(var)) {
+	      tLits = list_Cons((POINTER)j, tLits);
+	      tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)),
+				     tSort);
+	    }
+	  }
+	  tLits = list_Cons((POINTER)ti, tLits);
+	  tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)),
+				 tSort);
+	  list_PointerDeleteDuplicates(tSort);
+
+	  sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort);
+	  sort_Delete(tSort);
+
+	  cont_StartBinding();
+	  unify_UnifyNoOC(cont_LeftContext(), tAtom,
+			  cont_RightContext(), sAtom);
+
+	  result =
+	    list_Nconc(inf_InternWeakening(tClause, tLits, unifiers, sLit,
+					   sojuList, Flags, Precedence),
+		       result);
+
+	  cont_BackTrack();
+
+	  list_Delete(tLits);
+	}
+      }
+      sort_Delete(unifierSort);
+      list_Delete(unifiers);
+    }
+  }
+
+  return result;
+}