Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow04FixedCover

Independent generated check. This module provides an additional generated proof of row 04 and is not imported by the main LowGenus root.

Generated exact replay of the fixed AR row-04 divisor on a fundamental domain for the core's slot-level symmetry group.

The external discovery data are untrusted: cells_check and tree_check replay every arithmetic obligation in the kernel, and the chamber is discharged by the generated coverage theorem, so the conclusion is the row on the whole closed orthant.

The twelve root rows of the closed orthant followed by the six chamber inequalities cutting the fundamental domain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The 32 homogeneous affine forms whose signs determine branches of the row-04 decision tree; coefficients are indexed by the twelve edge lengths.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 1, 2, 3 and Farkas receipts excluding inconsistent sign branches.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Subtree splitting on length[0] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 4, 5, 6 and Farkas receipts excluding inconsistent sign branches.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Subtree splitting on length[0] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 7, 8, 9, 10, 11, 12, 13, 14, 15 and Farkas receipts excluding inconsistent sign branches.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Contradiction leaf using Farkas receipt 215 to exclude the accumulated affine constraints in this row-04 branch.

            Equations
            Instances For

              Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 16, 17, 18, 19, 20, 21, 22 and Farkas receipts excluding inconsistent sign branches.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 16, 19, 23, 24 and Farkas receipts excluding inconsistent sign branches.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Contradiction leaf using Farkas receipt 215 to exclude the accumulated affine constraints in this row-04 branch.

                  Equations
                  Instances For

                    Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 25, 26, 27, 28, 29, 30 and Farkas receipts excluding inconsistent sign branches.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 31, 32, 33 and Farkas receipts excluding inconsistent sign branches.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 34, 35, 36, 37, 38, 39 and Farkas receipts excluding inconsistent sign branches.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Subtree splitting on - length[5] - length[6] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 40, 41, 42 and Farkas receipts excluding inconsistent sign branches.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 43, 44, 45, 46, 47, 48 and Farkas receipts excluding inconsistent sign branches.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 34, 35, 36 and Farkas receipts excluding inconsistent sign branches.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Subtree splitting on - length[0] + length[2] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 18, 23, 31, 32, 33, 37, 38, 39 and Farkas receipts excluding inconsistent sign branches.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 19, 49, 50, 51, 52 and Farkas receipts excluding inconsistent sign branches.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 19, 22, 44, 46, 48 and Farkas receipts excluding inconsistent sign branches.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Leaf selecting row-04 cell 0, with 22 Farkas receipts deriving its cone inequalities from the active branch constraints.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Contradiction leaf using Farkas receipt 517 to exclude the accumulated affine constraints in this row-04 branch.

                                        Equations
                                        Instances For

                                          Subtree splitting on length[5] - length[8] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 53, 54, 55, 56, 57, 58, 59 and Farkas receipts excluding inconsistent sign branches.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Subtree splitting on length[5] + length[6] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 53, 57, 60 and Farkas receipts excluding inconsistent sign branches.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 57, 60, 61 and Farkas receipts excluding inconsistent sign branches.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Subtree splitting on - length[5] - length[6] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 0, 54, 55, 59, 62 and Farkas receipts excluding inconsistent sign branches.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Contradiction leaf using Farkas receipt 573 to exclude the accumulated affine constraints in this row-04 branch.

                                                  Equations
                                                  Instances For

                                                    Contradiction leaf using Farkas receipt 574 to exclude the accumulated affine constraints in this row-04 branch.

                                                    Equations
                                                    Instances For

                                                      Subtree splitting on length[5] - length[8] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 4, 63, 64, 65, 66, 67, 68, 69, 70, 71 and Farkas receipts excluding inconsistent sign branches.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        Contradiction leaf using Farkas receipt 607 to exclude the accumulated affine constraints in this row-04 branch.

                                                        Equations
                                                        Instances For

                                                          Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 5, 72, 73, 74, 75, 76, 77, 78, 79 and Farkas receipts excluding inconsistent sign branches.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            Contradiction leaf using Farkas receipt 628 to exclude the accumulated affine constraints in this row-04 branch.

                                                            Equations
                                                            Instances For

                                                              Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 6, 80, 81, 82, 83, 84, 85, 86, 87 and Farkas receipts excluding inconsistent sign branches.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For

                                                                Contradiction leaf using Farkas receipt 675 to exclude the accumulated affine constraints in this row-04 branch.

                                                                Equations
                                                                Instances For

                                                                  Contradiction leaf using Farkas receipt 676 to exclude the accumulated affine constraints in this row-04 branch.

                                                                  Equations
                                                                  Instances For

                                                                    Subtree splitting on length[5] + length[6] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 66, 70, 73, 74, 81, 82 and Farkas receipts excluding inconsistent sign branches.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Subtree splitting on - length[5] - length[6] + length[8] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 69, 78, 86, 88, 89, 90 and Farkas receipts excluding inconsistent sign branches.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 71, 79, 87 and Farkas receipts excluding inconsistent sign branches.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          Contradiction leaf using Farkas receipt 36 to exclude the accumulated affine constraints in this row-04 branch.

                                                                          Equations
                                                                          Instances For

                                                                            Contradiction leaf using Farkas receipt 705 to exclude the accumulated affine constraints in this row-04 branch.

                                                                            Equations
                                                                            Instances For

                                                                              Contradiction leaf using Farkas receipt 706 to exclude the accumulated affine constraints in this row-04 branch.

                                                                              Equations
                                                                              Instances For

                                                                                Contradiction leaf using Farkas receipt 707 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                Equations
                                                                                Instances For

                                                                                  Contradiction leaf using Farkas receipt 708 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                  Equations
                                                                                  Instances For

                                                                                    Subtree splitting on length[5] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 91, 92, 93, 94, 95, 96, 97, 98, 99 and Farkas receipts excluding inconsistent sign branches.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      Contradiction leaf using Farkas receipt 800 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart40_check :

                                                                                        Subtree splitting on length[5] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 20, 100, 101, 102, 103, 104, 105, 106, 107, 108 and Farkas receipts excluding inconsistent sign branches.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart41_check :
                                                                                          treePart41.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1]]) = true

                                                                                          Contradiction leaf using Farkas receipt 897 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart42_check :
                                                                                            treePart42.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1]]) = true

                                                                                            Contradiction leaf using Farkas receipt 898 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart43_check :
                                                                                              treePart43.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1]]) = true

                                                                                              Contradiction leaf using Farkas receipt 899 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart44_check :
                                                                                                treePart44.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -2, -1, 0, -1]]) = true

                                                                                                Subtree splitting on length[5] + length[6] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 109, 110, 111, 112 and Farkas receipts excluding inconsistent sign branches.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart45_check :
                                                                                                  treePart45.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -2, -1, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1]]) = true

                                                                                                  Subtree splitting on - length[5] - length[6] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 113, 114, 115, 116, 117, 118, 119, 120 and Farkas receipts excluding inconsistent sign branches.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart46_check :
                                                                                                    treePart46.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -2, -1, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 0, -1, 0, -1]]) = true

                                                                                                    Subtree splitting on - length[5] - length[6] + length[10] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 121, 122 and Farkas receipts excluding inconsistent sign branches.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart47_check :
                                                                                                      treePart47.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -2, -1, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 0, -1, 0, -1])]) = true

                                                                                                      Subtree splitting on length[5] + length[6] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 123, 124 and Farkas receipts excluding inconsistent sign branches.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart48_check :
                                                                                                        treePart48.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, -1, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -2, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1])]) = true

                                                                                                        Contradiction leaf using Farkas receipt 322 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart49_check :
                                                                                                          treePart49.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, -1])]) = true

                                                                                                          Subtree splitting on length[1] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 18, 125, 126, 127, 128, 129, 130, 131, 132, 133 and Farkas receipts excluding inconsistent sign branches.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For

                                                                                                            Contradiction leaf using Farkas receipt 217 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Contradiction leaf using Farkas receipt 1080 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                Contradiction leaf using Farkas receipt 1081 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Contradiction leaf using Farkas receipt 1082 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart54_check :
                                                                                                                    treePart54.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 1, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 1, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1]]) = true

                                                                                                                    Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 23, 134, 135, 136, 137, 138, 139, 140, 141 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart55_check :
                                                                                                                      treePart55.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 1, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 1, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, -1])]) = true

                                                                                                                      Contradiction leaf using Farkas receipt 1130 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart56_check :
                                                                                                                        treePart56.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 1, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 1, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])]) = true

                                                                                                                        Contradiction leaf using Farkas receipt 1131 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart57_check :
                                                                                                                          treePart57.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 1, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])]) = true

                                                                                                                          Contradiction leaf using Farkas receipt 82 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Contradiction leaf using Farkas receipt 1132 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              Contradiction leaf using Farkas receipt 337 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                Contradiction leaf using Farkas receipt 1133 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Contradiction leaf using Farkas receipt 1134 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 142, 143, 144, 145 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart63_check :

                                                                                                                                      Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 93, 127, 146, 147 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart64_check :
                                                                                                                                        treePart64.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1]]) = true

                                                                                                                                        Subtree splitting on length[0] + length[2] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 101, 109, 110, 111, 112, 148 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart65_check :
                                                                                                                                          treePart65.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 1, 0, 1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, -1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -2, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 0, 0, 1])]) = true

                                                                                                                                          Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 137, 149 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For

                                                                                                                                            Contradiction leaf using Farkas receipt 82 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                            Equations
                                                                                                                                            Instances For

                                                                                                                                              Contradiction leaf using Farkas receipt 1132 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                Contradiction leaf using Farkas receipt 1200 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  Contradiction leaf using Farkas receipt 1201 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For

                                                                                                                                                    Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 60, 98, 107, 123, 124, 132, 150, 151 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For

                                                                                                                                                      Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 60, 141, 150, 151, 152 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart72_check :

                                                                                                                                                        Contradiction leaf using Farkas receipt 1239 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For

                                                                                                                                                          Contradiction leaf using Farkas receipt 82 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            Contradiction leaf using Farkas receipt 1240 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              Contradiction leaf using Farkas receipt 386 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 54, 92, 102, 113, 114, 126, 153, 154 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For

                                                                                                                                                                  Subtree splitting on - length[0] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 54, 135, 153, 154, 155 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For

                                                                                                                                                                    Contradiction leaf using Farkas receipt 1201 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      Subtree splitting on - length[0] + length[2] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 55, 136, 156, 157, 158, 159 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For

                                                                                                                                                                        Subtree splitting on length[0] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 55, 97, 106, 121, 122, 131, 156 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart81_check :

                                                                                                                                                                          Contradiction leaf using Farkas receipt 1279 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For

                                                                                                                                                                            Contradiction leaf using Farkas receipt 82 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For

                                                                                                                                                                              Contradiction leaf using Farkas receipt 1132 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For

                                                                                                                                                                                Contradiction leaf using Farkas receipt 1201 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For

                                                                                                                                                                                  Subtree splitting on - length[0] + length[2] + length[3] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 62, 160, 161, 162, 163, 164 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Subtree splitting on length[0] - length[3] - length[5] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 62, 160, 165, 166, 167, 168, 169 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart87_check :

                                                                                                                                                                                      Contradiction leaf using Farkas receipt 1282 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Contradiction leaf using Farkas receipt 1283 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 59, 140, 170, 171, 172, 173 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart90_check :
                                                                                                                                                                                            treePart90.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 1, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, 1, 1, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 1, 0, -1, 0, -1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 1, -1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1]]) = true

                                                                                                                                                                                            Subtree splitting on - length[1] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 59, 96, 105, 118, 120, 130, 170 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart91_check :
                                                                                                                                                                                              treePart91.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [GenusFiveRow04CoverBase.aff [0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, -1, 1, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, 0, 1, 0, 1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, -1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 0, -1, -1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, -1, -1, 0, 1, 1, 0, 1])] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 1, 0, -1, 0, -1]] ++ [GenusFiveRow04CoverBase.aff [0, 0, 0, 0, 0, 0, 1, 0, 1, -1, -1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 0, -1, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (GenusFiveRow04CoverBase.aff [0, 1, 0, -1, -1, 0, -1, 0, 0, 0, 0, 0, 1])]) = true

                                                                                                                                                                                              Contradiction leaf using Farkas receipt 1299 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Contradiction leaf using Farkas receipt 1282 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  Contradiction leaf using Farkas receipt 82 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1132 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Contradiction leaf using Farkas receipt 1300 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                        Subtree splitting on length[5] - length[8] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 19, 142, 143, 151, 154, 157, 171, 174, 175, 176 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                          Contradiction leaf using Farkas receipt 1321 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                            Subtree splitting on length[5] - length[8] - length[10] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 144, 145, 177, 178, 179 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              Subtree splitting on - length[5] - length[6] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 158, 172, 177, 178, 180, 181, 182 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                Contradiction leaf using Farkas receipt 1345 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  Contradiction leaf using Farkas receipt 1346 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1347 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Subtree splitting on length[5] + length[6] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 154, 157, 158, 180 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                        Subtree splitting on - length[5] - length[6] + length[8] + length[9] + length[11] in the row-04 symmetry chamber, with leaves selecting cells 161, 162, 171, 172 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 151, 179 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                            Contradiction leaf using Farkas receipt 509 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              Contradiction leaf using Farkas receipt 1347 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                Contradiction leaf using Farkas receipt 1364 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 23, 134, 135, 136, 137, 138, 139, 140, 141 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1387 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                      Contradiction leaf using Farkas receipt 1388 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                        Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 137, 141, 149 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 135, 136 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                            Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 140, 163 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                              Contradiction leaf using Farkas receipt 1406 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 91, 92, 93, 94, 95, 96, 97, 98, 99 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  Contradiction leaf using Farkas receipt 1416 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1321 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 18, 125, 126, 127, 128, 129, 130, 131, 132 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                        Contradiction leaf using Farkas receipt 1430 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 93, 127, 146, 147 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                            Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 93, 98, 132 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                              Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 92, 97, 126, 131 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 17, 96, 130, 165, 166 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 49, 183, 184, 185, 186, 187, 188, 189, 190, 191 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1347 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                      Contradiction leaf using Farkas receipt 1364 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                        Subtree splitting on length[5] + length[6] + length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 22, 110, 114, 116, 119, 120, 122, 124, 192 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          theorem AtanasovRanganathan.GenusFiveRow04FixedCover.treePart131_check :

                                                                                                                                                                                                                                                                          Contradiction leaf using Farkas receipt 1486 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                            Contradiction leaf using Farkas receipt 1467 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                              Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 110, 112, 185, 193 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 124, 190 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                  Subtree splitting on - length[0] - length[2] + length[5] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 114, 122, 184, 189 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                    Contradiction leaf using Farkas receipt 1389 to exclude the accumulated affine constraints in this row-04 branch.

                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                      Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 188, 194 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                        Subtree splitting on length[5] - length[8] - length[9] - length[11] in the row-04 symmetry chamber, with leaves selecting cells 120, 169 and Farkas receipts excluding inconsistent sign branches.

                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                          A branch of the final row-04 cover assembly, starting at split form 1 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                            A branch of the final row-04 cover assembly, starting at split form 1 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                              A branch of the final row-04 cover assembly, starting at split form 11 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                A branch of the final row-04 cover assembly, starting at split form 7 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                  A branch of the final row-04 cover assembly, starting at split form 4 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                    A branch of the final row-04 cover assembly, starting at split form 2 and combining the previously verified decision subtrees.

                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      The complete compact decision tree for row 04 on the symmetry chamber, assembling 140 subtrees whose cell and Farkas certificates are replayed by the cover checker.

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                        On the chamber the eighteen active rows all hold: the first twelve because lengths are natural numbers, the last six by definition of the fundamental domain.

                                                                                                                                                                                                                                                                                                        Connectivity of the core, checked here so that the generated modules stay self-contained.