-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
35.log
87 lines (86 loc) · 9.13 KB
/
35.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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
40049686 c18m_low 48 COMPLETED 0:0 00:00:33
40049686.ba+ 48 COMPLETED 0:0 00:00:33 8979264K
40049686.ex+ 48 COMPLETED 0:0 00:00:33 80K
By 8979264 KiB = (8979264 / 1024^2) GiB = 8.56329345703125 GiB, it used approximately 8.56 gibibytes of memory. )
Thu Oct 12 20:09:20 2023: Process started. [pid: 79148, tid:23289182291840]
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).
Thu Oct 12 20:09:20 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
15.70 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:23289122043648]
16.51 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:23289119942400]
22.64 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:23289117841152]
17.89 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:23289115739904]
21.72 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:23289113638656]
27.63 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:23289111537408]
15.99 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:23289109436160]
26.43 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:23289107334912]
46.43 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:23289105233664]
54.00 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:23289103132416]
102.35 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:23289101031168]
512.53 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:23289098929920]
3552.19 ms (3 s 552.19 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:23289096828672]
390.52 ms taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:23289094727424]
802.10 ms taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:23289092626176]
1773.04 ms (1 s 773.04 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:23289090524928]
4276.46 ms (4 s 276.46 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:23289088423680]
4287.68 ms (4 s 287.68 ms) total read duration.
Loaded 18 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
3019234 representatives in total.
Thu Oct 12 20:09:24 2023: Inserted ≈ 5% of D-proof conclusions. [ 150961 of 3019234] (ETC: Thu Oct 12 20:09:27 2023 ; 2 s 866.03 ms remaining ; 3 s 16.87 ms total)
Thu Oct 12 20:09:25 2023: Inserted ≈10% of D-proof conclusions. [ 301923 of 3019234] (ETC: Thu Oct 12 20:09:29 2023 ; 4 s 16.38 ms remaining ; 4 s 462.64 ms total)
Thu Oct 12 20:09:25 2023: Inserted ≈15% of D-proof conclusions. [ 452885 of 3019234] (ETC: Thu Oct 12 20:09:30 2023 ; 4 s 955.99 ms remaining ; 5 s 830.58 ms total)
Thu Oct 12 20:09:25 2023: Inserted ≈20% of D-proof conclusions. [ 603846 of 3019234] (ETC: Thu Oct 12 20:09:30 2023 ; 4 s 973.17 ms remaining ; 6 s 216.46 ms total)
Thu Oct 12 20:09:26 2023: Inserted ≈25% of D-proof conclusions. [ 754808 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 4 s 774.96 ms remaining ; 6 s 366.61 ms total)
Thu Oct 12 20:09:26 2023: Inserted ≈30% of D-proof conclusions. [ 905770 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 4 s 540.66 ms remaining ; 6 s 486.66 ms total)
Thu Oct 12 20:09:27 2023: Inserted ≈35% of D-proof conclusions. [1056731 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 4 s 242.35 ms remaining ; 6 s 526.70 ms total)
Thu Oct 12 20:09:27 2023: Inserted ≈40% of D-proof conclusions. [1207693 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 3 s 954.74 ms remaining ; 6 s 591.24 ms total)
Thu Oct 12 20:09:27 2023: Inserted ≈45% of D-proof conclusions. [1358655 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 3 s 578.75 ms remaining ; 6 s 506.82 ms total)
Thu Oct 12 20:09:27 2023: Inserted ≈50% of D-proof conclusions. [1509617 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 3 s 220.32 ms remaining ; 6 s 440.64 ms total)
Thu Oct 12 20:09:28 2023: Inserted ≈55% of D-proof conclusions. [1660578 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 2 s 882.61 ms remaining ; 6 s 405.80 ms total)
Thu Oct 12 20:09:28 2023: Inserted ≈60% of D-proof conclusions. [1811540 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 2 s 560.34 ms remaining ; 6 s 400.84 ms total)
Thu Oct 12 20:09:28 2023: Inserted ≈65% of D-proof conclusions. [1962502 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 2 s 217.59 ms remaining ; 6 s 335.96 ms total)
Thu Oct 12 20:09:29 2023: Inserted ≈70% of D-proof conclusions. [2113463 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 1 s 905.71 ms remaining ; 6 s 352.38 ms total)
Thu Oct 12 20:09:29 2023: Inserted ≈75% of D-proof conclusions. [2264425 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 1 s 580.70 ms remaining ; 6 s 322.79 ms total)
Thu Oct 12 20:09:29 2023: Inserted ≈80% of D-proof conclusions. [2415387 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 1 s 292.44 ms remaining ; 6 s 462.20 ms total)
Thu Oct 12 20:09:30 2023: Inserted ≈85% of D-proof conclusions. [2566348 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 968.45 ms remaining ; 6 s 456.32 ms total)
Thu Oct 12 20:09:30 2023: Inserted ≈90% of D-proof conclusions. [2717310 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 645.30 ms remaining ; 6 s 453.03 ms total)
Thu Oct 12 20:09:30 2023: Inserted ≈95% of D-proof conclusions. [2868272 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 322.99 ms remaining ; 6 s 459.88 ms total)
Thu Oct 12 20:09:31 2023: Inserted 100% of D-proof conclusions. [3019234 of 3019234] (ETC: Thu Oct 12 20:09:31 2023 ; 0.00 ms remaining ; 6 s 508.60 ms total)
6508.83 ms (6 s 508.83 ms) total insertion duration.
Thu Oct 12 20:09:31 2023: Starting to iterate D-proof candidates of length 37.
9024.73 ms (9 s 24.73 ms) taken to iterate 10505128 condensed detachment proof strings of length 37.
[Copy] Next iteration count (filtered): { 37, 10505128 }
Thu Oct 12 20:09:40 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Thu Oct 12 20:09:49 2023: Process terminated. [pid: 79148, tid:23289182291840]