from z3 import *
from IPython import embed

flags = []

for _ in xrange(53):
  flags.append(BitVec('a' + str(_),8))

so = Solver()
v0 = 34 * flags[0]+ 3 * flags[0] * flags[0]+ 120 * flags[0] * flags[0] * flags[0]+ 12
so.add(v0 == 39437721)

v0 = 96 * flags[1]+ 127 * flags[1] * flags[1]+ 41 * flags[1] * flags[1] * flags[1]+ 87
so.add(v0 == 16633575)
v0 = 26 * flags[2]+ 70 * flags[2] * flags[2]+ 12 * flags[2] * flags[2] * flags[2]+ 33
so.add(v0 == 7345865)
v0 = 88 * flags[3]+ 31 * flags[3] * flags[3]+ 71 * flags[3] * flags[3] * flags[3]+ 105
so.add(v0 == 132601485)

v0 = 67 * flags[4]+ 29 * flags[4] * flags[4]+ 69 * flags[4] * flags[4] * flags[4]+ 32
so.add(v0 == 122670437)
v0 = 23 * flags[5]+ 79 * flags[5] * flags[5]+ 117 * flags[5] * flags[5] * flags[5]+ 112
so.add(v0 == 160988851)
v0 = 101 * flags[6]+ 101 * flags[6] * flags[6]+ 13 * flags[6] * flags[6] * flags[6]+ 25
so.add(v0 == 22215400)
v0 = 120 * flags[7]+ 25 * flags[7] * flags[7]+ 37 * flags[7] * flags[7] * flags[7]+ 106
so.add(v0 == 31960006)
v0 = 101 * flags[8]+ 92 * flags[8] * flags[8]+ 40 * flags[8] * flags[8] * flags[8]+ 35
so.add(v0 == 62063350)
v0 = 11 * flags[9]+ 31 * flags[9] * flags[9]+ 67 * flags[9] * flags[9] * flags[9]+ 99
so.add(v0 == 75702427)
v0 = 16 * flags[10]+ 67 * flags[10] * flags[10]+ 74 * flags[10] * flags[10] * flags[10]+ 17
so.add(v0 == 102031994)
v0 = 21 * flags[11]+ 93 * flags[11] * flags[11]+ 67 * flags[11] * flags[11] * flags[11]+ 2
so.add(v0 == 108583607)
v0 = 62 * flags[12]+ 109 * flags[12] * flags[12]+ 107 * flags[12] * flags[12] * flags[12]+ 61
so.add(v0 == 136067317)
v0 = 104 * flags[13]+ 47 * flags[13] * flags[13]+ 117 * flags[13] * flags[13] * flags[13]+ 79
so.add(v0 == 117480479)

v5 = 68 * flags[14]+ 124 * flags[14] * flags[14]+ 88 * flags[14] * flags[14] * flags[14]+ 115
so.add( v5 == 76574675 )
v0 = 86 * flags[15]+ 50 * flags[15] * flags[15]+ (flags[15] * flags[15] * flags[15] * (2**6))+ 93
so.add(v0 == 70473929)
v0 = 100 * flags[16]+ 70 * flags[16] * flags[16]+ 118 * flags[16] * flags[16] * flags[16]+ 84
so.add(v0 == 162254112)
v0 = 39 * flags[17]+ 76 * flags[17] * flags[17]+ 50 * flags[17] * flags[17] * flags[17]+ 23
so.add(v0 == 43558378)
v0 = 101 * flags[18]+ 74 * flags[18] * flags[18]+ 67 * flags[18] * flags[18] * flags[18]+ 45
so.add(v0 == 71881179)
v0 = 31 * flags[19]+ 115 * flags[19] * flags[19]+ 101 * flags[19] * flags[19] * flags[19]+ 7
so.add(v0 == 139551094)
v0 = 20 * flags[20]+ 11 * flags[20] * flags[20]+ 69 * flags[20] * flags[20] * flags[20]+ 119
so.add(v0 == 102371891)
v0 = 83 * flags[21]+ 122 * flags[21] * flags[21]+ 27 * flags[21] * flags[21] * flags[21]+ 111
so.add(v0 == 24258171)
v0 = 34 * flags[22]+ 51 * flags[22] * flags[22]+ 66 * flags[22] * flags[22] * flags[22]+ 10
so.add(v0 == 88466850)
v0 = 16 * flags[23]+ 58 * flags[23] * flags[23]+ 115 * flags[23] * flags[23] * flags[23]+ 35
so.add(v0 == 105504704)
v0 = 50 * flags[24]+ 125 * flags[24] * flags[24]+ 51 * flags[24] * flags[24] * flags[24]+ 18
so.add(v0 == 79223518)
v0 = 26 * flags[25]+ 127 * flags[25] * flags[25]+ 10 * flags[25] * flags[25] * flags[25]+ 3
so.add(v0 == 10950294)
v0 = 122 * flags[26]+ 83 * flags[26] * flags[26]+ 92 * flags[26] * flags[26] * flags[26]+ 60
so.add(v0 == 126858297)
v0 = 56 * flags[27]+ 36 * flags[27] * flags[27]+ 110 * flags[27] * flags[27] * flags[27]+ 69
so.add(v0 == 146851829)
v0 = 110 * flags[28]+ 23 * flags[28] * flags[28]+ 32 * flags[28] * flags[28] * flags[28]+ 127
so.add(v0 == 32241127)
v0 = 58 * flags[29]+ 123 * flags[29] * flags[29]+ 22 * flags[29] * flags[29] * flags[29]+ 44
so.add(v0 == 26829959)
v0 = 122 * flags[30]+ 60 * flags[30] * flags[30]+ 92 * flags[30] * flags[30] * flags[30]+ 65
so.add(v0 == 123191485)
v0 = 88 * flags[31]+ 36 * flags[31] * flags[31]+ 38 * flags[31] * flags[31] * flags[31]+ 38
so.add(v0 == 52423340)
v0 = 80 * flags[32]+ 72 * flags[32] * flags[32]+ 127 * flags[32] * flags[32] * flags[32]+ 44
so.add(v0 == 109544069)
v0 = 13 * flags[33]+ 23 * flags[33] * flags[33]+ 94 * flags[33] * flags[33] * flags[33]+ 28
so.add(v0 == 158732224)
v0 = 80 * flags[34]+ 24 * flags[34] * flags[34]+ 46 * flags[34] * flags[34] * flags[34]+ 79
so.add(v0 == 63215689)
v0 = 100 * flags[35]+ 101 * flags[35] * flags[35]+ 75 * flags[35] * flags[35] * flags[35]+ 104
so.add(v0 == 112439900)
v0 = 96 * flags[36]+ 8 * flags[36] * flags[36]+ 4 * flags[36] * flags[36] * flags[36]+ 49
so.add(v0 == 5142577)
v0 = 14 * flags[37]+ 89 * flags[37] * flags[37]+ 113 * flags[37] * flags[37] * flags[37]+ 56
so.add(v0 == 113891456)
v0 = 9 * flags[38]+ 82 * flags[38] * flags[38]+ 18 * flags[38] * flags[38] * flags[38]+ 74
so.add(v0 == 16173729)
v0 = 56 * flags[39]+ 14 * flags[39] * flags[39]+ 117 * flags[39] * flags[39] * flags[39]+ 70
so.add(v0 == 113667811)
v0 = 53 * flags[40]+ 49 * flags[40] * flags[40]+ 89 * flags[40] * flags[40] * flags[40]+ 94
so.add(v0 == 100648486)
v4 = 6 * flags[41]+ 23 * flags[41] * flags[41]+ 38 * flags[41] * flags[41] * flags[41]+ 22
so.add(v4 == 34898585)
v0 = 29 * flags[42]+ 72 * flags[42] * flags[42]+ 21 * flags[42] * flags[42] * flags[42]+ 43
so.add(v0 == 28054245)
v0 = 16 * flags[43]+ 90 * flags[43] * flags[43]+ 68 * flags[43] * flags[43] * flags[43]+ 105
so.add(v0 == 96665961)
v0 = 73 * flags[44]+ 116 * flags[44] * flags[44]+ 102 * flags[44] * flags[44] * flags[44]+ 51
so.add(v0 == 119364366)
v0 = 101 * flags[45]+ 15 * flags[45] * flags[45]+ 13 * flags[45] * flags[45] * flags[45]+ 34
so.add(v0 == 17975263)
v0 = 59 * flags[46]+ 72 * flags[46] * flags[46]+ 52 * flags[46] * flags[46] * flags[46]+ 83
so.add(v0 == 70089773)
v0 = 50 * flags[47]+ 22 * flags[47] * flags[47]+ 55 * flags[47] * flags[47] * flags[47]+ 41
so.add(v0 == 83944866)
v0 = 77 * flags[48]+ 42 * flags[48] * flags[48]+ 119 * flags[48] * flags[48] * flags[48]+ 110
so.add(v0 == 134321206)
v0 = 91 * flags[49]+ 38 * flags[49] * flags[49]+ 126 * flags[49] * flags[49] * flags[49]+ 64
so.add(v0 == 146289319)
v0 = 113 * flags[50]+ 113 * flags[50] * flags[50]+ 119 * flags[50] * flags[50] * flags[50]+ 22
so.add(v0 == 168616582)
v0 = 24 * flags[51]+ 88 * flags[51] * flags[51]+ 98 * flags[51] * flags[51] * flags[51]+ 30
so.add(v0 == 192784280)
v0 = 96 * flags[52]+ 12 * flags[52] * flags[52]+ 74 * flags[52] * flags[52] * flags[52]+ 104
so.add(v0 == 104)

print(so.check())
m = so.model()
print(m<