( 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 MPI node — 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory — running Linux, Rocky 8.8. Wall-clock time: 4.7930555… h CPU utilization: 230.0666… core-h ) Sun Oct 22 09:39:40 2023: Process started. [pid: 73513, tid:23253839562624] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(155, 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(155, false, true). Sun Oct 22 09:39:40 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 155, unfiltered] 0.01 ms taken to load initial representatives. 3.88 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23253139556096] 1.32 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23253154264832] 0.81 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23253775136512] 0.85 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23253766731520] 0.94 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23253762529024] 0.08 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23253150062336] 0.60 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23253779339008] 0.65 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23253147961088] 0.67 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23253764630272] 0.16 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23253126948608] 0.48 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23253152163584] 2.02 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23253131151104] 0.71 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23253112239872] 0.04 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23253141657344] 0.70 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23253129049856] 0.82 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23253133252352] 0.55 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23253135353600] 0.24 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23253777237760] 0.21 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23253143758592] 0.76 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23253145859840] 0.17 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23253137454848] 0.50 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23253773035264] 0.97 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23253108037376] 0.46 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23253770934016] 0.02 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23253760427776] 0.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23253120644864] 1.85 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23253114341120] 1697.80 ms (1 s 697.80 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23253779339008] 3926.67 ms (3 s 926.67 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23253777237760] 437.41 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23253775136512] 7070.97 ms (7 s 70.97 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23253773035264] 8655.92 ms (8 s 655.92 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23253770934016] 3.98 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23253768832768] 643.30 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23253766731520] 3595.78 ms (3 s 595.78 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23253764630272] 759.94 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23253762529024] 9354.35 ms (9 s 354.36 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23253760427776] 325.12 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23253154264832] 8464.69 ms (8 s 464.69 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23253152163584] 1177.73 ms (1 s 177.73 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23253150062336] 2583.07 ms (2 s 583.07 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23253147961088] 5440.51 ms (5 s 440.51 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23253145859840] 4603.10 ms (4 s 603.10 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23253143758592] 2009.97 ms (2 s 9.97 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23253141657344] 169.36 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23253139556096] 6167.82 ms (6 s 167.82 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23253137454848] 3337.10 ms (3 s 337.11 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23253135353600] 2884.76 ms (2 s 884.76 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23253133252352] 1294.50 ms (1 s 294.50 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23253131151104] 2418.99 ms (2 s 418.99 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23253129049856] 6119.89 ms (6 s 119.89 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23253126948608] 3.54 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23253124847360] 3.31 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23253122746112] 10103.53 ms (10 s 103.53 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23253120644864] 3.87 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23253118543616] 10.54 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23253116442368] 11016.32 ms (11 s 16.32 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23253114341120] 1615.08 ms (1 s 615.08 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23253112239872] 9.32 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23253110138624] 7882.52 ms (7 s 882.52 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23253108037376] 3.42 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23253105936128] 24.59 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23253103834880] 21.12 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23253101733632] 27.18 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23253099632384] 6.91 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23253097531136] 23.97 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23253095429888] 40.58 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23253093328640] 32.87 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23253091227392] 28.13 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23250939672320] 28.70 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23250805454592] 35.82 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23250937571072] 59.32 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23250935469824] 55.48 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23250933368576] 89.95 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23250931267328] 139.93 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23250929166080] 11080.08 ms (11 s 80.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. 19883.87 ms (19 s 883.87 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:23250929166080] 19885.56 ms (19 s 885.56 ms) additional read duration. Loaded 1 more representative collection of size: 153 : 21395853 45444063 representatives in total. Sun Oct 22 09:40:13 2023: Inserted ≈ 5% of D-proof conclusions. [ 2272203 of 45444063] (ETC: Sun Oct 22 09:40:57 2023 ; 44 s 538.95 ms remaining ; 46 s 883.10 ms total) Sun Oct 22 09:40:16 2023: Inserted ≈10% of D-proof conclusions. [ 4544406 of 45444063] (ETC: Sun Oct 22 09:41:02 2023 ; 45 s 971.20 ms remaining ; 51 s 79.11 ms total) Sun Oct 22 09:40:18 2023: Inserted ≈15% of D-proof conclusions. [ 6816609 of 45444063] (ETC: Sun Oct 22 09:41:02 2023 ; 43 s 621.60 ms remaining ; 51 s 319.52 ms total) Sun Oct 22 09:40:21 2023: Inserted ≈20% of D-proof conclusions. [ 9088812 of 45444063] (ETC: Sun Oct 22 09:41:02 2023 ; 40 s 839.15 ms remaining ; 51 s 48.93 ms total) Sun Oct 22 09:40:23 2023: Inserted ≈25% of D-proof conclusions. [11361015 of 45444063] (ETC: Sun Oct 22 09:41:01 2023 ; 37 s 992.48 ms remaining ; 50 s 656.64 ms total) Sun Oct 22 09:40:26 2023: Inserted ≈30% of D-proof conclusions. [13633218 of 45444063] (ETC: Sun Oct 22 09:41:00 2023 ; 34 s 990.02 ms remaining ; 49 s 985.75 ms total) Sun Oct 22 09:40:28 2023: Inserted ≈35% of D-proof conclusions. [15905422 of 45444063] (ETC: Sun Oct 22 09:41:01 2023 ; 32 s 936.56 ms remaining ; 50 s 671.64 ms total) Sun Oct 22 09:40:31 2023: Inserted ≈40% of D-proof conclusions. [18177625 of 45444063] (ETC: Sun Oct 22 09:41:02 2023 ; 30 s 678.37 ms remaining ; 51 s 130.61 ms total) Sun Oct 22 09:40:34 2023: Inserted ≈45% of D-proof conclusions. [20449828 of 45444063] (ETC: Sun Oct 22 09:41:03 2023 ; 28 s 804.22 ms remaining ; 52 s 371.31 ms total) Sun Oct 22 09:40:37 2023: Inserted ≈50% of D-proof conclusions. [22722031 of 45444063] (ETC: Sun Oct 22 09:41:03 2023 ; 26 s 440.44 ms remaining ; 52 s 880.88 ms total) Sun Oct 22 09:40:40 2023: Inserted ≈55% of D-proof conclusions. [24994234 of 45444063] (ETC: Sun Oct 22 09:41:04 2023 ; 24 s 78.93 ms remaining ; 53 s 508.73 ms total) Sun Oct 22 09:40:42 2023: Inserted ≈60% of D-proof conclusions. [27266437 of 45444063] (ETC: Sun Oct 22 09:41:04 2023 ; 21 s 310.65 ms remaining ; 53 s 276.62 ms total) Sun Oct 22 09:40:45 2023: Inserted ≈65% of D-proof conclusions. [29538640 of 45444063] (ETC: Sun Oct 22 09:41:04 2023 ; 18 s 759.45 ms remaining ; 53 s 598.43 ms total) Sun Oct 22 09:40:48 2023: Inserted ≈70% of D-proof conclusions. [31810844 of 45444063] (ETC: Sun Oct 22 09:41:04 2023 ; 16 s 160.55 ms remaining ; 53 s 868.48 ms total) Sun Oct 22 09:40:51 2023: Inserted ≈75% of D-proof conclusions. [34083047 of 45444063] (ETC: Sun Oct 22 09:41:05 2023 ; 13 s 567.42 ms remaining ; 54 s 269.69 ms total) Sun Oct 22 09:40:54 2023: Inserted ≈80% of D-proof conclusions. [36355250 of 45444063] (ETC: Sun Oct 22 09:41:05 2023 ; 10 s 866.90 ms remaining ; 54 s 334.49 ms total) Sun Oct 22 09:40:57 2023: Inserted ≈85% of D-proof conclusions. [38627453 of 45444063] (ETC: Sun Oct 22 09:41:05 2023 ; 8 s 187.97 ms remaining ; 54 s 586.43 ms total) Sun Oct 22 09:41:00 2023: Inserted ≈90% of D-proof conclusions. [40899656 of 45444063] (ETC: Sun Oct 22 09:41:06 2023 ; 5 s 500.09 ms remaining ; 55 s 0.89 ms total) Sun Oct 22 09:41:04 2023: Inserted ≈95% of D-proof conclusions. [43171859 of 45444063] (ETC: Sun Oct 22 09:41:06 2023 ; 2 s 798.23 ms remaining ; 55 s 964.66 ms total) Sun Oct 22 09:41:08 2023: Inserted 100% of D-proof conclusions. [45444063 of 45444063] (ETC: Sun Oct 22 09:41:08 2023 ; 0.00 ms remaining ; 57 s 744.84 ms total) 57745.06 ms (57 s 745.06 ms) total insertion duration. Estimated iteration count set to 293366090, based on entry 153:234799156 and last known pair (151:187924390, 153:234799156) with 234799156/187924390 ≈ 1.24943 and 234799156 * (234799156/187924390)^1 ≈ 293366090.79. Sun Oct 22 09:41:08 2023: Starting to generate D-proof representatives of length 155. Sun Oct 22 09:47:12 2023: Iterated ≈ 2% of D-proof candidates. [ 5867321 of approximately 293366090] (ETC: Sun Oct 22 14:44:13 2023 ; 4 h 57 min 1 s 283.47 ms remaining ; 5 h 3 min 4 s 983.08 ms total) Sun Oct 22 09:53:09 2023: Iterated ≈ 4% of D-proof candidates. [ 11734643 of approximately 293366090] (ETC: Sun Oct 22 14:41:31 2023 ; 4 h 48 min 22 s 180.76 ms remaining ; 5 h 23 s 104.92 ms total) Sun Oct 22 09:58:49 2023: Iterated ≈ 6% of D-proof candidates. [ 17601965 of approximately 293366090] (ETC: Sun Oct 22 14:35:49 2023 ; 4 h 36 min 59 s 782.76 ms remaining ; 4 h 54 min 40 s 619.94 ms total) Sun Oct 22 10:04:10 2023: Iterated ≈ 8% of D-proof candidates. [ 23469287 of approximately 293366090] (ETC: Sun Oct 22 14:28:55 2023 ; 4 h 24 min 45 s 612.97 ms remaining ; 4 h 47 min 46 s 970.61 ms total) Sun Oct 22 10:09:42 2023: Iterated ≈ 10% of D-proof candidates. [ 29336609 of approximately 293366090] (ETC: Sun Oct 22 14:26:48 2023 ; 4 h 17 min 5 s 371.51 ms remaining ; 4 h 45 min 39 s 301.68 ms total) Sun Oct 22 10:14:41 2023: Iterated ≈ 12% of D-proof candidates. [ 35203930 of approximately 293366090] (ETC: Sun Oct 22 14:20:42 2023 ; 4 h 6 min 591.77 ms remaining ; 4 h 39 min 33 s 399.69 ms total) Sun Oct 22 10:19:25 2023: Iterated ≈ 14% of D-proof candidates. [ 41071252 of approximately 293366090] (ETC: Sun Oct 22 14:14:31 2023 ; 3 h 55 min 6 s 777.30 ms remaining ; 4 h 33 min 23 s 229.38 ms total) Sun Oct 22 10:24:42 2023: Iterated ≈ 16% of D-proof candidates. [ 46938574 of approximately 293366090] (ETC: Sun Oct 22 14:13:25 2023 ; 3 h 48 min 43 s 103.44 ms remaining ; 4 h 32 min 17 s 27.88 ms total) Sun Oct 22 10:30:21 2023: Iterated ≈ 18% of D-proof candidates. [ 52805896 of approximately 293366090] (ETC: Sun Oct 22 14:14:32 2023 ; 3 h 44 min 11 s 328.46 ms remaining ; 4 h 33 min 24 s 59.09 ms total) Sun Oct 22 10:36:17 2023: Iterated ≈ 20% of D-proof candidates. [ 58673218 of approximately 293366090] (ETC: Sun Oct 22 14:16:53 2023 ; 3 h 40 min 35 s 437.08 ms remaining ; 4 h 35 min 44 s 296.35 ms total) Sun Oct 22 10:42:27 2023: Iterated ≈ 22% of D-proof candidates. [ 64540539 of approximately 293366090] (ETC: Sun Oct 22 14:19:52 2023 ; 3 h 37 min 24 s 156.83 ms remaining ; 4 h 38 min 43 s 277.93 ms total) Sun Oct 22 10:48:13 2023: Iterated ≈ 24% of D-proof candidates. [ 70407861 of approximately 293366090] (ETC: Sun Oct 22 14:20:37 2023 ; 3 h 32 min 23 s 878.33 ms remaining ; 4 h 39 min 28 s 260.91 ms total) Sun Oct 22 10:54:05 2023: Iterated ≈ 26% of D-proof candidates. [ 76275183 of approximately 293366090] (ETC: Sun Oct 22 14:21:43 2023 ; 3 h 27 min 37 s 539.80 ms remaining ; 4 h 40 min 34 s 513.21 ms total) Sun Oct 22 11:00:24 2023: Iterated ≈ 28% of D-proof candidates. [ 82142505 of approximately 293366090] (ETC: Sun Oct 22 14:24:15 2023 ; 3 h 23 min 50 s 333.41 ms remaining ; 4 h 43 min 6 s 574.17 ms total) Sun Oct 22 11:06:28 2023: Iterated ≈ 30% of D-proof candidates. [ 88009827 of approximately 293366090] (ETC: Sun Oct 22 14:25:36 2023 ; 3 h 19 min 7 s 159.10 ms remaining ; 4 h 44 min 27 s 370.15 ms total) Sun Oct 22 11:12:14 2023: Iterated ≈ 32% of D-proof candidates. [ 93877148 of approximately 293366090] (ETC: Sun Oct 22 14:25:48 2023 ; 3 h 13 min 33 s 933.82 ms remaining ; 4 h 44 min 39 s 314.37 ms total) Sun Oct 22 11:18:24 2023: Iterated ≈ 34% of D-proof candidates. [ 99744470 of approximately 293366090] (ETC: Sun Oct 22 14:27:12 2023 ; 3 h 8 min 47 s 864.04 ms remaining ; 4 h 46 min 3 s 430.32 ms total) Sun Oct 22 11:24:10 2023: Iterated ≈ 36% of D-proof candidates. [105611792 of approximately 293366090] (ETC: Sun Oct 22 14:27:20 2023 ; 3 h 3 min 10 s 40.11 ms remaining ; 4 h 46 min 11 s 937.63 ms total) Sun Oct 22 11:30:04 2023: Iterated ≈ 38% of D-proof candidates. [111479114 of approximately 293366090] (ETC: Sun Oct 22 14:27:48 2023 ; 2 h 57 min 43 s 562.95 ms remaining ; 4 h 46 min 39 s 295.05 ms total) Sun Oct 22 11:35:41 2023: Iterated ≈ 40% of D-proof candidates. [117346436 of approximately 293366090] (ETC: Sun Oct 22 14:27:30 2023 ; 2 h 51 min 49 s 93.51 ms remaining ; 4 h 46 min 21 s 822.52 ms total) Sun Oct 22 11:41:24 2023: Iterated ≈ 42% of D-proof candidates. [123213757 of approximately 293366090] (ETC: Sun Oct 22 14:27:29 2023 ; 2 h 46 min 5 s 80.69 ms remaining ; 4 h 46 min 21 s 173.52 ms total) Sun Oct 22 11:46:54 2023: Iterated ≈ 44% of D-proof candidates. [129081079 of approximately 293366090] (ETC: Sun Oct 22 14:26:58 2023 ; 2 h 40 min 3 s 760.20 ms remaining ; 4 h 45 min 49 s 571.72 ms total) Sun Oct 22 11:52:12 2023: Iterated ≈ 46% of D-proof candidates. [134948401 of approximately 293366090] (ETC: Sun Oct 22 14:26:04 2023 ; 2 h 33 min 51 s 881.94 ms remaining ; 4 h 44 min 56 s 77.61 ms total) Sun Oct 22 11:57:34 2023: Iterated ≈ 48% of D-proof candidates. [140815723 of approximately 293366090] (ETC: Sun Oct 22 14:25:21 2023 ; 2 h 27 min 47 s 648.08 ms remaining ; 4 h 44 min 13 s 169.37 ms total) Sun Oct 22 12:02:45 2023: Iterated ≈ 50% of D-proof candidates. [146683045 of approximately 293366090] (ETC: Sun Oct 22 14:24:22 2023 ; 2 h 21 min 36 s 900.03 ms remaining ; 4 h 43 min 13 s 800.06 ms total) Sun Oct 22 12:07:53 2023: Iterated ≈ 52% of D-proof candidates. [152550366 of approximately 293366090] (ETC: Sun Oct 22 14:23:20 2023 ; 2 h 15 min 27 s 214.20 ms remaining ; 4 h 42 min 11 s 696.16 ms total) Sun Oct 22 12:12:56 2023: Iterated ≈ 54% of D-proof candidates. [158417688 of approximately 293366090] (ETC: Sun Oct 22 14:22:15 2023 ; 2 h 9 min 18 s 559.24 ms remaining ; 4 h 41 min 6 s 433.05 ms total) Sun Oct 22 12:17:54 2023: Iterated ≈ 56% of D-proof candidates. [164285010 of approximately 293366090] (ETC: Sun Oct 22 14:21:05 2023 ; 2 h 3 min 10 s 428.63 ms remaining ; 4 h 39 min 56 s 428.66 ms total) Sun Oct 22 12:22:48 2023: Iterated ≈ 58% of D-proof candidates. [170152332 of approximately 293366090] (ETC: Sun Oct 22 14:19:51 2023 ; 1 h 57 min 3 s 612.24 ms remaining ; 4 h 38 min 42 s 886.25 ms total) Sun Oct 22 12:27:38 2023: Iterated ≈ 60% of D-proof candidates. [176019654 of approximately 293366090] (ETC: Sun Oct 22 14:18:37 2023 ; 1 h 50 min 59 s 546.27 ms remaining ; 4 h 37 min 28 s 865.68 ms total) Sun Oct 22 12:32:24 2023: Iterated ≈ 62% of D-proof candidates. [181886975 of approximately 293366090] (ETC: Sun Oct 22 14:17:22 2023 ; 1 h 44 min 58 s 79.25 ms remaining ; 4 h 36 min 13 s 892.66 ms total) Sun Oct 22 12:37:08 2023: Iterated ≈ 64% of D-proof candidates. [187754297 of approximately 293366090] (ETC: Sun Oct 22 14:16:07 2023 ; 1 h 38 min 59 s 629.26 ms remaining ; 4 h 34 min 58 s 970.07 ms total) Sun Oct 22 12:41:49 2023: Iterated ≈ 66% of D-proof candidates. [193621619 of approximately 293366090] (ETC: Sun Oct 22 14:14:54 2023 ; 1 h 33 min 4 s 685.54 ms remaining ; 4 h 33 min 45 s 545.63 ms total) Sun Oct 22 12:46:28 2023: Iterated ≈ 68% of D-proof candidates. [199488941 of approximately 293366090] (ETC: Sun Oct 22 14:13:40 2023 ; 1 h 27 min 12 s 608.27 ms remaining ; 4 h 32 min 31 s 900.80 ms total) Sun Oct 22 12:51:03 2023: Iterated ≈ 70% of D-proof candidates. [205356263 of approximately 293366090] (ETC: Sun Oct 22 14:12:27 2023 ; 1 h 21 min 23 s 522.90 ms remaining ; 4 h 31 min 18 s 409.68 ms total) Sun Oct 22 12:55:43 2023: Iterated ≈ 72% of D-proof candidates. [211223584 of approximately 293366090] (ETC: Sun Oct 22 14:11:24 2023 ; 1 h 15 min 40 s 353.69 ms remaining ; 4 h 30 min 15 s 548.75 ms total) Sun Oct 22 13:00:15 2023: Iterated ≈ 74% of D-proof candidates. [217090906 of approximately 293366090] (ETC: Sun Oct 22 14:10:12 2023 ; 1 h 9 min 57 s 332.70 ms remaining ; 4 h 29 min 3 s 587.17 ms total) Sun Oct 22 13:04:40 2023: Iterated ≈ 76% of D-proof candidates. [222958228 of approximately 293366090] (ETC: Sun Oct 22 14:08:56 2023 ; 1 h 4 min 16 s 322.89 ms remaining ; 4 h 27 min 48 s 11.97 ms total) Sun Oct 22 13:09:05 2023: Iterated ≈ 78% of D-proof candidates. [228825550 of approximately 293366090] (ETC: Sun Oct 22 14:07:44 2023 ; 58 min 39 s 2.58 ms remaining ; 4 h 26 min 35 s 466.24 ms total) Sun Oct 22 13:13:28 2023: Iterated ≈ 80% of D-proof candidates. [234692872 of approximately 293366090] (ETC: Sun Oct 22 14:06:32 2023 ; 53 min 4 s 820.13 ms remaining ; 4 h 25 min 24 s 100.67 ms total) Sun Oct 22 13:17:49 2023: Iterated ≈ 82% of D-proof candidates. [240560193 of approximately 293366090] (ETC: Sun Oct 22 14:05:23 2023 ; 47 min 33 s 848.12 ms remaining ; 4 h 24 min 14 s 711.52 ms total) Sun Oct 22 13:22:07 2023: Iterated ≈ 84% of D-proof candidates. [246427515 of approximately 293366090] (ETC: Sun Oct 22 14:04:12 2023 ; 42 min 5 s 424.07 ms remaining ; 4 h 23 min 3 s 900.24 ms total) Sun Oct 22 13:26:25 2023: Iterated ≈ 86% of D-proof candidates. [252294837 of approximately 293366090] (ETC: Sun Oct 22 14:03:06 2023 ; 36 min 40 s 454.19 ms remaining ; 4 h 21 min 57 s 529.75 ms total) Sun Oct 22 13:30:42 2023: Iterated ≈ 88% of D-proof candidates. [258162159 of approximately 293366090] (ETC: Sun Oct 22 14:02:01 2023 ; 31 min 18 s 286.84 ms remaining ; 4 h 20 min 52 s 390.28 ms total) Sun Oct 22 13:35:00 2023: Iterated ≈ 90% of D-proof candidates. [264029481 of approximately 293366090] (ETC: Sun Oct 22 14:00:59 2023 ; 25 min 59 s 64.10 ms remaining ; 4 h 19 min 50 s 641.02 ms total) Sun Oct 22 13:39:16 2023: Iterated ≈ 92% of D-proof candidates. [269896802 of approximately 293366090] (ETC: Sun Oct 22 13:59:58 2023 ; 20 min 42 s 391.59 ms remaining ; 4 h 18 min 49 s 894.39 ms total) Sun Oct 22 13:43:33 2023: Iterated ≈ 94% of D-proof candidates. [275764124 of approximately 293366090] (ETC: Sun Oct 22 13:59:01 2023 ; 15 min 28 s 371.75 ms remaining ; 4 h 17 min 52 s 861.91 ms total) Sun Oct 22 13:47:47 2023: Iterated ≈ 96% of D-proof candidates. [281631446 of approximately 293366090] (ETC: Sun Oct 22 13:58:04 2023 ; 10 min 16 s 618.66 ms remaining ; 4 h 16 min 55 s 465.97 ms total) Sun Oct 22 13:52:01 2023: Iterated ≈ 98% of D-proof candidates. [287498768 of approximately 293366090] (ETC: Sun Oct 22 13:57:08 2023 ; 5 min 7 s 194.85 ms remaining ; 4 h 15 min 59 s 741.95 ms total) Sun Oct 22 13:56:14 2023: Iterated ≈100% of D-proof candidates. [293366090 of approximately 293366090] (ETC: Sun Oct 22 13:56:14 2023 ; 0.00 ms remaining ; 4 h 15 min 5 s 535.51 ms total) 16660835.30 ms (4 h 37 min 40 s 835.30 ms) taken to collect 28040847 D-proofs of length 155. [iterated 324945288 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 } } 197590.68 ms (3 min 17 s 590.68 ms) taken to filter and order new representative proofs. Found 28040847 representative, 44272186 redundant, and 252632255 invalid condensed detachment proof strings. lengths up to 155 ; 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)} ; 28040847 new representative proofs (44272186 redundant, 252632255 invalid) Sun Oct 22 14:22:27 2023: Starting to write 28040847 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. 91515.42 ms (1 min 31 s 515.42 ms) taken to print and save 18088589265 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. Sun Oct 22 14:24:39 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 155, unfiltered] Sun Oct 22 14:27:15 2023: Process terminated. [pid: 73513, tid:23253839562624]