#!/usr/bin/env python2
#
# File: pnw.py
# by @BitK_
#

from z3 import *

solver = Solver()

s = [BitVec('s[%d]' % d, 8) for d in range(51)]
for x in s:
    solver.add(x > 0)

solver.add(s[0] == s[6] + (s[38] ^ s[30]) - s[8])
solver.add(s[1] == s[42] ^ s[38] ^ s[20] ^ s[19])
solver.add(s[2] == s[35] + s[36] - s[19] - s[3] - s[44])
solver.add(s[3] == s[19] + (s[17] ^ (s[41] - s[10] - s[10])))
solver.add(s[4] == s[33] - s[21])
solver.add(s[5] == s[4] ^ s[4] ^ s[8] ^ s[39])
solver.add(s[6] == s[14] ^ (s[10] + s[25] - s[39]))
solver.add(s[7] == s[32] + (s[15] ^ s[1]))
solver.add(s[8] == s[8])
solver.add(s[9] == s[24] ^ s[7])
solver.add(s[10] == s[32] + (s[49] ^ s[17]) - s[4] )
solver.add(s[11] == (s[42] ^ s[38]) - s[17] - s[8])
solver.add(s[12] == s[14] + s[8])
solver.add(s[13] == s[45] + s[20])
solver.add(s[14] == s[9] + (s[20] ^ (s[25] - s[48])))
solver.add(s[15] == s[18] - s[31])
solver.add(s[16] == s[24] ^ s[46])
solver.add(s[17] == (s[13] + s[2] + s[47]) ^ s[14] ^ s[50])
solver.add(s[18] == s[0] + s[36] + s[44] - s[3])
solver.add(s[19] == (s[41] ^ s[30]) - s[25] - s[28])
solver.add(s[20] == s[25] ^ s[44])
solver.add(s[21] == s[25] + ((s[28] + s[22]) ^ (s[39] ^ s[21])))
solver.add(s[22] == (s[31] ^ s[44] - s[4] - s[12]) - s[30])
solver.add(s[23] == s[39] ^ (s[32] - s[14]))
solver.add(s[24] == s[21] ^ s[0] ^ s[18] ^ s[21])
solver.add(s[25] == s[18] + s[4] + (s[12] ^ s[17]) - s[11])
solver.add(s[26] == (s[32] ^ s[46]) + s[49] + s[20])
solver.add(s[27] == (s[36] + s[25] + s[39] - s[48] ))
solver.add(s[28] == s[14] ^ s[15])
solver.add(s[29] == s[1] + s[35]  - s[42])
solver.add(s[30] == s[8] - s[31] - s[30] - s[24])
solver.add(s[31] == s[42] ^ (s[15] + (s[18] - s[29])))
solver.add(s[32] == s[14] + s[5] + s[15] - s[44])
solver.add(s[33] == (s[20] ^ (s[45] - s[15])) - s[32])
solver.add(s[34] == (s[3] ^ s[33]) - s[20] - s[10])
solver.add(s[35] == (s[44] ^ (s[6] - s[43])) + s[1] - s[44])
solver.add(s[36] == s[49] ^ (s[31] + s[25] - s[28]))
solver.add(s[37] == s[11] + (s[34] ^ s[31]) - s[34])
solver.add(s[38] == s[42] + (s[27] ^ s[36]) - s[5])
solver.add(s[39] == s[37] ^ s[8])
solver.add(s[40] == (s[44] ^ (s[7] + s[28])) - s[10])
solver.add(s[41] == s[20] ^ s[7] ^ s[17] ^ s[26])
solver.add(s[42] == s[50] + s[1] - s[28])
solver.add(s[43] == s[46] + s[33] - s[15])
solver.add(s[44] == (s[24] + s[42] + s[16]) ^ s[45] ^ s[21])
solver.add(s[45] == s[22] - s[40])
solver.add(s[46] == s[12] - s[46] - s[7] - s[35])
solver.add(s[47] == (s[39] ^ (s[15] + s[26])) - s[12])
solver.add(s[48] == s[11] ^ (s[15] - s[8]))
solver.add(s[49] == s[27] ^ s[37])
solver.add(s[50] == (s[13] + s[8] + s[17]) ^ s[24] ^ s[15])

#solver.add(s[] == )
print ("SOLVING ...")
print solver.check()
solution = solver.model()
print "".join(chr(solution[s[d]].as_long()) for d in range(51))