require "bundler/inline"

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

require "z3"

input = DATA.read

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

def wins(machine)
  a = Z3.Int("a")
  b = Z3.Int("b")

  solver = Z3::Solver.new
  machine.transpose.each do |a_, b_, c|
    solver.assert a*a_ + b*b_ == c
  end
  if solver.satisfiable?
    model = solver.model
    [a, b].map { model[_1].to_i }
  else
    nil
  end
end

pp machines.map { wins(_1) }.compact.sum { 3 * _1 + _2 }

pp machines
  .map {|a,b,c| [a,b,c.map { _1 + 10_000_000_000_000 }] }
  .map { wins(_1) }.compact.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