#!/usr/bin/ruby 

cages = [
  [3, [11,12]],
  [15,[13,14,15]],
  [22,[16,25,26,35]],
  [4, [17,27]],
  [16,[18,28]],
  [15,[19,29,39,49]],
  [25,[21,22,31,32]],
  [17,[23,24,]],
  [9, [33,34,44]],
  [8, [36,46,56]],
  [20,[37,38,47]],
  [6, [41,51]],
  [14,[42,43]],
  [17,[45,55,65]],
  [17,[48,57,58]],
  [13,[52,53,62]],
  [20,[54,64,74]],
  [12,[59,69]],
  [27,[61,62,63,64]],
  [6, [63,72,73]],
  [20,[66,76,77]],
  [6, [67,68]],
  [10,[75,84,85,94]],
  [14,[78,79,88,89]],
  [8, [82,92]],
  [16,[83,93]],
  [15,[86,87]],
  [13,[95,96,97]],
  [17,[98,99]]
]


for i in 1 .. 9
  for j in 1 .. 9
    print "(define x#{i}#{j} :: nat)\n"
  end
end
for i in 1 .. 9
  for j in 1 .. 9
    print "(assert (>= x#{i}#{j} 1))\n"
    print "(assert (<= x#{i}#{j} 9))\n"
  end
end

def alldifferent xs
  for i in 0 ... xs.size 
    for j in i+1 ... xs.size 
      print "(assert (not (= #{xs[i]} #{xs[j]})))\n"
    end
  end
end

cages.each {|a|
 print "(assert (= #{a[0]} (+ #{a[1].map{|i| "x#{i}"}.join(" ")})))\n"
 alldifferent(a[1].map {|i| "x#{i}"})
}

ns = 1 .. 9
ns.each {|i| 
  alldifferent(ns.map {|j| "x#{i}#{j}"})
  alldifferent(ns.map {|j| "x#{j}#{i}"})
}
ns.each {|i|
  alldifferent(ns.map {|j| "x#{i}#{j}"})
}
[1,4,7].each {|i| [1,4,7].each {|j|
  alldifferent(
    ["x#{i  }#{j}","x#{i  }#{j+1}","x#{i  }#{j+2}",
     "x#{i+1}#{j}","x#{i+1}#{j+1}","x#{i+1}#{j+2}",
     "x#{i+2}#{j}","x#{i+2}#{j+1}","x#{i+2}#{j+2}"])
} }

print "(set-evidence! true)\n(check)\n"