-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
79-71.log
134 lines (133 loc) · 14.6 KB
/
79-71.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
127
128
129
130
131
132
133
134
( This log file was generated by executing 'pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --iterate -u' (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-OPTANE MPI node
— 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
running Linux, Rocky 8.8.
The job led to the following output:
$ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS"
JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS
------------ ---------- ---------- ---------- -------- ---------- ----------
40493663 optane_low 64 COMPLETED 0:0 00:58:37
40493663.ba+ 64 COMPLETED 0:0 00:58:37 355670196K
40493663.ex+ 64 COMPLETED 0:0 00:58:37 0
By 355670196 KiB = (355670196 / 1024^2) GiB = 339.193531036376953125 GiB, it used approximately 339.19 gibibytes of memory. )
Thu Nov 2 02:21:09 2023: Process started. [pid: 28930, tid:22774479628160]
Tasks:
1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed]
(1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0))
[Main] Calling countNextIterationAmount(false, true).
Thu Nov 2 02:21:09 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.04 ms taken to load initial representatives.
18.60 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22774419379968]
22.89 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22774417278720]
23.82 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22774415177472]
19.43 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22774413076224]
15.12 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22774410974976]
27.27 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22774408873728]
28.40 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22774406772480]
26.37 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22774404671232]
23.84 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22774402569984]
21.50 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22774332520192]
29.21 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22774330418944]
29.84 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22774328317696]
33.38 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22774326216448]
11.76 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22774324115200]
324.62 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22774322013952]
44.82 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22774319912704]
54.96 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22774317811456]
106.01 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22774315710208]
60.75 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22774313608960]
226.85 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22774311507712]
186.41 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22774309406464]
111.01 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22774307305216]
294.76 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22774305203968]
768.52 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22774303102720]
767.52 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22774301001472]
1056.02 ms (1 s 56.02 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22774298900224]
4096.39 ms (4 s 96.39 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22774296798976]
3482.34 ms (3 s 482.34 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22774294697728]
2212.19 ms (2 s 212.19 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22774292596480]
2841.20 ms (2 s 841.20 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22774290495232]
4503.88 ms (4 s 503.88 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22774288393984]
4672.58 ms (4 s 672.58 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22774286292736]
5841.34 ms (5 s 841.34 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22774284191488]
7242.78 ms (7 s 242.78 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22774282090240]
7326.09 ms (7 s 326.10 ms) total read duration.
Loaded 35 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 3
9 : 7
11 : 10
13 : 13
15 : 19
17 : 37
19 : 56
21 : 87
23 : 140
25 : 227
27 : 369
29 : 579
31 : 918
33 : 1499
35 : 2408
37 : 3881
39 : 6254
41 : 10109
43 : 16460
45 : 26753
47 : 43360
49 : 70709
51 : 115604
53 : 188634
55 : 308241
57 : 504870
59 : 827701
61 : 1357539
63 : 2227822
65 : 3660735
67 : 6021110
69 : 9907537
25303694 representatives in total.
35712.72 ms (35 s 712.72 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22774282090240]
58890.09 ms (58 s 890.09 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22774284191488]
79554.91 ms (1 min 19 s 554.91 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22774286292736]
107561.71 ms (1 min 47 s 561.71 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:22774288393984]
144404.17 ms (2 min 24 s 404.17 ms) taken to read 263540491 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. [tid:22774290495232]
144572.03 ms (2 min 24 s 572.03 ms) additional read duration.
Loaded 5 more representative collections of sizes:
71 : 23150845
73 : 45156728
75 : 80141395
77 : 143296899
79 : 263540491
580590052 representatives in total.
Thu Nov 2 02:24:19 2023: Inserted ≈ 5% of D-proof conclusions. [ 29029502 of 580590052] (ETC: Thu Nov 2 02:36:11 2023 ; 11 min 52 s 468.04 ms remaining ; 12 min 29 s 966.36 ms total)
Thu Nov 2 02:25:02 2023: Inserted ≈10% of D-proof conclusions. [ 58059005 of 580590052] (ETC: Thu Nov 2 02:37:12 2023 ; 12 min 9 s 953.49 ms remaining ; 13 min 31 s 59.43 ms total)
Thu Nov 2 02:25:48 2023: Inserted ≈15% of D-proof conclusions. [ 87088507 of 580590052] (ETC: Thu Nov 2 02:37:49 2023 ; 12 min 977.25 ms remaining ; 14 min 8 s 208.53 ms total)
Thu Nov 2 02:26:24 2023: Inserted ≈20% of D-proof conclusions. [116118010 of 580590052] (ETC: Thu Nov 2 02:37:16 2023 ; 10 min 51 s 847.79 ms remaining ; 13 min 34 s 809.74 ms total)
Thu Nov 2 02:27:05 2023: Inserted ≈25% of D-proof conclusions. [145147513 of 580590052] (ETC: Thu Nov 2 02:37:18 2023 ; 10 min 12 s 748.83 ms remaining ; 13 min 36 s 998.44 ms total)
Thu Nov 2 02:27:49 2023: Inserted ≈30% of D-proof conclusions. [174177015 of 580590052] (ETC: Thu Nov 2 02:37:28 2023 ; 9 min 38 s 946.02 ms remaining ; 13 min 47 s 65.74 ms total)
Thu Nov 2 02:28:18 2023: Inserted ≈35% of D-proof conclusions. [203206518 of 580590052] (ETC: Thu Nov 2 02:36:53 2023 ; 8 min 34 s 884.78 ms remaining ; 13 min 12 s 130.43 ms total)
Thu Nov 2 02:28:50 2023: Inserted ≈40% of D-proof conclusions. [232236020 of 580590052] (ETC: Thu Nov 2 02:36:34 2023 ; 7 min 43 s 883.95 ms remaining ; 12 min 53 s 139.91 ms total)
Thu Nov 2 02:29:25 2023: Inserted ≈45% of D-proof conclusions. [261265523 of 580590052] (ETC: Thu Nov 2 02:36:26 2023 ; 7 min 619.31 ms remaining ; 12 min 44 s 762.38 ms total)
Thu Nov 2 02:30:03 2023: Inserted ≈50% of D-proof conclusions. [290295026 of 580590052] (ETC: Thu Nov 2 02:36:24 2023 ; 6 min 21 s 633.13 ms remaining ; 12 min 43 s 266.26 ms total)
Thu Nov 2 02:30:39 2023: Inserted ≈55% of D-proof conclusions. [319324528 of 580590052] (ETC: Thu Nov 2 02:36:20 2023 ; 5 min 41 s 719.43 ms remaining ; 12 min 39 s 376.51 ms total)
Thu Nov 2 02:31:02 2023: Inserted ≈60% of D-proof conclusions. [348354031 of 580590052] (ETC: Thu Nov 2 02:35:56 2023 ; 4 min 53 s 923.33 ms remaining ; 12 min 14 s 808.32 ms total)
Thu Nov 2 02:31:25 2023: Inserted ≈65% of D-proof conclusions. [377383533 of 580590052] (ETC: Thu Nov 2 02:35:35 2023 ; 4 min 10 s 26.59 ms remaining ; 11 min 54 s 361.68 ms total)
Thu Nov 2 02:31:50 2023: Inserted ≈70% of D-proof conclusions. [406413036 of 580590052] (ETC: Thu Nov 2 02:35:20 2023 ; 3 min 29 s 665.72 ms remaining ; 11 min 38 s 885.74 ms total)
Thu Nov 2 02:32:16 2023: Inserted ≈75% of D-proof conclusions. [435442539 of 580590052] (ETC: Thu Nov 2 02:35:07 2023 ; 2 min 51 s 558.50 ms remaining ; 11 min 26 s 233.99 ms total)
Thu Nov 2 02:32:42 2023: Inserted ≈80% of D-proof conclusions. [464472041 of 580590052] (ETC: Thu Nov 2 02:34:57 2023 ; 2 min 15 s 256.89 ms remaining ; 11 min 16 s 284.46 ms total)
Thu Nov 2 02:33:09 2023: Inserted ≈85% of D-proof conclusions. [493501544 of 580590052] (ETC: Thu Nov 2 02:34:50 2023 ; 1 min 40 s 283.44 ms remaining ; 11 min 8 s 556.25 ms total)
Thu Nov 2 02:33:44 2023: Inserted ≈90% of D-proof conclusions. [522531046 of 580590052] (ETC: Thu Nov 2 02:34:51 2023 ; 1 min 6 s 962.76 ms remaining ; 11 min 9 s 627.62 ms total)
Thu Nov 2 02:34:27 2023: Inserted ≈95% of D-proof conclusions. [551560549 of 580590052] (ETC: Thu Nov 2 02:35:01 2023 ; 34 s 5.51 ms remaining ; 11 min 20 s 110.13 ms total)
Thu Nov 2 02:35:12 2023: Inserted 100% of D-proof conclusions. [580590052 of 580590052] (ETC: Thu Nov 2 02:35:12 2023 ; 0.00 ms remaining ; 11 min 30 s 939.62 ms total)
690940.87 ms (11 min 30 s 940.87 ms) total insertion duration.
Thu Nov 2 02:35:12 2023: Starting to iterate D-proof candidates of length 81.
1876662.74 ms (31 min 16 s 662.74 ms) taken to iterate 3720990150 condensed detachment proof strings of length 81.
[Copy] Next iteration count (unfiltered71+): { 81, 3720990150 }
Thu Nov 2 03:06:40 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Thu Nov 2 03:19:21 2023: Process terminated. [pid: 28930, tid:22774479628160]