text: #define o mems++
  #define oo mems+= 2
  #define ooo mems+= 3 \
  
  #define show_basics 1
  #define show_choices 2
  #define show_details 4
  #define show_gory_details 8
  #define show_histogram 16
  #define show_pis 32 \
  
  #define vars_per_vchunk 341 \
  
  #define cells_per_chunk 511 \
  
  #define hack_in(q,t) (tmp_var*) (t|(ullng) q)  \
  
  #define hack_out(q) (((ullng) q) &0x3) 
  #define hack_clean(q) ((tmp_var*) ((ullng) q&-4) )  \
  
  #define cl(p) mem[p].eta.u \
  
  #define removed (uint) (-1)  \
  
  /*3:*/
  #line 79 "./sat9.w"
  
  #include <stdio.h> 
  #include <stdlib.h> 
  #include <string.h> 
  #include "gb_flip.h"
  typedef unsigned int uint;
  typedef unsigned long long ullng;
  /*6:*/
  #line 207 "./sat9.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;
  
  /*:6*//*7:*/
  #line 234 "./sat9.w"
  
  typedef struct chunk_struct{
  struct chunk_struct*prev;
  tmp_var*cell[cells_per_chunk];
  }chunk;
  
  /*:7*//*24:*/
  #line 515 "./sat9.w"
  
  typedef struct{
  double eta;
  double pi;
  uint zf;
  uint link;
  int rating;
  }literal;
  typedef struct{
  uint start;
  uint size;
  }clause;
  typedef struct{
  union{double d;ullng u;}eta;
  uint lit;
  uint next;
  }mem_item;
  
  /*:24*/
  #line 86 "./sat9.w"
  ;
  /*4:*/
  #line 111 "./sat9.w"
  
  int random_seed= 0;
  int verbose= show_basics;
  int hbits= 8;
  int buf_size= 1024;
  int max_iter= 1000;
  int min_iter= 5;
  int confidence= 50;
  double damper= 0.99;
  double threshold= 0.01;
  ullng imems,mems;
  ullng thresh= 0;
  ullng delta= 0;
  ullng bytes;
  
  /*:4*//*8:*/
  #line 240 "./sat9.w"
  
  char*buf;
  tmp_var**hash;
  uint hash_bits[93][8];
  vchunk*cur_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;
  ullng cells;
  
  /*:8*//*25:*/
  #line 533 "./sat9.w"
  
  clause*cmem;
  literal*lmem;
  mem_item*mem;
  mem_item*cur_mcell;
  octa*nmem;
  double*gam;
  
  /*:25*//*36:*/
  #line 690 "./sat9.w"
  
  int iter;
  double acc,etabar,pi0,pi1,old_eta,new_eta,new_gam,factor,rein,diff;
  
  double max_diff;
  double factor;
  int azf;
  int max_iter;
  
  /*:36*//*54:*/
  #line 1099 "./sat9.w"
  
  int bucket[101],unit;
  int fixcount,unitcount;
  char name_buf[32];
  FILE*out_file;
  
  /*:54*/
  #line 87 "./sat9.w"
  ;
  /*26:*/
  #line 545 "./sat9.w"
  
  void print_clause(uint c){
  register uint l,ll;
  fprintf(stderr,"%d:\n",c);
  for(l= cmem[c-1].start;l<cmem[c].start;l++){
  ll= mem[l].lit;
  fprintf(stderr," %s%.8s(%d), eta=%.15g\n",
  ll&1?"~":"",nmem[ll>>1].ch8,ll>>1,mem[l].eta.d);
  }
  }
  
  /*:26*//*27:*/
  #line 559 "./sat9.w"
  
  void print_var(uint k){
  register uint l= k<<1;
  fprintf(stderr,"pi(%.8s)=%.15g(%d), eta(%.8s)=%.15g, ",
  nmem[k].ch8,lmem[l].pi,lmem[l].zf,nmem[k].ch8,lmem[l].eta);
  fprintf(stderr,"pi(~%.8s)=%.15g(%d), eta(~%.8s)=%.15g\n",
  nmem[k].ch8,lmem[l+1].pi,lmem[l+1].zf,nmem[k].ch8,lmem[l+1].eta);
  }
  
  /*:27*//*47:*/
  #line 974 "./sat9.w"
  
  int fixlist(register int k,int b){
  register int c,j,l,ll,p,q;
  for(;k&1;o,k= lmem[k].rating){
  if(o,lmem[k-1].rating<0)l= k;
  else l= k-1;
  printf(" %s%.8s",l&1?"~":"",nmem[l>>1].ch8);
  /*48:*/
  #line 987 "./sat9.w"
  
  for(o,p= lmem[l].link;p;o,p= mem[p-1].next){
  oo,c= cl(p-1),j= cmem[c].size;
  if(j)o,cmem[c].size= 0;
  }
  
  /*:48*/
  #line 981 "./sat9.w"
  ;
  /*49:*/
  #line 997 "./sat9.w"
  
  for(o,p= lmem[l^1].link;p;p= q){
  o,q= mem[p-1].next;
  oo,c= cl(p-1),j= cmem[c].size;
  if(j==0)continue;
  oo,mem[p-1].next= removed,cmem[c].size= j-1;
  if(j==2){
  for(o,p= cmem[c].start;o,mem[p].next==removed;p++);
  /*50:*/
  #line 1013 "./sat9.w"
  
  ll= mem[p].lit;
  if(ll&1){
  if(o,lmem[ll].rating){
  if(o,lmem[ll-1].rating> 0)goto contra;
  }else{
  o,lmem[ll-1].rating= -1;
  o,lmem[ll].rating= unit,unit= ll,unitcount++;
  }
  }else{
  if(o,lmem[ll+1].rating){
  if(o,lmem[ll].rating<0){
  contra:printf("\n");
  fprintf(stderr,"Oops, clause %d is contradicted",c);
  if(b>=0)fprintf(stderr," in bucket %d!\n",b);
  else fprintf(stderr," while propagating unit literals!\n");
  return 0;
  }
  }else{
  o,lmem[ll].rating= +1;
  o,lmem[ll+1].rating= unit,unit= ll+1,unitcount++;
  }
  }
  
  /*:50*/
  #line 1005 "./sat9.w"
  ;
  }
  }
  
  /*:49*/
  #line 982 "./sat9.w"
  ;
  }
  return 1;
  }
  
  /*:47*/
  #line 88 "./sat9.w"
  ;
  main(int argc,char*argv[]){
  register uint c,g,h,i,j,k,l,p,q,r,ii,kk,ll,fcount;
  /*5:*/
  #line 159 "./sat9.w"
  
  for(j= argc-1,k= 0;j;j--)switch(argv[j][0]){
  case'v':k|= (sscanf(argv[j]+1,"%d",&verbose)-1);break;
  case'h':k|= (sscanf(argv[j]+1,"%d",&hbits)-1);break;
  case'b':k|= (sscanf(argv[j]+1,"%d",&buf_size)-1);break;
  case's':k|= (sscanf(argv[j]+1,"%d",&random_seed)-1);break;
  case'd':k|= (sscanf(argv[j]+1,"%lld",&delta)-1);thresh= delta;break;
  case't':k|= (sscanf(argv[j]+1,"%d",&max_iter)-1);break;
  case'l':k|= (sscanf(argv[j]+1,"%d",&min_iter)-1);break;
  case'c':k|= (sscanf(argv[j]+1,"%d",&confidence)-1);break;
  case'p':k|= (sscanf(argv[j]+1,"%lf",&damper)-1);break;
  case'e':k|= (sscanf(argv[j]+1,"%lf",&threshold)-1);break;
  default:k= 1;
  }
  if(k||hbits<0||hbits> 30||buf_size<=0){
  fprintf(stderr,
  "Usage: %s [v<n>] [h<n>] [b<n>] [s<n>] [d<n>] [t<n>] [l<n>] [c<n>] [p<f>] [e<f>]\n",
  argv[0]);
  exit(-1);
  }
  if(damper<0.0||damper> 1.0){
  fprintf(stderr,"Parameter p should be between 0.0 and 1.0!\n");
  exit(-666);
  }
  if(confidence<0||confidence> 100){
  fprintf(stderr,"Parameter c should be between 0 and 100!\n");
  exit(-667);
  }
  
  /*:5*/
  #line 91 "./sat9.w"
  ;
  /*9:*/
  #line 255 "./sat9.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=%d)!\n",
  buf_size);
  exit(-2);
  }
  hash= (tmp_var**)malloc(sizeof(tmp_var)<<hbits);
  if(!hash){
  fprintf(stderr,"Couldn't allocate %d hash list heads (hbits=%d)!\n",
  1<<hbits,hbits);
  exit(-3);
  }
  for(h= 0;h<1<<hbits;h++)hash[h]= NULL;
  
  /*:9*//*15:*/
  #line 393 "./sat9.w"
  
  for(j= 92;j;j--)for(k= 0;k<8;k++)
  hash_bits[j][k]= gb_next_rand();
  
  /*:15*/
  #line 92 "./sat9.w"
  ;
  /*10:*/
  #line 284 "./sat9.w"
  
  while(1){
  if(!fgets(buf,buf_size,stdin))break;
  clauses++;
  if(buf[strlen(buf)-1]!='\n'){
  fprintf(stderr,
  "The clause on line %d (%.20s...) is too long for me;\n",clauses,buf);
  fprintf(stderr," my buf_size is only %d!\n",buf_size);
  fprintf(stderr,"Please use the command-line option b<newsize>.\n");
  exit(-4);
  }
  /*11:*/
  #line 321 "./sat9.w"
  
  for(j= k= 0;;){
  while(buf[j]==' ')j++;
  if(buf[j]=='\n')break;
  if(buf[j]<' '||buf[j]> '~'){
  fprintf(stderr,"Illegal character (code #%x) in the clause on line %d!\n",
  buf[j],clauses);
  exit(-5);
  }
  if(buf[j]=='~')i= 1,j++;
  else i= 0;
  /*12:*/
  #line 346 "./sat9.w"
  
  {
  register tmp_var*p;
  if(cur_tmp_var==bad_tmp_var)/*13:*/
  #line 364 "./sat9.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 349 "./sat9.w"
  ;
  /*16:*/
  #line 397 "./sat9.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 %.9s... in the clause on line %d 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)goto empty_clause;
  j+= l;
  h&= (1<<hbits)-1;
  
  /*:16*/
  #line 351 "./sat9.w"
  ;
  /*17:*/
  #line 413 "./sat9.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 352 "./sat9.w"
  ;
  if(p->stamp==clauses||p->stamp==-clauses)/*18:*/
  #line 427 "./sat9.w"
  
  {
  if((p->stamp> 0)==(i> 0))goto empty_clause;
  }
  
  /*:18*/
  #line 353 "./sat9.w"
  
  else{
  p->stamp= (i?-clauses:clauses);
  if(cur_cell==bad_cell)/*14:*/
  #line 377 "./sat9.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 356 "./sat9.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 332 "./sat9.w"
  ;
  }
  if(k==0){
  fprintf(stderr,"(Empty line %d is being ignored)\n",clauses);
  nullclauses++;
  }
  goto clause_done;
  empty_clause:/*19:*/
  #line 437 "./sat9.w"
  
  while(k){
  /*20:*/
  #line 446 "./sat9.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 439 "./sat9.w"
  ;
  k--;
  }
  if((buf[0]!='~')||(buf[1]!=' '))
  fprintf(stderr,"(The clause on line %d is always satisfied)\n",clauses);
  nullclauses++;
  
  /*:19*/
  #line 339 "./sat9.w"
  ;
  clause_done:cells+= k;
  
  /*:11*/
  #line 295 "./sat9.w"
  ;
  }
  if((vars>>hbits)>=10){
  fprintf(stderr,"There are %d variables but only %d hash tables;\n",
  vars,1<<hbits);
  while((vars>>hbits)>=10)hbits++;
  fprintf(stderr," maybe you should use command-line option h%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 %llu variables!\n",vars);
  exit(-664);
  }
  if(clauses>=0x80000000){
  fprintf(stderr,"Whoa, the input had %llu clauses!\n",clauses);
  exit(-665);
  }
  if(cells>=0x100000000){
  fprintf(stderr,"Whoa, the input had %llu occurrences of literals!\n",cells);
  exit(-666);
  }
  
  /*:10*/
  #line 93 "./sat9.w"
  ;
  if(verbose&show_basics)
  /*22:*/
  #line 464 "./sat9.w"
  
  fprintf(stderr,"(%d variables, %d clauses, %llu literals successfully read)\n",
  vars,clauses,cells);
  
  /*:22*/
  #line 95 "./sat9.w"
  ;
  /*28:*/
  #line 572 "./sat9.w"
  
  /*29:*/
  #line 580 "./sat9.w"
  
  free(buf);free(hash);
  lmem= (literal*)malloc((vars+vars+1)*sizeof(literal));
  if(!lmem){
  fprintf(stderr,"Oops, I can't allocate the lmem array!\n");
  exit(-12);
  }
  bytes= (vars+vars+1)*sizeof(literal);
  nmem= (octa*)malloc(vars*sizeof(octa));
  if(!nmem){
  fprintf(stderr,"Oops, I can't allocate the nmem array!\n");
  exit(-13);
  }
  bytes+= vars*sizeof(octa);
  mem= (mem_item*)malloc(cells*sizeof(mem_item));
  if(!mem){
  fprintf(stderr,"Oops, I can't allocate the big mem array!\n");
  exit(-10);
  }
  bytes+= cells*sizeof(mem_item);
  cmem= (clause*)malloc((clauses+1)*sizeof(clause));
  if(!cmem){
  fprintf(stderr,"Oops, I can't allocate the cmem array!\n");
  exit(-11);
  }
  bytes+= (clauses+1)*sizeof(clause);
  
  /*:29*/
  #line 573 "./sat9.w"
  ;
  /*30:*/
  #line 607 "./sat9.w"
  
  for(l= vars+vars;l;l--)o,lmem[l-1].link= 0;
  
  /*:30*/
  #line 574 "./sat9.w"
  ;
  /*31:*/
  #line 610 "./sat9.w"
  
  for(c= clauses,cur_mcell= mem+cells,kk= 0;c;c--){
  o,cmem[c].start= cur_mcell-mem;
  k= 0;
  /*32:*/
  #line 635 "./sat9.w"
  
  for(i= 0;i<2;k++){
  /*20:*/
  #line 446 "./sat9.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 637 "./sat9.w"
  ;
  i= hack_out(*cur_cell);
  p= hack_clean(*cur_cell)->serial;
  cur_mcell--;
  o,cur_mcell->lit= l= p+p+(i&1);
  oo,cur_mcell->next= lmem[l].link;
  o,lmem[l].link= cur_mcell-mem+1;
  }
  
  /*:32*/
  #line 614 "./sat9.w"
  ;
  if(k> kk)kk= k;
  }
  if(cur_mcell!=mem){
  fprintf(stderr,"Confusion about the number of cells!\n");
  exit(-99);
  }
  o,cmem[0].start= 0;
  gam= (double*)malloc(kk*sizeof(double));
  if(!gam){
  fprintf(stderr,"Oops, I can't allocate the gamma array!\n");
  exit(-16);
  }
  bytes+= kk*sizeof(double);
  
  /*:31*/
  #line 576 "./sat9.w"
  ;
  /*33:*/
  #line 646 "./sat9.w"
  
  for(c= vars;c;c--){
  /*21:*/
  #line 455 "./sat9.w"
  
  if(cur_tmp_var> &cur_vchunk->var[0])cur_tmp_var--;
  else{
  register vchunk*old_vchunk= cur_vchunk;
  cur_vchunk= old_vchunk->prev;free(old_vchunk);
  bad_tmp_var= &cur_vchunk->var[vars_per_vchunk];
  cur_tmp_var= bad_tmp_var-1;
  }
  
  /*:21*/
  #line 648 "./sat9.w"
  ;
  o,nmem[c-1].lng= cur_tmp_var->name.lng;
  }
  
  /*:33*/
  #line 577 "./sat9.w"
  ;
  /*34:*/
  #line 655 "./sat9.w"
  
  if(cur_cell!=&cur_chunk->cell[0]||
  cur_chunk->prev!=NULL||
  cur_tmp_var!=&cur_vchunk->var[0]||
  cur_vchunk->prev!=NULL){
  fprintf(stderr,"This can't happen (consistency check failure)!\n");
  exit(-14);
  }
  free(cur_chunk);free(cur_vchunk);
  
  /*:34*/
  #line 578 "./sat9.w"
  ;
  
  /*:28*/
  #line 96 "./sat9.w"
  ;
  imems= mems,mems= 0;
  /*35:*/
  #line 667 "./sat9.w"
  
  factor= 1.0;
  /*37:*/
  #line 707 "./sat9.w"
  
  for(k= 0;k<cells;k++)
  mems+= 5,mem[k].eta.d= ((double)(gb_next_rand()))/2147483647.0;
  for(k= 0;k<vars+vars;k+= 2)
  ooo,lmem[k].eta= 0.0,lmem[k+1].eta= 0.0;
  
  /*:37*/
  #line 669 "./sat9.w"
  ;
  for(iter= 0;iter<max_iter;iter++){
  if((iter&1)&&iter>=min_iter){
  /*39:*/
  #line 746 "./sat9.w"
  
  {
  factor*= damper;
  rein= 1.0-factor;
  if(verbose&show_details)
  fprintf(stderr," (rein=%.15g)\n",rein);
  for(l= 0;l<vars+vars;l+= 2){
  if(o,lmem[l].zf)pi0= 0.0;
  else o,pi0= lmem[l].pi;
  if(o,lmem[l+1].zf)pi1= 0.0;
  else o,pi1= lmem[l+1].pi;
  if(pi0+pi1==0.0){
  if(verbose&show_basics)
  fprintf(stderr,
  "Sorry, a contradiction was found after iteration %d!\n",iter);
  goto contradiction;
  }
  if(pi1> pi0){
  o,lmem[l].rating= (pi0>=0.5?0:1);
  if((verbose&show_gory_details)&&lmem[l+1].eta)
  fprintf(stderr," eta(~%.8s) reset\n",nmem[l>>1].ch8);
  oo,lmem[l].eta= rein*(pi1-pi0)/(pi0+pi1-pi0*pi1),lmem[l+1].eta= 0.0;
  }else{
  o,lmem[l].rating= (pi1>=0.5?0:-1);
  if((verbose&show_gory_details)&&lmem[l].eta)
  fprintf(stderr," eta(%.8s) reset\n",nmem[l>>1].ch8);
  oo,lmem[l+1].eta= rein*(pi0-pi1)/(pi0+pi1-pi0*pi1),lmem[l].eta= 0.0;
  }
  }
  }
  
  /*:39*/
  #line 672 "./sat9.w"
  ;
  /*40:*/
  #line 784 "./sat9.w"
  
  for(k= c= 0;c<clauses;c++){
  for(o;k<cmem[c+1].start;k++){
  oo,l= mem[k].lit,p= lmem[l&-2].rating;
  if(p==0)goto ok;
  if(((int)p<0)==(l&1))goto ok;
  }
  goto not_ok;
  ok:k= cmem[c+1].start;
  continue;
  }
  if(verbose&show_details)
  fprintf(stderr,"Clauses pseudo-satisfied on iteration %d\n",iter+1);
  break;
  not_ok:
  
  /*:40*/
  #line 673 "./sat9.w"
  ;
  }
  if(verbose&show_choices)
  fprintf(stderr,"beginning iteration %d\n",iter+1);
  /*38:*/
  #line 713 "./sat9.w"
  
  for(l= 0;l<vars+vars;l++){
  if(o,lmem[l].eta==1.0)acc= 1.0,azf= 1;
  else acc= 1.0-lmem[l].eta,azf= 0;
  for(j= lmem[l].link;j;j= mem[j-1].next){
  o,etabar= 1.0-mem[j-1].eta.d;
  if(etabar==0.0)azf++;
  else acc*= etabar;
  }
  oo,lmem[l].zf= azf,lmem[l].pi= acc;
  }
  
  /*:38*/
  #line 677 "./sat9.w"
  ;
  /*41:*/
  #line 805 "./sat9.w"
  
  max_diff= 0.0;
  for(k= c= 0;c<clauses;c++){
  acc= 1.0,azf= 0;
  for(o,j= 0;k<cmem[c+1].start;j++,k++){
  o,l= mem[k].lit;
  if(o,lmem[l^1].zf)pi0= 0.0;
  else o,pi0= lmem[l^1].pi;
  o,old_eta= mem[k].eta.d;
  if(old_eta==1.0){
  if(o,lmem[l].zf> 1)pi1= 0.0;
  else o,pi1= lmem[l].pi;
  }else if(o,lmem[l].zf)pi1= 0.0;
  else o,pi1= lmem[l].pi/(1.0-old_eta);
  pi1= pi1*(1.0-pi0);
  if(pi1==0.0)azf++,o,gam[j]= 0.0;
  else{
  new_gam= pi1/(pi1+pi0);
  o,gam[j]= new_gam;
  acc*= new_gam;
  }
  }
  for(i= j;i;i--){
  if(o,gam[j-i]==0.0){
  if(azf> 1)new_eta= 0.0;
  else new_eta= acc;
  }else if(azf)new_eta= 0.0;
  else new_eta= acc/gam[j-i];
  o,diff= new_eta-mem[k-i].eta.d;
  if(diff> 0){
  if(diff> max_diff)max_diff= diff;
  }else if(-diff> max_diff)max_diff= -diff;
  o,mem[k-i].eta.d= new_eta;
  }
  }
  
  /*:41*/
  #line 678 "./sat9.w"
  ;
  if(verbose&show_details)
  fprintf(stderr," (max diff %.15g, %lld mems)\n",max_diff,mems);
  if(delta&&(mems>=thresh)){
  thresh+= delta;
  fprintf(stderr," after %lld mems, iteration %d had max diff %g\n",
  mems,iter+1,max_diff);
  }
  if(max_diff<threshold&&iter>=min_iter)break;
  }
  /*42:*/
  #line 847 "./sat9.w"
  
  if(iter==max_iter){
  if(verbose&show_basics)
  fprintf(stderr,"The messages didn't converge.\n");
  goto contradiction;
  }
  if(verbose&show_pis)
  /*43:*/
  #line 868 "./sat9.w"
  
  {
  if(iter<max_iter)
  fprintf(stderr,"converged after %d iterations.\n",iter+1);
  else fprintf(stderr,"no convergence (diff %g) after %d iterations.\n",
  max_diff,max_iter);
  fprintf(stderr,"variable      pi(v)        pi(~v)         1    0    *\n");
  for(k= 0;k<vars;k++){
  double den;
  fprintf(stderr,"%8.8s %10.7f(%d) %10.7f(%d)",
  nmem[k].ch8,lmem[k+k].pi,lmem[k+k].zf,lmem[k+k+1].pi,lmem[k+k+1].zf);
  pi0= lmem[k+k].pi;
  if(lmem[k+k].zf)pi0= 0.0;
  pi1= lmem[k+k+1].pi;
  if(lmem[k+k+1].zf)pi1= 0.0;
  den= pi0+pi1-pi0*pi1;
  fprintf(stderr,"    %4.2f %4.2f %4.2f\n",
  pi1*(1-pi0)/den,pi0*(1-pi1)/den,pi0*pi1/den);
  }
  }
  
  /*:43*/
  #line 854 "./sat9.w"
  ;
  if(verbose&show_histogram)
  /*44:*/
  #line 889 "./sat9.w"
  
  {
  uint hist[10][10];
  for(j= 0;j<10;j++)for(k= 0;k<10;k++)hist[j][k]= 0;
  for(k= 0;k<vars;k++){
  i= (int)(10*lmem[k+k].pi),j= (int)(10*lmem[k+k+1].pi);
  if(lmem[k+k].zf)i= 0;
  if(lmem[k+k+1].zf)j= 0;
  if(i==10)i= 9;
  if(j==10)j= 9;
  hist[i][j]++;
  }
  fprintf(stderr,"Histogram of the pi's, after %d iterations:\n",iter+1);
  for(j= 10;j;j--){
  for(i= 0;i<10;i++)fprintf(stderr,"%7d",hist[i][j-1]);
  fprintf(stderr,"\n");
  }
  }
  
  /*:44*/
  #line 856 "./sat9.w"
  ;
  /*45:*/
  #line 927 "./sat9.w"
  
  for(k= confidence;k<=100;k++)o,bucket[k]= 2;
  unit= 2;
  for(l= 0;l<vars+vars;l+= 2){
  if(o,lmem[l].zf)pi0= 0.0;
  else o,pi0= lmem[l].pi;
  if(o,lmem[l+1].zf)pi1= 0.0;
  else o,pi1= lmem[l+1].pi;
  if(pi0+pi1==0.0){
  if(verbose&show_basics)
  fprintf(stderr,"Sorry, a contradiction was found!\n");
  goto contradiction;
  }
  acc= (pi1-pi0)/(pi0+pi1-pi0*pi1);
  o,lmem[l].rating= acc> 0?+1:acc<0?-1:0;
  if(acc<0)acc= -acc;
  j= (int)(100.0*acc);
  if(j>=confidence){
  oo,lmem[l+1].rating= bucket[j];
  o,bucket[j]= l+1;
  fixcount++;
  }
  }
  if(verbose&show_basics)
  fprintf(stderr,"(fixing %d variables after %d iterations, e=%g)\n",
  fixcount,iter+1,max_diff);
  
  /*:45*/
  #line 857 "./sat9.w"
  ;
  /*46:*/
  #line 963 "./sat9.w"
  
  for(k= c= 0;c<clauses;c++){
  for(;k<cmem[c+1].start;k++)o,cl(k)= c;
  oo,cmem[c].size= k-cmem[c].start;
  if(cmem[c].size==1){
  /*51:*/
  #line 1037 "./sat9.w"
  
  ll= mem[k-1].lit;
  if(ll&1){
  if(o,lmem[ll].rating){
  if(o,lmem[ll-1].rating> 0)goto contra;
  }else{
  o,lmem[ll-1].rating= -1;
  o,lmem[ll].rating= unit,unit= ll,unitcount++;
  }
  }else{
  if(o,lmem[ll+1].rating){
  if(o,lmem[ll].rating<0){
  contra:printf("\n");
  fprintf(stderr,"Oops, clause %d is contradicted!\n",c);
  goto contradiction;
  }
  }else{
  o,lmem[ll].rating= +1;
  o,lmem[ll+1].rating= unit,unit= ll+1,unitcount++;
  }
  }
  
  /*:51*/
  #line 968 "./sat9.w"
  ;
  }
  }
  
  /*:46*/
  #line 858 "./sat9.w"
  ;
  /*52:*/
  #line 1059 "./sat9.w"
  
  for(k= 100;k>=confidence;k--)
  if(ooo,fixlist(bucket[k],k)==0)goto contradiction;
  while(unit&1){
  p= unit,unit= 2;
  if(oo,fixlist(p,-1)==0)goto contradiction;
  }
  printf("\n");
  if(unitcount&&(verbose&show_basics))
  fprintf(stderr,"(unit propagation fixed %d more variable%s)\n",
  unitcount,unitcount==1?"":"s");
  
  /*:52*/
  #line 859 "./sat9.w"
  ;
  /*53:*/
  #line 1071 "./sat9.w"
  
  sprintf(name_buf,"/tmp/sat9-%d.dat",random_seed);
  out_file= fopen(name_buf,"w");
  if(!out_file){
  fprintf(stderr,"I can't open `%s' for writing!\n");
  exit(-668);
  }
  for(kk= k= p= c= 0;c<clauses;c++){
  o,i= cmem[c].size;
  if(i==0){
  o,k= cmem[c+1].start;
  continue;
  }
  p++;
  while(i> kk)gam[kk++]= 0;
  gam[i-1]+= 1;
  for(o;k<cmem[c+1].start;k++)if(o,mem[k].next!=removed){
  l= mem[k].lit;
  fprintf(out_file," %s%.8s",l&1?"~":"",nmem[l>>1].ch8);
  }
  fprintf(out_file,"\n");
  }
  fclose(out_file);
  fprintf(stderr,"Reduced problem of %d clauses written on file %s\n",
  p,name_buf);
  for(i= 0;i<kk;i++)if(gam[i])
  fprintf(stderr," (%g %d-clauses)\n",gam[i],i+1);
  
  /*:53*/
  #line 860 "./sat9.w"
  ;
  goto done;
  contradiction:printf("~~?\n");
  done:
  
  /*:42*/
  #line 688 "./sat9.w"
  ;
  
  /*:35*/
  #line 98 "./sat9.w"
  ;
  if(verbose&show_basics)
  fprintf(stderr,"Altogether %llu+%llu mems, %llu bytes.\n",
  imems,mems,bytes);
  }
  
  /*:3*/
  