( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40281905 c18m_low 48 COMPLETED 0:0 00:06:59 40281905.ba+ 48 COMPLETED 0:0 00:06:59 22144164K 40281905.ex+ 48 COMPLETED 0:0 00:06:59 0 By 22144164 KiB = (22144164 / 1024^2) GiB = 21.118320465087890625 GiB, it used approximately 21.12 gibibytes of memory. ) Sun Oct 22 07:19:29 2023: Process started. [pid: 199216, tid:23129602705280] 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 07:19:29 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 5.08 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23129513039616] 2.18 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23129536153344] 1.09 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23129523545856] 1.24 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23129534052096] 1.34 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23129519343360] 0.25 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23129542457088] 1.06 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23129477318400] 1.70 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23129538254592] 1.80 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23129529849600] 0.17 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23129500432128] 0.30 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23129517242112] 0.50 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23129508837120] 1.12 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23129498330880] 0.02 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23129506735872] 0.12 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23129502533376] 0.23 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23129527748352] 0.45 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23129494128384] 0.89 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23129510938368] 1.40 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23129521444608] 0.93 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23129515140864] 1.03 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23129540355840] 0.75 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23129481520896] 0.19 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23129531950848] 0.30 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23129485723392] 0.00 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23129489925888] 0.38 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23129525647104] 1357.97 ms (1 s 357.97 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23129542457088] 5593.46 ms (5 s 593.46 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23129540355840] 2945.22 ms (2 s 945.22 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23129538254592] 336.01 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23129536153344] 668.72 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23129534052096] 6605.87 ms (6 s 605.87 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23129531950848] 4002.35 ms (4 s 2.35 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23129529849600] 2495.10 ms (2 s 495.10 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23129527748352] 8499.17 ms (8 s 499.17 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23129525647104] 478.83 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23129523545856] 4100.31 ms (4 s 100.31 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23129521444608] 930.47 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23129519343360] 8741.94 ms (8 s 741.94 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23129517242112] 4792.43 ms (4 s 792.43 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23129515140864] 194.33 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23129513039616] 3478.95 ms (3 s 478.95 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23129510938368] 1118.87 ms (1 s 118.87 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23129508837120] 1801.23 ms (1 s 801.23 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23129506735872] 0.04 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23129504634624] 2103.17 ms (2 s 103.17 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23129502533376] 7109.50 ms (7 s 109.50 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23129500432128] 1360.91 ms (1 s 360.91 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23129498330880] 10.43 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23129496229632] 2969.68 ms (2 s 969.68 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23129494128384] 8.46 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23129492027136] 8009.45 ms (8 s 9.46 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23129489925888] 1.38 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23129487824640] 7287.86 ms (7 s 287.86 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23129485723392] 6.10 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23129483622144] 6226.72 ms (6 s 226.72 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23129481520896] 1.67 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23129479419648] 1885.03 ms (1 s 885.03 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23129477318400] 7.22 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23129475217152] 12.21 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23127258035968] 28.92 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23127121716992] 17.26 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23127255934720] 24.23 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23127253833472] 23.86 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23127251732224] 38.78 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23127249630976] 38.69 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23127247529728] 42.13 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23127245428480] 28.73 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23127243327232] 45.43 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23127241225984] 43.02 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23127239124736] 35.42 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23127237023488] 58.37 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23127234922240] 112.35 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23127232820992] 158.36 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23127230719744] 8804.84 ms (8 s 804.84 ms) total read duration. Loaded 75 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 19520862 representatives in total. Sun Oct 22 07:19:39 2023: Inserted ≈ 5% of D-proof conclusions. [ 976043 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 18 s 834.70 ms remaining ; 19 s 826.00 ms total) Sun Oct 22 07:19:40 2023: Inserted ≈10% of D-proof conclusions. [ 1952086 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 17 s 687.26 ms remaining ; 19 s 652.51 ms total) Sun Oct 22 07:19:40 2023: Inserted ≈15% of D-proof conclusions. [ 2928129 of 19520862] (ETC: Sun Oct 22 07:19:56 2023 ; 15 s 464.82 ms remaining ; 18 s 193.90 ms total) Sun Oct 22 07:19:41 2023: Inserted ≈20% of D-proof conclusions. [ 3904172 of 19520862] (ETC: Sun Oct 22 07:19:55 2023 ; 13 s 873.97 ms remaining ; 17 s 342.47 ms total) Sun Oct 22 07:19:42 2023: Inserted ≈25% of D-proof conclusions. [ 4880215 of 19520862] (ETC: Sun Oct 22 07:19:55 2023 ; 13 s 131.68 ms remaining ; 17 s 508.91 ms total) Sun Oct 22 07:19:43 2023: Inserted ≈30% of D-proof conclusions. [ 5856258 of 19520862] (ETC: Sun Oct 22 07:19:56 2023 ; 12 s 575.31 ms remaining ; 17 s 964.73 ms total) Sun Oct 22 07:19:44 2023: Inserted ≈35% of D-proof conclusions. [ 6832301 of 19520862] (ETC: Sun Oct 22 07:19:56 2023 ; 12 s 104.39 ms remaining ; 18 s 622.13 ms total) Sun Oct 22 07:19:45 2023: Inserted ≈40% of D-proof conclusions. [ 7808344 of 19520862] (ETC: Sun Oct 22 07:19:56 2023 ; 11 s 301.64 ms remaining ; 18 s 836.07 ms total) Sun Oct 22 07:19:46 2023: Inserted ≈45% of D-proof conclusions. [ 8784387 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 10 s 817.09 ms remaining ; 19 s 667.44 ms total) Sun Oct 22 07:19:48 2023: Inserted ≈50% of D-proof conclusions. [ 9760431 of 19520862] (ETC: Sun Oct 22 07:19:58 2023 ; 9 s 957.55 ms remaining ; 19 s 915.09 ms total) Sun Oct 22 07:19:49 2023: Inserted ≈55% of D-proof conclusions. [10736474 of 19520862] (ETC: Sun Oct 22 07:19:58 2023 ; 9 s 1.37 ms remaining ; 20 s 3.05 ms total) Sun Oct 22 07:19:50 2023: Inserted ≈60% of D-proof conclusions. [11712517 of 19520862] (ETC: Sun Oct 22 07:19:58 2023 ; 7 s 972.93 ms remaining ; 19 s 932.32 ms total) Sun Oct 22 07:19:50 2023: Inserted ≈65% of D-proof conclusions. [12688560 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 6 s 945.07 ms remaining ; 19 s 843.06 ms total) Sun Oct 22 07:19:52 2023: Inserted ≈70% of D-proof conclusions. [13664603 of 19520862] (ETC: Sun Oct 22 07:19:58 2023 ; 5 s 990.97 ms remaining ; 19 s 969.91 ms total) Sun Oct 22 07:19:52 2023: Inserted ≈75% of D-proof conclusions. [14640646 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 4 s 945.17 ms remaining ; 19 s 780.66 ms total) Sun Oct 22 07:19:53 2023: Inserted ≈80% of D-proof conclusions. [15616689 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 3 s 942.01 ms remaining ; 19 s 710.04 ms total) Sun Oct 22 07:19:54 2023: Inserted ≈85% of D-proof conclusions. [16592732 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 2 s 936.88 ms remaining ; 19 s 579.19 ms total) Sun Oct 22 07:19:55 2023: Inserted ≈90% of D-proof conclusions. [17568775 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 1 s 954.66 ms remaining ; 19 s 546.56 ms total) Sun Oct 22 07:19:56 2023: Inserted ≈95% of D-proof conclusions. [18544818 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 979.37 ms remaining ; 19 s 587.29 ms total) Sun Oct 22 07:19:57 2023: Inserted 100% of D-proof conclusions. [19520862 of 19520862] (ETC: Sun Oct 22 07:19:57 2023 ; 0.00 ms remaining ; 19 s 513.08 ms total) 19513.41 ms (19 s 513.41 ms) total insertion duration. Sun Oct 22 07:19:57 2023: Starting to iterate D-proof candidates of length 151. 352639.38 ms (5 min 52 s 639.38 ms) taken to iterate 187924390 condensed detachment proof strings of length 151. [Copy] Next iteration count (filtered): { 151, 187924390 } Sun Oct 22 07:25:50 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sun Oct 22 07:26:23 2023: Process terminated. [pid: 199216, tid:23129602705280]