( 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.813888… h CPU utilization: 52.0888… core-h ) Tue May 26 09:22:04 2026: Process started. [pid: 401797, tid:22557135808320] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true) 2. generateDProofRepresentativeFiles(81, false, true, null, -1, -1, true) [Main] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true). Loaded 2 custom axioms. [SHA-512/224 hash: d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) (2) CO0 - COp - \bot\imply0 [Main] Calling generateDProofRepresentativeFiles(81, false, true, null, -1, -1, true). Tue May 26 09:22:04 2026: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 81, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.01 ms taken to load initial representatives. 9.95 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs3.txt. [tid:22556903966272] 12.64 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs5.txt. [tid:22556606174784] 5.23 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs7.txt. [tid:22556604073536] 6.46 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs9.txt. [tid:22556601972288] 15.44 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs11.txt. [tid:22556599871040] 8.74 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs13.txt. [tid:22556597769792] 18.71 ms taken to read 33 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs15.txt. [tid:22556595668544] 10.42 ms taken to read 45 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs17.txt. [tid:22556593567296] 23.81 ms taken to read 69 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs19.txt. [tid:22556591466048] 14.95 ms taken to read 101 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs21.txt. [tid:22556589364800] 22.79 ms taken to read 140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs23.txt. [tid:22556587263552] 13.65 ms taken to read 205 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs25.txt. [tid:22556585162304] 13.32 ms taken to read 280 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs27.txt. [tid:22556583061056] 8.05 ms taken to read 404 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs29.txt. [tid:22556580959808] 25.55 ms taken to read 568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs31.txt. [tid:22556578858560] 18.23 ms taken to read 809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs33.txt. [tid:22556576757312] 17.36 ms taken to read 1140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs35.txt. [tid:22556574656064] 16.59 ms taken to read 1614 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs37.txt. [tid:22556572554816] 22.88 ms taken to read 2278 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs39.txt. [tid:22556570453568] 24.55 ms taken to read 3217 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs41.txt. [tid:22556568352320] 50.11 ms taken to read 4529 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs43.txt. [tid:22556492949056] 32.95 ms taken to read 6426 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs45.txt. [tid:22556490847808] 35.48 ms taken to read 9042 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs47.txt. [tid:22556488746560] 34.06 ms taken to read 12829 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs49.txt. [tid:22556486645312] 46.60 ms taken to read 18076 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs51.txt. [tid:22556484544064] 62.49 ms taken to read 25667 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs53.txt. [tid:22556482442816] 49.69 ms taken to read 36224 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs55.txt. [tid:22556480341568] 174.94 ms taken to read 51530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs57.txt. [tid:22556478240320] 152.00 ms taken to read 72889 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs59.txt. [tid:22556476139072] 246.93 ms taken to read 103901 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs61.txt. [tid:22556474037824] 316.13 ms taken to read 147416 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs63.txt. [tid:22556471936576] 350.05 ms taken to read 210360 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs65.txt. [tid:22556469835328] 357.20 ms taken to read 299183 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs67.txt. [tid:22556467734080] 575.70 ms taken to read 427694 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs69.txt. [tid:22556465632832] 1036.69 ms (1 s 36.69 ms) taken to read 609264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs71.txt. [tid:22556463531584] 1131.33 ms (1 s 131.33 ms) taken to read 872065 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs73.txt. [tid:22556461430336] 1627.49 ms (1 s 627.49 ms) taken to read 1244628 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs75.txt. [tid:22556459329088] 1476.08 ms (1 s 476.08 ms) taken to read 1782980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs77.txt. [tid:22556457227840] 2004.32 ms (2 s 4.32 ms) taken to read 2547752 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs79.txt. [tid:22556455126592] 2091.50 ms (2 s 91.50 ms) total read duration. Loaded 40 representative collections of sizes: 1 : 2 3 : 1 5 : 1 7 : 3 9 : 8 11 : 15 13 : 22 15 : 33 17 : 45 19 : 69 21 : 101 23 : 140 25 : 205 27 : 280 29 : 404 31 : 568 33 : 809 35 : 1140 37 : 1614 39 : 2278 41 : 3217 43 : 4529 45 : 6426 47 : 9042 49 : 12829 51 : 18076 53 : 25667 55 : 36224 57 : 51530 59 : 72889 61 : 103901 63 : 147416 65 : 210360 67 : 299183 69 : 427694 71 : 609264 73 : 872065 75 : 1244628 77 : 1782980 79 : 2547752 8493410 representatives in total. Tue May 26 09:22:06 2026: Inserted ≈ 5% of D-proof conclusions. [ 424670 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 866.88 ms remaining ; 1 s 965.14 ms total) Tue May 26 09:22:06 2026: Inserted ≈10% of D-proof conclusions. [ 849341 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 729.66 ms remaining ; 1 s 921.85 ms total) Tue May 26 09:22:06 2026: Inserted ≈15% of D-proof conclusions. [1274011 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 615.46 ms remaining ; 1 s 900.54 ms total) Tue May 26 09:22:07 2026: Inserted ≈20% of D-proof conclusions. [1698682 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 512.40 ms remaining ; 1 s 890.50 ms total) Tue May 26 09:22:07 2026: Inserted ≈25% of D-proof conclusions. [2123352 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 422.42 ms remaining ; 1 s 896.56 ms total) Tue May 26 09:22:07 2026: Inserted ≈30% of D-proof conclusions. [2548023 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 322.23 ms remaining ; 1 s 888.90 ms total) Tue May 26 09:22:07 2026: Inserted ≈35% of D-proof conclusions. [2972693 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 225.25 ms remaining ; 1 s 885.00 ms total) Tue May 26 09:22:07 2026: Inserted ≈40% of D-proof conclusions. [3397364 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 144.50 ms remaining ; 1 s 907.50 ms total) Tue May 26 09:22:07 2026: Inserted ≈45% of D-proof conclusions. [3822034 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 1 s 58.98 ms remaining ; 1 s 925.41 ms total) Tue May 26 09:22:07 2026: Inserted ≈50% of D-proof conclusions. [4246705 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 973.60 ms remaining ; 1 s 947.20 ms total) Tue May 26 09:22:07 2026: Inserted ≈55% of D-proof conclusions. [4671375 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 911.68 ms remaining ; 2 s 25.95 ms total) Tue May 26 09:22:07 2026: Inserted ≈60% of D-proof conclusions. [5096046 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 816.02 ms remaining ; 2 s 40.05 ms total) Tue May 26 09:22:07 2026: Inserted ≈65% of D-proof conclusions. [5520716 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 716.51 ms remaining ; 2 s 47.17 ms total) Tue May 26 09:22:08 2026: Inserted ≈70% of D-proof conclusions. [5945387 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 614.14 ms remaining ; 2 s 47.14 ms total) Tue May 26 09:22:08 2026: Inserted ≈75% of D-proof conclusions. [6370057 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 512.08 ms remaining ; 2 s 48.32 ms total) Tue May 26 09:22:08 2026: Inserted ≈80% of D-proof conclusions. [6794728 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 409.01 ms remaining ; 2 s 45.04 ms total) Tue May 26 09:22:08 2026: Inserted ≈85% of D-proof conclusions. [7219398 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 307.53 ms remaining ; 2 s 50.17 ms total) Tue May 26 09:22:08 2026: Inserted ≈90% of D-proof conclusions. [7644069 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 204.37 ms remaining ; 2 s 43.69 ms total) Tue May 26 09:22:08 2026: Inserted ≈95% of D-proof conclusions. [8068739 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 101.87 ms remaining ; 2 s 37.44 ms total) Tue May 26 09:22:08 2026: Inserted 100% of D-proof conclusions. [8493410 of 8493410] (ETC: Tue May 26 09:22:08 2026 ; 0.00 ms remaining ; 2 s 49.37 ms total) 2049.55 ms (2 s 49.55 ms) total insertion duration. Determined the number of proof string candidates for iteration as 244825238. [most relevant: {25,55} with 2*7425920 = 14851840, i.e. ≈6.07%] Tue May 26 09:22:08 2026: Starting to generate D-proof representatives of length 81. Tue May 26 09:22:56 2026: Iterated ≈ 2% of D-proof candidates. [ 4896504 of 244825238] (ETC: Tue May 26 10:01:56 2026 ; 38 min 59 s 581.22 ms remaining ; 39 min 47 s 327.77 ms total) Tue May 26 09:23:40 2026: Iterated ≈ 4% of D-proof candidates. [ 9793009 of 244825238] (ETC: Tue May 26 10:00:19 2026 ; 36 min 39 s 148.80 ms remaining ; 38 min 10 s 780.00 ms total) Tue May 26 09:24:41 2026: Iterated ≈ 6% of D-proof candidates. [ 14689514 of 244825238] (ETC: Tue May 26 10:04:41 2026 ; 39 min 59 s 634.38 ms remaining ; 42 min 32 s 802.53 ms total) Tue May 26 09:25:37 2026: Iterated ≈ 8% of D-proof candidates. [ 19586019 of 244825238] (ETC: Tue May 26 10:05:37 2026 ; 40 min 404.35 ms remaining ; 43 min 29 s 135.17 ms total) Tue May 26 09:26:48 2026: Iterated ≈10% of D-proof candidates. [ 24482523 of 244825238] (ETC: Tue May 26 10:08:48 2026 ; 41 min 59 s 886.56 ms remaining ; 46 min 39 s 873.94 ms total) Tue May 26 09:27:38 2026: Iterated ≈12% of D-proof candidates. [ 29379028 of 244825238] (ETC: Tue May 26 10:07:53 2026 ; 40 min 15 s 784.73 ms remaining ; 45 min 45 s 209.91 ms total) Tue May 26 09:28:54 2026: Iterated ≈14% of D-proof candidates. [ 34275533 of 244825238] (ETC: Tue May 26 10:10:26 2026 ; 41 min 32 s 440.36 ms remaining ; 48 min 18 s 186.46 ms total) Tue May 26 09:29:51 2026: Iterated ≈16% of D-proof candidates. [ 39172038 of 244825238] (ETC: Tue May 26 10:10:19 2026 ; 40 min 28 s 31.35 ms remaining ; 48 min 10 s 513.51 ms total) Tue May 26 09:30:43 2026: Iterated ≈18% of D-proof candidates. [ 44068542 of 244825238] (ETC: Tue May 26 10:09:48 2026 ; 39 min 5 s 48.88 ms remaining ; 47 min 39 s 815.70 ms total) Tue May 26 09:32:02 2026: Iterated ≈20% of D-proof candidates. [ 48965047 of 244825238] (ETC: Tue May 26 10:11:39 2026 ; 39 min 36 s 481.52 ms remaining ; 49 min 30 s 601.89 ms total) Tue May 26 09:32:59 2026: Iterated ≈22% of D-proof candidates. [ 53861552 of 244825238] (ETC: Tue May 26 10:11:26 2026 ; 38 min 27 s 121.57 ms remaining ; 49 min 17 s 848.16 ms total) Tue May 26 09:34:04 2026: Iterated ≈24% of D-proof candidates. [ 58758057 of 244825238] (ETC: Tue May 26 10:11:51 2026 ; 37 min 46 s 899.51 ms remaining ; 49 min 42 s 762.52 ms total) Tue May 26 09:35:05 2026: Iterated ≈26% of D-proof candidates. [ 63654561 of 244825238] (ETC: Tue May 26 10:11:57 2026 ; 36 min 51 s 526.18 ms remaining ; 49 min 48 s 548.88 ms total) Tue May 26 09:36:04 2026: Iterated ≈28% of D-proof candidates. [ 68551066 of 244825238] (ETC: Tue May 26 10:11:54 2026 ; 35 min 49 s 688.41 ms remaining ; 49 min 45 s 678.34 ms total) Tue May 26 09:36:58 2026: Iterated ≈30% of D-proof candidates. [ 73447571 of 244825238] (ETC: Tue May 26 10:11:35 2026 ; 34 min 36 s 991.40 ms remaining ; 49 min 27 s 130.56 ms total) Tue May 26 09:37:45 2026: Iterated ≈32% of D-proof candidates. [ 78344076 of 244825238] (ETC: Tue May 26 10:10:56 2026 ; 33 min 10 s 653.73 ms remaining ; 48 min 47 s 431.95 ms total) Tue May 26 09:38:30 2026: Iterated ≈34% of D-proof candidates. [ 83240580 of 244825238] (ETC: Tue May 26 10:10:15 2026 ; 31 min 45 s 363.51 ms remaining ; 48 min 6 s 914.39 ms total) Tue May 26 09:39:28 2026: Iterated ≈36% of D-proof candidates. [ 88137085 of 244825238] (ETC: Tue May 26 10:10:17 2026 ; 30 min 48 s 614.54 ms remaining ; 48 min 8 s 460.21 ms total) Tue May 26 09:40:13 2026: Iterated ≈38% of D-proof candidates. [ 93033590 of 244825238] (ETC: Tue May 26 10:09:43 2026 ; 29 min 30 s 199.51 ms remaining ; 47 min 35 s 160.50 ms total) Tue May 26 09:40:59 2026: Iterated ≈40% of D-proof candidates. [ 97930095 of 244825238] (ETC: Tue May 26 10:09:16 2026 ; 28 min 16 s 557.24 ms remaining ; 47 min 7 s 595.40 ms total) Tue May 26 09:41:52 2026: Iterated ≈42% of D-proof candidates. [102826599 of 244825238] (ETC: Tue May 26 10:09:07 2026 ; 27 min 15 s 100.56 ms remaining ; 46 min 59 s 138.88 ms total) Tue May 26 09:42:48 2026: Iterated ≈44% of D-proof candidates. [107723104 of 244825238] (ETC: Tue May 26 10:09:07 2026 ; 26 min 18 s 492.04 ms remaining ; 46 min 58 s 735.76 ms total) Tue May 26 09:43:34 2026: Iterated ≈46% of D-proof candidates. [112619609 of 244825238] (ETC: Tue May 26 10:08:43 2026 ; 25 min 9 s 362.73 ms remaining ; 46 min 35 s 116.15 ms total) Tue May 26 09:44:32 2026: Iterated ≈48% of D-proof candidates. [117516114 of 244825238] (ETC: Tue May 26 10:08:49 2026 ; 24 min 16 s 297.22 ms remaining ; 46 min 40 s 571.58 ms total) Tue May 26 09:45:23 2026: Iterated ≈50% of D-proof candidates. [122412619 of 244825238] (ETC: Tue May 26 10:08:38 2026 ; 23 min 15 s 61.37 ms remaining ; 46 min 30 s 122.73 ms total) Tue May 26 09:46:16 2026: Iterated ≈52% of D-proof candidates. [127309123 of 244825238] (ETC: Tue May 26 10:08:32 2026 ; 22 min 16 s 15.21 ms remaining ; 46 min 23 s 365.01 ms total) Tue May 26 09:47:15 2026: Iterated ≈54% of D-proof candidates. [132205628 of 244825238] (ETC: Tue May 26 10:08:39 2026 ; 21 min 23 s 555.12 ms remaining ; 46 min 30 s 337.20 ms total) Tue May 26 09:48:06 2026: Iterated ≈56% of D-proof candidates. [137102133 of 244825238] (ETC: Tue May 26 10:08:31 2026 ; 20 min 24 s 294.08 ms remaining ; 46 min 22 s 486.54 ms total) Tue May 26 09:48:54 2026: Iterated ≈58% of D-proof candidates. [141998638 of 244825238] (ETC: Tue May 26 10:08:17 2026 ; 19 min 22 s 873.75 ms remaining ; 46 min 8 s 747.02 ms total) Tue May 26 09:49:46 2026: Iterated ≈60% of D-proof candidates. [146895142 of 244825238] (ETC: Tue May 26 10:08:12 2026 ; 18 min 25 s 441.10 ms remaining ; 46 min 3 s 602.73 ms total) Tue May 26 09:50:37 2026: Iterated ≈62% of D-proof candidates. [151791647 of 244825238] (ETC: Tue May 26 10:08:05 2026 ; 17 min 27 s 597.43 ms remaining ; 45 min 56 s 835.32 ms total) Tue May 26 09:51:26 2026: Iterated ≈64% of D-proof candidates. [156688152 of 244825238] (ETC: Tue May 26 10:07:55 2026 ; 16 min 28 s 693.87 ms remaining ; 45 min 46 s 371.84 ms total) Tue May 26 09:52:21 2026: Iterated ≈66% of D-proof candidates. [161584657 of 244825238] (ETC: Tue May 26 10:07:56 2026 ; 15 min 34 s 111.08 ms remaining ; 45 min 47 s 385.53 ms total) Tue May 26 09:53:13 2026: Iterated ≈68% of D-proof candidates. [166481161 of 244825238] (ETC: Tue May 26 10:07:51 2026 ; 14 min 37 s 640.89 ms remaining ; 45 min 42 s 627.74 ms total) Tue May 26 09:54:07 2026: Iterated ≈70% of D-proof candidates. [171377666 of 244825238] (ETC: Tue May 26 10:07:49 2026 ; 13 min 42 s 268.93 ms remaining ; 45 min 40 s 896.40 ms total) Tue May 26 09:55:00 2026: Iterated ≈72% of D-proof candidates. [176274171 of 244825238] (ETC: Tue May 26 10:07:47 2026 ; 12 min 46 s 752.98 ms remaining ; 45 min 38 s 403.48 ms total) Tue May 26 09:55:58 2026: Iterated ≈74% of D-proof candidates. [181170676 of 244825238] (ETC: Tue May 26 10:07:52 2026 ; 11 min 53 s 307.18 ms remaining ; 45 min 43 s 489.14 ms total) Tue May 26 09:57:00 2026: Iterated ≈76% of D-proof candidates. [186067180 of 244825238] (ETC: Tue May 26 10:08:01 2026 ; 11 min 724.26 ms remaining ; 45 min 53 s 17.73 ms total) Tue May 26 09:57:55 2026: Iterated ≈78% of D-proof candidates. [190963685 of 244825238] (ETC: Tue May 26 10:08:00 2026 ; 10 min 5 s 478.31 ms remaining ; 45 min 52 s 174.12 ms total) Tue May 26 09:58:53 2026: Iterated ≈80% of D-proof candidates. [195860190 of 244825238] (ETC: Tue May 26 10:08:04 2026 ; 9 min 11 s 228.14 ms remaining ; 45 min 56 s 140.66 ms total) Tue May 26 09:59:51 2026: Iterated ≈82% of D-proof candidates. [200756695 of 244825238] (ETC: Tue May 26 10:08:08 2026 ; 8 min 16 s 714.82 ms remaining ; 45 min 59 s 526.78 ms total) Tue May 26 10:00:49 2026: Iterated ≈84% of D-proof candidates. [205653199 of 244825238] (ETC: Tue May 26 10:08:11 2026 ; 7 min 22 s 11.44 ms remaining ; 46 min 2 s 571.42 ms total) Tue May 26 10:01:51 2026: Iterated ≈86% of D-proof candidates. [210549704 of 244825238] (ETC: Tue May 26 10:08:19 2026 ; 6 min 27 s 872.94 ms remaining ; 46 min 10 s 520.95 ms total) Tue May 26 10:02:38 2026: Iterated ≈88% of D-proof candidates. [215446209 of 244825238] (ETC: Tue May 26 10:08:09 2026 ; 5 min 31 s 290.06 ms remaining ; 46 min 750.48 ms total) Tue May 26 10:03:28 2026: Iterated ≈90% of D-proof candidates. [220342714 of 244825238] (ETC: Tue May 26 10:08:04 2026 ; 4 min 35 s 535.78 ms remaining ; 45 min 55 s 357.74 ms total) Tue May 26 10:04:20 2026: Iterated ≈92% of D-proof candidates. [225239218 of 244825238] (ETC: Tue May 26 10:08:00 2026 ; 3 min 40 s 157.96 ms remaining ; 45 min 51 s 974.34 ms total) Tue May 26 10:05:18 2026: Iterated ≈94% of D-proof candidates. [230135723 of 244825238] (ETC: Tue May 26 10:08:03 2026 ; 2 min 45 s 306.79 ms remaining ; 45 min 55 s 113.07 ms total) Tue May 26 10:06:14 2026: Iterated ≈96% of D-proof candidates. [235032228 of 244825238] (ETC: Tue May 26 10:08:04 2026 ; 1 min 50 s 224.87 ms remaining ; 45 min 55 s 621.61 ms total) Tue May 26 10:07:05 2026: Iterated ≈98% of D-proof candidates. [239928733 of 244825238] (ETC: Tue May 26 10:08:00 2026 ; 55 s 31.24 ms remaining ; 45 min 51 s 561.83 ms total) Tue May 26 10:07:56 2026: Iterated 100% of D-proof candidates. [244825238 of 244825238] (ETC: Tue May 26 10:07:56 2026 ; 0.00 ms remaining ; 45 min 47 s 846.63 ms total) 2748245.81 ms (45 min 48 s 245.81 ms) taken to collect 35197393 D-proofs of length 81. [iterated 244825238 condensed detachment proof strings] 129562.55 ms (2 min 9 s 562.55 ms) taken to filter and order new representative proofs. Found 35197393 representative, 190867946 redundant, and 18759899 invalid condensed detachment proof strings. lengths up to 81 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,33), (17,45), (19,69), (21,101), (23,140), (25,205), (27,280), (29,404), (31,568), (33,809), (35,1140), (37,1614), (39,2278), (41,3217), (43,4529), (45,6426), (47,9042), (49,12829), (51,18076), (53,25667), (55,36224), (57,51530), (59,72889), (61,103901), (63,147416), (65,210360), (67,299183), (69,427694), (71,609264), (73,872065), (75,1244628), (77,1782980), (79,2547752), (81,35197393)} ; 35197393 new representative proofs (190867946 redundant, 18759899 invalid) Tue May 26 10:10:08 2026: Starting to write 35197393 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81-unfiltered81+.txt. 22743.97 ms (22 s 743.97 ms) taken to print and save 7627643702 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81-unfiltered81+.txt. Tue May 26 10:10:42 2026: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 81, unfiltered, candidate queue capacities: 50, use conclusion strings] Tue May 26 10:10:54 2026: Process terminated. [pid: 401797, tid:22557135808320]