Forum Programmation.autre Advent of Code 2023, jour 24

Posté par  . Licence CC By‑SA.
Étiquettes :
2
24
déc.
2023

Dans ce problème, on a un ensemble de grêlons qui se déplacent dans un espace en 3 dimensions.
Ces grêlons ont une position initiale et une vitesse de déplacement.

Voici l'exemple.

19, 13, 30 @ -2,  1, -2
18, 19, 22 @ -1, -1, -2
20, 25, 34 @ -2, -2, -4
12, 31, 28 @ -1, -2, -1
20, 19, 15 @  1, -5, -3

Les trois premiers nombres sont les coordonnées initiales du grêlon (px, py, pz) et les trois suivantes sont un vecteur de vitesse (vx, vy, vz)..

Dans la première partie, on ignore la coordonnée z et on cherche à trouver combien de paires de trajectoires de grêlon se croisent dans une zone donnée: les coordonnées x et y
de l'intersection doivent se trouver entre 200_000_000_000_000 et 400_000_000_000_000.
Ces coordonnées ne sont pas forcément entières.
Remarquons qu'on parle des trajectoires: elles peuvent se croiser sans nécessairement que les deux grelons rentrent en collision.

Dans la partie 2, on essaie de trouver la position initiale et la vitesse d'un nouveau grélon qui va entrer en collision avec tous les autres.
La réponse est le produit des trois coordonnées initiales.

  • # Solution en Haskell

    Posté par  . Évalué à 2.

    Pour la première partie, il faut déterminer le point d'intersection entre deux droites données par chacune par un point et un vecteur.
    Je n'avais pas trop envie de me prendre la tête à calculer ça alors j'ai regardé sur Wikipedia. J'ai bien fait parce que la formule n'est pas évidente.

    https://en.wikipedia.org/wiki/Line%E2%80%93line_intersection

    Pour la partie 2:
    étant données n grelons de positions initiales px_i, py_i pz_i et de vitesse vx_i, vy_i vz_i, il faut trouver un grelon de position initial px, py, pz et de vitesse vx, vy, vz qui rentre en collision avec tous les autres.

    C'est à dire que pour tout i dans [1..n], il existe un temps t_i tel que
    - px + vx * t_i = px_i + vx_i * t_i
    - py + vy * t_i = py_i + vy_i * t_i
    - pz + vz * t_i = pz_i + vz_i * t_i

    Ca revient donc à résoudre un système d'équations linéaires (avec une matrice sparse).
    Comme je n'avais pas envie de réimplémenter ça, j'ai utilisé Z3. Et là, c'est vraiment une purge, le binding Z3 n'est pas terrible, il est beaucoup trop verbeux.
    Je vais essayer d'écrire quelques helpers pour simplifier ça si j'ai le temps.
    Ou alors, utiliser une autre librairie.

    Voici le code:

    type Position = V3 Integer
    type Velocity = V3 Integer
    data Hailstone = Hailstone !Position !Velocity
    
    parser :: Parser [Hailstone]
    parser = hailstone `sepEndBy1` eol where
        hailstone = Hailstone <$> v3 <* " @ " <*> v3
        v3 = do 
            x <- hspace *> signedDecimal 
            y <- ", " *> hspace *> signedDecimal 
            z <- "," *> hspace *> signedDecimal
            pure $ V3 x y z
    
    cross :: Hailstone -> Hailstone -> Maybe (V2 Rational)
    cross (Hailstone (V3 px1 py1 _) (V3 vx1 vy1 _)) (Hailstone (V3 px2 py2 _) (V3 vx2 vy2 _)) =
        if d == 0
            then Nothing
            else Just $! V2 x y
        where
        px3 = px1 + vx1
        px4 = px2 + vx2
        py3 = py1 + vy1
        py4 = py2 + vy2
        q1 = fromIntegral $ (px2 * py4 - py2 * px4) * vx1 - (px1 * py3 - py1 * px3) * vx2
        q2 = fromIntegral $ (px2 * py4 - py2 * px4) * vy1 - (px1 * py3 - py1 * px3) * vy2
        d = fromIntegral $ vx1 * vy2 - vy1 * vx2
        x = q1 / d
        y = q2 / d
    
    crossesInsideTestArea :: Int -> Int -> Hailstone -> Hailstone -> Bool
    crossesInsideTestArea  start end h1@(Hailstone (V3 px1 _ _) (V3 vx1 _ _)) 
                                     h2@(Hailstone (V3 px2 _ _) (V3 vx2 _ _)) =
        fromMaybe False do
            V2 x y <- cross h1 h2
            guard $ fromIntegral vx1 * (x - fromIntegral px1) >= 0
            guard $ fromIntegral vx2 * (x - fromIntegral px2) >= 0
            let start' = fromIntegral start
            let end' = fromIntegral end
            pure $ x >= start' && y >= start' && x <= end' && y <= end'
    
    part1 :: [Hailstone] -> Int
    part1 = count id . pairwise (crossesInsideTestArea 200_000_000_000_000 400_000_000_000_000)
    
    script :: [Hailstone] -> Z3 (Maybe [Integer])
    script hailstones = do
        _0 <- mkRealNum (0 :: Int)
        px <- mkFreshRealVar "px"
        py <- mkFreshRealVar "py"
        pz <- mkFreshRealVar "pz"
        vx <- mkFreshRealVar "vy"
        vy <- mkFreshRealVar "vy"
        vz <- mkFreshRealVar "vz"
        forM_ (zip [(0::Int)..] hailstones) \(i, Hailstone (V3 pxi pyi pzi) (V3 vxi vyi vzi)) -> do
            ti <- mkFreshRealVar ("t" <> show i)
            _vxi <- mkRealNum (-vxi)
            _vyi <- mkRealNum (-vyi)
            _vzi <- mkRealNum (-vzi)
            s1 <- mkAdd =<< sequence [pure px, mkMul [ti, vx], mkRealNum (-pxi), mkMul [ti, _vxi]]
            s2 <- mkAdd =<< sequence [pure py, mkMul [ti, vy], mkRealNum (-pyi), mkMul [ti, _vyi]]
            s3 <- mkAdd =<< sequence [pure pz, mkMul [ti, vz], mkRealNum (-pzi), mkMul [ti, _vzi]]
            assert =<< mkEq s1 _0
            assert =<< mkEq s2 _0
            assert =<< mkEq s3 _0
        fmap snd $ withModel $ \m ->
            catMaybes <$> mapM (evalInt m) [px,py,pz]
    
    part2 :: [Hailstone] -> Maybe Integer
    part2 hailstones =
        unsafePerformIO do
            sol <- evalZ3 (script hailstones)
            pure $ sum <$> sol
    
    solve :: Text -> IO ()
    solve = aoc parser part1 part2
    • [^] # Re: Solution en Haskell

      Posté par  . Évalué à 2. Dernière modification le 24 décembre 2023 à 12:26.

      Petite erreur de ma part, ce n'est pas un système d'équations linéaires mais quadratiques.
      Mais bon, ça n'empêche pas à Z3 de le résoudre.

      Comme annoncé, j'ai écrit des petites fonctions utilitaires pour Z3.
      Ca donne ça. C'est plus lisible qu'avant (si on a un peu l'habitude de la syntaxe d'Haskell.

      script :: [Hailstone] -> Z3 (Maybe [Integer])
      script hailstones = do
          px <- mkFreshRealVar "px"
          py <- mkFreshRealVar "py"
          pz <- mkFreshRealVar "pz"
          vx <- mkFreshRealVar "vy"
          vy <- mkFreshRealVar "vy"
          vz <- mkFreshRealVar "vz"
          forM_ (zip [(0::Int)..] hailstones) \(i, Hailstone (V3 pxi pyi pzi) (V3 vxi vyi vzi)) -> do
              ti <- mkFreshRealVar ("t" <> show i)
              assert =<< px +& ti *& vx ==& pxi +& ti *& vxi
              assert =<< py +& ti *& vy ==& pyi +& ti *& vyi
              assert =<< pz +& ti *& vz ==& pzi +& ti *& vzi
          getIntResults [px,py,pz]
  • # J'ai aussi utilisé le Z3 theorem prover.

    Posté par  . Évalué à 1. Dernière modification le 31 décembre 2023 à 11:07.

    J'ai aussi utilisé le Z3 theorem prover.

    En gros, je pose pour chaque axe & chaque grelon

    rock.x + t1 * rock.vx = grelon.x + t1 * grelon.vx
    rock.y + t1 * rock.vy = grelon.y + t1 * grelon.vy
    rock.z + t1 * rock.vz = grelon.z + t1 * grelon.vz

    Le solve du z3 se charge de trouver la solution des systèmes d'équation.
    Vu que je suis plus habitué à Java pour le parsing du input , j'ai écrit un petit programme qui me génère le code typescript attendu par le solver Z3.
    La première version pouvait directement s'éxecuter dans la sandbox https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples/

    On peut aussi l'éxecuter en locale de cette manière:
    Via package.json

    {
      "dependencies": {
        "z3-solver": "4.12.4"
      },
      "devDependencies": {
        "@types/node": "^20.10.5",
        "typescript": "^5.3.3"
      }
    }

    Code typescript

    const { init } = require('z3-solver');
    
    
    async function execute() {
        const { Context } = await init();
        const Z3 = Context('main');
    
        // Z3 https://microsoft.github.io/z3guide/programming/Z3 JavaScript Examples
    const x = Z3.Int.const('x');
    const y = Z3.Int.const('y');
    const z = Z3.Int.const('z');
    const vx = Z3.Int.const('vx');
    const vy = Z3.Int.const('vy');
    const vz = Z3.Int.const('vz');
    
    
    const t0 = Z3.Int.const('t0') 
    const t1 = Z3.Int.const('t1') 
    const t2 = Z3.Int.const('t2') 
    const t3 = Z3.Int.const('t3') 
    const t4 = Z3.Int.const('t4') 
    const t5 = Z3.Int.const('t5') 
    const t6 = Z3.Int.const('t6') 
    const t7 = Z3.Int.const('t7') 
    const t8 = Z3.Int.const('t8') 
    const t9 = Z3.Int.const('t9') 
    const t10 = Z3.Int.const('t10') 
    const t11 = Z3.Int.const('t11') 
    const t12 = Z3.Int.const('t12') 
    const t13 = Z3.Int.const('t13') 
    const t14 = Z3.Int.const('t14') 
    const t15 = Z3.Int.const('t15') 
    const t16 = Z3.Int.const('t16') 
    const t17 = Z3.Int.const('t17') 
    const t18 = Z3.Int.const('t18') 
    const t19 = Z3.Int.const('t19') 
    const t20 = Z3.Int.const('t20') 
    const t21 = Z3.Int.const('t21') 
    const t22 = Z3.Int.const('t22') 
    const t23 = Z3.Int.const('t23') 
    const t24 = Z3.Int.const('t24') 
    const t25 = Z3.Int.const('t25') 
    const t26 = Z3.Int.const('t26') 
    const t27 = Z3.Int.const('t27') 
    const t28 = Z3.Int.const('t28') 
    const t29 = Z3.Int.const('t29') 
    const t30 = Z3.Int.const('t30') 
    const t31 = Z3.Int.const('t31') 
    const t32 = Z3.Int.const('t32') 
    const t33 = Z3.Int.const('t33') 
    const t34 = Z3.Int.const('t34') 
    const t35 = Z3.Int.const('t35') 
    const t36 = Z3.Int.const('t36') 
    const t37 = Z3.Int.const('t37') 
    const t38 = Z3.Int.const('t38') 
    const t39 = Z3.Int.const('t39') 
    const t40 = Z3.Int.const('t40') 
    const t41 = Z3.Int.const('t41') 
    const t42 = Z3.Int.const('t42') 
    const t43 = Z3.Int.const('t43') 
    const t44 = Z3.Int.const('t44') 
    const t45 = Z3.Int.const('t45') 
    const t46 = Z3.Int.const('t46') 
    const t47 = Z3.Int.const('t47') 
    const t48 = Z3.Int.const('t48') 
    const t49 = Z3.Int.const('t49') 
    const t50 = Z3.Int.const('t50') 
    const t51 = Z3.Int.const('t51') 
    const t52 = Z3.Int.const('t52') 
    const t53 = Z3.Int.const('t53') 
    const t54 = Z3.Int.const('t54') 
    const t55 = Z3.Int.const('t55') 
    const t56 = Z3.Int.const('t56') 
    const t57 = Z3.Int.const('t57') 
    const t58 = Z3.Int.const('t58') 
    const t59 = Z3.Int.const('t59') 
    const t60 = Z3.Int.const('t60') 
    const t61 = Z3.Int.const('t61') 
    const t62 = Z3.Int.const('t62') 
    const t63 = Z3.Int.const('t63') 
    const t64 = Z3.Int.const('t64') 
    const t65 = Z3.Int.const('t65') 
    const t66 = Z3.Int.const('t66') 
    const t67 = Z3.Int.const('t67') 
    const t68 = Z3.Int.const('t68') 
    const t69 = Z3.Int.const('t69') 
    const t70 = Z3.Int.const('t70') 
    const t71 = Z3.Int.const('t71') 
    const t72 = Z3.Int.const('t72') 
    const t73 = Z3.Int.const('t73') 
    const t74 = Z3.Int.const('t74') 
    const t75 = Z3.Int.const('t75') 
    const t76 = Z3.Int.const('t76') 
    const t77 = Z3.Int.const('t77') 
    const t78 = Z3.Int.const('t78') 
    const t79 = Z3.Int.const('t79') 
    const t80 = Z3.Int.const('t80') 
    const t81 = Z3.Int.const('t81') 
    const t82 = Z3.Int.const('t82') 
    const t83 = Z3.Int.const('t83') 
    const t84 = Z3.Int.const('t84') 
    const t85 = Z3.Int.const('t85') 
    const t86 = Z3.Int.const('t86') 
    const t87 = Z3.Int.const('t87') 
    const t88 = Z3.Int.const('t88') 
    const t89 = Z3.Int.const('t89') 
    const t90 = Z3.Int.const('t90') 
    const t91 = Z3.Int.const('t91') 
    const t92 = Z3.Int.const('t92') 
    const t93 = Z3.Int.const('t93') 
    const t94 = Z3.Int.const('t94') 
    const t95 = Z3.Int.const('t95') 
    const t96 = Z3.Int.const('t96') 
    const t97 = Z3.Int.const('t97') 
    const t98 = Z3.Int.const('t98') 
    const t99 = Z3.Int.const('t99') 
    const t100 = Z3.Int.const('t100') 
    const t101 = Z3.Int.const('t101') 
    const t102 = Z3.Int.const('t102') 
    const t103 = Z3.Int.const('t103') 
    const t104 = Z3.Int.const('t104') 
    const t105 = Z3.Int.const('t105') 
    const t106 = Z3.Int.const('t106') 
    const t107 = Z3.Int.const('t107') 
    const t108 = Z3.Int.const('t108') 
    const t109 = Z3.Int.const('t109') 
    const t110 = Z3.Int.const('t110') 
    const t111 = Z3.Int.const('t111') 
    const t112 = Z3.Int.const('t112') 
    const t113 = Z3.Int.const('t113') 
    const t114 = Z3.Int.const('t114') 
    const t115 = Z3.Int.const('t115') 
    const t116 = Z3.Int.const('t116') 
    const t117 = Z3.Int.const('t117') 
    const t118 = Z3.Int.const('t118') 
    const t119 = Z3.Int.const('t119') 
    const t120 = Z3.Int.const('t120') 
    const t121 = Z3.Int.const('t121') 
    const t122 = Z3.Int.const('t122') 
    const t123 = Z3.Int.const('t123') 
    const t124 = Z3.Int.const('t124') 
    const t125 = Z3.Int.const('t125') 
    const t126 = Z3.Int.const('t126') 
    const t127 = Z3.Int.const('t127') 
    const t128 = Z3.Int.const('t128') 
    const t129 = Z3.Int.const('t129') 
    const t130 = Z3.Int.const('t130') 
    const t131 = Z3.Int.const('t131') 
    const t132 = Z3.Int.const('t132') 
    const t133 = Z3.Int.const('t133') 
    const t134 = Z3.Int.const('t134') 
    const t135 = Z3.Int.const('t135') 
    const t136 = Z3.Int.const('t136') 
    const t137 = Z3.Int.const('t137') 
    const t138 = Z3.Int.const('t138') 
    const t139 = Z3.Int.const('t139') 
    const t140 = Z3.Int.const('t140') 
    const t141 = Z3.Int.const('t141') 
    const t142 = Z3.Int.const('t142') 
    const t143 = Z3.Int.const('t143') 
    const t144 = Z3.Int.const('t144') 
    const t145 = Z3.Int.const('t145') 
    const t146 = Z3.Int.const('t146') 
    const t147 = Z3.Int.const('t147') 
    const t148 = Z3.Int.const('t148') 
    const t149 = Z3.Int.const('t149') 
    const t150 = Z3.Int.const('t150') 
    const t151 = Z3.Int.const('t151') 
    const t152 = Z3.Int.const('t152') 
    const t153 = Z3.Int.const('t153') 
    const t154 = Z3.Int.const('t154') 
    const t155 = Z3.Int.const('t155') 
    const t156 = Z3.Int.const('t156') 
    const t157 = Z3.Int.const('t157') 
    const t158 = Z3.Int.const('t158') 
    const t159 = Z3.Int.const('t159') 
    const t160 = Z3.Int.const('t160') 
    const t161 = Z3.Int.const('t161') 
    const t162 = Z3.Int.const('t162') 
    const t163 = Z3.Int.const('t163') 
    const t164 = Z3.Int.const('t164') 
    const t165 = Z3.Int.const('t165') 
    const t166 = Z3.Int.const('t166') 
    const t167 = Z3.Int.const('t167') 
    const t168 = Z3.Int.const('t168') 
    const t169 = Z3.Int.const('t169') 
    const t170 = Z3.Int.const('t170') 
    const t171 = Z3.Int.const('t171') 
    const t172 = Z3.Int.const('t172') 
    const t173 = Z3.Int.const('t173') 
    const t174 = Z3.Int.const('t174') 
    const t175 = Z3.Int.const('t175') 
    const t176 = Z3.Int.const('t176') 
    const t177 = Z3.Int.const('t177') 
    const t178 = Z3.Int.const('t178') 
    const t179 = Z3.Int.const('t179') 
    const t180 = Z3.Int.const('t180') 
    const t181 = Z3.Int.const('t181') 
    const t182 = Z3.Int.const('t182') 
    const t183 = Z3.Int.const('t183') 
    const t184 = Z3.Int.const('t184') 
    const t185 = Z3.Int.const('t185') 
    const t186 = Z3.Int.const('t186') 
    const t187 = Z3.Int.const('t187') 
    const t188 = Z3.Int.const('t188') 
    const t189 = Z3.Int.const('t189') 
    const t190 = Z3.Int.const('t190') 
    const t191 = Z3.Int.const('t191') 
    const t192 = Z3.Int.const('t192') 
    const t193 = Z3.Int.const('t193') 
    const t194 = Z3.Int.const('t194') 
    const t195 = Z3.Int.const('t195') 
    const t196 = Z3.Int.const('t196') 
    const t197 = Z3.Int.const('t197') 
    const t198 = Z3.Int.const('t198') 
    const t199 = Z3.Int.const('t199') 
    const t200 = Z3.Int.const('t200') 
    const t201 = Z3.Int.const('t201') 
    const t202 = Z3.Int.const('t202') 
    const t203 = Z3.Int.const('t203') 
    const t204 = Z3.Int.const('t204') 
    const t205 = Z3.Int.const('t205') 
    const t206 = Z3.Int.const('t206') 
    const t207 = Z3.Int.const('t207') 
    const t208 = Z3.Int.const('t208') 
    const t209 = Z3.Int.const('t209') 
    const t210 = Z3.Int.const('t210') 
    const t211 = Z3.Int.const('t211') 
    const t212 = Z3.Int.const('t212') 
    const t213 = Z3.Int.const('t213') 
    const t214 = Z3.Int.const('t214') 
    const t215 = Z3.Int.const('t215') 
    const t216 = Z3.Int.const('t216') 
    const t217 = Z3.Int.const('t217') 
    const t218 = Z3.Int.const('t218') 
    const t219 = Z3.Int.const('t219') 
    const t220 = Z3.Int.const('t220') 
    const t221 = Z3.Int.const('t221') 
    const t222 = Z3.Int.const('t222') 
    const t223 = Z3.Int.const('t223') 
    const t224 = Z3.Int.const('t224') 
    const t225 = Z3.Int.const('t225') 
    const t226 = Z3.Int.const('t226') 
    const t227 = Z3.Int.const('t227') 
    const t228 = Z3.Int.const('t228') 
    const t229 = Z3.Int.const('t229') 
    const t230 = Z3.Int.const('t230') 
    const t231 = Z3.Int.const('t231') 
    const t232 = Z3.Int.const('t232') 
    const t233 = Z3.Int.const('t233') 
    const t234 = Z3.Int.const('t234') 
    const t235 = Z3.Int.const('t235') 
    const t236 = Z3.Int.const('t236') 
    const t237 = Z3.Int.const('t237') 
    const t238 = Z3.Int.const('t238') 
    const t239 = Z3.Int.const('t239') 
    const t240 = Z3.Int.const('t240') 
    const t241 = Z3.Int.const('t241') 
    const t242 = Z3.Int.const('t242') 
    const t243 = Z3.Int.const('t243') 
    const t244 = Z3.Int.const('t244') 
    const t245 = Z3.Int.const('t245') 
    const t246 = Z3.Int.const('t246') 
    const t247 = Z3.Int.const('t247') 
    const t248 = Z3.Int.const('t248') 
    const t249 = Z3.Int.const('t249') 
    const t250 = Z3.Int.const('t250') 
    const t251 = Z3.Int.const('t251') 
    const t252 = Z3.Int.const('t252') 
    const t253 = Z3.Int.const('t253') 
    const t254 = Z3.Int.const('t254') 
    const t255 = Z3.Int.const('t255') 
    const t256 = Z3.Int.const('t256') 
    const t257 = Z3.Int.const('t257') 
    const t258 = Z3.Int.const('t258') 
    const t259 = Z3.Int.const('t259') 
    const t260 = Z3.Int.const('t260') 
    const t261 = Z3.Int.const('t261') 
    const t262 = Z3.Int.const('t262') 
    const t263 = Z3.Int.const('t263') 
    const t264 = Z3.Int.const('t264') 
    const t265 = Z3.Int.const('t265') 
    const t266 = Z3.Int.const('t266') 
    const t267 = Z3.Int.const('t267') 
    const t268 = Z3.Int.const('t268') 
    const t269 = Z3.Int.const('t269') 
    const t270 = Z3.Int.const('t270') 
    const t271 = Z3.Int.const('t271') 
    const t272 = Z3.Int.const('t272') 
    const t273 = Z3.Int.const('t273') 
    const t274 = Z3.Int.const('t274') 
    const t275 = Z3.Int.const('t275') 
    const t276 = Z3.Int.const('t276') 
    const t277 = Z3.Int.const('t277') 
    const t278 = Z3.Int.const('t278') 
    const t279 = Z3.Int.const('t279') 
    const t280 = Z3.Int.const('t280') 
    const t281 = Z3.Int.const('t281') 
    const t282 = Z3.Int.const('t282') 
    const t283 = Z3.Int.const('t283') 
    const t284 = Z3.Int.const('t284') 
    const t285 = Z3.Int.const('t285') 
    const t286 = Z3.Int.const('t286') 
    const t287 = Z3.Int.const('t287') 
    const t288 = Z3.Int.const('t288') 
    const t289 = Z3.Int.const('t289') 
    const t290 = Z3.Int.const('t290') 
    const t291 = Z3.Int.const('t291') 
    const t292 = Z3.Int.const('t292') 
    const t293 = Z3.Int.const('t293') 
    const t294 = Z3.Int.const('t294') 
    const t295 = Z3.Int.const('t295') 
    const t296 = Z3.Int.const('t296') 
    const t297 = Z3.Int.const('t297') 
    const t298 = Z3.Int.const('t298') 
    const t299 = Z3.Int.const('t299') 
    const eqs = [];
    let px, py, pz, vpx, vpy, vpz;
    px = 246694783951603;
    py = 201349632539530;
    pz = 307741668306846;
    vpx = 54;
    vpy = -21;
    vpz = 12;
    
    
    eqs.push(x.add(t0.mul(vx)).eq(t0.mul(vpx).add(px)));
    eqs.push(y.add(t0.mul(vy)).eq(t0.mul(vpy).add(py)));
    eqs.push(z.add(t0.mul(vz)).eq(t0.mul(vpz).add(pz)));
    px = 220339749104883;
    py = 131993821472398;
    pz = 381979584524072;
    vpx = 77;
    vpy = 7;
    vpz = -58;
    
    
    eqs.push(x.add(t1.mul(vx)).eq(t1.mul(vpx).add(px)));
    eqs.push(y.add(t1.mul(vy)).eq(t1.mul(vpy).add(py)));
    eqs.push(z.add(t1.mul(vz)).eq(t1.mul(vpz).add(pz)));
    px = 148729713759711;
    py = 225554040514665;
    pz = 96860758795727;
    vpx = 238;
    vpy = 84;
    vpz = 360;
    
    
    eqs.push(x.add(t2.mul(vx)).eq(t2.mul(vpx).add(px)));
    eqs.push(y.add(t2.mul(vy)).eq(t2.mul(vpy).add(py)));
    eqs.push(z.add(t2.mul(vz)).eq(t2.mul(vpz).add(pz)));
    px = 243519011458151;
    py = 277335413285770;
    pz = 177685287085848;
    vpx = 57;
    vpy = -116;
    vpz = 163;
    
    
    eqs.push(x.add(t3.mul(vx)).eq(t3.mul(vpx).add(px)));
    eqs.push(y.add(t3.mul(vy)).eq(t3.mul(vpy).add(py)));
    eqs.push(z.add(t3.mul(vz)).eq(t3.mul(vpz).add(pz)));
    px = 143332267182217;
    py = 225367189590686;
    pz = 145981889711118;
    vpx = 171;
    vpy = -59;
    vpz = 198;
    
    
    eqs.push(x.add(t4.mul(vx)).eq(t4.mul(vpx).add(px)));
    eqs.push(y.add(t4.mul(vy)).eq(t4.mul(vpy).add(py)));
    eqs.push(z.add(t4.mul(vz)).eq(t4.mul(vpz).add(pz)));
    px = 254741732348622;
    py = 413864429531780;
    pz = 57992504228203;
    vpx = 53;
    vpy = -245;
    vpz = 424;
    
    
    eqs.push(x.add(t5.mul(vx)).eq(t5.mul(vpx).add(px)));
    eqs.push(y.add(t5.mul(vy)).eq(t5.mul(vpy).add(py)));
    eqs.push(z.add(t5.mul(vz)).eq(t5.mul(vpz).add(pz)));
    px = 287588175352717;
    py = 369004130634898;
    pz = 288915032357048;
    vpx = -39;
    vpy = 27;
    vpz = -7;
    
    
    eqs.push(x.add(t6.mul(vx)).eq(t6.mul(vpx).add(px)));
    eqs.push(y.add(t6.mul(vy)).eq(t6.mul(vpy).add(py)));
    eqs.push(z.add(t6.mul(vz)).eq(t6.mul(vpz).add(pz)));
    px = 447514372965507;
    py = 419011885432650;
    pz = 289910622198608;
    vpx = -184;
    vpy = -278;
    vpz = 33;
    
    
    eqs.push(x.add(t7.mul(vx)).eq(t7.mul(vpx).add(px)));
    eqs.push(y.add(t7.mul(vy)).eq(t7.mul(vpy).add(py)));
    eqs.push(z.add(t7.mul(vz)).eq(t7.mul(vpz).add(pz)));
    px = 423849084726710;
    py = 199213120137139;
    pz = 503612707855311;
    vpx = -173;
    vpy = 12;
    vpz = -246;
    
    
    eqs.push(x.add(t8.mul(vx)).eq(t8.mul(vpx).add(px)));
    eqs.push(y.add(t8.mul(vy)).eq(t8.mul(vpy).add(py)));
    eqs.push(z.add(t8.mul(vz)).eq(t8.mul(vpz).add(pz)));
    px = 144839738540189;
    py = 369107692234507;
    pz = 296030329229962;
    vpx = 168;
    vpy = -224;
    vpz = 27;
    
    
    eqs.push(x.add(t9.mul(vx)).eq(t9.mul(vpx).add(px)));
    eqs.push(y.add(t9.mul(vy)).eq(t9.mul(vpy).add(py)));
    eqs.push(z.add(t9.mul(vz)).eq(t9.mul(vpz).add(pz)));
    px = 360925037945229;
    py = 286810941619090;
    pz = 174184175152638;
    vpx = -61;
    vpy = -161;
    vpz = 148;
    
    
    eqs.push(x.add(t10.mul(vx)).eq(t10.mul(vpx).add(px)));
    eqs.push(y.add(t10.mul(vy)).eq(t10.mul(vpy).add(py)));
    eqs.push(z.add(t10.mul(vz)).eq(t10.mul(vpz).add(pz)));
    px = 251557757123447;
    py = 3211438473033;
    pz = 459503063519822;
    vpx = 46;
    vpy = 158;
    vpz = -145;
    
    
    eqs.push(x.add(t11.mul(vx)).eq(t11.mul(vpx).add(px)));
    eqs.push(y.add(t11.mul(vy)).eq(t11.mul(vpy).add(py)));
    eqs.push(z.add(t11.mul(vz)).eq(t11.mul(vpz).add(pz)));
    px = 316625519187704;
    py = 218442590671631;
    pz = 340432751592346;
    vpx = -33;
    vpy = -18;
    vpz = -33;
    
    
    eqs.push(x.add(t12.mul(vx)).eq(t12.mul(vpx).add(px)));
    eqs.push(y.add(t12.mul(vy)).eq(t12.mul(vpy).add(py)));
    eqs.push(z.add(t12.mul(vz)).eq(t12.mul(vpz).add(pz)));
    px = 274401356328157;
    py = 323394494374360;
    pz = 297096642831308;
    vpx = 16;
    vpy = 19;
    vpz = -7;
    
    
    eqs.push(x.add(t13.mul(vx)).eq(t13.mul(vpx).add(px)));
    eqs.push(y.add(t13.mul(vy)).eq(t13.mul(vpy).add(py)));
    eqs.push(z.add(t13.mul(vz)).eq(t13.mul(vpz).add(pz)));
    px = 304828109276462;
    py = 349810827812905;
    pz = 428798006192786;
    vpx = -39;
    vpy = -116;
    vpz = -241;
    
    
    eqs.push(x.add(t14.mul(vx)).eq(t14.mul(vpx).add(px)));
    eqs.push(y.add(t14.mul(vy)).eq(t14.mul(vpy).add(py)));
    eqs.push(z.add(t14.mul(vz)).eq(t14.mul(vpz).add(pz)));
    px = 303443040396668;
    py = 402514782738987;
    pz = 345785270737548;
    vpx = -183;
    vpy = 56;
    vpz = -407;
    
    
    eqs.push(x.add(t15.mul(vx)).eq(t15.mul(vpx).add(px)));
    eqs.push(y.add(t15.mul(vy)).eq(t15.mul(vpy).add(py)));
    eqs.push(z.add(t15.mul(vz)).eq(t15.mul(vpz).add(pz)));
    px = 323340955971369;
    py = 92034804687714;
    pz = 417353097216926;
    vpx = -25;
    vpy = 27;
    vpz = -86;
    
    
    eqs.push(x.add(t16.mul(vx)).eq(t16.mul(vpx).add(px)));
    eqs.push(y.add(t16.mul(vy)).eq(t16.mul(vpy).add(py)));
    eqs.push(z.add(t16.mul(vz)).eq(t16.mul(vpz).add(pz)));
    px = 307765512354748;
    py = 188583122359672;
    pz = 325523485683806;
    vpx = -21;
    vpy = 15;
    vpz = -13;
    
    
    eqs.push(x.add(t17.mul(vx)).eq(t17.mul(vpx).add(px)));
    eqs.push(y.add(t17.mul(vy)).eq(t17.mul(vpy).add(py)));
    eqs.push(z.add(t17.mul(vz)).eq(t17.mul(vpz).add(pz)));
    px = 263488210563664;
    py = 385897724824405;
    pz = 270935537020622;
    vpx = 85;
    vpy = 334;
    vpz = 71;
    
    
    eqs.push(x.add(t18.mul(vx)).eq(t18.mul(vpx).add(px)));
    eqs.push(y.add(t18.mul(vy)).eq(t18.mul(vpy).add(py)));
    eqs.push(z.add(t18.mul(vz)).eq(t18.mul(vpz).add(pz)));
    px = 210178816788935;
    py = 189082262652706;
    pz = 228983255761448;
    vpx = 108;
    vpy = 43;
    vpz = 113;
    
    
    eqs.push(x.add(t19.mul(vx)).eq(t19.mul(vpx).add(px)));
    eqs.push(y.add(t19.mul(vy)).eq(t19.mul(vpy).add(py)));
    eqs.push(z.add(t19.mul(vz)).eq(t19.mul(vpz).add(pz)));
    px = 283985882559237;
    py = 367640038537875;
    pz = 230423888034968;
    vpx = -48;
    vpy = 192;
    vpz = 285;
    
    
    eqs.push(x.add(t20.mul(vx)).eq(t20.mul(vpx).add(px)));
    eqs.push(y.add(t20.mul(vy)).eq(t20.mul(vpy).add(py)));
    eqs.push(z.add(t20.mul(vz)).eq(t20.mul(vpz).add(pz)));
    px = 333130789363343;
    py = 379047533938042;
    pz = 237713333264712;
    vpx = -180;
    vpy = -53;
    vpz = 169;
    
    
    eqs.push(x.add(t21.mul(vx)).eq(t21.mul(vpx).add(px)));
    eqs.push(y.add(t21.mul(vy)).eq(t21.mul(vpy).add(py)));
    eqs.push(z.add(t21.mul(vz)).eq(t21.mul(vpz).add(pz)));
    px = 289287446432941;
    py = 397451442710462;
    pz = 326233192718027;
    vpx = -120;
    vpy = 181;
    vpz = -358;
    
    
    eqs.push(x.add(t22.mul(vx)).eq(t22.mul(vpx).add(px)));
    eqs.push(y.add(t22.mul(vy)).eq(t22.mul(vpy).add(py)));
    eqs.push(z.add(t22.mul(vz)).eq(t22.mul(vpz).add(pz)));
    px = 265072410973990;
    py = 426345702753054;
    pz = 330651523533836;
    vpx = 67;
    vpy = -43;
    vpz = -391;
    
    
    eqs.push(x.add(t23.mul(vx)).eq(t23.mul(vpx).add(px)));
    eqs.push(y.add(t23.mul(vy)).eq(t23.mul(vpy).add(py)));
    eqs.push(z.add(t23.mul(vz)).eq(t23.mul(vpz).add(pz)));
    px = 357521545644523;
    py = 129199780517120;
    pz = 329831493509697;
    vpx = -86;
    vpy = 99;
    vpz = -20;
    
    
    eqs.push(x.add(t24.mul(vx)).eq(t24.mul(vpx).add(px)));
    eqs.push(y.add(t24.mul(vy)).eq(t24.mul(vpy).add(py)));
    eqs.push(z.add(t24.mul(vz)).eq(t24.mul(vpz).add(pz)));
    px = 283408270669227;
    py = 202525462999982;
    pz = 260893535402016;
    vpx = 11;
    vpy = -30;
    vpz = 67;
    
    
    eqs.push(x.add(t25.mul(vx)).eq(t25.mul(vpx).add(px)));
    eqs.push(y.add(t25.mul(vy)).eq(t25.mul(vpy).add(py)));
    eqs.push(z.add(t25.mul(vz)).eq(t25.mul(vpz).add(pz)));
    px = 360621125237679;
    py = 176142496411170;
    pz = 311032962569312;
    vpx = -145;
    vpy = 214;
    vpz = -19;
    
    
    eqs.push(x.add(t26.mul(vx)).eq(t26.mul(vpx).add(px)));
    eqs.push(y.add(t26.mul(vy)).eq(t26.mul(vpy).add(py)));
    eqs.push(z.add(t26.mul(vz)).eq(t26.mul(vpz).add(pz)));
    px = 330191571870402;
    py = 459937341246504;
    pz = 289198161226967;
    vpx = -259;
    vpy = -313;
    vpz = -24;
    
    
    eqs.push(x.add(t27.mul(vx)).eq(t27.mul(vpx).add(px)));
    eqs.push(y.add(t27.mul(vy)).eq(t27.mul(vpy).add(py)));
    eqs.push(z.add(t27.mul(vz)).eq(t27.mul(vpz).add(pz)));
    px = 279219984868398;
    py = 482578947238962;
    pz = 271832563687538;
    vpx = -47;
    vpy = -487;
    vpz = 63;
    
    
    eqs.push(x.add(t28.mul(vx)).eq(t28.mul(vpx).add(px)));
    eqs.push(y.add(t28.mul(vy)).eq(t28.mul(vpy).add(py)));
    eqs.push(z.add(t28.mul(vz)).eq(t28.mul(vpz).add(pz)));
    px = 268772677767959;
    py = 372556851973094;
    pz = 290625485800272;
    vpx = 33;
    vpy = 63;
    vpz = -23;
    
    
    eqs.push(x.add(t29.mul(vx)).eq(t29.mul(vpx).add(px)));
    eqs.push(y.add(t29.mul(vy)).eq(t29.mul(vpy).add(py)));
    eqs.push(z.add(t29.mul(vz)).eq(t29.mul(vpz).add(pz)));
    px = 276393131794075;
    py = 291938143229626;
    pz = 238911680329090;
    vpx = 10;
    vpy = 127;
    vpz = 144;
    
    
    eqs.push(x.add(t30.mul(vx)).eq(t30.mul(vpx).add(px)));
    eqs.push(y.add(t30.mul(vy)).eq(t30.mul(vpy).add(py)));
    eqs.push(z.add(t30.mul(vz)).eq(t30.mul(vpz).add(pz)));
    px = 235700158714295;
    py = 318767843977690;
    pz = 173717989251612;
    vpx = 99;
    vpy = -26;
    vpz = 262;
    
    
    eqs.push(x.add(t31.mul(vx)).eq(t31.mul(vpx).add(px)));
    eqs.push(y.add(t31.mul(vy)).eq(t31.mul(vpy).add(py)));
    eqs.push(z.add(t31.mul(vz)).eq(t31.mul(vpz).add(pz)));
    px = 307035460762787;
    py = 433352602775398;
    pz = 329838863767902;
    vpx = -114;
    vpy = -215;
    vpz = -164;
    
    
    eqs.push(x.add(t32.mul(vx)).eq(t32.mul(vpx).add(px)));
    eqs.push(y.add(t32.mul(vy)).eq(t32.mul(vpy).add(py)));
    eqs.push(z.add(t32.mul(vz)).eq(t32.mul(vpz).add(pz)));
    px = 483366892313104;
    py = 262936260613156;
    pz = 342469711655622;
    vpx = -201;
    vpy = -117;
    vpz = -21;
    
    
    eqs.push(x.add(t33.mul(vx)).eq(t33.mul(vpx).add(px)));
    eqs.push(y.add(t33.mul(vy)).eq(t33.mul(vpy).add(py)));
    eqs.push(z.add(t33.mul(vz)).eq(t33.mul(vpz).add(pz)));
    px = 252037178725326;
    py = 239083355734533;
    pz = 100854044768291;
    vpx = 47;
    vpy = -74;
    vpz = 250;
    
    
    eqs.push(x.add(t34.mul(vx)).eq(t34.mul(vpx).add(px)));
    eqs.push(y.add(t34.mul(vy)).eq(t34.mul(vpy).add(py)));
    eqs.push(z.add(t34.mul(vz)).eq(t34.mul(vpz).add(pz)));
    px = 338759779357023;
    py = 411820696207434;
    pz = 365708713895558;
    vpx = -306;
    vpy = -79;
    vpz = -397;
    
    
    eqs.push(x.add(t35.mul(vx)).eq(t35.mul(vpx).add(px)));
    eqs.push(y.add(t35.mul(vy)).eq(t35.mul(vpy).add(py)));
    eqs.push(z.add(t35.mul(vz)).eq(t35.mul(vpz).add(pz)));
    px = 275725852568965;
    py = 437253800744482;
    pz = 228918187676310;
    vpx = -51;
    vpy = 51;
    vpz = 690;
    
    
    eqs.push(x.add(t36.mul(vx)).eq(t36.mul(vpx).add(px)));
    eqs.push(y.add(t36.mul(vy)).eq(t36.mul(vpy).add(py)));
    eqs.push(z.add(t36.mul(vz)).eq(t36.mul(vpz).add(pz)));
    px = 218291728169979;
    py = 225148716056766;
    pz = 301148692245056;
    vpx = 102;
    vpy = 17;
    vpz = 12;
    
    
    eqs.push(x.add(t37.mul(vx)).eq(t37.mul(vpx).add(px)));
    eqs.push(y.add(t37.mul(vy)).eq(t37.mul(vpy).add(py)));
    eqs.push(z.add(t37.mul(vz)).eq(t37.mul(vpz).add(pz)));
    px = 335796419585965;
    py = 273216483788310;
    pz = 218432517319212;
    vpx = -180;
    vpy = 269;
    vpz = 225;
    
    
    eqs.push(x.add(t38.mul(vx)).eq(t38.mul(vpx).add(px)));
    eqs.push(y.add(t38.mul(vy)).eq(t38.mul(vpy).add(py)));
    eqs.push(z.add(t38.mul(vz)).eq(t38.mul(vpz).add(pz)));
    px = 288650438469807;
    py = 393217145633735;
    pz = 393241761060833;
    vpx = -10;
    vpy = -192;
    vpz = -184;
    
    
    eqs.push(x.add(t39.mul(vx)).eq(t39.mul(vpx).add(px)));
    eqs.push(y.add(t39.mul(vy)).eq(t39.mul(vpy).add(py)));
    eqs.push(z.add(t39.mul(vz)).eq(t39.mul(vpz).add(pz)));
    px = 297535201134031;
    py = 320994614809658;
    pz = 200806502447378;
    vpx = -36;
    vpy = -5;
    vpz = 218;
    
    
    eqs.push(x.add(t40.mul(vx)).eq(t40.mul(vpx).add(px)));
    eqs.push(y.add(t40.mul(vy)).eq(t40.mul(vpy).add(py)));
    eqs.push(z.add(t40.mul(vz)).eq(t40.mul(vpz).add(pz)));
    px = 305894885039157;
    py = 266792713041662;
    pz = 262627732020492;
    vpx = -49;
    vpy = 85;
    vpz = 75;
    
    
    eqs.push(x.add(t41.mul(vx)).eq(t41.mul(vpx).add(px)));
    eqs.push(y.add(t41.mul(vy)).eq(t41.mul(vpy).add(py)));
    eqs.push(z.add(t41.mul(vz)).eq(t41.mul(vpz).add(pz)));
    px = 354668455172970;
    py = 352774244046983;
    pz = 536345552823415;
    vpx = -151;
    vpy = -98;
    vpz = -500;
    
    
    eqs.push(x.add(t42.mul(vx)).eq(t42.mul(vpx).add(px)));
    eqs.push(y.add(t42.mul(vy)).eq(t42.mul(vpy).add(py)));
    eqs.push(z.add(t42.mul(vz)).eq(t42.mul(vpz).add(pz)));
    px = 365871847999148;
    py = 287112731527968;
    pz = 359906767568725;
    vpx = -107;
    vpy = -85;
    vpz = -68;
    
    
    eqs.push(x.add(t43.mul(vx)).eq(t43.mul(vpx).add(px)));
    eqs.push(y.add(t43.mul(vy)).eq(t43.mul(vpy).add(py)));
    eqs.push(z.add(t43.mul(vz)).eq(t43.mul(vpz).add(pz)));
    px = 188863864270103;
    py = 133490031564998;
    pz = 361421327952572;
    vpx = 145;
    vpy = 151;
    vpz = -76;
    
    
    eqs.push(x.add(t44.mul(vx)).eq(t44.mul(vpx).add(px)));
    eqs.push(y.add(t44.mul(vy)).eq(t44.mul(vpy).add(py)));
    eqs.push(z.add(t44.mul(vz)).eq(t44.mul(vpz).add(pz)));
    px = 266041565973615;
    py = 80493722144573;
    pz = 323436962795307;
    vpx = 38;
    vpy = 726;
    vpz = -86;
    
    
    eqs.push(x.add(t45.mul(vx)).eq(t45.mul(vpx).add(px)));
    eqs.push(y.add(t45.mul(vy)).eq(t45.mul(vpy).add(py)));
    eqs.push(z.add(t45.mul(vz)).eq(t45.mul(vpz).add(pz)));
    px = 210524009414594;
    py = 307434778066041;
    pz = 336020097277997;
    vpx = 103;
    vpy = -130;
    vpz = -28;
    
    
    eqs.push(x.add(t46.mul(vx)).eq(t46.mul(vpx).add(px)));
    eqs.push(y.add(t46.mul(vy)).eq(t46.mul(vpy).add(py)));
    eqs.push(z.add(t46.mul(vz)).eq(t46.mul(vpz).add(pz)));
    px = 387419474737982;
    py = 246377818528285;
    pz = 469298726964458;
    vpx = -135;
    vpy = -32;
    vpz = -217;
    
    
    eqs.push(x.add(t47.mul(vx)).eq(t47.mul(vpx).add(px)));
    eqs.push(y.add(t47.mul(vy)).eq(t47.mul(vpy).add(py)));
    eqs.push(z.add(t47.mul(vz)).eq(t47.mul(vpz).add(pz)));
    px = 286379423522892;
    py = 415752542225355;
    pz = 261516190255763;
    vpx = -189;
    vpy = 314;
    vpz = 208;
    
    
    eqs.push(x.add(t48.mul(vx)).eq(t48.mul(vpx).add(px)));
    eqs.push(y.add(t48.mul(vy)).eq(t48.mul(vpy).add(py)));
    eqs.push(z.add(t48.mul(vz)).eq(t48.mul(vpz).add(pz)));
    px = 358423439654491;
    py = 474986432063286;
    pz = 379323436257296;
    vpx = -138;
    vpy = -352;
    vpz = -145;
    
    
    eqs.push(x.add(t49.mul(vx)).eq(t49.mul(vpx).add(px)));
    eqs.push(y.add(t49.mul(vy)).eq(t49.mul(vpy).add(py)));
    eqs.push(z.add(t49.mul(vz)).eq(t49.mul(vpz).add(pz)));
    px = 316468823323255;
    py = 178336491882174;
    pz = 353304310212440;
    vpx = -36;
    vpy = 53;
    vpz = -55;
    
    
    eqs.push(x.add(t50.mul(vx)).eq(t50.mul(vpx).add(px)));
    eqs.push(y.add(t50.mul(vy)).eq(t50.mul(vpy).add(py)));
    eqs.push(z.add(t50.mul(vz)).eq(t50.mul(vpz).add(pz)));
    px = 370513619404125;
    py = 438286486099934;
    pz = 516988421715709;
    vpx = -100;
    vpy = -299;
    vpz = -254;
    
    
    eqs.push(x.add(t51.mul(vx)).eq(t51.mul(vpx).add(px)));
    eqs.push(y.add(t51.mul(vy)).eq(t51.mul(vpy).add(py)));
    eqs.push(z.add(t51.mul(vz)).eq(t51.mul(vpz).add(pz)));
    px = 375291925637577;
    py = 465656729270115;
    pz = 409022941382558;
    vpx = -244;
    vpy = -336;
    vpz = -297;
    
    
    eqs.push(x.add(t52.mul(vx)).eq(t52.mul(vpx).add(px)));
    eqs.push(y.add(t52.mul(vy)).eq(t52.mul(vpy).add(py)));
    eqs.push(z.add(t52.mul(vz)).eq(t52.mul(vpz).add(pz)));
    px = 139537859245179;
    py = 292990088786943;
    pz = 222949159733159;
    vpx = 154;
    vpy = -164;
    vpz = 102;
    
    
    eqs.push(x.add(t53.mul(vx)).eq(t53.mul(vpx).add(px)));
    eqs.push(y.add(t53.mul(vy)).eq(t53.mul(vpy).add(py)));
    eqs.push(z.add(t53.mul(vz)).eq(t53.mul(vpz).add(pz)));
    px = 281771608749457;
    py = 286998983543310;
    pz = 331946898945808;
    vpx = 9;
    vpy = -67;
    vpz = -35;
    
    
    eqs.push(x.add(t54.mul(vx)).eq(t54.mul(vpx).add(px)));
    eqs.push(y.add(t54.mul(vy)).eq(t54.mul(vpy).add(py)));
    eqs.push(z.add(t54.mul(vz)).eq(t54.mul(vpz).add(pz)));
    px = 324649828198072;
    py = 422398718458555;
    pz = 467174560000358;
    vpx = -83;
    vpy = -248;
    vpz = -337;
    
    
    eqs.push(x.add(t55.mul(vx)).eq(t55.mul(vpx).add(px)));
    eqs.push(y.add(t55.mul(vy)).eq(t55.mul(vpy).add(py)));
    eqs.push(z.add(t55.mul(vz)).eq(t55.mul(vpz).add(pz)));
    px = 233274360798549;
    py = 207145055922274;
    pz = 267181130893562;
    vpx = 83;
    vpy = 63;
    vpz = 62;
    
    
    eqs.push(x.add(t56.mul(vx)).eq(t56.mul(vpx).add(px)));
    eqs.push(y.add(t56.mul(vy)).eq(t56.mul(vpy).add(py)));
    eqs.push(z.add(t56.mul(vz)).eq(t56.mul(vpz).add(pz)));
    px = 304178874538143;
    py = 53305704988308;
    pz = 529422903687140;
    vpx = -8;
    vpy = 82;
    vpz = -205;
    
    
    eqs.push(x.add(t57.mul(vx)).eq(t57.mul(vpx).add(px)));
    eqs.push(y.add(t57.mul(vy)).eq(t57.mul(vpy).add(py)));
    eqs.push(z.add(t57.mul(vz)).eq(t57.mul(vpz).add(pz)));
    px = 316304122802127;
    py = 392295632220390;
    pz = 357213661388378;
    vpx = -64;
    vpy = -191;
    vpz = -112;
    
    
    eqs.push(x.add(t58.mul(vx)).eq(t58.mul(vpx).add(px)));
    eqs.push(y.add(t58.mul(vy)).eq(t58.mul(vpy).add(py)));
    eqs.push(z.add(t58.mul(vz)).eq(t58.mul(vpz).add(pz)));
    px = 319638806555470;
    py = 420539055708926;
    pz = 216374545050404;
    vpx = -47;
    vpy = -267;
    vpz = 137;
    
    
    eqs.push(x.add(t59.mul(vx)).eq(t59.mul(vpx).add(px)));
    eqs.push(y.add(t59.mul(vy)).eq(t59.mul(vpy).add(py)));
    eqs.push(z.add(t59.mul(vz)).eq(t59.mul(vpz).add(pz)));
    px = 247237743462387;
    py = 360290797877334;
    pz = 387013342411292;
    vpx = 116;
    vpy = 71;
    vpz = -390;
    
    
    eqs.push(x.add(t60.mul(vx)).eq(t60.mul(vpx).add(px)));
    eqs.push(y.add(t60.mul(vy)).eq(t60.mul(vpy).add(py)));
    eqs.push(z.add(t60.mul(vz)).eq(t60.mul(vpz).add(pz)));
    px = 306702826165702;
    py = 106832790607142;
    pz = 342550713958507;
    vpx = -9;
    vpy = 13;
    vpz = -14;
    
    
    eqs.push(x.add(t61.mul(vx)).eq(t61.mul(vpx).add(px)));
    eqs.push(y.add(t61.mul(vy)).eq(t61.mul(vpy).add(py)));
    eqs.push(z.add(t61.mul(vz)).eq(t61.mul(vpz).add(pz)));
    px = 261417334297627;
    py = 325052103502854;
    pz = 344840959947648;
    vpx = 46;
    vpy = -22;
    vpz = -107;
    
    
    eqs.push(x.add(t62.mul(vx)).eq(t62.mul(vpx).add(px)));
    eqs.push(y.add(t62.mul(vy)).eq(t62.mul(vpy).add(py)));
    eqs.push(z.add(t62.mul(vz)).eq(t62.mul(vpz).add(pz)));
    px = 301336648580432;
    py = 378307529064045;
    pz = 144808148666922;
    vpx = -99;
    vpy = 14;
    vpz = 571;
    
    
    eqs.push(x.add(t63.mul(vx)).eq(t63.mul(vpx).add(px)));
    eqs.push(y.add(t63.mul(vy)).eq(t63.mul(vpy).add(py)));
    eqs.push(z.add(t63.mul(vz)).eq(t63.mul(vpz).add(pz)));
    px = 269012554705770;
    py = 387372467070396;
    pz = 393532923667106;
    vpx = 29;
    vpy = -165;
    vpz = -209;
    
    
    eqs.push(x.add(t64.mul(vx)).eq(t64.mul(vpx).add(px)));
    eqs.push(y.add(t64.mul(vy)).eq(t64.mul(vpy).add(py)));
    eqs.push(z.add(t64.mul(vz)).eq(t64.mul(vpz).add(pz)));
    px = 269312570033932;
    py = 434661648029110;
    pz = 307394457405958;
    vpx = 37;
    vpy = -35;
    vpz = -297;
    
    
    eqs.push(x.add(t65.mul(vx)).eq(t65.mul(vpx).add(px)));
    eqs.push(y.add(t65.mul(vy)).eq(t65.mul(vpy).add(py)));
    eqs.push(z.add(t65.mul(vz)).eq(t65.mul(vpz).add(pz)));
    px = 268744271151861;
    py = 289031189760834;
    pz = 291169322258114;
    vpx = 29;
    vpy = -13;
    vpz = 20;
    
    
    eqs.push(x.add(t66.mul(vx)).eq(t66.mul(vpx).add(px)));
    eqs.push(y.add(t66.mul(vy)).eq(t66.mul(vpy).add(py)));
    eqs.push(z.add(t66.mul(vz)).eq(t66.mul(vpz).add(pz)));
    px = 256196973903807;
    py = 290532096714210;
    pz = 200646072951758;
    vpx = 76;
    vpy = 279;
    vpz = 308;
    
    
    eqs.push(x.add(t67.mul(vx)).eq(t67.mul(vpx).add(px)));
    eqs.push(y.add(t67.mul(vy)).eq(t67.mul(vpy).add(py)));
    eqs.push(z.add(t67.mul(vz)).eq(t67.mul(vpz).add(pz)));
    px = 273118846488495;
    py = 445371405950118;
    pz = 389543008692968;
    vpx = 15;
    vpy = -257;
    vpz = -417;
    
    
    eqs.push(x.add(t68.mul(vx)).eq(t68.mul(vpx).add(px)));
    eqs.push(y.add(t68.mul(vy)).eq(t68.mul(vpy).add(py)));
    eqs.push(z.add(t68.mul(vz)).eq(t68.mul(vpz).add(pz)));
    px = 231693759411627;
    py = 45770729679966;
    pz = 206286995452310;
    vpx = 66;
    vpy = 101;
    vpz = 122;
    
    
    eqs.push(x.add(t69.mul(vx)).eq(t69.mul(vpx).add(px)));
    eqs.push(y.add(t69.mul(vy)).eq(t69.mul(vpy).add(py)));
    eqs.push(z.add(t69.mul(vz)).eq(t69.mul(vpz).add(pz)));
    px = 397593077056783;
    py = 303468227079126;
    pz = 340489985475012;
    vpx = -255;
    vpy = 23;
    vpz = -96;
    
    
    eqs.push(x.add(t70.mul(vx)).eq(t70.mul(vpx).add(px)));
    eqs.push(y.add(t70.mul(vy)).eq(t70.mul(vpy).add(py)));
    eqs.push(z.add(t70.mul(vz)).eq(t70.mul(vpz).add(pz)));
    px = 147291213144669;
    py = 127398963485282;
    pz = 289938063174374;
    vpx = 179;
    vpy = 87;
    vpz = 32;
    
    
    eqs.push(x.add(t71.mul(vx)).eq(t71.mul(vpx).add(px)));
    eqs.push(y.add(t71.mul(vy)).eq(t71.mul(vpy).add(py)));
    eqs.push(z.add(t71.mul(vz)).eq(t71.mul(vpz).add(pz)));
    px = 279062146022054;
    py = 218288644051118;
    pz = 283712519894512;
    vpx = 13;
    vpy = 37;
    vpz = 37;
    
    
    eqs.push(x.add(t72.mul(vx)).eq(t72.mul(vpx).add(px)));
    eqs.push(y.add(t72.mul(vy)).eq(t72.mul(vpy).add(py)));
    eqs.push(z.add(t72.mul(vz)).eq(t72.mul(vpz).add(pz)));
    px = 281974048517427;
    py = 162586692606990;
    pz = 317438841834668;
    vpx = 14;
    vpy = -19;
    vpz = 7;
    
    
    eqs.push(x.add(t73.mul(vx)).eq(t73.mul(vpx).add(px)));
    eqs.push(y.add(t73.mul(vy)).eq(t73.mul(vpy).add(py)));
    eqs.push(z.add(t73.mul(vz)).eq(t73.mul(vpz).add(pz)));
    px = 315097282844553;
    py = 236030235469392;
    pz = 104618134238444;
    vpx = -17;
    vpy = -112;
    vpz = 215;
    
    
    eqs.push(x.add(t74.mul(vx)).eq(t74.mul(vpx).add(px)));
    eqs.push(y.add(t74.mul(vy)).eq(t74.mul(vpy).add(py)));
    eqs.push(z.add(t74.mul(vz)).eq(t74.mul(vpz).add(pz)));
    px = 231684036933203;
    py = 310263831029412;
    pz = 364282571619596;
    vpx = 82;
    vpy = -109;
    vpz = -79;
    
    
    eqs.push(x.add(t75.mul(vx)).eq(t75.mul(vpx).add(px)));
    eqs.push(y.add(t75.mul(vy)).eq(t75.mul(vpy).add(py)));
    eqs.push(z.add(t75.mul(vz)).eq(t75.mul(vpz).add(pz)));
    px = 273377967027768;
    py = 236797636615074;
    pz = 204369745689605;
    vpx = 23;
    vpy = -103;
    vpz = 122;
    
    
    eqs.push(x.add(t76.mul(vx)).eq(t76.mul(vpx).add(px)));
    eqs.push(y.add(t76.mul(vy)).eq(t76.mul(vpy).add(py)));
    eqs.push(z.add(t76.mul(vz)).eq(t76.mul(vpz).add(pz)));
    px = 265666680959117;
    py = 435600154727410;
    pz = 232785008689678;
    vpx = 105;
    vpy = 139;
    vpz = 726;
    
    
    eqs.push(x.add(t77.mul(vx)).eq(t77.mul(vpx).add(px)));
    eqs.push(y.add(t77.mul(vy)).eq(t77.mul(vpy).add(py)));
    eqs.push(z.add(t77.mul(vz)).eq(t77.mul(vpz).add(pz)));
    px = 98536893585797;
    py = 312295662294412;
    pz = 62170711477966;
    vpx = 211;
    vpy = -168;
    vpz = 280;
    
    
    eqs.push(x.add(t78.mul(vx)).eq(t78.mul(vpx).add(px)));
    eqs.push(y.add(t78.mul(vy)).eq(t78.mul(vpy).add(py)));
    eqs.push(z.add(t78.mul(vz)).eq(t78.mul(vpz).add(pz)));
    px = 286415700563907;
    py = 459868507706766;
    pz = 268341626133232;
    vpx = -49;
    vpy = -313;
    vpz = 75;
    
    
    eqs.push(x.add(t79.mul(vx)).eq(t79.mul(vpx).add(px)));
    eqs.push(y.add(t79.mul(vy)).eq(t79.mul(vpy).add(py)));
    eqs.push(z.add(t79.mul(vz)).eq(t79.mul(vpz).add(pz)));
    px = 249907840686301;
    py = 301499975324576;
    pz = 422522477648468;
    vpx = 63;
    vpy = -38;
    vpz = -217;
    
    
    eqs.push(x.add(t80.mul(vx)).eq(t80.mul(vpx).add(px)));
    eqs.push(y.add(t80.mul(vy)).eq(t80.mul(vpy).add(py)));
    eqs.push(z.add(t80.mul(vz)).eq(t80.mul(vpz).add(pz)));
    px = 332999276737947;
    py = 434926077550905;
    pz = 317481674006573;
    vpx = -198;
    vpy = -228;
    vpz = -106;
    
    
    eqs.push(x.add(t81.mul(vx)).eq(t81.mul(vpx).add(px)));
    eqs.push(y.add(t81.mul(vy)).eq(t81.mul(vpy).add(py)));
    eqs.push(z.add(t81.mul(vz)).eq(t81.mul(vpz).add(pz)));
    px = 265638990566034;
    py = 251855758509942;
    pz = 298845110741690;
    vpx = 33;
    vpy = -19;
    vpz = 15;
    
    
    eqs.push(x.add(t82.mul(vx)).eq(t82.mul(vpx).add(px)));
    eqs.push(y.add(t82.mul(vy)).eq(t82.mul(vpy).add(py)));
    eqs.push(z.add(t82.mul(vz)).eq(t82.mul(vpz).add(pz)));
    px = 330149687686095;
    py = 254832195425806;
    pz = 276810334792564;
    vpx = -85;
    vpy = 57;
    vpz = 46;
    
    
    eqs.push(x.add(t83.mul(vx)).eq(t83.mul(vpx).add(px)));
    eqs.push(y.add(t83.mul(vy)).eq(t83.mul(vpy).add(py)));
    eqs.push(z.add(t83.mul(vz)).eq(t83.mul(vpz).add(pz)));
    px = 271216279199148;
    py = 299452379469804;
    pz = 279084920945042;
    vpx = 23;
    vpy = 267;
    vpz = 31;
    
    
    eqs.push(x.add(t84.mul(vx)).eq(t84.mul(vpx).add(px)));
    eqs.push(y.add(t84.mul(vy)).eq(t84.mul(vpy).add(py)));
    eqs.push(z.add(t84.mul(vz)).eq(t84.mul(vpz).add(pz)));
    px = 330849958763937;
    py = 301123922204940;
    pz = 203779586283428;
    vpx = -77;
    vpy = -54;
    vpz = 171;
    
    
    eqs.push(x.add(t85.mul(vx)).eq(t85.mul(vpx).add(px)));
    eqs.push(y.add(t85.mul(vy)).eq(t85.mul(vpy).add(py)));
    eqs.push(z.add(t85.mul(vz)).eq(t85.mul(vpz).add(pz)));
    px = 277661292234039;
    py = 274718355975078;
    pz = 308175678115746;
    vpx = 14;
    vpy = -19;
    vpz = -5;
    
    
    eqs.push(x.add(t86.mul(vx)).eq(t86.mul(vpx).add(px)));
    eqs.push(y.add(t86.mul(vy)).eq(t86.mul(vpy).add(py)));
    eqs.push(z.add(t86.mul(vz)).eq(t86.mul(vpz).add(pz)));
    px = 308881913543876;
    py = 406703097591989;
    pz = 328605909836864;
    vpx = -107;
    vpy = -134;
    vpz = -139;
    
    
    eqs.push(x.add(t87.mul(vx)).eq(t87.mul(vpx).add(px)));
    eqs.push(y.add(t87.mul(vy)).eq(t87.mul(vpy).add(py)));
    eqs.push(z.add(t87.mul(vz)).eq(t87.mul(vpz).add(pz)));
    px = 244806518069345;
    py = 323928824537342;
    pz = 355727357622573;
    vpx = 108;
    vpy = 117;
    vpz = -212;
    
    
    eqs.push(x.add(t88.mul(vx)).eq(t88.mul(vpx).add(px)));
    eqs.push(y.add(t88.mul(vy)).eq(t88.mul(vpy).add(py)));
    eqs.push(z.add(t88.mul(vz)).eq(t88.mul(vpz).add(pz)));
    px = 282765808815827;
    py = 428682433212430;
    pz = 331695854219608;
    vpx = -51;
    vpy = -113;
    vpz = -312;
    
    
    eqs.push(x.add(t89.mul(vx)).eq(t89.mul(vpx).add(px)));
    eqs.push(y.add(t89.mul(vy)).eq(t89.mul(vpy).add(py)));
    eqs.push(z.add(t89.mul(vz)).eq(t89.mul(vpz).add(pz)));
    px = 114042058484541;
    py = 57585054933291;
    pz = 155461437387323;
    vpx = 272;
    vpy = 308;
    vpz = 238;
    
    
    eqs.push(x.add(t90.mul(vx)).eq(t90.mul(vpx).add(px)));
    eqs.push(y.add(t90.mul(vy)).eq(t90.mul(vpy).add(py)));
    eqs.push(z.add(t90.mul(vz)).eq(t90.mul(vpz).add(pz)));
    px = 316947363623629;
    py = 366249784163292;
    pz = 234525003541438;
    vpx = -113;
    vpy = -40;
    vpz = 168;
    
    
    eqs.push(x.add(t91.mul(vx)).eq(t91.mul(vpx).add(px)));
    eqs.push(y.add(t91.mul(vy)).eq(t91.mul(vpy).add(py)));
    eqs.push(z.add(t91.mul(vz)).eq(t91.mul(vpz).add(pz)));
    px = 257454091974513;
    py = 358306423318053;
    pz = 272661312781067;
    vpx = 60;
    vpy = -54;
    vpz = 54;
    
    
    eqs.push(x.add(t92.mul(vx)).eq(t92.mul(vpx).add(px)));
    eqs.push(y.add(t92.mul(vy)).eq(t92.mul(vpy).add(py)));
    eqs.push(z.add(t92.mul(vz)).eq(t92.mul(vpz).add(pz)));
    px = 327941728613805;
    py = 516313152213920;
    pz = 403920559229147;
    vpx = -160;
    vpy = -501;
    vpz = -370;
    
    
    eqs.push(x.add(t93.mul(vx)).eq(t93.mul(vpx).add(px)));
    eqs.push(y.add(t93.mul(vy)).eq(t93.mul(vpy).add(py)));
    eqs.push(z.add(t93.mul(vz)).eq(t93.mul(vpz).add(pz)));
    px = 266268656989236;
    py = 320340905431026;
    pz = 161388351945824;
    vpx = 39;
    vpy = 121;
    vpz = 405;
    
    
    eqs.push(x.add(t94.mul(vx)).eq(t94.mul(vpx).add(px)));
    eqs.push(y.add(t94.mul(vy)).eq(t94.mul(vpy).add(py)));
    eqs.push(z.add(t94.mul(vz)).eq(t94.mul(vpz).add(pz)));
    px = 334169171100818;
    py = 344369161102431;
    pz = 299562952971470;
    vpx = -75;
    vpy = -142;
    vpz = 11;
    
    
    eqs.push(x.add(t95.mul(vx)).eq(t95.mul(vpx).add(px)));
    eqs.push(y.add(t95.mul(vy)).eq(t95.mul(vpy).add(py)));
    eqs.push(z.add(t95.mul(vz)).eq(t95.mul(vpz).add(pz)));
    px = 439234520585447;
    py = 423874948507650;
    pz = 301498412981108;
    vpx = -152;
    vpy = -289;
    vpz = 23;
    
    
    eqs.push(x.add(t96.mul(vx)).eq(t96.mul(vpx).add(px)));
    eqs.push(y.add(t96.mul(vy)).eq(t96.mul(vpy).add(py)));
    eqs.push(z.add(t96.mul(vz)).eq(t96.mul(vpz).add(pz)));
    px = 318895708853607;
    py = 486025745441448;
    pz = 536900806204640;
    vpx = -74;
    vpy = -377;
    vpz = -491;
    
    
    eqs.push(x.add(t97.mul(vx)).eq(t97.mul(vpx).add(px)));
    eqs.push(y.add(t97.mul(vy)).eq(t97.mul(vpy).add(py)));
    eqs.push(z.add(t97.mul(vz)).eq(t97.mul(vpz).add(pz)));
    px = 277309303017633;
    py = 342141230045350;
    pz = 269059285146990;
    vpx = -7;
    vpy = 249;
    vpz = 72;
    
    
    eqs.push(x.add(t98.mul(vx)).eq(t98.mul(vpx).add(px)));
    eqs.push(y.add(t98.mul(vy)).eq(t98.mul(vpy).add(py)));
    eqs.push(z.add(t98.mul(vz)).eq(t98.mul(vpz).add(pz)));
    px = 307111474143542;
    py = 146142245024510;
    pz = 344495522925368;
    vpx = -11;
    vpy = -11;
    vpz = -19;
    
    
    eqs.push(x.add(t99.mul(vx)).eq(t99.mul(vpx).add(px)));
    eqs.push(y.add(t99.mul(vy)).eq(t99.mul(vpy).add(py)));
    eqs.push(z.add(t99.mul(vz)).eq(t99.mul(vpz).add(pz)));
    px = 292035489628817;
    py = 378205500734800;
    pz = 312425494203218;
    vpx = -35;
    vpy = -90;
    vpz = -58;
    
    
    eqs.push(x.add(t100.mul(vx)).eq(t100.mul(vpx).add(px)));
    eqs.push(y.add(t100.mul(vy)).eq(t100.mul(vpy).add(py)));
    eqs.push(z.add(t100.mul(vz)).eq(t100.mul(vpz).add(pz)));
    px = 288046802811951;
    py = 481903708723622;
    pz = 335902848039198;
    vpx = -40;
    vpy = -399;
    vpz = -182;
    
    
    eqs.push(x.add(t101.mul(vx)).eq(t101.mul(vpx).add(px)));
    eqs.push(y.add(t101.mul(vy)).eq(t101.mul(vpy).add(py)));
    eqs.push(z.add(t101.mul(vz)).eq(t101.mul(vpz).add(pz)));
    px = 299077518805092;
    py = 451002619191319;
    pz = 299364822899846;
    vpx = -229;
    vpy = -218;
    vpz = -181;
    
    
    eqs.push(x.add(t102.mul(vx)).eq(t102.mul(vpx).add(px)));
    eqs.push(y.add(t102.mul(vy)).eq(t102.mul(vpy).add(py)));
    eqs.push(z.add(t102.mul(vz)).eq(t102.mul(vpz).add(pz)));
    px = 338578952775771;
    py = 260371574631762;
    pz = 259648024246724;
    vpx = -142;
    vpy = 170;
    vpz = 86;
    
    
    eqs.push(x.add(t103.mul(vx)).eq(t103.mul(vpx).add(px)));
    eqs.push(y.add(t103.mul(vy)).eq(t103.mul(vpy).add(py)));
    eqs.push(z.add(t103.mul(vz)).eq(t103.mul(vpz).add(pz)));
    px = 180222081436251;
    py = 287435576112478;
    pz = 242578960218608;
    vpx = 248;
    vpy = 103;
    vpz = 128;
    
    
    eqs.push(x.add(t104.mul(vx)).eq(t104.mul(vpx).add(px)));
    eqs.push(y.add(t104.mul(vy)).eq(t104.mul(vpy).add(py)));
    eqs.push(z.add(t104.mul(vz)).eq(t104.mul(vpz).add(pz)));
    px = 362547459087383;
    py = 295292504802178;
    pz = 497868843146721;
    vpx = -90;
    vpy = -119;
    vpz = -230;
    
    
    eqs.push(x.add(t105.mul(vx)).eq(t105.mul(vpx).add(px)));
    eqs.push(y.add(t105.mul(vy)).eq(t105.mul(vpy).add(py)));
    eqs.push(z.add(t105.mul(vz)).eq(t105.mul(vpz).add(pz)));
    px = 288808115934893;
    py = 346012569018756;
    pz = 280648410315037;
    vpx = -20;
    vpy = -37;
    vpz = 34;
    
    
    eqs.push(x.add(t106.mul(vx)).eq(t106.mul(vpx).add(px)));
    eqs.push(y.add(t106.mul(vy)).eq(t106.mul(vpy).add(py)));
    eqs.push(z.add(t106.mul(vz)).eq(t106.mul(vpz).add(pz)));
    px = 272807874105531;
    py = 390439408169982;
    pz = 264788373273776;
    vpx = 14;
    vpy = 33;
    vpz = 94;
    
    
    eqs.push(x.add(t107.mul(vx)).eq(t107.mul(vpx).add(px)));
    eqs.push(y.add(t107.mul(vy)).eq(t107.mul(vpy).add(py)));
    eqs.push(z.add(t107.mul(vz)).eq(t107.mul(vpz).add(pz)));
    px = 302511531241630;
    py = 184207826179129;
    pz = 224521189736869;
    vpx = -21;
    vpy = 78;
    vpz = 124;
    
    
    eqs.push(x.add(t108.mul(vx)).eq(t108.mul(vpx).add(px)));
    eqs.push(y.add(t108.mul(vy)).eq(t108.mul(vpy).add(py)));
    eqs.push(z.add(t108.mul(vz)).eq(t108.mul(vpz).add(pz)));
    px = 225296060369532;
    py = 273107692555221;
    pz = 308517494417711;
    vpx = 101;
    vpy = -14;
    vpz = -6;
    
    
    eqs.push(x.add(t109.mul(vx)).eq(t109.mul(vpx).add(px)));
    eqs.push(y.add(t109.mul(vy)).eq(t109.mul(vpy).add(py)));
    eqs.push(z.add(t109.mul(vz)).eq(t109.mul(vpz).add(pz)));
    px = 271285620465063;
    py = 104568575628198;
    pz = 270361655266940;
    vpx = 25;
    vpy = 71;
    vpz = 56;
    
    
    eqs.push(x.add(t110.mul(vx)).eq(t110.mul(vpx).add(px)));
    eqs.push(y.add(t110.mul(vy)).eq(t110.mul(vpy).add(py)));
    eqs.push(z.add(t110.mul(vz)).eq(t110.mul(vpz).add(pz)));
    px = 205779393651525;
    py = 158598001085695;
    pz = 168943397919337;
    vpx = 152;
    vpy = 264;
    vpz = 256;
    
    
    eqs.push(x.add(t111.mul(vx)).eq(t111.mul(vpx).add(px)));
    eqs.push(y.add(t111.mul(vy)).eq(t111.mul(vpy).add(py)));
    eqs.push(z.add(t111.mul(vz)).eq(t111.mul(vpz).add(pz)));
    px = 201750236796640;
    py = 12985344330332;
    pz = 2118606375894;
    vpx = 139;
    vpy = 411;
    vpz = 499;
    
    
    eqs.push(x.add(t112.mul(vx)).eq(t112.mul(vpx).add(px)));
    eqs.push(y.add(t112.mul(vy)).eq(t112.mul(vpy).add(py)));
    eqs.push(z.add(t112.mul(vz)).eq(t112.mul(vpz).add(pz)));
    px = 292284953515732;
    py = 350387069343910;
    pz = 274587215237438;
    vpx = -59;
    vpy = 109;
    vpz = 47;
    
    
    eqs.push(x.add(t113.mul(vx)).eq(t113.mul(vpx).add(px)));
    eqs.push(y.add(t113.mul(vy)).eq(t113.mul(vpy).add(py)));
    eqs.push(z.add(t113.mul(vz)).eq(t113.mul(vpz).add(pz)));
    px = 279339603973190;
    py = 396504749587547;
    pz = 287191191874116;
    vpx = -17;
    vpy = -8;
    vpz = -15;
    
    
    eqs.push(x.add(t114.mul(vx)).eq(t114.mul(vpx).add(px)));
    eqs.push(y.add(t114.mul(vy)).eq(t114.mul(vpy).add(py)));
    eqs.push(z.add(t114.mul(vz)).eq(t114.mul(vpz).add(pz)));
    px = 288204432689707;
    py = 392989194073110;
    pz = 280376285126608;
    vpx = -42;
    vpy = -61;
    vpz = 25;
    
    
    eqs.push(x.add(t115.mul(vx)).eq(t115.mul(vpx).add(px)));
    eqs.push(y.add(t115.mul(vy)).eq(t115.mul(vpy).add(py)));
    eqs.push(z.add(t115.mul(vz)).eq(t115.mul(vpz).add(pz)));
    px = 167132397590417;
    py = 213225790229422;
    pz = 62525039623800;
    vpx = 181;
    vpy = 45;
    vpz = 369;
    
    
    eqs.push(x.add(t116.mul(vx)).eq(t116.mul(vpx).add(px)));
    eqs.push(y.add(t116.mul(vy)).eq(t116.mul(vpy).add(py)));
    eqs.push(z.add(t116.mul(vz)).eq(t116.mul(vpz).add(pz)));
    px = 245654091693687;
    py = 334202746092570;
    pz = 156918144838580;
    vpx = 111;
    vpy = 114;
    vpz = 452;
    
    
    eqs.push(x.add(t117.mul(vx)).eq(t117.mul(vpx).add(px)));
    eqs.push(y.add(t117.mul(vy)).eq(t117.mul(vpy).add(py)));
    eqs.push(z.add(t117.mul(vz)).eq(t117.mul(vpz).add(pz)));
    px = 312867158510437;
    py = 261732270547545;
    pz = 387814542702538;
    vpx = -68;
    vpy = 116;
    vpz = -201;
    
    
    eqs.push(x.add(t118.mul(vx)).eq(t118.mul(vpx).add(px)));
    eqs.push(y.add(t118.mul(vy)).eq(t118.mul(vpy).add(py)));
    eqs.push(z.add(t118.mul(vz)).eq(t118.mul(vpz).add(pz)));
    px = 251443737700485;
    py = 299042777218395;
    pz = 331691921259038;
    vpx = 68;
    vpy = 34;
    vpz = -77;
    
    
    eqs.push(x.add(t119.mul(vx)).eq(t119.mul(vpx).add(px)));
    eqs.push(y.add(t119.mul(vy)).eq(t119.mul(vpy).add(py)));
    eqs.push(z.add(t119.mul(vz)).eq(t119.mul(vpz).add(pz)));
    px = 249071808318983;
    py = 339880497661598;
    pz = 318019160349960;
    vpx = 99;
    vpy = 93;
    vpz = -101;
    
    
    eqs.push(x.add(t120.mul(vx)).eq(t120.mul(vpx).add(px)));
    eqs.push(y.add(t120.mul(vy)).eq(t120.mul(vpy).add(py)));
    eqs.push(z.add(t120.mul(vz)).eq(t120.mul(vpz).add(pz)));
    px = 345158773413630;
    py = 462131781350082;
    pz = 309436145474852;
    vpx = -163;
    vpy = -327;
    vpz = -39;
    
    
    eqs.push(x.add(t121.mul(vx)).eq(t121.mul(vpx).add(px)));
    eqs.push(y.add(t121.mul(vy)).eq(t121.mul(vpy).add(py)));
    eqs.push(z.add(t121.mul(vz)).eq(t121.mul(vpz).add(pz)));
    px = 202130071322571;
    py = 279871754990196;
    pz = 257527720559768;
    vpx = 114;
    vpy = -94;
    vpz = 73;
    
    
    eqs.push(x.add(t122.mul(vx)).eq(t122.mul(vpx).add(px)));
    eqs.push(y.add(t122.mul(vy)).eq(t122.mul(vpy).add(py)));
    eqs.push(z.add(t122.mul(vz)).eq(t122.mul(vpz).add(pz)));
    px = 285698456170628;
    py = 389258400382057;
    pz = 283159525263149;
    vpx = -33;
    vpy = -44;
    vpz = 14;
    
    
    eqs.push(x.add(t123.mul(vx)).eq(t123.mul(vpx).add(px)));
    eqs.push(y.add(t123.mul(vy)).eq(t123.mul(vpy).add(py)));
    eqs.push(z.add(t123.mul(vz)).eq(t123.mul(vpz).add(pz)));
    px = 299827810110366;
    py = 263703105196145;
    pz = 180961293180126;
    vpx = -13;
    vpy = -66;
    vpz = 175;
    
    
    eqs.push(x.add(t124.mul(vx)).eq(t124.mul(vpx).add(px)));
    eqs.push(y.add(t124.mul(vy)).eq(t124.mul(vpy).add(py)));
    eqs.push(z.add(t124.mul(vz)).eq(t124.mul(vpz).add(pz)));
    px = 224485850365387;
    py = 70640821943795;
    pz = 141634852869037;
    vpx = 106;
    vpy = 354;
    vpz = 282;
    
    
    eqs.push(x.add(t125.mul(vx)).eq(t125.mul(vpx).add(px)));
    eqs.push(y.add(t125.mul(vy)).eq(t125.mul(vpy).add(py)));
    eqs.push(z.add(t125.mul(vz)).eq(t125.mul(vpz).add(pz)));
    px = 313614170820024;
    py = 195171223806147;
    pz = 341771827813217;
    vpx = -35;
    vpy = 48;
    vpz = -44;
    
    
    eqs.push(x.add(t126.mul(vx)).eq(t126.mul(vpx).add(px)));
    eqs.push(y.add(t126.mul(vy)).eq(t126.mul(vpy).add(py)));
    eqs.push(z.add(t126.mul(vz)).eq(t126.mul(vpz).add(pz)));
    px = 234803600210211;
    py = 72733572075097;
    pz = 404522037783646;
    vpx = 98;
    vpy = 460;
    vpz = -213;
    
    
    eqs.push(x.add(t127.mul(vx)).eq(t127.mul(vpx).add(px)));
    eqs.push(y.add(t127.mul(vy)).eq(t127.mul(vpy).add(py)));
    eqs.push(z.add(t127.mul(vz)).eq(t127.mul(vpz).add(pz)));
    px = 300197381692515;
    py = 549817932431822;
    pz = 349210583580184;
    vpx = -10;
    vpy = -435;
    vpz = -39;
    
    
    eqs.push(x.add(t128.mul(vx)).eq(t128.mul(vpx).add(px)));
    eqs.push(y.add(t128.mul(vy)).eq(t128.mul(vpy).add(py)));
    eqs.push(z.add(t128.mul(vz)).eq(t128.mul(vpz).add(pz)));
    px = 254308938013475;
    py = 228010819920710;
    pz = 270823461852576;
    vpx = 55;
    vpy = 94;
    vpz = 57;
    
    
    eqs.push(x.add(t129.mul(vx)).eq(t129.mul(vpx).add(px)));
    eqs.push(y.add(t129.mul(vy)).eq(t129.mul(vpy).add(py)));
    eqs.push(z.add(t129.mul(vz)).eq(t129.mul(vpz).add(pz)));
    px = 276569191946117;
    py = 456319180009760;
    pz = 277217824707488;
    vpx = -45;
    vpy = -246;
    vpz = 5;
    
    
    eqs.push(x.add(t130.mul(vx)).eq(t130.mul(vpx).add(px)));
    eqs.push(y.add(t130.mul(vy)).eq(t130.mul(vpy).add(py)));
    eqs.push(z.add(t130.mul(vz)).eq(t130.mul(vpz).add(pz)));
    px = 365061136404707;
    py = 490762403014510;
    pz = 227059802667528;
    vpx = -149;
    vpy = -381;
    vpz = 138;
    
    
    eqs.push(x.add(t131.mul(vx)).eq(t131.mul(vpx).add(px)));
    eqs.push(y.add(t131.mul(vy)).eq(t131.mul(vpy).add(py)));
    eqs.push(z.add(t131.mul(vz)).eq(t131.mul(vpz).add(pz)));
    px = 215364734017875;
    py = 180715624686174;
    pz = 309399294492047;
    vpx = 82;
    vpy = -43;
    vpz = 16;
    
    
    eqs.push(x.add(t132.mul(vx)).eq(t132.mul(vpx).add(px)));
    eqs.push(y.add(t132.mul(vy)).eq(t132.mul(vpy).add(py)));
    eqs.push(z.add(t132.mul(vz)).eq(t132.mul(vpz).add(pz)));
    px = 256910072363323;
    py = 125697352146654;
    pz = 366453893454240;
    vpx = 40;
    vpy = 20;
    vpz = -44;
    
    
    eqs.push(x.add(t133.mul(vx)).eq(t133.mul(vpx).add(px)));
    eqs.push(y.add(t133.mul(vy)).eq(t133.mul(vpy).add(py)));
    eqs.push(z.add(t133.mul(vz)).eq(t133.mul(vpz).add(pz)));
    px = 262846559729706;
    py = 375681397818765;
    pz = 273041846062208;
    vpx = 59;
    vpy = 54;
    vpz = 53;
    
    
    eqs.push(x.add(t134.mul(vx)).eq(t134.mul(vpx).add(px)));
    eqs.push(y.add(t134.mul(vy)).eq(t134.mul(vpy).add(py)));
    eqs.push(z.add(t134.mul(vz)).eq(t134.mul(vpz).add(pz)));
    px = 249059367699955;
    py = 319717365318984;
    pz = 316469445437246;
    vpx = 82;
    vpy = 47;
    vpz = -61;
    
    
    eqs.push(x.add(t135.mul(vx)).eq(t135.mul(vpx).add(px)));
    eqs.push(y.add(t135.mul(vy)).eq(t135.mul(vpy).add(py)));
    eqs.push(z.add(t135.mul(vz)).eq(t135.mul(vpz).add(pz)));
    px = 351641125870887;
    py = 373169814589095;
    pz = 279927346260308;
    vpx = -210;
    vpy = -68;
    vpz = 33;
    
    
    eqs.push(x.add(t136.mul(vx)).eq(t136.mul(vpx).add(px)));
    eqs.push(y.add(t136.mul(vy)).eq(t136.mul(vpy).add(py)));
    eqs.push(z.add(t136.mul(vz)).eq(t136.mul(vpz).add(pz)));
    px = 372162402226347;
    py = 397883781850710;
    pz = 390113135537768;
    vpx = -260;
    vpy = -146;
    vpz = -276;
    
    
    eqs.push(x.add(t137.mul(vx)).eq(t137.mul(vpx).add(px)));
    eqs.push(y.add(t137.mul(vy)).eq(t137.mul(vpy).add(py)));
    eqs.push(z.add(t137.mul(vz)).eq(t137.mul(vpz).add(pz)));
    px = 337578787443909;
    py = 271222575652692;
    pz = 273454033570862;
    vpx = -137;
    vpy = 136;
    vpz = 52;
    
    
    eqs.push(x.add(t138.mul(vx)).eq(t138.mul(vpx).add(px)));
    eqs.push(y.add(t138.mul(vy)).eq(t138.mul(vpy).add(py)));
    eqs.push(z.add(t138.mul(vz)).eq(t138.mul(vpz).add(pz)));
    px = 399858185929617;
    py = 297153999560655;
    pz = 206854191129263;
    vpx = -152;
    vpy = -102;
    vpz = 144;
    
    
    eqs.push(x.add(t139.mul(vx)).eq(t139.mul(vpx).add(px)));
    eqs.push(y.add(t139.mul(vy)).eq(t139.mul(vpy).add(py)));
    eqs.push(z.add(t139.mul(vz)).eq(t139.mul(vpz).add(pz)));
    px = 256793953778627;
    py = 450638882814610;
    pz = 135490117389868;
    vpx = 78;
    vpy = -281;
    vpz = 579;
    
    
    eqs.push(x.add(t140.mul(vx)).eq(t140.mul(vpx).add(px)));
    eqs.push(y.add(t140.mul(vy)).eq(t140.mul(vpy).add(py)));
    eqs.push(z.add(t140.mul(vz)).eq(t140.mul(vpz).add(pz)));
    px = 247177305739257;
    py = 208350046459560;
    pz = 104164698972158;
    vpx = 77;
    vpy = 230;
    vpz = 424;
    
    
    eqs.push(x.add(t141.mul(vx)).eq(t141.mul(vpx).add(px)));
    eqs.push(y.add(t141.mul(vy)).eq(t141.mul(vpy).add(py)));
    eqs.push(z.add(t141.mul(vz)).eq(t141.mul(vpz).add(pz)));
    px = 37127457323232;
    py = 142872779547270;
    pz = 37321661260448;
    vpx = 311;
    vpy = 61;
    vpz = 341;
    
    
    eqs.push(x.add(t142.mul(vx)).eq(t142.mul(vpx).add(px)));
    eqs.push(y.add(t142.mul(vy)).eq(t142.mul(vpy).add(py)));
    eqs.push(z.add(t142.mul(vz)).eq(t142.mul(vpz).add(pz)));
    px = 295888104359025;
    py = 343758112735404;
    pz = 317764128822074;
    vpx = -35;
    vpy = -44;
    vpz = -54;
    
    
    eqs.push(x.add(t143.mul(vx)).eq(t143.mul(vpx).add(px)));
    eqs.push(y.add(t143.mul(vy)).eq(t143.mul(vpy).add(py)));
    eqs.push(z.add(t143.mul(vz)).eq(t143.mul(vpz).add(pz)));
    px = 172249909503397;
    py = 363737392387940;
    pz = 180402839361078;
    vpx = 133;
    vpy = -222;
    vpz = 154;
    
    
    eqs.push(x.add(t144.mul(vx)).eq(t144.mul(vpx).add(px)));
    eqs.push(y.add(t144.mul(vy)).eq(t144.mul(vpy).add(py)));
    eqs.push(z.add(t144.mul(vz)).eq(t144.mul(vpz).add(pz)));
    px = 266945241349051;
    py = 252155610635398;
    pz = 284675410934072;
    vpx = 34;
    vpy = 160;
    vpz = 26;
    
    
    eqs.push(x.add(t145.mul(vx)).eq(t145.mul(vpx).add(px)));
    eqs.push(y.add(t145.mul(vy)).eq(t145.mul(vpy).add(py)));
    eqs.push(z.add(t145.mul(vz)).eq(t145.mul(vpz).add(pz)));
    px = 363630573951458;
    py = 250073512495827;
    pz = 350128671211073;
    vpx = -101;
    vpy = -40;
    vpz = -52;
    
    
    eqs.push(x.add(t146.mul(vx)).eq(t146.mul(vpx).add(px)));
    eqs.push(y.add(t146.mul(vy)).eq(t146.mul(vpy).add(py)));
    eqs.push(z.add(t146.mul(vz)).eq(t146.mul(vpz).add(pz)));
    px = 258823670942991;
    py = 155219406452350;
    pz = 365590266784736;
    vpx = 38;
    vpy = -11;
    vpz = -43;
    
    
    eqs.push(x.add(t147.mul(vx)).eq(t147.mul(vpx).add(px)));
    eqs.push(y.add(t147.mul(vy)).eq(t147.mul(vpy).add(py)));
    eqs.push(z.add(t147.mul(vz)).eq(t147.mul(vpz).add(pz)));
    px = 342703092464223;
    py = 215373784249550;
    pz = 286919689594404;
    vpx = -73;
    vpy = 9;
    vpz = 34;
    
    
    eqs.push(x.add(t148.mul(vx)).eq(t148.mul(vpx).add(px)));
    eqs.push(y.add(t148.mul(vy)).eq(t148.mul(vpy).add(py)));
    eqs.push(z.add(t148.mul(vz)).eq(t148.mul(vpz).add(pz)));
    px = 260407037303904;
    py = 414839283281769;
    pz = 219962698211171;
    vpx = 83;
    vpy = -52;
    vpz = 356;
    
    
    eqs.push(x.add(t149.mul(vx)).eq(t149.mul(vpx).add(px)));
    eqs.push(y.add(t149.mul(vy)).eq(t149.mul(vpy).add(py)));
    eqs.push(z.add(t149.mul(vz)).eq(t149.mul(vpz).add(pz)));
    px = 310782605378913;
    py = 113664166198858;
    pz = 274077496878762;
    vpx = -13;
    vpy = 7;
    vpz = 52;
    
    
    eqs.push(x.add(t150.mul(vx)).eq(t150.mul(vpx).add(px)));
    eqs.push(y.add(t150.mul(vy)).eq(t150.mul(vpy).add(py)));
    eqs.push(z.add(t150.mul(vz)).eq(t150.mul(vpz).add(pz)));
    px = 291127144241187;
    py = 318569697238950;
    pz = 259564147602086;
    vpx = 6;
    vpy = -191;
    vpz = 66;
    
    
    eqs.push(x.add(t151.mul(vx)).eq(t151.mul(vpx).add(px)));
    eqs.push(y.add(t151.mul(vy)).eq(t151.mul(vpy).add(py)));
    eqs.push(z.add(t151.mul(vz)).eq(t151.mul(vpz).add(pz)));
    px = 274748127176803;
    py = 292552751967326;
    pz = 223845757853312;
    vpx = 9;
    vpy = 337;
    vpz = 245;
    
    
    eqs.push(x.add(t152.mul(vx)).eq(t152.mul(vpx).add(px)));
    eqs.push(y.add(t152.mul(vy)).eq(t152.mul(vpy).add(py)));
    eqs.push(z.add(t152.mul(vz)).eq(t152.mul(vpz).add(pz)));
    px = 293125400088063;
    py = 476133192349023;
    pz = 361869628526162;
    vpx = -82;
    vpy = -390;
    vpz = -369;
    
    
    eqs.push(x.add(t153.mul(vx)).eq(t153.mul(vpx).add(px)));
    eqs.push(y.add(t153.mul(vy)).eq(t153.mul(vpy).add(py)));
    eqs.push(z.add(t153.mul(vz)).eq(t153.mul(vpz).add(pz)));
    px = 282164981148321;
    py = 279274272892224;
    pz = 276609348369788;
    vpx = -7;
    vpy = 186;
    vpz = 43;
    
    
    eqs.push(x.add(t154.mul(vx)).eq(t154.mul(vpx).add(px)));
    eqs.push(y.add(t154.mul(vy)).eq(t154.mul(vpy).add(py)));
    eqs.push(z.add(t154.mul(vz)).eq(t154.mul(vpz).add(pz)));
    px = 174918204232227;
    py = 112847121262641;
    pz = 27991863189436;
    vpx = 146;
    vpy = 110;
    vpz = 361;
    
    
    eqs.push(x.add(t155.mul(vx)).eq(t155.mul(vpx).add(px)));
    eqs.push(y.add(t155.mul(vy)).eq(t155.mul(vpy).add(py)));
    eqs.push(z.add(t155.mul(vz)).eq(t155.mul(vpz).add(pz)));
    px = 249955668205419;
    py = 17029432884558;
    pz = 46779983503448;
    vpx = 54;
    vpy = 281;
    vpz = 363;
    
    
    eqs.push(x.add(t156.mul(vx)).eq(t156.mul(vpx).add(px)));
    eqs.push(y.add(t156.mul(vy)).eq(t156.mul(vpy).add(py)));
    eqs.push(z.add(t156.mul(vz)).eq(t156.mul(vpz).add(pz)));
    px = 325400633182867;
    py = 521617731298910;
    pz = 409839075322298;
    vpx = -50;
    vpy = -411;
    vpz = -136;
    
    
    eqs.push(x.add(t157.mul(vx)).eq(t157.mul(vpx).add(px)));
    eqs.push(y.add(t157.mul(vy)).eq(t157.mul(vpy).add(py)));
    eqs.push(z.add(t157.mul(vz)).eq(t157.mul(vpz).add(pz)));
    px = 277793703195657;
    py = 422561915271444;
    pz = 188813007504665;
    vpx = -24;
    vpy = -53;
    vpz = 622;
    
    
    eqs.push(x.add(t158.mul(vx)).eq(t158.mul(vpx).add(px)));
    eqs.push(y.add(t158.mul(vy)).eq(t158.mul(vpy).add(py)));
    eqs.push(z.add(t158.mul(vz)).eq(t158.mul(vpz).add(pz)));
    px = 318315084458607;
    py = 323300159682981;
    pz = 286939475730545;
    vpx = -74;
    vpy = -38;
    vpz = 24;
    
    
    eqs.push(x.add(t159.mul(vx)).eq(t159.mul(vpx).add(px)));
    eqs.push(y.add(t159.mul(vy)).eq(t159.mul(vpy).add(py)));
    eqs.push(z.add(t159.mul(vz)).eq(t159.mul(vpz).add(pz)));
    px = 255642309986097;
    py = 153965957702700;
    pz = 396941119858772;
    vpx = 41;
    vpy = -16;
    vpz = -73;
    
    
    eqs.push(x.add(t160.mul(vx)).eq(t160.mul(vpx).add(px)));
    eqs.push(y.add(t160.mul(vy)).eq(t160.mul(vpy).add(py)));
    eqs.push(z.add(t160.mul(vz)).eq(t160.mul(vpz).add(pz)));
    px = 311855158178637;
    py = 285884222493028;
    pz = 276266740979067;
    vpx = -64;
    vpy = 55;
    vpz = 46;
    
    
    eqs.push(x.add(t161.mul(vx)).eq(t161.mul(vpx).add(px)));
    eqs.push(y.add(t161.mul(vy)).eq(t161.mul(vpy).add(py)));
    eqs.push(z.add(t161.mul(vz)).eq(t161.mul(vpz).add(pz)));
    px = 252905927924047;
    py = 229397781030026;
    pz = 369216471913138;
    vpx = 46;
    vpy = -63;
    vpz = -57;
    
    
    eqs.push(x.add(t162.mul(vx)).eq(t162.mul(vpx).add(px)));
    eqs.push(y.add(t162.mul(vy)).eq(t162.mul(vpy).add(py)));
    eqs.push(z.add(t162.mul(vz)).eq(t162.mul(vpz).add(pz)));
    px = 295981809556490;
    py = 246548466213584;
    pz = 395456892713651;
    vpx = -11;
    vpy = -17;
    vpz = -124;
    
    
    eqs.push(x.add(t163.mul(vx)).eq(t163.mul(vpx).add(px)));
    eqs.push(y.add(t163.mul(vy)).eq(t163.mul(vpy).add(py)));
    eqs.push(z.add(t163.mul(vz)).eq(t163.mul(vpz).add(pz)));
    px = 279043571254974;
    py = 200328667112248;
    pz = 359555323278878;
    vpx = 17;
    vpy = -57;
    vpz = -37;
    
    
    eqs.push(x.add(t164.mul(vx)).eq(t164.mul(vpx).add(px)));
    eqs.push(y.add(t164.mul(vy)).eq(t164.mul(vpy).add(py)));
    eqs.push(z.add(t164.mul(vz)).eq(t164.mul(vpz).add(pz)));
    px = 217695580278467;
    py = 167295523885635;
    pz = 369314559700858;
    vpx = 130;
    vpy = 254;
    vpz = -137;
    
    
    eqs.push(x.add(t165.mul(vx)).eq(t165.mul(vpx).add(px)));
    eqs.push(y.add(t165.mul(vy)).eq(t165.mul(vpy).add(py)));
    eqs.push(z.add(t165.mul(vz)).eq(t165.mul(vpz).add(pz)));
    px = 174106338139371;
    py = 39732596425854;
    pz = 161382584008736;
    vpx = 145;
    vpy = 193;
    vpz = 191;
    
    
    eqs.push(x.add(t166.mul(vx)).eq(t166.mul(vpx).add(px)));
    eqs.push(y.add(t166.mul(vy)).eq(t166.mul(vpy).add(py)));
    eqs.push(z.add(t166.mul(vz)).eq(t166.mul(vpz).add(pz)));
    px = 346210458355071;
    py = 309591828785934;
    pz = 307843658767280;
    vpx = -157;
    vpy = 41;
    vpz = -31;
    
    
    eqs.push(x.add(t167.mul(vx)).eq(t167.mul(vpx).add(px)));
    eqs.push(y.add(t167.mul(vy)).eq(t167.mul(vpy).add(py)));
    eqs.push(z.add(t167.mul(vz)).eq(t167.mul(vpz).add(pz)));
    px = 268115431092279;
    py = 437278052184396;
    pz = 275571615441128;
    vpx = 44;
    vpy = -122;
    vpz = 33;
    
    
    eqs.push(x.add(t168.mul(vx)).eq(t168.mul(vpx).add(px)));
    eqs.push(y.add(t168.mul(vy)).eq(t168.mul(vpy).add(py)));
    eqs.push(z.add(t168.mul(vz)).eq(t168.mul(vpz).add(pz)));
    px = 282893044906941;
    py = 149804627700634;
    pz = 292487568198972;
    vpx = 8;
    vpy = 121;
    vpz = 25;
    
    
    eqs.push(x.add(t169.mul(vx)).eq(t169.mul(vpx).add(px)));
    eqs.push(y.add(t169.mul(vy)).eq(t169.mul(vpy).add(py)));
    eqs.push(z.add(t169.mul(vz)).eq(t169.mul(vpz).add(pz)));
    px = 267897589339695;
    py = 437936255526786;
    pz = 277577544596048;
    vpx = 59;
    vpy = 10;
    vpz = -7;
    
    
    eqs.push(x.add(t170.mul(vx)).eq(t170.mul(vpx).add(px)));
    eqs.push(y.add(t170.mul(vy)).eq(t170.mul(vpy).add(py)));
    eqs.push(z.add(t170.mul(vz)).eq(t170.mul(vpz).add(pz)));
    px = 346296387214107;
    py = 194796533724990;
    pz = 320753034661568;
    vpx = -79;
    vpy = 41;
    vpz = -13;
    
    
    eqs.push(x.add(t171.mul(vx)).eq(t171.mul(vpx).add(px)));
    eqs.push(y.add(t171.mul(vy)).eq(t171.mul(vpy).add(py)));
    eqs.push(z.add(t171.mul(vz)).eq(t171.mul(vpz).add(pz)));
    px = 315255524851362;
    py = 229609278952623;
    pz = 335034771519884;
    vpx = -29;
    vpy = -44;
    vpz = -23;
    
    
    eqs.push(x.add(t172.mul(vx)).eq(t172.mul(vpx).add(px)));
    eqs.push(y.add(t172.mul(vy)).eq(t172.mul(vpy).add(py)));
    eqs.push(z.add(t172.mul(vz)).eq(t172.mul(vpz).add(pz)));
    px = 286757602361455;
    py = 297841319495254;
    pz = 420052876213368;
    vpx = -33;
    vpy = 267;
    vpz = -477;
    
    
    eqs.push(x.add(t173.mul(vx)).eq(t173.mul(vpx).add(px)));
    eqs.push(y.add(t173.mul(vy)).eq(t173.mul(vpy).add(py)));
    eqs.push(z.add(t173.mul(vz)).eq(t173.mul(vpz).add(pz)));
    px = 279149085394077;
    py = 286241741815838;
    pz = 295809686900210;
    vpx = 11;
    vpy = -27;
    vpz = 14;
    
    
    eqs.push(x.add(t174.mul(vx)).eq(t174.mul(vpx).add(px)));
    eqs.push(y.add(t174.mul(vy)).eq(t174.mul(vpy).add(py)));
    eqs.push(z.add(t174.mul(vz)).eq(t174.mul(vpz).add(pz)));
    px = 249787414488866;
    py = 224616754074458;
    pz = 353421002136562;
    vpx = 127;
    vpy = 841;
    vpz = -341;
    
    
    eqs.push(x.add(t175.mul(vx)).eq(t175.mul(vpx).add(px)));
    eqs.push(y.add(t175.mul(vy)).eq(t175.mul(vpy).add(py)));
    eqs.push(z.add(t175.mul(vz)).eq(t175.mul(vpz).add(pz)));
    px = 254897534574362;
    py = 284861161068002;
    pz = 291192767414115;
    vpx = 61;
    vpy = 73;
    vpz = 12;
    
    
    eqs.push(x.add(t176.mul(vx)).eq(t176.mul(vpx).add(px)));
    eqs.push(y.add(t176.mul(vy)).eq(t176.mul(vpy).add(py)));
    eqs.push(z.add(t176.mul(vz)).eq(t176.mul(vpz).add(pz)));
    px = 327689466751032;
    py = 312558557705445;
    pz = 390910460681528;
    vpx = -79;
    vpy = -54;
    vpz = -163;
    
    
    eqs.push(x.add(t177.mul(vx)).eq(t177.mul(vpx).add(px)));
    eqs.push(y.add(t177.mul(vy)).eq(t177.mul(vpy).add(py)));
    eqs.push(z.add(t177.mul(vz)).eq(t177.mul(vpz).add(pz)));
    px = 349426050024227;
    py = 325969473167078;
    pz = 411633306087357;
    vpx = -254;
    vpy = 157;
    vpz = -438;
    
    
    eqs.push(x.add(t178.mul(vx)).eq(t178.mul(vpx).add(px)));
    eqs.push(y.add(t178.mul(vy)).eq(t178.mul(vpy).add(py)));
    eqs.push(z.add(t178.mul(vz)).eq(t178.mul(vpz).add(pz)));
    px = 286724659720566;
    py = 160122975419178;
    pz = 286492087628186;
    vpx = 9;
    vpy = -15;
    vpz = 39;
    
    
    eqs.push(x.add(t179.mul(vx)).eq(t179.mul(vpx).add(px)));
    eqs.push(y.add(t179.mul(vy)).eq(t179.mul(vpy).add(py)));
    eqs.push(z.add(t179.mul(vz)).eq(t179.mul(vpz).add(pz)));
    px = 262042638250419;
    py = 379072267855814;
    pz = 314462337759672;
    vpx = 77;
    vpy = 186;
    vpz = -200;
    
    
    eqs.push(x.add(t180.mul(vx)).eq(t180.mul(vpx).add(px)));
    eqs.push(y.add(t180.mul(vy)).eq(t180.mul(vpy).add(py)));
    eqs.push(z.add(t180.mul(vz)).eq(t180.mul(vpz).add(pz)));
    px = 290089021697532;
    py = 396557439881800;
    pz = 284672336406798;
    vpx = -79;
    vpy = 27;
    vpz = -9;
    
    
    eqs.push(x.add(t181.mul(vx)).eq(t181.mul(vpx).add(px)));
    eqs.push(y.add(t181.mul(vy)).eq(t181.mul(vpy).add(py)));
    eqs.push(z.add(t181.mul(vz)).eq(t181.mul(vpz).add(pz)));
    px = 199041215073927;
    py = 175260919960890;
    pz = 160221875421308;
    vpx = 260;
    vpy = 615;
    vpz = 423;
    
    
    eqs.push(x.add(t182.mul(vx)).eq(t182.mul(vpx).add(px)));
    eqs.push(y.add(t182.mul(vy)).eq(t182.mul(vpy).add(py)));
    eqs.push(z.add(t182.mul(vz)).eq(t182.mul(vpz).add(pz)));
    px = 299001970398348;
    py = 410805706210815;
    pz = 309881794080206;
    vpx = -193;
    vpy = 74;
    vpz = -229;
    
    
    eqs.push(x.add(t183.mul(vx)).eq(t183.mul(vpx).add(px)));
    eqs.push(y.add(t183.mul(vy)).eq(t183.mul(vpy).add(py)));
    eqs.push(z.add(t183.mul(vz)).eq(t183.mul(vpz).add(pz)));
    px = 331984959199482;
    py = 407400783870750;
    pz = 286064310174485;
    vpx = -149;
    vpy = -171;
    vpz = 16;
    
    
    eqs.push(x.add(t184.mul(vx)).eq(t184.mul(vpx).add(px)));
    eqs.push(y.add(t184.mul(vy)).eq(t184.mul(vpy).add(py)));
    eqs.push(z.add(t184.mul(vz)).eq(t184.mul(vpz).add(pz)));
    px = 340834762010483;
    py = 451723922878846;
    pz = 270793679940596;
    vpx = -68;
    vpy = -315;
    vpz = 56;
    
    
    eqs.push(x.add(t185.mul(vx)).eq(t185.mul(vpx).add(px)));
    eqs.push(y.add(t185.mul(vy)).eq(t185.mul(vpy).add(py)));
    eqs.push(z.add(t185.mul(vz)).eq(t185.mul(vpz).add(pz)));
    px = 280650616915145;
    py = 300312590469119;
    pz = 236404726841358;
    vpx = 12;
    vpy = -108;
    vpz = 103;
    
    
    eqs.push(x.add(t186.mul(vx)).eq(t186.mul(vpx).add(px)));
    eqs.push(y.add(t186.mul(vy)).eq(t186.mul(vpy).add(py)));
    eqs.push(z.add(t186.mul(vz)).eq(t186.mul(vpz).add(pz)));
    px = 377338176867579;
    py = 289926968025918;
    pz = 270071125136256;
    vpx = -118;
    vpy = -97;
    vpz = 57;
    
    
    eqs.push(x.add(t187.mul(vx)).eq(t187.mul(vpx).add(px)));
    eqs.push(y.add(t187.mul(vy)).eq(t187.mul(vpy).add(py)));
    eqs.push(z.add(t187.mul(vz)).eq(t187.mul(vpz).add(pz)));
    px = 268907170557389;
    py = 477079618977372;
    pz = 213639727025488;
    vpx = 28;
    vpy = -349;
    vpz = 133;
    
    
    eqs.push(x.add(t188.mul(vx)).eq(t188.mul(vpx).add(px)));
    eqs.push(y.add(t188.mul(vy)).eq(t188.mul(vpy).add(py)));
    eqs.push(z.add(t188.mul(vz)).eq(t188.mul(vpz).add(pz)));
    px = 225234660515415;
    py = 245452587607632;
    pz = 302310636907138;
    vpx = 80;
    vpy = -70;
    vpz = 18;
    
    
    eqs.push(x.add(t189.mul(vx)).eq(t189.mul(vpx).add(px)));
    eqs.push(y.add(t189.mul(vy)).eq(t189.mul(vpy).add(py)));
    eqs.push(z.add(t189.mul(vz)).eq(t189.mul(vpz).add(pz)));
    px = 239124996839450;
    py = 329796020316647;
    pz = 217586764756122;
    vpx = 79;
    vpy = -104;
    vpz = 147;
    
    
    eqs.push(x.add(t190.mul(vx)).eq(t190.mul(vpx).add(px)));
    eqs.push(y.add(t190.mul(vy)).eq(t190.mul(vpy).add(py)));
    eqs.push(z.add(t190.mul(vz)).eq(t190.mul(vpz).add(pz)));
    px = 239554809832227;
    py = 129642160432410;
    pz = 315186311453684;
    vpx = 56;
    vpy = -6;
    vpz = 12;
    
    
    eqs.push(x.add(t191.mul(vx)).eq(t191.mul(vpx).add(px)));
    eqs.push(y.add(t191.mul(vy)).eq(t191.mul(vpy).add(py)));
    eqs.push(z.add(t191.mul(vz)).eq(t191.mul(vpz).add(pz)));
    px = 253320335853005;
    py = 413624098121136;
    pz = 266850941738582;
    vpx = 117;
    vpy = -64;
    vpz = 86;
    
    
    eqs.push(x.add(t192.mul(vx)).eq(t192.mul(vpx).add(px)));
    eqs.push(y.add(t192.mul(vy)).eq(t192.mul(vpy).add(py)));
    eqs.push(z.add(t192.mul(vz)).eq(t192.mul(vpz).add(pz)));
    px = 110151001176190;
    py = 232349810448540;
    pz = 176211588702025;
    vpx = 213;
    vpy = -61;
    vpz = 166;
    
    
    eqs.push(x.add(t193.mul(vx)).eq(t193.mul(vpx).add(px)));
    eqs.push(y.add(t193.mul(vy)).eq(t193.mul(vpy).add(py)));
    eqs.push(z.add(t193.mul(vz)).eq(t193.mul(vpz).add(pz)));
    px = 343059121083093;
    py = 337995951341106;
    pz = 558359726012288;
    vpx = -137;
    vpy = -49;
    vpz = -587;
    
    
    eqs.push(x.add(t194.mul(vx)).eq(t194.mul(vpx).add(px)));
    eqs.push(y.add(t194.mul(vy)).eq(t194.mul(vpy).add(py)));
    eqs.push(z.add(t194.mul(vz)).eq(t194.mul(vpz).add(pz)));
    px = 428022104051019;
    py = 368959101658182;
    pz = 365140203218624;
    vpx = -152;
    vpy = -224;
    vpz = -51;
    
    
    eqs.push(x.add(t195.mul(vx)).eq(t195.mul(vpx).add(px)));
    eqs.push(y.add(t195.mul(vy)).eq(t195.mul(vpy).add(py)));
    eqs.push(z.add(t195.mul(vz)).eq(t195.mul(vpz).add(pz)));
    px = 391393694476735;
    py = 271335399064952;
    pz = 241092019464786;
    vpx = -152;
    vpy = -48;
    vpz = 100;
    
    
    eqs.push(x.add(t196.mul(vx)).eq(t196.mul(vpx).add(px)));
    eqs.push(y.add(t196.mul(vy)).eq(t196.mul(vpy).add(py)));
    eqs.push(z.add(t196.mul(vz)).eq(t196.mul(vpz).add(pz)));
    px = 452639727139518;
    py = 425511057245729;
    pz = 406439503340981;
    vpx = -265;
    vpy = -270;
    vpz = -160;
    
    
    eqs.push(x.add(t197.mul(vx)).eq(t197.mul(vpx).add(px)));
    eqs.push(y.add(t197.mul(vy)).eq(t197.mul(vpy).add(py)));
    eqs.push(z.add(t197.mul(vz)).eq(t197.mul(vpz).add(pz)));
    px = 218921039491667;
    py = 108271625982030;
    pz = 352676508164368;
    vpx = 79;
    vpy = 35;
    vpz = -29;
    
    
    eqs.push(x.add(t198.mul(vx)).eq(t198.mul(vpx).add(px)));
    eqs.push(y.add(t198.mul(vy)).eq(t198.mul(vpy).add(py)));
    eqs.push(z.add(t198.mul(vz)).eq(t198.mul(vpz).add(pz)));
    px = 221949088556126;
    py = 205077065621025;
    pz = 338727452810928;
    vpx = 85;
    vpy = -16;
    vpz = -27;
    
    
    eqs.push(x.add(t199.mul(vx)).eq(t199.mul(vpx).add(px)));
    eqs.push(y.add(t199.mul(vy)).eq(t199.mul(vpy).add(py)));
    eqs.push(z.add(t199.mul(vz)).eq(t199.mul(vpz).add(pz)));
    px = 280534348923077;
    py = 134095067026585;
    pz = 348093573946506;
    vpx = 16;
    vpy = -6;
    vpz = -21;
    
    
    eqs.push(x.add(t200.mul(vx)).eq(t200.mul(vpx).add(px)));
    eqs.push(y.add(t200.mul(vy)).eq(t200.mul(vpy).add(py)));
    eqs.push(z.add(t200.mul(vz)).eq(t200.mul(vpz).add(pz)));
    px = 125204260705579;
    py = 234160200966486;
    pz = 267155847569192;
    vpx = 174;
    vpy = -97;
    vpz = 59;
    
    
    eqs.push(x.add(t201.mul(vx)).eq(t201.mul(vpx).add(px)));
    eqs.push(y.add(t201.mul(vy)).eq(t201.mul(vpy).add(py)));
    eqs.push(z.add(t201.mul(vz)).eq(t201.mul(vpz).add(pz)));
    px = 290559272158077;
    py = 442249798043770;
    pz = 274221205630908;
    vpx = -145;
    vpy = -149;
    vpz = 43;
    
    
    eqs.push(x.add(t202.mul(vx)).eq(t202.mul(vpx).add(px)));
    eqs.push(y.add(t202.mul(vy)).eq(t202.mul(vpy).add(py)));
    eqs.push(z.add(t202.mul(vz)).eq(t202.mul(vpz).add(pz)));
    px = 243475915019523;
    py = 329912782480662;
    pz = 192292920520856;
    vpx = 95;
    vpy = 12;
    vpz = 260;
    
    
    eqs.push(x.add(t203.mul(vx)).eq(t203.mul(vpx).add(px)));
    eqs.push(y.add(t203.mul(vy)).eq(t203.mul(vpy).add(py)));
    eqs.push(z.add(t203.mul(vz)).eq(t203.mul(vpz).add(pz)));
    px = 521918265103796;
    py = 310256015748577;
    pz = 518211633874598;
    vpx = -251;
    vpy = -162;
    vpz = -217;
    
    
    eqs.push(x.add(t204.mul(vx)).eq(t204.mul(vpx).add(px)));
    eqs.push(y.add(t204.mul(vy)).eq(t204.mul(vpy).add(py)));
    eqs.push(z.add(t204.mul(vz)).eq(t204.mul(vpz).add(pz)));
    px = 312727502788511;
    py = 201561066806116;
    pz = 321076105217151;
    vpx = -26;
    vpy = -9;
    vpz = -6;
    
    
    eqs.push(x.add(t205.mul(vx)).eq(t205.mul(vpx).add(px)));
    eqs.push(y.add(t205.mul(vy)).eq(t205.mul(vpy).add(py)));
    eqs.push(z.add(t205.mul(vz)).eq(t205.mul(vpz).add(pz)));
    px = 494755918231443;
    py = 397724820224070;
    pz = 553863071779156;
    vpx = -280;
    vpy = -241;
    vpz = -330;
    
    
    eqs.push(x.add(t206.mul(vx)).eq(t206.mul(vpx).add(px)));
    eqs.push(y.add(t206.mul(vy)).eq(t206.mul(vpy).add(py)));
    eqs.push(z.add(t206.mul(vz)).eq(t206.mul(vpz).add(pz)));
    px = 293481938243707;
    py = 113760653614610;
    pz = 275206506816308;
    vpx = -6;
    vpy = 154;
    vpz = 50;
    
    
    eqs.push(x.add(t207.mul(vx)).eq(t207.mul(vpx).add(px)));
    eqs.push(y.add(t207.mul(vy)).eq(t207.mul(vpy).add(py)));
    eqs.push(z.add(t207.mul(vz)).eq(t207.mul(vpz).add(pz)));
    px = 286912142714032;
    py = 364865445456985;
    pz = 315289508229308;
    vpx = -35;
    vpy = 34;
    vpz = -103;
    
    
    eqs.push(x.add(t208.mul(vx)).eq(t208.mul(vpx).add(px)));
    eqs.push(y.add(t208.mul(vy)).eq(t208.mul(vpy).add(py)));
    eqs.push(z.add(t208.mul(vz)).eq(t208.mul(vpz).add(pz)));
    px = 187420037282402;
    py = 262416403376697;
    pz = 270877354246967;
    vpx = 141;
    vpy = -52;
    vpz = 56;
    
    
    eqs.push(x.add(t209.mul(vx)).eq(t209.mul(vpx).add(px)));
    eqs.push(y.add(t209.mul(vy)).eq(t209.mul(vpy).add(py)));
    eqs.push(z.add(t209.mul(vz)).eq(t209.mul(vpz).add(pz)));
    px = 269265569314367;
    py = 311334159082475;
    pz = 281210089149523;
    vpx = 30;
    vpy = 210;
    vpz = 24;
    
    
    eqs.push(x.add(t210.mul(vx)).eq(t210.mul(vpx).add(px)));
    eqs.push(y.add(t210.mul(vy)).eq(t210.mul(vpy).add(py)));
    eqs.push(z.add(t210.mul(vz)).eq(t210.mul(vpz).add(pz)));
    px = 262429174710483;
    py = 108363088475589;
    pz = 352672334290448;
    vpx = 34;
    vpy = 26;
    vpz = -27;
    
    
    eqs.push(x.add(t211.mul(vx)).eq(t211.mul(vpx).add(px)));
    eqs.push(y.add(t211.mul(vy)).eq(t211.mul(vpy).add(py)));
    eqs.push(z.add(t211.mul(vz)).eq(t211.mul(vpz).add(pz)));
    px = 266123105107587;
    py = 231758707729990;
    pz = 314309990844168;
    vpx = 32;
    vpy = -5;
    vpz = -5;
    
    
    eqs.push(x.add(t212.mul(vx)).eq(t212.mul(vpx).add(px)));
    eqs.push(y.add(t212.mul(vy)).eq(t212.mul(vpy).add(py)));
    eqs.push(z.add(t212.mul(vz)).eq(t212.mul(vpz).add(pz)));
    px = 267316984179419;
    py = 474832315242782;
    pz = 311127502675744;
    vpx = 52;
    vpy = -425;
    vpz = -269;
    
    
    eqs.push(x.add(t213.mul(vx)).eq(t213.mul(vpx).add(px)));
    eqs.push(y.add(t213.mul(vy)).eq(t213.mul(vpy).add(py)));
    eqs.push(z.add(t213.mul(vz)).eq(t213.mul(vpz).add(pz)));
    px = 345898863591507;
    py = 388497912289980;
    pz = 265200771902318;
    vpx = -234;
    vpy = -72;
    vpz = 80;
    
    
    eqs.push(x.add(t214.mul(vx)).eq(t214.mul(vpx).add(px)));
    eqs.push(y.add(t214.mul(vy)).eq(t214.mul(vpy).add(py)));
    eqs.push(z.add(t214.mul(vz)).eq(t214.mul(vpz).add(pz)));
    px = 217520406141762;
    py = 130932703317915;
    pz = 337317388773498;
    vpx = 77;
    vpy = -10;
    vpz = -9;
    
    
    eqs.push(x.add(t215.mul(vx)).eq(t215.mul(vpx).add(px)));
    eqs.push(y.add(t215.mul(vy)).eq(t215.mul(vpy).add(py)));
    eqs.push(z.add(t215.mul(vz)).eq(t215.mul(vpz).add(pz)));
    px = 355913193078057;
    py = 207151233559860;
    pz = 210098412477272;
    vpx = -99;
    vpy = 44;
    vpz = 145;
    
    
    eqs.push(x.add(t216.mul(vx)).eq(t216.mul(vpx).add(px)));
    eqs.push(y.add(t216.mul(vy)).eq(t216.mul(vpy).add(py)));
    eqs.push(z.add(t216.mul(vz)).eq(t216.mul(vpz).add(pz)));
    px = 272808363486333;
    py = 375927723900832;
    pz = 296397865608126;
    vpx = 20;
    vpy = -113;
    vpz = -5;
    
    
    eqs.push(x.add(t217.mul(vx)).eq(t217.mul(vpx).add(px)));
    eqs.push(y.add(t217.mul(vy)).eq(t217.mul(vpy).add(py)));
    eqs.push(z.add(t217.mul(vz)).eq(t217.mul(vpz).add(pz)));
    px = 291898203879003;
    py = 420126128457744;
    pz = 308181081805622;
    vpx = -86;
    vpy = -104;
    vpz = -130;
    
    
    eqs.push(x.add(t218.mul(vx)).eq(t218.mul(vpx).add(px)));
    eqs.push(y.add(t218.mul(vy)).eq(t218.mul(vpy).add(py)));
    eqs.push(z.add(t218.mul(vz)).eq(t218.mul(vpz).add(pz)));
    px = 271920842740797;
    py = 434415607383885;
    pz = 274825235137613;
    vpx = 8;
    vpy = 14;
    vpz = 32;
    
    
    eqs.push(x.add(t219.mul(vx)).eq(t219.mul(vpx).add(px)));
    eqs.push(y.add(t219.mul(vy)).eq(t219.mul(vpy).add(py)));
    eqs.push(z.add(t219.mul(vz)).eq(t219.mul(vpz).add(pz)));
    px = 467787726572007;
    py = 345276840370890;
    pz = 452671753827425;
    vpx = -274;
    vpy = -151;
    vpz = -220;
    
    
    eqs.push(x.add(t220.mul(vx)).eq(t220.mul(vpx).add(px)));
    eqs.push(y.add(t220.mul(vy)).eq(t220.mul(vpy).add(py)));
    eqs.push(z.add(t220.mul(vz)).eq(t220.mul(vpz).add(pz)));
    px = 363813198582635;
    py = 426066883592142;
    pz = 467552682172376;
    vpx = -108;
    vpy = -277;
    vpz = -226;
    
    
    eqs.push(x.add(t221.mul(vx)).eq(t221.mul(vpx).add(px)));
    eqs.push(y.add(t221.mul(vy)).eq(t221.mul(vpy).add(py)));
    eqs.push(z.add(t221.mul(vz)).eq(t221.mul(vpz).add(pz)));
    px = 273480967034017;
    py = 426649220185590;
    pz = 335257965147938;
    vpx = 19;
    vpy = -247;
    vpz = -88;
    
    
    eqs.push(x.add(t222.mul(vx)).eq(t222.mul(vpx).add(px)));
    eqs.push(y.add(t222.mul(vy)).eq(t222.mul(vpy).add(py)));
    eqs.push(z.add(t222.mul(vz)).eq(t222.mul(vpz).add(pz)));
    px = 213281352574307;
    py = 221262331519110;
    pz = 241523110674458;
    vpx = 238;
    vpy = 569;
    vpz = 170;
    
    
    eqs.push(x.add(t223.mul(vx)).eq(t223.mul(vpx).add(px)));
    eqs.push(y.add(t223.mul(vy)).eq(t223.mul(vpy).add(py)));
    eqs.push(z.add(t223.mul(vz)).eq(t223.mul(vpz).add(pz)));
    px = 263573435700703;
    py = 441088164385924;
    pz = 175409202095378;
    vpx = 48;
    vpy = -258;
    vpz = 368;
    
    
    eqs.push(x.add(t224.mul(vx)).eq(t224.mul(vpx).add(px)));
    eqs.push(y.add(t224.mul(vy)).eq(t224.mul(vpy).add(py)));
    eqs.push(z.add(t224.mul(vz)).eq(t224.mul(vpz).add(pz)));
    px = 289945459220307;
    py = 377054201629326;
    pz = 372841561008656;
    vpx = -99;
    vpy = 223;
    vpz = -585;
    
    
    eqs.push(x.add(t225.mul(vx)).eq(t225.mul(vpx).add(px)));
    eqs.push(y.add(t225.mul(vy)).eq(t225.mul(vpy).add(py)));
    eqs.push(z.add(t225.mul(vz)).eq(t225.mul(vpz).add(pz)));
    px = 374047749163227;
    py = 125420199456462;
    pz = 169386320432288;
    vpx = -84;
    vpy = 28;
    vpz = 163;
    
    
    eqs.push(x.add(t226.mul(vx)).eq(t226.mul(vpx).add(px)));
    eqs.push(y.add(t226.mul(vy)).eq(t226.mul(vpy).add(py)));
    eqs.push(z.add(t226.mul(vz)).eq(t226.mul(vpz).add(pz)));
    px = 263769412974873;
    py = 408366368241483;
    pz = 273672589924916;
    vpx = 68;
    vpy = 20;
    vpz = 49;
    
    
    eqs.push(x.add(t227.mul(vx)).eq(t227.mul(vpx).add(px)));
    eqs.push(y.add(t227.mul(vy)).eq(t227.mul(vpy).add(py)));
    eqs.push(z.add(t227.mul(vz)).eq(t227.mul(vpz).add(pz)));
    px = 258388105998642;
    py = 392013872595165;
    pz = 296941935928523;
    vpx = 137;
    vpy = 332;
    vpz = -168;
    
    
    eqs.push(x.add(t228.mul(vx)).eq(t228.mul(vpx).add(px)));
    eqs.push(y.add(t228.mul(vy)).eq(t228.mul(vpy).add(py)));
    eqs.push(z.add(t228.mul(vz)).eq(t228.mul(vpz).add(pz)));
    px = 337052359836476;
    py = 219012376017920;
    pz = 195412320240796;
    vpx = -53;
    vpy = -41;
    vpz = 145;
    
    
    eqs.push(x.add(t229.mul(vx)).eq(t229.mul(vpx).add(px)));
    eqs.push(y.add(t229.mul(vy)).eq(t229.mul(vpy).add(py)));
    eqs.push(z.add(t229.mul(vz)).eq(t229.mul(vpz).add(pz)));
    px = 324272597155987;
    py = 281255604244580;
    pz = 91195585085663;
    vpx = -62;
    vpy = -33;
    vpz = 350;
    
    
    eqs.push(x.add(t230.mul(vx)).eq(t230.mul(vpx).add(px)));
    eqs.push(y.add(t230.mul(vy)).eq(t230.mul(vpy).add(py)));
    eqs.push(z.add(t230.mul(vz)).eq(t230.mul(vpz).add(pz)));
    px = 262437337440531;
    py = 287570235854070;
    pz = 346908645495128;
    vpx = 40;
    vpy = -21;
    vpz = -77;
    
    
    eqs.push(x.add(t231.mul(vx)).eq(t231.mul(vpx).add(px)));
    eqs.push(y.add(t231.mul(vy)).eq(t231.mul(vpy).add(py)));
    eqs.push(z.add(t231.mul(vz)).eq(t231.mul(vpz).add(pz)));
    px = 345825800459582;
    py = 209207813086330;
    pz = 293376114624943;
    vpx = -89;
    vpy = 57;
    vpz = 22;
    
    
    eqs.push(x.add(t232.mul(vx)).eq(t232.mul(vpx).add(px)));
    eqs.push(y.add(t232.mul(vy)).eq(t232.mul(vpy).add(py)));
    eqs.push(z.add(t232.mul(vz)).eq(t232.mul(vpz).add(pz)));
    px = 289000029711828;
    py = 197888339643810;
    pz = 351017414810296;
    vpx = 5;
    vpy = -31;
    vpz = -35;
    
    
    eqs.push(x.add(t233.mul(vx)).eq(t233.mul(vpx).add(px)));
    eqs.push(y.add(t233.mul(vy)).eq(t233.mul(vpy).add(py)));
    eqs.push(z.add(t233.mul(vz)).eq(t233.mul(vpz).add(pz)));
    px = 268158708478464;
    py = 197181345649512;
    pz = 322923682287035;
    vpx = 29;
    vpy = 27;
    vpz = -14;
    
    
    eqs.push(x.add(t234.mul(vx)).eq(t234.mul(vpx).add(px)));
    eqs.push(y.add(t234.mul(vy)).eq(t234.mul(vpy).add(py)));
    eqs.push(z.add(t234.mul(vz)).eq(t234.mul(vpz).add(pz)));
    px = 306374642927877;
    py = 236479711835674;
    pz = 294849372968008;
    vpx = -139;
    vpy = 711;
    vpz = -47;
    
    
    eqs.push(x.add(t235.mul(vx)).eq(t235.mul(vpx).add(px)));
    eqs.push(y.add(t235.mul(vy)).eq(t235.mul(vpy).add(py)));
    eqs.push(z.add(t235.mul(vz)).eq(t235.mul(vpz).add(pz)));
    px = 328253125942587;
    py = 134059263993870;
    pz = 322528144175408;
    vpx = -50;
    vpy = 102;
    vpz = -12;
    
    
    eqs.push(x.add(t236.mul(vx)).eq(t236.mul(vpx).add(px)));
    eqs.push(y.add(t236.mul(vy)).eq(t236.mul(vpy).add(py)));
    eqs.push(z.add(t236.mul(vz)).eq(t236.mul(vpz).add(pz)));
    px = 431481134597703;
    py = 353764567975554;
    pz = 364240330103956;
    vpx = -163;
    vpy = -202;
    vpz = -54;
    
    
    eqs.push(x.add(t237.mul(vx)).eq(t237.mul(vpx).add(px)));
    eqs.push(y.add(t237.mul(vy)).eq(t237.mul(vpy).add(py)));
    eqs.push(z.add(t237.mul(vz)).eq(t237.mul(vpz).add(pz)));
    px = 283117766261329;
    py = 340540492770048;
    pz = 303295023113732;
    vpx = -27;
    vpy = 182;
    vpz = -73;
    
    
    eqs.push(x.add(t238.mul(vx)).eq(t238.mul(vpx).add(px)));
    eqs.push(y.add(t238.mul(vy)).eq(t238.mul(vpy).add(py)));
    eqs.push(z.add(t238.mul(vz)).eq(t238.mul(vpz).add(pz)));
    px = 323910413067526;
    py = 211269851938360;
    pz = 527505690640004;
    vpx = -27;
    vpy = -81;
    vpz = -199;
    
    
    eqs.push(x.add(t239.mul(vx)).eq(t239.mul(vpx).add(px)));
    eqs.push(y.add(t239.mul(vy)).eq(t239.mul(vpy).add(py)));
    eqs.push(z.add(t239.mul(vz)).eq(t239.mul(vpz).add(pz)));
    px = 320624628251168;
    py = 104627051042668;
    pz = 352617932743968;
    vpx = -75;
    vpy = 391;
    vpz = -107;
    
    
    eqs.push(x.add(t240.mul(vx)).eq(t240.mul(vpx).add(px)));
    eqs.push(y.add(t240.mul(vy)).eq(t240.mul(vpy).add(py)));
    eqs.push(z.add(t240.mul(vz)).eq(t240.mul(vpz).add(pz)));
    px = 347175059335577;
    py = 146883914462638;
    pz = 322344509051034;
    vpx = -69;
    vpy = 61;
    vpz = -8;
    
    
    eqs.push(x.add(t241.mul(vx)).eq(t241.mul(vpx).add(px)));
    eqs.push(y.add(t241.mul(vy)).eq(t241.mul(vpy).add(py)));
    eqs.push(z.add(t241.mul(vz)).eq(t241.mul(vpz).add(pz)));
    px = 356532922902485;
    py = 428448486747668;
    pz = 367854427918216;
    vpx = -123;
    vpy = -270;
    vpz = -111;
    
    
    eqs.push(x.add(t242.mul(vx)).eq(t242.mul(vpx).add(px)));
    eqs.push(y.add(t242.mul(vy)).eq(t242.mul(vpy).add(py)));
    eqs.push(z.add(t242.mul(vz)).eq(t242.mul(vpz).add(pz)));
    px = 249748070667087;
    py = 318842894010110;
    pz = 282096299073708;
    vpx = 83;
    vpy = 69;
    vpz = 28;
    
    
    eqs.push(x.add(t243.mul(vx)).eq(t243.mul(vpx).add(px)));
    eqs.push(y.add(t243.mul(vy)).eq(t243.mul(vpy).add(py)));
    eqs.push(z.add(t243.mul(vz)).eq(t243.mul(vpz).add(pz)));
    px = 255019298626401;
    py = 274602764371060;
    pz = 289390829693362;
    vpx = 89;
    vpy = 444;
    vpz = -14;
    
    
    eqs.push(x.add(t244.mul(vx)).eq(t244.mul(vpx).add(px)));
    eqs.push(y.add(t244.mul(vy)).eq(t244.mul(vpy).add(py)));
    eqs.push(z.add(t244.mul(vz)).eq(t244.mul(vpz).add(pz)));
    px = 272016051241871;
    py = 250992712372226;
    pz = 253555913559440;
    vpx = 24;
    vpy = -69;
    vpz = 77;
    
    
    eqs.push(x.add(t245.mul(vx)).eq(t245.mul(vpx).add(px)));
    eqs.push(y.add(t245.mul(vy)).eq(t245.mul(vpy).add(py)));
    eqs.push(z.add(t245.mul(vz)).eq(t245.mul(vpz).add(pz)));
    px = 514434578625654;
    py = 249800472915633;
    pz = 557255782239715;
    vpx = -217;
    vpy = -118;
    vpz = -230;
    
    
    eqs.push(x.add(t246.mul(vx)).eq(t246.mul(vpx).add(px)));
    eqs.push(y.add(t246.mul(vy)).eq(t246.mul(vpy).add(py)));
    eqs.push(z.add(t246.mul(vz)).eq(t246.mul(vpz).add(pz)));
    px = 268165768443117;
    py = 406494246376227;
    pz = 482328624540068;
    vpx = 36;
    vpy = -74;
    vpz = -887;
    
    
    eqs.push(x.add(t247.mul(vx)).eq(t247.mul(vpx).add(px)));
    eqs.push(y.add(t247.mul(vy)).eq(t247.mul(vpy).add(py)));
    eqs.push(z.add(t247.mul(vz)).eq(t247.mul(vpz).add(pz)));
    px = 339850866338441;
    py = 442648816097471;
    pz = 122168564559253;
    vpx = -96;
    vpy = -294;
    vpz = 318;
    
    
    eqs.push(x.add(t248.mul(vx)).eq(t248.mul(vpx).add(px)));
    eqs.push(y.add(t248.mul(vy)).eq(t248.mul(vpy).add(py)));
    eqs.push(z.add(t248.mul(vz)).eq(t248.mul(vpz).add(pz)));
    px = 264492045152224;
    py = 92845786811750;
    pz = 257027076170697;
    vpx = 33;
    vpy = 109;
    vpz = 72;
    
    
    eqs.push(x.add(t249.mul(vx)).eq(t249.mul(vpx).add(px)));
    eqs.push(y.add(t249.mul(vy)).eq(t249.mul(vpy).add(py)));
    eqs.push(z.add(t249.mul(vz)).eq(t249.mul(vpz).add(pz)));
    px = 226970821111617;
    py = 357041090575470;
    pz = 293897795256878;
    vpx = 153;
    vpy = -19;
    vpz = -8;
    
    
    eqs.push(x.add(t250.mul(vx)).eq(t250.mul(vpx).add(px)));
    eqs.push(y.add(t250.mul(vy)).eq(t250.mul(vpy).add(py)));
    eqs.push(z.add(t250.mul(vz)).eq(t250.mul(vpz).add(pz)));
    px = 342089927413667;
    py = 411997765624670;
    pz = 342682648601738;
    vpx = -218;
    vpy = -155;
    vpz = -184;
    
    
    eqs.push(x.add(t251.mul(vx)).eq(t251.mul(vpx).add(px)));
    eqs.push(y.add(t251.mul(vy)).eq(t251.mul(vpy).add(py)));
    eqs.push(z.add(t251.mul(vz)).eq(t251.mul(vpz).add(pz)));
    px = 250668161400931;
    py = 243931735576206;
    pz = 92707563709056;
    vpx = 82;
    vpy = 293;
    vpz = 565;
    
    
    eqs.push(x.add(t252.mul(vx)).eq(t252.mul(vpx).add(px)));
    eqs.push(y.add(t252.mul(vy)).eq(t252.mul(vpy).add(py)));
    eqs.push(z.add(t252.mul(vz)).eq(t252.mul(vpz).add(pz)));
    px = 351411042914937;
    py = 361276554470210;
    pz = 440666989610408;
    vpx = -148;
    vpy = -111;
    vpz = -307;
    
    
    eqs.push(x.add(t253.mul(vx)).eq(t253.mul(vpx).add(px)));
    eqs.push(y.add(t253.mul(vy)).eq(t253.mul(vpy).add(py)));
    eqs.push(z.add(t253.mul(vz)).eq(t253.mul(vpz).add(pz)));
    px = 333282548167675;
    py = 191427623038494;
    pz = 368806658573632;
    vpx = -62;
    vpy = 50;
    vpz = -81;
    
    
    eqs.push(x.add(t254.mul(vx)).eq(t254.mul(vpx).add(px)));
    eqs.push(y.add(t254.mul(vy)).eq(t254.mul(vpy).add(py)));
    eqs.push(z.add(t254.mul(vz)).eq(t254.mul(vpz).add(pz)));
    px = 328331873426359;
    py = 328640111768590;
    pz = 542478990963640;
    vpx = -137;
    vpy = 49;
    vpz = -705;
    
    
    eqs.push(x.add(t255.mul(vx)).eq(t255.mul(vpx).add(px)));
    eqs.push(y.add(t255.mul(vy)).eq(t255.mul(vpy).add(py)));
    eqs.push(z.add(t255.mul(vz)).eq(t255.mul(vpz).add(pz)));
    px = 338578447617845;
    py = 517862026025949;
    pz = 243246185117704;
    vpx = -212;
    vpy = -520;
    vpz = 157;
    
    
    eqs.push(x.add(t256.mul(vx)).eq(t256.mul(vpx).add(px)));
    eqs.push(y.add(t256.mul(vy)).eq(t256.mul(vpy).add(py)));
    eqs.push(z.add(t256.mul(vz)).eq(t256.mul(vpz).add(pz)));
    px = 286592031513947;
    py = 354871682324185;
    pz = 553501021727038;
    vpx = -6;
    vpy = -116;
    vpz = -501;
    
    
    eqs.push(x.add(t257.mul(vx)).eq(t257.mul(vpx).add(px)));
    eqs.push(y.add(t257.mul(vy)).eq(t257.mul(vpy).add(py)));
    eqs.push(z.add(t257.mul(vz)).eq(t257.mul(vpz).add(pz)));
    px = 309625408577591;
    py = 132907059207079;
    pz = 412141320310124;
    vpx = -18;
    vpy = 40;
    vpz = -103;
    
    
    eqs.push(x.add(t258.mul(vx)).eq(t258.mul(vpx).add(px)));
    eqs.push(y.add(t258.mul(vy)).eq(t258.mul(vpy).add(py)));
    eqs.push(z.add(t258.mul(vz)).eq(t258.mul(vpz).add(pz)));
    px = 270392223533307;
    py = 270952402587212;
    pz = 225477260964402;
    vpx = 26;
    vpy = 208;
    vpz = 186;
    
    
    eqs.push(x.add(t259.mul(vx)).eq(t259.mul(vpx).add(px)));
    eqs.push(y.add(t259.mul(vy)).eq(t259.mul(vpy).add(py)));
    eqs.push(z.add(t259.mul(vz)).eq(t259.mul(vpz).add(pz)));
    px = 341270768940030;
    py = 247637799886236;
    pz = 298503071111225;
    vpx = -77;
    vpy = -17;
    vpz = 16;
    
    
    eqs.push(x.add(t260.mul(vx)).eq(t260.mul(vpx).add(px)));
    eqs.push(y.add(t260.mul(vy)).eq(t260.mul(vpy).add(py)));
    eqs.push(z.add(t260.mul(vz)).eq(t260.mul(vpz).add(pz)));
    px = 221649641193999;
    py = 329672040761013;
    pz = 359278722508676;
    vpx = 78;
    vpy = -188;
    vpz = -39;
    
    
    eqs.push(x.add(t261.mul(vx)).eq(t261.mul(vpx).add(px)));
    eqs.push(y.add(t261.mul(vy)).eq(t261.mul(vpy).add(py)));
    eqs.push(z.add(t261.mul(vz)).eq(t261.mul(vpz).add(pz)));
    px = 272098601220282;
    py = 429324068810460;
    pz = 278292238945208;
    vpx = 13;
    vpy = -69;
    vpz = 13;
    
    
    eqs.push(x.add(t262.mul(vx)).eq(t262.mul(vpx).add(px)));
    eqs.push(y.add(t262.mul(vy)).eq(t262.mul(vpy).add(py)));
    eqs.push(z.add(t262.mul(vz)).eq(t262.mul(vpz).add(pz)));
    px = 313181380730475;
    py = 334213182994734;
    pz = 337934011612880;
    vpx = -125;
    vpy = 126;
    vpz = -176;
    
    
    eqs.push(x.add(t263.mul(vx)).eq(t263.mul(vpx).add(px)));
    eqs.push(y.add(t263.mul(vy)).eq(t263.mul(vpy).add(py)));
    eqs.push(z.add(t263.mul(vz)).eq(t263.mul(vpz).add(pz)));
    px = 280003362379015;
    py = 347368777219750;
    pz = 416197229921964;
    vpx = 7;
    vpy = -101;
    vpz = -230;
    
    
    eqs.push(x.add(t264.mul(vx)).eq(t264.mul(vpx).add(px)));
    eqs.push(y.add(t264.mul(vy)).eq(t264.mul(vpy).add(py)));
    eqs.push(z.add(t264.mul(vz)).eq(t264.mul(vpz).add(pz)));
    px = 241813862847152;
    py = 159150469738801;
    pz = 361226501893772;
    vpx = 61;
    vpy = 42;
    vpz = -55;
    
    
    eqs.push(x.add(t265.mul(vx)).eq(t265.mul(vpx).add(px)));
    eqs.push(y.add(t265.mul(vy)).eq(t265.mul(vpy).add(py)));
    eqs.push(z.add(t265.mul(vz)).eq(t265.mul(vpz).add(pz)));
    px = 347694566155717;
    py = 421001322372236;
    pz = 370259368478866;
    vpx = -269;
    vpy = -168;
    vpz = -318;
    
    
    eqs.push(x.add(t266.mul(vx)).eq(t266.mul(vpx).add(px)));
    eqs.push(y.add(t266.mul(vy)).eq(t266.mul(vpy).add(py)));
    eqs.push(z.add(t266.mul(vz)).eq(t266.mul(vpz).add(pz)));
    px = 284902985674235;
    py = 243491987349438;
    pz = 349863527984768;
    vpx = 9;
    vpy = -73;
    vpz = -37;
    
    
    eqs.push(x.add(t267.mul(vx)).eq(t267.mul(vpx).add(px)));
    eqs.push(y.add(t267.mul(vy)).eq(t267.mul(vpy).add(py)));
    eqs.push(z.add(t267.mul(vz)).eq(t267.mul(vpz).add(pz)));
    px = 240539819926125;
    py = 53434954156942;
    pz = 140619645445734;
    vpx = 65;
    vpy = 205;
    vpz = 226;
    
    
    eqs.push(x.add(t268.mul(vx)).eq(t268.mul(vpx).add(px)));
    eqs.push(y.add(t268.mul(vy)).eq(t268.mul(vpy).add(py)));
    eqs.push(z.add(t268.mul(vz)).eq(t268.mul(vpz).add(pz)));
    px = 379018120747357;
    py = 234456327547615;
    pz = 333071947154183;
    vpx = -164;
    vpy = 70;
    vpz = -52;
    
    
    eqs.push(x.add(t269.mul(vx)).eq(t269.mul(vpx).add(px)));
    eqs.push(y.add(t269.mul(vy)).eq(t269.mul(vpy).add(py)));
    eqs.push(z.add(t269.mul(vz)).eq(t269.mul(vpz).add(pz)));
    px = 317771834387082;
    py = 438103541732610;
    pz = 439083905720933;
    vpx = -85;
    vpy = -271;
    vpz = -336;
    
    
    eqs.push(x.add(t270.mul(vx)).eq(t270.mul(vpx).add(px)));
    eqs.push(y.add(t270.mul(vy)).eq(t270.mul(vpy).add(py)));
    eqs.push(z.add(t270.mul(vz)).eq(t270.mul(vpz).add(pz)));
    px = 269556676003839;
    py = 348826356892260;
    pz = 305628199711460;
    vpx = 28;
    vpy = -56;
    vpz = -25;
    
    
    eqs.push(x.add(t271.mul(vx)).eq(t271.mul(vpx).add(px)));
    eqs.push(y.add(t271.mul(vy)).eq(t271.mul(vpy).add(py)));
    eqs.push(z.add(t271.mul(vz)).eq(t271.mul(vpz).add(pz)));
    px = 331741677987807;
    py = 537333487539510;
    pz = 435437460794708;
    vpx = -144;
    vpy = -535;
    vpz = -397;
    
    
    eqs.push(x.add(t272.mul(vx)).eq(t272.mul(vpx).add(px)));
    eqs.push(y.add(t272.mul(vy)).eq(t272.mul(vpy).add(py)));
    eqs.push(z.add(t272.mul(vz)).eq(t272.mul(vpz).add(pz)));
    px = 376406942380642;
    py = 278311657140166;
    pz = 259235278026276;
    vpx = -189;
    vpy = 45;
    vpz = 81;
    
    
    eqs.push(x.add(t273.mul(vx)).eq(t273.mul(vpx).add(px)));
    eqs.push(y.add(t273.mul(vy)).eq(t273.mul(vpy).add(py)));
    eqs.push(z.add(t273.mul(vz)).eq(t273.mul(vpz).add(pz)));
    px = 304404468922375;
    py = 260140849938953;
    pz = 402588486588217;
    vpx = -42;
    vpy = 76;
    vpz = -206;
    
    
    eqs.push(x.add(t274.mul(vx)).eq(t274.mul(vpx).add(px)));
    eqs.push(y.add(t274.mul(vy)).eq(t274.mul(vpy).add(py)));
    eqs.push(z.add(t274.mul(vz)).eq(t274.mul(vpz).add(pz)));
    px = 279180801330347;
    py = 349023201942738;
    pz = 119900877948786;
    vpx = -14;
    vpy = 191;
    vpz = 750;
    
    
    eqs.push(x.add(t275.mul(vx)).eq(t275.mul(vpx).add(px)));
    eqs.push(y.add(t275.mul(vy)).eq(t275.mul(vpy).add(py)));
    eqs.push(z.add(t275.mul(vz)).eq(t275.mul(vpz).add(pz)));
    px = 188333061901926;
    py = 318660068603285;
    pz = 244031031344043;
    vpx = 125;
    vpy = -156;
    vpz = 88;
    
    
    eqs.push(x.add(t276.mul(vx)).eq(t276.mul(vpx).add(px)));
    eqs.push(y.add(t276.mul(vy)).eq(t276.mul(vpy).add(py)));
    eqs.push(z.add(t276.mul(vz)).eq(t276.mul(vpz).add(pz)));
    px = 288725944455068;
    py = 467163692472072;
    pz = 295016758944040;
    vpx = -261;
    vpy = -385;
    vpz = -291;
    
    
    eqs.push(x.add(t277.mul(vx)).eq(t277.mul(vpx).add(px)));
    eqs.push(y.add(t277.mul(vy)).eq(t277.mul(vpy).add(py)));
    eqs.push(z.add(t277.mul(vz)).eq(t277.mul(vpz).add(pz)));
    px = 146106098497872;
    py = 69764788293913;
    pz = 174366195276499;
    vpx = 191;
    vpy = 192;
    vpz = 184;
    
    
    eqs.push(x.add(t278.mul(vx)).eq(t278.mul(vpx).add(px)));
    eqs.push(y.add(t278.mul(vy)).eq(t278.mul(vpy).add(py)));
    eqs.push(z.add(t278.mul(vz)).eq(t278.mul(vpz).add(pz)));
    px = 223140068566361;
    py = 239780016481192;
    pz = 175455873847863;
    vpx = 72;
    vpy = -113;
    vpz = 148;
    
    
    eqs.push(x.add(t279.mul(vx)).eq(t279.mul(vpx).add(px)));
    eqs.push(y.add(t279.mul(vy)).eq(t279.mul(vpy).add(py)));
    eqs.push(z.add(t279.mul(vz)).eq(t279.mul(vpz).add(pz)));
    px = 271599283420167;
    py = 328121081570170;
    pz = 313880705567638;
    vpx = 20;
    vpy = 343;
    vpz = -150;
    
    
    eqs.push(x.add(t280.mul(vx)).eq(t280.mul(vpx).add(px)));
    eqs.push(y.add(t280.mul(vy)).eq(t280.mul(vpy).add(py)));
    eqs.push(z.add(t280.mul(vz)).eq(t280.mul(vpz).add(pz)));
    px = 299714040995601;
    py = 312916223816598;
    pz = 194152194318417;
    vpx = -16;
    vpy = -115;
    vpz = 166;
    
    
    eqs.push(x.add(t281.mul(vx)).eq(t281.mul(vpx).add(px)));
    eqs.push(y.add(t281.mul(vy)).eq(t281.mul(vpy).add(py)));
    eqs.push(z.add(t281.mul(vz)).eq(t281.mul(vpz).add(pz)));
    px = 278675764379679;
    py = 171531065067534;
    pz = 395035811254232;
    vpx = 15;
    vpy = 57;
    vpz = -109;
    
    
    eqs.push(x.add(t282.mul(vx)).eq(t282.mul(vpx).add(px)));
    eqs.push(y.add(t282.mul(vy)).eq(t282.mul(vpy).add(py)));
    eqs.push(z.add(t282.mul(vz)).eq(t282.mul(vpz).add(pz)));
    px = 215107541859009;
    py = 109571688570346;
    pz = 196925255351218;
    vpx = 95;
    vpy = 111;
    vpz = 148;
    
    
    eqs.push(x.add(t283.mul(vx)).eq(t283.mul(vpx).add(px)));
    eqs.push(y.add(t283.mul(vy)).eq(t283.mul(vpy).add(py)));
    eqs.push(z.add(t283.mul(vz)).eq(t283.mul(vpz).add(pz)));
    px = 216241220884565;
    py = 173439581483993;
    pz = 339156442319393;
    vpx = 112;
    vpy = 130;
    vpz = -52;
    
    
    eqs.push(x.add(t284.mul(vx)).eq(t284.mul(vpx).add(px)));
    eqs.push(y.add(t284.mul(vy)).eq(t284.mul(vpy).add(py)));
    eqs.push(z.add(t284.mul(vz)).eq(t284.mul(vpz).add(pz)));
    px = 304209814619857;
    py = 196446083606860;
    pz = 264860170799333;
    vpx = -36;
    vpy = 159;
    vpz = 68;
    
    
    eqs.push(x.add(t285.mul(vx)).eq(t285.mul(vpx).add(px)));
    eqs.push(y.add(t285.mul(vy)).eq(t285.mul(vpy).add(py)));
    eqs.push(z.add(t285.mul(vz)).eq(t285.mul(vpz).add(pz)));
    px = 267658514050651;
    py = 431763912615568;
    pz = 268257854467560;
    vpx = 58;
    vpy = 43;
    vpz = 109;
    
    
    eqs.push(x.add(t286.mul(vx)).eq(t286.mul(vpx).add(px)));
    eqs.push(y.add(t286.mul(vy)).eq(t286.mul(vpy).add(py)));
    eqs.push(z.add(t286.mul(vz)).eq(t286.mul(vpz).add(pz)));
    px = 315708192092025;
    py = 260523186398568;
    pz = 509854326917444;
    vpx = -67;
    vpy = 86;
    vpz = -433;
    
    
    eqs.push(x.add(t287.mul(vx)).eq(t287.mul(vpx).add(px)));
    eqs.push(y.add(t287.mul(vy)).eq(t287.mul(vpy).add(py)));
    eqs.push(z.add(t287.mul(vz)).eq(t287.mul(vpz).add(pz)));
    px = 331751357074977;
    py = 515528521629298;
    pz = 145551201925627;
    vpx = -64;
    vpy = -407;
    vpz = 240;
    
    
    eqs.push(x.add(t288.mul(vx)).eq(t288.mul(vpx).add(px)));
    eqs.push(y.add(t288.mul(vy)).eq(t288.mul(vpy).add(py)));
    eqs.push(z.add(t288.mul(vz)).eq(t288.mul(vpz).add(pz)));
    px = 400296648324294;
    py = 388920685496269;
    pz = 371454289085683;
    vpx = -205;
    vpy = -198;
    vpz = -122;
    
    
    eqs.push(x.add(t289.mul(vx)).eq(t289.mul(vpx).add(px)));
    eqs.push(y.add(t289.mul(vy)).eq(t289.mul(vpy).add(py)));
    eqs.push(z.add(t289.mul(vz)).eq(t289.mul(vpz).add(pz)));
    px = 162546432374355;
    py = 299744520942234;
    pz = 221870118624542;
    vpx = 222;
    vpy = -33;
    vpz = 146;
    
    
    eqs.push(x.add(t290.mul(vx)).eq(t290.mul(vpx).add(px)));
    eqs.push(y.add(t290.mul(vy)).eq(t290.mul(vpy).add(py)));
    eqs.push(z.add(t290.mul(vz)).eq(t290.mul(vpz).add(pz)));
    px = 318167909934022;
    py = 328472199152086;
    pz = 112074533419799;
    vpx = -39;
    vpy = -147;
    vpz = 272;
    
    
    eqs.push(x.add(t291.mul(vx)).eq(t291.mul(vpx).add(px)));
    eqs.push(y.add(t291.mul(vy)).eq(t291.mul(vpy).add(py)));
    eqs.push(z.add(t291.mul(vz)).eq(t291.mul(vpz).add(pz)));
    px = 204650693234927;
    py = 198152960594075;
    pz = 188269872782718;
    vpx = 102;
    vpy = -24;
    vpz = 151;
    
    
    eqs.push(x.add(t292.mul(vx)).eq(t292.mul(vpx).add(px)));
    eqs.push(y.add(t292.mul(vy)).eq(t292.mul(vpy).add(py)));
    eqs.push(z.add(t292.mul(vz)).eq(t292.mul(vpz).add(pz)));
    px = 234473437726867;
    py = 324086186101470;
    pz = 313007819001768;
    vpx = 97;
    vpy = -55;
    vpz = -26;
    
    
    eqs.push(x.add(t293.mul(vx)).eq(t293.mul(vpx).add(px)));
    eqs.push(y.add(t293.mul(vy)).eq(t293.mul(vpy).add(py)));
    eqs.push(z.add(t293.mul(vz)).eq(t293.mul(vpz).add(pz)));
    px = 208245832758657;
    py = 180504161378205;
    pz = 257061345577298;
    vpx = 96;
    vpy = -12;
    vpz = 71;
    
    
    eqs.push(x.add(t294.mul(vx)).eq(t294.mul(vpx).add(px)));
    eqs.push(y.add(t294.mul(vy)).eq(t294.mul(vpy).add(py)));
    eqs.push(z.add(t294.mul(vz)).eq(t294.mul(vpz).add(pz)));
    px = 293473224944187;
    py = 376336065424350;
    pz = 272052660287456;
    vpx = -44;
    vpy = -66;
    vpz = 56;
    
    
    eqs.push(x.add(t295.mul(vx)).eq(t295.mul(vpx).add(px)));
    eqs.push(y.add(t295.mul(vy)).eq(t295.mul(vpy).add(py)));
    eqs.push(z.add(t295.mul(vz)).eq(t295.mul(vpz).add(pz)));
    px = 288576903408210;
    py = 474350464385091;
    pz = 241933462879984;
    vpx = -133;
    vpy = -424;
    vpz = 325;
    
    
    eqs.push(x.add(t296.mul(vx)).eq(t296.mul(vpx).add(px)));
    eqs.push(y.add(t296.mul(vy)).eq(t296.mul(vpy).add(py)));
    eqs.push(z.add(t296.mul(vz)).eq(t296.mul(vpz).add(pz)));
    px = 335647092276321;
    py = 359684641299450;
    pz = 379435653795383;
    vpx = -112;
    vpy = -111;
    vpz = -172;
    
    
    eqs.push(x.add(t297.mul(vx)).eq(t297.mul(vpx).add(px)));
    eqs.push(y.add(t297.mul(vy)).eq(t297.mul(vpy).add(py)));
    eqs.push(z.add(t297.mul(vz)).eq(t297.mul(vpz).add(pz)));
    px = 343665260864859;
    py = 292743721753822;
    pz = 358527056282352;
    vpx = -70;
    vpy = -107;
    vpz = -59;
    
    
    eqs.push(x.add(t298.mul(vx)).eq(t298.mul(vpx).add(px)));
    eqs.push(y.add(t298.mul(vy)).eq(t298.mul(vpy).add(py)));
    eqs.push(z.add(t298.mul(vz)).eq(t298.mul(vpz).add(pz)));
    px = 401753783270176;
    py = 450367245750257;
    pz = 441634222195088;
    vpx = -161;
    vpy = -312;
    vpz = -187;
    
    
    eqs.push(x.add(t299.mul(vx)).eq(t299.mul(vpx).add(px)));
    eqs.push(y.add(t299.mul(vy)).eq(t299.mul(vpy).add(py)));
    eqs.push(z.add(t299.mul(vz)).eq(t299.mul(vpz).add(pz)));
    
    const model = await Z3.solve(...eqs);
    
    console.log(model.eval(x).toString());
    console.log(model.eval(y).toString());
    console.log(model.eval(z).toString());
    
    console.log(model.eval(x.add(y).add(z)).toString());
    }
    
    execute();
    • [^] # Re: J'ai aussi utilisé le Z3 theorem prover.

      Posté par  . Évalué à 1. Dernière modification le 28 décembre 2023 à 23:31.

      Je viens de voir que j'avais oublié de corriger le problème de séparation des bloques

      `eqs.push(x.add(t298.mul(vx)).eq(t298.mul(vpx).add(px)));
      eqs.push(y.add(t298.mul(vy)).eq(t298.mul(vpy).add(py)));
      eqs.push(z.add(t298.mul(vz)).eq(t298.mul(vpz).add(pz)));
      px = 401753783270176;
      py = 450367245750257;
      pz = 441634222195088;
      vpx = -161;
      vpy = -312;
      vpz = -187;
      
      
      eqs.push(x.add(t299.mul(vx)).eq(t299.mul(vpx).add(px)));
      eqs.push(y.add(t299.mul(vy)).eq(t299.mul(vpy).add(py)));
      eqs.push(z.add(t299.mul(vz)).eq(t299.mul(vpz).add(pz)));

      il faut le lire. il manque un saut ligne est un commentaire.

      `eqs.push(x.add(t298.mul(vx)).eq(t298.mul(vpx).add(px)));
      eqs.push(y.add(t298.mul(vy)).eq(t298.mul(vpy).add(py)));
      eqs.push(z.add(t298.mul(vz)).eq(t298.mul(vpz).add(pz)));
      
      // Hailstone 299
      px = 401753783270176;
      py = 450367245750257;
      pz = 441634222195088;
      vpx = -161;
      vpy = -312;
      vpz = -187;
      eqs.push(x.add(t299.mul(vx)).eq(t299.mul(vpx).add(px)));
      eqs.push(y.add(t299.mul(vy)).eq(t299.mul(vpy).add(py)));
      eqs.push(z.add(t299.mul(vz)).eq(t299.mul(vpz).add(pz)));

      (En espérant que c'est plus clair)

    • [^] # Re: J'ai aussi utilisé le Z3 theorem prover.

      Posté par  (site web personnel) . Évalué à 3.

      Un code de cette longueur, ça aurait valu la peine de le mettre ailleurs, là ça nous fait une page terriblement longue à parcourir.

  • # Pas de Z3, mais au moins Z^3 neurones grillés

    Posté par  (Mastodon) . Évalué à 2.

    C'est celui qui m'a le plus gonflé sur téléphone.
    Pas la partie 1 bien sûr, encore expédiée assez vite dès que je m'y suis mis (c'est à dire une fois le jour précédent terminé).

    La partie 2.
    Où les données de test laissent entrevoir plein de simplifications qui ne fonctionnent pas avec le vrai problème.
    Et une résolution finale qui ne fonctionne pas sur les données de test !

    J'ai assez modélisé mes trajectoires de grêlon, pour faire des opérations en masse, je cherchais des simplifications, des translations, pivots, etc, mais je n'ai jamais réussi à résoudre autre chose que les données de test comme ça : à chaque fois il fallait tester au moins un paramètre final, et le plus complexe à tester a au final une valeur de 57 milliard et quelques au minimum, donc on ne va pas l'atteindre comme ça, en cherchant…
    C'est le temps nécessaire à notre caillou pour atteindre un élément.
    On tombe pas dessus par hasard.
    Dans les données de test, c'est 1, ça simplifie grandement le problème.

    En fait, il faut comprendre le problème.
    On choisit un point d'origine et une trajectoire : Traj(x=393358484426865.0, y=319768494554521.0, z=158856878271783.0, dx=-242, dy=-49, dz=209)
    À partir de là on choisit des entiers, grands, ça va de quelques dizaines de milliards à probablement mille milliards (j'ai un 943 538 374 225 pour un grêlon), ça définit des points de départ sur notre trajectoire.
    De chacun de ces points on choisit une direction, et on fait reculer notre grêlon du temps nécessaire à atteindre le point en question.
    Voilà, on a notre problème posé, on oublie la trajectoire initiale, il faut la retrouver.
    Facile à construire, pas simple à démêler…

    Et franchement, il faut trouver des simplifications.
    Et là on les trouve avec une première constatation : ce qui se passe en x, y et z est presque entièrement décorrélé, pour trouver dx, dy ou dz, on n'a besoin de se concentrer que sur la coordonnée en question. Après on fera une corrélation sur l'écart en temps entre deux grêlons, qu'on peut connaître pour dx, dy ou dz, et qui sera donc égale pour les autres, et permet de faire une triangulation.
    Et une seconde constatation, sur un axe on a des grêlons parallèles, c'est à dire qui ont le même dx, le même dy ou le même dz.
    Et ça va nous aider.
    C'est même la seule simplification que j'ai trouvé pour réussir à résoudre ce problème.

    Parce que si entre deux grêlons on a un dx identique, ça veut dire que l'écart en x entre ces deux grêlon est une constante.
    Et donc qu'on parcourt cette écart avec un nombre entier d'étapes, chacune d'un nombre entier de décalages.
    Donc pour deux grêlons a et b parallèles en x, donc a.dx==b.dx, on a que l'écart en x (a.x - b.x) est divisible par r.dx-a.dx ou r est notre trajectoire résultat à trouver. On cherche r.dx.
    Et ben on va chercher les diviseurs de a.x - b.x, sans connaître le sens on va tous les prendre en positif ou négatif, on ajoute a.dx, et on a des valeurs possibles de r.dx.
    Et on cherche les valeurs communes entre tous les éléments parallèles en x, on aura réduit drastiquement nos possibilités de r.dx.

    En pratique, si on n'oublie pas de considérer les diviseurs en négatif ou positif (parce qu'on ne sait pas dans quel sens on va, on a juste deux grêlons au pif), on va trouver une seul valeur pour dx, dy et dz.
    On a la direction parfaite de notre caillou !
    Ça aurait pu rater, on aurait pu avoir des choix et devoir tester parmi ces choix lesquels seraient les bons, mais on sent que même si on en avait eu plusieurs, ça n'aurait pas été trop explosif, et si l'algo pour finir le boulot est pas trop pourri on pouvait tout tester.

    Là, suite à une erreur de ma part, j'ai aussi pondu un algorithme capable de calculer dy si on connaît dx et dz !
    Sauf que ça foirait, à cause de mon erreur, mais j'ai corrigé et poursuivi, en pratique je calcule la solution pour tous les grêlons parallèles deux à deux en x, et je valide cette solution en montrant qu'ils donnent tous le même résultat. Ça m'a permis de débugger et d'être absolument certain d'avoir le bon résultat au bout du compte.

    En pratique, quand on a dx, dy, et dz, il suffit de prendre deux grêlons parallèles selon n'importe quel axe, et on va avoir la solution.
    On calcule le nombre d'étapes (microsecondes) pour que notre caillou passe de l'un à l'autre, ce qui est facile si on a compris l'algorithme qui a permit de trouver les dx, dy et dz : on divise l'écart en x a.x-b.x par r.dx-a.dx qui sont connus.
    Sachant le temps séparant ces deux chocs, on peut calculer l'écart en y ou en z, constaté parce que nos grêlons ne sont pas parallèles en y ou z, et ça va nous permettre de savoir de combien d'étapes dans le temps il faut remonter pour combler cet écart, et faire en sorte de bien percuter les deux grêlons, en x, y et z.

    En pratique mon algorithme, que je n'ai pas simplifié, calcule dy à partir de la connaissance de dx et dz sur des grêlons parallèles en z, c'est pas trop compliqué une fois qu'on a le nombre d'étapes à remonter dans le temps, et on valide déjà qu'on trouve pour tous la bonne valeur de dy. Puis on fait remonter effectivement dans le temps notre caillou depuis sa percussion avec a pour trouver un point de départ.
    J'ai juste validé que r.x était identique pour tous, mais tant que ce n'était pas le cas c'était que j'avais une erreur dans mes formules.

    Les maths sont simples, mais prise de tête et il faut bien se torturer les neurones.

    Au final je fais bien trop de calculs, qui me donnent tous le même résultat, heureusement, et ça prend moins d'une seconde malgré tout.

    Voici donc le code, avec trop de méthodes inutilisées dans mes Trajectoires, et des noms de variable bien trop peu lisibles.
    Heureusement le code n'est pas trop complexe, et reste a peu près lisible.
    Il y a un hack au milieu pour les données de test, puisqu'on n'a pas assez de parallèles pour trouver dx, dy et dz, je force les valeurs, connues, pour valider la seconde partie de l'algorithme.
    Mais ça aurait pu faire l'objet d'un développement intéressant pour valider sur un ensemble de valeurs possible, si on n'avait pas eu un dx, dy et dz unique à l'issue de la première partie.
    Rendant nécessaire de tester plusieurs cas et de vérifier qu'on ait bien un même résultat. Ça aurait été immonde à débugger par contre…
    J'ai tout de même utilisé sympy pour les diviseurs, pour le coup c'était quand même plus simple que de coder une fonction moi-même.

    from sys import stdin
    from dataclasses import dataclass
    from functools import total_ordering
    from sympy import divisors
    
    test = False
    data = stdin.read().strip().splitlines()
    ex1 = ex2 = 0
    m0, m1 = (7, 27) if test else (200000000000000, 400000000000000)
    
    
    @total_ordering
    @dataclass(frozen=True)
    class Traj:
      x: int = 0
      y: int = 0
      z: int = 0
      dx: int = 0
      dy: int = 0
      dz: int = 0
      @property
      def a(self):
        return self.dy / self.dx
      @property
      def b(self):
        return self.y - self.x * self.dy / self.dx
      def __mul__(self, other):
        # t = (x-x0)/dx
        # y = y0+dy*(x-x0)/dx = a*x+b
        # b = y0-x0*dy/dx
        # a = dy/dx
        # x = (B-b)/(a-A)
        if self.a == other.a:
          return 0, 0, -1, -1
        x = (other.b - self.b) / (self.a - other.a)
        y = self.a * x + self.b
        return x, y, (x - self.x) / self.dx, (x - other.x) / other.dx
      def __lt__(self, other):
        return self.tzero < other.tzero
      def __add__(self, n):
        return Traj(
          self.x + self.dx * n,
          self.y + self.dy * n,
          self.z + self.dz * n,
          self.dx, self.dy, self.dz)
      def __sub__(self, other):
        return Traj(
          self.x - other.x,
          self.y - other.y,
          self.z - other.z,
          self.dx, self.dy, self.dz)
      def __truediv__(self, other):
        return Traj(
          self.x, self.y, self.z,
          self.dx - other.dx,
          self.dy - other.dy,
          self.dz - other.dz)
      def __neg__(self):
        return Traj(-self.x, -self.y, -self.z, -self.dx, -self.dy, -self.dz)
      @property
      def tzero(self):
        return -self.z / self.dz if self.dz else 0
    
    # data
    D = [
      Traj(*(int(x) for x in line.replace(" ", "").replace("@", ",").split(",")))
      for line in data
    ]
    # ex1
    for i, d in enumerate(D):
      for f in D[i + 1:]:
        x, y, t, tt = d * f
        if x >= m0 and x <= m1 and y >= m0 and y <= m1 and t > 0 and tt > 0:
          ex1 += 1
    
    # ex2
    def correlate(trucs):
      dds = [d[0] for d in trucs]
      dds = {d for d in dds if dds.count(d) > 1}
      X = {
        d: sorted(x for dx, x in trucs if d == dx)
        for d in dds
      }
      Z = {
        dx: {
          s * di + dx
          for x1 in x
          for di in divisors(x0 - x1)
          for s in [1, -1]
        }
        for dx, (*x, x0) in X.items()
      }
      return set.intersection(*Z.values())
    
    def recorrelate(trucs, dx, dy, dz):
      dds = [d.dz for d in trucs]
      dds = {d for d in dds if dds.count(d) > 1}
      X = {
        d: sorted(
          (_ for _ in trucs if _.dz == d),
          key=lambda f: f.z
        )
        for d in dds
      }
      Y = [
        {
          "dy": (x0.y - x1.y - step0 * (x0.dy - x1.dy)) / step + x0.dy,
          "x0": x0,
          "x1": x1,
          "step": step,
          "xp": xp,
          "step0": step0,
          "src": Traj(
            x1.x - x1.dx * step0,
            x1.y - x1.dy * step0,
            x1.z - x1.dz * step0,
            dx, dy, dz) + step0,
        }
        for _, (*x, x0) in X.items()
        for x1 in x
        for step in [(x0.z - x1.z) / (dz - x0.dz)]
        if step
        for xp in [(x0.x - x1.x) - (dx - x0.dx) * step]
        for step0 in [xp / (x0.dx - x1.dx)]
      ]
      return Y, {h["dy"] for h in Y}, {h["src"].x for h in Y}
    
    
    PDX = correlate([(d.dx, d.x) for d in D])
    PDY = correlate([(d.dy, d.y) for d in D])
    PDZ = correlate([(d.dz, d.z) for d in D])
    
    print(PDX, PDY, PDZ)
    PDX, PDY, PDZ = (-3, 1, 2) if test else (PDX.pop(), PDY.pop(), PDZ.pop())
    Y, dys, xs = recorrelate(D, PDX, PDY, PDZ)
    print(Y)
    print(dys)
    print(xs)
    print(sorted(-h["step0"] for h in Y))
    # This searches for a hailstone going parallel to our rock in one axis.
    # Turns out that won't be useful, but it could lead to an easy way for initial position
    # for d in D:
    #   if d.dx == PDX or d.dy == PDY or d.dz == PDZ:
    #     print(d)
    T = Y[0]["x1"]
    R = Y[0]["src"]
    print(R)
    ex2 = R.x + R.y + R.z
    r1, r2 = (2, 47) if test else (16779, 871983857253169)
    
    print(f"{'ok' if ex1 == r1 else 'nok'}: {ex1}")
    print(f"{'ok' if ex2 == r2 else 'nok'}: {ex2}")

    J'ai pas trop nettoyé le code hein.
    Et dans la version téléphone, j'utilise s et o au lieu de self et other dans la classe Traj (qui ne va quand même pas s'appeler Trajectory non plus, trop long…), tout pour écrire le moins possible !

    • Yth.
    • [^] # Re: Pas de Z3, mais au moins Z^3 neurones grillés

      Posté par  (Mastodon) . Évalué à 2. Dernière modification le 03 janvier 2024 à 10:46.

      Ah, et côté perfs, on est sous la seconde pour l'exécution en python.

      Je ne suis pas sûr que ça aurait été beaucoup plus long si j'avais codé à l'arrache ma propre fonction pour les diviseurs, plutôt que d'utiliser sympy : on n'en calcule pas tant que ça, et au bout du compte les nombres ne sont pas si grands, avec de l'ordre de 200 diviseurs, et une racine carrée autour de 10 millions, ça se réduit assez vite, c'est pas vraiment là qu'on va perdre du temps.
      Avec sympy c'est immédiat.

      On perd probablement plus de temps à charger le module, from sympy import divisors prend un temps visible dans un shell python, ça doit être la majeure partie de la seconde qui part là-dedans !

      Bien sûr, ici, je sais que j'ai un dx, dy et dz, et l'algorithme ne s'adapte pas à une éventuelle situation où on n'en n'aurait que deux sur trois, mais à part de forcer à faire du code plus propre, ça ne changerait pas grand chose à l'algorithme final qui n'utilise que dz et dx et valide le dy recalculé.
      Et comme dit plus haut, je calcule un paquet de fois la solution à partir de toutes les parallèles en z, alors qu'une seule suffit.

      Bref, un algo plus générique ne serait pas beaucoup plus complexe, il faudrait formaliser mieux.

      Par contre si on n'a de parallèles que sur un seul axe, je coince a priori. Il faudrait essayer des valeurs possibles sur un autre axe, en supposant qu'elles ne soient pas trop grandes, ce qui est le cas puisque dx=-242, dy=-49, dz=209, donc en explorant depuis 0 en positif et négatif, on va mettre quelques centaines de tests pour trouver la solution.
      Et c'est nettement pire si on n'a aucune parallèle sur aucun axe…
      La force brute en essayant au pif des dx, dy et dz sans en connaître aucun, devrait permettre de tomber sur la solution en quelques dizaines de millions de tests, ce qui reste faisable, et probablement assez rapide (quelques minutes ? une heure max ?) sur un ordinateur moderne.

      • Yth.
  • # Géométrie vectorielle et analytique

    Posté par  (site web personnel) . Évalué à 3.

    Sommaire

    Bon, c'est un problème de géométrie.

    Je passe sur la première partie, trouver des intersections de ligne dans le plan c'est sans grand intérêt.

    La seconde partie est beaucoup, beaucoup plus intéressante. J'ai vainement cherché une solution élégante avant d'en trouver une sur Reddit. Je vous l'explique.

    À supposer que l'on trouve une position de départ p et une vitesse v qui permette de percuter tous les grêlons, en se plaçant dans le référentiel de notre projectile, ce sont tous les grêlons qui vont converger jusqu'à l'atteindre, chacun à son tour. Autrement dit, pour un grêlon (p0, v0), la droite (p0, v0 - v) passe par notre position de départ p. Et il en est de même pour les autres grêlons.

    Par conséquent, les trajectoires corrigées des trois premiers grêlons (p0, v0 -v), (p1, v1 -v) et (p2, v2 -v) se coupent deux à deux en p. Il est temps d'ouvrir une parenthèse sur les droites sécantes.

    Des droites sécantes

    Dans l'espace, contrairement au plan, des droites peuvent être identiques, parallèles, sécantes ou… rien de tout ça.

    Étant données deux droites caractérisées chacune par un point et un vecteur directeur l0 = (p0, v0) et l1 = (p1, v1), la première chose à vérifier est qu'elles ne sont ni identiques ni parallèles. Autrement dit, que leurs vecteurs directeurs ne sont pas colinéaires. Une façon de faire consiste à prendre leur produit vectoriel, qui ne doit pas être nul.

    Si ces droites ne sont pas parallèles, les droites vectorielles associées (O, v0) et (O, v1), définissent un plan vectoriel. Ce plan vectoriel peut être caractérisé par un vecteur normal facile à construire par le produit vectoriel des vecteurs directeurs de ces deux droites : n = v0 ^ v1.

    Le plan affine parallèle à ce plan vectoriel et incluant d0 a pour équation vectorielle r ⋅ n = p0 ⋅ n. Le plan affine incluant d1 a quant a lui pour équation vectorielle r ⋅ n = p1 ⋅ n.

    Ces plans sont identiques si et seulement si p0 ⋅ n = p1 ⋅ n. Autrement dit, en revenant à la définition de ce vecteur normal n, si (p0 - p1) ⋅ (v0 ^ v1) = 0. Si ces plans sont identiques, les droites sont coplanaire, et n'étant pas parallèles, elles sont donc sécantes. Réciproquement, si les droites sont coplanaires, les plans sont identiques.

    Retour au problème

    Puisque le problème a une solution, les trajectoires corrigées de deux grêlons (p0, v0 - v) et (p1, v1 - v) sont sécantes. Bon, ok, à condition qu'elles ne soient pas identiques : si c'était le cas on prendrait juste une autre grêlon, on en a plein à notre disposition. Mais vous pouvez vérifier sur vos données, ce cas ne se présente pas. Par conséquent :

    (p0 - p1) ⋅ ((v0 - v) ^ (v1 - v))               = 0
    (p0 - p1) ⋅ (v0 ^ v1 - v0 ^ v - v ^ v1 + v ^ v) = 0
    (p0 - p1) ⋅ (v0 ^ v1 + v ^ v0 - v ^ v1 + 0)     = 0
    (p0 - p1) ⋅ (v0 ^ v1 + v ^ (v0 - v1))           = 0

    En réorganisant un peu et en utilisant les propriété du produit mixte :

    (p0 - p1) ⋅ ((v0 - v1) ^ v) = (p0 - p1) ⋅ (v0 ^ v1)
    v ⋅ ((p0 - p1) ^ (v0 - v1)) = (p0 - p1) ⋅ (v0 ^ v1)

    Donnons un nom à ces termes constants :

    A0 = (p0 - p1) ^ (v0 - v1)
    M0 = (p0 - p1) ⋅ (v0 ^ v1)

    On a donc :

    v ⋅ A0 = M0

    Plus de droites

    De la même façon, en utilisant une droite de plus, posons :

    A0 = (p0 - p1) ^ (v0 - v1)
    A0 = (p1 - p2) ^ (v1 - v2)
    A0 = (p2 - p0) ^ (v2 - v0)
    
    M0 = (p0 - p1) ⋅ (v0 ^ v1)
    M0 = (p1 - p2) ⋅ (v1 ^ v2)
    M0 = (p2 - p0) ⋅ (v2 ^ v0)

    On a maintenant trois équations sur v :

    v ⋅ A0 = M0
    v ⋅ A1 = M1
    v ⋅ A2 = M2

    Pour résoudre ça simplement, il y a une astuce. On va utiliser une base vectorielle ainsi définie, avec des vecteurs conçus que chacun d'entre eux soit orthogonal à deux vecteurs des équations précédentes :

    u0 = A1 ^ A2
    u1 = A2 ^ A0
    u2 = A0 ^ A1

    Et écrire la vitesse que nous cherchons sur cette base : v = a0 u0 + a1 u1 + a2 u2. Les équations précédentes deviennent désormais :

    v ⋅ A0 = a0 (A1 ^ A2) ⋅ A0 = M0
    v ⋅ A1 = a1 (A2 ^ A0) ⋅ A1 = M1
    v ⋅ A2 = a2 (A0 ^ A1) ⋅ A2 = M2

    On peut reconnaître ici le produit mixte de nos vecteurs A0 et compagnie, que l'on va nommer A* = A0 ⋅ (A1 ^ A2), ce qui donne :

    a0 A* = M0
    a1 A* = M1
    a2 A* = M2

    Et finalement nos coefficients :

    a0 = M0 / A*
    a1 = M1 / A*
    a2 = M2 / A*

    Récapitulons

    Avec les trois premiers grêlons, on calcule les vecteurs et scalaires constants suivants :

    A0 = (p0 - p1) ^ (v0 - v1)
    A0 = (p1 - p2) ^ (v1 - v2)
    A0 = (p2 - p0) ^ (v2 - v0)
    
    M0 = (p0 - p1) ⋅ (v0 ^ v1)
    M0 = (p1 - p2) ⋅ (v1 ^ v2)
    M0 = (p2 - p0) ⋅ (v2 ^ v0)
    
    A* = A0 ⋅ (A1 ^ A2)

    Puis les vecteurs suivants :

    u0 = A1 ^ A2
    u1 = A2 ^ A0
    u2 = A0 ^ A1

    Et enfin les coefficients suivants :

    a0 = M0 / A*
    a1 = M1 / A*
    a2 = M2 / A*

    La vitesse de notre projectile doit être :

    v = a0 u0 + a1 u1 + a2 u2

    Et la position alors ?

    La vitesse, c'est bien, mais c'est surtout la position de départ qu'on nous demande. On va dire que c'est facile à déduire désormais : c'est l'intersection des trajectoires corrigées des deux premiers grêlons. Par exemple, on peut en prendre d'autres si on veut.

    Sauf que non, ce n'est vraiment pas trivial à calculer, l'intersection de deux droites sécantes dans l'espace. Il y a encore une astuce, et celle-là est vraiment de moi. Je vous la donnerai plus tard, là je suis fatigué de raconter mes aventures mathématiques.

    • [^] # Re: Géométrie vectorielle et analytique

      Posté par  (site web personnel) . Évalué à 3.

      Pour déterminer la position de départ donc, la première idée consiste à chercher l'intersection de deux trajectoires corrigées. Une intersection de droites donc. Sauf que c'est assez moche à calculer, on peut faire plus élégant.

      Les trajectoires corrigées étant toutes sécantes au même point, celui qu'on recherche, en les prenant deux par deux on peut définir des plans. Il est temps d'ouvrir une petite parenthèse.

      Plan défini par deux droites

      Dans l'espace, deux droites peuvent définir un plan, à condition nécessaire et suffisante qu'elles soient soit parallèles mais non identiques, soit sécantes.

      Soient deux droites pertinentes selon cette condition et définies chacune par un point et par un vecteur (p0, v0) et (p1, v1). On cherche à caractériser leur plan commun, par un point et un vecteur normal.

      Si elles ne sont pas parallèles, leurs vecteurs directeurs v0 et v1 ne sont pas colinéaires. Leur produit vectoriel n = v0 ^ v1 est non nul et orthogonal aux deux droites et fait donc un très bon vecteur normal pour le plan cherché.

      Si elles sont parallèles leurs vecteurs directeurs sont certes colinéraires, mais p0 - p1 n'est pas colinéaire à ces derniers (sinon, vous pouvez vérifier, les droites seraient identiques). On peut donc choisir n = v0 ^ (p0 - p1) comme vecteur normal pour le plan cherché.

      Il nous reste à trouver un point sur le plan cherché : c'est trivial, il suffit de prendre par exemple p0 puisque ce plan contient par définition la première droite. Pour obtenir une équation de plan du type n ⋅ r = d, il suffit de prendre d = p0 ⋅ n.

      En fait, nous nous intéressons seulement au cas de droites sécantes, voici donc le calcul pour obtenir l'équation du plan dans ce cas spécifique :

      n = v0 ^ v1
      d = p0 ⋅ n
      
      n ⋅ r = d

      Retour au problème

      En prenant les trajectoires corrigées deux par deux, on peut définir un tas de plans contenant tous le point cherché. Or l'intersection de trois plans non parallèles est un point, qui sera forcément ce dernier ! Ouvrons une nouvelle parenthèse.

      Intersection de plans

      Allons-y pour l'intersection de trois plan non parallèles (p0, d0), (p1, d1) et (p2, d2).

      Le point d'intersection, que nous allons noter r, respecte les équation des trois plans :

      n0 ⋅ r = d0
      n1 ⋅ r = d1
      n2 ⋅ r = d2

      L'astuce consiste ici à choisir une base vectorielle alternative :

      u0 = n1 ^ n2
      u1 = n2 ^ n0
      u2 = n0 ^ n1

      En exprimant la position cherchée comme combinaison de ces trois vecteurs r = a0 u 0 + a1 u1 + a2 u2, l'équation du premier plan devient :

      n0 ⋅ (a0 u0 + a1 u1 + a2 u2)         = d0
      a0 n0 ⋅ u0 + a1 n0 ⋅ u1 + a2 n0 ⋅ u2 = d0
      a0 n0 ⋅ u0 + a1 × 0     + a2 × 0     = d0
      a0 n0 ⋅ (n1 ^ n2)                    = d0

      On peut reconnaître ici le produit mixte de nos trois vecteurs normaux, un scalaire que l'on va noter U = n0 ⋅ (n1 ^ n2). Les trois équations deviennent de la même façon :

      a0 U = d0
      a1 U = d1
      a2 U = d2

      Ce qui nous donne finalement ces fameux coefficients :

      a0 = d0 / U
      a1 = d1 / U
      a2 = d2 / U

      Qui nous donnent donc le vecteur position de l'intersection de nos trois plans. Pour rappel, voici les calculs à effectuer à partir des constantes définissant les trois plans :

      u0 = n1 ^ n2
      u1 = n2 ^ n0
      u2 = n0 ^ n1
      
      U = n0 ⋅ (n1 ^ n2)
      
      a0 = d0 / U
      a1 = d1 / U
      a2 = d2 / U
      
      r = a0 u0 + a1 u1 + a2 u2

      Re-retour au problème

      En prenant trois trajectoires corrigées (p0, v0 - v), (p1, v1 - v) et (p2, v2 - v) , on sait désormais caractériser leurs plans communs deux à deux, soit trois plan. Et on sait également déterminer l'intersection de ces trois plan. Problème résolu !

    • [^] # Re: Géométrie vectorielle et analytique

      Posté par  (site web personnel) . Évalué à 3.

      Notes d'implémentation :

      • On fait pas mal de calculs sur des entiers qu'on finit à un moment ou à un autre par diviser. Le meilleur type de données pour cela, c'est à mon avis une implémentation des rationnels. En Python, c'est fractions.Fraction.
      • On est dans de la géométrie, on fait des produits scalaires, des produits vectoriels, des additions, des soustractions, des multiplications par un scalaire… C'est parfait pour implémenter une classe Vector et des opérateurs variés. En Python, on peut par exemple définir des méthodes qui réutilisent les opérateurs standard de façon habituelle ou futée (vous allez comprendre…) :
        • __rmul__ pour le produit par un scalaire alpha * v ;
        • __xor__ pour le produit vectoriel v ^ w ;
        • __add__ et __sub__ pour l'addition et la soustraction vectorielles ;
        • __neg__ pour l'opposition ;
        • __floordiv__ pour le test de colinéarité v // w ;
        • __bool__ pour le test de non-nullité (permet d'écrire des trucs comme if vector).
      • Enfin, on va travailler avec des droites, des plans, là aussi c'est parfait pour faire de la belle modélisation avec des méthodes permettant d'utiliser des opérateurs comme //, ==, etc.

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.