syj a écrit 654 commentaires

  • # Jour 24

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1.

    Pour la partie 1, il suffit de suivre les instructions et valider les TU.

    Pour la partie 2, je pense que je n'ai pas choisie la solution la plus rapide. Je mets environ 1min pour trouver la solution.

    Je fais une fonction recursive qui va descendre à une profondeur de 44.

    En gros, je vais valider l'addition de 2 entiers en commençant par les bits de poids faible jusqu'au bit de poids fort.
    Quand j'identifie une erreur j'applique une permutation de sortie.

    Pour valider, l'addition de 2 entiers, je ne considère pas tous les entiers 244. çà serait trop long.
    Je construits des additions particulières en binaires qui vont valider toutes les retenus à la profondeur ou je suis. A chaque addition , je valide la commutativité de mon addition.
    Par exemple , à la profondeur 3
    1
    1

    1
    11

    1
    111

    Mais je vais aussi valider le merge de nombre binaire sans retenu et je vérifie encore la commutativité.
    1
    0

    10
    101


    Bien paramétré cette fonction de validation a été déterminant car c'est elle qui garantit qu'au fur et à mesure de l'exploration des combinatoire possible , je n'engendre pas de régression dans les chiffres et çà me permet de déterminer rapidement une impasse dans le choix de la permutation

    L'autre point important, c'est quand on détecte une anomalie, je vais déterminer les bits concernés et en déduire les portes éligibles à la permutation.
    çà limite mon exploration.

        public static long wrongBit(long expected , long result) {
            return (expected ^ result);
        }
    
        public static long isOk(long current) {
            report.start("isOk");
            long wrong = 0;
            long mask = current;
    
            long x = 0;
            long r ;
            while(current > 0) {
                long expectedAddOne = 1l + current;         
                r = evaluateNetwork(1l, current);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(expectedAddOne, r);
                r = evaluateNetwork( current, 1l);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(expectedAddOne, r);
                r = evaluateNetwork( current, 0l);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(current, r);
    
                r = evaluateNetwork( 0l, current);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(current, r);
    
                long a = 1l << x;
                long b = mask - a;
                r = evaluateNetwork( a, b);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(mask, r);
    
                r = evaluateNetwork( b, a);
                if(r < 0) {
                    return -1;
                }
                wrong = wrong | wrongBit(mask, r);
    
                current = current >> 1l;
                x++;
            }
    
            report.end("isOk");
            return mask & wrong;
    
    
    
        }
    
    
    
        private static void recurseFixGates(Set<String> validated, int x) {
    
            if(x > maxDepth) {
                System.out.println(x + " " + validated.size() );
                maxDepth = x;
            }
            if(validated.size() % 2 == 1) {
                System.out.println("Whats");
            }
            if (x == 44) {      
    
                if(validate()) {                        
                    String resultsAsString = validated.stream().sorted().collect(Collectors.joining(","));
                    if (!availablesResults.contains(resultsAsString)) {
                        availablesResults.add(resultsAsString);
                        System.out.println(resultsAsString);
                    }
                    System.exit(0);
                }
    
                return;
    
            }
            if(validated.size() > 8) {
                return;
            }
    
            long right = 1l << (x+1);
    
    
            // System.out.println(x + ":" + left.toString(2) + " + " + right.toString(2) + "
            // =>" + z.toString(2));
            long wrong = isOk(right);
            if(wrong < 0) {
                System.out.println("There is a loop : " +x);
                return;
            }
    
            if (wrong != 0) {
    
                // System.out.println("Need fix to get " + expect.toString(2));
                Set<Gate> changes = computeRelated(wrong);
    
                for (Gate a : changes) {
                    if (validated.contains(a.wireOutput)) {
                        continue;
                    }
                    for (Gate b : gates) {
                        if (a.equals(b) || validated.contains(b.wireOutput) || lessZ(b.wireOutput, x)) {
                            continue;
                        }
    
                        String tmp = b.wireOutput;
                        b.wireOutput = a.wireOutput;
                        a.wireOutput = tmp;
                        try {
                            if (isOk(right) == 0l || (x <= 2 && isOk(right) == -1)) {
                                validated.add(a.wireOutput);
                                validated.add(b.wireOutput);
    
                                recurseFixGates(validated, x + 1);
                                validated.remove(a.wireOutput);
                                validated.remove(b.wireOutput);
    
                                if(validated.size() % 2 == 1) {
                                    System.out.println("Whats");
                                }
                            }
                        } finally {
                            tmp = b.wireOutput;
                            b.wireOutput = a.wireOutput;
                            a.wireOutput = tmp;
                        }
    
                    }
                }
            } else {
                recurseFixGates(validated, x + 1);
            }
        }
    
        private static boolean validate() {
    
            for(long x=0;x < 43;x++) {
                long a = (1l << x)-1;
                long b = 13;            
                if((a+b) != evaluateNetwork(a, b)) {
                    return false;
                }
            }
            return true;
        }
    
        public static boolean lessZ(String name, int x) {
            if(! name.startsWith("z")) {
                return false;
            }
    
            return Integer.valueOf(name.substring(1)) <= x;
        }
    
        public static Gate findByOutput(String name) {
            return gates.stream().filter(g->g.wireOutput.equals(name)).findFirst().orElse(null);
        }
    
        private static Set<Gate> computeRelated(long wrong) {
            if(wrong == -1) {
                return new HashSet<Aoc2024s24p2.Gate>(gates);
            }
            Set<Gate> related = new HashSet<Aoc2024s24p2.Gate>();
            for(int x=0;x < 45;x++) {
                long mask = 1l << x;
                if((wrong & mask)> 0) {
                    Gate gate = findByOutput(zindex(x));
                    recurseRelated(related, gate);                                                                  
                }
            }
    
            return related;
        }
    
        private static void recurseRelated(Set<Gate> related, Gate gate) {
            if(related.contains(gate) || gate == null) {
                return;
            }
            related.add(gate);              
            recurseRelated(related, findByOutput(gate.wireLeft.name));
            recurseRelated(related, findByOutput(gate.wireRight.name));
    
    
        }
    
        private static long evaluateNetwork(Long left, Long right) {
            report.start("evaluateNetwork");
            if(left != null) {
                initiate("x", left);
            }
            if(right != null) {
                initiate("y", right);
            }
    
            Map<Gate, AtomicInteger> updated = new HashMap<Aoc2024s24p2.Gate, AtomicInteger>();
            /*for(Wire wire : wireByName.values()) {
                if(! (wire.name.startsWith("x") || wire.name.startsWith("y"))) {
                    wire.state = null;
                }
            }*/
            boolean haveUpdate = false;
            do {
                haveUpdate = false;
    
                for (Gate gate : gates) {
                    if (gate.update()) {
    
                        int count = updated.computeIfAbsent(gate, k->new AtomicInteger()).incrementAndGet();                                        
                        if (count > 2) {
                            report.end("evaluateNetwork");
                            return -1;
                        }
                        haveUpdate = haveUpdate || true;                    
                    }
    
                }
            } while (haveUpdate);
    
            int x = 0;
    
            long z = 0;
            while(wireByName.get(zindex(x)) != null) {
                //System.out.println(x + " => " + wireByName.get(zindex(x)).state );
                Wire wire = wireByName.get(zindex(x));
                if(wire.state != null && wire.state) {
                    long v =  1l << x;
    
                    //System.out.println(v);
                    z = z + v;
                }
                x++;
            }
    
            report.end("evaluateNetwork");
            return z;
        }
    
        private static void initiate(String s, long left) {
    
            for (long x = 0; x < 45; x++) {
                long mask = 1l << x;
                if ((mask & left) > 0) {
                    wireByName.get(index(s, x)).state = true;
                } else {
                    wireByName.get(index(s, x)).state = false;
                }
            }
    
        }
    
        public static String index(String s, long x) {
            return (x < 10 ? s + "0" : s) + x;
    
        }
    
        public static String zindex(long x) {
            return (x < 10 ? "z0" : "z") + x;
        }
  • [^] # Re: jour 23 - cracra

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1.

    Ce n'est vraiment pas terrible comme performance :)

    En gros à la lecture, je charge mes map & mes liens.
    Puis, je regroupe mes éléments.
    A la fin, je filtre pour trouver le plus gros groupe.

        public static Map<String, Node> nodesByCode = new HashMap<>();
        public static Map<Node, List<Link>> linksByNodes = new HashMap<>();
    
        public record Node(String name) implements Comparable<Node> {
              //...
            }
    
            public record Link(Node left, Node right) {
              // ...
        }
    
            public record Group(TreeSet<Node> members) {
             // ...
            }
    
            public void main() {
             //...
    
    
             Set<Group> groups = new HashSet<>();
             for (Map.Entry<Node, List<Link>> entry : linksByNodes.entrySet()) {
                      Node a = entry.getKey();
                      TreeSet<Node> members = new TreeSet<>();
                      recurseGroup(members, a);
                      if (members.size() > 3) {
                               groups.add(new Group(members));
                      }
             }
         /* Chercher le plus grand groups */
            }
    
            private static void recurseGroup(TreeSet<Node> members, Node a) {
            for (Node n : members) {
    
                if (linksByNodes.get(a).stream().filter(l -> l.match(n)).count() == 0) {
                    return;
                }
    
            }
    
            members.add(a);
            for (Link link : linksByNodes.get(a)) {
                Node b = link.getOther(a);
                if (members.contains(b)) {
                    continue;
                }
    
                recurseGroup(members, b);
            }
    
        }

    Je fais 215ms
    et si je répète l'opération plusieurs fois , je descends à 15ms pour le même traitement.

  • [^] # Re: 22ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1. Dernière modification le 23 décembre 2024 à 10:16.

    Il n’était pas vraiment intéressant.
    Pareil, j’ai suivi les instructions. J’ai été dessus quand je me suis rendu compte que le but de la deuxième partie n’était pas de trouver le secret initial ou un truc du genre.

    Je n’ai pas cherché à optimiser, j’ai tout stocker dans un new long[2500][2001]

    Puis, j’ai distribué dans une map

    Map<Sequence, Map<Integer, SequenceResult>> firstGainsByBuyerBySequence;
    public record Sequence(int[] fours){}
    public record SequenceResult(int buyer, long endNumber, int[] fours){}
  • [^] # Re: 21ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2. Dernière modification le 23 décembre 2024 à 10:03.

    J'ai lutté sur celui-ci… presque 9h.

    Pour la partie 1, j'ai tenté trouver un ordre dans les mouvements qui était toujours valide via un sort.
    Finalement, je m'étais rabattu sur une fonction qui donnait tous les mouvements possibles.

    Pour la partie 2, mon code de la partie 1 explosait même pour un chiffre à profondeur de 4.
    Je me suis donc douté qu’il fallait faire un min. J’ai rapidement résolut ce problème avec un cache pour la programmation dynamique.
    Par erreur, je pensai que çà exploserai en temps. Si je considérai tous les mouvements d’une case à l’autre.
    Donc, j’ai tenté de chercher une distribution qui marchait dans tous les cas. J’ai réussi à trouver une combinaison qui valider pour la profondeur 2 et 3 pour les 2 jeux de test (j’ai obtenu la validation à 3 avec mon code de la partie 1) mais bien sûr, çà ne fonctionnait pas en profondeur 25. Il y a un cas non optimum qui doit apparaitre.
    J’ai finalement tenté d’envisager tous les chemins possibles et j’ai été surpris de voir que cela marchait.
    Comme quoi, quand on part sur une mauvaise piste, on bloque dessus.

        private static long processDoors(List<String> doors) {
            long sum = 0;
            for(String door : doors) {
                long messageLength = 0;
                String previous = "A";
    
                for(char c : door.toCharArray()) {  
                    messageLength += recurse(0, handleNumPad.get(previous + c));
                    previous = String.valueOf(c);
                }
    
                System.out.println(door + ":" +  messageLength);
                sum += messageLength * Long.valueOf(door.substring(0, door.length()-1));
            }
            return sum;
        }
    
        private static long recurse(int i, List<String> paths) {
            long sum = 0;
    
            Seek seek = new Seek(i, paths);
            Long cached = cacheResult.fromCache(seek);
    
            if(cached != null) {
                return cached;
            }
    
            if(i <= LIMIT) {
                long minPath = Long.MAX_VALUE;
                 for(String path: paths) {
                     char previous = 'A';
                     long currentPath = 0;
                     for(char c: path.toCharArray()) {                   
                         currentPath += recurse(i + 1, handleArrowPad.get("" + previous + c));                   
                         previous = c;
                     }
                     if(currentPath < minPath) {
                         minPath= currentPath;
                     }
                 }
                 sum+= minPath;
            } else {
                sum = 1;
            }
            cacheResult.setInCache(seek, Long.valueOf(sum));
            return sum;
        }
  • [^] # Re: 18ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2.

    Pour la première partie, j ai fait un simmle dijkstra.
    Pour la deuxième partie, j ai brute force ce dernier à chaque pixel. J étais un peu déçu car je m attendais à une deuxième bien plus complexe.

    Si le problème de performance aurait été plus complexe. En demultipliant la map d input. J aurai probablement tenter. De conserver le path dans mon dijkstra. De cette manière, j aurai pu déterminer rapidement les cases à mettre en jour quand c est dernier sont affecté par la mise à jour…

  • [^] # Re: 17ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2.

    Hello,

    J'ai procédé de cette manière pour la partie 2.

    Ce matin pendant le travail, j'ai tenté de brute-force, je suis monté à plusieurs milliard de possibilité testé :O)

    Ce midi:
    J'ai modifié mon Engine pour qu'elle affiche le code Java équivalent à chaque opération.

    Sur la base du code Java et l'impression du résultat en binaire
    Que le bit de A était consommé progressivement par le programmme pour construire la sortie.
    J'ai alors compris que le programme avançait par paquet de 3 à 6 bits.

    J'avais presque la réponse ce midi. Je trouvais un A qui me donnait le bon résultat un chiffre de plus ",2" :)

    Ce soir:
    J'ai revu plein de fois de mon algo pour m’apercevoir que j'avais merdé un <= en < dans ma fonction de contrôle progressif.
    Résultat, il me trouvait toujours un resultat matchant avec un chiffre de plus :O)

  • [^] # Re: jour 16

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1.

    Ce n'est pas un simple Dijkstra.

    Perso , j'ai du combiner le déplacement & la rotation.
    Au final même pour simplifier la partie 2, j'ai revu mon algo pour considérer la rotation comme un mouvement.

    Ensuite pour la partie 2, j'utilise la map de poids de la partie 1.

    Je pars du start et je parcours en profondeur ma map de poids.

    Je passe d'un poids à l'autre récursivement , si le poids d déplacement ou une rotation correspond au poids minimum que j'avais constaté.

  • [^] # Re: 14ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1.

    Pour la partie 2, j'ai opté pour un algo simple.

    Je compte le nombre de sapin avec au moins un autre adjacent.

    Ce nombre change à chaque tour. A chaque fois que je trouvai un maximum. J'affiche la carte.

    A un momemt le premier maximum affiche le sapin.

  • # 13ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 3.

    Aujourd'hui, je me suis dit que c'était le bon jour pour essayer une IA. Voir ce que cela donnerai.

    Je l'ai fait d'abord en Java en utilisant un Mistral (medium) car j'étais persuadé qu'il arriverait à me donner la bonne réponse.
    Après 10min à debug le code, j'avais la bonne réponse pour la première partie.

    Pour la deuxième partie , je lui ai demandé d'utiliser Apache Commons Math. En soit ,le code était correcte.
    Il y avait juste < 100 qui était resté, et il y avait un problème de cast à la sortie Apache Commons Math , où on sort des Double qu'il faut arrondir et non trunc.

    Vu que j'étais persuadé que j'aurai été plus vite avec Python. J'ai fait aussi l'exercice en python avec numpy :)
    J'ai aussi utilisé une IA pour voir et çà fonctionne.
    Par contre, bizarrement, il gérait encore plus mal la lecture des données que j'ai du aussi réecrire complétement.

    def solve_for_machine(xA, yA, xB, yB, xPrize, yPrize):
        # Set up the matrix and vectors
        coefficients = np.array([[xA, xB], [yA, yB]])
        constants = np.array([xPrize, yPrize])
    
        try:
            # Solve the system of equations
            solution = np.linalg.solve(coefficients, constants)
            a, b = solution
    
            a = round(a)
            b = round(b)
    
            verifyX = a*xA + b*xB
            verifyY = a*yA + b*yB
    
            # Check if the solution is valid
            if 0 <= a and 0 <= b and verifyX == xPrize and verifyY == yPrize:
                return int(3 * a + b)
        except np.linalg.LinAlgError:
            pass
    
        return -1  # No valid solution found
  • [^] # Re: 12ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 1.

    193ms première évaluation
    1,3ms pour la 100ème évaluation (Java , c'est du Diesel)

  • [^] # Re: 12ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2.

    compter le nombre de cotés revient à compter le nombre de coins.

    Je n'y avais pas pensé. J'ai utilisé une méthode différentes

    J'identifie les pièces sous forme d'un Set.

    Pour identifier les côtés, je détermine la bordure & la direction qui a servi à déterminer cette bordure. Cela me donne un Set

    Je regroupe les éléments de ce Set par exploration des adjacents de même directions. Le nombre groupe identifié correspond à mon nombre de côté.

        private static int computeSides(Set<Point> pieces) {
            Set<SidePart> set = new HashSet<>();
            int sides = 0;
            for (Point p : pieces) {
                for (Point d : Point.DIRECTIONS) {
                    Point i = p.add(d);
                    if (!pieces.contains(i)) {
                        set.add(new SidePart(p, d));
                    }
                }
            }
    
            Set<SidePart> counted = new HashSet<>();
            for (SidePart sidePart : set) {
                if (counted.contains(sidePart)) {
                    continue;
                }
    
                Set<SidePart> groups = new HashSet<>();
                buildGroup(set, sidePart, groups);
    
                counted.addAll(groups);
                sides++;
            }
            return sides;
        }
    
        private static void buildGroup(Set<SidePart> set, SidePart sidePart, Set<SidePart> groups) {
            if (!set.contains(sidePart)) {
                return;
            }
    
            if (groups.contains(sidePart)) {
                return;
            }
            groups.add(sidePart);
    
            Point direction = sidePart.direction;
            Point source = sidePart.source;
            if (direction.x != 0) {
                buildGroup(set, new SidePart(source.add(new Point(0, 1)), direction), groups);
                buildGroup(set, new SidePart(source.add(new Point(0, -1)), direction), groups);
            } else {
                buildGroup(set, new SidePart(source.add(new Point(1, 0)), direction), groups);
                buildGroup(set, new SidePart(source.add(new Point(-1, 0)), direction), groups);
            }
    
        }
    
        record SidePart(Point source, Point direction) {
        }
  • [^] # Re: 11ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2. Dernière modification le 11 décembre 2024 à 17:39.

    En fait, c'est moi qui avait du faire un cast en Int. Cela tenait bien dans un Long.

  • [^] # Re: 11ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 3. Dernière modification le 11 décembre 2024 à 13:48.

    u64, c'est pour unsigned 64 ?
    Car en Java, j'ai été obligé de passer tout en BigInteger car j'avais un dépassement et j'obtenais des chiffres négatifs

    Mais bon Java , tu ne peux pas faire de unsigned … donc peut être qui me manquait uniquement le 264 :)

  • # 11ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2.

    Si je l'avais fait en python. Je pense que j'aurai été plus vite environ 40min.
    J'ai été obligé de repasser tout en BigInteger pour la 2ème partie.

    La partie 2 : je mets 191ms pour trouver la solution ;-)

  • [^] # Re: 10ème jour

    Posté par  . En réponse au journal Advent of code 2024. Évalué à 2. Dernière modification le 11 décembre 2024 à 09:40.

    Hier, je l'ai pris de travers :)
    J'ai fait un dijkstra pour résoudre la première partie.

    Ce qui n'était pas du tout adapté à la partie 2, j'ai du repasser en récursion basique ensuite.
    Si j'avais pris ce choix, je pense que je faisais les 2 parties en moins de 20min

    Pour la partie 2 : 134ms (jvm lancé)

  • # Est-ce qu'il y a moyen de tester si l'imprimante réseau est sujette à cette faille ?

    Posté par  . En réponse au journal Faille d'exécution de code à distance dans cups. Évalué à 4.

    Hello,
    J'ai une imprimante en wifi sur mon réseau.
    Est-ce qu'il y a moyen de tester si l'imprimante réseau est sujette à cette faille ?

  • # Ça dépend

    Posté par  . En réponse au journal j'aime bien l'auto-complétion par IA (Github Copilot). Évalué à 2.

    Perso, je trouve que c'est très bien pour les juniors ou quand tu découvres un nouveau framework/nouvelle techno.

    Par contre pour mon usage, c'est contre productif. Les suggestions autre que les choses simple me coupe dans mon file de pensée. Ça me fait comme une sorte d'interruption et ça me perturbe plus qu'autre choses.
    Résultat, c'est l'inverse. Ça me rend moins productif.

    Après, je ne l'utilise pas au quotidien. Je l'utilise en général quand je travaille à quatre main sur le poste d'un junior. Donc peut-être que c'est un manque de pratique.

  • [^] # Re: Pre challenge

    Posté par  . En réponse au journal France Cybersecurity Challenge (FCSC) 2024 va commencer. Évalué à 1.

    J'ai bien aimé la première partie du prechall.
    Cela m'a rappelé l'époque où pour tricher dans les jeux. On allait modifier la mémoire ou le code.

    La deuxième partie est en python. Et c est ce qui m a fait perdre beaucoup de temps.
    C'est un classique des challenges de programmation mais je l'ai pris de travers…

  • [^] # Re: Même pour les quiches (comme moi)

    Posté par  . En réponse au journal France Cybersecurity Challenge (FCSC) 2024 va commencer. Évalué à 3.

    Les catégories introduction sont en général à la portée de tous.

    En général, les 1 étoiles me prennent en général 1 à 4h.
    Au-dessus, les 2 étoiles, j arrive à en avoir quelques une

    Les 3 étoiles, je ne suis pas sûr d en avoir eu une pendant le concours mais je suis toujours très intéressé de découvrir les write-up une fois le concours terminé.

  • [^] # Re: son altesse sérénissime

    Posté par  . En réponse au journal Atlassian SaaS.... Évalué à 2. Dernière modification le 13 février 2024 à 13:29.

    Je confirme , je me suis trompé.
    Je fais en général beaucoup fautes mais c'est encore pire que je suis énervé.

    Trop tard pour changer.

  • # 20 M €

    Posté par  . En réponse au journal Combien pour un algorithme de détection de piscines sur les photos aériennes ?. Évalué à 6. Dernière modification le 09 février 2024 à 08:56.

    20 M€ c'est le coup du dev.
    La maintenance annuelle, elle est à combien ?

  • [^] # Re: L'informatique c'est vaste

    Posté par  . En réponse au journal [Trolldi] La Big Tech vous souhaite une très belle réflexion existentielle. Évalué à 4.

    Je suis du même avis.
    On arrive sur ce genre de phase où il y a une restructuration de l'activité.
    Mais ça ne va pas durer.

    Il faudra probablement apprendre à revaloriser ses compétences ou revoir ses préférences techniques.

    Mais dans l'ensemble l'IA va augmenter la taille des SI et leur complexité.
    Résultat, on va passer moins de temps à coder et plus de temps en réunions de coordination.
    Les véritables compétences à revaloriser. Ça va être :
    - Les softskills: organisation, la motivation, la communication et le sens du service
    - la modélisation système
    - L'administration système.

  • # Algorithme de Karger

    Posté par  . En réponse au message Advent of Code 2023, jour 25. Évalué à 2.

    Pour le dernier jour, j'ai tenté plusieurs solutions naïve avant de chercher un algorithme qui pouvait répondre à mon problème.

    Je suis tombé sur l'algorithme de Karger qui me semblait relativement simple à implémenter.

    https://fr.wikipedia.org/wiki/Algorithme_de_Karger

    Je trouve que ma condition de sortie est un peu moisie mais dans l'ensemble.
    En gros, j'arrête le programme quand j'arrive à une contraction à 2 noeud avec 3 lien qui sont les 3 liens à couper.
    C'était la solution attendu. Je n'ai pas cherché plus loin.

    package aoc2023;
    
    import java.util.ArrayList;
    import java.util.Arrays;
    import java.util.HashMap;
    import java.util.HashSet;
    import java.util.LinkedList;
    import java.util.List;
    import java.util.Map;
    import java.util.Objects;
    import java.util.Random;
    import java.util.Scanner;
    import java.util.Set;
    import java.util.Stack;
    import java.util.stream.Collectors;
    import java.util.stream.Stream;
    
    public class Aoc2023s25 {
        final static Random random = new Random(0);
    
        public static class Link {
    
            String srcName;
            String dstName;
    
            public Link(String srcName, String dstName) {
                this.srcName = srcName;
                this.dstName = dstName;
            }
    
            @Override
            public String toString() {
                return dstName + "/" + srcName;
            }
    
            public boolean match(String name) {
                return name.equals(srcName) || name.equals(dstName);
            }
    
            public String otherName(String name) {
                return srcName.equals(name) ? dstName : srcName;
            }
    
            public Link replace(String left, String right, String b) {
                String nsrc = srcName;
                if (nsrc.equals(left) || nsrc.equals(right)) {
                    nsrc = b;
                }
    
                String ndst = dstName;
                if (ndst.equals(left) || ndst.equals(right)) {
                    ndst = b;
                }
    
                return new Link(nsrc, ndst);
            }
    
        }
    
        public static class Node {
            String name;
    
            public Node(String s) {
                this.name = s;
    
            }
    
            @Override
            public String toString() {
                return "Node [name=" + name + "]";
            }
    
            @Override
            public int hashCode() {
                return Objects.hash(name);
            }
    
            @Override
            public boolean equals(Object obj) {
                if (this == obj)
                    return true;
                if (obj == null)
                    return false;
                if (getClass() != obj.getClass())
                    return false;
                Node other = (Node) obj;
                return Objects.equals(name, other.name);
            }
        }
    
        public static void main(String[] args) {
            try (Scanner in = new Scanner(Aoc2023s25.class.getResourceAsStream("res/t25.txt"))) {
    
                Map<String, Node> nodeByName = new HashMap<>();
                List<Link> links = new ArrayList<>();
                while (in.hasNext()) {
                    String row = in.nextLine();
    
                    String[] fields = row.split(":");
                    Node n = new Node(fields[0].trim());
                    nodeByName.put(n.name, n);
    
                    links.addAll(Arrays.stream(fields[1].trim().split(" ")).map(String::trim)
                            .map(d -> new Link(n.name, d)).toList());
                }
    
                for (Link a : links) {
                    nodeByName.computeIfAbsent(a.dstName, k -> new Node(k + ": "));
                }
    
                while (true) {
                    Map<String, Node> clone = new HashMap<>(nodeByName);
                    algorithmKarger(clone, new ArrayList<>(links));
                }
            }
    
        }
    
        private static void algorithmKarger(Map<String, Node> nodeByName, List<Link> links) {
    
            while(nodeByName.size() > 2) {
                Link link = links.get(random.nextInt(links.size()));
    
                String leftName  = link.srcName;
                String rightName = link.dstName;
                String contractName = leftName + "," + rightName;
    
                nodeByName.remove(leftName);
                nodeByName.remove(rightName);
                nodeByName.put(contractName,new Node(contractName));
    
                List<Link> intLinks = links.stream()
                    .filter(l -> !(l.match(leftName) && l.match(rightName)))
                    .map(l->l.replace(leftName, rightName, contractName))
                    .toList();
    
                links =intLinks;
    
    
            }
    
            System.out.println(nodeByName.size());
            System.out.println(links.size());
            for(Node n : nodeByName.values()) {
                System.out.println(n.name + " => " + n);
            }
            if(links.size() == 3) {
                int prod = 1;
                for(String n :  nodeByName.keySet()) {
                    String[] keys = n.split(",");
                    System.out.println(keys.length);
                    prod *= keys.length;
                }
                System.out.println(prod);
                System.out.println(links);
                System.exit(0);
            }
    
        }
    }
  • [^] # Re: J'ai aussi utilisé le Z3 theorem prover.

    Posté par  . En réponse au message Advent of Code 2023, jour 24. É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)

  • # J'ai aussi utilisé le Z3 theorem prover.

    Posté par  . En réponse au message Advent of Code 2023, jour 24. É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();