(benchmark p2_zenonumeric_s6.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 ((b14))
  :extrapreds ((b20))
  :extrapreds ((b26))
  :extrapreds ((b32))
  :extrapreds ((b40))
  :extrapreds ((b46))
  :extrapreds ((b51))
  :extrapreds ((b56))
  :extrapreds ((b62))
  :extrapreds ((b67))
  :extrapreds ((b72))
  :extrapreds ((b78))
  :extrapreds ((b83))
  :extrapreds ((b89))
  :extrapreds ((b95))
  :extrapreds ((b101))
  :extrapreds ((b105))
  :extrapreds ((b109))
  :extrapreds ((b113))
  :extrapreds ((b118))
  :extrapreds ((b122))
  :extrapreds ((b126))
  :extrapreds ((b131))
  :extrapreds ((b136))
  :extrapreds ((b141))
  :extrapreds ((b146))
  :extrapreds ((b151))
  :extrapreds ((b156))
  :extrapreds ((b161))
  :extrapreds ((b166))
  :extrapreds ((b170))
  :extrapreds ((b174))
  :extrapreds ((b177))
  :extrapreds ((b180))
  :extrapreds ((b183))
  :extrapreds ((b186))
  :extrapreds ((b189))
  :extrapreds ((b192))
  :extrapreds ((b195))
  :extrapreds ((b198))
  :extrapreds ((b202))
  :extrapreds ((b205))
  :extrapreds ((b208))
  :extrapreds ((b211))
  :extrapreds ((b214))
  :extrapreds ((b217))
  :extrapreds ((b220))
  :extrapreds ((b223))
  :extrapreds ((b226))
  :extrapreds ((b229))
  :extrapreds ((b232))
  :extrapreds ((b235))
  :extrapreds ((b238))
  :extrapreds ((b241))
  :extrapreds ((b244))
  :extrapreds ((b247))
  :extrapreds ((b250))
  :extrapreds ((b253))
  :extrapreds ((b256))
  :extrapreds ((b259))
  :extrapreds ((b262))
  :extrapreds ((b265))
  :extrapreds ((b268))
  :extrapreds ((b271))
  :extrapreds ((b274))
  :extrapreds ((b277))
  :extrapreds ((b280))
  :extrapreds ((b283))
  :extrapreds ((b289))
  :extrapreds ((b295))
  :extrapreds ((b301))
  :extrapreds ((b310))
  :extrapreds ((b316))
  :extrapreds ((b322))
  :extrapreds ((b328))
  :extrapreds ((b337))
  :extrapreds ((b342))
  :extrapreds ((b347))
  :extrapreds ((b352))
  :extrapreds ((b357))
  :extrapreds ((b363))
  :extrapreds ((b369))
  :extrapreds ((b375))
  :extrapreds ((b381))
  :extrapreds ((b387))
  :extrapreds ((b393))
  :extrapreds ((b400))
  :extrapreds ((b405))
  :extrapreds ((b410))
  :extrapreds ((b415))
  :extrapreds ((b420))
  :extrapreds ((b426))
  :extrapreds ((b432))
  :extrapreds ((b437))
  :extrapreds ((b442))
  :extrapreds ((b447))
  :extrapreds ((b452))
  :extrapreds ((b457))
  :extrapreds ((b464))
  :extrapreds ((b471))
  :extrapreds ((b478))
  :extrapreds ((b487))
  :extrapreds ((b493))
  :extrapreds ((b499))
  :extrapreds ((b505))
  :extrapreds ((b513))
  :extrapreds ((b518))
  :extrapreds ((b523))
  :extrapreds ((b528))
  :extrapreds ((b533))
  :extrapreds ((b540))
  :extrapreds ((b546))
  :extrapreds ((b552))
  :extrapreds ((b558))
  :extrapreds ((b564))
  :extrapreds ((b570))
  :extrapreds ((b577))
  :extrapreds ((b582))
  :extrapreds ((b587))
  :extrapreds ((b592))
  :extrapreds ((b597))
  :extrapreds ((b603))
  :extrapreds ((b609))
  :extrapreds ((b614))
  :extrapreds ((b619))
  :extrapreds ((b624))
  :extrapreds ((b629))
  :extrapreds ((b633))
  :extrapreds ((b636))
  :extrapreds ((b639))
  :extrapreds ((b642))
  :extrapreds ((b645))
  :extrapreds ((b648))
  :extrapreds ((b649))
  :extrapreds ((b650))
  :extrapreds ((b651))
  :extrapreds ((b652))
  :extrapreds ((b653))
  :extrapreds ((b656))
  :extrapreds ((b657))
  :extrapreds ((b658))
  :extrapreds ((b659))
  :extrapreds ((b660))
  :extrapreds ((b16))
  :extrapreds ((b17))
  :extrapreds ((b18))
  :extrapreds ((b22))
  :extrapreds ((b23))
  :extrapreds ((b24))
  :extrapreds ((b28))
  :extrapreds ((b29))
  :extrapreds ((b30))
  :extrapreds ((b34))
  :extrapreds ((b35))
  :extrapreds ((b36))
  :extrapreds ((b38))
  :extrapreds ((b42))
  :extrapreds ((b43))
  :extrapreds ((b44))
  :extrapreds ((b48))
  :extrapreds ((b49))
  :extrapreds ((b53))
  :extrapreds ((b54))
  :extrapreds ((b58))
  :extrapreds ((b59))
  :extrapreds ((b60))
  :extrapreds ((b64))
  :extrapreds ((b65))
  :extrapreds ((b69))
  :extrapreds ((b70))
  :extrapreds ((b74))
  :extrapreds ((b75))
  :extrapreds ((b76))
  :extrapreds ((b80))
  :extrapreds ((b81))
  :extrapreds ((b85))
  :extrapreds ((b86))
  :extrapreds ((b87))
  :extrapreds ((b91))
  :extrapreds ((b92))
  :extrapreds ((b93))
  :extrapreds ((b97))
  :extrapreds ((b98))
  :extrapreds ((b99))
  :extrapreds ((b103))
  :extrapreds ((b107))
  :extrapreds ((b111))
  :extrapreds ((b115))
  :extrapreds ((b116))
  :extrapreds ((b120))
  :extrapreds ((b124))
  :extrapreds ((b128))
  :extrapreds ((b129))
  :extrapreds ((b133))
  :extrapreds ((b134))
  :extrapreds ((b138))
  :extrapreds ((b139))
  :extrapreds ((b143))
  :extrapreds ((b144))
  :extrapreds ((b148))
  :extrapreds ((b149))
  :extrapreds ((b153))
  :extrapreds ((b154))
  :extrapreds ((b158))
  :extrapreds ((b163))
  :extrapreds ((b164))
  :extrapreds ((b168))
  :extrapreds ((b172))
  :extrapreds ((b200))
  :extrapreds ((b308))
  :extrapreds ((b335))
  :extrapreds ((b397))
  :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))
  :assumption
(or (= r13 0)  b14 )
  :assumption
(or (not b14)  (= r13 1) )
  :assumption
(or (not b14)  b16 )
  :assumption
(or (not b14)  (not b17) )
  :assumption
(or (not b14)  b18 )
  :assumption
(or (= r14 0)  b20 )
  :assumption
(or (not b20)  (= r14 1) )
  :assumption
(or (not b20)  b22 )
  :assumption
(or (not b20)  (not b23) )
  :assumption
(or b17  (not b20) )
  :assumption
(or (not b20)  b24 )
  :assumption
(or (= r15 0)  b26 )
  :assumption
(or (not b26)  (= r15 1) )
  :assumption
(or (not b26)  b28 )
  :assumption
(or (not b26)  (not b29) )
  :assumption
(or b23  (not b26) )
  :assumption
(or (not b26)  b30 )
  :assumption
(or (= r16 0)  b32 )
  :assumption
(or (not b32)  (= r16 1) )
  :assumption
(or (not b32)  b34 )
  :assumption
(or (not b32)  (not b35) )
  :assumption
(or b29  (not b32) )
  :assumption
(or (not b32)  b36 )
  :assumption
(or (= r18 0)  b40 )
  :assumption
(or (not b40)  (= r18 1) )
  :assumption
(or b28  (not b40) )
  :assumption
(or (not b40)  (not b42) )
  :assumption
(or (not b40)  b43 )
  :assumption
(or (not b40)  b44 )
  :assumption
(or (= r19 0)  b46 )
  :assumption
(or (not b46)  (= r19 1) )
  :assumption
(or b34  (not b46) )
  :assumption
(or (not b46)  (not b48) )
  :assumption
(or b42  (not b46) )
  :assumption
(or (not b46)  b49 )
  :assumption
(or (= r20 0)  b51 )
  :assumption
(or (not b51)  (= r20 1) )
  :assumption
(or b38  (not b51) )
  :assumption
(or (not b51)  (not b53) )
  :assumption
(or b48  (not b51) )
  :assumption
(or (not b51)  b54 )
  :assumption
(or (= r21 0)  b56 )
  :assumption
(or (not b56)  (= r21 1) )
  :assumption
(or b28  (not b56) )
  :assumption
(or (not b56)  (not b58) )
  :assumption
(or (not b56)  b59 )
  :assumption
(or (not b56)  b60 )
  :assumption
(or (= r22 0)  b62 )
  :assumption
(or (not b62)  (= r22 1) )
  :assumption
(or b34  (not b62) )
  :assumption
(or (not b62)  (not b64) )
  :assumption
(or b58  (not b62) )
  :assumption
(or (not b62)  b65 )
  :assumption
(or (= r23 0)  b67 )
  :assumption
(or (not b67)  (= r23 1) )
  :assumption
(or b38  (not b67) )
  :assumption
(or (not b67)  (not b69) )
  :assumption
(or b64  (not b67) )
  :assumption
(or (not b67)  b70 )
  :assumption
(or (= r24 0)  b72 )
  :assumption
(or (not b72)  (= r24 1) )
  :assumption
(or (not b72)  b74 )
  :assumption
(or (not b72)  (not b75) )
  :assumption
(or (not b72)  b76 )
  :assumption
(or b30  (not b72) )
  :assumption
(or (= r25 0)  b78 )
  :assumption
(or (not b78)  (= r25 1) )
  :assumption
(or (not b78)  b80 )
  :assumption
(or (not b78)  (not b81) )
  :assumption
(or b75  (not b78) )
  :assumption
(or b36  (not b78) )
  :assumption
(or (= r26 0)  b83 )
  :assumption
(or (not b83)  (= r26 1) )
  :assumption
(or (not b83)  b85 )
  :assumption
(or (not b83)  (not b86) )
  :assumption
(or b81  (not b83) )
  :assumption
(or (not b83)  b87 )
  :assumption
(or (= r27 0)  b89 )
  :assumption
(or (not b89)  (= r27 1) )
  :assumption
(or (not b89)  b91 )
  :assumption
(or (not b89)  (not b92) )
  :assumption
(or (not b89)  b93 )
  :assumption
(or (= r28 0)  b95 )
  :assumption
(or (not b95)  (= r28 1) )
  :assumption
(or (not b95)  b97 )
  :assumption
(or (not b95)  (not b98) )
  :assumption
(or b92  (not b95) )
  :assumption
(or (not b95)  b99 )
  :assumption
(or (= r29 0)  b101 )
  :assumption
(or (not b101)  (= r29 1) )
  :assumption
(or b74  (not b101) )
  :assumption
(or (not b101)  (not b103) )
  :assumption
(or b98  (not b101) )
  :assumption
(or b44  (not b101) )
  :assumption
(or (= r30 0)  b105 )
  :assumption
(or (not b105)  (= r30 1) )
  :assumption
(or b80  (not b105) )
  :assumption
(or (not b105)  (not b107) )
  :assumption
(or b103  (not b105) )
  :assumption
(or b49  (not b105) )
  :assumption
(or (= r31 0)  b109 )
  :assumption
(or (not b109)  (= r31 1) )
  :assumption
(or b85  (not b109) )
  :assumption
(or (not b109)  (not b111) )
  :assumption
(or b107  (not b109) )
  :assumption
(or b54  (not b109) )
  :assumption
(or (= r32 0)  b113 )
  :assumption
(or (not b113)  (= r32 1) )
  :assumption
(or b74  (not b113) )
  :assumption
(or (not b113)  (not b115) )
  :assumption
(or (not b113)  b116 )
  :assumption
(or b60  (not b113) )
  :assumption
(or (= r33 0)  b118 )
  :assumption
(or (not b118)  (= r33 1) )
  :assumption
(or b80  (not b118) )
  :assumption
(or (not b118)  (not b120) )
  :assumption
(or b115  (not b118) )
  :assumption
(or b65  (not b118) )
  :assumption
(or (= r34 0)  b122 )
  :assumption
(or (not b122)  (= r34 1) )
  :assumption
(or b85  (not b122) )
  :assumption
(or (not b122)  (not b124) )
  :assumption
(or b120  (not b122) )
  :assumption
(or b70  (not b122) )
  :assumption
(or (= r35 0)  b126 )
  :assumption
(or (not b126)  (= r35 1) )
  :assumption
(or (not b126)  b128 )
  :assumption
(or (not b126)  (not b129) )
  :assumption
(or b18  (not b126) )
  :assumption
(or (= r36 0)  b131 )
  :assumption
(or (not b131)  (= r36 1) )
  :assumption
(or (not b131)  b133 )
  :assumption
(or (not b131)  (not b134) )
  :assumption
(or b129  (not b131) )
  :assumption
(or b24  (not b131) )
  :assumption
(or (= r37 0)  b136 )
  :assumption
(or (not b136)  (= r37 1) )
  :assumption
(or (not b136)  b138 )
  :assumption
(or (not b136)  (not b139) )
  :assumption
(or b134  (not b136) )
  :assumption
(or b30  (not b136) )
  :assumption
(or (= r38 0)  b141 )
  :assumption
(or (not b141)  (= r38 1) )
  :assumption
(or (not b141)  b143 )
  :assumption
(or (not b141)  (not b144) )
  :assumption
(or b139  (not b141) )
  :assumption
(or b36  (not b141) )
  :assumption
(or (= r39 0)  b146 )
  :assumption
(or (not b146)  (= r39 1) )
  :assumption
(or (not b146)  b148 )
  :assumption
(or (not b146)  (not b149) )
  :assumption
(or b144  (not b146) )
  :assumption
(or b87  (not b146) )
  :assumption
(or (= r40 0)  b151 )
  :assumption
(or (not b151)  (= r40 1) )
  :assumption
(or b138  (not b151) )
  :assumption
(or (not b151)  (not b153) )
  :assumption
(or (not b151)  b154 )
  :assumption
(or b44  (not b151) )
  :assumption
(or (= r41 0)  b156 )
  :assumption
(or (not b156)  (= r41 1) )
  :assumption
(or b143  (not b156) )
  :assumption
(or (not b156)  (not b158) )
  :assumption
(or b153  (not b156) )
  :assumption
(or b49  (not b156) )
  :assumption
(or (= r43 0)  b161 )
  :assumption
(or (not b161)  (= r43 1) )
  :assumption
(or b138  (not b161) )
  :assumption
(or (not b161)  (not b163) )
  :assumption
(or (not b161)  b164 )
  :assumption
(or b60  (not b161) )
  :assumption
(or (= r44 0)  b166 )
  :assumption
(or (not b166)  (= r44 1) )
  :assumption
(or b143  (not b166) )
  :assumption
(or (not b166)  (not b168) )
  :assumption
(or b163  (not b166) )
  :assumption
(or b65  (not b166) )
  :assumption
(or (= r45 0)  b170 )
  :assumption
(or (not b170)  (= r45 1) )
  :assumption
(or b148  (not b170) )
  :assumption
(or (not b170)  (not b172) )
  :assumption
(or b168  (not b170) )
  :assumption
(or b70  (not b170) )
  :assumption
(or (= r46 0)  b174 )
  :assumption
(or (not b174)  (= r46 (~ 1)) )
  :assumption
(or b23  (not b174) )
  :assumption
(or (not b22)  (not b174) )
  :assumption
(or b16  (not b174) )
  :assumption
(or b24  (not b174) )
  :assumption
(or (= r47 0)  b177 )
  :assumption
(or (not b177)  (= r47 (~ 1)) )
  :assumption
(or b29  (not b177) )
  :assumption
(or (not b28)  (not b177) )
  :assumption
(or b22  (not b177) )
  :assumption
(or b30  (not b177) )
  :assumption
(or (= r48 0)  b180 )
  :assumption
(or (not b180)  (= r48 (~ 1)) )
  :assumption
(or b35  (not b180) )
  :assumption
(or (not b34)  (not b180) )
  :assumption
(or b28  (not b180) )
  :assumption
(or b36  (not b180) )
  :assumption
(or (= r49 0)  b183 )
  :assumption
(or (not b183)  (= r49 (~ 1)) )
  :assumption
(or (not b38)  (not b183) )
  :assumption
(or b34  (not b183) )
  :assumption
(or b87  (not b183) )
  :assumption
(or (= r50 0)  b186 )
  :assumption
(or (not b186)  (= r50 (~ 1)) )
  :assumption
(or b43  (not b186) )
  :assumption
(or (not b22)  (not b186) )
  :assumption
(or b16  (not b186) )
  :assumption
(or b99  (not b186) )
  :assumption
(or (= r51 0)  b189 )
  :assumption
(or (not b189)  (= r51 (~ 1)) )
  :assumption
(or b42  (not b189) )
  :assumption
(or (not b28)  (not b189) )
  :assumption
(or b22  (not b189) )
  :assumption
(or b44  (not b189) )
  :assumption
(or (= r52 0)  b192 )
  :assumption
(or (not b192)  (= r52 (~ 1)) )
  :assumption
(or b48  (not b192) )
  :assumption
(or (not b34)  (not b192) )
  :assumption
(or b28  (not b192) )
  :assumption
(or b49  (not b192) )
  :assumption
(or (= r53 0)  b195 )
  :assumption
(or (not b195)  (= r53 (~ 1)) )
  :assumption
(or b53  (not b195) )
  :assumption
(or (not b38)  (not b195) )
  :assumption
(or b34  (not b195) )
  :assumption
(or b54  (not b195) )
  :assumption
(or (= r54 0)  b198 )
  :assumption
(or (not b198)  (= r54 (~ 1)) )
  :assumption
(or b59  (not b198) )
  :assumption
(or (not b22)  (not b198) )
  :assumption
(or b16  (not b198) )
  :assumption
(or (not b198)  b200 )
  :assumption
(or (= r55 0)  b202 )
  :assumption
(or (not b202)  (= r55 (~ 1)) )
  :assumption
(or b58  (not b202) )
  :assumption
(or (not b28)  (not b202) )
  :assumption
(or b22  (not b202) )
  :assumption
(or b60  (not b202) )
  :assumption
(or (= r56 0)  b205 )
  :assumption
(or (not b205)  (= r56 (~ 1)) )
  :assumption
(or b64  (not b205) )
  :assumption
(or (not b34)  (not b205) )
  :assumption
(or b28  (not b205) )
  :assumption
(or b65  (not b205) )
  :assumption
(or (= r57 0)  b208 )
  :assumption
(or (not b208)  (= r57 (~ 1)) )
  :assumption
(or b69  (not b208) )
  :assumption
(or (not b38)  (not b208) )
  :assumption
(or b34  (not b208) )
  :assumption
(or b70  (not b208) )
  :assumption
(or (= r58 0)  b211 )
  :assumption
(or (not b211)  (= r58 (~ 1)) )
  :assumption
(or b76  (not b211) )
  :assumption
(or (not b97)  (not b211) )
  :assumption
(or b91  (not b211) )
  :assumption
(or b24  (not b211) )
  :assumption
(or (= r59 0)  b214 )
  :assumption
(or (not b214)  (= r59 (~ 1)) )
  :assumption
(or b75  (not b214) )
  :assumption
(or (not b74)  (not b214) )
  :assumption
(or b97  (not b214) )
  :assumption
(or b30  (not b214) )
  :assumption
(or (= r60 0)  b217 )
  :assumption
(or (not b217)  (= r60 (~ 1)) )
  :assumption
(or b81  (not b217) )
  :assumption
(or (not b80)  (not b217) )
  :assumption
(or b74  (not b217) )
  :assumption
(or b36  (not b217) )
  :assumption
(or (= r61 0)  b220 )
  :assumption
(or (not b220)  (= r61 (~ 1)) )
  :assumption
(or b86  (not b220) )
  :assumption
(or (not b85)  (not b220) )
  :assumption
(or b80  (not b220) )
  :assumption
(or b87  (not b220) )
  :assumption
(or (= r62 0)  b223 )
  :assumption
(or (not b223)  (= r62 (~ 1)) )
  :assumption
(or b98  (not b223) )
  :assumption
(or (not b97)  (not b223) )
  :assumption
(or b91  (not b223) )
  :assumption
(or b99  (not b223) )
  :assumption
(or (= r63 0)  b226 )
  :assumption
(or (not b226)  (= r63 (~ 1)) )
  :assumption
(or b103  (not b226) )
  :assumption
(or (not b74)  (not b226) )
  :assumption
(or b97  (not b226) )
  :assumption
(or b44  (not b226) )
  :assumption
(or (= r64 0)  b229 )
  :assumption
(or (not b229)  (= r64 (~ 1)) )
  :assumption
(or b107  (not b229) )
  :assumption
(or (not b80)  (not b229) )
  :assumption
(or b74  (not b229) )
  :assumption
(or b49  (not b229) )
  :assumption
(or (= r65 0)  b232 )
  :assumption
(or (not b232)  (= r65 (~ 1)) )
  :assumption
(or b111  (not b232) )
  :assumption
(or (not b85)  (not b232) )
  :assumption
(or b80  (not b232) )
  :assumption
(or b54  (not b232) )
  :assumption
(or (= r66 0)  b235 )
  :assumption
(or (not b235)  (= r66 (~ 1)) )
  :assumption
(or b116  (not b235) )
  :assumption
(or (not b97)  (not b235) )
  :assumption
(or b91  (not b235) )
  :assumption
(or b200  (not b235) )
  :assumption
(or (= r67 0)  b238 )
  :assumption
(or (not b238)  (= r67 (~ 1)) )
  :assumption
(or b115  (not b238) )
  :assumption
(or (not b74)  (not b238) )
  :assumption
(or b97  (not b238) )
  :assumption
(or b60  (not b238) )
  :assumption
(or (= r68 0)  b241 )
  :assumption
(or (not b241)  (= r68 (~ 1)) )
  :assumption
(or b120  (not b241) )
  :assumption
(or (not b80)  (not b241) )
  :assumption
(or b74  (not b241) )
  :assumption
(or b65  (not b241) )
  :assumption
(or (= r69 0)  b244 )
  :assumption
(or (not b244)  (= r69 (~ 1)) )
  :assumption
(or b124  (not b244) )
  :assumption
(or (not b85)  (not b244) )
  :assumption
(or b80  (not b244) )
  :assumption
(or b70  (not b244) )
  :assumption
(or (= r70 0)  b247 )
  :assumption
(or (not b247)  (= r70 (~ 1)) )
  :assumption
(or b134  (not b247) )
  :assumption
(or (not b133)  (not b247) )
  :assumption
(or b128  (not b247) )
  :assumption
(or b24  (not b247) )
  :assumption
(or (= r71 0)  b250 )
  :assumption
(or (not b250)  (= r71 (~ 1)) )
  :assumption
(or b139  (not b250) )
  :assumption
(or (not b138)  (not b250) )
  :assumption
(or b133  (not b250) )
  :assumption
(or b30  (not b250) )
  :assumption
(or (= r72 0)  b253 )
  :assumption
(or (not b253)  (= r72 (~ 1)) )
  :assumption
(or b144  (not b253) )
  :assumption
(or (not b143)  (not b253) )
  :assumption
(or b138  (not b253) )
  :assumption
(or b36  (not b253) )
  :assumption
(or (= r73 0)  b256 )
  :assumption
(or (not b256)  (= r73 (~ 1)) )
  :assumption
(or b149  (not b256) )
  :assumption
(or (not b148)  (not b256) )
  :assumption
(or b143  (not b256) )
  :assumption
(or b87  (not b256) )
  :assumption
(or (= r74 0)  b259 )
  :assumption
(or (not b259)  (= r74 (~ 1)) )
  :assumption
(or b154  (not b259) )
  :assumption
(or (not b133)  (not b259) )
  :assumption
(or b128  (not b259) )
  :assumption
(or b99  (not b259) )
  :assumption
(or (= r75 0)  b262 )
  :assumption
(or (not b262)  (= r75 (~ 1)) )
  :assumption
(or b153  (not b262) )
  :assumption
(or (not b138)  (not b262) )
  :assumption
(or b133  (not b262) )
  :assumption
(or b44  (not b262) )
  :assumption
(or (= r76 0)  b265 )
  :assumption
(or (not b265)  (= r76 (~ 1)) )
  :assumption
(or b158  (not b265) )
  :assumption
(or (not b143)  (not b265) )
  :assumption
(or b138  (not b265) )
  :assumption
(or b49  (not b265) )
  :assumption
(or (= r77 0)  b268 )
  :assumption
(or (not b268)  (= r77 (~ 1)) )
  :assumption
(or (not b148)  (not b268) )
  :assumption
(or b143  (not b268) )
  :assumption
(or b54  (not b268) )
  :assumption
(or (= r78 0)  b271 )
  :assumption
(or (not b271)  (= r78 (~ 1)) )
  :assumption
(or b164  (not b271) )
  :assumption
(or (not b133)  (not b271) )
  :assumption
(or b128  (not b271) )
  :assumption
(or b200  (not b271) )
  :assumption
(or (= r79 0)  b274 )
  :assumption
(or (not b274)  (= r79 (~ 1)) )
  :assumption
(or b163  (not b274) )
  :assumption
(or (not b138)  (not b274) )
  :assumption
(or b133  (not b274) )
  :assumption
(or b60  (not b274) )
  :assumption
(or (= r80 0)  b277 )
  :assumption
(or (not b277)  (= r80 (~ 1)) )
  :assumption
(or b168  (not b277) )
  :assumption
(or (not b143)  (not b277) )
  :assumption
(or b138  (not b277) )
  :assumption
(or b65  (not b277) )
  :assumption
(or (= r81 0)  b280 )
  :assumption
(or (not b280)  (= r81 (~ 1)) )
  :assumption
(or b172  (not b280) )
  :assumption
(or (not b148)  (not b280) )
  :assumption
(or b143  (not b280) )
  :assumption
(or b70  (not b280) )
  :assumption
(or (= r82 0)  b283 )
  :assumption
(or b283  (= r83 0) )
  :assumption
(or (not b283)  (= r83 (* (~ 631) 3)) )
  :assumption
(or (not b283)  (= r82 (* 631 3)) )
  :assumption
(or b99  (not b283) )
  :assumption
(or (not b24)  (not b283) )
  :assumption
(or b18  (not b283) )
  :assumption
(or (not b283)  (>= r84 (* 631 3)) )
  :assumption
(or (= r85 0)  b289 )
  :assumption
(or b289  (= r86 0) )
  :assumption
(or (not b289)  (= r86 (* (~ 631) 3)) )
  :assumption
(or (not b289)  (= r85 (* 631 3)) )
  :assumption
(or b44  (not b289) )
  :assumption
(or (not b30)  (not b289) )
  :assumption
(or b24  (not b289) )
  :assumption
(or (not b289)  (>= r87 (* 631 3)) )
  :assumption
(or (= r88 0)  b295 )
  :assumption
(or b295  (= r89 0) )
  :assumption
(or (not b295)  (= r89 (* (~ 631) 3)) )
  :assumption
(or (not b295)  (= r88 (* 631 3)) )
  :assumption
(or b49  (not b295) )
  :assumption
(or (not b36)  (not b295) )
  :assumption
(or b30  (not b295) )
  :assumption
(or (not b295)  (>= r90 (* 631 3)) )
  :assumption
(or (= r91 0)  b301 )
  :assumption
(or b301  (= r92 0) )
  :assumption
(or (not b301)  (= r92 (* (~ 631) 3)) )
  :assumption
(or (not b301)  (= r91 (* 631 3)) )
  :assumption
(or b54  (not b301) )
  :assumption
(or (not b87)  (not b301) )
  :assumption
(or b36  (not b301) )
  :assumption
(or (not b301)  (>= r93 (* 631 3)) )
  :assumption
(or (= r96 0)  b310 )
  :assumption
(or b310  (= r97 0) )
  :assumption
(or (not b310)  (= r97 (* (~ 998) 3)) )
  :assumption
(or (not b310)  (= r96 (* 998 3)) )
  :assumption
(or b200  (not b310) )
  :assumption
(or (not b24)  (not b310) )
  :assumption
(or b18  (not b310) )
  :assumption
(or (not b310)  (>= r84 (* 998 3)) )
  :assumption
(or (= r98 0)  b316 )
  :assumption
(or b316  (= r99 0) )
  :assumption
(or (not b316)  (= r99 (* (~ 998) 3)) )
  :assumption
(or (not b316)  (= r98 (* 998 3)) )
  :assumption
(or b60  (not b316) )
  :assumption
(or (not b30)  (not b316) )
  :assumption
(or b24  (not b316) )
  :assumption
(or (not b316)  (>= r87 (* 998 3)) )
  :assumption
(or (= r100 0)  b322 )
  :assumption
(or b322  (= r101 0) )
  :assumption
(or (not b322)  (= r101 (* (~ 998) 3)) )
  :assumption
(or (not b322)  (= r100 (* 998 3)) )
  :assumption
(or b65  (not b322) )
  :assumption
(or (not b36)  (not b322) )
  :assumption
(or b30  (not b322) )
  :assumption
(or (not b322)  (>= r90 (* 998 3)) )
  :assumption
(or (= r102 0)  b328 )
  :assumption
(or b328  (= r103 0) )
  :assumption
(or (not b328)  (= r103 (* (~ 998) 3)) )
  :assumption
(or (not b328)  (= r102 (* 998 3)) )
  :assumption
(or b70  (not b328) )
  :assumption
(or (not b87)  (not b328) )
  :assumption
(or b36  (not b328) )
  :assumption
(or (not b328)  (>= r93 (* 998 3)) )
  :assumption
(or (= r106 0)  b337 )
  :assumption
(or b337  (= r107 0) )
  :assumption
(or (not b337)  (= r107 (* (~ 631) 3)) )
  :assumption
(or (not b337)  (= r106 (* 631 3)) )
  :assumption
(or b24  (not b337) )
  :assumption
(or (not b99)  (not b337) )
  :assumption
(or b93  (not b337) )
  :assumption
(or (>= r84 (* 631 3))  (not b337) )
  :assumption
(or (= r108 0)  b342 )
  :assumption
(or b342  (= r109 0) )
  :assumption
(or (not b342)  (= r109 (* (~ 631) 3)) )
  :assumption
(or (not b342)  (= r108 (* 631 3)) )
  :assumption
(or b30  (not b342) )
  :assumption
(or (not b44)  (not b342) )
  :assumption
(or b99  (not b342) )
  :assumption
(or (>= r87 (* 631 3))  (not b342) )
  :assumption
(or (= r110 0)  b347 )
  :assumption
(or b347  (= r111 0) )
  :assumption
(or (not b347)  (= r111 (* (~ 631) 3)) )
  :assumption
(or (not b347)  (= r110 (* 631 3)) )
  :assumption
(or b36  (not b347) )
  :assumption
(or (not b49)  (not b347) )
  :assumption
(or b44  (not b347) )
  :assumption
(or (>= r90 (* 631 3))  (not b347) )
  :assumption
(or (= r112 0)  b352 )
  :assumption
(or b352  (= r113 0) )
  :assumption
(or (not b352)  (= r113 (* (~ 631) 3)) )
  :assumption
(or (not b352)  (= r112 (* 631 3)) )
  :assumption
(or b87  (not b352) )
  :assumption
(or (not b54)  (not b352) )
  :assumption
(or b49  (not b352) )
  :assumption
(or (>= r93 (* 631 3))  (not b352) )
  :assumption
(or (= r114 0)  b357 )
  :assumption
(or b357  (= r115 0) )
  :assumption
(or (not b357)  (= r115 (* (~ 631) 3)) )
  :assumption
(or (not b357)  (= r114 (* 631 3)) )
  :assumption
(or (not b308)  (not b357) )
  :assumption
(or b54  (not b357) )
  :assumption
(or (not b357)  (>= r116 (* 631 3)) )
  :assumption
(or (= r117 0)  b363 )
  :assumption
(or b363  (= r118 0) )
  :assumption
(or (not b363)  (= r118 (* (~ 627) 3)) )
  :assumption
(or (not b363)  (= r117 (* 627 3)) )
  :assumption
(or b200  (not b363) )
  :assumption
(or (not b99)  (not b363) )
  :assumption
(or b93  (not b363) )
  :assumption
(or (not b363)  (>= r84 (* 627 3)) )
  :assumption
(or (= r119 0)  b369 )
  :assumption
(or b369  (= r120 0) )
  :assumption
(or (not b369)  (= r120 (* (~ 627) 3)) )
  :assumption
(or (not b369)  (= r119 (* 627 3)) )
  :assumption
(or b60  (not b369) )
  :assumption
(or (not b44)  (not b369) )
  :assumption
(or b99  (not b369) )
  :assumption
(or (not b369)  (>= r87 (* 627 3)) )
  :assumption
(or (= r121 0)  b375 )
  :assumption
(or b375  (= r122 0) )
  :assumption
(or (not b375)  (= r122 (* (~ 627) 3)) )
  :assumption
(or (not b375)  (= r121 (* 627 3)) )
  :assumption
(or b65  (not b375) )
  :assumption
(or (not b49)  (not b375) )
  :assumption
(or b44  (not b375) )
  :assumption
(or (not b375)  (>= r90 (* 627 3)) )
  :assumption
(or (= r123 0)  b381 )
  :assumption
(or b381  (= r124 0) )
  :assumption
(or (not b381)  (= r124 (* (~ 627) 3)) )
  :assumption
(or (not b381)  (= r123 (* 627 3)) )
  :assumption
(or b70  (not b381) )
  :assumption
(or (not b54)  (not b381) )
  :assumption
(or b49  (not b381) )
  :assumption
(or (not b381)  (>= r93 (* 627 3)) )
  :assumption
(or (= r125 0)  b387 )
  :assumption
(or b387  (= r126 0) )
  :assumption
(or (not b387)  (= r126 (* (~ 627) 3)) )
  :assumption
(or (not b387)  (= r125 (* 627 3)) )
  :assumption
(or b335  (not b387) )
  :assumption
(or (not b308)  (not b387) )
  :assumption
(or b54  (not b387) )
  :assumption
(or (not b387)  (>= r116 (* 627 3)) )
  :assumption
(or (= r127 0)  b393 )
  :assumption
(or b393  (= r128 0) )
  :assumption
(or (not b393)  (= r128 (* (~ 998) 3)) )
  :assumption
(or (not b393)  (= r127 (* 998 3)) )
  :assumption
(or b18  (not b393) )
  :assumption
(or (not b393)  (not b397) )
  :assumption
(or (not b393)  (>= r11 (* 998 3)) )
  :assumption
(or (= r129 0)  b400 )
  :assumption
(or b400  (= r130 0) )
  :assumption
(or (not b400)  (= r130 (* (~ 998) 3)) )
  :assumption
(or (not b400)  (= r129 (* 998 3)) )
  :assumption
(or b24  (not b400) )
  :assumption
(or (not b200)  (not b400) )
  :assumption
(or b397  (not b400) )
  :assumption
(or (>= r84 (* 998 3))  (not b400) )
  :assumption
(or (= r131 0)  b405 )
  :assumption
(or b405  (= r132 0) )
  :assumption
(or (not b405)  (= r132 (* (~ 998) 3)) )
  :assumption
(or (not b405)  (= r131 (* 998 3)) )
  :assumption
(or b30  (not b405) )
  :assumption
(or (not b60)  (not b405) )
  :assumption
(or b200  (not b405) )
  :assumption
(or (>= r87 (* 998 3))  (not b405) )
  :assumption
(or (= r133 0)  b410 )
  :assumption
(or b410  (= r134 0) )
  :assumption
(or (not b410)  (= r134 (* (~ 998) 3)) )
  :assumption
(or (not b410)  (= r133 (* 998 3)) )
  :assumption
(or b36  (not b410) )
  :assumption
(or (not b65)  (not b410) )
  :assumption
(or b60  (not b410) )
  :assumption
(or (>= r90 (* 998 3))  (not b410) )
  :assumption
(or (= r135 0)  b415 )
  :assumption
(or b415  (= r136 0) )
  :assumption
(or (not b415)  (= r136 (* (~ 998) 3)) )
  :assumption
(or (not b415)  (= r135 (* 998 3)) )
  :assumption
(or b87  (not b415) )
  :assumption
(or (not b70)  (not b415) )
  :assumption
(or b65  (not b415) )
  :assumption
(or (>= r93 (* 998 3))  (not b415) )
  :assumption
(or (= r137 0)  b420 )
  :assumption
(or b420  (= r138 0) )
  :assumption
(or (not b420)  (= r138 (* (~ 998) 3)) )
  :assumption
(or (not b420)  (= r137 (* 998 3)) )
  :assumption
(or (not b335)  (not b420) )
  :assumption
(or b70  (not b420) )
  :assumption
(or (not b420)  (>= r116 (* 998 3)) )
  :assumption
(or (= r139 0)  b426 )
  :assumption
(or b426  (= r140 0) )
  :assumption
(or (not b426)  (= r140 (* (~ 627) 3)) )
  :assumption
(or (not b426)  (= r139 (* 627 3)) )
  :assumption
(or b93  (not b426) )
  :assumption
(or (not b397)  (not b426) )
  :assumption
(or (not b426)  (>= r11 (* 627 3)) )
  :assumption
(or (= r141 0)  b432 )
  :assumption
(or b432  (= r142 0) )
  :assumption
(or (not b432)  (= r142 (* (~ 627) 3)) )
  :assumption
(or (not b432)  (= r141 (* 627 3)) )
  :assumption
(or b99  (not b432) )
  :assumption
(or (not b200)  (not b432) )
  :assumption
(or b397  (not b432) )
  :assumption
(or (>= r84 (* 627 3))  (not b432) )
  :assumption
(or (= r143 0)  b437 )
  :assumption
(or b437  (= r144 0) )
  :assumption
(or (not b437)  (= r144 (* (~ 627) 3)) )
  :assumption
(or (not b437)  (= r143 (* 627 3)) )
  :assumption
(or b44  (not b437) )
  :assumption
(or (not b60)  (not b437) )
  :assumption
(or b200  (not b437) )
  :assumption
(or (>= r87 (* 627 3))  (not b437) )
  :assumption
(or (= r145 0)  b442 )
  :assumption
(or b442  (= r146 0) )
  :assumption
(or (not b442)  (= r146 (* (~ 627) 3)) )
  :assumption
(or (not b442)  (= r145 (* 627 3)) )
  :assumption
(or b49  (not b442) )
  :assumption
(or (not b65)  (not b442) )
  :assumption
(or b60  (not b442) )
  :assumption
(or (>= r90 (* 627 3))  (not b442) )
  :assumption
(or (= r147 0)  b447 )
  :assumption
(or b447  (= r148 0) )
  :assumption
(or (not b447)  (= r148 (* (~ 627) 3)) )
  :assumption
(or (not b447)  (= r147 (* 627 3)) )
  :assumption
(or b54  (not b447) )
  :assumption
(or (not b70)  (not b447) )
  :assumption
(or b65  (not b447) )
  :assumption
(or (>= r93 (* 627 3))  (not b447) )
  :assumption
(or (= r149 0)  b452 )
  :assumption
(or b452  (= r150 0) )
  :assumption
(or (not b452)  (= r150 (* (~ 627) 3)) )
  :assumption
(or (not b452)  (= r149 (* 627 3)) )
  :assumption
(or b308  (not b452) )
  :assumption
(or (not b335)  (not b452) )
  :assumption
(or b70  (not b452) )
  :assumption
(or (>= r116 (* 627 3))  (not b452) )
  :assumption
(or (= r151 0)  b457 )
  :assumption
(or b457  (= r152 0) )
  :assumption
(or (not b457)  (= r152 (* (~ 631) 11)) )
  :assumption
(or (not b457)  (= r151 (* 631 11)) )
  :assumption
(or b99  (not b457) )
  :assumption
(or (not b24)  (not b457) )
  :assumption
(or b18  (not b457) )
  :assumption
(or (not b457)  (>= r84 (* 631 11)) )
  :assumption
(or (not b457)  (<= r153 9) )
  :assumption
(or (= r154 0)  b464 )
  :assumption
(or b464  (= r155 0) )
  :assumption
(or (not b464)  (= r155 (* (~ 631) 11)) )
  :assumption
(or (not b464)  (= r154 (* 631 11)) )
  :assumption
(or b44  (not b464) )
  :assumption
(or (not b30)  (not b464) )
  :assumption
(or b24  (not b464) )
  :assumption
(or (not b464)  (>= r87 (* 631 11)) )
  :assumption
(or (not b464)  (<= r156 9) )
  :assumption
(or (= r157 0)  b471 )
  :assumption
(or b471  (= r158 0) )
  :assumption
(or (not b471)  (= r158 (* (~ 631) 11)) )
  :assumption
(or (not b471)  (= r157 (* 631 11)) )
  :assumption
(or b49  (not b471) )
  :assumption
(or (not b36)  (not b471) )
  :assumption
(or b30  (not b471) )
  :assumption
(or (not b471)  (>= r90 (* 631 11)) )
  :assumption
(or (not b471)  (<= r159 9) )
  :assumption
(or (= r160 0)  b478 )
  :assumption
(or b478  (= r161 0) )
  :assumption
(or (not b478)  (= r161 (* (~ 631) 11)) )
  :assumption
(or (not b478)  (= r160 (* 631 11)) )
  :assumption
(or b54  (not b478) )
  :assumption
(or (not b87)  (not b478) )
  :assumption
(or b36  (not b478) )
  :assumption
(or (not b478)  (>= r93 (* 631 11)) )
  :assumption
(or (not b478)  (<= r162 9) )
  :assumption
(or (= r165 0)  b487 )
  :assumption
(or b487  (= r166 0) )
  :assumption
(or (not b487)  (= r166 (* (~ 998) 11)) )
  :assumption
(or (not b487)  (= r165 (* 998 11)) )
  :assumption
(or b200  (not b487) )
  :assumption
(or (not b24)  (not b487) )
  :assumption
(or b18  (not b487) )
  :assumption
(or (not b487)  (>= r84 (* 998 11)) )
  :assumption
(or (<= r153 9)  (not b487) )
  :assumption
(or (= r167 0)  b493 )
  :assumption
(or b493  (= r168 0) )
  :assumption
(or (not b493)  (= r168 (* (~ 998) 11)) )
  :assumption
(or (not b493)  (= r167 (* 998 11)) )
  :assumption
(or b60  (not b493) )
  :assumption
(or (not b30)  (not b493) )
  :assumption
(or b24  (not b493) )
  :assumption
(or (not b493)  (>= r87 (* 998 11)) )
  :assumption
(or (<= r156 9)  (not b493) )
  :assumption
(or (= r169 0)  b499 )
  :assumption
(or b499  (= r170 0) )
  :assumption
(or (not b499)  (= r170 (* (~ 998) 11)) )
  :assumption
(or (not b499)  (= r169 (* 998 11)) )
  :assumption
(or b65  (not b499) )
  :assumption
(or (not b36)  (not b499) )
  :assumption
(or b30  (not b499) )
  :assumption
(or (not b499)  (>= r90 (* 998 11)) )
  :assumption
(or (<= r159 9)  (not b499) )
  :assumption
(or (= r171 0)  b505 )
  :assumption
(or b505  (= r172 0) )
  :assumption
(or (not b505)  (= r172 (* (~ 998) 11)) )
  :assumption
(or (not b505)  (= r171 (* 998 11)) )
  :assumption
(or b70  (not b505) )
  :assumption
(or (not b87)  (not b505) )
  :assumption
(or b36  (not b505) )
  :assumption
(or (not b505)  (>= r93 (* 998 11)) )
  :assumption
(or (<= r162 9)  (not b505) )
  :assumption
(or (= r175 0)  b513 )
  :assumption
(or b513  (= r176 0) )
  :assumption
(or (not b513)  (= r176 (* (~ 631) 11)) )
  :assumption
(or (not b513)  (= r175 (* 631 11)) )
  :assumption
(or b24  (not b513) )
  :assumption
(or (not b99)  (not b513) )
  :assumption
(or b93  (not b513) )
  :assumption
(or (>= r84 (* 631 11))  (not b513) )
  :assumption
(or (<= r153 9)  (not b513) )
  :assumption
(or (= r177 0)  b518 )
  :assumption
(or b518  (= r178 0) )
  :assumption
(or (not b518)  (= r178 (* (~ 631) 11)) )
  :assumption
(or (not b518)  (= r177 (* 631 11)) )
  :assumption
(or b30  (not b518) )
  :assumption
(or (not b44)  (not b518) )
  :assumption
(or b99  (not b518) )
  :assumption
(or (>= r87 (* 631 11))  (not b518) )
  :assumption
(or (<= r156 9)  (not b518) )
  :assumption
(or (= r179 0)  b523 )
  :assumption
(or b523  (= r180 0) )
  :assumption
(or (not b523)  (= r180 (* (~ 631) 11)) )
  :assumption
(or (not b523)  (= r179 (* 631 11)) )
  :assumption
(or b36  (not b523) )
  :assumption
(or (not b49)  (not b523) )
  :assumption
(or b44  (not b523) )
  :assumption
(or (>= r90 (* 631 11))  (not b523) )
  :assumption
(or (<= r159 9)  (not b523) )
  :assumption
(or (= r181 0)  b528 )
  :assumption
(or b528  (= r182 0) )
  :assumption
(or (not b528)  (= r182 (* (~ 631) 11)) )
  :assumption
(or (not b528)  (= r181 (* 631 11)) )
  :assumption
(or b87  (not b528) )
  :assumption
(or (not b54)  (not b528) )
  :assumption
(or b49  (not b528) )
  :assumption
(or (>= r93 (* 631 11))  (not b528) )
  :assumption
(or (<= r162 9)  (not b528) )
  :assumption
(or (= r183 0)  b533 )
  :assumption
(or b533  (= r184 0) )
  :assumption
(or (not b533)  (= r184 (* (~ 631) 11)) )
  :assumption
(or (not b533)  (= r183 (* 631 11)) )
  :assumption
(or (not b308)  (not b533) )
  :assumption
(or b54  (not b533) )
  :assumption
(or (not b533)  (>= r116 (* 631 11)) )
  :assumption
(or (not b533)  (<= r185 9) )
  :assumption
(or (= r186 0)  b540 )
  :assumption
(or b540  (= r187 0) )
  :assumption
(or (not b540)  (= r187 (* (~ 627) 11)) )
  :assumption
(or (not b540)  (= r186 (* 627 11)) )
  :assumption
(or b200  (not b540) )
  :assumption
(or (not b99)  (not b540) )
  :assumption
(or b93  (not b540) )
  :assumption
(or (not b540)  (>= r84 (* 627 11)) )
  :assumption
(or (<= r153 9)  (not b540) )
  :assumption
(or (= r188 0)  b546 )
  :assumption
(or b546  (= r189 0) )
  :assumption
(or (not b546)  (= r189 (* (~ 627) 11)) )
  :assumption
(or (not b546)  (= r188 (* 627 11)) )
  :assumption
(or b60  (not b546) )
  :assumption
(or (not b44)  (not b546) )
  :assumption
(or b99  (not b546) )
  :assumption
(or (not b546)  (>= r87 (* 627 11)) )
  :assumption
(or (<= r156 9)  (not b546) )
  :assumption
(or (= r190 0)  b552 )
  :assumption
(or b552  (= r191 0) )
  :assumption
(or (not b552)  (= r191 (* (~ 627) 11)) )
  :assumption
(or (not b552)  (= r190 (* 627 11)) )
  :assumption
(or b65  (not b552) )
  :assumption
(or (not b49)  (not b552) )
  :assumption
(or b44  (not b552) )
  :assumption
(or (not b552)  (>= r90 (* 627 11)) )
  :assumption
(or (<= r159 9)  (not b552) )
  :assumption
(or (= r192 0)  b558 )
  :assumption
(or b558  (= r193 0) )
  :assumption
(or (not b558)  (= r193 (* (~ 627) 11)) )
  :assumption
(or (not b558)  (= r192 (* 627 11)) )
  :assumption
(or b70  (not b558) )
  :assumption
(or (not b54)  (not b558) )
  :assumption
(or b49  (not b558) )
  :assumption
(or (not b558)  (>= r93 (* 627 11)) )
  :assumption
(or (<= r162 9)  (not b558) )
  :assumption
(or (= r194 0)  b564 )
  :assumption
(or b564  (= r195 0) )
  :assumption
(or (not b564)  (= r195 (* (~ 627) 11)) )
  :assumption
(or (not b564)  (= r194 (* 627 11)) )
  :assumption
(or b335  (not b564) )
  :assumption
(or (not b308)  (not b564) )
  :assumption
(or b54  (not b564) )
  :assumption
(or (not b564)  (>= r116 (* 627 11)) )
  :assumption
(or (<= r185 9)  (not b564) )
  :assumption
(or (= r196 0)  b570 )
  :assumption
(or b570  (= r197 0) )
  :assumption
(or (not b570)  (= r197 (* (~ 998) 11)) )
  :assumption
(or (not b570)  (= r196 (* 998 11)) )
  :assumption
(or b18  (not b570) )
  :assumption
(or (not b397)  (not b570) )
  :assumption
(or (not b570)  (>= r11 (* 998 11)) )
  :assumption
(or (not b570)  (<= r10 9) )
  :assumption
(or (= r198 0)  b577 )
  :assumption
(or b577  (= r199 0) )
  :assumption
(or (not b577)  (= r199 (* (~ 998) 11)) )
  :assumption
(or (not b577)  (= r198 (* 998 11)) )
  :assumption
(or b24  (not b577) )
  :assumption
(or (not b200)  (not b577) )
  :assumption
(or b397  (not b577) )
  :assumption
(or (>= r84 (* 998 11))  (not b577) )
  :assumption
(or (<= r153 9)  (not b577) )
  :assumption
(or (= r200 0)  b582 )
  :assumption
(or b582  (= r201 0) )
  :assumption
(or (not b582)  (= r201 (* (~ 998) 11)) )
  :assumption
(or (not b582)  (= r200 (* 998 11)) )
  :assumption
(or b30  (not b582) )
  :assumption
(or (not b60)  (not b582) )
  :assumption
(or b200  (not b582) )
  :assumption
(or (>= r87 (* 998 11))  (not b582) )
  :assumption
(or (<= r156 9)  (not b582) )
  :assumption
(or (= r202 0)  b587 )
  :assumption
(or b587  (= r203 0) )
  :assumption
(or (not b587)  (= r203 (* (~ 998) 11)) )
  :assumption
(or (not b587)  (= r202 (* 998 11)) )
  :assumption
(or b36  (not b587) )
  :assumption
(or (not b65)  (not b587) )
  :assumption
(or b60  (not b587) )
  :assumption
(or (>= r90 (* 998 11))  (not b587) )
  :assumption
(or (<= r159 9)  (not b587) )
  :assumption
(or (= r204 0)  b592 )
  :assumption
(or b592  (= r205 0) )
  :assumption
(or (not b592)  (= r205 (* (~ 998) 11)) )
  :assumption
(or (not b592)  (= r204 (* 998 11)) )
  :assumption
(or b87  (not b592) )
  :assumption
(or (not b70)  (not b592) )
  :assumption
(or b65  (not b592) )
  :assumption
(or (>= r93 (* 998 11))  (not b592) )
  :assumption
(or (<= r162 9)  (not b592) )
  :assumption
(or (= r206 0)  b597 )
  :assumption
(or b597  (= r207 0) )
  :assumption
(or (not b597)  (= r207 (* (~ 998) 11)) )
  :assumption
(or (not b597)  (= r206 (* 998 11)) )
  :assumption
(or (not b335)  (not b597) )
  :assumption
(or b70  (not b597) )
  :assumption
(or (not b597)  (>= r116 (* 998 11)) )
  :assumption
(or (<= r185 9)  (not b597) )
  :assumption
(or (= r208 0)  b603 )
  :assumption
(or b603  (= r209 0) )
  :assumption
(or (not b603)  (= r209 (* (~ 627) 11)) )
  :assumption
(or (not b603)  (= r208 (* 627 11)) )
  :assumption
(or b93  (not b603) )
  :assumption
(or (not b397)  (not b603) )
  :assumption
(or (not b603)  (>= r11 (* 627 11)) )
  :assumption
(or (<= r10 9)  (not b603) )
  :assumption
(or (= r210 0)  b609 )
  :assumption
(or b609  (= r211 0) )
  :assumption
(or (not b609)  (= r211 (* (~ 627) 11)) )
  :assumption
(or (not b609)  (= r210 (* 627 11)) )
  :assumption
(or b99  (not b609) )
  :assumption
(or (not b200)  (not b609) )
  :assumption
(or b397  (not b609) )
  :assumption
(or (>= r84 (* 627 11))  (not b609) )
  :assumption
(or (<= r153 9)  (not b609) )
  :assumption
(or (= r212 0)  b614 )
  :assumption
(or b614  (= r213 0) )
  :assumption
(or (not b614)  (= r213 (* (~ 627) 11)) )
  :assumption
(or (not b614)  (= r212 (* 627 11)) )
  :assumption
(or b44  (not b614) )
  :assumption
(or (not b60)  (not b614) )
  :assumption
(or b200  (not b614) )
  :assumption
(or (>= r87 (* 627 11))  (not b614) )
  :assumption
(or (<= r156 9)  (not b614) )
  :assumption
(or (= r214 0)  b619 )
  :assumption
(or b619  (= r215 0) )
  :assumption
(or (not b619)  (= r215 (* (~ 627) 11)) )
  :assumption
(or (not b619)  (= r214 (* 627 11)) )
  :assumption
(or b49  (not b619) )
  :assumption
(or (not b65)  (not b619) )
  :assumption
(or b60  (not b619) )
  :assumption
(or (>= r90 (* 627 11))  (not b619) )
  :assumption
(or (<= r159 9)  (not b619) )
  :assumption
(or (= r216 0)  b624 )
  :assumption
(or b624  (= r217 0) )
  :assumption
(or (not b624)  (= r217 (* (~ 627) 11)) )
  :assumption
(or (not b624)  (= r216 (* 627 11)) )
  :assumption
(or b54  (not b624) )
  :assumption
(or (not b70)  (not b624) )
  :assumption
(or b65  (not b624) )
  :assumption
(or (>= r93 (* 627 11))  (not b624) )
  :assumption
(or (<= r162 9)  (not b624) )
  :assumption
(or (= r218 0)  b629 )
  :assumption
(or b629  (= r219 0) )
  :assumption
(or (not b629)  (= r219 (* (~ 627) 11)) )
  :assumption
(or (not b629)  (= r218 (* 627 11)) )
  :assumption
(or b308  (not b629) )
  :assumption
(or (not b335)  (not b629) )
  :assumption
(or b70  (not b629) )
  :assumption
(or (>= r116 (* 627 11))  (not b629) )
  :assumption
(or (<= r185 9)  (not b629) )
  :assumption
(or (not b633)  (= r87 6830) )
  :assumption
(or (not b633)  (< (+ r84 r220) 6830) )
  :assumption
(or b18  (not b633) )
  :assumption
(or (not b636)  (= r90 6830) )
  :assumption
(or (not b636)  (< (+ r87 r220) 6830) )
  :assumption
(or b24  (not b636) )
  :assumption
(or (not b639)  (= r93 6830) )
  :assumption
(or (not b639)  (< (+ r90 r220) 6830) )
  :assumption
(or b30  (not b639) )
  :assumption
(or (not b642)  (= r116 6830) )
  :assumption
(or (not b642)  (< (+ r93 r220) 6830) )
  :assumption
(or b36  (not b642) )
  :assumption
(or (not b645)  (= r221 6830) )
  :assumption
(or (not b645)  (< (+ r116 r220) 6830) )
  :assumption
(or b87  (not b645) )
  :assumption
(or (= r87 6830)  (not b648) )
  :assumption
(or (< (+ r84 r220) 6830)  (not b648) )
  :assumption
(or b93  (not b648) )
  :assumption
(or (= r90 6830)  (not b649) )
  :assumption
(or (< (+ r87 r220) 6830)  (not b649) )
  :assumption
(or b99  (not b649) )
  :assumption
(or (= r93 6830)  (not b650) )
  :assumption
(or (< (+ r90 r220) 6830)  (not b650) )
  :assumption
(or b44  (not b650) )
  :assumption
(or (= r116 6830)  (not b651) )
  :assumption
(or (< (+ r93 r220) 6830)  (not b651) )
  :assumption
(or b49  (not b651) )
  :assumption
(or (= r221 6830)  (not b652) )
  :assumption
(or (< (+ r116 r220) 6830)  (not b652) )
  :assumption
(or b54  (not b652) )
  :assumption
(or (not b653)  (= r84 6830) )
  :assumption
(or (not b653)  (< (+ r11 r220) 6830) )
  :assumption
(or (= r87 6830)  (not b656) )
  :assumption
(or (< (+ r84 r220) 6830)  (not b656) )
  :assumption
(or b397  (not b656) )
  :assumption
(or (= r90 6830)  (not b657) )
  :assumption
(or (< (+ r87 r220) 6830)  (not b657) )
  :assumption
(or b200  (not b657) )
  :assumption
(or (= r93 6830)  (not b658) )
  :assumption
(or (< (+ r90 r220) 6830)  (not b658) )
  :assumption
(or b60  (not b658) )
  :assumption
(or (= r116 6830)  (not b659) )
  :assumption
(or (< (+ r93 r220) 6830)  (not b659) )
  :assumption
(or b65  (not b659) )
  :assumption
(or (= r221 6830)  (not b660) )
  :assumption
(or (< (+ r116 r220) 6830)  (not b660) )
  :assumption
(or b70  (not b660) )
  :assumption
(or (or (or (or b393  b397 )  b426 )  b570 )  b603 )
  :assumption
(or (or (or (or (or (not b200)  b310 )  b363 )  b397 )  b487 )  b540 )
  :assumption
(or (or (or (or (or b200  (not b397) )  b400 )  b432 )  b577 )  b609 )
  :assumption
(or (or (or (or (or (not b60)  b200 )  b316 )  b369 )  b493 )  b546 )
  :assumption
(or (or (or (or (or b60  (not b200) )  b405 )  b437 )  b582 )  b614 )
  :assumption
(or (or (or (or (or b60  (not b65) )  b322 )  b375 )  b499 )  b552 )
  :assumption
(or (or (or (or (or (not b60)  b65 )  b410 )  b442 )  b587 )  b619 )
  :assumption
(or (or (or (or (or b65  (not b70) )  b328 )  b381 )  b505 )  b558 )
  :assumption
(or (or (or (or (or (not b65)  b70 )  b415 )  b447 )  b592 )  b624 )
  :assumption
(or (or (or b70  (not b335) )  b387 )  b564 )
  :assumption
(or (or (or (or (or (not b70)  b335 )  b420 )  b452 )  b597 )  b629 )
  :assumption
(or (or (not b93)  b426 )  b603 )
  :assumption
(or (or (or (or (or b93  (not b99) )  b283 )  b432 )  b457 )  b609 )
  :assumption
(or (or (or (or (or (not b93)  b99 )  b337 )  b363 )  b513 )  b540 )
  :assumption
(or (or (or (or (or (not b44)  b99 )  b289 )  b437 )  b464 )  b614 )
  :assumption
(or (or (or (or (or b44  (not b99) )  b342 )  b369 )  b518 )  b546 )
  :assumption
(or (or (or (or (or b44  (not b49) )  b295 )  b442 )  b471 )  b619 )
  :assumption
(or (or (or (or (or (not b44)  b49 )  b347 )  b375 )  b523 )  b552 )
  :assumption
(or (or (or (or (or b49  (not b54) )  b301 )  b447 )  b478 )  b624 )
  :assumption
(or (or (or (or (or (not b49)  b54 )  b352 )  b381 )  b528 )  b558 )
  :assumption
(or (or (or b54  (not b308) )  b452 )  b629 )
  :assumption
(or (or (or (or (or (not b54)  b308 )  b357 )  b387 )  b533 )  b564 )
  :assumption
(or (or (not b18)  b393 )  b570 )
  :assumption
(or (or (or (or (or b18  (not b24) )  b337 )  b400 )  b513 )  b577 )
  :assumption
(or (or (or (or (or (not b18)  b24 )  b283 )  b310 )  b457 )  b487 )
  :assumption
(or (or (or (or (or b24  (not b30) )  b342 )  b405 )  b518 )  b582 )
  :assumption
(or (or (or (or (or (not b24)  b30 )  b289 )  b316 )  b464 )  b493 )
  :assumption
(or (or (or (or (or b30  (not b36) )  b347 )  b410 )  b523 )  b587 )
  :assumption
(or (or (or (or (or (not b30)  b36 )  b295 )  b322 )  b471 )  b499 )
  :assumption
(or (or (or (or (or b36  (not b87) )  b352 )  b415 )  b528 )  b592 )
  :assumption
(or (or (or (or (or (not b36)  b87 )  b301 )  b328 )  b478 )  b505 )
  :assumption
(or (or (or (or b87  b357 )  b420 )  b533 )  b597 )
  :assumption
(or (not b164)  b271 )
  :assumption
(or (or (not b163)  b164 )  b274 )
  :assumption
(or (or b161  b163 )  (not b164) )
  :assumption
(or (or b163  (not b168) )  b277 )
  :assumption
(or (or (not b163)  b166 )  b168 )
  :assumption
(or (or b168  (not b172) )  b280 )
  :assumption
(or (or (not b168)  b170 )  b172 )
  :assumption
(or (not b154)  b259 )
  :assumption
(or (or (not b153)  b154 )  b262 )
  :assumption
(or (or b151  b153 )  (not b154) )
  :assumption
(or (or b153  (not b158) )  b265 )
  :assumption
(or (or (not b153)  b156 )  b158 )
  :assumption
(or b158  b268 )
  :assumption
(or b126  b129 )
  :assumption
(or (or b129  (not b134) )  b247 )
  :assumption
(or (or (not b129)  b131 )  b134 )
  :assumption
(or (or b134  (not b139) )  b250 )
  :assumption
(or (or (not b134)  b136 )  b139 )
  :assumption
(or (or b139  (not b144) )  b253 )
  :assumption
(or (or (not b139)  b141 )  b144 )
  :assumption
(or (or b144  (not b149) )  b256 )
  :assumption
(or (or (not b144)  b146 )  b149 )
  :assumption
(or (not b116)  b235 )
  :assumption
(or (or (not b115)  b116 )  b238 )
  :assumption
(or (or b113  b115 )  (not b116) )
  :assumption
(or (or b115  (not b120) )  b241 )
  :assumption
(or (or (not b115)  b118 )  b120 )
  :assumption
(or (or b120  (not b124) )  b244 )
  :assumption
(or (or (not b120)  b122 )  b124 )
  :assumption
(or b89  b92 )
  :assumption
(or (or b92  (not b98) )  b223 )
  :assumption
(or (or (not b92)  b95 )  b98 )
  :assumption
(or (or b98  (not b103) )  b226 )
  :assumption
(or (or (not b98)  b101 )  b103 )
  :assumption
(or (or b103  (not b107) )  b229 )
  :assumption
(or (or (not b103)  b105 )  b107 )
  :assumption
(or (or b107  (not b111) )  b232 )
  :assumption
(or (or (not b107)  b109 )  b111 )
  :assumption
(or (not b76)  b211 )
  :assumption
(or (or (not b75)  b76 )  b214 )
  :assumption
(or (or b72  b75 )  (not b76) )
  :assumption
(or (or b75  (not b81) )  b217 )
  :assumption
(or (or (not b75)  b78 )  b81 )
  :assumption
(or (or b81  (not b86) )  b220 )
  :assumption
(or (or (not b81)  b83 )  b86 )
  :assumption
(or (not b59)  b198 )
  :assumption
(or (or (not b58)  b59 )  b202 )
  :assumption
(or (or b56  b58 )  (not b59) )
  :assumption
(or (or b58  (not b64) )  b205 )
  :assumption
(or (or (not b58)  b62 )  b64 )
  :assumption
(or (or b64  (not b69) )  b208 )
  :assumption
(or (or (not b64)  b67 )  b69 )
  :assumption
(or (not b43)  b186 )
  :assumption
(or (or (not b42)  b43 )  b189 )
  :assumption
(or (or b40  b42 )  (not b43) )
  :assumption
(or (or b42  (not b48) )  b192 )
  :assumption
(or (or (not b42)  b46 )  b48 )
  :assumption
(or (or b48  (not b53) )  b195 )
  :assumption
(or (or (not b48)  b51 )  b53 )
  :assumption
(or b14  b17 )
  :assumption
(or (or b17  (not b23) )  b174 )
  :assumption
(or (or (not b17)  b20 )  b23 )
  :assumption
(or (or b23  (not b29) )  b177 )
  :assumption
(or (or (not b23)  b26 )  b29 )
  :assumption
(or (or b29  (not b35) )  b180 )
  :assumption
(or (or (not b29)  b32 )  b35 )
  :assumption
(or b35  b183 )
  :assumption
(or b126  (not b128) )
  :assumption
(or (or b128  b131 )  (not b133) )
  :assumption
(or (or (or (or (not b128)  b133 )  b247 )  b259 )  b271 )
  :assumption
(or (or (or (or b133  b136 )  (not b138) )  b151 )  b161 )
  :assumption
(or (or (or (or (not b133)  b138 )  b250 )  b262 )  b274 )
  :assumption
(or (or (or (or b138  b141 )  (not b143) )  b156 )  b166 )
  :assumption
(or (or (or (or (not b138)  b143 )  b253 )  b265 )  b277 )
  :assumption
(or (or (or b143  b146 )  (not b148) )  b170 )
  :assumption
(or (or (or (or (not b143)  b148 )  b256 )  b268 )  b280 )
  :assumption
(or b89  (not b91) )
  :assumption
(or (or b91  b95 )  (not b97) )
  :assumption
(or (or (or (or (not b91)  b97 )  b211 )  b223 )  b235 )
  :assumption
(or (or (or (or b72  (not b74) )  b97 )  b101 )  b113 )
  :assumption
(or (or (or (or b74  (not b97) )  b214 )  b226 )  b238 )
  :assumption
(or (or (or (or b74  b78 )  (not b80) )  b105 )  b118 )
  :assumption
(or (or (or (or (not b74)  b80 )  b217 )  b229 )  b241 )
  :assumption
(or (or (or (or b80  b83 )  (not b85) )  b109 )  b122 )
  :assumption
(or (or (or (or (not b80)  b85 )  b220 )  b232 )  b244 )
  :assumption
(or b14  (not b16) )
  :assumption
(or (or b16  b20 )  (not b22) )
  :assumption
(or (or (or (or (not b16)  b22 )  b174 )  b186 )  b198 )
  :assumption
(or (or (or (or b22  b26 )  (not b28) )  b40 )  b56 )
  :assumption
(or (or (or (or (not b22)  b28 )  b177 )  b189 )  b202 )
  :assumption
(or (or (or (or b28  b32 )  (not b34) )  b46 )  b62 )
  :assumption
(or (or (or (or (not b28)  b34 )  b180 )  b192 )  b205 )
  :assumption
(or (or (or b34  (not b38) )  b51 )  b67 )
  :assumption
(or (or (or (or (not b34)  b38 )  b183 )  b195 )  b208 )
  :assumption
(or b653  (= (- (- (- (- (- r84 r11) r209) r197) r140) r128) 0) )
  :assumption
(or (or (or b633  b648 )  b656 )  (= (- (- (- (- (- (- (- (- (- (- (- (- (- r87 r84) r211) r199) r187) r176) r166) r152) r142) r130) r118) r107) r97) r83) 0) )
  :assumption
(or (or (or b636  b649 )  b657 )  (= (- (- (- (- (- (- (- (- (- (- (- (- (- r90 r87) r213) r201) r189) r178) r168) r155) r144) r132) r120) r109) r99) r86) 0) )
  :assumption
(or (or (or b639  b650 )  b658 )  (= (- (- (- (- (- (- (- (- (- (- (- (- (- r93 r90) r215) r203) r191) r180) r170) r158) r146) r134) r122) r111) r101) r89) 0) )
  :assumption
(or (or (or b642  b651 )  b659 )  (= (- (- (- (- (- (- (- (- (- (- (- (- (- r116 r93) r217) r205) r193) r182) r172) r161) r148) r136) r124) r113) r103) r92) 0) )
  :assumption
(or (or (or b645  b652 )  b660 )  (= (- (- (- (- (- (- (- (- (- (- (- (- (- r221 r116) r219) r207) r195) r184) r174) r164) r150) r138) r126) r115) r105) r95) 0) )
  :assumption
(or (not b20)  (not b174) )
  :assumption
(or (not b26)  (not b177) )
  :assumption
(or (not b32)  (not b180) )
  :assumption
(or (not b20)  (not b198) )
  :assumption
(or (not b26)  (not b202) )
  :assumption
(or (not b32)  (not b205) )
  :assumption
(or (not b20)  (not b186) )
  :assumption
(or (not b26)  (not b189) )
  :assumption
(or (not b32)  (not b192) )
  :assumption
(or (not b14)  (not b609) )
  :assumption
(or (not b20)  (not b614) )
  :assumption
(or (not b26)  (not b619) )
  :assumption
(or (not b32)  (not b624) )
  :assumption
(or (not b14)  (not b577) )
  :assumption
(or (not b20)  (not b582) )
  :assumption
(or (not b26)  (not b587) )
  :assumption
(or (not b32)  (not b592) )
  :assumption
(or (not b14)  (not b540) )
  :assumption
(or (not b20)  (not b546) )
  :assumption
(or (not b26)  (not b552) )
  :assumption
(or (not b32)  (not b558) )
  :assumption
(or (not b14)  (not b513) )
  :assumption
(or (not b20)  (not b518) )
  :assumption
(or (not b26)  (not b523) )
  :assumption
(or (not b32)  (not b528) )
  :assumption
(or (not b14)  (not b487) )
  :assumption
(or (not b20)  (not b493) )
  :assumption
(or (not b26)  (not b499) )
  :assumption
(or (not b32)  (not b505) )
  :assumption
(or (not b14)  (not b457) )
  :assumption
(or (not b20)  (not b464) )
  :assumption
(or (not b26)  (not b471) )
  :assumption
(or (not b32)  (not b478) )
  :assumption
(or (not b40)  (not b189) )
  :assumption
(or (not b46)  (not b192) )
  :assumption
(or (not b51)  (not b195) )
  :assumption
(or (not b40)  (not b202) )
  :assumption
(or (not b46)  (not b205) )
  :assumption
(or (not b51)  (not b208) )
  :assumption
(or (not b40)  (not b177) )
  :assumption
(or (not b46)  (not b180) )
  :assumption
(or (not b51)  (not b183) )
  :assumption
(or (not b40)  (not b619) )
  :assumption
(or (not b46)  (not b624) )
  :assumption
(or (not b51)  (not b629) )
  :assumption
(or (not b40)  (not b587) )
  :assumption
(or (not b46)  (not b592) )
  :assumption
(or (not b51)  (not b597) )
  :assumption
(or (not b40)  (not b552) )
  :assumption
(or (not b46)  (not b558) )
  :assumption
(or (not b51)  (not b564) )
  :assumption
(or (not b40)  (not b523) )
  :assumption
(or (not b46)  (not b528) )
  :assumption
(or (not b51)  (not b533) )
  :assumption
(or (not b40)  (not b499) )
  :assumption
(or (not b46)  (not b505) )
  :assumption
(or (not b40)  (not b471) )
  :assumption
(or (not b46)  (not b478) )
  :assumption
(or (not b56)  (not b202) )
  :assumption
(or (not b62)  (not b205) )
  :assumption
(or (not b67)  (not b208) )
  :assumption
(or (not b56)  (not b189) )
  :assumption
(or (not b62)  (not b192) )
  :assumption
(or (not b67)  (not b195) )
  :assumption
(or (not b56)  (not b177) )
  :assumption
(or (not b62)  (not b180) )
  :assumption
(or (not b67)  (not b183) )
  :assumption
(or (not b56)  (not b619) )
  :assumption
(or (not b62)  (not b624) )
  :assumption
(or (not b67)  (not b629) )
  :assumption
(or (not b56)  (not b587) )
  :assumption
(or (not b62)  (not b592) )
  :assumption
(or (not b67)  (not b597) )
  :assumption
(or (not b56)  (not b552) )
  :assumption
(or (not b62)  (not b558) )
  :assumption
(or (not b67)  (not b564) )
  :assumption
(or (not b56)  (not b523) )
  :assumption
(or (not b62)  (not b528) )
  :assumption
(or (not b67)  (not b533) )
  :assumption
(or (not b56)  (not b499) )
  :assumption
(or (not b62)  (not b505) )
  :assumption
(or (not b56)  (not b471) )
  :assumption
(or (not b62)  (not b478) )
  :assumption
(or (not b72)  (not b214) )
  :assumption
(or (not b78)  (not b217) )
  :assumption
(or (not b83)  (not b220) )
  :assumption
(or (not b72)  (not b238) )
  :assumption
(or (not b78)  (not b241) )
  :assumption
(or (not b83)  (not b244) )
  :assumption
(or (not b72)  (not b226) )
  :assumption
(or (not b78)  (not b229) )
  :assumption
(or (not b83)  (not b232) )
  :assumption
(or (not b72)  (not b619) )
  :assumption
(or (not b78)  (not b624) )
  :assumption
(or (not b83)  (not b629) )
  :assumption
(or (not b72)  (not b587) )
  :assumption
(or (not b78)  (not b592) )
  :assumption
(or (not b83)  (not b597) )
  :assumption
(or (not b72)  (not b552) )
  :assumption
(or (not b78)  (not b558) )
  :assumption
(or (not b83)  (not b564) )
  :assumption
(or (not b72)  (not b523) )
  :assumption
(or (not b78)  (not b528) )
  :assumption
(or (not b83)  (not b533) )
  :assumption
(or (not b72)  (not b499) )
  :assumption
(or (not b78)  (not b505) )
  :assumption
(or (not b72)  (not b471) )
  :assumption
(or (not b78)  (not b478) )
  :assumption
(or (not b95)  (not b223) )
  :assumption
(or (not b101)  (not b226) )
  :assumption
(or (not b105)  (not b229) )
  :assumption
(or (not b109)  (not b232) )
  :assumption
(or (not b95)  (not b235) )
  :assumption
(or (not b101)  (not b238) )
  :assumption
(or (not b105)  (not b241) )
  :assumption
(or (not b109)  (not b244) )
  :assumption
(or (not b95)  (not b211) )
  :assumption
(or (not b101)  (not b214) )
  :assumption
(or (not b105)  (not b217) )
  :assumption
(or (not b109)  (not b220) )
  :assumption
(or (not b89)  (not b609) )
  :assumption
(or (not b95)  (not b614) )
  :assumption
(or (not b101)  (not b619) )
  :assumption
(or (not b105)  (not b624) )
  :assumption
(or (not b109)  (not b629) )
  :assumption
(or (not b89)  (not b577) )
  :assumption
(or (not b95)  (not b582) )
  :assumption
(or (not b101)  (not b587) )
  :assumption
(or (not b105)  (not b592) )
  :assumption
(or (not b109)  (not b597) )
  :assumption
(or (not b89)  (not b540) )
  :assumption
(or (not b95)  (not b546) )
  :assumption
(or (not b101)  (not b552) )
  :assumption
(or (not b105)  (not b558) )
  :assumption
(or (not b109)  (not b564) )
  :assumption
(or (not b89)  (not b513) )
  :assumption
(or (not b95)  (not b518) )
  :assumption
(or (not b101)  (not b523) )
  :assumption
(or (not b105)  (not b528) )
  :assumption
(or (not b109)  (not b533) )
  :assumption
(or (not b89)  (not b487) )
  :assumption
(or (not b95)  (not b493) )
  :assumption
(or (not b101)  (not b499) )
  :assumption
(or (not b105)  (not b505) )
  :assumption
(or (not b89)  (not b457) )
  :assumption
(or (not b95)  (not b464) )
  :assumption
(or (not b101)  (not b471) )
  :assumption
(or (not b105)  (not b478) )
  :assumption
(or (not b113)  (not b238) )
  :assumption
(or (not b118)  (not b241) )
  :assumption
(or (not b122)  (not b244) )
  :assumption
(or (not b113)  (not b226) )
  :assumption
(or (not b118)  (not b229) )
  :assumption
(or (not b122)  (not b232) )
  :assumption
(or (not b113)  (not b214) )
  :assumption
(or (not b118)  (not b217) )
  :assumption
(or (not b122)  (not b220) )
  :assumption
(or (not b113)  (not b619) )
  :assumption
(or (not b118)  (not b624) )
  :assumption
(or (not b122)  (not b629) )
  :assumption
(or (not b113)  (not b587) )
  :assumption
(or (not b118)  (not b592) )
  :assumption
(or (not b122)  (not b597) )
  :assumption
(or (not b113)  (not b552) )
  :assumption
(or (not b118)  (not b558) )
  :assumption
(or (not b122)  (not b564) )
  :assumption
(or (not b113)  (not b523) )
  :assumption
(or (not b118)  (not b528) )
  :assumption
(or (not b122)  (not b533) )
  :assumption
(or (not b113)  (not b499) )
  :assumption
(or (not b118)  (not b505) )
  :assumption
(or (not b113)  (not b471) )
  :assumption
(or (not b118)  (not b478) )
  :assumption
(or (not b131)  (not b247) )
  :assumption
(or (not b136)  (not b250) )
  :assumption
(or (not b141)  (not b253) )
  :assumption
(or (not b146)  (not b256) )
  :assumption
(or (not b131)  (not b271) )
  :assumption
(or (not b136)  (not b274) )
  :assumption
(or (not b141)  (not b277) )
  :assumption
(or (not b146)  (not b280) )
  :assumption
(or (not b131)  (not b259) )
  :assumption
(or (not b136)  (not b262) )
  :assumption
(or (not b141)  (not b265) )
  :assumption
(or (not b146)  (not b268) )
  :assumption
(or (not b126)  (not b609) )
  :assumption
(or (not b131)  (not b614) )
  :assumption
(or (not b136)  (not b619) )
  :assumption
(or (not b141)  (not b624) )
  :assumption
(or (not b146)  (not b629) )
  :assumption
(or (not b126)  (not b577) )
  :assumption
(or (not b131)  (not b582) )
  :assumption
(or (not b136)  (not b587) )
  :assumption
(or (not b141)  (not b592) )
  :assumption
(or (not b146)  (not b597) )
  :assumption
(or (not b126)  (not b540) )
  :assumption
(or (not b131)  (not b546) )
  :assumption
(or (not b136)  (not b552) )
  :assumption
(or (not b141)  (not b558) )
  :assumption
(or (not b146)  (not b564) )
  :assumption
(or (not b126)  (not b513) )
  :assumption
(or (not b131)  (not b518) )
  :assumption
(or (not b136)  (not b523) )
  :assumption
(or (not b141)  (not b528) )
  :assumption
(or (not b146)  (not b533) )
  :assumption
(or (not b126)  (not b487) )
  :assumption
(or (not b131)  (not b493) )
  :assumption
(or (not b136)  (not b499) )
  :assumption
(or (not b141)  (not b505) )
  :assumption
(or (not b126)  (not b457) )
  :assumption
(or (not b131)  (not b464) )
  :assumption
(or (not b136)  (not b471) )
  :assumption
(or (not b141)  (not b478) )
  :assumption
(or (not b151)  (not b262) )
  :assumption
(or (not b156)  (not b265) )
  :assumption
(or (not b151)  (not b274) )
  :assumption
(or (not b156)  (not b277) )
  :assumption
(or (not b151)  (not b250) )
  :assumption
(or (not b156)  (not b253) )
  :assumption
(or (not b151)  (not b619) )
  :assumption
(or (not b156)  (not b624) )
  :assumption
(or (not b151)  (not b587) )
  :assumption
(or (not b156)  (not b592) )
  :assumption
(or (not b151)  (not b552) )
  :assumption
(or (not b156)  (not b558) )
  :assumption
(or (not b151)  (not b523) )
  :assumption
(or (not b156)  (not b528) )
  :assumption
(or (not b151)  (not b499) )
  :assumption
(or (not b156)  (not b505) )
  :assumption
(or (not b151)  (not b471) )
  :assumption
(or (not b156)  (not b478) )
  :assumption
(or (not b161)  (not b274) )
  :assumption
(or (not b166)  (not b277) )
  :assumption
(or (not b170)  (not b280) )
  :assumption
(or (not b161)  (not b262) )
  :assumption
(or (not b166)  (not b265) )
  :assumption
(or (not b170)  (not b268) )
  :assumption
(or (not b161)  (not b250) )
  :assumption
(or (not b166)  (not b253) )
  :assumption
(or (not b170)  (not b256) )
  :assumption
(or (not b161)  (not b619) )
  :assumption
(or (not b166)  (not b624) )
  :assumption
(or (not b170)  (not b629) )
  :assumption
(or (not b161)  (not b587) )
  :assumption
(or (not b166)  (not b592) )
  :assumption
(or (not b170)  (not b597) )
  :assumption
(or (not b161)  (not b552) )
  :assumption
(or (not b166)  (not b558) )
  :assumption
(or (not b170)  (not b564) )
  :assumption
(or (not b161)  (not b523) )
  :assumption
(or (not b166)  (not b528) )
  :assumption
(or (not b170)  (not b533) )
  :assumption
(or (not b161)  (not b499) )
  :assumption
(or (not b166)  (not b505) )
  :assumption
(or (not b161)  (not b471) )
  :assumption
(or (not b166)  (not b478) )
  :assumption
(or (not b174)  (not b198) )
  :assumption
(or (not b177)  (not b202) )
  :assumption
(or (not b180)  (not b205) )
  :assumption
(or (not b183)  (not b208) )
  :assumption
(or (not b174)  (not b186) )
  :assumption
(or (not b177)  (not b189) )
  :assumption
(or (not b180)  (not b192) )
  :assumption
(or (not b183)  (not b195) )
  :assumption
(or (not b174)  (not b614) )
  :assumption
(or (not b177)  (not b619) )
  :assumption
(or (not b180)  (not b624) )
  :assumption
(or (not b183)  (not b629) )
  :assumption
(or (not b174)  (not b582) )
  :assumption
(or (not b177)  (not b587) )
  :assumption
(or (not b180)  (not b592) )
  :assumption
(or (not b183)  (not b597) )
  :assumption
(or (not b174)  (not b546) )
  :assumption
(or (not b177)  (not b552) )
  :assumption
(or (not b180)  (not b558) )
  :assumption
(or (not b183)  (not b564) )
  :assumption
(or (not b174)  (not b518) )
  :assumption
(or (not b177)  (not b523) )
  :assumption
(or (not b180)  (not b528) )
  :assumption
(or (not b183)  (not b533) )
  :assumption
(or (not b174)  (not b493) )
  :assumption
(or (not b177)  (not b499) )
  :assumption
(or (not b180)  (not b505) )
  :assumption
(or (not b174)  (not b464) )
  :assumption
(or (not b177)  (not b471) )
  :assumption
(or (not b180)  (not b478) )
  :assumption
(or (not b186)  (not b198) )
  :assumption
(or (not b189)  (not b202) )
  :assumption
(or (not b192)  (not b205) )
  :assumption
(or (not b195)  (not b208) )
  :assumption
(or (not b186)  (not b614) )
  :assumption
(or (not b189)  (not b619) )
  :assumption
(or (not b192)  (not b624) )
  :assumption
(or (not b195)  (not b629) )
  :assumption
(or (not b186)  (not b582) )
  :assumption
(or (not b189)  (not b587) )
  :assumption
(or (not b192)  (not b592) )
  :assumption
(or (not b195)  (not b597) )
  :assumption
(or (not b186)  (not b546) )
  :assumption
(or (not b189)  (not b552) )
  :assumption
(or (not b192)  (not b558) )
  :assumption
(or (not b195)  (not b564) )
  :assumption
(or (not b186)  (not b518) )
  :assumption
(or (not b189)  (not b523) )
  :assumption
(or (not b192)  (not b528) )
  :assumption
(or (not b195)  (not b533) )
  :assumption
(or (not b186)  (not b493) )
  :assumption
(or (not b189)  (not b499) )
  :assumption
(or (not b192)  (not b505) )
  :assumption
(or (not b186)  (not b464) )
  :assumption
(or (not b189)  (not b471) )
  :assumption
(or (not b192)  (not b478) )
  :assumption
(or (not b198)  (not b614) )
  :assumption
(or (not b202)  (not b619) )
  :assumption
(or (not b205)  (not b624) )
  :assumption
(or (not b208)  (not b629) )
  :assumption
(or (not b198)  (not b582) )
  :assumption
(or (not b202)  (not b587) )
  :assumption
(or (not b205)  (not b592) )
  :assumption
(or (not b208)  (not b597) )
  :assumption
(or (not b198)  (not b546) )
  :assumption
(or (not b202)  (not b552) )
  :assumption
(or (not b205)  (not b558) )
  :assumption
(or (not b208)  (not b564) )
  :assumption
(or (not b198)  (not b518) )
  :assumption
(or (not b202)  (not b523) )
  :assumption
(or (not b205)  (not b528) )
  :assumption
(or (not b208)  (not b533) )
  :assumption
(or (not b198)  (not b493) )
  :assumption
(or (not b202)  (not b499) )
  :assumption
(or (not b205)  (not b505) )
  :assumption
(or (not b198)  (not b464) )
  :assumption
(or (not b202)  (not b471) )
  :assumption
(or (not b205)  (not b478) )
  :assumption
(or (not b211)  (not b235) )
  :assumption
(or (not b214)  (not b238) )
  :assumption
(or (not b217)  (not b241) )
  :assumption
(or (not b220)  (not b244) )
  :assumption
(or (not b211)  (not b223) )
  :assumption
(or (not b214)  (not b226) )
  :assumption
(or (not b217)  (not b229) )
  :assumption
(or (not b220)  (not b232) )
  :assumption
(or (not b211)  (not b614) )
  :assumption
(or (not b214)  (not b619) )
  :assumption
(or (not b217)  (not b624) )
  :assumption
(or (not b220)  (not b629) )
  :assumption
(or (not b211)  (not b582) )
  :assumption
(or (not b214)  (not b587) )
  :assumption
(or (not b217)  (not b592) )
  :assumption
(or (not b220)  (not b597) )
  :assumption
(or (not b211)  (not b546) )
  :assumption
(or (not b214)  (not b552) )
  :assumption
(or (not b217)  (not b558) )
  :assumption
(or (not b220)  (not b564) )
  :assumption
(or (not b211)  (not b518) )
  :assumption
(or (not b214)  (not b523) )
  :assumption
(or (not b217)  (not b528) )
  :assumption
(or (not b220)  (not b533) )
  :assumption
(or (not b211)  (not b493) )
  :assumption
(or (not b214)  (not b499) )
  :assumption
(or (not b217)  (not b505) )
  :assumption
(or (not b211)  (not b464) )
  :assumption
(or (not b214)  (not b471) )
  :assumption
(or (not b217)  (not b478) )
  :assumption
(or (not b223)  (not b235) )
  :assumption
(or (not b226)  (not b238) )
  :assumption
(or (not b229)  (not b241) )
  :assumption
(or (not b232)  (not b244) )
  :assumption
(or (not b223)  (not b614) )
  :assumption
(or (not b226)  (not b619) )
  :assumption
(or (not b229)  (not b624) )
  :assumption
(or (not b232)  (not b629) )
  :assumption
(or (not b223)  (not b582) )
  :assumption
(or (not b226)  (not b587) )
  :assumption
(or (not b229)  (not b592) )
  :assumption
(or (not b232)  (not b597) )
  :assumption
(or (not b223)  (not b546) )
  :assumption
(or (not b226)  (not b552) )
  :assumption
(or (not b229)  (not b558) )
  :assumption
(or (not b232)  (not b564) )
  :assumption
(or (not b223)  (not b518) )
  :assumption
(or (not b226)  (not b523) )
  :assumption
(or (not b229)  (not b528) )
  :assumption
(or (not b232)  (not b533) )
  :assumption
(or (not b223)  (not b493) )
  :assumption
(or (not b226)  (not b499) )
  :assumption
(or (not b229)  (not b505) )
  :assumption
(or (not b223)  (not b464) )
  :assumption
(or (not b226)  (not b471) )
  :assumption
(or (not b229)  (not b478) )
  :assumption
(or (not b235)  (not b614) )
  :assumption
(or (not b238)  (not b619) )
  :assumption
(or (not b241)  (not b624) )
  :assumption
(or (not b244)  (not b629) )
  :assumption
(or (not b235)  (not b582) )
  :assumption
(or (not b238)  (not b587) )
  :assumption
(or (not b241)  (not b592) )
  :assumption
(or (not b244)  (not b597) )
  :assumption
(or (not b235)  (not b546) )
  :assumption
(or (not b238)  (not b552) )
  :assumption
(or (not b241)  (not b558) )
  :assumption
(or (not b244)  (not b564) )
  :assumption
(or (not b235)  (not b518) )
  :assumption
(or (not b238)  (not b523) )
  :assumption
(or (not b241)  (not b528) )
  :assumption
(or (not b244)  (not b533) )
  :assumption
(or (not b235)  (not b493) )
  :assumption
(or (not b238)  (not b499) )
  :assumption
(or (not b241)  (not b505) )
  :assumption
(or (not b235)  (not b464) )
  :assumption
(or (not b238)  (not b471) )
  :assumption
(or (not b241)  (not b478) )
  :assumption
(or (not b247)  (not b271) )
  :assumption
(or (not b250)  (not b274) )
  :assumption
(or (not b253)  (not b277) )
  :assumption
(or (not b256)  (not b280) )
  :assumption
(or (not b247)  (not b259) )
  :assumption
(or (not b250)  (not b262) )
  :assumption
(or (not b253)  (not b265) )
  :assumption
(or (not b256)  (not b268) )
  :assumption
(or (not b247)  (not b614) )
  :assumption
(or (not b250)  (not b619) )
  :assumption
(or (not b253)  (not b624) )
  :assumption
(or (not b256)  (not b629) )
  :assumption
(or (not b247)  (not b582) )
  :assumption
(or (not b250)  (not b587) )
  :assumption
(or (not b253)  (not b592) )
  :assumption
(or (not b256)  (not b597) )
  :assumption
(or (not b247)  (not b546) )
  :assumption
(or (not b250)  (not b552) )
  :assumption
(or (not b253)  (not b558) )
  :assumption
(or (not b256)  (not b564) )
  :assumption
(or (not b247)  (not b518) )
  :assumption
(or (not b250)  (not b523) )
  :assumption
(or (not b253)  (not b528) )
  :assumption
(or (not b256)  (not b533) )
  :assumption
(or (not b247)  (not b493) )
  :assumption
(or (not b250)  (not b499) )
  :assumption
(or (not b253)  (not b505) )
  :assumption
(or (not b247)  (not b464) )
  :assumption
(or (not b250)  (not b471) )
  :assumption
(or (not b253)  (not b478) )
  :assumption
(or (not b259)  (not b271) )
  :assumption
(or (not b262)  (not b274) )
  :assumption
(or (not b265)  (not b277) )
  :assumption
(or (not b268)  (not b280) )
  :assumption
(or (not b259)  (not b614) )
  :assumption
(or (not b262)  (not b619) )
  :assumption
(or (not b265)  (not b624) )
  :assumption
(or (not b268)  (not b629) )
  :assumption
(or (not b259)  (not b582) )
  :assumption
(or (not b262)  (not b587) )
  :assumption
(or (not b265)  (not b592) )
  :assumption
(or (not b268)  (not b597) )
  :assumption
(or (not b259)  (not b546) )
  :assumption
(or (not b262)  (not b552) )
  :assumption
(or (not b265)  (not b558) )
  :assumption
(or (not b268)  (not b564) )
  :assumption
(or (not b259)  (not b518) )
  :assumption
(or (not b262)  (not b523) )
  :assumption
(or (not b265)  (not b528) )
  :assumption
(or (not b268)  (not b533) )
  :assumption
(or (not b259)  (not b493) )
  :assumption
(or (not b262)  (not b499) )
  :assumption
(or (not b265)  (not b505) )
  :assumption
(or (not b259)  (not b464) )
  :assumption
(or (not b262)  (not b471) )
  :assumption
(or (not b265)  (not b478) )
  :assumption
(or (not b271)  (not b614) )
  :assumption
(or (not b274)  (not b619) )
  :assumption
(or (not b277)  (not b624) )
  :assumption
(or (not b280)  (not b629) )
  :assumption
(or (not b271)  (not b582) )
  :assumption
(or (not b274)  (not b587) )
  :assumption
(or (not b277)  (not b592) )
  :assumption
(or (not b280)  (not b597) )
  :assumption
(or (not b271)  (not b546) )
  :assumption
(or (not b274)  (not b552) )
  :assumption
(or (not b277)  (not b558) )
  :assumption
(or (not b280)  (not b564) )
  :assumption
(or (not b271)  (not b518) )
  :assumption
(or (not b274)  (not b523) )
  :assumption
(or (not b277)  (not b528) )
  :assumption
(or (not b280)  (not b533) )
  :assumption
(or (not b271)  (not b493) )
  :assumption
(or (not b274)  (not b499) )
  :assumption
(or (not b277)  (not b505) )
  :assumption
(or (not b271)  (not b464) )
  :assumption
(or (not b274)  (not b471) )
  :assumption
(or (not b277)  (not b478) )
  :assumption
(or (not b283)  (not b633) )
  :assumption
(or (not b289)  (not b636) )
  :assumption
(or (not b295)  (not b639) )
  :assumption
(or (not b301)  (not b642) )
  :assumption
(or (not b283)  (not b487) )
  :assumption
(or (not b289)  (not b493) )
  :assumption
(or (not b295)  (not b499) )
  :assumption
(or (not b301)  (not b505) )
  :assumption
(or (not b283)  (not b457) )
  :assumption
(or (not b289)  (not b464) )
  :assumption
(or (not b295)  (not b471) )
  :assumption
(or (not b301)  (not b478) )
  :assumption
(or (not b283)  (not b310) )
  :assumption
(or (not b289)  (not b316) )
  :assumption
(or (not b295)  (not b322) )
  :assumption
(or (not b301)  (not b328) )
  :assumption
(or (not b247)  (not b289) )
  :assumption
(or (not b250)  (not b295) )
  :assumption
(or (not b253)  (not b301) )
  :assumption
(or (not b211)  (not b289) )
  :assumption
(or (not b214)  (not b295) )
  :assumption
(or (not b217)  (not b301) )
  :assumption
(or (not b174)  (not b289) )
  :assumption
(or (not b177)  (not b295) )
  :assumption
(or (not b180)  (not b301) )
  :assumption
(or (not b126)  (not b283) )
  :assumption
(or (not b131)  (not b289) )
  :assumption
(or (not b136)  (not b295) )
  :assumption
(or (not b141)  (not b301) )
  :assumption
(or (not b72)  (not b295) )
  :assumption
(or (not b78)  (not b301) )
  :assumption
(or (not b14)  (not b283) )
  :assumption
(or (not b20)  (not b289) )
  :assumption
(or (not b26)  (not b295) )
  :assumption
(or (not b32)  (not b301) )
  :assumption
(or (not b283)  (not b577) )
  :assumption
(or (not b289)  (not b582) )
  :assumption
(or (not b295)  (not b587) )
  :assumption
(or (not b301)  (not b592) )
  :assumption
(or (not b283)  (not b513) )
  :assumption
(or (not b289)  (not b518) )
  :assumption
(or (not b295)  (not b523) )
  :assumption
(or (not b301)  (not b528) )
  :assumption
(or (not b283)  (not b400) )
  :assumption
(or (not b289)  (not b405) )
  :assumption
(or (not b295)  (not b410) )
  :assumption
(or (not b301)  (not b415) )
  :assumption
(or (not b283)  (not b337) )
  :assumption
(or (not b289)  (not b342) )
  :assumption
(or (not b295)  (not b347) )
  :assumption
(or (not b301)  (not b352) )
  :assumption
(or (not b283)  (not b648) )
  :assumption
(or (not b289)  (not b649) )
  :assumption
(or (not b295)  (not b650) )
  :assumption
(or (not b301)  (not b651) )
  :assumption
(or (not b283)  (not b540) )
  :assumption
(or (not b289)  (not b546) )
  :assumption
(or (not b295)  (not b552) )
  :assumption
(or (not b301)  (not b558) )
  :assumption
(or (not b283)  (not b363) )
  :assumption
(or (not b289)  (not b369) )
  :assumption
(or (not b295)  (not b375) )
  :assumption
(or (not b301)  (not b381) )
  :assumption
(or (not b259)  (not b289) )
  :assumption
(or (not b262)  (not b295) )
  :assumption
(or (not b265)  (not b301) )
  :assumption
(or (not b223)  (not b289) )
  :assumption
(or (not b226)  (not b295) )
  :assumption
(or (not b229)  (not b301) )
  :assumption
(or (not b186)  (not b289) )
  :assumption
(or (not b189)  (not b295) )
  :assumption
(or (not b192)  (not b301) )
  :assumption
(or (not b151)  (not b295) )
  :assumption
(or (not b156)  (not b301) )
  :assumption
(or (not b89)  (not b283) )
  :assumption
(or (not b95)  (not b289) )
  :assumption
(or (not b101)  (not b295) )
  :assumption
(or (not b105)  (not b301) )
  :assumption
(or (not b40)  (not b295) )
  :assumption
(or (not b46)  (not b301) )
  :assumption
(or (not b283)  (not b656) )
  :assumption
(or (not b289)  (not b657) )
  :assumption
(or (not b295)  (not b658) )
  :assumption
(or (not b301)  (not b659) )
  :assumption
(or (not b283)  (not b609) )
  :assumption
(or (not b289)  (not b614) )
  :assumption
(or (not b295)  (not b619) )
  :assumption
(or (not b301)  (not b624) )
  :assumption
(or (not b283)  (not b432) )
  :assumption
(or (not b289)  (not b437) )
  :assumption
(or (not b295)  (not b442) )
  :assumption
(or (not b301)  (not b447) )
  :assumption
(or (not b310)  (not b633) )
  :assumption
(or (not b316)  (not b636) )
  :assumption
(or (not b322)  (not b639) )
  :assumption
(or (not b328)  (not b642) )
  :assumption
(or (not b310)  (not b487) )
  :assumption
(or (not b316)  (not b493) )
  :assumption
(or (not b322)  (not b499) )
  :assumption
(or (not b328)  (not b505) )
  :assumption
(or (not b310)  (not b457) )
  :assumption
(or (not b316)  (not b464) )
  :assumption
(or (not b322)  (not b471) )
  :assumption
(or (not b328)  (not b478) )
  :assumption
(or (not b247)  (not b316) )
  :assumption
(or (not b250)  (not b322) )
  :assumption
(or (not b253)  (not b328) )
  :assumption
(or (not b211)  (not b316) )
  :assumption
(or (not b214)  (not b322) )
  :assumption
(or (not b217)  (not b328) )
  :assumption
(or (not b174)  (not b316) )
  :assumption
(or (not b177)  (not b322) )
  :assumption
(or (not b180)  (not b328) )
  :assumption
(or (not b126)  (not b310) )
  :assumption
(or (not b131)  (not b316) )
  :assumption
(or (not b136)  (not b322) )
  :assumption
(or (not b141)  (not b328) )
  :assumption
(or (not b72)  (not b322) )
  :assumption
(or (not b78)  (not b328) )
  :assumption
(or (not b14)  (not b310) )
  :assumption
(or (not b20)  (not b316) )
  :assumption
(or (not b26)  (not b322) )
  :assumption
(or (not b32)  (not b328) )
  :assumption
(or (not b310)  (not b577) )
  :assumption
(or (not b316)  (not b582) )
  :assumption
(or (not b322)  (not b587) )
  :assumption
(or (not b328)  (not b592) )
  :assumption
(or (not b310)  (not b513) )
  :assumption
(or (not b316)  (not b518) )
  :assumption
(or (not b322)  (not b523) )
  :assumption
(or (not b328)  (not b528) )
  :assumption
(or (not b310)  (not b400) )
  :assumption
(or (not b316)  (not b405) )
  :assumption
(or (not b322)  (not b410) )
  :assumption
(or (not b328)  (not b415) )
  :assumption
(or (not b310)  (not b337) )
  :assumption
(or (not b316)  (not b342) )
  :assumption
(or (not b322)  (not b347) )
  :assumption
(or (not b328)  (not b352) )
  :assumption
(or (not b310)  (not b656) )
  :assumption
(or (not b316)  (not b657) )
  :assumption
(or (not b322)  (not b658) )
  :assumption
(or (not b328)  (not b659) )
  :assumption
(or (not b310)  (not b609) )
  :assumption
(or (not b316)  (not b614) )
  :assumption
(or (not b322)  (not b619) )
  :assumption
(or (not b328)  (not b624) )
  :assumption
(or (not b310)  (not b432) )
  :assumption
(or (not b316)  (not b437) )
  :assumption
(or (not b322)  (not b442) )
  :assumption
(or (not b328)  (not b447) )
  :assumption
(or (not b271)  (not b316) )
  :assumption
(or (not b274)  (not b322) )
  :assumption
(or (not b277)  (not b328) )
  :assumption
(or (not b235)  (not b316) )
  :assumption
(or (not b238)  (not b322) )
  :assumption
(or (not b241)  (not b328) )
  :assumption
(or (not b198)  (not b316) )
  :assumption
(or (not b202)  (not b322) )
  :assumption
(or (not b205)  (not b328) )
  :assumption
(or (not b161)  (not b322) )
  :assumption
(or (not b166)  (not b328) )
  :assumption
(or (not b113)  (not b322) )
  :assumption
(or (not b118)  (not b328) )
  :assumption
(or (not b56)  (not b322) )
  :assumption
(or (not b62)  (not b328) )
  :assumption
(or (not b310)  (not b648) )
  :assumption
(or (not b316)  (not b649) )
  :assumption
(or (not b322)  (not b650) )
  :assumption
(or (not b328)  (not b651) )
  :assumption
(or (not b310)  (not b540) )
  :assumption
(or (not b316)  (not b546) )
  :assumption
(or (not b322)  (not b552) )
  :assumption
(or (not b328)  (not b558) )
  :assumption
(or (not b310)  (not b363) )
  :assumption
(or (not b316)  (not b369) )
  :assumption
(or (not b322)  (not b375) )
  :assumption
(or (not b328)  (not b381) )
  :assumption
(or (not b337)  (not b648) )
  :assumption
(or (not b342)  (not b649) )
  :assumption
(or (not b347)  (not b650) )
  :assumption
(or (not b352)  (not b651) )
  :assumption
(or (not b357)  (not b652) )
  :assumption
(or (not b337)  (not b540) )
  :assumption
(or (not b342)  (not b546) )
  :assumption
(or (not b347)  (not b552) )
  :assumption
(or (not b352)  (not b558) )
  :assumption
(or (not b357)  (not b564) )
  :assumption
(or (not b337)  (not b513) )
  :assumption
(or (not b342)  (not b518) )
  :assumption
(or (not b347)  (not b523) )
  :assumption
(or (not b352)  (not b528) )
  :assumption
(or (not b357)  (not b533) )
  :assumption
(or (not b337)  (not b363) )
  :assumption
(or (not b342)  (not b369) )
  :assumption
(or (not b347)  (not b375) )
  :assumption
(or (not b352)  (not b381) )
  :assumption
(or (not b357)  (not b387) )
  :assumption
(or (not b259)  (not b342) )
  :assumption
(or (not b262)  (not b347) )
  :assumption
(or (not b265)  (not b352) )
  :assumption
(or (not b268)  (not b357) )
  :assumption
(or (not b223)  (not b342) )
  :assumption
(or (not b226)  (not b347) )
  :assumption
(or (not b229)  (not b352) )
  :assumption
(or (not b232)  (not b357) )
  :assumption
(or (not b186)  (not b342) )
  :assumption
(or (not b189)  (not b347) )
  :assumption
(or (not b192)  (not b352) )
  :assumption
(or (not b195)  (not b357) )
  :assumption
(or (not b151)  (not b347) )
  :assumption
(or (not b156)  (not b352) )
  :assumption
(or (not b89)  (not b337) )
  :assumption
(or (not b95)  (not b342) )
  :assumption
(or (not b101)  (not b347) )
  :assumption
(or (not b105)  (not b352) )
  :assumption
(or (not b109)  (not b357) )
  :assumption
(or (not b40)  (not b347) )
  :assumption
(or (not b46)  (not b352) )
  :assumption
(or (not b51)  (not b357) )
  :assumption
(or (not b337)  (not b609) )
  :assumption
(or (not b342)  (not b614) )
  :assumption
(or (not b347)  (not b619) )
  :assumption
(or (not b352)  (not b624) )
  :assumption
(or (not b357)  (not b629) )
  :assumption
(or (not b337)  (not b457) )
  :assumption
(or (not b342)  (not b464) )
  :assumption
(or (not b347)  (not b471) )
  :assumption
(or (not b352)  (not b478) )
  :assumption
(or (not b337)  (not b432) )
  :assumption
(or (not b342)  (not b437) )
  :assumption
(or (not b347)  (not b442) )
  :assumption
(or (not b352)  (not b447) )
  :assumption
(or (not b357)  (not b452) )
  :assumption
(or (not b337)  (not b633) )
  :assumption
(or (not b342)  (not b636) )
  :assumption
(or (not b347)  (not b639) )
  :assumption
(or (not b352)  (not b642) )
  :assumption
(or (not b357)  (not b645) )
  :assumption
(or (not b337)  (not b487) )
  :assumption
(or (not b342)  (not b493) )
  :assumption
(or (not b347)  (not b499) )
  :assumption
(or (not b352)  (not b505) )
  :assumption
(or (not b247)  (not b342) )
  :assumption
(or (not b250)  (not b347) )
  :assumption
(or (not b253)  (not b352) )
  :assumption
(or (not b256)  (not b357) )
  :assumption
(or (not b211)  (not b342) )
  :assumption
(or (not b214)  (not b347) )
  :assumption
(or (not b217)  (not b352) )
  :assumption
(or (not b220)  (not b357) )
  :assumption
(or (not b174)  (not b342) )
  :assumption
(or (not b177)  (not b347) )
  :assumption
(or (not b180)  (not b352) )
  :assumption
(or (not b183)  (not b357) )
  :assumption
(or (not b126)  (not b337) )
  :assumption
(or (not b131)  (not b342) )
  :assumption
(or (not b136)  (not b347) )
  :assumption
(or (not b141)  (not b352) )
  :assumption
(or (not b146)  (not b357) )
  :assumption
(or (not b72)  (not b347) )
  :assumption
(or (not b78)  (not b352) )
  :assumption
(or (not b83)  (not b357) )
  :assumption
(or (not b14)  (not b337) )
  :assumption
(or (not b20)  (not b342) )
  :assumption
(or (not b26)  (not b347) )
  :assumption
(or (not b32)  (not b352) )
  :assumption
(or (not b337)  (not b656) )
  :assumption
(or (not b342)  (not b657) )
  :assumption
(or (not b347)  (not b658) )
  :assumption
(or (not b352)  (not b659) )
  :assumption
(or (not b357)  (not b660) )
  :assumption
(or (not b337)  (not b577) )
  :assumption
(or (not b342)  (not b582) )
  :assumption
(or (not b347)  (not b587) )
  :assumption
(or (not b352)  (not b592) )
  :assumption
(or (not b357)  (not b597) )
  :assumption
(or (not b337)  (not b400) )
  :assumption
(or (not b342)  (not b405) )
  :assumption
(or (not b347)  (not b410) )
  :assumption
(or (not b352)  (not b415) )
  :assumption
(or (not b357)  (not b420) )
  :assumption
(or (not b363)  (not b648) )
  :assumption
(or (not b369)  (not b649) )
  :assumption
(or (not b375)  (not b650) )
  :assumption
(or (not b381)  (not b651) )
  :assumption
(or (not b387)  (not b652) )
  :assumption
(or (not b363)  (not b540) )
  :assumption
(or (not b369)  (not b546) )
  :assumption
(or (not b375)  (not b552) )
  :assumption
(or (not b381)  (not b558) )
  :assumption
(or (not b387)  (not b564) )
  :assumption
(or (not b363)  (not b513) )
  :assumption
(or (not b369)  (not b518) )
  :assumption
(or (not b375)  (not b523) )
  :assumption
(or (not b381)  (not b528) )
  :assumption
(or (not b387)  (not b533) )
  :assumption
(or (not b259)  (not b369) )
  :assumption
(or (not b262)  (not b375) )
  :assumption
(or (not b265)  (not b381) )
  :assumption
(or (not b268)  (not b387) )
  :assumption
(or (not b223)  (not b369) )
  :assumption
(or (not b226)  (not b375) )
  :assumption
(or (not b229)  (not b381) )
  :assumption
(or (not b232)  (not b387) )
  :assumption
(or (not b186)  (not b369) )
  :assumption
(or (not b189)  (not b375) )
  :assumption
(or (not b192)  (not b381) )
  :assumption
(or (not b195)  (not b387) )
  :assumption
(or (not b151)  (not b375) )
  :assumption
(or (not b156)  (not b381) )
  :assumption
(or (not b89)  (not b363) )
  :assumption
(or (not b95)  (not b369) )
  :assumption
(or (not b101)  (not b375) )
  :assumption
(or (not b105)  (not b381) )
  :assumption
(or (not b109)  (not b387) )
  :assumption
(or (not b40)  (not b375) )
  :assumption
(or (not b46)  (not b381) )
  :assumption
(or (not b51)  (not b387) )
  :assumption
(or (not b363)  (not b609) )
  :assumption
(or (not b369)  (not b614) )
  :assumption
(or (not b375)  (not b619) )
  :assumption
(or (not b381)  (not b624) )
  :assumption
(or (not b387)  (not b629) )
  :assumption
(or (not b363)  (not b457) )
  :assumption
(or (not b369)  (not b464) )
  :assumption
(or (not b375)  (not b471) )
  :assumption
(or (not b381)  (not b478) )
  :assumption
(or (not b363)  (not b432) )
  :assumption
(or (not b369)  (not b437) )
  :assumption
(or (not b375)  (not b442) )
  :assumption
(or (not b381)  (not b447) )
  :assumption
(or (not b387)  (not b452) )
  :assumption
(or (not b363)  (not b656) )
  :assumption
(or (not b369)  (not b657) )
  :assumption
(or (not b375)  (not b658) )
  :assumption
(or (not b381)  (not b659) )
  :assumption
(or (not b387)  (not b660) )
  :assumption
(or (not b363)  (not b577) )
  :assumption
(or (not b369)  (not b582) )
  :assumption
(or (not b375)  (not b587) )
  :assumption
(or (not b381)  (not b592) )
  :assumption
(or (not b387)  (not b597) )
  :assumption
(or (not b363)  (not b400) )
  :assumption
(or (not b369)  (not b405) )
  :assumption
(or (not b375)  (not b410) )
  :assumption
(or (not b381)  (not b415) )
  :assumption
(or (not b387)  (not b420) )
  :assumption
(or (not b271)  (not b369) )
  :assumption
(or (not b274)  (not b375) )
  :assumption
(or (not b277)  (not b381) )
  :assumption
(or (not b280)  (not b387) )
  :assumption
(or (not b235)  (not b369) )
  :assumption
(or (not b238)  (not b375) )
  :assumption
(or (not b241)  (not b381) )
  :assumption
(or (not b244)  (not b387) )
  :assumption
(or (not b198)  (not b369) )
  :assumption
(or (not b202)  (not b375) )
  :assumption
(or (not b205)  (not b381) )
  :assumption
(or (not b208)  (not b387) )
  :assumption
(or (not b161)  (not b375) )
  :assumption
(or (not b166)  (not b381) )
  :assumption
(or (not b170)  (not b387) )
  :assumption
(or (not b113)  (not b375) )
  :assumption
(or (not b118)  (not b381) )
  :assumption
(or (not b122)  (not b387) )
  :assumption
(or (not b56)  (not b375) )
  :assumption
(or (not b62)  (not b381) )
  :assumption
(or (not b67)  (not b387) )
  :assumption
(or (not b363)  (not b633) )
  :assumption
(or (not b369)  (not b636) )
  :assumption
(or (not b375)  (not b639) )
  :assumption
(or (not b381)  (not b642) )
  :assumption
(or (not b387)  (not b645) )
  :assumption
(or (not b363)  (not b487) )
  :assumption
(or (not b369)  (not b493) )
  :assumption
(or (not b375)  (not b499) )
  :assumption
(or (not b381)  (not b505) )
  :assumption
(or (not b393)  (not b653) )
  :assumption
(or (not b400)  (not b656) )
  :assumption
(or (not b405)  (not b657) )
  :assumption
(or (not b410)  (not b658) )
  :assumption
(or (not b415)  (not b659) )
  :assumption
(or (not b420)  (not b660) )
  :assumption
(or (not b393)  (not b603) )
  :assumption
(or (not b400)  (not b609) )
  :assumption
(or (not b405)  (not b614) )
  :assumption
(or (not b410)  (not b619) )
  :assumption
(or (not b415)  (not b624) )
  :assumption
(or (not b420)  (not b629) )
  :assumption
(or (not b393)  (not b570) )
  :assumption
(or (not b400)  (not b577) )
  :assumption
(or (not b405)  (not b582) )
  :assumption
(or (not b410)  (not b587) )
  :assumption
(or (not b415)  (not b592) )
  :assumption
(or (not b420)  (not b597) )
  :assumption
(or (not b393)  (not b426) )
  :assumption
(or (not b400)  (not b432) )
  :assumption
(or (not b405)  (not b437) )
  :assumption
(or (not b410)  (not b442) )
  :assumption
(or (not b415)  (not b447) )
  :assumption
(or (not b420)  (not b452) )
  :assumption
(or (not b271)  (not b405) )
  :assumption
(or (not b274)  (not b410) )
  :assumption
(or (not b277)  (not b415) )
  :assumption
(or (not b280)  (not b420) )
  :assumption
(or (not b235)  (not b405) )
  :assumption
(or (not b238)  (not b410) )
  :assumption
(or (not b241)  (not b415) )
  :assumption
(or (not b244)  (not b420) )
  :assumption
(or (not b198)  (not b405) )
  :assumption
(or (not b202)  (not b410) )
  :assumption
(or (not b205)  (not b415) )
  :assumption
(or (not b208)  (not b420) )
  :assumption
(or (not b161)  (not b410) )
  :assumption
(or (not b166)  (not b415) )
  :assumption
(or (not b170)  (not b420) )
  :assumption
(or (not b113)  (not b410) )
  :assumption
(or (not b118)  (not b415) )
  :assumption
(or (not b122)  (not b420) )
  :assumption
(or (not b56)  (not b410) )
  :assumption
(or (not b62)  (not b415) )
  :assumption
(or (not b67)  (not b420) )
  :assumption
(or (not b400)  (not b540) )
  :assumption
(or (not b405)  (not b546) )
  :assumption
(or (not b410)  (not b552) )
  :assumption
(or (not b415)  (not b558) )
  :assumption
(or (not b420)  (not b564) )
  :assumption
(or (not b400)  (not b487) )
  :assumption
(or (not b405)  (not b493) )
  :assumption
(or (not b410)  (not b499) )
  :assumption
(or (not b415)  (not b505) )
  :assumption
(or (not b400)  (not b633) )
  :assumption
(or (not b405)  (not b636) )
  :assumption
(or (not b410)  (not b639) )
  :assumption
(or (not b415)  (not b642) )
  :assumption
(or (not b420)  (not b645) )
  :assumption
(or (not b400)  (not b457) )
  :assumption
(or (not b405)  (not b464) )
  :assumption
(or (not b410)  (not b471) )
  :assumption
(or (not b415)  (not b478) )
  :assumption
(or (not b247)  (not b405) )
  :assumption
(or (not b250)  (not b410) )
  :assumption
(or (not b253)  (not b415) )
  :assumption
(or (not b256)  (not b420) )
  :assumption
(or (not b211)  (not b405) )
  :assumption
(or (not b214)  (not b410) )
  :assumption
(or (not b217)  (not b415) )
  :assumption
(or (not b220)  (not b420) )
  :assumption
(or (not b174)  (not b405) )
  :assumption
(or (not b177)  (not b410) )
  :assumption
(or (not b180)  (not b415) )
  :assumption
(or (not b183)  (not b420) )
  :assumption
(or (not b126)  (not b400) )
  :assumption
(or (not b131)  (not b405) )
  :assumption
(or (not b136)  (not b410) )
  :assumption
(or (not b141)  (not b415) )
  :assumption
(or (not b146)  (not b420) )
  :assumption
(or (not b72)  (not b410) )
  :assumption
(or (not b78)  (not b415) )
  :assumption
(or (not b83)  (not b420) )
  :assumption
(or (not b14)  (not b400) )
  :assumption
(or (not b20)  (not b405) )
  :assumption
(or (not b26)  (not b410) )
  :assumption
(or (not b32)  (not b415) )
  :assumption
(or (not b400)  (not b648) )
  :assumption
(or (not b405)  (not b649) )
  :assumption
(or (not b410)  (not b650) )
  :assumption
(or (not b415)  (not b651) )
  :assumption
(or (not b420)  (not b652) )
  :assumption
(or (not b400)  (not b513) )
  :assumption
(or (not b405)  (not b518) )
  :assumption
(or (not b410)  (not b523) )
  :assumption
(or (not b415)  (not b528) )
  :assumption
(or (not b420)  (not b533) )
  :assumption
(or (not b426)  (not b653) )
  :assumption
(or (not b432)  (not b656) )
  :assumption
(or (not b437)  (not b657) )
  :assumption
(or (not b442)  (not b658) )
  :assumption
(or (not b447)  (not b659) )
  :assumption
(or (not b452)  (not b660) )
  :assumption
(or (not b426)  (not b603) )
  :assumption
(or (not b432)  (not b609) )
  :assumption
(or (not b437)  (not b614) )
  :assumption
(or (not b442)  (not b619) )
  :assumption
(or (not b447)  (not b624) )
  :assumption
(or (not b452)  (not b629) )
  :assumption
(or (not b426)  (not b570) )
  :assumption
(or (not b432)  (not b577) )
  :assumption
(or (not b437)  (not b582) )
  :assumption
(or (not b442)  (not b587) )
  :assumption
(or (not b447)  (not b592) )
  :assumption
(or (not b452)  (not b597) )
  :assumption
(or (not b271)  (not b437) )
  :assumption
(or (not b274)  (not b442) )
  :assumption
(or (not b277)  (not b447) )
  :assumption
(or (not b280)  (not b452) )
  :assumption
(or (not b235)  (not b437) )
  :assumption
(or (not b238)  (not b442) )
  :assumption
(or (not b241)  (not b447) )
  :assumption
(or (not b244)  (not b452) )
  :assumption
(or (not b198)  (not b437) )
  :assumption
(or (not b202)  (not b442) )
  :assumption
(or (not b205)  (not b447) )
  :assumption
(or (not b208)  (not b452) )
  :assumption
(or (not b161)  (not b442) )
  :assumption
(or (not b166)  (not b447) )
  :assumption
(or (not b170)  (not b452) )
  :assumption
(or (not b113)  (not b442) )
  :assumption
(or (not b118)  (not b447) )
  :assumption
(or (not b122)  (not b452) )
  :assumption
(or (not b56)  (not b442) )
  :assumption
(or (not b62)  (not b447) )
  :assumption
(or (not b67)  (not b452) )
  :assumption
(or (not b432)  (not b540) )
  :assumption
(or (not b437)  (not b546) )
  :assumption
(or (not b442)  (not b552) )
  :assumption
(or (not b447)  (not b558) )
  :assumption
(or (not b452)  (not b564) )
  :assumption
(or (not b432)  (not b487) )
  :assumption
(or (not b437)  (not b493) )
  :assumption
(or (not b442)  (not b499) )
  :assumption
(or (not b447)  (not b505) )
  :assumption
(or (not b432)  (not b648) )
  :assumption
(or (not b437)  (not b649) )
  :assumption
(or (not b442)  (not b650) )
  :assumption
(or (not b447)  (not b651) )
  :assumption
(or (not b452)  (not b652) )
  :assumption
(or (not b432)  (not b513) )
  :assumption
(or (not b437)  (not b518) )
  :assumption
(or (not b442)  (not b523) )
  :assumption
(or (not b447)  (not b528) )
  :assumption
(or (not b452)  (not b533) )
  :assumption
(or (not b259)  (not b437) )
  :assumption
(or (not b262)  (not b442) )
  :assumption
(or (not b265)  (not b447) )
  :assumption
(or (not b268)  (not b452) )
  :assumption
(or (not b223)  (not b437) )
  :assumption
(or (not b226)  (not b442) )
  :assumption
(or (not b229)  (not b447) )
  :assumption
(or (not b232)  (not b452) )
  :assumption
(or (not b186)  (not b437) )
  :assumption
(or (not b189)  (not b442) )
  :assumption
(or (not b192)  (not b447) )
  :assumption
(or (not b195)  (not b452) )
  :assumption
(or (not b151)  (not b442) )
  :assumption
(or (not b156)  (not b447) )
  :assumption
(or (not b89)  (not b432) )
  :assumption
(or (not b95)  (not b437) )
  :assumption
(or (not b101)  (not b442) )
  :assumption
(or (not b105)  (not b447) )
  :assumption
(or (not b109)  (not b452) )
  :assumption
(or (not b40)  (not b442) )
  :assumption
(or (not b46)  (not b447) )
  :assumption
(or (not b51)  (not b452) )
  :assumption
(or (not b432)  (not b633) )
  :assumption
(or (not b437)  (not b636) )
  :assumption
(or (not b442)  (not b639) )
  :assumption
(or (not b447)  (not b642) )
  :assumption
(or (not b452)  (not b645) )
  :assumption
(or (not b432)  (not b457) )
  :assumption
(or (not b437)  (not b464) )
  :assumption
(or (not b442)  (not b471) )
  :assumption
(or (not b447)  (not b478) )
  :assumption
(or (not b457)  (not b633) )
  :assumption
(or (not b464)  (not b636) )
  :assumption
(or (not b471)  (not b639) )
  :assumption
(or (not b478)  (not b642) )
  :assumption
(or (not b457)  (not b487) )
  :assumption
(or (not b464)  (not b493) )
  :assumption
(or (not b471)  (not b499) )
  :assumption
(or (not b478)  (not b505) )
  :assumption
(or (not b457)  (not b577) )
  :assumption
(or (not b464)  (not b582) )
  :assumption
(or (not b471)  (not b587) )
  :assumption
(or (not b478)  (not b592) )
  :assumption
(or (not b457)  (not b513) )
  :assumption
(or (not b464)  (not b518) )
  :assumption
(or (not b471)  (not b523) )
  :assumption
(or (not b478)  (not b528) )
  :assumption
(or (not b457)  (not b648) )
  :assumption
(or (not b464)  (not b649) )
  :assumption
(or (not b471)  (not b650) )
  :assumption
(or (not b478)  (not b651) )
  :assumption
(or (not b457)  (not b540) )
  :assumption
(or (not b464)  (not b546) )
  :assumption
(or (not b471)  (not b552) )
  :assumption
(or (not b478)  (not b558) )
  :assumption
(or (not b457)  (not b656) )
  :assumption
(or (not b464)  (not b657) )
  :assumption
(or (not b471)  (not b658) )
  :assumption
(or (not b478)  (not b659) )
  :assumption
(or (not b457)  (not b609) )
  :assumption
(or (not b464)  (not b614) )
  :assumption
(or (not b471)  (not b619) )
  :assumption
(or (not b478)  (not b624) )
  :assumption
(or (not b487)  (not b633) )
  :assumption
(or (not b493)  (not b636) )
  :assumption
(or (not b499)  (not b639) )
  :assumption
(or (not b505)  (not b642) )
  :assumption
(or (not b487)  (not b577) )
  :assumption
(or (not b493)  (not b582) )
  :assumption
(or (not b499)  (not b587) )
  :assumption
(or (not b505)  (not b592) )
  :assumption
(or (not b487)  (not b513) )
  :assumption
(or (not b493)  (not b518) )
  :assumption
(or (not b499)  (not b523) )
  :assumption
(or (not b505)  (not b528) )
  :assumption
(or (not b487)  (not b656) )
  :assumption
(or (not b493)  (not b657) )
  :assumption
(or (not b499)  (not b658) )
  :assumption
(or (not b505)  (not b659) )
  :assumption
(or (not b487)  (not b609) )
  :assumption
(or (not b493)  (not b614) )
  :assumption
(or (not b499)  (not b619) )
  :assumption
(or (not b505)  (not b624) )
  :assumption
(or (not b487)  (not b648) )
  :assumption
(or (not b493)  (not b649) )
  :assumption
(or (not b499)  (not b650) )
  :assumption
(or (not b505)  (not b651) )
  :assumption
(or (not b487)  (not b540) )
  :assumption
(or (not b493)  (not b546) )
  :assumption
(or (not b499)  (not b552) )
  :assumption
(or (not b505)  (not b558) )
  :assumption
(or (not b513)  (not b648) )
  :assumption
(or (not b518)  (not b649) )
  :assumption
(or (not b523)  (not b650) )
  :assumption
(or (not b528)  (not b651) )
  :assumption
(or (not b533)  (not b652) )
  :assumption
(or (not b513)  (not b540) )
  :assumption
(or (not b518)  (not b546) )
  :assumption
(or (not b523)  (not b552) )
  :assumption
(or (not b528)  (not b558) )
  :assumption
(or (not b533)  (not b564) )
  :assumption
(or (not b513)  (not b609) )
  :assumption
(or (not b518)  (not b614) )
  :assumption
(or (not b523)  (not b619) )
  :assumption
(or (not b528)  (not b624) )
  :assumption
(or (not b533)  (not b629) )
  :assumption
(or (not b513)  (not b633) )
  :assumption
(or (not b518)  (not b636) )
  :assumption
(or (not b523)  (not b639) )
  :assumption
(or (not b528)  (not b642) )
  :assumption
(or (not b533)  (not b645) )
  :assumption
(or (not b513)  (not b656) )
  :assumption
(or (not b518)  (not b657) )
  :assumption
(or (not b523)  (not b658) )
  :assumption
(or (not b528)  (not b659) )
  :assumption
(or (not b533)  (not b660) )
  :assumption
(or (not b513)  (not b577) )
  :assumption
(or (not b518)  (not b582) )
  :assumption
(or (not b523)  (not b587) )
  :assumption
(or (not b528)  (not b592) )
  :assumption
(or (not b533)  (not b597) )
  :assumption
(or (not b540)  (not b648) )
  :assumption
(or (not b546)  (not b649) )
  :assumption
(or (not b552)  (not b650) )
  :assumption
(or (not b558)  (not b651) )
  :assumption
(or (not b564)  (not b652) )
  :assumption
(or (not b540)  (not b609) )
  :assumption
(or (not b546)  (not b614) )
  :assumption
(or (not b552)  (not b619) )
  :assumption
(or (not b558)  (not b624) )
  :assumption
(or (not b564)  (not b629) )
  :assumption
(or (not b540)  (not b656) )
  :assumption
(or (not b546)  (not b657) )
  :assumption
(or (not b552)  (not b658) )
  :assumption
(or (not b558)  (not b659) )
  :assumption
(or (not b564)  (not b660) )
  :assumption
(or (not b540)  (not b577) )
  :assumption
(or (not b546)  (not b582) )
  :assumption
(or (not b552)  (not b587) )
  :assumption
(or (not b558)  (not b592) )
  :assumption
(or (not b564)  (not b597) )
  :assumption
(or (not b540)  (not b633) )
  :assumption
(or (not b546)  (not b636) )
  :assumption
(or (not b552)  (not b639) )
  :assumption
(or (not b558)  (not b642) )
  :assumption
(or (not b564)  (not b645) )
  :assumption
(or (not b570)  (not b653) )
  :assumption
(or (not b577)  (not b656) )
  :assumption
(or (not b582)  (not b657) )
  :assumption
(or (not b587)  (not b658) )
  :assumption
(or (not b592)  (not b659) )
  :assumption
(or (not b597)  (not b660) )
  :assumption
(or (not b570)  (not b603) )
  :assumption
(or (not b577)  (not b609) )
  :assumption
(or (not b582)  (not b614) )
  :assumption
(or (not b587)  (not b619) )
  :assumption
(or (not b592)  (not b624) )
  :assumption
(or (not b597)  (not b629) )
  :assumption
(or (not b577)  (not b633) )
  :assumption
(or (not b582)  (not b636) )
  :assumption
(or (not b587)  (not b639) )
  :assumption
(or (not b592)  (not b642) )
  :assumption
(or (not b597)  (not b645) )
  :assumption
(or (not b577)  (not b648) )
  :assumption
(or (not b582)  (not b649) )
  :assumption
(or (not b587)  (not b650) )
  :assumption
(or (not b592)  (not b651) )
  :assumption
(or (not b597)  (not b652) )
  :assumption
(or (not b603)  (not b653) )
  :assumption
(or (not b609)  (not b656) )
  :assumption
(or (not b614)  (not b657) )
  :assumption
(or (not b619)  (not b658) )
  :assumption
(or (not b624)  (not b659) )
  :assumption
(or (not b629)  (not b660) )
  :assumption
(or (not b609)  (not b648) )
  :assumption
(or (not b614)  (not b649) )
  :assumption
(or (not b619)  (not b650) )
  :assumption
(or (not b624)  (not b651) )
  :assumption
(or (not b629)  (not b652) )
  :assumption
(or (not b609)  (not b633) )
  :assumption
(or (not b614)  (not b636) )
  :assumption
(or (not b619)  (not b639) )
  :assumption
(or (not b624)  (not b642) )
  :assumption
(or (not b629)  (not b645) )
  :assumption
(or (not b633)  (not b656) )
  :assumption
(or (not b636)  (not b657) )
  :assumption
(or (not b639)  (not b658) )
  :assumption
(or (not b642)  (not b659) )
  :assumption
(or (not b645)  (not b660) )
  :assumption
(or (not b633)  (not b648) )
  :assumption
(or (not b636)  (not b649) )
  :assumption
(or (not b639)  (not b650) )
  :assumption
(or (not b642)  (not b651) )
  :assumption
(or (not b645)  (not b652) )
  :assumption
(or (not b648)  (not b656) )
  :assumption
(or (not b649)  (not b657) )
  :assumption
(or (not b650)  (not b658) )
  :assumption
(or (not b651)  (not b659) )
  :assumption
(or (not b652)  (not b660) )
  :assumption
(= r1 0)
  :assumption
(= r2 r3)
  :assumption
(= (- r4 r1) 1)
  :assumption
(= (- r5 r4) 1)
  :assumption
(= (- r6 r5) 1)
  :assumption
(= (- r7 r6) 1)
  :assumption
(= (- r8 r7) 1)
  :assumption
(= (- r3 r8) 1)
  :assumption
(= r9 0)
  :assumption
(= r10 0)
  :assumption
(= r11 1773)
  :assumption
(<= (+ (* 1 r2) (* 1 r12)) 6787)
  :assumption
(= r17 0)
  :assumption
(= r42 0)
  :assumption
(= r94 0)
  :assumption
(= r95 0)
  :assumption
(= r104 0)
  :assumption
(= r105 0)
  :assumption
(= r163 0)
  :assumption
(= r164 0)
  :assumption
(= r173 0)
  :assumption
(= r174 0)
  :assumption
(= (- r153 r10) 0)
  :assumption
(= (- (- (- (- r156 r153) r35) r27) r13) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r159 r156) r78) r74) r70) r66) r62) r58) r54) r50) r46) r36) r28) r14) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r162 r159) r79) r75) r71) r67) r63) r59) r55) r51) r47) r43) r40) r37) r32) r29) r24) r21) r18) r15) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r185 r162) r80) r76) r72) r68) r64) r60) r56) r52) r48) r44) r41) r38) r33) r30) r25) r22) r19) r16) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r222 r185) r81) r77) r73) r69) r65) r61) r57) r53) r49) r45) r42) r39) r34) r31) r26) r23) r20) r17) 0)
  :assumption
(= (- (- (- (- (- r223 r9) r208) r196) r139) r127) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r224 r223) r210) r198) r186) r175) r165) r151) r141) r129) r117) r106) r96) r82) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r225 r224) r212) r200) r188) r177) r167) r154) r143) r131) r119) r108) r98) r85) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r226 r225) r214) r202) r190) r179) r169) r157) r145) r133) r121) r110) r100) r88) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r227 r226) r216) r204) r192) r181) r171) r160) r147) r135) r123) r112) r102) r91) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- r12 r227) r218) r206) r194) r183) r173) r163) r149) r137) r125) r114) r104) r94) 0)
  :formula
(not false)
)