README.html

<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>@xamidi/pmGenerator | An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.</title>
<meta property="og:title" content="@xamidi/pmGenerator">
<meta property="og:locale" content="en_US">
<meta name="description" content="An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.">
<meta property="og:description" content="An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.">
<link rel="canonical" href="https://xamidi.github.io/pmGenerator/">
<meta property="og:url" content="https://xamidi.github.io/pmGenerator/">
<meta property="og:site_name" content="@xamidi/pmGenerator">
<meta property="og:type" content="website">
<meta name="twitter:card" content="summary">
<meta property="twitter:title" content="@xamidi/pmGenerator">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<style>
/**
 * Gained from https://github.com/KrauseFx/markdown-to-html-github-style/blob/master/style.css (partly modified)
 */
body {
  font-family: -apple-system, BlinkMacSystemFont, Segoe UI, Helvetica, Arial, sans-serif, Apple Color Emoji, Segoe UI Emoji;
  font-size: 16px;
  line-height: 1.5;
  word-wrap: break-word;
  box-sizing: border-box;
  color: #111;
  background-color: #fff;
  -webkit-text-size-adjust: 100%;
  -webkit-font-feature-settings: "kern" 1;
  -moz-font-feature-settings: "kern" 1;
  -o-font-feature-settings: "kern" 1;
  font-feature-settings: "kern" 1;
  font-kerning: normal;
  padding: 30px;
}
body > #content {
  margin: 0;
  max-width: 900px;
  border: 1px solid #e1e4e8;
  padding: 10px 40px;
  padding-bottom: 20px;
  border-radius: 2px;
  margin-left: auto;
  margin-right: auto;
}
hr {
  color: #bbb;
  background-color: #bbb;
  height: 1px;
  flex: 0 1 auto;
  margin: 1em 0;
  padding: 0;
  border: none;
}
a {
  color: #0366d6;
  text-decoration: none;
}
a:visited {
  color: #0366d6;
}
a:hover {
  color: #0366d6;
  text-decoration: underline;
}
pre {
  background-color: #f6f8fa;
  border-radius: 3px;
  font-size: 85%;
  line-height: 1.45;
  overflow: auto;
  padding: 16px;
}
code {
  background-color: rgba(27,31,35,.05);
  border-radius: 3px;
  font-size: 85%;
  margin: 0;
  word-wrap: break-word;
  padding: .2em .4em;
  font-family: SFMono-Regular,Consolas,Liberation Mono,Menlo,Courier,monospace;
}
pre > code {
  background-color: transparent;
  border: 0;
  display: inline;
  font-size: inherit;
  line-height: inherit;
  margin: 0;
  overflow: visible;
  padding: 0;
  word-wrap: normal;
}
blockquote {
  margin-left: 30px;
  margin-top: 0;
  margin-bottom: 16px;
  border-left-width: 3px;
  padding: 0 1em;
  color: #828282;
  border-left: 4px solid #e8e8e8;
  padding-left: 15px;
  font-size: 18px;
  letter-spacing: -1px;
  font-style: italic;
}
blockquote * {
  font-style: normal !important;
  letter-spacing: 0;
  color: #6a737d !important;
}
table {
  width: max-content;
  max-width: 100%;
  line-height: 1.5;
  border-spacing: 3px;
  display: block;
  overflow: auto;
  margin-bottom: 16px;
  border-collapse: collapse;
}
td {
  padding: 6px 13px;
  border: 1px solid #dfe2e5;
}
th {
  font-weight: 600;
  padding: 6px 13px;
  border: 1px solid #dfe2e5;
}
tr {
  background-color: #fff;
  border-top: 1px solid #c6cbd1;
}
table tr:nth-child(2n) {
  background-color: #f6f8fa;
}
img {
  max-width: 100%;
}
p {
  line-height: 24px;
  font-size: 16px;
  color: #24292e;
  margin-top: 0;
}
li {
  color: #24292e;
  font-size: 16px;
  line-height: 1.5;
}
li + li {
  margin-top: 0.25em;
}
a:visited {
  color: #0366d6;
}
small {
  font-size: 90%;
}

/**
 * Gained from analysis in Mozilla Firefox inspector
 */
.markdown-container {
  max-width: 1214px;
  margin: auto;
  background-color: #fff;
  border: 1px solid #e1e4e8;
  border-radius: 6px;
}
.markdown-container img {
  background-color: #fff;
}
.markdown-container table img {
  background-color: transparent;
}
#readme {
  padding: 40px !important;
}
.container-lg {
  max-width: 1012px;
  margin-right: auto;
  margin-left: auto;
}
img {
  border-style: none;
  box-sizing: initial;
  margin-left: 0;
  margin-right: 0;
}
img[align="left"] {
  padding-right: 20px;
}
img[align=right] {
  padding-left: 20px;
}
h1, h2, h3, h4, h5, h6 {
  margin-top: 24px;
  margin-bottom: 16px;
  font-weight: 600;
  line-height: 1.25;
  color: #1F2328;
}
summary h1, summary h2, summary h3, summary h4, summary h5, summary h6 {
  display: inline-block;
}
h1, h2 {
  padding-bottom: .3em;
  border-bottom: 1px solid #d7dde3;
}
h1 {
  margin: .67em 0;
  font-size: 2em;
}
h2 {
  font-size: 1.5em;
}
h3 {
  font-size: 1.25em
}
h4 {
  font-size: 1em
}
h5 {
  font-size: .875em
}
h6 {
  font-size: .85em;
  color: #57606a;
}
ol, ul {
  padding-left: 2em;
  margin-top: 0;
}
ol ol, ul ol {
  list-style-type: lower-roman;
}
ol ol ol, ol ul ol, ul ol ol, ul ul ol {
  list-style-type: lower-alpha;
}
li br {
  box-sizing: border-box;
  line-height: 1.5;
}
b, strong {
  font-weight: 600;
}
details {
  margin-top: 0;
  margin-bottom: 16px;
}
</style>
</head>
<body><div class="markdown-container ltr"><div id="readme"><article class="container-lg"><img src="icon/icon-readme.png" alt="icon" style="float: left; padding-right: 20px; margin-top: -24px;">
<h1 id="xamidipmgenerator">@xamidi/pmGenerator</h1>
<p><a href="https://doi.org/10.5281/zenodo.10931360"><img src="svg/zenodo.10931360.svg" alt="DOI zenodo.10931360"></a> <a href="https://github.com/xamidi/pmGenerator/releases"><img src="https://img.shields.io/github/v/release/xamidi/pmGenerator?label=latest%20release" alt="releases"></a></p>
<details><summary><h4 id="contents">Contents</h4> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>
<ol>
<li><a href="#introduction">Introduction</a><ol>
<li><a href="#freges-calculus-simplified-by-%C5%82ukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz <code>(CpCqp,CCpCqrCCpqCpr,CCNpNqCqp)</code></a></li>
</ol>
</li>
<li><a href="#navigation">Navigation</a></li>
<li><a href="#usage">Usage</a><ol>
<li><a href="#commands">Commands</a></li>
<li><a href="#examples">Examples</a></li>
</ol>
</li>
<li><a href="#multi-node-computing">Multi-node Computing</a></li>
<li><a href="#custom-proof-systems">Custom Proof Systems</a><ol>
<li><a href="#merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-sample-info">Meredith's Axiom; 1-basis <code>(CCCCCpqCNrNsrtCCtpCsp)</code></a></li>
<li><a href="#walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-sample-info">Walsh's 1st Axiom; 1-basis <code>(CCpCCNpqrCsCCNtCrtCpt)</code></a></li>
<li><a href="#walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-sample-info">Walsh's 2nd Axiom; 1-basis <code>(CpCCqCprCCNrCCNstqCsr)</code></a></li>
<li><a href="#walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-sample-info">Walsh's 3rd Axiom; 1-basis <code>(CpCCNqCCNrsCptCCtqCrq)</code></a></li>
<li><a href="#walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-sample-info">Walsh's 4th Axiom; 1-basis <code>(CpCCNqCCNrsCtqCCrtCrq)</code></a></li>
<li><a href="#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info">Walsh's 5th Axiom; 1-basis <code>(CCpqCCCrCstCqCNsNpCps)</code></a></li>
<li><a href="#walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-sample-info">Walsh's 6th Axiom; 1-basis <code>(CCCpqCCCNrNsrtCCtpCsp)</code></a></li>
<li><a href="#s5-cpcqpccpcqrccpqcprccnpnqcqpclppclcpqclplqcnlnplnlnp-top1000-cardinalities-db-sample-info">S5 <code>(CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp)</code></a></li>
</ol>
</li>
<li><a href="#footnotes">Footnotes</a></li>
</ol>
</details>
<h4 id="introduction">Introduction</h4>
<p>This tool can collect exhaustive sets of <a href="https://en.wikipedia.org/wiki/Condensed_detachment">condensed detachment</a> proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”</a> collection.<br>The D-rule combines <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)">unification</a> with <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a> (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus <em>pmGenerator</em> covers all <a href="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> within <a href="https://en.wikipedia.org/wiki/Hilbert_system">Hilbert systems</a> based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.<br>There is a <a href="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information. Numerous use cases of the tool are exemplified, for example <em>proof parsing</em> under the <a href="https://github.com/xamidi/pmGenerator/discussions/2#proof-notation">Proof Notation</a> section of the <a href="https://github.com/xamidi/pmGenerator/discussions/2">“Minimal 1-bases for C-N propositional calculus”</a> proof minimization challenge.</p>
<p>Eligible for high-performance computing. If you have access to a powerful computer, you may use <em>pmGenerator</em> to further contribute to our knowledge regarding the <a href="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>. Progress that has already been made is exemplarily shown below.</p>
<h6 id="freges-calculus-simplified-by-łukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz (<a href="svg/frege-1.svg">CpCqp</a>,<a href="svg/frege-2.svg">CCpCqrCCpqCpr</a>,<a href="svg/lukasiewicz-3.svg">CCNpNqCqp</a>) &nbsp;<small>[<a href="data/top1000SmallestConclusions_1to39Steps.txt">top1000</a>] [<a href="data/cardinalities.txt">cardinalities</a>] [<a href="https://us.metamath.org/mmsolitaire/pmproofs.txt">db</a>] [<a href="data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/!.def">customization info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/default-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/default-plot_data_x500.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/default-bgraph.svg"><img src="svg/plot/default-bgraph.svg" alt="default-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:center">Paths</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://github.com/xamidi/pmGenerator/tree/master/data/dProofs-withConclusions" title="735'676'962 bytes compressed into 41'959'698 bytes (ratio approx. 17.5329)">dProofs29.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#7" alt="111"></td>
<td style="text-align:right">735 676 962</td>
<td style="text-align:right"><a href="log/dProofs29_6node_288cpu.log">1276.72</a></td>
<td style="text-align:right"><a href="log/utilization/29.log">2.16</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L1-L9">3.22</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=516720692%2F153725015" title="size(dProofs29.txt) / size(dProofs27.txt)">3.3613...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM" title="2'161'632'450 bytes compressed into 112'364'583 bytes (ratio approx. 19.2377)">dProofs31‑unfiltered31+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#4" alt="100"></td>
<td style="text-align:right">2 897 309 412</td>
<td style="text-align:right"><a href="log/dProofs31-unfiltered31+_48cpu.log">23.19</a></td>
<td style="text-align:right"><a href="log/utilization/31-31.log">5.78</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L11-L18">12.54</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=2161632450%2F516720692" title="size(dProofs31-unfiltered31+.txt) / size(dProofs29.txt)">4.1833...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/P1ki0IKQ#mb0QCboSu0Ofgr9nxspZTdcGUaAHPLzt-rQ8y0TN27k" title="1'741'338'664 bytes compressed into 89'327'496 bytes (ratio approx. 19.4939)">dProofs31.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#3" alt="011"></td>
<td style="text-align:right">2 477 015 626</td>
<td style="text-align:right"><a href="log/dProofs31_6node_288cpu.log">12681.68</a></td>
<td style="text-align:right"><a href="log/utilization/31.log">5.00</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L20-L28">12.51</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1741338664%2F516720692" title="size(dProofs31.txt) / size(dProofs29.txt)">3.3699...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA" title="8'349'023'875 bytes compressed into 402'886'507 bytes (ratio approx. 20.7230)">dProofs33‑unfiltered31+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#4" alt="100"></td>
<td style="text-align:right">11 246 333 287</td>
<td style="text-align:right"><a href="log/dProofs33-unfiltered31+_48cpu.log">86.59</a></td>
<td style="text-align:right"><a href="log/utilization/33-31.log">19.49</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L30-L37">43.73</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=8349023875%2F2161632450" title="size(dProofs33-unfiltered31+.txt) / size(dProofs31-unfiltered31+.txt)">3.8623...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/ixshHB7S#ktigbEzeOvCvFP8pruhC0NFfeK91p__eS_uZxBtIy0w" title="7'295'621'951 bytes compressed into 352'588'174 bytes (ratio approx. 20.6916)">dProofs33‑unfiltered33+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#2" alt="010"></td>
<td style="text-align:right">10 192 931 363</td>
<td style="text-align:right"><a href="log/dProofs33-unfiltered33+_48cpu.log">92.19</a></td>
<td style="text-align:right"><a href="log/utilization/33-33.log">17.04</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L39-L46">39.42</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=7295621951%2F1741338664" title="size(dProofs33-unfiltered33+.txt) / size(dProofs31.txt)">4.1896...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/S5tDkSCC#WKEWeT7Niaj9ZVWrqiy-FGPI8ACGsd2H7mA3ZWUITFY" title="5'876'664'090 bytes compressed into 279'929'404 bytes (ratio approx. 20.9934)">dProofs33.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#1" alt="001"></td>
<td style="text-align:right">8 353 679 716</td>
<td style="text-align:right"><a href="log/dProofs33_60node_2880cpu.log">110356.00</a></td>
<td style="text-align:right"><a href="log/utilization/33.log">14.67</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L48-L56">39.20</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=5876664090%2F1741338664" title="size(dProofs33.txt) / size(dProofs31.txt)">3.3747...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/2893yZ7S#JlCHv4uOajgBJPPE2W87F_LAPzkH0-FlF4_2OrccuC4" title="30'717'801'573 bytes compressed into 1'400'853'331 bytes (ratio approx. 21.9279)">dProofs35‑unfiltered31+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#4" alt="100"></td>
<td style="text-align:right">41 964 134 860</td>
<td style="text-align:right"><a href="log/dProofs35-unfiltered31+_48cpu.log">366.69</a></td>
<td style="text-align:right"><a href="log/utilization/35-31.log">67.74</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L58-L65">154.60</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=30717801573%2F8349023875" title="size(dProofs35-unfiltered31+.txt) / size(dProofs33-unfiltered31+.txt)">3.6792...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/WwNViKRa#UBiPOFN4wRkMgetY60eAQi1oXVQ3fQdkcg7hFxB-Dfk" title="28'223'320'428 bytes compressed into 1'290'589'236 bytes (ratio approx. 21.8686)">dProofs35‑unfiltered33+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#2" alt="010"></td>
<td style="text-align:right">38 416 251 791</td>
<td style="text-align:right"><a href="log/dProofs35-unfiltered33+_48cpu.log">329.08</a></td>
<td style="text-align:right"><a href="log/utilization/35-33.log">61.41</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L67-L74">137.87</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=28223320428%2F7295621951" title="size(dProofs35-unfiltered33+.txt) / size(dProofs33-unfiltered33+.txt)">3.8685...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/b0t1xbKI#6sjAICTTNMfQ2VO5kyVMpxVHSQNZzxWPktOEGJkberk" title="24'669'947'024 bytes compressed into 1'121'466'816 bytes (ratio approx. 21.9979)">dProofs35‑unfiltered35+.txt</a></small></td>
<td style="text-align:center"><img src="svg/markers.svg#1" alt="001"></td>
<td style="text-align:right">33 023 626 740</td>
<td style="text-align:right"><a href="log/dProofs35-unfiltered35+_48cpu.log">307.16</a></td>
<td style="text-align:right"><a href="log/utilization/35-35.log">53.49</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L76-L83">124.14</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=24669947024%2F5876664090" title="size(dProofs35-unfiltered35+.txt) / size(dProofs33.txt)">4.1979...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/6wUyDQzT#DQIJOLd5dCn-6V9sJWiJXeGRPUTUaA-7LqbGfLStjV0" title="113'174'356'461 bytes compressed into 4'897'020'927 bytes (ratio approx. 23.1109)">dProofs37‑unfiltered31+.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#4" alt="100"></td>
<td style="text-align:right">155 138 491 321</td>
<td style="text-align:right"><a href="log/dProofs37-unfiltered31+_144cpu.log">18975.40</a></td>
<td style="text-align:right"><a href="log/utilization/37-31.log">238.30</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L85-L92">485.12</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=113174356461%2F30717801573" title="size(dProofs37-unfiltered31+.txt) / size(dProofs35-unfiltered31+.txt)">3.6843...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/q1txWSZA#P_HoU6_4_fCYd_1Zw7Y5UG7R4UWdlVm4_s9xG6pzsoY" title="103'965'043'304 bytes compressed into 4'479'575'346 bytes (ratio approx. 23.2087)">dProofs37‑unfiltered33+.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#2" alt="010"></td>
<td style="text-align:right">142 381 295 095</td>
<td style="text-align:right"><a href="log/dProofs37-unfiltered33+_144cpu.log">14331.28</a></td>
<td style="text-align:right"><a href="log/utilization/37-33.log">217.76</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L94-L101">446.50</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=103965043304%2F28223320428" title="size(dProofs37-unfiltered33+.txt) / size(dProofs35-unfiltered33+.txt)">3.6836...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/Pg0STDYL#YZF0i4i6AcLP2_gZQuHNb40ajbspYC8wOFsK7fmKQTw" title="95'571'571'048 bytes compressed into 4'105'722'124 bytes (ratio approx. 23.2777)">dProofs37‑unfiltered35+.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#1" alt="001"></td>
<td style="text-align:right">128 595 197 788</td>
<td style="text-align:right"><a href="log/dProofs37-unfiltered35+_144cpu.log">14740.88</a></td>
<td style="text-align:right"><a href="log/utilization/37-35.log">197.08</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L103-L110">408.38</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=95571571048%2F24669947024" title="size(dProofs37-unfiltered35+.txt) / size(dProofs35-unfiltered35+.txt)">3.8740...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/WwEgwITB#Fk145eaRsw7S3IFpuxwcbeyYi4IwNatrxF7SWnZwvIo" title="352'398'833'029 bytes compressed into 14'265'852'732 bytes (ratio approx. 24.7023)">dProofs39‑unfiltered35+.txt</a></small><sup>❈</sup></td>
<td style="text-align:center"><img src="svg/markers.svg#1" alt="001"></td>
<td style="text-align:right">480 994 030 817</td>
<td style="text-align:right"><a href="log/dProofs39-unfiltered35+_64cpu.log">4566.99</a></td>
<td style="text-align:right"><a href="log/utilization/39-35.log">1301.97</a></td>
<td style="text-align:right"><a href="log/jobsRSS.txt#L112-L119">1768.07</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=352398833029%2F95571571048" title="size(dProofs39-unfiltered35+.txt) / size(dProofs37-unfiltered35+.txt)">3.6872...</a></td>
</tr>
</tbody>
</table>

</details>

<p>Measured RAM requirements correspond to the maximum resident set size according to <a href="https://slurm.schedmd.com/documentation.html">Slurm</a>, i.e. <code>MaxRSS</code> of <a href="https://slurm.schedmd.com/sacct.html">sacct</a>.<br>Required resources vary based on implementation and environment; numbers are to illustrate orders of magnitude.<br>Some more – and very special – proof systems are illustrated <a href="#custom-proof-systems">further down below</a>.</p>
<h4 id="navigation">Navigation</h4>
<ul>
<li><a href="https://github.com/xamidi/pmGenerator/tree/master">C++20 branch</a> (master)</li>
<li><a href="https://github.com/xamidi/pmGenerator/tree/c++11">C++11 branch</a> (version 1.2.0, discontinued)</li>
<li><a href="https://codeberg.org/xamidi/pmGenerator">Mirror repository</a> (on Codeberg.org)</li>
</ul>
<h4 id="usage">Usage</h4>
<pre><code>pmGenerator ( &lt;configuring command&gt; | &lt;composable command&gt; )+ | &lt;configuring command&gt;* &lt;standalone command&gt;
</code></pre><h6 id="commands">Commands</h6>
<pre><code>Configuring:
  -c [-i &lt;file&gt;] [-s &lt;string&gt;] [-n] [-N &lt;limit or -1&gt;] [-l] [-e &lt;id&gt;] [-d]
     Proof system customization ; Generates a SHA-512/224 hash to identify the system, sets the effective data location to "&lt;data location&gt;/&lt;hash&gt;", and (if nonexisting) creates the !.def file.
       -i: specify axioms by input file path (where a LF-separated string of axioms is stored), ignoring lines that are empty or starting with '%'
       -s: specify axioms by comma-separated string ; used only when '-i' unspecified ; default: "C0C1.0,CC0C1.2CC0.1C0.2,CCN0N1C1.0"
       -n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
       -N: enable necessitation rule "N" for the given system with unlimited (-N -1) or limited (-N &lt;positive amount&gt;) consecutive necessitation steps allowed
       -l: disable lazy N-rule parsing ; parse proofs Nα:Lβ despite knowing α:β (requires more time but less memory)
       -e: specify extracted system with the given identifier
       -d: default system ; ignore all other arguments except '-e'

Composable:
  -g &lt;limit or -1&gt; [-u] [-q &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-k &lt;limit or -1&gt;] [-b] [-f] [-s]
     Generate proof files ; at ./data/[&lt;hash&gt;/]/dProofs-withConclusions/ when '-s' unspecified ; otherwise at ./data/[&lt;hash&gt;/]/dProofs-withoutConclusions/
       -u: unfiltered (significantly faster, but generates redundant proofs)
       -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates) ; default: 50
       -l: limit symbolic length of generated conclusions to at most the given number ; works only in extracted environments ; recommended to use in combination with '-q' to save memory
       -k: similar to '-l' ; limit symbolic length of consequents in generated conclusions, i.e. antecedents in conditionals are not limited (but non-conditionals are limited in full length)
       -b: brief parsing ; append conclusion structures to D-proof processing and use them for rule evaluation (collects faster, but requires significantly more memory)
       -f: full parsing ; parse entire D-proofs rather than using conclusion strings for rule evaluation ; used only when '-b' unspecified
       -s: proof files without conclusions, requires additional parsing ; entails '-f' ; used only when '-b' unspecified
  -r &lt;D-proof database&gt; &lt;output file&gt; [-l &lt;path&gt;] [-i &lt;prefix&gt;] [-s] [-d]
     Replacements file creation based on proof files
       -l: customize data location path ; default: "data"
       -i: customize input file path prefix in data location ; default: "dProofs-withConclusions/dProofs"
       -s: proof files without conclusions, requires additional parsing ; sets default input file path prefix to "dProofs-withoutConclusions/dProofs"
       -d: print debug information
  -a &lt;initials&gt; &lt;replacements file&gt; &lt;D-proof database&gt; &lt;output file&gt; [-s] [-l] [-w] [-d]
     Apply replacements file
       -s: style all proofs (replace proofs with alphanumerically smaller variants)
       -l: list all proofs (i.e. not only modified proofs)
       -w: wrap results
       -d: print debug information
  --parse &lt;string&gt; [-n] [-u] [-j &lt;limit or -1&gt;] [-b] [-s] [-e] [-f] [-o &lt;output file&gt;] [-d]
     Parse and print proofs given by a comma-separated string
       -n: print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
       -u: print formulas in infix notation with operators as Unicode characters ; used only when '-n' unspecified
       -j: join common subproofs together when they are used at least a given amount of times ; default: 2
       -b: only print conclusions of the given proofs ; sets default of '-j' to 1
       -s: only print summary with conclusions and abstract condensed detachment proofs ; used only when '-b' unspecified
       -e: keep expanded proof strings ; show fully detailed condensed detachment proofs rather than allowing them to contain references ; used only when '-b' unspecified
       -f: proofs are given by input file path (where a comma-separated string is stored), ignoring all CR, LF, whitespace, and lines starting with '%'
       -o: redirect the result's output to the specified file
       -d: print debug information
  --transform &lt;string&gt; [-s &lt;string&gt;] [-j &lt;limit or -1&gt;] [-p &lt;limit or -1&gt;] [-n] [-u] [-t &lt;string&gt;] [-e] [-i &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-b] [-w] [-z] [-x &lt;limit&gt;] [-y] [-k] [-v &lt;file&gt;] [-h] [-q] [-f] [-o &lt;output file&gt;] [-d]
     Transform proof summary (as by '--parse [...] -s') into recombined variant ; ignores configured system (proof summaries provide their own axioms) ; "," represents LF
       -s: list a subproof with its conclusion if it occurs in the given comma-separated list of conclusions
       -j: join common subproofs together when they are used at least a given amount of times ; default: 2
       -p: only keep subproofs with primitive lengths not exceeding the given limit ; default: -1
       -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
       -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified)
       -t: only transform proofs of specified theorems (proven by subsequences of the input), given by a comma-separated string ; '-t .': all given conclusions ; '-t _': all used conclusions ; default: final theorem only
       -e: keep expanded proof strings ; show fully detailed condensed detachment proofs rather than allowing them to contain references
       -i: decrease memory requirements but increase time consumption by not storing intermediate unfoldings that exceed a certain length ; default: -1
       -l: abort computation when combined requested proof sequences exceed the given limit in bytes ; default: 134217728 (i.e. 128 MiB)
       -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates ; beneficial in preparing '-z'
       -w: read input without conclusions given
       -z: proof compression ; find and remove internal redundancies (e.g. non-trivial parts not affecting intermediate theorems) by attempting to use shorter owned subproofs at all positions
       -x: proof compression with extended modification range; before each round generate relative abstract proofs (D-rules only) with up to &lt;range&gt; steps, potentially improving rules with new formulas ; default: 0
       -y: disable multi-threaded D-rule replacement search in case proof compression is performed (enables deterministic procedure) ; not affecting exhaustive generations via '-x', which remain nondeterministic
       -k: store maximum-size proofs generated via 'x' also when they do not prove known intermediate theorems, so they can still be used as replacements for subproofs ; increases memory consumption significantly
       -v: coordinate iteration phases for maximum-size proofs generated via 'x' with the specified vault file (to avoid repeating these computations over multiple runs) ; used only when '-k' unspecified
       -h: save raw intermediate results in files before each proof compression round (and after productive rounds) ; after each preparation phase (exhaustive generation) in case '-x' is specified
       -q: skip first round preparation for '-x' ; useful to continue working on intermediate results produced by an aborted computation using '-h'
       -f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
       -o: redirect the result's output to the specified file
       -d: print debug information
  --unfold &lt;string&gt; [-n] [-t &lt;string&gt;] [-i &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-w] [-v] [-f] [-o &lt;output file&gt;] [-d]
     Break down proof summary (as by '--parse [...] -s') into primitive steps ; ignores configured system (proof summaries provide their own axioms) ; "," represents LF
       -n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
       -t: obtain proofs of specified theorems (proven by subsequences of the input), given by a comma-separated string ; '-t .': all given conclusions ; '-t _': all used conclusions ; default: final theorem only
       -i: decrease memory requirements but increase time consumption by not storing intermediate unfoldings that exceed a certain length ; default: -1
       -l: abort computation when combined requested proof sequences exceed the given limit in bytes ; default: 134217728 (i.e. 128 MiB)
       -w: wrap results
       -v: read input without conclusions given
       -f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
       -o: redirect the result's output to the specified file
       -d: print debug information
  --search &lt;string&gt; [-n] [-s] [-w] [-t] [-p] [-f] [-d]
     Search in proof files at ./data/[&lt;hash&gt;/]/dProofs-withConclusions/ via comma-separated string of full formulas or full proofs ; [Hint: Generate missing files with '--variate 1 -s'.]
       -n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
       -s: search for schemas of the given formulas
       -w: search whole collections of schemas (i.e. enable multiple results per term) ; entails '-s'
       -t: search for formulas of the given schemas (allows multiple results per term) ; used only when '-s' and '-w' unspecified
       -p: search proofs (rather than conclusions) ; used only when '-n', '-s', '-w' and '-t' unspecified
       -f: search terms are given by input file path (where a comma-separated string is stored), ignoring all CR, LF, whitespace, and lines starting with '%'
       -d: print debug information
  --extract [-t &lt;limit or -1&gt;] [-o &lt;output file&gt;] [-s] [-z] [-# &lt;amount up to 35&gt;] [-h &lt;string&gt;] [-l &lt;limit or -1&gt;] [-k &lt;limit or -1&gt;] [-f] [-d]
     Various options to extract information from proof files ; [Hint: Generate missing files with '--variate 1 -s'.]
       -t: compose file with up to the given amount of smallest conclusions that occur in proof files ; includes origins, symbolic lengths, proofs, and formulas in normal Polish notation
       -o: specify output file path for '-t' ; relative to effective data location ; default: "top&lt;amount&gt;SmallestConclusions_&lt;min proof length&gt;to&lt;max proof length&gt;Steps&lt;unfiltered info&gt;.txt"
       -s: redundant schema removal for '-t' ; very time-intensive for requesting huge collections from unfiltered proof files - better pre-filter via '-g' or '-m' instead ; default: false
       -z: force redundant schema removal for '-t' ; like '-s', but also filter proof files not declared as unfiltered (which might be useful for non-standard procedures)
       -#: initialize proof system at ./data/[&lt;hash&gt;/]/extraction-&lt;id&gt;/ with the given amount of smallest filtered conclusions that occur in proof files ; specify with '-c &lt;parent system&gt; -e &lt;id&gt;'
       -h: similar to '-#' ; hand-pick conclusions with a comma-separated string of proofs ; "." to not modify axioms
       -l: similar to '-#' (but creates identical system with prebuilt proof files) ; copy proofs with conclusions that have symbolic lengths of at most the given number
       -k: similar to '-l' ; copy proofs with conclusions that have consequents or are non-conditionals of symbolic lengths of at most the given number ; can be combined with '-l'
       -f: proofs for '-h' are given by input file path (where a comma-separated string is stored), ignoring all CR, LF, whitespace, and lines starting with '%'
       -d: print debug information
  --assess [-u] [-s] [-d]
     Print proof file cardinalities, numbers of proof candidates for all generation steps up to the next one, and all stored and estimated next removal amounts (to assess generation expenditures)
       -u: use unfiltered proof files
       -s: use proof files without conclusions
       -d: print debug information
  --iterate [-u] [-s]
     Iterate proof candidates currently next up for generation and print their amount (for resource consumption measurements)
       -u: use unfiltered proof files
       -s: use proof files without conclusions
  --variate ( 0 | 1 ) [-l &lt;path&gt;] [-i &lt;prefix&gt;] [-o &lt;prefix&gt;] [-s] [-d]
     Create proof files with removed (--variate 0) or added (--variate 1) conclusions from in-memory data and proof files of the other variant
       -l: customize data location path ; default: "data"
       -i: customize input file path prefix in data location ; default: "dProofs-withConclusions/dProofs" or "dProofs-withoutConclusions/dProofs"
       -o: customize output file path prefix in data location ; default: "dProofs-withoutConclusions/dProofs" or "dProofs-withConclusions/dProofs"
       -s: only use data stored in-memory
       -d: print debug information
  --plot [-l &lt;path&gt;] [-i &lt;prefix&gt;] [-s] [-t] [-x &lt;limit or -1&gt;] [-y &lt;limit or -1&gt;] [-o &lt;output file&gt;] [-d]
     Print conclusion length plot data
       -l: customize data location path ; default: "data"
       -i: customize input file path prefix in data location ; requires files with conclusions ; default: "dProofs-withConclusions/dProofs"
       -s: measure symbolic length (in contrast to conclusion representation length)
       -u: include unfiltered proof files
       -t: table arrangement, one data point per row
       -x: upper horizontal limit
       -y: upper vertical limit
       -o: print to given output file
       -d: print debug information

Standalone:
  -m &lt;limit&gt; [-s]
     MPI-based multi-node filtering (-m &lt;n&gt;) of a first unfiltered proof file (with conclusions) at ./data/[&lt;hash&gt;/]dProofs-withConclusions/dProofs&lt;n&gt;-unfiltered&lt;n&gt;+.txt. Creates dProofs&lt;n&gt;.txt.
       -s: disable smooth progress mode (lowers memory requirements, but makes terrible progress predictions)
</code></pre><h6 id="examples">Examples</h6>
<pre><code>pmGenerator -g -1 -q 50
pmGenerator -g 19 -g 21 -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
pmGenerator --variate 0 -l data/ -o "dProofs-withoutConclusions (all)/dProofs" -d
pmGenerator --variate 1 -s --search CNpCCNpqNp -n -d --search CNpCCNpqNp -n -s
pmGenerator --variate 1 -s --search CCNpCpqCNpCpq,CCCCppCppCCCppCppCNCCqqCqqCCCqqCqqCCqqCqqCCCppCppCNCCqqCqqCCCqqCqqCCqqCqq -n -w -d
pmGenerator --plot -s -d --plot -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt
pmGenerator -c -N -1 -n -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp --parse DD2D16DD2DD2D13DD2D1D2DD2D1D2D1DD2DD2D13D1DD2DD2D13DD2D13114DD2D13DD2D1311D3DD2DD2D13DD2D1311 -j 2 -n
pmGenerator --parse DD2D11DD2D13DD2D1DD22D11DD2D11DD2D131 -n -s -o data/CNCpNqCrCsq.txt --transform data/CNCpNqCrCsq.txt -f -n -j 1 -e --transform data/CNCpNqCrCsq.txt -f -n -t CNCpNqCrq -d
pmGenerator --unfold CpCqp=1,CCpCqrCCpqCpr=2,CCNpNqCqp=3,[0]CCpCNqNrCpCrq:D2D13,[1]Cpp:DD211,[2]NCCppNCqq:DD3DD2DD2D[0]D[0]11D1[1][1] -n -t CNNpp,NCCppNCqq
pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -p -2 -d
pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDDD1D1D1D1DDDD1D1D11111111,[1]=D1DD[0]1[0],[2]=DDDD1DD[1][1]1111" -n -w -t _
pmGenerator -c -s CCCCC0.1CN2N3.2.4CC4.0C3.0 -g 35 --plot -s -t -x 50 -y 100 -o data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/plot_data_x50_y100.txt
pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --search CpCqp,CCpCqrCCpqCpr,CCNpNqCqp -n
pmGenerator --variate 1 -s --extract -t 1000 -s -d
pmGenerator --variate 1 -s --extract -# 35 -d -c -d -e 0
pmGenerator -m 17 -s
</code></pre><h4 id="multi-node-computing">Multi-node Computing</h4>
<p>For MPI-based filtering, each spawned process is multi-threaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.<br>The following exemplary <a href="https://slurm.schedmd.com/documentation.html">Slurm</a> batch script has been used via <a href="https://slurm.schedmd.com/sbatch.html">sbatch</a> in order to reduce <code>dProofs31‑unfiltered31+.txt</code> to <code>dProofs31.txt</code>.</p>
<pre><code>#!/bin/zsh
#SBATCH --job-name=pmGen-20
#SBATCH --output=output_%J.txt
#SBATCH --partition=c18m
#SBATCH --account=rwth1392
#SBATCH --time=3-00:00:00
#SBATCH --mem-per-cpu=3900M
#SBATCH --cpus-per-task=48
#SBATCH --mail-user=&lt;email&gt;
#SBATCH --mail-type=END,FAIL,TIME_LIMIT
## Number of nodes to use ; Also update #processes (via srun)!
#SBATCH --nodes=6
srun -n 6 ./pmGenerator -m 31
</code></pre><p>A subsequent query with <a href="https://slurm.schedmd.com/squeue.html">squeue</a> would then reveal the following information:</p>
<pre><code>$ squeue -o "%.9i %.8j %.9P %.11a %.8u %.5C %.5D %.10T %.10M %.10l %.19S %R" -u &lt;userID&gt;
    JOBID     NAME PARTITION     ACCOUNT     USER  CPUS NODES      STATE       TIME TIME_LIMIT          START_TIME NODELIST(REASON)
 34762453 pmGen-20      c18m    rwth1392 &lt;userID&gt;   288     6    RUNNING       3:34 3-00:00:00 2023-05-04T07:52:24 ncm[0297,0306-0307,0315,0320-0321]
</code></pre><p>You may have a look at the <a href="log/dProofs31_6node_288cpu.log">log file</a> generated by that computation.</p>
<h4 id="custom-proof-systems">Custom Proof Systems</h4>
<p>There are illustrated seven proof systems in the following which according to <a href="http://fitelson.org/walsh.pdf">M. Walsh and B. Fitelson</a> are minimal 1-bases (i.e. generators consisting of shortest single axioms) for propositional logic.
Their only remaining candidate CCCpqCCrNsCtNtCCtpCrp can be refuted since <code>pmGenerator -c -n -s CCCpqCCrNsCtNtCCtpCrp -g -1</code> produces only 9 more representatives (1.<code>D11:CCpCNpqCrCNpq</code>, 2.<code>D1D11:CCNppCqp</code>, 3.<code>D1D1D11:CCpNCpNpCqNCpNp</code>, 4.<code>DD11D11:CpCNCqCNqrCNqr</code>, 5.<code>DD11D1D11:CpCNCNqqq</code>, 6.<code>DDD11D111:CNCpCNpqCNpq</code>, 7.<code>DD11D1D1D11:CpCNCqNCqNqNCqNq</code>, 8.<code>DDD11D1D111:CNCNppp</code>, 9.<code>DDD11D1D1D111:CNCpNCpNpNCpNp</code>).<br>Therefore, these systems are implied to be the only minimal 1-bases for C-N propositional calculus.</p>
<p>Target files are distinguished using a hexadecimal SHA-512/224 digest as a folder name for each proof system.<br>For user identification of hash folders, I recommend to use custom icons, such as illustrated below.<br>&nbsp;&nbsp;<sub><img src="png/customIconPreview.png" alt="Icon-Preview" title="Hash folders with icons under Windows 7"></sub><br>For this purpose, a favicon database (<code>ico.dll</code>) is included in the release files, as well as an archive (<code>ico.7z</code>) with all the <code>.ico</code> files for usability with non-Windows operating systems.</p>
<h6 id="merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-sample-info">Meredith's Axiom; 1-basis (<a href="svg/meredith.svg">CCCCCpqCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/top1000SmallestConclusions_1to83Steps.txt">top1000</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/cardinalities.txt">cardinalities</a>] [<a href="data/m.txt">sample</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/m-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/m-plot_data_x200.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/m-bgraph.svg"><img src="svg/plot/m-bgraph.svg" alt="m-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/XkUgRB4J#iK3tk82M-QdI5dBJbuLgN21PFrHHKDKE9gVYdwaBvz0" title="2'422'110'008 bytes compressed into 108'455'851 bytes (ratio approx. 22.3327)">dProofs67.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">2 422 110 008</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs67_24node_1152cpu.log">5500.48</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/67.log">7.77</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L1-L9">10.00</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=996579205%2F586496233" title="size(dProofs67.txt) / size(dProofs65.txt)">1.6992...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/T501SRaY#aAB8wnSt2OEQ7WBPM_ceo44Gwu_ZY28v7g-y_xXWMAg" title="1'692'424'708 bytes compressed into 70'022'956 bytes (ratio approx. 24.1696)">dProofs69.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">4 114 534 716</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs69_72node_3456cpu.log">15432.96</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/69.log">12.79</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L11-L19">17.07</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1692424708%2F996579205" title="size(dProofs69.txt) / size(dProofs67.txt)">1.6982...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/vgM2VQ6L#9CepsGbebmnqlSdXlgsjL4PmoU8kmcB9vJiBFDCj3XE" title="4'269'010'294 bytes compressed into 174'601'845 bytes (ratio approx. 24.4500)">dProofs71‑unfiltered71+.txt</a></small></td>
<td style="text-align:right">8 383 545 010</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs71-unfiltered71+_48cpu.log">148.71</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/71-71.log">25.06</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L21-L28">47.19</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=4269010294%2F1692424708" title="size(dProofs71-unfiltered71+.txt) / size(dProofs69.txt)">2.5224...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/HsUwiaBI#Lr9dg_vkkl5LDniDbhoajaoUf5DMrSuhOLWs7AVtsZo" title="8'690'446'595 bytes compressed into 350'352'093 bytes (ratio approx. 24.8049)">dProofs73‑unfiltered71+.txt</a></small></td>
<td style="text-align:right">17 073 991 605</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs73-unfiltered71+_48cpu.log">254.48</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/73-71.log">50.85</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L30-L37">93.84</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=8690446595%2F4269010294" title="size(dProofs73-unfiltered71+.txt) / size(dProofs71-unfiltered71+.txt)">2.0357...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/G8klVCKA#vrclPrG9dTd7JuyKt3YoBCipmOyJh5WAGXi4A4qQH00" title="15'912'038'278 bytes compressed into 627'204'237 bytes (ratio approx. 25.3698)">dProofs75‑unfiltered71+.txt</a></small></td>
<td style="text-align:right">32 986 029 883</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs75-unfiltered71+_48cpu.log">372.08</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/75-71.log">97.22</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L39-L46">172.29</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=15912038278%2F8690446595" title="size(dProofs75-unfiltered71+.txt) / size(dProofs73-unfiltered71+.txt)">1.8309...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/W00zQRSS#pgCUAfcqdq6MqqaQ5tKLn7CQ_PsclH6_WKELo_FBA4k" title="29'440'512'597 bytes compressed into 1'137'980'567 bytes (ratio approx. 25.8708)">dProofs77‑unfiltered71+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">62 426 542 480</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs77-unfiltered71+_64cpu.log">742.28</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/77-71.log">181.43</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L48-L55">304.37</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=29440512597%2F15912038278" title="size(dProofs77-unfiltered71+.txt) / size(dProofs75-unfiltered71+.txt)">1.8502...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/vNC7xWrPSneFbn7" title="56'177'510'817 bytes compressed into 2'123'231'985 bytes (ratio approx. 26.4585)">dProofs79‑unfiltered71+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">118 604 053 297</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs79-unfiltered71+_64cpu.log">1578.13</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/79-71.log">339.19</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L57-L64">550.39</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=56177510817%2F29440512597" title="size(dProofs79-unfiltered71+.txt) / size(dProofs77-unfiltered71+.txt)">1.9081...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/xiKTUrcNNECfWJ2" title="108'323'290'318 bytes compressed into 4'002'658'331 bytes (ratio approx. 27.0628)">dProofs81‑unfiltered71+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">226 927 343 615</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs81-unfiltered71+_64cpu.log">2896.16</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/81-71.log">635.64</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L66-L73">1003.84</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=108323290318%2F56177510817" title="size(dProofs81-unfiltered71+.txt) / size(dProofs79-unfiltered71+.txt)">1.9282...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/Sy4u4kFrpBvXxYP" title="207'577'506'070 bytes compressed into 7'501'303'661 bytes (ratio approx. 27.6722)">dProofs83‑unfiltered71+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">434 504 849 685</td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/dProofs83-unfiltered71+_64cpu.log">5380.80</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/utilization/83-71.log">1196.78</a></td>
<td style="text-align:right"><a href="log/custom/meredith-CCCCCpqCNrNsrtCCtpCsp/jobsRSS.txt#L75-L82">1846.46</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=207577506070%2F108323290318" title="size(dProofs83-unfiltered71+.txt) / size(dProofs81-unfiltered71+.txt)">1.9162...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-sample-info">Walsh's 1st Axiom; 1-basis (<a href="svg/walsh1st.svg">CCpCCNpqrCsCCNtCrtCpt</a>) &nbsp;<small>[<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/top1000SmallestConclusions_1to161Steps.txt">top1000</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/cardinalities.txt">cardinalities</a>] [<a href="data/w1.txt">sample</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w1-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w1-plot_data_x400.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w1-bgraph.svg"><img src="svg/plot/w1-bgraph.svg" alt="w1-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/utFBXQoL#Om9V_K5VP65ggMDeJJ7L389oXcpFtfaBduNyzCCF_0s" title="5'371'226'962 bytes compressed into 164'113'739 bytes (ratio approx. 32.7287)">dProofs137.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">5 371 226 962</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs137_48node_2304cpu.log">6707.84</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/137.log">14.01</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L1-L9">20.56</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1235762264%2F954016122" title="size(dProofs137.txt) / size(dProofs135.txt)">1.2953...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/u0cnxDDJ#2GZAd2TC7bDiNivMBcj6Q20ls8qOottXK-NnGM0XEMM" title="1'602'917'394 bytes compressed into 46'630'892 bytes (ratio approx. 34.3746)">dProofs139.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">6 974 144 356</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs139_72node_3456cpu.log">11663.04</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/139.log">18.06</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L11-L19">25.23</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1602917394%2F1235762264" title="size(dProofs139.txt) / size(dProofs137.txt)">1.2971...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/L5sgkQ4J#PfkvYUDrVs-kC_e96LRCWHGulBywbLcTgDGqdrYCPLA" title="5'160'630'061 bytes compressed into 144'705'625 bytes (ratio approx. 35.6630)">dProofs141‑unfiltered141+.txt</a></small></td>
<td style="text-align:right">12 134 774 417</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs141-unfiltered141+_48cpu.log">121.87</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/141-141.log">31.18</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L21-L28">53.15</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=5160630061%2F1602917394" title="size(dProofs141-unfiltered141+.txt) / size(dProofs139.txt)">3.2195...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/v8ckRSTT#oqzUYIBn7JpCVuIWucRWnrDHd3QR8zcY3nkcAxvBqXk" title="8'473'778'240 bytes compressed into 236'694'201 bytes (ratio approx. 35.8005)">dProofs143‑unfiltered141+.txt</a></small></td>
<td style="text-align:right">20 608 552 657</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs143-unfiltered141+_48cpu.log">167.89</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/143-141.log">52.28</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L30-L37">83.02</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=8473778240%2F5160630061" title="size(dProofs143-unfiltered141+.txt) / size(dProofs141-unfiltered141+.txt)">1.6420...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/uwlhXCZL#WOjPacTW0IOP4Faw5Y5PcnQMsjEPkf36lXcMvZpgfDo" title="12'166'973'212 bytes compressed into 335'810'389 bytes (ratio approx. 36.2317)">dProofs145‑unfiltered141+.txt</a></small></td>
<td style="text-align:right">32 775 525 869</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs145-unfiltered141+_48cpu.log">281.73</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/145-141.log">82.13</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L39-L46">126.35</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=12166973212%2F8473778240" title="size(dProofs145-unfiltered141+.txt) / size(dProofs143-unfiltered141+.txt)">1.4358...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/7t0AEZBZ#yJRMROkE6QVRlg2xJx3KK2VWxN2ibSMXBrDF8VC-UQY" title="16'130'023'412 bytes compressed into 440'582'939 bytes (ratio approx. 36.6106)">dProofs147‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">48 905 549 281</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs147-unfiltered141+_64cpu.log">376.27</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/147-141.log">121.50</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L48-L55">185.33</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=16130023412%2F12166973212" title="size(dProofs147-unfiltered141+.txt) / size(dProofs145-unfiltered141+.txt)">1.3257...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/yxdCXKwL#SfnM2LGuViJ3lIQQyrXskTu6ObGZuYfOltmYTV4zqNw" title="21'575'998'815 bytes compressed into 582'486'170 bytes (ratio approx. 37.0412)">dProofs149‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">70 481 548 096</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs149-unfiltered141+_64cpu.log">564.46</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/149-141.log">173.34</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L57-L64">264.17</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=21575998815%2F16130023412" title="size(dProofs149-unfiltered141+.txt) / size(dProofs147-unfiltered141+.txt)">1.3376...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/kyJbalQmwpsBxIZ" title="29'138'591'117 bytes compressed into 779'973'708 bytes (ratio approx. 37.3584)">dProofs151‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">99 620 139 213</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs151-unfiltered141+_64cpu.log">825.12</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/151-141.log">243.11</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L66-L73">371.22</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=29138591117%2F21575998815" title="size(dProofs151-unfiltered141+.txt) / size(dProofs149-unfiltered141+.txt)">1.3505...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/n9ccdaAHt2YgyBO" title="39'867'127'446 bytes compressed into 1'058'080'615 bytes (ratio approx. 37.6787)">dProofs153‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">139 487 266 659</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs153-unfiltered141+_64cpu.log">1169.19</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/153-141.log">340.40</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L75-L82">520.65</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=39867127446%2F29138591117" title="size(dProofs153-unfiltered141+.txt) / size(dProofs151-unfiltered141+.txt)">1.3681...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/iw4tK8bBsjWldVW" title="53'770'763'259 bytes compressed into 1'413'419'788 bytes (ratio approx. 38.0430)">dProofs155‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">193 258 029 918</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs155-unfiltered141+_64cpu.log">1610.97</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/155-141.log">471.06</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L84-L91">708.37</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=53770763259%2F39867127446" title="size(dProofs155-unfiltered141+.txt) / size(dProofs153-unfiltered141+.txt)">1.3487...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/YWjWeIZ6ms6dPZf" title="73'644'408'291 bytes compressed into 1'913'276'599 bytes (ratio approx. 38.4913)">dProofs157‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">266 902 438 209</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs157-unfiltered141+_64cpu.log">2178.79</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/157-141.log">647.45</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L93-L100">965.41</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=73644408291%2F53770763259" title="size(dProofs157-unfiltered141+.txt) / size(dProofs155-unfiltered141+.txt)">1.3695...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/5gJDQbZdgszCFE7" title="98'773'762'822 bytes compressed into 2'541'220'153 bytes (ratio approx. 38.8686)">dProofs159‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">365 676 201 031</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs159-unfiltered141+_64cpu.log">3099.95</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/159-141.log">881.28</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L102-L109">1307.16</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=98773762822%2F73644408291" title="size(dProofs159-unfiltered141+.txt) / size(dProofs157-unfiltered141+.txt)">1.3412...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/JH7S80qFOdcIfT6" title="133'862'174'308 bytes compressed into 3'408'096'122 bytes (ratio approx. 39.2777)">dProofs161‑unfiltered141+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">499 538 375 339</td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/dProofs161-unfiltered141+_64cpu.log">4419.27</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/utilization/161-141.log">1198.88</a></td>
<td style="text-align:right"><a href="log/custom/walsh1-CCpCCNpqrCsCCNtCrtCpt/jobsRSS.txt#L111-L118">1789.96</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=133862174308%2F98773762822" title="size(dProofs161-unfiltered141+.txt) / size(dProofs159-unfiltered141+.txt)">1.3552...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-sample-info">Walsh's 2nd Axiom; 1-basis (<a href="svg/walsh2nd.svg">CpCCqCprCCNrCCNstqCsr</a>) &nbsp;<small>[<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/top1000SmallestConclusions_1to43Steps.txt">top1000</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/cardinalities.txt">cardinalities</a>] [<a href="data/w2.txt">sample</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w2-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w2-plot_data_x6000.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w2-bgraph.svg"><img src="svg/plot/w2-bgraph.svg" alt="w2-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/qkVhAYgZ#dgBiQbhJswQegZH4-fMHtxgPgnsLIJEgi1wvUMouYAw" title="4'428'081'090 bytes compressed into 48'240'683 bytes (ratio approx. 91.7914)">dProofs35.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">4 428 081 090</td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/dProofs35_24node_1152cpu.log">1335.68</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/utilization/35.log">8.56</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/jobsRSS.txt#L1-L9">12.14</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=2972554245%2F977151740" title="size(dProofs35.txt) / size(dProofs33.txt)">3.0420...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/CptW2J5J#XkOBO_cZMSyupCdrZ8ozbDHcrQzUURpALBHbKV01VM8" title="9'046'645'168 bytes compressed into 87'167'665 bytes (ratio approx. 103.7844)">dProofs37.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">13 474 726 258</td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/dProofs37_72node_3456cpu.log">11637.12</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/utilization/37.log">26.82</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/jobsRSS.txt#L11-L19">36.16</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=9046645168%2F2972554245" title="size(dProofs37.txt) / size(dProofs35.txt)">3.0433...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/jtliXJLZ#F14xQkIYPPY9U8FDcM_N_3DRoCx8u9j4J_aIMLcoAPY" title="27'702'180'806 bytes compressed into 250'367'939 bytes (ratio approx. 110.6459)">dProofs39‑unfiltered39+.txt</a></small></td>
<td style="text-align:right">41 176 907 064</td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/dProofs39-unfiltered39+_48cpu.log">139.36</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/utilization/39-39.log">81.00</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/jobsRSS.txt#L21-L28">99.42</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=27702180806%2F9046645168" title="size(dProofs39-unfiltered39+.txt) / size(dProofs37.txt)">3.0621...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/zwkHEaBb#3zHOZVNSnnDPRFTf2WzYaZBiKmo7s8I9hp6BssrItjM" title="84'489'763'512 bytes compressed into 714'705'708 bytes (ratio approx. 118.2162)">dProofs41‑unfiltered39+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">125 666 670 576</td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/dProofs41-unfiltered39+_64cpu.log">476.43</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/utilization/41-39.log">246.33</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/jobsRSS.txt#L30-L37">291.86</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=84489763512%2F27702180806" title="size(dProofs41-unfiltered39+.txt) / size(dProofs39-unfiltered39+.txt)">3.0499...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/f1P2wTUMf3nId0g" title="257'774'107'632 bytes compressed into 2'041'458'453 bytes (ratio approx. 126.2696)">dProofs43‑unfiltered39+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">383 440 778 208</td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/dProofs43-unfiltered39+_64cpu.log">1881.40</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/utilization/43-39.log">748.02</a></td>
<td style="text-align:right"><a href="log/custom/walsh2-CpCCqCprCCNrCCNstqCsr/jobsRSS.txt#L39-L46">888.57</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=257774107632%2F84489763512" title="size(dProofs43-unfiltered39+.txt) / size(dProofs41-unfiltered39+.txt)">3.0509...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-sample-info">Walsh's 3rd Axiom; 1-basis (<a href="svg/walsh3rd.svg">CpCCNqCCNrsCptCCtqCrq</a>) &nbsp;<small>[<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/top1000SmallestConclusions_1to73Steps.txt">top1000</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/cardinalities.txt">cardinalities</a>] [<a href="data/w3.txt">sample</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w3-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w3-plot_data_x1000.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w3-bgraph.svg"><img src="svg/plot/w3-bgraph.svg" alt="w3-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/61sCyYIb#MoxnnjaHKxvT6d4pJCbZZs3Z52ufUx9ARAc5LNJjnMk" title="4'295'581'846 bytes compressed into 77'688'599 bytes (ratio approx. 55.2923)">dProofs61.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">4 295 581 846</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs61_72node_3456cpu.log">3908.16</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/61.log">10.14</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L1-L9">13.43</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1786902420%2F1044902840" title="size(dProofs61.txt) / size(dProofs59.txt)">1.7101...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/WkMVkQbb#YEZX-szEMXLyaZW2a37D39FoXdNiQivXXOAS7d3Nb5M" title="3'053'239'506 bytes compressed into 49'574'609 bytes (ratio approx. 61.5888)">dProofs63.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">7 348 821 352</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs63_72node_3456cpu.log">10532.16</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/63.log">16.96</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L11-L19">26.15</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=3053239506%2F1786902420" title="size(dProofs63.txt) / size(dProofs61.txt)">1.7086...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/f41EjDiS#E7prfzRMDCzTw4kXcVf-En7tOMUZ0o1X1QrZ3Utw1sU" title="9'415'171'948 bytes compressed into 159'435'383 bytes (ratio approx. 59.0532)">dProofs65‑unfiltered65+.txt</a></small></td>
<td style="text-align:right">16 763 993 300</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs65-unfiltered65+_48cpu.log">352.47</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/65-65.log">37.46</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L21-L28">59.38</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=9415171948%2F3053239506" title="size(dProofs65-unfiltered65+.txt) / size(dProofs63.txt)">3.0836...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/j8NxySjQ#1sMFi4YPBJZzDYslYKan53VPSwUGWdVt9m78hM67k4s" title="22'771'527'998 bytes compressed into 382'594'819 bytes (ratio approx. 59.5187)">dProofs67‑unfiltered65+.txt</a></small></td>
<td style="text-align:right">39 535 521 298</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs67-unfiltered65+_48cpu.log">711.19</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/67-65.log">86.14</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L30-L37">124.11</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=22771527998%2F9415171948" title="size(dProofs67-unfiltered65+.txt) / size(dProofs65-unfiltered65+.txt)">2.4185...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/mlEwBbhZ#KBH21b6120HB2zqo0Cs8OWZYfjCUoWK6AeS75BtNdgY" title="49'180'529'600 bytes compressed into 801'720'838 bytes (ratio approx. 61.3437)">dProofs69‑unfiltered65+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">88 716 050 898</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs69-unfiltered65+_64cpu.log">1222.77</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/69-65.log">189.80</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L39-L46">251.38</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=49180529600%2F22771527998" title="size(dProofs69-unfiltered65+.txt) / size(dProofs67-unfiltered65+.txt)">2.1597...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/iDMtDYEdBpHTLRz" title="103'402'476'250 bytes compressed into 1'635'136'468 bytes (ratio approx. 63.2378)">dProofs71‑unfiltered65+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">192 118 527 148</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs71-unfiltered65+_64cpu.log">2507.20</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/71-65.log">405.23</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L48-L55">524.03</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=103402476250%2F49180529600" title="size(dProofs71-unfiltered65+.txt) / size(dProofs69-unfiltered65+.txt)">2.1025...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/rrZNVCfUpai5ZQC" title="220'718'480'631 bytes compressed into 3'365'806'262 bytes (ratio approx. 65.5767)">dProofs73‑unfiltered65+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">412 837 007 779</td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/dProofs73-unfiltered65+_64cpu.log">5133.48</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/utilization/73-65.log">867.31</a></td>
<td style="text-align:right"><a href="log/custom/walsh3-CpCCNqCCNrsCptCCtqCrq/jobsRSS.txt#L57-L64">1098.91</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=220718480631%2F103402476250" title="size(dProofs73-unfiltered65+.txt) / size(dProofs71-unfiltered65+.txt)">2.1345...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-sample-info">Walsh's 4th Axiom; 1-basis (<a href="svg/walsh4th.svg">CpCCNqCCNrsCtqCCrtCrq</a>) &nbsp;<small>[<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/top1000SmallestConclusions_1to169Steps.txt">top1000</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/cardinalities.txt">cardinalities</a>] [<a href="data/w4.txt">sample</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w4-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w4-plot_data_x1250.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w4-bgraph.svg"><img src="svg/plot/w4-bgraph.svg" alt="w4-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/Wld2zSQJ#6teaby3Dz71_kEjVDGJR3DPq2aR0aERqzi9j0NKNsT0" title="9'131'925'110 bytes compressed into 182'531'802 bytes (ratio approx. 50.0292)">dProofs149.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">9 131 925 110</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs149_24node_1152cpu.log">6302.40</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/149.log">21.12</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L1-L9">36.33</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1898469358%2F1504178093" title="size(dProofs149.txt) / size(dProofs147.txt)">1.2621...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/epNS1KJI#o546RRx4JG-pp5VxSCrp7P2ousuuy6SuLWMZ6wCB2Ok" title="2'394'008'601 bytes compressed into 43'962'661 bytes (ratio approx. 54.4555)">dProofs151.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">11 525 933 711</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs151_72node_3456cpu.log">10297.92</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/151.log">26.43</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L11-L19">45.07</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=2394008601%2F1898469358" title="size(dProofs151.txt) / size(dProofs149.txt)">1.2610...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/a9dG1TZK#ULVpQWaIMuhFkov8ozfyAscNEkSTQFeG4P8_4DUHpVU" title="13'257'500'572 bytes compressed into 259'889'811 bytes (ratio approx. 51.0120)">dProofs153‑unfiltered153+.txt</a></small></td>
<td style="text-align:right">24 783 434 283</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs153-unfiltered153+_48cpu.log">158.55</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/153-153.log">55.60</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L21-L28">86.32</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=13257500572%2F2394008601" title="size(dProofs153-unfiltered153+.txt) / size(dProofs151.txt)">5.5377...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/XxcFxSKQ#S7A_wpPAHPKUK56Sxsd6S3V8Kpxiga2VdPMVfvkqjr0" title="18'088'589'265 bytes compressed into 348'720'195 bytes (ratio approx. 51.8714)">dProofs155‑unfiltered153+.txt</a></small></td>
<td style="text-align:right">42 872 023 548</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs155-unfiltered153+_48cpu.log">230.07</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/155-153.log"> 95.18</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L30-L37">137.85</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=18088589265%2F13257500572" title="size(dProofs155-unfiltered153+.txt) / size(dProofs153-unfiltered153+.txt)">1.3644...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/zsUTEI7b#BOSxu1sy1SH8O_4ooXLauOyMgO0PoBKHff-GRu1dkOc" title="26'019'597'453 bytes compressed into 493'724'872 bytes (ratio approx. 52.7006)">dProofs157‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">68 891 621 001</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs157-unfiltered153+_64cpu.log">302.65</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/157-153.log">151.49</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L39-L46">199.75</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=26019597453%2F18088589265" title="size(dProofs157-unfiltered153+.txt) / size(dProofs155-unfiltered153+.txt)">1.4384...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/sxQG1x4rWREeGt6" title="34'641'539'688 bytes compressed into 651'219'941 bytes (ratio approx. 53.1948)">dProofs159‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">103 533 160 689</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs159-unfiltered153+_64cpu.log">453.35</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/159-153.log">226.16</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L48-L55">293.63</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=34641539688%2F26019597453" title="size(dProofs159-unfiltered153+.txt) / size(dProofs157-unfiltered153+.txt)">1.3313...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/BFnkL1fAj8Vi9Z9" title="55'681'200'733 bytes compressed into 1'040'015'069 bytes (ratio approx. 53.5388)">dProofs161‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">159 214 361 422</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs161-unfiltered153+_64cpu.log">644.41</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/161-153.log">345.00</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L57-L64">427.35</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=55681200733%2F34641539688" title="size(dProofs161-unfiltered153+.txt) / size(dProofs159-unfiltered153+.txt)">1.6073...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/L8jieKQK7qdtGtr" title="75'698'437'452 bytes compressed into 1'393'369'930 bytes (ratio approx. 54.3276)">dProofs163‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">234 912 798 874</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs163-unfiltered153+_64cpu.log">923.80</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/163-153.log">506.04</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L66-L73">613.85</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=75698437452%2F55681200733" title="size(dProofs163-unfiltered153+.txt) / size(dProofs161-unfiltered153+.txt)">1.3594...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/mzESbz3fOeuZf4u" title="127'132'189'367 bytes compressed into 2'232'538'824 bytes (ratio approx. 56.9451)">dProofs165‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">362 044 988 241</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs165-unfiltered153+_64cpu.log">1372.75</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/165-153.log">770.18</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L75-L82">899.59</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=127132189367%2F75698437452" title="size(dProofs165-unfiltered153+.txt) / size(dProofs163-unfiltered153+.txt)">1.6794...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/KWqprDlpJ8rIDgI" title="180'054'503'529 bytes compressed into 3'127'767'660 bytes (ratio approx. 57.5665)">dProofs167‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">542 099 491 770</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs167-unfiltered153+_64cpu.log">2013.71</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/167-153.log">1144.49</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L84-L91">1316.14</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=180054503529%2F127132189367" title="size(dProofs167-unfiltered153+.txt) / size(dProofs165-unfiltered153+.txt)">1.4162...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/EHjzWTh1uEPbb6v" title="273'688'640'204 bytes compressed into 4'667'700'887 bytes (ratio approx. 58.6346)">dProofs169‑unfiltered153+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">815 788 131 974</td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/dProofs169-unfiltered153+_64cpu.log">3061.78</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/utilization/169-153.log">1716.57</a></td>
<td style="text-align:right"><a href="log/custom/walsh4-CpCCNqCCNrsCtqCCrtCrq/jobsRSS.txt#L93-L100">1933.14</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=273688640204%2F180054503529" title="size(dProofs169-unfiltered153+.txt) / size(dProofs167-unfiltered153+.txt)">1.5200...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info">Walsh's 5th Axiom; 1-basis (<a href="svg/walsh5th.svg">CCpqCCCrCstCqCNsNpCps</a>) &nbsp;<small>[<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/top1000SmallestConclusions_1to55Steps.txt">top1000</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/cardinalities.txt">cardinalities</a>] [<a href="data/w5.txt">sample</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w5-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w5-plot_data_x30000.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w5-bgraph.svg"><img src="svg/plot/w5-bgraph.svg" alt="w5-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/rpdkmD7Q#KiBXlTbHX_Ik0WsrqpJiuY7dm2UxXHo2qx6pZQLiTe0" title="30'353'473'441 bytes compressed into 186'227'707 bytes (ratio approx. 162.9912)">dProofs49.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">30 353 473 441</td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/dProofs49_24node_1152cpu.log">3559.68</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/utilization/49.log">57.45</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/jobsRSS.txt#L1-L9">74.22</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=17543709434%2F7404015719" title="size(dProofs49.txt) / size(dProofs47.txt)">2.3694...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/Xld2xbLD#twvOLLo-EmrEWj3lS-Fl9WZx3Mx8-8_Tv1m_-0gHBX8" title="41'567'415'644 bytes compressed into 213'357'886 bytes (ratio approx. 194.8248)">dProofs51.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">71 920 889 085</td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/dProofs51_72node_3456cpu.log">18849.60</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/utilization/51.log">135.68</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/jobsRSS.txt#L11-L19">170.98</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=41567415644%2F17543709434" title="size(dProofs51.txt) / size(dProofs49.txt)">2.3693...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/D9lmlIBI#-t6sbz_b9uWfcu9UdrOfyjvofuqtr1TEwO4dU-OSCiA" title="98'556'622'203 bytes compressed into 460'765'948 bytes (ratio approx. 213.8974)">dProofs53‑unfiltered53+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">170 477 511 288</td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/dProofs53-unfiltered53+_64cpu.log">754.63</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/utilization/53-53.log">320.89</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/jobsRSS.txt#L21-L28">412.98</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=98556622203%2F41567415644" title="size(dProofs53-unfiltered53+.txt) / size(dProofs51.txt)">2.3710...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/k5gB5xLWduhCQDN" title="233'577'192'864 bytes compressed into 993'411'897 bytes (ratio approx. 235.1262)">dProofs55‑unfiltered53+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">404 054 704 152</td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/dProofs55-unfiltered53+_64cpu.log">2173.65</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/utilization/55-53.log">759.14</a></td>
<td style="text-align:right"><a href="log/custom/walsh5-CCpqCCCrCstCqCNsNpCps/jobsRSS.txt#L30-L37">916.66</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=233577192864%2F98556622203" title="size(dProofs55-unfiltered53+.txt) / size(dProofs53-unfiltered53+.txt)">2.3699...</a></td>
</tr>
</tbody>
</table>

</details>

<h6 id="walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-sample-info">Walsh's 6th Axiom; 1-basis (<a href="svg/walsh6th.svg">CCCpqCCCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/top1000SmallestConclusions_1to95Steps.txt">top1000</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/cardinalities.txt">cardinalities</a>] [<a href="data/w6.txt">sample</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/w6-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w6-plot_data_x800.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w6-bgraph.svg"><img src="svg/plot/w6-bgraph.svg" alt="w6-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/eo1HyTLZ#SJocgod8TDAJlMTHbYAUCFt5jVz6o9jgvMGskXfvjbc" title="3'484'676'910 bytes compressed into 104'717'502 bytes (ratio approx. 33.2769)">dProofs79.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">3 484 676 910</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs79_24node_1152cpu.log">6643.52</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/79.log">9.36</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L1-L9">16.18</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1224028908%2F793144209" title="size(dProofs79.txt) / size(dProofs77.txt)">1.5432...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/SoFVUZpB#-5srphNVczF5_bcXupk0ENkyuk1-VCqTDL5zfIwOTFc" title="1'883'180'962 bytes compressed into 52'125'039 bytes (ratio approx. 36.1281)">dProofs81.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">5 367 857 872</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs81_72node_3456cpu.log">15677.76</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/81.log">14.23</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L11-L19">24.41</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=1883180962%2F1224028908" title="size(dProofs81.txt) / size(dProofs79.txt)">1.5385...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/jwFHiJKS#645vcSU_-a4EA3elJaxhAcRIz6-IjuWBmnPIWLUCYSE" title="8'242'569'881 bytes compressed into 211'458'617 bytes (ratio approx. 38.9796)">dProofs83‑unfiltered83+.txt</a></small></td>
<td style="text-align:right">13 610 427 753</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs83-unfiltered83+_48cpu.log">235.56</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/83-83.log">33.96</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L21-L28">61.15</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=8242569881%2F1883180962" title="size(dProofs83-unfiltered83+.txt) / size(dProofs81.txt)">4.3769...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/PgFWBTaR#MMJ-jaRsXWSDJIpFzDFfXJ0lsLYXgWsY6eykjQsgs_Y" title="14'942'566'211 bytes compressed into 373'668'124 bytes (ratio approx. 39.9889)">dProofs85‑unfiltered83+.txt</a></small></td>
<td style="text-align:right">28 552 993 964</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs85-unfiltered83+_48cpu.log">415.03</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/85-83.log">69.16</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L30-L37">112.16</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=14942566211%2F8242569881" title="size(dProofs85-unfiltered83+.txt) / size(dProofs83-unfiltered83+.txt)">1.8128...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/OpEykDwB#qivTUdjYd0J-IFqFtdIOWNGBXbDL3liaKraMx5T9BGM" title="25'607'335'143 bytes compressed into 622'577'637 bytes (ratio approx. 41.1312)">dProofs87‑unfiltered83+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">54 160 329 107</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs87-unfiltered83+_64cpu.log">679.52</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/87-83.log">128.54</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L39-L46">196.18</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=25607335143%2F14942566211" title="size(dProofs87-unfiltered83+.txt) / size(dProofs85-unfiltered83+.txt)">1.7137...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/RqMWPM5NF9dVvjW" title="42'757'203'285 bytes compressed into 1'017'266'453 bytes (ratio approx. 42.0315)">dProofs89‑unfiltered83+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">96 917 532 392</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs89-unfiltered83+_64cpu.log">1166.01</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/89-83.log">229.28</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L48-L55">356.90</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=42757203285%2F25607335143" title="size(dProofs89-unfiltered83+.txt) / size(dProofs87-unfiltered83+.txt)">1.6697...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/S0dI5sz7g6OE5Wi" title="68'394'045'164 bytes compressed into 1'583'904'093 bytes (ratio approx. 43.1807)">dProofs91‑unfiltered83+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">165 311 577 556</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs91-unfiltered83+_64cpu.log">1997.90</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/91-83.log">389.83</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L57-L64">598.55</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=68394045164%2F42757203285" title="size(dProofs91-unfiltered83+.txt) / size(dProofs89-unfiltered83+.txt)">1.5995...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/mwVplLXdwBeuHF7" title="112'090'394'619 bytes compressed into 2'542'434'207 bytes (ratio approx. 44.0878)">dProofs93‑unfiltered83+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">277 401 972 175</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs93-unfiltered83+_64cpu.log">3700.55</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/93-83.log">650.43</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L66-L73">993.50</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=112090394619%2F68394045164" title="size(dProofs93-unfiltered83+.txt) / size(dProofs91-unfiltered83+.txt)">1.6388...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/D5fKvVtEOC4d82K" title="193'064'036'043 bytes compressed into 4'209'134'915 bytes (ratio approx. 45.8679)">dProofs95‑unfiltered83+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">470 466 008 218</td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/dProofs95-unfiltered83+_64cpu.log">6619.36</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/utilization/95-83.log">1089.83</a></td>
<td style="text-align:right"><a href="log/custom/walsh6-CCCpqCCCNrNsrtCCtpCsp/jobsRSS.txt#L75-L82">1638.71</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=193064036043%2F112090394619" title="size(dProofs95-unfiltered83+.txt) / size(dProofs93-unfiltered83+.txt)">1.7223...</a></td>
</tr>
</tbody>
</table>

</details>

<p>The above systems show remarkable differences in complexity, despite similarities. For example, the syntax trees of Walsh's 3rd and 4th axiom differ only in four leaf nodes.</p>
<p>Only systems with an odd-ary rule such as necessitation can have condensed detachment proofs of even lengths.<br>The system of modal logic illustrated below extends <a href="#freges-calculus-simplified-by-łukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz</a>. It can be covered by enabling the N-rule without limiting the number of its consecutive applications via <code>-c -N -1</code>.</p>
<h6 id="s5-cpcqpccpcqrccpqcprccnpnqcqpclppclcpqclplqcnlnplnlnp-top1000-cardinalities-db-sample-info">S5 (<a href="svg/frege-1.svg">CpCqp</a>,<a href="svg/frege-2.svg">CCpCqrCCpqCpr</a>,<a href="svg/lukasiewicz-3.svg">CCNpNqCqp</a>,<a href="svg/truth-4.svg">CLpp</a>,<a href="svg/kripke-5.svg">CLCpqCLpLq</a>,<a href="svg/lewis-6.svg">CNLNpLNLNp</a>) &nbsp;<small>[<a href="data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/top1000SmallestConclusions_1to30Steps.txt">top1000</a>] [<a href="data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/cardinalities.txt">cardinalities</a>] [<a href="data/s5proofs.txt">db</a>] [<a href="data/s5.txt">sample</a>] [<a href="data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/!.def">info</a>]</small></h6>
<details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/S5-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/S5-plot_data_x150.txt">raw</a>]</small></summary>
<a href="https://xamidi.github.io/pmGenerator/svg/plot/S5-bgraph.svg"><img src="svg/plot/S5-bgraph.svg" alt="S5-bgraph.svg" width="700"></a></details>
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

<table>
<thead>
<tr>
<th>Files up to..</th>
<th style="text-align:right">&nbsp; Size of Files   <br>[B]         &nbsp;</th>
<th style="text-align:right">+Costs&nbsp;&nbsp;<br>[≈core‑h]</th>
<th style="text-align:right">RAM&nbsp;(load)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">RAM&nbsp;(gen.)<br>[≈GiB]   &nbsp;</th>
<th style="text-align:right">Recent&nbsp;<br>Growth</th>
</tr>
</thead>
<tbody>
<tr>
<td><small><a href="https://mega.nz/file/uo1ykLqZ#fLIOtOVef7gjMSXQzFphqbEe-3Cu9OuyHILn-WXzaGY" title="929'688'759 bytes compressed into 45'411'380 bytes (ratio approx. 20.4726)">dProofs23.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">929 688 759</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs23_24node_1152cpu.log">2787.20</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/23.log">4.39</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L1-L9">5.02</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=486227545%2F228361353" title="size(dProofs23.txt) / size(dProofs22.txt)">2.1292...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/eg0HDByB#HpeNFCbHT-uOYkMW8L52sSsTGmXmvfrcRIlu1bUBOG0" title="996'813'323 bytes compressed into 4'4089'689 bytes (ratio approx. 22.6088)">dProofs24.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">1 926 502 082</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs24_72node_3456cpu.log">11495.04</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/24.log">9.00</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L11-L19">11.99</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=996813323%2F486227545" title="size(dProofs24.txt) / size(dProofs23.txt)">2.0500...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/bk8j2IxR#FmIU7zdKQIlTwv75bM92Qx-_y0hKUQWM5GYos6VAxbc" title="2'341'783'351 bytes compressed into 102'862'831 bytes (ratio approx. 22.7661)">dProofs25‑unfiltered25+.txt</a></small></td>
<td style="text-align:right">4 268 285 433</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs25-unfiltered25+_48cpu.log">90.85</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/25-25.log">19.50</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L21-L28">70.23</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=2341783351%2F996813323" title="size(dProofs25-unfiltered25+.txt) / size(dProofs24.txt)">2.3492...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/qwsyVIaY#NXvwJEzcU3bXL-ii-mIEQ8dFC9UwRetRfMccTY01EBg" title="5'023'015'642 bytes compressed into 212'381'862 bytes (ratio approx. 23.6509)">dProofs26‑unfiltered25+.txt</a></small></td>
<td style="text-align:right">9 291 301 075</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs26-unfiltered25+_48cpu.log">197.73</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/26-25.log">41.27</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L30-L37">143.64</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=5023015642%2F2341783351" title="size(dProofs26-unfiltered25+.txt) / size(dProofs25-unfiltered25+.txt)">2.1449...</a></td>
</tr>
<tr>
<td><small><a href="https://mega.nz/file/K4kyQRpZ#hqOhwlxioylT29_0NpuSpM9OOLWvAzGhw1mXL2ElwHs" title="11'414'777'022 bytes compressed into 494'039'493 bytes (ratio approx. 23.1050)">dProofs27‑unfiltered25+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">20 706 078 097</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs27-unfiltered25+_64cpu.log">450.03</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/27-25.log">89.08</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L39-L46">305.84</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=11414777022%2F5023015642" title="size(dProofs27-unfiltered25+.txt) / size(dProofs26-unfiltered25+.txt)">2.2724...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/nCADlGnlYCgOjvk" title="24'722'013'566 bytes compressed into 1'073'629'811 bytes (ratio approx. 23.0266)">dProofs28‑unfiltered25+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">45 428 091 663</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs28-unfiltered25+_64cpu.log">1052.76</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/28-25.log">190.06</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L48-L55">632.76</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=24722013566%2F11414777022" title="size(dProofs28-unfiltered25+.txt) / size(dProofs27-unfiltered25+.txt)">2.1657...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/qElEXv7QpbJ5KNs" title="54'687'281'728 bytes compressed into 2'345'678'277 bytes (ratio approx. 23.3141)">dProofs29‑unfiltered25+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">100 115 373 391</td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs29-unfiltered25+_64cpu.log">2364.16</a><br><sup><code>-q 50</code></sup><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs29-unfiltered25+_64cpu-2.log">2121.81</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/29-25.log">409.23</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L57-L64">1327.37</a><br><sup><code>-q 50</code></sup><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L66-L73">746.09</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=54687281728%2F24722013566" title="size(dProofs29-unfiltered25+.txt) / size(dProofs28-unfiltered25+.txt)">2.2120...</a></td>
</tr>
<tr>
<td><small><a href="https://rwth-aachen.sciebo.de/s/h0ipKwDK8xwU9ce" title="118'130'673'527 bytes compressed into 4'950'709'496 bytes (ratio approx. 23.8614)">dProofs30‑unfiltered25+.txt</a></small><sup>❈</sup></td>
<td style="text-align:right">218 246 046 918</td>
<td style="text-align:right"><sup><code>-q 50</code></sup><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/dProofs30-unfiltered25+_64cpu.log">4774.60</a></td>
<td style="text-align:right"><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/utilization/30-25.log">870.21</a></td>
<td style="text-align:right"><sup><code>-q 50</code></sup><a href="log/custom/s5-CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp/jobsRSS.txt#L75-L82">1563.51</a></td>
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=118130673527%2F54687281728" title="size(dProofs30-unfiltered25+.txt) / size(dProofs29-unfiltered25+.txt)">2.1601...</a></td>
</tr>
</tbody>
</table>

</details>
<a name="footnotes"></a>

<p><sup>✻</sup><sub>A proof is <em>minimal</em> in context of a behavioral graph if it is the alphanumerically smallest sequence of all shortest possible proofs towards its theorem. Consequently, each proof counted in a behavioral graph uniquely represents its theorem. So these graphs illustrate how many theorems (including but not counting all their infinitely many instances) of a certain size can first be proven using a certain amount of proof steps. These alphanumeric minima may not actually occur in the proof files, but they clearly exist. In contrast, proof minimization usually aims towards finding a <em>shortest</em> proof (also “minimal”, but referring to length) — not “<em>the</em> minimal proof” as in this context.</sub><br><sup>❈</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project <a href="pdf/rwth1392_extension_2025.pdf" title="View rwth1392_extension_2025.pdf">rwth1392</a>.</sub></p>
</article></div></div></body></html>