( 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 MPI node — 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory — running Linux, Rocky 8.8. Wall-clock time: 3.49777… h CPU utilization: 167.89333… core-h ) Fri Oct 6 11:55:02 2023: Process started. [pid: 58921, tid:23374501275520] Tasks: 1. resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true) 2. generateDProofRepresentativeFiles(143, 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(143, false, true). Fri Oct 6 11:55:02 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 143, unfiltered] 0.03 ms taken to load initial representatives. 0.16 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23374432622336] 1.39 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23374422116096] 1.85 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23373748893440] 2.21 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23373732083456] 0.16 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23374424217344] 0.60 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23373719475968] 1.79 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23374441027328] 0.46 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23373746792192] 0.54 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23373721577216] 1.22 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23373740488448] 0.05 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23373729982208] 0.15 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23373725779712] 0.91 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23374430521088] 0.25 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23373715273472] 0.42 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23374436824832] 0.67 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23374428419840] 0.91 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23374434723584] 1.18 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23373708969728] 1.19 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23374438926080] 0.17 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23373742589696] 0.22 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23373744690944] 5577.76 ms (5 s 577.76 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23374441027328] 5899.96 ms (5 s 899.96 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23374438926080] 3527.68 ms (3 s 527.68 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23374436824832] 4593.53 ms (4 s 593.53 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23374434723584] 460.64 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23374432622336] 2482.13 ms (2 s 482.13 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23374430521088] 3993.05 ms (3 s 993.05 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23374428419840] 6.59 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23374426318592] 2090.55 ms (2 s 90.55 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23374424217344] 683.33 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23374422116096] 944.69 ms taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23373748893440] 8696.75 ms (8 s 696.75 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23373746792192] 7222.73 ms (7 s 222.73 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23373744690944] 10.37 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23373474154240] 6593.41 ms (6 s 593.41 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23373742589696] 1299.13 ms (1 s 299.13 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23373740488448] 1.95 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23373738387200] 2.05 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23373736285952] 4.92 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23373734184704] 1353.86 ms (1 s 353.86 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23373732083456] 1606.56 ms (1 s 606.56 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23373729982208] 2.11 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23373727880960] 2015.05 ms (2 s 15.05 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23373725779712] 8.89 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23373723678464] 969.14 ms taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23373721577216] 3400.17 ms (3 s 400.17 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23373719475968] 12.67 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23373717374720] 2976.97 ms (2 s 976.97 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23373715273472] 13.61 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23373713172224] 26.12 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23373711070976] 5253.66 ms (5 s 253.66 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23373708969728] 24.82 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23373706868480] 17.13 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23373704767232] 21.76 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23373702665984] 17.57 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23373700564736] 20.88 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23373698463488] 27.62 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23373696362240] 33.19 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23373694260992] 23.60 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23373692159744] 36.16 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23373690058496] 32.69 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23373687957248] 41.95 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23373685856000] 52.14 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23373614675712] 51.82 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23373612574464] 79.60 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23373610473216] 139.13 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23373608371968] 138.87 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23373606270720] 283.07 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23373604169472] 8750.94 ms (8 s 750.94 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. 9402.12 ms (9 s 402.12 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23373604169472] 9403.53 ms (9 s 403.53 ms) additional read duration. Loaded 1 more representative collection of size: 141 : 16952082 40988590 representatives in total. Fri Oct 6 11:55:22 2023: Inserted ≈ 5% of D-proof conclusions. [ 2049429 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 31 s 126.34 ms remaining ; 32 s 764.57 ms total) Fri Oct 6 11:55:24 2023: Inserted ≈10% of D-proof conclusions. [ 4098859 of 40988590] (ETC: Fri Oct 6 11:55:54 2023 ; 30 s 107.48 ms remaining ; 33 s 452.75 ms total) Fri Oct 6 11:55:25 2023: Inserted ≈15% of D-proof conclusions. [ 6148288 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 27 s 297.65 ms remaining ; 32 s 114.88 ms total) Fri Oct 6 11:55:27 2023: Inserted ≈20% of D-proof conclusions. [ 8197718 of 40988590] (ETC: Fri Oct 6 11:55:52 2023 ; 25 s 190.40 ms remaining ; 31 s 488.00 ms total) Fri Oct 6 11:55:29 2023: Inserted ≈25% of D-proof conclusions. [10247147 of 40988590] (ETC: Fri Oct 6 11:55:52 2023 ; 23 s 893.86 ms remaining ; 31 s 858.49 ms total) Fri Oct 6 11:55:30 2023: Inserted ≈30% of D-proof conclusions. [12296577 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 22 s 544.99 ms remaining ; 32 s 207.13 ms total) Fri Oct 6 11:55:32 2023: Inserted ≈35% of D-proof conclusions. [14346006 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 21 s 73.76 ms remaining ; 32 s 421.17 ms total) Fri Oct 6 11:55:34 2023: Inserted ≈40% of D-proof conclusions. [16395436 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 19 s 561.66 ms remaining ; 32 s 602.77 ms total) Fri Oct 6 11:55:35 2023: Inserted ≈45% of D-proof conclusions. [18444865 of 40988590] (ETC: Fri Oct 6 11:55:54 2023 ; 18 s 229.08 ms remaining ; 33 s 143.79 ms total) Fri Oct 6 11:55:37 2023: Inserted ≈50% of D-proof conclusions. [20494295 of 40988590] (ETC: Fri Oct 6 11:55:54 2023 ; 16 s 537.56 ms remaining ; 33 s 75.12 ms total) Fri Oct 6 11:55:39 2023: Inserted ≈55% of D-proof conclusions. [22543724 of 40988590] (ETC: Fri Oct 6 11:55:54 2023 ; 14 s 828.94 ms remaining ; 32 s 953.20 ms total) Fri Oct 6 11:55:40 2023: Inserted ≈60% of D-proof conclusions. [24593154 of 40988590] (ETC: Fri Oct 6 11:55:53 2023 ; 13 s 10.74 ms remaining ; 32 s 526.84 ms total) Fri Oct 6 11:55:41 2023: Inserted ≈65% of D-proof conclusions. [26642583 of 40988590] (ETC: Fri Oct 6 11:55:52 2023 ; 11 s 53.32 ms remaining ; 31 s 580.91 ms total) Fri Oct 6 11:55:42 2023: Inserted ≈70% of D-proof conclusions. [28692013 of 40988590] (ETC: Fri Oct 6 11:55:52 2023 ; 9 s 289.08 ms remaining ; 30 s 963.61 ms total) Fri Oct 6 11:55:43 2023: Inserted ≈75% of D-proof conclusions. [30741442 of 40988590] (ETC: Fri Oct 6 11:55:51 2023 ; 7 s 501.08 ms remaining ; 30 s 4.32 ms total) Fri Oct 6 11:55:44 2023: Inserted ≈80% of D-proof conclusions. [32790872 of 40988590] (ETC: Fri Oct 6 11:55:50 2023 ; 5 s 889.27 ms remaining ; 29 s 446.33 ms total) Fri Oct 6 11:55:45 2023: Inserted ≈85% of D-proof conclusions. [34840301 of 40988590] (ETC: Fri Oct 6 11:55:50 2023 ; 4 s 354.25 ms remaining ; 29 s 28.33 ms total) Fri Oct 6 11:55:46 2023: Inserted ≈90% of D-proof conclusions. [36889731 of 40988590] (ETC: Fri Oct 6 11:55:49 2023 ; 2 s 868.72 ms remaining ; 28 s 687.18 ms total) Fri Oct 6 11:55:47 2023: Inserted ≈95% of D-proof conclusions. [38939160 of 40988590] (ETC: Fri Oct 6 11:55:49 2023 ; 1 s 411.91 ms remaining ; 28 s 238.27 ms total) Fri Oct 6 11:55:48 2023: Inserted 100% of D-proof conclusions. [40988590 of 40988590] (ETC: Fri Oct 6 11:55:48 2023 ; 0.00 ms remaining ; 27 s 834.29 ms total) 27834.46 ms (27 s 834.46 ms) total insertion duration. Estimated iteration count set to 195782836, based on entry 141:152368710 and last known pair (139:118581507, 141:152368710) with 152368710/118581507 ≈ 1.28493 and 152368710 * (152368710/118581507)^1 ≈ 195782836.42. Fri Oct 6 11:55:48 2023: Starting to generate D-proof representatives of length 143. Fri Oct 6 12:00:35 2023: Iterated ≈ 2% of D-proof candidates. [ 3915656 of approximately 195782836] (ETC: Fri Oct 6 15:54:40 2023 ; 3 h 54 min 5 s 18.90 ms remaining ; 3 h 58 min 51 s 651.88 ms total) Fri Oct 6 12:05:10 2023: Iterated ≈ 4% of D-proof candidates. [ 7831313 of approximately 195782836] (ETC: Fri Oct 6 15:49:41 2023 ; 3 h 44 min 31 s 369.17 ms remaining ; 3 h 53 min 52 s 676.19 ms total) Fri Oct 6 12:09:11 2023: Iterated ≈ 6% of D-proof candidates. [ 11746970 of approximately 195782836] (ETC: Fri Oct 6 15:38:38 2023 ; 3 h 29 min 27 s 455.67 ms remaining ; 3 h 42 min 49 s 633.68 ms total) Fri Oct 6 12:12:56 2023: Iterated ≈ 8% of D-proof candidates. [ 15662626 of approximately 195782836] (ETC: Fri Oct 6 15:29:50 2023 ; 3 h 16 min 54 s 440.82 ms remaining ; 3 h 34 min 1 s 783.43 ms total) Fri Oct 6 12:17:21 2023: Iterated ≈ 10% of D-proof candidates. [ 19578283 of approximately 195782836] (ETC: Fri Oct 6 15:31:13 2023 ; 3 h 13 min 52 s 55.51 ms remaining ; 3 h 35 min 24 s 506.08 ms total) Fri Oct 6 12:21:27 2023: Iterated ≈ 12% of D-proof candidates. [ 23493940 of approximately 195782836] (ETC: Fri Oct 6 15:29:28 2023 ; 3 h 8 min 838.50 ms remaining ; 3 h 33 min 39 s 134.63 ms total) Fri Oct 6 12:25:12 2023: Iterated ≈ 14% of D-proof candidates. [ 27409597 of approximately 195782836] (ETC: Fri Oct 6 15:25:45 2023 ; 3 h 32 s 991.23 ms remaining ; 3 h 29 min 56 s 501.43 ms total) Fri Oct 6 12:28:37 2023: Iterated ≈ 16% of D-proof candidates. [ 31325253 of approximately 195782836] (ETC: Fri Oct 6 15:20:54 2023 ; 2 h 52 min 16 s 732.17 ms remaining ; 3 h 25 min 5 s 633.48 ms total) Fri Oct 6 12:32:28 2023: Iterated ≈ 18% of D-proof candidates. [ 35240910 of approximately 195782836] (ETC: Fri Oct 6 15:19:29 2023 ; 2 h 47 min 1 s 61.79 ms remaining ; 3 h 23 min 40 s 807.02 ms total) Fri Oct 6 12:36:37 2023: Iterated ≈ 20% of D-proof candidates. [ 39156567 of approximately 195782836] (ETC: Fri Oct 6 15:19:50 2023 ; 2 h 43 min 13 s 376.59 ms remaining ; 3 h 24 min 1 s 720.72 ms total) Fri Oct 6 12:40:49 2023: Iterated ≈ 22% of D-proof candidates. [ 43072223 of approximately 195782836] (ETC: Fri Oct 6 15:20:22 2023 ; 2 h 39 min 33 s 415.81 ms remaining ; 3 h 24 min 33 s 609.94 ms total) Fri Oct 6 12:45:01 2023: Iterated ≈ 24% of D-proof candidates. [ 46987880 of approximately 195782836] (ETC: Fri Oct 6 15:20:51 2023 ; 2 h 35 min 50 s 157.39 ms remaining ; 3 h 25 min 2 s 838.62 ms total) Fri Oct 6 12:49:07 2023: Iterated ≈ 26% of D-proof candidates. [ 50903537 of approximately 195782836] (ETC: Fri Oct 6 15:20:52 2023 ; 2 h 31 min 44 s 924.41 ms remaining ; 3 h 25 min 3 s 951.87 ms total) Fri Oct 6 12:53:24 2023: Iterated ≈ 28% of D-proof candidates. [ 54819194 of approximately 195782836] (ETC: Fri Oct 6 15:21:31 2023 ; 2 h 28 min 6 s 471.36 ms remaining ; 3 h 25 min 42 s 321.32 ms total) Fri Oct 6 12:57:23 2023: Iterated ≈ 30% of D-proof candidates. [ 58734850 of approximately 195782836] (ETC: Fri Oct 6 15:21:04 2023 ; 2 h 23 min 41 s 234.21 ms remaining ; 3 h 25 min 16 s 48.80 ms total) Fri Oct 6 13:01:21 2023: Iterated ≈ 32% of D-proof candidates. [ 62650507 of approximately 195782836] (ETC: Fri Oct 6 15:20:39 2023 ; 2 h 19 min 17 s 542.53 ms remaining ; 3 h 24 min 50 s 503.67 ms total) Fri Oct 6 13:05:22 2023: Iterated ≈ 34% of D-proof candidates. [ 66566164 of approximately 195782836] (ETC: Fri Oct 6 15:20:24 2023 ; 2 h 15 min 1 s 685.66 ms remaining ; 3 h 24 min 35 s 281.28 ms total) Fri Oct 6 13:09:36 2023: Iterated ≈ 36% of D-proof candidates. [ 70481820 of approximately 195782836] (ETC: Fri Oct 6 15:20:48 2023 ; 2 h 11 min 11 s 933.16 ms remaining ; 3 h 24 min 59 s 895.47 ms total) Fri Oct 6 13:13:20 2023: Iterated ≈ 38% of D-proof candidates. [ 74397477 of approximately 195782836] (ETC: Fri Oct 6 15:19:50 2023 ; 2 h 6 min 29 s 608.37 ms remaining ; 3 h 24 min 1 s 303.75 ms total) Fri Oct 6 13:17:09 2023: Iterated ≈ 40% of D-proof candidates. [ 78313134 of approximately 195782836] (ETC: Fri Oct 6 15:19:10 2023 ; 2 h 2 min 1 s 242.68 ms remaining ; 3 h 23 min 22 s 71.08 ms total) Fri Oct 6 13:20:54 2023: Iterated ≈ 42% of D-proof candidates. [ 82228791 of approximately 195782836] (ETC: Fri Oct 6 15:18:24 2023 ; 1 h 57 min 30 s 180.11 ms remaining ; 3 h 22 min 35 s 482.93 ms total) Fri Oct 6 13:24:42 2023: Iterated ≈ 44% of D-proof candidates. [ 86144447 of approximately 195782836] (ETC: Fri Oct 6 15:17:51 2023 ; 1 h 53 min 8 s 818.61 ms remaining ; 3 h 22 min 2 s 890.28 ms total) Fri Oct 6 13:28:32 2023: Iterated ≈ 46% of D-proof candidates. [ 90060104 of approximately 195782836] (ETC: Fri Oct 6 15:17:23 2023 ; 1 h 48 min 51 s 321.01 ms remaining ; 3 h 21 min 35 s 38.85 ms total) Fri Oct 6 13:32:16 2023: Iterated ≈ 48% of D-proof candidates. [ 93975761 of approximately 195782836] (ETC: Fri Oct 6 15:16:45 2023 ; 1 h 44 min 29 s 414.06 ms remaining ; 3 h 20 min 56 s 565.47 ms total) Fri Oct 6 13:35:59 2023: Iterated ≈ 50% of D-proof candidates. [ 97891418 of approximately 195782836] (ETC: Fri Oct 6 15:16:10 2023 ; 1 h 40 min 10 s 604.72 ms remaining ; 3 h 20 min 21 s 209.45 ms total) Fri Oct 6 13:39:42 2023: Iterated ≈ 52% of D-proof candidates. [101807074 of approximately 195782836] (ETC: Fri Oct 6 15:15:36 2023 ; 1 h 35 min 53 s 949.17 ms remaining ; 3 h 19 min 47 s 394.01 ms total) Fri Oct 6 13:43:16 2023: Iterated ≈ 54% of D-proof candidates. [105722731 of approximately 195782836] (ETC: Fri Oct 6 15:14:48 2023 ; 1 h 31 min 32 s 306.18 ms remaining ; 3 h 18 min 59 s 795.98 ms total) Fri Oct 6 13:46:50 2023: Iterated ≈ 56% of D-proof candidates. [109638388 of approximately 195782836] (ETC: Fri Oct 6 15:14:05 2023 ; 1 h 27 min 14 s 294.49 ms remaining ; 3 h 18 min 16 s 123.82 ms total) Fri Oct 6 13:50:27 2023: Iterated ≈ 58% of D-proof candidates. [113554044 of approximately 195782836] (ETC: Fri Oct 6 15:13:28 2023 ; 1 h 23 min 1 s 135.14 ms remaining ; 3 h 17 min 39 s 845.45 ms total) Fri Oct 6 13:54:02 2023: Iterated ≈ 60% of D-proof candidates. [117469701 of approximately 195782836] (ETC: Fri Oct 6 15:12:51 2023 ; 1 h 18 min 49 s 162.08 ms remaining ; 3 h 17 min 2 s 905.12 ms total) Fri Oct 6 13:57:37 2023: Iterated ≈ 62% of D-proof candidates. [121385358 of approximately 195782836] (ETC: Fri Oct 6 15:12:16 2023 ; 1 h 14 min 39 s 337.39 ms remaining ; 3 h 16 min 27 s 729.93 ms total) Fri Oct 6 14:01:05 2023: Iterated ≈ 64% of D-proof candidates. [125301015 of approximately 195782836] (ETC: Fri Oct 6 15:11:34 2023 ; 1 h 10 min 28 s 321.11 ms remaining ; 3 h 15 min 45 s 336.42 ms total) Fri Oct 6 14:04:35 2023: Iterated ≈ 66% of D-proof candidates. [129216671 of approximately 195782836] (ETC: Fri Oct 6 15:10:56 2023 ; 1 h 6 min 20 s 445.54 ms remaining ; 3 h 15 min 7 s 192.64 ms total) Fri Oct 6 14:08:07 2023: Iterated ≈ 68% of D-proof candidates. [133132328 of approximately 195782836] (ETC: Fri Oct 6 15:10:23 2023 ; 1 h 2 min 15 s 760.76 ms remaining ; 3 h 14 min 34 s 252.27 ms total) Fri Oct 6 14:11:36 2023: Iterated ≈ 70% of D-proof candidates. [137047985 of approximately 195782836] (ETC: Fri Oct 6 15:09:48 2023 ; 58 min 11 s 934.48 ms remaining ; 3 h 13 min 59 s 781.54 ms total) Fri Oct 6 14:15:04 2023: Iterated ≈ 72% of D-proof candidates. [140963641 of approximately 195782836] (ETC: Fri Oct 6 15:09:14 2023 ; 54 min 9 s 576.89 ms remaining ; 3 h 13 min 25 s 631.54 ms total) Fri Oct 6 14:18:32 2023: Iterated ≈ 74% of D-proof candidates. [144879298 of approximately 195782836] (ETC: Fri Oct 6 15:08:41 2023 ; 50 min 8 s 837.55 ms remaining ; 3 h 12 min 52 s 451.97 ms total) Fri Oct 6 14:22:00 2023: Iterated ≈ 76% of D-proof candidates. [148794955 of approximately 195782836] (ETC: Fri Oct 6 15:08:10 2023 ; 46 min 10 s 61.48 ms remaining ; 3 h 12 min 21 s 922.73 ms total) Fri Oct 6 14:25:27 2023: Iterated ≈ 78% of D-proof candidates. [152710612 of approximately 195782836] (ETC: Fri Oct 6 15:07:39 2023 ; 42 min 12 s 407.33 ms remaining ; 3 h 11 min 50 s 942.40 ms total) Fri Oct 6 14:28:51 2023: Iterated ≈ 80% of D-proof candidates. [156626268 of approximately 195782836] (ETC: Fri Oct 6 15:07:07 2023 ; 38 min 15 s 758.44 ms remaining ; 3 h 11 min 18 s 791.99 ms total) Fri Oct 6 14:32:14 2023: Iterated ≈ 82% of D-proof candidates. [160541925 of approximately 195782836] (ETC: Fri Oct 6 15:06:35 2023 ; 34 min 20 s 351.14 ms remaining ; 3 h 10 min 46 s 395.08 ms total) Fri Oct 6 14:35:37 2023: Iterated ≈ 84% of D-proof candidates. [164457582 of approximately 195782836] (ETC: Fri Oct 6 15:06:03 2023 ; 30 min 26 s 307.88 ms remaining ; 3 h 10 min 14 s 424.15 ms total) Fri Oct 6 14:38:56 2023: Iterated ≈ 86% of D-proof candidates. [168373238 of approximately 195782836] (ETC: Fri Oct 6 15:05:29 2023 ; 26 min 33 s 293.59 ms remaining ; 3 h 9 min 40 s 668.09 ms total) Fri Oct 6 14:42:14 2023: Iterated ≈ 88% of D-proof candidates. [172288895 of approximately 195782836] (ETC: Fri Oct 6 15:04:56 2023 ; 22 min 41 s 696.93 ms remaining ; 3 h 9 min 7 s 474.10 ms total) Fri Oct 6 14:45:34 2023: Iterated ≈ 90% of D-proof candidates. [176204552 of approximately 195782836] (ETC: Fri Oct 6 15:04:25 2023 ; 18 min 51 s 707.38 ms remaining ; 3 h 8 min 37 s 73.53 ms total) Fri Oct 6 14:48:54 2023: Iterated ≈ 92% of D-proof candidates. [180120209 of approximately 195782836] (ETC: Fri Oct 6 15:03:57 2023 ; 15 min 3 s 83.97 ms remaining ; 3 h 8 min 8 s 549.60 ms total) Fri Oct 6 14:52:12 2023: Iterated ≈ 94% of D-proof candidates. [184035865 of approximately 195782836] (ETC: Fri Oct 6 15:03:28 2023 ; 11 min 15 s 573.31 ms remaining ; 3 h 7 min 39 s 554.36 ms total) Fri Oct 6 14:55:31 2023: Iterated ≈ 96% of D-proof candidates. [187951522 of approximately 195782836] (ETC: Fri Oct 6 15:03:00 2023 ; 7 min 29 s 261.95 ms remaining ; 3 h 7 min 11 s 547.98 ms total) Fri Oct 6 14:58:47 2023: Iterated ≈ 98% of D-proof candidates. [191867179 of approximately 195782836] (ETC: Fri Oct 6 15:02:31 2023 ; 3 min 44 s 53.81 ms remaining ; 3 h 6 min 42 s 689.58 ms total) Fri Oct 6 15:02:04 2023: Iterated ≈100% of D-proof candidates. [195782836 of approximately 195782836] (ETC: Fri Oct 6 15:02:04 2023 ; 0.00 ms remaining ; 3 h 6 min 15 s 422.32 ms total) 12213641.81 ms (3 h 23 min 33 s 641.81 ms) taken to collect 26431403 D-proofs of length 143. [iterated 216457445 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 } } 148679.96 ms (2 min 28 s 679.96 ms) taken to filter and order new representative proofs. Found 26431403 representative, 80136744 redundant, and 109889298 invalid condensed detachment proof strings. lengths up to 143 ; 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)} ; 26431403 new representative proofs (80136744 redundant, 109889298 invalid) Fri Oct 6 15:22:06 2023: Starting to write 26431403 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. 31218.94 ms (31 s 218.94 ms) taken to print and save 8473778240 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. Fri Oct 6 15:23:06 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 143, unfiltered] Fri Oct 6 15:24:54 2023: Process terminated. [pid: 58921, tid:23374501275520]