diff --git a/research/eisenstein-clique-copy-bound/CLAIM.md b/research/eisenstein-clique-copy-bound/CLAIM.md new file mode 100644 index 0000000000..63caf62b76 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/CLAIM.md @@ -0,0 +1,54 @@ +# Sprint claim + +- Track: structural decoder research; OS assignment seed **48**, drawn with + `secrets.randbelow(100)` at 2026-10-13 05:22:15 UTC. +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Object: scalar binary asymmetric decoders on the **40 Eisenstein E8 lines** + of PR620, charged by rational pairing rank divided by two. +- Method: reconstruct the rational order-three geometry, enumerate its + maximum nonorthogonality cliques and all line-matroid flats, then certify + the strongest uniform clique weight on every flat pair. Use the weighted + clique argument credited to PR703 and PR738, in this different geometry. +- Deliverable: a scoped copy-charge bound or exact limitation of this + method, a complete finite certificate, negative controls and a paid-format + optimistic screen. No new kappa is promised. +- Three candidates considered: (0) Eisenstein asymmetric copy cost; + (1) the remaining Gaussian decoder gap; (2) P112 decoders beyond frame + partitions. Recent Gaussian/P111 work makes (0) less crowded. Seed 48 + fixes the independent rank-control samples and distinguishes line 8 + (48 modulo 40) for the saturated-singleton dual rejection obligations. +- Prior work: PR620's extension-ring solver reports leave the asymmetric + Eisenstein cost unresolved. This changes the proof method and covers any + finite number of totals, rather than extending a timed-out solver run. + PR703 handles ten Hurwitz lines; PR738 handles 60 Gaussian lines; PR767 + handles Gaussian subclasses. None supplies the Eisenstein certificate. +- Coordination: no pinned issue existed at the fresh pre-claim check; + no separate reservation issue was opened. Open PR metadata through #769 + and the review ledger were inspected, including PR620's partial status + and PR446's unreviewed status. No matching Eisenstein/Witting claim was + found in the open PR search. +- Budget: 45 minutes from 05:22:15 UTC; stop investigation by 05:56 UTC + and reserve the final quarter for verification and handoff. Expected + finish: **2026-10-13 06:07 UTC**. Stop after the complete finite clique/flat + domain; do not broaden to other geometries or claim decoder optimality. +- Contributor: Jonathan Lam (@jonathanlam), with substantial OpenAI Codex + assistance in research, implementation and verification; Apache-2.0. + +## One result update — 2026-10-13 05:48 UTC + +Completed: **C ≥ 22 Eisenstein rank units**, and an exact matching dual proves +that *all* nonnegative clique-weight certificates have optimum 22. The actual +decoder optimum remains in [22,40]; no new κ is claimed. The same finite +domain gave one refinement: the maximum-clique-only bound 280/13 saturated, +so singleton inequalities were added, and the resulting all-clique dual +closed this proof method at 22. No other geometry or supplier was searched. + +Coverage: 772 flats, 298,378 unordered flat pairs, 40,054 cliques, eight +mathematical controls, and an independent modular/Fraction arithmetic check. +Python 3.11/3.12 replay, three packaging tests and selected-record integrity +passed. Final PR metadata covered 614 open PRs through #795 with no matching +Eisenstein contribution. Origin/main remains at the claimed base. + +Deliverable: [proof and reproduction](README.md), [validation](VALIDATION.md), +and the [focused contribution branch](https://github.com/jonathanlam/integer-mult-bounds/tree/research/eisenstein-clique-bound-seed48/research/eisenstein-clique-copy-bound). +One research-note PR is the intended handoff; no frontier edit or merge. diff --git a/research/eisenstein-clique-copy-bound/PROOF.md b/research/eisenstein-clique-copy-bound/PROOF.md new file mode 100644 index 0000000000..5c5fd2f87c --- /dev/null +++ b/research/eisenstein-clique-copy-bound/PROOF.md @@ -0,0 +1,198 @@ +# Eisenstein E8: copy charge at least 22, and a sharp limit of clique certificates + +This is a theorem about a specified finite decoder model. It is not a new +supplier, a proof of decoder optimality, or a new multiplication exponent. +The weighted-clique argument follows the distinct Hurwitz and Gaussian +geometries of [PR703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) +and [PR738](https://github.com/CrocSwap/integer-mult-bounds/pull/738). +The new result is the exact primal/dual certificate for the **40-line +Eisenstein geometry**, including a bound on *all* clique-weight certificates. + +## Model and geometry + +Start with the 240 E8 roots in doubled coordinates: vectors with two entries +equal to ±2 and all other entries zero, and the vectors in {±1}^8 with an even +number of minus signs. Each root has squared norm eight. + +Following Joel Pulikkan / GamingPuzzled's archived PR620, choose four mutually +orthogonal A2 planes, with roots (a,b) satisfying a·b = -4, and let J be the +product of their rotations s_a s_b. The literal pairs are in the certificate. +The independent implementation uses the same root order and greedy choices +as the pinned predecessor, so it defines the same rational action, not merely +a configuration with similar counts. The reflection formula is + + s_a(x) = x - (x·a)a/4. + +The exact checks establish J^3 = I, J^2 + J + I = 0, and preservation of the +inner product and root set. Thus Q^8 is a four-dimensional vector space over +K = Q(ω), with multiplication by ω realized by J. The root orbits under ±J +partition the roots into 40 K-lines. For a line set S, let X_S be the rational +span of r_i,Jr_i for i in S. Every X_S is J-invariant. + +Two distinct lines are nonorthogonal if r_i·r_j or r_i·Jr_j is nonzero. Each +line has 27 such neighbors. Let B be an arbitrary 40×40 matrix over F2 with + + B_tt = 1; + B_ts = 0 if distinct lines t,s are nonorthogonal. + +The other directed entries are unconstrained. Consider any finite decomposition + + B = Σ_j 1_(R_j) 1_(A_j)^T over F2. + +There is no symmetry, minimal-rank, or number-of-totals restriction. For any +row bases V_R,V_A of the rational spans, define the abstract copy charge + + c(R,A) = rank_Q(V_R V_A^T)/2, C = Σ_j c(R_j,A_j). + +This is a *pairing* rank; it need not equal either support's span dimension. +The rank is even: the kernel X_R ∩ X_A^⊥ is J-invariant, because J is an +isometry and X_A is J-invariant. Both domain and kernel are K-spaces. +Consequently each c is an integer. Translating this abstract charge into a +physical copy lower bound inherits PR446's premise, which the base review +ledger marks unreviewed. The finite algebraic result needs no such premise. + +## General clique bound and the lower certificate + +A clique Q is a set of pairwise nonorthogonal lines. The fitting rules give +B[Q,Q] = I. A binary rectangle restricted to Q×Q has rank one exactly when +both supports meet Q. Rank subadditivity gives + + |Q| ≤ Σ_j [Q∩R_j ≠ ∅ and Q∩A_j ≠ ∅]. (1) + +For each nonempty clique assign a nonnegative rational weight λ_Q. Suppose +these weights satisfy, for all supports R,A, + + Σ_Q λ_Q [Q meets R and A] ≤ c(R,A). (2) + +Multiplying (1) by λ_Q and summing proves C ≥ Σ_Q λ_Q |Q|. + +The certificate uses weight **1/40 on each singleton** and **1/960 on each +of the 2,880 seven-line cliques**, with weight zero elsewhere. The resulting +objective is exactly + + 40/40 + 2,880·7/960 = 22. (3) + +To certify (2), close R and A in the line matroid: cl(S) contains every +configuration line lying in X_S. Closure leaves X_S, hence the pairing rank, +unchanged. It can only increase the clique-hit indicators. Therefore it is +sufficient to check every pair of flats F,G. Write H_7(F,G) for the number +of seven-line cliques meeting both flats. The required integer inequality is + + 24 |F∩G| + H_7(F,G) ≤ 960 c(F,G). (4) + +The replay verifies (4) by exact rational rank on all **298,378 unordered +pairs of the 772 flats**, including the empty flat. Symmetry of the pairing +rank and hit count covers both orders. This is a complete reduction from +arbitrary supports; the theorem does not assume supports were originally +flats. Equations (1)–(4) prove **C ≥ 22** for every finite decomposition. + +## Why no weighting of cliques can prove more + +The following upper bound concerns the certificate method, not decoder cost. +Let P consist of the **240 unordered pairs** F,G of twelve-line, rank-three +flats with c(F,G)=2. Each such pair has |F∩G|=2 and H_7(F,G)=1,872, so (4) +is tight. Give each of these pairs dual weight 1/24; give the full/full +pair dual weight 1/2. Its cost is + + (240·2)/24 + 4/2 = 22. (5) + +For *every literal nonempty clique* Q, the certificate verifies + + 1/2 + #{(F,G) in P : Q meets F and G}/24 ≥ |Q|. (6) + +The complete incidence census is below. In particular, no unproved +transitivity assumption or orbit-averaging argument is needed. + +| Clique size | Dual pairs hit | Number of cliques | +|---:|---:|---:| +| 1 | 12 | 40 | +| 2 | 48 | 540 | +| 3 | 81 | 2,880 | +| 3 | 108 | 360 | +| 4 | 106 | 6,480 | +| 4 | 123 | 2,880 | +| 4 | 192 | 90 | +| 5 | 125 | 5,184 | +| 5 | 134 | 8,640 | +| 6 | 145 | 10,080 | +| 7 | 156 | 2,880 | + +Now take *any* nonnegative clique weights satisfying (2), including arbitrary +nonuniform weights on smaller cliques. Multiply (6) by λ_Q, sum over Q, +and apply (2) to the full/full pair and each pair in P. Equation (5) gives + + Σ_Q λ_Q |Q| ≤ 22. + +Together with (3), this proves that the optimum of the entire weighted-clique +certificate method is exactly **22**. A stronger copy lower bound will need +an ingredient beyond inequalities (1)–(2). In particular, using more clique +weights or a different clique-weight optimizer alone cannot improve it. + +## Decoder bounds and the optimistic accounting screen + +Every fitting B has an abstract cost-40 decomposition: for each row t, +take R={t} and A equal to that row's nonzero positions. A contains t; every +other member of A is orthogonal to t. The rational Gram block therefore has +rank two, so this row costs one. These 40 rectangles reproduce B. Hence the +minimum charge lies in **[22,40]**. The lower endpoint is attained by a +*certificate*, and no cost-22 decoder is constructed. + +For the separate Dfc stage accounting in the pinned format notes, v=40, +each line has rational rank k=2, and cst=2C. Thus, conditionally on that +accounting and the physical interpretation of the charge, + + D/T = (s-1)vk - s·cst ≤ 80(s-1) - 44s = 36s-80. + +At s=3 the upper deficit is 28, which is positive. This lower bound **does +not exclude three stages**. A positive three-stage deficit would require +C < 80/3; integrality narrows the unresolved possibilities to C=22,...,26. +All helpers, source access, frame changes, copies beyond this lower bound, +restoration and recursive children would still have to be paid. None is +implemented or assumed free in an achieved construction. At the cost-40 +row decomposition the deficit is -80 for every stage count, so that abstract +upper-bound witness itself cannot supply a saving under Dfc. + +The selected #626/#543 composition remains complex-bound. This research +does not provide a replacement supplier or change any assembly constraint. + +## Completeness and proof boundary + +Flats are generated from the empty span by adding one root line and taking +exact rational span/closure. Any flat has a line basis, so induction on basis +size proves this generates every flat in four K-dimensions. The verifier +also checks all 30,880 one-line extensions remain in the enumerated set. +The flat counts by (K-rank, number of lines) are + + (0,0):1; (1,1):40; (2,2):240; (2,4):90; + (3,5):360; (3,12):40; (4,40):1. + +All nonempty cliques are generated once by successively adjoining larger +vertices adjacent to every previous vertex. This recursion exhausts every +ordered increasing clique. A separate Bron–Kerbosch maximal-clique census +corroborates the 2,880 maximum cliques and 90 smaller maximal cliques. + +The committed certificate contains the literal flat generators, maximum +cliques, all 240 dual pairs, complete pair/incidence censuses, and hashes of +the regenerated root orbits and all 40,054 cliques. The replay uses no solver. +An ordinary Fraction elimination on original root generators checks 258 +seeded/boundary Gram blocks independently of the integer RREF implementation. +Eight mathematical negative controls cover fitting identities, clique +admission, rank accounting, and both primal and dual weights/coverage. + +The separate `crosscheck.py` imports neither implementation. It checks all +298,378 primal inequalities on original integer generators using rank modulo +101. Such a rank is a lower bound on rational rank, which is the sufficient +direction for (4). It checks all 240 dual-pair costs and the full-pair cost +by exact Fraction elimination. Geometry and enumeration completeness remain +the responsibilities of the main replay and the preceding argument. + +This is a written proof with exhaustive finite premises, not a proof-assistant +formalization or a finite replay claimed to prove the full multiplication +theorem. Whole K-lines, scalar binary totals and the stated fitting pattern +are essential to the scope. Sub-line/vector-valued operations, different +decoder patterns or geometries, physical realization, all-size compilation, +hosting, precision, tape and analytic transfer remain outside it. + +Prepared by Jonathan Lam (@jonathanlam) with substantial OpenAI Codex +assistance. See [SOURCES.json](SOURCES.json) for exact pins and predecessor +credit. New material is Apache-2.0 under the repository license. diff --git a/research/eisenstein-clique-copy-bound/README.md b/research/eisenstein-clique-copy-bound/README.md new file mode 100644 index 0000000000..ed6b996934 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/README.md @@ -0,0 +1,76 @@ +# Research note: Eisenstein E8 copy floor and clique-method limit + +**Every scalar binary decoder on the 40 Eisenstein E8 lines costs at least +22 Eisenstein pairing-rank units (44 rational units).** The best certificate +using arbitrary nonnegative weights on nonorthogonality cliques proves +exactly 22. This identifies a precise limit of that proof method. + +The abstract decoder optimum remains in **[22,40]**. No cost-22 decoder, +paid supplier or new κ is claimed. Under the inherited Dfc accounting, a +three-stage construction with positive deficit would need integer copy +cost 22–26. This result does not decide whether such a decoder exists. + +From the repository root, using Python 3.10+ and only the standard library: + +```sh +python3 -B research/eisenstein-clique-copy-bound/verify.py +``` + +Expected output: + +```text +PASS_EISENSTEIN_CLIQUE_COPY_BOUND: cost >= 22; clique-method optimum 22; 298378 flat pairs; 40054 cliques; 8 negative controls; no new kappa +``` + +The replay takes about 16 seconds on the development Linux host, verifies +the committed certificate, and leaves the checkout unchanged. Optional +`--write /tmp/eisenstein-replay.json` exports the receipt only after checking +it. Optimized Python is supported; checks do not depend on `assert`. + +Read [PROOF.md](PROOF.md) for the model, completeness argument and exact +primal/dual proof. [certificate.json](certificate.json) gives the literal +finite evidence. [SOURCES.json](SOURCES.json) records source hashes and +attribution; [CLAIM.md](CLAIM.md) records seed, scope and sprint handoff. + +Additional verification commands: + +```sh +python3 -B research/eisenstein-clique-copy-bound/crosscheck.py +python3 -B research/eisenstein-clique-copy-bound/test_verify.py +``` + +The first independently checks every primal inequality using ranks modulo +101 and all 241 dual costs using Fraction arithmetic; it imports no package +implementation. The second runs three tests for relocated optimized replay, +corrupt-certificate rejection and source-pin rejection. See +[VALIDATION.md](VALIDATION.md) for the checks actually run and their scope. + +The experiment exhausted all 772 line-spanned flats, all 298,378 unordered +flat pairs including empty supports, and all 40,054 nonempty cliques. It +stopped after this finite domain and its exact certificate. Seed **48** +controls the additional Fraction cross-checks and the distinguished line +for dual rejection controls. A discovery LP nominated the rational coefficients; the +reproduction command has no optimizer or numerical-infeasibility dependency. + +PR620's archived extension-ring report supplied the geometry and reported +the earlier lower bound of 9. Its solver/barrier claims were only partially +reviewed; they are not premises of this proof. Douglas R. Colkitt's PR703 +and Sagar Thakrar's PR738 supplied the weighted-clique method in the distinct +Hurwitz and Gaussian geometries. This package adds the Eisenstein certificate +and its matching upper certificate over *all* clique weights. None of their +implementations is imported or executed. DreamingOfClouds' PR446 pairing-rank +premise and PR595 format accounting are inherited only for the conditional +physical interpretation and stage screen. The E8 and wider community lineage +retains its predecessor credit. + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected conditional +κ there is `51110230636731/31250000000000000`, from #626 with #543. This +package changes no existing supplier, generator, selected pointer or +`upstream/` file. The finite algebraic result does not discharge the selected +construction's compiler, realization, hosting, precision, tape or analytic +assumptions. No full multiplication proof or independent human review is +claimed. + +Prepared by Jonathan Lam (@jonathanlam), with substantial OpenAI Codex +assistance in mathematics, implementation, verification and documentation. +New material is licensed under the repository's Apache-2.0 license. diff --git a/research/eisenstein-clique-copy-bound/SOURCES.json b/research/eisenstein-clique-copy-bound/SOURCES.json new file mode 100644 index 0000000000..1193b0af04 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/SOURCES.json @@ -0,0 +1,90 @@ +{ + "attribution": "Jonathan Lam (@jonathanlam), with substantial OpenAI Codex assistance in research, implementation and verification. Apache-2.0. All preceding E8, scalar/frame/copy, compiler and community work retains its credit.", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "context_inputs": [ + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "certificates/selected-result.json", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "docs/research/community-k492-review.md", + "sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + }, + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/community-k492-audit/pr626/replay/ASSEMBLY.json", + "sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e" + } + ], + "context_policy": "Context pins identify the selected result at the base; replay authenticates only the archived mathematical input files, so future selected-frontier changes do not invalidate this independent result.", + "discovery": "A ten-variable SciPy/HiGHS LP, grouped by clique size and span rank, nominated rational coefficients. Exact primal and literal-clique dual inequalities certify the full nonuniform method without SciPy, symmetry assumptions, or solver-status premises.", + "local_inputs": [ + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/algebra_lines.py", + "sha256": "bc4037049debf9b7affeb7e6b30da0193dea8c3850a7317afd045ac7ac481108" + }, + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md", + "sha256": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02" + }, + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/e8-decoder-floors-and-cold14-notes/s2-decoder/e8units.py", + "sha256": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1" + }, + { + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/format-limits-corrected/README.md", + "sha256": "1bcd80c1cd61fddae9f3a7f00fc9d1c796410408251e576600e94c19b16b1e5e" + } + ], + "predecessors": [ + { + "author": "Joel Pulikkan / GamingPuzzled", + "head_observed_at_start": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "pr": 620, + "role": "Eisenstein E8 geometry, prior extension-ring screens, pairing-rank model and scaling. Archived source used, not the changed live head. Ledger: partially reviewed.", + "source_head_on_base": "419c7374c3bf5f2eee28f08b1e50c1d57934081c" + }, + { + "author": "Douglas R. Colkitt / Mister-Meeseeks", + "commit": "358383e2f1b0f292d4d6eb897c06fd8558a4f5e6", + "path": "research/hurwitz-asymmetric-copy-floor/PROOF.md", + "pr": 703, + "role": "Weighted clique/transversal rank method for the distinct ten-line Hurwitz geometry; proof read, no code imported.", + "sha256": "7355fcb0eadef64ffd7909e6c3d7717d5a3fb2628449fa3c6c754cb2a5665585" + }, + { + "author": "Sagar Thakrar / thakrarsagar", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "path": "research/gaussian-clique-copy-bound/PROOF.md", + "pr": 738, + "role": "Weighted-clique flat closure argument for the distinct 60-line Gaussian geometry; proof read, no code imported.", + "sha256": "e33a3950f172bc93400fffd85df55236059f5391d4ed8a82e0f12bcd7f196812" + }, + { + "author": "DreamingOfClouds", + "head_observed_at_start": "309482849b6ddf34db998f53612d34c19f6e3233", + "pr": 446, + "role": "Physical pairing-rank copy premise, as cited by the archived format notes. Ledger: unreviewed; not independently established here." + }, + { + "author": "DreamingOfClouds", + "head_observed_at_start": "39112c2577452fa278489fb9fd77a9aecb2cdc24", + "pr": 595, + "role": "Dfc accounting context; the exact source consumed is the pinned local corrected README, not the live PR." + } + ], + "runtime_dependencies": "Python >= 3.10 standard library only. No solver, network, or predecessor code execution.", + "selected_context": { + "bit_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "bit_pr": 543, + "complex_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "complex_pr": 626, + "kappa": "51110230636731/31250000000000000" + } +} diff --git a/research/eisenstein-clique-copy-bound/VALIDATION.md b/research/eisenstein-clique-copy-bound/VALIDATION.md new file mode 100644 index 0000000000..076359da8f --- /dev/null +++ b/research/eisenstein-clique-copy-bound/VALIDATION.md @@ -0,0 +1,45 @@ +# Validation and handoff + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Local platform: Linux 6.6.87.2, x86_64, WSL2. Checks completed on +2026-10-13. New work is confined to this research package. + +| Check | Observed result | +|---|---| +| `python3 -B research/eisenstein-clique-copy-bound/verify.py --write /tmp/intmul-eisenstein-replay-seed48.json` | PASS on Python 3.12.3; committed certificate reproduced | +| `python3.11 -O -B research/eisenstein-clique-copy-bound/verify.py` | Identical certificate and PASS on Python 3.11.15 | +| `python3 -O -B research/eisenstein-clique-copy-bound/crosscheck.py` | PASS: 298,378 modular primal inequalities and 241 exact Fraction dual costs | +| `python3 -B research/eisenstein-clique-copy-bound/test_verify.py` | Three tests OK: relocated minimal-input optimized replay/export; corrupted dual receipt rejection; modified source rejection; output preserved on failure | +| `make selected-record-check` | PASS: selected record, exact κ, original source inventory and proof supplements | +| Python parsing, package links and staged whitespace | PASS | + +The main receipt contains eight mathematical rejection controls and the full +finite coverage. The modular checker imports no package implementation; its +rank lower bounds suffice for the primal inequalities, while its Fraction +engine checks the dual costs exactly. This corroborates the arithmetic; +the written proof and main replay supply the geometry/completeness reduction. + +The main replay and tests use only Python's standard library. The discovery +LP is unnecessary to reproduce or verify the result. No proof-assistant, +independent human review, hosted CI pass, repository-wide `make verify`, or +selected supplier cold-replay pass is claimed. Those expensive supplier +checks were not repeated because this adds a separate research certificate +without changing a supplier, generator, assembly, or selected-frontier input. + +The final fetch left `origin/main` at the recorded base. The pre-submission +metadata refresh covered **614 open PRs through #795**, plus an all-state +Eisenstein/Witting search. No competing Eisenstein result was found. PR703 +and PR738 retained the pinned heads; PR767 concerns Gaussian subclasses, +and PR785 extends the Hurwitz model to fixed-support nonlinear messages. +They are related work in different geometries/models, not this certificate. + +The completed result is **C ≥ 22**, with **22 the exact optimum of the +weighted-clique certificate method**. The actual decoder optimum remains +in [22,40]. The distinction is essential: no cost-22 decoder or new κ is +claimed. Under the stated physical/accounting premises, costs 22–26 remain +unexcluded candidates for a positive three-stage deficit; implementation +and all remaining expenses are unresolved. + +Prepared by Jonathan Lam (@jonathanlam) with substantial OpenAI Codex +assistance. Predecessor contributions and their review status are pinned +in [SOURCES.json](SOURCES.json). Apache-2.0. diff --git a/research/eisenstein-clique-copy-bound/certificate.json b/research/eisenstein-clique-copy-bound/certificate.json new file mode 100644 index 0000000000..3f2d9f7141 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/certificate.json @@ -0,0 +1,11845 @@ +{ + "abstract_decoder_cost_interval": [ + 22, + 40 + ], + "all_clique_weight_certificate_optimum": "22", + "assignment_seed": 48, + "asymmetric_positive_control_sha256": "bb631473c9af3d5d851b87d5b58ad06d04d855af28ff07dd9b047fadb5e1f4e0", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "dual": { + "clique_hit_census": [ + [ + 1, + 12, + 40 + ], + [ + 2, + 48, + 540 + ], + [ + 3, + 81, + 2880 + ], + [ + 3, + 108, + 360 + ], + [ + 4, + 106, + 6480 + ], + [ + 4, + 123, + 2880 + ], + [ + 4, + 192, + 90 + ], + [ + 5, + 125, + 5184 + ], + [ + 5, + 134, + 8640 + ], + [ + 6, + 145, + 10080 + ], + [ + 7, + 156, + 2880 + ] + ], + "cliques_checked": 40054, + "flat_pairs": [ + [ + 75456735744, + 51741724167 + ], + [ + 75470733620, + 51741724167 + ], + [ + 75564683466, + 51741724167 + ], + [ + 78946500812, + 51741724167 + ], + [ + 78946500812, + 75470733620 + ], + [ + 78959975424, + 51741724167 + ], + [ + 78959975424, + 75456735744 + ], + [ + 78987288882, + 51741724167 + ], + [ + 78987288882, + 75564683466 + ], + [ + 85925663025, + 51741724167 + ], + [ + 103119216841, + 51741724167 + ], + [ + 103119216841, + 85925663025 + ], + [ + 141873926737, + 12935432583 + ], + [ + 141873926737, + 78946500812 + ], + [ + 141873926737, + 78959975424 + ], + [ + 141873926737, + 78987288882 + ], + [ + 146106786857, + 12935432583 + ], + [ + 146106786857, + 75456735744 + ], + [ + 146106786857, + 75470733620 + ], + [ + 146106786857, + 75564683466 + ], + [ + 146106786857, + 141873926737 + ], + [ + 157320258130, + 12935432583 + ], + [ + 157320258130, + 75470733620 + ], + [ + 157320258130, + 78959975424 + ], + [ + 157320258130, + 103119216841 + ], + [ + 157381318912, + 12935432583 + ], + [ + 157381318912, + 75564683466 + ], + [ + 157381318912, + 78946500812 + ], + [ + 157381318912, + 103119216841 + ], + [ + 157442704428, + 12935432583 + ], + [ + 157442704428, + 75456735744 + ], + [ + 157442704428, + 78987288882 + ], + [ + 157442704428, + 103119216841 + ], + [ + 173174969386, + 12935432583 + ], + [ + 173174969386, + 75456735744 + ], + [ + 173174969386, + 78946500812 + ], + [ + 173174969386, + 85925663025 + ], + [ + 173174969386, + 157320258130 + ], + [ + 173218595412, + 12935432583 + ], + [ + 173218595412, + 75564683466 + ], + [ + 173218595412, + 78959975424 + ], + [ + 173218595412, + 85925663025 + ], + [ + 173218595412, + 157442704428 + ], + [ + 173280635008, + 12935432583 + ], + [ + 173280635008, + 75470733620 + ], + [ + 173280635008, + 78987288882 + ], + [ + 173280635008, + 85925663025 + ], + [ + 173280635008, + 157381318912 + ], + [ + 276053759121, + 3233859687 + ], + [ + 276053759121, + 75456735744 + ], + [ + 276053759121, + 75470733620 + ], + [ + 276053759121, + 75564683466 + ], + [ + 276053759121, + 157320258130 + ], + [ + 276053759121, + 157381318912 + ], + [ + 276053759121, + 157442704428 + ], + [ + 277179081481, + 3233859687 + ], + [ + 277179081481, + 78946500812 + ], + [ + 277179081481, + 78959975424 + ], + [ + 277179081481, + 78987288882 + ], + [ + 277179081481, + 173174969386 + ], + [ + 277179081481, + 173218595412 + ], + [ + 277179081481, + 173280635008 + ], + [ + 277179081481, + 276053759121 + ], + [ + 300924932874, + 3233859687 + ], + [ + 300924932874, + 75470733620 + ], + [ + 300924932874, + 78959975424 + ], + [ + 300924932874, + 103119216841 + ], + [ + 300924932874, + 141873926737 + ], + [ + 300924932874, + 157442704428 + ], + [ + 300924932874, + 173280635008 + ], + [ + 301018458144, + 3233859687 + ], + [ + 301018458144, + 75564683466 + ], + [ + 301018458144, + 78946500812 + ], + [ + 301018458144, + 103119216841 + ], + [ + 301018458144, + 141873926737 + ], + [ + 301018458144, + 157320258130 + ], + [ + 301018458144, + 173218595412 + ], + [ + 301069272212, + 3233859687 + ], + [ + 301069272212, + 75456735744 + ], + [ + 301069272212, + 78987288882 + ], + [ + 301069272212, + 103119216841 + ], + [ + 301069272212, + 141873926737 + ], + [ + 301069272212, + 157381318912 + ], + [ + 301069272212, + 173174969386 + ], + [ + 314074277010, + 3233859687 + ], + [ + 314074277010, + 75456735744 + ], + [ + 314074277010, + 78946500812 + ], + [ + 314074277010, + 85925663025 + ], + [ + 314074277010, + 146106786857 + ], + [ + 314074277010, + 157381318912 + ], + [ + 314074277010, + 173218595412 + ], + [ + 314074277010, + 300924932874 + ], + [ + 314171212556, + 3233859687 + ], + [ + 314171212556, + 75564683466 + ], + [ + 314171212556, + 78959975424 + ], + [ + 314171212556, + 85925663025 + ], + [ + 314171212556, + 146106786857 + ], + [ + 314171212556, + 157320258130 + ], + [ + 314171212556, + 173280635008 + ], + [ + 314171212556, + 301069272212 + ], + [ + 314222975040, + 3233859687 + ], + [ + 314222975040, + 75470733620 + ], + [ + 314222975040, + 78987288882 + ], + [ + 314222975040, + 85925663025 + ], + [ + 314222975040, + 146106786857 + ], + [ + 314222975040, + 157442704428 + ], + [ + 314222975040, + 173174969386 + ], + [ + 314222975040, + 301018458144 + ], + [ + 550201098913, + 808466463 + ], + [ + 550201098913, + 78946500812 + ], + [ + 550201098913, + 78959975424 + ], + [ + 550201098913, + 78987288882 + ], + [ + 550201098913, + 157320258130 + ], + [ + 550201098913, + 157381318912 + ], + [ + 550201098913, + 157442704428 + ], + [ + 550201098913, + 314074277010 + ], + [ + 550201098913, + 314171212556 + ], + [ + 550201098913, + 314222975040 + ], + [ + 550381110593, + 808466463 + ], + [ + 550381110593, + 75456735744 + ], + [ + 550381110593, + 75470733620 + ], + [ + 550381110593, + 75564683466 + ], + [ + 550381110593, + 173174969386 + ], + [ + 550381110593, + 173218595412 + ], + [ + 550381110593, + 173280635008 + ], + [ + 550381110593, + 300924932874 + ], + [ + 550381110593, + 301018458144 + ], + [ + 550381110593, + 301069272212 + ], + [ + 550381110593, + 550201098913 + ], + [ + 572305785506, + 808466463 + ], + [ + 572305785506, + 75470733620 + ], + [ + 572305785506, + 78959975424 + ], + [ + 572305785506, + 103119216841 + ], + [ + 572305785506, + 146106786857 + ], + [ + 572305785506, + 157381318912 + ], + [ + 572305785506, + 173218595412 + ], + [ + 572305785506, + 277179081481 + ], + [ + 572305785506, + 301069272212 + ], + [ + 572305785506, + 314222975040 + ], + [ + 572393162768, + 808466463 + ], + [ + 572393162768, + 75564683466 + ], + [ + 572393162768, + 78946500812 + ], + [ + 572393162768, + 103119216841 + ], + [ + 572393162768, + 146106786857 + ], + [ + 572393162768, + 157442704428 + ], + [ + 572393162768, + 173174969386 + ], + [ + 572393162768, + 277179081481 + ], + [ + 572393162768, + 300924932874 + ], + [ + 572393162768, + 314171212556 + ], + [ + 572480558404, + 808466463 + ], + [ + 572480558404, + 75456735744 + ], + [ + 572480558404, + 78987288882 + ], + [ + 572480558404, + 103119216841 + ], + [ + 572480558404, + 146106786857 + ], + [ + 572480558404, + 157320258130 + ], + [ + 572480558404, + 173280635008 + ], + [ + 572480558404, + 277179081481 + ], + [ + 572480558404, + 301018458144 + ], + [ + 572480558404, + 314074277010 + ], + [ + 594855757122, + 808466463 + ], + [ + 594855757122, + 75456735744 + ], + [ + 594855757122, + 78946500812 + ], + [ + 594855757122, + 85925663025 + ], + [ + 594855757122, + 141873926737 + ], + [ + 594855757122, + 157442704428 + ], + [ + 594855757122, + 173280635008 + ], + [ + 594855757122, + 276053759121 + ], + [ + 594855757122, + 301018458144 + ], + [ + 594855757122, + 314171212556 + ], + [ + 594855757122, + 572305785506 + ], + [ + 594941059748, + 808466463 + ], + [ + 594941059748, + 75564683466 + ], + [ + 594941059748, + 78959975424 + ], + [ + 594941059748, + 85925663025 + ], + [ + 594941059748, + 141873926737 + ], + [ + 594941059748, + 157381318912 + ], + [ + 594941059748, + 173174969386 + ], + [ + 594941059748, + 276053759121 + ], + [ + 594941059748, + 300924932874 + ], + [ + 594941059748, + 314222975040 + ], + [ + 594941059748, + 572480558404 + ], + [ + 595029477384, + 808466463 + ], + [ + 595029477384, + 75470733620 + ], + [ + 595029477384, + 78987288882 + ], + [ + 595029477384, + 85925663025 + ], + [ + 595029477384, + 141873926737 + ], + [ + 595029477384, + 157320258130 + ], + [ + 595029477384, + 173218595412 + ], + [ + 595029477384, + 276053759121 + ], + [ + 595029477384, + 301069272212 + ], + [ + 595029477384, + 314074277010 + ], + [ + 595029477384, + 572393162768 + ], + [ + 1030792153080, + 808466463 + ], + [ + 1030792153080, + 3233859687 + ], + [ + 1030792153080, + 12935432583 + ], + [ + 1030792153080, + 51741724167 + ], + [ + 1030792153080, + 75456735744 + ], + [ + 1030792153080, + 78959975424 + ], + [ + 1030792153080, + 157381318912 + ], + [ + 1030792153080, + 173280635008 + ], + [ + 1030792153080, + 301018458144 + ], + [ + 1030792153080, + 314222975040 + ], + [ + 1030792153080, + 572393162768 + ], + [ + 1030792153080, + 595029477384 + ], + [ + 1030793195520, + 808466463 + ], + [ + 1030793195520, + 3233859687 + ], + [ + 1030793195520, + 12935432583 + ], + [ + 1030793195520, + 51741724167 + ], + [ + 1030793195520, + 75470733620 + ], + [ + 1030793195520, + 78946500812 + ], + [ + 1030793195520, + 157442704428 + ], + [ + 1030793195520, + 173218595412 + ], + [ + 1030793195520, + 301069272212 + ], + [ + 1030793195520, + 314171212556 + ], + [ + 1030793195520, + 572480558404 + ], + [ + 1030793195520, + 594941059748 + ], + [ + 1031059537920, + 808466463 + ], + [ + 1031059537920, + 3233859687 + ], + [ + 1031059537920, + 12935432583 + ], + [ + 1031059537920, + 51741724167 + ], + [ + 1031059537920, + 75564683466 + ], + [ + 1031059537920, + 78987288882 + ], + [ + 1031059537920, + 157320258130 + ], + [ + 1031059537920, + 173174969386 + ], + [ + 1031059537920, + 300924932874 + ], + [ + 1031059537920, + 314074277010 + ], + [ + 1031059537920, + 572305785506 + ], + [ + 1031059537920, + 594855757122 + ], + [ + 1099243192320, + 808466463 + ], + [ + 1099243192320, + 3233859687 + ], + [ + 1099243192320, + 12935432583 + ], + [ + 1099243192320, + 51741724167 + ], + [ + 1099243192320, + 85925663025 + ], + [ + 1099243192320, + 103119216841 + ], + [ + 1099243192320, + 141873926737 + ], + [ + 1099243192320, + 146106786857 + ], + [ + 1099243192320, + 276053759121 + ], + [ + 1099243192320, + 277179081481 + ], + [ + 1099243192320, + 550201098913 + ], + [ + 1099243192320, + 550381110593 + ] + ], + "full_pair_weight": "1/2", + "objective": "22", + "pair_weight": "1/24" + }, + "geometry": { + "J_images": [ + [ + -2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + -1, + -1, + -1, + 1, + 1, + 1 + ], + [ + -1, + 1, + -1, + -1, + 1, + -1, + -1, + -1 + ], + [ + -1, + 1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + -1, + 1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + -1, + 1, + -1, + -1, + -1, + -1, + -1, + 1 + ], + [ + -1, + 1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + [ + -1, + 1, + -1, + -1, + -1, + 1, + -1, + -1 + ], + [ + -1, + 1, + -1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 0, + 0, + -2, + 2, + 0, + 0, + 0, + 0 + ], + [ + -1, + -1, + -1, + 1, + -1, + 1, + 1, + 1 + ], + [ + -1, + -1, + -1, + 1, + 1, + -1, + -1, + -1 + ], + [ + -1, + -1, + -1, + 1, + -1, + -1, + 1, + -1 + ], + [ + -1, + -1, + -1, + 1, + 1, + 1, + -1, + 1 + ], + [ + -1, + -1, + -1, + 1, + -1, + -1, + -1, + 1 + ], + [ + -1, + -1, + -1, + 1, + 1, + 1, + 1, + -1 + ], + [ + -1, + -1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + [ + -1, + -1, + -1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 1 + ], + [ + 1, + 1, + -1, + 1, + 1, + 1, + 1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + -1, + -1 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + -2, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + -2, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2 + ] + ], + "a2_pairs": [ + [ + [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1 + ] + ], + [ + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + -1, + -1 + ] + ], + [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2 + ] + ] + ], + "all_cliques_sha256": "c46031cc92f1492524865439f6d8d307f8913e498a53999aee55b8c4d8c48ec1", + "clique_census": [ + [ + 1, + 40 + ], + [ + 2, + 540 + ], + [ + 3, + 3240 + ], + [ + 4, + 9450 + ], + [ + 5, + 13824 + ], + [ + 6, + 10080 + ], + [ + 7, + 2880 + ] + ], + "flat_census": [ + [ + 0, + 0, + 1 + ], + [ + 1, + 1, + 40 + ], + [ + 2, + 2, + 240 + ], + [ + 2, + 4, + 90 + ], + [ + 3, + 5, + 360 + ], + [ + 3, + 12, + 40 + ], + [ + 4, + 40, + 1 + ] + ], + "flats": [ + { + "generators": [], + "mask": 0, + "rank": 0 + }, + { + "generators": [ + 0 + ], + "mask": 1, + "rank": 1 + }, + { + "generators": [ + 1 + ], + "mask": 2, + "rank": 1 + }, + { + "generators": [ + 2 + ], + "mask": 4, + "rank": 1 + }, + { + "generators": [ + 3 + ], + "mask": 8, + "rank": 1 + }, + { + "generators": [ + 4 + ], + "mask": 16, + "rank": 1 + }, + { + "generators": [ + 5 + ], + "mask": 32, + "rank": 1 + }, + { + "generators": [ + 6 + ], + "mask": 64, + "rank": 1 + }, + { + "generators": [ + 7 + ], + "mask": 128, + "rank": 1 + }, + { + "generators": [ + 8 + ], + "mask": 256, + "rank": 1 + }, + { + "generators": [ + 9 + ], + "mask": 512, + "rank": 1 + }, + { + "generators": [ + 10 + ], + "mask": 1024, + "rank": 1 + }, + { + "generators": [ + 11 + ], + "mask": 2048, + "rank": 1 + }, + { + "generators": [ + 12 + ], + "mask": 4096, + "rank": 1 + }, + { + "generators": [ + 13 + ], + "mask": 8192, + "rank": 1 + }, + { + "generators": [ + 14 + ], + "mask": 16384, + "rank": 1 + }, + { + "generators": [ + 15 + ], + "mask": 32768, + "rank": 1 + }, + { + "generators": [ + 16 + ], + "mask": 65536, + "rank": 1 + }, + { + "generators": [ + 17 + ], + "mask": 131072, + "rank": 1 + }, + { + "generators": [ + 18 + ], + "mask": 262144, + "rank": 1 + }, + { + "generators": [ + 19 + ], + "mask": 524288, + "rank": 1 + }, + { + "generators": [ + 20 + ], + "mask": 1048576, + "rank": 1 + }, + { + "generators": [ + 21 + ], + "mask": 2097152, + "rank": 1 + }, + { + "generators": [ + 22 + ], + "mask": 4194304, + "rank": 1 + }, + { + "generators": [ + 23 + ], + "mask": 8388608, + "rank": 1 + }, + { + "generators": [ + 24 + ], + "mask": 16777216, + "rank": 1 + }, + { + "generators": [ + 25 + ], + "mask": 33554432, + "rank": 1 + }, + { + "generators": [ + 26 + ], + "mask": 67108864, + "rank": 1 + }, + { + "generators": [ + 27 + ], + "mask": 134217728, + "rank": 1 + }, + { + "generators": [ + 28 + ], + "mask": 268435456, + "rank": 1 + }, + { + "generators": [ + 29 + ], + "mask": 536870912, + "rank": 1 + }, + { + "generators": [ + 30 + ], + "mask": 1073741824, + "rank": 1 + }, + { + "generators": [ + 31 + ], + "mask": 2147483648, + "rank": 1 + }, + { + "generators": [ + 32 + ], + "mask": 4294967296, + "rank": 1 + }, + { + "generators": [ + 33 + ], + "mask": 8589934592, + "rank": 1 + }, + { + "generators": [ + 34 + ], + "mask": 17179869184, + "rank": 1 + }, + { + "generators": [ + 35 + ], + "mask": 34359738368, + "rank": 1 + }, + { + "generators": [ + 36 + ], + "mask": 68719476736, + "rank": 1 + }, + { + "generators": [ + 37 + ], + "mask": 137438953472, + "rank": 1 + }, + { + "generators": [ + 38 + ], + "mask": 274877906944, + "rank": 1 + }, + { + "generators": [ + 39 + ], + "mask": 549755813888, + "rank": 1 + }, + { + "generators": [ + 3, + 4 + ], + "mask": 24, + "rank": 2 + }, + { + "generators": [ + 5, + 6 + ], + "mask": 96, + "rank": 2 + }, + { + "generators": [ + 7, + 8 + ], + "mask": 384, + "rank": 2 + }, + { + "generators": [ + 9, + 10 + ], + "mask": 1536, + "rank": 2 + }, + { + "generators": [ + 0, + 1 + ], + "mask": 2055, + "rank": 2 + }, + { + "generators": [ + 3, + 11 + ], + "mask": 2056, + "rank": 2 + }, + { + "generators": [ + 4, + 11 + ], + "mask": 2064, + "rank": 2 + }, + { + "generators": [ + 5, + 11 + ], + "mask": 2080, + "rank": 2 + }, + { + "generators": [ + 6, + 11 + ], + "mask": 2112, + "rank": 2 + }, + { + "generators": [ + 7, + 11 + ], + "mask": 2176, + "rank": 2 + }, + { + "generators": [ + 8, + 11 + ], + "mask": 2304, + "rank": 2 + }, + { + "generators": [ + 9, + 11 + ], + "mask": 2560, + "rank": 2 + }, + { + "generators": [ + 10, + 11 + ], + "mask": 3072, + "rank": 2 + }, + { + "generators": [ + 2, + 12 + ], + "mask": 4100, + "rank": 2 + }, + { + "generators": [ + 5, + 12 + ], + "mask": 4128, + "rank": 2 + }, + { + "generators": [ + 7, + 12 + ], + "mask": 4224, + "rank": 2 + }, + { + "generators": [ + 9, + 12 + ], + "mask": 4608, + "rank": 2 + }, + { + "generators": [ + 2, + 13 + ], + "mask": 8196, + "rank": 2 + }, + { + "generators": [ + 6, + 13 + ], + "mask": 8256, + "rank": 2 + }, + { + "generators": [ + 8, + 13 + ], + "mask": 8448, + "rank": 2 + }, + { + "generators": [ + 10, + 13 + ], + "mask": 9216, + "rank": 2 + }, + { + "generators": [ + 12, + 13 + ], + "mask": 12288, + "rank": 2 + }, + { + "generators": [ + 2, + 14 + ], + "mask": 16388, + "rank": 2 + }, + { + "generators": [ + 4, + 14 + ], + "mask": 16400, + "rank": 2 + }, + { + "generators": [ + 7, + 14 + ], + "mask": 16512, + "rank": 2 + }, + { + "generators": [ + 10, + 14 + ], + "mask": 17408, + "rank": 2 + }, + { + "generators": [ + 2, + 15 + ], + "mask": 32772, + "rank": 2 + }, + { + "generators": [ + 3, + 15 + ], + "mask": 32776, + "rank": 2 + }, + { + "generators": [ + 8, + 15 + ], + "mask": 33024, + "rank": 2 + }, + { + "generators": [ + 9, + 15 + ], + "mask": 33280, + "rank": 2 + }, + { + "generators": [ + 14, + 15 + ], + "mask": 49152, + "rank": 2 + }, + { + "generators": [ + 2, + 16 + ], + "mask": 65540, + "rank": 2 + }, + { + "generators": [ + 4, + 16 + ], + "mask": 65552, + "rank": 2 + }, + { + "generators": [ + 6, + 16 + ], + "mask": 65600, + "rank": 2 + }, + { + "generators": [ + 9, + 16 + ], + "mask": 66048, + "rank": 2 + }, + { + "generators": [ + 2, + 17 + ], + "mask": 131076, + "rank": 2 + }, + { + "generators": [ + 3, + 17 + ], + "mask": 131080, + "rank": 2 + }, + { + "generators": [ + 5, + 17 + ], + "mask": 131104, + "rank": 2 + }, + { + "generators": [ + 10, + 17 + ], + "mask": 132096, + "rank": 2 + }, + { + "generators": [ + 16, + 17 + ], + "mask": 196608, + "rank": 2 + }, + { + "generators": [ + 2, + 18 + ], + "mask": 262148, + "rank": 2 + }, + { + "generators": [ + 4, + 18 + ], + "mask": 262160, + "rank": 2 + }, + { + "generators": [ + 5, + 18 + ], + "mask": 262176, + "rank": 2 + }, + { + "generators": [ + 8, + 18 + ], + "mask": 262400, + "rank": 2 + }, + { + "generators": [ + 2, + 19 + ], + "mask": 524292, + "rank": 2 + }, + { + "generators": [ + 3, + 19 + ], + "mask": 524296, + "rank": 2 + }, + { + "generators": [ + 6, + 19 + ], + "mask": 524352, + "rank": 2 + }, + { + "generators": [ + 7, + 19 + ], + "mask": 524416, + "rank": 2 + }, + { + "generators": [ + 18, + 19 + ], + "mask": 786432, + "rank": 2 + }, + { + "generators": [ + 1, + 20 + ], + "mask": 1048578, + "rank": 2 + }, + { + "generators": [ + 6, + 20 + ], + "mask": 1048640, + "rank": 2 + }, + { + "generators": [ + 8, + 20 + ], + "mask": 1048832, + "rank": 2 + }, + { + "generators": [ + 10, + 20 + ], + "mask": 1049600, + "rank": 2 + }, + { + "generators": [ + 0, + 4 + ], + "mask": 1052689, + "rank": 2 + }, + { + "generators": [ + 15, + 20 + ], + "mask": 1081344, + "rank": 2 + }, + { + "generators": [ + 17, + 20 + ], + "mask": 1179648, + "rank": 2 + }, + { + "generators": [ + 19, + 20 + ], + "mask": 1572864, + "rank": 2 + }, + { + "generators": [ + 1, + 21 + ], + "mask": 2097154, + "rank": 2 + }, + { + "generators": [ + 5, + 21 + ], + "mask": 2097184, + "rank": 2 + }, + { + "generators": [ + 7, + 21 + ], + "mask": 2097280, + "rank": 2 + }, + { + "generators": [ + 9, + 21 + ], + "mask": 2097664, + "rank": 2 + }, + { + "generators": [ + 0, + 3 + ], + "mask": 2105353, + "rank": 2 + }, + { + "generators": [ + 14, + 21 + ], + "mask": 2113536, + "rank": 2 + }, + { + "generators": [ + 16, + 21 + ], + "mask": 2162688, + "rank": 2 + }, + { + "generators": [ + 18, + 21 + ], + "mask": 2359296, + "rank": 2 + }, + { + "generators": [ + 20, + 21 + ], + "mask": 3145728, + "rank": 2 + }, + { + "generators": [ + 1, + 22 + ], + "mask": 4194306, + "rank": 2 + }, + { + "generators": [ + 3, + 22 + ], + "mask": 4194312, + "rank": 2 + }, + { + "generators": [ + 8, + 22 + ], + "mask": 4194560, + "rank": 2 + }, + { + "generators": [ + 9, + 22 + ], + "mask": 4194816, + "rank": 2 + }, + { + "generators": [ + 12, + 22 + ], + "mask": 4198400, + "rank": 2 + }, + { + "generators": [ + 0, + 6 + ], + "mask": 4210753, + "rank": 2 + }, + { + "generators": [ + 17, + 22 + ], + "mask": 4325376, + "rank": 2 + }, + { + "generators": [ + 18, + 22 + ], + "mask": 4456448, + "rank": 2 + }, + { + "generators": [ + 1, + 23 + ], + "mask": 8388610, + "rank": 2 + }, + { + "generators": [ + 4, + 23 + ], + "mask": 8388624, + "rank": 2 + }, + { + "generators": [ + 7, + 23 + ], + "mask": 8388736, + "rank": 2 + }, + { + "generators": [ + 10, + 23 + ], + "mask": 8389632, + "rank": 2 + }, + { + "generators": [ + 13, + 23 + ], + "mask": 8396800, + "rank": 2 + }, + { + "generators": [ + 0, + 5 + ], + "mask": 8421409, + "rank": 2 + }, + { + "generators": [ + 16, + 23 + ], + "mask": 8454144, + "rank": 2 + }, + { + "generators": [ + 19, + 23 + ], + "mask": 8912896, + "rank": 2 + }, + { + "generators": [ + 22, + 23 + ], + "mask": 12582912, + "rank": 2 + }, + { + "generators": [ + 1, + 24 + ], + "mask": 16777218, + "rank": 2 + }, + { + "generators": [ + 3, + 24 + ], + "mask": 16777224, + "rank": 2 + }, + { + "generators": [ + 5, + 24 + ], + "mask": 16777248, + "rank": 2 + }, + { + "generators": [ + 10, + 24 + ], + "mask": 16778240, + "rank": 2 + }, + { + "generators": [ + 12, + 24 + ], + "mask": 16781312, + "rank": 2 + }, + { + "generators": [ + 14, + 24 + ], + "mask": 16793600, + "rank": 2 + }, + { + "generators": [ + 0, + 8 + ], + "mask": 16843009, + "rank": 2 + }, + { + "generators": [ + 19, + 24 + ], + "mask": 17301504, + "rank": 2 + }, + { + "generators": [ + 1, + 25 + ], + "mask": 33554434, + "rank": 2 + }, + { + "generators": [ + 4, + 25 + ], + "mask": 33554448, + "rank": 2 + }, + { + "generators": [ + 6, + 25 + ], + "mask": 33554496, + "rank": 2 + }, + { + "generators": [ + 9, + 25 + ], + "mask": 33554944, + "rank": 2 + }, + { + "generators": [ + 13, + 25 + ], + "mask": 33562624, + "rank": 2 + }, + { + "generators": [ + 15, + 25 + ], + "mask": 33587200, + "rank": 2 + }, + { + "generators": [ + 0, + 7 + ], + "mask": 33685633, + "rank": 2 + }, + { + "generators": [ + 18, + 25 + ], + "mask": 33816576, + "rank": 2 + }, + { + "generators": [ + 24, + 25 + ], + "mask": 50331648, + "rank": 2 + }, + { + "generators": [ + 1, + 26 + ], + "mask": 67108866, + "rank": 2 + }, + { + "generators": [ + 3, + 26 + ], + "mask": 67108872, + "rank": 2 + }, + { + "generators": [ + 6, + 26 + ], + "mask": 67108928, + "rank": 2 + }, + { + "generators": [ + 7, + 26 + ], + "mask": 67108992, + "rank": 2 + }, + { + "generators": [ + 12, + 26 + ], + "mask": 67112960, + "rank": 2 + }, + { + "generators": [ + 15, + 26 + ], + "mask": 67141632, + "rank": 2 + }, + { + "generators": [ + 16, + 26 + ], + "mask": 67174400, + "rank": 2 + }, + { + "generators": [ + 0, + 10 + ], + "mask": 67372033, + "rank": 2 + }, + { + "generators": [ + 1, + 27 + ], + "mask": 134217730, + "rank": 2 + }, + { + "generators": [ + 4, + 27 + ], + "mask": 134217744, + "rank": 2 + }, + { + "generators": [ + 5, + 27 + ], + "mask": 134217760, + "rank": 2 + }, + { + "generators": [ + 8, + 27 + ], + "mask": 134217984, + "rank": 2 + }, + { + "generators": [ + 13, + 27 + ], + "mask": 134225920, + "rank": 2 + }, + { + "generators": [ + 14, + 27 + ], + "mask": 134234112, + "rank": 2 + }, + { + "generators": [ + 17, + 27 + ], + "mask": 134348800, + "rank": 2 + }, + { + "generators": [ + 0, + 9 + ], + "mask": 134742529, + "rank": 2 + }, + { + "generators": [ + 26, + 27 + ], + "mask": 201326592, + "rank": 2 + }, + { + "generators": [ + 0, + 28 + ], + "mask": 268435457, + "rank": 2 + }, + { + "generators": [ + 6, + 28 + ], + "mask": 268435520, + "rank": 2 + }, + { + "generators": [ + 8, + 28 + ], + "mask": 268435712, + "rank": 2 + }, + { + "generators": [ + 10, + 28 + ], + "mask": 268436480, + "rank": 2 + }, + { + "generators": [ + 1, + 3 + ], + "mask": 268439562, + "rank": 2 + }, + { + "generators": [ + 14, + 28 + ], + "mask": 268451840, + "rank": 2 + }, + { + "generators": [ + 16, + 28 + ], + "mask": 268500992, + "rank": 2 + }, + { + "generators": [ + 18, + 28 + ], + "mask": 268697600, + "rank": 2 + }, + { + "generators": [ + 11, + 13 + ], + "mask": 269494272, + "rank": 2 + }, + { + "generators": [ + 2, + 4 + ], + "mask": 270532628, + "rank": 2 + }, + { + "generators": [ + 22, + 28 + ], + "mask": 272629760, + "rank": 2 + }, + { + "generators": [ + 9, + 17 + ], + "mask": 276955648, + "rank": 2 + }, + { + "generators": [ + 24, + 28 + ], + "mask": 285212672, + "rank": 2 + }, + { + "generators": [ + 5, + 19 + ], + "mask": 302514208, + "rank": 2 + }, + { + "generators": [ + 26, + 28 + ], + "mask": 335544320, + "rank": 2 + }, + { + "generators": [ + 7, + 15 + ], + "mask": 402686080, + "rank": 2 + }, + { + "generators": [ + 0, + 29 + ], + "mask": 536870913, + "rank": 2 + }, + { + "generators": [ + 5, + 29 + ], + "mask": 536870944, + "rank": 2 + }, + { + "generators": [ + 7, + 29 + ], + "mask": 536871040, + "rank": 2 + }, + { + "generators": [ + 9, + 29 + ], + "mask": 536871424, + "rank": 2 + }, + { + "generators": [ + 1, + 4 + ], + "mask": 536879122, + "rank": 2 + }, + { + "generators": [ + 15, + 29 + ], + "mask": 536903680, + "rank": 2 + }, + { + "generators": [ + 17, + 29 + ], + "mask": 537001984, + "rank": 2 + }, + { + "generators": [ + 19, + 29 + ], + "mask": 537395200, + "rank": 2 + }, + { + "generators": [ + 2, + 3 + ], + "mask": 537919500, + "rank": 2 + }, + { + "generators": [ + 11, + 12 + ], + "mask": 538974208, + "rank": 2 + }, + { + "generators": [ + 10, + 16 + ], + "mask": 541131776, + "rank": 2 + }, + { + "generators": [ + 23, + 29 + ], + "mask": 545259520, + "rank": 2 + }, + { + "generators": [ + 6, + 18 + ], + "mask": 553910336, + "rank": 2 + }, + { + "generators": [ + 25, + 29 + ], + "mask": 570425344, + "rank": 2 + }, + { + "generators": [ + 8, + 14 + ], + "mask": 603996416, + "rank": 2 + }, + { + "generators": [ + 27, + 29 + ], + "mask": 671088640, + "rank": 2 + }, + { + "generators": [ + 28, + 29 + ], + "mask": 805306368, + "rank": 2 + }, + { + "generators": [ + 0, + 30 + ], + "mask": 1073741825, + "rank": 2 + }, + { + "generators": [ + 3, + 30 + ], + "mask": 1073741832, + "rank": 2 + }, + { + "generators": [ + 8, + 30 + ], + "mask": 1073742080, + "rank": 2 + }, + { + "generators": [ + 9, + 30 + ], + "mask": 1073742336, + "rank": 2 + }, + { + "generators": [ + 13, + 30 + ], + "mask": 1073750016, + "rank": 2 + }, + { + "generators": [ + 1, + 5 + ], + "mask": 1073758242, + "rank": 2 + }, + { + "generators": [ + 16, + 30 + ], + "mask": 1073807360, + "rank": 2 + }, + { + "generators": [ + 19, + 30 + ], + "mask": 1074266112, + "rank": 2 + }, + { + "generators": [ + 7, + 18 + ], + "mask": 1075052672, + "rank": 2 + }, + { + "generators": [ + 21, + 30 + ], + "mask": 1075838976, + "rank": 2 + }, + { + "generators": [ + 11, + 15 + ], + "mask": 1077970944, + "rank": 2 + }, + { + "generators": [ + 2, + 6 + ], + "mask": 1082130500, + "rank": 2 + }, + { + "generators": [ + 24, + 30 + ], + "mask": 1090519040, + "rank": 2 + }, + { + "generators": [ + 10, + 12 + ], + "mask": 1107301376, + "rank": 2 + }, + { + "generators": [ + 4, + 17 + ], + "mask": 1140981776, + "rank": 2 + }, + { + "generators": [ + 27, + 30 + ], + "mask": 1207959552, + "rank": 2 + }, + { + "generators": [ + 0, + 31 + ], + "mask": 2147483649, + "rank": 2 + }, + { + "generators": [ + 4, + 31 + ], + "mask": 2147483664, + "rank": 2 + }, + { + "generators": [ + 7, + 31 + ], + "mask": 2147483776, + "rank": 2 + }, + { + "generators": [ + 10, + 31 + ], + "mask": 2147484672, + "rank": 2 + }, + { + "generators": [ + 12, + 31 + ], + "mask": 2147487744, + "rank": 2 + }, + { + "generators": [ + 1, + 6 + ], + "mask": 2147516482, + "rank": 2 + }, + { + "generators": [ + 17, + 31 + ], + "mask": 2147614720, + "rank": 2 + }, + { + "generators": [ + 18, + 31 + ], + "mask": 2147745792, + "rank": 2 + }, + { + "generators": [ + 20, + 31 + ], + "mask": 2148532224, + "rank": 2 + }, + { + "generators": [ + 8, + 19 + ], + "mask": 2150105344, + "rank": 2 + }, + { + "generators": [ + 2, + 5 + ], + "mask": 2151677988, + "rank": 2 + }, + { + "generators": [ + 11, + 14 + ], + "mask": 2155890688, + "rank": 2 + }, + { + "generators": [ + 9, + 13 + ], + "mask": 2164269568, + "rank": 2 + }, + { + "generators": [ + 25, + 31 + ], + "mask": 2181038080, + "rank": 2 + }, + { + "generators": [ + 26, + 31 + ], + "mask": 2214592512, + "rank": 2 + }, + { + "generators": [ + 3, + 16 + ], + "mask": 2281766920, + "rank": 2 + }, + { + "generators": [ + 30, + 31 + ], + "mask": 3221225472, + "rank": 2 + }, + { + "generators": [ + 0, + 32 + ], + "mask": 4294967297, + "rank": 2 + }, + { + "generators": [ + 3, + 32 + ], + "mask": 4294967304, + "rank": 2 + }, + { + "generators": [ + 5, + 32 + ], + "mask": 4294967328, + "rank": 2 + }, + { + "generators": [ + 10, + 32 + ], + "mask": 4294968320, + "rank": 2 + }, + { + "generators": [ + 13, + 32 + ], + "mask": 4294975488, + "rank": 2 + }, + { + "generators": [ + 15, + 32 + ], + "mask": 4295000064, + "rank": 2 + }, + { + "generators": [ + 1, + 7 + ], + "mask": 4295032962, + "rank": 2 + }, + { + "generators": [ + 18, + 32 + ], + "mask": 4295229440, + "rank": 2 + }, + { + "generators": [ + 9, + 14 + ], + "mask": 4296032768, + "rank": 2 + }, + { + "generators": [ + 21, + 32 + ], + "mask": 4297064448, + "rank": 2 + }, + { + "generators": [ + 4, + 19 + ], + "mask": 4299685904, + "rank": 2 + }, + { + "generators": [ + 23, + 32 + ], + "mask": 4303355904, + "rank": 2 + }, + { + "generators": [ + 11, + 17 + ], + "mask": 4311877632, + "rank": 2 + }, + { + "generators": [ + 2, + 8 + ], + "mask": 4328521988, + "rank": 2 + }, + { + "generators": [ + 26, + 32 + ], + "mask": 4362076160, + "rank": 2 + }, + { + "generators": [ + 6, + 12 + ], + "mask": 4429189184, + "rank": 2 + }, + { + "generators": [ + 0, + 33 + ], + "mask": 8589934593, + "rank": 2 + }, + { + "generators": [ + 4, + 33 + ], + "mask": 8589934608, + "rank": 2 + }, + { + "generators": [ + 6, + 33 + ], + "mask": 8589934656, + "rank": 2 + }, + { + "generators": [ + 9, + 33 + ], + "mask": 8589935104, + "rank": 2 + }, + { + "generators": [ + 12, + 33 + ], + "mask": 8589938688, + "rank": 2 + }, + { + "generators": [ + 14, + 33 + ], + "mask": 8589950976, + "rank": 2 + }, + { + "generators": [ + 1, + 8 + ], + "mask": 8590065922, + "rank": 2 + }, + { + "generators": [ + 19, + 33 + ], + "mask": 8590458880, + "rank": 2 + }, + { + "generators": [ + 20, + 33 + ], + "mask": 8590983168, + "rank": 2 + }, + { + "generators": [ + 10, + 15 + ], + "mask": 8592065536, + "rank": 2 + }, + { + "generators": [ + 22, + 33 + ], + "mask": 8594128896, + "rank": 2 + }, + { + "generators": [ + 3, + 18 + ], + "mask": 8598585352, + "rank": 2 + }, + { + "generators": [ + 2, + 7 + ], + "mask": 8606711940, + "rank": 2 + }, + { + "generators": [ + 11, + 16 + ], + "mask": 8623556608, + "rank": 2 + }, + { + "generators": [ + 5, + 13 + ], + "mask": 8657051680, + "rank": 2 + }, + { + "generators": [ + 27, + 33 + ], + "mask": 8724152320, + "rank": 2 + }, + { + "generators": [ + 32, + 33 + ], + "mask": 12884901888, + "rank": 2 + }, + { + "generators": [ + 0, + 34 + ], + "mask": 17179869185, + "rank": 2 + }, + { + "generators": [ + 3, + 34 + ], + "mask": 17179869192, + "rank": 2 + }, + { + "generators": [ + 6, + 34 + ], + "mask": 17179869248, + "rank": 2 + }, + { + "generators": [ + 7, + 34 + ], + "mask": 17179869312, + "rank": 2 + }, + { + "generators": [ + 13, + 34 + ], + "mask": 17179877376, + "rank": 2 + }, + { + "generators": [ + 14, + 34 + ], + "mask": 17179885568, + "rank": 2 + }, + { + "generators": [ + 17, + 34 + ], + "mask": 17180000256, + "rank": 2 + }, + { + "generators": [ + 1, + 9 + ], + "mask": 17180131842, + "rank": 2 + }, + { + "generators": [ + 5, + 16 + ], + "mask": 17180983328, + "rank": 2 + }, + { + "generators": [ + 21, + 34 + ], + "mask": 17181966336, + "rank": 2 + }, + { + "generators": [ + 22, + 34 + ], + "mask": 17184063488, + "rank": 2 + }, + { + "generators": [ + 8, + 12 + ], + "mask": 17188262144, + "rank": 2 + }, + { + "generators": [ + 4, + 15 + ], + "mask": 17196679184, + "rank": 2 + }, + { + "generators": [ + 25, + 34 + ], + "mask": 17213423616, + "rank": 2 + }, + { + "generators": [ + 11, + 19 + ], + "mask": 17247504384, + "rank": 2 + }, + { + "generators": [ + 2, + 10 + ], + "mask": 17314087940, + "rank": 2 + }, + { + "generators": [ + 0, + 35 + ], + "mask": 34359738369, + "rank": 2 + }, + { + "generators": [ + 4, + 35 + ], + "mask": 34359738384, + "rank": 2 + }, + { + "generators": [ + 5, + 35 + ], + "mask": 34359738400, + "rank": 2 + }, + { + "generators": [ + 8, + 35 + ], + "mask": 34359738624, + "rank": 2 + }, + { + "generators": [ + 12, + 35 + ], + "mask": 34359742464, + "rank": 2 + }, + { + "generators": [ + 15, + 35 + ], + "mask": 34359771136, + "rank": 2 + }, + { + "generators": [ + 16, + 35 + ], + "mask": 34359803904, + "rank": 2 + }, + { + "generators": [ + 1, + 10 + ], + "mask": 34360263682, + "rank": 2 + }, + { + "generators": [ + 20, + 35 + ], + "mask": 34360786944, + "rank": 2 + }, + { + "generators": [ + 6, + 17 + ], + "mask": 34361966656, + "rank": 2 + }, + { + "generators": [ + 7, + 13 + ], + "mask": 34363940992, + "rank": 2 + }, + { + "generators": [ + 23, + 35 + ], + "mask": 34368126976, + "rank": 2 + }, + { + "generators": [ + 24, + 35 + ], + "mask": 34376515584, + "rank": 2 + }, + { + "generators": [ + 3, + 14 + ], + "mask": 34393309192, + "rank": 2 + }, + { + "generators": [ + 2, + 9 + ], + "mask": 34426847748, + "rank": 2 + }, + { + "generators": [ + 11, + 18 + ], + "mask": 34494220288, + "rank": 2 + }, + { + "generators": [ + 34, + 35 + ], + "mask": 51539607552, + "rank": 2 + }, + { + "generators": [ + 0, + 36 + ], + "mask": 68719476737, + "rank": 2 + }, + { + "generators": [ + 1, + 36 + ], + "mask": 68719476738, + "rank": 2 + }, + { + "generators": [ + 2, + 36 + ], + "mask": 68719476740, + "rank": 2 + }, + { + "generators": [ + 3, + 6 + ], + "mask": 68719476936, + "rank": 2 + }, + { + "generators": [ + 4, + 5 + ], + "mask": 68719477040, + "rank": 2 + }, + { + "generators": [ + 9, + 36 + ], + "mask": 68719477248, + "rank": 2 + }, + { + "generators": [ + 10, + 36 + ], + "mask": 68719477760, + "rank": 2 + }, + { + "generators": [ + 11, + 36 + ], + "mask": 68719478784, + "rank": 2 + }, + { + "generators": [ + 12, + 15 + ], + "mask": 68719579136, + "rank": 2 + }, + { + "generators": [ + 13, + 14 + ], + "mask": 68719632384, + "rank": 2 + }, + { + "generators": [ + 18, + 36 + ], + "mask": 68719738880, + "rank": 2 + }, + { + "generators": [ + 19, + 36 + ], + "mask": 68720001024, + "rank": 2 + }, + { + "generators": [ + 20, + 23 + ], + "mask": 68745691136, + "rank": 2 + }, + { + "generators": [ + 21, + 22 + ], + "mask": 68759322624, + "rank": 2 + }, + { + "generators": [ + 26, + 36 + ], + "mask": 68786585600, + "rank": 2 + }, + { + "generators": [ + 27, + 36 + ], + "mask": 68853694464, + "rank": 2 + }, + { + "generators": [ + 28, + 31 + ], + "mask": 75430363136, + "rank": 2 + }, + { + "generators": [ + 29, + 30 + ], + "mask": 78920024064, + "rank": 2 + }, + { + "generators": [ + 34, + 36 + ], + "mask": 85899345920, + "rank": 2 + }, + { + "generators": [ + 35, + 36 + ], + "mask": 103079215104, + "rank": 2 + }, + { + "generators": [ + 0, + 37 + ], + "mask": 137438953473, + "rank": 2 + }, + { + "generators": [ + 1, + 37 + ], + "mask": 137438953474, + "rank": 2 + }, + { + "generators": [ + 2, + 37 + ], + "mask": 137438953476, + "rank": 2 + }, + { + "generators": [ + 7, + 37 + ], + "mask": 137438953600, + "rank": 2 + }, + { + "generators": [ + 8, + 37 + ], + "mask": 137438953728, + "rank": 2 + }, + { + "generators": [ + 4, + 6 + ], + "mask": 137438954064, + "rank": 2 + }, + { + "generators": [ + 3, + 5 + ], + "mask": 137438954536, + "rank": 2 + }, + { + "generators": [ + 11, + 37 + ], + "mask": 137438955520, + "rank": 2 + }, + { + "generators": [ + 16, + 37 + ], + "mask": 137439019008, + "rank": 2 + }, + { + "generators": [ + 17, + 37 + ], + "mask": 137439084544, + "rank": 2 + }, + { + "generators": [ + 13, + 15 + ], + "mask": 137439256576, + "rank": 2 + }, + { + "generators": [ + 12, + 14 + ], + "mask": 137439498240, + "rank": 2 + }, + { + "generators": [ + 24, + 37 + ], + "mask": 137455730688, + "rank": 2 + }, + { + "generators": [ + 25, + 37 + ], + "mask": 137472507904, + "rank": 2 + }, + { + "generators": [ + 21, + 23 + ], + "mask": 137516548096, + "rank": 2 + }, + { + "generators": [ + 20, + 22 + ], + "mask": 137578414080, + "rank": 2 + }, + { + "generators": [ + 32, + 37 + ], + "mask": 141733920768, + "rank": 2 + }, + { + "generators": [ + 33, + 37 + ], + "mask": 146028888064, + "rank": 2 + }, + { + "generators": [ + 29, + 31 + ], + "mask": 157303177216, + "rank": 2 + }, + { + "generators": [ + 28, + 30 + ], + "mask": 173140869120, + "rank": 2 + }, + { + "generators": [ + 0, + 38 + ], + "mask": 274877906945, + "rank": 2 + }, + { + "generators": [ + 1, + 38 + ], + "mask": 274877906946, + "rank": 2 + }, + { + "generators": [ + 2, + 38 + ], + "mask": 274877906948, + "rank": 2 + }, + { + "generators": [ + 5, + 38 + ], + "mask": 274877906976, + "rank": 2 + }, + { + "generators": [ + 6, + 38 + ], + "mask": 274877907008, + "rank": 2 + }, + { + "generators": [ + 3, + 8 + ], + "mask": 274877907720, + "rank": 2 + }, + { + "generators": [ + 4, + 7 + ], + "mask": 274877908112, + "rank": 2 + }, + { + "generators": [ + 11, + 38 + ], + "mask": 274877908992, + "rank": 2 + }, + { + "generators": [ + 14, + 38 + ], + "mask": 274877923328, + "rank": 2 + }, + { + "generators": [ + 15, + 38 + ], + "mask": 274877939712, + "rank": 2 + }, + { + "generators": [ + 12, + 17 + ], + "mask": 274878304256, + "rank": 2 + }, + { + "generators": [ + 13, + 16 + ], + "mask": 274878504960, + "rank": 2 + }, + { + "generators": [ + 22, + 38 + ], + "mask": 274882101248, + "rank": 2 + }, + { + "generators": [ + 23, + 38 + ], + "mask": 274886295552, + "rank": 2 + }, + { + "generators": [ + 20, + 25 + ], + "mask": 274979618816, + "rank": 2 + }, + { + "generators": [ + 21, + 24 + ], + "mask": 275030999040, + "rank": 2 + }, + { + "generators": [ + 30, + 38 + ], + "mask": 275951648768, + "rank": 2 + }, + { + "generators": [ + 31, + 38 + ], + "mask": 277025390592, + "rank": 2 + }, + { + "generators": [ + 28, + 33 + ], + "mask": 300916146176, + "rank": 2 + }, + { + "generators": [ + 29, + 32 + ], + "mask": 314069483520, + "rank": 2 + }, + { + "generators": [ + 0, + 39 + ], + "mask": 549755813889, + "rank": 2 + }, + { + "generators": [ + 1, + 39 + ], + "mask": 549755813890, + "rank": 2 + }, + { + "generators": [ + 2, + 39 + ], + "mask": 549755813892, + "rank": 2 + }, + { + "generators": [ + 3, + 39 + ], + "mask": 549755813896, + "rank": 2 + }, + { + "generators": [ + 4, + 39 + ], + "mask": 549755813904, + "rank": 2 + }, + { + "generators": [ + 5, + 7 + ], + "mask": 549755814560, + "rank": 2 + }, + { + "generators": [ + 6, + 8 + ], + "mask": 549755815232, + "rank": 2 + }, + { + "generators": [ + 11, + 39 + ], + "mask": 549755815936, + "rank": 2 + }, + { + "generators": [ + 12, + 39 + ], + "mask": 549755817984, + "rank": 2 + }, + { + "generators": [ + 13, + 39 + ], + "mask": 549755822080, + "rank": 2 + }, + { + "generators": [ + 14, + 16 + ], + "mask": 549756157952, + "rank": 2 + }, + { + "generators": [ + 15, + 17 + ], + "mask": 549756502016, + "rank": 2 + }, + { + "generators": [ + 20, + 39 + ], + "mask": 549756862464, + "rank": 2 + }, + { + "generators": [ + 21, + 39 + ], + "mask": 549757911040, + "rank": 2 + }, + { + "generators": [ + 22, + 24 + ], + "mask": 549843894272, + "rank": 2 + }, + { + "generators": [ + 23, + 25 + ], + "mask": 549931974656, + "rank": 2 + }, + { + "generators": [ + 28, + 39 + ], + "mask": 550024249344, + "rank": 2 + }, + { + "generators": [ + 29, + 39 + ], + "mask": 550292684800, + "rank": 2 + }, + { + "generators": [ + 30, + 32 + ], + "mask": 572304392192, + "rank": 2 + }, + { + "generators": [ + 31, + 33 + ], + "mask": 594852970496, + "rank": 2 + }, + { + "generators": [ + 36, + 37 + ], + "mask": 1030792151040, + "rank": 2 + }, + { + "generators": [ + 6, + 11, + 13 + ], + "mask": 269494336, + "rank": 3 + }, + { + "generators": [ + 8, + 11, + 13 + ], + "mask": 269494528, + "rank": 3 + }, + { + "generators": [ + 10, + 11, + 13 + ], + "mask": 269495296, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 14 + ], + "mask": 270549012, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 16 + ], + "mask": 270598164, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 18 + ], + "mask": 270794772, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 22 + ], + "mask": 272633866, + "rank": 3 + }, + { + "generators": [ + 0, + 6, + 28 + ], + "mask": 272646209, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 17 + ], + "mask": 276956672, + "rank": 3 + }, + { + "generators": [ + 9, + 16, + 17 + ], + "mask": 277021184, + "rank": 3 + }, + { + "generators": [ + 9, + 17, + 22 + ], + "mask": 281149952, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 24 + ], + "mask": 285216778, + "rank": 3 + }, + { + "generators": [ + 0, + 8, + 28 + ], + "mask": 285278465, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 19 + ], + "mask": 302514272, + "rank": 3 + }, + { + "generators": [ + 5, + 18, + 19 + ], + "mask": 302776352, + "rank": 3 + }, + { + "generators": [ + 5, + 19, + 24 + ], + "mask": 319291424, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 26 + ], + "mask": 335548426, + "rank": 3 + }, + { + "generators": [ + 0, + 10, + 28 + ], + "mask": 335807489, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 15 + ], + "mask": 402686336, + "rank": 3 + }, + { + "generators": [ + 7, + 14, + 15 + ], + "mask": 402702464, + "rank": 3 + }, + { + "generators": [ + 7, + 15, + 26 + ], + "mask": 469794944, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 15 + ], + "mask": 537952268, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 17 + ], + "mask": 538050572, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 19 + ], + "mask": 538443788, + "rank": 3 + }, + { + "generators": [ + 5, + 11, + 12 + ], + "mask": 538974240, + "rank": 3 + }, + { + "generators": [ + 7, + 11, + 12 + ], + "mask": 538974336, + "rank": 3 + }, + { + "generators": [ + 9, + 11, + 12 + ], + "mask": 538974720, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 16 + ], + "mask": 541132288, + "rank": 3 + }, + { + "generators": [ + 10, + 16, + 17 + ], + "mask": 541262848, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 23 + ], + "mask": 545267730, + "rank": 3 + }, + { + "generators": [ + 0, + 5, + 29 + ], + "mask": 545292321, + "rank": 3 + }, + { + "generators": [ + 10, + 16, + 23 + ], + "mask": 549520384, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 18 + ], + "mask": 553910368, + "rank": 3 + }, + { + "generators": [ + 6, + 18, + 19 + ], + "mask": 554434624, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 25 + ], + "mask": 570433554, + "rank": 3 + }, + { + "generators": [ + 0, + 7, + 29 + ], + "mask": 570556545, + "rank": 3 + }, + { + "generators": [ + 6, + 18, + 25 + ], + "mask": 587464768, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 14 + ], + "mask": 603996544, + "rank": 3 + }, + { + "generators": [ + 8, + 14, + 15 + ], + "mask": 604029184, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 27 + ], + "mask": 671096850, + "rank": 3 + }, + { + "generators": [ + 0, + 9, + 29 + ], + "mask": 671613441, + "rank": 3 + }, + { + "generators": [ + 8, + 14, + 27 + ], + "mask": 738214144, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 3 + ], + "mask": 808466463, + "rank": 3 + }, + { + "generators": [ + 10, + 16, + 28 + ], + "mask": 809567232, + "rank": 3 + }, + { + "generators": [ + 9, + 17, + 29 + ], + "mask": 813826560, + "rank": 3 + }, + { + "generators": [ + 6, + 18, + 28 + ], + "mask": 822345792, + "rank": 3 + }, + { + "generators": [ + 5, + 19, + 29 + ], + "mask": 839385120, + "rank": 3 + }, + { + "generators": [ + 8, + 14, + 28 + ], + "mask": 872431872, + "rank": 3 + }, + { + "generators": [ + 7, + 15, + 29 + ], + "mask": 939556992, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 18 + ], + "mask": 1075052928, + "rank": 3 + }, + { + "generators": [ + 7, + 18, + 19 + ], + "mask": 1075576960, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 30 + ], + "mask": 1075847177, + "rank": 3 + }, + { + "generators": [ + 1, + 5, + 21 + ], + "mask": 1075855394, + "rank": 3 + }, + { + "generators": [ + 7, + 18, + 21 + ], + "mask": 1077149824, + "rank": 3 + }, + { + "generators": [ + 3, + 11, + 15 + ], + "mask": 1077970952, + "rank": 3 + }, + { + "generators": [ + 8, + 11, + 15 + ], + "mask": 1077971200, + "rank": 3 + }, + { + "generators": [ + 9, + 11, + 15 + ], + "mask": 1077971456, + "rank": 3 + }, + { + "generators": [ + 2, + 6, + 13 + ], + "mask": 1082138692, + "rank": 3 + }, + { + "generators": [ + 2, + 6, + 16 + ], + "mask": 1082196036, + "rank": 3 + }, + { + "generators": [ + 2, + 6, + 19 + ], + "mask": 1082654788, + "rank": 3 + }, + { + "generators": [ + 1, + 5, + 24 + ], + "mask": 1090535458, + "rank": 3 + }, + { + "generators": [ + 0, + 8, + 30 + ], + "mask": 1090584833, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 12 + ], + "mask": 1107301888, + "rank": 3 + }, + { + "generators": [ + 10, + 12, + 13 + ], + "mask": 1107309568, + "rank": 3 + }, + { + "generators": [ + 10, + 12, + 24 + ], + "mask": 1124078592, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 17 + ], + "mask": 1140981784, + "rank": 3 + }, + { + "generators": [ + 4, + 16, + 17 + ], + "mask": 1141047312, + "rank": 3 + }, + { + "generators": [ + 1, + 5, + 27 + ], + "mask": 1207975970, + "rank": 3 + }, + { + "generators": [ + 0, + 9, + 30 + ], + "mask": 1208484353, + "rank": 3 + }, + { + "generators": [ + 4, + 17, + 27 + ], + "mask": 1275199504, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 31 + ], + "mask": 2148536337, + "rank": 3 + }, + { + "generators": [ + 1, + 6, + 20 + ], + "mask": 2148565058, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 19 + ], + "mask": 2150105472, + "rank": 3 + }, + { + "generators": [ + 8, + 18, + 19 + ], + "mask": 2150367488, + "rank": 3 + }, + { + "generators": [ + 8, + 19, + 20 + ], + "mask": 2151153920, + "rank": 3 + }, + { + "generators": [ + 2, + 5, + 12 + ], + "mask": 2151682084, + "rank": 3 + }, + { + "generators": [ + 2, + 5, + 17 + ], + "mask": 2151809060, + "rank": 3 + }, + { + "generators": [ + 2, + 5, + 18 + ], + "mask": 2151940132, + "rank": 3 + }, + { + "generators": [ + 4, + 11, + 14 + ], + "mask": 2155890704, + "rank": 3 + }, + { + "generators": [ + 7, + 11, + 14 + ], + "mask": 2155890816, + "rank": 3 + }, + { + "generators": [ + 10, + 11, + 14 + ], + "mask": 2155891712, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 13 + ], + "mask": 2164270592, + "rank": 3 + }, + { + "generators": [ + 9, + 12, + 13 + ], + "mask": 2164273664, + "rank": 3 + }, + { + "generators": [ + 1, + 6, + 25 + ], + "mask": 2181070914, + "rank": 3 + }, + { + "generators": [ + 0, + 7, + 31 + ], + "mask": 2181169281, + "rank": 3 + }, + { + "generators": [ + 9, + 13, + 25 + ], + "mask": 2197824000, + "rank": 3 + }, + { + "generators": [ + 1, + 6, + 26 + ], + "mask": 2214625346, + "rank": 3 + }, + { + "generators": [ + 0, + 10, + 31 + ], + "mask": 2214855681, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 16 + ], + "mask": 2281766936, + "rank": 3 + }, + { + "generators": [ + 3, + 16, + 17 + ], + "mask": 2281897992, + "rank": 3 + }, + { + "generators": [ + 3, + 16, + 26 + ], + "mask": 2348875784, + "rank": 3 + }, + { + "generators": [ + 7, + 18, + 31 + ], + "mask": 3222536320, + "rank": 3 + }, + { + "generators": [ + 8, + 19, + 30 + ], + "mask": 3223847168, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 5 + ], + "mask": 3233859687, + "rank": 3 + }, + { + "generators": [ + 9, + 13, + 30 + ], + "mask": 3238011392, + "rank": 3 + }, + { + "generators": [ + 10, + 12, + 31 + ], + "mask": 3254785024, + "rank": 3 + }, + { + "generators": [ + 4, + 17, + 31 + ], + "mask": 3288465424, + "rank": 3 + }, + { + "generators": [ + 3, + 16, + 30 + ], + "mask": 3355508744, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 14 + ], + "mask": 4296033792, + "rank": 3 + }, + { + "generators": [ + 9, + 14, + 15 + ], + "mask": 4296065536, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 32 + ], + "mask": 4297072649, + "rank": 3 + }, + { + "generators": [ + 1, + 7, + 21 + ], + "mask": 4297130114, + "rank": 3 + }, + { + "generators": [ + 9, + 14, + 21 + ], + "mask": 4298129920, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 19 + ], + "mask": 4299685912, + "rank": 3 + }, + { + "generators": [ + 4, + 18, + 19 + ], + "mask": 4299948048, + "rank": 3 + }, + { + "generators": [ + 0, + 5, + 32 + ], + "mask": 4303388705, + "rank": 3 + }, + { + "generators": [ + 1, + 7, + 23 + ], + "mask": 4303421570, + "rank": 3 + }, + { + "generators": [ + 4, + 19, + 23 + ], + "mask": 4308074512, + "rank": 3 + }, + { + "generators": [ + 3, + 11, + 17 + ], + "mask": 4311877640, + "rank": 3 + }, + { + "generators": [ + 5, + 11, + 17 + ], + "mask": 4311877664, + "rank": 3 + }, + { + "generators": [ + 10, + 11, + 17 + ], + "mask": 4311878656, + "rank": 3 + }, + { + "generators": [ + 2, + 8, + 13 + ], + "mask": 4328530180, + "rank": 3 + }, + { + "generators": [ + 2, + 8, + 15 + ], + "mask": 4328554756, + "rank": 3 + }, + { + "generators": [ + 2, + 8, + 18 + ], + "mask": 4328784132, + "rank": 3 + }, + { + "generators": [ + 1, + 7, + 26 + ], + "mask": 4362141826, + "rank": 3 + }, + { + "generators": [ + 0, + 10, + 32 + ], + "mask": 4362339329, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 12 + ], + "mask": 4429189216, + "rank": 3 + }, + { + "generators": [ + 6, + 12, + 13 + ], + "mask": 4429197376, + "rank": 3 + }, + { + "generators": [ + 6, + 12, + 26 + ], + "mask": 4496298048, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 33 + ], + "mask": 8590987281, + "rank": 3 + }, + { + "generators": [ + 1, + 8, + 20 + ], + "mask": 8591114498, + "rank": 3 + }, + { + "generators": [ + 9, + 10, + 15 + ], + "mask": 8592066048, + "rank": 3 + }, + { + "generators": [ + 10, + 14, + 15 + ], + "mask": 8592081920, + "rank": 3 + }, + { + "generators": [ + 10, + 15, + 20 + ], + "mask": 8593114112, + "rank": 3 + }, + { + "generators": [ + 0, + 6, + 33 + ], + "mask": 8594145345, + "rank": 3 + }, + { + "generators": [ + 1, + 8, + 22 + ], + "mask": 8594260226, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 18 + ], + "mask": 8598585368, + "rank": 3 + }, + { + "generators": [ + 3, + 18, + 19 + ], + "mask": 8599109640, + "rank": 3 + }, + { + "generators": [ + 3, + 18, + 22 + ], + "mask": 8602779656, + "rank": 3 + }, + { + "generators": [ + 2, + 7, + 12 + ], + "mask": 8606716036, + "rank": 3 + }, + { + "generators": [ + 2, + 7, + 14 + ], + "mask": 8606728324, + "rank": 3 + }, + { + "generators": [ + 2, + 7, + 19 + ], + "mask": 8607236228, + "rank": 3 + }, + { + "generators": [ + 4, + 11, + 16 + ], + "mask": 8623556624, + "rank": 3 + }, + { + "generators": [ + 6, + 11, + 16 + ], + "mask": 8623556672, + "rank": 3 + }, + { + "generators": [ + 9, + 11, + 16 + ], + "mask": 8623557120, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 13 + ], + "mask": 8657051744, + "rank": 3 + }, + { + "generators": [ + 5, + 12, + 13 + ], + "mask": 8657055776, + "rank": 3 + }, + { + "generators": [ + 1, + 8, + 27 + ], + "mask": 8724283650, + "rank": 3 + }, + { + "generators": [ + 0, + 9, + 33 + ], + "mask": 8724677121, + "rank": 3 + }, + { + "generators": [ + 5, + 13, + 27 + ], + "mask": 8791269408, + "rank": 3 + }, + { + "generators": [ + 9, + 14, + 33 + ], + "mask": 12885967360, + "rank": 3 + }, + { + "generators": [ + 10, + 15, + 32 + ], + "mask": 12887032832, + "rank": 3 + }, + { + "generators": [ + 4, + 19, + 33 + ], + "mask": 12889620496, + "rank": 3 + }, + { + "generators": [ + 3, + 18, + 32 + ], + "mask": 12893552648, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 7 + ], + "mask": 12935432583, + "rank": 3 + }, + { + "generators": [ + 5, + 13, + 32 + ], + "mask": 12952018976, + "rank": 3 + }, + { + "generators": [ + 6, + 12, + 33 + ], + "mask": 13019123776, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 16 + ], + "mask": 17180983392, + "rank": 3 + }, + { + "generators": [ + 5, + 16, + 17 + ], + "mask": 17181114400, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 34 + ], + "mask": 17181974537, + "rank": 3 + }, + { + "generators": [ + 1, + 9, + 21 + ], + "mask": 17182228994, + "rank": 3 + }, + { + "generators": [ + 5, + 16, + 21 + ], + "mask": 17183080480, + "rank": 3 + }, + { + "generators": [ + 0, + 6, + 34 + ], + "mask": 17184079937, + "rank": 3 + }, + { + "generators": [ + 1, + 9, + 22 + ], + "mask": 17184326146, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 12 + ], + "mask": 17188262272, + "rank": 3 + }, + { + "generators": [ + 8, + 12, + 13 + ], + "mask": 17188270336, + "rank": 3 + }, + { + "generators": [ + 8, + 12, + 22 + ], + "mask": 17192456448, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 15 + ], + "mask": 17196679192, + "rank": 3 + }, + { + "generators": [ + 4, + 14, + 15 + ], + "mask": 17196695568, + "rank": 3 + }, + { + "generators": [ + 0, + 7, + 34 + ], + "mask": 17213554817, + "rank": 3 + }, + { + "generators": [ + 1, + 9, + 25 + ], + "mask": 17213686274, + "rank": 3 + }, + { + "generators": [ + 4, + 15, + 25 + ], + "mask": 17230233616, + "rank": 3 + }, + { + "generators": [ + 3, + 11, + 19 + ], + "mask": 17247504392, + "rank": 3 + }, + { + "generators": [ + 6, + 11, + 19 + ], + "mask": 17247504448, + "rank": 3 + }, + { + "generators": [ + 7, + 11, + 19 + ], + "mask": 17247504512, + "rank": 3 + }, + { + "generators": [ + 2, + 10, + 13 + ], + "mask": 17314096132, + "rank": 3 + }, + { + "generators": [ + 2, + 10, + 14 + ], + "mask": 17314104324, + "rank": 3 + }, + { + "generators": [ + 2, + 10, + 17 + ], + "mask": 17314219012, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 35 + ], + "mask": 34360791057, + "rank": 3 + }, + { + "generators": [ + 1, + 10, + 20 + ], + "mask": 34361312258, + "rank": 3 + }, + { + "generators": [ + 5, + 6, + 17 + ], + "mask": 34361966688, + "rank": 3 + }, + { + "generators": [ + 6, + 16, + 17 + ], + "mask": 34362032192, + "rank": 3 + }, + { + "generators": [ + 6, + 17, + 20 + ], + "mask": 34363015232, + "rank": 3 + }, + { + "generators": [ + 7, + 8, + 13 + ], + "mask": 34363941248, + "rank": 3 + }, + { + "generators": [ + 7, + 12, + 13 + ], + "mask": 34363945088, + "rank": 3 + }, + { + "generators": [ + 0, + 5, + 35 + ], + "mask": 34368159777, + "rank": 3 + }, + { + "generators": [ + 1, + 10, + 23 + ], + "mask": 34368652290, + "rank": 3 + }, + { + "generators": [ + 7, + 13, + 23 + ], + "mask": 34372329600, + "rank": 3 + }, + { + "generators": [ + 0, + 8, + 35 + ], + "mask": 34376581377, + "rank": 3 + }, + { + "generators": [ + 1, + 10, + 24 + ], + "mask": 34377040898, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 14 + ], + "mask": 34393309208, + "rank": 3 + }, + { + "generators": [ + 3, + 14, + 15 + ], + "mask": 34393341960, + "rank": 3 + }, + { + "generators": [ + 3, + 14, + 24 + ], + "mask": 34410086408, + "rank": 3 + }, + { + "generators": [ + 2, + 9, + 12 + ], + "mask": 34426851844, + "rank": 3 + }, + { + "generators": [ + 2, + 9, + 15 + ], + "mask": 34426880516, + "rank": 3 + }, + { + "generators": [ + 2, + 9, + 16 + ], + "mask": 34426913284, + "rank": 3 + }, + { + "generators": [ + 4, + 11, + 18 + ], + "mask": 34494220304, + "rank": 3 + }, + { + "generators": [ + 5, + 11, + 18 + ], + "mask": 34494220320, + "rank": 3 + }, + { + "generators": [ + 8, + 11, + 18 + ], + "mask": 34494220544, + "rank": 3 + }, + { + "generators": [ + 5, + 16, + 35 + ], + "mask": 51540721696, + "rank": 3 + }, + { + "generators": [ + 6, + 17, + 34 + ], + "mask": 51541835840, + "rank": 3 + }, + { + "generators": [ + 7, + 13, + 34 + ], + "mask": 51543810176, + "rank": 3 + }, + { + "generators": [ + 8, + 12, + 35 + ], + "mask": 51548000512, + "rank": 3 + }, + { + "generators": [ + 4, + 15, + 35 + ], + "mask": 51556417552, + "rank": 3 + }, + { + "generators": [ + 3, + 14, + 34 + ], + "mask": 51573178376, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 9 + ], + "mask": 51741724167, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 36 + ], + "mask": 68719478791, + "rank": 3 + }, + { + "generators": [ + 3, + 6, + 11 + ], + "mask": 68719478984, + "rank": 3 + }, + { + "generators": [ + 4, + 5, + 11 + ], + "mask": 68719479088, + "rank": 3 + }, + { + "generators": [ + 2, + 12, + 15 + ], + "mask": 68719579140, + "rank": 3 + }, + { + "generators": [ + 9, + 12, + 15 + ], + "mask": 68719579648, + "rank": 3 + }, + { + "generators": [ + 2, + 13, + 14 + ], + "mask": 68719632388, + "rank": 3 + }, + { + "generators": [ + 10, + 13, + 14 + ], + "mask": 68719633408, + "rank": 3 + }, + { + "generators": [ + 4, + 5, + 18 + ], + "mask": 68719739184, + "rank": 3 + }, + { + "generators": [ + 3, + 6, + 19 + ], + "mask": 68720001224, + "rank": 3 + }, + { + "generators": [ + 1, + 20, + 23 + ], + "mask": 68745691138, + "rank": 3 + }, + { + "generators": [ + 10, + 20, + 23 + ], + "mask": 68745692160, + "rank": 3 + }, + { + "generators": [ + 19, + 20, + 23 + ], + "mask": 68746215424, + "rank": 3 + }, + { + "generators": [ + 1, + 21, + 22 + ], + "mask": 68759322626, + "rank": 3 + }, + { + "generators": [ + 9, + 21, + 22 + ], + "mask": 68759323136, + "rank": 3 + }, + { + "generators": [ + 18, + 21, + 22 + ], + "mask": 68759584768, + "rank": 3 + }, + { + "generators": [ + 3, + 6, + 26 + ], + "mask": 68786585800, + "rank": 3 + }, + { + "generators": [ + 12, + 15, + 26 + ], + "mask": 68786688000, + "rank": 3 + }, + { + "generators": [ + 0, + 10, + 36 + ], + "mask": 68786848769, + "rank": 3 + }, + { + "generators": [ + 4, + 5, + 27 + ], + "mask": 68853694768, + "rank": 3 + }, + { + "generators": [ + 13, + 14, + 27 + ], + "mask": 68853850112, + "rank": 3 + }, + { + "generators": [ + 0, + 9, + 36 + ], + "mask": 68854219265, + "rank": 3 + }, + { + "generators": [ + 0, + 28, + 31 + ], + "mask": 75430363137, + "rank": 3 + }, + { + "generators": [ + 10, + 28, + 31 + ], + "mask": 75430364160, + "rank": 3 + }, + { + "generators": [ + 18, + 28, + 31 + ], + "mask": 75430625280, + "rank": 3 + }, + { + "generators": [ + 9, + 11, + 13 + ], + "mask": 75456735744, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 5 + ], + "mask": 75470733620, + "rank": 3 + }, + { + "generators": [ + 26, + 28, + 31 + ], + "mask": 75497472000, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 6 + ], + "mask": 75564683466, + "rank": 3 + }, + { + "generators": [ + 0, + 29, + 30 + ], + "mask": 78920024065, + "rank": 3 + }, + { + "generators": [ + 9, + 29, + 30 + ], + "mask": 78920024576, + "rank": 3 + }, + { + "generators": [ + 19, + 29, + 30 + ], + "mask": 78920548352, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 6 + ], + "mask": 78946500812, + "rank": 3 + }, + { + "generators": [ + 10, + 11, + 12 + ], + "mask": 78959975424, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 5 + ], + "mask": 78987288882, + "rank": 3 + }, + { + "generators": [ + 27, + 29, + 30 + ], + "mask": 79054241792, + "rank": 3 + }, + { + "generators": [ + 3, + 6, + 34 + ], + "mask": 85899346120, + "rank": 3 + }, + { + "generators": [ + 13, + 14, + 34 + ], + "mask": 85899501568, + "rank": 3 + }, + { + "generators": [ + 1, + 9, + 36 + ], + "mask": 85899608578, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 5 + ], + "mask": 85925663025, + "rank": 3 + }, + { + "generators": [ + 21, + 22, + 34 + ], + "mask": 85939191808, + "rank": 3 + }, + { + "generators": [ + 11, + 19, + 36 + ], + "mask": 85966981120, + "rank": 3 + }, + { + "generators": [ + 2, + 10, + 36 + ], + "mask": 86033564676, + "rank": 3 + }, + { + "generators": [ + 4, + 5, + 35 + ], + "mask": 103079215408, + "rank": 3 + }, + { + "generators": [ + 12, + 15, + 35 + ], + "mask": 103079317504, + "rank": 3 + }, + { + "generators": [ + 1, + 10, + 36 + ], + "mask": 103079740418, + "rank": 3 + }, + { + "generators": [ + 20, + 23, + 35 + ], + "mask": 103105429504, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 6 + ], + "mask": 103119216841, + "rank": 3 + }, + { + "generators": [ + 2, + 9, + 36 + ], + "mask": 103146324484, + "rank": 3 + }, + { + "generators": [ + 11, + 18, + 36 + ], + "mask": 103213697024, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 37 + ], + "mask": 137438955527, + "rank": 3 + }, + { + "generators": [ + 4, + 6, + 11 + ], + "mask": 137438956112, + "rank": 3 + }, + { + "generators": [ + 3, + 5, + 11 + ], + "mask": 137438956584, + "rank": 3 + }, + { + "generators": [ + 4, + 6, + 16 + ], + "mask": 137439019600, + "rank": 3 + }, + { + "generators": [ + 3, + 5, + 17 + ], + "mask": 137439085608, + "rank": 3 + }, + { + "generators": [ + 2, + 13, + 15 + ], + "mask": 137439256580, + "rank": 3 + }, + { + "generators": [ + 8, + 13, + 15 + ], + "mask": 137439256832, + "rank": 3 + }, + { + "generators": [ + 2, + 12, + 14 + ], + "mask": 137439498244, + "rank": 3 + }, + { + "generators": [ + 7, + 12, + 14 + ], + "mask": 137439498368, + "rank": 3 + }, + { + "generators": [ + 3, + 5, + 24 + ], + "mask": 137455731752, + "rank": 3 + }, + { + "generators": [ + 0, + 8, + 37 + ], + "mask": 137455796481, + "rank": 3 + }, + { + "generators": [ + 12, + 14, + 24 + ], + "mask": 137456275456, + "rank": 3 + }, + { + "generators": [ + 4, + 6, + 25 + ], + "mask": 137472508496, + "rank": 3 + }, + { + "generators": [ + 0, + 7, + 37 + ], + "mask": 137472639105, + "rank": 3 + }, + { + "generators": [ + 13, + 15, + 25 + ], + "mask": 137472811008, + "rank": 3 + }, + { + "generators": [ + 1, + 21, + 23 + ], + "mask": 137516548098, + "rank": 3 + }, + { + "generators": [ + 7, + 21, + 23 + ], + "mask": 137516548224, + "rank": 3 + }, + { + "generators": [ + 16, + 21, + 23 + ], + "mask": 137516613632, + "rank": 3 + }, + { + "generators": [ + 1, + 20, + 22 + ], + "mask": 137578414082, + "rank": 3 + }, + { + "generators": [ + 8, + 20, + 22 + ], + "mask": 137578414336, + "rank": 3 + }, + { + "generators": [ + 17, + 20, + 22 + ], + "mask": 137578545152, + "rank": 3 + }, + { + "generators": [ + 3, + 5, + 32 + ], + "mask": 141733921832, + "rank": 3 + }, + { + "generators": [ + 1, + 7, + 37 + ], + "mask": 141733986434, + "rank": 3 + }, + { + "generators": [ + 13, + 15, + 32 + ], + "mask": 141734223872, + "rank": 3 + }, + { + "generators": [ + 11, + 17, + 37 + ], + "mask": 141750831104, + "rank": 3 + }, + { + "generators": [ + 2, + 8, + 37 + ], + "mask": 141767475460, + "rank": 3 + }, + { + "generators": [ + 21, + 23, + 32 + ], + "mask": 141811515392, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 6 + ], + "mask": 141873926737, + "rank": 3 + }, + { + "generators": [ + 4, + 6, + 33 + ], + "mask": 146028888656, + "rank": 3 + }, + { + "generators": [ + 1, + 8, + 37 + ], + "mask": 146029019394, + "rank": 3 + }, + { + "generators": [ + 12, + 14, + 33 + ], + "mask": 146029432832, + "rank": 3 + }, + { + "generators": [ + 2, + 7, + 37 + ], + "mask": 146045665412, + "rank": 3 + }, + { + "generators": [ + 11, + 16, + 37 + ], + "mask": 146062510080, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 5 + ], + "mask": 146106786857, + "rank": 3 + }, + { + "generators": [ + 20, + 22, + 33 + ], + "mask": 146168348672, + "rank": 3 + }, + { + "generators": [ + 0, + 29, + 31 + ], + "mask": 157303177217, + "rank": 3 + }, + { + "generators": [ + 7, + 29, + 31 + ], + "mask": 157303177344, + "rank": 3 + }, + { + "generators": [ + 17, + 29, + 31 + ], + "mask": 157303308288, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 6 + ], + "mask": 157320258130, + "rank": 3 + }, + { + "generators": [ + 25, + 29, + 31 + ], + "mask": 157336731648, + "rank": 3 + }, + { + "generators": [ + 8, + 11, + 12 + ], + "mask": 157381318912, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 5 + ], + "mask": 157442704428, + "rank": 3 + }, + { + "generators": [ + 0, + 28, + 30 + ], + "mask": 173140869121, + "rank": 3 + }, + { + "generators": [ + 8, + 28, + 30 + ], + "mask": 173140869376, + "rank": 3 + }, + { + "generators": [ + 16, + 28, + 30 + ], + "mask": 173140934656, + "rank": 3 + }, + { + "generators": [ + 24, + 28, + 30 + ], + "mask": 173157646336, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 5 + ], + "mask": 173174969386, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 6 + ], + "mask": 173218595412, + "rank": 3 + }, + { + "generators": [ + 7, + 11, + 13 + ], + "mask": 173280635008, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 38 + ], + "mask": 274877908999, + "rank": 3 + }, + { + "generators": [ + 3, + 8, + 11 + ], + "mask": 274877909768, + "rank": 3 + }, + { + "generators": [ + 4, + 7, + 11 + ], + "mask": 274877910160, + "rank": 3 + }, + { + "generators": [ + 4, + 7, + 14 + ], + "mask": 274877924496, + "rank": 3 + }, + { + "generators": [ + 3, + 8, + 15 + ], + "mask": 274877940488, + "rank": 3 + }, + { + "generators": [ + 2, + 12, + 17 + ], + "mask": 274878304260, + "rank": 3 + }, + { + "generators": [ + 5, + 12, + 17 + ], + "mask": 274878304288, + "rank": 3 + }, + { + "generators": [ + 2, + 13, + 16 + ], + "mask": 274878504964, + "rank": 3 + }, + { + "generators": [ + 6, + 13, + 16 + ], + "mask": 274878505024, + "rank": 3 + }, + { + "generators": [ + 3, + 8, + 22 + ], + "mask": 274882102024, + "rank": 3 + }, + { + "generators": [ + 0, + 6, + 38 + ], + "mask": 274882117697, + "rank": 3 + }, + { + "generators": [ + 12, + 17, + 22 + ], + "mask": 274882498560, + "rank": 3 + }, + { + "generators": [ + 4, + 7, + 23 + ], + "mask": 274886296720, + "rank": 3 + }, + { + "generators": [ + 0, + 5, + 38 + ], + "mask": 274886328353, + "rank": 3 + }, + { + "generators": [ + 13, + 16, + 23 + ], + "mask": 274886893568, + "rank": 3 + }, + { + "generators": [ + 1, + 20, + 25 + ], + "mask": 274979618818, + "rank": 3 + }, + { + "generators": [ + 6, + 20, + 25 + ], + "mask": 274979618880, + "rank": 3 + }, + { + "generators": [ + 15, + 20, + 25 + ], + "mask": 274979651584, + "rank": 3 + }, + { + "generators": [ + 1, + 21, + 24 + ], + "mask": 275030999042, + "rank": 3 + }, + { + "generators": [ + 5, + 21, + 24 + ], + "mask": 275030999072, + "rank": 3 + }, + { + "generators": [ + 14, + 21, + 24 + ], + "mask": 275031015424, + "rank": 3 + }, + { + "generators": [ + 3, + 8, + 30 + ], + "mask": 275951649544, + "rank": 3 + }, + { + "generators": [ + 1, + 5, + 38 + ], + "mask": 275951665186, + "rank": 3 + }, + { + "generators": [ + 13, + 16, + 30 + ], + "mask": 275952246784, + "rank": 3 + }, + { + "generators": [ + 11, + 15, + 38 + ], + "mask": 275955877888, + "rank": 3 + }, + { + "generators": [ + 2, + 6, + 38 + ], + "mask": 275960037444, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 7 + ], + "mask": 276053759121, + "rank": 3 + }, + { + "generators": [ + 21, + 24, + 30 + ], + "mask": 276104740864, + "rank": 3 + }, + { + "generators": [ + 4, + 7, + 31 + ], + "mask": 277025391760, + "rank": 3 + }, + { + "generators": [ + 1, + 6, + 38 + ], + "mask": 277025423426, + "rank": 3 + }, + { + "generators": [ + 12, + 17, + 31 + ], + "mask": 277025787904, + "rank": 3 + }, + { + "generators": [ + 2, + 5, + 38 + ], + "mask": 277029584932, + "rank": 3 + }, + { + "generators": [ + 11, + 14, + 38 + ], + "mask": 277033797632, + "rank": 3 + }, + { + "generators": [ + 20, + 25, + 31 + ], + "mask": 277127102464, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 8 + ], + "mask": 277179081481, + "rank": 3 + }, + { + "generators": [ + 0, + 28, + 33 + ], + "mask": 300916146177, + "rank": 3 + }, + { + "generators": [ + 6, + 28, + 33 + ], + "mask": 300916146240, + "rank": 3 + }, + { + "generators": [ + 14, + 28, + 33 + ], + "mask": 300916162560, + "rank": 3 + }, + { + "generators": [ + 22, + 28, + 33 + ], + "mask": 300920340480, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 8 + ], + "mask": 300924932874, + "rank": 3 + }, + { + "generators": [ + 5, + 11, + 13 + ], + "mask": 301018458144, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 7 + ], + "mask": 301069272212, + "rank": 3 + }, + { + "generators": [ + 0, + 29, + 32 + ], + "mask": 314069483521, + "rank": 3 + }, + { + "generators": [ + 5, + 29, + 32 + ], + "mask": 314069483552, + "rank": 3 + }, + { + "generators": [ + 15, + 29, + 32 + ], + "mask": 314069516288, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 7 + ], + "mask": 314074277010, + "rank": 3 + }, + { + "generators": [ + 23, + 29, + 32 + ], + "mask": 314077872128, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 8 + ], + "mask": 314171212556, + "rank": 3 + }, + { + "generators": [ + 6, + 11, + 12 + ], + "mask": 314222975040, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 39 + ], + "mask": 549755815943, + "rank": 3 + }, + { + "generators": [ + 5, + 7, + 11 + ], + "mask": 549755816608, + "rank": 3 + }, + { + "generators": [ + 6, + 8, + 11 + ], + "mask": 549755817280, + "rank": 3 + }, + { + "generators": [ + 5, + 7, + 12 + ], + "mask": 549755818656, + "rank": 3 + }, + { + "generators": [ + 6, + 8, + 13 + ], + "mask": 549755823424, + "rank": 3 + }, + { + "generators": [ + 2, + 14, + 16 + ], + "mask": 549756157956, + "rank": 3 + }, + { + "generators": [ + 4, + 14, + 16 + ], + "mask": 549756157968, + "rank": 3 + }, + { + "generators": [ + 2, + 15, + 17 + ], + "mask": 549756502020, + "rank": 3 + }, + { + "generators": [ + 3, + 15, + 17 + ], + "mask": 549756502024, + "rank": 3 + }, + { + "generators": [ + 6, + 8, + 20 + ], + "mask": 549756863808, + "rank": 3 + }, + { + "generators": [ + 0, + 4, + 39 + ], + "mask": 549756866577, + "rank": 3 + }, + { + "generators": [ + 15, + 17, + 20 + ], + "mask": 549757550592, + "rank": 3 + }, + { + "generators": [ + 5, + 7, + 21 + ], + "mask": 549757911712, + "rank": 3 + }, + { + "generators": [ + 0, + 3, + 39 + ], + "mask": 549757919241, + "rank": 3 + }, + { + "generators": [ + 14, + 16, + 21 + ], + "mask": 549758255104, + "rank": 3 + }, + { + "generators": [ + 1, + 22, + 24 + ], + "mask": 549843894274, + "rank": 3 + }, + { + "generators": [ + 3, + 22, + 24 + ], + "mask": 549843894280, + "rank": 3 + }, + { + "generators": [ + 12, + 22, + 24 + ], + "mask": 549843898368, + "rank": 3 + }, + { + "generators": [ + 1, + 23, + 25 + ], + "mask": 549931974658, + "rank": 3 + }, + { + "generators": [ + 4, + 23, + 25 + ], + "mask": 549931974672, + "rank": 3 + }, + { + "generators": [ + 13, + 23, + 25 + ], + "mask": 549931982848, + "rank": 3 + }, + { + "generators": [ + 6, + 8, + 28 + ], + "mask": 550024250688, + "rank": 3 + }, + { + "generators": [ + 1, + 3, + 39 + ], + "mask": 550024253450, + "rank": 3 + }, + { + "generators": [ + 14, + 16, + 28 + ], + "mask": 550024593408, + "rank": 3 + }, + { + "generators": [ + 11, + 13, + 39 + ], + "mask": 550025308160, + "rank": 3 + }, + { + "generators": [ + 2, + 4, + 39 + ], + "mask": 550026346516, + "rank": 3 + }, + { + "generators": [ + 22, + 24, + 28 + ], + "mask": 550112329728, + "rank": 3 + }, + { + "generators": [ + 0, + 5, + 7 + ], + "mask": 550201098913, + "rank": 3 + }, + { + "generators": [ + 5, + 7, + 29 + ], + "mask": 550292685472, + "rank": 3 + }, + { + "generators": [ + 1, + 4, + 39 + ], + "mask": 550292693010, + "rank": 3 + }, + { + "generators": [ + 15, + 17, + 29 + ], + "mask": 550293372928, + "rank": 3 + }, + { + "generators": [ + 2, + 3, + 39 + ], + "mask": 550293733388, + "rank": 3 + }, + { + "generators": [ + 11, + 12, + 39 + ], + "mask": 550294788096, + "rank": 3 + }, + { + "generators": [ + 0, + 6, + 8 + ], + "mask": 550381110593, + "rank": 3 + }, + { + "generators": [ + 23, + 25, + 29 + ], + "mask": 550468845568, + "rank": 3 + }, + { + "generators": [ + 0, + 30, + 32 + ], + "mask": 572304392193, + "rank": 3 + }, + { + "generators": [ + 3, + 30, + 32 + ], + "mask": 572304392200, + "rank": 3 + }, + { + "generators": [ + 13, + 30, + 32 + ], + "mask": 572304400384, + "rank": 3 + }, + { + "generators": [ + 1, + 5, + 7 + ], + "mask": 572305785506, + "rank": 3 + }, + { + "generators": [ + 21, + 30, + 32 + ], + "mask": 572306489344, + "rank": 3 + }, + { + "generators": [ + 4, + 11, + 15 + ], + "mask": 572393162768, + "rank": 3 + }, + { + "generators": [ + 2, + 6, + 8 + ], + "mask": 572480558404, + "rank": 3 + }, + { + "generators": [ + 0, + 31, + 33 + ], + "mask": 594852970497, + "rank": 3 + }, + { + "generators": [ + 4, + 31, + 33 + ], + "mask": 594852970512, + "rank": 3 + }, + { + "generators": [ + 12, + 31, + 33 + ], + "mask": 594852974592, + "rank": 3 + }, + { + "generators": [ + 20, + 31, + 33 + ], + "mask": 594854019072, + "rank": 3 + }, + { + "generators": [ + 1, + 6, + 8 + ], + "mask": 594855757122, + "rank": 3 + }, + { + "generators": [ + 2, + 5, + 7 + ], + "mask": 594941059748, + "rank": 3 + }, + { + "generators": [ + 3, + 11, + 14 + ], + "mask": 595029477384, + "rank": 3 + }, + { + "generators": [ + 0, + 36, + 37 + ], + "mask": 1030792151041, + "rank": 3 + }, + { + "generators": [ + 1, + 36, + 37 + ], + "mask": 1030792151042, + "rank": 3 + }, + { + "generators": [ + 2, + 36, + 37 + ], + "mask": 1030792151044, + "rank": 3 + }, + { + "generators": [ + 3, + 4, + 5 + ], + "mask": 1030792153080, + "rank": 3 + }, + { + "generators": [ + 11, + 36, + 37 + ], + "mask": 1030792153088, + "rank": 3 + }, + { + "generators": [ + 12, + 13, + 14 + ], + "mask": 1030793195520, + "rank": 3 + }, + { + "generators": [ + 20, + 21, + 22 + ], + "mask": 1031059537920, + "rank": 3 + }, + { + "generators": [ + 28, + 29, + 30 + ], + "mask": 1099243192320, + "rank": 3 + }, + { + "generators": [ + 0, + 1, + 3, + 5 + ], + "mask": 1099511627775, + "rank": 4 + } + ], + "maximal_clique_census": [ + [ + 4, + 90 + ], + [ + 7, + 2880 + ] + ], + "nonorthogonality_masks": [ + 268435454, + 68452089853, + 68718432251, + 527118464999, + 504482150375, + 785288652703, + 798493169567, + 942130308735, + 926230992511, + 1020551651839, + 1024054891007, + 68719472647, + 504570563931, + 527031061179, + 798442339179, + 785340382451, + 926292966827, + 942068792275, + 1024040632011, + 1020564602675, + 504654822077, + 527203745117, + 798582500597, + 785428962157, + 926319881173, + 942157815213, + 1023879835445, + 1020390121165, + 548862081726, + 548773657950, + 821258804470, + 821310385006, + 949109873622, + 949047766446, + 979212541750, + 979226226382, + 979050426872, + 949137241720, + 821399861144, + 548947347424 + ], + "representatives": [ + [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + -2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ] + ], + "root_orbits_sha256": "9fc99d6eab0e17a53ef6b9b0e95c3928ecd531d59442b5b1b123337b46109673" + }, + "independent_fraction_pairs": 258, + "negative_controls": [ + "nonclique_orthogonal_pair", + "missing_decoder_diagonal", + "forbidden_decoder_entry", + "increased_maximum_clique_weight", + "source_dimension_substituted_for_pairing_rank", + "missing_eisenstein_direction", + "underweighted_dual", + "omitted_dual_flat_pair" + ], + "one_line_extensions_checked": 30880, + "optimistic_Dfc": { + "conclusion": "Does not exclude three or more stages; no achieved supplier.", + "rational_copy_floor": 44, + "three_stage_upper_deficit": 28, + "upper_deficit_per_replica": "36*s-80" + }, + "primal": { + "flat_pairs_checked": 298378, + "maximum_clique_weight": "1/960", + "maximum_cliques": [ + 687, + 695, + 719, + 727, + 815, + 823, + 847, + 855, + 1199, + 1207, + 1231, + 1239, + 1327, + 1335, + 1359, + 1367, + 5451, + 5459, + 8875, + 8883, + 17195, + 17227, + 20811, + 25131, + 33971, + 34003, + 37971, + 41139, + 66731, + 66859, + 70923, + 73899, + 82219, + 86283, + 90155, + 99491, + 106659, + 131795, + 131923, + 135507, + 139923, + 148291, + 151875, + 164051, + 168019, + 172179, + 262859, + 263371, + 267339, + 270987, + 279115, + 282699, + 287243, + 296131, + 300099, + 328843, + 332811, + 336011, + 348171, + 350211, + 352267, + 354307, + 361603, + 365571, + 366595, + 368771, + 370691, + 393923, + 402051, + 410179, + 413763, + 415747, + 418307, + 419843, + 426179, + 430147, + 432131, + 434307, + 436227, + 525107, + 525619, + 529683, + 533043, + 541475, + 549411, + 558131, + 562195, + 565299, + 591139, + 595203, + 606499, + 610563, + 612355, + 614435, + 616451, + 623651, + 627715, + 628739, + 630819, + 632835, + 656147, + 659731, + 664083, + 672515, + 676099, + 677891, + 680451, + 681987, + 692243, + 694275, + 696339, + 698371, + 1049261, + 1049269, + 1057449, + 1057457, + 1073705, + 1122473, + 1138729, + 1319561, + 1335817, + 1384585, + 1396745, + 1398785, + 1400841, + 1402881, + 2098509, + 2098517, + 2102601, + 2102609, + 2135121, + 2232657, + 2265169, + 2626833, + 2659345, + 2756881, + 2789393, + 2791425, + 2793489, + 2795521, + 4195509, + 4195541, + 4228273, + 4228305, + 4235441, + 4293793, + 4300961, + 4752433, + 4759601, + 4808737, + 4810753, + 4817953, + 4825121, + 4827137, + 5243061, + 5251249, + 5316769, + 5333025, + 5335041, + 6292565, + 6325329, + 6849553, + 6856721, + 6858753, + 8389421, + 8389453, + 8405801, + 8405833, + 8409417, + 8536897, + 8540481, + 8667721, + 8671305, + 8798785, + 8802369, + 8804353, + 8818753, + 8820737, + 9437741, + 9454121, + 9716233, + 9719817, + 9721857, + 10486093, + 10490185, + 10621249, + 10653761, + 10655745, + 16777941, + 16778069, + 16909009, + 16909137, + 16917137, + 16941265, + 16949393, + 17145985, + 17147905, + 17171137, + 17179265, + 17203393, + 17211521, + 17213441, + 17826453, + 17834641, + 18096769, + 18161793, + 18163713, + 18874709, + 19005777, + 19038289, + 19046417, + 19048449, + 20971733, + 21004497, + 21012625, + 21078145, + 21080065, + 22020245, + 22028433, + 22093953, + 22095873, + 23068757, + 23101521, + 23109649, + 23111681, + 25166661, + 25297729, + 25559617, + 25591873, + 25593857, + 27263301, + 27394369, + 27426881, + 27428865, + 33555629, + 33555757, + 33621161, + 33621289, + 33625353, + 33636649, + 33640713, + 34145569, + 34149633, + 34160929, + 34164993, + 34166785, + 34230529, + 34232321, + 34603181, + 34668713, + 34684969, + 34689033, + 34691073, + 35652877, + 35656969, + 36181249, + 36311297, + 36313089, + 37749925, + 37815457, + 38339617, + 38354977, + 38356993, + 38797477, + 38863009, + 38879265, + 38881281, + 41943341, + 41959721, + 41963785, + 42094849, + 42096641, + 42991661, + 43008041, + 43012105, + 43014145, + 44040461, + 44044553, + 44175617, + 44177409, + 67109685, + 67110197, + 67527169, + 67528705, + 67633969, + 67634481, + 67641905, + 67650337, + 67658273, + 67765009, + 67772945, + 67781377, + 67789313, + 67790849, + 68158005, + 68166193, + 68182561, + 68444673, + 68446209, + 69207317, + 69731601, + 69861649, + 69869585, + 69871617, + 71304245, + 71828529, + 71835697, + 71852065, + 71854081, + 72351797, + 72359985, + 72376353, + 72378369, + 73401365, + 73925649, + 73932817, + 73934849, + 75498277, + 75514657, + 75645697, + 75907585, + 75909121, + 76546597, + 76562977, + 76825089, + 76826625, + 83886869, + 84017937, + 84025873, + 84288001, + 84289537, + 84935189, + 84943377, + 85205505, + 85207041, + 85983509, + 86114577, + 86122513, + 86124545, + 89128981, + 89131013, + 89137169, + 89139201, + 90177557, + 90179589, + 90185745, + 90187777, + 92275461, + 92406529, + 92668417, + 92669953, + 93323781, + 93325317, + 93585921, + 93587457, + 94372101, + 94373893, + 94503169, + 94504961, + 100664613, + 101188897, + 101204257, + 101335297, + 101337089, + 102761733, + 103286017, + 103416065, + 103417857, + 104858661, + 105382945, + 105398305, + 105400321, + 105906213, + 105908229, + 105922593, + 105924609, + 106955781, + 106956805, + 107480065, + 107481089, + 109052197, + 109068577, + 109199617, + 109201409, + 110100517, + 110102533, + 110116897, + 110118913, + 111149317, + 111151109, + 111280385, + 111282177, + 134218445, + 134218957, + 134480585, + 134481097, + 134485065, + 134513857, + 134517825, + 134546569, + 134550537, + 134579329, + 134583297, + 134584321, + 134845441, + 134846465, + 135266957, + 135529097, + 135594121, + 135598089, + 135600129, + 136315981, + 136320073, + 136352833, + 136877057, + 136878081, + 138413253, + 138446017, + 138511489, + 139035649, + 139036673, + 140510277, + 140543041, + 141067265, + 141068289, + 142606925, + 142869065, + 142872649, + 142905409, + 142907393, + 143655437, + 143917577, + 143921161, + 143923201, + 144703565, + 144707657, + 144740417, + 144742401, + 150995653, + 151257793, + 151290049, + 151355521, + 151357441, + 152044165, + 152306305, + 152371329, + 152373249, + 155189445, + 155222209, + 155287681, + 155289601, + 156237957, + 156239877, + 156303489, + 156305409, + 157286469, + 157288453, + 157319233, + 157321217, + 159384133, + 159646273, + 159678529, + 159680513, + 160432645, + 160434181, + 160694785, + 160696321, + 161480773, + 161482757, + 161513537, + 161515521, + 167773325, + 167838857, + 167842825, + 168367105, + 168368129, + 168820877, + 168886409, + 168890377, + 168892417, + 169870349, + 169874441, + 170398721, + 170399745, + 171967621, + 172033153, + 172557313, + 172558337, + 173015173, + 173017093, + 173080705, + 173082625, + 174064645, + 174065669, + 174588929, + 174589953, + 177209357, + 177211397, + 177213449, + 177215489, + 178257933, + 178259973, + 178262025, + 178264065, + 268436142, + 268436150, + 268444330, + 268444338, + 268476594, + 268575378, + 268607634, + 268968498, + 269000754, + 269099538, + 269127698, + 269129730, + 269131794, + 269133826, + 269484716, + 269484724, + 269492904, + 269492912, + 271224848, + 271226880, + 271228944, + 271230976, + 277873196, + 279091200, + 303038636, + 304748544, + 311427116, + 312612864, + 403702412, + 405313536, + 412090892, + 413177856, + 437256332, + 438835200, + 445644812, + 445646852, + 445648904, + 445650944, + 446693388, + 446695428, + 446697480, + 446699520, + 536872270, + 536872278, + 536876362, + 536876370, + 536891722, + 536941834, + 536957194, + 537138250, + 537153610, + 537203722, + 537219082, + 537221122, + 537223178, + 537225218, + 538267656, + 538269696, + 538271752, + 538273792, + 538969420, + 538969428, + 538973512, + 538973520, + 542205952, + 543163476, + 555034624, + 555745620, + 558966784, + 559939668, + 605317120, + 606078228, + 609249280, + 610272276, + 622077952, + 622854420, + 625999892, + 626001924, + 626008080, + 626010112, + 627048468, + 627050500, + 627056656, + 627058688, + 1073743030, + 1073743062, + 1073775794, + 1073775826, + 1073779794, + 1073905874, + 1073909842, + 1074037954, + 1074041922, + 1074155586, + 1074157570, + 1074168002, + 1074171970, + 1074173954, + 1077937332, + 1077937364, + 1077970096, + 1077970128, + 1078984884, + 1082544192, + 1082546176, + 1082560576, + 1082562560, + 1083463680, + 1111491748, + 1112539300, + 1115838464, + 1116755968, + 1145046068, + 1146093620, + 1149650944, + 1150568448, + 1178600484, + 1179648036, + 1179650052, + 1179664416, + 1179666432, + 1182943232, + 1183842340, + 1183844356, + 1183858720, + 1183860736, + 1342177462, + 1342210226, + 1342341266, + 1342345234, + 1342347266, + 1343226036, + 1350735872, + 1376780452, + 1384257536, + 1385168932, + 1385170948, + 1385175040, + 1610613846, + 1610617938, + 1610880066, + 1610895426, + 1610897410, + 1611945984, + 1614808148, + 1679050752, + 1681916948, + 1682964500, + 1682966532, + 1682982912, + 2147484462, + 2147484494, + 2147500842, + 2147500874, + 2147508778, + 2147565866, + 2147573802, + 2148025122, + 2148033058, + 2148090146, + 2148098082, + 2148100098, + 2148114466, + 2148116482, + 2152292384, + 2152294400, + 2152308768, + 2152310784, + 2154342400, + 2155873068, + 2155873100, + 2155889448, + 2155889480, + 2157969740, + 2168563712, + 2170595328, + 2172650308, + 2174746948, + 2286520320, + 2288551936, + 2290090572, + 2292187212, + 2302773248, + 2304770116, + 2304772100, + 2304802880, + 2304804864, + 2306867780, + 2308964420, + 2308966404, + 2308997184, + 2308999168, + 2415919662, + 2415927850, + 2416452130, + 2416484386, + 2416486402, + 2418583552, + 2424308268, + 2552793088, + 2558525964, + 2560622604, + 2560624644, + 2560657408, + 2684354894, + 2684371274, + 2684436746, + 2684444682, + 2684446722, + 2686452044, + 2688641024, + 2703229252, + 2705401856, + 2707423300, + 2707425284, + 2707433472, + 4294968022, + 4294968150, + 4295099090, + 4295099218, + 4295102802, + 4295115586, + 4295119170, + 4295577858, + 4295579650, + 4295623442, + 4295627026, + 4295639810, + 4295643394, + 4295645186, + 4311745236, + 4311745364, + 4311876304, + 4311876432, + 4312793748, + 4315939028, + 4316987540, + 4329132288, + 4329134080, + 4329197824, + 4329199616, + 4329658368, + 4333324288, + 4333848576, + 4445962948, + 4447011460, + 4450156740, + 4451205252, + 4451207172, + 4451270784, + 4451272704, + 4463335424, + 4463859712, + 4467525632, + 4467982468, + 4467984388, + 4468048000, + 4468049920, + 4563403414, + 4563534482, + 4564058642, + 4564062226, + 4564064258, + 4564451988, + 4597618688, + 4698669700, + 4731705344, + 4732223620, + 4732225540, + 4732229632, + 4831838550, + 4831842642, + 4831859010, + 4831924482, + 4831926274, + 4832974848, + 4837165056, + 4848615764, + 4852809812, + 4853858324, + 4853860356, + 4853925888, + 5368709334, + 5368840402, + 5368844370, + 5368860738, + 5368862722, + 5372903636, + 5373952148, + 5402417152, + 5403334656, + 5407506564, + 5407508484, + 5407524864, + 5637144726, + 5637275794, + 5637279762, + 5637281794, + 5638193300, + 5670836224, + 5671747716, + 5671749636, + 5671753728, + 5905580118, + 5905584210, + 5905600578, + 5905602562, + 5906651136, + 5909774420, + 5910822932, + 5910824964, + 5910841344, + 6442451782, + 6442468162, + 6442992386, + 6443057410, + 6443059202, + 6447253504, + 6459228996, + 6581454848, + 6593446468, + 6597640260, + 6597642244, + 6597707776, + 6979322182, + 6979338562, + 6979404034, + 6979405826, + 6983600128, + 6996099396, + 7000293444, + 7000295428, + 7000360960, + 8589935790, + 8589935918, + 8590001322, + 8590001450, + 8590008490, + 8590034082, + 8590041250, + 8590263434, + 8590270602, + 8590296194, + 8590303362, + 8590305282, + 8590368898, + 8590370818, + 8607080576, + 8607082496, + 8607146112, + 8607148032, + 8608983040, + 8615528448, + 8617363456, + 8623490220, + 8623490348, + 8623555752, + 8623555880, + 8625587468, + 8631877932, + 8633975052, + 8674224128, + 8676059136, + 8682604544, + 8684306692, + 8684308484, + 8684437760, + 8684439552, + 8690599204, + 8692696324, + 8698986788, + 8701083908, + 8701085700, + 8701214976, + 8701216768, + 8858370222, + 8858378410, + 8858411170, + 8858542210, + 8858544130, + 8860641280, + 8869021696, + 8891924652, + 8900313132, + 8902410252, + 8902412292, + 8902543360, + 9126806798, + 9126872330, + 9127134218, + 9127141386, + 9127143426, + 9128903948, + 9143920640, + 9196012804, + 9210963968, + 9212788996, + 9212790788, + 9212798976, + 9663677606, + 9663710370, + 9663972482, + 9664102530, + 9664104450, + 9672493056, + 9697232036, + 9739569152, + 9764340772, + 9772728356, + 9772730372, + 9772861440, + 9932112038, + 9932144802, + 9932275842, + 9932277762, + 9940666368, + 9965666468, + 9974054948, + 9974056964, + 9974188032, + 10737418542, + 10737484074, + 10737492010, + 10737524770, + 10737526786, + 10745807148, + 10747904268, + 10754304000, + 10756335616, + 10764681476, + 10764683268, + 10764716032, + 11005853742, + 11005861930, + 11005894690, + 11005896706, + 11007993856, + 11014242348, + 11016339468, + 11016341508, + 11016374272, + 11274289422, + 11274354954, + 11274362890, + 11274364930, + 11276386572, + 11291142144, + 11293163780, + 11293165572, + 11293173760, + 17179870006, + 17179870518, + 17180234754, + 17180235778, + 17180394290, + 17180394802, + 17180398866, + 17180427314, + 17180431378, + 17180460322, + 17180464386, + 17180492834, + 17180496898, + 17180497922, + 17246978868, + 17246979380, + 17247503152, + 17247503664, + 17248027188, + 17255367460, + 17256415780, + 17263756052, + 17264804372, + 17272144644, + 17273192964, + 17273194500, + 17273455104, + 17273456640, + 17314452480, + 17314453504, + 17314714624, + 17314715648, + 17315469312, + 17322776576, + 17323792384, + 17331226624, + 17332242432, + 17339549696, + 17340301828, + 17340303364, + 17340563968, + 17340565504, + 17448305206, + 17448829490, + 17448861746, + 17448865810, + 17448867842, + 17449353780, + 17457742372, + 17583085568, + 17590949888, + 17591960068, + 17591961604, + 17591965696, + 17716741398, + 17716745490, + 17716811010, + 17717072898, + 17717073922, + 17718122496, + 17734895616, + 17783850260, + 17800626452, + 17801674772, + 17801676804, + 17801938944, + 18253612086, + 18253644850, + 18253648914, + 18253911042, + 18253912066, + 18262300672, + 18263316480, + 18320720948, + 18321768500, + 18330157092, + 18330159108, + 18330421248, + 18522046518, + 18522079282, + 18522083346, + 18522085378, + 18523095092, + 18530473984, + 18531483684, + 18531485700, + 18531489792, + 18790482966, + 18790487058, + 18790749186, + 18790750210, + 18791798784, + 18857591828, + 18858639380, + 18858641412, + 18858903552, + 19327353638, + 19327877922, + 19327942946, + 19327975458, + 19327977474, + 19335742244, + 19352519428, + 19462195200, + 19478448128, + 19486736900, + 19486738436, + 19486771200, + 19595788838, + 19596313122, + 19596345378, + 19596347394, + 19604177444, + 19730565120, + 19738395140, + 19738396676, + 19738429440, + 21474837270, + 21475361554, + 21475365138, + 21475430658, + 21475432450, + 21491614484, + 21492662804, + 21609650176, + 21610174464, + 21626880516, + 21626882052, + 21626947584, + 21743272470, + 21743796754, + 21743800338, + 21743802370, + 21744321044, + 21878020096, + 21878538756, + 21878540292, + 21878544384, + 22011707670, + 22011711762, + 22011777282, + 22011779074, + 22012827648, + 22028484884, + 22029533204, + 22029535236, + 22029600768, + 22817013782, + 22817015814, + 22817017874, + 22817019906, + 22818062356, + 22818064388, + 22818066448, + 22818068480, + 23085449238, + 23085451270, + 23085453330, + 23085455362, + 23086497812, + 23086499844, + 23086501904, + 23086503936, + 23622320902, + 23622845186, + 23622910210, + 23622912002, + 23639098116, + 23757129728, + 23773315588, + 23773317124, + 23773382656, + 23890756102, + 23890757638, + 23891280386, + 23891281922, + 24024973828, + 24024975364, + 24025498112, + 24025499648, + 24159191302, + 24159193094, + 24159256834, + 24159258626, + 24175968516, + 24175970308, + 24176034048, + 24176035840, + 25769805094, + 25769870626, + 25769903138, + 25770165250, + 25770166274, + 25786943488, + 25795266560, + 25836913956, + 25845301540, + 25862078724, + 25862080516, + 25862342656, + 26306675974, + 26306741506, + 26307003394, + 26307004418, + 26323781632, + 26373784836, + 26390561028, + 26390562820, + 26390824960, + 26843546662, + 26843579426, + 26843841538, + 26843842562, + 26852231168, + 26910655524, + 26919043108, + 26919045124, + 26919307264, + 27111981094, + 27111983110, + 27112013858, + 27112015874, + 27120369700, + 27120371716, + 27120402464, + 27120404480, + 27380417542, + 27380418566, + 27380679682, + 27380680706, + 27447526404, + 27447527428, + 27447788544, + 27447789568, + 27917287718, + 27917353250, + 27917385762, + 27917387778, + 27925676324, + 27934164992, + 27942453508, + 27942455300, + 27942488064, + 28185722918, + 28185724934, + 28185755682, + 28185757698, + 28194111524, + 28194113540, + 28194144288, + 28194146304, + 28454158598, + 28454160390, + 28454224130, + 28454225922, + 28470935812, + 28470937604, + 28471001344, + 28471003136, + 34359739086, + 34359739598, + 34360001226, + 34360001738, + 34360009354, + 34360017482, + 34360025610, + 34360132290, + 34360140418, + 34360148546, + 34360156674, + 34360158210, + 34360418818, + 34360420354, + 34427265536, + 34427267072, + 34427527680, + 34427529216, + 34429609984, + 34431592448, + 34433673216, + 34461075456, + 34463156224, + 34465138688, + 34466694148, + 34466695172, + 34467218432, + 34467219456, + 34493956812, + 34493957324, + 34494218952, + 34494219464, + 34496054348, + 34498151620, + 34500248644, + 34527511692, + 34529608716, + 34531705988, + 34533803012, + 34533804036, + 34534327296, + 34534328320, + 34628174478, + 34628182666, + 34628313730, + 34628837890, + 34628839426, + 34630936576, + 34664482816, + 34762392204, + 34795946124, + 34798043148, + 34798045188, + 34798569472, + 34896610382, + 34896872522, + 34896887882, + 34896896010, + 34896898050, + 34898707532, + 34902901828, + 34964006912, + 34967939072, + 34970010628, + 34970011652, + 34970019840, + 35433481414, + 35433743554, + 35433873602, + 35433889858, + 35433891842, + 35437675716, + 35471230084, + 35501000704, + 35534292992, + 35538338820, + 35538339844, + 35538356224, + 35970352198, + 35970614338, + 35970629698, + 35970631682, + 35974546500, + 36037740544, + 36041655300, + 36041656324, + 36041672704, + 36507222606, + 36507238986, + 36507247114, + 36507771394, + 36507772930, + 36511967232, + 36514048000, + 36641440332, + 36643536972, + 36647731268, + 36647733252, + 36648257536, + 36775657998, + 36775666186, + 36776190466, + 36776192002, + 36778289152, + 36909875724, + 36911972364, + 36911974404, + 36912498688, + 37044093006, + 37044109386, + 37044117514, + 37044119554, + 37046190156, + 37048313856, + 37050384452, + 37050386436, + 37050394624, + 38654706374, + 38654837442, + 38654853698, + 38655377922, + 38655379458, + 38688933888, + 38692997120, + 38788924100, + 38793117892, + 38826672260, + 38826674180, + 38827198464, + 38923141766, + 38923272834, + 38923796994, + 38923798530, + 38957352960, + 39057359492, + 39090913412, + 39090915332, + 39091439616, + 39728447686, + 39728578754, + 39728595010, + 39728596994, + 39732641988, + 39762151424, + 39766196356, + 39766198276, + 39766214656, + 39996883078, + 39996884998, + 39997014146, + 39997016066, + 40030437508, + 40030439428, + 40030568576, + 40030570496, + 40265318470, + 40265320454, + 40265334850, + 40265336834, + 40269512772, + 40269514756, + 40269529152, + 40269531136, + 40802189894, + 40802206274, + 40802730498, + 40802732034, + 40806926336, + 40936407620, + 40940601412, + 40940603396, + 40941127680, + 41070625286, + 41070626822, + 41071149570, + 41071151106, + 41204843012, + 41204844548, + 41205367296, + 41205368832, + 41339060294, + 41339062278, + 41339076674, + 41339078658, + 41343254596, + 41343256580, + 41343270976, + 41343272960, + 42949674126, + 42949936266, + 42949943434, + 42950074498, + 42950076418, + 42983228556, + 42985325580, + 43017185280, + 43019020288, + 43052434436, + 43052435460, + 43052566528, + 43218108558, + 43218116746, + 43218247810, + 43218249730, + 43220346880, + 43251662988, + 43253760012, + 43253762052, + 43253893120, + 43486544910, + 43486807050, + 43486814218, + 43486816258, + 43488642060, + 43553925120, + 43555750916, + 43555751940, + 43555760128, + 44023415942, + 44023678082, + 44023808130, + 44023810050, + 44056970372, + 44090918912, + 44124079108, + 44124080132, + 44124211200, + 44291850374, + 44291852294, + 44291981442, + 44291983362, + 44325404804, + 44325406724, + 44325535872, + 44325537792, + 44560286726, + 44560287750, + 44560548866, + 44560549890, + 44627395588, + 44627396612, + 44627657728, + 44627658752, + 45365592078, + 45365594118, + 45365600266, + 45365602306, + 45367689228, + 45367691268, + 45367697416, + 45367699456, + 45634027534, + 45634029574, + 45634035722, + 45634037762, + 45636124684, + 45636126724, + 45636132872, + 45636134912, + 68720599208, + 68720615464, + 68721709392, + 68721741904, + 68723712176, + 68723777696, + 68724727984, + 68724793504, + 68724809760, + 68727886152, + 68728017216, + 68729966920, + 68730097984, + 68730130496, + 68736418000, + 68736426128, + 68738482512, + 68738515024, + 68738523152, + 68740481232, + 68740489360, + 68740554880, + 68741505168, + 68741570688, + 68742578256, + 68742586384, + 68746871104, + 68746903616, + 68753113384, + 68753117448, + 68754145448, + 68754161704, + 68754165768, + 68758339744, + 68758356000, + 68761436456, + 68761440520, + 68761571584, + 68762484776, + 68762488840, + 68763521288, + 68763652352, + 68987953328, + 68988084368, + 68988969128, + 68988969136, + 68990177296, + 68990181392, + 68998565888, + 69022515368, + 69030903848, + 69030907912, + 69031956488, + 69032087552, + 69256368456, + 69256433928, + 69257482248, + 69257486344, + 69258449224, + 69258449232, + 69261680640, + 69275222352, + 69278375952, + 69278441472, + 69279416400, + 69279424528, + 69793382608, + 69793386576, + 69797445808, + 69797445840, + 69798461616, + 69801758784, + 69801775168, + 69832016032, + 69832032288, + 69835313152, + 69836226592, + 69836230656, + 70061686960, + 70061818000, + 70061821968, + 70062702768, + 70070210560, + 70096257184, + 70103732224, + 70104645664, + 70104649728, + 70867042600, + 70867050536, + 70871244832, + 70871261216, + 70875365672, + 70875365704, + 70877446472, + 70888038400, + 70890061888, + 70890070016, + 70894223680, + 70894256192, + 71403848008, + 71403913480, + 71403921416, + 71405928776, + 71408115712, + 71422705984, + 71424876544, + 71426900032, + 71426908160, + 73014579536, + 73014595904, + 73031352528, + 73031352656, + 73035415760, + 73036464272, + 73036529792, + 73048084736, + 73048150272, + 73049133056, + 73053307008, + 73053323264, + 73551319376, + 73551335744, + 73551401216, + 73552449536, + 73556639744, + 73568092496, + 73572286544, + 73573335056, + 73573400576, + 74088317136, + 74088321104, + 74088337472, + 74092380368, + 74093428880, + 74121891840, + 74122809344, + 74126983296, + 74126999552, + 74356752528, + 74356756496, + 74357670032, + 74357674000, + 74390306944, + 74390310912, + 74391224448, + 74391228416, + 74625060944, + 74625077312, + 74626109456, + 74626125824, + 74629251152, + 74629267520, + 74630299664, + 74630316032, + 75698815296, + 75698880768, + 75703009344, + 75703074816, + 75715576128, + 75715641600, + 75719770176, + 75719835648, + 77309485224, + 77309517984, + 77326295168, + 77326360704, + 77328457728, + 77336805632, + 77336838144, + 77343031464, + 77343031592, + 77351354664, + 77353451784, + 77353582848, + 77577855144, + 77577887904, + 77578018944, + 77580115968, + 77588496384, + 77611401384, + 77619789864, + 77621886984, + 77622018048, + 78651621536, + 78651752576, + 78660010016, + 78660141056, + 78685143200, + 78685274240, + 78693531680, + 78693662720, + 79456960808, + 79456968744, + 79457001504, + 79465283880, + 79467381000, + 79473778688, + 79475810304, + 79484158208, + 79484190720, + 79725338664, + 79725371424, + 79727435784, + 79727468544, + 79733719080, + 79733751840, + 79735816200, + 79735848960, + 79993831688, + 79993839624, + 79995863304, + 79995871240, + 80010608896, + 80010616832, + 80012640512, + 80012648448, + 137440027176, + 137440289288, + 137441088592, + 137441612816, + 137443705904, + 137443713072, + 137445278800, + 137445803024, + 137445810192, + 137447621192, + 137447624776, + 137448407592, + 137448669704, + 137448673288, + 137506595376, + 137506611744, + 137507119664, + 137507136032, + 137507398144, + 137510782000, + 137510789168, + 137510805536, + 137511313456, + 137511329824, + 137512879120, + 137512886288, + 137515516448, + 137515778560, + 137573438536, + 137573471296, + 137575273544, + 137575306304, + 137575830528, + 137579496512, + 137580020736, + 137581822536, + 137581826120, + 137581858880, + 137582871048, + 137582874632, + 137583661128, + 137583693888, + 137707921968, + 137707954224, + 137708446248, + 137708446256, + 137710047248, + 137710051344, + 137716826664, + 137844264960, + 137851044360, + 137851047944, + 137852096520, + 137852129280, + 137976091720, + 137976107080, + 137977155592, + 137977159688, + 137977926728, + 137977926736, + 137982116944, + 138044268544, + 138048184336, + 138048200704, + 138049225744, + 138049232912, + 138512733264, + 138512995392, + 138516923440, + 138516923472, + 138521366592, + 138521382976, + 138522415104, + 138583999536, + 138585047088, + 138585063456, + 138589257760, + 138589519872, + 139049571408, + 139049833536, + 139049848896, + 139050897408, + 139053761616, + 139118002176, + 139120870416, + 139121917968, + 139121934336, + 139586462248, + 139586986528, + 139591180320, + 139591196704, + 139593293824, + 139594842664, + 139594842696, + 139726979136, + 139727503360, + 139729044040, + 139731140680, + 139731173440, + 139854881320, + 139855405600, + 139855437856, + 139857534976, + 139863261736, + 139991744512, + 139997479432, + 139999576072, + 139999608832, + 154619380784, + 154619384848, + 154686456368, + 154686456880, + 154686980656, + 154695369248, + 154695631360, + 154753340416, + 154753602560, + 154761728000, + 154762740224, + 154762743808, + 154887782960, + 154887815216, + 154887819280, + 154888307248, + 154896695840, + 155022036992, + 155029901312, + 155030913536, + 155030917120, + 155692598320, + 155692602384, + 155692864512, + 155701252096, + 155702267904, + 155759674416, + 155760721968, + 155769110560, + 155769372672, + 155961032752, + 155961036816, + 155962048560, + 155962052624, + 155969421344, + 155969425408, + 155970437152, + 155970441216, + 156229440528, + 156229702656, + 156230488080, + 156230750208, + 156296545296, + 156296807424, + 156297592848, + 156297854976, + 157035266592, + 157035298848, + 157043130912, + 157043163168, + 157169484288, + 157169516544, + 157177348608, + 157177380864, + 171798970952, + 171798979080, + 171866087936, + 171866350080, + 171870543872, + 171872617472, + 171872624640, + 171933172296, + 171933172808, + 171935007816, + 171939202112, + 171939726336, + 172335825992, + 172335841352, + 172335849480, + 172337661000, + 172341855296, + 172402958336, + 172406890496, + 172408964096, + 172408971264, + 173409567808, + 173409583168, + 173413499968, + 173413515328, + 173476676608, + 173476691968, + 173480608768, + 173480624128, + 173946192456, + 173946200584, + 173946724864, + 173950918656, + 173952999424, + 174080393800, + 174082490440, + 174086684736, + 174087208960, + 174214619656, + 174215143936, + 174216716296, + 174217240576, + 174348829192, + 174349353472, + 174350925832, + 174351450112, + 174483062856, + 174483070984, + 174485143624, + 174485151752, + 174487257152, + 174487265280, + 174489337920, + 174489346048, + 206159503400, + 206160564304, + 206162665520, + 206163681328, + 206163697696, + 206164754512, + 206164762640, + 206166839368, + 206167883816, + 206167887880, + 206168920136, + 206168952896, + 206426906672, + 206427922472, + 206427922480, + 206428999696, + 206429003792, + 206436302888, + 206436306952, + 206437355528, + 206437388288, + 206695321672, + 206696370184, + 206696374280, + 206697402440, + 206697402448, + 206700552208, + 206700568576, + 206701592656, + 206701600784, + 207232208976, + 207236399152, + 207236399184, + 207237414960, + 207237431328, + 207240581184, + 207240597568, + 207241625632, + 207241629696, + 207500640304, + 207500644368, + 207501656112, + 207501660176, + 207509028896, + 207509032960, + 207510044704, + 207510048768, + 207769047120, + 207769063488, + 207770095632, + 207770112000, + 207773237328, + 207773253696, + 207774285840, + 207774302208, + 208305938472, + 208310132768, + 208310149152, + 208312238144, + 208312246272, + 208314318888, + 208314318920, + 208316399688, + 208316432448, + 208574357544, + 208574390304, + 208576454664, + 208576487424, + 208582737960, + 208582770720, + 208584835080, + 208584867840, + 208842801224, + 208842809352, + 208844881992, + 208844890120, + 208846995520, + 208847003648, + 208849076288, + 208849084416, + 274879226504, + 274879291528, + 274880533776, + 274880663824, + 274894824080, + 274895086208, + 274895741584, + 274896003712, + 274896068736, + 274911532296, + 274912056576, + 274913563912, + 274914088192, + 274914218240, + 274945671952, + 274945679888, + 274947638544, + 274947768592, + 274947776528, + 274961924880, + 274961932816, + 274962194944, + 274962850320, + 274963112448, + 274964021520, + 274964029456, + 274981192960, + 274981323008, + 275012453512, + 275012457480, + 275013436040, + 275013501064, + 275013505032, + 275030213248, + 275030278272, + 275045745800, + 275045749768, + 275046274048, + 275046793352, + 275046797320, + 275047781384, + 275048305664, + 275146482320, + 275147006480, + 275147399816, + 275147399824, + 275149099024, + 275149103120, + 275182653440, + 275281609352, + 275315163272, + 275315167240, + 275316215816, + 275316740096, + 275414848776, + 275415110664, + 275416158216, + 275416162312, + 275416880392, + 275416880400, + 275432939520, + 275483985168, + 275499720720, + 275499982848, + 275500761360, + 275500769296, + 279173530384, + 279173533968, + 279189783184, + 279189783312, + 279190700688, + 279207022848, + 279207088384, + 279324918400, + 279324983424, + 279341240320, + 279341760640, + 279341764608, + 279441441424, + 279441965584, + 279441969168, + 279442358928, + 279475523584, + 279576576640, + 279609610240, + 279610130560, + 279610134528, + 283468170376, + 283468177544, + 283484954752, + 283485020288, + 283501462664, + 283501462792, + 283503494408, + 283552129024, + 283553956096, + 283553964032, + 283570603264, + 283570733312, + 284004779272, + 284005041160, + 284005048328, + 284006810888, + 284021825536, + 284073919744, + 284088868864, + 284090695936, + 284090703872, + 292058305808, + 292058371328, + 292125410064, + 292125410576, + 292141662992, + 292142711312, + 292142973440, + 292192326656, + 292192588800, + 292193374208, + 292210082304, + 292210147328, + 292594652432, + 292594717952, + 292594979840, + 292596027392, + 292612800512, + 292661757200, + 292678533392, + 292679581712, + 292679843840, + 296353268496, + 296353272080, + 296353337600, + 296369521424, + 296370569744, + 296487555072, + 296488079360, + 296504787456, + 296504852480, + 296621703696, + 296621707280, + 296622227984, + 296622231568, + 296755921408, + 296755924992, + 296756445696, + 296756449280, + 296889618704, + 296889684224, + 296890667024, + 296890732544, + 296906391824, + 296906457344, + 296907440144, + 296907505664, + 301184648448, + 301184910336, + 301201424640, + 301201686528, + 301251691776, + 301251953664, + 301268467968, + 301268729856, + 309237916296, + 309238047360, + 309305156096, + 309305418240, + 309307514880, + 309340931072, + 309341061120, + 309372125832, + 309372126344, + 309405418632, + 309407515656, + 309408039936, + 309506089608, + 309506220672, + 309506744832, + 309508841472, + 309542387712, + 309640299144, + 309673853064, + 309675950088, + 309676474368, + 313801179776, + 313801703936, + 313834733696, + 313835257856, + 313935266432, + 313935790592, + 313968820352, + 313969344512, + 317827843208, + 317827850376, + 317827981440, + 317861135496, + 317863232520, + 317895090176, + 317896925184, + 317930341376, + 317930471424, + 318096023688, + 318096154752, + 318098120712, + 318098251776, + 318129569928, + 318129700992, + 318131666952, + 318131798016, + 318364713992, + 318364721160, + 318366549000, + 318366556168, + 318431822848, + 318431830016, + 318433657856, + 318433665024, + 343598506120, + 343599616272, + 343614300304, + 343615217808, + 343615283328, + 343616389392, + 343616397328, + 343631008008, + 343632052360, + 343632056328, + 343633039624, + 343633170688, + 343865958544, + 343866876040, + 343866876048, + 343868051472, + 343868055568, + 343900422280, + 343900426248, + 343901474824, + 343901605888, + 344134324488, + 344135372808, + 344135376904, + 344136356104, + 344136356112, + 344152088592, + 344152154112, + 344153129232, + 344153137168, + 347892486416, + 347909259408, + 347909259536, + 347910176912, + 347910242432, + 347925975296, + 347926040832, + 347927019648, + 347927023616, + 348160917648, + 348160921616, + 348161835152, + 348161839120, + 348194472064, + 348194476032, + 348195389568, + 348195393536, + 348429226256, + 348429291776, + 348430274576, + 348430340096, + 348445999376, + 348446064896, + 348447047696, + 348447113216, + 352187392136, + 352204169344, + 352204234880, + 352206323968, + 352206331904, + 352220938376, + 352220938504, + 352222970120, + 352223101184, + 352455762056, + 352455893120, + 352457859080, + 352457990144, + 352489308296, + 352489439360, + 352491405320, + 352491536384, + 352724254984, + 352724262920, + 352726286600, + 352726294536, + 352741032192, + 352741040128, + 352743063808, + 352743071744, + 412318179848, + 412319486992, + 412384502288, + 412385026576, + 412385288704, + 412386591760, + 412386598928, + 412451345416, + 412452389384, + 412452392968, + 412453180424, + 412453704704, + 412585828880, + 412586353160, + 412586353168, + 412587921424, + 412587925520, + 412720562696, + 412720566280, + 412721614856, + 412722139136, + 412853998600, + 412855046152, + 412855050248, + 412855833608, + 412855833616, + 412921896976, + 412922159104, + 412922938384, + 412922945552, + 429497259024, + 429564363280, + 429564363792, + 429564887568, + 429565149696, + 429631214592, + 429631476736, + 429632258560, + 429632262144, + 429765689872, + 429765693456, + 429766214160, + 429766217744, + 429899907584, + 429899911168, + 429900431872, + 429900435456, + 430033605648, + 430033867776, + 430034653200, + 430034915328, + 430100710416, + 430100972544, + 430101757968, + 430102020096, + 446676869640, + 446743978496, + 446744240640, + 446746330112, + 446746337280, + 446811079176, + 446811079688, + 446812914696, + 446813438976, + 446945042952, + 446945567232, + 446947139592, + 446947663872, + 447079252488, + 447079776768, + 447081349128, + 447081873408, + 447213732872, + 447213740040, + 447215567880, + 447215575048, + 447280841728, + 447280848896, + 447282676736, + 447282683904, + 481305825288, + 481305825296, + 481305829384, + 481305829392, + 481306873864, + 481306873872, + 481306877960, + 481306877968, + 481574260744, + 481574260752, + 481574264840, + 481574264848, + 481575309320, + 481575309328, + 481575313416, + 481575313424, + 549760107680, + 549760631840, + 549764350784, + 549764612672, + 549772985024, + 549773017280, + 549781111616, + 549781373504, + 549781405760, + 549789959456, + 549789974816, + 549793629344, + 549794153504, + 549794168864, + 549823464224, + 549823595264, + 549831328544, + 549831459584, + 549831721472, + 549848220416, + 549848482304, + 549857002784, + 549857018144, + 549857149184, + 549861196832, + 549861212192, + 549864882464, + 549865013504, + 549890327744, + 549890393216, + 549894259904, + 549894325376, + 549894849536, + 549907071680, + 549907103936, + 549907169408, + 549911036096, + 549911101568, + 549915460160, + 549915492416, + 549927847040, + 549928371200, + 550829851840, + 550829981888, + 550833783968, + 550833784000, + 550838353984, + 550838370368, + 550867305632, + 550905462784, + 550934414368, + 550934429728, + 550938624032, + 550938755072, + 551903839008, + 551903904032, + 551908098080, + 551908114464, + 551911703328, + 551911703360, + 551928464192, + 552042332160, + 552058519616, + 552058585088, + 552062681664, + 552062713920, + 554050929472, + 554051453696, + 554067690176, + 554067690304, + 554084942080, + 554085007616, + 554089136128, + 554201776832, + 554205970624, + 554206036096, + 554222813312, + 554223337472, + 556198282048, + 556198806272, + 556198871296, + 556203065344, + 556215042880, + 556337266688, + 556349260352, + 556353454144, + 556353519616, + 558345847968, + 558346110080, + 558362886272, + 558362951808, + 558371340288, + 558379369632, + 558379369760, + 558438154496, + 558438416384, + 558446413088, + 558454800672, + 558454931712, + 559419524256, + 559419786368, + 559419916416, + 559428304896, + 559453045920, + 559495380992, + 559520154656, + 559528542240, + 559528673280, + 566936274208, + 566936306720, + 567003317024, + 567003317536, + 567011181344, + 567027958528, + 567028220416, + 567070262272, + 567070524416, + 567087038464, + 567095329280, + 567095361536, + 569083691808, + 569083756832, + 569083789344, + 569091556128, + 569108333312, + 569218007040, + 569234259968, + 569242550784, + 569242583040, + 573378659072, + 573378724096, + 573394912000, + 573394977024, + 573512876544, + 573512941568, + 573529129472, + 573529194496, + 575525684512, + 575525717024, + 575525979136, + 575542755328, + 575551078400, + 575592727840, + 575601115424, + 575617892608, + 575618154496, + 576599393312, + 576599655424, + 576607780896, + 576608043008, + 576666469408, + 576666731520, + 576674856992, + 576675119104, + 577673167136, + 577673199648, + 577681490208, + 577681522720, + 577689944320, + 577689976832, + 577698267392, + 577698299904, + 584115946176, + 584115962432, + 584183071232, + 584183333376, + 584216887296, + 584220935168, + 584220950528, + 584250032832, + 584250033344, + 584253965504, + 584287519872, + 584288044032, + 585189557440, + 585189687488, + 585189703744, + 585193489600, + 585227043968, + 585256812544, + 585290104832, + 585294152704, + 585294168064, + 588410651328, + 588410667584, + 588411191808, + 588444745728, + 588448808960, + 588544737984, + 588548931776, + 588582486144, + 588583010304, + 589484392640, + 589484408896, + 589488455872, + 589488472128, + 589517947008, + 589517963264, + 589522010240, + 589522026496, + 590558020160, + 590558544384, + 590562213952, + 590562738176, + 590692221504, + 590692745728, + 590696415296, + 590696939520, + 593779491968, + 593779622016, + 593812784256, + 593812914304, + 593846600704, + 593846730752, + 593879892992, + 593880023040, + 618479583392, + 618483827008, + 618492231872, + 618496295104, + 618496360576, + 618500587840, + 618500620352, + 618508927264, + 618513105056, + 618513121312, + 618517250336, + 618517381376, + 619549196480, + 619553259680, + 619553259712, + 619557568576, + 619557584960, + 619586781344, + 619586797600, + 619590991904, + 619591122944, + 620622856480, + 620627050528, + 620627066912, + 620631179552, + 620631179584, + 620643778624, + 620643844096, + 620647940416, + 620647972928, + 622770405696, + 622787166400, + 622787166528, + 622791229632, + 622791295104, + 622803894528, + 622803960064, + 622808072320, + 622808088576, + 623844131008, + 623844147264, + 623848194240, + 623848210496, + 623877685376, + 623877701632, + 623881748608, + 623881764864, + 624917758272, + 624917823744, + 624921952320, + 624922017792, + 624934519104, + 624934584576, + 624938713152, + 624938778624, + 627065323680, + 627082100864, + 627082166400, + 627090522368, + 627090554880, + 627098845344, + 627098845472, + 627107168544, + 627107299584, + 628138999968, + 628139131008, + 628147388448, + 628147519488, + 628172521632, + 628172652672, + 628180910112, + 628181041152, + 629212774688, + 629212807200, + 629221097760, + 629221130272, + 629229551872, + 629229584384, + 629237874944, + 629237907456, + 687199519776, + 687203435072, + 687262417440, + 687266595872, + 687266611232, + 687270281760, + 687270543872, + 687329281088, + 687333213248, + 687333737472, + 687337636416, + 687337668672, + 688268805184, + 688272737312, + 688272737344, + 688277176384, + 688277192768, + 688339813408, + 688339828768, + 688344023072, + 688344285184, + 689342792224, + 689346986016, + 689347002400, + 689350656544, + 689350656576, + 689480695872, + 689481220096, + 689484857920, + 689484890176, + 704375194656, + 704442270240, + 704442270752, + 704450134560, + 704450396672, + 704509150208, + 704509412352, + 704517505536, + 704517537792, + 705448412192, + 705448674304, + 705456799776, + 705457061888, + 705515488288, + 705515750400, + 705523875872, + 705524137984, + 706522645024, + 706522677280, + 706530509344, + 706530541600, + 706656862720, + 706656894976, + 706664727040, + 706664759296, + 721554784832, + 721621893632, + 721622155776, + 721626334208, + 721626349568, + 721688986176, + 721688986688, + 721692918848, + 721693443072, + 722628510784, + 722628526144, + 722632442944, + 722632458304, + 722695619584, + 722695634944, + 722699551744, + 722699567104, + 723702006336, + 723702530560, + 723706200128, + 723706724352, + 723836207680, + 723836731904, + 723840401472, + 723840925696, + 756992196640, + 756992196672, + 756992213024, + 756992213056, + 756996390944, + 756996390976, + 756996407328, + 756996407360, + 758065938464, + 758065938496, + 758065954848, + 758065954880, + 758070132768, + 758070132800, + 758070149152, + 758070149184, + 824650891904, + 824667866368, + 824701485824, + 824717738752, + 824718000640, + 824734909696, + 824735039744, + 824768267392, + 824784978560, + 824785043584, + 824801559680, + 824802083840, + 828929344256, + 828945597056, + 828945597184, + 828962832640, + 828962898176, + 829079683712, + 829079748736, + 829096525952, + 829097050112, + 833223984256, + 833240760448, + 833240825984, + 833257276544, + 833257276672, + 833307672832, + 833307934720, + 833324320000, + 833324450048, + 841814181120, + 841881223936, + 841881224448, + 841897476864, + 841897738752, + 841948136448, + 841948398592, + 841964847616, + 841964912640, + 846109082368, + 846109147392, + 846125335296, + 846125400320, + 846243299840, + 846243364864, + 846259552768, + 846259617792, + 850403591424, + 850403853312, + 850420367616, + 850420629504, + 850470634752, + 850470896640, + 850487410944, + 850487672832, + 858993853056, + 859060961792, + 859061223936, + 859094647808, + 859094777856, + 859127939712, + 859127940224, + 859161232512, + 859161756672, + 863288558208, + 863289082368, + 863322112128, + 863322636288, + 863422644864, + 863423169024, + 863456198784, + 863456722944, + 867583657088, + 867583787136, + 867616949376, + 867617079424, + 867650765824, + 867650895872, + 867684058112, + 867684188160, + 897665007744, + 897665007872, + 897665073280, + 897665073408, + 897681784960, + 897681785088, + 897681850496, + 897681850624, + 901959975040, + 901959975168, + 901960040576, + 901960040704, + 901976752256, + 901976752384, + 901976817792, + 901976817920, + 979319915008, + 979319915520, + 979320177152, + 979320177664, + 979387023872, + 979387024384, + 979387286016, + 979387286528, + 996499784192, + 996499784704, + 996500046336, + 996500046848, + 996566893056, + 996566893568, + 996567155200, + 996567155712 + ], + "objective": "22", + "pair_census": [ + [ + 0, + 0, + 0, + 2057 + ], + [ + 0, + 112, + 1, + 5940 + ], + [ + 0, + 224, + 1, + 8640 + ], + [ + 0, + 224, + 2, + 3240 + ], + [ + 0, + 245, + 1, + 8640 + ], + [ + 0, + 336, + 2, + 12960 + ], + [ + 0, + 357, + 1, + 8640 + ], + [ + 0, + 392, + 1, + 1080 + ], + [ + 0, + 448, + 2, + 5400 + ], + [ + 0, + 469, + 2, + 8640 + ], + [ + 0, + 490, + 1, + 2880 + ], + [ + 0, + 490, + 2, + 12960 + ], + [ + 0, + 548, + 1, + 1440 + ], + [ + 0, + 602, + 2, + 25920 + ], + [ + 0, + 688, + 2, + 1080 + ], + [ + 0, + 714, + 2, + 30240 + ], + [ + 0, + 784, + 2, + 4320 + ], + [ + 0, + 793, + 2, + 8640 + ], + [ + 0, + 904, + 1, + 360 + ], + [ + 0, + 933, + 2, + 8640 + ], + [ + 0, + 1150, + 3, + 12960 + ], + [ + 0, + 1178, + 2, + 4320 + ], + [ + 0, + 1290, + 3, + 12960 + ], + [ + 1, + 504, + 1, + 5960 + ], + [ + 1, + 616, + 2, + 6480 + ], + [ + 1, + 749, + 2, + 8640 + ], + [ + 1, + 828, + 2, + 4320 + ], + [ + 1, + 861, + 2, + 8640 + ], + [ + 1, + 896, + 2, + 4320 + ], + [ + 1, + 1052, + 2, + 2880 + ], + [ + 1, + 1073, + 2, + 8640 + ], + [ + 1, + 1163, + 2, + 2880 + ], + [ + 1, + 1185, + 3, + 8640 + ], + [ + 1, + 1297, + 3, + 8640 + ], + [ + 1, + 1318, + 3, + 4320 + ], + [ + 1, + 1408, + 2, + 1440 + ], + [ + 1, + 1430, + 3, + 8640 + ], + [ + 1, + 1555, + 3, + 8640 + ], + [ + 2, + 1008, + 2, + 3120 + ], + [ + 2, + 1332, + 3, + 1440 + ], + [ + 2, + 1556, + 3, + 1440 + ], + [ + 2, + 1667, + 3, + 2880 + ], + [ + 2, + 1872, + 2, + 240 + ], + [ + 4, + 1408, + 2, + 1260 + ], + [ + 4, + 1520, + 3, + 540 + ], + [ + 4, + 1800, + 3, + 1080 + ], + [ + 4, + 1984, + 3, + 540 + ], + [ + 5, + 1912, + 3, + 720 + ], + [ + 12, + 2376, + 3, + 80 + ], + [ + 40, + 2880, + 4, + 1 + ] + ], + "singleton_weight": "1/40" + }, + "scope": "Scalar F2 totals; whole Eisenstein lines; abstract pairing-rank charge; no new kappa.", + "sharp_example": { + "flat_indices": [ + 591, + 566 + ], + "joint_maximum_clique_hits": 1872, + "left": [ + 9, + 11, + 13, + 14, + 17, + 20, + 23, + 24, + 28, + 31, + 32, + 36 + ], + "pairing_rank": 2, + "right": [ + 0, + 1, + 2, + 9, + 10, + 11, + 18, + 19, + 26, + 27, + 34, + 35 + ], + "support_ranks": [ + 3, + 3 + ] + }, + "source_sha256": { + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/algebra_lines.py": "bc4037049debf9b7affeb7e6b30da0193dea8c3850a7317afd045ac7ac481108", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", + "research/format-limits-corrected/README.md": "1bcd80c1cd61fddae9f3a7f00fc9d1c796410408251e576600e94c19b16b1e5e" + }, + "status": "PASS_EISENSTEIN_CLIQUE_COPY_BOUND" +} diff --git a/research/eisenstein-clique-copy-bound/crosscheck.py b/research/eisenstein-clique-copy-bound/crosscheck.py new file mode 100644 index 0000000000..7a8fe199a5 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/crosscheck.py @@ -0,0 +1,96 @@ +#!/usr/bin/env python3 +"""Independent arithmetic cross-check of the replayed certificate. + +No geometry/verifier code is imported. Integer root generators are used +directly. Modular ranks LOWER-bound rational ranks for the primal check; +Fraction elimination certifies exact costs for the dual. Run verify.py too: +it supplies the geometry, enumeration completeness, and full receipt binding. + +Jonathan Lam, with substantial OpenAI Codex assistance; Apache-2.0. +""" + +from fractions import Fraction +import json +from pathlib import Path + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def rank(rows, prime=None): + if not rows: + return 0 + matrix = [[x % prime for x in row] if prime else list(map(Fraction, row)) + for row in rows] + result = 0 + for column in range(len(matrix[0])): + pivot = next((i for i in range(result, len(matrix)) if matrix[i][column]), None) + if pivot is None: + continue + matrix[result], matrix[pivot] = matrix[pivot], matrix[result] + inverse = (pow(matrix[result][column], prime - 2, prime) + if prime else 1 / matrix[result][column]) + matrix[result] = [(x * inverse) % prime if prime else x * inverse + for x in matrix[result]] + for i in range(result + 1, len(matrix)): + coefficient = matrix[i][column] + matrix[i] = [(x - coefficient * y) % prime if prime else x - coefficient * y + for x, y in zip(matrix[i], matrix[result])] + result += 1 + if result == len(matrix): + break + return result + + +def main(): + certificate = json.loads(Path(__file__).with_name('certificate.json').read_text()) + roots = certificate['geometry']['representatives'] + images = certificate['geometry']['J_images'] + flats = certificate['geometry']['flats'] + cliques = certificate['primal']['maximum_cliques'] + bases = [[vector for i in flat['generators'] for vector in (roots[i], images[i])] + for flat in flats] + check(len(flats) == 772, 'flat count') + for basis, flat in zip(bases, flats): + check(rank(basis, 101) == 2 * flat['rank'], 'modular generator rank') + adjacent = [sum(1 << k for k in range(40) if i != k and + (dot(roots[i], roots[k]) or dot(roots[i], images[k]))) + for i in range(40)] + check(adjacent == certificate['geometry']['nonorthogonality_masks'], 'adjacency') + check(len(cliques) == len(set(cliques)) == 2880, 'clique count') + for clique in cliques: + check(clique.bit_count() == 7 and all(not ((clique ^ (1 << i)) & ~adjacent[i]) + for i in range(40) if clique >> i & 1), 'clique admission') + hits = [sum(1 << i for i, clique in enumerate(cliques) if clique & flat['mask']) + for flat in flats] + count = 0 + for i, (basis, flat) in enumerate(zip(bases, flats)): + for k in range(i + 1): + gram = [[dot(x, y) for y in bases[k]] for x in basis] + # Integer minors nonzero mod 101 are nonzero over Q. No equality + # of the two ranks is assumed or needed in this inequality. + modular_rank = rank(gram, 101) + lhs = (24 * (flat['mask'] & flats[k]['mask']).bit_count() + + (hits[i] & hits[k]).bit_count()) + check(2 * lhs <= 960 * modular_rank, 'modular primal bound') + count += 1 + check(count == 298378, 'complete primal pair count') + lookup = {flat['mask']: basis for flat, basis in zip(flats, bases)} + dual = certificate['dual']['flat_pairs'] + check(len(dual) == 240, 'dual count') + for left, right in dual: + check(rank([[dot(x, y) for y in lookup[right]] for x in lookup[left]]) == 4, + 'exact dual pair cost') + full = lookup[(1 << 40) - 1] + check(rank([[dot(x, y) for y in full] for x in full]) == 8, 'exact full-pair cost') + print('PASS_EISENSTEIN_CROSSCHECK: 298378 modular primal bounds; 241 exact dual costs') + + +if __name__ == '__main__': + main() diff --git a/research/eisenstein-clique-copy-bound/geometry.py b/research/eisenstein-clique-copy-bound/geometry.py new file mode 100644 index 0000000000..a92c16295d --- /dev/null +++ b/research/eisenstein-clique-copy-bound/geometry.py @@ -0,0 +1,209 @@ +"""Exact rational geometry for the 40 Eisenstein E8 lines (standard library). + +Jonathan Lam, with substantial OpenAI Codex assistance; Apache-2.0. +The order-three construction is credited to GamingPuzzled's PR620. +No predecessor implementation is imported or executed. +""" + +from itertools import combinations, product +from math import gcd +from functools import reduce + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def primitive(row): + d = reduce(gcd, row, 0) + if not d: + return tuple(row) + first = next(x for x in row if x) + if first < 0: + d = -d + return tuple(x // d for x in row) + + +def echelon(rows): + """Canonical integer-scaled RREF; only exact integer operations.""" + pivots = {} + for row in rows: + row = primitive(row) + for p, b in sorted(pivots.items()): + if row[p]: + row = primitive(tuple(b[p] * x - row[p] * y + for x, y in zip(row, b))) + if any(row): + pivots[next(i for i, x in enumerate(row) if x)] = row + for p in sorted(pivots, reverse=True): + b = pivots[p] + for q in sorted(pivots): + if q < p and pivots[q][p]: + row = pivots[q] + pivots[q] = primitive(tuple(b[p] * x - row[p] * y + for x, y in zip(row, b))) + return tuple(pivots[p] for p in sorted(pivots)) + + +def contains(basis, row): + for b in basis: + p = next(i for i, x in enumerate(b) if x) + if row[p]: + row = primitive(tuple(b[p] * x - row[p] * y + for x, y in zip(row, b))) + return not any(row) + + +def roots(): + """PR620's standard root-line order, followed by the negatives.""" + candidates = [] + for i, j in combinations(range(8), 2): + for a, b in product((2, -2), repeat=2): + row = [0] * 8 + row[i], row[j] = a, b + candidates.append(tuple(row)) + candidates += [s for s in product((1, -1), repeat=8) + if s.count(-1) % 2 == 0] + lines, seen = [], set() + for r in candidates: + if r not in seen and tuple(-x for x in r) not in seen: + seen.add(r) + lines.append(r) + return lines + [tuple(-x for x in r) for r in lines] + + +def reflection(row, root): + # Roots have squared norm eight: s_a(x) = x - a/4. + numerator = tuple(4 * x - dot(row, root) * a + for x, a in zip(row, root)) + require(all(x % 4 == 0 for x in numerator), 'nonintegral root reflection') + return tuple(x // 4 for x in numerator) + + +def geometry(): + rr = roots() + require(len(rr) == len(set(rr)) == 240, 'root count') + require(all(dot(r, r) == 8 for r in rr), 'root norm') + pairs = [] + for a in rr: + if len(pairs) == 4: + break + if any(dot(a, x) for pair in pairs for x in pair): + continue + for b in rr: + if dot(a, b) == -4 and not any(dot(b, x) for pair in pairs for x in pair): + pairs.append((a, b)) + break + require(len(pairs) == 4, 'four orthogonal A2 planes') + + def rotate(row): + # The four plane actions commute; s_a s_b acts rightmost first. + for a, b in reversed(pairs): + row = reflection(reflection(row, b), a) + return row + + rotated = {r: rotate(r) for r in rr} + require(set(rotated.values()) == set(rr), 'root permutation') + require(all(rotated[rotated[rotated[r]]] == r for r in rr), 'order three') + require(all(all(x + y + z == 0 for x, y, z in zip(r, rotated[r], rotated[rotated[r]])) + for r in rr), 'J squared plus J plus I') + require(all(dot(r, s) == dot(rotated[r], rotated[s]) for r in rr for s in rr), + 'orthogonal action') + seen, reps, images, orbits = set(), [], [], [] + for r in rr: + if r in seen: + continue + orbit = {r, rotated[r], rotated[rotated[r]]} + orbit |= {tuple(-x for x in t) for t in tuple(orbit)} + basis = echelon((r, rotated[r])) + require(len(basis) == 2, 'line rational rank') + require(orbit == {s for s in rr if contains(basis, s)}, 'line orbit completeness') + require(len(orbit) == 6 and not (orbit & seen), 'six-root partition') + seen |= orbit + reps.append(r) + images.append(rotated[r]) + orbits.append(sorted(orbit)) + require(len(reps) == 40, 'Eisenstein line count') + adjacent = [] + for i, r in enumerate(reps): + mask = sum(1 << j for j, s in enumerate(reps) + if j != i and (dot(r, s) or dot(r, images[j]))) + adjacent.append(mask) + require(all(m.bit_count() == 27 for m in adjacent), 'nonorthogonal degree') + return reps, images, adjacent, pairs, orbits + + +def bits(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def maximal_cliques(adjacent): + """Bron--Kerbosch with a deterministic pivot; all maximal cliques.""" + out = [] + + def visit(chosen, possible, excluded): + if not (possible | excluded): + out.append(chosen) + return + pivot = max(bits(possible | excluded), + key=lambda i: (possible & adjacent[i]).bit_count()) + for i in list(bits(possible & ~adjacent[pivot])): + bit = 1 << i + visit(chosen | bit, possible & adjacent[i], excluded & adjacent[i]) + possible ^= bit + excluded |= bit + + visit(0, (1 << len(adjacent)) - 1, 0) + return sorted(out) + + +def all_cliques(adjacent): + """Every nonempty clique exactly once, by increasing vertex order.""" + result = [] + + def extend(chosen, possible): + while possible: + bit = possible & -possible + possible ^= bit + i = bit.bit_length() - 1 + result.append(chosen | bit) + extend(chosen | bit, possible & adjacent[i]) + + extend(0, (1 << len(adjacent)) - 1) + return sorted(result) + + +def flats(reps, images): + """Generate every line-spanned flat, by adjoining a line to each rank.""" + all_flats = [(0, (), ())] + level = {(): ()} + for degree in range(1, 5): + new = {} + for basis, generators in level.items(): + for i, r in enumerate(reps): + if not contains(basis, r): + enlarged = echelon(basis + (r, images[i])) + require(len(enlarged) == 2 * degree, 'flat rank increment') + new.setdefault(enlarged, generators + (i,)) + for basis, generators in new.items(): + mask = sum(1 << i for i, r in enumerate(reps) if contains(basis, r)) + require(all(contains(basis, images[i]) for i in bits(mask)), 'J-invariant flat') + all_flats.append((mask, basis, generators)) + level = new + require(len(level) == 1, 'one full flat') + require(len({m for m, _, _ in all_flats}) == len(all_flats), 'distinct flat closures') + return sorted(all_flats, key=lambda f: (len(f[1]), f[0])) + + +def pairing_rank(basis_a, basis_b): + rank = len(echelon(tuple(tuple(dot(a, b) for b in basis_b) for a in basis_a))) + require(rank % 2 == 0, 'odd rational pairing rank') + return rank // 2 diff --git a/research/eisenstein-clique-copy-bound/test_verify.py b/research/eisenstein-clique-copy-bound/test_verify.py new file mode 100644 index 0000000000..bf836571e5 --- /dev/null +++ b/research/eisenstein-clique-copy-bound/test_verify.py @@ -0,0 +1,69 @@ +"""Portable replay and rejection tests; standard-library unittest. + +Jonathan Lam, with substantial OpenAI Codex assistance; Apache-2.0. +""" + +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RELATIVE = HERE.relative_to(ROOT) + + +class ReplayPackagingTests(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory(prefix='eisenstein-replay-test-') + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) / 'minimal-checkout' + self.package = self.root / RELATIVE + shutil.copytree(HERE, self.package, ignore=shutil.ignore_patterns('__pycache__')) + self.inputs = json.loads((HERE / 'SOURCES.json').read_text())['local_inputs'] + for item in self.inputs: + target = self.root / item['path'] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / item['path'], target) + self.output = Path(self.temporary.name) / 'receipt.json' + self.output.write_text('preserve this output on failure\n') + + def run_replay(self): + return subprocess.run( + [sys.executable, '-O', '-B', str(self.package / 'verify.py'), + '--write', str(self.output)], + cwd=self.temporary.name, text=True, capture_output=True, timeout=180, + check=False) + + def test_relocated_optimized_replay_and_export(self): + result = self.run_replay() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('clique-method optimum 22', result.stdout) + self.assertEqual(json.loads(self.output.read_text()), + json.loads((HERE / 'certificate.json').read_text())) + self.assertFalse(list(self.root.rglob('__pycache__'))) + + def test_corrupt_certificate_rejected_before_export(self): + path = self.package / 'certificate.json' + data = json.loads(path.read_text()) + data['dual']['flat_pairs'].pop() + path.write_text(json.dumps(data)) + result = self.run_replay() + self.assertNotEqual(result.returncode, 0) + self.assertIn('committed certificate differs', result.stderr) + self.assertEqual(self.output.read_text(), 'preserve this output on failure\n') + + def test_changed_source_rejected_before_export(self): + path = self.root / self.inputs[0]['path'] + path.write_bytes(path.read_bytes() + b'\n# tampered source\n') + result = self.run_replay() + self.assertNotEqual(result.returncode, 0) + self.assertIn('source hash mismatch', result.stderr) + self.assertEqual(self.output.read_text(), 'preserve this output on failure\n') + + +if __name__ == '__main__': + unittest.main() diff --git a/research/eisenstein-clique-copy-bound/verify.py b/research/eisenstein-clique-copy-bound/verify.py new file mode 100644 index 0000000000..1dd6647c6b --- /dev/null +++ b/research/eisenstein-clique-copy-bound/verify.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""Replay an exact primal/dual clique certificate, with no solver dependency. + +Jonathan Lam, with substantial OpenAI Codex assistance; Apache-2.0. +""" + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import random + +from geometry import (all_cliques, bits, contains, dot, echelon, flats, + geometry, maximal_cliques, pairing_rank, require) + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def digest(value): + data = json.dumps(value, separators=(',', ':'), sort_keys=True).encode() + return hashlib.sha256(data).hexdigest() + + +def fraction_rank(rows): + """Independent ordinary Gaussian elimination over Fraction.""" + matrix = [list(map(Fraction, row)) for row in rows] + if not matrix: + return 0 + rank = 0 + for column in range(len(matrix[0])): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][column]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + q = matrix[rank][column] + matrix[rank] = [x / q for x in matrix[rank]] + for i in range(rank + 1, len(matrix)): + q = matrix[i][column] + matrix[i] = [x - q * y for x, y in zip(matrix[i], matrix[rank])] + rank += 1 + if rank == len(matrix): + break + return rank + + +def check_sources(): + source = json.loads((HERE / 'SOURCES.json').read_text()) + for item in source['local_inputs']: + actual = hashlib.sha256((ROOT / item['path']).read_bytes()).hexdigest() + require(actual == item['sha256'], 'source hash mismatch: ' + item['path']) + return {item['path']: item['sha256'] for item in source['local_inputs']} + + +def check_clique(mask, adjacent): + require(0 < mask < (1 << len(adjacent)), 'invalid clique mask') + require(all((mask ^ (1 << i)) & ~adjacent[i] == 0 for i in bits(mask)), + 'orthogonal pair in claimed clique') + + +def check_fitting(rectangles, adjacent): + rows = [0] * len(adjacent) + limit = (1 << len(adjacent)) - 1 + for readers, sources in rectangles: + require(readers >= 0 and sources >= 0 and not ((readers | sources) & ~limit), + 'invalid rectangle support') + for i in bits(readers): + rows[i] ^= sources + require(all(row & (1 << i) for i, row in enumerate(rows)), 'missing fitting diagonal') + require(all(not (row & adjacent[i]) for i, row in enumerate(rows)), + 'forbidden nonorthogonal entry') + return rows + + +def require_rejected(label, function): + try: + function() + except ValueError: + return label + raise ValueError('negative control accepted: ' + label) + + +def replay(): + source_hashes = check_sources() + reps, images, adjacent, a2_pairs, orbits = geometry() + every_clique = all_cliques(adjacent) + maximal = maximal_cliques(adjacent) + largest = [q for q in every_clique if q.bit_count() == 7] + require(max(q.bit_count() for q in every_clique) == 7, 'maximum clique size') + require(largest == [q for q in maximal if q.bit_count() == 7], + 'independent maximum-clique enumerations disagree') + require(len(every_clique) == len(set(every_clique)), 'duplicate clique') + for q in every_clique: + check_clique(q, adjacent) + ff = flats(reps, images) + require(len(ff) == 772 and len(largest) == 2880, 'geometry census') + hits = [sum(1 << i for i, q in enumerate(largest) if mask & q) + for mask, _, _ in ff] + + # All unordered pairs, INCLUDING empty supports, are checked exactly. + # Symmetry of the Gram pairing covers the reversed order. + pair_census = Counter() + dual_pairs = [] + sharp_pair = None + pair_count = 0 + for i, (left, bleft, _) in enumerate(ff): + for k in range(i + 1): + right, bright, _ = ff[k] + cost = pairing_rank(bleft, bright) + h7 = (hits[i] & hits[k]).bit_count() + h1 = (left & right).bit_count() + require(24 * h1 + h7 <= 960 * cost, 'primal clique inequality') + pair_census[(h1, h7, cost)] += 1 + pair_count += 1 + if (len(bleft) == len(bright) == 6 + and left.bit_count() == right.bit_count() == 12 and cost == 2): + dual_pairs.append((left, right)) + require((h1, h7) == (2, 1872), 'dual-pair incidence') + if sharp_pair is None: + sharp_pair = (i, k) + require(pair_count == len(ff) * (len(ff) + 1) // 2, 'complete flat pairs') + require(len(dual_pairs) == 240, 'dual-pair census') + require(len(set(dual_pairs)) == 240, 'duplicate dual pair') + + # This dual is checked on EVERY literal clique, not merely on orbit + # representatives or averages. Thus arbitrary nonuniform weights are covered. + dual_census = Counter() + for q in every_clique: + hit_count = sum(bool(q & left) and bool(q & right) for left, right in dual_pairs) + require(hit_count + 12 >= 24 * q.bit_count(), 'dual clique inequality') + dual_census[(q.bit_count(), hit_count)] += 1 + primal = Fraction(40, 40) + Fraction(len(largest) * 7, 960) + dual = Fraction(len(dual_pairs) * 2, 24) + Fraction(4, 2) + require(primal == dual == 22, 'exact primal-dual equality') + + # Independent rank controls use original root generators, not RREF rows. + rng = random.Random(48) + rank_pairs = set((rng.randrange(len(ff)), rng.randrange(len(ff))) for _ in range(256)) + rank_pairs.add(sharp_pair) + rank_pairs.add((0, len(ff) - 1)) + rank_pairs.add((len(ff) - 1, len(ff) - 1)) + for i, k in sorted(rank_pairs): + aa = [v for n in ff[i][2] for v in (reps[n], images[n])] + bb = [v for n in ff[k][2] for v in (reps[n], images[n])] + gram = [[dot(x, y) for y in bb] for x in aa] + require(fraction_rank(gram) == 2 * pairing_rank(ff[i][1], ff[k][1]), + 'independent Fraction Gram rank disagreement') + # Another completeness check closes every possible one-line extension. + flat_keys = {b for _, b, _ in ff} + for mask, basis, _ in ff: + for i in range(40): + require(echelon(basis + (reps[i], images[i])) in flat_keys, + 'missing one-line flat extension') + + identity = [(1 << i, 1 << i) for i in range(40)] + check_fitting(identity, adjacent) + directed = [] + for i in range(40): + sources = (1 << i) | sum(1 << k for k in range(40) + if k != i and not (adjacent[i] >> k) & 1 and rng.randrange(2)) + directed.append((1 << i, sources)) + rows = check_fitting(directed, adjacent) + require(any(bool(rows[i] & (1 << k)) != bool(rows[k] & (1 << i)) + for i in range(40) for k in range(40)), 'asymmetric positive control') + costs = [] + for readers, sources in directed: + aa = echelon(tuple(v for n in bits(readers) for v in (reps[n], images[n]))) + bb = echelon(tuple(v for n in bits(sources) for v in (reps[n], images[n]))) + costs.append(pairing_rank(aa, bb)) + require(costs == [1] * 40, 'cost-40 directed row decomposition') + + i, k = sharp_pair + left, bl, _ = ff[i] + right, br, _ = ff[k] + h1 = (left & right).bit_count() + h7 = (hits[i] & hits[k]).bit_count() + orthogonal = next((i, k) for i in range(40) for k in range(i) + if not (adjacent[i] >> k) & 1) + nonorthogonal = next(bits(adjacent[0])) + controls = [] + controls.append(require_rejected('nonclique_orthogonal_pair', + lambda: check_clique(sum(1 << n for n in orthogonal), adjacent))) + controls.append(require_rejected('missing_decoder_diagonal', + lambda: check_fitting(identity[1:], adjacent))) + controls.append(require_rejected('forbidden_decoder_entry', + lambda: check_fitting(identity + [(1, 1 << nonorthogonal)], adjacent))) + controls.append(require_rejected('increased_maximum_clique_weight', + lambda: require(Fraction(h1, 40) + Fraction(h7, 959) <= 2, 'invalid weight'))) + controls.append(require_rejected('source_dimension_substituted_for_pairing_rank', + lambda: require(pairing_rank(bl, br) == len(bl) // 2, 'rank-three supports pair at rank two'))) + controls.append(require_rejected('missing_eisenstein_direction', + lambda: pairing_rank((reps[8],), (reps[8],)))) + # Each singleton hits both flats in exactly twelve dual pairs. + singleton = 1 << 8 # assignment seed 48 modulo 40 + single_hits = sum(bool(singleton & x) and bool(singleton & y) for x, y in dual_pairs) + require(single_hits == 12, 'singleton dual saturation') + controls.append(require_rejected('underweighted_dual', + lambda: require(Fraction(1, 2) + Fraction(single_hits, 25) >= 1, 'dual weight too small'))) + reduced = list(dual_pairs) + reduced.remove(next((x, y) for x, y in reduced if singleton & x and singleton & y)) + controls.append(require_rejected('omitted_dual_flat_pair', + lambda: require(12 + sum(bool(singleton & x) and bool(singleton & y) for x, y in reduced) + >= 24, 'incomplete dual coverage'))) + + return { + 'status': 'PASS_EISENSTEIN_CLIQUE_COPY_BOUND', + 'base_commit': '66849e1475c930fd7732b1a0067ffee7e1e95f60', + 'assignment_seed': 48, + 'source_sha256': source_hashes, + 'scope': 'Scalar F2 totals; whole Eisenstein lines; abstract pairing-rank charge; no new kappa.', + 'geometry': { + 'a2_pairs': a2_pairs, 'representatives': reps, 'J_images': images, + 'root_orbits_sha256': digest(orbits), + 'nonorthogonality_masks': adjacent, + 'flat_census': [[rank, size, n] for (rank, size), n in sorted(Counter( + (len(b) // 2, m.bit_count()) for m, b, _ in ff).items())], + 'flats': [{'mask': m, 'rank': len(b) // 2, 'generators': g} for m, b, g in ff], + 'clique_census': sorted(Counter(q.bit_count() for q in every_clique).items()), + 'all_cliques_sha256': digest(every_clique), + 'maximal_clique_census': sorted(Counter(q.bit_count() for q in maximal).items()), + }, + 'primal': {'singleton_weight': '1/40', 'maximum_clique_weight': '1/960', + 'maximum_cliques': largest, 'objective': str(primal), + 'flat_pairs_checked': pair_count, + 'pair_census': [list(key) + [n] for key, n in sorted(pair_census.items())]}, + 'dual': {'pair_weight': '1/24', 'full_pair_weight': '1/2', 'flat_pairs': dual_pairs, + 'objective': str(dual), 'cliques_checked': len(every_clique), + 'clique_hit_census': [list(key) + [n] for key, n in sorted(dual_census.items())]}, + 'sharp_example': {'flat_indices': sharp_pair, 'left': list(bits(left)), 'right': list(bits(right)), + 'support_ranks': [3, 3], 'pairing_rank': 2, 'joint_maximum_clique_hits': h7}, + 'abstract_decoder_cost_interval': [22, 40], + 'all_clique_weight_certificate_optimum': '22', + 'optimistic_Dfc': {'rational_copy_floor': 44, 'upper_deficit_per_replica': '36*s-80', + 'three_stage_upper_deficit': 28, + 'conclusion': 'Does not exclude three or more stages; no achieved supplier.'}, + 'independent_fraction_pairs': len(rank_pairs), + 'one_line_extensions_checked': len(ff) * 40, + 'asymmetric_positive_control_sha256': digest(directed), + 'negative_controls': controls, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='Export the receipt AFTER checking the committed certificate.') + args = parser.parse_args() + result = replay() + # Round-trip tuples so semantic JSON equality is independent of whitespace. + result = json.loads(json.dumps(result)) + expected = json.loads((HERE / 'certificate.json').read_text()) + require(result == expected, 'committed certificate differs from exact replay') + if args.write: + require(args.write.resolve() != (HERE / 'certificate.json').resolve(), + 'refusing to overwrite the committed certificate') + args.write.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print('PASS_EISENSTEIN_CLIQUE_COPY_BOUND: cost >= 22; clique-method optimum 22; ' + f"{result['primal']['flat_pairs_checked']} flat pairs; " + f"{result['dual']['cliques_checked']} cliques; {len(result['negative_controls'])} negative controls; no new kappa") + + +if __name__ == '__main__': + main()