( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39736981 c18m 48 COMPLETED 0:0 00:06:35 39736981.ba+ 48 COMPLETED 0:0 00:06:35 14692492K 39736981.ex+ 48 COMPLETED 0:0 00:06:35 84K By 14692492 KiB = (14692492 / 1024^2) GiB = 14.011852264404296875 GiB, it used approximately 14.01 gibibytes of memory. ) Thu Oct 5 10:08:40 2023: Process started. [pid: 108219, tid:23029825247104] 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 Oct 5 10:08:40 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.30 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23029756593920] 2.95 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23029251778304] 4.99 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23029253879552] 1.55 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23029232867072] 0.54 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23029276993280] 0.68 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23029264385792] 0.48 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23029243373312] 0.16 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23029249677056] 0.30 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23029762897664] 0.06 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23029764998912] 0.17 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23029260183296] 0.93 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23029760796416] 1.50 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23029262284544] 0.18 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23029758695168] 0.60 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23029270689536] 0.02 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23029258082048] 0.29 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23029272790784] 0.39 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23029268588288] 0.37 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23029245474560] 0.03 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23029752391424] 914.67 ms taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23029764998912] 729.67 ms taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23029762897664] 1432.52 ms (1 s 432.52 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23029760796416] 1921.61 ms (1 s 921.62 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23029758695168] 419.78 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23029756593920] 7.26 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23029754492672] 4251.36 ms (4 s 251.37 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23029752391424] 2.38 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23029279094528] 2194.10 ms (2 s 194.10 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23029276993280] 0.07 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23029140674304] 5.62 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23029274892032] 2891.10 ms (2 s 891.10 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23029272790784] 2268.72 ms (2 s 268.72 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23029270689536] 3382.19 ms (3 s 382.19 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23029268588288] 0.07 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23029266487040] 3282.08 ms (3 s 282.08 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23029264385792] 1655.94 ms (1 s 655.94 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23029262284544] 1111.70 ms (1 s 111.70 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23029260183296] 2543.76 ms (2 s 543.76 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23029258082048] 5.94 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23029255980800] 1006.15 ms (1 s 6.15 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23029253879552] 632.37 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23029251778304] 8559.24 ms (8 s 559.24 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23029249677056] 8.13 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23029247575808] 3768.39 ms (3 s 768.39 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23029245474560] 5326.55 ms (5 s 326.55 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23029243373312] 19.87 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23029241272064] 8.62 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23029239170816] 10.67 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23029237069568] 44.89 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23029234968320] 1452.05 ms (1 s 452.05 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23029232867072] 8.82 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23029230765824] 24.90 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23029228664576] 23.59 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23029226563328] 28.05 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23029224462080] 25.27 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23029222360832] 32.15 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23029220259584] 22.06 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23029218158336] 38.07 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23029216057088] 44.33 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23029144876800] 36.29 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23029142775552] 59.47 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23029138573056] 63.68 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23029136471808] 60.89 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23029134370560] 88.15 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23029132269312] 100.98 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23029130168064] 192.19 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23029128066816] 291.94 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23029125965568] 8609.49 ms (8 s 609.49 ms) total read duration. Loaded 69 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 18856369 representatives in total. Thu Oct 5 10:08:49 2023: Inserted ≈ 5% of D-proof conclusions. [ 942818 of 18856369] (ETC: Thu Oct 5 10:09:00 2023 ; 10 s 328.25 ms remaining ; 10 s 871.85 ms total) Thu Oct 5 10:08:50 2023: Inserted ≈10% of D-proof conclusions. [ 1885636 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 9 s 673.56 ms remaining ; 10 s 748.39 ms total) Thu Oct 5 10:08:50 2023: Inserted ≈15% of D-proof conclusions. [ 2828455 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 9 s 167.47 ms remaining ; 10 s 785.26 ms total) Thu Oct 5 10:08:51 2023: Inserted ≈20% of D-proof conclusions. [ 3771273 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 8 s 539.91 ms remaining ; 10 s 674.88 ms total) Thu Oct 5 10:08:51 2023: Inserted ≈25% of D-proof conclusions. [ 4714092 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 7 s 889.28 ms remaining ; 10 s 519.04 ms total) Thu Oct 5 10:08:52 2023: Inserted ≈30% of D-proof conclusions. [ 5656910 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 7 s 48.55 ms remaining ; 10 s 69.36 ms total) Thu Oct 5 10:08:52 2023: Inserted ≈35% of D-proof conclusions. [ 6599729 of 18856369] (ETC: Thu Oct 5 10:08:59 2023 ; 6 s 384.68 ms remaining ; 9 s 822.59 ms total) Thu Oct 5 10:08:53 2023: Inserted ≈40% of D-proof conclusions. [ 7542547 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 5 s 809.95 ms remaining ; 9 s 683.25 ms total) Thu Oct 5 10:08:53 2023: Inserted ≈45% of D-proof conclusions. [ 8485366 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 5 s 244.38 ms remaining ; 9 s 535.24 ms total) Thu Oct 5 10:08:53 2023: Inserted ≈50% of D-proof conclusions. [ 9428184 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 4 s 750.95 ms remaining ; 9 s 501.90 ms total) Thu Oct 5 10:08:54 2023: Inserted ≈55% of D-proof conclusions. [10371002 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 4 s 226.65 ms remaining ; 9 s 392.56 ms total) Thu Oct 5 10:08:54 2023: Inserted ≈60% of D-proof conclusions. [11313821 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 3 s 854.06 ms remaining ; 9 s 635.15 ms total) Thu Oct 5 10:08:55 2023: Inserted ≈65% of D-proof conclusions. [12256639 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 3 s 382.05 ms remaining ; 9 s 662.99 ms total) Thu Oct 5 10:08:55 2023: Inserted ≈70% of D-proof conclusions. [13199458 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 2 s 900.70 ms remaining ; 9 s 669.00 ms total) Thu Oct 5 10:08:56 2023: Inserted ≈75% of D-proof conclusions. [14142276 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 2 s 384.89 ms remaining ; 9 s 539.56 ms total) Thu Oct 5 10:08:56 2023: Inserted ≈80% of D-proof conclusions. [15085095 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 1 s 913.78 ms remaining ; 9 s 568.91 ms total) Thu Oct 5 10:08:57 2023: Inserted ≈85% of D-proof conclusions. [16027913 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 1 s 421.97 ms remaining ; 9 s 479.79 ms total) Thu Oct 5 10:08:57 2023: Inserted ≈90% of D-proof conclusions. [16970732 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 952.41 ms remaining ; 9 s 524.09 ms total) Thu Oct 5 10:08:58 2023: Inserted ≈95% of D-proof conclusions. [17913550 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 478.68 ms remaining ; 9 s 573.53 ms total) Thu Oct 5 10:08:58 2023: Inserted 100% of D-proof conclusions. [18856369 of 18856369] (ETC: Thu Oct 5 10:08:58 2023 ; 0.00 ms remaining ; 9 s 577.92 ms total) 9578.17 ms (9 s 578.16 ms) total insertion duration. Thu Oct 5 10:08:58 2023: Starting to iterate D-proof candidates of length 139. 346719.79 ms (5 min 46 s 719.79 ms) taken to iterate 118581507 condensed detachment proof strings of length 139. [Copy] Next iteration count (filtered): { 139, 118581507 } Thu Oct 5 10:14:45 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Thu Oct 5 10:15:10 2023: Process terminated. [pid: 108219, tid:23029825247104]