(benchmark p4_zenonumeric_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 unknown :logic QF_LRA :extrapreds ((b15)) :extrapreds ((b20)) :extrapreds ((b26)) :extrapreds ((b32)) :extrapreds ((b40)) :extrapreds ((b46)) :extrapreds ((b51)) :extrapreds ((b56)) :extrapreds ((b62)) :extrapreds ((b67)) :extrapreds ((b72)) :extrapreds ((b76)) :extrapreds ((b81)) :extrapreds ((b86)) :extrapreds ((b93)) :extrapreds ((b97)) :extrapreds ((b101)) :extrapreds ((b105)) :extrapreds ((b109)) :extrapreds ((b113)) :extrapreds ((b117)) :extrapreds ((b123)) :extrapreds ((b129)) :extrapreds ((b135)) :extrapreds ((b141)) :extrapreds ((b146)) :extrapreds ((b150)) :extrapreds ((b154)) :extrapreds ((b158)) :extrapreds ((b163)) :extrapreds ((b167)) :extrapreds ((b172)) :extrapreds ((b176)) :extrapreds ((b179)) :extrapreds ((b182)) :extrapreds ((b188)) :extrapreds ((b193)) :extrapreds ((b198)) :extrapreds ((b202)) :extrapreds ((b207)) :extrapreds ((b212)) :extrapreds ((b217)) :extrapreds ((b221)) :extrapreds ((b225)) :extrapreds ((b228)) :extrapreds ((b231)) :extrapreds ((b235)) :extrapreds ((b239)) :extrapreds ((b243)) :extrapreds ((b251)) :extrapreds ((b257)) :extrapreds ((b262)) :extrapreds ((b266)) :extrapreds ((b270)) :extrapreds ((b275)) :extrapreds ((b279)) :extrapreds ((b285)) :extrapreds ((b290)) :extrapreds ((b294)) :extrapreds ((b297)) :extrapreds ((b300)) :extrapreds ((b303)) :extrapreds ((b306)) :extrapreds ((b312)) :extrapreds ((b317)) :extrapreds ((b322)) :extrapreds ((b326)) :extrapreds ((b331)) :extrapreds ((b336)) :extrapreds ((b340)) :extrapreds ((b344)) :extrapreds ((b348)) :extrapreds ((b352)) :extrapreds ((b355)) :extrapreds ((b358)) :extrapreds ((b362)) :extrapreds ((b366)) :extrapreds ((b369)) :extrapreds ((b372)) :extrapreds ((b375)) :extrapreds ((b378)) :extrapreds ((b381)) :extrapreds ((b384)) :extrapreds ((b387)) :extrapreds ((b390)) :extrapreds ((b393)) :extrapreds ((b396)) :extrapreds ((b399)) :extrapreds ((b402)) :extrapreds ((b405)) :extrapreds ((b408)) :extrapreds ((b411)) :extrapreds ((b414)) :extrapreds ((b417)) :extrapreds ((b420)) :extrapreds ((b423)) :extrapreds ((b426)) :extrapreds ((b429)) :extrapreds ((b432)) :extrapreds ((b435)) :extrapreds ((b438)) :extrapreds ((b441)) :extrapreds ((b444)) :extrapreds ((b447)) :extrapreds ((b450)) :extrapreds ((b453)) :extrapreds ((b456)) :extrapreds ((b459)) :extrapreds ((b462)) :extrapreds ((b465)) :extrapreds ((b468)) :extrapreds ((b471)) :extrapreds ((b474)) :extrapreds ((b477)) :extrapreds ((b480)) :extrapreds ((b483)) :extrapreds ((b486)) :extrapreds ((b489)) :extrapreds ((b492)) :extrapreds ((b495)) :extrapreds ((b498)) :extrapreds ((b501)) :extrapreds ((b504)) :extrapreds ((b507)) :extrapreds ((b510)) :extrapreds ((b513)) :extrapreds ((b516)) :extrapreds ((b519)) :extrapreds ((b522)) :extrapreds ((b525)) :extrapreds ((b528)) :extrapreds ((b531)) :extrapreds ((b534)) :extrapreds ((b537)) :extrapreds ((b540)) :extrapreds ((b543)) :extrapreds ((b546)) :extrapreds ((b549)) :extrapreds ((b552)) :extrapreds ((b555)) :extrapreds ((b558)) :extrapreds ((b561)) :extrapreds ((b564)) :extrapreds ((b567)) :extrapreds ((b570)) :extrapreds ((b573)) :extrapreds ((b576)) :extrapreds ((b579)) :extrapreds ((b582)) :extrapreds ((b585)) :extrapreds ((b588)) :extrapreds ((b591)) :extrapreds ((b594)) :extrapreds ((b597)) :extrapreds ((b600)) :extrapreds ((b603)) :extrapreds ((b606)) :extrapreds ((b609)) :extrapreds ((b612)) :extrapreds ((b615)) :extrapreds ((b618)) :extrapreds ((b621)) :extrapreds ((b624)) :extrapreds ((b627)) :extrapreds ((b630)) :extrapreds ((b633)) :extrapreds ((b636)) :extrapreds ((b639)) :extrapreds ((b642)) :extrapreds ((b645)) :extrapreds ((b648)) :extrapreds ((b651)) :extrapreds ((b654)) :extrapreds ((b657)) :extrapreds ((b660)) :extrapreds ((b666)) :extrapreds ((b672)) :extrapreds ((b678)) :extrapreds ((b684)) :extrapreds ((b692)) :extrapreds ((b698)) :extrapreds ((b704)) :extrapreds ((b710)) :extrapreds ((b716)) :extrapreds ((b723)) :extrapreds ((b728)) :extrapreds ((b733)) :extrapreds ((b738)) :extrapreds ((b743)) :extrapreds ((b749)) :extrapreds ((b755)) :extrapreds ((b761)) :extrapreds ((b767)) :extrapreds ((b772)) :extrapreds ((b777)) :extrapreds ((b782)) :extrapreds ((b787)) :extrapreds ((b792)) :extrapreds ((b797)) :extrapreds ((b802)) :extrapreds ((b807)) :extrapreds ((b813)) :extrapreds ((b819)) :extrapreds ((b825)) :extrapreds ((b831)) :extrapreds ((b839)) :extrapreds ((b845)) :extrapreds ((b851)) :extrapreds ((b857)) :extrapreds ((b863)) :extrapreds ((b869)) :extrapreds ((b874)) :extrapreds ((b879)) :extrapreds ((b884)) :extrapreds ((b889)) :extrapreds ((b895)) :extrapreds ((b901)) :extrapreds ((b907)) :extrapreds ((b913)) :extrapreds ((b918)) :extrapreds ((b923)) :extrapreds ((b930)) :extrapreds ((b935)) :extrapreds ((b940)) :extrapreds ((b947)) :extrapreds ((b954)) :extrapreds ((b961)) :extrapreds ((b968)) :extrapreds ((b975)) :extrapreds ((b982)) :extrapreds ((b988)) :extrapreds ((b994)) :extrapreds ((b1000)) :extrapreds ((b1006)) :extrapreds ((b1012)) :extrapreds ((b1017)) :extrapreds ((b1022)) :extrapreds ((b1027)) :extrapreds ((b1032)) :extrapreds ((b1038)) :extrapreds ((b1044)) :extrapreds ((b1050)) :extrapreds ((b1056)) :extrapreds ((b1061)) :extrapreds ((b1066)) :extrapreds ((b1071)) :extrapreds ((b1076)) :extrapreds ((b1081)) :extrapreds ((b1086)) :extrapreds ((b1091)) :extrapreds ((b1096)) :extrapreds ((b1103)) :extrapreds ((b1110)) :extrapreds ((b1117)) :extrapreds ((b1124)) :extrapreds ((b1131)) :extrapreds ((b1137)) :extrapreds ((b1143)) :extrapreds ((b1149)) :extrapreds ((b1155)) :extrapreds ((b1161)) :extrapreds ((b1166)) :extrapreds ((b1171)) :extrapreds ((b1176)) :extrapreds ((b1181)) :extrapreds ((b1187)) :extrapreds ((b1193)) :extrapreds ((b1199)) :extrapreds ((b1205)) :extrapreds ((b1210)) :extrapreds ((b1215)) :extrapreds ((b1222)) :extrapreds ((b1227)) :extrapreds ((b1232)) :extrapreds ((b1238)) :extrapreds ((b1241)) :extrapreds ((b1244)) :extrapreds ((b1247)) :extrapreds ((b1250)) :extrapreds ((b1253)) :extrapreds ((b1254)) :extrapreds ((b1255)) :extrapreds ((b1256)) :extrapreds ((b1257)) :extrapreds ((b1258)) :extrapreds ((b1259)) :extrapreds ((b1260)) :extrapreds ((b1261)) :extrapreds ((b1264)) :extrapreds ((b1267)) :extrapreds ((b1270)) :extrapreds ((b1273)) :extrapreds ((b1276)) :extrapreds ((b1277)) :extrapreds ((b1278)) :extrapreds ((b1279)) :extrapreds ((b1280)) :extrapreds ((b1281)) :extrapreds ((b1282)) :extrapreds ((b1283)) :extrapreds ((b17)) :extrapreds ((b18)) :extrapreds ((b22)) :extrapreds ((b23)) :extrapreds ((b24)) :extrapreds ((b28)) :extrapreds ((b29)) :extrapreds ((b30)) :extrapreds ((b34)) :extrapreds ((b35)) :extrapreds ((b36)) :extrapreds ((b38)) :extrapreds ((b42)) :extrapreds ((b43)) :extrapreds ((b44)) :extrapreds ((b48)) :extrapreds ((b49)) :extrapreds ((b53)) :extrapreds ((b54)) :extrapreds ((b58)) :extrapreds ((b59)) :extrapreds ((b60)) :extrapreds ((b64)) :extrapreds ((b65)) :extrapreds ((b69)) :extrapreds ((b70)) :extrapreds ((b74)) :extrapreds ((b78)) :extrapreds ((b79)) :extrapreds ((b83)) :extrapreds ((b84)) :extrapreds ((b88)) :extrapreds ((b89)) :extrapreds ((b91)) :extrapreds ((b95)) :extrapreds ((b99)) :extrapreds ((b103)) :extrapreds ((b107)) :extrapreds ((b111)) :extrapreds ((b115)) :extrapreds ((b119)) :extrapreds ((b120)) :extrapreds ((b121)) :extrapreds ((b125)) :extrapreds ((b126)) :extrapreds ((b127)) :extrapreds ((b131)) :extrapreds ((b132)) :extrapreds ((b137)) :extrapreds ((b138)) :extrapreds ((b139)) :extrapreds ((b143)) :extrapreds ((b144)) :extrapreds ((b148)) :extrapreds ((b152)) :extrapreds ((b156)) :extrapreds ((b160)) :extrapreds ((b161)) :extrapreds ((b169)) :extrapreds ((b170)) :extrapreds ((b174)) :extrapreds ((b184)) :extrapreds ((b185)) :extrapreds ((b186)) :extrapreds ((b190)) :extrapreds ((b191)) :extrapreds ((b195)) :extrapreds ((b196)) :extrapreds ((b200)) :extrapreds ((b204)) :extrapreds ((b205)) :extrapreds ((b209)) :extrapreds ((b210)) :extrapreds ((b214)) :extrapreds ((b219)) :extrapreds ((b223)) :extrapreds ((b233)) :extrapreds ((b237)) :extrapreds ((b245)) :extrapreds ((b246)) :extrapreds ((b247)) :extrapreds ((b249)) :extrapreds ((b253)) :extrapreds ((b254)) :extrapreds ((b255)) :extrapreds ((b259)) :extrapreds ((b260)) :extrapreds ((b264)) :extrapreds ((b268)) :extrapreds ((b272)) :extrapreds ((b273)) :extrapreds ((b277)) :extrapreds ((b281)) :extrapreds ((b283)) :extrapreds ((b287)) :extrapreds ((b288)) :extrapreds ((b292)) :extrapreds ((b308)) :extrapreds ((b309)) :extrapreds ((b310)) :extrapreds ((b314)) :extrapreds ((b315)) :extrapreds ((b319)) :extrapreds ((b320)) :extrapreds ((b324)) :extrapreds ((b328)) :extrapreds ((b329)) :extrapreds ((b333)) :extrapreds ((b334)) :extrapreds ((b338)) :extrapreds ((b342)) :extrapreds ((b346)) :extrapreds ((b350)) :extrapreds ((b360)) :extrapreds ((b364)) :extrapreds ((b688)) :extrapreds ((b689)) :extrapreds ((b720)) :extrapreds ((b835)) :extrapreds ((b836)) :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)) :extrafuns ((r219 Real)) :extrafuns ((r220 Real)) :extrafuns ((r221 Real)) :extrafuns ((r222 Real)) :extrafuns ((r223 Real)) :extrafuns ((r224 Real)) :extrafuns ((r225 Real)) :extrafuns ((r226 Real)) :extrafuns ((r227 Real)) :extrafuns ((r228 Real)) :extrafuns ((r229 Real)) :extrafuns ((r230 Real)) :extrafuns ((r231 Real)) :extrafuns ((r232 Real)) :extrafuns ((r233 Real)) :extrafuns ((r234 Real)) :extrafuns ((r235 Real)) :extrafuns ((r236 Real)) :extrafuns ((r237 Real)) :extrafuns ((r238 Real)) :extrafuns ((r239 Real)) :extrafuns ((r240 Real)) :extrafuns ((r241 Real)) :extrafuns ((r242 Real)) :extrafuns ((r243 Real)) :extrafuns ((r244 Real)) :extrafuns ((r245 Real)) :extrafuns ((r246 Real)) :extrafuns ((r247 Real)) :extrafuns ((r248 Real)) :extrafuns ((r249 Real)) :extrafuns ((r250 Real)) :extrafuns ((r251 Real)) :extrafuns ((r252 Real)) :extrafuns ((r253 Real)) :extrafuns ((r254 Real)) :extrafuns ((r255 Real)) :extrafuns ((r256 Real)) :extrafuns ((r257 Real)) :extrafuns ((r258 Real)) :extrafuns ((r259 Real)) :extrafuns ((r260 Real)) :extrafuns ((r261 Real)) :extrafuns ((r262 Real)) :extrafuns ((r263 Real)) :extrafuns ((r264 Real)) :extrafuns ((r265 Real)) :extrafuns ((r266 Real)) :extrafuns ((r267 Real)) :extrafuns ((r268 Real)) :extrafuns ((r269 Real)) :extrafuns ((r270 Real)) :extrafuns ((r271 Real)) :extrafuns ((r272 Real)) :extrafuns ((r273 Real)) :extrafuns ((r274 Real)) :extrafuns ((r275 Real)) :extrafuns ((r276 Real)) :extrafuns ((r277 Real)) :extrafuns ((r278 Real)) :extrafuns ((r279 Real)) :extrafuns ((r280 Real)) :extrafuns ((r281 Real)) :extrafuns ((r282 Real)) :extrafuns ((r283 Real)) :extrafuns ((r284 Real)) :extrafuns ((r285 Real)) :extrafuns ((r286 Real)) :extrafuns ((r287 Real)) :extrafuns ((r288 Real)) :extrafuns ((r289 Real)) :extrafuns ((r290 Real)) :extrafuns ((r291 Real)) :extrafuns ((r292 Real)) :extrafuns ((r293 Real)) :extrafuns ((r294 Real)) :extrafuns ((r295 Real)) :extrafuns ((r296 Real)) :extrafuns ((r297 Real)) :extrafuns ((r298 Real)) :extrafuns ((r299 Real)) :extrafuns ((r300 Real)) :extrafuns ((r301 Real)) :extrafuns ((r302 Real)) :extrafuns ((r303 Real)) :extrafuns ((r304 Real)) :extrafuns ((r305 Real)) :extrafuns ((r306 Real)) :extrafuns ((r307 Real)) :extrafuns ((r308 Real)) :extrafuns ((r309 Real)) :extrafuns ((r310 Real)) :extrafuns ((r311 Real)) :extrafuns ((r312 Real)) :extrafuns ((r313 Real)) :extrafuns ((r314 Real)) :extrafuns ((r315 Real)) :extrafuns ((r316 Real)) :extrafuns ((r317 Real)) :extrafuns ((r318 Real)) :extrafuns ((r319 Real)) :extrafuns ((r320 Real)) :extrafuns ((r321 Real)) :extrafuns ((r322 Real)) :extrafuns ((r323 Real)) :extrafuns ((r324 Real)) :extrafuns ((r325 Real)) :extrafuns ((r326 Real)) :extrafuns ((r327 Real)) :extrafuns ((r328 Real)) :extrafuns ((r329 Real)) :extrafuns ((r330 Real)) :extrafuns ((r331 Real)) :extrafuns ((r332 Real)) :extrafuns ((r333 Real)) :extrafuns ((r334 Real)) :extrafuns ((r335 Real)) :extrafuns ((r336 Real)) :extrafuns ((r337 Real)) :extrafuns ((r338 Real)) :extrafuns ((r339 Real)) :extrafuns ((r340 Real)) :extrafuns ((r341 Real)) :extrafuns ((r342 Real)) :extrafuns ((r343 Real)) :extrafuns ((r344 Real)) :extrafuns ((r345 Real)) :extrafuns ((r346 Real)) :extrafuns ((r347 Real)) :extrafuns ((r348 Real)) :extrafuns ((r349 Real)) :extrafuns ((r350 Real)) :extrafuns ((r351 Real)) :extrafuns ((r352 Real)) :extrafuns ((r353 Real)) :extrafuns ((r354 Real)) :extrafuns ((r355 Real)) :extrafuns ((r356 Real)) :extrafuns ((r357 Real)) :extrafuns ((r358 Real)) :extrafuns ((r359 Real)) :extrafuns ((r360 Real)) :extrafuns ((r361 Real)) :extrafuns ((r362 Real)) :extrafuns ((r363 Real)) :extrafuns ((r364 Real)) :extrafuns ((r365 Real)) :extrafuns ((r366 Real)) :extrafuns ((r367 Real)) :extrafuns ((r368 Real)) :extrafuns ((r369 Real)) :extrafuns ((r370 Real)) :extrafuns ((r371 Real)) :extrafuns ((r372 Real)) :extrafuns ((r373 Real)) :extrafuns ((r374 Real)) :extrafuns ((r375 Real)) :extrafuns ((r376 Real)) :extrafuns ((r377 Real)) :extrafuns ((r378 Real)) :extrafuns ((r379 Real)) :extrafuns ((r380 Real)) :extrafuns ((r381 Real)) :extrafuns ((r382 Real)) :extrafuns ((r383 Real)) :extrafuns ((r384 Real)) :extrafuns ((r385 Real)) :extrafuns ((r386 Real)) :extrafuns ((r387 Real)) :extrafuns ((r388 Real)) :extrafuns ((r389 Real)) :extrafuns ((r390 Real)) :extrafuns ((r391 Real)) :extrafuns ((r392 Real)) :extrafuns ((r393 Real)) :extrafuns ((r394 Real)) :extrafuns ((r395 Real)) :extrafuns ((r396 Real)) :extrafuns ((r397 Real)) :extrafuns ((r398 Real)) :extrafuns ((r399 Real)) :extrafuns ((r400 Real)) :extrafuns ((r401 Real)) :extrafuns ((r402 Real)) :extrafuns ((r403 Real)) :extrafuns ((r404 Real)) :extrafuns ((r405 Real)) :extrafuns ((r406 Real)) :extrafuns ((r407 Real)) :extrafuns ((r408 Real)) :extrafuns ((r409 Real)) :extrafuns ((r410 Real)) :extrafuns ((r411 Real)) :extrafuns ((r412 Real)) :extrafuns ((r413 Real)) :extrafuns ((r414 Real)) :extrafuns ((r415 Real)) :extrafuns ((r416 Real)) :extrafuns ((r417 Real)) :extrafuns ((r418 Real)) :extrafuns ((r419 Real)) :extrafuns ((r420 Real)) :extrafuns ((r421 Real)) :extrafuns ((r422 Real)) :extrafuns ((r423 Real)) :extrafuns ((r424 Real)) :extrafuns ((r425 Real)) :extrafuns ((r426 Real)) :extrafuns ((r427 Real)) :extrafuns ((r428 Real)) :assumption (or (= r14 0) b15 ) :assumption (or (not b15) (= r14 1) ) :assumption (or (not b15) b17 ) :assumption (or (not b15) (not b18) ) :assumption (or (= r15 0) b20 ) :assumption (or (not b20) (= r15 1) ) :assumption (or (not b20) b22 ) :assumption (or (not b20) (not b23) ) :assumption (or b18 (not b20) ) :assumption (or (not b20) b24 ) :assumption (or (= r16 0) b26 ) :assumption (or (not b26) (= r16 1) ) :assumption (or (not b26) b28 ) :assumption (or (not b26) (not b29) ) :assumption (or b23 (not b26) ) :assumption (or (not b26) b30 ) :assumption (or (= r17 0) b32 ) :assumption (or (not b32) (= r17 1) ) :assumption (or (not b32) b34 ) :assumption (or (not b32) (not b35) ) :assumption (or b29 (not b32) ) :assumption (or (not b32) b36 ) :assumption (or (= r19 0) b40 ) :assumption (or (not b40) (= r19 1) ) :assumption (or b28 (not b40) ) :assumption (or (not b40) (not b42) ) :assumption (or (not b40) b43 ) :assumption (or (not b40) b44 ) :assumption (or (= r20 0) b46 ) :assumption (or (not b46) (= r20 1) ) :assumption (or b34 (not b46) ) :assumption (or (not b46) (not b48) ) :assumption (or b42 (not b46) ) :assumption (or (not b46) b49 ) :assumption (or (= r21 0) b51 ) :assumption (or (not b51) (= r21 1) ) :assumption (or b38 (not b51) ) :assumption (or (not b51) (not b53) ) :assumption (or b48 (not b51) ) :assumption (or (not b51) b54 ) :assumption (or (= r22 0) b56 ) :assumption (or (not b56) (= r22 1) ) :assumption (or b28 (not b56) ) :assumption (or (not b56) (not b58) ) :assumption (or (not b56) b59 ) :assumption (or (not b56) b60 ) :assumption (or (= r23 0) b62 ) :assumption (or (not b62) (= r23 1) ) :assumption (or b34 (not b62) ) :assumption (or (not b62) (not b64) ) :assumption (or b58 (not b62) ) :assumption (or (not b62) b65 ) :assumption (or (= r24 0) b67 ) :assumption (or (not b67) (= r24 1) ) :assumption (or b38 (not b67) ) :assumption (or (not b67) (not b69) ) :assumption (or b64 (not b67) ) :assumption (or (not b67) b70 ) :assumption (or (= r25 0) b72 ) :assumption (or (not b72) (= r25 1) ) :assumption (or (not b72) b74 ) :assumption (or (not b18) (not b72) ) :assumption (or (= r26 0) b76 ) :assumption (or (not b76) (= r26 1) ) :assumption (or (not b76) b78 ) :assumption (or (not b23) (not b76) ) :assumption (or b18 (not b76) ) :assumption (or (not b76) b79 ) :assumption (or (= r27 0) b81 ) :assumption (or (not b81) (= r27 1) ) :assumption (or (not b81) b83 ) :assumption (or (not b29) (not b81) ) :assumption (or b23 (not b81) ) :assumption (or (not b81) b84 ) :assumption (or (= r28 0) b86 ) :assumption (or (not b86) (= r28 1) ) :assumption (or (not b86) b88 ) :assumption (or (not b35) (not b86) ) :assumption (or b29 (not b86) ) :assumption (or (not b86) b89 ) :assumption (or (= r30 0) b93 ) :assumption (or (not b93) (= r30 1) ) :assumption (or b83 (not b93) ) :assumption (or (not b42) (not b93) ) :assumption (or b43 (not b93) ) :assumption (or (not b93) b95 ) :assumption (or (= r31 0) b97 ) :assumption (or (not b97) (= r31 1) ) :assumption (or b88 (not b97) ) :assumption (or (not b48) (not b97) ) :assumption (or b42 (not b97) ) :assumption (or (not b97) b99 ) :assumption (or (= r32 0) b101 ) :assumption (or (not b101) (= r32 1) ) :assumption (or b91 (not b101) ) :assumption (or (not b53) (not b101) ) :assumption (or b48 (not b101) ) :assumption (or (not b101) b103 ) :assumption (or (= r33 0) b105 ) :assumption (or (not b105) (= r33 1) ) :assumption (or b83 (not b105) ) :assumption (or (not b58) (not b105) ) :assumption (or b59 (not b105) ) :assumption (or (not b105) b107 ) :assumption (or (= r34 0) b109 ) :assumption (or (not b109) (= r34 1) ) :assumption (or b88 (not b109) ) :assumption (or (not b64) (not b109) ) :assumption (or b58 (not b109) ) :assumption (or (not b109) b111 ) :assumption (or (= r35 0) b113 ) :assumption (or (not b113) (= r35 1) ) :assumption (or b91 (not b113) ) :assumption (or (not b69) (not b113) ) :assumption (or b64 (not b113) ) :assumption (or (not b113) b115 ) :assumption (or (= r36 0) b117 ) :assumption (or (not b117) (= r36 1) ) :assumption (or (not b117) b119 ) :assumption (or (not b117) (not b120) ) :assumption (or (not b117) b121 ) :assumption (or b36 (not b117) ) :assumption (or (= r37 0) b123 ) :assumption (or (not b123) (= r37 1) ) :assumption (or (not b123) b125 ) :assumption (or (not b123) (not b126) ) :assumption (or b120 (not b123) ) :assumption (or (not b123) b127 ) :assumption (or (= r38 0) b129 ) :assumption (or (not b129) (= r38 1) ) :assumption (or b119 (not b129) ) :assumption (or (not b129) (not b131) ) :assumption (or (not b129) b132 ) :assumption (or b49 (not b129) ) :assumption (or (= r40 0) b135 ) :assumption (or (not b135) (= r40 1) ) :assumption (or (not b135) b137 ) :assumption (or (not b135) (not b138) ) :assumption (or (not b135) b139 ) :assumption (or (= r41 0) b141 ) :assumption (or (not b141) (= r41 1) ) :assumption (or (not b141) b143 ) :assumption (or (not b141) (not b144) ) :assumption (or b138 (not b141) ) :assumption (or b60 (not b141) ) :assumption (or (= r42 0) b146 ) :assumption (or (not b146) (= r42 1) ) :assumption (or b119 (not b146) ) :assumption (or (not b146) (not b148) ) :assumption (or b144 (not b146) ) :assumption (or b65 (not b146) ) :assumption (or (= r43 0) b150 ) :assumption (or (not b150) (= r43 1) ) :assumption (or b125 (not b150) ) :assumption (or (not b150) (not b152) ) :assumption (or b148 (not b150) ) :assumption (or b70 (not b150) ) :assumption (or (= r44 0) b154 ) :assumption (or (not b154) (= r44 1) ) :assumption (or (not b154) b156 ) :assumption (or (not b120) (not b154) ) :assumption (or b121 (not b154) ) :assumption (or b89 (not b154) ) :assumption (or (= r45 0) b158 ) :assumption (or (not b158) (= r45 1) ) :assumption (or (not b158) b160 ) :assumption (or (not b126) (not b158) ) :assumption (or b120 (not b158) ) :assumption (or (not b158) b161 ) :assumption (or (= r46 0) b163 ) :assumption (or (not b163) (= r46 1) ) :assumption (or b156 (not b163) ) :assumption (or (not b131) (not b163) ) :assumption (or b132 (not b163) ) :assumption (or b99 (not b163) ) :assumption (or (= r48 0) b167 ) :assumption (or (not b167) (= r48 1) ) :assumption (or (not b167) b169 ) :assumption (or (not b138) (not b167) ) :assumption (or (not b167) b170 ) :assumption (or (= r49 0) b172 ) :assumption (or (not b172) (= r49 1) ) :assumption (or (not b172) b174 ) :assumption (or (not b144) (not b172) ) :assumption (or b138 (not b172) ) :assumption (or b107 (not b172) ) :assumption (or (= r50 0) b176 ) :assumption (or (not b176) (= r50 1) ) :assumption (or b156 (not b176) ) :assumption (or (not b148) (not b176) ) :assumption (or b144 (not b176) ) :assumption (or b111 (not b176) ) :assumption (or (= r51 0) b179 ) :assumption (or (not b179) (= r51 1) ) :assumption (or b160 (not b179) ) :assumption (or (not b152) (not b179) ) :assumption (or b148 (not b179) ) :assumption (or b115 (not b179) ) :assumption (or (= r52 0) b182 ) :assumption (or (not b182) (= r52 1) ) :assumption (or (not b182) b184 ) :assumption (or (not b182) (not b185) ) :assumption (or (not b182) b186 ) :assumption (or b36 (not b182) ) :assumption (or (= r53 0) b188 ) :assumption (or (not b188) (= r53 1) ) :assumption (or (not b188) b190 ) :assumption (or (not b188) (not b191) ) :assumption (or b185 (not b188) ) :assumption (or b127 (not b188) ) :assumption (or (= r54 0) b193 ) :assumption (or (not b193) (= r54 1) ) :assumption (or b184 (not b193) ) :assumption (or (not b193) (not b195) ) :assumption (or (not b193) b196 ) :assumption (or b49 (not b193) ) :assumption (or (= r55 0) b198 ) :assumption (or (not b198) (= r55 1) ) :assumption (or b190 (not b198) ) :assumption (or (not b198) (not b200) ) :assumption (or b195 (not b198) ) :assumption (or b54 (not b198) ) :assumption (or (= r56 0) b202 ) :assumption (or (not b202) (= r56 1) ) :assumption (or (not b202) b204 ) :assumption (or (not b202) (not b205) ) :assumption (or b139 (not b202) ) :assumption (or (= r57 0) b207 ) :assumption (or (not b207) (= r57 1) ) :assumption (or (not b207) b209 ) :assumption (or (not b207) (not b210) ) :assumption (or b205 (not b207) ) :assumption (or b60 (not b207) ) :assumption (or (= r58 0) b212 ) :assumption (or (not b212) (= r58 1) ) :assumption (or b184 (not b212) ) :assumption (or (not b212) (not b214) ) :assumption (or b210 (not b212) ) :assumption (or b65 (not b212) ) :assumption (or (= r60 0) b217 ) :assumption (or (not b217) (= r60 1) ) :assumption (or (not b217) b219 ) :assumption (or (not b185) (not b217) ) :assumption (or b186 (not b217) ) :assumption (or b89 (not b217) ) :assumption (or (= r61 0) b221 ) :assumption (or (not b221) (= r61 1) ) :assumption (or (not b221) b223 ) :assumption (or (not b191) (not b221) ) :assumption (or b185 (not b221) ) :assumption (or b161 (not b221) ) :assumption (or (= r62 0) b225 ) :assumption (or (not b225) (= r62 1) ) :assumption (or b219 (not b225) ) :assumption (or (not b195) (not b225) ) :assumption (or b196 (not b225) ) :assumption (or b99 (not b225) ) :assumption (or (= r63 0) b228 ) :assumption (or (not b228) (= r63 1) ) :assumption (or b223 (not b228) ) :assumption (or (not b200) (not b228) ) :assumption (or b195 (not b228) ) :assumption (or b103 (not b228) ) :assumption (or (= r64 0) b231 ) :assumption (or (not b231) (= r64 1) ) :assumption (or (not b231) b233 ) :assumption (or (not b205) (not b231) ) :assumption (or b170 (not b231) ) :assumption (or (= r65 0) b235 ) :assumption (or (not b235) (= r65 1) ) :assumption (or (not b235) b237 ) :assumption (or (not b210) (not b235) ) :assumption (or b205 (not b235) ) :assumption (or b107 (not b235) ) :assumption (or (= r66 0) b239 ) :assumption (or (not b239) (= r66 1) ) :assumption (or b219 (not b239) ) :assumption (or (not b214) (not b239) ) :assumption (or b210 (not b239) ) :assumption (or b111 (not b239) ) :assumption (or (= r68 0) b243 ) :assumption (or (not b243) (= r68 1) ) :assumption (or (not b243) b245 ) :assumption (or (not b243) (not b246) ) :assumption (or (not b243) b247 ) :assumption (or b36 (not b243) ) :assumption (or (= r70 0) b251 ) :assumption (or (not b251) (= r70 1) ) :assumption (or (not b251) b253 ) :assumption (or (not b251) (not b254) ) :assumption (or (not b251) b255 ) :assumption (or (= r71 0) b257 ) :assumption (or (not b257) (= r71 1) ) :assumption (or (not b257) b259 ) :assumption (or (not b257) (not b260) ) :assumption (or b254 (not b257) ) :assumption (or b44 (not b257) ) :assumption (or (= r72 0) b262 ) :assumption (or (not b262) (= r72 1) ) :assumption (or b245 (not b262) ) :assumption (or (not b262) (not b264) ) :assumption (or b260 (not b262) ) :assumption (or b49 (not b262) ) :assumption (or (= r73 0) b266 ) :assumption (or (not b266) (= r73 1) ) :assumption (or b249 (not b266) ) :assumption (or (not b266) (not b268) ) :assumption (or b264 (not b266) ) :assumption (or b54 (not b266) ) :assumption (or (= r74 0) b270 ) :assumption (or (not b270) (= r74 1) ) :assumption (or b245 (not b270) ) :assumption (or (not b270) (not b272) ) :assumption (or (not b270) b273 ) :assumption (or b65 (not b270) ) :assumption (or (= r75 0) b275 ) :assumption (or (not b275) (= r75 1) ) :assumption (or b249 (not b275) ) :assumption (or (not b275) (not b277) ) :assumption (or b272 (not b275) ) :assumption (or b70 (not b275) ) :assumption (or (= r76 0) b279 ) :assumption (or (not b279) (= r76 1) ) :assumption (or (not b279) b281 ) :assumption (or (not b246) (not b279) ) :assumption (or b247 (not b279) ) :assumption (or b89 (not b279) ) :assumption (or (= r78 0) b285 ) :assumption (or (not b285) (= r78 1) ) :assumption (or (not b285) b287 ) :assumption (or (not b254) (not b285) ) :assumption (or (not b285) b288 ) :assumption (or (= r79 0) b290 ) :assumption (or (not b290) (= r79 1) ) :assumption (or (not b290) b292 ) :assumption (or (not b260) (not b290) ) :assumption (or b254 (not b290) ) :assumption (or b95 (not b290) ) :assumption (or (= r80 0) b294 ) :assumption (or (not b294) (= r80 1) ) :assumption (or b281 (not b294) ) :assumption (or (not b264) (not b294) ) :assumption (or b260 (not b294) ) :assumption (or b99 (not b294) ) :assumption (or (= r81 0) b297 ) :assumption (or (not b297) (= r81 1) ) :assumption (or b283 (not b297) ) :assumption (or (not b268) (not b297) ) :assumption (or b264 (not b297) ) :assumption (or b103 (not b297) ) :assumption (or (= r82 0) b300 ) :assumption (or (not b300) (= r82 1) ) :assumption (or b281 (not b300) ) :assumption (or (not b272) (not b300) ) :assumption (or b273 (not b300) ) :assumption (or b111 (not b300) ) :assumption (or (= r83 0) b303 ) :assumption (or (not b303) (= r83 1) ) :assumption (or b283 (not b303) ) :assumption (or (not b277) (not b303) ) :assumption (or b272 (not b303) ) :assumption (or b115 (not b303) ) :assumption (or (= r84 0) b306 ) :assumption (or (not b306) (= r84 1) ) :assumption (or (not b306) b308 ) :assumption (or (not b306) (not b309) ) :assumption (or (not b306) b310 ) :assumption (or b36 (not b306) ) :assumption (or (= r85 0) b312 ) :assumption (or (not b312) (= r85 1) ) :assumption (or (not b312) b314 ) :assumption (or (not b312) (not b315) ) :assumption (or b309 (not b312) ) :assumption (or b127 (not b312) ) :assumption (or (= r86 0) b317 ) :assumption (or (not b317) (= r86 1) ) :assumption (or b308 (not b317) ) :assumption (or (not b317) (not b319) ) :assumption (or (not b317) b320 ) :assumption (or b49 (not b317) ) :assumption (or (= r87 0) b322 ) :assumption (or (not b322) (= r87 1) ) :assumption (or b314 (not b322) ) :assumption (or (not b322) (not b324) ) :assumption (or b319 (not b322) ) :assumption (or b54 (not b322) ) :assumption (or (= r88 0) b326 ) :assumption (or (not b326) (= r88 1) ) :assumption (or (not b326) b328 ) :assumption (or (not b326) (not b329) ) :assumption (or b139 (not b326) ) :assumption (or (= r89 0) b331 ) :assumption (or (not b331) (= r89 1) ) :assumption (or (not b331) b333 ) :assumption (or (not b331) (not b334) ) :assumption (or b329 (not b331) ) :assumption (or b60 (not b331) ) :assumption (or (= r90 0) b336 ) :assumption (or (not b336) (= r90 1) ) :assumption (or b308 (not b336) ) :assumption (or (not b336) (not b338) ) :assumption (or b334 (not b336) ) :assumption (or b65 (not b336) ) :assumption (or (= r91 0) b340 ) :assumption (or (not b340) (= r91 1) ) :assumption (or b314 (not b340) ) :assumption (or (not b340) (not b342) ) :assumption (or b338 (not b340) ) :assumption (or b70 (not b340) ) :assumption (or (= r92 0) b344 ) :assumption (or (not b344) (= r92 1) ) :assumption (or (not b344) b346 ) :assumption (or (not b309) (not b344) ) :assumption (or b310 (not b344) ) :assumption (or b89 (not b344) ) :assumption (or (= r93 0) b348 ) :assumption (or (not b348) (= r93 1) ) :assumption (or (not b348) b350 ) :assumption (or (not b315) (not b348) ) :assumption (or b309 (not b348) ) :assumption (or b161 (not b348) ) :assumption (or (= r94 0) b352 ) :assumption (or (not b352) (= r94 1) ) :assumption (or b346 (not b352) ) :assumption (or (not b319) (not b352) ) :assumption (or b320 (not b352) ) :assumption (or b99 (not b352) ) :assumption (or (= r95 0) b355 ) :assumption (or (not b355) (= r95 1) ) :assumption (or b350 (not b355) ) :assumption (or (not b324) (not b355) ) :assumption (or b319 (not b355) ) :assumption (or b103 (not b355) ) :assumption (or (= r96 0) b358 ) :assumption (or (not b358) (= r96 1) ) :assumption (or (not b358) b360 ) :assumption (or (not b329) (not b358) ) :assumption (or b170 (not b358) ) :assumption (or (= r97 0) b362 ) :assumption (or (not b362) (= r97 1) ) :assumption (or (not b362) b364 ) :assumption (or (not b334) (not b362) ) :assumption (or b329 (not b362) ) :assumption (or b107 (not b362) ) :assumption (or (= r98 0) b366 ) :assumption (or (not b366) (= r98 1) ) :assumption (or b346 (not b366) ) :assumption (or (not b338) (not b366) ) :assumption (or b334 (not b366) ) :assumption (or b111 (not b366) ) :assumption (or (= r99 0) b369 ) :assumption (or (not b369) (= r99 1) ) :assumption (or b350 (not b369) ) :assumption (or (not b342) (not b369) ) :assumption (or b338 (not b369) ) :assumption (or b115 (not b369) ) :assumption (or (= r100 0) b372 ) :assumption (or (not b372) (= r100 (~ 1)) ) :assumption (or b23 (not b372) ) :assumption (or (not b22) (not b372) ) :assumption (or b17 (not b372) ) :assumption (or b24 (not b372) ) :assumption (or (= r101 0) b375 ) :assumption (or (not b375) (= r101 (~ 1)) ) :assumption (or b29 (not b375) ) :assumption (or (not b28) (not b375) ) :assumption (or b22 (not b375) ) :assumption (or b30 (not b375) ) :assumption (or (= r102 0) b378 ) :assumption (or (not b378) (= r102 (~ 1)) ) :assumption (or b35 (not b378) ) :assumption (or (not b34) (not b378) ) :assumption (or b28 (not b378) ) :assumption (or b36 (not b378) ) :assumption (or (= r103 0) b381 ) :assumption (or (not b381) (= r103 (~ 1)) ) :assumption (or (not b38) (not b381) ) :assumption (or b34 (not b381) ) :assumption (or b127 (not b381) ) :assumption (or (= r104 0) b384 ) :assumption (or (not b384) (= r104 (~ 1)) ) :assumption (or b43 (not b384) ) :assumption (or (not b22) (not b384) ) :assumption (or b17 (not b384) ) :assumption (or b255 (not b384) ) :assumption (or (= r105 0) b387 ) :assumption (or (not b387) (= r105 (~ 1)) ) :assumption (or b42 (not b387) ) :assumption (or (not b28) (not b387) ) :assumption (or b22 (not b387) ) :assumption (or b44 (not b387) ) :assumption (or (= r106 0) b390 ) :assumption (or (not b390) (= r106 (~ 1)) ) :assumption (or b48 (not b390) ) :assumption (or (not b34) (not b390) ) :assumption (or b28 (not b390) ) :assumption (or b49 (not b390) ) :assumption (or (= r107 0) b393 ) :assumption (or (not b393) (= r107 (~ 1)) ) :assumption (or b53 (not b393) ) :assumption (or (not b38) (not b393) ) :assumption (or b34 (not b393) ) :assumption (or b54 (not b393) ) :assumption (or (= r108 0) b396 ) :assumption (or (not b396) (= r108 (~ 1)) ) :assumption (or b59 (not b396) ) :assumption (or (not b22) (not b396) ) :assumption (or b17 (not b396) ) :assumption (or b139 (not b396) ) :assumption (or (= r109 0) b399 ) :assumption (or (not b399) (= r109 (~ 1)) ) :assumption (or b58 (not b399) ) :assumption (or (not b28) (not b399) ) :assumption (or b22 (not b399) ) :assumption (or b60 (not b399) ) :assumption (or (= r110 0) b402 ) :assumption (or (not b402) (= r110 (~ 1)) ) :assumption (or b64 (not b402) ) :assumption (or (not b34) (not b402) ) :assumption (or b28 (not b402) ) :assumption (or b65 (not b402) ) :assumption (or (= r111 0) b405 ) :assumption (or (not b405) (= r111 (~ 1)) ) :assumption (or b69 (not b405) ) :assumption (or (not b38) (not b405) ) :assumption (or b34 (not b405) ) :assumption (or b70 (not b405) ) :assumption (or (= r112 0) b408 ) :assumption (or (not b408) (= r112 (~ 1)) ) :assumption (or b23 (not b408) ) :assumption (or (not b78) (not b408) ) :assumption (or b74 (not b408) ) :assumption (or b79 (not b408) ) :assumption (or (= r113 0) b411 ) :assumption (or (not b411) (= r113 (~ 1)) ) :assumption (or b29 (not b411) ) :assumption (or (not b83) (not b411) ) :assumption (or b78 (not b411) ) :assumption (or b84 (not b411) ) :assumption (or (= r114 0) b414 ) :assumption (or (not b414) (= r114 (~ 1)) ) :assumption (or b35 (not b414) ) :assumption (or (not b88) (not b414) ) :assumption (or b83 (not b414) ) :assumption (or b89 (not b414) ) :assumption (or (= r115 0) b417 ) :assumption (or (not b417) (= r115 (~ 1)) ) :assumption (or (not b91) (not b417) ) :assumption (or b88 (not b417) ) :assumption (or b161 (not b417) ) :assumption (or (= r116 0) b420 ) :assumption (or (not b420) (= r116 (~ 1)) ) :assumption (or b43 (not b420) ) :assumption (or (not b78) (not b420) ) :assumption (or b74 (not b420) ) :assumption (or b288 (not b420) ) :assumption (or (= r117 0) b423 ) :assumption (or (not b423) (= r117 (~ 1)) ) :assumption (or b42 (not b423) ) :assumption (or (not b83) (not b423) ) :assumption (or b78 (not b423) ) :assumption (or b95 (not b423) ) :assumption (or (= r118 0) b426 ) :assumption (or (not b426) (= r118 (~ 1)) ) :assumption (or b48 (not b426) ) :assumption (or (not b88) (not b426) ) :assumption (or b83 (not b426) ) :assumption (or b99 (not b426) ) :assumption (or (= r119 0) b429 ) :assumption (or (not b429) (= r119 (~ 1)) ) :assumption (or b53 (not b429) ) :assumption (or (not b91) (not b429) ) :assumption (or b88 (not b429) ) :assumption (or b103 (not b429) ) :assumption (or (= r120 0) b432 ) :assumption (or (not b432) (= r120 (~ 1)) ) :assumption (or b59 (not b432) ) :assumption (or (not b78) (not b432) ) :assumption (or b74 (not b432) ) :assumption (or b170 (not b432) ) :assumption (or (= r121 0) b435 ) :assumption (or (not b435) (= r121 (~ 1)) ) :assumption (or b58 (not b435) ) :assumption (or (not b83) (not b435) ) :assumption (or b78 (not b435) ) :assumption (or b107 (not b435) ) :assumption (or (= r122 0) b438 ) :assumption (or (not b438) (= r122 (~ 1)) ) :assumption (or b64 (not b438) ) :assumption (or (not b88) (not b438) ) :assumption (or b83 (not b438) ) :assumption (or b111 (not b438) ) :assumption (or (= r123 0) b441 ) :assumption (or (not b441) (= r123 (~ 1)) ) :assumption (or b69 (not b441) ) :assumption (or (not b91) (not b441) ) :assumption (or b88 (not b441) ) :assumption (or b115 (not b441) ) :assumption (or (= r124 0) b444 ) :assumption (or (not b444) (= r124 (~ 1)) ) :assumption (or b121 (not b444) ) :assumption (or (not b143) (not b444) ) :assumption (or b137 (not b444) ) :assumption (or b30 (not b444) ) :assumption (or (= r125 0) b447 ) :assumption (or (not b447) (= r125 (~ 1)) ) :assumption (or b120 (not b447) ) :assumption (or (not b119) (not b447) ) :assumption (or b143 (not b447) ) :assumption (or b36 (not b447) ) :assumption (or (= r126 0) b450 ) :assumption (or (not b450) (= r126 (~ 1)) ) :assumption (or b126 (not b450) ) :assumption (or (not b125) (not b450) ) :assumption (or b119 (not b450) ) :assumption (or b127 (not b450) ) :assumption (or (= r127 0) b453 ) :assumption (or (not b453) (= r127 (~ 1)) ) :assumption (or b132 (not b453) ) :assumption (or (not b143) (not b453) ) :assumption (or b137 (not b453) ) :assumption (or b44 (not b453) ) :assumption (or (= r128 0) b456 ) :assumption (or (not b456) (= r128 (~ 1)) ) :assumption (or b131 (not b456) ) :assumption (or (not b119) (not b456) ) :assumption (or b143 (not b456) ) :assumption (or b49 (not b456) ) :assumption (or (= r129 0) b459 ) :assumption (or (not b459) (= r129 (~ 1)) ) :assumption (or (not b125) (not b459) ) :assumption (or b119 (not b459) ) :assumption (or b54 (not b459) ) :assumption (or (= r130 0) b462 ) :assumption (or (not b462) (= r130 (~ 1)) ) :assumption (or b144 (not b462) ) :assumption (or (not b143) (not b462) ) :assumption (or b137 (not b462) ) :assumption (or b60 (not b462) ) :assumption (or (= r131 0) b465 ) :assumption (or (not b465) (= r131 (~ 1)) ) :assumption (or b148 (not b465) ) :assumption (or (not b119) (not b465) ) :assumption (or b143 (not b465) ) :assumption (or b65 (not b465) ) :assumption (or (= r132 0) b468 ) :assumption (or (not b468) (= r132 (~ 1)) ) :assumption (or b152 (not b468) ) :assumption (or (not b125) (not b468) ) :assumption (or b119 (not b468) ) :assumption (or b70 (not b468) ) :assumption (or (= r133 0) b471 ) :assumption (or (not b471) (= r133 (~ 1)) ) :assumption (or b121 (not b471) ) :assumption (or (not b174) (not b471) ) :assumption (or b169 (not b471) ) :assumption (or b84 (not b471) ) :assumption (or (= r134 0) b474 ) :assumption (or (not b474) (= r134 (~ 1)) ) :assumption (or b120 (not b474) ) :assumption (or (not b156) (not b474) ) :assumption (or b174 (not b474) ) :assumption (or b89 (not b474) ) :assumption (or (= r135 0) b477 ) :assumption (or (not b477) (= r135 (~ 1)) ) :assumption (or b126 (not b477) ) :assumption (or (not b160) (not b477) ) :assumption (or b156 (not b477) ) :assumption (or b161 (not b477) ) :assumption (or (= r136 0) b480 ) :assumption (or (not b480) (= r136 (~ 1)) ) :assumption (or b132 (not b480) ) :assumption (or (not b174) (not b480) ) :assumption (or b169 (not b480) ) :assumption (or b95 (not b480) ) :assumption (or (= r137 0) b483 ) :assumption (or (not b483) (= r137 (~ 1)) ) :assumption (or b131 (not b483) ) :assumption (or (not b156) (not b483) ) :assumption (or b174 (not b483) ) :assumption (or b99 (not b483) ) :assumption (or (= r138 0) b486 ) :assumption (or (not b486) (= r138 (~ 1)) ) :assumption (or (not b160) (not b486) ) :assumption (or b156 (not b486) ) :assumption (or b103 (not b486) ) :assumption (or (= r139 0) b489 ) :assumption (or (not b489) (= r139 (~ 1)) ) :assumption (or b144 (not b489) ) :assumption (or (not b174) (not b489) ) :assumption (or b169 (not b489) ) :assumption (or b107 (not b489) ) :assumption (or (= r140 0) b492 ) :assumption (or (not b492) (= r140 (~ 1)) ) :assumption (or b148 (not b492) ) :assumption (or (not b156) (not b492) ) :assumption (or b174 (not b492) ) :assumption (or b111 (not b492) ) :assumption (or (= r141 0) b495 ) :assumption (or (not b495) (= r141 (~ 1)) ) :assumption (or b152 (not b495) ) :assumption (or (not b160) (not b495) ) :assumption (or b156 (not b495) ) :assumption (or b115 (not b495) ) :assumption (or (= r142 0) b498 ) :assumption (or (not b498) (= r142 (~ 1)) ) :assumption (or b186 (not b498) ) :assumption (or (not b209) (not b498) ) :assumption (or b204 (not b498) ) :assumption (or b30 (not b498) ) :assumption (or (= r143 0) b501 ) :assumption (or (not b501) (= r143 (~ 1)) ) :assumption (or b185 (not b501) ) :assumption (or (not b184) (not b501) ) :assumption (or b209 (not b501) ) :assumption (or b36 (not b501) ) :assumption (or (= r144 0) b504 ) :assumption (or (not b504) (= r144 (~ 1)) ) :assumption (or b191 (not b504) ) :assumption (or (not b190) (not b504) ) :assumption (or b184 (not b504) ) :assumption (or b127 (not b504) ) :assumption (or (= r145 0) b507 ) :assumption (or (not b507) (= r145 (~ 1)) ) :assumption (or b196 (not b507) ) :assumption (or (not b209) (not b507) ) :assumption (or b204 (not b507) ) :assumption (or b44 (not b507) ) :assumption (or (= r146 0) b510 ) :assumption (or (not b510) (= r146 (~ 1)) ) :assumption (or b195 (not b510) ) :assumption (or (not b184) (not b510) ) :assumption (or b209 (not b510) ) :assumption (or b49 (not b510) ) :assumption (or (= r147 0) b513 ) :assumption (or (not b513) (= r147 (~ 1)) ) :assumption (or b200 (not b513) ) :assumption (or (not b190) (not b513) ) :assumption (or b184 (not b513) ) :assumption (or b54 (not b513) ) :assumption (or (= r148 0) b516 ) :assumption (or (not b516) (= r148 (~ 1)) ) :assumption (or b210 (not b516) ) :assumption (or (not b209) (not b516) ) :assumption (or b204 (not b516) ) :assumption (or b60 (not b516) ) :assumption (or (= r149 0) b519 ) :assumption (or (not b519) (= r149 (~ 1)) ) :assumption (or b214 (not b519) ) :assumption (or (not b184) (not b519) ) :assumption (or b209 (not b519) ) :assumption (or b65 (not b519) ) :assumption (or (= r150 0) b522 ) :assumption (or (not b522) (= r150 (~ 1)) ) :assumption (or (not b190) (not b522) ) :assumption (or b184 (not b522) ) :assumption (or b70 (not b522) ) :assumption (or (= r151 0) b525 ) :assumption (or (not b525) (= r151 (~ 1)) ) :assumption (or b186 (not b525) ) :assumption (or (not b237) (not b525) ) :assumption (or b233 (not b525) ) :assumption (or b84 (not b525) ) :assumption (or (= r152 0) b528 ) :assumption (or (not b528) (= r152 (~ 1)) ) :assumption (or b185 (not b528) ) :assumption (or (not b219) (not b528) ) :assumption (or b237 (not b528) ) :assumption (or b89 (not b528) ) :assumption (or (= r153 0) b531 ) :assumption (or (not b531) (= r153 (~ 1)) ) :assumption (or b191 (not b531) ) :assumption (or (not b223) (not b531) ) :assumption (or b219 (not b531) ) :assumption (or b161 (not b531) ) :assumption (or (= r154 0) b534 ) :assumption (or (not b534) (= r154 (~ 1)) ) :assumption (or b196 (not b534) ) :assumption (or (not b237) (not b534) ) :assumption (or b233 (not b534) ) :assumption (or b95 (not b534) ) :assumption (or (= r155 0) b537 ) :assumption (or (not b537) (= r155 (~ 1)) ) :assumption (or b195 (not b537) ) :assumption (or (not b219) (not b537) ) :assumption (or b237 (not b537) ) :assumption (or b99 (not b537) ) :assumption (or (= r156 0) b540 ) :assumption (or (not b540) (= r156 (~ 1)) ) :assumption (or b200 (not b540) ) :assumption (or (not b223) (not b540) ) :assumption (or b219 (not b540) ) :assumption (or b103 (not b540) ) :assumption (or (= r157 0) b543 ) :assumption (or (not b543) (= r157 (~ 1)) ) :assumption (or b210 (not b543) ) :assumption (or (not b237) (not b543) ) :assumption (or b233 (not b543) ) :assumption (or b107 (not b543) ) :assumption (or (= r158 0) b546 ) :assumption (or (not b546) (= r158 (~ 1)) ) :assumption (or b214 (not b546) ) :assumption (or (not b219) (not b546) ) :assumption (or b237 (not b546) ) :assumption (or b111 (not b546) ) :assumption (or (= r159 0) b549 ) :assumption (or (not b549) (= r159 (~ 1)) ) :assumption (or (not b223) (not b549) ) :assumption (or b219 (not b549) ) :assumption (or b115 (not b549) ) :assumption (or (= r160 0) b552 ) :assumption (or (not b552) (= r160 (~ 1)) ) :assumption (or b247 (not b552) ) :assumption (or (not b259) (not b552) ) :assumption (or b253 (not b552) ) :assumption (or b30 (not b552) ) :assumption (or (= r161 0) b555 ) :assumption (or (not b555) (= r161 (~ 1)) ) :assumption (or b246 (not b555) ) :assumption (or (not b245) (not b555) ) :assumption (or b259 (not b555) ) :assumption (or b36 (not b555) ) :assumption (or (= r162 0) b558 ) :assumption (or (not b558) (= r162 (~ 1)) ) :assumption (or (not b249) (not b558) ) :assumption (or b245 (not b558) ) :assumption (or b127 (not b558) ) :assumption (or (= r163 0) b561 ) :assumption (or (not b561) (= r163 (~ 1)) ) :assumption (or b260 (not b561) ) :assumption (or (not b259) (not b561) ) :assumption (or b253 (not b561) ) :assumption (or b44 (not b561) ) :assumption (or (= r164 0) b564 ) :assumption (or (not b564) (= r164 (~ 1)) ) :assumption (or b264 (not b564) ) :assumption (or (not b245) (not b564) ) :assumption (or b259 (not b564) ) :assumption (or b49 (not b564) ) :assumption (or (= r165 0) b567 ) :assumption (or (not b567) (= r165 (~ 1)) ) :assumption (or b268 (not b567) ) :assumption (or (not b249) (not b567) ) :assumption (or b245 (not b567) ) :assumption (or b54 (not b567) ) :assumption (or (= r166 0) b570 ) :assumption (or (not b570) (= r166 (~ 1)) ) :assumption (or b273 (not b570) ) :assumption (or (not b259) (not b570) ) :assumption (or b253 (not b570) ) :assumption (or b60 (not b570) ) :assumption (or (= r167 0) b573 ) :assumption (or (not b573) (= r167 (~ 1)) ) :assumption (or b272 (not b573) ) :assumption (or (not b245) (not b573) ) :assumption (or b259 (not b573) ) :assumption (or b65 (not b573) ) :assumption (or (= r168 0) b576 ) :assumption (or (not b576) (= r168 (~ 1)) ) :assumption (or b277 (not b576) ) :assumption (or (not b249) (not b576) ) :assumption (or b245 (not b576) ) :assumption (or b70 (not b576) ) :assumption (or (= r169 0) b579 ) :assumption (or (not b579) (= r169 (~ 1)) ) :assumption (or b247 (not b579) ) :assumption (or (not b292) (not b579) ) :assumption (or b287 (not b579) ) :assumption (or b84 (not b579) ) :assumption (or (= r170 0) b582 ) :assumption (or (not b582) (= r170 (~ 1)) ) :assumption (or b246 (not b582) ) :assumption (or (not b281) (not b582) ) :assumption (or b292 (not b582) ) :assumption (or b89 (not b582) ) :assumption (or (= r171 0) b585 ) :assumption (or (not b585) (= r171 (~ 1)) ) :assumption (or (not b283) (not b585) ) :assumption (or b281 (not b585) ) :assumption (or b161 (not b585) ) :assumption (or (= r172 0) b588 ) :assumption (or (not b588) (= r172 (~ 1)) ) :assumption (or b260 (not b588) ) :assumption (or (not b292) (not b588) ) :assumption (or b287 (not b588) ) :assumption (or b95 (not b588) ) :assumption (or (= r173 0) b591 ) :assumption (or (not b591) (= r173 (~ 1)) ) :assumption (or b264 (not b591) ) :assumption (or (not b281) (not b591) ) :assumption (or b292 (not b591) ) :assumption (or b99 (not b591) ) :assumption (or (= r174 0) b594 ) :assumption (or (not b594) (= r174 (~ 1)) ) :assumption (or b268 (not b594) ) :assumption (or (not b283) (not b594) ) :assumption (or b281 (not b594) ) :assumption (or b103 (not b594) ) :assumption (or (= r175 0) b597 ) :assumption (or (not b597) (= r175 (~ 1)) ) :assumption (or b273 (not b597) ) :assumption (or (not b292) (not b597) ) :assumption (or b287 (not b597) ) :assumption (or b107 (not b597) ) :assumption (or (= r176 0) b600 ) :assumption (or (not b600) (= r176 (~ 1)) ) :assumption (or b272 (not b600) ) :assumption (or (not b281) (not b600) ) :assumption (or b292 (not b600) ) :assumption (or b111 (not b600) ) :assumption (or (= r177 0) b603 ) :assumption (or (not b603) (= r177 (~ 1)) ) :assumption (or b277 (not b603) ) :assumption (or (not b283) (not b603) ) :assumption (or b281 (not b603) ) :assumption (or b115 (not b603) ) :assumption (or (= r178 0) b606 ) :assumption (or (not b606) (= r178 (~ 1)) ) :assumption (or b310 (not b606) ) :assumption (or (not b333) (not b606) ) :assumption (or b328 (not b606) ) :assumption (or b30 (not b606) ) :assumption (or (= r179 0) b609 ) :assumption (or (not b609) (= r179 (~ 1)) ) :assumption (or b309 (not b609) ) :assumption (or (not b308) (not b609) ) :assumption (or b333 (not b609) ) :assumption (or b36 (not b609) ) :assumption (or (= r180 0) b612 ) :assumption (or (not b612) (= r180 (~ 1)) ) :assumption (or b315 (not b612) ) :assumption (or (not b314) (not b612) ) :assumption (or b308 (not b612) ) :assumption (or b127 (not b612) ) :assumption (or (= r181 0) b615 ) :assumption (or (not b615) (= r181 (~ 1)) ) :assumption (or b320 (not b615) ) :assumption (or (not b333) (not b615) ) :assumption (or b328 (not b615) ) :assumption (or b44 (not b615) ) :assumption (or (= r182 0) b618 ) :assumption (or (not b618) (= r182 (~ 1)) ) :assumption (or b319 (not b618) ) :assumption (or (not b308) (not b618) ) :assumption (or b333 (not b618) ) :assumption (or b49 (not b618) ) :assumption (or (= r183 0) b621 ) :assumption (or (not b621) (= r183 (~ 1)) ) :assumption (or b324 (not b621) ) :assumption (or (not b314) (not b621) ) :assumption (or b308 (not b621) ) :assumption (or b54 (not b621) ) :assumption (or (= r184 0) b624 ) :assumption (or (not b624) (= r184 (~ 1)) ) :assumption (or b334 (not b624) ) :assumption (or (not b333) (not b624) ) :assumption (or b328 (not b624) ) :assumption (or b60 (not b624) ) :assumption (or (= r185 0) b627 ) :assumption (or (not b627) (= r185 (~ 1)) ) :assumption (or b338 (not b627) ) :assumption (or (not b308) (not b627) ) :assumption (or b333 (not b627) ) :assumption (or b65 (not b627) ) :assumption (or (= r186 0) b630 ) :assumption (or (not b630) (= r186 (~ 1)) ) :assumption (or b342 (not b630) ) :assumption (or (not b314) (not b630) ) :assumption (or b308 (not b630) ) :assumption (or b70 (not b630) ) :assumption (or (= r187 0) b633 ) :assumption (or (not b633) (= r187 (~ 1)) ) :assumption (or b310 (not b633) ) :assumption (or (not b364) (not b633) ) :assumption (or b360 (not b633) ) :assumption (or b84 (not b633) ) :assumption (or (= r188 0) b636 ) :assumption (or (not b636) (= r188 (~ 1)) ) :assumption (or b309 (not b636) ) :assumption (or (not b346) (not b636) ) :assumption (or b364 (not b636) ) :assumption (or b89 (not b636) ) :assumption (or (= r189 0) b639 ) :assumption (or (not b639) (= r189 (~ 1)) ) :assumption (or b315 (not b639) ) :assumption (or (not b350) (not b639) ) :assumption (or b346 (not b639) ) :assumption (or b161 (not b639) ) :assumption (or (= r190 0) b642 ) :assumption (or (not b642) (= r190 (~ 1)) ) :assumption (or b320 (not b642) ) :assumption (or (not b364) (not b642) ) :assumption (or b360 (not b642) ) :assumption (or b95 (not b642) ) :assumption (or (= r191 0) b645 ) :assumption (or (not b645) (= r191 (~ 1)) ) :assumption (or b319 (not b645) ) :assumption (or (not b346) (not b645) ) :assumption (or b364 (not b645) ) :assumption (or b99 (not b645) ) :assumption (or (= r192 0) b648 ) :assumption (or (not b648) (= r192 (~ 1)) ) :assumption (or b324 (not b648) ) :assumption (or (not b350) (not b648) ) :assumption (or b346 (not b648) ) :assumption (or b103 (not b648) ) :assumption (or (= r193 0) b651 ) :assumption (or (not b651) (= r193 (~ 1)) ) :assumption (or b334 (not b651) ) :assumption (or (not b364) (not b651) ) :assumption (or b360 (not b651) ) :assumption (or b107 (not b651) ) :assumption (or (= r194 0) b654 ) :assumption (or (not b654) (= r194 (~ 1)) ) :assumption (or b338 (not b654) ) :assumption (or (not b346) (not b654) ) :assumption (or b364 (not b654) ) :assumption (or b111 (not b654) ) :assumption (or (= r195 0) b657 ) :assumption (or (not b657) (= r195 (~ 1)) ) :assumption (or b342 (not b657) ) :assumption (or (not b350) (not b657) ) :assumption (or b346 (not b657) ) :assumption (or b115 (not b657) ) :assumption (or (= r196 0) b660 ) :assumption (or b660 (= r197 0) ) :assumption (or (not b660) (= r197 (* (~ 502) 2)) ) :assumption (or (not b660) (= r196 (* 502 2)) ) :assumption (or b255 (not b660) ) :assumption (or (not b24) (not b660) ) :assumption (or (not b660) (>= r10 (* 502 2)) ) :assumption (or (= r198 0) b666 ) :assumption (or b666 (= r199 0) ) :assumption (or (not b666) (= r199 (* (~ 502) 2)) ) :assumption (or (not b666) (= r198 (* 502 2)) ) :assumption (or b44 (not b666) ) :assumption (or (not b30) (not b666) ) :assumption (or b24 (not b666) ) :assumption (or (not b666) (>= r200 (* 502 2)) ) :assumption (or (= r201 0) b672 ) :assumption (or b672 (= r202 0) ) :assumption (or (not b672) (= r202 (* (~ 502) 2)) ) :assumption (or (not b672) (= r201 (* 502 2)) ) :assumption (or b49 (not b672) ) :assumption (or (not b36) (not b672) ) :assumption (or b30 (not b672) ) :assumption (or (not b672) (>= r203 (* 502 2)) ) :assumption (or (= r204 0) b678 ) :assumption (or b678 (= r205 0) ) :assumption (or (not b678) (= r205 (* (~ 502) 2)) ) :assumption (or (not b678) (= r204 (* 502 2)) ) :assumption (or b54 (not b678) ) :assumption (or (not b127) (not b678) ) :assumption (or b36 (not b678) ) :assumption (or (not b678) (>= r206 (* 502 2)) ) :assumption (or (= r207 0) b684 ) :assumption (or b684 (= r208 0) ) :assumption (or (not b684) (= r208 (* (~ 502) 2)) ) :assumption (or (not b684) (= r207 (* 502 2)) ) :assumption (or (not b684) b688 ) :assumption (or (not b684) (not b689) ) :assumption (or b127 (not b684) ) :assumption (or (not b684) (>= r209 (* 502 2)) ) :assumption (or (= r210 0) b692 ) :assumption (or b692 (= r211 0) ) :assumption (or (not b692) (= r211 (* (~ 743) 2)) ) :assumption (or (not b692) (= r210 (* 743 2)) ) :assumption (or b139 (not b692) ) :assumption (or (not b24) (not b692) ) :assumption (or (not b692) (>= r10 (* 743 2)) ) :assumption (or (= r212 0) b698 ) :assumption (or b698 (= r213 0) ) :assumption (or (not b698) (= r213 (* (~ 743) 2)) ) :assumption (or (not b698) (= r212 (* 743 2)) ) :assumption (or b60 (not b698) ) :assumption (or (not b30) (not b698) ) :assumption (or b24 (not b698) ) :assumption (or (not b698) (>= r200 (* 743 2)) ) :assumption (or (= r214 0) b704 ) :assumption (or b704 (= r215 0) ) :assumption (or (not b704) (= r215 (* (~ 743) 2)) ) :assumption (or (not b704) (= r214 (* 743 2)) ) :assumption (or b65 (not b704) ) :assumption (or (not b36) (not b704) ) :assumption (or b30 (not b704) ) :assumption (or (not b704) (>= r203 (* 743 2)) ) :assumption (or (= r216 0) b710 ) :assumption (or b710 (= r217 0) ) :assumption (or (not b710) (= r217 (* (~ 743) 2)) ) :assumption (or (not b710) (= r216 (* 743 2)) ) :assumption (or b70 (not b710) ) :assumption (or (not b127) (not b710) ) :assumption (or b36 (not b710) ) :assumption (or (not b710) (>= r206 (* 743 2)) ) :assumption (or (= r218 0) b716 ) :assumption (or b716 (= r219 0) ) :assumption (or (not b716) (= r219 (* (~ 743) 2)) ) :assumption (or (not b716) (= r218 (* 743 2)) ) :assumption (or (not b716) b720 ) :assumption (or (not b689) (not b716) ) :assumption (or b127 (not b716) ) :assumption (or (not b716) (>= r209 (* 743 2)) ) :assumption (or (= r220 0) b723 ) :assumption (or b723 (= r221 0) ) :assumption (or (not b723) (= r221 (* (~ 502) 2)) ) :assumption (or (not b723) (= r220 (* 502 2)) ) :assumption (or b30 (not b723) ) :assumption (or (not b44) (not b723) ) :assumption (or b255 (not b723) ) :assumption (or (>= r200 (* 502 2)) (not b723) ) :assumption (or (= r222 0) b728 ) :assumption (or b728 (= r223 0) ) :assumption (or (not b728) (= r223 (* (~ 502) 2)) ) :assumption (or (not b728) (= r222 (* 502 2)) ) :assumption (or b36 (not b728) ) :assumption (or (not b49) (not b728) ) :assumption (or b44 (not b728) ) :assumption (or (>= r203 (* 502 2)) (not b728) ) :assumption (or (= r224 0) b733 ) :assumption (or b733 (= r225 0) ) :assumption (or (not b733) (= r225 (* (~ 502) 2)) ) :assumption (or (not b733) (= r224 (* 502 2)) ) :assumption (or b127 (not b733) ) :assumption (or (not b54) (not b733) ) :assumption (or b49 (not b733) ) :assumption (or (>= r206 (* 502 2)) (not b733) ) :assumption (or (= r226 0) b738 ) :assumption (or b738 (= r227 0) ) :assumption (or (not b738) (= r227 (* (~ 502) 2)) ) :assumption (or (not b738) (= r226 (* 502 2)) ) :assumption (or b689 (not b738) ) :assumption (or (not b688) (not b738) ) :assumption (or b54 (not b738) ) :assumption (or (>= r209 (* 502 2)) (not b738) ) :assumption (or (= r228 0) b743 ) :assumption (or b743 (= r229 0) ) :assumption (or (not b743) (= r229 (* (~ 834) 2)) ) :assumption (or (not b743) (= r228 (* 834 2)) ) :assumption (or b60 (not b743) ) :assumption (or (not b44) (not b743) ) :assumption (or b255 (not b743) ) :assumption (or (not b743) (>= r200 (* 834 2)) ) :assumption (or (= r230 0) b749 ) :assumption (or b749 (= r231 0) ) :assumption (or (not b749) (= r231 (* (~ 834) 2)) ) :assumption (or (not b749) (= r230 (* 834 2)) ) :assumption (or b65 (not b749) ) :assumption (or (not b49) (not b749) ) :assumption (or b44 (not b749) ) :assumption (or (not b749) (>= r203 (* 834 2)) ) :assumption (or (= r232 0) b755 ) :assumption (or b755 (= r233 0) ) :assumption (or (not b755) (= r233 (* (~ 834) 2)) ) :assumption (or (not b755) (= r232 (* 834 2)) ) :assumption (or b70 (not b755) ) :assumption (or (not b54) (not b755) ) :assumption (or b49 (not b755) ) :assumption (or (not b755) (>= r206 (* 834 2)) ) :assumption (or (= r234 0) b761 ) :assumption (or b761 (= r235 0) ) :assumption (or (not b761) (= r235 (* (~ 834) 2)) ) :assumption (or (not b761) (= r234 (* 834 2)) ) :assumption (or b720 (not b761) ) :assumption (or (not b688) (not b761) ) :assumption (or b54 (not b761) ) :assumption (or (not b761) (>= r209 (* 834 2)) ) :assumption (or (= r236 0) b767 ) :assumption (or b767 (= r237 0) ) :assumption (or (not b767) (= r237 (* (~ 743) 2)) ) :assumption (or (not b767) (= r236 (* 743 2)) ) :assumption (or b30 (not b767) ) :assumption (or (not b60) (not b767) ) :assumption (or b139 (not b767) ) :assumption (or (>= r200 (* 743 2)) (not b767) ) :assumption (or (= r238 0) b772 ) :assumption (or b772 (= r239 0) ) :assumption (or (not b772) (= r239 (* (~ 743) 2)) ) :assumption (or (not b772) (= r238 (* 743 2)) ) :assumption (or b36 (not b772) ) :assumption (or (not b65) (not b772) ) :assumption (or b60 (not b772) ) :assumption (or (>= r203 (* 743 2)) (not b772) ) :assumption (or (= r240 0) b777 ) :assumption (or b777 (= r241 0) ) :assumption (or (not b777) (= r241 (* (~ 743) 2)) ) :assumption (or (not b777) (= r240 (* 743 2)) ) :assumption (or b127 (not b777) ) :assumption (or (not b70) (not b777) ) :assumption (or b65 (not b777) ) :assumption (or (>= r206 (* 743 2)) (not b777) ) :assumption (or (= r242 0) b782 ) :assumption (or b782 (= r243 0) ) :assumption (or (not b782) (= r243 (* (~ 743) 2)) ) :assumption (or (not b782) (= r242 (* 743 2)) ) :assumption (or b689 (not b782) ) :assumption (or (not b720) (not b782) ) :assumption (or b70 (not b782) ) :assumption (or (>= r209 (* 743 2)) (not b782) ) :assumption (or (= r244 0) b787 ) :assumption (or b787 (= r245 0) ) :assumption (or (not b787) (= r245 (* (~ 834) 2)) ) :assumption (or (not b787) (= r244 (* 834 2)) ) :assumption (or b44 (not b787) ) :assumption (or (not b60) (not b787) ) :assumption (or b139 (not b787) ) :assumption (or (>= r200 (* 834 2)) (not b787) ) :assumption (or (= r246 0) b792 ) :assumption (or b792 (= r247 0) ) :assumption (or (not b792) (= r247 (* (~ 834) 2)) ) :assumption (or (not b792) (= r246 (* 834 2)) ) :assumption (or b49 (not b792) ) :assumption (or (not b65) (not b792) ) :assumption (or b60 (not b792) ) :assumption (or (>= r203 (* 834 2)) (not b792) ) :assumption (or (= r248 0) b797 ) :assumption (or b797 (= r249 0) ) :assumption (or (not b797) (= r249 (* (~ 834) 2)) ) :assumption (or (not b797) (= r248 (* 834 2)) ) :assumption (or b54 (not b797) ) :assumption (or (not b70) (not b797) ) :assumption (or b65 (not b797) ) :assumption (or (>= r206 (* 834 2)) (not b797) ) :assumption (or (= r250 0) b802 ) :assumption (or b802 (= r251 0) ) :assumption (or (not b802) (= r251 (* (~ 834) 2)) ) :assumption (or (not b802) (= r250 (* 834 2)) ) :assumption (or b688 (not b802) ) :assumption (or (not b720) (not b802) ) :assumption (or b70 (not b802) ) :assumption (or (>= r209 (* 834 2)) (not b802) ) :assumption (or (= r252 0) b807 ) :assumption (or b807 (= r253 0) ) :assumption (or (not b807) (= r253 (* (~ 502) 2)) ) :assumption (or (not b807) (= r252 (* 502 2)) ) :assumption (or b288 (not b807) ) :assumption (or (not b79) (not b807) ) :assumption (or (not b807) (>= r12 (* 502 2)) ) :assumption (or (= r254 0) b813 ) :assumption (or b813 (= r255 0) ) :assumption (or (not b813) (= r255 (* (~ 502) 2)) ) :assumption (or (not b813) (= r254 (* 502 2)) ) :assumption (or b95 (not b813) ) :assumption (or (not b84) (not b813) ) :assumption (or b79 (not b813) ) :assumption (or (not b813) (>= r256 (* 502 2)) ) :assumption (or (= r257 0) b819 ) :assumption (or b819 (= r258 0) ) :assumption (or (not b819) (= r258 (* (~ 502) 2)) ) :assumption (or (not b819) (= r257 (* 502 2)) ) :assumption (or b99 (not b819) ) :assumption (or (not b89) (not b819) ) :assumption (or b84 (not b819) ) :assumption (or (not b819) (>= r259 (* 502 2)) ) :assumption (or (= r260 0) b825 ) :assumption (or b825 (= r261 0) ) :assumption (or (not b825) (= r261 (* (~ 502) 2)) ) :assumption (or (not b825) (= r260 (* 502 2)) ) :assumption (or b103 (not b825) ) :assumption (or (not b161) (not b825) ) :assumption (or b89 (not b825) ) :assumption (or (not b825) (>= r262 (* 502 2)) ) :assumption (or (= r263 0) b831 ) :assumption (or b831 (= r264 0) ) :assumption (or (not b831) (= r264 (* (~ 502) 2)) ) :assumption (or (not b831) (= r263 (* 502 2)) ) :assumption (or (not b831) b835 ) :assumption (or (not b831) (not b836) ) :assumption (or b161 (not b831) ) :assumption (or (not b831) (>= r265 (* 502 2)) ) :assumption (or (= r266 0) b839 ) :assumption (or b839 (= r267 0) ) :assumption (or (not b839) (= r267 (* (~ 743) 2)) ) :assumption (or (not b839) (= r266 (* 743 2)) ) :assumption (or b170 (not b839) ) :assumption (or (not b79) (not b839) ) :assumption (or (not b839) (>= r12 (* 743 2)) ) :assumption (or (= r268 0) b845 ) :assumption (or b845 (= r269 0) ) :assumption (or (not b845) (= r269 (* (~ 743) 2)) ) :assumption (or (not b845) (= r268 (* 743 2)) ) :assumption (or b107 (not b845) ) :assumption (or (not b84) (not b845) ) :assumption (or b79 (not b845) ) :assumption (or (not b845) (>= r256 (* 743 2)) ) :assumption (or (= r270 0) b851 ) :assumption (or b851 (= r271 0) ) :assumption (or (not b851) (= r271 (* (~ 743) 2)) ) :assumption (or (not b851) (= r270 (* 743 2)) ) :assumption (or b111 (not b851) ) :assumption (or (not b89) (not b851) ) :assumption (or b84 (not b851) ) :assumption (or (not b851) (>= r259 (* 743 2)) ) :assumption (or (= r272 0) b857 ) :assumption (or b857 (= r273 0) ) :assumption (or (not b857) (= r273 (* (~ 743) 2)) ) :assumption (or (not b857) (= r272 (* 743 2)) ) :assumption (or b115 (not b857) ) :assumption (or (not b161) (not b857) ) :assumption (or b89 (not b857) ) :assumption (or (not b857) (>= r262 (* 743 2)) ) :assumption (or (= r274 0) b863 ) :assumption (or b863 (= r275 0) ) :assumption (or (not b863) (= r275 (* (~ 743) 2)) ) :assumption (or (not b863) (= r274 (* 743 2)) ) :assumption (or (not b836) (not b863) ) :assumption (or b161 (not b863) ) :assumption (or (not b863) (>= r265 (* 743 2)) ) :assumption (or (= r276 0) b869 ) :assumption (or b869 (= r277 0) ) :assumption (or (not b869) (= r277 (* (~ 502) 2)) ) :assumption (or (not b869) (= r276 (* 502 2)) ) :assumption (or b84 (not b869) ) :assumption (or (not b95) (not b869) ) :assumption (or b288 (not b869) ) :assumption (or (>= r256 (* 502 2)) (not b869) ) :assumption (or (= r278 0) b874 ) :assumption (or b874 (= r279 0) ) :assumption (or (not b874) (= r279 (* (~ 502) 2)) ) :assumption (or (not b874) (= r278 (* 502 2)) ) :assumption (or b89 (not b874) ) :assumption (or (not b99) (not b874) ) :assumption (or b95 (not b874) ) :assumption (or (>= r259 (* 502 2)) (not b874) ) :assumption (or (= r280 0) b879 ) :assumption (or b879 (= r281 0) ) :assumption (or (not b879) (= r281 (* (~ 502) 2)) ) :assumption (or (not b879) (= r280 (* 502 2)) ) :assumption (or b161 (not b879) ) :assumption (or (not b103) (not b879) ) :assumption (or b99 (not b879) ) :assumption (or (>= r262 (* 502 2)) (not b879) ) :assumption (or (= r282 0) b884 ) :assumption (or b884 (= r283 0) ) :assumption (or (not b884) (= r283 (* (~ 502) 2)) ) :assumption (or (not b884) (= r282 (* 502 2)) ) :assumption (or b836 (not b884) ) :assumption (or (not b835) (not b884) ) :assumption (or b103 (not b884) ) :assumption (or (>= r265 (* 502 2)) (not b884) ) :assumption (or (= r284 0) b889 ) :assumption (or b889 (= r285 0) ) :assumption (or (not b889) (= r285 (* (~ 834) 2)) ) :assumption (or (not b889) (= r284 (* 834 2)) ) :assumption (or b107 (not b889) ) :assumption (or (not b95) (not b889) ) :assumption (or b288 (not b889) ) :assumption (or (not b889) (>= r256 (* 834 2)) ) :assumption (or (= r286 0) b895 ) :assumption (or b895 (= r287 0) ) :assumption (or (not b895) (= r287 (* (~ 834) 2)) ) :assumption (or (not b895) (= r286 (* 834 2)) ) :assumption (or b111 (not b895) ) :assumption (or (not b99) (not b895) ) :assumption (or b95 (not b895) ) :assumption (or (not b895) (>= r259 (* 834 2)) ) :assumption (or (= r288 0) b901 ) :assumption (or b901 (= r289 0) ) :assumption (or (not b901) (= r289 (* (~ 834) 2)) ) :assumption (or (not b901) (= r288 (* 834 2)) ) :assumption (or b115 (not b901) ) :assumption (or (not b103) (not b901) ) :assumption (or b99 (not b901) ) :assumption (or (not b901) (>= r262 (* 834 2)) ) :assumption (or (= r290 0) b907 ) :assumption (or b907 (= r291 0) ) :assumption (or (not b907) (= r291 (* (~ 834) 2)) ) :assumption (or (not b907) (= r290 (* 834 2)) ) :assumption (or (not b835) (not b907) ) :assumption (or b103 (not b907) ) :assumption (or (not b907) (>= r265 (* 834 2)) ) :assumption (or (= r292 0) b913 ) :assumption (or b913 (= r293 0) ) :assumption (or (not b913) (= r293 (* (~ 743) 2)) ) :assumption (or (not b913) (= r292 (* 743 2)) ) :assumption (or b84 (not b913) ) :assumption (or (not b107) (not b913) ) :assumption (or b170 (not b913) ) :assumption (or (>= r256 (* 743 2)) (not b913) ) :assumption (or (= r294 0) b918 ) :assumption (or b918 (= r295 0) ) :assumption (or (not b918) (= r295 (* (~ 743) 2)) ) :assumption (or (not b918) (= r294 (* 743 2)) ) :assumption (or b89 (not b918) ) :assumption (or (not b111) (not b918) ) :assumption (or b107 (not b918) ) :assumption (or (>= r259 (* 743 2)) (not b918) ) :assumption (or (= r296 0) b923 ) :assumption (or b923 (= r297 0) ) :assumption (or (not b923) (= r297 (* (~ 743) 2)) ) :assumption (or (not b923) (= r296 (* 743 2)) ) :assumption (or b161 (not b923) ) :assumption (or (not b115) (not b923) ) :assumption (or b111 (not b923) ) :assumption (or (>= r262 (* 743 2)) (not b923) ) :assumption (or (= r300 0) b930 ) :assumption (or b930 (= r301 0) ) :assumption (or (not b930) (= r301 (* (~ 834) 2)) ) :assumption (or (not b930) (= r300 (* 834 2)) ) :assumption (or b95 (not b930) ) :assumption (or (not b107) (not b930) ) :assumption (or b170 (not b930) ) :assumption (or (>= r256 (* 834 2)) (not b930) ) :assumption (or (= r302 0) b935 ) :assumption (or b935 (= r303 0) ) :assumption (or (not b935) (= r303 (* (~ 834) 2)) ) :assumption (or (not b935) (= r302 (* 834 2)) ) :assumption (or b99 (not b935) ) :assumption (or (not b111) (not b935) ) :assumption (or b107 (not b935) ) :assumption (or (>= r259 (* 834 2)) (not b935) ) :assumption (or (= r304 0) b940 ) :assumption (or b940 (= r305 0) ) :assumption (or (not b940) (= r305 (* (~ 834) 2)) ) :assumption (or (not b940) (= r304 (* 834 2)) ) :assumption (or b103 (not b940) ) :assumption (or (not b115) (not b940) ) :assumption (or b111 (not b940) ) :assumption (or (>= r262 (* 834 2)) (not b940) ) :assumption (or (= r308 0) b947 ) :assumption (or b947 (= r309 0) ) :assumption (or (not b947) (= r309 (* (~ 502) 4)) ) :assumption (or (not b947) (= r308 (* 502 4)) ) :assumption (or b255 (not b947) ) :assumption (or (not b24) (not b947) ) :assumption (or (not b947) (>= r10 (* 502 4)) ) :assumption (or (not b947) (<= r9 7) ) :assumption (or (= r310 0) b954 ) :assumption (or b954 (= r311 0) ) :assumption (or (not b954) (= r311 (* (~ 502) 4)) ) :assumption (or (not b954) (= r310 (* 502 4)) ) :assumption (or b44 (not b954) ) :assumption (or (not b30) (not b954) ) :assumption (or b24 (not b954) ) :assumption (or (not b954) (>= r200 (* 502 4)) ) :assumption (or (not b954) (<= r312 7) ) :assumption (or (= r313 0) b961 ) :assumption (or b961 (= r314 0) ) :assumption (or (not b961) (= r314 (* (~ 502) 4)) ) :assumption (or (not b961) (= r313 (* 502 4)) ) :assumption (or b49 (not b961) ) :assumption (or (not b36) (not b961) ) :assumption (or b30 (not b961) ) :assumption (or (not b961) (>= r203 (* 502 4)) ) :assumption (or (not b961) (<= r315 7) ) :assumption (or (= r316 0) b968 ) :assumption (or b968 (= r317 0) ) :assumption (or (not b968) (= r317 (* (~ 502) 4)) ) :assumption (or (not b968) (= r316 (* 502 4)) ) :assumption (or b54 (not b968) ) :assumption (or (not b127) (not b968) ) :assumption (or b36 (not b968) ) :assumption (or (not b968) (>= r206 (* 502 4)) ) :assumption (or (not b968) (<= r318 7) ) :assumption (or (= r319 0) b975 ) :assumption (or b975 (= r320 0) ) :assumption (or (not b975) (= r320 (* (~ 502) 4)) ) :assumption (or (not b975) (= r319 (* 502 4)) ) :assumption (or b688 (not b975) ) :assumption (or (not b689) (not b975) ) :assumption (or b127 (not b975) ) :assumption (or (not b975) (>= r209 (* 502 4)) ) :assumption (or (not b975) (<= r321 7) ) :assumption (or (= r322 0) b982 ) :assumption (or b982 (= r323 0) ) :assumption (or (not b982) (= r323 (* (~ 743) 4)) ) :assumption (or (not b982) (= r322 (* 743 4)) ) :assumption (or b139 (not b982) ) :assumption (or (not b24) (not b982) ) :assumption (or (not b982) (>= r10 (* 743 4)) ) :assumption (or (<= r9 7) (not b982) ) :assumption (or (= r324 0) b988 ) :assumption (or b988 (= r325 0) ) :assumption (or (not b988) (= r325 (* (~ 743) 4)) ) :assumption (or (not b988) (= r324 (* 743 4)) ) :assumption (or b60 (not b988) ) :assumption (or (not b30) (not b988) ) :assumption (or b24 (not b988) ) :assumption (or (not b988) (>= r200 (* 743 4)) ) :assumption (or (<= r312 7) (not b988) ) :assumption (or (= r326 0) b994 ) :assumption (or b994 (= r327 0) ) :assumption (or (not b994) (= r327 (* (~ 743) 4)) ) :assumption (or (not b994) (= r326 (* 743 4)) ) :assumption (or b65 (not b994) ) :assumption (or (not b36) (not b994) ) :assumption (or b30 (not b994) ) :assumption (or (not b994) (>= r203 (* 743 4)) ) :assumption (or (<= r315 7) (not b994) ) :assumption (or (= r328 0) b1000 ) :assumption (or b1000 (= r329 0) ) :assumption (or (not b1000) (= r329 (* (~ 743) 4)) ) :assumption (or (not b1000) (= r328 (* 743 4)) ) :assumption (or b70 (not b1000) ) :assumption (or (not b127) (not b1000) ) :assumption (or b36 (not b1000) ) :assumption (or (not b1000) (>= r206 (* 743 4)) ) :assumption (or (<= r318 7) (not b1000) ) :assumption (or (= r330 0) b1006 ) :assumption (or b1006 (= r331 0) ) :assumption (or (not b1006) (= r331 (* (~ 743) 4)) ) :assumption (or (not b1006) (= r330 (* 743 4)) ) :assumption (or b720 (not b1006) ) :assumption (or (not b689) (not b1006) ) :assumption (or b127 (not b1006) ) :assumption (or (not b1006) (>= r209 (* 743 4)) ) :assumption (or (<= r321 7) (not b1006) ) :assumption (or (= r332 0) b1012 ) :assumption (or b1012 (= r333 0) ) :assumption (or (not b1012) (= r333 (* (~ 502) 4)) ) :assumption (or (not b1012) (= r332 (* 502 4)) ) :assumption (or b30 (not b1012) ) :assumption (or (not b44) (not b1012) ) :assumption (or b255 (not b1012) ) :assumption (or (>= r200 (* 502 4)) (not b1012) ) :assumption (or (<= r312 7) (not b1012) ) :assumption (or (= r334 0) b1017 ) :assumption (or b1017 (= r335 0) ) :assumption (or (not b1017) (= r335 (* (~ 502) 4)) ) :assumption (or (not b1017) (= r334 (* 502 4)) ) :assumption (or b36 (not b1017) ) :assumption (or (not b49) (not b1017) ) :assumption (or b44 (not b1017) ) :assumption (or (>= r203 (* 502 4)) (not b1017) ) :assumption (or (<= r315 7) (not b1017) ) :assumption (or (= r336 0) b1022 ) :assumption (or b1022 (= r337 0) ) :assumption (or (not b1022) (= r337 (* (~ 502) 4)) ) :assumption (or (not b1022) (= r336 (* 502 4)) ) :assumption (or b127 (not b1022) ) :assumption (or (not b54) (not b1022) ) :assumption (or b49 (not b1022) ) :assumption (or (>= r206 (* 502 4)) (not b1022) ) :assumption (or (<= r318 7) (not b1022) ) :assumption (or (= r338 0) b1027 ) :assumption (or b1027 (= r339 0) ) :assumption (or (not b1027) (= r339 (* (~ 502) 4)) ) :assumption (or (not b1027) (= r338 (* 502 4)) ) :assumption (or b689 (not b1027) ) :assumption (or (not b688) (not b1027) ) :assumption (or b54 (not b1027) ) :assumption (or (>= r209 (* 502 4)) (not b1027) ) :assumption (or (<= r321 7) (not b1027) ) :assumption (or (= r340 0) b1032 ) :assumption (or b1032 (= r341 0) ) :assumption (or (not b1032) (= r341 (* (~ 834) 4)) ) :assumption (or (not b1032) (= r340 (* 834 4)) ) :assumption (or b60 (not b1032) ) :assumption (or (not b44) (not b1032) ) :assumption (or b255 (not b1032) ) :assumption (or (not b1032) (>= r200 (* 834 4)) ) :assumption (or (<= r312 7) (not b1032) ) :assumption (or (= r342 0) b1038 ) :assumption (or b1038 (= r343 0) ) :assumption (or (not b1038) (= r343 (* (~ 834) 4)) ) :assumption (or (not b1038) (= r342 (* 834 4)) ) :assumption (or b65 (not b1038) ) :assumption (or (not b49) (not b1038) ) :assumption (or b44 (not b1038) ) :assumption (or (not b1038) (>= r203 (* 834 4)) ) :assumption (or (<= r315 7) (not b1038) ) :assumption (or (= r344 0) b1044 ) :assumption (or b1044 (= r345 0) ) :assumption (or (not b1044) (= r345 (* (~ 834) 4)) ) :assumption (or (not b1044) (= r344 (* 834 4)) ) :assumption (or b70 (not b1044) ) :assumption (or (not b54) (not b1044) ) :assumption (or b49 (not b1044) ) :assumption (or (not b1044) (>= r206 (* 834 4)) ) :assumption (or (<= r318 7) (not b1044) ) :assumption (or (= r346 0) b1050 ) :assumption (or b1050 (= r347 0) ) :assumption (or (not b1050) (= r347 (* (~ 834) 4)) ) :assumption (or (not b1050) (= r346 (* 834 4)) ) :assumption (or b720 (not b1050) ) :assumption (or (not b688) (not b1050) ) :assumption (or b54 (not b1050) ) :assumption (or (not b1050) (>= r209 (* 834 4)) ) :assumption (or (<= r321 7) (not b1050) ) :assumption (or (= r348 0) b1056 ) :assumption (or b1056 (= r349 0) ) :assumption (or (not b1056) (= r349 (* (~ 743) 4)) ) :assumption (or (not b1056) (= r348 (* 743 4)) ) :assumption (or b30 (not b1056) ) :assumption (or (not b60) (not b1056) ) :assumption (or b139 (not b1056) ) :assumption (or (>= r200 (* 743 4)) (not b1056) ) :assumption (or (<= r312 7) (not b1056) ) :assumption (or (= r350 0) b1061 ) :assumption (or b1061 (= r351 0) ) :assumption (or (not b1061) (= r351 (* (~ 743) 4)) ) :assumption (or (not b1061) (= r350 (* 743 4)) ) :assumption (or b36 (not b1061) ) :assumption (or (not b65) (not b1061) ) :assumption (or b60 (not b1061) ) :assumption (or (>= r203 (* 743 4)) (not b1061) ) :assumption (or (<= r315 7) (not b1061) ) :assumption (or (= r352 0) b1066 ) :assumption (or b1066 (= r353 0) ) :assumption (or (not b1066) (= r353 (* (~ 743) 4)) ) :assumption (or (not b1066) (= r352 (* 743 4)) ) :assumption (or b127 (not b1066) ) :assumption (or (not b70) (not b1066) ) :assumption (or b65 (not b1066) ) :assumption (or (>= r206 (* 743 4)) (not b1066) ) :assumption (or (<= r318 7) (not b1066) ) :assumption (or (= r354 0) b1071 ) :assumption (or b1071 (= r355 0) ) :assumption (or (not b1071) (= r355 (* (~ 743) 4)) ) :assumption (or (not b1071) (= r354 (* 743 4)) ) :assumption (or b689 (not b1071) ) :assumption (or (not b720) (not b1071) ) :assumption (or b70 (not b1071) ) :assumption (or (>= r209 (* 743 4)) (not b1071) ) :assumption (or (<= r321 7) (not b1071) ) :assumption (or (= r356 0) b1076 ) :assumption (or b1076 (= r357 0) ) :assumption (or (not b1076) (= r357 (* (~ 834) 4)) ) :assumption (or (not b1076) (= r356 (* 834 4)) ) :assumption (or b44 (not b1076) ) :assumption (or (not b60) (not b1076) ) :assumption (or b139 (not b1076) ) :assumption (or (>= r200 (* 834 4)) (not b1076) ) :assumption (or (<= r312 7) (not b1076) ) :assumption (or (= r358 0) b1081 ) :assumption (or b1081 (= r359 0) ) :assumption (or (not b1081) (= r359 (* (~ 834) 4)) ) :assumption (or (not b1081) (= r358 (* 834 4)) ) :assumption (or b49 (not b1081) ) :assumption (or (not b65) (not b1081) ) :assumption (or b60 (not b1081) ) :assumption (or (>= r203 (* 834 4)) (not b1081) ) :assumption (or (<= r315 7) (not b1081) ) :assumption (or (= r360 0) b1086 ) :assumption (or b1086 (= r361 0) ) :assumption (or (not b1086) (= r361 (* (~ 834) 4)) ) :assumption (or (not b1086) (= r360 (* 834 4)) ) :assumption (or b54 (not b1086) ) :assumption (or (not b70) (not b1086) ) :assumption (or b65 (not b1086) ) :assumption (or (>= r206 (* 834 4)) (not b1086) ) :assumption (or (<= r318 7) (not b1086) ) :assumption (or (= r362 0) b1091 ) :assumption (or b1091 (= r363 0) ) :assumption (or (not b1091) (= r363 (* (~ 834) 4)) ) :assumption (or (not b1091) (= r362 (* 834 4)) ) :assumption (or b688 (not b1091) ) :assumption (or (not b720) (not b1091) ) :assumption (or b70 (not b1091) ) :assumption (or (>= r209 (* 834 4)) (not b1091) ) :assumption (or (<= r321 7) (not b1091) ) :assumption (or (= r364 0) b1096 ) :assumption (or b1096 (= r365 0) ) :assumption (or (not b1096) (= r365 (* (~ 502) 7)) ) :assumption (or (not b1096) (= r364 (* 502 7)) ) :assumption (or b288 (not b1096) ) :assumption (or (not b79) (not b1096) ) :assumption (or (not b1096) (>= r12 (* 502 7)) ) :assumption (or (not b1096) (<= r11 2) ) :assumption (or (= r366 0) b1103 ) :assumption (or b1103 (= r367 0) ) :assumption (or (not b1103) (= r367 (* (~ 502) 7)) ) :assumption (or (not b1103) (= r366 (* 502 7)) ) :assumption (or b95 (not b1103) ) :assumption (or (not b84) (not b1103) ) :assumption (or b79 (not b1103) ) :assumption (or (not b1103) (>= r256 (* 502 7)) ) :assumption (or (not b1103) (<= r368 2) ) :assumption (or (= r369 0) b1110 ) :assumption (or b1110 (= r370 0) ) :assumption (or (not b1110) (= r370 (* (~ 502) 7)) ) :assumption (or (not b1110) (= r369 (* 502 7)) ) :assumption (or b99 (not b1110) ) :assumption (or (not b89) (not b1110) ) :assumption (or b84 (not b1110) ) :assumption (or (not b1110) (>= r259 (* 502 7)) ) :assumption (or (not b1110) (<= r371 2) ) :assumption (or (= r372 0) b1117 ) :assumption (or b1117 (= r373 0) ) :assumption (or (not b1117) (= r373 (* (~ 502) 7)) ) :assumption (or (not b1117) (= r372 (* 502 7)) ) :assumption (or b103 (not b1117) ) :assumption (or (not b161) (not b1117) ) :assumption (or b89 (not b1117) ) :assumption (or (not b1117) (>= r262 (* 502 7)) ) :assumption (or (not b1117) (<= r374 2) ) :assumption (or (= r375 0) b1124 ) :assumption (or b1124 (= r376 0) ) :assumption (or (not b1124) (= r376 (* (~ 502) 7)) ) :assumption (or (not b1124) (= r375 (* 502 7)) ) :assumption (or b835 (not b1124) ) :assumption (or (not b836) (not b1124) ) :assumption (or b161 (not b1124) ) :assumption (or (not b1124) (>= r265 (* 502 7)) ) :assumption (or (not b1124) (<= r377 2) ) :assumption (or (= r378 0) b1131 ) :assumption (or b1131 (= r379 0) ) :assumption (or (not b1131) (= r379 (* (~ 743) 7)) ) :assumption (or (not b1131) (= r378 (* 743 7)) ) :assumption (or b170 (not b1131) ) :assumption (or (not b79) (not b1131) ) :assumption (or (not b1131) (>= r12 (* 743 7)) ) :assumption (or (<= r11 2) (not b1131) ) :assumption (or (= r380 0) b1137 ) :assumption (or b1137 (= r381 0) ) :assumption (or (not b1137) (= r381 (* (~ 743) 7)) ) :assumption (or (not b1137) (= r380 (* 743 7)) ) :assumption (or b107 (not b1137) ) :assumption (or (not b84) (not b1137) ) :assumption (or b79 (not b1137) ) :assumption (or (not b1137) (>= r256 (* 743 7)) ) :assumption (or (<= r368 2) (not b1137) ) :assumption (or (= r382 0) b1143 ) :assumption (or b1143 (= r383 0) ) :assumption (or (not b1143) (= r383 (* (~ 743) 7)) ) :assumption (or (not b1143) (= r382 (* 743 7)) ) :assumption (or b111 (not b1143) ) :assumption (or (not b89) (not b1143) ) :assumption (or b84 (not b1143) ) :assumption (or (not b1143) (>= r259 (* 743 7)) ) :assumption (or (<= r371 2) (not b1143) ) :assumption (or (= r384 0) b1149 ) :assumption (or b1149 (= r385 0) ) :assumption (or (not b1149) (= r385 (* (~ 743) 7)) ) :assumption (or (not b1149) (= r384 (* 743 7)) ) :assumption (or b115 (not b1149) ) :assumption (or (not b161) (not b1149) ) :assumption (or b89 (not b1149) ) :assumption (or (not b1149) (>= r262 (* 743 7)) ) :assumption (or (<= r374 2) (not b1149) ) :assumption (or (= r386 0) b1155 ) :assumption (or b1155 (= r387 0) ) :assumption (or (not b1155) (= r387 (* (~ 743) 7)) ) :assumption (or (not b1155) (= r386 (* 743 7)) ) :assumption (or (not b836) (not b1155) ) :assumption (or b161 (not b1155) ) :assumption (or (not b1155) (>= r265 (* 743 7)) ) :assumption (or (<= r377 2) (not b1155) ) :assumption (or (= r388 0) b1161 ) :assumption (or b1161 (= r389 0) ) :assumption (or (not b1161) (= r389 (* (~ 502) 7)) ) :assumption (or (not b1161) (= r388 (* 502 7)) ) :assumption (or b84 (not b1161) ) :assumption (or (not b95) (not b1161) ) :assumption (or b288 (not b1161) ) :assumption (or (>= r256 (* 502 7)) (not b1161) ) :assumption (or (<= r368 2) (not b1161) ) :assumption (or (= r390 0) b1166 ) :assumption (or b1166 (= r391 0) ) :assumption (or (not b1166) (= r391 (* (~ 502) 7)) ) :assumption (or (not b1166) (= r390 (* 502 7)) ) :assumption (or b89 (not b1166) ) :assumption (or (not b99) (not b1166) ) :assumption (or b95 (not b1166) ) :assumption (or (>= r259 (* 502 7)) (not b1166) ) :assumption (or (<= r371 2) (not b1166) ) :assumption (or (= r392 0) b1171 ) :assumption (or b1171 (= r393 0) ) :assumption (or (not b1171) (= r393 (* (~ 502) 7)) ) :assumption (or (not b1171) (= r392 (* 502 7)) ) :assumption (or b161 (not b1171) ) :assumption (or (not b103) (not b1171) ) :assumption (or b99 (not b1171) ) :assumption (or (>= r262 (* 502 7)) (not b1171) ) :assumption (or (<= r374 2) (not b1171) ) :assumption (or (= r394 0) b1176 ) :assumption (or b1176 (= r395 0) ) :assumption (or (not b1176) (= r395 (* (~ 502) 7)) ) :assumption (or (not b1176) (= r394 (* 502 7)) ) :assumption (or b836 (not b1176) ) :assumption (or (not b835) (not b1176) ) :assumption (or b103 (not b1176) ) :assumption (or (>= r265 (* 502 7)) (not b1176) ) :assumption (or (<= r377 2) (not b1176) ) :assumption (or (= r396 0) b1181 ) :assumption (or b1181 (= r397 0) ) :assumption (or (not b1181) (= r397 (* (~ 834) 7)) ) :assumption (or (not b1181) (= r396 (* 834 7)) ) :assumption (or b107 (not b1181) ) :assumption (or (not b95) (not b1181) ) :assumption (or b288 (not b1181) ) :assumption (or (not b1181) (>= r256 (* 834 7)) ) :assumption (or (<= r368 2) (not b1181) ) :assumption (or (= r398 0) b1187 ) :assumption (or b1187 (= r399 0) ) :assumption (or (not b1187) (= r399 (* (~ 834) 7)) ) :assumption (or (not b1187) (= r398 (* 834 7)) ) :assumption (or b111 (not b1187) ) :assumption (or (not b99) (not b1187) ) :assumption (or b95 (not b1187) ) :assumption (or (not b1187) (>= r259 (* 834 7)) ) :assumption (or (<= r371 2) (not b1187) ) :assumption (or (= r400 0) b1193 ) :assumption (or b1193 (= r401 0) ) :assumption (or (not b1193) (= r401 (* (~ 834) 7)) ) :assumption (or (not b1193) (= r400 (* 834 7)) ) :assumption (or b115 (not b1193) ) :assumption (or (not b103) (not b1193) ) :assumption (or b99 (not b1193) ) :assumption (or (not b1193) (>= r262 (* 834 7)) ) :assumption (or (<= r374 2) (not b1193) ) :assumption (or (= r402 0) b1199 ) :assumption (or b1199 (= r403 0) ) :assumption (or (not b1199) (= r403 (* (~ 834) 7)) ) :assumption (or (not b1199) (= r402 (* 834 7)) ) :assumption (or (not b835) (not b1199) ) :assumption (or b103 (not b1199) ) :assumption (or (not b1199) (>= r265 (* 834 7)) ) :assumption (or (<= r377 2) (not b1199) ) :assumption (or (= r404 0) b1205 ) :assumption (or b1205 (= r405 0) ) :assumption (or (not b1205) (= r405 (* (~ 743) 7)) ) :assumption (or (not b1205) (= r404 (* 743 7)) ) :assumption (or b84 (not b1205) ) :assumption (or (not b107) (not b1205) ) :assumption (or b170 (not b1205) ) :assumption (or (>= r256 (* 743 7)) (not b1205) ) :assumption (or (<= r368 2) (not b1205) ) :assumption (or (= r406 0) b1210 ) :assumption (or b1210 (= r407 0) ) :assumption (or (not b1210) (= r407 (* (~ 743) 7)) ) :assumption (or (not b1210) (= r406 (* 743 7)) ) :assumption (or b89 (not b1210) ) :assumption (or (not b111) (not b1210) ) :assumption (or b107 (not b1210) ) :assumption (or (>= r259 (* 743 7)) (not b1210) ) :assumption (or (<= r371 2) (not b1210) ) :assumption (or (= r408 0) b1215 ) :assumption (or b1215 (= r409 0) ) :assumption (or (not b1215) (= r409 (* (~ 743) 7)) ) :assumption (or (not b1215) (= r408 (* 743 7)) ) :assumption (or b161 (not b1215) ) :assumption (or (not b115) (not b1215) ) :assumption (or b111 (not b1215) ) :assumption (or (>= r262 (* 743 7)) (not b1215) ) :assumption (or (<= r374 2) (not b1215) ) :assumption (or (= r412 0) b1222 ) :assumption (or b1222 (= r413 0) ) :assumption (or (not b1222) (= r413 (* (~ 834) 7)) ) :assumption (or (not b1222) (= r412 (* 834 7)) ) :assumption (or b95 (not b1222) ) :assumption (or (not b107) (not b1222) ) :assumption (or b170 (not b1222) ) :assumption (or (>= r256 (* 834 7)) (not b1222) ) :assumption (or (<= r368 2) (not b1222) ) :assumption (or (= r414 0) b1227 ) :assumption (or b1227 (= r415 0) ) :assumption (or (not b1227) (= r415 (* (~ 834) 7)) ) :assumption (or (not b1227) (= r414 (* 834 7)) ) :assumption (or b99 (not b1227) ) :assumption (or (not b111) (not b1227) ) :assumption (or b107 (not b1227) ) :assumption (or (>= r259 (* 834 7)) (not b1227) ) :assumption (or (<= r371 2) (not b1227) ) :assumption (or (= r416 0) b1232 ) :assumption (or b1232 (= r417 0) ) :assumption (or (not b1232) (= r417 (* (~ 834) 7)) ) :assumption (or (not b1232) (= r416 (* 834 7)) ) :assumption (or b103 (not b1232) ) :assumption (or (not b115) (not b1232) ) :assumption (or b111 (not b1232) ) :assumption (or (>= r262 (* 834 7)) (not b1232) ) :assumption (or (<= r374 2) (not b1232) ) :assumption (or (not b1238) (= r200 6148) ) :assumption (or (not b1238) (< (+ r10 r420) 6148) ) :assumption (or (not b1241) (= r203 6148) ) :assumption (or (not b1241) (< (+ r200 r420) 6148) ) :assumption (or b24 (not b1241) ) :assumption (or (not b1244) (= r206 6148) ) :assumption (or (not b1244) (< (+ r203 r420) 6148) ) :assumption (or b30 (not b1244) ) :assumption (or (not b1247) (= r209 6148) ) :assumption (or (not b1247) (< (+ r206 r420) 6148) ) :assumption (or b36 (not b1247) ) :assumption (or (not b1250) (= r421 6148) ) :assumption (or (not b1250) (< (+ r209 r420) 6148) ) :assumption (or b127 (not b1250) ) :assumption (or (= r203 6148) (not b1253) ) :assumption (or (< (+ r200 r420) 6148) (not b1253) ) :assumption (or b255 (not b1253) ) :assumption (or (= r206 6148) (not b1254) ) :assumption (or (< (+ r203 r420) 6148) (not b1254) ) :assumption (or b44 (not b1254) ) :assumption (or (= r209 6148) (not b1255) ) :assumption (or (< (+ r206 r420) 6148) (not b1255) ) :assumption (or b49 (not b1255) ) :assumption (or (= r421 6148) (not b1256) ) :assumption (or (< (+ r209 r420) 6148) (not b1256) ) :assumption (or b54 (not b1256) ) :assumption (or (= r203 6148) (not b1257) ) :assumption (or (< (+ r200 r420) 6148) (not b1257) ) :assumption (or b139 (not b1257) ) :assumption (or (= r206 6148) (not b1258) ) :assumption (or (< (+ r203 r420) 6148) (not b1258) ) :assumption (or b60 (not b1258) ) :assumption (or (= r209 6148) (not b1259) ) :assumption (or (< (+ r206 r420) 6148) (not b1259) ) :assumption (or b65 (not b1259) ) :assumption (or (= r421 6148) (not b1260) ) :assumption (or (< (+ r209 r420) 6148) (not b1260) ) :assumption (or b70 (not b1260) ) :assumption (or (not b1261) (= r256 5304) ) :assumption (or (not b1261) (< (+ r12 r420) 5304) ) :assumption (or (not b1264) (= r259 5304) ) :assumption (or (not b1264) (< (+ r256 r420) 5304) ) :assumption (or b79 (not b1264) ) :assumption (or (not b1267) (= r262 5304) ) :assumption (or (not b1267) (< (+ r259 r420) 5304) ) :assumption (or b84 (not b1267) ) :assumption (or (not b1270) (= r265 5304) ) :assumption (or (not b1270) (< (+ r262 r420) 5304) ) :assumption (or b89 (not b1270) ) :assumption (or (not b1273) (= r422 5304) ) :assumption (or (not b1273) (< (+ r265 r420) 5304) ) :assumption (or b161 (not b1273) ) :assumption (or (= r259 5304) (not b1276) ) :assumption (or (< (+ r256 r420) 5304) (not b1276) ) :assumption (or b288 (not b1276) ) :assumption (or (= r262 5304) (not b1277) ) :assumption (or (< (+ r259 r420) 5304) (not b1277) ) :assumption (or b95 (not b1277) ) :assumption (or (= r265 5304) (not b1278) ) :assumption (or (< (+ r262 r420) 5304) (not b1278) ) :assumption (or b99 (not b1278) ) :assumption (or (= r422 5304) (not b1279) ) :assumption (or (< (+ r265 r420) 5304) (not b1279) ) :assumption (or b103 (not b1279) ) :assumption (or (= r259 5304) (not b1280) ) :assumption (or (< (+ r256 r420) 5304) (not b1280) ) :assumption (or b170 (not b1280) ) :assumption (or (= r262 5304) (not b1281) ) :assumption (or (< (+ r259 r420) 5304) (not b1281) ) :assumption (or b107 (not b1281) ) :assumption (or (= r265 5304) (not b1282) ) :assumption (or (< (+ r262 r420) 5304) (not b1282) ) :assumption (or b111 (not b1282) ) :assumption (or (= r422 5304) (not b1283) ) :assumption (or (< (+ r265 r420) 5304) (not b1283) ) :assumption (or b115 (not b1283) ) :assumption (or (or (not b170) b839 ) b1131 ) :assumption (or (or (or (or (or (not b107) b170 ) b845 ) b889 ) b1137 ) b1181 ) :assumption (or (or (or (or (or b107 (not b170) ) b913 ) b930 ) b1205 ) b1222 ) :assumption (or (or (or (or (or b107 (not b111) ) b851 ) b895 ) b1143 ) b1187 ) :assumption (or (or (or (or (or (not b107) b111 ) b918 ) b935 ) b1210 ) b1227 ) :assumption (or (or (or (or (or b111 (not b115) ) b857 ) b901 ) b1149 ) b1193 ) :assumption (or (or (or (or (or (not b111) b115 ) b923 ) b940 ) b1215 ) b1232 ) :assumption (or (or (or (or b115 b863 ) b907 ) b1155 ) b1199 ) :assumption (or (or (not b288) b807 ) b1096 ) :assumption (or (or (or (or (or (not b95) b288 ) b813 ) b930 ) b1103 ) b1222 ) :assumption (or (or (or (or (or b95 (not b288) ) b869 ) b889 ) b1161 ) b1181 ) :assumption (or (or (or (or (or b95 (not b99) ) b819 ) b935 ) b1110 ) b1227 ) :assumption (or (or (or (or (or (not b95) b99 ) b874 ) b895 ) b1166 ) b1187 ) :assumption (or (or (or (or (or b99 (not b103) ) b825 ) b940 ) b1117 ) b1232 ) :assumption (or (or (or (or (or (not b99) b103 ) b879 ) b901 ) b1171 ) b1193 ) :assumption (or (or (or b103 b831 ) (not b835) ) b1124 ) :assumption (or (or (or (or (or (not b103) b835 ) b884 ) b907 ) b1176 ) b1199 ) :assumption (or (or (or (or b79 b807 ) b839 ) b1096 ) b1131 ) :assumption (or (or (or (or (or b79 (not b84) ) b869 ) b913 ) b1161 ) b1205 ) :assumption (or (or (or (or (or (not b79) b84 ) b813 ) b845 ) b1103 ) b1137 ) :assumption (or (or (or (or (or b84 (not b89) ) b874 ) b918 ) b1166 ) b1210 ) :assumption (or (or (or (or (or (not b84) b89 ) b819 ) b851 ) b1110 ) b1143 ) :assumption (or (or (or (or (or b89 (not b161) ) b879 ) b923 ) b1171 ) b1215 ) :assumption (or (or (or (or (or (not b89) b161 ) b825 ) b857 ) b1117 ) b1149 ) :assumption (or (or (or b161 (not b836) ) b884 ) b1176 ) :assumption (or (or (or (or (or (not b161) b831 ) b836 ) b863 ) b1124 ) b1155 ) :assumption (or (or (not b139) b692 ) b982 ) :assumption (or (or (or (or (or (not b60) b139 ) b698 ) b743 ) b988 ) b1032 ) :assumption (or (or (or (or (or b60 (not b139) ) b767 ) b787 ) b1056 ) b1076 ) :assumption (or (or (or (or (or b60 (not b65) ) b704 ) b749 ) b994 ) b1038 ) :assumption (or (or (or (or (or (not b60) b65 ) b772 ) b792 ) b1061 ) b1081 ) :assumption (or (or (or (or (or b65 (not b70) ) b710 ) b755 ) b1000 ) b1044 ) :assumption (or (or (or (or (or (not b65) b70 ) b777 ) b797 ) b1066 ) b1086 ) :assumption (or (or (or (or (or b70 b716 ) (not b720) ) b761 ) b1006 ) b1050 ) :assumption (or (or (or (or (or (not b70) b720 ) b782 ) b802 ) b1071 ) b1091 ) :assumption (or (or (not b255) b660 ) b947 ) :assumption (or (or (or (or (or (not b44) b255 ) b666 ) b787 ) b954 ) b1076 ) :assumption (or (or (or (or (or b44 (not b255) ) b723 ) b743 ) b1012 ) b1032 ) :assumption (or (or (or (or (or b44 (not b49) ) b672 ) b792 ) b961 ) b1081 ) :assumption (or (or (or (or (or (not b44) b49 ) b728 ) b749 ) b1017 ) b1038 ) :assumption (or (or (or (or (or b49 (not b54) ) b678 ) b797 ) b968 ) b1086 ) :assumption (or (or (or (or (or (not b49) b54 ) b733 ) b755 ) b1022 ) b1044 ) :assumption (or (or (or (or (or b54 b684 ) (not b688) ) b802 ) b975 ) b1091 ) :assumption (or (or (or (or (or (not b54) b688 ) b738 ) b761 ) b1027 ) b1050 ) :assumption (or (or (or (or b24 b660 ) b692 ) b947 ) b982 ) :assumption (or (or (or (or (or b24 (not b30) ) b723 ) b767 ) b1012 ) b1056 ) :assumption (or (or (or (or (or (not b24) b30 ) b666 ) b698 ) b954 ) b988 ) :assumption (or (or (or (or (or b30 (not b36) ) b728 ) b772 ) b1017 ) b1061 ) :assumption (or (or (or (or (or (not b30) b36 ) b672 ) b704 ) b961 ) b994 ) :assumption (or (or (or (or (or b36 (not b127) ) b733 ) b777 ) b1022 ) b1066 ) :assumption (or (or (or (or (or (not b36) b127 ) b678 ) b710 ) b968 ) b1000 ) :assumption (or (or (or (or (or b127 (not b689) ) b738 ) b782 ) b1027 ) b1071 ) :assumption (or (or (or (or (or (not b127) b684 ) b689 ) b716 ) b975 ) b1006 ) :assumption (or (or b326 b329 ) b358 ) :assumption (or (or (or b329 (not b334) ) b624 ) b651 ) :assumption (or (or (or (not b329) b331 ) b334 ) b362 ) :assumption (or (or (or b334 (not b338) ) b627 ) b654 ) :assumption (or (or (or (not b334) b336 ) b338 ) b366 ) :assumption (or (or (or b338 (not b342) ) b630 ) b657 ) :assumption (or (or (or (not b338) b340 ) b342 ) b369 ) :assumption (or (or (not b320) b615 ) b642 ) :assumption (or (or (or (not b319) b320 ) b618 ) b645 ) :assumption (or (or (or b317 b319 ) (not b320) ) b352 ) :assumption (or (or (or b319 (not b324) ) b621 ) b648 ) :assumption (or (or (or (not b319) b322 ) b324 ) b355 ) :assumption (or (or (not b310) b606 ) b633 ) :assumption (or (or (or (not b309) b310 ) b609 ) b636 ) :assumption (or (or (or b306 b309 ) (not b310) ) b344 ) :assumption (or (or (or b309 (not b315) ) b612 ) b639 ) :assumption (or (or (or (not b309) b312 ) b315 ) b348 ) :assumption (or (or (not b273) b570 ) b597 ) :assumption (or (or (or (not b272) b273 ) b573 ) b600 ) :assumption (or (or (or b270 b272 ) (not b273) ) b300 ) :assumption (or (or (or b272 (not b277) ) b576 ) b603 ) :assumption (or (or (or (not b272) b275 ) b277 ) b303 ) :assumption (or (or b251 b254 ) b285 ) :assumption (or (or (or b254 (not b260) ) b561 ) b588 ) :assumption (or (or (or (not b254) b257 ) b260 ) b290 ) :assumption (or (or (or b260 (not b264) ) b564 ) b591 ) :assumption (or (or (or (not b260) b262 ) b264 ) b294 ) :assumption (or (or (or b264 (not b268) ) b567 ) b594 ) :assumption (or (or (or (not b264) b266 ) b268 ) b297 ) :assumption (or (or (not b247) b552 ) b579 ) :assumption (or (or (or (not b246) b247 ) b555 ) b582 ) :assumption (or (or (or b243 b246 ) (not b247) ) b279 ) :assumption (or (or b246 b558 ) b585 ) :assumption (or (or b202 b205 ) b231 ) :assumption (or (or (or b205 (not b210) ) b516 ) b543 ) :assumption (or (or (or (not b205) b207 ) b210 ) b235 ) :assumption (or (or (or b210 (not b214) ) b519 ) b546 ) :assumption (or (or (or (not b210) b212 ) b214 ) b239 ) :assumption (or (or b214 b522 ) b549 ) :assumption (or (or (not b196) b507 ) b534 ) :assumption (or (or (or (not b195) b196 ) b510 ) b537 ) :assumption (or (or (or b193 b195 ) (not b196) ) b225 ) :assumption (or (or (or b195 (not b200) ) b513 ) b540 ) :assumption (or (or (or (not b195) b198 ) b200 ) b228 ) :assumption (or (or (not b186) b498 ) b525 ) :assumption (or (or (or (not b185) b186 ) b501 ) b528 ) :assumption (or (or (or b182 b185 ) (not b186) ) b217 ) :assumption (or (or (or b185 (not b191) ) b504 ) b531 ) :assumption (or (or (or (not b185) b188 ) b191 ) b221 ) :assumption (or (or b135 b138 ) b167 ) :assumption (or (or (or b138 (not b144) ) b462 ) b489 ) :assumption (or (or (or (not b138) b141 ) b144 ) b172 ) :assumption (or (or (or b144 (not b148) ) b465 ) b492 ) :assumption (or (or (or (not b144) b146 ) b148 ) b176 ) :assumption (or (or (or b148 (not b152) ) b468 ) b495 ) :assumption (or (or (or (not b148) b150 ) b152 ) b179 ) :assumption (or (or (not b132) b453 ) b480 ) :assumption (or (or (or (not b131) b132 ) b456 ) b483 ) :assumption (or (or (or b129 b131 ) (not b132) ) b163 ) :assumption (or (or b131 b459 ) b486 ) :assumption (or (or (not b121) b444 ) b471 ) :assumption (or (or (or (not b120) b121 ) b447 ) b474 ) :assumption (or (or (or b117 b120 ) (not b121) ) b154 ) :assumption (or (or (or b120 (not b126) ) b450 ) b477 ) :assumption (or (or (or (not b120) b123 ) b126 ) b158 ) :assumption (or (or (not b59) b396 ) b432 ) :assumption (or (or (or (not b58) b59 ) b399 ) b435 ) :assumption (or (or (or b56 b58 ) (not b59) ) b105 ) :assumption (or (or (or b58 (not b64) ) b402 ) b438 ) :assumption (or (or (or (not b58) b62 ) b64 ) b109 ) :assumption (or (or (or b64 (not b69) ) b405 ) b441 ) :assumption (or (or (or (not b64) b67 ) b69 ) b113 ) :assumption (or (or (not b43) b384 ) b420 ) :assumption (or (or (or (not b42) b43 ) b387 ) b423 ) :assumption (or (or (or b40 b42 ) (not b43) ) b93 ) :assumption (or (or (or b42 (not b48) ) b390 ) b426 ) :assumption (or (or (or (not b42) b46 ) b48 ) b97 ) :assumption (or (or (or b48 (not b53) ) b393 ) b429 ) :assumption (or (or (or (not b48) b51 ) b53 ) b101 ) :assumption (or (or b15 b18 ) b72 ) :assumption (or (or (or b18 (not b23) ) b372 ) b408 ) :assumption (or (or (or (not b18) b20 ) b23 ) b76 ) :assumption (or (or (or b23 (not b29) ) b375 ) b411 ) :assumption (or (or (or (not b23) b26 ) b29 ) b81 ) :assumption (or (or (or b29 (not b35) ) b378 ) b414 ) :assumption (or (or (or (not b29) b32 ) b35 ) b86 ) :assumption (or (or b35 b381 ) b417 ) :assumption (or b358 (not b360) ) :assumption (or (or b360 b362 ) (not b364) ) :assumption (or (or (or (or (not b360) b364 ) b633 ) b642 ) b651 ) :assumption (or (or (or (or b344 (not b346) ) b352 ) b364 ) b366 ) :assumption (or (or (or (or b346 (not b364) ) b636 ) b645 ) b654 ) :assumption (or (or (or (or b346 b348 ) (not b350) ) b355 ) b369 ) :assumption (or (or (or (or (not b346) b350 ) b639 ) b648 ) b657 ) :assumption (or b326 (not b328) ) :assumption (or (or b328 b331 ) (not b333) ) :assumption (or (or (or (or (not b328) b333 ) b606 ) b615 ) b624 ) :assumption (or (or (or (or b306 (not b308) ) b317 ) b333 ) b336 ) :assumption (or (or (or (or b308 (not b333) ) b609 ) b618 ) b627 ) :assumption (or (or (or (or b308 b312 ) (not b314) ) b322 ) b340 ) :assumption (or (or (or (or (not b308) b314 ) b612 ) b621 ) b630 ) :assumption (or b285 (not b287) ) :assumption (or (or b287 b290 ) (not b292) ) :assumption (or (or (or (or (not b287) b292 ) b579 ) b588 ) b597 ) :assumption (or (or (or (or b279 (not b281) ) b292 ) b294 ) b300 ) :assumption (or (or (or (or b281 (not b292) ) b582 ) b591 ) b600 ) :assumption (or (or (or b281 (not b283) ) b297 ) b303 ) :assumption (or (or (or (or (not b281) b283 ) b585 ) b594 ) b603 ) :assumption (or b251 (not b253) ) :assumption (or (or b253 b257 ) (not b259) ) :assumption (or (or (or (or (not b253) b259 ) b552 ) b561 ) b570 ) :assumption (or (or (or (or b243 (not b245) ) b259 ) b262 ) b270 ) :assumption (or (or (or (or b245 (not b259) ) b555 ) b564 ) b573 ) :assumption (or (or (or b245 (not b249) ) b266 ) b275 ) :assumption (or (or (or (or (not b245) b249 ) b558 ) b567 ) b576 ) :assumption (or b231 (not b233) ) :assumption (or (or b233 b235 ) (not b237) ) :assumption (or (or (or (or (not b233) b237 ) b525 ) b534 ) b543 ) :assumption (or (or (or (or b217 (not b219) ) b225 ) b237 ) b239 ) :assumption (or (or (or (or b219 (not b237) ) b528 ) b537 ) b546 ) :assumption (or (or (or b219 b221 ) (not b223) ) b228 ) :assumption (or (or (or (or (not b219) b223 ) b531 ) b540 ) b549 ) :assumption (or b202 (not b204) ) :assumption (or (or b204 b207 ) (not b209) ) :assumption (or (or (or (or (not b204) b209 ) b498 ) b507 ) b516 ) :assumption (or (or (or (or b182 (not b184) ) b193 ) b209 ) b212 ) :assumption (or (or (or (or b184 (not b209) ) b501 ) b510 ) b519 ) :assumption (or (or (or b184 b188 ) (not b190) ) b198 ) :assumption (or (or (or (or (not b184) b190 ) b504 ) b513 ) b522 ) :assumption (or b167 (not b169) ) :assumption (or (or b169 b172 ) (not b174) ) :assumption (or (or (or (or (not b169) b174 ) b471 ) b480 ) b489 ) :assumption (or (or (or (or b154 (not b156) ) b163 ) b174 ) b176 ) :assumption (or (or (or (or b156 (not b174) ) b474 ) b483 ) b492 ) :assumption (or (or (or b156 b158 ) (not b160) ) b179 ) :assumption (or (or (or (or (not b156) b160 ) b477 ) b486 ) b495 ) :assumption (or b135 (not b137) ) :assumption (or (or b137 b141 ) (not b143) ) :assumption (or (or (or (or (not b137) b143 ) b444 ) b453 ) b462 ) :assumption (or (or (or (or b117 (not b119) ) b129 ) b143 ) b146 ) :assumption (or (or (or (or b119 (not b143) ) b447 ) b456 ) b465 ) :assumption (or (or (or b119 b123 ) (not b125) ) b150 ) :assumption (or (or (or (or (not b119) b125 ) b450 ) b459 ) b468 ) :assumption (or b72 (not b74) ) :assumption (or (or b74 b76 ) (not b78) ) :assumption (or (or (or (or (not b74) b78 ) b408 ) b420 ) b432 ) :assumption (or (or (or (or b78 b81 ) (not b83) ) b93 ) b105 ) :assumption (or (or (or (or (not b78) b83 ) b411 ) b423 ) b435 ) :assumption (or (or (or (or b83 b86 ) (not b88) ) b97 ) b109 ) :assumption (or (or (or (or (not b83) b88 ) b414 ) b426 ) b438 ) :assumption (or (or (or b88 (not b91) ) b101 ) b113 ) :assumption (or (or (or (or (not b88) b91 ) b417 ) b429 ) b441 ) :assumption (or b15 (not b17) ) :assumption (or (or b17 b20 ) (not b22) ) :assumption (or (or (or (or (not b17) b22 ) b372 ) b384 ) b396 ) :assumption (or (or (or (or b22 b26 ) (not b28) ) b40 ) b56 ) :assumption (or (or (or (or (not b22) b28 ) b375 ) b387 ) b399 ) :assumption (or (or (or (or b28 b32 ) (not b34) ) b46 ) b62 ) :assumption (or (or (or (or (not b28) b34 ) b378 ) b390 ) b402 ) :assumption (or (or (or b34 (not b38) ) b51 ) b67 ) :assumption (or (or (or (or (not b34) b38 ) b381 ) b393 ) b405 ) :assumption (or b1238 (= (- (- (- (- (- r200 r10) r323) r309) r211) r197) 0) ) :assumption (or (or (or b1241 b1253 ) b1257 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r203 r200) r357) r349) r341) r333) r325) r311) r245) r237) r229) r221) r213) r199) 0) ) :assumption (or (or (or b1244 b1254 ) b1258 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r206 r203) r359) r351) r343) r335) r327) r314) r247) r239) r231) r223) r215) r202) 0) ) :assumption (or (or (or b1247 b1255 ) b1259 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r209 r206) r361) r353) r345) r337) r329) r317) r249) r241) r233) r225) r217) r205) 0) ) :assumption (or (or (or b1250 b1256 ) b1260 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r421 r209) r363) r355) r347) r339) r331) r320) r251) r243) r235) r227) r219) r208) 0) ) :assumption (or b1261 (= (- (- (- (- (- r256 r12) r379) r365) r267) r253) 0) ) :assumption (or (or (or b1264 b1276 ) b1280 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r259 r256) r413) r405) r397) r389) r381) r367) r301) r293) r285) r277) r269) r255) 0) ) :assumption (or (or (or b1267 b1277 ) b1281 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r262 r259) r415) r407) r399) r391) r383) r370) r303) r295) r287) r279) r271) r258) 0) ) :assumption (or (or (or b1270 b1278 ) b1282 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r265 r262) r417) r409) r401) r393) r385) r373) r305) r297) r289) r281) r273) r261) 0) ) :assumption (or (or (or b1273 b1279 ) b1283 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r422 r265) r419) r411) r403) r395) r387) r376) r307) r299) r291) r283) r275) r264) 0) ) :assumption (or (not b15) (not b72) ) :assumption (or (not b20) (not b76) ) :assumption (or (not b26) (not b81) ) :assumption (or (not b32) (not b86) ) :assumption (or (not b20) (not b408) ) :assumption (or (not b26) (not b411) ) :assumption (or (not b32) (not b414) ) :assumption (or (not b20) (not b372) ) :assumption (or (not b26) (not b375) ) :assumption (or (not b32) (not b378) ) :assumption (or (not b20) (not b396) ) :assumption (or (not b26) (not b399) ) :assumption (or (not b32) (not b402) ) :assumption (or (not b20) (not b384) ) :assumption (or (not b26) (not b387) ) :assumption (or (not b32) (not b390) ) :assumption (or (not b20) (not b1076) ) :assumption (or (not b26) (not b1081) ) :assumption (or (not b32) (not b1086) ) :assumption (or (not b20) (not b1056) ) :assumption (or (not b26) (not b1061) ) :assumption (or (not b32) (not b1066) ) :assumption (or (not b20) (not b1032) ) :assumption (or (not b26) (not b1038) ) :assumption (or (not b32) (not b1044) ) :assumption (or (not b20) (not b1012) ) :assumption (or (not b26) (not b1017) ) :assumption (or (not b32) (not b1022) ) :assumption (or (not b15) (not b982) ) :assumption (or (not b20) (not b988) ) :assumption (or (not b26) (not b994) ) :assumption (or (not b32) (not b1000) ) :assumption (or (not b15) (not b947) ) :assumption (or (not b20) (not b954) ) :assumption (or (not b26) (not b961) ) :assumption (or (not b32) (not b968) ) :assumption (or (not b40) (not b93) ) :assumption (or (not b46) (not b97) ) :assumption (or (not b51) (not b101) ) :assumption (or (not b40) (not b423) ) :assumption (or (not b46) (not b426) ) :assumption (or (not b51) (not b429) ) :assumption (or (not b40) (not b387) ) :assumption (or (not b46) (not b390) ) :assumption (or (not b51) (not b393) ) :assumption (or (not b40) (not b399) ) :assumption (or (not b46) (not b402) ) :assumption (or (not b51) (not b405) ) :assumption (or (not b40) (not b375) ) :assumption (or (not b46) (not b378) ) :assumption (or (not b51) (not b381) ) :assumption (or (not b40) (not b1081) ) :assumption (or (not b46) (not b1086) ) :assumption (or (not b51) (not b1091) ) :assumption (or (not b40) (not b1061) ) :assumption (or (not b46) (not b1066) ) :assumption (or (not b51) (not b1071) ) :assumption (or (not b40) (not b1038) ) :assumption (or (not b46) (not b1044) ) :assumption (or (not b51) (not b1050) ) :assumption (or (not b40) (not b1017) ) :assumption (or (not b46) (not b1022) ) :assumption (or (not b51) (not b1027) ) :assumption (or (not b40) (not b994) ) :assumption (or (not b46) (not b1000) ) :assumption (or (not b51) (not b1006) ) :assumption (or (not b40) (not b961) ) :assumption (or (not b46) (not b968) ) :assumption (or (not b51) (not b975) ) :assumption (or (not b56) (not b105) ) :assumption (or (not b62) (not b109) ) :assumption (or (not b67) (not b113) ) :assumption (or (not b56) (not b435) ) :assumption (or (not b62) (not b438) ) :assumption (or (not b67) (not b441) ) :assumption (or (not b56) (not b399) ) :assumption (or (not b62) (not b402) ) :assumption (or (not b67) (not b405) ) :assumption (or (not b56) (not b387) ) :assumption (or (not b62) (not b390) ) :assumption (or (not b67) (not b393) ) :assumption (or (not b56) (not b375) ) :assumption (or (not b62) (not b378) ) :assumption (or (not b67) (not b381) ) :assumption (or (not b56) (not b1081) ) :assumption (or (not b62) (not b1086) ) :assumption (or (not b67) (not b1091) ) :assumption (or (not b56) (not b1061) ) :assumption (or (not b62) (not b1066) ) :assumption (or (not b67) (not b1071) ) :assumption (or (not b56) (not b1038) ) :assumption (or (not b62) (not b1044) ) :assumption (or (not b67) (not b1050) ) :assumption (or (not b56) (not b1017) ) :assumption (or (not b62) (not b1022) ) :assumption (or (not b67) (not b1027) ) :assumption (or (not b56) (not b994) ) :assumption (or (not b62) (not b1000) ) :assumption (or (not b67) (not b1006) ) :assumption (or (not b56) (not b961) ) :assumption (or (not b62) (not b968) ) :assumption (or (not b67) (not b975) ) :assumption (or (not b76) (not b408) ) :assumption (or (not b81) (not b411) ) :assumption (or (not b86) (not b414) ) :assumption (or (not b76) (not b372) ) :assumption (or (not b81) (not b375) ) :assumption (or (not b86) (not b378) ) :assumption (or (not b76) (not b432) ) :assumption (or (not b81) (not b435) ) :assumption (or (not b86) (not b438) ) :assumption (or (not b76) (not b420) ) :assumption (or (not b81) (not b423) ) :assumption (or (not b86) (not b426) ) :assumption (or (not b76) (not b1222) ) :assumption (or (not b81) (not b1227) ) :assumption (or (not b86) (not b1232) ) :assumption (or (not b76) (not b1205) ) :assumption (or (not b81) (not b1210) ) :assumption (or (not b86) (not b1215) ) :assumption (or (not b76) (not b1181) ) :assumption (or (not b81) (not b1187) ) :assumption (or (not b86) (not b1193) ) :assumption (or (not b76) (not b1161) ) :assumption (or (not b81) (not b1166) ) :assumption (or (not b86) (not b1171) ) :assumption (or (not b72) (not b1131) ) :assumption (or (not b76) (not b1137) ) :assumption (or (not b81) (not b1143) ) :assumption (or (not b86) (not b1149) ) :assumption (or (not b72) (not b1096) ) :assumption (or (not b76) (not b1103) ) :assumption (or (not b81) (not b1110) ) :assumption (or (not b86) (not b1117) ) :assumption (or (not b93) (not b423) ) :assumption (or (not b97) (not b426) ) :assumption (or (not b101) (not b429) ) :assumption (or (not b93) (not b387) ) :assumption (or (not b97) (not b390) ) :assumption (or (not b101) (not b393) ) :assumption (or (not b93) (not b435) ) :assumption (or (not b97) (not b438) ) :assumption (or (not b101) (not b441) ) :assumption (or (not b93) (not b411) ) :assumption (or (not b97) (not b414) ) :assumption (or (not b101) (not b417) ) :assumption (or (not b93) (not b1227) ) :assumption (or (not b97) (not b1232) ) :assumption (or (not b93) (not b1210) ) :assumption (or (not b97) (not b1215) ) :assumption (or (not b93) (not b1187) ) :assumption (or (not b97) (not b1193) ) :assumption (or (not b101) (not b1199) ) :assumption (or (not b93) (not b1166) ) :assumption (or (not b97) (not b1171) ) :assumption (or (not b101) (not b1176) ) :assumption (or (not b93) (not b1143) ) :assumption (or (not b97) (not b1149) ) :assumption (or (not b101) (not b1155) ) :assumption (or (not b93) (not b1110) ) :assumption (or (not b97) (not b1117) ) :assumption (or (not b101) (not b1124) ) :assumption (or (not b105) (not b435) ) :assumption (or (not b109) (not b438) ) :assumption (or (not b113) (not b441) ) :assumption (or (not b105) (not b399) ) :assumption (or (not b109) (not b402) ) :assumption (or (not b113) (not b405) ) :assumption (or (not b105) (not b423) ) :assumption (or (not b109) (not b426) ) :assumption (or (not b113) (not b429) ) :assumption (or (not b105) (not b411) ) :assumption (or (not b109) (not b414) ) :assumption (or (not b113) (not b417) ) :assumption (or (not b105) (not b1227) ) :assumption (or (not b109) (not b1232) ) :assumption (or (not b105) (not b1210) ) :assumption (or (not b109) (not b1215) ) :assumption (or (not b105) (not b1187) ) :assumption (or (not b109) (not b1193) ) :assumption (or (not b113) (not b1199) ) :assumption (or (not b105) (not b1166) ) :assumption (or (not b109) (not b1171) ) :assumption (or (not b113) (not b1176) ) :assumption (or (not b105) (not b1143) ) :assumption (or (not b109) (not b1149) ) :assumption (or (not b113) (not b1155) ) :assumption (or (not b105) (not b1110) ) :assumption (or (not b109) (not b1117) ) :assumption (or (not b113) (not b1124) ) :assumption (or (not b117) (not b154) ) :assumption (or (not b123) (not b158) ) :assumption (or (not b117) (not b474) ) :assumption (or (not b123) (not b477) ) :assumption (or (not b117) (not b447) ) :assumption (or (not b123) (not b450) ) :assumption (or (not b117) (not b465) ) :assumption (or (not b123) (not b468) ) :assumption (or (not b117) (not b456) ) :assumption (or (not b123) (not b459) ) :assumption (or (not b117) (not b1086) ) :assumption (or (not b123) (not b1091) ) :assumption (or (not b117) (not b1066) ) :assumption (or (not b123) (not b1071) ) :assumption (or (not b117) (not b1044) ) :assumption (or (not b123) (not b1050) ) :assumption (or (not b117) (not b1022) ) :assumption (or (not b123) (not b1027) ) :assumption (or (not b117) (not b1000) ) :assumption (or (not b123) (not b1006) ) :assumption (or (not b117) (not b968) ) :assumption (or (not b123) (not b975) ) :assumption (or (not b129) (not b163) ) :assumption (or (not b129) (not b483) ) :assumption (or (not b129) (not b456) ) :assumption (or (not b129) (not b465) ) :assumption (or (not b129) (not b447) ) :assumption (or (not b129) (not b1086) ) :assumption (or (not b129) (not b1066) ) :assumption (or (not b129) (not b1044) ) :assumption (or (not b129) (not b1022) ) :assumption (or (not b129) (not b1000) ) :assumption (or (not b129) (not b968) ) :assumption (or (not b135) (not b167) ) :assumption (or (not b141) (not b172) ) :assumption (or (not b146) (not b176) ) :assumption (or (not b150) (not b179) ) :assumption (or (not b141) (not b489) ) :assumption (or (not b146) (not b492) ) :assumption (or (not b150) (not b495) ) :assumption (or (not b141) (not b462) ) :assumption (or (not b146) (not b465) ) :assumption (or (not b150) (not b468) ) :assumption (or (not b141) (not b453) ) :assumption (or (not b146) (not b456) ) :assumption (or (not b150) (not b459) ) :assumption (or (not b141) (not b444) ) :assumption (or (not b146) (not b447) ) :assumption (or (not b150) (not b450) ) :assumption (or (not b135) (not b1076) ) :assumption (or (not b141) (not b1081) ) :assumption (or (not b146) (not b1086) ) :assumption (or (not b150) (not b1091) ) :assumption (or (not b135) (not b1056) ) :assumption (or (not b141) (not b1061) ) :assumption (or (not b146) (not b1066) ) :assumption (or (not b150) (not b1071) ) :assumption (or (not b135) (not b1032) ) :assumption (or (not b141) (not b1038) ) :assumption (or (not b146) (not b1044) ) :assumption (or (not b150) (not b1050) ) :assumption (or (not b135) (not b1012) ) :assumption (or (not b141) (not b1017) ) :assumption (or (not b146) (not b1022) ) :assumption (or (not b150) (not b1027) ) :assumption (or (not b135) (not b988) ) :assumption (or (not b141) (not b994) ) :assumption (or (not b146) (not b1000) ) :assumption (or (not b150) (not b1006) ) :assumption (or (not b135) (not b954) ) :assumption (or (not b141) (not b961) ) :assumption (or (not b146) (not b968) ) :assumption (or (not b150) (not b975) ) :assumption (or (not b154) (not b474) ) :assumption (or (not b158) (not b477) ) :assumption (or (not b154) (not b447) ) :assumption (or (not b158) (not b450) ) :assumption (or (not b154) (not b492) ) :assumption (or (not b158) (not b495) ) :assumption (or (not b154) (not b483) ) :assumption (or (not b158) (not b486) ) :assumption (or (not b154) (not b1232) ) :assumption (or (not b154) (not b1215) ) :assumption (or (not b154) (not b1193) ) :assumption (or (not b158) (not b1199) ) :assumption (or (not b154) (not b1171) ) :assumption (or (not b158) (not b1176) ) :assumption (or (not b154) (not b1149) ) :assumption (or (not b158) (not b1155) ) :assumption (or (not b154) (not b1117) ) :assumption (or (not b158) (not b1124) ) :assumption (or (not b163) (not b483) ) :assumption (or (not b163) (not b456) ) :assumption (or (not b163) (not b492) ) :assumption (or (not b163) (not b474) ) :assumption (or (not b163) (not b1232) ) :assumption (or (not b163) (not b1215) ) :assumption (or (not b163) (not b1193) ) :assumption (or (not b163) (not b1171) ) :assumption (or (not b163) (not b1149) ) :assumption (or (not b163) (not b1117) ) :assumption (or (not b172) (not b489) ) :assumption (or (not b176) (not b492) ) :assumption (or (not b179) (not b495) ) :assumption (or (not b172) (not b462) ) :assumption (or (not b176) (not b465) ) :assumption (or (not b179) (not b468) ) :assumption (or (not b172) (not b480) ) :assumption (or (not b176) (not b483) ) :assumption (or (not b179) (not b486) ) :assumption (or (not b172) (not b471) ) :assumption (or (not b176) (not b474) ) :assumption (or (not b179) (not b477) ) :assumption (or (not b167) (not b1222) ) :assumption (or (not b172) (not b1227) ) :assumption (or (not b176) (not b1232) ) :assumption (or (not b167) (not b1205) ) :assumption (or (not b172) (not b1210) ) :assumption (or (not b176) (not b1215) ) :assumption (or (not b167) (not b1181) ) :assumption (or (not b172) (not b1187) ) :assumption (or (not b176) (not b1193) ) :assumption (or (not b179) (not b1199) ) :assumption (or (not b167) (not b1161) ) :assumption (or (not b172) (not b1166) ) :assumption (or (not b176) (not b1171) ) :assumption (or (not b179) (not b1176) ) :assumption (or (not b167) (not b1137) ) :assumption (or (not b172) (not b1143) ) :assumption (or (not b176) (not b1149) ) :assumption (or (not b179) (not b1155) ) :assumption (or (not b167) (not b1103) ) :assumption (or (not b172) (not b1110) ) :assumption (or (not b176) (not b1117) ) :assumption (or (not b179) (not b1124) ) :assumption (or (not b182) (not b217) ) :assumption (or (not b188) (not b221) ) :assumption (or (not b182) (not b528) ) :assumption (or (not b188) (not b531) ) :assumption (or (not b182) (not b501) ) :assumption (or (not b188) (not b504) ) :assumption (or (not b182) (not b519) ) :assumption (or (not b188) (not b522) ) :assumption (or (not b182) (not b510) ) :assumption (or (not b188) (not b513) ) :assumption (or (not b182) (not b1086) ) :assumption (or (not b188) (not b1091) ) :assumption (or (not b182) (not b1066) ) :assumption (or (not b188) (not b1071) ) :assumption (or (not b182) (not b1044) ) :assumption (or (not b188) (not b1050) ) :assumption (or (not b182) (not b1022) ) :assumption (or (not b188) (not b1027) ) :assumption (or (not b182) (not b1000) ) :assumption (or (not b188) (not b1006) ) :assumption (or (not b182) (not b968) ) :assumption (or (not b188) (not b975) ) :assumption (or (not b193) (not b225) ) :assumption (or (not b198) (not b228) ) :assumption (or (not b193) (not b537) ) :assumption (or (not b198) (not b540) ) :assumption (or (not b193) (not b510) ) :assumption (or (not b198) (not b513) ) :assumption (or (not b193) (not b519) ) :assumption (or (not b198) (not b522) ) :assumption (or (not b193) (not b501) ) :assumption (or (not b198) (not b504) ) :assumption (or (not b193) (not b1086) ) :assumption (or (not b198) (not b1091) ) :assumption (or (not b193) (not b1066) ) :assumption (or (not b198) (not b1071) ) :assumption (or (not b193) (not b1044) ) :assumption (or (not b198) (not b1050) ) :assumption (or (not b193) (not b1022) ) :assumption (or (not b198) (not b1027) ) :assumption (or (not b193) (not b1000) ) :assumption (or (not b198) (not b1006) ) :assumption (or (not b193) (not b968) ) :assumption (or (not b198) (not b975) ) :assumption (or (not b202) (not b231) ) :assumption (or (not b207) (not b235) ) :assumption (or (not b212) (not b239) ) :assumption (or (not b207) (not b543) ) :assumption (or (not b212) (not b546) ) :assumption (or (not b207) (not b516) ) :assumption (or (not b212) (not b519) ) :assumption (or (not b207) (not b507) ) :assumption (or (not b212) (not b510) ) :assumption (or (not b207) (not b498) ) :assumption (or (not b212) (not b501) ) :assumption (or (not b202) (not b1076) ) :assumption (or (not b207) (not b1081) ) :assumption (or (not b212) (not b1086) ) :assumption (or (not b202) (not b1056) ) :assumption (or (not b207) (not b1061) ) :assumption (or (not b212) (not b1066) ) :assumption (or (not b202) (not b1032) ) :assumption (or (not b207) (not b1038) ) :assumption (or (not b212) (not b1044) ) :assumption (or (not b202) (not b1012) ) :assumption (or (not b207) (not b1017) ) :assumption (or (not b212) (not b1022) ) :assumption (or (not b202) (not b988) ) :assumption (or (not b207) (not b994) ) :assumption (or (not b212) (not b1000) ) :assumption (or (not b202) (not b954) ) :assumption (or (not b207) (not b961) ) :assumption (or (not b212) (not b968) ) :assumption (or (not b217) (not b528) ) :assumption (or (not b221) (not b531) ) :assumption (or (not b217) (not b501) ) :assumption (or (not b221) (not b504) ) :assumption (or (not b217) (not b546) ) :assumption (or (not b221) (not b549) ) :assumption (or (not b217) (not b537) ) :assumption (or (not b221) (not b540) ) :assumption (or (not b217) (not b1232) ) :assumption (or (not b217) (not b1215) ) :assumption (or (not b217) (not b1193) ) :assumption (or (not b221) (not b1199) ) :assumption (or (not b217) (not b1171) ) :assumption (or (not b221) (not b1176) ) :assumption (or (not b217) (not b1149) ) :assumption (or (not b221) (not b1155) ) :assumption (or (not b217) (not b1117) ) :assumption (or (not b221) (not b1124) ) :assumption (or (not b225) (not b537) ) :assumption (or (not b228) (not b540) ) :assumption (or (not b225) (not b510) ) :assumption (or (not b228) (not b513) ) :assumption (or (not b225) (not b546) ) :assumption (or (not b228) (not b549) ) :assumption (or (not b225) (not b528) ) :assumption (or (not b228) (not b531) ) :assumption (or (not b225) (not b1232) ) :assumption (or (not b225) (not b1215) ) :assumption (or (not b225) (not b1193) ) :assumption (or (not b228) (not b1199) ) :assumption (or (not b225) (not b1171) ) :assumption (or (not b228) (not b1176) ) :assumption (or (not b225) (not b1149) ) :assumption (or (not b228) (not b1155) ) :assumption (or (not b225) (not b1117) ) :assumption (or (not b228) (not b1124) ) :assumption (or (not b235) (not b543) ) :assumption (or (not b239) (not b546) ) :assumption (or (not b235) (not b516) ) :assumption (or (not b239) (not b519) ) :assumption (or (not b235) (not b534) ) :assumption (or (not b239) (not b537) ) :assumption (or (not b235) (not b525) ) :assumption (or (not b239) (not b528) ) :assumption (or (not b231) (not b1222) ) :assumption (or (not b235) (not b1227) ) :assumption (or (not b239) (not b1232) ) :assumption (or (not b231) (not b1205) ) :assumption (or (not b235) (not b1210) ) :assumption (or (not b239) (not b1215) ) :assumption (or (not b231) (not b1181) ) :assumption (or (not b235) (not b1187) ) :assumption (or (not b239) (not b1193) ) :assumption (or (not b231) (not b1161) ) :assumption (or (not b235) (not b1166) ) :assumption (or (not b239) (not b1171) ) :assumption (or (not b231) (not b1137) ) :assumption (or (not b235) (not b1143) ) :assumption (or (not b239) (not b1149) ) :assumption (or (not b231) (not b1103) ) :assumption (or (not b235) (not b1110) ) :assumption (or (not b239) (not b1117) ) :assumption (or (not b243) (not b279) ) :assumption (or (not b243) (not b582) ) :assumption (or (not b243) (not b555) ) :assumption (or (not b243) (not b573) ) :assumption (or (not b243) (not b564) ) :assumption (or (not b243) (not b1086) ) :assumption (or (not b243) (not b1066) ) :assumption (or (not b243) (not b1044) ) :assumption (or (not b243) (not b1022) ) :assumption (or (not b243) (not b1000) ) :assumption (or (not b243) (not b968) ) :assumption (or (not b251) (not b285) ) :assumption (or (not b257) (not b290) ) :assumption (or (not b262) (not b294) ) :assumption (or (not b266) (not b297) ) :assumption (or (not b257) (not b588) ) :assumption (or (not b262) (not b591) ) :assumption (or (not b266) (not b594) ) :assumption (or (not b257) (not b561) ) :assumption (or (not b262) (not b564) ) :assumption (or (not b266) (not b567) ) :assumption (or (not b257) (not b570) ) :assumption (or (not b262) (not b573) ) :assumption (or (not b266) (not b576) ) :assumption (or (not b257) (not b552) ) :assumption (or (not b262) (not b555) ) :assumption (or (not b266) (not b558) ) :assumption (or (not b251) (not b1076) ) :assumption (or (not b257) (not b1081) ) :assumption (or (not b262) (not b1086) ) :assumption (or (not b266) (not b1091) ) :assumption (or (not b251) (not b1056) ) :assumption (or (not b257) (not b1061) ) :assumption (or (not b262) (not b1066) ) :assumption (or (not b266) (not b1071) ) :assumption (or (not b251) (not b1032) ) :assumption (or (not b257) (not b1038) ) :assumption (or (not b262) (not b1044) ) :assumption (or (not b266) (not b1050) ) :assumption (or (not b251) (not b1012) ) :assumption (or (not b257) (not b1017) ) :assumption (or (not b262) (not b1022) ) :assumption (or (not b266) (not b1027) ) :assumption (or (not b251) (not b988) ) :assumption (or (not b257) (not b994) ) :assumption (or (not b262) (not b1000) ) :assumption (or (not b266) (not b1006) ) :assumption (or (not b251) (not b954) ) :assumption (or (not b257) (not b961) ) :assumption (or (not b262) (not b968) ) :assumption (or (not b266) (not b975) ) :assumption (or (not b270) (not b300) ) :assumption (or (not b275) (not b303) ) :assumption (or (not b270) (not b600) ) :assumption (or (not b275) (not b603) ) :assumption (or (not b270) (not b573) ) :assumption (or (not b275) (not b576) ) :assumption (or (not b270) (not b564) ) :assumption (or (not b275) (not b567) ) :assumption (or (not b270) (not b555) ) :assumption (or (not b275) (not b558) ) :assumption (or (not b270) (not b1086) ) :assumption (or (not b275) (not b1091) ) :assumption (or (not b270) (not b1066) ) :assumption (or (not b275) (not b1071) ) :assumption (or (not b270) (not b1044) ) :assumption (or (not b275) (not b1050) ) :assumption (or (not b270) (not b1022) ) :assumption (or (not b275) (not b1027) ) :assumption (or (not b270) (not b1000) ) :assumption (or (not b275) (not b1006) ) :assumption (or (not b270) (not b968) ) :assumption (or (not b275) (not b975) ) :assumption (or (not b279) (not b582) ) :assumption (or (not b279) (not b555) ) :assumption (or (not b279) (not b600) ) :assumption (or (not b279) (not b591) ) :assumption (or (not b279) (not b1232) ) :assumption (or (not b279) (not b1215) ) :assumption (or (not b279) (not b1193) ) :assumption (or (not b279) (not b1171) ) :assumption (or (not b279) (not b1149) ) :assumption (or (not b279) (not b1117) ) :assumption (or (not b290) (not b588) ) :assumption (or (not b294) (not b591) ) :assumption (or (not b297) (not b594) ) :assumption (or (not b290) (not b561) ) :assumption (or (not b294) (not b564) ) :assumption (or (not b297) (not b567) ) :assumption (or (not b290) (not b597) ) :assumption (or (not b294) (not b600) ) :assumption (or (not b297) (not b603) ) :assumption (or (not b290) (not b579) ) :assumption (or (not b294) (not b582) ) :assumption (or (not b297) (not b585) ) :assumption (or (not b285) (not b1222) ) :assumption (or (not b290) (not b1227) ) :assumption (or (not b294) (not b1232) ) :assumption (or (not b285) (not b1205) ) :assumption (or (not b290) (not b1210) ) :assumption (or (not b294) (not b1215) ) :assumption (or (not b285) (not b1181) ) :assumption (or (not b290) (not b1187) ) :assumption (or (not b294) (not b1193) ) :assumption (or (not b297) (not b1199) ) :assumption (or (not b285) (not b1161) ) :assumption (or (not b290) (not b1166) ) :assumption (or (not b294) (not b1171) ) :assumption (or (not b297) (not b1176) ) :assumption (or (not b285) (not b1137) ) :assumption (or (not b290) (not b1143) ) :assumption (or (not b294) (not b1149) ) :assumption (or (not b297) (not b1155) ) :assumption (or (not b285) (not b1103) ) :assumption (or (not b290) (not b1110) ) :assumption (or (not b294) (not b1117) ) :assumption (or (not b297) (not b1124) ) :assumption (or (not b300) (not b600) ) :assumption (or (not b303) (not b603) ) :assumption (or (not b300) (not b573) ) :assumption (or (not b303) (not b576) ) :assumption (or (not b300) (not b591) ) :assumption (or (not b303) (not b594) ) :assumption (or (not b300) (not b582) ) :assumption (or (not b303) (not b585) ) :assumption (or (not b300) (not b1232) ) :assumption (or (not b300) (not b1215) ) :assumption (or (not b300) (not b1193) ) :assumption (or (not b303) (not b1199) ) :assumption (or (not b300) (not b1171) ) :assumption (or (not b303) (not b1176) ) :assumption (or (not b300) (not b1149) ) :assumption (or (not b303) (not b1155) ) :assumption (or (not b300) (not b1117) ) :assumption (or (not b303) (not b1124) ) :assumption (or (not b306) (not b344) ) :assumption (or (not b312) (not b348) ) :assumption (or (not b306) (not b636) ) :assumption (or (not b312) (not b639) ) :assumption (or (not b306) (not b609) ) :assumption (or (not b312) (not b612) ) :assumption (or (not b306) (not b627) ) :assumption (or (not b312) (not b630) ) :assumption (or (not b306) (not b618) ) :assumption (or (not b312) (not b621) ) :assumption (or (not b306) (not b1086) ) :assumption (or (not b312) (not b1091) ) :assumption (or (not b306) (not b1066) ) :assumption (or (not b312) (not b1071) ) :assumption (or (not b306) (not b1044) ) :assumption (or (not b312) (not b1050) ) :assumption (or (not b306) (not b1022) ) :assumption (or (not b312) (not b1027) ) :assumption (or (not b306) (not b1000) ) :assumption (or (not b312) (not b1006) ) :assumption (or (not b306) (not b968) ) :assumption (or (not b312) (not b975) ) :assumption (or (not b317) (not b352) ) :assumption (or (not b322) (not b355) ) :assumption (or (not b317) (not b645) ) :assumption (or (not b322) (not b648) ) :assumption (or (not b317) (not b618) ) :assumption (or (not b322) (not b621) ) :assumption (or (not b317) (not b627) ) :assumption (or (not b322) (not b630) ) :assumption (or (not b317) (not b609) ) :assumption (or (not b322) (not b612) ) :assumption (or (not b317) (not b1086) ) :assumption (or (not b322) (not b1091) ) :assumption (or (not b317) (not b1066) ) :assumption (or (not b322) (not b1071) ) :assumption (or (not b317) (not b1044) ) :assumption (or (not b322) (not b1050) ) :assumption (or (not b317) (not b1022) ) :assumption (or (not b322) (not b1027) ) :assumption (or (not b317) (not b1000) ) :assumption (or (not b322) (not b1006) ) :assumption (or (not b317) (not b968) ) :assumption (or (not b322) (not b975) ) :assumption (or (not b326) (not b358) ) :assumption (or (not b331) (not b362) ) :assumption (or (not b336) (not b366) ) :assumption (or (not b340) (not b369) ) :assumption (or (not b331) (not b651) ) :assumption (or (not b336) (not b654) ) :assumption (or (not b340) (not b657) ) :assumption (or (not b331) (not b624) ) :assumption (or (not b336) (not b627) ) :assumption (or (not b340) (not b630) ) :assumption (or (not b331) (not b615) ) :assumption (or (not b336) (not b618) ) :assumption (or (not b340) (not b621) ) :assumption (or (not b331) (not b606) ) :assumption (or (not b336) (not b609) ) :assumption (or (not b340) (not b612) ) :assumption (or (not b326) (not b1076) ) :assumption (or (not b331) (not b1081) ) :assumption (or (not b336) (not b1086) ) :assumption (or (not b340) (not b1091) ) :assumption (or (not b326) (not b1056) ) :assumption (or (not b331) (not b1061) ) :assumption (or (not b336) (not b1066) ) :assumption (or (not b340) (not b1071) ) :assumption (or (not b326) (not b1032) ) :assumption (or (not b331) (not b1038) ) :assumption (or (not b336) (not b1044) ) :assumption (or (not b340) (not b1050) ) :assumption (or (not b326) (not b1012) ) :assumption (or (not b331) (not b1017) ) :assumption (or (not b336) (not b1022) ) :assumption (or (not b340) (not b1027) ) :assumption (or (not b326) (not b988) ) :assumption (or (not b331) (not b994) ) :assumption (or (not b336) (not b1000) ) :assumption (or (not b340) (not b1006) ) :assumption (or (not b326) (not b954) ) :assumption (or (not b331) (not b961) ) :assumption (or (not b336) (not b968) ) :assumption (or (not b340) (not b975) ) :assumption (or (not b344) (not b636) ) :assumption (or (not b348) (not b639) ) :assumption (or (not b344) (not b609) ) :assumption (or (not b348) (not b612) ) :assumption (or (not b344) (not b654) ) :assumption (or (not b348) (not b657) ) :assumption (or (not b344) (not b645) ) :assumption (or (not b348) (not b648) ) :assumption (or (not b344) (not b1232) ) :assumption (or (not b344) (not b1215) ) :assumption (or (not b344) (not b1193) ) :assumption (or (not b348) (not b1199) ) :assumption (or (not b344) (not b1171) ) :assumption (or (not b348) (not b1176) ) :assumption (or (not b344) (not b1149) ) :assumption (or (not b348) (not b1155) ) :assumption (or (not b344) (not b1117) ) :assumption (or (not b348) (not b1124) ) :assumption (or (not b352) (not b645) ) :assumption (or (not b355) (not b648) ) :assumption (or (not b352) (not b618) ) :assumption (or (not b355) (not b621) ) :assumption (or (not b352) (not b654) ) :assumption (or (not b355) (not b657) ) :assumption (or (not b352) (not b636) ) :assumption (or (not b355) (not b639) ) :assumption (or (not b352) (not b1232) ) :assumption (or (not b352) (not b1215) ) :assumption (or (not b352) (not b1193) ) :assumption (or (not b355) (not b1199) ) :assumption (or (not b352) (not b1171) ) :assumption (or (not b355) (not b1176) ) :assumption (or (not b352) (not b1149) ) :assumption (or (not b355) (not b1155) ) :assumption (or (not b352) (not b1117) ) :assumption (or (not b355) (not b1124) ) :assumption (or (not b362) (not b651) ) :assumption (or (not b366) (not b654) ) :assumption (or (not b369) (not b657) ) :assumption (or (not b362) (not b624) ) :assumption (or (not b366) (not b627) ) :assumption (or (not b369) (not b630) ) :assumption (or (not b362) (not b642) ) :assumption (or (not b366) (not b645) ) :assumption (or (not b369) (not b648) ) :assumption (or (not b362) (not b633) ) :assumption (or (not b366) (not b636) ) :assumption (or (not b369) (not b639) ) :assumption (or (not b358) (not b1222) ) :assumption (or (not b362) (not b1227) ) :assumption (or (not b366) (not b1232) ) :assumption (or (not b358) (not b1205) ) :assumption (or (not b362) (not b1210) ) :assumption (or (not b366) (not b1215) ) :assumption (or (not b358) (not b1181) ) :assumption (or (not b362) (not b1187) ) :assumption (or (not b366) (not b1193) ) :assumption (or (not b369) (not b1199) ) :assumption (or (not b358) (not b1161) ) :assumption (or (not b362) (not b1166) ) :assumption (or (not b366) (not b1171) ) :assumption (or (not b369) (not b1176) ) :assumption (or (not b358) (not b1137) ) :assumption (or (not b362) (not b1143) ) :assumption (or (not b366) (not b1149) ) :assumption (or (not b369) (not b1155) ) :assumption (or (not b358) (not b1103) ) :assumption (or (not b362) (not b1110) ) :assumption (or (not b366) (not b1117) ) :assumption (or (not b369) (not b1124) ) :assumption (or (not b372) (not b396) ) :assumption (or (not b375) (not b399) ) :assumption (or (not b378) (not b402) ) :assumption (or (not b381) (not b405) ) :assumption (or (not b372) (not b384) ) :assumption (or (not b375) (not b387) ) :assumption (or (not b378) (not b390) ) :assumption (or (not b381) (not b393) ) :assumption (or (not b372) (not b1076) ) :assumption (or (not b375) (not b1081) ) :assumption (or (not b378) (not b1086) ) :assumption (or (not b381) (not b1091) ) :assumption (or (not b372) (not b1056) ) :assumption (or (not b375) (not b1061) ) :assumption (or (not b378) (not b1066) ) :assumption (or (not b381) (not b1071) ) :assumption (or (not b372) (not b1032) ) :assumption (or (not b375) (not b1038) ) :assumption (or (not b378) (not b1044) ) :assumption (or (not b381) (not b1050) ) :assumption (or (not b372) (not b1012) ) :assumption (or (not b375) (not b1017) ) :assumption (or (not b378) (not b1022) ) :assumption (or (not b381) (not b1027) ) :assumption (or (not b372) (not b988) ) :assumption (or (not b375) (not b994) ) :assumption (or (not b378) (not b1000) ) :assumption (or (not b381) (not b1006) ) :assumption (or (not b372) (not b954) ) :assumption (or (not b375) (not b961) ) :assumption (or (not b378) (not b968) ) :assumption (or (not b381) (not b975) ) :assumption (or (not b384) (not b396) ) :assumption (or (not b387) (not b399) ) :assumption (or (not b390) (not b402) ) :assumption (or (not b393) (not b405) ) :assumption (or (not b384) (not b1076) ) :assumption (or (not b387) (not b1081) ) :assumption (or (not b390) (not b1086) ) :assumption (or (not b393) (not b1091) ) :assumption (or (not b384) (not b1056) ) :assumption (or (not b387) (not b1061) ) :assumption (or (not b390) (not b1066) ) :assumption (or (not b393) (not b1071) ) :assumption (or (not b384) (not b1032) ) :assumption (or (not b387) (not b1038) ) :assumption (or (not b390) (not b1044) ) :assumption (or (not b393) (not b1050) ) :assumption (or (not b384) (not b1012) ) :assumption (or (not b387) (not b1017) ) :assumption (or (not b390) (not b1022) ) :assumption (or (not b393) (not b1027) ) :assumption (or (not b384) (not b988) ) :assumption (or (not b387) (not b994) ) :assumption (or (not b390) (not b1000) ) :assumption (or (not b393) (not b1006) ) :assumption (or (not b384) (not b954) ) :assumption (or (not b387) (not b961) ) :assumption (or (not b390) (not b968) ) :assumption (or (not b393) (not b975) ) :assumption (or (not b396) (not b1076) ) :assumption (or (not b399) (not b1081) ) :assumption (or (not b402) (not b1086) ) :assumption (or (not b405) (not b1091) ) :assumption (or (not b396) (not b1056) ) :assumption (or (not b399) (not b1061) ) :assumption (or (not b402) (not b1066) ) :assumption (or (not b405) (not b1071) ) :assumption (or (not b396) (not b1032) ) :assumption (or (not b399) (not b1038) ) :assumption (or (not b402) (not b1044) ) :assumption (or (not b405) (not b1050) ) :assumption (or (not b396) (not b1012) ) :assumption (or (not b399) (not b1017) ) :assumption (or (not b402) (not b1022) ) :assumption (or (not b405) (not b1027) ) :assumption (or (not b396) (not b988) ) :assumption (or (not b399) (not b994) ) :assumption (or (not b402) (not b1000) ) :assumption (or (not b405) (not b1006) ) :assumption (or (not b396) (not b954) ) :assumption (or (not b399) (not b961) ) :assumption (or (not b402) (not b968) ) :assumption (or (not b405) (not b975) ) :assumption (or (not b408) (not b432) ) :assumption (or (not b411) (not b435) ) :assumption (or (not b414) (not b438) ) :assumption (or (not b417) (not b441) ) :assumption (or (not b408) (not b420) ) :assumption (or (not b411) (not b423) ) :assumption (or (not b414) (not b426) ) :assumption (or (not b417) (not b429) ) :assumption (or (not b408) (not b1222) ) :assumption (or (not b411) (not b1227) ) :assumption (or (not b414) (not b1232) ) :assumption (or (not b408) (not b1205) ) :assumption (or (not b411) (not b1210) ) :assumption (or (not b414) (not b1215) ) :assumption (or (not b408) (not b1181) ) :assumption (or (not b411) (not b1187) ) :assumption (or (not b414) (not b1193) ) :assumption (or (not b417) (not b1199) ) :assumption (or (not b408) (not b1161) ) :assumption (or (not b411) (not b1166) ) :assumption (or (not b414) (not b1171) ) :assumption (or (not b417) (not b1176) ) :assumption (or (not b408) (not b1137) ) :assumption (or (not b411) (not b1143) ) :assumption (or (not b414) (not b1149) ) :assumption (or (not b417) (not b1155) ) :assumption (or (not b408) (not b1103) ) :assumption (or (not b411) (not b1110) ) :assumption (or (not b414) (not b1117) ) :assumption (or (not b417) (not b1124) ) :assumption (or (not b420) (not b432) ) :assumption (or (not b423) (not b435) ) :assumption (or (not b426) (not b438) ) :assumption (or (not b429) (not b441) ) :assumption (or (not b420) (not b1222) ) :assumption (or (not b423) (not b1227) ) :assumption (or (not b426) (not b1232) ) :assumption (or (not b420) (not b1205) ) :assumption (or (not b423) (not b1210) ) :assumption (or (not b426) (not b1215) ) :assumption (or (not b420) (not b1181) ) :assumption (or (not b423) (not b1187) ) :assumption (or (not b426) (not b1193) ) :assumption (or (not b429) (not b1199) ) :assumption (or (not b420) (not b1161) ) :assumption (or (not b423) (not b1166) ) :assumption (or (not b426) (not b1171) ) :assumption (or (not b429) (not b1176) ) :assumption (or (not b420) (not b1137) ) :assumption (or (not b423) (not b1143) ) :assumption (or (not b426) (not b1149) ) :assumption (or (not b429) (not b1155) ) :assumption (or (not b420) (not b1103) ) :assumption (or (not b423) (not b1110) ) :assumption (or (not b426) (not b1117) ) :assumption (or (not b429) (not b1124) ) :assumption (or (not b432) (not b1222) ) :assumption (or (not b435) (not b1227) ) :assumption (or (not b438) (not b1232) ) :assumption (or (not b432) (not b1205) ) :assumption (or (not b435) (not b1210) ) :assumption (or (not b438) (not b1215) ) :assumption (or (not b432) (not b1181) ) :assumption (or (not b435) (not b1187) ) :assumption (or (not b438) (not b1193) ) :assumption (or (not b441) (not b1199) ) :assumption (or (not b432) (not b1161) ) :assumption (or (not b435) (not b1166) ) :assumption (or (not b438) (not b1171) ) :assumption (or (not b441) (not b1176) ) :assumption (or (not b432) (not b1137) ) :assumption (or (not b435) (not b1143) ) :assumption (or (not b438) (not b1149) ) :assumption (or (not b441) (not b1155) ) :assumption (or (not b432) (not b1103) ) :assumption (or (not b435) (not b1110) ) :assumption (or (not b438) (not b1117) ) :assumption (or (not b441) (not b1124) ) :assumption (or (not b444) (not b462) ) :assumption (or (not b447) (not b465) ) :assumption (or (not b450) (not b468) ) :assumption (or (not b444) (not b453) ) :assumption (or (not b447) (not b456) ) :assumption (or (not b450) (not b459) ) :assumption (or (not b444) (not b1081) ) :assumption (or (not b447) (not b1086) ) :assumption (or (not b450) (not b1091) ) :assumption (or (not b444) (not b1061) ) :assumption (or (not b447) (not b1066) ) :assumption (or (not b450) (not b1071) ) :assumption (or (not b444) (not b1038) ) :assumption (or (not b447) (not b1044) ) :assumption (or (not b450) (not b1050) ) :assumption (or (not b444) (not b1017) ) :assumption (or (not b447) (not b1022) ) :assumption (or (not b450) (not b1027) ) :assumption (or (not b444) (not b994) ) :assumption (or (not b447) (not b1000) ) :assumption (or (not b450) (not b1006) ) :assumption (or (not b444) (not b961) ) :assumption (or (not b447) (not b968) ) :assumption (or (not b450) (not b975) ) :assumption (or (not b453) (not b462) ) :assumption (or (not b456) (not b465) ) :assumption (or (not b459) (not b468) ) :assumption (or (not b453) (not b1081) ) :assumption (or (not b456) (not b1086) ) :assumption (or (not b459) (not b1091) ) :assumption (or (not b453) (not b1061) ) :assumption (or (not b456) (not b1066) ) :assumption (or (not b459) (not b1071) ) :assumption (or (not b453) (not b1038) ) :assumption (or (not b456) (not b1044) ) :assumption (or (not b459) (not b1050) ) :assumption (or (not b453) (not b1017) ) :assumption (or (not b456) (not b1022) ) :assumption (or (not b459) (not b1027) ) :assumption (or (not b453) (not b994) ) :assumption (or (not b456) (not b1000) ) :assumption (or (not b459) (not b1006) ) :assumption (or (not b453) (not b961) ) :assumption (or (not b456) (not b968) ) :assumption (or (not b459) (not b975) ) :assumption (or (not b462) (not b1081) ) :assumption (or (not b465) (not b1086) ) :assumption (or (not b468) (not b1091) ) :assumption (or (not b462) (not b1061) ) :assumption (or (not b465) (not b1066) ) :assumption (or (not b468) (not b1071) ) :assumption (or (not b462) (not b1038) ) :assumption (or (not b465) (not b1044) ) :assumption (or (not b468) (not b1050) ) :assumption (or (not b462) (not b1017) ) :assumption (or (not b465) (not b1022) ) :assumption (or (not b468) (not b1027) ) :assumption (or (not b462) (not b994) ) :assumption (or (not b465) (not b1000) ) :assumption (or (not b468) (not b1006) ) :assumption (or (not b462) (not b961) ) :assumption (or (not b465) (not b968) ) :assumption (or (not b468) (not b975) ) :assumption (or (not b471) (not b489) ) :assumption (or (not b474) (not b492) ) :assumption (or (not b477) (not b495) ) :assumption (or (not b471) (not b480) ) :assumption (or (not b474) (not b483) ) :assumption (or (not b477) (not b486) ) :assumption (or (not b471) (not b1227) ) :assumption (or (not b474) (not b1232) ) :assumption (or (not b471) (not b1210) ) :assumption (or (not b474) (not b1215) ) :assumption (or (not b471) (not b1187) ) :assumption (or (not b474) (not b1193) ) :assumption (or (not b477) (not b1199) ) :assumption (or (not b471) (not b1166) ) :assumption (or (not b474) (not b1171) ) :assumption (or (not b477) (not b1176) ) :assumption (or (not b471) (not b1143) ) :assumption (or (not b474) (not b1149) ) :assumption (or (not b477) (not b1155) ) :assumption (or (not b471) (not b1110) ) :assumption (or (not b474) (not b1117) ) :assumption (or (not b477) (not b1124) ) :assumption (or (not b480) (not b489) ) :assumption (or (not b483) (not b492) ) :assumption (or (not b486) (not b495) ) :assumption (or (not b480) (not b1227) ) :assumption (or (not b483) (not b1232) ) :assumption (or (not b480) (not b1210) ) :assumption (or (not b483) (not b1215) ) :assumption (or (not b480) (not b1187) ) :assumption (or (not b483) (not b1193) ) :assumption (or (not b486) (not b1199) ) :assumption (or (not b480) (not b1166) ) :assumption (or (not b483) (not b1171) ) :assumption (or (not b486) (not b1176) ) :assumption (or (not b480) (not b1143) ) :assumption (or (not b483) (not b1149) ) :assumption (or (not b486) (not b1155) ) :assumption (or (not b480) (not b1110) ) :assumption (or (not b483) (not b1117) ) :assumption (or (not b486) (not b1124) ) :assumption (or (not b489) (not b1227) ) :assumption (or (not b492) (not b1232) ) :assumption (or (not b489) (not b1210) ) :assumption (or (not b492) (not b1215) ) :assumption (or (not b489) (not b1187) ) :assumption (or (not b492) (not b1193) ) :assumption (or (not b495) (not b1199) ) :assumption (or (not b489) (not b1166) ) :assumption (or (not b492) (not b1171) ) :assumption (or (not b495) (not b1176) ) :assumption (or (not b489) (not b1143) ) :assumption (or (not b492) (not b1149) ) :assumption (or (not b495) (not b1155) ) :assumption (or (not b489) (not b1110) ) :assumption (or (not b492) (not b1117) ) :assumption (or (not b495) (not b1124) ) :assumption (or (not b498) (not b516) ) :assumption (or (not b501) (not b519) ) :assumption (or (not b504) (not b522) ) :assumption (or (not b498) (not b507) ) :assumption (or (not b501) (not b510) ) :assumption (or (not b504) (not b513) ) :assumption (or (not b498) (not b1081) ) :assumption (or (not b501) (not b1086) ) :assumption (or (not b504) (not b1091) ) :assumption (or (not b498) (not b1061) ) :assumption (or (not b501) (not b1066) ) :assumption (or (not b504) (not b1071) ) :assumption (or (not b498) (not b1038) ) :assumption (or (not b501) (not b1044) ) :assumption (or (not b504) (not b1050) ) :assumption (or (not b498) (not b1017) ) :assumption (or (not b501) (not b1022) ) :assumption (or (not b504) (not b1027) ) :assumption (or (not b498) (not b994) ) :assumption (or (not b501) (not b1000) ) :assumption (or (not b504) (not b1006) ) :assumption (or (not b498) (not b961) ) :assumption (or (not b501) (not b968) ) :assumption (or (not b504) (not b975) ) :assumption (or (not b507) (not b516) ) :assumption (or (not b510) (not b519) ) :assumption (or (not b513) (not b522) ) :assumption (or (not b507) (not b1081) ) :assumption (or (not b510) (not b1086) ) :assumption (or (not b513) (not b1091) ) :assumption (or (not b507) (not b1061) ) :assumption (or (not b510) (not b1066) ) :assumption (or (not b513) (not b1071) ) :assumption (or (not b507) (not b1038) ) :assumption (or (not b510) (not b1044) ) :assumption (or (not b513) (not b1050) ) :assumption (or (not b507) (not b1017) ) :assumption (or (not b510) (not b1022) ) :assumption (or (not b513) (not b1027) ) :assumption (or (not b507) (not b994) ) :assumption (or (not b510) (not b1000) ) :assumption (or (not b513) (not b1006) ) :assumption (or (not b507) (not b961) ) :assumption (or (not b510) (not b968) ) :assumption (or (not b513) (not b975) ) :assumption (or (not b516) (not b1081) ) :assumption (or (not b519) (not b1086) ) :assumption (or (not b522) (not b1091) ) :assumption (or (not b516) (not b1061) ) :assumption (or (not b519) (not b1066) ) :assumption (or (not b522) (not b1071) ) :assumption (or (not b516) (not b1038) ) :assumption (or (not b519) (not b1044) ) :assumption (or (not b522) (not b1050) ) :assumption (or (not b516) (not b1017) ) :assumption (or (not b519) (not b1022) ) :assumption (or (not b522) (not b1027) ) :assumption (or (not b516) (not b994) ) :assumption (or (not b519) (not b1000) ) :assumption (or (not b522) (not b1006) ) :assumption (or (not b516) (not b961) ) :assumption (or (not b519) (not b968) ) :assumption (or (not b522) (not b975) ) :assumption (or (not b525) (not b543) ) :assumption (or (not b528) (not b546) ) :assumption (or (not b531) (not b549) ) :assumption (or (not b525) (not b534) ) :assumption (or (not b528) (not b537) ) :assumption (or (not b531) (not b540) ) :assumption (or (not b525) (not b1227) ) :assumption (or (not b528) (not b1232) ) :assumption (or (not b525) (not b1210) ) :assumption (or (not b528) (not b1215) ) :assumption (or (not b525) (not b1187) ) :assumption (or (not b528) (not b1193) ) :assumption (or (not b531) (not b1199) ) :assumption (or (not b525) (not b1166) ) :assumption (or (not b528) (not b1171) ) :assumption (or (not b531) (not b1176) ) :assumption (or (not b525) (not b1143) ) :assumption (or (not b528) (not b1149) ) :assumption (or (not b531) (not b1155) ) :assumption (or (not b525) (not b1110) ) :assumption (or (not b528) (not b1117) ) :assumption (or (not b531) (not b1124) ) :assumption (or (not b534) (not b543) ) :assumption (or (not b537) (not b546) ) :assumption (or (not b540) (not b549) ) :assumption (or (not b534) (not b1227) ) :assumption (or (not b537) (not b1232) ) :assumption (or (not b534) (not b1210) ) :assumption (or (not b537) (not b1215) ) :assumption (or (not b534) (not b1187) ) :assumption (or (not b537) (not b1193) ) :assumption (or (not b540) (not b1199) ) :assumption (or (not b534) (not b1166) ) :assumption (or (not b537) (not b1171) ) :assumption (or (not b540) (not b1176) ) :assumption (or (not b534) (not b1143) ) :assumption (or (not b537) (not b1149) ) :assumption (or (not b540) (not b1155) ) :assumption (or (not b534) (not b1110) ) :assumption (or (not b537) (not b1117) ) :assumption (or (not b540) (not b1124) ) :assumption (or (not b543) (not b1227) ) :assumption (or (not b546) (not b1232) ) :assumption (or (not b543) (not b1210) ) :assumption (or (not b546) (not b1215) ) :assumption (or (not b543) (not b1187) ) :assumption (or (not b546) (not b1193) ) :assumption (or (not b549) (not b1199) ) :assumption (or (not b543) (not b1166) ) :assumption (or (not b546) (not b1171) ) :assumption (or (not b549) (not b1176) ) :assumption (or (not b543) (not b1143) ) :assumption (or (not b546) (not b1149) ) :assumption (or (not b549) (not b1155) ) :assumption (or (not b543) (not b1110) ) :assumption (or (not b546) (not b1117) ) :assumption (or (not b549) (not b1124) ) :assumption (or (not b552) (not b570) ) :assumption (or (not b555) (not b573) ) :assumption (or (not b558) (not b576) ) :assumption (or (not b552) (not b561) ) :assumption (or (not b555) (not b564) ) :assumption (or (not b558) (not b567) ) :assumption (or (not b552) (not b1081) ) :assumption (or (not b555) (not b1086) ) :assumption (or (not b558) (not b1091) ) :assumption (or (not b552) (not b1061) ) :assumption (or (not b555) (not b1066) ) :assumption (or (not b558) (not b1071) ) :assumption (or (not b552) (not b1038) ) :assumption (or (not b555) (not b1044) ) :assumption (or (not b558) (not b1050) ) :assumption (or (not b552) (not b1017) ) :assumption (or (not b555) (not b1022) ) :assumption (or (not b558) (not b1027) ) :assumption (or (not b552) (not b994) ) :assumption (or (not b555) (not b1000) ) :assumption (or (not b558) (not b1006) ) :assumption (or (not b552) (not b961) ) :assumption (or (not b555) (not b968) ) :assumption (or (not b558) (not b975) ) :assumption (or (not b561) (not b570) ) :assumption (or (not b564) (not b573) ) :assumption (or (not b567) (not b576) ) :assumption (or (not b561) (not b1081) ) :assumption (or (not b564) (not b1086) ) :assumption (or (not b567) (not b1091) ) :assumption (or (not b561) (not b1061) ) :assumption (or (not b564) (not b1066) ) :assumption (or (not b567) (not b1071) ) :assumption (or (not b561) (not b1038) ) :assumption (or (not b564) (not b1044) ) :assumption (or (not b567) (not b1050) ) :assumption (or (not b561) (not b1017) ) :assumption (or (not b564) (not b1022) ) :assumption (or (not b567) (not b1027) ) :assumption (or (not b561) (not b994) ) :assumption (or (not b564) (not b1000) ) :assumption (or (not b567) (not b1006) ) :assumption (or (not b561) (not b961) ) :assumption (or (not b564) (not b968) ) :assumption (or (not b567) (not b975) ) :assumption (or (not b570) (not b1081) ) :assumption (or (not b573) (not b1086) ) :assumption (or (not b576) (not b1091) ) :assumption (or (not b570) (not b1061) ) :assumption (or (not b573) (not b1066) ) :assumption (or (not b576) (not b1071) ) :assumption (or (not b570) (not b1038) ) :assumption (or (not b573) (not b1044) ) :assumption (or (not b576) (not b1050) ) :assumption (or (not b570) (not b1017) ) :assumption (or (not b573) (not b1022) ) :assumption (or (not b576) (not b1027) ) :assumption (or (not b570) (not b994) ) :assumption (or (not b573) (not b1000) ) :assumption (or (not b576) (not b1006) ) :assumption (or (not b570) (not b961) ) :assumption (or (not b573) (not b968) ) :assumption (or (not b576) (not b975) ) :assumption (or (not b579) (not b597) ) :assumption (or (not b582) (not b600) ) :assumption (or (not b585) (not b603) ) :assumption (or (not b579) (not b588) ) :assumption (or (not b582) (not b591) ) :assumption (or (not b585) (not b594) ) :assumption (or (not b579) (not b1227) ) :assumption (or (not b582) (not b1232) ) :assumption (or (not b579) (not b1210) ) :assumption (or (not b582) (not b1215) ) :assumption (or (not b579) (not b1187) ) :assumption (or (not b582) (not b1193) ) :assumption (or (not b585) (not b1199) ) :assumption (or (not b579) (not b1166) ) :assumption (or (not b582) (not b1171) ) :assumption (or (not b585) (not b1176) ) :assumption (or (not b579) (not b1143) ) :assumption (or (not b582) (not b1149) ) :assumption (or (not b585) (not b1155) ) :assumption (or (not b579) (not b1110) ) :assumption (or (not b582) (not b1117) ) :assumption (or (not b585) (not b1124) ) :assumption (or (not b588) (not b597) ) :assumption (or (not b591) (not b600) ) :assumption (or (not b594) (not b603) ) :assumption (or (not b588) (not b1227) ) :assumption (or (not b591) (not b1232) ) :assumption (or (not b588) (not b1210) ) :assumption (or (not b591) (not b1215) ) :assumption (or (not b588) (not b1187) ) :assumption (or (not b591) (not b1193) ) :assumption (or (not b594) (not b1199) ) :assumption (or (not b588) (not b1166) ) :assumption (or (not b591) (not b1171) ) :assumption (or (not b594) (not b1176) ) :assumption (or (not b588) (not b1143) ) :assumption (or (not b591) (not b1149) ) :assumption (or (not b594) (not b1155) ) :assumption (or (not b588) (not b1110) ) :assumption (or (not b591) (not b1117) ) :assumption (or (not b594) (not b1124) ) :assumption (or (not b597) (not b1227) ) :assumption (or (not b600) (not b1232) ) :assumption (or (not b597) (not b1210) ) :assumption (or (not b600) (not b1215) ) :assumption (or (not b597) (not b1187) ) :assumption (or (not b600) (not b1193) ) :assumption (or (not b603) (not b1199) ) :assumption (or (not b597) (not b1166) ) :assumption (or (not b600) (not b1171) ) :assumption (or (not b603) (not b1176) ) :assumption (or (not b597) (not b1143) ) :assumption (or (not b600) (not b1149) ) :assumption (or (not b603) (not b1155) ) :assumption (or (not b597) (not b1110) ) :assumption (or (not b600) (not b1117) ) :assumption (or (not b603) (not b1124) ) :assumption (or (not b606) (not b624) ) :assumption (or (not b609) (not b627) ) :assumption (or (not b612) (not b630) ) :assumption (or (not b606) (not b615) ) :assumption (or (not b609) (not b618) ) :assumption (or (not b612) (not b621) ) :assumption (or (not b606) (not b1081) ) :assumption (or (not b609) (not b1086) ) :assumption (or (not b612) (not b1091) ) :assumption (or (not b606) (not b1061) ) :assumption (or (not b609) (not b1066) ) :assumption (or (not b612) (not b1071) ) :assumption (or (not b606) (not b1038) ) :assumption (or (not b609) (not b1044) ) :assumption (or (not b612) (not b1050) ) :assumption (or (not b606) (not b1017) ) :assumption (or (not b609) (not b1022) ) :assumption (or (not b612) (not b1027) ) :assumption (or (not b606) (not b994) ) :assumption (or (not b609) (not b1000) ) :assumption (or (not b612) (not b1006) ) :assumption (or (not b606) (not b961) ) :assumption (or (not b609) (not b968) ) :assumption (or (not b612) (not b975) ) :assumption (or (not b615) (not b624) ) :assumption (or (not b618) (not b627) ) :assumption (or (not b621) (not b630) ) :assumption (or (not b615) (not b1081) ) :assumption (or (not b618) (not b1086) ) :assumption (or (not b621) (not b1091) ) :assumption (or (not b615) (not b1061) ) :assumption (or (not b618) (not b1066) ) :assumption (or (not b621) (not b1071) ) :assumption (or (not b615) (not b1038) ) :assumption (or (not b618) (not b1044) ) :assumption (or (not b621) (not b1050) ) :assumption (or (not b615) (not b1017) ) :assumption (or (not b618) (not b1022) ) :assumption (or (not b621) (not b1027) ) :assumption (or (not b615) (not b994) ) :assumption (or (not b618) (not b1000) ) :assumption (or (not b621) (not b1006) ) :assumption (or (not b615) (not b961) ) :assumption (or (not b618) (not b968) ) :assumption (or (not b621) (not b975) ) :assumption (or (not b624) (not b1081) ) :assumption (or (not b627) (not b1086) ) :assumption (or (not b630) (not b1091) ) :assumption (or (not b624) (not b1061) ) :assumption (or (not b627) (not b1066) ) :assumption (or (not b630) (not b1071) ) :assumption (or (not b624) (not b1038) ) :assumption (or (not b627) (not b1044) ) :assumption (or (not b630) (not b1050) ) :assumption (or (not b624) (not b1017) ) :assumption (or (not b627) (not b1022) ) :assumption (or (not b630) (not b1027) ) :assumption (or (not b624) (not b994) ) :assumption (or (not b627) (not b1000) ) :assumption (or (not b630) (not b1006) ) :assumption (or (not b624) (not b961) ) :assumption (or (not b627) (not b968) ) :assumption (or (not b630) (not b975) ) :assumption (or (not b633) (not b651) ) :assumption (or (not b636) (not b654) ) :assumption (or (not b639) (not b657) ) :assumption (or (not b633) (not b642) ) :assumption (or (not b636) (not b645) ) :assumption (or (not b639) (not b648) ) :assumption (or (not b633) (not b1227) ) :assumption (or (not b636) (not b1232) ) :assumption (or (not b633) (not b1210) ) :assumption (or (not b636) (not b1215) ) :assumption (or (not b633) (not b1187) ) :assumption (or (not b636) (not b1193) ) :assumption (or (not b639) (not b1199) ) :assumption (or (not b633) (not b1166) ) :assumption (or (not b636) (not b1171) ) :assumption (or (not b639) (not b1176) ) :assumption (or (not b633) (not b1143) ) :assumption (or (not b636) (not b1149) ) :assumption (or (not b639) (not b1155) ) :assumption (or (not b633) (not b1110) ) :assumption (or (not b636) (not b1117) ) :assumption (or (not b639) (not b1124) ) :assumption (or (not b642) (not b651) ) :assumption (or (not b645) (not b654) ) :assumption (or (not b648) (not b657) ) :assumption (or (not b642) (not b1227) ) :assumption (or (not b645) (not b1232) ) :assumption (or (not b642) (not b1210) ) :assumption (or (not b645) (not b1215) ) :assumption (or (not b642) (not b1187) ) :assumption (or (not b645) (not b1193) ) :assumption (or (not b648) (not b1199) ) :assumption (or (not b642) (not b1166) ) :assumption (or (not b645) (not b1171) ) :assumption (or (not b648) (not b1176) ) :assumption (or (not b642) (not b1143) ) :assumption (or (not b645) (not b1149) ) :assumption (or (not b648) (not b1155) ) :assumption (or (not b642) (not b1110) ) :assumption (or (not b645) (not b1117) ) :assumption (or (not b648) (not b1124) ) :assumption (or (not b651) (not b1227) ) :assumption (or (not b654) (not b1232) ) :assumption (or (not b651) (not b1210) ) :assumption (or (not b654) (not b1215) ) :assumption (or (not b651) (not b1187) ) :assumption (or (not b654) (not b1193) ) :assumption (or (not b657) (not b1199) ) :assumption (or (not b651) (not b1166) ) :assumption (or (not b654) (not b1171) ) :assumption (or (not b657) (not b1176) ) :assumption (or (not b651) (not b1143) ) :assumption (or (not b654) (not b1149) ) :assumption (or (not b657) (not b1155) ) :assumption (or (not b651) (not b1110) ) :assumption (or (not b654) (not b1117) ) :assumption (or (not b657) (not b1124) ) :assumption (or (not b660) (not b1238) ) :assumption (or (not b666) (not b1241) ) :assumption (or (not b672) (not b1244) ) :assumption (or (not b678) (not b1247) ) :assumption (or (not b684) (not b1250) ) :assumption (or (not b660) (not b982) ) :assumption (or (not b666) (not b988) ) :assumption (or (not b672) (not b994) ) :assumption (or (not b678) (not b1000) ) :assumption (or (not b684) (not b1006) ) :assumption (or (not b660) (not b947) ) :assumption (or (not b666) (not b954) ) :assumption (or (not b672) (not b961) ) :assumption (or (not b678) (not b968) ) :assumption (or (not b684) (not b975) ) :assumption (or (not b660) (not b692) ) :assumption (or (not b666) (not b698) ) :assumption (or (not b672) (not b704) ) :assumption (or (not b678) (not b710) ) :assumption (or (not b684) (not b716) ) :assumption (or (not b606) (not b672) ) :assumption (or (not b609) (not b678) ) :assumption (or (not b612) (not b684) ) :assumption (or (not b552) (not b672) ) :assumption (or (not b555) (not b678) ) :assumption (or (not b558) (not b684) ) :assumption (or (not b498) (not b672) ) :assumption (or (not b501) (not b678) ) :assumption (or (not b504) (not b684) ) :assumption (or (not b444) (not b672) ) :assumption (or (not b447) (not b678) ) :assumption (or (not b450) (not b684) ) :assumption (or (not b372) (not b666) ) :assumption (or (not b375) (not b672) ) :assumption (or (not b378) (not b678) ) :assumption (or (not b381) (not b684) ) :assumption (or (not b306) (not b678) ) :assumption (or (not b312) (not b684) ) :assumption (or (not b243) (not b678) ) :assumption (or (not b182) (not b678) ) :assumption (or (not b188) (not b684) ) :assumption (or (not b117) (not b678) ) :assumption (or (not b123) (not b684) ) :assumption (or (not b15) (not b660) ) :assumption (or (not b20) (not b666) ) :assumption (or (not b26) (not b672) ) :assumption (or (not b32) (not b678) ) :assumption (or (not b666) (not b1056) ) :assumption (or (not b672) (not b1061) ) :assumption (or (not b678) (not b1066) ) :assumption (or (not b684) (not b1071) ) :assumption (or (not b666) (not b1012) ) :assumption (or (not b672) (not b1017) ) :assumption (or (not b678) (not b1022) ) :assumption (or (not b684) (not b1027) ) :assumption (or (not b666) (not b767) ) :assumption (or (not b672) (not b772) ) :assumption (or (not b678) (not b777) ) :assumption (or (not b684) (not b782) ) :assumption (or (not b666) (not b723) ) :assumption (or (not b672) (not b728) ) :assumption (or (not b678) (not b733) ) :assumption (or (not b684) (not b738) ) :assumption (or (not b666) (not b1253) ) :assumption (or (not b672) (not b1254) ) :assumption (or (not b678) (not b1255) ) :assumption (or (not b684) (not b1256) ) :assumption (or (not b666) (not b1032) ) :assumption (or (not b672) (not b1038) ) :assumption (or (not b678) (not b1044) ) :assumption (or (not b684) (not b1050) ) :assumption (or (not b666) (not b743) ) :assumption (or (not b672) (not b749) ) :assumption (or (not b678) (not b755) ) :assumption (or (not b684) (not b761) ) :assumption (or (not b615) (not b672) ) :assumption (or (not b618) (not b678) ) :assumption (or (not b621) (not b684) ) :assumption (or (not b561) (not b672) ) :assumption (or (not b564) (not b678) ) :assumption (or (not b567) (not b684) ) :assumption (or (not b507) (not b672) ) :assumption (or (not b510) (not b678) ) :assumption (or (not b513) (not b684) ) :assumption (or (not b453) (not b672) ) :assumption (or (not b456) (not b678) ) :assumption (or (not b459) (not b684) ) :assumption (or (not b384) (not b666) ) :assumption (or (not b387) (not b672) ) :assumption (or (not b390) (not b678) ) :assumption (or (not b393) (not b684) ) :assumption (or (not b317) (not b678) ) :assumption (or (not b322) (not b684) ) :assumption (or (not b251) (not b666) ) :assumption (or (not b257) (not b672) ) :assumption (or (not b262) (not b678) ) :assumption (or (not b266) (not b684) ) :assumption (or (not b193) (not b678) ) :assumption (or (not b198) (not b684) ) :assumption (or (not b129) (not b678) ) :assumption (or (not b40) (not b672) ) :assumption (or (not b46) (not b678) ) :assumption (or (not b51) (not b684) ) :assumption (or (not b666) (not b1257) ) :assumption (or (not b672) (not b1258) ) :assumption (or (not b678) (not b1259) ) :assumption (or (not b684) (not b1260) ) :assumption (or (not b666) (not b1076) ) :assumption (or (not b672) (not b1081) ) :assumption (or (not b678) (not b1086) ) :assumption (or (not b684) (not b1091) ) :assumption (or (not b666) (not b787) ) :assumption (or (not b672) (not b792) ) :assumption (or (not b678) (not b797) ) :assumption (or (not b684) (not b802) ) :assumption (or (not b692) (not b1238) ) :assumption (or (not b698) (not b1241) ) :assumption (or (not b704) (not b1244) ) :assumption (or (not b710) (not b1247) ) :assumption (or (not b716) (not b1250) ) :assumption (or (not b692) (not b982) ) :assumption (or (not b698) (not b988) ) :assumption (or (not b704) (not b994) ) :assumption (or (not b710) (not b1000) ) :assumption (or (not b716) (not b1006) ) :assumption (or (not b692) (not b947) ) :assumption (or (not b698) (not b954) ) :assumption (or (not b704) (not b961) ) :assumption (or (not b710) (not b968) ) :assumption (or (not b716) (not b975) ) :assumption (or (not b606) (not b704) ) :assumption (or (not b609) (not b710) ) :assumption (or (not b612) (not b716) ) :assumption (or (not b552) (not b704) ) :assumption (or (not b555) (not b710) ) :assumption (or (not b558) (not b716) ) :assumption (or (not b498) (not b704) ) :assumption (or (not b501) (not b710) ) :assumption (or (not b504) (not b716) ) :assumption (or (not b444) (not b704) ) :assumption (or (not b447) (not b710) ) :assumption (or (not b450) (not b716) ) :assumption (or (not b372) (not b698) ) :assumption (or (not b375) (not b704) ) :assumption (or (not b378) (not b710) ) :assumption (or (not b381) (not b716) ) :assumption (or (not b306) (not b710) ) :assumption (or (not b312) (not b716) ) :assumption (or (not b243) (not b710) ) :assumption (or (not b182) (not b710) ) :assumption (or (not b188) (not b716) ) :assumption (or (not b117) (not b710) ) :assumption (or (not b123) (not b716) ) :assumption (or (not b15) (not b692) ) :assumption (or (not b20) (not b698) ) :assumption (or (not b26) (not b704) ) :assumption (or (not b32) (not b710) ) :assumption (or (not b698) (not b1056) ) :assumption (or (not b704) (not b1061) ) :assumption (or (not b710) (not b1066) ) :assumption (or (not b716) (not b1071) ) :assumption (or (not b698) (not b1012) ) :assumption (or (not b704) (not b1017) ) :assumption (or (not b710) (not b1022) ) :assumption (or (not b716) (not b1027) ) :assumption (or (not b698) (not b767) ) :assumption (or (not b704) (not b772) ) :assumption (or (not b710) (not b777) ) :assumption (or (not b716) (not b782) ) :assumption (or (not b698) (not b723) ) :assumption (or (not b704) (not b728) ) :assumption (or (not b710) (not b733) ) :assumption (or (not b716) (not b738) ) :assumption (or (not b698) (not b1257) ) :assumption (or (not b704) (not b1258) ) :assumption (or (not b710) (not b1259) ) :assumption (or (not b716) (not b1260) ) :assumption (or (not b698) (not b1076) ) :assumption (or (not b704) (not b1081) ) :assumption (or (not b710) (not b1086) ) :assumption (or (not b716) (not b1091) ) :assumption (or (not b698) (not b787) ) :assumption (or (not b704) (not b792) ) :assumption (or (not b710) (not b797) ) :assumption (or (not b716) (not b802) ) :assumption (or (not b624) (not b704) ) :assumption (or (not b627) (not b710) ) :assumption (or (not b630) (not b716) ) :assumption (or (not b570) (not b704) ) :assumption (or (not b573) (not b710) ) :assumption (or (not b576) (not b716) ) :assumption (or (not b516) (not b704) ) :assumption (or (not b519) (not b710) ) :assumption (or (not b522) (not b716) ) :assumption (or (not b462) (not b704) ) :assumption (or (not b465) (not b710) ) :assumption (or (not b468) (not b716) ) :assumption (or (not b396) (not b698) ) :assumption (or (not b399) (not b704) ) :assumption (or (not b402) (not b710) ) :assumption (or (not b405) (not b716) ) :assumption (or (not b326) (not b698) ) :assumption (or (not b331) (not b704) ) :assumption (or (not b336) (not b710) ) :assumption (or (not b340) (not b716) ) :assumption (or (not b270) (not b710) ) :assumption (or (not b275) (not b716) ) :assumption (or (not b202) (not b698) ) :assumption (or (not b207) (not b704) ) :assumption (or (not b212) (not b710) ) :assumption (or (not b135) (not b698) ) :assumption (or (not b141) (not b704) ) :assumption (or (not b146) (not b710) ) :assumption (or (not b150) (not b716) ) :assumption (or (not b56) (not b704) ) :assumption (or (not b62) (not b710) ) :assumption (or (not b67) (not b716) ) :assumption (or (not b698) (not b1253) ) :assumption (or (not b704) (not b1254) ) :assumption (or (not b710) (not b1255) ) :assumption (or (not b716) (not b1256) ) :assumption (or (not b698) (not b1032) ) :assumption (or (not b704) (not b1038) ) :assumption (or (not b710) (not b1044) ) :assumption (or (not b716) (not b1050) ) :assumption (or (not b698) (not b743) ) :assumption (or (not b704) (not b749) ) :assumption (or (not b710) (not b755) ) :assumption (or (not b716) (not b761) ) :assumption (or (not b723) (not b1253) ) :assumption (or (not b728) (not b1254) ) :assumption (or (not b733) (not b1255) ) :assumption (or (not b738) (not b1256) ) :assumption (or (not b723) (not b1032) ) :assumption (or (not b728) (not b1038) ) :assumption (or (not b733) (not b1044) ) :assumption (or (not b738) (not b1050) ) :assumption (or (not b723) (not b1012) ) :assumption (or (not b728) (not b1017) ) :assumption (or (not b733) (not b1022) ) :assumption (or (not b738) (not b1027) ) :assumption (or (not b723) (not b743) ) :assumption (or (not b728) (not b749) ) :assumption (or (not b733) (not b755) ) :assumption (or (not b738) (not b761) ) :assumption (or (not b615) (not b728) ) :assumption (or (not b618) (not b733) ) :assumption (or (not b621) (not b738) ) :assumption (or (not b561) (not b728) ) :assumption (or (not b564) (not b733) ) :assumption (or (not b567) (not b738) ) :assumption (or (not b507) (not b728) ) :assumption (or (not b510) (not b733) ) :assumption (or (not b513) (not b738) ) :assumption (or (not b453) (not b728) ) :assumption (or (not b456) (not b733) ) :assumption (or (not b459) (not b738) ) :assumption (or (not b384) (not b723) ) :assumption (or (not b387) (not b728) ) :assumption (or (not b390) (not b733) ) :assumption (or (not b393) (not b738) ) :assumption (or (not b317) (not b733) ) :assumption (or (not b322) (not b738) ) :assumption (or (not b251) (not b723) ) :assumption (or (not b257) (not b728) ) :assumption (or (not b262) (not b733) ) :assumption (or (not b266) (not b738) ) :assumption (or (not b193) (not b733) ) :assumption (or (not b198) (not b738) ) :assumption (or (not b129) (not b733) ) :assumption (or (not b40) (not b728) ) :assumption (or (not b46) (not b733) ) :assumption (or (not b51) (not b738) ) :assumption (or (not b723) (not b1076) ) :assumption (or (not b728) (not b1081) ) :assumption (or (not b733) (not b1086) ) :assumption (or (not b738) (not b1091) ) :assumption (or (not b723) (not b954) ) :assumption (or (not b728) (not b961) ) :assumption (or (not b733) (not b968) ) :assumption (or (not b738) (not b975) ) :assumption (or (not b723) (not b787) ) :assumption (or (not b728) (not b792) ) :assumption (or (not b733) (not b797) ) :assumption (or (not b738) (not b802) ) :assumption (or (not b723) (not b1241) ) :assumption (or (not b728) (not b1244) ) :assumption (or (not b733) (not b1247) ) :assumption (or (not b738) (not b1250) ) :assumption (or (not b723) (not b988) ) :assumption (or (not b728) (not b994) ) :assumption (or (not b733) (not b1000) ) :assumption (or (not b738) (not b1006) ) :assumption (or (not b606) (not b728) ) :assumption (or (not b609) (not b733) ) :assumption (or (not b612) (not b738) ) :assumption (or (not b552) (not b728) ) :assumption (or (not b555) (not b733) ) :assumption (or (not b558) (not b738) ) :assumption (or (not b498) (not b728) ) :assumption (or (not b501) (not b733) ) :assumption (or (not b504) (not b738) ) :assumption (or (not b444) (not b728) ) :assumption (or (not b447) (not b733) ) :assumption (or (not b450) (not b738) ) :assumption (or (not b372) (not b723) ) :assumption (or (not b375) (not b728) ) :assumption (or (not b378) (not b733) ) :assumption (or (not b381) (not b738) ) :assumption (or (not b306) (not b733) ) :assumption (or (not b312) (not b738) ) :assumption (or (not b243) (not b733) ) :assumption (or (not b182) (not b733) ) :assumption (or (not b188) (not b738) ) :assumption (or (not b117) (not b733) ) :assumption (or (not b123) (not b738) ) :assumption (or (not b20) (not b723) ) :assumption (or (not b26) (not b728) ) :assumption (or (not b32) (not b733) ) :assumption (or (not b723) (not b1257) ) :assumption (or (not b728) (not b1258) ) :assumption (or (not b733) (not b1259) ) :assumption (or (not b738) (not b1260) ) :assumption (or (not b723) (not b1056) ) :assumption (or (not b728) (not b1061) ) :assumption (or (not b733) (not b1066) ) :assumption (or (not b738) (not b1071) ) :assumption (or (not b723) (not b767) ) :assumption (or (not b728) (not b772) ) :assumption (or (not b733) (not b777) ) :assumption (or (not b738) (not b782) ) :assumption (or (not b743) (not b1253) ) :assumption (or (not b749) (not b1254) ) :assumption (or (not b755) (not b1255) ) :assumption (or (not b761) (not b1256) ) :assumption (or (not b743) (not b1032) ) :assumption (or (not b749) (not b1038) ) :assumption (or (not b755) (not b1044) ) :assumption (or (not b761) (not b1050) ) :assumption (or (not b743) (not b1012) ) :assumption (or (not b749) (not b1017) ) :assumption (or (not b755) (not b1022) ) :assumption (or (not b761) (not b1027) ) :assumption (or (not b615) (not b749) ) :assumption (or (not b618) (not b755) ) :assumption (or (not b621) (not b761) ) :assumption (or (not b561) (not b749) ) :assumption (or (not b564) (not b755) ) :assumption (or (not b567) (not b761) ) :assumption (or (not b507) (not b749) ) :assumption (or (not b510) (not b755) ) :assumption (or (not b513) (not b761) ) :assumption (or (not b453) (not b749) ) :assumption (or (not b456) (not b755) ) :assumption (or (not b459) (not b761) ) :assumption (or (not b384) (not b743) ) :assumption (or (not b387) (not b749) ) :assumption (or (not b390) (not b755) ) :assumption (or (not b393) (not b761) ) :assumption (or (not b317) (not b755) ) :assumption (or (not b322) (not b761) ) :assumption (or (not b251) (not b743) ) :assumption (or (not b257) (not b749) ) :assumption (or (not b262) (not b755) ) :assumption (or (not b266) (not b761) ) :assumption (or (not b193) (not b755) ) :assumption (or (not b198) (not b761) ) :assumption (or (not b129) (not b755) ) :assumption (or (not b40) (not b749) ) :assumption (or (not b46) (not b755) ) :assumption (or (not b51) (not b761) ) :assumption (or (not b743) (not b1076) ) :assumption (or (not b749) (not b1081) ) :assumption (or (not b755) (not b1086) ) :assumption (or (not b761) (not b1091) ) :assumption (or (not b743) (not b954) ) :assumption (or (not b749) (not b961) ) :assumption (or (not b755) (not b968) ) :assumption (or (not b761) (not b975) ) :assumption (or (not b743) (not b787) ) :assumption (or (not b749) (not b792) ) :assumption (or (not b755) (not b797) ) :assumption (or (not b761) (not b802) ) :assumption (or (not b743) (not b1257) ) :assumption (or (not b749) (not b1258) ) :assumption (or (not b755) (not b1259) ) :assumption (or (not b761) (not b1260) ) :assumption (or (not b743) (not b1056) ) :assumption (or (not b749) (not b1061) ) :assumption (or (not b755) (not b1066) ) :assumption (or (not b761) (not b1071) ) :assumption (or (not b743) (not b767) ) :assumption (or (not b749) (not b772) ) :assumption (or (not b755) (not b777) ) :assumption (or (not b761) (not b782) ) :assumption (or (not b624) (not b749) ) :assumption (or (not b627) (not b755) ) :assumption (or (not b630) (not b761) ) :assumption (or (not b570) (not b749) ) :assumption (or (not b573) (not b755) ) :assumption (or (not b576) (not b761) ) :assumption (or (not b516) (not b749) ) :assumption (or (not b519) (not b755) ) :assumption (or (not b522) (not b761) ) :assumption (or (not b462) (not b749) ) :assumption (or (not b465) (not b755) ) :assumption (or (not b468) (not b761) ) :assumption (or (not b396) (not b743) ) :assumption (or (not b399) (not b749) ) :assumption (or (not b402) (not b755) ) :assumption (or (not b405) (not b761) ) :assumption (or (not b326) (not b743) ) :assumption (or (not b331) (not b749) ) :assumption (or (not b336) (not b755) ) :assumption (or (not b340) (not b761) ) :assumption (or (not b270) (not b755) ) :assumption (or (not b275) (not b761) ) :assumption (or (not b202) (not b743) ) :assumption (or (not b207) (not b749) ) :assumption (or (not b212) (not b755) ) :assumption (or (not b135) (not b743) ) :assumption (or (not b141) (not b749) ) :assumption (or (not b146) (not b755) ) :assumption (or (not b150) (not b761) ) :assumption (or (not b56) (not b749) ) :assumption (or (not b62) (not b755) ) :assumption (or (not b67) (not b761) ) :assumption (or (not b743) (not b1241) ) :assumption (or (not b749) (not b1244) ) :assumption (or (not b755) (not b1247) ) :assumption (or (not b761) (not b1250) ) :assumption (or (not b743) (not b988) ) :assumption (or (not b749) (not b994) ) :assumption (or (not b755) (not b1000) ) :assumption (or (not b761) (not b1006) ) :assumption (or (not b767) (not b1257) ) :assumption (or (not b772) (not b1258) ) :assumption (or (not b777) (not b1259) ) :assumption (or (not b782) (not b1260) ) :assumption (or (not b767) (not b1076) ) :assumption (or (not b772) (not b1081) ) :assumption (or (not b777) (not b1086) ) :assumption (or (not b782) (not b1091) ) :assumption (or (not b767) (not b1056) ) :assumption (or (not b772) (not b1061) ) :assumption (or (not b777) (not b1066) ) :assumption (or (not b782) (not b1071) ) :assumption (or (not b767) (not b787) ) :assumption (or (not b772) (not b792) ) :assumption (or (not b777) (not b797) ) :assumption (or (not b782) (not b802) ) :assumption (or (not b624) (not b772) ) :assumption (or (not b627) (not b777) ) :assumption (or (not b630) (not b782) ) :assumption (or (not b570) (not b772) ) :assumption (or (not b573) (not b777) ) :assumption (or (not b576) (not b782) ) :assumption (or (not b516) (not b772) ) :assumption (or (not b519) (not b777) ) :assumption (or (not b522) (not b782) ) :assumption (or (not b462) (not b772) ) :assumption (or (not b465) (not b777) ) :assumption (or (not b468) (not b782) ) :assumption (or (not b396) (not b767) ) :assumption (or (not b399) (not b772) ) :assumption (or (not b402) (not b777) ) :assumption (or (not b405) (not b782) ) :assumption (or (not b326) (not b767) ) :assumption (or (not b331) (not b772) ) :assumption (or (not b336) (not b777) ) :assumption (or (not b340) (not b782) ) :assumption (or (not b270) (not b777) ) :assumption (or (not b275) (not b782) ) :assumption (or (not b202) (not b767) ) :assumption (or (not b207) (not b772) ) :assumption (or (not b212) (not b777) ) :assumption (or (not b135) (not b767) ) :assumption (or (not b141) (not b772) ) :assumption (or (not b146) (not b777) ) :assumption (or (not b150) (not b782) ) :assumption (or (not b56) (not b772) ) :assumption (or (not b62) (not b777) ) :assumption (or (not b67) (not b782) ) :assumption (or (not b767) (not b1032) ) :assumption (or (not b772) (not b1038) ) :assumption (or (not b777) (not b1044) ) :assumption (or (not b782) (not b1050) ) :assumption (or (not b767) (not b988) ) :assumption (or (not b772) (not b994) ) :assumption (or (not b777) (not b1000) ) :assumption (or (not b782) (not b1006) ) :assumption (or (not b767) (not b1241) ) :assumption (or (not b772) (not b1244) ) :assumption (or (not b777) (not b1247) ) :assumption (or (not b782) (not b1250) ) :assumption (or (not b767) (not b954) ) :assumption (or (not b772) (not b961) ) :assumption (or (not b777) (not b968) ) :assumption (or (not b782) (not b975) ) :assumption (or (not b606) (not b772) ) :assumption (or (not b609) (not b777) ) :assumption (or (not b612) (not b782) ) :assumption (or (not b552) (not b772) ) :assumption (or (not b555) (not b777) ) :assumption (or (not b558) (not b782) ) :assumption (or (not b498) (not b772) ) :assumption (or (not b501) (not b777) ) :assumption (or (not b504) (not b782) ) :assumption (or (not b444) (not b772) ) :assumption (or (not b447) (not b777) ) :assumption (or (not b450) (not b782) ) :assumption (or (not b372) (not b767) ) :assumption (or (not b375) (not b772) ) :assumption (or (not b378) (not b777) ) :assumption (or (not b381) (not b782) ) :assumption (or (not b306) (not b777) ) :assumption (or (not b312) (not b782) ) :assumption (or (not b243) (not b777) ) :assumption (or (not b182) (not b777) ) :assumption (or (not b188) (not b782) ) :assumption (or (not b117) (not b777) ) :assumption (or (not b123) (not b782) ) :assumption (or (not b20) (not b767) ) :assumption (or (not b26) (not b772) ) :assumption (or (not b32) (not b777) ) :assumption (or (not b767) (not b1253) ) :assumption (or (not b772) (not b1254) ) :assumption (or (not b777) (not b1255) ) :assumption (or (not b782) (not b1256) ) :assumption (or (not b767) (not b1012) ) :assumption (or (not b772) (not b1017) ) :assumption (or (not b777) (not b1022) ) :assumption (or (not b782) (not b1027) ) :assumption (or (not b787) (not b1257) ) :assumption (or (not b792) (not b1258) ) :assumption (or (not b797) (not b1259) ) :assumption (or (not b802) (not b1260) ) :assumption (or (not b787) (not b1076) ) :assumption (or (not b792) (not b1081) ) :assumption (or (not b797) (not b1086) ) :assumption (or (not b802) (not b1091) ) :assumption (or (not b787) (not b1056) ) :assumption (or (not b792) (not b1061) ) :assumption (or (not b797) (not b1066) ) :assumption (or (not b802) (not b1071) ) :assumption (or (not b624) (not b792) ) :assumption (or (not b627) (not b797) ) :assumption (or (not b630) (not b802) ) :assumption (or (not b570) (not b792) ) :assumption (or (not b573) (not b797) ) :assumption (or (not b576) (not b802) ) :assumption (or (not b516) (not b792) ) :assumption (or (not b519) (not b797) ) :assumption (or (not b522) (not b802) ) :assumption (or (not b462) (not b792) ) :assumption (or (not b465) (not b797) ) :assumption (or (not b468) (not b802) ) :assumption (or (not b396) (not b787) ) :assumption (or (not b399) (not b792) ) :assumption (or (not b402) (not b797) ) :assumption (or (not b405) (not b802) ) :assumption (or (not b326) (not b787) ) :assumption (or (not b331) (not b792) ) :assumption (or (not b336) (not b797) ) :assumption (or (not b340) (not b802) ) :assumption (or (not b270) (not b797) ) :assumption (or (not b275) (not b802) ) :assumption (or (not b202) (not b787) ) :assumption (or (not b207) (not b792) ) :assumption (or (not b212) (not b797) ) :assumption (or (not b135) (not b787) ) :assumption (or (not b141) (not b792) ) :assumption (or (not b146) (not b797) ) :assumption (or (not b150) (not b802) ) :assumption (or (not b56) (not b792) ) :assumption (or (not b62) (not b797) ) :assumption (or (not b67) (not b802) ) :assumption (or (not b787) (not b1032) ) :assumption (or (not b792) (not b1038) ) :assumption (or (not b797) (not b1044) ) :assumption (or (not b802) (not b1050) ) :assumption (or (not b787) (not b988) ) :assumption (or (not b792) (not b994) ) :assumption (or (not b797) (not b1000) ) :assumption (or (not b802) (not b1006) ) :assumption (or (not b787) (not b1253) ) :assumption (or (not b792) (not b1254) ) :assumption (or (not b797) (not b1255) ) :assumption (or (not b802) (not b1256) ) :assumption (or (not b787) (not b1012) ) :assumption (or (not b792) (not b1017) ) :assumption (or (not b797) (not b1022) ) :assumption (or (not b802) (not b1027) ) :assumption (or (not b615) (not b792) ) :assumption (or (not b618) (not b797) ) :assumption (or (not b621) (not b802) ) :assumption (or (not b561) (not b792) ) :assumption (or (not b564) (not b797) ) :assumption (or (not b567) (not b802) ) :assumption (or (not b507) (not b792) ) :assumption (or (not b510) (not b797) ) :assumption (or (not b513) (not b802) ) :assumption (or (not b453) (not b792) ) :assumption (or (not b456) (not b797) ) :assumption (or (not b459) (not b802) ) :assumption (or (not b384) (not b787) ) :assumption (or (not b387) (not b792) ) :assumption (or (not b390) (not b797) ) :assumption (or (not b393) (not b802) ) :assumption (or (not b317) (not b797) ) :assumption (or (not b322) (not b802) ) :assumption (or (not b251) (not b787) ) :assumption (or (not b257) (not b792) ) :assumption (or (not b262) (not b797) ) :assumption (or (not b266) (not b802) ) :assumption (or (not b193) (not b797) ) :assumption (or (not b198) (not b802) ) :assumption (or (not b129) (not b797) ) :assumption (or (not b40) (not b792) ) :assumption (or (not b46) (not b797) ) :assumption (or (not b51) (not b802) ) :assumption (or (not b787) (not b1241) ) :assumption (or (not b792) (not b1244) ) :assumption (or (not b797) (not b1247) ) :assumption (or (not b802) (not b1250) ) :assumption (or (not b787) (not b954) ) :assumption (or (not b792) (not b961) ) :assumption (or (not b797) (not b968) ) :assumption (or (not b802) (not b975) ) :assumption (or (not b807) (not b1261) ) :assumption (or (not b813) (not b1264) ) :assumption (or (not b819) (not b1267) ) :assumption (or (not b825) (not b1270) ) :assumption (or (not b831) (not b1273) ) :assumption (or (not b807) (not b1131) ) :assumption (or (not b813) (not b1137) ) :assumption (or (not b819) (not b1143) ) :assumption (or (not b825) (not b1149) ) :assumption (or (not b831) (not b1155) ) :assumption (or (not b807) (not b1096) ) :assumption (or (not b813) (not b1103) ) :assumption (or (not b819) (not b1110) ) :assumption (or (not b825) (not b1117) ) :assumption (or (not b831) (not b1124) ) :assumption (or (not b807) (not b839) ) :assumption (or (not b813) (not b845) ) :assumption (or (not b819) (not b851) ) :assumption (or (not b825) (not b857) ) :assumption (or (not b831) (not b863) ) :assumption (or (not b633) (not b819) ) :assumption (or (not b636) (not b825) ) :assumption (or (not b639) (not b831) ) :assumption (or (not b579) (not b819) ) :assumption (or (not b582) (not b825) ) :assumption (or (not b585) (not b831) ) :assumption (or (not b525) (not b819) ) :assumption (or (not b528) (not b825) ) :assumption (or (not b531) (not b831) ) :assumption (or (not b471) (not b819) ) :assumption (or (not b474) (not b825) ) :assumption (or (not b477) (not b831) ) :assumption (or (not b408) (not b813) ) :assumption (or (not b411) (not b819) ) :assumption (or (not b414) (not b825) ) :assumption (or (not b417) (not b831) ) :assumption (or (not b344) (not b825) ) :assumption (or (not b348) (not b831) ) :assumption (or (not b279) (not b825) ) :assumption (or (not b217) (not b825) ) :assumption (or (not b221) (not b831) ) :assumption (or (not b154) (not b825) ) :assumption (or (not b158) (not b831) ) :assumption (or (not b72) (not b807) ) :assumption (or (not b76) (not b813) ) :assumption (or (not b81) (not b819) ) :assumption (or (not b86) (not b825) ) :assumption (or (not b813) (not b1205) ) :assumption (or (not b819) (not b1210) ) :assumption (or (not b825) (not b1215) ) :assumption (or (not b813) (not b1161) ) :assumption (or (not b819) (not b1166) ) :assumption (or (not b825) (not b1171) ) :assumption (or (not b831) (not b1176) ) :assumption (or (not b813) (not b913) ) :assumption (or (not b819) (not b918) ) :assumption (or (not b825) (not b923) ) :assumption (or (not b813) (not b869) ) :assumption (or (not b819) (not b874) ) :assumption (or (not b825) (not b879) ) :assumption (or (not b831) (not b884) ) :assumption (or (not b813) (not b1276) ) :assumption (or (not b819) (not b1277) ) :assumption (or (not b825) (not b1278) ) :assumption (or (not b831) (not b1279) ) :assumption (or (not b813) (not b1181) ) :assumption (or (not b819) (not b1187) ) :assumption (or (not b825) (not b1193) ) :assumption (or (not b831) (not b1199) ) :assumption (or (not b813) (not b889) ) :assumption (or (not b819) (not b895) ) :assumption (or (not b825) (not b901) ) :assumption (or (not b831) (not b907) ) :assumption (or (not b642) (not b819) ) :assumption (or (not b645) (not b825) ) :assumption (or (not b648) (not b831) ) :assumption (or (not b588) (not b819) ) :assumption (or (not b591) (not b825) ) :assumption (or (not b594) (not b831) ) :assumption (or (not b534) (not b819) ) :assumption (or (not b537) (not b825) ) :assumption (or (not b540) (not b831) ) :assumption (or (not b480) (not b819) ) :assumption (or (not b483) (not b825) ) :assumption (or (not b486) (not b831) ) :assumption (or (not b420) (not b813) ) :assumption (or (not b423) (not b819) ) :assumption (or (not b426) (not b825) ) :assumption (or (not b429) (not b831) ) :assumption (or (not b352) (not b825) ) :assumption (or (not b355) (not b831) ) :assumption (or (not b285) (not b813) ) :assumption (or (not b290) (not b819) ) :assumption (or (not b294) (not b825) ) :assumption (or (not b297) (not b831) ) :assumption (or (not b225) (not b825) ) :assumption (or (not b228) (not b831) ) :assumption (or (not b163) (not b825) ) :assumption (or (not b93) (not b819) ) :assumption (or (not b97) (not b825) ) :assumption (or (not b101) (not b831) ) :assumption (or (not b813) (not b1280) ) :assumption (or (not b819) (not b1281) ) :assumption (or (not b825) (not b1282) ) :assumption (or (not b831) (not b1283) ) :assumption (or (not b813) (not b1222) ) :assumption (or (not b819) (not b1227) ) :assumption (or (not b825) (not b1232) ) :assumption (or (not b813) (not b930) ) :assumption (or (not b819) (not b935) ) :assumption (or (not b825) (not b940) ) :assumption (or (not b839) (not b1261) ) :assumption (or (not b845) (not b1264) ) :assumption (or (not b851) (not b1267) ) :assumption (or (not b857) (not b1270) ) :assumption (or (not b863) (not b1273) ) :assumption (or (not b839) (not b1131) ) :assumption (or (not b845) (not b1137) ) :assumption (or (not b851) (not b1143) ) :assumption (or (not b857) (not b1149) ) :assumption (or (not b863) (not b1155) ) :assumption (or (not b839) (not b1096) ) :assumption (or (not b845) (not b1103) ) :assumption (or (not b851) (not b1110) ) :assumption (or (not b857) (not b1117) ) :assumption (or (not b863) (not b1124) ) :assumption (or (not b633) (not b851) ) :assumption (or (not b636) (not b857) ) :assumption (or (not b639) (not b863) ) :assumption (or (not b579) (not b851) ) :assumption (or (not b582) (not b857) ) :assumption (or (not b585) (not b863) ) :assumption (or (not b525) (not b851) ) :assumption (or (not b528) (not b857) ) :assumption (or (not b531) (not b863) ) :assumption (or (not b471) (not b851) ) :assumption (or (not b474) (not b857) ) :assumption (or (not b477) (not b863) ) :assumption (or (not b408) (not b845) ) :assumption (or (not b411) (not b851) ) :assumption (or (not b414) (not b857) ) :assumption (or (not b417) (not b863) ) :assumption (or (not b344) (not b857) ) :assumption (or (not b348) (not b863) ) :assumption (or (not b279) (not b857) ) :assumption (or (not b217) (not b857) ) :assumption (or (not b221) (not b863) ) :assumption (or (not b154) (not b857) ) :assumption (or (not b158) (not b863) ) :assumption (or (not b72) (not b839) ) :assumption (or (not b76) (not b845) ) :assumption (or (not b81) (not b851) ) :assumption (or (not b86) (not b857) ) :assumption (or (not b845) (not b1205) ) :assumption (or (not b851) (not b1210) ) :assumption (or (not b857) (not b1215) ) :assumption (or (not b845) (not b1161) ) :assumption (or (not b851) (not b1166) ) :assumption (or (not b857) (not b1171) ) :assumption (or (not b863) (not b1176) ) :assumption (or (not b845) (not b913) ) :assumption (or (not b851) (not b918) ) :assumption (or (not b857) (not b923) ) :assumption (or (not b845) (not b869) ) :assumption (or (not b851) (not b874) ) :assumption (or (not b857) (not b879) ) :assumption (or (not b863) (not b884) ) :assumption (or (not b845) (not b1280) ) :assumption (or (not b851) (not b1281) ) :assumption (or (not b857) (not b1282) ) :assumption (or (not b863) (not b1283) ) :assumption (or (not b845) (not b1222) ) :assumption (or (not b851) (not b1227) ) :assumption (or (not b857) (not b1232) ) :assumption (or (not b845) (not b930) ) :assumption (or (not b851) (not b935) ) :assumption (or (not b857) (not b940) ) :assumption (or (not b651) (not b851) ) :assumption (or (not b654) (not b857) ) :assumption (or (not b657) (not b863) ) :assumption (or (not b597) (not b851) ) :assumption (or (not b600) (not b857) ) :assumption (or (not b603) (not b863) ) :assumption (or (not b543) (not b851) ) :assumption (or (not b546) (not b857) ) :assumption (or (not b549) (not b863) ) :assumption (or (not b489) (not b851) ) :assumption (or (not b492) (not b857) ) :assumption (or (not b495) (not b863) ) :assumption (or (not b432) (not b845) ) :assumption (or (not b435) (not b851) ) :assumption (or (not b438) (not b857) ) :assumption (or (not b441) (not b863) ) :assumption (or (not b358) (not b845) ) :assumption (or (not b362) (not b851) ) :assumption (or (not b366) (not b857) ) :assumption (or (not b369) (not b863) ) :assumption (or (not b300) (not b857) ) :assumption (or (not b303) (not b863) ) :assumption (or (not b231) (not b845) ) :assumption (or (not b235) (not b851) ) :assumption (or (not b239) (not b857) ) :assumption (or (not b167) (not b845) ) :assumption (or (not b172) (not b851) ) :assumption (or (not b176) (not b857) ) :assumption (or (not b179) (not b863) ) :assumption (or (not b105) (not b851) ) :assumption (or (not b109) (not b857) ) :assumption (or (not b113) (not b863) ) :assumption (or (not b845) (not b1276) ) :assumption (or (not b851) (not b1277) ) :assumption (or (not b857) (not b1278) ) :assumption (or (not b863) (not b1279) ) :assumption (or (not b845) (not b1181) ) :assumption (or (not b851) (not b1187) ) :assumption (or (not b857) (not b1193) ) :assumption (or (not b863) (not b1199) ) :assumption (or (not b845) (not b889) ) :assumption (or (not b851) (not b895) ) :assumption (or (not b857) (not b901) ) :assumption (or (not b863) (not b907) ) :assumption (or (not b869) (not b1276) ) :assumption (or (not b874) (not b1277) ) :assumption (or (not b879) (not b1278) ) :assumption (or (not b884) (not b1279) ) :assumption (or (not b869) (not b1181) ) :assumption (or (not b874) (not b1187) ) :assumption (or (not b879) (not b1193) ) :assumption (or (not b884) (not b1199) ) :assumption (or (not b869) (not b1161) ) :assumption (or (not b874) (not b1166) ) :assumption (or (not b879) (not b1171) ) :assumption (or (not b884) (not b1176) ) :assumption (or (not b869) (not b889) ) :assumption (or (not b874) (not b895) ) :assumption (or (not b879) (not b901) ) :assumption (or (not b884) (not b907) ) :assumption (or (not b642) (not b874) ) :assumption (or (not b645) (not b879) ) :assumption (or (not b648) (not b884) ) :assumption (or (not b588) (not b874) ) :assumption (or (not b591) (not b879) ) :assumption (or (not b594) (not b884) ) :assumption (or (not b534) (not b874) ) :assumption (or (not b537) (not b879) ) :assumption (or (not b540) (not b884) ) :assumption (or (not b480) (not b874) ) :assumption (or (not b483) (not b879) ) :assumption (or (not b486) (not b884) ) :assumption (or (not b420) (not b869) ) :assumption (or (not b423) (not b874) ) :assumption (or (not b426) (not b879) ) :assumption (or (not b429) (not b884) ) :assumption (or (not b352) (not b879) ) :assumption (or (not b355) (not b884) ) :assumption (or (not b285) (not b869) ) :assumption (or (not b290) (not b874) ) :assumption (or (not b294) (not b879) ) :assumption (or (not b297) (not b884) ) :assumption (or (not b225) (not b879) ) :assumption (or (not b228) (not b884) ) :assumption (or (not b163) (not b879) ) :assumption (or (not b93) (not b874) ) :assumption (or (not b97) (not b879) ) :assumption (or (not b101) (not b884) ) :assumption (or (not b869) (not b1222) ) :assumption (or (not b874) (not b1227) ) :assumption (or (not b879) (not b1232) ) :assumption (or (not b869) (not b1103) ) :assumption (or (not b874) (not b1110) ) :assumption (or (not b879) (not b1117) ) :assumption (or (not b884) (not b1124) ) :assumption (or (not b869) (not b930) ) :assumption (or (not b874) (not b935) ) :assumption (or (not b879) (not b940) ) :assumption (or (not b869) (not b1264) ) :assumption (or (not b874) (not b1267) ) :assumption (or (not b879) (not b1270) ) :assumption (or (not b884) (not b1273) ) :assumption (or (not b869) (not b1137) ) :assumption (or (not b874) (not b1143) ) :assumption (or (not b879) (not b1149) ) :assumption (or (not b884) (not b1155) ) :assumption (or (not b633) (not b874) ) :assumption (or (not b636) (not b879) ) :assumption (or (not b639) (not b884) ) :assumption (or (not b579) (not b874) ) :assumption (or (not b582) (not b879) ) :assumption (or (not b585) (not b884) ) :assumption (or (not b525) (not b874) ) :assumption (or (not b528) (not b879) ) :assumption (or (not b531) (not b884) ) :assumption (or (not b471) (not b874) ) :assumption (or (not b474) (not b879) ) :assumption (or (not b477) (not b884) ) :assumption (or (not b408) (not b869) ) :assumption (or (not b411) (not b874) ) :assumption (or (not b414) (not b879) ) :assumption (or (not b417) (not b884) ) :assumption (or (not b344) (not b879) ) :assumption (or (not b348) (not b884) ) :assumption (or (not b279) (not b879) ) :assumption (or (not b217) (not b879) ) :assumption (or (not b221) (not b884) ) :assumption (or (not b154) (not b879) ) :assumption (or (not b158) (not b884) ) :assumption (or (not b76) (not b869) ) :assumption (or (not b81) (not b874) ) :assumption (or (not b86) (not b879) ) :assumption (or (not b869) (not b1280) ) :assumption (or (not b874) (not b1281) ) :assumption (or (not b879) (not b1282) ) :assumption (or (not b884) (not b1283) ) :assumption (or (not b869) (not b1205) ) :assumption (or (not b874) (not b1210) ) :assumption (or (not b879) (not b1215) ) :assumption (or (not b869) (not b913) ) :assumption (or (not b874) (not b918) ) :assumption (or (not b879) (not b923) ) :assumption (or (not b889) (not b1276) ) :assumption (or (not b895) (not b1277) ) :assumption (or (not b901) (not b1278) ) :assumption (or (not b907) (not b1279) ) :assumption (or (not b889) (not b1181) ) :assumption (or (not b895) (not b1187) ) :assumption (or (not b901) (not b1193) ) :assumption (or (not b907) (not b1199) ) :assumption (or (not b889) (not b1161) ) :assumption (or (not b895) (not b1166) ) :assumption (or (not b901) (not b1171) ) :assumption (or (not b907) (not b1176) ) :assumption (or (not b642) (not b895) ) :assumption (or (not b645) (not b901) ) :assumption (or (not b648) (not b907) ) :assumption (or (not b588) (not b895) ) :assumption (or (not b591) (not b901) ) :assumption (or (not b594) (not b907) ) :assumption (or (not b534) (not b895) ) :assumption (or (not b537) (not b901) ) :assumption (or (not b540) (not b907) ) :assumption (or (not b480) (not b895) ) :assumption (or (not b483) (not b901) ) :assumption (or (not b486) (not b907) ) :assumption (or (not b420) (not b889) ) :assumption (or (not b423) (not b895) ) :assumption (or (not b426) (not b901) ) :assumption (or (not b429) (not b907) ) :assumption (or (not b352) (not b901) ) :assumption (or (not b355) (not b907) ) :assumption (or (not b285) (not b889) ) :assumption (or (not b290) (not b895) ) :assumption (or (not b294) (not b901) ) :assumption (or (not b297) (not b907) ) :assumption (or (not b225) (not b901) ) :assumption (or (not b228) (not b907) ) :assumption (or (not b163) (not b901) ) :assumption (or (not b93) (not b895) ) :assumption (or (not b97) (not b901) ) :assumption (or (not b101) (not b907) ) :assumption (or (not b889) (not b1222) ) :assumption (or (not b895) (not b1227) ) :assumption (or (not b901) (not b1232) ) :assumption (or (not b889) (not b1103) ) :assumption (or (not b895) (not b1110) ) :assumption (or (not b901) (not b1117) ) :assumption (or (not b907) (not b1124) ) :assumption (or (not b889) (not b930) ) :assumption (or (not b895) (not b935) ) :assumption (or (not b901) (not b940) ) :assumption (or (not b889) (not b1280) ) :assumption (or (not b895) (not b1281) ) :assumption (or (not b901) (not b1282) ) :assumption (or (not b907) (not b1283) ) :assumption (or (not b889) (not b1205) ) :assumption (or (not b895) (not b1210) ) :assumption (or (not b901) (not b1215) ) :assumption (or (not b889) (not b913) ) :assumption (or (not b895) (not b918) ) :assumption (or (not b901) (not b923) ) :assumption (or (not b651) (not b895) ) :assumption (or (not b654) (not b901) ) :assumption (or (not b657) (not b907) ) :assumption (or (not b597) (not b895) ) :assumption (or (not b600) (not b901) ) :assumption (or (not b603) (not b907) ) :assumption (or (not b543) (not b895) ) :assumption (or (not b546) (not b901) ) :assumption (or (not b549) (not b907) ) :assumption (or (not b489) (not b895) ) :assumption (or (not b492) (not b901) ) :assumption (or (not b495) (not b907) ) :assumption (or (not b432) (not b889) ) :assumption (or (not b435) (not b895) ) :assumption (or (not b438) (not b901) ) :assumption (or (not b441) (not b907) ) :assumption (or (not b358) (not b889) ) :assumption (or (not b362) (not b895) ) :assumption (or (not b366) (not b901) ) :assumption (or (not b369) (not b907) ) :assumption (or (not b300) (not b901) ) :assumption (or (not b303) (not b907) ) :assumption (or (not b231) (not b889) ) :assumption (or (not b235) (not b895) ) :assumption (or (not b239) (not b901) ) :assumption (or (not b167) (not b889) ) :assumption (or (not b172) (not b895) ) :assumption (or (not b176) (not b901) ) :assumption (or (not b179) (not b907) ) :assumption (or (not b105) (not b895) ) :assumption (or (not b109) (not b901) ) :assumption (or (not b113) (not b907) ) :assumption (or (not b889) (not b1264) ) :assumption (or (not b895) (not b1267) ) :assumption (or (not b901) (not b1270) ) :assumption (or (not b907) (not b1273) ) :assumption (or (not b889) (not b1137) ) :assumption (or (not b895) (not b1143) ) :assumption (or (not b901) (not b1149) ) :assumption (or (not b907) (not b1155) ) :assumption (or (not b913) (not b1280) ) :assumption (or (not b918) (not b1281) ) :assumption (or (not b923) (not b1282) ) :assumption (or (not b913) (not b1222) ) :assumption (or (not b918) (not b1227) ) :assumption (or (not b923) (not b1232) ) :assumption (or (not b913) (not b1205) ) :assumption (or (not b918) (not b1210) ) :assumption (or (not b923) (not b1215) ) :assumption (or (not b913) (not b930) ) :assumption (or (not b918) (not b935) ) :assumption (or (not b923) (not b940) ) :assumption (or (not b651) (not b918) ) :assumption (or (not b654) (not b923) ) :assumption (or (not b597) (not b918) ) :assumption (or (not b600) (not b923) ) :assumption (or (not b543) (not b918) ) :assumption (or (not b546) (not b923) ) :assumption (or (not b489) (not b918) ) :assumption (or (not b492) (not b923) ) :assumption (or (not b432) (not b913) ) :assumption (or (not b435) (not b918) ) :assumption (or (not b438) (not b923) ) :assumption (or (not b358) (not b913) ) :assumption (or (not b362) (not b918) ) :assumption (or (not b366) (not b923) ) :assumption (or (not b300) (not b923) ) :assumption (or (not b231) (not b913) ) :assumption (or (not b235) (not b918) ) :assumption (or (not b239) (not b923) ) :assumption (or (not b167) (not b913) ) :assumption (or (not b172) (not b918) ) :assumption (or (not b176) (not b923) ) :assumption (or (not b105) (not b918) ) :assumption (or (not b109) (not b923) ) :assumption (or (not b913) (not b1181) ) :assumption (or (not b918) (not b1187) ) :assumption (or (not b923) (not b1193) ) :assumption (or (not b913) (not b1137) ) :assumption (or (not b918) (not b1143) ) :assumption (or (not b923) (not b1149) ) :assumption (or (not b913) (not b1264) ) :assumption (or (not b918) (not b1267) ) :assumption (or (not b923) (not b1270) ) :assumption (or (not b913) (not b1103) ) :assumption (or (not b918) (not b1110) ) :assumption (or (not b923) (not b1117) ) :assumption (or (not b633) (not b918) ) :assumption (or (not b636) (not b923) ) :assumption (or (not b579) (not b918) ) :assumption (or (not b582) (not b923) ) :assumption (or (not b525) (not b918) ) :assumption (or (not b528) (not b923) ) :assumption (or (not b471) (not b918) ) :assumption (or (not b474) (not b923) ) :assumption (or (not b408) (not b913) ) :assumption (or (not b411) (not b918) ) :assumption (or (not b414) (not b923) ) :assumption (or (not b344) (not b923) ) :assumption (or (not b279) (not b923) ) :assumption (or (not b217) (not b923) ) :assumption (or (not b154) (not b923) ) :assumption (or (not b76) (not b913) ) :assumption (or (not b81) (not b918) ) :assumption (or (not b86) (not b923) ) :assumption (or (not b913) (not b1276) ) :assumption (or (not b918) (not b1277) ) :assumption (or (not b923) (not b1278) ) :assumption (or (not b913) (not b1161) ) :assumption (or (not b918) (not b1166) ) :assumption (or (not b923) (not b1171) ) :assumption (or (not b930) (not b1280) ) :assumption (or (not b935) (not b1281) ) :assumption (or (not b940) (not b1282) ) :assumption (or (not b930) (not b1222) ) :assumption (or (not b935) (not b1227) ) :assumption (or (not b940) (not b1232) ) :assumption (or (not b930) (not b1205) ) :assumption (or (not b935) (not b1210) ) :assumption (or (not b940) (not b1215) ) :assumption (or (not b651) (not b935) ) :assumption (or (not b654) (not b940) ) :assumption (or (not b597) (not b935) ) :assumption (or (not b600) (not b940) ) :assumption (or (not b543) (not b935) ) :assumption (or (not b546) (not b940) ) :assumption (or (not b489) (not b935) ) :assumption (or (not b492) (not b940) ) :assumption (or (not b432) (not b930) ) :assumption (or (not b435) (not b935) ) :assumption (or (not b438) (not b940) ) :assumption (or (not b358) (not b930) ) :assumption (or (not b362) (not b935) ) :assumption (or (not b366) (not b940) ) :assumption (or (not b300) (not b940) ) :assumption (or (not b231) (not b930) ) :assumption (or (not b235) (not b935) ) :assumption (or (not b239) (not b940) ) :assumption (or (not b167) (not b930) ) :assumption (or (not b172) (not b935) ) :assumption (or (not b176) (not b940) ) :assumption (or (not b105) (not b935) ) :assumption (or (not b109) (not b940) ) :assumption (or (not b930) (not b1181) ) :assumption (or (not b935) (not b1187) ) :assumption (or (not b940) (not b1193) ) :assumption (or (not b930) (not b1137) ) :assumption (or (not b935) (not b1143) ) :assumption (or (not b940) (not b1149) ) :assumption (or (not b930) (not b1276) ) :assumption (or (not b935) (not b1277) ) :assumption (or (not b940) (not b1278) ) :assumption (or (not b930) (not b1161) ) :assumption (or (not b935) (not b1166) ) :assumption (or (not b940) (not b1171) ) :assumption (or (not b642) (not b935) ) :assumption (or (not b645) (not b940) ) :assumption (or (not b588) (not b935) ) :assumption (or (not b591) (not b940) ) :assumption (or (not b534) (not b935) ) :assumption (or (not b537) (not b940) ) :assumption (or (not b480) (not b935) ) :assumption (or (not b483) (not b940) ) :assumption (or (not b420) (not b930) ) :assumption (or (not b423) (not b935) ) :assumption (or (not b426) (not b940) ) :assumption (or (not b352) (not b940) ) :assumption (or (not b285) (not b930) ) :assumption (or (not b290) (not b935) ) :assumption (or (not b294) (not b940) ) :assumption (or (not b225) (not b940) ) :assumption (or (not b163) (not b940) ) :assumption (or (not b93) (not b935) ) :assumption (or (not b97) (not b940) ) :assumption (or (not b930) (not b1264) ) :assumption (or (not b935) (not b1267) ) :assumption (or (not b940) (not b1270) ) :assumption (or (not b930) (not b1103) ) :assumption (or (not b935) (not b1110) ) :assumption (or (not b940) (not b1117) ) :assumption (or (not b947) (not b1238) ) :assumption (or (not b954) (not b1241) ) :assumption (or (not b961) (not b1244) ) :assumption (or (not b968) (not b1247) ) :assumption (or (not b975) (not b1250) ) :assumption (or (not b947) (not b982) ) :assumption (or (not b954) (not b988) ) :assumption (or (not b961) (not b994) ) :assumption (or (not b968) (not b1000) ) :assumption (or (not b975) (not b1006) ) :assumption (or (not b954) (not b1056) ) :assumption (or (not b961) (not b1061) ) :assumption (or (not b968) (not b1066) ) :assumption (or (not b975) (not b1071) ) :assumption (or (not b954) (not b1012) ) :assumption (or (not b961) (not b1017) ) :assumption (or (not b968) (not b1022) ) :assumption (or (not b975) (not b1027) ) :assumption (or (not b954) (not b1253) ) :assumption (or (not b961) (not b1254) ) :assumption (or (not b968) (not b1255) ) :assumption (or (not b975) (not b1256) ) :assumption (or (not b954) (not b1032) ) :assumption (or (not b961) (not b1038) ) :assumption (or (not b968) (not b1044) ) :assumption (or (not b975) (not b1050) ) :assumption (or (not b954) (not b1257) ) :assumption (or (not b961) (not b1258) ) :assumption (or (not b968) (not b1259) ) :assumption (or (not b975) (not b1260) ) :assumption (or (not b954) (not b1076) ) :assumption (or (not b961) (not b1081) ) :assumption (or (not b968) (not b1086) ) :assumption (or (not b975) (not b1091) ) :assumption (or (not b982) (not b1238) ) :assumption (or (not b988) (not b1241) ) :assumption (or (not b994) (not b1244) ) :assumption (or (not b1000) (not b1247) ) :assumption (or (not b1006) (not b1250) ) :assumption (or (not b988) (not b1056) ) :assumption (or (not b994) (not b1061) ) :assumption (or (not b1000) (not b1066) ) :assumption (or (not b1006) (not b1071) ) :assumption (or (not b988) (not b1012) ) :assumption (or (not b994) (not b1017) ) :assumption (or (not b1000) (not b1022) ) :assumption (or (not b1006) (not b1027) ) :assumption (or (not b988) (not b1257) ) :assumption (or (not b994) (not b1258) ) :assumption (or (not b1000) (not b1259) ) :assumption (or (not b1006) (not b1260) ) :assumption (or (not b988) (not b1076) ) :assumption (or (not b994) (not b1081) ) :assumption (or (not b1000) (not b1086) ) :assumption (or (not b1006) (not b1091) ) :assumption (or (not b988) (not b1253) ) :assumption (or (not b994) (not b1254) ) :assumption (or (not b1000) (not b1255) ) :assumption (or (not b1006) (not b1256) ) :assumption (or (not b988) (not b1032) ) :assumption (or (not b994) (not b1038) ) :assumption (or (not b1000) (not b1044) ) :assumption (or (not b1006) (not b1050) ) :assumption (or (not b1012) (not b1253) ) :assumption (or (not b1017) (not b1254) ) :assumption (or (not b1022) (not b1255) ) :assumption (or (not b1027) (not b1256) ) :assumption (or (not b1012) (not b1032) ) :assumption (or (not b1017) (not b1038) ) :assumption (or (not b1022) (not b1044) ) :assumption (or (not b1027) (not b1050) ) :assumption (or (not b1012) (not b1076) ) :assumption (or (not b1017) (not b1081) ) :assumption (or (not b1022) (not b1086) ) :assumption (or (not b1027) (not b1091) ) :assumption (or (not b1012) (not b1241) ) :assumption (or (not b1017) (not b1244) ) :assumption (or (not b1022) (not b1247) ) :assumption (or (not b1027) (not b1250) ) :assumption (or (not b1012) (not b1257) ) :assumption (or (not b1017) (not b1258) ) :assumption (or (not b1022) (not b1259) ) :assumption (or (not b1027) (not b1260) ) :assumption (or (not b1012) (not b1056) ) :assumption (or (not b1017) (not b1061) ) :assumption (or (not b1022) (not b1066) ) :assumption (or (not b1027) (not b1071) ) :assumption (or (not b1032) (not b1253) ) :assumption (or (not b1038) (not b1254) ) :assumption (or (not b1044) (not b1255) ) :assumption (or (not b1050) (not b1256) ) :assumption (or (not b1032) (not b1076) ) :assumption (or (not b1038) (not b1081) ) :assumption (or (not b1044) (not b1086) ) :assumption (or (not b1050) (not b1091) ) :assumption (or (not b1032) (not b1257) ) :assumption (or (not b1038) (not b1258) ) :assumption (or (not b1044) (not b1259) ) :assumption (or (not b1050) (not b1260) ) :assumption (or (not b1032) (not b1056) ) :assumption (or (not b1038) (not b1061) ) :assumption (or (not b1044) (not b1066) ) :assumption (or (not b1050) (not b1071) ) :assumption (or (not b1032) (not b1241) ) :assumption (or (not b1038) (not b1244) ) :assumption (or (not b1044) (not b1247) ) :assumption (or (not b1050) (not b1250) ) :assumption (or (not b1056) (not b1257) ) :assumption (or (not b1061) (not b1258) ) :assumption (or (not b1066) (not b1259) ) :assumption (or (not b1071) (not b1260) ) :assumption (or (not b1056) (not b1076) ) :assumption (or (not b1061) (not b1081) ) :assumption (or (not b1066) (not b1086) ) :assumption (or (not b1071) (not b1091) ) :assumption (or (not b1056) (not b1241) ) :assumption (or (not b1061) (not b1244) ) :assumption (or (not b1066) (not b1247) ) :assumption (or (not b1071) (not b1250) ) :assumption (or (not b1056) (not b1253) ) :assumption (or (not b1061) (not b1254) ) :assumption (or (not b1066) (not b1255) ) :assumption (or (not b1071) (not b1256) ) :assumption (or (not b1076) (not b1257) ) :assumption (or (not b1081) (not b1258) ) :assumption (or (not b1086) (not b1259) ) :assumption (or (not b1091) (not b1260) ) :assumption (or (not b1076) (not b1253) ) :assumption (or (not b1081) (not b1254) ) :assumption (or (not b1086) (not b1255) ) :assumption (or (not b1091) (not b1256) ) :assumption (or (not b1076) (not b1241) ) :assumption (or (not b1081) (not b1244) ) :assumption (or (not b1086) (not b1247) ) :assumption (or (not b1091) (not b1250) ) :assumption (or (not b1096) (not b1261) ) :assumption (or (not b1103) (not b1264) ) :assumption (or (not b1110) (not b1267) ) :assumption (or (not b1117) (not b1270) ) :assumption (or (not b1124) (not b1273) ) :assumption (or (not b1096) (not b1131) ) :assumption (or (not b1103) (not b1137) ) :assumption (or (not b1110) (not b1143) ) :assumption (or (not b1117) (not b1149) ) :assumption (or (not b1124) (not b1155) ) :assumption (or (not b1103) (not b1205) ) :assumption (or (not b1110) (not b1210) ) :assumption (or (not b1117) (not b1215) ) :assumption (or (not b1103) (not b1161) ) :assumption (or (not b1110) (not b1166) ) :assumption (or (not b1117) (not b1171) ) :assumption (or (not b1124) (not b1176) ) :assumption (or (not b1103) (not b1276) ) :assumption (or (not b1110) (not b1277) ) :assumption (or (not b1117) (not b1278) ) :assumption (or (not b1124) (not b1279) ) :assumption (or (not b1103) (not b1181) ) :assumption (or (not b1110) (not b1187) ) :assumption (or (not b1117) (not b1193) ) :assumption (or (not b1124) (not b1199) ) :assumption (or (not b1103) (not b1280) ) :assumption (or (not b1110) (not b1281) ) :assumption (or (not b1117) (not b1282) ) :assumption (or (not b1124) (not b1283) ) :assumption (or (not b1103) (not b1222) ) :assumption (or (not b1110) (not b1227) ) :assumption (or (not b1117) (not b1232) ) :assumption (or (not b1131) (not b1261) ) :assumption (or (not b1137) (not b1264) ) :assumption (or (not b1143) (not b1267) ) :assumption (or (not b1149) (not b1270) ) :assumption (or (not b1155) (not b1273) ) :assumption (or (not b1137) (not b1205) ) :assumption (or (not b1143) (not b1210) ) :assumption (or (not b1149) (not b1215) ) :assumption (or (not b1137) (not b1161) ) :assumption (or (not b1143) (not b1166) ) :assumption (or (not b1149) (not b1171) ) :assumption (or (not b1155) (not b1176) ) :assumption (or (not b1137) (not b1280) ) :assumption (or (not b1143) (not b1281) ) :assumption (or (not b1149) (not b1282) ) :assumption (or (not b1155) (not b1283) ) :assumption (or (not b1137) (not b1222) ) :assumption (or (not b1143) (not b1227) ) :assumption (or (not b1149) (not b1232) ) :assumption (or (not b1137) (not b1276) ) :assumption (or (not b1143) (not b1277) ) :assumption (or (not b1149) (not b1278) ) :assumption (or (not b1155) (not b1279) ) :assumption (or (not b1137) (not b1181) ) :assumption (or (not b1143) (not b1187) ) :assumption (or (not b1149) (not b1193) ) :assumption (or (not b1155) (not b1199) ) :assumption (or (not b1161) (not b1276) ) :assumption (or (not b1166) (not b1277) ) :assumption (or (not b1171) (not b1278) ) :assumption (or (not b1176) (not b1279) ) :assumption (or (not b1161) (not b1181) ) :assumption (or (not b1166) (not b1187) ) :assumption (or (not b1171) (not b1193) ) :assumption (or (not b1176) (not b1199) ) :assumption (or (not b1161) (not b1222) ) :assumption (or (not b1166) (not b1227) ) :assumption (or (not b1171) (not b1232) ) :assumption (or (not b1161) (not b1264) ) :assumption (or (not b1166) (not b1267) ) :assumption (or (not b1171) (not b1270) ) :assumption (or (not b1176) (not b1273) ) :assumption (or (not b1161) (not b1280) ) :assumption (or (not b1166) (not b1281) ) :assumption (or (not b1171) (not b1282) ) :assumption (or (not b1176) (not b1283) ) :assumption (or (not b1161) (not b1205) ) :assumption (or (not b1166) (not b1210) ) :assumption (or (not b1171) (not b1215) ) :assumption (or (not b1181) (not b1276) ) :assumption (or (not b1187) (not b1277) ) :assumption (or (not b1193) (not b1278) ) :assumption (or (not b1199) (not b1279) ) :assumption (or (not b1181) (not b1222) ) :assumption (or (not b1187) (not b1227) ) :assumption (or (not b1193) (not b1232) ) :assumption (or (not b1181) (not b1280) ) :assumption (or (not b1187) (not b1281) ) :assumption (or (not b1193) (not b1282) ) :assumption (or (not b1199) (not b1283) ) :assumption (or (not b1181) (not b1205) ) :assumption (or (not b1187) (not b1210) ) :assumption (or (not b1193) (not b1215) ) :assumption (or (not b1181) (not b1264) ) :assumption (or (not b1187) (not b1267) ) :assumption (or (not b1193) (not b1270) ) :assumption (or (not b1199) (not b1273) ) :assumption (or (not b1205) (not b1280) ) :assumption (or (not b1210) (not b1281) ) :assumption (or (not b1215) (not b1282) ) :assumption (or (not b1205) (not b1222) ) :assumption (or (not b1210) (not b1227) ) :assumption (or (not b1215) (not b1232) ) :assumption (or (not b1205) (not b1264) ) :assumption (or (not b1210) (not b1267) ) :assumption (or (not b1215) (not b1270) ) :assumption (or (not b1205) (not b1276) ) :assumption (or (not b1210) (not b1277) ) :assumption (or (not b1215) (not b1278) ) :assumption (or (not b1222) (not b1280) ) :assumption (or (not b1227) (not b1281) ) :assumption (or (not b1232) (not b1282) ) :assumption (or (not b1222) (not b1276) ) :assumption (or (not b1227) (not b1277) ) :assumption (or (not b1232) (not b1278) ) :assumption (or (not b1222) (not b1264) ) :assumption (or (not b1227) (not b1267) ) :assumption (or (not b1232) (not b1270) ) :assumption (or (not b1241) (not b1257) ) :assumption (or (not b1244) (not b1258) ) :assumption (or (not b1247) (not b1259) ) :assumption (or (not b1250) (not b1260) ) :assumption (or (not b1241) (not b1253) ) :assumption (or (not b1244) (not b1254) ) :assumption (or (not b1247) (not b1255) ) :assumption (or (not b1250) (not b1256) ) :assumption (or (not b1253) (not b1257) ) :assumption (or (not b1254) (not b1258) ) :assumption (or (not b1255) (not b1259) ) :assumption (or (not b1256) (not b1260) ) :assumption (or (not b1264) (not b1280) ) :assumption (or (not b1267) (not b1281) ) :assumption (or (not b1270) (not b1282) ) :assumption (or (not b1273) (not b1283) ) :assumption (or (not b1264) (not b1276) ) :assumption (or (not b1267) (not b1277) ) :assumption (or (not b1270) (not b1278) ) :assumption (or (not b1273) (not b1279) ) :assumption (or (not b1276) (not b1280) ) :assumption (or (not b1277) (not b1281) ) :assumption (or (not b1278) (not b1282) ) :assumption (or (not b1279) (not b1283) ) :assumption (= r1 0) :assumption (= r2 r3) :assumption (= (- r4 r1) 1) :assumption (= (- r5 r4) 1) :assumption (= (- r6 r5) 1) :assumption (= (- r7 r6) 1) :assumption (= (- r3 r7) 1) :assumption (= r8 0) :assumption (= r9 0) :assumption (= r10 973) :assumption (= r11 0) :assumption (= r12 1048) :assumption (<= (+ (* 4 r2) (* 3 r13)) 19964) :assumption (= r18 0) :assumption (= r29 0) :assumption (= r39 0) :assumption (= r47 0) :assumption (= r59 0) :assumption (= r67 0) :assumption (= r69 0) :assumption (= r77 0) :assumption (= r298 0) :assumption (= r299 0) :assumption (= r306 0) :assumption (= r307 0) :assumption (= r410 0) :assumption (= r411 0) :assumption (= r418 0) :assumption (= r419 0) :assumption (= (- (- r312 r9) r14) 0) :assumption (= (- (- (- (- (- (- (- (- (- r315 r312) r108) r104) r100) r88) r70) r56) r40) r15) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r318 r315) r184) r181) r178) r166) r163) r160) r148) r145) r142) r130) r127) r124) r109) r105) r101) r89) r71) r57) r41) r22) r19) r16) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r321 r318) r185) r182) r179) r167) r164) r161) r149) r146) r143) r131) r128) r125) r110) r106) r102) r90) r86) r84) r74) r72) r68) r58) r54) r52) r42) r38) r36) r23) r20) r17) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r423 r321) r186) r183) r180) r168) r165) r162) r150) r147) r144) r132) r129) r126) r111) r107) r103) r91) r87) r85) r75) r73) r69) r59) r55) r53) r43) r39) r37) r24) r21) r18) 0) :assumption (= (- (- r368 r11) r25) 0) :assumption (= (- (- (- (- (- (- (- (- (- r371 r368) r120) r116) r112) r96) r78) r64) r48) r26) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r374 r371) r193) r190) r187) r175) r172) r169) r157) r154) r151) r139) r136) r133) r121) r117) r113) r97) r79) r65) r49) r33) r30) r27) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r377 r374) r194) r191) r188) r176) r173) r170) r158) r155) r152) r140) r137) r134) r122) r118) r114) r98) r94) r92) r82) r80) r76) r66) r62) r60) r50) r46) r44) r34) r31) r28) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r424 r377) r195) r192) r189) r177) r174) r171) r159) r156) r153) r141) r138) r135) r123) r119) r115) r99) r95) r93) r83) r81) r77) r67) r63) r61) r51) r47) r45) r35) r32) r29) 0) :assumption (= (- (- (- (- (- (- (- (- (- r425 r8) r378) r364) r322) r308) r266) r252) r210) r196) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r426 r425) r412) r404) r396) r388) r380) r366) r356) r348) r340) r332) r324) r310) r300) r292) r284) r276) r268) r254) r244) r236) r228) r220) r212) r198) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r427 r426) r414) r406) r398) r390) r382) r369) r358) r350) r342) r334) r326) r313) r302) r294) r286) r278) r270) r257) r246) r238) r230) r222) r214) r201) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r428 r427) r416) r408) r400) r392) r384) r372) r360) r352) r344) r336) r328) r316) r304) r296) r288) r280) r272) r260) r248) r240) r232) r224) r216) r204) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r13 r428) r418) r410) r402) r394) r386) r375) r362) r354) r346) r338) r330) r319) r306) r298) r290) r282) r274) r263) r250) r242) r234) r226) r218) r207) 0) :formula (not false) )