( 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: 54.7213888… h CPU utilization: 3502.16888… core-h ) Sun May 31 03:21:03 2026: Process started. [pid: 457304, tid:22432755365696] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true) 2. generateDProofRepresentativeFiles(4294967295, 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(4294967295, false, true, null, -1, -1, true). Sun May 31 03:21:03 2026: Unlimited D-proof representative generator started. [parallel ; 64 hardware thread contexts, unfiltered, candidate queue capacities: 50, use conclusion strings] 0.01 ms taken to load initial representatives. 9.19 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs3.txt. [tid:22432140224064] 18.81 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs5.txt. [tid:22432138122816] 5.30 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs7.txt. [tid:22432136021568] 10.90 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs9.txt. [tid:22432133920320] 17.28 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs11.txt. [tid:22432131819072] 8.16 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs13.txt. [tid:22432129717824] 10.32 ms taken to read 33 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs15.txt. [tid:22432127616576] 17.12 ms taken to read 45 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs17.txt. [tid:22432125515328] 16.81 ms taken to read 69 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs19.txt. [tid:22432123414080] 9.83 ms taken to read 101 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs21.txt. [tid:22432121312832] 10.94 ms taken to read 140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs23.txt. [tid:22432119211584] 19.72 ms taken to read 205 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs25.txt. [tid:22432117110336] 7.14 ms taken to read 280 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs27.txt. [tid:22432115009088] 26.06 ms taken to read 404 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs29.txt. [tid:22432112907840] 32.88 ms taken to read 568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs31.txt. [tid:22432110806592] 28.14 ms taken to read 809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs33.txt. [tid:22432108705344] 44.90 ms taken to read 1140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs35.txt. [tid:22432106604096] 19.98 ms taken to read 1614 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs37.txt. [tid:22432104502848] 16.76 ms taken to read 2278 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs39.txt. [tid:22432102401600] 31.75 ms taken to read 3217 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs41.txt. [tid:22432100300352] 38.54 ms taken to read 4529 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs43.txt. [tid:22432098199104] 134.55 ms taken to read 6426 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs45.txt. [tid:22432096097856] 28.28 ms taken to read 9042 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs47.txt. [tid:22432093996608] 100.25 ms taken to read 12829 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs49.txt. [tid:22432091895360] 40.32 ms taken to read 18076 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs51.txt. [tid:22432089794112] 165.93 ms taken to read 25667 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs53.txt. [tid:22432087692864] 52.65 ms taken to read 36224 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs55.txt. [tid:22432085591616] 212.25 ms taken to read 51530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs57.txt. [tid:22432083490368] 124.90 ms taken to read 72889 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs59.txt. [tid:22432081389120] 374.02 ms taken to read 103901 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs61.txt. [tid:22431070680640] 533.85 ms taken to read 147416 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs63.txt. [tid:22431068579392] 557.37 ms taken to read 210360 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs65.txt. [tid:22431066478144] 494.09 ms taken to read 299183 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs67.txt. [tid:22431064376896] 841.72 ms taken to read 427694 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs69.txt. [tid:22431062275648] 1506.76 ms (1 s 506.76 ms) taken to read 609264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs71.txt. [tid:22431060174400] 1129.38 ms (1 s 129.38 ms) taken to read 872065 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs73.txt. [tid:22431058073152] 2153.11 ms (2 s 153.10 ms) taken to read 1244628 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs75.txt. [tid:22431055971904] 2246.79 ms (2 s 246.79 ms) taken to read 1782980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs77.txt. [tid:22431053870656] 2661.59 ms (2 s 661.59 ms) taken to read 2547752 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs79.txt. [tid:22431051769408] 3237.34 ms (3 s 237.34 ms) taken to read 3653261 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81.txt. [tid:22431049668160] 3743.04 ms (3 s 743.04 ms) taken to read 5226411 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83.txt. [tid:22431047566912] 3837.23 ms (3 s 837.23 ms) total read duration. Loaded 42 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 83 : 5226411 17373082 representatives in total. Sun May 31 03:21:07 2026: Inserted ≈ 5% of D-proof conclusions. [ 868654 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 838.16 ms remaining ; 2 s 987.54 ms total) Sun May 31 03:21:08 2026: Inserted ≈10% of D-proof conclusions. [ 1737308 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 669.36 ms remaining ; 2 s 965.95 ms total) Sun May 31 03:21:08 2026: Inserted ≈15% of D-proof conclusions. [ 2605962 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 520.69 ms remaining ; 2 s 965.51 ms total) Sun May 31 03:21:08 2026: Inserted ≈20% of D-proof conclusions. [ 3474616 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 370.80 ms remaining ; 2 s 963.50 ms total) Sun May 31 03:21:08 2026: Inserted ≈25% of D-proof conclusions. [ 4343270 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 259.55 ms remaining ; 3 s 12.73 ms total) Sun May 31 03:21:08 2026: Inserted ≈30% of D-proof conclusions. [ 5211924 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 2 s 101.02 ms remaining ; 3 s 1.45 ms total) Sun May 31 03:21:08 2026: Inserted ≈35% of D-proof conclusions. [ 6080578 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 1 s 949.12 ms remaining ; 2 s 998.64 ms total) Sun May 31 03:21:09 2026: Inserted ≈40% of D-proof conclusions. [ 6949232 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 1 s 837.20 ms remaining ; 3 s 62.01 ms total) Sun May 31 03:21:09 2026: Inserted ≈45% of D-proof conclusions. [ 7817886 of 17373082] (ETC: Sun May 31 03:21:10 2026 ; 1 s 702.91 ms remaining ; 3 s 96.20 ms total) Sun May 31 03:21:09 2026: Inserted ≈50% of D-proof conclusions. [ 8686541 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 1 s 602.40 ms remaining ; 3 s 204.80 ms total) Sun May 31 03:21:09 2026: Inserted ≈55% of D-proof conclusions. [ 9555195 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 1 s 451.08 ms remaining ; 3 s 224.62 ms total) Sun May 31 03:21:09 2026: Inserted ≈60% of D-proof conclusions. [10423849 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 1 s 292.97 ms remaining ; 3 s 232.43 ms total) Sun May 31 03:21:09 2026: Inserted ≈65% of D-proof conclusions. [11292503 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 1 s 143.66 ms remaining ; 3 s 267.61 ms total) Sun May 31 03:21:10 2026: Inserted ≈70% of D-proof conclusions. [12161157 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 996.08 ms remaining ; 3 s 320.26 ms total) Sun May 31 03:21:10 2026: Inserted ≈75% of D-proof conclusions. [13029811 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 831.02 ms remaining ; 3 s 324.06 ms total) Sun May 31 03:21:10 2026: Inserted ≈80% of D-proof conclusions. [13898465 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 665.69 ms remaining ; 3 s 328.43 ms total) Sun May 31 03:21:10 2026: Inserted ≈85% of D-proof conclusions. [14767119 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 503.50 ms remaining ; 3 s 356.63 ms total) Sun May 31 03:21:10 2026: Inserted ≈90% of D-proof conclusions. [15635773 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 336.64 ms remaining ; 3 s 366.44 ms total) Sun May 31 03:21:11 2026: Inserted ≈95% of D-proof conclusions. [16504427 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 170.06 ms remaining ; 3 s 401.14 ms total) Sun May 31 03:21:11 2026: Inserted 100% of D-proof conclusions. [17373082 of 17373082] (ETC: Sun May 31 03:21:11 2026 ; 0.00 ms remaining ; 3 s 449.64 ms total) 3449.93 ms (3 s 449.93 ms) total insertion duration. Determined the number of proof string candidates for iteration as 523212530. [most relevant: {25,59} with 2*14942245 = 29884490, i.e. ≈5.71%] Sun May 31 03:21:11 2026: Starting to generate D-proof representatives of length 85. Sun May 31 03:23:04 2026: Iterated ≈ 2% of D-proof candidates. [ 10464250 of 523212530] (ETC: Sun May 31 04:55:40 2026 ; 1 h 32 min 35 s 549.62 ms remaining ; 1 h 34 min 28 s 928.18 ms total) Sun May 31 03:24:37 2026: Iterated ≈ 4% of D-proof candidates. [ 20928501 of 523212530] (ETC: Sun May 31 04:47:09 2026 ; 1 h 22 min 31 s 891.95 ms remaining ; 1 h 25 min 58 s 220.77 ms total) Sun May 31 03:26:59 2026: Iterated ≈ 6% of D-proof candidates. [ 31392751 of 523212530] (ETC: Sun May 31 04:58:00 2026 ; 1 h 31 min 847.90 ms remaining ; 1 h 36 min 49 s 412.65 ms total) Sun May 31 03:29:03 2026: Iterated ≈ 8% of D-proof candidates. [ 41857002 of 523212530] (ETC: Sun May 31 04:59:33 2026 ; 1 h 30 min 30 s 485.38 ms remaining ; 1 h 38 min 22 s 701.49 ms total) Sun May 31 03:31:11 2026: Iterated ≈10% of D-proof candidates. [ 52321253 of 523212530] (ETC: Sun May 31 05:01:10 2026 ; 1 h 29 min 59 s 573.75 ms remaining ; 1 h 39 min 59 s 526.39 ms total) Sun May 31 03:32:48 2026: Iterated ≈12% of D-proof candidates. [ 62785503 of 523212530] (ETC: Sun May 31 04:57:59 2026 ; 1 h 25 min 11 s 138.78 ms remaining ; 1 h 36 min 48 s 112.24 ms total) Sun May 31 03:35:12 2026: Iterated ≈14% of D-proof candidates. [ 73249754 of 523212530] (ETC: Sun May 31 05:01:21 2026 ; 1 h 26 min 9 s 114.30 ms remaining ; 1 h 40 min 10 s 598.02 ms total) Sun May 31 03:36:51 2026: Iterated ≈16% of D-proof candidates. [ 83714004 of 523212530] (ETC: Sun May 31 04:59:06 2026 ; 1 h 22 min 15 s 44.35 ms remaining ; 1 h 37 min 55 s 52.79 ms total) Sun May 31 03:38:54 2026: Iterated ≈18% of D-proof candidates. [ 94178255 of 523212530] (ETC: Sun May 31 04:59:38 2026 ; 1 h 20 min 43 s 557.76 ms remaining ; 1 h 38 min 26 s 777.75 ms total) Sun May 31 03:40:50 2026: Iterated ≈20% of D-proof candidates. [104642506 of 523212530] (ETC: Sun May 31 04:59:25 2026 ; 1 h 18 min 34 s 989.10 ms remaining ; 1 h 38 min 13 s 736.38 ms total) Sun May 31 03:42:27 2026: Iterated ≈22% of D-proof candidates. [115106756 of 523212530] (ETC: Sun May 31 04:57:50 2026 ; 1 h 15 min 23 s 340.02 ms remaining ; 1 h 36 min 39 s 153.87 ms total) Sun May 31 03:44:46 2026: Iterated ≈24% of D-proof candidates. [125571007 of 523212530] (ETC: Sun May 31 04:59:26 2026 ; 1 h 14 min 40 s 207.33 ms remaining ; 1 h 38 min 15 s 9.64 ms total) Sun May 31 03:46:18 2026: Iterated ≈26% of D-proof candidates. [136035257 of 523212530] (ETC: Sun May 31 04:57:46 2026 ; 1 h 11 min 28 s 380.87 ms remaining ; 1 h 36 min 35 s 109.27 ms total) Sun May 31 03:48:02 2026: Iterated ≈28% of D-proof candidates. [146499508 of 523212530] (ETC: Sun May 31 04:57:07 2026 ; 1 h 9 min 4 s 117.69 ms remaining ; 1 h 35 min 55 s 719.01 ms total) Sun May 31 03:49:56 2026: Iterated ≈30% of D-proof candidates. [156963759 of 523212530] (ETC: Sun May 31 04:57:02 2026 ; 1 h 7 min 5 s 820.73 ms remaining ; 1 h 35 min 51 s 172.47 ms total) Sun May 31 03:51:43 2026: Iterated ≈32% of D-proof candidates. [167428009 of 523212530] (ETC: Sun May 31 04:56:37 2026 ; 1 h 4 min 53 s 599.58 ms remaining ; 1 h 35 min 25 s 881.73 ms total) Sun May 31 03:53:53 2026: Iterated ≈34% of D-proof candidates. [177892260 of 523212530] (ETC: Sun May 31 04:57:22 2026 ; 1 h 3 min 28 s 711.35 ms remaining ; 1 h 36 min 10 s 774.77 ms total) Sun May 31 03:55:42 2026: Iterated ≈36% of D-proof candidates. [188356510 of 523212530] (ETC: Sun May 31 04:57:04 2026 ; 1 h 1 min 22 s 77.75 ms remaining ; 1 h 35 min 53 s 246.48 ms total) Sun May 31 03:57:50 2026: Iterated ≈38% of D-proof candidates. [198820761 of 523212530] (ETC: Sun May 31 04:57:38 2026 ; 59 min 47 s 908.48 ms remaining ; 1 h 36 min 26 s 949.15 ms total) Sun May 31 03:59:51 2026: Iterated ≈40% of D-proof candidates. [209285012 of 523212530] (ETC: Sun May 31 04:57:50 2026 ; 57 min 59 s 797.07 ms remaining ; 1 h 36 min 39 s 661.78 ms total) Sun May 31 04:01:57 2026: Iterated ≈42% of D-proof candidates. [219749262 of 523212530] (ETC: Sun May 31 04:58:15 2026 ; 56 min 18 s 121.02 ms remaining ; 1 h 37 min 4 s 346.58 ms total) Sun May 31 04:03:37 2026: Iterated ≈44% of D-proof candidates. [230213513 of 523212530] (ETC: Sun May 31 04:57:38 2026 ; 54 min 1 s 36.97 ms remaining ; 1 h 36 min 27 s 566.01 ms total) Sun May 31 04:05:37 2026: Iterated ≈46% of D-proof candidates. [240677763 of 523212530] (ETC: Sun May 31 04:57:47 2026 ; 52 min 9 s 823.50 ms remaining ; 1 h 36 min 35 s 969.43 ms total) Sun May 31 04:07:38 2026: Iterated ≈48% of D-proof candidates. [251142014 of 523212530] (ETC: Sun May 31 04:57:58 2026 ; 50 min 19 s 840.20 ms remaining ; 1 h 36 min 47 s 384.99 ms total) Sun May 31 04:09:16 2026: Iterated ≈50% of D-proof candidates. [261606265 of 523212530] (ETC: Sun May 31 04:57:21 2026 ; 48 min 5 s 23.35 ms remaining ; 1 h 36 min 10 s 46.70 ms total) Sun May 31 04:11:05 2026: Iterated ≈52% of D-proof candidates. [272070515 of 523212530] (ETC: Sun May 31 04:57:09 2026 ; 46 min 3 s 938.52 ms remaining ; 1 h 35 min 58 s 205.24 ms total) Sun May 31 04:12:47 2026: Iterated ≈54% of D-proof candidates. [282534766 of 523212530] (ETC: Sun May 31 04:56:45 2026 ; 43 min 57 s 789.71 ms remaining ; 1 h 35 min 34 s 325.46 ms total) Sun May 31 04:14:56 2026: Iterated ≈56% of D-proof candidates. [292999016 of 523212530] (ETC: Sun May 31 04:57:10 2026 ; 42 min 13 s 878.79 ms remaining ; 1 h 35 min 58 s 815.41 ms total) Sun May 31 04:16:51 2026: Iterated ≈58% of D-proof candidates. [303463267 of 523212530] (ETC: Sun May 31 04:57:09 2026 ; 40 min 18 s 436.18 ms remaining ; 1 h 35 min 58 s 181.38 ms total) Sun May 31 04:18:47 2026: Iterated ≈60% of D-proof candidates. [313927518 of 523212530] (ETC: Sun May 31 04:57:10 2026 ; 38 min 23 s 826.55 ms remaining ; 1 h 35 min 59 s 566.38 ms total) Sun May 31 04:20:50 2026: Iterated ≈62% of D-proof candidates. [324391768 of 523212530] (ETC: Sun May 31 04:57:24 2026 ; 36 min 33 s 753.55 ms remaining ; 1 h 36 min 13 s 35.65 ms total) Sun May 31 04:22:50 2026: Iterated ≈64% of D-proof candidates. [334856019 of 523212530] (ETC: Sun May 31 04:57:31 2026 ; 34 min 40 s 736.00 ms remaining ; 1 h 36 min 19 s 822.21 ms total) Sun May 31 04:24:49 2026: Iterated ≈66% of D-proof candidates. [345320269 of 523212530] (ETC: Sun May 31 04:57:36 2026 ; 32 min 47 s 6.02 ms remaining ; 1 h 36 min 25 s 311.80 ms total) Sun May 31 04:26:38 2026: Iterated ≈68% of D-proof candidates. [355784520 of 523212530] (ETC: Sun May 31 04:57:26 2026 ; 30 min 47 s 951.22 ms remaining ; 1 h 36 min 14 s 847.55 ms total) Sun May 31 04:28:36 2026: Iterated ≈70% of D-proof candidates. [366248771 of 523212530] (ETC: Sun May 31 04:57:30 2026 ; 28 min 53 s 778.27 ms remaining ; 1 h 36 min 19 s 260.91 ms total) Sun May 31 04:30:26 2026: Iterated ≈72% of D-proof candidates. [376713021 of 523212530] (ETC: Sun May 31 04:57:22 2026 ; 26 min 55 s 855.55 ms remaining ; 1 h 36 min 10 s 912.64 ms total) Sun May 31 04:33:09 2026: Iterated ≈74% of D-proof candidates. [387177272 of 523212530] (ETC: Sun May 31 04:58:26 2026 ; 25 min 17 s 161.31 ms remaining ; 1 h 37 min 15 s 235.81 ms total) Sun May 31 04:35:25 2026: Iterated ≈76% of D-proof candidates. [397641522 of 523212530] (ETC: Sun May 31 04:58:52 2026 ; 23 min 26 s 591.18 ms remaining ; 1 h 37 min 40 s 796.53 ms total) Sun May 31 04:37:38 2026: Iterated ≈78% of D-proof candidates. [408105773 of 523212530] (ETC: Sun May 31 04:59:12 2026 ; 21 min 33 s 879.94 ms remaining ; 1 h 38 min 1 s 272.44 ms total) Sun May 31 04:39:43 2026: Iterated ≈80% of D-proof candidates. [418570024 of 523212530] (ETC: Sun May 31 04:59:21 2026 ; 19 min 38 s 3.36 ms remaining ; 1 h 38 min 10 s 16.80 ms total) Sun May 31 04:41:38 2026: Iterated ≈82% of D-proof candidates. [429034274 of 523212530] (ETC: Sun May 31 04:59:17 2026 ; 17 min 39 s 588.03 ms remaining ; 1 h 38 min 6 s 600.14 ms total) Sun May 31 04:43:44 2026: Iterated ≈84% of D-proof candidates. [439498525 of 523212530] (ETC: Sun May 31 04:59:27 2026 ; 15 min 43 s 426.25 ms remaining ; 1 h 38 min 16 s 414.04 ms total) Sun May 31 04:45:37 2026: Iterated ≈86% of D-proof candidates. [449962775 of 523212530] (ETC: Sun May 31 04:59:22 2026 ; 13 min 44 s 764.45 ms remaining ; 1 h 38 min 11 s 174.59 ms total) Sun May 31 04:48:04 2026: Iterated ≈88% of D-proof candidates. [460427026 of 523212530] (ETC: Sun May 31 04:59:55 2026 ; 11 min 50 s 936.67 ms remaining ; 1 h 38 min 44 s 472.22 ms total) Sun May 31 04:50:25 2026: Iterated ≈90% of D-proof candidates. [470891277 of 523212530] (ETC: Sun May 31 05:00:20 2026 ; 9 min 54 s 885.32 ms remaining ; 1 h 39 min 8 s 853.22 ms total) Sun May 31 04:52:26 2026: Iterated ≈92% of D-proof candidates. [481355527 of 523212530] (ETC: Sun May 31 05:00:22 2026 ; 7 min 56 s 128.11 ms remaining ; 1 h 39 min 11 s 601.25 ms total) Sun May 31 04:54:25 2026: Iterated ≈94% of D-proof candidates. [491819778 of 523212530] (ETC: Sun May 31 05:00:22 2026 ; 5 min 57 s 69.59 ms remaining ; 1 h 39 min 11 s 159.81 ms total) Sun May 31 04:56:44 2026: Iterated ≈96% of D-proof candidates. [502284028 of 523212530] (ETC: Sun May 31 05:00:43 2026 ; 3 min 58 s 888.43 ms remaining ; 1 h 39 min 32 s 210.60 ms total) Sun May 31 04:58:45 2026: Iterated ≈98% of D-proof candidates. [512748279 of 523212530] (ETC: Sun May 31 05:00:45 2026 ; 1 min 59 s 475.63 ms remaining ; 1 h 39 min 33 s 781.04 ms total) Sun May 31 05:00:55 2026: Iterated 100% of D-proof candidates. [523212530 of 523212530] (ETC: Sun May 31 05:00:55 2026 ; 0.00 ms remaining ; 1 h 39 min 43 s 801.70 ms total) 5984648.96 ms (1 h 39 min 44 s 648.96 ms) taken to collect 74024284 D-proofs of length 85. [iterated 523212530 condensed detachment proof strings] 304744.92 ms (5 min 4 s 744.93 ms) taken to filter and order new representative proofs. Found 74024284 representative, 409514410 redundant, and 39673836 invalid condensed detachment proof strings. lengths up to 85 ; 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,5226411), (85,74024284)} ; 74024284 new representative proofs (409514410 redundant, 39673836 invalid) Sun May 31 05:06:00 2026: Starting to write 74024284 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs85-unfiltered85+.txt. 49371.04 ms (49 s 371.04 ms) taken to print and save 16999648519 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs85-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 1030551239. [most relevant: {1,85} with 2*148048568 = 296097136, i.e. ≈28.73%] Sun May 31 05:07:49 2026: Starting to generate D-proof representatives of length 87. Sun May 31 05:12:25 2026: Iterated ≈ 2% of D-proof candidates. [ 20611024 of 1030551239] (ETC: Sun May 31 08:57:54 2026 ; 3 h 45 min 28 s 551.40 ms remaining ; 3 h 50 min 4 s 644.27 ms total) Sun May 31 05:15:28 2026: Iterated ≈ 4% of D-proof candidates. [ 41222049 of 1030551239] (ETC: Sun May 31 08:19:02 2026 ; 3 h 3 min 33 s 996.06 ms remaining ; 3 h 11 min 12 s 912.56 ms total) Sun May 31 05:18:16 2026: Iterated ≈ 6% of D-proof candidates. [ 61833074 of 1030551239] (ETC: Sun May 31 08:02:02 2026 ; 2 h 43 min 45 s 121.78 ms remaining ; 2 h 54 min 12 s 257.21 ms total) Sun May 31 05:21:13 2026: Iterated ≈ 8% of D-proof candidates. [ 82444099 of 1030551239] (ETC: Sun May 31 07:55:16 2026 ; 2 h 34 min 2 s 628.58 ms remaining ; 2 h 47 min 26 s 335.41 ms total) Sun May 31 05:24:12 2026: Iterated ≈10% of D-proof candidates. [ 103055123 of 1030551239] (ETC: Sun May 31 07:51:37 2026 ; 2 h 27 min 24 s 505.24 ms remaining ; 2 h 43 min 47 s 228.03 ms total) Sun May 31 05:27:05 2026: Iterated ≈12% of D-proof candidates. [ 123666148 of 1030551239] (ETC: Sun May 31 07:48:19 2026 ; 2 h 21 min 13 s 767.77 ms remaining ; 2 h 40 min 29 s 281.55 ms total) Sun May 31 05:30:38 2026: Iterated ≈14% of D-proof candidates. [ 144277173 of 1030551239] (ETC: Sun May 31 07:50:45 2026 ; 2 h 20 min 7 s 250.62 ms remaining ; 2 h 42 min 55 s 872.81 ms total) Sun May 31 05:33:59 2026: Iterated ≈16% of D-proof candidates. [ 164888198 of 1030551239] (ETC: Sun May 31 07:51:20 2026 ; 2 h 17 min 21 s 233.81 ms remaining ; 2 h 43 min 30 s 992.63 ms total) Sun May 31 05:37:22 2026: Iterated ≈18% of D-proof candidates. [ 185499223 of 1030551239] (ETC: Sun May 31 07:52:00 2026 ; 2 h 14 min 37 s 234.74 ms remaining ; 2 h 44 min 10 s 286.27 ms total) Sun May 31 05:40:35 2026: Iterated ≈20% of D-proof candidates. [ 206110247 of 1030551239] (ETC: Sun May 31 07:51:38 2026 ; 2 h 11 min 3 s 280.95 ms remaining ; 2 h 43 min 49 s 101.18 ms total) Sun May 31 05:43:34 2026: Iterated ≈22% of D-proof candidates. [ 226721272 of 1030551239] (ETC: Sun May 31 07:50:16 2026 ; 2 h 6 min 42 s 480.65 ms remaining ; 2 h 42 min 26 s 770.05 ms total) Sun May 31 05:46:33 2026: Iterated ≈24% of D-proof candidates. [ 247332297 of 1030551239] (ETC: Sun May 31 07:49:11 2026 ; 2 h 2 min 37 s 842.54 ms remaining ; 2 h 41 min 21 s 371.75 ms total) Sun May 31 05:49:24 2026: Iterated ≈26% of D-proof candidates. [ 267943322 of 1030551239] (ETC: Sun May 31 07:47:44 2026 ; 1 h 58 min 19 s 950.28 ms remaining ; 2 h 39 min 54 s 527.40 ms total) Sun May 31 05:52:12 2026: Iterated ≈28% of D-proof candidates. [ 288554346 of 1030551239] (ETC: Sun May 31 07:46:19 2026 ; 1 h 54 min 6 s 679.32 ms remaining ; 2 h 38 min 29 s 276.82 ms total) Sun May 31 05:56:16 2026: Iterated ≈30% of D-proof candidates. [ 309165371 of 1030551239] (ETC: Sun May 31 07:49:18 2026 ; 1 h 53 min 2 s 308.83 ms remaining ; 2 h 41 min 29 s 12.60 ms total) Sun May 31 06:00:12 2026: Iterated ≈32% of D-proof candidates. [ 329776396 of 1030551239] (ETC: Sun May 31 07:51:32 2026 ; 1 h 51 min 19 s 103.29 ms remaining ; 2 h 43 min 42 s 210.72 ms total) Sun May 31 06:04:00 2026: Iterated ≈34% of D-proof candidates. [ 350387421 of 1030551239] (ETC: Sun May 31 07:53:03 2026 ; 1 h 49 min 3 s 63.29 ms remaining ; 2 h 45 min 13 s 732.25 ms total) Sun May 31 06:08:28 2026: Iterated ≈36% of D-proof candidates. [ 370998446 of 1030551239] (ETC: Sun May 31 07:56:17 2026 ; 1 h 47 min 48 s 934.05 ms remaining ; 2 h 48 min 27 s 709.45 ms total) Sun May 31 06:11:42 2026: Iterated ≈38% of D-proof candidates. [ 391609470 of 1030551239] (ETC: Sun May 31 07:55:56 2026 ; 1 h 44 min 13 s 717.62 ms remaining ; 2 h 48 min 6 s 641.30 ms total) Sun May 31 06:15:55 2026: Iterated ≈40% of D-proof candidates. [ 412220495 of 1030551239] (ETC: Sun May 31 07:58:03 2026 ; 1 h 42 min 8 s 44.36 ms remaining ; 2 h 50 min 13 s 407.26 ms total) Sun May 31 06:19:19 2026: Iterated ≈42% of D-proof candidates. [ 432831520 of 1030551239] (ETC: Sun May 31 07:58:03 2026 ; 1 h 38 min 43 s 744.00 ms remaining ; 2 h 50 min 13 s 351.71 ms total) Sun May 31 06:23:45 2026: Iterated ≈44% of D-proof candidates. [ 453442545 of 1030551239] (ETC: Sun May 31 08:00:23 2026 ; 1 h 36 min 38 s 139.94 ms remaining ; 2 h 52 min 33 s 821.32 ms total) Sun May 31 06:27:17 2026: Iterated ≈46% of D-proof candidates. [ 474053569 of 1030551239] (ETC: Sun May 31 08:00:34 2026 ; 1 h 33 min 16 s 841.04 ms remaining ; 2 h 52 min 44 s 520.43 ms total) Sun May 31 06:30:57 2026: Iterated ≈48% of D-proof candidates. [ 494664594 of 1030551239] (ETC: Sun May 31 08:01:00 2026 ; 1 h 30 min 2 s 888.34 ms remaining ; 2 h 53 min 10 s 169.87 ms total) Sun May 31 06:34:27 2026: Iterated ≈50% of D-proof candidates. [ 515275619 of 1030551239] (ETC: Sun May 31 08:01:04 2026 ; 1 h 26 min 37 s 473.90 ms remaining ; 2 h 53 min 14 s 947.79 ms total) Sun May 31 06:37:57 2026: Iterated ≈52% of D-proof candidates. [ 535886644 of 1030551239] (ETC: Sun May 31 08:01:08 2026 ; 1 h 23 min 11 s 253.67 ms remaining ; 2 h 53 min 18 s 445.14 ms total) Sun May 31 06:41:44 2026: Iterated ≈54% of D-proof candidates. [ 556497669 of 1030551239] (ETC: Sun May 31 08:01:43 2026 ; 1 h 19 min 59 s 588.77 ms remaining ; 2 h 53 min 53 s 888.63 ms total) Sun May 31 06:45:28 2026: Iterated ≈56% of D-proof candidates. [ 577108693 of 1030551239] (ETC: Sun May 31 08:02:10 2026 ; 1 h 16 min 42 s 891.00 ms remaining ; 2 h 54 min 21 s 115.89 ms total) Sun May 31 06:49:07 2026: Iterated ≈58% of D-proof candidates. [ 597719718 of 1030551239] (ETC: Sun May 31 08:02:27 2026 ; 1 h 13 min 20 s 721.70 ms remaining ; 2 h 54 min 37 s 908.81 ms total) Sun May 31 06:52:54 2026: Iterated ≈60% of D-proof candidates. [ 618330743 of 1030551239] (ETC: Sun May 31 08:02:58 2026 ; 1 h 10 min 3 s 303.28 ms remaining ; 2 h 55 min 8 s 258.20 ms total) Sun May 31 06:56:38 2026: Iterated ≈62% of D-proof candidates. [ 638941768 of 1030551239] (ETC: Sun May 31 08:03:19 2026 ; 1 h 6 min 41 s 239.71 ms remaining ; 2 h 55 min 29 s 578.18 ms total) Sun May 31 07:00:31 2026: Iterated ≈64% of D-proof candidates. [ 659552792 of 1030551239] (ETC: Sun May 31 08:03:55 2026 ; 1 h 3 min 23 s 503.46 ms remaining ; 2 h 56 min 5 s 287.37 ms total) Sun May 31 07:04:19 2026: Iterated ≈66% of D-proof candidates. [ 680163817 of 1030551239] (ETC: Sun May 31 08:04:20 2026 ; 1 h 735.01 ms remaining ; 2 h 56 min 30 s 397.07 ms total) Sun May 31 07:08:04 2026: Iterated ≈68% of D-proof candidates. [ 700774842 of 1030551239] (ETC: Sun May 31 08:04:39 2026 ; 56 min 35 s 114.62 ms remaining ; 2 h 56 min 49 s 733.17 ms total) Sun May 31 07:11:55 2026: Iterated ≈70% of D-proof candidates. [ 721385867 of 1030551239] (ETC: Sun May 31 08:05:06 2026 ; 53 min 11 s 123.44 ms remaining ; 2 h 57 min 17 s 78.12 ms total) Sun May 31 07:15:41 2026: Iterated ≈72% of D-proof candidates. [ 741996892 of 1030551239] (ETC: Sun May 31 08:05:25 2026 ; 49 min 43 s 464.50 ms remaining ; 2 h 57 min 35 s 230.36 ms total) Sun May 31 07:19:40 2026: Iterated ≈74% of D-proof candidates. [ 762607916 of 1030551239] (ETC: Sun May 31 08:05:59 2026 ; 46 min 19 s 292.75 ms remaining ; 2 h 58 min 9 s 587.47 ms total) Sun May 31 07:23:20 2026: Iterated ≈76% of D-proof candidates. [ 783218941 of 1030551239] (ETC: Sun May 31 08:06:08 2026 ; 42 min 47 s 622.82 ms remaining ; 2 h 58 min 18 s 428.39 ms total) Sun May 31 07:27:23 2026: Iterated ≈78% of D-proof candidates. [ 803829966 of 1030551239] (ETC: Sun May 31 08:06:45 2026 ; 39 min 21 s 894.86 ms remaining ; 2 h 58 min 55 s 885.69 ms total) Sun May 31 07:31:13 2026: Iterated ≈80% of D-proof candidates. [ 824440991 of 1030551239] (ETC: Sun May 31 08:07:04 2026 ; 35 min 50 s 961.70 ms remaining ; 2 h 59 min 14 s 808.51 ms total) Sun May 31 07:35:14 2026: Iterated ≈82% of D-proof candidates. [ 845052015 of 1030551239] (ETC: Sun May 31 08:07:35 2026 ; 32 min 21 s 401.81 ms remaining ; 2 h 59 min 45 s 565.56 ms total) Sun May 31 07:39:32 2026: Iterated ≈84% of D-proof candidates. [ 865663040 of 1030551239] (ETC: Sun May 31 08:08:26 2026 ; 28 min 53 s 805.74 ms remaining ; 3 h 36 s 285.85 ms total) Sun May 31 07:43:04 2026: Iterated ≈86% of D-proof candidates. [ 886274065 of 1030551239] (ETC: Sun May 31 08:08:20 2026 ; 25 min 16 s 299.07 ms remaining ; 3 h 30 s 707.58 ms total) Sun May 31 07:47:09 2026: Iterated ≈88% of D-proof candidates. [ 906885090 of 1030551239] (ETC: Sun May 31 08:08:52 2026 ; 21 min 43 s 572.12 ms remaining ; 3 h 1 min 3 s 100.99 ms total) Sun May 31 07:51:05 2026: Iterated ≈90% of D-proof candidates. [ 927496115 of 1030551239] (ETC: Sun May 31 08:09:14 2026 ; 18 min 8 s 446.52 ms remaining ; 3 h 1 min 24 s 465.21 ms total) Sun May 31 07:55:01 2026: Iterated ≈92% of D-proof candidates. [ 948107139 of 1030551239] (ETC: Sun May 31 08:09:34 2026 ; 14 min 32 s 350.72 ms remaining ; 3 h 1 min 44 s 383.85 ms total) Sun May 31 07:58:53 2026: Iterated ≈94% of D-proof candidates. [ 968718164 of 1030551239] (ETC: Sun May 31 08:09:48 2026 ; 10 min 55 s 129.13 ms remaining ; 3 h 1 min 58 s 818.78 ms total) Sun May 31 08:03:08 2026: Iterated ≈96% of D-proof candidates. [ 989329189 of 1030551239] (ETC: Sun May 31 08:10:26 2026 ; 7 min 18 s 261.63 ms remaining ; 3 h 2 min 36 s 540.59 ms total) Sun May 31 08:06:57 2026: Iterated ≈98% of D-proof candidates. [1009940214 of 1030551239] (ETC: Sun May 31 08:10:36 2026 ; 3 min 39 s 330.05 ms remaining ; 3 h 2 min 46 s 502.27 ms total) Sun May 31 08:10:37 2026: Iterated 100% of D-proof candidates. [1030551239 of 1030551239] (ETC: Sun May 31 08:10:37 2026 ; 0.00 ms remaining ; 3 h 2 min 47 s 179.29 ms total) 10970280.77 ms (3 h 2 min 50 s 280.77 ms) taken to collect 185049299 D-proofs of length 87. [iterated 1030551239 condensed detachment proof strings] 912743.50 ms (15 min 12 s 743.50 ms) taken to filter and order new representative proofs. Found 185049299 representative, 713398627 redundant, and 132103313 invalid condensed detachment proof strings. lengths up to 87 ; 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,5226411), (85,74024284), (87,185049299)} ; 185049299 new representative proofs (713398627 redundant, 132103313 invalid) Sun May 31 08:25:53 2026: Starting to write 185049299 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs87-unfiltered85+.txt. 136293.64 ms (2 min 16 s 293.64 ms) taken to print and save 44053459224 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs87-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 1946752696. [most relevant: {1,87} with 2*370098598 = 740197196, i.e. ≈38.02%] Sun May 31 08:31:26 2026: Starting to generate D-proof representatives of length 89. Sun May 31 08:41:48 2026: Iterated ≈ 2% of D-proof candidates. [ 38935053 of 1946752696] (ETC: Sun May 31 17:09:16 2026 ; 8 h 27 min 28 s 86.82 ms remaining ; 8 h 37 min 49 s 476.33 ms total) Sun May 31 08:49:02 2026: Iterated ≈ 4% of D-proof candidates. [ 77870107 of 1946752696] (ETC: Sun May 31 15:51:06 2026 ; 7 h 2 min 4 s 592.23 ms remaining ; 7 h 19 min 39 s 783.56 ms total) Sun May 31 08:56:41 2026: Iterated ≈ 6% of D-proof candidates. [ 116805161 of 1946752696] (ETC: Sun May 31 15:32:04 2026 ; 6 h 35 min 23 s 515.62 ms remaining ; 7 h 37 s 782.56 ms total) Sun May 31 09:04:15 2026: Iterated ≈ 8% of D-proof candidates. [ 155740215 of 1946752696] (ETC: Sun May 31 15:21:27 2026 ; 6 h 17 min 12 s 557.32 ms remaining ; 6 h 50 min 605.77 ms total) Sun May 31 09:10:12 2026: Iterated ≈10% of D-proof candidates. [ 194675269 of 1946752696] (ETC: Sun May 31 14:58:58 2026 ; 5 h 48 min 46 s 394.92 ms remaining ; 6 h 27 min 31 s 549.90 ms total) Sun May 31 09:16:07 2026: Iterated ≈12% of D-proof candidates. [ 233610323 of 1946752696] (ETC: Sun May 31 14:43:43 2026 ; 5 h 27 min 36 s 556.76 ms remaining ; 6 h 12 min 16 s 996.31 ms total) Sun May 31 09:22:54 2026: Iterated ≈14% of D-proof candidates. [ 272545377 of 1946752696] (ETC: Sun May 31 14:39:04 2026 ; 5 h 16 min 9 s 221.04 ms remaining ; 6 h 7 min 37 s 233.76 ms total) Sun May 31 09:29:23 2026: Iterated ≈16% of D-proof candidates. [ 311480431 of 1946752696] (ETC: Sun May 31 14:33:36 2026 ; 5 h 4 min 12 s 891.93 ms remaining ; 6 h 2 min 9 s 633.25 ms total) Sun May 31 09:36:20 2026: Iterated ≈18% of D-proof candidates. [ 350415485 of 1946752696] (ETC: Sun May 31 14:32:00 2026 ; 4 h 55 min 39 s 350.82 ms remaining ; 6 h 33 s 354.66 ms total) Sun May 31 09:43:01 2026: Iterated ≈20% of D-proof candidates. [ 389350539 of 1946752696] (ETC: Sun May 31 14:29:20 2026 ; 4 h 46 min 18 s 937.25 ms remaining ; 5 h 57 min 53 s 671.56 ms total) Sun May 31 09:50:23 2026: Iterated ≈22% of D-proof candidates. [ 428285593 of 1946752696] (ETC: Sun May 31 14:30:16 2026 ; 4 h 39 min 53 s 190.73 ms remaining ; 5 h 58 min 49 s 731.71 ms total) Sun May 31 09:58:03 2026: Iterated ≈24% of D-proof candidates. [ 467220647 of 1946752696] (ETC: Sun May 31 14:32:18 2026 ; 4 h 34 min 15 s 279.51 ms remaining ; 6 h 51 s 683.57 ms total) Sun May 31 10:04:20 2026: Iterated ≈26% of D-proof candidates. [ 506155700 of 1946752696] (ETC: Sun May 31 14:28:42 2026 ; 4 h 24 min 22 s 200.49 ms remaining ; 5 h 57 min 15 s 406.05 ms total) Sun May 31 10:10:29 2026: Iterated ≈28% of D-proof candidates. [ 545090754 of 1946752696] (ETC: Sun May 31 14:25:09 2026 ; 4 h 14 min 40 s 425.44 ms remaining ; 5 h 53 min 42 s 813.10 ms total) Sun May 31 10:16:30 2026: Iterated ≈30% of D-proof candidates. [ 584025808 of 1946752696] (ETC: Sun May 31 14:21:38 2026 ; 4 h 5 min 8 s 94.13 ms remaining ; 5 h 50 min 11 s 563.03 ms total) Sun May 31 10:22:41 2026: Iterated ≈32% of D-proof candidates. [ 622960862 of 1946752696] (ETC: Sun May 31 14:19:06 2026 ; 3 h 56 min 24 s 215.03 ms remaining ; 5 h 47 min 39 s 139.74 ms total) Sun May 31 10:29:08 2026: Iterated ≈34% of D-proof candidates. [ 661895916 of 1946752696] (ETC: Sun May 31 14:17:35 2026 ; 3 h 48 min 27 s 521.23 ms remaining ; 5 h 46 min 8 s 971.55 ms total) Sun May 31 10:35:43 2026: Iterated ≈36% of D-proof candidates. [ 700830970 of 1946752696] (ETC: Sun May 31 14:16:38 2026 ; 3 h 40 min 55 s 485.32 ms remaining ; 5 h 45 min 11 s 695.81 ms total) Sun May 31 10:42:25 2026: Iterated ≈38% of D-proof candidates. [ 739766024 of 1946752696] (ETC: Sun May 31 14:16:06 2026 ; 3 h 33 min 41 s 224.10 ms remaining ; 5 h 44 min 39 s 393.71 ms total) Sun May 31 10:49:20 2026: Iterated ≈40% of D-proof candidates. [ 778701078 of 1946752696] (ETC: Sun May 31 14:16:10 2026 ; 3 h 26 min 50 s 152.00 ms remaining ; 5 h 44 min 43 s 586.65 ms total) Sun May 31 10:56:29 2026: Iterated ≈42% of D-proof candidates. [ 817636132 of 1946752696] (ETC: Sun May 31 14:16:46 2026 ; 3 h 20 min 17 s 399.23 ms remaining ; 5 h 45 min 19 s 653.83 ms total) Sun May 31 11:04:28 2026: Iterated ≈44% of D-proof candidates. [ 856571186 of 1946752696] (ETC: Sun May 31 14:19:14 2026 ; 3 h 14 min 45 s 682.88 ms remaining ; 5 h 47 min 47 s 290.85 ms total) Sun May 31 11:12:26 2026: Iterated ≈46% of D-proof candidates. [ 895506240 of 1946752696] (ETC: Sun May 31 14:21:25 2026 ; 3 h 8 min 59 s 18.39 ms remaining ; 5 h 49 min 58 s 182.19 ms total) Sun May 31 11:20:52 2026: Iterated ≈48% of D-proof candidates. [ 934441294 of 1946752696] (ETC: Sun May 31 14:24:25 2026 ; 3 h 3 min 32 s 640.22 ms remaining ; 5 h 52 min 58 s 154.26 ms total) Sun May 31 11:28:46 2026: Iterated ≈50% of D-proof candidates. [ 973376348 of 1946752696] (ETC: Sun May 31 14:26:06 2026 ; 2 h 57 min 19 s 567.26 ms remaining ; 5 h 54 min 39 s 134.52 ms total) Sun May 31 11:35:28 2026: Iterated ≈52% of D-proof candidates. [1012311401 of 1946752696] (ETC: Sun May 31 14:25:20 2026 ; 2 h 49 min 52 s 26.20 ms remaining ; 5 h 53 min 53 s 387.90 ms total) Sun May 31 11:43:29 2026: Iterated ≈54% of D-proof candidates. [1051246455 of 1946752696] (ETC: Sun May 31 14:27:04 2026 ; 2 h 43 min 35 s 421.16 ms remaining ; 5 h 55 min 37 s 872.07 ms total) Sun May 31 11:51:28 2026: Iterated ≈56% of D-proof candidates. [1090181509 of 1946752696] (ETC: Sun May 31 14:28:37 2026 ; 2 h 37 min 9 s 562.19 ms remaining ; 5 h 57 min 10 s 823.13 ms total) Sun May 31 11:58:15 2026: Iterated ≈58% of D-proof candidates. [1129116563 of 1946752696] (ETC: Sun May 31 14:28:01 2026 ; 2 h 29 min 45 s 647.88 ms remaining ; 5 h 56 min 34 s 399.70 ms total) Sun May 31 12:05:19 2026: Iterated ≈60% of D-proof candidates. [1168051617 of 1946752696] (ETC: Sun May 31 14:27:53 2026 ; 2 h 22 min 34 s 709.13 ms remaining ; 5 h 56 min 26 s 772.81 ms total) Sun May 31 12:12:18 2026: Iterated ≈62% of D-proof candidates. [1206986671 of 1946752696] (ETC: Sun May 31 14:27:40 2026 ; 2 h 15 min 21 s 955.50 ms remaining ; 5 h 56 min 13 s 567.10 ms total) Sun May 31 12:19:35 2026: Iterated ≈64% of D-proof candidates. [1245921725 of 1946752696] (ETC: Sun May 31 14:27:55 2026 ; 2 h 8 min 19 s 784.82 ms remaining ; 5 h 56 min 28 s 291.16 ms total) Sun May 31 12:26:38 2026: Iterated ≈66% of D-proof candidates. [1284856779 of 1946752696] (ETC: Sun May 31 14:27:47 2026 ; 2 h 1 min 9 s 451.60 ms remaining ; 5 h 56 min 20 s 740.00 ms total) Sun May 31 12:33:57 2026: Iterated ≈68% of D-proof candidates. [1323791833 of 1946752696] (ETC: Sun May 31 14:28:04 2026 ; 1 h 54 min 7 s 361.70 ms remaining ; 5 h 56 min 38 s 5.29 ms total) Sun May 31 12:41:15 2026: Iterated ≈70% of D-proof candidates. [1362726887 of 1946752696] (ETC: Sun May 31 14:28:19 2026 ; 1 h 47 min 3 s 613.27 ms remaining ; 5 h 56 min 52 s 44.22 ms total) Sun May 31 12:48:49 2026: Iterated ≈72% of D-proof candidates. [1401661941 of 1946752696] (ETC: Sun May 31 14:28:54 2026 ; 1 h 40 min 5 s 399.04 ms remaining ; 5 h 57 min 27 s 853.71 ms total) Sun May 31 12:56:35 2026: Iterated ≈74% of D-proof candidates. [1440596995 of 1946752696] (ETC: Sun May 31 14:29:45 2026 ; 1 h 33 min 9 s 509.07 ms remaining ; 5 h 58 min 18 s 111.82 ms total) Sun May 31 13:04:01 2026: Iterated ≈76% of D-proof candidates. [1479532048 of 1946752696] (ETC: Sun May 31 14:30:06 2026 ; 1 h 26 min 4 s 631.06 ms remaining ; 5 h 58 min 39 s 296.02 ms total) Sun May 31 13:11:34 2026: Iterated ≈78% of D-proof candidates. [1518467102 of 1946752696] (ETC: Sun May 31 14:30:35 2026 ; 1 h 19 min 668.73 ms remaining ; 5 h 59 min 8 s 494.20 ms total) Sun May 31 13:18:39 2026: Iterated ≈80% of D-proof candidates. [1557402156 of 1946752696] (ETC: Sun May 31 14:30:28 2026 ; 1 h 11 min 48 s 225.91 ms remaining ; 5 h 59 min 1 s 129.50 ms total) Sun May 31 13:26:21 2026: Iterated ≈82% of D-proof candidates. [1596337210 of 1946752696] (ETC: Sun May 31 14:31:05 2026 ; 1 h 4 min 44 s 111.31 ms remaining ; 5 h 59 min 38 s 396.13 ms total) Sun May 31 13:34:08 2026: Iterated ≈84% of D-proof candidates. [1635272264 of 1946752696] (ETC: Sun May 31 14:31:48 2026 ; 57 min 39 s 425.80 ms remaining ; 6 h 21 s 411.23 ms total) Sun May 31 13:41:38 2026: Iterated ≈86% of D-proof candidates. [1674207318 of 1946752696] (ETC: Sun May 31 14:32:07 2026 ; 50 min 29 s 717.84 ms remaining ; 6 h 40 s 841.68 ms total) Sun May 31 13:48:41 2026: Iterated ≈88% of D-proof candidates. [1713142372 of 1946752696] (ETC: Sun May 31 14:31:56 2026 ; 43 min 15 s 562.39 ms remaining ; 6 h 29 s 686.54 ms total) Sun May 31 13:56:00 2026: Iterated ≈90% of D-proof candidates. [1752077426 of 1946752696] (ETC: Sun May 31 14:32:04 2026 ; 36 min 3 s 754.59 ms remaining ; 6 h 37 s 545.86 ms total) Sun May 31 14:03:38 2026: Iterated ≈92% of D-proof candidates. [1791012480 of 1946752696] (ETC: Sun May 31 14:32:32 2026 ; 28 min 53 s 209.58 ms remaining ; 6 h 1 min 5 s 119.73 ms total) Sun May 31 14:10:59 2026: Iterated ≈94% of D-proof candidates. [1829947534 of 1946752696] (ETC: Sun May 31 14:32:39 2026 ; 21 min 40 s 378.25 ms remaining ; 6 h 1 min 12 s 970.71 ms total) Sun May 31 14:18:45 2026: Iterated ≈96% of D-proof candidates. [1868882588 of 1946752696] (ETC: Sun May 31 14:33:14 2026 ; 14 min 28 s 291.19 ms remaining ; 6 h 1 min 47 s 279.71 ms total) Sun May 31 14:26:12 2026: Iterated ≈98% of D-proof candidates. [1907817642 of 1946752696] (ETC: Sun May 31 14:33:27 2026 ; 7 min 14 s 404.09 ms remaining ; 6 h 2 min 204.69 ms total) Sun May 31 14:33:57 2026: Iterated 100% of D-proof candidates. [1946752696 of 1946752696] (ETC: Sun May 31 14:33:56 2026 ; 0.00 ms remaining ; 6 h 2 min 29 s 994.45 ms total) 21759178.59 ms (6 h 2 min 39 s 178.59 ms) taken to collect 364350012 D-proofs of length 89. [iterated 1946752696 condensed detachment proof strings] 2314452.84 ms (38 min 34 s 452.84 ms) taken to filter and order new representative proofs. Found 364350012 representative, 1204136169 redundant, and 378266515 invalid condensed detachment proof strings. lengths up to 89 ; 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,5226411), (85,74024284), (87,185049299), (89,364350012)} ; 364350012 new representative proofs (1204136169 redundant, 378266515 invalid) Sun May 31 15:12:40 2026: Starting to write 364350012 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs89-unfiltered85+.txt. 341995.62 ms (5 min 41 s 995.62 ms) taken to print and save 98473888755 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs89-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 3507582456. [most relevant: {1,89} with 2*728700024 = 1457400048, i.e. ≈41.55%] Sun May 31 15:27:04 2026: Starting to generate D-proof representatives of length 91. Sun May 31 15:50:57 2026: Iterated ≈ 2% of D-proof candidates. [ 70151649 of 3507582456] (ETC: Mon Jun 1 11:21:08 2026 ; 19 h 30 min 11 s 697.54 ms remaining ; 19 h 54 min 4 s 589.32 ms total) Sun May 31 16:11:30 2026: Iterated ≈ 4% of D-proof candidates. [ 140303298 of 3507582456] (ETC: Mon Jun 1 09:58:09 2026 ; 17 h 46 min 38 s 520.74 ms remaining ; 18 h 31 min 5 s 125.76 ms total) Sun May 31 16:26:40 2026: Iterated ≈ 6% of D-proof candidates. [ 210454947 of 3507582456] (ETC: Mon Jun 1 08:00:34 2026 ; 15 h 33 min 54 s 63.82 ms remaining ; 16 h 33 min 30 s 706.19 ms total) Sun May 31 16:40:50 2026: Iterated ≈ 8% of D-proof candidates. [ 280606596 of 3507582456] (ETC: Mon Jun 1 06:49:10 2026 ; 14 h 8 min 20 s 423.54 ms remaining ; 15 h 22 min 6 s 547.32 ms total) Sun May 31 16:55:48 2026: Iterated ≈10% of D-proof candidates. [ 350758245 of 3507582456] (ETC: Mon Jun 1 06:14:24 2026 ; 13 h 18 min 36 s 774.27 ms remaining ; 14 h 47 min 20 s 860.29 ms total) Sun May 31 17:07:08 2026: Iterated ≈12% of D-proof candidates. [ 420909894 of 3507582456] (ETC: Mon Jun 1 05:20:59 2026 ; 12 h 13 min 51 s 75.35 ms remaining ; 13 h 53 min 55 s 312.88 ms total) Sun May 31 17:18:09 2026: Iterated ≈14% of D-proof candidates. [ 491061543 of 3507582456] (ETC: Mon Jun 1 04:40:37 2026 ; 11 h 22 min 27 s 321.21 ms remaining ; 13 h 13 min 33 s 164.19 ms total) Sun May 31 17:29:09 2026: Iterated ≈16% of D-proof candidates. [ 561213192 of 3507582456] (ETC: Mon Jun 1 04:10:05 2026 ; 10 h 40 min 56 s 353.82 ms remaining ; 12 h 43 min 1 s 373.58 ms total) Sun May 31 17:42:40 2026: Iterated ≈18% of D-proof candidates. [ 631364842 of 3507582456] (ETC: Mon Jun 1 04:00:24 2026 ; 10 h 17 min 44 s 575.95 ms remaining ; 12 h 33 min 20 s 702.37 ms total) Sun May 31 17:55:59 2026: Iterated ≈20% of D-proof candidates. [ 701516491 of 3507582456] (ETC: Mon Jun 1 03:51:42 2026 ; 9 h 55 min 43 s 70.94 ms remaining ; 12 h 24 min 38 s 838.68 ms total) Sun May 31 18:08:22 2026: Iterated ≈22% of D-proof candidates. [ 771668140 of 3507582456] (ETC: Mon Jun 1 03:40:17 2026 ; 9 h 31 min 55 s 78.53 ms remaining ; 12 h 13 min 13 s 690.41 ms total) Sun May 31 18:22:37 2026: Iterated ≈24% of D-proof candidates. [ 841819789 of 3507582456] (ETC: Mon Jun 1 03:38:31 2026 ; 9 h 15 min 54 s 585.06 ms remaining ; 12 h 11 min 27 s 611.92 ms total) Sun May 31 18:36:51 2026: Iterated ≈26% of D-proof candidates. [ 911971438 of 3507582456] (ETC: Mon Jun 1 03:37:00 2026 ; 9 h 9 s 320.47 ms remaining ; 12 h 9 min 56 s 379.01 ms total) Sun May 31 18:50:50 2026: Iterated ≈28% of D-proof candidates. [ 982123087 of 3507582456] (ETC: Mon Jun 1 03:34:49 2026 ; 8 h 43 min 59 s 271.71 ms remaining ; 12 h 7 min 45 s 655.14 ms total) Sun May 31 19:05:36 2026: Iterated ≈30% of D-proof candidates. [1052274736 of 3507582456] (ETC: Mon Jun 1 03:35:32 2026 ; 8 h 29 min 55 s 838.04 ms remaining ; 12 h 8 min 28 s 340.05 ms total) Sun May 31 19:20:59 2026: Iterated ≈32% of D-proof candidates. [1122426385 of 3507582456] (ETC: Mon Jun 1 03:38:04 2026 ; 8 h 17 min 5 s 21.33 ms remaining ; 12 h 11 min 325.46 ms total) Sun May 31 19:37:12 2026: Iterated ≈34% of D-proof candidates. [1192578035 of 3507582456] (ETC: Mon Jun 1 03:42:47 2026 ; 8 h 5 min 34 s 570.74 ms remaining ; 12 h 15 min 43 s 289.00 ms total) Sun May 31 19:51:36 2026: Iterated ≈36% of D-proof candidates. [1262729684 of 3507582456] (ETC: Mon Jun 1 03:41:54 2026 ; 7 h 50 min 17 s 618.16 ms remaining ; 12 h 14 min 50 s 28.38 ms total) Sun May 31 20:04:01 2026: Iterated ≈38% of D-proof candidates. [1332881333 of 3507582456] (ETC: Mon Jun 1 03:35:53 2026 ; 7 h 31 min 52 s 25.46 ms remaining ; 12 h 8 min 49 s 73.31 ms total) Sun May 31 20:16:53 2026: Iterated ≈40% of D-proof candidates. [1403032982 of 3507582456] (ETC: Mon Jun 1 03:31:38 2026 ; 7 h 14 min 44 s 637.40 ms remaining ; 12 h 4 min 34 s 395.66 ms total) Sun May 31 20:31:42 2026: Iterated ≈42% of D-proof candidates. [1473184631 of 3507582456] (ETC: Mon Jun 1 03:32:23 2026 ; 7 h 41 s 258.26 ms remaining ; 12 h 5 min 19 s 410.78 ms total) Sun May 31 20:52:08 2026: Iterated ≈44% of D-proof candidates. [1543336280 of 3507582456] (ETC: Mon Jun 1 03:45:52 2026 ; 6 h 53 min 43 s 755.87 ms remaining ; 12 h 18 min 48 s 135.47 ms total) Sun May 31 21:05:38 2026: Iterated ≈46% of D-proof candidates. [1613487929 of 3507582456] (ETC: Mon Jun 1 03:43:05 2026 ; 6 h 37 min 27 s 409.17 ms remaining ; 12 h 16 min 1 s 868.82 ms total) Sun May 31 21:21:05 2026: Iterated ≈48% of D-proof candidates. [1683639578 of 3507582456] (ETC: Mon Jun 1 03:44:37 2026 ; 6 h 23 min 31 s 696.47 ms remaining ; 12 h 17 min 33 s 262.42 ms total) Sun May 31 21:38:11 2026: Iterated ≈50% of D-proof candidates. [1753791228 of 3507582456] (ETC: Mon Jun 1 03:49:19 2026 ; 6 h 11 min 7 s 724.93 ms remaining ; 12 h 22 min 15 s 449.86 ms total) Sun May 31 21:55:32 2026: Iterated ≈52% of D-proof candidates. [1823942877 of 3507582456] (ETC: Mon Jun 1 03:54:07 2026 ; 5 h 58 min 35 s 302.70 ms remaining ; 12 h 27 min 3 s 547.28 ms total) Sun May 31 22:08:41 2026: Iterated ≈54% of D-proof candidates. [1894094526 of 3507582456] (ETC: Mon Jun 1 03:50:48 2026 ; 5 h 42 min 7 s 119.27 ms remaining ; 12 h 23 min 44 s 172.32 ms total) Sun May 31 22:22:58 2026: Iterated ≈56% of D-proof candidates. [1964246175 of 3507582456] (ETC: Mon Jun 1 03:49:46 2026 ; 5 h 26 min 47 s 270.53 ms remaining ; 12 h 22 min 41 s 978.47 ms total) Sun May 31 22:37:32 2026: Iterated ≈58% of D-proof candidates. [2034397824 of 3507582456] (ETC: Mon Jun 1 03:49:16 2026 ; 5 h 11 min 43 s 665.47 ms remaining ; 12 h 22 min 12 s 536.81 ms total) Sun May 31 22:51:12 2026: Iterated ≈60% of D-proof candidates. [2104549473 of 3507582456] (ETC: Mon Jun 1 03:47:18 2026 ; 4 h 56 min 5 s 553.10 ms remaining ; 12 h 20 min 13 s 882.73 ms total) Sun May 31 23:04:55 2026: Iterated ≈62% of D-proof candidates. [2174701122 of 3507582456] (ETC: Mon Jun 1 03:45:32 2026 ; 4 h 40 min 37 s 338.44 ms remaining ; 12 h 18 min 28 s 785.35 ms total) Sun May 31 23:19:55 2026: Iterated ≈64% of D-proof candidates. [2244852771 of 3507582456] (ETC: Mon Jun 1 03:45:53 2026 ; 4 h 25 min 58 s 683.59 ms remaining ; 12 h 18 min 49 s 676.60 ms total) Sun May 31 23:32:48 2026: Iterated ≈66% of D-proof candidates. [2315004420 of 3507582456] (ETC: Mon Jun 1 03:43:01 2026 ; 4 h 10 min 13 s 599.98 ms remaining ; 12 h 15 min 57 s 646.95 ms total) Sun May 31 23:45:15 2026: Iterated ≈68% of D-proof candidates. [2385156070 of 3507582456] (ETC: Mon Jun 1 03:39:42 2026 ; 3 h 54 min 26 s 708.40 ms remaining ; 12 h 12 min 38 s 463.74 ms total) Sun May 31 23:57:54 2026: Iterated ≈70% of D-proof candidates. [2455307719 of 3507582456] (ETC: Mon Jun 1 03:36:50 2026 ; 3 h 38 min 55 s 767.08 ms remaining ; 12 h 9 min 45 s 890.26 ms total) Mon Jun 1 00:11:20 2026: Iterated ≈72% of D-proof candidates. [2525459368 of 3507582456] (ETC: Mon Jun 1 03:35:13 2026 ; 3 h 23 min 52 s 962.57 ms remaining ; 12 h 8 min 9 s 152.02 ms total) Mon Jun 1 00:24:37 2026: Iterated ≈74% of D-proof candidates. [2595611017 of 3507582456] (ETC: Mon Jun 1 03:33:30 2026 ; 3 h 8 min 52 s 412.55 ms remaining ; 12 h 6 min 26 s 202.11 ms total) Mon Jun 1 00:38:09 2026: Iterated ≈76% of D-proof candidates. [2665762666 of 3507582456] (ETC: Mon Jun 1 03:32:10 2026 ; 2 h 54 min 1 s 596.59 ms remaining ; 12 h 5 min 6 s 652.42 ms total) Mon Jun 1 00:51:15 2026: Iterated ≈78% of D-proof candidates. [2735914315 of 3507582456] (ETC: Mon Jun 1 03:30:23 2026 ; 2 h 39 min 7 s 823.30 ms remaining ; 12 h 3 min 19 s 196.77 ms total) Mon Jun 1 01:04:47 2026: Iterated ≈80% of D-proof candidates. [2806065964 of 3507582456] (ETC: Mon Jun 1 03:29:13 2026 ; 2 h 24 min 25 s 885.66 ms remaining ; 12 h 2 min 9 s 428.27 ms total) Mon Jun 1 01:18:40 2026: Iterated ≈82% of D-proof candidates. [2876217613 of 3507582456] (ETC: Mon Jun 1 03:28:32 2026 ; 2 h 9 min 51 s 965.75 ms remaining ; 12 h 1 min 28 s 698.56 ms total) Mon Jun 1 01:32:58 2026: Iterated ≈84% of D-proof candidates. [2946369263 of 3507582456] (ETC: Mon Jun 1 03:28:22 2026 ; 1 h 55 min 24 s 565.77 ms remaining ; 12 h 1 min 18 s 536.04 ms total) Mon Jun 1 01:47:29 2026: Iterated ≈86% of D-proof candidates. [3016520912 of 3507582456] (ETC: Mon Jun 1 03:28:29 2026 ; 1 h 40 min 59 s 906.23 ms remaining ; 12 h 1 min 25 s 44.49 ms total) Mon Jun 1 02:02:29 2026: Iterated ≈88% of D-proof candidates. [3086672561 of 3507582456] (ETC: Mon Jun 1 03:29:08 2026 ; 1 h 26 min 38 s 889.05 ms remaining ; 12 h 2 min 4 s 75.38 ms total) Mon Jun 1 02:16:38 2026: Iterated ≈90% of D-proof candidates. [3156824210 of 3507582456] (ETC: Mon Jun 1 03:28:49 2026 ; 1 h 12 min 10 s 541.09 ms remaining ; 12 h 1 min 45 s 410.89 ms total) Mon Jun 1 02:31:11 2026: Iterated ≈92% of D-proof candidates. [3226975859 of 3507582456] (ETC: Mon Jun 1 03:28:56 2026 ; 57 min 45 s 12.85 ms remaining ; 12 h 1 min 52 s 660.61 ms total) Mon Jun 1 02:45:08 2026: Iterated ≈94% of D-proof candidates. [3297127508 of 3507582456] (ETC: Mon Jun 1 03:28:25 2026 ; 43 min 16 s 896.80 ms remaining ; 12 h 1 min 21 s 613.13 ms total) Mon Jun 1 02:59:53 2026: Iterated ≈96% of D-proof candidates. [3367279157 of 3507582456] (ETC: Mon Jun 1 03:28:45 2026 ; 28 min 52 s 63.18 ms remaining ; 12 h 1 min 41 s 579.23 ms total) Mon Jun 1 03:14:38 2026: Iterated ≈98% of D-proof candidates. [3437430806 of 3507582456] (ETC: Mon Jun 1 03:29:04 2026 ; 14 min 26 s 415.18 ms remaining ; 12 h 2 min 758.56 ms total) Mon Jun 1 03:29:53 2026: Iterated 100% of D-proof candidates. [3507582456 of 3507582456] (ETC: Mon Jun 1 03:29:53 2026 ; 0.00 ms remaining ; 12 h 2 min 49 s 443.06 ms total) 43381686.65 ms (12 h 3 min 1 s 686.65 ms) taken to collect 633578953 D-proofs of length 91. [iterated 3507582456 condensed detachment proof strings] 5303857.78 ms (1 h 28 min 23 s 857.78 ms) taken to filter and order new representative proofs. Found 633578953 representative, 2075378879 redundant, and 798624624 invalid condensed detachment proof strings. lengths up to 91 ; 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,5226411), (85,74024284), (87,185049299), (89,364350012), (91,633578953)} ; 633578953 new representative proofs (2075378879 redundant, 798624624 invalid) Mon Jun 1 04:58:29 2026: Starting to write 633578953 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs91-unfiltered85+.txt. 926571.99 ms (15 min 26 s 571.99 ms) taken to print and save 178306670202 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs91-unfiltered85+.txt. Determined the number of proof string candidates for iteration as 6271062320. [most relevant: {1,91} with 2*1267157906 = 2534315812, i.e. ≈40.41%] Mon Jun 1 05:38:16 2026: Starting to generate D-proof representatives of length 93. Mon Jun 1 06:15:20 2026: Iterated ≈ 2% of D-proof candidates. [ 125421246 of 6271062320] (ETC: Tue Jun 2 12:31:38 2026 ; 1 d 6 h 16 min 18 s 145.72 ms remaining ; 1 d 6 h 53 min 22 s 189.50 ms total) Mon Jun 1 06:55:45 2026: Iterated ≈ 4% of D-proof candidates. [ 250842492 of 6271062320] (ETC: Tue Jun 2 13:55:05 2026 ; 1 d 6 h 59 min 20 s 212.47 ms remaining ; 1 d 8 h 16 min 48 s 554.64 ms total) Mon Jun 1 07:29:19 2026: Iterated ≈ 6% of D-proof candidates. [ 376263739 of 6271062320] (ETC: Tue Jun 2 12:28:58 2026 ; 1 d 4 h 59 min 39 s 137.98 ms remaining ; 1 d 6 h 50 min 41 s 636.14 ms total) Mon Jun 1 07:57:30 2026: Iterated ≈ 8% of D-proof candidates. [ 501684985 of 6271062320] (ETC: Tue Jun 2 10:38:41 2026 ; 1 d 2 h 41 min 10 s 773.48 ms remaining ; 1 d 5 h 24 s 753.77 ms total) Mon Jun 1 08:26:42 2026: Iterated ≈10% of D-proof candidates. [ 627106232 of 6271062320] (ETC: Tue Jun 2 09:42:36 2026 ; 1 d 1 h 15 min 53 s 921.21 ms remaining ; 1 d 4 h 4 min 19 s 912.46 ms total) Mon Jun 1 08:59:02 2026: Iterated ≈12% of D-proof candidates. [ 752527478 of 6271062320] (ETC: Tue Jun 2 09:31:21 2026 ; 1 d 32 min 18 s 987.10 ms remaining ; 1 d 3 h 53 min 5 s 212.60 ms total) Mon Jun 1 09:23:53 2026: Iterated ≈14% of D-proof candidates. [ 877948724 of 6271062320] (ETC: Tue Jun 2 08:29:50 2026 ; 23 h 5 min 56 s 685.07 ms remaining ; 1 d 2 h 51 min 33 s 819.84 ms total) Mon Jun 1 09:45:04 2026: Iterated ≈16% of D-proof candidates. [1003369971 of 6271062320] (ETC: Tue Jun 2 07:20:43 2026 ; 21 h 35 min 39 s 141.16 ms remaining ; 1 d 1 h 42 min 26 s 596.61 ms total) Mon Jun 1 10:08:13 2026: Iterated ≈18% of D-proof candidates. [1128791217 of 6271062320] (ETC: Tue Jun 2 06:37:57 2026 ; 20 h 29 min 44 s 553.30 ms remaining ; 1 d 59 min 41 s 162.55 ms total) Mon Jun 1 10:34:35 2026: Iterated ≈20% of D-proof candidates. [1254212464 of 6271062320] (ETC: Tue Jun 2 06:19:49 2026 ; 19 h 45 min 14 s 194.36 ms remaining ; 1 d 41 min 32 s 742.96 ms total) Mon Jun 1 11:01:46 2026: Iterated ≈22% of D-proof candidates. [1379633710 of 6271062320] (ETC: Tue Jun 2 06:08:44 2026 ; 19 h 6 min 57 s 865.60 ms remaining ; 1 d 30 min 28 s 32.81 ms total) Mon Jun 1 11:29:09 2026: Iterated ≈24% of D-proof candidates. [1505054956 of 6271062320] (ETC: Tue Jun 2 06:00:18 2026 ; 18 h 31 min 8 s 552.63 ms remaining ; 1 d 22 min 1 s 779.76 ms total) Mon Jun 1 11:59:29 2026: Iterated ≈26% of D-proof candidates. [1630476203 of 6271062320] (ETC: Tue Jun 2 06:04:29 2026 ; 18 h 4 min 59 s 591.41 ms remaining ; 1 d 26 min 12 s 420.82 ms total) Mon Jun 1 12:34:31 2026: Iterated ≈28% of D-proof candidates. [1755897449 of 6271062320] (ETC: Tue Jun 2 06:24:52 2026 ; 17 h 50 min 21 s 235.55 ms remaining ; 1 d 46 min 36 s 160.47 ms total) Mon Jun 1 12:59:35 2026: Iterated ≈30% of D-proof candidates. [1881318696 of 6271062320] (ETC: Tue Jun 2 06:09:20 2026 ; 17 h 9 min 44 s 606.78 ms remaining ; 1 d 31 min 3 s 723.97 ms total) Mon Jun 1 13:24:34 2026: Iterated ≈32% of D-proof candidates. [2006739942 of 6271062320] (ETC: Tue Jun 2 05:55:26 2026 ; 16 h 30 min 52 s 266.63 ms remaining ; 1 d 17 min 9 s 803.86 ms total) Mon Jun 1 13:51:17 2026: Iterated ≈34% of D-proof candidates. [2132161188 of 6271062320] (ETC: Tue Jun 2 05:48:20 2026 ; 15 h 57 min 2 s 486.04 ms remaining ; 1 d 10 min 3 s 766.72 ms total) Mon Jun 1 14:18:08 2026: Iterated ≈36% of D-proof candidates. [2257582435 of 6271062320] (ETC: Tue Jun 2 05:42:19 2026 ; 15 h 24 min 11 s 473.62 ms remaining ; 1 d 4 min 2 s 927.53 ms total) Mon Jun 1 14:46:31 2026: Iterated ≈38% of D-proof candidates. [2383003681 of 6271062320] (ETC: Tue Jun 2 05:41:00 2026 ; 14 h 54 min 29 s 754.28 ms remaining ; 1 d 2 min 44 s 119.80 ms total) Mon Jun 1 15:17:10 2026: Iterated ≈40% of D-proof candidates. [2508424928 of 6271062320] (ETC: Tue Jun 2 05:45:32 2026 ; 14 h 28 min 21 s 203.91 ms remaining ; 1 d 7 min 15 s 339.86 ms total) Mon Jun 1 16:02:25 2026: Iterated ≈42% of D-proof candidates. [2633846174 of 6271062320] (ETC: Tue Jun 2 06:24:21 2026 ; 14 h 21 min 55 s 380.52 ms remaining ; 1 d 46 min 4 s 449.16 ms total) Mon Jun 1 16:38:33 2026: Iterated ≈44% of D-proof candidates. [2759267420 of 6271062320] (ETC: Tue Jun 2 06:38:55 2026 ; 14 h 21 s 893.28 ms remaining ; 1 d 1 h 39 s 95.12 ms total) Mon Jun 1 17:06:24 2026: Iterated ≈46% of D-proof candidates. [2884688667 of 6271062320] (ETC: Tue Jun 2 06:34:13 2026 ; 13 h 27 min 48 s 479.77 ms remaining ; 1 d 55 min 56 s 444.02 ms total) Mon Jun 1 17:42:36 2026: Iterated ≈48% of D-proof candidates. [3010109913 of 6271062320] (ETC: Tue Jun 2 06:47:17 2026 ; 13 h 4 min 41 s 137.26 ms remaining ; 1 d 1 h 9 min 648.56 ms total) Mon Jun 1 18:15:38 2026: Iterated ≈50% of D-proof candidates. [3135531160 of 6271062320] (ETC: Tue Jun 2 06:52:59 2026 ; 12 h 37 min 21 s 422.22 ms remaining ; 1 d 1 h 14 min 42 s 844.43 ms total) Mon Jun 1 18:51:51 2026: Iterated ≈52% of D-proof candidates. [3260952406 of 6271062320] (ETC: Tue Jun 2 07:04:23 2026 ; 12 h 12 min 32 s 130.53 ms remaining ; 1 d 1 h 26 min 6 s 938.60 ms total) Mon Jun 1 19:26:55 2026: Iterated ≈54% of D-proof candidates. [3386373652 of 6271062320] (ETC: Tue Jun 2 07:12:49 2026 ; 11 h 45 min 53 s 293.79 ms remaining ; 1 d 1 h 34 min 32 s 377.78 ms total) Mon Jun 1 19:58:30 2026: Iterated ≈56% of D-proof candidates. [3511794899 of 6271062320] (ETC: Tue Jun 2 07:14:24 2026 ; 11 h 15 min 53 s 726.83 ms remaining ; 1 d 1 h 36 min 7 s 560.96 ms total) Mon Jun 1 20:31:47 2026: Iterated ≈58% of D-proof candidates. [3637216145 of 6271062320] (ETC: Tue Jun 2 07:18:49 2026 ; 10 h 47 min 1 s 834.24 ms remaining ; 1 d 1 h 40 min 32 s 938.63 ms total) Mon Jun 1 20:57:57 2026: Iterated ≈60% of D-proof candidates. [3762637392 of 6271062320] (ETC: Tue Jun 2 07:11:05 2026 ; 10 h 13 min 7 s 453.68 ms remaining ; 1 d 1 h 32 min 48 s 634.20 ms total) Mon Jun 1 21:25:51 2026: Iterated ≈62% of D-proof candidates. [3888058638 of 6271062320] (ETC: Tue Jun 2 07:06:38 2026 ; 9 h 40 min 46 s 722.27 ms remaining ; 1 d 1 h 28 min 21 s 900.69 ms total) Mon Jun 1 21:50:13 2026: Iterated ≈64% of D-proof candidates. [4013479884 of 6271062320] (ETC: Tue Jun 2 06:56:57 2026 ; 9 h 6 min 43 s 424.74 ms remaining ; 1 d 1 h 18 min 40 s 624.24 ms total) Mon Jun 1 22:17:23 2026: Iterated ≈66% of D-proof candidates. [4138901131 of 6271062320] (ETC: Tue Jun 2 06:52:05 2026 ; 8 h 34 min 41 s 865.12 ms remaining ; 1 d 1 h 13 min 49 s 15.06 ms total) Mon Jun 1 22:48:02 2026: Iterated ≈68% of D-proof candidates. [4264322377 of 6271062320] (ETC: Tue Jun 2 06:52:38 2026 ; 8 h 4 min 35 s 780.87 ms remaining ; 1 d 1 h 14 min 21 s 815.19 ms total) Mon Jun 1 23:19:33 2026: Iterated ≈70% of D-proof candidates. [4389743624 of 6271062320] (ETC: Tue Jun 2 06:54:23 2026 ; 7 h 34 min 50 s 1.13 ms remaining ; 1 d 1 h 16 min 6 s 670.44 ms total) Mon Jun 1 23:51:04 2026: Iterated ≈72% of D-proof candidates. [4515164870 of 6271062320] (ETC: Tue Jun 2 06:56:03 2026 ; 7 h 4 min 58 s 672.64 ms remaining ; 1 d 1 h 17 min 46 s 687.98 ms total) Tue Jun 2 00:21:38 2026: Iterated ≈74% of D-proof candidates. [4640586116 of 6271062320] (ETC: Tue Jun 2 06:56:20 2026 ; 6 h 34 min 41 s 704.21 ms remaining ; 1 d 1 h 18 min 3 s 477.69 ms total) Tue Jun 2 00:51:39 2026: Iterated ≈76% of D-proof candidates. [4766007363 of 6271062320] (ETC: Tue Jun 2 06:55:52 2026 ; 6 h 4 min 13 s 398.69 ms remaining ; 1 d 1 h 17 min 35 s 827.86 ms total) Tue Jun 2 01:24:22 2026: Iterated ≈78% of D-proof candidates. [4891428609 of 6271062320] (ETC: Tue Jun 2 06:58:55 2026 ; 5 h 34 min 32 s 491.33 ms remaining ; 1 d 1 h 20 min 38 s 596.90 ms total) Tue Jun 2 01:50:51 2026: Iterated ≈80% of D-proof candidates. [5016849856 of 6271062320] (ETC: Tue Jun 2 06:53:59 2026 ; 5 h 3 min 8 s 651.17 ms remaining ; 1 d 1 h 15 min 43 s 255.84 ms total) Tue Jun 2 02:19:37 2026: Iterated ≈82% of D-proof candidates. [5142271102 of 6271062320] (ETC: Tue Jun 2 06:52:06 2026 ; 4 h 32 min 29 s 444.87 ms remaining ; 1 d 1 h 13 min 50 s 249.22 ms total) Tue Jun 2 02:45:51 2026: Iterated ≈84% of D-proof candidates. [5267692348 of 6271062320] (ETC: Tue Jun 2 06:47:18 2026 ; 4 h 1 min 26 s 634.48 ms remaining ; 1 d 1 h 9 min 1 s 465.44 ms total) Tue Jun 2 03:14:06 2026: Iterated ≈86% of D-proof candidates. [5393113595 of 6271062320] (ETC: Tue Jun 2 06:45:03 2026 ; 3 h 30 min 56 s 902.26 ms remaining ; 1 d 1 h 6 min 46 s 444.67 ms total) Tue Jun 2 03:46:46 2026: Iterated ≈88% of D-proof candidates. [5518534841 of 6271062320] (ETC: Tue Jun 2 06:47:55 2026 ; 3 h 1 min 9 s 467.75 ms remaining ; 1 d 1 h 9 min 38 s 897.83 ms total) Tue Jun 2 04:15:45 2026: Iterated ≈90% of D-proof candidates. [5643956088 of 6271062320] (ETC: Tue Jun 2 06:46:34 2026 ; 2 h 30 min 49 s 828.96 ms remaining ; 1 d 1 h 8 min 18 s 289.61 ms total) Tue Jun 2 04:45:33 2026: Iterated ≈92% of D-proof candidates. [5769377334 of 6271062320] (ETC: Tue Jun 2 06:46:11 2026 ; 2 h 37 s 950.39 ms remaining ; 1 d 1 h 7 min 54 s 379.80 ms total) Tue Jun 2 05:15:25 2026: Iterated ≈94% of D-proof candidates. [5894798580 of 6271062320] (ETC: Tue Jun 2 06:45:52 2026 ; 1 h 30 min 27 s 375.63 ms remaining ; 1 d 1 h 7 min 36 s 260.24 ms total) Tue Jun 2 05:47:48 2026: Iterated ≈96% of D-proof candidates. [6020219827 of 6271062320] (ETC: Tue Jun 2 06:48:12 2026 ; 1 h 23 s 821.23 ms remaining ; 1 d 1 h 9 min 55 s 530.66 ms total) Tue Jun 2 06:18:15 2026: Iterated ≈98% of D-proof candidates. [6145641073 of 6271062320] (ETC: Tue Jun 2 06:48:28 2026 ; 30 min 12 s 226.98 ms remaining ; 1 d 1 h 10 min 11 s 348.80 ms total) Tue Jun 2 06:50:59 2026: Iterated 100% of D-proof candidates. [6271062320 of 6271062320] (ETC: Tue Jun 2 06:50:59 2026 ; 0.00 ms remaining ; 1 d 1 h 12 min 43 s 17.16 ms total) 90785761.00 ms (1 d 1 h 13 min 5 s 761.00 ms) taken to collect 1146953429 D-proofs of length 93. [iterated 6271062320 condensed detachment proof strings] 9642233.92 ms (2 h 40 min 42 s 233.92 ms) taken to filter and order new representative proofs. Found 1146953429 representative, 3716261502 redundant, and 1407847389 invalid condensed detachment proof strings. lengths up to 93 ; 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,5226411), (85,74024284), (87,185049299), (89,364350012), (91,633578953), (93,1146953429)} ; 1146953429 new representative proofs (3716261502 redundant, 1407847389 invalid) Tue Jun 2 09:32:04 2026: Starting to write 1146953429 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs93-unfiltered85+.txt. 1700079.60 ms (28 min 20 s 79.60 ms) taken to print and save 349868787801 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs93-unfiltered85+.txt. [2026-06-02T10:04:20.637] error: Detected 1 oom_kill event in StepId=700897.batch. Some of the step tasks have been OOM Killed.