(define p3::bool)
(define p4::bool)
(define p5::bool)
(define p6::bool)
(define p7::bool)
(define p8::bool)
(define p9::bool)
(define p10::bool)
(define p11::bool)
(define p12::bool)
(define p13::bool)
(define p14::bool)
(define p15::bool)
(define p16::bool)
(define p17::bool)
(define p18::bool)
(define p19::bool)
(define p20::bool)
(define p21::bool)
(define p22::bool)

(define p23::bool)
(define p24::bool)
(define p25::bool)
(define p26::bool)
(define p27::bool)
(define p28::bool)
(define p29::bool)
(define p30::bool)
(define p31::bool)
(define p32::bool)
(define p33::bool)
(define p34::bool)
(define p35::bool)
(define p36::bool)
(define p37::bool)
(define p38::bool)
(define p39::bool)
(define p40::bool)
(define p41::bool)
(define p42::bool)

(define p44::bool)
(define p45::bool)
(define p46::bool)
(define p47::bool)
(define p48::bool)
(define p49::bool)
(define p50::bool)
(define p51::bool)
(define p52::bool)
(define p53::bool)
(define p54::bool)
(define p55::bool)
(define p56::bool)
(define p57::bool)
(define p58::bool)
(define p59::bool)
(define p60::bool)
(define p61::bool)
(define p62::bool)
(define p63::bool)
(define p64::bool)
(define p65::bool)
(define p66::bool)
(define p67::bool)
(define p68::bool)
(define p69::bool)
(define p70::bool)
(define p71::bool)
(define p72::bool)
(define p73::bool)
(define p74::bool)
(define p75::bool)
(define p76::bool)
(define p77::bool)
(define p78::bool)
(define p79::bool)
(define p80::bool)
(define p81::bool)

(define p82::bool)
(define p83::bool)
(define p84::bool)
(define p85::bool)
(define p86::bool)
(define p87::bool)
(define p88::bool)
(define p89::bool)
(define p90::bool)
(define p91::bool)
(define p92::bool)
(define p93::bool)
(define p94::bool)
(define p95::bool)
(define p96::bool)
(define p97::bool)
(define p98::bool)
(define p99::bool)
(define p100::bool)
(define p101::bool)
(define p102::bool)
(define p103::bool)
(define p104::bool)
(define p105::bool)
(define p106::bool)
(define p107::bool)
(define p108::bool)
(define p109::bool)
(define p110::bool)
(define p111::bool)
(define p112::bool)
(define p113::bool)
(define p114::bool)
(define p115::bool)
(define p116::bool)
(define p117::bool)
(define p118::bool)
(define p119::bool)

(assert (= p3 p23))
(assert (= p4 p24))
(assert (= p5 p25))
(assert (= p6 p26))
(assert (= p7 p27))
(assert (= p8 p28))
(assert (= p9 p29))
(assert (= p10 p30))
(assert (= p11 p31))
(assert (= p12 p32))
(assert (= p13 p33))
(assert (= p14 p34))
(assert (= p15 p35))
(assert (= p16 p36))
(assert (= p17 p37))
(assert (= p18 p38))
(assert (= p19 p39))
(assert (= p20 p40))
(assert (= p21 p41))
(assert (= p22 p42))

(assert (or (/= p3 p23)(/= p44 p82)(/= p46 p84)(/= p48 p86)(/= p50 p88)
	    (/= p52 p90)(/= p54 p92)(/= p56 p94)(/= p58 p96)(/= p60 p98)
	    (/= p62 p100)(/= p64 p102)(/= p66 p104)(/= p68 p106)(/= p70 p108)
	    (/= p72 p110)(/= p74 p112)(/= p76 p114)(/= p78 p116)(/= p80 p118)))

(assert (= p44 (= (not p3) p4)))
(assert (= p45 (or p3 p4)))
(assert (= p46 (= p5 (not p45))))
(assert (= p47 (or p5 p45)))
(assert (= p48 (= p6 (not p47))))
(assert (= p49 (or p6 p47)))
(assert (= p50 (= p7 (not p49))))
(assert (= p51 (or p7 p49)))
(assert (= p52 (= p8 (not p51))))
(assert (= p53 (or p8 p51)))
(assert (= p54 (= p9 (not p53))))
(assert (= p55 (or p9 p53)))
(assert (= p56 (= p10 (not p55))))
(assert (= p57 (or p10 p55)))
(assert (= p58 (= p11 (not p57))))
(assert (= p59 (or p11 p57)))
(assert (= p60 (= p12 (not p59))))
(assert (= p61 (or p12 p59)))
(assert (= p62 (= p13 (not p61))))
(assert (= p63 (or p13 p61)))
(assert (= p64 (= p14 (not p63))))
(assert (= p65 (or p14 p63)))
(assert (= p66 (= p15 (not p65))))
(assert (= p67 (or p15 p65)))
(assert (= p68 (= p16 (not p67))))
(assert (= p69 (or p16 p67)))
(assert (= p70 (= p17 (not p69))))
(assert (= p71 (or p17 p69)))
(assert (= p72 (= p18 (not p71))))
(assert (= p73 (or p18 p71)))
(assert (= p74 (= p19 (not p73))))
(assert (= p75 (or p19 p73)))
(assert (= p76 (= p20 (not p75))))
(assert (= p77 (or p20 p75)))
(assert (= p78 (= p21 (not p77))))
(assert (= p79 (or p21 p77)))
(assert (= p80 (= p22 (not p79))))
(assert (= p81 (or p22 p79)))
(assert (= p82 (= (not p23) p24)))
(assert (= p83 (or p23 p24)))
(assert (= p84 (= p25 (not p83))))
(assert (= p85 (or p25 p83)))
(assert (= p86 (= p26 (not p85))))
(assert (= p87 (or p26 p85)))
(assert (= p88 (= p27 (not p87))))
(assert (= p89 (or p27 p87)))
(assert (= p90 (= p28 (not p89))))
(assert (= p91 (or p28 p89)))
(assert (= p92 (= p29 (not p91))))
(assert (= p93 (or p29 p91)))
(assert (= p94 (= p30 (not p93))))
(assert (= p95 (or p30 p93)))
(assert (= p96 (= p31 (not p95))))
(assert (= p97 (or p31 p95)))
(assert (= p98 (= p32 (not p97))))
(assert (= p99 (or p32 p97)))
(assert (= p100 (= p33 (not p99))))
(assert (= p101 (or p33 p99)))
(assert (= p102 (= p34 (not p101))))
(assert (= p103 (or p34 p101)))
(assert (= p104 (= p35 (not p103))))
(assert (= p105 (or p35 p103)))
(assert (= p106 (= p36 (not p105))))
(assert (= p107 (or p36 p105)))
(assert (= p108 (= p37 (not p107))))
(assert (= p109 (or p37 p107)))
(assert (= p110 (= p38 (not p109))))
(assert (= p111 (or p38 p109)))
(assert (= p112 (= p39 (not p111))))
(assert (= p113 (or p39 p111)))
(assert (= p114 (= p40 (not p113))))
(assert (= p115 (or p40 p113)))
(assert (= p116 (= p41 (not p115))))
(assert (= p117 (or p41 p115)))
(assert (= p118 (= p42 (not p117))))
(assert (= p119 (or p42 p117)))

(assert (or (not p3) p45))
(assert (or (not p4) p45))
(assert (or (not p5) p47))
(assert (or (not p6) p49))
(assert (or (not p7) p51))
(assert (or (not p8) p53))
(assert (or (not p9) p55))
(assert (or (not p10) p57))
(assert (or (not p11) p59))
(assert (or (not p12) p61))
(assert (or (not p13) p63))
(assert (or (not p14) p65))
(assert (or (not p15) p67))
(assert (or (not p16) p69))
(assert (or (not p17) p71))
(assert (or (not p18) p73))
(assert (or (not p19) p75))
(assert (or (not p20) p77))
(assert (or (not p21) p79))
(assert (or (not p22) p81))
(assert (or (not p23) p83))
(assert (or (not p24) p83))
(assert (or (not p25) p85))
(assert (or (not p26) p87))
(assert (or (not p27) p89))
(assert (or (not p28) p91))
(assert (or (not p29) p93))
(assert (or (not p30) p95))
(assert (or (not p31) p97))
(assert (or (not p32) p99))
(assert (or (not p33) p101))
(assert (or (not p34) p103))
(assert (or (not p35) p105))
(assert (or (not p36) p107))
(assert (or (not p37) p109))
(assert (or (not p38) p111))
(assert (or (not p39) p113))
(assert (or (not p40) p115))
(assert (or (not p41) p117))
(assert (or (not p42) p119))
(assert (or (not p45) p47))
(assert (or (not p47) p49))
(assert (or (not p49) p51))
(assert (or (not p51) p53))
(assert (or (not p53) p55))
(assert (or (not p55) p57))
(assert (or (not p57) p59))
(assert (or (not p59) p61))
(assert (or (not p61) p63))
(assert (or (not p63) p65))
(assert (or (not p65) p67))
(assert (or (not p67) p69))
(assert (or (not p69) p71))
(assert (or (not p71) p73))
(assert (or (not p73) p75))
(assert (or (not p75) p77))
(assert (or (not p77) p79))
(assert (or (not p79) p81))
(assert (or (not p83) p85))
(assert (or (not p85) p87))
(assert (or (not p87) p89))
(assert (or (not p89) p91))
(assert (or (not p91) p93))
(assert (or (not p93) p95))
(assert (or (not p95) p97))
(assert (or (not p97) p99))
(assert (or (not p99) p101))
(assert (or (not p101) p103))
(assert (or (not p103) p105))
(assert (or (not p105) p107))
(assert (or (not p107) p109))
(assert (or (not p109) p111))
(assert (or (not p111) p113))
(assert (or (not p113) p115))
(assert (or (not p115) p117))
(assert (or (not p117) p119))
(assert (or (not p3) (not p4) (not p44)))
(assert (or p3 p4 (not p44)))
(assert (or (not p3) p4 p44))
(assert (or p3 (not p4) p44))
(assert (or p3 p4 (not p45)))
(assert (or p5 p45 (not p46)))
(assert (or (not p5) (not p45) (not p46)))
(assert (or p5 (not p45) p46))
(assert (or (not p5) p45 p46))
(assert (or p5 p45 (not p47)))
(assert (or p6 p47 (not p48)))
(assert (or (not p6) (not p47) (not p48)))
(assert (or p6 (not p47) p48))
(assert (or (not p6) p47 p48))
(assert (or p6 p47 (not p49)))
(assert (or p7 p49 (not p50)))
(assert (or (not p7) (not p49) (not p50)))
(assert (or p7 (not p49) p50))
(assert (or (not p7) p49 p50))
(assert (or p7 p49 (not p51)))
(assert (or p8 p51 (not p52)))
(assert (or (not p8) (not p51) (not p52)))
(assert (or p8 (not p51) p52))
(assert (or (not p8) p51 p52))
(assert (or p8 p51 (not p53)))
(assert (or p9 p53 (not p54)))
(assert (or (not p9) (not p53) (not p54)))
(assert (or p9 (not p53) p54))
(assert (or (not p9) p53 p54))
(assert (or p9 p53 (not p55)))
(assert (or p10 p55 (not p56)))
(assert (or (not p10) (not p55) (not p56)))
(assert (or p10 (not p55) p56))
(assert (or (not p10) p55 p56))
(assert (or p10 p55 (not p57)))
(assert (or p11 p57 (not p58)))
(assert (or (not p11) (not p57) (not p58)))
(assert (or p11 (not p57) p58))
(assert (or (not p11) p57 p58))
(assert (or p11 p57 (not p59)))
(assert (or p12 p59 (not p60)))
(assert (or (not p12) (not p59) (not p60)))
(assert (or p12 (not p59) p60))
(assert (or (not p12) p59 p60))
(assert (or p12 p59 (not p61)))
(assert (or p13 p61 (not p62)))
(assert (or (not p13) (not p61) (not p62)))
(assert (or p13 (not p61) p62))
(assert (or (not p13) p61 p62))
(assert (or p13 p61 (not p63)))
(assert (or p14 p63 (not p64)))
(assert (or (not p14) (not p63) (not p64)))
(assert (or p14 (not p63) p64))
(assert (or (not p14) p63 p64))
(assert (or p14 p63 (not p65)))
(assert (or p15 p65 (not p66)))
(assert (or (not p15) (not p65) (not p66)))
(assert (or p15 (not p65) p66))
(assert (or (not p15) p65 p66))
(assert (or p15 p65 (not p67)))
(assert (or p16 p67 (not p68)))
(assert (or (not p16) (not p67) (not p68)))
(assert (or p16 (not p67) p68))
(assert (or (not p16) p67 p68))
(assert (or p16 p67 (not p69)))
(assert (or p17 p69 (not p70)))
(assert (or (not p17) (not p69) (not p70)))
(assert (or p17 (not p69) p70))
(assert (or (not p17) p69 p70))
(assert (or p17 p69 (not p71)))
(assert (or p18 p71 (not p72)))
(assert (or (not p18) (not p71) (not p72)))
(assert (or p18 (not p71) p72))
(assert (or (not p18) p71 p72))
(assert (or p18 p71 (not p73)))
(assert (or p19 p73 (not p74)))
(assert (or (not p19) (not p73) (not p74)))
(assert (or p19 (not p73) p74))
(assert (or (not p19) p73 p74))
(assert (or p19 p73 (not p75)))
(assert (or p20 p75 (not p76)))
(assert (or (not p20) (not p75) (not p76)))
(assert (or p20 (not p75) p76))
(assert (or (not p20) p75 p76))
(assert (or p20 p75 (not p77)))
(assert (or p21 p77 (not p78)))
(assert (or (not p21) (not p77) (not p78)))
(assert (or p21 (not p77) p78))
(assert (or (not p21) p77 p78))
(assert (or p21 p77 (not p79)))
(assert (or p22 p79 (not p80)))
(assert (or (not p22) (not p79) (not p80)))
(assert (or p22 (not p79) p80))
(assert (or (not p22) p79 p80))
(assert (or p22 p79 (not p81)))
(assert (or (not p23) (not p24) (not p82)))
(assert (or p23 p24 (not p82)))
(assert (or (not p23) p24 p82))
(assert (or p23 (not p24) p82))
(assert (or p23 p24 (not p83)))
(assert (or p25 p83 (not p84)))
(assert (or (not p25) (not p83) (not p84)))
(assert (or p25 (not p83) p84))
(assert (or (not p25) p83 p84))
(assert (or p25 p83 (not p85)))
(assert (or p26 p85 (not p86)))
(assert (or (not p26) (not p85) (not p86)))
(assert (or p26 (not p85) p86))
(assert (or (not p26) p85 p86))
(assert (or p26 p85 (not p87)))
(assert (or p27 p87 (not p88)))
(assert (or (not p27) (not p87) (not p88)))
(assert (or p27 (not p87) p88))
(assert (or (not p27) p87 p88))
(assert (or p27 p87 (not p89)))
(assert (or p28 p89 (not p90)))
(assert (or (not p28) (not p89) (not p90)))
(assert (or p28 (not p89) p90))
(assert (or (not p28) p89 p90))
(assert (or p28 p89 (not p91)))
(assert (or p29 p91 (not p92)))
(assert (or (not p29) (not p91) (not p92)))
(assert (or p29 (not p91) p92))
(assert (or (not p29) p91 p92))
(assert (or p29 p91 (not p93)))
(assert (or p30 p93 (not p94)))
(assert (or (not p30) (not p93) (not p94)))
(assert (or p30 (not p93) p94))
(assert (or (not p30) p93 p94))
(assert (or p30 p93 (not p95)))
(assert (or p31 p95 (not p96)))
(assert (or (not p31) (not p95) (not p96)))
(assert (or p31 (not p95) p96))
(assert (or (not p31) p95 p96))
(assert (or p31 p95 (not p97)))
(assert (or p32 p97 (not p98)))
(assert (or (not p32) (not p97) (not p98)))
(assert (or p32 (not p97) p98))
(assert (or (not p32) p97 p98))
(assert (or p32 p97 (not p99)))
(assert (or p33 p99 (not p100)))
(assert (or (not p33) (not p99) (not p100)))
(assert (or p33 (not p99) p100))
(assert (or (not p33) p99 p100))
(assert (or p33 p99 (not p101)))
(assert (or p34 p101 (not p102)))
(assert (or (not p34) (not p101) (not p102)))
(assert (or p34 (not p101) p102))
(assert (or (not p34) p101 p102))
(assert (or p34 p101 (not p103)))
(assert (or p35 p103 (not p104)))
(assert (or (not p35) (not p103) (not p104)))
(assert (or p35 (not p103) p104))
(assert (or (not p35) p103 p104))
(assert (or p35 p103 (not p105)))
(assert (or p36 p105 (not p106)))
(assert (or (not p36) (not p105) (not p106)))
(assert (or p36 (not p105) p106))
(assert (or (not p36) p105 p106))
(assert (or p36 p105 (not p107)))
(assert (or p37 p107 (not p108)))
(assert (or (not p37) (not p107) (not p108)))
(assert (or p37 (not p107) p108))
(assert (or (not p37) p107 p108))
(assert (or p37 p107 (not p109)))
(assert (or p38 p109 (not p110)))
(assert (or (not p38) (not p109) (not p110)))
(assert (or p38 (not p109) p110))
(assert (or (not p38) p109 p110))
(assert (or p38 p109 (not p111)))
(assert (or p39 p111 (not p112)))
(assert (or (not p39) (not p111) (not p112)))
(assert (or p39 (not p111) p112))
(assert (or (not p39) p111 p112))
(assert (or p39 p111 (not p113)))
(assert (or p40 p113 (not p114)))
(assert (or (not p40) (not p113) (not p114)))
(assert (or p40 (not p113) p114))
(assert (or (not p40) p113 p114))
(assert (or p40 p113 (not p115)))
(assert (or p41 p115 (not p116)))
(assert (or (not p41) (not p115) (not p116)))
(assert (or p41 (not p115) p116))
(assert (or (not p41) p115 p116))
(assert (or p41 p115 (not p117)))
(assert (or p42 p117 (not p118)))
(assert (or (not p42) (not p117) (not p118)))
(assert (or p42 (not p117) p118))
(assert (or (not p42) p117 p118))
(assert (or p42 p117 (not p119)))

(check)