(benchmark p6_driverlogNumeric_s5.smt
  :source {
Formulas from temporal metric planning problems contributed by Jiae Shin.  See
http://cs.nyu.edu/~jiae.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status sat
:category { industrial }
:difficulty { 0 }
  :logic QF_LRA
  :extrapreds ((b11))
  :extrapreds ((b16))
  :extrapreds ((b19))
  :extrapreds ((b23))
  :extrapreds ((b27))
  :extrapreds ((b30))
  :extrapreds ((b32))
  :extrapreds ((b34))
  :extrapreds ((b36))
  :extrapreds ((b38))
  :extrapreds ((b42))
  :extrapreds ((b45))
  :extrapreds ((b48))
  :extrapreds ((b51))
  :extrapreds ((b53))
  :extrapreds ((b55))
  :extrapreds ((b56))
  :extrapreds ((b57))
  :extrapreds ((b59))
  :extrapreds ((b63))
  :extrapreds ((b65))
  :extrapreds ((b68))
  :extrapreds ((b70))
  :extrapreds ((b74))
  :extrapreds ((b77))
  :extrapreds ((b80))
  :extrapreds ((b83))
  :extrapreds ((b85))
  :extrapreds ((b87))
  :extrapreds ((b88))
  :extrapreds ((b89))
  :extrapreds ((b91))
  :extrapreds ((b95))
  :extrapreds ((b98))
  :extrapreds ((b101))
  :extrapreds ((b104))
  :extrapreds ((b106))
  :extrapreds ((b108))
  :extrapreds ((b109))
  :extrapreds ((b110))
  :extrapreds ((b112))
  :extrapreds ((b115))
  :extrapreds ((b117))
  :extrapreds ((b120))
  :extrapreds ((b122))
  :extrapreds ((b125))
  :extrapreds ((b127))
  :extrapreds ((b130))
  :extrapreds ((b132))
  :extrapreds ((b135))
  :extrapreds ((b137))
  :extrapreds ((b138))
  :extrapreds ((b140))
  :extrapreds ((b141))
  :extrapreds ((b143))
  :extrapreds ((b144))
  :extrapreds ((b146))
  :extrapreds ((b147))
  :extrapreds ((b149))
  :extrapreds ((b152))
  :extrapreds ((b155))
  :extrapreds ((b157))
  :extrapreds ((b160))
  :extrapreds ((b162))
  :extrapreds ((b163))
  :extrapreds ((b165))
  :extrapreds ((b166))
  :extrapreds ((b168))
  :extrapreds ((b169))
  :extrapreds ((b171))
  :extrapreds ((b172))
  :extrapreds ((b174))
  :extrapreds ((b176))
  :extrapreds ((b179))
  :extrapreds ((b180))
  :extrapreds ((b181))
  :extrapreds ((b183))
  :extrapreds ((b186))
  :extrapreds ((b187))
  :extrapreds ((b188))
  :extrapreds ((b191))
  :extrapreds ((b197))
  :extrapreds ((b201))
  :extrapreds ((b205))
  :extrapreds ((b208))
  :extrapreds ((b210))
  :extrapreds ((b212))
  :extrapreds ((b215))
  :extrapreds ((b219))
  :extrapreds ((b222))
  :extrapreds ((b225))
  :extrapreds ((b227))
  :extrapreds ((b228))
  :extrapreds ((b229))
  :extrapreds ((b230))
  :extrapreds ((b234))
  :extrapreds ((b238))
  :extrapreds ((b241))
  :extrapreds ((b244))
  :extrapreds ((b246))
  :extrapreds ((b249))
  :extrapreds ((b251))
  :extrapreds ((b253))
  :extrapreds ((b255))
  :extrapreds ((b256))
  :extrapreds ((b257))
  :extrapreds ((b258))
  :extrapreds ((b259))
  :extrapreds ((b261))
  :extrapreds ((b263))
  :extrapreds ((b267))
  :extrapreds ((b270))
  :extrapreds ((b273))
  :extrapreds ((b275))
  :extrapreds ((b278))
  :extrapreds ((b280))
  :extrapreds ((b282))
  :extrapreds ((b284))
  :extrapreds ((b285))
  :extrapreds ((b286))
  :extrapreds ((b287))
  :extrapreds ((b288))
  :extrapreds ((b290))
  :extrapreds ((b292))
  :extrapreds ((b293))
  :extrapreds ((b294))
  :extrapreds ((b295))
  :extrapreds ((b296))
  :extrapreds ((b297))
  :extrapreds ((b298))
  :extrapreds ((b299))
  :extrapreds ((b300))
  :extrapreds ((b301))
  :extrapreds ((b302))
  :extrapreds ((b303))
  :extrapreds ((b304))
  :extrapreds ((b305))
  :extrapreds ((b306))
  :extrapreds ((b307))
  :extrapreds ((b308))
  :extrapreds ((b309))
  :extrapreds ((b312))
  :extrapreds ((b313))
  :extrapreds ((b314))
  :extrapreds ((b315))
  :extrapreds ((b318))
  :extrapreds ((b319))
  :extrapreds ((b322))
  :extrapreds ((b323))
  :extrapreds ((b324))
  :extrapreds ((b326))
  :extrapreds ((b327))
  :extrapreds ((b328))
  :extrapreds ((b329))
  :extrapreds ((b331))
  :extrapreds ((b332))
  :extrapreds ((b334))
  :extrapreds ((b336))
  :extrapreds ((b339))
  :extrapreds ((b344))
  :extrapreds ((b348))
  :extrapreds ((b352))
  :extrapreds ((b355))
  :extrapreds ((b360))
  :extrapreds ((b364))
  :extrapreds ((b368))
  :extrapreds ((b371))
  :extrapreds ((b374))
  :extrapreds ((b377))
  :extrapreds ((b380))
  :extrapreds ((b383))
  :extrapreds ((b386))
  :extrapreds ((b389))
  :extrapreds ((b392))
  :extrapreds ((b395))
  :extrapreds ((b398))
  :extrapreds ((b401))
  :extrapreds ((b404))
  :extrapreds ((b407))
  :extrapreds ((b410))
  :extrapreds ((b413))
  :extrapreds ((b416))
  :extrapreds ((b419))
  :extrapreds ((b422))
  :extrapreds ((b425))
  :extrapreds ((b428))
  :extrapreds ((b431))
  :extrapreds ((b434))
  :extrapreds ((b437))
  :extrapreds ((b440))
  :extrapreds ((b443))
  :extrapreds ((b446))
  :extrapreds ((b449))
  :extrapreds ((b452))
  :extrapreds ((b455))
  :extrapreds ((b458))
  :extrapreds ((b461))
  :extrapreds ((b464))
  :extrapreds ((b469))
  :extrapreds ((b472))
  :extrapreds ((b475))
  :extrapreds ((b478))
  :extrapreds ((b481))
  :extrapreds ((b484))
  :extrapreds ((b487))
  :extrapreds ((b490))
  :extrapreds ((b493))
  :extrapreds ((b496))
  :extrapreds ((b499))
  :extrapreds ((b502))
  :extrapreds ((b505))
  :extrapreds ((b508))
  :extrapreds ((b511))
  :extrapreds ((b514))
  :extrapreds ((b517))
  :extrapreds ((b520))
  :extrapreds ((b523))
  :extrapreds ((b526))
  :extrapreds ((b529))
  :extrapreds ((b532))
  :extrapreds ((b535))
  :extrapreds ((b538))
  :extrapreds ((b541))
  :extrapreds ((b544))
  :extrapreds ((b547))
  :extrapreds ((b550))
  :extrapreds ((b553))
  :extrapreds ((b557))
  :extrapreds ((b561))
  :extrapreds ((b565))
  :extrapreds ((b568))
  :extrapreds ((b572))
  :extrapreds ((b576))
  :extrapreds ((b580))
  :extrapreds ((b585))
  :extrapreds ((b588))
  :extrapreds ((b591))
  :extrapreds ((b594))
  :extrapreds ((b597))
  :extrapreds ((b600))
  :extrapreds ((b603))
  :extrapreds ((b606))
  :extrapreds ((b609))
  :extrapreds ((b612))
  :extrapreds ((b615))
  :extrapreds ((b619))
  :extrapreds ((b623))
  :extrapreds ((b628))
  :extrapreds ((b632))
  :extrapreds ((b636))
  :extrapreds ((b641))
  :extrapreds ((b646))
  :extrapreds ((b649))
  :extrapreds ((b653))
  :extrapreds ((b658))
  :extrapreds ((b662))
  :extrapreds ((b666))
  :extrapreds ((b670))
  :extrapreds ((b673))
  :extrapreds ((b676))
  :extrapreds ((b679))
  :extrapreds ((b683))
  :extrapreds ((b686))
  :extrapreds ((b689))
  :extrapreds ((b692))
  :extrapreds ((b695))
  :extrapreds ((b698))
  :extrapreds ((b701))
  :extrapreds ((b704))
  :extrapreds ((b707))
  :extrapreds ((b710))
  :extrapreds ((b713))
  :extrapreds ((b716))
  :extrapreds ((b719))
  :extrapreds ((b722))
  :extrapreds ((b727))
  :extrapreds ((b731))
  :extrapreds ((b735))
  :extrapreds ((b740))
  :extrapreds ((b743))
  :extrapreds ((b746))
  :extrapreds ((b749))
  :extrapreds ((b752))
  :extrapreds ((b757))
  :extrapreds ((b761))
  :extrapreds ((b765))
  :extrapreds ((b769))
  :extrapreds ((b772))
  :extrapreds ((b775))
  :extrapreds ((b778))
  :extrapreds ((b782))
  :extrapreds ((b786))
  :extrapreds ((b789))
  :extrapreds ((b792))
  :extrapreds ((b795))
  :extrapreds ((b798))
  :extrapreds ((b801))
  :extrapreds ((b804))
  :extrapreds ((b807))
  :extrapreds ((b810))
  :extrapreds ((b813))
  :extrapreds ((b816))
  :extrapreds ((b819))
  :extrapreds ((b822))
  :extrapreds ((b825))
  :extrapreds ((b829))
  :extrapreds ((b834))
  :extrapreds ((b838))
  :extrapreds ((b842))
  :extrapreds ((b847))
  :extrapreds ((b850))
  :extrapreds ((b853))
  :extrapreds ((b856))
  :extrapreds ((b860))
  :extrapreds ((b865))
  :extrapreds ((b869))
  :extrapreds ((b873))
  :extrapreds ((b877))
  :extrapreds ((b880))
  :extrapreds ((b883))
  :extrapreds ((b886))
  :extrapreds ((b889))
  :extrapreds ((b893))
  :extrapreds ((b896))
  :extrapreds ((b899))
  :extrapreds ((b902))
  :extrapreds ((b905))
  :extrapreds ((b908))
  :extrapreds ((b911))
  :extrapreds ((b914))
  :extrapreds ((b917))
  :extrapreds ((b920))
  :extrapreds ((b923))
  :extrapreds ((b927))
  :extrapreds ((b930))
  :extrapreds ((b933))
  :extrapreds ((b12))
  :extrapreds ((b13))
  :extrapreds ((b14))
  :extrapreds ((b15))
  :extrapreds ((b17))
  :extrapreds ((b18))
  :extrapreds ((b20))
  :extrapreds ((b21))
  :extrapreds ((b22))
  :extrapreds ((b24))
  :extrapreds ((b25))
  :extrapreds ((b26))
  :extrapreds ((b28))
  :extrapreds ((b29))
  :extrapreds ((b31))
  :extrapreds ((b33))
  :extrapreds ((b35))
  :extrapreds ((b37))
  :extrapreds ((b39))
  :extrapreds ((b40))
  :extrapreds ((b41))
  :extrapreds ((b43))
  :extrapreds ((b44))
  :extrapreds ((b46))
  :extrapreds ((b47))
  :extrapreds ((b49))
  :extrapreds ((b50))
  :extrapreds ((b52))
  :extrapreds ((b54))
  :extrapreds ((b58))
  :extrapreds ((b60))
  :extrapreds ((b61))
  :extrapreds ((b62))
  :extrapreds ((b64))
  :extrapreds ((b66))
  :extrapreds ((b67))
  :extrapreds ((b69))
  :extrapreds ((b71))
  :extrapreds ((b72))
  :extrapreds ((b73))
  :extrapreds ((b75))
  :extrapreds ((b76))
  :extrapreds ((b78))
  :extrapreds ((b79))
  :extrapreds ((b81))
  :extrapreds ((b82))
  :extrapreds ((b84))
  :extrapreds ((b86))
  :extrapreds ((b90))
  :extrapreds ((b92))
  :extrapreds ((b93))
  :extrapreds ((b94))
  :extrapreds ((b96))
  :extrapreds ((b97))
  :extrapreds ((b99))
  :extrapreds ((b100))
  :extrapreds ((b102))
  :extrapreds ((b103))
  :extrapreds ((b105))
  :extrapreds ((b107))
  :extrapreds ((b111))
  :extrapreds ((b113))
  :extrapreds ((b114))
  :extrapreds ((b116))
  :extrapreds ((b118))
  :extrapreds ((b119))
  :extrapreds ((b121))
  :extrapreds ((b123))
  :extrapreds ((b124))
  :extrapreds ((b126))
  :extrapreds ((b128))
  :extrapreds ((b129))
  :extrapreds ((b131))
  :extrapreds ((b133))
  :extrapreds ((b134))
  :extrapreds ((b136))
  :extrapreds ((b139))
  :extrapreds ((b142))
  :extrapreds ((b145))
  :extrapreds ((b148))
  :extrapreds ((b150))
  :extrapreds ((b151))
  :extrapreds ((b153))
  :extrapreds ((b154))
  :extrapreds ((b156))
  :extrapreds ((b158))
  :extrapreds ((b159))
  :extrapreds ((b161))
  :extrapreds ((b164))
  :extrapreds ((b167))
  :extrapreds ((b170))
  :extrapreds ((b173))
  :extrapreds ((b175))
  :extrapreds ((b177))
  :extrapreds ((b178))
  :extrapreds ((b182))
  :extrapreds ((b184))
  :extrapreds ((b185))
  :extrapreds ((b189))
  :extrapreds ((b190))
  :extrapreds ((b192))
  :extrapreds ((b193))
  :extrapreds ((b194))
  :extrapreds ((b195))
  :extrapreds ((b196))
  :extrapreds ((b198))
  :extrapreds ((b199))
  :extrapreds ((b200))
  :extrapreds ((b202))
  :extrapreds ((b203))
  :extrapreds ((b204))
  :extrapreds ((b206))
  :extrapreds ((b207))
  :extrapreds ((b209))
  :extrapreds ((b211))
  :extrapreds ((b213))
  :extrapreds ((b214))
  :extrapreds ((b216))
  :extrapreds ((b217))
  :extrapreds ((b218))
  :extrapreds ((b220))
  :extrapreds ((b221))
  :extrapreds ((b223))
  :extrapreds ((b224))
  :extrapreds ((b226))
  :extrapreds ((b231))
  :extrapreds ((b232))
  :extrapreds ((b233))
  :extrapreds ((b235))
  :extrapreds ((b236))
  :extrapreds ((b237))
  :extrapreds ((b239))
  :extrapreds ((b240))
  :extrapreds ((b242))
  :extrapreds ((b243))
  :extrapreds ((b245))
  :extrapreds ((b247))
  :extrapreds ((b248))
  :extrapreds ((b250))
  :extrapreds ((b252))
  :extrapreds ((b254))
  :extrapreds ((b260))
  :extrapreds ((b262))
  :extrapreds ((b264))
  :extrapreds ((b265))
  :extrapreds ((b266))
  :extrapreds ((b268))
  :extrapreds ((b269))
  :extrapreds ((b271))
  :extrapreds ((b272))
  :extrapreds ((b274))
  :extrapreds ((b276))
  :extrapreds ((b277))
  :extrapreds ((b279))
  :extrapreds ((b281))
  :extrapreds ((b283))
  :extrapreds ((b289))
  :extrapreds ((b291))
  :extrapreds ((b310))
  :extrapreds ((b311))
  :extrapreds ((b316))
  :extrapreds ((b317))
  :extrapreds ((b320))
  :extrapreds ((b321))
  :extrapreds ((b325))
  :extrapreds ((b330))
  :extrapreds ((b333))
  :extrapreds ((b342))
  :extrapreds ((b358))
  :extrapreds ((b466))
  :extrapreds ((b467))
  :extrapreds ((b582))
  :extrapreds ((b583))
  :extrapreds ((b638))
  :extrapreds ((b639))
  :extrapreds ((b643))
  :extrapreds ((b644))
  :extrapreds ((b651))
  :extrapreds ((b655))
  :extrapreds ((b656))
  :extrapreds ((b660))
  :extrapreds ((b664))
  :extrapreds ((b668))
  :extrapreds ((b681))
  :extrapreds ((b724))
  :extrapreds ((b725))
  :extrapreds ((b729))
  :extrapreds ((b733))
  :extrapreds ((b737))
  :extrapreds ((b738))
  :extrapreds ((b754))
  :extrapreds ((b755))
  :extrapreds ((b759))
  :extrapreds ((b763))
  :extrapreds ((b767))
  :extrapreds ((b780))
  :extrapreds ((b784))
  :extrapreds ((b831))
  :extrapreds ((b832))
  :extrapreds ((b836))
  :extrapreds ((b840))
  :extrapreds ((b844))
  :extrapreds ((b845))
  :extrapreds ((b858))
  :extrapreds ((b862))
  :extrapreds ((b863))
  :extrapreds ((b867))
  :extrapreds ((b871))
  :extrapreds ((b875))
  :extrapreds ((b891))
  :extrapreds ((b935))
  :extrapreds ((b936))
  :extrapreds ((b937))
  :extrapreds ((b938))
  :extrapreds ((b939))
  :extrapreds ((b940))
  :extrapreds ((b941))
  :extrapreds ((b942))
  :extrapreds ((b943))
  :extrapreds ((b944))
  :extrapreds ((b945))
  :extrafuns ((r1 Real))
  :extrafuns ((r2 Real))
  :extrafuns ((r3 Real))
  :extrafuns ((r4 Real))
  :extrafuns ((r5 Real))
  :extrafuns ((r6 Real))
  :extrafuns ((r7 Real))
  :extrafuns ((r8 Real))
  :extrafuns ((r9 Real))
  :extrafuns ((r10 Real))
  :extrafuns ((r11 Real))
  :extrafuns ((r12 Real))
  :extrafuns ((r13 Real))
  :extrafuns ((r14 Real))
  :extrafuns ((r15 Real))
  :extrafuns ((r16 Real))
  :extrafuns ((r17 Real))
  :extrafuns ((r18 Real))
  :extrafuns ((r19 Real))
  :extrafuns ((r20 Real))
  :extrafuns ((r21 Real))
  :extrafuns ((r22 Real))
  :extrafuns ((r23 Real))
  :extrafuns ((r24 Real))
  :extrafuns ((r25 Real))
  :extrafuns ((r26 Real))
  :extrafuns ((r27 Real))
  :extrafuns ((r28 Real))
  :extrafuns ((r29 Real))
  :extrafuns ((r30 Real))
  :extrafuns ((r31 Real))
  :extrafuns ((r32 Real))
  :extrafuns ((r33 Real))
  :extrafuns ((r34 Real))
  :extrafuns ((r35 Real))
  :extrafuns ((r36 Real))
  :extrafuns ((r37 Real))
  :extrafuns ((r38 Real))
  :extrafuns ((r39 Real))
  :extrafuns ((r40 Real))
  :extrafuns ((r41 Real))
  :extrafuns ((r42 Real))
  :extrafuns ((r43 Real))
  :extrafuns ((r44 Real))
  :extrafuns ((r45 Real))
  :extrafuns ((r46 Real))
  :extrafuns ((r47 Real))
  :extrafuns ((r48 Real))
  :extrafuns ((r49 Real))
  :extrafuns ((r50 Real))
  :extrafuns ((r51 Real))
  :extrafuns ((r52 Real))
  :extrafuns ((r53 Real))
  :extrafuns ((r54 Real))
  :extrafuns ((r55 Real))
  :extrafuns ((r56 Real))
  :extrafuns ((r57 Real))
  :extrafuns ((r58 Real))
  :extrafuns ((r59 Real))
  :extrafuns ((r60 Real))
  :extrafuns ((r61 Real))
  :extrafuns ((r62 Real))
  :extrafuns ((r63 Real))
  :extrafuns ((r64 Real))
  :extrafuns ((r65 Real))
  :extrafuns ((r66 Real))
  :extrafuns ((r67 Real))
  :extrafuns ((r68 Real))
  :extrafuns ((r69 Real))
  :extrafuns ((r70 Real))
  :extrafuns ((r71 Real))
  :extrafuns ((r72 Real))
  :extrafuns ((r73 Real))
  :extrafuns ((r74 Real))
  :extrafuns ((r75 Real))
  :extrafuns ((r76 Real))
  :extrafuns ((r77 Real))
  :extrafuns ((r78 Real))
  :extrafuns ((r79 Real))
  :extrafuns ((r80 Real))
  :extrafuns ((r81 Real))
  :extrafuns ((r82 Real))
  :extrafuns ((r83 Real))
  :extrafuns ((r84 Real))
  :extrafuns ((r85 Real))
  :extrafuns ((r86 Real))
  :extrafuns ((r87 Real))
  :extrafuns ((r88 Real))
  :extrafuns ((r89 Real))
  :extrafuns ((r90 Real))
  :extrafuns ((r91 Real))
  :extrafuns ((r92 Real))
  :extrafuns ((r93 Real))
  :extrafuns ((r94 Real))
  :extrafuns ((r95 Real))
  :extrafuns ((r96 Real))
  :extrafuns ((r97 Real))
  :extrafuns ((r98 Real))
  :extrafuns ((r99 Real))
  :extrafuns ((r100 Real))
  :extrafuns ((r101 Real))
  :extrafuns ((r102 Real))
  :extrafuns ((r103 Real))
  :extrafuns ((r104 Real))
  :extrafuns ((r105 Real))
  :extrafuns ((r106 Real))
  :extrafuns ((r107 Real))
  :extrafuns ((r108 Real))
  :extrafuns ((r109 Real))
  :extrafuns ((r110 Real))
  :extrafuns ((r111 Real))
  :extrafuns ((r112 Real))
  :extrafuns ((r113 Real))
  :extrafuns ((r114 Real))
  :extrafuns ((r115 Real))
  :extrafuns ((r116 Real))
  :extrafuns ((r117 Real))
  :extrafuns ((r118 Real))
  :extrafuns ((r119 Real))
  :extrafuns ((r120 Real))
  :extrafuns ((r121 Real))
  :extrafuns ((r122 Real))
  :extrafuns ((r123 Real))
  :extrafuns ((r124 Real))
  :extrafuns ((r125 Real))
  :extrafuns ((r126 Real))
  :extrafuns ((r127 Real))
  :extrafuns ((r128 Real))
  :extrafuns ((r129 Real))
  :extrafuns ((r130 Real))
  :extrafuns ((r131 Real))
  :extrafuns ((r132 Real))
  :extrafuns ((r133 Real))
  :extrafuns ((r134 Real))
  :extrafuns ((r135 Real))
  :extrafuns ((r136 Real))
  :extrafuns ((r137 Real))
  :extrafuns ((r138 Real))
  :extrafuns ((r139 Real))
  :extrafuns ((r140 Real))
  :extrafuns ((r141 Real))
  :extrafuns ((r142 Real))
  :extrafuns ((r143 Real))
  :extrafuns ((r144 Real))
  :extrafuns ((r145 Real))
  :extrafuns ((r146 Real))
  :extrafuns ((r147 Real))
  :extrafuns ((r148 Real))
  :extrafuns ((r149 Real))
  :extrafuns ((r150 Real))
  :extrafuns ((r151 Real))
  :extrafuns ((r152 Real))
  :extrafuns ((r153 Real))
  :extrafuns ((r154 Real))
  :extrafuns ((r155 Real))
  :extrafuns ((r156 Real))
  :extrafuns ((r157 Real))
  :extrafuns ((r158 Real))
  :extrafuns ((r159 Real))
  :extrafuns ((r160 Real))
  :extrafuns ((r161 Real))
  :extrafuns ((r162 Real))
  :extrafuns ((r163 Real))
  :extrafuns ((r164 Real))
  :extrafuns ((r165 Real))
  :extrafuns ((r166 Real))
  :extrafuns ((r167 Real))
  :extrafuns ((r168 Real))
  :extrafuns ((r169 Real))
  :extrafuns ((r170 Real))
  :extrafuns ((r171 Real))
  :extrafuns ((r172 Real))
  :extrafuns ((r173 Real))
  :extrafuns ((r174 Real))
  :extrafuns ((r175 Real))
  :extrafuns ((r176 Real))
  :extrafuns ((r177 Real))
  :extrafuns ((r178 Real))
  :extrafuns ((r179 Real))
  :extrafuns ((r180 Real))
  :extrafuns ((r181 Real))
  :extrafuns ((r182 Real))
  :extrafuns ((r183 Real))
  :extrafuns ((r184 Real))
  :extrafuns ((r185 Real))
  :extrafuns ((r186 Real))
  :extrafuns ((r187 Real))
  :extrafuns ((r188 Real))
  :extrafuns ((r189 Real))
  :extrafuns ((r190 Real))
  :extrafuns ((r191 Real))
  :extrafuns ((r192 Real))
  :extrafuns ((r193 Real))
  :extrafuns ((r194 Real))
  :extrafuns ((r195 Real))
  :extrafuns ((r196 Real))
  :extrafuns ((r197 Real))
  :extrafuns ((r198 Real))
  :extrafuns ((r199 Real))
  :extrafuns ((r200 Real))
  :extrafuns ((r201 Real))
  :extrafuns ((r202 Real))
  :extrafuns ((r203 Real))
  :extrafuns ((r204 Real))
  :extrafuns ((r205 Real))
  :extrafuns ((r206 Real))
  :extrafuns ((r207 Real))
  :extrafuns ((r208 Real))
  :extrafuns ((r209 Real))
  :extrafuns ((r210 Real))
  :extrafuns ((r211 Real))
  :extrafuns ((r212 Real))
  :extrafuns ((r213 Real))
  :extrafuns ((r214 Real))
  :extrafuns ((r215 Real))
  :extrafuns ((r216 Real))
  :extrafuns ((r217 Real))
  :extrafuns ((r218 Real))
  :assumption
(or (not b11)  b12 )
  :assumption
(or (not b11)  (not b13) )
  :assumption
(or (not b11)  b14 )
  :assumption
(or (not b11)  b15 )
  :assumption
(or (not b16)  b17 )
  :assumption
(or (not b16)  (not b18) )
  :assumption
(or b12  (not b19) )
  :assumption
(or (not b19)  (not b20) )
  :assumption
(or (not b19)  b21 )
  :assumption
(or (not b19)  b22 )
  :assumption
(or b12  (not b23) )
  :assumption
(or (not b23)  (not b24) )
  :assumption
(or (not b23)  b25 )
  :assumption
(or (not b23)  b26 )
  :assumption
(or (not b27)  b28 )
  :assumption
(or (not b13)  (not b27) )
  :assumption
(or (not b27)  b29 )
  :assumption
(or b15  (not b27) )
  :assumption
(or (not b30)  b31 )
  :assumption
(or (not b18)  (not b30) )
  :assumption
(or b28  (not b32) )
  :assumption
(or (not b20)  (not b32) )
  :assumption
(or (not b32)  b33 )
  :assumption
(or b22  (not b32) )
  :assumption
(or b28  (not b34) )
  :assumption
(or (not b24)  (not b34) )
  :assumption
(or (not b34)  b35 )
  :assumption
(or b26  (not b34) )
  :assumption
(or (not b36)  b37 )
  :assumption
(or (not b24)  (not b36) )
  :assumption
(or b26  (not b36) )
  :assumption
(or (not b38)  b39 )
  :assumption
(or (not b38)  (not b40) )
  :assumption
(or b14  (not b38) )
  :assumption
(or (not b38)  b41 )
  :assumption
(or (not b42)  b43 )
  :assumption
(or (not b42)  (not b44) )
  :assumption
(or b39  (not b45) )
  :assumption
(or (not b45)  (not b46) )
  :assumption
(or b21  (not b45) )
  :assumption
(or (not b45)  b47 )
  :assumption
(or b39  (not b48) )
  :assumption
(or (not b48)  (not b49) )
  :assumption
(or b25  (not b48) )
  :assumption
(or (not b48)  b50 )
  :assumption
(or (not b51)  b52 )
  :assumption
(or (not b40)  (not b51) )
  :assumption
(or b29  (not b51) )
  :assumption
(or b41  (not b51) )
  :assumption
(or (not b53)  b54 )
  :assumption
(or (not b44)  (not b53) )
  :assumption
(or b52  (not b55) )
  :assumption
(or (not b46)  (not b55) )
  :assumption
(or b33  (not b55) )
  :assumption
(or b47  (not b55) )
  :assumption
(or b52  (not b56) )
  :assumption
(or (not b49)  (not b56) )
  :assumption
(or b35  (not b56) )
  :assumption
(or b50  (not b56) )
  :assumption
(or (not b57)  b58 )
  :assumption
(or (not b49)  (not b57) )
  :assumption
(or b50  (not b57) )
  :assumption
(or (not b59)  b60 )
  :assumption
(or (not b59)  (not b61) )
  :assumption
(or b25  (not b59) )
  :assumption
(or (not b59)  b62 )
  :assumption
(or (not b63)  b64 )
  :assumption
(or (not b61)  (not b63) )
  :assumption
(or b35  (not b63) )
  :assumption
(or b62  (not b63) )
  :assumption
(or (not b65)  b66 )
  :assumption
(or (not b65)  (not b67) )
  :assumption
(or (not b68)  b69 )
  :assumption
(or (not b61)  (not b68) )
  :assumption
(or b62  (not b68) )
  :assumption
(or (not b70)  b71 )
  :assumption
(or (not b70)  (not b72) )
  :assumption
(or b14  (not b70) )
  :assumption
(or (not b70)  b73 )
  :assumption
(or (not b74)  b75 )
  :assumption
(or (not b74)  (not b76) )
  :assumption
(or b71  (not b77) )
  :assumption
(or (not b77)  (not b78) )
  :assumption
(or b21  (not b77) )
  :assumption
(or (not b77)  b79 )
  :assumption
(or b71  (not b80) )
  :assumption
(or (not b80)  (not b81) )
  :assumption
(or b25  (not b80) )
  :assumption
(or (not b80)  b82 )
  :assumption
(or (not b83)  b84 )
  :assumption
(or (not b72)  (not b83) )
  :assumption
(or b29  (not b83) )
  :assumption
(or b73  (not b83) )
  :assumption
(or (not b85)  b86 )
  :assumption
(or (not b76)  (not b85) )
  :assumption
(or b84  (not b87) )
  :assumption
(or (not b78)  (not b87) )
  :assumption
(or b33  (not b87) )
  :assumption
(or b79  (not b87) )
  :assumption
(or b84  (not b88) )
  :assumption
(or (not b81)  (not b88) )
  :assumption
(or b35  (not b88) )
  :assumption
(or b82  (not b88) )
  :assumption
(or (not b89)  b90 )
  :assumption
(or (not b81)  (not b89) )
  :assumption
(or b82  (not b89) )
  :assumption
(or (not b91)  b92 )
  :assumption
(or (not b91)  (not b93) )
  :assumption
(or b14  (not b91) )
  :assumption
(or (not b91)  b94 )
  :assumption
(or (not b95)  b96 )
  :assumption
(or (not b95)  (not b97) )
  :assumption
(or b92  (not b98) )
  :assumption
(or (not b98)  (not b99) )
  :assumption
(or b21  (not b98) )
  :assumption
(or (not b98)  b100 )
  :assumption
(or b92  (not b101) )
  :assumption
(or (not b101)  (not b102) )
  :assumption
(or b25  (not b101) )
  :assumption
(or (not b101)  b103 )
  :assumption
(or (not b104)  b105 )
  :assumption
(or (not b93)  (not b104) )
  :assumption
(or b29  (not b104) )
  :assumption
(or b94  (not b104) )
  :assumption
(or (not b106)  b107 )
  :assumption
(or (not b97)  (not b106) )
  :assumption
(or b105  (not b108) )
  :assumption
(or (not b99)  (not b108) )
  :assumption
(or b33  (not b108) )
  :assumption
(or b100  (not b108) )
  :assumption
(or b105  (not b109) )
  :assumption
(or (not b102)  (not b109) )
  :assumption
(or b35  (not b109) )
  :assumption
(or b103  (not b109) )
  :assumption
(or (not b110)  b111 )
  :assumption
(or (not b102)  (not b110) )
  :assumption
(or b103  (not b110) )
  :assumption
(or b15  (not b112) )
  :assumption
(or (not b112)  (not b113) )
  :assumption
(or (not b112)  b114 )
  :assumption
(or b17  (not b112) )
  :assumption
(or b22  (not b115) )
  :assumption
(or (not b113)  (not b115) )
  :assumption
(or (not b115)  b116 )
  :assumption
(or b17  (not b115) )
  :assumption
(or (not b117)  (not b118) )
  :assumption
(or (not b117)  b119 )
  :assumption
(or b12  (not b117) )
  :assumption
(or b26  (not b120) )
  :assumption
(or (not b113)  (not b120) )
  :assumption
(or (not b120)  b121 )
  :assumption
(or b17  (not b120) )
  :assumption
(or b15  (not b122) )
  :assumption
(or (not b122)  (not b123) )
  :assumption
(or (not b122)  b124 )
  :assumption
(or b31  (not b122) )
  :assumption
(or b22  (not b125) )
  :assumption
(or (not b123)  (not b125) )
  :assumption
(or (not b125)  b126 )
  :assumption
(or b31  (not b125) )
  :assumption
(or (not b127)  (not b128) )
  :assumption
(or (not b127)  b129 )
  :assumption
(or b28  (not b127) )
  :assumption
(or b26  (not b130) )
  :assumption
(or (not b123)  (not b130) )
  :assumption
(or (not b130)  b131 )
  :assumption
(or b31  (not b130) )
  :assumption
(or (not b132)  (not b133) )
  :assumption
(or (not b132)  b134 )
  :assumption
(or b37  (not b132) )
  :assumption
(or b41  (not b135) )
  :assumption
(or (not b135)  (not b136) )
  :assumption
(or b114  (not b135) )
  :assumption
(or b43  (not b135) )
  :assumption
(or b47  (not b137) )
  :assumption
(or (not b136)  (not b137) )
  :assumption
(or b116  (not b137) )
  :assumption
(or b43  (not b137) )
  :assumption
(or (not b138)  (not b139) )
  :assumption
(or b119  (not b138) )
  :assumption
(or b39  (not b138) )
  :assumption
(or b50  (not b140) )
  :assumption
(or (not b136)  (not b140) )
  :assumption
(or b121  (not b140) )
  :assumption
(or b43  (not b140) )
  :assumption
(or b41  (not b141) )
  :assumption
(or (not b141)  (not b142) )
  :assumption
(or b124  (not b141) )
  :assumption
(or b54  (not b141) )
  :assumption
(or b47  (not b143) )
  :assumption
(or (not b142)  (not b143) )
  :assumption
(or b126  (not b143) )
  :assumption
(or b54  (not b143) )
  :assumption
(or (not b144)  (not b145) )
  :assumption
(or b129  (not b144) )
  :assumption
(or b52  (not b144) )
  :assumption
(or b50  (not b146) )
  :assumption
(or (not b142)  (not b146) )
  :assumption
(or b131  (not b146) )
  :assumption
(or b54  (not b146) )
  :assumption
(or (not b147)  (not b148) )
  :assumption
(or b134  (not b147) )
  :assumption
(or b58  (not b147) )
  :assumption
(or (not b149)  (not b150) )
  :assumption
(or (not b149)  b151 )
  :assumption
(or b60  (not b149) )
  :assumption
(or (not b152)  (not b153) )
  :assumption
(or (not b152)  b154 )
  :assumption
(or b64  (not b152) )
  :assumption
(or b62  (not b155) )
  :assumption
(or (not b155)  (not b156) )
  :assumption
(or b66  (not b155) )
  :assumption
(or (not b157)  (not b158) )
  :assumption
(or (not b157)  b159 )
  :assumption
(or b69  (not b157) )
  :assumption
(or b73  (not b160) )
  :assumption
(or (not b160)  (not b161) )
  :assumption
(or b114  (not b160) )
  :assumption
(or b75  (not b160) )
  :assumption
(or b79  (not b162) )
  :assumption
(or (not b161)  (not b162) )
  :assumption
(or b116  (not b162) )
  :assumption
(or b75  (not b162) )
  :assumption
(or (not b163)  (not b164) )
  :assumption
(or b119  (not b163) )
  :assumption
(or b71  (not b163) )
  :assumption
(or b82  (not b165) )
  :assumption
(or (not b161)  (not b165) )
  :assumption
(or b121  (not b165) )
  :assumption
(or b75  (not b165) )
  :assumption
(or b73  (not b166) )
  :assumption
(or (not b166)  (not b167) )
  :assumption
(or b124  (not b166) )
  :assumption
(or b86  (not b166) )
  :assumption
(or b79  (not b168) )
  :assumption
(or (not b167)  (not b168) )
  :assumption
(or b126  (not b168) )
  :assumption
(or b86  (not b168) )
  :assumption
(or (not b169)  (not b170) )
  :assumption
(or b129  (not b169) )
  :assumption
(or b84  (not b169) )
  :assumption
(or b82  (not b171) )
  :assumption
(or (not b167)  (not b171) )
  :assumption
(or b131  (not b171) )
  :assumption
(or b86  (not b171) )
  :assumption
(or (not b172)  (not b173) )
  :assumption
(or b134  (not b172) )
  :assumption
(or b90  (not b172) )
  :assumption
(or b94  (not b174) )
  :assumption
(or (not b174)  (not b175) )
  :assumption
(or b114  (not b174) )
  :assumption
(or b96  (not b174) )
  :assumption
(or (not b176)  (not b177) )
  :assumption
(or (not b176)  b178 )
  :assumption
(or b92  (not b176) )
  :assumption
(or b100  (not b179) )
  :assumption
(or (not b175)  (not b179) )
  :assumption
(or b116  (not b179) )
  :assumption
(or b96  (not b179) )
  :assumption
(or b103  (not b180) )
  :assumption
(or (not b175)  (not b180) )
  :assumption
(or b121  (not b180) )
  :assumption
(or b96  (not b180) )
  :assumption
(or b94  (not b181) )
  :assumption
(or (not b181)  (not b182) )
  :assumption
(or b124  (not b181) )
  :assumption
(or b107  (not b181) )
  :assumption
(or (not b183)  (not b184) )
  :assumption
(or (not b183)  b185 )
  :assumption
(or b105  (not b183) )
  :assumption
(or b100  (not b186) )
  :assumption
(or (not b182)  (not b186) )
  :assumption
(or b126  (not b186) )
  :assumption
(or b107  (not b186) )
  :assumption
(or b103  (not b187) )
  :assumption
(or (not b182)  (not b187) )
  :assumption
(or b131  (not b187) )
  :assumption
(or b107  (not b187) )
  :assumption
(or (not b188)  (not b189) )
  :assumption
(or (not b188)  b190 )
  :assumption
(or b111  (not b188) )
  :assumption
(or (not b191)  (not b192) )
  :assumption
(or (not b191)  b193 )
  :assumption
(or (not b191)  (not b194) )
  :assumption
(or b114  (not b191) )
  :assumption
(or (not b191)  b195 )
  :assumption
(or (not b191)  b196 )
  :assumption
(or (not b197)  (not b198) )
  :assumption
(or (not b197)  b199 )
  :assumption
(or (not b197)  (not b200) )
  :assumption
(or b14  (not b197) )
  :assumption
(or b194  (not b197) )
  :assumption
(or b192  (not b197) )
  :assumption
(or (not b201)  (not b202) )
  :assumption
(or (not b201)  b203 )
  :assumption
(or (not b201)  (not b204) )
  :assumption
(or (not b196)  (not b205) )
  :assumption
(or (not b205)  b206 )
  :assumption
(or (not b205)  (not b207) )
  :assumption
(or b204  (not b205) )
  :assumption
(or b202  (not b205) )
  :assumption
(or (not b192)  (not b208) )
  :assumption
(or b193  (not b208) )
  :assumption
(or (not b208)  (not b209) )
  :assumption
(or b116  (not b208) )
  :assumption
(or b207  (not b208) )
  :assumption
(or b196  (not b208) )
  :assumption
(or (not b198)  (not b210) )
  :assumption
(or b199  (not b210) )
  :assumption
(or (not b210)  (not b211) )
  :assumption
(or b21  (not b210) )
  :assumption
(or b209  (not b210) )
  :assumption
(or b192  (not b210) )
  :assumption
(or (not b198)  (not b212) )
  :assumption
(or b199  (not b212) )
  :assumption
(or (not b212)  (not b213) )
  :assumption
(or b25  (not b212) )
  :assumption
(or (not b212)  b214 )
  :assumption
(or b192  (not b212) )
  :assumption
(or (not b215)  (not b216) )
  :assumption
(or (not b215)  b217 )
  :assumption
(or (not b194)  (not b215) )
  :assumption
(or b124  (not b215) )
  :assumption
(or b195  (not b215) )
  :assumption
(or (not b215)  b218 )
  :assumption
(or (not b219)  (not b220) )
  :assumption
(or (not b219)  b221 )
  :assumption
(or (not b200)  (not b219) )
  :assumption
(or b29  (not b219) )
  :assumption
(or b194  (not b219) )
  :assumption
(or b216  (not b219) )
  :assumption
(or (not b222)  (not b223) )
  :assumption
(or (not b222)  b224 )
  :assumption
(or (not b204)  (not b222) )
  :assumption
(or (not b218)  (not b225) )
  :assumption
(or (not b225)  b226 )
  :assumption
(or (not b207)  (not b225) )
  :assumption
(or b204  (not b225) )
  :assumption
(or b223  (not b225) )
  :assumption
(or (not b216)  (not b227) )
  :assumption
(or b217  (not b227) )
  :assumption
(or (not b209)  (not b227) )
  :assumption
(or b126  (not b227) )
  :assumption
(or b207  (not b227) )
  :assumption
(or b218  (not b227) )
  :assumption
(or (not b220)  (not b228) )
  :assumption
(or b221  (not b228) )
  :assumption
(or (not b211)  (not b228) )
  :assumption
(or b33  (not b228) )
  :assumption
(or b209  (not b228) )
  :assumption
(or b216  (not b228) )
  :assumption
(or (not b220)  (not b229) )
  :assumption
(or b221  (not b229) )
  :assumption
(or (not b213)  (not b229) )
  :assumption
(or b35  (not b229) )
  :assumption
(or b214  (not b229) )
  :assumption
(or b216  (not b229) )
  :assumption
(or (not b230)  (not b231) )
  :assumption
(or (not b230)  b232 )
  :assumption
(or (not b213)  (not b230) )
  :assumption
(or b214  (not b230) )
  :assumption
(or (not b230)  b233 )
  :assumption
(or (not b192)  (not b234) )
  :assumption
(or (not b234)  b235 )
  :assumption
(or (not b234)  (not b236) )
  :assumption
(or b114  (not b234) )
  :assumption
(or (not b234)  b237 )
  :assumption
(or b196  (not b234) )
  :assumption
(or (not b198)  (not b238) )
  :assumption
(or (not b238)  b239 )
  :assumption
(or (not b238)  (not b240) )
  :assumption
(or b14  (not b238) )
  :assumption
(or b236  (not b238) )
  :assumption
(or b192  (not b238) )
  :assumption
(or (not b192)  (not b241) )
  :assumption
(or b235  (not b241) )
  :assumption
(or (not b241)  (not b242) )
  :assumption
(or b116  (not b241) )
  :assumption
(or (not b241)  b243 )
  :assumption
(or b196  (not b241) )
  :assumption
(or (not b198)  (not b244) )
  :assumption
(or b239  (not b244) )
  :assumption
(or (not b244)  (not b245) )
  :assumption
(or b21  (not b244) )
  :assumption
(or b242  (not b244) )
  :assumption
(or b192  (not b244) )
  :assumption
(or (not b192)  (not b246) )
  :assumption
(or b235  (not b246) )
  :assumption
(or (not b246)  (not b247) )
  :assumption
(or b121  (not b246) )
  :assumption
(or (not b246)  b248 )
  :assumption
(or b196  (not b246) )
  :assumption
(or (not b198)  (not b249) )
  :assumption
(or b239  (not b249) )
  :assumption
(or (not b249)  (not b250) )
  :assumption
(or b25  (not b249) )
  :assumption
(or b247  (not b249) )
  :assumption
(or b192  (not b249) )
  :assumption
(or (not b216)  (not b251) )
  :assumption
(or (not b251)  b252 )
  :assumption
(or (not b236)  (not b251) )
  :assumption
(or b124  (not b251) )
  :assumption
(or b237  (not b251) )
  :assumption
(or b218  (not b251) )
  :assumption
(or (not b220)  (not b253) )
  :assumption
(or (not b253)  b254 )
  :assumption
(or (not b240)  (not b253) )
  :assumption
(or b29  (not b253) )
  :assumption
(or b236  (not b253) )
  :assumption
(or b216  (not b253) )
  :assumption
(or (not b216)  (not b255) )
  :assumption
(or b252  (not b255) )
  :assumption
(or (not b242)  (not b255) )
  :assumption
(or b126  (not b255) )
  :assumption
(or b243  (not b255) )
  :assumption
(or b218  (not b255) )
  :assumption
(or (not b220)  (not b256) )
  :assumption
(or b254  (not b256) )
  :assumption
(or (not b245)  (not b256) )
  :assumption
(or b33  (not b256) )
  :assumption
(or b242  (not b256) )
  :assumption
(or b216  (not b256) )
  :assumption
(or (not b216)  (not b257) )
  :assumption
(or b252  (not b257) )
  :assumption
(or (not b247)  (not b257) )
  :assumption
(or b131  (not b257) )
  :assumption
(or b248  (not b257) )
  :assumption
(or b218  (not b257) )
  :assumption
(or (not b220)  (not b258) )
  :assumption
(or b254  (not b258) )
  :assumption
(or (not b250)  (not b258) )
  :assumption
(or b35  (not b258) )
  :assumption
(or b247  (not b258) )
  :assumption
(or b216  (not b258) )
  :assumption
(or (not b233)  (not b259) )
  :assumption
(or (not b259)  b260 )
  :assumption
(or (not b247)  (not b259) )
  :assumption
(or b248  (not b259) )
  :assumption
(or (not b231)  (not b261) )
  :assumption
(or (not b261)  b262 )
  :assumption
(or (not b250)  (not b261) )
  :assumption
(or b247  (not b261) )
  :assumption
(or b233  (not b261) )
  :assumption
(or (not b192)  (not b263) )
  :assumption
(or (not b263)  b264 )
  :assumption
(or (not b263)  (not b265) )
  :assumption
(or b114  (not b263) )
  :assumption
(or (not b263)  b266 )
  :assumption
(or b196  (not b263) )
  :assumption
(or (not b198)  (not b267) )
  :assumption
(or (not b267)  b268 )
  :assumption
(or (not b267)  (not b269) )
  :assumption
(or b14  (not b267) )
  :assumption
(or b265  (not b267) )
  :assumption
(or b192  (not b267) )
  :assumption
(or (not b192)  (not b270) )
  :assumption
(or b264  (not b270) )
  :assumption
(or (not b270)  (not b271) )
  :assumption
(or b116  (not b270) )
  :assumption
(or (not b270)  b272 )
  :assumption
(or b196  (not b270) )
  :assumption
(or (not b198)  (not b273) )
  :assumption
(or b268  (not b273) )
  :assumption
(or (not b273)  (not b274) )
  :assumption
(or b21  (not b273) )
  :assumption
(or b271  (not b273) )
  :assumption
(or b192  (not b273) )
  :assumption
(or (not b192)  (not b275) )
  :assumption
(or b264  (not b275) )
  :assumption
(or (not b275)  (not b276) )
  :assumption
(or b121  (not b275) )
  :assumption
(or (not b275)  b277 )
  :assumption
(or b196  (not b275) )
  :assumption
(or (not b198)  (not b278) )
  :assumption
(or b268  (not b278) )
  :assumption
(or (not b278)  (not b279) )
  :assumption
(or b25  (not b278) )
  :assumption
(or b276  (not b278) )
  :assumption
(or b192  (not b278) )
  :assumption
(or (not b216)  (not b280) )
  :assumption
(or (not b280)  b281 )
  :assumption
(or (not b265)  (not b280) )
  :assumption
(or b124  (not b280) )
  :assumption
(or b266  (not b280) )
  :assumption
(or b218  (not b280) )
  :assumption
(or (not b220)  (not b282) )
  :assumption
(or (not b282)  b283 )
  :assumption
(or (not b269)  (not b282) )
  :assumption
(or b29  (not b282) )
  :assumption
(or b265  (not b282) )
  :assumption
(or b216  (not b282) )
  :assumption
(or (not b216)  (not b284) )
  :assumption
(or b281  (not b284) )
  :assumption
(or (not b271)  (not b284) )
  :assumption
(or b126  (not b284) )
  :assumption
(or b272  (not b284) )
  :assumption
(or b218  (not b284) )
  :assumption
(or (not b220)  (not b285) )
  :assumption
(or b283  (not b285) )
  :assumption
(or (not b274)  (not b285) )
  :assumption
(or b33  (not b285) )
  :assumption
(or b271  (not b285) )
  :assumption
(or b216  (not b285) )
  :assumption
(or (not b216)  (not b286) )
  :assumption
(or b281  (not b286) )
  :assumption
(or (not b276)  (not b286) )
  :assumption
(or b131  (not b286) )
  :assumption
(or b277  (not b286) )
  :assumption
(or b218  (not b286) )
  :assumption
(or (not b220)  (not b287) )
  :assumption
(or b283  (not b287) )
  :assumption
(or (not b279)  (not b287) )
  :assumption
(or b35  (not b287) )
  :assumption
(or b276  (not b287) )
  :assumption
(or b216  (not b287) )
  :assumption
(or (not b233)  (not b288) )
  :assumption
(or (not b288)  b289 )
  :assumption
(or (not b276)  (not b288) )
  :assumption
(or b277  (not b288) )
  :assumption
(or (not b231)  (not b290) )
  :assumption
(or (not b290)  b291 )
  :assumption
(or (not b279)  (not b290) )
  :assumption
(or b276  (not b290) )
  :assumption
(or b233  (not b290) )
  :assumption
(or b192  (not b292) )
  :assumption
(or b194  (not b292) )
  :assumption
(or (not b193)  (not b292) )
  :assumption
(or b114  (not b292) )
  :assumption
(or b206  (not b292) )
  :assumption
(or b198  (not b293) )
  :assumption
(or b200  (not b293) )
  :assumption
(or (not b199)  (not b293) )
  :assumption
(or b14  (not b293) )
  :assumption
(or b193  (not b293) )
  :assumption
(or b196  (not b294) )
  :assumption
(or b207  (not b294) )
  :assumption
(or (not b206)  (not b294) )
  :assumption
(or b203  (not b294) )
  :assumption
(or b192  (not b295) )
  :assumption
(or b209  (not b295) )
  :assumption
(or (not b193)  (not b295) )
  :assumption
(or b116  (not b295) )
  :assumption
(or b206  (not b295) )
  :assumption
(or b198  (not b296) )
  :assumption
(or b211  (not b296) )
  :assumption
(or (not b199)  (not b296) )
  :assumption
(or b21  (not b296) )
  :assumption
(or b193  (not b296) )
  :assumption
(or b192  (not b297) )
  :assumption
(or b214  (not b297) )
  :assumption
(or (not b193)  (not b297) )
  :assumption
(or b121  (not b297) )
  :assumption
(or b206  (not b297) )
  :assumption
(or b198  (not b298) )
  :assumption
(or b213  (not b298) )
  :assumption
(or (not b199)  (not b298) )
  :assumption
(or b25  (not b298) )
  :assumption
(or b193  (not b298) )
  :assumption
(or b216  (not b299) )
  :assumption
(or b194  (not b299) )
  :assumption
(or (not b217)  (not b299) )
  :assumption
(or b124  (not b299) )
  :assumption
(or b226  (not b299) )
  :assumption
(or b220  (not b300) )
  :assumption
(or b200  (not b300) )
  :assumption
(or (not b221)  (not b300) )
  :assumption
(or b29  (not b300) )
  :assumption
(or b217  (not b300) )
  :assumption
(or b218  (not b301) )
  :assumption
(or b207  (not b301) )
  :assumption
(or (not b226)  (not b301) )
  :assumption
(or b224  (not b301) )
  :assumption
(or b216  (not b302) )
  :assumption
(or b209  (not b302) )
  :assumption
(or (not b217)  (not b302) )
  :assumption
(or b126  (not b302) )
  :assumption
(or b226  (not b302) )
  :assumption
(or b220  (not b303) )
  :assumption
(or b211  (not b303) )
  :assumption
(or (not b221)  (not b303) )
  :assumption
(or b33  (not b303) )
  :assumption
(or b217  (not b303) )
  :assumption
(or b216  (not b304) )
  :assumption
(or b214  (not b304) )
  :assumption
(or (not b217)  (not b304) )
  :assumption
(or b131  (not b304) )
  :assumption
(or b226  (not b304) )
  :assumption
(or b220  (not b305) )
  :assumption
(or b213  (not b305) )
  :assumption
(or (not b221)  (not b305) )
  :assumption
(or b35  (not b305) )
  :assumption
(or b217  (not b305) )
  :assumption
(or b198  (not b306) )
  :assumption
(or b240  (not b306) )
  :assumption
(or (not b239)  (not b306) )
  :assumption
(or b14  (not b306) )
  :assumption
(or b235  (not b306) )
  :assumption
(or b198  (not b307) )
  :assumption
(or b245  (not b307) )
  :assumption
(or (not b239)  (not b307) )
  :assumption
(or b21  (not b307) )
  :assumption
(or b235  (not b307) )
  :assumption
(or b198  (not b308) )
  :assumption
(or b250  (not b308) )
  :assumption
(or (not b239)  (not b308) )
  :assumption
(or b25  (not b308) )
  :assumption
(or b235  (not b308) )
  :assumption
(or (not b309)  b310 )
  :assumption
(or (not b309)  (not b311) )
  :assumption
(or b151  (not b309) )
  :assumption
(or b239  (not b309) )
  :assumption
(or b220  (not b312) )
  :assumption
(or b240  (not b312) )
  :assumption
(or (not b254)  (not b312) )
  :assumption
(or b29  (not b312) )
  :assumption
(or b252  (not b312) )
  :assumption
(or b220  (not b313) )
  :assumption
(or b245  (not b313) )
  :assumption
(or (not b254)  (not b313) )
  :assumption
(or b33  (not b313) )
  :assumption
(or b252  (not b313) )
  :assumption
(or b220  (not b314) )
  :assumption
(or b250  (not b314) )
  :assumption
(or (not b254)  (not b314) )
  :assumption
(or b35  (not b314) )
  :assumption
(or b252  (not b314) )
  :assumption
(or (not b315)  b316 )
  :assumption
(or (not b315)  (not b317) )
  :assumption
(or b154  (not b315) )
  :assumption
(or b254  (not b315) )
  :assumption
(or b231  (not b318) )
  :assumption
(or b250  (not b318) )
  :assumption
(or (not b262)  (not b318) )
  :assumption
(or b260  (not b318) )
  :assumption
(or (not b319)  b320 )
  :assumption
(or (not b319)  (not b321) )
  :assumption
(or b159  (not b319) )
  :assumption
(or b262  (not b319) )
  :assumption
(or b198  (not b322) )
  :assumption
(or b269  (not b322) )
  :assumption
(or (not b268)  (not b322) )
  :assumption
(or b14  (not b322) )
  :assumption
(or b264  (not b322) )
  :assumption
(or b198  (not b323) )
  :assumption
(or b274  (not b323) )
  :assumption
(or (not b268)  (not b323) )
  :assumption
(or b21  (not b323) )
  :assumption
(or b264  (not b323) )
  :assumption
(or b310  (not b324) )
  :assumption
(or (not b324)  (not b325) )
  :assumption
(or b119  (not b324) )
  :assumption
(or b268  (not b324) )
  :assumption
(or b198  (not b326) )
  :assumption
(or b279  (not b326) )
  :assumption
(or (not b268)  (not b326) )
  :assumption
(or b25  (not b326) )
  :assumption
(or b264  (not b326) )
  :assumption
(or b220  (not b327) )
  :assumption
(or b269  (not b327) )
  :assumption
(or (not b283)  (not b327) )
  :assumption
(or b29  (not b327) )
  :assumption
(or b281  (not b327) )
  :assumption
(or b220  (not b328) )
  :assumption
(or b274  (not b328) )
  :assumption
(or (not b283)  (not b328) )
  :assumption
(or b33  (not b328) )
  :assumption
(or b281  (not b328) )
  :assumption
(or b316  (not b329) )
  :assumption
(or (not b329)  (not b330) )
  :assumption
(or b129  (not b329) )
  :assumption
(or b283  (not b329) )
  :assumption
(or b220  (not b331) )
  :assumption
(or b279  (not b331) )
  :assumption
(or (not b283)  (not b331) )
  :assumption
(or b35  (not b331) )
  :assumption
(or b281  (not b331) )
  :assumption
(or b320  (not b332) )
  :assumption
(or (not b332)  (not b333) )
  :assumption
(or b134  (not b332) )
  :assumption
(or b291  (not b332) )
  :assumption
(or b231  (not b334) )
  :assumption
(or b279  (not b334) )
  :assumption
(or (not b291)  (not b334) )
  :assumption
(or b289  (not b334) )
  :assumption
(or (= r123 0)  b336 )
  :assumption
(or (not b336)  (= r123 90) )
  :assumption
(or b21  (not b336) )
  :assumption
(or (not b14)  (not b336) )
  :assumption
(or b114  (not b336) )
  :assumption
(or b206  (not b336) )
  :assumption
(or (= r164 0)  b339 )
  :assumption
(or (not b339)  (= r164 90) )
  :assumption
(or b119  (not b339) )
  :assumption
(or (not b178)  (not b339) )
  :assumption
(or b14  (not b339) )
  :assumption
(or b193  (not b339) )
  :assumption
(or (= r163 0)  b344 )
  :assumption
(or (not b344)  (= r163 90) )
  :assumption
(or b119  (not b344) )
  :assumption
(or (not b178)  (not b344) )
  :assumption
(or b14  (not b344) )
  :assumption
(or b235  (not b344) )
  :assumption
(or (= r162 0)  b348 )
  :assumption
(or (not b348)  (= r162 90) )
  :assumption
(or b119  (not b348) )
  :assumption
(or (not b178)  (not b348) )
  :assumption
(or b14  (not b348) )
  :assumption
(or b264  (not b348) )
  :assumption
(or (= r122 0)  b352 )
  :assumption
(or (not b352)  (= r122 19) )
  :assumption
(or b25  (not b352) )
  :assumption
(or (not b14)  (not b352) )
  :assumption
(or b114  (not b352) )
  :assumption
(or b206  (not b352) )
  :assumption
(or (= r161 0)  b355 )
  :assumption
(or (not b355)  (= r161 19) )
  :assumption
(or b151  (not b355) )
  :assumption
(or (not b178)  (not b355) )
  :assumption
(or b14  (not b355) )
  :assumption
(or b193  (not b355) )
  :assumption
(or (= r160 0)  b360 )
  :assumption
(or (not b360)  (= r160 19) )
  :assumption
(or b151  (not b360) )
  :assumption
(or (not b178)  (not b360) )
  :assumption
(or b14  (not b360) )
  :assumption
(or b235  (not b360) )
  :assumption
(or (= r159 0)  b364 )
  :assumption
(or (not b364)  (= r159 19) )
  :assumption
(or b151  (not b364) )
  :assumption
(or (not b178)  (not b364) )
  :assumption
(or b14  (not b364) )
  :assumption
(or b264  (not b364) )
  :assumption
(or (= r110 0)  b368 )
  :assumption
(or (not b368)  (= r110 90) )
  :assumption
(or b114  (not b368) )
  :assumption
(or (not b116)  (not b368) )
  :assumption
(or b203  (not b368) )
  :assumption
(or (= r121 0)  b371 )
  :assumption
(or (not b371)  (= r121 90) )
  :assumption
(or b14  (not b371) )
  :assumption
(or (not b21)  (not b371) )
  :assumption
(or b116  (not b371) )
  :assumption
(or b206  (not b371) )
  :assumption
(or (= r158 0)  b374 )
  :assumption
(or (not b374)  (= r158 90) )
  :assumption
(or b178  (not b374) )
  :assumption
(or (not b119)  (not b374) )
  :assumption
(or b21  (not b374) )
  :assumption
(or b193  (not b374) )
  :assumption
(or (= r212 0)  b377 )
  :assumption
(or (not b377)  (= r212 90) )
  :assumption
(or (not b342)  (not b377) )
  :assumption
(or b119  (not b377) )
  :assumption
(or b199  (not b377) )
  :assumption
(or (= r157 0)  b380 )
  :assumption
(or (not b380)  (= r157 90) )
  :assumption
(or b178  (not b380) )
  :assumption
(or (not b119)  (not b380) )
  :assumption
(or b21  (not b380) )
  :assumption
(or b235  (not b380) )
  :assumption
(or (= r211 0)  b383 )
  :assumption
(or (not b383)  (= r211 90) )
  :assumption
(or (not b342)  (not b383) )
  :assumption
(or b119  (not b383) )
  :assumption
(or b239  (not b383) )
  :assumption
(or (= r156 0)  b386 )
  :assumption
(or (not b386)  (= r156 90) )
  :assumption
(or b178  (not b386) )
  :assumption
(or (not b119)  (not b386) )
  :assumption
(or b21  (not b386) )
  :assumption
(or b264  (not b386) )
  :assumption
(or (= r210 0)  b389 )
  :assumption
(or (not b389)  (= r210 90) )
  :assumption
(or (not b342)  (not b389) )
  :assumption
(or b119  (not b389) )
  :assumption
(or b268  (not b389) )
  :assumption
(or (= r109 0)  b392 )
  :assumption
(or (not b392)  (= r109 93) )
  :assumption
(or b121  (not b392) )
  :assumption
(or (not b116)  (not b392) )
  :assumption
(or b203  (not b392) )
  :assumption
(or (= r120 0)  b395 )
  :assumption
(or (not b395)  (= r120 93) )
  :assumption
(or b25  (not b395) )
  :assumption
(or (not b21)  (not b395) )
  :assumption
(or b116  (not b395) )
  :assumption
(or b206  (not b395) )
  :assumption
(or (= r155 0)  b398 )
  :assumption
(or (not b398)  (= r155 93) )
  :assumption
(or b151  (not b398) )
  :assumption
(or (not b119)  (not b398) )
  :assumption
(or b21  (not b398) )
  :assumption
(or b193  (not b398) )
  :assumption
(or (= r209 0)  b401 )
  :assumption
(or (not b401)  (= r209 93) )
  :assumption
(or b358  (not b401) )
  :assumption
(or (not b342)  (not b401) )
  :assumption
(or b119  (not b401) )
  :assumption
(or b199  (not b401) )
  :assumption
(or (= r154 0)  b404 )
  :assumption
(or (not b404)  (= r154 93) )
  :assumption
(or b151  (not b404) )
  :assumption
(or (not b119)  (not b404) )
  :assumption
(or b21  (not b404) )
  :assumption
(or b235  (not b404) )
  :assumption
(or (= r208 0)  b407 )
  :assumption
(or (not b407)  (= r208 93) )
  :assumption
(or b358  (not b407) )
  :assumption
(or (not b342)  (not b407) )
  :assumption
(or b119  (not b407) )
  :assumption
(or b239  (not b407) )
  :assumption
(or (= r153 0)  b410 )
  :assumption
(or (not b410)  (= r153 93) )
  :assumption
(or b151  (not b410) )
  :assumption
(or (not b119)  (not b410) )
  :assumption
(or b21  (not b410) )
  :assumption
(or b264  (not b410) )
  :assumption
(or (= r207 0)  b413 )
  :assumption
(or (not b413)  (= r207 93) )
  :assumption
(or b358  (not b413) )
  :assumption
(or (not b342)  (not b413) )
  :assumption
(or b119  (not b413) )
  :assumption
(or b268  (not b413) )
  :assumption
(or (= r119 0)  b416 )
  :assumption
(or (not b416)  (= r119 19) )
  :assumption
(or b14  (not b416) )
  :assumption
(or (not b25)  (not b416) )
  :assumption
(or b121  (not b416) )
  :assumption
(or b206  (not b416) )
  :assumption
(or (= r152 0)  b419 )
  :assumption
(or (not b419)  (= r152 19) )
  :assumption
(or b178  (not b419) )
  :assumption
(or (not b151)  (not b419) )
  :assumption
(or b25  (not b419) )
  :assumption
(or b193  (not b419) )
  :assumption
(or (= r206 0)  b422 )
  :assumption
(or (not b422)  (= r206 19) )
  :assumption
(or (not b358)  (not b422) )
  :assumption
(or b151  (not b422) )
  :assumption
(or b199  (not b422) )
  :assumption
(or (= r151 0)  b425 )
  :assumption
(or (not b425)  (= r151 19) )
  :assumption
(or b178  (not b425) )
  :assumption
(or (not b151)  (not b425) )
  :assumption
(or b25  (not b425) )
  :assumption
(or b235  (not b425) )
  :assumption
(or (= r205 0)  b428 )
  :assumption
(or (not b428)  (= r205 19) )
  :assumption
(or (not b358)  (not b428) )
  :assumption
(or b151  (not b428) )
  :assumption
(or b239  (not b428) )
  :assumption
(or (= r150 0)  b431 )
  :assumption
(or (not b431)  (= r150 19) )
  :assumption
(or b178  (not b431) )
  :assumption
(or (not b151)  (not b431) )
  :assumption
(or b25  (not b431) )
  :assumption
(or b264  (not b431) )
  :assumption
(or (= r204 0)  b434 )
  :assumption
(or (not b434)  (= r204 19) )
  :assumption
(or (not b358)  (not b434) )
  :assumption
(or b151  (not b434) )
  :assumption
(or b268  (not b434) )
  :assumption
(or (= r118 0)  b437 )
  :assumption
(or (not b437)  (= r118 93) )
  :assumption
(or b21  (not b437) )
  :assumption
(or (not b25)  (not b437) )
  :assumption
(or b121  (not b437) )
  :assumption
(or b206  (not b437) )
  :assumption
(or (= r149 0)  b440 )
  :assumption
(or (not b440)  (= r149 93) )
  :assumption
(or b119  (not b440) )
  :assumption
(or (not b151)  (not b440) )
  :assumption
(or b25  (not b440) )
  :assumption
(or b193  (not b440) )
  :assumption
(or (= r203 0)  b443 )
  :assumption
(or (not b443)  (= r203 93) )
  :assumption
(or b342  (not b443) )
  :assumption
(or (not b358)  (not b443) )
  :assumption
(or b151  (not b443) )
  :assumption
(or b199  (not b443) )
  :assumption
(or (= r148 0)  b446 )
  :assumption
(or (not b446)  (= r148 93) )
  :assumption
(or b119  (not b446) )
  :assumption
(or (not b151)  (not b446) )
  :assumption
(or b25  (not b446) )
  :assumption
(or b235  (not b446) )
  :assumption
(or (= r202 0)  b449 )
  :assumption
(or (not b449)  (= r202 93) )
  :assumption
(or b342  (not b449) )
  :assumption
(or (not b358)  (not b449) )
  :assumption
(or b151  (not b449) )
  :assumption
(or b239  (not b449) )
  :assumption
(or (= r147 0)  b452 )
  :assumption
(or (not b452)  (= r147 93) )
  :assumption
(or b119  (not b452) )
  :assumption
(or (not b151)  (not b452) )
  :assumption
(or b25  (not b452) )
  :assumption
(or b264  (not b452) )
  :assumption
(or (= r201 0)  b455 )
  :assumption
(or (not b455)  (= r201 93) )
  :assumption
(or b342  (not b455) )
  :assumption
(or (not b358)  (not b455) )
  :assumption
(or b151  (not b455) )
  :assumption
(or b268  (not b455) )
  :assumption
(or (= r117 0)  b458 )
  :assumption
(or (not b458)  (= r117 90) )
  :assumption
(or b33  (not b458) )
  :assumption
(or (not b29)  (not b458) )
  :assumption
(or b124  (not b458) )
  :assumption
(or b226  (not b458) )
  :assumption
(or (= r146 0)  b461 )
  :assumption
(or (not b461)  (= r146 90) )
  :assumption
(or b129  (not b461) )
  :assumption
(or (not b185)  (not b461) )
  :assumption
(or b29  (not b461) )
  :assumption
(or b217  (not b461) )
  :assumption
(or (= r200 0)  b464 )
  :assumption
(or (not b464)  (= r200 90) )
  :assumption
(or (not b464)  b466 )
  :assumption
(or (not b464)  (not b467) )
  :assumption
(or b185  (not b464) )
  :assumption
(or b221  (not b464) )
  :assumption
(or (= r145 0)  b469 )
  :assumption
(or (not b469)  (= r145 90) )
  :assumption
(or b129  (not b469) )
  :assumption
(or (not b185)  (not b469) )
  :assumption
(or b29  (not b469) )
  :assumption
(or b252  (not b469) )
  :assumption
(or (= r199 0)  b472 )
  :assumption
(or (not b472)  (= r199 90) )
  :assumption
(or b466  (not b472) )
  :assumption
(or (not b467)  (not b472) )
  :assumption
(or b185  (not b472) )
  :assumption
(or b254  (not b472) )
  :assumption
(or (= r144 0)  b475 )
  :assumption
(or (not b475)  (= r144 90) )
  :assumption
(or b129  (not b475) )
  :assumption
(or (not b185)  (not b475) )
  :assumption
(or b29  (not b475) )
  :assumption
(or b281  (not b475) )
  :assumption
(or (= r198 0)  b478 )
  :assumption
(or (not b478)  (= r198 90) )
  :assumption
(or b466  (not b478) )
  :assumption
(or (not b467)  (not b478) )
  :assumption
(or b185  (not b478) )
  :assumption
(or b283  (not b478) )
  :assumption
(or (= r116 0)  b481 )
  :assumption
(or (not b481)  (= r116 19) )
  :assumption
(or b35  (not b481) )
  :assumption
(or (not b29)  (not b481) )
  :assumption
(or b124  (not b481) )
  :assumption
(or b226  (not b481) )
  :assumption
(or (= r143 0)  b484 )
  :assumption
(or (not b484)  (= r143 19) )
  :assumption
(or b154  (not b484) )
  :assumption
(or (not b185)  (not b484) )
  :assumption
(or b29  (not b484) )
  :assumption
(or b217  (not b484) )
  :assumption
(or (= r197 0)  b487 )
  :assumption
(or (not b487)  (= r197 19) )
  :assumption
(or (not b467)  (not b487) )
  :assumption
(or b185  (not b487) )
  :assumption
(or b221  (not b487) )
  :assumption
(or (= r142 0)  b490 )
  :assumption
(or (not b490)  (= r142 19) )
  :assumption
(or b154  (not b490) )
  :assumption
(or (not b185)  (not b490) )
  :assumption
(or b29  (not b490) )
  :assumption
(or b252  (not b490) )
  :assumption
(or (= r196 0)  b493 )
  :assumption
(or (not b493)  (= r196 19) )
  :assumption
(or (not b467)  (not b493) )
  :assumption
(or b185  (not b493) )
  :assumption
(or b254  (not b493) )
  :assumption
(or (= r141 0)  b496 )
  :assumption
(or (not b496)  (= r141 19) )
  :assumption
(or b154  (not b496) )
  :assumption
(or (not b185)  (not b496) )
  :assumption
(or b29  (not b496) )
  :assumption
(or b281  (not b496) )
  :assumption
(or (= r195 0)  b499 )
  :assumption
(or (not b499)  (= r195 19) )
  :assumption
(or (not b467)  (not b499) )
  :assumption
(or b185  (not b499) )
  :assumption
(or b283  (not b499) )
  :assumption
(or (= r108 0)  b502 )
  :assumption
(or (not b502)  (= r108 90) )
  :assumption
(or b124  (not b502) )
  :assumption
(or (not b126)  (not b502) )
  :assumption
(or b224  (not b502) )
  :assumption
(or (= r115 0)  b505 )
  :assumption
(or (not b505)  (= r115 90) )
  :assumption
(or b29  (not b505) )
  :assumption
(or (not b33)  (not b505) )
  :assumption
(or b126  (not b505) )
  :assumption
(or b226  (not b505) )
  :assumption
(or (= r140 0)  b508 )
  :assumption
(or (not b508)  (= r140 90) )
  :assumption
(or b185  (not b508) )
  :assumption
(or (not b129)  (not b508) )
  :assumption
(or b33  (not b508) )
  :assumption
(or b217  (not b508) )
  :assumption
(or (= r194 0)  b511 )
  :assumption
(or (not b511)  (= r194 90) )
  :assumption
(or b467  (not b511) )
  :assumption
(or (not b466)  (not b511) )
  :assumption
(or b129  (not b511) )
  :assumption
(or b221  (not b511) )
  :assumption
(or (= r139 0)  b514 )
  :assumption
(or (not b514)  (= r139 90) )
  :assumption
(or b185  (not b514) )
  :assumption
(or (not b129)  (not b514) )
  :assumption
(or b33  (not b514) )
  :assumption
(or b252  (not b514) )
  :assumption
(or (= r193 0)  b517 )
  :assumption
(or (not b517)  (= r193 90) )
  :assumption
(or b467  (not b517) )
  :assumption
(or (not b466)  (not b517) )
  :assumption
(or b129  (not b517) )
  :assumption
(or b254  (not b517) )
  :assumption
(or (= r138 0)  b520 )
  :assumption
(or (not b520)  (= r138 90) )
  :assumption
(or b185  (not b520) )
  :assumption
(or (not b129)  (not b520) )
  :assumption
(or b33  (not b520) )
  :assumption
(or b281  (not b520) )
  :assumption
(or (= r192 0)  b523 )
  :assumption
(or (not b523)  (= r192 90) )
  :assumption
(or b467  (not b523) )
  :assumption
(or (not b466)  (not b523) )
  :assumption
(or b129  (not b523) )
  :assumption
(or b283  (not b523) )
  :assumption
(or (= r107 0)  b526 )
  :assumption
(or (not b526)  (= r107 93) )
  :assumption
(or b131  (not b526) )
  :assumption
(or (not b126)  (not b526) )
  :assumption
(or b224  (not b526) )
  :assumption
(or (= r114 0)  b529 )
  :assumption
(or (not b529)  (= r114 93) )
  :assumption
(or b35  (not b529) )
  :assumption
(or (not b33)  (not b529) )
  :assumption
(or b126  (not b529) )
  :assumption
(or b226  (not b529) )
  :assumption
(or (= r137 0)  b532 )
  :assumption
(or (not b532)  (= r137 93) )
  :assumption
(or b154  (not b532) )
  :assumption
(or (not b129)  (not b532) )
  :assumption
(or b33  (not b532) )
  :assumption
(or b217  (not b532) )
  :assumption
(or (= r191 0)  b535 )
  :assumption
(or (not b535)  (= r191 93) )
  :assumption
(or (not b466)  (not b535) )
  :assumption
(or b129  (not b535) )
  :assumption
(or b221  (not b535) )
  :assumption
(or (= r136 0)  b538 )
  :assumption
(or (not b538)  (= r136 93) )
  :assumption
(or b154  (not b538) )
  :assumption
(or (not b129)  (not b538) )
  :assumption
(or b33  (not b538) )
  :assumption
(or b252  (not b538) )
  :assumption
(or (= r190 0)  b541 )
  :assumption
(or (not b541)  (= r190 93) )
  :assumption
(or (not b466)  (not b541) )
  :assumption
(or b129  (not b541) )
  :assumption
(or b254  (not b541) )
  :assumption
(or (= r135 0)  b544 )
  :assumption
(or (not b544)  (= r135 93) )
  :assumption
(or b154  (not b544) )
  :assumption
(or (not b129)  (not b544) )
  :assumption
(or b33  (not b544) )
  :assumption
(or b281  (not b544) )
  :assumption
(or (= r189 0)  b547 )
  :assumption
(or (not b547)  (= r189 93) )
  :assumption
(or (not b466)  (not b547) )
  :assumption
(or b129  (not b547) )
  :assumption
(or b283  (not b547) )
  :assumption
(or (= r113 0)  b550 )
  :assumption
(or (not b550)  (= r113 19) )
  :assumption
(or b29  (not b550) )
  :assumption
(or (not b35)  (not b550) )
  :assumption
(or b131  (not b550) )
  :assumption
(or b226  (not b550) )
  :assumption
(or (= r134 0)  b553 )
  :assumption
(or (not b553)  (= r134 19) )
  :assumption
(or b185  (not b553) )
  :assumption
(or (not b154)  (not b553) )
  :assumption
(or b35  (not b553) )
  :assumption
(or b217  (not b553) )
  :assumption
(or (= r133 0)  b557 )
  :assumption
(or (not b557)  (= r133 19) )
  :assumption
(or b185  (not b557) )
  :assumption
(or (not b154)  (not b557) )
  :assumption
(or b35  (not b557) )
  :assumption
(or b252  (not b557) )
  :assumption
(or (= r132 0)  b561 )
  :assumption
(or (not b561)  (= r132 19) )
  :assumption
(or b185  (not b561) )
  :assumption
(or (not b154)  (not b561) )
  :assumption
(or b35  (not b561) )
  :assumption
(or b281  (not b561) )
  :assumption
(or (= r112 0)  b565 )
  :assumption
(or (not b565)  (= r112 93) )
  :assumption
(or b33  (not b565) )
  :assumption
(or (not b35)  (not b565) )
  :assumption
(or b131  (not b565) )
  :assumption
(or b226  (not b565) )
  :assumption
(or (= r131 0)  b568 )
  :assumption
(or (not b568)  (= r131 93) )
  :assumption
(or b129  (not b568) )
  :assumption
(or (not b154)  (not b568) )
  :assumption
(or b35  (not b568) )
  :assumption
(or b217  (not b568) )
  :assumption
(or (= r130 0)  b572 )
  :assumption
(or (not b572)  (= r130 93) )
  :assumption
(or b129  (not b572) )
  :assumption
(or (not b154)  (not b572) )
  :assumption
(or b35  (not b572) )
  :assumption
(or b252  (not b572) )
  :assumption
(or (= r129 0)  b576 )
  :assumption
(or (not b576)  (= r129 93) )
  :assumption
(or b129  (not b576) )
  :assumption
(or (not b154)  (not b576) )
  :assumption
(or b35  (not b576) )
  :assumption
(or b281  (not b576) )
  :assumption
(or (= r182 0)  b580 )
  :assumption
(or (not b580)  (= r182 90) )
  :assumption
(or (not b580)  b582 )
  :assumption
(or (not b580)  (not b583) )
  :assumption
(or b190  (not b580) )
  :assumption
(or b232  (not b580) )
  :assumption
(or (= r181 0)  b585 )
  :assumption
(or (not b585)  (= r181 90) )
  :assumption
(or b582  (not b585) )
  :assumption
(or (not b583)  (not b585) )
  :assumption
(or b190  (not b585) )
  :assumption
(or b262  (not b585) )
  :assumption
(or (= r180 0)  b588 )
  :assumption
(or (not b588)  (= r180 90) )
  :assumption
(or b582  (not b588) )
  :assumption
(or (not b583)  (not b588) )
  :assumption
(or b190  (not b588) )
  :assumption
(or b291  (not b588) )
  :assumption
(or (= r179 0)  b591 )
  :assumption
(or (not b591)  (= r179 19) )
  :assumption
(or (not b583)  (not b591) )
  :assumption
(or b190  (not b591) )
  :assumption
(or b232  (not b591) )
  :assumption
(or (= r178 0)  b594 )
  :assumption
(or (not b594)  (= r178 19) )
  :assumption
(or (not b583)  (not b594) )
  :assumption
(or b190  (not b594) )
  :assumption
(or b262  (not b594) )
  :assumption
(or (= r177 0)  b597 )
  :assumption
(or (not b597)  (= r177 19) )
  :assumption
(or (not b583)  (not b597) )
  :assumption
(or b190  (not b597) )
  :assumption
(or b291  (not b597) )
  :assumption
(or (= r176 0)  b600 )
  :assumption
(or (not b600)  (= r176 90) )
  :assumption
(or b583  (not b600) )
  :assumption
(or (not b582)  (not b600) )
  :assumption
(or b134  (not b600) )
  :assumption
(or b232  (not b600) )
  :assumption
(or (= r175 0)  b603 )
  :assumption
(or (not b603)  (= r175 90) )
  :assumption
(or b583  (not b603) )
  :assumption
(or (not b582)  (not b603) )
  :assumption
(or b134  (not b603) )
  :assumption
(or b262  (not b603) )
  :assumption
(or (= r174 0)  b606 )
  :assumption
(or (not b606)  (= r174 90) )
  :assumption
(or b583  (not b606) )
  :assumption
(or (not b582)  (not b606) )
  :assumption
(or b134  (not b606) )
  :assumption
(or b291  (not b606) )
  :assumption
(or (= r173 0)  b609 )
  :assumption
(or (not b609)  (= r173 93) )
  :assumption
(or (not b582)  (not b609) )
  :assumption
(or b134  (not b609) )
  :assumption
(or b232  (not b609) )
  :assumption
(or (= r172 0)  b612 )
  :assumption
(or (not b612)  (= r172 93) )
  :assumption
(or (not b582)  (not b612) )
  :assumption
(or b134  (not b612) )
  :assumption
(or b262  (not b612) )
  :assumption
(or (= r171 0)  b615 )
  :assumption
(or (not b615)  (= r171 93) )
  :assumption
(or (not b582)  (not b615) )
  :assumption
(or b134  (not b615) )
  :assumption
(or b291  (not b615) )
  :assumption
(or (= r128 0)  b619 )
  :assumption
(or (not b619)  (= r128 19) )
  :assumption
(or b190  (not b619) )
  :assumption
(or (not b159)  (not b619) )
  :assumption
(or b260  (not b619) )
  :assumption
(or (= r127 0)  b623 )
  :assumption
(or (not b623)  (= r127 19) )
  :assumption
(or b190  (not b623) )
  :assumption
(or (not b159)  (not b623) )
  :assumption
(or b289  (not b623) )
  :assumption
(or (= r126 0)  b628 )
  :assumption
(or (not b628)  (= r126 93) )
  :assumption
(or b134  (not b628) )
  :assumption
(or (not b159)  (not b628) )
  :assumption
(or b260  (not b628) )
  :assumption
(or (= r125 0)  b632 )
  :assumption
(or (not b632)  (= r125 93) )
  :assumption
(or b134  (not b632) )
  :assumption
(or (not b159)  (not b632) )
  :assumption
(or b289  (not b632) )
  :assumption
(or (= r93 0)  b636 )
  :assumption
(or (not b636)  (= r93 97) )
  :assumption
(or b200  (not b636) )
  :assumption
(or (not b636)  (not b638) )
  :assumption
(or (not b636)  b639 )
  :assumption
(or (= r104 0)  b641 )
  :assumption
(or (not b641)  (= r104 97) )
  :assumption
(or (not b641)  b643 )
  :assumption
(or (not b641)  (not b644) )
  :assumption
(or b638  (not b641) )
  :assumption
(or (= r92 0)  b646 )
  :assumption
(or (not b646)  (= r92 77) )
  :assumption
(or b213  (not b646) )
  :assumption
(or (not b638)  (not b646) )
  :assumption
(or b639  (not b646) )
  :assumption
(or (= r103 0)  b649 )
  :assumption
(or (not b649)  (= r103 77) )
  :assumption
(or (not b649)  b651 )
  :assumption
(or (not b644)  (not b649) )
  :assumption
(or b638  (not b649) )
  :assumption
(or (= r72 0)  b653 )
  :assumption
(or (not b653)  (= r72 29) )
  :assumption
(or b195  (not b653) )
  :assumption
(or (not b653)  (not b655) )
  :assumption
(or (not b653)  b656 )
  :assumption
(or (= r81 0)  b658 )
  :assumption
(or (not b658)  (= r81 29) )
  :assumption
(or b194  (not b658) )
  :assumption
(or (not b658)  (not b660) )
  :assumption
(or b655  (not b658) )
  :assumption
(or (= r91 0)  b662 )
  :assumption
(or (not b662)  (= r91 29) )
  :assumption
(or b200  (not b662) )
  :assumption
(or (not b662)  (not b664) )
  :assumption
(or b660  (not b662) )
  :assumption
(or (= r102 0)  b666 )
  :assumption
(or (not b666)  (= r102 29) )
  :assumption
(or b643  (not b666) )
  :assumption
(or (not b666)  (not b668) )
  :assumption
(or b664  (not b666) )
  :assumption
(or (= r71 0)  b670 )
  :assumption
(or (not b670)  (= r71 44) )
  :assumption
(or b207  (not b670) )
  :assumption
(or (not b655)  (not b670) )
  :assumption
(or b656  (not b670) )
  :assumption
(or (= r80 0)  b673 )
  :assumption
(or (not b673)  (= r80 44) )
  :assumption
(or b209  (not b673) )
  :assumption
(or (not b660)  (not b673) )
  :assumption
(or b655  (not b673) )
  :assumption
(or (= r90 0)  b676 )
  :assumption
(or (not b676)  (= r90 44) )
  :assumption
(or b211  (not b676) )
  :assumption
(or (not b664)  (not b676) )
  :assumption
(or b660  (not b676) )
  :assumption
(or (= r101 0)  b679 )
  :assumption
(or (not b679)  (= r101 44) )
  :assumption
(or (not b679)  b681 )
  :assumption
(or (not b668)  (not b679) )
  :assumption
(or b664  (not b679) )
  :assumption
(or (= r79 0)  b683 )
  :assumption
(or (not b683)  (= r79 97) )
  :assumption
(or b639  (not b683) )
  :assumption
(or (not b194)  (not b683) )
  :assumption
(or b195  (not b683) )
  :assumption
(or (= r89 0)  b686 )
  :assumption
(or (not b686)  (= r89 97) )
  :assumption
(or b638  (not b686) )
  :assumption
(or (not b200)  (not b686) )
  :assumption
(or b194  (not b686) )
  :assumption
(or (= r100 0)  b689 )
  :assumption
(or (not b689)  (= r100 97) )
  :assumption
(or b644  (not b689) )
  :assumption
(or (not b643)  (not b689) )
  :assumption
(or b200  (not b689) )
  :assumption
(or (= r78 0)  b692 )
  :assumption
(or (not b692)  (= r78 29) )
  :assumption
(or b660  (not b692) )
  :assumption
(or (not b194)  (not b692) )
  :assumption
(or b195  (not b692) )
  :assumption
(or (= r88 0)  b695 )
  :assumption
(or (not b695)  (= r88 29) )
  :assumption
(or b664  (not b695) )
  :assumption
(or (not b200)  (not b695) )
  :assumption
(or b194  (not b695) )
  :assumption
(or (= r99 0)  b698 )
  :assumption
(or (not b698)  (= r99 29) )
  :assumption
(or b668  (not b698) )
  :assumption
(or (not b643)  (not b698) )
  :assumption
(or b200  (not b698) )
  :assumption
(or (= r65 0)  b701 )
  :assumption
(or (not b701)  (= r65 44) )
  :assumption
(or b656  (not b701) )
  :assumption
(or (not b204)  (not b701) )
  :assumption
(or (= r70 0)  b704 )
  :assumption
(or (not b704)  (= r70 44) )
  :assumption
(or b655  (not b704) )
  :assumption
(or (not b207)  (not b704) )
  :assumption
(or b204  (not b704) )
  :assumption
(or (= r77 0)  b707 )
  :assumption
(or (not b707)  (= r77 44) )
  :assumption
(or b660  (not b707) )
  :assumption
(or (not b209)  (not b707) )
  :assumption
(or b207  (not b707) )
  :assumption
(or (= r87 0)  b710 )
  :assumption
(or (not b710)  (= r87 44) )
  :assumption
(or b664  (not b710) )
  :assumption
(or (not b211)  (not b710) )
  :assumption
(or b209  (not b710) )
  :assumption
(or (= r98 0)  b713 )
  :assumption
(or (not b713)  (= r98 44) )
  :assumption
(or b668  (not b713) )
  :assumption
(or (not b681)  (not b713) )
  :assumption
(or b211  (not b713) )
  :assumption
(or (= r86 0)  b716 )
  :assumption
(or (not b716)  (= r86 77) )
  :assumption
(or b638  (not b716) )
  :assumption
(or (not b213)  (not b716) )
  :assumption
(or b214  (not b716) )
  :assumption
(or (= r97 0)  b719 )
  :assumption
(or (not b719)  (= r97 77) )
  :assumption
(or b644  (not b719) )
  :assumption
(or (not b651)  (not b719) )
  :assumption
(or b213  (not b719) )
  :assumption
(or (= r69 0)  b722 )
  :assumption
(or (not b722)  (= r69 97) )
  :assumption
(or b237  (not b722) )
  :assumption
(or (not b722)  (not b724) )
  :assumption
(or (not b722)  b725 )
  :assumption
(or (= r76 0)  b727 )
  :assumption
(or (not b727)  (= r76 97) )
  :assumption
(or b236  (not b727) )
  :assumption
(or (not b727)  (not b729) )
  :assumption
(or b724  (not b727) )
  :assumption
(or (= r85 0)  b731 )
  :assumption
(or (not b731)  (= r85 97) )
  :assumption
(or b240  (not b731) )
  :assumption
(or (not b731)  (not b733) )
  :assumption
(or b729  (not b731) )
  :assumption
(or (= r96 0)  b735 )
  :assumption
(or (not b735)  (= r96 97) )
  :assumption
(or (not b735)  b737 )
  :assumption
(or (not b735)  (not b738) )
  :assumption
(or b733  (not b735) )
  :assumption
(or (= r68 0)  b740 )
  :assumption
(or (not b740)  (= r68 77) )
  :assumption
(or b248  (not b740) )
  :assumption
(or (not b724)  (not b740) )
  :assumption
(or b725  (not b740) )
  :assumption
(or (= r75 0)  b743 )
  :assumption
(or (not b743)  (= r75 77) )
  :assumption
(or b247  (not b743) )
  :assumption
(or (not b729)  (not b743) )
  :assumption
(or b724  (not b743) )
  :assumption
(or (= r84 0)  b746 )
  :assumption
(or (not b746)  (= r84 77) )
  :assumption
(or b250  (not b746) )
  :assumption
(or (not b733)  (not b746) )
  :assumption
(or b729  (not b746) )
  :assumption
(or (= r95 0)  b749 )
  :assumption
(or (not b749)  (= r95 77) )
  :assumption
(or (not b738)  (not b749) )
  :assumption
(or b733  (not b749) )
  :assumption
(or (= r67 0)  b752 )
  :assumption
(or (not b752)  (= r67 29) )
  :assumption
(or b237  (not b752) )
  :assumption
(or (not b752)  (not b754) )
  :assumption
(or (not b752)  b755 )
  :assumption
(or (= r74 0)  b757 )
  :assumption
(or (not b757)  (= r74 29) )
  :assumption
(or b236  (not b757) )
  :assumption
(or (not b757)  (not b759) )
  :assumption
(or b754  (not b757) )
  :assumption
(or (= r83 0)  b761 )
  :assumption
(or (not b761)  (= r83 29) )
  :assumption
(or b240  (not b761) )
  :assumption
(or (not b761)  (not b763) )
  :assumption
(or b759  (not b761) )
  :assumption
(or (= r94 0)  b765 )
  :assumption
(or (not b765)  (= r94 29) )
  :assumption
(or b737  (not b765) )
  :assumption
(or (not b765)  (not b767) )
  :assumption
(or b763  (not b765) )
  :assumption
(or (= r1 0)  b769 )
  :assumption
(or (not b769)  (= r1 44) )
  :assumption
(or b243  (not b769) )
  :assumption
(or (not b754)  (not b769) )
  :assumption
(or b755  (not b769) )
  :assumption
(or (= r3 0)  b772 )
  :assumption
(or (not b772)  (= r3 44) )
  :assumption
(or b242  (not b772) )
  :assumption
(or (not b759)  (not b772) )
  :assumption
(or b754  (not b772) )
  :assumption
(or (= r8 0)  b775 )
  :assumption
(or (not b775)  (= r8 44) )
  :assumption
(or b245  (not b775) )
  :assumption
(or (not b763)  (not b775) )
  :assumption
(or b759  (not b775) )
  :assumption
(or (= r11 0)  b778 )
  :assumption
(or (not b778)  (= r11 44) )
  :assumption
(or (not b778)  b780 )
  :assumption
(or (not b767)  (not b778) )
  :assumption
(or b763  (not b778) )
  :assumption
(or (= r16 0)  b782 )
  :assumption
(or (not b782)  (= r16 97) )
  :assumption
(or b725  (not b782) )
  :assumption
(or (not b782)  (not b784) )
  :assumption
(or (= r17 0)  b786 )
  :assumption
(or (not b786)  (= r17 97) )
  :assumption
(or b724  (not b786) )
  :assumption
(or (not b237)  (not b786) )
  :assumption
(or b784  (not b786) )
  :assumption
(or (= r18 0)  b789 )
  :assumption
(or (not b789)  (= r18 97) )
  :assumption
(or b729  (not b789) )
  :assumption
(or (not b236)  (not b789) )
  :assumption
(or b237  (not b789) )
  :assumption
(or (= r19 0)  b792 )
  :assumption
(or (not b792)  (= r19 97) )
  :assumption
(or b733  (not b792) )
  :assumption
(or (not b240)  (not b792) )
  :assumption
(or b236  (not b792) )
  :assumption
(or (= r20 0)  b795 )
  :assumption
(or (not b795)  (= r20 97) )
  :assumption
(or b738  (not b795) )
  :assumption
(or (not b737)  (not b795) )
  :assumption
(or b240  (not b795) )
  :assumption
(or (= r21 0)  b798 )
  :assumption
(or (not b798)  (= r21 29) )
  :assumption
(or b755  (not b798) )
  :assumption
(or (not b784)  (not b798) )
  :assumption
(or (= r22 0)  b801 )
  :assumption
(or (not b801)  (= r22 29) )
  :assumption
(or b754  (not b801) )
  :assumption
(or (not b237)  (not b801) )
  :assumption
(or b784  (not b801) )
  :assumption
(or (= r23 0)  b804 )
  :assumption
(or (not b804)  (= r23 29) )
  :assumption
(or b759  (not b804) )
  :assumption
(or (not b236)  (not b804) )
  :assumption
(or b237  (not b804) )
  :assumption
(or (= r24 0)  b807 )
  :assumption
(or (not b807)  (= r24 29) )
  :assumption
(or b763  (not b807) )
  :assumption
(or (not b240)  (not b807) )
  :assumption
(or b236  (not b807) )
  :assumption
(or (= r25 0)  b810 )
  :assumption
(or (not b810)  (= r25 29) )
  :assumption
(or b767  (not b810) )
  :assumption
(or (not b737)  (not b810) )
  :assumption
(or b240  (not b810) )
  :assumption
(or (= r26 0)  b813 )
  :assumption
(or (not b813)  (= r26 44) )
  :assumption
(or b759  (not b813) )
  :assumption
(or (not b242)  (not b813) )
  :assumption
(or b243  (not b813) )
  :assumption
(or (= r27 0)  b816 )
  :assumption
(or (not b816)  (= r27 44) )
  :assumption
(or b763  (not b816) )
  :assumption
(or (not b245)  (not b816) )
  :assumption
(or b242  (not b816) )
  :assumption
(or (= r28 0)  b819 )
  :assumption
(or (not b819)  (= r28 44) )
  :assumption
(or b767  (not b819) )
  :assumption
(or (not b780)  (not b819) )
  :assumption
(or b245  (not b819) )
  :assumption
(or (= r29 0)  b822 )
  :assumption
(or (not b822)  (= r29 77) )
  :assumption
(or b729  (not b822) )
  :assumption
(or (not b247)  (not b822) )
  :assumption
(or b248  (not b822) )
  :assumption
(or (= r30 0)  b825 )
  :assumption
(or (not b825)  (= r30 77) )
  :assumption
(or b733  (not b825) )
  :assumption
(or (not b250)  (not b825) )
  :assumption
(or b247  (not b825) )
  :assumption
(or (= r32 0)  b829 )
  :assumption
(or (not b829)  (= r32 97) )
  :assumption
(or b266  (not b829) )
  :assumption
(or (not b829)  (not b831) )
  :assumption
(or (not b829)  b832 )
  :assumption
(or (= r33 0)  b834 )
  :assumption
(or (not b834)  (= r33 97) )
  :assumption
(or b265  (not b834) )
  :assumption
(or (not b834)  (not b836) )
  :assumption
(or b831  (not b834) )
  :assumption
(or (= r34 0)  b838 )
  :assumption
(or (not b838)  (= r34 97) )
  :assumption
(or b269  (not b838) )
  :assumption
(or (not b838)  (not b840) )
  :assumption
(or b836  (not b838) )
  :assumption
(or (= r35 0)  b842 )
  :assumption
(or (not b842)  (= r35 97) )
  :assumption
(or (not b842)  b844 )
  :assumption
(or (not b842)  (not b845) )
  :assumption
(or b840  (not b842) )
  :assumption
(or (= r36 0)  b847 )
  :assumption
(or (not b847)  (= r36 77) )
  :assumption
(or b277  (not b847) )
  :assumption
(or (not b831)  (not b847) )
  :assumption
(or b832  (not b847) )
  :assumption
(or (= r37 0)  b850 )
  :assumption
(or (not b850)  (= r37 77) )
  :assumption
(or b276  (not b850) )
  :assumption
(or (not b836)  (not b850) )
  :assumption
(or b831  (not b850) )
  :assumption
(or (= r38 0)  b853 )
  :assumption
(or (not b853)  (= r38 77) )
  :assumption
(or b279  (not b853) )
  :assumption
(or (not b840)  (not b853) )
  :assumption
(or b836  (not b853) )
  :assumption
(or (= r39 0)  b856 )
  :assumption
(or (not b856)  (= r39 77) )
  :assumption
(or (not b856)  b858 )
  :assumption
(or (not b845)  (not b856) )
  :assumption
(or b840  (not b856) )
  :assumption
(or (= r40 0)  b860 )
  :assumption
(or (not b860)  (= r40 29) )
  :assumption
(or b266  (not b860) )
  :assumption
(or (not b860)  (not b862) )
  :assumption
(or (not b860)  b863 )
  :assumption
(or (= r41 0)  b865 )
  :assumption
(or (not b865)  (= r41 29) )
  :assumption
(or b265  (not b865) )
  :assumption
(or (not b865)  (not b867) )
  :assumption
(or b862  (not b865) )
  :assumption
(or (= r42 0)  b869 )
  :assumption
(or (not b869)  (= r42 29) )
  :assumption
(or b269  (not b869) )
  :assumption
(or (not b869)  (not b871) )
  :assumption
(or b867  (not b869) )
  :assumption
(or (= r43 0)  b873 )
  :assumption
(or (not b873)  (= r43 29) )
  :assumption
(or b844  (not b873) )
  :assumption
(or (not b873)  (not b875) )
  :assumption
(or b871  (not b873) )
  :assumption
(or (= r44 0)  b877 )
  :assumption
(or (not b877)  (= r44 44) )
  :assumption
(or b272  (not b877) )
  :assumption
(or (not b862)  (not b877) )
  :assumption
(or b863  (not b877) )
  :assumption
(or (= r45 0)  b880 )
  :assumption
(or (not b880)  (= r45 44) )
  :assumption
(or b271  (not b880) )
  :assumption
(or (not b867)  (not b880) )
  :assumption
(or b862  (not b880) )
  :assumption
(or (= r46 0)  b883 )
  :assumption
(or (not b883)  (= r46 44) )
  :assumption
(or b274  (not b883) )
  :assumption
(or (not b871)  (not b883) )
  :assumption
(or b867  (not b883) )
  :assumption
(or (= r47 0)  b886 )
  :assumption
(or (not b886)  (= r47 44) )
  :assumption
(or (not b875)  (not b886) )
  :assumption
(or b871  (not b886) )
  :assumption
(or (= r48 0)  b889 )
  :assumption
(or (not b889)  (= r48 97) )
  :assumption
(or b832  (not b889) )
  :assumption
(or (not b889)  (not b891) )
  :assumption
(or (= r49 0)  b893 )
  :assumption
(or (not b893)  (= r49 97) )
  :assumption
(or b831  (not b893) )
  :assumption
(or (not b266)  (not b893) )
  :assumption
(or b891  (not b893) )
  :assumption
(or (= r50 0)  b896 )
  :assumption
(or (not b896)  (= r50 97) )
  :assumption
(or b836  (not b896) )
  :assumption
(or (not b265)  (not b896) )
  :assumption
(or b266  (not b896) )
  :assumption
(or (= r51 0)  b899 )
  :assumption
(or (not b899)  (= r51 97) )
  :assumption
(or b840  (not b899) )
  :assumption
(or (not b269)  (not b899) )
  :assumption
(or b265  (not b899) )
  :assumption
(or (= r52 0)  b902 )
  :assumption
(or (not b902)  (= r52 97) )
  :assumption
(or b845  (not b902) )
  :assumption
(or (not b844)  (not b902) )
  :assumption
(or b269  (not b902) )
  :assumption
(or (= r53 0)  b905 )
  :assumption
(or (not b905)  (= r53 29) )
  :assumption
(or b863  (not b905) )
  :assumption
(or (not b891)  (not b905) )
  :assumption
(or (= r54 0)  b908 )
  :assumption
(or (not b908)  (= r54 29) )
  :assumption
(or b862  (not b908) )
  :assumption
(or (not b266)  (not b908) )
  :assumption
(or b891  (not b908) )
  :assumption
(or (= r55 0)  b911 )
  :assumption
(or (not b911)  (= r55 29) )
  :assumption
(or b867  (not b911) )
  :assumption
(or (not b265)  (not b911) )
  :assumption
(or b266  (not b911) )
  :assumption
(or (= r56 0)  b914 )
  :assumption
(or (not b914)  (= r56 29) )
  :assumption
(or b871  (not b914) )
  :assumption
(or (not b269)  (not b914) )
  :assumption
(or b265  (not b914) )
  :assumption
(or (= r57 0)  b917 )
  :assumption
(or (not b917)  (= r57 29) )
  :assumption
(or b875  (not b917) )
  :assumption
(or (not b844)  (not b917) )
  :assumption
(or b269  (not b917) )
  :assumption
(or (= r58 0)  b920 )
  :assumption
(or (not b920)  (= r58 44) )
  :assumption
(or b867  (not b920) )
  :assumption
(or (not b271)  (not b920) )
  :assumption
(or b272  (not b920) )
  :assumption
(or (= r59 0)  b923 )
  :assumption
(or (not b923)  (= r59 44) )
  :assumption
(or b871  (not b923) )
  :assumption
(or (not b274)  (not b923) )
  :assumption
(or b271  (not b923) )
  :assumption
(or (= r61 0)  b927 )
  :assumption
(or (not b927)  (= r61 77) )
  :assumption
(or b836  (not b927) )
  :assumption
(or (not b276)  (not b927) )
  :assumption
(or b277  (not b927) )
  :assumption
(or (= r62 0)  b930 )
  :assumption
(or (not b930)  (= r62 77) )
  :assumption
(or b840  (not b930) )
  :assumption
(or (not b279)  (not b930) )
  :assumption
(or b276  (not b930) )
  :assumption
(or (= r63 0)  b933 )
  :assumption
(or (not b933)  (= r63 77) )
  :assumption
(or b845  (not b933) )
  :assumption
(or (not b858)  (not b933) )
  :assumption
(or b279  (not b933) )
  :assumption
(or (or (not b103)  b180 )  b187 )
  :assumption
(or (not b102)  b103 )
  :assumption
(or (or (or (or b101  b102 )  (not b103) )  b109 )  b110 )
  :assumption
(or b102  (not b935) )
  :assumption
(or (not b102)  b935 )
  :assumption
(or (or b95  b97 )  b106 )
  :assumption
(or (or (or b97  (not b100) )  b179 )  b186 )
  :assumption
(or (not b97)  b100 )
  :assumption
(or (not b99)  b100 )
  :assumption
(or (or (or b98  b99 )  (not b100) )  b108 )
  :assumption
(or b99  (not b936) )
  :assumption
(or (not b99)  b936 )
  :assumption
(or (or (not b94)  b174 )  b181 )
  :assumption
(or (not b93)  b94 )
  :assumption
(or (or (or b91  b93 )  (not b94) )  b104 )
  :assumption
(or (or (or b93  b176 )  b183 )  b188 )
  :assumption
(or (or (not b82)  b165 )  b171 )
  :assumption
(or (not b81)  b82 )
  :assumption
(or (or (or (or b80  b81 )  (not b82) )  b88 )  b89 )
  :assumption
(or b81  (not b937) )
  :assumption
(or (not b81)  b937 )
  :assumption
(or (or b74  b76 )  b85 )
  :assumption
(or (or (or b76  (not b79) )  b162 )  b168 )
  :assumption
(or (not b76)  b79 )
  :assumption
(or (not b78)  b79 )
  :assumption
(or (or (or b77  b78 )  (not b79) )  b87 )
  :assumption
(or (or (or b78  b163 )  b169 )  b172 )
  :assumption
(or (or (not b73)  b160 )  b166 )
  :assumption
(or (not b72)  b73 )
  :assumption
(or (or (or b70  b72 )  (not b73) )  b83 )
  :assumption
(or b72  (not b938) )
  :assumption
(or (not b72)  b938 )
  :assumption
(or b65  b67 )
  :assumption
(or (or (not b62)  b67 )  b155 )
  :assumption
(or b62  (not b67) )
  :assumption
(or (not b61)  b62 )
  :assumption
(or (or (or (or b59  b61 )  (not b62) )  b63 )  b68 )
  :assumption
(or (or (or b61  b149 )  b152 )  b157 )
  :assumption
(or (or (not b50)  b140 )  b146 )
  :assumption
(or (not b49)  b50 )
  :assumption
(or (or (or (or b48  b49 )  (not b50) )  b56 )  b57 )
  :assumption
(or b49  (not b939) )
  :assumption
(or (not b49)  b939 )
  :assumption
(or (or b42  b44 )  b53 )
  :assumption
(or (or (or b44  (not b47) )  b137 )  b143 )
  :assumption
(or (not b44)  b47 )
  :assumption
(or (not b46)  b47 )
  :assumption
(or (or (or b45  b46 )  (not b47) )  b55 )
  :assumption
(or (or (or b46  b138 )  b144 )  b147 )
  :assumption
(or (or (not b41)  b135 )  b141 )
  :assumption
(or (not b40)  b41 )
  :assumption
(or (or (or b38  b40 )  (not b41) )  b51 )
  :assumption
(or b40  (not b940) )
  :assumption
(or (not b40)  b940 )
  :assumption
(or (or (not b26)  b120 )  b130 )
  :assumption
(or (not b24)  b26 )
  :assumption
(or (or (or (or b23  b24 )  (not b26) )  b34 )  b36 )
  :assumption
(or b24  (not b941) )
  :assumption
(or (not b24)  b941 )
  :assumption
(or (or b16  b18 )  b30 )
  :assumption
(or (or (or b18  (not b22) )  b115 )  b125 )
  :assumption
(or (not b18)  b22 )
  :assumption
(or (not b20)  b22 )
  :assumption
(or (or (or b19  b20 )  (not b22) )  b32 )
  :assumption
(or (or (or b20  b117 )  b127 )  b132 )
  :assumption
(or (or (not b15)  b112 )  b122 )
  :assumption
(or (not b13)  b15 )
  :assumption
(or (or (or b11  b13 )  (not b15) )  b27 )
  :assumption
(or b13  (not b942) )
  :assumption
(or (not b13)  b942 )
  :assumption
(or (or (or (or b159  b619 )  b623 )  b628 )  b632 )
  :assumption
(or (or (or (or (or (or b159  b591 )  b594 )  b597 )  b609 )  b612 )  b615 )
  :assumption
(or (or (not b134)  b628 )  b632 )
  :assumption
(or (or (or (or b134  b580 )  (not b582) )  b585 )  b588 )
  :assumption
(or (or (or (or (or (or (or (not b134)  b582 )  b600 )  b603 )  b606 )  b609 )  b612 )  b615 )
  :assumption
(or (or (not b190)  b619 )  b623 )
  :assumption
(or (or (or (or b190  (not b583) )  b600 )  b603 )  b606 )
  :assumption
(or (or (or (or (or (or (or (not b190)  b580 )  b583 )  b585 )  b588 )  b591 )  b594 )  b597 )
  :assumption
(or (not b131)  b526 )
  :assumption
(or (or (or (not b35)  b131 )  b481 )  b529 )
  :assumption
(or (or (or b35  (not b131) )  b550 )  b565 )
  :assumption
(or (or (or (or (or (or (or b35  (not b154) )  b484 )  b490 )  b496 )  b532 )  b538 )  b544 )
  :assumption
(or (or (or (or (or (or (or (not b35)  b154 )  b553 )  b557 )  b561 )  b568 )  b572 )  b576 )
  :assumption
(or (or (or (or (or (or b154  b487 )  b493 )  b499 )  b535 )  b541 )  b547 )
  :assumption
(or (or b126  b502 )  b526 )
  :assumption
(or (or (or (not b33)  b126 )  b458 )  b565 )
  :assumption
(or (or (or b33  (not b126) )  b505 )  b529 )
  :assumption
(or (or (or (or (or (or (or b33  (not b129) )  b461 )  b469 )  b475 )  b568 )  b572 )  b576 )
  :assumption
(or (or (or (or (or (or (or (not b33)  b129 )  b508 )  b514 )  b520 )  b532 )  b538 )  b544 )
  :assumption
(or (or (or (or b129  b464 )  (not b466) )  b472 )  b478 )
  :assumption
(or (or (or (or (or (or (or (not b129)  b466 )  b511 )  b517 )  b523 )  b535 )  b541 )  b547 )
  :assumption
(or (not b124)  b502 )
  :assumption
(or (or (or (not b29)  b124 )  b505 )  b550 )
  :assumption
(or (or (or b29  (not b124) )  b458 )  b481 )
  :assumption
(or (or (or (or (or (or (or b29  (not b185) )  b508 )  b514 )  b520 )  b553 )  b557 )  b561 )
  :assumption
(or (or (or (or (or (or (or (not b29)  b185 )  b461 )  b469 )  b475 )  b484 )  b490 )  b496 )
  :assumption
(or (or (or (or b185  (not b467) )  b511 )  b517 )  b523 )
  :assumption
(or (or (or (or (or (or (or (not b185)  b464 )  b467 )  b472 )  b478 )  b487 )  b493 )  b499 )
  :assumption
(or (not b121)  b392 )
  :assumption
(or (or (or (not b25)  b121 )  b352 )  b395 )
  :assumption
(or (or (or b25  (not b121) )  b416 )  b437 )
  :assumption
(or (or (or (or (or (or (or b25  (not b151) )  b355 )  b360 )  b364 )  b398 )  b404 )  b410 )
  :assumption
(or (or (or (or (or (or (or (not b25)  b151 )  b419 )  b425 )  b431 )  b440 )  b446 )  b452 )
  :assumption
(or (or (or (or b151  (not b358) )  b401 )  b407 )  b413 )
  :assumption
(or (or (or (or (or (or (or (not b151)  b358 )  b422 )  b428 )  b434 )  b443 )  b449 )  b455 )
  :assumption
(or (or b116  b368 )  b392 )
  :assumption
(or (or (or (not b21)  b116 )  b336 )  b437 )
  :assumption
(or (or (or b21  (not b116) )  b371 )  b395 )
  :assumption
(or (or (or (or (or (or (or b21  (not b119) )  b339 )  b344 )  b348 )  b440 )  b446 )  b452 )
  :assumption
(or (or (or (or (or (or (or (not b21)  b119 )  b374 )  b380 )  b386 )  b398 )  b404 )  b410 )
  :assumption
(or (or (or (or b119  (not b342) )  b443 )  b449 )  b455 )
  :assumption
(or (or (or (or (or (or (or (not b119)  b342 )  b377 )  b383 )  b389 )  b401 )  b407 )  b413 )
  :assumption
(or (not b114)  b368 )
  :assumption
(or (or (or (not b14)  b114 )  b371 )  b416 )
  :assumption
(or (or (or b14  (not b114) )  b336 )  b352 )
  :assumption
(or (or (or (or (or (or (or b14  (not b178) )  b374 )  b380 )  b386 )  b419 )  b425 )  b431 )
  :assumption
(or (or (or (or (or (or (or (not b14)  b178 )  b339 )  b344 )  b348 )  b355 )  b360 )  b364 )
  :assumption
(or (or (or (or (or (or b178  b377 )  b383 )  b389 )  b422 )  b428 )  b434 )
  :assumption
(or (not b277)  b847 )
  :assumption
(or (or (not b276)  b277 )  b850 )
  :assumption
(or (or (or (or (or b275  b276 )  (not b277) )  b286 )  b288 )  b927 )
  :assumption
(or (or (or (or (or b276  (not b279) )  b326 )  b331 )  b334 )  b853 )
  :assumption
(or (or (or (or (or (not b276)  b278 )  b279 )  b287 )  b290 )  b930 )
  :assumption
(or (or b279  b856 )  (not b858) )
  :assumption
(or (or (not b279)  b858 )  b933 )
  :assumption
(or (not b272)  b877 )
  :assumption
(or (or (not b271)  b272 )  b880 )
  :assumption
(or (or (or (or b270  b271 )  (not b272) )  b284 )  b920 )
  :assumption
(or (or (or (or b271  (not b274) )  b323 )  b328 )  b883 )
  :assumption
(or (or (or (or (not b271)  b273 )  b274 )  b285 )  b923 )
  :assumption
(or (or (or (or b274  b324 )  b329 )  b332 )  b886 )
  :assumption
(or (or b889  b891 )  b905 )
  :assumption
(or (or (or (not b266)  b829 )  b860 )  b891 )
  :assumption
(or (or (or b266  (not b891) )  b893 )  b908 )
  :assumption
(or (or (or (not b265)  b266 )  b834 )  b865 )
  :assumption
(or (or (or (or (or b263  b265 )  (not b266) )  b280 )  b896 )  b911 )
  :assumption
(or (or (or (or (or b265  (not b269) )  b322 )  b327 )  b838 )  b869 )
  :assumption
(or (or (or (or (or (not b265)  b267 )  b269 )  b282 )  b899 )  b914 )
  :assumption
(or (or (or b269  b842 )  (not b844) )  b873 )
  :assumption
(or (or (or (not b269)  b844 )  b902 )  b917 )
  :assumption
(or (not b863)  b905 )
  :assumption
(or (or (not b862)  b863 )  b908 )
  :assumption
(or (or (or b860  b862 )  (not b863) )  b877 )
  :assumption
(or (or (or b862  (not b867) )  b911 )  b920 )
  :assumption
(or (or (or (not b862)  b865 )  b867 )  b880 )
  :assumption
(or (or (or b867  (not b871) )  b914 )  b923 )
  :assumption
(or (or (or (not b867)  b869 )  b871 )  b883 )
  :assumption
(or (or b871  (not b875) )  b917 )
  :assumption
(or (or (or (not b871)  b873 )  b875 )  b886 )
  :assumption
(or (not b832)  b889 )
  :assumption
(or (or (not b831)  b832 )  b893 )
  :assumption
(or (or (or b829  b831 )  (not b832) )  b847 )
  :assumption
(or (or (or b831  (not b836) )  b896 )  b927 )
  :assumption
(or (or (or (not b831)  b834 )  b836 )  b850 )
  :assumption
(or (or (or b836  (not b840) )  b899 )  b930 )
  :assumption
(or (or (or (not b836)  b838 )  b840 )  b853 )
  :assumption
(or (or (or b840  (not b845) )  b902 )  b933 )
  :assumption
(or (or (or (not b840)  b842 )  b845 )  b856 )
  :assumption
(or (not b248)  b740 )
  :assumption
(or (or (not b247)  b248 )  b743 )
  :assumption
(or (or (or (or (or b246  b247 )  (not b248) )  b257 )  b259 )  b822 )
  :assumption
(or (or (or (or (or b247  (not b250) )  b308 )  b314 )  b318 )  b746 )
  :assumption
(or (or (or (or (or (not b247)  b249 )  b250 )  b258 )  b261 )  b825 )
  :assumption
(or (or (or (or b250  b309 )  b315 )  b319 )  b749 )
  :assumption
(or (not b243)  b769 )
  :assumption
(or (or (not b242)  b243 )  b772 )
  :assumption
(or (or (or (or b241  b242 )  (not b243) )  b255 )  b813 )
  :assumption
(or (or (or (or b242  (not b245) )  b307 )  b313 )  b775 )
  :assumption
(or (or (or (or (not b242)  b244 )  b245 )  b256 )  b816 )
  :assumption
(or (or b245  b778 )  (not b780) )
  :assumption
(or (or (not b245)  b780 )  b819 )
  :assumption
(or (or b782  b784 )  b798 )
  :assumption
(or (or (or (not b237)  b722 )  b752 )  b784 )
  :assumption
(or (or (or b237  (not b784) )  b786 )  b801 )
  :assumption
(or (or (or (not b236)  b237 )  b727 )  b757 )
  :assumption
(or (or (or (or (or b234  b236 )  (not b237) )  b251 )  b789 )  b804 )
  :assumption
(or (or (or (or (or b236  (not b240) )  b306 )  b312 )  b731 )  b761 )
  :assumption
(or (or (or (or (or (not b236)  b238 )  b240 )  b253 )  b792 )  b807 )
  :assumption
(or (or (or b240  b735 )  (not b737) )  b765 )
  :assumption
(or (or (or (not b240)  b737 )  b795 )  b810 )
  :assumption
(or (not b755)  b798 )
  :assumption
(or (or (not b754)  b755 )  b801 )
  :assumption
(or (or (or b752  b754 )  (not b755) )  b769 )
  :assumption
(or (or (or b754  (not b759) )  b804 )  b813 )
  :assumption
(or (or (or (not b754)  b757 )  b759 )  b772 )
  :assumption
(or (or (or b759  (not b763) )  b807 )  b816 )
  :assumption
(or (or (or (not b759)  b761 )  b763 )  b775 )
  :assumption
(or (or (or b763  (not b767) )  b810 )  b819 )
  :assumption
(or (or (or (not b763)  b765 )  b767 )  b778 )
  :assumption
(or (not b725)  b782 )
  :assumption
(or (or (not b724)  b725 )  b786 )
  :assumption
(or (or (or b722  b724 )  (not b725) )  b740 )
  :assumption
(or (or (or b724  (not b729) )  b789 )  b822 )
  :assumption
(or (or (or (not b724)  b727 )  b729 )  b743 )
  :assumption
(or (or (or b729  (not b733) )  b792 )  b825 )
  :assumption
(or (or (or (not b729)  b731 )  b733 )  b746 )
  :assumption
(or (or b733  (not b738) )  b795 )
  :assumption
(or (or (or (not b733)  b735 )  b738 )  b749 )
  :assumption
(or (or (not b214)  b297 )  b304 )
  :assumption
(or (or (or (or (not b213)  b214 )  b298 )  b305 )  b646 )
  :assumption
(or (or (or (or (or b212  b213 )  (not b214) )  b229 )  b230 )  b716 )
  :assumption
(or (or b213  b649 )  (not b651) )
  :assumption
(or (or (not b213)  b651 )  b719 )
  :assumption
(or (or (or b201  b204 )  b222 )  b701 )
  :assumption
(or (or (or (or b204  (not b207) )  b294 )  b301 )  b670 )
  :assumption
(or (or (or (or (not b204)  b205 )  b207 )  b225 )  b704 )
  :assumption
(or (or (or (or b207  (not b209) )  b295 )  b302 )  b673 )
  :assumption
(or (or (or (or (not b207)  b208 )  b209 )  b227 )  b707 )
  :assumption
(or (or (or (or b209  (not b211) )  b296 )  b303 )  b676 )
  :assumption
(or (or (or (or (not b209)  b210 )  b211 )  b228 )  b710 )
  :assumption
(or (or b211  b679 )  (not b681) )
  :assumption
(or (or (not b211)  b681 )  b713 )
  :assumption
(or (not b195)  b653 )
  :assumption
(or (or (or (or (not b194)  b195 )  b292 )  b299 )  b658 )
  :assumption
(or (or (or (or (or b191  b194 )  (not b195) )  b215 )  b683 )  b692 )
  :assumption
(or (or (or (or (or b194  (not b200) )  b293 )  b300 )  b636 )  b662 )
  :assumption
(or (or (or (or (or (not b194)  b197 )  b200 )  b219 )  b686 )  b695 )
  :assumption
(or (or (or b200  b641 )  (not b643) )  b666 )
  :assumption
(or (or (or (not b200)  b643 )  b689 )  b698 )
  :assumption
(or (not b656)  b701 )
  :assumption
(or (or (not b655)  b656 )  b704 )
  :assumption
(or (or (or b653  b655 )  (not b656) )  b670 )
  :assumption
(or (or (or b655  (not b660) )  b692 )  b707 )
  :assumption
(or (or (or (not b655)  b658 )  b660 )  b673 )
  :assumption
(or (or (or b660  (not b664) )  b695 )  b710 )
  :assumption
(or (or (or (not b660)  b662 )  b664 )  b676 )
  :assumption
(or (or (or b664  (not b668) )  b698 )  b713 )
  :assumption
(or (or (or (not b664)  b666 )  b668 )  b679 )
  :assumption
(or (not b639)  b683 )
  :assumption
(or (or (or (not b638)  b639 )  b686 )  b716 )
  :assumption
(or (or (or b636  b638 )  (not b639) )  b646 )
  :assumption
(or (or (or b638  (not b644) )  b689 )  b719 )
  :assumption
(or (or (or (not b638)  b641 )  b644 )  b649 )
  :assumption
(or b110  (not b111) )
  :assumption
(or b111  (not b189) )
  :assumption
(or (or (not b111)  b188 )  b189 )
  :assumption
(or b106  (not b107) )
  :assumption
(or b107  (not b182) )
  :assumption
(or (or (or (or (not b107)  b181 )  b182 )  b186 )  b187 )
  :assumption
(or (or (or (or b104  (not b105) )  b108 )  b109 )  b182 )
  :assumption
(or b105  (not b182) )
  :assumption
(or b105  (not b184) )
  :assumption
(or (or (not b105)  b183 )  b184 )
  :assumption
(or b95  (not b96) )
  :assumption
(or b96  (not b175) )
  :assumption
(or (or (or (or (not b96)  b174 )  b175 )  b179 )  b180 )
  :assumption
(or (or (or (or b91  (not b92) )  b98 )  b101 )  b175 )
  :assumption
(or b92  (not b175) )
  :assumption
(or b92  (not b177) )
  :assumption
(or (or (not b92)  b176 )  b177 )
  :assumption
(or b89  (not b90) )
  :assumption
(or b90  (not b173) )
  :assumption
(or (or (not b90)  b172 )  b173 )
  :assumption
(or b85  (not b86) )
  :assumption
(or b86  (not b167) )
  :assumption
(or (or (or (or (not b86)  b166 )  b167 )  b168 )  b171 )
  :assumption
(or (or (or (or b83  (not b84) )  b87 )  b88 )  b167 )
  :assumption
(or b84  (not b167) )
  :assumption
(or b84  (not b170) )
  :assumption
(or (or (not b84)  b169 )  b170 )
  :assumption
(or b74  (not b75) )
  :assumption
(or b75  (not b161) )
  :assumption
(or (or (or (or (not b75)  b160 )  b161 )  b162 )  b165 )
  :assumption
(or (or (or (or b70  (not b71) )  b77 )  b80 )  b161 )
  :assumption
(or b71  (not b161) )
  :assumption
(or b71  (not b164) )
  :assumption
(or (or (not b71)  b163 )  b164 )
  :assumption
(or b65  (not b66) )
  :assumption
(or b66  (not b156) )
  :assumption
(or (or (not b66)  b155 )  b156 )
  :assumption
(or (or b68  (not b69) )  b156 )
  :assumption
(or b69  (not b156) )
  :assumption
(or b69  (not b158) )
  :assumption
(or (or (not b69)  b157 )  b158 )
  :assumption
(or b63  (not b64) )
  :assumption
(or b64  (not b153) )
  :assumption
(or (or (not b64)  b152 )  b153 )
  :assumption
(or b59  (not b60) )
  :assumption
(or b60  (not b150) )
  :assumption
(or (or (not b60)  b149 )  b150 )
  :assumption
(or b57  (not b58) )
  :assumption
(or b58  (not b148) )
  :assumption
(or (or (not b58)  b147 )  b148 )
  :assumption
(or b53  (not b54) )
  :assumption
(or b54  (not b142) )
  :assumption
(or (or (or (or (not b54)  b141 )  b142 )  b143 )  b146 )
  :assumption
(or (or (or (or b51  (not b52) )  b55 )  b56 )  b142 )
  :assumption
(or b52  (not b142) )
  :assumption
(or b52  (not b145) )
  :assumption
(or (or (not b52)  b144 )  b145 )
  :assumption
(or b42  (not b43) )
  :assumption
(or b43  (not b136) )
  :assumption
(or (or (or (or (not b43)  b135 )  b136 )  b137 )  b140 )
  :assumption
(or (or (or (or b38  (not b39) )  b45 )  b48 )  b136 )
  :assumption
(or b39  (not b136) )
  :assumption
(or b39  (not b139) )
  :assumption
(or (or (not b39)  b138 )  b139 )
  :assumption
(or b36  (not b37) )
  :assumption
(or b37  (not b133) )
  :assumption
(or (or (not b37)  b132 )  b133 )
  :assumption
(or b30  (not b31) )
  :assumption
(or b31  (not b123) )
  :assumption
(or (or (or (or (not b31)  b122 )  b123 )  b125 )  b130 )
  :assumption
(or (or (or (or b27  (not b28) )  b32 )  b34 )  b123 )
  :assumption
(or b28  (not b123) )
  :assumption
(or b28  (not b128) )
  :assumption
(or (or (not b28)  b127 )  b128 )
  :assumption
(or b16  (not b17) )
  :assumption
(or b17  (not b113) )
  :assumption
(or (or (or (or (not b17)  b112 )  b113 )  b115 )  b120 )
  :assumption
(or (or (or (or b11  (not b12) )  b19 )  b23 )  b113 )
  :assumption
(or b12  (not b113) )
  :assumption
(or b12  (not b118) )
  :assumption
(or (or (not b12)  b117 )  b118 )
  :assumption
(or b288  (not b289) )
  :assumption
(or (or b289  b290 )  (not b291) )
  :assumption
(or (or (not b289)  b291 )  b334 )
  :assumption
(or b291  (not b333) )
  :assumption
(or (or (not b291)  b332 )  b333 )
  :assumption
(or (or (or b280  (not b281) )  b284 )  b286 )
  :assumption
(or (or (or (or b281  b282 )  (not b283) )  b285 )  b287 )
  :assumption
(or (or (or (or (not b281)  b283 )  b327 )  b328 )  b331 )
  :assumption
(or b283  (not b330) )
  :assumption
(or (or (not b283)  b329 )  b330 )
  :assumption
(or (or (or b263  (not b264) )  b270 )  b275 )
  :assumption
(or (or (or (or b264  b267 )  (not b268) )  b273 )  b278 )
  :assumption
(or (or (or (or (not b264)  b268 )  b322 )  b323 )  b326 )
  :assumption
(or b268  (not b325) )
  :assumption
(or (or (not b268)  b324 )  b325 )
  :assumption
(or b259  (not b260) )
  :assumption
(or (or b260  b261 )  (not b262) )
  :assumption
(or (or (not b260)  b262 )  b318 )
  :assumption
(or b262  (not b321) )
  :assumption
(or (or (not b262)  b319 )  b321 )
  :assumption
(or (or (or b251  (not b252) )  b255 )  b257 )
  :assumption
(or (or (or (or b252  b253 )  (not b254) )  b256 )  b258 )
  :assumption
(or (or (or (or (not b252)  b254 )  b312 )  b313 )  b314 )
  :assumption
(or b254  (not b317) )
  :assumption
(or (or (not b254)  b315 )  b317 )
  :assumption
(or (or (or b234  (not b235) )  b241 )  b246 )
  :assumption
(or (or (or (or b235  b238 )  (not b239) )  b244 )  b249 )
  :assumption
(or (or (or (or (not b235)  b239 )  b306 )  b307 )  b308 )
  :assumption
(or b239  (not b311) )
  :assumption
(or (or (not b239)  b309 )  b311 )
  :assumption
(or b230  (not b232) )
  :assumption
(or b232  (not b943) )
  :assumption
(or (not b232)  b943 )
  :assumption
(or b222  (not b224) )
  :assumption
(or (or b224  b225 )  (not b226) )
  :assumption
(or (or (not b224)  b226 )  b301 )
  :assumption
(or (or (or b215  (not b217) )  b226 )  b227 )
  :assumption
(or (or (or (or b217  (not b226) )  b299 )  b302 )  b304 )
  :assumption
(or (or (or (or b217  b219 )  (not b221) )  b228 )  b229 )
  :assumption
(or (or (or (or (not b217)  b221 )  b300 )  b303 )  b305 )
  :assumption
(or b221  (not b944) )
  :assumption
(or (not b221)  b944 )
  :assumption
(or b201  (not b203) )
  :assumption
(or (or b203  b205 )  (not b206) )
  :assumption
(or (or (not b203)  b206 )  b294 )
  :assumption
(or (or (or b191  (not b193) )  b206 )  b208 )
  :assumption
(or (or (or (or b193  (not b206) )  b292 )  b295 )  b297 )
  :assumption
(or (or (or (or b193  b197 )  (not b199) )  b210 )  b212 )
  :assumption
(or (or (or (or (not b193)  b199 )  b293 )  b296 )  b298 )
  :assumption
(or b199  (not b945) )
  :assumption
(or (not b199)  b945 )
  :assumption
(or (or b233  b259 )  b288 )
  :assumption
(or (or (or (not b231)  b233 )  b318 )  b334 )
  :assumption
(or (or (or (or b230  b231 )  (not b233) )  b261 )  b290 )
  :assumption
(or (or (or b231  b319 )  (not b320) )  b332 )
  :assumption
(or (not b231)  b320 )
  :assumption
(or b222  b223 )
  :assumption
(or (or (not b218)  b223 )  b301 )
  :assumption
(or (or b218  (not b223) )  b225 )
  :assumption
(or (or (or (or (not b216)  b218 )  b299 )  b302 )  b304 )
  :assumption
(or (or (or (or (or (or (or (or (or b215  b216 )  (not b218) )  b227 )  b251 )  b255 )  b257 )  b280 )  b284 )  b286 )
  :assumption
(or (or (or (or (or (or (or (or (or (or b216  (not b220) )  b300 )  b303 )  b305 )  b312 )  b313 )  b314 )  b327 )  b328 )  b331 )
  :assumption
(or (or (or (or (or (or (or (or (or (or (not b216)  b219 )  b220 )  b228 )  b229 )  b253 )  b256 )  b258 )  b282 )  b285 )  b287 )
  :assumption
(or (or (or b220  b315 )  (not b316) )  b329 )
  :assumption
(or (not b220)  b316 )
  :assumption
(or b201  b202 )
  :assumption
(or (or (not b196)  b202 )  b294 )
  :assumption
(or (or b196  (not b202) )  b205 )
  :assumption
(or (or (or (or (not b192)  b196 )  b292 )  b295 )  b297 )
  :assumption
(or (or (or (or (or (or (or (or (or b191  b192 )  (not b196) )  b208 )  b234 )  b241 )  b246 )  b263 )  b270 )  b275 )
  :assumption
(or (or (or (or (or (or (or (or (or (or b192  (not b198) )  b293 )  b296 )  b298 )  b306 )  b307 )  b308 )  b322 )  b323 )  b326 )
  :assumption
(or (or (or (or (or (or (or (or (or (or (not b192)  b197 )  b198 )  b210 )  b212 )  b238 )  b244 )  b249 )  b267 )  b273 )  b278 )
  :assumption
(or (or (or b198  b309 )  (not b310) )  b324 )
  :assumption
(or (not b198)  b310 )
  :assumption
(or (not b11)  (not b27) )
  :assumption
(or (not b16)  (not b30) )
  :assumption
(or (not b19)  (not b32) )
  :assumption
(or (not b23)  (not b36) )
  :assumption
(or (not b23)  (not b34) )
  :assumption
(or (not b34)  (not b36) )
  :assumption
(or (not b38)  (not b51) )
  :assumption
(or (not b42)  (not b53) )
  :assumption
(or (not b45)  (not b55) )
  :assumption
(or (not b48)  (not b57) )
  :assumption
(or (not b48)  (not b56) )
  :assumption
(or (not b56)  (not b57) )
  :assumption
(or (not b59)  (not b68) )
  :assumption
(or (not b59)  (not b63) )
  :assumption
(or (not b63)  (not b68) )
  :assumption
(or (not b70)  (not b83) )
  :assumption
(or (not b74)  (not b85) )
  :assumption
(or (not b77)  (not b87) )
  :assumption
(or (not b80)  (not b89) )
  :assumption
(or (not b80)  (not b88) )
  :assumption
(or (not b88)  (not b89) )
  :assumption
(or (not b91)  (not b104) )
  :assumption
(or (not b95)  (not b106) )
  :assumption
(or (not b98)  (not b108) )
  :assumption
(or (not b101)  (not b110) )
  :assumption
(or (not b101)  (not b109) )
  :assumption
(or (not b109)  (not b110) )
  :assumption
(or (not b112)  (not b120) )
  :assumption
(or (not b112)  (not b115) )
  :assumption
(or (not b115)  (not b120) )
  :assumption
(or (not b122)  (not b130) )
  :assumption
(or (not b122)  (not b125) )
  :assumption
(or (not b125)  (not b130) )
  :assumption
(or (not b135)  (not b140) )
  :assumption
(or (not b135)  (not b137) )
  :assumption
(or (not b137)  (not b140) )
  :assumption
(or (not b141)  (not b146) )
  :assumption
(or (not b141)  (not b143) )
  :assumption
(or (not b143)  (not b146) )
  :assumption
(or (not b160)  (not b165) )
  :assumption
(or (not b160)  (not b162) )
  :assumption
(or (not b162)  (not b165) )
  :assumption
(or (not b166)  (not b171) )
  :assumption
(or (not b166)  (not b168) )
  :assumption
(or (not b168)  (not b171) )
  :assumption
(or (not b174)  (not b180) )
  :assumption
(or (not b174)  (not b179) )
  :assumption
(or (not b179)  (not b180) )
  :assumption
(or (not b181)  (not b187) )
  :assumption
(or (not b181)  (not b186) )
  :assumption
(or (not b186)  (not b187) )
  :assumption
(or (not b191)  (not b692) )
  :assumption
(or (not b197)  (not b695) )
  :assumption
(or (not b191)  (not b683) )
  :assumption
(or (not b197)  (not b686) )
  :assumption
(or (not b191)  (not b215) )
  :assumption
(or (not b197)  (not b219) )
  :assumption
(or (not b191)  (not b658) )
  :assumption
(or (not b197)  (not b662) )
  :assumption
(or (not b197)  (not b636) )
  :assumption
(or (not b191)  (not b299) )
  :assumption
(or (not b197)  (not b300) )
  :assumption
(or (not b191)  (not b292) )
  :assumption
(or (not b197)  (not b293) )
  :assumption
(or (not b191)  (not b437) )
  :assumption
(or (not b197)  (not b440) )
  :assumption
(or (not b191)  (not b416) )
  :assumption
(or (not b197)  (not b419) )
  :assumption
(or (not b191)  (not b395) )
  :assumption
(or (not b197)  (not b398) )
  :assumption
(or (not b191)  (not b371) )
  :assumption
(or (not b197)  (not b374) )
  :assumption
(or (not b191)  (not b352) )
  :assumption
(or (not b197)  (not b355) )
  :assumption
(or (not b191)  (not b336) )
  :assumption
(or (not b197)  (not b339) )
  :assumption
(or (not b191)  (not b297) )
  :assumption
(or (not b197)  (not b298) )
  :assumption
(or (not b191)  (not b295) )
  :assumption
(or (not b197)  (not b296) )
  :assumption
(or (not b191)  (not b275) )
  :assumption
(or (not b197)  (not b278) )
  :assumption
(or (not b191)  (not b270) )
  :assumption
(or (not b197)  (not b273) )
  :assumption
(or (not b191)  (not b263) )
  :assumption
(or (not b197)  (not b267) )
  :assumption
(or (not b191)  (not b246) )
  :assumption
(or (not b197)  (not b249) )
  :assumption
(or (not b191)  (not b241) )
  :assumption
(or (not b197)  (not b244) )
  :assumption
(or (not b191)  (not b234) )
  :assumption
(or (not b197)  (not b238) )
  :assumption
(or (not b197)  (not b212) )
  :assumption
(or (not b191)  (not b208) )
  :assumption
(or (not b197)  (not b210) )
  :assumption
(or (not b197)  (not b326) )
  :assumption
(or (not b197)  (not b323) )
  :assumption
(or (not b197)  (not b322) )
  :assumption
(or (not b197)  (not b308) )
  :assumption
(or (not b197)  (not b307) )
  :assumption
(or (not b197)  (not b306) )
  :assumption
(or (not b201)  (not b701) )
  :assumption
(or (not b205)  (not b704) )
  :assumption
(or (not b208)  (not b707) )
  :assumption
(or (not b210)  (not b710) )
  :assumption
(or (not b201)  (not b222) )
  :assumption
(or (not b205)  (not b225) )
  :assumption
(or (not b208)  (not b227) )
  :assumption
(or (not b210)  (not b228) )
  :assumption
(or (not b205)  (not b670) )
  :assumption
(or (not b208)  (not b673) )
  :assumption
(or (not b210)  (not b676) )
  :assumption
(or (not b205)  (not b301) )
  :assumption
(or (not b208)  (not b302) )
  :assumption
(or (not b210)  (not b303) )
  :assumption
(or (not b205)  (not b294) )
  :assumption
(or (not b208)  (not b295) )
  :assumption
(or (not b210)  (not b296) )
  :assumption
(or (not b208)  (not b437) )
  :assumption
(or (not b210)  (not b440) )
  :assumption
(or (not b208)  (not b416) )
  :assumption
(or (not b210)  (not b419) )
  :assumption
(or (not b205)  (not b392) )
  :assumption
(or (not b208)  (not b395) )
  :assumption
(or (not b210)  (not b398) )
  :assumption
(or (not b205)  (not b368) )
  :assumption
(or (not b208)  (not b371) )
  :assumption
(or (not b210)  (not b374) )
  :assumption
(or (not b208)  (not b352) )
  :assumption
(or (not b210)  (not b355) )
  :assumption
(or (not b208)  (not b336) )
  :assumption
(or (not b210)  (not b339) )
  :assumption
(or (not b208)  (not b297) )
  :assumption
(or (not b210)  (not b298) )
  :assumption
(or (not b208)  (not b292) )
  :assumption
(or (not b210)  (not b293) )
  :assumption
(or (not b208)  (not b275) )
  :assumption
(or (not b210)  (not b278) )
  :assumption
(or (not b208)  (not b270) )
  :assumption
(or (not b210)  (not b273) )
  :assumption
(or (not b208)  (not b263) )
  :assumption
(or (not b210)  (not b267) )
  :assumption
(or (not b208)  (not b246) )
  :assumption
(or (not b210)  (not b249) )
  :assumption
(or (not b208)  (not b241) )
  :assumption
(or (not b210)  (not b244) )
  :assumption
(or (not b208)  (not b234) )
  :assumption
(or (not b210)  (not b238) )
  :assumption
(or (not b210)  (not b212) )
  :assumption
(or (not b210)  (not b326) )
  :assumption
(or (not b210)  (not b323) )
  :assumption
(or (not b210)  (not b322) )
  :assumption
(or (not b210)  (not b308) )
  :assumption
(or (not b210)  (not b307) )
  :assumption
(or (not b210)  (not b306) )
  :assumption
(or (not b212)  (not b716) )
  :assumption
(or (not b212)  (not b230) )
  :assumption
(or (not b212)  (not b229) )
  :assumption
(or (not b212)  (not b646) )
  :assumption
(or (not b212)  (not b305) )
  :assumption
(or (not b212)  (not b298) )
  :assumption
(or (not b212)  (not b440) )
  :assumption
(or (not b212)  (not b419) )
  :assumption
(or (not b212)  (not b398) )
  :assumption
(or (not b212)  (not b374) )
  :assumption
(or (not b212)  (not b355) )
  :assumption
(or (not b212)  (not b339) )
  :assumption
(or (not b212)  (not b296) )
  :assumption
(or (not b212)  (not b293) )
  :assumption
(or (not b212)  (not b278) )
  :assumption
(or (not b212)  (not b273) )
  :assumption
(or (not b212)  (not b267) )
  :assumption
(or (not b212)  (not b249) )
  :assumption
(or (not b212)  (not b244) )
  :assumption
(or (not b212)  (not b238) )
  :assumption
(or (not b212)  (not b326) )
  :assumption
(or (not b212)  (not b323) )
  :assumption
(or (not b212)  (not b322) )
  :assumption
(or (not b212)  (not b308) )
  :assumption
(or (not b212)  (not b307) )
  :assumption
(or (not b212)  (not b306) )
  :assumption
(or (not b215)  (not b692) )
  :assumption
(or (not b219)  (not b695) )
  :assumption
(or (not b215)  (not b683) )
  :assumption
(or (not b219)  (not b686) )
  :assumption
(or (not b215)  (not b658) )
  :assumption
(or (not b219)  (not b662) )
  :assumption
(or (not b219)  (not b636) )
  :assumption
(or (not b215)  (not b299) )
  :assumption
(or (not b219)  (not b300) )
  :assumption
(or (not b215)  (not b292) )
  :assumption
(or (not b219)  (not b293) )
  :assumption
(or (not b215)  (not b565) )
  :assumption
(or (not b219)  (not b568) )
  :assumption
(or (not b215)  (not b550) )
  :assumption
(or (not b219)  (not b553) )
  :assumption
(or (not b215)  (not b529) )
  :assumption
(or (not b219)  (not b532) )
  :assumption
(or (not b215)  (not b505) )
  :assumption
(or (not b219)  (not b508) )
  :assumption
(or (not b215)  (not b481) )
  :assumption
(or (not b219)  (not b484) )
  :assumption
(or (not b215)  (not b458) )
  :assumption
(or (not b219)  (not b461) )
  :assumption
(or (not b215)  (not b304) )
  :assumption
(or (not b219)  (not b305) )
  :assumption
(or (not b215)  (not b302) )
  :assumption
(or (not b219)  (not b303) )
  :assumption
(or (not b215)  (not b286) )
  :assumption
(or (not b219)  (not b287) )
  :assumption
(or (not b215)  (not b284) )
  :assumption
(or (not b219)  (not b285) )
  :assumption
(or (not b215)  (not b280) )
  :assumption
(or (not b219)  (not b282) )
  :assumption
(or (not b215)  (not b257) )
  :assumption
(or (not b219)  (not b258) )
  :assumption
(or (not b215)  (not b255) )
  :assumption
(or (not b219)  (not b256) )
  :assumption
(or (not b215)  (not b251) )
  :assumption
(or (not b219)  (not b253) )
  :assumption
(or (not b219)  (not b229) )
  :assumption
(or (not b215)  (not b227) )
  :assumption
(or (not b219)  (not b228) )
  :assumption
(or (not b219)  (not b331) )
  :assumption
(or (not b219)  (not b328) )
  :assumption
(or (not b219)  (not b327) )
  :assumption
(or (not b219)  (not b314) )
  :assumption
(or (not b219)  (not b313) )
  :assumption
(or (not b219)  (not b312) )
  :assumption
(or (not b222)  (not b701) )
  :assumption
(or (not b225)  (not b704) )
  :assumption
(or (not b227)  (not b707) )
  :assumption
(or (not b228)  (not b710) )
  :assumption
(or (not b225)  (not b670) )
  :assumption
(or (not b227)  (not b673) )
  :assumption
(or (not b228)  (not b676) )
  :assumption
(or (not b225)  (not b301) )
  :assumption
(or (not b227)  (not b302) )
  :assumption
(or (not b228)  (not b303) )
  :assumption
(or (not b225)  (not b294) )
  :assumption
(or (not b227)  (not b295) )
  :assumption
(or (not b228)  (not b296) )
  :assumption
(or (not b227)  (not b565) )
  :assumption
(or (not b228)  (not b568) )
  :assumption
(or (not b227)  (not b550) )
  :assumption
(or (not b228)  (not b553) )
  :assumption
(or (not b225)  (not b526) )
  :assumption
(or (not b227)  (not b529) )
  :assumption
(or (not b228)  (not b532) )
  :assumption
(or (not b225)  (not b502) )
  :assumption
(or (not b227)  (not b505) )
  :assumption
(or (not b228)  (not b508) )
  :assumption
(or (not b227)  (not b481) )
  :assumption
(or (not b228)  (not b484) )
  :assumption
(or (not b227)  (not b458) )
  :assumption
(or (not b228)  (not b461) )
  :assumption
(or (not b227)  (not b304) )
  :assumption
(or (not b228)  (not b305) )
  :assumption
(or (not b227)  (not b299) )
  :assumption
(or (not b228)  (not b300) )
  :assumption
(or (not b227)  (not b286) )
  :assumption
(or (not b228)  (not b287) )
  :assumption
(or (not b227)  (not b284) )
  :assumption
(or (not b228)  (not b285) )
  :assumption
(or (not b227)  (not b280) )
  :assumption
(or (not b228)  (not b282) )
  :assumption
(or (not b227)  (not b257) )
  :assumption
(or (not b228)  (not b258) )
  :assumption
(or (not b227)  (not b255) )
  :assumption
(or (not b228)  (not b256) )
  :assumption
(or (not b227)  (not b251) )
  :assumption
(or (not b228)  (not b253) )
  :assumption
(or (not b228)  (not b229) )
  :assumption
(or (not b228)  (not b331) )
  :assumption
(or (not b228)  (not b328) )
  :assumption
(or (not b228)  (not b327) )
  :assumption
(or (not b228)  (not b314) )
  :assumption
(or (not b228)  (not b313) )
  :assumption
(or (not b228)  (not b312) )
  :assumption
(or (not b229)  (not b716) )
  :assumption
(or (not b229)  (not b230) )
  :assumption
(or (not b229)  (not b646) )
  :assumption
(or (not b229)  (not b305) )
  :assumption
(or (not b229)  (not b298) )
  :assumption
(or (not b229)  (not b568) )
  :assumption
(or (not b229)  (not b553) )
  :assumption
(or (not b229)  (not b532) )
  :assumption
(or (not b229)  (not b508) )
  :assumption
(or (not b229)  (not b484) )
  :assumption
(or (not b229)  (not b461) )
  :assumption
(or (not b229)  (not b303) )
  :assumption
(or (not b229)  (not b300) )
  :assumption
(or (not b229)  (not b287) )
  :assumption
(or (not b229)  (not b285) )
  :assumption
(or (not b229)  (not b282) )
  :assumption
(or (not b229)  (not b258) )
  :assumption
(or (not b229)  (not b256) )
  :assumption
(or (not b229)  (not b253) )
  :assumption
(or (not b229)  (not b331) )
  :assumption
(or (not b229)  (not b328) )
  :assumption
(or (not b229)  (not b327) )
  :assumption
(or (not b229)  (not b314) )
  :assumption
(or (not b229)  (not b313) )
  :assumption
(or (not b229)  (not b312) )
  :assumption
(or (not b230)  (not b716) )
  :assumption
(or (not b230)  (not b646) )
  :assumption
(or (not b230)  (not b305) )
  :assumption
(or (not b230)  (not b298) )
  :assumption
(or (not b230)  (not b290) )
  :assumption
(or (not b230)  (not b261) )
  :assumption
(or (not b230)  (not b334) )
  :assumption
(or (not b230)  (not b318) )
  :assumption
(or (not b234)  (not b804) )
  :assumption
(or (not b238)  (not b807) )
  :assumption
(or (not b234)  (not b789) )
  :assumption
(or (not b238)  (not b792) )
  :assumption
(or (not b234)  (not b251) )
  :assumption
(or (not b238)  (not b253) )
  :assumption
(or (not b234)  (not b757) )
  :assumption
(or (not b238)  (not b761) )
  :assumption
(or (not b234)  (not b727) )
  :assumption
(or (not b238)  (not b731) )
  :assumption
(or (not b238)  (not b312) )
  :assumption
(or (not b238)  (not b306) )
  :assumption
(or (not b238)  (not b446) )
  :assumption
(or (not b238)  (not b425) )
  :assumption
(or (not b238)  (not b404) )
  :assumption
(or (not b238)  (not b380) )
  :assumption
(or (not b238)  (not b360) )
  :assumption
(or (not b238)  (not b344) )
  :assumption
(or (not b238)  (not b308) )
  :assumption
(or (not b238)  (not b307) )
  :assumption
(or (not b234)  (not b275) )
  :assumption
(or (not b238)  (not b278) )
  :assumption
(or (not b234)  (not b270) )
  :assumption
(or (not b238)  (not b273) )
  :assumption
(or (not b234)  (not b263) )
  :assumption
(or (not b238)  (not b267) )
  :assumption
(or (not b234)  (not b246) )
  :assumption
(or (not b238)  (not b249) )
  :assumption
(or (not b234)  (not b241) )
  :assumption
(or (not b238)  (not b244) )
  :assumption
(or (not b238)  (not b326) )
  :assumption
(or (not b238)  (not b323) )
  :assumption
(or (not b238)  (not b322) )
  :assumption
(or (not b234)  (not b297) )
  :assumption
(or (not b238)  (not b298) )
  :assumption
(or (not b234)  (not b295) )
  :assumption
(or (not b238)  (not b296) )
  :assumption
(or (not b234)  (not b292) )
  :assumption
(or (not b238)  (not b293) )
  :assumption
(or (not b241)  (not b813) )
  :assumption
(or (not b244)  (not b816) )
  :assumption
(or (not b241)  (not b255) )
  :assumption
(or (not b244)  (not b256) )
  :assumption
(or (not b241)  (not b772) )
  :assumption
(or (not b244)  (not b775) )
  :assumption
(or (not b244)  (not b313) )
  :assumption
(or (not b244)  (not b307) )
  :assumption
(or (not b244)  (not b446) )
  :assumption
(or (not b244)  (not b425) )
  :assumption
(or (not b244)  (not b404) )
  :assumption
(or (not b244)  (not b380) )
  :assumption
(or (not b244)  (not b360) )
  :assumption
(or (not b244)  (not b344) )
  :assumption
(or (not b244)  (not b308) )
  :assumption
(or (not b244)  (not b306) )
  :assumption
(or (not b241)  (not b275) )
  :assumption
(or (not b244)  (not b278) )
  :assumption
(or (not b241)  (not b270) )
  :assumption
(or (not b244)  (not b273) )
  :assumption
(or (not b241)  (not b263) )
  :assumption
(or (not b244)  (not b267) )
  :assumption
(or (not b241)  (not b246) )
  :assumption
(or (not b244)  (not b249) )
  :assumption
(or (not b244)  (not b326) )
  :assumption
(or (not b244)  (not b323) )
  :assumption
(or (not b244)  (not b322) )
  :assumption
(or (not b241)  (not b297) )
  :assumption
(or (not b244)  (not b298) )
  :assumption
(or (not b241)  (not b295) )
  :assumption
(or (not b244)  (not b296) )
  :assumption
(or (not b241)  (not b292) )
  :assumption
(or (not b244)  (not b293) )
  :assumption
(or (not b246)  (not b822) )
  :assumption
(or (not b249)  (not b825) )
  :assumption
(or (not b246)  (not b259) )
  :assumption
(or (not b249)  (not b261) )
  :assumption
(or (not b246)  (not b257) )
  :assumption
(or (not b249)  (not b258) )
  :assumption
(or (not b246)  (not b743) )
  :assumption
(or (not b249)  (not b746) )
  :assumption
(or (not b249)  (not b318) )
  :assumption
(or (not b249)  (not b314) )
  :assumption
(or (not b249)  (not b308) )
  :assumption
(or (not b249)  (not b446) )
  :assumption
(or (not b249)  (not b425) )
  :assumption
(or (not b249)  (not b404) )
  :assumption
(or (not b249)  (not b380) )
  :assumption
(or (not b249)  (not b360) )
  :assumption
(or (not b249)  (not b344) )
  :assumption
(or (not b249)  (not b307) )
  :assumption
(or (not b249)  (not b306) )
  :assumption
(or (not b246)  (not b275) )
  :assumption
(or (not b249)  (not b278) )
  :assumption
(or (not b246)  (not b270) )
  :assumption
(or (not b249)  (not b273) )
  :assumption
(or (not b246)  (not b263) )
  :assumption
(or (not b249)  (not b267) )
  :assumption
(or (not b249)  (not b326) )
  :assumption
(or (not b249)  (not b323) )
  :assumption
(or (not b249)  (not b322) )
  :assumption
(or (not b246)  (not b297) )
  :assumption
(or (not b249)  (not b298) )
  :assumption
(or (not b246)  (not b295) )
  :assumption
(or (not b249)  (not b296) )
  :assumption
(or (not b246)  (not b292) )
  :assumption
(or (not b249)  (not b293) )
  :assumption
(or (not b251)  (not b804) )
  :assumption
(or (not b253)  (not b807) )
  :assumption
(or (not b251)  (not b789) )
  :assumption
(or (not b253)  (not b792) )
  :assumption
(or (not b251)  (not b757) )
  :assumption
(or (not b253)  (not b761) )
  :assumption
(or (not b251)  (not b727) )
  :assumption
(or (not b253)  (not b731) )
  :assumption
(or (not b253)  (not b312) )
  :assumption
(or (not b253)  (not b306) )
  :assumption
(or (not b253)  (not b572) )
  :assumption
(or (not b253)  (not b557) )
  :assumption
(or (not b253)  (not b538) )
  :assumption
(or (not b253)  (not b514) )
  :assumption
(or (not b253)  (not b490) )
  :assumption
(or (not b253)  (not b469) )
  :assumption
(or (not b253)  (not b314) )
  :assumption
(or (not b253)  (not b313) )
  :assumption
(or (not b251)  (not b286) )
  :assumption
(or (not b253)  (not b287) )
  :assumption
(or (not b251)  (not b284) )
  :assumption
(or (not b253)  (not b285) )
  :assumption
(or (not b251)  (not b280) )
  :assumption
(or (not b253)  (not b282) )
  :assumption
(or (not b251)  (not b257) )
  :assumption
(or (not b253)  (not b258) )
  :assumption
(or (not b251)  (not b255) )
  :assumption
(or (not b253)  (not b256) )
  :assumption
(or (not b253)  (not b331) )
  :assumption
(or (not b253)  (not b328) )
  :assumption
(or (not b253)  (not b327) )
  :assumption
(or (not b251)  (not b304) )
  :assumption
(or (not b253)  (not b305) )
  :assumption
(or (not b251)  (not b302) )
  :assumption
(or (not b253)  (not b303) )
  :assumption
(or (not b251)  (not b299) )
  :assumption
(or (not b253)  (not b300) )
  :assumption
(or (not b255)  (not b813) )
  :assumption
(or (not b256)  (not b816) )
  :assumption
(or (not b255)  (not b772) )
  :assumption
(or (not b256)  (not b775) )
  :assumption
(or (not b256)  (not b313) )
  :assumption
(or (not b256)  (not b307) )
  :assumption
(or (not b256)  (not b572) )
  :assumption
(or (not b256)  (not b557) )
  :assumption
(or (not b256)  (not b538) )
  :assumption
(or (not b256)  (not b514) )
  :assumption
(or (not b256)  (not b490) )
  :assumption
(or (not b256)  (not b469) )
  :assumption
(or (not b256)  (not b314) )
  :assumption
(or (not b256)  (not b312) )
  :assumption
(or (not b255)  (not b286) )
  :assumption
(or (not b256)  (not b287) )
  :assumption
(or (not b255)  (not b284) )
  :assumption
(or (not b256)  (not b285) )
  :assumption
(or (not b255)  (not b280) )
  :assumption
(or (not b256)  (not b282) )
  :assumption
(or (not b255)  (not b257) )
  :assumption
(or (not b256)  (not b258) )
  :assumption
(or (not b256)  (not b331) )
  :assumption
(or (not b256)  (not b328) )
  :assumption
(or (not b256)  (not b327) )
  :assumption
(or (not b255)  (not b304) )
  :assumption
(or (not b256)  (not b305) )
  :assumption
(or (not b255)  (not b302) )
  :assumption
(or (not b256)  (not b303) )
  :assumption
(or (not b255)  (not b299) )
  :assumption
(or (not b256)  (not b300) )
  :assumption
(or (not b257)  (not b822) )
  :assumption
(or (not b258)  (not b825) )
  :assumption
(or (not b257)  (not b259) )
  :assumption
(or (not b258)  (not b261) )
  :assumption
(or (not b257)  (not b743) )
  :assumption
(or (not b258)  (not b746) )
  :assumption
(or (not b258)  (not b318) )
  :assumption
(or (not b258)  (not b314) )
  :assumption
(or (not b258)  (not b308) )
  :assumption
(or (not b258)  (not b572) )
  :assumption
(or (not b258)  (not b557) )
  :assumption
(or (not b258)  (not b538) )
  :assumption
(or (not b258)  (not b514) )
  :assumption
(or (not b258)  (not b490) )
  :assumption
(or (not b258)  (not b469) )
  :assumption
(or (not b258)  (not b313) )
  :assumption
(or (not b258)  (not b312) )
  :assumption
(or (not b257)  (not b286) )
  :assumption
(or (not b258)  (not b287) )
  :assumption
(or (not b257)  (not b284) )
  :assumption
(or (not b258)  (not b285) )
  :assumption
(or (not b257)  (not b280) )
  :assumption
(or (not b258)  (not b282) )
  :assumption
(or (not b258)  (not b331) )
  :assumption
(or (not b258)  (not b328) )
  :assumption
(or (not b258)  (not b327) )
  :assumption
(or (not b257)  (not b304) )
  :assumption
(or (not b258)  (not b305) )
  :assumption
(or (not b257)  (not b302) )
  :assumption
(or (not b258)  (not b303) )
  :assumption
(or (not b257)  (not b299) )
  :assumption
(or (not b258)  (not b300) )
  :assumption
(or (not b259)  (not b822) )
  :assumption
(or (not b261)  (not b825) )
  :assumption
(or (not b259)  (not b743) )
  :assumption
(or (not b261)  (not b746) )
  :assumption
(or (not b261)  (not b318) )
  :assumption
(or (not b261)  (not b314) )
  :assumption
(or (not b261)  (not b308) )
  :assumption
(or (not b261)  (not b628) )
  :assumption
(or (not b261)  (not b619) )
  :assumption
(or (not b259)  (not b288) )
  :assumption
(or (not b261)  (not b290) )
  :assumption
(or (not b261)  (not b334) )
  :assumption
(or (not b263)  (not b911) )
  :assumption
(or (not b267)  (not b914) )
  :assumption
(or (not b263)  (not b896) )
  :assumption
(or (not b267)  (not b899) )
  :assumption
(or (not b263)  (not b280) )
  :assumption
(or (not b267)  (not b282) )
  :assumption
(or (not b263)  (not b865) )
  :assumption
(or (not b267)  (not b869) )
  :assumption
(or (not b263)  (not b834) )
  :assumption
(or (not b267)  (not b838) )
  :assumption
(or (not b267)  (not b327) )
  :assumption
(or (not b267)  (not b322) )
  :assumption
(or (not b267)  (not b452) )
  :assumption
(or (not b267)  (not b431) )
  :assumption
(or (not b267)  (not b410) )
  :assumption
(or (not b267)  (not b386) )
  :assumption
(or (not b267)  (not b364) )
  :assumption
(or (not b267)  (not b348) )
  :assumption
(or (not b267)  (not b326) )
  :assumption
(or (not b267)  (not b323) )
  :assumption
(or (not b263)  (not b275) )
  :assumption
(or (not b267)  (not b278) )
  :assumption
(or (not b263)  (not b270) )
  :assumption
(or (not b267)  (not b273) )
  :assumption
(or (not b267)  (not b308) )
  :assumption
(or (not b267)  (not b307) )
  :assumption
(or (not b267)  (not b306) )
  :assumption
(or (not b263)  (not b297) )
  :assumption
(or (not b267)  (not b298) )
  :assumption
(or (not b263)  (not b295) )
  :assumption
(or (not b267)  (not b296) )
  :assumption
(or (not b263)  (not b292) )
  :assumption
(or (not b267)  (not b293) )
  :assumption
(or (not b270)  (not b920) )
  :assumption
(or (not b273)  (not b923) )
  :assumption
(or (not b270)  (not b284) )
  :assumption
(or (not b273)  (not b285) )
  :assumption
(or (not b270)  (not b880) )
  :assumption
(or (not b273)  (not b883) )
  :assumption
(or (not b273)  (not b328) )
  :assumption
(or (not b273)  (not b323) )
  :assumption
(or (not b273)  (not b452) )
  :assumption
(or (not b273)  (not b431) )
  :assumption
(or (not b273)  (not b410) )
  :assumption
(or (not b273)  (not b386) )
  :assumption
(or (not b273)  (not b364) )
  :assumption
(or (not b273)  (not b348) )
  :assumption
(or (not b273)  (not b326) )
  :assumption
(or (not b273)  (not b322) )
  :assumption
(or (not b270)  (not b275) )
  :assumption
(or (not b273)  (not b278) )
  :assumption
(or (not b273)  (not b308) )
  :assumption
(or (not b273)  (not b307) )
  :assumption
(or (not b273)  (not b306) )
  :assumption
(or (not b270)  (not b297) )
  :assumption
(or (not b273)  (not b298) )
  :assumption
(or (not b270)  (not b295) )
  :assumption
(or (not b273)  (not b296) )
  :assumption
(or (not b270)  (not b292) )
  :assumption
(or (not b273)  (not b293) )
  :assumption
(or (not b275)  (not b927) )
  :assumption
(or (not b278)  (not b930) )
  :assumption
(or (not b275)  (not b288) )
  :assumption
(or (not b278)  (not b290) )
  :assumption
(or (not b275)  (not b286) )
  :assumption
(or (not b278)  (not b287) )
  :assumption
(or (not b275)  (not b850) )
  :assumption
(or (not b278)  (not b853) )
  :assumption
(or (not b278)  (not b334) )
  :assumption
(or (not b278)  (not b331) )
  :assumption
(or (not b278)  (not b326) )
  :assumption
(or (not b278)  (not b452) )
  :assumption
(or (not b278)  (not b431) )
  :assumption
(or (not b278)  (not b410) )
  :assumption
(or (not b278)  (not b386) )
  :assumption
(or (not b278)  (not b364) )
  :assumption
(or (not b278)  (not b348) )
  :assumption
(or (not b278)  (not b323) )
  :assumption
(or (not b278)  (not b322) )
  :assumption
(or (not b278)  (not b308) )
  :assumption
(or (not b278)  (not b307) )
  :assumption
(or (not b278)  (not b306) )
  :assumption
(or (not b275)  (not b297) )
  :assumption
(or (not b278)  (not b298) )
  :assumption
(or (not b275)  (not b295) )
  :assumption
(or (not b278)  (not b296) )
  :assumption
(or (not b275)  (not b292) )
  :assumption
(or (not b278)  (not b293) )
  :assumption
(or (not b280)  (not b911) )
  :assumption
(or (not b282)  (not b914) )
  :assumption
(or (not b280)  (not b896) )
  :assumption
(or (not b282)  (not b899) )
  :assumption
(or (not b280)  (not b865) )
  :assumption
(or (not b282)  (not b869) )
  :assumption
(or (not b280)  (not b834) )
  :assumption
(or (not b282)  (not b838) )
  :assumption
(or (not b282)  (not b327) )
  :assumption
(or (not b282)  (not b322) )
  :assumption
(or (not b282)  (not b576) )
  :assumption
(or (not b282)  (not b561) )
  :assumption
(or (not b282)  (not b544) )
  :assumption
(or (not b282)  (not b520) )
  :assumption
(or (not b282)  (not b496) )
  :assumption
(or (not b282)  (not b475) )
  :assumption
(or (not b282)  (not b331) )
  :assumption
(or (not b282)  (not b328) )
  :assumption
(or (not b280)  (not b286) )
  :assumption
(or (not b282)  (not b287) )
  :assumption
(or (not b280)  (not b284) )
  :assumption
(or (not b282)  (not b285) )
  :assumption
(or (not b282)  (not b314) )
  :assumption
(or (not b282)  (not b313) )
  :assumption
(or (not b282)  (not b312) )
  :assumption
(or (not b280)  (not b304) )
  :assumption
(or (not b282)  (not b305) )
  :assumption
(or (not b280)  (not b302) )
  :assumption
(or (not b282)  (not b303) )
  :assumption
(or (not b280)  (not b299) )
  :assumption
(or (not b282)  (not b300) )
  :assumption
(or (not b284)  (not b920) )
  :assumption
(or (not b285)  (not b923) )
  :assumption
(or (not b284)  (not b880) )
  :assumption
(or (not b285)  (not b883) )
  :assumption
(or (not b285)  (not b328) )
  :assumption
(or (not b285)  (not b323) )
  :assumption
(or (not b285)  (not b576) )
  :assumption
(or (not b285)  (not b561) )
  :assumption
(or (not b285)  (not b544) )
  :assumption
(or (not b285)  (not b520) )
  :assumption
(or (not b285)  (not b496) )
  :assumption
(or (not b285)  (not b475) )
  :assumption
(or (not b285)  (not b331) )
  :assumption
(or (not b285)  (not b327) )
  :assumption
(or (not b284)  (not b286) )
  :assumption
(or (not b285)  (not b287) )
  :assumption
(or (not b285)  (not b314) )
  :assumption
(or (not b285)  (not b313) )
  :assumption
(or (not b285)  (not b312) )
  :assumption
(or (not b284)  (not b304) )
  :assumption
(or (not b285)  (not b305) )
  :assumption
(or (not b284)  (not b302) )
  :assumption
(or (not b285)  (not b303) )
  :assumption
(or (not b284)  (not b299) )
  :assumption
(or (not b285)  (not b300) )
  :assumption
(or (not b286)  (not b927) )
  :assumption
(or (not b287)  (not b930) )
  :assumption
(or (not b286)  (not b288) )
  :assumption
(or (not b287)  (not b290) )
  :assumption
(or (not b286)  (not b850) )
  :assumption
(or (not b287)  (not b853) )
  :assumption
(or (not b287)  (not b334) )
  :assumption
(or (not b287)  (not b331) )
  :assumption
(or (not b287)  (not b326) )
  :assumption
(or (not b287)  (not b576) )
  :assumption
(or (not b287)  (not b561) )
  :assumption
(or (not b287)  (not b544) )
  :assumption
(or (not b287)  (not b520) )
  :assumption
(or (not b287)  (not b496) )
  :assumption
(or (not b287)  (not b475) )
  :assumption
(or (not b287)  (not b328) )
  :assumption
(or (not b287)  (not b327) )
  :assumption
(or (not b287)  (not b314) )
  :assumption
(or (not b287)  (not b313) )
  :assumption
(or (not b287)  (not b312) )
  :assumption
(or (not b286)  (not b304) )
  :assumption
(or (not b287)  (not b305) )
  :assumption
(or (not b286)  (not b302) )
  :assumption
(or (not b287)  (not b303) )
  :assumption
(or (not b286)  (not b299) )
  :assumption
(or (not b287)  (not b300) )
  :assumption
(or (not b288)  (not b927) )
  :assumption
(or (not b290)  (not b930) )
  :assumption
(or (not b288)  (not b850) )
  :assumption
(or (not b290)  (not b853) )
  :assumption
(or (not b290)  (not b334) )
  :assumption
(or (not b290)  (not b331) )
  :assumption
(or (not b290)  (not b326) )
  :assumption
(or (not b290)  (not b632) )
  :assumption
(or (not b290)  (not b623) )
  :assumption
(or (not b290)  (not b318) )
  :assumption
(or (not b292)  (not b437) )
  :assumption
(or (not b293)  (not b440) )
  :assumption
(or (not b292)  (not b416) )
  :assumption
(or (not b293)  (not b419) )
  :assumption
(or (not b292)  (not b395) )
  :assumption
(or (not b293)  (not b398) )
  :assumption
(or (not b292)  (not b371) )
  :assumption
(or (not b293)  (not b374) )
  :assumption
(or (not b292)  (not b352) )
  :assumption
(or (not b293)  (not b355) )
  :assumption
(or (not b292)  (not b336) )
  :assumption
(or (not b293)  (not b339) )
  :assumption
(or (not b292)  (not b297) )
  :assumption
(or (not b293)  (not b298) )
  :assumption
(or (not b292)  (not b295) )
  :assumption
(or (not b293)  (not b296) )
  :assumption
(or (not b292)  (not b692) )
  :assumption
(or (not b293)  (not b695) )
  :assumption
(or (not b292)  (not b683) )
  :assumption
(or (not b293)  (not b686) )
  :assumption
(or (not b295)  (not b437) )
  :assumption
(or (not b296)  (not b440) )
  :assumption
(or (not b295)  (not b416) )
  :assumption
(or (not b296)  (not b419) )
  :assumption
(or (not b294)  (not b392) )
  :assumption
(or (not b295)  (not b395) )
  :assumption
(or (not b296)  (not b398) )
  :assumption
(or (not b294)  (not b368) )
  :assumption
(or (not b295)  (not b371) )
  :assumption
(or (not b296)  (not b374) )
  :assumption
(or (not b295)  (not b352) )
  :assumption
(or (not b296)  (not b355) )
  :assumption
(or (not b295)  (not b336) )
  :assumption
(or (not b296)  (not b339) )
  :assumption
(or (not b295)  (not b297) )
  :assumption
(or (not b296)  (not b298) )
  :assumption
(or (not b294)  (not b704) )
  :assumption
(or (not b295)  (not b707) )
  :assumption
(or (not b296)  (not b710) )
  :assumption
(or (not b297)  (not b437) )
  :assumption
(or (not b298)  (not b440) )
  :assumption
(or (not b297)  (not b416) )
  :assumption
(or (not b298)  (not b419) )
  :assumption
(or (not b297)  (not b395) )
  :assumption
(or (not b298)  (not b398) )
  :assumption
(or (not b297)  (not b371) )
  :assumption
(or (not b298)  (not b374) )
  :assumption
(or (not b297)  (not b352) )
  :assumption
(or (not b298)  (not b355) )
  :assumption
(or (not b297)  (not b336) )
  :assumption
(or (not b298)  (not b339) )
  :assumption
(or (not b298)  (not b716) )
  :assumption
(or (not b299)  (not b565) )
  :assumption
(or (not b300)  (not b568) )
  :assumption
(or (not b299)  (not b550) )
  :assumption
(or (not b300)  (not b553) )
  :assumption
(or (not b299)  (not b529) )
  :assumption
(or (not b300)  (not b532) )
  :assumption
(or (not b299)  (not b505) )
  :assumption
(or (not b300)  (not b508) )
  :assumption
(or (not b299)  (not b481) )
  :assumption
(or (not b300)  (not b484) )
  :assumption
(or (not b299)  (not b458) )
  :assumption
(or (not b300)  (not b461) )
  :assumption
(or (not b299)  (not b304) )
  :assumption
(or (not b300)  (not b305) )
  :assumption
(or (not b299)  (not b302) )
  :assumption
(or (not b300)  (not b303) )
  :assumption
(or (not b299)  (not b692) )
  :assumption
(or (not b300)  (not b695) )
  :assumption
(or (not b299)  (not b683) )
  :assumption
(or (not b300)  (not b686) )
  :assumption
(or (not b302)  (not b565) )
  :assumption
(or (not b303)  (not b568) )
  :assumption
(or (not b302)  (not b550) )
  :assumption
(or (not b303)  (not b553) )
  :assumption
(or (not b301)  (not b526) )
  :assumption
(or (not b302)  (not b529) )
  :assumption
(or (not b303)  (not b532) )
  :assumption
(or (not b301)  (not b502) )
  :assumption
(or (not b302)  (not b505) )
  :assumption
(or (not b303)  (not b508) )
  :assumption
(or (not b302)  (not b481) )
  :assumption
(or (not b303)  (not b484) )
  :assumption
(or (not b302)  (not b458) )
  :assumption
(or (not b303)  (not b461) )
  :assumption
(or (not b302)  (not b304) )
  :assumption
(or (not b303)  (not b305) )
  :assumption
(or (not b301)  (not b704) )
  :assumption
(or (not b302)  (not b707) )
  :assumption
(or (not b303)  (not b710) )
  :assumption
(or (not b304)  (not b565) )
  :assumption
(or (not b305)  (not b568) )
  :assumption
(or (not b304)  (not b550) )
  :assumption
(or (not b305)  (not b553) )
  :assumption
(or (not b304)  (not b529) )
  :assumption
(or (not b305)  (not b532) )
  :assumption
(or (not b304)  (not b505) )
  :assumption
(or (not b305)  (not b508) )
  :assumption
(or (not b304)  (not b481) )
  :assumption
(or (not b305)  (not b484) )
  :assumption
(or (not b304)  (not b458) )
  :assumption
(or (not b305)  (not b461) )
  :assumption
(or (not b305)  (not b716) )
  :assumption
(or (not b306)  (not b446) )
  :assumption
(or (not b306)  (not b425) )
  :assumption
(or (not b306)  (not b404) )
  :assumption
(or (not b306)  (not b380) )
  :assumption
(or (not b306)  (not b360) )
  :assumption
(or (not b306)  (not b344) )
  :assumption
(or (not b306)  (not b308) )
  :assumption
(or (not b306)  (not b307) )
  :assumption
(or (not b306)  (not b807) )
  :assumption
(or (not b306)  (not b792) )
  :assumption
(or (not b307)  (not b446) )
  :assumption
(or (not b307)  (not b425) )
  :assumption
(or (not b307)  (not b404) )
  :assumption
(or (not b307)  (not b380) )
  :assumption
(or (not b307)  (not b360) )
  :assumption
(or (not b307)  (not b344) )
  :assumption
(or (not b307)  (not b308) )
  :assumption
(or (not b307)  (not b816) )
  :assumption
(or (not b308)  (not b446) )
  :assumption
(or (not b309)  (not b449) )
  :assumption
(or (not b308)  (not b425) )
  :assumption
(or (not b309)  (not b428) )
  :assumption
(or (not b308)  (not b404) )
  :assumption
(or (not b309)  (not b407) )
  :assumption
(or (not b308)  (not b380) )
  :assumption
(or (not b309)  (not b383) )
  :assumption
(or (not b308)  (not b360) )
  :assumption
(or (not b308)  (not b344) )
  :assumption
(or (not b308)  (not b825) )
  :assumption
(or (not b312)  (not b572) )
  :assumption
(or (not b312)  (not b557) )
  :assumption
(or (not b312)  (not b538) )
  :assumption
(or (not b312)  (not b514) )
  :assumption
(or (not b312)  (not b490) )
  :assumption
(or (not b312)  (not b469) )
  :assumption
(or (not b312)  (not b314) )
  :assumption
(or (not b312)  (not b313) )
  :assumption
(or (not b312)  (not b807) )
  :assumption
(or (not b312)  (not b792) )
  :assumption
(or (not b313)  (not b572) )
  :assumption
(or (not b313)  (not b557) )
  :assumption
(or (not b313)  (not b538) )
  :assumption
(or (not b313)  (not b514) )
  :assumption
(or (not b313)  (not b490) )
  :assumption
(or (not b313)  (not b469) )
  :assumption
(or (not b313)  (not b314) )
  :assumption
(or (not b313)  (not b816) )
  :assumption
(or (not b314)  (not b572) )
  :assumption
(or (not b314)  (not b557) )
  :assumption
(or (not b314)  (not b538) )
  :assumption
(or (not b315)  (not b541) )
  :assumption
(or (not b314)  (not b514) )
  :assumption
(or (not b315)  (not b517) )
  :assumption
(or (not b314)  (not b490) )
  :assumption
(or (not b315)  (not b493) )
  :assumption
(or (not b314)  (not b469) )
  :assumption
(or (not b315)  (not b472) )
  :assumption
(or (not b314)  (not b825) )
  :assumption
(or (not b318)  (not b628) )
  :assumption
(or (not b318)  (not b619) )
  :assumption
(or (not b319)  (not b612) )
  :assumption
(or (not b319)  (not b603) )
  :assumption
(or (not b319)  (not b594) )
  :assumption
(or (not b319)  (not b585) )
  :assumption
(or (not b318)  (not b825) )
  :assumption
(or (not b322)  (not b452) )
  :assumption
(or (not b322)  (not b431) )
  :assumption
(or (not b322)  (not b410) )
  :assumption
(or (not b322)  (not b386) )
  :assumption
(or (not b322)  (not b364) )
  :assumption
(or (not b322)  (not b348) )
  :assumption
(or (not b322)  (not b326) )
  :assumption
(or (not b322)  (not b323) )
  :assumption
(or (not b322)  (not b914) )
  :assumption
(or (not b322)  (not b899) )
  :assumption
(or (not b323)  (not b452) )
  :assumption
(or (not b324)  (not b455) )
  :assumption
(or (not b323)  (not b431) )
  :assumption
(or (not b324)  (not b434) )
  :assumption
(or (not b323)  (not b410) )
  :assumption
(or (not b324)  (not b413) )
  :assumption
(or (not b323)  (not b386) )
  :assumption
(or (not b324)  (not b389) )
  :assumption
(or (not b323)  (not b364) )
  :assumption
(or (not b323)  (not b348) )
  :assumption
(or (not b323)  (not b326) )
  :assumption
(or (not b323)  (not b923) )
  :assumption
(or (not b326)  (not b452) )
  :assumption
(or (not b326)  (not b431) )
  :assumption
(or (not b326)  (not b410) )
  :assumption
(or (not b326)  (not b386) )
  :assumption
(or (not b326)  (not b364) )
  :assumption
(or (not b326)  (not b348) )
  :assumption
(or (not b326)  (not b930) )
  :assumption
(or (not b327)  (not b576) )
  :assumption
(or (not b327)  (not b561) )
  :assumption
(or (not b327)  (not b544) )
  :assumption
(or (not b327)  (not b520) )
  :assumption
(or (not b327)  (not b496) )
  :assumption
(or (not b327)  (not b475) )
  :assumption
(or (not b327)  (not b331) )
  :assumption
(or (not b327)  (not b328) )
  :assumption
(or (not b327)  (not b914) )
  :assumption
(or (not b327)  (not b899) )
  :assumption
(or (not b328)  (not b576) )
  :assumption
(or (not b328)  (not b561) )
  :assumption
(or (not b328)  (not b544) )
  :assumption
(or (not b329)  (not b547) )
  :assumption
(or (not b328)  (not b520) )
  :assumption
(or (not b329)  (not b523) )
  :assumption
(or (not b328)  (not b496) )
  :assumption
(or (not b329)  (not b499) )
  :assumption
(or (not b328)  (not b475) )
  :assumption
(or (not b329)  (not b478) )
  :assumption
(or (not b328)  (not b331) )
  :assumption
(or (not b328)  (not b923) )
  :assumption
(or (not b331)  (not b576) )
  :assumption
(or (not b331)  (not b561) )
  :assumption
(or (not b331)  (not b544) )
  :assumption
(or (not b331)  (not b520) )
  :assumption
(or (not b331)  (not b496) )
  :assumption
(or (not b331)  (not b475) )
  :assumption
(or (not b331)  (not b930) )
  :assumption
(or (not b332)  (not b615) )
  :assumption
(or (not b332)  (not b606) )
  :assumption
(or (not b332)  (not b597) )
  :assumption
(or (not b332)  (not b588) )
  :assumption
(or (not b334)  (not b632) )
  :assumption
(or (not b334)  (not b623) )
  :assumption
(or (not b334)  (not b930) )
  :assumption
(or (not b339)  (not b364) )
  :assumption
(or (not b339)  (not b360) )
  :assumption
(or (not b336)  (not b352) )
  :assumption
(or (not b339)  (not b355) )
  :assumption
(or (not b339)  (not b348) )
  :assumption
(or (not b339)  (not b344) )
  :assumption
(or (not b322)  (not b339) )
  :assumption
(or (not b306)  (not b339) )
  :assumption
(or (not b263)  (not b336) )
  :assumption
(or (not b267)  (not b339) )
  :assumption
(or (not b234)  (not b336) )
  :assumption
(or (not b238)  (not b339) )
  :assumption
(or (not b174)  (not b336) )
  :assumption
(or (not b160)  (not b336) )
  :assumption
(or (not b135)  (not b336) )
  :assumption
(or (not b112)  (not b336) )
  :assumption
(or (not b91)  (not b339) )
  :assumption
(or (not b70)  (not b339) )
  :assumption
(or (not b38)  (not b339) )
  :assumption
(or (not b11)  (not b339) )
  :assumption
(or (not b339)  (not b431) )
  :assumption
(or (not b339)  (not b425) )
  :assumption
(or (not b336)  (not b416) )
  :assumption
(or (not b339)  (not b419) )
  :assumption
(or (not b339)  (not b386) )
  :assumption
(or (not b339)  (not b380) )
  :assumption
(or (not b336)  (not b371) )
  :assumption
(or (not b339)  (not b374) )
  :assumption
(or (not b339)  (not b410) )
  :assumption
(or (not b339)  (not b404) )
  :assumption
(or (not b336)  (not b395) )
  :assumption
(or (not b339)  (not b398) )
  :assumption
(or (not b323)  (not b339) )
  :assumption
(or (not b307)  (not b339) )
  :assumption
(or (not b270)  (not b336) )
  :assumption
(or (not b273)  (not b339) )
  :assumption
(or (not b241)  (not b336) )
  :assumption
(or (not b244)  (not b339) )
  :assumption
(or (not b179)  (not b336) )
  :assumption
(or (not b162)  (not b336) )
  :assumption
(or (not b137)  (not b336) )
  :assumption
(or (not b115)  (not b336) )
  :assumption
(or (not b98)  (not b339) )
  :assumption
(or (not b77)  (not b339) )
  :assumption
(or (not b45)  (not b339) )
  :assumption
(or (not b19)  (not b339) )
  :assumption
(or (not b344)  (not b364) )
  :assumption
(or (not b344)  (not b360) )
  :assumption
(or (not b344)  (not b355) )
  :assumption
(or (not b344)  (not b348) )
  :assumption
(or (not b322)  (not b344) )
  :assumption
(or (not b293)  (not b344) )
  :assumption
(or (not b267)  (not b344) )
  :assumption
(or (not b197)  (not b344) )
  :assumption
(or (not b91)  (not b344) )
  :assumption
(or (not b70)  (not b344) )
  :assumption
(or (not b38)  (not b344) )
  :assumption
(or (not b11)  (not b344) )
  :assumption
(or (not b344)  (not b431) )
  :assumption
(or (not b344)  (not b425) )
  :assumption
(or (not b344)  (not b419) )
  :assumption
(or (not b344)  (not b386) )
  :assumption
(or (not b344)  (not b380) )
  :assumption
(or (not b344)  (not b374) )
  :assumption
(or (not b344)  (not b410) )
  :assumption
(or (not b344)  (not b404) )
  :assumption
(or (not b344)  (not b398) )
  :assumption
(or (not b323)  (not b344) )
  :assumption
(or (not b296)  (not b344) )
  :assumption
(or (not b273)  (not b344) )
  :assumption
(or (not b210)  (not b344) )
  :assumption
(or (not b98)  (not b344) )
  :assumption
(or (not b77)  (not b344) )
  :assumption
(or (not b45)  (not b344) )
  :assumption
(or (not b19)  (not b344) )
  :assumption
(or (not b348)  (not b364) )
  :assumption
(or (not b348)  (not b360) )
  :assumption
(or (not b348)  (not b355) )
  :assumption
(or (not b306)  (not b348) )
  :assumption
(or (not b293)  (not b348) )
  :assumption
(or (not b238)  (not b348) )
  :assumption
(or (not b197)  (not b348) )
  :assumption
(or (not b91)  (not b348) )
  :assumption
(or (not b70)  (not b348) )
  :assumption
(or (not b38)  (not b348) )
  :assumption
(or (not b11)  (not b348) )
  :assumption
(or (not b348)  (not b431) )
  :assumption
(or (not b348)  (not b425) )
  :assumption
(or (not b348)  (not b419) )
  :assumption
(or (not b348)  (not b386) )
  :assumption
(or (not b348)  (not b380) )
  :assumption
(or (not b348)  (not b374) )
  :assumption
(or (not b348)  (not b410) )
  :assumption
(or (not b348)  (not b404) )
  :assumption
(or (not b348)  (not b398) )
  :assumption
(or (not b307)  (not b348) )
  :assumption
(or (not b296)  (not b348) )
  :assumption
(or (not b244)  (not b348) )
  :assumption
(or (not b210)  (not b348) )
  :assumption
(or (not b98)  (not b348) )
  :assumption
(or (not b77)  (not b348) )
  :assumption
(or (not b45)  (not b348) )
  :assumption
(or (not b19)  (not b348) )
  :assumption
(or (not b355)  (not b364) )
  :assumption
(or (not b355)  (not b360) )
  :assumption
(or (not b322)  (not b355) )
  :assumption
(or (not b306)  (not b355) )
  :assumption
(or (not b263)  (not b352) )
  :assumption
(or (not b267)  (not b355) )
  :assumption
(or (not b234)  (not b352) )
  :assumption
(or (not b238)  (not b355) )
  :assumption
(or (not b174)  (not b352) )
  :assumption
(or (not b160)  (not b352) )
  :assumption
(or (not b135)  (not b352) )
  :assumption
(or (not b112)  (not b352) )
  :assumption
(or (not b91)  (not b355) )
  :assumption
(or (not b70)  (not b355) )
  :assumption
(or (not b38)  (not b355) )
  :assumption
(or (not b11)  (not b355) )
  :assumption
(or (not b355)  (not b431) )
  :assumption
(or (not b355)  (not b425) )
  :assumption
(or (not b352)  (not b416) )
  :assumption
(or (not b355)  (not b419) )
  :assumption
(or (not b355)  (not b386) )
  :assumption
(or (not b355)  (not b380) )
  :assumption
(or (not b352)  (not b371) )
  :assumption
(or (not b355)  (not b374) )
  :assumption
(or (not b355)  (not b452) )
  :assumption
(or (not b355)  (not b446) )
  :assumption
(or (not b352)  (not b437) )
  :assumption
(or (not b355)  (not b440) )
  :assumption
(or (not b326)  (not b355) )
  :assumption
(or (not b308)  (not b355) )
  :assumption
(or (not b275)  (not b352) )
  :assumption
(or (not b278)  (not b355) )
  :assumption
(or (not b246)  (not b352) )
  :assumption
(or (not b249)  (not b355) )
  :assumption
(or (not b180)  (not b352) )
  :assumption
(or (not b165)  (not b352) )
  :assumption
(or (not b140)  (not b352) )
  :assumption
(or (not b120)  (not b352) )
  :assumption
(or (not b101)  (not b355) )
  :assumption
(or (not b80)  (not b355) )
  :assumption
(or (not b59)  (not b355) )
  :assumption
(or (not b48)  (not b355) )
  :assumption
(or (not b23)  (not b355) )
  :assumption
(or (not b360)  (not b364) )
  :assumption
(or (not b322)  (not b360) )
  :assumption
(or (not b293)  (not b360) )
  :assumption
(or (not b267)  (not b360) )
  :assumption
(or (not b197)  (not b360) )
  :assumption
(or (not b91)  (not b360) )
  :assumption
(or (not b70)  (not b360) )
  :assumption
(or (not b38)  (not b360) )
  :assumption
(or (not b11)  (not b360) )
  :assumption
(or (not b360)  (not b431) )
  :assumption
(or (not b360)  (not b425) )
  :assumption
(or (not b360)  (not b419) )
  :assumption
(or (not b360)  (not b386) )
  :assumption
(or (not b360)  (not b380) )
  :assumption
(or (not b360)  (not b374) )
  :assumption
(or (not b360)  (not b452) )
  :assumption
(or (not b360)  (not b446) )
  :assumption
(or (not b360)  (not b440) )
  :assumption
(or (not b326)  (not b360) )
  :assumption
(or (not b298)  (not b360) )
  :assumption
(or (not b278)  (not b360) )
  :assumption
(or (not b212)  (not b360) )
  :assumption
(or (not b101)  (not b360) )
  :assumption
(or (not b80)  (not b360) )
  :assumption
(or (not b59)  (not b360) )
  :assumption
(or (not b48)  (not b360) )
  :assumption
(or (not b23)  (not b360) )
  :assumption
(or (not b306)  (not b364) )
  :assumption
(or (not b293)  (not b364) )
  :assumption
(or (not b238)  (not b364) )
  :assumption
(or (not b197)  (not b364) )
  :assumption
(or (not b91)  (not b364) )
  :assumption
(or (not b70)  (not b364) )
  :assumption
(or (not b38)  (not b364) )
  :assumption
(or (not b11)  (not b364) )
  :assumption
(or (not b364)  (not b431) )
  :assumption
(or (not b364)  (not b425) )
  :assumption
(or (not b364)  (not b419) )
  :assumption
(or (not b364)  (not b386) )
  :assumption
(or (not b364)  (not b380) )
  :assumption
(or (not b364)  (not b374) )
  :assumption
(or (not b364)  (not b452) )
  :assumption
(or (not b364)  (not b446) )
  :assumption
(or (not b364)  (not b440) )
  :assumption
(or (not b308)  (not b364) )
  :assumption
(or (not b298)  (not b364) )
  :assumption
(or (not b249)  (not b364) )
  :assumption
(or (not b212)  (not b364) )
  :assumption
(or (not b101)  (not b364) )
  :assumption
(or (not b80)  (not b364) )
  :assumption
(or (not b59)  (not b364) )
  :assumption
(or (not b48)  (not b364) )
  :assumption
(or (not b23)  (not b364) )
  :assumption
(or (not b374)  (not b410) )
  :assumption
(or (not b377)  (not b413) )
  :assumption
(or (not b374)  (not b404) )
  :assumption
(or (not b377)  (not b407) )
  :assumption
(or (not b368)  (not b392) )
  :assumption
(or (not b371)  (not b395) )
  :assumption
(or (not b374)  (not b398) )
  :assumption
(or (not b377)  (not b401) )
  :assumption
(or (not b374)  (not b386) )
  :assumption
(or (not b377)  (not b389) )
  :assumption
(or (not b374)  (not b380) )
  :assumption
(or (not b377)  (not b383) )
  :assumption
(or (not b323)  (not b374) )
  :assumption
(or (not b324)  (not b377) )
  :assumption
(or (not b307)  (not b374) )
  :assumption
(or (not b270)  (not b371) )
  :assumption
(or (not b273)  (not b374) )
  :assumption
(or (not b241)  (not b371) )
  :assumption
(or (not b244)  (not b374) )
  :assumption
(or (not b179)  (not b371) )
  :assumption
(or (not b162)  (not b371) )
  :assumption
(or (not b163)  (not b377) )
  :assumption
(or (not b137)  (not b371) )
  :assumption
(or (not b138)  (not b377) )
  :assumption
(or (not b115)  (not b371) )
  :assumption
(or (not b117)  (not b377) )
  :assumption
(or (not b95)  (not b368) )
  :assumption
(or (not b98)  (not b374) )
  :assumption
(or (not b74)  (not b368) )
  :assumption
(or (not b77)  (not b374) )
  :assumption
(or (not b42)  (not b368) )
  :assumption
(or (not b45)  (not b374) )
  :assumption
(or (not b16)  (not b368) )
  :assumption
(or (not b19)  (not b374) )
  :assumption
(or (not b374)  (not b452) )
  :assumption
(or (not b377)  (not b455) )
  :assumption
(or (not b374)  (not b446) )
  :assumption
(or (not b377)  (not b449) )
  :assumption
(or (not b371)  (not b437) )
  :assumption
(or (not b374)  (not b440) )
  :assumption
(or (not b377)  (not b443) )
  :assumption
(or (not b322)  (not b374) )
  :assumption
(or (not b306)  (not b374) )
  :assumption
(or (not b263)  (not b371) )
  :assumption
(or (not b267)  (not b374) )
  :assumption
(or (not b234)  (not b371) )
  :assumption
(or (not b238)  (not b374) )
  :assumption
(or (not b174)  (not b371) )
  :assumption
(or (not b176)  (not b377) )
  :assumption
(or (not b160)  (not b371) )
  :assumption
(or (not b135)  (not b371) )
  :assumption
(or (not b112)  (not b371) )
  :assumption
(or (not b91)  (not b374) )
  :assumption
(or (not b70)  (not b374) )
  :assumption
(or (not b38)  (not b374) )
  :assumption
(or (not b11)  (not b374) )
  :assumption
(or (not b380)  (not b410) )
  :assumption
(or (not b383)  (not b413) )
  :assumption
(or (not b380)  (not b404) )
  :assumption
(or (not b383)  (not b407) )
  :assumption
(or (not b380)  (not b398) )
  :assumption
(or (not b383)  (not b401) )
  :assumption
(or (not b380)  (not b386) )
  :assumption
(or (not b383)  (not b389) )
  :assumption
(or (not b323)  (not b380) )
  :assumption
(or (not b324)  (not b383) )
  :assumption
(or (not b296)  (not b380) )
  :assumption
(or (not b273)  (not b380) )
  :assumption
(or (not b210)  (not b380) )
  :assumption
(or (not b163)  (not b383) )
  :assumption
(or (not b138)  (not b383) )
  :assumption
(or (not b117)  (not b383) )
  :assumption
(or (not b98)  (not b380) )
  :assumption
(or (not b77)  (not b380) )
  :assumption
(or (not b45)  (not b380) )
  :assumption
(or (not b19)  (not b380) )
  :assumption
(or (not b380)  (not b452) )
  :assumption
(or (not b383)  (not b455) )
  :assumption
(or (not b380)  (not b446) )
  :assumption
(or (not b383)  (not b449) )
  :assumption
(or (not b380)  (not b440) )
  :assumption
(or (not b383)  (not b443) )
  :assumption
(or (not b322)  (not b380) )
  :assumption
(or (not b293)  (not b380) )
  :assumption
(or (not b267)  (not b380) )
  :assumption
(or (not b197)  (not b380) )
  :assumption
(or (not b176)  (not b383) )
  :assumption
(or (not b91)  (not b380) )
  :assumption
(or (not b70)  (not b380) )
  :assumption
(or (not b38)  (not b380) )
  :assumption
(or (not b11)  (not b380) )
  :assumption
(or (not b386)  (not b410) )
  :assumption
(or (not b389)  (not b413) )
  :assumption
(or (not b386)  (not b404) )
  :assumption
(or (not b389)  (not b407) )
  :assumption
(or (not b386)  (not b398) )
  :assumption
(or (not b389)  (not b401) )
  :assumption
(or (not b307)  (not b386) )
  :assumption
(or (not b296)  (not b386) )
  :assumption
(or (not b244)  (not b386) )
  :assumption
(or (not b210)  (not b386) )
  :assumption
(or (not b163)  (not b389) )
  :assumption
(or (not b138)  (not b389) )
  :assumption
(or (not b117)  (not b389) )
  :assumption
(or (not b98)  (not b386) )
  :assumption
(or (not b77)  (not b386) )
  :assumption
(or (not b45)  (not b386) )
  :assumption
(or (not b19)  (not b386) )
  :assumption
(or (not b386)  (not b452) )
  :assumption
(or (not b389)  (not b455) )
  :assumption
(or (not b386)  (not b446) )
  :assumption
(or (not b389)  (not b449) )
  :assumption
(or (not b386)  (not b440) )
  :assumption
(or (not b389)  (not b443) )
  :assumption
(or (not b306)  (not b386) )
  :assumption
(or (not b293)  (not b386) )
  :assumption
(or (not b238)  (not b386) )
  :assumption
(or (not b197)  (not b386) )
  :assumption
(or (not b176)  (not b389) )
  :assumption
(or (not b91)  (not b386) )
  :assumption
(or (not b70)  (not b386) )
  :assumption
(or (not b38)  (not b386) )
  :assumption
(or (not b11)  (not b386) )
  :assumption
(or (not b398)  (not b410) )
  :assumption
(or (not b401)  (not b413) )
  :assumption
(or (not b398)  (not b404) )
  :assumption
(or (not b401)  (not b407) )
  :assumption
(or (not b323)  (not b398) )
  :assumption
(or (not b324)  (not b401) )
  :assumption
(or (not b307)  (not b398) )
  :assumption
(or (not b270)  (not b395) )
  :assumption
(or (not b273)  (not b398) )
  :assumption
(or (not b241)  (not b395) )
  :assumption
(or (not b244)  (not b398) )
  :assumption
(or (not b179)  (not b395) )
  :assumption
(or (not b162)  (not b395) )
  :assumption
(or (not b163)  (not b401) )
  :assumption
(or (not b137)  (not b395) )
  :assumption
(or (not b138)  (not b401) )
  :assumption
(or (not b115)  (not b395) )
  :assumption
(or (not b117)  (not b401) )
  :assumption
(or (not b95)  (not b392) )
  :assumption
(or (not b98)  (not b398) )
  :assumption
(or (not b74)  (not b392) )
  :assumption
(or (not b77)  (not b398) )
  :assumption
(or (not b42)  (not b392) )
  :assumption
(or (not b45)  (not b398) )
  :assumption
(or (not b16)  (not b392) )
  :assumption
(or (not b19)  (not b398) )
  :assumption
(or (not b398)  (not b452) )
  :assumption
(or (not b401)  (not b455) )
  :assumption
(or (not b398)  (not b446) )
  :assumption
(or (not b401)  (not b449) )
  :assumption
(or (not b395)  (not b437) )
  :assumption
(or (not b398)  (not b440) )
  :assumption
(or (not b401)  (not b443) )
  :assumption
(or (not b398)  (not b431) )
  :assumption
(or (not b401)  (not b434) )
  :assumption
(or (not b398)  (not b425) )
  :assumption
(or (not b401)  (not b428) )
  :assumption
(or (not b395)  (not b416) )
  :assumption
(or (not b398)  (not b419) )
  :assumption
(or (not b401)  (not b422) )
  :assumption
(or (not b326)  (not b398) )
  :assumption
(or (not b308)  (not b398) )
  :assumption
(or (not b309)  (not b401) )
  :assumption
(or (not b275)  (not b395) )
  :assumption
(or (not b278)  (not b398) )
  :assumption
(or (not b246)  (not b395) )
  :assumption
(or (not b249)  (not b398) )
  :assumption
(or (not b180)  (not b395) )
  :assumption
(or (not b165)  (not b395) )
  :assumption
(or (not b149)  (not b401) )
  :assumption
(or (not b140)  (not b395) )
  :assumption
(or (not b120)  (not b395) )
  :assumption
(or (not b101)  (not b398) )
  :assumption
(or (not b80)  (not b398) )
  :assumption
(or (not b59)  (not b398) )
  :assumption
(or (not b48)  (not b398) )
  :assumption
(or (not b23)  (not b398) )
  :assumption
(or (not b404)  (not b410) )
  :assumption
(or (not b407)  (not b413) )
  :assumption
(or (not b323)  (not b404) )
  :assumption
(or (not b324)  (not b407) )
  :assumption
(or (not b296)  (not b404) )
  :assumption
(or (not b273)  (not b404) )
  :assumption
(or (not b210)  (not b404) )
  :assumption
(or (not b163)  (not b407) )
  :assumption
(or (not b138)  (not b407) )
  :assumption
(or (not b117)  (not b407) )
  :assumption
(or (not b98)  (not b404) )
  :assumption
(or (not b77)  (not b404) )
  :assumption
(or (not b45)  (not b404) )
  :assumption
(or (not b19)  (not b404) )
  :assumption
(or (not b404)  (not b452) )
  :assumption
(or (not b407)  (not b455) )
  :assumption
(or (not b404)  (not b446) )
  :assumption
(or (not b407)  (not b449) )
  :assumption
(or (not b404)  (not b440) )
  :assumption
(or (not b407)  (not b443) )
  :assumption
(or (not b404)  (not b431) )
  :assumption
(or (not b407)  (not b434) )
  :assumption
(or (not b404)  (not b425) )
  :assumption
(or (not b407)  (not b428) )
  :assumption
(or (not b404)  (not b419) )
  :assumption
(or (not b407)  (not b422) )
  :assumption
(or (not b326)  (not b404) )
  :assumption
(or (not b298)  (not b404) )
  :assumption
(or (not b278)  (not b404) )
  :assumption
(or (not b212)  (not b404) )
  :assumption
(or (not b149)  (not b407) )
  :assumption
(or (not b101)  (not b404) )
  :assumption
(or (not b80)  (not b404) )
  :assumption
(or (not b59)  (not b404) )
  :assumption
(or (not b48)  (not b404) )
  :assumption
(or (not b23)  (not b404) )
  :assumption
(or (not b307)  (not b410) )
  :assumption
(or (not b296)  (not b410) )
  :assumption
(or (not b244)  (not b410) )
  :assumption
(or (not b210)  (not b410) )
  :assumption
(or (not b163)  (not b413) )
  :assumption
(or (not b138)  (not b413) )
  :assumption
(or (not b117)  (not b413) )
  :assumption
(or (not b98)  (not b410) )
  :assumption
(or (not b77)  (not b410) )
  :assumption
(or (not b45)  (not b410) )
  :assumption
(or (not b19)  (not b410) )
  :assumption
(or (not b410)  (not b452) )
  :assumption
(or (not b413)  (not b455) )
  :assumption
(or (not b410)  (not b446) )
  :assumption
(or (not b413)  (not b449) )
  :assumption
(or (not b410)  (not b440) )
  :assumption
(or (not b413)  (not b443) )
  :assumption
(or (not b410)  (not b431) )
  :assumption
(or (not b413)  (not b434) )
  :assumption
(or (not b410)  (not b425) )
  :assumption
(or (not b413)  (not b428) )
  :assumption
(or (not b410)  (not b419) )
  :assumption
(or (not b413)  (not b422) )
  :assumption
(or (not b308)  (not b410) )
  :assumption
(or (not b309)  (not b413) )
  :assumption
(or (not b298)  (not b410) )
  :assumption
(or (not b249)  (not b410) )
  :assumption
(or (not b212)  (not b410) )
  :assumption
(or (not b149)  (not b413) )
  :assumption
(or (not b101)  (not b410) )
  :assumption
(or (not b80)  (not b410) )
  :assumption
(or (not b59)  (not b410) )
  :assumption
(or (not b48)  (not b410) )
  :assumption
(or (not b23)  (not b410) )
  :assumption
(or (not b419)  (not b452) )
  :assumption
(or (not b422)  (not b455) )
  :assumption
(or (not b419)  (not b446) )
  :assumption
(or (not b422)  (not b449) )
  :assumption
(or (not b416)  (not b437) )
  :assumption
(or (not b419)  (not b440) )
  :assumption
(or (not b422)  (not b443) )
  :assumption
(or (not b419)  (not b431) )
  :assumption
(or (not b422)  (not b434) )
  :assumption
(or (not b419)  (not b425) )
  :assumption
(or (not b422)  (not b428) )
  :assumption
(or (not b326)  (not b419) )
  :assumption
(or (not b308)  (not b419) )
  :assumption
(or (not b309)  (not b422) )
  :assumption
(or (not b275)  (not b416) )
  :assumption
(or (not b278)  (not b419) )
  :assumption
(or (not b246)  (not b416) )
  :assumption
(or (not b249)  (not b419) )
  :assumption
(or (not b180)  (not b416) )
  :assumption
(or (not b165)  (not b416) )
  :assumption
(or (not b149)  (not b422) )
  :assumption
(or (not b140)  (not b416) )
  :assumption
(or (not b120)  (not b416) )
  :assumption
(or (not b101)  (not b419) )
  :assumption
(or (not b80)  (not b419) )
  :assumption
(or (not b59)  (not b419) )
  :assumption
(or (not b48)  (not b419) )
  :assumption
(or (not b23)  (not b419) )
  :assumption
(or (not b322)  (not b419) )
  :assumption
(or (not b306)  (not b419) )
  :assumption
(or (not b263)  (not b416) )
  :assumption
(or (not b267)  (not b419) )
  :assumption
(or (not b234)  (not b416) )
  :assumption
(or (not b238)  (not b419) )
  :assumption
(or (not b174)  (not b416) )
  :assumption
(or (not b176)  (not b422) )
  :assumption
(or (not b160)  (not b416) )
  :assumption
(or (not b135)  (not b416) )
  :assumption
(or (not b112)  (not b416) )
  :assumption
(or (not b91)  (not b419) )
  :assumption
(or (not b70)  (not b419) )
  :assumption
(or (not b38)  (not b419) )
  :assumption
(or (not b11)  (not b419) )
  :assumption
(or (not b425)  (not b452) )
  :assumption
(or (not b428)  (not b455) )
  :assumption
(or (not b425)  (not b446) )
  :assumption
(or (not b428)  (not b449) )
  :assumption
(or (not b425)  (not b440) )
  :assumption
(or (not b428)  (not b443) )
  :assumption
(or (not b425)  (not b431) )
  :assumption
(or (not b428)  (not b434) )
  :assumption
(or (not b326)  (not b425) )
  :assumption
(or (not b298)  (not b425) )
  :assumption
(or (not b278)  (not b425) )
  :assumption
(or (not b212)  (not b425) )
  :assumption
(or (not b149)  (not b428) )
  :assumption
(or (not b101)  (not b425) )
  :assumption
(or (not b80)  (not b425) )
  :assumption
(or (not b59)  (not b425) )
  :assumption
(or (not b48)  (not b425) )
  :assumption
(or (not b23)  (not b425) )
  :assumption
(or (not b322)  (not b425) )
  :assumption
(or (not b293)  (not b425) )
  :assumption
(or (not b267)  (not b425) )
  :assumption
(or (not b197)  (not b425) )
  :assumption
(or (not b176)  (not b428) )
  :assumption
(or (not b91)  (not b425) )
  :assumption
(or (not b70)  (not b425) )
  :assumption
(or (not b38)  (not b425) )
  :assumption
(or (not b11)  (not b425) )
  :assumption
(or (not b431)  (not b452) )
  :assumption
(or (not b434)  (not b455) )
  :assumption
(or (not b431)  (not b446) )
  :assumption
(or (not b434)  (not b449) )
  :assumption
(or (not b431)  (not b440) )
  :assumption
(or (not b434)  (not b443) )
  :assumption
(or (not b308)  (not b431) )
  :assumption
(or (not b309)  (not b434) )
  :assumption
(or (not b298)  (not b431) )
  :assumption
(or (not b249)  (not b431) )
  :assumption
(or (not b212)  (not b431) )
  :assumption
(or (not b149)  (not b434) )
  :assumption
(or (not b101)  (not b431) )
  :assumption
(or (not b80)  (not b431) )
  :assumption
(or (not b59)  (not b431) )
  :assumption
(or (not b48)  (not b431) )
  :assumption
(or (not b23)  (not b431) )
  :assumption
(or (not b306)  (not b431) )
  :assumption
(or (not b293)  (not b431) )
  :assumption
(or (not b238)  (not b431) )
  :assumption
(or (not b197)  (not b431) )
  :assumption
(or (not b176)  (not b434) )
  :assumption
(or (not b91)  (not b431) )
  :assumption
(or (not b70)  (not b431) )
  :assumption
(or (not b38)  (not b431) )
  :assumption
(or (not b11)  (not b431) )
  :assumption
(or (not b440)  (not b452) )
  :assumption
(or (not b443)  (not b455) )
  :assumption
(or (not b440)  (not b446) )
  :assumption
(or (not b443)  (not b449) )
  :assumption
(or (not b326)  (not b440) )
  :assumption
(or (not b308)  (not b440) )
  :assumption
(or (not b309)  (not b443) )
  :assumption
(or (not b275)  (not b437) )
  :assumption
(or (not b278)  (not b440) )
  :assumption
(or (not b246)  (not b437) )
  :assumption
(or (not b249)  (not b440) )
  :assumption
(or (not b180)  (not b437) )
  :assumption
(or (not b165)  (not b437) )
  :assumption
(or (not b149)  (not b443) )
  :assumption
(or (not b140)  (not b437) )
  :assumption
(or (not b120)  (not b437) )
  :assumption
(or (not b101)  (not b440) )
  :assumption
(or (not b80)  (not b440) )
  :assumption
(or (not b59)  (not b440) )
  :assumption
(or (not b48)  (not b440) )
  :assumption
(or (not b23)  (not b440) )
  :assumption
(or (not b323)  (not b440) )
  :assumption
(or (not b324)  (not b443) )
  :assumption
(or (not b307)  (not b440) )
  :assumption
(or (not b270)  (not b437) )
  :assumption
(or (not b273)  (not b440) )
  :assumption
(or (not b241)  (not b437) )
  :assumption
(or (not b244)  (not b440) )
  :assumption
(or (not b179)  (not b437) )
  :assumption
(or (not b162)  (not b437) )
  :assumption
(or (not b163)  (not b443) )
  :assumption
(or (not b137)  (not b437) )
  :assumption
(or (not b138)  (not b443) )
  :assumption
(or (not b115)  (not b437) )
  :assumption
(or (not b117)  (not b443) )
  :assumption
(or (not b98)  (not b440) )
  :assumption
(or (not b77)  (not b440) )
  :assumption
(or (not b45)  (not b440) )
  :assumption
(or (not b19)  (not b440) )
  :assumption
(or (not b446)  (not b452) )
  :assumption
(or (not b449)  (not b455) )
  :assumption
(or (not b326)  (not b446) )
  :assumption
(or (not b298)  (not b446) )
  :assumption
(or (not b278)  (not b446) )
  :assumption
(or (not b212)  (not b446) )
  :assumption
(or (not b149)  (not b449) )
  :assumption
(or (not b101)  (not b446) )
  :assumption
(or (not b80)  (not b446) )
  :assumption
(or (not b59)  (not b446) )
  :assumption
(or (not b48)  (not b446) )
  :assumption
(or (not b23)  (not b446) )
  :assumption
(or (not b323)  (not b446) )
  :assumption
(or (not b324)  (not b449) )
  :assumption
(or (not b296)  (not b446) )
  :assumption
(or (not b273)  (not b446) )
  :assumption
(or (not b210)  (not b446) )
  :assumption
(or (not b163)  (not b449) )
  :assumption
(or (not b138)  (not b449) )
  :assumption
(or (not b117)  (not b449) )
  :assumption
(or (not b98)  (not b446) )
  :assumption
(or (not b77)  (not b446) )
  :assumption
(or (not b45)  (not b446) )
  :assumption
(or (not b19)  (not b446) )
  :assumption
(or (not b308)  (not b452) )
  :assumption
(or (not b309)  (not b455) )
  :assumption
(or (not b298)  (not b452) )
  :assumption
(or (not b249)  (not b452) )
  :assumption
(or (not b212)  (not b452) )
  :assumption
(or (not b149)  (not b455) )
  :assumption
(or (not b101)  (not b452) )
  :assumption
(or (not b80)  (not b452) )
  :assumption
(or (not b59)  (not b452) )
  :assumption
(or (not b48)  (not b452) )
  :assumption
(or (not b23)  (not b452) )
  :assumption
(or (not b307)  (not b452) )
  :assumption
(or (not b296)  (not b452) )
  :assumption
(or (not b244)  (not b452) )
  :assumption
(or (not b210)  (not b452) )
  :assumption
(or (not b163)  (not b455) )
  :assumption
(or (not b138)  (not b455) )
  :assumption
(or (not b117)  (not b455) )
  :assumption
(or (not b98)  (not b452) )
  :assumption
(or (not b77)  (not b452) )
  :assumption
(or (not b45)  (not b452) )
  :assumption
(or (not b19)  (not b452) )
  :assumption
(or (not b461)  (not b496) )
  :assumption
(or (not b464)  (not b499) )
  :assumption
(or (not b461)  (not b490) )
  :assumption
(or (not b464)  (not b493) )
  :assumption
(or (not b458)  (not b481) )
  :assumption
(or (not b461)  (not b484) )
  :assumption
(or (not b464)  (not b487) )
  :assumption
(or (not b461)  (not b475) )
  :assumption
(or (not b464)  (not b478) )
  :assumption
(or (not b461)  (not b469) )
  :assumption
(or (not b464)  (not b472) )
  :assumption
(or (not b327)  (not b461) )
  :assumption
(or (not b312)  (not b461) )
  :assumption
(or (not b280)  (not b458) )
  :assumption
(or (not b282)  (not b461) )
  :assumption
(or (not b251)  (not b458) )
  :assumption
(or (not b253)  (not b461) )
  :assumption
(or (not b181)  (not b458) )
  :assumption
(or (not b183)  (not b464) )
  :assumption
(or (not b166)  (not b458) )
  :assumption
(or (not b141)  (not b458) )
  :assumption
(or (not b122)  (not b458) )
  :assumption
(or (not b104)  (not b461) )
  :assumption
(or (not b83)  (not b461) )
  :assumption
(or (not b51)  (not b461) )
  :assumption
(or (not b27)  (not b461) )
  :assumption
(or (not b461)  (not b561) )
  :assumption
(or (not b461)  (not b557) )
  :assumption
(or (not b458)  (not b550) )
  :assumption
(or (not b461)  (not b553) )
  :assumption
(or (not b461)  (not b520) )
  :assumption
(or (not b464)  (not b523) )
  :assumption
(or (not b461)  (not b514) )
  :assumption
(or (not b464)  (not b517) )
  :assumption
(or (not b458)  (not b505) )
  :assumption
(or (not b461)  (not b508) )
  :assumption
(or (not b464)  (not b511) )
  :assumption
(or (not b461)  (not b544) )
  :assumption
(or (not b464)  (not b547) )
  :assumption
(or (not b461)  (not b538) )
  :assumption
(or (not b464)  (not b541) )
  :assumption
(or (not b458)  (not b529) )
  :assumption
(or (not b461)  (not b532) )
  :assumption
(or (not b464)  (not b535) )
  :assumption
(or (not b328)  (not b461) )
  :assumption
(or (not b329)  (not b464) )
  :assumption
(or (not b313)  (not b461) )
  :assumption
(or (not b284)  (not b458) )
  :assumption
(or (not b285)  (not b461) )
  :assumption
(or (not b255)  (not b458) )
  :assumption
(or (not b256)  (not b461) )
  :assumption
(or (not b186)  (not b458) )
  :assumption
(or (not b168)  (not b458) )
  :assumption
(or (not b169)  (not b464) )
  :assumption
(or (not b143)  (not b458) )
  :assumption
(or (not b144)  (not b464) )
  :assumption
(or (not b125)  (not b458) )
  :assumption
(or (not b127)  (not b464) )
  :assumption
(or (not b108)  (not b461) )
  :assumption
(or (not b87)  (not b461) )
  :assumption
(or (not b55)  (not b461) )
  :assumption
(or (not b32)  (not b461) )
  :assumption
(or (not b469)  (not b496) )
  :assumption
(or (not b472)  (not b499) )
  :assumption
(or (not b469)  (not b490) )
  :assumption
(or (not b472)  (not b493) )
  :assumption
(or (not b469)  (not b484) )
  :assumption
(or (not b472)  (not b487) )
  :assumption
(or (not b469)  (not b475) )
  :assumption
(or (not b472)  (not b478) )
  :assumption
(or (not b327)  (not b469) )
  :assumption
(or (not b300)  (not b469) )
  :assumption
(or (not b282)  (not b469) )
  :assumption
(or (not b219)  (not b469) )
  :assumption
(or (not b183)  (not b472) )
  :assumption
(or (not b104)  (not b469) )
  :assumption
(or (not b83)  (not b469) )
  :assumption
(or (not b51)  (not b469) )
  :assumption
(or (not b27)  (not b469) )
  :assumption
(or (not b469)  (not b561) )
  :assumption
(or (not b469)  (not b557) )
  :assumption
(or (not b469)  (not b553) )
  :assumption
(or (not b469)  (not b520) )
  :assumption
(or (not b472)  (not b523) )
  :assumption
(or (not b469)  (not b514) )
  :assumption
(or (not b472)  (not b517) )
  :assumption
(or (not b469)  (not b508) )
  :assumption
(or (not b472)  (not b511) )
  :assumption
(or (not b469)  (not b544) )
  :assumption
(or (not b472)  (not b547) )
  :assumption
(or (not b469)  (not b538) )
  :assumption
(or (not b472)  (not b541) )
  :assumption
(or (not b469)  (not b532) )
  :assumption
(or (not b472)  (not b535) )
  :assumption
(or (not b328)  (not b469) )
  :assumption
(or (not b329)  (not b472) )
  :assumption
(or (not b303)  (not b469) )
  :assumption
(or (not b285)  (not b469) )
  :assumption
(or (not b228)  (not b469) )
  :assumption
(or (not b169)  (not b472) )
  :assumption
(or (not b144)  (not b472) )
  :assumption
(or (not b127)  (not b472) )
  :assumption
(or (not b108)  (not b469) )
  :assumption
(or (not b87)  (not b469) )
  :assumption
(or (not b55)  (not b469) )
  :assumption
(or (not b32)  (not b469) )
  :assumption
(or (not b475)  (not b496) )
  :assumption
(or (not b478)  (not b499) )
  :assumption
(or (not b475)  (not b490) )
  :assumption
(or (not b478)  (not b493) )
  :assumption
(or (not b475)  (not b484) )
  :assumption
(or (not b478)  (not b487) )
  :assumption
(or (not b312)  (not b475) )
  :assumption
(or (not b300)  (not b475) )
  :assumption
(or (not b253)  (not b475) )
  :assumption
(or (not b219)  (not b475) )
  :assumption
(or (not b183)  (not b478) )
  :assumption
(or (not b104)  (not b475) )
  :assumption
(or (not b83)  (not b475) )
  :assumption
(or (not b51)  (not b475) )
  :assumption
(or (not b27)  (not b475) )
  :assumption
(or (not b475)  (not b561) )
  :assumption
(or (not b475)  (not b557) )
  :assumption
(or (not b475)  (not b553) )
  :assumption
(or (not b475)  (not b520) )
  :assumption
(or (not b478)  (not b523) )
  :assumption
(or (not b475)  (not b514) )
  :assumption
(or (not b478)  (not b517) )
  :assumption
(or (not b475)  (not b508) )
  :assumption
(or (not b478)  (not b511) )
  :assumption
(or (not b475)  (not b544) )
  :assumption
(or (not b478)  (not b547) )
  :assumption
(or (not b475)  (not b538) )
  :assumption
(or (not b478)  (not b541) )
  :assumption
(or (not b475)  (not b532) )
  :assumption
(or (not b478)  (not b535) )
  :assumption
(or (not b313)  (not b475) )
  :assumption
(or (not b303)  (not b475) )
  :assumption
(or (not b256)  (not b475) )
  :assumption
(or (not b228)  (not b475) )
  :assumption
(or (not b169)  (not b478) )
  :assumption
(or (not b144)  (not b478) )
  :assumption
(or (not b127)  (not b478) )
  :assumption
(or (not b108)  (not b475) )
  :assumption
(or (not b87)  (not b475) )
  :assumption
(or (not b55)  (not b475) )
  :assumption
(or (not b32)  (not b475) )
  :assumption
(or (not b484)  (not b496) )
  :assumption
(or (not b487)  (not b499) )
  :assumption
(or (not b484)  (not b490) )
  :assumption
(or (not b487)  (not b493) )
  :assumption
(or (not b327)  (not b484) )
  :assumption
(or (not b312)  (not b484) )
  :assumption
(or (not b280)  (not b481) )
  :assumption
(or (not b282)  (not b484) )
  :assumption
(or (not b251)  (not b481) )
  :assumption
(or (not b253)  (not b484) )
  :assumption
(or (not b181)  (not b481) )
  :assumption
(or (not b183)  (not b487) )
  :assumption
(or (not b166)  (not b481) )
  :assumption
(or (not b141)  (not b481) )
  :assumption
(or (not b122)  (not b481) )
  :assumption
(or (not b104)  (not b484) )
  :assumption
(or (not b83)  (not b484) )
  :assumption
(or (not b51)  (not b484) )
  :assumption
(or (not b27)  (not b484) )
  :assumption
(or (not b484)  (not b561) )
  :assumption
(or (not b484)  (not b557) )
  :assumption
(or (not b481)  (not b550) )
  :assumption
(or (not b484)  (not b553) )
  :assumption
(or (not b484)  (not b520) )
  :assumption
(or (not b487)  (not b523) )
  :assumption
(or (not b484)  (not b514) )
  :assumption
(or (not b487)  (not b517) )
  :assumption
(or (not b481)  (not b505) )
  :assumption
(or (not b484)  (not b508) )
  :assumption
(or (not b487)  (not b511) )
  :assumption
(or (not b484)  (not b576) )
  :assumption
(or (not b484)  (not b572) )
  :assumption
(or (not b481)  (not b565) )
  :assumption
(or (not b484)  (not b568) )
  :assumption
(or (not b331)  (not b484) )
  :assumption
(or (not b314)  (not b484) )
  :assumption
(or (not b315)  (not b487) )
  :assumption
(or (not b286)  (not b481) )
  :assumption
(or (not b287)  (not b484) )
  :assumption
(or (not b257)  (not b481) )
  :assumption
(or (not b258)  (not b484) )
  :assumption
(or (not b187)  (not b481) )
  :assumption
(or (not b171)  (not b481) )
  :assumption
(or (not b152)  (not b487) )
  :assumption
(or (not b146)  (not b481) )
  :assumption
(or (not b130)  (not b481) )
  :assumption
(or (not b109)  (not b484) )
  :assumption
(or (not b88)  (not b484) )
  :assumption
(or (not b63)  (not b484) )
  :assumption
(or (not b56)  (not b484) )
  :assumption
(or (not b34)  (not b484) )
  :assumption
(or (not b490)  (not b496) )
  :assumption
(or (not b493)  (not b499) )
  :assumption
(or (not b327)  (not b490) )
  :assumption
(or (not b300)  (not b490) )
  :assumption
(or (not b282)  (not b490) )
  :assumption
(or (not b219)  (not b490) )
  :assumption
(or (not b183)  (not b493) )
  :assumption
(or (not b104)  (not b490) )
  :assumption
(or (not b83)  (not b490) )
  :assumption
(or (not b51)  (not b490) )
  :assumption
(or (not b27)  (not b490) )
  :assumption
(or (not b490)  (not b561) )
  :assumption
(or (not b490)  (not b557) )
  :assumption
(or (not b490)  (not b553) )
  :assumption
(or (not b490)  (not b520) )
  :assumption
(or (not b493)  (not b523) )
  :assumption
(or (not b490)  (not b514) )
  :assumption
(or (not b493)  (not b517) )
  :assumption
(or (not b490)  (not b508) )
  :assumption
(or (not b493)  (not b511) )
  :assumption
(or (not b490)  (not b576) )
  :assumption
(or (not b490)  (not b572) )
  :assumption
(or (not b490)  (not b568) )
  :assumption
(or (not b331)  (not b490) )
  :assumption
(or (not b305)  (not b490) )
  :assumption
(or (not b287)  (not b490) )
  :assumption
(or (not b229)  (not b490) )
  :assumption
(or (not b152)  (not b493) )
  :assumption
(or (not b109)  (not b490) )
  :assumption
(or (not b88)  (not b490) )
  :assumption
(or (not b63)  (not b490) )
  :assumption
(or (not b56)  (not b490) )
  :assumption
(or (not b34)  (not b490) )
  :assumption
(or (not b312)  (not b496) )
  :assumption
(or (not b300)  (not b496) )
  :assumption
(or (not b253)  (not b496) )
  :assumption
(or (not b219)  (not b496) )
  :assumption
(or (not b183)  (not b499) )
  :assumption
(or (not b104)  (not b496) )
  :assumption
(or (not b83)  (not b496) )
  :assumption
(or (not b51)  (not b496) )
  :assumption
(or (not b27)  (not b496) )
  :assumption
(or (not b496)  (not b561) )
  :assumption
(or (not b496)  (not b557) )
  :assumption
(or (not b496)  (not b553) )
  :assumption
(or (not b496)  (not b520) )
  :assumption
(or (not b499)  (not b523) )
  :assumption
(or (not b496)  (not b514) )
  :assumption
(or (not b499)  (not b517) )
  :assumption
(or (not b496)  (not b508) )
  :assumption
(or (not b499)  (not b511) )
  :assumption
(or (not b496)  (not b576) )
  :assumption
(or (not b496)  (not b572) )
  :assumption
(or (not b496)  (not b568) )
  :assumption
(or (not b314)  (not b496) )
  :assumption
(or (not b315)  (not b499) )
  :assumption
(or (not b305)  (not b496) )
  :assumption
(or (not b258)  (not b496) )
  :assumption
(or (not b229)  (not b496) )
  :assumption
(or (not b152)  (not b499) )
  :assumption
(or (not b109)  (not b496) )
  :assumption
(or (not b88)  (not b496) )
  :assumption
(or (not b63)  (not b496) )
  :assumption
(or (not b56)  (not b496) )
  :assumption
(or (not b34)  (not b496) )
  :assumption
(or (not b508)  (not b544) )
  :assumption
(or (not b511)  (not b547) )
  :assumption
(or (not b508)  (not b538) )
  :assumption
(or (not b511)  (not b541) )
  :assumption
(or (not b502)  (not b526) )
  :assumption
(or (not b505)  (not b529) )
  :assumption
(or (not b508)  (not b532) )
  :assumption
(or (not b511)  (not b535) )
  :assumption
(or (not b508)  (not b520) )
  :assumption
(or (not b511)  (not b523) )
  :assumption
(or (not b508)  (not b514) )
  :assumption
(or (not b511)  (not b517) )
  :assumption
(or (not b328)  (not b508) )
  :assumption
(or (not b329)  (not b511) )
  :assumption
(or (not b313)  (not b508) )
  :assumption
(or (not b284)  (not b505) )
  :assumption
(or (not b285)  (not b508) )
  :assumption
(or (not b255)  (not b505) )
  :assumption
(or (not b256)  (not b508) )
  :assumption
(or (not b186)  (not b505) )
  :assumption
(or (not b168)  (not b505) )
  :assumption
(or (not b169)  (not b511) )
  :assumption
(or (not b143)  (not b505) )
  :assumption
(or (not b144)  (not b511) )
  :assumption
(or (not b125)  (not b505) )
  :assumption
(or (not b127)  (not b511) )
  :assumption
(or (not b106)  (not b502) )
  :assumption
(or (not b108)  (not b508) )
  :assumption
(or (not b85)  (not b502) )
  :assumption
(or (not b87)  (not b508) )
  :assumption
(or (not b53)  (not b502) )
  :assumption
(or (not b55)  (not b508) )
  :assumption
(or (not b30)  (not b502) )
  :assumption
(or (not b32)  (not b508) )
  :assumption
(or (not b508)  (not b576) )
  :assumption
(or (not b508)  (not b572) )
  :assumption
(or (not b505)  (not b565) )
  :assumption
(or (not b508)  (not b568) )
  :assumption
(or (not b327)  (not b508) )
  :assumption
(or (not b312)  (not b508) )
  :assumption
(or (not b280)  (not b505) )
  :assumption
(or (not b282)  (not b508) )
  :assumption
(or (not b251)  (not b505) )
  :assumption
(or (not b253)  (not b508) )
  :assumption
(or (not b181)  (not b505) )
  :assumption
(or (not b183)  (not b511) )
  :assumption
(or (not b166)  (not b505) )
  :assumption
(or (not b141)  (not b505) )
  :assumption
(or (not b122)  (not b505) )
  :assumption
(or (not b104)  (not b508) )
  :assumption
(or (not b83)  (not b508) )
  :assumption
(or (not b51)  (not b508) )
  :assumption
(or (not b27)  (not b508) )
  :assumption
(or (not b514)  (not b544) )
  :assumption
(or (not b517)  (not b547) )
  :assumption
(or (not b514)  (not b538) )
  :assumption
(or (not b517)  (not b541) )
  :assumption
(or (not b514)  (not b532) )
  :assumption
(or (not b517)  (not b535) )
  :assumption
(or (not b514)  (not b520) )
  :assumption
(or (not b517)  (not b523) )
  :assumption
(or (not b328)  (not b514) )
  :assumption
(or (not b329)  (not b517) )
  :assumption
(or (not b303)  (not b514) )
  :assumption
(or (not b285)  (not b514) )
  :assumption
(or (not b228)  (not b514) )
  :assumption
(or (not b169)  (not b517) )
  :assumption
(or (not b144)  (not b517) )
  :assumption
(or (not b127)  (not b517) )
  :assumption
(or (not b108)  (not b514) )
  :assumption
(or (not b87)  (not b514) )
  :assumption
(or (not b55)  (not b514) )
  :assumption
(or (not b32)  (not b514) )
  :assumption
(or (not b514)  (not b576) )
  :assumption
(or (not b514)  (not b572) )
  :assumption
(or (not b514)  (not b568) )
  :assumption
(or (not b327)  (not b514) )
  :assumption
(or (not b300)  (not b514) )
  :assumption
(or (not b282)  (not b514) )
  :assumption
(or (not b219)  (not b514) )
  :assumption
(or (not b183)  (not b517) )
  :assumption
(or (not b104)  (not b514) )
  :assumption
(or (not b83)  (not b514) )
  :assumption
(or (not b51)  (not b514) )
  :assumption
(or (not b27)  (not b514) )
  :assumption
(or (not b520)  (not b544) )
  :assumption
(or (not b523)  (not b547) )
  :assumption
(or (not b520)  (not b538) )
  :assumption
(or (not b523)  (not b541) )
  :assumption
(or (not b520)  (not b532) )
  :assumption
(or (not b523)  (not b535) )
  :assumption
(or (not b313)  (not b520) )
  :assumption
(or (not b303)  (not b520) )
  :assumption
(or (not b256)  (not b520) )
  :assumption
(or (not b228)  (not b520) )
  :assumption
(or (not b169)  (not b523) )
  :assumption
(or (not b144)  (not b523) )
  :assumption
(or (not b127)  (not b523) )
  :assumption
(or (not b108)  (not b520) )
  :assumption
(or (not b87)  (not b520) )
  :assumption
(or (not b55)  (not b520) )
  :assumption
(or (not b32)  (not b520) )
  :assumption
(or (not b520)  (not b576) )
  :assumption
(or (not b520)  (not b572) )
  :assumption
(or (not b520)  (not b568) )
  :assumption
(or (not b312)  (not b520) )
  :assumption
(or (not b300)  (not b520) )
  :assumption
(or (not b253)  (not b520) )
  :assumption
(or (not b219)  (not b520) )
  :assumption
(or (not b183)  (not b523) )
  :assumption
(or (not b104)  (not b520) )
  :assumption
(or (not b83)  (not b520) )
  :assumption
(or (not b51)  (not b520) )
  :assumption
(or (not b27)  (not b520) )
  :assumption
(or (not b532)  (not b544) )
  :assumption
(or (not b535)  (not b547) )
  :assumption
(or (not b532)  (not b538) )
  :assumption
(or (not b535)  (not b541) )
  :assumption
(or (not b328)  (not b532) )
  :assumption
(or (not b329)  (not b535) )
  :assumption
(or (not b313)  (not b532) )
  :assumption
(or (not b284)  (not b529) )
  :assumption
(or (not b285)  (not b532) )
  :assumption
(or (not b255)  (not b529) )
  :assumption
(or (not b256)  (not b532) )
  :assumption
(or (not b186)  (not b529) )
  :assumption
(or (not b168)  (not b529) )
  :assumption
(or (not b169)  (not b535) )
  :assumption
(or (not b143)  (not b529) )
  :assumption
(or (not b144)  (not b535) )
  :assumption
(or (not b125)  (not b529) )
  :assumption
(or (not b127)  (not b535) )
  :assumption
(or (not b106)  (not b526) )
  :assumption
(or (not b108)  (not b532) )
  :assumption
(or (not b85)  (not b526) )
  :assumption
(or (not b87)  (not b532) )
  :assumption
(or (not b53)  (not b526) )
  :assumption
(or (not b55)  (not b532) )
  :assumption
(or (not b30)  (not b526) )
  :assumption
(or (not b32)  (not b532) )
  :assumption
(or (not b532)  (not b576) )
  :assumption
(or (not b532)  (not b572) )
  :assumption
(or (not b529)  (not b565) )
  :assumption
(or (not b532)  (not b568) )
  :assumption
(or (not b532)  (not b561) )
  :assumption
(or (not b532)  (not b557) )
  :assumption
(or (not b529)  (not b550) )
  :assumption
(or (not b532)  (not b553) )
  :assumption
(or (not b331)  (not b532) )
  :assumption
(or (not b314)  (not b532) )
  :assumption
(or (not b315)  (not b535) )
  :assumption
(or (not b286)  (not b529) )
  :assumption
(or (not b287)  (not b532) )
  :assumption
(or (not b257)  (not b529) )
  :assumption
(or (not b258)  (not b532) )
  :assumption
(or (not b187)  (not b529) )
  :assumption
(or (not b171)  (not b529) )
  :assumption
(or (not b152)  (not b535) )
  :assumption
(or (not b146)  (not b529) )
  :assumption
(or (not b130)  (not b529) )
  :assumption
(or (not b109)  (not b532) )
  :assumption
(or (not b88)  (not b532) )
  :assumption
(or (not b63)  (not b532) )
  :assumption
(or (not b56)  (not b532) )
  :assumption
(or (not b34)  (not b532) )
  :assumption
(or (not b538)  (not b544) )
  :assumption
(or (not b541)  (not b547) )
  :assumption
(or (not b328)  (not b538) )
  :assumption
(or (not b329)  (not b541) )
  :assumption
(or (not b303)  (not b538) )
  :assumption
(or (not b285)  (not b538) )
  :assumption
(or (not b228)  (not b538) )
  :assumption
(or (not b169)  (not b541) )
  :assumption
(or (not b144)  (not b541) )
  :assumption
(or (not b127)  (not b541) )
  :assumption
(or (not b108)  (not b538) )
  :assumption
(or (not b87)  (not b538) )
  :assumption
(or (not b55)  (not b538) )
  :assumption
(or (not b32)  (not b538) )
  :assumption
(or (not b538)  (not b576) )
  :assumption
(or (not b538)  (not b572) )
  :assumption
(or (not b538)  (not b568) )
  :assumption
(or (not b538)  (not b561) )
  :assumption
(or (not b538)  (not b557) )
  :assumption
(or (not b538)  (not b553) )
  :assumption
(or (not b331)  (not b538) )
  :assumption
(or (not b305)  (not b538) )
  :assumption
(or (not b287)  (not b538) )
  :assumption
(or (not b229)  (not b538) )
  :assumption
(or (not b152)  (not b541) )
  :assumption
(or (not b109)  (not b538) )
  :assumption
(or (not b88)  (not b538) )
  :assumption
(or (not b63)  (not b538) )
  :assumption
(or (not b56)  (not b538) )
  :assumption
(or (not b34)  (not b538) )
  :assumption
(or (not b313)  (not b544) )
  :assumption
(or (not b303)  (not b544) )
  :assumption
(or (not b256)  (not b544) )
  :assumption
(or (not b228)  (not b544) )
  :assumption
(or (not b169)  (not b547) )
  :assumption
(or (not b144)  (not b547) )
  :assumption
(or (not b127)  (not b547) )
  :assumption
(or (not b108)  (not b544) )
  :assumption
(or (not b87)  (not b544) )
  :assumption
(or (not b55)  (not b544) )
  :assumption
(or (not b32)  (not b544) )
  :assumption
(or (not b544)  (not b576) )
  :assumption
(or (not b544)  (not b572) )
  :assumption
(or (not b544)  (not b568) )
  :assumption
(or (not b544)  (not b561) )
  :assumption
(or (not b544)  (not b557) )
  :assumption
(or (not b544)  (not b553) )
  :assumption
(or (not b314)  (not b544) )
  :assumption
(or (not b315)  (not b547) )
  :assumption
(or (not b305)  (not b544) )
  :assumption
(or (not b258)  (not b544) )
  :assumption
(or (not b229)  (not b544) )
  :assumption
(or (not b152)  (not b547) )
  :assumption
(or (not b109)  (not b544) )
  :assumption
(or (not b88)  (not b544) )
  :assumption
(or (not b63)  (not b544) )
  :assumption
(or (not b56)  (not b544) )
  :assumption
(or (not b34)  (not b544) )
  :assumption
(or (not b553)  (not b576) )
  :assumption
(or (not b553)  (not b572) )
  :assumption
(or (not b550)  (not b565) )
  :assumption
(or (not b553)  (not b568) )
  :assumption
(or (not b553)  (not b561) )
  :assumption
(or (not b553)  (not b557) )
  :assumption
(or (not b331)  (not b553) )
  :assumption
(or (not b314)  (not b553) )
  :assumption
(or (not b286)  (not b550) )
  :assumption
(or (not b287)  (not b553) )
  :assumption
(or (not b257)  (not b550) )
  :assumption
(or (not b258)  (not b553) )
  :assumption
(or (not b187)  (not b550) )
  :assumption
(or (not b171)  (not b550) )
  :assumption
(or (not b146)  (not b550) )
  :assumption
(or (not b130)  (not b550) )
  :assumption
(or (not b109)  (not b553) )
  :assumption
(or (not b88)  (not b553) )
  :assumption
(or (not b63)  (not b553) )
  :assumption
(or (not b56)  (not b553) )
  :assumption
(or (not b34)  (not b553) )
  :assumption
(or (not b327)  (not b553) )
  :assumption
(or (not b312)  (not b553) )
  :assumption
(or (not b280)  (not b550) )
  :assumption
(or (not b282)  (not b553) )
  :assumption
(or (not b251)  (not b550) )
  :assumption
(or (not b253)  (not b553) )
  :assumption
(or (not b181)  (not b550) )
  :assumption
(or (not b166)  (not b550) )
  :assumption
(or (not b141)  (not b550) )
  :assumption
(or (not b122)  (not b550) )
  :assumption
(or (not b104)  (not b553) )
  :assumption
(or (not b83)  (not b553) )
  :assumption
(or (not b51)  (not b553) )
  :assumption
(or (not b27)  (not b553) )
  :assumption
(or (not b557)  (not b576) )
  :assumption
(or (not b557)  (not b572) )
  :assumption
(or (not b557)  (not b568) )
  :assumption
(or (not b557)  (not b561) )
  :assumption
(or (not b331)  (not b557) )
  :assumption
(or (not b305)  (not b557) )
  :assumption
(or (not b287)  (not b557) )
  :assumption
(or (not b229)  (not b557) )
  :assumption
(or (not b109)  (not b557) )
  :assumption
(or (not b88)  (not b557) )
  :assumption
(or (not b63)  (not b557) )
  :assumption
(or (not b56)  (not b557) )
  :assumption
(or (not b34)  (not b557) )
  :assumption
(or (not b327)  (not b557) )
  :assumption
(or (not b300)  (not b557) )
  :assumption
(or (not b282)  (not b557) )
  :assumption
(or (not b219)  (not b557) )
  :assumption
(or (not b104)  (not b557) )
  :assumption
(or (not b83)  (not b557) )
  :assumption
(or (not b51)  (not b557) )
  :assumption
(or (not b27)  (not b557) )
  :assumption
(or (not b561)  (not b576) )
  :assumption
(or (not b561)  (not b572) )
  :assumption
(or (not b561)  (not b568) )
  :assumption
(or (not b314)  (not b561) )
  :assumption
(or (not b305)  (not b561) )
  :assumption
(or (not b258)  (not b561) )
  :assumption
(or (not b229)  (not b561) )
  :assumption
(or (not b109)  (not b561) )
  :assumption
(or (not b88)  (not b561) )
  :assumption
(or (not b63)  (not b561) )
  :assumption
(or (not b56)  (not b561) )
  :assumption
(or (not b34)  (not b561) )
  :assumption
(or (not b312)  (not b561) )
  :assumption
(or (not b300)  (not b561) )
  :assumption
(or (not b253)  (not b561) )
  :assumption
(or (not b219)  (not b561) )
  :assumption
(or (not b104)  (not b561) )
  :assumption
(or (not b83)  (not b561) )
  :assumption
(or (not b51)  (not b561) )
  :assumption
(or (not b27)  (not b561) )
  :assumption
(or (not b568)  (not b576) )
  :assumption
(or (not b568)  (not b572) )
  :assumption
(or (not b331)  (not b568) )
  :assumption
(or (not b314)  (not b568) )
  :assumption
(or (not b286)  (not b565) )
  :assumption
(or (not b287)  (not b568) )
  :assumption
(or (not b257)  (not b565) )
  :assumption
(or (not b258)  (not b568) )
  :assumption
(or (not b187)  (not b565) )
  :assumption
(or (not b171)  (not b565) )
  :assumption
(or (not b146)  (not b565) )
  :assumption
(or (not b130)  (not b565) )
  :assumption
(or (not b109)  (not b568) )
  :assumption
(or (not b88)  (not b568) )
  :assumption
(or (not b63)  (not b568) )
  :assumption
(or (not b56)  (not b568) )
  :assumption
(or (not b34)  (not b568) )
  :assumption
(or (not b328)  (not b568) )
  :assumption
(or (not b313)  (not b568) )
  :assumption
(or (not b284)  (not b565) )
  :assumption
(or (not b285)  (not b568) )
  :assumption
(or (not b255)  (not b565) )
  :assumption
(or (not b256)  (not b568) )
  :assumption
(or (not b186)  (not b565) )
  :assumption
(or (not b168)  (not b565) )
  :assumption
(or (not b143)  (not b565) )
  :assumption
(or (not b125)  (not b565) )
  :assumption
(or (not b108)  (not b568) )
  :assumption
(or (not b87)  (not b568) )
  :assumption
(or (not b55)  (not b568) )
  :assumption
(or (not b32)  (not b568) )
  :assumption
(or (not b572)  (not b576) )
  :assumption
(or (not b331)  (not b572) )
  :assumption
(or (not b305)  (not b572) )
  :assumption
(or (not b287)  (not b572) )
  :assumption
(or (not b229)  (not b572) )
  :assumption
(or (not b109)  (not b572) )
  :assumption
(or (not b88)  (not b572) )
  :assumption
(or (not b63)  (not b572) )
  :assumption
(or (not b56)  (not b572) )
  :assumption
(or (not b34)  (not b572) )
  :assumption
(or (not b328)  (not b572) )
  :assumption
(or (not b303)  (not b572) )
  :assumption
(or (not b285)  (not b572) )
  :assumption
(or (not b228)  (not b572) )
  :assumption
(or (not b108)  (not b572) )
  :assumption
(or (not b87)  (not b572) )
  :assumption
(or (not b55)  (not b572) )
  :assumption
(or (not b32)  (not b572) )
  :assumption
(or (not b314)  (not b576) )
  :assumption
(or (not b305)  (not b576) )
  :assumption
(or (not b258)  (not b576) )
  :assumption
(or (not b229)  (not b576) )
  :assumption
(or (not b109)  (not b576) )
  :assumption
(or (not b88)  (not b576) )
  :assumption
(or (not b63)  (not b576) )
  :assumption
(or (not b56)  (not b576) )
  :assumption
(or (not b34)  (not b576) )
  :assumption
(or (not b313)  (not b576) )
  :assumption
(or (not b303)  (not b576) )
  :assumption
(or (not b256)  (not b576) )
  :assumption
(or (not b228)  (not b576) )
  :assumption
(or (not b108)  (not b576) )
  :assumption
(or (not b87)  (not b576) )
  :assumption
(or (not b55)  (not b576) )
  :assumption
(or (not b32)  (not b576) )
  :assumption
(or (not b580)  (not b597) )
  :assumption
(or (not b580)  (not b594) )
  :assumption
(or (not b580)  (not b591) )
  :assumption
(or (not b580)  (not b588) )
  :assumption
(or (not b580)  (not b585) )
  :assumption
(or (not b188)  (not b580) )
  :assumption
(or (not b580)  (not b606) )
  :assumption
(or (not b580)  (not b603) )
  :assumption
(or (not b580)  (not b600) )
  :assumption
(or (not b580)  (not b615) )
  :assumption
(or (not b580)  (not b612) )
  :assumption
(or (not b580)  (not b609) )
  :assumption
(or (not b332)  (not b580) )
  :assumption
(or (not b172)  (not b580) )
  :assumption
(or (not b147)  (not b580) )
  :assumption
(or (not b132)  (not b580) )
  :assumption
(or (not b585)  (not b597) )
  :assumption
(or (not b585)  (not b594) )
  :assumption
(or (not b585)  (not b591) )
  :assumption
(or (not b585)  (not b588) )
  :assumption
(or (not b188)  (not b585) )
  :assumption
(or (not b585)  (not b606) )
  :assumption
(or (not b585)  (not b603) )
  :assumption
(or (not b585)  (not b600) )
  :assumption
(or (not b585)  (not b615) )
  :assumption
(or (not b585)  (not b612) )
  :assumption
(or (not b585)  (not b609) )
  :assumption
(or (not b332)  (not b585) )
  :assumption
(or (not b172)  (not b585) )
  :assumption
(or (not b147)  (not b585) )
  :assumption
(or (not b132)  (not b585) )
  :assumption
(or (not b588)  (not b597) )
  :assumption
(or (not b588)  (not b594) )
  :assumption
(or (not b588)  (not b591) )
  :assumption
(or (not b188)  (not b588) )
  :assumption
(or (not b588)  (not b606) )
  :assumption
(or (not b588)  (not b603) )
  :assumption
(or (not b588)  (not b600) )
  :assumption
(or (not b588)  (not b615) )
  :assumption
(or (not b588)  (not b612) )
  :assumption
(or (not b588)  (not b609) )
  :assumption
(or (not b172)  (not b588) )
  :assumption
(or (not b147)  (not b588) )
  :assumption
(or (not b132)  (not b588) )
  :assumption
(or (not b591)  (not b597) )
  :assumption
(or (not b591)  (not b594) )
  :assumption
(or (not b188)  (not b591) )
  :assumption
(or (not b591)  (not b606) )
  :assumption
(or (not b591)  (not b603) )
  :assumption
(or (not b591)  (not b600) )
  :assumption
(or (not b319)  (not b591) )
  :assumption
(or (not b157)  (not b591) )
  :assumption
(or (not b594)  (not b597) )
  :assumption
(or (not b188)  (not b594) )
  :assumption
(or (not b594)  (not b606) )
  :assumption
(or (not b594)  (not b603) )
  :assumption
(or (not b594)  (not b600) )
  :assumption
(or (not b157)  (not b594) )
  :assumption
(or (not b188)  (not b597) )
  :assumption
(or (not b597)  (not b606) )
  :assumption
(or (not b597)  (not b603) )
  :assumption
(or (not b597)  (not b600) )
  :assumption
(or (not b319)  (not b597) )
  :assumption
(or (not b157)  (not b597) )
  :assumption
(or (not b600)  (not b615) )
  :assumption
(or (not b600)  (not b612) )
  :assumption
(or (not b600)  (not b609) )
  :assumption
(or (not b600)  (not b606) )
  :assumption
(or (not b600)  (not b603) )
  :assumption
(or (not b332)  (not b600) )
  :assumption
(or (not b172)  (not b600) )
  :assumption
(or (not b147)  (not b600) )
  :assumption
(or (not b132)  (not b600) )
  :assumption
(or (not b188)  (not b600) )
  :assumption
(or (not b603)  (not b615) )
  :assumption
(or (not b603)  (not b612) )
  :assumption
(or (not b603)  (not b609) )
  :assumption
(or (not b603)  (not b606) )
  :assumption
(or (not b332)  (not b603) )
  :assumption
(or (not b172)  (not b603) )
  :assumption
(or (not b147)  (not b603) )
  :assumption
(or (not b132)  (not b603) )
  :assumption
(or (not b188)  (not b603) )
  :assumption
(or (not b606)  (not b615) )
  :assumption
(or (not b606)  (not b612) )
  :assumption
(or (not b606)  (not b609) )
  :assumption
(or (not b172)  (not b606) )
  :assumption
(or (not b147)  (not b606) )
  :assumption
(or (not b132)  (not b606) )
  :assumption
(or (not b188)  (not b606) )
  :assumption
(or (not b609)  (not b615) )
  :assumption
(or (not b609)  (not b612) )
  :assumption
(or (not b332)  (not b609) )
  :assumption
(or (not b172)  (not b609) )
  :assumption
(or (not b147)  (not b609) )
  :assumption
(or (not b132)  (not b609) )
  :assumption
(or (not b319)  (not b609) )
  :assumption
(or (not b157)  (not b609) )
  :assumption
(or (not b612)  (not b615) )
  :assumption
(or (not b332)  (not b612) )
  :assumption
(or (not b172)  (not b612) )
  :assumption
(or (not b147)  (not b612) )
  :assumption
(or (not b132)  (not b612) )
  :assumption
(or (not b157)  (not b612) )
  :assumption
(or (not b172)  (not b615) )
  :assumption
(or (not b147)  (not b615) )
  :assumption
(or (not b132)  (not b615) )
  :assumption
(or (not b319)  (not b615) )
  :assumption
(or (not b157)  (not b615) )
  :assumption
(or (not b619)  (not b632) )
  :assumption
(or (not b619)  (not b628) )
  :assumption
(or (not b619)  (not b623) )
  :assumption
(or (not b334)  (not b619) )
  :assumption
(or (not b290)  (not b619) )
  :assumption
(or (not b230)  (not b619) )
  :assumption
(or (not b110)  (not b619) )
  :assumption
(or (not b89)  (not b619) )
  :assumption
(or (not b68)  (not b619) )
  :assumption
(or (not b57)  (not b619) )
  :assumption
(or (not b36)  (not b619) )
  :assumption
(or (not b623)  (not b632) )
  :assumption
(or (not b623)  (not b628) )
  :assumption
(or (not b318)  (not b623) )
  :assumption
(or (not b261)  (not b623) )
  :assumption
(or (not b230)  (not b623) )
  :assumption
(or (not b110)  (not b623) )
  :assumption
(or (not b89)  (not b623) )
  :assumption
(or (not b68)  (not b623) )
  :assumption
(or (not b57)  (not b623) )
  :assumption
(or (not b36)  (not b623) )
  :assumption
(or (not b628)  (not b632) )
  :assumption
(or (not b334)  (not b628) )
  :assumption
(or (not b290)  (not b628) )
  :assumption
(or (not b230)  (not b628) )
  :assumption
(or (not b110)  (not b628) )
  :assumption
(or (not b89)  (not b628) )
  :assumption
(or (not b68)  (not b628) )
  :assumption
(or (not b57)  (not b628) )
  :assumption
(or (not b36)  (not b628) )
  :assumption
(or (not b318)  (not b632) )
  :assumption
(or (not b261)  (not b632) )
  :assumption
(or (not b230)  (not b632) )
  :assumption
(or (not b110)  (not b632) )
  :assumption
(or (not b89)  (not b632) )
  :assumption
(or (not b68)  (not b632) )
  :assumption
(or (not b57)  (not b632) )
  :assumption
(or (not b36)  (not b632) )
  :assumption
(or (not b636)  (not b646) )
  :assumption
(or (not b641)  (not b649) )
  :assumption
(or (not b636)  (not b716) )
  :assumption
(or (not b641)  (not b719) )
  :assumption
(or (not b636)  (not b686) )
  :assumption
(or (not b641)  (not b689) )
  :assumption
(or (not b636)  (not b695) )
  :assumption
(or (not b641)  (not b698) )
  :assumption
(or (not b646)  (not b716) )
  :assumption
(or (not b649)  (not b719) )
  :assumption
(or (not b646)  (not b686) )
  :assumption
(or (not b649)  (not b689) )
  :assumption
(or (not b653)  (not b670) )
  :assumption
(or (not b658)  (not b673) )
  :assumption
(or (not b662)  (not b676) )
  :assumption
(or (not b666)  (not b679) )
  :assumption
(or (not b653)  (not b704) )
  :assumption
(or (not b658)  (not b707) )
  :assumption
(or (not b662)  (not b710) )
  :assumption
(or (not b666)  (not b713) )
  :assumption
(or (not b658)  (not b692) )
  :assumption
(or (not b662)  (not b695) )
  :assumption
(or (not b666)  (not b698) )
  :assumption
(or (not b658)  (not b683) )
  :assumption
(or (not b662)  (not b686) )
  :assumption
(or (not b666)  (not b689) )
  :assumption
(or (not b670)  (not b704) )
  :assumption
(or (not b673)  (not b707) )
  :assumption
(or (not b676)  (not b710) )
  :assumption
(or (not b679)  (not b713) )
  :assumption
(or (not b673)  (not b692) )
  :assumption
(or (not b676)  (not b695) )
  :assumption
(or (not b679)  (not b698) )
  :assumption
(or (not b683)  (not b692) )
  :assumption
(or (not b686)  (not b695) )
  :assumption
(or (not b689)  (not b698) )
  :assumption
(or (not b722)  (not b740) )
  :assumption
(or (not b727)  (not b743) )
  :assumption
(or (not b731)  (not b746) )
  :assumption
(or (not b735)  (not b749) )
  :assumption
(or (not b727)  (not b822) )
  :assumption
(or (not b731)  (not b825) )
  :assumption
(or (not b722)  (not b786) )
  :assumption
(or (not b727)  (not b789) )
  :assumption
(or (not b731)  (not b792) )
  :assumption
(or (not b735)  (not b795) )
  :assumption
(or (not b722)  (not b801) )
  :assumption
(or (not b727)  (not b804) )
  :assumption
(or (not b731)  (not b807) )
  :assumption
(or (not b735)  (not b810) )
  :assumption
(or (not b743)  (not b822) )
  :assumption
(or (not b746)  (not b825) )
  :assumption
(or (not b740)  (not b786) )
  :assumption
(or (not b743)  (not b789) )
  :assumption
(or (not b746)  (not b792) )
  :assumption
(or (not b749)  (not b795) )
  :assumption
(or (not b752)  (not b769) )
  :assumption
(or (not b757)  (not b772) )
  :assumption
(or (not b761)  (not b775) )
  :assumption
(or (not b765)  (not b778) )
  :assumption
(or (not b757)  (not b813) )
  :assumption
(or (not b761)  (not b816) )
  :assumption
(or (not b765)  (not b819) )
  :assumption
(or (not b752)  (not b801) )
  :assumption
(or (not b757)  (not b804) )
  :assumption
(or (not b761)  (not b807) )
  :assumption
(or (not b765)  (not b810) )
  :assumption
(or (not b752)  (not b786) )
  :assumption
(or (not b757)  (not b789) )
  :assumption
(or (not b761)  (not b792) )
  :assumption
(or (not b765)  (not b795) )
  :assumption
(or (not b772)  (not b813) )
  :assumption
(or (not b775)  (not b816) )
  :assumption
(or (not b778)  (not b819) )
  :assumption
(or (not b769)  (not b801) )
  :assumption
(or (not b772)  (not b804) )
  :assumption
(or (not b775)  (not b807) )
  :assumption
(or (not b778)  (not b810) )
  :assumption
(or (not b782)  (not b798) )
  :assumption
(or (not b786)  (not b801) )
  :assumption
(or (not b789)  (not b804) )
  :assumption
(or (not b792)  (not b807) )
  :assumption
(or (not b795)  (not b810) )
  :assumption
(or (not b829)  (not b847) )
  :assumption
(or (not b834)  (not b850) )
  :assumption
(or (not b838)  (not b853) )
  :assumption
(or (not b842)  (not b856) )
  :assumption
(or (not b834)  (not b927) )
  :assumption
(or (not b838)  (not b930) )
  :assumption
(or (not b842)  (not b933) )
  :assumption
(or (not b829)  (not b893) )
  :assumption
(or (not b834)  (not b896) )
  :assumption
(or (not b838)  (not b899) )
  :assumption
(or (not b842)  (not b902) )
  :assumption
(or (not b829)  (not b908) )
  :assumption
(or (not b834)  (not b911) )
  :assumption
(or (not b838)  (not b914) )
  :assumption
(or (not b842)  (not b917) )
  :assumption
(or (not b850)  (not b927) )
  :assumption
(or (not b853)  (not b930) )
  :assumption
(or (not b856)  (not b933) )
  :assumption
(or (not b847)  (not b893) )
  :assumption
(or (not b850)  (not b896) )
  :assumption
(or (not b853)  (not b899) )
  :assumption
(or (not b856)  (not b902) )
  :assumption
(or (not b860)  (not b877) )
  :assumption
(or (not b865)  (not b880) )
  :assumption
(or (not b869)  (not b883) )
  :assumption
(or (not b873)  (not b886) )
  :assumption
(or (not b865)  (not b920) )
  :assumption
(or (not b869)  (not b923) )
  :assumption
(or (not b860)  (not b908) )
  :assumption
(or (not b865)  (not b911) )
  :assumption
(or (not b869)  (not b914) )
  :assumption
(or (not b873)  (not b917) )
  :assumption
(or (not b860)  (not b893) )
  :assumption
(or (not b865)  (not b896) )
  :assumption
(or (not b869)  (not b899) )
  :assumption
(or (not b873)  (not b902) )
  :assumption
(or (not b880)  (not b920) )
  :assumption
(or (not b883)  (not b923) )
  :assumption
(or (not b877)  (not b908) )
  :assumption
(or (not b880)  (not b911) )
  :assumption
(or (not b883)  (not b914) )
  :assumption
(or (not b886)  (not b917) )
  :assumption
(or (not b889)  (not b905) )
  :assumption
(or (not b893)  (not b908) )
  :assumption
(or (not b896)  (not b911) )
  :assumption
(or (not b899)  (not b914) )
  :assumption
(or (not b902)  (not b917) )
  :assumption
(= r2 0)
  :assumption
(= r4 r5)
  :assumption
(= (- r6 r2) 1)
  :assumption
(= r183 0)
  :assumption
(= (- r7 r6) 1)
  :assumption
(= (- r9 r7) 1)
  :assumption
(= (- r10 r9) 1)
  :assumption
(= (- r5 r10) 1)
  :assumption
(= (- (- (- (- (- (- r64 r12) r53) r48) r21) r16) r65) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r66 r64) r54) r49) r44) r40) r36) r32) r22) r17) r1) r67) r68) r69) r70) r71) r72) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r73 r66) r61) r58) r55) r50) r45) r41) r37) r33) r29) r26) r23) r18) r3) r74) r75) r76) r77) r78) r79) r80) r81) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r82 r73) r62) r59) r56) r51) r46) r42) r38) r34) r30) r27) r24) r19) r8) r83) r84) r85) r86) r87) r88) r89) r90) r91) r92) r93) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r15 r82) r63) r60) r57) r52) r47) r43) r39) r35) r31) r28) r25) r20) r11) r94) r95) r96) r97) r98) r99) r100) r101) r102) r103) r104) 0)
  :assumption
(= (- r105 r13) 0)
  :assumption
(= (- (- (- (- (- r106 r105) r107) r108) r109) r110) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r111 r106) r112) r113) r114) r115) r116) r117) r118) r119) r120) r121) r122) r123) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r124 r111) r125) r126) r127) r128) r129) r130) r131) r132) r133) r134) r135) r136) r137) r138) r139) r140) r141) r142) r143) r144) r145) r146) r147) r148) r149) r150) r151) r152) r153) r154) r155) r156) r157) r158) r159) r160) r161) r162) r163) r164) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r14 r124) r165) r166) r167) r168) r169) r170) r171) r172) r173) r174) r175) r176) r177) r178) r179) r180) r181) r182) r183) r184) r185) r186) r187) r188) r189) r190) r191) r192) r193) r194) r195) r196) r197) r198) r199) r200) r201) r202) r203) r204) r205) r206) r207) r208) r209) r210) r211) r212) r213) r214) r215) r216) r217) r218) 0)
  :assumption
(= r170 0)
  :assumption
(= r169 0)
  :assumption
(= r168 0)
  :assumption
(= r167 0)
  :assumption
(= r166 0)
  :assumption
(= r165 0)
  :assumption
(= r12 0)
  :assumption
(= r13 0)
  :assumption
(<= (+ (+ (* 3 r4) (* 2 r14)) (* 4 r15)) 965)
  :assumption
(= r31 0)
  :assumption
(= r60 0)
  :assumption
(= r218 0)
  :assumption
(= r217 0)
  :assumption
(= r216 0)
  :assumption
(= r215 0)
  :assumption
(= r214 0)
  :assumption
(= r213 0)
  :assumption
(= r188 0)
  :assumption
(= r187 0)
  :assumption
(= r186 0)
  :assumption
(= r185 0)
  :assumption
(= r184 0)
  :formula
(not false)
)