This is the mail archive of the
gcc-bugs@gcc.gnu.org
mailing list for the GCC project.
Bug in egcs.
- To: egcs-bugs at cygnus dot com
- Subject: Bug in egcs.
- From: Hans de Nivelle <nivelle at logic dot at>
- Date: Mon, 21 Sep 1998 15:11:39 +0200 (MET DST)
- Cc: pfeifer at dbai dot tuwien dot ac dot at
Dear reader,
I want to report a bug in the egcs C-compiler.
It showed up in a programm for proving first order formulae.
The program runs correctly on cc, djgpp, and other versions of gcc.
The bug shows up when compiling with optimization.
Command used:
gcc -O5 subsumption.c
./a.out
Version used:
Reading specs from /usr/local/lib/gcc-lib/alphaev56-dec-osf4.0d/egcs-2.91.57/specs
gcc version egcs-2.91.57 19980901 (egcs-1.1 release)
Operating System used:
Digital UNIX V4.0D (Rev. 878)
Computer used:
Digital AlphaPC 164 500 MHz
Firmware revision: 4.9
The problem occurs in the nested for loops, marked
with BB1.
The correct behaviour is to exit with success, through BB2.
It does this when either
Option -O5 is switched off. (just gcc subsumption.c)
The printf("*") BB1 is enabled.
The printf loop BB3 is enabled.
cc is used instead of gcc.
With -O5, without the print statements gcc produces a core dump,
and never reaches BB2.
(In the full program it hanged without crashing)
regards,
Hans de Nivelle.
nivelleatwins.uva.nl
(To replay replace at by @)
Included file subsumption.c:
/*****************************************************************/
/* file subsumption.c contains the functions that are related to */
/* subsumption. */
/*****************************************************************/
#define CLASS
/**************************/
/* Included file basics.h */
/**************************/
/*****************************************************/
/* basics.h bliksem is a resolution based */
/* theorem prover. */
/*****************************************************/
#include <stdio.h>
#include <setjmp.h>
/* your compiler may want to see one of setjmp/setjump.h here */
#include <string.h>
#include <stdlib.h>
#define MAXTERMSPACE 5000
CLASS int freetermspace;
CLASS int termspace [ MAXTERMSPACE ];
CLASS int termends [ MAXTERMSPACE ];
#define MAXARITY 16
/* The only use of this flag is when computing a multisetextension */
/* of the recursive path order. If you don't use RPO then the */
/* value does not matter. */
/* special operators: */
#define OP_NIL 0
#define OP_DOT 1
#define OP_FALSE 2
#define OP_TRUE 3
#define OP_NOT 4
#define OP_AND 5
#define OP_OR 6
#define OP_IMPLIES 7
#define OP_EQUIV 8
#define OP_FORALL 9
#define OP_EXISTS 10
#define OP_NECESSARY 11
#define OP_POSSIBLE 12
#define OP_EQUAL 13
#define OP_REWRITES 14
#define OP_LESS 15
#define OP_GREATER 16
#define OP_EQUALEQUAL 17
#define OP_LESSEQUAL 18
#define OP_GREATEREQUAL 19
#define OP_GREATERGREATER 20
#define OP_LESSLESS 21
#define OP_GREATERGREATEREQUAL 22
#define OP_LESSLESSEQUAL 23
#define OP_GREATERGREATEREQUALEQUAL 24
#define OP_LESSLESSEQUALEQUAL 25
#define OP_IN 26
#define OP_PLUS 27
#define OP_MINUS 28
#define OP_TIMES 29
#define OP_DIVIDES 30
#define OP_POW 31
#define OP_UNARYMINUS 32
#define OP_UNARYPLUS 33
/* the first non-primitive operator: */
/* For primitive operators, the entry */
/* operators []. name is useless. */
#define OP_NONPRIMITIVE 34
/********************************/
/* Included file resolution.h */
/********************************/
/**************************************************************/
/* resolution.h: The declarations relevant for resolution. */
/**************************************************************/
/**********************************************************/
/* clauses contains some other things, but it is */
/* called after its main use: */
/**********************************************************/
#define MAXCLAUSES 1000
CLASS int clauses [ MAXCLAUSES ];
CLASS int freeclauses;
/*******************************************/
/* Definition of a clause: */
/*******************************************/
#define CLAUSE_NUMBER 0
/* The number of kept clauses before this one was generated. */
#define CLAUSE_GENERATION 1
/* The generation level of this clause. Factorization */
/* is not counted, because it is considered */
/* postprocessing. */
#define CLAUSE_FILT1 2
#define CLAUSE_FILT2 3
#define CLAUSE_FILT3 4
#define CLAUSE_FILT4 5
#define CLAUSE_FILT5 6
#define CLAUSE_FILT6 7
#define CLAUSE_FILT7 8
#define CLAUSE_FILT8 9
/* Subsumption bit filter. */
/* 0 is used for an fpa that is there. 1 is used for */
/* an fpa that is not there. */
#define CLAUSE_NEXTHASH 10
/* The next clause with the same hash value. EMPTYCLAUSELIST */
/* is used to mark the end of the list. */
#define CLAUSE_NEXTINLIST 11
/* The next clause in the clause list = listinuse/ */
/* listpassive/listclauses/listunfactored/listproof. */
#define CLAUSE_DERIVATION 12
/* Reference to the derivation of the clause, see below for */
/* the structure. */
#define CLAUSE_COMP 13
/* Total complexity of the clause. */
#define CLAUSE_DEPTH 14
/* The maximal depth of the clause. */
#define CLAUSE_LENGTH 15
/* The length of the clause. */
#define CLAUSE_NRVARS 16
/* Number of variables in the clause. */
#define CLAUSE_LITERALS 17
/* Reference to the first literal. */
#define CLAUSE_MAXLITS 18
/* Reference to the first maximal literal. */
#define CLAUSE_END 19
/* Reference to the end of the clause. */
#define CLAUSE_REST 20
/* Start of the rest of the clause. */
/* So a clause has the following structure: */
/* 1. The header, on clauses [ clause ] ... */
/* clauses [ clause + CLAUSE_REST ]. */
/* 2. The derivation, on clauses [ clause + CLAUSE_DERIVATION ] */
/* ... clauses [ clause + CLAUSE_LITERALS ]. */
/* 3. The non-maximal literals, on */
/* clauses [ clause + CLAUSE_LITERALS ] ... */
/* clauses [ clause + CLAUSE_MAXLITS ]. */
/* 4. The maximal literals, on */
/* clauses [ clause + CLAUSE_MAXLITS ] ... */
/* clauses [ clause + CLAUSE_END ]. */
/* The derivation has the following form: */
/* RULE + Parents + ( PROC + parents ) * . */
/* So one rule + its parents, followed by 0 or */
/* postprocessings. */
/* Derivation rules: */
#define RULE_BINARY (-100)
/* Standard, ordered binary resolution. */
#define RULE_PARAMOD (-101)
/* Standard, ordered binary paramodulation. */
#define RULE_EQREFL (-102)
/* Standard, ordered equality reflexivity. */
#define RULE_DEMOD (-103)
/* Demodulation as a derivation rule. As */
/* paramodulation, but unordered and */
/* possibly deleting a parent. */
#define RULE_UNIT (-104)
/* As binary resolution but unordered, and */
/* possibly deleting a parent. */
#define RULE_EQDEL (-105)
/* As equality reflexivity, but unordered */
/* and possibly deleting the parent. */
#define RULE_INITIAL (-106)
/* For initial clauses. */
/* Postprocessings: */
#define PROC_SPLITPOS (-200)
#define PROC_SPLITNEG (-201)
#define PROC_DEMOD (-202)
#define PROC_UNIT (-203)
#define PROC_EQDEL (-204)
#define PROC_FACTOR (-205)
/*******************************************************/
/* Variables that control the deduction process: */
/*******************************************************/
CLASS int subssnl1;
/* If 1, then each literal must be renamed by subsumption. */
/*********************************************************/
/* Variables used during the deduction process: */
/*********************************************************/
#define MAXNRVARS 100
/* The maximal number of variables allowed in one clause. */
#define MAXCLAUSELEN 50
/* Maximal length of a clause. */
CLASS int subsentry;
/* How often the subsumption test is entered. */
CLASS int subssymbcomp;
/* How often the symbol + complexity test is */
/* passed. */
CLASS int subslitmatch;
/* How often the literals individually could */
/* be matched. */
CLASS int subsfullsubs;
/* How often the full subsumption test is */
/* entered. */
/**********************************************************/
/* Substitutions and matchings: */
/**********************************************************/
#define MAXSUBST 300
CLASS struct
{
int var;
int varorig;
int term;
int termorig;
}
subst [ MAXSUBST ];
CLASS int freesubst;
CLASS struct
{
int var;
int varorig;
}
renaming [ MAXNRVARS ];
CLASS int freerenaming;
#define MAXMATCHING 100
CLASS struct
{
int var;
int term;
}
matching [ MAXMATCHING ];
CLASS int freematching;
/* if 1, a lot of interesting debugging information will be printed. */
#define DEBUG 0
#define MAXASSIGNMENTS 500
static struct
{
int var;
int term;
}
assignments [ MAXASSIGNMENTS ];
static int freeassignments;
/* Array containing lists of sets of simple assignments. */
/* assignments [ matchstarts ] ... assignments [ matchend ] */
/* contains a set of assignnments. matchlists [ matchrest ] */
/* refers to the cdr of the list. */
/* The list gives the possible alternatives for matching */
/* a certain literal. */
#define MAXMATCHLISTS 500
static struct
{
int matchstart; /* references into assignments. */
int matchend;
int matchrest; /* reference into matchlists, -1 on end. */
}
matchlists [ MAXMATCHLISTS ];
static int freematchlists;
/* literalmatch stores a number of data on the literals in c1 on how */
/* they can be matched into c2. */
static struct
{
int matchlist; /* reference into matchlists, -1 if there is none. */
int firstfit; /* clauses [ .firstfit ] is the first literal */
/* that matches. */
int nralternatives;
int nrvariables; /* nr of variables in the matched literal. */
int notinsemtab;
}
literalmatch [ MAXCLAUSELEN ];
static int freeliteralmatch;
/* equal to the length of the first clause. */
static struct
{
int conflict; /* used in conflict. */
int m; /* the matching. */
}
semtab [ MAXCLAUSELEN ];
/* We use a semantic tableaux for the subsumption algorithm. */
/*****************************************************************/
/* Matching for flatterms: */
/*****************************************************************/
/* return 1 if term1 and term2 are equal. */
static int termsareequal( term1, term2 )
int term1;
int term2;
{
int endterm1;
int a;
#if 0
printstring( &outputfile, "termsareequal " );
printterm( &outputfile, term1 );
printstring( &outputfile, " = " );
printterm( &outputfile, term2 );
printstring( &outputfile, "?\n" );
#endif
endterm1 = termends [ term1 ];
while( term1 < endterm1 )
{
a = termspace [ term1 ++ ];
if( a != termspace [ term2 ++ ] )
return 0;
}
return 1;
}
#if DEBUG
static void printmatchlist( f, m )
bliksemfile *f;
int m;
{
int i;
for( i = matchlists [m]. matchstart;
i < matchlists [m]. matchend;
i ++ )
{
printvariable( f, assignments [i].var );
printstring( f, ":=" );
printterm( f, assignments [i]. term );
printstring( f, " ");
}
}
static void printliteralmatch ( f, clause2start )
bliksemfile *f;
int clause2start;
{
int i, j, k;
printstring( f, "Match lists:\n\n" );
for( i = 0; i < freeliteralmatch; i ++ )
{
printstring( f, "(F" );
printint( f, literalmatch [i]. firstfit - clause2start );
printstring( f, ", A" );
printint( f, literalmatch [i]. nralternatives );
printstring( f, ", V" );
printint( f, literalmatch [i]. nrvariables );
printstring( f, ", S" );
printint( f, literalmatch [i]. notinsemtab );
printstring( f, ") " );
k = literalmatch [i]. matchlist;
while( k != -1 )
{
printmatchlist( f, k );
printstring( f, "| " );
k = matchlists [k]. matchrest;
}
printstring( f, "\n" );
}
}
#endif
/* return 1 if matchlists m1 and m2 are consistent. */
/* both m1 and m2 are references into matchlists. */
/* matchlists are consistent if they do not assign */
/* different values to the same variable. */
static int matchlistsconsistent( m1, m2 )
int m1;
int m2;
{
int b1, e1;
int b2, e2;
int i, j;
b1 = matchlists [ m1 ]. matchstart;
e1 = matchlists [ m1 ]. matchend;
b2 = matchlists [ m2 ]. matchstart;
e2 = matchlists [ m2 ]. matchend;
for( i = b1; i < e1; i ++ )
{
for( j = b2; j < e2; j ++ )
{
if( assignments [i]. var == assignments [j]. var )
{
if( ! termsareequal( assignments [i]. term,
assignments [j]. term ))
return 0;
}
}
}
return 1;
}
/* try to construct a matching of term1 into term2. */
/* If none exists, then return -1. */
/* If there exists one, then put it in */
/* matchlists [ freematchlists ], and return */
/* freematchlists. */
static int makematch ( term1, term2 )
int term1;
int term2;
{
int i;
int a;
int term1end;
int firstassignment;
term1end = termends [ term1 ];
if( term1end - term1 > termends [ term2 ] - term2 )
return -1;
firstassignment = freeassignments;
while( term1 < term1end )
{
a = termspace [ term1 ++ ];
if( a < 0 )
{
for( i = firstassignment; i < freeassignments; i ++ )
{
if( assignments [i]. var == a )
{
if( ! termsareequal( assignments [i]. term, term2 ))
{
freeassignments = firstassignment;
return -1;
}
term2 = termends [ term2 ];
goto next;
}
}
assignments [ freeassignments ]. var = a;
assignments [ freeassignments ]. term = term2;
freeassignments ++ ;
if( freeassignments >= MAXASSIGNMENTS - 3 )
printf( "assignments is full" );
term2 = termends [ term2 ];
}
else
{
if( a != termspace [ term2 ++ ] )
{
freeassignments = firstassignment;
return -1;
}
}
next:
;
}
matchlists [ freematchlists ]. matchstart = firstassignment;
matchlists [ freematchlists ]. matchend = freeassignments;
matchlists [ freematchlists ]. matchrest = -1;
if( freematchlists >= MAXMATCHLISTS - 3 )
printf( "matchlists is full" );
return freematchlists ++;
}
/* try to construct a matching of term1 into term2, with the */
/* additional constraint that the matching must be a */
/* renaming. */
/* For the rest makematchsnl1 behaves the same as */
/* makematchsnl. */
static int makematchsnl1 ( term1, term2 )
int term1;
int term2;
{
int i;
int a;
int term1end;
int firstassignment;
term1end = termends [ term1 ];
if( term1end - term1 != termends [ term2 ] - term2 )
return -1;
firstassignment = freeassignments;
while( term1 < term1end )
{
a = termspace [ term1 ++ ];
if( a < 0 )
{
if( termspace [ term2 ] >= 0 )
{
freeassignments = firstassignment;
return -1;
}
for( i = firstassignment; i < freeassignments; i ++ )
{
if( assignments [i]. var == a )
{
if( ! termsareequal( assignments [i]. term, term2 ))
{
freeassignments = firstassignment;
return -1;
}
term2 = termends [ term2 ];
goto next;
}
}
for( i = firstassignment; i < freeassignments; i ++ )
{
if( termspace [ term2 ] == termspace [ assignments [i]. term ] )
{
freeassignments = firstassignment;
return -1;
}
}
assignments [ freeassignments ]. var = a;
assignments [ freeassignments ]. term = term2;
freeassignments ++ ;
if( freeassignments >= MAXASSIGNMENTS - 3 )
printf( "assignments is full" );
term2 = termends [ term2 ];
}
else
{
if( a != termspace [ term2 ++ ] )
{
freeassignments = firstassignment;
return -1;
}
}
next:
;
}
matchlists [ freematchlists ]. matchstart = firstassignment;
matchlists [ freematchlists ]. matchend = freeassignments;
matchlists [ freematchlists ]. matchrest = -1;
if( freematchlists >= MAXMATCHLISTS - 3 )
printf( "matchlists is full" );
return freematchlists ++;
}
/* this function tries to refute in a semantic tableaux manner. */
/* the backtracking for subsumption. */
/* n is the depth. */
static int subsbt( n )
int n;
{
int best, mostvar;
int i;
int m;
#if DEBUG
printf("-------------------------\n");
printf("subsbt( %d )\n", n );
for( i = 0; i < n; i ++ )
{
printf("%d: %d ", i, semtab [i].conflict );
printmatchlist( &outputfile, semtab [i]. m );
printf("\n");
}
printstring( &outputfile, "\n" );
#endif
if( n == freeliteralmatch )
{
return 1;
}
/* determine which is the best to start with. */
/* This is one which has nralternatives == 1, */
/* or otherwise the largest number of variables. */
mostvar = -1;
for( i = 0; i < freeliteralmatch; i ++ )
{
if( literalmatch [i]. notinsemtab )
{
if( literalmatch [i]. nralternatives == 1 )
{
best = i;
goto decided;
}
if( literalmatch [i]. nrvariables > mostvar )
{
best = i;
mostvar = literalmatch [i]. nrvariables;
}
}
}
decided:
#if DEBUG
printf("chosen %d\n", best );
#endif
literalmatch [ best ]. notinsemtab = 0;
for( m = literalmatch [ best ]. matchlist;
m >= 0;
m = matchlists [m]. matchrest )
{
for( i = 0; i < n; i ++ )
{
if( ! matchlistsconsistent( m, semtab [i]. m ))
{
semtab [i]. conflict = 1;
goto conflict;
}
}
semtab [n]. conflict = 0;
semtab [n]. m = m;
if( subsbt( n + 1 ))
return 1;
if( ! semtab [n]. conflict )
{
#if DEBUG
printf("%d is irrelevant\n", n );
#endif
goto notused;
}
conflict:
;
}
notused:
literalmatch [ best ]. notinsemtab = 1;
#if DEBUG
printf("failed on level %d\n", n );
#endif
return 0;
}
/* return 1 if clause1 subsumes clause2. */
int subsumes2( clause1, clause2 )
int clause1;
int clause2;
{
/* these are references into termspace: */
int clause1start, clause2start;
int clause1end, clause2end;
int clause1len, clause2len;
int i, j;
int term1, term2;
int m;
int othermatch;
clause2 = clause1;
printf("%d\n", clause1 );
/* BB3. */
#if 0
for( i = 0; i < 7; i ++ )
printf("%d ", termspace [i] );
printf("\n\n");
for( i = 0; i < 7; i ++ )
printf("%d ", termends [i] );
printf("\n\n");
#endif
for( i = 0; i < 23; i ++ )
{
printf("%d ", clauses [clause1 + i] );
}
printf("\n");
subsentry ++ ;
clause1len = clauses [ clause1 + CLAUSE_LENGTH ];
clause2len = clauses [ clause2 + CLAUSE_LENGTH ];
if( clause1len > clause2len )
return 0;
if( clauses [ clause1 + CLAUSE_COMP ] >
clauses [ clause2 + CLAUSE_COMP ] )
return 0;
if( clauses [ clause1 + CLAUSE_DEPTH ] >
clauses [ clause2 + CLAUSE_DEPTH ] )
return 0;
clause1start = clauses [ clause1 + CLAUSE_LITERALS ];
clause1end = clauses [ clause1 + CLAUSE_END ];
clause2start = clauses [ clause2 + CLAUSE_LITERALS ];
clause2end = clauses [ clause2 + CLAUSE_END ];
/* Step 1: Try a propositional matching, using the */
/* complexities. */
if( subssnl1 && clause1len > 1 )
{
for( i = clause1start; i < clause1end; i ++ )
{
for( j = clause2start; j < clause2end; j ++ )
{
term1 = clauses [i];
term2 = clauses [j];
if( termspace [ term1 ] != termspace [ term2 ] )
goto doesnotfit1;
if( termends [ term1 ] - term1 !=
termends [ term2 ] - term2 )
goto doesnotfit1;
if( termspace [ term1 ] == OP_NOT )
{
term1 ++ ; term2 ++ ;
if( termspace [ term1 ] != termspace [ term2 ] )
goto doesnotfit1;
}
literalmatch [ i - clause1start ]. firstfit = j;
goto propmatchfound1;
doesnotfit1:
;
}
/* propositional matching failed: */
return 0;
propmatchfound1:
;
}
subssymbcomp ++ ;
/* Step 2: Try to construct the complete matchings: */
freeassignments = 0;
freematchlists = 0;
for( i = clause1start; i < clause1end; i ++ )
{
for( j = literalmatch [ i - clause1start ]. firstfit;
j < clause2end; j ++ )
{
m = makematchsnl1( clauses [i], clauses [j] );
if( m >= 0 )
{
literalmatch [ i - clause1start ]. matchlist = m;
literalmatch [ i - clause1start ]. firstfit = j;
literalmatch [ i - clause1start ]. nralternatives = 1;
literalmatch [ i - clause1start ]. nrvariables =
matchlists [m]. matchend - matchlists [m]. matchstart;
goto fullmatchfound1;
}
}
/* matching failed. Bye bye! */
return 0;
fullmatchfound1:
;
}
}
else
{
/* printf("Try propositional matchings:"); */
printf("entering:\n");
for( i = clause1start; i < clause1end; i ++ )
{
for( j = clause2start; j < clause2end; j ++ )
{
#if 0
/* BB1. */
printf("*");
#endif
term1 = clauses [i];
term2 = clauses [j];
if( termspace [ term1 ] != termspace [ term2 ] )
goto doesnotfit2;
if( termends [ term1 ] - term1 >
termends [ term2 ] - term2 )
goto doesnotfit2;
if( termspace [ term1 ] == OP_NOT )
{
term1 ++ ; term2 ++ ;
if( termspace [ term1 ] != termspace [ term2 ] )
goto doesnotfit2;
}
literalmatch [ i - clause1start ]. firstfit = j;
goto propmatchfound2;
doesnotfit2:
;
}
/* propositional matching failed: */
printf("exit with 0\n");
return 0;
propmatchfound2:
;
}
/* BB2. */
printf("exit with success\n");
subssymbcomp ++ ;
/* Step 2: Try to construct the complete matchings: */
freeassignments = 0;
freematchlists = 0;
for( i = clause1start; i < clause1end; i ++ )
{
for( j = literalmatch [ i - clause1start ]. firstfit;
j < clause2end; j ++ )
{
m = makematch( clauses [i], clauses [j] );
if( m >= 0 )
{
literalmatch [ i - clause1start ]. matchlist = m;
literalmatch [ i - clause1start ]. firstfit = j;
literalmatch [ i - clause1start ]. nralternatives = 1;
literalmatch [ i - clause1start ]. nrvariables =
matchlists [m]. matchend - matchlists [m]. matchstart;
goto fullmatchfound2;
}
}
/* matching failed. Bye bye! */
return 0;
fullmatchfound2:
;
}
}
subslitmatch ++ ;
freeliteralmatch = clause1len;
/* Step 3 is to see if the matchings constructed by Step 2 */
/* can be combined. If this is the case we are lucky. */
for( i = 0; i < freeliteralmatch; i ++ )
{
for( j = 0; j < i; j ++ )
{
if( ! matchlistsconsistent(
literalmatch [ i ]. matchlist,
literalmatch [ j ]. matchlist ))
goto step4;
}
}
return 1;
step4:
/* Step 4: At this point we have been unlucky. Now we must */
/* construct all matchings, and start backtracking. */
/* First construct all possible matchings: */
/* It might be not worth the effort to continue at this */
/* moment. Maybe one can live with incomplete subsumption. */
othermatch = 0;
for( i = clause1start; i < clause1end; i ++ )
{
for( j = literalmatch [ i - clause1start ]. firstfit + 1;
j < clause2end; j ++ )
{
m = makematch( clauses [i], clauses [j] );
if( m >= 0 )
{
matchlists [m]. matchrest =
literalmatch [ i - clause1start ]. matchlist;
literalmatch [ i - clause1start ]. matchlist = m;
literalmatch [ i - clause1start ]. nralternatives ++ ;
othermatch = 1;
}
}
literalmatch [ i - clause1start ]. notinsemtab = 1;
}
#if DEBUG
printliteralmatch( &outputfile, clause2start );
#endif
if( ! othermatch )
return 0;
subsfullsubs ++ ;
#if 0
printstring( &outputfile, "full subsumption: ");
printclause( &outputfile, clause1 );
printclause( &outputfile, clause2 );
printstring( &outputfile, "\n\n" );
#endif
/* step 5: So now the real hard works starts: */
return subsbt ( 0 );
}
main( )
{
subssnl1 = 0;
clauses [0] = 11;
clauses [1] = 1;
clauses [2] = -17;
clauses [3] = -9;
clauses [4] = -1;
clauses [5] = -1;
clauses [6] = 0;
clauses [7] = -1;
clauses [8] = -1;
clauses [9] = -1;
clauses [10] = 0;
clauses [11] = 0;
clauses [12] = 20;
clauses [13] = 6;
clauses [14] = 2;
clauses [15] = 2;
clauses [16] = 2;
clauses [17] = 21;
clauses [18] = 22;
clauses [19] = 23;
clauses [20] = -106;
clauses [21] = 4;
clauses [22] = 0;
termspace [0] = 4;
termspace [1] = 54;
termspace [2] = -1;
termspace [3] = -2;
termspace [4] = 35;
termspace [5] = -1;
termspace [6] = -2;
termends [0] = 4;
termends [1] = 4;
termends [2] = 3;
termends [3] = 4;
termends [4] = 7;
termends [5] = 6;
termends [6] = 7;
subsumes2( 0, 0 );
exit(0);
}