( 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: 1.20111… h CPU utilization: 76.87111… core-h ) Wed May 27 14:27:04 2026: Process started. [pid: 342441, tid:23031488436032] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true) 2. generateDProofRepresentativeFiles(83, 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(83, false, true, null, -1, -1, true). Wed May 27 14:27:04 2026: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 83, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.00 ms taken to load initial representatives. 10.80 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs3.txt. [tid:23030663190080] 11.06 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs5.txt. [tid:23030661088832] 17.04 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs7.txt. [tid:23030658987584] 13.70 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs9.txt. [tid:23030656886336] 13.79 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs11.txt. [tid:23030654785088] 10.73 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs13.txt. [tid:23030652683840] 26.85 ms taken to read 33 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs15.txt. [tid:23030650582592] 16.40 ms taken to read 45 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs17.txt. [tid:23030648481344] 6.41 ms taken to read 69 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs19.txt. [tid:23030646380096] 52.44 ms taken to read 101 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs21.txt. [tid:23030644278848] 23.67 ms taken to read 140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs23.txt. [tid:23030642177600] 17.13 ms taken to read 205 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs25.txt. [tid:23030640076352] 32.53 ms taken to read 280 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs27.txt. [tid:23030637975104] 22.31 ms taken to read 404 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs29.txt. [tid:23030635873856] 18.46 ms taken to read 568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs31.txt. [tid:23030633772608] 26.69 ms taken to read 809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs33.txt. [tid:23030631671360] 24.31 ms taken to read 1140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs35.txt. [tid:23030629570112] 22.54 ms taken to read 1614 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs37.txt. [tid:23030627468864] 27.46 ms taken to read 2278 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs39.txt. [tid:23030625367616] 95.46 ms taken to read 3217 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs41.txt. [tid:23029413312064] 69.41 ms taken to read 4529 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs43.txt. [tid:23029411210816] 183.78 ms taken to read 6426 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs45.txt. [tid:23029409109568] 35.41 ms taken to read 9042 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs47.txt. [tid:23029407008320] 45.97 ms taken to read 12829 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs49.txt. [tid:23029404907072] 51.85 ms taken to read 18076 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs51.txt. [tid:23029402805824] 202.05 ms taken to read 25667 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs53.txt. [tid:23029400704576] 54.62 ms taken to read 36224 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs55.txt. [tid:23029398603328] 177.88 ms taken to read 51530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs57.txt. [tid:23029396502080] 114.56 ms taken to read 72889 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs59.txt. [tid:23029394400832] 228.01 ms taken to read 103901 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs61.txt. [tid:23029392299584] 329.65 ms taken to read 147416 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs63.txt. [tid:23029390198336] 385.26 ms taken to read 210360 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs65.txt. [tid:23029388097088] 592.53 ms taken to read 299183 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs67.txt. [tid:23029385995840] 703.43 ms taken to read 427694 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs69.txt. [tid:23029383894592] 1909.64 ms (1 s 909.64 ms) taken to read 609264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs71.txt. [tid:23029381793344] 1323.39 ms (1 s 323.39 ms) taken to read 872065 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs73.txt. [tid:23029379692096] 1642.10 ms (1 s 642.10 ms) taken to read 1244628 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs75.txt. [tid:23029377590848] 2237.92 ms (2 s 237.92 ms) taken to read 1782980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs77.txt. [tid:23029375489600] 2235.87 ms (2 s 235.87 ms) taken to read 2547752 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs79.txt. [tid:23029373388352] 2886.49 ms (2 s 886.49 ms) taken to read 3653261 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81.txt. [tid:23029371287104] 2966.46 ms (2 s 966.46 ms) total read duration. Loaded 41 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 81 : 3653261 12146671 representatives in total. Wed May 27 14:27:07 2026: Inserted ≈ 5% of D-proof conclusions. [ 607333 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 720.89 ms remaining ; 1 s 811.46 ms total) Wed May 27 14:27:07 2026: Inserted ≈10% of D-proof conclusions. [ 1214667 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 588.94 ms remaining ; 1 s 765.49 ms total) Wed May 27 14:27:07 2026: Inserted ≈15% of D-proof conclusions. [ 1822000 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 486.17 ms remaining ; 1 s 748.44 ms total) Wed May 27 14:27:08 2026: Inserted ≈20% of D-proof conclusions. [ 2429334 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 392.55 ms remaining ; 1 s 740.69 ms total) Wed May 27 14:27:08 2026: Inserted ≈25% of D-proof conclusions. [ 3036667 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 301.44 ms remaining ; 1 s 735.25 ms total) Wed May 27 14:27:08 2026: Inserted ≈30% of D-proof conclusions. [ 3644001 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 214.68 ms remaining ; 1 s 735.26 ms total) Wed May 27 14:27:08 2026: Inserted ≈35% of D-proof conclusions. [ 4251334 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 144.52 ms remaining ; 1 s 760.80 ms total) Wed May 27 14:27:08 2026: Inserted ≈40% of D-proof conclusions. [ 4858668 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 89.16 ms remaining ; 1 s 815.27 ms total) Wed May 27 14:27:08 2026: Inserted ≈45% of D-proof conclusions. [ 5466001 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 1 s 9.19 ms remaining ; 1 s 834.89 ms total) Wed May 27 14:27:08 2026: Inserted ≈50% of D-proof conclusions. [ 6073335 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 929.10 ms remaining ; 1 s 858.19 ms total) Wed May 27 14:27:08 2026: Inserted ≈55% of D-proof conclusions. [ 6680669 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 843.03 ms remaining ; 1 s 873.39 ms total) Wed May 27 14:27:08 2026: Inserted ≈60% of D-proof conclusions. [ 7288002 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 747.34 ms remaining ; 1 s 868.34 ms total) Wed May 27 14:27:08 2026: Inserted ≈65% of D-proof conclusions. [ 7895336 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 662.37 ms remaining ; 1 s 892.49 ms total) Wed May 27 14:27:09 2026: Inserted ≈70% of D-proof conclusions. [ 8502669 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 588.34 ms remaining ; 1 s 961.12 ms total) Wed May 27 14:27:09 2026: Inserted ≈75% of D-proof conclusions. [ 9110003 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 491.31 ms remaining ; 1 s 965.24 ms total) Wed May 27 14:27:09 2026: Inserted ≈80% of D-proof conclusions. [ 9717336 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 395.79 ms remaining ; 1 s 978.95 ms total) Wed May 27 14:27:09 2026: Inserted ≈85% of D-proof conclusions. [10324670 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 297.52 ms remaining ; 1 s 983.44 ms total) Wed May 27 14:27:09 2026: Inserted ≈90% of D-proof conclusions. [10932003 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 199.42 ms remaining ; 1 s 994.19 ms total) Wed May 27 14:27:09 2026: Inserted ≈95% of D-proof conclusions. [11539337 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 100.34 ms remaining ; 2 s 6.74 ms total) Wed May 27 14:27:09 2026: Inserted 100% of D-proof conclusions. [12146671 of 12146671] (ETC: Wed May 27 14:27:09 2026 ; 0.00 ms remaining ; 2 s 22.33 ms total) 2022.45 ms (2 s 22.45 ms) total insertion duration. Determined the number of proof string candidates for iteration as 357996015. [most relevant: {25,57} with 2*10563650 = 21127300, i.e. ≈5.90%] Wed May 27 14:27:09 2026: Starting to generate D-proof representatives of length 83. Wed May 27 14:28:22 2026: Iterated ≈ 2% of D-proof candidates. [ 7159920 of 357996015] (ETC: Wed May 27 15:27:49 2026 ; 59 min 27 s 140.08 ms remaining ; 1 h 39 s 938.85 ms total) Wed May 27 14:29:28 2026: Iterated ≈ 4% of D-proof candidates. [ 14319840 of 357996015] (ETC: Wed May 27 15:25:03 2026 ; 55 min 34 s 508.91 ms remaining ; 57 min 53 s 446.77 ms total) Wed May 27 14:31:04 2026: Iterated ≈ 6% of D-proof candidates. [ 21479760 of 357996015] (ETC: Wed May 27 15:32:28 2026 ; 1 h 1 min 23 s 779.07 ms remaining ; 1 h 5 min 18 s 913.90 ms total) Wed May 27 14:32:30 2026: Iterated ≈ 8% of D-proof candidates. [ 28639681 of 357996015] (ETC: Wed May 27 15:33:59 2026 ; 1 h 1 min 28 s 709.61 ms remaining ; 1 h 6 min 49 s 466.97 ms total) Wed May 27 14:33:59 2026: Iterated ≈10% of D-proof candidates. [ 35799601 of 357996015] (ETC: Wed May 27 15:35:25 2026 ; 1 h 1 min 26 s 181.18 ms remaining ; 1 h 8 min 15 s 756.86 ms total) Wed May 27 14:35:07 2026: Iterated ≈12% of D-proof candidates. [ 42959521 of 357996015] (ETC: Wed May 27 15:33:29 2026 ; 58 min 22 s 13.05 ms remaining ; 1 h 6 min 19 s 560.27 ms total) Wed May 27 14:36:46 2026: Iterated ≈14% of D-proof candidates. [ 50119442 of 357996015] (ETC: Wed May 27 15:35:53 2026 ; 59 min 6 s 79.48 ms remaining ; 1 h 8 min 43 s 348.24 ms total) Wed May 27 14:37:53 2026: Iterated ≈16% of D-proof candidates. [ 57279362 of 357996015] (ETC: Wed May 27 15:34:13 2026 ; 56 min 20 s 261.81 ms remaining ; 1 h 7 min 4 s 121.20 ms total) Wed May 27 14:39:09 2026: Iterated ≈18% of D-proof candidates. [ 64439282 of 357996015] (ETC: Wed May 27 15:33:49 2026 ; 54 min 39 s 622.30 ms remaining ; 1 h 6 min 39 s 539.38 ms total) Wed May 27 14:40:33 2026: Iterated ≈20% of D-proof candidates. [ 71599203 of 357996015] (ETC: Wed May 27 15:34:11 2026 ; 53 min 37 s 60.27 ms remaining ; 1 h 7 min 1 s 325.33 ms total) Wed May 27 14:41:35 2026: Iterated ≈22% of D-proof candidates. [ 78759123 of 357996015] (ETC: Wed May 27 15:32:45 2026 ; 51 min 9 s 877.51 ms remaining ; 1 h 5 min 35 s 740.39 ms total) Wed May 27 14:43:11 2026: Iterated ≈24% of D-proof candidates. [ 85919043 of 357996015] (ETC: Wed May 27 15:33:56 2026 ; 50 min 45 s 20.20 ms remaining ; 1 h 6 min 46 s 605.52 ms total) Wed May 27 14:44:26 2026: Iterated ≈26% of D-proof candidates. [ 93078963 of 357996015] (ETC: Wed May 27 15:33:36 2026 ; 49 min 10 s 27.95 ms remaining ; 1 h 6 min 26 s 524.24 ms total) Wed May 27 14:45:35 2026: Iterated ≈28% of D-proof candidates. [100238884 of 357996015] (ETC: Wed May 27 15:32:59 2026 ; 47 min 23 s 902.44 ms remaining ; 1 h 5 min 49 s 864.50 ms total) Wed May 27 14:46:58 2026: Iterated ≈30% of D-proof candidates. [107398804 of 357996015] (ETC: Wed May 27 15:33:13 2026 ; 46 min 14 s 432.98 ms remaining ; 1 h 6 min 3 s 475.68 ms total) Wed May 27 14:47:59 2026: Iterated ≈32% of D-proof candidates. [114558724 of 357996015] (ETC: Wed May 27 15:32:13 2026 ; 44 min 14 s 867.15 ms remaining ; 1 h 5 min 4 s 216.38 ms total) Wed May 27 14:49:08 2026: Iterated ≈34% of D-proof candidates. [121718645 of 357996015] (ETC: Wed May 27 15:31:48 2026 ; 42 min 39 s 842.98 ms remaining ; 1 h 4 min 38 s 549.97 ms total) Wed May 27 14:50:20 2026: Iterated ≈36% of D-proof candidates. [128878565 of 357996015] (ETC: Wed May 27 15:31:32 2026 ; 41 min 12 s 201.45 ms remaining ; 1 h 4 min 22 s 814.75 ms total) Wed May 27 14:51:34 2026: Iterated ≈38% of D-proof candidates. [136038485 of 357996015] (ETC: Wed May 27 15:31:23 2026 ; 39 min 49 s 201.00 ms remaining ; 1 h 4 min 13 s 549.98 ms total) Wed May 27 14:52:50 2026: Iterated ≈40% of D-proof candidates. [143198406 of 357996015] (ETC: Wed May 27 15:31:21 2026 ; 38 min 30 s 998.66 ms remaining ; 1 h 4 min 11 s 664.44 ms total) Wed May 27 14:54:13 2026: Iterated ≈42% of D-proof candidates. [150358326 of 357996015] (ETC: Wed May 27 15:31:36 2026 ; 37 min 22 s 747.59 ms remaining ; 1 h 4 min 26 s 806.18 ms total) Wed May 27 14:55:28 2026: Iterated ≈44% of D-proof candidates. [157518246 of 357996015] (ETC: Wed May 27 15:31:30 2026 ; 36 min 2 s 225.95 ms remaining ; 1 h 4 min 21 s 117.76 ms total) Wed May 27 14:56:49 2026: Iterated ≈46% of D-proof candidates. [164678166 of 357996015] (ETC: Wed May 27 15:31:39 2026 ; 34 min 49 s 521.97 ms remaining ; 1 h 4 min 29 s 485.12 ms total) Wed May 27 14:58:10 2026: Iterated ≈48% of D-proof candidates. [171838087 of 357996015] (ETC: Wed May 27 15:31:45 2026 ; 33 min 35 s 570.31 ms remaining ; 1 h 4 min 36 s 96.74 ms total) Wed May 27 14:59:39 2026: Iterated ≈50% of D-proof candidates. [178998007 of 357996015] (ETC: Wed May 27 15:32:08 2026 ; 32 min 29 s 421.22 ms remaining ; 1 h 4 min 58 s 842.42 ms total) Wed May 27 15:01:16 2026: Iterated ≈52% of D-proof candidates. [186157927 of 357996015] (ETC: Wed May 27 15:32:46 2026 ; 31 min 29 s 447.52 ms remaining ; 1 h 5 min 36 s 348.99 ms total) Wed May 27 15:02:37 2026: Iterated ≈54% of D-proof candidates. [193317848 of 357996015] (ETC: Wed May 27 15:32:50 2026 ; 30 min 12 s 976.52 ms remaining ; 1 h 5 min 41 s 253.30 ms total) Wed May 27 15:04:02 2026: Iterated ≈56% of D-proof candidates. [200477768 of 357996015] (ETC: Wed May 27 15:33:00 2026 ; 28 min 58 s 294.45 ms remaining ; 1 h 5 min 50 s 669.21 ms total) Wed May 27 15:05:18 2026: Iterated ≈58% of D-proof candidates. [207637688 of 357996015] (ETC: Wed May 27 15:32:55 2026 ; 27 min 37 s 255.65 ms remaining ; 1 h 5 min 45 s 846.76 ms total) Wed May 27 15:06:39 2026: Iterated ≈60% of D-proof candidates. [214797609 of 357996015] (ETC: Wed May 27 15:32:59 2026 ; 26 min 19 s 759.06 ms remaining ; 1 h 5 min 49 s 397.64 ms total) Wed May 27 15:07:52 2026: Iterated ≈62% of D-proof candidates. [221957529 of 357996015] (ETC: Wed May 27 15:32:49 2026 ; 24 min 57 s 217.01 ms remaining ; 1 h 5 min 40 s 44.76 ms total) Wed May 27 15:09:08 2026: Iterated ≈64% of D-proof candidates. [229117449 of 357996015] (ETC: Wed May 27 15:32:44 2026 ; 23 min 36 s 598.63 ms remaining ; 1 h 5 min 34 s 996.18 ms total) Wed May 27 15:10:34 2026: Iterated ≈66% of D-proof candidates. [236277369 of 357996015] (ETC: Wed May 27 15:32:55 2026 ; 22 min 21 s 697.35 ms remaining ; 1 h 5 min 46 s 168.65 ms total) Wed May 27 15:11:54 2026: Iterated ≈68% of D-proof candidates. [243437290 of 357996015] (ETC: Wed May 27 15:32:57 2026 ; 21 min 3 s 418.32 ms remaining ; 1 h 5 min 48 s 182.24 ms total) Wed May 27 15:13:11 2026: Iterated ≈70% of D-proof candidates. [250597210 of 357996015] (ETC: Wed May 27 15:32:54 2026 ; 19 min 43 s 491.42 ms remaining ; 1 h 5 min 44 s 971.38 ms total) Wed May 27 15:14:28 2026: Iterated ≈72% of D-proof candidates. [257757130 of 357996015] (ETC: Wed May 27 15:32:53 2026 ; 18 min 24 s 155.42 ms remaining ; 1 h 5 min 43 s 412.19 ms total) Wed May 27 15:15:57 2026: Iterated ≈74% of D-proof candidates. [264917051 of 357996015] (ETC: Wed May 27 15:33:05 2026 ; 17 min 8 s 529.37 ms remaining ; 1 h 5 min 55 s 882.17 ms total) Wed May 27 15:17:21 2026: Iterated ≈76% of D-proof candidates. [272076971 of 357996015] (ETC: Wed May 27 15:33:13 2026 ; 15 min 51 s 205.28 ms remaining ; 1 h 6 min 3 s 355.30 ms total) Wed May 27 15:18:52 2026: Iterated ≈78% of D-proof candidates. [279236891 of 357996015] (ETC: Wed May 27 15:33:27 2026 ; 14 min 35 s 194.01 ms remaining ; 1 h 6 min 18 s 154.56 ms total) Wed May 27 15:20:19 2026: Iterated ≈80% of D-proof candidates. [286396812 of 357996015] (ETC: Wed May 27 15:33:37 2026 ; 13 min 17 s 466.45 ms remaining ; 1 h 6 min 27 s 332.26 ms total) Wed May 27 15:21:38 2026: Iterated ≈82% of D-proof candidates. [293556732 of 357996015] (ETC: Wed May 27 15:33:36 2026 ; 11 min 57 s 574.88 ms remaining ; 1 h 6 min 26 s 527.09 ms total) Wed May 27 15:23:10 2026: Iterated ≈84% of D-proof candidates. [300716652 of 357996015] (ETC: Wed May 27 15:33:51 2026 ; 10 min 40 s 218.59 ms remaining ; 1 h 6 min 41 s 366.12 ms total) Wed May 27 15:24:37 2026: Iterated ≈86% of D-proof candidates. [307876572 of 357996015] (ETC: Wed May 27 15:33:58 2026 ; 9 min 21 s 274.77 ms remaining ; 1 h 6 min 49 s 105.43 ms total) Wed May 27 15:25:55 2026: Iterated ≈88% of D-proof candidates. [315036493 of 357996015] (ETC: Wed May 27 15:33:56 2026 ; 8 min 797.57 ms remaining ; 1 h 6 min 46 s 646.40 ms total) Wed May 27 15:27:22 2026: Iterated ≈90% of D-proof candidates. [322196413 of 357996015] (ETC: Wed May 27 15:34:03 2026 ; 6 min 41 s 364.18 ms remaining ; 1 h 6 min 53 s 641.73 ms total) Wed May 27 15:28:42 2026: Iterated ≈92% of D-proof candidates. [329356333 of 357996015] (ETC: Wed May 27 15:34:03 2026 ; 5 min 21 s 77.05 ms remaining ; 1 h 6 min 53 s 463.00 ms total) Wed May 27 15:29:59 2026: Iterated ≈94% of D-proof candidates. [336516254 of 357996015] (ETC: Wed May 27 15:34:00 2026 ; 4 min 619.16 ms remaining ; 1 h 6 min 50 s 319.29 ms total) Wed May 27 15:31:28 2026: Iterated ≈96% of D-proof candidates. [343676174 of 357996015] (ETC: Wed May 27 15:34:09 2026 ; 2 min 40 s 783.41 ms remaining ; 1 h 6 min 59 s 585.09 ms total) Wed May 27 15:32:48 2026: Iterated ≈98% of D-proof candidates. [350836094 of 357996015] (ETC: Wed May 27 15:34:09 2026 ; 1 min 20 s 389.96 ms remaining ; 1 h 6 min 59 s 497.69 ms total) Wed May 27 15:34:05 2026: Iterated 100% of D-proof candidates. [357996015 of 357996015] (ETC: Wed May 27 15:34:05 2026 ; 0.00 ms remaining ; 1 h 6 min 56 s 223.40 ms total) 4016704.28 ms (1 h 6 min 56 s 704.28 ms) taken to collect 51074573 D-proofs of length 83. [iterated 357996015 condensed detachment proof strings] 207846.72 ms (3 min 27 s 846.72 ms) taken to filter and order new representative proofs. Found 51074573 representative, 279645319 redundant, and 27276123 invalid condensed detachment proof strings. lengths up to 83 ; 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,3653261), (83,51074573)} ; 51074573 new representative proofs (279645319 redundant, 27276123 invalid) Wed May 27 15:37:37 2026: Starting to write 51074573 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83-unfiltered83+.txt. 36014.58 ms (36 s 14.58 ms) taken to print and save 11398694341 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83-unfiltered83+.txt. Wed May 27 15:38:49 2026: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 83, unfiltered, candidate queue capacities: 50, use conclusion strings] Wed May 27 15:39:08 2026: Process terminated. [pid: 342441, tid:23031488436032]