suctf2018-simpleformat

Author Avatar
Xzhah 6月 09, 2018
  • 在其它设备中阅读本文章

再一次感谢我队师傅带我，进了前十，记录一些东西方便以后回顾

思路

格式化字符串

printf(“%1$2$s%3$n”,a1,a2,a3)的意思就是输出a1，\表示宽度，如果a1字符串长度大于a2，输出a1。如果<=a2的值，就输出a2宽度的a1。最后把输出的字符串宽度送到a3指向的内存

所以这道题思路就是一个18元1次方程，word_6271A0[x]是我们的输入

最后对比输出字符串宽度

脚本

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
#-*- coding:utf-8 -*-
from z3 import *
import re
def get_models(s):
	while s.check() == sat:
		m = s.model()
		yield m
		s.add(Or([sym() != m[sym] for sym in m.decls()]))
foramat1='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat2='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%20$n'
foramat3='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat4='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat5='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat6='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat7='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%20$'
foramat8='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat9='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat10='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat11='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat12='%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat13='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat14='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat15='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat16='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat17='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*5$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
foramat18='%1$*2$s%1$*2$s%1$*2$s%1$*2$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*3$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*4$s%1$*5$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*6$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*7$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*8$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*9$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*10$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*11$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*12$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*13$s%1$*14$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*15$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*16$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*17$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*18$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%1$*19$s%20$n'
dist=[0x00535908, 0x0042528A, 0x0059E457, 0x00685E38, 0x0078BD81, 0x006B923E, 0x0071C428, 0x006F90FC, 0x00601E78, 0x006C8D74, 0x006B6073, 0x0068DFDB, 0x005621FA, 0x007A4975, 0x006225D7, 0x00654B72, 0x006A3321, 0x006652DC]
s=Solver()
data=[Int('flag%d'%i) for i in range(20)]
def solve1(fmti,x):
	total=0
	for s1 in fmti[1:-1]:
		m=re.match('1\$\*([0-9]*)\$s',s1)
		intt=int(m.group(1),10)
		total=total+If(data[intt]<127,127,data[intt])
	s.add(total==dist[x])
solve1(foramat1.split('%'),0)
solve1(foramat2.split('%'),1)
solve1(foramat3.split('%'),2)
solve1(foramat4.split('%'),3)
solve1(foramat5.split('%'),4)
solve1(foramat6.split('%'),5)
solve1(foramat7.split('%'),6)
solve1(foramat8.split('%'),7)
solve1(foramat9.split('%'),8)
solve1(foramat10.split('%'),9)
solve1(foramat11.split('%'),10)
solve1(foramat12.split('%'),11)
solve1(foramat13.split('%'),12)
solve1(foramat14.split('%'),13)
solve1(foramat15.split('%'),14)
solve1(foramat16.split('%'),15)
solve1(foramat17.split('%'),16)
solve1(foramat18.split('%'),17)
print s.check()
res = s.model()

def unpack(v):
	s = ''
	for i in range(4):
		x = v & 0xff
		v >>= 8
		s = s + chr(x)
	return s
for m in get_models(s):
	a = ''
	for i in range(2,20):
		a += unpack(m[data[i]].as_long())

	print a

#SUCTF{s1mpl3_prin7f_l1near_f0rmulas}

结果