(benchmark p_driverlogNumeric_s7.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 ((b17))
  :extrapreds ((b20))
  :extrapreds ((b23))
  :extrapreds ((b26))
  :extrapreds ((b29))
  :extrapreds ((b33))
  :extrapreds ((b35))
  :extrapreds ((b37))
  :extrapreds ((b39))
  :extrapreds ((b41))
  :extrapreds ((b43))
  :extrapreds ((b46))
  :extrapreds ((b49))
  :extrapreds ((b52))
  :extrapreds ((b55))
  :extrapreds ((b58))
  :extrapreds ((b61))
  :extrapreds ((b65))
  :extrapreds ((b67))
  :extrapreds ((b69))
  :extrapreds ((b71))
  :extrapreds ((b73))
  :extrapreds ((b75))
  :extrapreds ((b78))
  :extrapreds ((b81))
  :extrapreds ((b84))
  :extrapreds ((b85))
  :extrapreds ((b86))
  :extrapreds ((b87))
  :extrapreds ((b88))
  :extrapreds ((b89))
  :extrapreds ((b91))
  :extrapreds ((b93))
  :extrapreds ((b95))
  :extrapreds ((b96))
  :extrapreds ((b97))
  :extrapreds ((b98))
  :extrapreds ((b99))
  :extrapreds ((b100))
  :extrapreds ((b102))
  :extrapreds ((b104))
  :extrapreds ((b106))
  :extrapreds ((b107))
  :extrapreds ((b108))
  :extrapreds ((b109))
  :extrapreds ((b110))
  :extrapreds ((b111))
  :extrapreds ((b112))
  :extrapreds ((b113))
  :extrapreds ((b114))
  :extrapreds ((b115))
  :extrapreds ((b116))
  :extrapreds ((b117))
  :extrapreds ((b118))
  :extrapreds ((b119))
  :extrapreds ((b120))
  :extrapreds ((b126))
  :extrapreds ((b129))
  :extrapreds ((b134))
  :extrapreds ((b137))
  :extrapreds ((b139))
  :extrapreds ((b143))
  :extrapreds ((b144))
  :extrapreds ((b147))
  :extrapreds ((b149))
  :extrapreds ((b150))
  :extrapreds ((b154))
  :extrapreds ((b158))
  :extrapreds ((b161))
  :extrapreds ((b163))
  :extrapreds ((b165))
  :extrapreds ((b167))
  :extrapreds ((b169))
  :extrapreds ((b170))
  :extrapreds ((b171))
  :extrapreds ((b172))
  :extrapreds ((b173))
  :extrapreds ((b174))
  :extrapreds ((b175))
  :extrapreds ((b176))
  :extrapreds ((b177))
  :extrapreds ((b178))
  :extrapreds ((b179))
  :extrapreds ((b180))
  :extrapreds ((b181))
  :extrapreds ((b182))
  :extrapreds ((b183))
  :extrapreds ((b184))
  :extrapreds ((b185))
  :extrapreds ((b187))
  :extrapreds ((b192))
  :extrapreds ((b195))
  :extrapreds ((b199))
  :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 ((b242))
  :extrapreds ((b245))
  :extrapreds ((b249))
  :extrapreds ((b256))
  :extrapreds ((b259))
  :extrapreds ((b262))
  :extrapreds ((b265))
  :extrapreds ((b268))
  :extrapreds ((b271))
  :extrapreds ((b274))
  :extrapreds ((b277))
  :extrapreds ((b280))
  :extrapreds ((b286))
  :extrapreds ((b291))
  :extrapreds ((b296))
  :extrapreds ((b301))
  :extrapreds ((b305))
  :extrapreds ((b309))
  :extrapreds ((b313))
  :extrapreds ((b317))
  :extrapreds ((b321))
  :extrapreds ((b325))
  :extrapreds ((b328))
  :extrapreds ((b331))
  :extrapreds ((b336))
  :extrapreds ((b340))
  :extrapreds ((b344))
  :extrapreds ((b348))
  :extrapreds ((b351))
  :extrapreds ((b354))
  :extrapreds ((b357))
  :extrapreds ((b360))
  :extrapreds ((b364))
  :extrapreds ((b367))
  :extrapreds ((b370))
  :extrapreds ((b373))
  :extrapreds ((b376))
  :extrapreds ((b379))
  :extrapreds ((b382))
  :extrapreds ((b385))
  :extrapreds ((b388))
  :extrapreds ((b391))
  :extrapreds ((b394))
  :extrapreds ((b397))
  :extrapreds ((b400))
  :extrapreds ((b403))
  :extrapreds ((b406))
  :extrapreds ((b409))
  :extrapreds ((b412))
  :extrapreds ((b415))
  :extrapreds ((b418))
  :extrapreds ((b421))
  :extrapreds ((b427))
  :extrapreds ((b432))
  :extrapreds ((b437))
  :extrapreds ((b442))
  :extrapreds ((b446))
  :extrapreds ((b450))
  :extrapreds ((b454))
  :extrapreds ((b458))
  :extrapreds ((b462))
  :extrapreds ((b466))
  :extrapreds ((b470))
  :extrapreds ((b473))
  :extrapreds ((b478))
  :extrapreds ((b482))
  :extrapreds ((b486))
  :extrapreds ((b490))
  :extrapreds ((b493))
  :extrapreds ((b496))
  :extrapreds ((b499))
  :extrapreds ((b502))
  :extrapreds ((b506))
  :extrapreds ((b509))
  :extrapreds ((b512))
  :extrapreds ((b515))
  :extrapreds ((b518))
  :extrapreds ((b521))
  :extrapreds ((b524))
  :extrapreds ((b527))
  :extrapreds ((b530))
  :extrapreds ((b533))
  :extrapreds ((b537))
  :extrapreds ((b540))
  :extrapreds ((b543))
  :extrapreds ((b546))
  :extrapreds ((b550))
  :extrapreds ((b553))
  :extrapreds ((b556))
  :extrapreds ((b15))
  :extrapreds ((b16))
  :extrapreds ((b18))
  :extrapreds ((b19))
  :extrapreds ((b21))
  :extrapreds ((b22))
  :extrapreds ((b24))
  :extrapreds ((b25))
  :extrapreds ((b27))
  :extrapreds ((b28))
  :extrapreds ((b30))
  :extrapreds ((b31))
  :extrapreds ((b32))
  :extrapreds ((b34))
  :extrapreds ((b36))
  :extrapreds ((b38))
  :extrapreds ((b40))
  :extrapreds ((b42))
  :extrapreds ((b44))
  :extrapreds ((b45))
  :extrapreds ((b47))
  :extrapreds ((b48))
  :extrapreds ((b50))
  :extrapreds ((b51))
  :extrapreds ((b53))
  :extrapreds ((b54))
  :extrapreds ((b56))
  :extrapreds ((b57))
  :extrapreds ((b59))
  :extrapreds ((b60))
  :extrapreds ((b62))
  :extrapreds ((b63))
  :extrapreds ((b64))
  :extrapreds ((b66))
  :extrapreds ((b68))
  :extrapreds ((b70))
  :extrapreds ((b72))
  :extrapreds ((b74))
  :extrapreds ((b76))
  :extrapreds ((b77))
  :extrapreds ((b79))
  :extrapreds ((b80))
  :extrapreds ((b82))
  :extrapreds ((b83))
  :extrapreds ((b90))
  :extrapreds ((b92))
  :extrapreds ((b94))
  :extrapreds ((b101))
  :extrapreds ((b103))
  :extrapreds ((b105))
  :extrapreds ((b121))
  :extrapreds ((b122))
  :extrapreds ((b123))
  :extrapreds ((b124))
  :extrapreds ((b125))
  :extrapreds ((b127))
  :extrapreds ((b128))
  :extrapreds ((b130))
  :extrapreds ((b131))
  :extrapreds ((b132))
  :extrapreds ((b133))
  :extrapreds ((b135))
  :extrapreds ((b136))
  :extrapreds ((b138))
  :extrapreds ((b140))
  :extrapreds ((b141))
  :extrapreds ((b142))
  :extrapreds ((b145))
  :extrapreds ((b146))
  :extrapreds ((b148))
  :extrapreds ((b151))
  :extrapreds ((b152))
  :extrapreds ((b153))
  :extrapreds ((b155))
  :extrapreds ((b156))
  :extrapreds ((b157))
  :extrapreds ((b159))
  :extrapreds ((b160))
  :extrapreds ((b162))
  :extrapreds ((b164))
  :extrapreds ((b166))
  :extrapreds ((b168))
  :extrapreds ((b189))
  :extrapreds ((b190))
  :extrapreds ((b197))
  :extrapreds ((b240))
  :extrapreds ((b247))
  :extrapreds ((b282))
  :extrapreds ((b283))
  :extrapreds ((b284))
  :extrapreds ((b288))
  :extrapreds ((b289))
  :extrapreds ((b293))
  :extrapreds ((b294))
  :extrapreds ((b298))
  :extrapreds ((b299))
  :extrapreds ((b303))
  :extrapreds ((b307))
  :extrapreds ((b311))
  :extrapreds ((b315))
  :extrapreds ((b319))
  :extrapreds ((b323))
  :extrapreds ((b333))
  :extrapreds ((b334))
  :extrapreds ((b338))
  :extrapreds ((b342))
  :extrapreds ((b346))
  :extrapreds ((b362))
  :extrapreds ((b423))
  :extrapreds ((b424))
  :extrapreds ((b425))
  :extrapreds ((b429))
  :extrapreds ((b430))
  :extrapreds ((b434))
  :extrapreds ((b435))
  :extrapreds ((b439))
  :extrapreds ((b440))
  :extrapreds ((b444))
  :extrapreds ((b448))
  :extrapreds ((b452))
  :extrapreds ((b456))
  :extrapreds ((b460))
  :extrapreds ((b464))
  :extrapreds ((b468))
  :extrapreds ((b475))
  :extrapreds ((b476))
  :extrapreds ((b480))
  :extrapreds ((b484))
  :extrapreds ((b488))
  :extrapreds ((b504))
  :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))
  :assumption
(or (not b14)  b15 )
  :assumption
(or (not b14)  (not b16) )
  :assumption
(or (not b17)  b18 )
  :assumption
(or (not b17)  (not b19) )
  :assumption
(or b16  (not b17) )
  :assumption
(or (not b20)  b21 )
  :assumption
(or (not b20)  (not b22) )
  :assumption
(or b19  (not b20) )
  :assumption
(or (not b23)  b24 )
  :assumption
(or (not b23)  (not b25) )
  :assumption
(or b22  (not b23) )
  :assumption
(or (not b26)  b27 )
  :assumption
(or (not b26)  (not b28) )
  :assumption
(or b25  (not b26) )
  :assumption
(or (not b29)  b30 )
  :assumption
(or (not b29)  (not b31) )
  :assumption
(or b28  (not b29) )
  :assumption
(or (not b33)  b34 )
  :assumption
(or (not b16)  (not b33) )
  :assumption
(or (not b35)  b36 )
  :assumption
(or (not b19)  (not b35) )
  :assumption
(or b16  (not b35) )
  :assumption
(or (not b37)  b38 )
  :assumption
(or (not b22)  (not b37) )
  :assumption
(or b19  (not b37) )
  :assumption
(or (not b39)  b40 )
  :assumption
(or (not b25)  (not b39) )
  :assumption
(or b22  (not b39) )
  :assumption
(or (not b41)  b42 )
  :assumption
(or (not b28)  (not b41) )
  :assumption
(or b25  (not b41) )
  :assumption
(or (not b43)  b44 )
  :assumption
(or (not b31)  (not b43) )
  :assumption
(or b28  (not b43) )
  :assumption
(or (not b46)  b47 )
  :assumption
(or (not b46)  (not b48) )
  :assumption
(or (not b49)  b50 )
  :assumption
(or (not b49)  (not b51) )
  :assumption
(or b48  (not b49) )
  :assumption
(or (not b52)  b53 )
  :assumption
(or (not b52)  (not b54) )
  :assumption
(or b51  (not b52) )
  :assumption
(or (not b55)  b56 )
  :assumption
(or (not b55)  (not b57) )
  :assumption
(or b54  (not b55) )
  :assumption
(or (not b58)  b59 )
  :assumption
(or (not b58)  (not b60) )
  :assumption
(or b57  (not b58) )
  :assumption
(or (not b61)  b62 )
  :assumption
(or (not b61)  (not b63) )
  :assumption
(or b60  (not b61) )
  :assumption
(or (not b65)  b66 )
  :assumption
(or (not b48)  (not b65) )
  :assumption
(or (not b67)  b68 )
  :assumption
(or (not b51)  (not b67) )
  :assumption
(or b48  (not b67) )
  :assumption
(or (not b69)  b70 )
  :assumption
(or (not b54)  (not b69) )
  :assumption
(or b51  (not b69) )
  :assumption
(or (not b71)  b72 )
  :assumption
(or (not b57)  (not b71) )
  :assumption
(or b54  (not b71) )
  :assumption
(or (not b73)  b74 )
  :assumption
(or (not b60)  (not b73) )
  :assumption
(or b57  (not b73) )
  :assumption
(or (not b75)  b76 )
  :assumption
(or (not b63)  (not b75) )
  :assumption
(or b60  (not b75) )
  :assumption
(or (not b78)  b79 )
  :assumption
(or (not b32)  (not b78) )
  :assumption
(or (not b78)  b80 )
  :assumption
(or b30  (not b78) )
  :assumption
(or (not b81)  b82 )
  :assumption
(or (not b32)  (not b81) )
  :assumption
(or (not b81)  b83 )
  :assumption
(or b30  (not b81) )
  :assumption
(or b19  (not b84) )
  :assumption
(or (not b18)  (not b84) )
  :assumption
(or b15  (not b84) )
  :assumption
(or b22  (not b85) )
  :assumption
(or (not b21)  (not b85) )
  :assumption
(or b18  (not b85) )
  :assumption
(or b25  (not b86) )
  :assumption
(or (not b24)  (not b86) )
  :assumption
(or b21  (not b86) )
  :assumption
(or b28  (not b87) )
  :assumption
(or (not b27)  (not b87) )
  :assumption
(or b24  (not b87) )
  :assumption
(or b31  (not b88) )
  :assumption
(or (not b30)  (not b88) )
  :assumption
(or b27  (not b88) )
  :assumption
(or (not b32)  (not b89) )
  :assumption
(or (not b89)  b90 )
  :assumption
(or b30  (not b89) )
  :assumption
(or b79  (not b91) )
  :assumption
(or (not b45)  (not b91) )
  :assumption
(or (not b91)  b92 )
  :assumption
(or b44  (not b91) )
  :assumption
(or b82  (not b93) )
  :assumption
(or (not b45)  (not b93) )
  :assumption
(or (not b93)  b94 )
  :assumption
(or b44  (not b93) )
  :assumption
(or b19  (not b95) )
  :assumption
(or (not b36)  (not b95) )
  :assumption
(or b34  (not b95) )
  :assumption
(or b22  (not b96) )
  :assumption
(or (not b38)  (not b96) )
  :assumption
(or b36  (not b96) )
  :assumption
(or b25  (not b97) )
  :assumption
(or (not b40)  (not b97) )
  :assumption
(or b38  (not b97) )
  :assumption
(or b28  (not b98) )
  :assumption
(or (not b42)  (not b98) )
  :assumption
(or b40  (not b98) )
  :assumption
(or b31  (not b99) )
  :assumption
(or (not b44)  (not b99) )
  :assumption
(or b42  (not b99) )
  :assumption
(or (not b45)  (not b100) )
  :assumption
(or (not b100)  b101 )
  :assumption
(or b44  (not b100) )
  :assumption
(or (not b102)  b103 )
  :assumption
(or (not b64)  (not b102) )
  :assumption
(or b80  (not b102) )
  :assumption
(or b62  (not b102) )
  :assumption
(or (not b104)  b105 )
  :assumption
(or (not b64)  (not b104) )
  :assumption
(or b83  (not b104) )
  :assumption
(or b62  (not b104) )
  :assumption
(or b51  (not b106) )
  :assumption
(or (not b50)  (not b106) )
  :assumption
(or b47  (not b106) )
  :assumption
(or b54  (not b107) )
  :assumption
(or (not b53)  (not b107) )
  :assumption
(or b50  (not b107) )
  :assumption
(or b57  (not b108) )
  :assumption
(or (not b56)  (not b108) )
  :assumption
(or b53  (not b108) )
  :assumption
(or b60  (not b109) )
  :assumption
(or (not b59)  (not b109) )
  :assumption
(or b56  (not b109) )
  :assumption
(or b63  (not b110) )
  :assumption
(or (not b62)  (not b110) )
  :assumption
(or b59  (not b110) )
  :assumption
(or (not b64)  (not b111) )
  :assumption
(or b90  (not b111) )
  :assumption
(or b62  (not b111) )
  :assumption
(or b103  (not b112) )
  :assumption
(or (not b77)  (not b112) )
  :assumption
(or b92  (not b112) )
  :assumption
(or b76  (not b112) )
  :assumption
(or b105  (not b113) )
  :assumption
(or (not b77)  (not b113) )
  :assumption
(or b94  (not b113) )
  :assumption
(or b76  (not b113) )
  :assumption
(or b51  (not b114) )
  :assumption
(or (not b68)  (not b114) )
  :assumption
(or b66  (not b114) )
  :assumption
(or b54  (not b115) )
  :assumption
(or (not b70)  (not b115) )
  :assumption
(or b68  (not b115) )
  :assumption
(or b57  (not b116) )
  :assumption
(or (not b72)  (not b116) )
  :assumption
(or b70  (not b116) )
  :assumption
(or b60  (not b117) )
  :assumption
(or (not b74)  (not b117) )
  :assumption
(or b72  (not b117) )
  :assumption
(or b63  (not b118) )
  :assumption
(or (not b76)  (not b118) )
  :assumption
(or b74  (not b118) )
  :assumption
(or (not b77)  (not b119) )
  :assumption
(or b101  (not b119) )
  :assumption
(or b76  (not b119) )
  :assumption
(or (not b120)  (not b121) )
  :assumption
(or (not b120)  b122 )
  :assumption
(or (not b120)  (not b123) )
  :assumption
(or b80  (not b120) )
  :assumption
(or (not b120)  b124 )
  :assumption
(or (not b120)  b125 )
  :assumption
(or (not b121)  (not b126) )
  :assumption
(or b122  (not b126) )
  :assumption
(or (not b126)  (not b127) )
  :assumption
(or b83  (not b126) )
  :assumption
(or (not b126)  b128 )
  :assumption
(or b125  (not b126) )
  :assumption
(or (not b129)  (not b130) )
  :assumption
(or (not b129)  b131 )
  :assumption
(or (not b129)  (not b132) )
  :assumption
(or (not b129)  b133 )
  :assumption
(or (not b125)  (not b134) )
  :assumption
(or (not b134)  b135 )
  :assumption
(or (not b134)  (not b136) )
  :assumption
(or b132  (not b134) )
  :assumption
(or b130  (not b134) )
  :assumption
(or (not b121)  (not b137) )
  :assumption
(or b122  (not b137) )
  :assumption
(or (not b137)  (not b138) )
  :assumption
(or b90  (not b137) )
  :assumption
(or b136  (not b137) )
  :assumption
(or b125  (not b137) )
  :assumption
(or (not b139)  (not b140) )
  :assumption
(or (not b139)  b141 )
  :assumption
(or (not b123)  (not b139) )
  :assumption
(or b92  (not b139) )
  :assumption
(or b124  (not b139) )
  :assumption
(or (not b139)  b142 )
  :assumption
(or (not b140)  (not b143) )
  :assumption
(or b141  (not b143) )
  :assumption
(or (not b127)  (not b143) )
  :assumption
(or b94  (not b143) )
  :assumption
(or b128  (not b143) )
  :assumption
(or b142  (not b143) )
  :assumption
(or (not b144)  (not b145) )
  :assumption
(or (not b144)  b146 )
  :assumption
(or (not b132)  (not b144) )
  :assumption
(or b133  (not b144) )
  :assumption
(or (not b142)  (not b147) )
  :assumption
(or (not b147)  b148 )
  :assumption
(or (not b136)  (not b147) )
  :assumption
(or b132  (not b147) )
  :assumption
(or b145  (not b147) )
  :assumption
(or (not b140)  (not b149) )
  :assumption
(or b141  (not b149) )
  :assumption
(or (not b138)  (not b149) )
  :assumption
(or b101  (not b149) )
  :assumption
(or b136  (not b149) )
  :assumption
(or b142  (not b149) )
  :assumption
(or (not b121)  (not b150) )
  :assumption
(or (not b150)  b151 )
  :assumption
(or (not b150)  (not b152) )
  :assumption
(or b80  (not b150) )
  :assumption
(or (not b150)  b153 )
  :assumption
(or b125  (not b150) )
  :assumption
(or (not b130)  (not b154) )
  :assumption
(or (not b154)  b155 )
  :assumption
(or (not b154)  (not b156) )
  :assumption
(or (not b154)  b157 )
  :assumption
(or (not b125)  (not b158) )
  :assumption
(or (not b158)  b159 )
  :assumption
(or (not b158)  (not b160) )
  :assumption
(or b156  (not b158) )
  :assumption
(or b130  (not b158) )
  :assumption
(or (not b121)  (not b161) )
  :assumption
(or b151  (not b161) )
  :assumption
(or (not b161)  (not b162) )
  :assumption
(or b90  (not b161) )
  :assumption
(or b160  (not b161) )
  :assumption
(or b125  (not b161) )
  :assumption
(or (not b140)  (not b163) )
  :assumption
(or (not b163)  b164 )
  :assumption
(or (not b152)  (not b163) )
  :assumption
(or b92  (not b163) )
  :assumption
(or b153  (not b163) )
  :assumption
(or b142  (not b163) )
  :assumption
(or (not b145)  (not b165) )
  :assumption
(or (not b165)  b166 )
  :assumption
(or (not b156)  (not b165) )
  :assumption
(or b157  (not b165) )
  :assumption
(or (not b142)  (not b167) )
  :assumption
(or (not b167)  b168 )
  :assumption
(or (not b160)  (not b167) )
  :assumption
(or b156  (not b167) )
  :assumption
(or b145  (not b167) )
  :assumption
(or (not b140)  (not b169) )
  :assumption
(or b164  (not b169) )
  :assumption
(or (not b162)  (not b169) )
  :assumption
(or b101  (not b169) )
  :assumption
(or b160  (not b169) )
  :assumption
(or b142  (not b169) )
  :assumption
(or b121  (not b170) )
  :assumption
(or b123  (not b170) )
  :assumption
(or (not b122)  (not b170) )
  :assumption
(or b80  (not b170) )
  :assumption
(or b135  (not b170) )
  :assumption
(or b121  (not b171) )
  :assumption
(or b127  (not b171) )
  :assumption
(or (not b122)  (not b171) )
  :assumption
(or b83  (not b171) )
  :assumption
(or b135  (not b171) )
  :assumption
(or b125  (not b172) )
  :assumption
(or b136  (not b172) )
  :assumption
(or (not b135)  (not b172) )
  :assumption
(or b131  (not b172) )
  :assumption
(or b121  (not b173) )
  :assumption
(or b138  (not b173) )
  :assumption
(or (not b122)  (not b173) )
  :assumption
(or b90  (not b173) )
  :assumption
(or b135  (not b173) )
  :assumption
(or b140  (not b174) )
  :assumption
(or b123  (not b174) )
  :assumption
(or (not b141)  (not b174) )
  :assumption
(or b92  (not b174) )
  :assumption
(or b148  (not b174) )
  :assumption
(or b140  (not b175) )
  :assumption
(or b127  (not b175) )
  :assumption
(or (not b141)  (not b175) )
  :assumption
(or b94  (not b175) )
  :assumption
(or b148  (not b175) )
  :assumption
(or b142  (not b176) )
  :assumption
(or b136  (not b176) )
  :assumption
(or (not b148)  (not b176) )
  :assumption
(or b146  (not b176) )
  :assumption
(or b140  (not b177) )
  :assumption
(or b138  (not b177) )
  :assumption
(or (not b141)  (not b177) )
  :assumption
(or b101  (not b177) )
  :assumption
(or b148  (not b177) )
  :assumption
(or b121  (not b178) )
  :assumption
(or b152  (not b178) )
  :assumption
(or (not b151)  (not b178) )
  :assumption
(or b80  (not b178) )
  :assumption
(or b159  (not b178) )
  :assumption
(or b121  (not b179) )
  :assumption
(or (not b151)  (not b179) )
  :assumption
(or b83  (not b179) )
  :assumption
(or b159  (not b179) )
  :assumption
(or b125  (not b180) )
  :assumption
(or b160  (not b180) )
  :assumption
(or (not b159)  (not b180) )
  :assumption
(or b155  (not b180) )
  :assumption
(or b121  (not b181) )
  :assumption
(or b162  (not b181) )
  :assumption
(or (not b151)  (not b181) )
  :assumption
(or b90  (not b181) )
  :assumption
(or b159  (not b181) )
  :assumption
(or b140  (not b182) )
  :assumption
(or b152  (not b182) )
  :assumption
(or (not b164)  (not b182) )
  :assumption
(or b92  (not b182) )
  :assumption
(or b168  (not b182) )
  :assumption
(or b140  (not b183) )
  :assumption
(or (not b164)  (not b183) )
  :assumption
(or b94  (not b183) )
  :assumption
(or b168  (not b183) )
  :assumption
(or b142  (not b184) )
  :assumption
(or b160  (not b184) )
  :assumption
(or (not b168)  (not b184) )
  :assumption
(or b166  (not b184) )
  :assumption
(or b140  (not b185) )
  :assumption
(or b162  (not b185) )
  :assumption
(or (not b164)  (not b185) )
  :assumption
(or b101  (not b185) )
  :assumption
(or b168  (not b185) )
  :assumption
(or (= r138 0)  b187 )
  :assumption
(or (not b187)  (= r138 24) )
  :assumption
(or (not b187)  b189 )
  :assumption
(or (not b187)  (not b190) )
  :assumption
(or b80  (not b187) )
  :assumption
(or b135  (not b187) )
  :assumption
(or (= r137 0)  b192 )
  :assumption
(or (not b192)  (= r137 24) )
  :assumption
(or b189  (not b192) )
  :assumption
(or (not b190)  (not b192) )
  :assumption
(or b80  (not b192) )
  :assumption
(or b159  (not b192) )
  :assumption
(or (= r136 0)  b195 )
  :assumption
(or (not b195)  (= r136 47) )
  :assumption
(or (not b195)  b197 )
  :assumption
(or (not b190)  (not b195) )
  :assumption
(or b80  (not b195) )
  :assumption
(or b135  (not b195) )
  :assumption
(or (= r135 0)  b199 )
  :assumption
(or (not b199)  (= r135 47) )
  :assumption
(or b197  (not b199) )
  :assumption
(or (not b190)  (not b199) )
  :assumption
(or b80  (not b199) )
  :assumption
(or b159  (not b199) )
  :assumption
(or (= r134 0)  b202 )
  :assumption
(or (not b202)  (= r134 24) )
  :assumption
(or b190  (not b202) )
  :assumption
(or (not b189)  (not b202) )
  :assumption
(or b83  (not b202) )
  :assumption
(or b135  (not b202) )
  :assumption
(or (= r133 0)  b205 )
  :assumption
(or (not b205)  (= r133 24) )
  :assumption
(or b190  (not b205) )
  :assumption
(or (not b189)  (not b205) )
  :assumption
(or b83  (not b205) )
  :assumption
(or b159  (not b205) )
  :assumption
(or (= r132 0)  b208 )
  :assumption
(or (not b208)  (= r132 70) )
  :assumption
(or b197  (not b208) )
  :assumption
(or (not b189)  (not b208) )
  :assumption
(or b83  (not b208) )
  :assumption
(or b135  (not b208) )
  :assumption
(or (= r131 0)  b211 )
  :assumption
(or (not b211)  (= r131 70) )
  :assumption
(or b197  (not b211) )
  :assumption
(or (not b189)  (not b211) )
  :assumption
(or b83  (not b211) )
  :assumption
(or b159  (not b211) )
  :assumption
(or (= r114 0)  b214 )
  :assumption
(or (not b214)  (= r114 47) )
  :assumption
(or b80  (not b214) )
  :assumption
(or (not b90)  (not b214) )
  :assumption
(or b131  (not b214) )
  :assumption
(or (= r130 0)  b217 )
  :assumption
(or (not b217)  (= r130 47) )
  :assumption
(or b190  (not b217) )
  :assumption
(or (not b197)  (not b217) )
  :assumption
(or b90  (not b217) )
  :assumption
(or b135  (not b217) )
  :assumption
(or (= r113 0)  b220 )
  :assumption
(or (not b220)  (= r113 47) )
  :assumption
(or b80  (not b220) )
  :assumption
(or (not b90)  (not b220) )
  :assumption
(or b155  (not b220) )
  :assumption
(or (= r129 0)  b223 )
  :assumption
(or (not b223)  (= r129 47) )
  :assumption
(or b190  (not b223) )
  :assumption
(or (not b197)  (not b223) )
  :assumption
(or b90  (not b223) )
  :assumption
(or b159  (not b223) )
  :assumption
(or (= r112 0)  b226 )
  :assumption
(or (not b226)  (= r112 70) )
  :assumption
(or b83  (not b226) )
  :assumption
(or (not b90)  (not b226) )
  :assumption
(or b131  (not b226) )
  :assumption
(or (= r128 0)  b229 )
  :assumption
(or (not b229)  (= r128 70) )
  :assumption
(or b189  (not b229) )
  :assumption
(or (not b197)  (not b229) )
  :assumption
(or b90  (not b229) )
  :assumption
(or b135  (not b229) )
  :assumption
(or (= r111 0)  b232 )
  :assumption
(or (not b232)  (= r111 70) )
  :assumption
(or b83  (not b232) )
  :assumption
(or (not b90)  (not b232) )
  :assumption
(or b155  (not b232) )
  :assumption
(or (= r127 0)  b235 )
  :assumption
(or (not b235)  (= r127 70) )
  :assumption
(or b189  (not b235) )
  :assumption
(or (not b197)  (not b235) )
  :assumption
(or b90  (not b235) )
  :assumption
(or b159  (not b235) )
  :assumption
(or (= r126 0)  b238 )
  :assumption
(or (not b238)  (= r126 24) )
  :assumption
(or (not b238)  (not b240) )
  :assumption
(or b92  (not b238) )
  :assumption
(or b148  (not b238) )
  :assumption
(or (= r125 0)  b242 )
  :assumption
(or (not b242)  (= r125 24) )
  :assumption
(or (not b240)  (not b242) )
  :assumption
(or b92  (not b242) )
  :assumption
(or b168  (not b242) )
  :assumption
(or (= r124 0)  b245 )
  :assumption
(or (not b245)  (= r124 47) )
  :assumption
(or (not b245)  b247 )
  :assumption
(or (not b240)  (not b245) )
  :assumption
(or b92  (not b245) )
  :assumption
(or b148  (not b245) )
  :assumption
(or (= r123 0)  b249 )
  :assumption
(or (not b249)  (= r123 47) )
  :assumption
(or b247  (not b249) )
  :assumption
(or (not b240)  (not b249) )
  :assumption
(or b92  (not b249) )
  :assumption
(or b168  (not b249) )
  :assumption
(or (= r110 0)  b256 )
  :assumption
(or (not b256)  (= r110 47) )
  :assumption
(or b92  (not b256) )
  :assumption
(or (not b101)  (not b256) )
  :assumption
(or b146  (not b256) )
  :assumption
(or (= r118 0)  b259 )
  :assumption
(or (not b259)  (= r118 47) )
  :assumption
(or b240  (not b259) )
  :assumption
(or (not b247)  (not b259) )
  :assumption
(or b101  (not b259) )
  :assumption
(or b148  (not b259) )
  :assumption
(or (= r109 0)  b262 )
  :assumption
(or (not b262)  (= r109 47) )
  :assumption
(or b92  (not b262) )
  :assumption
(or (not b101)  (not b262) )
  :assumption
(or b166  (not b262) )
  :assumption
(or (= r117 0)  b265 )
  :assumption
(or (not b265)  (= r117 47) )
  :assumption
(or b240  (not b265) )
  :assumption
(or (not b247)  (not b265) )
  :assumption
(or b101  (not b265) )
  :assumption
(or b168  (not b265) )
  :assumption
(or (= r108 0)  b268 )
  :assumption
(or (not b268)  (= r108 70) )
  :assumption
(or b94  (not b268) )
  :assumption
(or (not b101)  (not b268) )
  :assumption
(or b146  (not b268) )
  :assumption
(or (= r116 0)  b271 )
  :assumption
(or (not b271)  (= r116 70) )
  :assumption
(or (not b247)  (not b271) )
  :assumption
(or b101  (not b271) )
  :assumption
(or b148  (not b271) )
  :assumption
(or (= r107 0)  b274 )
  :assumption
(or (not b274)  (= r107 70) )
  :assumption
(or b94  (not b274) )
  :assumption
(or (not b101)  (not b274) )
  :assumption
(or b166  (not b274) )
  :assumption
(or (= r115 0)  b277 )
  :assumption
(or (not b277)  (= r115 70) )
  :assumption
(or (not b247)  (not b277) )
  :assumption
(or b101  (not b277) )
  :assumption
(or b168  (not b277) )
  :assumption
(or (= r70 0)  b280 )
  :assumption
(or (not b280)  (= r70 79) )
  :assumption
(or (not b280)  b282 )
  :assumption
(or (not b280)  (not b283) )
  :assumption
(or (not b280)  b284 )
  :assumption
(or (= r75 0)  b286 )
  :assumption
(or (not b286)  (= r75 79) )
  :assumption
(or (not b286)  b288 )
  :assumption
(or (not b286)  (not b289) )
  :assumption
(or b283  (not b286) )
  :assumption
(or (= r82 0)  b291 )
  :assumption
(or (not b291)  (= r82 79) )
  :assumption
(or (not b291)  b293 )
  :assumption
(or (not b291)  (not b294) )
  :assumption
(or b289  (not b291) )
  :assumption
(or (= r89 0)  b296 )
  :assumption
(or (not b296)  (= r89 79) )
  :assumption
(or (not b296)  b298 )
  :assumption
(or (not b296)  (not b299) )
  :assumption
(or b294  (not b296) )
  :assumption
(or (= r95 0)  b301 )
  :assumption
(or (not b301)  (= r95 79) )
  :assumption
(or b124  (not b301) )
  :assumption
(or (not b301)  (not b303) )
  :assumption
(or b299  (not b301) )
  :assumption
(or (= r100 0)  b305 )
  :assumption
(or (not b305)  (= r100 79) )
  :assumption
(or b123  (not b305) )
  :assumption
(or (not b305)  (not b307) )
  :assumption
(or b303  (not b305) )
  :assumption
(or (= r69 0)  b309 )
  :assumption
(or (not b309)  (= r69 29) )
  :assumption
(or (not b309)  b311 )
  :assumption
(or (not b283)  (not b309) )
  :assumption
(or b284  (not b309) )
  :assumption
(or (= r74 0)  b313 )
  :assumption
(or (not b313)  (= r74 29) )
  :assumption
(or (not b313)  b315 )
  :assumption
(or (not b289)  (not b313) )
  :assumption
(or b283  (not b313) )
  :assumption
(or (= r81 0)  b317 )
  :assumption
(or (not b317)  (= r81 29) )
  :assumption
(or (not b317)  b319 )
  :assumption
(or (not b294)  (not b317) )
  :assumption
(or b289  (not b317) )
  :assumption
(or (= r88 0)  b321 )
  :assumption
(or (not b321)  (= r88 29) )
  :assumption
(or (not b321)  b323 )
  :assumption
(or (not b299)  (not b321) )
  :assumption
(or b294  (not b321) )
  :assumption
(or (= r94 0)  b325 )
  :assumption
(or (not b325)  (= r94 29) )
  :assumption
(or b128  (not b325) )
  :assumption
(or (not b303)  (not b325) )
  :assumption
(or b299  (not b325) )
  :assumption
(or (= r99 0)  b328 )
  :assumption
(or (not b328)  (= r99 29) )
  :assumption
(or b127  (not b328) )
  :assumption
(or (not b307)  (not b328) )
  :assumption
(or b303  (not b328) )
  :assumption
(or (= r80 0)  b331 )
  :assumption
(or (not b331)  (= r80 43) )
  :assumption
(or b319  (not b331) )
  :assumption
(or (not b331)  (not b333) )
  :assumption
(or (not b331)  b334 )
  :assumption
(or (= r87 0)  b336 )
  :assumption
(or (not b336)  (= r87 43) )
  :assumption
(or b323  (not b336) )
  :assumption
(or (not b336)  (not b338) )
  :assumption
(or b333  (not b336) )
  :assumption
(or (= r93 0)  b340 )
  :assumption
(or (not b340)  (= r93 43) )
  :assumption
(or b128  (not b340) )
  :assumption
(or (not b340)  (not b342) )
  :assumption
(or b338  (not b340) )
  :assumption
(or (= r98 0)  b344 )
  :assumption
(or (not b344)  (= r98 43) )
  :assumption
(or b127  (not b344) )
  :assumption
(or (not b344)  (not b346) )
  :assumption
(or b342  (not b344) )
  :assumption
(or (= r79 0)  b348 )
  :assumption
(or (not b348)  (= r79 80) )
  :assumption
(or b133  (not b348) )
  :assumption
(or (not b333)  (not b348) )
  :assumption
(or b334  (not b348) )
  :assumption
(or (= r86 0)  b351 )
  :assumption
(or (not b351)  (= r86 80) )
  :assumption
(or b132  (not b351) )
  :assumption
(or (not b338)  (not b351) )
  :assumption
(or b333  (not b351) )
  :assumption
(or (= r92 0)  b354 )
  :assumption
(or (not b354)  (= r92 80) )
  :assumption
(or b136  (not b354) )
  :assumption
(or (not b342)  (not b354) )
  :assumption
(or b338  (not b354) )
  :assumption
(or (= r97 0)  b357 )
  :assumption
(or (not b357)  (= r97 80) )
  :assumption
(or b138  (not b357) )
  :assumption
(or (not b346)  (not b357) )
  :assumption
(or b342  (not b357) )
  :assumption
(or (= r66 0)  b360 )
  :assumption
(or (not b360)  (= r66 79) )
  :assumption
(or b284  (not b360) )
  :assumption
(or (not b360)  (not b362) )
  :assumption
(or (= r68 0)  b364 )
  :assumption
(or (not b364)  (= r68 79) )
  :assumption
(or b283  (not b364) )
  :assumption
(or (not b282)  (not b364) )
  :assumption
(or b362  (not b364) )
  :assumption
(or (= r73 0)  b367 )
  :assumption
(or (not b367)  (= r73 79) )
  :assumption
(or b289  (not b367) )
  :assumption
(or (not b288)  (not b367) )
  :assumption
(or b282  (not b367) )
  :assumption
(or (= r78 0)  b370 )
  :assumption
(or (not b370)  (= r78 79) )
  :assumption
(or b294  (not b370) )
  :assumption
(or (not b293)  (not b370) )
  :assumption
(or b288  (not b370) )
  :assumption
(or (= r85 0)  b373 )
  :assumption
(or (not b373)  (= r85 79) )
  :assumption
(or b299  (not b373) )
  :assumption
(or (not b298)  (not b373) )
  :assumption
(or b293  (not b373) )
  :assumption
(or (= r91 0)  b376 )
  :assumption
(or (not b376)  (= r91 79) )
  :assumption
(or b303  (not b376) )
  :assumption
(or (not b124)  (not b376) )
  :assumption
(or b298  (not b376) )
  :assumption
(or (= r96 0)  b379 )
  :assumption
(or (not b379)  (= r96 79) )
  :assumption
(or b307  (not b379) )
  :assumption
(or (not b123)  (not b379) )
  :assumption
(or b124  (not b379) )
  :assumption
(or (= r72 0)  b382 )
  :assumption
(or (not b382)  (= r72 29) )
  :assumption
(or b289  (not b382) )
  :assumption
(or (not b315)  (not b382) )
  :assumption
(or b311  (not b382) )
  :assumption
(or (= r77 0)  b385 )
  :assumption
(or (not b385)  (= r77 29) )
  :assumption
(or b294  (not b385) )
  :assumption
(or (not b319)  (not b385) )
  :assumption
(or b315  (not b385) )
  :assumption
(or (= r84 0)  b388 )
  :assumption
(or (not b388)  (= r84 29) )
  :assumption
(or b299  (not b388) )
  :assumption
(or (not b323)  (not b388) )
  :assumption
(or b319  (not b388) )
  :assumption
(or (= r1 0)  b391 )
  :assumption
(or (not b391)  (= r1 29) )
  :assumption
(or b303  (not b391) )
  :assumption
(or (not b128)  (not b391) )
  :assumption
(or b323  (not b391) )
  :assumption
(or (= r6 0)  b394 )
  :assumption
(or (not b394)  (= r6 29) )
  :assumption
(or b307  (not b394) )
  :assumption
(or (not b127)  (not b394) )
  :assumption
(or b128  (not b394) )
  :assumption
(or (= r10 0)  b397 )
  :assumption
(or (not b397)  (= r10 43) )
  :assumption
(or b334  (not b397) )
  :assumption
(or (not b315)  (not b397) )
  :assumption
(or b311  (not b397) )
  :assumption
(or (= r14 0)  b400 )
  :assumption
(or (not b400)  (= r14 43) )
  :assumption
(or b333  (not b400) )
  :assumption
(or (not b319)  (not b400) )
  :assumption
(or b315  (not b400) )
  :assumption
(or (= r17 0)  b403 )
  :assumption
(or (not b403)  (= r17 43) )
  :assumption
(or b338  (not b403) )
  :assumption
(or (not b323)  (not b403) )
  :assumption
(or b319  (not b403) )
  :assumption
(or (= r20 0)  b406 )
  :assumption
(or (not b406)  (= r20 43) )
  :assumption
(or b342  (not b406) )
  :assumption
(or (not b128)  (not b406) )
  :assumption
(or b323  (not b406) )
  :assumption
(or (= r21 0)  b409 )
  :assumption
(or (not b409)  (= r21 43) )
  :assumption
(or b346  (not b409) )
  :assumption
(or (not b127)  (not b409) )
  :assumption
(or b128  (not b409) )
  :assumption
(or (= r22 0)  b412 )
  :assumption
(or (not b412)  (= r22 80) )
  :assumption
(or b338  (not b412) )
  :assumption
(or (not b132)  (not b412) )
  :assumption
(or b133  (not b412) )
  :assumption
(or (= r23 0)  b415 )
  :assumption
(or (not b415)  (= r23 80) )
  :assumption
(or b342  (not b415) )
  :assumption
(or (not b136)  (not b415) )
  :assumption
(or b132  (not b415) )
  :assumption
(or (= r24 0)  b418 )
  :assumption
(or (not b418)  (= r24 80) )
  :assumption
(or b346  (not b418) )
  :assumption
(or (not b138)  (not b418) )
  :assumption
(or b136  (not b418) )
  :assumption
(or (= r25 0)  b421 )
  :assumption
(or (not b421)  (= r25 79) )
  :assumption
(or (not b421)  b423 )
  :assumption
(or (not b421)  (not b424) )
  :assumption
(or (not b421)  b425 )
  :assumption
(or (= r26 0)  b427 )
  :assumption
(or (not b427)  (= r26 79) )
  :assumption
(or (not b427)  b429 )
  :assumption
(or (not b427)  (not b430) )
  :assumption
(or b424  (not b427) )
  :assumption
(or (= r27 0)  b432 )
  :assumption
(or (not b432)  (= r27 79) )
  :assumption
(or (not b432)  b434 )
  :assumption
(or (not b432)  (not b435) )
  :assumption
(or b430  (not b432) )
  :assumption
(or (= r28 0)  b437 )
  :assumption
(or (not b437)  (= r28 79) )
  :assumption
(or (not b437)  b439 )
  :assumption
(or (not b437)  (not b440) )
  :assumption
(or b435  (not b437) )
  :assumption
(or (= r29 0)  b442 )
  :assumption
(or (not b442)  (= r29 79) )
  :assumption
(or b153  (not b442) )
  :assumption
(or (not b442)  (not b444) )
  :assumption
(or b440  (not b442) )
  :assumption
(or (= r30 0)  b446 )
  :assumption
(or (not b446)  (= r30 79) )
  :assumption
(or b152  (not b446) )
  :assumption
(or (not b446)  (not b448) )
  :assumption
(or b444  (not b446) )
  :assumption
(or (= r31 0)  b450 )
  :assumption
(or (not b450)  (= r31 29) )
  :assumption
(or (not b450)  b452 )
  :assumption
(or (not b424)  (not b450) )
  :assumption
(or b425  (not b450) )
  :assumption
(or (= r32 0)  b454 )
  :assumption
(or (not b454)  (= r32 29) )
  :assumption
(or (not b454)  b456 )
  :assumption
(or (not b430)  (not b454) )
  :assumption
(or b424  (not b454) )
  :assumption
(or (= r33 0)  b458 )
  :assumption
(or (not b458)  (= r33 29) )
  :assumption
(or (not b458)  b460 )
  :assumption
(or (not b435)  (not b458) )
  :assumption
(or b430  (not b458) )
  :assumption
(or (= r34 0)  b462 )
  :assumption
(or (not b462)  (= r34 29) )
  :assumption
(or (not b462)  b464 )
  :assumption
(or (not b440)  (not b462) )
  :assumption
(or b435  (not b462) )
  :assumption
(or (= r35 0)  b466 )
  :assumption
(or (not b466)  (= r35 29) )
  :assumption
(or (not b466)  b468 )
  :assumption
(or (not b444)  (not b466) )
  :assumption
(or b440  (not b466) )
  :assumption
(or (= r36 0)  b470 )
  :assumption
(or (not b470)  (= r36 29) )
  :assumption
(or (not b448)  (not b470) )
  :assumption
(or b444  (not b470) )
  :assumption
(or (= r37 0)  b473 )
  :assumption
(or (not b473)  (= r37 43) )
  :assumption
(or b460  (not b473) )
  :assumption
(or (not b473)  (not b475) )
  :assumption
(or (not b473)  b476 )
  :assumption
(or (= r38 0)  b478 )
  :assumption
(or (not b478)  (= r38 43) )
  :assumption
(or b464  (not b478) )
  :assumption
(or (not b478)  (not b480) )
  :assumption
(or b475  (not b478) )
  :assumption
(or (= r39 0)  b482 )
  :assumption
(or (not b482)  (= r39 43) )
  :assumption
(or b468  (not b482) )
  :assumption
(or (not b482)  (not b484) )
  :assumption
(or b480  (not b482) )
  :assumption
(or (= r40 0)  b486 )
  :assumption
(or (not b486)  (= r40 43) )
  :assumption
(or (not b486)  (not b488) )
  :assumption
(or b484  (not b486) )
  :assumption
(or (= r41 0)  b490 )
  :assumption
(or (not b490)  (= r41 80) )
  :assumption
(or b157  (not b490) )
  :assumption
(or (not b475)  (not b490) )
  :assumption
(or b476  (not b490) )
  :assumption
(or (= r42 0)  b493 )
  :assumption
(or (not b493)  (= r42 80) )
  :assumption
(or b156  (not b493) )
  :assumption
(or (not b480)  (not b493) )
  :assumption
(or b475  (not b493) )
  :assumption
(or (= r43 0)  b496 )
  :assumption
(or (not b496)  (= r43 80) )
  :assumption
(or b160  (not b496) )
  :assumption
(or (not b484)  (not b496) )
  :assumption
(or b480  (not b496) )
  :assumption
(or (= r44 0)  b499 )
  :assumption
(or (not b499)  (= r44 80) )
  :assumption
(or b162  (not b499) )
  :assumption
(or (not b488)  (not b499) )
  :assumption
(or b484  (not b499) )
  :assumption
(or (= r45 0)  b502 )
  :assumption
(or (not b502)  (= r45 79) )
  :assumption
(or b425  (not b502) )
  :assumption
(or (not b502)  (not b504) )
  :assumption
(or (= r46 0)  b506 )
  :assumption
(or (not b506)  (= r46 79) )
  :assumption
(or b424  (not b506) )
  :assumption
(or (not b423)  (not b506) )
  :assumption
(or b504  (not b506) )
  :assumption
(or (= r47 0)  b509 )
  :assumption
(or (not b509)  (= r47 79) )
  :assumption
(or b430  (not b509) )
  :assumption
(or (not b429)  (not b509) )
  :assumption
(or b423  (not b509) )
  :assumption
(or (= r48 0)  b512 )
  :assumption
(or (not b512)  (= r48 79) )
  :assumption
(or b435  (not b512) )
  :assumption
(or (not b434)  (not b512) )
  :assumption
(or b429  (not b512) )
  :assumption
(or (= r49 0)  b515 )
  :assumption
(or (not b515)  (= r49 79) )
  :assumption
(or b440  (not b515) )
  :assumption
(or (not b439)  (not b515) )
  :assumption
(or b434  (not b515) )
  :assumption
(or (= r50 0)  b518 )
  :assumption
(or (not b518)  (= r50 79) )
  :assumption
(or b444  (not b518) )
  :assumption
(or (not b153)  (not b518) )
  :assumption
(or b439  (not b518) )
  :assumption
(or (= r51 0)  b521 )
  :assumption
(or (not b521)  (= r51 79) )
  :assumption
(or b448  (not b521) )
  :assumption
(or (not b152)  (not b521) )
  :assumption
(or b153  (not b521) )
  :assumption
(or (= r52 0)  b524 )
  :assumption
(or (not b524)  (= r52 29) )
  :assumption
(or b430  (not b524) )
  :assumption
(or (not b456)  (not b524) )
  :assumption
(or b452  (not b524) )
  :assumption
(or (= r53 0)  b527 )
  :assumption
(or (not b527)  (= r53 29) )
  :assumption
(or b435  (not b527) )
  :assumption
(or (not b460)  (not b527) )
  :assumption
(or b456  (not b527) )
  :assumption
(or (= r54 0)  b530 )
  :assumption
(or (not b530)  (= r54 29) )
  :assumption
(or b440  (not b530) )
  :assumption
(or (not b464)  (not b530) )
  :assumption
(or b460  (not b530) )
  :assumption
(or (= r55 0)  b533 )
  :assumption
(or (not b533)  (= r55 29) )
  :assumption
(or b444  (not b533) )
  :assumption
(or (not b468)  (not b533) )
  :assumption
(or b464  (not b533) )
  :assumption
(or (= r57 0)  b537 )
  :assumption
(or (not b537)  (= r57 43) )
  :assumption
(or b476  (not b537) )
  :assumption
(or (not b456)  (not b537) )
  :assumption
(or b452  (not b537) )
  :assumption
(or (= r58 0)  b540 )
  :assumption
(or (not b540)  (= r58 43) )
  :assumption
(or b475  (not b540) )
  :assumption
(or (not b460)  (not b540) )
  :assumption
(or b456  (not b540) )
  :assumption
(or (= r59 0)  b543 )
  :assumption
(or (not b543)  (= r59 43) )
  :assumption
(or b480  (not b543) )
  :assumption
(or (not b464)  (not b543) )
  :assumption
(or b460  (not b543) )
  :assumption
(or (= r60 0)  b546 )
  :assumption
(or (not b546)  (= r60 43) )
  :assumption
(or b484  (not b546) )
  :assumption
(or (not b468)  (not b546) )
  :assumption
(or b464  (not b546) )
  :assumption
(or (= r62 0)  b550 )
  :assumption
(or (not b550)  (= r62 80) )
  :assumption
(or b480  (not b550) )
  :assumption
(or (not b156)  (not b550) )
  :assumption
(or b157  (not b550) )
  :assumption
(or (= r63 0)  b553 )
  :assumption
(or (not b553)  (= r63 80) )
  :assumption
(or b484  (not b553) )
  :assumption
(or (not b160)  (not b553) )
  :assumption
(or b156  (not b553) )
  :assumption
(or (= r64 0)  b556 )
  :assumption
(or (not b556)  (= r64 80) )
  :assumption
(or b488  (not b556) )
  :assumption
(or (not b162)  (not b556) )
  :assumption
(or b160  (not b556) )
  :assumption
(or (or b46  b48 )  b65 )
  :assumption
(or (or (or b48  (not b51) )  b106 )  b114 )
  :assumption
(or (or (or (not b48)  b49 )  b51 )  b67 )
  :assumption
(or (or (or b51  (not b54) )  b107 )  b115 )
  :assumption
(or (or (or (not b51)  b52 )  b54 )  b69 )
  :assumption
(or (or (or b54  (not b57) )  b108 )  b116 )
  :assumption
(or (or (or (not b54)  b55 )  b57 )  b71 )
  :assumption
(or (or (or b57  (not b60) )  b109 )  b117 )
  :assumption
(or (or (or (not b57)  b58 )  b60 )  b73 )
  :assumption
(or (or (or b60  (not b63) )  b110 )  b118 )
  :assumption
(or (or (or (not b60)  b61 )  b63 )  b75 )
  :assumption
(or (or b63  b111 )  b119 )
  :assumption
(or (or b104  (not b105) )  b113 )
  :assumption
(or (or b102  (not b103) )  b112 )
  :assumption
(or (or b14  b16 )  b33 )
  :assumption
(or (or (or b16  (not b19) )  b84 )  b95 )
  :assumption
(or (or (or (not b16)  b17 )  b19 )  b35 )
  :assumption
(or (or (or b19  (not b22) )  b85 )  b96 )
  :assumption
(or (or (or (not b19)  b20 )  b22 )  b37 )
  :assumption
(or (or (or b22  (not b25) )  b86 )  b97 )
  :assumption
(or (or (or (not b22)  b23 )  b25 )  b39 )
  :assumption
(or (or (or b25  (not b28) )  b87 )  b98 )
  :assumption
(or (or (or (not b25)  b26 )  b28 )  b41 )
  :assumption
(or (or (or b28  (not b31) )  b88 )  b99 )
  :assumption
(or (or (or (not b28)  b29 )  b31 )  b43 )
  :assumption
(or (or b31  b89 )  b100 )
  :assumption
(or (or b81  (not b82) )  b93 )
  :assumption
(or (or b78  (not b79) )  b91 )
  :assumption
(or (or (or (or b101  b256 )  b262 )  b268 )  b274 )
  :assumption
(or (or (or b101  b245 )  (not b247) )  b249 )
  :assumption
(or (or (or (or (or (not b101)  b247 )  b259 )  b265 )  b271 )  b277 )
  :assumption
(or (or (not b94)  b268 )  b274 )
  :assumption
(or (or (or (or b94  b238 )  b242 )  b271 )  b277 )
  :assumption
(or (or (not b92)  b256 )  b262 )
  :assumption
(or (or (or b92  (not b240) )  b259 )  b265 )
  :assumption
(or (or (or (or (or (not b92)  b238 )  b240 )  b242 )  b245 )  b249 )
  :assumption
(or (or (or (or b90  b214 )  b220 )  b226 )  b232 )
  :assumption
(or (or (or (or (or b90  b195 )  (not b197) )  b199 )  b208 )  b211 )
  :assumption
(or (or (or (or (or (not b90)  b197 )  b217 )  b223 )  b229 )  b235 )
  :assumption
(or (or (not b83)  b226 )  b232 )
  :assumption
(or (or (or (or (or b83  b187 )  (not b189) )  b192 )  b229 )  b235 )
  :assumption
(or (or (or (or (or (not b83)  b189 )  b202 )  b205 )  b208 )  b211 )
  :assumption
(or (or (not b80)  b214 )  b220 )
  :assumption
(or (or (or (or (or b80  (not b190) )  b202 )  b205 )  b217 )  b223 )
  :assumption
(or (or (or (or (or (not b80)  b187 )  b190 )  b192 )  b195 )  b199 )
  :assumption
(or (not b157)  b490 )
  :assumption
(or (or (not b156)  b157 )  b493 )
  :assumption
(or (or (or (or b154  b156 )  (not b157) )  b165 )  b550 )
  :assumption
(or (or (or (or b156  (not b160) )  b180 )  b184 )  b496 )
  :assumption
(or (or (or (or (not b156)  b158 )  b160 )  b167 )  b553 )
  :assumption
(or (or (or (or b160  (not b162) )  b181 )  b185 )  b499 )
  :assumption
(or (or (or (or (not b160)  b161 )  b162 )  b169 )  b556 )
  :assumption
(or b450  (not b452) )
  :assumption
(or (or b452  b454 )  (not b456) )
  :assumption
(or (or (or (not b452)  b456 )  b524 )  b537 )
  :assumption
(or (or (or b456  b458 )  (not b460) )  b473 )
  :assumption
(or (or (or (not b456)  b460 )  b527 )  b540 )
  :assumption
(or (or (or b460  b462 )  (not b464) )  b478 )
  :assumption
(or (or (or (not b460)  b464 )  b530 )  b543 )
  :assumption
(or (or (or b464  b466 )  (not b468) )  b482 )
  :assumption
(or (or (or (not b464)  b468 )  b533 )  b546 )
  :assumption
(or (or (or (or b179  b183 )  b468 )  b470 )  b486 )
  :assumption
(or b502  b504 )
  :assumption
(or (or b421  (not b423) )  b504 )
  :assumption
(or (or b423  (not b504) )  b506 )
  :assumption
(or (or b423  b427 )  (not b429) )
  :assumption
(or (or (not b423)  b429 )  b509 )
  :assumption
(or (or b429  b432 )  (not b434) )
  :assumption
(or (or (not b429)  b434 )  b512 )
  :assumption
(or (or b434  b437 )  (not b439) )
  :assumption
(or (or (not b434)  b439 )  b515 )
  :assumption
(or (or (not b153)  b439 )  b442 )
  :assumption
(or (or b153  (not b439) )  b518 )
  :assumption
(or (or (or (or (not b152)  b153 )  b178 )  b182 )  b446 )
  :assumption
(or (or (or (or b150  b152 )  (not b153) )  b163 )  b521 )
  :assumption
(or (not b476)  b537 )
  :assumption
(or (or (not b475)  b476 )  b540 )
  :assumption
(or (or (or b473  b475 )  (not b476) )  b490 )
  :assumption
(or (or (or b475  (not b480) )  b543 )  b550 )
  :assumption
(or (or (or (not b475)  b478 )  b480 )  b493 )
  :assumption
(or (or (or b480  (not b484) )  b546 )  b553 )
  :assumption
(or (or (or (not b480)  b482 )  b484 )  b496 )
  :assumption
(or (or b484  (not b488) )  b556 )
  :assumption
(or (or (or (not b484)  b486 )  b488 )  b499 )
  :assumption
(or (not b425)  b502 )
  :assumption
(or (or (not b424)  b425 )  b506 )
  :assumption
(or (or (or b421  b424 )  (not b425) )  b450 )
  :assumption
(or (or (or b424  (not b430) )  b509 )  b524 )
  :assumption
(or (or (or (not b424)  b427 )  b430 )  b454 )
  :assumption
(or (or (or b430  (not b435) )  b512 )  b527 )
  :assumption
(or (or (or (not b430)  b432 )  b435 )  b458 )
  :assumption
(or (or (or b435  (not b440) )  b515 )  b530 )
  :assumption
(or (or (or (not b435)  b437 )  b440 )  b462 )
  :assumption
(or (or (or b440  (not b444) )  b518 )  b533 )
  :assumption
(or (or (or (not b440)  b442 )  b444 )  b466 )
  :assumption
(or (or b444  (not b448) )  b521 )
  :assumption
(or (or (or (not b444)  b446 )  b448 )  b470 )
  :assumption
(or (not b133)  b348 )
  :assumption
(or (or (not b132)  b133 )  b351 )
  :assumption
(or (or (or (or b129  b132 )  (not b133) )  b144 )  b412 )
  :assumption
(or (or (or (or b132  (not b136) )  b172 )  b176 )  b354 )
  :assumption
(or (or (or (or (not b132)  b134 )  b136 )  b147 )  b415 )
  :assumption
(or (or (or (or b136  (not b138) )  b173 )  b177 )  b357 )
  :assumption
(or (or (or (or (not b136)  b137 )  b138 )  b149 )  b418 )
  :assumption
(or b309  (not b311) )
  :assumption
(or (or b311  b313 )  (not b315) )
  :assumption
(or (or (or (not b311)  b315 )  b382 )  b397 )
  :assumption
(or (or (or b315  b317 )  (not b319) )  b331 )
  :assumption
(or (or (or (not b315)  b319 )  b385 )  b400 )
  :assumption
(or (or (or b319  b321 )  (not b323) )  b336 )
  :assumption
(or (or (or (not b319)  b323 )  b388 )  b403 )
  :assumption
(or (or (or (not b128)  b323 )  b325 )  b340 )
  :assumption
(or (or (or b128  (not b323) )  b391 )  b406 )
  :assumption
(or (or (or (or (or (not b127)  b128 )  b171 )  b175 )  b328 )  b344 )
  :assumption
(or (or (or (or (or b126  b127 )  (not b128) )  b143 )  b394 )  b409 )
  :assumption
(or b360  b362 )
  :assumption
(or (or b280  (not b282) )  b362 )
  :assumption
(or (or b282  (not b362) )  b364 )
  :assumption
(or (or b282  b286 )  (not b288) )
  :assumption
(or (or (not b282)  b288 )  b367 )
  :assumption
(or (or b288  b291 )  (not b293) )
  :assumption
(or (or (not b288)  b293 )  b370 )
  :assumption
(or (or b293  b296 )  (not b298) )
  :assumption
(or (or (not b293)  b298 )  b373 )
  :assumption
(or (or (not b124)  b298 )  b301 )
  :assumption
(or (or b124  (not b298) )  b376 )
  :assumption
(or (or (or (or (not b123)  b124 )  b170 )  b174 )  b305 )
  :assumption
(or (or (or (or b120  b123 )  (not b124) )  b139 )  b379 )
  :assumption
(or (not b334)  b397 )
  :assumption
(or (or (not b333)  b334 )  b400 )
  :assumption
(or (or (or b331  b333 )  (not b334) )  b348 )
  :assumption
(or (or (or b333  (not b338) )  b403 )  b412 )
  :assumption
(or (or (or (not b333)  b336 )  b338 )  b351 )
  :assumption
(or (or (or b338  (not b342) )  b406 )  b415 )
  :assumption
(or (or (or (not b338)  b340 )  b342 )  b354 )
  :assumption
(or (or (or b342  (not b346) )  b409 )  b418 )
  :assumption
(or (or (or (not b342)  b344 )  b346 )  b357 )
  :assumption
(or (not b284)  b360 )
  :assumption
(or (or (not b283)  b284 )  b364 )
  :assumption
(or (or (or b280  b283 )  (not b284) )  b309 )
  :assumption
(or (or (or b283  (not b289) )  b367 )  b382 )
  :assumption
(or (or (or (not b283)  b286 )  b289 )  b313 )
  :assumption
(or (or (or b289  (not b294) )  b370 )  b385 )
  :assumption
(or (or (or (not b289)  b291 )  b294 )  b317 )
  :assumption
(or (or (or b294  (not b299) )  b373 )  b388 )
  :assumption
(or (or (or (not b294)  b296 )  b299 )  b321 )
  :assumption
(or (or (or b299  (not b303) )  b376 )  b391 )
  :assumption
(or (or (or (not b299)  b301 )  b303 )  b325 )
  :assumption
(or (or (or b303  (not b307) )  b379 )  b394 )
  :assumption
(or (or (or (not b303)  b305 )  b307 )  b328 )
  :assumption
(or b65  (not b66) )
  :assumption
(or (or b66  b67 )  (not b68) )
  :assumption
(or (or (not b66)  b68 )  b114 )
  :assumption
(or (or b68  b69 )  (not b70) )
  :assumption
(or (or (not b68)  b70 )  b115 )
  :assumption
(or (or b70  b71 )  (not b72) )
  :assumption
(or (or (not b70)  b72 )  b116 )
  :assumption
(or (or b72  b73 )  (not b74) )
  :assumption
(or (or (not b72)  b74 )  b117 )
  :assumption
(or (or b74  b75 )  (not b76) )
  :assumption
(or (or (not b74)  b76 )  b118 )
  :assumption
(or b76  (not b77) )
  :assumption
(or (or (or (or (not b76)  b77 )  b112 )  b113 )  b119 )
  :assumption
(or b46  (not b47) )
  :assumption
(or (or b47  b49 )  (not b50) )
  :assumption
(or (or (not b47)  b50 )  b106 )
  :assumption
(or (or b50  b52 )  (not b53) )
  :assumption
(or (or (not b50)  b53 )  b107 )
  :assumption
(or (or b53  b55 )  (not b56) )
  :assumption
(or (or (not b53)  b56 )  b108 )
  :assumption
(or (or b56  b58 )  (not b59) )
  :assumption
(or (or (not b56)  b59 )  b109 )
  :assumption
(or (or b59  b61 )  (not b62) )
  :assumption
(or (or (not b59)  b62 )  b110 )
  :assumption
(or b62  (not b64) )
  :assumption
(or (or (or (or (not b62)  b64 )  b102 )  b104 )  b111 )
  :assumption
(or b33  (not b34) )
  :assumption
(or (or b34  b35 )  (not b36) )
  :assumption
(or (or (not b34)  b36 )  b95 )
  :assumption
(or (or b36  b37 )  (not b38) )
  :assumption
(or (or (not b36)  b38 )  b96 )
  :assumption
(or (or b38  b39 )  (not b40) )
  :assumption
(or (or (not b38)  b40 )  b97 )
  :assumption
(or (or b40  b41 )  (not b42) )
  :assumption
(or (or (not b40)  b42 )  b98 )
  :assumption
(or (or b42  b43 )  (not b44) )
  :assumption
(or (or (not b42)  b44 )  b99 )
  :assumption
(or b44  (not b45) )
  :assumption
(or (or (or (or (not b44)  b45 )  b91 )  b93 )  b100 )
  :assumption
(or b14  (not b15) )
  :assumption
(or (or b15  b17 )  (not b18) )
  :assumption
(or (or (not b15)  b18 )  b84 )
  :assumption
(or (or b18  b20 )  (not b21) )
  :assumption
(or (or (not b18)  b21 )  b85 )
  :assumption
(or (or b21  b23 )  (not b24) )
  :assumption
(or (or (not b21)  b24 )  b86 )
  :assumption
(or (or b24  b26 )  (not b27) )
  :assumption
(or (or (not b24)  b27 )  b87 )
  :assumption
(or (or b27  b29 )  (not b30) )
  :assumption
(or (or (not b27)  b30 )  b88 )
  :assumption
(or b30  (not b32) )
  :assumption
(or (or (or (or (not b30)  b32 )  b78 )  b81 )  b89 )
  :assumption
(or b165  (not b166) )
  :assumption
(or (or b166  b167 )  (not b168) )
  :assumption
(or (or (not b166)  b168 )  b184 )
  :assumption
(or (or (or b163  (not b164) )  b168 )  b169 )
  :assumption
(or (or (or (or b164  (not b168) )  b182 )  b183 )  b185 )
  :assumption
(or b154  (not b155) )
  :assumption
(or (or b155  b158 )  (not b159) )
  :assumption
(or (or (not b155)  b159 )  b180 )
  :assumption
(or (or (or b150  (not b151) )  b159 )  b161 )
  :assumption
(or (or (or (or b151  (not b159) )  b178 )  b179 )  b181 )
  :assumption
(or b144  (not b146) )
  :assumption
(or (or b146  b147 )  (not b148) )
  :assumption
(or (or (not b146)  b148 )  b176 )
  :assumption
(or (or (or (or b139  (not b141) )  b143 )  b148 )  b149 )
  :assumption
(or (or (or (or b141  (not b148) )  b174 )  b175 )  b177 )
  :assumption
(or b129  (not b131) )
  :assumption
(or (or b131  b134 )  (not b135) )
  :assumption
(or (or (not b131)  b135 )  b172 )
  :assumption
(or (or (or (or b120  (not b122) )  b126 )  b135 )  b137 )
  :assumption
(or (or (or (or b122  (not b135) )  b170 )  b171 )  b173 )
  :assumption
(or (or b144  b145 )  b165 )
  :assumption
(or (or (or (not b142)  b145 )  b176 )  b184 )
  :assumption
(or (or (or b142  (not b145) )  b147 )  b167 )
  :assumption
(or (or (or (or (or (or (or (not b140)  b142 )  b174 )  b175 )  b177 )  b182 )  b183 )  b185 )
  :assumption
(or (or (or (or (or (or b139  b140 )  (not b142) )  b143 )  b149 )  b163 )  b169 )
  :assumption
(or (or b129  b130 )  b154 )
  :assumption
(or (or (or (not b125)  b130 )  b172 )  b180 )
  :assumption
(or (or (or b125  (not b130) )  b134 )  b158 )
  :assumption
(or (or (or (or (or (or (or (not b121)  b125 )  b170 )  b171 )  b173 )  b178 )  b179 )  b181 )
  :assumption
(or (or (or (or (or (or b120  b121 )  (not b125) )  b126 )  b137 )  b150 )  b161 )
  :assumption
(or (not b14)  (not b33) )
  :assumption
(or (not b17)  (not b35) )
  :assumption
(or (not b20)  (not b37) )
  :assumption
(or (not b23)  (not b39) )
  :assumption
(or (not b26)  (not b41) )
  :assumption
(or (not b29)  (not b43) )
  :assumption
(or (not b17)  (not b95) )
  :assumption
(or (not b20)  (not b96) )
  :assumption
(or (not b23)  (not b97) )
  :assumption
(or (not b26)  (not b98) )
  :assumption
(or (not b29)  (not b99) )
  :assumption
(or (not b17)  (not b84) )
  :assumption
(or (not b20)  (not b85) )
  :assumption
(or (not b23)  (not b86) )
  :assumption
(or (not b26)  (not b87) )
  :assumption
(or (not b29)  (not b88) )
  :assumption
(or (not b35)  (not b95) )
  :assumption
(or (not b37)  (not b96) )
  :assumption
(or (not b39)  (not b97) )
  :assumption
(or (not b41)  (not b98) )
  :assumption
(or (not b43)  (not b99) )
  :assumption
(or (not b35)  (not b84) )
  :assumption
(or (not b37)  (not b85) )
  :assumption
(or (not b39)  (not b86) )
  :assumption
(or (not b41)  (not b87) )
  :assumption
(or (not b43)  (not b88) )
  :assumption
(or (not b46)  (not b65) )
  :assumption
(or (not b49)  (not b67) )
  :assumption
(or (not b52)  (not b69) )
  :assumption
(or (not b55)  (not b71) )
  :assumption
(or (not b58)  (not b73) )
  :assumption
(or (not b61)  (not b75) )
  :assumption
(or (not b49)  (not b114) )
  :assumption
(or (not b52)  (not b115) )
  :assumption
(or (not b55)  (not b116) )
  :assumption
(or (not b58)  (not b117) )
  :assumption
(or (not b61)  (not b118) )
  :assumption
(or (not b49)  (not b106) )
  :assumption
(or (not b52)  (not b107) )
  :assumption
(or (not b55)  (not b108) )
  :assumption
(or (not b58)  (not b109) )
  :assumption
(or (not b61)  (not b110) )
  :assumption
(or (not b67)  (not b114) )
  :assumption
(or (not b69)  (not b115) )
  :assumption
(or (not b71)  (not b116) )
  :assumption
(or (not b73)  (not b117) )
  :assumption
(or (not b75)  (not b118) )
  :assumption
(or (not b67)  (not b106) )
  :assumption
(or (not b69)  (not b107) )
  :assumption
(or (not b71)  (not b108) )
  :assumption
(or (not b73)  (not b109) )
  :assumption
(or (not b75)  (not b110) )
  :assumption
(or (not b78)  (not b89) )
  :assumption
(or (not b78)  (not b81) )
  :assumption
(or (not b81)  (not b89) )
  :assumption
(or (not b91)  (not b100) )
  :assumption
(or (not b91)  (not b93) )
  :assumption
(or (not b93)  (not b100) )
  :assumption
(or (not b102)  (not b111) )
  :assumption
(or (not b102)  (not b104) )
  :assumption
(or (not b104)  (not b111) )
  :assumption
(or (not b112)  (not b119) )
  :assumption
(or (not b112)  (not b113) )
  :assumption
(or (not b113)  (not b119) )
  :assumption
(or (not b120)  (not b379) )
  :assumption
(or (not b120)  (not b139) )
  :assumption
(or (not b120)  (not b305) )
  :assumption
(or (not b120)  (not b174) )
  :assumption
(or (not b120)  (not b170) )
  :assumption
(or (not b120)  (not b229) )
  :assumption
(or (not b120)  (not b217) )
  :assumption
(or (not b120)  (not b208) )
  :assumption
(or (not b120)  (not b202) )
  :assumption
(or (not b120)  (not b195) )
  :assumption
(or (not b120)  (not b187) )
  :assumption
(or (not b120)  (not b173) )
  :assumption
(or (not b120)  (not b171) )
  :assumption
(or (not b120)  (not b161) )
  :assumption
(or (not b120)  (not b150) )
  :assumption
(or (not b120)  (not b137) )
  :assumption
(or (not b120)  (not b126) )
  :assumption
(or (not b120)  (not b181) )
  :assumption
(or (not b120)  (not b179) )
  :assumption
(or (not b120)  (not b178) )
  :assumption
(or (not b126)  (not b409) )
  :assumption
(or (not b126)  (not b394) )
  :assumption
(or (not b126)  (not b143) )
  :assumption
(or (not b126)  (not b344) )
  :assumption
(or (not b126)  (not b328) )
  :assumption
(or (not b126)  (not b175) )
  :assumption
(or (not b126)  (not b171) )
  :assumption
(or (not b126)  (not b229) )
  :assumption
(or (not b126)  (not b217) )
  :assumption
(or (not b126)  (not b208) )
  :assumption
(or (not b126)  (not b202) )
  :assumption
(or (not b126)  (not b195) )
  :assumption
(or (not b126)  (not b187) )
  :assumption
(or (not b126)  (not b173) )
  :assumption
(or (not b126)  (not b170) )
  :assumption
(or (not b126)  (not b161) )
  :assumption
(or (not b126)  (not b150) )
  :assumption
(or (not b126)  (not b137) )
  :assumption
(or (not b126)  (not b181) )
  :assumption
(or (not b126)  (not b179) )
  :assumption
(or (not b126)  (not b178) )
  :assumption
(or (not b129)  (not b412) )
  :assumption
(or (not b134)  (not b415) )
  :assumption
(or (not b137)  (not b418) )
  :assumption
(or (not b129)  (not b144) )
  :assumption
(or (not b134)  (not b147) )
  :assumption
(or (not b137)  (not b149) )
  :assumption
(or (not b129)  (not b351) )
  :assumption
(or (not b134)  (not b354) )
  :assumption
(or (not b137)  (not b357) )
  :assumption
(or (not b134)  (not b176) )
  :assumption
(or (not b137)  (not b177) )
  :assumption
(or (not b134)  (not b172) )
  :assumption
(or (not b137)  (not b173) )
  :assumption
(or (not b134)  (not b226) )
  :assumption
(or (not b137)  (not b229) )
  :assumption
(or (not b134)  (not b214) )
  :assumption
(or (not b137)  (not b217) )
  :assumption
(or (not b137)  (not b208) )
  :assumption
(or (not b137)  (not b202) )
  :assumption
(or (not b137)  (not b195) )
  :assumption
(or (not b137)  (not b187) )
  :assumption
(or (not b137)  (not b171) )
  :assumption
(or (not b137)  (not b170) )
  :assumption
(or (not b129)  (not b154) )
  :assumption
(or (not b134)  (not b158) )
  :assumption
(or (not b137)  (not b161) )
  :assumption
(or (not b137)  (not b150) )
  :assumption
(or (not b134)  (not b180) )
  :assumption
(or (not b137)  (not b181) )
  :assumption
(or (not b137)  (not b179) )
  :assumption
(or (not b137)  (not b178) )
  :assumption
(or (not b139)  (not b379) )
  :assumption
(or (not b139)  (not b305) )
  :assumption
(or (not b139)  (not b174) )
  :assumption
(or (not b139)  (not b170) )
  :assumption
(or (not b139)  (not b271) )
  :assumption
(or (not b139)  (not b259) )
  :assumption
(or (not b139)  (not b245) )
  :assumption
(or (not b139)  (not b238) )
  :assumption
(or (not b139)  (not b177) )
  :assumption
(or (not b139)  (not b175) )
  :assumption
(or (not b139)  (not b169) )
  :assumption
(or (not b139)  (not b163) )
  :assumption
(or (not b139)  (not b149) )
  :assumption
(or (not b139)  (not b143) )
  :assumption
(or (not b139)  (not b185) )
  :assumption
(or (not b139)  (not b183) )
  :assumption
(or (not b139)  (not b182) )
  :assumption
(or (not b143)  (not b409) )
  :assumption
(or (not b143)  (not b394) )
  :assumption
(or (not b143)  (not b344) )
  :assumption
(or (not b143)  (not b328) )
  :assumption
(or (not b143)  (not b175) )
  :assumption
(or (not b143)  (not b171) )
  :assumption
(or (not b143)  (not b271) )
  :assumption
(or (not b143)  (not b259) )
  :assumption
(or (not b143)  (not b245) )
  :assumption
(or (not b143)  (not b238) )
  :assumption
(or (not b143)  (not b177) )
  :assumption
(or (not b143)  (not b174) )
  :assumption
(or (not b143)  (not b169) )
  :assumption
(or (not b143)  (not b163) )
  :assumption
(or (not b143)  (not b149) )
  :assumption
(or (not b143)  (not b185) )
  :assumption
(or (not b143)  (not b183) )
  :assumption
(or (not b143)  (not b182) )
  :assumption
(or (not b144)  (not b412) )
  :assumption
(or (not b147)  (not b415) )
  :assumption
(or (not b149)  (not b418) )
  :assumption
(or (not b144)  (not b351) )
  :assumption
(or (not b147)  (not b354) )
  :assumption
(or (not b149)  (not b357) )
  :assumption
(or (not b147)  (not b176) )
  :assumption
(or (not b149)  (not b177) )
  :assumption
(or (not b147)  (not b172) )
  :assumption
(or (not b149)  (not b173) )
  :assumption
(or (not b147)  (not b268) )
  :assumption
(or (not b149)  (not b271) )
  :assumption
(or (not b147)  (not b256) )
  :assumption
(or (not b149)  (not b259) )
  :assumption
(or (not b149)  (not b245) )
  :assumption
(or (not b149)  (not b238) )
  :assumption
(or (not b149)  (not b175) )
  :assumption
(or (not b149)  (not b174) )
  :assumption
(or (not b144)  (not b165) )
  :assumption
(or (not b147)  (not b167) )
  :assumption
(or (not b149)  (not b169) )
  :assumption
(or (not b149)  (not b163) )
  :assumption
(or (not b147)  (not b184) )
  :assumption
(or (not b149)  (not b185) )
  :assumption
(or (not b149)  (not b183) )
  :assumption
(or (not b149)  (not b182) )
  :assumption
(or (not b150)  (not b521) )
  :assumption
(or (not b150)  (not b163) )
  :assumption
(or (not b150)  (not b446) )
  :assumption
(or (not b150)  (not b182) )
  :assumption
(or (not b150)  (not b178) )
  :assumption
(or (not b150)  (not b235) )
  :assumption
(or (not b150)  (not b223) )
  :assumption
(or (not b150)  (not b211) )
  :assumption
(or (not b150)  (not b205) )
  :assumption
(or (not b150)  (not b199) )
  :assumption
(or (not b150)  (not b192) )
  :assumption
(or (not b150)  (not b181) )
  :assumption
(or (not b150)  (not b179) )
  :assumption
(or (not b150)  (not b161) )
  :assumption
(or (not b150)  (not b173) )
  :assumption
(or (not b150)  (not b171) )
  :assumption
(or (not b150)  (not b170) )
  :assumption
(or (not b154)  (not b550) )
  :assumption
(or (not b158)  (not b553) )
  :assumption
(or (not b161)  (not b556) )
  :assumption
(or (not b154)  (not b165) )
  :assumption
(or (not b158)  (not b167) )
  :assumption
(or (not b161)  (not b169) )
  :assumption
(or (not b154)  (not b493) )
  :assumption
(or (not b158)  (not b496) )
  :assumption
(or (not b161)  (not b499) )
  :assumption
(or (not b158)  (not b184) )
  :assumption
(or (not b161)  (not b185) )
  :assumption
(or (not b158)  (not b180) )
  :assumption
(or (not b161)  (not b181) )
  :assumption
(or (not b158)  (not b232) )
  :assumption
(or (not b161)  (not b235) )
  :assumption
(or (not b158)  (not b220) )
  :assumption
(or (not b161)  (not b223) )
  :assumption
(or (not b161)  (not b211) )
  :assumption
(or (not b161)  (not b205) )
  :assumption
(or (not b161)  (not b199) )
  :assumption
(or (not b161)  (not b192) )
  :assumption
(or (not b161)  (not b179) )
  :assumption
(or (not b161)  (not b178) )
  :assumption
(or (not b158)  (not b172) )
  :assumption
(or (not b161)  (not b173) )
  :assumption
(or (not b161)  (not b171) )
  :assumption
(or (not b161)  (not b170) )
  :assumption
(or (not b163)  (not b521) )
  :assumption
(or (not b163)  (not b446) )
  :assumption
(or (not b163)  (not b182) )
  :assumption
(or (not b163)  (not b178) )
  :assumption
(or (not b163)  (not b277) )
  :assumption
(or (not b163)  (not b265) )
  :assumption
(or (not b163)  (not b249) )
  :assumption
(or (not b163)  (not b242) )
  :assumption
(or (not b163)  (not b185) )
  :assumption
(or (not b163)  (not b183) )
  :assumption
(or (not b163)  (not b169) )
  :assumption
(or (not b163)  (not b177) )
  :assumption
(or (not b163)  (not b175) )
  :assumption
(or (not b163)  (not b174) )
  :assumption
(or (not b165)  (not b550) )
  :assumption
(or (not b167)  (not b553) )
  :assumption
(or (not b169)  (not b556) )
  :assumption
(or (not b165)  (not b493) )
  :assumption
(or (not b167)  (not b496) )
  :assumption
(or (not b169)  (not b499) )
  :assumption
(or (not b167)  (not b184) )
  :assumption
(or (not b169)  (not b185) )
  :assumption
(or (not b167)  (not b180) )
  :assumption
(or (not b169)  (not b181) )
  :assumption
(or (not b167)  (not b274) )
  :assumption
(or (not b169)  (not b277) )
  :assumption
(or (not b167)  (not b262) )
  :assumption
(or (not b169)  (not b265) )
  :assumption
(or (not b169)  (not b249) )
  :assumption
(or (not b169)  (not b242) )
  :assumption
(or (not b169)  (not b183) )
  :assumption
(or (not b169)  (not b182) )
  :assumption
(or (not b167)  (not b176) )
  :assumption
(or (not b169)  (not b177) )
  :assumption
(or (not b169)  (not b175) )
  :assumption
(or (not b169)  (not b174) )
  :assumption
(or (not b170)  (not b229) )
  :assumption
(or (not b170)  (not b217) )
  :assumption
(or (not b170)  (not b208) )
  :assumption
(or (not b170)  (not b202) )
  :assumption
(or (not b170)  (not b195) )
  :assumption
(or (not b170)  (not b187) )
  :assumption
(or (not b170)  (not b173) )
  :assumption
(or (not b170)  (not b171) )
  :assumption
(or (not b170)  (not b379) )
  :assumption
(or (not b171)  (not b229) )
  :assumption
(or (not b171)  (not b217) )
  :assumption
(or (not b171)  (not b208) )
  :assumption
(or (not b171)  (not b202) )
  :assumption
(or (not b171)  (not b195) )
  :assumption
(or (not b171)  (not b187) )
  :assumption
(or (not b171)  (not b173) )
  :assumption
(or (not b171)  (not b409) )
  :assumption
(or (not b171)  (not b394) )
  :assumption
(or (not b172)  (not b226) )
  :assumption
(or (not b173)  (not b229) )
  :assumption
(or (not b172)  (not b214) )
  :assumption
(or (not b173)  (not b217) )
  :assumption
(or (not b173)  (not b208) )
  :assumption
(or (not b173)  (not b202) )
  :assumption
(or (not b173)  (not b195) )
  :assumption
(or (not b173)  (not b187) )
  :assumption
(or (not b172)  (not b415) )
  :assumption
(or (not b173)  (not b418) )
  :assumption
(or (not b174)  (not b271) )
  :assumption
(or (not b174)  (not b259) )
  :assumption
(or (not b174)  (not b245) )
  :assumption
(or (not b174)  (not b238) )
  :assumption
(or (not b174)  (not b177) )
  :assumption
(or (not b174)  (not b175) )
  :assumption
(or (not b174)  (not b379) )
  :assumption
(or (not b175)  (not b271) )
  :assumption
(or (not b175)  (not b259) )
  :assumption
(or (not b175)  (not b245) )
  :assumption
(or (not b175)  (not b238) )
  :assumption
(or (not b175)  (not b177) )
  :assumption
(or (not b175)  (not b409) )
  :assumption
(or (not b175)  (not b394) )
  :assumption
(or (not b176)  (not b268) )
  :assumption
(or (not b177)  (not b271) )
  :assumption
(or (not b176)  (not b256) )
  :assumption
(or (not b177)  (not b259) )
  :assumption
(or (not b177)  (not b245) )
  :assumption
(or (not b177)  (not b238) )
  :assumption
(or (not b176)  (not b415) )
  :assumption
(or (not b177)  (not b418) )
  :assumption
(or (not b178)  (not b235) )
  :assumption
(or (not b178)  (not b223) )
  :assumption
(or (not b178)  (not b211) )
  :assumption
(or (not b178)  (not b205) )
  :assumption
(or (not b178)  (not b199) )
  :assumption
(or (not b178)  (not b192) )
  :assumption
(or (not b178)  (not b181) )
  :assumption
(or (not b178)  (not b179) )
  :assumption
(or (not b178)  (not b521) )
  :assumption
(or (not b179)  (not b235) )
  :assumption
(or (not b179)  (not b223) )
  :assumption
(or (not b179)  (not b211) )
  :assumption
(or (not b179)  (not b205) )
  :assumption
(or (not b179)  (not b199) )
  :assumption
(or (not b179)  (not b192) )
  :assumption
(or (not b179)  (not b181) )
  :assumption
(or (not b180)  (not b232) )
  :assumption
(or (not b181)  (not b235) )
  :assumption
(or (not b180)  (not b220) )
  :assumption
(or (not b181)  (not b223) )
  :assumption
(or (not b181)  (not b211) )
  :assumption
(or (not b181)  (not b205) )
  :assumption
(or (not b181)  (not b199) )
  :assumption
(or (not b181)  (not b192) )
  :assumption
(or (not b180)  (not b553) )
  :assumption
(or (not b181)  (not b556) )
  :assumption
(or (not b182)  (not b277) )
  :assumption
(or (not b182)  (not b265) )
  :assumption
(or (not b182)  (not b249) )
  :assumption
(or (not b182)  (not b242) )
  :assumption
(or (not b182)  (not b185) )
  :assumption
(or (not b182)  (not b183) )
  :assumption
(or (not b182)  (not b521) )
  :assumption
(or (not b183)  (not b277) )
  :assumption
(or (not b183)  (not b265) )
  :assumption
(or (not b183)  (not b249) )
  :assumption
(or (not b183)  (not b242) )
  :assumption
(or (not b183)  (not b185) )
  :assumption
(or (not b184)  (not b274) )
  :assumption
(or (not b185)  (not b277) )
  :assumption
(or (not b184)  (not b262) )
  :assumption
(or (not b185)  (not b265) )
  :assumption
(or (not b185)  (not b249) )
  :assumption
(or (not b185)  (not b242) )
  :assumption
(or (not b184)  (not b553) )
  :assumption
(or (not b185)  (not b556) )
  :assumption
(or (not b187)  (not b199) )
  :assumption
(or (not b187)  (not b195) )
  :assumption
(or (not b187)  (not b192) )
  :assumption
(or (not b178)  (not b187) )
  :assumption
(or (not b150)  (not b187) )
  :assumption
(or (not b102)  (not b187) )
  :assumption
(or (not b78)  (not b187) )
  :assumption
(or (not b187)  (not b223) )
  :assumption
(or (not b187)  (not b217) )
  :assumption
(or (not b187)  (not b205) )
  :assumption
(or (not b187)  (not b202) )
  :assumption
(or (not b187)  (not b211) )
  :assumption
(or (not b187)  (not b208) )
  :assumption
(or (not b179)  (not b187) )
  :assumption
(or (not b104)  (not b187) )
  :assumption
(or (not b81)  (not b187) )
  :assumption
(or (not b192)  (not b199) )
  :assumption
(or (not b192)  (not b195) )
  :assumption
(or (not b170)  (not b192) )
  :assumption
(or (not b120)  (not b192) )
  :assumption
(or (not b102)  (not b192) )
  :assumption
(or (not b78)  (not b192) )
  :assumption
(or (not b192)  (not b223) )
  :assumption
(or (not b192)  (not b217) )
  :assumption
(or (not b192)  (not b205) )
  :assumption
(or (not b192)  (not b202) )
  :assumption
(or (not b192)  (not b211) )
  :assumption
(or (not b192)  (not b208) )
  :assumption
(or (not b171)  (not b192) )
  :assumption
(or (not b126)  (not b192) )
  :assumption
(or (not b104)  (not b192) )
  :assumption
(or (not b81)  (not b192) )
  :assumption
(or (not b195)  (not b199) )
  :assumption
(or (not b178)  (not b195) )
  :assumption
(or (not b150)  (not b195) )
  :assumption
(or (not b102)  (not b195) )
  :assumption
(or (not b78)  (not b195) )
  :assumption
(or (not b195)  (not b223) )
  :assumption
(or (not b195)  (not b217) )
  :assumption
(or (not b195)  (not b205) )
  :assumption
(or (not b195)  (not b202) )
  :assumption
(or (not b195)  (not b235) )
  :assumption
(or (not b195)  (not b229) )
  :assumption
(or (not b181)  (not b195) )
  :assumption
(or (not b161)  (not b195) )
  :assumption
(or (not b111)  (not b195) )
  :assumption
(or (not b89)  (not b195) )
  :assumption
(or (not b170)  (not b199) )
  :assumption
(or (not b120)  (not b199) )
  :assumption
(or (not b102)  (not b199) )
  :assumption
(or (not b78)  (not b199) )
  :assumption
(or (not b199)  (not b223) )
  :assumption
(or (not b199)  (not b217) )
  :assumption
(or (not b199)  (not b205) )
  :assumption
(or (not b199)  (not b202) )
  :assumption
(or (not b199)  (not b235) )
  :assumption
(or (not b199)  (not b229) )
  :assumption
(or (not b173)  (not b199) )
  :assumption
(or (not b137)  (not b199) )
  :assumption
(or (not b111)  (not b199) )
  :assumption
(or (not b89)  (not b199) )
  :assumption
(or (not b202)  (not b211) )
  :assumption
(or (not b202)  (not b208) )
  :assumption
(or (not b202)  (not b205) )
  :assumption
(or (not b179)  (not b202) )
  :assumption
(or (not b104)  (not b202) )
  :assumption
(or (not b81)  (not b202) )
  :assumption
(or (not b202)  (not b235) )
  :assumption
(or (not b202)  (not b229) )
  :assumption
(or (not b178)  (not b202) )
  :assumption
(or (not b150)  (not b202) )
  :assumption
(or (not b102)  (not b202) )
  :assumption
(or (not b78)  (not b202) )
  :assumption
(or (not b205)  (not b211) )
  :assumption
(or (not b205)  (not b208) )
  :assumption
(or (not b171)  (not b205) )
  :assumption
(or (not b126)  (not b205) )
  :assumption
(or (not b104)  (not b205) )
  :assumption
(or (not b81)  (not b205) )
  :assumption
(or (not b205)  (not b235) )
  :assumption
(or (not b205)  (not b229) )
  :assumption
(or (not b170)  (not b205) )
  :assumption
(or (not b120)  (not b205) )
  :assumption
(or (not b102)  (not b205) )
  :assumption
(or (not b78)  (not b205) )
  :assumption
(or (not b208)  (not b211) )
  :assumption
(or (not b179)  (not b208) )
  :assumption
(or (not b104)  (not b208) )
  :assumption
(or (not b81)  (not b208) )
  :assumption
(or (not b208)  (not b235) )
  :assumption
(or (not b208)  (not b229) )
  :assumption
(or (not b208)  (not b223) )
  :assumption
(or (not b208)  (not b217) )
  :assumption
(or (not b181)  (not b208) )
  :assumption
(or (not b161)  (not b208) )
  :assumption
(or (not b111)  (not b208) )
  :assumption
(or (not b89)  (not b208) )
  :assumption
(or (not b171)  (not b211) )
  :assumption
(or (not b126)  (not b211) )
  :assumption
(or (not b104)  (not b211) )
  :assumption
(or (not b81)  (not b211) )
  :assumption
(or (not b211)  (not b235) )
  :assumption
(or (not b211)  (not b229) )
  :assumption
(or (not b211)  (not b223) )
  :assumption
(or (not b211)  (not b217) )
  :assumption
(or (not b173)  (not b211) )
  :assumption
(or (not b137)  (not b211) )
  :assumption
(or (not b111)  (not b211) )
  :assumption
(or (not b89)  (not b211) )
  :assumption
(or (not b214)  (not b232) )
  :assumption
(or (not b217)  (not b235) )
  :assumption
(or (not b214)  (not b226) )
  :assumption
(or (not b217)  (not b229) )
  :assumption
(or (not b214)  (not b220) )
  :assumption
(or (not b217)  (not b223) )
  :assumption
(or (not b180)  (not b214) )
  :assumption
(or (not b181)  (not b217) )
  :assumption
(or (not b158)  (not b214) )
  :assumption
(or (not b161)  (not b217) )
  :assumption
(or (not b110)  (not b214) )
  :assumption
(or (not b111)  (not b217) )
  :assumption
(or (not b88)  (not b214) )
  :assumption
(or (not b89)  (not b217) )
  :assumption
(or (not b61)  (not b214) )
  :assumption
(or (not b29)  (not b214) )
  :assumption
(or (not b178)  (not b217) )
  :assumption
(or (not b150)  (not b217) )
  :assumption
(or (not b102)  (not b217) )
  :assumption
(or (not b78)  (not b217) )
  :assumption
(or (not b220)  (not b232) )
  :assumption
(or (not b223)  (not b235) )
  :assumption
(or (not b220)  (not b226) )
  :assumption
(or (not b223)  (not b229) )
  :assumption
(or (not b172)  (not b220) )
  :assumption
(or (not b173)  (not b223) )
  :assumption
(or (not b134)  (not b220) )
  :assumption
(or (not b137)  (not b223) )
  :assumption
(or (not b110)  (not b220) )
  :assumption
(or (not b111)  (not b223) )
  :assumption
(or (not b88)  (not b220) )
  :assumption
(or (not b89)  (not b223) )
  :assumption
(or (not b61)  (not b220) )
  :assumption
(or (not b29)  (not b220) )
  :assumption
(or (not b170)  (not b223) )
  :assumption
(or (not b120)  (not b223) )
  :assumption
(or (not b102)  (not b223) )
  :assumption
(or (not b78)  (not b223) )
  :assumption
(or (not b226)  (not b232) )
  :assumption
(or (not b229)  (not b235) )
  :assumption
(or (not b180)  (not b226) )
  :assumption
(or (not b181)  (not b229) )
  :assumption
(or (not b158)  (not b226) )
  :assumption
(or (not b161)  (not b229) )
  :assumption
(or (not b110)  (not b226) )
  :assumption
(or (not b111)  (not b229) )
  :assumption
(or (not b88)  (not b226) )
  :assumption
(or (not b89)  (not b229) )
  :assumption
(or (not b61)  (not b226) )
  :assumption
(or (not b29)  (not b226) )
  :assumption
(or (not b179)  (not b229) )
  :assumption
(or (not b104)  (not b229) )
  :assumption
(or (not b81)  (not b229) )
  :assumption
(or (not b172)  (not b232) )
  :assumption
(or (not b173)  (not b235) )
  :assumption
(or (not b134)  (not b232) )
  :assumption
(or (not b137)  (not b235) )
  :assumption
(or (not b110)  (not b232) )
  :assumption
(or (not b111)  (not b235) )
  :assumption
(or (not b88)  (not b232) )
  :assumption
(or (not b89)  (not b235) )
  :assumption
(or (not b61)  (not b232) )
  :assumption
(or (not b29)  (not b232) )
  :assumption
(or (not b171)  (not b235) )
  :assumption
(or (not b126)  (not b235) )
  :assumption
(or (not b104)  (not b235) )
  :assumption
(or (not b81)  (not b235) )
  :assumption
(or (not b238)  (not b249) )
  :assumption
(or (not b238)  (not b245) )
  :assumption
(or (not b238)  (not b242) )
  :assumption
(or (not b182)  (not b238) )
  :assumption
(or (not b163)  (not b238) )
  :assumption
(or (not b112)  (not b238) )
  :assumption
(or (not b91)  (not b238) )
  :assumption
(or (not b238)  (not b265) )
  :assumption
(or (not b238)  (not b259) )
  :assumption
(or (not b183)  (not b238) )
  :assumption
(or (not b113)  (not b238) )
  :assumption
(or (not b93)  (not b238) )
  :assumption
(or (not b242)  (not b249) )
  :assumption
(or (not b242)  (not b245) )
  :assumption
(or (not b174)  (not b242) )
  :assumption
(or (not b139)  (not b242) )
  :assumption
(or (not b112)  (not b242) )
  :assumption
(or (not b91)  (not b242) )
  :assumption
(or (not b242)  (not b265) )
  :assumption
(or (not b242)  (not b259) )
  :assumption
(or (not b175)  (not b242) )
  :assumption
(or (not b143)  (not b242) )
  :assumption
(or (not b113)  (not b242) )
  :assumption
(or (not b93)  (not b242) )
  :assumption
(or (not b245)  (not b249) )
  :assumption
(or (not b182)  (not b245) )
  :assumption
(or (not b163)  (not b245) )
  :assumption
(or (not b112)  (not b245) )
  :assumption
(or (not b91)  (not b245) )
  :assumption
(or (not b245)  (not b265) )
  :assumption
(or (not b245)  (not b259) )
  :assumption
(or (not b245)  (not b277) )
  :assumption
(or (not b245)  (not b271) )
  :assumption
(or (not b185)  (not b245) )
  :assumption
(or (not b169)  (not b245) )
  :assumption
(or (not b119)  (not b245) )
  :assumption
(or (not b100)  (not b245) )
  :assumption
(or (not b174)  (not b249) )
  :assumption
(or (not b139)  (not b249) )
  :assumption
(or (not b112)  (not b249) )
  :assumption
(or (not b91)  (not b249) )
  :assumption
(or (not b249)  (not b265) )
  :assumption
(or (not b249)  (not b259) )
  :assumption
(or (not b249)  (not b277) )
  :assumption
(or (not b249)  (not b271) )
  :assumption
(or (not b177)  (not b249) )
  :assumption
(or (not b149)  (not b249) )
  :assumption
(or (not b119)  (not b249) )
  :assumption
(or (not b100)  (not b249) )
  :assumption
(or (not b256)  (not b274) )
  :assumption
(or (not b259)  (not b277) )
  :assumption
(or (not b256)  (not b268) )
  :assumption
(or (not b259)  (not b271) )
  :assumption
(or (not b256)  (not b262) )
  :assumption
(or (not b259)  (not b265) )
  :assumption
(or (not b184)  (not b256) )
  :assumption
(or (not b185)  (not b259) )
  :assumption
(or (not b167)  (not b256) )
  :assumption
(or (not b169)  (not b259) )
  :assumption
(or (not b118)  (not b256) )
  :assumption
(or (not b119)  (not b259) )
  :assumption
(or (not b99)  (not b256) )
  :assumption
(or (not b100)  (not b259) )
  :assumption
(or (not b75)  (not b256) )
  :assumption
(or (not b43)  (not b256) )
  :assumption
(or (not b182)  (not b259) )
  :assumption
(or (not b163)  (not b259) )
  :assumption
(or (not b112)  (not b259) )
  :assumption
(or (not b91)  (not b259) )
  :assumption
(or (not b262)  (not b274) )
  :assumption
(or (not b265)  (not b277) )
  :assumption
(or (not b262)  (not b268) )
  :assumption
(or (not b265)  (not b271) )
  :assumption
(or (not b176)  (not b262) )
  :assumption
(or (not b177)  (not b265) )
  :assumption
(or (not b147)  (not b262) )
  :assumption
(or (not b149)  (not b265) )
  :assumption
(or (not b118)  (not b262) )
  :assumption
(or (not b119)  (not b265) )
  :assumption
(or (not b99)  (not b262) )
  :assumption
(or (not b100)  (not b265) )
  :assumption
(or (not b75)  (not b262) )
  :assumption
(or (not b43)  (not b262) )
  :assumption
(or (not b174)  (not b265) )
  :assumption
(or (not b139)  (not b265) )
  :assumption
(or (not b112)  (not b265) )
  :assumption
(or (not b91)  (not b265) )
  :assumption
(or (not b268)  (not b274) )
  :assumption
(or (not b271)  (not b277) )
  :assumption
(or (not b184)  (not b268) )
  :assumption
(or (not b185)  (not b271) )
  :assumption
(or (not b167)  (not b268) )
  :assumption
(or (not b169)  (not b271) )
  :assumption
(or (not b118)  (not b268) )
  :assumption
(or (not b119)  (not b271) )
  :assumption
(or (not b99)  (not b268) )
  :assumption
(or (not b100)  (not b271) )
  :assumption
(or (not b75)  (not b268) )
  :assumption
(or (not b43)  (not b268) )
  :assumption
(or (not b183)  (not b271) )
  :assumption
(or (not b113)  (not b271) )
  :assumption
(or (not b93)  (not b271) )
  :assumption
(or (not b176)  (not b274) )
  :assumption
(or (not b177)  (not b277) )
  :assumption
(or (not b147)  (not b274) )
  :assumption
(or (not b149)  (not b277) )
  :assumption
(or (not b118)  (not b274) )
  :assumption
(or (not b119)  (not b277) )
  :assumption
(or (not b99)  (not b274) )
  :assumption
(or (not b100)  (not b277) )
  :assumption
(or (not b75)  (not b274) )
  :assumption
(or (not b43)  (not b274) )
  :assumption
(or (not b175)  (not b277) )
  :assumption
(or (not b143)  (not b277) )
  :assumption
(or (not b113)  (not b277) )
  :assumption
(or (not b93)  (not b277) )
  :assumption
(or (not b280)  (not b309) )
  :assumption
(or (not b286)  (not b313) )
  :assumption
(or (not b291)  (not b317) )
  :assumption
(or (not b296)  (not b321) )
  :assumption
(or (not b301)  (not b325) )
  :assumption
(or (not b305)  (not b328) )
  :assumption
(or (not b286)  (not b382) )
  :assumption
(or (not b291)  (not b385) )
  :assumption
(or (not b296)  (not b388) )
  :assumption
(or (not b301)  (not b391) )
  :assumption
(or (not b305)  (not b394) )
  :assumption
(or (not b280)  (not b364) )
  :assumption
(or (not b286)  (not b367) )
  :assumption
(or (not b291)  (not b370) )
  :assumption
(or (not b296)  (not b373) )
  :assumption
(or (not b301)  (not b376) )
  :assumption
(or (not b305)  (not b379) )
  :assumption
(or (not b313)  (not b382) )
  :assumption
(or (not b317)  (not b385) )
  :assumption
(or (not b321)  (not b388) )
  :assumption
(or (not b325)  (not b391) )
  :assumption
(or (not b328)  (not b394) )
  :assumption
(or (not b309)  (not b364) )
  :assumption
(or (not b313)  (not b367) )
  :assumption
(or (not b317)  (not b370) )
  :assumption
(or (not b321)  (not b373) )
  :assumption
(or (not b325)  (not b376) )
  :assumption
(or (not b328)  (not b379) )
  :assumption
(or (not b313)  (not b397) )
  :assumption
(or (not b317)  (not b400) )
  :assumption
(or (not b321)  (not b403) )
  :assumption
(or (not b325)  (not b406) )
  :assumption
(or (not b328)  (not b409) )
  :assumption
(or (not b331)  (not b348) )
  :assumption
(or (not b336)  (not b351) )
  :assumption
(or (not b340)  (not b354) )
  :assumption
(or (not b344)  (not b357) )
  :assumption
(or (not b336)  (not b412) )
  :assumption
(or (not b340)  (not b415) )
  :assumption
(or (not b344)  (not b418) )
  :assumption
(or (not b331)  (not b400) )
  :assumption
(or (not b336)  (not b403) )
  :assumption
(or (not b340)  (not b406) )
  :assumption
(or (not b344)  (not b409) )
  :assumption
(or (not b331)  (not b385) )
  :assumption
(or (not b336)  (not b388) )
  :assumption
(or (not b340)  (not b391) )
  :assumption
(or (not b344)  (not b394) )
  :assumption
(or (not b351)  (not b412) )
  :assumption
(or (not b354)  (not b415) )
  :assumption
(or (not b357)  (not b418) )
  :assumption
(or (not b348)  (not b400) )
  :assumption
(or (not b351)  (not b403) )
  :assumption
(or (not b354)  (not b406) )
  :assumption
(or (not b357)  (not b409) )
  :assumption
(or (not b382)  (not b397) )
  :assumption
(or (not b385)  (not b400) )
  :assumption
(or (not b388)  (not b403) )
  :assumption
(or (not b391)  (not b406) )
  :assumption
(or (not b394)  (not b409) )
  :assumption
(or (not b421)  (not b450) )
  :assumption
(or (not b427)  (not b454) )
  :assumption
(or (not b432)  (not b458) )
  :assumption
(or (not b437)  (not b462) )
  :assumption
(or (not b442)  (not b466) )
  :assumption
(or (not b446)  (not b470) )
  :assumption
(or (not b427)  (not b524) )
  :assumption
(or (not b432)  (not b527) )
  :assumption
(or (not b437)  (not b530) )
  :assumption
(or (not b442)  (not b533) )
  :assumption
(or (not b421)  (not b506) )
  :assumption
(or (not b427)  (not b509) )
  :assumption
(or (not b432)  (not b512) )
  :assumption
(or (not b437)  (not b515) )
  :assumption
(or (not b442)  (not b518) )
  :assumption
(or (not b446)  (not b521) )
  :assumption
(or (not b454)  (not b524) )
  :assumption
(or (not b458)  (not b527) )
  :assumption
(or (not b462)  (not b530) )
  :assumption
(or (not b466)  (not b533) )
  :assumption
(or (not b450)  (not b506) )
  :assumption
(or (not b454)  (not b509) )
  :assumption
(or (not b458)  (not b512) )
  :assumption
(or (not b462)  (not b515) )
  :assumption
(or (not b466)  (not b518) )
  :assumption
(or (not b470)  (not b521) )
  :assumption
(or (not b454)  (not b537) )
  :assumption
(or (not b458)  (not b540) )
  :assumption
(or (not b462)  (not b543) )
  :assumption
(or (not b466)  (not b546) )
  :assumption
(or (not b473)  (not b490) )
  :assumption
(or (not b478)  (not b493) )
  :assumption
(or (not b482)  (not b496) )
  :assumption
(or (not b486)  (not b499) )
  :assumption
(or (not b478)  (not b550) )
  :assumption
(or (not b482)  (not b553) )
  :assumption
(or (not b486)  (not b556) )
  :assumption
(or (not b473)  (not b540) )
  :assumption
(or (not b478)  (not b543) )
  :assumption
(or (not b482)  (not b546) )
  :assumption
(or (not b473)  (not b527) )
  :assumption
(or (not b478)  (not b530) )
  :assumption
(or (not b482)  (not b533) )
  :assumption
(or (not b493)  (not b550) )
  :assumption
(or (not b496)  (not b553) )
  :assumption
(or (not b499)  (not b556) )
  :assumption
(or (not b490)  (not b540) )
  :assumption
(or (not b493)  (not b543) )
  :assumption
(or (not b496)  (not b546) )
  :assumption
(or (not b524)  (not b537) )
  :assumption
(or (not b527)  (not b540) )
  :assumption
(or (not b530)  (not b543) )
  :assumption
(or (not b533)  (not b546) )
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- r71 r67) r57) r52) r47) r32) r26) r10) r72) r73) r74) r75) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r76 r71) r58) r53) r48) r41) r37) r33) r27) r14) r77) r78) r79) r80) r81) r82) 0)
  :assumption
(= r3 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r83 r76) r62) r59) r54) r49) r42) r38) r34) r28) r22) r17) r84) r85) r86) r87) r88) r89) 0)
  :assumption
(= r4 r5)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r90 r83) r63) r60) r55) r50) r43) r39) r35) r29) r23) r20) r1) r91) r92) r93) r94) r95) 0)
  :assumption
(= (- r7 r3) 1)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r19 r90) r64) r61) r56) r51) r44) r40) r36) r30) r24) r21) r6) r96) r97) r98) r99) r100) 0)
  :assumption
(= (- r8 r7) 1)
  :assumption
(= (- r101 r16) 0)
  :assumption
(= (- r9 r8) 1)
  :assumption
(= (- r102 r101) 0)
  :assumption
(= (- r11 r9) 1)
  :assumption
(= (- r103 r102) 0)
  :assumption
(= (- r12 r11) 1)
  :assumption
(= (- r104 r103) 0)
  :assumption
(= (- r13 r12) 1)
  :assumption
(= (- r105 r104) 0)
  :assumption
(= (- r5 r13) 1)
  :assumption
(= (- (- (- (- (- (- (- (- (- r106 r105) r107) r108) r109) r110) r111) r112) r113) r114) 0)
  :assumption
(= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r18 r106) r115) r116) r117) r118) r119) r120) r121) r122) r123) r124) r125) r126) r127) r128) r129) r130) r131) r132) r133) r134) r135) r136) r137) r138) 0)
  :assumption
(= r15 0)
  :assumption
(= r16 0)
  :assumption
(<= (+ (+ (* 2 r4) (* 1 r18)) (* 3 r19)) 777)
  :assumption
(= r56 0)
  :assumption
(= r61 0)
  :assumption
(= r122 0)
  :assumption
(= r121 0)
  :assumption
(= r120 0)
  :assumption
(= r119 0)
  :assumption
(= (- (- (- r65 r15) r45) r66) 0)
  :assumption
(= (- (- (- (- (- (- (- r67 r65) r46) r31) r25) r68) r69) r70) 0)
  :formula
(not false)
)