( This log file was generated by 'pmGenerator 1.1' (c++11 branch; with known iteration counts 35:755567051 and 35:37:2497890936), compiled by 'icpc (ICC) 19.0.1.144 20181018'. The run was executed on a CLAIX-2016 SMP node — 8-socket Intel Xeon E7-8860v4 (Broadwell-EX), 18 cores each (144 cores total per node), 2.2 GHz, 3.2 GHz turbo mode, 1024 GiB main memory — running Linux, CentOS 7.9. Wall-clock time: 102.367222… h CPU utilization: 14740.88 core-h ) Mon May 15 21:57:22 2023: Process started. [pid: 83670, tid:46919538027008] Tasks: 1. generateDProofRepresentativeFiles(37, false, true) [Main] Calling generateDProofRepresentativeFiles(37, false, true). Mon May 15 21:57:22 2023: Limited D-proof representative generator started. [parallel ; 144 hardware thread contexts, limit: 37, unfiltered] 0.14 ms taken to load built-in representatives. 71.39 ms taken to read 5221 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs17.txt. [tid:46919587006208] 41.24 ms taken to read 15275 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs19.txt. [tid:46919589107456] 127.18 ms taken to read 44206 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs21.txt. [tid:46919591208704] 775.41 ms taken to read 129885 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs23.txt. [tid:46919593309952] 6277.89 ms (6 s 277.88 ms) taken to read 385789 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs25.txt. [tid:46919595411200] 2001.46 ms (2 s 1.46 ms) taken to read 1149058 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs27.txt. [tid:46919597512448] 5332.20 ms (5 s 332.20 ms) taken to read 3449251 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs29.txt. [tid:46919599613696] 11933.87 ms (11 s 933.87 ms) taken to read 10411430 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs31.txt. [tid:46919601714944] 22166.00 ms (22 s 166.00 ms) taken to read 31559297 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs33.txt. [tid:46919603816192] 22176.13 ms (22 s 176.13 ms) total read duration. Loaded 17 representative collections of sizes: 1 : 3 3 : 6 5 : 12 7 : 38 9 : 89 11 : 229 13 : 672 15 : 1844 17 : 5221 19 : 15275 21 : 44206 23 : 129885 25 : 385789 27 : 1149058 29 : 3449251 31 : 10411430 33 : 31559297 47152305 representatives in total. 62969.74 ms (1 min 2 s 969.74 ms) taken to read 121473262 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs35-unfiltered35+.txt. [tid:46919603816192] 62972.46 ms (1 min 2 s 972.46 ms) additional read duration. Loaded 1 more representative collection of size: 35 : 121473262 168625567 representatives in total. Mon May 15 21:58:53 2023: Inserted 5% of D-proof conclusions. [ 8431278 of 168625567] (ETC: Mon May 15 22:00:29 2023 ; 1 min 36 s 823.40 ms remaining ; 1 min 41 s 919.36 ms total) Mon May 15 21:58:57 2023: Inserted 10% of D-proof conclusions. [ 16862556 of 168625567] (ETC: Mon May 15 22:00:26 2023 ; 1 min 28 s 404.35 ms remaining ; 1 min 38 s 227.05 ms total) Mon May 15 21:59:02 2023: Inserted 15% of D-proof conclusions. [ 25293835 of 168625567] (ETC: Mon May 15 22:00:22 2023 ; 1 min 20 s 344.10 ms remaining ; 1 min 34 s 522.47 ms total) Mon May 15 21:59:06 2023: Inserted 20% of D-proof conclusions. [ 33725113 of 168625567] (ETC: Mon May 15 22:00:23 2023 ; 1 min 16 s 97.55 ms remaining ; 1 min 35 s 121.93 ms total) Mon May 15 21:59:12 2023: Inserted 25% of D-proof conclusions. [ 42156391 of 168625567] (ETC: Mon May 15 22:00:24 2023 ; 1 min 12 s 710.88 ms remaining ; 1 min 36 s 947.84 ms total) Mon May 15 21:59:17 2023: Inserted 30% of D-proof conclusions. [ 50587670 of 168625567] (ETC: Mon May 15 22:00:25 2023 ; 1 min 8 s 390.26 ms remaining ; 1 min 37 s 700.38 ms total) Mon May 15 21:59:22 2023: Inserted 35% of D-proof conclusions. [ 59018948 of 168625567] (ETC: Mon May 15 22:00:25 2023 ; 1 min 3 s 329.09 ms remaining ; 1 min 37 s 429.37 ms total) Mon May 15 21:59:27 2023: Inserted 40% of D-proof conclusions. [ 67450226 of 168625567] (ETC: Mon May 15 22:00:25 2023 ; 58 s 675.96 ms remaining ; 1 min 37 s 793.27 ms total) Mon May 15 21:59:32 2023: Inserted 45% of D-proof conclusions. [ 75881505 of 168625567] (ETC: Mon May 15 22:00:27 2023 ; 54 s 521.59 ms remaining ; 1 min 39 s 130.16 ms total) Mon May 15 21:59:37 2023: Inserted 50% of D-proof conclusions. [ 84312783 of 168625567] (ETC: Mon May 15 22:00:27 2023 ; 50 s 39.00 ms remaining ; 1 min 40 s 78.00 ms total) Mon May 15 21:59:43 2023: Inserted 55% of D-proof conclusions. [ 92744061 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 45 s 280.58 ms remaining ; 1 min 40 s 623.50 ms total) Mon May 15 21:59:48 2023: Inserted 60% of D-proof conclusions. [101175340 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 40 s 167.33 ms remaining ; 1 min 40 s 418.31 ms total) Mon May 15 21:59:52 2023: Inserted 65% of D-proof conclusions. [109606618 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 35 s 34.90 ms remaining ; 1 min 40 s 99.71 ms total) Mon May 15 21:59:57 2023: Inserted 70% of D-proof conclusions. [118037896 of 168625567] (ETC: Mon May 15 22:00:27 2023 ; 29 s 997.68 ms remaining ; 1 min 39 s 992.28 ms total) Mon May 15 22:00:03 2023: Inserted 75% of D-proof conclusions. [126469175 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 25 s 30.74 ms remaining ; 1 min 40 s 122.98 ms total) Mon May 15 22:00:08 2023: Inserted 80% of D-proof conclusions. [134900453 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 20 s 153.98 ms remaining ; 1 min 40 s 769.88 ms total) Mon May 15 22:00:14 2023: Inserted 85% of D-proof conclusions. [143331731 of 168625567] (ETC: Mon May 15 22:00:29 2023 ; 15 s 211.78 ms remaining ; 1 min 41 s 411.90 ms total) Mon May 15 22:00:18 2023: Inserted 90% of D-proof conclusions. [151763010 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 10 s 95.26 ms remaining ; 1 min 40 s 952.58 ms total) Mon May 15 22:00:23 2023: Inserted 95% of D-proof conclusions. [160194288 of 168625567] (ETC: Mon May 15 22:00:28 2023 ; 5 s 26.99 ms remaining ; 1 min 40 s 539.75 ms total) 100215.80 ms (1 min 40 s 215.80 ms) total insertion duration. Known iteration count loaded from 37:2497890936. Mon May 15 22:00:28 2023: Starting to generate D-proof representatives of length 37. Tue May 16 01:04:32 2023: Iterated 2% of D-proof candidates. [ 49957818 of 2497890936] (ETC: Mon May 22 07:24:20 2023 ; 6 d 6 h 19 min 47 s 853.60 ms remaining ; 6 d 9 h 23 min 52 s 503.51 ms total) Tue May 16 03:51:53 2023: Iterated 4% of D-proof candidates. [ 99915637 of 2497890936] (ETC: Mon May 22 00:26:10 2023 ; 5 d 20 h 34 min 16 s 526.75 ms remaining ; 6 d 2 h 25 min 42 s 215.27 ms total) Tue May 16 06:27:23 2023: Iterated 6% of D-proof candidates. [ 149873456 of 2497890936] (ETC: Sun May 21 18:49:14 2023 ; 5 d 12 h 21 min 50 s 758.97 ms remaining ; 5 d 20 h 48 min 46 s 339.29 ms total) Tue May 16 10:08:46 2023: Iterated 8% of D-proof candidates. [ 199831274 of 2497890936] (ETC: Mon May 22 05:44:16 2023 ; 5 d 19 h 35 min 30 s 178.88 ms remaining ; 6 d 7 h 43 min 48 s 455.09 ms total) Tue May 16 12:47:32 2023: Iterated 10% of D-proof candidates. [ 249789093 of 2497890936] (ETC: Mon May 22 01:51:12 2023 ; 5 d 13 h 3 min 39 s 846.84 ms remaining ; 6 d 3 h 50 min 44 s 274.13 ms total) Tue May 16 15:15:51 2023: Iterated 12% of D-proof candidates. [ 299746912 of 2497890936] (ETC: Sun May 21 21:48:40 2023 ; 5 d 6 h 32 min 49 s 462.70 ms remaining ; 5 d 23 h 48 min 12 s 571.18 ms total) Tue May 16 17:16:10 2023: Iterated 14% of D-proof candidates. [ 349704731 of 2497890936] (ETC: Sun May 21 15:35:31 2023 ; 4 d 22 h 19 min 21 s 208.80 ms remaining ; 5 d 17 h 35 min 3 s 731.16 ms total) Tue May 16 19:30:39 2023: Iterated 16% of D-proof candidates. [ 399662549 of 2497890936] (ETC: Sun May 21 12:24:10 2023 ; 4 d 16 h 53 min 30 s 701.76 ms remaining ; 5 d 14 h 23 min 42 s 263.83 ms total) Tue May 16 21:49:36 2023: Iterated 18% of D-proof candidates. [ 449620368 of 2497890936] (ETC: Sun May 21 10:20:08 2023 ; 4 d 12 h 30 min 31 s 496.98 ms remaining ; 5 d 12 h 19 min 39 s 874.26 ms total) Wed May 17 00:30:28 2023: Iterated 20% of D-proof candidates. [ 499578187 of 2497890936] (ETC: Sun May 21 10:30:28 2023 ; 4 d 10 h 325.78 ms remaining ; 5 d 12 h 30 min 407.18 ms total) Wed May 17 03:25:11 2023: Iterated 22% of D-proof candidates. [ 549536005 of 2497890936] (ETC: Sun May 21 11:41:54 2023 ; 4 d 8 h 16 min 43 s 521.66 ms remaining ; 5 d 13 h 41 min 26 s 566.01 ms total) Wed May 17 05:50:03 2023: Iterated 24% of D-proof candidates. [ 599493824 of 2497890936] (ETC: Sun May 21 10:37:07 2023 ; 4 d 4 h 47 min 3 s 512.67 ms remaining ; 5 d 12 h 36 min 39 s 358.62 ms total) Wed May 17 07:57:23 2023: Iterated 26% of D-proof candidates. [ 649451643 of 2497890936] (ETC: Sun May 21 08:34:48 2023 ; 4 d 37 min 24 s 890.77 ms remaining ; 5 d 10 h 34 min 20 s 663.12 ms total) Wed May 17 10:02:29 2023: Iterated 28% of D-proof candidates. [ 699409462 of 2497890936] (ETC: Sun May 21 06:42:00 2023 ; 3 d 20 h 39 min 30 s 170.54 ms remaining ; 5 d 8 h 41 min 31 s 903.51 ms total) Wed May 17 12:04:22 2023: Iterated 30% of D-proof candidates. [ 749367280 of 2497890936] (ETC: Sun May 21 04:53:29 2023 ; 3 d 16 h 49 min 7 s 25.62 ms remaining ; 5 d 6 h 53 min 1 s 464.97 ms total) Wed May 17 14:24:40 2023: Iterated 32% of D-proof candidates. [ 799325099 of 2497890936] (ETC: Sun May 21 04:16:06 2023 ; 3 d 13 h 51 min 26 s 352.93 ms remaining ; 5 d 6 h 15 min 38 s 754.17 ms total) Wed May 17 16:50:02 2023: Iterated 34% of D-proof candidates. [ 849282918 of 2497890936] (ETC: Sun May 21 03:58:01 2023 ; 3 d 11 h 7 min 59 s 434.78 ms remaining ; 5 d 5 h 57 min 33 s 688.99 ms total) Wed May 17 19:18:03 2023: Iterated 36% of D-proof candidates. [ 899240736 of 2497890936] (ETC: Sun May 21 03:49:18 2023 ; 3 d 8 h 31 min 15 s 526.38 ms remaining ; 5 d 5 h 48 min 50 s 509.69 ms total) Wed May 17 21:26:30 2023: Iterated 38% of D-proof candidates. [ 949198555 of 2497890936] (ETC: Sun May 21 02:50:02 2023 ; 3 d 5 h 23 min 32 s 127.43 ms remaining ; 5 d 4 h 49 min 34 s 398.89 ms total) Wed May 17 23:45:16 2023: Iterated 40% of D-proof candidates. [ 999156374 of 2497890936] (ETC: Sun May 21 02:22:27 2023 ; 3 d 2 h 37 min 11 s 843.24 ms remaining ; 5 d 4 h 21 min 59 s 738.62 ms total) Thu May 18 02:12:42 2023: Iterated 42% of D-proof candidates. [1049114193 of 2497890936] (ETC: Sun May 21 02:18:11 2023 ; 3 d 5 min 28 s 695.14 ms remaining ; 5 d 4 h 17 min 43 s 267.45 ms total) Thu May 18 04:09:22 2023: Iterated 44% of D-proof candidates. [1099072011 of 2497890936] (ETC: Sun May 21 01:04:20 2023 ; 2 d 20 h 54 min 58 s 86.82 ms remaining ; 5 d 3 h 3 min 52 s 297.62 ms total) Thu May 18 06:03:48 2023: Iterated 46% of D-proof candidates. [1149029830 of 2497890936] (ETC: Sat May 20 23:52:03 2023 ; 2 d 17 h 48 min 15 s 761.84 ms remaining ; 5 d 1 h 51 min 35 s 855.07 ms total) Thu May 18 08:12:12 2023: Iterated 48% of D-proof candidates. [1198987649 of 2497890936] (ETC: Sat May 20 23:14:56 2023 ; 2 d 15 h 2 min 43 s 528.11 ms remaining ; 5 d 1 h 14 min 28 s 323.19 ms total) Thu May 18 10:12:59 2023: Iterated 50% of D-proof candidates. [1248945468 of 2497890936] (ETC: Sat May 20 22:25:30 2023 ; 2 d 12 h 12 min 31 s 146.51 ms remaining ; 5 d 25 min 2 s 293.02 ms total) Thu May 18 12:17:23 2023: Iterated 52% of D-proof candidates. [1298903286 of 2497890936] (ETC: Sat May 20 21:46:50 2023 ; 2 d 9 h 29 min 27 s 582.10 ms remaining ; 4 d 23 h 46 min 22 s 462.45 ms total) Thu May 18 14:13:10 2023: Iterated 54% of D-proof candidates. [1348861105 of 2497890936] (ETC: Sat May 20 20:55:06 2023 ; 2 d 6 h 41 min 55 s 883.79 ms remaining ; 4 d 22 h 54 min 38 s 8.08 ms total) Thu May 18 16:02:13 2023: Iterated 56% of D-proof candidates. [1398818924 of 2497890936] (ETC: Sat May 20 19:55:02 2023 ; 2 d 3 h 52 min 48 s 499.78 ms remaining ; 4 d 21 h 54 min 33 s 863.08 ms total) Thu May 18 17:53:35 2023: Iterated 58% of D-proof candidates. [1448776742 of 2497890936] (ETC: Sat May 20 19:03:05 2023 ; 2 d 1 h 9 min 30 s 23.48 ms remaining ; 4 d 21 h 2 min 37 s 198.41 ms total) Thu May 18 19:40:41 2023: Iterated 60% of D-proof candidates. [1498734561 of 2497890936] (ETC: Sat May 20 18:07:30 2023 ; 1 d 22 h 26 min 48 s 932.42 ms remaining ; 4 d 20 h 7 min 2 s 330.80 ms total) Thu May 18 21:28:33 2023: Iterated 62% of D-proof candidates. [1548692380 of 2497890936] (ETC: Sat May 20 17:16:44 2023 ; 1 d 19 h 48 min 10 s 869.86 ms remaining ; 4 d 19 h 16 min 15 s 973.16 ms total) Thu May 18 23:08:23 2023: Iterated 64% of D-proof candidates. [1598650199 of 2497890936] (ETC: Sat May 20 16:16:35 2023 ; 1 d 17 h 8 min 12 s 392.46 ms remaining ; 4 d 18 h 16 min 7 s 756.81 ms total) Fri May 19 00:48:09 2023: Iterated 66% of D-proof candidates. [1648608017 of 2497890936] (ETC: Sat May 20 15:19:59 2023 ; 1 d 14 h 31 min 50 s 262.80 ms remaining ; 4 d 17 h 19 min 31 s 360.82 ms total) Fri May 19 02:24:12 2023: Iterated 68% of D-proof candidates. [1698565836 of 2497890936] (ETC: Sat May 20 14:21:16 2023 ; 1 d 11 h 57 min 3 s 381.91 ms remaining ; 4 d 16 h 20 min 48 s 68.22 ms total) Fri May 19 04:09:53 2023: Iterated 70% of D-proof candidates. [1748523655 of 2497890936] (ETC: Sat May 20 13:39:38 2023 ; 1 d 9 h 29 min 45 s 145.01 ms remaining ; 4 d 15 h 39 min 10 s 483.25 ms total) Fri May 19 05:45:37 2023: Iterated 72% of D-proof candidates. [1798481473 of 2497890936] (ETC: Sat May 20 12:46:31 2023 ; 1 d 7 h 53 s 733.96 ms remaining ; 4 d 14 h 46 min 3 s 335.04 ms total) Fri May 19 07:21:16 2023: Iterated 74% of D-proof candidates. [1848439292 of 2497890936] (ETC: Sat May 20 11:56:08 2023 ; 1 d 4 h 34 min 52 s 510.64 ms remaining ; 4 d 13 h 55 min 40 s 425.16 ms total) Fri May 19 08:58:17 2023: Iterated 76% of D-proof candidates. [1898397111 of 2497890936] (ETC: Sat May 20 11:10:14 2023 ; 1 d 2 h 11 min 56 s 615.41 ms remaining ; 4 d 13 h 9 min 45 s 897.30 ms total) Fri May 19 10:31:01 2023: Iterated 78% of D-proof candidates. [1948354930 of 2497890936] (ETC: Sat May 20 10:21:10 2023 ; 23 h 50 min 9 s 404.07 ms remaining ; 4 d 12 h 20 min 42 s 745.74 ms total) Fri May 19 12:03:36 2023: Iterated 80% of D-proof candidates. [1998312748 of 2497890936] (ETC: Sat May 20 09:34:23 2023 ; 21 h 30 min 47 s 94.07 ms remaining ; 4 d 11 h 33 min 55 s 469.71 ms total) Fri May 19 13:29:16 2023: Iterated 82% of D-proof candidates. [2048270567 of 2497890936] (ETC: Sat May 20 08:41:27 2023 ; 19 h 12 min 10 s 713.89 ms remaining ; 4 d 10 h 40 min 59 s 521.16 ms total) Fri May 19 14:55:04 2023: Iterated 84% of D-proof candidates. [2098228386 of 2497890936] (ETC: Sat May 20 07:51:11 2023 ; 16 h 56 min 6 s 965.56 ms remaining ; 4 d 9 h 50 min 43 s 534.51 ms total) Fri May 19 16:17:27 2023: Iterated 86% of D-proof candidates. [2148186204 of 2497890936] (ETC: Sat May 20 06:59:17 2023 ; 14 h 41 min 50 s 83.34 ms remaining ; 4 d 8 h 58 min 49 s 165.68 ms total) Fri May 19 17:39:59 2023: Iterated 88% of D-proof candidates. [2198144023 of 2497890936] (ETC: Sat May 20 06:09:55 2023 ; 12 h 29 min 56 s 76.55 ms remaining ; 4 d 8 h 9 min 27 s 303.74 ms total) Fri May 19 18:56:54 2023: Iterated 90% of D-proof candidates. [2248101842 of 2497890936] (ETC: Sat May 20 05:16:30 2023 ; 10 h 19 min 36 s 252.55 ms remaining ; 4 d 7 h 16 min 2 s 524.88 ms total) Fri May 19 20:13:59 2023: Iterated 92% of D-proof candidates. [2298059661 of 2497890936] (ETC: Sat May 20 04:25:36 2023 ; 8 h 11 min 36 s 638.17 ms remaining ; 4 d 6 h 25 min 7 s 976.90 ms total) Fri May 19 21:31:13 2023: Iterated 94% of D-proof candidates. [2348017479 of 2497890936] (ETC: Sat May 20 03:37:01 2023 ; 6 h 5 min 47 s 601.91 ms remaining ; 4 d 5 h 36 min 33 s 363.19 ms total) Fri May 19 22:52:12 2023: Iterated 96% of D-proof candidates. [2397975298 of 2497890936] (ETC: Sat May 20 02:54:21 2023 ; 4 h 2 min 9 s 333.54 ms remaining ; 4 d 4 h 53 min 53 s 336.47 ms total) Sat May 20 00:10:31 2023: Iterated 98% of D-proof candidates. [2447933117 of 2497890936] (ETC: Sat May 20 02:10:43 2023 ; 2 h 12 s 314.20 ms remaining ; 4 d 4 h 10 min 15 s 707.93 ms total) 358060928.49 ms (4 d 3 h 27 min 40 s 928.49 ms) taken to collect 424088648 D-proofs of length 37. [iterated 2497890936 condensed detachment proof strings] [Copy] Static filtered iteration counts: { { 1, 3 }, { 3, 9 }, { 5, 36 }, { 7, 108 }, { 9, 372 }, { 11, 1134 }, { 13, 3354 }, { 15, 10360 }, { 17, 31388 }, { 19, 94907 }, { 21, 290392 }, { 23, 886041 }, { 25, 2709186 }, { 27, 8320672 }, { 29, 25589216 }, { 31, 78896376 }, { 33, 243907474 }, { 35, 755567051 } } [Copy] Static unfiltered iteration counts: { 35, { { 37, 2497890936 } } }, 7015322.52 ms (1 h 56 min 55 s 322.52 ms) taken to filter and order new representative proofs. Found 424088648 representative, 977225433 redundant, and 1096576855 invalid condensed detachment proof strings. lengths up to 37 ; amounts per length: {(1,3), (3,6), (5,12), (7,38), (9,89), (11,229), (13,672), (15,1844), (17,5221), (19,15275), (21,44206), (23,129885), (25,385789), (27,1149058), (29,3449251), (31,10411430), (33,31559297), (35,121473262), (37,424088648)} ; 424088648 new representative proofs (977225433 redundant, 1096576855 invalid) Sat May 20 03:29:26 2023: Starting to write 424088648 entries to data/dProofs-withConclusions/dProofs37-unfiltered35+.txt. 898382.23 ms (14 min 58 s 382.23 ms) taken to print and save 95571571048 bytes of representative condensed detachment proof strings to data/dProofs-withConclusions/dProofs37-unfiltered35+.txt. Sat May 20 03:50:33 2023: Limited D-proof representative generator complete. [parallel ; 144 hardware thread contexts, limit: 37, unfiltered] Sat May 20 04:19:24 2023: Process terminated. [pid: 83670, tid:46919538027008]