solve.py

# -*- coding: utf-8 -*- 

mapping = {
    '♈': 0,
    '♉': 1,
    '♊': 2,
    '♋': 3,
    '♌': 4,
    '♍': 5,
    '♎': 6,
    '♏': 7,
    '♐': 8,
    '♑': 9,
    '♒': 10,
    '♓': 11,
    '🕙': 12,
}
var_mapping = 'abcdefghijklmnopqrstuvwxyz'
for r in range(64):
    eqns = []
    temp = 0
    output = 'xB^r_En}INc4v'
    target = [ord(ch) for ch in output]
    emoji_var = [
        var(var_mapping[mapping['♈']]),
        var(var_mapping[mapping['♉']]),
        var(var_mapping[mapping['♊']]),
        var(var_mapping[mapping['♋']]),
        var(var_mapping[mapping['♌']]),
        var(var_mapping[mapping['♍']]),
        var(var_mapping[mapping['♎']]),
        var(var_mapping[mapping['♏']]),
        var(var_mapping[mapping['♐']]),
        var(var_mapping[mapping['♑']]),
        var(var_mapping[mapping['♒']]),
        var(var_mapping[mapping['♓']]),
        var(var_mapping[mapping['🕙']]),
    ]
    if ((r & 1) == 0):
        emoji_var[mapping['♓']] -= emoji_var[mapping['♈']]

    if ((r & 2) == 0):
        emoji_var[mapping['♊']] = emoji_var[mapping['♏']] 

    emoji_var[mapping['♉']] -= emoji_var[mapping['♌']]
    emoji_var[mapping['♑']] += emoji_var[mapping['♎']]

    if ((r & 4) == 0):
        temp = emoji_var[mapping['♋']] 

    emoji_var[mapping['♊']] -= 8
    emoji_var[mapping['♋']] = emoji_var[mapping['🕙']]
    emoji_var[mapping['🕙']] = temp
    emoji_var[mapping['♉']] += emoji_var[mapping['♏']]
    emoji_var[mapping['♉']] -= emoji_var[mapping['♋']]
    emoji_var[mapping['♈']] += emoji_var[mapping['♓']]
    emoji_var[mapping['♊']] += 4
    emoji_var[mapping['♋']] += 2

    if ((r & 8) == 0):
        emoji_var[mapping['♌']] += emoji_var[mapping['♑']]

    emoji_var[mapping['♓']] += 1
    emoji_var[mapping['♒']] -= 8
    emoji_var[mapping['♏']] += emoji_var[mapping['♐']]
    emoji_var[mapping['♍']] -= emoji_var[mapping['♎']]

    if ((r & 16) == 0):
        emoji_var[mapping['♎']] += emoji_var[mapping['♐']]

    emoji_var[mapping['♐']] += 8
    emoji_var[mapping['♈']] -= emoji_var[mapping['♊']]
    emoji_var[mapping['♌']] -= emoji_var[mapping['♓']]
    emoji_var[mapping['♊']] += emoji_var[mapping['♊']]
    emoji_var[mapping['♏']] -= emoji_var[mapping['♓']]

    if ((r & 32) == 0):
        emoji_var[mapping['♑']] -= emoji_var[mapping['♉']]
    for idx in range(len(emoji_var)):
        eqns.append(emoji_var[idx] == target[idx])
    solutions = solve(eqns, a, b, c, d, e, f, g, h, i, j, k, l, m)
    flags = []
    if solutions:
        flag = []
        for solution in solutions:
            for sol in solution:
                num = sol.rhs()
                if num >=0 and num <= 255:
                    flag.append(chr(num))
                else:
                    flag.append('_')
        print(''.join(flag))