#!/usr/bin/python3

from z3 import *

x,y,z = Ints('x y z')
a1,a2,a3,a4,a5,a6 = Ints('a1 a2 a3 a4 a5 a6')
s=Solver()
s.add(x>y, y>z, z>0)
max_limit=1000000
s.add(x<max_limit)
s.add(y<max_limit)
s.add(z<max_limit)
max_limit_sqr=(max_limit*2)**2
s.add(a1<max_limit_sqr)
s.add(a2<max_limit_sqr)
s.add(a3<max_limit_sqr)
s.add(a4<max_limit_sqr)
s.add(a5<max_limit_sqr)
s.add(a6<max_limit_sqr)
s.add(x + y == a1**2)
s.add(x - y == a2**2)
s.add(x + z == a3**2)
s.add(x - z == a4**2)
s.add(y + z == a5**2)
s.add(y - z == a6**2)

print (s.check())
print (s.model())