( 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: 48.43666… h CPU utilization: 3099.94666… core-h ) Thu Nov 9 03:32:07 2023: Process started. [pid: 63158, tid:23383611914112] Tasks: 1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true) 2. generateDProofRepresentativeFiles(159, 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(159, false, true). Thu Nov 9 03:32:07 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 159, unfiltered] 0.01 ms taken to load initial representatives. 0.41 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23383543260928] 0.85 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23383536957184] 1.31 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23383547463424] 1.76 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23383549564672] 1.67 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23383530653440] 6.44 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23383551665920] 10190.48 ms (10 s 190.48 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23383549564672] 9850.03 ms (9 s 850.03 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23383547463424] 7.44 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23383545362176] 8873.11 ms (8 s 873.11 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23383543260928] 16.43 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23383541159680] 2.16 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23383539058432] 9475.44 ms (9 s 475.44 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23383536957184] 8.96 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23383534855936] 15.41 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23383532754688] 10655.82 ms (10 s 655.82 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23383530653440] 6.85 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23383528552192] 2.73 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23383526450944] 7.88 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23383524349696] 11.32 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23383522248448] 16.27 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23383520147200] 20.77 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23383518045952] 4.34 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23383515944704] 8.41 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23383513843456] 1.79 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23383511742208] 19.67 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23383509640960] 10.51 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23383507539712] 20.00 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23383505438464] 22.70 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23383503337216] 15.30 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23383501235968] 10.91 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23383499134720] 8.75 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23383497033472] 13.64 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23383494932224] 32.48 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23383492830976] 20.96 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23383490729728] 25.13 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23383488628480] 9.99 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23383486527232] 27.06 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23383484425984] 39.11 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23383482324736] 43.00 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23381533521664] 30.56 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23381531420416] 44.85 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23381529319168] 26.61 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23381527217920] 321.33 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23381525116672] 372.54 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23381523015424] 36.86 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23381520914176] 519.12 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23381518812928] 581.82 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23381516711680] 505.12 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23381514610432] 65.32 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23381512509184] 581.75 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23381510407936] 870.97 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23381508306688] 1109.13 ms (1 s 109.13 ms) taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23381506205440] 1358.69 ms (1 s 358.69 ms) taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23381504104192] 1520.60 ms (1 s 520.60 ms) taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23381502002944] 1563.16 ms (1 s 563.16 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23381499901696] 1747.16 ms (1 s 747.16 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23381497800448] 2087.71 ms (2 s 87.72 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23381495699200] 2214.38 ms (2 s 214.38 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23381493597952] 4863.60 ms (4 s 863.60 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23381491496704] 7759.09 ms (7 s 759.09 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23381489395456] 3259.13 ms (3 s 259.13 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23381487294208] 3405.86 ms (3 s 405.86 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23381485192960] 3821.55 ms (3 s 821.55 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23381483091712] 4546.41 ms (4 s 546.41 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23381480990464] 4783.12 ms (4 s 783.12 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23381478889216] 3157.73 ms (3 s 157.73 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23381476787968] 8421.97 ms (8 s 421.97 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23381474686720] 7839.84 ms (7 s 839.84 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23381472585472] 10797.97 ms (10 s 797.97 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. 86716.58 ms (1 min 26 s 716.58 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23381472585472] 141770.94 ms (2 min 21 s 770.94 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23381474686720] 180820.80 ms (3 min 820.80 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23381476787968] 245771.30 ms (4 min 5 s 771.30 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:23381478889216] 273581.82 ms (4 min 33 s 581.82 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:23381480990464] 304001.83 ms (5 min 4 s 1.82 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:23381483091712] 338533.61 ms (5 min 38 s 533.61 ms) taken to read 109705510 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs153-unfiltered141+.txt. [tid:23381485192960] 363634.06 ms (6 min 3 s 634.06 ms) taken to read 144348401 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs155-unfiltered141+.txt. [tid:23381487294208] 389043.42 ms (6 min 29 s 43.42 ms) taken to read 192661720 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. [tid:23381489395456] 389076.52 ms (6 min 29 s 76.52 ms) additional read duration. Loaded 9 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 151 : 82234537 153 : 109705510 155 : 144348401 157 : 192661720 743407184 representatives in total. Thu Nov 9 03:39:41 2023: Inserted ≈ 5% of D-proof conclusions. [ 37170359 of 743407184] (ETC: Thu Nov 9 03:56:40 2023 ; 16 min 59 s 203.90 ms remaining ; 17 min 52 s 846.21 ms total) Thu Nov 9 03:40:23 2023: Inserted ≈10% of D-proof conclusions. [ 74340718 of 743407184] (ETC: Thu Nov 9 03:54:46 2023 ; 14 min 23 s 332.06 ms remaining ; 15 min 59 s 257.85 ms total) Thu Nov 9 03:41:16 2023: Inserted ≈15% of D-proof conclusions. [111511077 of 743407184] (ETC: Thu Nov 9 03:55:21 2023 ; 14 min 4 s 614.78 ms remaining ; 16 min 33 s 664.45 ms total) Thu Nov 9 03:42:24 2023: Inserted ≈20% of D-proof conclusions. [148681436 of 743407184] (ETC: Thu Nov 9 03:56:53 2023 ; 14 min 28 s 499.51 ms remaining ; 18 min 5 s 624.38 ms total) Thu Nov 9 03:43:30 2023: Inserted ≈25% of D-proof conclusions. [185851796 of 743407184] (ETC: Thu Nov 9 03:57:39 2023 ; 14 min 9 s 78.11 ms remaining ; 18 min 52 s 104.14 ms total) Thu Nov 9 03:44:45 2023: Inserted ≈30% of D-proof conclusions. [223022155 of 743407184] (ETC: Thu Nov 9 03:58:39 2023 ; 13 min 54 s 410.57 ms remaining ; 19 min 52 s 15.10 ms total) Thu Nov 9 03:45:58 2023: Inserted ≈35% of D-proof conclusions. [260192514 of 743407184] (ETC: Thu Nov 9 03:59:19 2023 ; 13 min 20 s 735.38 ms remaining ; 20 min 31 s 900.58 ms total) Thu Nov 9 03:47:24 2023: Inserted ≈40% of D-proof conclusions. [297362873 of 743407184] (ETC: Thu Nov 9 04:00:19 2023 ; 12 min 55 s 188.95 ms remaining ; 21 min 31 s 981.59 ms total) Thu Nov 9 03:48:24 2023: Inserted ≈45% of D-proof conclusions. [334533232 of 743407184] (ETC: Thu Nov 9 04:00:10 2023 ; 11 min 45 s 424.45 ms remaining ; 21 min 22 s 589.91 ms total) Thu Nov 9 03:49:41 2023: Inserted ≈50% of D-proof conclusions. [371703592 of 743407184] (ETC: Thu Nov 9 04:00:35 2023 ; 10 min 53 s 973.64 ms remaining ; 21 min 47 s 947.27 ms total) Thu Nov 9 03:50:57 2023: Inserted ≈55% of D-proof conclusions. [408873951 of 743407184] (ETC: Thu Nov 9 04:00:54 2023 ; 9 min 57 s 73.69 ms remaining ; 22 min 6 s 830.42 ms total) Thu Nov 9 03:52:19 2023: Inserted ≈60% of D-proof conclusions. [446044310 of 743407184] (ETC: Thu Nov 9 04:01:20 2023 ; 9 min 944.59 ms remaining ; 22 min 32 s 361.48 ms total) Thu Nov 9 03:53:23 2023: Inserted ≈65% of D-proof conclusions. [483214669 of 743407184] (ETC: Thu Nov 9 04:01:15 2023 ; 7 min 51 s 624.17 ms remaining ; 22 min 27 s 497.62 ms total) Thu Nov 9 03:54:29 2023: Inserted ≈70% of D-proof conclusions. [520385028 of 743407184] (ETC: Thu Nov 9 04:01:12 2023 ; 6 min 43 s 490.53 ms remaining ; 22 min 24 s 968.43 ms total) Thu Nov 9 03:55:41 2023: Inserted ≈75% of D-proof conclusions. [557555388 of 743407184] (ETC: Thu Nov 9 04:01:19 2023 ; 5 min 37 s 857.33 ms remaining ; 22 min 31 s 429.30 ms total) Thu Nov 9 03:56:53 2023: Inserted ≈80% of D-proof conclusions. [594725747 of 743407184] (ETC: Thu Nov 9 04:01:25 2023 ; 4 min 31 s 473.73 ms remaining ; 22 min 37 s 368.64 ms total) Thu Nov 9 03:58:11 2023: Inserted ≈85% of D-proof conclusions. [631896106 of 743407184] (ETC: Thu Nov 9 04:01:36 2023 ; 3 min 25 s 394.09 ms remaining ; 22 min 49 s 293.90 ms total) Thu Nov 9 03:59:23 2023: Inserted ≈90% of D-proof conclusions. [669066465 of 743407184] (ETC: Thu Nov 9 04:01:41 2023 ; 2 min 17 s 353.99 ms remaining ; 22 min 53 s 539.84 ms total) Thu Nov 9 04:00:22 2023: Inserted ≈95% of D-proof conclusions. [706236824 of 743407184] (ETC: Thu Nov 9 04:01:31 2023 ; 1 min 8 s 168.13 ms remaining ; 22 min 43 s 362.49 ms total) Thu Nov 9 04:01:14 2023: Inserted 100% of D-proof conclusions. [743407184 of 743407184] (ETC: Thu Nov 9 04:01:14 2023 ; 0.00 ms remaining ; 22 min 26 s 583.57 ms total) 1346587.66 ms (22 min 26 s 587.66 ms) total insertion duration. Known iteration count loaded from 159:2814993667. Thu Nov 9 04:01:14 2023: Starting to generate D-proof representatives of length 159. Thu Nov 9 05:00:34 2023: Iterated ≈ 2% of D-proof candidates. [ 56299873 of 2814993667] (ETC: Sat Nov 11 05:27:42 2023 ; 2 d 27 min 8 s 590.64 ms remaining ; 2 d 1 h 26 min 28 s 357.77 ms total) Thu Nov 9 05:56:07 2023: Iterated ≈ 4% of D-proof candidates. [ 112599746 of 2814993667] (ETC: Sat Nov 11 03:53:18 2023 ; 1 d 21 h 57 min 11 s 63.91 ms remaining ; 1 d 23 h 52 min 4 s 24.87 ms total) Thu Nov 9 06:51:39 2023: Iterated ≈ 6% of D-proof candidates. [ 168899620 of 2814993667] (ETC: Sat Nov 11 03:21:41 2023 ; 1 d 20 h 30 min 1 s 601.44 ms remaining ; 1 d 23 h 20 min 27 s 235.57 ms total) Thu Nov 9 07:55:06 2023: Iterated ≈ 8% of D-proof candidates. [ 225199493 of 2814993667] (ETC: Sat Nov 11 04:44:38 2023 ; 1 d 20 h 49 min 31 s 578.91 ms remaining ; 2 d 43 min 23 s 890.09 ms total) Thu Nov 9 09:01:30 2023: Iterated ≈10% of D-proof candidates. [ 281499366 of 2814993667] (ETC: Sat Nov 11 06:03:55 2023 ; 1 d 21 h 2 min 25 s 375.37 ms remaining ; 2 d 2 h 2 min 41 s 528.14 ms total) Thu Nov 9 09:59:37 2023: Iterated ≈12% of D-proof candidates. [ 337799240 of 2814993667] (ETC: Sat Nov 11 05:47:52 2023 ; 1 d 19 h 48 min 14 s 57.72 ms remaining ; 2 d 1 h 46 min 37 s 792.86 ms total) Thu Nov 9 10:56:18 2023: Iterated ≈14% of D-proof candidates. [ 394099113 of 2814993667] (ETC: Sat Nov 11 05:26:01 2023 ; 1 d 18 h 29 min 42 s 764.75 ms remaining ; 2 d 1 h 24 min 46 s 935.73 ms total) Thu Nov 9 12:07:16 2023: Iterated ≈16% of D-proof candidates. [ 450398986 of 2814993667] (ETC: Sat Nov 11 06:38:58 2023 ; 1 d 18 h 31 min 41 s 755.89 ms remaining ; 2 d 2 h 37 min 43 s 995.05 ms total) Thu Nov 9 13:05:34 2023: Iterated ≈18% of D-proof candidates. [ 506698860 of 2814993667] (ETC: Sat Nov 11 06:25:18 2023 ; 1 d 17 h 19 min 44 s 267.77 ms remaining ; 2 d 2 h 24 min 4 s 228.99 ms total) Thu Nov 9 14:09:39 2023: Iterated ≈20% of D-proof candidates. [ 562998733 of 2814993667] (ETC: Sat Nov 11 06:43:19 2023 ; 1 d 16 h 33 min 40 s 417.01 ms remaining ; 2 d 2 h 42 min 5 s 521.23 ms total) Thu Nov 9 15:12:13 2023: Iterated ≈22% of D-proof candidates. [ 619298606 of 2814993667] (ETC: Sat Nov 11 06:51:09 2023 ; 1 d 15 h 38 min 55 s 998.57 ms remaining ; 2 d 2 h 49 min 54 s 869.90 ms total) Thu Nov 9 16:05:29 2023: Iterated ≈24% of D-proof candidates. [ 675598480 of 2814993667] (ETC: Sat Nov 11 06:18:58 2023 ; 1 d 14 h 13 min 28 s 770.87 ms remaining ; 2 d 2 h 17 min 44 s 172.19 ms total) Thu Nov 9 17:13:18 2023: Iterated ≈26% of D-proof candidates. [ 731898353 of 2814993667] (ETC: Sat Nov 11 06:47:40 2023 ; 1 d 13 h 34 min 21 s 686.51 ms remaining ; 2 d 2 h 46 min 26 s 62.82 ms total) Thu Nov 9 18:09:58 2023: Iterated ≈28% of D-proof candidates. [ 788198226 of 2814993667] (ETC: Sat Nov 11 06:32:25 2023 ; 1 d 12 h 22 min 27 s 95.08 ms remaining ; 2 d 2 h 31 min 10 s 965.32 ms total) Thu Nov 9 19:13:51 2023: Iterated ≈30% of D-proof candidates. [ 844498100 of 2814993667] (ETC: Sat Nov 11 06:43:18 2023 ; 1 d 11 h 29 min 27 s 38.52 ms remaining ; 2 d 2 h 42 min 4 s 340.74 ms total) Thu Nov 9 20:10:08 2023: Iterated ≈32% of D-proof candidates. [ 900797973 of 2814993667] (ETC: Sat Nov 11 06:29:05 2023 ; 1 d 10 h 18 min 56 s 155.17 ms remaining ; 2 d 2 h 27 min 50 s 816.38 ms total) Thu Nov 9 21:17:30 2023: Iterated ≈34% of D-proof candidates. [ 957097846 of 2814993667] (ETC: Sat Nov 11 06:49:04 2023 ; 1 d 9 h 31 min 34 s 278.37 ms remaining ; 2 d 2 h 47 min 50 s 118.67 ms total) Thu Nov 9 22:19:26 2023: Iterated ≈36% of D-proof candidates. [1013397720 of 2814993667] (ETC: Sat Nov 11 06:51:48 2023 ; 1 d 8 h 32 min 22 s 53.79 ms remaining ; 2 d 2 h 50 min 34 s 459.04 ms total) Thu Nov 9 23:12:33 2023: Iterated ≈38% of D-proof candidates. [1069697593 of 2814993667] (ETC: Sat Nov 11 06:31:00 2023 ; 1 d 7 h 18 min 27 s 792.01 ms remaining ; 2 d 2 h 29 min 46 s 761.27 ms total) Fri Nov 10 00:08:50 2023: Iterated ≈40% of D-proof candidates. [1125997466 of 2814993667] (ETC: Sat Nov 11 06:20:13 2023 ; 1 d 6 h 11 min 23 s 844.58 ms remaining ; 2 d 2 h 18 min 59 s 740.88 ms total) Fri Nov 10 01:08:41 2023: Iterated ≈42% of D-proof candidates. [1182297340 of 2814993667] (ETC: Sat Nov 11 06:18:59 2023 ; 1 d 5 h 10 min 17 s 823.21 ms remaining ; 2 d 2 h 17 min 45 s 212.42 ms total) Fri Nov 10 02:09:38 2023: Iterated ≈44% of D-proof candidates. [1238597213 of 2814993667] (ETC: Sat Nov 11 06:20:21 2023 ; 1 d 4 h 10 min 42 s 340.84 ms remaining ; 2 d 2 h 19 min 7 s 37.16 ms total) Fri Nov 10 03:07:35 2023: Iterated ≈46% of D-proof candidates. [1294897086 of 2814993667] (ETC: Sat Nov 11 06:15:03 2023 ; 1 d 3 h 7 min 27 s 650.98 ms remaining ; 2 d 2 h 13 min 48 s 983.19 ms total) Fri Nov 10 04:11:25 2023: Iterated ≈48% of D-proof candidates. [1351196960 of 2814993667] (ETC: Sat Nov 11 06:22:27 2023 ; 1 d 2 h 11 min 2 s 190.00 ms remaining ; 2 d 2 h 21 min 13 s 442.30 ms total) Fri Nov 10 05:04:35 2023: Iterated ≈50% of D-proof candidates. [1407496833 of 2814993667] (ETC: Sat Nov 11 06:07:55 2023 ; 1 d 1 h 3 min 20 s 792.29 ms remaining ; 2 d 2 h 6 min 41 s 584.52 ms total) Fri Nov 10 06:01:14 2023: Iterated ≈52% of D-proof candidates. [1463796706 of 2814993667] (ETC: Sat Nov 11 06:01:15 2023 ; 1 d 414.77 ms remaining ; 2 d 2 h 863.99 ms total) Fri Nov 10 06:58:05 2023: Iterated ≈54% of D-proof candidates. [1520096580 of 2814993667] (ETC: Sat Nov 11 05:55:24 2023 ; 22 h 57 min 18 s 960.95 ms remaining ; 2 d 1 h 54 min 9 s 915.09 ms total) Fri Nov 10 07:52:30 2023: Iterated ≈56% of D-proof candidates. [1576396453 of 2814993667] (ETC: Sat Nov 11 05:45:39 2023 ; 21 h 53 min 8 s 788.86 ms remaining ; 2 d 1 h 44 min 25 s 429.15 ms total) Fri Nov 10 08:46:38 2023: Iterated ≈58% of D-proof candidates. [1632696326 of 2814993667] (ETC: Sat Nov 11 05:36:05 2023 ; 20 h 49 min 26 s 176.84 ms remaining ; 2 d 1 h 34 min 50 s 897.10 ms total) Fri Nov 10 09:41:14 2023: Iterated ≈60% of D-proof candidates. [1688996200 of 2814993667] (ETC: Sat Nov 11 05:27:54 2023 ; 19 h 46 min 39 s 960.87 ms remaining ; 2 d 1 h 26 min 39 s 902.15 ms total) Fri Nov 10 10:34:46 2023: Iterated ≈62% of D-proof candidates. [1745296073 of 2814993667] (ETC: Sat Nov 11 05:18:32 2023 ; 18 h 43 min 46 s 581.77 ms remaining ; 2 d 1 h 17 min 18 s 373.00 ms total) Fri Nov 10 11:28:10 2023: Iterated ≈64% of D-proof candidates. [1801595946 of 2814993667] (ETC: Sat Nov 11 05:09:33 2023 ; 17 h 41 min 23 s 899.47 ms remaining ; 2 d 1 h 8 min 19 s 720.61 ms total) Fri Nov 10 12:19:26 2023: Iterated ≈66% of D-proof candidates. [1857895820 of 2814993667] (ETC: Sat Nov 11 04:57:54 2023 ; 16 h 38 min 28 s 100.58 ms remaining ; 2 d 56 min 40 s 295.80 ms total) Fri Nov 10 13:13:16 2023: Iterated ≈68% of D-proof candidates. [1914195693 of 2814993667] (ETC: Sat Nov 11 04:50:41 2023 ; 15 h 37 min 25 s 570.58 ms remaining ; 2 d 49 min 27 s 407.95 ms total) Fri Nov 10 14:05:42 2023: Iterated ≈70% of D-proof candidates. [1970495566 of 2814993667] (ETC: Sat Nov 11 04:41:54 2023 ; 14 h 36 min 11 s 986.82 ms remaining ; 2 d 40 min 39 s 955.89 ms total) Fri Nov 10 14:57:58 2023: Iterated ≈72% of D-proof candidates. [2026795440 of 2814993667] (ETC: Sat Nov 11 04:33:21 2023 ; 13 h 35 min 23 s 719.51 ms remaining ; 2 d 32 min 7 s 569.63 ms total) Fri Nov 10 15:49:24 2023: Iterated ≈74% of D-proof candidates. [2083095313 of 2814993667] (ETC: Sat Nov 11 04:24:10 2023 ; 12 h 34 min 45 s 707.10 ms remaining ; 2 d 22 min 55 s 796.42 ms total) Fri Nov 10 16:40:19 2023: Iterated ≈76% of D-proof candidates. [2139395186 of 2814993667] (ETC: Sat Nov 11 04:14:46 2023 ; 11 h 34 min 26 s 934.14 ms remaining ; 2 d 13 min 32 s 225.34 ms total) Fri Nov 10 17:30:55 2023: Iterated ≈78% of D-proof candidates. [2195695060 of 2814993667] (ETC: Sat Nov 11 04:05:26 2023 ; 10 h 34 min 31 s 530.90 ms remaining ; 2 d 4 min 12 s 413.12 ms total) Fri Nov 10 18:21:20 2023: Iterated ≈80% of D-proof candidates. [2251994933 of 2814993667] (ETC: Sat Nov 11 03:56:21 2023 ; 9 h 35 min 1 s 457.87 ms remaining ; 1 d 23 h 55 min 7 s 289.17 ms total) Fri Nov 10 19:10:51 2023: Iterated ≈82% of D-proof candidates. [2308294806 of 2814993667] (ETC: Sat Nov 11 03:46:37 2023 ; 8 h 35 min 46 s 254.51 ms remaining ; 1 d 23 h 45 min 23 s 635.87 ms total) Fri Nov 10 19:59:20 2023: Iterated ≈84% of D-proof candidates. [2364594680 of 2814993667] (ETC: Sat Nov 11 03:36:07 2023 ; 7 h 36 min 46 s 936.44 ms remaining ; 1 d 23 h 34 min 53 s 352.65 ms total) Fri Nov 10 20:47:23 2023: Iterated ≈86% of D-proof candidates. [2420894553 of 2814993667] (ETC: Sat Nov 11 03:25:35 2023 ; 6 h 38 min 12 s 643.62 ms remaining ; 1 d 23 h 24 min 21 s 739.84 ms total) Fri Nov 10 21:35:13 2023: Iterated ≈88% of D-proof candidates. [2477194426 of 2814993667] (ETC: Sat Nov 11 03:15:19 2023 ; 5 h 40 min 5 s 410.56 ms remaining ; 1 d 23 h 14 min 5 s 87.49 ms total) Fri Nov 10 22:22:49 2023: Iterated ≈90% of D-proof candidates. [2533494300 of 2814993667] (ETC: Sat Nov 11 03:05:13 2023 ; 4 h 42 min 23 s 888.60 ms remaining ; 1 d 23 h 3 min 58 s 885.82 ms total) Fri Nov 10 23:09:57 2023: Iterated ≈92% of D-proof candidates. [2589794173 of 2814993667] (ETC: Sat Nov 11 02:55:03 2023 ; 3 h 45 min 6 s 331.55 ms remaining ; 1 d 22 h 53 min 49 s 143.83 ms total) Fri Nov 10 23:56:47 2023: Iterated ≈94% of D-proof candidates. [2646094046 of 2814993667] (ETC: Sat Nov 11 02:45:00 2023 ; 2 h 48 min 13 s 604.11 ms remaining ; 1 d 22 h 43 min 46 s 734.26 ms total) Sat Nov 11 00:43:24 2023: Iterated ≈96% of D-proof candidates. [2702393920 of 2814993667] (ETC: Sat Nov 11 02:35:09 2023 ; 1 h 51 min 45 s 416.76 ms remaining ; 1 d 22 h 33 min 55 s 418.61 ms total) Sat Nov 11 01:30:15 2023: Iterated ≈98% of D-proof candidates. [2758693793 of 2814993667] (ETC: Sat Nov 11 02:25:56 2023 ; 55 min 41 s 650.43 ms remaining ; 1 d 22 h 24 min 42 s 519.50 ms total) Sat Nov 11 02:17:18 2023: Iterated 100% of D-proof candidates. [2814993667 of 2814993667] (ETC: Sat Nov 11 02:17:18 2023 ; 0.00 ms remaining ; 1 d 22 h 16 min 4 s 424.63 ms total) 166566805.56 ms (1 d 22 h 16 min 6 s 805.57 ms) taken to collect 253992520 D-proofs of length 159. [iterated 2814993667 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 }, { 159, 2814993667 } } 2339183.44 ms (38 min 59 s 183.44 ms) taken to filter and order new representative proofs. Found 253992520 representative, 1105095636 redundant, and 1455905511 invalid condensed detachment proof strings. lengths up to 159 ; 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), (159,253992520)} ; 253992520 new representative proofs (1105095636 redundant, 1455905511 invalid) Sat Nov 11 03:33:09 2023: Starting to write 253992520 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs159-unfiltered141+.txt. 358991.77 ms (5 min 58 s 991.77 ms) taken to print and save 98773762822 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs159-unfiltered141+.txt. Sat Nov 11 03:44:38 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 159, unfiltered] Sat Nov 11 03:58:19 2023: Process terminated. [pid: 63158, tid:23383611914112]