from z3 import *
char = [Int('char[' + str(i) + ']') for i in range(0, 16)]
s = Solver()
for c in char:
    s.add(c >= 32)
    s.add(c <= 127)
s.add(((char[0] * 10) + (char[1] * 12) + (char[6] * 62) + (char[3] * 15) + (char[10] * 95) + (char[9] * 2) + (char[13] * 38) + (char[12] * 17) + (char[15] * 25) + (char[14] * 67)) == 0x8120)
s.add(((char[2] * 15) + (char[0] * 8) + (char[7] * 50) + (char[5] * 25) + (char[12] * 64) + (char[8] * 13) + (char[13] * 85))== 0x6002)
s.add(((char[0] * 58) + (char[5] * 55) + (char[2] * 25) + (char[9] * 12) + (char[14] * 86) + (char[13] * 57) + (char[1] * 35) + (char[7] * 35))== 0x7C2D)
s.add(((char[0] * 67) + (char[3] * 71) + (char[7] * 97) + (char[5] * 39) + (char[11] * 10) + (char[10] * 60))== 0x6D22)
s.add(((char[0] * 85) + (char[2] * 5) + (char[4] * 25) + (char[3] * 38) + (char[11] * 16) + (char[10] * 83) + (char[13] * 53) + (char[12] * 29))== 0x7550)
s.add(((char[0] * 0x3A) + (char[1] * 28) + (char[2]) + (char[8] * 3) + (char[4] * 65) + (char[10] * 81) + (char[9] * 6) + (char[14] * 78) + (char[12] * 62)) == 0x85F9)
s.add(((char[1] * 0x33) + (char[2] * 0x42) + (char[6] * 0x50) + (char[3] * 0x3F) + (char[13] * 0x5D) + (char[9] * 0x17))== 0x842C)
s.add(((char[3] * 0x13) + (char[5] * 0x5E) + (char[7] * 0x5A) + (char[6] * 0x1E) + (char[10] * 0x59) + (char[9] * 9) + (char[14] * 0x1A) + (char[11] * 8) + (char[15] * 0xA))== 0x7C9E)
s.add(((char[0] * 72) + (char[2] * 7) + (char[4] * 59) + (char[3] * 65) + (char[6] * 22) + (char[5] * 50) + (char[14] * 68) + (char[8] * 74) + (char[15] * 41))== 0x8E1C)
s.add(((char[12] * 13) + (char[0] * 13) + (char[5] * 11) + (char[8] * 50) + (char[7] * 84) + (char[11] * 52) + (char[10] * 57) + (char[14] * 60))== 0x7723)
s.add(((char[0] * 31) + (char[2] * 93) + (char[6] * 56) + (char[4] * 57) + (char[12] * 96) + (char[9] * 37) + (char[14] * 97))== 0xB050)
s.add(((char[0] * 18) + (char[2] * 17) + (char[4] * 12) + (char[3] * 58) + (char[6] * 14) + (char[5] * 71) + (char[11] * 46) +((char[9] + char[14] + (char[10] * 4)) * 8))== 0x5A4C)
s.add(((char[0] * 75) + (char[3] * 62) + (char[7] * 85) + (char[11] * 44) + (char[9] * 59) + (char[14] * 12) + ((char[6] + char[2] + char[4]) * 0x25))== 0x924E)
s.add(((char[4] * 36) + (char[11] * 86))== 0x1D7C)
s.add(((char[3] * 55) + (char[12] * 0xD) + (char[0] * 0x48) + (char[6] * 36) + (char[5] * 79) + (char[8] * 94) + (char[7] * 88) + (char[10] * 34) + (char[9] * 20) + (char[11] * 65) + (char[13] * 19))== 0xC1F0)
s.add(((char[1] * 56) + (char[2] * 36) + (char[5] * 19) + (char[4] * 8) + (char[8] * 57) + (char[7] * 71) + (char[13] * 6) + (char[11] * 99))== 0x60A0)
if str(s.check()) == 'sat':
    input = ''.join(chr(int(str(s.model()[i]))) for i in char)
    count = 1
    for i in input:
        print 'char' + str(count) + ' = ' + (hex(ord(i)))
        count += 1
    print input