( This log file was generated by '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. Wall-clock time: 31.4641666… h CPU utilization: 2013.70666… core-h ) Sun Nov 12 08:39:03 2023: Process started. [pid: 73613, tid:22578865051520] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(167, 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 generateDProofRepresentativeFiles(167, false, true). Sun Nov 12 08:39:03 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 167, unfiltered] 0.01 ms taken to load initial representatives. 3.83 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22578781689600] 4.73 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22578804803328] 0.68 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22578800600832] 0.04 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22578802702080] 0.41 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22578792195840] 4.45 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22578571761408] 1.66 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22578565457664] 0.93 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22578575963904] 1.43 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22578563356416] 0.22 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22578552850176] 0.01 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22578557052672] 7855.61 ms (7 s 855.61 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22578804803328] 9500.10 ms (9 s 500.10 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22578802702080] 9365.71 ms (9 s 365.71 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22578800600832] 0.97 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22578798499584] 0.86 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22578796398336] 0.86 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22578794297088] 11749.81 ms (11 s 749.81 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22578792195840] 4.25 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22578790094592] 2.11 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22578787993344] 1.36 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22578785892096] 5.42 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22578783790848] 6874.82 ms (6 s 874.82 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22578781689600] 0.81 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22578779588352] 15759.62 ms (15 s 759.62 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22578575963904] 6.78 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22578573862656] 13195.36 ms (13 s 195.36 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22578571761408] 2.73 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22578569660160] 0.65 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22578567558912] 13703.00 ms (13 s 703.00 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22578565457664] 15722.11 ms (15 s 722.11 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22578563356416] 3.85 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22578561255168] 8.13 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22578559153920] 16835.31 ms (16 s 835.31 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:22578557052672] 6.21 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22578554951424] 16224.19 ms (16 s 224.19 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:22578552850176] 17.73 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22578550748928] 11.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22578548647680] 6.84 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22578546546432] 14.82 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22578544445184] 12.63 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22578542343936] 13.07 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22578540242688] 37.11 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22578538141440] 20.70 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22578536040192] 16.01 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22578533938944] 18.55 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22578531837696] 10.38 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22578529736448] 32.00 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22578527635200] 86.56 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22578525533952] 35.40 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22578523432704] 401.08 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22578521331456] 356.65 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22578519230208] 257.49 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22578517128960] 183.56 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22578515027712] 44.84 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22578512926464] 421.89 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22576629806848] 45.79 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22576627705600] 76.51 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22576625604352] 535.55 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22576623503104] 661.03 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22576621401856] 475.78 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22576619300608] 378.71 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22576617199360] 220.70 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22576615098112] 1495.08 ms (1 s 495.08 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22576612996864] 1823.61 ms (1 s 823.61 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22576610895616] 1879.50 ms (1 s 879.50 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22576608794368] 1974.19 ms (1 s 974.19 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22576606693120] 2736.23 ms (2 s 736.23 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22576604591872] 4485.50 ms (4 s 485.50 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22576602490624] 3553.64 ms (3 s 553.64 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22576600389376] 3288.04 ms (3 s 288.04 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22576598288128] 4065.08 ms (4 s 65.08 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22576596186880] 4508.09 ms (4 s 508.09 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22576594085632] 5178.95 ms (5 s 178.95 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22576591984384] 5534.28 ms (5 s 534.28 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22576589883136] 17003.66 ms (17 s 3.66 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. 150858.48 ms (2 min 30 s 858.48 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:22576589883136] 184028.86 ms (3 min 4 s 28.86 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:22576591984384] 225600.33 ms (3 min 45 s 600.33 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:22576594085632] 262775.71 ms (4 min 22 s 775.71 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:22576596186880] 320030.08 ms (5 min 20 s 30.08 ms) taken to read 78239557 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. [tid:22576598288128] 353527.72 ms (5 min 53 s 527.72 ms) taken to read 101757325 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt. [tid:22576600389376] 415693.84 ms (6 min 55 s 693.84 ms) taken to read 147063822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs165-unfiltered153+.txt. [tid:22576602490624] 415736.88 ms (6 min 55 s 736.88 ms) additional read duration. Loaded 7 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 161 : 78239557 163 : 101757325 165 : 147063822 489395942 representatives in total. Sun Nov 12 08:47:07 2023: Inserted ≈ 5% of D-proof conclusions. [ 24469797 of 489395942] (ETC: Sun Nov 12 09:03:29 2023 ; 16 min 21 s 322.97 ms remaining ; 17 min 12 s 971.54 ms total) Sun Nov 12 08:48:13 2023: Inserted ≈10% of D-proof conclusions. [ 48939594 of 489395942] (ETC: Sun Nov 12 09:05:48 2023 ; 17 min 35 s 322.91 ms remaining ; 19 min 32 s 581.01 ms total) Sun Nov 12 08:49:28 2023: Inserted ≈15% of D-proof conclusions. [ 73409391 of 489395942] (ETC: Sun Nov 12 09:07:35 2023 ; 18 min 7 s 522.85 ms remaining ; 21 min 19 s 438.64 ms total) Sun Nov 12 08:50:40 2023: Inserted ≈20% of D-proof conclusions. [ 97879188 of 489395942] (ETC: Sun Nov 12 09:08:17 2023 ; 17 min 37 s 155.36 ms remaining ; 22 min 1 s 444.19 ms total) Sun Nov 12 08:51:53 2023: Inserted ≈25% of D-proof conclusions. [122348985 of 489395942] (ETC: Sun Nov 12 09:08:45 2023 ; 16 min 51 s 845.31 ms remaining ; 22 min 29 s 127.08 ms total) Sun Nov 12 08:53:10 2023: Inserted ≈30% of D-proof conclusions. [146818782 of 489395942] (ETC: Sun Nov 12 09:09:16 2023 ; 16 min 5 s 952.75 ms remaining ; 22 min 59 s 932.50 ms total) Sun Nov 12 08:54:22 2023: Inserted ≈35% of D-proof conclusions. [171288579 of 489395942] (ETC: Sun Nov 12 09:09:25 2023 ; 15 min 2 s 810.52 ms remaining ; 23 min 8 s 939.26 ms total) Sun Nov 12 08:55:39 2023: Inserted ≈40% of D-proof conclusions. [195758376 of 489395942] (ETC: Sun Nov 12 09:09:44 2023 ; 14 min 4 s 748.94 ms remaining ; 23 min 27 s 914.89 ms total) Sun Nov 12 08:56:54 2023: Inserted ≈45% of D-proof conclusions. [220228173 of 489395942] (ETC: Sun Nov 12 09:09:53 2023 ; 12 min 59 s 796.46 ms remaining ; 23 min 37 s 811.74 ms total) Sun Nov 12 08:58:14 2023: Inserted ≈50% of D-proof conclusions. [244697971 of 489395942] (ETC: Sun Nov 12 09:10:13 2023 ; 11 min 58 s 828.01 ms remaining ; 23 min 57 s 656.03 ms total) Sun Nov 12 08:59:28 2023: Inserted ≈55% of D-proof conclusions. [269167768 of 489395942] (ETC: Sun Nov 12 09:10:16 2023 ; 10 min 48 s 175.69 ms remaining ; 24 min 390.41 ms total) Sun Nov 12 09:00:45 2023: Inserted ≈60% of D-proof conclusions. [293637565 of 489395942] (ETC: Sun Nov 12 09:10:24 2023 ; 9 min 39 s 326.10 ms remaining ; 24 min 8 s 315.24 ms total) Sun Nov 12 09:02:15 2023: Inserted ≈65% of D-proof conclusions. [318107362 of 489395942] (ETC: Sun Nov 12 09:10:51 2023 ; 8 min 36 s 469.44 ms remaining ; 24 min 35 s 626.96 ms total) Sun Nov 12 09:03:44 2023: Inserted ≈70% of D-proof conclusions. [342577159 of 489395942] (ETC: Sun Nov 12 09:11:13 2023 ; 7 min 29 s 260.54 ms remaining ; 24 min 57 s 535.12 ms total) Sun Nov 12 09:04:47 2023: Inserted ≈75% of D-proof conclusions. [367046956 of 489395942] (ETC: Sun Nov 12 09:10:57 2023 ; 6 min 10 s 413.98 ms remaining ; 24 min 41 s 655.91 ms total) Sun Nov 12 09:05:56 2023: Inserted ≈80% of D-proof conclusions. [391516753 of 489395942] (ETC: Sun Nov 12 09:10:51 2023 ; 4 min 55 s 74.71 ms remaining ; 24 min 35 s 373.54 ms total) Sun Nov 12 09:07:07 2023: Inserted ≈85% of D-proof conclusions. [415986550 of 489395942] (ETC: Sun Nov 12 09:10:48 2023 ; 3 min 40 s 905.26 ms remaining ; 24 min 32 s 701.74 ms total) Sun Nov 12 09:08:30 2023: Inserted ≈90% of D-proof conclusions. [440456347 of 489395942] (ETC: Sun Nov 12 09:10:58 2023 ; 2 min 28 s 281.64 ms remaining ; 24 min 42 s 816.38 ms total) Sun Nov 12 09:10:08 2023: Inserted ≈95% of D-proof conclusions. [464926144 of 489395942] (ETC: Sun Nov 12 09:11:23 2023 ; 1 min 15 s 373.02 ms remaining ; 25 min 7 s 460.31 ms total) Sun Nov 12 09:11:37 2023: Inserted 100% of D-proof conclusions. [489395942 of 489395942] (ETC: Sun Nov 12 09:11:37 2023 ; 0.00 ms remaining ; 25 min 21 s 131.21 ms total) 1521132.65 ms (25 min 21 s 132.65 ms) total insertion duration. Known iteration count loaded from 167:2016753823. Sun Nov 12 09:11:37 2023: Starting to generate D-proof representatives of length 167. Sun Nov 12 09:44:06 2023: Iterated ≈ 2% of D-proof candidates. [ 40335076 of 2016753823] (ETC: Mon Nov 13 12:15:50 2023 ; 1 d 2 h 31 min 44 s 340.85 ms remaining ; 1 d 3 h 4 min 13 s 409.01 ms total) Sun Nov 12 10:13:47 2023: Iterated ≈ 4% of D-proof candidates. [ 80670152 of 2016753823] (ETC: Mon Nov 13 11:05:49 2023 ; 1 d 52 min 1 s 759.78 ms remaining ; 1 d 1 h 54 min 11 s 833.06 ms total) Sun Nov 12 10:44:40 2023: Iterated ≈ 6% of D-proof candidates. [ 121005229 of 2016753823] (ETC: Mon Nov 13 11:02:22 2023 ; 1 d 17 min 42 s 869.98 ms remaining ; 1 d 1 h 50 min 45 s 606.34 ms total) Sun Nov 12 11:15:12 2023: Iterated ≈ 8% of D-proof candidates. [ 161340305 of 2016753823] (ETC: Mon Nov 13 10:56:28 2023 ; 23 h 41 min 16 s 134.57 ms remaining ; 1 d 1 h 44 min 51 s 450.58 ms total) Sun Nov 12 11:48:41 2023: Iterated ≈10% of D-proof candidates. [ 201675382 of 2016753823] (ETC: Mon Nov 13 11:22:17 2023 ; 23 h 33 min 36 s 591.93 ms remaining ; 1 d 2 h 10 min 40 s 657.68 ms total) Sun Nov 12 12:22:56 2023: Iterated ≈12% of D-proof candidates. [ 242010458 of 2016753823] (ETC: Mon Nov 13 11:45:59 2023 ; 23 h 23 min 2 s 709.32 ms remaining ; 1 d 2 h 34 min 22 s 169.64 ms total) Sun Nov 12 12:57:58 2023: Iterated ≈14% of D-proof candidates. [ 282345535 of 2016753823] (ETC: Mon Nov 13 12:08:25 2023 ; 23 h 10 min 26 s 626.82 ms remaining ; 1 d 2 h 56 min 47 s 705.60 ms total) Sun Nov 12 13:37:05 2023: Iterated ≈16% of D-proof candidates. [ 322680611 of 2016753823] (ETC: Mon Nov 13 12:50:47 2023 ; 23 h 13 min 42 s 125.75 ms remaining ; 1 d 3 h 39 min 10 s 149.66 ms total) Sun Nov 12 14:12:53 2023: Iterated ≈18% of D-proof candidates. [ 363015688 of 2016753823] (ETC: Mon Nov 13 13:05:21 2023 ; 22 h 52 min 27 s 847.08 ms remaining ; 1 d 3 h 53 min 44 s 203.74 ms total) Sun Nov 12 14:50:50 2023: Iterated ≈20% of D-proof candidates. [ 403350764 of 2016753823] (ETC: Mon Nov 13 13:27:42 2023 ; 22 h 36 min 51 s 968.25 ms remaining ; 1 d 4 h 16 min 4 s 960.28 ms total) Sun Nov 12 15:33:53 2023: Iterated ≈22% of D-proof candidates. [ 443685841 of 2016753823] (ETC: Mon Nov 13 14:09:14 2023 ; 22 h 35 min 20 s 657.59 ms remaining ; 1 d 4 h 57 min 37 s 253.31 ms total) Sun Nov 12 16:11:30 2023: Iterated ≈24% of D-proof candidates. [ 484020917 of 2016753823] (ETC: Mon Nov 13 14:21:10 2023 ; 22 h 9 min 39 s 902.02 ms remaining ; 1 d 5 h 9 min 33 s 555.25 ms total) Sun Nov 12 16:57:24 2023: Iterated ≈26% of D-proof candidates. [ 524355993 of 2016753823] (ETC: Mon Nov 13 15:03:07 2023 ; 22 h 5 min 42 s 495.63 ms remaining ; 1 d 5 h 51 min 29 s 858.89 ms total) Sun Nov 12 17:45:01 2023: Iterated ≈28% of D-proof candidates. [ 564691070 of 2016753823] (ETC: Mon Nov 13 15:45:11 2023 ; 22 h 10 s 383.03 ms remaining ; 1 d 6 h 33 min 34 s 420.84 ms total) Sun Nov 12 18:32:14 2023: Iterated ≈30% of D-proof candidates. [ 605026146 of 2016753823] (ETC: Mon Nov 13 16:20:19 2023 ; 21 h 48 min 5 s 867.40 ms remaining ; 1 d 7 h 8 min 42 s 667.64 ms total) Sun Nov 12 19:10:12 2023: Iterated ≈32% of D-proof candidates. [ 645361223 of 2016753823] (ETC: Mon Nov 13 16:22:12 2023 ; 21 h 11 min 59 s 717.41 ms remaining ; 1 d 7 h 10 min 34 s 878.51 ms total) Sun Nov 12 19:57:58 2023: Iterated ≈34% of D-proof candidates. [ 685696299 of 2016753823] (ETC: Mon Nov 13 16:52:39 2023 ; 20 h 54 min 41 s 44.69 ms remaining ; 1 d 7 h 41 min 2 s 188.85 ms total) Sun Nov 12 20:45:07 2023: Iterated ≈36% of D-proof candidates. [ 726031376 of 2016753823] (ETC: Mon Nov 13 17:18:01 2023 ; 20 h 32 min 53 s 621.26 ms remaining ; 1 d 8 h 6 min 23 s 783.19 ms total) Sun Nov 12 21:24:43 2023: Iterated ≈38% of D-proof candidates. [ 766366452 of 2016753823] (ETC: Mon Nov 13 17:20:49 2023 ; 19 h 56 min 6 s 218.14 ms remaining ; 1 d 8 h 9 min 11 s 964.67 ms total) Sun Nov 12 22:05:20 2023: Iterated ≈40% of D-proof candidates. [ 806701529 of 2016753823] (ETC: Mon Nov 13 17:25:55 2023 ; 19 h 20 min 34 s 681.75 ms remaining ; 1 d 8 h 14 min 17 s 802.90 ms total) Sun Nov 12 22:45:55 2023: Iterated ≈42% of D-proof candidates. [ 847036605 of 2016753823] (ETC: Mon Nov 13 17:30:25 2023 ; 18 h 44 min 30 s 246.49 ms remaining ; 1 d 8 h 18 min 48 s 11.12 ms total) Sun Nov 12 23:24:03 2023: Iterated ≈44% of D-proof candidates. [ 887371682 of 2016753823] (ETC: Mon Nov 13 17:28:58 2023 ; 18 h 4 min 55 s 31.15 ms remaining ; 1 d 8 h 17 min 21 s 127.04 ms total) Mon Nov 13 00:05:07 2023: Iterated ≈46% of D-proof candidates. [ 927706758 of 2016753823] (ETC: Mon Nov 13 17:34:00 2023 ; 17 h 28 min 53 s 240.20 ms remaining ; 1 d 8 h 22 min 23 s 37.34 ms total) Mon Nov 13 00:52:23 2023: Iterated ≈48% of D-proof candidates. [ 968041835 of 2016753823] (ETC: Mon Nov 13 17:51:33 2023 ; 16 h 59 min 9 s 768.27 ms remaining ; 1 d 8 h 39 min 55 s 708.20 ms total) Mon Nov 13 01:31:04 2023: Iterated ≈50% of D-proof candidates. [1008376911 of 2016753823] (ETC: Mon Nov 13 17:50:31 2023 ; 16 h 19 min 26 s 981.63 ms remaining ; 1 d 8 h 38 min 53 s 963.21 ms total) Mon Nov 13 02:09:48 2023: Iterated ≈52% of D-proof candidates. [1048711987 of 2016753823] (ETC: Mon Nov 13 17:49:39 2023 ; 15 h 39 min 51 s 577.27 ms remaining ; 1 d 8 h 38 min 2 s 452.54 ms total) Mon Nov 13 02:50:39 2023: Iterated ≈54% of D-proof candidates. [1089047064 of 2016753823] (ETC: Mon Nov 13 17:52:47 2023 ; 15 h 2 min 8 s 391.95 ms remaining ; 1 d 8 h 41 min 10 s 417.22 ms total) Mon Nov 13 03:28:02 2023: Iterated ≈56% of D-proof candidates. [1129382140 of 2016753823] (ETC: Mon Nov 13 17:49:30 2023 ; 14 h 21 min 28 s 365.31 ms remaining ; 1 d 8 h 37 min 53 s 557.41 ms total) Mon Nov 13 04:08:33 2023: Iterated ≈58% of D-proof candidates. [1169717217 of 2016753823] (ETC: Mon Nov 13 17:51:50 2023 ; 13 h 43 min 17 s 661.99 ms remaining ; 1 d 8 h 40 min 13 s 480.88 ms total) Mon Nov 13 04:46:50 2023: Iterated ≈60% of D-proof candidates. [1210052293 of 2016753823] (ETC: Mon Nov 13 17:50:18 2023 ; 13 h 3 min 28 s 604.62 ms remaining ; 1 d 8 h 38 min 41 s 511.43 ms total) Mon Nov 13 05:23:03 2023: Iterated ≈62% of D-proof candidates. [1250387370 of 2016753823] (ETC: Mon Nov 13 17:45:32 2023 ; 12 h 22 min 29 s 415.30 ms remaining ; 1 d 8 h 33 min 55 s 303.37 ms total) Mon Nov 13 05:57:34 2023: Iterated ≈64% of D-proof candidates. [1290722446 of 2016753823] (ETC: Mon Nov 13 17:38:26 2023 ; 11 h 40 min 51 s 157.21 ms remaining ; 1 d 8 h 26 min 48 s 769.91 ms total) Mon Nov 13 06:30:30 2023: Iterated ≈66% of D-proof candidates. [1331057523 of 2016753823] (ETC: Mon Nov 13 17:29:19 2023 ; 10 h 58 min 49 s 45.34 ms remaining ; 1 d 8 h 17 min 41 s 898.02 ms total) Mon Nov 13 07:02:33 2023: Iterated ≈68% of D-proof candidates. [1371392599 of 2016753823] (ETC: Mon Nov 13 17:19:27 2023 ; 10 h 16 min 54 s 411.47 ms remaining ; 1 d 8 h 7 min 50 s 35.72 ms total) Mon Nov 13 07:33:28 2023: Iterated ≈70% of D-proof candidates. [1411727676 of 2016753823] (ETC: Mon Nov 13 17:08:33 2023 ; 9 h 35 min 4 s 798.84 ms remaining ; 1 d 7 h 56 min 55 s 996.11 ms total) Mon Nov 13 08:03:37 2023: Iterated ≈72% of D-proof candidates. [1452062752 of 2016753823] (ETC: Mon Nov 13 16:57:10 2023 ; 8 h 53 min 33 s 399.65 ms remaining ; 1 d 7 h 45 min 33 s 570.08 ms total) Mon Nov 13 08:33:14 2023: Iterated ≈74% of D-proof candidates. [1492397829 of 2016753823] (ETC: Mon Nov 13 16:45:41 2023 ; 8 h 12 min 27 s 534.95 ms remaining ; 1 d 7 h 34 min 4 s 365.19 ms total) Mon Nov 13 09:02:05 2023: Iterated ≈76% of D-proof candidates. [1532732905 of 2016753823] (ETC: Mon Nov 13 16:33:49 2023 ; 7 h 31 min 43 s 634.61 ms remaining ; 1 d 7 h 22 min 11 s 810.76 ms total) Mon Nov 13 09:30:31 2023: Iterated ≈78% of D-proof candidates. [1573067981 of 2016753823] (ETC: Mon Nov 13 16:22:00 2023 ; 6 h 51 min 29 s 193.06 ms remaining ; 1 d 7 h 10 min 23 s 604.58 ms total) Mon Nov 13 09:58:24 2023: Iterated ≈80% of D-proof candidates. [1613403058 of 2016753823] (ETC: Mon Nov 13 16:10:06 2023 ; 6 h 11 min 41 s 763.18 ms remaining ; 1 d 6 h 58 min 28 s 815.78 ms total) Mon Nov 13 10:25:51 2023: Iterated ≈82% of D-proof candidates. [1653738134 of 2016753823] (ETC: Mon Nov 13 15:58:14 2023 ; 5 h 32 min 23 s 557.07 ms remaining ; 1 d 6 h 46 min 37 s 539.03 ms total) Mon Nov 13 10:52:53 2023: Iterated ≈84% of D-proof candidates. [1694073211 of 2016753823] (ETC: Mon Nov 13 15:46:28 2023 ; 4 h 53 min 34 s 570.93 ms remaining ; 1 d 6 h 34 min 51 s 68.18 ms total) Mon Nov 13 11:19:31 2023: Iterated ≈86% of D-proof candidates. [1734408287 of 2016753823] (ETC: Mon Nov 13 15:34:46 2023 ; 4 h 15 min 14 s 451.93 ms remaining ; 1 d 6 h 23 min 8 s 942.02 ms total) Mon Nov 13 11:45:53 2023: Iterated ≈88% of D-proof candidates. [1774743364 of 2016753823] (ETC: Mon Nov 13 15:23:17 2023 ; 3 h 37 min 23 s 984.02 ms remaining ; 1 d 6 h 11 min 39 s 866.75 ms total) Mon Nov 13 12:12:00 2023: Iterated ≈90% of D-proof candidates. [1815078440 of 2016753823] (ETC: Mon Nov 13 15:12:03 2023 ; 3 h 2 s 622.94 ms remaining ; 1 d 6 h 26 s 228.99 ms total) Mon Nov 13 12:37:55 2023: Iterated ≈92% of D-proof candidates. [1855413517 of 2016753823] (ETC: Mon Nov 13 15:01:05 2023 ; 2 h 23 min 9 s 438.05 ms remaining ; 1 d 5 h 49 min 27 s 975.55 ms total) Mon Nov 13 13:03:36 2023: Iterated ≈94% of D-proof candidates. [1895748593 of 2016753823] (ETC: Mon Nov 13 14:50:20 2023 ; 1 h 46 min 43 s 376.10 ms remaining ; 1 d 5 h 38 min 42 s 934.42 ms total) Mon Nov 13 13:29:14 2023: Iterated ≈96% of D-proof candidates. [1936083670 of 2016753823] (ETC: Mon Nov 13 14:39:58 2023 ; 1 h 10 min 44 s 52.24 ms remaining ; 1 d 5 h 28 min 21 s 305.89 ms total) Mon Nov 13 13:55:11 2023: Iterated ≈98% of D-proof candidates. [1976418746 of 2016753823] (ETC: Mon Nov 13 14:30:21 2023 ; 35 min 10 s 484.37 ms remaining ; 1 d 5 h 18 min 44 s 217.13 ms total) Mon Nov 13 14:21:28 2023: Iterated 100% of D-proof candidates. [2016753823 of 2016753823] (ETC: Mon Nov 13 14:21:28 2023 ; 0.00 ms remaining ; 1 d 5 h 9 min 50 s 914.31 ms total) 104992707.42 ms (1 d 5 h 9 min 52 s 707.42 ms) taken to collect 205771643 D-proofs of length 167. [iterated 2016753823 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 3 }, { 9, 4 }, { 11, 7 }, { 13, 10 }, { 15, 13 }, { 17, 16 }, { 19, 26 }, { 21, 36 }, { 23, 42 }, { 25, 54 }, { 27, 80 }, { 29, 100 }, { 31, 126 }, { 33, 162 }, { 35, 221 }, { 37, 282 }, { 39, 359 }, { 41, 454 }, { 43, 615 }, { 45, 778 }, { 47, 1002 }, { 49, 1298 }, { 51, 1678 }, { 53, 2134 }, { 55, 2803 }, { 57, 3534 }, { 59, 4530 }, { 61, 5848 }, { 63, 7496 }, { 65, 9424 }, { 67, 12147 }, { 69, 15402 }, { 71, 19615 }, { 73, 24892 }, { 75, 31620 }, { 77, 39936 }, { 79, 50946 }, { 81, 64168 }, { 83, 81204 }, { 85, 102794 }, { 87, 130094 }, { 89, 163718 }, { 91, 207474 }, { 93, 261220 }, { 95, 329568 }, { 97, 415628 }, { 99, 524144 }, { 101, 658432 }, { 103, 831003 }, { 105, 1044792 }, { 107, 1313760 }, { 109, 1651616 }, { 111, 2077927 }, { 113, 2606646 }, { 115, 3277103 }, { 117, 4112052 }, { 119, 5160229 }, { 121, 6472942 }, { 123, 8122690 }, { 125, 10173684 }, { 127, 12760188 }, { 129, 15985436 }, { 131, 20022824 }, { 133, 25070468 }, { 135, 31402887 }, { 137, 39284338 }, { 139, 49176381 }, { 141, 61517174 }, { 143, 76945234 }, { 145, 96208206 }, { 147, 120320734 }, { 149, 150346484 }, { 151, 187924390 }, { 153, 234799156 }, { 155, 324945288 }, { 157, 440272080 }, { 159, 592215521 }, { 161, 784979956 }, { 163, 1089248702 }, { 165, 1480315260 }, { 167, 2016753823 } } 2393998.94 ms (39 min 53 s 998.94 ms) taken to filter and order new representative proofs. Found 205771643 representative, 363784673 redundant, and 1447197507 invalid condensed detachment proof strings. lengths up to 167 ; amounts per length: {(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), (153,21395853), (155,28040847), (157,38836822), (159,50013506), (161,78239557), (163,101757325), (165,147063822), (167,205771643)} ; 205771643 new representative proofs (363784673 redundant, 1447197507 invalid) Mon Nov 13 15:36:50 2023: Starting to write 205771643 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs167-unfiltered153+.txt. 637534.23 ms (10 min 37 s 534.23 ms) taken to print and save 180054503529 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs167-unfiltered153+.txt. Mon Nov 13 15:53:32 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 167, unfiltered] Mon Nov 13 16:06:54 2023: Process terminated. [pid: 73613, tid:22578865051520]