( 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: 69.05111… h CPU utilization: 4419.27111… core-h ) Sat Nov 11 12:24:33 2023: Process started. [pid: 42171, tid:22773566412672] Tasks: 1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true) 2. generateDProofRepresentativeFiles(161, 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(161, false, true). Sat Nov 11 12:24:33 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 161, unfiltered] 0.04 ms taken to load initial representatives. 0.21 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:22773501961984] 0.15 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:22773497759488] 1.48 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:22773485152000] 2.30 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:22773506164480] 2.10 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:22773487253248] 10861.38 ms (10 s 861.38 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:22773506164480] 2.13 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:22773504063232] 9266.51 ms (9 s 266.51 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:22773501961984] 6.21 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:22773499860736] 10777.45 ms (10 s 777.45 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:22773497759488] 27.15 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:22773495658240] 5.91 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:22773493556992] 21.81 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:22773491455744] 174.06 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:22773489354496] 11575.83 ms (11 s 575.83 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:22773487253248] 10661.26 ms (10 s 661.25 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:22773485152000] 6.74 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:22773483050752] 5.95 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:22773480949504] 8.33 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:22773478848256] 18.26 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:22773476747008] 18.15 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:22773474645760] 5.96 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:22773472544512] 2.53 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:22773470443264] 1.86 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:22773468342016] 1.68 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:22773466240768] 55.53 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:22773464139520] 33.37 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:22772185036544] 656.66 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:22772182935296] 12.53 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:22772180834048] 6.39 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:22772178732800] 6.03 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:22772176631552] 28.28 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:22772174530304] 78.38 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:22772172429056] 11.54 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:22772170327808] 1282.73 ms (1 s 282.73 ms) taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:22772168226560] 21.80 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:22772166125312] 11.93 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:22772164024064] 27.98 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:22772161922816] 712.90 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:22772159821568] 52.45 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:22772157720320] 271.82 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:22772155619072] 144.40 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:22772153517824] 40.61 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:22772151416576] 373.65 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:22772149315328] 226.87 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:22772147214080] 144.30 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:22772145112832] 956.58 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:22772143011584] 604.34 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:22772140910336] 756.93 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:22772138809088] 306.40 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:22772136707840] 919.13 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:22772134606592] 761.51 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:22772132505344] 581.43 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:22772130404096] 1086.77 ms (1 s 86.77 ms) taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:22772128302848] 859.20 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:22772126201600] 726.34 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:22772124100352] 1165.59 ms (1 s 165.59 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:22772121999104] 1069.34 ms (1 s 69.34 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:22771782383360] 1677.58 ms (1 s 677.58 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:22771780282112] 5115.43 ms (5 s 115.43 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:22771778180864] 8244.46 ms (8 s 244.46 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:22771776079616] 3347.63 ms (3 s 347.63 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:22771773978368] 4125.27 ms (4 s 125.27 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:22771771877120] 3848.50 ms (3 s 848.50 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:22771769775872] 5154.01 ms (5 s 154.00 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:22771767674624] 2664.98 ms (2 s 664.98 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:22771765573376] 6601.33 ms (6 s 601.33 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:22771763472128] 7270.97 ms (7 s 270.97 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:22771761370880] 8470.32 ms (8 s 470.32 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:22771759269632] 11733.37 ms (11 s 733.37 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. 85831.29 ms (1 min 25 s 831.30 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:22771759269632] 139949.69 ms (2 min 19 s 949.69 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:22771761370880] 192539.35 ms (3 min 12 s 539.35 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:22771763472128] 240489.78 ms (4 min 489.78 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:22771765573376] 296535.17 ms (4 min 56 s 535.17 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:22771767674624] 348752.49 ms (5 min 48 s 752.49 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:22771769775872] 393509.30 ms (6 min 33 s 509.30 ms) taken to read 109705510 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs153-unfiltered141+.txt. [tid:22771771877120] 438112.51 ms (7 min 18 s 112.51 ms) taken to read 144348401 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs155-unfiltered141+.txt. [tid:22771773978368] 472636.50 ms (7 min 52 s 636.50 ms) taken to read 192661720 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. [tid:22771776079616] 506738.99 ms (8 min 26 s 739.00 ms) taken to read 253992520 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs159-unfiltered141+.txt. [tid:22771778180864] 506768.33 ms (8 min 26 s 768.33 ms) additional read duration. Loaded 10 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 147 : 47814846 149 : 62366737 151 : 82234537 153 : 109705510 155 : 144348401 157 : 192661720 159 : 253992520 997399704 representatives in total. Sat Nov 11 12:34:36 2023: Inserted ≈ 5% of D-proof conclusions. [ 49869985 of 997399704] (ETC: Sat Nov 11 13:01:30 2023 ; 26 min 53 s 753.85 ms remaining ; 28 min 18 s 688.27 ms total) Sat Nov 11 12:35:52 2023: Inserted ≈10% of D-proof conclusions. [ 99739970 of 997399704] (ETC: Sat Nov 11 12:59:57 2023 ; 24 min 4 s 950.44 ms remaining ; 26 min 45 s 500.49 ms total) Sat Nov 11 12:37:13 2023: Inserted ≈15% of D-proof conclusions. [149609955 of 997399704] (ETC: Sat Nov 11 13:00:01 2023 ; 22 min 48 s 198.06 ms remaining ; 26 min 49 s 644.77 ms total) Sat Nov 11 12:38:39 2023: Inserted ≈20% of D-proof conclusions. [199479940 of 997399704] (ETC: Sat Nov 11 13:00:30 2023 ; 21 min 51 s 327.46 ms remaining ; 27 min 19 s 159.33 ms total) Sat Nov 11 12:40:23 2023: Inserted ≈25% of D-proof conclusions. [249349926 of 997399704] (ETC: Sat Nov 11 13:01:57 2023 ; 21 min 34 s 361.45 ms remaining ; 28 min 45 s 815.27 ms total) Sat Nov 11 12:42:02 2023: Inserted ≈30% of D-proof conclusions. [299219911 of 997399704] (ETC: Sat Nov 11 13:02:41 2023 ; 20 min 38 s 875.08 ms remaining ; 29 min 29 s 821.54 ms total) Sat Nov 11 12:43:49 2023: Inserted ≈35% of D-proof conclusions. [349089896 of 997399704] (ETC: Sat Nov 11 13:03:34 2023 ; 19 min 44 s 635.71 ms remaining ; 30 min 22 s 516.47 ms total) Sat Nov 11 12:45:24 2023: Inserted ≈40% of D-proof conclusions. [398959881 of 997399704] (ETC: Sat Nov 11 13:03:44 2023 ; 18 min 19 s 460.19 ms remaining ; 30 min 32 s 433.64 ms total) Sat Nov 11 12:46:50 2023: Inserted ≈45% of D-proof conclusions. [448829866 of 997399704] (ETC: Sat Nov 11 13:03:31 2023 ; 16 min 40 s 833.74 ms remaining ; 30 min 19 s 697.70 ms total) Sat Nov 11 12:48:22 2023: Inserted ≈50% of D-proof conclusions. [498699852 of 997399704] (ETC: Sat Nov 11 13:03:34 2023 ; 15 min 11 s 174.27 ms remaining ; 30 min 22 s 348.54 ms total) Sat Nov 11 12:50:14 2023: Inserted ≈55% of D-proof conclusions. [548569837 of 997399704] (ETC: Sat Nov 11 13:04:10 2023 ; 13 min 56 s 564.73 ms remaining ; 30 min 59 s 32.73 ms total) Sat Nov 11 12:51:30 2023: Inserted ≈60% of D-proof conclusions. [598439822 of 997399704] (ETC: Sat Nov 11 13:03:42 2023 ; 12 min 12 s 404.80 ms remaining ; 30 min 31 s 12.00 ms total) Sat Nov 11 12:52:49 2023: Inserted ≈65% of D-proof conclusions. [648309807 of 997399704] (ETC: Sat Nov 11 13:03:24 2023 ; 10 min 34 s 437.39 ms remaining ; 30 min 12 s 678.27 ms total) Sat Nov 11 12:54:27 2023: Inserted ≈70% of D-proof conclusions. [698179792 of 997399704] (ETC: Sat Nov 11 13:03:34 2023 ; 9 min 6 s 971.15 ms remaining ; 30 min 23 s 237.15 ms total) Sat Nov 11 12:56:13 2023: Inserted ≈75% of D-proof conclusions. [748049778 of 997399704] (ETC: Sat Nov 11 13:03:53 2023 ; 7 min 40 s 508.16 ms remaining ; 30 min 42 s 32.64 ms total) Sat Nov 11 12:57:36 2023: Inserted ≈80% of D-proof conclusions. [797919763 of 997399704] (ETC: Sat Nov 11 13:03:42 2023 ; 6 min 6 s 181.09 ms remaining ; 30 min 30 s 905.43 ms total) Sat Nov 11 12:59:02 2023: Inserted ≈85% of D-proof conclusions. [847789748 of 997399704] (ETC: Sat Nov 11 13:03:35 2023 ; 4 min 33 s 603.89 ms remaining ; 30 min 24 s 25.93 ms total) Sat Nov 11 13:00:35 2023: Inserted ≈90% of D-proof conclusions. [897659733 of 997399704] (ETC: Sat Nov 11 13:03:38 2023 ; 3 min 2 s 643.20 ms remaining ; 30 min 26 s 432.03 ms total) Sat Nov 11 13:02:18 2023: Inserted ≈95% of D-proof conclusions. [947529718 of 997399704] (ETC: Sat Nov 11 13:03:50 2023 ; 1 min 31 s 941.34 ms remaining ; 30 min 38 s 826.81 ms total) Sat Nov 11 13:03:38 2023: Inserted 100% of D-proof conclusions. [997399704 of 997399704] (ETC: Sat Nov 11 13:03:38 2023 ; 0.00 ms remaining ; 30 min 26 s 623.99 ms total) 1826628.70 ms (30 min 26 s 628.70 ms) total insertion duration. Known iteration count loaded from 161:3806955248. Sat Nov 11 13:03:38 2023: Starting to generate D-proof representatives of length 161. Sat Nov 11 14:26:49 2023: Iterated ≈ 2% of D-proof candidates. [ 76139104 of 3806955248] (ETC: Tue Nov 14 10:22:51 2023 ; 2 d 19 h 56 min 1 s 611.81 ms remaining ; 2 d 21 h 19 min 12 s 665.05 ms total) Sat Nov 11 15:46:01 2023: Iterated ≈ 4% of D-proof candidates. [ 152278209 of 3806955248] (ETC: Tue Nov 14 08:43:04 2023 ; 2 d 16 h 57 min 3 s 638.07 ms remaining ; 2 d 19 h 39 min 26 s 289.60 ms total) Sat Nov 11 17:03:59 2023: Iterated ≈ 6% of D-proof candidates. [ 228417314 of 3806955248] (ETC: Tue Nov 14 07:49:21 2023 ; 2 d 14 h 45 min 22 s 281.46 ms remaining ; 2 d 18 h 45 min 42 s 852.56 ms total) Sat Nov 11 18:36:06 2023: Iterated ≈ 8% of D-proof candidates. [ 304556419 of 3806955248] (ETC: Tue Nov 14 10:19:34 2023 ; 2 d 15 h 43 min 27 s 408.49 ms remaining ; 2 d 21 h 15 min 55 s 878.74 ms total) Sat Nov 11 20:10:08 2023: Iterated ≈10% of D-proof candidates. [ 380695524 of 3806955248] (ETC: Tue Nov 14 12:08:38 2023 ; 2 d 15 h 58 min 30 s 533.11 ms remaining ; 2 d 23 h 5 min 592.29 ms total) Sat Nov 11 21:33:37 2023: Iterated ≈12% of D-proof candidates. [ 456834629 of 3806955248] (ETC: Tue Nov 14 11:53:28 2023 ; 2 d 14 h 19 min 51 s 3.82 ms remaining ; 2 d 22 h 49 min 49 s 777.01 ms total) Sat Nov 11 23:04:00 2023: Iterated ≈14% of D-proof candidates. [ 532973734 of 3806955248] (ETC: Tue Nov 14 12:31:59 2023 ; 2 d 13 h 27 min 59 s 107.59 ms remaining ; 2 d 23 h 28 min 21 s 287.83 ms total) Sun Nov 12 00:46:32 2023: Iterated ≈16% of D-proof candidates. [ 609112839 of 3806955248] (ETC: Tue Nov 14 14:16:45 2023 ; 2 d 13 h 30 min 13 s 139.33 ms remaining ; 3 d 1 h 13 min 7 s 70.58 ms total) Sun Nov 12 02:12:45 2023: Iterated ≈18% of D-proof candidates. [ 685251944 of 3806955248] (ETC: Tue Nov 14 14:07:35 2023 ; 2 d 11 h 54 min 50 s 533.28 ms remaining ; 3 d 1 h 3 min 57 s 235.66 ms total) Sun Nov 12 03:49:47 2023: Iterated ≈20% of D-proof candidates. [ 761391049 of 3806955248] (ETC: Tue Nov 14 14:54:25 2023 ; 2 d 11 h 4 min 37 s 420.89 ms remaining ; 3 d 1 h 50 min 46 s 776.06 ms total) Sun Nov 12 05:15:09 2023: Iterated ≈22% of D-proof candidates. [ 837530154 of 3806955248] (ETC: Tue Nov 14 14:39:35 2023 ; 2 d 9 h 24 min 26 s 744.37 ms remaining ; 3 d 1 h 35 min 57 s 364.53 ms total) Sun Nov 12 06:37:19 2023: Iterated ≈24% of D-proof candidates. [ 913669259 of 3806955248] (ETC: Tue Nov 14 14:13:57 2023 ; 2 d 7 h 36 min 38 s 504.38 ms remaining ; 3 d 1 h 10 min 19 s 84.66 ms total) Sun Nov 12 08:10:06 2023: Iterated ≈26% of D-proof candidates. [ 989808364 of 3806955248] (ETC: Tue Nov 14 14:33:06 2023 ; 2 d 6 h 23 min 459.83 ms remaining ; 3 d 1 h 29 min 28 s 188.91 ms total) Sun Nov 12 09:34:24 2023: Iterated ≈28% of D-proof candidates. [1065947469 of 3806955248] (ETC: Tue Nov 14 14:19:12 2023 ; 2 d 4 h 44 min 48 s 747.97 ms remaining ; 3 d 1 h 15 min 34 s 372.14 ms total) Sun Nov 12 10:59:41 2023: Iterated ≈30% of D-proof candidates. [1142086574 of 3806955248] (ETC: Tue Nov 14 14:10:27 2023 ; 2 d 3 h 10 min 46 s 391.30 ms remaining ; 3 d 1 h 6 min 49 s 130.38 ms total) Sun Nov 12 12:26:23 2023: Iterated ≈32% of D-proof candidates. [1218225679 of 3806955248] (ETC: Tue Nov 14 14:07:14 2023 ; 2 d 1 h 40 min 51 s 8.09 ms remaining ; 3 d 1 h 3 min 36 s 188.33 ms total) Sun Nov 12 14:00:35 2023: Iterated ≈34% of D-proof candidates. [1294364784 of 3806955248] (ETC: Tue Nov 14 14:26:27 2023 ; 2 d 25 min 51 s 602.63 ms remaining ; 3 d 1 h 22 min 49 s 94.86 ms total) Sun Nov 12 15:24:09 2023: Iterated ≈36% of D-proof candidates. [1370503889 of 3806955248] (ETC: Tue Nov 14 14:13:57 2023 ; 1 d 22 h 49 min 47 s 924.01 ms remaining ; 3 d 1 h 10 min 18 s 631.24 ms total) Sun Nov 12 16:37:40 2023: Iterated ≈38% of D-proof candidates. [1446642994 of 3806955248] (ETC: Tue Nov 14 13:36:22 2023 ; 1 d 20 h 58 min 41 s 509.18 ms remaining ; 3 d 32 min 43 s 724.46 ms total) Sun Nov 12 18:05:34 2023: Iterated ≈40% of D-proof candidates. [1522782099 of 3806955248] (ETC: Tue Nov 14 13:38:28 2023 ; 1 d 19 h 32 min 54 s 324.54 ms remaining ; 3 d 34 min 50 s 540.88 ms total) Sun Nov 12 19:27:33 2023: Iterated ≈42% of D-proof candidates. [1598921204 of 3806955248] (ETC: Tue Nov 14 13:26:18 2023 ; 1 d 17 h 58 min 44 s 634.63 ms remaining ; 3 d 22 min 39 s 714.85 ms total) Sun Nov 12 20:48:28 2023: Iterated ≈44% of D-proof candidates. [1675060309 of 3806955248] (ETC: Tue Nov 14 13:12:49 2023 ; 1 d 16 h 24 min 20 s 453.42 ms remaining ; 3 d 9 min 10 s 809.67 ms total) Sun Nov 12 22:18:49 2023: Iterated ≈46% of D-proof candidates. [1751199414 of 3806955248] (ETC: Tue Nov 14 13:20:59 2023 ; 1 d 15 h 2 min 10 s 317.70 ms remaining ; 3 d 17 min 21 s 329.07 ms total) Sun Nov 12 23:43:40 2023: Iterated ≈48% of D-proof candidates. [1827338519 of 3806955248] (ETC: Tue Nov 14 13:17:02 2023 ; 1 d 13 h 33 min 21 s 974.10 ms remaining ; 3 d 13 min 23 s 796.33 ms total) Mon Nov 13 00:55:15 2023: Iterated ≈50% of D-proof candidates. [1903477624 of 3806955248] (ETC: Tue Nov 14 12:46:51 2023 ; 1 d 11 h 51 min 36 s 803.85 ms remaining ; 2 d 23 h 43 min 13 s 607.70 ms total) Mon Nov 13 02:16:34 2023: Iterated ≈52% of D-proof candidates. [1979616728 of 3806955248] (ETC: Tue Nov 14 12:37:44 2023 ; 1 d 10 h 21 min 10 s 242.82 ms remaining ; 2 d 23 h 34 min 6 s 339.07 ms total) Mon Nov 13 03:36:33 2023: Iterated ≈54% of D-proof candidates. [2055755833 of 3806955248] (ETC: Tue Nov 14 12:26:48 2023 ; 1 d 8 h 50 min 15 s 470.90 ms remaining ; 2 d 23 h 23 min 10 s 153.99 ms total) Mon Nov 13 04:55:00 2023: Iterated ≈56% of D-proof candidates. [2131894938 of 3806955248] (ETC: Tue Nov 14 12:13:56 2023 ; 1 d 7 h 18 min 56 s 28.00 ms remaining ; 2 d 23 h 10 min 18 s 245.31 ms total) Mon Nov 13 06:10:58 2023: Iterated ≈58% of D-proof candidates. [2208034043 of 3806955248] (ETC: Tue Nov 14 11:57:40 2023 ; 1 d 5 h 46 min 41 s 665.34 ms remaining ; 2 d 22 h 54 min 2 s 60.20 ms total) Mon Nov 13 07:31:29 2023: Iterated ≈60% of D-proof candidates. [2284173148 of 3806955248] (ETC: Tue Nov 14 11:50:03 2023 ; 1 d 4 h 18 min 33 s 937.57 ms remaining ; 2 d 22 h 46 min 24 s 843.78 ms total) Mon Nov 13 08:47:46 2023: Iterated ≈62% of D-proof candidates. [2360312253 of 3806955248] (ETC: Tue Nov 14 11:36:06 2023 ; 1 d 2 h 48 min 20 s 229.15 ms remaining ; 2 d 22 h 32 min 27 s 971.31 ms total) Mon Nov 13 10:05:22 2023: Iterated ≈64% of D-proof candidates. [2436451358 of 3806955248] (ETC: Tue Nov 14 11:25:05 2023 ; 1 d 1 h 19 min 43 s 365.69 ms remaining ; 2 d 22 h 21 min 27 s 126.79 ms total) Mon Nov 13 11:18:13 2023: Iterated ≈66% of D-proof candidates. [2512590463 of 3806955248] (ETC: Tue Nov 14 11:07:32 2023 ; 23 h 49 min 19 s 765.74 ms remaining ; 2 d 22 h 3 min 54 s 605.00 ms total) Mon Nov 13 12:31:58 2023: Iterated ≈68% of D-proof candidates. [2588729568 of 3806955248] (ETC: Tue Nov 14 10:52:21 2023 ; 22 h 20 min 23 s 436.53 ms remaining ; 2 d 21 h 48 min 43 s 239.02 ms total) Mon Nov 13 13:45:04 2023: Iterated ≈70% of D-proof candidates. [2664868673 of 3806955248] (ETC: Tue Nov 14 10:37:07 2023 ; 20 h 52 min 2 s 815.51 ms remaining ; 2 d 21 h 33 min 29 s 384.89 ms total) Mon Nov 13 14:59:00 2023: Iterated ≈72% of D-proof candidates. [2741007778 of 3806955248] (ETC: Tue Nov 14 10:23:52 2023 ; 19 h 24 min 51 s 959.70 ms remaining ; 2 d 21 h 20 min 14 s 141.67 ms total) Mon Nov 13 16:12:44 2023: Iterated ≈74% of D-proof candidates. [2817146883 of 3806955248] (ETC: Tue Nov 14 10:11:04 2023 ; 17 h 58 min 19 s 869.45 ms remaining ; 2 d 21 h 7 min 25 s 651.61 ms total) Mon Nov 13 17:25:13 2023: Iterated ≈76% of D-proof candidates. [2893285988 of 3806955248] (ETC: Tue Nov 14 09:57:17 2023 ; 16 h 32 min 4 s 627.04 ms remaining ; 2 d 20 h 53 min 39 s 279.19 ms total) Mon Nov 13 18:38:07 2023: Iterated ≈78% of D-proof candidates. [2969425093 of 3806955248] (ETC: Tue Nov 14 09:44:46 2023 ; 15 h 6 min 39 s 41.83 ms remaining ; 2 d 20 h 41 min 8 s 371.82 ms total) Mon Nov 13 19:50:11 2023: Iterated ≈80% of D-proof candidates. [3045564198 of 3806955248] (ETC: Tue Nov 14 09:31:49 2023 ; 13 h 41 min 38 s 202.13 ms remaining ; 2 d 20 h 28 min 11 s 10.50 ms total) Mon Nov 13 21:01:45 2023: Iterated ≈82% of D-proof candidates. [3121703303 of 3806955248] (ETC: Tue Nov 14 09:18:54 2023 ; 12 h 17 min 8 s 953.84 ms remaining ; 2 d 20 h 15 min 16 s 410.11 ms total) Mon Nov 13 22:11:45 2023: Iterated ≈84% of D-proof candidates. [3197842408 of 3806955248] (ETC: Tue Nov 14 09:04:43 2023 ; 10 h 52 min 58 s 465.88 ms remaining ; 2 d 20 h 1 min 5 s 411.62 ms total) Mon Nov 13 23:20:51 2023: Iterated ≈86% of D-proof candidates. [3273981513 of 3806955248] (ETC: Tue Nov 14 08:50:10 2023 ; 9 h 29 min 18 s 889.51 ms remaining ; 2 d 19 h 46 min 32 s 67.78 ms total) Tue Nov 14 00:30:17 2023: Iterated ≈88% of D-proof candidates. [3350120618 of 3806955248] (ETC: Tue Nov 14 08:36:39 2023 ; 8 h 6 min 21 s 715.93 ms remaining ; 2 d 19 h 33 min 965.94 ms total) Tue Nov 14 01:39:22 2023: Iterated ≈90% of D-proof candidates. [3426259723 of 3806955248] (ETC: Tue Nov 14 08:23:19 2023 ; 6 h 43 min 58 s 152.37 ms remaining ; 2 d 19 h 19 min 41 s 523.54 ms total) Tue Nov 14 02:47:55 2023: Iterated ≈92% of D-proof candidates. [3502398828 of 3806955248] (ETC: Tue Nov 14 08:10:01 2023 ; 5 h 22 min 6 s 673.83 ms remaining ; 2 d 19 h 6 min 23 s 422.77 ms total) Tue Nov 14 03:56:00 2023: Iterated ≈94% of D-proof candidates. [3578537933 of 3806955248] (ETC: Tue Nov 14 07:56:47 2023 ; 4 h 47 s 360.30 ms remaining ; 2 d 18 h 53 min 9 s 338.21 ms total) Tue Nov 14 05:04:09 2023: Iterated ≈96% of D-proof candidates. [3654677038 of 3806955248] (ETC: Tue Nov 14 07:44:11 2023 ; 2 h 40 min 1 s 311.09 ms remaining ; 2 d 18 h 40 min 32 s 777.14 ms total) Tue Nov 14 06:12:18 2023: Iterated ≈98% of D-proof candidates. [3730816143 of 3806955248] (ETC: Tue Nov 14 07:32:04 2023 ; 1 h 19 min 46 s 123.35 ms remaining ; 2 d 18 h 28 min 26 s 167.53 ms total) Tue Nov 14 07:20:51 2023: Iterated 100% of D-proof candidates. [3806955248 of 3806955248] (ETC: Tue Nov 14 07:20:51 2023 ; 0.00 ms remaining ; 2 d 18 h 17 min 13 s 538.44 ms total) 238635826.19 ms (2 d 18 h 17 min 15 s 826.20 ms) taken to collect 338777355 D-proofs of length 161. [iterated 3806955248 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 }, { 161, 3806955248 } } 2961416.65 ms (49 min 21 s 416.65 ms) taken to filter and order new representative proofs. Found 338777355 representative, 1508534665 redundant, and 1959643228 invalid condensed detachment proof strings. lengths up to 161 ; 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), (161,338777355)} ; 338777355 new representative proofs (1508534665 redundant, 1959643228 invalid) Tue Nov 14 08:53:11 2023: Starting to write 338777355 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs161-unfiltered141+.txt. 488866.59 ms (8 min 8 s 866.59 ms) taken to print and save 133862174308 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs161-unfiltered141+.txt. Tue Nov 14 09:09:46 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 161, unfiltered] Tue Nov 14 09:27:37 2023: Process terminated. [pid: 42171, tid:22773566412672]