Mister-Meeseeks · Oct 16, 2026 · Oct 15, 2026
diff --git a/research/punctured-e8-48-56/LICENSE b/research/punctured-e8-48-56/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/punctured-e8-48-56/MANIFEST.sha256 b/research/punctured-e8-48-56/MANIFEST.sha256
@@ -0,0 +1,65 @@
+c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4  LICENSE
+275cf58a48222108e0250623534c6aaedeeee7b36a69ac89d320598e775afcab  NOTICE.md
+5a53633afff65a2e571ffc410a714dd22b6e98f4b1156835deded17bf991fd83  README.md
+8340eaa1a1735b3db4f4483da693495f668f3e41875b0270c90850ff944a417f  SOURCES.json
+183f938fb1e935dca151122478e43b0d1dd9ce792ca9c1de3703e8aea0cf98ba  checks/c1_tallies.py
+8dc01d1407a4f533c87a7c007e6f9d0c1afd379bf3f469cd4923acfaf8f55a42  checks/c2_encoding.py
+d1aa8ce3c0948f4cc92dfc13bbc5d8330a506d23a717511d6255a4d5e89a0024  checks/c3_cover.py
+4bed464e50ccc5d0baa8ad6cca6df64a3a258e955708fab8c3d2fab74f11dc36  data/logs/opts_build.txt
+3686489ed0c3a9f88795d563ecf0089af84c9dca9eaaf6721053a2fcde005ca3  data/states/T0_P53_k6.json
+31425ff8e85e6ea884d8d3718396cc6ca448fabcc71d63b0f812f41df3229739  data/states/T0_P56_k17.json
+36636713fad00617919d331d1d5be6d6448e291118e06327f4baf9ef1c73a93a  data/states/T1_P53_k6.json
+b11a35b6b8b01bc2fe55a97744a0d828019467286badff53ff1a015564c5665d  data/states/T1_P56_k17.json
+9c64b97a41de79f8557484bcb5d133ef3ae49edabdcacc81acce21b9565ff28a  data/states/T2_P53_k6.json
+5e992a6a1bc3af984c887a31c97a63ec8d4a4440b156491bc19bd24fe4a7855a  data/states/T2_P56_k17.json
+74748af4021ebebcada4a1fe5b78eff3136ea85d4b9f4618eebe337c779a39c8  data/states/T3_P53_k6.json
+0406bd3662aa5e23088b608b0af5e3665a441a3062ddad577c8f97f1de9efbcd  data/states/T3_P56_k17.json
+c321c338d8414d70a9ca9a393e795f63cbc28f3418dc6941e975772289ddf297  data/states/T4_P53_k6.json
+fe90fae6471935671da7f2de7d325042852bdea77a495b9a5561a728eda2fb9d  data/states/T4_P56_k17.json
+19d41abd194c40507394b939873625938425a6b42e421411be5528e174aa02b6  data/states/T5_P53_k6.json
+a577233612472156a162a0fd7fd2261d0a6d412ab539f0ec0205bbc9e08acacf  data/states/T5_P56_k17.json
+9ea6a74bd0fef806c7543dd0c06a82bb06e9c36da8801701f0266ac6f085bbb7  data/states/T6_P53_k6.json
+6c695083b7398515e76b728f45c31d2d87c01438c0544845a038b1d92516e644  data/states/T6_P56_k17.json
+d768bbd9cd1ba50c175bb05906fa9c61a6eaff242ab965f5a628df680f1ee6ce  data/states/T7_P53_k6.json
+3ae403d3bf3e3743e78cbafb08217a2a459fcaa982c9c78c5b6bbb09e4fffcaa  data/states/T7_P56_k17.json
+4a8d601013238cd225a19029e498ecd8a55508fd85c0801a8d0c190248bf5588  data/summaries/helper.summary
+f58150388781d4ae5e844312f183a3e3b23bde4b757ea6fbdc7ac9406fc89f19  data/summaries/lane.summary
+192296726caa9621dceb808a73e96f009625943695bd235e012f41b22ea0cffd  data/tables/T0_P53_k6.tsv
+fc8f9ff11cc7ed03b2617bbd1152313fe83b3b3c52a7d98fd05f81f670a75c21  data/tables/T0_P56_k17.tsv
+dce982ce679e78afe839968dbe2cb381826c65be93e03230debed644d3c809ec  data/tables/T1_P53_k6.tsv
+b54267d4234f294c95472b4722e7a98b9d42077b3762c0315dd9d450ade84207  data/tables/T1_P56_k17.tsv
+9986c5a9091cafc2ffbcc2cdf5fb8ddda587294983e8e180e7585a4d5ffa949b  data/tables/T2_P53_k6.tsv
+a692ceaad62059b704e4ff7bf234754f6d7d3bfdbdaae2af7b56ee7e543fa2ea  data/tables/T2_P56_k17.tsv
+ba5f15c4e5fb7b8aaa8b2970850a483503fcc8d80e82561f23edf8e00fb371f2  data/tables/T3_P53_k6.tsv
+4083289843dffff11ee5097ab8f01bd00210bd175c0da1389daaaf33b98e3994  data/tables/T3_P56_k17.tsv
+aa704e0bd73f427a2f22e0eef6d48015ecad041c392adc6608d6cb1529e0e89a  data/tables/T4_P53_k6.tsv
+9d6f239049c3c0ae88ce27ae1bfa45a0cb221fa08610b88672080c58fc32e9d3  data/tables/T4_P56_k17.tsv
+090e1506f4a8921cb051d0542651a99fe859a6be64cb3cd254c670e7d5683c0d  data/tables/T5_P53_k6.tsv
+e50a3000903ae988fd5069ed7787e2551c9796c521911db24752e7751a57762d  data/tables/T5_P56_k17.tsv
+3ac0373fcf8de2a69bc9f16e8d6aeb160ffb4a8b557ff5f1bddff816b91dc2b7  data/tables/T6_P53_k6.tsv
+8af9814a7d05b295b8bffdfc4f74c6c9f25bd04026c5a2ee3efe2d2fe6943d25  data/tables/T6_P56_k17.tsv
+331c377ed0f4150a8bcef90f2ed9796ae6e3b7f33d35e545db9350d9b16300f4  data/tables/T7_P53_k6.tsv
+64bbe6c5e19179987aaa3c1577ef25b0e9d7d63dd7187b62cce0feb5632d60f4  data/tables/T7_P56_k17.tsv
+1712b0363dba8e33698d3ef500ae6e9cae333b909451e857300adefb1852cb04  evidence/PUNCT-MID_THEORY_snapshot.md
+f6aae0fc0ae469a4a7be0a8261c2b204c640daf4482f1ae16687606eeccc7b92  evidence/proofs/T0P53k6_T0_P53_k6_o0_7213ba5548.drat.xz
+c5c8ae2a131414db2af7a861c2c556d15352791010d7e209662aeb8bf6c5c1c3  evidence/proofs/T0P53k6_T0_P53_k6_o0_9fbae75fd8.drat.xz
+5146503ec08b5b26e31cb9ad44b26f523df0468ec41b60f8115d3e34213a68af  evidence/proofs/T0P53k6_T0_P53_k6_o0_e80d14d770.drat.xz
+89ad6ea783bf1556e3fdb3589d42ef87bce55d81fc13f87f3ee005c6846d922f  evidence/proofs/T0P56k17_T0_P56_k17_o0_6100d2a49c_L70_2321a8.drat.xz
+8afaeca9f9160f3944d77b4e57067e7d44857b8a9a798324ceb3689e040f8517  evidence/proofs/T0P56k17_T0_P56_k17_o0_6100d2a49c_L70_85990f.drat.xz
+5c461b53cc3324374ac0d8b4d0f2dbddf952d96ffffe2a68b24dfe7bc116e0f3  evidence/proofs/T0P56k17_T0_P56_k17_o0_6100d2a49c_L70_af71a2.drat.xz
+962e4369ea48cb8cc55702b181cbfb83834f652875a386ee3b8ba4dfa396c1d6  evidence/proofs/T7P53k6_T7_P53_k6_o0_1289a5523a.drat.xz
+b98d4b1ee1442a2272381d41d626f95c6b9f281a911848e7897a0baee1754c31  evidence/proofs/T7P53k6_T7_P53_k6_o0_97e63f7375.drat.xz
+14b34e542d712ac45e50e867987d7f884b2a9bf7836a43a8d3dc6582bf0b43d6  evidence/proofs/T7P53k6_T7_P53_k6_o0_9fe87cd8cc.drat.xz
+7adf8f927602321168caf51d3152918f31b3d7a2bfe1fd178f480b9cb3115748  evidence/proofs/T7P56k17_T7_P56_k17_o0_1289a5523a.drat.xz
+74d15aa19a87c0f67c3ca1290b7189879b13e18f99695682d02279d8fd3eb671  evidence/proofs/T7P56k17_T7_P56_k17_o0_83fafc668f.drat.xz
+51a80e2dfdf5276f2f0c64631df1951c419fbea306c4ed93b13756de77a34548  evidence/proofs/T7P56k17_T7_P56_k17_o0_fe2dff1e1b_L12_75dafb.drat.xz
+b2e57f7a5bd4f9ada1cf284101476748ee534a2ffb3c7f85cde82b624c623076  evidence/proofs/index.tsv
+3d744ef52a949014c2faf7281b61a6c2c34c7bbdfd5202730366dba41fbd9148  evidence/sample_cnf_sha256.tsv
+cb671d2a912bc84d0cb02d47b1d0461ab33548696c9332dcebf7fd2f827790b0  lib/e8punct.py
+13b38e451f573633a4b7b48bb3217dae3cca08e0095f0feca7f974eaa53a22db  requirements.txt
+50e8810e2fb4ff2f3ea37dbde069a073a856fd68b8a00aec092665269f8d7c6d  sat/middrv.py
+991ced64e21d943d8e469285d90502e0e1b1e9063373b201e07d914c69f2fa69  sat/opts.py
+0a5591fc3ae201ce44dcd0b0617d51188f76d5b47a80b28fe54501f90bbc23c7  scripts/make_tables.py
+a4cd33cef93721cd79ae3dfaf69556f8502b22152e363fcab33b1fa402d68d11  scripts/provenance.py
+b7d8a05e24459fce88984160daad6b5cd3638fcb39f6c6bb54ec177d35849d28  scripts/replay.py
+2d53ba7139a16b9434d4d0a205467541b2531440456c89d8df5dd743d18e54f8  verify.sh
diff --git a/research/punctured-e8-48-56/NOTICE.md b/research/punctured-e8-48-56/NOTICE.md
@@ -0,0 +1,5 @@
+# Notice
+
+Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root).
+
+Based on #2639 (and #2338), the author's own; credits for the puncture lineage are in README.md and in #2639's NOTICE. Tools: kissat 4.0.4, drat-trim (Marijn Heule and Nathan Wetzler), neither vendored. `lib/e8punct.py`, `sat/*`, `scripts/*`, `checks/*` are the author's files (working-card PUNCT-MID, paths stripped); `scripts/provenance.py` is from #2639. `data/` and `evidence/` are exports of the author's working card PUNCT-MID taken on Oct 15, 2026.