( 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: 2.90333… h CPU utilization: 139.36 core-h ) Sun Oct 8 13:15:54 2023: Process started. [pid: 207019, tid:22511623939968] Tasks: 1. resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true) 2. generateDProofRepresentativeFiles(39, false, true) [Main] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff] (1) C0CC1C0.2CCN2CCN3.4.1C3.2 - CpCCqCprCCNrCCNstqCsr - 0\imply((1\imply(0\imply2))\imply((\not2\imply((\not3\imply4)\imply1))\imply(3\imply2))) [Main] Calling generateDProofRepresentativeFiles(39, false, true). Sun Oct 8 13:15:54 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 39, unfiltered] 0.03 ms taken to load initial representatives. 3.39 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:22511563691776] 0.07 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:22511561590528] 0.02 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:22511467099904] 0.08 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:22511559489280] 0.10 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:22511557388032] 33.51 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:22511555286784] 58.57 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:22511553185536] 1.82 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:22511551084288] 3.19 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:22511548983040] 14.53 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:22511546881792] 67.12 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:22511544780544] 463.93 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:22511542679296] 3505.03 ms (3 s 505.03 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:22511540578048] 349.90 ms taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:22511538476800] 1028.77 ms (1 s 28.77 ms) taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:22511536375552] 2643.13 ms (2 s 643.13 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:22511464998656] 5490.38 ms (5 s 490.38 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:22511462897408] 12929.13 ms (12 s 929.13 ms) taken to read 5081180 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt. [tid:22511460796160] 12942.70 ms (12 s 942.70 ms) total read duration. Loaded 19 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 5 9 : 10 11 : 24 13 : 57 15 : 137 17 : 339 19 : 854 21 : 2171 23 : 5583 25 : 14478 27 : 37874 29 : 99756 31 : 264466 33 : 705026 35 : 1888450 37 : 5081180 8100414 representatives in total. Sun Oct 8 13:16:08 2023: Inserted ≈ 5% of D-proof conclusions. [ 405020 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 17 s 323.53 ms remaining ; 18 s 235.29 ms total) Sun Oct 8 13:16:09 2023: Inserted ≈10% of D-proof conclusions. [ 810041 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 17 s 954.22 ms remaining ; 19 s 949.13 ms total) Sun Oct 8 13:16:10 2023: Inserted ≈15% of D-proof conclusions. [1215062 of 8100414] (ETC: Sun Oct 8 13:16:28 2023 ; 17 s 836.37 ms remaining ; 20 s 983.97 ms total) Sun Oct 8 13:16:11 2023: Inserted ≈20% of D-proof conclusions. [1620082 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 15 s 805.54 ms remaining ; 19 s 756.92 ms total) Sun Oct 8 13:16:12 2023: Inserted ≈25% of D-proof conclusions. [2025103 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 14 s 622.16 ms remaining ; 19 s 496.22 ms total) Sun Oct 8 13:16:13 2023: Inserted ≈30% of D-proof conclusions. [2430124 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 13 s 820.69 ms remaining ; 19 s 743.84 ms total) Sun Oct 8 13:16:14 2023: Inserted ≈35% of D-proof conclusions. [2835144 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 12 s 802.36 ms remaining ; 19 s 695.94 ms total) Sun Oct 8 13:16:15 2023: Inserted ≈40% of D-proof conclusions. [3240165 of 8100414] (ETC: Sun Oct 8 13:16:27 2023 ; 11 s 688.96 ms remaining ; 19 s 481.60 ms total) Sun Oct 8 13:16:16 2023: Inserted ≈45% of D-proof conclusions. [3645186 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 10 s 405.75 ms remaining ; 18 s 919.54 ms total) Sun Oct 8 13:16:17 2023: Inserted ≈50% of D-proof conclusions. [4050207 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 9 s 318.28 ms remaining ; 18 s 636.55 ms total) Sun Oct 8 13:16:17 2023: Inserted ≈55% of D-proof conclusions. [4455227 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 8 s 234.45 ms remaining ; 18 s 298.77 ms total) Sun Oct 8 13:16:18 2023: Inserted ≈60% of D-proof conclusions. [4860248 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 7 s 289.67 ms remaining ; 18 s 224.16 ms total) Sun Oct 8 13:16:19 2023: Inserted ≈65% of D-proof conclusions. [5265269 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 6 s 352.41 ms remaining ; 18 s 149.73 ms total) Sun Oct 8 13:16:20 2023: Inserted ≈70% of D-proof conclusions. [5670289 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 5 s 493.87 ms remaining ; 18 s 312.88 ms total) Sun Oct 8 13:16:21 2023: Inserted ≈75% of D-proof conclusions. [6075310 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 4 s 550.30 ms remaining ; 18 s 201.21 ms total) Sun Oct 8 13:16:22 2023: Inserted ≈80% of D-proof conclusions. [6480331 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 3 s 644.20 ms remaining ; 18 s 221.02 ms total) Sun Oct 8 13:16:23 2023: Inserted ≈85% of D-proof conclusions. [6885351 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 2 s 729.75 ms remaining ; 18 s 198.36 ms total) Sun Oct 8 13:16:24 2023: Inserted ≈90% of D-proof conclusions. [7290372 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 1 s 851.35 ms remaining ; 18 s 513.50 ms total) Sun Oct 8 13:16:25 2023: Inserted ≈95% of D-proof conclusions. [7695393 of 8100414] (ETC: Sun Oct 8 13:16:26 2023 ; 918.67 ms remaining ; 18 s 373.49 ms total) Sun Oct 8 13:16:25 2023: Inserted 100% of D-proof conclusions. [8100414 of 8100414] (ETC: Sun Oct 8 13:16:25 2023 ; 0.00 ms remaining ; 18 s 212.27 ms total) 18212.47 ms (18 s 212.47 ms) total insertion duration. Estimated iteration count set to 28511026, based on entry 37:10505128 and last known pair (35:3870703, 37:10505128) with 10505128/3870703 ≈ 2.71401 and 10505128 * (10505128/3870703)^1 ≈ 28511026.11. Sun Oct 8 13:16:25 2023: Starting to generate D-proof representatives of length 39. Sun Oct 8 13:19:09 2023: Iterated ≈ 2% of D-proof candidates. [ 570220 of approximately 28511026] (ETC: Sun Oct 8 15:32:32 2023 ; 2 h 13 min 23 s 342.33 ms remaining ; 2 h 16 min 6 s 675.70 ms total) Sun Oct 8 13:21:56 2023: Iterated ≈ 4% of D-proof candidates. [ 1140441 of approximately 28511026] (ETC: Sun Oct 8 15:34:09 2023 ; 2 h 12 min 12 s 848.23 ms remaining ; 2 h 17 min 43 s 383.56 ms total) Sun Oct 8 13:25:23 2023: Iterated ≈ 6% of D-proof candidates. [ 1710661 of approximately 28511026] (ETC: Sun Oct 8 15:45:47 2023 ; 2 h 20 min 23 s 851.47 ms remaining ; 2 h 29 min 21 s 543.93 ms total) Sun Oct 8 13:28:39 2023: Iterated ≈ 8% of D-proof candidates. [ 2280882 of approximately 28511026] (ETC: Sun Oct 8 15:49:09 2023 ; 2 h 20 min 30 s 171.71 ms remaining ; 2 h 32 min 43 s 230.10 ms total) Sun Oct 8 13:31:45 2023: Iterated ≈ 10% of D-proof candidates. [ 2851102 of approximately 28511026] (ETC: Sun Oct 8 15:49:41 2023 ; 2 h 17 min 55 s 789.58 ms remaining ; 2 h 33 min 15 s 321.54 ms total) Sun Oct 8 13:35:10 2023: Iterated ≈ 12% of D-proof candidates. [ 3421323 of approximately 28511026] (ETC: Sun Oct 8 15:52:35 2023 ; 2 h 17 min 25 s 531.48 ms remaining ; 2 h 36 min 9 s 922.09 ms total) Sun Oct 8 13:38:45 2023: Iterated ≈ 14% of D-proof candidates. [ 3991543 of approximately 28511026] (ETC: Sun Oct 8 15:55:53 2023 ; 2 h 17 min 8 s 197.65 ms remaining ; 2 h 39 min 27 s 671.43 ms total) Sun Oct 8 13:43:27 2023: Iterated ≈ 16% of D-proof candidates. [ 4561764 of approximately 28511026] (ETC: Sun Oct 8 16:05:18 2023 ; 2 h 21 min 50 s 919.78 ms remaining ; 2 h 48 min 52 s 47.29 ms total) Sun Oct 8 13:47:24 2023: Iterated ≈ 18% of D-proof candidates. [ 5131984 of approximately 28511026] (ETC: Sun Oct 8 16:08:28 2023 ; 2 h 21 min 4 s 550.64 ms remaining ; 2 h 52 min 2 s 622.43 ms total) Sun Oct 8 13:52:48 2023: Iterated ≈ 20% of D-proof candidates. [ 5702205 of approximately 28511026] (ETC: Sun Oct 8 16:18:21 2023 ; 2 h 25 min 32 s 72.96 ms remaining ; 3 h 1 min 55 s 91.10 ms total) Sun Oct 8 13:58:20 2023: Iterated ≈ 22% of D-proof candidates. [ 6272425 of approximately 28511026] (ETC: Sun Oct 8 16:26:56 2023 ; 2 h 28 min 35 s 473.04 ms remaining ; 3 h 10 min 30 s 93.27 ms total) Sun Oct 8 14:04:35 2023: Iterated ≈ 24% of D-proof candidates. [ 6842646 of approximately 28511026] (ETC: Sun Oct 8 16:37:05 2023 ; 2 h 32 min 30 s 145.33 ms remaining ; 3 h 20 min 39 s 664.78 ms total) Sun Oct 8 14:09:17 2023: Iterated ≈ 26% of D-proof candidates. [ 7412866 of approximately 28511026] (ETC: Sun Oct 8 16:39:43 2023 ; 2 h 30 min 26 s 333.17 ms remaining ; 3 h 23 min 17 s 747.08 ms total) Sun Oct 8 14:13:11 2023: Iterated ≈ 28% of D-proof candidates. [ 7983087 of approximately 28511026] (ETC: Sun Oct 8 16:39:09 2023 ; 2 h 25 min 57 s 756.32 ms remaining ; 3 h 22 min 43 s 550.28 ms total) Sun Oct 8 14:17:22 2023: Iterated ≈ 30% of D-proof candidates. [ 8553307 of approximately 28511026] (ETC: Sun Oct 8 16:39:33 2023 ; 2 h 22 min 11 s 281.83 ms remaining ; 3 h 23 min 7 s 544.99 ms total) Sun Oct 8 14:22:12 2023: Iterated ≈ 32% of D-proof candidates. [ 9123528 of approximately 28511026] (ETC: Sun Oct 8 16:41:59 2023 ; 2 h 19 min 46 s 958.02 ms remaining ; 3 h 25 min 33 s 761.60 ms total) Sun Oct 8 14:27:25 2023: Iterated ≈ 34% of D-proof candidates. [ 9693748 of approximately 28511026] (ETC: Sun Oct 8 16:45:14 2023 ; 2 h 17 min 49 s 9.63 ms remaining ; 3 h 28 min 48 s 801.91 ms total) Sun Oct 8 14:32:01 2023: Iterated ≈ 36% of D-proof candidates. [10263969 of approximately 28511026] (ETC: Sun Oct 8 16:46:26 2023 ; 2 h 14 min 24 s 61.73 ms remaining ; 3 h 30 min 96.20 ms total) Sun Oct 8 14:37:16 2023: Iterated ≈ 38% of D-proof candidates. [10834189 of approximately 28511026] (ETC: Sun Oct 8 16:49:10 2023 ; 2 h 11 min 53 s 799.14 ms remaining ; 3 h 32 min 44 s 191.53 ms total) Sun Oct 8 14:41:57 2023: Iterated ≈ 40% of D-proof candidates. [11404410 of approximately 28511026] (ETC: Sun Oct 8 16:50:15 2023 ; 2 h 8 min 17 s 563.16 ms remaining ; 3 h 33 min 49 s 271.63 ms total) Sun Oct 8 14:46:24 2023: Iterated ≈ 42% of D-proof candidates. [11974630 of approximately 28511026] (ETC: Sun Oct 8 16:50:40 2023 ; 2 h 4 min 15 s 660.72 ms remaining ; 3 h 34 min 14 s 586.73 ms total) Sun Oct 8 14:50:22 2023: Iterated ≈ 44% of D-proof candidates. [12544851 of approximately 28511026] (ETC: Sun Oct 8 16:49:55 2023 ; 1 h 59 min 33 s 428.46 ms remaining ; 3 h 33 min 29 s 693.32 ms total) Sun Oct 8 14:53:55 2023: Iterated ≈ 46% of D-proof candidates. [13115071 of approximately 28511026] (ETC: Sun Oct 8 16:48:22 2023 ; 1 h 54 min 26 s 856.99 ms remaining ; 3 h 31 min 56 s 401.04 ms total) Sun Oct 8 14:57:26 2023: Iterated ≈ 48% of D-proof candidates. [13685292 of approximately 28511026] (ETC: Sun Oct 8 16:46:52 2023 ; 1 h 49 min 26 s 37.15 ms remaining ; 3 h 30 min 26 s 994.10 ms total) Sun Oct 8 15:01:05 2023: Iterated ≈ 50% of D-proof candidates. [14255513 of approximately 28511026] (ETC: Sun Oct 8 16:45:46 2023 ; 1 h 44 min 40 s 40.45 ms remaining ; 3 h 29 min 20 s 80.90 ms total) Sun Oct 8 15:04:37 2023: Iterated ≈ 52% of D-proof candidates. [14825733 of approximately 28511026] (ETC: Sun Oct 8 16:44:29 2023 ; 1 h 39 min 52 s 331.26 ms remaining ; 3 h 28 min 4 s 22.99 ms total) Sun Oct 8 15:08:07 2023: Iterated ≈ 54% of D-proof candidates. [15395954 of approximately 28511026] (ETC: Sun Oct 8 16:43:16 2023 ; 1 h 35 min 8 s 625.01 ms remaining ; 3 h 26 min 50 s 54.34 ms total) Sun Oct 8 15:11:33 2023: Iterated ≈ 56% of D-proof candidates. [15966174 of approximately 28511026] (ETC: Sun Oct 8 16:42:00 2023 ; 1 h 30 min 27 s 333.10 ms remaining ; 3 h 25 min 34 s 847.40 ms total) Sun Oct 8 15:14:45 2023: Iterated ≈ 58% of D-proof candidates. [16536395 of approximately 28511026] (ETC: Sun Oct 8 16:40:26 2023 ; 1 h 25 min 40 s 829.86 ms remaining ; 3 h 24 min 71.02 ms total) Sun Oct 8 15:17:49 2023: Iterated ≈ 60% of D-proof candidates. [17106615 of approximately 28511026] (ETC: Sun Oct 8 16:38:44 2023 ; 1 h 20 min 55 s 384.53 ms remaining ; 3 h 22 min 18 s 460.68 ms total) Sun Oct 8 15:20:52 2023: Iterated ≈ 62% of D-proof candidates. [17676836 of approximately 28511026] (ETC: Sun Oct 8 16:37:09 2023 ; 1 h 16 min 16 s 564.77 ms remaining ; 3 h 20 min 43 s 591.38 ms total) Sun Oct 8 15:23:59 2023: Iterated ≈ 64% of D-proof candidates. [18247056 of approximately 28511026] (ETC: Sun Oct 8 16:35:44 2023 ; 1 h 11 min 45 s 126.85 ms remaining ; 3 h 19 min 18 s 684.96 ms total) Sun Oct 8 15:27:07 2023: Iterated ≈ 66% of D-proof candidates. [18817277 of approximately 28511026] (ETC: Sun Oct 8 16:34:27 2023 ; 1 h 7 min 19 s 704.78 ms remaining ; 3 h 18 min 1 s 484.44 ms total) Sun Oct 8 15:30:14 2023: Iterated ≈ 68% of D-proof candidates. [19387497 of approximately 28511026] (ETC: Sun Oct 8 16:33:12 2023 ; 1 h 2 min 58 s 36.49 ms remaining ; 3 h 16 min 46 s 363.15 ms total) Sun Oct 8 15:33:04 2023: Iterated ≈ 70% of D-proof candidates. [19957718 of approximately 28511026] (ETC: Sun Oct 8 16:31:37 2023 ; 58 min 33 s 563.84 ms remaining ; 3 h 15 min 11 s 879.20 ms total) Sun Oct 8 15:35:47 2023: Iterated ≈ 72% of D-proof candidates. [20527938 of approximately 28511026] (ETC: Sun Oct 8 16:29:58 2023 ; 54 min 11 s 591.32 ms remaining ; 3 h 13 min 32 s 825.11 ms total) Sun Oct 8 15:38:23 2023: Iterated ≈ 74% of D-proof candidates. [21098159 of approximately 28511026] (ETC: Sun Oct 8 16:28:16 2023 ; 49 min 52 s 644.66 ms remaining ; 3 h 11 min 50 s 171.42 ms total) Sun Oct 8 15:40:44 2023: Iterated ≈ 76% of D-proof candidates. [21668379 of approximately 28511026] (ETC: Sun Oct 8 16:26:19 2023 ; 45 min 34 s 384.26 ms remaining ; 3 h 9 min 53 s 266.50 ms total) Sun Oct 8 15:43:09 2023: Iterated ≈ 78% of D-proof candidates. [22238600 of approximately 28511026] (ETC: Sun Oct 8 16:24:33 2023 ; 41 min 23 s 184.17 ms remaining ; 3 h 8 min 7 s 200.27 ms total) Sun Oct 8 15:45:24 2023: Iterated ≈ 80% of D-proof candidates. [22808820 of approximately 28511026] (ETC: Sun Oct 8 16:22:39 2023 ; 37 min 14 s 644.43 ms remaining ; 3 h 6 min 13 s 220.57 ms total) Sun Oct 8 15:47:34 2023: Iterated ≈ 82% of D-proof candidates. [23379041 of approximately 28511026] (ETC: Sun Oct 8 16:20:45 2023 ; 33 min 10 s 734.77 ms remaining ; 3 h 4 min 19 s 636.94 ms total) Sun Oct 8 15:49:40 2023: Iterated ≈ 84% of D-proof candidates. [23949261 of approximately 28511026] (ETC: Sun Oct 8 16:18:51 2023 ; 29 min 11 s 256.82 ms remaining ; 3 h 2 min 25 s 353.09 ms total) Sun Oct 8 15:51:40 2023: Iterated ≈ 86% of D-proof candidates. [24519482 of approximately 28511026] (ETC: Sun Oct 8 16:16:56 2023 ; 25 min 16 s 298.22 ms remaining ; 3 h 30 s 700.62 ms total) Sun Oct 8 15:53:40 2023: Iterated ≈ 88% of D-proof candidates. [25089702 of approximately 28511026] (ETC: Sun Oct 8 16:15:06 2023 ; 21 min 26 s 472.65 ms remaining ; 2 h 58 min 40 s 602.65 ms total) Sun Oct 8 15:55:37 2023: Iterated ≈ 90% of D-proof candidates. [25659923 of approximately 28511026] (ETC: Sun Oct 8 16:13:18 2023 ; 17 min 41 s 239.27 ms remaining ; 2 h 56 min 52 s 391.25 ms total) Sun Oct 8 15:57:30 2023: Iterated ≈ 92% of D-proof candidates. [26230143 of approximately 28511026] (ETC: Sun Oct 8 16:11:31 2023 ; 14 min 433.32 ms remaining ; 2 h 55 min 5 s 412.30 ms total) Sun Oct 8 15:59:21 2023: Iterated ≈ 94% of D-proof candidates. [26800364 of approximately 28511026] (ETC: Sun Oct 8 16:09:45 2023 ; 10 min 23 s 944.61 ms remaining ; 2 h 53 min 19 s 74.14 ms total) Sun Oct 8 16:01:07 2023: Iterated ≈ 96% of D-proof candidates. [27370584 of approximately 28511026] (ETC: Sun Oct 8 16:07:59 2023 ; 6 min 51 s 749.79 ms remaining ; 2 h 51 min 33 s 736.01 ms total) Sun Oct 8 16:02:54 2023: Iterated ≈ 98% of D-proof candidates. [27940805 of approximately 28511026] (ETC: Sun Oct 8 16:06:17 2023 ; 3 min 23 s 838.08 ms remaining ; 2 h 49 min 51 s 895.52 ms total) Sun Oct 8 16:04:37 2023: Iterated ≈100% of D-proof candidates. [28511026 of approximately 28511026] (ETC: Sun Oct 8 16:04:37 2023 ; 0.00 ms remaining ; 2 h 48 min 11 s 44.59 ms total) 10106799.41 ms (2 h 48 min 26 s 799.41 ms) taken to collect 13863883 D-proofs of length 39. [iterated 28598584 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 14 }, { 11, 34 }, { 13, 88 }, { 15, 227 }, { 17, 584 }, { 19, 1520 }, { 21, 3984 }, { 23, 10492 }, { 25, 27790 }, { 27, 73951 }, { 29, 197716 }, { 31, 530829 }, { 33, 1430830 }, { 35, 3870703 }, { 37, 10505128 }, { 39, 28598584 } } 119037.46 ms (1 min 59 s 37.46 ms) taken to filter and order new representative proofs. Found 13863883 representative, 221118 redundant, and 14513583 invalid condensed detachment proof strings. lengths up to 39 ; amounts per length: {(1,1), (3,1), (5,2), (7,5), (9,10), (11,24), (13,57), (15,137), (17,339), (19,854), (21,2171), (23,5583), (25,14478), (27,37874), (29,99756), (31,264466), (33,705026), (35,1888450), (37,5081180), (39,13863883)} ; 13863883 new representative proofs (221118 redundant, 14513583 invalid) Sun Oct 8 16:06:59 2023: Starting to write 13863883 entries to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs39-unfiltered39+.txt. 105933.18 ms (1 min 45 s 933.18 ms) taken to print and save 27702180806 bytes of representative condensed detachment proof strings to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs39-unfiltered39+.txt. Sun Oct 8 16:09:05 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 39, unfiltered] Sun Oct 8 16:10:06 2023: Process terminated. [pid: 207019, tid:22511623939968]