( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40493665 c18m_low 48 COMPLETED 0:0 00:34:55 40493665.ba+ 48 COMPLETED 0:0 00:34:55 181758720K 40493665.ex+ 48 COMPLETED 0:0 00:34:55 0 By 181758720 KiB = (181758720 / 1024^2) GiB = 173.338623046875 GiB, it used approximately 173.34 gibibytes of memory. ) Wed Nov 1 10:29:20 2023: Process started. [pid: 135583, tid:22657008568192] 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). Wed Nov 1 10:29:20 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.01 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:22656939915008] 6.43 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:22656948320000] 0.72 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:22656925206272] 2.90 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:22656904193792] 1.07 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:22656899991296] 0.29 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:22656937813760] 0.47 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:22656916801280] 0.08 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:22656897890048] 3.21 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:22656906295040] 0.29 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:22656927307520] 0.02 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:22656908396288] 0.52 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:22656944117504] 0.02 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:22656912598784] 0.03 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:22656923105024] 0.04 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:22656902092544] 0.07 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:22656914700032] 0.11 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:22656935712512] 0.05 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:22656946218752] 3.42 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:22656933611264] 3.60 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:22656910497536] 0.06 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:22656942016256] 635.62 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:22656948320000] 5143.86 ms (5 s 143.87 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:22656946218752] 2017.04 ms (2 s 17.04 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:22656944117504] 7102.33 ms (7 s 102.33 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:22656942016256] 413.01 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:22656939915008] 3320.22 ms (3 s 320.22 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:22656937813760] 4590.03 ms (4 s 590.03 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:22656935712512] 5747.54 ms (5 s 747.54 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:22656933611264] 5.03 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:22656931510016] 12.15 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:22656929408768] 1213.36 ms (1 s 213.36 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:22656927307520] 1009.93 ms (1 s 9.93 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:22656925206272] 2877.81 ms (2 s 877.81 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:22656923105024] 0.51 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:22656921003776] 1.69 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:22656918902528] 5129.43 ms (5 s 129.43 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:22656916801280] 4014.33 ms (4 s 14.33 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:22656914700032] 2448.40 ms (2 s 448.40 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:22656912598784] 6488.85 ms (6 s 488.85 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:22656910497536] 1588.70 ms (1 s 588.70 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:22656908396288] 961.31 ms taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:22656906295040] 1450.68 ms (1 s 450.68 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:22656904193792] 3500.09 ms (3 s 500.09 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:22656902092544] 2102.41 ms (2 s 102.41 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:22656899991296] 8362.22 ms (8 s 362.22 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:22656897890048] 5.74 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:22656895788800] 6.00 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:22655214286592] 10.14 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:22655077967616] 12.07 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:22655212185344] 6.34 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:22655210084096] 7.47 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:22655207982848] 7.94 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:22655205881600] 2.51 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:22655203780352] 24.07 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:22655201679104] 20.78 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:22655199577856] 19.22 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:22655197476608] 12.60 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:22655195375360] 34.37 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:22655193274112] 19.84 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:22655191172864] 21.99 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:22655189071616] 25.70 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:22655186970368] 46.09 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:22655184869120] 54.69 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:22655182767872] 59.28 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:22655180666624] 63.99 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:22655178565376] 111.48 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:22655176464128] 228.28 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:22655174362880] 265.82 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:22655172261632] 8435.84 ms (8 s 435.84 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. 18346.68 ms (18 s 346.68 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:22655172261632] 28139.25 ms (28 s 139.25 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:22655174362880] 40411.50 ms (40 s 411.50 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:22655176464128] 49381.53 ms (49 s 381.53 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:22655178565376] 57880.12 ms (57 s 880.13 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:22655180666624] 57892.46 ms (57 s 892.46 ms) additional read duration. Loaded 5 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 214457016 representatives in total. Wed Nov 1 10:30:34 2023: Inserted ≈ 5% of D-proof conclusions. [ 10722850 of 214457016] (ETC: Wed Nov 1 10:33:14 2023 ; 2 min 39 s 586.90 ms remaining ; 2 min 47 s 986.21 ms total) Wed Nov 1 10:30:44 2023: Inserted ≈10% of D-proof conclusions. [ 21445701 of 214457016] (ETC: Wed Nov 1 10:33:22 2023 ; 2 min 38 s 216.50 ms remaining ; 2 min 55 s 796.11 ms total) Wed Nov 1 10:30:53 2023: Inserted ≈15% of D-proof conclusions. [ 32168552 of 214457016] (ETC: Wed Nov 1 10:33:27 2023 ; 2 min 33 s 923.74 ms remaining ; 3 min 1 s 86.75 ms total) Wed Nov 1 10:31:03 2023: Inserted ≈20% of D-proof conclusions. [ 42891403 of 214457016] (ETC: Wed Nov 1 10:33:30 2023 ; 2 min 26 s 878.33 ms remaining ; 3 min 3 s 597.91 ms total) Wed Nov 1 10:31:13 2023: Inserted ≈25% of D-proof conclusions. [ 53614254 of 214457016] (ETC: Wed Nov 1 10:33:33 2023 ; 2 min 19 s 851.66 ms remaining ; 3 min 6 s 468.88 ms total) Wed Nov 1 10:31:23 2023: Inserted ≈30% of D-proof conclusions. [ 64337104 of 214457016] (ETC: Wed Nov 1 10:33:35 2023 ; 2 min 12 s 563.35 ms remaining ; 3 min 9 s 376.21 ms total) Wed Nov 1 10:31:33 2023: Inserted ≈35% of D-proof conclusions. [ 75059955 of 214457016] (ETC: Wed Nov 1 10:33:36 2023 ; 2 min 3 s 699.48 ms remaining ; 3 min 10 s 306.90 ms total) Wed Nov 1 10:31:42 2023: Inserted ≈40% of D-proof conclusions. [ 85782806 of 214457016] (ETC: Wed Nov 1 10:33:35 2023 ; 1 min 53 s 342.21 ms remaining ; 3 min 8 s 903.68 ms total) Wed Nov 1 10:31:50 2023: Inserted ≈45% of D-proof conclusions. [ 96505657 of 214457016] (ETC: Wed Nov 1 10:33:32 2023 ; 1 min 42 s 408.06 ms remaining ; 3 min 6 s 196.48 ms total) Wed Nov 1 10:31:58 2023: Inserted ≈50% of D-proof conclusions. [107228508 of 214457016] (ETC: Wed Nov 1 10:33:30 2023 ; 1 min 31 s 724.22 ms remaining ; 3 min 3 s 448.44 ms total) Wed Nov 1 10:32:05 2023: Inserted ≈55% of D-proof conclusions. [117951358 of 214457016] (ETC: Wed Nov 1 10:33:26 2023 ; 1 min 21 s 110.50 ms remaining ; 3 min 245.56 ms total) Wed Nov 1 10:32:13 2023: Inserted ≈60% of D-proof conclusions. [128674209 of 214457016] (ETC: Wed Nov 1 10:33:24 2023 ; 1 min 11 s 332.36 ms remaining ; 2 min 58 s 330.90 ms total) Wed Nov 1 10:32:23 2023: Inserted ≈65% of D-proof conclusions. [139397060 of 214457016] (ETC: Wed Nov 1 10:33:25 2023 ; 1 min 2 s 731.35 ms remaining ; 2 min 59 s 232.41 ms total) Wed Nov 1 10:32:30 2023: Inserted ≈70% of D-proof conclusions. [150119911 of 214457016] (ETC: Wed Nov 1 10:33:24 2023 ; 53 s 311.42 ms remaining ; 2 min 57 s 704.72 ms total) Wed Nov 1 10:32:37 2023: Inserted ≈75% of D-proof conclusions. [160842762 of 214457016] (ETC: Wed Nov 1 10:33:21 2023 ; 43 s 755.48 ms remaining ; 2 min 55 s 21.91 ms total) Wed Nov 1 10:32:44 2023: Inserted ≈80% of D-proof conclusions. [171565612 of 214457016] (ETC: Wed Nov 1 10:33:18 2023 ; 34 s 469.90 ms remaining ; 2 min 52 s 349.50 ms total) Wed Nov 1 10:32:53 2023: Inserted ≈85% of D-proof conclusions. [182288463 of 214457016] (ETC: Wed Nov 1 10:33:18 2023 ; 25 s 849.53 ms remaining ; 2 min 52 s 330.18 ms total) Wed Nov 1 10:33:01 2023: Inserted ≈90% of D-proof conclusions. [193011314 of 214457016] (ETC: Wed Nov 1 10:33:18 2023 ; 17 s 212.32 ms remaining ; 2 min 52 s 123.22 ms total) Wed Nov 1 10:33:08 2023: Inserted ≈95% of D-proof conclusions. [203734165 of 214457016] (ETC: Wed Nov 1 10:33:17 2023 ; 8 s 538.84 ms remaining ; 2 min 50 s 776.85 ms total) Wed Nov 1 10:33:17 2023: Inserted 100% of D-proof conclusions. [214457016 of 214457016] (ETC: Wed Nov 1 10:33:17 2023 ; 0.00 ms remaining ; 2 min 51 s 238.12 ms total) 171246.16 ms (2 min 51 s 246.16 ms) total insertion duration. Wed Nov 1 10:33:17 2023: Starting to iterate D-proof candidates of length 151. 1336290.90 ms (22 min 16 s 290.90 ms) taken to iterate 891383185 condensed detachment proof strings of length 151. [Copy] Next iteration count (unfiltered141+): { 151, 891383185 } Wed Nov 1 10:55:34 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Wed Nov 1 11:03:58 2023: Process terminated. [pid: 135583, tid:22657008568192]