( 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-2023 MPI (medium) node — 2-socket Intel Xeon Platinum 8468 (Sapphire Rapids), 48 cores each (96 cores total per node), 2.1 GHz, 3.8 GHz turbo mode, 512 GiB main memory — running Linux, Rocky 9.6. Wall-clock time: 0.9169444… h CPU utilization: 88.02666… core-h ) Mon May 25 18:38:37 2026: Process started. [pid: 486451, tid:22579904632640] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(81, 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(81, false, true, null, -1, -1, true). Mon May 25 18:38:37 2026: Limited D-proof representative generator started. [parallel ; 96 hardware thread contexts, limit: 81, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.00 ms taken to load initial representatives. 5.63 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs3.txt. [tid:22579702134336] 9.71 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs5.txt. [tid:22579700033088] 13.69 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs7.txt. [tid:22579697931840] 14.66 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs9.txt. [tid:22579695830592] 18.94 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs11.txt. [tid:22579693729344] 15.87 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs13.txt. [tid:22579691628096] 20.54 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs15.txt. [tid:22579689526848] 11.42 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs17.txt. [tid:22579687425600] 11.45 ms taken to read 65 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs19.txt. [tid:22579685324352] 18.35 ms taken to read 98 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs21.txt. [tid:22579683223104] 20.06 ms taken to read 135 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs23.txt. [tid:22579681121856] 22.42 ms taken to read 197 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs25.txt. [tid:22579679020608] 26.14 ms taken to read 270 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs27.txt. [tid:22579676919360] 25.86 ms taken to read 388 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs29.txt. [tid:22579674818112] 13.33 ms taken to read 551 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs31.txt. [tid:22579672716864] 27.45 ms taken to read 783 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs33.txt. [tid:22579670615616] 29.39 ms taken to read 1106 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs35.txt. [tid:22579668514368] 20.91 ms taken to read 1563 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs37.txt. [tid:22579666413120] 31.84 ms taken to read 2211 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs39.txt. [tid:22579664311872] 35.11 ms taken to read 3116 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs41.txt. [tid:22579662210624] 27.47 ms taken to read 4400 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs43.txt. [tid:22579660109376] 40.08 ms taken to read 6223 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs45.txt. [tid:22579658008128] 68.60 ms taken to read 8774 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs47.txt. [tid:22579655906880] 34.95 ms taken to read 12413 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs49.txt. [tid:22579653805632] 53.90 ms taken to read 17529 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs51.txt. [tid:22578173310528] 49.62 ms taken to read 24829 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs53.txt. [tid:22578171209280] 55.95 ms taken to read 35088 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs55.txt. [tid:22578169108032] 60.67 ms taken to read 49805 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs57.txt. [tid:22578167006784] 70.74 ms taken to read 70539 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs59.txt. [tid:22578164905536] 90.79 ms taken to read 100323 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs61.txt. [tid:22578162804288] 96.92 ms taken to read 142420 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs63.txt. [tid:22578160703040] 134.35 ms taken to read 202794 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs65.txt. [tid:22578158601792] 223.62 ms taken to read 288534 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs67.txt. [tid:22578156500544] 283.09 ms taken to read 411654 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs69.txt. [tid:22578154399296] 334.69 ms taken to read 586547 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs71.txt. [tid:22578152298048] 437.24 ms taken to read 837981 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs73.txt. [tid:22578150196800] 608.18 ms taken to read 1196203 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs75.txt. [tid:22578148095552] 789.33 ms taken to read 1710627 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs77.txt. [tid:22578145994304] 1026.98 ms (1 s 26.98 ms) taken to read 2444582 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs79.txt. [tid:22578143893056] 1043.40 ms (1 s 43.40 ms) total read duration. Loaded 40 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 8161870 representatives in total. Mon May 25 18:38:38 2026: Inserted ≈ 5% of D-proof conclusions. [ 408093 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 923.75 ms remaining ; 2 s 25.00 ms total) Mon May 25 18:38:38 2026: Inserted ≈10% of D-proof conclusions. [ 816187 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 691.85 ms remaining ; 1 s 879.83 ms total) Mon May 25 18:38:38 2026: Inserted ≈15% of D-proof conclusions. [1224280 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 551.51 ms remaining ; 1 s 825.31 ms total) Mon May 25 18:38:38 2026: Inserted ≈20% of D-proof conclusions. [1632374 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 474.06 ms remaining ; 1 s 842.58 ms total) Mon May 25 18:38:38 2026: Inserted ≈25% of D-proof conclusions. [2040467 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 366.72 ms remaining ; 1 s 822.30 ms total) Mon May 25 18:38:38 2026: Inserted ≈30% of D-proof conclusions. [2448561 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 275.82 ms remaining ; 1 s 822.60 ms total) Mon May 25 18:38:39 2026: Inserted ≈35% of D-proof conclusions. [2856654 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 186.49 ms remaining ; 1 s 825.37 ms total) Mon May 25 18:38:39 2026: Inserted ≈40% of D-proof conclusions. [3264748 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 97.28 ms remaining ; 1 s 828.80 ms total) Mon May 25 18:38:39 2026: Inserted ≈45% of D-proof conclusions. [3672841 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 1 s 3.27 ms remaining ; 1 s 824.13 ms total) Mon May 25 18:38:39 2026: Inserted ≈50% of D-proof conclusions. [4080935 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 912.44 ms remaining ; 1 s 824.87 ms total) Mon May 25 18:38:39 2026: Inserted ≈55% of D-proof conclusions. [4489028 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 823.66 ms remaining ; 1 s 830.37 ms total) Mon May 25 18:38:39 2026: Inserted ≈60% of D-proof conclusions. [4897122 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 729.96 ms remaining ; 1 s 824.89 ms total) Mon May 25 18:38:39 2026: Inserted ≈65% of D-proof conclusions. [5305215 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 637.46 ms remaining ; 1 s 821.33 ms total) Mon May 25 18:38:39 2026: Inserted ≈70% of D-proof conclusions. [5713309 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 545.58 ms remaining ; 1 s 818.59 ms total) Mon May 25 18:38:39 2026: Inserted ≈75% of D-proof conclusions. [6121402 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 456.69 ms remaining ; 1 s 826.78 ms total) Mon May 25 18:38:39 2026: Inserted ≈80% of D-proof conclusions. [6529496 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 364.71 ms remaining ; 1 s 823.56 ms total) Mon May 25 18:38:39 2026: Inserted ≈85% of D-proof conclusions. [6937589 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 273.03 ms remaining ; 1 s 820.19 ms total) Mon May 25 18:38:40 2026: Inserted ≈90% of D-proof conclusions. [7345683 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 181.70 ms remaining ; 1 s 817.04 ms total) Mon May 25 18:38:40 2026: Inserted ≈95% of D-proof conclusions. [7753776 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 90.77 ms remaining ; 1 s 815.43 ms total) Mon May 25 18:38:40 2026: Inserted 100% of D-proof conclusions. [8161870 of 8161870] (ETC: Mon May 25 18:38:40 2026 ; 0.00 ms remaining ; 1 s 811.65 ms total) 1811.84 ms (1 s 811.84 ms) total insertion duration. Determined the number of proof string candidates for iteration as 223164368. [most relevant: {21,59} with 2*6912822 = 13825644, i.e. ≈6.20%] Mon May 25 18:38:40 2026: Starting to generate D-proof representatives of length 81. Mon May 25 18:39:46 2026: Iterated ≈ 2% of D-proof candidates. [ 4463287 of 223164368] (ETC: Mon May 25 19:33:56 2026 ; 54 min 9 s 567.52 ms remaining ; 55 min 15 s 885.22 ms total) Mon May 25 18:40:56 2026: Iterated ≈ 4% of D-proof candidates. [ 8926574 of 223164368] (ETC: Mon May 25 19:35:28 2026 ; 54 min 32 s 163.59 ms remaining ; 56 min 48 s 503.72 ms total) Mon May 25 18:41:58 2026: Iterated ≈ 6% of D-proof candidates. [ 13389862 of 223164368] (ETC: Mon May 25 19:33:40 2026 ; 51 min 41 s 967.21 ms remaining ; 54 min 59 s 965.12 ms total) Mon May 25 18:43:02 2026: Iterated ≈ 8% of D-proof candidates. [ 17853149 of 223164368] (ETC: Mon May 25 19:33:21 2026 ; 50 min 18 s 790.15 ms remaining ; 54 min 41 s 293.63 ms total) Mon May 25 18:43:52 2026: Iterated ≈10% of D-proof candidates. [ 22316436 of 223164368] (ETC: Mon May 25 19:30:47 2026 ; 46 min 54 s 321.69 ms remaining ; 52 min 7 s 24.08 ms total) Mon May 25 18:45:00 2026: Iterated ≈12% of D-proof candidates. [ 26779724 of 223164368] (ETC: Mon May 25 19:31:30 2026 ; 46 min 29 s 678.77 ms remaining ; 52 min 50 s 89.51 ms total) Mon May 25 18:46:02 2026: Iterated ≈14% of D-proof candidates. [ 31243011 of 223164368] (ETC: Mon May 25 19:31:21 2026 ; 45 min 18 s 667.85 ms remaining ; 52 min 41 s 241.68 ms total) Mon May 25 18:47:01 2026: Iterated ≈16% of D-proof candidates. [ 35706298 of 223164368] (ETC: Mon May 25 19:30:53 2026 ; 43 min 51 s 558.91 ms remaining ; 52 min 12 s 808.21 ms total) Mon May 25 18:48:17 2026: Iterated ≈18% of D-proof candidates. [ 40169586 of 223164368] (ETC: Mon May 25 19:32:09 2026 ; 43 min 51 s 869.42 ms remaining ; 53 min 29 s 596.85 ms total) Mon May 25 18:49:12 2026: Iterated ≈20% of D-proof candidates. [ 44632873 of 223164368] (ETC: Mon May 25 19:31:20 2026 ; 42 min 8 s 454.00 ms remaining ; 52 min 40 s 567.49 ms total) Mon May 25 18:50:13 2026: Iterated ≈22% of D-proof candidates. [ 49096160 of 223164368] (ETC: Mon May 25 19:31:11 2026 ; 40 min 58 s 311.49 ms remaining ; 52 min 31 s 681.38 ms total) Mon May 25 18:51:27 2026: Iterated ≈24% of D-proof candidates. [ 53559448 of 223164368] (ETC: Mon May 25 19:31:57 2026 ; 40 min 29 s 691.54 ms remaining ; 53 min 16 s 962.55 ms total) Mon May 25 18:52:24 2026: Iterated ≈26% of D-proof candidates. [ 58022735 of 223164368] (ETC: Mon May 25 19:31:30 2026 ; 39 min 6 s 130.62 ms remaining ; 52 min 50 s 446.77 ms total) Mon May 25 18:53:24 2026: Iterated ≈28% of D-proof candidates. [ 62486023 of 223164368] (ETC: Mon May 25 19:31:18 2026 ; 37 min 54 s 55.84 ms remaining ; 52 min 38 s 410.89 ms total) Mon May 25 18:54:25 2026: Iterated ≈30% of D-proof candidates. [ 66949310 of 223164368] (ETC: Mon May 25 19:31:10 2026 ; 36 min 45 s 282.67 ms remaining ; 52 min 30 s 403.80 ms total) Mon May 25 18:55:18 2026: Iterated ≈32% of D-proof candidates. [ 71412597 of 223164368] (ETC: Mon May 25 19:30:40 2026 ; 35 min 21 s 550.88 ms remaining ; 51 min 59 s 927.74 ms total) Mon May 25 18:56:32 2026: Iterated ≈34% of D-proof candidates. [ 75875885 of 223164368] (ETC: Mon May 25 19:31:13 2026 ; 34 min 41 s 77.47 ms remaining ; 52 min 33 s 147.68 ms total) Mon May 25 18:57:26 2026: Iterated ≈36% of D-proof candidates. [ 80339172 of 223164368] (ETC: Mon May 25 19:30:49 2026 ; 33 min 23 s 60.39 ms remaining ; 52 min 9 s 781.85 ms total) Mon May 25 18:58:23 2026: Iterated ≈38% of D-proof candidates. [ 84802459 of 223164368] (ETC: Mon May 25 19:30:35 2026 ; 32 min 11 s 216.47 ms remaining ; 51 min 54 s 865.26 ms total) Mon May 25 18:59:34 2026: Iterated ≈40% of D-proof candidates. [ 89265747 of 223164368] (ETC: Mon May 25 19:30:55 2026 ; 31 min 21 s 98.91 ms remaining ; 52 min 15 s 164.85 ms total) Mon May 25 19:00:27 2026: Iterated ≈42% of D-proof candidates. [ 93729034 of 223164368] (ETC: Mon May 25 19:30:32 2026 ; 30 min 5 s 177.16 ms remaining ; 51 min 52 s 374.40 ms total) Mon May 25 19:01:21 2026: Iterated ≈44% of D-proof candidates. [ 98192321 of 223164368] (ETC: Mon May 25 19:30:14 2026 ; 28 min 52 s 821.95 ms remaining ; 51 min 34 s 324.89 ms total) Mon May 25 19:02:30 2026: Iterated ≈46% of D-proof candidates. [102655609 of 223164368] (ETC: Mon May 25 19:30:28 2026 ; 27 min 58 s 707.56 ms remaining ; 51 min 48 s 717.70 ms total) Mon May 25 19:03:28 2026: Iterated ≈48% of D-proof candidates. [107118896 of 223164368] (ETC: Mon May 25 19:30:21 2026 ; 26 min 52 s 773.25 ms remaining ; 51 min 41 s 487.00 ms total) Mon May 25 19:04:27 2026: Iterated ≈50% of D-proof candidates. [111582184 of 223164368] (ETC: Mon May 25 19:30:15 2026 ; 25 min 47 s 615.86 ms remaining ; 51 min 35 s 231.72 ms total) Mon May 25 19:05:34 2026: Iterated ≈52% of D-proof candidates. [116045471 of 223164368] (ETC: Mon May 25 19:30:23 2026 ; 24 min 49 s 711.04 ms remaining ; 51 min 43 s 564.66 ms total) Mon May 25 19:06:34 2026: Iterated ≈54% of D-proof candidates. [120508758 of 223164368] (ETC: Mon May 25 19:30:19 2026 ; 23 min 45 s 841.02 ms remaining ; 51 min 39 s 654.38 ms total) Mon May 25 19:07:32 2026: Iterated ≈56% of D-proof candidates. [124972046 of 223164368] (ETC: Mon May 25 19:30:13 2026 ; 22 min 40 s 867.84 ms remaining ; 51 min 32 s 881.44 ms total) Mon May 25 19:08:34 2026: Iterated ≈58% of D-proof candidates. [129435333 of 223164368] (ETC: Mon May 25 19:30:14 2026 ; 21 min 39 s 664.54 ms remaining ; 51 min 34 s 439.37 ms total) Mon May 25 19:09:40 2026: Iterated ≈60% of D-proof candidates. [133898620 of 223164368] (ETC: Mon May 25 19:30:20 2026 ; 20 min 40 s 143.33 ms remaining ; 51 min 40 s 358.29 ms total) Mon May 25 19:10:38 2026: Iterated ≈62% of D-proof candidates. [138361908 of 223164368] (ETC: Mon May 25 19:30:13 2026 ; 19 min 35 s 562.88 ms remaining ; 51 min 33 s 586.52 ms total) Mon May 25 19:11:43 2026: Iterated ≈64% of D-proof candidates. [142825195 of 223164368] (ETC: Mon May 25 19:30:19 2026 ; 18 min 35 s 882.65 ms remaining ; 51 min 39 s 674.01 ms total) Mon May 25 19:12:47 2026: Iterated ≈66% of D-proof candidates. [147288482 of 223164368] (ETC: Mon May 25 19:30:22 2026 ; 17 min 34 s 771.19 ms remaining ; 51 min 42 s 268.17 ms total) Mon May 25 19:13:46 2026: Iterated ≈68% of D-proof candidates. [151751770 of 223164368] (ETC: Mon May 25 19:30:18 2026 ; 16 min 31 s 425.77 ms remaining ; 51 min 38 s 205.53 ms total) Mon May 25 19:14:52 2026: Iterated ≈70% of D-proof candidates. [156215057 of 223164368] (ETC: Mon May 25 19:30:23 2026 ; 15 min 31 s 133.19 ms remaining ; 51 min 43 s 777.26 ms total) Mon May 25 19:15:55 2026: Iterated ≈72% of D-proof candidates. [160678344 of 223164368] (ETC: Mon May 25 19:30:25 2026 ; 14 min 29 s 414.79 ms remaining ; 51 min 45 s 52.79 ms total) Mon May 25 19:16:56 2026: Iterated ≈74% of D-proof candidates. [165141632 of 223164368] (ETC: Mon May 25 19:30:22 2026 ; 13 min 26 s 683.99 ms remaining ; 51 min 42 s 630.72 ms total) Mon May 25 19:17:58 2026: Iterated ≈76% of D-proof candidates. [169604919 of 223164368] (ETC: Mon May 25 19:30:23 2026 ; 12 min 24 s 881.29 ms remaining ; 51 min 43 s 671.99 ms total) Mon May 25 19:19:02 2026: Iterated ≈78% of D-proof candidates. [174068207 of 223164368] (ETC: Mon May 25 19:30:25 2026 ; 11 min 23 s 246.40 ms remaining ; 51 min 45 s 665.45 ms total) Mon May 25 19:20:07 2026: Iterated ≈80% of D-proof candidates. [178531494 of 223164368] (ETC: Mon May 25 19:30:29 2026 ; 10 min 21 s 916.81 ms remaining ; 51 min 49 s 584.03 ms total) Mon May 25 19:21:08 2026: Iterated ≈82% of D-proof candidates. [182994781 of 223164368] (ETC: Mon May 25 19:30:27 2026 ; 9 min 19 s 352.96 ms remaining ; 51 min 47 s 516.37 ms total) Mon May 25 19:22:12 2026: Iterated ≈84% of D-proof candidates. [187458069 of 223164368] (ETC: Mon May 25 19:30:29 2026 ; 8 min 17 s 567.16 ms remaining ; 51 min 49 s 794.78 ms total) Mon May 25 19:23:16 2026: Iterated ≈86% of D-proof candidates. [191921356 of 223164368] (ETC: Mon May 25 19:30:32 2026 ; 7 min 15 s 710.15 ms remaining ; 51 min 52 s 215.30 ms total) Mon May 25 19:24:18 2026: Iterated ≈88% of D-proof candidates. [196384643 of 223164368] (ETC: Mon May 25 19:30:31 2026 ; 6 min 13 s 349.56 ms remaining ; 51 min 51 s 246.23 ms total) Mon May 25 19:25:22 2026: Iterated ≈90% of D-proof candidates. [200847931 of 223164368] (ETC: Mon May 25 19:30:34 2026 ; 5 min 11 s 390.72 ms remaining ; 51 min 53 s 907.18 ms total) Mon May 25 19:26:26 2026: Iterated ≈92% of D-proof candidates. [205311218 of 223164368] (ETC: Mon May 25 19:30:35 2026 ; 4 min 9 s 254.56 ms remaining ; 51 min 55 s 681.90 ms total) Mon May 25 19:27:28 2026: Iterated ≈94% of D-proof candidates. [209774505 of 223164368] (ETC: Mon May 25 19:30:34 2026 ; 3 min 6 s 887.04 ms remaining ; 51 min 54 s 783.86 ms total) Mon May 25 19:28:29 2026: Iterated ≈96% of D-proof candidates. [214237793 of 223164368] (ETC: Mon May 25 19:30:34 2026 ; 2 min 4 s 568.32 ms remaining ; 51 min 54 s 207.82 ms total) Mon May 25 19:29:37 2026: Iterated ≈98% of D-proof candidates. [218701080 of 223164368] (ETC: Mon May 25 19:30:39 2026 ; 1 min 2 s 385.10 ms remaining ; 51 min 59 s 254.64 ms total) Mon May 25 19:30:39 2026: Iterated 100% of D-proof candidates. [223164368 of 223164368] (ETC: Mon May 25 19:30:39 2026 ; 0.00 ms remaining ; 51 min 59 s 779.49 ms total) 3119804.01 ms (51 min 59 s 804.01 ms) taken to collect 32747235 D-proofs of length 81. [iterated 223164368 condensed detachment proof strings] 135516.98 ms (2 min 15 s 516.98 ms) taken to filter and order new representative proofs. Found 32747235 representative, 177980809 redundant, and 12436324 invalid condensed detachment proof strings. lengths up to 81 ; 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,32747235)} ; 32747235 new representative proofs (177980809 redundant, 12436324 invalid) Mon May 25 19:32:58 2026: Starting to write 32747235 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81-unfiltered81+.txt. 18244.28 ms (18 s 244.28 ms) taken to print and save 7196071762 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81-unfiltered81+.txt. Mon May 25 19:33:27 2026: Limited D-proof representative generator complete. [parallel ; 96 hardware thread contexts, limit: 81, unfiltered, candidate queue capacities: 50, use conclusion strings] Mon May 25 19:33:38 2026: Process terminated. [pid: 486451, tid:22579904632640]