( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39789301 c18m 48 COMPLETED 0:0 00:24:04 39789301.ba+ 48 COMPLETED 0:0 00:24:04 86120476K 39789301.ex+ 48 COMPLETED 0:0 00:24:04 0 By 86120476 KiB = (86120476 / 1024^2) GiB = 82.130886077880859375 GiB, it used approximately 82.13 gibibytes of memory. ) Sat Oct 7 05:24:35 2023: Process started. [pid: 168936, tid:23077128157056] 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). Sat Oct 7 05:24:35 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.02 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23076991395584] 8.71 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23076951471872] 0.70 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23076970383104] 0.50 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23077067908864] 0.32 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23076955674368] 1.61 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23076980889344] 0.93 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23076968281856] 1.03 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23077065807616] 0.89 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23076949370624] 1.15 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23076989294336] 0.18 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23076987193088] 1.20 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23076966180608] 1.28 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23076976686848] 1.77 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23076936763136] 0.19 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23076993496832] 0.11 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23076953573120] 0.21 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23076961978112] 0.00 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23076985091840] 0.03 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23077063706368] 1.15 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23076974585600] 3.15 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23076959876864] 1404.56 ms (1 s 404.56 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23077067908864] 8387.49 ms (8 s 387.49 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23077065807616] 5445.37 ms (5 s 445.37 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23077063706368] 3226.65 ms (3 s 226.65 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23076993496832] 389.12 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23076991395584] 1208.10 ms (1 s 208.10 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23076989294336] 1516.51 ms (1 s 516.51 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23076987193088] 4881.80 ms (4 s 881.81 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23076985091840] 3.80 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23076982990592] 3457.63 ms (3 s 457.63 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23076980889344] 3.22 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23076978788096] 2307.13 ms (2 s 307.13 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23076976686848] 6043.76 ms (6 s 43.76 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23076974585600] 1.63 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23076972484352] 965.44 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23076970383104] 5641.17 ms (5 s 641.17 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23076968281856] 1923.08 ms (1 s 923.08 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23076966180608] 0.30 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23076964079360] 4221.46 ms (4 s 221.46 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23076961978112] 6756.32 ms (6 s 756.32 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23076959876864] 3.21 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23076957775616] 2219.88 ms (2 s 219.88 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23076955674368] 3695.38 ms (3 s 695.38 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23076953573120] 661.00 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23076951471872] 883.00 ms taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23076949370624] 4.85 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23076947269376] 1.76 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23076945168128] 7.42 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23076943066880] 0.55 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23076940965632] 11.78 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23076938864384] 2813.27 ms (2 s 813.27 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23076936763136] 4.28 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23076934661888] 7.83 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23076932560640] 22.14 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23076930459392] 9.72 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23074711795456] 7.83 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23074709694208] 21.41 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23074707592960] 24.87 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23074705491712] 27.55 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23074703390464] 33.24 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23074701289216] 25.75 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23074699187968] 39.54 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23074697086720] 52.90 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23074694985472] 62.25 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23074692884224] 75.23 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23074690782976] 94.24 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23074688681728] 197.44 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23074686580480] 288.56 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23074684479232] 8449.15 ms (8 s 449.15 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. 13787.36 ms (13 s 787.36 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23074684479232] 22221.56 ms (22 s 221.56 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23074686580480] 29352.94 ms (29 s 352.94 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23074688681728] 29355.21 ms (29 s 355.21 ms) additional read duration. Loaded 3 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 104275433 representatives in total. Sat Oct 7 05:25:17 2023: Inserted ≈ 5% of D-proof conclusions. [ 5213771 of 104275433] (ETC: Sat Oct 7 05:26:38 2023 ; 1 min 20 s 392.45 ms remaining ; 1 min 24 s 623.63 ms total) Sat Oct 7 05:25:21 2023: Inserted ≈10% of D-proof conclusions. [ 10427543 of 104275433] (ETC: Sat Oct 7 05:26:27 2023 ; 1 min 6 s 7.98 ms remaining ; 1 min 13 s 342.20 ms total) Sat Oct 7 05:25:23 2023: Inserted ≈15% of D-proof conclusions. [ 15641314 of 104275433] (ETC: Sat Oct 7 05:26:20 2023 ; 56 s 632.30 ms remaining ; 1 min 6 s 626.23 ms total) Sat Oct 7 05:25:26 2023: Inserted ≈20% of D-proof conclusions. [ 20855086 of 104275433] (ETC: Sat Oct 7 05:26:17 2023 ; 51 s 383.63 ms remaining ; 1 min 4 s 229.54 ms total) Sat Oct 7 05:25:29 2023: Inserted ≈25% of D-proof conclusions. [ 26068858 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 46 s 400.48 ms remaining ; 1 min 1 s 867.30 ms total) Sat Oct 7 05:25:31 2023: Inserted ≈30% of D-proof conclusions. [ 31282629 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 42 s 102.78 ms remaining ; 1 min 146.83 ms total) Sat Oct 7 05:25:34 2023: Inserted ≈35% of D-proof conclusions. [ 36496401 of 104275433] (ETC: Sat Oct 7 05:26:14 2023 ; 39 s 394.89 ms remaining ; 1 min 607.53 ms total) Sat Oct 7 05:25:38 2023: Inserted ≈40% of D-proof conclusions. [ 41710173 of 104275433] (ETC: Sat Oct 7 05:26:16 2023 ; 37 s 765.91 ms remaining ; 1 min 2 s 943.19 ms total) Sat Oct 7 05:25:41 2023: Inserted ≈45% of D-proof conclusions. [ 46923944 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 34 s 63.19 ms remaining ; 1 min 1 s 933.07 ms total) Sat Oct 7 05:25:44 2023: Inserted ≈50% of D-proof conclusions. [ 52137716 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 30 s 680.02 ms remaining ; 1 min 1 s 360.04 ms total) Sat Oct 7 05:25:47 2023: Inserted ≈55% of D-proof conclusions. [ 57351488 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 27 s 615.81 ms remaining ; 1 min 1 s 368.47 ms total) Sat Oct 7 05:25:50 2023: Inserted ≈60% of D-proof conclusions. [ 62565259 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 24 s 643.77 ms remaining ; 1 min 1 s 609.43 ms total) Sat Oct 7 05:25:54 2023: Inserted ≈65% of D-proof conclusions. [ 67779031 of 104275433] (ETC: Sat Oct 7 05:26:15 2023 ; 21 s 684.10 ms remaining ; 1 min 1 s 954.57 ms total) Sat Oct 7 05:25:56 2023: Inserted ≈70% of D-proof conclusions. [ 72992803 of 104275433] (ETC: Sat Oct 7 05:26:14 2023 ; 18 s 154.02 ms remaining ; 1 min 513.39 ms total) Sat Oct 7 05:25:58 2023: Inserted ≈75% of D-proof conclusions. [ 78206574 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 14 s 991.53 ms remaining ; 59 s 966.13 ms total) Sat Oct 7 05:26:01 2023: Inserted ≈80% of D-proof conclusions. [ 83420346 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 11 s 866.58 ms remaining ; 59 s 332.91 ms total) Sat Oct 7 05:26:03 2023: Inserted ≈85% of D-proof conclusions. [ 88634118 of 104275433] (ETC: Sat Oct 7 05:26:12 2023 ; 8 s 858.67 ms remaining ; 59 s 57.78 ms total) Sat Oct 7 05:26:07 2023: Inserted ≈90% of D-proof conclusions. [ 93847889 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 5 s 940.78 ms remaining ; 59 s 407.82 ms total) Sat Oct 7 05:26:10 2023: Inserted ≈95% of D-proof conclusions. [ 99061661 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 2 s 986.35 ms remaining ; 59 s 727.05 ms total) Sat Oct 7 05:26:13 2023: Inserted 100% of D-proof conclusions. [104275433 of 104275433] (ETC: Sat Oct 7 05:26:13 2023 ; 0.00 ms remaining ; 59 s 912.40 ms total) 59912.62 ms (59 s 912.62 ms) total insertion duration. Sat Oct 7 05:26:13 2023: Starting to iterate D-proof candidates of length 147. 1128383.60 ms (18 min 48 s 383.61 ms) taken to iterate 453382622 condensed detachment proof strings of length 147. [Copy] Next iteration count (unfiltered141+): { 147, 453382622 } Sat Oct 7 05:45:02 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sat Oct 7 05:48:29 2023: Process terminated. [pid: 168936, tid:23077128157056]