/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *           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$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             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;
}