( 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: 0.745 h CPU utilization: 47.68 core-h ) Tue May 26 00:47:15 2026: Process started. [pid: 197229, tid:22623298705216] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(83, 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(83, false, true, null, -1, -1, true). Tue May 26 00:47:15 2026: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 83, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.01 ms taken to load initial representatives. 4.57 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs3.txt. [tid:22623100597824] 12.36 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs5.txt. [tid:22623098496576] 67.85 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs7.txt. [tid:22623096395328] 9.86 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs9.txt. [tid:22623094294080] 19.28 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs11.txt. [tid:22622957975104] 9.87 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs13.txt. [tid:22623002031680] 10.84 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs15.txt. [tid:22623092192832] 4.41 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs17.txt. [tid:22623090091584] 13.32 ms taken to read 65 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs19.txt. [tid:22623087990336] 9.92 ms taken to read 98 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs21.txt. [tid:22623085889088] 33.65 ms taken to read 135 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs23.txt. [tid:22623083787840] 26.78 ms taken to read 197 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs25.txt. [tid:22623081686592] 13.40 ms taken to read 270 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs27.txt. [tid:22623079585344] 15.22 ms taken to read 388 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs29.txt. [tid:22623077484096] 28.93 ms taken to read 551 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs31.txt. [tid:22623075382848] 28.58 ms taken to read 783 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs33.txt. [tid:22623073281600] 22.34 ms taken to read 1106 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs35.txt. [tid:22622999930432] 33.01 ms taken to read 1563 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs37.txt. [tid:22622997829184] 39.66 ms taken to read 2211 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs39.txt. [tid:22622995727936] 36.15 ms taken to read 3116 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs41.txt. [tid:22622993626688] 34.90 ms taken to read 4400 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs43.txt. [tid:22622991525440] 106.08 ms taken to read 6223 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs45.txt. [tid:22622989424192] 29.93 ms taken to read 8774 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs47.txt. [tid:22622987322944] 48.12 ms taken to read 12413 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs49.txt. [tid:22622985221696] 42.55 ms taken to read 17529 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs51.txt. [tid:22622983120448] 139.49 ms taken to read 24829 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs53.txt. [tid:22622981019200] 58.54 ms taken to read 35088 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs55.txt. [tid:22622978917952] 255.15 ms taken to read 49805 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs57.txt. [tid:22622976816704] 301.12 ms taken to read 70539 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs59.txt. [tid:22622974715456] 246.68 ms taken to read 100323 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs61.txt. [tid:22622972614208] 247.64 ms taken to read 142420 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs63.txt. [tid:22622970512960] 371.77 ms taken to read 202794 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs65.txt. [tid:22622968411712] 476.87 ms taken to read 288534 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs67.txt. [tid:22622966310464] 852.90 ms taken to read 411654 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs69.txt. [tid:22622964209216] 866.62 ms taken to read 586547 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs71.txt. [tid:22622962107968] 1333.69 ms (1 s 333.69 ms) taken to read 837981 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs73.txt. [tid:22622955873856] 2202.07 ms (2 s 202.07 ms) taken to read 1196203 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs75.txt. [tid:22622953772608] 2389.10 ms (2 s 389.10 ms) taken to read 1710627 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs77.txt. [tid:22622951671360] 2325.62 ms (2 s 325.62 ms) taken to read 2444582 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs79.txt. [tid:22622949570112] 2728.97 ms (2 s 728.97 ms) taken to read 3499861 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81.txt. [tid:22622947468864] 2819.91 ms (2 s 819.91 ms) total read duration. Loaded 41 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 11661731 representatives in total. Tue May 26 00:47:18 2026: Inserted ≈ 5% of D-proof conclusions. [ 583086 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 2 s 24.17 ms remaining ; 2 s 130.70 ms total) Tue May 26 00:47:18 2026: Inserted ≈10% of D-proof conclusions. [ 1166173 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 860.11 ms remaining ; 2 s 66.79 ms total) Tue May 26 00:47:18 2026: Inserted ≈15% of D-proof conclusions. [ 1749259 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 875.58 ms remaining ; 2 s 206.56 ms total) Tue May 26 00:47:18 2026: Inserted ≈20% of D-proof conclusions. [ 2332346 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 779.70 ms remaining ; 2 s 224.63 ms total) Tue May 26 00:47:18 2026: Inserted ≈25% of D-proof conclusions. [ 2915432 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 682.52 ms remaining ; 2 s 243.36 ms total) Tue May 26 00:47:18 2026: Inserted ≈30% of D-proof conclusions. [ 3498519 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 555.82 ms remaining ; 2 s 222.59 ms total) Tue May 26 00:47:18 2026: Inserted ≈35% of D-proof conclusions. [ 4081605 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 440.28 ms remaining ; 2 s 215.82 ms total) Tue May 26 00:47:19 2026: Inserted ≈40% of D-proof conclusions. [ 4664692 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 338.79 ms remaining ; 2 s 231.31 ms total) Tue May 26 00:47:19 2026: Inserted ≈45% of D-proof conclusions. [ 5247778 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 224.71 ms remaining ; 2 s 226.74 ms total) Tue May 26 00:47:19 2026: Inserted ≈50% of D-proof conclusions. [ 5830865 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 120.45 ms remaining ; 2 s 240.90 ms total) Tue May 26 00:47:19 2026: Inserted ≈55% of D-proof conclusions. [ 6413952 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 1 s 19.91 ms remaining ; 2 s 266.47 ms total) Tue May 26 00:47:19 2026: Inserted ≈60% of D-proof conclusions. [ 6997038 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 906.56 ms remaining ; 2 s 266.39 ms total) Tue May 26 00:47:19 2026: Inserted ≈65% of D-proof conclusions. [ 7580125 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 791.32 ms remaining ; 2 s 260.90 ms total) Tue May 26 00:47:19 2026: Inserted ≈70% of D-proof conclusions. [ 8163211 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 676.59 ms remaining ; 2 s 255.30 ms total) Tue May 26 00:47:19 2026: Inserted ≈75% of D-proof conclusions. [ 8746298 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 568.82 ms remaining ; 2 s 275.28 ms total) Tue May 26 00:47:19 2026: Inserted ≈80% of D-proof conclusions. [ 9329384 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 455.83 ms remaining ; 2 s 279.16 ms total) Tue May 26 00:47:20 2026: Inserted ≈85% of D-proof conclusions. [ 9912471 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 341.15 ms remaining ; 2 s 274.34 ms total) Tue May 26 00:47:20 2026: Inserted ≈90% of D-proof conclusions. [10495557 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 228.12 ms remaining ; 2 s 281.17 ms total) Tue May 26 00:47:20 2026: Inserted ≈95% of D-proof conclusions. [11078644 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 114.32 ms remaining ; 2 s 286.42 ms total) Tue May 26 00:47:20 2026: Inserted 100% of D-proof conclusions. [11661731 of 11661731] (ETC: Tue May 26 00:47:20 2026 ; 0.00 ms remaining ; 2 s 286.10 ms total) 2286.21 ms (2 s 286.21 ms) total insertion duration. Determined the number of proof string candidates for iteration as 326376232. [most relevant: {21,61} with 2*9831654 = 19663308, i.e. ≈6.02%] Tue May 26 00:47:20 2026: Starting to generate D-proof representatives of length 83. Tue May 26 00:48:11 2026: Iterated ≈ 2% of D-proof candidates. [ 6527524 of 326376232] (ETC: Tue May 26 01:30:08 2026 ; 41 min 56 s 412.65 ms remaining ; 42 min 47 s 768.00 ms total) Tue May 26 00:49:19 2026: Iterated ≈ 4% of D-proof candidates. [ 13055049 of 326376232] (ETC: Tue May 26 01:36:59 2026 ; 47 min 39 s 865.72 ms remaining ; 49 min 39 s 26.79 ms total) Tue May 26 00:50:07 2026: Iterated ≈ 6% of D-proof candidates. [ 19582573 of 326376232] (ETC: Tue May 26 01:33:38 2026 ; 43 min 31 s 857.53 ms remaining ; 46 min 18 s 571.83 ms total) Tue May 26 00:51:03 2026: Iterated ≈ 8% of D-proof candidates. [ 26110098 of 326376232] (ETC: Tue May 26 01:33:49 2026 ; 42 min 45 s 701.20 ms remaining ; 46 min 28 s 805.65 ms total) Tue May 26 00:51:47 2026: Iterated ≈10% of D-proof candidates. [ 32637623 of 326376232] (ETC: Tue May 26 01:31:49 2026 ; 40 min 2 s 31.04 ms remaining ; 44 min 28 s 923.38 ms total) Tue May 26 00:52:46 2026: Iterated ≈12% of D-proof candidates. [ 39165147 of 326376232] (ETC: Tue May 26 01:32:38 2026 ; 39 min 51 s 749.16 ms remaining ; 45 min 17 s 896.77 ms total) Tue May 26 00:53:33 2026: Iterated ≈14% of D-proof candidates. [ 45692672 of 326376232] (ETC: Tue May 26 01:31:47 2026 ; 38 min 13 s 782.75 ms remaining ; 44 min 27 s 189.24 ms total) Tue May 26 00:54:19 2026: Iterated ≈16% of D-proof candidates. [ 52220197 of 326376232] (ETC: Tue May 26 01:31:01 2026 ; 36 min 41 s 990.69 ms remaining ; 43 min 41 s 417.49 ms total) Tue May 26 00:55:22 2026: Iterated ≈18% of D-proof candidates. [ 58747721 of 326376232] (ETC: Tue May 26 01:31:56 2026 ; 36 min 34 s 439.24 ms remaining ; 44 min 36 s 145.41 ms total) Tue May 26 00:56:02 2026: Iterated ≈20% of D-proof candidates. [ 65275246 of 326376232] (ETC: Tue May 26 01:30:49 2026 ; 34 min 47 s 210.56 ms remaining ; 43 min 29 s 13.20 ms total) Tue May 26 00:56:59 2026: Iterated ≈22% of D-proof candidates. [ 71802771 of 326376232] (ETC: Tue May 26 01:31:12 2026 ; 34 min 12 s 796.40 ms remaining ; 43 min 51 s 790.25 ms total) Tue May 26 00:57:50 2026: Iterated ≈24% of D-proof candidates. [ 78330295 of 326376232] (ETC: Tue May 26 01:31:05 2026 ; 33 min 14 s 797.22 ms remaining ; 43 min 44 s 733.18 ms total) Tue May 26 00:58:38 2026: Iterated ≈26% of D-proof candidates. [ 84857820 of 326376232] (ETC: Tue May 26 01:30:46 2026 ; 32 min 8 s 733.43 ms remaining ; 43 min 26 s 396.52 ms total) Tue May 26 00:59:30 2026: Iterated ≈28% of D-proof candidates. [ 91385344 of 326376232] (ETC: Tue May 26 01:30:47 2026 ; 31 min 17 s 55.36 ms remaining ; 43 min 27 s 21.33 ms total) Tue May 26 01:00:10 2026: Iterated ≈30% of D-proof candidates. [ 97912869 of 326376232] (ETC: Tue May 26 01:30:08 2026 ; 29 min 57 s 914.86 ms remaining ; 42 min 48 s 449.79 ms total) Tue May 26 01:00:59 2026: Iterated ≈32% of D-proof candidates. [104440394 of 326376232] (ETC: Tue May 26 01:30:00 2026 ; 29 min 630.07 ms remaining ; 42 min 39 s 750.09 ms total) Tue May 26 01:01:49 2026: Iterated ≈34% of D-proof candidates. [110967918 of 326376232] (ETC: Tue May 26 01:29:57 2026 ; 28 min 7 s 941.68 ms remaining ; 42 min 37 s 487.39 ms total) Tue May 26 01:02:30 2026: Iterated ≈36% of D-proof candidates. [117495443 of 326376232] (ETC: Tue May 26 01:29:29 2026 ; 26 min 58 s 718.08 ms remaining ; 42 min 9 s 247.00 ms total) Tue May 26 01:03:16 2026: Iterated ≈38% of D-proof candidates. [124022968 of 326376232] (ETC: Tue May 26 01:29:17 2026 ; 26 min 686.77 ms remaining ; 41 min 57 s 236.72 ms total) Tue May 26 01:04:01 2026: Iterated ≈40% of D-proof candidates. [130550492 of 326376232] (ETC: Tue May 26 01:29:02 2026 ; 25 min 967.71 ms remaining ; 41 min 41 s 612.84 ms total) Tue May 26 01:04:45 2026: Iterated ≈42% of D-proof candidates. [137078017 of 326376232] (ETC: Tue May 26 01:28:49 2026 ; 24 min 3 s 631.25 ms remaining ; 41 min 29 s 19.39 ms total) Tue May 26 01:05:31 2026: Iterated ≈44% of D-proof candidates. [143605542 of 326376232] (ETC: Tue May 26 01:28:39 2026 ; 23 min 8 s 195.60 ms remaining ; 41 min 18 s 920.72 ms total) Tue May 26 01:06:16 2026: Iterated ≈46% of D-proof candidates. [150133066 of 326376232] (ETC: Tue May 26 01:28:29 2026 ; 22 min 13 s 546.87 ms remaining ; 41 min 9 s 531.23 ms total) Tue May 26 01:06:58 2026: Iterated ≈48% of D-proof candidates. [156660591 of 326376232] (ETC: Tue May 26 01:28:14 2026 ; 21 min 15 s 901.40 ms remaining ; 40 min 53 s 656.54 ms total) Tue May 26 01:07:46 2026: Iterated ≈50% of D-proof candidates. [163188116 of 326376232] (ETC: Tue May 26 01:28:12 2026 ; 20 min 26 s 187.94 ms remaining ; 40 min 52 s 375.88 ms total) Tue May 26 01:08:32 2026: Iterated ≈52% of D-proof candidates. [169715640 of 326376232] (ETC: Tue May 26 01:28:06 2026 ; 19 min 34 s 125.42 ms remaining ; 40 min 46 s 94.63 ms total) Tue May 26 01:09:13 2026: Iterated ≈54% of D-proof candidates. [176243165 of 326376232] (ETC: Tue May 26 01:27:52 2026 ; 18 min 38 s 901.72 ms remaining ; 40 min 32 s 395.03 ms total) Tue May 26 01:10:04 2026: Iterated ≈56% of D-proof candidates. [182770689 of 326376232] (ETC: Tue May 26 01:27:56 2026 ; 17 min 52 s 10.58 ms remaining ; 40 min 36 s 387.67 ms total) Tue May 26 01:10:55 2026: Iterated ≈58% of D-proof candidates. [189298214 of 326376232] (ETC: Tue May 26 01:28:00 2026 ; 17 min 4 s 907.10 ms remaining ; 40 min 40 s 254.99 ms total) Tue May 26 01:11:39 2026: Iterated ≈60% of D-proof candidates. [195825739 of 326376232] (ETC: Tue May 26 01:27:52 2026 ; 16 min 12 s 640.50 ms remaining ; 40 min 31 s 601.24 ms total) Tue May 26 01:12:30 2026: Iterated ≈62% of D-proof candidates. [202353263 of 326376232] (ETC: Tue May 26 01:27:55 2026 ; 15 min 25 s 467.01 ms remaining ; 40 min 35 s 439.49 ms total) Tue May 26 01:13:15 2026: Iterated ≈64% of D-proof candidates. [208880788 of 326376232] (ETC: Tue May 26 01:27:49 2026 ; 14 min 34 s 511.43 ms remaining ; 40 min 29 s 198.40 ms total) Tue May 26 01:14:03 2026: Iterated ≈66% of D-proof candidates. [215408313 of 326376232] (ETC: Tue May 26 01:27:48 2026 ; 13 min 45 s 633.76 ms remaining ; 40 min 28 s 334.59 ms total) Tue May 26 01:14:50 2026: Iterated ≈68% of D-proof candidates. [221935837 of 326376232] (ETC: Tue May 26 01:27:47 2026 ; 12 min 56 s 602.97 ms remaining ; 40 min 26 s 884.26 ms total) Tue May 26 01:15:37 2026: Iterated ≈70% of D-proof candidates. [228463362 of 326376232] (ETC: Tue May 26 01:27:44 2026 ; 12 min 7 s 246.41 ms remaining ; 40 min 24 s 154.70 ms total) Tue May 26 01:16:24 2026: Iterated ≈72% of D-proof candidates. [234990887 of 326376232] (ETC: Tue May 26 01:27:43 2026 ; 11 min 18 s 373.15 ms remaining ; 40 min 22 s 761.24 ms total) Tue May 26 01:17:16 2026: Iterated ≈74% of D-proof candidates. [241518411 of 326376232] (ETC: Tue May 26 01:27:47 2026 ; 10 min 30 s 918.56 ms remaining ; 40 min 26 s 609.82 ms total) Tue May 26 01:18:01 2026: Iterated ≈76% of D-proof candidates. [248045936 of 326376232] (ETC: Tue May 26 01:27:42 2026 ; 9 min 41 s 297.46 ms remaining ; 40 min 22 s 72.75 ms total) Tue May 26 01:18:51 2026: Iterated ≈78% of D-proof candidates. [254573460 of 326376232] (ETC: Tue May 26 01:27:45 2026 ; 8 min 53 s 498.46 ms remaining ; 40 min 24 s 992.98 ms total) Tue May 26 01:19:37 2026: Iterated ≈80% of D-proof candidates. [261100985 of 326376232] (ETC: Tue May 26 01:27:41 2026 ; 8 min 4 s 227.49 ms remaining ; 40 min 21 s 137.43 ms total) Tue May 26 01:20:27 2026: Iterated ≈82% of D-proof candidates. [267628510 of 326376232] (ETC: Tue May 26 01:27:44 2026 ; 7 min 16 s 250.56 ms remaining ; 40 min 23 s 614.21 ms total) Tue May 26 01:21:20 2026: Iterated ≈84% of D-proof candidates. [274156034 of 326376232] (ETC: Tue May 26 01:27:48 2026 ; 6 min 28 s 538.16 ms remaining ; 40 min 28 s 363.48 ms total) Tue May 26 01:22:03 2026: Iterated ≈86% of D-proof candidates. [280683559 of 326376232] (ETC: Tue May 26 01:27:42 2026 ; 5 min 39 s 160.94 ms remaining ; 40 min 22 s 578.10 ms total) Tue May 26 01:22:49 2026: Iterated ≈88% of D-proof candidates. [287211084 of 326376232] (ETC: Tue May 26 01:27:40 2026 ; 4 min 50 s 389.22 ms remaining ; 40 min 19 s 910.12 ms total) Tue May 26 01:23:40 2026: Iterated ≈90% of D-proof candidates. [293738608 of 326376232] (ETC: Tue May 26 01:27:42 2026 ; 4 min 2 s 186.06 ms remaining ; 40 min 21 s 860.58 ms total) Tue May 26 01:24:23 2026: Iterated ≈92% of D-proof candidates. [300266133 of 326376232] (ETC: Tue May 26 01:27:36 2026 ; 3 min 13 s 321.42 ms remaining ; 40 min 16 s 517.69 ms total) Tue May 26 01:25:14 2026: Iterated ≈94% of D-proof candidates. [306793658 of 326376232] (ETC: Tue May 26 01:27:39 2026 ; 2 min 25 s 174.72 ms remaining ; 40 min 19 s 578.64 ms total) Tue May 26 01:26:05 2026: Iterated ≈96% of D-proof candidates. [313321182 of 326376232] (ETC: Tue May 26 01:27:42 2026 ; 1 min 36 s 893.76 ms remaining ; 40 min 22 s 343.94 ms total) Tue May 26 01:26:52 2026: Iterated ≈98% of D-proof candidates. [319848707 of 326376232] (ETC: Tue May 26 01:27:41 2026 ; 48 s 414.97 ms remaining ; 40 min 20 s 748.36 ms total) Tue May 26 01:27:38 2026: Iterated 100% of D-proof candidates. [326376232 of 326376232] (ETC: Tue May 26 01:27:38 2026 ; 0.00 ms remaining ; 40 min 17 s 711.63 ms total) 2418162.65 ms (40 min 18 s 162.65 ms) taken to collect 47493930 D-proofs of length 83. [iterated 326376232 condensed detachment proof strings] 186132.62 ms (3 min 6 s 132.62 ms) taken to filter and order new representative proofs. Found 47493930 representative, 260712882 redundant, and 18169420 invalid condensed detachment proof strings. lengths up to 83 ; 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,47493930)} ; 47493930 new representative proofs (260712882 redundant, 18169420 invalid) Tue May 26 01:30:47 2026: Starting to write 47493930 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83-unfiltered83+.txt. 33823.26 ms (33 s 823.26 ms) taken to print and save 10747183948 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83-unfiltered83+.txt. Tue May 26 01:31:36 2026: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 83, unfiltered, candidate queue capacities: 50, use conclusion strings] Tue May 26 01:31:57 2026: Process terminated. [pid: 197229, tid:22623298705216]