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

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unknown
  :logic QF_LRA
  :extrapreds ((b25))
  :extrapreds ((b36))
  :extrapreds ((b47))
  :extrapreds ((b58))
  :extrapreds ((b69))
  :extrapreds ((b80))
  :extrapreds ((b91))
  :extrapreds ((b102))
  :extrapreds ((b113))
  :extrapreds ((b124))
  :extrapreds ((b135))
  :extrapreds ((b146))
  :extrapreds ((b157))
  :extrapreds ((b167))
  :extrapreds ((b177))
  :extrapreds ((b187))
  :extrapreds ((b197))
  :extrapreds ((b207))
  :extrapreds ((b217))
  :extrapreds ((b227))
  :extrapreds ((b237))
  :extrapreds ((b247))
  :extrapreds ((b257))
  :extrapreds ((b267))
  :extrapreds ((b277))
  :extrapreds ((b287))
  :extrapreds ((b297))
  :extrapreds ((b307))
  :extrapreds ((b317))
  :extrapreds ((b327))
  :extrapreds ((b337))
  :extrapreds ((b347))
  :extrapreds ((b357))
  :extrapreds ((b367))
  :extrapreds ((b377))
  :extrapreds ((b386))
  :extrapreds ((b395))
  :extrapreds ((b404))
  :extrapreds ((b413))
  :extrapreds ((b422))
  :extrapreds ((b431))
  :extrapreds ((b440))
  :extrapreds ((b449))
  :extrapreds ((b458))
  :extrapreds ((b467))
  :extrapreds ((b475))
  :extrapreds ((b482))
  :extrapreds ((b489))
  :extrapreds ((b496))
  :extrapreds ((b503))
  :extrapreds ((b510))
  :extrapreds ((b517))
  :extrapreds ((b524))
  :extrapreds ((b531))
  :extrapreds ((b538))
  :extrapreds ((b545))
  :extrapreds ((b552))
  :extrapreds ((b559))
  :extrapreds ((b566))
  :extrapreds ((b573))
  :extrapreds ((b580))
  :extrapreds ((b587))
  :extrapreds ((b594))
  :extrapreds ((b601))
  :extrapreds ((b608))
  :extrapreds ((b615))
  :extrapreds ((b622))
  :extrapreds ((b629))
  :extrapreds ((b636))
  :extrapreds ((b643))
  :extrapreds ((b650))
  :extrapreds ((b657))
  :extrapreds ((b664))
  :extrapreds ((b671))
  :extrapreds ((b678))
  :extrapreds ((b685))
  :extrapreds ((b692))
  :extrapreds ((b699))
  :extrapreds ((b706))
  :extrapreds ((b713))
  :extrapreds ((b720))
  :extrapreds ((b727))
  :extrapreds ((b734))
  :extrapreds ((b741))
  :extrapreds ((b748))
  :extrapreds ((b755))
  :extrapreds ((b762))
  :extrapreds ((b769))
  :extrapreds ((b776))
  :extrapreds ((b783))
  :extrapreds ((b789))
  :extrapreds ((b792))
  :extrapreds ((b795))
  :extrapreds ((b798))
  :extrapreds ((b801))
  :extrapreds ((b804))
  :extrapreds ((b807))
  :extrapreds ((b810))
  :extrapreds ((b813))
  :extrapreds ((b816))
  :extrapreds ((b819))
  :extrapreds ((b822))
  :extrapreds ((b825))
  :extrapreds ((b828))
  :extrapreds ((b830))
  :extrapreds ((b832))
  :extrapreds ((b834))
  :extrapreds ((b836))
  :extrapreds ((b838))
  :extrapreds ((b840))
  :extrapreds ((b842))
  :extrapreds ((b844))
  :extrapreds ((b846))
  :extrapreds ((b848))
  :extrapreds ((b850))
  :extrapreds ((b852))
  :extrapreds ((b854))
  :extrapreds ((b855))
  :extrapreds ((b856))
  :extrapreds ((b857))
  :extrapreds ((b858))
  :extrapreds ((b859))
  :extrapreds ((b860))
  :extrapreds ((b861))
  :extrapreds ((b862))
  :extrapreds ((b863))
  :extrapreds ((b864))
  :extrapreds ((b865))
  :extrapreds ((b866))
  :extrapreds ((b867))
  :extrapreds ((b868))
  :extrapreds ((b869))
  :extrapreds ((b870))
  :extrapreds ((b871))
  :extrapreds ((b872))
  :extrapreds ((b873))
  :extrapreds ((b874))
  :extrapreds ((b875))
  :extrapreds ((b876))
  :extrapreds ((b877))
  :extrapreds ((b1094))
  :extrapreds ((b1095))
  :extrapreds ((b1096))
  :extrapreds ((b1097))
  :extrapreds ((b1098))
  :extrapreds ((b1099))
  :extrapreds ((b1100))
  :extrapreds ((b1101))
  :extrapreds ((b1102))
  :extrapreds ((b1103))
  :extrapreds ((b1106))
  :extrapreds ((b1107))
  :extrapreds ((b1108))
  :extrapreds ((b1109))
  :extrapreds ((b1110))
  :extrapreds ((b1111))
  :extrapreds ((b1112))
  :extrapreds ((b1113))
  :extrapreds ((b1114))
  :extrapreds ((b1115))
  :extrapreds ((b1116))
  :extrapreds ((b1117))
  :extrapreds ((b1118))
  :extrapreds ((b1120))
  :extrapreds ((b1121))
  :extrapreds ((b1122))
  :extrapreds ((b1123))
  :extrapreds ((b1124))
  :extrapreds ((b1125))
  :extrapreds ((b1126))
  :extrapreds ((b1127))
  :extrapreds ((b1128))
  :extrapreds ((b1129))
  :extrapreds ((b1132))
  :extrapreds ((b1133))
  :extrapreds ((b1134))
  :extrapreds ((b1135))
  :extrapreds ((b1136))
  :extrapreds ((b1137))
  :extrapreds ((b1138))
  :extrapreds ((b1139))
  :extrapreds ((b1140))
  :extrapreds ((b1141))
  :extrapreds ((b1142))
  :extrapreds ((b1143))
  :extrapreds ((b1144))
  :extrapreds ((b1146))
  :extrapreds ((b1147))
  :extrapreds ((b1148))
  :extrapreds ((b1149))
  :extrapreds ((b1150))
  :extrapreds ((b1151))
  :extrapreds ((b1152))
  :extrapreds ((b1153))
  :extrapreds ((b1154))
  :extrapreds ((b1155))
  :extrapreds ((b1156))
  :extrapreds ((b1157))
  :extrapreds ((b1158))
  :extrapreds ((b1159))
  :extrapreds ((b1160))
  :extrapreds ((b1161))
  :extrapreds ((b1162))
  :extrapreds ((b1163))
  :extrapreds ((b1164))
  :extrapreds ((b1165))
  :extrapreds ((b1166))
  :extrapreds ((b1167))
  :extrapreds ((b1168))
  :extrapreds ((b1169))
  :extrapreds ((b1170))
  :extrapreds ((b1171))
  :extrapreds ((b1172))
  :extrapreds ((b1173))
  :extrapreds ((b1174))
  :extrapreds ((b1175))
  :extrapreds ((b1176))
  :extrapreds ((b1177))
  :extrapreds ((b1178))
  :extrapreds ((b1179))
  :extrapreds ((b1180))
  :extrapreds ((b1181))
  :extrapreds ((b1182))
  :extrapreds ((b1183))
  :extrapreds ((b1184))
  :extrapreds ((b1185))
  :extrapreds ((b1186))
  :extrapreds ((b1187))
  :extrapreds ((b1188))
  :extrapreds ((b1189))
  :extrapreds ((b1190))
  :extrapreds ((b1191))
  :extrapreds ((b1192))
  :extrapreds ((b1195))
  :extrapreds ((b1198))
  :extrapreds ((b1201))
  :extrapreds ((b1204))
  :extrapreds ((b1207))
  :extrapreds ((b1210))
  :extrapreds ((b1213))
  :extrapreds ((b1216))
  :extrapreds ((b1219))
  :extrapreds ((b1222))
  :extrapreds ((b1226))
  :extrapreds ((b1229))
  :extrapreds ((b1232))
  :extrapreds ((b1235))
  :extrapreds ((b1238))
  :extrapreds ((b1241))
  :extrapreds ((b1244))
  :extrapreds ((b1247))
  :extrapreds ((b1250))
  :extrapreds ((b1253))
  :extrapreds ((b1256))
  :extrapreds ((b1259))
  :extrapreds ((b1262))
  :extrapreds ((b29))
  :extrapreds ((b30))
  :extrapreds ((b31))
  :extrapreds ((b40))
  :extrapreds ((b41))
  :extrapreds ((b42))
  :extrapreds ((b51))
  :extrapreds ((b52))
  :extrapreds ((b53))
  :extrapreds ((b62))
  :extrapreds ((b63))
  :extrapreds ((b64))
  :extrapreds ((b73))
  :extrapreds ((b74))
  :extrapreds ((b75))
  :extrapreds ((b84))
  :extrapreds ((b85))
  :extrapreds ((b86))
  :extrapreds ((b95))
  :extrapreds ((b96))
  :extrapreds ((b97))
  :extrapreds ((b106))
  :extrapreds ((b107))
  :extrapreds ((b108))
  :extrapreds ((b117))
  :extrapreds ((b118))
  :extrapreds ((b119))
  :extrapreds ((b128))
  :extrapreds ((b129))
  :extrapreds ((b130))
  :extrapreds ((b139))
  :extrapreds ((b140))
  :extrapreds ((b141))
  :extrapreds ((b150))
  :extrapreds ((b151))
  :extrapreds ((b152))
  :extrapreds ((b161))
  :extrapreds ((b162))
  :extrapreds ((b171))
  :extrapreds ((b172))
  :extrapreds ((b181))
  :extrapreds ((b182))
  :extrapreds ((b191))
  :extrapreds ((b192))
  :extrapreds ((b201))
  :extrapreds ((b202))
  :extrapreds ((b211))
  :extrapreds ((b212))
  :extrapreds ((b221))
  :extrapreds ((b222))
  :extrapreds ((b231))
  :extrapreds ((b232))
  :extrapreds ((b241))
  :extrapreds ((b242))
  :extrapreds ((b251))
  :extrapreds ((b252))
  :extrapreds ((b261))
  :extrapreds ((b262))
  :extrapreds ((b271))
  :extrapreds ((b272))
  :extrapreds ((b281))
  :extrapreds ((b282))
  :extrapreds ((b291))
  :extrapreds ((b292))
  :extrapreds ((b301))
  :extrapreds ((b302))
  :extrapreds ((b311))
  :extrapreds ((b312))
  :extrapreds ((b321))
  :extrapreds ((b322))
  :extrapreds ((b331))
  :extrapreds ((b332))
  :extrapreds ((b341))
  :extrapreds ((b342))
  :extrapreds ((b351))
  :extrapreds ((b352))
  :extrapreds ((b361))
  :extrapreds ((b362))
  :extrapreds ((b371))
  :extrapreds ((b372))
  :extrapreds ((b381))
  :extrapreds ((b390))
  :extrapreds ((b399))
  :extrapreds ((b408))
  :extrapreds ((b417))
  :extrapreds ((b426))
  :extrapreds ((b435))
  :extrapreds ((b444))
  :extrapreds ((b453))
  :extrapreds ((b462))
  :extrapreds ((b471))
  :extrapreds ((b790))
  :extrapreds ((b791))
  :extrapreds ((b793))
  :extrapreds ((b794))
  :extrapreds ((b796))
  :extrapreds ((b797))
  :extrapreds ((b799))
  :extrapreds ((b800))
  :extrapreds ((b802))
  :extrapreds ((b803))
  :extrapreds ((b805))
  :extrapreds ((b806))
  :extrapreds ((b808))
  :extrapreds ((b809))
  :extrapreds ((b811))
  :extrapreds ((b812))
  :extrapreds ((b814))
  :extrapreds ((b815))
  :extrapreds ((b817))
  :extrapreds ((b818))
  :extrapreds ((b820))
  :extrapreds ((b821))
  :extrapreds ((b823))
  :extrapreds ((b824))
  :extrapreds ((b826))
  :extrapreds ((b827))
  :extrapreds ((b829))
  :extrapreds ((b831))
  :extrapreds ((b833))
  :extrapreds ((b835))
  :extrapreds ((b837))
  :extrapreds ((b839))
  :extrapreds ((b841))
  :extrapreds ((b843))
  :extrapreds ((b845))
  :extrapreds ((b847))
  :extrapreds ((b849))
  :extrapreds ((b851))
  :extrapreds ((b853))
  :extrapreds ((b879))
  :extrapreds ((b886))
  :extrapreds ((b895))
  :extrapreds ((b904))
  :extrapreds ((b913))
  :extrapreds ((b922))
  :extrapreds ((b931))
  :extrapreds ((b940))
  :extrapreds ((b949))
  :extrapreds ((b958))
  :extrapreds ((b967))
  :extrapreds ((b976))
  :extrapreds ((b987))
  :extrapreds ((b994))
  :extrapreds ((b1003))
  :extrapreds ((b1012))
  :extrapreds ((b1021))
  :extrapreds ((b1030))
  :extrapreds ((b1039))
  :extrapreds ((b1048))
  :extrapreds ((b1057))
  :extrapreds ((b1066))
  :extrapreds ((b1075))
  :extrapreds ((b1084))
  :extrapreds ((b1104))
  :extrapreds ((b1105))
  :extrapreds ((b1119))
  :extrapreds ((b1130))
  :extrapreds ((b1131))
  :extrapreds ((b1145))
  :extrapreds ((b1194))
  :extrapreds ((b1197))
  :extrapreds ((b1200))
  :extrapreds ((b1203))
  :extrapreds ((b1206))
  :extrapreds ((b1209))
  :extrapreds ((b1212))
  :extrapreds ((b1215))
  :extrapreds ((b1218))
  :extrapreds ((b1221))
  :extrapreds ((b1224))
  :extrapreds ((b1225))
  :extrapreds ((b1228))
  :extrapreds ((b1231))
  :extrapreds ((b1234))
  :extrapreds ((b1237))
  :extrapreds ((b1240))
  :extrapreds ((b1243))
  :extrapreds ((b1246))
  :extrapreds ((b1249))
  :extrapreds ((b1252))
  :extrapreds ((b1255))
  :extrapreds ((b1258))
  :extrapreds ((b1261))
  :extrapreds ((b1264))
  :extrapreds ((b1265))
  :extrapreds ((b1267))
  :extrapreds ((b1274))
  :extrapreds ((b1283))
  :extrapreds ((b1292))
  :extrapreds ((b1301))
  :extrapreds ((b1310))
  :extrapreds ((b1319))
  :extrapreds ((b1328))
  :extrapreds ((b1337))
  :extrapreds ((b1346))
  :extrapreds ((b1355))
  :extrapreds ((b1364))
  :extrapreds ((b1375))
  :extrapreds ((b1383))
  :extrapreds ((b1392))
  :extrapreds ((b1401))
  :extrapreds ((b1410))
  :extrapreds ((b1419))
  :extrapreds ((b1428))
  :extrapreds ((b1437))
  :extrapreds ((b1446))
  :extrapreds ((b1455))
  :extrapreds ((b1465))
  :extrapreds ((b1470))
  :extrapreds ((b1474))
  :extrapreds ((b1478))
  :extrapreds ((b1482))
  :extrapreds ((b1486))
  :extrapreds ((b1490))
  :extrapreds ((b1494))
  :extrapreds ((b1498))
  :extrapreds ((b1502))
  :extrapreds ((b1506))
  :extrapreds ((b1510))
  :extrapreds ((b1513))
  :extrapreds ((b1516))
  :extrapreds ((b1519))
  :extrapreds ((b1522))
  :extrapreds ((b1525))
  :extrapreds ((b1528))
  :extrapreds ((b1531))
  :extrapreds ((b1534))
  :extrafuns ((r1 Real))
  :extrafuns ((r2 Real))
  :extrafuns ((r3 Real))
  :extrafuns ((r4 Real))
  :extrafuns ((r5 Real))
  :extrafuns ((r6 Real))
  :extrafuns ((r7 Real))
  :extrafuns ((r8 Real))
  :extrafuns ((r9 Real))
  :extrafuns ((r10 Real))
  :extrafuns ((r11 Real))
  :extrafuns ((r12 Real))
  :extrafuns ((r13 Real))
  :extrafuns ((r14 Real))
  :extrafuns ((r15 Real))
  :extrafuns ((r16 Real))
  :extrafuns ((r17 Real))
  :extrafuns ((r18 Real))
  :extrafuns ((r19 Real))
  :extrafuns ((r20 Real))
  :extrafuns ((r21 Real))
  :extrafuns ((r22 Real))
  :extrafuns ((r23 Real))
  :extrafuns ((r24 Real))
  :extrafuns ((r25 Real))
  :extrafuns ((r26 Real))
  :extrafuns ((r27 Real))
  :extrafuns ((r28 Real))
  :extrafuns ((r29 Real))
  :extrafuns ((r30 Real))
  :extrafuns ((r31 Real))
  :extrafuns ((r32 Real))
  :extrafuns ((r33 Real))
  :extrafuns ((r34 Real))
  :extrafuns ((r35 Real))
  :extrafuns ((r36 Real))
  :extrafuns ((r37 Real))
  :extrafuns ((r38 Real))
  :extrafuns ((r39 Real))
  :extrafuns ((r40 Real))
  :extrafuns ((r41 Real))
  :extrafuns ((r42 Real))
  :extrafuns ((r43 Real))
  :extrafuns ((r44 Real))
  :extrafuns ((r45 Real))
  :extrafuns ((r46 Real))
  :extrafuns ((r47 Real))
  :extrafuns ((r48 Real))
  :extrafuns ((r49 Real))
  :extrafuns ((r50 Real))
  :extrafuns ((r51 Real))
  :extrafuns ((r52 Real))
  :extrafuns ((r53 Real))
  :extrafuns ((r54 Real))
  :extrafuns ((r55 Real))
  :extrafuns ((r56 Real))
  :extrafuns ((r57 Real))
  :extrafuns ((r58 Real))
  :extrafuns ((r59 Real))
  :extrafuns ((r60 Real))
  :extrafuns ((r61 Real))
  :extrafuns ((r62 Real))
  :extrafuns ((r63 Real))
  :extrafuns ((r64 Real))
  :extrafuns ((r65 Real))
  :extrafuns ((r66 Real))
  :extrafuns ((r67 Real))
  :extrafuns ((r68 Real))
  :extrafuns ((r69 Real))
  :extrafuns ((r70 Real))
  :extrafuns ((r71 Real))
  :extrafuns ((r72 Real))
  :extrafuns ((r73 Real))
  :extrafuns ((r74 Real))
  :extrafuns ((r75 Real))
  :extrafuns ((r76 Real))
  :extrafuns ((r77 Real))
  :extrafuns ((r78 Real))
  :extrafuns ((r79 Real))
  :extrafuns ((r80 Real))
  :extrafuns ((r81 Real))
  :extrafuns ((r82 Real))
  :extrafuns ((r83 Real))
  :extrafuns ((r84 Real))
  :extrafuns ((r85 Real))
  :extrafuns ((r86 Real))
  :extrafuns ((r87 Real))
  :extrafuns ((r88 Real))
  :extrafuns ((r89 Real))
  :extrafuns ((r90 Real))
  :extrafuns ((r91 Real))
  :extrafuns ((r92 Real))
  :extrafuns ((r93 Real))
  :extrafuns ((r94 Real))
  :extrafuns ((r95 Real))
  :extrafuns ((r96 Real))
  :extrafuns ((r97 Real))
  :extrafuns ((r98 Real))
  :extrafuns ((r99 Real))
  :extrafuns ((r100 Real))
  :extrafuns ((r101 Real))
  :extrafuns ((r102 Real))
  :extrafuns ((r103 Real))
  :extrafuns ((r104 Real))
  :extrafuns ((r105 Real))
  :extrafuns ((r106 Real))
  :extrafuns ((r107 Real))
  :extrafuns ((r108 Real))
  :extrafuns ((r109 Real))
  :extrafuns ((r110 Real))
  :extrafuns ((r111 Real))
  :extrafuns ((r112 Real))
  :extrafuns ((r113 Real))
  :extrafuns ((r114 Real))
  :extrafuns ((r115 Real))
  :extrafuns ((r116 Real))
  :extrafuns ((r117 Real))
  :extrafuns ((r118 Real))
  :extrafuns ((r119 Real))
  :extrafuns ((r120 Real))
  :extrafuns ((r121 Real))
  :extrafuns ((r122 Real))
  :extrafuns ((r123 Real))
  :extrafuns ((r124 Real))
  :extrafuns ((r125 Real))
  :extrafuns ((r126 Real))
  :extrafuns ((r127 Real))
  :extrafuns ((r128 Real))
  :extrafuns ((r129 Real))
  :extrafuns ((r130 Real))
  :extrafuns ((r131 Real))
  :extrafuns ((r132 Real))
  :extrafuns ((r133 Real))
  :extrafuns ((r134 Real))
  :extrafuns ((r135 Real))
  :extrafuns ((r136 Real))
  :extrafuns ((r137 Real))
  :extrafuns ((r138 Real))
  :extrafuns ((r139 Real))
  :extrafuns ((r140 Real))
  :extrafuns ((r141 Real))
  :extrafuns ((r142 Real))
  :extrafuns ((r143 Real))
  :extrafuns ((r144 Real))
  :extrafuns ((r145 Real))
  :extrafuns ((r146 Real))
  :extrafuns ((r147 Real))
  :extrafuns ((r148 Real))
  :extrafuns ((r149 Real))
  :extrafuns ((r150 Real))
  :extrafuns ((r151 Real))
  :extrafuns ((r152 Real))
  :extrafuns ((r153 Real))
  :extrafuns ((r154 Real))
  :extrafuns ((r155 Real))
  :extrafuns ((r156 Real))
  :extrafuns ((r157 Real))
  :extrafuns ((r158 Real))
  :extrafuns ((r159 Real))
  :extrafuns ((r160 Real))
  :extrafuns ((r161 Real))
  :extrafuns ((r162 Real))
  :extrafuns ((r163 Real))
  :extrafuns ((r164 Real))
  :extrafuns ((r165 Real))
  :extrafuns ((r166 Real))
  :extrafuns ((r167 Real))
  :extrafuns ((r168 Real))
  :extrafuns ((r169 Real))
  :extrafuns ((r170 Real))
  :extrafuns ((r171 Real))
  :extrafuns ((r172 Real))
  :extrafuns ((r173 Real))
  :extrafuns ((r174 Real))
  :extrafuns ((r175 Real))
  :extrafuns ((r176 Real))
  :extrafuns ((r177 Real))
  :extrafuns ((r178 Real))
  :extrafuns ((r179 Real))
  :extrafuns ((r180 Real))
  :extrafuns ((r181 Real))
  :extrafuns ((r182 Real))
  :extrafuns ((r183 Real))
  :extrafuns ((r184 Real))
  :extrafuns ((r185 Real))
  :extrafuns ((r186 Real))
  :extrafuns ((r187 Real))
  :extrafuns ((r188 Real))
  :extrafuns ((r189 Real))
  :extrafuns ((r190 Real))
  :extrafuns ((r191 Real))
  :extrafuns ((r192 Real))
  :extrafuns ((r193 Real))
  :extrafuns ((r194 Real))
  :extrafuns ((r195 Real))
  :extrafuns ((r196 Real))
  :extrafuns ((r197 Real))
  :extrafuns ((r198 Real))
  :extrafuns ((r199 Real))
  :extrafuns ((r200 Real))
  :extrafuns ((r201 Real))
  :extrafuns ((r202 Real))
  :extrafuns ((r203 Real))
  :extrafuns ((r204 Real))
  :extrafuns ((r205 Real))
  :extrafuns ((r206 Real))
  :extrafuns ((r207 Real))
  :extrafuns ((r208 Real))
  :extrafuns ((r209 Real))
  :extrafuns ((r210 Real))
  :extrafuns ((r211 Real))
  :extrafuns ((r212 Real))
  :extrafuns ((r213 Real))
  :extrafuns ((r214 Real))
  :extrafuns ((r215 Real))
  :extrafuns ((r216 Real))
  :extrafuns ((r217 Real))
  :extrafuns ((r218 Real))
  :extrafuns ((r219 Real))
  :extrafuns ((r220 Real))
  :extrafuns ((r221 Real))
  :extrafuns ((r222 Real))
  :extrafuns ((r223 Real))
  :extrafuns ((r224 Real))
  :extrafuns ((r225 Real))
  :extrafuns ((r226 Real))
  :extrafuns ((r227 Real))
  :extrafuns ((r228 Real))
  :extrafuns ((r229 Real))
  :extrafuns ((r230 Real))
  :extrafuns ((r231 Real))
  :extrafuns ((r232 Real))
  :extrafuns ((r233 Real))
  :extrafuns ((r234 Real))
  :extrafuns ((r235 Real))
  :extrafuns ((r236 Real))
  :extrafuns ((r237 Real))
  :extrafuns ((r238 Real))
  :extrafuns ((r239 Real))
  :extrafuns ((r240 Real))
  :extrafuns ((r241 Real))
  :extrafuns ((r242 Real))
  :extrafuns ((r243 Real))
  :extrafuns ((r244 Real))
  :extrafuns ((r245 Real))
  :extrafuns ((r246 Real))
  :extrafuns ((r247 Real))
  :extrafuns ((r248 Real))
  :extrafuns ((r249 Real))
  :extrafuns ((r250 Real))
  :extrafuns ((r251 Real))
  :extrafuns ((r252 Real))
  :extrafuns ((r253 Real))
  :extrafuns ((r254 Real))
  :extrafuns ((r255 Real))
  :extrafuns ((r256 Real))
  :extrafuns ((r257 Real))
  :extrafuns ((r258 Real))
  :extrafuns ((r259 Real))
  :extrafuns ((r260 Real))
  :extrafuns ((r261 Real))
  :extrafuns ((r262 Real))
  :extrafuns ((r263 Real))
  :extrafuns ((r264 Real))
  :extrafuns ((r265 Real))
  :extrafuns ((r266 Real))
  :extrafuns ((r267 Real))
  :extrafuns ((r268 Real))
  :extrafuns ((r269 Real))
  :extrafuns ((r270 Real))
  :extrafuns ((r271 Real))
  :extrafuns ((r272 Real))
  :extrafuns ((r273 Real))
  :extrafuns ((r274 Real))
  :extrafuns ((r275 Real))
  :extrafuns ((r276 Real))
  :extrafuns ((r277 Real))
  :extrafuns ((r278 Real))
  :extrafuns ((r279 Real))
  :extrafuns ((r280 Real))
  :extrafuns ((r281 Real))
  :extrafuns ((r282 Real))
  :extrafuns ((r283 Real))
  :extrafuns ((r284 Real))
  :extrafuns ((r285 Real))
  :extrafuns ((r286 Real))
  :extrafuns ((r287 Real))
  :extrafuns ((r288 Real))
  :extrafuns ((r289 Real))
  :extrafuns ((r290 Real))
  :extrafuns ((r291 Real))
  :extrafuns ((r292 Real))
  :extrafuns ((r293 Real))
  :extrafuns ((r294 Real))
  :extrafuns ((r295 Real))
  :extrafuns ((r296 Real))
  :extrafuns ((r297 Real))
  :extrafuns ((r298 Real))
  :extrafuns ((r299 Real))
  :extrafuns ((r300 Real))
  :extrafuns ((r301 Real))
  :extrafuns ((r302 Real))
  :extrafuns ((r303 Real))
  :extrafuns ((r304 Real))
  :extrafuns ((r305 Real))
  :extrafuns ((r306 Real))
  :extrafuns ((r307 Real))
  :extrafuns ((r308 Real))
  :extrafuns ((r309 Real))
  :extrafuns ((r310 Real))
  :extrafuns ((r311 Real))
  :extrafuns ((r312 Real))
  :extrafuns ((r313 Real))
  :extrafuns ((r314 Real))
  :extrafuns ((r315 Real))
  :extrafuns ((r316 Real))
  :extrafuns ((r317 Real))
  :extrafuns ((r318 Real))
  :extrafuns ((r319 Real))
  :extrafuns ((r320 Real))
  :extrafuns ((r321 Real))
  :extrafuns ((r322 Real))
  :extrafuns ((r323 Real))
  :extrafuns ((r324 Real))
  :extrafuns ((r325 Real))
  :extrafuns ((r326 Real))
  :extrafuns ((r327 Real))
  :extrafuns ((r328 Real))
  :extrafuns ((r329 Real))
  :extrafuns ((r330 Real))
  :extrafuns ((r331 Real))
  :extrafuns ((r332 Real))
  :extrafuns ((r333 Real))
  :extrafuns ((r334 Real))
  :extrafuns ((r335 Real))
  :extrafuns ((r336 Real))
  :extrafuns ((r337 Real))
  :extrafuns ((r338 Real))
  :extrafuns ((r339 Real))
  :extrafuns ((r340 Real))
  :extrafuns ((r341 Real))
  :extrafuns ((r342 Real))
  :extrafuns ((r343 Real))
  :extrafuns ((r344 Real))
  :extrafuns ((r345 Real))
  :extrafuns ((r346 Real))
  :extrafuns ((r347 Real))
  :extrafuns ((r348 Real))
  :extrafuns ((r349 Real))
  :extrafuns ((r350 Real))
  :extrafuns ((r351 Real))
  :extrafuns ((r352 Real))
  :extrafuns ((r353 Real))
  :extrafuns ((r354 Real))
  :extrafuns ((r355 Real))
  :extrafuns ((r356 Real))
  :extrafuns ((r357 Real))
  :extrafuns ((r358 Real))
  :extrafuns ((r359 Real))
  :extrafuns ((r360 Real))
  :extrafuns ((r361 Real))
  :extrafuns ((r362 Real))
  :extrafuns ((r363 Real))
  :extrafuns ((r364 Real))
  :extrafuns ((r365 Real))
  :extrafuns ((r366 Real))
  :extrafuns ((r367 Real))
  :extrafuns ((r368 Real))
  :extrafuns ((r369 Real))
  :extrafuns ((r370 Real))
  :extrafuns ((r371 Real))
  :extrafuns ((r372 Real))
  :extrafuns ((r373 Real))
  :extrafuns ((r374 Real))
  :extrafuns ((r375 Real))
  :extrafuns ((r376 Real))
  :extrafuns ((r377 Real))
  :extrafuns ((r378 Real))
  :extrafuns ((r379 Real))
  :extrafuns ((r380 Real))
  :extrafuns ((r381 Real))
  :extrafuns ((r382 Real))
  :extrafuns ((r383 Real))
  :extrafuns ((r384 Real))
  :extrafuns ((r385 Real))
  :extrafuns ((r386 Real))
  :extrafuns ((r387 Real))
  :extrafuns ((r388 Real))
  :extrafuns ((r389 Real))
  :extrafuns ((r390 Real))
  :extrafuns ((r391 Real))
  :extrafuns ((r392 Real))
  :extrafuns ((r393 Real))
  :extrafuns ((r394 Real))
  :extrafuns ((r395 Real))
  :extrafuns ((r396 Real))
  :extrafuns ((r397 Real))
  :extrafuns ((r398 Real))
  :extrafuns ((r399 Real))
  :extrafuns ((r400 Real))
  :extrafuns ((r401 Real))
  :extrafuns ((r402 Real))
  :extrafuns ((r403 Real))
  :extrafuns ((r404 Real))
  :extrafuns ((r405 Real))
  :extrafuns ((r406 Real))
  :extrafuns ((r407 Real))
  :extrafuns ((r408 Real))
  :extrafuns ((r409 Real))
  :extrafuns ((r410 Real))
  :extrafuns ((r411 Real))
  :extrafuns ((r412 Real))
  :extrafuns ((r413 Real))
  :extrafuns ((r414 Real))
  :extrafuns ((r415 Real))
  :extrafuns ((r416 Real))
  :extrafuns ((r417 Real))
  :extrafuns ((r418 Real))
  :extrafuns ((r419 Real))
  :extrafuns ((r420 Real))
  :extrafuns ((r421 Real))
  :extrafuns ((r422 Real))
  :extrafuns ((r423 Real))
  :extrafuns ((r424 Real))
  :extrafuns ((r425 Real))
  :extrafuns ((r426 Real))
  :extrafuns ((r427 Real))
  :extrafuns ((r428 Real))
  :extrafuns ((r429 Real))
  :extrafuns ((r430 Real))
  :extrafuns ((r431 Real))
  :extrafuns ((r432 Real))
  :extrafuns ((r433 Real))
  :extrafuns ((r434 Real))
  :extrafuns ((r435 Real))
  :extrafuns ((r436 Real))
  :extrafuns ((r437 Real))
  :extrafuns ((r438 Real))
  :extrafuns ((r439 Real))
  :extrafuns ((r440 Real))
  :extrafuns ((r441 Real))
  :extrafuns ((r442 Real))
  :extrafuns ((r443 Real))
  :extrafuns ((r444 Real))
  :extrafuns ((r445 Real))
  :extrafuns ((r446 Real))
  :extrafuns ((r447 Real))
  :extrafuns ((r448 Real))
  :extrafuns ((r449 Real))
  :extrafuns ((r450 Real))
  :extrafuns ((r451 Real))
  :extrafuns ((r452 Real))
  :extrafuns ((r453 Real))
  :extrafuns ((r454 Real))
  :extrafuns ((r455 Real))
  :extrafuns ((r456 Real))
  :extrafuns ((r457 Real))
  :extrafuns ((r458 Real))
  :extrafuns ((r459 Real))
  :extrafuns ((r460 Real))
  :extrafuns ((r461 Real))
  :extrafuns ((r462 Real))
  :extrafuns ((r463 Real))
  :extrafuns ((r464 Real))
  :extrafuns ((r465 Real))
  :extrafuns ((r466 Real))
  :extrafuns ((r467 Real))
  :extrafuns ((r468 Real))
  :extrafuns ((r469 Real))
  :extrafuns ((r470 Real))
  :extrafuns ((r471 Real))
  :extrafuns ((r472 Real))
  :extrafuns ((r473 Real))
  :extrafuns ((r474 Real))
  :extrafuns ((r475 Real))
  :extrafuns ((r476 Real))
  :extrafuns ((r477 Real))
  :extrafuns ((r478 Real))
  :extrafuns ((r479 Real))
  :extrafuns ((r480 Real))
  :extrafuns ((r481 Real))
  :extrafuns ((r482 Real))
  :extrafuns ((r483 Real))
  :extrafuns ((r484 Real))
  :extrafuns ((r485 Real))
  :extrafuns ((r486 Real))
  :extrafuns ((r487 Real))
  :extrafuns ((r488 Real))
  :extrafuns ((r489 Real))
  :extrafuns ((r490 Real))
  :extrafuns ((r491 Real))
  :extrafuns ((r492 Real))
  :extrafuns ((r493 Real))
  :extrafuns ((r494 Real))
  :extrafuns ((r495 Real))
  :extrafuns ((r496 Real))
  :extrafuns ((r497 Real))
  :assumption
(or (= r180 0)  b25 )
  :assumption
(or b25  (= r79 0) )
  :assumption
(or (not b25)  (= r79 r193) )
  :assumption
(or (not b25)  (= r180 (~ r193)) )
  :assumption
(or (not b25)  b29 )
  :assumption
(or (not b25)  b30 )
  :assumption
(or (not b25)  b31 )
  :assumption
(or (not b25)  (> r193 0) )
  :assumption
(or (not b25)  (<= r193 r215) )
  :assumption
(or (not b25)  (<= r193 (- 4 r73)) )
  :assumption
(or (= r224 0)  b36 )
  :assumption
(or b36  (= r88 0) )
  :assumption
(or (not b36)  (= r88 r237) )
  :assumption
(or (not b36)  (= r224 (~ r237)) )
  :assumption
(or (not b36)  b40 )
  :assumption
(or (not b36)  b41 )
  :assumption
(or (not b36)  b42 )
  :assumption
(or (not b36)  (> r237 0) )
  :assumption
(or (not b36)  (<= r237 r262) )
  :assumption
(or (not b36)  (<= r237 (- 4 r82)) )
  :assumption
(or (= r269 0)  b47 )
  :assumption
(or b47  (= r97 0) )
  :assumption
(or (not b47)  (= r97 r276) )
  :assumption
(or (not b47)  (= r269 (~ r276)) )
  :assumption
(or (not b47)  b51 )
  :assumption
(or (not b47)  b52 )
  :assumption
(or (not b47)  b53 )
  :assumption
(or (not b47)  (> r276 0) )
  :assumption
(or (not b47)  (<= r276 r289) )
  :assumption
(or (not b47)  (<= r276 (- 4 r91)) )
  :assumption
(or (= r294 0)  b58 )
  :assumption
(or b58  (= r106 0) )
  :assumption
(or (not b58)  (= r106 r301) )
  :assumption
(or (not b58)  (= r294 (~ r301)) )
  :assumption
(or (not b58)  b62 )
  :assumption
(or (not b58)  b63 )
  :assumption
(or (not b58)  b64 )
  :assumption
(or (not b58)  (> r301 0) )
  :assumption
(or (not b58)  (<= r301 r314) )
  :assumption
(or (not b58)  (<= r301 (- 4 r100)) )
  :assumption
(or (= r8 0)  b69 )
  :assumption
(or b69  (= r115 0) )
  :assumption
(or (not b69)  (= r115 r325) )
  :assumption
(or (not b69)  (= r8 (~ r325)) )
  :assumption
(or (not b69)  b73 )
  :assumption
(or (not b69)  b74 )
  :assumption
(or (not b69)  b75 )
  :assumption
(or (not b69)  (> r325 0) )
  :assumption
(or (not b69)  (<= r325 r2) )
  :assumption
(or (not b69)  (<= r325 (- 4 r109)) )
  :assumption
(or (= r17 0)  b80 )
  :assumption
(or b80  (= r124 0) )
  :assumption
(or (not b80)  (= r124 r346) )
  :assumption
(or (not b80)  (= r17 (~ r346)) )
  :assumption
(or (not b80)  b84 )
  :assumption
(or (not b80)  b85 )
  :assumption
(or (not b80)  b86 )
  :assumption
(or (not b80)  (> r346 0) )
  :assumption
(or (not b80)  (<= r346 r11) )
  :assumption
(or (not b80)  (<= r346 (- 4 r118)) )
  :assumption
(or (= r27 0)  b91 )
  :assumption
(or b91  (= r132 0) )
  :assumption
(or (not b91)  (= r132 r357) )
  :assumption
(or (not b91)  (= r27 (~ r357)) )
  :assumption
(or (not b91)  b95 )
  :assumption
(or (not b91)  b96 )
  :assumption
(or (not b91)  b97 )
  :assumption
(or (not b91)  (> r357 0) )
  :assumption
(or (not b91)  (<= r357 r21) )
  :assumption
(or (not b91)  (<= r357 (- 4 r126)) )
  :assumption
(or (= r36 0)  b102 )
  :assumption
(or b102  (= r141 0) )
  :assumption
(or (not b102)  (= r141 r362) )
  :assumption
(or (not b102)  (= r36 (~ r362)) )
  :assumption
(or (not b102)  b106 )
  :assumption
(or (not b102)  b107 )
  :assumption
(or (not b102)  b108 )
  :assumption
(or (not b102)  (> r362 0) )
  :assumption
(or (not b102)  (<= r362 r30) )
  :assumption
(or (not b102)  (<= r362 (- 4 r135)) )
  :assumption
(or (= r45 0)  b113 )
  :assumption
(or b113  (= r150 0) )
  :assumption
(or (not b113)  (= r150 r363) )
  :assumption
(or (not b113)  (= r45 (~ r363)) )
  :assumption
(or (not b113)  b117 )
  :assumption
(or (not b113)  b118 )
  :assumption
(or (not b113)  b119 )
  :assumption
(or (not b113)  (> r363 0) )
  :assumption
(or (not b113)  (<= r363 r39) )
  :assumption
(or (not b113)  (<= r363 (- 4 r144)) )
  :assumption
(or (= r54 0)  b124 )
  :assumption
(or b124  (= r159 0) )
  :assumption
(or (not b124)  (= r159 r366) )
  :assumption
(or (not b124)  (= r54 (~ r366)) )
  :assumption
(or (not b124)  b128 )
  :assumption
(or (not b124)  b129 )
  :assumption
(or (not b124)  b130 )
  :assumption
(or (not b124)  (> r366 0) )
  :assumption
(or (not b124)  (<= r366 r48) )
  :assumption
(or (not b124)  (<= r366 (- 4 r153)) )
  :assumption
(or (= r375 0)  b135 )
  :assumption
(or b135  (= r63 0) )
  :assumption
(or (not b135)  (= r63 r378) )
  :assumption
(or (not b135)  (= r375 (~ r378)) )
  :assumption
(or (not b135)  b139 )
  :assumption
(or (not b135)  b140 )
  :assumption
(or (not b135)  b141 )
  :assumption
(or (not b135)  (> r378 0) )
  :assumption
(or (not b135)  (<= r378 r327) )
  :assumption
(or (not b135)  (<= r378 (- 4 r60)) )
  :assumption
(or (= r385 0)  b146 )
  :assumption
(or b146  (= r70 0) )
  :assumption
(or (not b146)  (= r70 r389) )
  :assumption
(or (not b146)  (= r385 (~ r389)) )
  :assumption
(or (not b146)  b150 )
  :assumption
(or (not b146)  b151 )
  :assumption
(or (not b146)  b152 )
  :assumption
(or (not b146)  (> r389 0) )
  :assumption
(or (not b146)  (<= r389 r330) )
  :assumption
(or (not b146)  (<= r389 (- 4 r66)) )
  :assumption
(or (= r391 0)  b157 )
  :assumption
(or b157  (= r78 0) )
  :assumption
(or (not b157)  (= r78 r392) )
  :assumption
(or (not b157)  (= r391 (~ r392)) )
  :assumption
(or (not b157)  b161 )
  :assumption
(or b30  (not b157) )
  :assumption
(or (not b157)  b162 )
  :assumption
(or (not b157)  (> r392 0) )
  :assumption
(or (not b157)  (<= r392 r215) )
  :assumption
(or (not b157)  (<= r392 (- 4 r73)) )
  :assumption
(or (= r393 0)  b167 )
  :assumption
(or b167  (= r87 0) )
  :assumption
(or (not b167)  (= r87 r394) )
  :assumption
(or (not b167)  (= r393 (~ r394)) )
  :assumption
(or (not b167)  b171 )
  :assumption
(or b41  (not b167) )
  :assumption
(or (not b167)  b172 )
  :assumption
(or (not b167)  (> r394 0) )
  :assumption
(or (not b167)  (<= r394 r262) )
  :assumption
(or (not b167)  (<= r394 (- 4 r82)) )
  :assumption
(or (= r395 0)  b177 )
  :assumption
(or b177  (= r96 0) )
  :assumption
(or (not b177)  (= r96 r396) )
  :assumption
(or (not b177)  (= r395 (~ r396)) )
  :assumption
(or (not b177)  b181 )
  :assumption
(or b52  (not b177) )
  :assumption
(or (not b177)  b182 )
  :assumption
(or (not b177)  (> r396 0) )
  :assumption
(or (not b177)  (<= r396 r289) )
  :assumption
(or (not b177)  (<= r396 (- 4 r91)) )
  :assumption
(or (= r397 0)  b187 )
  :assumption
(or b187  (= r105 0) )
  :assumption
(or (not b187)  (= r105 r398) )
  :assumption
(or (not b187)  (= r397 (~ r398)) )
  :assumption
(or (not b187)  b191 )
  :assumption
(or b63  (not b187) )
  :assumption
(or (not b187)  b192 )
  :assumption
(or (not b187)  (> r398 0) )
  :assumption
(or (not b187)  (<= r398 r314) )
  :assumption
(or (not b187)  (<= r398 (- 4 r100)) )
  :assumption
(or (= r7 0)  b197 )
  :assumption
(or b197  (= r114 0) )
  :assumption
(or (not b197)  (= r114 r399) )
  :assumption
(or (not b197)  (= r7 (~ r399)) )
  :assumption
(or (not b197)  b201 )
  :assumption
(or b74  (not b197) )
  :assumption
(or (not b197)  b202 )
  :assumption
(or (not b197)  (> r399 0) )
  :assumption
(or (not b197)  (<= r399 r2) )
  :assumption
(or (not b197)  (<= r399 (- 4 r109)) )
  :assumption
(or (= r16 0)  b207 )
  :assumption
(or b207  (= r123 0) )
  :assumption
(or (not b207)  (= r123 r400) )
  :assumption
(or (not b207)  (= r16 (~ r400)) )
  :assumption
(or (not b207)  b211 )
  :assumption
(or b85  (not b207) )
  :assumption
(or (not b207)  b212 )
  :assumption
(or (not b207)  (> r400 0) )
  :assumption
(or (not b207)  (<= r400 r11) )
  :assumption
(or (not b207)  (<= r400 (- 4 r118)) )
  :assumption
(or (= r26 0)  b217 )
  :assumption
(or b217  (= r131 0) )
  :assumption
(or (not b217)  (= r131 r401) )
  :assumption
(or (not b217)  (= r26 (~ r401)) )
  :assumption
(or (not b217)  b221 )
  :assumption
(or b96  (not b217) )
  :assumption
(or (not b217)  b222 )
  :assumption
(or (not b217)  (> r401 0) )
  :assumption
(or (not b217)  (<= r401 r21) )
  :assumption
(or (not b217)  (<= r401 (- 4 r126)) )
  :assumption
(or (= r35 0)  b227 )
  :assumption
(or b227  (= r140 0) )
  :assumption
(or (not b227)  (= r140 r402) )
  :assumption
(or (not b227)  (= r35 (~ r402)) )
  :assumption
(or (not b227)  b231 )
  :assumption
(or b107  (not b227) )
  :assumption
(or (not b227)  b232 )
  :assumption
(or (not b227)  (> r402 0) )
  :assumption
(or (not b227)  (<= r402 r30) )
  :assumption
(or (not b227)  (<= r402 (- 4 r135)) )
  :assumption
(or (= r44 0)  b237 )
  :assumption
(or b237  (= r149 0) )
  :assumption
(or (not b237)  (= r149 r403) )
  :assumption
(or (not b237)  (= r44 (~ r403)) )
  :assumption
(or (not b237)  b241 )
  :assumption
(or b118  (not b237) )
  :assumption
(or (not b237)  b242 )
  :assumption
(or (not b237)  (> r403 0) )
  :assumption
(or (not b237)  (<= r403 r39) )
  :assumption
(or (not b237)  (<= r403 (- 4 r144)) )
  :assumption
(or (= r53 0)  b247 )
  :assumption
(or b247  (= r158 0) )
  :assumption
(or (not b247)  (= r158 r404) )
  :assumption
(or (not b247)  (= r53 (~ r404)) )
  :assumption
(or (not b247)  b251 )
  :assumption
(or b129  (not b247) )
  :assumption
(or (not b247)  b252 )
  :assumption
(or (not b247)  (> r404 0) )
  :assumption
(or (not b247)  (<= r404 r48) )
  :assumption
(or (not b247)  (<= r404 (- 4 r153)) )
  :assumption
(or (= r77 0)  b257 )
  :assumption
(or b257  (= r405 0) )
  :assumption
(or (not b257)  (= r405 r406) )
  :assumption
(or (not b257)  (= r77 (~ r406)) )
  :assumption
(or b29  (not b257) )
  :assumption
(or (not b257)  b261 )
  :assumption
(or (not b257)  b262 )
  :assumption
(or (not b257)  (> r406 0) )
  :assumption
(or (not b257)  (<= r406 r73) )
  :assumption
(or (not b257)  (<= r406 (- 4 r215)) )
  :assumption
(or (= r86 0)  b267 )
  :assumption
(or b267  (= r407 0) )
  :assumption
(or (not b267)  (= r407 r408) )
  :assumption
(or (not b267)  (= r86 (~ r408)) )
  :assumption
(or b40  (not b267) )
  :assumption
(or (not b267)  b271 )
  :assumption
(or (not b267)  b272 )
  :assumption
(or (not b267)  (> r408 0) )
  :assumption
(or (not b267)  (<= r408 r82) )
  :assumption
(or (not b267)  (<= r408 (- 4 r262)) )
  :assumption
(or (= r95 0)  b277 )
  :assumption
(or b277  (= r409 0) )
  :assumption
(or (not b277)  (= r409 r410) )
  :assumption
(or (not b277)  (= r95 (~ r410)) )
  :assumption
(or b51  (not b277) )
  :assumption
(or (not b277)  b281 )
  :assumption
(or (not b277)  b282 )
  :assumption
(or (not b277)  (> r410 0) )
  :assumption
(or (not b277)  (<= r410 r91) )
  :assumption
(or (not b277)  (<= r410 (- 4 r289)) )
  :assumption
(or (= r104 0)  b287 )
  :assumption
(or b287  (= r411 0) )
  :assumption
(or (not b287)  (= r411 r412) )
  :assumption
(or (not b287)  (= r104 (~ r412)) )
  :assumption
(or b62  (not b287) )
  :assumption
(or (not b287)  b291 )
  :assumption
(or (not b287)  b292 )
  :assumption
(or (not b287)  (> r412 0) )
  :assumption
(or (not b287)  (<= r412 r100) )
  :assumption
(or (not b287)  (<= r412 (- 4 r314)) )
  :assumption
(or (= r113 0)  b297 )
  :assumption
(or b297  (= r6 0) )
  :assumption
(or (not b297)  (= r6 r413) )
  :assumption
(or (not b297)  (= r113 (~ r413)) )
  :assumption
(or b73  (not b297) )
  :assumption
(or (not b297)  b301 )
  :assumption
(or (not b297)  b302 )
  :assumption
(or (not b297)  (> r413 0) )
  :assumption
(or (not b297)  (<= r413 r109) )
  :assumption
(or (not b297)  (<= r413 (- 4 r2)) )
  :assumption
(or (= r122 0)  b307 )
  :assumption
(or b307  (= r15 0) )
  :assumption
(or (not b307)  (= r15 r414) )
  :assumption
(or (not b307)  (= r122 (~ r414)) )
  :assumption
(or b84  (not b307) )
  :assumption
(or (not b307)  b311 )
  :assumption
(or (not b307)  b312 )
  :assumption
(or (not b307)  (> r414 0) )
  :assumption
(or (not b307)  (<= r414 r118) )
  :assumption
(or (not b307)  (<= r414 (- 4 r11)) )
  :assumption
(or (= r130 0)  b317 )
  :assumption
(or b317  (= r25 0) )
  :assumption
(or (not b317)  (= r25 r415) )
  :assumption
(or (not b317)  (= r130 (~ r415)) )
  :assumption
(or b95  (not b317) )
  :assumption
(or (not b317)  b321 )
  :assumption
(or (not b317)  b322 )
  :assumption
(or (not b317)  (> r415 0) )
  :assumption
(or (not b317)  (<= r415 r126) )
  :assumption
(or (not b317)  (<= r415 (- 4 r21)) )
  :assumption
(or (= r139 0)  b327 )
  :assumption
(or b327  (= r34 0) )
  :assumption
(or (not b327)  (= r34 r416) )
  :assumption
(or (not b327)  (= r139 (~ r416)) )
  :assumption
(or b106  (not b327) )
  :assumption
(or (not b327)  b331 )
  :assumption
(or (not b327)  b332 )
  :assumption
(or (not b327)  (> r416 0) )
  :assumption
(or (not b327)  (<= r416 r135) )
  :assumption
(or (not b327)  (<= r416 (- 4 r30)) )
  :assumption
(or (= r148 0)  b337 )
  :assumption
(or b337  (= r43 0) )
  :assumption
(or (not b337)  (= r43 r417) )
  :assumption
(or (not b337)  (= r148 (~ r417)) )
  :assumption
(or b117  (not b337) )
  :assumption
(or (not b337)  b341 )
  :assumption
(or (not b337)  b342 )
  :assumption
(or (not b337)  (> r417 0) )
  :assumption
(or (not b337)  (<= r417 r144) )
  :assumption
(or (not b337)  (<= r417 (- 4 r39)) )
  :assumption
(or (= r157 0)  b347 )
  :assumption
(or b347  (= r52 0) )
  :assumption
(or (not b347)  (= r52 r418) )
  :assumption
(or (not b347)  (= r157 (~ r418)) )
  :assumption
(or b128  (not b347) )
  :assumption
(or (not b347)  b351 )
  :assumption
(or (not b347)  b352 )
  :assumption
(or (not b347)  (> r418 0) )
  :assumption
(or (not b347)  (<= r418 r153) )
  :assumption
(or (not b347)  (<= r418 (- 4 r48)) )
  :assumption
(or (= r62 0)  b357 )
  :assumption
(or b357  (= r419 0) )
  :assumption
(or (not b357)  (= r419 r420) )
  :assumption
(or (not b357)  (= r62 (~ r420)) )
  :assumption
(or b139  (not b357) )
  :assumption
(or (not b357)  b361 )
  :assumption
(or (not b357)  b362 )
  :assumption
(or (not b357)  (> r420 0) )
  :assumption
(or (not b357)  (<= r420 r60) )
  :assumption
(or (not b357)  (<= r420 (- 4 r327)) )
  :assumption
(or (= r69 0)  b367 )
  :assumption
(or b367  (= r421 0) )
  :assumption
(or (not b367)  (= r421 r422) )
  :assumption
(or (not b367)  (= r69 (~ r422)) )
  :assumption
(or b150  (not b367) )
  :assumption
(or (not b367)  b371 )
  :assumption
(or (not b367)  b372 )
  :assumption
(or (not b367)  (> r422 0) )
  :assumption
(or (not b367)  (<= r422 r66) )
  :assumption
(or (not b367)  (<= r422 (- 4 r330)) )
  :assumption
(or (= r76 0)  b377 )
  :assumption
(or b377  (= r423 0) )
  :assumption
(or (not b377)  (= r423 r424) )
  :assumption
(or (not b377)  (= r76 (~ r424)) )
  :assumption
(or b161  (not b377) )
  :assumption
(or b261  (not b377) )
  :assumption
(or (not b377)  b381 )
  :assumption
(or (not b377)  (> r424 0) )
  :assumption
(or (not b377)  (<= r424 r73) )
  :assumption
(or (not b377)  (<= r424 (- 4 r215)) )
  :assumption
(or (= r85 0)  b386 )
  :assumption
(or b386  (= r425 0) )
  :assumption
(or (not b386)  (= r425 r426) )
  :assumption
(or (not b386)  (= r85 (~ r426)) )
  :assumption
(or b171  (not b386) )
  :assumption
(or b271  (not b386) )
  :assumption
(or (not b386)  b390 )
  :assumption
(or (not b386)  (> r426 0) )
  :assumption
(or (not b386)  (<= r426 r82) )
  :assumption
(or (not b386)  (<= r426 (- 4 r262)) )
  :assumption
(or (= r94 0)  b395 )
  :assumption
(or b395  (= r427 0) )
  :assumption
(or (not b395)  (= r427 r428) )
  :assumption
(or (not b395)  (= r94 (~ r428)) )
  :assumption
(or b181  (not b395) )
  :assumption
(or b281  (not b395) )
  :assumption
(or (not b395)  b399 )
  :assumption
(or (not b395)  (> r428 0) )
  :assumption
(or (not b395)  (<= r428 r91) )
  :assumption
(or (not b395)  (<= r428 (- 4 r289)) )
  :assumption
(or (= r103 0)  b404 )
  :assumption
(or b404  (= r429 0) )
  :assumption
(or (not b404)  (= r429 r430) )
  :assumption
(or (not b404)  (= r103 (~ r430)) )
  :assumption
(or b191  (not b404) )
  :assumption
(or b291  (not b404) )
  :assumption
(or (not b404)  b408 )
  :assumption
(or (not b404)  (> r430 0) )
  :assumption
(or (not b404)  (<= r430 r100) )
  :assumption
(or (not b404)  (<= r430 (- 4 r314)) )
  :assumption
(or (= r112 0)  b413 )
  :assumption
(or b413  (= r5 0) )
  :assumption
(or (not b413)  (= r5 r431) )
  :assumption
(or (not b413)  (= r112 (~ r431)) )
  :assumption
(or b201  (not b413) )
  :assumption
(or b301  (not b413) )
  :assumption
(or (not b413)  b417 )
  :assumption
(or (not b413)  (> r431 0) )
  :assumption
(or (not b413)  (<= r431 r109) )
  :assumption
(or (not b413)  (<= r431 (- 4 r2)) )
  :assumption
(or (= r121 0)  b422 )
  :assumption
(or b422  (= r14 0) )
  :assumption
(or (not b422)  (= r14 r432) )
  :assumption
(or (not b422)  (= r121 (~ r432)) )
  :assumption
(or b211  (not b422) )
  :assumption
(or b311  (not b422) )
  :assumption
(or (not b422)  b426 )
  :assumption
(or (not b422)  (> r432 0) )
  :assumption
(or (not b422)  (<= r432 r118) )
  :assumption
(or (not b422)  (<= r432 (- 4 r11)) )
  :assumption
(or (= r129 0)  b431 )
  :assumption
(or b431  (= r24 0) )
  :assumption
(or (not b431)  (= r24 r433) )
  :assumption
(or (not b431)  (= r129 (~ r433)) )
  :assumption
(or b221  (not b431) )
  :assumption
(or b321  (not b431) )
  :assumption
(or (not b431)  b435 )
  :assumption
(or (not b431)  (> r433 0) )
  :assumption
(or (not b431)  (<= r433 r126) )
  :assumption
(or (not b431)  (<= r433 (- 4 r21)) )
  :assumption
(or (= r138 0)  b440 )
  :assumption
(or b440  (= r33 0) )
  :assumption
(or (not b440)  (= r33 r434) )
  :assumption
(or (not b440)  (= r138 (~ r434)) )
  :assumption
(or b231  (not b440) )
  :assumption
(or b331  (not b440) )
  :assumption
(or (not b440)  b444 )
  :assumption
(or (not b440)  (> r434 0) )
  :assumption
(or (not b440)  (<= r434 r135) )
  :assumption
(or (not b440)  (<= r434 (- 4 r30)) )
  :assumption
(or (= r147 0)  b449 )
  :assumption
(or b449  (= r42 0) )
  :assumption
(or (not b449)  (= r42 r435) )
  :assumption
(or (not b449)  (= r147 (~ r435)) )
  :assumption
(or b241  (not b449) )
  :assumption
(or b341  (not b449) )
  :assumption
(or (not b449)  b453 )
  :assumption
(or (not b449)  (> r435 0) )
  :assumption
(or (not b449)  (<= r435 r144) )
  :assumption
(or (not b449)  (<= r435 (- 4 r39)) )
  :assumption
(or (= r156 0)  b458 )
  :assumption
(or b458  (= r51 0) )
  :assumption
(or (not b458)  (= r51 r436) )
  :assumption
(or (not b458)  (= r156 (~ r436)) )
  :assumption
(or b251  (not b458) )
  :assumption
(or b351  (not b458) )
  :assumption
(or (not b458)  b462 )
  :assumption
(or (not b458)  (> r436 0) )
  :assumption
(or (not b458)  (<= r436 r153) )
  :assumption
(or (not b458)  (<= r436 (- 4 r48)) )
  :assumption
(or (= r170 0)  b467 )
  :assumption
(or b467  (= r437 0) )
  :assumption
(or (not b467)  (= r437 (~ r438)) )
  :assumption
(or (not b467)  (= r170 r438) )
  :assumption
(or (not b467)  b471 )
  :assumption
(or b151  (not b467) )
  :assumption
(or (not b467)  (> r438 0) )
  :assumption
(or (not b467)  (<= r438 r330) )
  :assumption
(or (= r174 0)  b475 )
  :assumption
(or b475  (= r439 0) )
  :assumption
(or (not b475)  (= r439 (~ r440)) )
  :assumption
(or (not b475)  (= r174 r440) )
  :assumption
(or b29  (not b475) )
  :assumption
(or b30  (not b475) )
  :assumption
(or (not b475)  (> r440 0) )
  :assumption
(or (not b475)  (<= r440 r215) )
  :assumption
(or (= r179 0)  b482 )
  :assumption
(or b482  (= r441 0) )
  :assumption
(or (not b482)  (= r441 (~ r442)) )
  :assumption
(or (not b482)  (= r179 r442) )
  :assumption
(or b40  (not b482) )
  :assumption
(or b41  (not b482) )
  :assumption
(or (not b482)  (> r442 0) )
  :assumption
(or (not b482)  (<= r442 r262) )
  :assumption
(or (= r184 0)  b489 )
  :assumption
(or b489  (= r443 0) )
  :assumption
(or (not b489)  (= r443 (~ r444)) )
  :assumption
(or (not b489)  (= r184 r444) )
  :assumption
(or b51  (not b489) )
  :assumption
(or b52  (not b489) )
  :assumption
(or (not b489)  (> r444 0) )
  :assumption
(or (not b489)  (<= r444 r289) )
  :assumption
(or (= r188 0)  b496 )
  :assumption
(or b496  (= r445 0) )
  :assumption
(or (not b496)  (= r445 (~ r446)) )
  :assumption
(or (not b496)  (= r188 r446) )
  :assumption
(or b62  (not b496) )
  :assumption
(or b63  (not b496) )
  :assumption
(or (not b496)  (> r446 0) )
  :assumption
(or (not b496)  (<= r446 r314) )
  :assumption
(or (= r192 0)  b503 )
  :assumption
(or b503  (= r4 0) )
  :assumption
(or (not b503)  (= r4 (~ r447)) )
  :assumption
(or (not b503)  (= r192 r447) )
  :assumption
(or b73  (not b503) )
  :assumption
(or b74  (not b503) )
  :assumption
(or (not b503)  (> r447 0) )
  :assumption
(or (not b503)  (<= r447 r2) )
  :assumption
(or (= r197 0)  b510 )
  :assumption
(or b510  (= r13 0) )
  :assumption
(or (not b510)  (= r13 (~ r448)) )
  :assumption
(or (not b510)  (= r197 r448) )
  :assumption
(or b84  (not b510) )
  :assumption
(or b85  (not b510) )
  :assumption
(or (not b510)  (> r448 0) )
  :assumption
(or (not b510)  (<= r448 r11) )
  :assumption
(or (= r201 0)  b517 )
  :assumption
(or b517  (= r23 0) )
  :assumption
(or (not b517)  (= r23 (~ r449)) )
  :assumption
(or (not b517)  (= r201 r449) )
  :assumption
(or b95  (not b517) )
  :assumption
(or b96  (not b517) )
  :assumption
(or (not b517)  (> r449 0) )
  :assumption
(or (not b517)  (<= r449 r21) )
  :assumption
(or (= r205 0)  b524 )
  :assumption
(or b524  (= r32 0) )
  :assumption
(or (not b524)  (= r32 (~ r450)) )
  :assumption
(or (not b524)  (= r205 r450) )
  :assumption
(or b106  (not b524) )
  :assumption
(or b107  (not b524) )
  :assumption
(or (not b524)  (> r450 0) )
  :assumption
(or (not b524)  (<= r450 r30) )
  :assumption
(or (= r209 0)  b531 )
  :assumption
(or b531  (= r41 0) )
  :assumption
(or (not b531)  (= r41 (~ r451)) )
  :assumption
(or (not b531)  (= r209 r451) )
  :assumption
(or b117  (not b531) )
  :assumption
(or b118  (not b531) )
  :assumption
(or (not b531)  (> r451 0) )
  :assumption
(or (not b531)  (<= r451 r39) )
  :assumption
(or (= r212 0)  b538 )
  :assumption
(or b538  (= r50 0) )
  :assumption
(or (not b538)  (= r50 (~ r452)) )
  :assumption
(or (not b538)  (= r212 r452) )
  :assumption
(or b128  (not b538) )
  :assumption
(or b129  (not b538) )
  :assumption
(or (not b538)  (> r452 0) )
  :assumption
(or (not b538)  (<= r452 r48) )
  :assumption
(or (= r219 0)  b545 )
  :assumption
(or b545  (= r453 0) )
  :assumption
(or (not b545)  (= r453 (~ r454)) )
  :assumption
(or (not b545)  (= r219 r454) )
  :assumption
(or b139  (not b545) )
  :assumption
(or b140  (not b545) )
  :assumption
(or (not b545)  (> r454 0) )
  :assumption
(or (not b545)  (<= r454 r327) )
  :assumption
(or (= r223 0)  b552 )
  :assumption
(or b552  (= r455 0) )
  :assumption
(or (not b552)  (= r455 (~ r456)) )
  :assumption
(or (not b552)  (= r223 r456) )
  :assumption
(or b150  (not b552) )
  :assumption
(or b151  (not b552) )
  :assumption
(or (not b552)  (> r456 0) )
  :assumption
(or (not b552)  (<= r456 r330) )
  :assumption
(or (= r228 0)  b559 )
  :assumption
(or b559  (= r457 0) )
  :assumption
(or (not b559)  (= r457 (~ r458)) )
  :assumption
(or (not b559)  (= r228 r458) )
  :assumption
(or b161  (not b559) )
  :assumption
(or b30  (not b559) )
  :assumption
(or (not b559)  (> r458 0) )
  :assumption
(or (not b559)  (<= r458 r215) )
  :assumption
(or (= r232 0)  b566 )
  :assumption
(or b566  (= r459 0) )
  :assumption
(or (not b566)  (= r459 (~ r460)) )
  :assumption
(or (not b566)  (= r232 r460) )
  :assumption
(or b171  (not b566) )
  :assumption
(or b41  (not b566) )
  :assumption
(or (not b566)  (> r460 0) )
  :assumption
(or (not b566)  (<= r460 r262) )
  :assumption
(or (= r236 0)  b573 )
  :assumption
(or b573  (= r461 0) )
  :assumption
(or (not b573)  (= r461 (~ r462)) )
  :assumption
(or (not b573)  (= r236 r462) )
  :assumption
(or b181  (not b573) )
  :assumption
(or b52  (not b573) )
  :assumption
(or (not b573)  (> r462 0) )
  :assumption
(or (not b573)  (<= r462 r289) )
  :assumption
(or (= r241 0)  b580 )
  :assumption
(or b580  (= r463 0) )
  :assumption
(or (not b580)  (= r463 (~ r464)) )
  :assumption
(or (not b580)  (= r241 r464) )
  :assumption
(or b191  (not b580) )
  :assumption
(or b63  (not b580) )
  :assumption
(or (not b580)  (> r464 0) )
  :assumption
(or (not b580)  (<= r464 r314) )
  :assumption
(or (= r245 0)  b587 )
  :assumption
(or b587  (= r3 0) )
  :assumption
(or (not b587)  (= r3 (~ r465)) )
  :assumption
(or (not b587)  (= r245 r465) )
  :assumption
(or b201  (not b587) )
  :assumption
(or b74  (not b587) )
  :assumption
(or (not b587)  (> r465 0) )
  :assumption
(or (not b587)  (<= r465 r2) )
  :assumption
(or (= r249 0)  b594 )
  :assumption
(or b594  (= r12 0) )
  :assumption
(or (not b594)  (= r12 (~ r466)) )
  :assumption
(or (not b594)  (= r249 r466) )
  :assumption
(or b211  (not b594) )
  :assumption
(or b85  (not b594) )
  :assumption
(or (not b594)  (> r466 0) )
  :assumption
(or (not b594)  (<= r466 r11) )
  :assumption
(or (= r253 0)  b601 )
  :assumption
(or b601  (= r22 0) )
  :assumption
(or (not b601)  (= r22 (~ r467)) )
  :assumption
(or (not b601)  (= r253 r467) )
  :assumption
(or b221  (not b601) )
  :assumption
(or b96  (not b601) )
  :assumption
(or (not b601)  (> r467 0) )
  :assumption
(or (not b601)  (<= r467 r21) )
  :assumption
(or (= r257 0)  b608 )
  :assumption
(or b608  (= r31 0) )
  :assumption
(or (not b608)  (= r31 (~ r468)) )
  :assumption
(or (not b608)  (= r257 r468) )
  :assumption
(or b231  (not b608) )
  :assumption
(or b107  (not b608) )
  :assumption
(or (not b608)  (> r468 0) )
  :assumption
(or (not b608)  (<= r468 r30) )
  :assumption
(or (= r261 0)  b615 )
  :assumption
(or b615  (= r40 0) )
  :assumption
(or (not b615)  (= r40 (~ r469)) )
  :assumption
(or (not b615)  (= r261 r469) )
  :assumption
(or b241  (not b615) )
  :assumption
(or b118  (not b615) )
  :assumption
(or (not b615)  (> r469 0) )
  :assumption
(or (not b615)  (<= r469 r39) )
  :assumption
(or (= r266 0)  b622 )
  :assumption
(or b622  (= r49 0) )
  :assumption
(or (not b622)  (= r49 (~ r470)) )
  :assumption
(or (not b622)  (= r266 r470) )
  :assumption
(or b251  (not b622) )
  :assumption
(or b129  (not b622) )
  :assumption
(or (not b622)  (> r470 0) )
  :assumption
(or (not b622)  (<= r470 r48) )
  :assumption
(or (= r169 0)  b629 )
  :assumption
(or b629  (= r68 0) )
  :assumption
(or (not b629)  (= r68 (~ r471)) )
  :assumption
(or (not b629)  (= r169 r471) )
  :assumption
(or b471  (not b629) )
  :assumption
(or b371  (not b629) )
  :assumption
(or (not b629)  (> r471 0) )
  :assumption
(or (not b629)  (<= r471 r66) )
  :assumption
(or (= r173 0)  b636 )
  :assumption
(or b636  (= r75 0) )
  :assumption
(or (not b636)  (= r75 (~ r472)) )
  :assumption
(or (not b636)  (= r173 r472) )
  :assumption
(or b29  (not b636) )
  :assumption
(or b261  (not b636) )
  :assumption
(or (not b636)  (> r472 0) )
  :assumption
(or (not b636)  (<= r472 r73) )
  :assumption
(or (= r178 0)  b643 )
  :assumption
(or b643  (= r84 0) )
  :assumption
(or (not b643)  (= r84 (~ r473)) )
  :assumption
(or (not b643)  (= r178 r473) )
  :assumption
(or b40  (not b643) )
  :assumption
(or b271  (not b643) )
  :assumption
(or (not b643)  (> r473 0) )
  :assumption
(or (not b643)  (<= r473 r82) )
  :assumption
(or (= r183 0)  b650 )
  :assumption
(or b650  (= r93 0) )
  :assumption
(or (not b650)  (= r93 (~ r474)) )
  :assumption
(or (not b650)  (= r183 r474) )
  :assumption
(or b51  (not b650) )
  :assumption
(or b281  (not b650) )
  :assumption
(or (not b650)  (> r474 0) )
  :assumption
(or (not b650)  (<= r474 r91) )
  :assumption
(or (= r187 0)  b657 )
  :assumption
(or b657  (= r102 0) )
  :assumption
(or (not b657)  (= r102 (~ r475)) )
  :assumption
(or (not b657)  (= r187 r475) )
  :assumption
(or b62  (not b657) )
  :assumption
(or b291  (not b657) )
  :assumption
(or (not b657)  (> r475 0) )
  :assumption
(or (not b657)  (<= r475 r100) )
  :assumption
(or (= r191 0)  b664 )
  :assumption
(or b664  (= r111 0) )
  :assumption
(or (not b664)  (= r111 (~ r476)) )
  :assumption
(or (not b664)  (= r191 r476) )
  :assumption
(or b73  (not b664) )
  :assumption
(or b301  (not b664) )
  :assumption
(or (not b664)  (> r476 0) )
  :assumption
(or (not b664)  (<= r476 r109) )
  :assumption
(or (= r196 0)  b671 )
  :assumption
(or b671  (= r120 0) )
  :assumption
(or (not b671)  (= r120 (~ r477)) )
  :assumption
(or (not b671)  (= r196 r477) )
  :assumption
(or b84  (not b671) )
  :assumption
(or b311  (not b671) )
  :assumption
(or (not b671)  (> r477 0) )
  :assumption
(or (not b671)  (<= r477 r118) )
  :assumption
(or (= r200 0)  b678 )
  :assumption
(or b678  (= r128 0) )
  :assumption
(or (not b678)  (= r128 (~ r478)) )
  :assumption
(or (not b678)  (= r200 r478) )
  :assumption
(or b95  (not b678) )
  :assumption
(or b321  (not b678) )
  :assumption
(or (not b678)  (> r478 0) )
  :assumption
(or (not b678)  (<= r478 r126) )
  :assumption
(or (= r204 0)  b685 )
  :assumption
(or b685  (= r137 0) )
  :assumption
(or (not b685)  (= r137 (~ r479)) )
  :assumption
(or (not b685)  (= r204 r479) )
  :assumption
(or b106  (not b685) )
  :assumption
(or b331  (not b685) )
  :assumption
(or (not b685)  (> r479 0) )
  :assumption
(or (not b685)  (<= r479 r135) )
  :assumption
(or (= r208 0)  b692 )
  :assumption
(or b692  (= r146 0) )
  :assumption
(or (not b692)  (= r146 (~ r480)) )
  :assumption
(or (not b692)  (= r208 r480) )
  :assumption
(or b117  (not b692) )
  :assumption
(or b341  (not b692) )
  :assumption
(or (not b692)  (> r480 0) )
  :assumption
(or (not b692)  (<= r480 r144) )
  :assumption
(or (= r211 0)  b699 )
  :assumption
(or b699  (= r155 0) )
  :assumption
(or (not b699)  (= r155 (~ r481)) )
  :assumption
(or (not b699)  (= r211 r481) )
  :assumption
(or b128  (not b699) )
  :assumption
(or b351  (not b699) )
  :assumption
(or (not b699)  (> r481 0) )
  :assumption
(or (not b699)  (<= r481 r153) )
  :assumption
(or (= r218 0)  b706 )
  :assumption
(or b706  (= r61 0) )
  :assumption
(or (not b706)  (= r61 (~ r482)) )
  :assumption
(or (not b706)  (= r218 r482) )
  :assumption
(or b139  (not b706) )
  :assumption
(or b361  (not b706) )
  :assumption
(or (not b706)  (> r482 0) )
  :assumption
(or (not b706)  (<= r482 r60) )
  :assumption
(or (= r222 0)  b713 )
  :assumption
(or b713  (= r67 0) )
  :assumption
(or (not b713)  (= r67 (~ r483)) )
  :assumption
(or (not b713)  (= r222 r483) )
  :assumption
(or b150  (not b713) )
  :assumption
(or b371  (not b713) )
  :assumption
(or (not b713)  (> r483 0) )
  :assumption
(or (not b713)  (<= r483 r66) )
  :assumption
(or (= r227 0)  b720 )
  :assumption
(or b720  (= r74 0) )
  :assumption
(or (not b720)  (= r74 (~ r484)) )
  :assumption
(or (not b720)  (= r227 r484) )
  :assumption
(or b161  (not b720) )
  :assumption
(or b261  (not b720) )
  :assumption
(or (not b720)  (> r484 0) )
  :assumption
(or (not b720)  (<= r484 r73) )
  :assumption
(or (= r231 0)  b727 )
  :assumption
(or b727  (= r83 0) )
  :assumption
(or (not b727)  (= r83 (~ r485)) )
  :assumption
(or (not b727)  (= r231 r485) )
  :assumption
(or b171  (not b727) )
  :assumption
(or b271  (not b727) )
  :assumption
(or (not b727)  (> r485 0) )
  :assumption
(or (not b727)  (<= r485 r82) )
  :assumption
(or (= r235 0)  b734 )
  :assumption
(or b734  (= r92 0) )
  :assumption
(or (not b734)  (= r92 (~ r486)) )
  :assumption
(or (not b734)  (= r235 r486) )
  :assumption
(or b181  (not b734) )
  :assumption
(or b281  (not b734) )
  :assumption
(or (not b734)  (> r486 0) )
  :assumption
(or (not b734)  (<= r486 r91) )
  :assumption
(or (= r240 0)  b741 )
  :assumption
(or b741  (= r101 0) )
  :assumption
(or (not b741)  (= r101 (~ r487)) )
  :assumption
(or (not b741)  (= r240 r487) )
  :assumption
(or b191  (not b741) )
  :assumption
(or b291  (not b741) )
  :assumption
(or (not b741)  (> r487 0) )
  :assumption
(or (not b741)  (<= r487 r100) )
  :assumption
(or (= r244 0)  b748 )
  :assumption
(or b748  (= r110 0) )
  :assumption
(or (not b748)  (= r110 (~ r488)) )
  :assumption
(or (not b748)  (= r244 r488) )
  :assumption
(or b201  (not b748) )
  :assumption
(or b301  (not b748) )
  :assumption
(or (not b748)  (> r488 0) )
  :assumption
(or (not b748)  (<= r488 r109) )
  :assumption
(or (= r248 0)  b755 )
  :assumption
(or b755  (= r119 0) )
  :assumption
(or (not b755)  (= r119 (~ r489)) )
  :assumption
(or (not b755)  (= r248 r489) )
  :assumption
(or b211  (not b755) )
  :assumption
(or b311  (not b755) )
  :assumption
(or (not b755)  (> r489 0) )
  :assumption
(or (not b755)  (<= r489 r118) )
  :assumption
(or (= r252 0)  b762 )
  :assumption
(or b762  (= r127 0) )
  :assumption
(or (not b762)  (= r127 (~ r490)) )
  :assumption
(or (not b762)  (= r252 r490) )
  :assumption
(or b221  (not b762) )
  :assumption
(or b321  (not b762) )
  :assumption
(or (not b762)  (> r490 0) )
  :assumption
(or (not b762)  (<= r490 r126) )
  :assumption
(or (= r256 0)  b769 )
  :assumption
(or b769  (= r136 0) )
  :assumption
(or (not b769)  (= r136 (~ r491)) )
  :assumption
(or (not b769)  (= r256 r491) )
  :assumption
(or b231  (not b769) )
  :assumption
(or b331  (not b769) )
  :assumption
(or (not b769)  (> r491 0) )
  :assumption
(or (not b769)  (<= r491 r135) )
  :assumption
(or (= r260 0)  b776 )
  :assumption
(or b776  (= r145 0) )
  :assumption
(or (not b776)  (= r145 (~ r492)) )
  :assumption
(or (not b776)  (= r260 r492) )
  :assumption
(or b241  (not b776) )
  :assumption
(or b341  (not b776) )
  :assumption
(or (not b776)  (> r492 0) )
  :assumption
(or (not b776)  (<= r492 r144) )
  :assumption
(or (= r265 0)  b783 )
  :assumption
(or b783  (= r154 0) )
  :assumption
(or (not b783)  (= r154 (~ r493)) )
  :assumption
(or (not b783)  (= r265 r493) )
  :assumption
(or b251  (not b783) )
  :assumption
(or b351  (not b783) )
  :assumption
(or (not b783)  (> r493 0) )
  :assumption
(or (not b783)  (<= r493 r153) )
  :assumption
(or (not b789)  b790 )
  :assumption
(or (not b789)  b791 )
  :assumption
(or (not b792)  b793 )
  :assumption
(or (not b792)  b794 )
  :assumption
(or b139  (not b792) )
  :assumption
(or b362  (not b792) )
  :assumption
(or (not b791)  (not b792) )
  :assumption
(or (not b795)  b796 )
  :assumption
(or (not b795)  b797 )
  :assumption
(or b150  (not b795) )
  :assumption
(or b372  (not b795) )
  :assumption
(or (not b794)  (not b795) )
  :assumption
(or (not b798)  b799 )
  :assumption
(or (not b798)  b800 )
  :assumption
(or b161  (not b798) )
  :assumption
(or b381  (not b798) )
  :assumption
(or (not b797)  (not b798) )
  :assumption
(or (not b801)  b802 )
  :assumption
(or (not b801)  b803 )
  :assumption
(or b171  (not b801) )
  :assumption
(or b390  (not b801) )
  :assumption
(or (not b800)  (not b801) )
  :assumption
(or (not b804)  b805 )
  :assumption
(or (not b804)  b806 )
  :assumption
(or b181  (not b804) )
  :assumption
(or b399  (not b804) )
  :assumption
(or (not b803)  (not b804) )
  :assumption
(or (not b807)  b808 )
  :assumption
(or (not b807)  b809 )
  :assumption
(or b191  (not b807) )
  :assumption
(or b408  (not b807) )
  :assumption
(or (not b806)  (not b807) )
  :assumption
(or (not b810)  b811 )
  :assumption
(or (not b810)  b812 )
  :assumption
(or b201  (not b810) )
  :assumption
(or b417  (not b810) )
  :assumption
(or (not b809)  (not b810) )
  :assumption
(or (not b813)  b814 )
  :assumption
(or (not b813)  b815 )
  :assumption
(or b211  (not b813) )
  :assumption
(or b426  (not b813) )
  :assumption
(or (not b812)  (not b813) )
  :assumption
(or (not b816)  b817 )
  :assumption
(or (not b816)  b818 )
  :assumption
(or b221  (not b816) )
  :assumption
(or b435  (not b816) )
  :assumption
(or (not b815)  (not b816) )
  :assumption
(or (not b819)  b820 )
  :assumption
(or (not b819)  b821 )
  :assumption
(or b231  (not b819) )
  :assumption
(or b444  (not b819) )
  :assumption
(or (not b818)  (not b819) )
  :assumption
(or (not b822)  b823 )
  :assumption
(or (not b822)  b824 )
  :assumption
(or b241  (not b822) )
  :assumption
(or b453  (not b822) )
  :assumption
(or (not b821)  (not b822) )
  :assumption
(or (not b825)  b826 )
  :assumption
(or (not b825)  b827 )
  :assumption
(or b251  (not b825) )
  :assumption
(or b462  (not b825) )
  :assumption
(or (not b824)  (not b825) )
  :assumption
(or (not b828)  b829 )
  :assumption
(or b791  (not b828) )
  :assumption
(or (not b830)  b831 )
  :assumption
(or b794  (not b830) )
  :assumption
(or b139  (not b830) )
  :assumption
(or b141  (not b830) )
  :assumption
(or (not b791)  (not b830) )
  :assumption
(or (not b832)  b833 )
  :assumption
(or b797  (not b832) )
  :assumption
(or b150  (not b832) )
  :assumption
(or b152  (not b832) )
  :assumption
(or (not b794)  (not b832) )
  :assumption
(or (not b834)  b835 )
  :assumption
(or b800  (not b834) )
  :assumption
(or b161  (not b834) )
  :assumption
(or b162  (not b834) )
  :assumption
(or (not b797)  (not b834) )
  :assumption
(or (not b836)  b837 )
  :assumption
(or b803  (not b836) )
  :assumption
(or b171  (not b836) )
  :assumption
(or b172  (not b836) )
  :assumption
(or (not b800)  (not b836) )
  :assumption
(or (not b838)  b839 )
  :assumption
(or b806  (not b838) )
  :assumption
(or b181  (not b838) )
  :assumption
(or b182  (not b838) )
  :assumption
(or (not b803)  (not b838) )
  :assumption
(or (not b840)  b841 )
  :assumption
(or b809  (not b840) )
  :assumption
(or b191  (not b840) )
  :assumption
(or b192  (not b840) )
  :assumption
(or (not b806)  (not b840) )
  :assumption
(or (not b842)  b843 )
  :assumption
(or b812  (not b842) )
  :assumption
(or b201  (not b842) )
  :assumption
(or b202  (not b842) )
  :assumption
(or (not b809)  (not b842) )
  :assumption
(or (not b844)  b845 )
  :assumption
(or b815  (not b844) )
  :assumption
(or b211  (not b844) )
  :assumption
(or b212  (not b844) )
  :assumption
(or (not b812)  (not b844) )
  :assumption
(or (not b846)  b847 )
  :assumption
(or b818  (not b846) )
  :assumption
(or b221  (not b846) )
  :assumption
(or b222  (not b846) )
  :assumption
(or (not b815)  (not b846) )
  :assumption
(or (not b848)  b849 )
  :assumption
(or b821  (not b848) )
  :assumption
(or b231  (not b848) )
  :assumption
(or b232  (not b848) )
  :assumption
(or (not b818)  (not b848) )
  :assumption
(or (not b850)  b851 )
  :assumption
(or b824  (not b850) )
  :assumption
(or b241  (not b850) )
  :assumption
(or b242  (not b850) )
  :assumption
(or (not b821)  (not b850) )
  :assumption
(or (not b852)  b853 )
  :assumption
(or b827  (not b852) )
  :assumption
(or b251  (not b852) )
  :assumption
(or b252  (not b852) )
  :assumption
(or (not b824)  (not b852) )
  :assumption
(or (not b793)  (not b854) )
  :assumption
(or (not b794)  (not b854) )
  :assumption
(or b139  (not b854) )
  :assumption
(or b791  (not b854) )
  :assumption
(or b790  (not b854) )
  :assumption
(or (not b796)  (not b855) )
  :assumption
(or (not b797)  (not b855) )
  :assumption
(or b150  (not b855) )
  :assumption
(or b794  (not b855) )
  :assumption
(or b793  (not b855) )
  :assumption
(or (not b799)  (not b856) )
  :assumption
(or (not b800)  (not b856) )
  :assumption
(or b161  (not b856) )
  :assumption
(or b797  (not b856) )
  :assumption
(or b796  (not b856) )
  :assumption
(or (not b802)  (not b857) )
  :assumption
(or (not b803)  (not b857) )
  :assumption
(or b171  (not b857) )
  :assumption
(or b800  (not b857) )
  :assumption
(or b799  (not b857) )
  :assumption
(or (not b805)  (not b858) )
  :assumption
(or (not b806)  (not b858) )
  :assumption
(or b181  (not b858) )
  :assumption
(or b803  (not b858) )
  :assumption
(or b802  (not b858) )
  :assumption
(or (not b808)  (not b859) )
  :assumption
(or (not b809)  (not b859) )
  :assumption
(or b191  (not b859) )
  :assumption
(or b806  (not b859) )
  :assumption
(or b805  (not b859) )
  :assumption
(or (not b811)  (not b860) )
  :assumption
(or (not b812)  (not b860) )
  :assumption
(or b201  (not b860) )
  :assumption
(or b809  (not b860) )
  :assumption
(or b808  (not b860) )
  :assumption
(or (not b814)  (not b861) )
  :assumption
(or (not b815)  (not b861) )
  :assumption
(or b211  (not b861) )
  :assumption
(or b812  (not b861) )
  :assumption
(or b811  (not b861) )
  :assumption
(or (not b817)  (not b862) )
  :assumption
(or (not b818)  (not b862) )
  :assumption
(or b221  (not b862) )
  :assumption
(or b815  (not b862) )
  :assumption
(or b814  (not b862) )
  :assumption
(or (not b820)  (not b863) )
  :assumption
(or (not b821)  (not b863) )
  :assumption
(or b231  (not b863) )
  :assumption
(or b818  (not b863) )
  :assumption
(or b817  (not b863) )
  :assumption
(or (not b823)  (not b864) )
  :assumption
(or (not b824)  (not b864) )
  :assumption
(or b241  (not b864) )
  :assumption
(or b821  (not b864) )
  :assumption
(or b820  (not b864) )
  :assumption
(or (not b826)  (not b865) )
  :assumption
(or (not b827)  (not b865) )
  :assumption
(or b251  (not b865) )
  :assumption
(or b824  (not b865) )
  :assumption
(or b823  (not b865) )
  :assumption
(or (not b831)  (not b866) )
  :assumption
(or (not b794)  (not b866) )
  :assumption
(or b139  (not b866) )
  :assumption
(or b791  (not b866) )
  :assumption
(or b829  (not b866) )
  :assumption
(or (not b833)  (not b867) )
  :assumption
(or (not b797)  (not b867) )
  :assumption
(or b150  (not b867) )
  :assumption
(or b794  (not b867) )
  :assumption
(or b831  (not b867) )
  :assumption
(or (not b835)  (not b868) )
  :assumption
(or (not b800)  (not b868) )
  :assumption
(or b161  (not b868) )
  :assumption
(or b797  (not b868) )
  :assumption
(or b833  (not b868) )
  :assumption
(or (not b837)  (not b869) )
  :assumption
(or (not b803)  (not b869) )
  :assumption
(or b171  (not b869) )
  :assumption
(or b800  (not b869) )
  :assumption
(or b835  (not b869) )
  :assumption
(or (not b839)  (not b870) )
  :assumption
(or (not b806)  (not b870) )
  :assumption
(or b181  (not b870) )
  :assumption
(or b803  (not b870) )
  :assumption
(or b837  (not b870) )
  :assumption
(or (not b841)  (not b871) )
  :assumption
(or (not b809)  (not b871) )
  :assumption
(or b191  (not b871) )
  :assumption
(or b806  (not b871) )
  :assumption
(or b839  (not b871) )
  :assumption
(or (not b843)  (not b872) )
  :assumption
(or (not b812)  (not b872) )
  :assumption
(or b201  (not b872) )
  :assumption
(or b809  (not b872) )
  :assumption
(or b841  (not b872) )
  :assumption
(or (not b845)  (not b873) )
  :assumption
(or (not b815)  (not b873) )
  :assumption
(or b211  (not b873) )
  :assumption
(or b812  (not b873) )
  :assumption
(or b843  (not b873) )
  :assumption
(or (not b847)  (not b874) )
  :assumption
(or (not b818)  (not b874) )
  :assumption
(or b221  (not b874) )
  :assumption
(or b815  (not b874) )
  :assumption
(or b845  (not b874) )
  :assumption
(or (not b849)  (not b875) )
  :assumption
(or (not b821)  (not b875) )
  :assumption
(or b231  (not b875) )
  :assumption
(or b818  (not b875) )
  :assumption
(or b847  (not b875) )
  :assumption
(or (not b851)  (not b876) )
  :assumption
(or (not b824)  (not b876) )
  :assumption
(or b241  (not b876) )
  :assumption
(or b821  (not b876) )
  :assumption
(or b849  (not b876) )
  :assumption
(or (not b853)  (not b877) )
  :assumption
(or (not b827)  (not b877) )
  :assumption
(or b251  (not b877) )
  :assumption
(or b824  (not b877) )
  :assumption
(or b851  (not b877) )
  :assumption
(or (= r329 0)  b879 )
  :assumption
(or (not b879)  (= r329 (* (- r37 r28) (/ 1 10))) )
  :assumption
(or (or (or (not b362)  (not b790) )  b879 )  (> r328 4) )
  :assumption
(or (not b879)  (<= r328 4) )
  :assumption
(or b790  (not b879) )
  :assumption
(or b362  (not b879) )
  :assumption
(or (or (or (not b362)  (not b790) )  b879 )  (> r327 4) )
  :assumption
(or (not b879)  (<= r327 4) )
  :assumption
(or (= r332 0)  b886 )
  :assumption
(or (not b886)  (= r332 (* (- r46 r37) (/ 1 10))) )
  :assumption
(or (or (or (not b372)  (not b793) )  b886 )  (> r331 4) )
  :assumption
(or (not b886)  (<= r331 4) )
  :assumption
(or b793  (not b886) )
  :assumption
(or b372  (not b886) )
  :assumption
(or (or (or (not b372)  (not b793) )  b886 )  (> r330 4) )
  :assumption
(or (not b886)  (<= r330 4) )
  :assumption
(or (or (or (not b362)  (not b790) )  (<= r328 4) )  (>= r327 4) )
  :assumption
(or (<= r330 4)  (>= r331 4) )
  :assumption
(or (= r334 0)  b895 )
  :assumption
(or (not b895)  (= r334 (* (- r55 r46) (/ 1 10))) )
  :assumption
(or (or (or (not b381)  (not b796) )  b895 )  (> r333 4) )
  :assumption
(or (not b895)  (<= r333 4) )
  :assumption
(or b796  (not b895) )
  :assumption
(or b381  (not b895) )
  :assumption
(or (or (or (not b381)  (not b796) )  b895 )  (> r215 4) )
  :assumption
(or (not b895)  (<= r215 4) )
  :assumption
(or (or (or (not b372)  (not b793) )  (<= r331 4) )  (>= r330 4) )
  :assumption
(or (<= r215 4)  (>= r333 4) )
  :assumption
(or (= r336 0)  b904 )
  :assumption
(or (not b904)  (= r336 (* (- r58 r55) (/ 1 10))) )
  :assumption
(or (or (or (not b390)  (not b799) )  b904 )  (> r335 4) )
  :assumption
(or (not b904)  (<= r335 4) )
  :assumption
(or b799  (not b904) )
  :assumption
(or b390  (not b904) )
  :assumption
(or (or (or (not b390)  (not b799) )  b904 )  (> r262 4) )
  :assumption
(or (not b904)  (<= r262 4) )
  :assumption
(or (or (or (not b381)  (not b796) )  (<= r333 4) )  (>= r215 4) )
  :assumption
(or (<= r262 4)  (>= r335 4) )
  :assumption
(or (= r338 0)  b913 )
  :assumption
(or (not b913)  (= r338 (* (- r64 r58) (/ 1 10))) )
  :assumption
(or (or (or (not b399)  (not b802) )  b913 )  (> r337 4) )
  :assumption
(or (not b913)  (<= r337 4) )
  :assumption
(or b802  (not b913) )
  :assumption
(or b399  (not b913) )
  :assumption
(or (or (or (not b399)  (not b802) )  b913 )  (> r289 4) )
  :assumption
(or (not b913)  (<= r289 4) )
  :assumption
(or (or (or (not b390)  (not b799) )  (<= r335 4) )  (>= r262 4) )
  :assumption
(or (<= r289 4)  (>= r337 4) )
  :assumption
(or (= r340 0)  b922 )
  :assumption
(or (not b922)  (= r340 (* (- r71 r64) (/ 1 10))) )
  :assumption
(or (or (or (not b408)  (not b805) )  b922 )  (> r339 4) )
  :assumption
(or (not b922)  (<= r339 4) )
  :assumption
(or b805  (not b922) )
  :assumption
(or b408  (not b922) )
  :assumption
(or (or (or (not b408)  (not b805) )  b922 )  (> r314 4) )
  :assumption
(or (not b922)  (<= r314 4) )
  :assumption
(or (or (or (not b399)  (not b802) )  (<= r337 4) )  (>= r289 4) )
  :assumption
(or (<= r314 4)  (>= r339 4) )
  :assumption
(or (= r342 0)  b931 )
  :assumption
(or (not b931)  (= r342 (* (- r80 r71) (/ 1 10))) )
  :assumption
(or (or (or (not b417)  (not b808) )  b931 )  (> r341 4) )
  :assumption
(or (not b931)  (<= r341 4) )
  :assumption
(or b808  (not b931) )
  :assumption
(or b417  (not b931) )
  :assumption
(or (or (or (not b417)  (not b808) )  b931 )  (> r2 4) )
  :assumption
(or (not b931)  (<= r2 4) )
  :assumption
(or (or (or (not b408)  (not b805) )  (<= r339 4) )  (>= r314 4) )
  :assumption
(or (<= r2 4)  (>= r341 4) )
  :assumption
(or (= r343 0)  b940 )
  :assumption
(or (not b940)  (= r343 (* (- r89 r80) (/ 1 10))) )
  :assumption
(or (or (or (not b426)  (not b811) )  b940 )  (> r1 4) )
  :assumption
(or (not b940)  (<= r1 4) )
  :assumption
(or b811  (not b940) )
  :assumption
(or b426  (not b940) )
  :assumption
(or (or (or (not b426)  (not b811) )  b940 )  (> r11 4) )
  :assumption
(or (not b940)  (<= r11 4) )
  :assumption
(or (or (or (not b417)  (not b808) )  (<= r341 4) )  (>= r2 4) )
  :assumption
(or (<= r11 4)  (>= r1 4) )
  :assumption
(or (= r344 0)  b949 )
  :assumption
(or (not b949)  (= r344 (* (- r98 r89) (/ 1 10))) )
  :assumption
(or (or (or (not b435)  (not b814) )  b949 )  (> r10 4) )
  :assumption
(or (not b949)  (<= r10 4) )
  :assumption
(or b814  (not b949) )
  :assumption
(or b435  (not b949) )
  :assumption
(or (or (or (not b435)  (not b814) )  b949 )  (> r21 4) )
  :assumption
(or (not b949)  (<= r21 4) )
  :assumption
(or (or (or (not b426)  (not b811) )  (<= r1 4) )  (>= r11 4) )
  :assumption
(or (<= r21 4)  (>= r10 4) )
  :assumption
(or (= r345 0)  b958 )
  :assumption
(or (not b958)  (= r345 (* (- r107 r98) (/ 1 10))) )
  :assumption
(or (or (or (not b444)  (not b817) )  b958 )  (> r20 4) )
  :assumption
(or (not b958)  (<= r20 4) )
  :assumption
(or b817  (not b958) )
  :assumption
(or b444  (not b958) )
  :assumption
(or (or (or (not b444)  (not b817) )  b958 )  (> r30 4) )
  :assumption
(or (not b958)  (<= r30 4) )
  :assumption
(or (or (or (not b435)  (not b814) )  (<= r10 4) )  (>= r21 4) )
  :assumption
(or (<= r30 4)  (>= r20 4) )
  :assumption
(or (= r347 0)  b967 )
  :assumption
(or (not b967)  (= r347 (* (- r116 r107) (/ 1 10))) )
  :assumption
(or (or (or (not b453)  (not b820) )  b967 )  (> r29 4) )
  :assumption
(or (not b967)  (<= r29 4) )
  :assumption
(or b820  (not b967) )
  :assumption
(or b453  (not b967) )
  :assumption
(or (or (or (not b453)  (not b820) )  b967 )  (> r39 4) )
  :assumption
(or (not b967)  (<= r39 4) )
  :assumption
(or (or (or (not b444)  (not b817) )  (<= r20 4) )  (>= r30 4) )
  :assumption
(or (<= r39 4)  (>= r29 4) )
  :assumption
(or (= r348 0)  b976 )
  :assumption
(or (not b976)  (= r348 (* (- r19 r116) (/ 1 10))) )
  :assumption
(or (or (or (not b462)  (not b823) )  b976 )  (> r38 4) )
  :assumption
(or (not b976)  (<= r38 4) )
  :assumption
(or b823  (not b976) )
  :assumption
(or b462  (not b976) )
  :assumption
(or (or (or (not b462)  (not b823) )  b976 )  (> r48 4) )
  :assumption
(or (not b976)  (<= r48 4) )
  :assumption
(or (or (or (not b453)  (not b820) )  (<= r29 4) )  (>= r39 4) )
  :assumption
(or (<= r48 4)  (>= r38 4) )
  :assumption
(or (>= r47 4)  (<= r494 4) )
  :assumption
(or (= r349 0)  b987 )
  :assumption
(or (not b987)  (= r349 (* (- r37 r28) (/ 1 10))) )
  :assumption
(or (or (or (not b141)  (not b829) )  b987 )  (> r56 4) )
  :assumption
(or (not b987)  (<= r56 4) )
  :assumption
(or b829  (not b987) )
  :assumption
(or b141  (not b987) )
  :assumption
(or (or (or (not b141)  (not b829) )  b987 )  (> r60 4) )
  :assumption
(or (not b987)  (<= r60 4) )
  :assumption
(or (= r350 0)  b994 )
  :assumption
(or (not b994)  (= r350 (* (- r46 r37) (/ 1 10))) )
  :assumption
(or (or (or (not b152)  (not b831) )  b994 )  (> r59 4) )
  :assumption
(or (not b994)  (<= r59 4) )
  :assumption
(or b831  (not b994) )
  :assumption
(or b152  (not b994) )
  :assumption
(or (or (or (not b152)  (not b831) )  b994 )  (> r66 4) )
  :assumption
(or (not b994)  (<= r66 4) )
  :assumption
(or (or (or (not b141)  (not b829) )  (<= r56 4) )  (>= r60 4) )
  :assumption
(or (<= r66 4)  (>= r59 4) )
  :assumption
(or (= r351 0)  b1003 )
  :assumption
(or (not b1003)  (= r351 (* (- r55 r46) (/ 1 10))) )
  :assumption
(or (or (or (not b162)  (not b833) )  b1003 )  (> r65 4) )
  :assumption
(or (not b1003)  (<= r65 4) )
  :assumption
(or b833  (not b1003) )
  :assumption
(or b162  (not b1003) )
  :assumption
(or (or (or (not b162)  (not b833) )  b1003 )  (> r73 4) )
  :assumption
(or (not b1003)  (<= r73 4) )
  :assumption
(or (or (or (not b152)  (not b831) )  (<= r59 4) )  (>= r66 4) )
  :assumption
(or (<= r73 4)  (>= r65 4) )
  :assumption
(or (= r352 0)  b1012 )
  :assumption
(or (not b1012)  (= r352 (* (- r58 r55) (/ 1 10))) )
  :assumption
(or (or (or (not b172)  (not b835) )  b1012 )  (> r72 4) )
  :assumption
(or (not b1012)  (<= r72 4) )
  :assumption
(or b835  (not b1012) )
  :assumption
(or b172  (not b1012) )
  :assumption
(or (or (or (not b172)  (not b835) )  b1012 )  (> r82 4) )
  :assumption
(or (not b1012)  (<= r82 4) )
  :assumption
(or (or (or (not b162)  (not b833) )  (<= r65 4) )  (>= r73 4) )
  :assumption
(or (<= r82 4)  (>= r72 4) )
  :assumption
(or (= r353 0)  b1021 )
  :assumption
(or (not b1021)  (= r353 (* (- r64 r58) (/ 1 10))) )
  :assumption
(or (or (or (not b182)  (not b837) )  b1021 )  (> r81 4) )
  :assumption
(or (not b1021)  (<= r81 4) )
  :assumption
(or b837  (not b1021) )
  :assumption
(or b182  (not b1021) )
  :assumption
(or (or (or (not b182)  (not b837) )  b1021 )  (> r91 4) )
  :assumption
(or (not b1021)  (<= r91 4) )
  :assumption
(or (or (or (not b172)  (not b835) )  (<= r72 4) )  (>= r82 4) )
  :assumption
(or (<= r91 4)  (>= r81 4) )
  :assumption
(or (= r354 0)  b1030 )
  :assumption
(or (not b1030)  (= r354 (* (- r71 r64) (/ 1 10))) )
  :assumption
(or (or (or (not b192)  (not b839) )  b1030 )  (> r90 4) )
  :assumption
(or (not b1030)  (<= r90 4) )
  :assumption
(or b839  (not b1030) )
  :assumption
(or b192  (not b1030) )
  :assumption
(or (or (or (not b192)  (not b839) )  b1030 )  (> r100 4) )
  :assumption
(or (not b1030)  (<= r100 4) )
  :assumption
(or (or (or (not b182)  (not b837) )  (<= r81 4) )  (>= r91 4) )
  :assumption
(or (<= r100 4)  (>= r90 4) )
  :assumption
(or (= r355 0)  b1039 )
  :assumption
(or (not b1039)  (= r355 (* (- r80 r71) (/ 1 10))) )
  :assumption
(or (or (or (not b202)  (not b841) )  b1039 )  (> r99 4) )
  :assumption
(or (not b1039)  (<= r99 4) )
  :assumption
(or b841  (not b1039) )
  :assumption
(or b202  (not b1039) )
  :assumption
(or (or (or (not b202)  (not b841) )  b1039 )  (> r109 4) )
  :assumption
(or (not b1039)  (<= r109 4) )
  :assumption
(or (or (or (not b192)  (not b839) )  (<= r90 4) )  (>= r100 4) )
  :assumption
(or (<= r109 4)  (>= r99 4) )
  :assumption
(or (= r356 0)  b1048 )
  :assumption
(or (not b1048)  (= r356 (* (- r89 r80) (/ 1 10))) )
  :assumption
(or (or (or (not b212)  (not b843) )  b1048 )  (> r108 4) )
  :assumption
(or (not b1048)  (<= r108 4) )
  :assumption
(or b843  (not b1048) )
  :assumption
(or b212  (not b1048) )
  :assumption
(or (or (or (not b212)  (not b843) )  b1048 )  (> r118 4) )
  :assumption
(or (not b1048)  (<= r118 4) )
  :assumption
(or (or (or (not b202)  (not b841) )  (<= r99 4) )  (>= r109 4) )
  :assumption
(or (<= r118 4)  (>= r108 4) )
  :assumption
(or (= r358 0)  b1057 )
  :assumption
(or (not b1057)  (= r358 (* (- r98 r89) (/ 1 10))) )
  :assumption
(or (or (or (not b222)  (not b845) )  b1057 )  (> r117 4) )
  :assumption
(or (not b1057)  (<= r117 4) )
  :assumption
(or b845  (not b1057) )
  :assumption
(or b222  (not b1057) )
  :assumption
(or (or (or (not b222)  (not b845) )  b1057 )  (> r126 4) )
  :assumption
(or (not b1057)  (<= r126 4) )
  :assumption
(or (or (or (not b212)  (not b843) )  (<= r108 4) )  (>= r118 4) )
  :assumption
(or (<= r126 4)  (>= r117 4) )
  :assumption
(or (= r359 0)  b1066 )
  :assumption
(or (not b1066)  (= r359 (* (- r107 r98) (/ 1 10))) )
  :assumption
(or (or (or (not b232)  (not b847) )  b1066 )  (> r125 4) )
  :assumption
(or (not b1066)  (<= r125 4) )
  :assumption
(or b847  (not b1066) )
  :assumption
(or b232  (not b1066) )
  :assumption
(or (or (or (not b232)  (not b847) )  b1066 )  (> r135 4) )
  :assumption
(or (not b1066)  (<= r135 4) )
  :assumption
(or (or (or (not b222)  (not b845) )  (<= r117 4) )  (>= r126 4) )
  :assumption
(or (<= r135 4)  (>= r125 4) )
  :assumption
(or (= r360 0)  b1075 )
  :assumption
(or (not b1075)  (= r360 (* (- r116 r107) (/ 1 10))) )
  :assumption
(or (or (or (not b242)  (not b849) )  b1075 )  (> r134 4) )
  :assumption
(or (not b1075)  (<= r134 4) )
  :assumption
(or b849  (not b1075) )
  :assumption
(or b242  (not b1075) )
  :assumption
(or (or (or (not b242)  (not b849) )  b1075 )  (> r144 4) )
  :assumption
(or (not b1075)  (<= r144 4) )
  :assumption
(or (or (or (not b232)  (not b847) )  (<= r125 4) )  (>= r135 4) )
  :assumption
(or (<= r144 4)  (>= r134 4) )
  :assumption
(or (= r361 0)  b1084 )
  :assumption
(or (not b1084)  (= r361 (* (- r19 r116) (/ 1 10))) )
  :assumption
(or (or (or (not b252)  (not b851) )  b1084 )  (> r143 4) )
  :assumption
(or (not b1084)  (<= r143 4) )
  :assumption
(or b851  (not b1084) )
  :assumption
(or b252  (not b1084) )
  :assumption
(or (or (or (not b252)  (not b851) )  b1084 )  (> r153 4) )
  :assumption
(or (not b1084)  (<= r153 4) )
  :assumption
(or (or (or (not b242)  (not b849) )  (<= r134 4) )  (>= r144 4) )
  :assumption
(or (<= r153 4)  (>= r143 4) )
  :assumption
(or (>= r152 4)  (<= r495 4) )
  :assumption
(or b41  (not b1094) )
  :assumption
(or (not b272)  (not b1094) )
  :assumption
(or b29  (not b1094) )
  :assumption
(or b262  (not b1094) )
  :assumption
(or b52  (not b1095) )
  :assumption
(or (not b282)  (not b1095) )
  :assumption
(or b40  (not b1095) )
  :assumption
(or b272  (not b1095) )
  :assumption
(or b63  (not b1096) )
  :assumption
(or (not b292)  (not b1096) )
  :assumption
(or b51  (not b1096) )
  :assumption
(or b282  (not b1096) )
  :assumption
(or b74  (not b1097) )
  :assumption
(or (not b302)  (not b1097) )
  :assumption
(or b62  (not b1097) )
  :assumption
(or b292  (not b1097) )
  :assumption
(or b85  (not b1098) )
  :assumption
(or (not b312)  (not b1098) )
  :assumption
(or b73  (not b1098) )
  :assumption
(or b302  (not b1098) )
  :assumption
(or b96  (not b1099) )
  :assumption
(or (not b322)  (not b1099) )
  :assumption
(or b84  (not b1099) )
  :assumption
(or b312  (not b1099) )
  :assumption
(or b107  (not b1100) )
  :assumption
(or (not b332)  (not b1100) )
  :assumption
(or b95  (not b1100) )
  :assumption
(or b322  (not b1100) )
  :assumption
(or b118  (not b1101) )
  :assumption
(or (not b342)  (not b1101) )
  :assumption
(or b106  (not b1101) )
  :assumption
(or b332  (not b1101) )
  :assumption
(or b129  (not b1102) )
  :assumption
(or (not b352)  (not b1102) )
  :assumption
(or b117  (not b1102) )
  :assumption
(or b342  (not b1102) )
  :assumption
(or (not b1103)  b1104 )
  :assumption
(or (not b1103)  (not b1105) )
  :assumption
(or b128  (not b1103) )
  :assumption
(or b352  (not b1103) )
  :assumption
(or b140  (not b1106) )
  :assumption
(or (not b362)  (not b1106) )
  :assumption
(or b151  (not b1107) )
  :assumption
(or (not b372)  (not b1107) )
  :assumption
(or b139  (not b1107) )
  :assumption
(or b362  (not b1107) )
  :assumption
(or b30  (not b1108) )
  :assumption
(or (not b381)  (not b1108) )
  :assumption
(or b150  (not b1108) )
  :assumption
(or b372  (not b1108) )
  :assumption
(or b41  (not b1109) )
  :assumption
(or (not b390)  (not b1109) )
  :assumption
(or b161  (not b1109) )
  :assumption
(or b381  (not b1109) )
  :assumption
(or b52  (not b1110) )
  :assumption
(or (not b399)  (not b1110) )
  :assumption
(or b171  (not b1110) )
  :assumption
(or b390  (not b1110) )
  :assumption
(or b63  (not b1111) )
  :assumption
(or (not b408)  (not b1111) )
  :assumption
(or b181  (not b1111) )
  :assumption
(or b399  (not b1111) )
  :assumption
(or b74  (not b1112) )
  :assumption
(or (not b417)  (not b1112) )
  :assumption
(or b191  (not b1112) )
  :assumption
(or b408  (not b1112) )
  :assumption
(or b85  (not b1113) )
  :assumption
(or (not b426)  (not b1113) )
  :assumption
(or b201  (not b1113) )
  :assumption
(or b417  (not b1113) )
  :assumption
(or b96  (not b1114) )
  :assumption
(or (not b435)  (not b1114) )
  :assumption
(or b211  (not b1114) )
  :assumption
(or b426  (not b1114) )
  :assumption
(or b107  (not b1115) )
  :assumption
(or (not b444)  (not b1115) )
  :assumption
(or b221  (not b1115) )
  :assumption
(or b435  (not b1115) )
  :assumption
(or b118  (not b1116) )
  :assumption
(or (not b453)  (not b1116) )
  :assumption
(or b231  (not b1116) )
  :assumption
(or b444  (not b1116) )
  :assumption
(or b129  (not b1117) )
  :assumption
(or (not b462)  (not b1117) )
  :assumption
(or b241  (not b1117) )
  :assumption
(or b453  (not b1117) )
  :assumption
(or b1104  (not b1118) )
  :assumption
(or (not b1118)  (not b1119) )
  :assumption
(or b251  (not b1118) )
  :assumption
(or b462  (not b1118) )
  :assumption
(or b271  (not b1120) )
  :assumption
(or (not b42)  (not b1120) )
  :assumption
(or b29  (not b1120) )
  :assumption
(or b31  (not b1120) )
  :assumption
(or b281  (not b1121) )
  :assumption
(or (not b53)  (not b1121) )
  :assumption
(or b40  (not b1121) )
  :assumption
(or b42  (not b1121) )
  :assumption
(or b291  (not b1122) )
  :assumption
(or (not b64)  (not b1122) )
  :assumption
(or b51  (not b1122) )
  :assumption
(or b53  (not b1122) )
  :assumption
(or b301  (not b1123) )
  :assumption
(or (not b75)  (not b1123) )
  :assumption
(or b62  (not b1123) )
  :assumption
(or b64  (not b1123) )
  :assumption
(or b311  (not b1124) )
  :assumption
(or (not b86)  (not b1124) )
  :assumption
(or b73  (not b1124) )
  :assumption
(or b75  (not b1124) )
  :assumption
(or b321  (not b1125) )
  :assumption
(or (not b97)  (not b1125) )
  :assumption
(or b84  (not b1125) )
  :assumption
(or b86  (not b1125) )
  :assumption
(or b331  (not b1126) )
  :assumption
(or (not b108)  (not b1126) )
  :assumption
(or b95  (not b1126) )
  :assumption
(or b97  (not b1126) )
  :assumption
(or b341  (not b1127) )
  :assumption
(or (not b119)  (not b1127) )
  :assumption
(or b106  (not b1127) )
  :assumption
(or b108  (not b1127) )
  :assumption
(or b351  (not b1128) )
  :assumption
(or (not b130)  (not b1128) )
  :assumption
(or b117  (not b1128) )
  :assumption
(or b119  (not b1128) )
  :assumption
(or (not b1129)  b1130 )
  :assumption
(or (not b1129)  (not b1131) )
  :assumption
(or b128  (not b1129) )
  :assumption
(or b130  (not b1129) )
  :assumption
(or b361  (not b1132) )
  :assumption
(or (not b141)  (not b1132) )
  :assumption
(or b371  (not b1133) )
  :assumption
(or (not b152)  (not b1133) )
  :assumption
(or b139  (not b1133) )
  :assumption
(or b141  (not b1133) )
  :assumption
(or b261  (not b1134) )
  :assumption
(or (not b162)  (not b1134) )
  :assumption
(or b150  (not b1134) )
  :assumption
(or b152  (not b1134) )
  :assumption
(or b271  (not b1135) )
  :assumption
(or (not b172)  (not b1135) )
  :assumption
(or b161  (not b1135) )
  :assumption
(or b162  (not b1135) )
  :assumption
(or b281  (not b1136) )
  :assumption
(or (not b182)  (not b1136) )
  :assumption
(or b171  (not b1136) )
  :assumption
(or b172  (not b1136) )
  :assumption
(or b291  (not b1137) )
  :assumption
(or (not b192)  (not b1137) )
  :assumption
(or b181  (not b1137) )
  :assumption
(or b182  (not b1137) )
  :assumption
(or b301  (not b1138) )
  :assumption
(or (not b202)  (not b1138) )
  :assumption
(or b191  (not b1138) )
  :assumption
(or b192  (not b1138) )
  :assumption
(or b311  (not b1139) )
  :assumption
(or (not b212)  (not b1139) )
  :assumption
(or b201  (not b1139) )
  :assumption
(or b202  (not b1139) )
  :assumption
(or b321  (not b1140) )
  :assumption
(or (not b222)  (not b1140) )
  :assumption
(or b211  (not b1140) )
  :assumption
(or b212  (not b1140) )
  :assumption
(or b331  (not b1141) )
  :assumption
(or (not b232)  (not b1141) )
  :assumption
(or b221  (not b1141) )
  :assumption
(or b222  (not b1141) )
  :assumption
(or b341  (not b1142) )
  :assumption
(or (not b242)  (not b1142) )
  :assumption
(or b231  (not b1142) )
  :assumption
(or b232  (not b1142) )
  :assumption
(or b351  (not b1143) )
  :assumption
(or (not b252)  (not b1143) )
  :assumption
(or b241  (not b1143) )
  :assumption
(or b242  (not b1143) )
  :assumption
(or b1130  (not b1144) )
  :assumption
(or (not b1144)  (not b1145) )
  :assumption
(or b251  (not b1144) )
  :assumption
(or b252  (not b1144) )
  :assumption
(or (not b30)  (not b1146) )
  :assumption
(or b262  (not b1146) )
  :assumption
(or b471  (not b1146) )
  :assumption
(or b151  (not b1146) )
  :assumption
(or (not b41)  (not b1147) )
  :assumption
(or b272  (not b1147) )
  :assumption
(or b29  (not b1147) )
  :assumption
(or b30  (not b1147) )
  :assumption
(or (not b52)  (not b1148) )
  :assumption
(or b282  (not b1148) )
  :assumption
(or b40  (not b1148) )
  :assumption
(or b41  (not b1148) )
  :assumption
(or (not b63)  (not b1149) )
  :assumption
(or b292  (not b1149) )
  :assumption
(or b51  (not b1149) )
  :assumption
(or b52  (not b1149) )
  :assumption
(or (not b74)  (not b1150) )
  :assumption
(or b302  (not b1150) )
  :assumption
(or b62  (not b1150) )
  :assumption
(or b63  (not b1150) )
  :assumption
(or (not b85)  (not b1151) )
  :assumption
(or b312  (not b1151) )
  :assumption
(or b73  (not b1151) )
  :assumption
(or b74  (not b1151) )
  :assumption
(or (not b96)  (not b1152) )
  :assumption
(or b322  (not b1152) )
  :assumption
(or b84  (not b1152) )
  :assumption
(or b85  (not b1152) )
  :assumption
(or (not b107)  (not b1153) )
  :assumption
(or b332  (not b1153) )
  :assumption
(or b95  (not b1153) )
  :assumption
(or b96  (not b1153) )
  :assumption
(or (not b118)  (not b1154) )
  :assumption
(or b342  (not b1154) )
  :assumption
(or b106  (not b1154) )
  :assumption
(or b107  (not b1154) )
  :assumption
(or (not b129)  (not b1155) )
  :assumption
(or b352  (not b1155) )
  :assumption
(or b117  (not b1155) )
  :assumption
(or b118  (not b1155) )
  :assumption
(or (not b1104)  (not b1156) )
  :assumption
(or b1105  (not b1156) )
  :assumption
(or b128  (not b1156) )
  :assumption
(or b129  (not b1156) )
  :assumption
(or (not b151)  (not b1157) )
  :assumption
(or b372  (not b1157) )
  :assumption
(or b139  (not b1157) )
  :assumption
(or b140  (not b1157) )
  :assumption
(or (not b30)  (not b1158) )
  :assumption
(or b381  (not b1158) )
  :assumption
(or b150  (not b1158) )
  :assumption
(or b151  (not b1158) )
  :assumption
(or (not b41)  (not b1159) )
  :assumption
(or b390  (not b1159) )
  :assumption
(or b161  (not b1159) )
  :assumption
(or b30  (not b1159) )
  :assumption
(or (not b52)  (not b1160) )
  :assumption
(or b399  (not b1160) )
  :assumption
(or b171  (not b1160) )
  :assumption
(or b41  (not b1160) )
  :assumption
(or (not b63)  (not b1161) )
  :assumption
(or b408  (not b1161) )
  :assumption
(or b181  (not b1161) )
  :assumption
(or b52  (not b1161) )
  :assumption
(or (not b74)  (not b1162) )
  :assumption
(or b417  (not b1162) )
  :assumption
(or b191  (not b1162) )
  :assumption
(or b63  (not b1162) )
  :assumption
(or (not b85)  (not b1163) )
  :assumption
(or b426  (not b1163) )
  :assumption
(or b201  (not b1163) )
  :assumption
(or b74  (not b1163) )
  :assumption
(or (not b96)  (not b1164) )
  :assumption
(or b435  (not b1164) )
  :assumption
(or b211  (not b1164) )
  :assumption
(or b85  (not b1164) )
  :assumption
(or (not b107)  (not b1165) )
  :assumption
(or b444  (not b1165) )
  :assumption
(or b221  (not b1165) )
  :assumption
(or b96  (not b1165) )
  :assumption
(or (not b118)  (not b1166) )
  :assumption
(or b453  (not b1166) )
  :assumption
(or b231  (not b1166) )
  :assumption
(or b107  (not b1166) )
  :assumption
(or (not b129)  (not b1167) )
  :assumption
(or b462  (not b1167) )
  :assumption
(or b241  (not b1167) )
  :assumption
(or b118  (not b1167) )
  :assumption
(or (not b1104)  (not b1168) )
  :assumption
(or b1119  (not b1168) )
  :assumption
(or b251  (not b1168) )
  :assumption
(or b129  (not b1168) )
  :assumption
(or (not b261)  (not b1169) )
  :assumption
(or b31  (not b1169) )
  :assumption
(or b471  (not b1169) )
  :assumption
(or b371  (not b1169) )
  :assumption
(or (not b271)  (not b1170) )
  :assumption
(or b42  (not b1170) )
  :assumption
(or b29  (not b1170) )
  :assumption
(or b261  (not b1170) )
  :assumption
(or (not b281)  (not b1171) )
  :assumption
(or b53  (not b1171) )
  :assumption
(or b40  (not b1171) )
  :assumption
(or b271  (not b1171) )
  :assumption
(or (not b291)  (not b1172) )
  :assumption
(or b64  (not b1172) )
  :assumption
(or b51  (not b1172) )
  :assumption
(or b281  (not b1172) )
  :assumption
(or (not b301)  (not b1173) )
  :assumption
(or b75  (not b1173) )
  :assumption
(or b62  (not b1173) )
  :assumption
(or b291  (not b1173) )
  :assumption
(or (not b311)  (not b1174) )
  :assumption
(or b86  (not b1174) )
  :assumption
(or b73  (not b1174) )
  :assumption
(or b301  (not b1174) )
  :assumption
(or (not b321)  (not b1175) )
  :assumption
(or b97  (not b1175) )
  :assumption
(or b84  (not b1175) )
  :assumption
(or b311  (not b1175) )
  :assumption
(or (not b331)  (not b1176) )
  :assumption
(or b108  (not b1176) )
  :assumption
(or b95  (not b1176) )
  :assumption
(or b321  (not b1176) )
  :assumption
(or (not b341)  (not b1177) )
  :assumption
(or b119  (not b1177) )
  :assumption
(or b106  (not b1177) )
  :assumption
(or b331  (not b1177) )
  :assumption
(or (not b351)  (not b1178) )
  :assumption
(or b130  (not b1178) )
  :assumption
(or b117  (not b1178) )
  :assumption
(or b341  (not b1178) )
  :assumption
(or (not b1130)  (not b1179) )
  :assumption
(or b1131  (not b1179) )
  :assumption
(or b128  (not b1179) )
  :assumption
(or b351  (not b1179) )
  :assumption
(or (not b371)  (not b1180) )
  :assumption
(or b152  (not b1180) )
  :assumption
(or b139  (not b1180) )
  :assumption
(or b361  (not b1180) )
  :assumption
(or (not b261)  (not b1181) )
  :assumption
(or b162  (not b1181) )
  :assumption
(or b150  (not b1181) )
  :assumption
(or b371  (not b1181) )
  :assumption
(or (not b271)  (not b1182) )
  :assumption
(or b172  (not b1182) )
  :assumption
(or b161  (not b1182) )
  :assumption
(or b261  (not b1182) )
  :assumption
(or (not b281)  (not b1183) )
  :assumption
(or b182  (not b1183) )
  :assumption
(or b171  (not b1183) )
  :assumption
(or b271  (not b1183) )
  :assumption
(or (not b291)  (not b1184) )
  :assumption
(or b192  (not b1184) )
  :assumption
(or b181  (not b1184) )
  :assumption
(or b281  (not b1184) )
  :assumption
(or (not b301)  (not b1185) )
  :assumption
(or b202  (not b1185) )
  :assumption
(or b191  (not b1185) )
  :assumption
(or b291  (not b1185) )
  :assumption
(or (not b311)  (not b1186) )
  :assumption
(or b212  (not b1186) )
  :assumption
(or b201  (not b1186) )
  :assumption
(or b301  (not b1186) )
  :assumption
(or (not b321)  (not b1187) )
  :assumption
(or b222  (not b1187) )
  :assumption
(or b211  (not b1187) )
  :assumption
(or b311  (not b1187) )
  :assumption
(or (not b331)  (not b1188) )
  :assumption
(or b232  (not b1188) )
  :assumption
(or b221  (not b1188) )
  :assumption
(or b321  (not b1188) )
  :assumption
(or (not b341)  (not b1189) )
  :assumption
(or b242  (not b1189) )
  :assumption
(or b231  (not b1189) )
  :assumption
(or b331  (not b1189) )
  :assumption
(or (not b351)  (not b1190) )
  :assumption
(or b252  (not b1190) )
  :assumption
(or b241  (not b1190) )
  :assumption
(or b341  (not b1190) )
  :assumption
(or (not b1130)  (not b1191) )
  :assumption
(or b1145  (not b1191) )
  :assumption
(or b251  (not b1191) )
  :assumption
(or b351  (not b1191) )
  :assumption
(or (not b1192)  (= r302 100) )
  :assumption
(or (not b1192)  b1194 )
  :assumption
(or (not b29)  (not b1192) )
  :assumption
(or b471  (not b1192) )
  :assumption
(or (not b1195)  (= r304 100) )
  :assumption
(or (not b1195)  b1197 )
  :assumption
(or (not b40)  (not b1195) )
  :assumption
(or b29  (not b1195) )
  :assumption
(or (not b1194)  (not b1195) )
  :assumption
(or (not b1198)  (= r306 100) )
  :assumption
(or (not b1198)  b1200 )
  :assumption
(or (not b51)  (not b1198) )
  :assumption
(or b40  (not b1198) )
  :assumption
(or (not b1197)  (not b1198) )
  :assumption
(or (not b1201)  (= r308 100) )
  :assumption
(or (not b1201)  b1203 )
  :assumption
(or (not b62)  (not b1201) )
  :assumption
(or b51  (not b1201) )
  :assumption
(or (not b1200)  (not b1201) )
  :assumption
(or (not b1204)  (= r310 100) )
  :assumption
(or (not b1204)  b1206 )
  :assumption
(or (not b73)  (not b1204) )
  :assumption
(or b62  (not b1204) )
  :assumption
(or (not b1203)  (not b1204) )
  :assumption
(or (not b1207)  (= r312 100) )
  :assumption
(or (not b1207)  b1209 )
  :assumption
(or (not b84)  (not b1207) )
  :assumption
(or b73  (not b1207) )
  :assumption
(or (not b1206)  (not b1207) )
  :assumption
(or (not b1210)  (= r315 100) )
  :assumption
(or (not b1210)  b1212 )
  :assumption
(or (not b95)  (not b1210) )
  :assumption
(or b84  (not b1210) )
  :assumption
(or (not b1209)  (not b1210) )
  :assumption
(or (not b1213)  (= r317 100) )
  :assumption
(or (not b1213)  b1215 )
  :assumption
(or (not b106)  (not b1213) )
  :assumption
(or b95  (not b1213) )
  :assumption
(or (not b1212)  (not b1213) )
  :assumption
(or (not b1216)  (= r319 100) )
  :assumption
(or (not b1216)  b1218 )
  :assumption
(or (not b117)  (not b1216) )
  :assumption
(or b106  (not b1216) )
  :assumption
(or (not b1215)  (not b1216) )
  :assumption
(or (not b1219)  (= r321 100) )
  :assumption
(or (not b1219)  b1221 )
  :assumption
(or (not b128)  (not b1219) )
  :assumption
(or b117  (not b1219) )
  :assumption
(or (not b1218)  (not b1219) )
  :assumption
(or (not b1222)  (= r323 100) )
  :assumption
(or (not b1222)  b1224 )
  :assumption
(or (not b1222)  (not b1225) )
  :assumption
(or b128  (not b1222) )
  :assumption
(or (not b1221)  (not b1222) )
  :assumption
(or (not b1226)  (= r267 100) )
  :assumption
(or (not b1226)  b1228 )
  :assumption
(or (not b139)  (not b1226) )
  :assumption
(or (not b1229)  (= r270 100) )
  :assumption
(or (not b1229)  b1231 )
  :assumption
(or (not b150)  (not b1229) )
  :assumption
(or b139  (not b1229) )
  :assumption
(or (not b1228)  (not b1229) )
  :assumption
(or (not b1232)  (= r272 100) )
  :assumption
(or (not b1232)  b1234 )
  :assumption
(or (not b161)  (not b1232) )
  :assumption
(or b150  (not b1232) )
  :assumption
(or (not b1231)  (not b1232) )
  :assumption
(or (not b1235)  (= r274 100) )
  :assumption
(or (not b1235)  b1237 )
  :assumption
(or (not b171)  (not b1235) )
  :assumption
(or b161  (not b1235) )
  :assumption
(or (not b1234)  (not b1235) )
  :assumption
(or (not b1238)  (= r277 100) )
  :assumption
(or (not b1238)  b1240 )
  :assumption
(or (not b181)  (not b1238) )
  :assumption
(or b171  (not b1238) )
  :assumption
(or (not b1237)  (not b1238) )
  :assumption
(or (not b1241)  (= r279 100) )
  :assumption
(or (not b1241)  b1243 )
  :assumption
(or (not b191)  (not b1241) )
  :assumption
(or b181  (not b1241) )
  :assumption
(or (not b1240)  (not b1241) )
  :assumption
(or (not b1244)  (= r281 100) )
  :assumption
(or (not b1244)  b1246 )
  :assumption
(or (not b201)  (not b1244) )
  :assumption
(or b191  (not b1244) )
  :assumption
(or (not b1243)  (not b1244) )
  :assumption
(or (not b1247)  (= r283 100) )
  :assumption
(or (not b1247)  b1249 )
  :assumption
(or (not b211)  (not b1247) )
  :assumption
(or b201  (not b1247) )
  :assumption
(or (not b1246)  (not b1247) )
  :assumption
(or (not b1250)  (= r285 100) )
  :assumption
(or (not b1250)  b1252 )
  :assumption
(or (not b221)  (not b1250) )
  :assumption
(or b211  (not b1250) )
  :assumption
(or (not b1249)  (not b1250) )
  :assumption
(or (not b1253)  (= r287 100) )
  :assumption
(or (not b1253)  b1255 )
  :assumption
(or (not b231)  (not b1253) )
  :assumption
(or b221  (not b1253) )
  :assumption
(or (not b1252)  (not b1253) )
  :assumption
(or (not b1256)  (= r290 100) )
  :assumption
(or (not b1256)  b1258 )
  :assumption
(or (not b241)  (not b1256) )
  :assumption
(or b231  (not b1256) )
  :assumption
(or (not b1255)  (not b1256) )
  :assumption
(or (not b1259)  (= r292 100) )
  :assumption
(or (not b1259)  b1261 )
  :assumption
(or (not b251)  (not b1259) )
  :assumption
(or b241  (not b1259) )
  :assumption
(or (not b1258)  (not b1259) )
  :assumption
(or (not b1262)  (= r295 100) )
  :assumption
(or (not b1262)  b1264 )
  :assumption
(or (not b1262)  (not b1265) )
  :assumption
(or b251  (not b1262) )
  :assumption
(or (not b1261)  (not b1262) )
  :assumption
(or (= r364 0)  b1267 )
  :assumption
(or (not b1267)  (= r364 (* (~ (- r37 r28)) 5)) )
  :assumption
(or (or (not b1228)  b1267 )  (< r267 0) )
  :assumption
(or (not b1267)  (>= r267 0) )
  :assumption
(or b1228  (not b1267) )
  :assumption
(or (or (not b1228)  b1267 )  (< r271 0) )
  :assumption
(or (not b1267)  (>= r271 0) )
  :assumption
(or (= r365 0)  b1274 )
  :assumption
(or (not b1274)  (= r365 (* (~ (- r46 r37)) 5)) )
  :assumption
(or (or (not b1231)  b1274 )  (< r270 0) )
  :assumption
(or (not b1274)  (>= r270 0) )
  :assumption
(or b1231  (not b1274) )
  :assumption
(or (or (not b1231)  b1274 )  (< r273 0) )
  :assumption
(or (not b1274)  (>= r273 0) )
  :assumption
(or (or (not b1228)  (>= r267 0) )  (<= r271 0) )
  :assumption
(or (>= r273 0)  (<= r270 0) )
  :assumption
(or (= r367 0)  b1283 )
  :assumption
(or (not b1283)  (= r367 (* (~ (- r55 r46)) 5)) )
  :assumption
(or (or (not b1234)  b1283 )  (< r272 0) )
  :assumption
(or (not b1283)  (>= r272 0) )
  :assumption
(or b1234  (not b1283) )
  :assumption
(or (or (not b1234)  b1283 )  (< r275 0) )
  :assumption
(or (not b1283)  (>= r275 0) )
  :assumption
(or (or (not b1231)  (>= r270 0) )  (<= r273 0) )
  :assumption
(or (>= r275 0)  (<= r272 0) )
  :assumption
(or (= r368 0)  b1292 )
  :assumption
(or (not b1292)  (= r368 (* (~ (- r58 r55)) 5)) )
  :assumption
(or (or (not b1237)  b1292 )  (< r274 0) )
  :assumption
(or (not b1292)  (>= r274 0) )
  :assumption
(or b1237  (not b1292) )
  :assumption
(or (or (not b1237)  b1292 )  (< r278 0) )
  :assumption
(or (not b1292)  (>= r278 0) )
  :assumption
(or (or (not b1234)  (>= r272 0) )  (<= r275 0) )
  :assumption
(or (>= r278 0)  (<= r274 0) )
  :assumption
(or (= r369 0)  b1301 )
  :assumption
(or (not b1301)  (= r369 (* (~ (- r64 r58)) 5)) )
  :assumption
(or (or (not b1240)  b1301 )  (< r277 0) )
  :assumption
(or (not b1301)  (>= r277 0) )
  :assumption
(or b1240  (not b1301) )
  :assumption
(or (or (not b1240)  b1301 )  (< r280 0) )
  :assumption
(or (not b1301)  (>= r280 0) )
  :assumption
(or (or (not b1237)  (>= r274 0) )  (<= r278 0) )
  :assumption
(or (>= r280 0)  (<= r277 0) )
  :assumption
(or (= r370 0)  b1310 )
  :assumption
(or (not b1310)  (= r370 (* (~ (- r71 r64)) 5)) )
  :assumption
(or (or (not b1243)  b1310 )  (< r279 0) )
  :assumption
(or (not b1310)  (>= r279 0) )
  :assumption
(or b1243  (not b1310) )
  :assumption
(or (or (not b1243)  b1310 )  (< r282 0) )
  :assumption
(or (not b1310)  (>= r282 0) )
  :assumption
(or (or (not b1240)  (>= r277 0) )  (<= r280 0) )
  :assumption
(or (>= r282 0)  (<= r279 0) )
  :assumption
(or (= r371 0)  b1319 )
  :assumption
(or (not b1319)  (= r371 (* (~ (- r80 r71)) 5)) )
  :assumption
(or (or (not b1246)  b1319 )  (< r281 0) )
  :assumption
(or (not b1319)  (>= r281 0) )
  :assumption
(or b1246  (not b1319) )
  :assumption
(or (or (not b1246)  b1319 )  (< r284 0) )
  :assumption
(or (not b1319)  (>= r284 0) )
  :assumption
(or (or (not b1243)  (>= r279 0) )  (<= r282 0) )
  :assumption
(or (>= r284 0)  (<= r281 0) )
  :assumption
(or (= r372 0)  b1328 )
  :assumption
(or (not b1328)  (= r372 (* (~ (- r89 r80)) 5)) )
  :assumption
(or (or (not b1249)  b1328 )  (< r283 0) )
  :assumption
(or (not b1328)  (>= r283 0) )
  :assumption
(or b1249  (not b1328) )
  :assumption
(or (or (not b1249)  b1328 )  (< r286 0) )
  :assumption
(or (not b1328)  (>= r286 0) )
  :assumption
(or (or (not b1246)  (>= r281 0) )  (<= r284 0) )
  :assumption
(or (>= r286 0)  (<= r283 0) )
  :assumption
(or (= r373 0)  b1337 )
  :assumption
(or (not b1337)  (= r373 (* (~ (- r98 r89)) 5)) )
  :assumption
(or (or (not b1252)  b1337 )  (< r285 0) )
  :assumption
(or (not b1337)  (>= r285 0) )
  :assumption
(or b1252  (not b1337) )
  :assumption
(or (or (not b1252)  b1337 )  (< r288 0) )
  :assumption
(or (not b1337)  (>= r288 0) )
  :assumption
(or (or (not b1249)  (>= r283 0) )  (<= r286 0) )
  :assumption
(or (>= r288 0)  (<= r285 0) )
  :assumption
(or (= r374 0)  b1346 )
  :assumption
(or (not b1346)  (= r374 (* (~ (- r107 r98)) 5)) )
  :assumption
(or (or (not b1255)  b1346 )  (< r287 0) )
  :assumption
(or (not b1346)  (>= r287 0) )
  :assumption
(or b1255  (not b1346) )
  :assumption
(or (or (not b1255)  b1346 )  (< r291 0) )
  :assumption
(or (not b1346)  (>= r291 0) )
  :assumption
(or (or (not b1252)  (>= r285 0) )  (<= r288 0) )
  :assumption
(or (>= r291 0)  (<= r287 0) )
  :assumption
(or (= r376 0)  b1355 )
  :assumption
(or (not b1355)  (= r376 (* (~ (- r116 r107)) 5)) )
  :assumption
(or (or (not b1258)  b1355 )  (< r290 0) )
  :assumption
(or (not b1355)  (>= r290 0) )
  :assumption
(or b1258  (not b1355) )
  :assumption
(or (or (not b1258)  b1355 )  (< r293 0) )
  :assumption
(or (not b1355)  (>= r293 0) )
  :assumption
(or (or (not b1255)  (>= r287 0) )  (<= r291 0) )
  :assumption
(or (>= r293 0)  (<= r290 0) )
  :assumption
(or (= r377 0)  b1364 )
  :assumption
(or (not b1364)  (= r377 (* (~ (- r19 r116)) 5)) )
  :assumption
(or (or (not b1261)  b1364 )  (< r292 0) )
  :assumption
(or (not b1364)  (>= r292 0) )
  :assumption
(or b1261  (not b1364) )
  :assumption
(or (or (not b1261)  b1364 )  (< r296 0) )
  :assumption
(or (not b1364)  (>= r296 0) )
  :assumption
(or (or (not b1258)  (>= r290 0) )  (<= r293 0) )
  :assumption
(or (>= r296 0)  (<= r292 0) )
  :assumption
(or (<= r295 0)  (>= r496 0) )
  :assumption
(or (= r379 0)  b1375 )
  :assumption
(or (not b1375)  (= r379 (* (~ (- r55 r46)) 5)) )
  :assumption
(or (or (not b1194)  b1375 )  (< r302 0) )
  :assumption
(or (not b1375)  (>= r302 0) )
  :assumption
(or b1194  (not b1375) )
  :assumption
(or (or (not b1194)  b1375 )  (< r305 0) )
  :assumption
(or (not b1375)  (>= r305 0) )
  :assumption
(or (>= r305 0)  (<= r302 0) )
  :assumption
(or (= r380 0)  b1383 )
  :assumption
(or (not b1383)  (= r380 (* (~ (- r58 r55)) 5)) )
  :assumption
(or (or (not b1197)  b1383 )  (< r304 0) )
  :assumption
(or (not b1383)  (>= r304 0) )
  :assumption
(or b1197  (not b1383) )
  :assumption
(or (or (not b1197)  b1383 )  (< r307 0) )
  :assumption
(or (not b1383)  (>= r307 0) )
  :assumption
(or (or (not b1194)  (>= r302 0) )  (<= r305 0) )
  :assumption
(or (>= r307 0)  (<= r304 0) )
  :assumption
(or (= r381 0)  b1392 )
  :assumption
(or (not b1392)  (= r381 (* (~ (- r64 r58)) 5)) )
  :assumption
(or (or (not b1200)  b1392 )  (< r306 0) )
  :assumption
(or (not b1392)  (>= r306 0) )
  :assumption
(or b1200  (not b1392) )
  :assumption
(or (or (not b1200)  b1392 )  (< r309 0) )
  :assumption
(or (not b1392)  (>= r309 0) )
  :assumption
(or (or (not b1197)  (>= r304 0) )  (<= r307 0) )
  :assumption
(or (>= r309 0)  (<= r306 0) )
  :assumption
(or (= r382 0)  b1401 )
  :assumption
(or (not b1401)  (= r382 (* (~ (- r71 r64)) 5)) )
  :assumption
(or (or (not b1203)  b1401 )  (< r308 0) )
  :assumption
(or (not b1401)  (>= r308 0) )
  :assumption
(or b1203  (not b1401) )
  :assumption
(or (or (not b1203)  b1401 )  (< r311 0) )
  :assumption
(or (not b1401)  (>= r311 0) )
  :assumption
(or (or (not b1200)  (>= r306 0) )  (<= r309 0) )
  :assumption
(or (>= r311 0)  (<= r308 0) )
  :assumption
(or (= r383 0)  b1410 )
  :assumption
(or (not b1410)  (= r383 (* (~ (- r80 r71)) 5)) )
  :assumption
(or (or (not b1206)  b1410 )  (< r310 0) )
  :assumption
(or (not b1410)  (>= r310 0) )
  :assumption
(or b1206  (not b1410) )
  :assumption
(or (or (not b1206)  b1410 )  (< r313 0) )
  :assumption
(or (not b1410)  (>= r313 0) )
  :assumption
(or (or (not b1203)  (>= r308 0) )  (<= r311 0) )
  :assumption
(or (>= r313 0)  (<= r310 0) )
  :assumption
(or (= r384 0)  b1419 )
  :assumption
(or (not b1419)  (= r384 (* (~ (- r89 r80)) 5)) )
  :assumption
(or (or (not b1209)  b1419 )  (< r312 0) )
  :assumption
(or (not b1419)  (>= r312 0) )
  :assumption
(or b1209  (not b1419) )
  :assumption
(or (or (not b1209)  b1419 )  (< r316 0) )
  :assumption
(or (not b1419)  (>= r316 0) )
  :assumption
(or (or (not b1206)  (>= r310 0) )  (<= r313 0) )
  :assumption
(or (>= r316 0)  (<= r312 0) )
  :assumption
(or (= r386 0)  b1428 )
  :assumption
(or (not b1428)  (= r386 (* (~ (- r98 r89)) 5)) )
  :assumption
(or (or (not b1212)  b1428 )  (< r315 0) )
  :assumption
(or (not b1428)  (>= r315 0) )
  :assumption
(or b1212  (not b1428) )
  :assumption
(or (or (not b1212)  b1428 )  (< r318 0) )
  :assumption
(or (not b1428)  (>= r318 0) )
  :assumption
(or (or (not b1209)  (>= r312 0) )  (<= r316 0) )
  :assumption
(or (>= r318 0)  (<= r315 0) )
  :assumption
(or (= r387 0)  b1437 )
  :assumption
(or (not b1437)  (= r387 (* (~ (- r107 r98)) 5)) )
  :assumption
(or (or (not b1215)  b1437 )  (< r317 0) )
  :assumption
(or (not b1437)  (>= r317 0) )
  :assumption
(or b1215  (not b1437) )
  :assumption
(or (or (not b1215)  b1437 )  (< r320 0) )
  :assumption
(or (not b1437)  (>= r320 0) )
  :assumption
(or (or (not b1212)  (>= r315 0) )  (<= r318 0) )
  :assumption
(or (>= r320 0)  (<= r317 0) )
  :assumption
(or (= r388 0)  b1446 )
  :assumption
(or (not b1446)  (= r388 (* (~ (- r116 r107)) 5)) )
  :assumption
(or (or (not b1218)  b1446 )  (< r319 0) )
  :assumption
(or (not b1446)  (>= r319 0) )
  :assumption
(or b1218  (not b1446) )
  :assumption
(or (or (not b1218)  b1446 )  (< r322 0) )
  :assumption
(or (not b1446)  (>= r322 0) )
  :assumption
(or (or (not b1215)  (>= r317 0) )  (<= r320 0) )
  :assumption
(or (>= r322 0)  (<= r319 0) )
  :assumption
(or (= r390 0)  b1455 )
  :assumption
(or (not b1455)  (= r390 (* (~ (- r19 r116)) 5)) )
  :assumption
(or (or (not b1221)  b1455 )  (< r321 0) )
  :assumption
(or (not b1455)  (>= r321 0) )
  :assumption
(or b1221  (not b1455) )
  :assumption
(or (or (not b1221)  b1455 )  (< r324 0) )
  :assumption
(or (not b1455)  (>= r324 0) )
  :assumption
(or (or (not b1218)  (>= r319 0) )  (<= r322 0) )
  :assumption
(or (>= r324 0)  (<= r321 0) )
  :assumption
(or (<= r323 0)  (>= r497 0) )
  :assumption
(or (not b1231)  (not b1465) )
  :assumption
(or b471  (not b1465) )
  :assumption
(or (or (not b1228)  b1465 )  (> r271 0) )
  :assumption
(or (<= r271 0)  (not b1465) )
  :assumption
(or b1228  (not b1465) )
  :assumption
(or (or (not b1228)  (>= r271 0) )  (<= r267 0) )
  :assumption
(or (or (not b1228)  (> r267 0) )  (= r37 r28) )
  :assumption
(or (not b1234)  (not b1470) )
  :assumption
(or b29  (not b1470) )
  :assumption
(or (or (not b1231)  b1470 )  (> r273 0) )
  :assumption
(or (<= r273 0)  (not b1470) )
  :assumption
(or b1231  (not b1470) )
  :assumption
(or (or (not b1231)  (>= r273 0) )  (<= r270 0) )
  :assumption
(or (or (not b1231)  (> r270 0) )  (= r46 r37) )
  :assumption
(or (not b1237)  (not b1474) )
  :assumption
(or b40  (not b1474) )
  :assumption
(or (or (not b1234)  b1474 )  (> r275 0) )
  :assumption
(or (<= r275 0)  (not b1474) )
  :assumption
(or b1234  (not b1474) )
  :assumption
(or (or (not b1234)  (>= r275 0) )  (<= r272 0) )
  :assumption
(or (or (not b1234)  (> r272 0) )  (= r55 r46) )
  :assumption
(or (not b1240)  (not b1478) )
  :assumption
(or b51  (not b1478) )
  :assumption
(or (or (not b1237)  b1478 )  (> r278 0) )
  :assumption
(or (<= r278 0)  (not b1478) )
  :assumption
(or b1237  (not b1478) )
  :assumption
(or (or (not b1237)  (>= r278 0) )  (<= r274 0) )
  :assumption
(or (or (not b1237)  (> r274 0) )  (= r58 r55) )
  :assumption
(or (not b1243)  (not b1482) )
  :assumption
(or b62  (not b1482) )
  :assumption
(or (or (not b1240)  b1482 )  (> r280 0) )
  :assumption
(or (<= r280 0)  (not b1482) )
  :assumption
(or b1240  (not b1482) )
  :assumption
(or (or (not b1240)  (>= r280 0) )  (<= r277 0) )
  :assumption
(or (or (not b1240)  (> r277 0) )  (= r64 r58) )
  :assumption
(or (not b1246)  (not b1486) )
  :assumption
(or b73  (not b1486) )
  :assumption
(or (or (not b1243)  b1486 )  (> r282 0) )
  :assumption
(or (<= r282 0)  (not b1486) )
  :assumption
(or b1243  (not b1486) )
  :assumption
(or (or (not b1243)  (>= r282 0) )  (<= r279 0) )
  :assumption
(or (or (not b1243)  (> r279 0) )  (= r71 r64) )
  :assumption
(or (not b1249)  (not b1490) )
  :assumption
(or b84  (not b1490) )
  :assumption
(or (or (not b1246)  b1490 )  (> r284 0) )
  :assumption
(or (<= r284 0)  (not b1490) )
  :assumption
(or b1246  (not b1490) )
  :assumption
(or (or (not b1246)  (>= r284 0) )  (<= r281 0) )
  :assumption
(or (or (not b1246)  (> r281 0) )  (= r80 r71) )
  :assumption
(or (not b1252)  (not b1494) )
  :assumption
(or b95  (not b1494) )
  :assumption
(or (or (not b1249)  b1494 )  (> r286 0) )
  :assumption
(or (<= r286 0)  (not b1494) )
  :assumption
(or b1249  (not b1494) )
  :assumption
(or (or (not b1249)  (>= r286 0) )  (<= r283 0) )
  :assumption
(or (or (not b1249)  (> r283 0) )  (= r89 r80) )
  :assumption
(or (not b1255)  (not b1498) )
  :assumption
(or b106  (not b1498) )
  :assumption
(or (or (not b1252)  b1498 )  (> r288 0) )
  :assumption
(or (<= r288 0)  (not b1498) )
  :assumption
(or b1252  (not b1498) )
  :assumption
(or (or (not b1252)  (>= r288 0) )  (<= r285 0) )
  :assumption
(or (or (not b1252)  (> r285 0) )  (= r98 r89) )
  :assumption
(or (not b1258)  (not b1502) )
  :assumption
(or b117  (not b1502) )
  :assumption
(or (or (not b1255)  b1502 )  (> r291 0) )
  :assumption
(or (<= r291 0)  (not b1502) )
  :assumption
(or b1255  (not b1502) )
  :assumption
(or (or (not b1255)  (>= r291 0) )  (<= r287 0) )
  :assumption
(or (or (not b1255)  (> r287 0) )  (= r107 r98) )
  :assumption
(or (not b1261)  (not b1506) )
  :assumption
(or b128  (not b1506) )
  :assumption
(or (or (not b1258)  b1506 )  (> r293 0) )
  :assumption
(or (<= r293 0)  (not b1506) )
  :assumption
(or b1258  (not b1506) )
  :assumption
(or (or (not b1258)  (>= r293 0) )  (<= r290 0) )
  :assumption
(or (or (not b1258)  (> r290 0) )  (= r116 r107) )
  :assumption
(or (not b1197)  (not b1510) )
  :assumption
(or b171  (not b1510) )
  :assumption
(or (or (not b1194)  b1510 )  (> r305 0) )
  :assumption
(or (<= r305 0)  (not b1510) )
  :assumption
(or b1194  (not b1510) )
  :assumption
(or (or (not b1194)  (>= r305 0) )  (<= r302 0) )
  :assumption
(or (or (not b1194)  (= r55 r46) )  (> r302 0) )
  :assumption
(or (not b1200)  (not b1513) )
  :assumption
(or b181  (not b1513) )
  :assumption
(or (or (not b1197)  b1513 )  (> r307 0) )
  :assumption
(or (<= r307 0)  (not b1513) )
  :assumption
(or b1197  (not b1513) )
  :assumption
(or (or (not b1197)  (>= r307 0) )  (<= r304 0) )
  :assumption
(or (or (not b1197)  (= r58 r55) )  (> r304 0) )
  :assumption
(or (not b1203)  (not b1516) )
  :assumption
(or b191  (not b1516) )
  :assumption
(or (or (not b1200)  b1516 )  (> r309 0) )
  :assumption
(or (<= r309 0)  (not b1516) )
  :assumption
(or b1200  (not b1516) )
  :assumption
(or (or (not b1200)  (>= r309 0) )  (<= r306 0) )
  :assumption
(or (or (not b1200)  (= r64 r58) )  (> r306 0) )
  :assumption
(or (not b1206)  (not b1519) )
  :assumption
(or b201  (not b1519) )
  :assumption
(or (or (not b1203)  b1519 )  (> r311 0) )
  :assumption
(or (<= r311 0)  (not b1519) )
  :assumption
(or b1203  (not b1519) )
  :assumption
(or (or (not b1203)  (>= r311 0) )  (<= r308 0) )
  :assumption
(or (or (not b1203)  (= r71 r64) )  (> r308 0) )
  :assumption
(or (not b1209)  (not b1522) )
  :assumption
(or b211  (not b1522) )
  :assumption
(or (or (not b1206)  b1522 )  (> r313 0) )
  :assumption
(or (<= r313 0)  (not b1522) )
  :assumption
(or b1206  (not b1522) )
  :assumption
(or (or (not b1206)  (>= r313 0) )  (<= r310 0) )
  :assumption
(or (or (not b1206)  (= r80 r71) )  (> r310 0) )
  :assumption
(or (not b1212)  (not b1525) )
  :assumption
(or b221  (not b1525) )
  :assumption
(or (or (not b1209)  b1525 )  (> r316 0) )
  :assumption
(or (<= r316 0)  (not b1525) )
  :assumption
(or b1209  (not b1525) )
  :assumption
(or (or (not b1209)  (>= r316 0) )  (<= r312 0) )
  :assumption
(or (or (not b1209)  (= r89 r80) )  (> r312 0) )
  :assumption
(or (not b1215)  (not b1528) )
  :assumption
(or b231  (not b1528) )
  :assumption
(or (or (not b1212)  b1528 )  (> r318 0) )
  :assumption
(or (<= r318 0)  (not b1528) )
  :assumption
(or b1212  (not b1528) )
  :assumption
(or (or (not b1212)  (>= r318 0) )  (<= r315 0) )
  :assumption
(or (or (not b1212)  (= r98 r89) )  (> r315 0) )
  :assumption
(or (not b1218)  (not b1531) )
  :assumption
(or b241  (not b1531) )
  :assumption
(or (or (not b1215)  b1531 )  (> r320 0) )
  :assumption
(or (<= r320 0)  (not b1531) )
  :assumption
(or b1215  (not b1531) )
  :assumption
(or (or (not b1215)  (>= r320 0) )  (<= r317 0) )
  :assumption
(or (or (not b1215)  (= r107 r98) )  (> r317 0) )
  :assumption
(or (not b1221)  (not b1534) )
  :assumption
(or b251  (not b1534) )
  :assumption
(or (or (not b1218)  b1534 )  (> r322 0) )
  :assumption
(or (<= r322 0)  (not b1534) )
  :assumption
(or b1218  (not b1534) )
  :assumption
(or (or (not b1218)  (>= r322 0) )  (<= r319 0) )
  :assumption
(or (or (not b1218)  (= r116 r107) )  (> r319 0) )
  :assumption
(or b139  b1226 )
  :assumption
(or b139  (not b150) )
  :assumption
(or (or (not b139)  b150 )  b1229 )
  :assumption
(or b150  (not b161) )
  :assumption
(or (or (not b150)  b161 )  b1232 )
  :assumption
(or (or b161  (not b171) )  b1510 )
  :assumption
(or (or (not b161)  b171 )  b1235 )
  :assumption
(or (or b171  (not b181) )  b1513 )
  :assumption
(or (or (not b171)  b181 )  b1238 )
  :assumption
(or (or b181  (not b191) )  b1516 )
  :assumption
(or (or (not b181)  b191 )  b1241 )
  :assumption
(or (or b191  (not b201) )  b1519 )
  :assumption
(or (or (not b191)  b201 )  b1244 )
  :assumption
(or (or b201  (not b211) )  b1522 )
  :assumption
(or (or (not b201)  b211 )  b1247 )
  :assumption
(or (or b211  (not b221) )  b1525 )
  :assumption
(or (or (not b211)  b221 )  b1250 )
  :assumption
(or (or b221  (not b231) )  b1528 )
  :assumption
(or (or (not b221)  b231 )  b1253 )
  :assumption
(or (or b231  (not b241) )  b1531 )
  :assumption
(or (or (not b231)  b241 )  b1256 )
  :assumption
(or (or b241  (not b251) )  b1534 )
  :assumption
(or (or (not b241)  b251 )  b1259 )
  :assumption
(or b251  (not b1265) )
  :assumption
(or (or (not b251)  b1262 )  b1265 )
  :assumption
(or (not b471)  b1465 )
  :assumption
(or (or (not b29)  b471 )  b1470 )
  :assumption
(or (or b29  (not b471) )  b1192 )
  :assumption
(or (or b29  (not b40) )  b1474 )
  :assumption
(or (or (not b29)  b40 )  b1195 )
  :assumption
(or (or b40  (not b51) )  b1478 )
  :assumption
(or (or (not b40)  b51 )  b1198 )
  :assumption
(or (or b51  (not b62) )  b1482 )
  :assumption
(or (or (not b51)  b62 )  b1201 )
  :assumption
(or (or b62  (not b73) )  b1486 )
  :assumption
(or (or (not b62)  b73 )  b1204 )
  :assumption
(or (or b73  (not b84) )  b1490 )
  :assumption
(or (or (not b73)  b84 )  b1207 )
  :assumption
(or (or b84  (not b95) )  b1494 )
  :assumption
(or (or (not b84)  b95 )  b1210 )
  :assumption
(or (or b95  (not b106) )  b1498 )
  :assumption
(or (or (not b95)  b106 )  b1213 )
  :assumption
(or (or b106  (not b117) )  b1502 )
  :assumption
(or (or (not b106)  b117 )  b1216 )
  :assumption
(or (or b117  (not b128) )  b1506 )
  :assumption
(or (or (not b117)  b128 )  b1219 )
  :assumption
(or b128  (not b1225) )
  :assumption
(or (or (not b128)  b1222 )  b1225 )
  :assumption
(or b141  b1132 )
  :assumption
(or (or b141  (not b152) )  b1180 )
  :assumption
(or (or (not b141)  b152 )  b1133 )
  :assumption
(or (or b152  (not b162) )  b1181 )
  :assumption
(or (or (not b152)  b162 )  b1134 )
  :assumption
(or (or b162  (not b172) )  b1182 )
  :assumption
(or (or (not b162)  b172 )  b1135 )
  :assumption
(or (or b172  (not b182) )  b1183 )
  :assumption
(or (or (not b172)  b182 )  b1136 )
  :assumption
(or (or b182  (not b192) )  b1184 )
  :assumption
(or (or (not b182)  b192 )  b1137 )
  :assumption
(or (or b192  (not b202) )  b1185 )
  :assumption
(or (or (not b192)  b202 )  b1138 )
  :assumption
(or (or b202  (not b212) )  b1186 )
  :assumption
(or (or (not b202)  b212 )  b1139 )
  :assumption
(or (or b212  (not b222) )  b1187 )
  :assumption
(or (or (not b212)  b222 )  b1140 )
  :assumption
(or (or b222  (not b232) )  b1188 )
  :assumption
(or (or (not b222)  b232 )  b1141 )
  :assumption
(or (or b232  (not b242) )  b1189 )
  :assumption
(or (or (not b232)  b242 )  b1142 )
  :assumption
(or (or b242  (not b252) )  b1190 )
  :assumption
(or (or (not b242)  b252 )  b1143 )
  :assumption
(or (or b252  (not b1145) )  b1191 )
  :assumption
(or (or (not b252)  b1144 )  b1145 )
  :assumption
(or (not b31)  b1169 )
  :assumption
(or (or b31  (not b42) )  b1170 )
  :assumption
(or (or (not b31)  b42 )  b1120 )
  :assumption
(or (or b42  (not b53) )  b1171 )
  :assumption
(or (or (not b42)  b53 )  b1121 )
  :assumption
(or (or b53  (not b64) )  b1172 )
  :assumption
(or (or (not b53)  b64 )  b1122 )
  :assumption
(or (or b64  (not b75) )  b1173 )
  :assumption
(or (or (not b64)  b75 )  b1123 )
  :assumption
(or (or b75  (not b86) )  b1174 )
  :assumption
(or (or (not b75)  b86 )  b1124 )
  :assumption
(or (or b86  (not b97) )  b1175 )
  :assumption
(or (or (not b86)  b97 )  b1125 )
  :assumption
(or (or b97  (not b108) )  b1176 )
  :assumption
(or (or (not b97)  b108 )  b1126 )
  :assumption
(or (or b108  (not b119) )  b1177 )
  :assumption
(or (or (not b108)  b119 )  b1127 )
  :assumption
(or (or b119  (not b130) )  b1178 )
  :assumption
(or (or (not b119)  b130 )  b1128 )
  :assumption
(or (or b130  (not b1131) )  b1179 )
  :assumption
(or (or (not b130)  b1129 )  b1131 )
  :assumption
(or b362  b1106 )
  :assumption
(or (or b362  (not b372) )  b1157 )
  :assumption
(or (or (not b362)  b372 )  b1107 )
  :assumption
(or (or b372  (not b381) )  b1158 )
  :assumption
(or (or (not b372)  b381 )  b1108 )
  :assumption
(or (or b381  (not b390) )  b1159 )
  :assumption
(or (or (not b381)  b390 )  b1109 )
  :assumption
(or (or b390  (not b399) )  b1160 )
  :assumption
(or (or (not b390)  b399 )  b1110 )
  :assumption
(or (or b399  (not b408) )  b1161 )
  :assumption
(or (or (not b399)  b408 )  b1111 )
  :assumption
(or (or b408  (not b417) )  b1162 )
  :assumption
(or (or (not b408)  b417 )  b1112 )
  :assumption
(or (or b417  (not b426) )  b1163 )
  :assumption
(or (or (not b417)  b426 )  b1113 )
  :assumption
(or (or b426  (not b435) )  b1164 )
  :assumption
(or (or (not b426)  b435 )  b1114 )
  :assumption
(or (or b435  (not b444) )  b1165 )
  :assumption
(or (or (not b435)  b444 )  b1115 )
  :assumption
(or (or b444  (not b453) )  b1166 )
  :assumption
(or (or (not b444)  b453 )  b1116 )
  :assumption
(or (or b453  (not b462) )  b1167 )
  :assumption
(or (or (not b453)  b462 )  b1117 )
  :assumption
(or (or b462  (not b1119) )  b1168 )
  :assumption
(or (or (not b462)  b1118 )  b1119 )
  :assumption
(or (not b262)  b1146 )
  :assumption
(or (or b262  (not b272) )  b1147 )
  :assumption
(or (or (not b262)  b272 )  b1094 )
  :assumption
(or (or b272  (not b282) )  b1148 )
  :assumption
(or (or (not b272)  b282 )  b1095 )
  :assumption
(or (or b282  (not b292) )  b1149 )
  :assumption
(or (or (not b282)  b292 )  b1096 )
  :assumption
(or (or b292  (not b302) )  b1150 )
  :assumption
(or (or (not b292)  b302 )  b1097 )
  :assumption
(or (or b302  (not b312) )  b1151 )
  :assumption
(or (or (not b302)  b312 )  b1098 )
  :assumption
(or (or b312  (not b322) )  b1152 )
  :assumption
(or (or (not b312)  b322 )  b1099 )
  :assumption
(or (or b322  (not b332) )  b1153 )
  :assumption
(or (or (not b322)  b332 )  b1100 )
  :assumption
(or (or b332  (not b342) )  b1154 )
  :assumption
(or (or (not b332)  b342 )  b1101 )
  :assumption
(or (or b342  (not b352) )  b1155 )
  :assumption
(or (or (not b342)  b352 )  b1102 )
  :assumption
(or (or b352  (not b1105) )  b1156 )
  :assumption
(or (or (not b352)  b1103 )  b1105 )
  :assumption
(or (or b789  (not b791) )  b828 )
  :assumption
(or (or (or b791  b792 )  (not b794) )  b830 )
  :assumption
(or (or (or (not b791)  b794 )  b854 )  b866 )
  :assumption
(or (or (or b794  b795 )  (not b797) )  b832 )
  :assumption
(or (or (or (not b794)  b797 )  b855 )  b867 )
  :assumption
(or (or (or b797  b798 )  (not b800) )  b834 )
  :assumption
(or (or (or (not b797)  b800 )  b856 )  b868 )
  :assumption
(or (or (or b800  b801 )  (not b803) )  b836 )
  :assumption
(or (or (or (not b800)  b803 )  b857 )  b869 )
  :assumption
(or (or (or b803  b804 )  (not b806) )  b838 )
  :assumption
(or (or (or (not b803)  b806 )  b858 )  b870 )
  :assumption
(or (or (or b806  b807 )  (not b809) )  b840 )
  :assumption
(or (or (or (not b806)  b809 )  b859 )  b871 )
  :assumption
(or (or (or b809  b810 )  (not b812) )  b842 )
  :assumption
(or (or (or (not b809)  b812 )  b860 )  b872 )
  :assumption
(or (or (or b812  b813 )  (not b815) )  b844 )
  :assumption
(or (or (or (not b812)  b815 )  b861 )  b873 )
  :assumption
(or (or (or b815  b816 )  (not b818) )  b846 )
  :assumption
(or (or (or (not b815)  b818 )  b862 )  b874 )
  :assumption
(or (or (or b818  b819 )  (not b821) )  b848 )
  :assumption
(or (or (or (not b818)  b821 )  b863 )  b875 )
  :assumption
(or (or (or b821  b822 )  (not b824) )  b850 )
  :assumption
(or (or (or (not b821)  b824 )  b864 )  b876 )
  :assumption
(or (or (or b824  b825 )  (not b827) )  b852 )
  :assumption
(or (or (or (not b824)  b827 )  b865 )  b877 )
  :assumption
(or b828  (not b829) )
  :assumption
(or (or b829  b830 )  (not b831) )
  :assumption
(or (or (not b829)  b831 )  b866 )
  :assumption
(or (or b831  b832 )  (not b833) )
  :assumption
(or (or (not b831)  b833 )  b867 )
  :assumption
(or (or b833  b834 )  (not b835) )
  :assumption
(or (or (not b833)  b835 )  b868 )
  :assumption
(or (or b835  b836 )  (not b837) )
  :assumption
(or (or (not b835)  b837 )  b869 )
  :assumption
(or (or b837  b838 )  (not b839) )
  :assumption
(or (or (not b837)  b839 )  b870 )
  :assumption
(or (or b839  b840 )  (not b841) )
  :assumption
(or (or (not b839)  b841 )  b871 )
  :assumption
(or (or b841  b842 )  (not b843) )
  :assumption
(or (or (not b841)  b843 )  b872 )
  :assumption
(or (or b843  b844 )  (not b845) )
  :assumption
(or (or (not b843)  b845 )  b873 )
  :assumption
(or (or b845  b846 )  (not b847) )
  :assumption
(or (or (not b845)  b847 )  b874 )
  :assumption
(or (or b847  b848 )  (not b849) )
  :assumption
(or (or (not b847)  b849 )  b875 )
  :assumption
(or (or b849  b850 )  (not b851) )
  :assumption
(or (or (not b849)  b851 )  b876 )
  :assumption
(or (or b851  b852 )  (not b853) )
  :assumption
(or (or (not b851)  b853 )  b877 )
  :assumption
(or b789  (not b790) )
  :assumption
(or (or b790  b792 )  (not b793) )
  :assumption
(or (or (not b790)  b793 )  b854 )
  :assumption
(or (or b793  b795 )  (not b796) )
  :assumption
(or (or (not b793)  b796 )  b855 )
  :assumption
(or (or b796  b798 )  (not b799) )
  :assumption
(or (or (not b796)  b799 )  b856 )
  :assumption
(or (or b799  b801 )  (not b802) )
  :assumption
(or (or (not b799)  b802 )  b857 )
  :assumption
(or (or b802  b804 )  (not b805) )
  :assumption
(or (or (not b802)  b805 )  b858 )
  :assumption
(or (or b805  b807 )  (not b808) )
  :assumption
(or (or (not b805)  b808 )  b859 )
  :assumption
(or (or b808  b810 )  (not b811) )
  :assumption
(or (or (not b808)  b811 )  b860 )
  :assumption
(or (or b811  b813 )  (not b814) )
  :assumption
(or (or (not b811)  b814 )  b861 )
  :assumption
(or (or b814  b816 )  (not b817) )
  :assumption
(or (or (not b814)  b817 )  b862 )
  :assumption
(or (or b817  b819 )  (not b820) )
  :assumption
(or (or (not b817)  b820 )  b863 )
  :assumption
(or (or b820  b822 )  (not b823) )
  :assumption
(or (or (not b820)  b823 )  b864 )
  :assumption
(or (or b823  b825 )  (not b826) )
  :assumption
(or (or (not b823)  b826 )  b865 )
  :assumption
(or (not b361)  b1132 )
  :assumption
(or (or b361  (not b371) )  b1133 )
  :assumption
(or (or (not b361)  b371 )  b1180 )
  :assumption
(or (or (not b261)  b371 )  b1134 )
  :assumption
(or (or (or b261  (not b371) )  b1169 )  b1181 )
  :assumption
(or (or (or b261  (not b271) )  b1120 )  b1135 )
  :assumption
(or (or (or (not b261)  b271 )  b1170 )  b1182 )
  :assumption
(or (or (or b271  (not b281) )  b1121 )  b1136 )
  :assumption
(or (or (or (not b271)  b281 )  b1171 )  b1183 )
  :assumption
(or (or (or b281  (not b291) )  b1122 )  b1137 )
  :assumption
(or (or (or (not b281)  b291 )  b1172 )  b1184 )
  :assumption
(or (or (or b291  (not b301) )  b1123 )  b1138 )
  :assumption
(or (or (or (not b291)  b301 )  b1173 )  b1185 )
  :assumption
(or (or (or b301  (not b311) )  b1124 )  b1139 )
  :assumption
(or (or (or (not b301)  b311 )  b1174 )  b1186 )
  :assumption
(or (or (or b311  (not b321) )  b1125 )  b1140 )
  :assumption
(or (or (or (not b311)  b321 )  b1175 )  b1187 )
  :assumption
(or (or (or b321  (not b331) )  b1126 )  b1141 )
  :assumption
(or (or (or (not b321)  b331 )  b1176 )  b1188 )
  :assumption
(or (or (or b331  (not b341) )  b1127 )  b1142 )
  :assumption
(or (or (or (not b331)  b341 )  b1177 )  b1189 )
  :assumption
(or (or (or b341  (not b351) )  b1128 )  b1143 )
  :assumption
(or (or (or (not b341)  b351 )  b1178 )  b1190 )
  :assumption
(or (or (or b351  b1129 )  (not b1130) )  b1144 )
  :assumption
(or (or (or (not b351)  b1130 )  b1179 )  b1191 )
  :assumption
(or (not b140)  b1106 )
  :assumption
(or (or b140  (not b151) )  b1107 )
  :assumption
(or (or (not b140)  b151 )  b1157 )
  :assumption
(or (or (not b30)  b151 )  b1108 )
  :assumption
(or (or (or b30  (not b151) )  b1146 )  b1158 )
  :assumption
(or (or (or b30  (not b41) )  b1094 )  b1109 )
  :assumption
(or (or (or (not b30)  b41 )  b1147 )  b1159 )
  :assumption
(or (or (or b41  (not b52) )  b1095 )  b1110 )
  :assumption
(or (or (or (not b41)  b52 )  b1148 )  b1160 )
  :assumption
(or (or (or b52  (not b63) )  b1096 )  b1111 )
  :assumption
(or (or (or (not b52)  b63 )  b1149 )  b1161 )
  :assumption
(or (or (or b63  (not b74) )  b1097 )  b1112 )
  :assumption
(or (or (or (not b63)  b74 )  b1150 )  b1162 )
  :assumption
(or (or (or b74  (not b85) )  b1098 )  b1113 )
  :assumption
(or (or (or (not b74)  b85 )  b1151 )  b1163 )
  :assumption
(or (or (or b85  (not b96) )  b1099 )  b1114 )
  :assumption
(or (or (or (not b85)  b96 )  b1152 )  b1164 )
  :assumption
(or (or (or b96  (not b107) )  b1100 )  b1115 )
  :assumption
(or (or (or (not b96)  b107 )  b1153 )  b1165 )
  :assumption
(or (or (or b107  (not b118) )  b1101 )  b1116 )
  :assumption
(or (or (or (not b107)  b118 )  b1154 )  b1166 )
  :assumption
(or (or (or b118  (not b129) )  b1102 )  b1117 )
  :assumption
(or (or (or (not b118)  b129 )  b1155 )  b1167 )
  :assumption
(or (or (or b129  b1103 )  (not b1104) )  b1118 )
  :assumption
(or (or (or (not b129)  b1104 )  b1156 )  b1168 )
  :assumption
(or b1192  (not b1194) )
  :assumption
(or (or b1194  b1195 )  (not b1197) )
  :assumption
(or (or (not b1194)  b1197 )  b1510 )
  :assumption
(or (or b1197  b1198 )  (not b1200) )
  :assumption
(or (or (not b1197)  b1200 )  b1513 )
  :assumption
(or (or b1200  b1201 )  (not b1203) )
  :assumption
(or (or (not b1200)  b1203 )  b1516 )
  :assumption
(or (or b1203  b1204 )  (not b1206) )
  :assumption
(or (or (not b1203)  b1206 )  b1519 )
  :assumption
(or (or b1206  b1207 )  (not b1209) )
  :assumption
(or (or (not b1206)  b1209 )  b1522 )
  :assumption
(or (or b1209  b1210 )  (not b1212) )
  :assumption
(or (or (not b1209)  b1212 )  b1525 )
  :assumption
(or (or b1212  b1213 )  (not b1215) )
  :assumption
(or (or (not b1212)  b1215 )  b1528 )
  :assumption
(or (or b1215  b1216 )  (not b1218) )
  :assumption
(or (or (not b1215)  b1218 )  b1531 )
  :assumption
(or (or b1218  b1219 )  (not b1221) )
  :assumption
(or (or (not b1218)  b1221 )  b1534 )
  :assumption
(or (or b1221  b1222 )  (not b1224) )
  :assumption
(or (not b1221)  b1224 )
  :assumption
(or b1226  (not b1228) )
  :assumption
(or (or b1228  b1229 )  (not b1231) )
  :assumption
(or (or (not b1228)  b1231 )  b1465 )
  :assumption
(or (or b1231  b1232 )  (not b1234) )
  :assumption
(or (or (not b1231)  b1234 )  b1470 )
  :assumption
(or (or b1234  b1235 )  (not b1237) )
  :assumption
(or (or (not b1234)  b1237 )  b1474 )
  :assumption
(or (or b1237  b1238 )  (not b1240) )
  :assumption
(or (or (not b1237)  b1240 )  b1478 )
  :assumption
(or (or b1240  b1241 )  (not b1243) )
  :assumption
(or (or (not b1240)  b1243 )  b1482 )
  :assumption
(or (or b1243  b1244 )  (not b1246) )
  :assumption
(or (or (not b1243)  b1246 )  b1486 )
  :assumption
(or (or b1246  b1247 )  (not b1249) )
  :assumption
(or (or (not b1246)  b1249 )  b1490 )
  :assumption
(or (or b1249  b1250 )  (not b1252) )
  :assumption
(or (or (not b1249)  b1252 )  b1494 )
  :assumption
(or (or b1252  b1253 )  (not b1255) )
  :assumption
(or (or (not b1252)  b1255 )  b1498 )
  :assumption
(or (or b1255  b1256 )  (not b1258) )
  :assumption
(or (or (not b1255)  b1258 )  b1502 )
  :assumption
(or (or b1258  b1259 )  (not b1261) )
  :assumption
(or (or (not b1258)  b1261 )  b1506 )
  :assumption
(or (or b1261  b1262 )  (not b1264) )
  :assumption
(or (not b1261)  b1264 )
  :assumption
(or b1226  (= (- r267 r268) 0) )
  :assumption
(or b1229  (= (- r270 r271) 0) )
  :assumption
(or b1232  (= (- r272 r273) 0) )
  :assumption
(or b1235  (= (- r274 r275) 0) )
  :assumption
(or b1238  (= (- r277 r278) 0) )
  :assumption
(or b1241  (= (- r279 r280) 0) )
  :assumption
(or b1244  (= (- r281 r282) 0) )
  :assumption
(or b1247  (= (- r283 r284) 0) )
  :assumption
(or b1250  (= (- r285 r286) 0) )
  :assumption
(or b1253  (= (- r287 r288) 0) )
  :assumption
(or b1256  (= (- r290 r291) 0) )
  :assumption
(or b1259  (= (- r292 r293) 0) )
  :assumption
(or b1262  (= (- r295 r296) 0) )
  :assumption
(or b1192  (= (- r302 r303) 0) )
  :assumption
(or b1195  (= (- r304 r305) 0) )
  :assumption
(or b1198  (= (- r306 r307) 0) )
  :assumption
(or b1201  (= (- r308 r309) 0) )
  :assumption
(or b1204  (= (- r310 r311) 0) )
  :assumption
(or b1207  (= (- r312 r313) 0) )
  :assumption
(or b1210  (= (- r315 r316) 0) )
  :assumption
(or b1213  (= (- r317 r318) 0) )
  :assumption
(or b1216  (= (- r319 r320) 0) )
  :assumption
(or b1219  (= (- r321 r322) 0) )
  :assumption
(or b1222  (= (- r323 r324) 0) )
  :assumption
(or (not b25)  (not b559) )
  :assumption
(or (not b36)  (not b566) )
  :assumption
(or (not b47)  (not b573) )
  :assumption
(or (not b58)  (not b580) )
  :assumption
(or (not b69)  (not b587) )
  :assumption
(or (not b80)  (not b594) )
  :assumption
(or (not b91)  (not b601) )
  :assumption
(or (not b102)  (not b608) )
  :assumption
(or (not b113)  (not b615) )
  :assumption
(or (not b124)  (not b622) )
  :assumption
(or (not b25)  (not b475) )
  :assumption
(or (not b36)  (not b482) )
  :assumption
(or (not b47)  (not b489) )
  :assumption
(or (not b58)  (not b496) )
  :assumption
(or (not b69)  (not b503) )
  :assumption
(or (not b80)  (not b510) )
  :assumption
(or (not b91)  (not b517) )
  :assumption
(or (not b102)  (not b524) )
  :assumption
(or (not b113)  (not b531) )
  :assumption
(or (not b124)  (not b538) )
  :assumption
(or (not b25)  (not b377) )
  :assumption
(or (not b36)  (not b386) )
  :assumption
(or (not b47)  (not b395) )
  :assumption
(or (not b58)  (not b404) )
  :assumption
(or (not b69)  (not b413) )
  :assumption
(or (not b80)  (not b422) )
  :assumption
(or (not b91)  (not b431) )
  :assumption
(or (not b102)  (not b440) )
  :assumption
(or (not b113)  (not b449) )
  :assumption
(or (not b124)  (not b458) )
  :assumption
(or (not b25)  (not b257) )
  :assumption
(or (not b36)  (not b267) )
  :assumption
(or (not b47)  (not b277) )
  :assumption
(or (not b58)  (not b287) )
  :assumption
(or (not b69)  (not b297) )
  :assumption
(or (not b80)  (not b307) )
  :assumption
(or (not b91)  (not b317) )
  :assumption
(or (not b102)  (not b327) )
  :assumption
(or (not b113)  (not b337) )
  :assumption
(or (not b124)  (not b347) )
  :assumption
(or (not b25)  (not b157) )
  :assumption
(or (not b36)  (not b167) )
  :assumption
(or (not b47)  (not b177) )
  :assumption
(or (not b58)  (not b187) )
  :assumption
(or (not b69)  (not b197) )
  :assumption
(or (not b80)  (not b207) )
  :assumption
(or (not b91)  (not b217) )
  :assumption
(or (not b102)  (not b227) )
  :assumption
(or (not b113)  (not b237) )
  :assumption
(or (not b124)  (not b247) )
  :assumption
(or (not b25)  (not b720) )
  :assumption
(or (not b36)  (not b727) )
  :assumption
(or (not b47)  (not b734) )
  :assumption
(or (not b58)  (not b741) )
  :assumption
(or (not b69)  (not b748) )
  :assumption
(or (not b80)  (not b755) )
  :assumption
(or (not b91)  (not b762) )
  :assumption
(or (not b102)  (not b769) )
  :assumption
(or (not b113)  (not b776) )
  :assumption
(or (not b124)  (not b783) )
  :assumption
(or (not b25)  (not b636) )
  :assumption
(or (not b36)  (not b643) )
  :assumption
(or (not b47)  (not b650) )
  :assumption
(or (not b58)  (not b657) )
  :assumption
(or (not b69)  (not b664) )
  :assumption
(or (not b80)  (not b671) )
  :assumption
(or (not b91)  (not b678) )
  :assumption
(or (not b102)  (not b685) )
  :assumption
(or (not b113)  (not b692) )
  :assumption
(or (not b124)  (not b699) )
  :assumption
(or (not b135)  (not b545) )
  :assumption
(or (not b146)  (not b552) )
  :assumption
(or (not b157)  (not b559) )
  :assumption
(or (not b167)  (not b566) )
  :assumption
(or (not b177)  (not b573) )
  :assumption
(or (not b187)  (not b580) )
  :assumption
(or (not b197)  (not b587) )
  :assumption
(or (not b207)  (not b594) )
  :assumption
(or (not b217)  (not b601) )
  :assumption
(or (not b227)  (not b608) )
  :assumption
(or (not b237)  (not b615) )
  :assumption
(or (not b247)  (not b622) )
  :assumption
(or (not b146)  (not b467) )
  :assumption
(or (not b157)  (not b475) )
  :assumption
(or (not b167)  (not b482) )
  :assumption
(or (not b177)  (not b489) )
  :assumption
(or (not b187)  (not b496) )
  :assumption
(or (not b197)  (not b503) )
  :assumption
(or (not b207)  (not b510) )
  :assumption
(or (not b217)  (not b517) )
  :assumption
(or (not b227)  (not b524) )
  :assumption
(or (not b237)  (not b531) )
  :assumption
(or (not b247)  (not b538) )
  :assumption
(or (not b135)  (not b357) )
  :assumption
(or (not b146)  (not b367) )
  :assumption
(or (not b157)  (not b377) )
  :assumption
(or (not b167)  (not b386) )
  :assumption
(or (not b177)  (not b395) )
  :assumption
(or (not b187)  (not b404) )
  :assumption
(or (not b197)  (not b413) )
  :assumption
(or (not b207)  (not b422) )
  :assumption
(or (not b217)  (not b431) )
  :assumption
(or (not b227)  (not b440) )
  :assumption
(or (not b237)  (not b449) )
  :assumption
(or (not b247)  (not b458) )
  :assumption
(or (not b157)  (not b257) )
  :assumption
(or (not b167)  (not b267) )
  :assumption
(or (not b177)  (not b277) )
  :assumption
(or (not b187)  (not b287) )
  :assumption
(or (not b197)  (not b297) )
  :assumption
(or (not b207)  (not b307) )
  :assumption
(or (not b217)  (not b317) )
  :assumption
(or (not b227)  (not b327) )
  :assumption
(or (not b237)  (not b337) )
  :assumption
(or (not b247)  (not b347) )
  :assumption
(or (not b135)  (not b706) )
  :assumption
(or (not b146)  (not b713) )
  :assumption
(or (not b157)  (not b720) )
  :assumption
(or (not b167)  (not b727) )
  :assumption
(or (not b177)  (not b734) )
  :assumption
(or (not b187)  (not b741) )
  :assumption
(or (not b197)  (not b748) )
  :assumption
(or (not b207)  (not b755) )
  :assumption
(or (not b217)  (not b762) )
  :assumption
(or (not b227)  (not b769) )
  :assumption
(or (not b237)  (not b776) )
  :assumption
(or (not b247)  (not b783) )
  :assumption
(or (not b146)  (not b629) )
  :assumption
(or (not b157)  (not b636) )
  :assumption
(or (not b167)  (not b643) )
  :assumption
(or (not b177)  (not b650) )
  :assumption
(or (not b187)  (not b657) )
  :assumption
(or (not b197)  (not b664) )
  :assumption
(or (not b207)  (not b671) )
  :assumption
(or (not b217)  (not b678) )
  :assumption
(or (not b227)  (not b685) )
  :assumption
(or (not b237)  (not b692) )
  :assumption
(or (not b247)  (not b699) )
  :assumption
(or (not b257)  (not b720) )
  :assumption
(or (not b267)  (not b727) )
  :assumption
(or (not b277)  (not b734) )
  :assumption
(or (not b287)  (not b741) )
  :assumption
(or (not b297)  (not b748) )
  :assumption
(or (not b307)  (not b755) )
  :assumption
(or (not b317)  (not b762) )
  :assumption
(or (not b327)  (not b769) )
  :assumption
(or (not b337)  (not b776) )
  :assumption
(or (not b347)  (not b783) )
  :assumption
(or (not b257)  (not b636) )
  :assumption
(or (not b267)  (not b643) )
  :assumption
(or (not b277)  (not b650) )
  :assumption
(or (not b287)  (not b657) )
  :assumption
(or (not b297)  (not b664) )
  :assumption
(or (not b307)  (not b671) )
  :assumption
(or (not b317)  (not b678) )
  :assumption
(or (not b327)  (not b685) )
  :assumption
(or (not b337)  (not b692) )
  :assumption
(or (not b347)  (not b699) )
  :assumption
(or (not b257)  (not b377) )
  :assumption
(or (not b267)  (not b386) )
  :assumption
(or (not b277)  (not b395) )
  :assumption
(or (not b287)  (not b404) )
  :assumption
(or (not b297)  (not b413) )
  :assumption
(or (not b307)  (not b422) )
  :assumption
(or (not b317)  (not b431) )
  :assumption
(or (not b327)  (not b440) )
  :assumption
(or (not b337)  (not b449) )
  :assumption
(or (not b347)  (not b458) )
  :assumption
(or (not b257)  (not b559) )
  :assumption
(or (not b267)  (not b566) )
  :assumption
(or (not b277)  (not b573) )
  :assumption
(or (not b287)  (not b580) )
  :assumption
(or (not b297)  (not b587) )
  :assumption
(or (not b307)  (not b594) )
  :assumption
(or (not b317)  (not b601) )
  :assumption
(or (not b327)  (not b608) )
  :assumption
(or (not b337)  (not b615) )
  :assumption
(or (not b347)  (not b622) )
  :assumption
(or (not b257)  (not b475) )
  :assumption
(or (not b267)  (not b482) )
  :assumption
(or (not b277)  (not b489) )
  :assumption
(or (not b287)  (not b496) )
  :assumption
(or (not b297)  (not b503) )
  :assumption
(or (not b307)  (not b510) )
  :assumption
(or (not b317)  (not b517) )
  :assumption
(or (not b327)  (not b524) )
  :assumption
(or (not b337)  (not b531) )
  :assumption
(or (not b347)  (not b538) )
  :assumption
(or (not b357)  (not b706) )
  :assumption
(or (not b367)  (not b713) )
  :assumption
(or (not b377)  (not b720) )
  :assumption
(or (not b386)  (not b727) )
  :assumption
(or (not b395)  (not b734) )
  :assumption
(or (not b404)  (not b741) )
  :assumption
(or (not b413)  (not b748) )
  :assumption
(or (not b422)  (not b755) )
  :assumption
(or (not b431)  (not b762) )
  :assumption
(or (not b440)  (not b769) )
  :assumption
(or (not b449)  (not b776) )
  :assumption
(or (not b458)  (not b783) )
  :assumption
(or (not b367)  (not b629) )
  :assumption
(or (not b377)  (not b636) )
  :assumption
(or (not b386)  (not b643) )
  :assumption
(or (not b395)  (not b650) )
  :assumption
(or (not b404)  (not b657) )
  :assumption
(or (not b413)  (not b664) )
  :assumption
(or (not b422)  (not b671) )
  :assumption
(or (not b431)  (not b678) )
  :assumption
(or (not b440)  (not b685) )
  :assumption
(or (not b449)  (not b692) )
  :assumption
(or (not b458)  (not b699) )
  :assumption
(or (not b357)  (not b545) )
  :assumption
(or (not b367)  (not b552) )
  :assumption
(or (not b377)  (not b559) )
  :assumption
(or (not b386)  (not b566) )
  :assumption
(or (not b395)  (not b573) )
  :assumption
(or (not b404)  (not b580) )
  :assumption
(or (not b413)  (not b587) )
  :assumption
(or (not b422)  (not b594) )
  :assumption
(or (not b431)  (not b601) )
  :assumption
(or (not b440)  (not b608) )
  :assumption
(or (not b449)  (not b615) )
  :assumption
(or (not b458)  (not b622) )
  :assumption
(or (not b367)  (not b467) )
  :assumption
(or (not b377)  (not b475) )
  :assumption
(or (not b386)  (not b482) )
  :assumption
(or (not b395)  (not b489) )
  :assumption
(or (not b404)  (not b496) )
  :assumption
(or (not b413)  (not b503) )
  :assumption
(or (not b422)  (not b510) )
  :assumption
(or (not b431)  (not b517) )
  :assumption
(or (not b440)  (not b524) )
  :assumption
(or (not b449)  (not b531) )
  :assumption
(or (not b458)  (not b538) )
  :assumption
(or (not b467)  (not b552) )
  :assumption
(or (not b475)  (not b559) )
  :assumption
(or (not b482)  (not b566) )
  :assumption
(or (not b489)  (not b573) )
  :assumption
(or (not b496)  (not b580) )
  :assumption
(or (not b503)  (not b587) )
  :assumption
(or (not b510)  (not b594) )
  :assumption
(or (not b517)  (not b601) )
  :assumption
(or (not b524)  (not b608) )
  :assumption
(or (not b531)  (not b615) )
  :assumption
(or (not b538)  (not b622) )
  :assumption
(or (not b629)  (not b713) )
  :assumption
(or (not b636)  (not b720) )
  :assumption
(or (not b643)  (not b727) )
  :assumption
(or (not b650)  (not b734) )
  :assumption
(or (not b657)  (not b741) )
  :assumption
(or (not b664)  (not b748) )
  :assumption
(or (not b671)  (not b755) )
  :assumption
(or (not b678)  (not b762) )
  :assumption
(or (not b685)  (not b769) )
  :assumption
(or (not b692)  (not b776) )
  :assumption
(or (not b699)  (not b783) )
  :assumption
(or (not b789)  (not b828) )
  :assumption
(or (not b792)  (not b830) )
  :assumption
(or (not b795)  (not b832) )
  :assumption
(or (not b798)  (not b834) )
  :assumption
(or (not b801)  (not b836) )
  :assumption
(or (not b804)  (not b838) )
  :assumption
(or (not b807)  (not b840) )
  :assumption
(or (not b810)  (not b842) )
  :assumption
(or (not b813)  (not b844) )
  :assumption
(or (not b816)  (not b846) )
  :assumption
(or (not b819)  (not b848) )
  :assumption
(or (not b822)  (not b850) )
  :assumption
(or (not b825)  (not b852) )
  :assumption
(or (not b792)  (not b866) )
  :assumption
(or (not b795)  (not b867) )
  :assumption
(or (not b798)  (not b868) )
  :assumption
(or (not b801)  (not b869) )
  :assumption
(or (not b804)  (not b870) )
  :assumption
(or (not b807)  (not b871) )
  :assumption
(or (not b810)  (not b872) )
  :assumption
(or (not b813)  (not b873) )
  :assumption
(or (not b816)  (not b874) )
  :assumption
(or (not b819)  (not b875) )
  :assumption
(or (not b822)  (not b876) )
  :assumption
(or (not b825)  (not b877) )
  :assumption
(or (not b792)  (not b854) )
  :assumption
(or (not b795)  (not b855) )
  :assumption
(or (not b798)  (not b856) )
  :assumption
(or (not b801)  (not b857) )
  :assumption
(or (not b804)  (not b858) )
  :assumption
(or (not b807)  (not b859) )
  :assumption
(or (not b810)  (not b860) )
  :assumption
(or (not b813)  (not b861) )
  :assumption
(or (not b816)  (not b862) )
  :assumption
(or (not b819)  (not b863) )
  :assumption
(or (not b822)  (not b864) )
  :assumption
(or (not b825)  (not b865) )
  :assumption
(or (not b830)  (not b866) )
  :assumption
(or (not b832)  (not b867) )
  :assumption
(or (not b834)  (not b868) )
  :assumption
(or (not b836)  (not b869) )
  :assumption
(or (not b838)  (not b870) )
  :assumption
(or (not b840)  (not b871) )
  :assumption
(or (not b842)  (not b872) )
  :assumption
(or (not b844)  (not b873) )
  :assumption
(or (not b846)  (not b874) )
  :assumption
(or (not b848)  (not b875) )
  :assumption
(or (not b850)  (not b876) )
  :assumption
(or (not b852)  (not b877) )
  :assumption
(or (not b830)  (not b854) )
  :assumption
(or (not b832)  (not b855) )
  :assumption
(or (not b834)  (not b856) )
  :assumption
(or (not b836)  (not b857) )
  :assumption
(or (not b838)  (not b858) )
  :assumption
(or (not b840)  (not b859) )
  :assumption
(or (not b842)  (not b860) )
  :assumption
(or (not b844)  (not b861) )
  :assumption
(or (not b846)  (not b862) )
  :assumption
(or (not b848)  (not b863) )
  :assumption
(or (not b850)  (not b864) )
  :assumption
(or (not b852)  (not b865) )
  :assumption
(or (not b854)  (not b866) )
  :assumption
(or (not b855)  (not b867) )
  :assumption
(or (not b856)  (not b868) )
  :assumption
(or (not b857)  (not b869) )
  :assumption
(or (not b858)  (not b870) )
  :assumption
(or (not b859)  (not b871) )
  :assumption
(or (not b860)  (not b872) )
  :assumption
(or (not b861)  (not b873) )
  :assumption
(or (not b862)  (not b874) )
  :assumption
(or (not b863)  (not b875) )
  :assumption
(or (not b864)  (not b876) )
  :assumption
(or (not b865)  (not b877) )
  :assumption
(or (not b257)  (not b1094) )
  :assumption
(or (not b267)  (not b1095) )
  :assumption
(or (not b277)  (not b1096) )
  :assumption
(or (not b287)  (not b1097) )
  :assumption
(or (not b297)  (not b1098) )
  :assumption
(or (not b307)  (not b1099) )
  :assumption
(or (not b317)  (not b1100) )
  :assumption
(or (not b327)  (not b1101) )
  :assumption
(or (not b337)  (not b1102) )
  :assumption
(or (not b347)  (not b1103) )
  :assumption
(or (not b1094)  (not b1147) )
  :assumption
(or (not b1095)  (not b1148) )
  :assumption
(or (not b1096)  (not b1149) )
  :assumption
(or (not b1097)  (not b1150) )
  :assumption
(or (not b1098)  (not b1151) )
  :assumption
(or (not b1099)  (not b1152) )
  :assumption
(or (not b1100)  (not b1153) )
  :assumption
(or (not b1101)  (not b1154) )
  :assumption
(or (not b1102)  (not b1155) )
  :assumption
(or (not b1103)  (not b1156) )
  :assumption
(or (not b1094)  (not b1159) )
  :assumption
(or (not b1095)  (not b1160) )
  :assumption
(or (not b1096)  (not b1161) )
  :assumption
(or (not b1097)  (not b1162) )
  :assumption
(or (not b1098)  (not b1163) )
  :assumption
(or (not b1099)  (not b1164) )
  :assumption
(or (not b1100)  (not b1165) )
  :assumption
(or (not b1101)  (not b1166) )
  :assumption
(or (not b1102)  (not b1167) )
  :assumption
(or (not b1103)  (not b1168) )
  :assumption
(or (not b559)  (not b1094) )
  :assumption
(or (not b566)  (not b1095) )
  :assumption
(or (not b573)  (not b1096) )
  :assumption
(or (not b580)  (not b1097) )
  :assumption
(or (not b587)  (not b1098) )
  :assumption
(or (not b594)  (not b1099) )
  :assumption
(or (not b601)  (not b1100) )
  :assumption
(or (not b608)  (not b1101) )
  :assumption
(or (not b615)  (not b1102) )
  :assumption
(or (not b622)  (not b1103) )
  :assumption
(or (not b475)  (not b1094) )
  :assumption
(or (not b482)  (not b1095) )
  :assumption
(or (not b489)  (not b1096) )
  :assumption
(or (not b496)  (not b1097) )
  :assumption
(or (not b503)  (not b1098) )
  :assumption
(or (not b510)  (not b1099) )
  :assumption
(or (not b517)  (not b1100) )
  :assumption
(or (not b524)  (not b1101) )
  :assumption
(or (not b531)  (not b1102) )
  :assumption
(or (not b538)  (not b1103) )
  :assumption
(or (not b157)  (not b1094) )
  :assumption
(or (not b167)  (not b1095) )
  :assumption
(or (not b177)  (not b1096) )
  :assumption
(or (not b187)  (not b1097) )
  :assumption
(or (not b197)  (not b1098) )
  :assumption
(or (not b207)  (not b1099) )
  :assumption
(or (not b217)  (not b1100) )
  :assumption
(or (not b227)  (not b1101) )
  :assumption
(or (not b237)  (not b1102) )
  :assumption
(or (not b247)  (not b1103) )
  :assumption
(or (not b25)  (not b1094) )
  :assumption
(or (not b36)  (not b1095) )
  :assumption
(or (not b47)  (not b1096) )
  :assumption
(or (not b58)  (not b1097) )
  :assumption
(or (not b69)  (not b1098) )
  :assumption
(or (not b80)  (not b1099) )
  :assumption
(or (not b91)  (not b1100) )
  :assumption
(or (not b102)  (not b1101) )
  :assumption
(or (not b113)  (not b1102) )
  :assumption
(or (not b124)  (not b1103) )
  :assumption
(or (not b789)  (not b1106) )
  :assumption
(or (not b792)  (not b1107) )
  :assumption
(or (not b795)  (not b1108) )
  :assumption
(or (not b798)  (not b1109) )
  :assumption
(or (not b801)  (not b1110) )
  :assumption
(or (not b804)  (not b1111) )
  :assumption
(or (not b807)  (not b1112) )
  :assumption
(or (not b810)  (not b1113) )
  :assumption
(or (not b813)  (not b1114) )
  :assumption
(or (not b816)  (not b1115) )
  :assumption
(or (not b819)  (not b1116) )
  :assumption
(or (not b822)  (not b1117) )
  :assumption
(or (not b825)  (not b1118) )
  :assumption
(or (not b357)  (not b1107) )
  :assumption
(or (not b367)  (not b1108) )
  :assumption
(or (not b377)  (not b1109) )
  :assumption
(or (not b386)  (not b1110) )
  :assumption
(or (not b395)  (not b1111) )
  :assumption
(or (not b404)  (not b1112) )
  :assumption
(or (not b413)  (not b1113) )
  :assumption
(or (not b422)  (not b1114) )
  :assumption
(or (not b431)  (not b1115) )
  :assumption
(or (not b440)  (not b1116) )
  :assumption
(or (not b449)  (not b1117) )
  :assumption
(or (not b458)  (not b1118) )
  :assumption
(or (not b1107)  (not b1157) )
  :assumption
(or (not b1108)  (not b1158) )
  :assumption
(or (not b1109)  (not b1159) )
  :assumption
(or (not b1110)  (not b1160) )
  :assumption
(or (not b1111)  (not b1161) )
  :assumption
(or (not b1112)  (not b1162) )
  :assumption
(or (not b1113)  (not b1163) )
  :assumption
(or (not b1114)  (not b1164) )
  :assumption
(or (not b1115)  (not b1165) )
  :assumption
(or (not b1116)  (not b1166) )
  :assumption
(or (not b1117)  (not b1167) )
  :assumption
(or (not b1118)  (not b1168) )
  :assumption
(or (not b1108)  (not b1146) )
  :assumption
(or (not b1109)  (not b1147) )
  :assumption
(or (not b1110)  (not b1148) )
  :assumption
(or (not b1111)  (not b1149) )
  :assumption
(or (not b1112)  (not b1150) )
  :assumption
(or (not b1113)  (not b1151) )
  :assumption
(or (not b1114)  (not b1152) )
  :assumption
(or (not b1115)  (not b1153) )
  :assumption
(or (not b1116)  (not b1154) )
  :assumption
(or (not b1117)  (not b1155) )
  :assumption
(or (not b1118)  (not b1156) )
  :assumption
(or (not b545)  (not b1107) )
  :assumption
(or (not b552)  (not b1108) )
  :assumption
(or (not b559)  (not b1109) )
  :assumption
(or (not b566)  (not b1110) )
  :assumption
(or (not b573)  (not b1111) )
  :assumption
(or (not b580)  (not b1112) )
  :assumption
(or (not b587)  (not b1113) )
  :assumption
(or (not b594)  (not b1114) )
  :assumption
(or (not b601)  (not b1115) )
  :assumption
(or (not b608)  (not b1116) )
  :assumption
(or (not b615)  (not b1117) )
  :assumption
(or (not b622)  (not b1118) )
  :assumption
(or (not b467)  (not b1108) )
  :assumption
(or (not b475)  (not b1109) )
  :assumption
(or (not b482)  (not b1110) )
  :assumption
(or (not b489)  (not b1111) )
  :assumption
(or (not b496)  (not b1112) )
  :assumption
(or (not b503)  (not b1113) )
  :assumption
(or (not b510)  (not b1114) )
  :assumption
(or (not b517)  (not b1115) )
  :assumption
(or (not b524)  (not b1116) )
  :assumption
(or (not b531)  (not b1117) )
  :assumption
(or (not b538)  (not b1118) )
  :assumption
(or (not b135)  (not b1107) )
  :assumption
(or (not b146)  (not b1108) )
  :assumption
(or (not b157)  (not b1109) )
  :assumption
(or (not b167)  (not b1110) )
  :assumption
(or (not b177)  (not b1111) )
  :assumption
(or (not b187)  (not b1112) )
  :assumption
(or (not b197)  (not b1113) )
  :assumption
(or (not b207)  (not b1114) )
  :assumption
(or (not b217)  (not b1115) )
  :assumption
(or (not b227)  (not b1116) )
  :assumption
(or (not b237)  (not b1117) )
  :assumption
(or (not b247)  (not b1118) )
  :assumption
(or (not b25)  (not b1109) )
  :assumption
(or (not b36)  (not b1110) )
  :assumption
(or (not b47)  (not b1111) )
  :assumption
(or (not b58)  (not b1112) )
  :assumption
(or (not b69)  (not b1113) )
  :assumption
(or (not b80)  (not b1114) )
  :assumption
(or (not b91)  (not b1115) )
  :assumption
(or (not b102)  (not b1116) )
  :assumption
(or (not b113)  (not b1117) )
  :assumption
(or (not b124)  (not b1118) )
  :assumption
(or (not b25)  (not b1120) )
  :assumption
(or (not b36)  (not b1121) )
  :assumption
(or (not b47)  (not b1122) )
  :assumption
(or (not b58)  (not b1123) )
  :assumption
(or (not b69)  (not b1124) )
  :assumption
(or (not b80)  (not b1125) )
  :assumption
(or (not b91)  (not b1126) )
  :assumption
(or (not b102)  (not b1127) )
  :assumption
(or (not b113)  (not b1128) )
  :assumption
(or (not b124)  (not b1129) )
  :assumption
(or (not b1120)  (not b1170) )
  :assumption
(or (not b1121)  (not b1171) )
  :assumption
(or (not b1122)  (not b1172) )
  :assumption
(or (not b1123)  (not b1173) )
  :assumption
(or (not b1124)  (not b1174) )
  :assumption
(or (not b1125)  (not b1175) )
  :assumption
(or (not b1126)  (not b1176) )
  :assumption
(or (not b1127)  (not b1177) )
  :assumption
(or (not b1128)  (not b1178) )
  :assumption
(or (not b1129)  (not b1179) )
  :assumption
(or (not b1120)  (not b1182) )
  :assumption
(or (not b1121)  (not b1183) )
  :assumption
(or (not b1122)  (not b1184) )
  :assumption
(or (not b1123)  (not b1185) )
  :assumption
(or (not b1124)  (not b1186) )
  :assumption
(or (not b1125)  (not b1187) )
  :assumption
(or (not b1126)  (not b1188) )
  :assumption
(or (not b1127)  (not b1189) )
  :assumption
(or (not b1128)  (not b1190) )
  :assumption
(or (not b1129)  (not b1191) )
  :assumption
(or (not b720)  (not b1120) )
  :assumption
(or (not b727)  (not b1121) )
  :assumption
(or (not b734)  (not b1122) )
  :assumption
(or (not b741)  (not b1123) )
  :assumption
(or (not b748)  (not b1124) )
  :assumption
(or (not b755)  (not b1125) )
  :assumption
(or (not b762)  (not b1126) )
  :assumption
(or (not b769)  (not b1127) )
  :assumption
(or (not b776)  (not b1128) )
  :assumption
(or (not b783)  (not b1129) )
  :assumption
(or (not b636)  (not b1120) )
  :assumption
(or (not b643)  (not b1121) )
  :assumption
(or (not b650)  (not b1122) )
  :assumption
(or (not b657)  (not b1123) )
  :assumption
(or (not b664)  (not b1124) )
  :assumption
(or (not b671)  (not b1125) )
  :assumption
(or (not b678)  (not b1126) )
  :assumption
(or (not b685)  (not b1127) )
  :assumption
(or (not b692)  (not b1128) )
  :assumption
(or (not b699)  (not b1129) )
  :assumption
(or (not b377)  (not b1120) )
  :assumption
(or (not b386)  (not b1121) )
  :assumption
(or (not b395)  (not b1122) )
  :assumption
(or (not b404)  (not b1123) )
  :assumption
(or (not b413)  (not b1124) )
  :assumption
(or (not b422)  (not b1125) )
  :assumption
(or (not b431)  (not b1126) )
  :assumption
(or (not b440)  (not b1127) )
  :assumption
(or (not b449)  (not b1128) )
  :assumption
(or (not b458)  (not b1129) )
  :assumption
(or (not b257)  (not b1120) )
  :assumption
(or (not b267)  (not b1121) )
  :assumption
(or (not b277)  (not b1122) )
  :assumption
(or (not b287)  (not b1123) )
  :assumption
(or (not b297)  (not b1124) )
  :assumption
(or (not b307)  (not b1125) )
  :assumption
(or (not b317)  (not b1126) )
  :assumption
(or (not b327)  (not b1127) )
  :assumption
(or (not b337)  (not b1128) )
  :assumption
(or (not b347)  (not b1129) )
  :assumption
(or (not b828)  (not b1132) )
  :assumption
(or (not b830)  (not b1133) )
  :assumption
(or (not b832)  (not b1134) )
  :assumption
(or (not b834)  (not b1135) )
  :assumption
(or (not b836)  (not b1136) )
  :assumption
(or (not b838)  (not b1137) )
  :assumption
(or (not b840)  (not b1138) )
  :assumption
(or (not b842)  (not b1139) )
  :assumption
(or (not b844)  (not b1140) )
  :assumption
(or (not b846)  (not b1141) )
  :assumption
(or (not b848)  (not b1142) )
  :assumption
(or (not b850)  (not b1143) )
  :assumption
(or (not b852)  (not b1144) )
  :assumption
(or (not b135)  (not b1133) )
  :assumption
(or (not b146)  (not b1134) )
  :assumption
(or (not b157)  (not b1135) )
  :assumption
(or (not b167)  (not b1136) )
  :assumption
(or (not b177)  (not b1137) )
  :assumption
(or (not b187)  (not b1138) )
  :assumption
(or (not b197)  (not b1139) )
  :assumption
(or (not b207)  (not b1140) )
  :assumption
(or (not b217)  (not b1141) )
  :assumption
(or (not b227)  (not b1142) )
  :assumption
(or (not b237)  (not b1143) )
  :assumption
(or (not b247)  (not b1144) )
  :assumption
(or (not b1133)  (not b1180) )
  :assumption
(or (not b1134)  (not b1181) )
  :assumption
(or (not b1135)  (not b1182) )
  :assumption
(or (not b1136)  (not b1183) )
  :assumption
(or (not b1137)  (not b1184) )
  :assumption
(or (not b1138)  (not b1185) )
  :assumption
(or (not b1139)  (not b1186) )
  :assumption
(or (not b1140)  (not b1187) )
  :assumption
(or (not b1141)  (not b1188) )
  :assumption
(or (not b1142)  (not b1189) )
  :assumption
(or (not b1143)  (not b1190) )
  :assumption
(or (not b1144)  (not b1191) )
  :assumption
(or (not b1134)  (not b1169) )
  :assumption
(or (not b1135)  (not b1170) )
  :assumption
(or (not b1136)  (not b1171) )
  :assumption
(or (not b1137)  (not b1172) )
  :assumption
(or (not b1138)  (not b1173) )
  :assumption
(or (not b1139)  (not b1174) )
  :assumption
(or (not b1140)  (not b1175) )
  :assumption
(or (not b1141)  (not b1176) )
  :assumption
(or (not b1142)  (not b1177) )
  :assumption
(or (not b1143)  (not b1178) )
  :assumption
(or (not b1144)  (not b1179) )
  :assumption
(or (not b706)  (not b1133) )
  :assumption
(or (not b713)  (not b1134) )
  :assumption
(or (not b720)  (not b1135) )
  :assumption
(or (not b727)  (not b1136) )
  :assumption
(or (not b734)  (not b1137) )
  :assumption
(or (not b741)  (not b1138) )
  :assumption
(or (not b748)  (not b1139) )
  :assumption
(or (not b755)  (not b1140) )
  :assumption
(or (not b762)  (not b1141) )
  :assumption
(or (not b769)  (not b1142) )
  :assumption
(or (not b776)  (not b1143) )
  :assumption
(or (not b783)  (not b1144) )
  :assumption
(or (not b629)  (not b1134) )
  :assumption
(or (not b636)  (not b1135) )
  :assumption
(or (not b643)  (not b1136) )
  :assumption
(or (not b650)  (not b1137) )
  :assumption
(or (not b657)  (not b1138) )
  :assumption
(or (not b664)  (not b1139) )
  :assumption
(or (not b671)  (not b1140) )
  :assumption
(or (not b678)  (not b1141) )
  :assumption
(or (not b685)  (not b1142) )
  :assumption
(or (not b692)  (not b1143) )
  :assumption
(or (not b699)  (not b1144) )
  :assumption
(or (not b357)  (not b1133) )
  :assumption
(or (not b367)  (not b1134) )
  :assumption
(or (not b377)  (not b1135) )
  :assumption
(or (not b386)  (not b1136) )
  :assumption
(or (not b395)  (not b1137) )
  :assumption
(or (not b404)  (not b1138) )
  :assumption
(or (not b413)  (not b1139) )
  :assumption
(or (not b422)  (not b1140) )
  :assumption
(or (not b431)  (not b1141) )
  :assumption
(or (not b440)  (not b1142) )
  :assumption
(or (not b449)  (not b1143) )
  :assumption
(or (not b458)  (not b1144) )
  :assumption
(or (not b257)  (not b1135) )
  :assumption
(or (not b267)  (not b1136) )
  :assumption
(or (not b277)  (not b1137) )
  :assumption
(or (not b287)  (not b1138) )
  :assumption
(or (not b297)  (not b1139) )
  :assumption
(or (not b307)  (not b1140) )
  :assumption
(or (not b317)  (not b1141) )
  :assumption
(or (not b327)  (not b1142) )
  :assumption
(or (not b337)  (not b1143) )
  :assumption
(or (not b347)  (not b1144) )
  :assumption
(or (not b257)  (not b1147) )
  :assumption
(or (not b267)  (not b1148) )
  :assumption
(or (not b277)  (not b1149) )
  :assumption
(or (not b287)  (not b1150) )
  :assumption
(or (not b297)  (not b1151) )
  :assumption
(or (not b307)  (not b1152) )
  :assumption
(or (not b317)  (not b1153) )
  :assumption
(or (not b327)  (not b1154) )
  :assumption
(or (not b337)  (not b1155) )
  :assumption
(or (not b347)  (not b1156) )
  :assumption
(or (not b1146)  (not b1158) )
  :assumption
(or (not b1147)  (not b1159) )
  :assumption
(or (not b1148)  (not b1160) )
  :assumption
(or (not b1149)  (not b1161) )
  :assumption
(or (not b1150)  (not b1162) )
  :assumption
(or (not b1151)  (not b1163) )
  :assumption
(or (not b1152)  (not b1164) )
  :assumption
(or (not b1153)  (not b1165) )
  :assumption
(or (not b1154)  (not b1166) )
  :assumption
(or (not b1155)  (not b1167) )
  :assumption
(or (not b1156)  (not b1168) )
  :assumption
(or (not b552)  (not b1146) )
  :assumption
(or (not b559)  (not b1147) )
  :assumption
(or (not b566)  (not b1148) )
  :assumption
(or (not b573)  (not b1149) )
  :assumption
(or (not b580)  (not b1150) )
  :assumption
(or (not b587)  (not b1151) )
  :assumption
(or (not b594)  (not b1152) )
  :assumption
(or (not b601)  (not b1153) )
  :assumption
(or (not b608)  (not b1154) )
  :assumption
(or (not b615)  (not b1155) )
  :assumption
(or (not b622)  (not b1156) )
  :assumption
(or (not b467)  (not b1146) )
  :assumption
(or (not b475)  (not b1147) )
  :assumption
(or (not b482)  (not b1148) )
  :assumption
(or (not b489)  (not b1149) )
  :assumption
(or (not b496)  (not b1150) )
  :assumption
(or (not b503)  (not b1151) )
  :assumption
(or (not b510)  (not b1152) )
  :assumption
(or (not b517)  (not b1153) )
  :assumption
(or (not b524)  (not b1154) )
  :assumption
(or (not b531)  (not b1155) )
  :assumption
(or (not b538)  (not b1156) )
  :assumption
(or (not b146)  (not b1146) )
  :assumption
(or (not b157)  (not b1147) )
  :assumption
(or (not b167)  (not b1148) )
  :assumption
(or (not b177)  (not b1149) )
  :assumption
(or (not b187)  (not b1150) )
  :assumption
(or (not b197)  (not b1151) )
  :assumption
(or (not b207)  (not b1152) )
  :assumption
(or (not b217)  (not b1153) )
  :assumption
(or (not b227)  (not b1154) )
  :assumption
(or (not b237)  (not b1155) )
  :assumption
(or (not b247)  (not b1156) )
  :assumption
(or (not b25)  (not b1147) )
  :assumption
(or (not b36)  (not b1148) )
  :assumption
(or (not b47)  (not b1149) )
  :assumption
(or (not b58)  (not b1150) )
  :assumption
(or (not b69)  (not b1151) )
  :assumption
(or (not b80)  (not b1152) )
  :assumption
(or (not b91)  (not b1153) )
  :assumption
(or (not b102)  (not b1154) )
  :assumption
(or (not b113)  (not b1155) )
  :assumption
(or (not b124)  (not b1156) )
  :assumption
(or (not b792)  (not b1157) )
  :assumption
(or (not b795)  (not b1158) )
  :assumption
(or (not b798)  (not b1159) )
  :assumption
(or (not b801)  (not b1160) )
  :assumption
(or (not b804)  (not b1161) )
  :assumption
(or (not b807)  (not b1162) )
  :assumption
(or (not b810)  (not b1163) )
  :assumption
(or (not b813)  (not b1164) )
  :assumption
(or (not b816)  (not b1165) )
  :assumption
(or (not b819)  (not b1166) )
  :assumption
(or (not b822)  (not b1167) )
  :assumption
(or (not b825)  (not b1168) )
  :assumption
(or (not b357)  (not b1157) )
  :assumption
(or (not b367)  (not b1158) )
  :assumption
(or (not b377)  (not b1159) )
  :assumption
(or (not b386)  (not b1160) )
  :assumption
(or (not b395)  (not b1161) )
  :assumption
(or (not b404)  (not b1162) )
  :assumption
(or (not b413)  (not b1163) )
  :assumption
(or (not b422)  (not b1164) )
  :assumption
(or (not b431)  (not b1165) )
  :assumption
(or (not b440)  (not b1166) )
  :assumption
(or (not b449)  (not b1167) )
  :assumption
(or (not b458)  (not b1168) )
  :assumption
(or (not b545)  (not b1157) )
  :assumption
(or (not b552)  (not b1158) )
  :assumption
(or (not b559)  (not b1159) )
  :assumption
(or (not b566)  (not b1160) )
  :assumption
(or (not b573)  (not b1161) )
  :assumption
(or (not b580)  (not b1162) )
  :assumption
(or (not b587)  (not b1163) )
  :assumption
(or (not b594)  (not b1164) )
  :assumption
(or (not b601)  (not b1165) )
  :assumption
(or (not b608)  (not b1166) )
  :assumption
(or (not b615)  (not b1167) )
  :assumption
(or (not b622)  (not b1168) )
  :assumption
(or (not b467)  (not b1158) )
  :assumption
(or (not b475)  (not b1159) )
  :assumption
(or (not b482)  (not b1160) )
  :assumption
(or (not b489)  (not b1161) )
  :assumption
(or (not b496)  (not b1162) )
  :assumption
(or (not b503)  (not b1163) )
  :assumption
(or (not b510)  (not b1164) )
  :assumption
(or (not b517)  (not b1165) )
  :assumption
(or (not b524)  (not b1166) )
  :assumption
(or (not b531)  (not b1167) )
  :assumption
(or (not b538)  (not b1168) )
  :assumption
(or (not b135)  (not b1157) )
  :assumption
(or (not b146)  (not b1158) )
  :assumption
(or (not b157)  (not b1159) )
  :assumption
(or (not b167)  (not b1160) )
  :assumption
(or (not b177)  (not b1161) )
  :assumption
(or (not b187)  (not b1162) )
  :assumption
(or (not b197)  (not b1163) )
  :assumption
(or (not b207)  (not b1164) )
  :assumption
(or (not b217)  (not b1165) )
  :assumption
(or (not b227)  (not b1166) )
  :assumption
(or (not b237)  (not b1167) )
  :assumption
(or (not b247)  (not b1168) )
  :assumption
(or (not b25)  (not b1159) )
  :assumption
(or (not b36)  (not b1160) )
  :assumption
(or (not b47)  (not b1161) )
  :assumption
(or (not b58)  (not b1162) )
  :assumption
(or (not b69)  (not b1163) )
  :assumption
(or (not b80)  (not b1164) )
  :assumption
(or (not b91)  (not b1165) )
  :assumption
(or (not b102)  (not b1166) )
  :assumption
(or (not b113)  (not b1167) )
  :assumption
(or (not b124)  (not b1168) )
  :assumption
(or (not b25)  (not b1170) )
  :assumption
(or (not b36)  (not b1171) )
  :assumption
(or (not b47)  (not b1172) )
  :assumption
(or (not b58)  (not b1173) )
  :assumption
(or (not b69)  (not b1174) )
  :assumption
(or (not b80)  (not b1175) )
  :assumption
(or (not b91)  (not b1176) )
  :assumption
(or (not b102)  (not b1177) )
  :assumption
(or (not b113)  (not b1178) )
  :assumption
(or (not b124)  (not b1179) )
  :assumption
(or (not b1169)  (not b1181) )
  :assumption
(or (not b1170)  (not b1182) )
  :assumption
(or (not b1171)  (not b1183) )
  :assumption
(or (not b1172)  (not b1184) )
  :assumption
(or (not b1173)  (not b1185) )
  :assumption
(or (not b1174)  (not b1186) )
  :assumption
(or (not b1175)  (not b1187) )
  :assumption
(or (not b1176)  (not b1188) )
  :assumption
(or (not b1177)  (not b1189) )
  :assumption
(or (not b1178)  (not b1190) )
  :assumption
(or (not b1179)  (not b1191) )
  :assumption
(or (not b713)  (not b1169) )
  :assumption
(or (not b720)  (not b1170) )
  :assumption
(or (not b727)  (not b1171) )
  :assumption
(or (not b734)  (not b1172) )
  :assumption
(or (not b741)  (not b1173) )
  :assumption
(or (not b748)  (not b1174) )
  :assumption
(or (not b755)  (not b1175) )
  :assumption
(or (not b762)  (not b1176) )
  :assumption
(or (not b769)  (not b1177) )
  :assumption
(or (not b776)  (not b1178) )
  :assumption
(or (not b783)  (not b1179) )
  :assumption
(or (not b629)  (not b1169) )
  :assumption
(or (not b636)  (not b1170) )
  :assumption
(or (not b643)  (not b1171) )
  :assumption
(or (not b650)  (not b1172) )
  :assumption
(or (not b657)  (not b1173) )
  :assumption
(or (not b664)  (not b1174) )
  :assumption
(or (not b671)  (not b1175) )
  :assumption
(or (not b678)  (not b1176) )
  :assumption
(or (not b685)  (not b1177) )
  :assumption
(or (not b692)  (not b1178) )
  :assumption
(or (not b699)  (not b1179) )
  :assumption
(or (not b367)  (not b1169) )
  :assumption
(or (not b377)  (not b1170) )
  :assumption
(or (not b386)  (not b1171) )
  :assumption
(or (not b395)  (not b1172) )
  :assumption
(or (not b404)  (not b1173) )
  :assumption
(or (not b413)  (not b1174) )
  :assumption
(or (not b422)  (not b1175) )
  :assumption
(or (not b431)  (not b1176) )
  :assumption
(or (not b440)  (not b1177) )
  :assumption
(or (not b449)  (not b1178) )
  :assumption
(or (not b458)  (not b1179) )
  :assumption
(or (not b257)  (not b1170) )
  :assumption
(or (not b267)  (not b1171) )
  :assumption
(or (not b277)  (not b1172) )
  :assumption
(or (not b287)  (not b1173) )
  :assumption
(or (not b297)  (not b1174) )
  :assumption
(or (not b307)  (not b1175) )
  :assumption
(or (not b317)  (not b1176) )
  :assumption
(or (not b327)  (not b1177) )
  :assumption
(or (not b337)  (not b1178) )
  :assumption
(or (not b347)  (not b1179) )
  :assumption
(or (not b830)  (not b1180) )
  :assumption
(or (not b832)  (not b1181) )
  :assumption
(or (not b834)  (not b1182) )
  :assumption
(or (not b836)  (not b1183) )
  :assumption
(or (not b838)  (not b1184) )
  :assumption
(or (not b840)  (not b1185) )
  :assumption
(or (not b842)  (not b1186) )
  :assumption
(or (not b844)  (not b1187) )
  :assumption
(or (not b846)  (not b1188) )
  :assumption
(or (not b848)  (not b1189) )
  :assumption
(or (not b850)  (not b1190) )
  :assumption
(or (not b852)  (not b1191) )
  :assumption
(or (not b135)  (not b1180) )
  :assumption
(or (not b146)  (not b1181) )
  :assumption
(or (not b157)  (not b1182) )
  :assumption
(or (not b167)  (not b1183) )
  :assumption
(or (not b177)  (not b1184) )
  :assumption
(or (not b187)  (not b1185) )
  :assumption
(or (not b197)  (not b1186) )
  :assumption
(or (not b207)  (not b1187) )
  :assumption
(or (not b217)  (not b1188) )
  :assumption
(or (not b227)  (not b1189) )
  :assumption
(or (not b237)  (not b1190) )
  :assumption
(or (not b247)  (not b1191) )
  :assumption
(or (not b706)  (not b1180) )
  :assumption
(or (not b713)  (not b1181) )
  :assumption
(or (not b720)  (not b1182) )
  :assumption
(or (not b727)  (not b1183) )
  :assumption
(or (not b734)  (not b1184) )
  :assumption
(or (not b741)  (not b1185) )
  :assumption
(or (not b748)  (not b1186) )
  :assumption
(or (not b755)  (not b1187) )
  :assumption
(or (not b762)  (not b1188) )
  :assumption
(or (not b769)  (not b1189) )
  :assumption
(or (not b776)  (not b1190) )
  :assumption
(or (not b783)  (not b1191) )
  :assumption
(or (not b629)  (not b1181) )
  :assumption
(or (not b636)  (not b1182) )
  :assumption
(or (not b643)  (not b1183) )
  :assumption
(or (not b650)  (not b1184) )
  :assumption
(or (not b657)  (not b1185) )
  :assumption
(or (not b664)  (not b1186) )
  :assumption
(or (not b671)  (not b1187) )
  :assumption
(or (not b678)  (not b1188) )
  :assumption
(or (not b685)  (not b1189) )
  :assumption
(or (not b692)  (not b1190) )
  :assumption
(or (not b699)  (not b1191) )
  :assumption
(or (not b357)  (not b1180) )
  :assumption
(or (not b367)  (not b1181) )
  :assumption
(or (not b377)  (not b1182) )
  :assumption
(or (not b386)  (not b1183) )
  :assumption
(or (not b395)  (not b1184) )
  :assumption
(or (not b404)  (not b1185) )
  :assumption
(or (not b413)  (not b1186) )
  :assumption
(or (not b422)  (not b1187) )
  :assumption
(or (not b431)  (not b1188) )
  :assumption
(or (not b440)  (not b1189) )
  :assumption
(or (not b449)  (not b1190) )
  :assumption
(or (not b458)  (not b1191) )
  :assumption
(or (not b257)  (not b1182) )
  :assumption
(or (not b267)  (not b1183) )
  :assumption
(or (not b277)  (not b1184) )
  :assumption
(or (not b287)  (not b1185) )
  :assumption
(or (not b297)  (not b1186) )
  :assumption
(or (not b307)  (not b1187) )
  :assumption
(or (not b317)  (not b1188) )
  :assumption
(or (not b327)  (not b1189) )
  :assumption
(or (not b337)  (not b1190) )
  :assumption
(or (not b347)  (not b1191) )
  :assumption
(or (not b1169)  (not b1192) )
  :assumption
(or (not b1170)  (not b1195) )
  :assumption
(or (not b1171)  (not b1198) )
  :assumption
(or (not b1172)  (not b1201) )
  :assumption
(or (not b1173)  (not b1204) )
  :assumption
(or (not b1174)  (not b1207) )
  :assumption
(or (not b1175)  (not b1210) )
  :assumption
(or (not b1176)  (not b1213) )
  :assumption
(or (not b1177)  (not b1216) )
  :assumption
(or (not b1178)  (not b1219) )
  :assumption
(or (not b1179)  (not b1222) )
  :assumption
(or (not b1146)  (not b1192) )
  :assumption
(or (not b1147)  (not b1195) )
  :assumption
(or (not b1148)  (not b1198) )
  :assumption
(or (not b1149)  (not b1201) )
  :assumption
(or (not b1150)  (not b1204) )
  :assumption
(or (not b1151)  (not b1207) )
  :assumption
(or (not b1152)  (not b1210) )
  :assumption
(or (not b1153)  (not b1213) )
  :assumption
(or (not b1154)  (not b1216) )
  :assumption
(or (not b1155)  (not b1219) )
  :assumption
(or (not b1156)  (not b1222) )
  :assumption
(or (not b1120)  (not b1195) )
  :assumption
(or (not b1121)  (not b1198) )
  :assumption
(or (not b1122)  (not b1201) )
  :assumption
(or (not b1123)  (not b1204) )
  :assumption
(or (not b1124)  (not b1207) )
  :assumption
(or (not b1125)  (not b1210) )
  :assumption
(or (not b1126)  (not b1213) )
  :assumption
(or (not b1127)  (not b1216) )
  :assumption
(or (not b1128)  (not b1219) )
  :assumption
(or (not b1129)  (not b1222) )
  :assumption
(or (not b1094)  (not b1195) )
  :assumption
(or (not b1095)  (not b1198) )
  :assumption
(or (not b1096)  (not b1201) )
  :assumption
(or (not b1097)  (not b1204) )
  :assumption
(or (not b1098)  (not b1207) )
  :assumption
(or (not b1099)  (not b1210) )
  :assumption
(or (not b1100)  (not b1213) )
  :assumption
(or (not b1101)  (not b1216) )
  :assumption
(or (not b1102)  (not b1219) )
  :assumption
(or (not b1103)  (not b1222) )
  :assumption
(or (not b629)  (not b1192) )
  :assumption
(or (not b636)  (not b1195) )
  :assumption
(or (not b643)  (not b1198) )
  :assumption
(or (not b650)  (not b1201) )
  :assumption
(or (not b657)  (not b1204) )
  :assumption
(or (not b664)  (not b1207) )
  :assumption
(or (not b671)  (not b1210) )
  :assumption
(or (not b678)  (not b1213) )
  :assumption
(or (not b685)  (not b1216) )
  :assumption
(or (not b692)  (not b1219) )
  :assumption
(or (not b699)  (not b1222) )
  :assumption
(or (not b467)  (not b1192) )
  :assumption
(or (not b475)  (not b1195) )
  :assumption
(or (not b482)  (not b1198) )
  :assumption
(or (not b489)  (not b1201) )
  :assumption
(or (not b496)  (not b1204) )
  :assumption
(or (not b503)  (not b1207) )
  :assumption
(or (not b510)  (not b1210) )
  :assumption
(or (not b517)  (not b1213) )
  :assumption
(or (not b524)  (not b1216) )
  :assumption
(or (not b531)  (not b1219) )
  :assumption
(or (not b538)  (not b1222) )
  :assumption
(or (not b257)  (not b1195) )
  :assumption
(or (not b267)  (not b1198) )
  :assumption
(or (not b277)  (not b1201) )
  :assumption
(or (not b287)  (not b1204) )
  :assumption
(or (not b297)  (not b1207) )
  :assumption
(or (not b307)  (not b1210) )
  :assumption
(or (not b317)  (not b1213) )
  :assumption
(or (not b327)  (not b1216) )
  :assumption
(or (not b337)  (not b1219) )
  :assumption
(or (not b347)  (not b1222) )
  :assumption
(or (not b25)  (not b1195) )
  :assumption
(or (not b36)  (not b1198) )
  :assumption
(or (not b47)  (not b1201) )
  :assumption
(or (not b58)  (not b1204) )
  :assumption
(or (not b69)  (not b1207) )
  :assumption
(or (not b80)  (not b1210) )
  :assumption
(or (not b91)  (not b1213) )
  :assumption
(or (not b102)  (not b1216) )
  :assumption
(or (not b113)  (not b1219) )
  :assumption
(or (not b124)  (not b1222) )
  :assumption
(or (not b1195)  (not b1510) )
  :assumption
(or (not b1198)  (not b1513) )
  :assumption
(or (not b1201)  (not b1516) )
  :assumption
(or (not b1204)  (not b1519) )
  :assumption
(or (not b1207)  (not b1522) )
  :assumption
(or (not b1210)  (not b1525) )
  :assumption
(or (not b1213)  (not b1528) )
  :assumption
(or (not b1216)  (not b1531) )
  :assumption
(or (not b1219)  (not b1534) )
  :assumption
(or (not b1180)  (not b1229) )
  :assumption
(or (not b1181)  (not b1232) )
  :assumption
(or (not b1182)  (not b1235) )
  :assumption
(or (not b1183)  (not b1238) )
  :assumption
(or (not b1184)  (not b1241) )
  :assumption
(or (not b1185)  (not b1244) )
  :assumption
(or (not b1186)  (not b1247) )
  :assumption
(or (not b1187)  (not b1250) )
  :assumption
(or (not b1188)  (not b1253) )
  :assumption
(or (not b1189)  (not b1256) )
  :assumption
(or (not b1190)  (not b1259) )
  :assumption
(or (not b1191)  (not b1262) )
  :assumption
(or (not b1157)  (not b1229) )
  :assumption
(or (not b1158)  (not b1232) )
  :assumption
(or (not b1159)  (not b1235) )
  :assumption
(or (not b1160)  (not b1238) )
  :assumption
(or (not b1161)  (not b1241) )
  :assumption
(or (not b1162)  (not b1244) )
  :assumption
(or (not b1163)  (not b1247) )
  :assumption
(or (not b1164)  (not b1250) )
  :assumption
(or (not b1165)  (not b1253) )
  :assumption
(or (not b1166)  (not b1256) )
  :assumption
(or (not b1167)  (not b1259) )
  :assumption
(or (not b1168)  (not b1262) )
  :assumption
(or (not b1132)  (not b1226) )
  :assumption
(or (not b1133)  (not b1229) )
  :assumption
(or (not b1134)  (not b1232) )
  :assumption
(or (not b1135)  (not b1235) )
  :assumption
(or (not b1136)  (not b1238) )
  :assumption
(or (not b1137)  (not b1241) )
  :assumption
(or (not b1138)  (not b1244) )
  :assumption
(or (not b1139)  (not b1247) )
  :assumption
(or (not b1140)  (not b1250) )
  :assumption
(or (not b1141)  (not b1253) )
  :assumption
(or (not b1142)  (not b1256) )
  :assumption
(or (not b1143)  (not b1259) )
  :assumption
(or (not b1144)  (not b1262) )
  :assumption
(or (not b1106)  (not b1226) )
  :assumption
(or (not b1107)  (not b1229) )
  :assumption
(or (not b1108)  (not b1232) )
  :assumption
(or (not b1109)  (not b1235) )
  :assumption
(or (not b1110)  (not b1238) )
  :assumption
(or (not b1111)  (not b1241) )
  :assumption
(or (not b1112)  (not b1244) )
  :assumption
(or (not b1113)  (not b1247) )
  :assumption
(or (not b1114)  (not b1250) )
  :assumption
(or (not b1115)  (not b1253) )
  :assumption
(or (not b1116)  (not b1256) )
  :assumption
(or (not b1117)  (not b1259) )
  :assumption
(or (not b1118)  (not b1262) )
  :assumption
(or (not b866)  (not b1229) )
  :assumption
(or (not b867)  (not b1232) )
  :assumption
(or (not b868)  (not b1235) )
  :assumption
(or (not b869)  (not b1238) )
  :assumption
(or (not b870)  (not b1241) )
  :assumption
(or (not b871)  (not b1244) )
  :assumption
(or (not b872)  (not b1247) )
  :assumption
(or (not b873)  (not b1250) )
  :assumption
(or (not b874)  (not b1253) )
  :assumption
(or (not b875)  (not b1256) )
  :assumption
(or (not b876)  (not b1259) )
  :assumption
(or (not b877)  (not b1262) )
  :assumption
(or (not b854)  (not b1229) )
  :assumption
(or (not b855)  (not b1232) )
  :assumption
(or (not b856)  (not b1235) )
  :assumption
(or (not b857)  (not b1238) )
  :assumption
(or (not b858)  (not b1241) )
  :assumption
(or (not b859)  (not b1244) )
  :assumption
(or (not b860)  (not b1247) )
  :assumption
(or (not b861)  (not b1250) )
  :assumption
(or (not b862)  (not b1253) )
  :assumption
(or (not b863)  (not b1256) )
  :assumption
(or (not b864)  (not b1259) )
  :assumption
(or (not b865)  (not b1262) )
  :assumption
(or (not b828)  (not b1226) )
  :assumption
(or (not b830)  (not b1229) )
  :assumption
(or (not b832)  (not b1232) )
  :assumption
(or (not b834)  (not b1235) )
  :assumption
(or (not b836)  (not b1238) )
  :assumption
(or (not b838)  (not b1241) )
  :assumption
(or (not b840)  (not b1244) )
  :assumption
(or (not b842)  (not b1247) )
  :assumption
(or (not b844)  (not b1250) )
  :assumption
(or (not b846)  (not b1253) )
  :assumption
(or (not b848)  (not b1256) )
  :assumption
(or (not b850)  (not b1259) )
  :assumption
(or (not b852)  (not b1262) )
  :assumption
(or (not b789)  (not b1226) )
  :assumption
(or (not b792)  (not b1229) )
  :assumption
(or (not b795)  (not b1232) )
  :assumption
(or (not b798)  (not b1235) )
  :assumption
(or (not b801)  (not b1238) )
  :assumption
(or (not b804)  (not b1241) )
  :assumption
(or (not b807)  (not b1244) )
  :assumption
(or (not b810)  (not b1247) )
  :assumption
(or (not b813)  (not b1250) )
  :assumption
(or (not b816)  (not b1253) )
  :assumption
(or (not b819)  (not b1256) )
  :assumption
(or (not b822)  (not b1259) )
  :assumption
(or (not b825)  (not b1262) )
  :assumption
(or (not b706)  (not b1229) )
  :assumption
(or (not b713)  (not b1232) )
  :assumption
(or (not b720)  (not b1235) )
  :assumption
(or (not b727)  (not b1238) )
  :assumption
(or (not b734)  (not b1241) )
  :assumption
(or (not b741)  (not b1244) )
  :assumption
(or (not b748)  (not b1247) )
  :assumption
(or (not b755)  (not b1250) )
  :assumption
(or (not b762)  (not b1253) )
  :assumption
(or (not b769)  (not b1256) )
  :assumption
(or (not b776)  (not b1259) )
  :assumption
(or (not b783)  (not b1262) )
  :assumption
(or (not b545)  (not b1229) )
  :assumption
(or (not b552)  (not b1232) )
  :assumption
(or (not b559)  (not b1235) )
  :assumption
(or (not b566)  (not b1238) )
  :assumption
(or (not b573)  (not b1241) )
  :assumption
(or (not b580)  (not b1244) )
  :assumption
(or (not b587)  (not b1247) )
  :assumption
(or (not b594)  (not b1250) )
  :assumption
(or (not b601)  (not b1253) )
  :assumption
(or (not b608)  (not b1256) )
  :assumption
(or (not b615)  (not b1259) )
  :assumption
(or (not b622)  (not b1262) )
  :assumption
(or (not b357)  (not b1229) )
  :assumption
(or (not b367)  (not b1232) )
  :assumption
(or (not b377)  (not b1235) )
  :assumption
(or (not b386)  (not b1238) )
  :assumption
(or (not b395)  (not b1241) )
  :assumption
(or (not b404)  (not b1244) )
  :assumption
(or (not b413)  (not b1247) )
  :assumption
(or (not b422)  (not b1250) )
  :assumption
(or (not b431)  (not b1253) )
  :assumption
(or (not b440)  (not b1256) )
  :assumption
(or (not b449)  (not b1259) )
  :assumption
(or (not b458)  (not b1262) )
  :assumption
(or (not b135)  (not b1229) )
  :assumption
(or (not b146)  (not b1232) )
  :assumption
(or (not b157)  (not b1235) )
  :assumption
(or (not b167)  (not b1238) )
  :assumption
(or (not b177)  (not b1241) )
  :assumption
(or (not b187)  (not b1244) )
  :assumption
(or (not b197)  (not b1247) )
  :assumption
(or (not b207)  (not b1250) )
  :assumption
(or (not b217)  (not b1253) )
  :assumption
(or (not b227)  (not b1256) )
  :assumption
(or (not b237)  (not b1259) )
  :assumption
(or (not b247)  (not b1262) )
  :assumption
(or (not b1229)  (not b1465) )
  :assumption
(or (not b1232)  (not b1470) )
  :assumption
(or (not b1235)  (not b1474) )
  :assumption
(or (not b1238)  (not b1478) )
  :assumption
(or (not b1241)  (not b1482) )
  :assumption
(or (not b1244)  (not b1486) )
  :assumption
(or (not b1247)  (not b1490) )
  :assumption
(or (not b1250)  (not b1494) )
  :assumption
(or (not b1253)  (not b1498) )
  :assumption
(or (not b1256)  (not b1502) )
  :assumption
(or (not b1259)  (not b1506) )
  :assumption
(= r9 0)
  :assumption
(= r18 r19)
  :assumption
(>= r28 r9)
  :assumption
(>= r37 r28)
  :assumption
(>= r46 r37)
  :assumption
(>= r55 r46)
  :assumption
(>= r58 r55)
  :assumption
(>= r64 r58)
  :assumption
(>= r71 r64)
  :assumption
(>= r80 r71)
  :assumption
(>= r89 r80)
  :assumption
(>= r98 r89)
  :assumption
(>= r107 r98)
  :assumption
(>= r116 r107)
  :assumption
(>= r19 r116)
  :assumption
(= r133 0)
  :assumption
(= r142 0)
  :assumption
(= r151 0)
  :assumption
(= r160 0)
  :assumption
(= r163 0)
  :assumption
(= r166 0)
  :assumption
(<= r18 70)
  :assumption
(>= r175 5)
  :assumption
(= (- r328 r326) 0)
  :assumption
(= (- (- (- (- r331 r327) r453) r419) r375) 0)
  :assumption
(= (- (- (- (- (- r333 r330) r455) r437) r421) r385) 0)
  :assumption
(= (- (- (- (- (- (- (- r335 r215) r457) r439) r423) r405) r391) r180) 0)
  :assumption
(= (- (- (- (- (- (- (- r337 r262) r459) r441) r425) r407) r393) r224) 0)
  :assumption
(= (- (- (- (- (- (- (- r339 r289) r461) r443) r427) r409) r395) r269) 0)
  :assumption
(= (- (- (- (- (- (- (- r341 r314) r463) r445) r429) r411) r397) r294) 0)
  :assumption
(= (- (- (- (- (- (- (- r1 r2) r3) r4) r5) r6) r7) r8) 0)
  :assumption
(= (- (- (- (- (- (- (- r10 r11) r12) r13) r14) r15) r16) r17) 0)
  :assumption
(= (- (- (- (- (- (- (- r20 r21) r22) r23) r24) r25) r26) r27) 0)
  :assumption
(= (- (- (- (- (- (- (- r29 r30) r31) r32) r33) r34) r35) r36) 0)
  :assumption
(= (- (- (- (- (- (- (- r38 r39) r40) r41) r42) r43) r44) r45) 0)
  :assumption
(= (- (- (- (- (- (- (- r47 r48) r49) r50) r51) r52) r53) r54) 0)
  :assumption
(= (- r56 r57) 0)
  :assumption
(= (- (- (- (- r59 r60) r61) r62) r63) 0)
  :assumption
(= (- (- (- (- (- r65 r66) r67) r68) r69) r70) 0)
  :assumption
(= (- (- (- (- (- (- (- r72 r73) r74) r75) r76) r77) r78) r79) 0)
  :assumption
(= (- (- (- (- (- (- (- r81 r82) r83) r84) r85) r86) r87) r88) 0)
  :assumption
(= (- (- (- (- (- (- (- r90 r91) r92) r93) r94) r95) r96) r97) 0)
  :assumption
(= (- (- (- (- (- (- (- r99 r100) r101) r102) r103) r104) r105) r106) 0)
  :assumption
(= (- (- (- (- (- (- (- r108 r109) r110) r111) r112) r113) r114) r115) 0)
  :assumption
(= (- (- (- (- (- (- (- r117 r118) r119) r120) r121) r122) r123) r124) 0)
  :assumption
(= (- (- (- (- (- (- (- r125 r126) r127) r128) r129) r130) r131) r132) 0)
  :assumption
(= (- (- (- (- (- (- (- r134 r135) r136) r137) r138) r139) r140) r141) 0)
  :assumption
(= (- (- (- (- (- (- (- r143 r144) r145) r146) r147) r148) r149) r150) 0)
  :assumption
(= (- (- (- (- (- (- (- r152 r153) r154) r155) r156) r157) r158) r159) 0)
  :assumption
(= (- r161 r162) 0)
  :assumption
(= (- r164 r165) 0)
  :assumption
(= (- (- (- r167 r168) r169) r170) 0)
  :assumption
(= (- (- (- r171 r172) r173) r174) 0)
  :assumption
(= (- (- (- r176 r177) r178) r179) 0)
  :assumption
(= (- (- (- r181 r182) r183) r184) 0)
  :assumption
(= (- (- (- r185 r186) r187) r188) 0)
  :assumption
(= (- (- (- r189 r190) r191) r192) 0)
  :assumption
(= (- (- (- r194 r195) r196) r197) 0)
  :assumption
(= (- (- (- r198 r199) r200) r201) 0)
  :assumption
(= (- (- (- r202 r203) r204) r205) 0)
  :assumption
(= (- (- (- r206 r207) r208) r209) 0)
  :assumption
(= (- (- (- r175 r210) r211) r212) 0)
  :assumption
(= (- r213 r214) 0)
  :assumption
(= (- (- (- r216 r217) r218) r219) 0)
  :assumption
(= (- (- (- r220 r221) r222) r223) 0)
  :assumption
(= (- (- (- r225 r226) r227) r228) 0)
  :assumption
(= (- (- (- r229 r230) r231) r232) 0)
  :assumption
(= (- (- (- r233 r234) r235) r236) 0)
  :assumption
(= (- (- (- r238 r239) r240) r241) 0)
  :assumption
(= (- (- (- r242 r243) r244) r245) 0)
  :assumption
(= (- (- (- r246 r247) r248) r249) 0)
  :assumption
(= (- (- (- r250 r251) r252) r253) 0)
  :assumption
(= (- (- (- r254 r255) r256) r257) 0)
  :assumption
(= (- (- (- r258 r259) r260) r261) 0)
  :assumption
(= (- (- (- r263 r264) r265) r266) 0)
  :assumption
(= (- r297 r298) 0)
  :assumption
(= (- r299 r300) 0)
  :assumption
(= r326 r133)
  :assumption
(= r327 (+ r328 r329))
  :assumption
(= r330 (+ r331 r332))
  :assumption
(= r215 (+ r333 r334))
  :assumption
(= r262 (+ r335 r336))
  :assumption
(= r289 (+ r337 r338))
  :assumption
(= r314 (+ r339 r340))
  :assumption
(= r2 (+ r341 r342))
  :assumption
(= r11 (+ r1 r343))
  :assumption
(= r21 (+ r10 r344))
  :assumption
(= r30 (+ r20 r345))
  :assumption
(= r39 (+ r29 r347))
  :assumption
(= r48 (+ r38 r348))
  :assumption
(= r57 r142)
  :assumption
(= r60 (+ r56 r349))
  :assumption
(= r66 (+ r59 r350))
  :assumption
(= r73 (+ r65 r351))
  :assumption
(= r82 (+ r72 r352))
  :assumption
(= r91 (+ r81 r353))
  :assumption
(= r100 (+ r90 r354))
  :assumption
(= r109 (+ r99 r355))
  :assumption
(= r118 (+ r108 r356))
  :assumption
(= r126 (+ r117 r358))
  :assumption
(= r135 (+ r125 r359))
  :assumption
(= r144 (+ r134 r360))
  :assumption
(= r153 (+ r143 r361))
  :assumption
(= r162 r163)
  :assumption
(= r165 r161)
  :assumption
(= r168 r164)
  :assumption
(= r172 r167)
  :assumption
(= r177 r171)
  :assumption
(= r182 r176)
  :assumption
(= r186 r181)
  :assumption
(= r190 r185)
  :assumption
(= r195 r189)
  :assumption
(= r199 r194)
  :assumption
(= r203 r198)
  :assumption
(= r207 r202)
  :assumption
(= r210 r206)
  :assumption
(= r214 r166)
  :assumption
(= r217 r213)
  :assumption
(= r221 r216)
  :assumption
(= r226 r220)
  :assumption
(= r230 r225)
  :assumption
(= r234 r229)
  :assumption
(= r239 r233)
  :assumption
(= r243 r238)
  :assumption
(= r247 r242)
  :assumption
(= r251 r246)
  :assumption
(= r255 r250)
  :assumption
(= r259 r254)
  :assumption
(= r264 r258)
  :assumption
(= r268 r151)
  :assumption
(= r271 (+ r267 r364))
  :assumption
(= r273 (+ r270 r365))
  :assumption
(= r275 (+ r272 r367))
  :assumption
(= r278 (+ r274 r368))
  :assumption
(= r280 (+ r277 r369))
  :assumption
(= r282 (+ r279 r370))
  :assumption
(= r284 (+ r281 r371))
  :assumption
(= r286 (+ r283 r372))
  :assumption
(= r288 (+ r285 r373))
  :assumption
(= r291 (+ r287 r374))
  :assumption
(= r293 (+ r290 r376))
  :assumption
(= r296 (+ r292 r377))
  :assumption
(= r298 r160)
  :assumption
(= r300 r297)
  :assumption
(= r303 r299)
  :assumption
(= r305 (+ r302 r379))
  :assumption
(= r307 (+ r304 r380))
  :assumption
(= r309 (+ r306 r381))
  :assumption
(= r311 (+ r308 r382))
  :assumption
(= r313 (+ r310 r383))
  :assumption
(= r316 (+ r312 r384))
  :assumption
(= r318 (+ r315 r386))
  :assumption
(= r320 (+ r317 r387))
  :assumption
(= r322 (+ r319 r388))
  :assumption
(= r324 (+ r321 r390))
  :formula
(not false)
)