-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs35-unfiltered33+_48cpu.log
126 lines (125 loc) · 16.5 KB
/
dProofs35-unfiltered33+_48cpu.log
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
( This log file was generated by 'pmGenerator 1.1' (master branch; without known iteration count 33:37:2703737502), compiled by 'GCC: (GNU) 11.3.0'.
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.7.
Wall-clock time: 6.8558333… h
CPU utilization: 329.08 core-h )
Sat May 6 08:52:08 2023: Process started. [pid: 1346668, tid:22757167990656]
Tasks:
1. generateDProofRepresentativeFiles(35, false, true)
[Main] Calling generateDProofRepresentativeFiles(35, false, true).
Sat May 6 08:52:08 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 35, unfiltered]
0.29 ms taken to load built-in representatives.
39.64 ms taken to read 5221 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs17.txt. [tid:22757115471616]
53.64 ms taken to read 15275 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs19.txt. [tid:22757113370368]
133.45 ms taken to read 44206 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs21.txt. [tid:22757111269120]
712.06 ms taken to read 129885 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs23.txt. [tid:22757109167872]
6061.07 ms (6 s 61.07 ms) taken to read 385789 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs25.txt. [tid:22757107066624]
797.07 ms taken to read 1149058 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs27.txt. [tid:22757104965376]
1701.20 ms (1 s 701.20 ms) taken to read 3449251 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs29.txt. [tid:22757102864128]
4277.58 ms (4 s 277.58 ms) taken to read 10411430 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs31.txt. [tid:22757100762880]
6066.96 ms (6 s 66.96 ms) total read duration.
Loaded 16 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
15593008 representatives in total.
15294.50 ms (15 s 294.50 ms) taken to read 39933795 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs33-unfiltered33+.txt. [tid:22757100762880]
15304.25 ms (15 s 304.25 ms) additional read duration.
Loaded 1 more representative collection of size:
33 : 39933795
55526803 representatives in total.
Sat May 6 08:52:31 2023: Inserted 5% of D-proof conclusions. [ 2776340 of 55526803] (ETC: Sat May 6 08:53:00 2023 ; 29 s 330.55 ms remaining ; 30 s 874.26 ms total)
Sat May 6 08:52:32 2023: Inserted 10% of D-proof conclusions. [ 5552680 of 55526803] (ETC: Sat May 6 08:53:01 2023 ; 28 s 696.13 ms remaining ; 31 s 884.59 ms total)
Sat May 6 08:52:34 2023: Inserted 15% of D-proof conclusions. [ 8329020 of 55526803] (ETC: Sat May 6 08:53:02 2023 ; 27 s 907.65 ms remaining ; 32 s 832.53 ms total)
Sat May 6 08:52:36 2023: Inserted 20% of D-proof conclusions. [11105360 of 55526803] (ETC: Sat May 6 08:53:03 2023 ; 27 s 187.15 ms remaining ; 33 s 983.94 ms total)
Sat May 6 08:52:37 2023: Inserted 25% of D-proof conclusions. [13881700 of 55526803] (ETC: Sat May 6 08:53:03 2023 ; 25 s 376.57 ms remaining ; 33 s 835.43 ms total)
Sat May 6 08:52:39 2023: Inserted 30% of D-proof conclusions. [16658040 of 55526803] (ETC: Sat May 6 08:53:02 2023 ; 23 s 161.45 ms remaining ; 33 s 87.79 ms total)
Sat May 6 08:52:40 2023: Inserted 35% of D-proof conclusions. [19434381 of 55526803] (ETC: Sat May 6 08:53:01 2023 ; 20 s 528.92 ms remaining ; 31 s 582.96 ms total)
Sat May 6 08:52:41 2023: Inserted 40% of D-proof conclusions. [22210721 of 55526803] (ETC: Sat May 6 08:52:59 2023 ; 18 s 227.38 ms remaining ; 30 s 378.96 ms total)
Sat May 6 08:52:42 2023: Inserted 45% of D-proof conclusions. [24987061 of 55526803] (ETC: Sat May 6 08:52:58 2023 ; 16 s 148.66 ms remaining ; 29 s 361.20 ms total)
Sat May 6 08:52:43 2023: Inserted 50% of D-proof conclusions. [27763401 of 55526803] (ETC: Sat May 6 08:52:57 2023 ; 14 s 200.68 ms remaining ; 28 s 401.35 ms total)
Sat May 6 08:52:44 2023: Inserted 55% of D-proof conclusions. [30539741 of 55526803] (ETC: Sat May 6 08:52:57 2023 ; 12 s 402.92 ms remaining ; 27 s 562.03 ms total)
Sat May 6 08:52:45 2023: Inserted 60% of D-proof conclusions. [33316081 of 55526803] (ETC: Sat May 6 08:52:56 2023 ; 10 s 804.89 ms remaining ; 27 s 12.21 ms total)
Sat May 6 08:52:46 2023: Inserted 65% of D-proof conclusions. [36092421 of 55526803] (ETC: Sat May 6 08:52:56 2023 ; 9 s 429.15 ms remaining ; 26 s 940.44 ms total)
Sat May 6 08:52:48 2023: Inserted 70% of D-proof conclusions. [38868762 of 55526803] (ETC: Sat May 6 08:52:56 2023 ; 8 s 12.28 ms remaining ; 26 s 707.60 ms total)
Sat May 6 08:52:49 2023: Inserted 75% of D-proof conclusions. [41645102 of 55526803] (ETC: Sat May 6 08:52:55 2023 ; 6 s 600.41 ms remaining ; 26 s 401.65 ms total)
Sat May 6 08:52:50 2023: Inserted 80% of D-proof conclusions. [44421442 of 55526803] (ETC: Sat May 6 08:52:55 2023 ; 5 s 238.47 ms remaining ; 26 s 192.35 ms total)
Sat May 6 08:52:51 2023: Inserted 85% of D-proof conclusions. [47197782 of 55526803] (ETC: Sat May 6 08:52:55 2023 ; 3 s 884.65 ms remaining ; 25 s 897.63 ms total)
Sat May 6 08:52:52 2023: Inserted 90% of D-proof conclusions. [49974122 of 55526803] (ETC: Sat May 6 08:52:55 2023 ; 2 s 560.60 ms remaining ; 25 s 606.04 ms total)
Sat May 6 08:52:53 2023: Inserted 95% of D-proof conclusions. [52750462 of 55526803] (ETC: Sat May 6 08:52:54 2023 ; 1 s 267.47 ms remaining ; 25 s 349.47 ms total)
25109.67 ms (25 s 109.67 ms) total insertion duration.
Known iteration count loaded from 35:805814039.
Sat May 6 08:52:54 2023: Starting to generate D-proof representatives of length 35.
Sat May 6 09:01:40 2023: Iterated 2% of D-proof candidates. [ 16116280 of 805814039] (ETC: Sat May 6 16:11:24 2023 ; 7 h 9 min 44 s 203.42 ms remaining ; 7 h 18 min 30 s 411.62 ms total)
Sat May 6 09:09:32 2023: Iterated 4% of D-proof candidates. [ 32232561 of 805814039] (ETC: Sat May 6 15:48:35 2023 ; 6 h 39 min 3 s 610.42 ms remaining ; 6 h 55 min 41 s 260.83 ms total)
Sat May 6 09:16:54 2023: Iterated 6% of D-proof candidates. [ 48348842 of 805814039] (ETC: Sat May 6 15:32:51 2023 ; 6 h 15 min 57 s 124.77 ms remaining ; 6 h 39 min 56 s 941.24 ms total)
Sat May 6 09:27:49 2023: Iterated 8% of D-proof candidates. [ 64465123 of 805814039] (ETC: Sat May 6 16:09:23 2023 ; 6 h 41 min 34 s 218.64 ms remaining ; 7 h 16 min 29 s 368.09 ms total)
Sat May 6 09:36:46 2023: Iterated 10% of D-proof candidates. [ 80581403 of 805814039] (ETC: Sat May 6 16:11:32 2023 ; 6 h 34 min 46 s 258.51 ms remaining ; 7 h 18 min 38 s 64.98 ms total)
Sat May 6 09:45:20 2023: Iterated 12% of D-proof candidates. [ 96697684 of 805814039] (ETC: Sat May 6 16:09:47 2023 ; 6 h 24 min 27 s 389.27 ms remaining ; 7 h 16 min 52 s 942.33 ms total)
Sat May 6 09:52:55 2023: Iterated 14% of D-proof candidates. [112813965 of 805814039] (ETC: Sat May 6 16:01:36 2023 ; 6 h 8 min 40 s 535.83 ms remaining ; 7 h 8 min 41 s 553.28 ms total)
Sat May 6 10:01:19 2023: Iterated 16% of D-proof candidates. [128930246 of 805814039] (ETC: Sat May 6 16:00:31 2023 ; 5 h 59 min 11 s 470.33 ms remaining ; 7 h 7 min 36 s 512.29 ms total)
Sat May 6 10:11:01 2023: Iterated 18% of D-proof candidates. [145046527 of 805814039] (ETC: Sat May 6 16:06:51 2023 ; 5 h 55 min 50 s 602.93 ms remaining ; 7 h 13 min 57 s 320.64 ms total)
Sat May 6 10:20:28 2023: Iterated 20% of D-proof candidates. [161162807 of 805814039] (ETC: Sat May 6 16:10:45 2023 ; 5 h 50 min 16 s 774.07 ms remaining ; 7 h 17 min 50 s 967.56 ms total)
Sat May 6 10:30:33 2023: Iterated 22% of D-proof candidates. [177279088 of 805814039] (ETC: Sat May 6 16:16:46 2023 ; 5 h 46 min 12 s 720.75 ms remaining ; 7 h 23 min 51 s 693.24 ms total)
Sat May 6 10:39:16 2023: Iterated 24% of D-proof candidates. [193395369 of 805814039] (ETC: Sat May 6 16:16:06 2023 ; 5 h 36 min 49 s 679.35 ms remaining ; 7 h 23 min 11 s 683.34 ms total)
Sat May 6 10:47:12 2023: Iterated 26% of D-proof candidates. [209511650 of 805814039] (ETC: Sat May 6 16:12:32 2023 ; 5 h 25 min 19 s 440.03 ms remaining ; 7 h 19 min 37 s 621.66 ms total)
Sat May 6 10:55:04 2023: Iterated 28% of D-proof candidates. [225627930 of 805814039] (ETC: Sat May 6 16:09:12 2023 ; 5 h 14 min 8 s 346.35 ms remaining ; 7 h 16 min 18 s 258.78 ms total)
Sat May 6 11:02:37 2023: Iterated 30% of D-proof candidates. [241744211 of 805814039] (ETC: Sat May 6 16:05:16 2023 ; 5 h 2 min 39 s 50.39 ms remaining ; 7 h 12 min 21 s 500.53 ms total)
Sat May 6 11:11:02 2023: Iterated 32% of D-proof candidates. [257860492 of 805814039] (ETC: Sat May 6 16:04:33 2023 ; 4 h 53 min 31 s 388.38 ms remaining ; 7 h 11 min 39 s 100.54 ms total)
Sat May 6 11:19:55 2023: Iterated 34% of D-proof candidates. [273976773 of 805814039] (ETC: Sat May 6 16:05:17 2023 ; 4 h 45 min 22 s 506.70 ms remaining ; 7 h 12 min 23 s 191.96 ms total)
Sat May 6 11:28:44 2023: Iterated 36% of D-proof candidates. [290093054 of 805814039] (ETC: Sat May 6 16:05:45 2023 ; 4 h 37 min 1 s 240.28 ms remaining ; 7 h 12 min 50 s 687.93 ms total)
Sat May 6 11:37:06 2023: Iterated 38% of D-proof candidates. [306209334 of 805814039] (ETC: Sat May 6 16:05:00 2023 ; 4 h 27 min 54 s 246.29 ms remaining ; 7 h 12 min 6 s 203.65 ms total)
Sat May 6 11:45:46 2023: Iterated 40% of D-proof candidates. [322325615 of 805814039] (ETC: Sat May 6 16:05:04 2023 ; 4 h 19 min 17 s 681.83 ms remaining ; 7 h 12 min 9 s 469.68 ms total)
Sat May 6 11:54:48 2023: Iterated 42% of D-proof candidates. [338441896 of 805814039] (ETC: Sat May 6 16:06:00 2023 ; 4 h 11 min 11 s 861.83 ms remaining ; 7 h 13 min 5 s 968.66 ms total)
Sat May 6 12:02:29 2023: Iterated 44% of D-proof candidates. [354558177 of 805814039] (ETC: Sat May 6 16:03:47 2023 ; 4 h 1 min 17 s 748.16 ms remaining ; 7 h 10 min 53 s 121.71 ms total)
Sat May 6 12:10:12 2023: Iterated 46% of D-proof candidates. [370674457 of 805814039] (ETC: Sat May 6 16:01:48 2023 ; 3 h 51 min 36 s 457.26 ms remaining ; 7 h 8 min 54 s 180.05 ms total)
Sat May 6 12:18:40 2023: Iterated 48% of D-proof candidates. [386790738 of 805814039] (ETC: Sat May 6 16:01:34 2023 ; 3 h 42 min 54 s 208.98 ms remaining ; 7 h 8 min 39 s 632.61 ms total)
Sat May 6 12:26:49 2023: Iterated 50% of D-proof candidates. [402907019 of 805814039] (ETC: Sat May 6 16:00:44 2023 ; 3 h 33 min 54 s 869.99 ms remaining ; 7 h 7 min 49 s 739.94 ms total)
Sat May 6 12:35:00 2023: Iterated 52% of D-proof candidates. [419023300 of 805814039] (ETC: Sat May 6 16:00:01 2023 ; 3 h 25 min 695.18 ms remaining ; 7 h 7 min 6 s 448.27 ms total)
Sat May 6 12:42:43 2023: Iterated 54% of D-proof candidates. [435139581 of 805814039] (ETC: Sat May 6 15:58:29 2023 ; 3 h 15 min 45 s 904.18 ms remaining ; 7 h 5 min 34 s 574.30 ms total)
Sat May 6 12:49:51 2023: Iterated 56% of D-proof candidates. [451255861 of 805814039] (ETC: Sat May 6 15:56:01 2023 ; 3 h 6 min 10 s 307.08 ms remaining ; 7 h 3 min 7 s 61.47 ms total)
Sat May 6 12:57:27 2023: Iterated 58% of D-proof candidates. [467372142 of 805814039] (ETC: Sat May 6 15:54:31 2023 ; 2 h 57 min 4 s 864.40 ms remaining ; 7 h 1 min 37 s 296.14 ms total)
Sat May 6 13:04:41 2023: Iterated 60% of D-proof candidates. [483488423 of 805814039] (ETC: Sat May 6 15:52:32 2023 ; 2 h 47 min 51 s 46.64 ms remaining ; 6 h 59 min 37 s 616.56 ms total)
Sat May 6 13:11:48 2023: Iterated 62% of D-proof candidates. [499604704 of 805814039] (ETC: Sat May 6 15:50:29 2023 ; 2 h 38 min 40 s 721.60 ms remaining ; 6 h 57 min 34 s 530.51 ms total)
Sat May 6 13:18:54 2023: Iterated 64% of D-proof candidates. [515720984 of 805814039] (ETC: Sat May 6 15:48:32 2023 ; 2 h 29 min 37 s 727.82 ms remaining ; 6 h 55 min 38 s 132.76 ms total)
Sat May 6 13:25:22 2023: Iterated 66% of D-proof candidates. [531837265 of 805814039] (ETC: Sat May 6 15:45:44 2023 ; 2 h 20 min 21 s 822.04 ms remaining ; 6 h 52 min 50 s 64.76 ms total)
Sat May 6 13:32:31 2023: Iterated 68% of D-proof candidates. [547953546 of 805814039] (ETC: Sat May 6 15:44:06 2023 ; 2 h 11 min 35 s 172.32 ms remaining ; 6 h 51 min 12 s 413.45 ms total)
Sat May 6 13:39:19 2023: Iterated 70% of D-proof candidates. [564069827 of 805814039] (ETC: Sat May 6 15:42:04 2023 ; 2 h 2 min 44 s 877.55 ms remaining ; 6 h 49 min 9 s 591.81 ms total)
Sat May 6 13:46:07 2023: Iterated 72% of D-proof candidates. [580186108 of 805814039] (ETC: Sat May 6 15:40:08 2023 ; 1 h 54 min 1 s 634.62 ms remaining ; 6 h 47 min 14 s 409.36 ms total)
Sat May 6 13:52:17 2023: Iterated 74% of D-proof candidates. [596302388 of 805814039] (ETC: Sat May 6 15:37:28 2023 ; 1 h 45 min 11 s 327.26 ms remaining ; 6 h 44 min 34 s 335.52 ms total)
Sat May 6 13:58:50 2023: Iterated 76% of D-proof candidates. [612418669 of 805814039] (ETC: Sat May 6 15:35:27 2023 ; 1 h 36 min 36 s 729.00 ms remaining ; 6 h 42 min 33 s 37.44 ms total)
Sat May 6 14:05:13 2023: Iterated 78% of D-proof candidates. [628534950 of 805814039] (ETC: Sat May 6 15:33:18 2023 ; 1 h 28 min 5 s 295.99 ms remaining ; 6 h 40 min 24 s 72.65 ms total)
Sat May 6 14:11:35 2023: Iterated 80% of D-proof candidates. [644651231 of 805814039] (ETC: Sat May 6 15:31:15 2023 ; 1 h 19 min 40 s 278.61 ms remaining ; 6 h 38 min 21 s 393.00 ms total)
Sat May 6 14:17:32 2023: Iterated 82% of D-proof candidates. [660767511 of 805814039] (ETC: Sat May 6 15:28:48 2023 ; 1 h 11 min 15 s 737.97 ms remaining ; 6 h 35 min 54 s 99.65 ms total)
Sat May 6 14:23:42 2023: Iterated 84% of D-proof candidates. [676883792 of 805814039] (ETC: Sat May 6 15:26:43 2023 ; 1 h 3 min 644.68 ms remaining ; 6 h 33 min 49 s 29.08 ms total)
Sat May 6 14:29:43 2023: Iterated 86% of D-proof candidates. [693000073 of 805814039] (ETC: Sat May 6 15:24:33 2023 ; 54 min 49 s 801.27 ms remaining ; 6 h 31 min 38 s 580.42 ms total)
Sat May 6 14:35:36 2023: Iterated 88% of D-proof candidates. [709116354 of 805814039] (ETC: Sat May 6 15:22:20 2023 ; 46 min 43 s 919.21 ms remaining ; 6 h 29 min 25 s 993.38 ms total)
Sat May 6 14:41:31 2023: Iterated 90% of D-proof candidates. [725232635 of 805814039] (ETC: Sat May 6 15:20:15 2023 ; 38 min 44 s 54.45 ms remaining ; 6 h 27 min 20 s 544.43 ms total)
Sat May 6 14:47:25 2023: Iterated 92% of D-proof candidates. [741348915 of 805814039] (ETC: Sat May 6 15:18:14 2023 ; 30 min 49 s 633.41 ms remaining ; 6 h 25 min 20 s 417.25 ms total)
Sat May 6 14:53:23 2023: Iterated 94% of D-proof candidates. [757465196 of 805814039] (ETC: Sat May 6 15:16:23 2023 ; 23 min 552.69 ms remaining ; 6 h 23 min 29 s 211.11 ms total)
Sat May 6 14:59:03 2023: Iterated 96% of D-proof candidates. [773581477 of 805814039] (ETC: Sat May 6 15:14:19 2023 ; 15 min 15 s 384.12 ms remaining ; 6 h 21 min 24 s 602.76 ms total)
Sat May 6 15:04:55 2023: Iterated 98% of D-proof candidates. [789697758 of 805814039] (ETC: Sat May 6 15:12:30 2023 ; 7 min 35 s 521.76 ms remaining ; 6 h 19 min 36 s 87.91 ms total)
22877558.61 ms (6 h 21 min 17 s 558.61 ms) taken to collect 139032027 D-proofs of length 35. [iterated 805814039 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 } }
[Copy] Static unfiltered iteration counts: { 33, { { 35, 805814039 } } },
869615.82 ms (14 min 29 s 615.82 ms) taken to filter and order new representative proofs.
Found 139032027 representative, 316487114 redundant, and 350294898 invalid condensed detachment proof strings.
lengths up to 35 ; 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,39933795), (35,139032027)} ; 139032027 new representative proofs (316487114 redundant, 350294898 invalid)
Sat May 6 15:30:06 2023: Starting to write 139032027 entries to data/dProofs-withConclusions/dProofs35-unfiltered33+.txt.
213053.23 ms (3 min 33 s 53.23 ms) taken to print and save 28223320428 bytes of representative condensed detachment proof strings to data/dProofs-withConclusions/dProofs35-unfiltered33+.txt.
Sat May 6 15:35:37 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 35, unfiltered]
Sat May 6 15:43:29 2023: Process terminated. [pid: 1346668, tid:22757167990656]