( This log file was generated by 'pmGenerator 1.2.3' (master branch), compiled by 'oneAPI DPC++/C++ Compiler 2024.2.0 (2024.2.0.20240602)'. The run was executed on a CLAIX-2018-OPTANE MPI node — 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) — running Linux, Rocky 9.6. Wall-clock time: 32.51555… h CPU utilization: 2080.99555… core-h ) Wed May 27 11:23:36 2026: Process started. [pid: 496960, tid:22908007675712] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(4294967295, false, true, null, -1, -1, true) [Main] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Main] Calling generateDProofRepresentativeFiles(4294967295, false, true, null, -1, -1, true). Wed May 27 11:23:36 2026: Unlimited D-proof representative generator started. [parallel ; 64 hardware thread contexts, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.01 ms taken to load initial representatives. 3.53 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs3.txt. [tid:22907805759040] 9.88 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs5.txt. [tid:22907803657792] 12.71 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs7.txt. [tid:22907801556544] 16.87 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs9.txt. [tid:22907799455296] 9.03 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs11.txt. [tid:22907797354048] 1.46 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs13.txt. [tid:22907795252800] 12.61 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs15.txt. [tid:22907793151552] 12.36 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs17.txt. [tid:22907791050304] 8.62 ms taken to read 65 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs19.txt. [tid:22907788949056] 13.24 ms taken to read 98 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs21.txt. [tid:22907786847808] 13.76 ms taken to read 135 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs23.txt. [tid:22907784746560] 27.93 ms taken to read 197 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs25.txt. [tid:22907782645312] 44.23 ms taken to read 270 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs27.txt. [tid:22907780544064] 12.07 ms taken to read 388 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs29.txt. [tid:22907778442816] 15.03 ms taken to read 551 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs31.txt. [tid:22907776341568] 28.30 ms taken to read 783 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs33.txt. [tid:22907774240320] 25.89 ms taken to read 1106 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs35.txt. [tid:22907772139072] 14.76 ms taken to read 1563 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs37.txt. [tid:22907770037824] 13.32 ms taken to read 2211 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs39.txt. [tid:22907767936576] 45.05 ms taken to read 3116 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs41.txt. [tid:22907765835328] 16.54 ms taken to read 4400 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs43.txt. [tid:22907763734080] 115.88 ms taken to read 6223 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs45.txt. [tid:22907761632832] 137.81 ms taken to read 8774 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs47.txt. [tid:22907759531584] 34.99 ms taken to read 12413 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs49.txt. [tid:22907757430336] 95.31 ms taken to read 17529 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs51.txt. [tid:22907755329088] 41.46 ms taken to read 24829 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs53.txt. [tid:22907753227840] 237.01 ms taken to read 35088 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs55.txt. [tid:22907751126592] 152.36 ms taken to read 49805 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs57.txt. [tid:22907749025344] 226.04 ms taken to read 70539 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs59.txt. [tid:22905933002304] 279.33 ms taken to read 100323 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs61.txt. [tid:22905796683328] 316.12 ms taken to read 142420 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs63.txt. [tid:22905664566848] 651.95 ms taken to read 202794 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs65.txt. [tid:22905930901056] 664.46 ms taken to read 288534 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs67.txt. [tid:22905928799808] 727.16 ms taken to read 411654 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs69.txt. [tid:22905926698560] 1251.14 ms (1 s 251.14 ms) taken to read 586547 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs71.txt. [tid:22905924597312] 1424.45 ms (1 s 424.44 ms) taken to read 837981 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs73.txt. [tid:22905922496064] 2816.36 ms (2 s 816.36 ms) taken to read 1196203 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs75.txt. [tid:22905920394816] 2979.77 ms (2 s 979.77 ms) taken to read 1710627 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs77.txt. [tid:22905918293568] 2080.37 ms (2 s 80.37 ms) taken to read 2444582 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs79.txt. [tid:22905916192320] 3223.44 ms (3 s 223.44 ms) taken to read 3499861 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81.txt. [tid:22905914091072] 3591.18 ms (3 s 591.18 ms) taken to read 5006994 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83.txt. [tid:22905911989824] 3687.20 ms (3 s 687.20 ms) total read duration. Loaded 42 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 65 21 : 98 23 : 135 25 : 197 27 : 270 29 : 388 31 : 551 33 : 783 35 : 1106 37 : 1563 39 : 2211 41 : 3116 43 : 4400 45 : 6223 47 : 8774 49 : 12413 51 : 17529 53 : 24829 55 : 35088 57 : 49805 59 : 70539 61 : 100323 63 : 142420 65 : 202794 67 : 288534 69 : 411654 71 : 586547 73 : 837981 75 : 1196203 77 : 1710627 79 : 2444582 81 : 3499861 83 : 5006994 16668725 representatives in total. Wed May 27 11:23:40 2026: Inserted ≈ 5% of D-proof conclusions. [ 833436 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 905.84 ms remaining ; 3 s 58.78 ms total) Wed May 27 11:23:40 2026: Inserted ≈10% of D-proof conclusions. [ 1666872 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 678.69 ms remaining ; 2 s 976.32 ms total) Wed May 27 11:23:40 2026: Inserted ≈15% of D-proof conclusions. [ 2500308 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 567.24 ms remaining ; 3 s 20.29 ms total) Wed May 27 11:23:41 2026: Inserted ≈20% of D-proof conclusions. [ 3333745 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 405.36 ms remaining ; 3 s 6.70 ms total) Wed May 27 11:23:41 2026: Inserted ≈25% of D-proof conclusions. [ 4167181 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 306.12 ms remaining ; 3 s 74.83 ms total) Wed May 27 11:23:41 2026: Inserted ≈30% of D-proof conclusions. [ 5000617 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 185.47 ms remaining ; 3 s 122.10 ms total) Wed May 27 11:23:41 2026: Inserted ≈35% of D-proof conclusions. [ 5834053 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 2 s 46.20 ms remaining ; 3 s 148.00 ms total) Wed May 27 11:23:41 2026: Inserted ≈40% of D-proof conclusions. [ 6667490 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 899.06 ms remaining ; 3 s 165.10 ms total) Wed May 27 11:23:41 2026: Inserted ≈45% of D-proof conclusions. [ 7500926 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 828.11 ms remaining ; 3 s 323.83 ms total) Wed May 27 11:23:42 2026: Inserted ≈50% of D-proof conclusions. [ 8334362 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 674.49 ms remaining ; 3 s 348.98 ms total) Wed May 27 11:23:42 2026: Inserted ≈55% of D-proof conclusions. [ 9167798 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 516.56 ms remaining ; 3 s 370.12 ms total) Wed May 27 11:23:42 2026: Inserted ≈60% of D-proof conclusions. [10001235 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 350.00 ms remaining ; 3 s 374.99 ms total) Wed May 27 11:23:42 2026: Inserted ≈65% of D-proof conclusions. [10834671 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 186.02 ms remaining ; 3 s 388.64 ms total) Wed May 27 11:23:42 2026: Inserted ≈70% of D-proof conclusions. [11668107 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 1 s 13.65 ms remaining ; 3 s 378.83 ms total) Wed May 27 11:23:43 2026: Inserted ≈75% of D-proof conclusions. [12501543 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 862.19 ms remaining ; 3 s 448.76 ms total) Wed May 27 11:23:43 2026: Inserted ≈80% of D-proof conclusions. [13334980 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 692.63 ms remaining ; 3 s 463.18 ms total) Wed May 27 11:23:43 2026: Inserted ≈85% of D-proof conclusions. [14168416 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 518.91 ms remaining ; 3 s 459.43 ms total) Wed May 27 11:23:43 2026: Inserted ≈90% of D-proof conclusions. [15001852 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 345.94 ms remaining ; 3 s 459.44 ms total) Wed May 27 11:23:43 2026: Inserted ≈95% of D-proof conclusions. [15835288 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 172.78 ms remaining ; 3 s 455.58 ms total) Wed May 27 11:23:43 2026: Inserted 100% of D-proof conclusions. [16668725 of 16668725] (ETC: Wed May 27 11:23:43 2026 ; 0.00 ms remaining ; 3 s 488.48 ms total) 3488.66 ms (3 s 488.66 ms) total insertion duration. Determined the number of proof string candidates for iteration as 477079792. [most relevant: {21,63} with 2*13957160 = 27914320, i.e. ≈5.85%] Wed May 27 11:23:43 2026: Starting to generate D-proof representatives of length 85. Wed May 27 11:24:56 2026: Iterated ≈ 2% of D-proof candidates. [ 9541595 of 477079792] (ETC: Wed May 27 12:24:10 2026 ; 59 min 14 s 369.33 ms remaining ; 1 h 26 s 907.47 ms total) Wed May 27 11:26:27 2026: Iterated ≈ 4% of D-proof candidates. [ 19083191 of 477079792] (ETC: Wed May 27 12:31:52 2026 ; 1 h 5 min 24 s 942.63 ms remaining ; 1 h 8 min 8 s 481.89 ms total) Wed May 27 11:27:40 2026: Iterated ≈ 6% of D-proof candidates. [ 28624787 of 477079792] (ETC: Wed May 27 12:29:28 2026 ; 1 h 1 min 48 s 215.75 ms remaining ; 1 h 5 min 44 s 910.37 ms total) Wed May 27 11:29:03 2026: Iterated ≈ 8% of D-proof candidates. [ 38166383 of 477079792] (ETC: Wed May 27 12:30:16 2026 ; 1 h 1 min 13 s 209.76 ms remaining ; 1 h 6 min 32 s 619.30 ms total) Wed May 27 11:30:10 2026: Iterated ≈10% of D-proof candidates. [ 47707979 of 477079792] (ETC: Wed May 27 12:28:12 2026 ; 58 min 2 s 130.48 ms remaining ; 1 h 4 min 29 s 33.87 ms total) Wed May 27 11:31:38 2026: Iterated ≈12% of D-proof candidates. [ 57249575 of 477079792] (ETC: Wed May 27 12:29:39 2026 ; 58 min 1 s 169.98 ms remaining ; 1 h 5 min 55 s 874.98 ms total) Wed May 27 11:32:44 2026: Iterated ≈14% of D-proof candidates. [ 66791170 of 477079792] (ETC: Wed May 27 12:28:04 2026 ; 55 min 19 s 910.45 ms remaining ; 1 h 4 min 20 s 360.98 ms total) Wed May 27 11:34:02 2026: Iterated ≈16% of D-proof candidates. [ 76332766 of 477079792] (ETC: Wed May 27 12:28:10 2026 ; 54 min 7 s 562.58 ms remaining ; 1 h 4 min 26 s 145.92 ms total) Wed May 27 11:35:15 2026: Iterated ≈18% of D-proof candidates. [ 85874362 of 477079792] (ETC: Wed May 27 12:27:48 2026 ; 52 min 32 s 440.90 ms remaining ; 1 h 4 min 4 s 440.11 ms total) Wed May 27 11:36:24 2026: Iterated ≈20% of D-proof candidates. [ 95415958 of 477079792] (ETC: Wed May 27 12:27:05 2026 ; 50 min 41 s 8.61 ms remaining ; 1 h 3 min 21 s 260.75 ms total) Wed May 27 11:37:50 2026: Iterated ≈22% of D-proof candidates. [104957554 of 477079792] (ETC: Wed May 27 12:27:53 2026 ; 50 min 2 s 306.84 ms remaining ; 1 h 4 min 9 s 111.34 ms total) Wed May 27 11:38:51 2026: Iterated ≈24% of D-proof candidates. [114499150 of 477079792] (ETC: Wed May 27 12:26:46 2026 ; 47 min 54 s 422.87 ms remaining ; 1 h 3 min 2 s 135.35 ms total) Wed May 27 11:40:06 2026: Iterated ≈26% of D-proof candidates. [124040745 of 477079792] (ETC: Wed May 27 12:26:42 2026 ; 46 min 36 s 174.09 ms remaining ; 1 h 2 min 58 s 613.62 ms total) Wed May 27 11:41:23 2026: Iterated ≈28% of D-proof candidates. [133582341 of 477079792] (ETC: Wed May 27 12:26:48 2026 ; 45 min 25 s 80.48 ms remaining ; 1 h 3 min 4 s 833.99 ms total) Wed May 27 11:42:29 2026: Iterated ≈30% of D-proof candidates. [143123937 of 477079792] (ETC: Wed May 27 12:26:17 2026 ; 43 min 47 s 370.71 ms remaining ; 1 h 2 min 33 s 386.72 ms total) Wed May 27 11:43:42 2026: Iterated ≈32% of D-proof candidates. [152665533 of 477079792] (ETC: Wed May 27 12:26:09 2026 ; 42 min 26 s 861.71 ms remaining ; 1 h 2 min 25 s 384.87 ms total) Wed May 27 11:44:41 2026: Iterated ≈34% of D-proof candidates. [162207129 of 477079792] (ETC: Wed May 27 12:25:22 2026 ; 40 min 40 s 936.12 ms remaining ; 1 h 1 min 38 s 388.05 ms total) Wed May 27 11:45:50 2026: Iterated ≈36% of D-proof candidates. [171748725 of 477079792] (ETC: Wed May 27 12:25:07 2026 ; 39 min 17 s 457.39 ms remaining ; 1 h 1 min 23 s 527.17 ms total) Wed May 27 11:47:04 2026: Iterated ≈38% of D-proof candidates. [181290320 of 477079792] (ETC: Wed May 27 12:25:09 2026 ; 38 min 5 s 358.36 ms remaining ; 1 h 1 min 26 s 61.86 ms total) Wed May 27 11:48:06 2026: Iterated ≈40% of D-proof candidates. [190831916 of 477079792] (ETC: Wed May 27 12:24:39 2026 ; 36 min 33 s 357.43 ms remaining ; 1 h 55 s 595.70 ms total) Wed May 27 11:49:16 2026: Iterated ≈42% of D-proof candidates. [200373512 of 477079792] (ETC: Wed May 27 12:24:32 2026 ; 35 min 15 s 906.70 ms remaining ; 1 h 48 s 114.99 ms total) Wed May 27 11:50:18 2026: Iterated ≈44% of D-proof candidates. [209915108 of 477079792] (ETC: Wed May 27 12:24:06 2026 ; 33 min 48 s 857.13 ms remaining ; 1 h 22 s 959.16 ms total) Wed May 27 11:51:26 2026: Iterated ≈46% of D-proof candidates. [219456704 of 477079792] (ETC: Wed May 27 12:23:59 2026 ; 32 min 32 s 202.51 ms remaining ; 1 h 15 s 189.82 ms total) Wed May 27 11:52:35 2026: Iterated ≈48% of D-proof candidates. [228998300 of 477079792] (ETC: Wed May 27 12:23:50 2026 ; 31 min 15 s 643.38 ms remaining ; 1 h 7 s 6.50 ms total) Wed May 27 11:53:46 2026: Iterated ≈50% of D-proof candidates. [238539896 of 477079792] (ETC: Wed May 27 12:23:48 2026 ; 30 min 2 s 506.03 ms remaining ; 1 h 5 s 12.05 ms total) Wed May 27 11:54:50 2026: Iterated ≈52% of D-proof candidates. [248081491 of 477079792] (ETC: Wed May 27 12:23:32 2026 ; 28 min 42 s 726.97 ms remaining ; 59 min 49 s 14.51 ms total) Wed May 27 11:56:01 2026: Iterated ≈54% of D-proof candidates. [257623087 of 477079792] (ETC: Wed May 27 12:23:32 2026 ; 27 min 30 s 894.93 ms remaining ; 59 min 48 s 902.00 ms total) Wed May 27 11:57:12 2026: Iterated ≈56% of D-proof candidates. [267164683 of 477079792] (ETC: Wed May 27 12:23:30 2026 ; 26 min 18 s 36.13 ms remaining ; 59 min 46 s 445.74 ms total) Wed May 27 11:58:19 2026: Iterated ≈58% of D-proof candidates. [276706279 of 477079792] (ETC: Wed May 27 12:23:22 2026 ; 25 min 3 s 74.41 ms remaining ; 59 min 38 s 748.60 ms total) Wed May 27 11:59:37 2026: Iterated ≈60% of D-proof candidates. [286247875 of 477079792] (ETC: Wed May 27 12:23:32 2026 ; 23 min 55 s 603.91 ms remaining ; 59 min 49 s 9.77 ms total) Wed May 27 12:00:45 2026: Iterated ≈62% of D-proof candidates. [295789471 of 477079792] (ETC: Wed May 27 12:23:26 2026 ; 22 min 41 s 500.02 ms remaining ; 59 min 42 s 894.79 ms total) Wed May 27 12:01:50 2026: Iterated ≈64% of D-proof candidates. [305331066 of 477079792] (ETC: Wed May 27 12:23:16 2026 ; 21 min 26 s 217.01 ms remaining ; 59 min 32 s 825.00 ms total) Wed May 27 12:03:04 2026: Iterated ≈66% of D-proof candidates. [314872662 of 477079792] (ETC: Wed May 27 12:23:20 2026 ; 20 min 15 s 948.77 ms remaining ; 59 min 36 s 319.90 ms total) Wed May 27 12:04:12 2026: Iterated ≈68% of D-proof candidates. [324414258 of 477079792] (ETC: Wed May 27 12:23:15 2026 ; 19 min 3 s 15.20 ms remaining ; 59 min 31 s 922.49 ms total) Wed May 27 12:05:23 2026: Iterated ≈70% of D-proof candidates. [333955854 of 477079792] (ETC: Wed May 27 12:23:15 2026 ; 17 min 51 s 441.03 ms remaining ; 59 min 31 s 470.10 ms total) Wed May 27 12:06:34 2026: Iterated ≈72% of D-proof candidates. [343497450 of 477079792] (ETC: Wed May 27 12:23:14 2026 ; 16 min 39 s 838.94 ms remaining ; 59 min 30 s 853.35 ms total) Wed May 27 12:07:43 2026: Iterated ≈74% of D-proof candidates. [353039046 of 477079792] (ETC: Wed May 27 12:23:11 2026 ; 15 min 27 s 477.14 ms remaining ; 59 min 27 s 219.79 ms total) Wed May 27 12:08:53 2026: Iterated ≈76% of D-proof candidates. [362580641 of 477079792] (ETC: Wed May 27 12:23:09 2026 ; 14 min 15 s 633.91 ms remaining ; 59 min 25 s 141.27 ms total) Wed May 27 12:10:04 2026: Iterated ≈78% of D-proof candidates. [372122237 of 477079792] (ETC: Wed May 27 12:23:08 2026 ; 13 min 4 s 204.13 ms remaining ; 59 min 24 s 564.21 ms total) Wed May 27 12:11:12 2026: Iterated ≈80% of D-proof candidates. [381663833 of 477079792] (ETC: Wed May 27 12:23:04 2026 ; 11 min 52 s 204.00 ms remaining ; 59 min 21 s 20.00 ms total) Wed May 27 12:12:27 2026: Iterated ≈82% of D-proof candidates. [391205429 of 477079792] (ETC: Wed May 27 12:23:09 2026 ; 10 min 41 s 766.87 ms remaining ; 59 min 25 s 371.47 ms total) Wed May 27 12:13:40 2026: Iterated ≈84% of D-proof candidates. [400747025 of 477079792] (ETC: Wed May 27 12:23:11 2026 ; 9 min 30 s 863.99 ms remaining ; 59 min 27 s 899.89 ms total) Wed May 27 12:14:49 2026: Iterated ≈86% of D-proof candidates. [410288621 of 477079792] (ETC: Wed May 27 12:23:08 2026 ; 8 min 19 s 43.12 ms remaining ; 59 min 24 s 593.68 ms total) Wed May 27 12:16:02 2026: Iterated ≈88% of D-proof candidates. [419830216 of 477079792] (ETC: Wed May 27 12:23:10 2026 ; 7 min 8 s 35.90 ms remaining ; 59 min 26 s 965.79 ms total) Wed May 27 12:17:16 2026: Iterated ≈90% of D-proof candidates. [429371812 of 477079792] (ETC: Wed May 27 12:23:13 2026 ; 5 min 56 s 991.70 ms remaining ; 59 min 29 s 916.90 ms total) Wed May 27 12:18:25 2026: Iterated ≈92% of D-proof candidates. [438913408 of 477079792] (ETC: Wed May 27 12:23:11 2026 ; 4 min 45 s 385.47 ms remaining ; 59 min 27 s 318.32 ms total) Wed May 27 12:19:33 2026: Iterated ≈94% of D-proof candidates. [448455004 of 477079792] (ETC: Wed May 27 12:23:07 2026 ; 3 min 33 s 814.28 ms remaining ; 59 min 23 s 571.21 ms total) Wed May 27 12:20:40 2026: Iterated ≈96% of D-proof candidates. [457996600 of 477079792] (ETC: Wed May 27 12:23:03 2026 ; 2 min 22 s 369.20 ms remaining ; 59 min 19 s 229.97 ms total) Wed May 27 12:21:53 2026: Iterated ≈98% of D-proof candidates. [467538196 of 477079792] (ETC: Wed May 27 12:23:04 2026 ; 1 min 11 s 217.96 ms remaining ; 59 min 20 s 897.95 ms total) Wed May 27 12:23:00 2026: Iterated 100% of D-proof candidates. [477079792 of 477079792] (ETC: Wed May 27 12:23:00 2026 ; 0.00 ms remaining ; 59 min 16 s 188.36 ms total) 3556767.81 ms (59 min 16 s 767.81 ms) taken to collect 68838412 D-proofs of length 85. [iterated 477079792 condensed detachment proof strings] 282442.30 ms (4 min 42 s 442.30 ms) taken to filter and order new representative proofs. Found 68838412 representative, 381691542 redundant, and 26549838 invalid condensed detachment proof strings. lengths up to 85 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,8), (11,14), (13,21), (15,31), (17,42), (19,65), (21,98), (23,135), (25,197), (27,270), (29,388), (31,551), (33,783), (35,1106), (37,1563), (39,2211), (41,3116), (43,4400), (45,6223), (47,8774), (49,12413), (51,17529), (53,24829), (55,35088), (57,49805), (59,70539), (61,100323), (63,142420), (65,202794), (67,288534), (69,411654), (71,586547), (73,837981), (75,1196203), (77,1710627), (79,2444582), (81,3499861), (83,5006994), (85,68838412)} ; 68838412 new representative proofs (381691542 redundant, 26549838 invalid) Wed May 27 12:27:43 2026: Starting to write 68838412 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs85-unfiltered85+.txt. 50539.55 ms (50 s 539.55 ms) taken to print and save 16028860749 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs85-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 820405980. [most relevant: {1,85} with 2*68838412 = 137676824, i.e. ≈16.78%] Wed May 27 12:29:37 2026: Starting to generate D-proof representatives of length 87. Wed May 27 12:32:15 2026: Iterated ≈ 2% of D-proof candidates. [ 16408119 of 820405980] (ETC: Wed May 27 14:41:06 2026 ; 2 h 8 min 50 s 919.33 ms remaining ; 2 h 11 min 28 s 693.19 ms total) Wed May 27 12:33:54 2026: Iterated ≈ 4% of D-proof candidates. [ 32816239 of 820405980] (ETC: Wed May 27 14:16:49 2026 ; 1 h 42 min 55 s 38.42 ms remaining ; 1 h 47 min 12 s 331.69 ms total) Wed May 27 12:35:41 2026: Iterated ≈ 6% of D-proof candidates. [ 49224358 of 820405980] (ETC: Wed May 27 14:10:37 2026 ; 1 h 34 min 56 s 52.63 ms remaining ; 1 h 40 min 59 s 630.45 ms total) Wed May 27 12:37:41 2026: Iterated ≈ 8% of D-proof candidates. [ 65632478 of 820405980] (ETC: Wed May 27 14:10:25 2026 ; 1 h 32 min 44 s 236.87 ms remaining ; 1 h 40 min 48 s 83.55 ms total) Wed May 27 12:39:36 2026: Iterated ≈10% of D-proof candidates. [ 82040598 of 820405980] (ETC: Wed May 27 14:09:29 2026 ; 1 h 29 min 52 s 463.50 ms remaining ; 1 h 39 min 51 s 626.11 ms total) Wed May 27 12:41:39 2026: Iterated ≈12% of D-proof candidates. [ 98448717 of 820405980] (ETC: Wed May 27 14:09:54 2026 ; 1 h 28 min 14 s 471.76 ms remaining ; 1 h 40 min 16 s 445.18 ms total) Wed May 27 12:43:48 2026: Iterated ≈14% of D-proof candidates. [114856837 of 820405980] (ETC: Wed May 27 14:10:56 2026 ; 1 h 27 min 7 s 972.28 ms remaining ; 1 h 41 min 19 s 37.53 ms total) Wed May 27 12:46:17 2026: Iterated ≈16% of D-proof candidates. [131264956 of 820405980] (ETC: Wed May 27 14:13:45 2026 ; 1 h 27 min 28 s 269.62 ms remaining ; 1 h 44 min 7 s 940.01 ms total) Wed May 27 12:48:50 2026: Iterated ≈18% of D-proof candidates. [147673076 of 820405980] (ETC: Wed May 27 14:16:21 2026 ; 1 h 27 min 30 s 945.22 ms remaining ; 1 h 46 min 43 s 591.73 ms total) Wed May 27 12:51:07 2026: Iterated ≈20% of D-proof candidates. [164081196 of 820405980] (ETC: Wed May 27 14:17:07 2026 ; 1 h 25 min 59 s 803.88 ms remaining ; 1 h 47 min 29 s 754.85 ms total) Wed May 27 12:53:19 2026: Iterated ≈22% of D-proof candidates. [180489315 of 820405980] (ETC: Wed May 27 14:17:18 2026 ; 1 h 23 min 59 s 451.41 ms remaining ; 1 h 47 min 40 s 835.14 ms total) Wed May 27 12:55:14 2026: Iterated ≈24% of D-proof candidates. [196897435 of 820405980] (ETC: Wed May 27 14:16:22 2026 ; 1 h 21 min 7 s 556.76 ms remaining ; 1 h 46 min 44 s 679.95 ms total) Wed May 27 12:57:33 2026: Iterated ≈26% of D-proof candidates. [213305554 of 820405980] (ETC: Wed May 27 14:17:02 2026 ; 1 h 19 min 29 s 475.39 ms remaining ; 1 h 47 min 25 s 237.00 ms total) Wed May 27 12:59:40 2026: Iterated ≈28% of D-proof candidates. [229713674 of 820405980] (ETC: Wed May 27 14:16:58 2026 ; 1 h 17 min 17 s 143.88 ms remaining ; 1 h 47 min 20 s 477.61 ms total) Wed May 27 13:01:58 2026: Iterated ≈30% of D-proof candidates. [246121794 of 820405980] (ETC: Wed May 27 14:17:28 2026 ; 1 h 15 min 29 s 612.50 ms remaining ; 1 h 47 min 50 s 875.01 ms total) Wed May 27 13:03:45 2026: Iterated ≈32% of D-proof candidates. [262529913 of 820405980] (ETC: Wed May 27 14:16:17 2026 ; 1 h 12 min 31 s 772.46 ms remaining ; 1 h 46 min 39 s 665.37 ms total) Wed May 27 13:06:14 2026: Iterated ≈34% of D-proof candidates. [278938033 of 820405980] (ETC: Wed May 27 14:17:18 2026 ; 1 h 11 min 4 s 0.61 ms remaining ; 1 h 47 min 40 s 606.99 ms total) Wed May 27 13:08:24 2026: Iterated ≈36% of D-proof candidates. [295346152 of 820405980] (ETC: Wed May 27 14:17:20 2026 ; 1 h 8 min 56 s 82.64 ms remaining ; 1 h 47 min 42 s 629.11 ms total) Wed May 27 13:10:39 2026: Iterated ≈38% of D-proof candidates. [311754272 of 820405980] (ETC: Wed May 27 14:17:36 2026 ; 1 h 6 min 57 s 65.25 ms remaining ; 1 h 47 min 59 s 137.50 ms total) Wed May 27 13:12:27 2026: Iterated ≈40% of D-proof candidates. [328162392 of 820405980] (ETC: Wed May 27 14:16:43 2026 ; 1 h 4 min 15 s 490.94 ms remaining ; 1 h 47 min 5 s 818.23 ms total) Wed May 27 13:14:51 2026: Iterated ≈42% of D-proof candidates. [344570511 of 820405980] (ETC: Wed May 27 14:17:19 2026 ; 1 h 2 min 28 s 153.62 ms remaining ; 1 h 47 min 42 s 333.81 ms total) Wed May 27 13:16:36 2026: Iterated ≈44% of D-proof candidates. [360978631 of 820405980] (ETC: Wed May 27 14:16:24 2026 ; 59 min 48 s 33.65 ms remaining ; 1 h 46 min 47 s 202.95 ms total) Wed May 27 13:18:49 2026: Iterated ≈46% of D-proof candidates. [377386750 of 820405980] (ETC: Wed May 27 14:16:35 2026 ; 57 min 45 s 630.19 ms remaining ; 1 h 46 min 57 s 833.67 ms total) Wed May 27 13:20:44 2026: Iterated ≈48% of D-proof candidates. [393794870 of 820405980] (ETC: Wed May 27 14:16:06 2026 ; 55 min 22 s 424.74 ms remaining ; 1 h 46 min 29 s 278.34 ms total) Wed May 27 13:22:53 2026: Iterated ≈50% of D-proof candidates. [410202990 of 820405980] (ETC: Wed May 27 14:16:09 2026 ; 53 min 15 s 854.94 ms remaining ; 1 h 46 min 31 s 709.88 ms total) Wed May 27 13:24:58 2026: Iterated ≈52% of D-proof candidates. [426611109 of 820405980] (ETC: Wed May 27 14:16:03 2026 ; 51 min 5 s 430.90 ms remaining ; 1 h 46 min 26 s 314.36 ms total) Wed May 27 13:26:57 2026: Iterated ≈54% of D-proof candidates. [443019229 of 820405980] (ETC: Wed May 27 14:15:47 2026 ; 48 min 49 s 921.63 ms remaining ; 1 h 46 min 9 s 394.85 ms total) Wed May 27 13:29:00 2026: Iterated ≈56% of D-proof candidates. [459427348 of 820405980] (ETC: Wed May 27 14:15:40 2026 ; 46 min 39 s 494.98 ms remaining ; 1 h 46 min 2 s 488.58 ms total) Wed May 27 13:31:00 2026: Iterated ≈58% of D-proof candidates. [475835468 of 820405980] (ETC: Wed May 27 14:15:26 2026 ; 44 min 26 s 720.48 ms remaining ; 1 h 45 min 49 s 334.47 ms total) Wed May 27 13:32:59 2026: Iterated ≈60% of D-proof candidates. [492243588 of 820405980] (ETC: Wed May 27 14:15:14 2026 ; 42 min 14 s 733.16 ms remaining ; 1 h 45 min 36 s 832.89 ms total) Wed May 27 13:35:04 2026: Iterated ≈62% of D-proof candidates. [508651707 of 820405980] (ETC: Wed May 27 14:15:11 2026 ; 40 min 6 s 876.14 ms remaining ; 1 h 45 min 33 s 884.57 ms total) Wed May 27 13:37:05 2026: Iterated ≈64% of D-proof candidates. [525059827 of 820405980] (ETC: Wed May 27 14:15:02 2026 ; 37 min 57 s 101.05 ms remaining ; 1 h 45 min 25 s 280.69 ms total) Wed May 27 13:39:13 2026: Iterated ≈66% of D-proof candidates. [541467946 of 820405980] (ETC: Wed May 27 14:15:05 2026 ; 35 min 51 s 421.82 ms remaining ; 1 h 45 min 27 s 711.22 ms total) Wed May 27 13:41:10 2026: Iterated ≈68% of D-proof candidates. [557876066 of 820405980] (ETC: Wed May 27 14:14:51 2026 ; 33 min 40 s 381.73 ms remaining ; 1 h 45 min 13 s 692.89 ms total) Wed May 27 13:43:10 2026: Iterated ≈70% of D-proof candidates. [574284186 of 820405980] (ETC: Wed May 27 14:14:42 2026 ; 31 min 31 s 330.01 ms remaining ; 1 h 45 min 4 s 433.35 ms total) Wed May 27 13:45:13 2026: Iterated ≈72% of D-proof candidates. [590692305 of 820405980] (ETC: Wed May 27 14:14:37 2026 ; 29 min 24 s 66.84 ms remaining ; 1 h 45 min 238.70 ms total) Wed May 27 13:47:26 2026: Iterated ≈74% of D-proof candidates. [607100425 of 820405980] (ETC: Wed May 27 14:14:46 2026 ; 27 min 20 s 292.77 ms remaining ; 1 h 45 min 8 s 818.33 ms total) Wed May 27 13:49:24 2026: Iterated ≈76% of D-proof candidates. [623508544 of 820405980] (ETC: Wed May 27 14:14:36 2026 ; 25 min 11 s 672.48 ms remaining ; 1 h 44 min 58 s 635.31 ms total) Wed May 27 13:51:27 2026: Iterated ≈78% of D-proof candidates. [639916664 of 820405980] (ETC: Wed May 27 14:14:32 2026 ; 23 min 4 s 781.57 ms remaining ; 1 h 44 min 54 s 461.66 ms total) Wed May 27 13:53:32 2026: Iterated ≈80% of D-proof candidates. [656324784 of 820405980] (ETC: Wed May 27 14:14:31 2026 ; 20 min 58 s 756.61 ms remaining ; 1 h 44 min 53 s 783.05 ms total) Wed May 27 13:55:29 2026: Iterated ≈82% of D-proof candidates. [672732903 of 820405980] (ETC: Wed May 27 14:14:20 2026 ; 18 min 50 s 959.67 ms remaining ; 1 h 44 min 43 s 109.27 ms total) Wed May 27 13:57:42 2026: Iterated ≈84% of D-proof candidates. [689141023 of 820405980] (ETC: Wed May 27 14:14:29 2026 ; 16 min 46 s 671.05 ms remaining ; 1 h 44 min 51 s 694.07 ms total) Wed May 27 13:59:42 2026: Iterated ≈86% of D-proof candidates. [705549142 of 820405980] (ETC: Wed May 27 14:14:21 2026 ; 14 min 39 s 798.50 ms remaining ; 1 h 44 min 44 s 274.99 ms total) Wed May 27 14:01:46 2026: Iterated ≈88% of D-proof candidates. [721957262 of 820405980] (ETC: Wed May 27 14:14:20 2026 ; 12 min 33 s 973.72 ms remaining ; 1 h 44 min 43 s 114.28 ms total) Wed May 27 14:03:53 2026: Iterated ≈90% of D-proof candidates. [738365382 of 820405980] (ETC: Wed May 27 14:14:21 2026 ; 10 min 28 s 385.35 ms remaining ; 1 h 44 min 43 s 853.51 ms total) Wed May 27 14:06:06 2026: Iterated ≈92% of D-proof candidates. [754773501 of 820405980] (ETC: Wed May 27 14:14:29 2026 ; 8 min 23 s 385.70 ms remaining ; 1 h 44 min 52 s 321.20 ms total) Wed May 27 14:08:12 2026: Iterated ≈94% of D-proof candidates. [771181621 of 820405980] (ETC: Wed May 27 14:14:30 2026 ; 6 min 17 s 549.02 ms remaining ; 1 h 44 min 52 s 483.69 ms total) Wed May 27 14:10:11 2026: Iterated ≈96% of D-proof candidates. [787589740 of 820405980] (ETC: Wed May 27 14:14:23 2026 ; 4 min 11 s 431.88 ms remaining ; 1 h 44 min 45 s 796.99 ms total) Wed May 27 14:12:24 2026: Iterated ≈98% of D-proof candidates. [803997860 of 820405980] (ETC: Wed May 27 14:14:30 2026 ; 2 min 5 s 860.22 ms remaining ; 1 h 44 min 53 s 11.06 ms total) Wed May 27 14:14:32 2026: Iterated 100% of D-proof candidates. [820405980 of 820405980] (ETC: Wed May 27 14:14:32 2026 ; 0.00 ms remaining ; 1 h 44 min 54 s 677.03 ms total) 6297065.91 ms (1 h 44 min 57 s 65.91 ms) taken to collect 170845717 D-proofs of length 87. [iterated 820405980 condensed detachment proof strings] 891790.83 ms (14 min 51 s 790.83 ms) taken to filter and order new representative proofs. Found 170845717 representative, 609764452 redundant, and 39795811 invalid condensed detachment proof strings. lengths up to 87 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,8), (11,14), (13,21), (15,31), (17,42), (19,65), (21,98), (23,135), (25,197), (27,270), (29,388), (31,551), (33,783), (35,1106), (37,1563), (39,2211), (41,3116), (43,4400), (45,6223), (47,8774), (49,12413), (51,17529), (53,24829), (55,35088), (57,49805), (59,70539), (61,100323), (63,142420), (65,202794), (67,288534), (69,411654), (71,586547), (73,837981), (75,1196203), (77,1710627), (79,2444582), (81,3499861), (83,5006994), (85,68838412), (87,170845717)} ; 170845717 new representative proofs (609764452 redundant, 39795811 invalid) Wed May 27 14:29:26 2026: Starting to write 170845717 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs87-unfiltered85+.txt. 139473.04 ms (2 min 19 s 473.04 ms) taken to print and save 41283300306 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs87-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 1462588378. [most relevant: {1,87} with 2*170845717 = 341691434, i.e. ≈23.36%] Wed May 27 14:35:11 2026: Starting to generate D-proof representatives of length 89. Wed May 27 14:41:46 2026: Iterated ≈ 2% of D-proof candidates. [ 29251767 of 1462588378] (ETC: Wed May 27 20:04:28 2026 ; 5 h 22 min 41 s 572.26 ms remaining ; 5 h 29 min 16 s 706.38 ms total) Wed May 27 14:46:40 2026: Iterated ≈ 4% of D-proof candidates. [ 58503535 of 1462588378] (ETC: Wed May 27 19:22:09 2026 ; 4 h 35 min 29 s 46.37 ms remaining ; 4 h 46 min 57 s 756.63 ms total) Wed May 27 14:50:43 2026: Iterated ≈ 6% of D-proof candidates. [ 87755302 of 1462588378] (ETC: Wed May 27 18:54:07 2026 ; 4 h 3 min 23 s 658.64 ms remaining ; 4 h 18 min 55 s 807.05 ms total) Wed May 27 14:54:00 2026: Iterated ≈ 8% of D-proof candidates. [ 117007070 of 1462588378] (ETC: Wed May 27 18:30:23 2026 ; 3 h 36 min 22 s 465.42 ms remaining ; 3 h 55 min 11 s 375.45 ms total) Wed May 27 14:58:32 2026: Iterated ≈10% of D-proof candidates. [ 146258837 of 1462588378] (ETC: Wed May 27 18:28:41 2026 ; 3 h 30 min 8 s 475.48 ms remaining ; 3 h 53 min 29 s 417.20 ms total) Wed May 27 15:02:47 2026: Iterated ≈12% of D-proof candidates. [ 175510605 of 1462588378] (ETC: Wed May 27 18:25:13 2026 ; 3 h 22 min 25 s 395.10 ms remaining ; 3 h 50 min 1 s 585.34 ms total) Wed May 27 15:06:47 2026: Iterated ≈14% of D-proof candidates. [ 204762372 of 1462588378] (ETC: Wed May 27 18:20:52 2026 ; 3 h 14 min 4 s 907.66 ms remaining ; 3 h 45 min 40 s 590.30 ms total) Wed May 27 15:10:44 2026: Iterated ≈16% of D-proof candidates. [ 234014140 of 1462588378] (ETC: Wed May 27 18:17:22 2026 ; 3 h 6 min 37 s 656.45 ms remaining ; 3 h 42 min 10 s 543.39 ms total) Wed May 27 15:15:14 2026: Iterated ≈18% of D-proof candidates. [ 263265908 of 1462588378] (ETC: Wed May 27 18:17:39 2026 ; 3 h 2 min 25 s 328.51 ms remaining ; 3 h 42 min 27 s 961.60 ms total) Wed May 27 15:19:39 2026: Iterated ≈20% of D-proof candidates. [ 292517675 of 1462588378] (ETC: Wed May 27 18:17:32 2026 ; 2 h 57 min 52 s 504.02 ms remaining ; 3 h 42 min 20 s 630.02 ms total) Wed May 27 15:24:15 2026: Iterated ≈22% of D-proof candidates. [ 321769443 of 1462588378] (ETC: Wed May 27 18:18:13 2026 ; 2 h 53 min 57 s 575.07 ms remaining ; 3 h 43 min 1 s 506.49 ms total) Wed May 27 15:29:11 2026: Iterated ≈24% of D-proof candidates. [ 351021210 of 1462588378] (ETC: Wed May 27 18:20:09 2026 ; 2 h 50 min 58 s 244.08 ms remaining ; 3 h 44 min 57 s 689.57 ms total) Wed May 27 15:32:50 2026: Iterated ≈26% of D-proof candidates. [ 380272978 of 1462588378] (ETC: Wed May 27 18:16:53 2026 ; 2 h 44 min 3 s 296.21 ms remaining ; 3 h 41 min 41 s 751.63 ms total) Wed May 27 15:37:00 2026: Iterated ≈28% of D-proof candidates. [ 409524745 of 1462588378] (ETC: Wed May 27 18:15:57 2026 ; 2 h 38 min 57 s 266.84 ms remaining ; 3 h 40 min 46 s 203.94 ms total) Wed May 27 15:41:38 2026: Iterated ≈30% of D-proof candidates. [ 438776513 of 1462588378] (ETC: Wed May 27 18:16:40 2026 ; 2 h 35 min 1 s 818.63 ms remaining ; 3 h 41 min 28 s 312.32 ms total) Wed May 27 15:46:33 2026: Iterated ≈32% of D-proof candidates. [ 468028280 of 1462588378] (ETC: Wed May 27 18:18:12 2026 ; 2 h 31 min 38 s 582.23 ms remaining ; 3 h 43 min 267.97 ms total) Wed May 27 15:51:09 2026: Iterated ≈34% of D-proof candidates. [ 497280048 of 1462588378] (ETC: Wed May 27 18:18:36 2026 ; 2 h 27 min 26 s 902.59 ms remaining ; 3 h 43 min 24 s 397.86 ms total) Wed May 27 15:55:14 2026: Iterated ≈36% of D-proof candidates. [ 526531816 of 1462588378] (ETC: Wed May 27 18:17:31 2026 ; 2 h 22 min 17 s 358.67 ms remaining ; 3 h 42 min 19 s 622.92 ms total) Wed May 27 15:59:17 2026: Iterated ≈38% of D-proof candidates. [ 555783583 of 1462588378] (ETC: Wed May 27 18:16:30 2026 ; 2 h 17 min 12 s 793.54 ms remaining ; 3 h 41 min 18 s 699.25 ms total) Wed May 27 16:03:34 2026: Iterated ≈40% of D-proof candidates. [ 585035351 of 1462588378] (ETC: Wed May 27 18:16:08 2026 ; 2 h 12 min 33 s 863.81 ms remaining ; 3 h 40 min 56 s 439.68 ms total) Wed May 27 16:08:01 2026: Iterated ≈42% of D-proof candidates. [ 614287118 of 1462588378] (ETC: Wed May 27 18:16:12 2026 ; 2 h 8 min 11 s 86.94 ms remaining ; 3 h 41 min 494.71 ms total) Wed May 27 16:11:46 2026: Iterated ≈44% of D-proof candidates. [ 643538886 of 1462588378] (ETC: Wed May 27 18:14:40 2026 ; 2 h 2 min 54 s 557.34 ms remaining ; 3 h 39 min 28 s 852.38 ms total) Wed May 27 16:16:05 2026: Iterated ≈46% of D-proof candidates. [ 672790653 of 1462588378] (ETC: Wed May 27 18:14:31 2026 ; 1 h 58 min 26 s 60.95 ms remaining ; 3 h 39 min 19 s 372.12 ms total) Wed May 27 16:20:03 2026: Iterated ≈48% of D-proof candidates. [ 702042421 of 1462588378] (ETC: Wed May 27 18:13:38 2026 ; 1 h 53 min 35 s 591.75 ms remaining ; 3 h 38 min 26 s 907.21 ms total) Wed May 27 16:23:58 2026: Iterated ≈50% of D-proof candidates. [ 731294189 of 1462588378] (ETC: Wed May 27 18:12:45 2026 ; 1 h 48 min 46 s 776.43 ms remaining ; 3 h 37 min 33 s 552.86 ms total) Wed May 27 16:28:21 2026: Iterated ≈52% of D-proof candidates. [ 760545956 of 1462588378] (ETC: Wed May 27 18:12:48 2026 ; 1 h 44 min 27 s 370.10 ms remaining ; 3 h 37 min 37 s 21.03 ms total) Wed May 27 16:32:06 2026: Iterated ≈54% of D-proof candidates. [ 789797724 of 1462588378] (ETC: Wed May 27 18:11:42 2026 ; 1 h 39 min 35 s 590.19 ms remaining ; 3 h 36 min 30 s 413.46 ms total) Wed May 27 16:35:32 2026: Iterated ≈56% of D-proof candidates. [ 819049491 of 1462588378] (ETC: Wed May 27 18:10:05 2026 ; 1 h 34 min 33 s 61.16 ms remaining ; 3 h 34 min 53 s 320.81 ms total) Wed May 27 16:39:36 2026: Iterated ≈58% of D-proof candidates. [ 848301259 of 1462588378] (ETC: Wed May 27 18:09:41 2026 ; 1 h 30 min 5 s 368.63 ms remaining ; 3 h 34 min 29 s 925.31 ms total) Wed May 27 16:44:01 2026: Iterated ≈60% of D-proof candidates. [ 877553026 of 1462588378] (ETC: Wed May 27 18:09:54 2026 ; 1 h 25 min 53 s 193.91 ms remaining ; 3 h 34 min 42 s 984.77 ms total) Wed May 27 16:48:05 2026: Iterated ≈62% of D-proof candidates. [ 906804794 of 1462588378] (ETC: Wed May 27 18:09:32 2026 ; 1 h 21 min 27 s 208.94 ms remaining ; 3 h 34 min 21 s 76.15 ms total) Wed May 27 16:51:48 2026: Iterated ≈64% of D-proof candidates. [ 936056561 of 1462588378] (ETC: Wed May 27 18:08:38 2026 ; 1 h 16 min 50 s 442.12 ms remaining ; 3 h 33 min 26 s 783.63 ms total) Wed May 27 16:55:30 2026: Iterated ≈66% of D-proof candidates. [ 965308329 of 1462588378] (ETC: Wed May 27 18:07:47 2026 ; 1 h 12 min 17 s 75.73 ms remaining ; 3 h 32 min 36 s 105.09 ms total) Wed May 27 16:59:21 2026: Iterated ≈68% of D-proof candidates. [ 994560097 of 1462588378] (ETC: Wed May 27 18:07:11 2026 ; 1 h 7 min 50 s 234.82 ms remaining ; 3 h 31 min 59 s 483.82 ms total) Wed May 27 17:03:12 2026: Iterated ≈70% of D-proof candidates. [1023811864 of 1462588378] (ETC: Wed May 27 18:06:38 2026 ; 1 h 3 min 26 s 155.59 ms remaining ; 3 h 31 min 27 s 185.27 ms total) Wed May 27 17:07:04 2026: Iterated ≈72% of D-proof candidates. [1053063632 of 1462588378] (ETC: Wed May 27 18:06:08 2026 ; 59 min 3 s 832.27 ms remaining ; 3 h 30 min 56 s 543.82 ms total) Wed May 27 17:11:17 2026: Iterated ≈74% of D-proof candidates. [1082315399 of 1462588378] (ETC: Wed May 27 18:06:08 2026 ; 54 min 50 s 819.18 ms remaining ; 3 h 30 min 56 s 996.83 ms total) Wed May 27 17:15:01 2026: Iterated ≈76% of D-proof candidates. [1111567167 of 1462588378] (ETC: Wed May 27 18:05:29 2026 ; 50 min 28 s 329.54 ms remaining ; 3 h 30 min 18 s 39.72 ms total) Wed May 27 17:18:59 2026: Iterated ≈78% of D-proof candidates. [1140818934 of 1462588378] (ETC: Wed May 27 18:05:11 2026 ; 46 min 11 s 965.96 ms remaining ; 3 h 29 min 59 s 845.23 ms total) Wed May 27 17:22:47 2026: Iterated ≈80% of D-proof candidates. [1170070702 of 1462588378] (ETC: Wed May 27 18:04:40 2026 ; 41 min 53 s 841.48 ms remaining ; 3 h 29 min 29 s 207.39 ms total) Wed May 27 17:26:40 2026: Iterated ≈82% of D-proof candidates. [1199322469 of 1462588378] (ETC: Wed May 27 18:04:19 2026 ; 37 min 38 s 558.21 ms remaining ; 3 h 29 min 7 s 545.56 ms total) Wed May 27 17:30:47 2026: Iterated ≈84% of D-proof candidates. [1228574237 of 1462588378] (ETC: Wed May 27 18:04:14 2026 ; 33 min 26 s 767.92 ms remaining ; 3 h 29 min 2 s 299.45 ms total) Wed May 27 17:34:50 2026: Iterated ≈86% of D-proof candidates. [1257826005 of 1462588378] (ETC: Wed May 27 18:04:05 2026 ; 29 min 14 s 718.76 ms remaining ; 3 h 28 min 53 s 705.40 ms total) Wed May 27 17:38:59 2026: Iterated ≈88% of D-proof candidates. [1287077772 of 1462588378] (ETC: Wed May 27 18:04:02 2026 ; 25 min 3 s 743.15 ms remaining ; 3 h 28 min 51 s 192.86 ms total) Wed May 27 17:43:12 2026: Iterated ≈90% of D-proof candidates. [1316329540 of 1462588378] (ETC: Wed May 27 18:04:06 2026 ; 20 min 53 s 460.50 ms remaining ; 3 h 28 min 54 s 604.95 ms total) Wed May 27 17:47:25 2026: Iterated ≈92% of D-proof candidates. [1345581307 of 1462588378] (ETC: Wed May 27 18:04:08 2026 ; 16 min 42 s 912.21 ms remaining ; 3 h 28 min 56 s 402.56 ms total) Wed May 27 17:51:09 2026: Iterated ≈94% of D-proof candidates. [1374833075 of 1462588378] (ETC: Wed May 27 18:03:39 2026 ; 12 min 30 s 475.14 ms remaining ; 3 h 28 min 27 s 918.90 ms total) Wed May 27 17:55:00 2026: Iterated ≈96% of D-proof candidates. [1404084842 of 1462588378] (ETC: Wed May 27 18:03:20 2026 ; 8 min 19 s 539.63 ms remaining ; 3 h 28 min 8 s 490.69 ms total) Wed May 27 17:58:53 2026: Iterated ≈98% of D-proof candidates. [1433336610 of 1462588378] (ETC: Wed May 27 18:03:02 2026 ; 4 min 9 s 420.06 ms remaining ; 3 h 27 min 51 s 2.91 ms total) Wed May 27 18:03:12 2026: Iterated 100% of D-proof candidates. [1462588378 of 1462588378] (ETC: Wed May 27 18:03:12 2026 ; 0.00 ms remaining ; 3 h 28 min 621.77 ms total) 12486431.29 ms (3 h 28 min 6 s 431.30 ms) taken to collect 335691857 D-proofs of length 89. [iterated 1462588378 condensed detachment proof strings] 2369014.76 ms (39 min 29 s 14.76 ms) taken to filter and order new representative proofs. Found 335691857 representative, 1056027538 redundant, and 70868983 invalid condensed detachment proof strings. lengths up to 89 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,8), (11,14), (13,21), (15,31), (17,42), (19,65), (21,98), (23,135), (25,197), (27,270), (29,388), (31,551), (33,783), (35,1106), (37,1563), (39,2211), (41,3116), (43,4400), (45,6223), (47,8774), (49,12413), (51,17529), (53,24829), (55,35088), (57,49805), (59,70539), (61,100323), (63,142420), (65,202794), (67,288534), (69,411654), (71,586547), (73,837981), (75,1196203), (77,1710627), (79,2444582), (81,3499861), (83,5006994), (85,68838412), (87,170845717), (89,335691857)} ; 335691857 new representative proofs (1056027538 redundant, 70868983 invalid) Wed May 27 18:42:47 2026: Starting to write 335691857 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs89-unfiltered85+.txt. 397341.13 ms (6 min 37 s 341.13 ms) taken to print and save 92241090323 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs89-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 2572905791. [most relevant: {1,89} with 2*335691857 = 671383714, i.e. ≈26.09%] Wed May 27 18:59:57 2026: Starting to generate D-proof representatives of length 91. Wed May 27 19:16:16 2026: Iterated ≈ 2% of D-proof candidates. [ 51458115 of 2572905791] (ETC: Thu May 28 08:36:18 2026 ; 13 h 20 min 1 s 804.34 ms remaining ; 13 h 36 min 21 s 432.98 ms total) Wed May 27 19:26:13 2026: Iterated ≈ 4% of D-proof candidates. [ 102916231 of 2572905791] (ETC: Thu May 28 05:56:41 2026 ; 10 h 30 min 28 s 364.84 ms remaining ; 10 h 56 min 44 s 546.70 ms total) Wed May 27 19:36:33 2026: Iterated ≈ 6% of D-proof candidates. [ 154374347 of 2572905791] (ETC: Thu May 28 05:10:05 2026 ; 9 h 33 min 31 s 784.84 ms remaining ; 10 h 10 min 8 s 281.74 ms total) Wed May 27 19:43:39 2026: Iterated ≈ 8% of D-proof candidates. [ 205832463 of 2572905791] (ETC: Thu May 28 04:06:08 2026 ; 8 h 22 min 29 s 777.57 ms remaining ; 9 h 6 min 11 s 497.36 ms total) Wed May 27 19:49:29 2026: Iterated ≈10% of D-proof candidates. [ 257290579 of 2572905791] (ETC: Thu May 28 03:15:21 2026 ; 7 h 25 min 51 s 332.69 ms remaining ; 8 h 15 min 23 s 702.99 ms total) Wed May 27 19:57:44 2026: Iterated ≈12% of D-proof candidates. [ 308748694 of 2572905791] (ETC: Thu May 28 03:01:29 2026 ; 7 h 3 min 45 s 92.63 ms remaining ; 8 h 1 min 32 s 150.70 ms total) Wed May 27 20:06:38 2026: Iterated ≈14% of D-proof candidates. [ 360206810 of 2572905791] (ETC: Thu May 28 02:56:17 2026 ; 6 h 49 min 39 s 136.66 ms remaining ; 7 h 56 min 20 s 391.45 ms total) Wed May 27 20:15:13 2026: Iterated ≈16% of D-proof candidates. [ 411664926 of 2572905791] (ETC: Thu May 28 02:50:21 2026 ; 6 h 35 min 8 s 450.23 ms remaining ; 7 h 50 min 24 s 345.51 ms total) Wed May 27 20:24:07 2026: Iterated ≈18% of D-proof candidates. [ 463123042 of 2572905791] (ETC: Thu May 28 02:47:31 2026 ; 6 h 23 min 24 s 143.85 ms remaining ; 7 h 47 min 33 s 833.96 ms total) Wed May 27 20:32:13 2026: Iterated ≈20% of D-proof candidates. [ 514581158 of 2572905791] (ETC: Thu May 28 02:41:17 2026 ; 6 h 9 min 4 s 42.56 ms remaining ; 7 h 41 min 20 s 53.20 ms total) Wed May 27 20:40:08 2026: Iterated ≈22% of D-proof candidates. [ 566039274 of 2572905791] (ETC: Thu May 28 02:35:18 2026 ; 5 h 55 min 10 s 774.05 ms remaining ; 7 h 35 min 21 s 505.19 ms total) Wed May 27 20:48:11 2026: Iterated ≈24% of D-proof candidates. [ 617497389 of 2572905791] (ETC: Thu May 28 02:30:54 2026 ; 5 h 42 min 43 s 110.67 ms remaining ; 7 h 30 min 56 s 724.55 ms total) Wed May 27 20:56:10 2026: Iterated ≈26% of D-proof candidates. [ 668955505 of 2572905791] (ETC: Thu May 28 02:26:55 2026 ; 5 h 30 min 45 s 783.61 ms remaining ; 7 h 26 min 58 s 626.49 ms total) Wed May 27 21:09:00 2026: Iterated ≈28% of D-proof candidates. [ 720413621 of 2572905791] (ETC: Thu May 28 02:40:49 2026 ; 5 h 31 min 49 s 888.95 ms remaining ; 7 h 40 min 52 s 623.53 ms total) Wed May 27 21:17:52 2026: Iterated ≈30% of D-proof candidates. [ 771871737 of 2572905791] (ETC: Thu May 28 02:39:41 2026 ; 5 h 21 min 49 s 73.00 ms remaining ; 7 h 39 min 44 s 389.99 ms total) Wed May 27 21:26:02 2026: Iterated ≈32% of D-proof candidates. [ 823329853 of 2572905791] (ETC: Thu May 28 02:36:28 2026 ; 5 h 10 min 25 s 719.43 ms remaining ; 7 h 36 min 30 s 763.87 ms total) Wed May 27 21:35:08 2026: Iterated ≈34% of D-proof candidates. [ 874787968 of 2572905791] (ETC: Thu May 28 02:36:21 2026 ; 5 h 1 min 13 s 709.58 ms remaining ; 7 h 36 min 24 s 408.44 ms total) Wed May 27 21:44:31 2026: Iterated ≈36% of D-proof candidates. [ 926246084 of 2572905791] (ETC: Thu May 28 02:37:06 2026 ; 4 h 52 min 34 s 816.84 ms remaining ; 7 h 37 min 9 s 401.31 ms total) Wed May 27 21:54:03 2026: Iterated ≈38% of D-proof candidates. [ 977704200 of 2572905791] (ETC: Thu May 28 02:38:08 2026 ; 4 h 44 min 4 s 541.83 ms remaining ; 7 h 38 min 11 s 196.49 ms total) Wed May 27 22:03:28 2026: Iterated ≈40% of D-proof candidates. [1029162316 of 2572905791] (ETC: Thu May 28 02:38:45 2026 ; 4 h 35 min 16 s 829.65 ms remaining ; 7 h 38 min 48 s 49.40 ms total) Wed May 27 22:09:50 2026: Iterated ≈42% of D-proof candidates. [1080620432 of 2572905791] (ETC: Thu May 28 02:32:04 2026 ; 4 h 22 min 13 s 756.20 ms remaining ; 7 h 32 min 7 s 165.87 ms total) Wed May 27 22:17:05 2026: Iterated ≈44% of D-proof candidates. [1132078548 of 2572905791] (ETC: Thu May 28 02:28:00 2026 ; 4 h 10 min 54 s 314.16 ms remaining ; 7 h 28 min 2 s 703.86 ms total) Wed May 27 22:24:03 2026: Iterated ≈46% of D-proof candidates. [1183536663 of 2572905791] (ETC: Thu May 28 02:23:39 2026 ; 3 h 59 min 35 s 774.19 ms remaining ; 7 h 23 min 41 s 804.04 ms total) Wed May 27 22:30:39 2026: Iterated ≈48% of D-proof candidates. [1234994779 of 2572905791] (ETC: Thu May 28 02:18:55 2026 ; 3 h 48 min 15 s 800.86 ms remaining ; 7 h 18 min 58 s 78.57 ms total) Wed May 27 22:37:44 2026: Iterated ≈50% of D-proof candidates. [1286452895 of 2572905791] (ETC: Thu May 28 02:15:31 2026 ; 3 h 37 min 47 s 108.79 ms remaining ; 7 h 15 min 34 s 217.58 ms total) Wed May 27 22:44:38 2026: Iterated ≈52% of D-proof candidates. [1337911011 of 2572905791] (ETC: Thu May 28 02:12:03 2026 ; 3 h 27 min 24 s 440.68 ms remaining ; 7 h 12 min 5 s 918.08 ms total) Wed May 27 22:51:33 2026: Iterated ≈54% of D-proof candidates. [1389369127 of 2572905791] (ETC: Thu May 28 02:08:51 2026 ; 3 h 17 min 17 s 821.72 ms remaining ; 7 h 8 min 54 s 395.04 ms total) Wed May 27 22:57:45 2026: Iterated ≈56% of D-proof candidates. [1440827242 of 2572905791] (ETC: Thu May 28 02:04:36 2026 ; 3 h 6 min 50 s 932.19 ms remaining ; 7 h 4 min 39 s 391.31 ms total) Wed May 27 23:05:07 2026: Iterated ≈58% of D-proof candidates. [1492285358 of 2572905791] (ETC: Thu May 28 02:02:40 2026 ; 2 h 57 min 32 s 523.40 ms remaining ; 7 h 2 min 43 s 150.93 ms total) Wed May 27 23:12:23 2026: Iterated ≈60% of D-proof candidates. [1543743474 of 2572905791] (ETC: Thu May 28 02:00:40 2026 ; 2 h 48 min 17 s 333.78 ms remaining ; 7 h 43 s 334.43 ms total) Wed May 27 23:18:34 2026: Iterated ≈62% of D-proof candidates. [1595201590 of 2572905791] (ETC: Thu May 28 01:57:04 2026 ; 2 h 38 min 30 s 347.57 ms remaining ; 6 h 57 min 7 s 230.43 ms total) Wed May 27 23:25:17 2026: Iterated ≈64% of D-proof candidates. [1646659706 of 2572905791] (ETC: Thu May 28 01:54:32 2026 ; 2 h 29 min 15 s 112.20 ms remaining ; 6 h 54 min 35 s 311.66 ms total) Wed May 27 23:32:14 2026: Iterated ≈66% of D-proof candidates. [1698117822 of 2572905791] (ETC: Thu May 28 01:52:30 2026 ; 2 h 20 min 16 s 199.97 ms remaining ; 6 h 52 min 33 s 529.32 ms total) Wed May 27 23:38:43 2026: Iterated ≈68% of D-proof candidates. [1749575937 of 2572905791] (ETC: Thu May 28 01:49:54 2026 ; 2 h 11 min 10 s 982.90 ms remaining ; 6 h 49 min 56 s 821.53 ms total) Wed May 27 23:45:45 2026: Iterated ≈70% of D-proof candidates. [1801034053 of 2572905791] (ETC: Thu May 28 01:48:14 2026 ; 2 h 2 min 29 s 214.01 ms remaining ; 6 h 48 min 17 s 380.01 ms total) Wed May 27 23:52:36 2026: Iterated ≈72% of D-proof candidates. [1852492169 of 2572905791] (ETC: Thu May 28 01:46:24 2026 ; 1 h 53 min 48 s 438.89 ms remaining ; 6 h 46 min 27 s 281.73 ms total) Wed May 27 23:59:14 2026: Iterated ≈74% of D-proof candidates. [1903950285 of 2572905791] (ETC: Thu May 28 01:44:23 2026 ; 1 h 45 min 9 s 162.83 ms remaining ; 6 h 44 min 26 s 10.86 ms total) Thu May 28 00:06:21 2026: Iterated ≈76% of D-proof candidates. [1955408401 of 2572905791] (ETC: Thu May 28 01:43:06 2026 ; 1 h 36 min 45 s 408.31 ms remaining ; 6 h 43 min 9 s 201.27 ms total) Thu May 28 00:13:17 2026: Iterated ≈78% of D-proof candidates. [2006866516 of 2572905791] (ETC: Thu May 28 01:41:40 2026 ; 1 h 28 min 22 s 736.86 ms remaining ; 6 h 41 min 43 s 349.32 ms total) Thu May 28 00:20:45 2026: Iterated ≈80% of D-proof candidates. [2058324632 of 2572905791] (ETC: Thu May 28 01:40:57 2026 ; 1 h 20 min 11 s 941.03 ms remaining ; 6 h 40 min 59 s 705.14 ms total) Thu May 28 00:27:59 2026: Iterated ≈82% of D-proof candidates. [2109782748 of 2572905791] (ETC: Thu May 28 01:40:00 2026 ; 1 h 12 min 533.36 ms remaining ; 6 h 40 min 2 s 963.06 ms total) Thu May 28 00:34:40 2026: Iterated ≈84% of D-proof candidates. [2161240864 of 2572905791] (ETC: Thu May 28 01:38:26 2026 ; 1 h 3 min 45 s 417.52 ms remaining ; 6 h 38 min 28 s 859.47 ms total) Thu May 28 00:42:07 2026: Iterated ≈86% of D-proof candidates. [2212698980 of 2572905791] (ETC: Thu May 28 01:37:49 2026 ; 55 min 42 s 121.45 ms remaining ; 6 h 37 min 52 s 296.06 ms total) Thu May 28 00:49:21 2026: Iterated ≈88% of D-proof candidates. [2264157096 of 2572905791] (ETC: Thu May 28 01:37:00 2026 ; 47 min 38 s 768.53 ms remaining ; 6 h 37 min 3 s 71.10 ms total) Thu May 28 00:56:31 2026: Iterated ≈90% of D-proof candidates. [2315615211 of 2572905791] (ETC: Thu May 28 01:36:08 2026 ; 39 min 37 s 152.80 ms remaining ; 6 h 36 min 11 s 527.88 ms total) Thu May 28 01:03:32 2026: Iterated ≈92% of D-proof candidates. [2367073327 of 2572905791] (ETC: Thu May 28 01:35:09 2026 ; 31 min 36 s 985.10 ms remaining ; 6 h 35 min 12 s 313.63 ms total) Thu May 28 01:10:53 2026: Iterated ≈94% of D-proof candidates. [2418531443 of 2572905791] (ETC: Thu May 28 01:34:34 2026 ; 23 min 40 s 603.99 ms remaining ; 6 h 34 min 36 s 733.16 ms total) Thu May 28 01:18:03 2026: Iterated ≈96% of D-proof candidates. [2469989559 of 2572905791] (ETC: Thu May 28 01:33:48 2026 ; 15 min 45 s 256.80 ms remaining ; 6 h 33 min 51 s 419.82 ms total) Thu May 28 01:25:06 2026: Iterated ≈98% of D-proof candidates. [2521447675 of 2572905791] (ETC: Thu May 28 01:32:58 2026 ; 7 min 51 s 625.46 ms remaining ; 6 h 33 min 1 s 272.94 ms total) Thu May 28 01:32:01 2026: Iterated 100% of D-proof candidates. [2572905791 of 2572905791] (ETC: Thu May 28 01:32:01 2026 ; 0.00 ms remaining ; 6 h 32 min 4 s 676.76 ms total) 23535595.93 ms (6 h 32 min 15 s 595.93 ms) taken to collect 584703462 D-proofs of length 91. [iterated 2572905791 condensed detachment proof strings] 4678790.90 ms (1 h 17 min 58 s 790.90 ms) taken to filter and order new representative proofs. Found 584703462 representative, 1819347184 redundant, and 168855145 invalid condensed detachment proof strings. lengths up to 91 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,8), (11,14), (13,21), (15,31), (17,42), (19,65), (21,98), (23,135), (25,197), (27,270), (29,388), (31,551), (33,783), (35,1106), (37,1563), (39,2211), (41,3116), (43,4400), (45,6223), (47,8774), (49,12413), (51,17529), (53,24829), (55,35088), (57,49805), (59,70539), (61,100323), (63,142420), (65,202794), (67,288534), (69,411654), (71,586547), (73,837981), (75,1196203), (77,1710627), (79,2444582), (81,3499861), (83,5006994), (85,68838412), (87,170845717), (89,335691857), (91,584703462)} ; 584703462 new representative proofs (1819347184 redundant, 168855145 invalid) Thu May 28 02:50:11 2026: Starting to write 584703462 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs91-unfiltered85+.txt. 957817.81 ms (15 min 57 s 817.81 ms) taken to print and save 167173802257 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs91-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 4629933262. [most relevant: {1,91} with 2*584703462 = 1169406924, i.e. ≈25.26%] Thu May 28 03:28:47 2026: Starting to generate D-proof representatives of length 93. Thu May 28 03:58:30 2026: Iterated ≈ 2% of D-proof candidates. [ 92598665 of 4629933262] (ETC: Fri May 29 04:13:55 2026 ; 1 d 15 min 25 s 158.59 ms remaining ; 1 d 45 min 7 s 304.68 ms total) Thu May 28 04:18:45 2026: Iterated ≈ 4% of D-proof candidates. [ 185197330 of 4629933262] (ETC: Fri May 29 00:17:53 2026 ; 19 h 59 min 7 s 598.45 ms remaining ; 20 h 49 min 5 s 415.04 ms total) Thu May 28 04:37:40 2026: Iterated ≈ 6% of D-proof candidates. [ 277795995 of 4629933262] (ETC: Thu May 28 22:36:51 2026 ; 17 h 59 min 10 s 783.52 ms remaining ; 19 h 8 min 3 s 812.25 ms total) Thu May 28 04:55:44 2026: Iterated ≈ 8% of D-proof candidates. [ 370394660 of 4629933262] (ETC: Thu May 28 21:35:37 2026 ; 16 h 39 min 53 s 310.27 ms remaining ; 18 h 6 min 50 s 119.84 ms total) Thu May 28 05:06:49 2026: Iterated ≈10% of D-proof candidates. [ 462993326 of 4629933262] (ETC: Thu May 28 19:48:59 2026 ; 14 h 42 min 10 s 270.61 ms remaining ; 16 h 20 min 11 s 411.79 ms total) Thu May 28 05:20:28 2026: Iterated ≈12% of D-proof candidates. [ 555591991 of 4629933262] (ETC: Thu May 28 18:59:25 2026 ; 13 h 38 min 57 s 535.96 ms remaining ; 15 h 30 min 38 s 109.03 ms total) Thu May 28 05:36:51 2026: Iterated ≈14% of D-proof candidates. [ 648190656 of 4629933262] (ETC: Thu May 28 18:43:30 2026 ; 13 h 6 min 38 s 843.27 ms remaining ; 15 h 14 min 42 s 375.89 ms total) Thu May 28 05:53:12 2026: Iterated ≈16% of D-proof candidates. [ 740789321 of 4629933262] (ETC: Thu May 28 18:31:21 2026 ; 12 h 38 min 8 s 937.19 ms remaining ; 15 h 2 min 33 s 496.64 ms total) Thu May 28 06:10:18 2026: Iterated ≈18% of D-proof candidates. [ 833387987 of 4629933262] (ETC: Thu May 28 18:26:03 2026 ; 12 h 15 min 45 s 480.94 ms remaining ; 14 h 57 min 15 s 952.37 ms total) Thu May 28 06:26:19 2026: Iterated ≈20% of D-proof candidates. [ 925986652 of 4629933262] (ETC: Thu May 28 18:16:28 2026 ; 11 h 50 min 8 s 162.85 ms remaining ; 14 h 47 min 40 s 203.56 ms total) Thu May 28 06:40:30 2026: Iterated ≈22% of D-proof candidates. [1018585317 of 4629933262] (ETC: Thu May 28 18:00:12 2026 ; 11 h 19 min 42 s 104.37 ms remaining ; 14 h 31 min 24 s 749.18 ms total) Thu May 28 06:54:45 2026: Iterated ≈24% of D-proof candidates. [1111183982 of 4629933262] (ETC: Thu May 28 17:46:58 2026 ; 10 h 52 min 12 s 593.76 ms remaining ; 14 h 18 min 10 s 254.93 ms total) Thu May 28 07:11:29 2026: Iterated ≈26% of D-proof candidates. [1203782648 of 4629933262] (ETC: Thu May 28 17:45:20 2026 ; 10 h 33 min 50 s 319.10 ms remaining ; 14 h 16 min 32 s 323.11 ms total) Thu May 28 07:35:32 2026: Iterated ≈28% of D-proof candidates. [1296381313 of 4629933262] (ETC: Thu May 28 18:10:03 2026 ; 10 h 34 min 30 s 327.66 ms remaining ; 14 h 41 min 15 s 455.08 ms total) Thu May 28 07:54:25 2026: Iterated ≈30% of D-proof candidates. [1388979978 of 4629933262] (ETC: Thu May 28 18:14:12 2026 ; 10 h 19 min 47 s 87.31 ms remaining ; 14 h 45 min 24 s 410.43 ms total) Thu May 28 08:08:48 2026: Iterated ≈32% of D-proof candidates. [1481578643 of 4629933262] (ETC: Thu May 28 18:03:49 2026 ; 9 h 55 min 1 s 443.65 ms remaining ; 14 h 35 min 2 s 123.01 ms total) Thu May 28 08:32:00 2026: Iterated ≈34% of D-proof candidates. [1574177309 of 4629933262] (ETC: Thu May 28 18:20:36 2026 ; 9 h 48 min 35 s 857.07 ms remaining ; 14 h 51 min 48 s 874.34 ms total) Thu May 28 08:50:51 2026: Iterated ≈36% of D-proof candidates. [1666775974 of 4629933262] (ETC: Thu May 28 18:23:25 2026 ; 9 h 32 min 33 s 480.75 ms remaining ; 14 h 54 min 37 s 313.66 ms total) Thu May 28 09:15:10 2026: Iterated ≈38% of D-proof candidates. [1759374639 of 4629933262] (ETC: Thu May 28 18:40:19 2026 ; 9 h 25 min 8 s 514.70 ms remaining ; 15 h 11 min 31 s 152.72 ms total) Thu May 28 09:36:56 2026: Iterated ≈40% of D-proof candidates. [1851973304 of 4629933262] (ETC: Thu May 28 18:49:08 2026 ; 9 h 12 min 12 s 552.00 ms remaining ; 15 h 20 min 20 s 919.99 ms total) Thu May 28 09:54:09 2026: Iterated ≈42% of D-proof candidates. [1944571970 of 4629933262] (ETC: Thu May 28 18:46:20 2026 ; 8 h 52 min 10 s 247.08 ms remaining ; 15 h 17 min 32 s 150.13 ms total) Thu May 28 10:08:57 2026: Iterated ≈44% of D-proof candidates. [2037170635 of 4629933262] (ETC: Thu May 28 18:38:16 2026 ; 8 h 29 min 18 s 309.83 ms remaining ; 15 h 9 min 28 s 410.40 ms total) Thu May 28 10:26:48 2026: Iterated ≈46% of D-proof candidates. [2129769300 of 4629933262] (ETC: Thu May 28 18:37:30 2026 ; 8 h 10 min 42 s 246.77 ms remaining ; 15 h 8 min 42 s 679.20 ms total) Thu May 28 10:41:59 2026: Iterated ≈48% of D-proof candidates. [2222367965 of 4629933262] (ETC: Thu May 28 18:31:17 2026 ; 7 h 49 min 17 s 811.29 ms remaining ; 15 h 2 min 29 s 637.07 ms total) Thu May 28 10:51:52 2026: Iterated ≈50% of D-proof candidates. [2314966631 of 4629933262] (ETC: Thu May 28 18:14:56 2026 ; 7 h 23 min 4 s 156.71 ms remaining ; 14 h 46 min 8 s 313.43 ms total) Thu May 28 11:03:35 2026: Iterated ≈52% of D-proof candidates. [2407565296 of 4629933262] (ETC: Thu May 28 18:03:23 2026 ; 6 h 59 min 48 s 281.71 ms remaining ; 14 h 34 min 35 s 586.90 ms total) Thu May 28 11:15:06 2026: Iterated ≈54% of D-proof candidates. [2500163961 of 4629933262] (ETC: Thu May 28 17:52:21 2026 ; 6 h 37 min 14 s 74.09 ms remaining ; 14 h 23 min 33 s 204.53 ms total) Thu May 28 11:28:09 2026: Iterated ≈56% of D-proof candidates. [2592762626 of 4629933262] (ETC: Thu May 28 17:44:48 2026 ; 6 h 16 min 38 s 683.93 ms remaining ; 14 h 16 min 645.27 ms total) Thu May 28 11:41:23 2026: Iterated ≈58% of D-proof candidates. [2685361291 of 4629933262] (ETC: Thu May 28 17:38:05 2026 ; 5 h 56 min 42 s 53.79 ms remaining ; 14 h 9 min 17 s 270.91 ms total) Thu May 28 11:54:05 2026: Iterated ≈60% of D-proof candidates. [2777959957 of 4629933262] (ETC: Thu May 28 17:30:57 2026 ; 5 h 36 min 52 s 24.14 ms remaining ; 14 h 2 min 10 s 60.36 ms total) Thu May 28 12:06:12 2026: Iterated ≈62% of D-proof candidates. [2870558622 of 4629933262] (ETC: Thu May 28 17:23:20 2026 ; 5 h 17 min 7 s 556.94 ms remaining ; 13 h 54 min 32 s 518.25 ms total) Thu May 28 12:19:03 2026: Iterated ≈64% of D-proof candidates. [2963157287 of 4629933262] (ETC: Thu May 28 17:17:19 2026 ; 4 h 58 min 16 s 356.41 ms remaining ; 13 h 48 min 32 s 101.12 ms total) Thu May 28 12:31:56 2026: Iterated ≈66% of D-proof candidates. [3055755952 of 4629933262] (ETC: Thu May 28 17:11:44 2026 ; 4 h 39 min 47 s 922.83 ms remaining ; 13 h 42 min 56 s 243.60 ms total) Thu May 28 12:45:22 2026: Iterated ≈68% of D-proof candidates. [3148354618 of 4629933262] (ETC: Thu May 28 17:07:17 2026 ; 4 h 21 min 55 s 237.06 ms remaining ; 13 h 38 min 30 s 115.80 ms total) Thu May 28 12:59:32 2026: Iterated ≈70% of D-proof candidates. [3240953283 of 4629933262] (ETC: Thu May 28 17:04:08 2026 ; 4 h 4 min 36 s 237.60 ms remaining ; 13 h 35 min 20 s 791.97 ms total) Thu May 28 13:12:57 2026: Iterated ≈72% of D-proof candidates. [3333551948 of 4629933262] (ETC: Thu May 28 17:00:07 2026 ; 3 h 47 min 10 s 341.84 ms remaining ; 13 h 31 min 19 s 792.26 ms total) Thu May 28 13:25:25 2026: Iterated ≈74% of D-proof candidates. [3426150613 of 4629933262] (ETC: Thu May 28 16:55:03 2026 ; 3 h 29 min 37 s 569.20 ms remaining ; 13 h 26 min 15 s 266.10 ms total) Thu May 28 13:37:57 2026: Iterated ≈76% of D-proof candidates. [3518749279 of 4629933262] (ETC: Thu May 28 16:50:19 2026 ; 3 h 12 min 22 s 60.93 ms remaining ; 13 h 21 min 31 s 920.52 ms total) Thu May 28 13:51:27 2026: Iterated ≈78% of D-proof candidates. [3611347944 of 4629933262] (ETC: Thu May 28 16:47:04 2026 ; 2 h 55 min 37 s 330.85 ms remaining ; 13 h 18 min 16 s 958.39 ms total) Thu May 28 14:04:58 2026: Iterated ≈80% of D-proof candidates. [3703946609 of 4629933262] (ETC: Thu May 28 16:44:01 2026 ; 2 h 39 min 2 s 628.14 ms remaining ; 13 h 15 min 13 s 140.66 ms total) Thu May 28 14:18:35 2026: Iterated ≈82% of D-proof candidates. [3796545274 of 4629933262] (ETC: Thu May 28 16:41:13 2026 ; 2 h 22 min 38 s 259.57 ms remaining ; 13 h 12 min 25 s 886.46 ms total) Thu May 28 14:31:11 2026: Iterated ≈84% of D-proof candidates. [3889143940 of 4629933262] (ETC: Thu May 28 16:37:21 2026 ; 2 h 6 min 10 s 244.45 ms remaining ; 13 h 8 min 34 s 27.80 ms total) Thu May 28 14:44:00 2026: Iterated ≈86% of D-proof candidates. [3981742605 of 4629933262] (ETC: Thu May 28 16:33:55 2026 ; 1 h 49 min 55 s 9.68 ms remaining ; 13 h 5 min 7 s 211.96 ms total) Thu May 28 14:57:18 2026: Iterated ≈88% of D-proof candidates. [4074341270 of 4629933262] (ETC: Thu May 28 16:31:12 2026 ; 1 h 33 min 53 s 327.41 ms remaining ; 13 h 2 min 24 s 395.00 ms total) Thu May 28 15:11:10 2026: Iterated ≈90% of D-proof candidates. [4166939935 of 4629933262] (ETC: Thu May 28 16:29:13 2026 ; 1 h 18 min 2 s 570.45 ms remaining ; 13 h 25 s 704.41 ms total) Thu May 28 15:25:08 2026: Iterated ≈92% of D-proof candidates. [4259538601 of 4629933262] (ETC: Thu May 28 16:27:25 2026 ; 1 h 2 min 17 s 410.01 ms remaining ; 12 h 58 min 37 s 625.12 ms total) Thu May 28 15:38:20 2026: Iterated ≈94% of D-proof candidates. [4352137266 of 4629933262] (ETC: Thu May 28 16:24:54 2026 ; 46 min 34 s 8.96 ms remaining ; 12 h 56 min 6 s 815.88 ms total) Thu May 28 15:51:14 2026: Iterated ≈96% of D-proof candidates. [4444735931 of 4629933262] (ETC: Thu May 28 16:22:10 2026 ; 30 min 56 s 120.83 ms remaining ; 12 h 53 min 23 s 20.66 ms total) Thu May 28 16:04:20 2026: Iterated ≈98% of D-proof candidates. [4537334596 of 4629933262] (ETC: Thu May 28 16:19:46 2026 ; 15 min 25 s 165.05 ms remaining ; 12 h 50 min 58 s 252.10 ms total) Thu May 28 16:17:24 2026: Iterated 100% of D-proof candidates. [4629933262 of 4629933262] (ETC: Thu May 28 16:17:24 2026 ; 0.00 ms remaining ; 12 h 48 min 36 s 777.05 ms total) 46149716.67 ms (12 h 49 min 9 s 716.67 ms) taken to collect 1060815488 D-proofs of length 93. [iterated 4629933262 condensed detachment proof strings] 10472064.00 ms (2 h 54 min 32 s 64.00 ms) taken to filter and order new representative proofs. Found 1060815488 representative, 3261492947 redundant, and 307624827 invalid condensed detachment proof strings. lengths up to 93 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,8), (11,14), (13,21), (15,31), (17,42), (19,65), (21,98), (23,135), (25,197), (27,270), (29,388), (31,551), (33,783), (35,1106), (37,1563), (39,2211), (41,3116), (43,4400), (45,6223), (47,8774), (49,12413), (51,17529), (53,24829), (55,35088), (57,49805), (59,70539), (61,100323), (63,142420), (65,202794), (67,288534), (69,411654), (71,586547), (73,837981), (75,1196203), (77,1710627), (79,2444582), (81,3499861), (83,5006994), (85,68838412), (87,170845717), (89,335691857), (91,584703462), (93,1060815488)} ; 1060815488 new representative proofs (3261492947 redundant, 307624827 invalid) Thu May 28 19:12:29 2026: Starting to write 1060815488 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs93-unfiltered85+.txt. 1866944.94 ms (31 min 6 s 944.94 ms) taken to print and save 328964537344 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs93-unfiltered85+.txt. [2026-05-28T19:54:32.915] error: Detected 1 oom_kill event in StepId=611895.batch. Some of the step tasks have been OOM Killed.