#define o mems++
#define oo mems+= 2
#define ooo mems+= 3
#define O "%" \

#define show_basics 1
#define show_choices 2
#define show_details 4
#define show_gory_details 8
#define show_doubly_gory_details 16
#define show_unused_vars 32
#define show_big_clauses 64
#define show_scores 64
#define show_strong_comps 128
#define show_looks 256 \

#define vars_per_vchunk 341 \

#define cells_per_chunk 511 \

#define hack_in(q,t) (tmp_var*) (t|(ullng) q)  \

#define thevar(l) ((l) >>1) 
#define bar(l) ((l) ^1) 
#define poslit(x) ((x) <<1) 
#define neglit(x) (((x) <<1) +1)  \

#define sanity_checking 0 \

#define litname(l) (l) &1?"~":"",vmem[thevar(l) ].name.ch8 \

#define hack_out(q) (((ullng) q) &0x3) 
#define hack_clean(q) ((tmp_var*) ((ullng) q&-4) )  \

#define linkf(b) mem[b]
#define linkb(b) mem[(b) +1]
#define kval(b) mem[(b) +2]
#define avail(k) (((k) -2) <<2) 
#define memfree(b) ((int) mem[b]<0) 
#define memk_max_default 22 \

#define real_truth 0xfffffffe
#define near_truth 0xfffffffc
#define proto_truth 0xfffffffa
#define isfixed(l) (o,stamp[thevar(l) ]>=cs) 
#define isfree(l) (o,stamp[thevar(l) ]<real_truth) 
#define iscontrary(l) ((stamp[thevar(l) ]^l) &1) 
#define stamptrue(l) (o,stamp[thevar(l) ]= cs+(l&1) )  \

#define infty badlit \

#define height untagged
#define child min
#define root 1 \

/*2:*/
#line 101 "sat11.w"

#include <stdio.h> 
#include <stdlib.h> 
#include <string.h> 
#include "gb_flip.h"
typedef unsigned int uint;
typedef unsigned long long ullng;
/*5:*/
#line 293 "sat11.w"

typedef union{
char ch8[8];
uint u2[2];
long long lng;
}octa;
typedef struct tmp_var_struct{
octa name;
uint serial;
int stamp;
struct tmp_var_struct*next;
}tmp_var;

typedef struct vchunk_struct{
struct vchunk_struct*prev;
tmp_var var[vars_per_vchunk];
}vchunk;

/*:5*//*6:*/
#line 320 "sat11.w"

typedef struct chunk_struct{
struct chunk_struct*prev;
tmp_var*cell[cells_per_chunk];
}chunk;

/*:6*//*26:*/
#line 737 "sat11.w"

typedef struct bdata_struct{
uint addr;
uint size;
uint alloc;
uint k;
}bdata;
typedef struct idata_struct{
uint lit;
uint size;
}idata;

#line 166 "sat11k.ch"
/*:26*//*27:*/
#line 761 "sat11.w"

typedef struct tdata_struct{
uint addr;
uint size;
}tdata;
#line 191 "sat11k.ch"
typedef struct tpair_struct{
uint u,v;
}tpair;
#line 771 "sat11.w"

/*:27*//*28:*/
#line 780 "sat11.w"

typedef struct ndata_struct{
uint decision;
int branch;
int rptr,iptr,lptr;
}ndata;

/*:28*//*34:*/
#line 904 "sat11.w"

typedef struct lit_struct{
int rank;
int link;
int untagged;
int min;
int parent;
int vcomp;
int arcs;
uint bstamp;
uint dl_fail;
uint istamp;
float wnb;
uint filler;
}literal;

/*:34*//*35:*/
#line 924 "sat11.w"

typedef struct var_struct{
octa name;
int pfx,len;
}variable;

/*:35*//*88:*/
#line 2016 "sat11.w"

typedef struct cdata_struct{
uint var;
float rating;
}cdata;

/*:88*//*107:*/
#line 2414 "sat11.w"

typedef struct arc_struct{
uint tip;
int next;
}arc;

/*:107*//*119:*/
#line 2696 "sat11.w"

typedef struct ldata_struct{
uint lit;
uint offset;
}ldata;

/*:119*/
#line 108 "sat11.w"
;
/*3:*/
#line 142 "sat11.w"

int random_seed= 0;
int verbose= show_basics+show_unused_vars;
int show_choices_max= 1000000;
int hbits= 8;
int print_state_cutoff= 32*80;
int buf_size= 1024;
FILE*out_file;
char*out_name;
FILE*primary_file;
char*primary_name;
int primary_vars;
ullng imems,mems;
ullng bytes;
ullng nodes;
ullng thresh= 0;
ullng delta= 0;
ullng timeout= 0x1fffffffffffffff;
uint memk_max= memk_max_default;
#line 45 "sat11k.ch"
float alpha= 0.001;
float gamm= 0.20;
int theta64= 25;
int levelcand= 600;
int mincutoff= 30;
int max_prelook_arcs= 5000;
int dl_max_iter= 1;
float dl_rho= 0.9998;
#line 169 "sat11.w"

/*:3*//*7:*/
#line 326 "sat11.w"

char*buf;
tmp_var**hash;
uint hash_bits[93][8];
vchunk*cur_vchunk;
vchunk*last_vchunk;
tmp_var*cur_tmp_var;
tmp_var*bad_tmp_var;
chunk*cur_chunk;
tmp_var**cur_cell;
tmp_var**bad_cell;
ullng vars;
ullng clauses;
ullng nullclauses;
#line 97 "sat11k.ch"
ullng cells;
ullng bclauses;
ullng bcells;
#line 342 "sat11.w"
int non_clause;

/*:7*//*24:*/
#line 685 "sat11.w"

uint*stamp;
uint*mem;
bdata*bimp;
#line 139 "sat11k.ch"
uint*cmem,*kmem;
tdata*cinx,*kinx;

tpair*bstack;
int bptr;
int max_use;
tpair*tmem;
tdata*timp;
#line 691 "sat11.w"
uint*freevar,*freeloc;
int freevars;
uint*rstack;
int rptr;
idata*istack;
int iptr;
int iptr_max;
ndata*nstack;
int level;
literal*lmem;
variable*vmem;

/*:24*//*36:*/
#line 935 "sat11.w"

uint lits;
uint badlit;

/*:36*//*48:*/
#line 1198 "sat11.w"

int memk;

/*:48*//*60:*/
#line 1430 "sat11.w"

uint bestlit;
uint cs;
uint look_cs,dlook_cs;
int fptr,eptr,lfptr;

/*:60*//*67:*/
#line 1546 "sat11.w"

uint istamp;
uint bstamp= 32;

/*:67*//*89:*/
#line 2022 "sat11.w"

cdata*cand;
int cands;
float sum;
int no_newbies;
float*rating;
uint prefix;
int plevel;
int maxcand;

/*:89*//*108:*/
#line 2420 "sat11.w"

arc*cand_arc;
int cand_arc_alloc;
int active;
int settled;

/*:108*//*120:*/
#line 2702 "sat11.w"

ldata*look;
int looks;

/*:120*//*124:*/
#line 2787 "sat11.w"

ullng base,last_base;
uint*forcedlit;
int forcedlits,fl;
int last_change;
int looki;
uint looklit;
uint old_looklit;

/*:124*//*133:*/
#line 2988 "sat11.w"

uint*wstack;
int wptr;
float weighted_new_binaries;

/*:133*//*141:*/
#line 3147 "sat11.w"

float dl_trigger;
uint dl_truth;
int dlooki;
uint dlooklit;
uint dl_last_change;

/*:141*//*164:*/
#line 1288 "sat11k.ch"

int max_clause;
float*clause_weight;

/*:164*/
#line 109 "sat11.w"
;
/*29:*/
#line 790 "sat11.w"

void print_bimp(int l){
register uint la,ls;
printf(""O"s"O".8s ->",litname(l));
for(la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--)
printf(" "O"s"O".8s",litname(mem[la]));
printf("\n");
}

#line 220 "sat11k.ch"
/*:29*//*30:*/
#line 222 "sat11k.ch"

void print_clause(int c){
register uint la,ls;
printf(""O"d:",c);
for(la= cinx[c].addr;la<cinx[c-1].addr;la++)
printf(" "O"s"O".8s"O"s",litname(cmem[la]),
isfree(cmem[la])?"":iscontrary(cmem[la])?"-":"+");
printf(" ("O"d)\n",cinx[c].size);
}

void print_kinx(int l){
register uint la,ls;
printf("kinx["O"s"O".8s]:",litname(l));
for(la= kinx[l].addr,ls= kinx[l].size;ls;la++,ls--)
printf(" "O"d",kmem[la]);
printf("\n");
}

void print_full_kinx(int l){
register uint la,k;
printf("kinx["O"s"O".8s]:",litname(l));
for(la= kinx[l].addr,k= 0;k<kinx[l].size;k++)
printf(" "O"d",kmem[la+k]);
if(la+k!=kinx[l-1].addr){
printf(" #");
for(;la+k<kinx[l-1].addr;k++)
printf(" "O"d",kmem[la+k]);
}
printf("\n");
}
#line 822 "sat11.w"

/*:30*//*31:*/
#line 828 "sat11.w"

void sanity(void){
#line 256 "sat11k.ch"
register int c,j,k,l,la,ls,p,q,u,v;
#line 831 "sat11.w"
for(k= 0;k<vars;k++){
if(freevar[freeloc[k+1]]!=k+1)
fprintf(stderr,"freeloc["O"d] is wrong!\n",k+1);
if(freeloc[freevar[k]]!=k)
fprintf(stderr,"freevar["O"d] is wrong!\n",k);
}
for(k= 0;k<rptr;k++){
l= rstack[k];
if(freeloc[thevar(l)]<freevars)
fprintf(stderr,"literal "O"d on rstack is free!\n",l);
}
if(rptr+freevars!=vars)
fprintf(stderr,"rptr="O"d, freevars="O"d, vars="O"lld\n",rptr,freevars,vars);
/*49:*/
#line 1201 "sat11.w"

for(l= 2;l<badlit;l++){
la= bimp[l].addr,k= bimp[l].k;
if(la&((1<<k)-1))
fprintf(stderr,"addr of bimp["O"d] is clobbered (0x"O"x, k="O"d)!\n",
l,la,k);
else if(bimp[l].alloc!=1<<k)
fprintf(stderr,"alloc of bimp["O"d] is clobbered ("O"d, k="O"d)!\n",
l,bimp[l].alloc,k);
else if(bimp[l].size> bimp[l].alloc)
fprintf(stderr,"size of bimp["O"d] is clobbered ("O"d>"O"d)!\n",
l,bimp[l].size,bimp[l].alloc);
else if(la>=1<<memk)
fprintf(stderr,"addr of bimp["O"d] is out of bounds (0x"O"d>0x"O"d)!\n",
l,la,1<<memk);
else if(memfree(la))
fprintf(stderr,"block 0x"O"x of bimp["O"d] isn't reserved!\n",
la,l);
else for(j= bimp[l].size-1;j>=0;j--)if(mem[la+j]<2||mem[la+j]>=badlit)
fprintf(stderr,"literal "O"d in bimp["O"d] is out of bounds!\n",
mem[la+j],l);
}
for(k= 2;k<memk;k++){
for(p= ~mem[avail(k)];;p= ~linkf(p)){
if((p&((1<<k)-1))&&p!=avail(k))
fprintf(stderr,"link in avail("O"d) is clobbered (0x"O"x)!\n",
k,p);
else if(p>=1<<memk)
fprintf(stderr,"link in avail("O"d) is out of bounds (0x"O"d>0x"O"d)!\n",
k,p,1<<memk);
else if(kval(p)!=k)
fprintf(stderr,"kval of 0x"O"x in avail("O"d) is "O"d!\n",
p,k,kval(p));
else if(memfree(p^(1<<k))&&kval(p^(1<<k))==k)
fprintf(stderr,"buddy of 0x"O"x in avail("O"d) is also in that list!\n",
p,k);
else if(~linkf(~linkb(p))!=p)
fprintf(stderr,"linking anomaly at 0x"O"x in avail("O"d)!\n",
p,k);
if(~linkf(p)==avail(k))break;
}
}

/*:49*/
#line 844 "sat11.w"
;
#line 285 "sat11k.ch"
/*32:*/
#line 303 "sat11k.ch"

for(c= bclauses;c;c--){
for(la= cinx[c].addr,k= ls= cinx[c-1].addr-la,j= 0;ls;la++,ls--){
l= cmem[la];
if(isfree(l))continue;
if(iscontrary(l))j++;
else goto inactive;
}
if(j>=k-2){
if(cinx[c].size!=2)
fprintf(stderr,"ex-big clause "O"d has size "O"d!\n",c,cinx[c].size);
goto inactive;
}
if(cinx[c].size!=k-j)
fprintf(stderr,"big clause "O"d has size "O"d not "O"d\n",c,cinx[c].size,k-j);
continue;
inactive:cinx[c].size= ~cinx[c].size;
}
for(l= 2;l<badlit;l++)if(isfree(l)){
for(la= kinx[l].addr,ls= kinx[l].size;ls;la++,ls--){
c= kmem[la];
if((int)cinx[c].size<0)
fprintf(stderr,"kinx["O"s"O".8s] includes active clause "O"d!\n",
litname(l),c);
}
for(;la<kinx[l-1].addr;la++){
c= kmem[la];
if((int)cinx[c].size>=0)
fprintf(stderr,"kinx["O"s"O".8s] omits active clause "O"d!\n",
litname(l),c);
}
}
for(c= bclauses;c;c--)if((int)cinx[c].size<0)cinx[c].size= ~cinx[c].size;
#line 870 "sat11.w"

/*:32*/
#line 285 "sat11k.ch"
;
}

/*:31*//*33:*/
#line 882 "sat11.w"

void print_state(int lev){
register int k,r;
fprintf(stderr," after "O"lld mems:",mems);
for(k= r= 0;k<lev;k++){
for(;r<nstack[k].rptr;r++)
fprintf(stderr,""O"c",'6'+(rstack[r]&1));
if(nstack[k].branch<0)fprintf(stderr,"|");
else fprintf(stderr,""O"c",'0'+(rstack[r++]&1)+(nstack[k].branch<<1));
for(;r<nstack[k+1].lptr;r++)
fprintf(stderr,""O"c",'4'+(rstack[r]&1));
if(k>=print_state_cutoff){
fprintf(stderr,"...");break;
}
}
fprintf(stderr,"\n");
fflush(stderr);
}

/*:33*//*50:*/
#line 1252 "sat11.w"

void resize(register int l){
register uint a,j,k,kk,n,p,q,r,s;
mems+= 4;
oo,a= bimp[l].addr,n= bimp[l].size,k= bimp[l].k,s= 1<<k,p= a^s;
if((o,memfree(p))&&(o,kval(p)==k))/*51:*/
#line 1266 "sat11.w"

{
/*52:*/
#line 1275 "sat11.w"

q= ~linkb(p),r= ~linkf(p);
oo,linkf(q)= ~r,linkb(r)= ~q;

/*:52*/
#line 1268 "sat11.w"
;
if((a&s)==0)goto finish;
oo,mem[p]= mem[a];
for(j= 1;j<n;j++)oo,mem[p+j]= mem[a+j];
o,bimp[l].addr= p;
}

/*:51*/
#line 1257 "sat11.w"

else/*53:*/
#line 1282 "sat11.w"

{
/*54:*/
#line 1291 "sat11.w"

for(kk= k+1;kk<memk;kk++)
if(o,linkf(avail(kk))!=~avail(kk)){
p= ~linkf(avail(kk));
o;/*52:*/
#line 1275 "sat11.w"

q= ~linkb(p),r= ~linkf(p);
oo,linkf(q)= ~r,linkb(r)= ~q;

/*:52*/
#line 1295 "sat11.w"
;
goto found;
}
if(memk==memk_max){
fprintf(stderr,"Sorry... more memory is needed! (Try option m"O"d.)\n",
memk_max+1);
fprintf(stderr,"Job aborted after "O"llu mems, "O"llu nodes.\n",mems,nodes);
exit(-666);
}
p= 1<<memk;
o,linkf(avail(memk))= linkb(avail(memk))= ~avail(memk);
o,kval(avail(memk))= memk;
bytes+= p*sizeof(uint),memk++;
found:
while(--kk> k)/*55:*/
#line 1311 "sat11.w"

{
o,q= ~linkf(avail(kk)),r= p+(1<<kk);
oo,linkf(avail(kk))= linkb(q)= ~r;
oo,linkb(r)= ~avail(kk),linkf(r)= ~q,kval(r)= kk;
}

/*:55*/
#line 1309 "sat11.w"
;

/*:54*/
#line 1284 "sat11.w"
;
oo,mem[p]= mem[a];
for(j= 1;j<n;j++)oo,mem[p+j]= mem[a+j];
/*56:*/
#line 1321 "sat11.w"

o,q= ~linkf(avail(k));
oo,linkf(avail(k))= linkb(q)= ~a;
oo,linkb(a)= ~avail(k),linkf(a)= ~q,kval(a)= k;

/*:56*/
#line 1287 "sat11.w"
;
o,bimp[l].addr= p;
}

/*:53*/
#line 1258 "sat11.w"
;
finish:o,bimp[l].alloc= s+s,bimp[l].k= k+1;
}

/*:50*//*61:*/
#line 1439 "sat11.w"

void print_truths(uint cs){
register int x;
if(cs>=proto_truth){
switch((cs-proto_truth)>>1){
case 0:fprintf(stderr,"proto_truths or better:");break;
case 1:fprintf(stderr,"near_truths or better:");break;
case 2:fprintf(stderr,"real_truths:");break;
}
}else fprintf(stderr,"truths at least "O"d:",
cs);
for(x= 1;x<=vars;x++)if(stamp[x]>=cs)
fprintf(stderr," "O"s"O".8s",
stamp[x]&1?"~":"",vmem[x].name.ch8);
fprintf(stderr,"\n");
}

void print_proto_truths(void){
print_truths(proto_truth);
}

void print_near_truths(void){
print_truths(near_truth);
}

void print_real_truths(void){
print_truths(real_truth);
}

/*:61*//*154:*/
#line 3371 "sat11.w"

void confusion(char*id){
fprintf(stderr,"This can't happen ("O"s)!\n",id);
exit(-666);
}

void debugstop(int foo){
fprintf(stderr,"You rang("O"d)?\n",foo);
}

#line 1177 "sat11k.ch"
/*:154*/
#line 110 "sat11.w"
;
main(int argc,char*argv[]){
#line 20 "sat11k.ch"
register int au,av,aw,h,i,j,jj,k,kk,l,ll,p,pp,q,qq,r,s,cia,cis,ci;
#line 113 "sat11.w"
register int c,cc,hh,la,lp,ls,ola,ols,tla,tls,tll,sl,su,sv,sw;
register int t,tt,u,uu,v0,v,vv,w,ww,x,y,xl,pu,aa,ss,pv,ua,va;
/*4:*/
#line 235 "sat11.w"

for(j= argc-1,k= 0;j;j--)switch(argv[j][0]){
case'v':k|= (sscanf(argv[j]+1,""O"d",&verbose)-1);break;
case'c':k|= (sscanf(argv[j]+1,""O"d",&show_choices_max)-1);break;
case'H':k|= (sscanf(argv[j]+1,""O"d",&print_state_cutoff)-1);break;
case'h':k|= (sscanf(argv[j]+1,""O"d",&hbits)-1);break;
case'b':k|= (sscanf(argv[j]+1,""O"d",&buf_size)-1);break;
case's':k|= (sscanf(argv[j]+1,""O"d",&random_seed)-1);break;
case'd':k|= (sscanf(argv[j]+1,""O"lld",&delta)-1);thresh= delta;break;
case'm':k|= (sscanf(argv[j]+1,""O"d",&memk_max)-1);break;
case'a':k|= (sscanf(argv[j]+1,""O"f",&alpha)-1);break;
#line 73 "sat11k.ch"
case'g':k|= (sscanf(argv[j]+1,""O"f",&gamm)-1);break;
case't':k|= (sscanf(argv[j]+1,""O"d",&theta64)-1);break;
#line 248 "sat11.w"
case'p':k|= (sscanf(argv[j]+1,""O"d",&levelcand)-1);break;
case'q':k|= (sscanf(argv[j]+1,""O"d",&mincutoff)-1);break;
case'z':k|= (sscanf(argv[j]+1,""O"d",&max_prelook_arcs)-1);break;
case'i':k|= (sscanf(argv[j]+1,""O"d",&dl_max_iter)-1);break;
case'r':k|= (sscanf(argv[j]+1,""O"f",&dl_rho)-1);break;
case'x':out_name= argv[j]+1,out_file= fopen(out_name,"w");
if(!out_file)
fprintf(stderr,"I can't open file `"O"s' for output!\n",out_name);
break;
case'V':primary_name= argv[j]+1,primary_file= fopen(primary_name,"r");
if(!primary_file)
fprintf(stderr,"I can't open file `"O"s' for input!\n",primary_name);
break;
case'T':k|= (sscanf(argv[j]+1,""O"lld",&timeout)-1);break;
default:k= 1;
}
#line 85 "sat11k.ch"
if(k||hbits<0||hbits> 30||buf_size<=0||memk_max<2||memk_max> 31||
alpha<=0.0||gamm<=0||theta64<0||levelcand<=0||
mincutoff<=0||max_prelook_arcs<=0||dl_max_iter<=0){
fprintf(stderr,
"Usage: "O"s [v<n>] [c<n>] [h<n>] [b<n>] [s<n>] [d<n>] [m<n>] ",argv[0]);
fprintf(stderr," [H<n>] [g<f>] [a<f>] [t<n>] [p<n>] [q<n] [z<n>]");
fprintf(stderr," [i<n>] [r<f>] [x<foo>] [V<foo>] [T<n>] < foo.sat\n");
#line 271 "sat11.w"
exit(-1);
}

/*:4*/
#line 115 "sat11.w"
;
/*8:*/
#line 344 "sat11.w"

gb_init_rand(random_seed);
buf= (char*)malloc(buf_size*sizeof(char));
if(!buf){
fprintf(stderr,"Couldn't allocate the input buffer (buf_size="O"d)!\n",
buf_size);
exit(-2);
}
hash= (tmp_var**)malloc(sizeof(tmp_var)<<hbits);
if(!hash){
fprintf(stderr,"Couldn't allocate "O"d hash list heads (hbits="O"d)!\n",
1<<hbits,hbits);
exit(-3);
}
for(h= 0;h<1<<hbits;h++)hash[h]= NULL;

/*:8*//*15:*/
#line 522 "sat11.w"

for(j= 92;j;j--)for(k= 0;k<8;k++)
hash_bits[j][k]= gb_next_rand();

/*:15*/
#line 116 "sat11.w"
;
/*9:*/
#line 373 "sat11.w"

if(primary_file)/*10:*/
#line 418 "sat11.w"

{
while(1){
if(!fgets(buf,buf_size,primary_file))break;
if(buf[strlen(buf)-1]!='\n'){
fprintf(stderr,
"The clause on line "O"lld ("O".20s...) is too long for me;\n",clauses,buf);
fprintf(stderr," my buf_size is only "O"d!\n",buf_size);
fprintf(stderr,"Please use the command-line option b<newsize>.\n");
exit(-4);
}
/*11:*/
#line 439 "sat11.w"

for(j= k= non_clause= 0;!non_clause;){
while(buf[j]==' ')j++;
if(buf[j]=='\n')break;
if(buf[j]<' '||buf[j]> '~'){
fprintf(stderr,"Illegal character (code #"O"x) in the clause on line "O"lld!\n",
buf[j],clauses);
exit(-5);
}
if(buf[j]=='~')i= 1,j++;
else i= 0;
/*12:*/
#line 472 "sat11.w"

{
register tmp_var*p;
if(cur_tmp_var==bad_tmp_var)/*13:*/
#line 493 "sat11.w"

{
register vchunk*new_vchunk;
new_vchunk= (vchunk*)malloc(sizeof(vchunk));
if(!new_vchunk){
fprintf(stderr,"Can't allocate a new vchunk!\n");
exit(-6);
}
new_vchunk->prev= cur_vchunk,cur_vchunk= new_vchunk;
cur_tmp_var= &new_vchunk->var[0];
bad_tmp_var= &new_vchunk->var[vars_per_vchunk];
}

/*:13*/
#line 475 "sat11.w"
;
/*16:*/
#line 526 "sat11.w"

cur_tmp_var->name.lng= 0;
for(h= l= 0;buf[j+l]> ' '&&buf[j+l]<='~';l++){
if(l> 7){
fprintf(stderr,
"Variable name "O".9s... in the clause on line "O"lld is too long!\n",
buf+j,clauses);
exit(-8);
}
h^= hash_bits[buf[j+l]-'!'][l];
cur_tmp_var->name.ch8[l]= buf[j+l];
}
if(l==0)non_clause= 1;
else j+= l,h&= (1<<hbits)-1;

/*:16*/
#line 477 "sat11.w"
;
if(!non_clause){
/*17:*/
#line 541 "sat11.w"

for(p= hash[h];p;p= p->next)
if(p->name.lng==cur_tmp_var->name.lng)break;
if(!p){
p= cur_tmp_var++;
p->next= hash[h],hash[h]= p;
p->serial= vars++;
p->stamp= 0;
}

/*:17*/
#line 479 "sat11.w"
;
if(clauses&&(p->stamp==clauses||p->stamp==-clauses))
/*18:*/
#line 555 "sat11.w"

{
if((p->stamp> 0)==(i> 0))non_clause= 1;
}

/*:18*/
#line 481 "sat11.w"

else{
p->stamp= (i?-clauses:clauses);
if(cur_cell==bad_cell)/*14:*/
#line 506 "sat11.w"

{
register chunk*new_chunk;
new_chunk= (chunk*)malloc(sizeof(chunk));
if(!new_chunk){
fprintf(stderr,"Can't allocate a new chunk!\n");
exit(-7);
}
new_chunk->prev= cur_chunk,cur_chunk= new_chunk;
cur_cell= &new_chunk->cell[0];
bad_cell= &new_chunk->cell[cells_per_chunk];
}

/*:14*/
#line 484 "sat11.w"
;
*cur_cell= p;
if(i==1)*cur_cell= hack_in(*cur_cell,1);
if(k==0)*cur_cell= hack_in(*cur_cell,2);
cur_cell++,k++;
}
}
}

/*:12*/
#line 450 "sat11.w"
;
}
if(k==0&&!non_clause){
fprintf(stderr,"(Empty line "O"lld is being ignored)\n",clauses);
nullclauses++;
}
if(non_clause)/*19:*/
#line 565 "sat11.w"

{
while(k){
/*20:*/
#line 576 "sat11.w"

if(cur_cell> &cur_chunk->cell[0])cur_cell--;
else{
register chunk*old_chunk= cur_chunk;
cur_chunk= old_chunk->prev;free(old_chunk);
bad_cell= &cur_chunk->cell[cells_per_chunk];
cur_cell= bad_cell-1;
}

/*:20*/
#line 568 "sat11.w"
;
k--;
}
if(non_clause&&((buf[0]!='~')||(buf[1]!=' ')))
fprintf(stderr,"(The clause on line "O"lld is always satisfied)\n",clauses);
nullclauses++;
}

/*:19*/
#line 456 "sat11.w"

else{
#line 110 "sat11k.ch"
if(k>=3)bclauses++,bcells+= k;
if(k> max_clause)max_clause= k;
#line 465 "sat11.w"
}
cells+= k;

/*:11*/
#line 429 "sat11.w"
;
/*19:*/
#line 565 "sat11.w"

{
while(k){
/*20:*/
#line 576 "sat11.w"

if(cur_cell> &cur_chunk->cell[0])cur_cell--;
else{
register chunk*old_chunk= cur_chunk;
cur_chunk= old_chunk->prev;free(old_chunk);
bad_cell= &cur_chunk->cell[cells_per_chunk];
cur_cell= bad_cell-1;
}

/*:20*/
#line 568 "sat11.w"
;
k--;
}
if(non_clause&&((buf[0]!='~')||(buf[1]!=' ')))
fprintf(stderr,"(The clause on line "O"lld is always satisfied)\n",clauses);
nullclauses++;
}

/*:19*/
#line 430 "sat11.w"
;
}
cells= nullclauses= 0;
primary_vars= vars;
if(verbose&show_basics)
fprintf(stderr,"("O"d primary variables read from "O"s)\n",
primary_vars,primary_name);
}

/*:10*/
#line 374 "sat11.w"
;
while(1){
if(!fgets(buf,buf_size,stdin))break;
clauses++;
if(buf[strlen(buf)-1]!='\n'){
fprintf(stderr,
"The clause on line "O"lld ("O".20s...) is too long for me;\n",clauses,buf);
fprintf(stderr," my buf_size is only "O"d!\n",buf_size);
fprintf(stderr,"Please use the command-line option b<newsize>.\n");
exit(-4);
}
/*11:*/
#line 439 "sat11.w"

for(j= k= non_clause= 0;!non_clause;){
while(buf[j]==' ')j++;
if(buf[j]=='\n')break;
if(buf[j]<' '||buf[j]> '~'){
fprintf(stderr,"Illegal character (code #"O"x) in the clause on line "O"lld!\n",
buf[j],clauses);
exit(-5);
}
if(buf[j]=='~')i= 1,j++;
else i= 0;
/*12:*/
#line 472 "sat11.w"

{
register tmp_var*p;
if(cur_tmp_var==bad_tmp_var)/*13:*/
#line 493 "sat11.w"

{
register vchunk*new_vchunk;
new_vchunk= (vchunk*)malloc(sizeof(vchunk));
if(!new_vchunk){
fprintf(stderr,"Can't allocate a new vchunk!\n");
exit(-6);
}
new_vchunk->prev= cur_vchunk,cur_vchunk= new_vchunk;
cur_tmp_var= &new_vchunk->var[0];
bad_tmp_var= &new_vchunk->var[vars_per_vchunk];
}

/*:13*/
#line 475 "sat11.w"
;
/*16:*/
#line 526 "sat11.w"

cur_tmp_var->name.lng= 0;
for(h= l= 0;buf[j+l]> ' '&&buf[j+l]<='~';l++){
if(l> 7){
fprintf(stderr,
"Variable name "O".9s... in the clause on line "O"lld is too long!\n",
buf+j,clauses);
exit(-8);
}
h^= hash_bits[buf[j+l]-'!'][l];
cur_tmp_var->name.ch8[l]= buf[j+l];
}
if(l==0)non_clause= 1;
else j+= l,h&= (1<<hbits)-1;

/*:16*/
#line 477 "sat11.w"
;
if(!non_clause){
/*17:*/
#line 541 "sat11.w"

for(p= hash[h];p;p= p->next)
if(p->name.lng==cur_tmp_var->name.lng)break;
if(!p){
p= cur_tmp_var++;
p->next= hash[h],hash[h]= p;
p->serial= vars++;
p->stamp= 0;
}

/*:17*/
#line 479 "sat11.w"
;
if(clauses&&(p->stamp==clauses||p->stamp==-clauses))
/*18:*/
#line 555 "sat11.w"

{
if((p->stamp> 0)==(i> 0))non_clause= 1;
}

/*:18*/
#line 481 "sat11.w"

else{
p->stamp= (i?-clauses:clauses);
if(cur_cell==bad_cell)/*14:*/
#line 506 "sat11.w"

{
register chunk*new_chunk;
new_chunk= (chunk*)malloc(sizeof(chunk));
if(!new_chunk){
fprintf(stderr,"Can't allocate a new chunk!\n");
exit(-7);
}
new_chunk->prev= cur_chunk,cur_chunk= new_chunk;
cur_cell= &new_chunk->cell[0];
bad_cell= &new_chunk->cell[cells_per_chunk];
}

/*:14*/
#line 484 "sat11.w"
;
*cur_cell= p;
if(i==1)*cur_cell= hack_in(*cur_cell,1);
if(k==0)*cur_cell= hack_in(*cur_cell,2);
cur_cell++,k++;
}
}
}

/*:12*/
#line 450 "sat11.w"
;
}
if(k==0&&!non_clause){
fprintf(stderr,"(Empty line "O"lld is being ignored)\n",clauses);
nullclauses++;
}
if(non_clause)/*19:*/
#line 565 "sat11.w"

{
while(k){
/*20:*/
#line 576 "sat11.w"

if(cur_cell> &cur_chunk->cell[0])cur_cell--;
else{
register chunk*old_chunk= cur_chunk;
cur_chunk= old_chunk->prev;free(old_chunk);
bad_cell= &cur_chunk->cell[cells_per_chunk];
cur_cell= bad_cell-1;
}

/*:20*/
#line 568 "sat11.w"
;
k--;
}
if(non_clause&&((buf[0]!='~')||(buf[1]!=' ')))
fprintf(stderr,"(The clause on line "O"lld is always satisfied)\n",clauses);
nullclauses++;
}

/*:19*/
#line 456 "sat11.w"

else{
#line 110 "sat11k.ch"
if(k>=3)bclauses++,bcells+= k;
if(k> max_clause)max_clause= k;
#line 465 "sat11.w"
}
cells+= k;

/*:11*/
#line 385 "sat11.w"
;
}
if(!primary_file)primary_vars= vars;
if((vars>>hbits)>=10){
fprintf(stderr,"There are "O"lld variables but only "O"d hash tables;\n",
vars,1<<hbits);
while((vars>>hbits)>=10)hbits++;
fprintf(stderr," maybe you should use command-line option h"O"d?\n",hbits);
}
clauses-= nullclauses;
if(clauses==0){
fprintf(stderr,"No clauses were input!\n");
exit(-77);
}
if(vars>=0x80000000){
fprintf(stderr,"Whoa, the input had "O"llu variables!\n",vars);
exit(-664);
}
if(clauses>=0x80000000){
fprintf(stderr,"Whoa, the input had "O"llu clauses!\n",clauses);
exit(-665);
}
if(cells>=0x100000000){
fprintf(stderr,"Whoa, the input had "O"llu occurrences of literals!\n",cells);
exit(-666);
}

/*:9*/
#line 117 "sat11.w"
;
if(verbose&show_basics)
/*22:*/
#line 597 "sat11.w"

fprintf(stderr,
"("O"lld variables, "O"lld clauses, "O"llu literals successfully read)\n",
vars,clauses,cells);

/*:22*/
#line 119 "sat11.w"
;
/*37:*/
#line 939 "sat11.w"

lits= vars<<1,badlit= lits+2;
last_vchunk= cur_vchunk;
/*38:*/
#line 951 "sat11.w"

stamp= (uint*)malloc((vars+1)*sizeof(uint));
if(!stamp){
fprintf(stderr,"Oops, I can't allocate the stamp array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(uint);

bimp= (bdata*)malloc(badlit*sizeof(bdata));
if(!bimp){
fprintf(stderr,"Oops, I can't allocate the bimp array!\n");
exit(-10);
}
bytes+= badlit*sizeof(bdata);
/*57:*/
#line 1330 "sat11.w"

for(memk= 4;1<<memk<4*(memk_max-2+lits);memk++);
if(memk> memk_max){
fprintf(stderr,"The value of memk_max is way too small for "O"d literals!\n",
lits);
exit(-667);
}
mem= (uint*)malloc((1<<memk_max)*sizeof(uint));
if(!mem){
fprintf(stderr,"Oops, I can't allocate the mem array!\n");
exit(-10);
}
bytes+= (1<<memk)*sizeof(uint);
j= avail(memk_max);
for(l= 2;l<badlit;l++){
oo,mem[j]= 0,bimp[l].addr= j,bimp[l].size= 0,j+= 4;
o,bimp[l].alloc= 4,bimp[l].k= 2;
}
for(k= 2;k<memk;k++){
if(j&(1<<k)){
o,linkf(avail(k))= linkb(avail(k))= ~j;
o,linkf(j)= linkb(j)= ~avail(k);
oo,kval(avail(k))= kval(j)= k;
j+= 1<<k;
}else{
o,linkf(avail(k))= linkb(avail(k))= ~avail(k);
o,kval(avail(k))= k;
}
}

/*:57*/
#line 965 "sat11.w"
;

#line 351 "sat11k.ch"
cinx= (tdata*)malloc((bclauses+1)*sizeof(tdata));
if(!cinx){
fprintf(stderr,"Oops, I can't allocate the cinx array!\n");
exit(-10);
}
bytes+= (bclauses+1)*sizeof(tdata);
cmem= (uint*)malloc(bcells*sizeof(uint));
if(!cmem){
fprintf(stderr,"Oops, I can't allocate the cmem array!\n");
exit(-10);
}
kinx= (tdata*)malloc(badlit*sizeof(tdata));
if(!kinx){
fprintf(stderr,"Oops, I can't allocate the cmem array!\n");
exit(-10);
}
bytes+= badlit*sizeof(tdata);
kmem= (uint*)malloc(bcells*sizeof(uint));
if(!kmem){
fprintf(stderr,"Oops, I can't allocate the kmem array!\n");
exit(-10);
}
bytes+= bcells*sizeof(uint);
#line 979 "sat11.w"

freevar= (uint*)malloc(vars*sizeof(uint));
if(!freevar){
fprintf(stderr,"Oops, I can't allocate the freevar array!\n");
exit(-10);
}
bytes+= vars*sizeof(uint);
freeloc= (uint*)malloc((vars+1)*sizeof(uint));
if(!freeloc){
fprintf(stderr,"Oops, I can't allocate the freeloc array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(uint);
for(k= 0;k<vars;k++){
mems+= 4,j= gb_unif_rand(k+1);
if(j!=k){
o,i= freevar[j];
oo,freevar[k]= i,freeloc[i]= k;
oo,freevar[j]= k+1,freeloc[k+1]= j;
}else oo,freevar[k]= k+1,freeloc[k+1]= k;
}
freevars= vars;

/*:38*//*39:*/
#line 1006 "sat11.w"

rstack= (uint*)malloc((vars+1)*sizeof(uint));
if(!rstack){
fprintf(stderr,"Oops, I can't allocate the rstack array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(uint);

nstack= (ndata*)malloc((vars+1)*sizeof(ndata));
if(!nstack){
fprintf(stderr,"Oops, I can't allocate the nstack array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(ndata);

lmem= (literal*)malloc(badlit*sizeof(literal));
if(!lmem){
fprintf(stderr,"Oops, I can't allocate the lmem array!\n");
exit(-10);
}
bytes+= badlit*sizeof(literal);
for(l= 2;l<badlit;l++)oo,lmem[l].dl_fail= lmem[l].bstamp= lmem[l].istamp= 0;

vmem= (variable*)malloc((vars+1)*sizeof(variable));
if(!vmem){
fprintf(stderr,"Oops, I can't allocate the vmem array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(variable);

forcedlit= (uint*)malloc(vars*sizeof(uint));
if(!forcedlit){
fprintf(stderr,"Oops, I can't allocate the forcedlit array!\n");
exit(-10);
}
bytes+= vars*sizeof(uint);

#line 385 "sat11k.ch"
/*:39*/
#line 942 "sat11.w"
;
/*46:*/
#line 1143 "sat11.w"

for(c= vars;c;c--){
/*21:*/
#line 588 "sat11.w"

if(cur_tmp_var> &cur_vchunk->var[0])cur_tmp_var--;
else{
register vchunk*old_vchunk= cur_vchunk;
cur_vchunk= old_vchunk->prev;
bad_tmp_var= &cur_vchunk->var[vars_per_vchunk];
cur_tmp_var= bad_tmp_var-1;
}

/*:21*/
#line 1145 "sat11.w"
;
o,vmem[c].name.lng= cur_tmp_var->name.lng;
o,vmem[c].len= vars+1;
}

/*:46*/
#line 943 "sat11.w"
;
/*40:*/
#line 386 "sat11k.ch"

forcedlits= 0,cs= proto_truth;
for(l= 2;l<badlit;l++)o,kinx[l].addr= kinx[l].size= 0;
for(c= clauses,k= 0,cc= bclauses;c;c--){
la= k;
/*41:*/
#line 1059 "sat11.w"

for(i= j= 0;i<2;){
/*20:*/
#line 576 "sat11.w"

if(cur_cell> &cur_chunk->cell[0])cur_cell--;
else{
register chunk*old_chunk= cur_chunk;
cur_chunk= old_chunk->prev;free(old_chunk);
bad_cell= &cur_chunk->cell[cells_per_chunk];
cur_cell= bad_cell-1;
}

/*:20*/
#line 1061 "sat11.w"
;
i= hack_out(*cur_cell);
p= hack_clean(*cur_cell)->serial;
p+= p+(i&1);
#line 410 "sat11k.ch"
o,cmem[k++]= p+2,j++;
oo,kinx[p+2].size++;
}
if(out_file){
for(jj= 0;jj<j;jj++)fprintf(out_file," "O"s"O".8s",litname(cmem[la+jj]));
fprintf(out_file,"\n");
}
if(j<3){
k= la,u= cmem[la];
oo,kinx[u].size--;
if(j==2){
oo,v= cmem[la+1],kinx[v].size--;
/*43:*/
#line 1096 "sat11.w"

{
o,la= bimp[bar(u)].addr,ls= bimp[bar(u)].size;
if(o,ls==bimp[bar(u)].alloc)
resize(bar(u)),o,la= bimp[bar(u)].addr;
oo,mem[la+ls]= v,bimp[bar(u)].size= ls+1;
o,la= bimp[bar(v)].addr,ls= bimp[bar(v)].size;
if(o,ls==bimp[bar(v)].alloc)
resize(bar(v)),o,la= bimp[bar(v)].addr;
oo,mem[la+ls]= u,bimp[bar(v)].size= ls+1;
}

#line 491 "sat11k.ch"
/*:43*/
#line 422 "sat11k.ch"
;
}else/*42:*/
#line 444 "sat11k.ch"

{
if(o,kinx[u].addr==0){
if(o,kinx[bar(u)].addr){
if(verbose&show_choices)
fprintf(stderr,"Unary clause "O"d contradicts unary clause "O"d\n",
c,kinx[bar(u)].addr);
goto unsat;
}
o,kinx[u].addr= c;
#line 1092 "sat11.w"
o,forcedlit[forcedlits++]= u;
}
}

/*:42*/
#line 423 "sat11k.ch"
;
}else o,cinx[cc].addr= la,cinx[cc].size= k-la,cc--;
#line 1076 "sat11.w"

/*:41*/
#line 391 "sat11k.ch"
;
}
cinx[0].addr= k;
if(k!=bcells||cc)confusion("cmem");
/*44:*/
#line 491 "sat11k.ch"

max_use= 0;
for(j= 0,l= badlit-1;l>=2;l--){
oo,kinx[l].addr= j,jj= kinx[l].size,j+= jj,kinx[l].size= 0;
if(jj> max_use)max_use= jj;
}
o,kinx[l].addr= j;
if(j!=bcells)confusion("kinx1");
for(c= bclauses,j= 0;c;c--){
for(o,k= cinx[c].size;k;k--){
o,u= cmem[j++];
o,la= kinx[u].addr,ls= kinx[u].size;
o,kmem[la+ls]= c;
o,kinx[u].size= ls+1;
}
}
if(j!=bcells)confusion("kinx2");
/*45:*/
#line 510 "sat11k.ch"

bstack= (tpair*)malloc(max_use*sizeof(tpair));
if(!bstack){
fprintf(stderr,"Oops, I can't allocate the bstack array!\n");
exit(-10);
}
bytes+= max_use*sizeof(tpair);
#line 1142 "sat11.w"

/*:45*/
#line 508 "sat11k.ch"
;

/*:44*/
#line 395 "sat11k.ch"
;
#line 1051 "sat11.w"
if(out_file)fflush(out_file);

/*:40*/
#line 944 "sat11.w"
;
/*47:*/
#line 1153 "sat11.w"

if(cur_cell!=&cur_chunk->cell[0]||
cur_chunk->prev!=NULL||
cur_tmp_var!=&cur_vchunk->var[0]||
cur_vchunk->prev!=NULL)confusion("consistency");
free(cur_chunk);
for(cur_vchunk= last_vchunk;cur_vchunk;cur_vchunk= last_vchunk){
last_vchunk= cur_vchunk->prev;
free(cur_vchunk);
}

/*:47*/
#line 945 "sat11.w"
;
/*58:*/
#line 1365 "sat11.w"

istack= (idata*)malloc((1<<memk_max)*sizeof(idata));
if(!istack){
fprintf(stderr,"Oops, I can't allocate the istack array!\n");
exit(-10);
}
bytes+= (1<<memk)*sizeof(idata);
iptr_max= 1<<memk;

/*:58*//*90:*/
#line 2032 "sat11.w"

cand= (cdata*)malloc(vars*sizeof(cdata));
if(!cand){
fprintf(stderr,"Oops, I can't allocate the cand array!\n");
exit(-10);
}
bytes+= vars*sizeof(cdata);
rating= (float*)malloc((vars+1)*sizeof(float));
if(!rating){
fprintf(stderr,"Oops, I can't allocate the rating array!\n");
exit(-10);
}
bytes+= (vars+1)*sizeof(float);

/*:90*//*109:*/
#line 2428 "sat11.w"

max_prelook_arcs&= -2;
cand_arc= (arc*)malloc(max_prelook_arcs*sizeof(arc));
if(!cand_arc){
fprintf(stderr,"Oops, I can't allocate the cand_arc array!\n");
exit(-10);
}

/*:109*//*121:*/
#line 2706 "sat11.w"

look= (ldata*)malloc(lits*sizeof(ldata));
if(!look){
fprintf(stderr,"Oops, I can't allocate the look array!\n");
exit(-10);
}
bytes+= lits*sizeof(ldata);

/*:121*//*134:*/
#line 2993 "sat11.w"

wstack= (uint*)malloc(lits*sizeof(uint));
if(!wstack){
fprintf(stderr,"Oops, I can't allocate the wstack array!\n");
exit(-10);
}
bytes+= lits*sizeof(uint);

#line 1011 "sat11k.ch"
/*:134*//*165:*/
#line 1295 "sat11k.ch"

clause_weight= (float*)malloc(max_clause*sizeof(float));
if(!clause_weight){
fprintf(stderr,"Oops, I can't allocate the clause_weight array!\n");
exit(-10);
}
bytes+= max_clause*sizeof(float);
clause_weight[2]= 1.0;
for(k= 3;k<max_clause;k++)o,clause_weight[k]= clause_weight[k-1]*gamm+0.01;

/*:165*/
#line 946 "sat11.w"
;

/*:37*/
#line 120 "sat11.w"
;
imems= mems,mems= 0;
/*152:*/
#line 1171 "sat11k.ch"

if(verbose&show_big_clauses)/*155:*/
#line 1182 "sat11k.ch"

for(c= 1;c<=bclauses;c++){
fprintf(stderr,""O"d:",c);
for(la= cinx[c].addr;la<cinx[c-1].addr;la++)
fprintf(stderr," "O"s"O".8s",litname(cmem[la]));
fprintf(stderr,"\n");
}

/*:155*/
#line 1172 "sat11k.ch"
;
#line 3343 "sat11.w"
level= 0;
if(forcedlits){
o,nstack[0].branch= -1;
goto special_start;
}
enter_level:if(sanity_checking)sanity();
/*59:*/
#line 1385 "sat11.w"

nstack[level].lptr= rptr,nodes++;
if(delta&&(mems>=thresh))thresh+= delta,print_state(level);
if(mems> timeout){
fprintf(stderr,"TIMEOUT!\n");
goto done;
}
o,nstack[level].branch= -1,plevel= level;
/*123:*/
#line 2758 "sat11.w"

/*87:*/
#line 2007 "sat11.w"

if(freevars==0)goto satisfied;
/*97:*/
#line 919 "sat11k.ch"

/*95:*/
#line 909 "sat11k.ch"

for(k= 0;k<freevars;k++){
o,x= freevar[k];
/*94:*/
#line 871 "sat11k.ch"

{
float s;
l= poslit(x);
/*93:*/
#line 856 "sat11k.ch"

{
ullng acc;
o,acc= kinx[bar(l)].size;
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,u= mem[la];
if(isfree(u))acc+= kinx[bar(u)].size;
}
sum= alpha+(float)acc;
}

/*:93*/
#line 875 "sat11k.ch"
;
s= sum;
l++;
/*93:*/
#line 856 "sat11k.ch"

{
ullng acc;
o,acc= kinx[bar(l)].size;
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,u= mem[la];
if(isfree(u))acc+= kinx[bar(u)].size;
}
sum= alpha+(float)acc;
}

/*:93*/
#line 878 "sat11k.ch"
;
rating[x]= s*sum;
if(verbose&show_scores)
fprintf(stderr,"("O".8s: pos "O".2f neg "O".2f r="O".4g)\n",
vmem[x].name.ch8,s,sum,s*sum);
}
#line 2144 "sat11.w"

#line 909 "sat11k.ch"
/*:94*/
#line 912 "sat11k.ch"
;
}
#line 2167 "sat11.w"

/*:95*/
#line 920 "sat11k.ch"
;
#line 2192 "sat11.w"
maxcand= (level==0?freevars:levelcand/level);
if(maxcand<mincutoff)maxcand= mincutoff;
/*98:*/
#line 2211 "sat11.w"

no_newbies= (plevel> 0);
init_cand:for(cands= k= 0,sum= 0.0;k<freevars;k++){
o,x= freevar[k];
o,stamp[x]= 0;
if(no_newbies){
if(x> primary_vars)continue;
o,t= vmem[x].pfx,l= vmem[x].len;
if(l==plevel){
if(t!=prefix)continue;
}else if(l> plevel)continue;
else if(t!=(l<32?prefix&-(uint)(1LL<<(32-l)):prefix))continue;
}
oo,cand[cands].var= x,cand[cands].rating= rating[x];
cands++,sum+= rating[x];
}
if(cands==0){
/*99:*/
#line 2233 "sat11.w"

for(j= 0;j<freevars;j++){
o,x= freevar[j];
l= poslit(x);
/*100:*/
#line 2244 "sat11.w"

#line 925 "sat11k.ch"
if(o,kinx[bar(l)].size)goto nogood;
#line 2246 "sat11.w"
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,u= mem[la];
if(o,stamp[thevar(u)]!=real_truth+(u&1))goto nogood;
}

/*:100*/
#line 2237 "sat11.w"
;
l++;
/*100:*/
#line 2244 "sat11.w"

#line 925 "sat11k.ch"
if(o,kinx[bar(l)].size)goto nogood;
#line 2246 "sat11.w"
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,u= mem[la];
if(o,stamp[thevar(u)]!=real_truth+(u&1))goto nogood;
}

/*:100*/
#line 2239 "sat11.w"
;
}
goto satisfied;
nogood:

/*:99*/
#line 2228 "sat11.w"
;
no_newbies= 0;
goto init_cand;
}

/*:98*/
#line 2194 "sat11.w"
;
/*101:*/
#line 2255 "sat11.w"

for(k= 1;cands>=2*maxcand&&k;){
register float mean= 0.9999*sum/(double)cands;
for(j= k= 0,sum= 0.0;j<cands;){
if(o,cand[j].rating>=mean)sum+= cand[j].rating,j++;
else oo,k= 1,cand[j]= cand[--cands];
}
}
if(cands> maxcand)/*102:*/
#line 2273 "sat11.w"

{
j= cands>>1;
while(j> 0){
j--;
/*103:*/
#line 2287 "sat11.w"

{
register float r;
cdata c;
o,c= cand[j],r= c.rating;
for(i= j,jj= (j<<1)+1;jj<cands;i= jj,jj= (jj<<1)+1){
if(jj+1<cands&&(o,cand[jj+1].rating<cand[jj].rating))jj++;
if(o,r<=cand[jj].rating)break;
o,cand[i]= cand[jj];
}
if(i> j)o,cand[i]= c;
}

/*:103*/
#line 2278 "sat11.w"
;
}
while(1){
oo,cand[0]= cand[--cands];
if(cands==maxcand)break;
/*103:*/
#line 2287 "sat11.w"

{
register float r;
cdata c;
o,c= cand[j],r= c.rating;
for(i= j,jj= (j<<1)+1;jj<cands;i= jj,jj= (jj<<1)+1){
if(jj+1<cands&&(o,cand[jj+1].rating<cand[jj].rating))jj++;
if(o,r<=cand[jj].rating)break;
o,cand[i]= cand[jj];
}
if(i> j)o,cand[i]= c;
}

/*:103*/
#line 2283 "sat11.w"
;
}
}

/*:102*/
#line 2263 "sat11.w"
;
if(cands==0)confusion("cands");

/*:101*/
#line 2195 "sat11.w"
;

/*:97*/
#line 2009 "sat11.w"
;
/*104:*/
#line 2357 "sat11.w"

/*106:*/
#line 2398 "sat11.w"

/*66:*/
#line 1540 "sat11.w"

if(++bstamp==0){
bstamp= 1;
for(l= 2;l<badlit;l++)o,lmem[l].bstamp= 0;
}

/*:66*/
#line 2399 "sat11.w"
;
for(i= 0;i<cands;i++){
o,l= poslit(cand[i].var);
oo,lmem[l].rank= 0,lmem[l].arcs= -1,lmem[l].bstamp= bstamp;
oo,lmem[l+1].rank= 0,lmem[l+1].arcs= -1,lmem[l+1].bstamp= bstamp;
}
/*110:*/
#line 2436 "sat11.w"

for(j= i= 0;i<cands;i++){
o,l= poslit(cand[i].var);
/*111:*/
#line 2451 "sat11.w"

for(oo,la= bimp[l].addr,ls= bimp[l].size,p= lmem[bar(l)].arcs;ls;la++,ls--){
o,u= mem[la];
if(u<l)continue;
if(o,lmem[u].bstamp!=bstamp)continue;

o,cand_arc[j].tip= bar(u),cand_arc[j].next= p,p= j;

oo,cand_arc[j+1].tip= l,cand_arc[j+1].next= lmem[u].arcs;
o,lmem[u].arcs= j+1,j+= 2;
if(j==max_prelook_arcs){
if(verbose&show_details)
fprintf(stderr,"prelook arcs cut off at "O"d; see option z\n",
max_prelook_arcs);
o,lmem[bar(l)].arcs= lmem[bar(l)].untagged= p;
goto arcs_done;
}
}
o,lmem[bar(l)].arcs= lmem[bar(l)].untagged= p;

/*:111*/
#line 2439 "sat11.w"
;
l++;
/*111:*/
#line 2451 "sat11.w"

for(oo,la= bimp[l].addr,ls= bimp[l].size,p= lmem[bar(l)].arcs;ls;la++,ls--){
o,u= mem[la];
if(u<l)continue;
if(o,lmem[u].bstamp!=bstamp)continue;

o,cand_arc[j].tip= bar(u),cand_arc[j].next= p,p= j;

oo,cand_arc[j+1].tip= l,cand_arc[j+1].next= lmem[u].arcs;
o,lmem[u].arcs= j+1,j+= 2;
if(j==max_prelook_arcs){
if(verbose&show_details)
fprintf(stderr,"prelook arcs cut off at "O"d; see option z\n",
max_prelook_arcs);
o,lmem[bar(l)].arcs= lmem[bar(l)].untagged= p;
goto arcs_done;
}
}
o,lmem[bar(l)].arcs= lmem[bar(l)].untagged= p;

/*:111*/
#line 2441 "sat11.w"
;
}
arcs_done:if(j> cand_arc_alloc)
bytes+= (j-cand_arc_alloc)*sizeof(arc),cand_arc_alloc= j;

/*:110*/
#line 2405 "sat11.w"
;
for(i= 0;i<cands;i++){
o,l= poslit(cand[i].var);
oo,lmem[l].untagged= lmem[l].arcs;
oo,lmem[l+1].untagged= lmem[l+1].arcs;
}
k= 0;
active= settled= 0;

/*:106*/
#line 2358 "sat11.w"
;
for(i= 0;i<cands;i++){
o,l= poslit(cand[i].var);
check_rank:if(o,lmem[l].rank==0)
/*112:*/
#line 2471 "sat11.w"

{
v= l;
o,lmem[l].parent= 0;
/*113:*/
#line 2481 "sat11.w"

o,lmem[v].rank= ++k;
lmem[v].link= active,active= v;
o,lmem[v].min= v;

/*:113*/
#line 2475 "sat11.w"
;
do/*114:*/
#line 2489 "sat11.w"

{
o,vv= lmem[v].untagged,ll= lmem[v].min;
if(vv>=0){
o,u= cand_arc[vv].tip,vv= cand_arc[vv].next;
o,lmem[v].untagged= vv;
o,j= lmem[u].rank;
if(j){
if(o,j<lmem[ll].rank)lmem[v].min= u;

}else{
lmem[u].parent= v;
v= u;
/*113:*/
#line 2481 "sat11.w"

o,lmem[v].rank= ++k;
lmem[v].link= active,active= v;
o,lmem[v].min= v;

/*:113*/
#line 2502 "sat11.w"
;
}
}else{
o,u= lmem[v].parent;
if(v==ll)
/*115:*/
#line 2526 "sat11.w"

{
float r,rr;
t= active;
o,r= rating[thevar(v)],w= v;
o,active= lmem[v].link;
o,lmem[v].rank= infty;
lmem[v].link= settled,settled= t;

while(t!=v){
if(t==bar(v)){
if(verbose&show_gory_details)
fprintf(stderr,"the binary clauses are inconsistent\n");
goto look_bad;
}
o,lmem[t].rank= infty;
o,lmem[t].parent= v;
o,rr= rating[thevar(t)];
if(rr> r)r= rr,w= t;
o,t= lmem[t].link;
}
o,lmem[v].parent= v,lmem[v].vcomp= w;
if(o,lmem[bar(v)].rank==infty)
oo,lmem[v].vcomp= bar(lmem[lmem[bar(v)].parent].vcomp);
}

/*:115*/
#line 2508 "sat11.w"

else{
if(ooo,lmem[ll].rank<lmem[lmem[u].min].rank)
o,lmem[u].min= ll;
}
v= u;
}
}

/*:114*/
#line 2477 "sat11.w"

while(v> 0);
}

/*:112*/
#line 2363 "sat11.w"
;
if((l&1)==0){
l++;goto check_rank;
}
}
if(verbose&show_strong_comps)/*105:*/
#line 2370 "sat11.w"

{
fprintf(stderr,"Strong components:\n");
for(l= settled;l;l= lmem[l].link){
fprintf(stderr," "O"s"O".8s ",
litname(l));
if(lmem[l].parent!=l)fprintf(stderr,"with "O"s"O".8s\n",
litname(lmem[l].parent));
else{
if(lmem[l].vcomp!=l)fprintf(stderr,"-> "O"s"O".8s ",
litname(lmem[l].vcomp));
fprintf(stderr,""O".4g\n",
rating[thevar(lmem[l].vcomp)]);
}
}
}

/*:105*/
#line 2368 "sat11.w"
;

/*:104*/
#line 2010 "sat11.w"
;
/*117:*/
#line 2644 "sat11.w"

/*118:*/
#line 2663 "sat11.w"

o,lmem[root].child= 0,lmem[root].height= -1,pp= root;
for(u= settled;u;u= uu){
oo,uu= lmem[u].link,p= lmem[u].parent;
if(p!=pp)h= 0,w= root,pp= p;

for(o,j= lmem[bar(u)].arcs;j>=0;j= cand_arc[j].next){
o,v= bar(cand_arc[j].tip);
o,vv= lmem[v].parent;
if(vv==p)continue;
o,hh= lmem[vv].height;
if(hh>=h)h= hh+1,w= vv;
}
if(p==u){
o,v= lmem[w].child;
oo,lmem[u].height= h,lmem[u].child= 0,lmem[u].link= v;
o,lmem[w].child= u;
}
}

/*:118*/
#line 2645 "sat11.w"
;
/*122:*/
#line 2722 "sat11.w"

o,u= lmem[root].child,j= k= v= 0;
while(1){
oo,look[k].lit= lmem[u].vcomp;
o,lmem[u].rank= k++;
if(o,lmem[u].child){
o,lmem[u].parent= v;
v= u,u= lmem[u].child;
}else{
post:o,i= lmem[u].rank;
o,look[i].offset= j,j+= 2;
if(v)oo,lmem[u].parent= lmem[v].vcomp;
else o,lmem[u].parent= 0;
if(o,lmem[u].link)u= lmem[u].link;
else if(v){
o,u= v,v= lmem[u].parent;
goto post;
}else break;
}
}
looks= k;
if(j!=k+k)confusion("looks");

/*:122*/
#line 2646 "sat11.w"
;

/*:117*/
#line 2011 "sat11.w"
;

/*:87*/
#line 2759 "sat11.w"
;
if(verbose&show_looks){
fprintf(stderr,"Looks at level "O"d:\n",
level);
for(i= 0;i<looks;i++)
fprintf(stderr," "O"s"O".8s "O"d\n",
litname(look[i].lit),look[i].offset);
}
#line 930 "sat11k.ch"
fl= forcedlits,last_change= -1,fptr= rptr;
#line 2768 "sat11.w"
base= 2;
while(1){
for(looki= 0;looki<looks;looki++){
if(looki==last_change)goto look_done;
o,l= look[looki].lit,cs= base+look[looki].offset;
/*126:*/
#line 2852 "sat11.w"

looklit= l;
o,ll= lmem[looklit].parent;
if(ll)oo,lmem[looklit].wnb= lmem[ll].wnb;
else o,lmem[l].wnb= 0.0;
if(verbose&show_gory_details)
fprintf(stderr,"looking at "O"s"O".8s ("O"d)\n",
litname(looklit),cs);
if(isfixed(l)){
if(iscontrary(l)&&stamp[thevar(l)]<proto_truth)
/*129:*/
#line 2941 "sat11.w"

{
looklit= bar(looklit);
forcedlit[forcedlits++]= looklit;
look_cs= cs,cs= proto_truth;
/*132:*/
#line 2976 "sat11.w"

#line 974 "sat11k.ch"
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 974 "sat11k.ch"
;
wptr= 0;eptr= fptr;
#line 2978 "sat11.w"
weighted_new_binaries= 0;
l= looklit;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 2980 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*135:*/
#line 1024 "sat11k.ch"

bptr= 0;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls>=2)weighted_new_binaries+= clause_weight[ls];
else if(bptr>=0)/*136:*/
#line 1049 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3033 "sat11.w"

/*:136*/
#line 1033 "sat11k.ch"
;
}
if(bptr<0)goto contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto contra;
}else{
wstack[wptr++]= l= u;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 1042 "sat11k.ch"
;
}
}

/*:135*/
#line 2984 "sat11.w"
;
}
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 2986 "sat11.w"
;

/*:132*/
#line 2946 "sat11.w"
;
cs= look_cs;
}

/*:129*/
#line 2862 "sat11.w"
;
}else{
/*132:*/
#line 2976 "sat11.w"

#line 974 "sat11k.ch"
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 974 "sat11k.ch"
;
wptr= 0;eptr= fptr;
#line 2978 "sat11.w"
weighted_new_binaries= 0;
l= looklit;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 2980 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*135:*/
#line 1024 "sat11k.ch"

bptr= 0;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls>=2)weighted_new_binaries+= clause_weight[ls];
else if(bptr>=0)/*136:*/
#line 1049 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3033 "sat11.w"

/*:136*/
#line 1033 "sat11k.ch"
;
}
if(bptr<0)goto contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto contra;
}else{
wstack[wptr++]= l= u;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 1042 "sat11k.ch"
;
}
}

/*:135*/
#line 2984 "sat11.w"
;
}
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 2986 "sat11.w"
;

/*:132*/
#line 2865 "sat11.w"
;
if(weighted_new_binaries==0)/*127:*/
#line 2891 "sat11.w"

{
if(lmem[looklit].wnb==0){
if(verbose&show_gory_details)
fprintf(stderr," autarky at "O"s"O".8s\n",
litname(looklit));
looklit= bar(looklit);
/*129:*/
#line 2941 "sat11.w"

{
looklit= bar(looklit);
forcedlit[forcedlits++]= looklit;
look_cs= cs,cs= proto_truth;
/*132:*/
#line 2976 "sat11.w"

#line 974 "sat11k.ch"
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 974 "sat11k.ch"
;
wptr= 0;eptr= fptr;
#line 2978 "sat11.w"
weighted_new_binaries= 0;
l= looklit;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 2980 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*135:*/
#line 1024 "sat11k.ch"

bptr= 0;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls>=2)weighted_new_binaries+= clause_weight[ls];
else if(bptr>=0)/*136:*/
#line 1049 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3033 "sat11.w"

/*:136*/
#line 1033 "sat11k.ch"
;
}
if(bptr<0)goto contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto contra;
}else{
wstack[wptr++]= l= u;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 1042 "sat11k.ch"
;
}
}

/*:135*/
#line 2984 "sat11.w"
;
}
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 2986 "sat11.w"
;

/*:132*/
#line 2946 "sat11.w"
;
cs= look_cs;
}

/*:129*/
#line 2898 "sat11.w"
;
}else{
ll= lmem[looklit].parent;
if(verbose&show_gory_details)
fprintf(stderr," autarky "O"s"O".8s -> "O"s"O".8s\n",
litname(ll),litname(looklit));
/*128:*/
#line 2926 "sat11.w"

{
u= bar(ll);
o,au= bimp[ll].addr,su= bimp[ll].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 2930 "sat11.w"
;
if(o,su==bimp[ll].alloc)resize(ll),o,au= bimp[ll].addr;
oo,mem[au+su]= looklit,bimp[ll].size= su+1;
u= looklit;
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 2935 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
oo,mem[au+su]= bar(ll),bimp[bar(u)].size= su+1;
#line 2939 "sat11.w"
}

/*:128*/
#line 2904 "sat11.w"
;
}
}

/*:127*/
#line 2866 "sat11.w"

else o,lmem[looklit].wnb+= weighted_new_binaries;
/*142:*/
#line 3154 "sat11.w"

if(level&&(o,lmem[looklit].dl_fail!=istamp)){
if(lmem[looklit].wnb> dl_trigger){
if(cs+2*looks*((ullng)dl_max_iter+1)<proto_truth){
/*143:*/
#line 3189 "sat11.w"

last_base= cs+2*looks*dl_max_iter;
dl_truth= last_base+cs-base;
base= cs;
#line 1076 "sat11k.ch"
cs= dl_truth,l= looklit,dlooklit= l;
wptr= 0;
/*149:*/
#line 1090 "sat11k.ch"

/*162:*/
#line 1265 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1272 "sat11k.ch"
;
}

/*:162*/
#line 1091 "sat11k.ch"
;
eptr= fptr;
#line 3302 "sat11.w"
l= dlooklit;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 3303 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*150:*/
#line 1126 "sat11k.ch"

bptr= 0;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls<2&&bptr>=0)/*151:*/
#line 1147 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3339 "sat11.w"

/*:151*/
#line 1134 "sat11k.ch"
;
}
if(bptr<0)goto dl_contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto dl_contra;
}else{
l= u;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 1143 "sat11k.ch"
;
}
}

/*:150*/
#line 3307 "sat11.w"
;
}

#line 1125 "sat11k.ch"
/*:149*/
#line 1078 "sat11k.ch"
;
#line 3197 "sat11.w"
/*144:*/
#line 3206 "sat11.w"

dl_last_change= 0;
while(1){
for(dlooki= 0;dlooki<looks;dlooki++){
o,l= look[dlooki].lit,cs= base+look[dlooki].offset;
if(l==dl_last_change)goto dlook_done;
/*146:*/
#line 3256 "sat11.w"

dlooklit= l;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"dlooking at "O"s"O".8s ("O"d)\n",
litname(dlooklit),cs);
if(isfixed(l)){
if(stamp[thevar(l)]<dl_truth&&iscontrary(l))
/*147:*/
#line 3272 "sat11.w"

{
dl_last_change= dlooklit;
dlooklit= bar(dlooklit);
dlook_cs= cs,cs= dl_truth;
/*149:*/
#line 1090 "sat11k.ch"

/*162:*/
#line 1265 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1272 "sat11k.ch"
;
}

/*:162*/
#line 1091 "sat11k.ch"
;
eptr= fptr;
#line 3302 "sat11.w"
l= dlooklit;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 3303 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*150:*/
#line 1126 "sat11k.ch"

bptr= 0;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls<2&&bptr>=0)/*151:*/
#line 1147 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3339 "sat11.w"

/*:151*/
#line 1134 "sat11k.ch"
;
}
if(bptr<0)goto dl_contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto dl_contra;
}else{
l= u;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 1143 "sat11k.ch"
;
}
}

/*:150*/
#line 3307 "sat11.w"
;
}

#line 1125 "sat11k.ch"
/*:149*/
#line 3277 "sat11.w"
;
cs= dlook_cs;
wstack[wptr++]= dlooklit;
}

/*:147*/
#line 3263 "sat11.w"
;
}else{
/*149:*/
#line 1090 "sat11k.ch"

/*162:*/
#line 1265 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1272 "sat11k.ch"
;
}

/*:162*/
#line 1091 "sat11k.ch"
;
eptr= fptr;
#line 3302 "sat11.w"
l= dlooklit;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 3303 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*150:*/
#line 1126 "sat11k.ch"

bptr= 0;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls<2&&bptr>=0)/*151:*/
#line 1147 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3339 "sat11.w"

/*:151*/
#line 1134 "sat11k.ch"
;
}
if(bptr<0)goto dl_contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto dl_contra;
}else{
l= u;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 1143 "sat11k.ch"
;
}
}

/*:150*/
#line 3307 "sat11.w"
;
}

#line 1125 "sat11k.ch"
/*:149*/
#line 3266 "sat11.w"
;
}

/*:146*/
#line 3213 "sat11.w"
;
dlook_on:continue;
}
if(dl_last_change==0)break;
base+= 2*looks;
if(base==last_base)break;
}
#line 1083 "sat11k.ch"
dlook_done:base= last_base,cs= dl_truth;
/*162:*/
#line 1265 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1272 "sat11k.ch"
;
}

/*:162*/
#line 1084 "sat11k.ch"
;
#line 3221 "sat11.w"

/*:144*/
#line 3198 "sat11.w"
;
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 3199 "sat11.w"
;

/*:143*/
#line 3159 "sat11.w"
;
o,dl_trigger= lmem[looklit].wnb;

o,lmem[looklit].dl_fail= istamp;

}
}else dl_trigger*= dl_rho;

}

/*:142*/
#line 2868 "sat11.w"
;
/*139:*/
#line 3070 "sat11.w"

old_looklit= looklit;
for(o,ola= bimp[bar(looklit)].addr,ols= bimp[bar(looklit)].size;ols;ols--){
o,looklit= bar(mem[ola+ols-1]);
if((isfixed(looklit))&&(stamp[thevar(looklit)]<proto_truth)&&
iscontrary(looklit)){
if(verbose&show_gory_details)
fprintf(stderr," necessary "O"s"O".8s\n",
litname(bar(looklit)));
/*129:*/
#line 2941 "sat11.w"

{
looklit= bar(looklit);
forcedlit[forcedlits++]= looklit;
look_cs= cs,cs= proto_truth;
/*132:*/
#line 2976 "sat11.w"

#line 974 "sat11k.ch"
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 974 "sat11k.ch"
;
wptr= 0;eptr= fptr;
#line 2978 "sat11.w"
weighted_new_binaries= 0;
l= looklit;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 2980 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*135:*/
#line 1024 "sat11k.ch"

bptr= 0;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls>=2)weighted_new_binaries+= clause_weight[ls];
else if(bptr>=0)/*136:*/
#line 1049 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3033 "sat11.w"

/*:136*/
#line 1033 "sat11k.ch"
;
}
if(bptr<0)goto contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto contra;
}else{
wstack[wptr++]= l= u;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 1042 "sat11k.ch"
;
}
}

/*:135*/
#line 2984 "sat11.w"
;
}
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 2986 "sat11.w"
;

/*:132*/
#line 2946 "sat11.w"
;
cs= look_cs;
}

/*:129*/
#line 3079 "sat11.w"
;
o,ola= bimp[bar(old_looklit)].addr;
}
}

/*:139*/
#line 2869 "sat11.w"
;
}

/*:126*/
#line 2774 "sat11.w"
;
look_on:if(forcedlits> fl)fl= forcedlits,last_change= looki;
}
if(last_change==-1)break;
base+= 2*looks;
if(base+2*looks>=proto_truth)break;
}
#line 935 "sat11k.ch"
look_done:cs= near_truth;
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 936 "sat11k.ch"
;
#line 2782 "sat11.w"

/*:123*/
#line 1394 "sat11.w"
;
if(forcedlits)/*64:*/
#line 1505 "sat11.w"

{
special_start:if(verbose&show_details)
fprintf(stderr,"(lookahead for level "O"d forces "O"d)\n",
level,forcedlits);
cs= near_truth;
fptr= eptr= rptr;
/*65:*/
#line 1530 "sat11.w"

if(++istamp==0){
istamp= 1;
for(l= 2;l<badlit;l++)o,lmem[l].istamp= 0;
}

/*:65*/
#line 1512 "sat11.w"
;
for(i= 0;i<forcedlits;i++){
o,l= forcedlit[i];
/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1515 "sat11.w"
;
}
goto promote;
}

/*:64*/
#line 1397 "sat11.w"
;
chooseit:/*140:*/
#line 3102 "sat11.w"

{
float best_score;
if(freevars==0)goto satisfied;
for(i= 0,best_score= -1.0,bestlit= 0;i<looks;i++){
o,l= look[i].lit;
if((l&1)==0){
float pos,neg,score;
oo,pos= lmem[l].wnb,neg= lmem[l+1].wnb;
score= (pos+.1)*(neg+.1);
if(verbose&show_gory_details)
fprintf(stderr," "O".8s, "O".4g:"O".4g ("O".4g)\n",
vmem[thevar(l)].name.ch8,pos,neg,score);
if(score> best_score){
best_score= score;
bestlit= (pos> neg?l+1:l);
}
}
}
if(!isfree(bestlit))bestlit= 0;
if(bestlit+forcedlits==0)confusion("choice");
}

/*:140*/
#line 1398 "sat11.w"
;
o,nstack[level].rptr= rptr,nstack[level].iptr= iptr;
if(bestlit){
o,nstack[level].decision= bestlit,nstack[level].branch= 0;
tryit:l= bestlit,plevel= level+1;
if((verbose&show_choices)&&level<=show_choices_max)
fprintf(stderr,"Level "O"d"O"s: "O"s"O".8s ("O"lld mems)\n",
level,nstack[level].branch?"'":"",litname(l),mems);
/*62:*/
#line 1478 "sat11.w"

cs= near_truth;
fptr= eptr= rptr;
/*65:*/
#line 1530 "sat11.w"

if(++istamp==0){
istamp= 1;
for(l= 2;l<badlit;l++)o,lmem[l].istamp= 0;
}

/*:65*/
#line 1481 "sat11.w"
;
/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1483 "sat11.w"
;
promote:/*63:*/
#line 1492 "sat11.w"

while(fptr<eptr){
o,ll= rstack[fptr++];
/*69:*/
#line 1591 "sat11.w"

o,stamp[thevar(ll)]= real_truth+(ll&1);
if(verbose&show_details)
fprintf(stderr,"fixing "O"s"O".8s\n",
litname(ll));
/*70:*/
#line 1608 "sat11.w"

x= thevar(ll);
o,y= freevar[--freevars];
if(x!=y){
o,xl= freeloc[x];
o,freevar[xl]= y;
o,freeloc[y]= xl;
o,freeloc[x]= freevars;
o,freevar[freevars]= x;
}

#line 604 "sat11k.ch"
/*:70*/
#line 1596 "sat11.w"
;
#line 547 "sat11k.ch"
/*156:*/
#line 1195 "sat11k.ch"

for(o,tla= kinx[ll].addr,tls= kinx[ll].size;tls;tla++,tls--){
o,c= kmem[tla];
o,cia= cinx[c].addr,cis= cinx[c].size;
o,kk= cinx[c-1].addr-cia;
cis--;
if(cis<=(theta64*kk)>>6)
/*157:*/
#line 1212 "sat11k.ch"

{
for(ci= cia;cis;cia++){
o,u= cmem[cia];
if(isfree(u)){
if(ci!=cia)ooo,v= cmem[ci],cmem[ci]= u,cmem[cia]= v;
/*158:*/
#line 1224 "sat11k.ch"

{
for(o,su= kinx[u].size-1,au= ua= kinx[u].addr+su;o,kmem[au]!=c;au--);
if(au!=ua)oo,kmem[au]= kmem[ua],kmem[ua]= c;
o,kinx[u].size= su;
}

/*:158*/
#line 1218 "sat11k.ch"
;
ci++,cis--;
}
}
}

/*:157*/
#line 1202 "sat11k.ch"

else for(;cis;cia++){
o,u= cmem[cia];
if(isfree(u)){
/*158:*/
#line 1224 "sat11k.ch"

{
for(o,su= kinx[u].size-1,au= ua= kinx[u].addr+su;o,kmem[au]!=c;au--);
if(au!=ua)oo,kmem[au]= kmem[ua],kmem[ua]= c;
o,kinx[u].size= su;
}

/*:158*/
#line 1206 "sat11k.ch"
;
cis--;
}
}
}

/*:156*/
#line 547 "sat11k.ch"
;
tll= bar(ll),bptr= 0;
/*71:*/
#line 616 "sat11k.ch"

if(verbose&show_details)
fprintf(stderr," ("O"s"O".8s out)\n",litname(tll));
for(o,tla= kinx[tll].addr,tls= kinx[tll].size;tls;tla++,tls--){
oo,c= kmem[tla],cia= cinx[c].addr,cis= cinx[c].size;
if(o,cia+cis==cinx[c-1].addr){
for(ua= cia,su= cis;su;ua++,su--){
o,u= cmem[ua];
if(u==tll)au= ua;
else/*86:*/
#line 742 "sat11k.ch"

{
x= thevar(u);
o,p= vmem[x].pfx,q= vmem[x].len;
if(q<plevel){
t= prefix;
if(q<32)t&= -(1LL<<(32-q));
if(p!=t)o,vmem[x].pfx= prefix,vmem[x].len= plevel;
}else o,vmem[x].pfx= prefix,vmem[x].len= plevel;
}
#line 1996 "sat11.w"

/*:86*/
#line 625 "sat11k.ch"
;
}
if(u!=tll)oo,cmem[ua-1]= tll,cmem[au]= u;
}
o,cinx[c].size= cis-1;
if(cis==3){
for(ci= cia,v= cmem[ci];;ci++){
o,u= cmem[ci];
if(isfree(u))break;
}
if(ci!=cia)oo,cmem[cia]= u,cmem[ci]= v;
for(ci++;;ci++){
o,v= cmem[ci];
if(isfree(v))break;
}
if(ci!=cia+1)ooo,cmem[ci]= cmem[cia+1],cmem[cia+1]= v;
o,bstack[bptr].u= u,bstack[bptr].v= v,bptr++;
if(verbose&show_details)
fprintf(stderr,"  "O"s"O".8s->"O"s"O".8s|"O"s"O".8s\n",
litname(bar(tll)),litname(u),litname(v));
/*158:*/
#line 1224 "sat11k.ch"

{
for(o,su= kinx[u].size-1,au= ua= kinx[u].addr+su;o,kmem[au]!=c;au--);
if(au!=ua)oo,kmem[au]= kmem[ua],kmem[ua]= c;
o,kinx[u].size= su;
}

/*:158*/
#line 645 "sat11k.ch"
;
u= v;/*158:*/
#line 1224 "sat11k.ch"

{
for(o,su= kinx[u].size-1,au= ua= kinx[u].addr+su;o,kmem[au]!=c;au--);
if(au!=ua)oo,kmem[au]= kmem[ua],kmem[ua]= c;
o,kinx[u].size= su;
}

/*:158*/
#line 646 "sat11k.ch"
;
}
}

/*:71*/
#line 550 "sat11k.ch"
;
while(bptr){
o,bptr--,u= bstack[bptr].u,v= bstack[bptr].v;
/*72:*/
#line 1688 "sat11.w"

if(isfixed(u)){
if(iscontrary(u)){
if(isfixed(v)){
if(iscontrary(v))goto conflict;
}else{
l= v;
/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1695 "sat11.w"
;
}
}
}else{
if(isfixed(v)){
if(iscontrary(v)){
l= u;
/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1702 "sat11.w"
;
}
}else/*73:*/
#line 1733 "sat11.w"

{
/*66:*/
#line 1540 "sat11.w"

if(++bstamp==0){
bstamp= 1;
for(l= 2;l<badlit;l++)o,lmem[l].bstamp= 0;
}

/*:66*/
#line 1735 "sat11.w"
;
o,lmem[bar(u)].bstamp= bstamp;
for(o,au= bimp[bar(u)].addr,k= su= bimp[bar(u)].size;k;au++,k--)
oo,lmem[mem[au]].bstamp= bstamp;
if(o,lmem[bar(v)].bstamp==bstamp){
fix_u:l= u;/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1740 "sat11.w"
;
}else if(o,lmem[v].bstamp!=bstamp){
o,ua= bimp[bar(u)].alloc;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 1743 "sat11.w"
;
/*76:*/
#line 1792 "sat11.w"

for(o,la= bimp[v].addr,ls= bimp[v].size;ls;la++,ls--){
o,w= mem[la];
if(!isfixed(w)){
if(o,lmem[bar(w)].bstamp==bstamp)
goto fix_u;
if(o,lmem[w].bstamp!=bstamp){
if(verbose&show_details)
fprintf(stderr,"   ->"O"s"O".8s|"O"s"O".8s\n",
litname(u),litname(w));
if(su==ua)resize(bar(u)),ua+= ua,o,au= bimp[bar(u)].addr+su;
oo,mem[au++]= w,bimp[bar(u)].size= ++su;
o,aw= bimp[bar(w)].addr,sw= bimp[bar(w)].size;
/*78:*/
#line 1824 "sat11.w"

if(o,lmem[bar(w)].istamp!=istamp){
o,lmem[bar(w)].istamp= istamp;
o,istack[iptr].lit= bar(w),istack[iptr].size= sw;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1828 "sat11.w"
;
}

/*:78*/
#line 1805 "sat11.w"
;
if(o,sw==bimp[bar(w)].alloc)resize(bar(w)),o,aw= bimp[bar(w)].addr;
o,bimp[bar(w)].size= sw+1;
o,mem[aw+sw]= u;
}
}
}

/*:76*/
#line 1745 "sat11.w"
;
/*66:*/
#line 1540 "sat11.w"

if(++bstamp==0){
bstamp= 1;
for(l= 2;l<badlit;l++)o,lmem[l].bstamp= 0;
}

/*:66*/
#line 1746 "sat11.w"
;
o,lmem[bar(v)].bstamp= bstamp;
for(o,av= bimp[bar(v)].addr,k= sv= bimp[bar(v)].size;k;av++,k--)
oo,lmem[mem[av]].bstamp= bstamp;
if(o,lmem[bar(u)].bstamp==bstamp){
fix_v:l= v;/*68:*/
#line 1561 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr,"nearfixing "O"s"O".8s\n",
litname(l));
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto conflict;
}else{
if(verbose&show_details)
fprintf(stderr," nearfixing "O"s"O".8s\n",
litname(lp));
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:68*/
#line 1751 "sat11.w"
;
}else{
o,va= bimp[bar(v)].alloc;
/*77:*/
#line 1815 "sat11.w"

if(o,lmem[bar(v)].istamp!=istamp){
o,lmem[bar(v)].istamp= istamp;
o,istack[iptr].lit= bar(v),istack[iptr].size= sv;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1819 "sat11.w"
;
}

/*:77*/
#line 1754 "sat11.w"
;
/*79:*/
#line 1834 "sat11.w"

for(o,la= bimp[u].addr,ls= bimp[u].size;ls;la++,ls--){
o,w= mem[la];
if(!isfixed(w)){
if(o,lmem[bar(w)].bstamp==bstamp)
goto fix_v;
if(o,lmem[w].bstamp!=bstamp){
if(verbose&show_details)
fprintf(stderr,"   ->"O"s"O".8s|"O"s"O".8s\n",
litname(v),litname(w));
if(sv==va)resize(bar(v)),va+= va,o,av= bimp[bar(v)].addr+sv;
oo,mem[av++]= w,bimp[bar(v)].size= ++sv;
o,aw= bimp[bar(w)].addr,sw= bimp[bar(w)].size;
/*78:*/
#line 1824 "sat11.w"

if(o,lmem[bar(w)].istamp!=istamp){
o,lmem[bar(w)].istamp= istamp;
o,istack[iptr].lit= bar(w),istack[iptr].size= sw;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1828 "sat11.w"
;
}

/*:78*/
#line 1847 "sat11.w"
;
if(o,sw==bimp[bar(w)].alloc)resize(bar(w)),o,aw= bimp[bar(w)].addr;
o,bimp[bar(w)].size= sw+1;
o,mem[aw+sw]= v;
}
}
}

/*:79*/
#line 1756 "sat11.w"
;
if(su==ua)resize(bar(u)),ua+= ua,o,au= bimp[bar(u)].addr+su;
oo,mem[au]= v,bimp[bar(u)].size= su+1;
if(sv==va)resize(bar(v)),va+= va,o,av= bimp[bar(v)].addr+sv;
oo,mem[av]= u,bimp[bar(v)].size= sv+1;
}
}
}

/*:73*/
#line 1704 "sat11.w"
;
}

/*:72*/
#line 553 "sat11k.ch"
;
}
#line 1607 "sat11.w"

/*:69*/
#line 1496 "sat11.w"
;
}
rptr= eptr;

/*:63*/
#line 1485 "sat11.w"
;
if(o,nstack[level].branch<0){
if(level)goto chooseit;
forcedlits= 0;
goto enter_level;
}

/*:62*/
#line 1407 "sat11.w"
;
}else if((verbose&show_choices)&&level<=show_choices_max)
fprintf(stderr,"Level "O"d: no branch\n",
level);

/*:59*/
#line 3349 "sat11.w"
;
forcedlits= 0;
level++;
goto enter_level;
/*84:*/
#line 1929 "sat11.w"

dl_contra:/*148:*/
#line 3293 "sat11.w"

if(cs<dl_truth){
/*147:*/
#line 3272 "sat11.w"

{
dl_last_change= dlooklit;
dlooklit= bar(dlooklit);
dlook_cs= cs,cs= dl_truth;
/*149:*/
#line 1090 "sat11k.ch"

/*162:*/
#line 1265 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1272 "sat11k.ch"
;
}

/*:162*/
#line 1091 "sat11k.ch"
;
eptr= fptr;
#line 3302 "sat11.w"
l= dlooklit;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 3303 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*150:*/
#line 1126 "sat11k.ch"

bptr= 0;
if(verbose&show_doubly_gory_details)
fprintf(stderr," ("O"s"O".8s dlookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls<2&&bptr>=0)/*151:*/
#line 1147 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_doubly_gory_details)
fprintf(stderr,"  dlooking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3339 "sat11.w"

/*:151*/
#line 1134 "sat11k.ch"
;
}
if(bptr<0)goto dl_contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto dl_contra;
}else{
l= u;
/*145:*/
#line 3222 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr,"dlfixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto dl_contra;
}else{
if(verbose&show_doubly_gory_details){
if(cs>=dl_truth)fprintf(stderr," dlfixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:145*/
#line 1143 "sat11k.ch"
;
}
}

/*:150*/
#line 3307 "sat11.w"
;
}

#line 1125 "sat11k.ch"
/*:149*/
#line 3277 "sat11.w"
;
cs= dlook_cs;
wstack[wptr++]= dlooklit;
}

/*:147*/
#line 3295 "sat11.w"
;
goto dlook_on;
}
base= last_base;

#line 1090 "sat11k.ch"
/*:148*/
#line 1930 "sat11.w"
;
contra:/*130:*/
#line 2959 "sat11.w"

if(cs<proto_truth){
/*129:*/
#line 2941 "sat11.w"

{
looklit= bar(looklit);
forcedlit[forcedlits++]= looklit;
look_cs= cs,cs= proto_truth;
/*132:*/
#line 2976 "sat11.w"

#line 974 "sat11k.ch"
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 974 "sat11k.ch"
;
wptr= 0;eptr= fptr;
#line 2978 "sat11.w"
weighted_new_binaries= 0;
l= looklit;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 2980 "sat11.w"
;
while(fptr<eptr){
o,ll= rstack[fptr++];
/*135:*/
#line 1024 "sat11k.ch"

bptr= 0;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookout)\n",litname(bar(ll)));
for(o,tla= kinx[bar(ll)].addr,tls= kinx[bar(ll)].size;tls;tla++,tls--){
o,c= kmem[tla];
o,la= cinx[c].addr,ls= cinx[c].size-1;
o,cinx[c].size= ls;
if(ls>=2)weighted_new_binaries+= clause_weight[ls];
else if(bptr>=0)/*136:*/
#line 1049 "sat11k.ch"

{
for(o,ua= cinx[c-1].addr;la<ua;la++){
o,u= cmem[la];
if(!isfixed(u))break;
if(iscontrary(u))continue;
u= 0;break;
}
if(la==ua){
bptr= -1;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s-> ["O"d]\n",
litname(ll),c);
}else if(u){
o,bstack[bptr++].u= u;
if(verbose&show_gory_details)
fprintf(stderr,"  looking "O"s"O".8s->"O"s"O".8s ["O"d]\n",
litname(ll),litname(u),c);
}
}
#line 3033 "sat11.w"

/*:136*/
#line 1033 "sat11k.ch"
;
}
if(bptr<0)goto contra;
while(bptr){
o,u= bstack[--bptr].u;
if(isfixed(u)){
if(iscontrary(u))goto contra;
}else{
wstack[wptr++]= l= u;
/*125:*/
#line 2809 "sat11.w"

if(isfixed(l)){
if(iscontrary(l))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr,"protofixing "O"s"O".8s\n",
litname(l));
else fprintf(stderr,""O"dfixing "O"s"O".8s\n",
cs,litname(l));
}
stamptrue(l);
lfptr= eptr;
o,rstack[eptr++]= l;
while(lfptr<eptr){
o,l= rstack[lfptr++];
for(o,la= bimp[l].addr,ls= bimp[l].size;ls;la++,ls--){
o,lp= mem[la];
if(isfixed(lp)){
if(iscontrary(lp))goto contra;
}else{
if(verbose&show_gory_details){
if(cs>=proto_truth)fprintf(stderr," protofixing "O"s"O".8s\n",
litname(lp));
else fprintf(stderr," "O"dfixing "O"s"O".8s\n",
cs,litname(lp));
}
stamptrue(lp);
o,rstack[eptr++]= lp;
}
}
}
}

/*:125*/
#line 1042 "sat11k.ch"
;
}
}

/*:135*/
#line 2984 "sat11.w"
;
}
/*137:*/
#line 3036 "sat11.w"

if(wptr){
oo,sl= bimp[looklit].size,ls= bimp[looklit].alloc;
/*138:*/
#line 3056 "sat11.w"

if(o,lmem[looklit].istamp!=istamp){
o,lmem[looklit].istamp= istamp;
o,istack[iptr].lit= looklit,istack[iptr].size= sl;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 3060 "sat11.w"
;
}

/*:138*/
#line 3039 "sat11.w"
;
while(sl+wptr> ls)resize(looklit),ls<<= 1;
o,bimp[looklit].size= sl+wptr;
for(o,la= bimp[looklit].addr+sl;wptr;wptr--){
o,u= wstack[wptr-1];
o,mem[la++]= u;
if(verbose&show_gory_details)
fprintf(stderr," windfall "O"s"O".8s->"O"s"O".8s\n",
litname(looklit),litname(u));
o,au= bimp[bar(u)].addr,su= bimp[bar(u)].size;
/*74:*/
#line 1767 "sat11.w"

if(o,lmem[bar(u)].istamp!=istamp){
o,lmem[bar(u)].istamp= istamp;
o,istack[iptr].lit= bar(u),istack[iptr].size= su;
/*75:*/
#line 1774 "sat11.w"

iptr++;
if(iptr==iptr_max){
bytes+= iptr*sizeof(idata);
iptr_max<<= 1;
}

/*:75*/
#line 1771 "sat11.w"
;
}

/*:74*/
#line 3049 "sat11.w"
;
if(o,su==bimp[bar(u)].alloc)resize(bar(u)),o,au= bimp[bar(u)].addr;
o,mem[au+su]= bar(looklit);
o,bimp[bar(u)].size= su+1;
}
}

/*:137*/
#line 2986 "sat11.w"
;

/*:132*/
#line 2946 "sat11.w"
;
cs= look_cs;
}

/*:129*/
#line 2961 "sat11.w"
;
#line 957 "sat11k.ch"
goto look_on;
}
cs= near_truth;
/*161:*/
#line 1255 "sat11k.ch"

while(fptr> rptr){
o,u= rstack[fptr-1];
if(isfixed(u))break;
fptr--;
if(verbose&show_gory_details)
fprintf(stderr," ("O"s"O".8s lookin)\n",litname(bar(u)));
/*163:*/
#line 1275 "sat11k.ch"

for(o,tls= kinx[bar(u)].size,tla= kinx[bar(u)].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cis= cinx[c].size+1;
o,cinx[c].size= cis;
}

/*:163*/
#line 1262 "sat11k.ch"
;
}

/*:161*/
#line 960 "sat11k.ch"
;
#line 2964 "sat11.w"

/*:130*/
#line 1931 "sat11.w"
;
goto look_bad;
conflict:/*81:*/
#line 1880 "sat11.w"

for(j= fptr;j<eptr;j++)oo,stamp[thevar(rstack[j])]= 0;

#line 674 "sat11k.ch"
/*:81*/
#line 1933 "sat11.w"
;
backtrack:/*82:*/
#line 1913 "sat11.w"

for(j= fptr-1;j>=rptr;j--){
o,ll= rstack[j];
#line 699 "sat11k.ch"
tll= bar(ll);
/*83:*/
#line 712 "sat11k.ch"

if(verbose&show_details)
fprintf(stderr," ("O"s"O".8s in)\n",litname(tll));
for(o,tls= kinx[tll].size,tla= kinx[tll].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
o,cia= cinx[c].addr,cis= cinx[c].size+1;
o,cinx[c].size= cis;
if(cis==3){
o,u= cmem[cia];/*160:*/
#line 1243 "sat11k.ch"

oo,kinx[u].size++;

/*:160*/
#line 720 "sat11k.ch"
;
o,u= cmem[cia+1];/*160:*/
#line 1243 "sat11k.ch"

oo,kinx[u].size++;

/*:160*/
#line 721 "sat11k.ch"
;
}
}
#line 1928 "sat11.w"

/*:83*/
#line 701 "sat11k.ch"
;
/*159:*/
#line 1231 "sat11k.ch"

for(o,tls= kinx[ll].size,tla= kinx[ll].addr+tls-1;tls;tla--,tls--){
o,c= kmem[tla];
for(o,cia= cinx[c].addr,cis= cinx[c].size-1;cis;cia++){
o,u= cmem[cia];
if(isfree(u)){
/*160:*/
#line 1243 "sat11k.ch"

oo,kinx[u].size++;

/*:160*/
#line 1237 "sat11k.ch"
;
cis--;
}
}
}

/*:159*/
#line 702 "sat11k.ch"
;
#line 1918 "sat11.w"
freevars++;
o,stamp[thevar(ll)]= 0;
}

#line 712 "sat11k.ch"
/*:82*/
#line 1934 "sat11.w"
;
/*80:*/
#line 1866 "sat11.w"

if(o,nstack[level].branch>=0){
for(o,j= nstack[level].iptr;iptr> j;iptr--){
o,l= istack[iptr-1].lit,sl= istack[iptr-1].size;
o,bimp[l].size= sl;
}
}

/*:80*/
#line 1935 "sat11.w"
;
if(o,nstack[level].branch==0)/*85:*/
#line 1961 "sat11.w"

{
bestlit= bar(nstack[level].decision);
o,nstack[level].decision= bestlit,nstack[level].branch= 1;
if(level<32)prefix+= 1<<(31-level);
goto tryit;
}

/*:85*/
#line 1936 "sat11.w"
;
look_bad:if(level){
level--;
if(level<31)prefix&= -(1<<(31-level));
fptr= rptr;
o,rptr= nstack[level].rptr;
goto backtrack;
}
unsat:if(1){
printf("~\n");
if(verbose&show_basics)fprintf(stderr,"UNSAT\n");
}else{
satisfied:if(verbose&show_basics)fprintf(stderr,"!SAT!\n");
/*153:*/
#line 3355 "sat11.w"

for(k= 0;k<rptr;k++){
printf(" "O"s"O".8s",litname(rstack[k]));
if(out_file)fprintf(out_file," "O"s"O".8s",litname(bar(rstack[k])));
}
printf("\n");
if(freevars){
if(verbose&show_unused_vars)printf("(Unused:");
for(k= 0;k<freevars;k++){
if(verbose&show_unused_vars)printf(" "O".8s",vmem[freevar[k]].name.ch8);
if(out_file)fprintf(out_file," "O".8s",vmem[freevar[k]].name.ch8);
}
if(verbose&show_unused_vars)printf(")\n");
}
if(out_file)fprintf(out_file,"\n");

/*:153*/
#line 1949 "sat11.w"
;
}

/*:84*/
#line 3353 "sat11.w"
;

/*:152*/
#line 122 "sat11.w"
;
done:if(verbose&show_basics)
fprintf(stderr,
"Altogether "O"llu+"O"llu mems, "O"llu bytes, "O"llu nodes.\n",
imems,mems,bytes,nodes);
}

#line 26 "sat11k.ch"
/*:2*/