from z3 import *
import ipdb

# "String" of symbolic integer "bytes".
b = [Int('b_{}'.format(i)) for i in range(23)]

s = Solver()

# We know this part.
s.add(b[0] == ord('c'))
s.add(b[1] == ord('y'))
s.add(b[2] == ord('b'))
s.add(b[3] == ord('e'))
s.add(b[4] == ord('a'))
s.add(b[5] == ord('r'))
s.add(b[6] == ord('s'))

s.add(b[9] - b[3] - b[14] - b[16] == -114)
s.add(b[6] + b[17] * b[0] == 10213 )
s.add(b[14] * b[21] - b[10] * b[10] == -6190 )
s.add(b[20] + b[12] - b[16] == 112 )
s.add(b[6] + b[21] + b[11] == 261)
s.add(b[3] * b[1] + b[10] * b[13] == 20201)
s.add(b[8] + b[16] * b[7] == 6601)
s.add(b[22] * b[19] - b[9] == 6290)
s.add(b[12] * b[14] * b[21] == 184275)
s.add(b[4] - b[17] * b[15] - b[19] == -4952)
s.add(b[1] * b[1] - b[18] == 14592)
s.add(b[10] - (b[8] + b[22]) == -112)
s.add(b[1] - b[4] == 24)
s.add(b[21] * b[19] * b[5] == 366282)
s.add(b[8] + b[15] + b[11] * b[14] == 3866)
s.add(b[16] + b[1] == 174)
s.add(b[11] - b[6] * b[4] * b[15] == -546512)
s.add(b[16] * b[21] * b[4] - b[5] == 323769)
s.add(b[11] * b[3] - b[17] * b[4] == -1511)
s.add(b[9] + b[16] - b[5] * b[14] == -4992)
s.add(b[21] - b[6] * b[22] == -14312)
s.add(b[0] - b[19] * b[17] * b[6] == -598131)

# Attempt to determine if the constraints can be satisfied.
if s.check() == sat:
    model = s.model()

    # Split out the integer tag at the end of the byte name.
    def z3_byte_comparator(b):
       return int(str(b).split('_')[1])

    # This is gross, I know.
    ordered_results = sorted([byte for byte in model], key = z3_byte_comparator)
    result_characters = [chr(int(str(model[byte]))) for byte in ordered_results]
    print ''.join(result_characters)