BEGIN{
 size = 12;
}
{
 if(NR<3){
  size = $0;
 }
 if((NR>2)&&(NR<size+3)){
  for(i=0;i<size;i++){
   hi[(NR-3)*size+i] = $(i+1);
  }
 }
}

END{
 for(i=0;i<size;i++){
  for(j=0;j<size;j++){
   printf("(int x_%d_%d 1 %d)\n",i,j,size);
  }
 }


 for(i=0;i<size;i++){
  for(j=0;j<size;j++){
   flag[j]=1;
  }
  for(j=0;j<size;j++){
   if(hi[size*i+j]=="0"){
    flag[j]=1;
   }else{
    for(k=j+1;k<size;k++){
     if(hi[size*i+j]==hi[size*i+k]){
      flag[j]=0;
      printf("(= x_%d_%d x_%d_%d)\n",i,j,i,k);
     }
    }
   }
  }
  printf "(alldifferent ";
  for(j=0;j<size;j++){
   if(flag[j]==1){
    printf("x_%d_%d ",i,j);
   }
  }
  printf ")\n";
 }

 printf("\n");

 for(i=0;i<size;i++){
  for(j=0;j<size;j++){
   flag[j]=1;
  }
  for(j=0;j<size;j++){
   if(hi[size*j+i]=="0"){
    flag[j]=1;
   }else{
    for(k=j+1;k<size;k++){
     if(hi[size*j+i]==hi[size*k+i]){
      flag[j]=0;
      printf("(= x_%d_%d x_%d_%d)\n",j,i,k,i);
     }
    }
   }
  }
  printf "(alldifferent ";
  for(j=0;j<size;j++){
   if(flag[j]==1){
    printf("x_%d_%d ",j,i);
   }
  }
  printf ")\n";
 }

}