( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'. The run was executed on a CLAIX-2018 MPI node — 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory — running Linux, Rocky 8.8. Wall-clock time: 2.53888… h CPU utilization: 121.8666… core-h ) Fri Oct 6 08:19:48 2023: Process started. [pid: 13008, tid:23334345246592] Tasks: 1. resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true) 2. generateDProofRepresentativeFiles(141, false, true) [Main] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c] (1) CC0CCN0.1.2C3CCN4C2.4C0.4 - CCpCCNpqrCsCCNtCrtCpt - (0\imply((\not0\imply1)\imply2))\imply(3\imply((\not4\imply(2\imply4))\imply(0\imply4))) [Main] Calling generateDProofRepresentativeFiles(141, false, true). Fri Oct 6 08:19:48 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 141, unfiltered] 0.03 ms taken to load initial representatives. 0.07 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23334280795904] 5.84 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23334274492160] 0.85 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23334154663680] 1.63 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23334251378432] 3.25 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23334266087168] 2.22 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23334272390912] 2.39 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23334276593408] 2.42 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23334261884672] 0.20 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23334282897152] 0.34 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23334236669696] 0.07 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23334270289664] 0.25 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23334242973440] 0.21 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23334020445952] 0.23 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23334268188416] 0.27 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23334249277184] 0.26 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23334234568448] 0.57 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23334245074688] 1.19 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23334230365952] 0.08 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23334259783424] 0.73 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23334278694656] 0.39 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23334263985920] 4.53 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23334284998400] 1153.51 ms (1 s 153.51 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23334282897152] 977.92 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23334154663680] 2313.27 ms (2 s 313.27 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23334020445952] 400.73 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23334280795904] 6114.70 ms (6 s 114.70 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23334278694656] 5466.80 ms (5 s 466.81 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23334276593408] 686.00 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23334274492160] 3335.55 ms (3 s 335.55 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23334272390912] 1459.57 ms (1 s 459.56 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23334270289664] 2699.19 ms (2 s 699.19 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23334268188416] 2048.98 ms (2 s 48.98 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23334266087168] 6902.88 ms (6 s 902.88 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23334263985920] 8816.37 ms (8 s 816.37 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23334261884672] 5390.29 ms (5 s 390.29 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23334259783424] 2.25 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23334257682176] 5.18 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23334255580928] 3.66 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23334253479680] 1447.52 ms (1 s 447.52 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23334251378432] 3287.05 ms (3 s 287.05 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23334249277184] 8.34 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23334247175936] 4198.10 ms (4 s 198.10 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23334245074688] 1909.10 ms (1 s 909.10 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23334242973440] 14.32 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23334240872192] 6.72 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23334238770944] 1248.35 ms (1 s 248.35 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23334236669696] 3729.73 ms (3 s 729.73 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23334234568448] 6.64 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23334232467200] 4832.09 ms (4 s 832.09 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23334230365952] 13.21 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23334228264704] 10.66 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23334226163456] 11.78 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23334224062208] 21.92 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23334152562432] 29.92 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23334150461184] 24.00 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23334148359936] 20.02 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23334146258688] 25.13 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23334144157440] 23.05 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23334142056192] 29.49 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23334139954944] 31.39 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23334137853696] 47.09 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23334135752448] 35.58 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23334133651200] 69.70 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23334131549952] 52.92 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23334129448704] 72.89 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23334127347456] 120.41 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23334125246208] 218.18 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23334123144960] 274.57 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23334121043712] 8876.39 ms (8 s 876.38 ms) total read duration. Loaded 70 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 2 9 : 1 11 : 0 13 : 1 15 : 2 17 : 3 19 : 4 21 : 5 23 : 5 25 : 5 27 : 6 29 : 7 31 : 15 33 : 20 35 : 25 37 : 30 39 : 37 41 : 42 43 : 51 45 : 63 47 : 85 49 : 122 51 : 162 53 : 206 55 : 251 57 : 292 59 : 339 61 : 444 63 : 598 65 : 781 67 : 1016 69 : 1303 71 : 1593 73 : 1922 75 : 2359 77 : 2986 79 : 3875 81 : 5006 83 : 6466 85 : 8184 87 : 10182 89 : 12488 91 : 15534 93 : 19614 95 : 25087 97 : 32452 99 : 41840 101 : 53343 103 : 67105 105 : 84222 107 : 105925 109 : 134564 111 : 172053 113 : 221055 115 : 283569 117 : 361751 119 : 458509 121 : 579502 123 : 734352 125 : 935212 127 : 1197027 129 : 1534565 131 : 1965596 133 : 2509883 135 : 3196594 137 : 4066027 139 : 5180139 24036508 representatives in total. Fri Oct 6 08:19:57 2023: Inserted ≈ 5% of D-proof conclusions. [ 1201825 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 7 s 689.59 ms remaining ; 8 s 94.30 ms total) Fri Oct 6 08:19:57 2023: Inserted ≈10% of D-proof conclusions. [ 2403650 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 7 s 511.54 ms remaining ; 8 s 346.15 ms total) Fri Oct 6 08:19:58 2023: Inserted ≈15% of D-proof conclusions. [ 3605476 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 6 s 856.00 ms remaining ; 8 s 65.88 ms total) Fri Oct 6 08:19:58 2023: Inserted ≈20% of D-proof conclusions. [ 4807301 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 6 s 795.53 ms remaining ; 8 s 494.42 ms total) Fri Oct 6 08:19:59 2023: Inserted ≈25% of D-proof conclusions. [ 6009127 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 6 s 282.34 ms remaining ; 8 s 376.45 ms total) Fri Oct 6 08:19:59 2023: Inserted ≈30% of D-proof conclusions. [ 7210952 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 5 s 844.49 ms remaining ; 8 s 349.27 ms total) Fri Oct 6 08:20:00 2023: Inserted ≈35% of D-proof conclusions. [ 8412777 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 5 s 447.63 ms remaining ; 8 s 380.98 ms total) Fri Oct 6 08:20:00 2023: Inserted ≈40% of D-proof conclusions. [ 9614603 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 5 s 153.06 ms remaining ; 8 s 588.43 ms total) Fri Oct 6 08:20:01 2023: Inserted ≈45% of D-proof conclusions. [10816428 of 24036508] (ETC: Fri Oct 6 08:20:05 2023 ; 4 s 802.59 ms remaining ; 8 s 731.99 ms total) Fri Oct 6 08:20:01 2023: Inserted ≈50% of D-proof conclusions. [12018254 of 24036508] (ETC: Fri Oct 6 08:20:06 2023 ; 4 s 533.79 ms remaining ; 9 s 67.59 ms total) Fri Oct 6 08:20:02 2023: Inserted ≈55% of D-proof conclusions. [13220079 of 24036508] (ETC: Fri Oct 6 08:20:06 2023 ; 4 s 195.24 ms remaining ; 9 s 322.76 ms total) Fri Oct 6 08:20:02 2023: Inserted ≈60% of D-proof conclusions. [14421904 of 24036508] (ETC: Fri Oct 6 08:20:06 2023 ; 3 s 862.33 ms remaining ; 9 s 655.83 ms total) Fri Oct 6 08:20:03 2023: Inserted ≈65% of D-proof conclusions. [15623730 of 24036508] (ETC: Fri Oct 6 08:20:07 2023 ; 3 s 497.94 ms remaining ; 9 s 994.11 ms total) Fri Oct 6 08:20:04 2023: Inserted ≈70% of D-proof conclusions. [16825555 of 24036508] (ETC: Fri Oct 6 08:20:07 2023 ; 3 s 154.24 ms remaining ; 10 s 514.15 ms total) Fri Oct 6 08:20:05 2023: Inserted ≈75% of D-proof conclusions. [18027381 of 24036508] (ETC: Fri Oct 6 08:20:08 2023 ; 2 s 811.30 ms remaining ; 11 s 245.20 ms total) Fri Oct 6 08:20:06 2023: Inserted ≈80% of D-proof conclusions. [19229206 of 24036508] (ETC: Fri Oct 6 08:20:08 2023 ; 2 s 292.97 ms remaining ; 11 s 464.83 ms total) Fri Oct 6 08:20:07 2023: Inserted ≈85% of D-proof conclusions. [20431031 of 24036508] (ETC: Fri Oct 6 08:20:08 2023 ; 1 s 750.99 ms remaining ; 11 s 673.27 ms total) Fri Oct 6 08:20:07 2023: Inserted ≈90% of D-proof conclusions. [21632857 of 24036508] (ETC: Fri Oct 6 08:20:08 2023 ; 1 s 181.91 ms remaining ; 11 s 819.16 ms total) Fri Oct 6 08:20:08 2023: Inserted ≈95% of D-proof conclusions. [22834682 of 24036508] (ETC: Fri Oct 6 08:20:09 2023 ; 602.96 ms remaining ; 12 s 59.24 ms total) Fri Oct 6 08:20:09 2023: Inserted 100% of D-proof conclusions. [24036508 of 24036508] (ETC: Fri Oct 6 08:20:09 2023 ; 0.00 ms remaining ; 12 s 317.57 ms total) 12317.84 ms (12 s 317.84 ms) total insertion duration. Estimated iteration count set to 152491875, based on entry 139:118581507 and last known pair (137:92211954, 139:118581507) with 118581507/92211954 ≈ 1.28597 and 118581507 * (118581507/92211954)^1 ≈ 152491875.43. Fri Oct 6 08:20:09 2023: Starting to generate D-proof representatives of length 141. Fri Oct 6 08:23:53 2023: Iterated ≈ 2% of D-proof candidates. [ 3049837 of approximately 152491875] (ETC: Fri Oct 6 11:27:16 2023 ; 3 h 3 min 22 s 813.32 ms remaining ; 3 h 7 min 7 s 360.49 ms total) Fri Oct 6 08:27:22 2023: Iterated ≈ 4% of D-proof candidates. [ 6099675 of approximately 152491875] (ETC: Fri Oct 6 11:20:28 2023 ; 2 h 53 min 6 s 356.98 ms remaining ; 3 h 19 s 121.85 ms total) Fri Oct 6 08:30:44 2023: Iterated ≈ 6% of D-proof candidates. [ 9149512 of approximately 152491875] (ETC: Fri Oct 6 11:16:29 2023 ; 2 h 45 min 44 s 828.89 ms remaining ; 2 h 56 min 19 s 605.16 ms total) Fri Oct 6 08:34:03 2023: Iterated ≈ 8% of D-proof candidates. [ 12199350 of approximately 152491875] (ETC: Fri Oct 6 11:13:49 2023 ; 2 h 39 min 46 s 628.76 ms remaining ; 2 h 53 min 40 s 248.65 ms total) Fri Oct 6 08:37:14 2023: Iterated ≈ 10% of D-proof candidates. [ 15249187 of approximately 152491875] (ETC: Fri Oct 6 11:10:56 2023 ; 2 h 33 min 42 s 801.36 ms remaining ; 2 h 50 min 47 s 557.03 ms total) Fri Oct 6 08:40:22 2023: Iterated ≈ 12% of D-proof candidates. [ 18299025 of approximately 152491875] (ETC: Fri Oct 6 11:08:37 2023 ; 2 h 28 min 15 s 121.85 ms remaining ; 2 h 48 min 28 s 93.02 ms total) Fri Oct 6 08:43:35 2023: Iterated ≈ 14% of D-proof candidates. [ 21348862 of approximately 152491875] (ETC: Fri Oct 6 11:07:30 2023 ; 2 h 23 min 55 s 193.15 ms remaining ; 2 h 47 min 20 s 922.23 ms total) Fri Oct 6 08:46:44 2023: Iterated ≈ 16% of D-proof candidates. [ 24398700 of approximately 152491875] (ETC: Fri Oct 6 11:06:21 2023 ; 2 h 19 min 36 s 529.94 ms remaining ; 2 h 46 min 12 s 59.46 ms total) Fri Oct 6 08:50:08 2023: Iterated ≈ 18% of D-proof candidates. [ 27448537 of approximately 152491875] (ETC: Fri Oct 6 11:06:41 2023 ; 2 h 16 min 33 s 852.68 ms remaining ; 2 h 46 min 32 s 503.23 ms total) Fri Oct 6 08:53:04 2023: Iterated ≈ 20% of D-proof candidates. [ 30498375 of approximately 152491875] (ETC: Fri Oct 6 11:04:47 2023 ; 2 h 11 min 42 s 127.55 ms remaining ; 2 h 44 min 37 s 659.44 ms total) Fri Oct 6 08:56:11 2023: Iterated ≈ 22% of D-proof candidates. [ 33548212 of approximately 152491875] (ETC: Fri Oct 6 11:03:56 2023 ; 2 h 7 min 45 s 452.49 ms remaining ; 2 h 43 min 47 s 503.16 ms total) Fri Oct 6 08:59:20 2023: Iterated ≈ 24% of D-proof candidates. [ 36598050 of approximately 152491875] (ETC: Fri Oct 6 11:03:26 2023 ; 2 h 4 min 6 s 159.67 ms remaining ; 2 h 43 min 17 s 578.52 ms total) Fri Oct 6 09:02:33 2023: Iterated ≈ 26% of D-proof candidates. [ 39647887 of approximately 152491875] (ETC: Fri Oct 6 11:03:16 2023 ; 2 h 42 s 196.25 ms remaining ; 2 h 43 min 6 s 751.65 ms total) Fri Oct 6 09:05:29 2023: Iterated ≈ 28% of D-proof candidates. [ 42697725 of approximately 152491875] (ETC: Fri Oct 6 11:02:05 2023 ; 1 h 56 min 35 s 679.90 ms remaining ; 2 h 41 min 56 s 222.08 ms total) Fri Oct 6 09:08:29 2023: Iterated ≈ 30% of D-proof candidates. [ 45747562 of approximately 152491875] (ETC: Fri Oct 6 11:01:16 2023 ; 1 h 52 min 47 s 66.09 ms remaining ; 2 h 41 min 7 s 237.22 ms total) Fri Oct 6 09:11:26 2023: Iterated ≈ 32% of D-proof candidates. [ 48797400 of approximately 152491875] (ETC: Fri Oct 6 11:00:26 2023 ; 1 h 48 min 59 s 706.28 ms remaining ; 2 h 40 min 17 s 215.12 ms total) Fri Oct 6 09:14:28 2023: Iterated ≈ 34% of D-proof candidates. [ 51847237 of approximately 152491875] (ETC: Fri Oct 6 10:59:55 2023 ; 1 h 45 min 27 s 104.06 ms remaining ; 2 h 39 min 46 s 521.26 ms total) Fri Oct 6 09:17:29 2023: Iterated ≈ 36% of D-proof candidates. [ 54897075 of approximately 152491875] (ETC: Fri Oct 6 10:59:23 2023 ; 1 h 41 min 54 s 877.99 ms remaining ; 2 h 39 min 14 s 496.85 ms total) Fri Oct 6 09:20:29 2023: Iterated ≈ 38% of D-proof candidates. [ 57946912 of approximately 152491875] (ETC: Fri Oct 6 10:58:55 2023 ; 1 h 38 min 26 s 436.18 ms remaining ; 2 h 38 min 46 s 509.91 ms total) Fri Oct 6 09:23:27 2023: Iterated ≈ 40% of D-proof candidates. [ 60996750 of approximately 152491875] (ETC: Fri Oct 6 10:58:25 2023 ; 1 h 34 min 57 s 496.31 ms remaining ; 2 h 38 min 15 s 827.19 ms total) Fri Oct 6 09:26:24 2023: Iterated ≈ 42% of D-proof candidates. [ 64046587 of approximately 152491875] (ETC: Fri Oct 6 10:57:55 2023 ; 1 h 31 min 30 s 73.11 ms remaining ; 2 h 37 min 45 s 643.23 ms total) Fri Oct 6 09:29:17 2023: Iterated ≈ 44% of D-proof candidates. [ 67096425 of approximately 152491875] (ETC: Fri Oct 6 10:57:17 2023 ; 1 h 27 min 59 s 586.69 ms remaining ; 2 h 37 min 7 s 833.37 ms total) Fri Oct 6 09:32:09 2023: Iterated ≈ 46% of D-proof candidates. [ 70146262 of approximately 152491875] (ETC: Fri Oct 6 10:56:41 2023 ; 1 h 24 min 31 s 904.20 ms remaining ; 2 h 36 min 32 s 415.13 ms total) Fri Oct 6 09:35:04 2023: Iterated ≈ 48% of D-proof candidates. [ 73196100 of approximately 152491875] (ETC: Fri Oct 6 10:56:14 2023 ; 1 h 21 min 9 s 968.13 ms remaining ; 2 h 36 min 5 s 323.33 ms total) Fri Oct 6 09:37:59 2023: Iterated ≈ 50% of D-proof candidates. [ 76245937 of approximately 152491875] (ETC: Fri Oct 6 10:55:49 2023 ; 1 h 17 min 49 s 847.72 ms remaining ; 2 h 35 min 39 s 695.37 ms total) Fri Oct 6 09:40:51 2023: Iterated ≈ 52% of D-proof candidates. [ 79295775 of approximately 152491875] (ETC: Fri Oct 6 10:55:20 2023 ; 1 h 14 min 29 s 227.83 ms remaining ; 2 h 35 min 10 s 891.32 ms total) Fri Oct 6 09:43:44 2023: Iterated ≈ 54% of D-proof candidates. [ 82345612 of approximately 152491875] (ETC: Fri Oct 6 10:54:57 2023 ; 1 h 11 min 12 s 398.00 ms remaining ; 2 h 34 min 47 s 821.67 ms total) Fri Oct 6 09:46:37 2023: Iterated ≈ 56% of D-proof candidates. [ 85395450 of approximately 152491875] (ETC: Fri Oct 6 10:54:33 2023 ; 1 h 7 min 56 s 10.11 ms remaining ; 2 h 34 min 23 s 659.33 ms total) Fri Oct 6 09:49:30 2023: Iterated ≈ 58% of D-proof candidates. [ 88445287 of approximately 152491875] (ETC: Fri Oct 6 10:54:12 2023 ; 1 h 4 min 42 s 55.41 ms remaining ; 2 h 34 min 2 s 989.01 ms total) Fri Oct 6 09:52:21 2023: Iterated ≈ 60% of D-proof candidates. [ 91495125 of approximately 152491875] (ETC: Fri Oct 6 10:53:49 2023 ; 1 h 1 min 28 s 195.17 ms remaining ; 2 h 33 min 40 s 487.93 ms total) Fri Oct 6 09:55:15 2023: Iterated ≈ 62% of D-proof candidates. [ 94544962 of approximately 152491875] (ETC: Fri Oct 6 10:53:33 2023 ; 58 min 17 s 434.30 ms remaining ; 2 h 33 min 23 s 774.38 ms total) Fri Oct 6 09:58:09 2023: Iterated ≈ 64% of D-proof candidates. [ 97594800 of approximately 152491875] (ETC: Fri Oct 6 10:53:17 2023 ; 55 min 7 s 587.20 ms remaining ; 2 h 33 min 7 s 742.22 ms total) Fri Oct 6 10:01:02 2023: Iterated ≈ 66% of D-proof candidates. [100644637 of approximately 152491875] (ETC: Fri Oct 6 10:53:01 2023 ; 51 min 58 s 480.43 ms remaining ; 2 h 32 min 52 s 1.18 ms total) Fri Oct 6 10:03:55 2023: Iterated ≈ 68% of D-proof candidates. [103694475 of approximately 152491875] (ETC: Fri Oct 6 10:52:45 2023 ; 48 min 50 s 102.24 ms remaining ; 2 h 32 min 36 s 569.50 ms total) Fri Oct 6 10:06:47 2023: Iterated ≈ 70% of D-proof candidates. [106744312 of approximately 152491875] (ETC: Fri Oct 6 10:52:29 2023 ; 45 min 42 s 106.56 ms remaining ; 2 h 32 min 20 s 355.11 ms total) Fri Oct 6 10:09:38 2023: Iterated ≈ 72% of D-proof candidates. [109794150 of approximately 152491875] (ETC: Fri Oct 6 10:52:12 2023 ; 42 min 34 s 530.37 ms remaining ; 2 h 32 min 3 s 322.73 ms total) Fri Oct 6 10:12:27 2023: Iterated ≈ 74% of D-proof candidates. [112843987 of approximately 152491875] (ETC: Fri Oct 6 10:51:54 2023 ; 39 min 27 s 413.45 ms remaining ; 2 h 31 min 45 s 436.25 ms total) Fri Oct 6 10:15:14 2023: Iterated ≈ 76% of D-proof candidates. [115893825 of approximately 152491875] (ETC: Fri Oct 6 10:51:34 2023 ; 36 min 20 s 454.99 ms remaining ; 2 h 31 min 25 s 229.12 ms total) Fri Oct 6 10:18:01 2023: Iterated ≈ 78% of D-proof candidates. [118943662 of approximately 152491875] (ETC: Fri Oct 6 10:51:16 2023 ; 33 min 14 s 787.83 ms remaining ; 2 h 31 min 7 s 217.25 ms total) Fri Oct 6 10:20:47 2023: Iterated ≈ 80% of D-proof candidates. [121993500 of approximately 152491875] (ETC: Fri Oct 6 10:50:57 2023 ; 30 min 9 s 572.94 ms remaining ; 2 h 30 min 47 s 864.69 ms total) Fri Oct 6 10:23:35 2023: Iterated ≈ 82% of D-proof candidates. [125043337 of approximately 152491875] (ETC: Fri Oct 6 10:50:41 2023 ; 27 min 5 s 687.55 ms remaining ; 2 h 30 min 31 s 597.36 ms total) Fri Oct 6 10:26:24 2023: Iterated ≈ 84% of D-proof candidates. [128093175 of approximately 152491875] (ETC: Fri Oct 6 10:50:27 2023 ; 24 min 2 s 843.51 ms remaining ; 2 h 30 min 17 s 771.97 ms total) Fri Oct 6 10:29:11 2023: Iterated ≈ 86% of D-proof candidates. [131143012 of approximately 152491875] (ETC: Fri Oct 6 10:50:12 2023 ; 21 min 391.80 ms remaining ; 2 h 30 min 2 s 798.34 ms total) Fri Oct 6 10:31:59 2023: Iterated ≈ 88% of D-proof candidates. [134192850 of approximately 152491875] (ETC: Fri Oct 6 10:49:57 2023 ; 17 min 58 s 602.53 ms remaining ; 2 h 29 min 48 s 354.46 ms total) Fri Oct 6 10:34:46 2023: Iterated ≈ 90% of D-proof candidates. [137242687 of approximately 152491875] (ETC: Fri Oct 6 10:49:44 2023 ; 14 min 57 s 508.74 ms remaining ; 2 h 29 min 35 s 87.13 ms total) Fri Oct 6 10:37:34 2023: Iterated ≈ 92% of D-proof candidates. [140292525 of approximately 152491875] (ETC: Fri Oct 6 10:49:31 2023 ; 11 min 56 s 973.26 ms remaining ; 2 h 29 min 22 s 165.78 ms total) Fri Oct 6 10:40:21 2023: Iterated ≈ 94% of D-proof candidates. [143342362 of approximately 152491875] (ETC: Fri Oct 6 10:49:18 2023 ; 8 min 56 s 959.53 ms remaining ; 2 h 29 min 9 s 324.99 ms total) Fri Oct 6 10:43:08 2023: Iterated ≈ 96% of D-proof candidates. [146392200 of approximately 152491875] (ETC: Fri Oct 6 10:49:05 2023 ; 5 min 57 s 442.14 ms remaining ; 2 h 28 min 56 s 53.48 ms total) Fri Oct 6 10:45:55 2023: Iterated ≈ 98% of D-proof candidates. [149442037 of approximately 152491875] (ETC: Fri Oct 6 10:48:54 2023 ; 2 min 58 s 498.62 ms remaining ; 2 h 28 min 44 s 929.41 ms total) 8906410.57 ms (2 h 28 min 26 s 410.57 ms) taken to collect 16952082 D-proofs of length 141. [iterated 152368710 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 8 }, { 11, 10 }, { 13, 10 }, { 15, 10 }, { 17, 10 }, { 19, 15 }, { 21, 26 }, { 23, 40 }, { 25, 52 }, { 27, 63 }, { 29, 74 }, { 31, 86 }, { 33, 118 }, { 35, 167 }, { 37, 244 }, { 39, 340 }, { 41, 446 }, { 43, 551 }, { 45, 688 }, { 47, 869 }, { 49, 1128 }, { 51, 1509 }, { 53, 2046 }, { 55, 2758 }, { 57, 3636 }, { 59, 4659 }, { 61, 5848 }, { 63, 7415 }, { 65, 9546 }, { 67, 12520 }, { 69, 16626 }, { 71, 21997 }, { 73, 28576 }, { 75, 36634 }, { 77, 46614 }, { 79, 59337 }, { 81, 76266 }, { 83, 99080 }, { 85, 129482 }, { 87, 168717 }, { 89, 218196 }, { 91, 279663 }, { 93, 357074 }, { 95, 456119 }, { 97, 585294 }, { 99, 755798 }, { 101, 979916 }, { 103, 1269838 }, { 105, 1639296 }, { 107, 2106748 }, { 109, 2698758 }, { 111, 3457865 }, { 113, 4441498 }, { 115, 5724404 }, { 117, 7393098 }, { 119, 9547567 }, { 121, 12303220 }, { 123, 15814238 }, { 125, 20294070 }, { 127, 26041382 }, { 129, 33464926 }, { 131, 43088171 }, { 133, 55549258 }, { 135, 71608010 }, { 137, 92211954 }, { 139, 118581507 }, { 141, 152368710 } } 88596.95 ms (1 min 28 s 596.95 ms) taken to filter and order new representative proofs. Found 16952082 representative, 57851078 redundant, and 77565550 invalid condensed detachment proof strings. lengths up to 141 ; amounts per length: {(1,1), (3,1), (5,2), (7,2), (9,1), (13,1), (15,2), (17,3), (19,4), (21,5), (23,5), (25,5), (27,6), (29,7), (31,15), (33,20), (35,25), (37,30), (39,37), (41,42), (43,51), (45,63), (47,85), (49,122), (51,162), (53,206), (55,251), (57,292), (59,339), (61,444), (63,598), (65,781), (67,1016), (69,1303), (71,1593), (73,1922), (75,2359), (77,2986), (79,3875), (81,5006), (83,6466), (85,8184), (87,10182), (89,12488), (91,15534), (93,19614), (95,25087), (97,32452), (99,41840), (101,53343), (103,67105), (105,84222), (107,105925), (109,134564), (111,172053), (113,221055), (115,283569), (117,361751), (119,458509), (121,579502), (123,734352), (125,935212), (127,1197027), (129,1534565), (131,1965596), (133,2509883), (135,3196594), (137,4066027), (139,5180139), (141,16952082)} ; 16952082 new representative proofs (57851078 redundant, 77565550 invalid) Fri Oct 6 10:50:16 2023: Starting to write 16952082 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. 23058.08 ms (23 s 58.09 ms) taken to print and save 5160630061 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. Fri Oct 6 10:50:56 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 141, unfiltered] Fri Oct 6 10:52:08 2023: Process terminated. [pid: 13008, tid:23334345246592]