(declare-fun vx () Int)
(declare-fun vy () Int)
(declare-fun vz () Int)
(declare-fun t_0 () Int)
(declare-fun px () Int)
(declare-fun py () Int)
(declare-fun pz () Int)
(declare-fun t_1 () Int)
(declare-fun t_2 () Int)
(declare-fun t_3 () Int)
(declare-fun t_4 () Int)
(declare-fun t_5 () Int)
(declare-fun t_6 () Int)
(declare-fun t_7 () Int)
(declare-fun t_8 () Int)
(declare-fun t_9 () Int)
(declare-fun t_10 () Int)
(declare-fun t_11 () Int)
(declare-fun t_12 () Int)
(declare-fun t_13 () Int)
(declare-fun t_14 () Int)
(declare-fun t_15 () Int)
(declare-fun t_16 () Int)
(declare-fun t_17 () Int)
(declare-fun t_18 () Int)
(declare-fun t_19 () Int)
(declare-fun t_20 () Int)
(declare-fun t_21 () Int)
(declare-fun t_22 () Int)
(declare-fun t_23 () Int)
(declare-fun t_24 () Int)
(declare-fun t_25 () Int)
(declare-fun t_26 () Int)
(declare-fun t_27 () Int)
(declare-fun t_28 () Int)
(declare-fun t_29 () Int)
(declare-fun t_30 () Int)
(declare-fun t_31 () Int)
(declare-fun t_32 () Int)
(declare-fun t_33 () Int)
(declare-fun t_34 () Int)
(declare-fun t_35 () Int)
(declare-fun t_36 () Int)
(declare-fun t_37 () Int)
(declare-fun t_38 () Int)
(declare-fun t_39 () Int)
(declare-fun t_40 () Int)
(declare-fun t_41 () Int)
(declare-fun t_42 () Int)
(declare-fun t_43 () Int)
(declare-fun t_44 () Int)
(declare-fun t_45 () Int)
(declare-fun t_46 () Int)
(declare-fun t_47 () Int)
(declare-fun t_48 () Int)
(declare-fun t_49 () Int)
(declare-fun t_50 () Int)
(declare-fun t_51 () Int)
(declare-fun t_52 () Int)
(declare-fun t_53 () Int)
(declare-fun t_54 () Int)
(declare-fun t_55 () Int)
(declare-fun t_56 () Int)
(declare-fun t_57 () Int)
(declare-fun t_58 () Int)
(declare-fun t_59 () Int)
(declare-fun t_60 () Int)
(declare-fun t_61 () Int)
(declare-fun t_62 () Int)
(declare-fun t_63 () Int)
(declare-fun t_64 () Int)
(declare-fun t_65 () Int)
(declare-fun t_66 () Int)
(declare-fun t_67 () Int)
(declare-fun t_68 () Int)
(declare-fun t_69 () Int)
(declare-fun t_70 () Int)
(declare-fun t_71 () Int)
(declare-fun t_72 () Int)
(declare-fun t_73 () Int)
(declare-fun t_74 () Int)
(declare-fun t_75 () Int)
(declare-fun t_76 () Int)
(declare-fun t_77 () Int)
(declare-fun t_78 () Int)
(declare-fun t_79 () Int)
(declare-fun t_80 () Int)
(declare-fun t_81 () Int)
(declare-fun t_82 () Int)
(declare-fun t_83 () Int)
(declare-fun t_84 () Int)
(declare-fun t_85 () Int)
(declare-fun t_86 () Int)
(declare-fun t_87 () Int)
(declare-fun t_88 () Int)
(declare-fun t_89 () Int)
(declare-fun t_90 () Int)
(declare-fun t_91 () Int)
(declare-fun t_92 () Int)
(declare-fun t_93 () Int)
(declare-fun t_94 () Int)
(declare-fun t_95 () Int)
(declare-fun t_96 () Int)
(declare-fun t_97 () Int)
(declare-fun t_98 () Int)
(declare-fun t_99 () Int)
(declare-fun t_100 () Int)
(declare-fun t_101 () Int)
(declare-fun t_102 () Int)
(declare-fun t_103 () Int)
(declare-fun t_104 () Int)
(declare-fun t_105 () Int)
(declare-fun t_106 () Int)
(declare-fun t_107 () Int)
(declare-fun t_108 () Int)
(declare-fun t_109 () Int)
(declare-fun t_110 () Int)
(declare-fun t_111 () Int)
(declare-fun t_112 () Int)
(declare-fun t_113 () Int)
(declare-fun t_114 () Int)
(declare-fun t_115 () Int)
(declare-fun t_116 () Int)
(declare-fun t_117 () Int)
(declare-fun t_118 () Int)
(declare-fun t_119 () Int)
(declare-fun t_120 () Int)
(declare-fun t_121 () Int)
(declare-fun t_122 () Int)
(declare-fun t_123 () Int)
(declare-fun t_124 () Int)
(declare-fun t_125 () Int)
(declare-fun t_126 () Int)
(declare-fun t_127 () Int)
(declare-fun t_128 () Int)
(declare-fun t_129 () Int)
(declare-fun t_130 () Int)
(declare-fun t_131 () Int)
(declare-fun t_132 () Int)
(declare-fun t_133 () Int)
(declare-fun t_134 () Int)
(declare-fun t_135 () Int)
(declare-fun t_136 () Int)
(declare-fun t_137 () Int)
(declare-fun t_138 () Int)
(declare-fun t_139 () Int)
(declare-fun t_140 () Int)
(declare-fun t_141 () Int)
(declare-fun t_142 () Int)
(declare-fun t_143 () Int)
(declare-fun t_144 () Int)
(declare-fun t_145 () Int)
(declare-fun t_146 () Int)
(declare-fun t_147 () Int)
(declare-fun t_148 () Int)
(declare-fun t_149 () Int)
(declare-fun t_150 () Int)
(declare-fun t_151 () Int)
(declare-fun t_152 () Int)
(declare-fun t_153 () Int)
(declare-fun t_154 () Int)
(declare-fun t_155 () Int)
(declare-fun t_156 () Int)
(declare-fun t_157 () Int)
(declare-fun t_158 () Int)
(declare-fun t_159 () Int)
(declare-fun t_160 () Int)
(declare-fun t_161 () Int)
(declare-fun t_162 () Int)
(declare-fun t_163 () Int)
(declare-fun t_164 () Int)
(declare-fun t_165 () Int)
(declare-fun t_166 () Int)
(declare-fun t_167 () Int)
(declare-fun t_168 () Int)
(declare-fun t_169 () Int)
(declare-fun t_170 () Int)
(declare-fun t_171 () Int)
(declare-fun t_172 () Int)
(declare-fun t_173 () Int)
(declare-fun t_174 () Int)
(declare-fun t_175 () Int)
(declare-fun t_176 () Int)
(declare-fun t_177 () Int)
(declare-fun t_178 () Int)
(declare-fun t_179 () Int)
(declare-fun t_180 () Int)
(declare-fun t_181 () Int)
(declare-fun t_182 () Int)
(declare-fun t_183 () Int)
(declare-fun t_184 () Int)
(declare-fun t_185 () Int)
(declare-fun t_186 () Int)
(declare-fun t_187 () Int)
(declare-fun t_188 () Int)
(declare-fun t_189 () Int)
(declare-fun t_190 () Int)
(declare-fun t_191 () Int)
(declare-fun t_192 () Int)
(declare-fun t_193 () Int)
(declare-fun t_194 () Int)
(declare-fun t_195 () Int)
(declare-fun t_196 () Int)
(declare-fun t_197 () Int)
(declare-fun t_198 () Int)
(declare-fun t_199 () Int)
(declare-fun t_200 () Int)
(declare-fun t_201 () Int)
(declare-fun t_202 () Int)
(declare-fun t_203 () Int)
(declare-fun t_204 () Int)
(declare-fun t_205 () Int)
(declare-fun t_206 () Int)
(declare-fun t_207 () Int)
(declare-fun t_208 () Int)
(declare-fun t_209 () Int)
(declare-fun t_210 () Int)
(declare-fun t_211 () Int)
(declare-fun t_212 () Int)
(declare-fun t_213 () Int)
(declare-fun t_214 () Int)
(declare-fun t_215 () Int)
(declare-fun t_216 () Int)
(declare-fun t_217 () Int)
(declare-fun t_218 () Int)
(declare-fun t_219 () Int)
(declare-fun t_220 () Int)
(declare-fun t_221 () Int)
(declare-fun t_222 () Int)
(declare-fun t_223 () Int)
(declare-fun t_224 () Int)
(declare-fun t_225 () Int)
(declare-fun t_226 () Int)
(declare-fun t_227 () Int)
(declare-fun t_228 () Int)
(declare-fun t_229 () Int)
(declare-fun t_230 () Int)
(declare-fun t_231 () Int)
(declare-fun t_232 () Int)
(declare-fun t_233 () Int)
(declare-fun t_234 () Int)
(declare-fun t_235 () Int)
(declare-fun t_236 () Int)
(declare-fun t_237 () Int)
(declare-fun t_238 () Int)
(declare-fun t_239 () Int)
(declare-fun t_240 () Int)
(declare-fun t_241 () Int)
(declare-fun t_242 () Int)
(declare-fun t_243 () Int)
(declare-fun t_244 () Int)
(declare-fun t_245 () Int)
(declare-fun t_246 () Int)
(declare-fun t_247 () Int)
(declare-fun t_248 () Int)
(declare-fun t_249 () Int)
(declare-fun t_250 () Int)
(declare-fun t_251 () Int)
(declare-fun t_252 () Int)
(declare-fun t_253 () Int)
(declare-fun t_254 () Int)
(declare-fun t_255 () Int)
(declare-fun t_256 () Int)
(declare-fun t_257 () Int)
(declare-fun t_258 () Int)
(declare-fun t_259 () Int)
(declare-fun t_260 () Int)
(declare-fun t_261 () Int)
(declare-fun t_262 () Int)
(declare-fun t_263 () Int)
(declare-fun t_264 () Int)
(declare-fun t_265 () Int)
(declare-fun t_266 () Int)
(declare-fun t_267 () Int)
(declare-fun t_268 () Int)
(declare-fun t_269 () Int)
(declare-fun t_270 () Int)
(declare-fun t_271 () Int)
(declare-fun t_272 () Int)
(declare-fun t_273 () Int)
(declare-fun t_274 () Int)
(declare-fun t_275 () Int)
(declare-fun t_276 () Int)
(declare-fun t_277 () Int)
(declare-fun t_278 () Int)
(declare-fun t_279 () Int)
(declare-fun t_280 () Int)
(declare-fun t_281 () Int)
(declare-fun t_282 () Int)
(declare-fun t_283 () Int)
(declare-fun t_284 () Int)
(declare-fun t_285 () Int)
(declare-fun t_286 () Int)
(declare-fun t_287 () Int)
(declare-fun t_288 () Int)
(declare-fun t_289 () Int)
(declare-fun t_290 () Int)
(declare-fun t_291 () Int)
(declare-fun t_292 () Int)
(declare-fun t_293 () Int)
(declare-fun t_294 () Int)
(declare-fun t_295 () Int)
(declare-fun t_296 () Int)
(declare-fun t_297 () Int)
(declare-fun t_298 () Int)
(declare-fun t_299 () Int)
(assert (<= vx 250))
(assert (>= vx (- 250)))
(assert (<= vy 250))
(assert (>= vy (- 250)))
(assert (<= vz 250))
(assert (>= vz (- 250)))
(assert (>= t_0 0))
(assert (= (+ px (* t_0 vx)) (+ 212542581053874 (* t_0 (- 88)))))
(assert (= (+ py (* t_0 vy)) (+ 357959731032403 (* t_0 (- 256)))))
(assert (= (+ pz (* t_0 vz)) (+ 176793474286781 (* t_0 (- 240)))))
(assert (>= t_1 0))
(assert (= (+ px (* t_1 vx)) (+ 154677220587564 (* t_1 184))))
(assert (= (+ py (* t_1 vy)) (+ 207254130208265 (* t_1 74))))
(assert (= (+ pz (* t_1 vz)) (+ 139183938188421 (* t_1 235))))
(assert (>= t_2 0))
(assert (= (+ px (* t_2 vx)) (+ 216869547613134 (* t_2 109))))
(assert (= (+ py (* t_2 vy)) (+ 38208083662943 (* t_2 262))))
(assert (= (+ pz (* t_2 vz)) (+ 397740686492049 (* t_2 (- 66)))))
(assert (>= t_3 0))
(assert (= (+ px (* t_3 vx)) (+ 221241619250961 (* t_3 48))))
(assert (= (+ py (* t_3 vy)) (+ 303902532813154 (* t_3 24))))
(assert (= (+ pz (* t_3 vz)) (+ 249144641113790 (* t_3 (- 112)))))
(assert (>= t_4 0))
(assert (= (+ px (* t_4 vx)) (+ 432610900189894 (* t_4 (- 166)))))
(assert (= (+ py (* t_4 vy)) (+ 347346225570463 (* t_4 (- 99)))))
(assert (= (+ pz (* t_4 vz)) (+ 389169322099761 (* t_4 (- 81)))))
(assert (>= t_5 0))
(assert (= (+ px (* t_5 vx)) (+ 247078054674939 (* t_5 68))))
(assert (= (+ py (* t_5 vy)) (+ 279574769079583 (* t_5 (- 13)))))
(assert (= (+ pz (* t_5 vz)) (+ 357168683293046 (* t_5 (- 42)))))
(assert (>= t_6 0))
(assert (= (+ px (* t_6 vx)) (+ 282963504691878 (* t_6 (- 17)))))
(assert (= (+ py (* t_6 vy)) (+ 53019767043895 (* t_6 399))))
(assert (= (+ pz (* t_6 vz)) (+ 238787901458543 (* t_6 62))))
(assert (>= t_7 0))
(assert (= (+ px (* t_7 vx)) (+ 337163551253985 (* t_7 (- 8)))))
(assert (= (+ py (* t_7 vy)) (+ 323723171285276 (* t_7 (- 74)))))
(assert (= (+ pz (* t_7 vz)) (+ 476752372944125 (* t_7 (- 103)))))
(assert (>= t_8 0))
(assert (= (+ px (* t_8 vx)) (+ 253985064168104 (* t_8 (- 10)))))
(assert (= (+ py (* t_8 vy)) (+ 111063839515573 (* t_8 456))))
(assert (= (+ pz (* t_8 vz)) (+ 450754418443501 (* t_8 (- 513)))))
(assert (>= t_9 0))
(assert (= (+ px (* t_9 vx)) (+ 258074760233454 (* t_9 49))))
(assert (= (+ py (* t_9 vy)) (+ 457117599855759 (* t_9 (- 247)))))
(assert (= (+ pz (* t_9 vz)) (+ 244857473415713 (* t_9 92))))
(assert (>= t_10 0))
(assert (= (+ px (* t_10 vx)) (+ 314400910480251 (* t_10 (- 14)))))
(assert (= (+ py (* t_10 vy)) (+ 261232162431814 (* t_10 8))))
(assert (= (+ pz (* t_10 vz)) (+ 339725786848352 (* t_10 (- 14)))))
(assert (>= t_11 0))
(assert (= (+ px (* t_11 vx)) (+ 246590774392044 (* t_11 (- 76)))))
(assert (= (+ py (* t_11 vy)) (+ 268326724153423 (* t_11 195))))
(assert (= (+ pz (* t_11 vz)) (+ 252283137292781 (* t_11 (- 225)))))
(assert (>= t_12 0))
(assert (= (+ px (* t_12 vx)) (+ 283441229604303 (* t_12 (- 8)))))
(assert (= (+ py (* t_12 vy)) (+ 368965998122557 (* t_12 (- 135)))))
(assert (= (+ pz (* t_12 vz)) (+ 461958957382550 (* t_12 (- 282)))))
(assert (>= t_13 0))
(assert (= (+ px (* t_13 vx)) (+ 175273393192850 (* t_13 167))))
(assert (= (+ py (* t_13 vy)) (+ 325589084134993 (* t_13 (- 63)))))
(assert (= (+ pz (* t_13 vz)) (+ 358406853832354 (* t_13 (- 156)))))
(assert (>= t_14 0))
(assert (= (+ px (* t_14 vx)) (+ 208105215242940 (* t_14 25))))
(assert (= (+ py (* t_14 vy)) (+ 346463859222197 (* t_14 (- 119)))))
(assert (= (+ pz (* t_14 vz)) (+ 284004541154973 (* t_14 (- 783)))))
(assert (>= t_15 0))
(assert (= (+ px (* t_15 vx)) (+ 336054085870446 (* t_15 (- 125)))))
(assert (= (+ py (* t_15 vy)) (+ 539099420004527 (* t_15 (- 451)))))
(assert (= (+ pz (* t_15 vz)) (+ 243053582150753 (* t_15 41))))
(assert (>= t_16 0))
(assert (= (+ px (* t_16 vx)) (+ 192157026866775 (* t_16 138))))
(assert (= (+ py (* t_16 vy)) (+ 221346796869463 (* t_16 27))))
(assert (= (+ pz (* t_16 vz)) (+ 239193597650948 (* t_16 138))))
(assert (>= t_17 0))
(assert (= (+ px (* t_17 vx)) (+ 276769382377332 (* t_17 (- 118)))))
(assert (= (+ py (* t_17 vy)) (+ 404564336355307 (* t_17 (- 279)))))
(assert (= (+ pz (* t_17 vz)) (+ 139075528478897 (* t_17 221))))
(assert (>= t_18 0))
(assert (= (+ px (* t_18 vx)) (+ 244171538000181 (* t_18 6))))
(assert (= (+ py (* t_18 vy)) (+ 413561793671125 (* t_18 (- 271)))))
(assert (= (+ pz (* t_18 vz)) (+ 231547901494709 (* t_18 (- 7)))))
(assert (>= t_19 0))
(assert (= (+ px (* t_19 vx)) (+ 247208942851962 (* t_19 (- 14)))))
(assert (= (+ py (* t_19 vy)) (+ 296793553833683 (* t_19 32))))
(assert (= (+ pz (* t_19 vz)) (+ 207661499518285 (* t_19 36))))
(assert (>= t_20 0))
(assert (= (+ px (* t_20 vx)) (+ 234192138385646 (* t_20 (- 28)))))
(assert (= (+ py (* t_20 vy)) (+ 334863379919503 (* t_20 (- 63)))))
(assert (= (+ pz (* t_20 vz)) (+ 180826848665889 (* t_20 52))))
(assert (>= t_21 0))
(assert (= (+ px (* t_21 vx)) (+ 130437043915331 (* t_21 338))))
(assert (= (+ py (* t_21 vy)) (+ 177551493108966 (* t_21 448))))
(assert (= (+ pz (* t_21 vz)) (+ 166468122354373 (* t_21 129))))
(assert (>= t_22 0))
(assert (= (+ px (* t_22 vx)) (+ 253559901772970 (* t_22 (- 9)))))
(assert (= (+ py (* t_22 vy)) (+ 311389465584945 (* t_22 (- 19)))))
(assert (= (+ pz (* t_22 vz)) (+ 216687040440642 (* t_22 42))))
(assert (>= t_23 0))
(assert (= (+ px (* t_23 vx)) (+ 254322299286702 (* t_23 (- 17)))))
(assert (= (+ py (* t_23 vy)) (+ 321942519715615 (* t_23 (- 42)))))
(assert (= (+ pz (* t_23 vz)) (+ 221793429844513 (* t_23 21))))
(assert (>= t_24 0))
(assert (= (+ px (* t_24 vx)) (+ 317611519474313 (* t_24 (- 24)))))
(assert (= (+ py (* t_24 vy)) (+ 509405643844478 (* t_24 (- 308)))))
(assert (= (+ pz (* t_24 vz)) (+ 492629597734339 (* t_24 (- 221)))))
(assert (>= t_25 0))
(assert (= (+ px (* t_25 vx)) (+ 312434433255435 (* t_25 (- 50)))))
(assert (= (+ py (* t_25 vy)) (+ 526132170689517 (* t_25 (- 379)))))
(assert (= (+ pz (* t_25 vz)) (+ 256217852328836 (* t_25 50))))
(assert (>= t_26 0))
(assert (= (+ px (* t_26 vx)) (+ 192520813054515 (* t_26 130))))
(assert (= (+ py (* t_26 vy)) (+ 351604734054654 (* t_26 (- 152)))))
(assert (= (+ pz (* t_26 vz)) (+ 148333436370478 (* t_26 132))))
(assert (>= t_27 0))
(assert (= (+ px (* t_27 vx)) (+ 225639342892974 (* t_27 19))))
(assert (= (+ py (* t_27 vy)) (+ 304654108851055 (* t_27 39))))
(assert (= (+ pz (* t_27 vz)) (+ 198053006284713 (* t_27 12))))
(assert (>= t_28 0))
(assert (= (+ px (* t_28 vx)) (+ 264606145094124 (* t_28 29))))
(assert (= (+ py (* t_28 vy)) (+ 239752767682501 (* t_28 61))))
(assert (= (+ pz (* t_28 vz)) (+ 207210412874243 (* t_28 131))))
(assert (>= t_29 0))
(assert (= (+ px (* t_29 vx)) (+ 73119136879824 (* t_29 253))))
(assert (= (+ py (* t_29 vy)) (+ 45456753334198 (* t_29 194))))
(assert (= (+ pz (* t_29 vz)) (+ 74136546109856 (* t_29 300))))
(assert (>= t_30 0))
(assert (= (+ px (* t_30 vx)) (+ 231632956914705 (* t_30 26))))
(assert (= (+ py (* t_30 vy)) (+ 457605979777570 (* t_30 (- 414)))))
(assert (= (+ pz (* t_30 vz)) (+ 302698719514094 (* t_30 (- 234)))))
(assert (>= t_31 0))
(assert (= (+ px (* t_31 vx)) (+ 229858006692918 (* t_31 (- 34)))))
(assert (= (+ py (* t_31 vy)) (+ 295381637696215 (* t_31 118))))
(assert (= (+ pz (* t_31 vz)) (+ 265115021539193 (* t_31 (- 354)))))
(assert (>= t_32 0))
(assert (= (+ px (* t_32 vx)) (+ 461793485716737 (* t_32 (- 158)))))
(assert (= (+ py (* t_32 vy)) (+ 253291754164921 (* t_32 5))))
(assert (= (+ pz (* t_32 vz)) (+ 311510874631043 (* t_32 47))))
(assert (>= t_33 0))
(assert (= (+ px (* t_33 vx)) (+ 325336710582066 (* t_33 5))))
(assert (= (+ py (* t_33 vy)) (+ 310550712766927 (* t_33 (- 61)))))
(assert (= (+ pz (* t_33 vz)) (+ 330361932845723 (* t_33 46))))
(assert (>= t_34 0))
(assert (= (+ px (* t_34 vx)) (+ 272391892781881 (* t_34 (- 34)))))
(assert (= (+ py (* t_34 vy)) (+ 310661548818291 (* t_34 (- 25)))))
(assert (= (+ pz (* t_34 vz)) (+ 260226744483606 (* t_34 (- 30)))))
(assert (>= t_35 0))
(assert (= (+ px (* t_35 vx)) (+ 191540619797068 (* t_35 138))))
(assert (= (+ py (* t_35 vy)) (+ 314621834402429 (* t_35 (- 22)))))
(assert (= (+ pz (* t_35 vz)) (+ 114137462106199 (* t_35 288))))
(assert (>= t_36 0))
(assert (= (+ px (* t_36 vx)) (+ 191146615936494 (* t_36 139))))
(assert (= (+ py (* t_36 vy)) (+ 272599606676084 (* t_36 136))))
(assert (= (+ pz (* t_36 vz)) (+ 172343941415066 (* t_36 110))))
(assert (>= t_37 0))
(assert (= (+ px (* t_37 vx)) (+ 267901500435402 (* t_37 (- 39)))))
(assert (= (+ py (* t_37 vy)) (+ 344752144584613 (* t_37 (- 98)))))
(assert (= (+ pz (* t_37 vz)) (+ 304856136274139 (* t_37 (- 158)))))
(assert (>= t_38 0))
(assert (= (+ px (* t_38 vx)) (+ 190703217190290 (* t_38 142))))
(assert (= (+ py (* t_38 vy)) (+ 247560977233459 (* t_38 550))))
(assert (= (+ pz (* t_38 vz)) (+ 149406776287313 (* t_38 121))))
(assert (>= t_39 0))
(assert (= (+ px (* t_39 vx)) (+ 201153500629286 (* t_39 35))))
(assert (= (+ py (* t_39 vy)) (+ 339132186878755 (* t_39 (- 57)))))
(assert (= (+ pz (* t_39 vz)) (+ 150323637135481 (* t_39 45))))
(assert (>= t_40 0))
(assert (= (+ px (* t_40 vx)) (+ 179357508767544 (* t_40 154))))
(assert (= (+ py (* t_40 vy)) (+ 21932393507743 (* t_40 315))))
(assert (= (+ pz (* t_40 vz)) (+ 145226556713621 (* t_40 227))))
(assert (>= t_41 0))
(assert (= (+ px (* t_41 vx)) (+ 307987323598344 (* t_41 (- 11)))))
(assert (= (+ py (* t_41 vy)) (+ 301312391795996 (* t_41 (- 40)))))
(assert (= (+ pz (* t_41 vz)) (+ 300888123246103 (* t_41 27))))
(assert (>= t_42 0))
(assert (= (+ px (* t_42 vx)) (+ 181344541654818 (* t_42 196))))
(assert (= (+ py (* t_42 vy)) (+ 250938115658739 (* t_42 440))))
(assert (= (+ pz (* t_42 vz)) (+ 239246377640253 (* t_42 (- 384)))))
(assert (>= t_43 0))
(assert (= (+ px (* t_43 vx)) (+ 324550882422222 (* t_43 (- 29)))))
(assert (= (+ py (* t_43 vy)) (+ 211574061061843 (* t_43 72))))
(assert (= (+ pz (* t_43 vz)) (+ 237485412093545 (* t_43 111))))
(assert (>= t_44 0))
(assert (= (+ px (* t_44 vx)) (+ 98537457698304 (* t_44 249))))
(assert (= (+ py (* t_44 vy)) (+ 238200330125587 (* t_44 31))))
(assert (= (+ pz (* t_44 vz)) (+ 135289135303526 (* t_44 240))))
(assert (>= t_45 0))
(assert (= (+ px (* t_45 vx)) (+ 313205485078410 (* t_45 (- 104)))))
(assert (= (+ py (* t_45 vy)) (+ 121081864504891 (* t_45 348))))
(assert (= (+ pz (* t_45 vz)) (+ 172268217697865 (* t_45 163))))
(assert (>= t_46 0))
(assert (= (+ px (* t_46 vx)) (+ 284584577159870 (* t_46 (- 57)))))
(assert (= (+ py (* t_46 vy)) (+ 144278803049487 (* t_46 323))))
(assert (= (+ pz (* t_46 vz)) (+ 200681374736457 (* t_46 99))))
(assert (>= t_47 0))
(assert (= (+ px (* t_47 vx)) (+ 226456734486356 (* t_47 (- 108)))))
(assert (= (+ py (* t_47 vy)) (+ 282983479210501 (* t_47 324))))
(assert (= (+ pz (* t_47 vz)) (+ 218425710839487 (* t_47 (- 366)))))
(assert (>= t_48 0))
(assert (= (+ px (* t_48 vx)) (+ 548706725108910 (* t_48 (- 217)))))
(assert (= (+ py (* t_48 vy)) (+ 277311257109343 (* t_48 (- 28)))))
(assert (= (+ pz (* t_48 vz)) (+ 307850918038817 (* t_48 69))))
(assert (>= t_49 0))
(assert (= (+ px (* t_49 vx)) (+ 275949926976102 (* t_49 (- 113)))))
(assert (= (+ py (* t_49 vy)) (+ 282022314903463 (* t_49 87))))
(assert (= (+ pz (* t_49 vz)) (+ 311454924607825 (* t_49 (- 291)))))
(assert (>= t_50 0))
(assert (= (+ px (* t_50 vx)) (+ 213263551904504 (* t_50 36))))
(assert (= (+ py (* t_50 vy)) (+ 318546624732143 (* t_50 19))))
(assert (= (+ pz (* t_50 vz)) (+ 175742955114241 (* t_50 37))))
(assert (>= t_51 0))
(assert (= (+ px (* t_51 vx)) (+ 216681369963291 (* t_51 82))))
(assert (= (+ py (* t_51 vy)) (+ 296454359998620 (* t_51 10))))
(assert (= (+ pz (* t_51 vz)) (+ 462583452318421 (* t_51 (- 495)))))
(assert (>= t_52 0))
(assert (= (+ px (* t_52 vx)) (+ 219979404537774 (* t_52 77))))
(assert (= (+ py (* t_52 vy)) (+ 211918469842543 (* t_52 188))))
(assert (= (+ pz (* t_52 vz)) (+ 232459433192801 (* t_52 27))))
(assert (>= t_53 0))
(assert (= (+ px (* t_53 vx)) (+ 325980549629430 (* t_53 (- 13)))))
(assert (= (+ py (* t_53 vy)) (+ 547508205102316 (* t_53 (- 324)))))
(assert (= (+ pz (* t_53 vz)) (+ 314702156232182 (* t_53 38))))
(assert (>= t_54 0))
(assert (= (+ px (* t_54 vx)) (+ 284385758172543 (* t_54 (- 128)))))
(assert (= (+ py (* t_54 vy)) (+ 352024785807952 (* t_54 (- 120)))))
(assert (= (+ pz (* t_54 vz)) (+ 218382195747631 (* t_54 (- 5)))))
(assert (>= t_55 0))
(assert (= (+ px (* t_55 vx)) (+ 190048554539654 (* t_55 149))))
(assert (= (+ py (* t_55 vy)) (+ 289779355315179 (* t_55 388))))
(assert (= (+ pz (* t_55 vz)) (+ 173904022587641 (* t_55 (- 145)))))
(assert (>= t_56 0))
(assert (= (+ px (* t_56 vx)) (+ 246873768466142 (* t_56 (- 39)))))
(assert (= (+ py (* t_56 vy)) (+ 272467557005199 (* t_56 131))))
(assert (= (+ pz (* t_56 vz)) (+ 232828642561081 (* t_56 (- 80)))))
(assert (>= t_57 0))
(assert (= (+ px (* t_57 vx)) (+ 163218080831461 (* t_57 176))))
(assert (= (+ py (* t_57 vy)) (+ 148606013314170 (* t_57 164))))
(assert (= (+ pz (* t_57 vz)) (+ 142402007207516 (* t_57 230))))
(assert (>= t_58 0))
(assert (= (+ px (* t_58 vx)) (+ 343986154477558 (* t_58 (- 205)))))
(assert (= (+ py (* t_58 vy)) (+ 348372021296886 (* t_58 (- 106)))))
(assert (= (+ pz (* t_58 vz)) (+ 250152291857989 (* t_58 (- 23)))))
(assert (>= t_59 0))
(assert (= (+ px (* t_59 vx)) (+ 197767130311944 (* t_59 114))))
(assert (= (+ py (* t_59 vy)) (+ 180525916592167 (* t_59 519))))
(assert (= (+ pz (* t_59 vz)) (+ 161798814812969 (* t_59 129))))
(assert (>= t_60 0))
(assert (= (+ px (* t_60 vx)) (+ 198370970228262 (* t_60 115))))
(assert (= (+ py (* t_60 vy)) (+ 298346938466104 (* t_60 54))))
(assert (= (+ pz (* t_60 vz)) (+ 174124739099332 (* t_60 102))))
(assert (>= t_61 0))
(assert (= (+ px (* t_61 vx)) (+ 380807631586707 (* t_61 (- 200)))))
(assert (= (+ py (* t_61 vy)) (+ 369450765586399 (* t_61 (- 141)))))
(assert (= (+ pz (* t_61 vz)) (+ 481309114237823 (* t_61 (- 381)))))
(assert (>= t_62 0))
(assert (= (+ px (* t_62 vx)) (+ 187175525195694 (* t_62 171))))
(assert (= (+ py (* t_62 vy)) (+ 309586416720283 (* t_62 173))))
(assert (= (+ pz (* t_62 vz)) (+ 109735015379081 (* t_62 417))))
(assert (>= t_63 0))
(assert (= (+ px (* t_63 vx)) (+ 281478516067897 (* t_63 (- 204)))))
(assert (= (+ py (* t_63 vy)) (+ 366561714660494 (* t_63 (- 184)))))
(assert (= (+ pz (* t_63 vz)) (+ 230365710762598 (* t_63 (- 132)))))
(assert (>= t_64 0))
(assert (= (+ px (* t_64 vx)) (+ 208535431591002 (* t_64 57))))
(assert (= (+ py (* t_64 vy)) (+ 325419351576169 (* t_64 (- 12)))))
(assert (= (+ pz (* t_64 vz)) (+ 191516365446671 (* t_64 (- 40)))))
(assert (>= t_65 0))
(assert (= (+ px (* t_65 vx)) (+ 226624736718348 (* t_65 (- 23)))))
(assert (= (+ py (* t_65 vy)) (+ 308650992940298 (* t_65 62))))
(assert (= (+ pz (* t_65 vz)) (+ 199188859982218 (* t_65 (- 66)))))
(assert (>= t_66 0))
(assert (= (+ px (* t_66 vx)) (+ 236728026197754 (* t_66 79))))
(assert (= (+ py (* t_66 vy)) (+ 172425510194479 (* t_66 131))))
(assert (= (+ pz (* t_66 vz)) (+ 206288955041960 (* t_66 146))))
(assert (>= t_67 0))
(assert (= (+ px (* t_67 vx)) (+ 405157823215560 (* t_67 (- 83)))))
(assert (= (+ py (* t_67 vy)) (+ 285719256118206 (* t_67 (- 34)))))
(assert (= (+ pz (* t_67 vz)) (+ 491621031364803 (* t_67 (- 129)))))
(assert (>= t_68 0))
(assert (= (+ px (* t_68 vx)) (+ 204644528670384 (* t_68 (- 56)))))
(assert (= (+ py (* t_68 vy)) (+ 339896525956405 (* t_68 (- 54)))))
(assert (= (+ pz (* t_68 vz)) (+ 151222667113763 (* t_68 (- 46)))))
(assert (>= t_69 0))
(assert (= (+ px (* t_69 vx)) (+ 185135616546414 (* t_69 179))))
(assert (= (+ py (* t_69 vy)) (+ 293907013443535 (* t_69 231))))
(assert (= (+ pz (* t_69 vz)) (+ 166394249527601 (* t_69 10))))
(assert (>= t_70 0))
(assert (= (+ px (* t_70 vx)) (+ 238567782335982 (* t_70 (- 85)))))
(assert (= (+ py (* t_70 vy)) (+ 328412098910479 (* t_70 (- 26)))))
(assert (= (+ pz (* t_70 vz)) (+ 192473102467361 (* t_70 (- 45)))))
(assert (>= t_71 0))
(assert (= (+ px (* t_71 vx)) (+ 337502877434493 (* t_71 (- 8)))))
(assert (= (+ py (* t_71 vy)) (+ 307749379575088 (* t_71 (- 58)))))
(assert (= (+ pz (* t_71 vz)) (+ 369033005648444 (* t_71 6))))
(assert (>= t_72 0))
(assert (= (+ px (* t_72 vx)) (+ 241635494672614 (* t_72 51))))
(assert (= (+ py (* t_72 vy)) (+ 304729449451093 (* t_72 (- 27)))))
(assert (= (+ pz (* t_72 vz)) (+ 326150295954981 (* t_72 (- 95)))))
(assert (>= t_73 0))
(assert (= (+ px (* t_73 vx)) (+ 243264345725652 (* t_73 73))))
(assert (= (+ py (* t_73 vy)) (+ 264419513819446 (* t_73 6))))
(assert (= (+ pz (* t_73 vz)) (+ 345867847848017 (* t_73 (- 27)))))
(assert (>= t_74 0))
(assert (= (+ px (* t_74 vx)) (+ 262661477328582 (* t_74 (- 42)))))
(assert (= (+ py (* t_74 vy)) (+ 274242124962679 (* t_74 80))))
(assert (= (+ pz (* t_74 vz)) (+ 187580319707945 (* t_74 102))))
(assert (>= t_75 0))
(assert (= (+ px (* t_75 vx)) (+ 208059705739518 (* t_75 115))))
(assert (= (+ py (* t_75 vy)) (+ 217157359130755 (* t_75 85))))
(assert (= (+ pz (* t_75 vz)) (+ 219168637501631 (* t_75 120))))
(assert (>= t_76 0))
(assert (= (+ px (* t_76 vx)) (+ 242872575971229 (* t_76 36))))
(assert (= (+ py (* t_76 vy)) (+ 425458083316108 (* t_76 (- 258)))))
(assert (= (+ pz (* t_76 vz)) (+ 227500835165921 (* t_76 53))))
(assert (>= t_77 0))
(assert (= (+ px (* t_77 vx)) (+ 448263894001344 (* t_77 (- 176)))))
(assert (= (+ py (* t_77 vy)) (+ 301783842143683 (* t_77 (- 43)))))
(assert (= (+ pz (* t_77 vz)) (+ 426560436553661 (* t_77 (- 117)))))
(assert (>= t_78 0))
(assert (= (+ px (* t_78 vx)) (+ 322545182274254 (* t_78 (- 21)))))
(assert (= (+ py (* t_78 vy)) (+ 452642407811057 (* t_78 (- 227)))))
(assert (= (+ pz (* t_78 vz)) (+ 305182728508413 (* t_78 33))))
(assert (>= t_79 0))
(assert (= (+ px (* t_79 vx)) (+ 75201284514819 (* t_79 352))))
(assert (= (+ py (* t_79 vy)) (+ 160785119325533 (* t_79 241))))
(assert (= (+ pz (* t_79 vz)) (+ 104951102720081 (* t_79 293))))
(assert (>= t_80 0))
(assert (= (+ px (* t_80 vx)) (+ 185323568951310 (* t_80 163))))
(assert (= (+ py (* t_80 vy)) (+ 233171350573267 (* t_80 358))))
(assert (= (+ pz (* t_80 vz)) (+ 165775283064269 (* t_80 102))))
(assert (>= t_81 0))
(assert (= (+ px (* t_81 vx)) (+ 242854931589532 (* t_81 18))))
(assert (= (+ py (* t_81 vy)) (+ 319092328660893 (* t_81 (- 38)))))
(assert (= (+ pz (* t_81 vz)) (+ 243043088450517 (* t_81 (- 17)))))
(assert (>= t_82 0))
(assert (= (+ px (* t_82 vx)) (+ 216818686888044 (* t_82 58))))
(assert (= (+ py (* t_82 vy)) (+ 223426989024383 (* t_82 283))))
(assert (= (+ pz (* t_82 vz)) (+ 346281309297331 (* t_82 (- 434)))))
(assert (>= t_83 0))
(assert (= (+ px (* t_83 vx)) (+ 248624452315030 (* t_83 83))))
(assert (= (+ py (* t_83 vy)) (+ 297434951348619 (* t_83 (- 49)))))
(assert (= (+ pz (* t_83 vz)) (+ 284011728475200 (* t_83 96))))
(assert (>= t_84 0))
(assert (= (+ px (* t_84 vx)) (+ 308774084417184 (* t_84 (- 22)))))
(assert (= (+ py (* t_84 vy)) (+ 254923461188383 (* t_84 27))))
(assert (= (+ pz (* t_84 vz)) (+ 324690057597731 (* t_84 (- 20)))))
(assert (>= t_85 0))
(assert (= (+ px (* t_85 vx)) (+ 477086131906062 (* t_85 (- 153)))))
(assert (= (+ py (* t_85 vy)) (+ 293633862617983 (* t_85 (- 43)))))
(assert (= (+ pz (* t_85 vz)) (+ 289717304778929 (* t_85 83))))
(assert (>= t_86 0))
(assert (= (+ px (* t_86 vx)) (+ 310556413418768 (* t_86 (- 67)))))
(assert (= (+ py (* t_86 vy)) (+ 388389186178424 (* t_86 (- 172)))))
(assert (= (+ pz (* t_86 vz)) (+ 201218392651440 (* t_86 124))))
(assert (>= t_87 0))
(assert (= (+ px (* t_87 vx)) (+ 294335453543209 (* t_87 6))))
(assert (= (+ py (* t_87 vy)) (+ 239407270896468 (* t_87 40))))
(assert (= (+ pz (* t_87 vz)) (+ 327371176340196 (* t_87 (- 8)))))
(assert (>= t_88 0))
(assert (= (+ px (* t_88 vx)) (+ 198704436992819 (* t_88 114))))
(assert (= (+ py (* t_88 vy)) (+ 423313637384734 (* t_88 (- 360)))))
(assert (= (+ pz (* t_88 vz)) (+ 211494844150179 (* t_88 (- 21)))))
(assert (>= t_89 0))
(assert (= (+ px (* t_89 vx)) (+ 329848820747522 (* t_89 (- 19)))))
(assert (= (+ py (* t_89 vy)) (+ 171413007628813 (* t_89 102))))
(assert (= (+ pz (* t_89 vz)) (+ 298751280762187 (* t_89 54))))
(assert (>= t_90 0))
(assert (= (+ px (* t_90 vx)) (+ 232791155115204 (* t_90 (- 56)))))
(assert (= (+ py (* t_90 vy)) (+ 389793252905721 (* t_90 (- 314)))))
(assert (= (+ pz (* t_90 vz)) (+ 200914316887487 (* t_90 (- 82)))))
(assert (>= t_91 0))
(assert (= (+ px (* t_91 vx)) (+ 371238777825072 (* t_91 (- 35)))))
(assert (= (+ py (* t_91 vy)) (+ 364331369420770 (* t_91 (- 114)))))
(assert (= (+ pz (* t_91 vz)) (+ 349467249711398 (* t_91 34))))
(assert (>= t_92 0))
(assert (= (+ px (* t_92 vx)) (+ 290194660125822 (* t_92 (- 93)))))
(assert (= (+ py (* t_92 vy)) (+ 286241186809255 (* t_92 39))))
(assert (= (+ pz (* t_92 vz)) (+ 265989895196345 (* t_92 (- 71)))))
(assert (>= t_93 0))
(assert (= (+ px (* t_93 vx)) (+ 138500514403427 (* t_93 270))))
(assert (= (+ py (* t_93 vy)) (+ 150096241065480 (* t_93 386))))
(assert (= (+ pz (* t_93 vz)) (+ 90891764345181 (* t_93 345))))
(assert (>= t_94 0))
(assert (= (+ px (* t_94 vx)) (+ 342432728761822 (* t_94 (- 69)))))
(assert (= (+ py (* t_94 vy)) (+ 169489883251125 (* t_94 145))))
(assert (= (+ pz (* t_94 vz)) (+ 160900448427412 (* t_94 204))))
(assert (>= t_95 0))
(assert (= (+ px (* t_95 vx)) (+ 387284555873510 (* t_95 (- 235)))))
(assert (= (+ py (* t_95 vy)) (+ 268651056280939 (* t_95 48))))
(assert (= (+ pz (* t_95 vz)) (+ 472485507519965 (* t_95 (- 406)))))
(assert (>= t_96 0))
(assert (= (+ px (* t_96 vx)) (+ 348183642749259 (* t_96 (- 26)))))
(assert (= (+ py (* t_96 vy)) (+ 358775680962680 (* t_96 (- 110)))))
(assert (= (+ pz (* t_96 vz)) (+ 425167151051150 (* t_96 (- 64)))))
(assert (>= t_97 0))
(assert (= (+ px (* t_97 vx)) (+ 214564960481976 (* t_97 (- 35)))))
(assert (= (+ py (* t_97 vy)) (+ 332636582662001 (* t_97 (- 19)))))
(assert (= (+ pz (* t_97 vz)) (+ 166341733116147 (* t_97 (- 17)))))
(assert (>= t_98 0))
(assert (= (+ px (* t_98 vx)) (+ 288352094438008 (* t_98 32))))
(assert (= (+ py (* t_98 vy)) (+ 172713636729509 (* t_98 94))))
(assert (= (+ pz (* t_98 vz)) (+ 508999993126113 (* t_98 (- 171)))))
(assert (>= t_99 0))
(assert (= (+ px (* t_99 vx)) (+ 429522310493674 (* t_99 (- 241)))))
(assert (= (+ py (* t_99 vy)) (+ 350751066474876 (* t_99 (- 106)))))
(assert (= (+ pz (* t_99 vz)) (+ 353772711184036 (* t_99 (- 110)))))
(assert (>= t_100 0))
(assert (= (+ px (* t_100 vx)) (+ 235317931818252 (* t_100 8))))
(assert (= (+ py (* t_100 vy)) (+ 321016228988431 (* t_100 (- 29)))))
(assert (= (+ pz (* t_100 vz)) (+ 221782559196323 (* t_100 (- 24)))))
(assert (>= t_101 0))
(assert (= (+ px (* t_101 vx)) (+ 237395224369976 (* t_101 48))))
(assert (= (+ py (* t_101 vy)) (+ 271952629687205 (* t_101 46))))
(assert (= (+ pz (* t_101 vz)) (+ 200198427527953 (* t_101 109))))
(assert (>= t_102 0))
(assert (= (+ px (* t_102 vx)) (+ 267689676493904 (* t_102 (- 151)))))
(assert (= (+ py (* t_102 vy)) (+ 197692176620362 (* t_102 456))))
(assert (= (+ pz (* t_102 vz)) (+ 371002531720142 (* t_102 (- 664)))))
(assert (>= t_103 0))
(assert (= (+ px (* t_103 vx)) (+ 245022629101794 (* t_103 79))))
(assert (= (+ py (* t_103 vy)) (+ 336310573633898 (* t_103 (- 86)))))
(assert (= (+ pz (* t_103 vz)) (+ 178670106406896 (* t_103 192))))
(assert (>= t_104 0))
(assert (= (+ px (* t_104 vx)) (+ 308555808260267 (* t_104 20))))
(assert (= (+ py (* t_104 vy)) (+ 235053234862080 (* t_104 16))))
(assert (= (+ pz (* t_104 vz)) (+ 386617281992034 (* t_104 (- 14)))))
(assert (>= t_105 0))
(assert (= (+ px (* t_105 vx)) (+ 254939001555789 (* t_105 46))))
(assert (= (+ py (* t_105 vy)) (+ 196490967246088 (* t_105 120))))
(assert (= (+ pz (* t_105 vz)) (+ 344406853138846 (* t_105 (- 66)))))
(assert (>= t_106 0))
(assert (= (+ px (* t_106 vx)) (+ 198067603029891 (* t_106 112))))
(assert (= (+ py (* t_106 vy)) (+ 228271655034477 (* t_106 353))))
(assert (= (+ pz (* t_106 vz)) (+ 230280443116238 (* t_106 (- 142)))))
(assert (>= t_107 0))
(assert (= (+ px (* t_107 vx)) (+ 286182290367015 (* t_107 40))))
(assert (= (+ py (* t_107 vy)) (+ 324356938662982 (* t_107 (- 74)))))
(assert (= (+ pz (* t_107 vz)) (+ 337470234197366 (* t_107 30))))
(assert (>= t_108 0))
(assert (= (+ px (* t_108 vx)) (+ 182772323746872 (* t_108 182))))
(assert (= (+ py (* t_108 vy)) (+ 243078357133489 (* t_108 418))))
(assert (= (+ pz (* t_108 vz)) (+ 180935879286305 (* t_108 (- 11)))))
(assert (>= t_109 0))
(assert (= (+ px (* t_109 vx)) (+ 334555295661618 (* t_109 (- 19)))))
(assert (= (+ py (* t_109 vy)) (+ 283598866844113 (* t_109 (- 28)))))
(assert (= (+ pz (* t_109 vz)) (+ 307163703216413 (* t_109 51))))
(assert (>= t_110 0))
(assert (= (+ px (* t_110 vx)) (+ 268032515539496 (* t_110 53))))
(assert (= (+ py (* t_110 vy)) (+ 179884088413109 (* t_110 89))))
(assert (= (+ pz (* t_110 vz)) (+ 201707373095034 (* t_110 166))))
(assert (>= t_111 0))
(assert (= (+ px (* t_111 vx)) (+ 314152706857177 (* t_111 (- 10)))))
(assert (= (+ py (* t_111 vy)) (+ 231973181098005 (* t_111 41))))
(assert (= (+ pz (* t_111 vz)) (+ 294537386515547 (* t_111 47))))
(assert (>= t_112 0))
(assert (= (+ px (* t_112 vx)) (+ 211145445957746 (* t_112 105))))
(assert (= (+ py (* t_112 vy)) (+ 256130578705417 (* t_112 54))))
(assert (= (+ pz (* t_112 vz)) (+ 227544572919273 (* t_112 81))))
(assert (>= t_113 0))
(assert (= (+ px (* t_113 vx)) (+ 240281216930434 (* t_113 (- 81)))))
(assert (= (+ py (* t_113 vy)) (+ 308871905093706 (* t_113 58))))
(assert (= (+ pz (* t_113 vz)) (+ 201208104074959 (* t_113 (- 69)))))
(assert (>= t_114 0))
(assert (= (+ px (* t_114 vx)) (+ 194990331403464 (* t_114 96))))
(assert (= (+ py (* t_114 vy)) (+ 353680311245143 (* t_114 (- 217)))))
(assert (= (+ pz (* t_114 vz)) (+ 148152875882771 (* t_114 54))))
(assert (>= t_115 0))
(assert (= (+ px (* t_115 vx)) (+ 376506453102756 (* t_115 (- 59)))))
(assert (= (+ py (* t_115 vy)) (+ 282681817701967 (* t_115 (- 29)))))
(assert (= (+ pz (* t_115 vz)) (+ 308014018133222 (* t_115 56))))
(assert (>= t_116 0))
(assert (= (+ px (* t_116 vx)) (+ 270559608594507 (* t_116 (- 38)))))
(assert (= (+ py (* t_116 vy)) (+ 293243401201593 (* t_116 17))))
(assert (= (+ pz (* t_116 vz)) (+ 219465840278274 (* t_116 48))))
(assert (>= t_117 0))
(assert (= (+ px (* t_117 vx)) (+ 271434227107862 (* t_117 (- 157)))))
(assert (= (+ py (* t_117 vy)) (+ 301909819058233 (* t_117 57))))
(assert (= (+ pz (* t_117 vz)) (+ 255037189953162 (* t_117 (- 212)))))
(assert (>= t_118 0))
(assert (= (+ px (* t_118 vx)) (+ 228819748864119 (* t_118 100))))
(assert (= (+ py (* t_118 vy)) (+ 35415178477933 (* t_118 225))))
(assert (= (+ pz (* t_118 vz)) (+ 360982336746131 (* t_118 7))))
(assert (>= t_119 0))
(assert (= (+ px (* t_119 vx)) (+ 282571416535269 (* t_119 34))))
(assert (= (+ py (* t_119 vy)) (+ 237239909717928 (* t_119 28))))
(assert (= (+ pz (* t_119 vz)) (+ 361818410574456 (* t_119 (- 20)))))
(assert (>= t_120 0))
(assert (= (+ px (* t_120 vx)) (+ 237878607070278 (* t_120 42))))
(assert (= (+ py (* t_120 vy)) (+ 316580360861695 (* t_120 (- 39)))))
(assert (= (+ pz (* t_120 vz)) (+ 326197735422041 (* t_120 (- 160)))))
(assert (>= t_121 0))
(assert (= (+ px (* t_121 vx)) (+ 182576050978588 (* t_121 153))))
(assert (= (+ py (* t_121 vy)) (+ 187101572838317 (* t_121 161))))
(assert (= (+ pz (* t_121 vz)) (+ 131079628110881 (* t_121 245))))
(assert (>= t_122 0))
(assert (= (+ px (* t_122 vx)) (+ 235076492312502 (* t_122 (- 203)))))
(assert (= (+ py (* t_122 vy)) (+ 318319071558547 (* t_122 96))))
(assert (= (+ pz (* t_122 vz)) (+ 260428708551349 (* t_122 (- 762)))))
(assert (>= t_123 0))
(assert (= (+ px (* t_123 vx)) (+ 187583408959494 (* t_123 189))))
(assert (= (+ py (* t_123 vy)) (+ 313306547152243 (* t_123 318))))
(assert (= (+ pz (* t_123 vz)) (+ 102716500573961 (* t_123 643))))
(assert (>= t_124 0))
(assert (= (+ px (* t_124 vx)) (+ 239870832918417 (* t_124 10))))
(assert (= (+ py (* t_124 vy)) (+ 26077551674877 (* t_124 745))))
(assert (= (+ pz (* t_124 vz)) (+ 194534422319897 (* t_124 77))))
(assert (>= t_125 0))
(assert (= (+ px (* t_125 vx)) (+ 268344200395759 (* t_125 (- 144)))))
(assert (= (+ py (* t_125 vy)) (+ 336594882856173 (* t_125 (- 71)))))
(assert (= (+ pz (* t_125 vz)) (+ 201457637971271 (* t_125 (- 13)))))
(assert (>= t_126 0))
(assert (= (+ px (* t_126 vx)) (+ 351502642713711 (* t_126 (- 54)))))
(assert (= (+ py (* t_126 vy)) (+ 343426968745552 (* t_126 (- 94)))))
(assert (= (+ pz (* t_126 vz)) (+ 327993505552334 (* t_126 8))))
(assert (>= t_127 0))
(assert (= (+ px (* t_127 vx)) (+ 203247301060818 (* t_127 17))))
(assert (= (+ py (* t_127 vy)) (+ 304211148313729 (* t_127 294))))
(assert (= (+ pz (* t_127 vz)) (+ 144668102389835 (* t_127 108))))
(assert (>= t_128 0))
(assert (= (+ px (* t_128 vx)) (+ 205287991254828 (* t_128 73))))
(assert (= (+ py (* t_128 vy)) (+ 326526363823258 (* t_128 (- 18)))))
(assert (= (+ pz (* t_128 vz)) (+ 176717703001868 (* t_128 32))))
(assert (>= t_129 0))
(assert (= (+ px (* t_129 vx)) (+ 228237293076774 (* t_129 49))))
(assert (= (+ py (* t_129 vy)) (+ 492607291603871 (* t_129 (- 457)))))
(assert (= (+ pz (* t_129 vz)) (+ 215976066898633 (* t_129 39))))
(assert (>= t_130 0))
(assert (= (+ px (* t_130 vx)) (+ 210744469193866 (* t_130 87))))
(assert (= (+ py (* t_130 vy)) (+ 242345551455857 (* t_130 173))))
(assert (= (+ pz (* t_130 vz)) (+ 338364614486931 (* t_130 (- 305)))))
(assert (>= t_131 0))
(assert (= (+ px (* t_131 vx)) (+ 283795432748766 (* t_131 27))))
(assert (= (+ py (* t_131 vy)) (+ 324397233772201 (* t_131 (- 71)))))
(assert (= (+ pz (* t_131 vz)) (+ 303141716476529 (* t_131 37))))
(assert (>= t_132 0))
(assert (= (+ px (* t_132 vx)) (+ 318328668468378 (* t_132 (- 9)))))
(assert (= (+ py (* t_132 vy)) (+ 290176478743420 (* t_132 (- 32)))))
(assert (= (+ pz (* t_132 vz)) (+ 393177776909696 (* t_132 (- 60)))))
(assert (>= t_133 0))
(assert (= (+ px (* t_133 vx)) (+ 296886504660264 (* t_133 (- 8)))))
(assert (= (+ py (* t_133 vy)) (+ 330367685997713 (* t_133 (- 76)))))
(assert (= (+ pz (* t_133 vz)) (+ 290768439652901 (* t_133 23))))
(assert (>= t_134 0))
(assert (= (+ px (* t_134 vx)) (+ 354925965270690 (* t_134 (- 73)))))
(assert (= (+ py (* t_134 vy)) (+ 204310714489876 (* t_134 86))))
(assert (= (+ pz (* t_134 vz)) (+ 324988197369764 (* t_134 (- 6)))))
(assert (>= t_135 0))
(assert (= (+ px (* t_135 vx)) (+ 277940901110162 (* t_135 26))))
(assert (= (+ py (* t_135 vy)) (+ 351813200734015 (* t_135 (- 105)))))
(assert (= (+ pz (* t_135 vz)) (+ 35068250706381 (* t_135 370))))
(assert (>= t_136 0))
(assert (= (+ px (* t_136 vx)) (+ 302119534267998 (* t_136 (- 185)))))
(assert (= (+ py (* t_136 vy)) (+ 319648005021051 (* t_136 (- 26)))))
(assert (= (+ pz (* t_136 vz)) (+ 257122942759009 (* t_136 (- 123)))))
(assert (>= t_137 0))
(assert (= (+ px (* t_137 vx)) (+ 220643077695684 (* t_137 30))))
(assert (= (+ py (* t_137 vy)) (+ 355855985807773 (* t_137 (- 142)))))
(assert (= (+ pz (* t_137 vz)) (+ 179518771733771 (* t_137 66))))
(assert (>= t_138 0))
(assert (= (+ px (* t_138 vx)) (+ 281128245154754 (* t_138 47))))
(assert (= (+ py (* t_138 vy)) (+ 261417029969318 (* t_138 (- 10)))))
(assert (= (+ pz (* t_138 vz)) (+ 390265842706956 (* t_138 (- 20)))))
(assert (>= t_139 0))
(assert (= (+ px (* t_139 vx)) (+ 401214520647879 (* t_139 (- 66)))))
(assert (= (+ py (* t_139 vy)) (+ 209382315271573 (* t_139 37))))
(assert (= (+ pz (* t_139 vz)) (+ 394433050114910 (* t_139 (- 12)))))
(assert (>= t_140 0))
(assert (= (+ px (* t_140 vx)) (+ 202419387388134 (* t_140 115))))
(assert (= (+ py (* t_140 vy)) (+ 370308338321798 (* t_140 (- 152)))))
(assert (= (+ pz (* t_140 vz)) (+ 371095720268716 (* t_140 (- 266)))))
(assert (>= t_141 0))
(assert (= (+ px (* t_141 vx)) (+ 243933688132567 (* t_141 (- 60)))))
(assert (= (+ py (* t_141 vy)) (+ 284238541251243 (* t_141 127))))
(assert (= (+ pz (* t_141 vz)) (+ 160523673406178 (* t_141 134))))
(assert (>= t_142 0))
(assert (= (+ px (* t_142 vx)) (+ 207949728449758 (* t_142 27))))
(assert (= (+ py (* t_142 vy)) (+ 342146025132292 (* t_142 (- 90)))))
(assert (= (+ pz (* t_142 vz)) (+ 160034991638202 (* t_142 52))))
(assert (>= t_143 0))
(assert (= (+ px (* t_143 vx)) (+ 328107083354006 (* t_143 (- 27)))))
(assert (= (+ py (* t_143 vy)) (+ 506783656792851 (* t_143 (- 292)))))
(assert (= (+ pz (* t_143 vz)) (+ 68374835799249 (* t_143 321))))
(assert (>= t_144 0))
(assert (= (+ px (* t_144 vx)) (+ 334371695727666 (* t_144 (- 209)))))
(assert (= (+ py (* t_144 vy)) (+ 295677547881937 (* t_144 21))))
(assert (= (+ pz (* t_144 vz)) (+ 372669058678174 (* t_144 (- 342)))))
(assert (>= t_145 0))
(assert (= (+ px (* t_145 vx)) (+ 425555650358416 (* t_145 (- 94)))))
(assert (= (+ py (* t_145 vy)) (+ 141386636896383 (* t_145 107))))
(assert (= (+ pz (* t_145 vz)) (+ 400700320063993 (* t_145 (- 23)))))
(assert (>= t_146 0))
(assert (= (+ px (* t_146 vx)) (+ 354111348691934 (* t_146 (- 183)))))
(assert (= (+ py (* t_146 vy)) (+ 360815768065903 (* t_146 (- 129)))))
(assert (= (+ pz (* t_146 vz)) (+ 286452836048521 (* t_146 (- 62)))))
(assert (>= t_147 0))
(assert (= (+ px (* t_147 vx)) (+ 186640407106107 (* t_147 172))))
(assert (= (+ py (* t_147 vy)) (+ 302586436160656 (* t_147 200))))
(assert (= (+ pz (* t_147 vz)) (+ 178053441373097 (* t_147 (- 99)))))
(assert (>= t_148 0))
(assert (= (+ px (* t_148 vx)) (+ 184504662208422 (* t_148 217))))
(assert (= (+ py (* t_148 vy)) (+ 279753007845271 (* t_148 645))))
(assert (= (+ pz (* t_148 vz)) (+ 194263341780489 (* t_148 (- 497)))))
(assert (>= t_149 0))
(assert (= (+ px (* t_149 vx)) (+ 207498586652070 (* t_149 88))))
(assert (= (+ py (* t_149 vy)) (+ 122966697911623 (* t_149 592))))
(assert (= (+ pz (* t_149 vz)) (+ 453309639270761 (* t_149 (- 760)))))
(assert (>= t_150 0))
(assert (= (+ px (* t_150 vx)) (+ 175420575327994 (* t_150 159))))
(assert (= (+ py (* t_150 vy)) (+ 240376844547933 (* t_150 37))))
(assert (= (+ pz (* t_150 vz)) (+ 227794777853156 (* t_150 122))))
(assert (>= t_151 0))
(assert (= (+ px (* t_151 vx)) (+ 164379037426222 (* t_151 171))))
(assert (= (+ py (* t_151 vy)) (+ 314155556336019 (* t_151 (- 59)))))
(assert (= (+ pz (* t_151 vz)) (+ 361113505933531 (* t_151 (- 30)))))
(assert (>= t_152 0))
(assert (= (+ px (* t_152 vx)) (+ 276158080997198 (* t_152 27))))
(assert (= (+ py (* t_152 vy)) (+ 255307550628353 (* t_152 22))))
(assert (= (+ pz (* t_152 vz)) (+ 190284041278157 (* t_152 167))))
(assert (>= t_153 0))
(assert (= (+ px (* t_153 vx)) (+ 188538116291142 (* t_153 166))))
(assert (= (+ py (* t_153 vy)) (+ 332645165411655 (* t_153 10))))
(assert (= (+ pz (* t_153 vz)) (+ 164893512402481 (* t_153 (- 105)))))
(assert (>= t_154 0))
(assert (= (+ px (* t_154 vx)) (+ 206485169181270 (* t_154 37))))
(assert (= (+ py (* t_154 vy)) (+ 324400373771635 (* t_154 28))))
(assert (= (+ pz (* t_154 vz)) (+ 174538862304413 (* t_154 (- 44)))))
(assert (>= t_155 0))
(assert (= (+ px (* t_155 vx)) (+ 231705775027484 (* t_155 53))))
(assert (= (+ py (* t_155 vy)) (+ 354858179856273 (* t_155 (- 119)))))
(assert (= (+ pz (* t_155 vz)) (+ 282940665637611 (* t_155 (- 77)))))
(assert (>= t_156 0))
(assert (= (+ px (* t_156 vx)) (+ 192935594972436 (* t_156 125))))
(assert (= (+ py (* t_156 vy)) (+ 232318329359044 (* t_156 770))))
(assert (= (+ pz (* t_156 vz)) (+ 140280091724297 (* t_156 173))))
(assert (>= t_157 0))
(assert (= (+ px (* t_157 vx)) (+ 195865425610134 (* t_157 121))))
(assert (= (+ py (* t_157 vy)) (+ 156203126394403 (* t_157 618))))
(assert (= (+ pz (* t_157 vz)) (+ 201075304936541 (* t_157 (- 22)))))
(assert (>= t_158 0))
(assert (= (+ px (* t_158 vx)) (+ 220291544685654 (* t_158 97))))
(assert (= (+ py (* t_158 vy)) (+ 60861797261303 (* t_158 313))))
(assert (= (+ pz (* t_158 vz)) (+ 192839119984101 (* t_158 156))))
(assert (>= t_159 0))
(assert (= (+ px (* t_159 vx)) (+ 216421547979532 (* t_159 33))))
(assert (= (+ py (* t_159 vy)) (+ 166625355222409 (* t_159 645))))
(assert (= (+ pz (* t_159 vz)) (+ 138232910764571 (* t_159 215))))
(assert (>= t_160 0))
(assert (= (+ px (* t_160 vx)) (+ 454745381031134 (* t_160 (- 229)))))
(assert (= (+ py (* t_160 vy)) (+ 359071031321598 (* t_160 (- 116)))))
(assert (= (+ pz (* t_160 vz)) (+ 433358646779191 (* t_160 (- 177)))))
(assert (>= t_161 0))
(assert (= (+ px (* t_161 vx)) (+ 241211456940334 (* t_161 87))))
(assert (= (+ py (* t_161 vy)) (+ 274238344824863 (* t_161 (- 22)))))
(assert (= (+ pz (* t_161 vz)) (+ 449761596808401 (* t_161 (- 86)))))
(assert (>= t_162 0))
(assert (= (+ px (* t_162 vx)) (+ 300489403237401 (* t_162 12))))
(assert (= (+ py (* t_162 vy)) (+ 150600505604740 (* t_162 130))))
(assert (= (+ pz (* t_162 vz)) (+ 311021695401350 (* t_162 36))))
(assert (>= t_163 0))
(assert (= (+ px (* t_163 vx)) (+ 351714451571994 (* t_163 (- 79)))))
(assert (= (+ py (* t_163 vy)) (+ 313870670017933 (* t_163 (- 54)))))
(assert (= (+ pz (* t_163 vz)) (+ 87623195530631 (* t_163 304))))
(assert (>= t_164 0))
(assert (= (+ px (* t_164 vx)) (+ 206304315814166 (* t_164 47))))
(assert (= (+ py (* t_164 vy)) (+ 322825195619263 (* t_164 27))))
(assert (= (+ pz (* t_164 vz)) (+ 165678725657741 (* t_164 35))))
(assert (>= t_165 0))
(assert (= (+ px (* t_165 vx)) (+ 235260754952454 (* t_165 88))))
(assert (= (+ py (* t_165 vy)) (+ 192089045978143 (* t_165 81))))
(assert (= (+ pz (* t_165 vz)) (+ 324835846533921 (* t_165 21))))
(assert (>= t_166 0))
(assert (= (+ px (* t_166 vx)) (+ 234012378392974 (* t_166 21))))
(assert (= (+ py (* t_166 vy)) (+ 220537666254223 (* t_166 243))))
(assert (= (+ pz (* t_166 vz)) (+ 244419610199201 (* t_166 (- 67)))))
(assert (>= t_167 0))
(assert (= (+ px (* t_167 vx)) (+ 271646520250074 (* t_167 38))))
(assert (= (+ py (* t_167 vy)) (+ 328249590902743 (* t_167 (- 75)))))
(assert (= (+ pz (* t_167 vz)) (+ 281718062915501 (* t_167 56))))
(assert (>= t_168 0))
(assert (= (+ px (* t_168 vx)) (+ 221872342890713 (* t_168 96))))
(assert (= (+ py (* t_168 vy)) (+ 311155829759331 (* t_168 (- 49)))))
(assert (= (+ pz (* t_168 vz)) (+ 169665424751063 (* t_168 191))))
(assert (>= t_169 0))
(assert (= (+ px (* t_169 vx)) (+ 234965964033108 (* t_169 53))))
(assert (= (+ py (* t_169 vy)) (+ 289605268944487 (* t_169 11))))
(assert (= (+ pz (* t_169 vz)) (+ 264575781614519 (* t_169 (- 17)))))
(assert (>= t_170 0))
(assert (= (+ px (* t_170 vx)) (+ 302656676541801 (* t_170 22))))
(assert (= (+ py (* t_170 vy)) (+ 314956862712124 (* t_170 (- 64)))))
(assert (= (+ pz (* t_170 vz)) (+ 279759708917957 (* t_170 89))))
(assert (>= t_171 0))
(assert (= (+ px (* t_171 vx)) (+ 194778772231287 (* t_171 100))))
(assert (= (+ py (* t_171 vy)) (+ 358987377936095 (* t_171 (- 269)))))
(assert (= (+ pz (* t_171 vz)) (+ 94944329588325 (* t_171 633))))
(assert (>= t_172 0))
(assert (= (+ px (* t_172 vx)) (+ 213962227655009 (* t_172 78))))
(assert (= (+ py (* t_172 vy)) (+ 360175350319088 (* t_172 (- 140)))))
(assert (= (+ pz (* t_172 vz)) (+ 187183591353131 (* t_172 95))))
(assert (>= t_173 0))
(assert (= (+ px (* t_173 vx)) (+ 335872446070469 (* t_173 (- 196)))))
(assert (= (+ py (* t_173 vy)) (+ 310194803249308 (* t_173 (- 18)))))
(assert (= (+ pz (* t_173 vz)) (+ 258956779512841 (* t_173 (- 51)))))
(assert (>= t_174 0))
(assert (= (+ px (* t_174 vx)) (+ 237632929340327 (* t_174 (- 54)))))
(assert (= (+ py (* t_174 vy)) (+ 282862400087895 (* t_174 155))))
(assert (= (+ pz (* t_174 vz)) (+ 329308829827744 (* t_174 (- 578)))))
(assert (>= t_175 0))
(assert (= (+ px (* t_175 vx)) (+ 195165381881310 (* t_175 83))))
(assert (= (+ py (* t_175 vy)) (+ 334127994548035 (* t_175 25))))
(assert (= (+ pz (* t_175 vz)) (+ 177008381765921 (* t_175 (- 395)))))
(assert (>= t_176 0))
(assert (= (+ px (* t_176 vx)) (+ 322431513433582 (* t_176 (- 117)))))
(assert (= (+ py (* t_176 vy)) (+ 335929297302159 (* t_176 (- 80)))))
(assert (= (+ pz (* t_176 vz)) (+ 292621591828001 (* t_176 (- 70)))))
(assert (>= t_177 0))
(assert (= (+ px (* t_177 vx)) (+ 315117522492294 (* t_177 (- 11)))))
(assert (= (+ py (* t_177 vy)) (+ 188045711663619 (* t_177 94))))
(assert (= (+ pz (* t_177 vz)) (+ 217859262699941 (* t_177 140))))
(assert (>= t_178 0))
(assert (= (+ px (* t_178 vx)) (+ 373704262775700 (* t_178 (- 143)))))
(assert (= (+ py (* t_178 vy)) (+ 207296292228736 (* t_178 116))))
(assert (= (+ pz (* t_178 vz)) (+ 462531809606177 (* t_178 (- 267)))))
(assert (>= t_179 0))
(assert (= (+ px (* t_179 vx)) (+ 251431566932470 (* t_179 (- 45)))))
(assert (= (+ py (* t_179 vy)) (+ 262653021312867 (* t_179 151))))
(assert (= (+ pz (* t_179 vz)) (+ 228387402272864 (* t_179 (- 52)))))
(assert (>= t_180 0))
(assert (= (+ px (* t_180 vx)) (+ 200968557727895 (* t_180 (- 28)))))
(assert (= (+ py (* t_180 vy)) (+ 335950123937744 (* t_180 20))))
(assert (= (+ pz (* t_180 vz)) (+ 148782648944484 (* t_180 (- 56)))))
(assert (>= t_181 0))
(assert (= (+ px (* t_181 vx)) (+ 236191762393467 (* t_181 22))))
(assert (= (+ py (* t_181 vy)) (+ 21120063276068 (* t_181 742))))
(assert (= (+ pz (* t_181 vz)) (+ 319730241477691 (* t_181 (- 245)))))
(assert (>= t_182 0))
(assert (= (+ px (* t_182 vx)) (+ 208913018909190 (* t_182 (- 29)))))
(assert (= (+ py (* t_182 vy)) (+ 375167847286459 (* t_182 (- 401)))))
(assert (= (+ pz (* t_182 vz)) (+ 97238860543841 (* t_182 565))))
(assert (>= t_183 0))
(assert (= (+ px (* t_183 vx)) (+ 290435031159135 (* t_183 28))))
(assert (= (+ py (* t_183 vy)) (+ 56359235789263 (* t_183 227))))
(assert (= (+ pz (* t_183 vz)) (+ 318028085602160 (* t_183 36))))
(assert (>= t_184 0))
(assert (= (+ px (* t_184 vx)) (+ 205348838719584 (* t_184 109))))
(assert (= (+ py (* t_184 vy)) (+ 129089359330730 (* t_184 358))))
(assert (= (+ pz (* t_184 vz)) (+ 397134601580767 (* t_184 (- 317)))))
(assert (>= t_185 0))
(assert (= (+ px (* t_185 vx)) (+ 194757851501280 (* t_185 122))))
(assert (= (+ py (* t_185 vy)) (+ 310732265284483 (* t_185 57))))
(assert (= (+ pz (* t_185 vz)) (+ 257897724121307 (* t_185 (- 352)))))
(assert (>= t_186 0))
(assert (= (+ px (* t_186 vx)) (+ 322105170096600 (* t_186 (- 40)))))
(assert (= (+ py (* t_186 vy)) (+ 281140697612407 (* t_186 (- 9)))))
(assert (= (+ pz (* t_186 vz)) (+ 384217392018125 (* t_186 (- 101)))))
(assert (>= t_187 0))
(assert (= (+ px (* t_187 vx)) (+ 227263802927379 (* t_187 34))))
(assert (= (+ py (* t_187 vy)) (+ 293407939553692 (* t_187 50))))
(assert (= (+ pz (* t_187 vz)) (+ 217416903679568 (* t_187 (- 6)))))
(assert (>= t_188 0))
(assert (= (+ px (* t_188 vx)) (+ 253024402494847 (* t_188 (- 60)))))
(assert (= (+ py (* t_188 vy)) (+ 472881498291876 (* t_188 (- 512)))))
(assert (= (+ pz (* t_188 vz)) (+ 346563578286452 (* t_188 (- 448)))))
(assert (>= t_189 0))
(assert (= (+ px (* t_189 vx)) (+ 314479634908016 (* t_189 (- 102)))))
(assert (= (+ py (* t_189 vy)) (+ 119470812770471 (* t_189 343))))
(assert (= (+ pz (* t_189 vz)) (+ 423291884678263 (* t_189 (- 326)))))
(assert (>= t_190 0))
(assert (= (+ px (* t_190 vx)) (+ 285064202741996 (* t_190 17))))
(assert (= (+ py (* t_190 vy)) (+ 260225765977046 (* t_190 14))))
(assert (= (+ pz (* t_190 vz)) (+ 328922413430668 (* t_190 (- 12)))))
(assert (>= t_191 0))
(assert (= (+ px (* t_191 vx)) (+ 164764803937924 (* t_191 209))))
(assert (= (+ py (* t_191 vy)) (+ 131918495543174 (* t_191 466))))
(assert (= (+ pz (* t_191 vz)) (+ 24421731030948 (* t_191 528))))
(assert (>= t_192 0))
(assert (= (+ px (* t_192 vx)) (+ 302401846001018 (* t_192 (- 43)))))
(assert (= (+ py (* t_192 vy)) (+ 47953136574059 (* t_192 389))))
(assert (= (+ pz (* t_192 vz)) (+ 415330628001011 (* t_192 (- 220)))))
(assert (>= t_193 0))
(assert (= (+ px (* t_193 vx)) (+ 136889723461149 (* t_193 254))))
(assert (= (+ py (* t_193 vy)) (+ 102922183481659 (* t_193 415))))
(assert (= (+ pz (* t_193 vz)) (+ 257049978466682 (* t_193 (- 22)))))
(assert (>= t_194 0))
(assert (= (+ px (* t_194 vx)) (+ 266977346640134 (* t_194 29))))
(assert (= (+ py (* t_194 vy)) (+ 399124471391351 (* t_194 (- 175)))))
(assert (= (+ pz (* t_194 vz)) (+ 389593482782381 (* t_194 (- 130)))))
(assert (>= t_195 0))
(assert (= (+ px (* t_195 vx)) (+ 372790937915094 (* t_195 (- 242)))))
(assert (= (+ py (* t_195 vy)) (+ 329723676236983 (* t_195 (- 66)))))
(assert (= (+ pz (* t_195 vz)) (+ 408552056960081 (* t_195 (- 337)))))
(assert (>= t_196 0))
(assert (= (+ px (* t_196 vx)) (+ 295046549007926 (* t_196 (- 93)))))
(assert (= (+ py (* t_196 vy)) (+ 307216389914204 (* t_196 (- 14)))))
(assert (= (+ pz (* t_196 vz)) (+ 245279985581636 (* t_196 (- 10)))))
(assert (>= t_197 0))
(assert (= (+ px (* t_197 vx)) (+ 222962551504923 (* t_197 42))))
(assert (= (+ py (* t_197 vy)) (+ 300940192862044 (* t_197 34))))
(assert (= (+ pz (* t_197 vz)) (+ 205863476663477 (* t_197 17))))
(assert (>= t_198 0))
(assert (= (+ px (* t_198 vx)) (+ 217936499850689 (* t_198 86))))
(assert (= (+ py (* t_198 vy)) (+ 313784346557728 (* t_198 (- 36)))))
(assert (= (+ pz (* t_198 vz)) (+ 244304797861441 (* t_198 21))))
(assert (>= t_199 0))
(assert (= (+ px (* t_199 vx)) (+ 167754243520824 (* t_199 184))))
(assert (= (+ py (* t_199 vy)) (+ 183008145578501 (* t_199 214))))
(assert (= (+ pz (* t_199 vz)) (+ 255319117162995 (* t_199 6))))
(assert (>= t_200 0))
(assert (= (+ px (* t_200 vx)) (+ 210177003182478 (* t_200 101))))
(assert (= (+ py (* t_200 vy)) (+ 429234450438847 (* t_200 (- 266)))))
(assert (= (+ pz (* t_200 vz)) (+ 105538845228113 (* t_200 296))))
(assert (>= t_201 0))
(assert (= (+ px (* t_201 vx)) (+ 199347157290654 (* t_201 99))))
(assert (= (+ py (* t_201 vy)) (+ 270021317518867 (* t_201 261))))
(assert (= (+ pz (* t_201 vz)) (+ 163266752925959 (* t_201 88))))
(assert (>= t_202 0))
(assert (= (+ px (* t_202 vx)) (+ 236595610312209 (* t_202 (- 116)))))
(assert (= (+ py (* t_202 vy)) (+ 357567541944595 (* t_202 (- 177)))))
(assert (= (+ pz (* t_202 vz)) (+ 163695965251100 (* t_202 62))))
(assert (>= t_203 0))
(assert (= (+ px (* t_203 vx)) (+ 312426175948804 (* t_203 20))))
(assert (= (+ py (* t_203 vy)) (+ 126535043607303 (* t_203 119))))
(assert (= (+ pz (* t_203 vz)) (+ 334910821408881 (* t_203 45))))
(assert (>= t_204 0))
(assert (= (+ px (* t_204 vx)) (+ 250185142335527 (* t_204 (- 40)))))
(assert (= (+ py (* t_204 vy)) (+ 339957515144567 (* t_204 (- 85)))))
(assert (= (+ pz (* t_204 vz)) (+ 186490088641817 (* t_204 77))))
(assert (>= t_205 0))
(assert (= (+ px (* t_205 vx)) (+ 187486534782198 (* t_205 145))))
(assert (= (+ py (* t_205 vy)) (+ 153491915531223 (* t_205 217))))
(assert (= (+ pz (* t_205 vz)) (+ 178050669591013 (* t_205 168))))
(assert (>= t_206 0))
(assert (= (+ px (* t_206 vx)) (+ 264452793637374 (* t_206 (- 66)))))
(assert (= (+ py (* t_206 vy)) (+ 364051575147343 (* t_206 (- 153)))))
(assert (= (+ pz (* t_206 vz)) (+ 278407165734113 (* t_206 (- 167)))))
(assert (>= t_207 0))
(assert (= (+ px (* t_207 vx)) (+ 321652447174633 (* t_207 (- 94)))))
(assert (= (+ py (* t_207 vy)) (+ 234494711812364 (* t_207 100))))
(assert (= (+ pz (* t_207 vz)) (+ 293511778578951 (* t_207 (- 45)))))
(assert (>= t_208 0))
(assert (= (+ px (* t_208 vx)) (+ 101178528277354 (* t_208 231))))
(assert (= (+ py (* t_208 vy)) (+ 45310253629503 (* t_208 211))))
(assert (= (+ pz (* t_208 vz)) (+ 279722555547721 (* t_208 93))))
(assert (>= t_209 0))
(assert (= (+ px (* t_209 vx)) (+ 311483135370989 (* t_209 (- 30)))))
(assert (= (+ py (* t_209 vy)) (+ 117588178673003 (* t_209 223))))
(assert (= (+ pz (* t_209 vz)) (+ 195876215498686 (* t_209 154))))
(assert (>= t_210 0))
(assert (= (+ px (* t_210 vx)) (+ 349074097657518 (* t_210 (- 53)))))
(assert (= (+ py (* t_210 vy)) (+ 71980788262470 (* t_210 236))))
(assert (= (+ pz (* t_210 vz)) (+ 67744127629012 (* t_210 322))))
(assert (>= t_211 0))
(assert (= (+ px (* t_211 vx)) (+ 205665951950534 (* t_211 9))))
(assert (= (+ py (* t_211 vy)) (+ 317578175678991 (* t_211 131))))
(assert (= (+ pz (* t_211 vz)) (+ 174079200152461 (* t_211 (- 140)))))
(assert (>= t_212 0))
(assert (= (+ px (* t_212 vx)) (+ 172224556223070 (* t_212 163))))
(assert (= (+ py (* t_212 vy)) (+ 207776433045037 (* t_212 78))))
(assert (= (+ pz (* t_212 vz)) (+ 341587542422723 (* t_212 (- 22)))))
(assert (>= t_213 0))
(assert (= (+ px (* t_213 vx)) (+ 199777030731058 (* t_213 108))))
(assert (= (+ py (* t_213 vy)) (+ 159408594476631 (* t_213 565))))
(assert (= (+ pz (* t_213 vz)) (+ 309534334024285 (* t_213 (- 396)))))
(assert (>= t_214 0))
(assert (= (+ px (* t_214 vx)) (+ 464121799742544 (* t_214 (- 191)))))
(assert (= (+ py (* t_214 vy)) (+ 439378219125328 (* t_214 (- 210)))))
(assert (= (+ pz (* t_214 vz)) (+ 480156984371951 (* t_214 (- 177)))))
(assert (>= t_215 0))
(assert (= (+ px (* t_215 vx)) (+ 512533623338691 (* t_215 (- 200)))))
(assert (= (+ py (* t_215 vy)) (+ 269596699742212 (* t_215 (- 16)))))
(assert (= (+ pz (* t_215 vz)) (+ 497024716185359 (* t_215 (- 141)))))
(assert (>= t_216 0))
(assert (= (+ px (* t_216 vx)) (+ 449327916519144 (* t_216 (- 131)))))
(assert (= (+ py (* t_216 vy)) (+ 205855641898298 (* t_216 50))))
(assert (= (+ pz (* t_216 vz)) (+ 303200495165981 (* t_216 65))))
(assert (>= t_217 0))
(assert (= (+ px (* t_217 vx)) (+ 283724606928492 (* t_217 38))))
(assert (= (+ py (* t_217 vy)) (+ 240851979789205 (* t_217 18))))
(assert (= (+ pz (* t_217 vz)) (+ 384065029237529 (* t_217 (- 31)))))
(assert (>= t_218 0))
(assert (= (+ px (* t_218 vx)) (+ 288013100270877 (* t_218 42))))
(assert (= (+ py (* t_218 vy)) (+ 208780552824757 (* t_218 41))))
(assert (= (+ pz (* t_218 vz)) (+ 275880042837536 (* t_218 100))))
(assert (>= t_219 0))
(assert (= (+ px (* t_219 vx)) (+ 225018718395018 (* t_219 73))))
(assert (= (+ py (* t_219 vy)) (+ 305644724002975 (* t_219 (- 21)))))
(assert (= (+ pz (* t_219 vz)) (+ 271186961007503 (* t_219 (- 28)))))
(assert (>= t_220 0))
(assert (= (+ px (* t_220 vx)) (+ 252580597893096 (* t_220 (- 14)))))
(assert (= (+ py (* t_220 vy)) (+ 289594241717095 (* t_220 39))))
(assert (= (+ pz (* t_220 vz)) (+ 283259230473967 (* t_220 (- 134)))))
(assert (>= t_221 0))
(assert (= (+ px (* t_221 vx)) (+ 217696966439229 (* t_221 82))))
(assert (= (+ py (* t_221 vy)) (+ 236860502115098 (* t_221 134))))
(assert (= (+ pz (* t_221 vz)) (+ 202812154030551 (* t_221 91))))
(assert (>= t_222 0))
(assert (= (+ px (* t_222 vx)) (+ 290383585895985 (* t_222 22))))
(assert (= (+ py (* t_222 vy)) (+ 172960262418583 (* t_222 107))))
(assert (= (+ pz (* t_222 vz)) (+ 413523311841740 (* t_222 (- 88)))))
(assert (>= t_223 0))
(assert (= (+ px (* t_223 vx)) (+ 246394854383374 (* t_223 63))))
(assert (= (+ py (* t_223 vy)) (+ 404386901502983 (* t_223 (- 178)))))
(assert (= (+ pz (* t_223 vz)) (+ 316452007110281 (* t_223 (- 10)))))
(assert (>= t_224 0))
(assert (= (+ px (* t_224 vx)) (+ 277440283560394 (* t_224 29))))
(assert (= (+ py (* t_224 vy)) (+ 298664786803743 (* t_224 (- 37)))))
(assert (= (+ pz (* t_224 vz)) (+ 343675845620671 (* t_224 (- 26)))))
(assert (>= t_225 0))
(assert (= (+ px (* t_225 vx)) (+ 549218613325353 (* t_225 (- 212)))))
(assert (= (+ py (* t_225 vy)) (+ 365039367598781 (* t_225 (- 115)))))
(assert (= (+ pz (* t_225 vz)) (+ 370814441177496 (* t_225 10))))
(assert (>= t_226 0))
(assert (= (+ px (* t_226 vx)) (+ 314422297180566 (* t_226 (- 127)))))
(assert (= (+ py (* t_226 vy)) (+ 290227116094987 (* t_226 20))))
(assert (= (+ pz (* t_226 vz)) (+ 220524013374437 (* t_226 52))))
(assert (>= t_227 0))
(assert (= (+ px (* t_227 vx)) (+ 208288985823519 (* t_227 38))))
(assert (= (+ py (* t_227 vy)) (+ 332582248866208 (* t_227 (- 34)))))
(assert (= (+ pz (* t_227 vz)) (+ 173680963176656 (* t_227 (- 6)))))
(assert (>= t_228 0))
(assert (= (+ px (* t_228 vx)) (+ 344954667419544 (* t_228 (- 11)))))
(assert (= (+ py (* t_228 vy)) (+ 271844404820980 (* t_228 (- 24)))))
(assert (= (+ pz (* t_228 vz)) (+ 373070962444213 (* t_228 9))))
(assert (>= t_229 0))
(assert (= (+ px (* t_229 vx)) (+ 253707352980234 (* t_229 22))))
(assert (= (+ py (* t_229 vy)) (+ 336179622652543 (* t_229 (- 81)))))
(assert (= (+ pz (* t_229 vz)) (+ 293095895839541 (* t_229 (- 58)))))
(assert (>= t_230 0))
(assert (= (+ px (* t_230 vx)) (+ 348619876072741 (* t_230 (- 48)))))
(assert (= (+ py (* t_230 vy)) (+ 233964822099034 (* t_230 36))))
(assert (= (+ pz (* t_230 vz)) (+ 330658038016178 (* t_230 8))))
(assert (>= t_231 0))
(assert (= (+ px (* t_231 vx)) (+ 294065185957476 (* t_231 (- 14)))))
(assert (= (+ py (* t_231 vy)) (+ 303581225750131 (* t_231 (- 35)))))
(assert (= (+ pz (* t_231 vz)) (+ 130406957718587 (* t_231 246))))
(assert (>= t_232 0))
(assert (= (+ px (* t_232 vx)) (+ 299497691666274 (* t_232 (- 30)))))
(assert (= (+ py (* t_232 vy)) (+ 143845614560983 (* t_232 217))))
(assert (= (+ pz (* t_232 vz)) (+ 193269298796021 (* t_232 148))))
(assert (>= t_233 0))
(assert (= (+ px (* t_233 vx)) (+ 243761048715324 (* t_233 (- 56)))))
(assert (= (+ py (* t_233 vy)) (+ 305091461548017 (* t_233 46))))
(assert (= (+ pz (* t_233 vz)) (+ 163187922986167 (* t_233 126))))
(assert (>= t_234 0))
(assert (= (+ px (* t_234 vx)) (+ 228852534457750 (* t_234 (- 19)))))
(assert (= (+ py (* t_234 vy)) (+ 321833988811099 (* t_234 (- 6)))))
(assert (= (+ pz (* t_234 vz)) (+ 195275147618589 (* t_234 (- 24)))))
(assert (>= t_235 0))
(assert (= (+ px (* t_235 vx)) (+ 210326083482005 (* t_235 48))))
(assert (= (+ py (* t_235 vy)) (+ 405825122389483 (* t_235 (- 393)))))
(assert (= (+ pz (* t_235 vz)) (+ 255008495328029 (* t_235 (- 343)))))
(assert (>= t_236 0))
(assert (= (+ px (* t_236 vx)) (+ 234154015900814 (* t_236 15))))
(assert (= (+ py (* t_236 vy)) (+ 320051906908983 (* t_236 (- 28)))))
(assert (= (+ pz (* t_236 vz)) (+ 254552486072961 (* t_236 (- 111)))))
(assert (>= t_237 0))
(assert (= (+ px (* t_237 vx)) (+ 221069337881082 (* t_237 40))))
(assert (= (+ py (* t_237 vy)) (+ 268544927933243 (* t_237 152))))
(assert (= (+ pz (* t_237 vz)) (+ 253793013055353 (* t_237 (- 161)))))
(assert (>= t_238 0))
(assert (= (+ px (* t_238 vx)) (+ 350843574391570 (* t_238 (- 57)))))
(assert (= (+ py (* t_238 vy)) (+ 546291208573433 (* t_238 (- 343)))))
(assert (= (+ pz (* t_238 vz)) (+ 245148884150221 (* t_238 105))))
(assert (>= t_239 0))
(assert (= (+ px (* t_239 vx)) (+ 321884637993916 (* t_239 (- 108)))))
(assert (= (+ py (* t_239 vy)) (+ 151517460880797 (* t_239 268))))
(assert (= (+ pz (* t_239 vz)) (+ 338566691457073 (* t_239 (- 147)))))
(assert (>= t_240 0))
(assert (= (+ px (* t_240 vx)) (+ 332310394683086 (* t_240 (- 133)))))
(assert (= (+ py (* t_240 vy)) (+ 296925474202815 (* t_240 (- 5)))))
(assert (= (+ pz (* t_240 vz)) (+ 290407863681483 (* t_240 (- 62)))))
(assert (>= t_241 0))
(assert (= (+ px (* t_241 vx)) (+ 238868612579282 (* t_241 (- 73)))))
(assert (= (+ py (* t_241 vy)) (+ 442767280701488 (* t_241 (- 538)))))
(assert (= (+ pz (* t_241 vz)) (+ 312738360614324 (* t_241 (- 562)))))
(assert (>= t_242 0))
(assert (= (+ px (* t_242 vx)) (+ 238005301025171 (* t_242 62))))
(assert (= (+ py (* t_242 vy)) (+ 315819717023939 (* t_242 (- 49)))))
(assert (= (+ pz (* t_242 vz)) (+ 310603161892176 (* t_242 (- 50)))))
(assert (>= t_243 0))
(assert (= (+ px (* t_243 vx)) (+ 184500511341324 (* t_243 184))))
(assert (= (+ py (* t_243 vy)) (+ 354706787987715 (* t_243 (- 175)))))
(assert (= (+ pz (* t_243 vz)) (+ 106858269141817 (* t_243 409))))
(assert (>= t_244 0))
(assert (= (+ px (* t_244 vx)) (+ 218719926572754 (* t_244 109))))
(assert (= (+ py (* t_244 vy)) (+ 248846852339899 (* t_244 9))))
(assert (= (+ pz (* t_244 vz)) (+ 417842058727985 (* t_244 (- 67)))))
(assert (>= t_245 0))
(assert (= (+ px (* t_245 vx)) (+ 61527743340558 (* t_245 311))))
(assert (= (+ py (* t_245 vy)) (+ 41910468004471 (* t_245 306))))
(assert (= (+ pz (* t_245 vz)) (+ 21054306023633 (* t_245 391))))
(assert (>= t_246 0))
(assert (= (+ px (* t_246 vx)) (+ 206891968805558 (* t_246 71))))
(assert (= (+ py (* t_246 vy)) (+ 359036109292941 (* t_246 (- 164)))))
(assert (= (+ pz (* t_246 vz)) (+ 96347232076181 (* t_246 395))))
(assert (>= t_247 0))
(assert (= (+ px (* t_247 vx)) (+ 358569854122062 (* t_247 (- 219)))))
(assert (= (+ py (* t_247 vy)) (+ 275252683087759 (* t_247 51))))
(assert (= (+ pz (* t_247 vz)) (+ 280731684589601 (* t_247 (- 75)))))
(assert (>= t_248 0))
(assert (= (+ px (* t_248 vx)) (+ 281134641567294 (* t_248 (- 11)))))
(assert (= (+ py (* t_248 vy)) (+ 255607683726743 (* t_248 52))))
(assert (= (+ pz (* t_248 vz)) (+ 288258712879345 (* t_248 (- 17)))))
(assert (>= t_249 0))
(assert (= (+ px (* t_249 vx)) (+ 325364111053745 (* t_249 (- 82)))))
(assert (= (+ py (* t_249 vy)) (+ 294010589908703 (* t_249 (- 13)))))
(assert (= (+ pz (* t_249 vz)) (+ 211245733791773 (* t_249 113))))
(assert (>= t_250 0))
(assert (= (+ px (* t_250 vx)) (+ 268578371026014 (* t_250 59))))
(assert (= (+ py (* t_250 vy)) (+ 236127445255093 (* t_250 17))))
(assert (= (+ pz (* t_250 vz)) (+ 380797038274583 (* t_250 (- 13)))))
(assert (>= t_251 0))
(assert (= (+ px (* t_251 vx)) (+ 489485534335218 (* t_251 (- 155)))))
(assert (= (+ py (* t_251 vy)) (+ 226913670756739 (* t_251 21))))
(assert (= (+ pz (* t_251 vz)) (+ 271116263277629 (* t_251 107))))
(assert (>= t_252 0))
(assert (= (+ px (* t_252 vx)) (+ 200091726654254 (* t_252 125))))
(assert (= (+ py (* t_252 vy)) (+ 345151854422543 (* t_252 (- 97)))))
(assert (= (+ pz (* t_252 vz)) (+ 355346332534721 (* t_252 (- 106)))))
(assert (>= t_253 0))
(assert (= (+ px (* t_253 vx)) (+ 288773407987668 (* t_253 (- 128)))))
(assert (= (+ py (* t_253 vy)) (+ 371116294945099 (* t_253 (- 171)))))
(assert (= (+ pz (* t_253 vz)) (+ 330355289788371 (* t_253 (- 300)))))
(assert (>= t_254 0))
(assert (= (+ px (* t_254 vx)) (+ 398345872685398 (* t_254 (- 127)))))
(assert (= (+ py (* t_254 vy)) (+ 211733420030191 (* t_254 75))))
(assert (= (+ pz (* t_254 vz)) (+ 256489704564165 (* t_254 84))))
(assert (>= t_255 0))
(assert (= (+ px (* t_255 vx)) (+ 410444070061341 (* t_255 (- 80)))))
(assert (= (+ py (* t_255 vy)) (+ 232446702321753 (* t_255 17))))
(assert (= (+ pz (* t_255 vz)) (+ 270268423194688 (* t_255 106))))
(assert (>= t_256 0))
(assert (= (+ px (* t_256 vx)) (+ 223446110503560 (* t_256 (- 23)))))
(assert (= (+ py (* t_256 vy)) (+ 342994867695369 (* t_256 (- 95)))))
(assert (= (+ pz (* t_256 vz)) (+ 176936935212271 (* t_256 15))))
(assert (>= t_257 0))
(assert (= (+ px (* t_257 vx)) (+ 221456980555537 (* t_257 8))))
(assert (= (+ py (* t_257 vy)) (+ 346760891427937 (* t_257 (- 111)))))
(assert (= (+ pz (* t_257 vz)) (+ 198873039052710 (* t_257 (- 48)))))
(assert (>= t_258 0))
(assert (= (+ px (* t_258 vx)) (+ 241138246161499 (* t_258 44))))
(assert (= (+ py (* t_258 vy)) (+ 378379591190555 (* t_258 (- 161)))))
(assert (= (+ pz (* t_258 vz)) (+ 197910544306414 (* t_258 118))))
(assert (>= t_259 0))
(assert (= (+ px (* t_259 vx)) (+ 239309488603942 (* t_259 51))))
(assert (= (+ py (* t_259 vy)) (+ 346974551472951 (* t_259 (- 101)))))
(assert (= (+ pz (* t_259 vz)) (+ 243277229211186 (* t_259 40))))
(assert (>= t_260 0))
(assert (= (+ px (* t_260 vx)) (+ 266720686719534 (* t_260 59))))
(assert (= (+ py (* t_260 vy)) (+ 249073195909171 (* t_260 6))))
(assert (= (+ pz (* t_260 vz)) (+ 326627536261997 (* t_260 38))))
(assert (>= t_261 0))
(assert (= (+ px (* t_261 vx)) (+ 175265275057344 (* t_261 228))))
(assert (= (+ py (* t_261 vy)) (+ 233389584704983 (* t_261 519))))
(assert (= (+ pz (* t_261 vz)) (+ 166232708483831 (* t_261 48))))
(assert (>= t_262 0))
(assert (= (+ px (* t_262 vx)) (+ 199647143220834 (* t_262 87))))
(assert (= (+ py (* t_262 vy)) (+ 333605166183208 (* t_262 (- 38)))))
(assert (= (+ pz (* t_262 vz)) (+ 126338949433076 (* t_262 274))))
(assert (>= t_263 0))
(assert (= (+ px (* t_263 vx)) (+ 355059474706240 (* t_263 (- 18)))))
(assert (= (+ py (* t_263 vy)) (+ 112909300036023 (* t_263 127))))
(assert (= (+ pz (* t_263 vz)) (+ 456817283755217 (* t_263 (- 67)))))
(assert (>= t_264 0))
(assert (= (+ px (* t_264 vx)) (+ 291234253229982 (* t_264 (- 17)))))
(assert (= (+ py (* t_264 vy)) (+ 225827198327447 (* t_264 89))))
(assert (= (+ pz (* t_264 vz)) (+ 300458706607553 (* t_264 (- 19)))))
(assert (>= t_265 0))
(assert (= (+ px (* t_265 vx)) (+ 289865647604208 (* t_265 12))))
(assert (= (+ py (* t_265 vy)) (+ 451420237900663 (* t_265 (- 233)))))
(assert (= (+ pz (* t_265 vz)) (+ 518182602681917 (* t_265 (- 253)))))
(assert (>= t_266 0))
(assert (= (+ px (* t_266 vx)) (+ 351557916167787 (* t_266 (- 112)))))
(assert (= (+ py (* t_266 vy)) (+ 226921027459900 (* t_266 88))))
(assert (= (+ pz (* t_266 vz)) (+ 441676807044779 (* t_266 (- 241)))))
(assert (>= t_267 0))
(assert (= (+ px (* t_267 vx)) (+ 171724416708978 (* t_267 210))))
(assert (= (+ py (* t_267 vy)) (+ 120198249743035 (* t_267 720))))
(assert (= (+ pz (* t_267 vz)) (+ 113845845697733 (* t_267 308))))
(assert (>= t_268 0))
(assert (= (+ px (* t_268 vx)) (+ 324992776605402 (* t_268 (- 35)))))
(assert (= (+ py (* t_268 vy)) (+ 546442272740313 (* t_268 (- 358)))))
(assert (= (+ pz (* t_268 vz)) (+ 176464245808959 (* t_268 186))))
(assert (>= t_269 0))
(assert (= (+ px (* t_269 vx)) (+ 266166769986634 (* t_269 9))))
(assert (= (+ py (* t_269 vy)) (+ 268730110669199 (* t_269 35))))
(assert (= (+ pz (* t_269 vz)) (+ 328440341073557 (* t_269 (- 97)))))
(assert (>= t_270 0))
(assert (= (+ px (* t_270 vx)) (+ 225525857274734 (* t_270 75))))
(assert (= (+ py (* t_270 vy)) (+ 233012276737543 (* t_270 111))))
(assert (= (+ pz (* t_270 vz)) (+ 309959118198911 (* t_270 (- 88)))))
(assert (>= t_271 0))
(assert (= (+ px (* t_271 vx)) (+ 183405703797942 (* t_271 173))))
(assert (= (+ py (* t_271 vy)) (+ 309355721084695 (* t_271 53))))
(assert (= (+ pz (* t_271 vz)) (+ 182533926443609 (* t_271 19))))
(assert (>= t_272 0))
(assert (= (+ px (* t_272 vx)) (+ 210515462842953 (* t_272 (- 72)))))
(assert (= (+ py (* t_272 vy)) (+ 291925001904295 (* t_272 459))))
(assert (= (+ pz (* t_272 vz)) (+ 215164290510485 (* t_272 (- 671)))))
(assert (>= t_273 0))
(assert (= (+ px (* t_273 vx)) (+ 235537482505454 (* t_273 (- 21)))))
(assert (= (+ py (* t_273 vy)) (+ 310690173156743 (* t_273 22))))
(assert (= (+ pz (* t_273 vz)) (+ 156326933471977 (* t_273 154))))
(assert (>= t_274 0))
(assert (= (+ px (* t_274 vx)) (+ 273084618253552 (* t_274 8))))
(assert (= (+ py (* t_274 vy)) (+ 382626888261135 (* t_274 (- 157)))))
(assert (= (+ pz (* t_274 vz)) (+ 273689280998585 (* t_274 17))))
(assert (>= t_275 0))
(assert (= (+ px (* t_275 vx)) (+ 253722385917350 (* t_275 57))))
(assert (= (+ py (* t_275 vy)) (+ 315123819243295 (* t_275 (- 57)))))
(assert (= (+ pz (* t_275 vz)) (+ 240205666004325 (* t_275 102))))
(assert (>= t_276 0))
(assert (= (+ px (* t_276 vx)) (+ 196398380835834 (* t_276 109))))
(assert (= (+ py (* t_276 vy)) (+ 355900579581511 (* t_276 (- 169)))))
(assert (= (+ pz (* t_276 vz)) (+ 153312099518087 (* t_276 118))))
(assert (>= t_277 0))
(assert (= (+ px (* t_277 vx)) (+ 283444009699329 (* t_277 (- 146)))))
(assert (= (+ py (* t_277 vy)) (+ 366561045831077 (* t_277 (- 167)))))
(assert (= (+ pz (* t_277 vz)) (+ 202002888581270 (* t_277 26))))
(assert (>= t_278 0))
(assert (= (+ px (* t_278 vx)) (+ 296532850164962 (* t_278 38))))
(assert (= (+ py (* t_278 vy)) (+ 253904723261403 (* t_278 (- 8)))))
(assert (= (+ pz (* t_278 vz)) (+ 296984689916093 (* t_278 86))))
(assert (>= t_279 0))
(assert (= (+ px (* t_279 vx)) (+ 356774602967614 (* t_279 (- 67)))))
(assert (= (+ py (* t_279 vy)) (+ 373148843974943 (* t_279 (- 131)))))
(assert (= (+ pz (* t_279 vz)) (+ 387561802202761 (* t_279 (- 74)))))
(assert (>= t_280 0))
(assert (= (+ px (* t_280 vx)) (+ 252770877244094 (* t_280 (- 25)))))
(assert (= (+ py (* t_280 vy)) (+ 318171858594683 (* t_280 (- 28)))))
(assert (= (+ pz (* t_280 vz)) (+ 216752381636081 (* t_280 17))))
(assert (>= t_281 0))
(assert (= (+ px (* t_281 vx)) (+ 338919821368038 (* t_281 (- 29)))))
(assert (= (+ py (* t_281 vy)) (+ 232645806842808 (* t_281 32))))
(assert (= (+ pz (* t_281 vz)) (+ 377368303830121 (* t_281 (- 35)))))
(assert (>= t_282 0))
(assert (= (+ px (* t_282 vx)) (+ 209566211606045 (* t_282 (- 72)))))
(assert (= (+ py (* t_282 vy)) (+ 338493165391956 (* t_282 (- 46)))))
(assert (= (+ pz (* t_282 vz)) (+ 150634080385665 (* t_282 21))))
(assert (>= t_283 0))
(assert (= (+ px (* t_283 vx)) (+ 328388255345246 (* t_283 (- 13)))))
(assert (= (+ py (* t_283 vy)) (+ 295645021337031 (* t_283 (- 41)))))
(assert (= (+ pz (* t_283 vz)) (+ 342359520358565 (* t_283 11))))
(assert (>= t_284 0))
(assert (= (+ px (* t_284 vx)) (+ 357923314873354 (* t_284 (- 145)))))
(assert (= (+ py (* t_284 vy)) (+ 213990132914548 (* t_284 126))))
(assert (= (+ pz (* t_284 vz)) (+ 252051459029871 (* t_284 39))))
(assert (>= t_285 0))
(assert (= (+ px (* t_285 vx)) (+ 300794330404169 (* t_285 (- 28)))))
(assert (= (+ py (* t_285 vy)) (+ 291383403542233 (* t_285 (- 15)))))
(assert (= (+ pz (* t_285 vz)) (+ 331991009111531 (* t_285 (- 61)))))
(assert (>= t_286 0))
(assert (= (+ px (* t_286 vx)) (+ 171452764273723 (* t_286 168))))
(assert (= (+ py (* t_286 vy)) (+ 106269888549931 (* t_286 255))))
(assert (= (+ pz (* t_286 vz)) (+ 325980849738994 (* t_286 (- 42)))))
(assert (>= t_287 0))
(assert (= (+ px (* t_287 vx)) (+ 400651551538638 (* t_287 (- 113)))))
(assert (= (+ py (* t_287 vy)) (+ 227035846405175 (* t_287 46))))
(assert (= (+ pz (* t_287 vz)) (+ 440348818761665 (* t_287 (- 127)))))
(assert (>= t_288 0))
(assert (= (+ px (* t_288 vx)) (+ 183528864416638 (* t_288 155))))
(assert (= (+ py (* t_288 vy)) (+ 337358904333282 (* t_288 (- 82)))))
(assert (= (+ pz (* t_288 vz)) (+ 149647897440530 (* t_288 206))))
(assert (>= t_289 0))
(assert (= (+ px (* t_289 vx)) (+ 407834029671234 (* t_289 (- 126)))))
(assert (= (+ py (* t_289 vy)) (+ 363038317346083 (* t_289 (- 118)))))
(assert (= (+ pz (* t_289 vz)) (+ 326507144649005 (* t_289 6))))
(assert (>= t_290 0))
(assert (= (+ px (* t_290 vx)) (+ 261232554625244 (* t_290 (- 139)))))
(assert (= (+ py (* t_290 vy)) (+ 272762277507558 (* t_290 184))))
(assert (= (+ pz (* t_290 vz)) (+ 260158766990881 (* t_290 (- 267)))))
(assert (>= t_291 0))
(assert (= (+ px (* t_291 vx)) (+ 276291421501401 (* t_291 32))))
(assert (= (+ py (* t_291 vy)) (+ 231191690007043 (* t_291 47))))
(assert (= (+ pz (* t_291 vz)) (+ 332403327250334 (* t_291 (- 8)))))
(assert (>= t_292 0))
(assert (= (+ px (* t_292 vx)) (+ 213146770430035 (* t_292 36))))
(assert (= (+ py (* t_292 vy)) (+ 320595954009642 (* t_292 10))))
(assert (= (+ pz (* t_292 vz)) (+ 182342124018161 (* t_292 5))))
(assert (>= t_293 0))
(assert (= (+ px (* t_293 vx)) (+ 431072263340031 (* t_293 (- 234)))))
(assert (= (+ py (* t_293 vy)) (+ 549716908674601 (* t_293 (- 415)))))
(assert (= (+ pz (* t_293 vz)) (+ 541461834661703 (* t_293 (- 393)))))
(assert (>= t_294 0))
(assert (= (+ px (* t_294 vx)) (+ 271067118142410 (* t_294 25))))
(assert (= (+ py (* t_294 vy)) (+ 252860807780751 (* t_294 35))))
(assert (= (+ pz (* t_294 vz)) (+ 293724860670289 (* t_294 13))))
(assert (>= t_295 0))
(assert (= (+ px (* t_295 vx)) (+ 230424456187626 (* t_295 76))))
(assert (= (+ py (* t_295 vy)) (+ 346336855193767 (* t_295 (- 99)))))
(assert (= (+ pz (* t_295 vz)) (+ 374228162998841 (* t_295 (- 145)))))
(assert (>= t_296 0))
(assert (= (+ px (* t_296 vx)) (+ 233683858918340 (* t_296 45))))
(assert (= (+ py (* t_296 vy)) (+ 451654359126852 (* t_296 (- 334)))))
(assert (= (+ pz (* t_296 vz)) (+ 407119183631371 (* t_296 (- 365)))))
(assert (>= t_297 0))
(assert (= (+ px (* t_297 vx)) (+ 309530132675051 (* t_297 (- 118)))))
(assert (= (+ py (* t_297 vy)) (+ 360560922327322 (* t_297 (- 132)))))
(assert (= (+ pz (* t_297 vz)) (+ 427729374335125 (* t_297 (- 399)))))
(assert (>= t_298 0))
(assert (= (+ px (* t_298 vx)) (+ 171253360815090 (* t_298 286))))
(assert (= (+ py (* t_298 vy)) (+ 226755112694191 (* t_298 763))))
(assert (= (+ pz (* t_298 vz)) (+ 106314555408725 (* t_298 428))))
(assert (>= t_299 0))
(assert (= (+ px (* t_299 vx)) (+ 195185795409569 (* t_299 134))))
(assert (= (+ py (* t_299 vy)) (+ 365215513552403 (* t_299 (- 121)))))
(assert (= (+ pz (* t_299 vz)) (+ 270027401984661 (* t_299 73))))
(check-sat)