( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40285985 c18m_low 48 COMPLETED 0:0 00:16:06 40285985.ba+ 48 COMPLETED 0:0 00:16:06 99801564K 40285985.ex+ 48 COMPLETED 0:0 00:16:06 16K By 99801564 KiB = (99801564 / 1024^2) GiB = 95.178188323974609375 GiB, it used approximately 95.18 gibibytes of memory. ) Sun Oct 22 16:23:08 2023: Process started. [pid: 53075, tid:23390181336960] 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). Sun Oct 22 16:23:08 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 1.69 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23390104303360] 0.04 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23390083290880] 4.82 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23390121113344] 5.17 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23390079088384] 0.10 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23390095898368] 0.78 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23390116910848] 0.07 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23390081189632] 0.24 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23388110190336] 0.74 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23390076987136] 0.87 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23390106404608] 0.18 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23390097999616] 0.03 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23390119012096] 0.15 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23390102202112] 0.05 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23390068582144] 0.02 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23390072784640] 2.24 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23390100100864] 0.71 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23390093797120] 0.23 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23390089594624] 0.23 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23388105987840] 1.28 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23390108505856] 1.45 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23390087493376] 0.68 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23390114809600] 0.85 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23390064379648] 0.79 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23390060177152] 0.85 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23390110607104] 0.01 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23390112708352] 0.14 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23390074885888] 451.95 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23390121113344] 1135.72 ms (1 s 135.72 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23390119012096] 1443.06 ms (1 s 443.06 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23390116910848] 6824.61 ms (6 s 824.61 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23390114809600] 9988.14 ms (9 s 988.14 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23390112708352] 9354.31 ms (9 s 354.31 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23390110607104] 5134.72 ms (5 s 134.72 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23390108505856] 5822.08 ms (5 s 822.08 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23390106404608] 146.29 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23390104303360] 1389.48 ms (1 s 389.48 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23390102202112] 2678.89 ms (2 s 678.89 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23390100100864] 8706.29 ms (8 s 706.29 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23390097999616] 1153.27 ms (1 s 153.27 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23390095898368] 3234.12 ms (3 s 234.13 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23390093797120] 0.46 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23390091695872] 3771.16 ms (3 s 771.16 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23390089594624] 5939.16 ms (5 s 939.16 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23390087493376] 7.09 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23390085392128] 327.06 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23390083290880] 1721.99 ms (1 s 721.99 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23390081189632] 650.15 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23390079088384] 4573.22 ms (4 s 573.23 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23390076987136] 10759.76 ms (10 s 759.75 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23390074885888] 2098.59 ms (2 s 98.59 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23390072784640] 2.46 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23390070683392] 1838.82 ms (1 s 838.82 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23390068582144] 1.65 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23390066480896] 7523.49 ms (7 s 523.49 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23390064379648] 5.91 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23390062278400] 8325.31 ms (8 s 325.31 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23390060177152] 3072.98 ms (3 s 72.98 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23388110190336] 2.22 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23388108089088] 4335.44 ms (4 s 335.44 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23388105987840] 5.28 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23388103886592] 5.15 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23388101785344] 3.91 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23388099684096] 21.83 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23388097582848] 21.16 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23388095481600] 21.77 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23388093380352] 27.53 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23388091279104] 34.51 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23388089177856] 23.75 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23388087076608] 17.72 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23388084975360] 43.62 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23388082874112] 45.42 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23388080772864] 56.21 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23388078671616] 77.81 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23388076570368] 118.11 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23388074469120] 10821.74 ms (10 s 821.74 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. 24901.44 ms (24 s 901.44 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:23388074469120] 31968.52 ms (31 s 968.52 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:23388076570368] 31972.51 ms (31 s 972.51 ms) additional read duration. Loaded 2 more representative collections of sizes: 153 : 21395853 155 : 28040847 73484910 representatives in total. Sun Oct 22 16:23:54 2023: Inserted ≈ 5% of D-proof conclusions. [ 3674245 of 73484910] (ETC: Sun Oct 22 16:25:10 2023 ; 1 min 15 s 56.62 ms remaining ; 1 min 19 s 6.97 ms total) Sun Oct 22 16:23:59 2023: Inserted ≈10% of D-proof conclusions. [ 7348491 of 73484910] (ETC: Sun Oct 22 16:25:15 2023 ; 1 min 16 s 258.68 ms remaining ; 1 min 24 s 731.87 ms total) Sun Oct 22 16:24:04 2023: Inserted ≈15% of D-proof conclusions. [11022736 of 73484910] (ETC: Sun Oct 22 16:25:20 2023 ; 1 min 15 s 683.77 ms remaining ; 1 min 29 s 39.72 ms total) Sun Oct 22 16:24:09 2023: Inserted ≈20% of D-proof conclusions. [14696982 of 73484910] (ETC: Sun Oct 22 16:25:21 2023 ; 1 min 12 s 637.15 ms remaining ; 1 min 30 s 796.44 ms total) Sun Oct 22 16:24:14 2023: Inserted ≈25% of D-proof conclusions. [18371227 of 73484910] (ETC: Sun Oct 22 16:25:23 2023 ; 1 min 9 s 240.69 ms remaining ; 1 min 32 s 320.91 ms total) Sun Oct 22 16:24:18 2023: Inserted ≈30% of D-proof conclusions. [22045473 of 73484910] (ETC: Sun Oct 22 16:25:22 2023 ; 1 min 4 s 240.81 ms remaining ; 1 min 31 s 772.58 ms total) Sun Oct 22 16:24:22 2023: Inserted ≈35% of D-proof conclusions. [25719718 of 73484910] (ETC: Sun Oct 22 16:25:20 2023 ; 58 s 426.13 ms remaining ; 1 min 29 s 886.36 ms total) Sun Oct 22 16:24:25 2023: Inserted ≈40% of D-proof conclusions. [29393964 of 73484910] (ETC: Sun Oct 22 16:25:16 2023 ; 51 s 119.94 ms remaining ; 1 min 25 s 199.90 ms total) Sun Oct 22 16:24:27 2023: Inserted ≈45% of D-proof conclusions. [33068209 of 73484910] (ETC: Sun Oct 22 16:25:12 2023 ; 44 s 905.87 ms remaining ; 1 min 21 s 647.04 ms total) Sun Oct 22 16:24:30 2023: Inserted ≈50% of D-proof conclusions. [36742455 of 73484910] (ETC: Sun Oct 22 16:25:09 2023 ; 39 s 483.20 ms remaining ; 1 min 18 s 966.41 ms total) Sun Oct 22 16:24:33 2023: Inserted ≈55% of D-proof conclusions. [40416700 of 73484910] (ETC: Sun Oct 22 16:25:07 2023 ; 34 s 607.79 ms remaining ; 1 min 16 s 906.20 ms total) Sun Oct 22 16:24:36 2023: Inserted ≈60% of D-proof conclusions. [44090946 of 73484910] (ETC: Sun Oct 22 16:25:07 2023 ; 30 s 507.08 ms remaining ; 1 min 16 s 267.69 ms total) Sun Oct 22 16:24:40 2023: Inserted ≈65% of D-proof conclusions. [47765191 of 73484910] (ETC: Sun Oct 22 16:25:06 2023 ; 26 s 585.29 ms remaining ; 1 min 15 s 957.98 ms total) Sun Oct 22 16:24:44 2023: Inserted ≈70% of D-proof conclusions. [51439437 of 73484910] (ETC: Sun Oct 22 16:25:06 2023 ; 22 s 789.58 ms remaining ; 1 min 15 s 965.28 ms total) Sun Oct 22 16:24:47 2023: Inserted ≈75% of D-proof conclusions. [55113682 of 73484910] (ETC: Sun Oct 22 16:25:06 2023 ; 18 s 985.75 ms remaining ; 1 min 15 s 943.00 ms total) Sun Oct 22 16:24:52 2023: Inserted ≈80% of D-proof conclusions. [58787928 of 73484910] (ETC: Sun Oct 22 16:25:08 2023 ; 15 s 427.84 ms remaining ; 1 min 17 s 139.19 ms total) Sun Oct 22 16:24:56 2023: Inserted ≈85% of D-proof conclusions. [62462173 of 73484910] (ETC: Sun Oct 22 16:25:08 2023 ; 11 s 593.41 ms remaining ; 1 min 17 s 289.42 ms total) Sun Oct 22 16:25:00 2023: Inserted ≈90% of D-proof conclusions. [66136419 of 73484910] (ETC: Sun Oct 22 16:25:08 2023 ; 7 s 709.05 ms remaining ; 1 min 17 s 90.47 ms total) Sun Oct 22 16:25:04 2023: Inserted ≈95% of D-proof conclusions. [69810664 of 73484910] (ETC: Sun Oct 22 16:25:08 2023 ; 3 s 866.25 ms remaining ; 1 min 17 s 324.97 ms total) Sun Oct 22 16:25:08 2023: Inserted 100% of D-proof conclusions. [73484910 of 73484910] (ETC: Sun Oct 22 16:25:08 2023 ; 0.00 ms remaining ; 1 min 17 s 241.20 ms total) 77246.43 ms (1 min 17 s 246.43 ms) total insertion duration. Sun Oct 22 16:25:08 2023: Starting to iterate D-proof candidates of length 157. 712657.78 ms (11 min 52 s 657.77 ms) taken to iterate 440272080 condensed detachment proof strings of length 157. [Copy] Next iteration count (unfiltered153+): { 157, 440272080 } Sun Oct 22 16:37:00 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sun Oct 22 16:39:04 2023: Process terminated. [pid: 53075, tid:23390181336960]