#!/usr/bin/env perl

$m=shift;
$n=shift;

$m > 0 and $n > 0 or die "Usage: $0 m n\n";
@formula=();

# So: xi,j,k ~ (k-1)*n*n + (j-1)*n+i

for($k=1; $k <= $m; $k++) {
  @clause=();
  for($i=1; $i <= $n; $i++) {
    for($j=1; $j <= $n; $j++) {
      push(@clause, ($k-1)*$n*$n + ($j-1)*$n+$i);
    }
  }
  push(@formula,join(" ",@clause) . " 0");
}


for($i=1; $i <= $n; $i++) {
  for($j=1; $j <= $n; $j++) {
    for($k=1; $k <= $m; $k++) { 
      for($l=1; $l <= $m; $l++) { 
        if($k != $l) {
          push(@formula,sprintf("-%d -%d 0",
                 ($k-1)*$n*$n + ($j-1)*$n+$i ,
                 ($l-1)*$n*$n + ($j-1)*$n+$i));
        }
      }
    }
  }
}

for($i=1; $i <= $n; $i++) {      
  for($j=1; $j <= $n; $j++) {    
    for($k=1; $k <= $m; $k++) {
      for($l=1; $l <= $n; $l++) {  
        for($h=1; $h <= $n; $h++) {  
          if(!($l==$i && $h==$j)) {
            push(@formula,sprintf("-%d -%d 0", 
                 ($k-1)*$n*$n + ($j-1)*$n+$i , 
                 ($k-1)*$n*$n + ($h-1)*$n+$l));
          }
        }
      }
    }
  }
}

for($i=1; $i <= $n; $i++) {
  for($j=1; $j <= $n; $j++) {
    for($k=1; $k <= $m; $k++) {
      for($l=1; $l <= $n; $l++) {
        for($h=1; $h <= $m; $h++) {
          if(!($l==$i && $h==$k)) {
            push(@formula,sprintf("-%d -%d 0", 
                 ($k-1)*$n*$n + ($j-1)*$n+$i , 
                 ($h-1)*$n*$n + ($j-1)*$n+$l));
          }
        }
      }
    }
  }
}

for($i=1; $i <= $n; $i++) {
  for($j=1; $j <= $n; $j++) {
    for($k=1; $k <= $m; $k++) {
      for($l=1; $l <= $n; $l++) {
        for($h=1; $h <= $m; $h++) {
          if(!($l==$j && $h==$k)) {
            push(@formula,sprintf("-%d -%d 0",
                 ($k-1)*$n*$n + ($j-1)*$n+$i ,
                 ($h-1)*$n*$n + ($l-1)*$n+$i));
          }                  
        }
      }
    }
  }
}


printf("p cnf %d %d\n",$m*$n*$n,$#formula+1);
foreach (@formula)
  {
  print "$_\n";
  }
