( 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.3030555… h CPU utilization: 158.54666… core-h ) Sun Oct 22 06:21:17 2023: Process started. [pid: 120923, tid:23140340451200] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. generateDProofRepresentativeFiles(153, false, true) [Main] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9] (1) C0CCN1CCN2.3C4.1CC2.4C2.1 - CpCCNqCCNrsCtqCCrtCrq - 0\imply((\not1\imply((\not2\imply3)\imply(4\imply1)))\imply((2\imply4)\imply(2\imply1))) [Main] Calling generateDProofRepresentativeFiles(153, false, true). Sun Oct 22 06:21:17 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 153, unfiltered] 0.03 ms taken to load initial representatives. 2.37 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23140273899264] 6.54 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23140278101760] 6.69 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23140254988032] 6.52 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23140246583040] 0.68 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23140219266816] 0.51 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23140236076800] 1.14 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23140244481792] 1.88 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23140212963072] 0.32 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23140261291776] 0.43 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23140267595520] 0.44 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23140276000512] 0.61 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23140250785536] 0.01 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23140257089280] 1.28 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23140252886784] 2.12 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23140229773056] 2.22 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23140248684288] 0.28 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23140263393024] 0.50 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23140280203008] 0.00 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23140271798016] 0.74 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23140269696768] 0.06 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23140240279296] 0.15 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23140233975552] 0.28 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23140242380544] 0.69 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23140227671808] 0.78 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23140265494272] 0.33 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23140215064320] 0.36 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23140231874304] 3840.58 ms (3 s 840.58 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23140280203008] 314.09 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23140278101760] 9638.24 ms (9 s 638.24 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23140276000512] 158.19 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23140273899264] 4391.63 ms (4 s 391.63 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23140271798016] 5218.88 ms (5 s 218.88 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23140269696768] 5946.51 ms (5 s 946.51 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23140267595520] 8081.88 ms (8 s 81.88 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23140265494272] 3208.26 ms (3 s 208.26 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23140263393024] 3851.96 ms (3 s 851.96 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23140261291776] 0.43 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23140259190528] 1405.05 ms (1 s 405.05 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23140257089280] 473.64 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23140254988032] 1830.43 ms (1 s 830.43 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23140252886784] 1266.86 ms (1 s 266.86 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23140250785536] 2744.30 ms (2 s 744.30 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23140248684288] 673.04 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23140246583040] 1915.53 ms (1 s 915.53 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23140244481792] 6810.46 ms (6 s 810.46 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23140242380544] 5789.98 ms (5 s 789.98 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23140240279296] 3.66 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23140238178048] 1370.83 ms (1 s 370.83 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23140236076800] 6276.12 ms (6 s 276.12 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23140233975552] 9503.82 ms (9 s 503.82 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23140231874304] 2326.51 ms (2 s 326.51 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23140229773056] 7463.15 ms (7 s 463.15 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23140227671808] 5.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23140225570560] 1.73 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23140223469312] 4.00 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23140221368064] 1052.10 ms (1 s 52.10 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23140219266816] 9.18 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23140217165568] 8748.33 ms (8 s 748.33 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23140215064320] 2480.02 ms (2 s 480.02 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23140212963072] 7.16 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23137995454208] 25.68 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23137859135232] 24.93 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23137993352960] 30.27 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23137991251712] 17.65 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23137989150464] 12.61 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23137987049216] 32.44 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23137984947968] 19.54 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23137982846720] 58.43 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23137980745472] 40.96 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23137978644224] 64.16 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23137976542976] 44.73 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23137974441728] 60.90 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23137972340480] 91.28 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23137970239232] 115.73 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23137968137984] 9704.58 ms (9 s 704.58 ms) total read duration. Loaded 76 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 1 9 : 2 11 : 2 13 : 2 15 : 2 17 : 5 19 : 5 21 : 3 23 : 6 25 : 10 27 : 7 29 : 12 31 : 14 33 : 17 35 : 21 37 : 30 39 : 28 41 : 44 43 : 56 45 : 66 47 : 80 49 : 108 51 : 123 53 : 168 55 : 197 57 : 241 59 : 303 61 : 390 63 : 444 65 : 570 67 : 707 69 : 863 71 : 1052 73 : 1340 75 : 1586 77 : 1990 79 : 2467 81 : 3018 83 : 3679 85 : 4661 87 : 5632 89 : 6994 91 : 8637 93 : 10677 95 : 13008 97 : 16295 99 : 19833 101 : 24567 103 : 30296 105 : 37377 107 : 45724 109 : 56922 111 : 69661 113 : 85894 115 : 105871 117 : 130737 119 : 160270 121 : 198446 123 : 243740 125 : 300530 127 : 370216 129 : 456911 131 : 560926 133 : 693346 135 : 853090 137 : 1051251 139 : 1294413 141 : 1597383 143 : 1963944 145 : 2423655 147 : 2983754 149 : 3676539 151 : 4527348 24048210 representatives in total. Sun Oct 22 06:21:28 2023: Inserted ≈ 5% of D-proof conclusions. [ 1202410 of 24048210] (ETC: Sun Oct 22 06:21:51 2023 ; 22 s 742.23 ms remaining ; 23 s 939.19 ms total) Sun Oct 22 06:21:29 2023: Inserted ≈10% of D-proof conclusions. [ 2404821 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 20 s 381.93 ms remaining ; 22 s 646.59 ms total) Sun Oct 22 06:21:30 2023: Inserted ≈15% of D-proof conclusions. [ 3607231 of 24048210] (ETC: Sun Oct 22 06:21:48 2023 ; 18 s 363.69 ms remaining ; 21 s 604.34 ms total) Sun Oct 22 06:21:31 2023: Inserted ≈20% of D-proof conclusions. [ 4809642 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 17 s 838.83 ms remaining ; 22 s 298.54 ms total) Sun Oct 22 06:21:32 2023: Inserted ≈25% of D-proof conclusions. [ 6012052 of 24048210] (ETC: Sun Oct 22 06:21:50 2023 ; 17 s 46.15 ms remaining ; 22 s 728.20 ms total) Sun Oct 22 06:21:34 2023: Inserted ≈30% of D-proof conclusions. [ 7214463 of 24048210] (ETC: Sun Oct 22 06:21:50 2023 ; 16 s 148.09 ms remaining ; 23 s 68.70 ms total) Sun Oct 22 06:21:35 2023: Inserted ≈35% of D-proof conclusions. [ 8416873 of 24048210] (ETC: Sun Oct 22 06:21:50 2023 ; 15 s 26.27 ms remaining ; 23 s 117.34 ms total) Sun Oct 22 06:21:36 2023: Inserted ≈40% of D-proof conclusions. [ 9619284 of 24048210] (ETC: Sun Oct 22 06:21:50 2023 ; 13 s 645.59 ms remaining ; 22 s 742.64 ms total) Sun Oct 22 06:21:37 2023: Inserted ≈45% of D-proof conclusions. [10821694 of 24048210] (ETC: Sun Oct 22 06:21:50 2023 ; 12 s 587.81 ms remaining ; 22 s 886.93 ms total) Sun Oct 22 06:21:38 2023: Inserted ≈50% of D-proof conclusions. [12024105 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 11 s 290.99 ms remaining ; 22 s 581.97 ms total) Sun Oct 22 06:21:39 2023: Inserted ≈55% of D-proof conclusions. [13226515 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 10 s 151.42 ms remaining ; 22 s 558.71 ms total) Sun Oct 22 06:21:40 2023: Inserted ≈60% of D-proof conclusions. [14428926 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 8 s 982.69 ms remaining ; 22 s 456.72 ms total) Sun Oct 22 06:21:41 2023: Inserted ≈65% of D-proof conclusions. [15631336 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 7 s 837.31 ms remaining ; 22 s 392.30 ms total) Sun Oct 22 06:21:42 2023: Inserted ≈70% of D-proof conclusions. [16833747 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 6 s 665.66 ms remaining ; 22 s 218.88 ms total) Sun Oct 22 06:21:43 2023: Inserted ≈75% of D-proof conclusions. [18036157 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 5 s 543.53 ms remaining ; 22 s 174.14 ms total) Sun Oct 22 06:21:45 2023: Inserted ≈80% of D-proof conclusions. [19238568 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 4 s 449.04 ms remaining ; 22 s 245.19 ms total) Sun Oct 22 06:21:46 2023: Inserted ≈85% of D-proof conclusions. [20440978 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 3 s 336.04 ms remaining ; 22 s 240.27 ms total) Sun Oct 22 06:21:47 2023: Inserted ≈90% of D-proof conclusions. [21643389 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 2 s 217.16 ms remaining ; 22 s 171.57 ms total) Sun Oct 22 06:21:48 2023: Inserted ≈95% of D-proof conclusions. [22845799 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 1 s 108.34 ms remaining ; 22 s 166.83 ms total) Sun Oct 22 06:21:49 2023: Inserted 100% of D-proof conclusions. [24048210 of 24048210] (ETC: Sun Oct 22 06:21:49 2023 ; 0.00 ms remaining ; 21 s 804.80 ms total) 21805.05 ms (21 s 805.05 ms) total insertion duration. Estimated iteration count set to 234894594, based on entry 151:187924390 and last known pair (149:150346484, 151:187924390) with 187924390/150346484 ≈ 1.24994 and 187924390 * (187924390/150346484)^1 ≈ 234894594.26. Sun Oct 22 06:21:49 2023: Starting to generate D-proof representatives of length 153. Sun Oct 22 06:26:39 2023: Iterated ≈ 2% of D-proof candidates. [ 4697891 of approximately 234894594] (ETC: Sun Oct 22 10:23:53 2023 ; 3 h 57 min 13 s 866.50 ms remaining ; 4 h 2 min 4 s 353.52 ms total) Sun Oct 22 06:31:11 2023: Iterated ≈ 4% of D-proof candidates. [ 9395783 of approximately 234894594] (ETC: Sun Oct 22 10:16:11 2023 ; 3 h 44 min 59 s 691.06 ms remaining ; 3 h 54 min 22 s 178.14 ms total) Sun Oct 22 06:35:30 2023: Iterated ≈ 6% of D-proof candidates. [ 14093675 of approximately 234894594] (ETC: Sun Oct 22 10:09:54 2023 ; 3 h 34 min 24 s 628.26 ms remaining ; 3 h 48 min 5 s 774.70 ms total) Sun Oct 22 06:39:59 2023: Iterated ≈ 8% of D-proof candidates. [ 18791567 of approximately 234894594] (ETC: Sun Oct 22 10:09:04 2023 ; 3 h 29 min 4 s 387.01 ms remaining ; 3 h 47 min 15 s 203.24 ms total) Sun Oct 22 06:44:06 2023: Iterated ≈ 10% of D-proof candidates. [ 23489459 of approximately 234894594] (ETC: Sun Oct 22 10:04:46 2023 ; 3 h 20 min 39 s 281.75 ms remaining ; 3 h 42 min 56 s 979.70 ms total) Sun Oct 22 06:48:30 2023: Iterated ≈ 12% of D-proof candidates. [ 28187351 of approximately 234894594] (ETC: Sun Oct 22 10:04:10 2023 ; 3 h 15 min 40 s 221.97 ms remaining ; 3 h 42 min 21 s 161.31 ms total) Sun Oct 22 06:52:52 2023: Iterated ≈ 14% of D-proof candidates. [ 32885243 of approximately 234894594] (ETC: Sun Oct 22 10:03:37 2023 ; 3 h 10 min 45 s 614.98 ms remaining ; 3 h 41 min 48 s 854.62 ms total) Sun Oct 22 06:57:27 2023: Iterated ≈ 16% of D-proof candidates. [ 37583135 of approximately 234894594] (ETC: Sun Oct 22 10:04:35 2023 ; 3 h 7 min 8 s 183.35 ms remaining ; 3 h 42 min 46 s 884.94 ms total) Sun Oct 22 07:02:01 2023: Iterated ≈ 18% of D-proof candidates. [ 42281026 of approximately 234894594] (ETC: Sun Oct 22 10:05:10 2023 ; 3 h 3 min 9 s 259.90 ms remaining ; 3 h 43 min 21 s 536.40 ms total) Sun Oct 22 07:06:40 2023: Iterated ≈ 20% of D-proof candidates. [ 46978918 of approximately 234894594] (ETC: Sun Oct 22 10:06:07 2023 ; 2 h 59 min 26 s 551.73 ms remaining ; 3 h 44 min 18 s 189.61 ms total) Sun Oct 22 07:11:08 2023: Iterated ≈ 22% of D-proof candidates. [ 51676810 of approximately 234894594] (ETC: Sun Oct 22 10:05:58 2023 ; 2 h 54 min 50 s 677.47 ms remaining ; 3 h 44 min 9 s 586.45 ms total) Sun Oct 22 07:15:54 2023: Iterated ≈ 24% of D-proof candidates. [ 56374702 of approximately 234894594] (ETC: Sun Oct 22 10:07:10 2023 ; 2 h 51 min 16 s 219.92 ms remaining ; 3 h 45 min 21 s 341.96 ms total) Sun Oct 22 07:20:13 2023: Iterated ≈ 26% of D-proof candidates. [ 61072594 of approximately 234894594] (ETC: Sun Oct 22 10:06:28 2023 ; 2 h 46 min 15 s 31.77 ms remaining ; 3 h 44 min 39 s 772.63 ms total) Sun Oct 22 07:24:41 2023: Iterated ≈ 28% of D-proof candidates. [ 65770486 of approximately 234894594] (ETC: Sun Oct 22 10:06:22 2023 ; 2 h 41 min 40 s 541.09 ms remaining ; 3 h 44 min 32 s 973.72 ms total) Sun Oct 22 07:29:01 2023: Iterated ≈ 30% of D-proof candidates. [ 70468378 of approximately 234894594] (ETC: Sun Oct 22 10:05:50 2023 ; 2 h 36 min 49 s 57.15 ms remaining ; 3 h 44 min 1 s 510.20 ms total) Sun Oct 22 07:33:21 2023: Iterated ≈ 32% of D-proof candidates. [ 75166270 of approximately 234894594] (ETC: Sun Oct 22 10:05:23 2023 ; 2 h 32 min 1 s 961.39 ms remaining ; 3 h 43 min 34 s 649.10 ms total) Sun Oct 22 07:37:39 2023: Iterated ≈ 34% of D-proof candidates. [ 79864161 of approximately 234894594] (ETC: Sun Oct 22 10:04:51 2023 ; 2 h 27 min 12 s 544.80 ms remaining ; 3 h 43 min 2 s 643.56 ms total) Sun Oct 22 07:41:43 2023: Iterated ≈ 36% of D-proof candidates. [ 84562053 of approximately 234894594] (ETC: Sun Oct 22 10:03:47 2023 ; 2 h 22 min 3 s 737.59 ms remaining ; 3 h 41 min 58 s 339.92 ms total) Sun Oct 22 07:45:48 2023: Iterated ≈ 38% of D-proof candidates. [ 89259945 of approximately 234894594] (ETC: Sun Oct 22 10:02:49 2023 ; 2 h 17 min 1 s 728.44 ms remaining ; 3 h 41 min 852.26 ms total) Sun Oct 22 07:49:46 2023: Iterated ≈ 40% of D-proof candidates. [ 93957837 of approximately 234894594] (ETC: Sun Oct 22 10:01:43 2023 ; 2 h 11 min 56 s 477.67 ms remaining ; 3 h 39 min 54 s 129.40 ms total) Sun Oct 22 07:53:41 2023: Iterated ≈ 42% of D-proof candidates. [ 98655729 of approximately 234894594] (ETC: Sun Oct 22 10:00:33 2023 ; 2 h 6 min 51 s 951.72 ms remaining ; 3 h 38 min 44 s 54.65 ms total) Sun Oct 22 07:57:34 2023: Iterated ≈ 44% of D-proof candidates. [103353621 of approximately 234894594] (ETC: Sun Oct 22 09:59:26 2023 ; 2 h 1 min 52 s 118.51 ms remaining ; 3 h 37 min 37 s 354.45 ms total) Sun Oct 22 08:01:26 2023: Iterated ≈ 46% of D-proof candidates. [108051513 of approximately 234894594] (ETC: Sun Oct 22 09:58:23 2023 ; 1 h 56 min 56 s 882.00 ms remaining ; 3 h 36 min 34 s 225.90 ms total) Sun Oct 22 08:05:15 2023: Iterated ≈ 48% of D-proof candidates. [112749405 of approximately 234894594] (ETC: Sun Oct 22 09:57:19 2023 ; 1 h 52 min 3 s 745.13 ms remaining ; 3 h 35 min 30 s 279.09 ms total) Sun Oct 22 08:08:57 2023: Iterated ≈ 50% of D-proof candidates. [117447297 of approximately 234894594] (ETC: Sun Oct 22 09:56:05 2023 ; 1 h 47 min 8 s 369.28 ms remaining ; 3 h 34 min 16 s 738.57 ms total) Sun Oct 22 08:12:38 2023: Iterated ≈ 52% of D-proof candidates. [122145188 of approximately 234894594] (ETC: Sun Oct 22 09:54:56 2023 ; 1 h 42 min 17 s 717.39 ms remaining ; 3 h 33 min 6 s 911.13 ms total) Sun Oct 22 08:16:18 2023: Iterated ≈ 54% of D-proof candidates. [126843080 of approximately 234894594] (ETC: Sun Oct 22 09:53:50 2023 ; 1 h 37 min 31 s 742.57 ms remaining ; 3 h 32 min 1 s 179.42 ms total) Sun Oct 22 08:19:55 2023: Iterated ≈ 56% of D-proof candidates. [131540972 of approximately 234894594] (ETC: Sun Oct 22 09:52:43 2023 ; 1 h 32 min 47 s 757.31 ms remaining ; 3 h 30 min 53 s 993.80 ms total) Sun Oct 22 08:23:32 2023: Iterated ≈ 58% of D-proof candidates. [136238864 of approximately 234894594] (ETC: Sun Oct 22 09:51:40 2023 ; 1 h 28 min 8 s 586.27 ms remaining ; 3 h 29 min 51 s 872.02 ms total) Sun Oct 22 08:27:05 2023: Iterated ≈ 60% of D-proof candidates. [140936756 of approximately 234894594] (ETC: Sun Oct 22 09:50:36 2023 ; 1 h 23 min 30 s 930.09 ms remaining ; 3 h 28 min 47 s 325.18 ms total) Sun Oct 22 08:30:36 2023: Iterated ≈ 62% of D-proof candidates. [145634648 of approximately 234894594] (ETC: Sun Oct 22 09:49:33 2023 ; 1 h 18 min 56 s 359.98 ms remaining ; 3 h 27 min 44 s 105.16 ms total) Sun Oct 22 08:34:06 2023: Iterated ≈ 64% of D-proof candidates. [150332540 of approximately 234894594] (ETC: Sun Oct 22 09:48:30 2023 ; 1 h 14 min 24 s 673.53 ms remaining ; 3 h 26 min 41 s 870.89 ms total) Sun Oct 22 08:37:35 2023: Iterated ≈ 66% of D-proof candidates. [155030432 of approximately 234894594] (ETC: Sun Oct 22 09:47:32 2023 ; 1 h 9 min 56 s 672.55 ms remaining ; 3 h 25 min 43 s 154.54 ms total) Sun Oct 22 08:41:01 2023: Iterated ≈ 68% of D-proof candidates. [159728323 of approximately 234894594] (ETC: Sun Oct 22 09:46:32 2023 ; 1 h 5 min 30 s 613.73 ms remaining ; 3 h 24 min 43 s 167.76 ms total) Sun Oct 22 08:44:26 2023: Iterated ≈ 70% of D-proof candidates. [164426215 of approximately 234894594] (ETC: Sun Oct 22 09:45:34 2023 ; 1 h 1 min 7 s 549.59 ms remaining ; 3 h 23 min 45 s 165.16 ms total) Sun Oct 22 08:47:48 2023: Iterated ≈ 72% of D-proof candidates. [169124107 of approximately 234894594] (ETC: Sun Oct 22 09:44:34 2023 ; 56 min 46 s 441.19 ms remaining ; 3 h 22 min 45 s 861.29 ms total) Sun Oct 22 08:51:11 2023: Iterated ≈ 74% of D-proof candidates. [173821999 of approximately 234894594] (ETC: Sun Oct 22 09:43:40 2023 ; 52 min 28 s 882.08 ms remaining ; 3 h 21 min 51 s 84.80 ms total) Sun Oct 22 08:54:31 2023: Iterated ≈ 76% of D-proof candidates. [178519891 of approximately 234894594] (ETC: Sun Oct 22 09:42:44 2023 ; 48 min 13 s 323.67 ms remaining ; 3 h 20 min 55 s 515.21 ms total) Sun Oct 22 08:57:52 2023: Iterated ≈ 78% of D-proof candidates. [183217783 of approximately 234894594] (ETC: Sun Oct 22 09:41:53 2023 ; 44 min 1 s 28.00 ms remaining ; 3 h 20 min 4 s 672.68 ms total) Sun Oct 22 09:01:11 2023: Iterated ≈ 80% of D-proof candidates. [187915675 of approximately 234894594] (ETC: Sun Oct 22 09:41:02 2023 ; 39 min 50 s 642.88 ms remaining ; 3 h 19 min 13 s 214.33 ms total) Sun Oct 22 09:04:30 2023: Iterated ≈ 82% of D-proof candidates. [192613567 of approximately 234894594] (ETC: Sun Oct 22 09:40:12 2023 ; 35 min 42 s 683.65 ms remaining ; 3 h 18 min 23 s 798.02 ms total) Sun Oct 22 09:07:47 2023: Iterated ≈ 84% of D-proof candidates. [197311458 of approximately 234894594] (ETC: Sun Oct 22 09:39:24 2023 ; 31 min 36 s 869.32 ms remaining ; 3 h 17 min 35 s 432.93 ms total) Sun Oct 22 09:11:04 2023: Iterated ≈ 86% of D-proof candidates. [202009350 of approximately 234894594] (ETC: Sun Oct 22 09:38:38 2023 ; 27 min 33 s 277.38 ms remaining ; 3 h 16 min 49 s 123.88 ms total) Sun Oct 22 09:14:21 2023: Iterated ≈ 88% of D-proof candidates. [206707242 of approximately 234894594] (ETC: Sun Oct 22 09:37:52 2023 ; 23 min 31 s 623.59 ms remaining ; 3 h 16 min 3 s 529.63 ms total) Sun Oct 22 09:17:38 2023: Iterated ≈ 90% of D-proof candidates. [211405134 of approximately 234894594] (ETC: Sun Oct 22 09:37:11 2023 ; 19 min 32 s 198.68 ms remaining ; 3 h 15 min 21 s 986.55 ms total) Sun Oct 22 09:20:54 2023: Iterated ≈ 92% of D-proof candidates. [216103026 of approximately 234894594] (ETC: Sun Oct 22 09:36:29 2023 ; 15 min 34 s 398.28 ms remaining ; 3 h 14 min 39 s 978.22 ms total) Sun Oct 22 09:24:10 2023: Iterated ≈ 94% of D-proof candidates. [220800918 of approximately 234894594] (ETC: Sun Oct 22 09:35:48 2023 ; 11 min 38 s 388.66 ms remaining ; 3 h 13 min 59 s 810.74 ms total) Sun Oct 22 09:27:26 2023: Iterated ≈ 96% of D-proof candidates. [225498810 of approximately 234894594] (ETC: Sun Oct 22 09:35:10 2023 ; 7 min 44 s 57.34 ms remaining ; 3 h 13 min 21 s 433.23 ms total) Sun Oct 22 09:30:42 2023: Iterated ≈ 98% of D-proof candidates. [230196702 of approximately 234894594] (ETC: Sun Oct 22 09:34:33 2023 ; 3 min 51 s 291.97 ms remaining ; 3 h 12 min 44 s 598.34 ms total) 11526400.25 ms (3 h 12 min 6 s 400.25 ms) taken to collect 21395853 D-proofs of length 153. [iterated 234799156 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 3 }, { 9, 4 }, { 11, 7 }, { 13, 10 }, { 15, 13 }, { 17, 16 }, { 19, 26 }, { 21, 36 }, { 23, 42 }, { 25, 54 }, { 27, 80 }, { 29, 100 }, { 31, 126 }, { 33, 162 }, { 35, 221 }, { 37, 282 }, { 39, 359 }, { 41, 454 }, { 43, 615 }, { 45, 778 }, { 47, 1002 }, { 49, 1298 }, { 51, 1678 }, { 53, 2134 }, { 55, 2803 }, { 57, 3534 }, { 59, 4530 }, { 61, 5848 }, { 63, 7496 }, { 65, 9424 }, { 67, 12147 }, { 69, 15402 }, { 71, 19615 }, { 73, 24892 }, { 75, 31620 }, { 77, 39936 }, { 79, 50946 }, { 81, 64168 }, { 83, 81204 }, { 85, 102794 }, { 87, 130094 }, { 89, 163718 }, { 91, 207474 }, { 93, 261220 }, { 95, 329568 }, { 97, 415628 }, { 99, 524144 }, { 101, 658432 }, { 103, 831003 }, { 105, 1044792 }, { 107, 1313760 }, { 109, 1651616 }, { 111, 2077927 }, { 113, 2606646 }, { 115, 3277103 }, { 117, 4112052 }, { 119, 5160229 }, { 121, 6472942 }, { 123, 8122690 }, { 125, 10173684 }, { 127, 12760188 }, { 129, 15985436 }, { 131, 20022824 }, { 133, 25070468 }, { 135, 31402887 }, { 137, 39284338 }, { 139, 49176381 }, { 141, 61517174 }, { 143, 76945234 }, { 145, 96208206 }, { 147, 120320734 }, { 149, 150346484 }, { 151, 187924390 }, { 153, 234799156 } } 159295.60 ms (2 min 39 s 295.60 ms) taken to filter and order new representative proofs. Found 21395853 representative, 21771166 redundant, and 191632137 invalid condensed detachment proof strings. lengths up to 153 ; amounts per length: {(1,1), (3,1), (5,1), (7,1), (9,2), (11,2), (13,2), (15,2), (17,5), (19,5), (21,3), (23,6), (25,10), (27,7), (29,12), (31,14), (33,17), (35,21), (37,30), (39,28), (41,44), (43,56), (45,66), (47,80), (49,108), (51,123), (53,168), (55,197), (57,241), (59,303), (61,390), (63,444), (65,570), (67,707), (69,863), (71,1052), (73,1340), (75,1586), (77,1990), (79,2467), (81,3018), (83,3679), (85,4661), (87,5632), (89,6994), (91,8637), (93,10677), (95,13008), (97,16295), (99,19833), (101,24567), (103,30296), (105,37377), (107,45724), (109,56922), (111,69661), (113,85894), (115,105871), (117,130737), (119,160270), (121,198446), (123,243740), (125,300530), (127,370216), (129,456911), (131,560926), (133,693346), (135,853090), (137,1051251), (139,1294413), (141,1597383), (143,1963944), (145,2423655), (147,2983754), (149,3676539), (151,4527348), (153,21395853)} ; 21395853 new representative proofs (21771166 redundant, 191632137 invalid) Sun Oct 22 09:36:52 2023: Starting to write 21395853 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. 49147.43 ms (49 s 147.43 ms) taken to print and save 13257500572 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. Sun Oct 22 09:38:08 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 153, unfiltered] Sun Oct 22 09:39:28 2023: Process terminated. [pid: 120923, tid:23140340451200]