( 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-OPTANE MPI node — 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) — 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40688358 optane_low 64 COMPLETED 0:0 00:30:53 40688358.ba+ 64 COMPLETED 0:0 00:30:53 237150564K 40688358.ex+ 64 COMPLETED 0:0 00:30:53 0 By 237150564 KiB = (237150564 / 1024^2) GiB = 226.164402008056640625 GiB, it used approximately 226.16 gibibytes of memory. ) Wed Nov 8 20:10:12 2023: Process started. [pid: 220240, tid:22696559179648] 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). Wed Nov 8 20:10:12 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.43 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22696412825344] 1.28 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22696494753536] 0.85 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22696402319104] 0.46 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22696393914112] 0.19 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22696406521600] 0.35 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22696410724096] 0.84 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22696414926592] 0.36 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22696488449792] 0.07 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22696400217856] 0.86 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22696391812864] 0.17 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22696398116608] 4.92 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22696498956032] 4.78 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22696496854784] 9812.18 ms (9 s 812.18 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22696494753536] 9.26 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22696492652288] 14.60 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22696490551040] 16477.28 ms (16 s 477.28 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22696488449792] 2.39 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22696419129088] 2.89 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22696417027840] 15332.33 ms (15 s 332.33 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22696414926592] 8121.40 ms (8 s 121.40 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22696412825344] 14365.25 ms (14 s 365.25 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22696410724096] 5.42 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22696408622848] 13864.11 ms (13 s 864.11 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22696406521600] 13.16 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22696404420352] 10170.10 ms (10 s 170.10 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22696402319104] 17891.35 ms (17 s 891.35 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22696400217856] 18692.38 ms (18 s 692.38 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:22696398116608] 9.64 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22696396015360] 11378.75 ms (11 s 378.75 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22696393914112] 17992.72 ms (17 s 992.72 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:22696391812864] 11.13 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22696389711616] 8.08 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22696387610368] 7.49 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22696385509120] 4.10 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22696383407872] 14.46 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22696381306624] 7.16 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22696379205376] 11.34 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22696377104128] 4.62 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22696375002880] 5.56 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22696372901632] 8.89 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22696370800384] 16.05 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22696368699136] 0.63 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22696366597888] 34.58 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22696364496640] 164.31 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22696362395392] 32.15 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22696360294144] 238.87 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22696358192896] 103.27 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22696356091648] 37.91 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22694338754304] 481.11 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22694336653056] 36.93 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22694334551808] 36.83 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22694198232832] 87.58 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22694332450560] 50.16 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22694330349312] 628.01 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22694328248064] 135.89 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22694326146816] 61.36 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22694324045568] 344.79 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22694321944320] 662.16 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22694319843072] 1202.99 ms (1 s 202.99 ms) taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22694317741824] 1081.73 ms (1 s 81.73 ms) taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22694315640576] 1363.84 ms (1 s 363.84 ms) taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22694313539328] 395.65 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22694311438080] 1605.45 ms (1 s 605.45 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22694309336832] 1682.84 ms (1 s 682.84 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22694307235584] 1841.41 ms (1 s 841.41 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22694305134336] 1870.48 ms (1 s 870.48 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22694303033088] 3438.49 ms (3 s 438.49 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22694300931840] 3409.71 ms (3 s 409.71 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22694298830592] 4805.57 ms (4 s 805.57 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22694296729344] 3340.64 ms (3 s 340.64 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22694294628096] 4237.82 ms (4 s 237.82 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22694292526848] 4914.52 ms (4 s 914.52 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22694290425600] 5898.13 ms (5 s 898.13 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22694288324352] 7030.50 ms (7 s 30.50 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22694286223104] 18834.84 ms (18 s 834.84 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. 48741.97 ms (48 s 741.97 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:22694286223104] 62171.82 ms (1 min 2 s 171.82 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:22694288324352] 77359.21 ms (1 min 17 s 359.21 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:22694290425600] 86670.60 ms (1 min 26 s 670.60 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:22694292526848] 86681.37 ms (1 min 26 s 681.37 ms) additional read duration. Loaded 4 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 162335238 representatives in total. Wed Nov 8 20:12:17 2023: Inserted ≈ 5% of D-proof conclusions. [ 8116761 of 162335238] (ETC: Wed Nov 8 20:18:26 2023 ; 6 min 9 s 8.11 ms remaining ; 6 min 28 s 429.58 ms total) Wed Nov 8 20:12:37 2023: Inserted ≈10% of D-proof conclusions. [ 16233523 of 162335238] (ETC: Wed Nov 8 20:18:29 2023 ; 5 min 52 s 224.05 ms remaining ; 6 min 31 s 360.05 ms total) Wed Nov 8 20:12:55 2023: Inserted ≈15% of D-proof conclusions. [ 24350285 of 162335238] (ETC: Wed Nov 8 20:18:23 2023 ; 5 min 27 s 371.03 ms remaining ; 6 min 25 s 142.38 ms total) Wed Nov 8 20:13:09 2023: Inserted ≈20% of D-proof conclusions. [ 32467047 of 162335238] (ETC: Wed Nov 8 20:17:54 2023 ; 4 min 45 s 240.02 ms remaining ; 5 min 56 s 550.02 ms total) Wed Nov 8 20:13:23 2023: Inserted ≈25% of D-proof conclusions. [ 40583809 of 162335238] (ETC: Wed Nov 8 20:17:39 2023 ; 4 min 16 s 185.70 ms remaining ; 5 min 41 s 580.93 ms total) Wed Nov 8 20:13:38 2023: Inserted ≈30% of D-proof conclusions. [ 48700571 of 162335238] (ETC: Wed Nov 8 20:17:32 2023 ; 3 min 53 s 827.70 ms remaining ; 5 min 34 s 39.57 ms total) Wed Nov 8 20:13:52 2023: Inserted ≈35% of D-proof conclusions. [ 56817333 of 162335238] (ETC: Wed Nov 8 20:17:25 2023 ; 3 min 32 s 834.36 ms remaining ; 5 min 27 s 437.48 ms total) Wed Nov 8 20:14:07 2023: Inserted ≈40% of D-proof conclusions. [ 64934095 of 162335238] (ETC: Wed Nov 8 20:17:21 2023 ; 3 min 14 s 303.67 ms remaining ; 5 min 23 s 839.45 ms total) Wed Nov 8 20:14:22 2023: Inserted ≈45% of D-proof conclusions. [ 73050857 of 162335238] (ETC: Wed Nov 8 20:17:19 2023 ; 2 min 56 s 796.09 ms remaining ; 5 min 21 s 447.44 ms total) Wed Nov 8 20:14:36 2023: Inserted ≈50% of D-proof conclusions. [ 81167619 of 162335238] (ETC: Wed Nov 8 20:17:15 2023 ; 2 min 38 s 986.25 ms remaining ; 5 min 17 s 972.51 ms total) Wed Nov 8 20:14:52 2023: Inserted ≈55% of D-proof conclusions. [ 89284380 of 162335238] (ETC: Wed Nov 8 20:17:15 2023 ; 2 min 22 s 978.16 ms remaining ; 5 min 17 s 729.24 ms total) Wed Nov 8 20:15:07 2023: Inserted ≈60% of D-proof conclusions. [ 97401142 of 162335238] (ETC: Wed Nov 8 20:17:14 2023 ; 2 min 6 s 421.94 ms remaining ; 5 min 16 s 54.85 ms total) Wed Nov 8 20:15:22 2023: Inserted ≈65% of D-proof conclusions. [105517904 of 162335238] (ETC: Wed Nov 8 20:17:12 2023 ; 1 min 50 s 208.38 ms remaining ; 5 min 14 s 881.09 ms total) Wed Nov 8 20:15:38 2023: Inserted ≈70% of D-proof conclusions. [113634666 of 162335238] (ETC: Wed Nov 8 20:17:12 2023 ; 1 min 34 s 334.00 ms remaining ; 5 min 14 s 446.68 ms total) Wed Nov 8 20:15:53 2023: Inserted ≈75% of D-proof conclusions. [121751428 of 162335238] (ETC: Wed Nov 8 20:17:11 2023 ; 1 min 18 s 425.55 ms remaining ; 5 min 13 s 702.19 ms total) Wed Nov 8 20:16:09 2023: Inserted ≈80% of D-proof conclusions. [129868190 of 162335238] (ETC: Wed Nov 8 20:17:12 2023 ; 1 min 2 s 835.51 ms remaining ; 5 min 14 s 177.57 ms total) Wed Nov 8 20:16:25 2023: Inserted ≈85% of D-proof conclusions. [137984952 of 162335238] (ETC: Wed Nov 8 20:17:13 2023 ; 47 s 285.96 ms remaining ; 5 min 15 s 239.74 ms total) Wed Nov 8 20:16:40 2023: Inserted ≈90% of D-proof conclusions. [146101714 of 162335238] (ETC: Wed Nov 8 20:17:12 2023 ; 31 s 403.95 ms remaining ; 5 min 14 s 39.47 ms total) Wed Nov 8 20:16:56 2023: Inserted ≈95% of D-proof conclusions. [154218476 of 162335238] (ETC: Wed Nov 8 20:17:11 2023 ; 15 s 686.96 ms remaining ; 5 min 13 s 739.11 ms total) Wed Nov 8 20:17:11 2023: Inserted 100% of D-proof conclusions. [162335238 of 162335238] (ETC: Wed Nov 8 20:17:11 2023 ; 0.00 ms remaining ; 5 min 13 s 362.79 ms total) 313364.28 ms (5 min 13 s 364.28 ms) total insertion duration. Wed Nov 8 20:17:11 2023: Starting to iterate D-proof candidates of length 161. 1005699.60 ms (16 min 45 s 699.60 ms) taken to iterate 784979956 condensed detachment proof strings of length 161. [Copy] Next iteration count (unfiltered153+): { 161, 784979956 } Wed Nov 8 20:33:57 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Wed Nov 8 20:40:49 2023: Process terminated. [pid: 220240, tid:22696559179648]