matectf_number.py

x = [Int('x'+i) for i in xrange(1,9)]

s = Solver()

for i in xrange(1,9):
    s.add(x[i] < 256)
# first
s.add(((x[5] + x[6])*(x[5] + x[6]) + x[4] * x[4]) == 153844)

s.add(((x[5] + x[6])*(x[5] + x[6]) + x[3] * x[3]) == 131400)

s.add(x[5] * x[5] - x[1] * x[1] == 181)

s.add(x[6] * x[6] - x[2] * x[2] == 46717)

s.add(x[1] * x[4] == 19080)

s.add(x[2] * x[3] == 15300)

s.add(x[1] * x[6] - x[5] * 119 + x[1] * x[5] == 18871)

s.add(x[2] * x[5] - 70 * x[6] + x[2] *x[6] == 16930 )

s.add(x[4] * x[5] - x[3] * x[6] == -16558)

s.add(x[1] * x[2] - x[7] == 9043)

s.add(x[7] * x[8] == 4247)

#second

s.add((x[4] + x[6]) * (x[5]+x[7])+x[5]*x[4] == 43907)

s.add(x[1] * x[2] + x[5] == 12563)

s.add((x[1] + x[6]) * (x[2] + x[6]) + x[3] * x[3] == 130348)

s.add(x[5] * x[1] - x[1] * x[2] == -10682)

s.add(x[4] * x[6] - x[3] * x[2] == -9474)

s.add(x[1] * x[4] == 15484)

s.add(x[2] * x[3] == 32384)

s.add(x[1] * x[6] - x[5] * 27 + x[2]*x[6] == 32257)

s.add(x[2] * x[7] - 74 * x[3] + x[1] * x[2] == 8670)

s.add(x[3] * x[4] - x[8] * x[7] == 28838)

s.add(x[1] * x[3] + x[7] == 24910)

s.add(x[7] * x[8] == 11136)

s.check()

print s.model()