#!/usr/bin/env python
"""
"""
from z3 import *
import sys
clave = []
s = Solver()
for i in range(21):
	clave.append(Int(str(i)))
	s.add(Or(And(clave[i] >= 48, clave[i] <= 57), And(clave[i] >= 65, clave[i] <= 90), And(clave[i] >= 97, clave[i] <= 125)))
s.add(clave[11]-clave[19]*clave[19]-clave[12]+clave[1] == -2500)
s.add(clave[16]+clave[14]+clave[6]-clave[17] == 262)
s.add(clave[20]*clave[15]-clave[11] == 5918)
s.add(clave[14]-clave[15]-clave[7]*clave[5]+clave[18] == -11683)
s.add(clave[15]*clave[3]*clave[0]-clave[9]+clave[3] == 1481101)
s.add(clave[10]*clave[15]*clave[10]-clave[17] == 1429187)
s.add(clave[7]*clave[4]-clave[16]*clave[1] == 3775)
s.add(clave[9]*clave[20]-clave[18] == 5098)
s.add(clave[18]*clave[13]*clave[14]*clave[13] == 50494950)
s.add(clave[9]-clave[14]-clave[3]-clave[6] == -227)
s.add(clave[9]*clave[0]*clave[3] == 1264032)
s.add(clave[3]*clave[10]-clave[1]*clave[18]-clave[4] == 7265)
s.add(clave[18]-clave[8]+clave[4]-clave[16]-clave[9] == -126)
s.add(clave[2]-clave[6]+clave[13]*clave[20]+clave[0] == 5366)
s.add(clave[5]-clave[17]*clave[10]-clave[18]+clave[12] == -5274)
s.add(clave[3]*clave[0]*clave[1] == 1289568)
s.add(clave[2]-clave[14]+clave[5]*clave[11] == 11530)
s.add(clave[16]+clave[14]*clave[14]+clave[7]*clave[19] == 15814)
s.add(clave[18]+clave[16]-clave[9]-clave[3] == -64)
s.add(clave[0]-clave[10]-clave[3]-clave[8] == -206)
s.add(clave[20]-clave[18]+clave[14]+clave[14]-clave[7] == 84)
s.check()
m = s.model()
sys.stdout.write("solucion: ")
for d in reversed(m.decls()):
	sys.stdout.write(chr(int(str(m[d]))))
sys.stdout.write('\n')
sys.stdout.flush()