( 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: 10.06888… h CPU utilization: 644.40888… core-h ) Thu Nov 9 03:51:16 2023: Process started. [pid: 53152, tid:22603806386048] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(161, 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(161, false, true). Thu Nov 9 03:51:16 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 161, unfiltered] 0.01 ms taken to load initial representatives. 8.50 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22603725125376] 8.95 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22603741935360] 8.74 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22603735631616] 2.43 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22603737732864] 0.55 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22603712517888] 1.29 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22603744036608] 0.49 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22603739834112] 0.91 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22603731429120] 0.22 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22603710416640] 0.66 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22603733530368] 1.14 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22603727226624] 1.94 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22603746137856] 14391.16 ms (14 s 391.16 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22603744036608] 7208.15 ms (7 s 208.15 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22603741935360] 14146.26 ms (14 s 146.26 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22603739834112] 10464.94 ms (10 s 464.94 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22603737732864] 1.11 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22603473352448] 8322.13 ms (8 s 322.13 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22603735631616] 16154.71 ms (16 s 154.71 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:22603733530368] 15090.57 ms (15 s 90.57 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22603731429120] 3.29 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22603729327872] 17131.88 ms (17 s 131.88 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:22603727226624] 8547.79 ms (8 s 547.79 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22603725125376] 0.13 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22603723024128] 5.05 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22603720922880] 4.42 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22603718821632] 2.62 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22603716720384] 0.14 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22603714619136] 11257.83 ms (11 s 257.83 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22603712517888] 15688.41 ms (15 s 688.41 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22603710416640] 0.39 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22603708315392] 3.49 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22603706214144] 10.36 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22603704112896] 10.38 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22603702011648] 0.31 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22603699910400] 0.76 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22603697809152] 16.34 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22603695707904] 7.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22603693606656] 10.65 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22603691505408] 9.12 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22603689404160] 3.16 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22603687302912] 4.78 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22603685201664] 10.64 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22603683100416] 7.19 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22603680999168] 392.80 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22603678897920] 435.67 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22603676796672] 5.86 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22603471251200] 27.64 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22603469149952] 394.03 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22603467048704] 400.68 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22603464947456] 85.15 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22603462846208] 39.82 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22603460744960] 403.58 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22603458643712] 488.48 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22603456542464] 42.82 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22603454441216] 47.52 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22603452339968] 50.69 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22603450238720] 719.09 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22603448137472] 433.93 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22603446036224] 935.18 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22603443934976] 144.87 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22603441833728] 228.50 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22603439732480] 1441.35 ms (1 s 441.35 ms) taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22603437631232] 1646.07 ms (1 s 646.07 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22603435529984] 1627.75 ms (1 s 627.75 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22603433428736] 1812.48 ms (1 s 812.48 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22603431327488] 2174.47 ms (2 s 174.47 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22603429226240] 2944.27 ms (2 s 944.27 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22603427124992] 3580.60 ms (3 s 580.60 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22603425023744] 5904.80 ms (5 s 904.80 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22603422922496] 2980.34 ms (2 s 980.34 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22603420821248] 3749.61 ms (3 s 749.61 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22603418720000] 4362.59 ms (4 s 362.59 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22603416618752] 5018.06 ms (5 s 18.06 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22603414517504] 6116.85 ms (6 s 116.85 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22603412416256] 17292.08 ms (17 s 292.08 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. 45835.52 ms (45 s 835.52 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:22603412416256] 57578.31 ms (57 s 578.32 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:22603414517504] 72013.16 ms (1 min 12 s 13.16 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:22603416618752] 81607.91 ms (1 min 21 s 607.91 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:22603418720000] 81630.21 ms (1 min 21 s 630.21 ms) additional read duration. Loaded 4 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 162335238 representatives in total. Thu Nov 9 03:53:14 2023: Inserted ≈ 5% of D-proof conclusions. [ 8116761 of 162335238] (ETC: Thu Nov 9 03:59:09 2023 ; 5 min 54 s 778.87 ms remaining ; 6 min 13 s 451.44 ms total) Thu Nov 9 03:53:35 2023: Inserted ≈10% of D-proof conclusions. [ 16233523 of 162335238] (ETC: Thu Nov 9 03:59:33 2023 ; 5 min 57 s 781.88 ms remaining ; 6 min 37 s 535.42 ms total) Thu Nov 9 03:53:53 2023: Inserted ≈15% of D-proof conclusions. [ 24350285 of 162335238] (ETC: Thu Nov 9 03:59:21 2023 ; 5 min 27 s 765.50 ms remaining ; 6 min 25 s 606.47 ms total) Thu Nov 9 03:54:06 2023: Inserted ≈20% of D-proof conclusions. [ 32467047 of 162335238] (ETC: Thu Nov 9 03:58:50 2023 ; 4 min 44 s 179.59 ms remaining ; 5 min 55 s 224.49 ms total) Thu Nov 9 03:54:19 2023: Inserted ≈25% of D-proof conclusions. [ 40583809 of 162335238] (ETC: Thu Nov 9 03:58:32 2023 ; 4 min 12 s 995.54 ms remaining ; 5 min 37 s 327.39 ms total) Thu Nov 9 03:54:34 2023: Inserted ≈30% of D-proof conclusions. [ 48700571 of 162335238] (ETC: Thu Nov 9 03:58:24 2023 ; 3 min 50 s 520.35 ms remaining ; 5 min 29 s 314.79 ms total) Thu Nov 9 03:54:48 2023: Inserted ≈35% of D-proof conclusions. [ 56817333 of 162335238] (ETC: Thu Nov 9 03:58:19 2023 ; 3 min 30 s 460.92 ms remaining ; 5 min 23 s 786.03 ms total) Thu Nov 9 03:55:04 2023: Inserted ≈40% of D-proof conclusions. [ 64934095 of 162335238] (ETC: Thu Nov 9 03:58:17 2023 ; 3 min 12 s 886.58 ms remaining ; 5 min 21 s 477.63 ms total) Thu Nov 9 03:55:17 2023: Inserted ≈45% of D-proof conclusions. [ 73050857 of 162335238] (ETC: Thu Nov 9 03:58:11 2023 ; 2 min 53 s 759.81 ms remaining ; 5 min 15 s 926.93 ms total) Thu Nov 9 03:55:31 2023: Inserted ≈50% of D-proof conclusions. [ 81167619 of 162335238] (ETC: Thu Nov 9 03:58:07 2023 ; 2 min 35 s 692.52 ms remaining ; 5 min 11 s 385.04 ms total) Thu Nov 9 03:55:45 2023: Inserted ≈55% of D-proof conclusions. [ 89284380 of 162335238] (ETC: Thu Nov 9 03:58:04 2023 ; 2 min 19 s 43.48 ms remaining ; 5 min 8 s 985.50 ms total) Thu Nov 9 03:55:59 2023: Inserted ≈60% of D-proof conclusions. [ 97401142 of 162335238] (ETC: Thu Nov 9 03:58:02 2023 ; 2 min 2 s 686.29 ms remaining ; 5 min 6 s 715.72 ms total) Thu Nov 9 03:56:14 2023: Inserted ≈65% of D-proof conclusions. [105517904 of 162335238] (ETC: Thu Nov 9 03:58:02 2023 ; 1 min 47 s 253.38 ms remaining ; 5 min 6 s 438.22 ms total) Thu Nov 9 03:56:31 2023: Inserted ≈70% of D-proof conclusions. [113634666 of 162335238] (ETC: Thu Nov 9 03:58:04 2023 ; 1 min 32 s 600.75 ms remaining ; 5 min 8 s 669.15 ms total) Thu Nov 9 03:56:45 2023: Inserted ≈75% of D-proof conclusions. [121751428 of 162335238] (ETC: Thu Nov 9 03:58:02 2023 ; 1 min 16 s 741.32 ms remaining ; 5 min 6 s 965.27 ms total) Thu Nov 9 03:57:00 2023: Inserted ≈80% of D-proof conclusions. [129868190 of 162335238] (ETC: Thu Nov 9 03:58:01 2023 ; 1 min 1 s 156.03 ms remaining ; 5 min 5 s 780.14 ms total) Thu Nov 9 03:57:15 2023: Inserted ≈85% of D-proof conclusions. [137984952 of 162335238] (ETC: Thu Nov 9 03:58:01 2023 ; 45 s 872.13 ms remaining ; 5 min 5 s 814.17 ms total) Thu Nov 9 03:57:30 2023: Inserted ≈90% of D-proof conclusions. [146101714 of 162335238] (ETC: Thu Nov 9 03:58:01 2023 ; 30 s 561.26 ms remaining ; 5 min 5 s 612.63 ms total) Thu Nov 9 03:57:45 2023: Inserted ≈95% of D-proof conclusions. [154218476 of 162335238] (ETC: Thu Nov 9 03:58:00 2023 ; 15 s 253.95 ms remaining ; 5 min 5 s 78.98 ms total) Thu Nov 9 03:58:03 2023: Inserted 100% of D-proof conclusions. [162335238 of 162335238] (ETC: Thu Nov 9 03:58:03 2023 ; 0.00 ms remaining ; 5 min 7 s 975.71 ms total) 307977.26 ms (5 min 7 s 977.26 ms) total insertion duration. Known iteration count loaded from 161:784979956. Thu Nov 9 03:58:03 2023: Starting to generate D-proof representatives of length 161. Thu Nov 9 04:09:42 2023: Iterated ≈ 2% of D-proof candidates. [ 15699599 of 784979956] (ETC: Thu Nov 9 13:40:13 2023 ; 9 h 30 min 31 s 66.18 ms remaining ; 9 h 42 min 9 s 659.37 ms total) Thu Nov 9 04:20:18 2023: Iterated ≈ 4% of D-proof candidates. [ 31399198 of 784979956] (ETC: Thu Nov 9 13:14:13 2023 ; 8 h 53 min 54 s 608.80 ms remaining ; 9 h 16 min 9 s 384.16 ms total) Thu Nov 9 04:30:16 2023: Iterated ≈ 6% of D-proof candidates. [ 47098797 of 784979956] (ETC: Thu Nov 9 12:55:05 2023 ; 8 h 24 min 48 s 342.55 ms remaining ; 8 h 57 min 1 s 641.00 ms total) Thu Nov 9 04:42:06 2023: Iterated ≈ 8% of D-proof candidates. [ 62798396 of 784979956] (ETC: Thu Nov 9 13:08:42 2023 ; 8 h 26 min 36 s 119.99 ms remaining ; 9 h 10 min 39 s 260.84 ms total) Thu Nov 9 04:53:04 2023: Iterated ≈10% of D-proof candidates. [ 78497995 of 784979956] (ETC: Thu Nov 9 13:08:11 2023 ; 8 h 15 min 6 s 700.47 ms remaining ; 9 h 10 min 7 s 444.94 ms total) Thu Nov 9 05:03:43 2023: Iterated ≈12% of D-proof candidates. [ 94197594 of 784979956] (ETC: Thu Nov 9 13:05:11 2023 ; 8 h 1 min 28 s 787.53 ms remaining ; 9 h 7 min 8 s 167.62 ms total) Thu Nov 9 05:16:03 2023: Iterated ≈14% of D-proof candidates. [109897193 of 784979956] (ETC: Thu Nov 9 13:15:08 2023 ; 7 h 59 min 5 s 570.04 ms remaining ; 9 h 17 min 5 s 81.41 ms total) Thu Nov 9 05:28:24 2023: Iterated ≈16% of D-proof candidates. [125596792 of 784979956] (ETC: Thu Nov 9 13:22:40 2023 ; 7 h 54 min 16 s 936.51 ms remaining ; 9 h 24 min 37 s 305.31 ms total) Thu Nov 9 05:40:23 2023: Iterated ≈18% of D-proof candidates. [141296392 of 784979956] (ETC: Thu Nov 9 13:26:35 2023 ; 7 h 46 min 11 s 341.33 ms remaining ; 9 h 28 min 31 s 391.86 ms total) Thu Nov 9 05:52:42 2023: Iterated ≈20% of D-proof candidates. [156995991 of 784979956] (ETC: Thu Nov 9 13:31:17 2023 ; 7 h 38 min 34 s 981.84 ms remaining ; 9 h 33 min 13 s 727.29 ms total) Thu Nov 9 06:03:55 2023: Iterated ≈22% of D-proof candidates. [172695590 of 784979956] (ETC: Thu Nov 9 13:30:09 2023 ; 7 h 26 min 14 s 394.96 ms remaining ; 9 h 32 min 6 s 147.37 ms total) Thu Nov 9 06:17:28 2023: Iterated ≈24% of D-proof candidates. [188395189 of 784979956] (ETC: Thu Nov 9 13:38:57 2023 ; 7 h 21 min 28 s 750.32 ms remaining ; 9 h 40 min 53 s 618.81 ms total) Thu Nov 9 06:32:11 2023: Iterated ≈26% of D-proof candidates. [204094788 of 784979956] (ETC: Thu Nov 9 13:50:51 2023 ; 7 h 18 min 39 s 871.38 ms remaining ; 9 h 52 min 47 s 393.73 ms total) Thu Nov 9 06:45:46 2023: Iterated ≈28% of D-proof candidates. [219794387 of 784979956] (ETC: Thu Nov 9 13:57:03 2023 ; 7 h 11 min 16 s 893.04 ms remaining ; 9 h 59 min 129.18 ms total) Thu Nov 9 06:58:00 2023: Iterated ≈30% of D-proof candidates. [235493986 of 784979956] (ETC: Thu Nov 9 13:57:52 2023 ; 6 h 59 min 52 s 186.88 ms remaining ; 9 h 59 min 48 s 838.35 ms total) Thu Nov 9 07:13:38 2023: Iterated ≈32% of D-proof candidates. [251193585 of 784979956] (ETC: Thu Nov 9 14:09:16 2023 ; 6 h 55 min 37 s 527.94 ms remaining ; 10 h 11 min 12 s 835.15 ms total) Thu Nov 9 07:27:31 2023: Iterated ≈34% of D-proof candidates. [266893185 of 784979956] (ETC: Thu Nov 9 14:14:08 2023 ; 6 h 46 min 36 s 666.95 ms remaining ; 10 h 16 min 4 s 646.89 ms total) Thu Nov 9 07:40:15 2023: Iterated ≈36% of D-proof candidates. [282592784 of 784979956] (ETC: Thu Nov 9 14:15:15 2023 ; 6 h 35 min 300.29 ms remaining ; 10 h 17 min 11 s 719.20 ms total) Thu Nov 9 07:54:26 2023: Iterated ≈38% of D-proof candidates. [298292383 of 784979956] (ETC: Thu Nov 9 14:20:06 2023 ; 6 h 25 min 40 s 143.06 ms remaining ; 10 h 22 min 2 s 811.37 ms total) Thu Nov 9 08:08:35 2023: Iterated ≈40% of D-proof candidates. [313991982 of 784979956] (ETC: Thu Nov 9 14:24:22 2023 ; 6 h 15 min 47 s 341.64 ms remaining ; 10 h 26 min 18 s 902.71 ms total) Thu Nov 9 08:21:51 2023: Iterated ≈42% of D-proof candidates. [329691581 of 784979956] (ETC: Thu Nov 9 14:26:08 2023 ; 6 h 4 min 17 s 309.58 ms remaining ; 10 h 28 min 5 s 16.48 ms total) Thu Nov 9 08:35:21 2023: Iterated ≈44% of D-proof candidates. [345391180 of 784979956] (ETC: Thu Nov 9 14:28:17 2023 ; 5 h 52 min 55 s 966.39 ms remaining ; 10 h 30 min 14 s 225.65 ms total) Thu Nov 9 08:48:13 2023: Iterated ≈46% of D-proof candidates. [361090779 of 784979956] (ETC: Thu Nov 9 14:28:50 2023 ; 5 h 40 min 37 s 68.55 ms remaining ; 10 h 30 min 46 s 423.17 ms total) Thu Nov 9 09:00:41 2023: Iterated ≈48% of D-proof candidates. [376790378 of 784979956] (ETC: Thu Nov 9 14:28:31 2023 ; 5 h 27 min 50 s 422.97 ms remaining ; 10 h 30 min 27 s 736.40 ms total) Thu Nov 9 09:12:57 2023: Iterated ≈50% of D-proof candidates. [392489978 of 784979956] (ETC: Thu Nov 9 14:27:51 2023 ; 5 h 14 min 53 s 992.57 ms remaining ; 10 h 29 min 47 s 985.13 ms total) Thu Nov 9 09:24:53 2023: Iterated ≈52% of D-proof candidates. [408189577 of 784979956] (ETC: Thu Nov 9 14:26:34 2023 ; 5 h 1 min 41 s 95.40 ms remaining ; 10 h 28 min 30 s 615.41 ms total) Thu Nov 9 09:36:33 2023: Iterated ≈54% of D-proof candidates. [423889176 of 784979956] (ETC: Thu Nov 9 14:24:55 2023 ; 4 h 48 min 21 s 367.19 ms remaining ; 10 h 26 min 51 s 667.78 ms total) Thu Nov 9 09:47:53 2023: Iterated ≈56% of D-proof candidates. [439588775 of 784979956] (ETC: Thu Nov 9 14:22:44 2023 ; 4 h 34 min 51 s 744.53 ms remaining ; 10 h 24 min 41 s 237.53 ms total) Thu Nov 9 09:59:01 2023: Iterated ≈58% of D-proof candidates. [455288374 of 784979956] (ETC: Thu Nov 9 14:20:24 2023 ; 4 h 21 min 22 s 977.77 ms remaining ; 10 h 22 min 20 s 423.21 ms total) Thu Nov 9 10:10:01 2023: Iterated ≈60% of D-proof candidates. [470987973 of 784979956] (ETC: Thu Nov 9 14:18:00 2023 ; 4 h 7 min 58 s 693.37 ms remaining ; 10 h 19 min 56 s 733.35 ms total) Thu Nov 9 10:20:47 2023: Iterated ≈62% of D-proof candidates. [486687572 of 784979956] (ETC: Thu Nov 9 14:15:22 2023 ; 3 h 54 min 34 s 790.26 ms remaining ; 10 h 17 min 18 s 921.64 ms total) Thu Nov 9 10:31:29 2023: Iterated ≈64% of D-proof candidates. [502387171 of 784979956] (ETC: Thu Nov 9 14:12:47 2023 ; 3 h 41 min 18 s 336.70 ms remaining ; 10 h 14 min 44 s 268.49 ms total) Thu Nov 9 10:42:01 2023: Iterated ≈66% of D-proof candidates. [518086770 of 784979956] (ETC: Thu Nov 9 14:10:07 2023 ; 3 h 28 min 6 s 125.27 ms remaining ; 10 h 12 min 3 s 897.72 ms total) Thu Nov 9 10:52:23 2023: Iterated ≈68% of D-proof candidates. [533786370 of 784979956] (ETC: Thu Nov 9 14:07:22 2023 ; 3 h 14 min 58 s 781.41 ms remaining ; 10 h 9 min 18 s 691.90 ms total) Thu Nov 9 11:02:39 2023: Iterated ≈70% of D-proof candidates. [549485969 of 784979956] (ETC: Thu Nov 9 14:04:37 2023 ; 3 h 1 min 58 s 102.08 ms remaining ; 10 h 6 min 33 s 673.58 ms total) Thu Nov 9 11:12:46 2023: Iterated ≈72% of D-proof candidates. [565185568 of 784979956] (ETC: Thu Nov 9 14:01:50 2023 ; 2 h 49 min 3 s 409.80 ms remaining ; 10 h 3 min 46 s 463.52 ms total) Thu Nov 9 11:22:52 2023: Iterated ≈74% of D-proof candidates. [580885167 of 784979956] (ETC: Thu Nov 9 13:59:09 2023 ; 2 h 36 min 17 s 59.04 ms remaining ; 10 h 1 min 5 s 611.60 ms total) Thu Nov 9 11:32:48 2023: Iterated ≈76% of D-proof candidates. [596584766 of 784979956] (ETC: Thu Nov 9 13:56:24 2023 ; 2 h 23 min 36 s 299.14 ms remaining ; 9 h 58 min 21 s 246.31 ms total) Thu Nov 9 11:42:37 2023: Iterated ≈78% of D-proof candidates. [612284365 of 784979956] (ETC: Thu Nov 9 13:53:39 2023 ; 2 h 11 min 1 s 890.47 ms remaining ; 9 h 55 min 35 s 865.63 ms total) Thu Nov 9 11:52:24 2023: Iterated ≈80% of D-proof candidates. [627983964 of 784979956] (ETC: Thu Nov 9 13:50:59 2023 ; 1 h 58 min 35 s 248.14 ms remaining ; 9 h 52 min 56 s 240.52 ms total) Thu Nov 9 12:02:06 2023: Iterated ≈82% of D-proof candidates. [643683563 of 784979956] (ETC: Thu Nov 9 13:48:22 2023 ; 1 h 46 min 15 s 353.91 ms remaining ; 9 h 50 min 18 s 632.63 ms total) Thu Nov 9 12:11:46 2023: Iterated ≈84% of D-proof candidates. [659383163 of 784979956] (ETC: Thu Nov 9 13:45:48 2023 ; 1 h 34 min 2 s 360.15 ms remaining ; 9 h 47 min 44 s 750.90 ms total) Thu Nov 9 12:21:26 2023: Iterated ≈86% of D-proof candidates. [675082762 of 784979956] (ETC: Thu Nov 9 13:43:23 2023 ; 1 h 21 min 56 s 786.04 ms remaining ; 9 h 45 min 19 s 900.27 ms total) Thu Nov 9 12:31:10 2023: Iterated ≈88% of D-proof candidates. [690782361 of 784979956] (ETC: Thu Nov 9 13:41:08 2023 ; 1 h 9 min 58 s 139.56 ms remaining ; 9 h 43 min 4 s 496.24 ms total) Thu Nov 9 12:40:43 2023: Iterated ≈90% of D-proof candidates. [706481960 of 784979956] (ETC: Thu Nov 9 13:38:47 2023 ; 58 min 4 s 372.63 ms remaining ; 9 h 40 min 43 s 726.10 ms total) Thu Nov 9 12:50:14 2023: Iterated ≈92% of D-proof candidates. [722181559 of 784979956] (ETC: Thu Nov 9 13:36:31 2023 ; 46 min 16 s 592.71 ms remaining ; 9 h 38 min 27 s 408.59 ms total) Thu Nov 9 12:59:43 2023: Iterated ≈94% of D-proof candidates. [737881158 of 784979956] (ETC: Thu Nov 9 13:34:18 2023 ; 34 min 34 s 479.45 ms remaining ; 9 h 36 min 14 s 656.97 ms total) Thu Nov 9 13:09:13 2023: Iterated ≈96% of D-proof candidates. [753580757 of 784979956] (ETC: Thu Nov 9 13:32:11 2023 ; 22 min 57 s 896.60 ms remaining ; 9 h 34 min 7 s 414.18 ms total) Thu Nov 9 13:18:44 2023: Iterated ≈98% of D-proof candidates. [769280356 of 784979956] (ETC: Thu Nov 9 13:30:11 2023 ; 11 min 26 s 548.99 ms remaining ; 9 h 32 min 7 s 447.51 ms total) Thu Nov 9 13:28:20 2023: Iterated 100% of D-proof candidates. [784979956 of 784979956] (ETC: Thu Nov 9 13:28:20 2023 ; 0.00 ms remaining ; 9 h 30 min 17 s 90.39 ms total) 34218093.27 ms (9 h 30 min 18 s 93.28 ms) taken to collect 78239557 D-proofs of length 161. [iterated 784979956 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 } } 700740.81 ms (11 min 40 s 740.81 ms) taken to filter and order new representative proofs. Found 78239557 representative, 118848510 redundant, and 587891889 invalid condensed detachment proof strings. lengths up to 161 ; 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)} ; 78239557 new representative proofs (118848510 redundant, 587891889 invalid) Thu Nov 9 13:46:40 2023: Starting to write 78239557 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. 195331.95 ms (3 min 15 s 331.95 ms) taken to print and save 55681200733 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. Thu Nov 9 13:51:44 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 161, unfiltered] Thu Nov 9 13:55:24 2023: Process terminated. [pid: 53152, tid:22603806386048]