#!/usr/bin/env python2

from z3 import *

s = Solver()

res = []
res.append(([220, 14, 22, 235, 183, 129, 245, 145, 25, 113, 235, 35, 246, 240, 93, 107], 146))
res.append(([0, 152, 34, 136, 253, 131, 123, 165, 232, 231, 182, 18, 220, 171, 69, 75], 141))
res.append(([43, 219, 165, 225, 193, 11, 248, 28, 86, 5, 198, 56, 212, 218, 18, 154], 161))
res.append(([8, 79, 96, 233, 169, 183, 226, 188, 205, 20, 56, 119, 110, 52, 233, 146], 112))
res.append(([197, 241, 177, 75, 107, 76, 68, 208, 102, 110, 26, 83, 17, 26, 57, 63], 164))
res.append(([205, 148, 209, 248, 18, 142, 67, 53, 80, 174, 123, 194, 201, 223, 84, 47], 50))
res.append(([68, 120, 89, 96, 153, 29, 37, 218, 101, 117, 248, 65, 140, 43, 239, 106], 51))
res.append(([14, 218, 92, 251, 91, 29, 155, 16, 31, 1, 118, 214, 220, 174, 159, 70], 145))
res.append(([196, 24, 230, 117, 133, 191, 90, 84, 61, 82, 19, 216, 93, 95, 128, 161], 23))
res.append(([80, 23, 133, 17, 58, 134, 204, 222, 245, 66, 223, 96, 153, 76, 189, 4], 90))
res.append(([96, 116, 110, 226, 57, 112, 132, 185, 234, 30, 167, 5, 171, 222, 137, 54], 215))
res.append(([68, 71, 197, 155, 88, 188, 220, 8, 22, 42, 188, 64, 23, 27, 64, 204], 196))
res.append(([95, 144, 238, 1, 67, 18, 231, 29, 18, 243, 250, 119, 66, 56, 12, 110], 236))
res.append(([188, 219, 205, 136, 205, 232, 25, 192, 72, 94, 148, 141, 59, 0, 195, 98], 33))
res.append(([107, 196, 112, 47, 237, 172, 223, 90, 242, 207, 163, 117, 162, 128, 50, 139], 9))
res.append(([44, 185, 38, 75, 115, 112, 160, 161, 178, 46, 218, 239, 160, 254, 59, 137], 176))

flag = [0] * 16
for i in range(16):
	flag[i] = BitVec('flag%d' % (i,), 8)

for l, out in res:
	s.add(l[0] * flag[0] + l[1] * flag[1] + l[2] * flag[2] + l[3] * flag[3] + l[4] * flag[4] + l[5] * flag[5] + l[6] * flag[6] + l[7] * flag[7] + l[8] * flag[8] + l[9] * flag[9] + l[10] * flag[10] + l[11] * flag[11] + l[12] * flag[12] + l[13] * flag[13] + l[14] * flag[14] + l[15] * flag[15] == out)


def swap(l, i, j):
    tmp = l[i]
    l[i] = l[j]
    l[j] = tmp

print s
if s.check():
	l = []
	for i in range(16):
		v = int(str(s.model()[flag[i]]))
		l.append(v)
	
	swap(l, 14, 15)
	swap(l, 13, 15)
	swap(l, 12, 14)
	swap(l, 10,15)
	swap(l, 9,14)
	swap(l, 15,7)
	swap(l, 6, 14)
	swap(l, 5, 10)
	swap(l, 2,10)
	swap(l, 1,7)
	swap(l, 0, 13)
	print ''.join(map(chr, l))
else:
	print 'Failure'

402f452597b1cc491a7345834cf084cf7c9aa531
#!/usr/bin/env python2

from z3 import *

s = Solver()

res = []
res.append(([220, 14, 22, 235, 183, 129, 245, 145, 25, 113, 235, 35, 246, 240, 93, 107], 146))
res.append(([0, 152, 34, 136, 253, 131, 123, 165, 232, 231, 182, 18, 220, 171, 69, 75], 141))
res.append(([43, 219, 165, 225, 193, 11, 248, 28, 86, 5, 198, 56, 212, 218, 18, 154], 161))
res.append(([8, 79, 96, 233, 169, 183, 226, 188, 205, 20, 56, 119, 110, 52, 233, 146], 112))
res.append(([197, 241, 177, 75, 107, 76, 68, 208, 102, 110, 26, 83, 17, 26, 57, 63], 164))
res.append(([205, 148, 209, 248, 18, 142, 67, 53, 80, 174, 123, 194, 201, 223, 84, 47], 50))
res.append(([68, 120, 89, 96, 153, 29, 37, 218, 101, 117, 248, 65, 140, 43, 239, 106], 51))
res.append(([14, 218, 92, 251, 91, 29, 155, 16, 31, 1, 118, 214, 220, 174, 159, 70], 145))
res.append(([196, 24, 230, 117, 133, 191, 90, 84, 61, 82, 19, 216, 93, 95, 128, 161], 23))
res.append(([80, 23, 133, 17, 58, 134, 204, 222, 245, 66, 223, 96, 153, 76, 189, 4], 90))
res.append(([96, 116, 110, 226, 57, 112, 132, 185, 234, 30, 167, 5, 171, 222, 137, 54], 215))
res.append(([68, 71, 197, 155, 88, 188, 220, 8, 22, 42, 188, 64, 23, 27, 64, 204], 196))
res.append(([95, 144, 238, 1, 67, 18, 231, 29, 18, 243, 250, 119, 66, 56, 12, 110], 236))
res.append(([188, 219, 205, 136, 205, 232, 25, 192, 72, 94, 148, 141, 59, 0, 195, 98], 33))
res.append(([107, 196, 112, 47, 237, 172, 223, 90, 242, 207, 163, 117, 162, 128, 50, 139], 9))
res.append(([44, 185, 38, 75, 115, 112, 160, 161, 178, 46, 218, 239, 160, 254, 59, 137], 176))

flag = [0] * 16
for i in range(16):
	flag[i] = BitVec('flag%d' % (i,), 8)

for l, out in res:
	s.add(l[0] * flag[0] + l[1] * flag[1] + l[2] * flag[2] + l[3] * flag[3] + l[4] * flag[4] + l[5] * flag[5] + l[6] * flag[6] + l[7] * flag[7] + l[8] * flag[8] + l[9] * flag[9] + l[10] * flag[10] + l[11] * flag[11] + l[12] * flag[12] + l[13] * flag[13] + l[14] * flag[14] + l[15] * flag[15] == out)


def swap(l, i, j):
    tmp = l[i]
    l[i] = l[j]
    l[j] = tmp

print s
if s.check():
	l = []
	for i in range(16):
		v = int(str(s.model()[flag[i]]))
		l.append(v)
	
	swap(l, 14, 15)
	swap(l, 13, 15)
	swap(l, 12, 14)
	swap(l, 10,15)
	swap(l, 9,14)
	swap(l, 15,7)
	swap(l, 6, 14)
	swap(l, 5, 10)
	swap(l, 2,10)
	swap(l, 1,7)
	swap(l, 0, 13)
	print ''.join(map(chr, l))
else:
	print 'Failure'
