( 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: 34.0436111… h CPU utilization: 2178.79111… core-h ) Tue Nov 7 11:34:14 2023: Process started. [pid: 170951, tid:23205880297344] Tasks: 1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true) 2. generateDProofRepresentativeFiles(157, 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(157, false, true). Tue Nov 7 11:34:14 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 157, unfiltered] 0.01 ms taken to load initial representatives. 0.40 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23205811644160] 0.70 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23205780125440] 0.15 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23205796935424] 0.96 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23205691488000] 1.64 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23205820049152] 11542.50 ms (11 s 542.50 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23205820049152] 0.69 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23205817947904] 5.23 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23205815846656] 10.36 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23205813745408] 9388.82 ms (9 s 388.82 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23205811644160] 12.26 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23205675325184] 17.19 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23205809542912] 8.72 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23205807441664] 1.52 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23205805340416] 3.35 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23205803239168] 7.73 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23205801137920] 13.78 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23205799036672] 10568.47 ms (10 s 568.47 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23205796935424] 16.23 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23205794834176] 2.45 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23205792732928] 11.41 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23205790631680] 11.66 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23205788530432] 0.63 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23205786429184] 10.04 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23205784327936] 8.28 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23205782226688] 9900.40 ms (9 s 900.40 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23205780125440] 20.65 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23205778024192] 14.66 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23205708297984] 0.93 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23205706196736] 19.57 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23205704095488] 2.94 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23205701994240] 18.19 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23205699892992] 12.61 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23205697791744] 1.25 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23205695690496] 350.50 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23205693589248] 11147.83 ms (11 s 147.83 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23205691488000] 34.43 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23205689386752] 9.48 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23205687285504] 26.99 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23205685184256] 24.96 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23205683083008] 11.56 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23205680981760] 45.77 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23205678880512] 35.08 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23205673223936] 165.20 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23205671122688] 193.31 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23205669021440] 354.61 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23205666920192] 559.20 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23205664818944] 346.65 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23205662717696] 40.89 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23205660616448] 248.98 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23205658515200] 72.43 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23205656413952] 324.47 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23205654312704] 819.03 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23205652211456] 902.62 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23205650110208] 1320.29 ms (1 s 320.29 ms) taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23205648008960] 1417.11 ms (1 s 417.11 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23205645907712] 920.37 ms taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23205643806464] 1444.32 ms (1 s 444.32 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23204701665024] 1463.49 ms (1 s 463.49 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23204699563776] 1579.35 ms (1 s 579.35 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23204697462528] 3253.17 ms (3 s 253.17 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23204695361280] 2405.16 ms (2 s 405.16 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23204693260032] 3202.73 ms (3 s 202.73 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23204691158784] 3606.56 ms (3 s 606.56 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23204689057536] 4352.84 ms (4 s 352.84 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23204686956288] 5465.12 ms (5 s 465.12 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23204684855040] 5793.28 ms (5 s 793.28 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23204682753792] 8217.75 ms (8 s 217.75 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23204680652544] 8864.79 ms (8 s 864.79 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23204678551296] 11684.08 ms (11 s 684.09 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. 76013.14 ms (1 min 16 s 13.13 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23204678551296] 123293.53 ms (2 min 3 s 293.53 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23204680652544] 162214.77 ms (2 min 42 s 214.77 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23204682753792] 206504.65 ms (3 min 26 s 504.65 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:23204684855040] 224919.06 ms (3 min 44 s 919.06 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:23204686956288] 243601.81 ms (4 min 3 s 601.81 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:23204689057536] 262926.90 ms (4 min 22 s 926.90 ms) taken to read 109705510 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs153-unfiltered141+.txt. [tid:23204691158784] 284238.62 ms (4 min 44 s 238.62 ms) taken to read 144348401 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs155-unfiltered141+.txt. [tid:23204693260032] 284297.55 ms (4 min 44 s 297.55 ms) additional read duration. Loaded 8 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 151 : 82234537 153 : 109705510 155 : 144348401 550745464 representatives in total. Tue Nov 7 11:39:50 2023: Inserted ≈ 5% of D-proof conclusions. [ 27537273 of 550745464] (ETC: Tue Nov 7 11:52:36 2023 ; 12 min 46 s 251.40 ms remaining ; 13 min 26 s 580.43 ms total) Tue Nov 7 11:40:22 2023: Inserted ≈10% of D-proof conclusions. [ 55074546 of 550745464] (ETC: Tue Nov 7 11:51:15 2023 ; 10 min 52 s 730.72 ms remaining ; 12 min 5 s 256.36 ms total) Tue Nov 7 11:41:05 2023: Inserted ≈15% of D-proof conclusions. [ 82611819 of 550745464] (ETC: Tue Nov 7 11:51:55 2023 ; 10 min 50 s 643.85 ms remaining ; 12 min 45 s 463.35 ms total) Tue Nov 7 11:41:57 2023: Inserted ≈20% of D-proof conclusions. [110149092 of 550745464] (ETC: Tue Nov 7 11:53:04 2023 ; 11 min 7 s 692.81 ms remaining ; 13 min 54 s 616.02 ms total) Tue Nov 7 11:42:43 2023: Inserted ≈25% of D-proof conclusions. [137686366 of 550745464] (ETC: Tue Nov 7 11:53:23 2023 ; 10 min 39 s 799.32 ms remaining ; 14 min 13 s 65.76 ms total) Tue Nov 7 11:43:26 2023: Inserted ≈30% of D-proof conclusions. [165223639 of 550745464] (ETC: Tue Nov 7 11:53:25 2023 ; 9 min 58 s 861.91 ms remaining ; 14 min 15 s 517.01 ms total) Tue Nov 7 11:44:22 2023: Inserted ≈35% of D-proof conclusions. [192760912 of 550745464] (ETC: Tue Nov 7 11:54:02 2023 ; 9 min 39 s 780.25 ms remaining ; 14 min 51 s 969.61 ms total) Tue Nov 7 11:45:17 2023: Inserted ≈40% of D-proof conclusions. [220298185 of 550745464] (ETC: Tue Nov 7 11:54:28 2023 ; 9 min 10 s 988.44 ms remaining ; 15 min 18 s 314.06 ms total) Tue Nov 7 11:46:04 2023: Inserted ≈45% of D-proof conclusions. [247835458 of 550745464] (ETC: Tue Nov 7 11:54:31 2023 ; 8 min 26 s 837.94 ms remaining ; 15 min 21 s 523.52 ms total) Tue Nov 7 11:46:59 2023: Inserted ≈50% of D-proof conclusions. [275372732 of 550745464] (ETC: Tue Nov 7 11:54:48 2023 ; 7 min 49 s 117.20 ms remaining ; 15 min 38 s 234.40 ms total) Tue Nov 7 11:47:48 2023: Inserted ≈55% of D-proof conclusions. [302910005 of 550745464] (ETC: Tue Nov 7 11:54:51 2023 ; 7 min 3 s 588.00 ms remaining ; 15 min 41 s 306.67 ms total) Tue Nov 7 11:48:31 2023: Inserted ≈60% of D-proof conclusions. [330447278 of 550745464] (ETC: Tue Nov 7 11:54:46 2023 ; 6 min 14 s 361.10 ms remaining ; 15 min 35 s 902.74 ms total) Tue Nov 7 11:49:19 2023: Inserted ≈65% of D-proof conclusions. [357984551 of 550745464] (ETC: Tue Nov 7 11:54:48 2023 ; 5 min 28 s 229.41 ms remaining ; 15 min 37 s 798.31 ms total) Tue Nov 7 11:50:11 2023: Inserted ≈70% of D-proof conclusions. [385521824 of 550745464] (ETC: Tue Nov 7 11:54:54 2023 ; 4 min 43 s 347.08 ms remaining ; 15 min 44 s 490.27 ms total) Tue Nov 7 11:50:57 2023: Inserted ≈75% of D-proof conclusions. [413059098 of 550745464] (ETC: Tue Nov 7 11:54:53 2023 ; 3 min 55 s 881.91 ms remaining ; 15 min 43 s 527.63 ms total) Tue Nov 7 11:51:35 2023: Inserted ≈80% of D-proof conclusions. [440596371 of 550745464] (ETC: Tue Nov 7 11:54:41 2023 ; 3 min 6 s 295.48 ms remaining ; 15 min 31 s 477.39 ms total) Tue Nov 7 11:52:16 2023: Inserted ≈85% of D-proof conclusions. [468133644 of 550745464] (ETC: Tue Nov 7 11:54:34 2023 ; 2 min 18 s 670.51 ms remaining ; 15 min 24 s 470.09 ms total) Tue Nov 7 11:52:58 2023: Inserted ≈90% of D-proof conclusions. [495670917 of 550745464] (ETC: Tue Nov 7 11:54:30 2023 ; 1 min 32 s 68.36 ms remaining ; 15 min 20 s 683.62 ms total) Tue Nov 7 11:53:44 2023: Inserted ≈95% of D-proof conclusions. [523208190 of 550745464] (ETC: Tue Nov 7 11:54:30 2023 ; 46 s 29.12 ms remaining ; 15 min 20 s 582.32 ms total) Tue Nov 7 11:54:38 2023: Inserted 100% of D-proof conclusions. [550745464 of 550745464] (ETC: Tue Nov 7 11:54:38 2023 ; 0.00 ms remaining ; 15 min 28 s 695.07 ms total) 928696.66 ms (15 min 28 s 696.66 ms) total insertion duration. Known iteration count loaded from 157:2083519342. Tue Nov 7 11:54:38 2023: Starting to generate D-proof representatives of length 157. Tue Nov 7 12:36:02 2023: Iterated ≈ 2% of D-proof candidates. [ 41670386 of 2083519342] (ETC: Wed Nov 8 22:24:01 2023 ; 1 d 9 h 47 min 59 s 363.39 ms remaining ; 1 d 10 h 29 min 22 s 615.65 ms total) Tue Nov 7 13:15:38 2023: Iterated ≈ 4% of D-proof candidates. [ 83340773 of 2083519342] (ETC: Wed Nov 8 21:39:37 2023 ; 1 d 8 h 23 min 58 s 296.08 ms remaining ; 1 d 9 h 44 min 58 s 225.04 ms total) Tue Nov 7 13:54:11 2023: Iterated ≈ 6% of D-proof candidates. [ 125011160 of 2083519342] (ETC: Wed Nov 8 21:06:57 2023 ; 1 d 7 h 12 min 46 s 369.02 ms remaining ; 1 d 9 h 12 min 18 s 690.41 ms total) Tue Nov 7 14:38:28 2023: Iterated ≈ 8% of D-proof candidates. [ 166681547 of 2083519342] (ETC: Wed Nov 8 22:02:25 2023 ; 1 d 7 h 23 min 56 s 825.14 ms remaining ; 1 d 10 h 7 min 46 s 114.27 ms total) Tue Nov 7 15:25:57 2023: Iterated ≈10% of D-proof candidates. [ 208351934 of 2083519342] (ETC: Wed Nov 8 23:07:46 2023 ; 1 d 7 h 41 min 48 s 860.94 ms remaining ; 1 d 11 h 13 min 7 s 623.25 ms total) Tue Nov 7 16:06:42 2023: Iterated ≈12% of D-proof candidates. [ 250022321 of 2083519342] (ETC: Wed Nov 8 22:55:04 2023 ; 1 d 6 h 48 min 22 s 829.98 ms remaining ; 1 d 11 h 25 s 943.16 ms total) Tue Nov 7 16:44:44 2023: Iterated ≈14% of D-proof candidates. [ 291692707 of 2083519342] (ETC: Wed Nov 8 22:26:45 2023 ; 1 d 5 h 42 min 1 s 55.25 ms remaining ; 1 d 10 h 32 min 6 s 808.37 ms total) Tue Nov 7 17:34:37 2023: Iterated ≈16% of D-proof candidates. [ 333363094 of 2083519342] (ETC: Wed Nov 8 23:19:27 2023 ; 1 d 5 h 44 min 50 s 456.82 ms remaining ; 1 d 11 h 24 min 48 s 639.02 ms total) Tue Nov 7 18:16:08 2023: Iterated ≈18% of D-proof candidates. [ 375033481 of 2083519342] (ETC: Wed Nov 8 23:14:01 2023 ; 1 d 4 h 57 min 53 s 155.35 ms remaining ; 1 d 11 h 19 min 22 s 384.53 ms total) Tue Nov 7 18:59:15 2023: Iterated ≈20% of D-proof candidates. [ 416703868 of 2083519342] (ETC: Wed Nov 8 23:17:40 2023 ; 1 d 4 h 18 min 25 s 217.94 ms remaining ; 1 d 11 h 23 min 1 s 522.40 ms total) Tue Nov 7 19:45:03 2023: Iterated ≈22% of D-proof candidates. [ 458374255 of 2083519342] (ETC: Wed Nov 8 23:32:50 2023 ; 1 d 3 h 47 min 47 s 354.56 ms remaining ; 1 d 11 h 38 min 11 s 480.19 ms total) Tue Nov 7 20:22:23 2023: Iterated ≈24% of D-proof candidates. [ 500044642 of 2083519342] (ETC: Wed Nov 8 23:10:12 2023 ; 1 d 2 h 47 min 49 s 520.02 ms remaining ; 1 d 11 h 15 min 33 s 578.97 ms total) Tue Nov 7 21:09:05 2023: Iterated ≈26% of D-proof candidates. [ 541715028 of 2083519342] (ETC: Wed Nov 8 23:27:05 2023 ; 1 d 2 h 18 min 638.08 ms remaining ; 1 d 11 h 32 min 26 s 808.14 ms total) Tue Nov 7 21:48:54 2023: Iterated ≈28% of D-proof candidates. [ 583385415 of 2083519342] (ETC: Wed Nov 8 23:16:59 2023 ; 1 d 1 h 28 min 5 s 129.99 ms remaining ; 1 d 11 h 22 min 20 s 458.25 ms total) Tue Nov 7 22:33:56 2023: Iterated ≈30% of D-proof candidates. [ 625055802 of 2083519342] (ETC: Wed Nov 8 23:25:37 2023 ; 1 d 51 min 40 s 840.62 ms remaining ; 1 d 11 h 30 min 58 s 343.70 ms total) Tue Nov 7 23:12:10 2023: Iterated ≈32% of D-proof candidates. [ 666726189 of 2083519342] (ETC: Wed Nov 8 23:11:53 2023 ; 23 h 59 min 43 s 577.35 ms remaining ; 1 d 11 h 17 min 14 s 672.54 ms total) Tue Nov 7 23:58:56 2023: Iterated ≈34% of D-proof candidates. [ 708396576 of 2083519342] (ETC: Wed Nov 8 23:24:54 2023 ; 23 h 25 min 58 s 201.18 ms remaining ; 1 d 11 h 30 min 15 s 456.31 ms total) Wed Nov 8 00:43:51 2023: Iterated ≈36% of D-proof candidates. [ 750066963 of 2083519342] (ETC: Wed Nov 8 23:31:20 2023 ; 22 h 47 min 28 s 871.43 ms remaining ; 1 d 11 h 36 min 41 s 361.60 ms total) Wed Nov 8 01:21:55 2023: Iterated ≈38% of D-proof candidates. [ 791737349 of 2083519342] (ETC: Wed Nov 8 23:19:02 2023 ; 21 h 57 min 7 s 328.54 ms remaining ; 1 d 11 h 24 min 23 s 433.04 ms total) Wed Nov 8 01:58:02 2023: Iterated ≈40% of D-proof candidates. [ 833407736 of 2083519342] (ETC: Wed Nov 8 23:03:08 2023 ; 21 h 5 min 5 s 554.81 ms remaining ; 1 d 11 h 8 min 29 s 257.94 ms total) Wed Nov 8 02:42:43 2023: Iterated ≈42% of D-proof candidates. [ 875078123 of 2083519342] (ETC: Wed Nov 8 23:09:06 2023 ; 20 h 26 min 23 s 57.77 ms remaining ; 1 d 11 h 14 min 27 s 340.91 ms total) Wed Nov 8 03:24:21 2023: Iterated ≈44% of D-proof candidates. [ 916748510 of 2083519342] (ETC: Wed Nov 8 23:07:38 2023 ; 19 h 43 min 16 s 343.81 ms remaining ; 1 d 11 h 12 min 59 s 185.32 ms total) Wed Nov 8 04:03:28 2023: Iterated ≈46% of D-proof candidates. [ 958418897 of 2083519342] (ETC: Wed Nov 8 23:00:47 2023 ; 18 h 57 min 19 s 252.15 ms remaining ; 1 d 11 h 6 min 8 s 985.43 ms total) Wed Nov 8 04:49:39 2023: Iterated ≈48% of D-proof candidates. [1000089284 of 2083519342] (ETC: Wed Nov 8 23:09:15 2023 ; 18 h 19 min 35 s 611.21 ms remaining ; 1 d 11 h 14 min 36 s 175.39 ms total) Wed Nov 8 05:30:00 2023: Iterated ≈50% of D-proof candidates. [1041759671 of 2083519342] (ETC: Wed Nov 8 23:05:22 2023 ; 17 h 35 min 21 s 791.66 ms remaining ; 1 d 11 h 10 min 43 s 583.33 ms total) Wed Nov 8 06:05:56 2023: Iterated ≈52% of D-proof candidates. [1083430057 of 2083519342] (ETC: Wed Nov 8 22:53:17 2023 ; 16 h 47 min 20 s 860.04 ms remaining ; 1 d 10 h 58 min 38 s 458.30 ms total) Wed Nov 8 06:46:39 2023: Iterated ≈54% of D-proof candidates. [1125100444 of 2083519342] (ETC: Wed Nov 8 22:50:58 2023 ; 16 h 4 min 18 s 586.42 ms remaining ; 1 d 10 h 56 min 19 s 535.61 ms total) Wed Nov 8 07:27:14 2023: Iterated ≈56% of D-proof candidates. [1166770831 of 2083519342] (ETC: Wed Nov 8 22:48:33 2023 ; 15 h 21 min 19 s 294.28 ms remaining ; 1 d 10 h 53 min 54 s 759.66 ms total) Wed Nov 8 08:05:34 2023: Iterated ≈58% of D-proof candidates. [1208441218 of 2083519342] (ETC: Wed Nov 8 22:42:27 2023 ; 14 h 36 min 52 s 730.39 ms remaining ; 1 d 10 h 47 min 48 s 405.65 ms total) Wed Nov 8 08:42:49 2023: Iterated ≈60% of D-proof candidates. [1250111605 of 2083519342] (ETC: Wed Nov 8 22:34:55 2023 ; 13 h 52 min 6 s 752.13 ms remaining ; 1 d 10 h 40 min 16 s 880.30 ms total) Wed Nov 8 09:20:23 2023: Iterated ≈62% of D-proof candidates. [1291781992 of 2083519342] (ETC: Wed Nov 8 22:28:25 2023 ; 13 h 8 min 2 s 143.42 ms remaining ; 1 d 10 h 33 min 46 s 693.21 ms total) Wed Nov 8 09:58:44 2023: Iterated ≈64% of D-proof candidates. [1333452378 of 2083519342] (ETC: Wed Nov 8 22:23:32 2023 ; 12 h 24 min 47 s 903.23 ms remaining ; 1 d 10 h 28 min 53 s 64.38 ms total) Wed Nov 8 10:37:41 2023: Iterated ≈66% of D-proof candidates. [1375122765 of 2083519342] (ETC: Wed Nov 8 22:19:52 2023 ; 11 h 42 min 10 s 548.93 ms remaining ; 1 d 10 h 25 min 13 s 379.09 ms total) Wed Nov 8 11:15:27 2023: Iterated ≈68% of D-proof candidates. [1416793152 of 2083519342] (ETC: Wed Nov 8 22:14:39 2023 ; 10 h 59 min 12 s 236.41 ms remaining ; 1 d 10 h 20 min 738.68 ms total) Wed Nov 8 11:53:00 2023: Iterated ≈70% of D-proof candidates. [1458463539 of 2083519342] (ETC: Wed Nov 8 22:09:27 2023 ; 10 h 16 min 26 s 490.12 ms remaining ; 1 d 10 h 14 min 48 s 300.31 ms total) Wed Nov 8 12:29:56 2023: Iterated ≈72% of D-proof candidates. [1500133926 of 2083519342] (ETC: Wed Nov 8 22:03:39 2023 ; 9 h 33 min 43 s 318.51 ms remaining ; 1 d 10 h 9 min 423.19 ms total) Wed Nov 8 13:06:22 2023: Iterated ≈74% of D-proof candidates. [1541804313 of 2083519342] (ETC: Wed Nov 8 21:57:30 2023 ; 8 h 51 min 8 s 677.20 ms remaining ; 1 d 10 h 2 min 51 s 835.36 ms total) Wed Nov 8 13:42:37 2023: Iterated ≈76% of D-proof candidates. [1583474699 of 2083519342] (ETC: Wed Nov 8 21:51:27 2023 ; 8 h 8 min 50 s 81.21 ms remaining ; 1 d 9 h 56 min 48 s 671.47 ms total) Wed Nov 8 14:18:40 2023: Iterated ≈78% of D-proof candidates. [1625145086 of 2083519342] (ETC: Wed Nov 8 21:45:27 2023 ; 7 h 26 min 46 s 564.88 ms remaining ; 1 d 9 h 50 min 48 s 21.99 ms total) Wed Nov 8 14:54:29 2023: Iterated ≈80% of D-proof candidates. [1666815473 of 2083519342] (ETC: Wed Nov 8 21:39:26 2023 ; 6 h 44 min 57 s 518.86 ms remaining ; 1 d 9 h 44 min 47 s 594.11 ms total) Wed Nov 8 15:29:33 2023: Iterated ≈82% of D-proof candidates. [1708485860 of 2083519342] (ETC: Wed Nov 8 21:32:50 2023 ; 6 h 3 min 16 s 388.84 ms remaining ; 1 d 9 h 38 min 11 s 48.95 ms total) Wed Nov 8 16:04:04 2023: Iterated ≈84% of D-proof candidates. [1750156247 of 2083519342] (ETC: Wed Nov 8 21:25:52 2023 ; 5 h 21 min 47 s 740.99 ms remaining ; 1 d 9 h 31 min 13 s 381.10 ms total) Wed Nov 8 16:38:09 2023: Iterated ≈86% of D-proof candidates. [1791826634 of 2083519342] (ETC: Wed Nov 8 21:18:43 2023 ; 4 h 40 min 34 s 265.32 ms remaining ; 1 d 9 h 24 min 4 s 752.22 ms total) Wed Nov 8 17:12:26 2023: Iterated ≈88% of D-proof candidates. [1833497020 of 2083519342] (ETC: Wed Nov 8 21:12:07 2023 ; 3 h 59 min 41 s 866.08 ms remaining ; 1 d 9 h 17 min 28 s 883.51 ms total) Wed Nov 8 17:46:36 2023: Iterated ≈90% of D-proof candidates. [1875167407 of 2083519342] (ETC: Wed Nov 8 21:05:43 2023 ; 3 h 19 min 6 s 407.30 ms remaining ; 1 d 9 h 11 min 4 s 72.59 ms total) Wed Nov 8 18:20:26 2023: Iterated ≈92% of D-proof candidates. [1916837794 of 2083519342] (ETC: Wed Nov 8 20:59:12 2023 ; 2 h 38 min 45 s 845.88 ms remaining ; 1 d 9 h 4 min 33 s 73.06 ms total) Wed Nov 8 18:53:48 2023: Iterated ≈94% of D-proof candidates. [1958508181 of 2083519342] (ETC: Wed Nov 8 20:52:28 2023 ; 1 h 58 min 40 s 155.05 ms remaining ; 1 d 8 h 57 min 49 s 250.30 ms total) Wed Nov 8 19:27:04 2023: Iterated ≈96% of D-proof candidates. [2000178568 of 2083519342] (ETC: Wed Nov 8 20:45:55 2023 ; 1 h 18 min 51 s 61.73 ms remaining ; 1 d 8 h 51 min 16 s 542.73 ms total) Wed Nov 8 20:00:25 2023: Iterated ≈98% of D-proof candidates. [2041848955 of 2083519342] (ETC: Wed Nov 8 20:39:43 2023 ; 39 min 18 s 97.42 ms remaining ; 1 d 8 h 45 min 4 s 870.68 ms total) Wed Nov 8 20:34:22 2023: Iterated 100% of D-proof candidates. [2083519342 of 2083519342] (ETC: Wed Nov 8 20:34:22 2023 ; 0.00 ms remaining ; 1 d 8 h 39 min 43 s 993.59 ms total) 117585361.55 ms (1 d 8 h 39 min 45 s 361.55 ms) taken to collect 192661720 D-proofs of length 157. [iterated 2083519342 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 }, { 153, 1176314122 }, { 155, 1558170072 }, { 157, 2083519342 } } 1456113.58 ms (24 min 16 s 113.58 ms) taken to filter and order new representative proofs. Found 192661720 representative, 809233406 redundant, and 1081624216 invalid condensed detachment proof strings. lengths up to 157 ; 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), (153,109705510), (155,144348401), (157,192661720)} ; 192661720 new representative proofs (809233406 redundant, 1081624216 invalid) Wed Nov 8 21:20:13 2023: Starting to write 192661720 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. 251823.42 ms (4 min 11 s 823.43 ms) taken to print and save 73644408291 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. Wed Nov 8 21:28:20 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 157, unfiltered] Wed Nov 8 21:36:51 2023: Process terminated. [pid: 170951, tid:23205880297344]