( This log file was generated by executing 'pmGenerator -c -n -s CCpCCNpqrCsCCNtCrtCpt --iterate -u' (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-OPTANE MPI node — 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) — running Linux, Rocky 8.8. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 40502334 optane_low 64 COMPLETED 0:0 00:51:08 40502334.ba+ 64 COMPLETED 0:0 00:51:08 254921764K 40502334.ex+ 64 COMPLETED 0:0 00:51:08 0 By 254921764 KiB = (254921764 / 1024^2) GiB = 243.112339019775390625 GiB, it used approximately 243.11 gibibytes of memory. ) Thu Nov 2 07:23:51 2023: Process started. [pid: 14675, tid:22624255580032] Tasks: 1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 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 countNextIterationAmount(false, true). Thu Nov 2 07:23:51 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.34 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:22624186926848] 2.13 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:22624161711872] 1.21 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:22624193230592] 1.56 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:22623941555968] 5.93 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:22624189028096] 3.06 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:22624195331840] 11616.23 ms (11 s 616.23 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:22624193230592] 6.78 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:22624191129344] 12310.61 ms (12 s 310.61 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:22624189028096] 10207.77 ms (10 s 207.77 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:22624186926848] 11760.62 ms (11 s 760.62 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:22623941555968] 1.39 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:22624184825600] 7.77 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:22624182724352] 5.17 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:22624180623104] 4.32 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:22624178521856] 8.15 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:22624176420608] 7.68 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:22624174319360] 7.35 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:22624172218112] 11.28 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:22624170116864] 7.24 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:22624168015616] 0.98 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:22624165914368] 1.22 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:22624163813120] 10563.54 ms (10 s 563.54 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:22624161711872] 7.74 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:22624159610624] 8.19 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:22624157509376] 4.34 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:22624155408128] 2.46 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:22624153306880] 13.46 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:22624151205632] 10.20 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:22624149104384] 23.64 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:22624147003136] 6.58 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:22623939454720] 18.13 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:22623937353472] 12.70 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:22623935252224] 21.42 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:22623933150976] 239.69 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:22623931049728] 11.59 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:22623928948480] 20.70 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:22623926847232] 11.78 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:22623924745984] 21.25 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:22623922644736] 11.08 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:22623920543488] 33.20 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:22623918442240] 35.92 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:22623916340992] 172.93 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:22623914239744] 46.10 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:22623912138496] 38.12 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:22623910037248] 283.49 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:22623907936000] 278.62 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:22623905834752] 386.46 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:22623903733504] 95.28 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:22623901632256] 331.49 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:22623899531008] 96.19 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:22623897429760] 1061.85 ms (1 s 61.85 ms) taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:22623895328512] 789.05 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:22623893227264] 990.06 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:22623891126016] 811.15 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:22623889024768] 1077.41 ms (1 s 77.41 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:22623886923520] 1001.83 ms (1 s 1.83 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:22623884822272] 1152.15 ms (1 s 152.15 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:22623882721024] 2554.95 ms (2 s 554.95 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:22623880619776] 6991.79 ms (6 s 991.79 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:22623878518528] 9738.13 ms (9 s 738.13 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:22621659854592] 3939.05 ms (3 s 939.05 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:22621657753344] 4107.62 ms (4 s 107.62 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:22621655652096] 4620.55 ms (4 s 620.55 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:22621653550848] 5321.51 ms (5 s 321.51 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:22621651449600] 5512.38 ms (5 s 512.38 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:22621649348352] 6132.58 ms (6 s 132.58 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:22621647247104] 8301.63 ms (8 s 301.63 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:22621645145856] 9270.01 ms (9 s 270.01 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:22621643044608] 12461.52 ms (12 s 461.53 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. 56730.97 ms (56 s 730.97 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:22621643044608] 75774.44 ms (1 min 15 s 774.44 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:22621645145856] 98439.55 ms (1 min 38 s 439.55 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:22621647247104] 103003.24 ms (1 min 43 s 3.24 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:22621649348352] 111589.92 ms (1 min 51 s 589.92 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:22621651449600] 121537.47 ms (2 min 1 s 537.47 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:22621653550848] 121548.47 ms (2 min 1 s 548.47 ms) additional read duration. Loaded 6 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 151 : 82234537 296691553 representatives in total. Thu Nov 2 07:26:26 2023: Inserted ≈ 5% of D-proof conclusions. [ 14834577 of 296691553] (ETC: Thu Nov 2 07:33:03 2023 ; 6 min 37 s 58.75 ms remaining ; 6 min 57 s 956.58 ms total) Thu Nov 2 07:26:46 2023: Inserted ≈10% of D-proof conclusions. [ 29669155 of 296691553] (ETC: Thu Nov 2 07:32:59 2023 ; 6 min 12 s 599.09 ms remaining ; 6 min 53 s 998.98 ms total) Thu Nov 2 07:27:02 2023: Inserted ≈15% of D-proof conclusions. [ 44503732 of 296691553] (ETC: Thu Nov 2 07:32:29 2023 ; 5 min 26 s 465.63 ms remaining ; 6 min 24 s 77.21 ms total) Thu Nov 2 07:27:18 2023: Inserted ≈20% of D-proof conclusions. [ 59338310 of 296691553] (ETC: Thu Nov 2 07:32:13 2023 ; 4 min 54 s 185.01 ms remaining ; 6 min 7 s 731.26 ms total) Thu Nov 2 07:27:35 2023: Inserted ≈25% of D-proof conclusions. [ 74172888 of 296691553] (ETC: Thu Nov 2 07:32:06 2023 ; 4 min 31 s 229.63 ms remaining ; 6 min 1 s 639.50 ms total) Thu Nov 2 07:27:52 2023: Inserted ≈30% of D-proof conclusions. [ 89007465 of 296691553] (ETC: Thu Nov 2 07:32:03 2023 ; 4 min 10 s 735.69 ms remaining ; 5 min 58 s 193.84 ms total) Thu Nov 2 07:28:10 2023: Inserted ≈35% of D-proof conclusions. [103842043 of 296691553] (ETC: Thu Nov 2 07:32:04 2023 ; 3 min 53 s 269.69 ms remaining ; 5 min 58 s 876.45 ms total) Thu Nov 2 07:28:30 2023: Inserted ≈40% of D-proof conclusions. [118676621 of 296691553] (ETC: Thu Nov 2 07:32:07 2023 ; 3 min 37 s 262.68 ms remaining ; 6 min 2 s 104.47 ms total) Thu Nov 2 07:28:51 2023: Inserted ≈45% of D-proof conclusions. [133511198 of 296691553] (ETC: Thu Nov 2 07:32:14 2023 ; 3 min 23 s 182.67 ms remaining ; 6 min 9 s 423.03 ms total) Thu Nov 2 07:29:14 2023: Inserted ≈50% of D-proof conclusions. [148345776 of 296691553] (ETC: Thu Nov 2 07:32:23 2023 ; 3 min 8 s 885.16 ms remaining ; 6 min 17 s 770.33 ms total) Thu Nov 2 07:29:38 2023: Inserted ≈55% of D-proof conclusions. [163180354 of 296691553] (ETC: Thu Nov 2 07:32:32 2023 ; 2 min 54 s 201.13 ms remaining ; 6 min 27 s 113.62 ms total) Thu Nov 2 07:30:04 2023: Inserted ≈60% of D-proof conclusions. [178014931 of 296691553] (ETC: Thu Nov 2 07:32:44 2023 ; 2 min 39 s 687.22 ms remaining ; 6 min 39 s 218.04 ms total) Thu Nov 2 07:30:26 2023: Inserted ≈65% of D-proof conclusions. [192849509 of 296691553] (ETC: Thu Nov 2 07:32:47 2023 ; 2 min 20 s 835.89 ms remaining ; 6 min 42 s 388.27 ms total) Thu Nov 2 07:30:47 2023: Inserted ≈70% of D-proof conclusions. [207684087 of 296691553] (ETC: Thu Nov 2 07:32:48 2023 ; 2 min 900.35 ms remaining ; 6 min 43 s 1.16 ms total) Thu Nov 2 07:31:10 2023: Inserted ≈75% of D-proof conclusions. [222518664 of 296691553] (ETC: Thu Nov 2 07:32:51 2023 ; 1 min 41 s 661.68 ms remaining ; 6 min 46 s 646.72 ms total) Thu Nov 2 07:31:33 2023: Inserted ≈80% of D-proof conclusions. [237353242 of 296691553] (ETC: Thu Nov 2 07:32:55 2023 ; 1 min 22 s 122.44 ms remaining ; 6 min 50 s 612.21 ms total) Thu Nov 2 07:31:56 2023: Inserted ≈85% of D-proof conclusions. [252187820 of 296691553] (ETC: Thu Nov 2 07:32:58 2023 ; 1 min 2 s 47.74 ms remaining ; 6 min 53 s 651.61 ms total) Thu Nov 2 07:32:19 2023: Inserted ≈90% of D-proof conclusions. [267022397 of 296691553] (ETC: Thu Nov 2 07:33:01 2023 ; 41 s 592.96 ms remaining ; 6 min 55 s 929.63 ms total) Thu Nov 2 07:32:45 2023: Inserted ≈95% of D-proof conclusions. [281856975 of 296691553] (ETC: Thu Nov 2 07:33:06 2023 ; 21 s 72.11 ms remaining ; 7 min 1 s 442.15 ms total) Thu Nov 2 07:33:10 2023: Inserted 100% of D-proof conclusions. [296691553 of 296691553] (ETC: Thu Nov 2 07:33:10 2023 ; 0.00 ms remaining ; 7 min 5 s 375.88 ms total) 425376.07 ms (7 min 5 s 376.07 ms) total insertion duration. Thu Nov 2 07:33:10 2023: Starting to iterate D-proof candidates of length 153. 1946329.91 ms (32 min 26 s 329.91 ms) taken to iterate 1176314122 condensed detachment proof strings of length 153. [Copy] Next iteration count (unfiltered141+): { 153, 1176314122 } Thu Nov 2 08:05:59 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Thu Nov 2 08:14:41 2023: Process terminated. [pid: 14675, tid:22624255580032]