-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy path37.log
89 lines (88 loc) · 9.42 KB
/
37.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
( This log file was generated by executing 'pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --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 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.
The job led to the following output:
$ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS"
JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS
------------ ---------- ---------- ---------- -------- ---------- ----------
39801022 c18m_low 48 COMPLETED 0:0 00:01:47
39801022.ba+ 48 COMPLETED 0:0 00:01:47 28120984K
39801022.ex+ 48 COMPLETED 0:0 00:01:47 80K
By 28120984 KiB = (28120984 / 1024^2) GiB = 26.81826019287109375 GiB, it used approximately 26.82 gibibytes of memory. )
Mon Oct 9 07:24:14 2023: Process started. [pid: 35094, tid:22462652753792]
Tasks:
1. resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true)
2. countNextIterationAmount(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 countNextIterationAmount(false, true).
Mon Oct 9 07:24:14 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.04 ms taken to load initial representatives.
21.03 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:22462592505600]
15.05 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:22462590404352]
23.06 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:22462588303104]
14.84 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:22462586201856]
21.03 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:22462584100608]
32.20 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:22462581999360]
29.32 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:22462579898112]
24.52 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:22462577796864]
53.57 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:22462575695616]
63.28 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:22462573594368]
102.60 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:22462571493120]
551.52 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:22462569391872]
3641.27 ms (3 s 641.26 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:22462567290624]
293.70 ms taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:22462565189376]
979.97 ms taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:22462563088128]
2673.12 ms (2 s 673.12 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:22462560986880]
5791.39 ms (5 s 791.39 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:22462558885632]
13450.79 ms (13 s 450.79 ms) taken to read 5081180 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt. [tid:22462556784384]
13464.14 ms (13 s 464.14 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.
Mon Oct 9 07:24:29 2023: Inserted ≈ 5% of D-proof conclusions. [ 405020 of 8100414] (ETC: Mon Oct 9 07:24:54 2023 ; 24 s 727.06 ms remaining ; 26 s 28.48 ms total)
Mon Oct 9 07:24:30 2023: Inserted ≈10% of D-proof conclusions. [ 810041 of 8100414] (ETC: Mon Oct 9 07:24:55 2023 ; 24 s 445.09 ms remaining ; 27 s 161.21 ms total)
Mon Oct 9 07:24:32 2023: Inserted ≈15% of D-proof conclusions. [1215062 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 25 s 378.08 ms remaining ; 29 s 856.56 ms total)
Mon Oct 9 07:24:34 2023: Inserted ≈20% of D-proof conclusions. [1620082 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 24 s 29.34 ms remaining ; 30 s 36.67 ms total)
Mon Oct 9 07:24:35 2023: Inserted ≈25% of D-proof conclusions. [2025103 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 23 s 53.27 ms remaining ; 30 s 737.70 ms total)
Mon Oct 9 07:24:37 2023: Inserted ≈30% of D-proof conclusions. [2430124 of 8100414] (ETC: Mon Oct 9 07:24:59 2023 ; 22 s 182.90 ms remaining ; 31 s 689.86 ms total)
Mon Oct 9 07:24:39 2023: Inserted ≈35% of D-proof conclusions. [2835144 of 8100414] (ETC: Mon Oct 9 07:25:00 2023 ; 21 s 2.77 ms remaining ; 32 s 311.95 ms total)
Mon Oct 9 07:24:40 2023: Inserted ≈40% of D-proof conclusions. [3240165 of 8100414] (ETC: Mon Oct 9 07:25:00 2023 ; 19 s 286.24 ms remaining ; 32 s 143.73 ms total)
Mon Oct 9 07:24:42 2023: Inserted ≈45% of D-proof conclusions. [3645186 of 8100414] (ETC: Mon Oct 9 07:24:59 2023 ; 17 s 74.59 ms remaining ; 31 s 44.72 ms total)
Mon Oct 9 07:24:43 2023: Inserted ≈50% of D-proof conclusions. [4050207 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 15 s 200.89 ms remaining ; 30 s 401.79 ms total)
Mon Oct 9 07:24:44 2023: Inserted ≈55% of D-proof conclusions. [4455227 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 13 s 474.59 ms remaining ; 29 s 943.53 ms total)
Mon Oct 9 07:24:45 2023: Inserted ≈60% of D-proof conclusions. [4860248 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 11 s 855.61 ms remaining ; 29 s 639.03 ms total)
Mon Oct 9 07:24:47 2023: Inserted ≈65% of D-proof conclusions. [5265269 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 10 s 317.20 ms remaining ; 29 s 477.72 ms total)
Mon Oct 9 07:24:48 2023: Inserted ≈70% of D-proof conclusions. [5670289 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 8 s 756.34 ms remaining ; 29 s 187.78 ms total)
Mon Oct 9 07:24:49 2023: Inserted ≈75% of D-proof conclusions. [6075310 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 7 s 289.26 ms remaining ; 29 s 157.05 ms total)
Mon Oct 9 07:24:51 2023: Inserted ≈80% of D-proof conclusions. [6480331 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 5 s 858.50 ms remaining ; 29 s 292.49 ms total)
Mon Oct 9 07:24:53 2023: Inserted ≈85% of D-proof conclusions. [6885351 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 4 s 415.00 ms remaining ; 29 s 433.35 ms total)
Mon Oct 9 07:24:54 2023: Inserted ≈90% of D-proof conclusions. [7290372 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 2 s 979.57 ms remaining ; 29 s 795.68 ms total)
Mon Oct 9 07:24:56 2023: Inserted ≈95% of D-proof conclusions. [7695393 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 1 s 500.66 ms remaining ; 30 s 13.14 ms total)
Mon Oct 9 07:24:58 2023: Inserted 100% of D-proof conclusions. [8100414 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 0.00 ms remaining ; 30 s 698.91 ms total)
30699.14 ms (30 s 699.14 ms) total insertion duration.
Mon Oct 9 07:24:58 2023: Starting to iterate D-proof candidates of length 39.
31507.42 ms (31 s 507.42 ms) taken to iterate 28598584 condensed detachment proof strings of length 39.
[Copy] Next iteration count (filtered): { 39, 28598584 }
Mon Oct 9 07:25:30 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Mon Oct 9 07:25:56 2023: Process terminated. [pid: 35094, tid:22462652753792]