( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39788922 c18m 48 COMPLETED 0:0 00:10:12 39788922.ba+ 48 COMPLETED 0:0 00:10:12 32691036K 39788922.ex+ 48 COMPLETED 0:0 00:10:12 0 By 32691036 KiB = (32691036 / 1024^2) GiB = 31.176601409912109375 GiB, it used approximately 31.18 gibibytes of memory. ) Fri Oct 6 22:32:16 2023: Process started. [pid: 97453, tid:23011560392576] 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:32:16 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.02 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:23011423934208] 3.45 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23011407124224] 0.55 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23011405022976] 0.04 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23011402921728] 0.11 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23011381909248] 0.28 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23011413427968] 1.10 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23011398719232] 0.91 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23011417630464] 2.36 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23011426035456] 0.31 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23011421832960] 0.55 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23011394516736] 0.02 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23011367200512] 1.89 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23011409225472] 1.57 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23011384010496] 1.62 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23011388212992] 0.03 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23011415529216] 0.16 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23011498043136] 0.10 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23011379808000] 0.25 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23011500144384] 0.50 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23011375605504] 0.18 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23011419731712] 5890.98 ms (5 s 890.98 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23011500144384] 4669.20 ms (4 s 669.20 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23011498043136] 0.18 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23011428136704] 1028.49 ms (1 s 28.49 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23011426035456] 400.30 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23011423934208] 1304.83 ms (1 s 304.83 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23011421832960] 7189.35 ms (7 s 189.35 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23011419731712] 8589.70 ms (8 s 589.70 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23011417630464] 4055.63 ms (4 s 55.63 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23011415529216] 3385.88 ms (3 s 385.88 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23011413427968] 5.46 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23011411326720] 2501.87 ms (2 s 501.87 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23011409225472] 641.19 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23011407124224] 969.21 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23011405022976] 1454.43 ms (1 s 454.43 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23011402921728] 9.10 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23011400820480] 5717.92 ms (5 s 717.92 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23011398719232] 2.70 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23011396617984] 1641.23 ms (1 s 641.23 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23011394516736] 5.53 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23011392415488] 0.00 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23011390314240] 3603.57 ms (3 s 603.57 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23011388212992] 12.66 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23011386111744] 2972.84 ms (2 s 972.84 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23011384010496] 2275.03 ms (2 s 275.03 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23011381909248] 5379.76 ms (5 s 379.76 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23011379808000] 3.20 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23011377706752] 6558.81 ms (6 s 558.81 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23011375605504] 7.52 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23011373504256] 14.51 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23011371403008] 10.01 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23011369301760] 2067.13 ms (2 s 67.13 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23011367200512] 17.46 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23011365099264] 25.72 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23011293918976] 20.80 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23011291817728] 23.79 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23011289716480] 44.21 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23011287615232] 26.82 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23011285513984] 15.68 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23011283412736] 32.27 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23011281311488] 47.72 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23011279210240] 43.86 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23011277108992] 66.06 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23011275007744] 67.75 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23011272906496] 75.95 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23011270805248] 100.76 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23011268704000] 170.59 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23011266602752] 276.58 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23011264501504] 8644.93 ms (8 s 644.93 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. 9477.84 ms (9 s 477.84 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23011264501504] 9480.67 ms (9 s 480.67 ms) additional read duration. Loaded 1 more representative collection of size: 141 : 16952082 40988590 representatives in total. Fri Oct 6 22:32:36 2023: Inserted ≈ 5% of D-proof conclusions. [ 2049429 of 40988590] (ETC: Fri Oct 6 22:33:09 2023 ; 32 s 693.76 ms remaining ; 34 s 414.49 ms total) Fri Oct 6 22:32:38 2023: Inserted ≈10% of D-proof conclusions. [ 4098859 of 40988590] (ETC: Fri Oct 6 22:33:10 2023 ; 32 s 575.72 ms remaining ; 36 s 195.24 ms total) Fri Oct 6 22:32:40 2023: Inserted ≈15% of D-proof conclusions. [ 6148288 of 40988590] (ETC: Fri Oct 6 22:33:11 2023 ; 31 s 476.78 ms remaining ; 37 s 31.51 ms total) Fri Oct 6 22:32:42 2023: Inserted ≈20% of D-proof conclusions. [ 8197718 of 40988590] (ETC: Fri Oct 6 22:33:11 2023 ; 29 s 775.58 ms remaining ; 37 s 219.48 ms total) Fri Oct 6 22:32:44 2023: Inserted ≈25% of D-proof conclusions. [10247147 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 28 s 57.83 ms remaining ; 37 s 410.44 ms total) Fri Oct 6 22:32:45 2023: Inserted ≈30% of D-proof conclusions. [12296577 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 26 s 168.38 ms remaining ; 37 s 383.40 ms total) Fri Oct 6 22:32:47 2023: Inserted ≈35% of D-proof conclusions. [14346006 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 24 s 445.83 ms remaining ; 37 s 608.98 ms total) Fri Oct 6 22:32:49 2023: Inserted ≈40% of D-proof conclusions. [16395436 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 22 s 752.07 ms remaining ; 37 s 920.12 ms total) Fri Oct 6 22:32:51 2023: Inserted ≈45% of D-proof conclusions. [18444865 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 21 s 23.39 ms remaining ; 38 s 224.34 ms total) Fri Oct 6 22:32:53 2023: Inserted ≈50% of D-proof conclusions. [20494295 of 40988590] (ETC: Fri Oct 6 22:33:13 2023 ; 19 s 241.00 ms remaining ; 38 s 481.99 ms total) Fri Oct 6 22:32:56 2023: Inserted ≈55% of D-proof conclusions. [22543724 of 40988590] (ETC: Fri Oct 6 22:33:13 2023 ; 17 s 454.64 ms remaining ; 38 s 788.10 ms total) Fri Oct 6 22:32:57 2023: Inserted ≈60% of D-proof conclusions. [24593154 of 40988590] (ETC: Fri Oct 6 22:33:13 2023 ; 15 s 487.30 ms remaining ; 38 s 718.26 ms total) Fri Oct 6 22:32:59 2023: Inserted ≈65% of D-proof conclusions. [26642583 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 13 s 368.75 ms remaining ; 38 s 196.43 ms total) Fri Oct 6 22:33:01 2023: Inserted ≈70% of D-proof conclusions. [28692013 of 40988590] (ETC: Fri Oct 6 22:33:12 2023 ; 11 s 291.26 ms remaining ; 37 s 637.52 ms total) Fri Oct 6 22:33:02 2023: Inserted ≈75% of D-proof conclusions. [30741442 of 40988590] (ETC: Fri Oct 6 22:33:11 2023 ; 9 s 241.56 ms remaining ; 36 s 966.25 ms total) Fri Oct 6 22:33:03 2023: Inserted ≈80% of D-proof conclusions. [32790872 of 40988590] (ETC: Fri Oct 6 22:33:10 2023 ; 7 s 234.17 ms remaining ; 36 s 170.84 ms total) Fri Oct 6 22:33:04 2023: Inserted ≈85% of D-proof conclusions. [34840301 of 40988590] (ETC: Fri Oct 6 22:33:10 2023 ; 5 s 336.52 ms remaining ; 35 s 576.81 ms total) Fri Oct 6 22:33:06 2023: Inserted ≈90% of D-proof conclusions. [36889731 of 40988590] (ETC: Fri Oct 6 22:33:09 2023 ; 3 s 499.70 ms remaining ; 34 s 997.01 ms total) Fri Oct 6 22:33:07 2023: Inserted ≈95% of D-proof conclusions. [38939160 of 40988590] (ETC: Fri Oct 6 22:33:08 2023 ; 1 s 715.00 ms remaining ; 34 s 300.01 ms total) Fri Oct 6 22:33:08 2023: Inserted 100% of D-proof conclusions. [40988590 of 40988590] (ETC: Fri Oct 6 22:33:08 2023 ; 0.00 ms remaining ; 33 s 587.90 ms total) 33588.05 ms (33 s 588.05 ms) total insertion duration. Fri Oct 6 22:33:08 2023: Starting to iterate D-proof candidates of length 143. 493435.62 ms (8 min 13 s 435.62 ms) taken to iterate 216457445 condensed detachment proof strings of length 143. [Copy] Next iteration count (unfiltered141+): { 143, 216457445 } Fri Oct 6 22:41:21 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 6 22:42:22 2023: Process terminated. [pid: 97453, tid:23011560392576]