( 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: 12.8925 h CPU utilization: 825.12 core-h ) Wed Nov 1 18:29:51 2023: Process started. [pid: 52765, tid:23443697252224] Tasks: 1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true) 2. generateDProofRepresentativeFiles(151, false, true) [Main] Calling resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c] (1) CC0CCN0.1.2C3CCN4C2.4C0.4 - CCpCCNpqrCsCCNtCrtCpt - (0\imply((\not0\imply1)\imply2))\imply(3\imply((\not4\imply(2\imply4))\imply(0\imply4))) [Main] Calling generateDProofRepresentativeFiles(151, false, true). Wed Nov 1 18:29:51 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 151, unfiltered] 0.03 ms taken to load initial representatives. 0.76 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23443637004032] 0.00 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23443628599040] 0.90 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23443630700288] 1.68 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23443271575296] 3.45 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23443634902784] 9973.56 ms (9 s 973.56 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23443637004032] 11334.99 ms (11 s 334.99 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23443634902784] 5.64 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23443632801536] 10251.42 ms (10 s 251.42 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23443630700288] 10371.89 ms (10 s 371.88 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23443628599040] 2.26 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23443626497792] 7.71 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23443624396544] 4.05 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23443622295296] 6.86 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23443620194048] 5.26 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23443618092800] 3.94 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23443615991552] 6.07 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23443613890304] 4.89 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23443611789056] 3.49 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23443273676544] 11204.46 ms (11 s 204.46 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23443271575296] 4.38 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23443269474048] 8.24 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23443267372800] 3.89 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23443265271552] 5.52 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23443263170304] 4.28 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23443261069056] 7.28 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23443258967808] 22.08 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23443256866560] 9.79 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23443254765312] 13.61 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23443252664064] 10.95 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23443250562816] 9.18 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23443248461568] 26.26 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23443246360320] 18.18 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23443244259072] 21.84 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23443242157824] 30.73 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23443240056576] 16.02 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23443237955328] 27.60 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23443235854080] 51.50 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23443233752832] 30.50 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23443231651584] 17.62 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23443229550336] 31.23 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23443227449088] 34.37 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23443225347840] 36.96 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23443223246592] 54.79 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23443221145344] 41.87 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23443219044096] 651.91 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23443216942848] 47.29 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23443214841600] 751.77 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23443212740352] 735.58 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23443210639104] 335.30 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23440857757440] 75.17 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23440855656192] 381.97 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23440853554944] 114.84 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23440851453696] 801.32 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23440849352448] 1250.75 ms (1 s 250.75 ms) taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23440847251200] 1344.54 ms (1 s 344.54 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23440845149952] 1694.32 ms (1 s 694.32 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23440843048704] 4497.71 ms (4 s 497.71 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23440840947456] 1430.41 ms (1 s 430.41 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23440838846208] 5801.08 ms (5 s 801.08 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23440836744960] 9017.83 ms (9 s 17.83 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23440834643712] 1749.67 ms (1 s 749.67 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23440832542464] 1859.79 ms (1 s 859.79 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23440830441216] 4042.73 ms (4 s 42.73 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23440828339968] 2319.03 ms (2 s 319.03 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23440826238720] 6942.17 ms (6 s 942.17 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23440824137472] 6487.04 ms (6 s 487.04 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23440822036224] 7311.98 ms (7 s 311.98 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23440819934976] 9685.01 ms (9 s 685.00 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23440817833728] 11493.59 ms (11 s 493.59 ms) total read duration. Loaded 70 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 2 9 : 1 11 : 0 13 : 1 15 : 2 17 : 3 19 : 4 21 : 5 23 : 5 25 : 5 27 : 6 29 : 7 31 : 15 33 : 20 35 : 25 37 : 30 39 : 37 41 : 42 43 : 51 45 : 63 47 : 85 49 : 122 51 : 162 53 : 206 55 : 251 57 : 292 59 : 339 61 : 444 63 : 598 65 : 781 67 : 1016 69 : 1303 71 : 1593 73 : 1922 75 : 2359 77 : 2986 79 : 3875 81 : 5006 83 : 6466 85 : 8184 87 : 10182 89 : 12488 91 : 15534 93 : 19614 95 : 25087 97 : 32452 99 : 41840 101 : 53343 103 : 67105 105 : 84222 107 : 105925 109 : 134564 111 : 172053 113 : 221055 115 : 283569 117 : 361751 119 : 458509 121 : 579502 123 : 734352 125 : 935212 127 : 1197027 129 : 1534565 131 : 1965596 133 : 2509883 135 : 3196594 137 : 4066027 139 : 5180139 24036508 representatives in total. 31942.42 ms (31 s 942.42 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23440817833728] 44384.10 ms (44 s 384.10 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23440819934976] 55715.92 ms (55 s 715.91 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23440822036224] 63045.70 ms (1 min 3 s 45.70 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:23440824137472] 68287.96 ms (1 min 8 s 287.97 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:23440826238720] 68297.43 ms (1 min 8 s 297.44 ms) additional read duration. Loaded 5 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 214457016 representatives in total. Wed Nov 1 18:31:26 2023: Inserted ≈ 5% of D-proof conclusions. [ 10722850 of 214457016] (ETC: Wed Nov 1 18:36:09 2023 ; 4 min 42 s 814.28 ms remaining ; 4 min 57 s 699.24 ms total) Wed Nov 1 18:31:40 2023: Inserted ≈10% of D-proof conclusions. [ 21445701 of 214457016] (ETC: Wed Nov 1 18:35:56 2023 ; 4 min 16 s 547.11 ms remaining ; 4 min 45 s 52.35 ms total) Wed Nov 1 18:31:52 2023: Inserted ≈15% of D-proof conclusions. [ 32168552 of 214457016] (ETC: Wed Nov 1 18:35:44 2023 ; 3 min 52 s 35.57 ms remaining ; 4 min 32 s 983.02 ms total) Wed Nov 1 18:32:07 2023: Inserted ≈20% of D-proof conclusions. [ 42891403 of 214457016] (ETC: Wed Nov 1 18:35:48 2023 ; 3 min 41 s 525.07 ms remaining ; 4 min 36 s 906.34 ms total) Wed Nov 1 18:32:21 2023: Inserted ≈25% of D-proof conclusions. [ 53614254 of 214457016] (ETC: Wed Nov 1 18:35:48 2023 ; 3 min 27 s 920.19 ms remaining ; 4 min 37 s 226.92 ms total) Wed Nov 1 18:32:35 2023: Inserted ≈30% of D-proof conclusions. [ 64337104 of 214457016] (ETC: Wed Nov 1 18:35:51 2023 ; 3 min 16 s 138.28 ms remaining ; 4 min 40 s 197.55 ms total) Wed Nov 1 18:32:52 2023: Inserted ≈35% of D-proof conclusions. [ 75059955 of 214457016] (ETC: Wed Nov 1 18:35:58 2023 ; 3 min 6 s 352.83 ms remaining ; 4 min 46 s 696.67 ms total) Wed Nov 1 18:33:08 2023: Inserted ≈40% of D-proof conclusions. [ 85782806 of 214457016] (ETC: Wed Nov 1 18:36:04 2023 ; 2 min 55 s 795.37 ms remaining ; 4 min 52 s 992.28 ms total) Wed Nov 1 18:33:25 2023: Inserted ≈45% of D-proof conclusions. [ 96505657 of 214457016] (ETC: Wed Nov 1 18:36:09 2023 ; 2 min 43 s 558.25 ms remaining ; 4 min 57 s 378.64 ms total) Wed Nov 1 18:33:42 2023: Inserted ≈50% of D-proof conclusions. [107228508 of 214457016] (ETC: Wed Nov 1 18:36:12 2023 ; 2 min 30 s 578.46 ms remaining ; 5 min 1 s 156.92 ms total) Wed Nov 1 18:33:59 2023: Inserted ≈55% of D-proof conclusions. [117951358 of 214457016] (ETC: Wed Nov 1 18:36:16 2023 ; 2 min 17 s 181.52 ms remaining ; 5 min 4 s 847.82 ms total) Wed Nov 1 18:34:17 2023: Inserted ≈60% of D-proof conclusions. [128674209 of 214457016] (ETC: Wed Nov 1 18:36:21 2023 ; 2 min 3 s 771.82 ms remaining ; 5 min 9 s 429.55 ms total) Wed Nov 1 18:34:36 2023: Inserted ≈65% of D-proof conclusions. [139397060 of 214457016] (ETC: Wed Nov 1 18:36:26 2023 ; 1 min 50 s 340.88 ms remaining ; 5 min 15 s 259.66 ms total) Wed Nov 1 18:34:54 2023: Inserted ≈70% of D-proof conclusions. [150119911 of 214457016] (ETC: Wed Nov 1 18:36:29 2023 ; 1 min 35 s 353.69 ms remaining ; 5 min 17 s 845.65 ms total) Wed Nov 1 18:35:09 2023: Inserted ≈75% of D-proof conclusions. [160842762 of 214457016] (ETC: Wed Nov 1 18:36:28 2023 ; 1 min 19 s 133.39 ms remaining ; 5 min 16 s 533.57 ms total) Wed Nov 1 18:35:22 2023: Inserted ≈80% of D-proof conclusions. [171565612 of 214457016] (ETC: Wed Nov 1 18:36:25 2023 ; 1 min 2 s 678.95 ms remaining ; 5 min 13 s 394.73 ms total) Wed Nov 1 18:35:35 2023: Inserted ≈85% of D-proof conclusions. [182288463 of 214457016] (ETC: Wed Nov 1 18:36:22 2023 ; 46 s 558.08 ms remaining ; 5 min 10 s 387.17 ms total) Wed Nov 1 18:35:48 2023: Inserted ≈90% of D-proof conclusions. [193011314 of 214457016] (ETC: Wed Nov 1 18:36:19 2023 ; 30 s 762.78 ms remaining ; 5 min 7 s 627.82 ms total) Wed Nov 1 18:36:05 2023: Inserted ≈95% of D-proof conclusions. [203734165 of 214457016] (ETC: Wed Nov 1 18:36:20 2023 ; 15 s 437.78 ms remaining ; 5 min 8 s 755.66 ms total) Wed Nov 1 18:36:24 2023: Inserted 100% of D-proof conclusions. [214457016 of 214457016] (ETC: Wed Nov 1 18:36:24 2023 ; 0.00 ms remaining ; 5 min 13 s 272.18 ms total) 313275.86 ms (5 min 13 s 275.86 ms) total insertion duration. Known iteration count loaded from 151:891383185. Wed Nov 1 18:36:24 2023: Starting to generate D-proof representatives of length 151. Wed Nov 1 18:51:52 2023: Iterated ≈ 2% of D-proof candidates. [ 17827663 of 891383185] (ETC: Thu Nov 2 07:29:38 2023 ; 12 h 37 min 45 s 784.70 ms remaining ; 12 h 53 min 13 s 657.82 ms total) Wed Nov 1 19:07:00 2023: Iterated ≈ 4% of D-proof candidates. [ 35655327 of 891383185] (ETC: Thu Nov 2 07:21:16 2023 ; 12 h 14 min 16 s 277.46 ms remaining ; 12 h 44 min 51 s 955.66 ms total) Wed Nov 1 19:20:44 2023: Iterated ≈ 6% of D-proof candidates. [ 53482991 of 891383185] (ETC: Thu Nov 2 06:55:05 2023 ; 11 h 34 min 21 s 444.28 ms remaining ; 12 h 18 min 40 s 685.40 ms total) Wed Nov 1 19:36:27 2023: Iterated ≈ 8% of D-proof candidates. [ 71310654 of 891383185] (ETC: Thu Nov 2 07:07:00 2023 ; 11 h 30 min 32 s 525.93 ms remaining ; 12 h 30 min 35 s 354.23 ms total) Wed Nov 1 19:53:31 2023: Iterated ≈10% of D-proof candidates. [ 89138318 of 891383185] (ETC: Thu Nov 2 07:27:28 2023 ; 11 h 33 min 57 s 433.44 ms remaining ; 12 h 51 min 3 s 814.91 ms total) Wed Nov 1 20:07:48 2023: Iterated ≈12% of D-proof candidates. [106965982 of 891383185] (ETC: Thu Nov 2 07:18:00 2023 ; 11 h 10 min 12 s 369.14 ms remaining ; 12 h 41 min 35 s 874.01 ms total) Wed Nov 1 20:21:41 2023: Iterated ≈14% of D-proof candidates. [124793645 of 891383185] (ETC: Thu Nov 2 07:08:25 2023 ; 10 h 46 min 43 s 877.68 ms remaining ; 12 h 32 min 787.95 ms total) Wed Nov 1 20:40:16 2023: Iterated ≈16% of D-proof candidates. [142621309 of 891383185] (ETC: Thu Nov 2 07:30:31 2023 ; 10 h 50 min 15 s 104.56 ms remaining ; 12 h 54 min 6 s 553.01 ms total) Wed Nov 1 20:55:33 2023: Iterated ≈18% of D-proof candidates. [160448973 of 891383185] (ETC: Thu Nov 2 07:29:24 2023 ; 10 h 33 min 50 s 820.85 ms remaining ; 12 h 52 min 59 s 49.79 ms total) Wed Nov 1 21:11:13 2023: Iterated ≈20% of D-proof candidates. [178276637 of 891383185] (ETC: Thu Nov 2 07:30:28 2023 ; 10 h 19 min 14 s 574.09 ms remaining ; 12 h 54 min 3 s 217.62 ms total) Wed Nov 1 21:28:15 2023: Iterated ≈22% of D-proof candidates. [196104300 of 891383185] (ETC: Thu Nov 2 07:37:29 2023 ; 10 h 9 min 14 s 569.57 ms remaining ; 13 h 1 min 4 s 832.74 ms total) Wed Nov 1 21:42:22 2023: Iterated ≈24% of D-proof candidates. [213931964 of 891383185] (ETC: Thu Nov 2 07:31:13 2023 ; 9 h 48 min 50 s 992.33 ms remaining ; 12 h 54 min 48 s 147.77 ms total) Wed Nov 1 21:59:08 2023: Iterated ≈26% of D-proof candidates. [231759628 of 891383185] (ETC: Thu Nov 2 07:36:08 2023 ; 9 h 37 min 114.22 ms remaining ; 12 h 59 min 43 s 938.13 ms total) Wed Nov 1 22:14:35 2023: Iterated ≈28% of D-proof candidates. [249587291 of 891383185] (ETC: Thu Nov 2 07:35:35 2023 ; 9 h 21 min 85.27 ms remaining ; 12 h 59 min 10 s 118.37 ms total) Wed Nov 1 22:31:00 2023: Iterated ≈30% of D-proof candidates. [267414955 of 891383185] (ETC: Thu Nov 2 07:38:23 2023 ; 9 h 7 min 23 s 149.38 ms remaining ; 13 h 1 min 58 s 784.79 ms total) Wed Nov 1 22:46:20 2023: Iterated ≈32% of D-proof candidates. [285242619 of 891383185] (ETC: Thu Nov 2 07:37:25 2023 ; 8 h 51 min 5 s 27.59 ms remaining ; 13 h 1 min 334.67 ms total) Wed Nov 1 23:02:42 2023: Iterated ≈34% of D-proof candidates. [303070282 of 891383185] (ETC: Thu Nov 2 07:39:38 2023 ; 8 h 36 min 55 s 870.81 ms remaining ; 13 h 3 min 13 s 743.57 ms total) Wed Nov 1 23:20:10 2023: Iterated ≈36% of D-proof candidates. [320897946 of 891383185] (ETC: Thu Nov 2 07:44:36 2023 ; 8 h 24 min 26 s 687.88 ms remaining ; 13 h 8 min 11 s 699.77 ms total) Wed Nov 1 23:35:50 2023: Iterated ≈38% of D-proof candidates. [338725610 of 891383185] (ETC: Thu Nov 2 07:44:21 2023 ; 8 h 8 min 31 s 445.41 ms remaining ; 13 h 7 min 56 s 524.84 ms total) Wed Nov 1 23:49:34 2023: Iterated ≈40% of D-proof candidates. [356553274 of 891383185] (ETC: Thu Nov 2 07:39:18 2023 ; 7 h 49 min 44 s 6.00 ms remaining ; 13 h 2 min 53 s 343.34 ms total) Thu Nov 2 00:04:48 2023: Iterated ≈42% of D-proof candidates. [374380937 of 891383185] (ETC: Thu Nov 2 07:38:17 2023 ; 7 h 33 min 29 s 231.75 ms remaining ; 13 h 1 min 52 s 468.48 ms total) Thu Nov 2 00:19:54 2023: Iterated ≈44% of D-proof candidates. [392208601 of 891383185] (ETC: Thu Nov 2 07:37:05 2023 ; 7 h 17 min 10 s 613.46 ms remaining ; 13 h 40 s 381.15 ms total) Thu Nov 2 00:35:52 2023: Iterated ≈46% of D-proof candidates. [410036265 of 891383185] (ETC: Thu Nov 2 07:37:50 2023 ; 7 h 1 min 57 s 962.70 ms remaining ; 13 h 1 min 25 s 116.09 ms total) Thu Nov 2 00:51:28 2023: Iterated ≈48% of D-proof candidates. [427863928 of 891383185] (ETC: Thu Nov 2 07:37:47 2023 ; 6 h 46 min 18 s 998.46 ms remaining ; 13 h 1 min 22 s 689.26 ms total) Thu Nov 2 01:07:51 2023: Iterated ≈50% of D-proof candidates. [445691592 of 891383185] (ETC: Thu Nov 2 07:39:17 2023 ; 6 h 31 min 26 s 141.56 ms remaining ; 13 h 2 min 52 s 283.06 ms total) Thu Nov 2 01:21:54 2023: Iterated ≈52% of D-proof candidates. [463519256 of 891383185] (ETC: Thu Nov 2 07:36:11 2023 ; 6 h 14 min 17 s 640.24 ms remaining ; 12 h 59 min 46 s 750.48 ms total) Thu Nov 2 01:36:19 2023: Iterated ≈54% of D-proof candidates. [481346919 of 891383185] (ETC: Thu Nov 2 07:34:00 2023 ; 5 h 57 min 41 s 660.79 ms remaining ; 12 h 57 min 35 s 784.24 ms total) Thu Nov 2 01:50:48 2023: Iterated ≈56% of D-proof candidates. [499174583 of 891383185] (ETC: Thu Nov 2 07:32:07 2023 ; 5 h 41 min 18 s 511.86 ms remaining ; 12 h 55 min 42 s 72.33 ms total) Thu Nov 2 02:04:59 2023: Iterated ≈58% of D-proof candidates. [517002247 of 891383185] (ETC: Thu Nov 2 07:29:49 2023 ; 5 h 24 min 49 s 832.02 ms remaining ; 12 h 53 min 24 s 361.92 ms total) Thu Nov 2 02:20:01 2023: Iterated ≈60% of D-proof candidates. [534829911 of 891383185] (ETC: Thu Nov 2 07:29:05 2023 ; 5 h 9 min 4 s 188.72 ms remaining ; 12 h 52 min 40 s 471.79 ms total) Thu Nov 2 02:35:15 2023: Iterated ≈62% of D-proof candidates. [552657574 of 891383185] (ETC: Thu Nov 2 07:28:43 2023 ; 4 h 53 min 28 s 730.27 ms remaining ; 12 h 52 min 18 s 763.78 ms total) Thu Nov 2 02:50:21 2023: Iterated ≈64% of D-proof candidates. [570485238 of 891383185] (ETC: Thu Nov 2 07:28:11 2023 ; 4 h 37 min 50 s 363.40 ms remaining ; 12 h 51 min 46 s 564.96 ms total) Thu Nov 2 03:05:15 2023: Iterated ≈66% of D-proof candidates. [588312902 of 891383185] (ETC: Thu Nov 2 07:27:22 2023 ; 4 h 22 min 7 s 636.16 ms remaining ; 12 h 50 min 57 s 753.39 ms total) Thu Nov 2 03:20:18 2023: Iterated ≈68% of D-proof candidates. [606140565 of 891383185] (ETC: Thu Nov 2 07:26:51 2023 ; 4 h 6 min 32 s 344.26 ms remaining ; 12 h 50 min 26 s 75.68 ms total) Thu Nov 2 03:34:57 2023: Iterated ≈70% of D-proof candidates. [623968229 of 891383185] (ETC: Thu Nov 2 07:25:45 2023 ; 3 h 50 min 48 s 298.06 ms remaining ; 12 h 49 min 20 s 993.44 ms total) Thu Nov 2 03:49:11 2023: Iterated ≈72% of D-proof candidates. [641795893 of 891383185] (ETC: Thu Nov 2 07:24:09 2023 ; 3 h 34 min 58 s 142.22 ms remaining ; 12 h 47 min 44 s 793.60 ms total) Thu Nov 2 04:03:27 2023: Iterated ≈74% of D-proof candidates. [659623556 of 891383185] (ETC: Thu Nov 2 07:22:41 2023 ; 3 h 19 min 13 s 933.51 ms remaining ; 12 h 46 min 16 s 667.15 ms total) Thu Nov 2 04:17:41 2023: Iterated ≈76% of D-proof candidates. [677451220 of 891383185] (ETC: Thu Nov 2 07:21:14 2023 ; 3 h 3 min 33 s 556.37 ms remaining ; 12 h 44 min 49 s 818.09 ms total) Thu Nov 2 04:31:59 2023: Iterated ≈78% of D-proof candidates. [695278884 of 891383185] (ETC: Thu Nov 2 07:19:58 2023 ; 2 h 47 min 58 s 965.31 ms remaining ; 12 h 43 min 33 s 478.62 ms total) Thu Nov 2 04:46:06 2023: Iterated ≈80% of D-proof candidates. [713106548 of 891383185] (ETC: Thu Nov 2 07:18:31 2023 ; 2 h 32 min 25 s 383.98 ms remaining ; 12 h 42 min 6 s 919.92 ms total) Thu Nov 2 04:59:56 2023: Iterated ≈82% of D-proof candidates. [730934211 of 891383185] (ETC: Thu Nov 2 07:16:48 2023 ; 2 h 16 min 52 s 188.20 ms remaining ; 12 h 40 min 23 s 267.58 ms total) Thu Nov 2 05:13:26 2023: Iterated ≈84% of D-proof candidates. [748761875 of 891383185] (ETC: Thu Nov 2 07:14:46 2023 ; 2 h 1 min 20 s 206.66 ms remaining ; 12 h 38 min 21 s 291.52 ms total) Thu Nov 2 05:26:59 2023: Iterated ≈86% of D-proof candidates. [766589539 of 891383185] (ETC: Thu Nov 2 07:12:53 2023 ; 1 h 45 min 54 s 395.41 ms remaining ; 12 h 36 min 28 s 538.62 ms total) Thu Nov 2 05:40:41 2023: Iterated ≈88% of D-proof candidates. [784417202 of 891383185] (ETC: Thu Nov 2 07:11:16 2023 ; 1 h 30 min 34 s 975.35 ms remaining ; 12 h 34 min 51 s 460.88 ms total) Thu Nov 2 05:54:22 2023: Iterated ≈90% of D-proof candidates. [802244866 of 891383185] (ETC: Thu Nov 2 07:09:42 2023 ; 1 h 15 min 19 s 709.18 ms remaining ; 12 h 33 min 17 s 91.50 ms total) Thu Nov 2 06:07:54 2023: Iterated ≈92% of D-proof candidates. [820072530 of 891383185] (ETC: Thu Nov 2 07:08:02 2023 ; 1 h 7 s 774.98 ms remaining ; 12 h 31 min 37 s 187.10 ms total) Thu Nov 2 06:21:16 2023: Iterated ≈94% of D-proof candidates. [837900193 of 891383185] (ETC: Thu Nov 2 07:06:16 2023 ; 44 min 59 s 489.09 ms remaining ; 12 h 29 min 51 s 484.13 ms total) Thu Nov 2 06:34:39 2023: Iterated ≈96% of D-proof candidates. [855727857 of 891383185] (ETC: Thu Nov 2 07:04:35 2023 ; 29 min 55 s 619.59 ms remaining ; 12 h 28 min 10 s 489.11 ms total) Thu Nov 2 06:48:08 2023: Iterated ≈98% of D-proof candidates. [873555521 of 891383185] (ETC: Thu Nov 2 07:03:04 2023 ; 14 min 55 s 993.74 ms remaining ; 12 h 26 min 39 s 686.39 ms total) Thu Nov 2 07:01:51 2023: Iterated 100% of D-proof candidates. [891383185 of 891383185] (ETC: Thu Nov 2 07:01:51 2023 ; 0.00 ms remaining ; 12 h 25 min 26 s 858.11 ms total) 44727919.76 ms (12 h 25 min 27 s 919.76 ms) taken to collect 82234537 D-proofs of length 151. [iterated 891383185 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 8 }, { 11, 10 }, { 13, 10 }, { 15, 10 }, { 17, 10 }, { 19, 15 }, { 21, 26 }, { 23, 40 }, { 25, 52 }, { 27, 63 }, { 29, 74 }, { 31, 86 }, { 33, 118 }, { 35, 167 }, { 37, 244 }, { 39, 340 }, { 41, 446 }, { 43, 551 }, { 45, 688 }, { 47, 869 }, { 49, 1128 }, { 51, 1509 }, { 53, 2046 }, { 55, 2758 }, { 57, 3636 }, { 59, 4659 }, { 61, 5848 }, { 63, 7415 }, { 65, 9546 }, { 67, 12520 }, { 69, 16626 }, { 71, 21997 }, { 73, 28576 }, { 75, 36634 }, { 77, 46614 }, { 79, 59337 }, { 81, 76266 }, { 83, 99080 }, { 85, 129482 }, { 87, 168717 }, { 89, 218196 }, { 91, 279663 }, { 93, 357074 }, { 95, 456119 }, { 97, 585294 }, { 99, 755798 }, { 101, 979916 }, { 103, 1269838 }, { 105, 1639296 }, { 107, 2106748 }, { 109, 2698758 }, { 111, 3457865 }, { 113, 4441498 }, { 115, 5724404 }, { 117, 7393098 }, { 119, 9547567 }, { 121, 12303220 }, { 123, 15814238 }, { 125, 20294070 }, { 127, 26041382 }, { 129, 33464926 }, { 131, 43088171 }, { 133, 55549258 }, { 135, 71608010 }, { 137, 92211954 }, { 139, 118581507 }, { 141, 152368710 }, { 143, 216457445 }, { 145, 308369644 }, { 147, 453382622 }, { 149, 650543112 }, { 151, 891383185 } } 620531.30 ms (10 min 20 s 531.30 ms) taken to filter and order new representative proofs. Found 82234537 representative, 356642399 redundant, and 452506249 invalid condensed detachment proof strings. lengths up to 151 ; amounts per length: {(1,1), (3,1), (5,2), (7,2), (9,1), (13,1), (15,2), (17,3), (19,4), (21,5), (23,5), (25,5), (27,6), (29,7), (31,15), (33,20), (35,25), (37,30), (39,37), (41,42), (43,51), (45,63), (47,85), (49,122), (51,162), (53,206), (55,251), (57,292), (59,339), (61,444), (63,598), (65,781), (67,1016), (69,1303), (71,1593), (73,1922), (75,2359), (77,2986), (79,3875), (81,5006), (83,6466), (85,8184), (87,10182), (89,12488), (91,15534), (93,19614), (95,25087), (97,32452), (99,41840), (101,53343), (103,67105), (105,84222), (107,105925), (109,134564), (111,172053), (113,221055), (115,283569), (117,361751), (119,458509), (121,579502), (123,734352), (125,935212), (127,1197027), (129,1534565), (131,1965596), (133,2509883), (135,3196594), (137,4066027), (139,5180139), (141,16952082), (143,26431403), (145,36855440), (147,47814846), (149,62366737), (151,82234537)} ; 82234537 new representative proofs (356642399 redundant, 452506249 invalid) Thu Nov 2 07:17:45 2023: Starting to write 82234537 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. 103040.69 ms (1 min 43 s 40.69 ms) taken to print and save 29138591117 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. Thu Nov 2 07:20:50 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 151, unfiltered] Thu Nov 2 07:23:24 2023: Process terminated. [pid: 52765, tid:23443697252224]