( 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: 47.8402777… h CPU utilization: 3061.777… core-h ) Mon Nov 13 22:58:20 2023: Process started. [pid: 212376, tid:22396875122560] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(169, 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(169, false, true). Mon Nov 13 22:58:20 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 169, unfiltered] 0.01 ms taken to load initial representatives. 4.17 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22396781254400] 4.42 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22396787558144] 4.89 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22396708841216] 1.01 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22396710942464] 1.34 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22396800165632] 2.12 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22396798064384] 2.94 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22396814874368] 0.43 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22396806469376] 2.64 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22396802266880] 0.18 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22396698334976] 0.60 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22396810671872] 14115.10 ms (14 s 115.11 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22396814874368] 2.23 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22396812773120] 16739.08 ms (16 s 739.08 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:22396810671872] 10553.41 ms (10 s 553.41 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22396710942464] 3.90 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22396808570624] 15781.03 ms (15 s 781.03 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22396806469376] 0.63 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22396804368128] 15725.61 ms (15 s 725.61 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22396802266880] 13604.39 ms (13 s 604.39 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22396800165632] 13266.15 ms (13 s 266.15 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22396798064384] 1.35 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22396795963136] 0.59 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22396793861888] 6.82 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22396791760640] 1.32 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22396789659392] 7891.89 ms (7 s 891.89 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22396787558144] 8.39 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22396785456896] 6.28 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22396783355648] 7383.96 ms (7 s 383.96 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22396781254400] 8948.57 ms (8 s 948.57 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22396708841216] 11.88 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22396706739968] 6.02 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22396704638720] 7.73 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22396702537472] 6.32 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22396700436224] 16179.42 ms (16 s 179.42 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:22396698334976] 11.66 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22396696233728] 34.43 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22396694132480] 18.73 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22396692031232] 9.86 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22396689929984] 13.14 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22396687828736] 15.95 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22396685727488] 10.62 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22396683626240] 5.98 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22396681524992] 13.76 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22396679423744] 17.56 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22396677322496] 424.01 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22396675221248] 39.67 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22396673120000] 27.19 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22396671018752] 38.61 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22396668917504] 17.15 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22396666816256] 43.96 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22396664715008] 45.20 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22396662613760] 40.55 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22396660512512] 90.75 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22396658411264] 593.54 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22396656310016] 136.64 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22396654208768] 210.13 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22396652107520] 654.54 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22396650006272] 67.00 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22396647905024] 408.80 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22394429241088] 1098.75 ms (1 s 98.75 ms) taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22394427139840] 1172.43 ms (1 s 172.43 ms) taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22394425038592] 1373.28 ms (1 s 373.28 ms) taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22394422937344] 1019.52 ms (1 s 19.52 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22394420836096] 1701.29 ms (1 s 701.29 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22394418734848] 1841.53 ms (1 s 841.53 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22394416633600] 1846.99 ms (1 s 846.99 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22394414532352] 2170.82 ms (2 s 170.82 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22394412431104] 3577.35 ms (3 s 577.35 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22394410329856] 4765.38 ms (4 s 765.38 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22394408228608] 2903.26 ms (2 s 903.26 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22394406127360] 3633.45 ms (3 s 633.45 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22394404026112] 5186.95 ms (5 s 186.95 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22394401924864] 4941.32 ms (4 s 941.32 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22394399823616] 5939.50 ms (5 s 939.50 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22394397722368] 16910.97 ms (16 s 910.97 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. 175693.89 ms (2 min 55 s 693.89 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:22394397722368] 239025.09 ms (3 min 59 s 25.09 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:22394399823616] 304756.43 ms (5 min 4 s 756.43 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:22394401924864] 351355.03 ms (5 min 51 s 355.03 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:22394404026112] 434406.77 ms (7 min 14 s 406.78 ms) taken to read 78239557 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. [tid:22394406127360] 483688.95 ms (8 min 3 s 688.95 ms) taken to read 101757325 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt. [tid:22394408228608] 578113.20 ms (9 min 38 s 113.20 ms) taken to read 147063822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs165-unfiltered153+.txt. [tid:22394410329856] 645558.78 ms (10 min 45 s 558.78 ms) taken to read 205771643 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs167-unfiltered153+.txt. [tid:22394412431104] 645616.44 ms (10 min 45 s 616.44 ms) additional read duration. Loaded 8 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 161 : 78239557 163 : 101757325 165 : 147063822 167 : 205771643 695167585 representatives in total. Mon Nov 13 23:10:34 2023: Inserted ≈ 5% of D-proof conclusions. [ 34758379 of 695167585] (ETC: Mon Nov 13 23:33:17 2023 ; 22 min 42 s 493.09 ms remaining ; 23 min 54 s 203.25 ms total) Mon Nov 13 23:12:06 2023: Inserted ≈10% of D-proof conclusions. [ 69516758 of 695167585] (ETC: Mon Nov 13 23:36:40 2023 ; 24 min 33 s 825.44 ms remaining ; 27 min 17 s 583.82 ms total) Mon Nov 13 23:13:42 2023: Inserted ≈15% of D-proof conclusions. [104275137 of 695167585] (ETC: Mon Nov 13 23:38:12 2023 ; 24 min 29 s 791.11 ms remaining ; 28 min 49 s 166.01 ms total) Mon Nov 13 23:15:19 2023: Inserted ≈20% of D-proof conclusions. [139033517 of 695167585] (ETC: Mon Nov 13 23:39:07 2023 ; 23 min 47 s 316.73 ms remaining ; 29 min 44 s 145.91 ms total) Mon Nov 13 23:17:03 2023: Inserted ≈25% of D-proof conclusions. [173791896 of 695167585] (ETC: Mon Nov 13 23:40:06 2023 ; 23 min 2 s 639.10 ms remaining ; 30 min 43 s 518.79 ms total) Mon Nov 13 23:18:43 2023: Inserted ≈30% of D-proof conclusions. [208550275 of 695167585] (ETC: Mon Nov 13 23:40:31 2023 ; 21 min 47 s 985.93 ms remaining ; 31 min 8 s 551.32 ms total) Mon Nov 13 23:20:34 2023: Inserted ≈35% of D-proof conclusions. [243308654 of 695167585] (ETC: Mon Nov 13 23:41:21 2023 ; 20 min 46 s 826.27 ms remaining ; 31 min 58 s 194.27 ms total) Mon Nov 13 23:22:14 2023: Inserted ≈40% of D-proof conclusions. [278067034 of 695167585] (ETC: Mon Nov 13 23:41:30 2023 ; 19 min 16 s 618.00 ms remaining ; 32 min 7 s 696.66 ms total) Mon Nov 13 23:23:54 2023: Inserted ≈45% of D-proof conclusions. [312825413 of 695167585] (ETC: Mon Nov 13 23:41:39 2023 ; 17 min 44 s 924.15 ms remaining ; 32 min 16 s 225.73 ms total) Mon Nov 13 23:25:33 2023: Inserted ≈50% of D-proof conclusions. [347583792 of 695167585] (ETC: Mon Nov 13 23:41:44 2023 ; 16 min 10 s 865.79 ms remaining ; 32 min 21 s 731.59 ms total) Mon Nov 13 23:27:05 2023: Inserted ≈55% of D-proof conclusions. [382342171 of 695167585] (ETC: Mon Nov 13 23:41:33 2023 ; 14 min 28 s 927.33 ms remaining ; 32 min 10 s 949.61 ms total) Mon Nov 13 23:28:51 2023: Inserted ≈60% of D-proof conclusions. [417100551 of 695167585] (ETC: Mon Nov 13 23:41:50 2023 ; 12 min 58 s 788.55 ms remaining ; 32 min 26 s 971.38 ms total) Mon Nov 13 23:30:56 2023: Inserted ≈65% of D-proof conclusions. [451858930 of 695167585] (ETC: Mon Nov 13 23:42:33 2023 ; 11 min 36 s 499.71 ms remaining ; 33 min 9 s 999.18 ms total) Mon Nov 13 23:32:54 2023: Inserted ≈70% of D-proof conclusions. [486617309 of 695167585] (ETC: Mon Nov 13 23:42:59 2023 ; 10 min 4 s 796.41 ms remaining ; 33 min 35 s 988.03 ms total) Mon Nov 13 23:34:21 2023: Inserted ≈75% of D-proof conclusions. [521375688 of 695167585] (ETC: Mon Nov 13 23:42:40 2023 ; 8 min 19 s 387.27 ms remaining ; 33 min 17 s 549.08 ms total) Mon Nov 13 23:35:54 2023: Inserted ≈80% of D-proof conclusions. [556134068 of 695167585] (ETC: Mon Nov 13 23:42:32 2023 ; 6 min 37 s 959.00 ms remaining ; 33 min 9 s 795.01 ms total) Mon Nov 13 23:37:28 2023: Inserted ≈85% of D-proof conclusions. [590892447 of 695167585] (ETC: Mon Nov 13 23:42:26 2023 ; 4 min 57 s 466.66 ms remaining ; 33 min 3 s 111.04 ms total) Mon Nov 13 23:39:16 2023: Inserted ≈90% of D-proof conclusions. [625650826 of 695167585] (ETC: Mon Nov 13 23:42:35 2023 ; 3 min 19 s 245.13 ms remaining ; 33 min 12 s 451.25 ms total) Mon Nov 13 23:41:19 2023: Inserted ≈95% of D-proof conclusions. [660409205 of 695167585] (ETC: Mon Nov 13 23:43:00 2023 ; 1 min 40 s 861.28 ms remaining ; 33 min 37 s 225.56 ms total) Mon Nov 13 23:43:12 2023: Inserted 100% of D-proof conclusions. [695167585 of 695167585] (ETC: Mon Nov 13 23:43:12 2023 ; 0.00 ms remaining ; 33 min 49 s 774.74 ms total) 2029776.34 ms (33 min 49 s 776.34 ms) total insertion duration. Known iteration count loaded from 169:2734328708. Mon Nov 13 23:43:12 2023: Starting to generate D-proof representatives of length 169. Tue Nov 14 00:28:41 2023: Iterated ≈ 2% of D-proof candidates. [ 54686574 of 2734328708] (ETC: Wed Nov 15 13:37:13 2023 ; 1 d 13 h 8 min 31 s 438.10 ms remaining ; 1 d 13 h 54 min 242.95 ms total) Tue Nov 14 01:10:16 2023: Iterated ≈ 4% of D-proof candidates. [ 109373148 of 2734328708] (ETC: Wed Nov 15 11:59:47 2023 ; 1 d 10 h 49 min 31 s 229.49 ms remaining ; 1 d 12 h 16 min 35 s 30.71 ms total) Tue Nov 14 01:53:48 2023: Iterated ≈ 6% of D-proof candidates. [ 164059722 of 2734328708] (ETC: Wed Nov 15 11:59:38 2023 ; 1 d 10 h 5 min 50 s 872.12 ms remaining ; 1 d 12 h 16 min 26 s 34.15 ms total) Tue Nov 14 02:34:55 2023: Iterated ≈ 8% of D-proof candidates. [ 218746296 of 2734328708] (ETC: Wed Nov 15 11:29:36 2023 ; 1 d 8 h 54 min 40 s 977.74 ms remaining ; 1 d 11 h 46 min 23 s 671.43 ms total) Tue Nov 14 03:26:58 2023: Iterated ≈10% of D-proof candidates. [ 273432870 of 2734328708] (ETC: Wed Nov 15 13:00:52 2023 ; 1 d 9 h 33 min 53 s 800.76 ms remaining ; 1 d 13 h 17 min 39 s 778.58 ms total) Tue Nov 14 04:19:27 2023: Iterated ≈12% of D-proof candidates. [ 328119444 of 2734328708] (ETC: Wed Nov 15 14:05:16 2023 ; 1 d 9 h 45 min 48 s 400.12 ms remaining ; 1 d 14 h 22 min 3 s 181.90 ms total) Tue Nov 14 05:13:54 2023: Iterated ≈14% of D-proof candidates. [ 382806019 of 2734328708] (ETC: Wed Nov 15 15:05:22 2023 ; 1 d 9 h 51 min 27 s 119.46 ms remaining ; 1 d 15 h 22 min 9 s 208.67 ms total) Tue Nov 14 06:14:25 2023: Iterated ≈16% of D-proof candidates. [ 437492593 of 2734328708] (ETC: Wed Nov 15 16:28:16 2023 ; 1 d 10 h 13 min 50 s 944.72 ms remaining ; 1 d 16 h 45 min 3 s 505.60 ms total) Tue Nov 14 07:11:28 2023: Iterated ≈18% of D-proof candidates. [ 492179167 of 2734328708] (ETC: Wed Nov 15 17:13:31 2023 ; 1 d 10 h 2 min 2 s 973.11 ms remaining ; 1 d 17 h 30 min 18 s 259.86 ms total) Tue Nov 14 08:26:22 2023: Iterated ≈20% of D-proof candidates. [ 546865741 of 2734328708] (ETC: Wed Nov 15 19:19:01 2023 ; 1 d 10 h 52 min 38 s 843.85 ms remaining ; 1 d 19 h 35 min 48 s 554.77 ms total) Tue Nov 14 09:41:16 2023: Iterated ≈22% of D-proof candidates. [ 601552315 of 2734328708] (ETC: Wed Nov 15 21:01:41 2023 ; 1 d 11 h 20 min 24 s 753.40 ms remaining ; 1 d 21 h 18 min 28 s 658.15 ms total) Tue Nov 14 10:47:36 2023: Iterated ≈24% of D-proof candidates. [ 656238889 of 2734328708] (ETC: Wed Nov 15 21:51:32 2023 ; 1 d 11 h 3 min 55 s 370.09 ms remaining ; 1 d 22 h 8 min 19 s 171.09 ms total) Tue Nov 14 11:49:02 2023: Iterated ≈26% of D-proof candidates. [ 710925464 of 2734328708] (ETC: Wed Nov 15 22:14:51 2023 ; 1 d 10 h 25 min 48 s 883.59 ms remaining ; 1 d 22 h 31 min 38 s 491.33 ms total) Tue Nov 14 13:10:17 2023: Iterated ≈28% of D-proof candidates. [ 765612038 of 2734328708] (ETC: Wed Nov 15 23:45:36 2023 ; 1 d 10 h 35 min 19 s 167.89 ms remaining ; 2 d 2 min 23 s 288.72 ms total) Tue Nov 14 14:24:08 2023: Iterated ≈30% of D-proof candidates. [ 820298612 of 2734328708] (ETC: Thu Nov 16 00:39:36 2023 ; 1 d 10 h 15 min 28 s 883.64 ms remaining ; 2 d 56 min 24 s 119.45 ms total) Tue Nov 14 15:30:09 2023: Iterated ≈32% of D-proof candidates. [ 874985186 of 2734328708] (ETC: Thu Nov 16 01:02:24 2023 ; 1 d 9 h 32 min 14 s 943.31 ms remaining ; 2 d 1 h 19 min 11 s 387.17 ms total) Tue Nov 14 16:34:25 2023: Iterated ≈34% of D-proof candidates. [ 929671760 of 2734328708] (ETC: Thu Nov 16 01:17:22 2023 ; 1 d 8 h 42 min 56 s 745.74 ms remaining ; 2 d 1 h 34 min 9 s 614.68 ms total) Tue Nov 14 17:48:34 2023: Iterated ≈36% of D-proof candidates. [ 984358334 of 2734328708] (ETC: Thu Nov 16 01:58:06 2023 ; 1 d 8 h 9 min 32 s 169.67 ms remaining ; 2 d 2 h 14 min 54 s 15.02 ms total) Tue Nov 14 18:55:48 2023: Iterated ≈38% of D-proof candidates. [1039044909 of 2734328708] (ETC: Thu Nov 16 02:16:22 2023 ; 1 d 7 h 20 min 33 s 533.74 ms remaining ; 2 d 2 h 33 min 9 s 570.54 ms total) Tue Nov 14 19:56:25 2023: Iterated ≈40% of D-proof candidates. [1093731483 of 2734328708] (ETC: Thu Nov 16 02:16:13 2023 ; 1 d 6 h 19 min 48 s 196.49 ms remaining ; 2 d 2 h 33 min 327.46 ms total) Tue Nov 14 20:58:23 2023: Iterated ≈42% of D-proof candidates. [1148418057 of 2734328708] (ETC: Thu Nov 16 02:19:21 2023 ; 1 d 5 h 20 min 57 s 878.98 ms remaining ; 2 d 2 h 36 min 8 s 756.82 ms total) Tue Nov 14 22:01:55 2023: Iterated ≈44% of D-proof candidates. [1203104631 of 2734328708] (ETC: Thu Nov 16 02:25:44 2023 ; 1 d 4 h 23 min 48 s 856.57 ms remaining ; 2 d 2 h 42 min 31 s 529.52 ms total) Tue Nov 14 22:58:31 2023: Iterated ≈46% of D-proof candidates. [1257791205 of 2734328708] (ETC: Thu Nov 16 02:16:29 2023 ; 1 d 3 h 17 min 58 s 229.65 ms remaining ; 2 d 2 h 33 min 16 s 721.50 ms total) Wed Nov 15 00:05:49 2023: Iterated ≈48% of D-proof candidates. [1312477779 of 2734328708] (ETC: Thu Nov 16 02:30:18 2023 ; 1 d 2 h 24 min 29 s 574.11 ms remaining ; 2 d 2 h 47 min 6 s 103.95 ms total) Wed Nov 15 01:13:40 2023: Iterated ≈50% of D-proof candidates. [1367164354 of 2734328708] (ETC: Thu Nov 16 02:44:08 2023 ; 1 d 1 h 30 min 27 s 802.91 ms remaining ; 2 d 3 h 55 s 605.82 ms total) Wed Nov 15 02:08:50 2023: Iterated ≈52% of D-proof candidates. [1421850928 of 2734328708] (ETC: Thu Nov 16 02:32:30 2023 ; 1 d 23 min 39 s 606.87 ms remaining ; 2 d 2 h 49 min 17 s 514.28 ms total) Wed Nov 15 03:09:26 2023: Iterated ≈54% of D-proof candidates. [1476537502 of 2734328708] (ETC: Thu Nov 16 02:31:46 2023 ; 23 h 22 min 20 s 70.28 ms remaining ; 2 d 2 h 48 min 33 s 196.21 ms total) Wed Nov 15 04:05:19 2023: Iterated ≈56% of D-proof candidates. [1531224076 of 2734328708] (ETC: Thu Nov 16 02:22:41 2023 ; 22 h 17 min 22 s 412.57 ms remaining ; 2 d 2 h 39 min 29 s 119.41 ms total) Wed Nov 15 04:58:55 2023: Iterated ≈58% of D-proof candidates. [1585910650 of 2734328708] (ETC: Thu Nov 16 02:10:17 2023 ; 21 h 11 min 22 s 508.65 ms remaining ; 2 d 2 h 27 min 5 s 20.50 ms total) Wed Nov 15 05:54:40 2023: Iterated ≈60% of D-proof candidates. [1640597224 of 2734328708] (ETC: Thu Nov 16 02:02:18 2023 ; 20 h 7 min 38 s 277.33 ms remaining ; 2 d 2 h 19 min 5 s 693.21 ms total) Wed Nov 15 06:51:35 2023: Iterated ≈62% of D-proof candidates. [1695283798 of 2734328708] (ETC: Thu Nov 16 01:56:43 2023 ; 19 h 5 min 8 s 143.81 ms remaining ; 2 d 2 h 13 min 30 s 904.59 ms total) Wed Nov 15 07:46:02 2023: Iterated ≈64% of D-proof candidates. [1749970373 of 2734328708] (ETC: Thu Nov 16 01:47:38 2023 ; 18 h 1 min 35 s 525.36 ms remaining ; 2 d 2 h 4 min 25 s 348.20 ms total) Wed Nov 15 08:37:49 2023: Iterated ≈66% of D-proof candidates. [1804656947 of 2734328708] (ETC: Thu Nov 16 01:35:03 2023 ; 16 h 57 min 13 s 537.53 ms remaining ; 2 d 1 h 51 min 50 s 404.46 ms total) Wed Nov 15 09:27:08 2023: Iterated ≈68% of D-proof candidates. [1859343521 of 2734328708] (ETC: Thu Nov 16 01:19:35 2023 ; 15 h 52 min 26 s 311.53 ms remaining ; 2 d 1 h 36 min 22 s 223.44 ms total) Wed Nov 15 10:14:31 2023: Iterated ≈70% of D-proof candidates. [1914030095 of 2734328708] (ETC: Thu Nov 16 01:02:14 2023 ; 14 h 47 min 42 s 408.39 ms remaining ; 2 d 1 h 19 min 1 s 361.18 ms total) Wed Nov 15 11:00:08 2023: Iterated ≈72% of D-proof candidates. [1968716669 of 2734328708] (ETC: Thu Nov 16 00:43:23 2023 ; 13 h 43 min 15 s 94.45 ms remaining ; 2 d 1 h 11 s 51.45 ms total) Wed Nov 15 11:44:15 2023: Iterated ≈74% of D-proof candidates. [2023403243 of 2734328708] (ETC: Thu Nov 16 00:23:32 2023 ; 12 h 39 min 17 s 95.32 ms remaining ; 2 d 40 min 19 s 597.15 ms total) Wed Nov 15 12:27:17 2023: Iterated ≈76% of D-proof candidates. [2078089818 of 2734328708] (ETC: Thu Nov 16 00:03:19 2023 ; 11 h 36 min 1 s 536.00 ms remaining ; 2 d 20 min 6 s 399.99 ms total) Wed Nov 15 13:09:16 2023: Iterated ≈78% of D-proof candidates. [2132776392 of 2734328708] (ETC: Wed Nov 15 23:42:46 2023 ; 10 h 33 min 30 s 280.51 ms remaining ; 1 d 23 h 59 min 34 s 2.24 ms total) Wed Nov 15 13:50:20 2023: Iterated ≈80% of D-proof candidates. [2187462966 of 2734328708] (ETC: Wed Nov 15 23:22:06 2023 ; 9 h 31 min 46 s 791.76 ms remaining ; 1 d 23 h 38 min 53 s 958.70 ms total) Wed Nov 15 14:30:34 2023: Iterated ≈82% of D-proof candidates. [2242149540 of 2734328708] (ETC: Wed Nov 15 23:01:27 2023 ; 8 h 30 min 53 s 11.78 ms remaining ; 1 d 23 h 18 min 14 s 509.67 ms total) Wed Nov 15 15:10:05 2023: Iterated ≈84% of D-proof candidates. [2296836114 of 2734328708] (ETC: Wed Nov 15 22:40:54 2023 ; 7 h 30 min 49 s 934.87 ms remaining ; 1 d 22 h 57 min 42 s 92.64 ms total) Wed Nov 15 15:49:03 2023: Iterated ≈86% of D-proof candidates. [2351522688 of 2734328708] (ETC: Wed Nov 15 22:20:42 2023 ; 6 h 31 min 38 s 891.94 ms remaining ; 1 d 22 h 37 min 29 s 227.78 ms total) Wed Nov 15 16:27:29 2023: Iterated ≈88% of D-proof candidates. [2406209263 of 2734328708] (ETC: Wed Nov 15 22:00:47 2023 ; 5 h 33 min 18 s 581.84 ms remaining ; 1 d 22 h 17 min 34 s 848.68 ms total) Wed Nov 15 17:05:27 2023: Iterated ≈90% of D-proof candidates. [2460895837 of 2734328708] (ETC: Wed Nov 15 21:41:15 2023 ; 4 h 35 min 48 s 276.52 ms remaining ; 1 d 21 h 58 min 2 s 765.13 ms total) Wed Nov 15 17:43:01 2023: Iterated ≈92% of D-proof candidates. [2515582411 of 2734328708] (ETC: Wed Nov 15 21:22:08 2023 ; 3 h 39 min 6 s 874.67 ms remaining ; 1 d 21 h 38 min 55 s 933.15 ms total) Wed Nov 15 18:20:22 2023: Iterated ≈94% of D-proof candidates. [2570268985 of 2734328708] (ETC: Wed Nov 15 21:03:35 2023 ; 2 h 43 min 13 s 352.89 ms remaining ; 1 d 21 h 20 min 22 s 547.74 ms total) Wed Nov 15 18:57:20 2023: Iterated ≈96% of D-proof candidates. [2624955559 of 2734328708] (ETC: Wed Nov 15 20:45:26 2023 ; 1 h 48 min 5 s 334.02 ms remaining ; 1 d 21 h 2 min 13 s 349.57 ms total) Wed Nov 15 19:34:22 2023: Iterated ≈98% of D-proof candidates. [2679642133 of 2734328708] (ETC: Wed Nov 15 20:28:03 2023 ; 53 min 41 s 819.90 ms remaining ; 1 d 20 h 44 min 50 s 992.67 ms total) Wed Nov 15 20:11:46 2023: Iterated 100% of D-proof candidates. [2734328708 of 2734328708] (ETC: Wed Nov 15 20:11:46 2023 ; 0.00 ms remaining ; 1 d 20 h 28 min 33 s 881.12 ms total) 160117172.58 ms (1 d 20 h 28 min 37 s 172.58 ms) taken to collect 299846803 D-proofs of length 169. [iterated 2734328708 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 }, { 169, 2734328708 } } 3663917.27 ms (1 h 1 min 3 s 917.27 ms) taken to filter and order new representative proofs. Found 299846803 representative, 494006383 redundant, and 1940475522 invalid condensed detachment proof strings. lengths up to 169 ; 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), (169,299846803)} ; 299846803 new representative proofs (494006383 redundant, 1940475522 invalid) Wed Nov 15 21:59:46 2023: Starting to write 299846803 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs169-unfiltered153+.txt. 1041459.10 ms (17 min 21 s 459.10 ms) taken to print and save 273688640204 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs169-unfiltered153+.txt. Wed Nov 15 22:26:15 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 169, unfiltered] Wed Nov 15 22:48:45 2023: Process terminated. [pid: 212376, tid:22396875122560]