( 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: 14.43444… h CPU utilization: 923.80444… core-h ) Thu Nov 9 19:47:45 2023: Process started. [pid: 254588, tid:23141686105984] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(163, 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(163, false, true). Thu Nov 9 19:47:45 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 163, unfiltered] 0.03 ms taken to load initial representatives. 0.04 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23141621655296] 1.44 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23141590136576] 1.30 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23141623756544] 2.38 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23141613250304] 0.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23141571225344] 1.26 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23141609047808] 0.01 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23141611149056] 0.46 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23141602744064] 0.86 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23141598541568] 0.47 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23141588035328] 0.73 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23141579630336] 10.63 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23141625857792] 7614.46 ms (7 s 614.46 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23141623756544] 6336.09 ms (6 s 336.09 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23141621655296] 2.75 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23141619554048] 6.68 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23141617452800] 0.04 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23141615351552] 11058.82 ms (11 s 58.82 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23141613250304] 14915.59 ms (14 s 915.59 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23141611149056] 13787.43 ms (13 s 787.43 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23141609047808] 5.52 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23141606946560] 6.18 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23141604845312] 15718.03 ms (15 s 718.03 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23141602744064] 0.14 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23141600642816] 15950.87 ms (15 s 950.87 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23141598541568] 0.72 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23141596440320] 3.08 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23141594339072] 7.77 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23141592237824] 8540.79 ms (8 s 540.79 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23141590136576] 16673.54 ms (16 s 673.54 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23141588035328] 1.80 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23141585934080] 9.91 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23141583832832] 0.74 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23141581731584] 17517.22 ms (17 s 517.22 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23141579630336] 0.22 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23141577529088] 13.63 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23141575427840] 6.14 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23141573326592] 12891.36 ms (12 s 891.36 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23141571225344] 13.09 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23141569124096] 6.38 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23141567022848] 10.15 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23141564921600] 19.07 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23141562820352] 3.06 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23141560719104] 11.17 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23141558617856] 37.13 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23141556516608] 44.01 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23141554415360] 13.94 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23139337631488] 360.88 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23139335530240] 471.89 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23139333428992] 54.96 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23139331327744] 11.68 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23139329226496] 53.60 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23139327125248] 57.65 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23139325024000] 47.91 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23139322922752] 304.18 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23139320821504] 315.30 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23139318720256] 61.20 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23139316619008] 498.24 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23139314517760] 822.13 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23139312416512] 494.66 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23139310315264] 922.14 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23139308214016] 1247.09 ms (1 s 247.09 ms) taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23139306112768] 224.87 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23139304011520] 1379.85 ms (1 s 379.85 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23139301910272] 1549.51 ms (1 s 549.51 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23139299809024] 1525.96 ms (1 s 525.96 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23139297707776] 1916.37 ms (1 s 916.37 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23139295606528] 2445.16 ms (2 s 445.17 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23139293505280] 8269.04 ms (8 s 269.04 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23139291404032] 9255.88 ms (9 s 255.88 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23139289302784] 4571.39 ms (4 s 571.39 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23139287201536] 1787.38 ms (1 s 787.38 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23139285100288] 3473.21 ms (3 s 473.21 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23139282999040] 2339.27 ms (2 s 339.27 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23139280897792] 5718.05 ms (5 s 718.06 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23139278796544] 17673.38 ms (17 s 673.38 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. 71212.86 ms (1 min 11 s 212.86 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:23139278796544] 87525.71 ms (1 min 27 s 525.71 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:23139280897792] 109871.89 ms (1 min 49 s 871.89 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:23139282999040] 125644.13 ms (2 min 5 s 644.13 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:23139285100288] 146203.59 ms (2 min 26 s 203.59 ms) taken to read 78239557 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. [tid:23139287201536] 146249.87 ms (2 min 26 s 249.87 ms) additional read duration. Loaded 5 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 161 : 78239557 240574795 representatives in total. Thu Nov 9 19:50:58 2023: Inserted ≈ 5% of D-proof conclusions. [ 12028739 of 240574795] (ETC: Thu Nov 9 20:00:04 2023 ; 9 min 6 s 458.26 ms remaining ; 9 min 35 s 219.22 ms total) Thu Nov 9 19:51:31 2023: Inserted ≈10% of D-proof conclusions. [ 24057479 of 240574795] (ETC: Thu Nov 9 20:00:46 2023 ; 9 min 15 s 604.67 ms remaining ; 10 min 17 s 338.52 ms total) Thu Nov 9 19:51:55 2023: Inserted ≈15% of D-proof conclusions. [ 36086219 of 240574795] (ETC: Thu Nov 9 20:00:02 2023 ; 8 min 6 s 729.10 ms remaining ; 9 min 32 s 622.47 ms total) Thu Nov 9 19:52:20 2023: Inserted ≈20% of D-proof conclusions. [ 48114959 of 240574795] (ETC: Thu Nov 9 19:59:41 2023 ; 7 min 21 s 570.49 ms remaining ; 9 min 11 s 963.12 ms total) Thu Nov 9 19:52:43 2023: Inserted ≈25% of D-proof conclusions. [ 60143698 of 240574795] (ETC: Thu Nov 9 19:59:24 2023 ; 6 min 40 s 964.73 ms remaining ; 8 min 54 s 619.63 ms total) Thu Nov 9 19:53:08 2023: Inserted ≈30% of D-proof conclusions. [ 72172438 of 240574795] (ETC: Thu Nov 9 19:59:19 2023 ; 6 min 11 s 118.12 ms remaining ; 8 min 50 s 168.74 ms total) Thu Nov 9 19:53:30 2023: Inserted ≈35% of D-proof conclusions. [ 84201178 of 240574795] (ETC: Thu Nov 9 19:59:07 2023 ; 5 min 36 s 457.30 ms remaining ; 8 min 37 s 626.62 ms total) Thu Nov 9 19:53:54 2023: Inserted ≈40% of D-proof conclusions. [ 96229918 of 240574795] (ETC: Thu Nov 9 19:59:02 2023 ; 5 min 7 s 873.96 ms remaining ; 8 min 33 s 123.27 ms total) Thu Nov 9 19:54:20 2023: Inserted ≈45% of D-proof conclusions. [108258657 of 240574795] (ETC: Thu Nov 9 19:59:01 2023 ; 4 min 41 s 633.40 ms remaining ; 8 min 32 s 60.72 ms total) Thu Nov 9 19:54:49 2023: Inserted ≈50% of D-proof conclusions. [120287397 of 240574795] (ETC: Thu Nov 9 19:59:10 2023 ; 4 min 20 s 327.45 ms remaining ; 8 min 40 s 654.90 ms total) Thu Nov 9 19:55:18 2023: Inserted ≈55% of D-proof conclusions. [132316137 of 240574795] (ETC: Thu Nov 9 19:59:14 2023 ; 3 min 56 s 287.79 ms remaining ; 8 min 45 s 83.97 ms total) Thu Nov 9 19:55:46 2023: Inserted ≈60% of D-proof conclusions. [144344877 of 240574795] (ETC: Thu Nov 9 19:59:18 2023 ; 3 min 31 s 537.04 ms remaining ; 8 min 48 s 842.60 ms total) Thu Nov 9 19:56:20 2023: Inserted ≈65% of D-proof conclusions. [156373616 of 240574795] (ETC: Thu Nov 9 19:59:29 2023 ; 3 min 9 s 77.41 ms remaining ; 9 min 221.17 ms total) Thu Nov 9 19:56:53 2023: Inserted ≈70% of D-proof conclusions. [168402356 of 240574795] (ETC: Thu Nov 9 19:59:38 2023 ; 2 min 44 s 603.32 ms remaining ; 9 min 8 s 677.72 ms total) Thu Nov 9 19:57:25 2023: Inserted ≈75% of D-proof conclusions. [180431096 of 240574795] (ETC: Thu Nov 9 19:59:44 2023 ; 2 min 18 s 602.35 ms remaining ; 9 min 14 s 409.41 ms total) Thu Nov 9 19:57:57 2023: Inserted ≈80% of D-proof conclusions. [192459836 of 240574795] (ETC: Thu Nov 9 19:59:49 2023 ; 1 min 52 s 52.92 ms remaining ; 9 min 20 s 264.60 ms total) Thu Nov 9 19:58:28 2023: Inserted ≈85% of D-proof conclusions. [204488575 of 240574795] (ETC: Thu Nov 9 19:59:52 2023 ; 1 min 24 s 507.21 ms remaining ; 9 min 23 s 381.37 ms total) Thu Nov 9 19:58:57 2023: Inserted ≈90% of D-proof conclusions. [216517315 of 240574795] (ETC: Thu Nov 9 19:59:54 2023 ; 56 s 453.95 ms remaining ; 9 min 24 s 539.54 ms total) Thu Nov 9 19:59:27 2023: Inserted ≈95% of D-proof conclusions. [228546055 of 240574795] (ETC: Thu Nov 9 19:59:55 2023 ; 28 s 290.58 ms remaining ; 9 min 25 s 811.52 ms total) Thu Nov 9 19:59:53 2023: Inserted 100% of D-proof conclusions. [240574795 of 240574795] (ETC: Thu Nov 9 19:59:53 2023 ; 0.00 ms remaining ; 9 min 24 s 193.43 ms total) 564194.88 ms (9 min 24 s 194.88 ms) total insertion duration. Known iteration count loaded from 163:1089248702. Thu Nov 9 19:59:53 2023: Starting to generate D-proof representatives of length 163. Thu Nov 9 20:16:08 2023: Iterated ≈ 2% of D-proof candidates. [ 21784974 of 1089248702] (ETC: Fri Nov 10 09:31:49 2023 ; 13 h 15 min 41 s 494.72 ms remaining ; 13 h 31 min 55 s 810.94 ms total) Thu Nov 9 20:30:43 2023: Iterated ≈ 4% of D-proof candidates. [ 43569948 of 1089248702] (ETC: Fri Nov 10 08:50:40 2023 ; 12 h 19 min 56 s 339.53 ms remaining ; 12 h 50 min 46 s 187.01 ms total) Thu Nov 9 20:44:57 2023: Iterated ≈ 6% of D-proof candidates. [ 65354922 of 1089248702] (ETC: Fri Nov 10 08:30:55 2023 ; 11 h 45 min 57 s 553.57 ms remaining ; 12 h 31 min 1 s 227.20 ms total) Thu Nov 9 20:59:50 2023: Iterated ≈ 8% of D-proof candidates. [ 87139896 of 1089248702] (ETC: Fri Nov 10 08:29:05 2023 ; 11 h 29 min 15 s 698.22 ms remaining ; 12 h 29 min 11 s 845.88 ms total) Thu Nov 9 21:16:18 2023: Iterated ≈10% of D-proof candidates. [ 108924870 of 1089248702] (ETC: Fri Nov 10 08:44:03 2023 ; 11 h 27 min 44 s 778.15 ms remaining ; 12 h 44 min 9 s 753.49 ms total) Thu Nov 9 21:31:40 2023: Iterated ≈12% of D-proof candidates. [ 130709844 of 1089248702] (ETC: Fri Nov 10 08:44:46 2023 ; 11 h 13 min 5 s 379.51 ms remaining ; 12 h 44 min 52 s 476.71 ms total) Thu Nov 9 21:46:23 2023: Iterated ≈14% of D-proof candidates. [ 152494818 of 1089248702] (ETC: Fri Nov 10 08:40:31 2023 ; 10 h 54 min 8 s 403.99 ms remaining ; 12 h 40 min 37 s 679.05 ms total) Thu Nov 9 22:04:57 2023: Iterated ≈16% of D-proof candidates. [ 174279792 of 1089248702] (ETC: Fri Nov 10 09:01:29 2023 ; 10 h 56 min 31 s 987.29 ms remaining ; 13 h 1 min 35 s 222.95 ms total) Thu Nov 9 22:22:09 2023: Iterated ≈18% of D-proof candidates. [ 196064766 of 1089248702] (ETC: Fri Nov 10 09:10:16 2023 ; 10 h 48 min 6 s 487.09 ms remaining ; 13 h 10 min 22 s 545.21 ms total) Thu Nov 9 22:40:55 2023: Iterated ≈20% of D-proof candidates. [ 217849740 of 1089248702] (ETC: Fri Nov 10 09:25:00 2023 ; 10 h 44 min 5 s 447.95 ms remaining ; 13 h 25 min 6 s 809.91 ms total) Thu Nov 9 22:58:16 2023: Iterated ≈22% of D-proof candidates. [ 239634714 of 1089248702] (ETC: Fri Nov 10 09:30:40 2023 ; 10 h 32 min 24 s 487.76 ms remaining ; 13 h 30 min 46 s 779.15 ms total) Thu Nov 9 23:16:13 2023: Iterated ≈24% of D-proof candidates. [ 261419688 of 1089248702] (ETC: Fri Nov 10 09:37:54 2023 ; 10 h 21 min 41 s 683.43 ms remaining ; 13 h 38 min 1 s 162.38 ms total) Thu Nov 9 23:37:53 2023: Iterated ≈26% of D-proof candidates. [ 283204662 of 1089248702] (ETC: Fri Nov 10 09:58:18 2023 ; 10 h 20 min 25 s 438.66 ms remaining ; 13 h 58 min 24 s 646.80 ms total) Fri Nov 10 00:00:02 2023: Iterated ≈28% of D-proof candidates. [ 304989636 of 1089248702] (ETC: Fri Nov 10 10:17:34 2023 ; 10 h 17 min 31 s 852.18 ms remaining ; 14 h 17 min 40 s 905.77 ms total) Fri Nov 10 00:18:00 2023: Iterated ≈30% of D-proof candidates. [ 326774610 of 1089248702] (ETC: Fri Nov 10 10:20:16 2023 ; 10 h 2 min 16 s 110.16 ms remaining ; 14 h 20 min 23 s 14.48 ms total) Fri Nov 10 00:39:19 2023: Iterated ≈32% of D-proof candidates. [ 348559584 of 1089248702] (ETC: Fri Nov 10 10:33:05 2023 ; 9 h 53 min 46 s 33.48 ms remaining ; 14 h 33 min 11 s 225.66 ms total) Fri Nov 10 01:00:59 2023: Iterated ≈34% of D-proof candidates. [ 370344558 of 1089248702] (ETC: Fri Nov 10 10:45:27 2023 ; 9 h 44 min 28 s 8.56 ms remaining ; 14 h 45 min 33 s 346.26 ms total) Fri Nov 10 01:19:30 2023: Iterated ≈36% of D-proof candidates. [ 392129532 of 1089248702] (ETC: Fri Nov 10 10:47:42 2023 ; 9 h 28 min 11 s 903.32 ms remaining ; 14 h 47 min 48 s 598.89 ms total) Fri Nov 10 01:38:32 2023: Iterated ≈38% of D-proof candidates. [ 413914506 of 1089248702] (ETC: Fri Nov 10 10:51:04 2023 ; 9 h 12 min 31 s 848.58 ms remaining ; 14 h 51 min 10 s 723.46 ms total) Fri Nov 10 01:57:41 2023: Iterated ≈40% of D-proof candidates. [ 435699480 of 1089248702] (ETC: Fri Nov 10 10:54:22 2023 ; 8 h 56 min 41 s 162.70 ms remaining ; 14 h 54 min 28 s 604.44 ms total) Fri Nov 10 02:16:50 2023: Iterated ≈42% of D-proof candidates. [ 457484454 of 1089248702] (ETC: Fri Nov 10 10:57:22 2023 ; 8 h 40 min 32 s 492.03 ms remaining ; 14 h 57 min 29 s 124.11 ms total) Fri Nov 10 02:34:45 2023: Iterated ≈44% of D-proof candidates. [ 479269428 of 1089248702] (ETC: Fri Nov 10 10:57:18 2023 ; 8 h 22 min 32 s 780.72 ms remaining ; 14 h 57 min 24 s 251.21 ms total) Fri Nov 10 02:55:36 2023: Iterated ≈46% of D-proof candidates. [ 501054402 of 1089248702] (ETC: Fri Nov 10 11:03:38 2023 ; 8 h 8 min 1 s 69.25 ms remaining ; 15 h 3 min 44 s 202.23 ms total) Fri Nov 10 03:15:02 2023: Iterated ≈48% of D-proof candidates. [ 522839376 of 1089248702] (ETC: Fri Nov 10 11:06:26 2023 ; 7 h 51 min 24 s 293.55 ms remaining ; 15 h 6 min 32 s 872.11 ms total) Fri Nov 10 03:34:24 2023: Iterated ≈50% of D-proof candidates. [ 544624351 of 1089248702] (ETC: Fri Nov 10 11:08:54 2023 ; 7 h 34 min 30 s 585.54 ms remaining ; 15 h 9 min 1 s 171.09 ms total) Fri Nov 10 03:53:03 2023: Iterated ≈52% of D-proof candidates. [ 566409325 of 1089248702] (ETC: Fri Nov 10 11:09:49 2023 ; 7 h 16 min 45 s 879.47 ms remaining ; 15 h 9 min 55 s 582.22 ms total) Fri Nov 10 04:11:20 2023: Iterated ≈54% of D-proof candidates. [ 588194299 of 1089248702] (ETC: Fri Nov 10 11:09:58 2023 ; 6 h 58 min 38 s 97.29 ms remaining ; 15 h 10 min 4 s 559.32 ms total) Fri Nov 10 04:28:40 2023: Iterated ≈56% of D-proof candidates. [ 609979273 of 1089248702] (ETC: Fri Nov 10 11:08:25 2023 ; 6 h 39 min 45 s 130.67 ms remaining ; 15 h 8 min 31 s 660.59 ms total) Fri Nov 10 04:45:38 2023: Iterated ≈58% of D-proof candidates. [ 631764247 of 1089248702] (ETC: Fri Nov 10 11:06:20 2023 ; 6 h 20 min 42 s 539.22 ms remaining ; 15 h 6 min 26 s 998.11 ms total) Fri Nov 10 05:01:55 2023: Iterated ≈60% of D-proof candidates. [ 653549221 of 1089248702] (ETC: Fri Nov 10 11:03:15 2023 ; 6 h 1 min 20 s 857.79 ms remaining ; 15 h 3 min 22 s 144.45 ms total) Fri Nov 10 05:17:59 2023: Iterated ≈62% of D-proof candidates. [ 675334195 of 1089248702] (ETC: Fri Nov 10 11:00:02 2023 ; 5 h 42 min 3 s 333.66 ms remaining ; 15 h 8 s 772.76 ms total) Fri Nov 10 05:33:48 2023: Iterated ≈64% of D-proof candidates. [ 697119169 of 1089248702] (ETC: Fri Nov 10 10:56:38 2023 ; 5 h 22 min 49 s 518.11 ms remaining ; 14 h 56 min 44 s 216.93 ms total) Fri Nov 10 05:49:11 2023: Iterated ≈66% of D-proof candidates. [ 718904143 of 1089248702] (ETC: Fri Nov 10 10:52:46 2023 ; 5 h 3 min 34 s 756.00 ms remaining ; 14 h 52 min 52 s 811.73 ms total) Fri Nov 10 06:04:20 2023: Iterated ≈68% of D-proof candidates. [ 740689117 of 1089248702] (ETC: Fri Nov 10 10:48:46 2023 ; 4 h 44 min 26 s 441.47 ms remaining ; 14 h 48 min 52 s 629.53 ms total) Fri Nov 10 06:19:16 2023: Iterated ≈70% of D-proof candidates. [ 762474091 of 1089248702] (ETC: Fri Nov 10 10:44:42 2023 ; 4 h 25 min 26 s 652.28 ms remaining ; 14 h 44 min 48 s 840.86 ms total) Fri Nov 10 06:33:59 2023: Iterated ≈72% of D-proof candidates. [ 784259065 of 1089248702] (ETC: Fri Nov 10 10:40:35 2023 ; 4 h 6 min 35 s 574.96 ms remaining ; 14 h 40 min 41 s 339.06 ms total) Fri Nov 10 06:48:19 2023: Iterated ≈74% of D-proof candidates. [ 806044039 of 1089248702] (ETC: Fri Nov 10 10:36:08 2023 ; 3 h 47 min 49 s 541.08 ms remaining ; 14 h 36 min 15 s 157.89 ms total) Fri Nov 10 07:02:34 2023: Iterated ≈76% of D-proof candidates. [ 827829013 of 1089248702] (ETC: Fri Nov 10 10:31:50 2023 ; 3 h 29 min 15 s 924.26 ms remaining ; 14 h 31 min 56 s 350.99 ms total) Fri Nov 10 07:16:24 2023: Iterated ≈78% of D-proof candidates. [ 849613987 of 1089248702] (ETC: Fri Nov 10 10:27:13 2023 ; 3 h 10 min 48 s 686.84 ms remaining ; 14 h 27 min 19 s 485.49 ms total) Fri Nov 10 07:30:03 2023: Iterated ≈80% of D-proof candidates. [ 871398961 of 1089248702] (ETC: Fri Nov 10 10:22:35 2023 ; 2 h 52 min 32 s 433.21 ms remaining ; 14 h 22 min 42 s 165.89 ms total) Fri Nov 10 07:43:40 2023: Iterated ≈82% of D-proof candidates. [ 893183935 of 1089248702] (ETC: Fri Nov 10 10:18:09 2023 ; 2 h 34 min 29 s 186.12 ms remaining ; 14 h 18 min 15 s 478.28 ms total) Fri Nov 10 07:57:06 2023: Iterated ≈84% of D-proof candidates. [ 914968909 of 1089248702] (ETC: Fri Nov 10 10:13:43 2023 ; 2 h 16 min 36 s 786.40 ms remaining ; 14 h 13 min 49 s 914.83 ms total) Fri Nov 10 08:10:28 2023: Iterated ≈86% of D-proof candidates. [ 936753883 of 1089248702] (ETC: Fri Nov 10 10:09:24 2023 ; 1 h 58 min 55 s 949.85 ms remaining ; 14 h 9 min 31 s 70.12 ms total) Fri Nov 10 08:23:42 2023: Iterated ≈88% of D-proof candidates. [ 958538857 of 1089248702] (ETC: Fri Nov 10 10:05:08 2023 ; 1 h 41 min 25 s 795.98 ms remaining ; 14 h 5 min 14 s 966.17 ms total) Fri Nov 10 08:36:54 2023: Iterated ≈90% of D-proof candidates. [ 980323831 of 1089248702] (ETC: Fri Nov 10 10:01:01 2023 ; 1 h 24 min 6 s 778.00 ms remaining ; 14 h 1 min 7 s 779.59 ms total) Fri Nov 10 08:50:06 2023: Iterated ≈92% of D-proof candidates. [1002108805 of 1089248702] (ETC: Fri Nov 10 09:57:04 2023 ; 1 h 6 min 58 s 454.71 ms remaining ; 13 h 57 min 10 s 683.44 ms total) Fri Nov 10 09:03:07 2023: Iterated ≈94% of D-proof candidates. [1023893779 of 1089248702] (ETC: Fri Nov 10 09:53:06 2023 ; 49 min 59 s 587.28 ms remaining ; 13 h 53 min 13 s 120.67 ms total) Fri Nov 10 09:16:09 2023: Iterated ≈96% of D-proof candidates. [1045678753 of 1089248702] (ETC: Fri Nov 10 09:49:19 2023 ; 33 min 10 s 647.26 ms remaining ; 13 h 49 min 26 s 180.44 ms total) Fri Nov 10 09:29:09 2023: Iterated ≈98% of D-proof candidates. [1067463727 of 1089248702] (ETC: Fri Nov 10 09:45:40 2023 ; 16 min 30 s 933.97 ms remaining ; 13 h 45 min 46 s 696.38 ms total) Fri Nov 10 09:42:21 2023: Iterated 100% of D-proof candidates. [1089248702 of 1089248702] (ETC: Fri Nov 10 09:42:21 2023 ; 0.00 ms remaining ; 13 h 42 min 28 s 61.28 ms total) 49349065.90 ms (13 h 42 min 29 s 65.90 ms) taken to collect 101757325 D-proofs of length 163. [iterated 1089248702 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 } } 776722.83 ms (12 min 56 s 722.83 ms) taken to filter and order new representative proofs. Found 101757325 representative, 187537763 redundant, and 799953614 invalid condensed detachment proof strings. lengths up to 163 ; 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)} ; 101757325 new representative proofs (187537763 redundant, 799953614 invalid) Fri Nov 10 10:04:55 2023: Starting to write 101757325 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt. 214250.74 ms (3 min 34 s 250.74 ms) taken to print and save 75698437452 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt. Fri Nov 10 10:10:34 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 163, unfiltered] Fri Nov 10 10:13:49 2023: Process terminated. [pid: 254588, tid:23141686105984]