BEGIN{
 max = 1;
 wm = 1;
}

{
 if(NR==1){
  yoko = $1;
 }else if(NR==2){
  tate = $1;
 }else{
  if((NF<=yoko)||(NF<=tate)){
   print "(||"
  }
  if(NF<=yoko){
   for(i=0;i<tate;i++){
    for(j=0;j<yoko-NF+1;j++){
     print "(&&";
     if(j!=0){
      printf "(= x_" i "_" j-1 " " 0 ")\n";
     }
     for(k=0;k<NF;k++){
      printf "(= x_" i "_" k+j " " $(k+1) ")\n";
     }
     if(j!=yoko-NF){
      printf "(= x_" i "_" j+NF " " 0 ")\n";
     }
     print ")";
    }
   }
  }
  if(NF<=tate){
   for(i=0;i<yoko;i++){
    for(j=0;j<tate-NF+1;j++){
     print "(&&";
     if(j!=0){
      printf "(= x_" i "_" j-1 " " 0 ")\n";
     }
     for(k=0;k<NF;k++){
      printf "(= x_" k+j "_" i " " $(k+1) ")\n";
     }
     if(j!=yoko-NF){
      printf "(= x_" i "_" j+NF " " 0 ")\n";
     }
     print ")";
    }
   }
  }
  if((NF<=yoko)||(NF<=tate)){
   print ")";
  }

  wm = wm + NF - 1;
  for(k=0;k<NF;k++){
   if($(k+1)>=max){
    max = $(k+1);
   }
  }
 }
}

END{
 printf "\n";
 for(i=0;i<tate;i++){
  for(j=0;j<yoko;j++){
   print "(int x_" i "_" j " 0 " max ")";
  }
 }
 printf "\n";
 print "(= " wm " (+";
 for(i=0;i<tate;i++){
  for(j=0;j<yoko;j++){
   print "  (if ( > x_" i "_" j " 0 ) 1 0)";
  }
 }
 print ") )";
# print wm "\t" max;

 for(i=0;i<tate-1;i++){
  for(j=0;j<yoko-1;j++){
   print "(> 4 (+";
   print " (if ( > x_" i "_" j " 0 ) 1 0)";
   print " (if ( > x_" i+1 "_" j " 0 ) 1 0)";
   print " (if ( > x_" i "_" j+1 " 0 ) 1 0)";
   print " (if ( > x_" i+1 "_" j+1 " 0 ) 1 0)";
   print "))";
  }
 }

}