require "bundler/inline"

gemfile do
  source "https://rubygems.org"
  gem "z3"
end

input = DATA.read

machines = input.split("\n\n")
  .map {|machine| machine.scan(/\d+/).map(&:to_i) }

wins = ->(machine) {
  ax, ay = machine[0,2]
  bx, by = machine[2,2]
  cx, cy = machine[4,2]

  (0..cx/ax).filter_map {|a|
    b = (cx - a * ax) / bx.to_f
    if a * ax + b.to_i * bx == cx && a * ay + b.to_i * by == cy
      [a, b.to_i]
    else
      nil
    end
  }.sort_by {|a,b| a + b }
}

pp machines.map { wins[_1].first }.compact.sum { 3 * _1 + _2 }

require "z3"

machines.each do |machine|
  machine[4,2] = machine[4,2].map { _1 + 10_000_000_000_000 }
end

def wins(machine)
  return enum_for(__method__, machine) unless block_given?

  ax, ay = machine[0,2]
  bx, by = machine[2,2]
  cx, cy = machine[4,2]

  solutions = []
  loop do
    a = Z3.Int("a")
    b = Z3.Int("b")
    solver = Z3::Solver.new
    solver.assert cx == a*ax + b*bx
    solver.assert cy == a*ay + b*by
    solutions.each do |a_s, b_s|
      solver.assert a != a_s
    end
    return unless solver.satisfiable?

    model = solver.model
    solutions << [model[a].to_i, model[b].to_i]
    yield solutions.last
  end
end

pp machines.flat_map {|m| wins(m).sort_by { _1 + _2 } }.reject(&:empty?).sum { 3 * _1 + _2 }

__END__
Button A: X+94, Y+34
Button B: X+22, Y+67
Prize: X=8400, Y=5400

Button A: X+26, Y+66
Button B: X+67, Y+21
Prize: X=12748, Y=12176

Button A: X+17, Y+86
Button B: X+84, Y+37
Prize: X=7870, Y=6450

Button A: X+69, Y+23
Button B: X+27, Y+71
Prize: X=18641, Y=10279