from z3 import *

s = Solver()
vars = [IntVector(f"x{i}", i+1) for i in range(9)]

for i in range(9):
  # ziadne cisla v riadku sa neopakuju
  s.add(Distinct(vars[i]))
  for j in range(i+1):
    # domena je <1, 9>
    s.add(vars[i][j] > 0, vars[i][j] < 10)

def SumOrDec(x, y, z):
  return Or(x == y + z, x == y - z, x == z - y)

for i in range(8):
  # kazde cislo je +/- cisiel pod
  s.add([SumOrDec(vars[i][j],
                 vars[i+1][j],
                 vars[i+1][j+1]) for j in range(i+1)])

s.add(vars[1][0] == 5)
s.add(vars[2][2] == 1)
s.add(vars[3][0] == 1)
s.add(vars[4][2] == 4)
s.add(vars[5][0] == 6)
s.add(vars[5][4] == 3)
s.add(vars[7][3] == 2)