( 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 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. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 39788924 c18m 48 COMPLETED 0:0 00:13:35 39788924.ba+ 48 COMPLETED 0:0 00:13:35 54814444K 39788924.ex+ 48 COMPLETED 0:0 00:13:35 48K By 54814444 KiB = (54814444 / 1024^2) GiB = 52.275127410888671875 GiB, it used approximately 52.28 gibibytes of memory. ) Fri Oct 6 22:34:47 2023: Process started. [pid: 132956, tid:23225486927744] 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). Fri Oct 6 22:34:47 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.14 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23225418274560] 6.16 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23225403565824] 0.38 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23225395160832] 2.05 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23225409869568] 0.15 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23225424578304] 0.08 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23225374148352] 0.30 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23225405667072] 0.47 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23225386755840] 0.16 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23225426679552] 0.92 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23224765114112] 0.98 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23225401464576] 0.19 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23225376249600] 0.32 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23225407768320] 0.09 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23225397262080] 3.50 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23225416173312] 3.72 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23225414072064] 0.12 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23225420375808] 3.72 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23224763012864] 0.08 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23225388857088] 0.08 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23225384654592] 1.43 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23225422477056] 859.10 ms taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23225426679552] 2247.98 ms (2 s 247.98 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23225424578304] 6574.40 ms (6 s 574.40 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23225422477056] 4227.35 ms (4 s 227.35 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23225420375808] 410.43 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23225418274560] 3213.49 ms (3 s 213.50 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23225416173312] 3818.85 ms (3 s 818.85 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23225414072064] 6.39 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23225411970816] 1465.24 ms (1 s 465.24 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23225409869568] 2250.04 ms (2 s 250.04 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23225407768320] 5614.94 ms (5 s 614.94 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23225405667072] 625.18 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23225403565824] 1570.84 ms (1 s 570.84 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23225401464576] 0.19 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23225399363328] 2800.10 ms (2 s 800.10 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23225397262080] 973.42 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23225395160832] 2.71 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23225393059584] 0.78 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23225390958336] 5363.81 ms (5 s 363.81 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23225388857088] 8792.11 ms (8 s 792.11 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23225386755840] 5863.38 ms (5 s 863.38 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23225384654592] 6.22 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23225382553344] 2.73 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23225380452096] 3.06 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23225378350848] 1926.89 ms (1 s 926.89 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23225376249600] 3496.80 ms (3 s 496.80 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23225374148352] 11.53 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23224767215360] 1242.36 ms (1 s 242.36 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23224765114112] 5107.11 ms (5 s 107.11 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23224763012864] 8.32 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23224760911616] 8.57 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23224758810368] 5.64 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23224756709120] 16.35 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23224754607872] 16.18 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23224752506624] 10.51 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23224750405376] 23.06 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23224748304128] 31.57 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23224746202880] 39.98 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23224744101632] 24.91 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23224742000384] 28.65 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23224739899136] 38.74 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23224737797888] 64.44 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23224735696640] 54.49 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23224733595392] 64.29 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23224731494144] 70.97 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23224729392896] 115.49 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23224727291648] 192.09 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23224725190400] 290.79 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23224723089152] 8846.77 ms (8 s 846.77 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. 11480.66 ms (11 s 480.66 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23224723089152] 16837.09 ms (16 s 837.09 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23224725190400] 16839.13 ms (16 s 839.13 ms) additional read duration. Loaded 2 more representative collections of sizes: 141 : 16952082 143 : 26431403 67419993 representatives in total. Fri Oct 6 22:35:15 2023: Inserted ≈ 5% of D-proof conclusions. [ 3370999 of 67419993] (ETC: Fri Oct 6 22:36:02 2023 ; 46 s 965.90 ms remaining ; 49 s 437.79 ms total) Fri Oct 6 22:35:17 2023: Inserted ≈10% of D-proof conclusions. [ 6741999 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 39 s 89.87 ms remaining ; 43 s 433.19 ms total) Fri Oct 6 22:35:19 2023: Inserted ≈15% of D-proof conclusions. [10112998 of 67419993] (ETC: Fri Oct 6 22:35:54 2023 ; 35 s 58.55 ms remaining ; 41 s 245.35 ms total) Fri Oct 6 22:35:21 2023: Inserted ≈20% of D-proof conclusions. [13483998 of 67419993] (ETC: Fri Oct 6 22:35:52 2023 ; 31 s 407.44 ms remaining ; 39 s 259.31 ms total) Fri Oct 6 22:35:22 2023: Inserted ≈25% of D-proof conclusions. [16854998 of 67419993] (ETC: Fri Oct 6 22:35:51 2023 ; 28 s 724.56 ms remaining ; 38 s 299.41 ms total) Fri Oct 6 22:35:24 2023: Inserted ≈30% of D-proof conclusions. [20225997 of 67419993] (ETC: Fri Oct 6 22:35:51 2023 ; 26 s 510.40 ms remaining ; 37 s 872.00 ms total) Fri Oct 6 22:35:26 2023: Inserted ≈35% of D-proof conclusions. [23596997 of 67419993] (ETC: Fri Oct 6 22:35:50 2023 ; 24 s 292.97 ms remaining ; 37 s 373.80 ms total) Fri Oct 6 22:35:28 2023: Inserted ≈40% of D-proof conclusions. [26967997 of 67419993] (ETC: Fri Oct 6 22:35:52 2023 ; 23 s 461.79 ms remaining ; 39 s 102.99 ms total) Fri Oct 6 22:35:31 2023: Inserted ≈45% of D-proof conclusions. [30338996 of 67419993] (ETC: Fri Oct 6 22:35:53 2023 ; 22 s 301.00 ms remaining ; 40 s 547.27 ms total) Fri Oct 6 22:35:33 2023: Inserted ≈50% of D-proof conclusions. [33709996 of 67419993] (ETC: Fri Oct 6 22:35:54 2023 ; 20 s 641.94 ms remaining ; 41 s 283.88 ms total) Fri Oct 6 22:35:36 2023: Inserted ≈55% of D-proof conclusions. [37080996 of 67419993] (ETC: Fri Oct 6 22:35:55 2023 ; 18 s 965.78 ms remaining ; 42 s 146.18 ms total) Fri Oct 6 22:35:38 2023: Inserted ≈60% of D-proof conclusions. [40451995 of 67419993] (ETC: Fri Oct 6 22:35:55 2023 ; 17 s 47.68 ms remaining ; 42 s 619.20 ms total) Fri Oct 6 22:35:41 2023: Inserted ≈65% of D-proof conclusions. [43822995 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 15 s 66.09 ms remaining ; 43 s 45.97 ms total) Fri Oct 6 22:35:43 2023: Inserted ≈70% of D-proof conclusions. [47193995 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 12 s 922.57 ms remaining ; 43 s 75.24 ms total) Fri Oct 6 22:35:45 2023: Inserted ≈75% of D-proof conclusions. [50564994 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 10 s 838.13 ms remaining ; 43 s 352.52 ms total) Fri Oct 6 22:35:47 2023: Inserted ≈80% of D-proof conclusions. [53935994 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 8 s 675.59 ms remaining ; 43 s 377.95 ms total) Fri Oct 6 22:35:49 2023: Inserted ≈85% of D-proof conclusions. [57306994 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 6 s 482.72 ms remaining ; 43 s 218.16 ms total) Fri Oct 6 22:35:52 2023: Inserted ≈90% of D-proof conclusions. [60677993 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 4 s 314.93 ms remaining ; 43 s 149.34 ms total) Fri Oct 6 22:35:54 2023: Inserted ≈95% of D-proof conclusions. [64048993 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 2 s 156.50 ms remaining ; 43 s 129.93 ms total) Fri Oct 6 22:35:56 2023: Inserted 100% of D-proof conclusions. [67419993 of 67419993] (ETC: Fri Oct 6 22:35:56 2023 ; 0.00 ms remaining ; 43 s 404.27 ms total) 43404.58 ms (43 s 404.59 ms) total insertion duration. Fri Oct 6 22:35:56 2023: Starting to iterate D-proof candidates of length 145. 599387.28 ms (9 min 59 s 387.28 ms) taken to iterate 308369644 condensed detachment proof strings of length 145. [Copy] Next iteration count (unfiltered141+): { 145, 308369644 } Fri Oct 6 22:45:55 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 6 22:48:15 2023: Process terminated. [pid: 132956, tid:23225486927744]