( This log file was generated by 'pmGenerator 1.2.3' (master branch), compiled by 'GCC 11.3.0'. The run was executed on a PC — Intel Core i7-3770, 4 cores (8 hardware threads), 3.4 GHz, 3.8 GHz turbo mode, 32 GiB main memory — running Windows 7 Ultimate. Wall-clock time: 2.9958333… h CPU utilization: 11.98333… core-h ) $ ./pmGenerator -c -n -s CCCpqrCCrpCsp,COp -e l21 -g -1 -l 21 -b Tue Jun 16 17:25:42 2026: Process started. [pid: 6876, tid:1] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true, "l21") 2. generateDProofRepresentativeFiles(4294967295, true, true, null, 21, -1, true, true) [Main] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true, "l21"). 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 Selected extracted proof system at "data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/". (1) 1 - CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) (2) 2 - CO0 - COp - \bot\imply0 [Main] Calling generateDProofRepresentativeFiles(4294967295, true, true, null, 21, -1, true, true). Tue Jun 16 17:25:42 2026: Unlimited D-proof representative generator started. [parallel ; 8 hardware thread contexts, candidate queue capacities: 50, conclusion length limit: 21, use conclusion trees] 0.00 ms taken to load initial representatives. 0.06 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs3.txt. [tid:2] 0.05 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs5.txt. [tid:3] 0.09 ms taken to read 63 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs19.txt. [tid:10] 0.13 ms taken to read 90 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs21.txt. [tid:11] 0.13 ms taken to read 113 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs23.txt. [tid:12] 0.12 ms taken to read 165 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs25.txt. [tid:13] 0.06 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs7.txt. [tid:4] 0.06 ms taken to read 195 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs27.txt. [tid:14] 0.05 ms taken to read 264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs29.txt. [tid:15] 0.06 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs9.txt. [tid:5] 0.10 ms taken to read 439 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs33.txt. [tid:17] 0.02 ms taken to read 344 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs31.txt. [tid:16] 0.06 ms taken to read 592 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs35.txt. [tid:18] 0.18 ms taken to read 704 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs37.txt. [tid:19] 0.10 ms taken to read 168 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs43.txt. [tid:22] 0.16 ms taken to read 168 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs45.txt. [tid:23] 0.03 ms taken to read 980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs39.txt. [tid:20] 0.03 ms taken to read 198 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs47.txt. [tid:24] 0.17 ms taken to read 1212 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs41.txt. [tid:21] 0.05 ms taken to read 249 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs51.txt. [tid:26] 0.07 ms taken to read 298 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs53.txt. [tid:27] 0.07 ms taken to read 345 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs55.txt. [tid:28] 0.14 ms taken to read 376 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs57.txt. [tid:29] 0.03 ms taken to read 236 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs49.txt. [tid:25] 0.44 ms taken to read 450 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs59.txt. [tid:30] 0.25 ms taken to read 522 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs61.txt. [tid:31] 0.50 ms taken to read 630 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs63.txt. [tid:32] 0.44 ms taken to read 754 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs65.txt. [tid:33] 0.05 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs11.txt. [tid:6] 0.42 ms taken to read 792 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs67.txt. [tid:34] 0.04 ms taken to read 987 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs69.txt. [tid:35] 0.88 ms taken to read 1126 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs71.txt. [tid:36] 0.64 ms taken to read 1214 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs73.txt. [tid:37] 0.73 ms taken to read 1273 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs75.txt. [tid:38] 0.06 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs13.txt. [tid:7] 0.25 ms taken to read 1355 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs77.txt. [tid:39] 0.24 ms taken to read 1462 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs79.txt. [tid:40] 0.28 ms taken to read 1572 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs81.txt. [tid:41] 0.55 ms taken to read 1602 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs83.txt. [tid:42] 1.02 ms taken to read 2002 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs89.txt. [tid:45] 0.47 ms taken to read 1807 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs85.txt. [tid:43] 1.39 ms taken to read 2382 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs91.txt. [tid:46] 1.43 ms taken to read 2568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs93.txt. [tid:47] 1.65 ms taken to read 2470 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs97.txt. [tid:49] 1.61 ms taken to read 2405 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs99.txt. [tid:50] 1.43 ms taken to read 1854 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs87.txt. [tid:44] 0.06 ms taken to read 32 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs15.txt. [tid:8] 1.02 ms taken to read 2583 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs101.txt. [tid:51] 1.19 ms taken to read 2727 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs103.txt. [tid:52] 0.43 ms taken to read 2726 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs95.txt. [tid:48] 1.27 ms taken to read 3154 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs107.txt. [tid:54] 0.08 ms taken to read 41 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs17.txt. [tid:9] 1.02 ms taken to read 2949 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs105.txt. [tid:53] 0.56 ms taken to read 3800 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs115.txt. [tid:58] 0.33 ms taken to read 3723 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs113.txt. [tid:57] 0.18 ms taken to read 3594 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs117.txt. [tid:59] 1.12 ms taken to read 3809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs119.txt. [tid:60] 0.77 ms taken to read 3362 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs109.txt. [tid:55] 1.78 ms taken to read 3530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs111.txt. [tid:56] 0.46 ms taken to read 4112 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs121.txt. [tid:61] 1.66 ms taken to read 4394 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs123.txt. [tid:62] 2.68 ms taken to read 4453 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs125.txt. [tid:63] 4.96 ms taken to read 6242 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs141.txt. [tid:71] 3.72 ms taken to read 5906 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs139.txt. [tid:70] 0.70 ms taken to read 4805 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs127.txt. [tid:64] 3.06 ms taken to read 4819 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs129.txt. [tid:65] 3.22 ms taken to read 4998 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs131.txt. [tid:66] 3.10 ms taken to read 5230 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs133.txt. [tid:67] 0.42 ms taken to read 5409 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs135.txt. [tid:68] 3.00 ms taken to read 5737 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs137.txt. [tid:69] 42.64 ms total read duration. Loaded 71 representative collections of sizes: 1 : 2 3 : 1 5 : 1 7 : 3 9 : 8 11 : 15 13 : 22 15 : 32 17 : 41 19 : 63 21 : 90 23 : 113 25 : 165 27 : 195 29 : 264 31 : 344 33 : 439 35 : 592 37 : 704 39 : 980 41 : 1212 43 : 168 45 : 168 47 : 198 49 : 236 51 : 249 53 : 298 55 : 345 57 : 376 59 : 450 61 : 522 63 : 630 65 : 754 67 : 792 69 : 987 71 : 1126 73 : 1214 75 : 1273 77 : 1355 79 : 1462 81 : 1572 83 : 1602 85 : 1807 87 : 1854 89 : 2002 91 : 2382 93 : 2568 95 : 2726 97 : 2470 99 : 2405 101 : 2583 103 : 2727 105 : 2949 107 : 3154 109 : 3362 111 : 3530 113 : 3723 115 : 3800 117 : 3594 119 : 3809 121 : 4112 123 : 4394 125 : 4453 127 : 4805 129 : 4819 131 : 4998 133 : 5230 135 : 5409 137 : 5737 139 : 5906 141 : 6242 128613 representatives in total. Tue Jun 16 17:25:42 2026: Inserted ≈ 5% of D-proof conclusions. [ 6430 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 19.00 ms remaining ; 20.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈10% of D-proof conclusions. [ 12861 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 27.00 ms remaining ; 30.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈15% of D-proof conclusions. [ 19291 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 22.67 ms remaining ; 26.67 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈20% of D-proof conclusions. [ 25722 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 20.00 ms remaining ; 25.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈25% of D-proof conclusions. [ 32153 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 21.00 ms remaining ; 28.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈30% of D-proof conclusions. [ 38583 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 18.67 ms remaining ; 26.67 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈35% of D-proof conclusions. [ 45014 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 16.71 ms remaining ; 25.71 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈40% of D-proof conclusions. [ 51445 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 16.50 ms remaining ; 27.50 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈45% of D-proof conclusions. [ 57875 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 14.67 ms remaining ; 26.67 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈50% of D-proof conclusions. [ 64306 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 13.00 ms remaining ; 26.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈55% of D-proof conclusions. [ 70737 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 12.27 ms remaining ; 27.27 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈60% of D-proof conclusions. [ 77167 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 11.33 ms remaining ; 28.33 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈65% of D-proof conclusions. [ 83598 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 9.69 ms remaining ; 27.69 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈70% of D-proof conclusions. [ 90029 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 8.57 ms remaining ; 28.57 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈75% of D-proof conclusions. [ 96459 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 7.00 ms remaining ; 28.00 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈80% of D-proof conclusions. [102890 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 5.50 ms remaining ; 27.50 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈85% of D-proof conclusions. [109321 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 4.24 ms remaining ; 28.24 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈90% of D-proof conclusions. [115751 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 2.78 ms remaining ; 27.78 ms total) Tue Jun 16 17:25:42 2026: Inserted ≈95% of D-proof conclusions. [122182 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 1.37 ms remaining ; 27.37 ms total) Tue Jun 16 17:25:42 2026: Inserted 100% of D-proof conclusions. [128613 of 128613] (ETC: Tue Jun 16 17:25:42 2026 ; 0.00 ms remaining ; 28.00 ms total) 27.98 ms total insertion duration. Determined the number of proof string candidates for iteration as 54456864. [most relevant: {41,101} with 2*3130596 = 6261192, i.e. ≈11.50%] Could not estimate removal count since there are no known entries yet. Tue Jun 16 17:25:42 2026: Starting to generate D-proof representatives of length 143. Tue Jun 16 17:25:55 2026: Iterated ≈ 2% of D-proof candidates. [ 1089137 of 54456864] (ETC: Tue Jun 16 17:36:39 2026 ; 10 min 43 s 504.97 ms remaining ; 10 min 56 s 637.72 ms total) Tue Jun 16 17:26:11 2026: Iterated ≈ 4% of D-proof candidates. [ 2178274 of 54456864] (ETC: Tue Jun 16 17:37:47 2026 ; 11 min 36 s 184.00 ms remaining ; 12 min 5 s 191.66 ms total) Tue Jun 16 17:26:29 2026: Iterated ≈ 6% of D-proof candidates. [ 3267411 of 54456864] (ETC: Tue Jun 16 17:38:43 2026 ; 12 min 14 s 385.87 ms remaining ; 13 min 1 s 261.55 ms total) Tue Jun 16 17:26:47 2026: Iterated ≈ 8% of D-proof candidates. [ 4356549 of 54456864] (ETC: Tue Jun 16 17:39:08 2026 ; 12 min 21 s 677.43 ms remaining ; 13 min 26 s 171.12 ms total) Tue Jun 16 17:27:03 2026: Iterated ≈10% of D-proof candidates. [ 5445686 of 54456864] (ETC: Tue Jun 16 17:39:15 2026 ; 12 min 11 s 930.92 ms remaining ; 13 min 33 s 256.57 ms total) Tue Jun 16 17:27:22 2026: Iterated ≈12% of D-proof candidates. [ 6534823 of 54456864] (ETC: Tue Jun 16 17:39:39 2026 ; 12 min 16 s 389.54 ms remaining ; 13 min 56 s 806.28 ms total) Tue Jun 16 17:27:39 2026: Iterated ≈14% of D-proof candidates. [ 7623960 of 54456864] (ETC: Tue Jun 16 17:39:38 2026 ; 11 min 59 s 228.52 ms remaining ; 13 min 56 s 312.22 ms total) Tue Jun 16 17:27:59 2026: Iterated ≈16% of D-proof candidates. [ 8713098 of 54456864] (ETC: Tue Jun 16 17:40:00 2026 ; 12 min 1 s 44.76 ms remaining ; 14 min 18 s 386.62 ms total) Tue Jun 16 17:28:19 2026: Iterated ≈18% of D-proof candidates. [ 9802235 of 54456864] (ETC: Tue Jun 16 17:40:15 2026 ; 11 min 55 s 946.55 ms remaining ; 14 min 33 s 105.54 ms total) Tue Jun 16 17:28:40 2026: Iterated ≈20% of D-proof candidates. [10891372 of 54456864] (ETC: Tue Jun 16 17:40:30 2026 ; 11 min 50 s 128.68 ms remaining ; 14 min 47 s 660.84 ms total) Tue Jun 16 17:28:59 2026: Iterated ≈22% of D-proof candidates. [11980510 of 54456864] (ETC: Tue Jun 16 17:40:38 2026 ; 11 min 38 s 760.42 ms remaining ; 14 min 55 s 846.70 ms total) Tue Jun 16 17:29:19 2026: Iterated ≈24% of D-proof candidates. [13069647 of 54456864] (ETC: Tue Jun 16 17:40:47 2026 ; 11 min 27 s 582.85 ms remaining ; 15 min 4 s 714.27 ms total) Tue Jun 16 17:29:42 2026: Iterated ≈26% of D-proof candidates. [14158784 of 54456864] (ETC: Tue Jun 16 17:41:07 2026 ; 11 min 24 s 271.64 ms remaining ; 15 min 24 s 691.39 ms total) Tue Jun 16 17:30:05 2026: Iterated ≈28% of D-proof candidates. [15247921 of 54456864] (ETC: Tue Jun 16 17:41:20 2026 ; 11 min 15 s 5.24 ms remaining ; 15 min 37 s 507.25 ms total) Tue Jun 16 17:30:25 2026: Iterated ≈30% of D-proof candidates. [16337059 of 54456864] (ETC: Tue Jun 16 17:41:24 2026 ; 10 min 59 s 603.40 ms remaining ; 15 min 42 s 290.57 ms total) Tue Jun 16 17:30:47 2026: Iterated ≈32% of D-proof candidates. [17426196 of 54456864] (ETC: Tue Jun 16 17:41:35 2026 ; 10 min 48 s 289.61 ms remaining ; 15 min 53 s 367.05 ms total) Tue Jun 16 17:31:08 2026: Iterated ≈34% of D-proof candidates. [18515333 of 54456864] (ETC: Tue Jun 16 17:41:41 2026 ; 10 min 32 s 789.88 ms remaining ; 15 min 58 s 772.52 ms total) Tue Jun 16 17:31:27 2026: Iterated ≈36% of D-proof candidates. [19604471 of 54456864] (ETC: Tue Jun 16 17:41:40 2026 ; 10 min 12 s 895.50 ms remaining ; 15 min 57 s 649.22 ms total) Tue Jun 16 17:31:47 2026: Iterated ≈38% of D-proof candidates. [20693608 of 54456864] (ETC: Tue Jun 16 17:41:43 2026 ; 9 min 55 s 511.44 ms remaining ; 16 min 502.32 ms total) Tue Jun 16 17:32:14 2026: Iterated ≈40% of D-proof candidates. [21782745 of 54456864] (ETC: Tue Jun 16 17:42:01 2026 ; 9 min 47 s 477.13 ms remaining ; 16 min 19 s 128.53 ms total) Tue Jun 16 17:32:36 2026: Iterated ≈42% of D-proof candidates. [22871882 of 54456864] (ETC: Tue Jun 16 17:42:09 2026 ; 9 min 32 s 182.05 ms remaining ; 16 min 26 s 520.75 ms total) Tue Jun 16 17:32:58 2026: Iterated ≈44% of D-proof candidates. [23961020 of 54456864] (ETC: Tue Jun 16 17:42:13 2026 ; 9 min 14 s 706.64 ms remaining ; 16 min 30 s 547.57 ms total) Tue Jun 16 17:33:19 2026: Iterated ≈46% of D-proof candidates. [25050157 of 54456864] (ETC: Tue Jun 16 17:42:14 2026 ; 8 min 55 s 869.14 ms remaining ; 16 min 32 s 350.25 ms total) Tue Jun 16 17:33:39 2026: Iterated ≈48% of D-proof candidates. [26139294 of 54456864] (ETC: Tue Jun 16 17:42:16 2026 ; 8 min 37 s 27.68 ms remaining ; 16 min 34 s 283.98 ms total) Tue Jun 16 17:34:00 2026: Iterated ≈50% of D-proof candidates. [27228432 of 54456864] (ETC: Tue Jun 16 17:42:19 2026 ; 8 min 18 s 343.50 ms remaining ; 16 min 36 s 687.01 ms total) Tue Jun 16 17:34:23 2026: Iterated ≈52% of D-proof candidates. [28317569 of 54456864] (ETC: Tue Jun 16 17:42:24 2026 ; 8 min 934.90 ms remaining ; 16 min 41 s 947.70 ms total) Tue Jun 16 17:34:43 2026: Iterated ≈54% of D-proof candidates. [29406706 of 54456864] (ETC: Tue Jun 16 17:42:24 2026 ; 7 min 40 s 763.22 ms remaining ; 16 min 41 s 659.16 ms total) Tue Jun 16 17:35:02 2026: Iterated ≈56% of D-proof candidates. [30495843 of 54456864] (ETC: Tue Jun 16 17:42:22 2026 ; 7 min 19 s 827.97 ms remaining ; 16 min 39 s 608.99 ms total) Tue Jun 16 17:35:23 2026: Iterated ≈58% of D-proof candidates. [31584981 of 54456864] (ETC: Tue Jun 16 17:42:24 2026 ; 7 min 934.32 ms remaining ; 16 min 42 s 224.57 ms total) Tue Jun 16 17:35:45 2026: Iterated ≈60% of D-proof candidates. [32674118 of 54456864] (ETC: Tue Jun 16 17:42:26 2026 ; 6 min 41 s 782.99 ms remaining ; 16 min 44 s 457.46 ms total) Tue Jun 16 17:36:00 2026: Iterated ≈62% of D-proof candidates. [33763255 of 54456864] (ETC: Tue Jun 16 17:42:19 2026 ; 6 min 18 s 887.21 ms remaining ; 16 min 37 s 71.56 ms total) Tue Jun 16 17:36:14 2026: Iterated ≈64% of D-proof candidates. [34852392 of 54456864] (ETC: Tue Jun 16 17:42:09 2026 ; 5 min 55 s 473.11 ms remaining ; 16 min 27 s 425.25 ms total) Tue Jun 16 17:36:26 2026: Iterated ≈66% of D-proof candidates. [35941530 of 54456864] (ETC: Tue Jun 16 17:41:58 2026 ; 5 min 31 s 877.53 ms remaining ; 16 min 16 s 110.38 ms total) Tue Jun 16 17:36:39 2026: Iterated ≈68% of D-proof candidates. [37030667 of 54456864] (ETC: Tue Jun 16 17:41:48 2026 ; 5 min 9 s 215.35 ms remaining ; 16 min 6 s 297.93 ms total) Tue Jun 16 17:36:51 2026: Iterated ≈70% of D-proof candidates. [38119804 of 54456864] (ETC: Tue Jun 16 17:41:38 2026 ; 4 min 46 s 825.42 ms remaining ; 15 min 56 s 84.70 ms total) Tue Jun 16 17:37:04 2026: Iterated ≈72% of D-proof candidates. [39208942 of 54456864] (ETC: Tue Jun 16 17:41:29 2026 ; 4 min 25 s 44.10 ms remaining ; 15 min 46 s 586.09 ms total) Tue Jun 16 17:37:14 2026: Iterated ≈74% of D-proof candidates. [40298079 of 54456864] (ETC: Tue Jun 16 17:41:17 2026 ; 4 min 3 s 124.81 ms remaining ; 15 min 35 s 95.38 ms total) Tue Jun 16 17:37:26 2026: Iterated ≈76% of D-proof candidates. [41387216 of 54456864] (ETC: Tue Jun 16 17:41:08 2026 ; 3 min 42 s 226.83 ms remaining ; 15 min 25 s 945.08 ms total) Tue Jun 16 17:37:36 2026: Iterated ≈78% of D-proof candidates. [42476353 of 54456864] (ETC: Tue Jun 16 17:40:58 2026 ; 3 min 21 s 428.59 ms remaining ; 15 min 15 s 584.44 ms total) Tue Jun 16 17:37:48 2026: Iterated ≈80% of D-proof candidates. [43565491 of 54456864] (ETC: Tue Jun 16 17:40:50 2026 ; 3 min 1 s 509.13 ms remaining ; 15 min 7 s 545.66 ms total) Tue Jun 16 17:38:01 2026: Iterated ≈82% of D-proof candidates. [44654628 of 54456864] (ETC: Tue Jun 16 17:40:43 2026 ; 2 min 42 s 256.68 ms remaining ; 15 min 1 s 425.96 ms total) Tue Jun 16 17:38:13 2026: Iterated ≈84% of D-proof candidates. [45743765 of 54456864] (ETC: Tue Jun 16 17:40:36 2026 ; 2 min 23 s 66.48 ms remaining ; 14 min 54 s 165.44 ms total) Tue Jun 16 17:38:23 2026: Iterated ≈86% of D-proof candidates. [46832903 of 54456864] (ETC: Tue Jun 16 17:40:27 2026 ; 2 min 3 s 900.74 ms remaining ; 14 min 45 s 5.27 ms total) Tue Jun 16 17:38:35 2026: Iterated ≈88% of D-proof candidates. [47922040 of 54456864] (ETC: Tue Jun 16 17:40:21 2026 ; 1 min 45 s 432.31 ms remaining ; 14 min 38 s 602.53 ms total) Tue Jun 16 17:38:45 2026: Iterated ≈90% of D-proof candidates. [49011177 of 54456864] (ETC: Tue Jun 16 17:40:12 2026 ; 1 min 26 s 993.32 ms remaining ; 14 min 29 s 933.10 ms total) Tue Jun 16 17:38:58 2026: Iterated ≈92% of D-proof candidates. [50100314 of 54456864] (ETC: Tue Jun 16 17:40:07 2026 ; 1 min 9 s 222.76 ms remaining ; 14 min 25 s 284.29 ms total) Tue Jun 16 17:39:11 2026: Iterated ≈94% of D-proof candidates. [51189452 of 54456864] (ETC: Tue Jun 16 17:40:03 2026 ; 51 s 648.02 ms remaining ; 14 min 20 s 800.30 ms total) Tue Jun 16 17:39:21 2026: Iterated ≈96% of D-proof candidates. [52278589 of 54456864] (ETC: Tue Jun 16 17:39:55 2026 ; 34 s 125.25 ms remaining ; 14 min 13 s 131.09 ms total) Tue Jun 16 17:39:31 2026: Iterated ≈98% of D-proof candidates. [53367726 of 54456864] (ETC: Tue Jun 16 17:39:48 2026 ; 16 s 922.65 ms remaining ; 14 min 6 s 132.08 ms total) Tue Jun 16 17:39:44 2026: Iterated 100% of D-proof candidates. [54456864 of 54456864] (ETC: Tue Jun 16 17:39:44 2026 ; 0.00 ms remaining ; 14 min 2 s 44.16 ms total) 842035.31 ms (14 min 2 s 35.31 ms) taken to collect 110262 D-proofs of length 143. [iterated 54456864 condensed detachment proof strings] 84965.58 ms (1 min 24 s 965.58 ms) taken to detect 107139 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 } } 17.40 ms taken to filter and order new representative proofs. Found 3123 representative, 31130422 redundant, and 23323319 invalid condensed detachment proof strings. lengths up to 143 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123)} ; 3123 new representative proofs (31130422 redundant, 23323319 invalid) Tue Jun 16 17:41:09 2026: Starting to write 3123 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs143.txt. 3.48 ms taken to print and save 529758 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs143.txt. Determined the number of proof string candidates for iteration as 58948062. [most relevant: {41,103} with 2*3305124 = 6610248, i.e. ≈11.21%] Could not estimate removal count since there are no relevant entries yet. Tue Jun 16 17:41:09 2026: Starting to generate D-proof representatives of length 145. Tue Jun 16 17:41:23 2026: Iterated ≈ 2% of D-proof candidates. [ 1178961 of 58948062] (ETC: Tue Jun 16 17:52:34 2026 ; 11 min 11 s 387.51 ms remaining ; 11 min 25 s 89.29 ms total) Tue Jun 16 17:41:37 2026: Iterated ≈ 4% of D-proof candidates. [ 2357922 of 58948062] (ETC: Tue Jun 16 17:52:44 2026 ; 11 min 6 s 926.28 ms remaining ; 11 min 34 s 714.87 ms total) Tue Jun 16 17:41:54 2026: Iterated ≈ 6% of D-proof candidates. [ 3536883 of 58948062] (ETC: Tue Jun 16 17:53:35 2026 ; 11 min 41 s 248.93 ms remaining ; 12 min 26 s 9.48 ms total) Tue Jun 16 17:42:11 2026: Iterated ≈ 8% of D-proof candidates. [ 4715844 of 58948062] (ETC: Tue Jun 16 17:53:59 2026 ; 11 min 48 s 693.68 ms remaining ; 12 min 50 s 319.21 ms total) Tue Jun 16 17:42:29 2026: Iterated ≈10% of D-proof candidates. [ 5894806 of 58948062] (ETC: Tue Jun 16 17:54:31 2026 ; 12 min 1 s 337.28 ms remaining ; 13 min 21 s 485.87 ms total) Tue Jun 16 17:42:47 2026: Iterated ≈12% of D-proof candidates. [ 7073767 of 58948062] (ETC: Tue Jun 16 17:54:47 2026 ; 11 min 59 s 866.55 ms remaining ; 13 min 38 s 30.17 ms total) Tue Jun 16 17:43:07 2026: Iterated ≈14% of D-proof candidates. [ 8252728 of 58948062] (ETC: Tue Jun 16 17:55:14 2026 ; 12 min 6 s 299.32 ms remaining ; 14 min 4 s 534.08 ms total) Tue Jun 16 17:43:26 2026: Iterated ≈16% of D-proof candidates. [ 9431689 of 58948062] (ETC: Tue Jun 16 17:55:25 2026 ; 11 min 59 s 254.47 ms remaining ; 14 min 16 s 255.31 ms total) Tue Jun 16 17:43:46 2026: Iterated ≈18% of D-proof candidates. [10610651 of 58948062] (ETC: Tue Jun 16 17:55:43 2026 ; 11 min 56 s 743.79 ms remaining ; 14 min 34 s 77.78 ms total) Tue Jun 16 17:44:07 2026: Iterated ≈20% of D-proof candidates. [11789612 of 58948062] (ETC: Tue Jun 16 17:56:01 2026 ; 11 min 53 s 504.84 ms remaining ; 14 min 51 s 881.04 ms total) Tue Jun 16 17:44:28 2026: Iterated ≈22% of D-proof candidates. [12968573 of 58948062] (ETC: Tue Jun 16 17:56:15 2026 ; 11 min 46 s 291.44 ms remaining ; 15 min 5 s 501.83 ms total) Tue Jun 16 17:44:48 2026: Iterated ≈24% of D-proof candidates. [14147534 of 58948062] (ETC: Tue Jun 16 17:56:23 2026 ; 11 min 34 s 321.93 ms remaining ; 15 min 13 s 581.47 ms total) Tue Jun 16 17:45:11 2026: Iterated ≈26% of D-proof candidates. [15326496 of 58948062] (ETC: Tue Jun 16 17:56:38 2026 ; 11 min 27 s 294.39 ms remaining ; 15 min 28 s 776.21 ms total) Tue Jun 16 17:45:31 2026: Iterated ≈28% of D-proof candidates. [16505457 of 58948062] (ETC: Tue Jun 16 17:56:45 2026 ; 11 min 14 s 200.29 ms remaining ; 15 min 36 s 389.29 ms total) Tue Jun 16 17:45:53 2026: Iterated ≈30% of D-proof candidates. [17684418 of 58948062] (ETC: Tue Jun 16 17:56:57 2026 ; 11 min 3 s 194.63 ms remaining ; 15 min 47 s 420.88 ms total) Tue Jun 16 17:46:14 2026: Iterated ≈32% of D-proof candidates. [18863379 of 58948062] (ETC: Tue Jun 16 17:57:03 2026 ; 10 min 48 s 544.64 ms remaining ; 15 min 53 s 742.09 ms total) Tue Jun 16 17:46:35 2026: Iterated ≈34% of D-proof candidates. [20042341 of 58948062] (ETC: Tue Jun 16 17:57:07 2026 ; 10 min 32 s 545.24 ms remaining ; 15 min 58 s 401.88 ms total) Tue Jun 16 17:46:57 2026: Iterated ≈36% of D-proof candidates. [21221302 of 58948062] (ETC: Tue Jun 16 17:57:17 2026 ; 10 min 19 s 228.32 ms remaining ; 16 min 7 s 544.24 ms total) Tue Jun 16 17:47:20 2026: Iterated ≈38% of D-proof candidates. [22400263 of 58948062] (ETC: Tue Jun 16 17:57:24 2026 ; 10 min 4 s 629.24 ms remaining ; 16 min 15 s 208.43 ms total) Tue Jun 16 17:47:40 2026: Iterated ≈40% of D-proof candidates. [23579224 of 58948062] (ETC: Tue Jun 16 17:57:25 2026 ; 9 min 45 s 726.53 ms remaining ; 16 min 16 s 210.87 ms total) Tue Jun 16 17:48:06 2026: Iterated ≈42% of D-proof candidates. [24758186 of 58948062] (ETC: Tue Jun 16 17:57:41 2026 ; 9 min 35 s 217.52 ms remaining ; 16 min 31 s 754.34 ms total) Tue Jun 16 17:48:26 2026: Iterated ≈44% of D-proof candidates. [25937147 of 58948062] (ETC: Tue Jun 16 17:57:42 2026 ; 9 min 16 s 244.19 ms remaining ; 16 min 33 s 293.19 ms total) Tue Jun 16 17:48:46 2026: Iterated ≈46% of D-proof candidates. [27116108 of 58948062] (ETC: Tue Jun 16 17:57:41 2026 ; 8 min 55 s 832.75 ms remaining ; 16 min 32 s 282.86 ms total) Tue Jun 16 17:49:08 2026: Iterated ≈48% of D-proof candidates. [28295069 of 58948062] (ETC: Tue Jun 16 17:57:47 2026 ; 8 min 39 s 142.47 ms remaining ; 16 min 38 s 350.88 ms total) Tue Jun 16 17:49:33 2026: Iterated ≈50% of D-proof candidates. [29474031 of 58948062] (ETC: Tue Jun 16 17:57:56 2026 ; 8 min 23 s 451.80 ms remaining ; 16 min 46 s 903.59 ms total) Tue Jun 16 17:49:58 2026: Iterated ≈52% of D-proof candidates. [30652992 of 58948062] (ETC: Tue Jun 16 17:58:07 2026 ; 8 min 8 s 676.26 ms remaining ; 16 min 58 s 75.54 ms total) Tue Jun 16 17:50:22 2026: Iterated ≈54% of D-proof candidates. [31831953 of 58948062] (ETC: Tue Jun 16 17:58:13 2026 ; 7 min 51 s 174.30 ms remaining ; 17 min 4 s 291.93 ms total) Tue Jun 16 17:50:40 2026: Iterated ≈56% of D-proof candidates. [33010914 of 58948062] (ETC: Tue Jun 16 17:58:08 2026 ; 7 min 28 s 253.66 ms remaining ; 16 min 58 s 758.29 ms total) Tue Jun 16 17:51:02 2026: Iterated ≈58% of D-proof candidates. [34189875 of 58948062] (ETC: Tue Jun 16 17:58:12 2026 ; 7 min 9 s 477.49 ms remaining ; 17 min 2 s 565.41 ms total) Tue Jun 16 17:51:21 2026: Iterated ≈60% of D-proof candidates. [35368837 of 58948062] (ETC: Tue Jun 16 17:58:09 2026 ; 6 min 47 s 791.33 ms remaining ; 16 min 59 s 478.31 ms total) Tue Jun 16 17:51:34 2026: Iterated ≈62% of D-proof candidates. [36547798 of 58948062] (ETC: Tue Jun 16 17:57:57 2026 ; 6 min 23 s 146.51 ms remaining ; 16 min 48 s 280.26 ms total) Tue Jun 16 17:51:47 2026: Iterated ≈64% of D-proof candidates. [37726759 of 58948062] (ETC: Tue Jun 16 17:57:47 2026 ; 5 min 59 s 86.24 ms remaining ; 16 min 37 s 461.76 ms total) Tue Jun 16 17:52:00 2026: Iterated ≈66% of D-proof candidates. [38905720 of 58948062] (ETC: Tue Jun 16 17:57:35 2026 ; 5 min 35 s 77.34 ms remaining ; 16 min 25 s 521.54 ms total) Tue Jun 16 17:52:13 2026: Iterated ≈68% of D-proof candidates. [40084682 of 58948062] (ETC: Tue Jun 16 17:57:25 2026 ; 5 min 12 s 358.11 ms remaining ; 16 min 16 s 119.07 ms total) Tue Jun 16 17:52:23 2026: Iterated ≈70% of D-proof candidates. [41263643 of 58948062] (ETC: Tue Jun 16 17:57:11 2026 ; 4 min 48 s 721.09 ms remaining ; 16 min 2 s 403.63 ms total) Tue Jun 16 17:52:35 2026: Iterated ≈72% of D-proof candidates. [42442604 of 58948062] (ETC: Tue Jun 16 17:57:02 2026 ; 4 min 26 s 776.72 ms remaining ; 15 min 52 s 773.95 ms total) Tue Jun 16 17:52:45 2026: Iterated ≈74% of D-proof candidates. [43621565 of 58948062] (ETC: Tue Jun 16 17:56:50 2026 ; 4 min 4 s 664.17 ms remaining ; 15 min 41 s 16.00 ms total) Tue Jun 16 17:52:58 2026: Iterated ≈76% of D-proof candidates. [44800527 of 58948062] (ETC: Tue Jun 16 17:56:42 2026 ; 3 min 43 s 804.59 ms remaining ; 15 min 32 s 519.13 ms total) Tue Jun 16 17:53:09 2026: Iterated ≈78% of D-proof candidates. [45979488 of 58948062] (ETC: Tue Jun 16 17:56:32 2026 ; 3 min 23 s 92.50 ms remaining ; 15 min 23 s 147.68 ms total) Tue Jun 16 17:53:21 2026: Iterated ≈80% of D-proof candidates. [47158449 of 58948062] (ETC: Tue Jun 16 17:56:24 2026 ; 3 min 2 s 941.23 ms remaining ; 15 min 14 s 706.08 ms total) Tue Jun 16 17:53:33 2026: Iterated ≈82% of D-proof candidates. [48337410 of 58948062] (ETC: Tue Jun 16 17:56:16 2026 ; 2 min 43 s 234.67 ms remaining ; 15 min 6 s 859.20 ms total) Tue Jun 16 17:53:46 2026: Iterated ≈84% of D-proof candidates. [49516372 of 58948062] (ETC: Tue Jun 16 17:56:11 2026 ; 2 min 24 s 249.59 ms remaining ; 15 min 1 s 559.90 ms total) Tue Jun 16 17:54:00 2026: Iterated ≈86% of D-proof candidates. [50695333 of 58948062] (ETC: Tue Jun 16 17:56:05 2026 ; 2 min 5 s 484.14 ms remaining ; 14 min 56 s 315.23 ms total) Tue Jun 16 17:54:11 2026: Iterated ≈88% of D-proof candidates. [51874294 of 58948062] (ETC: Tue Jun 16 17:55:58 2026 ; 1 min 46 s 624.20 ms remaining ; 14 min 48 s 534.92 ms total) Tue Jun 16 17:54:24 2026: Iterated ≈90% of D-proof candidates. [53053255 of 58948062] (ETC: Tue Jun 16 17:55:53 2026 ; 1 min 28 s 345.95 ms remaining ; 14 min 43 s 459.43 ms total) Tue Jun 16 17:54:37 2026: Iterated ≈92% of D-proof candidates. [54232217 of 58948062] (ETC: Tue Jun 16 17:55:47 2026 ; 1 min 10 s 219.41 ms remaining ; 14 min 37 s 742.60 ms total) Tue Jun 16 17:54:49 2026: Iterated ≈94% of D-proof candidates. [55411178 of 58948062] (ETC: Tue Jun 16 17:55:41 2026 ; 52 s 310.42 ms remaining ; 14 min 31 s 840.29 ms total) Tue Jun 16 17:54:59 2026: Iterated ≈96% of D-proof candidates. [56590139 of 58948062] (ETC: Tue Jun 16 17:55:34 2026 ; 34 s 600.11 ms remaining ; 14 min 25 s 2.61 ms total) Tue Jun 16 17:55:14 2026: Iterated ≈98% of D-proof candidates. [57769100 of 58948062] (ETC: Tue Jun 16 17:55:31 2026 ; 17 s 233.43 ms remaining ; 14 min 21 s 670.72 ms total) Tue Jun 16 17:55:24 2026: Iterated 100% of D-proof candidates. [58948062 of 58948062] (ETC: Tue Jun 16 17:55:24 2026 ; 0.00 ms remaining ; 14 min 14 s 554.88 ms total) 854546.54 ms (14 min 14 s 546.54 ms) taken to collect 116000 D-proofs of length 145. [iterated 58948062 condensed detachment proof strings] 90253.47 ms (1 min 30 s 253.47 ms) taken to detect 113100 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 } } 14.21 ms taken to filter and order new representative proofs. Found 2900 representative, 33623117 redundant, and 25322045 invalid condensed detachment proof strings. lengths up to 145 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900)} ; 2900 new representative proofs (33623117 redundant, 25322045 invalid) Tue Jun 16 17:56:54 2026: Starting to write 2900 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs145.txt. 7.09 ms taken to print and save 498362 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs145.txt. Determined the number of proof string candidates for iteration as 63746634. [most relevant: {41,105} with 2*3574188 = 7148376, i.e. ≈11.21%] Estimated removal count set to 119392, based on entry 145:113100 and last known pair (143:107139, 145:113100) with 113100/107139 ≈ 1.05564 and 113100 * (113100/107139)^1 ≈ 119392.66. Tue Jun 16 17:56:54 2026: Starting to generate D-proof representatives of length 147. Tue Jun 16 17:57:09 2026: Iterated ≈ 2% of D-proof candidates. [ 1274932 of 63746634] (ETC: Tue Jun 16 18:09:09 2026 ; 12 min 47.55 ms remaining ; 12 min 14 s 742.39 ms total) Tue Jun 16 17:57:25 2026: Iterated ≈ 4% of D-proof candidates. [ 2549865 of 63746634] (ETC: Tue Jun 16 18:10:00 2026 ; 12 min 34 s 171.24 ms remaining ; 13 min 5 s 595.03 ms total) Tue Jun 16 17:57:45 2026: Iterated ≈ 6% of D-proof candidates. [ 3824798 of 63746634] (ETC: Tue Jun 16 18:11:12 2026 ; 13 min 26 s 597.46 ms remaining ; 14 min 18 s 82.41 ms total) Tue Jun 16 17:58:07 2026: Iterated ≈ 8% of D-proof candidates. [ 5099730 of 63746634] (ETC: Tue Jun 16 18:12:05 2026 ; 13 min 57 s 869.05 ms remaining ; 15 min 10 s 727.22 ms total) Tue Jun 16 17:58:26 2026: Iterated ≈10% of D-proof candidates. [ 6374663 of 63746634] (ETC: Tue Jun 16 18:12:19 2026 ; 13 min 52 s 322.66 ms remaining ; 15 min 24 s 802.95 ms total) Tue Jun 16 17:58:49 2026: Iterated ≈12% of D-proof candidates. [ 7649596 of 63746634] (ETC: Tue Jun 16 18:12:52 2026 ; 14 min 2 s 912.22 ms remaining ; 15 min 57 s 854.79 ms total) Tue Jun 16 17:59:11 2026: Iterated ≈14% of D-proof candidates. [ 8924528 of 63746634] (ETC: Tue Jun 16 18:13:11 2026 ; 14 min 237.42 ms remaining ; 16 min 17 s 20.25 ms total) Tue Jun 16 17:59:31 2026: Iterated ≈16% of D-proof candidates. [10199461 of 63746634] (ETC: Tue Jun 16 18:13:15 2026 ; 13 min 43 s 735.40 ms remaining ; 16 min 20 s 637.38 ms total) Tue Jun 16 17:59:52 2026: Iterated ≈18% of D-proof candidates. [11474394 of 63746634] (ETC: Tue Jun 16 18:13:24 2026 ; 13 min 32 s 110.68 ms remaining ; 16 min 30 s 378.88 ms total) Tue Jun 16 18:00:13 2026: Iterated ≈20% of D-proof candidates. [12749326 of 63746634] (ETC: Tue Jun 16 18:13:29 2026 ; 13 min 15 s 681.57 ms remaining ; 16 min 34 s 601.95 ms total) Tue Jun 16 18:00:33 2026: Iterated ≈22% of D-proof candidates. [14024259 of 63746634] (ETC: Tue Jun 16 18:13:28 2026 ; 12 min 55 s 679.94 ms remaining ; 16 min 34 s 461.46 ms total) Tue Jun 16 18:00:54 2026: Iterated ≈24% of D-proof candidates. [15299192 of 63746634] (ETC: Tue Jun 16 18:13:35 2026 ; 12 min 40 s 930.20 ms remaining ; 16 min 41 s 223.94 ms total) Tue Jun 16 18:01:15 2026: Iterated ≈26% of D-proof candidates. [16574124 of 63746634] (ETC: Tue Jun 16 18:13:37 2026 ; 12 min 22 s 350.74 ms remaining ; 16 min 43 s 176.66 ms total) Tue Jun 16 18:01:34 2026: Iterated ≈28% of D-proof candidates. [17849057 of 63746634] (ETC: Tue Jun 16 18:13:33 2026 ; 11 min 59 s 408.60 ms remaining ; 16 min 39 s 178.60 ms total) Tue Jun 16 18:01:54 2026: Iterated ≈30% of D-proof candidates. [19123990 of 63746634] (ETC: Tue Jun 16 18:13:34 2026 ; 11 min 40 s 49.38 ms remaining ; 16 min 40 s 70.54 ms total) Tue Jun 16 18:02:18 2026: Iterated ≈32% of D-proof candidates. [20398922 of 63746634] (ETC: Tue Jun 16 18:13:47 2026 ; 11 min 28 s 592.55 ms remaining ; 16 min 52 s 636.09 ms total) Tue Jun 16 18:02:39 2026: Iterated ≈34% of D-proof candidates. [21673855 of 63746634] (ETC: Tue Jun 16 18:13:49 2026 ; 11 min 9 s 979.11 ms remaining ; 16 min 55 s 119.85 ms total) Tue Jun 16 18:03:00 2026: Iterated ≈36% of D-proof candidates. [22948788 of 63746634] (ETC: Tue Jun 16 18:13:52 2026 ; 10 min 51 s 607.06 ms remaining ; 16 min 58 s 136.02 ms total) Tue Jun 16 18:03:24 2026: Iterated ≈38% of D-proof candidates. [24223720 of 63746634] (ETC: Tue Jun 16 18:14:01 2026 ; 10 min 36 s 838.46 ms remaining ; 17 min 7 s 158.79 ms total) Tue Jun 16 18:03:48 2026: Iterated ≈40% of D-proof candidates. [25498653 of 63746634] (ETC: Tue Jun 16 18:14:09 2026 ; 10 min 21 s 305.56 ms remaining ; 17 min 15 s 509.25 ms total) Tue Jun 16 18:04:11 2026: Iterated ≈42% of D-proof candidates. [26773586 of 63746634] (ETC: Tue Jun 16 18:14:14 2026 ; 10 min 3 s 56.36 ms remaining ; 17 min 19 s 752.34 ms total) Tue Jun 16 18:04:33 2026: Iterated ≈44% of D-proof candidates. [28048518 of 63746634] (ETC: Tue Jun 16 18:14:16 2026 ; 9 min 43 s 801.61 ms remaining ; 17 min 22 s 502.84 ms total) Tue Jun 16 18:04:58 2026: Iterated ≈46% of D-proof candidates. [29323451 of 63746634] (ETC: Tue Jun 16 18:14:26 2026 ; 9 min 27 s 878.89 ms remaining ; 17 min 31 s 627.56 ms total) Tue Jun 16 18:05:24 2026: Iterated ≈48% of D-proof candidates. [30598384 of 63746634] (ETC: Tue Jun 16 18:14:37 2026 ; 9 min 12 s 979.05 ms remaining ; 17 min 43 s 421.25 ms total) Tue Jun 16 18:05:50 2026: Iterated ≈50% of D-proof candidates. [31873317 of 63746634] (ETC: Tue Jun 16 18:14:46 2026 ; 8 min 56 s 78.66 ms remaining ; 17 min 52 s 157.32 ms total) Tue Jun 16 18:06:14 2026: Iterated ≈52% of D-proof candidates. [33148249 of 63746634] (ETC: Tue Jun 16 18:14:51 2026 ; 8 min 36 s 919.43 ms remaining ; 17 min 56 s 915.46 ms total) Tue Jun 16 18:06:36 2026: Iterated ≈54% of D-proof candidates. [34423182 of 63746634] (ETC: Tue Jun 16 18:14:52 2026 ; 8 min 15 s 828.30 ms remaining ; 17 min 57 s 887.59 ms total) Tue Jun 16 18:07:01 2026: Iterated ≈56% of D-proof candidates. [35698115 of 63746634] (ETC: Tue Jun 16 18:14:57 2026 ; 7 min 56 s 684.76 ms remaining ; 18 min 3 s 374.46 ms total) Tue Jun 16 18:07:22 2026: Iterated ≈58% of D-proof candidates. [36973047 of 63746634] (ETC: Tue Jun 16 18:14:56 2026 ; 7 min 34 s 615.92 ms remaining ; 18 min 2 s 418.83 ms total) Tue Jun 16 18:07:37 2026: Iterated ≈60% of D-proof candidates. [38247980 of 63746634] (ETC: Tue Jun 16 18:14:45 2026 ; 7 min 8 s 504.52 ms remaining ; 17 min 51 s 261.28 ms total) Tue Jun 16 18:07:52 2026: Iterated ≈62% of D-proof candidates. [39522913 of 63746634] (ETC: Tue Jun 16 18:14:35 2026 ; 6 min 43 s 306.04 ms remaining ; 17 min 41 s 331.67 ms total) Tue Jun 16 18:08:03 2026: Iterated ≈64% of D-proof candidates. [40797845 of 63746634] (ETC: Tue Jun 16 18:14:20 2026 ; 6 min 16 s 422.36 ms remaining ; 17 min 25 s 617.64 ms total) Tue Jun 16 18:08:17 2026: Iterated ≈66% of D-proof candidates. [42072778 of 63746634] (ETC: Tue Jun 16 18:14:08 2026 ; 5 min 51 s 739.31 ms remaining ; 17 min 14 s 527.36 ms total) Tue Jun 16 18:08:31 2026: Iterated ≈68% of D-proof candidates. [43347711 of 63746634] (ETC: Tue Jun 16 18:13:59 2026 ; 5 min 28 s 154.30 ms remaining ; 17 min 5 s 482.19 ms total) Tue Jun 16 18:08:44 2026: Iterated ≈70% of D-proof candidates. [44622643 of 63746634] (ETC: Tue Jun 16 18:13:49 2026 ; 5 min 4 s 484.86 ms remaining ; 16 min 54 s 949.50 ms total) Tue Jun 16 18:08:58 2026: Iterated ≈72% of D-proof candidates. [45897576 of 63746634] (ETC: Tue Jun 16 18:13:39 2026 ; 4 min 41 s 471.72 ms remaining ; 16 min 45 s 256.12 ms total) Tue Jun 16 18:09:11 2026: Iterated ≈74% of D-proof candidates. [47172509 of 63746634] (ETC: Tue Jun 16 18:13:30 2026 ; 4 min 18 s 860.62 ms remaining ; 16 min 35 s 617.76 ms total) Tue Jun 16 18:09:23 2026: Iterated ≈76% of D-proof candidates. [48447441 of 63746634] (ETC: Tue Jun 16 18:13:19 2026 ; 3 min 56 s 427.12 ms remaining ; 16 min 25 s 112.94 ms total) Tue Jun 16 18:09:32 2026: Iterated ≈78% of D-proof candidates. [49722374 of 63746634] (ETC: Tue Jun 16 18:13:06 2026 ; 3 min 33 s 930.94 ms remaining ; 16 min 12 s 413.32 ms total) Tue Jun 16 18:09:46 2026: Iterated ≈80% of D-proof candidates. [50997307 of 63746634] (ETC: Tue Jun 16 18:12:59 2026 ; 3 min 13 s 40.80 ms remaining ; 16 min 5 s 203.96 ms total) Tue Jun 16 18:09:58 2026: Iterated ≈82% of D-proof candidates. [52272239 of 63746634] (ETC: Tue Jun 16 18:12:51 2026 ; 2 min 52 s 189.08 ms remaining ; 15 min 56 s 605.95 ms total) Tue Jun 16 18:10:09 2026: Iterated ≈84% of D-proof candidates. [53547172 of 63746634] (ETC: Tue Jun 16 18:12:41 2026 ; 2 min 31 s 539.72 ms remaining ; 15 min 47 s 123.23 ms total) Tue Jun 16 18:10:21 2026: Iterated ≈86% of D-proof candidates. [54822105 of 63746634] (ETC: Tue Jun 16 18:12:33 2026 ; 2 min 11 s 464.27 ms remaining ; 15 min 39 s 30.46 ms total) Tue Jun 16 18:10:33 2026: Iterated ≈88% of D-proof candidates. [56097037 of 63746634] (ETC: Tue Jun 16 18:12:25 2026 ; 1 min 51 s 712.09 ms remaining ; 15 min 30 s 933.94 ms total) Tue Jun 16 18:10:45 2026: Iterated ≈90% of D-proof candidates. [57371970 of 63746634] (ETC: Tue Jun 16 18:12:17 2026 ; 1 min 32 s 340.18 ms remaining ; 15 min 23 s 401.71 ms total) Tue Jun 16 18:10:58 2026: Iterated ≈92% of D-proof candidates. [58646903 of 63746634] (ETC: Tue Jun 16 18:12:11 2026 ; 1 min 13 s 359.76 ms remaining ; 15 min 16 s 997.02 ms total) Tue Jun 16 18:11:10 2026: Iterated ≈94% of D-proof candidates. [59921835 of 63746634] (ETC: Tue Jun 16 18:12:04 2026 ; 54 s 631.41 ms remaining ; 15 min 10 s 523.37 ms total) Tue Jun 16 18:11:21 2026: Iterated ≈96% of D-proof candidates. [61196768 of 63746634] (ETC: Tue Jun 16 18:11:57 2026 ; 36 s 135.83 ms remaining ; 15 min 3 s 395.43 ms total) Tue Jun 16 18:11:35 2026: Iterated ≈98% of D-proof candidates. [62471701 of 63746634] (ETC: Tue Jun 16 18:11:53 2026 ; 17 s 982.71 ms remaining ; 14 min 59 s 135.10 ms total) Tue Jun 16 18:11:47 2026: Iterated 100% of D-proof candidates. [63746634 of 63746634] (ETC: Tue Jun 16 18:11:47 2026 ; 0.00 ms remaining ; 14 min 52 s 917.07 ms total) 892908.14 ms (14 min 52 s 908.14 ms) taken to collect 123586 D-proofs of length 147. [iterated 63746634 condensed detachment proof strings] Tue Jun 16 18:11:49 2026: Removed ≈ 2% of redundant conclusions. [ 2387 of approximately 119392] (ETC: Tue Jun 16 18:13:19 2026 ; 1 min 30 s 148.50 ms remaining ; 1 min 31 s 987.61 ms total) Tue Jun 16 18:11:50 2026: Removed ≈ 4% of redundant conclusions. [ 4775 of approximately 119392] (ETC: Tue Jun 16 18:13:18 2026 ; 1 min 27 s 305.94 ms remaining ; 1 min 30 s 943.15 ms total) Tue Jun 16 18:11:53 2026: Removed ≈ 6% of redundant conclusions. [ 7163 of approximately 119392] (ETC: Tue Jun 16 18:13:23 2026 ; 1 min 29 s 923.08 ms remaining ; 1 min 35 s 662.41 ms total) Tue Jun 16 18:11:54 2026: Removed ≈ 8% of redundant conclusions. [ 9551 of approximately 119392] (ETC: Tue Jun 16 18:13:22 2026 ; 1 min 27 s 822.61 ms remaining ; 1 min 35 s 459.05 ms total) Tue Jun 16 18:11:56 2026: Removed ≈ 10% of redundant conclusions. [ 11939 of approximately 119392] (ETC: Tue Jun 16 18:13:23 2026 ; 1 min 26 s 280.54 ms remaining ; 1 min 35 s 867.09 ms total) Tue Jun 16 18:11:59 2026: Removed ≈ 12% of redundant conclusions. [ 14327 of approximately 119392] (ETC: Tue Jun 16 18:13:24 2026 ; 1 min 25 s 511.83 ms remaining ; 1 min 37 s 172.50 ms total) Tue Jun 16 18:12:01 2026: Removed ≈ 14% of redundant conclusions. [ 16714 of approximately 119392] (ETC: Tue Jun 16 18:13:24 2026 ; 1 min 23 s 847.64 ms remaining ; 1 min 37 s 496.42 ms total) Tue Jun 16 18:12:03 2026: Removed ≈ 16% of redundant conclusions. [ 19102 of approximately 119392] (ETC: Tue Jun 16 18:13:25 2026 ; 1 min 22 s 391.41 ms remaining ; 1 min 38 s 84.30 ms total) Tue Jun 16 18:12:05 2026: Removed ≈ 18% of redundant conclusions. [ 21490 of approximately 119392] (ETC: Tue Jun 16 18:13:25 2026 ; 1 min 20 s 745.29 ms remaining ; 1 min 38 s 469.30 ms total) Tue Jun 16 18:12:07 2026: Removed ≈ 20% of redundant conclusions. [ 23878 of approximately 119392] (ETC: Tue Jun 16 18:13:25 2026 ; 1 min 18 s 858.16 ms remaining ; 1 min 38 s 572.29 ms total) Tue Jun 16 18:12:09 2026: Removed ≈ 22% of redundant conclusions. [ 26266 of approximately 119392] (ETC: Tue Jun 16 18:13:25 2026 ; 1 min 16 s 931.03 ms remaining ; 1 min 38 s 629.27 ms total) Tue Jun 16 18:12:11 2026: Removed ≈ 24% of redundant conclusions. [ 28654 of approximately 119392] (ETC: Tue Jun 16 18:13:26 2026 ; 1 min 15 s 374.42 ms remaining ; 1 min 39 s 176.78 ms total) Tue Jun 16 18:12:13 2026: Removed ≈ 26% of redundant conclusions. [ 31041 of approximately 119392] (ETC: Tue Jun 16 18:13:26 2026 ; 1 min 13 s 733.94 ms remaining ; 1 min 39 s 639.42 ms total) Tue Jun 16 18:12:15 2026: Removed ≈ 28% of redundant conclusions. [ 33429 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 1 min 12 s 245.55 ms remaining ; 1 min 40 s 340.16 ms total) Tue Jun 16 18:12:17 2026: Removed ≈ 30% of redundant conclusions. [ 35817 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 10 s 736.07 ms remaining ; 1 min 41 s 50.80 ms total) Tue Jun 16 18:12:19 2026: Removed ≈ 32% of redundant conclusions. [ 38205 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 8 s 593.71 ms remaining ; 1 min 40 s 872.56 ms total) Tue Jun 16 18:12:21 2026: Removed ≈ 34% of redundant conclusions. [ 40593 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 6 s 445.14 ms remaining ; 1 min 40 s 674.10 ms total) Tue Jun 16 18:12:23 2026: Removed ≈ 36% of redundant conclusions. [ 42981 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 4 s 828.88 ms remaining ; 1 min 41 s 294.96 ms total) Tue Jun 16 18:12:25 2026: Removed ≈ 38% of redundant conclusions. [ 45368 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 2 s 705.67 ms remaining ; 1 min 41 s 136.87 ms total) Tue Jun 16 18:12:27 2026: Removed ≈ 40% of redundant conclusions. [ 47756 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 1 min 531.65 ms remaining ; 1 min 40 s 884.96 ms total) Tue Jun 16 18:12:29 2026: Removed ≈ 42% of redundant conclusions. [ 50144 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 58 s 170.32 ms remaining ; 1 min 40 s 292.73 ms total) Tue Jun 16 18:12:31 2026: Removed ≈ 44% of redundant conclusions. [ 52532 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 56 s 125.03 ms remaining ; 1 min 40 s 222.56 ms total) Tue Jun 16 18:12:33 2026: Removed ≈ 46% of redundant conclusions. [ 54920 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 54 s 96.42 ms remaining ; 1 min 40 s 178.05 ms total) Tue Jun 16 18:12:35 2026: Removed ≈ 48% of redundant conclusions. [ 57308 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 51 s 954.50 ms remaining ; 1 min 39 s 912.24 ms total) Tue Jun 16 18:12:37 2026: Removed ≈ 50% of redundant conclusions. [ 59696 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 49 s 940.86 ms remaining ; 1 min 39 s 881.71 ms total) Tue Jun 16 18:12:39 2026: Removed ≈ 52% of redundant conclusions. [ 62083 of approximately 119392] (ETC: Tue Jun 16 18:13:26 2026 ; 47 s 725.31 ms remaining ; 1 min 39 s 426.26 ms total) Tue Jun 16 18:12:41 2026: Removed ≈ 54% of redundant conclusions. [ 64471 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 45 s 889.53 ms remaining ; 1 min 39 s 758.61 ms total) Tue Jun 16 18:12:43 2026: Removed ≈ 56% of redundant conclusions. [ 66859 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 43 s 904.29 ms remaining ; 1 min 39 s 781.48 ms total) Tue Jun 16 18:12:45 2026: Removed ≈ 58% of redundant conclusions. [ 69247 of approximately 119392] (ETC: Tue Jun 16 18:13:26 2026 ; 41 s 852.29 ms remaining ; 1 min 39 s 647.60 ms total) Tue Jun 16 18:12:47 2026: Removed ≈ 60% of redundant conclusions. [ 71635 of approximately 119392] (ETC: Tue Jun 16 18:13:26 2026 ; 39 s 831.22 ms remaining ; 1 min 39 s 577.64 ms total) Tue Jun 16 18:12:49 2026: Removed ≈ 62% of redundant conclusions. [ 74023 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 37 s 955.03 ms remaining ; 1 min 39 s 881.57 ms total) Tue Jun 16 18:12:51 2026: Removed ≈ 64% of redundant conclusions. [ 76410 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 36 s 49.90 ms remaining ; 1 min 40 s 136.57 ms total) Tue Jun 16 18:12:53 2026: Removed ≈ 66% of redundant conclusions. [ 78798 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 34 s 83.74 ms remaining ; 1 min 40 s 244.53 ms total) Tue Jun 16 18:12:55 2026: Removed ≈ 68% of redundant conclusions. [ 81186 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 32 s 143.24 ms remaining ; 1 min 40 s 446.14 ms total) Tue Jun 16 18:12:57 2026: Removed ≈ 70% of redundant conclusions. [ 83574 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 30 s 191.21 ms remaining ; 1 min 40 s 636.24 ms total) Tue Jun 16 18:12:59 2026: Removed ≈ 72% of redundant conclusions. [ 85962 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 28 s 250.01 ms remaining ; 1 min 40 s 892.16 ms total) Tue Jun 16 18:13:01 2026: Removed ≈ 74% of redundant conclusions. [ 88350 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 26 s 150.21 ms remaining ; 1 min 40 s 577.47 ms total) Tue Jun 16 18:13:03 2026: Removed ≈ 76% of redundant conclusions. [ 90737 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 24 s 174.51 ms remaining ; 1 min 40 s 723.89 ms total) Tue Jun 16 18:13:06 2026: Removed ≈ 78% of redundant conclusions. [ 93125 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 22 s 185.42 ms remaining ; 1 min 40 s 839.92 ms total) Tue Jun 16 18:13:08 2026: Removed ≈ 80% of redundant conclusions. [ 95513 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 20 s 178.54 ms remaining ; 1 min 40 s 890.15 ms total) Tue Jun 16 18:13:10 2026: Removed ≈ 82% of redundant conclusions. [ 97901 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 18 s 182.37 ms remaining ; 1 min 41 s 11.11 ms total) Tue Jun 16 18:13:12 2026: Removed ≈ 84% of redundant conclusions. [100289 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 16 s 144.44 ms remaining ; 1 min 40 s 901.29 ms total) Tue Jun 16 18:13:14 2026: Removed ≈ 86% of redundant conclusions. [102677 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 14 s 112.76 ms remaining ; 1 min 40 s 804.72 ms total) Tue Jun 16 18:13:15 2026: Removed ≈ 88% of redundant conclusions. [105064 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 12 s 77.70 ms remaining ; 1 min 40 s 640.77 ms total) Tue Jun 16 18:13:17 2026: Removed ≈ 90% of redundant conclusions. [107452 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 10 s 44.10 ms remaining ; 1 min 40 s 434.27 ms total) Tue Jun 16 18:13:19 2026: Removed ≈ 92% of redundant conclusions. [109840 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 8 s 35.83 ms remaining ; 1 min 40 s 441.11 ms total) Tue Jun 16 18:13:21 2026: Removed ≈ 94% of redundant conclusions. [112228 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 6 s 25.86 ms remaining ; 1 min 40 s 424.26 ms total) Tue Jun 16 18:13:23 2026: Removed ≈ 96% of redundant conclusions. [114616 of approximately 119392] (ETC: Tue Jun 16 18:13:27 2026 ; 4 s 24.22 ms remaining ; 1 min 40 s 598.74 ms total) Tue Jun 16 18:13:26 2026: Removed ≈ 98% of redundant conclusions. [117004 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 2 s 14.33 ms remaining ; 1 min 40 s 709.98 ms total) Tue Jun 16 18:13:28 2026: Removed ≈100% of redundant conclusions. [119392 of approximately 119392] (ETC: Tue Jun 16 18:13:28 2026 ; 0.00 ms remaining ; 1 min 40 s 725.76 ms total) 101839.56 ms (1 min 41 s 839.55 ms) taken to detect 120397 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 } } 16.38 ms taken to filter and order new representative proofs. Found 3189 representative, 36251074 redundant, and 27492371 invalid condensed detachment proof strings. lengths up to 147 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189)} ; 3189 new representative proofs (36251074 redundant, 27492371 invalid) Tue Jun 16 18:13:29 2026: Starting to write 3189 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs147.txt. 3.79 ms taken to print and save 554540 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs147.txt. Determined the number of proof string candidates for iteration as 68708352. [most relevant: {41,107} with 2*3822648 = 7645296, i.e. ≈11.13%] Estimated removal count set to 128164, based on entry 147:120397 and last known pair (145:113100, 147:120397) with 120397/113100 ≈ 1.06452 and 120397 * (120397/113100)^1 ≈ 128164.79. Tue Jun 16 18:13:29 2026: Starting to generate D-proof representatives of length 149. Tue Jun 16 18:13:44 2026: Iterated ≈ 2% of D-proof candidates. [ 1374167 of 68708352] (ETC: Tue Jun 16 18:26:07 2026 ; 12 min 22 s 686.46 ms remaining ; 12 min 37 s 843.32 ms total) Tue Jun 16 18:14:03 2026: Iterated ≈ 4% of D-proof candidates. [ 2748334 of 68708352] (ETC: Tue Jun 16 18:27:47 2026 ; 13 min 43 s 535.11 ms remaining ; 14 min 17 s 849.07 ms total) Tue Jun 16 18:14:25 2026: Iterated ≈ 6% of D-proof candidates. [ 4122501 of 68708352] (ETC: Tue Jun 16 18:29:14 2026 ; 14 min 48 s 585.85 ms remaining ; 15 min 45 s 304.09 ms total) Tue Jun 16 18:14:47 2026: Iterated ≈ 8% of D-proof candidates. [ 5496668 of 68708352] (ETC: Tue Jun 16 18:29:44 2026 ; 14 min 57 s 672.36 ms remaining ; 16 min 15 s 730.83 ms total) Tue Jun 16 18:15:08 2026: Iterated ≈10% of D-proof candidates. [ 6870835 of 68708352] (ETC: Tue Jun 16 18:29:58 2026 ; 14 min 50 s 780.98 ms remaining ; 16 min 29 s 756.64 ms total) Tue Jun 16 18:15:30 2026: Iterated ≈12% of D-proof candidates. [ 8245002 of 68708352] (ETC: Tue Jun 16 18:30:18 2026 ; 14 min 48 s 608.85 ms remaining ; 16 min 49 s 782.78 ms total) Tue Jun 16 18:15:50 2026: Iterated ≈14% of D-proof candidates. [ 9619169 of 68708352] (ETC: Tue Jun 16 18:30:21 2026 ; 14 min 30 s 185.51 ms remaining ; 16 min 51 s 843.62 ms total) Tue Jun 16 18:16:16 2026: Iterated ≈16% of D-proof candidates. [10993336 of 68708352] (ETC: Tue Jun 16 18:30:53 2026 ; 14 min 36 s 821.18 ms remaining ; 17 min 23 s 834.73 ms total) Tue Jun 16 18:16:41 2026: Iterated ≈18% of D-proof candidates. [12367503 of 68708352] (ETC: Tue Jun 16 18:31:16 2026 ; 14 min 34 s 880.74 ms remaining ; 17 min 46 s 927.72 ms total) Tue Jun 16 18:17:02 2026: Iterated ≈20% of D-proof candidates. [13741670 of 68708352] (ETC: Tue Jun 16 18:31:17 2026 ; 14 min 15 s 32.94 ms remaining ; 17 min 48 s 791.16 ms total) Tue Jun 16 18:17:25 2026: Iterated ≈22% of D-proof candidates. [15115837 of 68708352] (ETC: Tue Jun 16 18:31:22 2026 ; 13 min 57 s 299.92 ms remaining ; 17 min 53 s 461.43 ms total) Tue Jun 16 18:17:53 2026: Iterated ≈24% of D-proof candidates. [16490004 of 68708352] (ETC: Tue Jun 16 18:31:49 2026 ; 13 min 56 s 108.02 ms remaining ; 18 min 20 s 142.12 ms total) Tue Jun 16 18:18:17 2026: Iterated ≈26% of D-proof candidates. [17864171 of 68708352] (ETC: Tue Jun 16 18:31:58 2026 ; 13 min 40 s 775.28 ms remaining ; 18 min 29 s 155.78 ms total) Tue Jun 16 18:18:46 2026: Iterated ≈28% of D-proof candidates. [19238338 of 68708352] (ETC: Tue Jun 16 18:32:22 2026 ; 13 min 35 s 773.26 ms remaining ; 18 min 53 s 18.41 ms total) Tue Jun 16 18:19:13 2026: Iterated ≈30% of D-proof candidates. [20612505 of 68708352] (ETC: Tue Jun 16 18:32:37 2026 ; 13 min 23 s 986.68 ms remaining ; 19 min 8 s 552.39 ms total) Tue Jun 16 18:19:37 2026: Iterated ≈32% of D-proof candidates. [21986672 of 68708352] (ETC: Tue Jun 16 18:32:40 2026 ; 13 min 2 s 671.67 ms remaining ; 19 min 10 s 987.74 ms total) Tue Jun 16 18:19:59 2026: Iterated ≈34% of D-proof candidates. [23360839 of 68708352] (ETC: Tue Jun 16 18:32:37 2026 ; 12 min 38 s 156.28 ms remaining ; 19 min 8 s 721.62 ms total) Tue Jun 16 18:20:25 2026: Iterated ≈36% of D-proof candidates. [24735006 of 68708352] (ETC: Tue Jun 16 18:32:46 2026 ; 12 min 20 s 861.96 ms remaining ; 19 min 17 s 596.80 ms total) Tue Jun 16 18:20:51 2026: Iterated ≈38% of D-proof candidates. [26109173 of 68708352] (ETC: Tue Jun 16 18:32:52 2026 ; 12 min 1 s 280.76 ms remaining ; 19 min 23 s 356.05 ms total) Tue Jun 16 18:21:17 2026: Iterated ≈40% of D-proof candidates. [27483340 of 68708352] (ETC: Tue Jun 16 18:32:58 2026 ; 11 min 41 s 749.17 ms remaining ; 19 min 29 s 581.93 ms total) Tue Jun 16 18:21:40 2026: Iterated ≈42% of D-proof candidates. [28857507 of 68708352] (ETC: Tue Jun 16 18:32:59 2026 ; 11 min 18 s 605.70 ms remaining ; 19 min 30 s 9.81 ms total) Tue Jun 16 18:22:05 2026: Iterated ≈44% of D-proof candidates. [30231674 of 68708352] (ETC: Tue Jun 16 18:33:02 2026 ; 10 min 56 s 775.05 ms remaining ; 19 min 32 s 812.57 ms total) Tue Jun 16 18:22:31 2026: Iterated ≈46% of D-proof candidates. [31605841 of 68708352] (ETC: Tue Jun 16 18:33:08 2026 ; 10 min 36 s 564.96 ms remaining ; 19 min 38 s 823.98 ms total) Tue Jun 16 18:22:57 2026: Iterated ≈48% of D-proof candidates. [32980008 of 68708352] (ETC: Tue Jun 16 18:33:12 2026 ; 10 min 15 s 230.97 ms remaining ; 19 min 43 s 136.46 ms total) Tue Jun 16 18:23:21 2026: Iterated ≈50% of D-proof candidates. [34354176 of 68708352] (ETC: Tue Jun 16 18:33:13 2026 ; 9 min 51 s 986.86 ms remaining ; 19 min 43 s 973.72 ms total) Tue Jun 16 18:23:43 2026: Iterated ≈52% of D-proof candidates. [35728343 of 68708352] (ETC: Tue Jun 16 18:33:10 2026 ; 9 min 27 s 7.51 ms remaining ; 19 min 41 s 265.64 ms total) Tue Jun 16 18:24:07 2026: Iterated ≈54% of D-proof candidates. [37102510 of 68708352] (ETC: Tue Jun 16 18:33:10 2026 ; 9 min 3 s 621.61 ms remaining ; 19 min 41 s 786.11 ms total) Tue Jun 16 18:24:29 2026: Iterated ≈56% of D-proof candidates. [38476677 of 68708352] (ETC: Tue Jun 16 18:33:07 2026 ; 8 min 38 s 513.87 ms remaining ; 19 min 38 s 440.62 ms total) Tue Jun 16 18:24:44 2026: Iterated ≈58% of D-proof candidates. [39850844 of 68708352] (ETC: Tue Jun 16 18:32:54 2026 ; 8 min 9 s 242.54 ms remaining ; 19 min 24 s 863.18 ms total) Tue Jun 16 18:24:59 2026: Iterated ≈60% of D-proof candidates. [41225011 of 68708352] (ETC: Tue Jun 16 18:32:39 2026 ; 7 min 40 s 308.33 ms remaining ; 19 min 10 s 770.83 ms total) Tue Jun 16 18:25:14 2026: Iterated ≈62% of D-proof candidates. [42599178 of 68708352] (ETC: Tue Jun 16 18:32:26 2026 ; 7 min 12 s 0.13 ms remaining ; 18 min 56 s 842.45 ms total) Tue Jun 16 18:25:28 2026: Iterated ≈64% of D-proof candidates. [43973345 of 68708352] (ETC: Tue Jun 16 18:32:13 2026 ; 6 min 44 s 794.78 ms remaining ; 18 min 44 s 429.94 ms total) Tue Jun 16 18:25:42 2026: Iterated ≈66% of D-proof candidates. [45347512 of 68708352] (ETC: Tue Jun 16 18:32:00 2026 ; 6 min 17 s 983.14 ms remaining ; 18 min 31 s 715.11 ms total) Tue Jun 16 18:25:56 2026: Iterated ≈68% of D-proof candidates. [46721679 of 68708352] (ETC: Tue Jun 16 18:31:47 2026 ; 5 min 51 s 541.53 ms remaining ; 18 min 18 s 567.25 ms total) Tue Jun 16 18:26:09 2026: Iterated ≈70% of D-proof candidates. [48095846 of 68708352] (ETC: Tue Jun 16 18:31:35 2026 ; 5 min 25 s 980.65 ms remaining ; 18 min 6 s 602.16 ms total) Tue Jun 16 18:26:22 2026: Iterated ≈72% of D-proof candidates. [49470013 of 68708352] (ETC: Tue Jun 16 18:31:22 2026 ; 5 min 635.32 ms remaining ; 17 min 53 s 697.53 ms total) Tue Jun 16 18:26:35 2026: Iterated ≈74% of D-proof candidates. [50844180 of 68708352] (ETC: Tue Jun 16 18:31:12 2026 ; 4 min 36 s 387.38 ms remaining ; 17 min 43 s 28.38 ms total) Tue Jun 16 18:26:50 2026: Iterated ≈76% of D-proof candidates. [52218347 of 68708352] (ETC: Tue Jun 16 18:31:03 2026 ; 4 min 12 s 941.00 ms remaining ; 17 min 33 s 920.82 ms total) Tue Jun 16 18:27:06 2026: Iterated ≈78% of D-proof candidates. [53592514 of 68708352] (ETC: Tue Jun 16 18:30:57 2026 ; 3 min 50 s 561.35 ms remaining ; 17 min 28 s 6.11 ms total) Tue Jun 16 18:27:22 2026: Iterated ≈80% of D-proof candidates. [54966681 of 68708352] (ETC: Tue Jun 16 18:30:51 2026 ; 3 min 28 s 425.18 ms remaining ; 17 min 22 s 125.87 ms total) Tue Jun 16 18:27:38 2026: Iterated ≈82% of D-proof candidates. [56340848 of 68708352] (ETC: Tue Jun 16 18:30:44 2026 ; 3 min 6 s 394.75 ms remaining ; 17 min 15 s 526.31 ms total) Tue Jun 16 18:27:54 2026: Iterated ≈84% of D-proof candidates. [57715015 of 68708352] (ETC: Tue Jun 16 18:30:39 2026 ; 2 min 44 s 869.25 ms remaining ; 17 min 10 s 432.76 ms total) Tue Jun 16 18:28:09 2026: Iterated ≈86% of D-proof candidates. [59089182 of 68708352] (ETC: Tue Jun 16 18:30:32 2026 ; 2 min 23 s 330.12 ms remaining ; 17 min 3 s 786.48 ms total) Tue Jun 16 18:28:25 2026: Iterated ≈88% of D-proof candidates. [60463349 of 68708352] (ETC: Tue Jun 16 18:30:27 2026 ; 2 min 2 s 197.96 ms remaining ; 16 min 58 s 316.21 ms total) Tue Jun 16 18:28:42 2026: Iterated ≈90% of D-proof candidates. [61837516 of 68708352] (ETC: Tue Jun 16 18:30:23 2026 ; 1 min 41 s 432.15 ms remaining ; 16 min 54 s 321.36 ms total) Tue Jun 16 18:28:57 2026: Iterated ≈92% of D-proof candidates. [63211683 of 68708352] (ETC: Tue Jun 16 18:30:18 2026 ; 1 min 20 s 725.07 ms remaining ; 16 min 49 s 63.16 ms total) Tue Jun 16 18:29:14 2026: Iterated ≈94% of D-proof candidates. [64585850 of 68708352] (ETC: Tue Jun 16 18:30:15 2026 ; 1 min 351.46 ms remaining ; 16 min 45 s 857.54 ms total) Tue Jun 16 18:29:33 2026: Iterated ≈96% of D-proof candidates. [65960017 of 68708352] (ETC: Tue Jun 16 18:30:13 2026 ; 40 s 180.40 ms remaining ; 16 min 44 s 509.55 ms total) Tue Jun 16 18:29:48 2026: Iterated ≈98% of D-proof candidates. [67334184 of 68708352] (ETC: Tue Jun 16 18:30:07 2026 ; 19 s 976.01 ms remaining ; 16 min 38 s 800.00 ms total) Tue Jun 16 18:30:04 2026: Iterated 100% of D-proof candidates. [68708352 of 68708352] (ETC: Tue Jun 16 18:30:04 2026 ; 0.00 ms remaining ; 16 min 35 s 553.94 ms total) 995542.95 ms (16 min 35 s 542.95 ms) taken to collect 130757 D-proofs of length 149. [iterated 68708352 condensed detachment proof strings] Tue Jun 16 18:30:07 2026: Removed ≈ 2% of redundant conclusions. [ 2563 of approximately 128164] (ETC: Tue Jun 16 18:32:08 2026 ; 2 min 1 s 344.43 ms remaining ; 2 min 3 s 820.58 ms total) Tue Jun 16 18:30:09 2026: Removed ≈ 4% of redundant conclusions. [ 5126 of approximately 128164] (ETC: Tue Jun 16 18:31:59 2026 ; 1 min 50 s 178.82 ms remaining ; 1 min 54 s 769.09 ms total) Tue Jun 16 18:30:11 2026: Removed ≈ 6% of redundant conclusions. [ 7689 of approximately 128164] (ETC: Tue Jun 16 18:31:54 2026 ; 1 min 43 s 308.24 ms remaining ; 1 min 49 s 901.62 ms total) Tue Jun 16 18:30:13 2026: Removed ≈ 8% of redundant conclusions. [ 10253 of approximately 128164] (ETC: Tue Jun 16 18:31:52 2026 ; 1 min 39 s 171.43 ms remaining ; 1 min 47 s 794.92 ms total) Tue Jun 16 18:30:15 2026: Removed ≈ 10% of redundant conclusions. [ 12816 of approximately 128164] (ETC: Tue Jun 16 18:31:54 2026 ; 1 min 38 s 910.08 ms remaining ; 1 min 49 s 899.71 ms total) Tue Jun 16 18:30:18 2026: Removed ≈ 12% of redundant conclusions. [ 15379 of approximately 128164] (ETC: Tue Jun 16 18:31:55 2026 ; 1 min 37 s 602.48 ms remaining ; 1 min 50 s 911.25 ms total) Tue Jun 16 18:30:20 2026: Removed ≈ 14% of redundant conclusions. [ 17942 of approximately 128164] (ETC: Tue Jun 16 18:31:59 2026 ; 1 min 38 s 328.17 ms remaining ; 1 min 54 s 334.08 ms total) Tue Jun 16 18:30:23 2026: Removed ≈ 16% of redundant conclusions. [ 20506 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 36 s 911.39 ms remaining ; 1 min 55 s 370.44 ms total) Tue Jun 16 18:30:25 2026: Removed ≈ 18% of redundant conclusions. [ 23069 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 35 s 210.06 ms remaining ; 1 min 56 s 109.26 ms total) Tue Jun 16 18:30:27 2026: Removed ≈ 20% of redundant conclusions. [ 25632 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 32 s 904.94 ms remaining ; 1 min 56 s 130.26 ms total) Tue Jun 16 18:30:30 2026: Removed ≈ 22% of redundant conclusions. [ 28196 of approximately 128164] (ETC: Tue Jun 16 18:32:01 2026 ; 1 min 30 s 733.70 ms remaining ; 1 min 56 s 325.16 ms total) Tue Jun 16 18:30:32 2026: Removed ≈ 24% of redundant conclusions. [ 30759 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 28 s 305.74 ms remaining ; 1 min 56 s 191.34 ms total) Tue Jun 16 18:30:34 2026: Removed ≈ 26% of redundant conclusions. [ 33322 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 25 s 949.61 ms remaining ; 1 min 56 s 147.33 ms total) Tue Jun 16 18:30:37 2026: Removed ≈ 28% of redundant conclusions. [ 35885 of approximately 128164] (ETC: Tue Jun 16 18:32:00 2026 ; 1 min 23 s 471.17 ms remaining ; 1 min 55 s 931.03 ms total) Tue Jun 16 18:30:39 2026: Removed ≈ 30% of redundant conclusions. [ 38449 of approximately 128164] (ETC: Tue Jun 16 18:32:01 2026 ; 1 min 21 s 657.94 ms remaining ; 1 min 56 s 653.94 ms total) Tue Jun 16 18:30:42 2026: Removed ≈ 32% of redundant conclusions. [ 41012 of approximately 128164] (ETC: Tue Jun 16 18:32:01 2026 ; 1 min 19 s 565.92 ms remaining ; 1 min 57 s 8.06 ms total) Tue Jun 16 18:30:44 2026: Removed ≈ 34% of redundant conclusions. [ 43575 of approximately 128164] (ETC: Tue Jun 16 18:32:02 2026 ; 1 min 17 s 412.82 ms remaining ; 1 min 57 s 291.10 ms total) Tue Jun 16 18:30:47 2026: Removed ≈ 36% of redundant conclusions. [ 46139 of approximately 128164] (ETC: Tue Jun 16 18:32:02 2026 ; 1 min 15 s 339.52 ms remaining ; 1 min 57 s 717.94 ms total) Tue Jun 16 18:30:49 2026: Removed ≈ 38% of redundant conclusions. [ 48702 of approximately 128164] (ETC: Tue Jun 16 18:32:02 2026 ; 1 min 13 s 269.39 ms remaining ; 1 min 58 s 175.96 ms total) Tue Jun 16 18:30:52 2026: Removed ≈ 40% of redundant conclusions. [ 51265 of approximately 128164] (ETC: Tue Jun 16 18:32:03 2026 ; 1 min 11 s 529.99 ms remaining ; 1 min 59 s 215.71 ms total) Tue Jun 16 18:30:54 2026: Removed ≈ 42% of redundant conclusions. [ 53828 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 1 min 9 s 309.01 ms remaining ; 1 min 59 s 496.88 ms total) Tue Jun 16 18:30:57 2026: Removed ≈ 44% of redundant conclusions. [ 56392 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 1 min 7 s 116.36 ms remaining ; 1 min 59 s 850.38 ms total) Tue Jun 16 18:31:00 2026: Removed ≈ 46% of redundant conclusions. [ 58955 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 1 min 4 s 857.43 ms remaining ; 2 min 105.59 ms total) Tue Jun 16 18:31:02 2026: Removed ≈ 48% of redundant conclusions. [ 61518 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 1 min 2 s 543.65 ms remaining ; 2 min 274.95 ms total) Tue Jun 16 18:31:04 2026: Removed ≈ 50% of redundant conclusions. [ 64082 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 1 min 209.44 ms remaining ; 2 min 418.89 ms total) Tue Jun 16 18:31:07 2026: Removed ≈ 52% of redundant conclusions. [ 66645 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 57 s 845.66 ms remaining ; 2 min 511.24 ms total) Tue Jun 16 18:31:09 2026: Removed ≈ 54% of redundant conclusions. [ 69208 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 55 s 449.48 ms remaining ; 2 min 541.20 ms total) Tue Jun 16 18:31:12 2026: Removed ≈ 56% of redundant conclusions. [ 71771 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 52 s 941.15 ms remaining ; 2 min 319.00 ms total) Tue Jun 16 18:31:14 2026: Removed ≈ 58% of redundant conclusions. [ 74335 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 50 s 292.28 ms remaining ; 1 min 59 s 743.25 ms total) Tue Jun 16 18:31:16 2026: Removed ≈ 60% of redundant conclusions. [ 76898 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 47 s 818.69 ms remaining ; 1 min 59 s 545.79 ms total) Tue Jun 16 18:31:19 2026: Removed ≈ 62% of redundant conclusions. [ 79461 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 45 s 515.37 ms remaining ; 1 min 59 s 775.62 ms total) Tue Jun 16 18:31:21 2026: Removed ≈ 64% of redundant conclusions. [ 82024 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 43 s 184.19 ms remaining ; 1 min 59 s 953.58 ms total) Tue Jun 16 18:31:24 2026: Removed ≈ 66% of redundant conclusions. [ 84588 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 40 s 916.01 ms remaining ; 2 min 340.56 ms total) Tue Jun 16 18:31:26 2026: Removed ≈ 68% of redundant conclusions. [ 87151 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 38 s 461.74 ms remaining ; 2 min 191.41 ms total) Tue Jun 16 18:31:29 2026: Removed ≈ 70% of redundant conclusions. [ 89714 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 36 s 153.57 ms remaining ; 2 min 509.39 ms total) Tue Jun 16 18:31:31 2026: Removed ≈ 72% of redundant conclusions. [ 92278 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 33 s 717.92 ms remaining ; 2 min 420.88 ms total) Tue Jun 16 18:31:33 2026: Removed ≈ 74% of redundant conclusions. [ 94841 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 31 s 328.03 ms remaining ; 2 min 491.13 ms total) Tue Jun 16 18:31:36 2026: Removed ≈ 76% of redundant conclusions. [ 97404 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 28 s 879.18 ms remaining ; 2 min 327.41 ms total) Tue Jun 16 18:31:38 2026: Removed ≈ 78% of redundant conclusions. [ 99967 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 26 s 481.60 ms remaining ; 2 min 366.97 ms total) Tue Jun 16 18:31:41 2026: Removed ≈ 80% of redundant conclusions. [102531 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 24 s 103.36 ms remaining ; 2 min 515.88 ms total) Tue Jun 16 18:31:43 2026: Removed ≈ 82% of redundant conclusions. [105094 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 21 s 731.97 ms remaining ; 2 min 730.63 ms total) Tue Jun 16 18:31:46 2026: Removed ≈ 84% of redundant conclusions. [107657 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 19 s 303.48 ms remaining ; 2 min 642.28 ms total) Tue Jun 16 18:31:48 2026: Removed ≈ 86% of redundant conclusions. [110221 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 16 s 872.80 ms remaining ; 2 min 519.73 ms total) Tue Jun 16 18:31:50 2026: Removed ≈ 88% of redundant conclusions. [112784 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 14 s 432.94 ms remaining ; 2 min 271.99 ms total) Tue Jun 16 18:31:53 2026: Removed ≈ 90% of redundant conclusions. [115347 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 12 s 41.76 ms remaining ; 2 min 411.96 ms total) Tue Jun 16 18:31:55 2026: Removed ≈ 92% of redundant conclusions. [117910 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 9 s 620.93 ms remaining ; 2 min 251.25 ms total) Tue Jun 16 18:31:57 2026: Removed ≈ 94% of redundant conclusions. [120474 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 7 s 218.89 ms remaining ; 2 min 312.36 ms total) Tue Jun 16 18:32:00 2026: Removed ≈ 96% of redundant conclusions. [123037 of approximately 128164] (ETC: Tue Jun 16 18:32:05 2026 ; 4 s 811.75 ms remaining ; 2 min 283.35 ms total) Tue Jun 16 18:32:02 2026: Removed ≈ 98% of redundant conclusions. [125600 of approximately 128164] (ETC: Tue Jun 16 18:32:04 2026 ; 2 s 400.97 ms remaining ; 2 min 14.70 ms total) 120950.66 ms (2 min 950.65 ms) taken to detect 127004 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 } } 18.93 ms taken to filter and order new representative proofs. Found 3753 representative, 38985899 redundant, and 29718700 invalid condensed detachment proof strings. lengths up to 149 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753)} ; 3753 new representative proofs (38985899 redundant, 29718700 invalid) Tue Jun 16 18:32:05 2026: Starting to write 3753 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs149.txt. 4.01 ms taken to print and save 659975 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs149.txt. Determined the number of proof string candidates for iteration as 73843459. [most relevant: {41,109} with 2*4074744 = 8149488, i.e. ≈11.04%] Estimated removal count set to 133973, based on entry 149:127004 and last known pair (147:120397, 149:127004) with 127004/120397 ≈ 1.05488 and 127004 * (127004/120397)^1 ≈ 133973.57. Tue Jun 16 18:32:05 2026: Starting to generate D-proof representatives of length 151. Tue Jun 16 18:32:23 2026: Iterated ≈ 2% of D-proof candidates. [ 1476869 of 73843459] (ETC: Tue Jun 16 18:46:39 2026 ; 14 min 16 s 128.06 ms remaining ; 14 min 33 s 600.06 ms total) Tue Jun 16 18:32:45 2026: Iterated ≈ 4% of D-proof candidates. [ 2953738 of 73843459] (ETC: Tue Jun 16 18:48:34 2026 ; 15 min 49 s 638.43 ms remaining ; 16 min 29 s 206.69 ms total) Tue Jun 16 18:33:07 2026: Iterated ≈ 6% of D-proof candidates. [ 4430607 of 73843459] (ETC: Tue Jun 16 18:49:12 2026 ; 16 min 5 s 121.98 ms remaining ; 17 min 6 s 725.51 ms total) Tue Jun 16 18:33:29 2026: Iterated ≈ 8% of D-proof candidates. [ 5907476 of 73843459] (ETC: Tue Jun 16 18:49:37 2026 ; 16 min 7 s 975.99 ms remaining ; 17 min 32 s 147.80 ms total) Tue Jun 16 18:33:51 2026: Iterated ≈10% of D-proof candidates. [ 7384345 of 73843459] (ETC: Tue Jun 16 18:49:44 2026 ; 15 min 53 s 190.64 ms remaining ; 17 min 39 s 100.70 ms total) Tue Jun 16 18:34:13 2026: Iterated ≈12% of D-proof candidates. [ 8861215 of 73843459] (ETC: Tue Jun 16 18:49:49 2026 ; 15 min 36 s 432.23 ms remaining ; 17 min 44 s 127.53 ms total) Tue Jun 16 18:34:39 2026: Iterated ≈14% of D-proof candidates. [10338084 of 73843459] (ETC: Tue Jun 16 18:50:21 2026 ; 15 min 42 s 251.49 ms remaining ; 18 min 15 s 641.26 ms total) Tue Jun 16 18:35:04 2026: Iterated ≈16% of D-proof candidates. [11814953 of 73843459] (ETC: Tue Jun 16 18:50:45 2026 ; 15 min 40 s 901.10 ms remaining ; 18 min 40 s 120.35 ms total) Tue Jun 16 18:35:30 2026: Iterated ≈18% of D-proof candidates. [13291822 of 73843459] (ETC: Tue Jun 16 18:51:03 2026 ; 15 min 33 s 8.42 ms remaining ; 18 min 57 s 815.13 ms total) Tue Jun 16 18:35:52 2026: Iterated ≈20% of D-proof candidates. [14768691 of 73843459] (ETC: Tue Jun 16 18:51:00 2026 ; 15 min 8 s 172.00 ms remaining ; 18 min 55 s 214.99 ms total) Tue Jun 16 18:36:20 2026: Iterated ≈22% of D-proof candidates. [16245560 of 73843459] (ETC: Tue Jun 16 18:51:22 2026 ; 15 min 2 s 330.86 ms remaining ; 19 min 16 s 834.41 ms total) Tue Jun 16 18:36:45 2026: Iterated ≈24% of D-proof candidates. [17722430 of 73843459] (ETC: Tue Jun 16 18:51:31 2026 ; 14 min 46 s 1.69 ms remaining ; 19 min 25 s 791.69 ms total) Tue Jun 16 18:37:09 2026: Iterated ≈26% of D-proof candidates. [19199299 of 73843459] (ETC: Tue Jun 16 18:51:34 2026 ; 14 min 24 s 699.63 ms remaining ; 19 min 28 s 513.01 ms total) Tue Jun 16 18:37:33 2026: Iterated ≈28% of D-proof candidates. [20676168 of 73843459] (ETC: Tue Jun 16 18:51:36 2026 ; 14 min 3 s 62.82 ms remaining ; 19 min 30 s 920.57 ms total) Tue Jun 16 18:37:50 2026: Iterated ≈30% of D-proof candidates. [22153037 of 73843459] (ETC: Tue Jun 16 18:51:15 2026 ; 13 min 25 s 118.42 ms remaining ; 19 min 10 s 169.15 ms total) Tue Jun 16 18:38:15 2026: Iterated ≈32% of D-proof candidates. [23629906 of 73843459] (ETC: Tue Jun 16 18:51:22 2026 ; 13 min 6 s 278.01 ms remaining ; 19 min 16 s 291.18 ms total) Tue Jun 16 18:38:42 2026: Iterated ≈34% of D-proof candidates. [25106776 of 73843459] (ETC: Tue Jun 16 18:51:33 2026 ; 12 min 50 s 452.36 ms remaining ; 19 min 27 s 352.06 ms total) Tue Jun 16 18:39:12 2026: Iterated ≈36% of D-proof candidates. [26583645 of 73843459] (ETC: Tue Jun 16 18:51:50 2026 ; 12 min 38 s 55.81 ms remaining ; 19 min 44 s 462.20 ms total) Tue Jun 16 18:39:41 2026: Iterated ≈38% of D-proof candidates. [28060514 of 73843459] (ETC: Tue Jun 16 18:52:04 2026 ; 12 min 23 s 97.84 ms remaining ; 19 min 58 s 544.89 ms total) Tue Jun 16 18:40:05 2026: Iterated ≈40% of D-proof candidates. [29537383 of 73843459] (ETC: Tue Jun 16 18:52:06 2026 ; 12 min 198.72 ms remaining ; 20 min 331.18 ms total) Tue Jun 16 18:40:33 2026: Iterated ≈42% of D-proof candidates. [31014252 of 73843459] (ETC: Tue Jun 16 18:52:14 2026 ; 11 min 40 s 928.69 ms remaining ; 20 min 8 s 497.72 ms total) Tue Jun 16 18:41:04 2026: Iterated ≈44% of D-proof candidates. [32491121 of 73843459] (ETC: Tue Jun 16 18:52:30 2026 ; 11 min 26 s 95.28 ms remaining ; 20 min 25 s 170.11 ms total) Tue Jun 16 18:41:31 2026: Iterated ≈46% of D-proof candidates. [33967991 of 73843459] (ETC: Tue Jun 16 18:52:35 2026 ; 11 min 4 s 232.13 ms remaining ; 20 min 30 s 59.49 ms total) Tue Jun 16 18:41:53 2026: Iterated ≈48% of D-proof candidates. [35444860 of 73843459] (ETC: Tue Jun 16 18:52:31 2026 ; 10 min 37 s 150.20 ms remaining ; 20 min 25 s 288.84 ms total) Tue Jun 16 18:42:22 2026: Iterated ≈50% of D-proof candidates. [36921729 of 73843459] (ETC: Tue Jun 16 18:52:39 2026 ; 10 min 17 s 7.31 ms remaining ; 20 min 34 s 14.60 ms total) Tue Jun 16 18:42:50 2026: Iterated ≈52% of D-proof candidates. [38398598 of 73843459] (ETC: Tue Jun 16 18:52:45 2026 ; 9 min 55 s 30.98 ms remaining ; 20 min 39 s 647.85 ms total) Tue Jun 16 18:43:18 2026: Iterated ≈54% of D-proof candidates. [39875467 of 73843459] (ETC: Tue Jun 16 18:52:51 2026 ; 9 min 33 s 282.26 ms remaining ; 20 min 46 s 265.75 ms total) Tue Jun 16 18:43:36 2026: Iterated ≈56% of D-proof candidates. [41352337 of 73843459] (ETC: Tue Jun 16 18:52:39 2026 ; 9 min 2 s 941.55 ms remaining ; 20 min 33 s 958.08 ms total) Tue Jun 16 18:43:51 2026: Iterated ≈58% of D-proof candidates. [42829206 of 73843459] (ETC: Tue Jun 16 18:52:22 2026 ; 8 min 31 s 104.79 ms remaining ; 20 min 16 s 916.16 ms total) Tue Jun 16 18:44:05 2026: Iterated ≈60% of D-proof candidates. [44306075 of 73843459] (ETC: Tue Jun 16 18:52:05 2026 ; 7 min 59 s 932.13 ms remaining ; 19 min 59 s 830.30 ms total) Tue Jun 16 18:44:21 2026: Iterated ≈62% of D-proof candidates. [45782944 of 73843459] (ETC: Tue Jun 16 18:51:51 2026 ; 7 min 30 s 719.28 ms remaining ; 19 min 46 s 103.34 ms total) Tue Jun 16 18:44:35 2026: Iterated ≈64% of D-proof candidates. [47259813 of 73843459] (ETC: Tue Jun 16 18:51:36 2026 ; 7 min 1 s 549.82 ms remaining ; 19 min 30 s 971.68 ms total) Tue Jun 16 18:44:46 2026: Iterated ≈66% of D-proof candidates. [48736682 of 73843459] (ETC: Tue Jun 16 18:51:18 2026 ; 6 min 31 s 932.20 ms remaining ; 19 min 12 s 741.71 ms total) Tue Jun 16 18:45:01 2026: Iterated ≈68% of D-proof candidates. [50213552 of 73843459] (ETC: Tue Jun 16 18:51:06 2026 ; 6 min 5 s 142.77 ms remaining ; 19 min 1 s 71.15 ms total) Tue Jun 16 18:45:14 2026: Iterated ≈70% of D-proof candidates. [51690421 of 73843459] (ETC: Tue Jun 16 18:50:52 2026 ; 5 min 38 s 171.63 ms remaining ; 18 min 47 s 238.77 ms total) Tue Jun 16 18:45:32 2026: Iterated ≈72% of D-proof candidates. [53167290 of 73843459] (ETC: Tue Jun 16 18:50:45 2026 ; 5 min 13 s 558.05 ms remaining ; 18 min 39 s 850.17 ms total) Tue Jun 16 18:45:48 2026: Iterated ≈74% of D-proof candidates. [54644159 of 73843459] (ETC: Tue Jun 16 18:50:36 2026 ; 4 min 48 s 925.02 ms remaining ; 18 min 31 s 250.06 ms total) Tue Jun 16 18:46:02 2026: Iterated ≈76% of D-proof candidates. [56121028 of 73843459] (ETC: Tue Jun 16 18:50:26 2026 ; 4 min 24 s 129.44 ms remaining ; 18 min 20 s 539.28 ms total) Tue Jun 16 18:46:15 2026: Iterated ≈78% of D-proof candidates. [57597898 of 73843459] (ETC: Tue Jun 16 18:50:15 2026 ; 3 min 59 s 775.92 ms remaining ; 18 min 9 s 890.54 ms total) Tue Jun 16 18:46:28 2026: Iterated ≈80% of D-proof candidates. [59074767 of 73843459] (ETC: Tue Jun 16 18:50:04 2026 ; 3 min 35 s 816.60 ms remaining ; 17 min 59 s 82.97 ms total) Tue Jun 16 18:46:46 2026: Iterated ≈82% of D-proof candidates. [60551636 of 73843459] (ETC: Tue Jun 16 18:49:59 2026 ; 3 min 13 s 329.09 ms remaining ; 17 min 54 s 50.46 ms total) Tue Jun 16 18:47:02 2026: Iterated ≈84% of D-proof candidates. [62028505 of 73843459] (ETC: Tue Jun 16 18:49:53 2026 ; 2 min 50 s 867.12 ms remaining ; 17 min 47 s 919.42 ms total) Tue Jun 16 18:47:17 2026: Iterated ≈86% of D-proof candidates. [63505374 of 73843459] (ETC: Tue Jun 16 18:49:46 2026 ; 2 min 28 s 501.62 ms remaining ; 17 min 40 s 725.80 ms total) Tue Jun 16 18:47:32 2026: Iterated ≈88% of D-proof candidates. [64982243 of 73843459] (ETC: Tue Jun 16 18:49:39 2026 ; 2 min 6 s 413.20 ms remaining ; 17 min 33 s 443.22 ms total) Tue Jun 16 18:47:46 2026: Iterated ≈90% of D-proof candidates. [66459113 of 73843459] (ETC: Tue Jun 16 18:49:30 2026 ; 1 min 44 s 497.87 ms remaining ; 17 min 24 s 978.66 ms total) Tue Jun 16 18:48:05 2026: Iterated ≈92% of D-proof candidates. [67935982 of 73843459] (ETC: Tue Jun 16 18:49:28 2026 ; 1 min 23 s 454.17 ms remaining ; 17 min 23 s 177.06 ms total) Tue Jun 16 18:48:21 2026: Iterated ≈94% of D-proof candidates. [69412851 of 73843459] (ETC: Tue Jun 16 18:49:24 2026 ; 1 min 2 s 297.87 ms remaining ; 17 min 18 s 297.69 ms total) Tue Jun 16 18:48:36 2026: Iterated ≈96% of D-proof candidates. [70889720 of 73843459] (ETC: Tue Jun 16 18:49:17 2026 ; 41 s 265.16 ms remaining ; 17 min 11 s 628.81 ms total) Tue Jun 16 18:48:48 2026: Iterated ≈98% of D-proof candidates. [72366589 of 73843459] (ETC: Tue Jun 16 18:49:09 2026 ; 20 s 472.12 ms remaining ; 17 min 3 s 605.50 ms total) Tue Jun 16 18:49:03 2026: Iterated 100% of D-proof candidates. [73843459 of 73843459] (ETC: Tue Jun 16 18:49:03 2026 ; 0.00 ms remaining ; 16 min 58 s 199.24 ms total) 1018189.24 ms (16 min 58 s 189.24 ms) taken to collect 138919 D-proofs of length 151. [iterated 73843459 condensed detachment proof strings] Tue Jun 16 18:49:06 2026: Removed ≈ 2% of redundant conclusions. [ 2679 of approximately 133973] (ETC: Tue Jun 16 18:51:13 2026 ; 2 min 6 s 841.47 ms remaining ; 2 min 9 s 429.62 ms total) Tue Jun 16 18:49:09 2026: Removed ≈ 4% of redundant conclusions. [ 5358 of approximately 133973] (ETC: Tue Jun 16 18:51:17 2026 ; 2 min 8 s 598.34 ms remaining ; 2 min 13 s 955.65 ms total) Tue Jun 16 18:49:11 2026: Removed ≈ 6% of redundant conclusions. [ 8038 of approximately 133973] (ETC: Tue Jun 16 18:51:17 2026 ; 2 min 5 s 691.50 ms remaining ; 2 min 13 s 713.95 ms total) Tue Jun 16 18:49:14 2026: Removed ≈ 8% of redundant conclusions. [ 10717 of approximately 133973] (ETC: Tue Jun 16 18:51:18 2026 ; 2 min 3 s 746.11 ms remaining ; 2 min 14 s 505.73 ms total) Tue Jun 16 18:49:17 2026: Removed ≈ 10% of redundant conclusions. [ 13397 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 2 min 3 s 562.14 ms remaining ; 2 min 17 s 290.92 ms total) Tue Jun 16 18:49:20 2026: Removed ≈ 12% of redundant conclusions. [ 16076 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 2 min 147.99 ms remaining ; 2 min 16 s 530.93 ms total) Tue Jun 16 18:49:23 2026: Removed ≈ 14% of redundant conclusions. [ 18756 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 58 s 252.23 ms remaining ; 2 min 17 s 502.33 ms total) Tue Jun 16 18:49:26 2026: Removed ≈ 16% of redundant conclusions. [ 21435 of approximately 133973] (ETC: Tue Jun 16 18:51:22 2026 ; 1 min 56 s 41.27 ms remaining ; 2 min 18 s 143.53 ms total) Tue Jun 16 18:49:28 2026: Removed ≈ 18% of redundant conclusions. [ 24115 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 52 s 579.57 ms remaining ; 2 min 17 s 291.98 ms total) Tue Jun 16 18:49:31 2026: Removed ≈ 20% of redundant conclusions. [ 26794 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 49 s 561.33 ms remaining ; 2 min 16 s 950.90 ms total) Tue Jun 16 18:49:33 2026: Removed ≈ 22% of redundant conclusions. [ 29474 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 46 s 479.91 ms remaining ; 2 min 16 s 512.63 ms total) Tue Jun 16 18:49:36 2026: Removed ≈ 24% of redundant conclusions. [ 32153 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 44 s 140.84 ms remaining ; 2 min 17 s 26.72 ms total) Tue Jun 16 18:49:39 2026: Removed ≈ 26% of redundant conclusions. [ 34832 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 41 s 161.94 ms remaining ; 2 min 16 s 703.97 ms total) Tue Jun 16 18:49:42 2026: Removed ≈ 28% of redundant conclusions. [ 37512 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 38 s 130.35 ms remaining ; 2 min 16 s 291.53 ms total) Tue Jun 16 18:49:44 2026: Removed ≈ 30% of redundant conclusions. [ 40191 of approximately 133973] (ETC: Tue Jun 16 18:51:19 2026 ; 1 min 35 s 203.82 ms remaining ; 2 min 16 s 4.16 ms total) Tue Jun 16 18:49:47 2026: Removed ≈ 32% of redundant conclusions. [ 42871 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 32 s 654.32 ms remaining ; 2 min 16 s 255.81 ms total) Tue Jun 16 18:49:50 2026: Removed ≈ 34% of redundant conclusions. [ 45550 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 30 s 466.46 ms remaining ; 2 min 17 s 69.13 ms total) Tue Jun 16 18:49:53 2026: Removed ≈ 36% of redundant conclusions. [ 48230 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 27 s 813.82 ms remaining ; 2 min 17 s 208.64 ms total) Tue Jun 16 18:49:56 2026: Removed ≈ 38% of redundant conclusions. [ 50909 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 25 s 57.81 ms remaining ; 2 min 17 s 188.79 ms total) Tue Jun 16 18:49:58 2026: Removed ≈ 40% of redundant conclusions. [ 53589 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 22 s 200.71 ms remaining ; 2 min 17 s 0.85 ms total) Tue Jun 16 18:50:01 2026: Removed ≈ 42% of redundant conclusions. [ 56268 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 19 s 613.92 ms remaining ; 2 min 17 s 264.22 ms total) Tue Jun 16 18:50:04 2026: Removed ≈ 44% of redundant conclusions. [ 58948 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 16 s 831.58 ms remaining ; 2 min 17 s 199.03 ms total) Tue Jun 16 18:50:06 2026: Removed ≈ 46% of redundant conclusions. [ 61627 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 13 s 794.16 ms remaining ; 2 min 16 s 654.75 ms total) Tue Jun 16 18:50:09 2026: Removed ≈ 48% of redundant conclusions. [ 64307 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 10 s 885.56 ms remaining ; 2 min 16 s 318.30 ms total) Tue Jun 16 18:50:12 2026: Removed ≈ 50% of redundant conclusions. [ 66986 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 8 s 408.93 ms remaining ; 2 min 16 s 816.85 ms total) Tue Jun 16 18:50:15 2026: Removed ≈ 52% of redundant conclusions. [ 69665 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 1 min 5 s 725.03 ms remaining ; 2 min 16 s 925.10 ms total) Tue Jun 16 18:50:17 2026: Removed ≈ 54% of redundant conclusions. [ 72345 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 3 s 73.81 ms remaining ; 2 min 17 s 116.05 ms total) Tue Jun 16 18:50:20 2026: Removed ≈ 56% of redundant conclusions. [ 75024 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 1 min 355.77 ms remaining ; 2 min 17 s 170.17 ms total) Tue Jun 16 18:50:23 2026: Removed ≈ 58% of redundant conclusions. [ 77704 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 57 s 600.38 ms remaining ; 2 min 17 s 142.93 ms total) Tue Jun 16 18:50:26 2026: Removed ≈ 60% of redundant conclusions. [ 80383 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 54 s 869.17 ms remaining ; 2 min 17 s 170.88 ms total) Tue Jun 16 18:50:28 2026: Removed ≈ 62% of redundant conclusions. [ 83063 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 52 s 59.12 ms remaining ; 2 min 16 s 996.97 ms total) Tue Jun 16 18:50:31 2026: Removed ≈ 64% of redundant conclusions. [ 85742 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 49 s 128.21 ms remaining ; 2 min 16 s 465.20 ms total) Tue Jun 16 18:50:34 2026: Removed ≈ 66% of redundant conclusions. [ 88422 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 46 s 473.21 ms remaining ; 2 min 16 s 685.37 ms total) Tue Jun 16 18:50:36 2026: Removed ≈ 68% of redundant conclusions. [ 91101 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 43 s 786.05 ms remaining ; 2 min 16 s 829.37 ms total) Tue Jun 16 18:50:39 2026: Removed ≈ 70% of redundant conclusions. [ 93781 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 41 s 89.64 ms remaining ; 2 min 16 s 965.12 ms total) Tue Jun 16 18:50:42 2026: Removed ≈ 72% of redundant conclusions. [ 96460 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 38 s 390.21 ms remaining ; 2 min 17 s 105.86 ms total) Tue Jun 16 18:50:45 2026: Removed ≈ 74% of redundant conclusions. [ 99140 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 35 s 686.37 ms remaining ; 2 min 17 s 255.17 ms total) Tue Jun 16 18:50:48 2026: Removed ≈ 76% of redundant conclusions. [101819 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 32 s 898.63 ms remaining ; 2 min 17 s 75.59 ms total) Tue Jun 16 18:50:50 2026: Removed ≈ 78% of redundant conclusions. [104498 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 30 s 142.96 ms remaining ; 2 min 17 s 9.07 ms total) Tue Jun 16 18:50:53 2026: Removed ≈ 80% of redundant conclusions. [107178 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 27 s 443.83 ms remaining ; 2 min 17 s 217.11 ms total) Tue Jun 16 18:50:56 2026: Removed ≈ 82% of redundant conclusions. [109857 of approximately 133973] (ETC: Tue Jun 16 18:51:21 2026 ; 24 s 702.44 ms remaining ; 2 min 17 s 230.87 ms total) Tue Jun 16 18:50:58 2026: Removed ≈ 84% of redundant conclusions. [112537 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 21 s 868.50 ms remaining ; 2 min 16 s 676.06 ms total) Tue Jun 16 18:51:01 2026: Removed ≈ 86% of redundant conclusions. [115216 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 19 s 150.11 ms remaining ; 2 min 16 s 780.84 ms total) Tue Jun 16 18:51:04 2026: Removed ≈ 88% of redundant conclusions. [117896 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 16 s 399.90 ms remaining ; 2 min 16 s 663.78 ms total) Tue Jun 16 18:51:06 2026: Removed ≈ 90% of redundant conclusions. [120575 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 13 s 649.46 ms remaining ; 2 min 16 s 487.49 ms total) Tue Jun 16 18:51:09 2026: Removed ≈ 92% of redundant conclusions. [123255 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 10 s 921.15 ms remaining ; 2 min 16 s 512.33 ms total) Tue Jun 16 18:51:12 2026: Removed ≈ 94% of redundant conclusions. [125934 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 8 s 206.21 ms remaining ; 2 min 16 s 759.56 ms total) Tue Jun 16 18:51:15 2026: Removed ≈ 96% of redundant conclusions. [128614 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 5 s 464.61 ms remaining ; 2 min 16 s 613.11 ms total) Tue Jun 16 18:51:17 2026: Removed ≈ 98% of redundant conclusions. [131293 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 2 s 732.78 ms remaining ; 2 min 16 s 611.44 ms total) Tue Jun 16 18:51:20 2026: Removed ≈100% of redundant conclusions. [133973 of approximately 133973] (ETC: Tue Jun 16 18:51:20 2026 ; 0.00 ms remaining ; 2 min 16 s 551.81 ms total) 137305.12 ms (2 min 17 s 305.12 ms) taken to detect 134627 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 }, { 151, 134627 } } 22.73 ms taken to filter and order new representative proofs. Found 4292 representative, 41821212 redundant, and 32017955 invalid condensed detachment proof strings. lengths up to 151 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753), (151,4292)} ; 4292 new representative proofs (41821212 redundant, 32017955 invalid) Tue Jun 16 18:51:21 2026: Starting to write 4292 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs151.txt. 3.95 ms taken to print and save 763456 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs151.txt. Determined the number of proof string candidates for iteration as 79078166. [most relevant: {41,111} with 2*4278360 = 8556720, i.e. ≈10.82%] Estimated removal count set to 142707, based on entry 151:134627 and last known pair (149:127004, 151:134627) with 134627/127004 ≈ 1.06002 and 134627 * (134627/127004)^1 ≈ 142707.55. Tue Jun 16 18:51:21 2026: Starting to generate D-proof representatives of length 153. Tue Jun 16 18:51:40 2026: Iterated ≈ 2% of D-proof candidates. [ 1581563 of 79078166] (ETC: Tue Jun 16 19:07:12 2026 ; 15 min 31 s 984.46 ms remaining ; 15 min 51 s 4.54 ms total) Tue Jun 16 18:52:00 2026: Iterated ≈ 4% of D-proof candidates. [ 3163126 of 79078166] (ETC: Tue Jun 16 19:07:54 2026 ; 15 min 53 s 334.73 ms remaining ; 16 min 33 s 57.00 ms total) Tue Jun 16 18:52:27 2026: Iterated ≈ 6% of D-proof candidates. [ 4744689 of 79078166] (ETC: Tue Jun 16 19:09:39 2026 ; 17 min 12 s 696.28 ms remaining ; 18 min 18 s 613.05 ms total) Tue Jun 16 18:52:50 2026: Iterated ≈ 8% of D-proof candidates. [ 6326253 of 79078166] (ETC: Tue Jun 16 19:09:51 2026 ; 17 min 1 s 16.95 ms remaining ; 18 min 29 s 801.02 ms total) Tue Jun 16 18:53:16 2026: Iterated ≈10% of D-proof candidates. [ 7907816 of 79078166] (ETC: Tue Jun 16 19:10:34 2026 ; 17 min 17 s 579.43 ms remaining ; 19 min 12 s 866.03 ms total) Tue Jun 16 18:53:39 2026: Iterated ≈12% of D-proof candidates. [ 9489379 of 79078166] (ETC: Tue Jun 16 19:10:34 2026 ; 16 min 54 s 749.48 ms remaining ; 19 min 13 s 124.39 ms total) Tue Jun 16 18:54:07 2026: Iterated ≈14% of D-proof candidates. [11070943 of 79078166] (ETC: Tue Jun 16 19:11:08 2026 ; 17 min 1 s 118.00 ms remaining ; 19 min 47 s 346.50 ms total) Tue Jun 16 18:54:38 2026: Iterated ≈16% of D-proof candidates. [12652506 of 79078166] (ETC: Tue Jun 16 19:11:55 2026 ; 17 min 17 s 86.62 ms remaining ; 20 min 34 s 626.92 ms total) Tue Jun 16 18:55:08 2026: Iterated ≈18% of D-proof candidates. [14234069 of 79078166] (ETC: Tue Jun 16 19:12:22 2026 ; 17 min 14 s 10.88 ms remaining ; 21 min 988.87 ms total) Tue Jun 16 18:55:37 2026: Iterated ≈20% of D-proof candidates. [15815633 of 79078166] (ETC: Tue Jun 16 19:12:44 2026 ; 17 min 6 s 446.72 ms remaining ; 21 min 23 s 58.40 ms total) Tue Jun 16 18:56:08 2026: Iterated ≈22% of D-proof candidates. [17397196 of 79078166] (ETC: Tue Jun 16 19:13:06 2026 ; 16 min 57 s 944.08 ms remaining ; 21 min 45 s 56.50 ms total) Tue Jun 16 18:56:39 2026: Iterated ≈24% of D-proof candidates. [18978759 of 79078166] (ETC: Tue Jun 16 19:13:26 2026 ; 16 min 47 s 269.84 ms remaining ; 22 min 5 s 355.03 ms total) Tue Jun 16 18:57:17 2026: Iterated ≈26% of D-proof candidates. [20560323 of 79078166] (ETC: Tue Jun 16 19:14:11 2026 ; 16 min 53 s 980.39 ms remaining ; 22 min 50 s 243.77 ms total) Tue Jun 16 18:57:50 2026: Iterated ≈28% of D-proof candidates. [22141886 of 79078166] (ETC: Tue Jun 16 19:14:30 2026 ; 16 min 40 s 209.24 ms remaining ; 23 min 9 s 179.48 ms total) Tue Jun 16 18:58:20 2026: Iterated ≈30% of D-proof candidates. [23723449 of 79078166] (ETC: Tue Jun 16 19:14:39 2026 ; 16 min 18 s 730.69 ms remaining ; 23 min 18 s 186.68 ms total) Tue Jun 16 18:58:51 2026: Iterated ≈32% of D-proof candidates. [25305013 of 79078166] (ETC: Tue Jun 16 19:14:47 2026 ; 15 min 56 s 113.44 ms remaining ; 23 min 26 s 49.17 ms total) Tue Jun 16 18:59:28 2026: Iterated ≈34% of D-proof candidates. [26886576 of 79078166] (ETC: Tue Jun 16 19:15:14 2026 ; 15 min 46 s 74.84 ms remaining ; 23 min 53 s 446.72 ms total) Tue Jun 16 19:00:06 2026: Iterated ≈36% of D-proof candidates. [28468139 of 79078166] (ETC: Tue Jun 16 19:15:39 2026 ; 15 min 33 s 283.64 ms remaining ; 24 min 18 s 255.67 ms total) Tue Jun 16 19:00:34 2026: Iterated ≈38% of D-proof candidates. [30049703 of 79078166] (ETC: Tue Jun 16 19:15:36 2026 ; 15 min 2 s 34.12 ms remaining ; 24 min 14 s 893.74 ms total) Tue Jun 16 19:01:05 2026: Iterated ≈40% of D-proof candidates. [31631266 of 79078166] (ETC: Tue Jun 16 19:15:41 2026 ; 14 min 36 s 194.13 ms remaining ; 24 min 20 s 323.54 ms total) Tue Jun 16 19:01:36 2026: Iterated ≈42% of D-proof candidates. [33212829 of 79078166] (ETC: Tue Jun 16 19:15:46 2026 ; 14 min 9 s 687.87 ms remaining ; 24 min 24 s 979.06 ms total) Tue Jun 16 19:02:09 2026: Iterated ≈44% of D-proof candidates. [34794393 of 79078166] (ETC: Tue Jun 16 19:15:53 2026 ; 13 min 44 s 569.53 ms remaining ; 24 min 32 s 445.58 ms total) Tue Jun 16 19:02:41 2026: Iterated ≈46% of D-proof candidates. [36375956 of 79078166] (ETC: Tue Jun 16 19:15:59 2026 ; 13 min 18 s 155.10 ms remaining ; 24 min 38 s 64.99 ms total) Tue Jun 16 19:03:09 2026: Iterated ≈48% of D-proof candidates. [37957519 of 79078166] (ETC: Tue Jun 16 19:15:56 2026 ; 12 min 46 s 869.47 ms remaining ; 24 min 34 s 748.96 ms total) Tue Jun 16 19:03:34 2026: Iterated ≈50% of D-proof candidates. [39539083 of 79078166] (ETC: Tue Jun 16 19:15:46 2026 ; 12 min 12 s 761.91 ms remaining ; 24 min 25 s 523.82 ms total) Tue Jun 16 19:03:59 2026: Iterated ≈52% of D-proof candidates. [41120646 of 79078166] (ETC: Tue Jun 16 19:15:39 2026 ; 11 min 39 s 724.96 ms remaining ; 24 min 17 s 760.31 ms total) Tue Jun 16 19:04:16 2026: Iterated ≈54% of D-proof candidates. [42702209 of 79078166] (ETC: Tue Jun 16 19:15:16 2026 ; 11 min 150.56 ms remaining ; 23 min 55 s 109.88 ms total) Tue Jun 16 19:04:34 2026: Iterated ≈56% of D-proof candidates. [44283772 of 79078166] (ETC: Tue Jun 16 19:14:56 2026 ; 10 min 22 s 916.94 ms remaining ; 23 min 35 s 720.29 ms total) Tue Jun 16 19:04:50 2026: Iterated ≈58% of D-proof candidates. [45865336 of 79078166] (ETC: Tue Jun 16 19:14:37 2026 ; 9 min 46 s 284.75 ms remaining ; 23 min 15 s 916.06 ms total) Tue Jun 16 19:05:07 2026: Iterated ≈60% of D-proof candidates. [47446899 of 79078166] (ETC: Tue Jun 16 19:14:17 2026 ; 9 min 10 s 572.17 ms remaining ; 22 min 56 s 430.41 ms total) Tue Jun 16 19:05:22 2026: Iterated ≈62% of D-proof candidates. [49028462 of 79078166] (ETC: Tue Jun 16 19:13:58 2026 ; 8 min 35 s 854.40 ms remaining ; 22 min 37 s 511.54 ms total) Tue Jun 16 19:05:38 2026: Iterated ≈64% of D-proof candidates. [50610026 of 79078166] (ETC: Tue Jun 16 19:13:40 2026 ; 8 min 2 s 284.72 ms remaining ; 22 min 19 s 679.76 ms total) Tue Jun 16 19:05:54 2026: Iterated ≈66% of D-proof candidates. [52191589 of 79078166] (ETC: Tue Jun 16 19:13:24 2026 ; 7 min 29 s 755.07 ms remaining ; 22 min 2 s 809.01 ms total) Tue Jun 16 19:06:10 2026: Iterated ≈68% of D-proof candidates. [53773152 of 79078166] (ETC: Tue Jun 16 19:13:09 2026 ; 6 min 58 s 479.49 ms remaining ; 21 min 47 s 748.35 ms total) Tue Jun 16 19:06:27 2026: Iterated ≈70% of D-proof candidates. [55354716 of 79078166] (ETC: Tue Jun 16 19:12:56 2026 ; 6 min 28 s 469.08 ms remaining ; 21 min 34 s 896.92 ms total) Tue Jun 16 19:06:42 2026: Iterated ≈72% of D-proof candidates. [56936279 of 79078166] (ETC: Tue Jun 16 19:12:40 2026 ; 5 min 58 s 266.11 ms remaining ; 21 min 19 s 521.81 ms total) Tue Jun 16 19:06:58 2026: Iterated ≈74% of D-proof candidates. [58517842 of 79078166] (ETC: Tue Jun 16 19:12:28 2026 ; 5 min 29 s 380.88 ms remaining ; 21 min 6 s 849.50 ms total) Tue Jun 16 19:07:13 2026: Iterated ≈76% of D-proof candidates. [60099406 of 79078166] (ETC: Tue Jun 16 19:12:14 2026 ; 5 min 751.73 ms remaining ; 20 min 53 s 132.20 ms total) Tue Jun 16 19:07:30 2026: Iterated ≈78% of D-proof candidates. [61680969 of 79078166] (ETC: Tue Jun 16 19:12:04 2026 ; 4 min 33 s 425.44 ms remaining ; 20 min 42 s 842.89 ms total) Tue Jun 16 19:07:48 2026: Iterated ≈80% of D-proof candidates. [63262532 of 79078166] (ETC: Tue Jun 16 19:11:55 2026 ; 4 min 6 s 892.39 ms remaining ; 20 min 34 s 461.87 ms total) Tue Jun 16 19:08:05 2026: Iterated ≈82% of D-proof candidates. [64844096 of 79078166] (ETC: Tue Jun 16 19:11:45 2026 ; 3 min 40 s 338.75 ms remaining ; 20 min 24 s 104.16 ms total) Tue Jun 16 19:08:23 2026: Iterated ≈84% of D-proof candidates. [66425659 of 79078166] (ETC: Tue Jun 16 19:11:37 2026 ; 3 min 14 s 650.57 ms remaining ; 20 min 16 s 566.02 ms total) Tue Jun 16 19:08:37 2026: Iterated ≈86% of D-proof candidates. [68007222 of 79078166] (ETC: Tue Jun 16 19:11:26 2026 ; 2 min 48 s 749.87 ms remaining ; 20 min 5 s 356.16 ms total) Tue Jun 16 19:08:50 2026: Iterated ≈88% of D-proof candidates. [69588786 of 79078166] (ETC: Tue Jun 16 19:11:13 2026 ; 2 min 23 s 112.14 ms remaining ; 19 min 52 s 601.17 ms total) Tue Jun 16 19:09:03 2026: Iterated ≈90% of D-proof candidates. [71170349 of 79078166] (ETC: Tue Jun 16 19:11:01 2026 ; 1 min 58 s 11.20 ms remaining ; 19 min 40 s 111.95 ms total) Tue Jun 16 19:09:19 2026: Iterated ≈92% of D-proof candidates. [72751912 of 79078166] (ETC: Tue Jun 16 19:10:53 2026 ; 1 min 33 s 796.07 ms remaining ; 19 min 32 s 450.77 ms total) Tue Jun 16 19:09:36 2026: Iterated ≈94% of D-proof candidates. [74333476 of 79078166] (ETC: Tue Jun 16 19:10:45 2026 ; 1 min 9 s 881.34 ms remaining ; 19 min 24 s 688.96 ms total) Tue Jun 16 19:09:55 2026: Iterated ≈96% of D-proof candidates. [75915039 of 79078166] (ETC: Tue Jun 16 19:10:41 2026 ; 46 s 412.74 ms remaining ; 19 min 20 s 318.45 ms total) Tue Jun 16 19:10:11 2026: Iterated ≈98% of D-proof candidates. [77496602 of 79078166] (ETC: Tue Jun 16 19:10:34 2026 ; 23 s 69.86 ms remaining ; 19 min 13 s 492.52 ms total) Tue Jun 16 19:10:26 2026: Iterated 100% of D-proof candidates. [79078166 of 79078166] (ETC: Tue Jun 16 19:10:26 2026 ; 0.00 ms remaining ; 19 min 5 s 599.52 ms total) 1145587.55 ms (19 min 5 s 587.55 ms) taken to collect 146678 D-proofs of length 153. [iterated 79078166 condensed detachment proof strings] Tue Jun 16 19:10:29 2026: Removed ≈ 2% of redundant conclusions. [ 2854 of approximately 142707] (ETC: Tue Jun 16 19:12:55 2026 ; 2 min 25 s 300.55 ms remaining ; 2 min 28 s 265.72 ms total) Tue Jun 16 19:10:32 2026: Removed ≈ 4% of redundant conclusions. [ 5708 of approximately 142707] (ETC: Tue Jun 16 19:12:57 2026 ; 2 min 24 s 975.69 ms remaining ; 2 min 31 s 16.03 ms total) Tue Jun 16 19:10:35 2026: Removed ≈ 6% of redundant conclusions. [ 8562 of approximately 142707] (ETC: Tue Jun 16 19:12:55 2026 ; 2 min 19 s 354.56 ms remaining ; 2 min 28 s 249.07 ms total) Tue Jun 16 19:10:38 2026: Removed ≈ 8% of redundant conclusions. [ 11416 of approximately 142707] (ETC: Tue Jun 16 19:12:56 2026 ; 2 min 17 s 877.23 ms remaining ; 2 min 29 s 865.91 ms total) Tue Jun 16 19:10:41 2026: Removed ≈ 10% of redundant conclusions. [ 14270 of approximately 142707] (ETC: Tue Jun 16 19:12:56 2026 ; 2 min 14 s 376.00 ms remaining ; 2 min 29 s 305.85 ms total) Tue Jun 16 19:10:45 2026: Removed ≈ 12% of redundant conclusions. [ 17124 of approximately 142707] (ETC: Tue Jun 16 19:12:57 2026 ; 2 min 12 s 917.01 ms remaining ; 2 min 31 s 41.04 ms total) Tue Jun 16 19:10:47 2026: Removed ≈ 14% of redundant conclusions. [ 19978 of approximately 142707] (ETC: Tue Jun 16 19:12:56 2026 ; 2 min 8 s 830.43 ms remaining ; 2 min 29 s 801.63 ms total) Tue Jun 16 19:10:51 2026: Removed ≈ 16% of redundant conclusions. [ 22833 of approximately 142707] (ETC: Tue Jun 16 19:12:57 2026 ; 2 min 6 s 921.55 ms remaining ; 2 min 31 s 96.93 ms total) Tue Jun 16 19:10:54 2026: Removed ≈ 18% of redundant conclusions. [ 25687 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 2 min 5 s 195.37 ms remaining ; 2 min 32 s 676.94 ms total) Tue Jun 16 19:10:57 2026: Removed ≈ 20% of redundant conclusions. [ 28541 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 2 min 2 s 505.15 ms remaining ; 2 min 33 s 130.90 ms total) Tue Jun 16 19:11:00 2026: Removed ≈ 22% of redundant conclusions. [ 31395 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 59 s 232.45 ms remaining ; 2 min 32 s 861.37 ms total) Tue Jun 16 19:11:03 2026: Removed ≈ 24% of redundant conclusions. [ 34249 of approximately 142707] (ETC: Tue Jun 16 19:12:58 2026 ; 1 min 55 s 494.79 ms remaining ; 2 min 31 s 965.88 ms total) Tue Jun 16 19:11:06 2026: Removed ≈ 26% of redundant conclusions. [ 37103 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 53 s 79.00 ms remaining ; 2 min 32 s 808.27 ms total) Tue Jun 16 19:11:09 2026: Removed ≈ 28% of redundant conclusions. [ 39957 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 49 s 838.23 ms remaining ; 2 min 32 s 551.68 ms total) Tue Jun 16 19:11:12 2026: Removed ≈ 30% of redundant conclusions. [ 42812 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 46 s 751.79 ms remaining ; 2 min 32 s 502.41 ms total) Tue Jun 16 19:11:15 2026: Removed ≈ 32% of redundant conclusions. [ 45666 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 43 s 579.22 ms remaining ; 2 min 32 s 322.01 ms total) Tue Jun 16 19:11:18 2026: Removed ≈ 34% of redundant conclusions. [ 48520 of approximately 142707] (ETC: Tue Jun 16 19:12:59 2026 ; 1 min 40 s 581.24 ms remaining ; 2 min 32 s 395.20 ms total) Tue Jun 16 19:11:22 2026: Removed ≈ 36% of redundant conclusions. [ 51374 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 38 s 74.72 ms remaining ; 2 min 33 s 240.87 ms total) Tue Jun 16 19:11:25 2026: Removed ≈ 38% of redundant conclusions. [ 54228 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 35 s 262.16 ms remaining ; 2 min 33 s 647.50 ms total) Tue Jun 16 19:11:28 2026: Removed ≈ 40% of redundant conclusions. [ 57082 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 32 s 297.93 ms remaining ; 2 min 33 s 828.45 ms total) Tue Jun 16 19:11:31 2026: Removed ≈ 42% of redundant conclusions. [ 59936 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 29 s 244.66 ms remaining ; 2 min 33 s 868.36 ms total) Tue Jun 16 19:11:34 2026: Removed ≈ 44% of redundant conclusions. [ 62791 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 26 s 406.77 ms remaining ; 2 min 34 s 297.66 ms total) Tue Jun 16 19:11:37 2026: Removed ≈ 46% of redundant conclusions. [ 65645 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 23 s 312.02 ms remaining ; 2 min 34 s 281.08 ms total) Tue Jun 16 19:11:41 2026: Removed ≈ 48% of redundant conclusions. [ 68499 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 20 s 420.16 ms remaining ; 2 min 34 s 653.41 ms total) Tue Jun 16 19:11:44 2026: Removed ≈ 50% of redundant conclusions. [ 71353 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 17 s 200.50 ms remaining ; 2 min 34 s 399.91 ms total) Tue Jun 16 19:11:47 2026: Removed ≈ 52% of redundant conclusions. [ 74207 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 14 s 38.18 ms remaining ; 2 min 34 s 244.77 ms total) Tue Jun 16 19:11:50 2026: Removed ≈ 54% of redundant conclusions. [ 77061 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 10 s 825.16 ms remaining ; 2 min 33 s 965.92 ms total) Tue Jun 16 19:11:53 2026: Removed ≈ 56% of redundant conclusions. [ 79915 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 7 s 922.80 ms remaining ; 2 min 34 s 367.75 ms total) Tue Jun 16 19:11:56 2026: Removed ≈ 58% of redundant conclusions. [ 82770 of approximately 142707] (ETC: Tue Jun 16 19:13:00 2026 ; 1 min 4 s 596.91 ms remaining ; 2 min 33 s 802.01 ms total) Tue Jun 16 19:11:59 2026: Removed ≈ 60% of redundant conclusions. [ 85624 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 1 min 1 s 729.89 ms remaining ; 2 min 34 s 324.19 ms total) Tue Jun 16 19:12:02 2026: Removed ≈ 62% of redundant conclusions. [ 88478 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 58 s 762.99 ms remaining ; 2 min 34 s 638.47 ms total) Tue Jun 16 19:12:05 2026: Removed ≈ 64% of redundant conclusions. [ 91332 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 55 s 669.56 ms remaining ; 2 min 34 s 636.22 ms total) Tue Jun 16 19:12:08 2026: Removed ≈ 66% of redundant conclusions. [ 94186 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 52 s 485.08 ms remaining ; 2 min 34 s 365.91 ms total) Tue Jun 16 19:12:11 2026: Removed ≈ 68% of redundant conclusions. [ 97040 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 49 s 430.39 ms remaining ; 2 min 34 s 467.40 ms total) Tue Jun 16 19:12:15 2026: Removed ≈ 70% of redundant conclusions. [ 99894 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 46 s 358.33 ms remaining ; 2 min 34 s 524.52 ms total) Tue Jun 16 19:12:18 2026: Removed ≈ 72% of redundant conclusions. [102749 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 43 s 351.98 ms remaining ; 2 min 34 s 828.36 ms total) Tue Jun 16 19:12:21 2026: Removed ≈ 74% of redundant conclusions. [105603 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 40 s 230.54 ms remaining ; 2 min 34 s 732.09 ms total) Tue Jun 16 19:12:24 2026: Removed ≈ 76% of redundant conclusions. [108457 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 37 s 123.32 ms remaining ; 2 min 34 s 679.04 ms total) Tue Jun 16 19:12:27 2026: Removed ≈ 78% of redundant conclusions. [111311 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 34 s 55.77 ms remaining ; 2 min 34 s 796.67 ms total) Tue Jun 16 19:12:30 2026: Removed ≈ 80% of redundant conclusions. [114165 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 30 s 903.83 ms remaining ; 2 min 34 s 515.90 ms total) Tue Jun 16 19:12:33 2026: Removed ≈ 82% of redundant conclusions. [117019 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 27 s 823.11 ms remaining ; 2 min 34 s 568.35 ms total) Tue Jun 16 19:12:36 2026: Removed ≈ 84% of redundant conclusions. [119873 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 24 s 767.51 ms remaining ; 2 min 34 s 790.94 ms total) Tue Jun 16 19:12:40 2026: Removed ≈ 86% of redundant conclusions. [122728 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 21 s 676.52 ms remaining ; 2 min 34 s 832.14 ms total) Tue Jun 16 19:12:43 2026: Removed ≈ 88% of redundant conclusions. [125582 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 18 s 590.90 ms remaining ; 2 min 34 s 922.69 ms total) Tue Jun 16 19:12:45 2026: Removed ≈ 90% of redundant conclusions. [128436 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 15 s 452.02 ms remaining ; 2 min 34 s 516.98 ms total) Tue Jun 16 19:12:48 2026: Removed ≈ 92% of redundant conclusions. [131290 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 12 s 351.14 ms remaining ; 2 min 34 s 383.26 ms total) Tue Jun 16 19:12:51 2026: Removed ≈ 94% of redundant conclusions. [134144 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 9 s 254.22 ms remaining ; 2 min 34 s 226.51 ms total) Tue Jun 16 19:12:55 2026: Removed ≈ 96% of redundant conclusions. [136998 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 6 s 174.33 ms remaining ; 2 min 34 s 338.80 ms total) Tue Jun 16 19:12:58 2026: Removed ≈ 98% of redundant conclusions. [139852 of approximately 142707] (ETC: Tue Jun 16 19:13:01 2026 ; 3 s 87.25 ms remaining ; 2 min 34 s 315.90 ms total) 153777.77 ms (2 min 33 s 777.77 ms) taken to detect 142023 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 }, { 151, 134627 }, { 153, 142023 } } 20.60 ms taken to filter and order new representative proofs. Found 4655 representative, 44785568 redundant, and 34287943 invalid condensed detachment proof strings. lengths up to 153 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753), (151,4292), (153,4655)} ; 4655 new representative proofs (44785568 redundant, 34287943 invalid) Tue Jun 16 19:13:00 2026: Starting to write 4655 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs153.txt. 7.82 ms taken to print and save 836970 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs153.txt. Determined the number of proof string candidates for iteration as 84573361. [most relevant: {41,113} with 2*4512276 = 9024552, i.e. ≈10.67%] Estimated removal count set to 149825, based on entry 153:142023 and last known pair (151:134627, 153:142023) with 142023/134627 ≈ 1.05494 and 142023 * (142023/134627)^1 ≈ 149825.31. Tue Jun 16 19:13:00 2026: Starting to generate D-proof representatives of length 155. Tue Jun 16 19:13:20 2026: Iterated ≈ 2% of D-proof candidates. [ 1691467 of 84573361] (ETC: Tue Jun 16 19:29:31 2026 ; 16 min 11 s 382.64 ms remaining ; 16 min 31 s 206.78 ms total) Tue Jun 16 19:13:42 2026: Iterated ≈ 4% of D-proof candidates. [ 3382934 of 84573361] (ETC: Tue Jun 16 19:30:32 2026 ; 16 min 50 s 49.90 ms remaining ; 17 min 32 s 135.31 ms total) Tue Jun 16 19:14:04 2026: Iterated ≈ 6% of D-proof candidates. [ 5074401 of 84573361] (ETC: Tue Jun 16 19:30:45 2026 ; 16 min 40 s 875.38 ms remaining ; 17 min 44 s 761.04 ms total) Tue Jun 16 19:14:31 2026: Iterated ≈ 8% of D-proof candidates. [ 6765868 of 84573361] (ETC: Tue Jun 16 19:31:54 2026 ; 17 min 22 s 845.29 ms remaining ; 18 min 53 s 527.47 ms total) Tue Jun 16 19:15:02 2026: Iterated ≈10% of D-proof candidates. [ 8457336 of 84573361] (ETC: Tue Jun 16 19:33:23 2026 ; 18 min 20 s 501.95 ms remaining ; 20 min 22 s 779.94 ms total) Tue Jun 16 19:15:32 2026: Iterated ≈12% of D-proof candidates. [10148803 of 84573361] (ETC: Tue Jun 16 19:34:07 2026 ; 18 min 35 s 148.48 ms remaining ; 21 min 7 s 214.18 ms total) Tue Jun 16 19:16:04 2026: Iterated ≈14% of D-proof candidates. [11840270 of 84573361] (ETC: Tue Jun 16 19:34:50 2026 ; 18 min 46 s 689.07 ms remaining ; 21 min 50 s 103.56 ms total) Tue Jun 16 19:16:32 2026: Iterated ≈16% of D-proof candidates. [13531737 of 84573361] (ETC: Tue Jun 16 19:35:06 2026 ; 18 min 34 s 113.79 ms remaining ; 22 min 6 s 325.93 ms total) Tue Jun 16 19:16:59 2026: Iterated ≈18% of D-proof candidates. [15223204 of 84573361] (ETC: Tue Jun 16 19:35:09 2026 ; 18 min 9 s 737.64 ms remaining ; 22 min 8 s 948.32 ms total) Tue Jun 16 19:17:26 2026: Iterated ≈20% of D-proof candidates. [16914672 of 84573361] (ETC: Tue Jun 16 19:35:11 2026 ; 17 min 44 s 848.92 ms remaining ; 22 min 11 s 61.15 ms total) Tue Jun 16 19:17:56 2026: Iterated ≈22% of D-proof candidates. [18606139 of 84573361] (ETC: Tue Jun 16 19:35:23 2026 ; 17 min 27 s 248.93 ms remaining ; 22 min 22 s 626.82 ms total) Tue Jun 16 19:18:23 2026: Iterated ≈24% of D-proof candidates. [20297606 of 84573361] (ETC: Tue Jun 16 19:35:27 2026 ; 17 min 3 s 560.08 ms remaining ; 22 min 26 s 789.57 ms total) Tue Jun 16 19:18:57 2026: Iterated ≈26% of D-proof candidates. [21989073 of 84573361] (ETC: Tue Jun 16 19:35:53 2026 ; 16 min 55 s 636.99 ms remaining ; 22 min 52 s 482.40 ms total) Tue Jun 16 19:19:23 2026: Iterated ≈28% of D-proof candidates. [23680541 of 84573361] (ETC: Tue Jun 16 19:35:49 2026 ; 16 min 25 s 412.37 ms remaining ; 22 min 48 s 628.28 ms total) Tue Jun 16 19:19:46 2026: Iterated ≈30% of D-proof candidates. [25372008 of 84573361] (ETC: Tue Jun 16 19:35:35 2026 ; 15 min 48 s 47.91 ms remaining ; 22 min 34 s 354.15 ms total) Tue Jun 16 19:20:15 2026: Iterated ≈32% of D-proof candidates. [27063475 of 84573361] (ETC: Tue Jun 16 19:35:39 2026 ; 15 min 24 s 255.76 ms remaining ; 22 min 39 s 199.64 ms total) Tue Jun 16 19:20:43 2026: Iterated ≈34% of D-proof candidates. [28754942 of 84573361] (ETC: Tue Jun 16 19:35:43 2026 ; 14 min 59 s 355.83 ms remaining ; 22 min 42 s 660.33 ms total) Tue Jun 16 19:21:14 2026: Iterated ≈36% of D-proof candidates. [30446409 of 84573361] (ETC: Tue Jun 16 19:35:52 2026 ; 14 min 38 s 132.05 ms remaining ; 22 min 52 s 81.30 ms total) Tue Jun 16 19:21:42 2026: Iterated ≈38% of D-proof candidates. [32137877 of 84573361] (ETC: Tue Jun 16 19:35:53 2026 ; 14 min 11 s 287.49 ms remaining ; 22 min 53 s 44.33 ms total) Tue Jun 16 19:22:13 2026: Iterated ≈40% of D-proof candidates. [33829344 of 84573361] (ETC: Tue Jun 16 19:36:02 2026 ; 13 min 48 s 849.92 ms remaining ; 23 min 1 s 416.53 ms total) Tue Jun 16 19:22:42 2026: Iterated ≈42% of D-proof candidates. [35520811 of 84573361] (ETC: Tue Jun 16 19:36:05 2026 ; 13 min 23 s 185.77 ms remaining ; 23 min 4 s 803.04 ms total) Tue Jun 16 19:23:09 2026: Iterated ≈44% of D-proof candidates. [37212278 of 84573361] (ETC: Tue Jun 16 19:36:04 2026 ; 12 min 54 s 967.26 ms remaining ; 23 min 3 s 870.09 ms total) Tue Jun 16 19:23:37 2026: Iterated ≈46% of D-proof candidates. [38903746 of 84573361] (ETC: Tue Jun 16 19:36:06 2026 ; 12 min 28 s 120.05 ms remaining ; 23 min 5 s 407.50 ms total) Tue Jun 16 19:24:07 2026: Iterated ≈48% of D-proof candidates. [40595213 of 84573361] (ETC: Tue Jun 16 19:36:09 2026 ; 12 min 2 s 414.50 ms remaining ; 23 min 9 s 258.64 ms total) Tue Jun 16 19:24:33 2026: Iterated ≈50% of D-proof candidates. [42286680 of 84573361] (ETC: Tue Jun 16 19:36:05 2026 ; 11 min 32 s 344.62 ms remaining ; 23 min 4 s 689.21 ms total) Tue Jun 16 19:24:51 2026: Iterated ≈52% of D-proof candidates. [43978147 of 84573361] (ETC: Tue Jun 16 19:35:47 2026 ; 10 min 56 s 190.17 ms remaining ; 22 min 47 s 62.83 ms total) Tue Jun 16 19:25:10 2026: Iterated ≈54% of D-proof candidates. [45669614 of 84573361] (ETC: Tue Jun 16 19:35:31 2026 ; 10 min 21 s 442.76 ms remaining ; 22 min 30 s 962.48 ms total) Tue Jun 16 19:25:27 2026: Iterated ≈56% of D-proof candidates. [47361082 of 84573361] (ETC: Tue Jun 16 19:35:14 2026 ; 9 min 46 s 749.21 ms remaining ; 22 min 13 s 520.92 ms total) Tue Jun 16 19:25:47 2026: Iterated ≈58% of D-proof candidates. [49052549 of 84573361] (ETC: Tue Jun 16 19:35:02 2026 ; 9 min 15 s 87.83 ms remaining ; 22 min 1 s 637.67 ms total) Tue Jun 16 19:26:05 2026: Iterated ≈60% of D-proof candidates. [50744016 of 84573361] (ETC: Tue Jun 16 19:34:49 2026 ; 8 min 43 s 461.29 ms remaining ; 21 min 48 s 653.20 ms total) Tue Jun 16 19:26:23 2026: Iterated ≈62% of D-proof candidates. [52435483 of 84573361] (ETC: Tue Jun 16 19:34:34 2026 ; 8 min 11 s 821.09 ms remaining ; 21 min 34 s 265.98 ms total) Tue Jun 16 19:26:38 2026: Iterated ≈64% of D-proof candidates. [54126951 of 84573361] (ETC: Tue Jun 16 19:34:18 2026 ; 7 min 40 s 7.87 ms remaining ; 21 min 17 s 799.65 ms total) Tue Jun 16 19:26:56 2026: Iterated ≈66% of D-proof candidates. [55818418 of 84573361] (ETC: Tue Jun 16 19:34:07 2026 ; 7 min 10 s 749.52 ms remaining ; 21 min 6 s 910.35 ms total) Tue Jun 16 19:27:15 2026: Iterated ≈68% of D-proof candidates. [57509885 of 84573361] (ETC: Tue Jun 16 19:33:57 2026 ; 6 min 42 s 302.08 ms remaining ; 20 min 57 s 193.98 ms total) Tue Jun 16 19:27:34 2026: Iterated ≈70% of D-proof candidates. [59201352 of 84573361] (ETC: Tue Jun 16 19:33:48 2026 ; 6 min 14 s 296.71 ms remaining ; 20 min 47 s 655.66 ms total) Tue Jun 16 19:27:50 2026: Iterated ≈72% of D-proof candidates. [60892819 of 84573361] (ETC: Tue Jun 16 19:33:37 2026 ; 5 min 46 s 188.10 ms remaining ; 20 min 36 s 386.01 ms total) Tue Jun 16 19:28:06 2026: Iterated ≈74% of D-proof candidates. [62584287 of 84573361] (ETC: Tue Jun 16 19:33:24 2026 ; 5 min 18 s 95.17 ms remaining ; 20 min 23 s 442.95 ms total) Tue Jun 16 19:28:23 2026: Iterated ≈76% of D-proof candidates. [64275754 of 84573361] (ETC: Tue Jun 16 19:33:14 2026 ; 4 min 51 s 383.62 ms remaining ; 20 min 14 s 98.40 ms total) Tue Jun 16 19:28:42 2026: Iterated ≈78% of D-proof candidates. [65967221 of 84573361] (ETC: Tue Jun 16 19:33:08 2026 ; 4 min 25 s 690.31 ms remaining ; 20 min 7 s 683.19 ms total) Tue Jun 16 19:29:01 2026: Iterated ≈80% of D-proof candidates. [67658688 of 84573361] (ETC: Tue Jun 16 19:33:01 2026 ; 4 min 228.50 ms remaining ; 20 min 1 s 142.47 ms total) Tue Jun 16 19:29:20 2026: Iterated ≈82% of D-proof candidates. [69350156 of 84573361] (ETC: Tue Jun 16 19:32:55 2026 ; 3 min 35 s 89.91 ms remaining ; 19 min 54 s 943.96 ms total) Tue Jun 16 19:29:36 2026: Iterated ≈84% of D-proof candidates. [71041623 of 84573361] (ETC: Tue Jun 16 19:32:46 2026 ; 3 min 9 s 771.24 ms remaining ; 19 min 46 s 70.22 ms total) Tue Jun 16 19:29:55 2026: Iterated ≈86% of D-proof candidates. [72733090 of 84573361] (ETC: Tue Jun 16 19:32:40 2026 ; 2 min 45 s 139.94 ms remaining ; 19 min 39 s 570.96 ms total) Tue Jun 16 19:30:11 2026: Iterated ≈88% of D-proof candidates. [74424557 of 84573361] (ETC: Tue Jun 16 19:32:32 2026 ; 2 min 20 s 568.96 ms remaining ; 19 min 31 s 407.92 ms total) Tue Jun 16 19:30:30 2026: Iterated ≈90% of D-proof candidates. [76116024 of 84573361] (ETC: Tue Jun 16 19:32:26 2026 ; 1 min 56 s 617.68 ms remaining ; 19 min 26 s 176.71 ms total) Tue Jun 16 19:30:46 2026: Iterated ≈92% of D-proof candidates. [77807492 of 84573361] (ETC: Tue Jun 16 19:32:19 2026 ; 1 min 32 s 706.61 ms remaining ; 19 min 18 s 832.59 ms total) Tue Jun 16 19:31:04 2026: Iterated ≈94% of D-proof candidates. [79498959 of 84573361] (ETC: Tue Jun 16 19:32:13 2026 ; 1 min 9 s 156.19 ms remaining ; 19 min 12 s 603.16 ms total) Tue Jun 16 19:31:20 2026: Iterated ≈96% of D-proof candidates. [81190426 of 84573361] (ETC: Tue Jun 16 19:32:06 2026 ; 45 s 838.75 ms remaining ; 19 min 5 s 968.68 ms total) Tue Jun 16 19:31:34 2026: Iterated ≈98% of D-proof candidates. [82881893 of 84573361] (ETC: Tue Jun 16 19:31:57 2026 ; 22 s 735.72 ms remaining ; 18 min 56 s 785.44 ms total) Tue Jun 16 19:31:54 2026: Iterated 100% of D-proof candidates. [84573361 of 84573361] (ETC: Tue Jun 16 19:31:54 2026 ; 0.00 ms remaining ; 18 min 54 s 194.87 ms total) 1134183.32 ms (18 min 54 s 183.31 ms) taken to collect 152930 D-proofs of length 155. [iterated 84573361 condensed detachment proof strings] Tue Jun 16 19:31:58 2026: Removed ≈ 2% of redundant conclusions. [ 2996 of approximately 149825] (ETC: Tue Jun 16 19:34:42 2026 ; 2 min 44 s 481.41 ms remaining ; 2 min 47 s 837.61 ms total) Tue Jun 16 19:32:02 2026: Removed ≈ 4% of redundant conclusions. [ 5993 of approximately 149825] (ETC: Tue Jun 16 19:34:58 2026 ; 2 min 56 s 554.08 ms remaining ; 3 min 3 s 910.50 ms total) Tue Jun 16 19:32:05 2026: Removed ≈ 6% of redundant conclusions. [ 8989 of approximately 149825] (ETC: Tue Jun 16 19:34:54 2026 ; 2 min 48 s 796.64 ms remaining ; 2 min 59 s 570.25 ms total) Tue Jun 16 19:32:08 2026: Removed ≈ 8% of redundant conclusions. [ 11986 of approximately 149825] (ETC: Tue Jun 16 19:34:50 2026 ; 2 min 41 s 906.26 ms remaining ; 2 min 55 s 985.06 ms total) Tue Jun 16 19:32:12 2026: Removed ≈ 10% of redundant conclusions. [ 14982 of approximately 149825] (ETC: Tue Jun 16 19:34:51 2026 ; 2 min 39 s 198.00 ms remaining ; 2 min 56 s 886.01 ms total) Tue Jun 16 19:32:16 2026: Removed ≈ 12% of redundant conclusions. [ 17979 of approximately 149825] (ETC: Tue Jun 16 19:34:51 2026 ; 2 min 35 s 204.21 ms remaining ; 2 min 56 s 368.42 ms total) Tue Jun 16 19:32:19 2026: Removed ≈ 14% of redundant conclusions. [ 20975 of approximately 149825] (ETC: Tue Jun 16 19:34:50 2026 ; 2 min 31 s 434.29 ms remaining ; 2 min 56 s 85.70 ms total) Tue Jun 16 19:32:22 2026: Removed ≈ 16% of redundant conclusions. [ 23972 of approximately 149825] (ETC: Tue Jun 16 19:34:49 2026 ; 2 min 26 s 745.89 ms remaining ; 2 min 54 s 697.49 ms total) Tue Jun 16 19:32:26 2026: Removed ≈ 18% of redundant conclusions. [ 26968 of approximately 149825] (ETC: Tue Jun 16 19:34:48 2026 ; 2 min 22 s 459.03 ms remaining ; 2 min 53 s 729.82 ms total) Tue Jun 16 19:32:29 2026: Removed ≈ 20% of redundant conclusions. [ 29965 of approximately 149825] (ETC: Tue Jun 16 19:34:49 2026 ; 2 min 19 s 567.98 ms remaining ; 2 min 54 s 459.98 ms total) Tue Jun 16 19:32:33 2026: Removed ≈ 22% of redundant conclusions. [ 32961 of approximately 149825] (ETC: Tue Jun 16 19:34:48 2026 ; 2 min 15 s 602.75 ms remaining ; 2 min 53 s 848.94 ms total) Tue Jun 16 19:32:36 2026: Removed ≈ 24% of redundant conclusions. [ 35958 of approximately 149825] (ETC: Tue Jun 16 19:34:47 2026 ; 2 min 10 s 993.49 ms remaining ; 2 min 52 s 359.86 ms total) Tue Jun 16 19:32:39 2026: Removed ≈ 26% of redundant conclusions. [ 38954 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 2 min 7 s 360.65 ms remaining ; 2 min 52 s 108.21 ms total) Tue Jun 16 19:32:42 2026: Removed ≈ 28% of redundant conclusions. [ 41951 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 2 min 3 s 8.75 ms remaining ; 2 min 50 s 845.49 ms total) Tue Jun 16 19:32:45 2026: Removed ≈ 30% of redundant conclusions. [ 44947 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 1 min 59 s 190.71 ms remaining ; 2 min 50 s 271.63 ms total) Tue Jun 16 19:32:49 2026: Removed ≈ 32% of redundant conclusions. [ 47944 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 56 s 422.66 ms remaining ; 2 min 51 s 209.79 ms total) Tue Jun 16 19:32:53 2026: Removed ≈ 34% of redundant conclusions. [ 50940 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 53 s 77.79 ms remaining ; 2 min 51 s 329.13 ms total) Tue Jun 16 19:32:56 2026: Removed ≈ 36% of redundant conclusions. [ 53937 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 49 s 696.94 ms remaining ; 2 min 51 s 401.47 ms total) Tue Jun 16 19:33:00 2026: Removed ≈ 38% of redundant conclusions. [ 56933 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 46 s 355.54 ms remaining ; 2 min 51 s 540.26 ms total) Tue Jun 16 19:33:03 2026: Removed ≈ 40% of redundant conclusions. [ 59930 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 42 s 742.38 ms remaining ; 2 min 51 s 237.29 ms total) Tue Jun 16 19:33:06 2026: Removed ≈ 42% of redundant conclusions. [ 62926 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 39 s 478.43 ms remaining ; 2 min 51 s 513.55 ms total) Tue Jun 16 19:33:10 2026: Removed ≈ 44% of redundant conclusions. [ 65923 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 36 s 162.59 ms remaining ; 2 min 51 s 718.91 ms total) Tue Jun 16 19:33:13 2026: Removed ≈ 46% of redundant conclusions. [ 68919 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 32 s 574.28 ms remaining ; 2 min 51 s 432.79 ms total) Tue Jun 16 19:33:17 2026: Removed ≈ 48% of redundant conclusions. [ 71916 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 29 s 215.44 ms remaining ; 2 min 51 s 568.15 ms total) Tue Jun 16 19:33:20 2026: Removed ≈ 50% of redundant conclusions. [ 74912 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 25 s 795.05 ms remaining ; 2 min 51 s 588.96 ms total) Tue Jun 16 19:33:24 2026: Removed ≈ 52% of redundant conclusions. [ 77909 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 22 s 585.95 ms remaining ; 2 min 52 s 54.07 ms total) Tue Jun 16 19:33:27 2026: Removed ≈ 54% of redundant conclusions. [ 80905 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 19 s 62.55 ms remaining ; 2 min 51 s 873.85 ms total) Tue Jun 16 19:33:30 2026: Removed ≈ 56% of redundant conclusions. [ 83902 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 15 s 487.89 ms remaining ; 2 min 51 s 563.38 ms total) Tue Jun 16 19:33:34 2026: Removed ≈ 58% of redundant conclusions. [ 86898 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 12 s 205.29 ms remaining ; 2 min 51 s 915.99 ms total) Tue Jun 16 19:33:38 2026: Removed ≈ 60% of redundant conclusions. [ 89895 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 8 s 742.60 ms remaining ; 2 min 51 s 856.50 ms total) Tue Jun 16 19:33:41 2026: Removed ≈ 62% of redundant conclusions. [ 92891 of approximately 149825] (ETC: Tue Jun 16 19:34:46 2026 ; 1 min 5 s 155.04 ms remaining ; 2 min 51 s 459.12 ms total) Tue Jun 16 19:33:44 2026: Removed ≈ 64% of redundant conclusions. [ 95888 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 1 min 1 s 585.46 ms remaining ; 2 min 51 s 70.72 ms total) Tue Jun 16 19:33:47 2026: Removed ≈ 66% of redundant conclusions. [ 98884 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 58 s 159.65 ms remaining ; 2 min 51 s 56.10 ms total) Tue Jun 16 19:33:50 2026: Removed ≈ 68% of redundant conclusions. [101881 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 54 s 627.59 ms remaining ; 2 min 50 s 711.23 ms total) Tue Jun 16 19:33:54 2026: Removed ≈ 70% of redundant conclusions. [104877 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 51 s 147.74 ms remaining ; 2 min 50 s 490.56 ms total) Tue Jun 16 19:33:57 2026: Removed ≈ 72% of redundant conclusions. [107874 of approximately 149825] (ETC: Tue Jun 16 19:34:44 2026 ; 47 s 604.28 ms remaining ; 2 min 50 s 15.28 ms total) Tue Jun 16 19:34:00 2026: Removed ≈ 74% of redundant conclusions. [110870 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 44 s 267.60 ms remaining ; 2 min 50 s 257.80 ms total) Tue Jun 16 19:34:04 2026: Removed ≈ 76% of redundant conclusions. [113867 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 40 s 893.92 ms remaining ; 2 min 50 s 391.32 ms total) Tue Jun 16 19:34:07 2026: Removed ≈ 78% of redundant conclusions. [116863 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 37 s 504.13 ms remaining ; 2 min 50 s 470.74 ms total) Tue Jun 16 19:34:11 2026: Removed ≈ 80% of redundant conclusions. [119860 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 34 s 87.95 ms remaining ; 2 min 50 s 439.75 ms total) Tue Jun 16 19:34:14 2026: Removed ≈ 82% of redundant conclusions. [122856 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 30 s 712.21 ms remaining ; 2 min 50 s 620.21 ms total) Tue Jun 16 19:34:18 2026: Removed ≈ 84% of redundant conclusions. [125853 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 27 s 276.23 ms remaining ; 2 min 50 s 476.42 ms total) Tue Jun 16 19:34:21 2026: Removed ≈ 86% of redundant conclusions. [128849 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 23 s 842.23 ms remaining ; 2 min 50 s 297.61 ms total) Tue Jun 16 19:34:24 2026: Removed ≈ 88% of redundant conclusions. [131846 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 20 s 430.08 ms remaining ; 2 min 50 s 250.65 ms total) Tue Jun 16 19:34:28 2026: Removed ≈ 90% of redundant conclusions. [134842 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 17 s 63.50 ms remaining ; 2 min 50 s 629.28 ms total) Tue Jun 16 19:34:31 2026: Removed ≈ 92% of redundant conclusions. [137839 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 13 s 651.91 ms remaining ; 2 min 50 s 648.89 ms total) Tue Jun 16 19:34:35 2026: Removed ≈ 94% of redundant conclusions. [140835 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 10 s 227.30 ms remaining ; 2 min 50 s 445.46 ms total) Tue Jun 16 19:34:38 2026: Removed ≈ 96% of redundant conclusions. [143832 of approximately 149825] (ETC: Tue Jun 16 19:34:45 2026 ; 6 s 811.43 ms remaining ; 2 min 50 s 285.78 ms total) Tue Jun 16 19:34:41 2026: Removed ≈ 98% of redundant conclusions. [146828 of approximately 149825] (ETC: Tue Jun 16 19:34:44 2026 ; 3 s 397.69 ms remaining ; 2 min 49 s 856.21 ms total) 167930.34 ms (2 min 47 s 930.34 ms) taken to detect 148062 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 }, { 151, 134627 }, { 153, 142023 }, { 155, 148062 } } 26.85 ms taken to filter and order new representative proofs. Found 4868 representative, 47840686 redundant, and 36727807 invalid condensed detachment proof strings. lengths up to 155 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753), (151,4292), (153,4655), (155,4868)} ; 4868 new representative proofs (47840686 redundant, 36727807 invalid) Tue Jun 16 19:34:42 2026: Starting to write 4868 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs155.txt. 3.64 ms taken to print and save 884389 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs155.txt. Determined the number of proof string candidates for iteration as 90164836. [most relevant: {41,115} with 2*4605600 = 9211200, i.e. ≈10.22%] Estimated removal count set to 154357, based on entry 155:148062 and last known pair (153:142023, 155:148062) with 148062/142023 ≈ 1.04252 and 148062 * (148062/142023)^1 ≈ 154357.79. Tue Jun 16 19:34:42 2026: Starting to generate D-proof representatives of length 157. Tue Jun 16 19:35:03 2026: Iterated ≈ 2% of D-proof candidates. [ 1803296 of 90164836] (ETC: Tue Jun 16 19:51:53 2026 ; 16 min 49 s 997.13 ms remaining ; 17 min 10 s 609.31 ms total) Tue Jun 16 19:35:26 2026: Iterated ≈ 4% of D-proof candidates. [ 3606593 of 90164836] (ETC: Tue Jun 16 19:52:58 2026 ; 17 min 31 s 716.28 ms remaining ; 18 min 15 s 537.78 ms total) Tue Jun 16 19:35:52 2026: Iterated ≈ 6% of D-proof candidates. [ 5409890 of 90164836] (ETC: Tue Jun 16 19:54:10 2026 ; 18 min 17 s 982.83 ms remaining ; 19 min 28 s 66.83 ms total) Tue Jun 16 19:36:21 2026: Iterated ≈ 8% of D-proof candidates. [ 7213186 of 90164836] (ETC: Tue Jun 16 19:55:11 2026 ; 18 min 50 s 411.30 ms remaining ; 20 min 28 s 707.92 ms total) Tue Jun 16 19:36:49 2026: Iterated ≈10% of D-proof candidates. [ 9016483 of 90164836] (ETC: Tue Jun 16 19:55:53 2026 ; 19 min 3 s 794.50 ms remaining ; 21 min 10 s 882.77 ms total) Tue Jun 16 19:37:20 2026: Iterated ≈12% of D-proof candidates. [10819780 of 90164836] (ETC: Tue Jun 16 19:56:36 2026 ; 19 min 15 s 806.81 ms remaining ; 21 min 53 s 416.82 ms total) Tue Jun 16 19:37:49 2026: Iterated ≈14% of D-proof candidates. [12623077 of 90164836] (ETC: Tue Jun 16 19:56:58 2026 ; 19 min 8 s 331.54 ms remaining ; 22 min 15 s 269.23 ms total) Tue Jun 16 19:38:20 2026: Iterated ≈16% of D-proof candidates. [14426373 of 90164836] (ETC: Tue Jun 16 19:57:25 2026 ; 19 min 4 s 948.80 ms remaining ; 22 min 43 s 34.28 ms total) Tue Jun 16 19:38:51 2026: Iterated ≈18% of D-proof candidates. [16229670 of 90164836] (ETC: Tue Jun 16 19:57:41 2026 ; 18 min 50 s 680.71 ms remaining ; 22 min 58 s 878.91 ms total) Tue Jun 16 19:39:25 2026: Iterated ≈20% of D-proof candidates. [18032967 of 90164836] (ETC: Tue Jun 16 19:58:14 2026 ; 18 min 49 s 164.60 ms remaining ; 23 min 31 s 455.75 ms total) Tue Jun 16 19:39:53 2026: Iterated ≈22% of D-proof candidates. [19836263 of 90164836] (ETC: Tue Jun 16 19:58:15 2026 ; 18 min 21 s 678.35 ms remaining ; 23 min 32 s 408.12 ms total) Tue Jun 16 19:40:24 2026: Iterated ≈24% of D-proof candidates. [21639560 of 90164836] (ETC: Tue Jun 16 19:58:26 2026 ; 18 min 1 s 928.25 ms remaining ; 23 min 43 s 589.80 ms total) Tue Jun 16 19:41:00 2026: Iterated ≈26% of D-proof candidates. [23442857 of 90164836] (ETC: Tue Jun 16 19:58:55 2026 ; 17 min 54 s 868.81 ms remaining ; 24 min 12 s 525.41 ms total) Tue Jun 16 19:41:29 2026: Iterated ≈28% of D-proof candidates. [25246154 of 90164836] (ETC: Tue Jun 16 19:58:56 2026 ; 17 min 26 s 783.02 ms remaining ; 24 min 13 s 865.30 ms total) Tue Jun 16 19:42:03 2026: Iterated ≈30% of D-proof candidates. [27049450 of 90164836] (ETC: Tue Jun 16 19:59:12 2026 ; 17 min 8 s 865.22 ms remaining ; 24 min 29 s 807.44 ms total) Tue Jun 16 19:42:42 2026: Iterated ≈32% of D-proof candidates. [28852747 of 90164836] (ETC: Tue Jun 16 19:59:40 2026 ; 16 min 58 s 466.65 ms remaining ; 24 min 57 s 745.07 ms total) Tue Jun 16 19:43:19 2026: Iterated ≈34% of D-proof candidates. [30656044 of 90164836] (ETC: Tue Jun 16 20:00:02 2026 ; 16 min 43 s 80.74 ms remaining ; 25 min 19 s 819.29 ms total) Tue Jun 16 19:43:50 2026: Iterated ≈36% of D-proof candidates. [32459340 of 90164836] (ETC: Tue Jun 16 20:00:05 2026 ; 16 min 14 s 466.45 ms remaining ; 25 min 22 s 603.80 ms total) Tue Jun 16 19:44:23 2026: Iterated ≈38% of D-proof candidates. [34262637 of 90164836] (ETC: Tue Jun 16 20:00:11 2026 ; 15 min 48 s 68.52 ms remaining ; 25 min 29 s 142.75 ms total) Tue Jun 16 19:44:58 2026: Iterated ≈40% of D-proof candidates. [36065934 of 90164836] (ETC: Tue Jun 16 20:00:20 2026 ; 15 min 22 s 797.30 ms remaining ; 25 min 37 s 995.48 ms total) Tue Jun 16 19:45:30 2026: Iterated ≈42% of D-proof candidates. [37869231 of 90164836] (ETC: Tue Jun 16 20:00:25 2026 ; 14 min 54 s 996.72 ms remaining ; 25 min 43 s 97.79 ms total) Tue Jun 16 19:46:00 2026: Iterated ≈44% of D-proof candidates. [39672527 of 90164836] (ETC: Tue Jun 16 20:00:23 2026 ; 14 min 22 s 921.57 ms remaining ; 25 min 40 s 931.35 ms total) Tue Jun 16 19:46:29 2026: Iterated ≈46% of D-proof candidates. [41475824 of 90164836] (ETC: Tue Jun 16 20:00:18 2026 ; 13 min 49 s 134.10 ms remaining ; 25 min 35 s 433.49 ms total) Tue Jun 16 19:46:59 2026: Iterated ≈48% of D-proof candidates. [43279121 of 90164836] (ETC: Tue Jun 16 20:00:17 2026 ; 13 min 18 s 51.74 ms remaining ; 25 min 34 s 714.87 ms total) Tue Jun 16 19:47:21 2026: Iterated ≈50% of D-proof candidates. [45082418 of 90164836] (ETC: Tue Jun 16 19:59:59 2026 ; 12 min 38 s 209.37 ms remaining ; 25 min 16 s 418.73 ms total) Tue Jun 16 19:47:40 2026: Iterated ≈52% of D-proof candidates. [46885714 of 90164836] (ETC: Tue Jun 16 19:59:38 2026 ; 11 min 58 s 129.40 ms remaining ; 24 min 56 s 102.90 ms total) Tue Jun 16 19:48:01 2026: Iterated ≈54% of D-proof candidates. [48689011 of 90164836] (ETC: Tue Jun 16 19:59:21 2026 ; 11 min 20 s 176.18 ms remaining ; 24 min 38 s 643.84 ms total) Tue Jun 16 19:48:20 2026: Iterated ≈56% of D-proof candidates. [50492308 of 90164836] (ETC: Tue Jun 16 19:59:02 2026 ; 10 min 42 s 449.32 ms remaining ; 24 min 20 s 112.09 ms total) Tue Jun 16 19:48:37 2026: Iterated ≈58% of D-proof candidates. [52295604 of 90164836] (ETC: Tue Jun 16 19:58:42 2026 ; 10 min 4 s 518.88 ms remaining ; 23 min 59 s 330.62 ms total) Tue Jun 16 19:48:56 2026: Iterated ≈60% of D-proof candidates. [54098901 of 90164836] (ETC: Tue Jun 16 19:58:25 2026 ; 9 min 28 s 901.89 ms remaining ; 23 min 42 s 254.70 ms total) Tue Jun 16 19:49:12 2026: Iterated ≈62% of D-proof candidates. [55902198 of 90164836] (ETC: Tue Jun 16 19:58:05 2026 ; 8 min 52 s 889.16 ms remaining ; 23 min 22 s 339.89 ms total) Tue Jun 16 19:49:29 2026: Iterated ≈64% of D-proof candidates. [57705495 of 90164836] (ETC: Tue Jun 16 19:57:47 2026 ; 8 min 18 s 646.52 ms remaining ; 23 min 5 s 129.22 ms total) Tue Jun 16 19:49:47 2026: Iterated ≈66% of D-proof candidates. [59508791 of 90164836] (ETC: Tue Jun 16 19:57:33 2026 ; 7 min 46 s 138.86 ms remaining ; 22 min 50 s 996.61 ms total) Tue Jun 16 19:50:04 2026: Iterated ≈68% of D-proof candidates. [61312088 of 90164836] (ETC: Tue Jun 16 19:57:18 2026 ; 7 min 13 s 886.00 ms remaining ; 22 min 35 s 893.74 ms total) Tue Jun 16 19:50:24 2026: Iterated ≈70% of D-proof candidates. [63115385 of 90164836] (ETC: Tue Jun 16 19:57:08 2026 ; 6 min 43 s 556.94 ms remaining ; 22 min 25 s 189.80 ms total) Tue Jun 16 19:50:46 2026: Iterated ≈72% of D-proof candidates. [64918681 of 90164836] (ETC: Tue Jun 16 19:57:00 2026 ; 6 min 14 s 568.50 ms remaining ; 22 min 17 s 744.59 ms total) Tue Jun 16 19:51:07 2026: Iterated ≈74% of D-proof candidates. [66721978 of 90164836] (ETC: Tue Jun 16 19:56:53 2026 ; 5 min 45 s 957.53 ms remaining ; 22 min 10 s 605.85 ms total) Tue Jun 16 19:51:25 2026: Iterated ≈76% of D-proof candidates. [68525275 of 90164836] (ETC: Tue Jun 16 19:56:41 2026 ; 5 min 16 s 533.59 ms remaining ; 21 min 58 s 889.92 ms total) Tue Jun 16 19:51:44 2026: Iterated ≈78% of D-proof candidates. [70328572 of 90164836] (ETC: Tue Jun 16 19:56:32 2026 ; 4 min 48 s 32.30 ms remaining ; 21 min 49 s 237.71 ms total) Tue Jun 16 19:52:01 2026: Iterated ≈80% of D-proof candidates. [72131868 of 90164836] (ETC: Tue Jun 16 19:56:21 2026 ; 4 min 19 s 670.87 ms remaining ; 21 min 38 s 354.27 ms total) Tue Jun 16 19:52:19 2026: Iterated ≈82% of D-proof candidates. [73935165 of 90164836] (ETC: Tue Jun 16 19:56:11 2026 ; 3 min 51 s 879.39 ms remaining ; 21 min 28 s 218.81 ms total) Tue Jun 16 19:52:35 2026: Iterated ≈84% of D-proof candidates. [75738462 of 90164836] (ETC: Tue Jun 16 19:55:59 2026 ; 3 min 24 s 286.36 ms remaining ; 21 min 16 s 789.70 ms total) Tue Jun 16 19:52:49 2026: Iterated ≈86% of D-proof candidates. [77541758 of 90164836] (ETC: Tue Jun 16 19:55:46 2026 ; 2 min 56 s 956.30 ms remaining ; 21 min 3 s 973.47 ms total) Tue Jun 16 19:53:07 2026: Iterated ≈88% of D-proof candidates. [79345055 of 90164836] (ETC: Tue Jun 16 19:55:37 2026 ; 2 min 30 s 575.89 ms remaining ; 20 min 54 s 799.05 ms total) Tue Jun 16 19:53:27 2026: Iterated ≈90% of D-proof candidates. [81148352 of 90164836] (ETC: Tue Jun 16 19:55:32 2026 ; 2 min 4 s 976.49 ms remaining ; 20 min 49 s 764.82 ms total) Tue Jun 16 19:53:48 2026: Iterated ≈92% of D-proof candidates. [82951649 of 90164836] (ETC: Tue Jun 16 19:55:28 2026 ; 1 min 39 s 666.66 ms remaining ; 20 min 45 s 833.21 ms total) Tue Jun 16 19:54:07 2026: Iterated ≈94% of D-proof candidates. [84754945 of 90164836] (ETC: Tue Jun 16 19:55:22 2026 ; 1 min 14 s 371.33 ms remaining ; 20 min 39 s 521.97 ms total) Tue Jun 16 19:54:31 2026: Iterated ≈96% of D-proof candidates. [86558242 of 90164836] (ETC: Tue Jun 16 19:55:20 2026 ; 49 s 508.88 ms remaining ; 20 min 37 s 721.84 ms total) Tue Jun 16 19:54:48 2026: Iterated ≈98% of D-proof candidates. [88361539 of 90164836] (ETC: Tue Jun 16 19:55:13 2026 ; 24 s 613.88 ms remaining ; 20 min 30 s 693.86 ms total) Tue Jun 16 19:55:06 2026: Iterated 100% of D-proof candidates. [90164836 of 90164836] (ETC: Tue Jun 16 19:55:06 2026 ; 0.00 ms remaining ; 20 min 23 s 917.00 ms total) 1223904.33 ms (20 min 23 s 904.33 ms) taken to collect 158760 D-proofs of length 157. [iterated 90164836 condensed detachment proof strings] Tue Jun 16 19:55:10 2026: Removed ≈ 2% of redundant conclusions. [ 3087 of approximately 154357] (ETC: Tue Jun 16 19:58:15 2026 ; 3 min 5 s 92.15 ms remaining ; 3 min 8 s 869.37 ms total) Tue Jun 16 19:55:14 2026: Removed ≈ 4% of redundant conclusions. [ 6174 of approximately 154357] (ETC: Tue Jun 16 19:58:14 2026 ; 3 min 474.85 ms remaining ; 3 min 7 s 994.27 ms total) Tue Jun 16 19:55:17 2026: Removed ≈ 6% of redundant conclusions. [ 9261 of approximately 154357] (ETC: Tue Jun 16 19:58:13 2026 ; 2 min 55 s 109.13 ms remaining ; 3 min 6 s 285.76 ms total) Tue Jun 16 19:55:21 2026: Removed ≈ 8% of redundant conclusions. [ 12348 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 2 min 49 s 482.04 ms remaining ; 3 min 4 s 218.88 ms total) Tue Jun 16 19:55:25 2026: Removed ≈ 10% of redundant conclusions. [ 15435 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 2 min 46 s 436.90 ms remaining ; 3 min 4 s 928.96 ms total) Tue Jun 16 19:55:28 2026: Removed ≈ 12% of redundant conclusions. [ 18522 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 2 min 41 s 966.94 ms remaining ; 3 min 4 s 52.20 ms total) Tue Jun 16 19:55:32 2026: Removed ≈ 14% of redundant conclusions. [ 21609 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 2 min 38 s 361.83 ms remaining ; 3 min 4 s 140.31 ms total) Tue Jun 16 19:55:36 2026: Removed ≈ 16% of redundant conclusions. [ 24697 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 2 min 35 s 163.02 ms remaining ; 3 min 4 s 717.71 ms total) Tue Jun 16 19:55:40 2026: Removed ≈ 18% of redundant conclusions. [ 27784 of approximately 154357] (ETC: Tue Jun 16 19:58:13 2026 ; 2 min 33 s 377.85 ms remaining ; 3 min 7 s 45.78 ms total) Tue Jun 16 19:55:44 2026: Removed ≈ 20% of redundant conclusions. [ 30871 of approximately 154357] (ETC: Tue Jun 16 19:58:13 2026 ; 2 min 29 s 110.94 ms remaining ; 3 min 6 s 388.08 ms total) Tue Jun 16 19:55:47 2026: Removed ≈ 22% of redundant conclusions. [ 33958 of approximately 154357] (ETC: Tue Jun 16 19:58:13 2026 ; 2 min 25 s 300.45 ms remaining ; 3 min 6 s 281.80 ms total) Tue Jun 16 19:55:51 2026: Removed ≈ 24% of redundant conclusions. [ 37045 of approximately 154357] (ETC: Tue Jun 16 19:58:12 2026 ; 2 min 20 s 905.96 ms remaining ; 3 min 5 s 401.51 ms total) Tue Jun 16 19:55:54 2026: Removed ≈ 26% of redundant conclusions. [ 40132 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 2 min 16 s 484.65 ms remaining ; 3 min 4 s 437.39 ms total) Tue Jun 16 19:55:58 2026: Removed ≈ 28% of redundant conclusions. [ 43219 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 2 min 12 s 347.65 ms remaining ; 3 min 3 s 814.59 ms total) Tue Jun 16 19:56:01 2026: Removed ≈ 30% of redundant conclusions. [ 46307 of approximately 154357] (ETC: Tue Jun 16 19:58:09 2026 ; 2 min 8 s 79.72 ms remaining ; 3 min 2 s 970.86 ms total) Tue Jun 16 19:56:05 2026: Removed ≈ 32% of redundant conclusions. [ 49394 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 2 min 4 s 609.52 ms remaining ; 3 min 3 s 248.87 ms total) Tue Jun 16 19:56:09 2026: Removed ≈ 34% of redundant conclusions. [ 52481 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 2 min 1 s 706.47 ms remaining ; 3 min 4 s 403.06 ms total) Tue Jun 16 19:56:13 2026: Removed ≈ 36% of redundant conclusions. [ 55568 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 57 s 996.03 ms remaining ; 3 min 4 s 367.83 ms total) Tue Jun 16 19:56:16 2026: Removed ≈ 38% of redundant conclusions. [ 58655 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 54 s 305.61 ms remaining ; 3 min 4 s 362.62 ms total) Tue Jun 16 19:56:20 2026: Removed ≈ 40% of redundant conclusions. [ 61742 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 50 s 885.74 ms remaining ; 3 min 4 s 807.96 ms total) Tue Jun 16 19:56:24 2026: Removed ≈ 42% of redundant conclusions. [ 64829 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 46 s 785.40 ms remaining ; 3 min 4 s 110.82 ms total) Tue Jun 16 19:56:27 2026: Removed ≈ 44% of redundant conclusions. [ 67917 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 43 s 256.12 ms remaining ; 3 min 4 s 385.76 ms total) Tue Jun 16 19:56:31 2026: Removed ≈ 46% of redundant conclusions. [ 71004 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 39 s 333.38 ms remaining ; 3 min 3 s 950.22 ms total) Tue Jun 16 19:56:35 2026: Removed ≈ 48% of redundant conclusions. [ 74091 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 35 s 702.62 ms remaining ; 3 min 4 s 42.67 ms total) Tue Jun 16 19:56:39 2026: Removed ≈ 50% of redundant conclusions. [ 77178 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 32 s 257.47 ms remaining ; 3 min 4 s 513.75 ms total) Tue Jun 16 19:56:42 2026: Removed ≈ 52% of redundant conclusions. [ 80265 of approximately 154357] (ETC: Tue Jun 16 19:58:11 2026 ; 1 min 28 s 605.31 ms remaining ; 3 min 4 s 592.80 ms total) Tue Jun 16 19:56:46 2026: Removed ≈ 54% of redundant conclusions. [ 83352 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 24 s 577.56 ms remaining ; 3 min 3 s 862.24 ms total) Tue Jun 16 19:56:49 2026: Removed ≈ 56% of redundant conclusions. [ 86439 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 20 s 752.86 ms remaining ; 3 min 3 s 526.74 ms total) Tue Jun 16 19:56:53 2026: Removed ≈ 58% of redundant conclusions. [ 89527 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 16 s 965.18 ms remaining ; 3 min 3 s 250.26 ms total) Tue Jun 16 19:56:56 2026: Removed ≈ 60% of redundant conclusions. [ 92614 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 13 s 381.26 ms remaining ; 3 min 3 s 452.55 ms total) Tue Jun 16 19:57:00 2026: Removed ≈ 62% of redundant conclusions. [ 95701 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 9 s 989.01 ms remaining ; 3 min 4 s 180.54 ms total) Tue Jun 16 19:57:04 2026: Removed ≈ 64% of redundant conclusions. [ 98788 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 6 s 255.37 ms remaining ; 3 min 4 s 41.11 ms total) Tue Jun 16 19:57:08 2026: Removed ≈ 66% of redundant conclusions. [101875 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 1 min 2 s 626.01 ms remaining ; 3 min 4 s 191.96 ms total) Tue Jun 16 19:57:11 2026: Removed ≈ 68% of redundant conclusions. [104962 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 58 s 852.23 ms remaining ; 3 min 3 s 910.38 ms total) Tue Jun 16 19:57:15 2026: Removed ≈ 70% of redundant conclusions. [108049 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 55 s 129.25 ms remaining ; 3 min 3 s 760.61 ms total) Tue Jun 16 19:57:19 2026: Removed ≈ 72% of redundant conclusions. [111137 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 51 s 442.12 ms remaining ; 3 min 3 s 721.68 ms total) Tue Jun 16 19:57:22 2026: Removed ≈ 74% of redundant conclusions. [114224 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 47 s 655.74 ms remaining ; 3 min 3 s 290.50 ms total) Tue Jun 16 19:57:26 2026: Removed ≈ 76% of redundant conclusions. [117311 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 44 s 31.33 ms remaining ; 3 min 3 s 462.31 ms total) Tue Jun 16 19:57:29 2026: Removed ≈ 78% of redundant conclusions. [120398 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 40 s 335.78 ms remaining ; 3 min 3 s 341.96 ms total) Tue Jun 16 19:57:33 2026: Removed ≈ 80% of redundant conclusions. [123485 of approximately 154357] (ETC: Tue Jun 16 19:58:09 2026 ; 36 s 604.48 ms remaining ; 3 min 3 s 18.86 ms total) Tue Jun 16 19:57:36 2026: Removed ≈ 82% of redundant conclusions. [126572 of approximately 154357] (ETC: Tue Jun 16 19:58:09 2026 ; 32 s 930.66 ms remaining ; 3 min 2 s 943.24 ms total) Tue Jun 16 19:57:40 2026: Removed ≈ 84% of redundant conclusions. [129659 of approximately 154357] (ETC: Tue Jun 16 19:58:09 2026 ; 29 s 307.30 ms remaining ; 3 min 3 s 164.10 ms total) Tue Jun 16 19:57:44 2026: Removed ≈ 86% of redundant conclusions. [132747 of approximately 154357] (ETC: Tue Jun 16 19:58:09 2026 ; 25 s 613.68 ms remaining ; 3 min 2 s 954.68 ms total) Tue Jun 16 19:57:48 2026: Removed ≈ 88% of redundant conclusions. [135834 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 21 s 992.16 ms remaining ; 3 min 3 s 266.38 ms total) Tue Jun 16 19:57:52 2026: Removed ≈ 90% of redundant conclusions. [138921 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 18 s 372.00 ms remaining ; 3 min 3 s 716.46 ms total) Tue Jun 16 19:57:55 2026: Removed ≈ 92% of redundant conclusions. [142008 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 14 s 700.28 ms remaining ; 3 min 3 s 746.95 ms total) Tue Jun 16 19:57:59 2026: Removed ≈ 94% of redundant conclusions. [145095 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 11 s 17.81 ms remaining ; 3 min 3 s 618.68 ms total) Tue Jun 16 19:58:03 2026: Removed ≈ 96% of redundant conclusions. [148182 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 7 s 351.23 ms remaining ; 3 min 3 s 759.32 ms total) Tue Jun 16 19:58:06 2026: Removed ≈ 98% of redundant conclusions. [151269 of approximately 154357] (ETC: Tue Jun 16 19:58:10 2026 ; 3 s 670.40 ms remaining ; 3 min 3 s 468.68 ms total) 182783.01 ms (3 min 2 s 783.00 ms) taken to detect 153674 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 }, { 151, 134627 }, { 153, 142023 }, { 155, 148062 }, { 157, 153674 } } 19.45 ms taken to filter and order new representative proofs. Found 5086 representative, 50899742 redundant, and 39260008 invalid condensed detachment proof strings. lengths up to 157 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753), (151,4292), (153,4655), (155,4868), (157,5086)} ; 5086 new representative proofs (50899742 redundant, 39260008 invalid) Tue Jun 16 19:58:09 2026: Starting to write 5086 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs157.txt. 3.85 ms taken to print and save 934779 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs157.txt. Determined the number of proof string candidates for iteration as 96143434. [most relevant: {41,117} with 2*4355928 = 8711856, i.e. ≈9.06%] Estimated removal count set to 159498, based on entry 157:153674 and last known pair (155:148062, 157:153674) with 153674/148062 ≈ 1.0379 and 153674 * (153674/148062)^1 ≈ 159498.71. Tue Jun 16 19:58:09 2026: Starting to generate D-proof representatives of length 159. Tue Jun 16 19:58:34 2026: Iterated ≈ 2% of D-proof candidates. [ 1922868 of 96143434] (ETC: Tue Jun 16 20:18:38 2026 ; 20 min 4 s 342.28 ms remaining ; 20 min 28 s 920.68 ms total) Tue Jun 16 19:59:03 2026: Iterated ≈ 4% of D-proof candidates. [ 3845737 of 96143434] (ETC: Tue Jun 16 20:20:46 2026 ; 21 min 43 s 58.65 ms remaining ; 22 min 37 s 352.75 ms total) Tue Jun 16 19:59:32 2026: Iterated ≈ 6% of D-proof candidates. [ 5768606 of 96143434] (ETC: Tue Jun 16 20:21:04 2026 ; 21 min 32 s 714.94 ms remaining ; 22 min 55 s 228.66 ms total) Tue Jun 16 20:00:01 2026: Iterated ≈ 8% of D-proof candidates. [ 7691474 of 96143434] (ETC: Tue Jun 16 20:21:31 2026 ; 21 min 30 s 109.42 ms remaining ; 23 min 22 s 292.83 ms total) Tue Jun 16 20:00:31 2026: Iterated ≈10% of D-proof candidates. [ 9614343 of 96143434] (ETC: Tue Jun 16 20:21:50 2026 ; 21 min 19 s 153.22 ms remaining ; 23 min 41 s 281.35 ms total) Tue Jun 16 20:01:02 2026: Iterated ≈12% of D-proof candidates. [11537212 of 96143434] (ETC: Tue Jun 16 20:22:14 2026 ; 21 min 11 s 628.74 ms remaining ; 24 min 5 s 32.66 ms total) Tue Jun 16 20:01:34 2026: Iterated ≈14% of D-proof candidates. [13460080 of 96143434] (ETC: Tue Jun 16 20:22:32 2026 ; 20 min 58 s 24.75 ms remaining ; 24 min 22 s 819.46 ms total) Tue Jun 16 20:02:08 2026: Iterated ≈16% of D-proof candidates. [15382949 of 96143434] (ETC: Tue Jun 16 20:23:04 2026 ; 20 min 56 s 113.38 ms remaining ; 24 min 55 s 373.07 ms total) Tue Jun 16 20:02:42 2026: Iterated ≈18% of D-proof candidates. [17305818 of 96143434] (ETC: Tue Jun 16 20:23:25 2026 ; 20 min 43 s 314.12 ms remaining ; 25 min 16 s 236.73 ms total) Tue Jun 16 20:03:16 2026: Iterated ≈20% of D-proof candidates. [19228686 of 96143434] (ETC: Tue Jun 16 20:23:45 2026 ; 20 min 28 s 954.36 ms remaining ; 25 min 36 s 192.93 ms total) Tue Jun 16 20:03:48 2026: Iterated ≈22% of D-proof candidates. [21151555 of 96143434] (ETC: Tue Jun 16 20:23:47 2026 ; 19 min 59 s 942.67 ms remaining ; 25 min 38 s 388.02 ms total) Tue Jun 16 20:04:21 2026: Iterated ≈24% of D-proof candidates. [23074424 of 96143434] (ETC: Tue Jun 16 20:24:00 2026 ; 19 min 38 s 437.91 ms remaining ; 25 min 50 s 576.20 ms total) Tue Jun 16 20:04:55 2026: Iterated ≈26% of D-proof candidates. [24997292 of 96143434] (ETC: Tue Jun 16 20:24:09 2026 ; 19 min 14 s 565.70 ms remaining ; 26 min 223.91 ms total) Tue Jun 16 20:05:25 2026: Iterated ≈28% of D-proof candidates. [26920161 of 96143434] (ETC: Tue Jun 16 20:24:05 2026 ; 18 min 40 s 11.23 ms remaining ; 25 min 55 s 571.14 ms total) Tue Jun 16 20:06:03 2026: Iterated ≈30% of D-proof candidates. [28843030 of 96143434] (ETC: Tue Jun 16 20:24:28 2026 ; 18 min 25 s 456.57 ms remaining ; 26 min 19 s 223.67 ms total) Tue Jun 16 20:06:40 2026: Iterated ≈32% of D-proof candidates. [30765898 of 96143434] (ETC: Tue Jun 16 20:24:45 2026 ; 18 min 5 s 104.11 ms remaining ; 26 min 35 s 741.31 ms total) Tue Jun 16 20:07:17 2026: Iterated ≈34% of D-proof candidates. [32688767 of 96143434] (ETC: Tue Jun 16 20:25:00 2026 ; 17 min 43 s 540.21 ms remaining ; 26 min 51 s 424.55 ms total) Tue Jun 16 20:07:49 2026: Iterated ≈36% of D-proof candidates. [34611636 of 96143434] (ETC: Tue Jun 16 20:25:01 2026 ; 17 min 11 s 486.56 ms remaining ; 26 min 51 s 697.75 ms total) Tue Jun 16 20:08:27 2026: Iterated ≈38% of D-proof candidates. [36534504 of 96143434] (ETC: Tue Jun 16 20:25:14 2026 ; 16 min 47 s 652.31 ms remaining ; 27 min 5 s 245.63 ms total) Tue Jun 16 20:09:03 2026: Iterated ≈40% of D-proof candidates. [38457373 of 96143434] (ETC: Tue Jun 16 20:25:24 2026 ; 16 min 21 s 194.15 ms remaining ; 27 min 15 s 323.56 ms total) Tue Jun 16 20:09:36 2026: Iterated ≈42% of D-proof candidates. [40380242 of 96143434] (ETC: Tue Jun 16 20:25:25 2026 ; 15 min 48 s 967.43 ms remaining ; 27 min 16 s 150.74 ms total) Tue Jun 16 20:10:06 2026: Iterated ≈44% of D-proof candidates. [42303110 of 96143434] (ETC: Tue Jun 16 20:25:18 2026 ; 15 min 12 s 250.21 ms remaining ; 27 min 9 s 18.21 ms total) Tue Jun 16 20:10:38 2026: Iterated ≈46% of D-proof candidates. [44225979 of 96143434] (ETC: Tue Jun 16 20:25:17 2026 ; 14 min 39 s 346.40 ms remaining ; 27 min 8 s 419.25 ms total) Tue Jun 16 20:11:03 2026: Iterated ≈48% of D-proof candidates. [46148848 of 96143434] (ETC: Tue Jun 16 20:25:01 2026 ; 13 min 57 s 994.36 ms remaining ; 26 min 51 s 527.60 ms total) Tue Jun 16 20:11:22 2026: Iterated ≈50% of D-proof candidates. [48071717 of 96143434] (ETC: Tue Jun 16 20:24:35 2026 ; 13 min 12 s 996.36 ms remaining ; 26 min 25 s 992.71 ms total) Tue Jun 16 20:11:40 2026: Iterated ≈52% of D-proof candidates. [49994585 of 96143434] (ETC: Tue Jun 16 20:24:09 2026 ; 12 min 28 s 540.07 ms remaining ; 25 min 59 s 458.45 ms total) Tue Jun 16 20:12:01 2026: Iterated ≈54% of D-proof candidates. [51917454 of 96143434] (ETC: Tue Jun 16 20:23:49 2026 ; 11 min 48 s 472.05 ms remaining ; 25 min 40 s 156.62 ms total) Tue Jun 16 20:12:22 2026: Iterated ≈56% of D-proof candidates. [53840323 of 96143434] (ETC: Tue Jun 16 20:23:32 2026 ; 11 min 10 s 255.76 ms remaining ; 25 min 23 s 308.56 ms total) Tue Jun 16 20:12:41 2026: Iterated ≈58% of D-proof candidates. [55763191 of 96143434] (ETC: Tue Jun 16 20:23:13 2026 ; 10 min 31 s 548.14 ms remaining ; 25 min 3 s 686.02 ms total) Tue Jun 16 20:13:01 2026: Iterated ≈60% of D-proof candidates. [57686060 of 96143434] (ETC: Tue Jun 16 20:22:56 2026 ; 9 min 54 s 711.36 ms remaining ; 24 min 46 s 778.38 ms total) Tue Jun 16 20:13:22 2026: Iterated ≈62% of D-proof candidates. [59608929 of 96143434] (ETC: Tue Jun 16 20:22:41 2026 ; 9 min 19 s 396.29 ms remaining ; 24 min 32 s 95.49 ms total) Tue Jun 16 20:13:42 2026: Iterated ≈64% of D-proof candidates. [61531797 of 96143434] (ETC: Tue Jun 16 20:22:26 2026 ; 8 min 44 s 581.52 ms remaining ; 24 min 17 s 170.86 ms total) Tue Jun 16 20:14:03 2026: Iterated ≈66% of D-proof candidates. [63454666 of 96143434] (ETC: Tue Jun 16 20:22:14 2026 ; 8 min 11 s 327.08 ms remaining ; 24 min 5 s 79.63 ms total) Tue Jun 16 20:14:21 2026: Iterated ≈68% of D-proof candidates. [65377535 of 96143434] (ETC: Tue Jun 16 20:21:59 2026 ; 7 min 37 s 532.52 ms remaining ; 23 min 49 s 789.13 ms total) Tue Jun 16 20:14:40 2026: Iterated ≈70% of D-proof candidates. [67300403 of 96143434] (ETC: Tue Jun 16 20:21:45 2026 ; 7 min 4 s 709.45 ms remaining ; 23 min 35 s 698.13 ms total) Tue Jun 16 20:14:58 2026: Iterated ≈72% of D-proof candidates. [69223272 of 96143434] (ETC: Tue Jun 16 20:21:31 2026 ; 6 min 32 s 444.79 ms remaining ; 23 min 21 s 588.51 ms total) Tue Jun 16 20:15:19 2026: Iterated ≈74% of D-proof candidates. [71146141 of 96143434] (ETC: Tue Jun 16 20:21:21 2026 ; 6 min 1 s 850.40 ms remaining ; 23 min 11 s 732.31 ms total) Tue Jun 16 20:15:38 2026: Iterated ≈76% of D-proof candidates. [73069009 of 96143434] (ETC: Tue Jun 16 20:21:09 2026 ; 5 min 31 s 215.80 ms remaining ; 23 min 65.79 ms total) Tue Jun 16 20:15:55 2026: Iterated ≈78% of D-proof candidates. [74991878 of 96143434] (ETC: Tue Jun 16 20:20:55 2026 ; 5 min 531.27 ms remaining ; 22 min 46 s 51.22 ms total) Tue Jun 16 20:16:13 2026: Iterated ≈80% of D-proof candidates. [76914747 of 96143434] (ETC: Tue Jun 16 20:20:44 2026 ; 4 min 30 s 975.25 ms remaining ; 22 min 34 s 876.25 ms total) Tue Jun 16 20:16:32 2026: Iterated ≈82% of D-proof candidates. [78837615 of 96143434] (ETC: Tue Jun 16 20:20:35 2026 ; 4 min 2 s 202.99 ms remaining ; 22 min 25 s 572.10 ms total) Tue Jun 16 20:16:53 2026: Iterated ≈84% of D-proof candidates. [80760484 of 96143434] (ETC: Tue Jun 16 20:20:27 2026 ; 3 min 33 s 998.91 ms remaining ; 22 min 17 s 493.18 ms total) Tue Jun 16 20:17:11 2026: Iterated ≈86% of D-proof candidates. [82683353 of 96143434] (ETC: Tue Jun 16 20:20:17 2026 ; 3 min 5 s 875.94 ms remaining ; 22 min 7 s 685.24 ms total) Tue Jun 16 20:17:33 2026: Iterated ≈88% of D-proof candidates. [84606221 of 96143434] (ETC: Tue Jun 16 20:20:12 2026 ; 2 min 38 s 780.28 ms remaining ; 22 min 3 s 168.88 ms total) Tue Jun 16 20:17:51 2026: Iterated ≈90% of D-proof candidates. [86529090 of 96143434] (ETC: Tue Jun 16 20:20:03 2026 ; 2 min 11 s 354.63 ms remaining ; 21 min 53 s 546.25 ms total) Tue Jun 16 20:18:12 2026: Iterated ≈92% of D-proof candidates. [88451959 of 96143434] (ETC: Tue Jun 16 20:19:57 2026 ; 1 min 44 s 622.08 ms remaining ; 21 min 47 s 775.89 ms total) Tue Jun 16 20:18:30 2026: Iterated ≈94% of D-proof candidates. [90374827 of 96143434] (ETC: Tue Jun 16 20:19:48 2026 ; 1 min 17 s 956.02 ms remaining ; 21 min 39 s 266.88 ms total) Tue Jun 16 20:18:49 2026: Iterated ≈96% of D-proof candidates. [92297696 of 96143434] (ETC: Tue Jun 16 20:19:41 2026 ; 51 s 661.09 ms remaining ; 21 min 31 s 527.00 ms total) Tue Jun 16 20:19:10 2026: Iterated ≈98% of D-proof candidates. [94220565 of 96143434] (ETC: Tue Jun 16 20:19:35 2026 ; 25 s 724.03 ms remaining ; 21 min 26 s 201.12 ms total) Tue Jun 16 20:19:29 2026: Iterated 100% of D-proof candidates. [96143434 of 96143434] (ETC: Tue Jun 16 20:19:29 2026 ; 0.00 ms remaining ; 21 min 20 s 353.23 ms total) 1280339.38 ms (21 min 20 s 339.38 ms) taken to collect 166743 D-proofs of length 159. [iterated 96143434 condensed detachment proof strings] Tue Jun 16 20:19:34 2026: Removed ≈ 2% of redundant conclusions. [ 3189 of approximately 159498] (ETC: Tue Jun 16 20:22:58 2026 ; 3 min 23 s 963.30 ms remaining ; 3 min 28 s 124.53 ms total) Tue Jun 16 20:19:38 2026: Removed ≈ 4% of redundant conclusions. [ 6379 of approximately 159498] (ETC: Tue Jun 16 20:22:54 2026 ; 3 min 16 s 216.68 ms remaining ; 3 min 24 s 391.15 ms total) Tue Jun 16 20:19:42 2026: Removed ≈ 6% of redundant conclusions. [ 9569 of approximately 159498] (ETC: Tue Jun 16 20:22:52 2026 ; 3 min 10 s 128.81 ms remaining ; 3 min 22 s 263.50 ms total) Tue Jun 16 20:19:46 2026: Removed ≈ 8% of redundant conclusions. [ 12759 of approximately 159498] (ETC: Tue Jun 16 20:22:51 2026 ; 3 min 5 s 576.38 ms remaining ; 3 min 21 s 712.30 ms total) Tue Jun 16 20:19:49 2026: Removed ≈ 10% of redundant conclusions. [ 15949 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 2 min 58 s 742.18 ms remaining ; 3 min 18 s 601.31 ms total) Tue Jun 16 20:19:53 2026: Removed ≈ 12% of redundant conclusions. [ 19139 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 53 s 656.43 ms remaining ; 3 min 17 s 335.79 ms total) Tue Jun 16 20:19:57 2026: Removed ≈ 14% of redundant conclusions. [ 22329 of approximately 159498] (ETC: Tue Jun 16 20:22:46 2026 ; 2 min 49 s 227.16 ms remaining ; 3 min 16 s 774.74 ms total) Tue Jun 16 20:20:01 2026: Removed ≈ 16% of redundant conclusions. [ 25519 of approximately 159498] (ETC: Tue Jun 16 20:22:46 2026 ; 2 min 45 s 121.93 ms remaining ; 3 min 16 s 572.73 ms total) Tue Jun 16 20:20:05 2026: Removed ≈ 18% of redundant conclusions. [ 28709 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 42 s 268.91 ms remaining ; 3 min 17 s 887.95 ms total) Tue Jun 16 20:20:09 2026: Removed ≈ 20% of redundant conclusions. [ 31899 of approximately 159498] (ETC: Tue Jun 16 20:22:46 2026 ; 2 min 36 s 856.66 ms remaining ; 3 min 16 s 69.90 ms total) Tue Jun 16 20:20:13 2026: Removed ≈ 22% of redundant conclusions. [ 35089 of approximately 159498] (ETC: Tue Jun 16 20:22:46 2026 ; 2 min 33 s 108.16 ms remaining ; 3 min 16 s 291.63 ms total) Tue Jun 16 20:20:17 2026: Removed ≈ 24% of redundant conclusions. [ 38279 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 2 min 30 s 782.65 ms remaining ; 3 min 18 s 397.37 ms total) Tue Jun 16 20:20:21 2026: Removed ≈ 26% of redundant conclusions. [ 41469 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 2 min 27 s 45.86 ms remaining ; 3 min 18 s 709.82 ms total) Tue Jun 16 20:20:25 2026: Removed ≈ 28% of redundant conclusions. [ 44659 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 2 min 23 s 809.62 ms remaining ; 3 min 19 s 734.82 ms total) Tue Jun 16 20:20:29 2026: Removed ≈ 30% of redundant conclusions. [ 47849 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 18 s 439.24 ms remaining ; 3 min 17 s 769.63 ms total) Tue Jun 16 20:20:32 2026: Removed ≈ 32% of redundant conclusions. [ 51039 of approximately 159498] (ETC: Tue Jun 16 20:22:46 2026 ; 2 min 13 s 930.80 ms remaining ; 3 min 16 s 956.40 ms total) Tue Jun 16 20:20:37 2026: Removed ≈ 34% of redundant conclusions. [ 54229 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 10 s 211.08 ms remaining ; 3 min 17 s 288.92 ms total) Tue Jun 16 20:20:41 2026: Removed ≈ 36% of redundant conclusions. [ 57419 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 6 s 543.31 ms remaining ; 3 min 17 s 723.38 ms total) Tue Jun 16 20:20:44 2026: Removed ≈ 38% of redundant conclusions. [ 60609 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 2 min 2 s 475.73 ms remaining ; 3 min 17 s 541.03 ms total) Tue Jun 16 20:20:48 2026: Removed ≈ 40% of redundant conclusions. [ 63799 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 1 min 58 s 405.39 ms remaining ; 3 min 17 s 341.90 ms total) Tue Jun 16 20:20:52 2026: Removed ≈ 42% of redundant conclusions. [ 66989 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 1 min 54 s 642.65 ms remaining ; 3 min 17 s 659.40 ms total) Tue Jun 16 20:20:56 2026: Removed ≈ 44% of redundant conclusions. [ 70179 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 1 min 50 s 619.39 ms remaining ; 3 min 17 s 534.36 ms total) Tue Jun 16 20:21:00 2026: Removed ≈ 46% of redundant conclusions. [ 73369 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 1 min 46 s 860.59 ms remaining ; 3 min 17 s 889.79 ms total) Tue Jun 16 20:21:04 2026: Removed ≈ 48% of redundant conclusions. [ 76559 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 1 min 42 s 729.81 ms remaining ; 3 min 17 s 557.23 ms total) Tue Jun 16 20:21:09 2026: Removed ≈ 50% of redundant conclusions. [ 79749 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 1 min 39 s 145.67 ms remaining ; 3 min 18 s 291.34 ms total) Tue Jun 16 20:21:13 2026: Removed ≈ 52% of redundant conclusions. [ 82938 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 1 min 35 s 406.83 ms remaining ; 3 min 18 s 761.74 ms total) Tue Jun 16 20:21:17 2026: Removed ≈ 54% of redundant conclusions. [ 86128 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 31 s 861.72 ms remaining ; 3 min 19 s 696.89 ms total) Tue Jun 16 20:21:21 2026: Removed ≈ 56% of redundant conclusions. [ 89318 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 27 s 904.85 ms remaining ; 3 min 19 s 781.25 ms total) Tue Jun 16 20:21:25 2026: Removed ≈ 58% of redundant conclusions. [ 92508 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 23 s 653.21 ms remaining ; 3 min 19 s 171.82 ms total) Tue Jun 16 20:21:29 2026: Removed ≈ 60% of redundant conclusions. [ 95698 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 19 s 672.89 ms remaining ; 3 min 19 s 179.72 ms total) Tue Jun 16 20:21:33 2026: Removed ≈ 62% of redundant conclusions. [ 98888 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 15 s 730.67 ms remaining ; 3 min 19 s 288.74 ms total) Tue Jun 16 20:21:37 2026: Removed ≈ 64% of redundant conclusions. [102078 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 1 min 11 s 481.24 ms remaining ; 3 min 18 s 556.51 ms total) Tue Jun 16 20:21:41 2026: Removed ≈ 66% of redundant conclusions. [105268 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 7 s 731.10 ms remaining ; 3 min 19 s 206.62 ms total) Tue Jun 16 20:21:45 2026: Removed ≈ 68% of redundant conclusions. [108458 of approximately 159498] (ETC: Tue Jun 16 20:22:49 2026 ; 1 min 3 s 772.82 ms remaining ; 3 min 19 s 287.57 ms total) Tue Jun 16 20:21:49 2026: Removed ≈ 70% of redundant conclusions. [111648 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 59 s 701.48 ms remaining ; 3 min 19 s 2.45 ms total) Tue Jun 16 20:21:52 2026: Removed ≈ 72% of redundant conclusions. [114838 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 55 s 525.42 ms remaining ; 3 min 18 s 302.59 ms total) Tue Jun 16 20:21:56 2026: Removed ≈ 74% of redundant conclusions. [118028 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 51 s 479.60 ms remaining ; 3 min 17 s 995.98 ms total) Tue Jun 16 20:22:00 2026: Removed ≈ 76% of redundant conclusions. [121218 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 47 s 441.71 ms remaining ; 3 min 17 s 671.30 ms total) Tue Jun 16 20:22:04 2026: Removed ≈ 78% of redundant conclusions. [124408 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 43 s 509.03 ms remaining ; 3 min 17 s 765.86 ms total) Tue Jun 16 20:22:07 2026: Removed ≈ 80% of redundant conclusions. [127598 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 39 s 494.88 ms remaining ; 3 min 17 s 471.91 ms total) Tue Jun 16 20:22:12 2026: Removed ≈ 82% of redundant conclusions. [130788 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 35 s 591.87 ms remaining ; 3 min 17 s 730.15 ms total) Tue Jun 16 20:22:16 2026: Removed ≈ 84% of redundant conclusions. [133978 of approximately 159498] (ETC: Tue Jun 16 20:22:47 2026 ; 31 s 659.81 ms remaining ; 3 min 17 s 871.31 ms total) Tue Jun 16 20:22:20 2026: Removed ≈ 86% of redundant conclusions. [137168 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 27 s 746.74 ms remaining ; 3 min 18 s 188.48 ms total) Tue Jun 16 20:22:24 2026: Removed ≈ 88% of redundant conclusions. [140358 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 23 s 792.38 ms remaining ; 3 min 18 s 267.36 ms total) Tue Jun 16 20:22:28 2026: Removed ≈ 90% of redundant conclusions. [143548 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 19 s 850.97 ms remaining ; 3 min 18 s 507.19 ms total) Tue Jun 16 20:22:32 2026: Removed ≈ 92% of redundant conclusions. [146738 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 15 s 883.04 ms remaining ; 3 min 18 s 535.48 ms total) Tue Jun 16 20:22:36 2026: Removed ≈ 94% of redundant conclusions. [149928 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 11 s 911.22 ms remaining ; 3 min 18 s 517.90 ms total) Tue Jun 16 20:22:40 2026: Removed ≈ 96% of redundant conclusions. [153118 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 7 s 934.31 ms remaining ; 3 min 18 s 355.20 ms total) Tue Jun 16 20:22:44 2026: Removed ≈ 98% of redundant conclusions. [156308 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 3 s 963.36 ms remaining ; 3 min 18 s 165.47 ms total) Tue Jun 16 20:22:48 2026: Removed ≈100% of redundant conclusions. [159498 of approximately 159498] (ETC: Tue Jun 16 20:22:48 2026 ; 0.00 ms remaining ; 3 min 18 s 556.36 ms total) 201551.65 ms (3 min 21 s 551.65 ms) taken to detect 161569 conclusions for which there are more general variants proven in lower or equal amounts of steps. [Copy] Custom removal counts: { { 143, 107139 }, { 145, 113100 }, { 147, 120397 }, { 149, 127004 }, { 151, 134627 }, { 153, 142023 }, { 155, 148062 }, { 157, 153674 }, { 159, 161569 } } 21.40 ms taken to filter and order new representative proofs. Found 5174 representative, 54276863 redundant, and 41861397 invalid condensed detachment proof strings. lengths up to 159 ; amounts per length: {(1,2), (3,1), (5,1), (7,3), (9,8), (11,15), (13,22), (15,32), (17,41), (19,63), (21,90), (23,113), (25,165), (27,195), (29,264), (31,344), (33,439), (35,592), (37,704), (39,980), (41,1212), (43,168), (45,168), (47,198), (49,236), (51,249), (53,298), (55,345), (57,376), (59,450), (61,522), (63,630), (65,754), (67,792), (69,987), (71,1126), (73,1214), (75,1273), (77,1355), (79,1462), (81,1572), (83,1602), (85,1807), (87,1854), (89,2002), (91,2382), (93,2568), (95,2726), (97,2470), (99,2405), (101,2583), (103,2727), (105,2949), (107,3154), (109,3362), (111,3530), (113,3723), (115,3800), (117,3594), (119,3809), (121,4112), (123,4394), (125,4453), (127,4805), (129,4819), (131,4998), (133,5230), (135,5409), (137,5737), (139,5906), (141,6242), (143,3123), (145,2900), (147,3189), (149,3753), (151,4292), (153,4655), (155,4868), (157,5086), (159,5174)} ; 5174 new representative proofs (54276863 redundant, 41861397 invalid) Tue Jun 16 20:22:51 2026: Starting to write 5174 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs159.txt. 4.96 ms taken to print and save 961362 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/extraction-l21/dProofs-withConclusions/dProofs159.txt. Determined the number of proof string candidates for iteration as 103368768. [most relevant: {41,119} with 2*4616508 = 9233016, i.e. ≈8.93%] Estimated removal count set to 169869, based on entry 159:161569 and last known pair (157:153674, 159:161569) with 161569/153674 ≈ 1.05137 and 161569 * (161569/153674)^1 ≈ 169869.61. Tue Jun 16 20:22:51 2026: Starting to generate D-proof representatives of length 161. Tue Jun 16 20:23:17 2026: Iterated ≈ 2% of D-proof candidates. [ 2067375 of 103368768] (ETC: Tue Jun 16 20:44:41 2026 ; 21 min 23 s 824.63 ms remaining ; 21 min 50 s 25.13 ms total) Tue Jun 16 20:23:44 2026: Iterated ≈ 4% of D-proof candidates. [ 4134750 of 103368768] (ETC: Tue Jun 16 20:44:56 2026 ; 21 min 12 s 313.00 ms remaining ; 22 min 5 s 326.03 ms total) Tue Jun 16 20:24:14 2026: Iterated ≈ 6% of D-proof candidates. [ 6202126 of 103368768] (ETC: Tue Jun 16 20:45:58 2026 ; 21 min 43 s 525.56 ms remaining ; 23 min 6 s 729.32 ms total) Tue Jun 16 20:24:50 2026: Iterated ≈ 8% of D-proof candidates. [ 8269501 of 103368768] (ETC: Tue Jun 16 20:47:43 2026 ; 22 min 52 s 672.59 ms remaining ; 24 min 52 s 35.42 ms total) Tue Jun 16 20:25:27 2026: Iterated ≈10% of D-proof candidates. [ 10336876 of 103368768] (ETC: Tue Jun 16 20:48:51 2026 ; 23 min 23 s 954.42 ms remaining ; 25 min 59 s 949.34 ms total) [Aborted after finding a proof of A3_{C-O}:CCCpOCqOCqp at dProofs155.txt:1350. Going to continue searching for A2:CCpCqrCCpqCpr based on CCCpqrCCrpCsp alone.]