2022DASCTF X SU-Crypto-FlowerCipher之暴力暴力求解法(z3约束器)

题目

from pickle import LONG1
from secret import flag
import random

# flag = b'flag{%s}' % md5(something).hexdigest()
# note that md5 only have characters 'abcdef' and digits

def Flower(x, key):
    flower = random.randint(0, 4096)
    return x * (key ** 3 + flower)

flag = flag[5:-1]
rounds = len(flag)

L, R = 1, 0
for i in range(rounds):
    L, R = R + Flower(L, flag[i]), L

print(L, R)
'''
L=15720197268945348388429429351303006925387388927292304717594511259390194100850889852747653387197205392431053069043632340374252629529419776874410817927770922310808632581666181899
R=139721425176294317602347104909475448503147767726747922243703132013053043430193232376860554749633894589164137720010858254771905261753520854314908256431590570426632742469003
'''

分析一下

# flag = b'flag{%s}' % md5(something).hexdigest()
# note that md5 only have characters 'abcdef' and digits

def Flower(x, key):
    flower = random.randint(0, 4096)
    return x * (key ** 3 + flower)

flag = flag[5:-1]
rounds = len(flag)

L, R = 1, 0
for i in range(rounds):
    L, R = R + Flower(L, flag[i]), L

print(L, R)
L=15720197268945348388429429351303006925387388927292304717594511259390194100850889852747653387197205392431053069043632340374252629529419776874410817927770922310808632581666181899
R=139721425176294317602347104909475448503147767726747922243703132013053043430193232376860554749633894589164137720010858254771905261753520854314908256431590570426632742469003
## L比R长几位

感觉这些条件可以把中间过程都推出来.

由于前几天才做了一道LFSR的题D3bug,用的是z3-solve求解,先列一点条件出来看看

条件

• $L0,R0=1,0$

• $L32=15720197268945348388429429351303006925387388927292304717594511259390194100850889852747653387197205392431053069043632340374252629529419776874410817927770922310808632581666181899$

• $R32=139721425176294317602347104909475448503147767726747922243703132013053043430193232376860554749633894589164137720010858254771905261753520854314908256431590570426632742469003$

• $L_n=R_{n-1}+L_{n-1}\ast (fla{g}_{n-1}^3+rando{m}_{n-1})$

• $rando{m}_n\in [0,4096]$

• f l a g n ∈ a s c i i { a b c d e f 0123456789 } flag_n\in ascii\{abcdef0123456789\} flagn​∈ascii{abcdef0123456789}

  • 因为这里abcdef与0123456789之间还隔着一些ascii字符，用一般的逻辑式怕z3识别不了，就利用了简单粗暴的逻辑表达比如 f l a g < = a s c i i { e } , f l a g > = a s c i i { 0 } 且 f l a g ≠ a s c i i { 9 → a } flag<=ascii\{e\},flag>=ascii\{0\}且flag\not=ascii\{9\rightarrow a\} flag<=ascii{e},flag>=ascii{0}且flag​=ascii{9→a}

当时就写了那么多条件,然后发现z3一直跑呀跑呀跑呀跑呀，没有任何回应.

然后后面就考虑到要加条件上去，又开始看代码：

L, R = 1, 0
for i in range(rounds):
    L, R = R + Flower(L, flag[i]), L

我们当时用了$R_n=L_{n-1}的条件，要想逆推出R_{n-1}来，继续分析一下$
$$\{\begin{array}{l}{L}_n=R_{n-1}+L_{n-1}\ast (fla{g}_{n-1}^3+rando{m}_{n-1})(1)\\ R_n=L_{n-1}(2)\end{array}$$
简单分析一下L和R的值大小可知，在n相同的情况下$L_n>R_n$

且$L_{n-1}\ast (fla{g}_{n-1}^3+rando{m}_{n-1})中含有L_{n-1}$

即我们可以用$(1)\%(2)$

即$L_n\%R_n就可以得到R_{n-1}$

加上条件

• $L_n\%R_n=R_{n-1}$

然后来编写一个超级超级超级长的z3求解代码

Solve

from z3 import *
L0=Int('L0')
L1=Int('L1')  
L2=Int('L2')  
L3=Int('L3')  
L4=Int('L4')  
L5=Int('L5')  
L6=Int('L6')  
L7=Int('L7')  
L8=Int('L8')  
L9=Int('L9')  
L10=Int('L10')
L11=Int('L11')
L12=Int('L12')
L13=Int('L13')
L14=Int('L14')
L15=Int('L15')
L16=Int('L16')
L17=Int('L17')
L18=Int('L18')
L19=Int('L19')
L20=Int('L20')
L21=Int('L21')
L22=Int('L22')
L23=Int('L23')
L24=Int('L24')
L25=Int('L25')
L26=Int('L26')
L27=Int('L27')
L28=Int('L28')
L29=Int('L29')
L30=Int('L30')
L31=Int('L31')
L32=Int('L32')
R0=Int('R0')
R1=Int('R1')
R2=Int('R2')
R3=Int('R3')
R4=Int('R4')
R5=Int('R5')
R6=Int('R6')
R7=Int('R7')
R8=Int('R8')
R9=Int('R9')
R10=Int('R10')
R11=Int('R11')
R12=Int('R12')
R13=Int('R13')
R14=Int('R14')
R15=Int('R15')
R16=Int('R16')
R17=Int('R17')
R18=Int('R18')
R19=Int('R19')
R20=Int('R20')
R21=Int('R21')
R22=Int('R22')
R23=Int('R23')
R24=Int('R24')
R25=Int('R25')
R26=Int('R26')
R27=Int('R27')
R28=Int('R28')
R29=Int('R29')
R30=Int('R30')
R31=Int('R31')
R32=Int('R32')
flag0=Int('flag0')
flag1=Int('flag1')
flag2=Int('flag2')
flag3=Int('flag3')
flag4=Int('flag4')
flag5=Int('flag5')
flag6=Int('flag6')
flag7=Int('flag7')
flag8=Int('flag8')
flag9=Int('flag9')
flag10=Int('flag10')
flag11=Int('flag11')
flag12=Int('flag12')
flag13=Int('flag13')
flag14=Int('flag14')
flag15=Int('flag15')
flag16=Int('flag16')
flag17=Int('flag17')
flag18=Int('flag18')
flag19=Int('flag19')
flag20=Int('flag20')
flag21=Int('flag21')
flag22=Int('flag22')
flag23=Int('flag23')
flag24=Int('flag24')
flag25=Int('flag25')
flag26=Int('flag26')
flag27=Int('flag27')
flag28=Int('flag28')
flag29=Int('flag29')
flag30=Int('flag30')
flag31=Int('flag31')
random0=Int('random0')
random1=Int('random1')
random2=Int('random2')
random3=Int('random3')
random4=Int('random4')
random5=Int('random5')
random6=Int('random6')
random7=Int('random7')
random8=Int('random8')
random9=Int('random9')
random10=Int('random10')
random11=Int('random11')
random12=Int('random12')
random13=Int('random13')
random14=Int('random14')
random15=Int('random15')
random16=Int('random16')
random17=Int('random17')
random18=Int('random18')
random19=Int('random19')
random20=Int('random20')
random21=Int('random21')
random22=Int('random22')
random23=Int('random23')
random24=Int('random24')
random25=Int('random25')
random26=Int('random26')
random27=Int('random27')
random28=Int('random28')
random29=Int('random29')
random30=Int('random30')
random31=Int('random31')
so=Solver()
so.add(L1==R0+(L0*(flag0**3+random0)))
so.add(L2==R1+(L1*(flag1**3+random1)))
so.add(L3==R2+(L2*(flag2**3+random2)))
so.add(L4==R3+(L3*(flag3**3+random3)))
so.add(L5==R4+(L4*(flag4**3+random4)))
so.add(L6==R5+(L5*(flag5**3+random5)))
so.add(L7==R6+(L6*(flag6**3+random6)))
so.add(L8==R7+(L7*(flag7**3+random7)))
so.add(L9==R8+(L8*(flag8**3+random8)))
so.add(L10==R9+(L9*(flag9**3+random9)))
so.add(L11==R10+(L10*(flag10**3+random10)))
so.add(L12==R11+(L11*(flag11**3+random11)))
so.add(L13==R12+(L12*(flag12**3+random12)))
so.add(L14==R13+(L13*(flag13**3+random13)))
so.add(L15==R14+(L14*(flag14**3+random14)))
so.add(L16==R15+(L15*(flag15**3+random15)))
so.add(L17==R16+(L16*(flag16**3+random16)))
so.add(L18==R17+(L17*(flag17**3+random17)))
so.add(L19==R18+(L18*(flag18**3+random18)))
so.add(L20==R19+(L19*(flag19**3+random19)))
so.add(L21==R20+(L20*(flag20**3+random20)))
so.add(L22==R21+(L21*(flag21**3+random21)))
so.add(L23==R22+(L22*(flag22**3+random22)))
so.add(L24==R23+(L23*(flag23**3+random23)))
so.add(L25==R24+(L24*(flag24**3+random24)))
so.add(L26==R25+(L25*(flag25**3+random25)))
so.add(L27==R26+(L26*(flag26**3+random26)))
so.add(L28==R27+(L27*(flag27**3+random27)))
so.add(L29==R28+(L28*(flag28**3+random28)))
so.add(L30==R29+(L29*(flag29**3+random29)))
so.add(L31==R30+(L30*(flag30**3+random30)))
so.add(L32==R31+(L31*(flag31**3+random31)))
so.add(R1==L0)
so.add(R2==L1)
so.add(R3==L2)
so.add(R4==L3)
so.add(R5==L4)
so.add(R6==L5)
so.add(R7==L6)
so.add(R8==L7)
so.add(R9==L8)
so.add(R10==L9)
so.add(R11==L10)
so.add(R12==L11)
so.add(R13==L12)
so.add(R14==L13)
so.add(R15==L14)
so.add(R16==L15)
so.add(R17==L16)
so.add(R18==L17)
so.add(R19==L18)
so.add(R20==L19)
so.add(R21==L20)
so.add(R22==L21)
so.add(R23==L22)
so.add(R24==L23)
so.add(R25==L24)
so.add(R26==L25)
so.add(R27==L26)
so.add(R28==L27)
so.add(R29==L28)
so.add(R30==L29)
so.add(R31==L30)
so.add(R32==L31)
so.add(R0==0)
so.add(L0==1)
so.add(R0==L1%R1)
so.add(R1==L2%R2)
so.add(R2==L3%R3)
so.add(R3==L4%R4)
so.add(R4==L5%R5)
so.add(R5==L6%R6)
so.add(R6==L7%R7)
so.add(R7==L8%R8)
so.add(R8==L9%R9)
so.add(R9==L10%R10)
so.add(R10==L11%R11)
so.add(R11==L12%R12)
so.add(R12==L13%R13)
so.add(R13==L14%R14)
so.add(R14==L15%R15)
so.add(R15==L16%R16)
so.add(R16==L17%R17)
so.add(R17==L18%R18)
so.add(R18==L19%R19)
so.add(R19==L20%R20)
so.add(R20==L21%R21)
so.add(R21==L22%R22)
so.add(R22==L23%R23)
so.add(R23==L24%R24)
so.add(R24==L25%R25)
so.add(R25==L26%R26)
so.add(R26==L27%R27)
so.add(R27==L28%R28)
so.add(R28==L29%R29)
so.add(R29==L30%R30)
so.add(R30==L31%R31)
so.add(R31==L32%R32)
so.add(L32==15720197268945348388429429351303006925387388927292304717594511259390194100850889852747653387197205392431053069043632340374252629529419776874410817927770922310808632581666181899)
so.add(R32==139721425176294317602347104909475448503147767726747922243703132013053043430193232376860554749633894589164137720010858254771905261753520854314908256431590570426632742469003)
so.add(random0<=4096)
so.add(random0>=0)
so.add(random1<=4096)
so.add(random1>=0)
so.add(random2<=4096)
so.add(random2>=0)
so.add(random3<=4096)
so.add(random3>=0)
so.add(random4<=4096)
so.add(random4>=0)
so.add(random5<=4096)
so.add(random5>=0)
so.add(random6<=4096)
so.add(random6>=0)
so.add(random7<=4096)
so.add(random7>=0)
so.add(random8<=4096)
so.add(random8>=0)
so.add(random9<=4096)
so.add(random9>=0)
so.add(random10<=4096)
so.add(random10>=0)
so.add(random11<=4096)
so.add(random11>=0)
so.add(random12<=4096)
so.add(random12>=0)
so.add(random13<=4096)
so.add(random13>=0)
so.add(random14<=4096)
so.add(random14>=0)
so.add(random15<=4096)
so.add(random15>=0)
so.add(random16<=4096)
so.add(random16>=0)
so.add(random17<=4096)
so.add(random17>=0)
so.add(random18<=4096)
so.add(random18>=0)
so.add(random19<=4096)
so.add(random19>=0)
so.add(random20<=4096)
so.add(random20>=0)
so.add(random21<=4096)
so.add(random21>=0)
so.add(random22<=4096)
so.add(random22>=0)
so.add(random23<=4096)
so.add(random23>=0)
so.add(random24<=4096)
so.add(random24>=0)
so.add(random25<=4096)
so.add(random25>=0)
so.add(random26<=4096)
so.add(random26>=0)
so.add(random27<=4096)
so.add(random27>=0)
so.add(random28<=4096)
so.add(random28>=0)
so.add(random29<=4096)
so.add(random29>=0)
so.add(random30<=4096)
so.add(random30>=0)
so.add(random31<=4096)
so.add(random31>=0)
so.add(flag0>=48)
so.add(flag0<=102)
so.add(flag0!=58)
so.add(flag0!=59)
so.add(flag0!=60)
so.add(flag0!=61)
so.add(flag0!=62)
so.add(flag0!=63)
so.add(flag0!=64)
so.add(flag0!=65)
so.add(flag0!=66)
so.add(flag0!=67)
so.add(flag0!=68)
so.add(flag0!=69)
so.add(flag0!=70)
so.add(flag0!=71)
so.add(flag0!=72)
so.add(flag0!=73)
so.add(flag0!=74)
so.add(flag0!=75)
so.add(flag0!=76)
so.add(flag0!=77)
so.add(flag0!=78)
so.add(flag0!=79)
so.add(flag0!=80)
so.add(flag0!=81)
so.add(flag0!=82)
so.add(flag0!=83)
so.add(flag0!=84)
so.add(flag0!=85)
so.add(flag0!=86)
so.add(flag0!=87)
so.add(flag0!=88)
so.add(flag0!=89)
so.add(flag0!=90)
so.add(flag0!=91)
so.add(flag0!=92)
so.add(flag0!=93)
so.add(flag0!=94)
so.add(flag0!=95)
so.add(flag0!=96)
so.add(flag1>=48)
so.add(flag1<=102)
so.add(flag1!=58)
so.add(flag1!=59)
so.add(flag1!=60)
so.add(flag1!=61)
so.add(flag1!=62)
so.add(flag1!=63)
so.add(flag1!=64)
so.add(flag1!=65)
so.add(flag1!=66)
so.add(flag1!=67)
so.add(flag1!=68)
so.add(flag1!=69)
so.add(flag1!=70)
so.add(flag1!=71)
so.add(flag1!=72)
so.add(flag1!=73)
so.add(flag1!=74)
so.add(flag1!=75)
so.add(flag1!=76)
so.add(flag1!=77)
so.add(flag1!=78)
so.add(flag1!=79)
so.add(flag1!=80)
so.add(flag1!=81)
so.add(flag1!=82)
so.add(flag1!=83)
so.add(flag1!=84)
so.add(flag1!=85)
so.add(flag1!=86)
so.add(flag1!=87)
so.add(flag1!=88)
so.add(flag1!=89)
so.add(flag1!=90)
so.add(flag1!=91)
so.add(flag1!=92)
so.add(flag1!=93)
so.add(flag1!=94)
so.add(flag1!=95)
so.add(flag1!=96)
so.add(flag2>=48)
so.add(flag2<=102)
so.add(flag2!=58)
so.add(flag2!=59)
so.add(flag2!=60)
so.add(flag2!=61)
so.add(flag2!=62)
so.add(flag2!=63)
so.add(flag2!=64)
so.add(flag2!=65)
so.add(flag2!=66)
so.add(flag2!=67)
so.add(flag2!=68)
so.add(flag2!=69)
so.add(flag2!=70)
so.add(flag2!=71)
so.add(flag2!=72)
so.add(flag2!=73)
so.add(flag2!=74)
so.add(flag2!=75)
so.add(flag2!=76)
so.add(flag2!=77)
so.add(flag2!=78)
so.add(flag2!=79)
so.add(flag2!=80)
so.add(flag2!=81)
so.add(flag2!=82)
so.add(flag2!=83)
so.add(flag2!=84)
so.add(flag2!=85)
so.add(flag2!=86)
so.add(flag2!=87)
so.add(flag2!=88)
so.add(flag2!=89)
so.add(flag2!=90)
so.add(flag2!=91)
so.add(flag2!=92)
so.add(flag2!=93)
so.add(flag2!=94)
so.add(flag2!=95)
so.add(flag2!=96)
so.add(flag3>=48)
so.add(flag3<=102)
so.add(flag3!=58)
so.add(flag3!=59)
so.add(flag3!=60)
so.add(flag3!=61)
so.add(flag3!=62)
so.add(flag3!=63)
so.add(flag3!=64)
so.add(flag3!=65)
so.add(flag3!=66)
so.add(flag3!=67)
so.add(flag3!=68)
so.add(flag3!=69)
so.add(flag3!=70)
so.add(flag3!=71)
so.add(flag3!=72)
so.add(flag3!=73)
so.add(flag3!=74)
so.add(flag3!=75)
so.add(flag3!=76)
so.add(flag3!=77)
so.add(flag3!=78)
so.add(flag3!=79)
so.add(flag3!=80)
so.add(flag3!=81)
so.add(flag3!=82)
so.add(flag3!=83)
so.add(flag3!=84)
so.add(flag3!=85)
so.add(flag3!=86)
so.add(flag3!=87)
so.add(flag3!=88)
so.add(flag3!=89)
so.add(flag3!=90)
so.add(flag3!=91)
so.add(flag3!=92)
so.add(flag3!=93)
so.add(flag3!=94)
so.add(flag3!=95)
so.add(flag3!=96)
so.add(flag4>=48)
so.add(flag4<=102)
so.add(flag4!=58)
so.add(flag4!=59)
so.add(flag4!=60)
so.add(flag4!=61)
so.add(flag4!=62)
so.add(flag4!=63)
so.add(flag4!=64)
so.add(flag4!=65)
so.add(flag4!=66)
so.add(flag4!=67)
so.add(flag4!=68)
so.add(flag4!=69)
so.add(flag4!=70)
so.add(flag4!=71)
so.add(flag4!=72)
so.add(flag4!=73)
so.add(flag4!=74)
so.add(flag4!=75)
so.add(flag4!=76)
so.add(flag4!=77)
so.add(flag4!=78)
so.add(flag4!=79)
so.add(flag4!=80)
so.add(flag4!=81)
so.add(flag4!=82)
so.add(flag4!=83)
so.add(flag4!=84)
so.add(flag4!=85)
so.add(flag4!=86)
so.add(flag4!=87)
so.add(flag4!=88)
so.add(flag4!=89)
so.add(flag4!=90)
so.add(flag4!=91)
so.add(flag4!=92)
so.add(flag4!=93)
so.add(flag4!=94)
so.add(flag4!=95)
so.add(flag4!=96)
so.add(flag5>=48)
so.add(flag5<=102)
so.add(flag5!=58)
so.add(flag5!=59)
so.add(flag5!=60)
so.add(flag5!=61)
so.add(flag5!=62)
so.add(flag5!=63)
so.add(flag5!=64)
so.add(flag5!=65)
so.add(flag5!=66)
so.add(flag5!=67)
so.add(flag5!=68)
so.add(flag5!=69)
so.add(flag5!=70)
so.add(flag5!=71)
so.add(flag5!=72)
so.add(flag5!=73)
so.add(flag5!=74)
so.add(flag5!=75)
so.add(flag5!=76)
so.add(flag5!=77)
so.add(flag5!=78)
so.add(flag5!=79)
so.add(flag5!=80)
so.add(flag5!=81)
so.add(flag5!=82)
so.add(flag5!=83)
so.add(flag5!=84)
so.add(flag5!=85)
so.add(flag5!=86)
so.add(flag5!=87)
so.add(flag5!=88)
so.add(flag5!=89)
so.add(flag5!=90)
so.add(flag5!=91)
so.add(flag5!=92)
so.add(flag5!=93)
so.add(flag5!=94)
so.add(flag5!=95)
so.add(flag5!=96)
so.add(flag6>=48)
so.add(flag6<=102)
so.add(flag6!=58)
so.add(flag6!=59)
so.add(flag6!=60)
so.add(flag6!=61)
so.add(flag6!=62)
so.add(flag6!=63)
so.add(flag6!=64)
so.add(flag6!=65)
so.add(flag6!=66)
so.add(flag6!=67)
so.add(flag6!=68)
so.add(flag6!=69)
so.add(flag6!=70)
so.add(flag6!=71)
so.add(flag6!=72)
so.add(flag6!=73)
so.add(flag6!=74)
so.add(flag6!=75)
so.add(flag6!=76)
so.add(flag6!=77)
so.add(flag6!=78)
so.add(flag6!=79)
so.add(flag6!=80)
so.add(flag6!=81)
so.add(flag6!=82)
so.add(flag6!=83)
so.add(flag6!=84)
so.add(flag6!=85)
so.add(flag6!=86)
so.add(flag6!=87)
so.add(flag6!=88)
so.add(flag6!=89)
so.add(flag6!=90)
so.add(flag6!=91)
so.add(flag6!=92)
so.add(flag6!=93)
so.add(flag6!=94)
so.add(flag6!=95)
so.add(flag6!=96)
so.add(flag7>=48)
so.add(flag7<=102)
so.add(flag7!=58)
so.add(flag7!=59)
so.add(flag7!=60)
so.add(flag7!=61)
so.add(flag7!=62)
so.add(flag7!=63)
so.add(flag7!=64)
so.add(flag7!=65)
so.add(flag7!=66)
so.add(flag7!=67)
so.add(flag7!=68)
so.add(flag7!=69)
so.add(flag7!=70)
so.add(flag7!=71)
so.add(flag7!=72)
so.add(flag7!=73)
so.add(flag7!=74)
so.add(flag7!=75)
so.add(flag7!=76)
so.add(flag7!=77)
so.add(flag7!=78)
so.add(flag7!=79)
so.add(flag7!=80)
so.add(flag7!=81)
so.add(flag7!=82)
so.add(flag7!=83)
so.add(flag7!=84)
so.add(flag7!=85)
so.add(flag7!=86)
so.add(flag7!=87)
so.add(flag7!=88)
so.add(flag7!=89)
so.add(flag7!=90)
so.add(flag7!=91)
so.add(flag7!=92)
so.add(flag7!=93)
so.add(flag7!=94)
so.add(flag7!=95)
so.add(flag7!=96)
so.add(flag8>=48)
so.add(flag8<=102)
so.add(flag8!=58)
so.add(flag8!=59)
so.add(flag8!=60)
so.add(flag8!=61)
so.add(flag8!=62)
so.add(flag8!=63)
so.add(flag8!=64)
so.add(flag8!=65)
so.add(flag8!=66)
so.add(flag8!=67)
so.add(flag8!=68)
so.add(flag8!=69)
so.add(flag8!=70)
so.add(flag8!=71)
so.add(flag8!=72)
so.add(flag8!=73)
so.add(flag8!=74)
so.add(flag8!=75)
so.add(flag8!=76)
so.add(flag8!=77)
so.add(flag8!=78)
so.add(flag8!=79)
so.add(flag8!=80)
so.add(flag8!=81)
so.add(flag8!=82)
so.add(flag8!=83)
so.add(flag8!=84)
so.add(flag8!=85)
so.add(flag8!=86)
so.add(flag8!=87)
so.add(flag8!=88)
so.add(flag8!=89)
so.add(flag8!=90)
so.add(flag8!=91)
so.add(flag8!=92)
so.add(flag8!=93)
so.add(flag8!=94)
so.add(flag8!=95)
so.add(flag8!=96)
so.add(flag9>=48)
so.add(flag9<=102)
so.add(flag9!=58)
so.add(flag9!=59)
so.add(flag9!=60)
so.add(flag9!=61)
so.add(flag9!=62)
so.add(flag9!=63)
so.add(flag9!=64)
so.add(flag9!=65)
so.add(flag9!=66)
so.add(flag9!=67)
so.add(flag9!=68)
so.add(flag9!=69)
so.add(flag9!=70)
so.add(flag9!=71)
so.add(flag9!=72)
so.add(flag9!=73)
so.add(flag9!=74)
so.add(flag9!=75)
so.add(flag9!=76)
so.add(flag9!=77)
so.add(flag9!=78)
so.add(flag9!=79)
so.add(flag9!=80)
so.add(flag9!=81)
so.add(flag9!=82)
so.add(flag9!=83)
so.add(flag9!=84)
so.add(flag9!=85)
so.add(flag9!=86)
so.add(flag9!=87)
so.add(flag9!=88)
so.add(flag9!=89)
so.add(flag9!=90)
so.add(flag9!=91)
so.add(flag9!=92)
so.add(flag9!=93)
so.add(flag9!=94)
so.add(flag9!=95)
so.add(flag9!=96)
so.add(flag10>=48)
so.add(flag10<=102)
so.add(flag10!=58)
so.add(flag10!=59)
so.add(flag10!=60)
so.add(flag10!=61)
so.add(flag10!=62)
so.add(flag10!=63)
so.add(flag10!=64)
so.add(flag10!=65)
so.add(flag10!=66)
so.add(flag10!=67)
so.add(flag10!=68)
so.add(flag10!=69)
so.add(flag10!=70)
so.add(flag10!=71)
so.add(flag10!=72)
so.add(flag10!=73)
so.add(flag10!=74)
so.add(flag10!=75)
so.add(flag10!=76)
so.add(flag10!=77)
so.add(flag10!=78)
so.add(flag10!=79)
so.add(flag10!=80)
so.add(flag10!=81)
so.add(flag10!=82)
so.add(flag10!=83)
so.add(flag10!=84)
so.add(flag10!=85)
so.add(flag10!=86)
so.add(flag10!=87)
so.add(flag10!=88)
so.add(flag10!=89)
so.add(flag10!=90)
so.add(flag10!=91)
so.add(flag10!=92)
so.add(flag10!=93)
so.add(flag10!=94)
so.add(flag10!=95)
so.add(flag10!=96)
so.add(flag11>=48)
so.add(flag11<=102)
so.add(flag11!=58)
so.add(flag11!=59)
so.add(flag11!=60)
so.add(flag11!=61)
so.add(flag11!=62)
so.add(flag11!=63)
so.add(flag11!=64)
so.add(flag11!=65)
so.add(flag11!=66)
so.add(flag11!=67)
so.add(flag11!=68)
so.add(flag11!=69)
so.add(flag11!=70)
so.add(flag11!=71)
so.add(flag11!=72)
so.add(flag11!=73)
so.add(flag11!=74)
so.add(flag11!=75)
so.add(flag11!=76)
so.add(flag11!=77)
so.add(flag11!=78)
so.add(flag11!=79)
so.add(flag11!=80)
so.add(flag11!=81)
so.add(flag11!=82)
so.add(flag11!=83)
so.add(flag11!=84)
so.add(flag11!=85)
so.add(flag11!=86)
so.add(flag11!=87)
so.add(flag11!=88)
so.add(flag11!=89)
so.add(flag11!=90)
so.add(flag11!=91)
so.add(flag11!=92)
so.add(flag11!=93)
so.add(flag11!=94)
so.add(flag11!=95)
so.add(flag11!=96)
so.add(flag12>=48)
so.add(flag12<=102)
so.add(flag12!=58)
so.add(flag12!=59)
so.add(flag12!=60)
so.add(flag12!=61)
so.add(flag12!=62)
so.add(flag12!=63)
so.add(flag12!=64)
so.add(flag12!=65)
so.add(flag12!=66)
so.add(flag12!=67)
so.add(flag12!=68)
so.add(flag12!=69)
so.add(flag12!=70)
so.add(flag12!=71)
so.add(flag12!=72)
so.add(flag12!=73)
so.add(flag12!=74)
so.add(flag12!=75)
so.add(flag12!=76)
so.add(flag12!=77)
so.add(flag12!=78)
so.add(flag12!=79)
so.add(flag12!=80)
so.add(flag12!=81)
so.add(flag12!=82)
so.add(flag12!=83)
so.add(flag12!=84)
so.add(flag12!=85)
so.add(flag12!=86)
so.add(flag12!=87)
so.add(flag12!=88)
so.add(flag12!=89)
so.add(flag12!=90)
so.add(flag12!=91)
so.add(flag12!=92)
so.add(flag12!=93)
so.add(flag12!=94)
so.add(flag12!=95)
so.add(flag12!=96)
so.add(flag13>=48)
so.add(flag13<=102)
so.add(flag13!=58)
so.add(flag13!=59)
so.add(flag13!=60)
so.add(flag13!=61)
so.add(flag13!=62)
so.add(flag13!=63)
so.add(flag13!=64)
so.add(flag13!=65)
so.add(flag13!=66)
so.add(flag13!=67)
so.add(flag13!=68)
so.add(flag13!=69)
so.add(flag13!=70)
so.add(flag13!=71)
so.add(flag13!=72)
so.add(flag13!=73)
so.add(flag13!=74)
so.add(flag13!=75)
so.add(flag13!=76)
so.add(flag13!=77)
so.add(flag13!=78)
so.add(flag13!=79)
so.add(flag13!=80)
so.add(flag13!=81)
so.add(flag13!=82)
so.add(flag13!=83)
so.add(flag13!=84)
so.add(flag13!=85)
so.add(flag13!=86)
so.add(flag13!=87)
so.add(flag13!=88)
so.add(flag13!=89)
so.add(flag13!=90)
so.add(flag13!=91)
so.add(flag13!=92)
so.add(flag13!=93)
so.add(flag13!=94)
so.add(flag13!=95)
so.add(flag13!=96)
so.add(flag14>=48)
so.add(flag14<=102)
so.add(flag14!=58)
so.add(flag14!=59)
so.add(flag14!=60)
so.add(flag14!=61)
so.add(flag14!=62)
so.add(flag14!=63)
so.add(flag14!=64)
so.add(flag14!=65)
so.add(flag14!=66)
so.add(flag14!=67)
so.add(flag14!=68)
so.add(flag14!=69)
so.add(flag14!=70)
so.add(flag14!=71)
so.add(flag14!=72)
so.add(flag14!=73)
so.add(flag14!=74)
so.add(flag14!=75)
so.add(flag14!=76)
so.add(flag14!=77)
so.add(flag14!=78)
so.add(flag14!=79)
so.add(flag14!=80)
so.add(flag14!=81)
so.add(flag14!=82)
so.add(flag14!=83)
so.add(flag14!=84)
so.add(flag14!=85)
so.add(flag14!=86)
so.add(flag14!=87)
so.add(flag14!=88)
so.add(flag14!=89)
so.add(flag14!=90)
so.add(flag14!=91)
so.add(flag14!=92)
so.add(flag14!=93)
so.add(flag14!=94)
so.add(flag14!=95)
so.add(flag14!=96)
so.add(flag15>=48)
so.add(flag15<=102)
so.add(flag15!=58)
so.add(flag15!=59)
so.add(flag15!=60)
so.add(flag15!=61)
so.add(flag15!=62)
so.add(flag15!=63)
so.add(flag15!=64)
so.add(flag15!=65)
so.add(flag15!=66)
so.add(flag15!=67)
so.add(flag15!=68)
so.add(flag15!=69)
so.add(flag15!=70)
so.add(flag15!=71)
so.add(flag15!=72)
so.add(flag15!=73)
so.add(flag15!=74)
so.add(flag15!=75)
so.add(flag15!=76)
so.add(flag15!=77)
so.add(flag15!=78)
so.add(flag15!=79)
so.add(flag15!=80)
so.add(flag15!=81)
so.add(flag15!=82)
so.add(flag15!=83)
so.add(flag15!=84)
so.add(flag15!=85)
so.add(flag15!=86)
so.add(flag15!=87)
so.add(flag15!=88)
so.add(flag15!=89)
so.add(flag15!=90)
so.add(flag15!=91)
so.add(flag15!=92)
so.add(flag15!=93)
so.add(flag15!=94)
so.add(flag15!=95)
so.add(flag15!=96)
so.add(flag16>=48)
so.add(flag16<=102)
so.add(flag16!=58)
so.add(flag16!=59)
so.add(flag16!=60)
so.add(flag16!=61)
so.add(flag16!=62)
so.add(flag16!=63)
so.add(flag16!=64)
so.add(flag16!=65)
so.add(flag16!=66)
so.add(flag16!=67)
so.add(flag16!=68)
so.add(flag16!=69)
so.add(flag16!=70)
so.add(flag16!=71)
so.add(flag16!=72)
so.add(flag16!=73)
so.add(flag16!=74)
so.add(flag16!=75)
so.add(flag16!=76)
so.add(flag16!=77)
so.add(flag16!=78)
so.add(flag16!=79)
so.add(flag16!=80)
so.add(flag16!=81)
so.add(flag16!=82)
so.add(flag16!=83)
so.add(flag16!=84)
so.add(flag16!=85)
so.add(flag16!=86)
so.add(flag16!=87)
so.add(flag16!=88)
so.add(flag16!=89)
so.add(flag16!=90)
so.add(flag16!=91)
so.add(flag16!=92)
so.add(flag16!=93)
so.add(flag16!=94)
so.add(flag16!=95)
so.add(flag16!=96)
so.add(flag17>=48)
so.add(flag17<=102)
so.add(flag17!=58)
so.add(flag17!=59)
so.add(flag17!=60)
so.add(flag17!=61)
so.add(flag17!=62)
so.add(flag17!=63)
so.add(flag17!=64)
so.add(flag17!=65)
so.add(flag17!=66)
so.add(flag17!=67)
so.add(flag17!=68)
so.add(flag17!=69)
so.add(flag17!=70)
so.add(flag17!=71)
so.add(flag17!=72)
so.add(flag17!=73)
so.add(flag17!=74)
so.add(flag17!=75)
so.add(flag17!=76)
so.add(flag17!=77)
so.add(flag17!=78)
so.add(flag17!=79)
so.add(flag17!=80)
so.add(flag17!=81)
so.add(flag17!=82)
so.add(flag17!=83)
so.add(flag17!=84)
so.add(flag17!=85)
so.add(flag17!=86)
so.add(flag17!=87)
so.add(flag17!=88)
so.add(flag17!=89)
so.add(flag17!=90)
so.add(flag17!=91)
so.add(flag17!=92)
so.add(flag17!=93)
so.add(flag17!=94)
so.add(flag17!=95)
so.add(flag17!=96)
so.add(flag18>=48)
so.add(flag18<=102)
so.add(flag18!=58)
so.add(flag18!=59)
so.add(flag18!=60)
so.add(flag18!=61)
so.add(flag18!=62)
so.add(flag18!=63)
so.add(flag18!=64)
so.add(flag18!=65)
so.add(flag18!=66)
so.add(flag18!=67)
so.add(flag18!=68)
so.add(flag18!=69)
so.add(flag18!=70)
so.add(flag18!=71)
so.add(flag18!=72)
so.add(flag18!=73)
so.add(flag18!=74)
so.add(flag18!=75)
so.add(flag18!=76)
so.add(flag18!=77)
so.add(flag18!=78)
so.add(flag18!=79)
so.add(flag18!=80)
so.add(flag18!=81)
so.add(flag18!=82)
so.add(flag18!=83)
so.add(flag18!=84)
so.add(flag18!=85)
so.add(flag18!=86)
so.add(flag18!=87)
so.add(flag18!=88)
so.add(flag18!=89)
so.add(flag18!=90)
so.add(flag18!=91)
so.add(flag18!=92)
so.add(flag18!=93)
so.add(flag18!=94)
so.add(flag18!=95)
so.add(flag18!=96)
so.add(flag19>=48)
so.add(flag19<=102)
so.add(flag19!=58)
so.add(flag19!=59)
so.add(flag19!=60)
so.add(flag19!=61)
so.add(flag19!=62)
so.add(flag19!=63)
so.add(flag19!=64)
so.add(flag19!=65)
so.add(flag19!=66)
so.add(flag19!=67)
so.add(flag19!=68)
so.add(flag19!=69)
so.add(flag19!=70)
so.add(flag19!=71)
so.add(flag19!=72)
so.add(flag19!=73)
so.add(flag19!=74)
so.add(flag19!=75)
so.add(flag19!=76)
so.add(flag19!=77)
so.add(flag19!=78)
so.add(flag19!=79)
so.add(flag19!=80)
so.add(flag19!=81)
so.add(flag19!=82)
so.add(flag19!=83)
so.add(flag19!=84)
so.add(flag19!=85)
so.add(flag19!=86)
so.add(flag19!=87)
so.add(flag19!=88)
so.add(flag19!=89)
so.add(flag19!=90)
so.add(flag19!=91)
so.add(flag19!=92)
so.add(flag19!=93)
so.add(flag19!=94)
so.add(flag19!=95)
so.add(flag19!=96)
so.add(flag20>=48)
so.add(flag20<=102)
so.add(flag20!=58)
so.add(flag20!=59)
so.add(flag20!=60)
so.add(flag20!=61)
so.add(flag20!=62)
so.add(flag20!=63)
so.add(flag20!=64)
so.add(flag20!=65)
so.add(flag20!=66)
so.add(flag20!=67)
so.add(flag20!=68)
so.add(flag20!=69)
so.add(flag20!=70)
so.add(flag20!=71)
so.add(flag20!=72)
so.add(flag20!=73)
so.add(flag20!=74)
so.add(flag20!=75)
so.add(flag20!=76)
so.add(flag20!=77)
so.add(flag20!=78)
so.add(flag20!=79)
so.add(flag20!=80)
so.add(flag20!=81)
so.add(flag20!=82)
so.add(flag20!=83)
so.add(flag20!=84)
so.add(flag20!=85)
so.add(flag20!=86)
so.add(flag20!=87)
so.add(flag20!=88)
so.add(flag20!=89)
so.add(flag20!=90)
so.add(flag20!=91)
so.add(flag20!=92)
so.add(flag20!=93)
so.add(flag20!=94)
so.add(flag20!=95)
so.add(flag20!=96)
so.add(flag21>=48)
so.add(flag21<=102)
so.add(flag21!=58)
so.add(flag21!=59)
so.add(flag21!=60)
so.add(flag21!=61)
so.add(flag21!=62)
so.add(flag21!=63)
so.add(flag21!=64)
so.add(flag21!=65)
so.add(flag21!=66)
so.add(flag21!=67)
so.add(flag21!=68)
so.add(flag21!=69)
so.add(flag21!=70)
so.add(flag21!=71)
so.add(flag21!=72)
so.add(flag21!=73)
so.add(flag21!=74)
so.add(flag21!=75)
so.add(flag21!=76)
so.add(flag21!=77)
so.add(flag21!=78)
so.add(flag21!=79)
so.add(flag21!=80)
so.add(flag21!=81)
so.add(flag21!=82)
so.add(flag21!=83)
so.add(flag21!=84)
so.add(flag21!=85)
so.add(flag21!=86)
so.add(flag21!=87)
so.add(flag21!=88)
so.add(flag21!=89)
so.add(flag21!=90)
so.add(flag21!=91)
so.add(flag21!=92)
so.add(flag21!=93)
so.add(flag21!=94)
so.add(flag21!=95)
so.add(flag21!=96)
so.add(flag22>=48)
so.add(flag22<=102)
so.add(flag22!=58)
so.add(flag22!=59)
so.add(flag22!=60)
so.add(flag22!=61)
so.add(flag22!=62)
so.add(flag22!=63)
so.add(flag22!=64)
so.add(flag22!=65)
so.add(flag22!=66)
so.add(flag22!=67)
so.add(flag22!=68)
so.add(flag22!=69)
so.add(flag22!=70)
so.add(flag22!=71)
so.add(flag22!=72)
so.add(flag22!=73)
so.add(flag22!=74)
so.add(flag22!=75)
so.add(flag22!=76)
so.add(flag22!=77)
so.add(flag22!=78)
so.add(flag22!=79)
so.add(flag22!=80)
so.add(flag22!=81)
so.add(flag22!=82)
so.add(flag22!=83)
so.add(flag22!=84)
so.add(flag22!=85)
so.add(flag22!=86)
so.add(flag22!=87)
so.add(flag22!=88)
so.add(flag22!=89)
so.add(flag22!=90)
so.add(flag22!=91)
so.add(flag22!=92)
so.add(flag22!=93)
so.add(flag22!=94)
so.add(flag22!=95)
so.add(flag22!=96)
so.add(flag23>=48)
so.add(flag23<=102)
so.add(flag23!=58)
so.add(flag23!=59)
so.add(flag23!=60)
so.add(flag23!=61)
so.add(flag23!=62)
so.add(flag23!=63)
so.add(flag23!=64)
so.add(flag23!=65)
so.add(flag23!=66)
so.add(flag23!=67)
so.add(flag23!=68)
so.add(flag23!=69)
so.add(flag23!=70)
so.add(flag23!=71)
so.add(flag23!=72)
so.add(flag23!=73)
so.add(flag23!=74)
so.add(flag23!=75)
so.add(flag23!=76)
so.add(flag23!=77)
so.add(flag23!=78)
so.add(flag23!=79)
so.add(flag23!=80)
so.add(flag23!=81)
so.add(flag23!=82)
so.add(flag23!=83)
so.add(flag23!=84)
so.add(flag23!=85)
so.add(flag23!=86)
so.add(flag23!=87)
so.add(flag23!=88)
so.add(flag23!=89)
so.add(flag23!=90)
so.add(flag23!=91)
so.add(flag23!=92)
so.add(flag23!=93)
so.add(flag23!=94)
so.add(flag23!=95)
so.add(flag23!=96)
so.add(flag24>=48)
so.add(flag24<=102)
so.add(flag24!=58)
so.add(flag24!=59)
so.add(flag24!=60)
so.add(flag24!=61)
so.add(flag24!=62)
so.add(flag24!=63)
so.add(flag24!=64)
so.add(flag24!=65)
so.add(flag24!=66)
so.add(flag24!=67)
so.add(flag24!=68)
so.add(flag24!=69)
so.add(flag24!=70)
so.add(flag24!=71)
so.add(flag24!=72)
so.add(flag24!=73)
so.add(flag24!=74)
so.add(flag24!=75)
so.add(flag24!=76)
so.add(flag24!=77)
so.add(flag24!=78)
so.add(flag24!=79)
so.add(flag24!=80)
so.add(flag24!=81)
so.add(flag24!=82)
so.add(flag24!=83)
so.add(flag24!=84)
so.add(flag24!=85)
so.add(flag24!=86)
so.add(flag24!=87)
so.add(flag24!=88)
so.add(flag24!=89)
so.add(flag24!=90)
so.add(flag24!=91)
so.add(flag24!=92)
so.add(flag24!=93)
so.add(flag24!=94)
so.add(flag24!=95)
so.add(flag24!=96)
so.add(flag25>=48)
so.add(flag25<=102)
so.add(flag25!=58)
so.add(flag25!=59)
so.add(flag25!=60)
so.add(flag25!=61)
so.add(flag25!=62)
so.add(flag25!=63)
so.add(flag25!=64)
so.add(flag25!=65)
so.add(flag25!=66)
so.add(flag25!=67)
so.add(flag25!=68)
so.add(flag25!=69)
so.add(flag25!=70)
so.add(flag25!=71)
so.add(flag25!=72)
so.add(flag25!=73)
so.add(flag25!=74)
so.add(flag25!=75)
so.add(flag25!=76)
so.add(flag25!=77)
so.add(flag25!=78)
so.add(flag25!=79)
so.add(flag25!=80)
so.add(flag25!=81)
so.add(flag25!=82)
so.add(flag25!=83)
so.add(flag25!=84)
so.add(flag25!=85)
so.add(flag25!=86)
so.add(flag25!=87)
so.add(flag25!=88)
so.add(flag25!=89)
so.add(flag25!=90)
so.add(flag25!=91)
so.add(flag25!=92)
so.add(flag25!=93)
so.add(flag25!=94)
so.add(flag25!=95)
so.add(flag25!=96)
so.add(flag26>=48)
so.add(flag26<=102)
so.add(flag26!=58)
so.add(flag26!=59)
so.add(flag26!=60)
so.add(flag26!=61)
so.add(flag26!=62)
so.add(flag26!=63)
so.add(flag26!=64)
so.add(flag26!=65)
so.add(flag26!=66)
so.add(flag26!=67)
so.add(flag26!=68)
so.add(flag26!=69)
so.add(flag26!=70)
so.add(flag26!=71)
so.add(flag26!=72)
so.add(flag26!=73)
so.add(flag26!=74)
so.add(flag26!=75)
so.add(flag26!=76)
so.add(flag26!=77)
so.add(flag26!=78)
so.add(flag26!=79)
so.add(flag26!=80)
so.add(flag26!=81)
so.add(flag26!=82)
so.add(flag26!=83)
so.add(flag26!=84)
so.add(flag26!=85)
so.add(flag26!=86)
so.add(flag26!=87)
so.add(flag26!=88)
so.add(flag26!=89)
so.add(flag26!=90)
so.add(flag26!=91)
so.add(flag26!=92)
so.add(flag26!=93)
so.add(flag26!=94)
so.add(flag26!=95)
so.add(flag26!=96)
so.add(flag27>=48)
so.add(flag27<=102)
so.add(flag27!=58)
so.add(flag27!=59)
so.add(flag27!=60)
so.add(flag27!=61)
so.add(flag27!=62)
so.add(flag27!=63)
so.add(flag27!=64)
so.add(flag27!=65)
so.add(flag27!=66)
so.add(flag27!=67)
so.add(flag27!=68)
so.add(flag27!=69)
so.add(flag27!=70)
so.add(flag27!=71)
so.add(flag27!=72)
so.add(flag27!=73)
so.add(flag27!=74)
so.add(flag27!=75)
so.add(flag27!=76)
so.add(flag27!=77)
so.add(flag27!=78)
so.add(flag27!=79)
so.add(flag27!=80)
so.add(flag27!=81)
so.add(flag27!=82)
so.add(flag27!=83)
so.add(flag27!=84)
so.add(flag27!=85)
so.add(flag27!=86)
so.add(flag27!=87)
so.add(flag27!=88)
so.add(flag27!=89)
so.add(flag27!=90)
so.add(flag27!=91)
so.add(flag27!=92)
so.add(flag27!=93)
so.add(flag27!=94)
so.add(flag27!=95)
so.add(flag27!=96)
so.add(flag28>=48)
so.add(flag28<=102)
so.add(flag28!=58)
so.add(flag28!=59)
so.add(flag28!=60)
so.add(flag28!=61)
so.add(flag28!=62)
so.add(flag28!=63)
so.add(flag28!=64)
so.add(flag28!=65)
so.add(flag28!=66)
so.add(flag28!=67)
so.add(flag28!=68)
so.add(flag28!=69)
so.add(flag28!=70)
so.add(flag28!=71)
so.add(flag28!=72)
so.add(flag28!=73)
so.add(flag28!=74)
so.add(flag28!=75)
so.add(flag28!=76)
so.add(flag28!=77)
so.add(flag28!=78)
so.add(flag28!=79)
so.add(flag28!=80)
so.add(flag28!=81)
so.add(flag28!=82)
so.add(flag28!=83)
so.add(flag28!=84)
so.add(flag28!=85)
so.add(flag28!=86)
so.add(flag28!=87)
so.add(flag28!=88)
so.add(flag28!=89)
so.add(flag28!=90)
so.add(flag28!=91)
so.add(flag28!=92)
so.add(flag28!=93)
so.add(flag28!=94)
so.add(flag28!=95)
so.add(flag28!=96)
so.add(flag29>=48)
so.add(flag29<=102)
so.add(flag29!=58)
so.add(flag29!=59)
so.add(flag29!=60)
so.add(flag29!=61)
so.add(flag29!=62)
so.add(flag29!=63)
so.add(flag29!=64)
so.add(flag29!=65)
so.add(flag29!=66)
so.add(flag29!=67)
so.add(flag29!=68)
so.add(flag29!=69)
so.add(flag29!=70)
so.add(flag29!=71)
so.add(flag29!=72)
so.add(flag29!=73)
so.add(flag29!=74)
so.add(flag29!=75)
so.add(flag29!=76)
so.add(flag29!=77)
so.add(flag29!=78)
so.add(flag29!=79)
so.add(flag29!=80)
so.add(flag29!=81)
so.add(flag29!=82)
so.add(flag29!=83)
so.add(flag29!=84)
so.add(flag29!=85)
so.add(flag29!=86)
so.add(flag29!=87)
so.add(flag29!=88)
so.add(flag29!=89)
so.add(flag29!=90)
so.add(flag29!=91)
so.add(flag29!=92)
so.add(flag29!=93)
so.add(flag29!=94)
so.add(flag29!=95)
so.add(flag29!=96)
so.add(flag30>=48)
so.add(flag30<=102)
so.add(flag30!=58)
so.add(flag30!=59)
so.add(flag30!=60)
so.add(flag30!=61)
so.add(flag30!=62)
so.add(flag30!=63)
so.add(flag30!=64)
so.add(flag30!=65)
so.add(flag30!=66)
so.add(flag30!=67)
so.add(flag30!=68)
so.add(flag30!=69)
so.add(flag30!=70)
so.add(flag30!=71)
so.add(flag30!=72)
so.add(flag30!=73)
so.add(flag30!=74)
so.add(flag30!=75)
so.add(flag30!=76)
so.add(flag30!=77)
so.add(flag30!=78)
so.add(flag30!=79)
so.add(flag30!=80)
so.add(flag30!=81)
so.add(flag30!=82)
so.add(flag30!=83)
so.add(flag30!=84)
so.add(flag30!=85)
so.add(flag30!=86)
so.add(flag30!=87)
so.add(flag30!=88)
so.add(flag30!=89)
so.add(flag30!=90)
so.add(flag30!=91)
so.add(flag30!=92)
so.add(flag30!=93)
so.add(flag30!=94)
so.add(flag30!=95)
so.add(flag30!=96)
so.add(flag31>=48)
so.add(flag31<=102)
so.add(flag31!=58)
so.add(flag31!=59)
so.add(flag31!=60)
so.add(flag31!=61)
so.add(flag31!=62)
so.add(flag31!=63)
so.add(flag31!=64)
so.add(flag31!=65)
so.add(flag31!=66)
so.add(flag31!=67)
so.add(flag31!=68)
so.add(flag31!=69)
so.add(flag31!=70)
so.add(flag31!=71)
so.add(flag31!=72)
so.add(flag31!=73)
so.add(flag31!=74)
so.add(flag31!=75)
so.add(flag31!=76)
so.add(flag31!=77)
so.add(flag31!=78)
so.add(flag31!=79)
so.add(flag31!=80)
so.add(flag31!=81)
so.add(flag31!=82)
so.add(flag31!=83)
so.add(flag31!=84)
so.add(flag31!=85)
so.add(flag31!=86)
so.add(flag31!=87)
so.add(flag31!=88)
so.add(flag31!=89)
so.add(flag31!=90)
so.add(flag31!=91)
so.add(flag31!=92)
so.add(flag31!=93)
so.add(flag31!=94)
so.add(flag31!=95)
so.add(flag31!=96)
print(so.check())
print(so.model())