from z3 import *
import string

solver = Solver()
f = [BitVec(f"f_{i}", 8) for i in range(16)]
length = Int("length")
solver.add(length >= 8, length <= 16)

ascii_letters = string.ascii_letters
solver.add(And([Or(And(f[i] >= ord('a'), f[i] <= ord('z')), And(f[i] >= ord('A'), f[i] <= ord('Z'))) for i in range(16)]))

num = BitVecVal(0, 32)
for i in range(16):
    extended_char = ZeroExt(24, f[i])
    num = If(i < length, (num << 3) ^ (extended_char * 17), num)
solver.add((num & 65535) == 23130)
key = [ord(c) for c in "CrazyCrackMe"]
reversed_f = [BitVec(f"rev_f_{i}", 8) for i in range(16)]
for i in range(16):
    for j in range(16):
        solver.add(If(And(i < length, j == length - i - 1), reversed_f[i] == f[j], True))
    solver.add(If(i >= length, reversed_f[i] == 0, True))

def contains_subarray(arr, subarray):
    return Or([And([arr[j + k] == subarray[k] for k in range(len(subarray))]) for j in range(16 - len(subarray) + 1)])

solver.add(contains_subarray(reversed_f, key))
solutions = []
for _ in range(10):
    if solver.check() == sat:
        model = solver.model()
        actual_length = model[length].as_long()
        result = [chr(model[f[i]].as_long()) for i in range(actual_length)]
        solutions.append("".join(result))
        solver.add(Or([f[i] != model[f[i]] for i in range(actual_length)]))
    else:
        break

if solutions:
    for idx, solution in enumerate(solutions, 1):
        print(f"{idx}: {solution}")
else:
    exit()