(benchmark p3_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 sat :category { industrial } :difficulty { 0 } :logic QF_LRA :extrapreds ((b15)) :extrapreds ((b22)) :extrapreds ((b28)) :extrapreds ((b34)) :extrapreds ((b40)) :extrapreds ((b46)) :extrapreds ((b52)) :extrapreds ((b57)) :extrapreds ((b62)) :extrapreds ((b67)) :extrapreds ((b72)) :extrapreds ((b77)) :extrapreds ((b82)) :extrapreds ((b86)) :extrapreds ((b90)) :extrapreds ((b96)) :extrapreds ((b101)) :extrapreds ((b106)) :extrapreds ((b111)) :extrapreds ((b115)) :extrapreds ((b120)) :extrapreds ((b126)) :extrapreds ((b130)) :extrapreds ((b134)) :extrapreds ((b138)) :extrapreds ((b142)) :extrapreds ((b145)) :extrapreds ((b149)) :extrapreds ((b153)) :extrapreds ((b160)) :extrapreds ((b165)) :extrapreds ((b170)) :extrapreds ((b175)) :extrapreds ((b179)) :extrapreds ((b183)) :extrapreds ((b190)) :extrapreds ((b195)) :extrapreds ((b200)) :extrapreds ((b205)) :extrapreds ((b209)) :extrapreds ((b213)) :extrapreds ((b216)) :extrapreds ((b219)) :extrapreds ((b222)) :extrapreds ((b226)) :extrapreds ((b231)) :extrapreds ((b235)) :extrapreds ((b239)) :extrapreds ((b245)) :extrapreds ((b250)) :extrapreds ((b255)) :extrapreds ((b260)) :extrapreds ((b265)) :extrapreds ((b271)) :extrapreds ((b275)) :extrapreds ((b279)) :extrapreds ((b283)) :extrapreds ((b287)) :extrapreds ((b291)) :extrapreds ((b295)) :extrapreds ((b298)) :extrapreds ((b302)) :extrapreds ((b306)) :extrapreds ((b310)) :extrapreds ((b313)) :extrapreds ((b316)) :extrapreds ((b319)) :extrapreds ((b322)) :extrapreds ((b325)) :extrapreds ((b328)) :extrapreds ((b331)) :extrapreds ((b334)) :extrapreds ((b337)) :extrapreds ((b340)) :extrapreds ((b343)) :extrapreds ((b346)) :extrapreds ((b349)) :extrapreds ((b352)) :extrapreds ((b355)) :extrapreds ((b358)) :extrapreds ((b361)) :extrapreds ((b364)) :extrapreds ((b367)) :extrapreds ((b370)) :extrapreds ((b373)) :extrapreds ((b376)) :extrapreds ((b379)) :extrapreds ((b382)) :extrapreds ((b385)) :extrapreds ((b388)) :extrapreds ((b391)) :extrapreds ((b394)) :extrapreds ((b397)) :extrapreds ((b400)) :extrapreds ((b403)) :extrapreds ((b406)) :extrapreds ((b409)) :extrapreds ((b412)) :extrapreds ((b415)) :extrapreds ((b418)) :extrapreds ((b421)) :extrapreds ((b424)) :extrapreds ((b427)) :extrapreds ((b430)) :extrapreds ((b433)) :extrapreds ((b436)) :extrapreds ((b439)) :extrapreds ((b442)) :extrapreds ((b445)) :extrapreds ((b448)) :extrapreds ((b451)) :extrapreds ((b454)) :extrapreds ((b458)) :extrapreds ((b461)) :extrapreds ((b464)) :extrapreds ((b467)) :extrapreds ((b470)) :extrapreds ((b473)) :extrapreds ((b476)) :extrapreds ((b479)) :extrapreds ((b482)) :extrapreds ((b485)) :extrapreds ((b488)) :extrapreds ((b491)) :extrapreds ((b494)) :extrapreds ((b497)) :extrapreds ((b500)) :extrapreds ((b503)) :extrapreds ((b506)) :extrapreds ((b509)) :extrapreds ((b512)) :extrapreds ((b515)) :extrapreds ((b518)) :extrapreds ((b521)) :extrapreds ((b524)) :extrapreds ((b527)) :extrapreds ((b530)) :extrapreds ((b533)) :extrapreds ((b536)) :extrapreds ((b539)) :extrapreds ((b542)) :extrapreds ((b545)) :extrapreds ((b548)) :extrapreds ((b551)) :extrapreds ((b554)) :extrapreds ((b561)) :extrapreds ((b567)) :extrapreds ((b573)) :extrapreds ((b582)) :extrapreds ((b588)) :extrapreds ((b594)) :extrapreds ((b600)) :extrapreds ((b609)) :extrapreds ((b614)) :extrapreds ((b619)) :extrapreds ((b624)) :extrapreds ((b630)) :extrapreds ((b636)) :extrapreds ((b642)) :extrapreds ((b648)) :extrapreds ((b654)) :extrapreds ((b659)) :extrapreds ((b664)) :extrapreds ((b669)) :extrapreds ((b675)) :extrapreds ((b680)) :extrapreds ((b685)) :extrapreds ((b690)) :extrapreds ((b695)) :extrapreds ((b701)) :extrapreds ((b707)) :extrapreds ((b713)) :extrapreds ((b721)) :extrapreds ((b727)) :extrapreds ((b733)) :extrapreds ((b739)) :extrapreds ((b746)) :extrapreds ((b751)) :extrapreds ((b756)) :extrapreds ((b761)) :extrapreds ((b766)) :extrapreds ((b772)) :extrapreds ((b778)) :extrapreds ((b784)) :extrapreds ((b790)) :extrapreds ((b796)) :extrapreds ((b801)) :extrapreds ((b806)) :extrapreds ((b811)) :extrapreds ((b816)) :extrapreds ((b822)) :extrapreds ((b827)) :extrapreds ((b832)) :extrapreds ((b837)) :extrapreds ((b842)) :extrapreds ((b849)) :extrapreds ((b856)) :extrapreds ((b863)) :extrapreds ((b872)) :extrapreds ((b878)) :extrapreds ((b884)) :extrapreds ((b890)) :extrapreds ((b898)) :extrapreds ((b903)) :extrapreds ((b908)) :extrapreds ((b913)) :extrapreds ((b920)) :extrapreds ((b926)) :extrapreds ((b932)) :extrapreds ((b938)) :extrapreds ((b944)) :extrapreds ((b949)) :extrapreds ((b954)) :extrapreds ((b959)) :extrapreds ((b965)) :extrapreds ((b970)) :extrapreds ((b975)) :extrapreds ((b980)) :extrapreds ((b985)) :extrapreds ((b992)) :extrapreds ((b999)) :extrapreds ((b1006)) :extrapreds ((b1013)) :extrapreds ((b1019)) :extrapreds ((b1025)) :extrapreds ((b1031)) :extrapreds ((b1037)) :extrapreds ((b1042)) :extrapreds ((b1047)) :extrapreds ((b1052)) :extrapreds ((b1057)) :extrapreds ((b1063)) :extrapreds ((b1069)) :extrapreds ((b1075)) :extrapreds ((b1081)) :extrapreds ((b1088)) :extrapreds ((b1093)) :extrapreds ((b1098)) :extrapreds ((b1103)) :extrapreds ((b1108)) :extrapreds ((b1114)) :extrapreds ((b1119)) :extrapreds ((b1124)) :extrapreds ((b1129)) :extrapreds ((b1133)) :extrapreds ((b1136)) :extrapreds ((b1139)) :extrapreds ((b1142)) :extrapreds ((b1145)) :extrapreds ((b1148)) :extrapreds ((b1149)) :extrapreds ((b1150)) :extrapreds ((b1151)) :extrapreds ((b1152)) :extrapreds ((b1153)) :extrapreds ((b1154)) :extrapreds ((b1155)) :extrapreds ((b1156)) :extrapreds ((b1159)) :extrapreds ((b1162)) :extrapreds ((b1165)) :extrapreds ((b1168)) :extrapreds ((b1169)) :extrapreds ((b1170)) :extrapreds ((b1171)) :extrapreds ((b1172)) :extrapreds ((b1175)) :extrapreds ((b1176)) :extrapreds ((b1177)) :extrapreds ((b1178)) :extrapreds ((b17)) :extrapreds ((b18)) :extrapreds ((b19)) :extrapreds ((b20)) :extrapreds ((b24)) :extrapreds ((b25)) :extrapreds ((b26)) :extrapreds ((b30)) :extrapreds ((b31)) :extrapreds ((b32)) :extrapreds ((b36)) :extrapreds ((b37)) :extrapreds ((b38)) :extrapreds ((b42)) :extrapreds ((b43)) :extrapreds ((b48)) :extrapreds ((b49)) :extrapreds ((b50)) :extrapreds ((b54)) :extrapreds ((b55)) :extrapreds ((b59)) :extrapreds ((b60)) :extrapreds ((b64)) :extrapreds ((b65)) :extrapreds ((b69)) :extrapreds ((b70)) :extrapreds ((b74)) :extrapreds ((b75)) :extrapreds ((b79)) :extrapreds ((b84)) :extrapreds ((b88)) :extrapreds ((b92)) :extrapreds ((b93)) :extrapreds ((b94)) :extrapreds ((b98)) :extrapreds ((b99)) :extrapreds ((b103)) :extrapreds ((b104)) :extrapreds ((b108)) :extrapreds ((b109)) :extrapreds ((b113)) :extrapreds ((b117)) :extrapreds ((b118)) :extrapreds ((b122)) :extrapreds ((b123)) :extrapreds ((b128)) :extrapreds ((b132)) :extrapreds ((b136)) :extrapreds ((b140)) :extrapreds ((b147)) :extrapreds ((b155)) :extrapreds ((b156)) :extrapreds ((b157)) :extrapreds ((b158)) :extrapreds ((b162)) :extrapreds ((b163)) :extrapreds ((b167)) :extrapreds ((b168)) :extrapreds ((b172)) :extrapreds ((b173)) :extrapreds ((b177)) :extrapreds ((b181)) :extrapreds ((b185)) :extrapreds ((b186)) :extrapreds ((b187)) :extrapreds ((b188)) :extrapreds ((b192)) :extrapreds ((b193)) :extrapreds ((b197)) :extrapreds ((b202)) :extrapreds ((b203)) :extrapreds ((b207)) :extrapreds ((b211)) :extrapreds ((b224)) :extrapreds ((b228)) :extrapreds ((b229)) :extrapreds ((b233)) :extrapreds ((b241)) :extrapreds ((b242)) :extrapreds ((b243)) :extrapreds ((b247)) :extrapreds ((b248)) :extrapreds ((b252)) :extrapreds ((b253)) :extrapreds ((b257)) :extrapreds ((b258)) :extrapreds ((b262)) :extrapreds ((b267)) :extrapreds ((b268)) :extrapreds ((b269)) :extrapreds ((b273)) :extrapreds ((b277)) :extrapreds ((b281)) :extrapreds ((b285)) :extrapreds ((b289)) :extrapreds ((b293)) :extrapreds ((b304)) :extrapreds ((b308)) :extrapreds ((b456)) :extrapreds ((b558)) :extrapreds ((b580)) :extrapreds ((b607)) :extrapreds ((b717)) :extrapreds ((b718)) :extrapreds ((b743)) :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)) :assumption (or (= r14 0) b15 ) :assumption (or (not b15) (= r14 1) ) :assumption (or (not b15) b17 ) :assumption (or (not b15) (not b18) ) :assumption (or (not b15) b19 ) :assumption (or (not b15) b20 ) :assumption (or (= r15 0) b22 ) :assumption (or (not b22) (= r15 1) ) :assumption (or (not b22) b24 ) :assumption (or (not b22) (not b25) ) :assumption (or b18 (not b22) ) :assumption (or (not b22) b26 ) :assumption (or (= r16 0) b28 ) :assumption (or (not b28) (= r16 1) ) :assumption (or (not b28) b30 ) :assumption (or (not b28) (not b31) ) :assumption (or (not b28) b32 ) :assumption (or (= r17 0) b34 ) :assumption (or (not b34) (= r17 1) ) :assumption (or (not b34) b36 ) :assumption (or (not b34) (not b37) ) :assumption (or b31 (not b34) ) :assumption (or (not b34) b38 ) :assumption (or (= r18 0) b40 ) :assumption (or (not b40) (= r18 1) ) :assumption (or b17 (not b40) ) :assumption (or (not b40) (not b42) ) :assumption (or b37 (not b40) ) :assumption (or (not b40) b43 ) :assumption (or (= r20 0) b46 ) :assumption (or (not b46) (= r20 1) ) :assumption (or b17 (not b46) ) :assumption (or (not b46) (not b48) ) :assumption (or (not b46) b49 ) :assumption (or (not b46) b50 ) :assumption (or (= r21 0) b52 ) :assumption (or (not b52) (= r21 1) ) :assumption (or b24 (not b52) ) :assumption (or (not b52) (not b54) ) :assumption (or b48 (not b52) ) :assumption (or (not b52) b55 ) :assumption (or (= r22 0) b57 ) :assumption (or (not b57) (= r22 1) ) :assumption (or (not b57) b59 ) :assumption (or (not b18) (not b57) ) :assumption (or b19 (not b57) ) :assumption (or (not b57) b60 ) :assumption (or (= r23 0) b62 ) :assumption (or (not b62) (= r23 1) ) :assumption (or (not b62) b64 ) :assumption (or (not b25) (not b62) ) :assumption (or b18 (not b62) ) :assumption (or (not b62) b65 ) :assumption (or (= r24 0) b67 ) :assumption (or (not b67) (= r24 1) ) :assumption (or (not b67) b69 ) :assumption (or (not b31) (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 b37) (not b72) ) :assumption (or b31 (not b72) ) :assumption (or (not b72) b75 ) :assumption (or (= r26 0) b77 ) :assumption (or (not b77) (= r26 1) ) :assumption (or b59 (not b77) ) :assumption (or (not b42) (not b77) ) :assumption (or b37 (not b77) ) :assumption (or (not b77) b79 ) :assumption (or (= r28 0) b82 ) :assumption (or (not b82) (= r28 1) ) :assumption (or b59 (not b82) ) :assumption (or (not b48) (not b82) ) :assumption (or b49 (not b82) ) :assumption (or (not b82) b84 ) :assumption (or (= r29 0) b86 ) :assumption (or (not b86) (= r29 1) ) :assumption (or b64 (not b86) ) :assumption (or (not b54) (not b86) ) :assumption (or b48 (not b86) ) :assumption (or (not b86) b88 ) :assumption (or (= r30 0) b90 ) :assumption (or (not b90) (= r30 1) ) :assumption (or (not b90) b92 ) :assumption (or (not b90) (not b93) ) :assumption (or (not b90) b94 ) :assumption (or b20 (not b90) ) :assumption (or (= r31 0) b96 ) :assumption (or (not b96) (= r31 1) ) :assumption (or (not b96) b98 ) :assumption (or (not b96) (not b99) ) :assumption (or b93 (not b96) ) :assumption (or b26 (not b96) ) :assumption (or (= r32 0) b101 ) :assumption (or (not b101) (= r32 1) ) :assumption (or (not b101) b103 ) :assumption (or (not b101) (not b104) ) :assumption (or b32 (not b101) ) :assumption (or (= r33 0) b106 ) :assumption (or (not b106) (= r33 1) ) :assumption (or (not b106) b108 ) :assumption (or (not b106) (not b109) ) :assumption (or b104 (not b106) ) :assumption (or b38 (not b106) ) :assumption (or (= r34 0) b111 ) :assumption (or (not b111) (= r34 1) ) :assumption (or b92 (not b111) ) :assumption (or (not b111) (not b113) ) :assumption (or b109 (not b111) ) :assumption (or b43 (not b111) ) :assumption (or (= r35 0) b115 ) :assumption (or (not b115) (= r35 1) ) :assumption (or b98 (not b115) ) :assumption (or (not b115) (not b117) ) :assumption (or b113 (not b115) ) :assumption (or (not b115) b118 ) :assumption (or (= r36 0) b120 ) :assumption (or (not b120) (= r36 1) ) :assumption (or b92 (not b120) ) :assumption (or (not b120) (not b122) ) :assumption (or (not b120) b123 ) :assumption (or b50 (not b120) ) :assumption (or (= r38 0) b126 ) :assumption (or (not b126) (= r38 1) ) :assumption (or (not b126) b128 ) :assumption (or (not b93) (not b126) ) :assumption (or b94 (not b126) ) :assumption (or b60 (not b126) ) :assumption (or (= r39 0) b130 ) :assumption (or (not b130) (= r39 1) ) :assumption (or (not b130) b132 ) :assumption (or (not b99) (not b130) ) :assumption (or b93 (not b130) ) :assumption (or b65 (not b130) ) :assumption (or (= r40 0) b134 ) :assumption (or (not b134) (= r40 1) ) :assumption (or (not b134) b136 ) :assumption (or (not b104) (not b134) ) :assumption (or b70 (not b134) ) :assumption (or (= r41 0) b138 ) :assumption (or (not b138) (= r41 1) ) :assumption (or (not b138) b140 ) :assumption (or (not b109) (not b138) ) :assumption (or b104 (not b138) ) :assumption (or b75 (not b138) ) :assumption (or (= r42 0) b142 ) :assumption (or (not b142) (= r42 1) ) :assumption (or b128 (not b142) ) :assumption (or (not b113) (not b142) ) :assumption (or b109 (not b142) ) :assumption (or b79 (not b142) ) :assumption (or (= r43 0) b145 ) :assumption (or (not b145) (= r43 1) ) :assumption (or b132 (not b145) ) :assumption (or (not b117) (not b145) ) :assumption (or b113 (not b145) ) :assumption (or (not b145) b147 ) :assumption (or (= r44 0) b149 ) :assumption (or (not b149) (= r44 1) ) :assumption (or b128 (not b149) ) :assumption (or (not b122) (not b149) ) :assumption (or b123 (not b149) ) :assumption (or b84 (not b149) ) :assumption (or (= r46 0) b153 ) :assumption (or (not b153) (= r46 1) ) :assumption (or (not b153) b155 ) :assumption (or (not b153) (not b156) ) :assumption (or (not b153) b157 ) :assumption (or (not b153) b158 ) :assumption (or (= r47 0) b160 ) :assumption (or (not b160) (= r47 1) ) :assumption (or (not b160) b162 ) :assumption (or (not b160) (not b163) ) :assumption (or b156 (not b160) ) :assumption (or b20 (not b160) ) :assumption (or (= r48 0) b165 ) :assumption (or (not b165) (= r48 1) ) :assumption (or (not b165) b167 ) :assumption (or (not b165) (not b168) ) :assumption (or b163 (not b165) ) :assumption (or b26 (not b165) ) :assumption (or (= r49 0) b170 ) :assumption (or (not b170) (= r49 1) ) :assumption (or b155 (not b170) ) :assumption (or (not b170) (not b172) ) :assumption (or (not b170) b173 ) :assumption (or b38 (not b170) ) :assumption (or (= r50 0) b175 ) :assumption (or (not b175) (= r50 1) ) :assumption (or b162 (not b175) ) :assumption (or (not b175) (not b177) ) :assumption (or b172 (not b175) ) :assumption (or b43 (not b175) ) :assumption (or (= r51 0) b179 ) :assumption (or (not b179) (= r51 1) ) :assumption (or b167 (not b179) ) :assumption (or (not b179) (not b181) ) :assumption (or b177 (not b179) ) :assumption (or b118 (not b179) ) :assumption (or (= r52 0) b183 ) :assumption (or (not b183) (= r52 1) ) :assumption (or (not b183) b185 ) :assumption (or (not b183) (not b186) ) :assumption (or (not b183) b187 ) :assumption (or (not b183) b188 ) :assumption (or (= r53 0) b190 ) :assumption (or (not b190) (= r53 1) ) :assumption (or b155 (not b190) ) :assumption (or (not b190) (not b192) ) :assumption (or b186 (not b190) ) :assumption (or (not b190) b193 ) :assumption (or (= r54 0) b195 ) :assumption (or (not b195) (= r54 1) ) :assumption (or b162 (not b195) ) :assumption (or (not b195) (not b197) ) :assumption (or b192 (not b195) ) :assumption (or b50 (not b195) ) :assumption (or (= r56 0) b200 ) :assumption (or (not b200) (= r56 1) ) :assumption (or (not b200) b202 ) :assumption (or (not b156) (not b200) ) :assumption (or b157 (not b200) ) :assumption (or (not b200) b203 ) :assumption (or (= r57 0) b205 ) :assumption (or (not b205) (= r57 1) ) :assumption (or (not b205) b207 ) :assumption (or (not b163) (not b205) ) :assumption (or b156 (not b205) ) :assumption (or b60 (not b205) ) :assumption (or (= r58 0) b209 ) :assumption (or (not b209) (= r58 1) ) :assumption (or (not b209) b211 ) :assumption (or (not b168) (not b209) ) :assumption (or b163 (not b209) ) :assumption (or b65 (not b209) ) :assumption (or (= r59 0) b213 ) :assumption (or (not b213) (= r59 1) ) :assumption (or b202 (not b213) ) :assumption (or (not b172) (not b213) ) :assumption (or b173 (not b213) ) :assumption (or b75 (not b213) ) :assumption (or (= r60 0) b216 ) :assumption (or (not b216) (= r60 1) ) :assumption (or b207 (not b216) ) :assumption (or (not b177) (not b216) ) :assumption (or b172 (not b216) ) :assumption (or b79 (not b216) ) :assumption (or (= r61 0) b219 ) :assumption (or (not b219) (= r61 1) ) :assumption (or b211 (not b219) ) :assumption (or (not b181) (not b219) ) :assumption (or b177 (not b219) ) :assumption (or b147 (not b219) ) :assumption (or (= r62 0) b222 ) :assumption (or (not b222) (= r62 1) ) :assumption (or (not b222) b224 ) :assumption (or (not b187) (not b222) ) :assumption (or (= r63 0) b226 ) :assumption (or (not b226) (= r63 1) ) :assumption (or (not b226) b228 ) :assumption (or (not b186) (not b226) ) :assumption (or b187 (not b226) ) :assumption (or (not b226) b229 ) :assumption (or (= r64 0) b231 ) :assumption (or (not b231) (= r64 1) ) :assumption (or b202 (not b231) ) :assumption (or (not b192) (not b231) ) :assumption (or b186 (not b231) ) :assumption (or (not b231) b233 ) :assumption (or (= r65 0) b235 ) :assumption (or (not b235) (= r65 1) ) :assumption (or b207 (not b235) ) :assumption (or (not b197) (not b235) ) :assumption (or b192 (not b235) ) :assumption (or b84 (not b235) ) :assumption (or (= r67 0) b239 ) :assumption (or (not b239) (= r67 1) ) :assumption (or (not b239) b241 ) :assumption (or (not b239) (not b242) ) :assumption (or (not b239) b243 ) :assumption (or b158 (not b239) ) :assumption (or (= r68 0) b245 ) :assumption (or (not b245) (= r68 1) ) :assumption (or (not b245) b247 ) :assumption (or (not b245) (not b248) ) :assumption (or b242 (not b245) ) :assumption (or b20 (not b245) ) :assumption (or (= r69 0) b250 ) :assumption (or (not b250) (= r69 1) ) :assumption (or (not b250) b252 ) :assumption (or (not b250) (not b253) ) :assumption (or b248 (not b250) ) :assumption (or b26 (not b250) ) :assumption (or (= r70 0) b255 ) :assumption (or (not b255) (= r70 1) ) :assumption (or b241 (not b255) ) :assumption (or (not b255) (not b257) ) :assumption (or (not b255) b258 ) :assumption (or b38 (not b255) ) :assumption (or (= r71 0) b260 ) :assumption (or (not b260) (= r71 1) ) :assumption (or b247 (not b260) ) :assumption (or (not b260) (not b262) ) :assumption (or b257 (not b260) ) :assumption (or b43 (not b260) ) :assumption (or (= r73 0) b265 ) :assumption (or (not b265) (= r73 1) ) :assumption (or (not b265) b267 ) :assumption (or (not b265) (not b268) ) :assumption (or (not b265) b269 ) :assumption (or b188 (not b265) ) :assumption (or (= r74 0) b271 ) :assumption (or (not b271) (= r74 1) ) :assumption (or b241 (not b271) ) :assumption (or (not b271) (not b273) ) :assumption (or b268 (not b271) ) :assumption (or b193 (not b271) ) :assumption (or (= r75 0) b275 ) :assumption (or (not b275) (= r75 1) ) :assumption (or b247 (not b275) ) :assumption (or (not b275) (not b277) ) :assumption (or b273 (not b275) ) :assumption (or b50 (not b275) ) :assumption (or (= r76 0) b279 ) :assumption (or (not b279) (= r76 1) ) :assumption (or b252 (not b279) ) :assumption (or (not b279) (not b281) ) :assumption (or b277 (not b279) ) :assumption (or b55 (not b279) ) :assumption (or (= r77 0) b283 ) :assumption (or (not b283) (= r77 1) ) :assumption (or (not b283) b285 ) :assumption (or (not b242) (not b283) ) :assumption (or b243 (not b283) ) :assumption (or b203 (not b283) ) :assumption (or (= r78 0) b287 ) :assumption (or (not b287) (= r78 1) ) :assumption (or (not b287) b289 ) :assumption (or (not b248) (not b287) ) :assumption (or b242 (not b287) ) :assumption (or b60 (not b287) ) :assumption (or (= r79 0) b291 ) :assumption (or (not b291) (= r79 1) ) :assumption (or (not b291) b293 ) :assumption (or (not b253) (not b291) ) :assumption (or b248 (not b291) ) :assumption (or b65 (not b291) ) :assumption (or (= r80 0) b295 ) :assumption (or (not b295) (= r80 1) ) :assumption (or b285 (not b295) ) :assumption (or (not b257) (not b295) ) :assumption (or b258 (not b295) ) :assumption (or b75 (not b295) ) :assumption (or (= r81 0) b298 ) :assumption (or (not b298) (= r81 1) ) :assumption (or b289 (not b298) ) :assumption (or (not b262) (not b298) ) :assumption (or b257 (not b298) ) :assumption (or b79 (not b298) ) :assumption (or (= r83 0) b302 ) :assumption (or (not b302) (= r83 1) ) :assumption (or (not b302) b304 ) :assumption (or (not b269) (not b302) ) :assumption (or (= r84 0) b306 ) :assumption (or (not b306) (= r84 1) ) :assumption (or (not b306) b308 ) :assumption (or (not b268) (not b306) ) :assumption (or b269 (not b306) ) :assumption (or b229 (not b306) ) :assumption (or (= r85 0) b310 ) :assumption (or (not b310) (= r85 1) ) :assumption (or b285 (not b310) ) :assumption (or (not b273) (not b310) ) :assumption (or b268 (not b310) ) :assumption (or b233 (not b310) ) :assumption (or (= r86 0) b313 ) :assumption (or (not b313) (= r86 1) ) :assumption (or b289 (not b313) ) :assumption (or (not b277) (not b313) ) :assumption (or b273 (not b313) ) :assumption (or b84 (not b313) ) :assumption (or (= r87 0) b316 ) :assumption (or (not b316) (= r87 1) ) :assumption (or b293 (not b316) ) :assumption (or (not b281) (not b316) ) :assumption (or b277 (not b316) ) :assumption (or b88 (not b316) ) :assumption (or (= r88 0) b319 ) :assumption (or (not b319) (= r88 (~ 1)) ) :assumption (or b19 (not b319) ) :assumption (or (not b36) (not b319) ) :assumption (or b30 (not b319) ) :assumption (or b158 (not b319) ) :assumption (or (= r89 0) b322 ) :assumption (or (not b322) (= r89 (~ 1)) ) :assumption (or b18 (not b322) ) :assumption (or (not b17) (not b322) ) :assumption (or b36 (not b322) ) :assumption (or b20 (not b322) ) :assumption (or (= r90 0) b325 ) :assumption (or (not b325) (= r90 (~ 1)) ) :assumption (or b25 (not b325) ) :assumption (or (not b24) (not b325) ) :assumption (or b17 (not b325) ) :assumption (or b26 (not b325) ) :assumption (or (= r91 0) b328 ) :assumption (or (not b328) (= r91 (~ 1)) ) :assumption (or b37 (not b328) ) :assumption (or (not b36) (not b328) ) :assumption (or b30 (not b328) ) :assumption (or b38 (not b328) ) :assumption (or (= r92 0) b331 ) :assumption (or (not b331) (= r92 (~ 1)) ) :assumption (or b42 (not b331) ) :assumption (or (not b17) (not b331) ) :assumption (or b36 (not b331) ) :assumption (or b43 (not b331) ) :assumption (or (= r93 0) b334 ) :assumption (or (not b334) (= r93 (~ 1)) ) :assumption (or (not b24) (not b334) ) :assumption (or b17 (not b334) ) :assumption (or b118 (not b334) ) :assumption (or (= r94 0) b337 ) :assumption (or (not b337) (= r94 (~ 1)) ) :assumption (or b49 (not b337) ) :assumption (or (not b36) (not b337) ) :assumption (or b30 (not b337) ) :assumption (or b193 (not b337) ) :assumption (or (= r95 0) b340 ) :assumption (or (not b340) (= r95 (~ 1)) ) :assumption (or b48 (not b340) ) :assumption (or (not b17) (not b340) ) :assumption (or b36 (not b340) ) :assumption (or b50 (not b340) ) :assumption (or (= r96 0) b343 ) :assumption (or (not b343) (= r96 (~ 1)) ) :assumption (or b54 (not b343) ) :assumption (or (not b24) (not b343) ) :assumption (or b17 (not b343) ) :assumption (or b55 (not b343) ) :assumption (or (= r97 0) b346 ) :assumption (or (not b346) (= r97 (~ 1)) ) :assumption (or b19 (not b346) ) :assumption (or (not b74) (not b346) ) :assumption (or b69 (not b346) ) :assumption (or b203 (not b346) ) :assumption (or (= r98 0) b349 ) :assumption (or (not b349) (= r98 (~ 1)) ) :assumption (or b18 (not b349) ) :assumption (or (not b59) (not b349) ) :assumption (or b74 (not b349) ) :assumption (or b60 (not b349) ) :assumption (or (= r99 0) b352 ) :assumption (or (not b352) (= r99 (~ 1)) ) :assumption (or b25 (not b352) ) :assumption (or (not b64) (not b352) ) :assumption (or b59 (not b352) ) :assumption (or b65 (not b352) ) :assumption (or (= r100 0) b355 ) :assumption (or (not b355) (= r100 (~ 1)) ) :assumption (or b37 (not b355) ) :assumption (or (not b74) (not b355) ) :assumption (or b69 (not b355) ) :assumption (or b75 (not b355) ) :assumption (or (= r101 0) b358 ) :assumption (or (not b358) (= r101 (~ 1)) ) :assumption (or b42 (not b358) ) :assumption (or (not b59) (not b358) ) :assumption (or b74 (not b358) ) :assumption (or b79 (not b358) ) :assumption (or (= r102 0) b361 ) :assumption (or (not b361) (= r102 (~ 1)) ) :assumption (or (not b64) (not b361) ) :assumption (or b59 (not b361) ) :assumption (or b147 (not b361) ) :assumption (or (= r103 0) b364 ) :assumption (or (not b364) (= r103 (~ 1)) ) :assumption (or b49 (not b364) ) :assumption (or (not b74) (not b364) ) :assumption (or b69 (not b364) ) :assumption (or b233 (not b364) ) :assumption (or (= r104 0) b367 ) :assumption (or (not b367) (= r104 (~ 1)) ) :assumption (or b48 (not b367) ) :assumption (or (not b59) (not b367) ) :assumption (or b74 (not b367) ) :assumption (or b84 (not b367) ) :assumption (or (= r105 0) b370 ) :assumption (or (not b370) (= r105 (~ 1)) ) :assumption (or b54 (not b370) ) :assumption (or (not b64) (not b370) ) :assumption (or b59 (not b370) ) :assumption (or b88 (not b370) ) :assumption (or (= r106 0) b373 ) :assumption (or (not b373) (= r106 (~ 1)) ) :assumption (or b94 (not b373) ) :assumption (or (not b108) (not b373) ) :assumption (or b103 (not b373) ) :assumption (or b158 (not b373) ) :assumption (or (= r107 0) b376 ) :assumption (or (not b376) (= r107 (~ 1)) ) :assumption (or b93 (not b376) ) :assumption (or (not b92) (not b376) ) :assumption (or b108 (not b376) ) :assumption (or b20 (not b376) ) :assumption (or (= r108 0) b379 ) :assumption (or (not b379) (= r108 (~ 1)) ) :assumption (or b99 (not b379) ) :assumption (or (not b98) (not b379) ) :assumption (or b92 (not b379) ) :assumption (or b26 (not b379) ) :assumption (or (= r109 0) b382 ) :assumption (or (not b382) (= r109 (~ 1)) ) :assumption (or b109 (not b382) ) :assumption (or (not b108) (not b382) ) :assumption (or b103 (not b382) ) :assumption (or b38 (not b382) ) :assumption (or (= r110 0) b385 ) :assumption (or (not b385) (= r110 (~ 1)) ) :assumption (or b113 (not b385) ) :assumption (or (not b92) (not b385) ) :assumption (or b108 (not b385) ) :assumption (or b43 (not b385) ) :assumption (or (= r111 0) b388 ) :assumption (or (not b388) (= r111 (~ 1)) ) :assumption (or b117 (not b388) ) :assumption (or (not b98) (not b388) ) :assumption (or b92 (not b388) ) :assumption (or b118 (not b388) ) :assumption (or (= r112 0) b391 ) :assumption (or (not b391) (= r112 (~ 1)) ) :assumption (or b123 (not b391) ) :assumption (or (not b108) (not b391) ) :assumption (or b103 (not b391) ) :assumption (or b193 (not b391) ) :assumption (or (= r113 0) b394 ) :assumption (or (not b394) (= r113 (~ 1)) ) :assumption (or b122 (not b394) ) :assumption (or (not b92) (not b394) ) :assumption (or b108 (not b394) ) :assumption (or b50 (not b394) ) :assumption (or (= r114 0) b397 ) :assumption (or (not b397) (= r114 (~ 1)) ) :assumption (or (not b98) (not b397) ) :assumption (or b92 (not b397) ) :assumption (or b55 (not b397) ) :assumption (or (= r115 0) b400 ) :assumption (or (not b400) (= r115 (~ 1)) ) :assumption (or b94 (not b400) ) :assumption (or (not b140) (not b400) ) :assumption (or b136 (not b400) ) :assumption (or b203 (not b400) ) :assumption (or (= r116 0) b403 ) :assumption (or (not b403) (= r116 (~ 1)) ) :assumption (or b93 (not b403) ) :assumption (or (not b128) (not b403) ) :assumption (or b140 (not b403) ) :assumption (or b60 (not b403) ) :assumption (or (= r117 0) b406 ) :assumption (or (not b406) (= r117 (~ 1)) ) :assumption (or b99 (not b406) ) :assumption (or (not b132) (not b406) ) :assumption (or b128 (not b406) ) :assumption (or b65 (not b406) ) :assumption (or (= r118 0) b409 ) :assumption (or (not b409) (= r118 (~ 1)) ) :assumption (or b109 (not b409) ) :assumption (or (not b140) (not b409) ) :assumption (or b136 (not b409) ) :assumption (or b75 (not b409) ) :assumption (or (= r119 0) b412 ) :assumption (or (not b412) (= r119 (~ 1)) ) :assumption (or b113 (not b412) ) :assumption (or (not b128) (not b412) ) :assumption (or b140 (not b412) ) :assumption (or b79 (not b412) ) :assumption (or (= r120 0) b415 ) :assumption (or (not b415) (= r120 (~ 1)) ) :assumption (or b117 (not b415) ) :assumption (or (not b132) (not b415) ) :assumption (or b128 (not b415) ) :assumption (or b147 (not b415) ) :assumption (or (= r121 0) b418 ) :assumption (or (not b418) (= r121 (~ 1)) ) :assumption (or b123 (not b418) ) :assumption (or (not b140) (not b418) ) :assumption (or b136 (not b418) ) :assumption (or b233 (not b418) ) :assumption (or (= r122 0) b421 ) :assumption (or (not b421) (= r122 (~ 1)) ) :assumption (or b122 (not b421) ) :assumption (or (not b128) (not b421) ) :assumption (or b140 (not b421) ) :assumption (or b84 (not b421) ) :assumption (or (= r123 0) b424 ) :assumption (or (not b424) (= r123 (~ 1)) ) :assumption (or (not b132) (not b424) ) :assumption (or b128 (not b424) ) :assumption (or b88 (not b424) ) :assumption (or (= r124 0) b427 ) :assumption (or (not b427) (= r124 (~ 1)) ) :assumption (or b156 (not b427) ) :assumption (or (not b155) (not b427) ) :assumption (or b185 (not b427) ) :assumption (or b158 (not b427) ) :assumption (or (= r125 0) b430 ) :assumption (or (not b430) (= r125 (~ 1)) ) :assumption (or b163 (not b430) ) :assumption (or (not b162) (not b430) ) :assumption (or b155 (not b430) ) :assumption (or b20 (not b430) ) :assumption (or (= r126 0) b433 ) :assumption (or (not b433) (= r126 (~ 1)) ) :assumption (or b168 (not b433) ) :assumption (or (not b167) (not b433) ) :assumption (or b162 (not b433) ) :assumption (or b26 (not b433) ) :assumption (or (= r127 0) b436 ) :assumption (or (not b436) (= r127 (~ 1)) ) :assumption (or b172 (not b436) ) :assumption (or (not b155) (not b436) ) :assumption (or b185 (not b436) ) :assumption (or b38 (not b436) ) :assumption (or (= r128 0) b439 ) :assumption (or (not b439) (= r128 (~ 1)) ) :assumption (or b177 (not b439) ) :assumption (or (not b162) (not b439) ) :assumption (or b155 (not b439) ) :assumption (or b43 (not b439) ) :assumption (or (= r129 0) b442 ) :assumption (or (not b442) (= r129 (~ 1)) ) :assumption (or b181 (not b442) ) :assumption (or (not b167) (not b442) ) :assumption (or b162 (not b442) ) :assumption (or b118 (not b442) ) :assumption (or (= r130 0) b445 ) :assumption (or (not b445) (= r130 (~ 1)) ) :assumption (or b192 (not b445) ) :assumption (or (not b155) (not b445) ) :assumption (or b185 (not b445) ) :assumption (or b193 (not b445) ) :assumption (or (= r131 0) b448 ) :assumption (or (not b448) (= r131 (~ 1)) ) :assumption (or b197 (not b448) ) :assumption (or (not b162) (not b448) ) :assumption (or b155 (not b448) ) :assumption (or b50 (not b448) ) :assumption (or (= r132 0) b451 ) :assumption (or (not b451) (= r132 (~ 1)) ) :assumption (or (not b167) (not b451) ) :assumption (or b162 (not b451) ) :assumption (or b55 (not b451) ) :assumption (or (= r133 0) b454 ) :assumption (or (not b454) (= r133 (~ 1)) ) :assumption (or b157 (not b454) ) :assumption (or (not b228) (not b454) ) :assumption (or b224 (not b454) ) :assumption (or (not b454) b456 ) :assumption (or (= r134 0) b458 ) :assumption (or (not b458) (= r134 (~ 1)) ) :assumption (or b156 (not b458) ) :assumption (or (not b202) (not b458) ) :assumption (or b228 (not b458) ) :assumption (or b203 (not b458) ) :assumption (or (= r135 0) b461 ) :assumption (or (not b461) (= r135 (~ 1)) ) :assumption (or b163 (not b461) ) :assumption (or (not b207) (not b461) ) :assumption (or b202 (not b461) ) :assumption (or b60 (not b461) ) :assumption (or (= r136 0) b464 ) :assumption (or (not b464) (= r136 (~ 1)) ) :assumption (or b168 (not b464) ) :assumption (or (not b211) (not b464) ) :assumption (or b207 (not b464) ) :assumption (or b65 (not b464) ) :assumption (or (= r137 0) b467 ) :assumption (or (not b467) (= r137 (~ 1)) ) :assumption (or b173 (not b467) ) :assumption (or (not b228) (not b467) ) :assumption (or b224 (not b467) ) :assumption (or b70 (not b467) ) :assumption (or (= r138 0) b470 ) :assumption (or (not b470) (= r138 (~ 1)) ) :assumption (or b172 (not b470) ) :assumption (or (not b202) (not b470) ) :assumption (or b228 (not b470) ) :assumption (or b75 (not b470) ) :assumption (or (= r139 0) b473 ) :assumption (or (not b473) (= r139 (~ 1)) ) :assumption (or b177 (not b473) ) :assumption (or (not b207) (not b473) ) :assumption (or b202 (not b473) ) :assumption (or b79 (not b473) ) :assumption (or (= r140 0) b476 ) :assumption (or (not b476) (= r140 (~ 1)) ) :assumption (or b181 (not b476) ) :assumption (or (not b211) (not b476) ) :assumption (or b207 (not b476) ) :assumption (or b147 (not b476) ) :assumption (or (= r141 0) b479 ) :assumption (or (not b479) (= r141 (~ 1)) ) :assumption (or b186 (not b479) ) :assumption (or (not b228) (not b479) ) :assumption (or b224 (not b479) ) :assumption (or b229 (not b479) ) :assumption (or (= r142 0) b482 ) :assumption (or (not b482) (= r142 (~ 1)) ) :assumption (or b192 (not b482) ) :assumption (or (not b202) (not b482) ) :assumption (or b228 (not b482) ) :assumption (or b233 (not b482) ) :assumption (or (= r143 0) b485 ) :assumption (or (not b485) (= r143 (~ 1)) ) :assumption (or b197 (not b485) ) :assumption (or (not b207) (not b485) ) :assumption (or b202 (not b485) ) :assumption (or b84 (not b485) ) :assumption (or (= r144 0) b488 ) :assumption (or (not b488) (= r144 (~ 1)) ) :assumption (or (not b211) (not b488) ) :assumption (or b207 (not b488) ) :assumption (or b88 (not b488) ) :assumption (or (= r145 0) b491 ) :assumption (or (not b491) (= r145 (~ 1)) ) :assumption (or b242 (not b491) ) :assumption (or (not b241) (not b491) ) :assumption (or b267 (not b491) ) :assumption (or b158 (not b491) ) :assumption (or (= r146 0) b494 ) :assumption (or (not b494) (= r146 (~ 1)) ) :assumption (or b248 (not b494) ) :assumption (or (not b247) (not b494) ) :assumption (or b241 (not b494) ) :assumption (or b20 (not b494) ) :assumption (or (= r147 0) b497 ) :assumption (or (not b497) (= r147 (~ 1)) ) :assumption (or b253 (not b497) ) :assumption (or (not b252) (not b497) ) :assumption (or b247 (not b497) ) :assumption (or b26 (not b497) ) :assumption (or (= r148 0) b500 ) :assumption (or (not b500) (= r148 (~ 1)) ) :assumption (or b257 (not b500) ) :assumption (or (not b241) (not b500) ) :assumption (or b267 (not b500) ) :assumption (or b38 (not b500) ) :assumption (or (= r149 0) b503 ) :assumption (or (not b503) (= r149 (~ 1)) ) :assumption (or b262 (not b503) ) :assumption (or (not b247) (not b503) ) :assumption (or b241 (not b503) ) :assumption (or b43 (not b503) ) :assumption (or (= r150 0) b506 ) :assumption (or (not b506) (= r150 (~ 1)) ) :assumption (or (not b252) (not b506) ) :assumption (or b247 (not b506) ) :assumption (or b118 (not b506) ) :assumption (or (= r151 0) b509 ) :assumption (or (not b509) (= r151 (~ 1)) ) :assumption (or b273 (not b509) ) :assumption (or (not b241) (not b509) ) :assumption (or b267 (not b509) ) :assumption (or b193 (not b509) ) :assumption (or (= r152 0) b512 ) :assumption (or (not b512) (= r152 (~ 1)) ) :assumption (or b277 (not b512) ) :assumption (or (not b247) (not b512) ) :assumption (or b241 (not b512) ) :assumption (or b50 (not b512) ) :assumption (or (= r153 0) b515 ) :assumption (or (not b515) (= r153 (~ 1)) ) :assumption (or b281 (not b515) ) :assumption (or (not b252) (not b515) ) :assumption (or b247 (not b515) ) :assumption (or b55 (not b515) ) :assumption (or (= r154 0) b518 ) :assumption (or (not b518) (= r154 (~ 1)) ) :assumption (or b243 (not b518) ) :assumption (or (not b308) (not b518) ) :assumption (or b304 (not b518) ) :assumption (or b456 (not b518) ) :assumption (or (= r155 0) b521 ) :assumption (or (not b521) (= r155 (~ 1)) ) :assumption (or b242 (not b521) ) :assumption (or (not b285) (not b521) ) :assumption (or b308 (not b521) ) :assumption (or b203 (not b521) ) :assumption (or (= r156 0) b524 ) :assumption (or (not b524) (= r156 (~ 1)) ) :assumption (or b248 (not b524) ) :assumption (or (not b289) (not b524) ) :assumption (or b285 (not b524) ) :assumption (or b60 (not b524) ) :assumption (or (= r157 0) b527 ) :assumption (or (not b527) (= r157 (~ 1)) ) :assumption (or b253 (not b527) ) :assumption (or (not b293) (not b527) ) :assumption (or b289 (not b527) ) :assumption (or b65 (not b527) ) :assumption (or (= r158 0) b530 ) :assumption (or (not b530) (= r158 (~ 1)) ) :assumption (or b258 (not b530) ) :assumption (or (not b308) (not b530) ) :assumption (or b304 (not b530) ) :assumption (or b70 (not b530) ) :assumption (or (= r159 0) b533 ) :assumption (or (not b533) (= r159 (~ 1)) ) :assumption (or b257 (not b533) ) :assumption (or (not b285) (not b533) ) :assumption (or b308 (not b533) ) :assumption (or b75 (not b533) ) :assumption (or (= r160 0) b536 ) :assumption (or (not b536) (= r160 (~ 1)) ) :assumption (or b262 (not b536) ) :assumption (or (not b289) (not b536) ) :assumption (or b285 (not b536) ) :assumption (or b79 (not b536) ) :assumption (or (= r161 0) b539 ) :assumption (or (not b539) (= r161 (~ 1)) ) :assumption (or (not b293) (not b539) ) :assumption (or b289 (not b539) ) :assumption (or b147 (not b539) ) :assumption (or (= r162 0) b542 ) :assumption (or (not b542) (= r162 (~ 1)) ) :assumption (or b268 (not b542) ) :assumption (or (not b308) (not b542) ) :assumption (or b304 (not b542) ) :assumption (or b229 (not b542) ) :assumption (or (= r163 0) b545 ) :assumption (or (not b545) (= r163 (~ 1)) ) :assumption (or b273 (not b545) ) :assumption (or (not b285) (not b545) ) :assumption (or b308 (not b545) ) :assumption (or b233 (not b545) ) :assumption (or (= r164 0) b548 ) :assumption (or (not b548) (= r164 (~ 1)) ) :assumption (or b277 (not b548) ) :assumption (or (not b289) (not b548) ) :assumption (or b285 (not b548) ) :assumption (or b84 (not b548) ) :assumption (or (= r165 0) b551 ) :assumption (or (not b551) (= r165 (~ 1)) ) :assumption (or b281 (not b551) ) :assumption (or (not b293) (not b551) ) :assumption (or b289 (not b551) ) :assumption (or b88 (not b551) ) :assumption (or (= r166 0) b554 ) :assumption (or b554 (= r167 0) ) :assumption (or (not b554) (= r167 (* (~ 768) 4)) ) :assumption (or (not b554) (= r166 (* 768 4)) ) :assumption (or b32 (not b554) ) :assumption (or (not b554) (not b558) ) :assumption (or (not b554) (>= r10 (* 768 4)) ) :assumption (or (= r168 0) b561 ) :assumption (or b561 (= r169 0) ) :assumption (or (not b561) (= r169 (* (~ 768) 4)) ) :assumption (or (not b561) (= r168 (* 768 4)) ) :assumption (or b38 (not b561) ) :assumption (or (not b158) (not b561) ) :assumption (or b558 (not b561) ) :assumption (or (not b561) (>= r170 (* 768 4)) ) :assumption (or (= r171 0) b567 ) :assumption (or b567 (= r172 0) ) :assumption (or (not b567) (= r172 (* (~ 768) 4)) ) :assumption (or (not b567) (= r171 (* 768 4)) ) :assumption (or b43 (not b567) ) :assumption (or (not b20) (not b567) ) :assumption (or b158 (not b567) ) :assumption (or (not b567) (>= r173 (* 768 4)) ) :assumption (or (= r174 0) b573 ) :assumption (or b573 (= r175 0) ) :assumption (or (not b573) (= r175 (* (~ 768) 4)) ) :assumption (or (not b573) (= r174 (* 768 4)) ) :assumption (or b118 (not b573) ) :assumption (or (not b26) (not b573) ) :assumption (or b20 (not b573) ) :assumption (or (not b573) (>= r176 (* 768 4)) ) :assumption (or (= r179 0) b582 ) :assumption (or b582 (= r180 0) ) :assumption (or (not b582) (= r180 (* (~ 532) 4)) ) :assumption (or (not b582) (= r179 (* 532 4)) ) :assumption (or b188 (not b582) ) :assumption (or (not b558) (not b582) ) :assumption (or (not b582) (>= r10 (* 532 4)) ) :assumption (or (= r181 0) b588 ) :assumption (or b588 (= r182 0) ) :assumption (or (not b588) (= r182 (* (~ 532) 4)) ) :assumption (or (not b588) (= r181 (* 532 4)) ) :assumption (or b193 (not b588) ) :assumption (or (not b158) (not b588) ) :assumption (or b558 (not b588) ) :assumption (or (not b588) (>= r170 (* 532 4)) ) :assumption (or (= r183 0) b594 ) :assumption (or b594 (= r184 0) ) :assumption (or (not b594) (= r184 (* (~ 532) 4)) ) :assumption (or (not b594) (= r183 (* 532 4)) ) :assumption (or b50 (not b594) ) :assumption (or (not b20) (not b594) ) :assumption (or b158 (not b594) ) :assumption (or (not b594) (>= r173 (* 532 4)) ) :assumption (or (= r185 0) b600 ) :assumption (or b600 (= r186 0) ) :assumption (or (not b600) (= r186 (* (~ 532) 4)) ) :assumption (or (not b600) (= r185 (* 532 4)) ) :assumption (or b55 (not b600) ) :assumption (or (not b26) (not b600) ) :assumption (or b20 (not b600) ) :assumption (or (not b600) (>= r176 (* 532 4)) ) :assumption (or (= r189 0) b609 ) :assumption (or b609 (= r190 0) ) :assumption (or (not b609) (= r190 (* (~ 768) 4)) ) :assumption (or (not b609) (= r189 (* 768 4)) ) :assumption (or b158 (not b609) ) :assumption (or (not b38) (not b609) ) :assumption (or b32 (not b609) ) :assumption (or (>= r170 (* 768 4)) (not b609) ) :assumption (or (= r191 0) b614 ) :assumption (or b614 (= r192 0) ) :assumption (or (not b614) (= r192 (* (~ 768) 4)) ) :assumption (or (not b614) (= r191 (* 768 4)) ) :assumption (or b20 (not b614) ) :assumption (or (not b43) (not b614) ) :assumption (or b38 (not b614) ) :assumption (or (>= r173 (* 768 4)) (not b614) ) :assumption (or (= r193 0) b619 ) :assumption (or b619 (= r194 0) ) :assumption (or (not b619) (= r194 (* (~ 768) 4)) ) :assumption (or (not b619) (= r193 (* 768 4)) ) :assumption (or b26 (not b619) ) :assumption (or (not b118) (not b619) ) :assumption (or b43 (not b619) ) :assumption (or (>= r176 (* 768 4)) (not b619) ) :assumption (or (= r195 0) b624 ) :assumption (or b624 (= r196 0) ) :assumption (or (not b624) (= r196 (* (~ 768) 4)) ) :assumption (or (not b624) (= r195 (* 768 4)) ) :assumption (or (not b580) (not b624) ) :assumption (or b118 (not b624) ) :assumption (or (not b624) (>= r197 (* 768 4)) ) :assumption (or (= r198 0) b630 ) :assumption (or b630 (= r199 0) ) :assumption (or (not b630) (= r199 (* (~ 750) 4)) ) :assumption (or (not b630) (= r198 (* 750 4)) ) :assumption (or b193 (not b630) ) :assumption (or (not b38) (not b630) ) :assumption (or b32 (not b630) ) :assumption (or (not b630) (>= r170 (* 750 4)) ) :assumption (or (= r200 0) b636 ) :assumption (or b636 (= r201 0) ) :assumption (or (not b636) (= r201 (* (~ 750) 4)) ) :assumption (or (not b636) (= r200 (* 750 4)) ) :assumption (or b50 (not b636) ) :assumption (or (not b43) (not b636) ) :assumption (or b38 (not b636) ) :assumption (or (not b636) (>= r173 (* 750 4)) ) :assumption (or (= r202 0) b642 ) :assumption (or b642 (= r203 0) ) :assumption (or (not b642) (= r203 (* (~ 750) 4)) ) :assumption (or (not b642) (= r202 (* 750 4)) ) :assumption (or b55 (not b642) ) :assumption (or (not b118) (not b642) ) :assumption (or b43 (not b642) ) :assumption (or (not b642) (>= r176 (* 750 4)) ) :assumption (or (= r204 0) b648 ) :assumption (or b648 (= r205 0) ) :assumption (or (not b648) (= r205 (* (~ 750) 4)) ) :assumption (or (not b648) (= r204 (* 750 4)) ) :assumption (or b607 (not b648) ) :assumption (or (not b580) (not b648) ) :assumption (or b118 (not b648) ) :assumption (or (not b648) (>= r197 (* 750 4)) ) :assumption (or (= r206 0) b654 ) :assumption (or b654 (= r207 0) ) :assumption (or (not b654) (= r207 (* (~ 532) 4)) ) :assumption (or (not b654) (= r206 (* 532 4)) ) :assumption (or b158 (not b654) ) :assumption (or (not b193) (not b654) ) :assumption (or b188 (not b654) ) :assumption (or (>= r170 (* 532 4)) (not b654) ) :assumption (or (= r208 0) b659 ) :assumption (or b659 (= r209 0) ) :assumption (or (not b659) (= r209 (* (~ 532) 4)) ) :assumption (or (not b659) (= r208 (* 532 4)) ) :assumption (or b20 (not b659) ) :assumption (or (not b50) (not b659) ) :assumption (or b193 (not b659) ) :assumption (or (>= r173 (* 532 4)) (not b659) ) :assumption (or (= r210 0) b664 ) :assumption (or b664 (= r211 0) ) :assumption (or (not b664) (= r211 (* (~ 532) 4)) ) :assumption (or (not b664) (= r210 (* 532 4)) ) :assumption (or b26 (not b664) ) :assumption (or (not b55) (not b664) ) :assumption (or b50 (not b664) ) :assumption (or (>= r176 (* 532 4)) (not b664) ) :assumption (or (= r212 0) b669 ) :assumption (or b669 (= r213 0) ) :assumption (or (not b669) (= r213 (* (~ 532) 4)) ) :assumption (or (not b669) (= r212 (* 532 4)) ) :assumption (or (not b607) (not b669) ) :assumption (or b55 (not b669) ) :assumption (or (not b669) (>= r197 (* 532 4)) ) :assumption (or (= r214 0) b675 ) :assumption (or b675 (= r215 0) ) :assumption (or (not b675) (= r215 (* (~ 750) 4)) ) :assumption (or (not b675) (= r214 (* 750 4)) ) :assumption (or b38 (not b675) ) :assumption (or (not b193) (not b675) ) :assumption (or b188 (not b675) ) :assumption (or (>= r170 (* 750 4)) (not b675) ) :assumption (or (= r216 0) b680 ) :assumption (or b680 (= r217 0) ) :assumption (or (not b680) (= r217 (* (~ 750) 4)) ) :assumption (or (not b680) (= r216 (* 750 4)) ) :assumption (or b43 (not b680) ) :assumption (or (not b50) (not b680) ) :assumption (or b193 (not b680) ) :assumption (or (>= r173 (* 750 4)) (not b680) ) :assumption (or (= r218 0) b685 ) :assumption (or b685 (= r219 0) ) :assumption (or (not b685) (= r219 (* (~ 750) 4)) ) :assumption (or (not b685) (= r218 (* 750 4)) ) :assumption (or b118 (not b685) ) :assumption (or (not b55) (not b685) ) :assumption (or b50 (not b685) ) :assumption (or (>= r176 (* 750 4)) (not b685) ) :assumption (or (= r220 0) b690 ) :assumption (or b690 (= r221 0) ) :assumption (or (not b690) (= r221 (* (~ 750) 4)) ) :assumption (or (not b690) (= r220 (* 750 4)) ) :assumption (or b580 (not b690) ) :assumption (or (not b607) (not b690) ) :assumption (or b55 (not b690) ) :assumption (or (>= r197 (* 750 4)) (not b690) ) :assumption (or (= r222 0) b695 ) :assumption (or b695 (= r223 0) ) :assumption (or (not b695) (= r223 (* (~ 768) 3)) ) :assumption (or (not b695) (= r222 (* 768 3)) ) :assumption (or b75 (not b695) ) :assumption (or (not b203) (not b695) ) :assumption (or b456 (not b695) ) :assumption (or (not b695) (>= r224 (* 768 3)) ) :assumption (or (= r225 0) b701 ) :assumption (or b701 (= r226 0) ) :assumption (or (not b701) (= r226 (* (~ 768) 3)) ) :assumption (or (not b701) (= r225 (* 768 3)) ) :assumption (or b79 (not b701) ) :assumption (or (not b60) (not b701) ) :assumption (or b203 (not b701) ) :assumption (or (not b701) (>= r227 (* 768 3)) ) :assumption (or (= r228 0) b707 ) :assumption (or b707 (= r229 0) ) :assumption (or (not b707) (= r229 (* (~ 768) 3)) ) :assumption (or (not b707) (= r228 (* 768 3)) ) :assumption (or b147 (not b707) ) :assumption (or (not b65) (not b707) ) :assumption (or b60 (not b707) ) :assumption (or (not b707) (>= r230 (* 768 3)) ) :assumption (or (= r231 0) b713 ) :assumption (or b713 (= r232 0) ) :assumption (or (not b713) (= r232 (* (~ 768) 3)) ) :assumption (or (not b713) (= r231 (* 768 3)) ) :assumption (or (not b713) b717 ) :assumption (or (not b713) (not b718) ) :assumption (or b65 (not b713) ) :assumption (or (not b713) (>= r233 (* 768 3)) ) :assumption (or (= r234 0) b721 ) :assumption (or b721 (= r235 0) ) :assumption (or (not b721) (= r235 (* (~ 532) 3)) ) :assumption (or (not b721) (= r234 (* 532 3)) ) :assumption (or b233 (not b721) ) :assumption (or (not b203) (not b721) ) :assumption (or b456 (not b721) ) :assumption (or (not b721) (>= r224 (* 532 3)) ) :assumption (or (= r236 0) b727 ) :assumption (or b727 (= r237 0) ) :assumption (or (not b727) (= r237 (* (~ 532) 3)) ) :assumption (or (not b727) (= r236 (* 532 3)) ) :assumption (or b84 (not b727) ) :assumption (or (not b60) (not b727) ) :assumption (or b203 (not b727) ) :assumption (or (not b727) (>= r227 (* 532 3)) ) :assumption (or (= r238 0) b733 ) :assumption (or b733 (= r239 0) ) :assumption (or (not b733) (= r239 (* (~ 532) 3)) ) :assumption (or (not b733) (= r238 (* 532 3)) ) :assumption (or b88 (not b733) ) :assumption (or (not b65) (not b733) ) :assumption (or b60 (not b733) ) :assumption (or (not b733) (>= r230 (* 532 3)) ) :assumption (or (= r240 0) b739 ) :assumption (or b739 (= r241 0) ) :assumption (or (not b739) (= r241 (* (~ 532) 3)) ) :assumption (or (not b739) (= r240 (* 532 3)) ) :assumption (or (not b739) b743 ) :assumption (or (not b718) (not b739) ) :assumption (or b65 (not b739) ) :assumption (or (not b739) (>= r233 (* 532 3)) ) :assumption (or (= r242 0) b746 ) :assumption (or b746 (= r243 0) ) :assumption (or (not b746) (= r243 (* (~ 768) 3)) ) :assumption (or (not b746) (= r242 (* 768 3)) ) :assumption (or b203 (not b746) ) :assumption (or (not b75) (not b746) ) :assumption (or b70 (not b746) ) :assumption (or (>= r224 (* 768 3)) (not b746) ) :assumption (or (= r244 0) b751 ) :assumption (or b751 (= r245 0) ) :assumption (or (not b751) (= r245 (* (~ 768) 3)) ) :assumption (or (not b751) (= r244 (* 768 3)) ) :assumption (or b60 (not b751) ) :assumption (or (not b79) (not b751) ) :assumption (or b75 (not b751) ) :assumption (or (>= r227 (* 768 3)) (not b751) ) :assumption (or (= r246 0) b756 ) :assumption (or b756 (= r247 0) ) :assumption (or (not b756) (= r247 (* (~ 768) 3)) ) :assumption (or (not b756) (= r246 (* 768 3)) ) :assumption (or b65 (not b756) ) :assumption (or (not b147) (not b756) ) :assumption (or b79 (not b756) ) :assumption (or (>= r230 (* 768 3)) (not b756) ) :assumption (or (= r248 0) b761 ) :assumption (or b761 (= r249 0) ) :assumption (or (not b761) (= r249 (* (~ 768) 3)) ) :assumption (or (not b761) (= r248 (* 768 3)) ) :assumption (or b718 (not b761) ) :assumption (or (not b717) (not b761) ) :assumption (or b147 (not b761) ) :assumption (or (>= r233 (* 768 3)) (not b761) ) :assumption (or (= r250 0) b766 ) :assumption (or b766 (= r251 0) ) :assumption (or (not b766) (= r251 (* (~ 750) 3)) ) :assumption (or (not b766) (= r250 (* 750 3)) ) :assumption (or b233 (not b766) ) :assumption (or (not b75) (not b766) ) :assumption (or b70 (not b766) ) :assumption (or (not b766) (>= r224 (* 750 3)) ) :assumption (or (= r252 0) b772 ) :assumption (or b772 (= r253 0) ) :assumption (or (not b772) (= r253 (* (~ 750) 3)) ) :assumption (or (not b772) (= r252 (* 750 3)) ) :assumption (or b84 (not b772) ) :assumption (or (not b79) (not b772) ) :assumption (or b75 (not b772) ) :assumption (or (not b772) (>= r227 (* 750 3)) ) :assumption (or (= r254 0) b778 ) :assumption (or b778 (= r255 0) ) :assumption (or (not b778) (= r255 (* (~ 750) 3)) ) :assumption (or (not b778) (= r254 (* 750 3)) ) :assumption (or b88 (not b778) ) :assumption (or (not b147) (not b778) ) :assumption (or b79 (not b778) ) :assumption (or (not b778) (>= r230 (* 750 3)) ) :assumption (or (= r256 0) b784 ) :assumption (or b784 (= r257 0) ) :assumption (or (not b784) (= r257 (* (~ 750) 3)) ) :assumption (or (not b784) (= r256 (* 750 3)) ) :assumption (or b743 (not b784) ) :assumption (or (not b717) (not b784) ) :assumption (or b147 (not b784) ) :assumption (or (not b784) (>= r233 (* 750 3)) ) :assumption (or (= r258 0) b790 ) :assumption (or b790 (= r259 0) ) :assumption (or (not b790) (= r259 (* (~ 532) 3)) ) :assumption (or (not b790) (= r258 (* 532 3)) ) :assumption (or b456 (not b790) ) :assumption (or (not b229) (not b790) ) :assumption (or (not b790) (>= r12 (* 532 3)) ) :assumption (or (= r260 0) b796 ) :assumption (or b796 (= r261 0) ) :assumption (or (not b796) (= r261 (* (~ 532) 3)) ) :assumption (or (not b796) (= r260 (* 532 3)) ) :assumption (or b203 (not b796) ) :assumption (or (not b233) (not b796) ) :assumption (or b229 (not b796) ) :assumption (or (>= r224 (* 532 3)) (not b796) ) :assumption (or (= r262 0) b801 ) :assumption (or b801 (= r263 0) ) :assumption (or (not b801) (= r263 (* (~ 532) 3)) ) :assumption (or (not b801) (= r262 (* 532 3)) ) :assumption (or b60 (not b801) ) :assumption (or (not b84) (not b801) ) :assumption (or b233 (not b801) ) :assumption (or (>= r227 (* 532 3)) (not b801) ) :assumption (or (= r264 0) b806 ) :assumption (or b806 (= r265 0) ) :assumption (or (not b806) (= r265 (* (~ 532) 3)) ) :assumption (or (not b806) (= r264 (* 532 3)) ) :assumption (or b65 (not b806) ) :assumption (or (not b88) (not b806) ) :assumption (or b84 (not b806) ) :assumption (or (>= r230 (* 532 3)) (not b806) ) :assumption (or (= r266 0) b811 ) :assumption (or b811 (= r267 0) ) :assumption (or (not b811) (= r267 (* (~ 532) 3)) ) :assumption (or (not b811) (= r266 (* 532 3)) ) :assumption (or b718 (not b811) ) :assumption (or (not b743) (not b811) ) :assumption (or b88 (not b811) ) :assumption (or (>= r233 (* 532 3)) (not b811) ) :assumption (or (= r268 0) b816 ) :assumption (or b816 (= r269 0) ) :assumption (or (not b816) (= r269 (* (~ 750) 3)) ) :assumption (or (not b816) (= r268 (* 750 3)) ) :assumption (or b70 (not b816) ) :assumption (or (not b229) (not b816) ) :assumption (or (not b816) (>= r12 (* 750 3)) ) :assumption (or (= r270 0) b822 ) :assumption (or b822 (= r271 0) ) :assumption (or (not b822) (= r271 (* (~ 750) 3)) ) :assumption (or (not b822) (= r270 (* 750 3)) ) :assumption (or b75 (not b822) ) :assumption (or (not b233) (not b822) ) :assumption (or b229 (not b822) ) :assumption (or (>= r224 (* 750 3)) (not b822) ) :assumption (or (= r272 0) b827 ) :assumption (or b827 (= r273 0) ) :assumption (or (not b827) (= r273 (* (~ 750) 3)) ) :assumption (or (not b827) (= r272 (* 750 3)) ) :assumption (or b79 (not b827) ) :assumption (or (not b84) (not b827) ) :assumption (or b233 (not b827) ) :assumption (or (>= r227 (* 750 3)) (not b827) ) :assumption (or (= r274 0) b832 ) :assumption (or b832 (= r275 0) ) :assumption (or (not b832) (= r275 (* (~ 750) 3)) ) :assumption (or (not b832) (= r274 (* 750 3)) ) :assumption (or b147 (not b832) ) :assumption (or (not b88) (not b832) ) :assumption (or b84 (not b832) ) :assumption (or (>= r230 (* 750 3)) (not b832) ) :assumption (or (= r276 0) b837 ) :assumption (or b837 (= r277 0) ) :assumption (or (not b837) (= r277 (* (~ 750) 3)) ) :assumption (or (not b837) (= r276 (* 750 3)) ) :assumption (or b717 (not b837) ) :assumption (or (not b743) (not b837) ) :assumption (or b88 (not b837) ) :assumption (or (>= r233 (* 750 3)) (not b837) ) :assumption (or (= r278 0) b842 ) :assumption (or b842 (= r279 0) ) :assumption (or (not b842) (= r279 (* (~ 768) 10)) ) :assumption (or (not b842) (= r278 (* 768 10)) ) :assumption (or b32 (not b842) ) :assumption (or (not b558) (not b842) ) :assumption (or (not b842) (>= r10 (* 768 10)) ) :assumption (or (not b842) (<= r9 2) ) :assumption (or (= r280 0) b849 ) :assumption (or b849 (= r281 0) ) :assumption (or (not b849) (= r281 (* (~ 768) 10)) ) :assumption (or (not b849) (= r280 (* 768 10)) ) :assumption (or b38 (not b849) ) :assumption (or (not b158) (not b849) ) :assumption (or b558 (not b849) ) :assumption (or (not b849) (>= r170 (* 768 10)) ) :assumption (or (not b849) (<= r282 2) ) :assumption (or (= r283 0) b856 ) :assumption (or b856 (= r284 0) ) :assumption (or (not b856) (= r284 (* (~ 768) 10)) ) :assumption (or (not b856) (= r283 (* 768 10)) ) :assumption (or b43 (not b856) ) :assumption (or (not b20) (not b856) ) :assumption (or b158 (not b856) ) :assumption (or (not b856) (>= r173 (* 768 10)) ) :assumption (or (not b856) (<= r285 2) ) :assumption (or (= r286 0) b863 ) :assumption (or b863 (= r287 0) ) :assumption (or (not b863) (= r287 (* (~ 768) 10)) ) :assumption (or (not b863) (= r286 (* 768 10)) ) :assumption (or b118 (not b863) ) :assumption (or (not b26) (not b863) ) :assumption (or b20 (not b863) ) :assumption (or (not b863) (>= r176 (* 768 10)) ) :assumption (or (not b863) (<= r288 2) ) :assumption (or (= r291 0) b872 ) :assumption (or b872 (= r292 0) ) :assumption (or (not b872) (= r292 (* (~ 532) 10)) ) :assumption (or (not b872) (= r291 (* 532 10)) ) :assumption (or b188 (not b872) ) :assumption (or (not b558) (not b872) ) :assumption (or (not b872) (>= r10 (* 532 10)) ) :assumption (or (<= r9 2) (not b872) ) :assumption (or (= r293 0) b878 ) :assumption (or b878 (= r294 0) ) :assumption (or (not b878) (= r294 (* (~ 532) 10)) ) :assumption (or (not b878) (= r293 (* 532 10)) ) :assumption (or b193 (not b878) ) :assumption (or (not b158) (not b878) ) :assumption (or b558 (not b878) ) :assumption (or (not b878) (>= r170 (* 532 10)) ) :assumption (or (<= r282 2) (not b878) ) :assumption (or (= r295 0) b884 ) :assumption (or b884 (= r296 0) ) :assumption (or (not b884) (= r296 (* (~ 532) 10)) ) :assumption (or (not b884) (= r295 (* 532 10)) ) :assumption (or b50 (not b884) ) :assumption (or (not b20) (not b884) ) :assumption (or b158 (not b884) ) :assumption (or (not b884) (>= r173 (* 532 10)) ) :assumption (or (<= r285 2) (not b884) ) :assumption (or (= r297 0) b890 ) :assumption (or b890 (= r298 0) ) :assumption (or (not b890) (= r298 (* (~ 532) 10)) ) :assumption (or (not b890) (= r297 (* 532 10)) ) :assumption (or b55 (not b890) ) :assumption (or (not b26) (not b890) ) :assumption (or b20 (not b890) ) :assumption (or (not b890) (>= r176 (* 532 10)) ) :assumption (or (<= r288 2) (not b890) ) :assumption (or (= r301 0) b898 ) :assumption (or b898 (= r302 0) ) :assumption (or (not b898) (= r302 (* (~ 768) 10)) ) :assumption (or (not b898) (= r301 (* 768 10)) ) :assumption (or b158 (not b898) ) :assumption (or (not b38) (not b898) ) :assumption (or b32 (not b898) ) :assumption (or (>= r170 (* 768 10)) (not b898) ) :assumption (or (<= r282 2) (not b898) ) :assumption (or (= r303 0) b903 ) :assumption (or b903 (= r304 0) ) :assumption (or (not b903) (= r304 (* (~ 768) 10)) ) :assumption (or (not b903) (= r303 (* 768 10)) ) :assumption (or b20 (not b903) ) :assumption (or (not b43) (not b903) ) :assumption (or b38 (not b903) ) :assumption (or (>= r173 (* 768 10)) (not b903) ) :assumption (or (<= r285 2) (not b903) ) :assumption (or (= r305 0) b908 ) :assumption (or b908 (= r306 0) ) :assumption (or (not b908) (= r306 (* (~ 768) 10)) ) :assumption (or (not b908) (= r305 (* 768 10)) ) :assumption (or b26 (not b908) ) :assumption (or (not b118) (not b908) ) :assumption (or b43 (not b908) ) :assumption (or (>= r176 (* 768 10)) (not b908) ) :assumption (or (<= r288 2) (not b908) ) :assumption (or (= r307 0) b913 ) :assumption (or b913 (= r308 0) ) :assumption (or (not b913) (= r308 (* (~ 768) 10)) ) :assumption (or (not b913) (= r307 (* 768 10)) ) :assumption (or (not b580) (not b913) ) :assumption (or b118 (not b913) ) :assumption (or (not b913) (>= r197 (* 768 10)) ) :assumption (or (not b913) (<= r309 2) ) :assumption (or (= r310 0) b920 ) :assumption (or b920 (= r311 0) ) :assumption (or (not b920) (= r311 (* (~ 750) 10)) ) :assumption (or (not b920) (= r310 (* 750 10)) ) :assumption (or b193 (not b920) ) :assumption (or (not b38) (not b920) ) :assumption (or b32 (not b920) ) :assumption (or (not b920) (>= r170 (* 750 10)) ) :assumption (or (<= r282 2) (not b920) ) :assumption (or (= r312 0) b926 ) :assumption (or b926 (= r313 0) ) :assumption (or (not b926) (= r313 (* (~ 750) 10)) ) :assumption (or (not b926) (= r312 (* 750 10)) ) :assumption (or b50 (not b926) ) :assumption (or (not b43) (not b926) ) :assumption (or b38 (not b926) ) :assumption (or (not b926) (>= r173 (* 750 10)) ) :assumption (or (<= r285 2) (not b926) ) :assumption (or (= r314 0) b932 ) :assumption (or b932 (= r315 0) ) :assumption (or (not b932) (= r315 (* (~ 750) 10)) ) :assumption (or (not b932) (= r314 (* 750 10)) ) :assumption (or b55 (not b932) ) :assumption (or (not b118) (not b932) ) :assumption (or b43 (not b932) ) :assumption (or (not b932) (>= r176 (* 750 10)) ) :assumption (or (<= r288 2) (not b932) ) :assumption (or (= r316 0) b938 ) :assumption (or b938 (= r317 0) ) :assumption (or (not b938) (= r317 (* (~ 750) 10)) ) :assumption (or (not b938) (= r316 (* 750 10)) ) :assumption (or b607 (not b938) ) :assumption (or (not b580) (not b938) ) :assumption (or b118 (not b938) ) :assumption (or (not b938) (>= r197 (* 750 10)) ) :assumption (or (<= r309 2) (not b938) ) :assumption (or (= r318 0) b944 ) :assumption (or b944 (= r319 0) ) :assumption (or (not b944) (= r319 (* (~ 532) 10)) ) :assumption (or (not b944) (= r318 (* 532 10)) ) :assumption (or b158 (not b944) ) :assumption (or (not b193) (not b944) ) :assumption (or b188 (not b944) ) :assumption (or (>= r170 (* 532 10)) (not b944) ) :assumption (or (<= r282 2) (not b944) ) :assumption (or (= r320 0) b949 ) :assumption (or b949 (= r321 0) ) :assumption (or (not b949) (= r321 (* (~ 532) 10)) ) :assumption (or (not b949) (= r320 (* 532 10)) ) :assumption (or b20 (not b949) ) :assumption (or (not b50) (not b949) ) :assumption (or b193 (not b949) ) :assumption (or (>= r173 (* 532 10)) (not b949) ) :assumption (or (<= r285 2) (not b949) ) :assumption (or (= r322 0) b954 ) :assumption (or b954 (= r323 0) ) :assumption (or (not b954) (= r323 (* (~ 532) 10)) ) :assumption (or (not b954) (= r322 (* 532 10)) ) :assumption (or b26 (not b954) ) :assumption (or (not b55) (not b954) ) :assumption (or b50 (not b954) ) :assumption (or (>= r176 (* 532 10)) (not b954) ) :assumption (or (<= r288 2) (not b954) ) :assumption (or (= r324 0) b959 ) :assumption (or b959 (= r325 0) ) :assumption (or (not b959) (= r325 (* (~ 532) 10)) ) :assumption (or (not b959) (= r324 (* 532 10)) ) :assumption (or (not b607) (not b959) ) :assumption (or b55 (not b959) ) :assumption (or (not b959) (>= r197 (* 532 10)) ) :assumption (or (<= r309 2) (not b959) ) :assumption (or (= r326 0) b965 ) :assumption (or b965 (= r327 0) ) :assumption (or (not b965) (= r327 (* (~ 750) 10)) ) :assumption (or (not b965) (= r326 (* 750 10)) ) :assumption (or b38 (not b965) ) :assumption (or (not b193) (not b965) ) :assumption (or b188 (not b965) ) :assumption (or (>= r170 (* 750 10)) (not b965) ) :assumption (or (<= r282 2) (not b965) ) :assumption (or (= r328 0) b970 ) :assumption (or b970 (= r329 0) ) :assumption (or (not b970) (= r329 (* (~ 750) 10)) ) :assumption (or (not b970) (= r328 (* 750 10)) ) :assumption (or b43 (not b970) ) :assumption (or (not b50) (not b970) ) :assumption (or b193 (not b970) ) :assumption (or (>= r173 (* 750 10)) (not b970) ) :assumption (or (<= r285 2) (not b970) ) :assumption (or (= r330 0) b975 ) :assumption (or b975 (= r331 0) ) :assumption (or (not b975) (= r331 (* (~ 750) 10)) ) :assumption (or (not b975) (= r330 (* 750 10)) ) :assumption (or b118 (not b975) ) :assumption (or (not b55) (not b975) ) :assumption (or b50 (not b975) ) :assumption (or (>= r176 (* 750 10)) (not b975) ) :assumption (or (<= r288 2) (not b975) ) :assumption (or (= r332 0) b980 ) :assumption (or b980 (= r333 0) ) :assumption (or (not b980) (= r333 (* (~ 750) 10)) ) :assumption (or (not b980) (= r332 (* 750 10)) ) :assumption (or b580 (not b980) ) :assumption (or (not b607) (not b980) ) :assumption (or b55 (not b980) ) :assumption (or (>= r197 (* 750 10)) (not b980) ) :assumption (or (<= r309 2) (not b980) ) :assumption (or (= r334 0) b985 ) :assumption (or b985 (= r335 0) ) :assumption (or (not b985) (= r335 (* (~ 768) 7)) ) :assumption (or (not b985) (= r334 (* 768 7)) ) :assumption (or b75 (not b985) ) :assumption (or (not b203) (not b985) ) :assumption (or b456 (not b985) ) :assumption (or (not b985) (>= r224 (* 768 7)) ) :assumption (or (not b985) (<= r336 8) ) :assumption (or (= r337 0) b992 ) :assumption (or b992 (= r338 0) ) :assumption (or (not b992) (= r338 (* (~ 768) 7)) ) :assumption (or (not b992) (= r337 (* 768 7)) ) :assumption (or b79 (not b992) ) :assumption (or (not b60) (not b992) ) :assumption (or b203 (not b992) ) :assumption (or (not b992) (>= r227 (* 768 7)) ) :assumption (or (not b992) (<= r339 8) ) :assumption (or (= r340 0) b999 ) :assumption (or b999 (= r341 0) ) :assumption (or (not b999) (= r341 (* (~ 768) 7)) ) :assumption (or (not b999) (= r340 (* 768 7)) ) :assumption (or b147 (not b999) ) :assumption (or (not b65) (not b999) ) :assumption (or b60 (not b999) ) :assumption (or (not b999) (>= r230 (* 768 7)) ) :assumption (or (not b999) (<= r342 8) ) :assumption (or (= r343 0) b1006 ) :assumption (or b1006 (= r344 0) ) :assumption (or (not b1006) (= r344 (* (~ 768) 7)) ) :assumption (or (not b1006) (= r343 (* 768 7)) ) :assumption (or b717 (not b1006) ) :assumption (or (not b718) (not b1006) ) :assumption (or b65 (not b1006) ) :assumption (or (not b1006) (>= r233 (* 768 7)) ) :assumption (or (not b1006) (<= r345 8) ) :assumption (or (= r346 0) b1013 ) :assumption (or b1013 (= r347 0) ) :assumption (or (not b1013) (= r347 (* (~ 532) 7)) ) :assumption (or (not b1013) (= r346 (* 532 7)) ) :assumption (or b233 (not b1013) ) :assumption (or (not b203) (not b1013) ) :assumption (or b456 (not b1013) ) :assumption (or (not b1013) (>= r224 (* 532 7)) ) :assumption (or (<= r336 8) (not b1013) ) :assumption (or (= r348 0) b1019 ) :assumption (or b1019 (= r349 0) ) :assumption (or (not b1019) (= r349 (* (~ 532) 7)) ) :assumption (or (not b1019) (= r348 (* 532 7)) ) :assumption (or b84 (not b1019) ) :assumption (or (not b60) (not b1019) ) :assumption (or b203 (not b1019) ) :assumption (or (not b1019) (>= r227 (* 532 7)) ) :assumption (or (<= r339 8) (not b1019) ) :assumption (or (= r350 0) b1025 ) :assumption (or b1025 (= r351 0) ) :assumption (or (not b1025) (= r351 (* (~ 532) 7)) ) :assumption (or (not b1025) (= r350 (* 532 7)) ) :assumption (or b88 (not b1025) ) :assumption (or (not b65) (not b1025) ) :assumption (or b60 (not b1025) ) :assumption (or (not b1025) (>= r230 (* 532 7)) ) :assumption (or (<= r342 8) (not b1025) ) :assumption (or (= r352 0) b1031 ) :assumption (or b1031 (= r353 0) ) :assumption (or (not b1031) (= r353 (* (~ 532) 7)) ) :assumption (or (not b1031) (= r352 (* 532 7)) ) :assumption (or b743 (not b1031) ) :assumption (or (not b718) (not b1031) ) :assumption (or b65 (not b1031) ) :assumption (or (not b1031) (>= r233 (* 532 7)) ) :assumption (or (<= r345 8) (not b1031) ) :assumption (or (= r354 0) b1037 ) :assumption (or b1037 (= r355 0) ) :assumption (or (not b1037) (= r355 (* (~ 768) 7)) ) :assumption (or (not b1037) (= r354 (* 768 7)) ) :assumption (or b203 (not b1037) ) :assumption (or (not b75) (not b1037) ) :assumption (or b70 (not b1037) ) :assumption (or (>= r224 (* 768 7)) (not b1037) ) :assumption (or (<= r336 8) (not b1037) ) :assumption (or (= r356 0) b1042 ) :assumption (or b1042 (= r357 0) ) :assumption (or (not b1042) (= r357 (* (~ 768) 7)) ) :assumption (or (not b1042) (= r356 (* 768 7)) ) :assumption (or b60 (not b1042) ) :assumption (or (not b79) (not b1042) ) :assumption (or b75 (not b1042) ) :assumption (or (>= r227 (* 768 7)) (not b1042) ) :assumption (or (<= r339 8) (not b1042) ) :assumption (or (= r358 0) b1047 ) :assumption (or b1047 (= r359 0) ) :assumption (or (not b1047) (= r359 (* (~ 768) 7)) ) :assumption (or (not b1047) (= r358 (* 768 7)) ) :assumption (or b65 (not b1047) ) :assumption (or (not b147) (not b1047) ) :assumption (or b79 (not b1047) ) :assumption (or (>= r230 (* 768 7)) (not b1047) ) :assumption (or (<= r342 8) (not b1047) ) :assumption (or (= r360 0) b1052 ) :assumption (or b1052 (= r361 0) ) :assumption (or (not b1052) (= r361 (* (~ 768) 7)) ) :assumption (or (not b1052) (= r360 (* 768 7)) ) :assumption (or b718 (not b1052) ) :assumption (or (not b717) (not b1052) ) :assumption (or b147 (not b1052) ) :assumption (or (>= r233 (* 768 7)) (not b1052) ) :assumption (or (<= r345 8) (not b1052) ) :assumption (or (= r362 0) b1057 ) :assumption (or b1057 (= r363 0) ) :assumption (or (not b1057) (= r363 (* (~ 750) 7)) ) :assumption (or (not b1057) (= r362 (* 750 7)) ) :assumption (or b233 (not b1057) ) :assumption (or (not b75) (not b1057) ) :assumption (or b70 (not b1057) ) :assumption (or (not b1057) (>= r224 (* 750 7)) ) :assumption (or (<= r336 8) (not b1057) ) :assumption (or (= r364 0) b1063 ) :assumption (or b1063 (= r365 0) ) :assumption (or (not b1063) (= r365 (* (~ 750) 7)) ) :assumption (or (not b1063) (= r364 (* 750 7)) ) :assumption (or b84 (not b1063) ) :assumption (or (not b79) (not b1063) ) :assumption (or b75 (not b1063) ) :assumption (or (not b1063) (>= r227 (* 750 7)) ) :assumption (or (<= r339 8) (not b1063) ) :assumption (or (= r366 0) b1069 ) :assumption (or b1069 (= r367 0) ) :assumption (or (not b1069) (= r367 (* (~ 750) 7)) ) :assumption (or (not b1069) (= r366 (* 750 7)) ) :assumption (or b88 (not b1069) ) :assumption (or (not b147) (not b1069) ) :assumption (or b79 (not b1069) ) :assumption (or (not b1069) (>= r230 (* 750 7)) ) :assumption (or (<= r342 8) (not b1069) ) :assumption (or (= r368 0) b1075 ) :assumption (or b1075 (= r369 0) ) :assumption (or (not b1075) (= r369 (* (~ 750) 7)) ) :assumption (or (not b1075) (= r368 (* 750 7)) ) :assumption (or b743 (not b1075) ) :assumption (or (not b717) (not b1075) ) :assumption (or b147 (not b1075) ) :assumption (or (not b1075) (>= r233 (* 750 7)) ) :assumption (or (<= r345 8) (not b1075) ) :assumption (or (= r370 0) b1081 ) :assumption (or b1081 (= r371 0) ) :assumption (or (not b1081) (= r371 (* (~ 532) 7)) ) :assumption (or (not b1081) (= r370 (* 532 7)) ) :assumption (or b456 (not b1081) ) :assumption (or (not b229) (not b1081) ) :assumption (or (not b1081) (>= r12 (* 532 7)) ) :assumption (or (not b1081) (<= r11 8) ) :assumption (or (= r372 0) b1088 ) :assumption (or b1088 (= r373 0) ) :assumption (or (not b1088) (= r373 (* (~ 532) 7)) ) :assumption (or (not b1088) (= r372 (* 532 7)) ) :assumption (or b203 (not b1088) ) :assumption (or (not b233) (not b1088) ) :assumption (or b229 (not b1088) ) :assumption (or (>= r224 (* 532 7)) (not b1088) ) :assumption (or (<= r336 8) (not b1088) ) :assumption (or (= r374 0) b1093 ) :assumption (or b1093 (= r375 0) ) :assumption (or (not b1093) (= r375 (* (~ 532) 7)) ) :assumption (or (not b1093) (= r374 (* 532 7)) ) :assumption (or b60 (not b1093) ) :assumption (or (not b84) (not b1093) ) :assumption (or b233 (not b1093) ) :assumption (or (>= r227 (* 532 7)) (not b1093) ) :assumption (or (<= r339 8) (not b1093) ) :assumption (or (= r376 0) b1098 ) :assumption (or b1098 (= r377 0) ) :assumption (or (not b1098) (= r377 (* (~ 532) 7)) ) :assumption (or (not b1098) (= r376 (* 532 7)) ) :assumption (or b65 (not b1098) ) :assumption (or (not b88) (not b1098) ) :assumption (or b84 (not b1098) ) :assumption (or (>= r230 (* 532 7)) (not b1098) ) :assumption (or (<= r342 8) (not b1098) ) :assumption (or (= r378 0) b1103 ) :assumption (or b1103 (= r379 0) ) :assumption (or (not b1103) (= r379 (* (~ 532) 7)) ) :assumption (or (not b1103) (= r378 (* 532 7)) ) :assumption (or b718 (not b1103) ) :assumption (or (not b743) (not b1103) ) :assumption (or b88 (not b1103) ) :assumption (or (>= r233 (* 532 7)) (not b1103) ) :assumption (or (<= r345 8) (not b1103) ) :assumption (or (= r380 0) b1108 ) :assumption (or b1108 (= r381 0) ) :assumption (or (not b1108) (= r381 (* (~ 750) 7)) ) :assumption (or (not b1108) (= r380 (* 750 7)) ) :assumption (or b70 (not b1108) ) :assumption (or (not b229) (not b1108) ) :assumption (or (not b1108) (>= r12 (* 750 7)) ) :assumption (or (<= r11 8) (not b1108) ) :assumption (or (= r382 0) b1114 ) :assumption (or b1114 (= r383 0) ) :assumption (or (not b1114) (= r383 (* (~ 750) 7)) ) :assumption (or (not b1114) (= r382 (* 750 7)) ) :assumption (or b75 (not b1114) ) :assumption (or (not b233) (not b1114) ) :assumption (or b229 (not b1114) ) :assumption (or (>= r224 (* 750 7)) (not b1114) ) :assumption (or (<= r336 8) (not b1114) ) :assumption (or (= r384 0) b1119 ) :assumption (or b1119 (= r385 0) ) :assumption (or (not b1119) (= r385 (* (~ 750) 7)) ) :assumption (or (not b1119) (= r384 (* 750 7)) ) :assumption (or b79 (not b1119) ) :assumption (or (not b84) (not b1119) ) :assumption (or b233 (not b1119) ) :assumption (or (>= r227 (* 750 7)) (not b1119) ) :assumption (or (<= r339 8) (not b1119) ) :assumption (or (= r386 0) b1124 ) :assumption (or b1124 (= r387 0) ) :assumption (or (not b1124) (= r387 (* (~ 750) 7)) ) :assumption (or (not b1124) (= r386 (* 750 7)) ) :assumption (or b147 (not b1124) ) :assumption (or (not b88) (not b1124) ) :assumption (or b84 (not b1124) ) :assumption (or (>= r230 (* 750 7)) (not b1124) ) :assumption (or (<= r342 8) (not b1124) ) :assumption (or (= r388 0) b1129 ) :assumption (or b1129 (= r389 0) ) :assumption (or (not b1129) (= r389 (* (~ 750) 7)) ) :assumption (or (not b1129) (= r388 (* 750 7)) ) :assumption (or b717 (not b1129) ) :assumption (or (not b743) (not b1129) ) :assumption (or b88 (not b1129) ) :assumption (or (>= r233 (* 750 7)) (not b1129) ) :assumption (or (<= r345 8) (not b1129) ) :assumption (or (not b1133) (= r170 9074) ) :assumption (or (not b1133) (< (+ r10 r390) 9074) ) :assumption (or (not b1136) (= r173 9074) ) :assumption (or (not b1136) (< (+ r170 r390) 9074) ) :assumption (or b558 (not b1136) ) :assumption (or (not b1139) (= r176 9074) ) :assumption (or (not b1139) (< (+ r173 r390) 9074) ) :assumption (or b158 (not b1139) ) :assumption (or (not b1142) (= r197 9074) ) :assumption (or (not b1142) (< (+ r176 r390) 9074) ) :assumption (or b20 (not b1142) ) :assumption (or (not b1145) (= r391 9074) ) :assumption (or (not b1145) (< (+ r197 r390) 9074) ) :assumption (or b26 (not b1145) ) :assumption (or (= r173 9074) (not b1148) ) :assumption (or (< (+ r170 r390) 9074) (not b1148) ) :assumption (or b32 (not b1148) ) :assumption (or (= r176 9074) (not b1149) ) :assumption (or (< (+ r173 r390) 9074) (not b1149) ) :assumption (or b38 (not b1149) ) :assumption (or (= r197 9074) (not b1150) ) :assumption (or (< (+ r176 r390) 9074) (not b1150) ) :assumption (or b43 (not b1150) ) :assumption (or (= r391 9074) (not b1151) ) :assumption (or (< (+ r197 r390) 9074) (not b1151) ) :assumption (or b118 (not b1151) ) :assumption (or (= r173 9074) (not b1152) ) :assumption (or (< (+ r170 r390) 9074) (not b1152) ) :assumption (or b188 (not b1152) ) :assumption (or (= r176 9074) (not b1153) ) :assumption (or (< (+ r173 r390) 9074) (not b1153) ) :assumption (or b193 (not b1153) ) :assumption (or (= r197 9074) (not b1154) ) :assumption (or (< (+ r176 r390) 9074) (not b1154) ) :assumption (or b50 (not b1154) ) :assumption (or (= r391 9074) (not b1155) ) :assumption (or (< (+ r197 r390) 9074) (not b1155) ) :assumption (or b55 (not b1155) ) :assumption (or (not b1156) (= r227 8873) ) :assumption (or (not b1156) (< (+ r224 r390) 8873) ) :assumption (or b456 (not b1156) ) :assumption (or (not b1159) (= r230 8873) ) :assumption (or (not b1159) (< (+ r227 r390) 8873) ) :assumption (or b203 (not b1159) ) :assumption (or (not b1162) (= r233 8873) ) :assumption (or (not b1162) (< (+ r230 r390) 8873) ) :assumption (or b60 (not b1162) ) :assumption (or (not b1165) (= r392 8873) ) :assumption (or (not b1165) (< (+ r233 r390) 8873) ) :assumption (or b65 (not b1165) ) :assumption (or (= r227 8873) (not b1168) ) :assumption (or (< (+ r224 r390) 8873) (not b1168) ) :assumption (or b70 (not b1168) ) :assumption (or (= r230 8873) (not b1169) ) :assumption (or (< (+ r227 r390) 8873) (not b1169) ) :assumption (or b75 (not b1169) ) :assumption (or (= r233 8873) (not b1170) ) :assumption (or (< (+ r230 r390) 8873) (not b1170) ) :assumption (or b79 (not b1170) ) :assumption (or (= r392 8873) (not b1171) ) :assumption (or (< (+ r233 r390) 8873) (not b1171) ) :assumption (or b147 (not b1171) ) :assumption (or (not b1172) (= r224 8873) ) :assumption (or (not b1172) (< (+ r12 r390) 8873) ) :assumption (or (= r227 8873) (not b1175) ) :assumption (or (< (+ r224 r390) 8873) (not b1175) ) :assumption (or b229 (not b1175) ) :assumption (or (= r230 8873) (not b1176) ) :assumption (or (< (+ r227 r390) 8873) (not b1176) ) :assumption (or b233 (not b1176) ) :assumption (or (= r233 8873) (not b1177) ) :assumption (or (< (+ r230 r390) 8873) (not b1177) ) :assumption (or b84 (not b1177) ) :assumption (or (= r392 8873) (not b1178) ) :assumption (or (< (+ r233 r390) 8873) (not b1178) ) :assumption (or b88 (not b1178) ) :assumption (or (or (or (or b229 b790 ) b816 ) b1081 ) b1108 ) :assumption (or (or (or (or (or b229 (not b233) ) b721 ) b766 ) b1013 ) b1057 ) :assumption (or (or (or (or (or (not b229) b233 ) b796 ) b822 ) b1088 ) b1114 ) :assumption (or (or (or (or (or (not b84) b233 ) b727 ) b772 ) b1019 ) b1063 ) :assumption (or (or (or (or (or b84 (not b233) ) b801 ) b827 ) b1093 ) b1119 ) :assumption (or (or (or (or (or b84 (not b88) ) b733 ) b778 ) b1025 ) b1069 ) :assumption (or (or (or (or (or (not b84) b88 ) b806 ) b832 ) b1098 ) b1124 ) :assumption (or (or (or (or (or b88 b739 ) (not b743) ) b784 ) b1031 ) b1075 ) :assumption (or (or (or (or (or (not b88) b743 ) b811 ) b837 ) b1103 ) b1129 ) :assumption (or (or (not b70) b816 ) b1108 ) :assumption (or (or (or (or (or b70 (not b75) ) b695 ) b822 ) b985 ) b1114 ) :assumption (or (or (or (or (or (not b70) b75 ) b746 ) b766 ) b1037 ) b1057 ) :assumption (or (or (or (or (or b75 (not b79) ) b701 ) b827 ) b992 ) b1119 ) :assumption (or (or (or (or (or (not b75) b79 ) b751 ) b772 ) b1042 ) b1063 ) :assumption (or (or (or (or (or b79 (not b147) ) b707 ) b832 ) b999 ) b1124 ) :assumption (or (or (or (or (or (not b79) b147 ) b756 ) b778 ) b1047 ) b1069 ) :assumption (or (or (or (or (or b147 b713 ) (not b717) ) b837 ) b1006 ) b1129 ) :assumption (or (or (or (or (or (not b147) b717 ) b761 ) b784 ) b1052 ) b1075 ) :assumption (or (or (not b456) b790 ) b1081 ) :assumption (or (or (or (or (or (not b203) b456 ) b746 ) b796 ) b1037 ) b1088 ) :assumption (or (or (or (or (or b203 (not b456) ) b695 ) b721 ) b985 ) b1013 ) :assumption (or (or (or (or (or (not b60) b203 ) b751 ) b801 ) b1042 ) b1093 ) :assumption (or (or (or (or (or b60 (not b203) ) b701 ) b727 ) b992 ) b1019 ) :assumption (or (or (or (or (or b60 (not b65) ) b756 ) b806 ) b1047 ) b1098 ) :assumption (or (or (or (or (or (not b60) b65 ) b707 ) b733 ) b999 ) b1025 ) :assumption (or (or (or (or (or b65 (not b718) ) b761 ) b811 ) b1052 ) b1103 ) :assumption (or (or (or (or (or (not b65) b713 ) b718 ) b739 ) b1006 ) b1031 ) :assumption (or (or (not b188) b582 ) b872 ) :assumption (or (or (or (or (or b188 (not b193) ) b588 ) b630 ) b878 ) b920 ) :assumption (or (or (or (or (or (not b188) b193 ) b654 ) b675 ) b944 ) b965 ) :assumption (or (or (or (or (or (not b50) b193 ) b594 ) b636 ) b884 ) b926 ) :assumption (or (or (or (or (or b50 (not b193) ) b659 ) b680 ) b949 ) b970 ) :assumption (or (or (or (or (or b50 (not b55) ) b600 ) b642 ) b890 ) b932 ) :assumption (or (or (or (or (or (not b50) b55 ) b664 ) b685 ) b954 ) b975 ) :assumption (or (or (or b55 (not b607) ) b648 ) b938 ) :assumption (or (or (or (or (or (not b55) b607 ) b669 ) b690 ) b959 ) b980 ) :assumption (or (or (not b32) b554 ) b842 ) :assumption (or (or (or (or (or b32 (not b38) ) b561 ) b675 ) b849 ) b965 ) :assumption (or (or (or (or (or (not b32) b38 ) b609 ) b630 ) b898 ) b920 ) :assumption (or (or (or (or (or b38 (not b43) ) b567 ) b680 ) b856 ) b970 ) :assumption (or (or (or (or (or (not b38) b43 ) b614 ) b636 ) b903 ) b926 ) :assumption (or (or (or (or (or b43 (not b118) ) b573 ) b685 ) b863 ) b975 ) :assumption (or (or (or (or (or (not b43) b118 ) b619 ) b642 ) b908 ) b932 ) :assumption (or (or (or b118 (not b580) ) b690 ) b980 ) :assumption (or (or (or (or (or (not b118) b580 ) b624 ) b648 ) b913 ) b938 ) :assumption (or (or (or (or b554 b558 ) b582 ) b842 ) b872 ) :assumption (or (or (or (or (or (not b158) b558 ) b609 ) b654 ) b898 ) b944 ) :assumption (or (or (or (or (or b158 (not b558) ) b561 ) b588 ) b849 ) b878 ) :assumption (or (or (or (or (or (not b20) b158 ) b614 ) b659 ) b903 ) b949 ) :assumption (or (or (or (or (or b20 (not b158) ) b567 ) b594 ) b856 ) b884 ) :assumption (or (or (or (or (or b20 (not b26) ) b619 ) b664 ) b908 ) b954 ) :assumption (or (or (or (or (or (not b20) b26 ) b573 ) b600 ) b863 ) b890 ) :assumption (or (or (or (or b26 b624 ) b669 ) b913 ) b959 ) :assumption (or b269 b302 ) :assumption (or (or (not b268) b269 ) b542 ) :assumption (or (or (or b265 b268 ) (not b269) ) b306 ) :assumption (or (or (or b268 (not b273) ) b509 ) b545 ) :assumption (or (or (or (not b268) b271 ) b273 ) b310 ) :assumption (or (or (or b273 (not b277) ) b512 ) b548 ) :assumption (or (or (or (not b273) b275 ) b277 ) b313 ) :assumption (or (or (or b277 (not b281) ) b515 ) b551 ) :assumption (or (or (or (not b277) b279 ) b281 ) b316 ) :assumption (or (not b258) b530 ) :assumption (or (or (or (not b257) b258 ) b500 ) b533 ) :assumption (or (or (or b255 b257 ) (not b258) ) b295 ) :assumption (or (or (or b257 (not b262) ) b503 ) b536 ) :assumption (or (or (or (not b257) b260 ) b262 ) b298 ) :assumption (or (or b262 b506 ) b539 ) :assumption (or (not b243) b518 ) :assumption (or (or (or (not b242) b243 ) b491 ) b521 ) :assumption (or (or (or b239 b242 ) (not b243) ) b283 ) :assumption (or (or (or b242 (not b248) ) b494 ) b524 ) :assumption (or (or (or (not b242) b245 ) b248 ) b287 ) :assumption (or (or (or b248 (not b253) ) b497 ) b527 ) :assumption (or (or (or (not b248) b250 ) b253 ) b291 ) :assumption (or b187 b222 ) :assumption (or (or (not b186) b187 ) b479 ) :assumption (or (or (or b183 b186 ) (not b187) ) b226 ) :assumption (or (or (or b186 (not b192) ) b445 ) b482 ) :assumption (or (or (or (not b186) b190 ) b192 ) b231 ) :assumption (or (or (or b192 (not b197) ) b448 ) b485 ) :assumption (or (or (or (not b192) b195 ) b197 ) b235 ) :assumption (or (or b197 b451 ) b488 ) :assumption (or (not b173) b467 ) :assumption (or (or (or (not b172) b173 ) b436 ) b470 ) :assumption (or (or (or b170 b172 ) (not b173) ) b213 ) :assumption (or (or (or b172 (not b177) ) b439 ) b473 ) :assumption (or (or (or (not b172) b175 ) b177 ) b216 ) :assumption (or (or (or b177 (not b181) ) b442 ) b476 ) :assumption (or (or (or (not b177) b179 ) b181 ) b219 ) :assumption (or (not b157) b454 ) :assumption (or (or (or (not b156) b157 ) b427 ) b458 ) :assumption (or (or (or b153 b156 ) (not b157) ) b200 ) :assumption (or (or (or b156 (not b163) ) b430 ) b461 ) :assumption (or (or (or (not b156) b160 ) b163 ) b205 ) :assumption (or (or (or b163 (not b168) ) b433 ) b464 ) :assumption (or (or (or (not b163) b165 ) b168 ) b209 ) :assumption (or (or (not b123) b391 ) b418 ) :assumption (or (or (or (not b122) b123 ) b394 ) b421 ) :assumption (or (or (or b120 b122 ) (not b123) ) b149 ) :assumption (or (or b122 b397 ) b424 ) :assumption (or (or b101 b104 ) b134 ) :assumption (or (or (or b104 (not b109) ) b382 ) b409 ) :assumption (or (or (or (not b104) b106 ) b109 ) b138 ) :assumption (or (or (or b109 (not b113) ) b385 ) b412 ) :assumption (or (or (or (not b109) b111 ) b113 ) b142 ) :assumption (or (or (or b113 (not b117) ) b388 ) b415 ) :assumption (or (or (or (not b113) b115 ) b117 ) b145 ) :assumption (or (or (not b94) b373 ) b400 ) :assumption (or (or (or (not b93) b94 ) b376 ) b403 ) :assumption (or (or (or b90 b93 ) (not b94) ) b126 ) :assumption (or (or (or b93 (not b99) ) b379 ) b406 ) :assumption (or (or (or (not b93) b96 ) b99 ) b130 ) :assumption (or (or (not b49) b337 ) b364 ) :assumption (or (or (or (not b48) b49 ) b340 ) b367 ) :assumption (or (or (or b46 b48 ) (not b49) ) b82 ) :assumption (or (or (or b48 (not b54) ) b343 ) b370 ) :assumption (or (or (or (not b48) b52 ) b54 ) b86 ) :assumption (or (or b28 b31 ) b67 ) :assumption (or (or (or b31 (not b37) ) b328 ) b355 ) :assumption (or (or (or (not b31) b34 ) b37 ) b72 ) :assumption (or (or (or b37 (not b42) ) b331 ) b358 ) :assumption (or (or (or (not b37) b40 ) b42 ) b77 ) :assumption (or (or b42 b334 ) b361 ) :assumption (or (or (not b19) b319 ) b346 ) :assumption (or (or (or (not b18) b19 ) b322 ) b349 ) :assumption (or (or (or b15 b18 ) (not b19) ) b57 ) :assumption (or (or (or b18 (not b25) ) b325 ) b352 ) :assumption (or (or (or (not b18) b22 ) b25 ) b62 ) :assumption (or b302 (not b304) ) :assumption (or (or b304 b306 ) (not b308) ) :assumption (or (or (or (or (not b304) b308 ) b518 ) b530 ) b542 ) :assumption (or (or (or (or b283 (not b285) ) b295 ) b308 ) b310 ) :assumption (or (or (or (or b285 (not b308) ) b521 ) b533 ) b545 ) :assumption (or (or (or (or b285 b287 ) (not b289) ) b298 ) b313 ) :assumption (or (or (or (or (not b285) b289 ) b524 ) b536 ) b548 ) :assumption (or (or (or b289 b291 ) (not b293) ) b316 ) :assumption (or (or (or (or (not b289) b293 ) b527 ) b539 ) b551 ) :assumption (or b265 (not b267) ) :assumption (or (or (or (or b239 (not b241) ) b255 ) b267 ) b271 ) :assumption (or (or (or (or b241 (not b267) ) b491 ) b500 ) b509 ) :assumption (or (or (or (or b241 b245 ) (not b247) ) b260 ) b275 ) :assumption (or (or (or (or (not b241) b247 ) b494 ) b503 ) b512 ) :assumption (or (or (or b247 b250 ) (not b252) ) b279 ) :assumption (or (or (or (or (not b247) b252 ) b497 ) b506 ) b515 ) :assumption (or b222 (not b224) ) :assumption (or (or b224 b226 ) (not b228) ) :assumption (or (or (or (or (not b224) b228 ) b454 ) b467 ) b479 ) :assumption (or (or (or (or b200 (not b202) ) b213 ) b228 ) b231 ) :assumption (or (or (or (or b202 (not b228) ) b458 ) b470 ) b482 ) :assumption (or (or (or (or b202 b205 ) (not b207) ) b216 ) b235 ) :assumption (or (or (or (or (not b202) b207 ) b461 ) b473 ) b485 ) :assumption (or (or (or b207 b209 ) (not b211) ) b219 ) :assumption (or (or (or (or (not b207) b211 ) b464 ) b476 ) b488 ) :assumption (or b183 (not b185) ) :assumption (or (or (or (or b153 (not b155) ) b170 ) b185 ) b190 ) :assumption (or (or (or (or b155 (not b185) ) b427 ) b436 ) b445 ) :assumption (or (or (or (or b155 b160 ) (not b162) ) b175 ) b195 ) :assumption (or (or (or (or (not b155) b162 ) b430 ) b439 ) b448 ) :assumption (or (or (or b162 b165 ) (not b167) ) b179 ) :assumption (or (or (or (or (not b162) b167 ) b433 ) b442 ) b451 ) :assumption (or b134 (not b136) ) :assumption (or (or b136 b138 ) (not b140) ) :assumption (or (or (or (or (not b136) b140 ) b400 ) b409 ) b418 ) :assumption (or (or (or (or b126 (not b128) ) b140 ) b142 ) b149 ) :assumption (or (or (or (or b128 (not b140) ) b403 ) b412 ) b421 ) :assumption (or (or (or b128 b130 ) (not b132) ) b145 ) :assumption (or (or (or (or (not b128) b132 ) b406 ) b415 ) b424 ) :assumption (or b101 (not b103) ) :assumption (or (or b103 b106 ) (not b108) ) :assumption (or (or (or (or (not b103) b108 ) b373 ) b382 ) b391 ) :assumption (or (or (or (or b90 (not b92) ) b108 ) b111 ) b120 ) :assumption (or (or (or (or b92 (not b108) ) b376 ) b385 ) b394 ) :assumption (or (or (or b92 b96 ) (not b98) ) b115 ) :assumption (or (or (or (or (not b92) b98 ) b379 ) b388 ) b397 ) :assumption (or b67 (not b69) ) :assumption (or (or b69 b72 ) (not b74) ) :assumption (or (or (or (or (not b69) b74 ) b346 ) b355 ) b364 ) :assumption (or (or (or (or b57 (not b59) ) b74 ) b77 ) b82 ) :assumption (or (or (or (or b59 (not b74) ) b349 ) b358 ) b367 ) :assumption (or (or (or b59 b62 ) (not b64) ) b86 ) :assumption (or (or (or (or (not b59) b64 ) b352 ) b361 ) b370 ) :assumption (or b28 (not b30) ) :assumption (or (or b30 b34 ) (not b36) ) :assumption (or (or (or (or (not b30) b36 ) b319 ) b328 ) b337 ) :assumption (or (or (or (or b15 (not b17) ) b36 ) b40 ) b46 ) :assumption (or (or (or (or b17 (not b36) ) b322 ) b331 ) b340 ) :assumption (or (or (or b17 b22 ) (not b24) ) b52 ) :assumption (or (or (or (or (not b17) b24 ) b325 ) b334 ) b343 ) :assumption (or b1133 (= (- (- (- (- (- r170 r10) r292) r279) r180) r167) 0) ) :assumption (or (or (or b1136 b1148 ) b1152 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r173 r170) r327) r319) r311) r302) r294) r281) r215) r207) r199) r190) r182) r169) 0) ) :assumption (or (or (or b1139 b1149 ) b1153 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r176 r173) r329) r321) r313) r304) r296) r284) r217) r209) r201) r192) r184) r172) 0) ) :assumption (or (or (or b1142 b1150 ) b1154 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r197 r176) r331) r323) r315) r306) r298) r287) r219) r211) r203) r194) r186) r175) 0) ) :assumption (or (or (or b1145 b1151 ) b1155 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r391 r197) r333) r325) r317) r308) r300) r290) r221) r213) r205) r196) r188) r178) 0) ) :assumption (or b1172 (= (- (- (- (- (- r224 r12) r381) r371) r269) r259) 0) ) :assumption (or (or (or b1156 b1168 ) b1175 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r227 r224) r383) r373) r363) r355) r347) r335) r271) r261) r251) r243) r235) r223) 0) ) :assumption (or (or (or b1159 b1169 ) b1176 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r230 r227) r385) r375) r365) r357) r349) r338) r273) r263) r253) r245) r237) r226) 0) ) :assumption (or (or (or b1162 b1170 ) b1177 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r233 r230) r387) r377) r367) r359) r351) r341) r275) r265) r255) r247) r239) r229) 0) ) :assumption (or (or (or b1165 b1171 ) b1178 ) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r392 r233) r389) r379) r369) r361) r353) r344) r277) r267) r257) r249) r241) r232) 0) ) :assumption (or (not b15) (not b57) ) :assumption (or (not b22) (not b62) ) :assumption (or (not b15) (not b349) ) :assumption (or (not b22) (not b352) ) :assumption (or (not b15) (not b322) ) :assumption (or (not b22) (not b325) ) :assumption (or (not b15) (not b340) ) :assumption (or (not b22) (not b343) ) :assumption (or (not b15) (not b331) ) :assumption (or (not b22) (not b334) ) :assumption (or (not b15) (not b975) ) :assumption (or (not b22) (not b980) ) :assumption (or (not b15) (not b954) ) :assumption (or (not b22) (not b959) ) :assumption (or (not b15) (not b932) ) :assumption (or (not b22) (not b938) ) :assumption (or (not b15) (not b908) ) :assumption (or (not b22) (not b913) ) :assumption (or (not b15) (not b890) ) :assumption (or (not b15) (not b863) ) :assumption (or (not b28) (not b67) ) :assumption (or (not b34) (not b72) ) :assumption (or (not b40) (not b77) ) :assumption (or (not b34) (not b355) ) :assumption (or (not b40) (not b358) ) :assumption (or (not b34) (not b328) ) :assumption (or (not b40) (not b331) ) :assumption (or (not b34) (not b337) ) :assumption (or (not b40) (not b340) ) :assumption (or (not b34) (not b319) ) :assumption (or (not b40) (not b322) ) :assumption (or (not b28) (not b965) ) :assumption (or (not b34) (not b970) ) :assumption (or (not b40) (not b975) ) :assumption (or (not b28) (not b944) ) :assumption (or (not b34) (not b949) ) :assumption (or (not b40) (not b954) ) :assumption (or (not b28) (not b920) ) :assumption (or (not b34) (not b926) ) :assumption (or (not b40) (not b932) ) :assumption (or (not b28) (not b898) ) :assumption (or (not b34) (not b903) ) :assumption (or (not b40) (not b908) ) :assumption (or (not b28) (not b878) ) :assumption (or (not b34) (not b884) ) :assumption (or (not b40) (not b890) ) :assumption (or (not b28) (not b849) ) :assumption (or (not b34) (not b856) ) :assumption (or (not b40) (not b863) ) :assumption (or (not b46) (not b82) ) :assumption (or (not b52) (not b86) ) :assumption (or (not b46) (not b367) ) :assumption (or (not b52) (not b370) ) :assumption (or (not b46) (not b340) ) :assumption (or (not b52) (not b343) ) :assumption (or (not b46) (not b331) ) :assumption (or (not b52) (not b334) ) :assumption (or (not b46) (not b322) ) :assumption (or (not b52) (not b325) ) :assumption (or (not b46) (not b975) ) :assumption (or (not b52) (not b980) ) :assumption (or (not b46) (not b954) ) :assumption (or (not b52) (not b959) ) :assumption (or (not b46) (not b932) ) :assumption (or (not b52) (not b938) ) :assumption (or (not b46) (not b908) ) :assumption (or (not b52) (not b913) ) :assumption (or (not b46) (not b890) ) :assumption (or (not b46) (not b863) ) :assumption (or (not b57) (not b349) ) :assumption (or (not b62) (not b352) ) :assumption (or (not b57) (not b322) ) :assumption (or (not b62) (not b325) ) :assumption (or (not b57) (not b367) ) :assumption (or (not b62) (not b370) ) :assumption (or (not b57) (not b358) ) :assumption (or (not b62) (not b361) ) :assumption (or (not b57) (not b1124) ) :assumption (or (not b62) (not b1129) ) :assumption (or (not b57) (not b1098) ) :assumption (or (not b62) (not b1103) ) :assumption (or (not b57) (not b1069) ) :assumption (or (not b62) (not b1075) ) :assumption (or (not b57) (not b1047) ) :assumption (or (not b62) (not b1052) ) :assumption (or (not b57) (not b1025) ) :assumption (or (not b62) (not b1031) ) :assumption (or (not b57) (not b999) ) :assumption (or (not b62) (not b1006) ) :assumption (or (not b72) (not b355) ) :assumption (or (not b77) (not b358) ) :assumption (or (not b72) (not b328) ) :assumption (or (not b77) (not b331) ) :assumption (or (not b72) (not b364) ) :assumption (or (not b77) (not b367) ) :assumption (or (not b72) (not b346) ) :assumption (or (not b77) (not b349) ) :assumption (or (not b67) (not b1114) ) :assumption (or (not b72) (not b1119) ) :assumption (or (not b77) (not b1124) ) :assumption (or (not b67) (not b1088) ) :assumption (or (not b72) (not b1093) ) :assumption (or (not b77) (not b1098) ) :assumption (or (not b67) (not b1057) ) :assumption (or (not b72) (not b1063) ) :assumption (or (not b77) (not b1069) ) :assumption (or (not b67) (not b1037) ) :assumption (or (not b72) (not b1042) ) :assumption (or (not b77) (not b1047) ) :assumption (or (not b67) (not b1013) ) :assumption (or (not b72) (not b1019) ) :assumption (or (not b77) (not b1025) ) :assumption (or (not b67) (not b985) ) :assumption (or (not b72) (not b992) ) :assumption (or (not b77) (not b999) ) :assumption (or (not b82) (not b367) ) :assumption (or (not b86) (not b370) ) :assumption (or (not b82) (not b340) ) :assumption (or (not b86) (not b343) ) :assumption (or (not b82) (not b358) ) :assumption (or (not b86) (not b361) ) :assumption (or (not b82) (not b349) ) :assumption (or (not b86) (not b352) ) :assumption (or (not b82) (not b1124) ) :assumption (or (not b86) (not b1129) ) :assumption (or (not b82) (not b1098) ) :assumption (or (not b86) (not b1103) ) :assumption (or (not b82) (not b1069) ) :assumption (or (not b86) (not b1075) ) :assumption (or (not b82) (not b1047) ) :assumption (or (not b86) (not b1052) ) :assumption (or (not b82) (not b1025) ) :assumption (or (not b86) (not b1031) ) :assumption (or (not b82) (not b999) ) :assumption (or (not b86) (not b1006) ) :assumption (or (not b90) (not b126) ) :assumption (or (not b96) (not b130) ) :assumption (or (not b90) (not b403) ) :assumption (or (not b96) (not b406) ) :assumption (or (not b90) (not b376) ) :assumption (or (not b96) (not b379) ) :assumption (or (not b90) (not b394) ) :assumption (or (not b96) (not b397) ) :assumption (or (not b90) (not b385) ) :assumption (or (not b96) (not b388) ) :assumption (or (not b90) (not b975) ) :assumption (or (not b96) (not b980) ) :assumption (or (not b90) (not b954) ) :assumption (or (not b96) (not b959) ) :assumption (or (not b90) (not b932) ) :assumption (or (not b96) (not b938) ) :assumption (or (not b90) (not b908) ) :assumption (or (not b96) (not b913) ) :assumption (or (not b90) (not b890) ) :assumption (or (not b90) (not b863) ) :assumption (or (not b101) (not b134) ) :assumption (or (not b106) (not b138) ) :assumption (or (not b111) (not b142) ) :assumption (or (not b115) (not b145) ) :assumption (or (not b106) (not b409) ) :assumption (or (not b111) (not b412) ) :assumption (or (not b115) (not b415) ) :assumption (or (not b106) (not b382) ) :assumption (or (not b111) (not b385) ) :assumption (or (not b115) (not b388) ) :assumption (or (not b106) (not b391) ) :assumption (or (not b111) (not b394) ) :assumption (or (not b115) (not b397) ) :assumption (or (not b106) (not b373) ) :assumption (or (not b111) (not b376) ) :assumption (or (not b115) (not b379) ) :assumption (or (not b101) (not b965) ) :assumption (or (not b106) (not b970) ) :assumption (or (not b111) (not b975) ) :assumption (or (not b115) (not b980) ) :assumption (or (not b101) (not b944) ) :assumption (or (not b106) (not b949) ) :assumption (or (not b111) (not b954) ) :assumption (or (not b115) (not b959) ) :assumption (or (not b101) (not b920) ) :assumption (or (not b106) (not b926) ) :assumption (or (not b111) (not b932) ) :assumption (or (not b115) (not b938) ) :assumption (or (not b101) (not b898) ) :assumption (or (not b106) (not b903) ) :assumption (or (not b111) (not b908) ) :assumption (or (not b115) (not b913) ) :assumption (or (not b101) (not b878) ) :assumption (or (not b106) (not b884) ) :assumption (or (not b111) (not b890) ) :assumption (or (not b101) (not b849) ) :assumption (or (not b106) (not b856) ) :assumption (or (not b111) (not b863) ) :assumption (or (not b120) (not b149) ) :assumption (or (not b120) (not b421) ) :assumption (or (not b120) (not b394) ) :assumption (or (not b120) (not b385) ) :assumption (or (not b120) (not b376) ) :assumption (or (not b120) (not b975) ) :assumption (or (not b120) (not b954) ) :assumption (or (not b120) (not b932) ) :assumption (or (not b120) (not b908) ) :assumption (or (not b120) (not b890) ) :assumption (or (not b120) (not b863) ) :assumption (or (not b126) (not b403) ) :assumption (or (not b130) (not b406) ) :assumption (or (not b126) (not b376) ) :assumption (or (not b130) (not b379) ) :assumption (or (not b126) (not b421) ) :assumption (or (not b130) (not b424) ) :assumption (or (not b126) (not b412) ) :assumption (or (not b130) (not b415) ) :assumption (or (not b126) (not b1124) ) :assumption (or (not b130) (not b1129) ) :assumption (or (not b126) (not b1098) ) :assumption (or (not b130) (not b1103) ) :assumption (or (not b126) (not b1069) ) :assumption (or (not b130) (not b1075) ) :assumption (or (not b126) (not b1047) ) :assumption (or (not b130) (not b1052) ) :assumption (or (not b126) (not b1025) ) :assumption (or (not b130) (not b1031) ) :assumption (or (not b126) (not b999) ) :assumption (or (not b130) (not b1006) ) :assumption (or (not b138) (not b409) ) :assumption (or (not b142) (not b412) ) :assumption (or (not b145) (not b415) ) :assumption (or (not b138) (not b382) ) :assumption (or (not b142) (not b385) ) :assumption (or (not b145) (not b388) ) :assumption (or (not b138) (not b418) ) :assumption (or (not b142) (not b421) ) :assumption (or (not b145) (not b424) ) :assumption (or (not b138) (not b400) ) :assumption (or (not b142) (not b403) ) :assumption (or (not b145) (not b406) ) :assumption (or (not b134) (not b1114) ) :assumption (or (not b138) (not b1119) ) :assumption (or (not b142) (not b1124) ) :assumption (or (not b145) (not b1129) ) :assumption (or (not b134) (not b1088) ) :assumption (or (not b138) (not b1093) ) :assumption (or (not b142) (not b1098) ) :assumption (or (not b145) (not b1103) ) :assumption (or (not b134) (not b1057) ) :assumption (or (not b138) (not b1063) ) :assumption (or (not b142) (not b1069) ) :assumption (or (not b145) (not b1075) ) :assumption (or (not b134) (not b1037) ) :assumption (or (not b138) (not b1042) ) :assumption (or (not b142) (not b1047) ) :assumption (or (not b145) (not b1052) ) :assumption (or (not b134) (not b1013) ) :assumption (or (not b138) (not b1019) ) :assumption (or (not b142) (not b1025) ) :assumption (or (not b145) (not b1031) ) :assumption (or (not b134) (not b985) ) :assumption (or (not b138) (not b992) ) :assumption (or (not b142) (not b999) ) :assumption (or (not b145) (not b1006) ) :assumption (or (not b149) (not b421) ) :assumption (or (not b149) (not b394) ) :assumption (or (not b149) (not b412) ) :assumption (or (not b149) (not b403) ) :assumption (or (not b149) (not b1124) ) :assumption (or (not b149) (not b1098) ) :assumption (or (not b149) (not b1069) ) :assumption (or (not b149) (not b1047) ) :assumption (or (not b149) (not b1025) ) :assumption (or (not b149) (not b999) ) :assumption (or (not b153) (not b200) ) :assumption (or (not b160) (not b205) ) :assumption (or (not b165) (not b209) ) :assumption (or (not b153) (not b458) ) :assumption (or (not b160) (not b461) ) :assumption (or (not b165) (not b464) ) :assumption (or (not b153) (not b427) ) :assumption (or (not b160) (not b430) ) :assumption (or (not b165) (not b433) ) :assumption (or (not b153) (not b445) ) :assumption (or (not b160) (not b448) ) :assumption (or (not b165) (not b451) ) :assumption (or (not b153) (not b436) ) :assumption (or (not b160) (not b439) ) :assumption (or (not b165) (not b442) ) :assumption (or (not b153) (not b970) ) :assumption (or (not b160) (not b975) ) :assumption (or (not b165) (not b980) ) :assumption (or (not b153) (not b949) ) :assumption (or (not b160) (not b954) ) :assumption (or (not b165) (not b959) ) :assumption (or (not b153) (not b926) ) :assumption (or (not b160) (not b932) ) :assumption (or (not b165) (not b938) ) :assumption (or (not b153) (not b903) ) :assumption (or (not b160) (not b908) ) :assumption (or (not b165) (not b913) ) :assumption (or (not b153) (not b884) ) :assumption (or (not b160) (not b890) ) :assumption (or (not b153) (not b856) ) :assumption (or (not b160) (not b863) ) :assumption (or (not b170) (not b213) ) :assumption (or (not b175) (not b216) ) :assumption (or (not b179) (not b219) ) :assumption (or (not b170) (not b470) ) :assumption (or (not b175) (not b473) ) :assumption (or (not b179) (not b476) ) :assumption (or (not b170) (not b436) ) :assumption (or (not b175) (not b439) ) :assumption (or (not b179) (not b442) ) :assumption (or (not b170) (not b445) ) :assumption (or (not b175) (not b448) ) :assumption (or (not b179) (not b451) ) :assumption (or (not b170) (not b427) ) :assumption (or (not b175) (not b430) ) :assumption (or (not b179) (not b433) ) :assumption (or (not b170) (not b970) ) :assumption (or (not b175) (not b975) ) :assumption (or (not b179) (not b980) ) :assumption (or (not b170) (not b949) ) :assumption (or (not b175) (not b954) ) :assumption (or (not b179) (not b959) ) :assumption (or (not b170) (not b926) ) :assumption (or (not b175) (not b932) ) :assumption (or (not b179) (not b938) ) :assumption (or (not b170) (not b903) ) :assumption (or (not b175) (not b908) ) :assumption (or (not b179) (not b913) ) :assumption (or (not b170) (not b884) ) :assumption (or (not b175) (not b890) ) :assumption (or (not b170) (not b856) ) :assumption (or (not b175) (not b863) ) :assumption (or (not b183) (not b226) ) :assumption (or (not b190) (not b231) ) :assumption (or (not b195) (not b235) ) :assumption (or (not b183) (not b479) ) :assumption (or (not b190) (not b482) ) :assumption (or (not b195) (not b485) ) :assumption (or (not b190) (not b445) ) :assumption (or (not b195) (not b448) ) :assumption (or (not b190) (not b436) ) :assumption (or (not b195) (not b439) ) :assumption (or (not b190) (not b427) ) :assumption (or (not b195) (not b430) ) :assumption (or (not b183) (not b965) ) :assumption (or (not b190) (not b970) ) :assumption (or (not b195) (not b975) ) :assumption (or (not b183) (not b944) ) :assumption (or (not b190) (not b949) ) :assumption (or (not b195) (not b954) ) :assumption (or (not b183) (not b920) ) :assumption (or (not b190) (not b926) ) :assumption (or (not b195) (not b932) ) :assumption (or (not b183) (not b898) ) :assumption (or (not b190) (not b903) ) :assumption (or (not b195) (not b908) ) :assumption (or (not b183) (not b878) ) :assumption (or (not b190) (not b884) ) :assumption (or (not b195) (not b890) ) :assumption (or (not b183) (not b849) ) :assumption (or (not b190) (not b856) ) :assumption (or (not b195) (not b863) ) :assumption (or (not b200) (not b458) ) :assumption (or (not b205) (not b461) ) :assumption (or (not b209) (not b464) ) :assumption (or (not b200) (not b427) ) :assumption (or (not b205) (not b430) ) :assumption (or (not b209) (not b433) ) :assumption (or (not b200) (not b482) ) :assumption (or (not b205) (not b485) ) :assumption (or (not b209) (not b488) ) :assumption (or (not b200) (not b470) ) :assumption (or (not b205) (not b473) ) :assumption (or (not b209) (not b476) ) :assumption (or (not b200) (not b1119) ) :assumption (or (not b205) (not b1124) ) :assumption (or (not b209) (not b1129) ) :assumption (or (not b200) (not b1093) ) :assumption (or (not b205) (not b1098) ) :assumption (or (not b209) (not b1103) ) :assumption (or (not b200) (not b1063) ) :assumption (or (not b205) (not b1069) ) :assumption (or (not b209) (not b1075) ) :assumption (or (not b200) (not b1042) ) :assumption (or (not b205) (not b1047) ) :assumption (or (not b209) (not b1052) ) :assumption (or (not b200) (not b1019) ) :assumption (or (not b205) (not b1025) ) :assumption (or (not b209) (not b1031) ) :assumption (or (not b200) (not b992) ) :assumption (or (not b205) (not b999) ) :assumption (or (not b209) (not b1006) ) :assumption (or (not b213) (not b470) ) :assumption (or (not b216) (not b473) ) :assumption (or (not b219) (not b476) ) :assumption (or (not b213) (not b436) ) :assumption (or (not b216) (not b439) ) :assumption (or (not b219) (not b442) ) :assumption (or (not b213) (not b482) ) :assumption (or (not b216) (not b485) ) :assumption (or (not b219) (not b488) ) :assumption (or (not b213) (not b458) ) :assumption (or (not b216) (not b461) ) :assumption (or (not b219) (not b464) ) :assumption (or (not b213) (not b1119) ) :assumption (or (not b216) (not b1124) ) :assumption (or (not b219) (not b1129) ) :assumption (or (not b213) (not b1093) ) :assumption (or (not b216) (not b1098) ) :assumption (or (not b219) (not b1103) ) :assumption (or (not b213) (not b1063) ) :assumption (or (not b216) (not b1069) ) :assumption (or (not b219) (not b1075) ) :assumption (or (not b213) (not b1042) ) :assumption (or (not b216) (not b1047) ) :assumption (or (not b219) (not b1052) ) :assumption (or (not b213) (not b1019) ) :assumption (or (not b216) (not b1025) ) :assumption (or (not b219) (not b1031) ) :assumption (or (not b213) (not b992) ) :assumption (or (not b216) (not b999) ) :assumption (or (not b219) (not b1006) ) :assumption (or (not b226) (not b479) ) :assumption (or (not b231) (not b482) ) :assumption (or (not b235) (not b485) ) :assumption (or (not b231) (not b445) ) :assumption (or (not b235) (not b448) ) :assumption (or (not b226) (not b467) ) :assumption (or (not b231) (not b470) ) :assumption (or (not b235) (not b473) ) :assumption (or (not b226) (not b454) ) :assumption (or (not b231) (not b458) ) :assumption (or (not b235) (not b461) ) :assumption (or (not b222) (not b1108) ) :assumption (or (not b226) (not b1114) ) :assumption (or (not b231) (not b1119) ) :assumption (or (not b235) (not b1124) ) :assumption (or (not b222) (not b1081) ) :assumption (or (not b226) (not b1088) ) :assumption (or (not b231) (not b1093) ) :assumption (or (not b235) (not b1098) ) :assumption (or (not b226) (not b1057) ) :assumption (or (not b231) (not b1063) ) :assumption (or (not b235) (not b1069) ) :assumption (or (not b226) (not b1037) ) :assumption (or (not b231) (not b1042) ) :assumption (or (not b235) (not b1047) ) :assumption (or (not b226) (not b1013) ) :assumption (or (not b231) (not b1019) ) :assumption (or (not b235) (not b1025) ) :assumption (or (not b226) (not b985) ) :assumption (or (not b231) (not b992) ) :assumption (or (not b235) (not b999) ) :assumption (or (not b239) (not b283) ) :assumption (or (not b245) (not b287) ) :assumption (or (not b250) (not b291) ) :assumption (or (not b239) (not b521) ) :assumption (or (not b245) (not b524) ) :assumption (or (not b250) (not b527) ) :assumption (or (not b239) (not b491) ) :assumption (or (not b245) (not b494) ) :assumption (or (not b250) (not b497) ) :assumption (or (not b239) (not b509) ) :assumption (or (not b245) (not b512) ) :assumption (or (not b250) (not b515) ) :assumption (or (not b239) (not b500) ) :assumption (or (not b245) (not b503) ) :assumption (or (not b250) (not b506) ) :assumption (or (not b239) (not b970) ) :assumption (or (not b245) (not b975) ) :assumption (or (not b250) (not b980) ) :assumption (or (not b239) (not b949) ) :assumption (or (not b245) (not b954) ) :assumption (or (not b250) (not b959) ) :assumption (or (not b239) (not b926) ) :assumption (or (not b245) (not b932) ) :assumption (or (not b250) (not b938) ) :assumption (or (not b239) (not b903) ) :assumption (or (not b245) (not b908) ) :assumption (or (not b250) (not b913) ) :assumption (or (not b239) (not b884) ) :assumption (or (not b245) (not b890) ) :assumption (or (not b239) (not b856) ) :assumption (or (not b245) (not b863) ) :assumption (or (not b255) (not b295) ) :assumption (or (not b260) (not b298) ) :assumption (or (not b255) (not b533) ) :assumption (or (not b260) (not b536) ) :assumption (or (not b255) (not b500) ) :assumption (or (not b260) (not b503) ) :assumption (or (not b255) (not b509) ) :assumption (or (not b260) (not b512) ) :assumption (or (not b255) (not b491) ) :assumption (or (not b260) (not b494) ) :assumption (or (not b255) (not b970) ) :assumption (or (not b260) (not b975) ) :assumption (or (not b255) (not b949) ) :assumption (or (not b260) (not b954) ) :assumption (or (not b255) (not b926) ) :assumption (or (not b260) (not b932) ) :assumption (or (not b255) (not b903) ) :assumption (or (not b260) (not b908) ) :assumption (or (not b255) (not b884) ) :assumption (or (not b260) (not b890) ) :assumption (or (not b255) (not b856) ) :assumption (or (not b260) (not b863) ) :assumption (or (not b265) (not b306) ) :assumption (or (not b271) (not b310) ) :assumption (or (not b275) (not b313) ) :assumption (or (not b279) (not b316) ) :assumption (or (not b265) (not b542) ) :assumption (or (not b271) (not b545) ) :assumption (or (not b275) (not b548) ) :assumption (or (not b279) (not b551) ) :assumption (or (not b271) (not b509) ) :assumption (or (not b275) (not b512) ) :assumption (or (not b279) (not b515) ) :assumption (or (not b271) (not b500) ) :assumption (or (not b275) (not b503) ) :assumption (or (not b279) (not b506) ) :assumption (or (not b271) (not b491) ) :assumption (or (not b275) (not b494) ) :assumption (or (not b279) (not b497) ) :assumption (or (not b265) (not b965) ) :assumption (or (not b271) (not b970) ) :assumption (or (not b275) (not b975) ) :assumption (or (not b279) (not b980) ) :assumption (or (not b265) (not b944) ) :assumption (or (not b271) (not b949) ) :assumption (or (not b275) (not b954) ) :assumption (or (not b279) (not b959) ) :assumption (or (not b265) (not b920) ) :assumption (or (not b271) (not b926) ) :assumption (or (not b275) (not b932) ) :assumption (or (not b279) (not b938) ) :assumption (or (not b265) (not b898) ) :assumption (or (not b271) (not b903) ) :assumption (or (not b275) (not b908) ) :assumption (or (not b279) (not b913) ) :assumption (or (not b265) (not b878) ) :assumption (or (not b271) (not b884) ) :assumption (or (not b275) (not b890) ) :assumption (or (not b265) (not b849) ) :assumption (or (not b271) (not b856) ) :assumption (or (not b275) (not b863) ) :assumption (or (not b283) (not b521) ) :assumption (or (not b287) (not b524) ) :assumption (or (not b291) (not b527) ) :assumption (or (not b283) (not b491) ) :assumption (or (not b287) (not b494) ) :assumption (or (not b291) (not b497) ) :assumption (or (not b283) (not b545) ) :assumption (or (not b287) (not b548) ) :assumption (or (not b291) (not b551) ) :assumption (or (not b283) (not b533) ) :assumption (or (not b287) (not b536) ) :assumption (or (not b291) (not b539) ) :assumption (or (not b283) (not b1119) ) :assumption (or (not b287) (not b1124) ) :assumption (or (not b291) (not b1129) ) :assumption (or (not b283) (not b1093) ) :assumption (or (not b287) (not b1098) ) :assumption (or (not b291) (not b1103) ) :assumption (or (not b283) (not b1063) ) :assumption (or (not b287) (not b1069) ) :assumption (or (not b291) (not b1075) ) :assumption (or (not b283) (not b1042) ) :assumption (or (not b287) (not b1047) ) :assumption (or (not b291) (not b1052) ) :assumption (or (not b283) (not b1019) ) :assumption (or (not b287) (not b1025) ) :assumption (or (not b291) (not b1031) ) :assumption (or (not b283) (not b992) ) :assumption (or (not b287) (not b999) ) :assumption (or (not b291) (not b1006) ) :assumption (or (not b295) (not b533) ) :assumption (or (not b298) (not b536) ) :assumption (or (not b295) (not b500) ) :assumption (or (not b298) (not b503) ) :assumption (or (not b295) (not b545) ) :assumption (or (not b298) (not b548) ) :assumption (or (not b295) (not b521) ) :assumption (or (not b298) (not b524) ) :assumption (or (not b295) (not b1119) ) :assumption (or (not b298) (not b1124) ) :assumption (or (not b295) (not b1093) ) :assumption (or (not b298) (not b1098) ) :assumption (or (not b295) (not b1063) ) :assumption (or (not b298) (not b1069) ) :assumption (or (not b295) (not b1042) ) :assumption (or (not b298) (not b1047) ) :assumption (or (not b295) (not b1019) ) :assumption (or (not b298) (not b1025) ) :assumption (or (not b295) (not b992) ) :assumption (or (not b298) (not b999) ) :assumption (or (not b306) (not b542) ) :assumption (or (not b310) (not b545) ) :assumption (or (not b313) (not b548) ) :assumption (or (not b316) (not b551) ) :assumption (or (not b310) (not b509) ) :assumption (or (not b313) (not b512) ) :assumption (or (not b316) (not b515) ) :assumption (or (not b306) (not b530) ) :assumption (or (not b310) (not b533) ) :assumption (or (not b313) (not b536) ) :assumption (or (not b316) (not b539) ) :assumption (or (not b306) (not b518) ) :assumption (or (not b310) (not b521) ) :assumption (or (not b313) (not b524) ) :assumption (or (not b316) (not b527) ) :assumption (or (not b302) (not b1108) ) :assumption (or (not b306) (not b1114) ) :assumption (or (not b310) (not b1119) ) :assumption (or (not b313) (not b1124) ) :assumption (or (not b316) (not b1129) ) :assumption (or (not b302) (not b1081) ) :assumption (or (not b306) (not b1088) ) :assumption (or (not b310) (not b1093) ) :assumption (or (not b313) (not b1098) ) :assumption (or (not b316) (not b1103) ) :assumption (or (not b306) (not b1057) ) :assumption (or (not b310) (not b1063) ) :assumption (or (not b313) (not b1069) ) :assumption (or (not b316) (not b1075) ) :assumption (or (not b306) (not b1037) ) :assumption (or (not b310) (not b1042) ) :assumption (or (not b313) (not b1047) ) :assumption (or (not b316) (not b1052) ) :assumption (or (not b306) (not b1013) ) :assumption (or (not b310) (not b1019) ) :assumption (or (not b313) (not b1025) ) :assumption (or (not b316) (not b1031) ) :assumption (or (not b306) (not b985) ) :assumption (or (not b310) (not b992) ) :assumption (or (not b313) (not b999) ) :assumption (or (not b316) (not b1006) ) :assumption (or (not b319) (not b337) ) :assumption (or (not b322) (not b340) ) :assumption (or (not b325) (not b343) ) :assumption (or (not b319) (not b328) ) :assumption (or (not b322) (not b331) ) :assumption (or (not b325) (not b334) ) :assumption (or (not b319) (not b970) ) :assumption (or (not b322) (not b975) ) :assumption (or (not b325) (not b980) ) :assumption (or (not b319) (not b949) ) :assumption (or (not b322) (not b954) ) :assumption (or (not b325) (not b959) ) :assumption (or (not b319) (not b926) ) :assumption (or (not b322) (not b932) ) :assumption (or (not b325) (not b938) ) :assumption (or (not b319) (not b903) ) :assumption (or (not b322) (not b908) ) :assumption (or (not b325) (not b913) ) :assumption (or (not b319) (not b884) ) :assumption (or (not b322) (not b890) ) :assumption (or (not b319) (not b856) ) :assumption (or (not b322) (not b863) ) :assumption (or (not b328) (not b337) ) :assumption (or (not b331) (not b340) ) :assumption (or (not b334) (not b343) ) :assumption (or (not b328) (not b970) ) :assumption (or (not b331) (not b975) ) :assumption (or (not b334) (not b980) ) :assumption (or (not b328) (not b949) ) :assumption (or (not b331) (not b954) ) :assumption (or (not b334) (not b959) ) :assumption (or (not b328) (not b926) ) :assumption (or (not b331) (not b932) ) :assumption (or (not b334) (not b938) ) :assumption (or (not b328) (not b903) ) :assumption (or (not b331) (not b908) ) :assumption (or (not b334) (not b913) ) :assumption (or (not b328) (not b884) ) :assumption (or (not b331) (not b890) ) :assumption (or (not b328) (not b856) ) :assumption (or (not b331) (not b863) ) :assumption (or (not b337) (not b970) ) :assumption (or (not b340) (not b975) ) :assumption (or (not b343) (not b980) ) :assumption (or (not b337) (not b949) ) :assumption (or (not b340) (not b954) ) :assumption (or (not b343) (not b959) ) :assumption (or (not b337) (not b926) ) :assumption (or (not b340) (not b932) ) :assumption (or (not b343) (not b938) ) :assumption (or (not b337) (not b903) ) :assumption (or (not b340) (not b908) ) :assumption (or (not b343) (not b913) ) :assumption (or (not b337) (not b884) ) :assumption (or (not b340) (not b890) ) :assumption (or (not b337) (not b856) ) :assumption (or (not b340) (not b863) ) :assumption (or (not b346) (not b364) ) :assumption (or (not b349) (not b367) ) :assumption (or (not b352) (not b370) ) :assumption (or (not b346) (not b355) ) :assumption (or (not b349) (not b358) ) :assumption (or (not b352) (not b361) ) :assumption (or (not b346) (not b1119) ) :assumption (or (not b349) (not b1124) ) :assumption (or (not b352) (not b1129) ) :assumption (or (not b346) (not b1093) ) :assumption (or (not b349) (not b1098) ) :assumption (or (not b352) (not b1103) ) :assumption (or (not b346) (not b1063) ) :assumption (or (not b349) (not b1069) ) :assumption (or (not b352) (not b1075) ) :assumption (or (not b346) (not b1042) ) :assumption (or (not b349) (not b1047) ) :assumption (or (not b352) (not b1052) ) :assumption (or (not b346) (not b1019) ) :assumption (or (not b349) (not b1025) ) :assumption (or (not b352) (not b1031) ) :assumption (or (not b346) (not b992) ) :assumption (or (not b349) (not b999) ) :assumption (or (not b352) (not b1006) ) :assumption (or (not b355) (not b364) ) :assumption (or (not b358) (not b367) ) :assumption (or (not b361) (not b370) ) :assumption (or (not b355) (not b1119) ) :assumption (or (not b358) (not b1124) ) :assumption (or (not b361) (not b1129) ) :assumption (or (not b355) (not b1093) ) :assumption (or (not b358) (not b1098) ) :assumption (or (not b361) (not b1103) ) :assumption (or (not b355) (not b1063) ) :assumption (or (not b358) (not b1069) ) :assumption (or (not b361) (not b1075) ) :assumption (or (not b355) (not b1042) ) :assumption (or (not b358) (not b1047) ) :assumption (or (not b361) (not b1052) ) :assumption (or (not b355) (not b1019) ) :assumption (or (not b358) (not b1025) ) :assumption (or (not b361) (not b1031) ) :assumption (or (not b355) (not b992) ) :assumption (or (not b358) (not b999) ) :assumption (or (not b361) (not b1006) ) :assumption (or (not b364) (not b1119) ) :assumption (or (not b367) (not b1124) ) :assumption (or (not b370) (not b1129) ) :assumption (or (not b364) (not b1093) ) :assumption (or (not b367) (not b1098) ) :assumption (or (not b370) (not b1103) ) :assumption (or (not b364) (not b1063) ) :assumption (or (not b367) (not b1069) ) :assumption (or (not b370) (not b1075) ) :assumption (or (not b364) (not b1042) ) :assumption (or (not b367) (not b1047) ) :assumption (or (not b370) (not b1052) ) :assumption (or (not b364) (not b1019) ) :assumption (or (not b367) (not b1025) ) :assumption (or (not b370) (not b1031) ) :assumption (or (not b364) (not b992) ) :assumption (or (not b367) (not b999) ) :assumption (or (not b370) (not b1006) ) :assumption (or (not b373) (not b391) ) :assumption (or (not b376) (not b394) ) :assumption (or (not b379) (not b397) ) :assumption (or (not b373) (not b382) ) :assumption (or (not b376) (not b385) ) :assumption (or (not b379) (not b388) ) :assumption (or (not b373) (not b970) ) :assumption (or (not b376) (not b975) ) :assumption (or (not b379) (not b980) ) :assumption (or (not b373) (not b949) ) :assumption (or (not b376) (not b954) ) :assumption (or (not b379) (not b959) ) :assumption (or (not b373) (not b926) ) :assumption (or (not b376) (not b932) ) :assumption (or (not b379) (not b938) ) :assumption (or (not b373) (not b903) ) :assumption (or (not b376) (not b908) ) :assumption (or (not b379) (not b913) ) :assumption (or (not b373) (not b884) ) :assumption (or (not b376) (not b890) ) :assumption (or (not b373) (not b856) ) :assumption (or (not b376) (not b863) ) :assumption (or (not b382) (not b391) ) :assumption (or (not b385) (not b394) ) :assumption (or (not b388) (not b397) ) :assumption (or (not b382) (not b970) ) :assumption (or (not b385) (not b975) ) :assumption (or (not b388) (not b980) ) :assumption (or (not b382) (not b949) ) :assumption (or (not b385) (not b954) ) :assumption (or (not b388) (not b959) ) :assumption (or (not b382) (not b926) ) :assumption (or (not b385) (not b932) ) :assumption (or (not b388) (not b938) ) :assumption (or (not b382) (not b903) ) :assumption (or (not b385) (not b908) ) :assumption (or (not b388) (not b913) ) :assumption (or (not b382) (not b884) ) :assumption (or (not b385) (not b890) ) :assumption (or (not b382) (not b856) ) :assumption (or (not b385) (not b863) ) :assumption (or (not b391) (not b970) ) :assumption (or (not b394) (not b975) ) :assumption (or (not b397) (not b980) ) :assumption (or (not b391) (not b949) ) :assumption (or (not b394) (not b954) ) :assumption (or (not b397) (not b959) ) :assumption (or (not b391) (not b926) ) :assumption (or (not b394) (not b932) ) :assumption (or (not b397) (not b938) ) :assumption (or (not b391) (not b903) ) :assumption (or (not b394) (not b908) ) :assumption (or (not b397) (not b913) ) :assumption (or (not b391) (not b884) ) :assumption (or (not b394) (not b890) ) :assumption (or (not b391) (not b856) ) :assumption (or (not b394) (not b863) ) :assumption (or (not b400) (not b418) ) :assumption (or (not b403) (not b421) ) :assumption (or (not b406) (not b424) ) :assumption (or (not b400) (not b409) ) :assumption (or (not b403) (not b412) ) :assumption (or (not b406) (not b415) ) :assumption (or (not b400) (not b1119) ) :assumption (or (not b403) (not b1124) ) :assumption (or (not b406) (not b1129) ) :assumption (or (not b400) (not b1093) ) :assumption (or (not b403) (not b1098) ) :assumption (or (not b406) (not b1103) ) :assumption (or (not b400) (not b1063) ) :assumption (or (not b403) (not b1069) ) :assumption (or (not b406) (not b1075) ) :assumption (or (not b400) (not b1042) ) :assumption (or (not b403) (not b1047) ) :assumption (or (not b406) (not b1052) ) :assumption (or (not b400) (not b1019) ) :assumption (or (not b403) (not b1025) ) :assumption (or (not b406) (not b1031) ) :assumption (or (not b400) (not b992) ) :assumption (or (not b403) (not b999) ) :assumption (or (not b406) (not b1006) ) :assumption (or (not b409) (not b418) ) :assumption (or (not b412) (not b421) ) :assumption (or (not b415) (not b424) ) :assumption (or (not b409) (not b1119) ) :assumption (or (not b412) (not b1124) ) :assumption (or (not b415) (not b1129) ) :assumption (or (not b409) (not b1093) ) :assumption (or (not b412) (not b1098) ) :assumption (or (not b415) (not b1103) ) :assumption (or (not b409) (not b1063) ) :assumption (or (not b412) (not b1069) ) :assumption (or (not b415) (not b1075) ) :assumption (or (not b409) (not b1042) ) :assumption (or (not b412) (not b1047) ) :assumption (or (not b415) (not b1052) ) :assumption (or (not b409) (not b1019) ) :assumption (or (not b412) (not b1025) ) :assumption (or (not b415) (not b1031) ) :assumption (or (not b409) (not b992) ) :assumption (or (not b412) (not b999) ) :assumption (or (not b415) (not b1006) ) :assumption (or (not b418) (not b1119) ) :assumption (or (not b421) (not b1124) ) :assumption (or (not b424) (not b1129) ) :assumption (or (not b418) (not b1093) ) :assumption (or (not b421) (not b1098) ) :assumption (or (not b424) (not b1103) ) :assumption (or (not b418) (not b1063) ) :assumption (or (not b421) (not b1069) ) :assumption (or (not b424) (not b1075) ) :assumption (or (not b418) (not b1042) ) :assumption (or (not b421) (not b1047) ) :assumption (or (not b424) (not b1052) ) :assumption (or (not b418) (not b1019) ) :assumption (or (not b421) (not b1025) ) :assumption (or (not b424) (not b1031) ) :assumption (or (not b418) (not b992) ) :assumption (or (not b421) (not b999) ) :assumption (or (not b424) (not b1006) ) :assumption (or (not b427) (not b445) ) :assumption (or (not b430) (not b448) ) :assumption (or (not b433) (not b451) ) :assumption (or (not b427) (not b436) ) :assumption (or (not b430) (not b439) ) :assumption (or (not b433) (not b442) ) :assumption (or (not b427) (not b970) ) :assumption (or (not b430) (not b975) ) :assumption (or (not b433) (not b980) ) :assumption (or (not b427) (not b949) ) :assumption (or (not b430) (not b954) ) :assumption (or (not b433) (not b959) ) :assumption (or (not b427) (not b926) ) :assumption (or (not b430) (not b932) ) :assumption (or (not b433) (not b938) ) :assumption (or (not b427) (not b903) ) :assumption (or (not b430) (not b908) ) :assumption (or (not b433) (not b913) ) :assumption (or (not b427) (not b884) ) :assumption (or (not b430) (not b890) ) :assumption (or (not b427) (not b856) ) :assumption (or (not b430) (not b863) ) :assumption (or (not b436) (not b445) ) :assumption (or (not b439) (not b448) ) :assumption (or (not b442) (not b451) ) :assumption (or (not b436) (not b970) ) :assumption (or (not b439) (not b975) ) :assumption (or (not b442) (not b980) ) :assumption (or (not b436) (not b949) ) :assumption (or (not b439) (not b954) ) :assumption (or (not b442) (not b959) ) :assumption (or (not b436) (not b926) ) :assumption (or (not b439) (not b932) ) :assumption (or (not b442) (not b938) ) :assumption (or (not b436) (not b903) ) :assumption (or (not b439) (not b908) ) :assumption (or (not b442) (not b913) ) :assumption (or (not b436) (not b884) ) :assumption (or (not b439) (not b890) ) :assumption (or (not b436) (not b856) ) :assumption (or (not b439) (not b863) ) :assumption (or (not b445) (not b970) ) :assumption (or (not b448) (not b975) ) :assumption (or (not b451) (not b980) ) :assumption (or (not b445) (not b949) ) :assumption (or (not b448) (not b954) ) :assumption (or (not b451) (not b959) ) :assumption (or (not b445) (not b926) ) :assumption (or (not b448) (not b932) ) :assumption (or (not b451) (not b938) ) :assumption (or (not b445) (not b903) ) :assumption (or (not b448) (not b908) ) :assumption (or (not b451) (not b913) ) :assumption (or (not b445) (not b884) ) :assumption (or (not b448) (not b890) ) :assumption (or (not b445) (not b856) ) :assumption (or (not b448) (not b863) ) :assumption (or (not b454) (not b479) ) :assumption (or (not b458) (not b482) ) :assumption (or (not b461) (not b485) ) :assumption (or (not b464) (not b488) ) :assumption (or (not b454) (not b467) ) :assumption (or (not b458) (not b470) ) :assumption (or (not b461) (not b473) ) :assumption (or (not b464) (not b476) ) :assumption (or (not b454) (not b1114) ) :assumption (or (not b458) (not b1119) ) :assumption (or (not b461) (not b1124) ) :assumption (or (not b464) (not b1129) ) :assumption (or (not b454) (not b1088) ) :assumption (or (not b458) (not b1093) ) :assumption (or (not b461) (not b1098) ) :assumption (or (not b464) (not b1103) ) :assumption (or (not b454) (not b1057) ) :assumption (or (not b458) (not b1063) ) :assumption (or (not b461) (not b1069) ) :assumption (or (not b464) (not b1075) ) :assumption (or (not b454) (not b1037) ) :assumption (or (not b458) (not b1042) ) :assumption (or (not b461) (not b1047) ) :assumption (or (not b464) (not b1052) ) :assumption (or (not b454) (not b1013) ) :assumption (or (not b458) (not b1019) ) :assumption (or (not b461) (not b1025) ) :assumption (or (not b464) (not b1031) ) :assumption (or (not b454) (not b985) ) :assumption (or (not b458) (not b992) ) :assumption (or (not b461) (not b999) ) :assumption (or (not b464) (not b1006) ) :assumption (or (not b467) (not b479) ) :assumption (or (not b470) (not b482) ) :assumption (or (not b473) (not b485) ) :assumption (or (not b476) (not b488) ) :assumption (or (not b467) (not b1114) ) :assumption (or (not b470) (not b1119) ) :assumption (or (not b473) (not b1124) ) :assumption (or (not b476) (not b1129) ) :assumption (or (not b467) (not b1088) ) :assumption (or (not b470) (not b1093) ) :assumption (or (not b473) (not b1098) ) :assumption (or (not b476) (not b1103) ) :assumption (or (not b467) (not b1057) ) :assumption (or (not b470) (not b1063) ) :assumption (or (not b473) (not b1069) ) :assumption (or (not b476) (not b1075) ) :assumption (or (not b467) (not b1037) ) :assumption (or (not b470) (not b1042) ) :assumption (or (not b473) (not b1047) ) :assumption (or (not b476) (not b1052) ) :assumption (or (not b467) (not b1013) ) :assumption (or (not b470) (not b1019) ) :assumption (or (not b473) (not b1025) ) :assumption (or (not b476) (not b1031) ) :assumption (or (not b467) (not b985) ) :assumption (or (not b470) (not b992) ) :assumption (or (not b473) (not b999) ) :assumption (or (not b476) (not b1006) ) :assumption (or (not b479) (not b1114) ) :assumption (or (not b482) (not b1119) ) :assumption (or (not b485) (not b1124) ) :assumption (or (not b488) (not b1129) ) :assumption (or (not b479) (not b1088) ) :assumption (or (not b482) (not b1093) ) :assumption (or (not b485) (not b1098) ) :assumption (or (not b488) (not b1103) ) :assumption (or (not b479) (not b1057) ) :assumption (or (not b482) (not b1063) ) :assumption (or (not b485) (not b1069) ) :assumption (or (not b488) (not b1075) ) :assumption (or (not b479) (not b1037) ) :assumption (or (not b482) (not b1042) ) :assumption (or (not b485) (not b1047) ) :assumption (or (not b488) (not b1052) ) :assumption (or (not b479) (not b1013) ) :assumption (or (not b482) (not b1019) ) :assumption (or (not b485) (not b1025) ) :assumption (or (not b488) (not b1031) ) :assumption (or (not b479) (not b985) ) :assumption (or (not b482) (not b992) ) :assumption (or (not b485) (not b999) ) :assumption (or (not b488) (not b1006) ) :assumption (or (not b491) (not b509) ) :assumption (or (not b494) (not b512) ) :assumption (or (not b497) (not b515) ) :assumption (or (not b491) (not b500) ) :assumption (or (not b494) (not b503) ) :assumption (or (not b497) (not b506) ) :assumption (or (not b491) (not b970) ) :assumption (or (not b494) (not b975) ) :assumption (or (not b497) (not b980) ) :assumption (or (not b491) (not b949) ) :assumption (or (not b494) (not b954) ) :assumption (or (not b497) (not b959) ) :assumption (or (not b491) (not b926) ) :assumption (or (not b494) (not b932) ) :assumption (or (not b497) (not b938) ) :assumption (or (not b491) (not b903) ) :assumption (or (not b494) (not b908) ) :assumption (or (not b497) (not b913) ) :assumption (or (not b491) (not b884) ) :assumption (or (not b494) (not b890) ) :assumption (or (not b491) (not b856) ) :assumption (or (not b494) (not b863) ) :assumption (or (not b500) (not b509) ) :assumption (or (not b503) (not b512) ) :assumption (or (not b506) (not b515) ) :assumption (or (not b500) (not b970) ) :assumption (or (not b503) (not b975) ) :assumption (or (not b506) (not b980) ) :assumption (or (not b500) (not b949) ) :assumption (or (not b503) (not b954) ) :assumption (or (not b506) (not b959) ) :assumption (or (not b500) (not b926) ) :assumption (or (not b503) (not b932) ) :assumption (or (not b506) (not b938) ) :assumption (or (not b500) (not b903) ) :assumption (or (not b503) (not b908) ) :assumption (or (not b506) (not b913) ) :assumption (or (not b500) (not b884) ) :assumption (or (not b503) (not b890) ) :assumption (or (not b500) (not b856) ) :assumption (or (not b503) (not b863) ) :assumption (or (not b509) (not b970) ) :assumption (or (not b512) (not b975) ) :assumption (or (not b515) (not b980) ) :assumption (or (not b509) (not b949) ) :assumption (or (not b512) (not b954) ) :assumption (or (not b515) (not b959) ) :assumption (or (not b509) (not b926) ) :assumption (or (not b512) (not b932) ) :assumption (or (not b515) (not b938) ) :assumption (or (not b509) (not b903) ) :assumption (or (not b512) (not b908) ) :assumption (or (not b515) (not b913) ) :assumption (or (not b509) (not b884) ) :assumption (or (not b512) (not b890) ) :assumption (or (not b509) (not b856) ) :assumption (or (not b512) (not b863) ) :assumption (or (not b518) (not b542) ) :assumption (or (not b521) (not b545) ) :assumption (or (not b524) (not b548) ) :assumption (or (not b527) (not b551) ) :assumption (or (not b518) (not b530) ) :assumption (or (not b521) (not b533) ) :assumption (or (not b524) (not b536) ) :assumption (or (not b527) (not b539) ) :assumption (or (not b518) (not b1114) ) :assumption (or (not b521) (not b1119) ) :assumption (or (not b524) (not b1124) ) :assumption (or (not b527) (not b1129) ) :assumption (or (not b518) (not b1088) ) :assumption (or (not b521) (not b1093) ) :assumption (or (not b524) (not b1098) ) :assumption (or (not b527) (not b1103) ) :assumption (or (not b518) (not b1057) ) :assumption (or (not b521) (not b1063) ) :assumption (or (not b524) (not b1069) ) :assumption (or (not b527) (not b1075) ) :assumption (or (not b518) (not b1037) ) :assumption (or (not b521) (not b1042) ) :assumption (or (not b524) (not b1047) ) :assumption (or (not b527) (not b1052) ) :assumption (or (not b518) (not b1013) ) :assumption (or (not b521) (not b1019) ) :assumption (or (not b524) (not b1025) ) :assumption (or (not b527) (not b1031) ) :assumption (or (not b518) (not b985) ) :assumption (or (not b521) (not b992) ) :assumption (or (not b524) (not b999) ) :assumption (or (not b527) (not b1006) ) :assumption (or (not b530) (not b542) ) :assumption (or (not b533) (not b545) ) :assumption (or (not b536) (not b548) ) :assumption (or (not b539) (not b551) ) :assumption (or (not b530) (not b1114) ) :assumption (or (not b533) (not b1119) ) :assumption (or (not b536) (not b1124) ) :assumption (or (not b539) (not b1129) ) :assumption (or (not b530) (not b1088) ) :assumption (or (not b533) (not b1093) ) :assumption (or (not b536) (not b1098) ) :assumption (or (not b539) (not b1103) ) :assumption (or (not b530) (not b1057) ) :assumption (or (not b533) (not b1063) ) :assumption (or (not b536) (not b1069) ) :assumption (or (not b539) (not b1075) ) :assumption (or (not b530) (not b1037) ) :assumption (or (not b533) (not b1042) ) :assumption (or (not b536) (not b1047) ) :assumption (or (not b539) (not b1052) ) :assumption (or (not b530) (not b1013) ) :assumption (or (not b533) (not b1019) ) :assumption (or (not b536) (not b1025) ) :assumption (or (not b539) (not b1031) ) :assumption (or (not b530) (not b985) ) :assumption (or (not b533) (not b992) ) :assumption (or (not b536) (not b999) ) :assumption (or (not b539) (not b1006) ) :assumption (or (not b542) (not b1114) ) :assumption (or (not b545) (not b1119) ) :assumption (or (not b548) (not b1124) ) :assumption (or (not b551) (not b1129) ) :assumption (or (not b542) (not b1088) ) :assumption (or (not b545) (not b1093) ) :assumption (or (not b548) (not b1098) ) :assumption (or (not b551) (not b1103) ) :assumption (or (not b542) (not b1057) ) :assumption (or (not b545) (not b1063) ) :assumption (or (not b548) (not b1069) ) :assumption (or (not b551) (not b1075) ) :assumption (or (not b542) (not b1037) ) :assumption (or (not b545) (not b1042) ) :assumption (or (not b548) (not b1047) ) :assumption (or (not b551) (not b1052) ) :assumption (or (not b542) (not b1013) ) :assumption (or (not b545) (not b1019) ) :assumption (or (not b548) (not b1025) ) :assumption (or (not b551) (not b1031) ) :assumption (or (not b542) (not b985) ) :assumption (or (not b545) (not b992) ) :assumption (or (not b548) (not b999) ) :assumption (or (not b551) (not b1006) ) :assumption (or (not b554) (not b1133) ) :assumption (or (not b561) (not b1136) ) :assumption (or (not b567) (not b1139) ) :assumption (or (not b573) (not b1142) ) :assumption (or (not b554) (not b872) ) :assumption (or (not b561) (not b878) ) :assumption (or (not b567) (not b884) ) :assumption (or (not b573) (not b890) ) :assumption (or (not b554) (not b842) ) :assumption (or (not b561) (not b849) ) :assumption (or (not b567) (not b856) ) :assumption (or (not b573) (not b863) ) :assumption (or (not b554) (not b582) ) :assumption (or (not b561) (not b588) ) :assumption (or (not b567) (not b594) ) :assumption (or (not b573) (not b600) ) :assumption (or (not b491) (not b567) ) :assumption (or (not b494) (not b573) ) :assumption (or (not b427) (not b567) ) :assumption (or (not b430) (not b573) ) :assumption (or (not b373) (not b567) ) :assumption (or (not b376) (not b573) ) :assumption (or (not b319) (not b567) ) :assumption (or (not b322) (not b573) ) :assumption (or (not b239) (not b567) ) :assumption (or (not b245) (not b573) ) :assumption (or (not b153) (not b567) ) :assumption (or (not b160) (not b573) ) :assumption (or (not b90) (not b573) ) :assumption (or (not b15) (not b573) ) :assumption (or (not b561) (not b944) ) :assumption (or (not b567) (not b949) ) :assumption (or (not b573) (not b954) ) :assumption (or (not b561) (not b898) ) :assumption (or (not b567) (not b903) ) :assumption (or (not b573) (not b908) ) :assumption (or (not b561) (not b654) ) :assumption (or (not b567) (not b659) ) :assumption (or (not b573) (not b664) ) :assumption (or (not b561) (not b609) ) :assumption (or (not b567) (not b614) ) :assumption (or (not b573) (not b619) ) :assumption (or (not b561) (not b1148) ) :assumption (or (not b567) (not b1149) ) :assumption (or (not b573) (not b1150) ) :assumption (or (not b561) (not b920) ) :assumption (or (not b567) (not b926) ) :assumption (or (not b573) (not b932) ) :assumption (or (not b561) (not b630) ) :assumption (or (not b567) (not b636) ) :assumption (or (not b573) (not b642) ) :assumption (or (not b500) (not b567) ) :assumption (or (not b503) (not b573) ) :assumption (or (not b436) (not b567) ) :assumption (or (not b439) (not b573) ) :assumption (or (not b382) (not b567) ) :assumption (or (not b385) (not b573) ) :assumption (or (not b328) (not b567) ) :assumption (or (not b331) (not b573) ) :assumption (or (not b255) (not b567) ) :assumption (or (not b260) (not b573) ) :assumption (or (not b170) (not b567) ) :assumption (or (not b175) (not b573) ) :assumption (or (not b101) (not b561) ) :assumption (or (not b106) (not b567) ) :assumption (or (not b111) (not b573) ) :assumption (or (not b28) (not b561) ) :assumption (or (not b34) (not b567) ) :assumption (or (not b40) (not b573) ) :assumption (or (not b561) (not b1152) ) :assumption (or (not b567) (not b1153) ) :assumption (or (not b573) (not b1154) ) :assumption (or (not b561) (not b965) ) :assumption (or (not b567) (not b970) ) :assumption (or (not b573) (not b975) ) :assumption (or (not b561) (not b675) ) :assumption (or (not b567) (not b680) ) :assumption (or (not b573) (not b685) ) :assumption (or (not b582) (not b1133) ) :assumption (or (not b588) (not b1136) ) :assumption (or (not b594) (not b1139) ) :assumption (or (not b600) (not b1142) ) :assumption (or (not b582) (not b872) ) :assumption (or (not b588) (not b878) ) :assumption (or (not b594) (not b884) ) :assumption (or (not b600) (not b890) ) :assumption (or (not b582) (not b842) ) :assumption (or (not b588) (not b849) ) :assumption (or (not b594) (not b856) ) :assumption (or (not b600) (not b863) ) :assumption (or (not b491) (not b594) ) :assumption (or (not b494) (not b600) ) :assumption (or (not b427) (not b594) ) :assumption (or (not b430) (not b600) ) :assumption (or (not b373) (not b594) ) :assumption (or (not b376) (not b600) ) :assumption (or (not b319) (not b594) ) :assumption (or (not b322) (not b600) ) :assumption (or (not b239) (not b594) ) :assumption (or (not b245) (not b600) ) :assumption (or (not b153) (not b594) ) :assumption (or (not b160) (not b600) ) :assumption (or (not b90) (not b600) ) :assumption (or (not b15) (not b600) ) :assumption (or (not b588) (not b944) ) :assumption (or (not b594) (not b949) ) :assumption (or (not b600) (not b954) ) :assumption (or (not b588) (not b898) ) :assumption (or (not b594) (not b903) ) :assumption (or (not b600) (not b908) ) :assumption (or (not b588) (not b654) ) :assumption (or (not b594) (not b659) ) :assumption (or (not b600) (not b664) ) :assumption (or (not b588) (not b609) ) :assumption (or (not b594) (not b614) ) :assumption (or (not b600) (not b619) ) :assumption (or (not b588) (not b1152) ) :assumption (or (not b594) (not b1153) ) :assumption (or (not b600) (not b1154) ) :assumption (or (not b588) (not b965) ) :assumption (or (not b594) (not b970) ) :assumption (or (not b600) (not b975) ) :assumption (or (not b588) (not b675) ) :assumption (or (not b594) (not b680) ) :assumption (or (not b600) (not b685) ) :assumption (or (not b509) (not b594) ) :assumption (or (not b512) (not b600) ) :assumption (or (not b445) (not b594) ) :assumption (or (not b448) (not b600) ) :assumption (or (not b391) (not b594) ) :assumption (or (not b394) (not b600) ) :assumption (or (not b337) (not b594) ) :assumption (or (not b340) (not b600) ) :assumption (or (not b265) (not b588) ) :assumption (or (not b271) (not b594) ) :assumption (or (not b275) (not b600) ) :assumption (or (not b183) (not b588) ) :assumption (or (not b190) (not b594) ) :assumption (or (not b195) (not b600) ) :assumption (or (not b120) (not b600) ) :assumption (or (not b46) (not b600) ) :assumption (or (not b588) (not b1148) ) :assumption (or (not b594) (not b1149) ) :assumption (or (not b600) (not b1150) ) :assumption (or (not b588) (not b920) ) :assumption (or (not b594) (not b926) ) :assumption (or (not b600) (not b932) ) :assumption (or (not b588) (not b630) ) :assumption (or (not b594) (not b636) ) :assumption (or (not b600) (not b642) ) :assumption (or (not b609) (not b1148) ) :assumption (or (not b614) (not b1149) ) :assumption (or (not b619) (not b1150) ) :assumption (or (not b624) (not b1151) ) :assumption (or (not b609) (not b920) ) :assumption (or (not b614) (not b926) ) :assumption (or (not b619) (not b932) ) :assumption (or (not b624) (not b938) ) :assumption (or (not b609) (not b898) ) :assumption (or (not b614) (not b903) ) :assumption (or (not b619) (not b908) ) :assumption (or (not b624) (not b913) ) :assumption (or (not b609) (not b630) ) :assumption (or (not b614) (not b636) ) :assumption (or (not b619) (not b642) ) :assumption (or (not b624) (not b648) ) :assumption (or (not b500) (not b614) ) :assumption (or (not b503) (not b619) ) :assumption (or (not b506) (not b624) ) :assumption (or (not b436) (not b614) ) :assumption (or (not b439) (not b619) ) :assumption (or (not b442) (not b624) ) :assumption (or (not b382) (not b614) ) :assumption (or (not b385) (not b619) ) :assumption (or (not b388) (not b624) ) :assumption (or (not b328) (not b614) ) :assumption (or (not b331) (not b619) ) :assumption (or (not b334) (not b624) ) :assumption (or (not b255) (not b614) ) :assumption (or (not b260) (not b619) ) :assumption (or (not b170) (not b614) ) :assumption (or (not b175) (not b619) ) :assumption (or (not b179) (not b624) ) :assumption (or (not b101) (not b609) ) :assumption (or (not b106) (not b614) ) :assumption (or (not b111) (not b619) ) :assumption (or (not b115) (not b624) ) :assumption (or (not b28) (not b609) ) :assumption (or (not b34) (not b614) ) :assumption (or (not b40) (not b619) ) :assumption (or (not b609) (not b965) ) :assumption (or (not b614) (not b970) ) :assumption (or (not b619) (not b975) ) :assumption (or (not b624) (not b980) ) :assumption (or (not b609) (not b849) ) :assumption (or (not b614) (not b856) ) :assumption (or (not b619) (not b863) ) :assumption (or (not b609) (not b675) ) :assumption (or (not b614) (not b680) ) :assumption (or (not b619) (not b685) ) :assumption (or (not b624) (not b690) ) :assumption (or (not b609) (not b1136) ) :assumption (or (not b614) (not b1139) ) :assumption (or (not b619) (not b1142) ) :assumption (or (not b624) (not b1145) ) :assumption (or (not b609) (not b878) ) :assumption (or (not b614) (not b884) ) :assumption (or (not b619) (not b890) ) :assumption (or (not b491) (not b614) ) :assumption (or (not b494) (not b619) ) :assumption (or (not b497) (not b624) ) :assumption (or (not b427) (not b614) ) :assumption (or (not b430) (not b619) ) :assumption (or (not b433) (not b624) ) :assumption (or (not b373) (not b614) ) :assumption (or (not b376) (not b619) ) :assumption (or (not b379) (not b624) ) :assumption (or (not b319) (not b614) ) :assumption (or (not b322) (not b619) ) :assumption (or (not b325) (not b624) ) :assumption (or (not b239) (not b614) ) :assumption (or (not b245) (not b619) ) :assumption (or (not b250) (not b624) ) :assumption (or (not b153) (not b614) ) :assumption (or (not b160) (not b619) ) :assumption (or (not b165) (not b624) ) :assumption (or (not b90) (not b619) ) :assumption (or (not b96) (not b624) ) :assumption (or (not b15) (not b619) ) :assumption (or (not b22) (not b624) ) :assumption (or (not b609) (not b1152) ) :assumption (or (not b614) (not b1153) ) :assumption (or (not b619) (not b1154) ) :assumption (or (not b624) (not b1155) ) :assumption (or (not b609) (not b944) ) :assumption (or (not b614) (not b949) ) :assumption (or (not b619) (not b954) ) :assumption (or (not b624) (not b959) ) :assumption (or (not b609) (not b654) ) :assumption (or (not b614) (not b659) ) :assumption (or (not b619) (not b664) ) :assumption (or (not b624) (not b669) ) :assumption (or (not b630) (not b1148) ) :assumption (or (not b636) (not b1149) ) :assumption (or (not b642) (not b1150) ) :assumption (or (not b648) (not b1151) ) :assumption (or (not b630) (not b920) ) :assumption (or (not b636) (not b926) ) :assumption (or (not b642) (not b932) ) :assumption (or (not b648) (not b938) ) :assumption (or (not b630) (not b898) ) :assumption (or (not b636) (not b903) ) :assumption (or (not b642) (not b908) ) :assumption (or (not b648) (not b913) ) :assumption (or (not b500) (not b636) ) :assumption (or (not b503) (not b642) ) :assumption (or (not b506) (not b648) ) :assumption (or (not b436) (not b636) ) :assumption (or (not b439) (not b642) ) :assumption (or (not b442) (not b648) ) :assumption (or (not b382) (not b636) ) :assumption (or (not b385) (not b642) ) :assumption (or (not b388) (not b648) ) :assumption (or (not b328) (not b636) ) :assumption (or (not b331) (not b642) ) :assumption (or (not b334) (not b648) ) :assumption (or (not b255) (not b636) ) :assumption (or (not b260) (not b642) ) :assumption (or (not b170) (not b636) ) :assumption (or (not b175) (not b642) ) :assumption (or (not b179) (not b648) ) :assumption (or (not b101) (not b630) ) :assumption (or (not b106) (not b636) ) :assumption (or (not b111) (not b642) ) :assumption (or (not b115) (not b648) ) :assumption (or (not b28) (not b630) ) :assumption (or (not b34) (not b636) ) :assumption (or (not b40) (not b642) ) :assumption (or (not b630) (not b965) ) :assumption (or (not b636) (not b970) ) :assumption (or (not b642) (not b975) ) :assumption (or (not b648) (not b980) ) :assumption (or (not b630) (not b849) ) :assumption (or (not b636) (not b856) ) :assumption (or (not b642) (not b863) ) :assumption (or (not b630) (not b675) ) :assumption (or (not b636) (not b680) ) :assumption (or (not b642) (not b685) ) :assumption (or (not b648) (not b690) ) :assumption (or (not b630) (not b1152) ) :assumption (or (not b636) (not b1153) ) :assumption (or (not b642) (not b1154) ) :assumption (or (not b648) (not b1155) ) :assumption (or (not b630) (not b944) ) :assumption (or (not b636) (not b949) ) :assumption (or (not b642) (not b954) ) :assumption (or (not b648) (not b959) ) :assumption (or (not b630) (not b654) ) :assumption (or (not b636) (not b659) ) :assumption (or (not b642) (not b664) ) :assumption (or (not b648) (not b669) ) :assumption (or (not b509) (not b636) ) :assumption (or (not b512) (not b642) ) :assumption (or (not b515) (not b648) ) :assumption (or (not b445) (not b636) ) :assumption (or (not b448) (not b642) ) :assumption (or (not b451) (not b648) ) :assumption (or (not b391) (not b636) ) :assumption (or (not b394) (not b642) ) :assumption (or (not b397) (not b648) ) :assumption (or (not b337) (not b636) ) :assumption (or (not b340) (not b642) ) :assumption (or (not b343) (not b648) ) :assumption (or (not b265) (not b630) ) :assumption (or (not b271) (not b636) ) :assumption (or (not b275) (not b642) ) :assumption (or (not b279) (not b648) ) :assumption (or (not b183) (not b630) ) :assumption (or (not b190) (not b636) ) :assumption (or (not b195) (not b642) ) :assumption (or (not b120) (not b642) ) :assumption (or (not b46) (not b642) ) :assumption (or (not b52) (not b648) ) :assumption (or (not b630) (not b1136) ) :assumption (or (not b636) (not b1139) ) :assumption (or (not b642) (not b1142) ) :assumption (or (not b648) (not b1145) ) :assumption (or (not b630) (not b878) ) :assumption (or (not b636) (not b884) ) :assumption (or (not b642) (not b890) ) :assumption (or (not b654) (not b1152) ) :assumption (or (not b659) (not b1153) ) :assumption (or (not b664) (not b1154) ) :assumption (or (not b669) (not b1155) ) :assumption (or (not b654) (not b965) ) :assumption (or (not b659) (not b970) ) :assumption (or (not b664) (not b975) ) :assumption (or (not b669) (not b980) ) :assumption (or (not b654) (not b944) ) :assumption (or (not b659) (not b949) ) :assumption (or (not b664) (not b954) ) :assumption (or (not b669) (not b959) ) :assumption (or (not b654) (not b675) ) :assumption (or (not b659) (not b680) ) :assumption (or (not b664) (not b685) ) :assumption (or (not b669) (not b690) ) :assumption (or (not b509) (not b659) ) :assumption (or (not b512) (not b664) ) :assumption (or (not b515) (not b669) ) :assumption (or (not b445) (not b659) ) :assumption (or (not b448) (not b664) ) :assumption (or (not b451) (not b669) ) :assumption (or (not b391) (not b659) ) :assumption (or (not b394) (not b664) ) :assumption (or (not b397) (not b669) ) :assumption (or (not b337) (not b659) ) :assumption (or (not b340) (not b664) ) :assumption (or (not b343) (not b669) ) :assumption (or (not b265) (not b654) ) :assumption (or (not b271) (not b659) ) :assumption (or (not b275) (not b664) ) :assumption (or (not b279) (not b669) ) :assumption (or (not b183) (not b654) ) :assumption (or (not b190) (not b659) ) :assumption (or (not b195) (not b664) ) :assumption (or (not b120) (not b664) ) :assumption (or (not b46) (not b664) ) :assumption (or (not b52) (not b669) ) :assumption (or (not b654) (not b920) ) :assumption (or (not b659) (not b926) ) :assumption (or (not b664) (not b932) ) :assumption (or (not b669) (not b938) ) :assumption (or (not b654) (not b878) ) :assumption (or (not b659) (not b884) ) :assumption (or (not b664) (not b890) ) :assumption (or (not b654) (not b1136) ) :assumption (or (not b659) (not b1139) ) :assumption (or (not b664) (not b1142) ) :assumption (or (not b669) (not b1145) ) :assumption (or (not b654) (not b849) ) :assumption (or (not b659) (not b856) ) :assumption (or (not b664) (not b863) ) :assumption (or (not b491) (not b659) ) :assumption (or (not b494) (not b664) ) :assumption (or (not b497) (not b669) ) :assumption (or (not b427) (not b659) ) :assumption (or (not b430) (not b664) ) :assumption (or (not b433) (not b669) ) :assumption (or (not b373) (not b659) ) :assumption (or (not b376) (not b664) ) :assumption (or (not b379) (not b669) ) :assumption (or (not b319) (not b659) ) :assumption (or (not b322) (not b664) ) :assumption (or (not b325) (not b669) ) :assumption (or (not b239) (not b659) ) :assumption (or (not b245) (not b664) ) :assumption (or (not b250) (not b669) ) :assumption (or (not b153) (not b659) ) :assumption (or (not b160) (not b664) ) :assumption (or (not b165) (not b669) ) :assumption (or (not b90) (not b664) ) :assumption (or (not b96) (not b669) ) :assumption (or (not b15) (not b664) ) :assumption (or (not b22) (not b669) ) :assumption (or (not b654) (not b1148) ) :assumption (or (not b659) (not b1149) ) :assumption (or (not b664) (not b1150) ) :assumption (or (not b669) (not b1151) ) :assumption (or (not b654) (not b898) ) :assumption (or (not b659) (not b903) ) :assumption (or (not b664) (not b908) ) :assumption (or (not b669) (not b913) ) :assumption (or (not b675) (not b1152) ) :assumption (or (not b680) (not b1153) ) :assumption (or (not b685) (not b1154) ) :assumption (or (not b690) (not b1155) ) :assumption (or (not b675) (not b965) ) :assumption (or (not b680) (not b970) ) :assumption (or (not b685) (not b975) ) :assumption (or (not b690) (not b980) ) :assumption (or (not b675) (not b944) ) :assumption (or (not b680) (not b949) ) :assumption (or (not b685) (not b954) ) :assumption (or (not b690) (not b959) ) :assumption (or (not b509) (not b680) ) :assumption (or (not b512) (not b685) ) :assumption (or (not b515) (not b690) ) :assumption (or (not b445) (not b680) ) :assumption (or (not b448) (not b685) ) :assumption (or (not b451) (not b690) ) :assumption (or (not b391) (not b680) ) :assumption (or (not b394) (not b685) ) :assumption (or (not b397) (not b690) ) :assumption (or (not b337) (not b680) ) :assumption (or (not b340) (not b685) ) :assumption (or (not b343) (not b690) ) :assumption (or (not b265) (not b675) ) :assumption (or (not b271) (not b680) ) :assumption (or (not b275) (not b685) ) :assumption (or (not b279) (not b690) ) :assumption (or (not b183) (not b675) ) :assumption (or (not b190) (not b680) ) :assumption (or (not b195) (not b685) ) :assumption (or (not b120) (not b685) ) :assumption (or (not b46) (not b685) ) :assumption (or (not b52) (not b690) ) :assumption (or (not b675) (not b920) ) :assumption (or (not b680) (not b926) ) :assumption (or (not b685) (not b932) ) :assumption (or (not b690) (not b938) ) :assumption (or (not b675) (not b878) ) :assumption (or (not b680) (not b884) ) :assumption (or (not b685) (not b890) ) :assumption (or (not b675) (not b1148) ) :assumption (or (not b680) (not b1149) ) :assumption (or (not b685) (not b1150) ) :assumption (or (not b690) (not b1151) ) :assumption (or (not b675) (not b898) ) :assumption (or (not b680) (not b903) ) :assumption (or (not b685) (not b908) ) :assumption (or (not b690) (not b913) ) :assumption (or (not b500) (not b680) ) :assumption (or (not b503) (not b685) ) :assumption (or (not b506) (not b690) ) :assumption (or (not b436) (not b680) ) :assumption (or (not b439) (not b685) ) :assumption (or (not b442) (not b690) ) :assumption (or (not b382) (not b680) ) :assumption (or (not b385) (not b685) ) :assumption (or (not b388) (not b690) ) :assumption (or (not b328) (not b680) ) :assumption (or (not b331) (not b685) ) :assumption (or (not b334) (not b690) ) :assumption (or (not b255) (not b680) ) :assumption (or (not b260) (not b685) ) :assumption (or (not b170) (not b680) ) :assumption (or (not b175) (not b685) ) :assumption (or (not b179) (not b690) ) :assumption (or (not b101) (not b675) ) :assumption (or (not b106) (not b680) ) :assumption (or (not b111) (not b685) ) :assumption (or (not b115) (not b690) ) :assumption (or (not b28) (not b675) ) :assumption (or (not b34) (not b680) ) :assumption (or (not b40) (not b685) ) :assumption (or (not b675) (not b1136) ) :assumption (or (not b680) (not b1139) ) :assumption (or (not b685) (not b1142) ) :assumption (or (not b690) (not b1145) ) :assumption (or (not b675) (not b849) ) :assumption (or (not b680) (not b856) ) :assumption (or (not b685) (not b863) ) :assumption (or (not b695) (not b1156) ) :assumption (or (not b701) (not b1159) ) :assumption (or (not b707) (not b1162) ) :assumption (or (not b713) (not b1165) ) :assumption (or (not b695) (not b1013) ) :assumption (or (not b701) (not b1019) ) :assumption (or (not b707) (not b1025) ) :assumption (or (not b713) (not b1031) ) :assumption (or (not b695) (not b985) ) :assumption (or (not b701) (not b992) ) :assumption (or (not b707) (not b999) ) :assumption (or (not b713) (not b1006) ) :assumption (or (not b695) (not b721) ) :assumption (or (not b701) (not b727) ) :assumption (or (not b707) (not b733) ) :assumption (or (not b713) (not b739) ) :assumption (or (not b518) (not b695) ) :assumption (or (not b521) (not b701) ) :assumption (or (not b524) (not b707) ) :assumption (or (not b527) (not b713) ) :assumption (or (not b454) (not b695) ) :assumption (or (not b458) (not b701) ) :assumption (or (not b461) (not b707) ) :assumption (or (not b464) (not b713) ) :assumption (or (not b400) (not b701) ) :assumption (or (not b403) (not b707) ) :assumption (or (not b406) (not b713) ) :assumption (or (not b346) (not b701) ) :assumption (or (not b349) (not b707) ) :assumption (or (not b352) (not b713) ) :assumption (or (not b283) (not b701) ) :assumption (or (not b287) (not b707) ) :assumption (or (not b291) (not b713) ) :assumption (or (not b200) (not b701) ) :assumption (or (not b205) (not b707) ) :assumption (or (not b209) (not b713) ) :assumption (or (not b126) (not b707) ) :assumption (or (not b130) (not b713) ) :assumption (or (not b57) (not b707) ) :assumption (or (not b62) (not b713) ) :assumption (or (not b695) (not b1088) ) :assumption (or (not b701) (not b1093) ) :assumption (or (not b707) (not b1098) ) :assumption (or (not b713) (not b1103) ) :assumption (or (not b695) (not b1037) ) :assumption (or (not b701) (not b1042) ) :assumption (or (not b707) (not b1047) ) :assumption (or (not b713) (not b1052) ) :assumption (or (not b695) (not b796) ) :assumption (or (not b701) (not b801) ) :assumption (or (not b707) (not b806) ) :assumption (or (not b713) (not b811) ) :assumption (or (not b695) (not b746) ) :assumption (or (not b701) (not b751) ) :assumption (or (not b707) (not b756) ) :assumption (or (not b713) (not b761) ) :assumption (or (not b695) (not b1168) ) :assumption (or (not b701) (not b1169) ) :assumption (or (not b707) (not b1170) ) :assumption (or (not b713) (not b1171) ) :assumption (or (not b695) (not b1057) ) :assumption (or (not b701) (not b1063) ) :assumption (or (not b707) (not b1069) ) :assumption (or (not b713) (not b1075) ) :assumption (or (not b695) (not b766) ) :assumption (or (not b701) (not b772) ) :assumption (or (not b707) (not b778) ) :assumption (or (not b713) (not b784) ) :assumption (or (not b530) (not b695) ) :assumption (or (not b533) (not b701) ) :assumption (or (not b536) (not b707) ) :assumption (or (not b539) (not b713) ) :assumption (or (not b467) (not b695) ) :assumption (or (not b470) (not b701) ) :assumption (or (not b473) (not b707) ) :assumption (or (not b476) (not b713) ) :assumption (or (not b409) (not b701) ) :assumption (or (not b412) (not b707) ) :assumption (or (not b415) (not b713) ) :assumption (or (not b355) (not b701) ) :assumption (or (not b358) (not b707) ) :assumption (or (not b361) (not b713) ) :assumption (or (not b295) (not b701) ) :assumption (or (not b298) (not b707) ) :assumption (or (not b213) (not b701) ) :assumption (or (not b216) (not b707) ) :assumption (or (not b219) (not b713) ) :assumption (or (not b134) (not b695) ) :assumption (or (not b138) (not b701) ) :assumption (or (not b142) (not b707) ) :assumption (or (not b145) (not b713) ) :assumption (or (not b67) (not b695) ) :assumption (or (not b72) (not b701) ) :assumption (or (not b77) (not b707) ) :assumption (or (not b695) (not b1175) ) :assumption (or (not b701) (not b1176) ) :assumption (or (not b707) (not b1177) ) :assumption (or (not b713) (not b1178) ) :assumption (or (not b695) (not b1114) ) :assumption (or (not b701) (not b1119) ) :assumption (or (not b707) (not b1124) ) :assumption (or (not b713) (not b1129) ) :assumption (or (not b695) (not b822) ) :assumption (or (not b701) (not b827) ) :assumption (or (not b707) (not b832) ) :assumption (or (not b713) (not b837) ) :assumption (or (not b721) (not b1156) ) :assumption (or (not b727) (not b1159) ) :assumption (or (not b733) (not b1162) ) :assumption (or (not b739) (not b1165) ) :assumption (or (not b721) (not b1013) ) :assumption (or (not b727) (not b1019) ) :assumption (or (not b733) (not b1025) ) :assumption (or (not b739) (not b1031) ) :assumption (or (not b721) (not b985) ) :assumption (or (not b727) (not b992) ) :assumption (or (not b733) (not b999) ) :assumption (or (not b739) (not b1006) ) :assumption (or (not b518) (not b721) ) :assumption (or (not b521) (not b727) ) :assumption (or (not b524) (not b733) ) :assumption (or (not b527) (not b739) ) :assumption (or (not b454) (not b721) ) :assumption (or (not b458) (not b727) ) :assumption (or (not b461) (not b733) ) :assumption (or (not b464) (not b739) ) :assumption (or (not b400) (not b727) ) :assumption (or (not b403) (not b733) ) :assumption (or (not b406) (not b739) ) :assumption (or (not b346) (not b727) ) :assumption (or (not b349) (not b733) ) :assumption (or (not b352) (not b739) ) :assumption (or (not b283) (not b727) ) :assumption (or (not b287) (not b733) ) :assumption (or (not b291) (not b739) ) :assumption (or (not b200) (not b727) ) :assumption (or (not b205) (not b733) ) :assumption (or (not b209) (not b739) ) :assumption (or (not b126) (not b733) ) :assumption (or (not b130) (not b739) ) :assumption (or (not b57) (not b733) ) :assumption (or (not b62) (not b739) ) :assumption (or (not b721) (not b1088) ) :assumption (or (not b727) (not b1093) ) :assumption (or (not b733) (not b1098) ) :assumption (or (not b739) (not b1103) ) :assumption (or (not b721) (not b1037) ) :assumption (or (not b727) (not b1042) ) :assumption (or (not b733) (not b1047) ) :assumption (or (not b739) (not b1052) ) :assumption (or (not b721) (not b796) ) :assumption (or (not b727) (not b801) ) :assumption (or (not b733) (not b806) ) :assumption (or (not b739) (not b811) ) :assumption (or (not b721) (not b746) ) :assumption (or (not b727) (not b751) ) :assumption (or (not b733) (not b756) ) :assumption (or (not b739) (not b761) ) :assumption (or (not b721) (not b1175) ) :assumption (or (not b727) (not b1176) ) :assumption (or (not b733) (not b1177) ) :assumption (or (not b739) (not b1178) ) :assumption (or (not b721) (not b1114) ) :assumption (or (not b727) (not b1119) ) :assumption (or (not b733) (not b1124) ) :assumption (or (not b739) (not b1129) ) :assumption (or (not b721) (not b822) ) :assumption (or (not b727) (not b827) ) :assumption (or (not b733) (not b832) ) :assumption (or (not b739) (not b837) ) :assumption (or (not b542) (not b721) ) :assumption (or (not b545) (not b727) ) :assumption (or (not b548) (not b733) ) :assumption (or (not b551) (not b739) ) :assumption (or (not b479) (not b721) ) :assumption (or (not b482) (not b727) ) :assumption (or (not b485) (not b733) ) :assumption (or (not b488) (not b739) ) :assumption (or (not b418) (not b727) ) :assumption (or (not b421) (not b733) ) :assumption (or (not b424) (not b739) ) :assumption (or (not b364) (not b727) ) :assumption (or (not b367) (not b733) ) :assumption (or (not b370) (not b739) ) :assumption (or (not b306) (not b721) ) :assumption (or (not b310) (not b727) ) :assumption (or (not b313) (not b733) ) :assumption (or (not b316) (not b739) ) :assumption (or (not b226) (not b721) ) :assumption (or (not b231) (not b727) ) :assumption (or (not b235) (not b733) ) :assumption (or (not b149) (not b733) ) :assumption (or (not b82) (not b733) ) :assumption (or (not b86) (not b739) ) :assumption (or (not b721) (not b1168) ) :assumption (or (not b727) (not b1169) ) :assumption (or (not b733) (not b1170) ) :assumption (or (not b739) (not b1171) ) :assumption (or (not b721) (not b1057) ) :assumption (or (not b727) (not b1063) ) :assumption (or (not b733) (not b1069) ) :assumption (or (not b739) (not b1075) ) :assumption (or (not b721) (not b766) ) :assumption (or (not b727) (not b772) ) :assumption (or (not b733) (not b778) ) :assumption (or (not b739) (not b784) ) :assumption (or (not b746) (not b1168) ) :assumption (or (not b751) (not b1169) ) :assumption (or (not b756) (not b1170) ) :assumption (or (not b761) (not b1171) ) :assumption (or (not b746) (not b1057) ) :assumption (or (not b751) (not b1063) ) :assumption (or (not b756) (not b1069) ) :assumption (or (not b761) (not b1075) ) :assumption (or (not b746) (not b1037) ) :assumption (or (not b751) (not b1042) ) :assumption (or (not b756) (not b1047) ) :assumption (or (not b761) (not b1052) ) :assumption (or (not b746) (not b766) ) :assumption (or (not b751) (not b772) ) :assumption (or (not b756) (not b778) ) :assumption (or (not b761) (not b784) ) :assumption (or (not b530) (not b746) ) :assumption (or (not b533) (not b751) ) :assumption (or (not b536) (not b756) ) :assumption (or (not b539) (not b761) ) :assumption (or (not b467) (not b746) ) :assumption (or (not b470) (not b751) ) :assumption (or (not b473) (not b756) ) :assumption (or (not b476) (not b761) ) :assumption (or (not b409) (not b751) ) :assumption (or (not b412) (not b756) ) :assumption (or (not b415) (not b761) ) :assumption (or (not b355) (not b751) ) :assumption (or (not b358) (not b756) ) :assumption (or (not b361) (not b761) ) :assumption (or (not b295) (not b751) ) :assumption (or (not b298) (not b756) ) :assumption (or (not b213) (not b751) ) :assumption (or (not b216) (not b756) ) :assumption (or (not b219) (not b761) ) :assumption (or (not b134) (not b746) ) :assumption (or (not b138) (not b751) ) :assumption (or (not b142) (not b756) ) :assumption (or (not b145) (not b761) ) :assumption (or (not b67) (not b746) ) :assumption (or (not b72) (not b751) ) :assumption (or (not b77) (not b756) ) :assumption (or (not b746) (not b1114) ) :assumption (or (not b751) (not b1119) ) :assumption (or (not b756) (not b1124) ) :assumption (or (not b761) (not b1129) ) :assumption (or (not b746) (not b985) ) :assumption (or (not b751) (not b992) ) :assumption (or (not b756) (not b999) ) :assumption (or (not b761) (not b1006) ) :assumption (or (not b746) (not b822) ) :assumption (or (not b751) (not b827) ) :assumption (or (not b756) (not b832) ) :assumption (or (not b761) (not b837) ) :assumption (or (not b746) (not b1156) ) :assumption (or (not b751) (not b1159) ) :assumption (or (not b756) (not b1162) ) :assumption (or (not b761) (not b1165) ) :assumption (or (not b746) (not b1013) ) :assumption (or (not b751) (not b1019) ) :assumption (or (not b756) (not b1025) ) :assumption (or (not b761) (not b1031) ) :assumption (or (not b518) (not b746) ) :assumption (or (not b521) (not b751) ) :assumption (or (not b524) (not b756) ) :assumption (or (not b527) (not b761) ) :assumption (or (not b454) (not b746) ) :assumption (or (not b458) (not b751) ) :assumption (or (not b461) (not b756) ) :assumption (or (not b464) (not b761) ) :assumption (or (not b400) (not b751) ) :assumption (or (not b403) (not b756) ) :assumption (or (not b406) (not b761) ) :assumption (or (not b346) (not b751) ) :assumption (or (not b349) (not b756) ) :assumption (or (not b352) (not b761) ) :assumption (or (not b283) (not b751) ) :assumption (or (not b287) (not b756) ) :assumption (or (not b291) (not b761) ) :assumption (or (not b200) (not b751) ) :assumption (or (not b205) (not b756) ) :assumption (or (not b209) (not b761) ) :assumption (or (not b126) (not b756) ) :assumption (or (not b130) (not b761) ) :assumption (or (not b57) (not b756) ) :assumption (or (not b62) (not b761) ) :assumption (or (not b746) (not b1175) ) :assumption (or (not b751) (not b1176) ) :assumption (or (not b756) (not b1177) ) :assumption (or (not b761) (not b1178) ) :assumption (or (not b746) (not b1088) ) :assumption (or (not b751) (not b1093) ) :assumption (or (not b756) (not b1098) ) :assumption (or (not b761) (not b1103) ) :assumption (or (not b746) (not b796) ) :assumption (or (not b751) (not b801) ) :assumption (or (not b756) (not b806) ) :assumption (or (not b761) (not b811) ) :assumption (or (not b766) (not b1168) ) :assumption (or (not b772) (not b1169) ) :assumption (or (not b778) (not b1170) ) :assumption (or (not b784) (not b1171) ) :assumption (or (not b766) (not b1057) ) :assumption (or (not b772) (not b1063) ) :assumption (or (not b778) (not b1069) ) :assumption (or (not b784) (not b1075) ) :assumption (or (not b766) (not b1037) ) :assumption (or (not b772) (not b1042) ) :assumption (or (not b778) (not b1047) ) :assumption (or (not b784) (not b1052) ) :assumption (or (not b530) (not b766) ) :assumption (or (not b533) (not b772) ) :assumption (or (not b536) (not b778) ) :assumption (or (not b539) (not b784) ) :assumption (or (not b467) (not b766) ) :assumption (or (not b470) (not b772) ) :assumption (or (not b473) (not b778) ) :assumption (or (not b476) (not b784) ) :assumption (or (not b409) (not b772) ) :assumption (or (not b412) (not b778) ) :assumption (or (not b415) (not b784) ) :assumption (or (not b355) (not b772) ) :assumption (or (not b358) (not b778) ) :assumption (or (not b361) (not b784) ) :assumption (or (not b295) (not b772) ) :assumption (or (not b298) (not b778) ) :assumption (or (not b213) (not b772) ) :assumption (or (not b216) (not b778) ) :assumption (or (not b219) (not b784) ) :assumption (or (not b134) (not b766) ) :assumption (or (not b138) (not b772) ) :assumption (or (not b142) (not b778) ) :assumption (or (not b145) (not b784) ) :assumption (or (not b67) (not b766) ) :assumption (or (not b72) (not b772) ) :assumption (or (not b77) (not b778) ) :assumption (or (not b766) (not b1114) ) :assumption (or (not b772) (not b1119) ) :assumption (or (not b778) (not b1124) ) :assumption (or (not b784) (not b1129) ) :assumption (or (not b766) (not b985) ) :assumption (or (not b772) (not b992) ) :assumption (or (not b778) (not b999) ) :assumption (or (not b784) (not b1006) ) :assumption (or (not b766) (not b822) ) :assumption (or (not b772) (not b827) ) :assumption (or (not b778) (not b832) ) :assumption (or (not b784) (not b837) ) :assumption (or (not b766) (not b1175) ) :assumption (or (not b772) (not b1176) ) :assumption (or (not b778) (not b1177) ) :assumption (or (not b784) (not b1178) ) :assumption (or (not b766) (not b1088) ) :assumption (or (not b772) (not b1093) ) :assumption (or (not b778) (not b1098) ) :assumption (or (not b784) (not b1103) ) :assumption (or (not b766) (not b796) ) :assumption (or (not b772) (not b801) ) :assumption (or (not b778) (not b806) ) :assumption (or (not b784) (not b811) ) :assumption (or (not b542) (not b766) ) :assumption (or (not b545) (not b772) ) :assumption (or (not b548) (not b778) ) :assumption (or (not b551) (not b784) ) :assumption (or (not b479) (not b766) ) :assumption (or (not b482) (not b772) ) :assumption (or (not b485) (not b778) ) :assumption (or (not b488) (not b784) ) :assumption (or (not b418) (not b772) ) :assumption (or (not b421) (not b778) ) :assumption (or (not b424) (not b784) ) :assumption (or (not b364) (not b772) ) :assumption (or (not b367) (not b778) ) :assumption (or (not b370) (not b784) ) :assumption (or (not b306) (not b766) ) :assumption (or (not b310) (not b772) ) :assumption (or (not b313) (not b778) ) :assumption (or (not b316) (not b784) ) :assumption (or (not b226) (not b766) ) :assumption (or (not b231) (not b772) ) :assumption (or (not b235) (not b778) ) :assumption (or (not b149) (not b778) ) :assumption (or (not b82) (not b778) ) :assumption (or (not b86) (not b784) ) :assumption (or (not b766) (not b1156) ) :assumption (or (not b772) (not b1159) ) :assumption (or (not b778) (not b1162) ) :assumption (or (not b784) (not b1165) ) :assumption (or (not b766) (not b1013) ) :assumption (or (not b772) (not b1019) ) :assumption (or (not b778) (not b1025) ) :assumption (or (not b784) (not b1031) ) :assumption (or (not b790) (not b1172) ) :assumption (or (not b796) (not b1175) ) :assumption (or (not b801) (not b1176) ) :assumption (or (not b806) (not b1177) ) :assumption (or (not b811) (not b1178) ) :assumption (or (not b790) (not b1108) ) :assumption (or (not b796) (not b1114) ) :assumption (or (not b801) (not b1119) ) :assumption (or (not b806) (not b1124) ) :assumption (or (not b811) (not b1129) ) :assumption (or (not b790) (not b1081) ) :assumption (or (not b796) (not b1088) ) :assumption (or (not b801) (not b1093) ) :assumption (or (not b806) (not b1098) ) :assumption (or (not b811) (not b1103) ) :assumption (or (not b790) (not b816) ) :assumption (or (not b796) (not b822) ) :assumption (or (not b801) (not b827) ) :assumption (or (not b806) (not b832) ) :assumption (or (not b811) (not b837) ) :assumption (or (not b542) (not b796) ) :assumption (or (not b545) (not b801) ) :assumption (or (not b548) (not b806) ) :assumption (or (not b551) (not b811) ) :assumption (or (not b479) (not b796) ) :assumption (or (not b482) (not b801) ) :assumption (or (not b485) (not b806) ) :assumption (or (not b488) (not b811) ) :assumption (or (not b418) (not b801) ) :assumption (or (not b421) (not b806) ) :assumption (or (not b424) (not b811) ) :assumption (or (not b364) (not b801) ) :assumption (or (not b367) (not b806) ) :assumption (or (not b370) (not b811) ) :assumption (or (not b302) (not b790) ) :assumption (or (not b306) (not b796) ) :assumption (or (not b310) (not b801) ) :assumption (or (not b313) (not b806) ) :assumption (or (not b316) (not b811) ) :assumption (or (not b222) (not b790) ) :assumption (or (not b226) (not b796) ) :assumption (or (not b231) (not b801) ) :assumption (or (not b235) (not b806) ) :assumption (or (not b149) (not b806) ) :assumption (or (not b82) (not b806) ) :assumption (or (not b86) (not b811) ) :assumption (or (not b796) (not b1057) ) :assumption (or (not b801) (not b1063) ) :assumption (or (not b806) (not b1069) ) :assumption (or (not b811) (not b1075) ) :assumption (or (not b796) (not b1013) ) :assumption (or (not b801) (not b1019) ) :assumption (or (not b806) (not b1025) ) :assumption (or (not b811) (not b1031) ) :assumption (or (not b796) (not b1156) ) :assumption (or (not b801) (not b1159) ) :assumption (or (not b806) (not b1162) ) :assumption (or (not b811) (not b1165) ) :assumption (or (not b796) (not b985) ) :assumption (or (not b801) (not b992) ) :assumption (or (not b806) (not b999) ) :assumption (or (not b811) (not b1006) ) :assumption (or (not b518) (not b796) ) :assumption (or (not b521) (not b801) ) :assumption (or (not b524) (not b806) ) :assumption (or (not b527) (not b811) ) :assumption (or (not b454) (not b796) ) :assumption (or (not b458) (not b801) ) :assumption (or (not b461) (not b806) ) :assumption (or (not b464) (not b811) ) :assumption (or (not b400) (not b801) ) :assumption (or (not b403) (not b806) ) :assumption (or (not b406) (not b811) ) :assumption (or (not b346) (not b801) ) :assumption (or (not b349) (not b806) ) :assumption (or (not b352) (not b811) ) :assumption (or (not b283) (not b801) ) :assumption (or (not b287) (not b806) ) :assumption (or (not b291) (not b811) ) :assumption (or (not b200) (not b801) ) :assumption (or (not b205) (not b806) ) :assumption (or (not b209) (not b811) ) :assumption (or (not b126) (not b806) ) :assumption (or (not b130) (not b811) ) :assumption (or (not b57) (not b806) ) :assumption (or (not b62) (not b811) ) :assumption (or (not b796) (not b1168) ) :assumption (or (not b801) (not b1169) ) :assumption (or (not b806) (not b1170) ) :assumption (or (not b811) (not b1171) ) :assumption (or (not b796) (not b1037) ) :assumption (or (not b801) (not b1042) ) :assumption (or (not b806) (not b1047) ) :assumption (or (not b811) (not b1052) ) :assumption (or (not b816) (not b1172) ) :assumption (or (not b822) (not b1175) ) :assumption (or (not b827) (not b1176) ) :assumption (or (not b832) (not b1177) ) :assumption (or (not b837) (not b1178) ) :assumption (or (not b816) (not b1108) ) :assumption (or (not b822) (not b1114) ) :assumption (or (not b827) (not b1119) ) :assumption (or (not b832) (not b1124) ) :assumption (or (not b837) (not b1129) ) :assumption (or (not b816) (not b1081) ) :assumption (or (not b822) (not b1088) ) :assumption (or (not b827) (not b1093) ) :assumption (or (not b832) (not b1098) ) :assumption (or (not b837) (not b1103) ) :assumption (or (not b542) (not b822) ) :assumption (or (not b545) (not b827) ) :assumption (or (not b548) (not b832) ) :assumption (or (not b551) (not b837) ) :assumption (or (not b479) (not b822) ) :assumption (or (not b482) (not b827) ) :assumption (or (not b485) (not b832) ) :assumption (or (not b488) (not b837) ) :assumption (or (not b418) (not b827) ) :assumption (or (not b421) (not b832) ) :assumption (or (not b424) (not b837) ) :assumption (or (not b364) (not b827) ) :assumption (or (not b367) (not b832) ) :assumption (or (not b370) (not b837) ) :assumption (or (not b302) (not b816) ) :assumption (or (not b306) (not b822) ) :assumption (or (not b310) (not b827) ) :assumption (or (not b313) (not b832) ) :assumption (or (not b316) (not b837) ) :assumption (or (not b222) (not b816) ) :assumption (or (not b226) (not b822) ) :assumption (or (not b231) (not b827) ) :assumption (or (not b235) (not b832) ) :assumption (or (not b149) (not b832) ) :assumption (or (not b82) (not b832) ) :assumption (or (not b86) (not b837) ) :assumption (or (not b822) (not b1057) ) :assumption (or (not b827) (not b1063) ) :assumption (or (not b832) (not b1069) ) :assumption (or (not b837) (not b1075) ) :assumption (or (not b822) (not b1013) ) :assumption (or (not b827) (not b1019) ) :assumption (or (not b832) (not b1025) ) :assumption (or (not b837) (not b1031) ) :assumption (or (not b822) (not b1168) ) :assumption (or (not b827) (not b1169) ) :assumption (or (not b832) (not b1170) ) :assumption (or (not b837) (not b1171) ) :assumption (or (not b822) (not b1037) ) :assumption (or (not b827) (not b1042) ) :assumption (or (not b832) (not b1047) ) :assumption (or (not b837) (not b1052) ) :assumption (or (not b530) (not b822) ) :assumption (or (not b533) (not b827) ) :assumption (or (not b536) (not b832) ) :assumption (or (not b539) (not b837) ) :assumption (or (not b467) (not b822) ) :assumption (or (not b470) (not b827) ) :assumption (or (not b473) (not b832) ) :assumption (or (not b476) (not b837) ) :assumption (or (not b409) (not b827) ) :assumption (or (not b412) (not b832) ) :assumption (or (not b415) (not b837) ) :assumption (or (not b355) (not b827) ) :assumption (or (not b358) (not b832) ) :assumption (or (not b361) (not b837) ) :assumption (or (not b295) (not b827) ) :assumption (or (not b298) (not b832) ) :assumption (or (not b213) (not b827) ) :assumption (or (not b216) (not b832) ) :assumption (or (not b219) (not b837) ) :assumption (or (not b134) (not b822) ) :assumption (or (not b138) (not b827) ) :assumption (or (not b142) (not b832) ) :assumption (or (not b145) (not b837) ) :assumption (or (not b67) (not b822) ) :assumption (or (not b72) (not b827) ) :assumption (or (not b77) (not b832) ) :assumption (or (not b822) (not b1156) ) :assumption (or (not b827) (not b1159) ) :assumption (or (not b832) (not b1162) ) :assumption (or (not b837) (not b1165) ) :assumption (or (not b822) (not b985) ) :assumption (or (not b827) (not b992) ) :assumption (or (not b832) (not b999) ) :assumption (or (not b837) (not b1006) ) :assumption (or (not b842) (not b1133) ) :assumption (or (not b849) (not b1136) ) :assumption (or (not b856) (not b1139) ) :assumption (or (not b863) (not b1142) ) :assumption (or (not b842) (not b872) ) :assumption (or (not b849) (not b878) ) :assumption (or (not b856) (not b884) ) :assumption (or (not b863) (not b890) ) :assumption (or (not b849) (not b944) ) :assumption (or (not b856) (not b949) ) :assumption (or (not b863) (not b954) ) :assumption (or (not b849) (not b898) ) :assumption (or (not b856) (not b903) ) :assumption (or (not b863) (not b908) ) :assumption (or (not b849) (not b1148) ) :assumption (or (not b856) (not b1149) ) :assumption (or (not b863) (not b1150) ) :assumption (or (not b849) (not b920) ) :assumption (or (not b856) (not b926) ) :assumption (or (not b863) (not b932) ) :assumption (or (not b849) (not b1152) ) :assumption (or (not b856) (not b1153) ) :assumption (or (not b863) (not b1154) ) :assumption (or (not b849) (not b965) ) :assumption (or (not b856) (not b970) ) :assumption (or (not b863) (not b975) ) :assumption (or (not b872) (not b1133) ) :assumption (or (not b878) (not b1136) ) :assumption (or (not b884) (not b1139) ) :assumption (or (not b890) (not b1142) ) :assumption (or (not b878) (not b944) ) :assumption (or (not b884) (not b949) ) :assumption (or (not b890) (not b954) ) :assumption (or (not b878) (not b898) ) :assumption (or (not b884) (not b903) ) :assumption (or (not b890) (not b908) ) :assumption (or (not b878) (not b1152) ) :assumption (or (not b884) (not b1153) ) :assumption (or (not b890) (not b1154) ) :assumption (or (not b878) (not b965) ) :assumption (or (not b884) (not b970) ) :assumption (or (not b890) (not b975) ) :assumption (or (not b878) (not b1148) ) :assumption (or (not b884) (not b1149) ) :assumption (or (not b890) (not b1150) ) :assumption (or (not b878) (not b920) ) :assumption (or (not b884) (not b926) ) :assumption (or (not b890) (not b932) ) :assumption (or (not b898) (not b1148) ) :assumption (or (not b903) (not b1149) ) :assumption (or (not b908) (not b1150) ) :assumption (or (not b913) (not b1151) ) :assumption (or (not b898) (not b920) ) :assumption (or (not b903) (not b926) ) :assumption (or (not b908) (not b932) ) :assumption (or (not b913) (not b938) ) :assumption (or (not b898) (not b965) ) :assumption (or (not b903) (not b970) ) :assumption (or (not b908) (not b975) ) :assumption (or (not b913) (not b980) ) :assumption (or (not b898) (not b1136) ) :assumption (or (not b903) (not b1139) ) :assumption (or (not b908) (not b1142) ) :assumption (or (not b913) (not b1145) ) :assumption (or (not b898) (not b1152) ) :assumption (or (not b903) (not b1153) ) :assumption (or (not b908) (not b1154) ) :assumption (or (not b913) (not b1155) ) :assumption (or (not b898) (not b944) ) :assumption (or (not b903) (not b949) ) :assumption (or (not b908) (not b954) ) :assumption (or (not b913) (not b959) ) :assumption (or (not b920) (not b1148) ) :assumption (or (not b926) (not b1149) ) :assumption (or (not b932) (not b1150) ) :assumption (or (not b938) (not b1151) ) :assumption (or (not b920) (not b965) ) :assumption (or (not b926) (not b970) ) :assumption (or (not b932) (not b975) ) :assumption (or (not b938) (not b980) ) :assumption (or (not b920) (not b1152) ) :assumption (or (not b926) (not b1153) ) :assumption (or (not b932) (not b1154) ) :assumption (or (not b938) (not b1155) ) :assumption (or (not b920) (not b944) ) :assumption (or (not b926) (not b949) ) :assumption (or (not b932) (not b954) ) :assumption (or (not b938) (not b959) ) :assumption (or (not b920) (not b1136) ) :assumption (or (not b926) (not b1139) ) :assumption (or (not b932) (not b1142) ) :assumption (or (not b938) (not b1145) ) :assumption (or (not b944) (not b1152) ) :assumption (or (not b949) (not b1153) ) :assumption (or (not b954) (not b1154) ) :assumption (or (not b959) (not b1155) ) :assumption (or (not b944) (not b965) ) :assumption (or (not b949) (not b970) ) :assumption (or (not b954) (not b975) ) :assumption (or (not b959) (not b980) ) :assumption (or (not b944) (not b1136) ) :assumption (or (not b949) (not b1139) ) :assumption (or (not b954) (not b1142) ) :assumption (or (not b959) (not b1145) ) :assumption (or (not b944) (not b1148) ) :assumption (or (not b949) (not b1149) ) :assumption (or (not b954) (not b1150) ) :assumption (or (not b959) (not b1151) ) :assumption (or (not b965) (not b1152) ) :assumption (or (not b970) (not b1153) ) :assumption (or (not b975) (not b1154) ) :assumption (or (not b980) (not b1155) ) :assumption (or (not b965) (not b1148) ) :assumption (or (not b970) (not b1149) ) :assumption (or (not b975) (not b1150) ) :assumption (or (not b980) (not b1151) ) :assumption (or (not b965) (not b1136) ) :assumption (or (not b970) (not b1139) ) :assumption (or (not b975) (not b1142) ) :assumption (or (not b980) (not b1145) ) :assumption (or (not b985) (not b1156) ) :assumption (or (not b992) (not b1159) ) :assumption (or (not b999) (not b1162) ) :assumption (or (not b1006) (not b1165) ) :assumption (or (not b985) (not b1013) ) :assumption (or (not b992) (not b1019) ) :assumption (or (not b999) (not b1025) ) :assumption (or (not b1006) (not b1031) ) :assumption (or (not b985) (not b1088) ) :assumption (or (not b992) (not b1093) ) :assumption (or (not b999) (not b1098) ) :assumption (or (not b1006) (not b1103) ) :assumption (or (not b985) (not b1037) ) :assumption (or (not b992) (not b1042) ) :assumption (or (not b999) (not b1047) ) :assumption (or (not b1006) (not b1052) ) :assumption (or (not b985) (not b1168) ) :assumption (or (not b992) (not b1169) ) :assumption (or (not b999) (not b1170) ) :assumption (or (not b1006) (not b1171) ) :assumption (or (not b985) (not b1057) ) :assumption (or (not b992) (not b1063) ) :assumption (or (not b999) (not b1069) ) :assumption (or (not b1006) (not b1075) ) :assumption (or (not b985) (not b1175) ) :assumption (or (not b992) (not b1176) ) :assumption (or (not b999) (not b1177) ) :assumption (or (not b1006) (not b1178) ) :assumption (or (not b985) (not b1114) ) :assumption (or (not b992) (not b1119) ) :assumption (or (not b999) (not b1124) ) :assumption (or (not b1006) (not b1129) ) :assumption (or (not b1013) (not b1156) ) :assumption (or (not b1019) (not b1159) ) :assumption (or (not b1025) (not b1162) ) :assumption (or (not b1031) (not b1165) ) :assumption (or (not b1013) (not b1088) ) :assumption (or (not b1019) (not b1093) ) :assumption (or (not b1025) (not b1098) ) :assumption (or (not b1031) (not b1103) ) :assumption (or (not b1013) (not b1037) ) :assumption (or (not b1019) (not b1042) ) :assumption (or (not b1025) (not b1047) ) :assumption (or (not b1031) (not b1052) ) :assumption (or (not b1013) (not b1175) ) :assumption (or (not b1019) (not b1176) ) :assumption (or (not b1025) (not b1177) ) :assumption (or (not b1031) (not b1178) ) :assumption (or (not b1013) (not b1114) ) :assumption (or (not b1019) (not b1119) ) :assumption (or (not b1025) (not b1124) ) :assumption (or (not b1031) (not b1129) ) :assumption (or (not b1013) (not b1168) ) :assumption (or (not b1019) (not b1169) ) :assumption (or (not b1025) (not b1170) ) :assumption (or (not b1031) (not b1171) ) :assumption (or (not b1013) (not b1057) ) :assumption (or (not b1019) (not b1063) ) :assumption (or (not b1025) (not b1069) ) :assumption (or (not b1031) (not b1075) ) :assumption (or (not b1037) (not b1168) ) :assumption (or (not b1042) (not b1169) ) :assumption (or (not b1047) (not b1170) ) :assumption (or (not b1052) (not b1171) ) :assumption (or (not b1037) (not b1057) ) :assumption (or (not b1042) (not b1063) ) :assumption (or (not b1047) (not b1069) ) :assumption (or (not b1052) (not b1075) ) :assumption (or (not b1037) (not b1114) ) :assumption (or (not b1042) (not b1119) ) :assumption (or (not b1047) (not b1124) ) :assumption (or (not b1052) (not b1129) ) :assumption (or (not b1037) (not b1156) ) :assumption (or (not b1042) (not b1159) ) :assumption (or (not b1047) (not b1162) ) :assumption (or (not b1052) (not b1165) ) :assumption (or (not b1037) (not b1175) ) :assumption (or (not b1042) (not b1176) ) :assumption (or (not b1047) (not b1177) ) :assumption (or (not b1052) (not b1178) ) :assumption (or (not b1037) (not b1088) ) :assumption (or (not b1042) (not b1093) ) :assumption (or (not b1047) (not b1098) ) :assumption (or (not b1052) (not b1103) ) :assumption (or (not b1057) (not b1168) ) :assumption (or (not b1063) (not b1169) ) :assumption (or (not b1069) (not b1170) ) :assumption (or (not b1075) (not b1171) ) :assumption (or (not b1057) (not b1114) ) :assumption (or (not b1063) (not b1119) ) :assumption (or (not b1069) (not b1124) ) :assumption (or (not b1075) (not b1129) ) :assumption (or (not b1057) (not b1175) ) :assumption (or (not b1063) (not b1176) ) :assumption (or (not b1069) (not b1177) ) :assumption (or (not b1075) (not b1178) ) :assumption (or (not b1057) (not b1088) ) :assumption (or (not b1063) (not b1093) ) :assumption (or (not b1069) (not b1098) ) :assumption (or (not b1075) (not b1103) ) :assumption (or (not b1057) (not b1156) ) :assumption (or (not b1063) (not b1159) ) :assumption (or (not b1069) (not b1162) ) :assumption (or (not b1075) (not b1165) ) :assumption (or (not b1081) (not b1172) ) :assumption (or (not b1088) (not b1175) ) :assumption (or (not b1093) (not b1176) ) :assumption (or (not b1098) (not b1177) ) :assumption (or (not b1103) (not b1178) ) :assumption (or (not b1081) (not b1108) ) :assumption (or (not b1088) (not b1114) ) :assumption (or (not b1093) (not b1119) ) :assumption (or (not b1098) (not b1124) ) :assumption (or (not b1103) (not b1129) ) :assumption (or (not b1088) (not b1156) ) :assumption (or (not b1093) (not b1159) ) :assumption (or (not b1098) (not b1162) ) :assumption (or (not b1103) (not b1165) ) :assumption (or (not b1088) (not b1168) ) :assumption (or (not b1093) (not b1169) ) :assumption (or (not b1098) (not b1170) ) :assumption (or (not b1103) (not b1171) ) :assumption (or (not b1108) (not b1172) ) :assumption (or (not b1114) (not b1175) ) :assumption (or (not b1119) (not b1176) ) :assumption (or (not b1124) (not b1177) ) :assumption (or (not b1129) (not b1178) ) :assumption (or (not b1114) (not b1168) ) :assumption (or (not b1119) (not b1169) ) :assumption (or (not b1124) (not b1170) ) :assumption (or (not b1129) (not b1171) ) :assumption (or (not b1114) (not b1156) ) :assumption (or (not b1119) (not b1159) ) :assumption (or (not b1124) (not b1162) ) :assumption (or (not b1129) (not b1165) ) :assumption (or (not b1136) (not b1152) ) :assumption (or (not b1139) (not b1153) ) :assumption (or (not b1142) (not b1154) ) :assumption (or (not b1145) (not b1155) ) :assumption (or (not b1136) (not b1148) ) :assumption (or (not b1139) (not b1149) ) :assumption (or (not b1142) (not b1150) ) :assumption (or (not b1145) (not b1151) ) :assumption (or (not b1148) (not b1152) ) :assumption (or (not b1149) (not b1153) ) :assumption (or (not b1150) (not b1154) ) :assumption (or (not b1151) (not b1155) ) :assumption (or (not b1156) (not b1175) ) :assumption (or (not b1159) (not b1176) ) :assumption (or (not b1162) (not b1177) ) :assumption (or (not b1165) (not b1178) ) :assumption (or (not b1156) (not b1168) ) :assumption (or (not b1159) (not b1169) ) :assumption (or (not b1162) (not b1170) ) :assumption (or (not b1165) (not b1171) ) :assumption (or (not b1168) (not b1175) ) :assumption (or (not b1169) (not b1176) ) :assumption (or (not b1170) (not b1177) ) :assumption (or (not b1171) (not b1178) ) :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 3624) :assumption (= r11 0) :assumption (= r12 2328) :assumption (<= (+ (* 1 r2) (* 1 r13)) 4506) :assumption (= r19 0) :assumption (= r27 0) :assumption (= r37 0) :assumption (= r45 0) :assumption (= r55 0) :assumption (= r66 0) :assumption (= r72 0) :assumption (= r82 0) :assumption (= r177 0) :assumption (= r178 0) :assumption (= r187 0) :assumption (= r188 0) :assumption (= r289 0) :assumption (= r290 0) :assumption (= r299 0) :assumption (= r300 0) :assumption (= (- r282 r9) 0) :assumption (= (- (- (- (- (- r285 r282) r73) r52) r32) r16) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r288 r285) r151) r148) r145) r130) r127) r124) r112) r109) r106) r94) r91) r88) r74) r70) r67) r53) r49) r46) r33) r17) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r309 r288) r152) r149) r146) r131) r128) r125) r113) r110) r107) r95) r92) r89) r75) r71) r68) r54) r50) r47) r36) r34) r30) r20) r18) r14) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r393 r309) r153) r150) r147) r132) r129) r126) r114) r111) r108) r96) r93) r90) r76) r72) r69) r55) r51) r48) r37) r35) r31) r21) r19) r15) 0) :assumption (= (- (- (- r336 r11) r83) r62) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- r339 r336) r162) r158) r154) r141) r137) r133) r84) r63) r40) r24) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r342 r339) r163) r159) r155) r142) r138) r134) r121) r118) r115) r103) r100) r97) r85) r80) r77) r64) r59) r56) r41) r25) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r345 r342) r164) r160) r156) r143) r139) r135) r122) r119) r116) r104) r101) r98) r86) r81) r78) r65) r60) r57) r44) r42) r38) r28) r26) r22) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r394 r345) r165) r161) r157) r144) r140) r136) r123) r120) r117) r105) r102) r99) r87) r82) r79) r66) r61) r58) r45) r43) r39) r29) r27) r23) 0) :assumption (= (- (- (- (- (- (- (- (- (- r395 r8) r380) r370) r291) r278) r268) r258) r179) r166) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r396 r395) r382) r372) r362) r354) r346) r334) r326) r318) r310) r301) r293) r280) r270) r260) r250) r242) r234) r222) r214) r206) r198) r189) r181) r168) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r397 r396) r384) r374) r364) r356) r348) r337) r328) r320) r312) r303) r295) r283) r272) r262) r252) r244) r236) r225) r216) r208) r200) r191) r183) r171) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r398 r397) r386) r376) r366) r358) r350) r340) r330) r322) r314) r305) r297) r286) r274) r264) r254) r246) r238) r228) r218) r210) r202) r193) r185) r174) 0) :assumption (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r13 r398) r388) r378) r368) r360) r352) r343) r332) r324) r316) r307) r299) r289) r276) r266) r256) r248) r240) r231) r220) r212) r204) r195) r187) r177) 0) :formula (not false) )