admin

#!/usr/bin/env ruby

require "z3"
require "pry"

solver = Z3::Solver.new

r = (0..35).map{|i| Z3.Int("c#{i}")}
u = (0..4).map{|i| Z3.Int("u#{i}")}

solver.assert Z3.And(*u.zip("admin".chars.map(&:ord)).map{|var,val| var == val})

solver.assert Z3.And(
  r[29] == u[3] - 56,
  r[31] == r[4] + 2,
  r[4] == r[18] + 1,
  r[35] == r[8] - 45,
  r[33] == r[10] - 7,
  r[12] == r[25] + 28,
  r[11] == r[31] - 19,
  r[2] == u[0] - 46,
  r[34] == r[6],
  r[9] == r[26],
  r[30] == r[19] + 57,
  r[1] == r[12],
  r[23] == r[7] + 63,
  r[24] == r[0] - 33,
  r[8] == r[28] - 29,
  r[17] == r[1] - 55,
  r[15] == r[23],
  r[32] == u[4] - 40,
  r[14] == r[24] + 17,
  r[16] == r[17] - 1,
  r[7] == r[9] + 3,
  r[22] == r[16] + 69,
  r[19] == r[3],
  r[26] == r[21],
  r[25] == r[34] - 38,
  r[6] == r[15],
  r[3] == r[35] + 20,
  r[21] == r[33],
  r[13] == u[2] - 58,
  r[27] == r[22] - 6,
  r[10] == r[20] - 34,
  r[5] == r[30] - 45,
  r[0] == r[11],
  r[20] == r[5] + 24,
  r[28] == r[14] + 39,
  r[18] == u[1],
)

raise unless solver.satisfiable?
puts r.map{|ri| solver.model[ri].to_i.chr}.join # Th35eAr3N07Th3Dr01d5Y0ur3L0ok1ngF0r!