( This log file was generated by executing 'pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40414369 c18m_low 48 COMPLETED 0:0 00:28:58 40414369.ba+ 48 COMPLETED 0:0 00:28:58 158848256K 40414369.ex+ 48 COMPLETED 0:0 00:28:58 8K By 158848256 KiB = (158848256 / 1024^2) GiB = 151.489501953125 GiB, it used approximately 151.49 gibibytes of memory. ) Fri Oct 27 15:37:29 2023: Process started. [pid: 163819, tid:22386628032384] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9] (1) C0CCN1CCN2.3C4.1CC2.4C2.1 - CpCCNqCCNrsCtqCCrtCrq - 0\imply((\not1\imply((\not2\imply3)\imply(4\imply1)))\imply((2\imply4)\imply(2\imply1))) [Main] Calling countNextIterationAmount(false, true). Fri Oct 27 15:37:29 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.02 ms taken to load initial representatives. 1.83 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22386538366720] 1.93 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22386563581696] 0.07 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22386567784192] 0.26 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22386523657984] 0.59 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22384694253312] 0.29 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22386553075456] 0.26 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22386519455488] 0.73 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22386550974208] 3.02 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22386527860480] 3.26 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22386548872960] 0.06 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22386544670464] 0.13 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22386536265472] 0.09 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22386559379200] 0.17 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22386555176704] 0.04 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22386557277952] 0.10 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22386521556736] 0.11 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22386513151744] 3.47 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22386546771712] 0.93 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22386529961728] 1.16 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22386534164224] 0.03 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22384562136832] 0.71 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22384696354560] 1.35 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22384687949568] 0.48 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22386561480448] 0.85 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22386540467968] 0.11 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22386515252992] 0.43 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22386565682944] 509.65 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22386567784192] 10816.08 ms (10 s 816.08 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:22386565682944] 363.95 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22386563581696] 8341.63 ms (8 s 341.63 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22386561480448] 1449.86 ms (1 s 449.86 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22386559379200] 2199.83 ms (2 s 199.83 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22386557277952] 1824.75 ms (1 s 824.75 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22386555176704] 1448.78 ms (1 s 448.78 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22386553075456] 2972.47 ms (2 s 972.47 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22386550974208] 6033.72 ms (6 s 33.72 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22386548872960] 3738.39 ms (3 s 738.39 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22386546771712] 10233.86 ms (10 s 233.86 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22386544670464] 2.25 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22386542569216] 9112.20 ms (9 s 112.20 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22386540467968] 293.07 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22386538366720] 938.29 ms taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22386536265472] 5140.77 ms (5 s 140.77 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22386534164224] 0.60 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22386532062976] 4345.29 ms (4 s 345.29 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22386529961728] 4344.12 ms (4 s 344.12 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22386527860480] 2.17 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22386525759232] 586.68 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22386523657984] 2613.56 ms (2 s 613.56 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22386521556736] 2035.40 ms (2 s 35.40 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22386519455488] 5.44 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22386517354240] 9911.10 ms (9 s 911.10 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:22386515252992] 3186.59 ms (3 s 186.59 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22386513151744] 27.02 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22384698455808] 5945.78 ms (5 s 945.78 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22384562136832] 6845.64 ms (6 s 845.64 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22384696354560] 898.90 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22384694253312] 9.51 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22384692152064] 11.28 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22384690050816] 7561.16 ms (7 s 561.16 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22384687949568] 14.03 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22384685848320] 17.25 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22384683747072] 14.52 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22384681645824] 13.22 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22384679544576] 24.52 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22384677443328] 16.60 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22384675342080] 24.12 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22384673240832] 23.45 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22384671139584] 8.05 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22384669038336] 63.74 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22384666937088] 45.22 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22384664835840] 58.15 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22384662734592] 105.98 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22384660633344] 121.71 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22384658532096] 10880.41 ms (10 s 880.41 ms) total read duration. Loaded 76 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 1 9 : 2 11 : 2 13 : 2 15 : 2 17 : 5 19 : 5 21 : 3 23 : 6 25 : 10 27 : 7 29 : 12 31 : 14 33 : 17 35 : 21 37 : 30 39 : 28 41 : 44 43 : 56 45 : 66 47 : 80 49 : 108 51 : 123 53 : 168 55 : 197 57 : 241 59 : 303 61 : 390 63 : 444 65 : 570 67 : 707 69 : 863 71 : 1052 73 : 1340 75 : 1586 77 : 1990 79 : 2467 81 : 3018 83 : 3679 85 : 4661 87 : 5632 89 : 6994 91 : 8637 93 : 10677 95 : 13008 97 : 16295 99 : 19833 101 : 24567 103 : 30296 105 : 37377 107 : 45724 109 : 56922 111 : 69661 113 : 85894 115 : 105871 117 : 130737 119 : 160270 121 : 198446 123 : 243740 125 : 300530 127 : 370216 129 : 456911 131 : 560926 133 : 693346 135 : 853090 137 : 1051251 139 : 1294413 141 : 1597383 143 : 1963944 145 : 2423655 147 : 2983754 149 : 3676539 151 : 4527348 24048210 representatives in total. 33044.88 ms (33 s 44.88 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:22384658532096] 44294.94 ms (44 s 294.94 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:22384660633344] 54733.59 ms (54 s 733.59 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:22384662734592] 54736.51 ms (54 s 736.50 ms) additional read duration. Loaded 3 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 112321732 representatives in total. Fri Oct 27 15:38:42 2023: Inserted ≈ 5% of D-proof conclusions. [ 5616086 of 112321732] (ETC: Fri Oct 27 15:41:03 2023 ; 2 min 20 s 894.50 ms remaining ; 2 min 28 s 310.00 ms total) Fri Oct 27 15:38:48 2023: Inserted ≈10% of D-proof conclusions. [ 11232173 of 112321732] (ETC: Fri Oct 27 15:40:56 2023 ; 2 min 7 s 34.49 ms remaining ; 2 min 21 s 149.43 ms total) Fri Oct 27 15:38:54 2023: Inserted ≈15% of D-proof conclusions. [ 16848259 of 112321732] (ETC: Fri Oct 27 15:40:44 2023 ; 1 min 50 s 121.89 ms remaining ; 2 min 9 s 555.17 ms total) Fri Oct 27 15:38:59 2023: Inserted ≈20% of D-proof conclusions. [ 22464346 of 112321732] (ETC: Fri Oct 27 15:40:39 2023 ; 1 min 39 s 351.73 ms remaining ; 2 min 4 s 189.67 ms total) Fri Oct 27 15:39:05 2023: Inserted ≈25% of D-proof conclusions. [ 28080433 of 112321732] (ETC: Fri Oct 27 15:40:36 2023 ; 1 min 31 s 63.69 ms remaining ; 2 min 1 s 418.25 ms total) Fri Oct 27 15:39:12 2023: Inserted ≈30% of D-proof conclusions. [ 33696519 of 112321732] (ETC: Fri Oct 27 15:40:41 2023 ; 1 min 28 s 408.29 ms remaining ; 2 min 6 s 297.55 ms total) Fri Oct 27 15:39:20 2023: Inserted ≈35% of D-proof conclusions. [ 39312606 of 112321732] (ETC: Fri Oct 27 15:40:45 2023 ; 1 min 24 s 635.47 ms remaining ; 2 min 10 s 208.42 ms total) Fri Oct 27 15:39:30 2023: Inserted ≈40% of D-proof conclusions. [ 44928692 of 112321732] (ETC: Fri Oct 27 15:40:54 2023 ; 1 min 23 s 906.50 ms remaining ; 2 min 19 s 844.17 ms total) Fri Oct 27 15:39:41 2023: Inserted ≈45% of D-proof conclusions. [ 50544779 of 112321732] (ETC: Fri Oct 27 15:41:02 2023 ; 1 min 21 s 283.80 ms remaining ; 2 min 27 s 788.73 ms total) Fri Oct 27 15:39:49 2023: Inserted ≈50% of D-proof conclusions. [ 56160866 of 112321732] (ETC: Fri Oct 27 15:41:04 2023 ; 1 min 14 s 791.76 ms remaining ; 2 min 29 s 583.52 ms total) Fri Oct 27 15:39:57 2023: Inserted ≈55% of D-proof conclusions. [ 61776952 of 112321732] (ETC: Fri Oct 27 15:41:05 2023 ; 1 min 7 s 695.44 ms remaining ; 2 min 30 s 434.32 ms total) Fri Oct 27 15:40:05 2023: Inserted ≈60% of D-proof conclusions. [ 67393039 of 112321732] (ETC: Fri Oct 27 15:41:06 2023 ; 1 min 528.04 ms remaining ; 2 min 31 s 320.09 ms total) Fri Oct 27 15:40:11 2023: Inserted ≈65% of D-proof conclusions. [ 73009125 of 112321732] (ETC: Fri Oct 27 15:41:03 2023 ; 51 s 982.28 ms remaining ; 2 min 28 s 520.79 ms total) Fri Oct 27 15:40:18 2023: Inserted ≈70% of D-proof conclusions. [ 78625212 of 112321732] (ETC: Fri Oct 27 15:41:03 2023 ; 44 s 479.19 ms remaining ; 2 min 28 s 263.95 ms total) Fri Oct 27 15:40:25 2023: Inserted ≈75% of D-proof conclusions. [ 84241299 of 112321732] (ETC: Fri Oct 27 15:41:02 2023 ; 36 s 896.84 ms remaining ; 2 min 27 s 587.35 ms total) Fri Oct 27 15:40:30 2023: Inserted ≈80% of D-proof conclusions. [ 89857385 of 112321732] (ETC: Fri Oct 27 15:40:59 2023 ; 29 s 4.74 ms remaining ; 2 min 25 s 23.68 ms total) Fri Oct 27 15:40:36 2023: Inserted ≈85% of D-proof conclusions. [ 95473472 of 112321732] (ETC: Fri Oct 27 15:40:57 2023 ; 21 s 397.02 ms remaining ; 2 min 22 s 646.80 ms total) Fri Oct 27 15:40:42 2023: Inserted ≈90% of D-proof conclusions. [101089558 of 112321732] (ETC: Fri Oct 27 15:40:56 2023 ; 14 s 137.67 ms remaining ; 2 min 21 s 376.66 ms total) Fri Oct 27 15:40:49 2023: Inserted ≈95% of D-proof conclusions. [106705645 of 112321732] (ETC: Fri Oct 27 15:40:56 2023 ; 7 s 99.87 ms remaining ; 2 min 21 s 997.30 ms total) Fri Oct 27 15:40:58 2023: Inserted 100% of D-proof conclusions. [112321732 of 112321732] (ETC: Fri Oct 27 15:40:58 2023 ; 0.00 ms remaining ; 2 min 23 s 216.51 ms total) 143238.33 ms (2 min 23 s 238.33 ms) total insertion duration. Fri Oct 27 15:40:58 2023: Starting to iterate D-proof candidates of length 159. 1238361.03 ms (20 min 38 s 361.03 ms) taken to iterate 592215521 condensed detachment proof strings of length 159. [Copy] Next iteration count (unfiltered153+): { 159, 592215521 } Fri Oct 27 16:01:36 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 27 16:06:12 2023: Process terminated. [pid: 163819, tid:22386628032384]