from z3 import *

s = Solver()
char1 = BitVec('char1', 8)
char2 = BitVec('char2', 8)
char3 = BitVec('char3', 8)
char4 = BitVec('char4', 8)
char5 = BitVec('char5', 8)
char6 = BitVec('char6', 8)
char7 = BitVec('char7', 8)
char8 = BitVec('char8', 8)
char9 = BitVec('char9', 8)
char10 = BitVec('char10', 8)
char11 = BitVec('char11', 8)
char12 = BitVec('char12', 8)
char13 = BitVec('char13', 8)
char14 = BitVec('char14', 8)
char15 = BitVec('char15', 8)
char16 = BitVec('char16', 8)
char = [char1, char2, char3, char4, char5, char6, char7, char8, char9, char10, char11, char12, char13, char14, char15, char16]
s.add(char1 >= 32, char1 <= 127)
s.add(char2 >= 32, char2 <= 127)
s.add(char3 >= 32, char3 <= 127)
s.add(char4 >= 32, char4 <= 127)
s.add(char5 >= 32, char5 <= 127)
s.add(char6 >= 32, char6 <= 127)
s.add(char7 >= 32, char7 <= 127)
s.add(char8 >= 32, char8 <= 127)
s.add(char9 >= 32, char9 <= 127)
s.add(char10 >= 32, char10 <= 127)
s.add(char11 >= 32, char11 <= 127)
s.add(char12 >= 32, char12 <= 127)
s.add(char13 >= 32, char13 <= 127)
s.add(char14 >= 32, char14 <= 127)
s.add(char15 >= 32, char15 <= 127)
s.add(char16 >= 32, char16 <= 127)
s.add(((char1 * 10) + (char2 * 12) + (char7 * 62) + (char4 * 15) + (char11 * 95) + (char10 << 1) + (char14 * 38) + (char13 * 17) + (char16 * 25) + (char15 * 67)) == 0x8120)
s.add(((char3 * 15) + (char1 << 3) + (char8 * 50) + (char6 * 25) + (char13 << 6) + (char9 * 13) + (char14 * 85)) == 0x6002)
s.add(((char1 * 58) + (char6 * 55) + (char3 * 25) + (char10 * 12) + (char15 * 86) + (char14 * 57)) == 0x7C2D)
s.add(((char1 * 67) + (char4 * 71) + (char8 * 97) + (char6 * 39) + (char12 * 10) + (char11 * 60)) == 0x6D22)
s.add(((char1 * 85) + (char3 * 5) + (char5 * 25) + (char4 * 38) + (char12 << 4) + (char11 * 83) + (char14 * 53) + (char13 * 29)) == 0x7550)
s.add(((char2 * 28) + (char9 * 3) + (char5 * 65) + (char11 * 81) + (char10 * 6) + (char15 * 78) + (char13 * 62)) == 0x85F9)
s.add(((char2 * 51) + (char3 * 66) + (char7 * 80) + (char4 * 63) + (char14 * 93) + (char10 * 23)) == 0x842C)
s.add(((char4 * 19) + (char6 * 94) + (char8 * 90) + (char7 * 30) + (char11 * 89) + (char10 * 9) + (char15 * 26) + (char12 << 3) + (char16 * 10)) == 0x7C9E)
s.add(((char1 * 72) + (char3 * 7) + (char5 * 59) + (char4 * 65) + (char7 * 22) + (char6 * 50) + (char15 * 68) + (char9 * 74) + (char16 * 41)) == 0x8E1C)
s.add(((char13 * 13) + (char1 * 13) + (char6 * 11) + (char9 * 50) + (char8 * 84) + (char12 * 52) + (char11 * 57) + (char15 * 60)) == 0x7733)
s.add(((char1 * 31) + (char3 * 93) + (char7 * 56) + (char5 * 57) + (char13 * 96) + (char10 * 37) + (char15 * 97)) == 0xB050)
s.add(((char1 * 18) + (char3 * 17) + (char5 * 12) + (char4 * 58) + (char7 * 14) + (char6 * 71) + (char12 * 46) + (char11 << 2) + (char10 << 3)) == 0x5A4C)
s.add(((char1 * 75) + (char4 * 62) + (char8 * 85) + (char12 * 44) + (char10 * 59) + (char15 * 12)) == 0x924E)
# s.add(((char5 * 36) + (char12 * 86)) == 0x1D7C)
# s.add(((char4 * 55) + (char7 * 36) + (char6 * 79) + (char9 * 94) + (char8 * 88) + (char11 * 34) + (char10 * 20) + (char12 * 65) + (char14 * 19)) == 0xC1F0)
# s.add(((char2 * 56) + (char3 * 36) + (char6 * 19) + (char5 << 3) + (char9 * 57) + (char8 * 71) + (char14 * 6) + (char12 * 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