( 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: 5.8791666… h CPU utilization: 376.2666… core-h ) Thu Oct 26 19:31:39 2023: Process started. [pid: 29350, tid:23209699268480] Tasks: 1. resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true) 2. generateDProofRepresentativeFiles(147, false, true) [Main] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 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(147, false, true). Thu Oct 26 19:31:39 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 147, unfiltered] 0.00 ms taken to load initial representatives. 0.08 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23209639020288] 0.03 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23209636919040] 0.00 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23209630615296] 4.13 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23209634817792] 4.61 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23208518465280] 8589.20 ms (8 s 589.20 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23209639020288] 9665.20 ms (9 s 665.20 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23209636919040] 10378.49 ms (10 s 378.49 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23209634817792] 3.55 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23209632716544] 10021.74 ms (10 s 21.74 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23209630615296] 0.25 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23209628514048] 9.91 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23209626412800] 8.18 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23209624311552] 11.37 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23209622210304] 7.25 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23209620109056] 11.56 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23209618007808] 3.88 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23209615906560] 9.68 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23209613805312] 3.49 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23209611704064] 3.49 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23209609602816] 10.09 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23209607501568] 4.59 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23209605400320] 3.15 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23209603299072] 11.27 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23208526870272] 11.94 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23208524769024] 10.77 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23208522667776] 6.48 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23208520566528] 10893.90 ms (10 s 893.90 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23208518465280] 3.26 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23208516364032] 23.31 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23208514262784] 12.75 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23208512161536] 2.09 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23208510060288] 1.99 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23208507959040] 2.01 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23208505857792] 124.80 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23208503756544] 3.30 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23208501655296] 15.20 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23208499554048] 274.61 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23208497452800] 265.38 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23208495351552] 907.21 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23208493250304] 26.60 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23208491149056] 46.38 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23208489047808] 21.75 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23208486946560] 37.04 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23208484845312] 535.73 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23208482744064] 46.89 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23208480642816] 43.43 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23208478541568] 108.06 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23208476440320] 262.24 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23208474339072] 159.98 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23208472237824] 162.17 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23208470136576] 365.01 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23208468035328] 1030.72 ms (1 s 30.72 ms) taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23208465934080] 1115.56 ms (1 s 115.56 ms) taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23208463832832] 668.19 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23207453128448] 771.43 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23207451027200] 1733.90 ms (1 s 733.90 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23207448925952] 1271.27 ms (1 s 271.27 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23207446824704] 2222.85 ms (2 s 222.85 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23207444723456] 5276.86 ms (5 s 276.86 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23207442622208] 6946.30 ms (6 s 946.30 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23207440520960] 1878.09 ms (1 s 878.09 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23207438419712] 3568.30 ms (3 s 568.30 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23207436318464] 4731.42 ms (4 s 731.42 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23207434217216] 4520.68 ms (4 s 520.68 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23207432115968] 3985.63 ms (3 s 985.63 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23207430014720] 5759.70 ms (5 s 759.70 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23207427913472] 7370.91 ms (7 s 370.92 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23207425812224] 7760.29 ms (7 s 760.29 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23207423710976] 11054.83 ms (11 s 54.83 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. 15220.59 ms (15 s 220.59 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23207423710976] 20771.69 ms (20 s 771.69 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23207425812224] 25975.85 ms (25 s 975.85 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23207427913472] 25981.67 ms (25 s 981.67 ms) additional read duration. Loaded 3 more representative collections of sizes: 141 : 16952082 143 : 26431403 145 : 36855440 104275433 representatives in total. Thu Oct 26 19:32:22 2023: Inserted ≈ 5% of D-proof conclusions. [ 5213771 of 104275433] (ETC: Thu Oct 26 19:34:19 2023 ; 1 min 56 s 806.28 ms remaining ; 2 min 2 s 953.98 ms total) Thu Oct 26 19:32:28 2023: Inserted ≈10% of D-proof conclusions. [ 10427543 of 104275433] (ETC: Thu Oct 26 19:34:15 2023 ; 1 min 46 s 789.97 ms remaining ; 1 min 58 s 655.52 ms total) Thu Oct 26 19:32:33 2023: Inserted ≈15% of D-proof conclusions. [ 15641314 of 104275433] (ETC: Thu Oct 26 19:34:11 2023 ; 1 min 37 s 503.15 ms remaining ; 1 min 54 s 709.59 ms total) Thu Oct 26 19:32:39 2023: Inserted ≈20% of D-proof conclusions. [ 20855086 of 104275433] (ETC: Thu Oct 26 19:34:12 2023 ; 1 min 32 s 491.14 ms remaining ; 1 min 55 s 613.92 ms total) Thu Oct 26 19:32:45 2023: Inserted ≈25% of D-proof conclusions. [ 26068858 of 104275433] (ETC: Thu Oct 26 19:34:11 2023 ; 1 min 26 s 143.85 ms remaining ; 1 min 54 s 858.47 ms total) Thu Oct 26 19:32:50 2023: Inserted ≈30% of D-proof conclusions. [ 31282629 of 104275433] (ETC: Thu Oct 26 19:34:10 2023 ; 1 min 19 s 838.55 ms remaining ; 1 min 54 s 55.06 ms total) Thu Oct 26 19:32:56 2023: Inserted ≈35% of D-proof conclusions. [ 36496401 of 104275433] (ETC: Thu Oct 26 19:34:10 2023 ; 1 min 14 s 412.12 ms remaining ; 1 min 54 s 480.18 ms total) Thu Oct 26 19:33:02 2023: Inserted ≈40% of D-proof conclusions. [ 41710173 of 104275433] (ETC: Thu Oct 26 19:34:12 2023 ; 1 min 9 s 643.86 ms remaining ; 1 min 56 s 73.10 ms total) Thu Oct 26 19:33:08 2023: Inserted ≈45% of D-proof conclusions. [ 46923944 of 104275433] (ETC: Thu Oct 26 19:34:12 2023 ; 1 min 3 s 737.80 ms remaining ; 1 min 55 s 886.90 ms total) Thu Oct 26 19:33:14 2023: Inserted ≈50% of D-proof conclusions. [ 52137716 of 104275433] (ETC: Thu Oct 26 19:34:12 2023 ; 58 s 225.54 ms remaining ; 1 min 56 s 451.08 ms total) Thu Oct 26 19:33:21 2023: Inserted ≈55% of D-proof conclusions. [ 57351488 of 104275433] (ETC: Thu Oct 26 19:34:14 2023 ; 53 s 18.80 ms remaining ; 1 min 57 s 819.55 ms total) Thu Oct 26 19:33:28 2023: Inserted ≈60% of D-proof conclusions. [ 62565259 of 104275433] (ETC: Thu Oct 26 19:34:16 2023 ; 47 s 942.12 ms remaining ; 1 min 59 s 855.29 ms total) Thu Oct 26 19:33:35 2023: Inserted ≈65% of D-proof conclusions. [ 67779031 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 42 s 648.62 ms remaining ; 2 min 1 s 853.21 ms total) Thu Oct 26 19:33:41 2023: Inserted ≈70% of D-proof conclusions. [ 72992803 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 36 s 600.03 ms remaining ; 2 min 2 s 0.09 ms total) Thu Oct 26 19:33:47 2023: Inserted ≈75% of D-proof conclusions. [ 78206574 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 30 s 496.99 ms remaining ; 2 min 1 s 987.96 ms total) Thu Oct 26 19:33:53 2023: Inserted ≈80% of D-proof conclusions. [ 83420346 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 24 s 378.49 ms remaining ; 2 min 1 s 892.46 ms total) Thu Oct 26 19:34:00 2023: Inserted ≈85% of D-proof conclusions. [ 88634118 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 18 s 288.10 ms remaining ; 2 min 1 s 920.67 ms total) Thu Oct 26 19:34:05 2023: Inserted ≈90% of D-proof conclusions. [ 93847889 of 104275433] (ETC: Thu Oct 26 19:34:18 2023 ; 12 s 172.87 ms remaining ; 2 min 1 s 728.66 ms total) Thu Oct 26 19:34:11 2023: Inserted ≈95% of D-proof conclusions. [ 99061661 of 104275433] (ETC: Thu Oct 26 19:34:17 2023 ; 6 s 69.15 ms remaining ; 2 min 1 s 382.92 ms total) Thu Oct 26 19:34:17 2023: Inserted 100% of D-proof conclusions. [104275433 of 104275433] (ETC: Thu Oct 26 19:34:17 2023 ; 0.00 ms remaining ; 2 min 1 s 79.87 ms total) 121080.53 ms (2 min 1 s 80.53 ms) total insertion duration. Known iteration count loaded from 147:453382622. Thu Oct 26 19:34:17 2023: Starting to generate D-proof representatives of length 147. Thu Oct 26 19:42:02 2023: Iterated ≈ 2% of D-proof candidates. [ 9067652 of 453382622] (ETC: Fri Oct 27 02:01:54 2023 ; 6 h 19 min 51 s 467.27 ms remaining ; 6 h 27 min 36 s 599.23 ms total) Thu Oct 26 19:49:23 2023: Iterated ≈ 4% of D-proof candidates. [ 18135304 of 453382622] (ETC: Fri Oct 27 01:51:43 2023 ; 6 h 2 min 19 s 767.83 ms remaining ; 6 h 17 min 25 s 591.45 ms total) Thu Oct 26 19:56:22 2023: Iterated ≈ 6% of D-proof candidates. [ 27202957 of 453382622] (ETC: Fri Oct 27 01:42:15 2023 ; 5 h 45 min 53 s 85.40 ms remaining ; 6 h 7 min 57 s 750.41 ms total) Thu Oct 26 20:03:17 2023: Iterated ≈ 8% of D-proof candidates. [ 36270609 of 453382622] (ETC: Fri Oct 27 01:36:48 2023 ; 5 h 33 min 30 s 625.32 ms remaining ; 6 h 2 min 30 s 679.65 ms total) Thu Oct 26 20:11:29 2023: Iterated ≈10% of D-proof candidates. [ 45338262 of 453382622] (ETC: Fri Oct 27 01:46:20 2023 ; 5 h 34 min 50 s 823.15 ms remaining ; 6 h 12 min 3 s 136.83 ms total) Thu Oct 26 20:19:15 2023: Iterated ≈12% of D-proof candidates. [ 54405914 of 453382622] (ETC: Fri Oct 27 01:49:03 2023 ; 5 h 29 min 47 s 492.74 ms remaining ; 6 h 14 min 45 s 787.17 ms total) Thu Oct 26 20:26:05 2023: Iterated ≈14% of D-proof candidates. [ 63473567 of 453382622] (ETC: Fri Oct 27 01:44:16 2023 ; 5 h 18 min 10 s 933.18 ms remaining ; 6 h 9 min 58 s 759.51 ms total) Thu Oct 26 20:32:37 2023: Iterated ≈16% of D-proof candidates. [ 72541219 of 453382622] (ETC: Fri Oct 27 01:38:54 2023 ; 5 h 6 min 16 s 352.06 ms remaining ; 6 h 4 min 36 s 609.57 ms total) Thu Oct 26 20:40:49 2023: Iterated ≈18% of D-proof candidates. [ 81608871 of 453382622] (ETC: Fri Oct 27 01:43:57 2023 ; 5 h 3 min 7 s 464.61 ms remaining ; 6 h 9 min 39 s 834.84 ms total) Thu Oct 26 20:48:13 2023: Iterated ≈20% of D-proof candidates. [ 90676524 of 453382622] (ETC: Fri Oct 27 01:43:57 2023 ; 4 h 55 min 44 s 357.04 ms remaining ; 6 h 9 min 40 s 446.27 ms total) Thu Oct 26 20:54:54 2023: Iterated ≈22% of D-proof candidates. [ 99744176 of 453382622] (ETC: Fri Oct 27 01:40:45 2023 ; 4 h 45 min 50 s 810.53 ms remaining ; 6 h 6 min 28 s 218.58 ms total) Thu Oct 26 21:02:59 2023: Iterated ≈24% of D-proof candidates. [108811829 of 453382622] (ETC: Fri Oct 27 01:43:53 2023 ; 4 h 40 min 53 s 788.13 ms remaining ; 6 h 9 min 36 s 36.99 ms total) Thu Oct 26 21:10:04 2023: Iterated ≈26% of D-proof candidates. [117879481 of 453382622] (ETC: Fri Oct 27 01:42:42 2023 ; 4 h 32 min 37 s 438.43 ms remaining ; 6 h 8 min 24 s 646.47 ms total) Thu Oct 26 21:16:39 2023: Iterated ≈28% of D-proof candidates. [126947134 of 453382622] (ETC: Fri Oct 27 01:39:54 2023 ; 4 h 23 min 14 s 471.07 ms remaining ; 6 h 5 min 36 s 765.36 ms total) Thu Oct 26 21:24:18 2023: Iterated ≈30% of D-proof candidates. [136014786 of 453382622] (ETC: Fri Oct 27 01:40:59 2023 ; 4 h 16 min 41 s 670.20 ms remaining ; 6 h 6 min 42 s 385.95 ms total) Thu Oct 26 21:31:10 2023: Iterated ≈32% of D-proof candidates. [145082439 of 453382622] (ETC: Fri Oct 27 01:39:32 2023 ; 4 h 8 min 22 s 424.44 ms remaining ; 6 h 5 min 15 s 330.06 ms total) Thu Oct 26 21:38:22 2023: Iterated ≈34% of D-proof candidates. [154150091 of 453382622] (ETC: Fri Oct 27 01:39:15 2023 ; 4 h 52 s 922.32 ms remaining ; 6 h 4 min 58 s 367.12 ms total) Thu Oct 26 21:45:37 2023: Iterated ≈36% of D-proof candidates. [163217743 of 453382622] (ETC: Fri Oct 27 01:39:06 2023 ; 3 h 53 min 28 s 820.74 ms remaining ; 6 h 4 min 48 s 782.34 ms total) Thu Oct 26 21:53:18 2023: Iterated ≈38% of D-proof candidates. [172285396 of 453382622] (ETC: Fri Oct 27 01:40:08 2023 ; 3 h 46 min 49 s 676.04 ms remaining ; 6 h 5 min 51 s 90.35 ms total) Thu Oct 26 22:00:07 2023: Iterated ≈40% of D-proof candidates. [181353048 of 453382622] (ETC: Fri Oct 27 01:38:51 2023 ; 3 h 38 min 44 s 663.40 ms remaining ; 6 h 4 min 34 s 438.94 ms total) Thu Oct 26 22:06:28 2023: Iterated ≈42% of D-proof candidates. [190420701 of 453382622] (ETC: Fri Oct 27 01:36:37 2023 ; 3 h 30 min 9 s 450.95 ms remaining ; 6 h 2 min 20 s 432.65 ms total) Thu Oct 26 22:13:26 2023: Iterated ≈44% of D-proof candidates. [199488353 of 453382622] (ETC: Fri Oct 27 01:36:00 2023 ; 3 h 22 min 33 s 819.31 ms remaining ; 6 h 1 min 43 s 248.71 ms total) Thu Oct 26 22:20:57 2023: Iterated ≈46% of D-proof candidates. [208556006 of 453382622] (ETC: Fri Oct 27 01:36:37 2023 ; 3 h 15 min 39 s 578.62 ms remaining ; 6 h 2 min 19 s 960.40 ms total) Thu Oct 26 22:27:54 2023: Iterated ≈48% of D-proof candidates. [217623658 of 453382622] (ETC: Fri Oct 27 01:35:58 2023 ; 3 h 8 min 4 s 698.38 ms remaining ; 6 h 1 min 41 s 342.99 ms total) Thu Oct 26 22:34:47 2023: Iterated ≈50% of D-proof candidates. [226691311 of 453382622] (ETC: Fri Oct 27 01:35:17 2023 ; 3 h 30 s 229.35 ms remaining ; 6 h 1 min 458.70 ms total) Thu Oct 26 22:41:37 2023: Iterated ≈52% of D-proof candidates. [235758963 of 453382622] (ETC: Fri Oct 27 01:34:32 2023 ; 2 h 52 min 55 s 294.59 ms remaining ; 6 h 15 s 197.02 ms total) Thu Oct 26 22:48:27 2023: Iterated ≈54% of D-proof candidates. [244826615 of 453382622] (ETC: Fri Oct 27 01:33:50 2023 ; 2 h 45 min 23 s 802.13 ms remaining ; 5 h 59 min 33 s 482.80 ms total) Thu Oct 26 22:55:19 2023: Iterated ≈56% of D-proof candidates. [253894268 of 453382622] (ETC: Fri Oct 27 01:33:16 2023 ; 2 h 37 min 56 s 988.15 ms remaining ; 5 h 58 min 58 s 609.41 ms total) Thu Oct 26 23:02:01 2023: Iterated ≈58% of D-proof candidates. [262961920 of 453382622] (ETC: Fri Oct 27 01:32:27 2023 ; 2 h 30 min 25 s 693.28 ms remaining ; 5 h 58 min 9 s 745.81 ms total) Thu Oct 26 23:08:35 2023: Iterated ≈60% of D-proof candidates. [272029573 of 453382622] (ETC: Fri Oct 27 01:31:27 2023 ; 2 h 22 min 51 s 967.98 ms remaining ; 5 h 57 min 9 s 919.91 ms total) Thu Oct 26 23:15:12 2023: Iterated ≈62% of D-proof candidates. [281097225 of 453382622] (ETC: Fri Oct 27 01:30:37 2023 ; 2 h 15 min 24 s 246.91 ms remaining ; 5 h 56 min 19 s 597.06 ms total) Thu Oct 26 23:21:41 2023: Iterated ≈64% of D-proof candidates. [290164878 of 453382622] (ETC: Fri Oct 27 01:29:36 2023 ; 2 h 7 min 54 s 902.77 ms remaining ; 5 h 55 min 19 s 174.34 ms total) Thu Oct 26 23:28:06 2023: Iterated ≈66% of D-proof candidates. [299232530 of 453382622] (ETC: Fri Oct 27 01:28:32 2023 ; 2 h 26 s 829.30 ms remaining ; 5 h 54 min 15 s 380.22 ms total) Thu Oct 26 23:34:31 2023: Iterated ≈68% of D-proof candidates. [308300182 of 453382622] (ETC: Fri Oct 27 01:27:33 2023 ; 1 h 53 min 2 s 868.17 ms remaining ; 5 h 53 min 16 s 462.89 ms total) Thu Oct 26 23:40:56 2023: Iterated ≈70% of D-proof candidates. [317367835 of 453382622] (ETC: Fri Oct 27 01:26:39 2023 ; 1 h 45 min 42 s 625.35 ms remaining ; 5 h 52 min 22 s 84.43 ms total) Thu Oct 26 23:47:24 2023: Iterated ≈72% of D-proof candidates. [326435487 of 453382622] (ETC: Fri Oct 27 01:25:50 2023 ; 1 h 38 min 26 s 106.38 ms remaining ; 5 h 51 min 33 s 236.93 ms total) Thu Oct 26 23:53:50 2023: Iterated ≈74% of D-proof candidates. [335503140 of 453382622] (ETC: Fri Oct 27 01:25:01 2023 ; 1 h 31 min 11 s 442.35 ms remaining ; 5 h 50 min 44 s 8.98 ms total) Fri Oct 27 00:00:14 2023: Iterated ≈76% of D-proof candidates. [344570792 of 453382622] (ETC: Fri Oct 27 01:24:13 2023 ; 1 h 23 min 59 s 88.26 ms remaining ; 5 h 49 min 56 s 200.94 ms total) Fri Oct 27 00:06:33 2023: Iterated ≈78% of D-proof candidates. [353638445 of 453382622] (ETC: Fri Oct 27 01:23:20 2023 ; 1 h 16 min 47 s 461.57 ms remaining ; 5 h 49 min 3 s 7.09 ms total) Fri Oct 27 00:12:47 2023: Iterated ≈80% of D-proof candidates. [362706097 of 453382622] (ETC: Fri Oct 27 01:22:24 2023 ; 1 h 9 min 37 s 435.28 ms remaining ; 5 h 48 min 7 s 176.25 ms total) Fri Oct 27 00:18:54 2023: Iterated ≈82% of D-proof candidates. [371773750 of 453382622] (ETC: Fri Oct 27 01:21:22 2023 ; 1 h 2 min 28 s 574.58 ms remaining ; 5 h 47 min 5 s 414.30 ms total) Fri Oct 27 00:25:03 2023: Iterated ≈84% of D-proof candidates. [380841402 of 453382622] (ETC: Fri Oct 27 01:20:26 2023 ; 55 min 23 s 90.72 ms remaining ; 5 h 46 min 9 s 316.89 ms total) Fri Oct 27 00:31:19 2023: Iterated ≈86% of D-proof candidates. [389909054 of 453382622] (ETC: Fri Oct 27 01:19:40 2023 ; 48 min 21 s 179.76 ms remaining ; 5 h 45 min 22 s 712.24 ms total) Fri Oct 27 00:37:31 2023: Iterated ≈88% of D-proof candidates. [398976707 of 453382622] (ETC: Fri Oct 27 01:18:52 2023 ; 41 min 20 s 958.36 ms remaining ; 5 h 44 min 34 s 652.87 ms total) Fri Oct 27 00:43:42 2023: Iterated ≈90% of D-proof candidates. [408044359 of 453382622] (ETC: Fri Oct 27 01:18:05 2023 ; 34 min 22 s 813.12 ms remaining ; 5 h 43 min 48 s 130.83 ms total) Fri Oct 27 00:49:48 2023: Iterated ≈92% of D-proof candidates. [417112012 of 453382622] (ETC: Fri Oct 27 01:17:14 2023 ; 27 min 26 s 139.02 ms remaining ; 5 h 42 min 56 s 737.58 ms total) Fri Oct 27 00:55:52 2023: Iterated ≈94% of D-proof candidates. [426179664 of 453382622] (ETC: Fri Oct 27 01:16:24 2023 ; 20 min 31 s 602.46 ms remaining ; 5 h 42 min 6 s 707.21 ms total) Fri Oct 27 01:01:58 2023: Iterated ≈96% of D-proof candidates. [435247317 of 453382622] (ETC: Fri Oct 27 01:15:37 2023 ; 13 min 39 s 206.72 ms remaining ; 5 h 41 min 20 s 168.01 ms total) Fri Oct 27 01:08:05 2023: Iterated ≈98% of D-proof candidates. [444314969 of 453382622] (ETC: Fri Oct 27 01:14:54 2023 ; 6 min 48 s 739.25 ms remaining ; 5 h 40 min 36 s 961.50 ms total) Fri Oct 27 01:14:19 2023: Iterated 100% of D-proof candidates. [453382622 of 453382622] (ETC: Fri Oct 27 01:14:19 2023 ; 0.00 ms remaining ; 5 h 40 min 1 s 523.28 ms total) 20402063.09 ms (5 h 40 min 2 s 63.09 ms) taken to collect 47814846 D-proofs of length 147. [iterated 453382622 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 } } 288955.52 ms (4 min 48 s 955.52 ms) taken to filter and order new representative proofs. Found 47814846 representative, 180129243 redundant, and 225438533 invalid condensed detachment proof strings. lengths up to 147 ; 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)} ; 47814846 new representative proofs (180129243 redundant, 225438533 invalid) Fri Oct 27 01:21:37 2023: Starting to write 47814846 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. 48139.62 ms (48 s 139.62 ms) taken to print and save 16130023412 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. Fri Oct 27 01:23:08 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 147, unfiltered] Fri Oct 27 01:24:24 2023: Process terminated. [pid: 29350, tid:23209699268480]