DASCTF2022十一月赛Re赛后复现

0x00 babytea

看名字猜测魔改的TEA加密算法

第一步老规矩查壳

32位无壳PE文件

IDA反编译一下得到主函数伪代码

int __cdecl main(int argc, const char **argv, const char **envp)
{
  unsigned int i; // [esp+4h] [ebp-28h]
  char Buf1[32]; // [esp+8h] [ebp-24h] BYREF

  memset(Buf1, 0, sizeof(Buf1));
  sub_401350("please input: \n");
  sub_401390("%32s", Buf1);
  for ( i = 0; i < 4; ++i )
    __scrt_is_nonwritable_in_current_image(dword_41F014, &Buf1[8 * i], &unk_41F004);
  if ( !memcmp(Buf1, &unk_41F018, 0x20u) )
    sub_401350("Great\nYour input is right!!!\n");
  else
    sub_401350("Sorry\nYour input is wrong...\n");
  return 0;
}

简单分析一下

用户先输入一个长度为32的字符串Buf1

然后将Buf1进行四轮加密

最后将加密后的字符串与unk_41F018进行比较

定位到进行比较的字符串

.data:0041F018 unk_41F018      db  30h ; 0             ; DATA XREF: _main+82↑o
.data:0041F019                 db 0B5h
.data:0041F01A                 db  27h ; '
.data:0041F01B                 db  5Eh ; ^
.data:0041F01C                 db 0F3h
.data:0041F01D                 db 0F7h
.data:0041F01E                 db 0BEh
.data:0041F01F                 db 0BDh
.data:0041F020                 db  8Fh
.data:0041F021                 db  6Ah ; j
.data:0041F022                 db  51h ; Q
.data:0041F023                 db 0E3h
.data:0041F024                 db 0FEh
.data:0041F025                 db  6Ch ; l
.data:0041F026                 db  83h
.data:0041F027                 db  5Dh ; ]
.data:0041F028                 db    9
.data:0041F029                 db 0FAh
.data:0041F02A                 db  3Dh ; =
.data:0041F02B                 db 0D8h
.data:0041F02C                 db  7Ah ; z
.data:0041F02D                 db  73h ; s
.data:0041F02E                 db 0FCh
.data:0041F02F                 db  8Eh
.data:0041F030                 db 0A3h
.data:0041F031                 db  53h ; S
.data:0041F032                 db 0A8h
.data:0041F033                 db  55h ; U
.data:0041F034                 db 0C5h
.data:0041F035                 db  4Eh ; N
.data:0041F036                 db  56h ; V
.data:0041F037                 db  7Ah ; z

提取值,得到加密后的字符串

[0x30,0x0B5,0x27,0x5E,0x0F3,0x0F7,0x0BE,0x0BD,0x8F,0x6A,0x51,0x0E3,0x0FE,0x6C,0x83,0x5D,0x9,0x0FA,0x3D,0x0D8,0x7A,0x73,0x0FC,0x8E,0x0A3,0x53,0x0A8,0x55,0x0C5,0x4E,0x56,0x7A]

再定位到加密函数 __scrt_is_nonwritable_in_current_image

int __cdecl __scrt_is_nonwritable_in_current_image(unsigned int a1, unsigned int *a2, _DWORD *a3)
{
  int result; // eax
  unsigned int i; // [esp+20h] [ebp-28h]
  int v5; // [esp+24h] [ebp-24h]
  unsigned int v6; // [esp+28h] [ebp-20h]
  unsigned int v7; // [esp+2Ch] [ebp-1Ch]

  v7 = *a2;
  v6 = a2[1];
  v5 = 0;
  for ( i = 0; i < a1; ++i )
  {
    v5 += dword_41F000;
    v7 += (a3[1] + (v6 >> 5)) ^ (v5 + v6) ^ (*a3 + 16 * v6);
    v6 += (a3[3] + (v7 >> 5)) ^ (v5 + v7) ^ (a3[2] + 16 * v7);
  }
  *a2 = v7;
  result = 4;
  a2[1] = v6;
  return result;
}

简单分析一下，是一个魔改过的TEA加密算法

dword_41F000即为delta值，查看一下

所以delta = 0x9E3779B1

分析一下加密函数的形参

a1是dword_41F014,值为32

a2是用户输入的字符串Buf1，每八位一组分成四组，一次进行加密

a3是dword_41F004，是一个数组，对应TEA算法中的key数组

寻得大佬解密脚本如下

#include <stdio.h>  
#include <stdint.h>  
unsigned int dword_69F038 = 0x1234567;
unsigned int dword_69F03C = 0x89ABCDEF;
//解密函数  
void decrypt (uint32_t* v, uint32_t* k,uint32_t Xor1,uint32_t Xor2) {  
    uint32_t v0=v[0], v1=v[1], sum=0, i;  /* set up */  
    uint32_t delta=0x9E3779B1;                     /* a key schedule constant */  
    uint32_t k0=k[0], k1=k[1], k2=k[2], k3=k[3];   /* cache key */  
    dword_69F038 = v0;
    dword_69F03C = v1;
  uint32_t summ[0x20] = {0};
  for(i = 0;i<=31;i++){
    sum += delta;  
        if((sum >> 0x1f) == 0){
          sum ^= 0x1234567;
    }
    summ[i] = sum;
  }


    for (i=0; i<32; i++) {                         /* basic cycle start */  
        v1 -= ((v0<<4) + k2) ^ (v0 + summ[31-i]) ^ ((v0>>5) + k3);  
        v0 -= ((v1<<4) + k0) ^ (v1 + summ[31-i]) ^ ((v1>>5) + k1);  
    }                
  v0 ^= Xor1;
    v1 ^= Xor2;                         
    v[0]=v0; v[1]=v1;  
}  

void hexdump(unsigned int * t1,unsigned int *t2){
  for(int i = 0;i<4;i++){
    printf("%c",((unsigned char *)t1)[i]);

  }
  for(int i = 0;i<4;i++){
    printf("%c",((unsigned char *)t2)[i]);

  }
}
void Tea()
{
  unsigned int cip[8] = {
      0x5E27B530, 0xBDBEF7F3, 0xE3516A8F, 0x5D836CFE, 0xD83DFA09, 0x8EFC737A, 0x55A853A3, 0x7A564EC5
  };
    unsigned int key[4] = {
      0x67452301, 0xEFCDAB89, 0x98BADCFE, 0x10325476
  };
  unsigned int Xor0[8] = {0x1234567,0x5E27B530,0xE3516A8F,0xD83DFA09};
  unsigned int Xor1[8] = {0x89ABCDEF,0xBDBEF7F3,0x5D836CFE,0x8EFC737A};
  for(int i = 0;i<=3;i++){
    uint32_t v[2];
    v[0] = cip[i * 2];
    v[1] = cip[i*2 +1];

      decrypt(v, key,Xor0[i],Xor1[i]);  
//      printf("%x %x\n",v[0],v[1]);  
    hexdump(&v[0],&v[1]);
  }


}

int main(){
  Tea();
  return 0;
}

0x01 baby smc （⭐）

smc自解密代码 第一次做

查壳

32位无壳PE文件

IDA反编译一下

主函数伪代码如下

int __cdecl main(int argc, const char **argv, const char **envp)
{
  char v4[36]; // [esp+0h] [ebp-28h] BYREF

  memset(v4, 0, 0x22u);
  sub_404830("please input: \n", v4[0]);
  sub_404870("%34s", v4);
  sub_404630(v4[0], v4[33]);
  ((void (__cdecl *)(char *, int))loc_401850)(&v4[1], 32);
  if ( (unsigned __int8)sub_4018C0(&v4[1], 16) && (unsigned __int8)sub_402F30(&v4[17]) )
    sub_404830("Great\nYour input is right!!!\n", v4[0]);
  else
    sub_404830("Sorry\nYour input is wrong...\n", v4[0]);
  return 0;
}

定位到SMC自解密代码

int __cdecl sub_404630(char a1, char a2)
{
  DWORD flOldProtect; // [esp+0h] [ebp-Ch] BYREF
  SIZE_T dwSize; // [esp+4h] [ebp-8h]
  SIZE_T i; // [esp+8h] [ebp-4h]

  dwSize = 256;
  VirtualProtect(&loc_401850, 0x100u, 0x40u, &flOldProtect);
  for ( i = 0; i < dwSize; ++i )
    *((_BYTE *)&loc_401850 + i) ^= a1;
  VirtualProtect(&loc_401850, dwSize, flOldProtect, &flOldProtect);
  return sub_4045B0(a2);
}

没看懂，根据大佬wp所说需要我们输入正确的字符串才能解密成功

爆破所有可见字符，利用capstone进行筛选

脚本:

from struct import *
from capstone import *
code = "74AACDA2CD29E664DD2121212199202121214AE921AA7429E7252B23AA64DDA2E120A864DD9820212121E0C021AA7429E7252B22AA64DDA2E120A864DDE664D925212121CA28AA6CD9A2E020A86CD9A25CD93F5610A25CDD2B5323CA08AA74D973C97BDEDEDEA2E5252E97E1A4E15535AA6C29226CDDAB74D9A930AA64DDA2E120A864DDCAE1AAC47CE2EDEDEDEDEDED5789EE81EE16A3FE3C400231C78B47FE680868028F47F252EA7139020281C60E8F4FF253EA45FDFDFD81C606C547EE02020202E90B8957EE81C0038B57EE817FEE08711C89470E52894F0A538957EE0DB44617F2890E87823C4002FDD381C60AE9D1894FFE31CFEAEC2D020289E75FC1"
xcode = bytes.fromhex(code)
print(hex(len(xcode)))
for XOr in range(28,126):
    x32code = b""
    for j in range(len(xcode)):
        x32code += pack("B",xcode[j] ^ XOr)
    if XOr == 0x21:
        for i in range(len(x32code)):
            print(hex(x32code[i]),end = ",")
    CP = Cs(CS_ARCH_X86, CS_MODE_32)

    for p in CP.disasm(x32code, 0x04017C0):
        # if XOr == 0x21:
            if p.address > 0x04017C0 + 0x90 - 0x10:
                print(f"{hex(XOr)} => ")
                print()
                for q in CP.disasm(x32code, 0x04017C0):
                    print("0x%x:\t%s\t%s" %(q.address, q.mnemonic, q.op_str)) 
                break


from struct import *
from capstone import *
code = "76A8CFA0CF3782DF1D612310E6AA66DF49294923AE66D373CB50182323A0E72FAE6ED372CB64DCDCDCA0E727E466CF23232323C82AA876CFA0E122AA76CFA05ECF29503DA8662F73A86E2B72A876CF2C956736D3A82FA6A31D6123DCF2A0E72BC8F0A86EDF10EECBCD0C2323A8C67EE076A8CF759B2723232348EB2F992223232348E120A8762B2C95272148F3249B2223232348E326A8562B2C9527254AE39C23232320F39B2223232348E328A8562B2C9527254AE39623232320F39B22232323F2C3A8562B2C95272548E33120F39B2223232348E325A8562B2C95272548E35F20F39B22232323E2C323A8562B2C95272548E30A20F39B2223232348E323A8"
xcode = bytes.fromhex(code)
print(hex(len(xcode)))
for XOr in range(20,126):
    x32code = b""
    for j in range(len(xcode)):
        x32code += pack("B",xcode[j] ^ XOr)
    if XOr == 0x23:
        for i in range(len(x32code)):
            print(hex(x32code[i]),end = ",")
    CP = Cs(CS_ARCH_X86, CS_MODE_32)

    for p in CP.disasm(x32code, 0x0401850):
        # if XOr == 0x21:
            if p.address > 0x0401850 + 0x100 - 0x10:
                print(f"{hex(XOr)} => ")
                print()
                for q in CP.disasm(x32code, 0x0401850):
                    print("0x%x:\t%s\t%s" %(q.address, q.mnemonic, q.op_str)) 
                break

爆破出第一段自解密的异或值为0x23，第二段为0x21

patch,恢复原来的指令

import idc
data = [0x55,0x8b,0xec,0x83,0xec,0x8,0xc7,0x45,0xfc,0x0,0x0,0x0,0x0,0xb8,0x1,0x0,0x0,0x0,0x6b,0xc8,0x0,0x8b,0x55,0x8,0xc6,0x4,0xa,0x2,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xb9,0x1,0x0,0x0,0x0,0xc1,0xe1,0x0,0x8b,0x55,0x8,0xc6,0x4,0xa,0x3,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xc7,0x45,0xf8,0x4,0x0,0x0,0x0,0xeb,0x9,0x8b,0x4d,0xf8,0x83,0xc1,0x1,0x89,0x4d,0xf8,0x83,0x7d,0xf8,0x1e,0x77,0x31,0x83,0x7d,0xfc,0xa,0x72,0x2,0xeb,0x29,0x8b,0x55,0xf8,0x52,0xe8,0x5a,0xff,0xff,0xff,0x83,0xc4,0x4,0xf,0xb6,0xc0,0x85,0xc0,0x74,0x14,0x8b,0x4d,0x8,0x3,0x4d,0xfc,0x8a,0x55,0xf8,0x88,0x11,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xeb,0xc0,0x8b,0xe5,0x5d,0xc3,0xcc,0xcc,0xcc,0xcc,0xcc,0xcc,0x76,0xa8,0xcf,0xa0,0xcf,0x37,0x82,0xdf,0x1d,0x61,0x23,0x10,0xe6,0xaa,0x66,0xdf,0x49,0x29,0x49,0x23,0xae,0x66,0xd3,0x73,0xcb,0x50,0x18,0x23,0x23,0xa0,0xe7,0x2f,0xae,0x6e,0xd3,0x72,0xcb,0x64,0xdc,0xdc,0xdc,0xa0,0xe7,0x27,0xe4,0x66,0xcf,0x23,0x23,0x23,0x23,0xc8,0x2a,0xa8,0x76,0xcf,0xa0,0xe1,0x22,0xaa,0x76,0xcf,0xa0,0x5e,0xcf,0x29,0x50,0x3d,0xa8,0x66,0x2f,0x73,0xa8,0x6e,0x2b,0x72,0xa8,0x76,0xcf,0x2c,0x95,0x67,0x36,0xd3,0xa8,0x2f,0xa6,0xa3,0x1d,0x61,0x23,0xdc,0xf2,0xa0,0xe7,0x2b,0xc8,0xf0,0xa8,0x6e,0xdf,0x10,0xee,0xcb,0xcd,0xc,0x23,0x23,0xa8,0xc6,0x7e,0xe0]
def Patch(begin,end,Xor):
    for i in range(begin,end):  
        idc.patch_byte(i,Xor[i-begin])

beginn = 0x04017C0
endd = beginn + len(data)
Patch(beginn,endd,data)

0x23
import idc
data = [0x55,0x8b,0xec,0x83,0xec,0x8,0xc7,0x45,0xfc,0x0,0x0,0x0,0x0,0xb8,0x1,0x0,0x0,0x0,0x6b,0xc8,0x0,0x8b,0x55,0x8,0xc6,0x4,0xa,0x2,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xb9,0x1,0x0,0x0,0x0,0xc1,0xe1,0x0,0x8b,0x55,0x8,0xc6,0x4,0xa,0x3,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xc7,0x45,0xf8,0x4,0x0,0x0,0x0,0xeb,0x9,0x8b,0x4d,0xf8,0x83,0xc1,0x1,0x89,0x4d,0xf8,0x83,0x7d,0xf8,0x1e,0x77,0x31,0x83,0x7d,0xfc,0xa,0x72,0x2,0xeb,0x29,0x8b,0x55,0xf8,0x52,0xe8,0x5a,0xff,0xff,0xff,0x83,0xc4,0x4,0xf,0xb6,0xc0,0x85,0xc0,0x74,0x14,0x8b,0x4d,0x8,0x3,0x4d,0xfc,0x8a,0x55,0xf8,0x88,0x11,0x8b,0x45,0xfc,0x83,0xc0,0x1,0x89,0x45,0xfc,0xeb,0xc0,0x8b,0xe5,0x5d,0xc3,0xcc,0xcc,0xcc,0xcc,0xcc,0xcc,0x76,0xa8,0xcf,0xa0,0xcf,0x37,0x82,0xdf,0x1d,0x61,0x23,0x10,0xe6,0xaa,0x66,0xdf,0x49,0x29,0x49,0x23,0xae,0x66,0xd3,0x73,0xcb,0x50,0x18,0x23,0x23,0xa0,0xe7,0x2f,0xae,0x6e,0xd3,0x72,0xcb,0x64,0xdc,0xdc,0xdc,0xa0,0xe7,0x27,0xe4,0x66,0xcf,0x23,0x23,0x23,0x23,0xc8,0x2a,0xa8,0x76,0xcf,0xa0,0xe1,0x22,0xaa,0x76,0xcf,0xa0,0x5e,0xcf,0x29,0x50,0x3d,0xa8,0x66,0x2f,0x73,0xa8,0x6e,0x2b,0x72,0xa8,0x76,0xcf,0x2c,0x95,0x67,0x36,0xd3,0xa8,0x2f,0xa6,0xa3,0x1d,0x61,0x23,0xdc,0xf2,0xa0,0xe7,0x2b,0xc8,0xf0,0xa8,0x6e,0xdf,0x10,0xee,0xcb,0xcd,0xc,0x23,0x23,0xa8,0xc6,0x7e,0xe0]
def Patch(begin,end,Xor):
    for i in range(begin,end):  
        idc.patch_byte(i,Xor[i-begin])

最后利用z3求解器求解

exp:

from z3 import *
input = [z3.BitVec(f"input[{i}]",8) for i in range(16)]
dword_422000 = [0x0002A81A, 0x00028D44, 0x00022653, 0x0002E993, 0x000249B5, 0x00024265, 0x0003253D, 0x0002D77B, 0x000282C8, 0x00022892, 0x0002BD54, 0x0002482E, 0x00024C1F, 0x00028127, 0x0001E62E, 0x0001F009]
Sol = Solver()
Sol.add(dword_422000[12] == (199 * input[9]                     \
                           + 98 * input[7]                  \
                           + 192 * input[8]                 \
                           + 23 * input[12]                 \
                           + 79 * input[14]                 \
                           + 77 * input[10]                 \
                           + 185 * input[13]                \
                           + 135 * input[15]                \
                           + 119 * input[4]                 \
                           + 54 * input[0]                    \
                           + 41 * input[1]                  \
                           + 124 * input[6]                 \
                           + 18 * input[2]                  \
                           + 181 * input[11]                \
                           + 191 * input[5]                 \
                           + 7 * input[3]) & 0xffffffff                   )

Sol.add(dword_422000[3] == (210 * input[11]                \
                          + 26 * input[15]                  \
                          + 169 * input[0]                    \
                          + 177 * input[13]                 \
                          + input[6]                        \
                          + 205 * input[8]                  \
                          + 223 * input[10]                 \
                          + 32 * input[5]                   \
                          + 225 * input[3]                  \
                          + 61 * input[14]                  \
                          + 72 * input[1]                   \
                          + 186 * input[9]                  \
                          + 253 * input[12]                 \
                          + 205 * input[2]                  \
                          + 49 * input[4]                   \
                          + 232 * input[7] ) & 0xffffffff                 )

Sol.add(dword_422000[13] == (192 * input[3]                \
                           + 22 * input[10]                 \
                           + 175 * input[1]                 \
                           + 184 * input[7]                 \
                           + 116 * input[15]                \
                           + 70 * input[13]                 \
                           + 153 * input[14]                \
                           + 119 * input[0]                   \
                           + 217 * input[6]                 \
                           + 123 * input[5]                 \
                           + 17 * input[2]                  \
                           + 244 * input[12]                \
                           + 116 * input[8]                 \
                           + 46 * input[4]                  \
                           + 19 * input[9]                  \
                           + 130 * input[11])& 0xffffffff                 )

Sol.add (dword_422000[7] == (41 * input[12]                 \
                          + 71 * input[7]                   \
                          + 185 * input[1]                  \
                          + 69 * input[11]                  \
                          + 142 * input[8]                  \
                          + 221 * input[5]                  \
                          + 24 * input[3]                   \
                          + 208 * input[6]                  \
                          + 41 * input[9]                   \
                          + 159 * input[2]                  \
                          + 231 * input[14]                 \
                          + 235 * input[13]                 \
                          + 225 * input[0]                    \
                          + (input[4] << 6)                 \
                          + 162 * input[10]                 \
                          + 134 * input[15] )& 0xffffffff                 )
Sol.add (dword_422000[11] == (36 * input[12]                \
                           + 220 * input[4]                 \
                           + 110 * input[13]                \
                           + 45 * input[7]                  \
                           + 123 * input[9]                 \
                           + 133 * input[1]                 \
                           + 101 * input[5]                 \
                           + 137 * input[10]                \
                           + 102 * input[0]                   \
                           + 227 * input[14]                \
                           + 94 * input[15]                 \
                           + 18 * input[2]                  \
                           + 22 * input[6]                  \
                           + 189 * input[11]                \
                           + 218 * input[8])& 0xffffffff                  )
Sol.add (dword_422000[15] == (86 * input[11]                \
                           + 31 * input[9]                  \
                           + 229 * input[6]                 \
                           + 27 * input[3]                  \
                           + 6 * input[12]                  \
                           + 13 * input[10]                 \
                           + 158 * input[1]                 \
                           + 89 * input[7]                  \
                           + 35 * input[15]                 \
                           + 126 * input[8]                 \
                           + 165 * input[13]                \
                           + 220 * input[0]                   \
                           + 138 * input[5]                 \
                           + 100 * input[4]                 \
                           + 84 * input[14]                 \
                           + 175 * input[2]) & 0xffffffff                  )
Sol.add(dword_422000[8] == ( 7 * input[1]                   \
                          + 28 * input[8]                   \
                          + 131 * input[10]                 \
                          + 6 * input[6]                    \
                          + 254 * input[0]                    \
                          + 130 * input[13]                 \
                          + 124 * input[3]                  \
                          + 55 * input[12]                  \
                          + 157 * input[14]                 \
                          + 175 * input[5]                  \
                          + 140 * input[4]                  \
                          + 241 * input[9]                  \
                          + 11 * input[11]                  \
                          + 211 * input[2]                  \
                          + 121 * input[7]                  \
                          + 200 * input[15]  )  & 0xffffffff              )
Sol.add(dword_422000[6] == (195 * input[14]                \
                          + 197 * input[13]                 \
                          + 218 * input[7]                  \
                          + 83 * input[1]                   \
                          + 98 * input[2]                   \
                          + 70 * input[10]                  \
                          + 229 * input[15]                 \
                          + 148 * input[11]                 \
                          + 195 * input[0]                    \
                          + 94 * input[6]                   \
                          + 211 * input[12]                 \
                          + 220 * input[9]                  \
                          + 81 * input[5]                   \
                          + 253 * input[8]                  \
                          + 78 * input[4]                   \
                          + 4 * input[3]   ) & 0xffffffff                 ) 
Sol.add(dword_422000[14] == (3 * input[4]                  \
                           + 136 * input[7]                 \
                           + 156 * input[3]                 \
                           + 189 * input[1]                 \
                           + 244 * input[12]                \
                           + 157 * input[15]                \
                           + 83 * input[9]                  \
                           + 6 * input[0]                     \
                           + 113 * input[6]                 \
                           + 63 * input[14]                 \
                           + 35 * input[2]                  \
                           + 22 * input[8]                  \
                           + 26 * input[10]                 \
                           + 62 * input[11]                 \
                           + 98 * input[5]                  \
                           + 110 * input[13] )& 0xffffffff                )
Sol.add(dword_422000[4] == (96 * input[4]                  \
                          + 248 * input[8]                  \
                          + 191 * input[9]                  \
                          + 194 * input[2]                  \
                          + 154 * input[1]                  \
                          + 31 * input[6]                   \
                          + 157 * input[7]                  \
                          + 248 * input[13]                 \
                          + 81 * input[15]                  \
                          + 56 * input[10]                  \
                          + 52 * input[0]                     \
                          + 94 * input[12]                  \
                          + 212 * input[5]                  \
                          + 83 * input[3]                   \
                          + 83 * input[14]                  \
                          + 158 * input[11]  )& 0xffffffff                )
Sol.add(dword_422000[1] == (67 * input[4]                  \
                          + 220 * input[2]                  \
                          + 123 * input[11]                 \
                          + 168 * input[5]                  \
                          + 23 * input[12]                  \
                          + 148 * input[7]                  \
                          + 127 * input[10]                 \
                          + 194 * input[1]                  \
                          + 132 * input[8]                  \
                          + 44 * input[0]                     \
                          + 60 * input[13]                  \
                          + 98 * input[15]                  \
                          + 38 * input[14]                  \
                          + 245 * input[9]                  \
                          + 159 * input[6]                  \
                          + 146 * input[3] )& 0xffffffff                  )
Sol.add(dword_422000[5] == (132 * input[3]                 \
                          + 10 * input[7]                   \
                          + 95 * input[0]                     \
                          + 83 * input[10]                  \
                          + 99 * input[1]                   \
                          + 77 * input[12]                  \
                          + 195 * input[2]                  \
                          + 47 * input[6]                   \
                          + 38 * input[13]                  \
                          + 178 * input[8]                  \
                          + 74 * input[4]                   \
                          + 86 * input[11]                  \
                          + 208 * input[9]                  \
                          + 240 * input[14]                 \
                          + 120 * input[5]                  \
                          + 43 * input[15]   )& 0xffffffff                )
Sol.add(dword_422000[9] == (172 * input[1]                 \
                          + 110 * input[2]                  \
                          + 92 * input[7]                   \
                          + 126 * input[15]                 \
                          + 91 * input[0]                     \
                          + 77 * input[6]                   \
                          + 207 * input[5]                  \
                          + 249 * input[11]                 \
                          + 240 * input[12]                 \
                          + 129 * input[10]                 \
                          + 6 * input[13]                   \
                          + 100 * input[3]                  \
                          + input[14]                       \
                          + 76 * input[9]                   \
                          + 127 * input[4]                  \
                          + 4 * input[8]  )& 0xffffffff                   )
Sol.add(dword_422000[10] == (46 * input[15]                \
                           + 37 * input[0]                    \
                           + 3 * input[3]                   \
                           + 72 * input[6]                  \
                           + 116 * input[7]                 \
                           + 186 * input[1]                 \
                           + 221 * input[14]                \
                           + 236 * input[4]                 \
                           + 79 * input[2]                  \
                           + 175 * input[10]                \
                           + 184 * input[9]                 \
                           + 160 * input[11]                \
                           + 227 * input[12]                \
                           + 99 * input[8]                  \
                           + 71 * input[13]                 \
                           + 4 * input[5]   )& 0xffffffff                 )
Sol.add(dword_422000[0] == (203 * input[3]                 \
                          + 31 * input[0]                     \
                          + 11 * input[14]                  \
                          + 149 * input[7]                  \
                          + 215 * input[5]                  \
                          + 206 * input[1]                  \
                          + 245 * input[6]                  \
                          + 9 * input[11]                   \
                          + 16 * input[10]                  \
                          + 241 * input[13]                 \
                          + 110 * input[8]                  \
                          + 175 * input[2]                  \
                          + 38 * input[4]                   \
                          + 227 * input[9]                  \
                          + 208 * input[12]                 \
                          + 8 * input[15]     )& 0xffffffff               )
Sol.add(dword_422000[2] == (132 * input[3]                 \
                          + 119 * input[14]                 \
                          + 26 * input[8]                   \
                          + 24 * input[6]                   \
                          + 121 * input[11]                 \
                          + 235 * input[2]                  \
                          + 228 * input[12]                 \
                          + 34 * input[5]                   \
                          + 37 * input[15]                  \
                          + 24 * input[9]                   \
                          + 145 * input[13]                 \
                          + 199 * input[4]                  \
                          + 173 * input[10]                 \
                          + 58 * input[0]                     \
                          + 246 * input[7]                  \
                          + 199 * input[1]) & 0xffffffff   )              

assert Sol.check() == sat
print(Sol.model())

input = [None] * 16
input[11] = 51
input[0] = 90
input[2] = 1
input[14] = 114
input[6] = 186
input[13] = 43
input[5] = 42
input[4] = 43
input[12] = 113
input[15] = 72
input[1] = 45
input[10] = 186
input[9] = 179
input[7] = 51
input[8] = 72
input[3] = 51

idx = [0x02, 0x03, 0x05, 0x07, 0x0B, 0x0D, 0x11, 0x13, 0x17, 0x1D]
byte_423D80 = [0xD1, 0x9C, 0x68, 0xC0, 0x13, 0xAC, 0x48, 0x32, 0xA3, 0xBA, 0x4C, 0xE7, 0x6D, 0xC8, 0x1C, 0xAB, 0xE2, 0x7A, 0x42, 0xE1, 0x7B, 0x16, 0x67, 0x03, 0xAE, 0x7E, 0xAA, 0x38, 0x22, 0x02, 0x39, 0x51, 0xC7, 0x79, 0xD7, 0xCB, 0xEF, 0x62, 0x98, 0xDC, 0x53, 0x72, 0x89, 0xA5, 0x4B, 0xC6, 0x86, 0xF6, 0xFC, 0x77, 0x5A, 0xF5, 0x2E, 0x3D, 0xB2, 0xFE, 0x59, 0x27, 0x80, 0x63, 0xDD, 0x1A, 0x12, 0x5E, 0xED, 0xB0, 0xBC, 0xC4, 0x5F, 0x11, 0xC9, 0x09, 0xC5, 0x75, 0x96, 0x0A, 0x2F, 0x00, 0x17, 0x81, 0x14, 0x47, 0xBB, 0x9D, 0x8E, 0x3C, 0xD6, 0xA1, 0xE0, 0xA2, 0x26, 0x5D, 0x08, 0x6E, 0x4E, 0xF1, 0xCF, 0x73, 0x8A, 0x90, 0x0B, 0xB3, 0x3E, 0xB6, 0x1F, 0xC3, 0xB7, 0xDA, 0x8D, 0x05, 0xEE, 0x18, 0x93, 0x3A, 0x6A, 0x8C, 0x43, 0x8F, 0xEB, 0xE9, 0x5B, 0x29, 0x37, 0x1E, 0x46, 0x33, 0x31, 0xFB, 0x35, 0x34, 0x61, 0x04, 0x0E, 0x2B, 0x74, 0xF9, 0x8B, 0x2C, 0x20, 0x0C, 0x7C, 0x28, 0x5C, 0xCA, 0xE6, 0x6B, 0xD8, 0x30, 0xE4, 0x21, 0x44, 0x70, 0x06, 0xA6, 0x60, 0x41, 0x84, 0x10, 0x95, 0x4F, 0x64, 0x83, 0xD2, 0x9A, 0xBE, 0xAF, 0x9F, 0x07, 0xC1, 0xB8, 0x3B, 0x65, 0xCC, 0x57, 0xB5, 0xD9, 0x92, 0xDE, 0x0D, 0xE3, 0xF3, 0xA4, 0xBD, 0x6F, 0xD3, 0x25, 0x88, 0x71, 0xFF, 0xA9, 0x36, 0xB1, 0x78, 0x24, 0x69, 0xAD, 0x19, 0xBF, 0xFD, 0xCD, 0x4A, 0xEA, 0x87, 0x91, 0xA8, 0x66, 0x82, 0x50, 0x0F, 0x99, 0x45, 0xF2, 0xD5, 0x9B, 0x94, 0x7D, 0xCE, 0xDB, 0xB9, 0x52, 0xE5, 0xF4, 0x01, 0x7F, 0xD4, 0x15, 0x2D, 0x3F, 0x1D, 0xA7, 0xC2, 0xFA, 0x40, 0xE8, 0xA0, 0x55, 0x6C, 0xF7, 0x1B, 0x58, 0x85, 0x56, 0x9E, 0xEC, 0x97, 0x23, 0xF0, 0x4D, 0xD0, 0xF8, 0x2A, 0x49, 0xB4, 0x76, 0x54, 0xDF]
def Fun_0x1d():
    for i in range(len(input)):
        for j in range(len(byte_423D80)):
            if byte_423D80[j] == input[i]:
                input[i] = j
                break



byte_423780 = [0x38, 0x5A, 0xC7, 0x98, 0x15, 0x6A, 0xC9, 0x28, 0x33, 0xEA, 0xF4, 0xD9, 0xDB, 0x77, 0xB8, 0x49, 0x1B, 0x79, 0xF5, 0xFD, 0x3E, 0xA2, 0xDE, 0x17, 0xC4, 0x5E, 0xE5, 0x11, 0xB6, 0x1D, 0x86, 0xF9, 0x90, 0x78, 0x8A, 0x14, 0x12, 0xB1, 0xC2, 0x21, 0xF1, 0x02, 0x58, 0xA1, 0x23, 0x0C, 0xAD, 0xA5, 0x50, 0x48, 0x1E, 0x6D, 0xF8, 0x96, 0x9D, 0x19, 0x00, 0xBD, 0x26, 0xCE, 0xA7, 0x24, 0x2E, 0x39, 0x7B, 0xFA, 0x5F, 0xCC, 0x1A, 0x0B, 0x40, 0x0F, 0x4B, 0x82, 0xE2, 0x97, 0x10, 0x2A, 0xFC, 0x3B, 0xB2, 0x66, 0x27, 0x54, 0x07, 0xE3, 0x08, 0xA3, 0xA6, 0xED, 0x62, 0x13, 0x9C, 0x20, 0x01, 0x92, 0xE8, 0xAE, 0xBE, 0xE1, 0x0A, 0x41, 0x94, 0x80, 0xA9, 0x2F, 0x29, 0x70, 0x35, 0x16, 0xF7, 0x6B, 0xFE, 0x9E, 0x0D, 0xD3, 0x7F, 0x1F, 0xA0, 0x32, 0xD2, 0x52, 0x05, 0x76, 0x89, 0x9B, 0x7A, 0x8F, 0x99, 0xEF, 0xCF, 0x51, 0x0E, 0xEC, 0x59, 0x5C, 0x37, 0xD5, 0x8E, 0x31, 0x34, 0x2D, 0x93, 0x25, 0x1C, 0xC8, 0x5B, 0x47, 0x9F, 0x03, 0x67, 0x7E, 0x42, 0x7D, 0x3A, 0xAA, 0x57, 0xDA, 0x9A, 0xAB, 0x74, 0x72, 0xE4, 0xB7, 0x5D, 0xCD, 0x87, 0x46, 0x2B, 0x43, 0xF3, 0xD0, 0x85, 0x55, 0xBB, 0xD4, 0xC6, 0x61, 0x56, 0x04, 0x65, 0x7C, 0x88, 0xC3, 0x73, 0xBC, 0xEB, 0xDD, 0x4D, 0xE0, 0xE6, 0xC0, 0x63, 0x8D, 0xF2, 0x81, 0xF6, 0xA8, 0x3D, 0x3F, 0xA4, 0xE9, 0x4A, 0xB5, 0xF0, 0xCA, 0x8B, 0x2C, 0xD7, 0xAC, 0xC5, 0xC1, 0xBF, 0x53, 0xD1, 0x6F, 0x06, 0xE7, 0xD6, 0x09, 0x95, 0x44, 0x71, 0xB9, 0x83, 0x4C, 0x22, 0xAF, 0xB4, 0x75, 0x36, 0x30, 0xCB, 0xEE, 0x91, 0x45, 0x8C, 0x4E, 0x6E, 0x6C, 0x4F, 0x84, 0xBA, 0xFF, 0x64, 0xB3, 0x60, 0xFB, 0xB0, 0x18, 0xD8, 0xDF, 0x3C, 0x68, 0xDC, 0x69]
def Fun_0x17():
    for i in range(len(input)):
        for j in range(len(byte_423780)):
            if byte_423780[j] == input[i]:
                input[i] = j
                break

byte_423380 = [0x91, 0x67, 0x1A, 0xBE, 0xAB, 0xC2, 0x85, 0xD5, 0xDA, 0xCC, 0xF7, 0x5B, 0x54, 0x61, 0x05, 0xDF, 0x02, 0x70, 0x65, 0x69, 0x9A, 0x7A, 0x09, 0x92, 0x5D, 0x2A, 0xA7, 0x37, 0xFF, 0x19, 0xE6, 0x99, 0xF3, 0x1E, 0xBD, 0x82, 0x48, 0x3C, 0xE8, 0xC8, 0x66, 0x17, 0xB7, 0xA9, 0xC5, 0x4E, 0x33, 0x84, 0x45, 0xD3, 0x8B, 0x49, 0x50, 0x43, 0x8F, 0xCD, 0x73, 0x29, 0x04, 0xDC, 0x01, 0x0C, 0xDD, 0x2E, 0xFB, 0x6E, 0x0F, 0x24, 0x57, 0xE9, 0xC9, 0x7D, 0xB3, 0x40, 0x4B, 0x56, 0x6C, 0x68, 0xE2, 0x22, 0xF6, 0x80, 0xAA, 0x95, 0xD4, 0x97, 0x94, 0x21, 0x53, 0xD1, 0xE3, 0x59, 0xD2, 0xED, 0x41, 0x4D, 0x74, 0xA3, 0xA0, 0x32, 0x0D, 0xFC, 0x46, 0x34, 0xFA, 0xB1, 0x5E, 0xC6, 0x71, 0xC0, 0xE0, 0x3F, 0x13, 0x12, 0xD7, 0xEE, 0xF8, 0x26, 0xE1, 0x25, 0x88, 0x77, 0xB0, 0x8D, 0x6A, 0xEA, 0x0E, 0xD6, 0x3E, 0x03, 0x64, 0xBF, 0x8C, 0x96, 0xD9, 0xA4, 0x42, 0xAD, 0xFD, 0x16, 0x5A, 0xE4, 0x06, 0x9D, 0x07, 0x87, 0x5F, 0xAF, 0xDB, 0xC1, 0x93, 0x1C, 0xF1, 0xDE, 0xA6, 0x3A, 0xF4, 0x2C, 0x1B, 0x39, 0xE7, 0x4A, 0xC7, 0x35, 0xFE, 0x0A, 0x62, 0xF0, 0xCA, 0xEC, 0x27, 0x52, 0x23, 0x7F, 0xA5, 0x79, 0x7C, 0x75, 0x86, 0xEB, 0x60, 0xA8, 0xF5, 0x1F, 0x20, 0xC3, 0x63, 0x5C, 0x72, 0x18, 0xE5, 0x51, 0xAC, 0xB9, 0x90, 0x9F, 0x4C, 0xB2, 0xCB, 0x00, 0x6F, 0x28, 0xA1, 0xB6, 0x9B, 0xD0, 0x7B, 0x36, 0x4F, 0x9C, 0xCF, 0x98, 0x8A, 0x0B, 0x78, 0xB4, 0x7E, 0x2B, 0xEF, 0x58, 0xB5, 0xBA, 0x55, 0xB8, 0x10, 0x2F, 0x44, 0xAE, 0x89, 0x08, 0xC4, 0x3B, 0x9E, 0xF9, 0x6D, 0xF2, 0x15, 0x1D, 0x30, 0x47, 0x8E, 0x31, 0x2D, 0xD8, 0x6B, 0x3D, 0x11, 0x14, 0xA2, 0x83, 0xCE, 0xBB, 0x81, 0xBC, 0x76, 0x38]
def Fun_0x13():
    for i in range(len(input)):
        for j in range(len(byte_423380)):
            if byte_423380[j] == input[i]:
                input[i] = j
                break

byte_423180 = [0xE8, 0x22, 0x64, 0x9F, 0xC5, 0xD5, 0x25, 0xC9, 0x5D, 0xDF, 0xA1, 0x74, 0xCB, 0x57, 0xF7, 0xF0, 0xBD, 0x56, 0xFF, 0x33, 0x79, 0xFE, 0x87, 0xB6, 0xB1, 0x54, 0x10, 0x95, 0x8A, 0xEC, 0x7B, 0x48, 0x84, 0x3D, 0x30, 0xEF, 0x86, 0xFA, 0x97, 0x1C, 0xDC, 0xA9, 0x5A, 0xF3, 0x67, 0x18, 0x83, 0x72, 0x06, 0xB9, 0xF5, 0x05, 0x68, 0x59, 0xF2, 0xE4, 0x88, 0x5E, 0x14, 0x17, 0x11, 0x9C, 0xAB, 0xDE, 0xEB, 0x7D, 0x62, 0x9B, 0xD6, 0xF4, 0x01, 0x29, 0xBC, 0xC0, 0x69, 0xA2, 0x2B, 0x0D, 0x1D, 0x98, 0x6A, 0xBE, 0x65, 0x09, 0xF8, 0x96, 0xB4, 0x6E, 0x63, 0xE3, 0x34, 0x2D, 0xCE, 0x0A, 0xCD, 0xAA, 0x21, 0xCC, 0xE7, 0xA5, 0xDB, 0xD8, 0x03, 0xDD, 0xB2, 0x1F, 0x9D, 0x9E, 0x0E, 0x8F, 0x8B, 0xCA, 0x92, 0x0B, 0xA7, 0x5B, 0xD2, 0xCF, 0x47, 0x07, 0x04, 0xAE, 0x3B, 0xA8, 0x7C, 0x73, 0xF9, 0x35, 0xEE, 0x7A, 0xB0, 0xBA, 0x85, 0x46, 0x3E, 0x81, 0xC7, 0x40, 0x37, 0x15, 0x3A, 0x19, 0xE0, 0x1E, 0x28, 0x4A, 0x4F, 0x8C, 0xD4, 0x51, 0x2E, 0x94, 0x89, 0x2A, 0x0F, 0x7E, 0xE1, 0xC8, 0x5F, 0x4E, 0x6D, 0xF6, 0x49, 0xB8, 0x55, 0x60, 0x82, 0x20, 0x36, 0xC1, 0x0C, 0x1B, 0xC4, 0x00, 0xE5, 0xA3, 0x2C, 0xE9, 0xC2, 0xF1, 0x23, 0x3F, 0xC3, 0xB5, 0x8D, 0xD7, 0x42, 0xFC, 0x50, 0x13, 0xBB, 0x61, 0x9A, 0x44, 0xE6, 0x91, 0x2F, 0x70, 0xC6, 0x6F, 0xD1, 0x27, 0x43, 0x08, 0xDA, 0xFD, 0x52, 0x71, 0x77, 0xED, 0xE2, 0xAD, 0x16, 0x8E, 0x12, 0x4C, 0x31, 0x3C, 0x39, 0x78, 0x90, 0xBF, 0x1A, 0x76, 0x75, 0x41, 0x99, 0xD0, 0x80, 0xB7, 0x66, 0x24, 0xD3, 0x7F, 0x4B, 0x45, 0x5C, 0x53, 0x4D, 0x26, 0x32, 0xA0, 0xFB, 0xB3, 0x38, 0x6B, 0xAF, 0xA6, 0xD9, 0x02, 0xA4, 0xEA, 0x6C, 0xAC, 0x58, 0x93]
def Fun_0x11():
    for i in range(len(input)):
        for j in range(len(byte_423180)):
            if byte_423180[j] == input[i]:
                input[i] = j
                break

byte_422D80 = [0xB0, 0x28, 0x0B, 0x89, 0x4B, 0xA4, 0xBE, 0x1A, 0x8F, 0x6C, 0xCF, 0xB2, 0xB5, 0xFE, 0xFB, 0x59, 0x2D, 0x29, 0x39, 0x62, 0x97, 0xAA, 0xD7, 0x7D, 0x94, 0x2C, 0xFC, 0x5D, 0xB4, 0x7C, 0x8A, 0x82, 0xD3, 0xA7, 0xBA, 0xDF, 0x21, 0xE6, 0xA2, 0xD0, 0xE8, 0xF0, 0x67, 0x3A, 0xB9, 0x98, 0xF9, 0xAE, 0xD1, 0x56, 0xD8, 0xCA, 0x10, 0xEA, 0x92, 0xA8, 0x75, 0x7E, 0x65, 0xA9, 0xAF, 0x51, 0xC9, 0x8E, 0xD4, 0x77, 0xE4, 0x49, 0x06, 0x61, 0x9E, 0x24, 0xD9, 0x9B, 0x11, 0x05, 0x1D, 0x96, 0x9A, 0xB1, 0xE0, 0x83, 0xE1, 0x1C, 0xCD, 0xF3, 0x38, 0xB3, 0x57, 0x50, 0xF4, 0xAC, 0xEB, 0x14, 0xA5, 0x46, 0xF6, 0x93, 0xAD, 0x7B, 0x30, 0xEF, 0x79, 0x17, 0x47, 0xDA, 0xC0, 0xDD, 0xDE, 0xDC, 0x5A, 0x76, 0x3B, 0x31, 0x0D, 0x0E, 0x86, 0xF1, 0x71, 0xFA, 0x0C, 0x00, 0xA3, 0xBF, 0x64, 0x37, 0x22, 0xD2, 0x69, 0x5C, 0xC6, 0x16, 0x9F, 0x5E, 0x7A, 0x1E, 0x27, 0x60, 0x6E, 0xF8, 0x8C, 0xEE, 0xC2, 0x74, 0x81, 0x8B, 0x33, 0x03, 0xBD, 0x2A, 0x0A, 0x68, 0x6B, 0x3F, 0x4C, 0xC3, 0x15, 0x04, 0x3D, 0x63, 0xF5, 0xAB, 0xCC, 0x3C, 0x53, 0x20, 0x66, 0xC4, 0xC1, 0x23, 0xE7, 0x25, 0x55, 0xC7, 0xED, 0xB7, 0xBC, 0xCB, 0x8D, 0x09, 0xCE, 0x52, 0xBB, 0xE2, 0xC5, 0xB6, 0x26, 0x12, 0x2F, 0x99, 0x58, 0x40, 0x6D, 0xA1, 0x3E, 0x48, 0x85, 0xA6, 0xF2, 0x0F, 0x43, 0x78, 0xB8, 0x01, 0xE5, 0xD5, 0x6F, 0x4E, 0xF7, 0x13, 0x42, 0xEC, 0x45, 0x2B, 0x4F, 0x36, 0xDB, 0x9C, 0xE3, 0x44, 0x34, 0x84, 0x73, 0x2E, 0x7F, 0xFD, 0x91, 0x41, 0xD6, 0x95, 0x18, 0xFF, 0x70, 0xC8, 0x02, 0x5F, 0x08, 0x1B, 0x6A, 0x5B, 0x19, 0xA0, 0x4D, 0x35, 0x54, 0xE9, 0x32, 0x88, 0x72, 0x07, 0x87, 0x90, 0x4A, 0x80, 0x1F, 0x9D]
def Fun_0xd():
    for i in range(len(input)):
        for j in range(len(byte_422D80)):
            if byte_422D80[j] == input[i]:
                input[i] = j
                break

byte_422B80 = [0x38, 0xD9, 0xDA, 0xE6, 0xB5, 0xF1, 0x0B, 0x93, 0x0C, 0x58, 0x0D, 0xAE, 0x0A, 0x85, 0x2A, 0x50, 0xC2, 0xBF, 0xD4, 0x28, 0x52, 0xC4, 0x4F, 0xE1, 0x44, 0xE0, 0xA2, 0x70, 0x36, 0x65, 0x4B, 0x41, 0x9D, 0x5F, 0x05, 0x7C, 0xF7, 0xD7, 0x99, 0x8B, 0xCC, 0xCE, 0x16, 0xBE, 0xB6, 0xC5, 0x8F, 0x79, 0xC7, 0x20, 0x7E, 0xF4, 0xF3, 0x2E, 0x4A, 0x89, 0xD6, 0x0F, 0x6E, 0xB0, 0x61, 0xB1, 0x6D, 0x19, 0x73, 0x03, 0x74, 0xA1, 0x40, 0xEC, 0xC0, 0x57, 0x94, 0x7A, 0x66, 0xD5, 0xEA, 0x17, 0x6A, 0x84, 0x37, 0xED, 0xF6, 0x13, 0x31, 0x5B, 0x82, 0x1E, 0xFC, 0x92, 0xE2, 0x42, 0x86, 0xBA, 0xE3, 0x91, 0x7F, 0x67, 0x5C, 0x98, 0x15, 0x22, 0x8D, 0x80, 0x04, 0xE4, 0x25, 0x09, 0xA0, 0xAD, 0x63, 0xE5, 0xB4, 0x9A, 0x3C, 0xA3, 0x3A, 0x69, 0xF8, 0xCD, 0xBC, 0x88, 0x55, 0xB2, 0xBD, 0x6B, 0x77, 0x71, 0xB3, 0xD3, 0x90, 0x75, 0x06, 0x49, 0xC3, 0x32, 0x4D, 0x1D, 0xA8, 0xAA, 0xFB, 0x7B, 0x7D, 0x2B, 0xA6, 0x34, 0x72, 0x47, 0xF0, 0x2F, 0x9C, 0x08, 0x00, 0x14, 0x8C, 0x26, 0x5E, 0x87, 0xD1, 0xCF, 0xC9, 0x18, 0x51, 0x23, 0xCB, 0xF5, 0x1C, 0x9F, 0x97, 0xF9, 0xBB, 0xA7, 0x39, 0x45, 0x02, 0xFD, 0x46, 0x8A, 0x54, 0xA4, 0x8E, 0x9E, 0x68, 0x96, 0x0E, 0x78, 0xB8, 0x3D, 0x11, 0x64, 0xAF, 0x10, 0xDE, 0x6C, 0x60, 0x5A, 0x76, 0x1A, 0xE9, 0xC1, 0x3E, 0xCA, 0x9B, 0x27, 0x30, 0xEF, 0xFF, 0x07, 0xD2, 0xB9, 0x2D, 0xD0, 0xEE, 0x83, 0xAB, 0xF2, 0x4C, 0xA5, 0x21, 0x62, 0x81, 0x33, 0x1B, 0xD8, 0x6F, 0xAC, 0x3B, 0x5D, 0xE8, 0xFA, 0x3F, 0xDB, 0x95, 0xE7, 0x59, 0x12, 0x48, 0x35, 0xC6, 0x2C, 0x4E, 0x01, 0xDD, 0x43, 0x29, 0xDC, 0x24, 0x1F, 0xB7, 0xA9, 0xEB, 0xC8, 0xFE, 0x56, 0xDF, 0x53]
def Fun_0xb():
    for i in range(len(input)):
        for j in range(len(byte_422B80)):
            if byte_422B80[j] == input[i]:
                input[i] = j
                break

byte_422780 = [0x0F, 0xA5, 0xBA, 0x03, 0xF9, 0x69, 0x2A, 0xD7, 0xEA, 0xB5, 0xFC, 0xA1, 0x39, 0x20, 0x68, 0x72, 0x25, 0xB2, 0x6C, 0xAD, 0x88, 0x51, 0x73, 0xEB, 0xCF, 0x13, 0xDE, 0x7C, 0x6D, 0x38, 0x05, 0x09, 0xC2, 0x96, 0x1F, 0x7F, 0x37, 0x4A, 0xC9, 0xE7, 0x6A, 0xB0, 0x59, 0xF7, 0xD2, 0xB9, 0x16, 0xC8, 0xEE, 0xA9, 0x18, 0x80, 0xAC, 0xE3, 0x9E, 0x6F, 0x3C, 0x2F, 0x3E, 0x9A, 0xBE, 0x1D, 0xB4, 0x7B, 0x7D, 0x32, 0x6B, 0x74, 0xC5, 0xC0, 0xC7, 0xD1, 0x29, 0x98, 0xDD, 0xB6, 0x0E, 0x4D, 0xBF, 0x79, 0x0D, 0xDA, 0x7A, 0x17, 0x71, 0x43, 0x87, 0xFF, 0xDC, 0xC6, 0x12, 0xE9, 0x67, 0x2D, 0x70, 0x9F, 0x95, 0x30, 0x26, 0x24, 0x2B, 0xA8, 0xA2, 0xD8, 0x3B, 0x31, 0xA0, 0x3D, 0x4B, 0x90, 0x60, 0x34, 0x75, 0xE8, 0x5D, 0xF4, 0x85, 0xF3, 0xFE, 0x35, 0xCB, 0xB8, 0x02, 0x50, 0xB1, 0xF1, 0x1A, 0x1B, 0x21, 0xCD, 0xC4, 0x7E, 0xED, 0x07, 0xD9, 0xD6, 0x44, 0x15, 0x8E, 0x49, 0xB3, 0x97, 0xE6, 0x63, 0xB7, 0xEF, 0x3A, 0x8F, 0xF2, 0x53, 0x10, 0x77, 0x86, 0xF8, 0x8A, 0x28, 0x3F, 0xD4, 0x4C, 0xE5, 0x82, 0x83, 0xEC, 0x62, 0x89, 0xDF, 0xC3, 0x14, 0xCA, 0xA3, 0x5F, 0x64, 0x47, 0xFD, 0x00, 0x84, 0x66, 0xA7, 0x5A, 0x0C, 0x01, 0xD5, 0x5B, 0x0A, 0x4F, 0x27, 0x78, 0x0B, 0x2E, 0x48, 0x36, 0xFA, 0x08, 0x56, 0xE0, 0xA6, 0xC1, 0x5C, 0x8B, 0x41, 0x06, 0xBB, 0x52, 0x93, 0xAF, 0x2C, 0x5E, 0xF6, 0x61, 0xF0, 0xAB, 0x91, 0x45, 0x04, 0xBD, 0xCC, 0xE4, 0x65, 0x9D, 0x92, 0xCE, 0x40, 0xAE, 0x76, 0x9B, 0x9C, 0xAA, 0x54, 0xD0, 0x1C, 0x81, 0x4E, 0x57, 0x55, 0x23, 0x6E, 0x1E, 0x99, 0xDB, 0xFB, 0xA4, 0x22, 0x19, 0x58, 0x11, 0x8D, 0x94, 0xD3, 0xE2, 0x8C, 0xF5, 0x42, 0x46, 0xBC, 0x33, 0xE1]
def Fun_0x7():
    for i in range(len(input)):
        for j in range(len(byte_422780)):
            if byte_422780[j] == input[i]:
                input[i] = j
                break

byte_422580 = [0x00, 0x74, 0x59, 0xC6, 0xAC, 0xD3, 0xC1, 0xA0, 0x88, 0x3F, 0x1C, 0x28, 0x17, 0x22, 0xC5, 0x38, 0xF9, 0x1B, 0x21, 0x49, 0x99, 0xAF, 0xD6, 0x95, 0xA4, 0x9D, 0x5D, 0x5B, 0x73, 0xFE, 0xC9, 0x9A, 0x4C, 0xB4, 0x27, 0x5E, 0x71, 0x25, 0xE2, 0x90, 0xC0, 0x62, 0x5F, 0x48, 0x77, 0xE0, 0xF2, 0x8E, 0x40, 0xC7, 0x79, 0x1A, 0xDC, 0xF3, 0x01, 0xB6, 0xD8, 0xB5, 0x67, 0x1E, 0x85, 0x12, 0x68, 0x87, 0xD0, 0x30, 0xEB, 0x2F, 0x50, 0xCF, 0xEE, 0xDD, 0xFB, 0xE6, 0xA5, 0x69, 0x05, 0x75, 0xB7, 0xEF, 0x70, 0x53, 0xFF, 0xBA, 0x80, 0x41, 0x9B, 0xA1, 0x39, 0xF8, 0x65, 0x1F, 0x7A, 0x51, 0x98, 0xAD, 0x02, 0x13, 0x18, 0xC3, 0x31, 0x89, 0xCD, 0xCA, 0x91, 0xD1, 0x78, 0x57, 0x47, 0xB8, 0x54, 0x9F, 0x96, 0x04, 0x23, 0x2B, 0xE5, 0x46, 0x29, 0x7C, 0x76, 0x82, 0xBC, 0xFC, 0x6E, 0xEC, 0xED, 0x64, 0x4A, 0x26, 0x34, 0x5C, 0x19, 0x55, 0xFD, 0x6D, 0xFA, 0x7E, 0xB2, 0xD4, 0xF1, 0xF6, 0xE4, 0x60, 0xB0, 0x52, 0x9E, 0x8F, 0xBB, 0x08, 0x3B, 0x97, 0xE8, 0x10, 0x6C, 0x44, 0x3A, 0x36, 0x35, 0x03, 0xC4, 0x81, 0x9C, 0xAB, 0xCB, 0x66, 0xAA, 0x37, 0xA2, 0xD2, 0xE1, 0xE9, 0x7B, 0x14, 0x8D, 0xD9, 0xF5, 0x0B, 0xC2, 0x07, 0xA8, 0x0D, 0xA3, 0x0A, 0x84, 0x6B, 0x2C, 0xEA, 0x0C, 0xAE, 0x7D, 0x6F, 0xD7, 0xE7, 0xC8, 0x3C, 0x45, 0xCC, 0x58, 0xB9, 0x3D, 0x33, 0x4E, 0x4B, 0x8C, 0xCE, 0x72, 0x6A, 0x8B, 0x2D, 0x24, 0x11, 0xDF, 0x5A, 0x2E, 0x92, 0xDA, 0x86, 0x94, 0xA7, 0xD5, 0x4F, 0x2A, 0xB3, 0x63, 0x61, 0xE3, 0xDE, 0x43, 0x1D, 0xBF, 0x15, 0x32, 0xBE, 0x16, 0x3E, 0x93, 0x7F, 0x83, 0x56, 0x06, 0xF7, 0x8A, 0x20, 0xBD, 0x0E, 0xA6, 0xDB, 0x0F, 0xB1, 0x42, 0xF0, 0x09, 0x4D, 0xA9, 0xF4]

def Fun_0x5():
    for i in range(len(input)):
        for j in range(len(byte_422580)):
            if byte_422580[j] == input[i]:
                input[i] = j
                break

byte_422380 = [0x45, 0x1F, 0x63, 0x81, 0xE6, 0xAD, 0x4F, 0xD3, 0xC0, 0x15, 0x69, 0x8F, 0x0D, 0x31, 0x0C, 0xB0, 0xF1, 0x2E, 0x98, 0xC1, 0xC2, 0x96, 0xB2, 0xEB, 0xBF, 0xDF, 0x17, 0xF4, 0x7F, 0xE5, 0x66, 0x73, 0xD8, 0x56, 0x46, 0x20, 0x9C, 0x77, 0x3D, 0x72, 0xA3, 0x91, 0x49, 0x68, 0x4C, 0x1E, 0xAE, 0x06, 0x7A, 0x94, 0xDD, 0x52, 0x55, 0x2C, 0xB8, 0x42, 0x79, 0xFE, 0x38, 0xEF, 0x8B, 0xF7, 0xAC, 0xDC, 0xFF, 0x78, 0x34, 0x70, 0xA9, 0xCE, 0x3F, 0x0E, 0x11, 0x43, 0x5B, 0xF8, 0xAF, 0xD0, 0xFA, 0x33, 0xBA, 0xCF, 0x4A, 0xC9, 0x88, 0x4E, 0x80, 0x10, 0x85, 0x37, 0x12, 0xAB, 0xE1, 0x61, 0xB7, 0x3E, 0x4D, 0x19, 0x3A, 0x04, 0x8C, 0x92, 0x0B, 0xE7, 0x3C, 0xEA, 0xC7, 0x16, 0x35, 0xB1, 0xA7, 0x8E, 0x40, 0x9F, 0xB6, 0xB5, 0x25, 0xA0, 0x5A, 0x30, 0x7D, 0xA2, 0x1A, 0x64, 0xC5, 0x6D, 0x74, 0x82, 0x08, 0x7E, 0xD2, 0xF6, 0xAA, 0xDA, 0xED, 0x4B, 0x6E, 0xE8, 0xE9, 0xE2, 0xD4, 0x71, 0xB9, 0x09, 0x84, 0x3B, 0xC4, 0x1C, 0x60, 0xFD, 0x22, 0x99, 0x39, 0x97, 0x18, 0x89, 0x7C, 0xA4, 0x27, 0xBD, 0x0F, 0xCC, 0x95, 0xF5, 0xB3, 0x65, 0x6B, 0x8A, 0x58, 0x36, 0xBB, 0x9E, 0x75, 0xD1, 0x03, 0x9D, 0x6A, 0x6C, 0x53, 0x05, 0xB4, 0xE4, 0xEE, 0x67, 0x87, 0x7B, 0x32, 0x2D, 0x24, 0x2A, 0x59, 0xEC, 0x0A, 0xDB, 0x21, 0x07, 0x23, 0x50, 0x02, 0x41, 0xF2, 0x83, 0xD9, 0x26, 0xBC, 0x6F, 0x86, 0xA6, 0x93, 0xF9, 0xC8, 0xD6, 0xA5, 0x1D, 0xE3, 0xE0, 0xFC, 0xCA, 0x1B, 0x5E, 0x8D, 0x2F, 0x5C, 0xBE, 0x47, 0xA8, 0x44, 0x57, 0x54, 0x48, 0xC3, 0x00, 0x62, 0x5D, 0xCB, 0xD7, 0x76, 0xCD, 0x28, 0xD5, 0x14, 0x90, 0x13, 0xDE, 0x5F, 0xF0, 0x01, 0x2B, 0xC6, 0x29, 0x9A, 0x9B, 0x51, 0xF3, 0xFB, 0xA1]
def Fun_0x3():
    for i in range(len(input)):
        for j in range(len(byte_422380)):
            if byte_422380[j] == input[i]:
                input[i] = j
                break

byte_422280 = [0x7A, 0x91, 0x9F, 0x23, 0x71, 0xD1, 0x63, 0xDB, 0x59, 0x0A, 0xEC, 0x69, 0xEE, 0x76, 0x5D, 0x64, 0x37, 0x42, 0x8C, 0x0B, 0x3C, 0x5C, 0x80, 0xAD, 0x6A, 0x03, 0x43, 0x93, 0xBC, 0xBF, 0xE3, 0xAF, 0x5A, 0x8A, 0x65, 0x0D, 0x31, 0xDF, 0x3E, 0xA7, 0xE4, 0xDD, 0xB4, 0xB0, 0x56, 0x1C, 0x12, 0xA4, 0x9E, 0xD8, 0x3D, 0x81, 0x60, 0x9A, 0xCB, 0xFA, 0xB1, 0xE0, 0xD3, 0xF4, 0xA2, 0x26, 0x68, 0x90, 0x4B, 0x45, 0x85, 0x20, 0x16, 0xDE, 0xED, 0x4C, 0x6F, 0x34, 0xDC, 0xBE, 0xD2, 0x46, 0x33, 0x14, 0x77, 0xC6, 0xCD, 0xF0, 0xC5, 0xAC, 0x1F, 0xD0, 0x95, 0x97, 0x3F, 0xD7, 0x52, 0xAE, 0xB9, 0xC9, 0x0C, 0xCA, 0x4E, 0xF1, 0xB7, 0x39, 0x7F, 0x27, 0x2B, 0x40, 0x4A, 0x51, 0xA1, 0xCC, 0xCE, 0x6E, 0x70, 0xFF, 0x0E, 0xEF, 0x8E, 0x25, 0xB3, 0x5E, 0x6C, 0xAB, 0x02, 0x49, 0xE9, 0x9B, 0x36, 0x13, 0x9C, 0x04, 0x35, 0xC0, 0xFB, 0x3A, 0x67, 0xB6, 0x9D, 0xC2, 0x73, 0xB5, 0x6D, 0xCF, 0x83, 0x2C, 0x01, 0xC1, 0x10, 0x6B, 0x79, 0x87, 0x5B, 0x57, 0x47, 0xE5, 0x15, 0xF7, 0xA5, 0x74, 0xAA, 0x53, 0x7D, 0x2E, 0xD5, 0xA3, 0x19, 0xF5, 0x2D, 0xFD, 0x61, 0x8D, 0xC8, 0x1B, 0xC3, 0xDA, 0xF6, 0x72, 0x54, 0x5F, 0x1E, 0xE8, 0x17, 0x50, 0xB2, 0xE7, 0x0F, 0x7E, 0x55, 0xBD, 0x86, 0x00, 0x78, 0x94, 0x92, 0x09, 0x2F, 0xD6, 0xD9, 0xF3, 0x29, 0xE6, 0x24, 0x32, 0x66, 0x22, 0x41, 0xC4, 0x7C, 0x05, 0x98, 0x44, 0x4F, 0x99, 0xA9, 0xE1, 0x8F, 0x08, 0x1A, 0x2A, 0x11, 0xEA, 0x3B, 0xE2, 0x38, 0xB8, 0x18, 0xF9, 0xD4, 0xC7, 0x62, 0x7B, 0x75, 0x58, 0x96, 0x28, 0xEB, 0x06, 0x84, 0x89, 0x48, 0x82, 0x88, 0xA6, 0xFE, 0xA0, 0xF2, 0xF8, 0x1D, 0x8B, 0xFC, 0xA8, 0x21, 0x30, 0xBB, 0x07, 0xBA, 0x4D]
def Fun_0x2():
    for i in range(len(input)):
        for j in range(len(byte_422280)):
            if byte_422280[j] == input[i]:
                input[i] = j
                break


Fun_0x1d()
Fun_0x17()
Fun_0x13()
Fun_0x11()
Fun_0xd()
Fun_0xb()
Fun_0x7()
Fun_0x5()
Fun_0x3()
Fun_0x2()

for i in range(len(input)):
    print(chr(input[i]),end = "")






from z3 import *
inputt = [BitVec(f"inputt[{i}]",8) for i in range(16)]
dword_422040 = [0x00027FC8, 0x00029049, 0x0003336C, 0x0002C6A7, 0x00036CB0, 0x0001F2BB, 0x00035262, 0x0002AEDF, 0x0002955E, 0x0002EE10, 0x0002B057, 0x0002FDE8, 0x00029B92, 0x00035842, 0x000294D2, 0x0002B984]
x = Solver()
x.add(dword_422040[0] == (159 * inputt[8]                     \
                          + 109 * inputt[12]           \
                          + 14 * inputt[0]               \
                          + 92 * inputt[14]            \
                          + 211 * inputt[4]            \
                          + 178 * inputt[7]            \
                          + 57 * inputt[2]             \
                          + 175 * inputt[5]            \
                          + 170 * inputt[11]           \
                          + 59 * inputt[6]             \
                          + 200 * inputt[9]            \
                          + 5 * inputt[15]             \
                          + 48 * inputt[13]            \
                          + 28 * inputt[3]             \
                          + 18 * inputt[10]            \
                          + 228 * inputt[1]   ) & 0xffffffff    )


x.add(dword_422040[6] == (173 * inputt[11]           \
                 + 34 * inputt[5]             \
                 + 69 * inputt[4]             \
                 + 216 * inputt[14]           \
                 + 225 * inputt[9]            \
                 + 160 * inputt[1]            \
                 + 207 * inputt[10]           \
                 + 175 * inputt[7]            \
                 + 121 * inputt[0]              \
                 + 122 * inputt[2]            \
                 + 179 * inputt[12]           \
                 + 91 * inputt[13]            \
                 + 181 * inputt[8]            \
                 + 93 * inputt[3]             \
                 + 121 * inputt[6]            \
                 + 12 * inputt[15]        )&0xffffffff    )
x.add(dword_422040[8] == (215 * inputt[11]           \
                 + 164 * inputt[5]            \
                 + 97 * inputt[2]             \
                 + 99 * inputt[3]             \
                 + 188 * inputt[4]            \
                 + ((inputt[9] << 7)& 0xffffffff )           \
                 + 214 * inputt[6]            \
                 + 106 * inputt[8]            \
                 + 169 * inputt[0]              \
                 + 28 * inputt[14]            \
                 + 18 * inputt[12]            \
                 + inputt[1]                  \
                 + 177 * inputt[10]           \
                 + 114 * inputt[7]            \
                 + 176 * inputt[15]           \
                 + 25 * inputt[13]           )&0xffffffff )
x.add(dword_422040[9] == (175 * inputt[14]           \
                 + 42 * inputt[4]             \
                 + 214 * inputt[12]           \
                 + 43 * inputt[13]            \
                 + 147 * inputt[6]            \
                 + 53 * inputt[10]            \
                 + 12 * inputt[1]             \
                 + 213 * inputt[7]            \
                 + 241 * inputt[9]            \
                 + 223 * inputt[5]            \
                 + 65 * inputt[3]             \
                 + 42 * inputt[15]            \
                 + 131 * inputt[2]            \
                 + 81 * inputt[0]               \
                 + 92 * inputt[11]            \
                 + 110 * inputt[8] )&0xffffffff           )
x.add(dword_422040[13] == (57 * inputt[0]              \
                  + 109 * inputt[7]           \
                  + 60 * inputt[2]            \
                  + 228 * inputt[13]          \
                  + 166 * inputt[4]           \
                  + 236 * inputt[9]           \
                  + 100 * inputt[6]           \
                  + 179 * inputt[11]          \
                  + 20 * inputt[12]           \
                  + 45 * inputt[8]            \
                  + 204 * inputt[3]           \
                  + 182 * inputt[14]          \
                  + 84 * inputt[10]           \
                  + 170 * inputt[15]          \
                  + 199 * inputt[5]           \
                  + 138 * inputt[1]        )&0xffffffff   )
x.add(dword_422040[10] == (98 * inputt[11]           \
                  + 122 * inputt[9]           \
                  + 237 * inputt[12]          \
                  + 117 * inputt[0]             \
                  + 34 * inputt[3]            \
                  + 168 * inputt[8]           \
                  + 135 * inputt[10]          \
                  + 119 * inputt[6]           \
                  + 91 * inputt[2]            \
                  + 161 * inputt[15]          \
                  + 152 * inputt[7]           \
                  + 186 * inputt[4]           \
                  + 187 * inputt[13]          \
                  + 72 * inputt[14]           \
                  + 36 * inputt[5]            \
                  + 171 * inputt[1]     )&0xffffffff      )
x.add(dword_422040[7] == (184 * inputt[9]            \
                 + 112 * inputt[0]              \
                 + 107 * inputt[11]           \
                 + 170 * inputt[13]           \
                 + 55 * inputt[8]             \
                 + 85 * inputt[14]            \
                 + 212 * inputt[10]           \
                 + 173 * inputt[15]           \
                 + 166 * inputt[12]           \
                 + 142 * inputt[4]            \
                 + 202 * inputt[5]            \
                 + 63 * inputt[2]             \
                 + 30 * inputt[7]             \
                 + 175 * inputt[3]            \
                 + 217 * inputt[6]            \
                 + 63 * inputt[1]   )&0xffffffff          )
x.add(dword_422040[15] == (((inputt[7] << 6) &0xffffffff)          \
                  + 228 * inputt[4]           \
                  + 90 * inputt[11]           \
                  + 85 * inputt[3]            \
                  + 196 * inputt[6]           \
                  + 219 * inputt[0]             \
                  + 93 * inputt[14]           \
                  + 183 * inputt[15]          \
                  + 156 * inputt[12]          \
                  + 197 * inputt[8]           \
                  + 119 * inputt[13]          \
                  + 36 * inputt[10]           \
                  + 205 * inputt[2]           \
                  + 94 * inputt[9]            \
                  + 153 * inputt[5]        )&0xffffffff   )
x.add(dword_422040[5] == (9 * inputt[4]              \
                 + ((inputt[5] << 6)& 0xffffffff)           \
                 + 62 * inputt[1]             \
                 + 58 * inputt[7]             \
                 + 100 * inputt[13]           \
                 + 137 * inputt[11]           \
                 + 6 * inputt[0]                \
                 + 119 * inputt[9]            \
                 + 180 * inputt[6]            \
                 + 228 * inputt[8]            \
                 + 88 * inputt[12]            \
                 + 107 * inputt[15]           \
                 + 56 * inputt[14]            \
                 + 207 * inputt[2]            \
                 + 248 * inputt[10]           \
                 + 150 * inputt[3]     )&0xffffffff       )



x.add(dword_422040[3] == (38 * inputt[7]             \
                 + 194 * inputt[4]            \
                 + 105 * inputt[0]              \
                 + 150 * inputt[6]            \
                 + 75 * inputt[1]             \
                 + 89 * inputt[15]            \
                 + 99 * inputt[14]            \
                 + 98 * inputt[3]             \
                 + 91 * inputt[8]             \
                 + 178 * inputt[12]           \
                 + 117 * inputt[2]            \
                 + 48 * inputt[13]            \
                 + 239 * inputt[10]           \
                 + 233 * inputt[11]           \
                 + 63 * inputt[5]             \
                 + 250 * inputt[9]     )&0xffffffff       )



x.add(dword_422040[11] ==( 30 * inputt[8]            \
                  + 13 * inputt[5]            \
                  + 206 * inputt[3]           \
                  + 234 * inputt[15]          \
                  + 71 * inputt[7]            \
                  + 239 * inputt[12]          \
                  + 141 * inputt[10]          \
                  + 179 * inputt[13]          \
                  + 113 * inputt[14]          \
                  + 181 * inputt[9]           \
                  + 52 * inputt[6]            \
                  + 74 * inputt[11]           \
                  + 168 * inputt[4]           \
                  + 239 * inputt[1]           \
                  + 164 * inputt[0]             \
                  + 179 * inputt[2]      )&0xffffffff     )




x.add(dword_422040[14] == (211 * inputt[1]           \
                  + 74 * inputt[5]            \
                  + 144 * inputt[8]           \
                  + 234 * inputt[0]             \
                  + 241 * inputt[2]           \
                  + 157 * inputt[11]          \
                  + 25 * inputt[15]           \
                  + 6 * inputt[10]            \
                  + 243 * inputt[6]           \
                  + 107 * inputt[9]           \
                  + 77 * inputt[12]           \
                  + 127 * inputt[4]           \
                  + 67 * inputt[7]            \
                  + 13 * inputt[14]           \
                  + 151 * inputt[3]           \
                  + 127 * inputt[13] )&0xffffffff         )




x.add(dword_422040[2] == (209 * inputt[9]            \
                 + 110 * inputt[7]            \
                 + 22 * inputt[10]            \
                 + 102 * inputt[11]           \
                 + 187 * inputt[1]            \
                 + 58 * inputt[8]             \
                 + 236 * inputt[6]            \
                 + 146 * inputt[13]           \
                 + 205 * inputt[15]           \
                 + 63 * inputt[2]             \
                 + 211 * inputt[4]            \
                 + 152 * inputt[3]            \
                 + 82 * inputt[14]            \
                 + 14 * inputt[5]             \
                 + 49 * inputt[12]            \
                 + 251 * inputt[0]  )&0xffffffff            )



x.add(dword_422040[12] == (230 * inputt[0]             \
                  + 27 * inputt[3]            \
                  + 186 * inputt[10]          \
                  + 58 * inputt[7]            \
                  + 121 * inputt[1]           \
                  + 59 * inputt[14]           \
                  + 90 * inputt[12]           \
                  + 40 * inputt[2]            \
                  + 230 * inputt[11]          \
                  + 25 * inputt[6]            \
                  + 198 * inputt[5]           \
                  + 81 * inputt[4]            \
                  + 71 * inputt[13]           \
                  + 180 * inputt[8]           \
                  + 149 * inputt[9]           \
                  + 73 * inputt[15]   )&0xffffffff        )




x.add(dword_422040[4] == (188 * inputt[5]            \
                 + 80 * inputt[1]             \
                 + 221 * inputt[6]            \
                 + ((inputt[12] << 6) & 0xffffffff)          \
                 + 230 * inputt[3]            \
                 + 123 * inputt[8]            \
                 + 124 * inputt[11]           \
                 + 253 * inputt[0]              \
                 + 202 * inputt[10]           \
                 + 63 * inputt[2]             \
                 + 40 * inputt[7]             \
                 + 109 * inputt[9]            \
                 + 195 * inputt[15]           \
                 + 199 * inputt[13]           \
                 + 82 * inputt[4]             \
                 + 225 * inputt[14]   )&0xffffffff        )




x.add(dword_422040[1] == (236 * inputt[15]           \
                 + 44 * inputt[14]            \
                 + 214 * inputt[13]           \
                 + 52 * inputt[8]             \
                 + 37 * inputt[6]             \
                 + 101 * inputt[9]            \
                 + 244 * inputt[10]           \
                 + 238 * inputt[11]           \
                 + 109 * inputt[0]              \
                 + 188 * inputt[1]            \
                 + 20 * inputt[3]             \
                 + 87 * inputt[7]             \
                 + 93 * inputt[4]             \
                 + 158 * inputt[5]            \
                 + 105 * inputt[12]           \
                 + 3 * inputt[2]     )&0xffffffff        )

assert x.check() == sat
print(x.model())

input = [None] * 16
input[2] = 51
input[12] = 11
input[3] = 45 
input[0] = 186
input[7] = 186
input[13] = 124
input[4] = 71
input[1] = 42
input[11] = 114
input[15] = 51
input[6] = 42
input[10] = 42
input[8] = 25
input[14] = 209
input[9] = 186
input[5] = 51
print(input)
byte_423D80 = [0xD1, 0x9C, 0x68, 0xC0, 0x13, 0xAC, 0x48, 0x32, 0xA3, 0xBA, 0x4C, 0xE7, 0x6D, 0xC8, 0x1C, 0xAB, 0xE2, 0x7A, 0x42, 0xE1, 0x7B, 0x16, 0x67, 0x03, 0xAE, 0x7E, 0xAA, 0x38, 0x22, 0x02, 0x39, 0x51, 0xC7, 0x79, 0xD7, 0xCB, 0xEF, 0x62, 0x98, 0xDC, 0x53, 0x72, 0x89, 0xA5, 0x4B, 0xC6, 0x86, 0xF6, 0xFC, 0x77, 0x5A, 0xF5, 0x2E, 0x3D, 0xB2, 0xFE, 0x59, 0x27, 0x80, 0x63, 0xDD, 0x1A, 0x12, 0x5E, 0xED, 0xB0, 0xBC, 0xC4, 0x5F, 0x11, 0xC9, 0x09, 0xC5, 0x75, 0x96, 0x0A, 0x2F, 0x00, 0x17, 0x81, 0x14, 0x47, 0xBB, 0x9D, 0x8E, 0x3C, 0xD6, 0xA1, 0xE0, 0xA2, 0x26, 0x5D, 0x08, 0x6E, 0x4E, 0xF1, 0xCF, 0x73, 0x8A, 0x90, 0x0B, 0xB3, 0x3E, 0xB6, 0x1F, 0xC3, 0xB7, 0xDA, 0x8D, 0x05, 0xEE, 0x18, 0x93, 0x3A, 0x6A, 0x8C, 0x43, 0x8F, 0xEB, 0xE9, 0x5B, 0x29, 0x37, 0x1E, 0x46, 0x33, 0x31, 0xFB, 0x35, 0x34, 0x61, 0x04, 0x0E, 0x2B, 0x74, 0xF9, 0x8B, 0x2C, 0x20, 0x0C, 0x7C, 0x28, 0x5C, 0xCA, 0xE6, 0x6B, 0xD8, 0x30, 0xE4, 0x21, 0x44, 0x70, 0x06, 0xA6, 0x60, 0x41, 0x84, 0x10, 0x95, 0x4F, 0x64, 0x83, 0xD2, 0x9A, 0xBE, 0xAF, 0x9F, 0x07, 0xC1, 0xB8, 0x3B, 0x65, 0xCC, 0x57, 0xB5, 0xD9, 0x92, 0xDE, 0x0D, 0xE3, 0xF3, 0xA4, 0xBD, 0x6F, 0xD3, 0x25, 0x88, 0x71, 0xFF, 0xA9, 0x36, 0xB1, 0x78, 0x24, 0x69, 0xAD, 0x19, 0xBF, 0xFD, 0xCD, 0x4A, 0xEA, 0x87, 0x91, 0xA8, 0x66, 0x82, 0x50, 0x0F, 0x99, 0x45, 0xF2, 0xD5, 0x9B, 0x94, 0x7D, 0xCE, 0xDB, 0xB9, 0x52, 0xE5, 0xF4, 0x01, 0x7F, 0xD4, 0x15, 0x2D, 0x3F, 0x1D, 0xA7, 0xC2, 0xFA, 0x40, 0xE8, 0xA0, 0x55, 0x6C, 0xF7, 0x1B, 0x58, 0x85, 0x56, 0x9E, 0xEC, 0x97, 0x23, 0xF0, 0x4D, 0xD0, 0xF8, 0x2A, 0x49, 0xB4, 0x76, 0x54, 0xDF]
def Fun_0x1d():
    for i in range(len(input)):
        for j in range(len(byte_423D80)):
            if byte_423D80[j] == input[i]:
                input[i] = j
                break



byte_423780 = [0x38, 0x5A, 0xC7, 0x98, 0x15, 0x6A, 0xC9, 0x28, 0x33, 0xEA, 0xF4, 0xD9, 0xDB, 0x77, 0xB8, 0x49, 0x1B, 0x79, 0xF5, 0xFD, 0x3E, 0xA2, 0xDE, 0x17, 0xC4, 0x5E, 0xE5, 0x11, 0xB6, 0x1D, 0x86, 0xF9, 0x90, 0x78, 0x8A, 0x14, 0x12, 0xB1, 0xC2, 0x21, 0xF1, 0x02, 0x58, 0xA1, 0x23, 0x0C, 0xAD, 0xA5, 0x50, 0x48, 0x1E, 0x6D, 0xF8, 0x96, 0x9D, 0x19, 0x00, 0xBD, 0x26, 0xCE, 0xA7, 0x24, 0x2E, 0x39, 0x7B, 0xFA, 0x5F, 0xCC, 0x1A, 0x0B, 0x40, 0x0F, 0x4B, 0x82, 0xE2, 0x97, 0x10, 0x2A, 0xFC, 0x3B, 0xB2, 0x66, 0x27, 0x54, 0x07, 0xE3, 0x08, 0xA3, 0xA6, 0xED, 0x62, 0x13, 0x9C, 0x20, 0x01, 0x92, 0xE8, 0xAE, 0xBE, 0xE1, 0x0A, 0x41, 0x94, 0x80, 0xA9, 0x2F, 0x29, 0x70, 0x35, 0x16, 0xF7, 0x6B, 0xFE, 0x9E, 0x0D, 0xD3, 0x7F, 0x1F, 0xA0, 0x32, 0xD2, 0x52, 0x05, 0x76, 0x89, 0x9B, 0x7A, 0x8F, 0x99, 0xEF, 0xCF, 0x51, 0x0E, 0xEC, 0x59, 0x5C, 0x37, 0xD5, 0x8E, 0x31, 0x34, 0x2D, 0x93, 0x25, 0x1C, 0xC8, 0x5B, 0x47, 0x9F, 0x03, 0x67, 0x7E, 0x42, 0x7D, 0x3A, 0xAA, 0x57, 0xDA, 0x9A, 0xAB, 0x74, 0x72, 0xE4, 0xB7, 0x5D, 0xCD, 0x87, 0x46, 0x2B, 0x43, 0xF3, 0xD0, 0x85, 0x55, 0xBB, 0xD4, 0xC6, 0x61, 0x56, 0x04, 0x65, 0x7C, 0x88, 0xC3, 0x73, 0xBC, 0xEB, 0xDD, 0x4D, 0xE0, 0xE6, 0xC0, 0x63, 0x8D, 0xF2, 0x81, 0xF6, 0xA8, 0x3D, 0x3F, 0xA4, 0xE9, 0x4A, 0xB5, 0xF0, 0xCA, 0x8B, 0x2C, 0xD7, 0xAC, 0xC5, 0xC1, 0xBF, 0x53, 0xD1, 0x6F, 0x06, 0xE7, 0xD6, 0x09, 0x95, 0x44, 0x71, 0xB9, 0x83, 0x4C, 0x22, 0xAF, 0xB4, 0x75, 0x36, 0x30, 0xCB, 0xEE, 0x91, 0x45, 0x8C, 0x4E, 0x6E, 0x6C, 0x4F, 0x84, 0xBA, 0xFF, 0x64, 0xB3, 0x60, 0xFB, 0xB0, 0x18, 0xD8, 0xDF, 0x3C, 0x68, 0xDC, 0x69]
def Fun_0x17():
    for i in range(len(input)):
        for j in range(len(byte_423780)):
            if byte_423780[j] == input[i]:
                input[i] = j
                break

byte_423380 = [0x91, 0x67, 0x1A, 0xBE, 0xAB, 0xC2, 0x85, 0xD5, 0xDA, 0xCC, 0xF7, 0x5B, 0x54, 0x61, 0x05, 0xDF, 0x02, 0x70, 0x65, 0x69, 0x9A, 0x7A, 0x09, 0x92, 0x5D, 0x2A, 0xA7, 0x37, 0xFF, 0x19, 0xE6, 0x99, 0xF3, 0x1E, 0xBD, 0x82, 0x48, 0x3C, 0xE8, 0xC8, 0x66, 0x17, 0xB7, 0xA9, 0xC5, 0x4E, 0x33, 0x84, 0x45, 0xD3, 0x8B, 0x49, 0x50, 0x43, 0x8F, 0xCD, 0x73, 0x29, 0x04, 0xDC, 0x01, 0x0C, 0xDD, 0x2E, 0xFB, 0x6E, 0x0F, 0x24, 0x57, 0xE9, 0xC9, 0x7D, 0xB3, 0x40, 0x4B, 0x56, 0x6C, 0x68, 0xE2, 0x22, 0xF6, 0x80, 0xAA, 0x95, 0xD4, 0x97, 0x94, 0x21, 0x53, 0xD1, 0xE3, 0x59, 0xD2, 0xED, 0x41, 0x4D, 0x74, 0xA3, 0xA0, 0x32, 0x0D, 0xFC, 0x46, 0x34, 0xFA, 0xB1, 0x5E, 0xC6, 0x71, 0xC0, 0xE0, 0x3F, 0x13, 0x12, 0xD7, 0xEE, 0xF8, 0x26, 0xE1, 0x25, 0x88, 0x77, 0xB0, 0x8D, 0x6A, 0xEA, 0x0E, 0xD6, 0x3E, 0x03, 0x64, 0xBF, 0x8C, 0x96, 0xD9, 0xA4, 0x42, 0xAD, 0xFD, 0x16, 0x5A, 0xE4, 0x06, 0x9D, 0x07, 0x87, 0x5F, 0xAF, 0xDB, 0xC1, 0x93, 0x1C, 0xF1, 0xDE, 0xA6, 0x3A, 0xF4, 0x2C, 0x1B, 0x39, 0xE7, 0x4A, 0xC7, 0x35, 0xFE, 0x0A, 0x62, 0xF0, 0xCA, 0xEC, 0x27, 0x52, 0x23, 0x7F, 0xA5, 0x79, 0x7C, 0x75, 0x86, 0xEB, 0x60, 0xA8, 0xF5, 0x1F, 0x20, 0xC3, 0x63, 0x5C, 0x72, 0x18, 0xE5, 0x51, 0xAC, 0xB9, 0x90, 0x9F, 0x4C, 0xB2, 0xCB, 0x00, 0x6F, 0x28, 0xA1, 0xB6, 0x9B, 0xD0, 0x7B, 0x36, 0x4F, 0x9C, 0xCF, 0x98, 0x8A, 0x0B, 0x78, 0xB4, 0x7E, 0x2B, 0xEF, 0x58, 0xB5, 0xBA, 0x55, 0xB8, 0x10, 0x2F, 0x44, 0xAE, 0x89, 0x08, 0xC4, 0x3B, 0x9E, 0xF9, 0x6D, 0xF2, 0x15, 0x1D, 0x30, 0x47, 0x8E, 0x31, 0x2D, 0xD8, 0x6B, 0x3D, 0x11, 0x14, 0xA2, 0x83, 0xCE, 0xBB, 0x81, 0xBC, 0x76, 0x38]
def Fun_0x13():
    for i in range(len(input)):
        for j in range(len(byte_423380)):
            if byte_423380[j] == input[i]:
                input[i] = j
                break

byte_423180 = [0xE8, 0x22, 0x64, 0x9F, 0xC5, 0xD5, 0x25, 0xC9, 0x5D, 0xDF, 0xA1, 0x74, 0xCB, 0x57, 0xF7, 0xF0, 0xBD, 0x56, 0xFF, 0x33, 0x79, 0xFE, 0x87, 0xB6, 0xB1, 0x54, 0x10, 0x95, 0x8A, 0xEC, 0x7B, 0x48, 0x84, 0x3D, 0x30, 0xEF, 0x86, 0xFA, 0x97, 0x1C, 0xDC, 0xA9, 0x5A, 0xF3, 0x67, 0x18, 0x83, 0x72, 0x06, 0xB9, 0xF5, 0x05, 0x68, 0x59, 0xF2, 0xE4, 0x88, 0x5E, 0x14, 0x17, 0x11, 0x9C, 0xAB, 0xDE, 0xEB, 0x7D, 0x62, 0x9B, 0xD6, 0xF4, 0x01, 0x29, 0xBC, 0xC0, 0x69, 0xA2, 0x2B, 0x0D, 0x1D, 0x98, 0x6A, 0xBE, 0x65, 0x09, 0xF8, 0x96, 0xB4, 0x6E, 0x63, 0xE3, 0x34, 0x2D, 0xCE, 0x0A, 0xCD, 0xAA, 0x21, 0xCC, 0xE7, 0xA5, 0xDB, 0xD8, 0x03, 0xDD, 0xB2, 0x1F, 0x9D, 0x9E, 0x0E, 0x8F, 0x8B, 0xCA, 0x92, 0x0B, 0xA7, 0x5B, 0xD2, 0xCF, 0x47, 0x07, 0x04, 0xAE, 0x3B, 0xA8, 0x7C, 0x73, 0xF9, 0x35, 0xEE, 0x7A, 0xB0, 0xBA, 0x85, 0x46, 0x3E, 0x81, 0xC7, 0x40, 0x37, 0x15, 0x3A, 0x19, 0xE0, 0x1E, 0x28, 0x4A, 0x4F, 0x8C, 0xD4, 0x51, 0x2E, 0x94, 0x89, 0x2A, 0x0F, 0x7E, 0xE1, 0xC8, 0x5F, 0x4E, 0x6D, 0xF6, 0x49, 0xB8, 0x55, 0x60, 0x82, 0x20, 0x36, 0xC1, 0x0C, 0x1B, 0xC4, 0x00, 0xE5, 0xA3, 0x2C, 0xE9, 0xC2, 0xF1, 0x23, 0x3F, 0xC3, 0xB5, 0x8D, 0xD7, 0x42, 0xFC, 0x50, 0x13, 0xBB, 0x61, 0x9A, 0x44, 0xE6, 0x91, 0x2F, 0x70, 0xC6, 0x6F, 0xD1, 0x27, 0x43, 0x08, 0xDA, 0xFD, 0x52, 0x71, 0x77, 0xED, 0xE2, 0xAD, 0x16, 0x8E, 0x12, 0x4C, 0x31, 0x3C, 0x39, 0x78, 0x90, 0xBF, 0x1A, 0x76, 0x75, 0x41, 0x99, 0xD0, 0x80, 0xB7, 0x66, 0x24, 0xD3, 0x7F, 0x4B, 0x45, 0x5C, 0x53, 0x4D, 0x26, 0x32, 0xA0, 0xFB, 0xB3, 0x38, 0x6B, 0xAF, 0xA6, 0xD9, 0x02, 0xA4, 0xEA, 0x6C, 0xAC, 0x58, 0x93]
def Fun_0x11():
    for i in range(len(input)):
        for j in range(len(byte_423180)):
            if byte_423180[j] == input[i]:
                input[i] = j
                break

byte_422D80 = [0xB0, 0x28, 0x0B, 0x89, 0x4B, 0xA4, 0xBE, 0x1A, 0x8F, 0x6C, 0xCF, 0xB2, 0xB5, 0xFE, 0xFB, 0x59, 0x2D, 0x29, 0x39, 0x62, 0x97, 0xAA, 0xD7, 0x7D, 0x94, 0x2C, 0xFC, 0x5D, 0xB4, 0x7C, 0x8A, 0x82, 0xD3, 0xA7, 0xBA, 0xDF, 0x21, 0xE6, 0xA2, 0xD0, 0xE8, 0xF0, 0x67, 0x3A, 0xB9, 0x98, 0xF9, 0xAE, 0xD1, 0x56, 0xD8, 0xCA, 0x10, 0xEA, 0x92, 0xA8, 0x75, 0x7E, 0x65, 0xA9, 0xAF, 0x51, 0xC9, 0x8E, 0xD4, 0x77, 0xE4, 0x49, 0x06, 0x61, 0x9E, 0x24, 0xD9, 0x9B, 0x11, 0x05, 0x1D, 0x96, 0x9A, 0xB1, 0xE0, 0x83, 0xE1, 0x1C, 0xCD, 0xF3, 0x38, 0xB3, 0x57, 0x50, 0xF4, 0xAC, 0xEB, 0x14, 0xA5, 0x46, 0xF6, 0x93, 0xAD, 0x7B, 0x30, 0xEF, 0x79, 0x17, 0x47, 0xDA, 0xC0, 0xDD, 0xDE, 0xDC, 0x5A, 0x76, 0x3B, 0x31, 0x0D, 0x0E, 0x86, 0xF1, 0x71, 0xFA, 0x0C, 0x00, 0xA3, 0xBF, 0x64, 0x37, 0x22, 0xD2, 0x69, 0x5C, 0xC6, 0x16, 0x9F, 0x5E, 0x7A, 0x1E, 0x27, 0x60, 0x6E, 0xF8, 0x8C, 0xEE, 0xC2, 0x74, 0x81, 0x8B, 0x33, 0x03, 0xBD, 0x2A, 0x0A, 0x68, 0x6B, 0x3F, 0x4C, 0xC3, 0x15, 0x04, 0x3D, 0x63, 0xF5, 0xAB, 0xCC, 0x3C, 0x53, 0x20, 0x66, 0xC4, 0xC1, 0x23, 0xE7, 0x25, 0x55, 0xC7, 0xED, 0xB7, 0xBC, 0xCB, 0x8D, 0x09, 0xCE, 0x52, 0xBB, 0xE2, 0xC5, 0xB6, 0x26, 0x12, 0x2F, 0x99, 0x58, 0x40, 0x6D, 0xA1, 0x3E, 0x48, 0x85, 0xA6, 0xF2, 0x0F, 0x43, 0x78, 0xB8, 0x01, 0xE5, 0xD5, 0x6F, 0x4E, 0xF7, 0x13, 0x42, 0xEC, 0x45, 0x2B, 0x4F, 0x36, 0xDB, 0x9C, 0xE3, 0x44, 0x34, 0x84, 0x73, 0x2E, 0x7F, 0xFD, 0x91, 0x41, 0xD6, 0x95, 0x18, 0xFF, 0x70, 0xC8, 0x02, 0x5F, 0x08, 0x1B, 0x6A, 0x5B, 0x19, 0xA0, 0x4D, 0x35, 0x54, 0xE9, 0x32, 0x88, 0x72, 0x07, 0x87, 0x90, 0x4A, 0x80, 0x1F, 0x9D]
def Fun_0xd():
    for i in range(len(input)):
        for j in range(len(byte_422D80)):
            if byte_422D80[j] == input[i]:
                input[i] = j
                break

byte_422B80 = [0x38, 0xD9, 0xDA, 0xE6, 0xB5, 0xF1, 0x0B, 0x93, 0x0C, 0x58, 0x0D, 0xAE, 0x0A, 0x85, 0x2A, 0x50, 0xC2, 0xBF, 0xD4, 0x28, 0x52, 0xC4, 0x4F, 0xE1, 0x44, 0xE0, 0xA2, 0x70, 0x36, 0x65, 0x4B, 0x41, 0x9D, 0x5F, 0x05, 0x7C, 0xF7, 0xD7, 0x99, 0x8B, 0xCC, 0xCE, 0x16, 0xBE, 0xB6, 0xC5, 0x8F, 0x79, 0xC7, 0x20, 0x7E, 0xF4, 0xF3, 0x2E, 0x4A, 0x89, 0xD6, 0x0F, 0x6E, 0xB0, 0x61, 0xB1, 0x6D, 0x19, 0x73, 0x03, 0x74, 0xA1, 0x40, 0xEC, 0xC0, 0x57, 0x94, 0x7A, 0x66, 0xD5, 0xEA, 0x17, 0x6A, 0x84, 0x37, 0xED, 0xF6, 0x13, 0x31, 0x5B, 0x82, 0x1E, 0xFC, 0x92, 0xE2, 0x42, 0x86, 0xBA, 0xE3, 0x91, 0x7F, 0x67, 0x5C, 0x98, 0x15, 0x22, 0x8D, 0x80, 0x04, 0xE4, 0x25, 0x09, 0xA0, 0xAD, 0x63, 0xE5, 0xB4, 0x9A, 0x3C, 0xA3, 0x3A, 0x69, 0xF8, 0xCD, 0xBC, 0x88, 0x55, 0xB2, 0xBD, 0x6B, 0x77, 0x71, 0xB3, 0xD3, 0x90, 0x75, 0x06, 0x49, 0xC3, 0x32, 0x4D, 0x1D, 0xA8, 0xAA, 0xFB, 0x7B, 0x7D, 0x2B, 0xA6, 0x34, 0x72, 0x47, 0xF0, 0x2F, 0x9C, 0x08, 0x00, 0x14, 0x8C, 0x26, 0x5E, 0x87, 0xD1, 0xCF, 0xC9, 0x18, 0x51, 0x23, 0xCB, 0xF5, 0x1C, 0x9F, 0x97, 0xF9, 0xBB, 0xA7, 0x39, 0x45, 0x02, 0xFD, 0x46, 0x8A, 0x54, 0xA4, 0x8E, 0x9E, 0x68, 0x96, 0x0E, 0x78, 0xB8, 0x3D, 0x11, 0x64, 0xAF, 0x10, 0xDE, 0x6C, 0x60, 0x5A, 0x76, 0x1A, 0xE9, 0xC1, 0x3E, 0xCA, 0x9B, 0x27, 0x30, 0xEF, 0xFF, 0x07, 0xD2, 0xB9, 0x2D, 0xD0, 0xEE, 0x83, 0xAB, 0xF2, 0x4C, 0xA5, 0x21, 0x62, 0x81, 0x33, 0x1B, 0xD8, 0x6F, 0xAC, 0x3B, 0x5D, 0xE8, 0xFA, 0x3F, 0xDB, 0x95, 0xE7, 0x59, 0x12, 0x48, 0x35, 0xC6, 0x2C, 0x4E, 0x01, 0xDD, 0x43, 0x29, 0xDC, 0x24, 0x1F, 0xB7, 0xA9, 0xEB, 0xC8, 0xFE, 0x56, 0xDF, 0x53]
def Fun_0xb():
    for i in range(len(input)):
        for j in range(len(byte_422B80)):
            if byte_422B80[j] == input[i]:
                input[i] = j
                break

byte_422780 = [0x0F, 0xA5, 0xBA, 0x03, 0xF9, 0x69, 0x2A, 0xD7, 0xEA, 0xB5, 0xFC, 0xA1, 0x39, 0x20, 0x68, 0x72, 0x25, 0xB2, 0x6C, 0xAD, 0x88, 0x51, 0x73, 0xEB, 0xCF, 0x13, 0xDE, 0x7C, 0x6D, 0x38, 0x05, 0x09, 0xC2, 0x96, 0x1F, 0x7F, 0x37, 0x4A, 0xC9, 0xE7, 0x6A, 0xB0, 0x59, 0xF7, 0xD2, 0xB9, 0x16, 0xC8, 0xEE, 0xA9, 0x18, 0x80, 0xAC, 0xE3, 0x9E, 0x6F, 0x3C, 0x2F, 0x3E, 0x9A, 0xBE, 0x1D, 0xB4, 0x7B, 0x7D, 0x32, 0x6B, 0x74, 0xC5, 0xC0, 0xC7, 0xD1, 0x29, 0x98, 0xDD, 0xB6, 0x0E, 0x4D, 0xBF, 0x79, 0x0D, 0xDA, 0x7A, 0x17, 0x71, 0x43, 0x87, 0xFF, 0xDC, 0xC6, 0x12, 0xE9, 0x67, 0x2D, 0x70, 0x9F, 0x95, 0x30, 0x26, 0x24, 0x2B, 0xA8, 0xA2, 0xD8, 0x3B, 0x31, 0xA0, 0x3D, 0x4B, 0x90, 0x60, 0x34, 0x75, 0xE8, 0x5D, 0xF4, 0x85, 0xF3, 0xFE, 0x35, 0xCB, 0xB8, 0x02, 0x50, 0xB1, 0xF1, 0x1A, 0x1B, 0x21, 0xCD, 0xC4, 0x7E, 0xED, 0x07, 0xD9, 0xD6, 0x44, 0x15, 0x8E, 0x49, 0xB3, 0x97, 0xE6, 0x63, 0xB7, 0xEF, 0x3A, 0x8F, 0xF2, 0x53, 0x10, 0x77, 0x86, 0xF8, 0x8A, 0x28, 0x3F, 0xD4, 0x4C, 0xE5, 0x82, 0x83, 0xEC, 0x62, 0x89, 0xDF, 0xC3, 0x14, 0xCA, 0xA3, 0x5F, 0x64, 0x47, 0xFD, 0x00, 0x84, 0x66, 0xA7, 0x5A, 0x0C, 0x01, 0xD5, 0x5B, 0x0A, 0x4F, 0x27, 0x78, 0x0B, 0x2E, 0x48, 0x36, 0xFA, 0x08, 0x56, 0xE0, 0xA6, 0xC1, 0x5C, 0x8B, 0x41, 0x06, 0xBB, 0x52, 0x93, 0xAF, 0x2C, 0x5E, 0xF6, 0x61, 0xF0, 0xAB, 0x91, 0x45, 0x04, 0xBD, 0xCC, 0xE4, 0x65, 0x9D, 0x92, 0xCE, 0x40, 0xAE, 0x76, 0x9B, 0x9C, 0xAA, 0x54, 0xD0, 0x1C, 0x81, 0x4E, 0x57, 0x55, 0x23, 0x6E, 0x1E, 0x99, 0xDB, 0xFB, 0xA4, 0x22, 0x19, 0x58, 0x11, 0x8D, 0x94, 0xD3, 0xE2, 0x8C, 0xF5, 0x42, 0x46, 0xBC, 0x33, 0xE1]
def Fun_0x7():
    for i in range(len(input)):
        for j in range(len(byte_422780)):
            if byte_422780[j] == input[i]:
                input[i] = j
                break

byte_422580 = [0x00, 0x74, 0x59, 0xC6, 0xAC, 0xD3, 0xC1, 0xA0, 0x88, 0x3F, 0x1C, 0x28, 0x17, 0x22, 0xC5, 0x38, 0xF9, 0x1B, 0x21, 0x49, 0x99, 0xAF, 0xD6, 0x95, 0xA4, 0x9D, 0x5D, 0x5B, 0x73, 0xFE, 0xC9, 0x9A, 0x4C, 0xB4, 0x27, 0x5E, 0x71, 0x25, 0xE2, 0x90, 0xC0, 0x62, 0x5F, 0x48, 0x77, 0xE0, 0xF2, 0x8E, 0x40, 0xC7, 0x79, 0x1A, 0xDC, 0xF3, 0x01, 0xB6, 0xD8, 0xB5, 0x67, 0x1E, 0x85, 0x12, 0x68, 0x87, 0xD0, 0x30, 0xEB, 0x2F, 0x50, 0xCF, 0xEE, 0xDD, 0xFB, 0xE6, 0xA5, 0x69, 0x05, 0x75, 0xB7, 0xEF, 0x70, 0x53, 0xFF, 0xBA, 0x80, 0x41, 0x9B, 0xA1, 0x39, 0xF8, 0x65, 0x1F, 0x7A, 0x51, 0x98, 0xAD, 0x02, 0x13, 0x18, 0xC3, 0x31, 0x89, 0xCD, 0xCA, 0x91, 0xD1, 0x78, 0x57, 0x47, 0xB8, 0x54, 0x9F, 0x96, 0x04, 0x23, 0x2B, 0xE5, 0x46, 0x29, 0x7C, 0x76, 0x82, 0xBC, 0xFC, 0x6E, 0xEC, 0xED, 0x64, 0x4A, 0x26, 0x34, 0x5C, 0x19, 0x55, 0xFD, 0x6D, 0xFA, 0x7E, 0xB2, 0xD4, 0xF1, 0xF6, 0xE4, 0x60, 0xB0, 0x52, 0x9E, 0x8F, 0xBB, 0x08, 0x3B, 0x97, 0xE8, 0x10, 0x6C, 0x44, 0x3A, 0x36, 0x35, 0x03, 0xC4, 0x81, 0x9C, 0xAB, 0xCB, 0x66, 0xAA, 0x37, 0xA2, 0xD2, 0xE1, 0xE9, 0x7B, 0x14, 0x8D, 0xD9, 0xF5, 0x0B, 0xC2, 0x07, 0xA8, 0x0D, 0xA3, 0x0A, 0x84, 0x6B, 0x2C, 0xEA, 0x0C, 0xAE, 0x7D, 0x6F, 0xD7, 0xE7, 0xC8, 0x3C, 0x45, 0xCC, 0x58, 0xB9, 0x3D, 0x33, 0x4E, 0x4B, 0x8C, 0xCE, 0x72, 0x6A, 0x8B, 0x2D, 0x24, 0x11, 0xDF, 0x5A, 0x2E, 0x92, 0xDA, 0x86, 0x94, 0xA7, 0xD5, 0x4F, 0x2A, 0xB3, 0x63, 0x61, 0xE3, 0xDE, 0x43, 0x1D, 0xBF, 0x15, 0x32, 0xBE, 0x16, 0x3E, 0x93, 0x7F, 0x83, 0x56, 0x06, 0xF7, 0x8A, 0x20, 0xBD, 0x0E, 0xA6, 0xDB, 0x0F, 0xB1, 0x42, 0xF0, 0x09, 0x4D, 0xA9, 0xF4]

def Fun_0x5():
    for i in range(len(input)):
        for j in range(len(byte_422580)):
            if byte_422580[j] == input[i]:
                input[i] = j
                break

byte_422380 = [0x45, 0x1F, 0x63, 0x81, 0xE6, 0xAD, 0x4F, 0xD3, 0xC0, 0x15, 0x69, 0x8F, 0x0D, 0x31, 0x0C, 0xB0, 0xF1, 0x2E, 0x98, 0xC1, 0xC2, 0x96, 0xB2, 0xEB, 0xBF, 0xDF, 0x17, 0xF4, 0x7F, 0xE5, 0x66, 0x73, 0xD8, 0x56, 0x46, 0x20, 0x9C, 0x77, 0x3D, 0x72, 0xA3, 0x91, 0x49, 0x68, 0x4C, 0x1E, 0xAE, 0x06, 0x7A, 0x94, 0xDD, 0x52, 0x55, 0x2C, 0xB8, 0x42, 0x79, 0xFE, 0x38, 0xEF, 0x8B, 0xF7, 0xAC, 0xDC, 0xFF, 0x78, 0x34, 0x70, 0xA9, 0xCE, 0x3F, 0x0E, 0x11, 0x43, 0x5B, 0xF8, 0xAF, 0xD0, 0xFA, 0x33, 0xBA, 0xCF, 0x4A, 0xC9, 0x88, 0x4E, 0x80, 0x10, 0x85, 0x37, 0x12, 0xAB, 0xE1, 0x61, 0xB7, 0x3E, 0x4D, 0x19, 0x3A, 0x04, 0x8C, 0x92, 0x0B, 0xE7, 0x3C, 0xEA, 0xC7, 0x16, 0x35, 0xB1, 0xA7, 0x8E, 0x40, 0x9F, 0xB6, 0xB5, 0x25, 0xA0, 0x5A, 0x30, 0x7D, 0xA2, 0x1A, 0x64, 0xC5, 0x6D, 0x74, 0x82, 0x08, 0x7E, 0xD2, 0xF6, 0xAA, 0xDA, 0xED, 0x4B, 0x6E, 0xE8, 0xE9, 0xE2, 0xD4, 0x71, 0xB9, 0x09, 0x84, 0x3B, 0xC4, 0x1C, 0x60, 0xFD, 0x22, 0x99, 0x39, 0x97, 0x18, 0x89, 0x7C, 0xA4, 0x27, 0xBD, 0x0F, 0xCC, 0x95, 0xF5, 0xB3, 0x65, 0x6B, 0x8A, 0x58, 0x36, 0xBB, 0x9E, 0x75, 0xD1, 0x03, 0x9D, 0x6A, 0x6C, 0x53, 0x05, 0xB4, 0xE4, 0xEE, 0x67, 0x87, 0x7B, 0x32, 0x2D, 0x24, 0x2A, 0x59, 0xEC, 0x0A, 0xDB, 0x21, 0x07, 0x23, 0x50, 0x02, 0x41, 0xF2, 0x83, 0xD9, 0x26, 0xBC, 0x6F, 0x86, 0xA6, 0x93, 0xF9, 0xC8, 0xD6, 0xA5, 0x1D, 0xE3, 0xE0, 0xFC, 0xCA, 0x1B, 0x5E, 0x8D, 0x2F, 0x5C, 0xBE, 0x47, 0xA8, 0x44, 0x57, 0x54, 0x48, 0xC3, 0x00, 0x62, 0x5D, 0xCB, 0xD7, 0x76, 0xCD, 0x28, 0xD5, 0x14, 0x90, 0x13, 0xDE, 0x5F, 0xF0, 0x01, 0x2B, 0xC6, 0x29, 0x9A, 0x9B, 0x51, 0xF3, 0xFB, 0xA1]
def Fun_0x3():
    for i in range(len(input)):
        for j in range(len(byte_422380)):
            if byte_422380[j] == input[i]:
                input[i] = j
                break

byte_422280 = [0x7A, 0x91, 0x9F, 0x23, 0x71, 0xD1, 0x63, 0xDB, 0x59, 0x0A, 0xEC, 0x69, 0xEE, 0x76, 0x5D, 0x64, 0x37, 0x42, 0x8C, 0x0B, 0x3C, 0x5C, 0x80, 0xAD, 0x6A, 0x03, 0x43, 0x93, 0xBC, 0xBF, 0xE3, 0xAF, 0x5A, 0x8A, 0x65, 0x0D, 0x31, 0xDF, 0x3E, 0xA7, 0xE4, 0xDD, 0xB4, 0xB0, 0x56, 0x1C, 0x12, 0xA4, 0x9E, 0xD8, 0x3D, 0x81, 0x60, 0x9A, 0xCB, 0xFA, 0xB1, 0xE0, 0xD3, 0xF4, 0xA2, 0x26, 0x68, 0x90, 0x4B, 0x45, 0x85, 0x20, 0x16, 0xDE, 0xED, 0x4C, 0x6F, 0x34, 0xDC, 0xBE, 0xD2, 0x46, 0x33, 0x14, 0x77, 0xC6, 0xCD, 0xF0, 0xC5, 0xAC, 0x1F, 0xD0, 0x95, 0x97, 0x3F, 0xD7, 0x52, 0xAE, 0xB9, 0xC9, 0x0C, 0xCA, 0x4E, 0xF1, 0xB7, 0x39, 0x7F, 0x27, 0x2B, 0x40, 0x4A, 0x51, 0xA1, 0xCC, 0xCE, 0x6E, 0x70, 0xFF, 0x0E, 0xEF, 0x8E, 0x25, 0xB3, 0x5E, 0x6C, 0xAB, 0x02, 0x49, 0xE9, 0x9B, 0x36, 0x13, 0x9C, 0x04, 0x35, 0xC0, 0xFB, 0x3A, 0x67, 0xB6, 0x9D, 0xC2, 0x73, 0xB5, 0x6D, 0xCF, 0x83, 0x2C, 0x01, 0xC1, 0x10, 0x6B, 0x79, 0x87, 0x5B, 0x57, 0x47, 0xE5, 0x15, 0xF7, 0xA5, 0x74, 0xAA, 0x53, 0x7D, 0x2E, 0xD5, 0xA3, 0x19, 0xF5, 0x2D, 0xFD, 0x61, 0x8D, 0xC8, 0x1B, 0xC3, 0xDA, 0xF6, 0x72, 0x54, 0x5F, 0x1E, 0xE8, 0x17, 0x50, 0xB2, 0xE7, 0x0F, 0x7E, 0x55, 0xBD, 0x86, 0x00, 0x78, 0x94, 0x92, 0x09, 0x2F, 0xD6, 0xD9, 0xF3, 0x29, 0xE6, 0x24, 0x32, 0x66, 0x22, 0x41, 0xC4, 0x7C, 0x05, 0x98, 0x44, 0x4F, 0x99, 0xA9, 0xE1, 0x8F, 0x08, 0x1A, 0x2A, 0x11, 0xEA, 0x3B, 0xE2, 0x38, 0xB8, 0x18, 0xF9, 0xD4, 0xC7, 0x62, 0x7B, 0x75, 0x58, 0x96, 0x28, 0xEB, 0x06, 0x84, 0x89, 0x48, 0x82, 0x88, 0xA6, 0xFE, 0xA0, 0xF2, 0xF8, 0x1D, 0x8B, 0xFC, 0xA8, 0x21, 0x30, 0xBB, 0x07, 0xBA, 0x4D]
def Fun_0x2():
    for i in range(len(input)):
        for j in range(len(byte_422280)):
            if byte_422280[j] == input[i]:
                input[i] = j
                break


Fun_0x1d()
Fun_0x17()
Fun_0x13()
Fun_0x11()
Fun_0xd()
Fun_0xb()
Fun_0x7()
Fun_0x5()
Fun_0x3()
Fun_0x2()

for i in range(len(input)):
    print(chr(input[i]),end = "")