-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy path65-65.log
120 lines (119 loc) · 12.6 KB
/
65-65.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
( This log file was generated by executing 'pmGenerator -c -n -s CpCCNqCCNrsCptCCtqCrq --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
------------ ---------- ---------- ---------- -------- ---------- ----------
40105008 c18m_low 48 COMPLETED 0:0 00:05:57
40105008.ba+ 48 COMPLETED 0:0 00:05:57 39278476K
40105008.ex+ 48 COMPLETED 0:0 00:05:57 8K
By 39278476 KiB = (39278476 / 1024^2) GiB = 37.458873748779296875 GiB, it used approximately 37.46 gibibytes of memory. )
Sun Oct 15 05:23:27 2023: Process started. [pid: 271209, tid:23040696874880]
Tasks:
1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314]
(1) C0CCN1CCN2.3C0.4CC4.1C2.1 - CpCCNqCCNrsCptCCtqCrq - 0\imply((\not1\imply((\not2\imply3)\imply(0\imply4)))\imply((4\imply1)\imply(2\imply1)))
[Main] Calling countNextIterationAmount(false, true).
Sun Oct 15 05:23:27 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.02 ms taken to load initial representatives.
16.61 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:23040636626688]
20.92 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:23040634525440]
27.48 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:23040632424192]
25.12 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:23040630322944]
17.09 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:23040628221696]
22.66 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:23040626120448]
8.28 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:23040624019200]
21.02 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:23040150730496]
19.28 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:23040014411520]
32.57 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:23040148629248]
20.16 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:23040146528000]
49.73 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:23040144426752]
50.54 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:23040142325504]
44.85 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:23040140224256]
44.14 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:23040138123008]
52.96 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:23040136021760]
65.15 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:23040133920512]
85.00 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:23040131819264]
173.01 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:23040129718016]
357.35 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:23040127616768]
775.80 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:23040125515520]
1885.03 ms (1 s 885.03 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:23040123414272]
5056.89 ms (5 s 56.89 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:23040121313024]
546.93 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:23040119211776]
933.01 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:23040117110528]
1514.48 ms (1 s 514.48 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:23040115009280]
2075.97 ms (2 s 75.97 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:23040112908032]
2905.43 ms (2 s 905.43 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:23040110806784]
4130.20 ms (4 s 130.20 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:23040108705536]
5800.19 ms (5 s 800.19 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:23040106604288]
7737.40 ms (7 s 737.40 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:23040104503040]
7755.34 ms (7 s 755.35 ms) total read duration.
Loaded 32 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 4
9 : 7
11 : 14
13 : 23
15 : 42
17 : 72
19 : 119
21 : 180
23 : 296
25 : 493
27 : 809
29 : 1330
31 : 2190
33 : 3606
35 : 5925
37 : 9738
39 : 15948
41 : 26109
43 : 42844
45 : 70083
47 : 115027
49 : 188519
51 : 308975
53 : 506415
55 : 830126
57 : 1360461
59 : 2229126
61 : 3652191
63 : 5983166
15353842 representatives in total.
14214.81 ms (14 s 214.81 ms) taken to read 15025264 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. [tid:23040104503040]
14216.62 ms (14 s 216.62 ms) additional read duration.
Loaded 1 more representative collection of size:
65 : 15025264
30379106 representatives in total.
Sun Oct 15 05:23:51 2023: Inserted ≈ 5% of D-proof conclusions. [ 1518955 of 30379106] (ETC: Sun Oct 15 05:24:23 2023 ; 31 s 760.04 ms remaining ; 33 s 431.63 ms total)
Sun Oct 15 05:23:53 2023: Inserted ≈10% of D-proof conclusions. [ 3037910 of 30379106] (ETC: Sun Oct 15 05:24:24 2023 ; 31 s 62.76 ms remaining ; 34 s 514.18 ms total)
Sun Oct 15 05:23:54 2023: Inserted ≈15% of D-proof conclusions. [ 4556865 of 30379106] (ETC: Sun Oct 15 05:24:23 2023 ; 28 s 711.13 ms remaining ; 33 s 777.80 ms total)
Sun Oct 15 05:23:56 2023: Inserted ≈20% of D-proof conclusions. [ 6075821 of 30379106] (ETC: Sun Oct 15 05:24:22 2023 ; 26 s 212.09 ms remaining ; 32 s 765.11 ms total)
Sun Oct 15 05:23:57 2023: Inserted ≈25% of D-proof conclusions. [ 7594776 of 30379106] (ETC: Sun Oct 15 05:24:21 2023 ; 23 s 747.02 ms remaining ; 31 s 662.69 ms total)
Sun Oct 15 05:23:59 2023: Inserted ≈30% of D-proof conclusions. [ 9113731 of 30379106] (ETC: Sun Oct 15 05:24:21 2023 ; 21 s 909.84 ms remaining ; 31 s 299.77 ms total)
Sun Oct 15 05:24:00 2023: Inserted ≈35% of D-proof conclusions. [10632687 of 30379106] (ETC: Sun Oct 15 05:24:21 2023 ; 20 s 350.16 ms remaining ; 31 s 307.94 ms total)
Sun Oct 15 05:24:02 2023: Inserted ≈40% of D-proof conclusions. [12151642 of 30379106] (ETC: Sun Oct 15 05:24:20 2023 ; 18 s 353.12 ms remaining ; 30 s 588.54 ms total)
Sun Oct 15 05:24:03 2023: Inserted ≈45% of D-proof conclusions. [13670597 of 30379106] (ETC: Sun Oct 15 05:24:20 2023 ; 16 s 657.05 ms remaining ; 30 s 285.55 ms total)
Sun Oct 15 05:24:04 2023: Inserted ≈50% of D-proof conclusions. [15189553 of 30379106] (ETC: Sun Oct 15 05:24:19 2023 ; 14 s 914.34 ms remaining ; 29 s 828.69 ms total)
Sun Oct 15 05:24:05 2023: Inserted ≈55% of D-proof conclusions. [16708508 of 30379106] (ETC: Sun Oct 15 05:24:19 2023 ; 13 s 153.81 ms remaining ; 29 s 230.68 ms total)
Sun Oct 15 05:24:07 2023: Inserted ≈60% of D-proof conclusions. [18227463 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 11 s 455.14 ms remaining ; 28 s 637.84 ms total)
Sun Oct 15 05:24:08 2023: Inserted ≈65% of D-proof conclusions. [19746418 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 9 s 899.13 ms remaining ; 28 s 283.23 ms total)
Sun Oct 15 05:24:09 2023: Inserted ≈70% of D-proof conclusions. [21265374 of 30379106] (ETC: Sun Oct 15 05:24:17 2023 ; 8 s 402.10 ms remaining ; 28 s 7.00 ms total)
Sun Oct 15 05:24:11 2023: Inserted ≈75% of D-proof conclusions. [22784329 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 7 s 98.41 ms remaining ; 28 s 393.64 ms total)
Sun Oct 15 05:24:12 2023: Inserted ≈80% of D-proof conclusions. [24303284 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 5 s 686.80 ms remaining ; 28 s 433.98 ms total)
Sun Oct 15 05:24:14 2023: Inserted ≈85% of D-proof conclusions. [25822240 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 4 s 298.70 ms remaining ; 28 s 658.02 ms total)
Sun Oct 15 05:24:15 2023: Inserted ≈90% of D-proof conclusions. [27341195 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 2 s 894.49 ms remaining ; 28 s 944.86 ms total)
Sun Oct 15 05:24:17 2023: Inserted ≈95% of D-proof conclusions. [28860150 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 1 s 436.43 ms remaining ; 28 s 728.66 ms total)
Sun Oct 15 05:24:18 2023: Inserted 100% of D-proof conclusions. [30379106 of 30379106] (ETC: Sun Oct 15 05:24:18 2023 ; 0.00 ms remaining ; 28 s 615.70 ms total)
28615.91 ms (28 s 615.91 ms) total insertion duration.
Sun Oct 15 05:24:18 2023: Starting to iterate D-proof candidates of length 67.
249078.90 ms (4 min 9 s 78.90 ms) taken to iterate 387519448 condensed detachment proof strings of length 67.
[Copy] Next iteration count (unfiltered65+): { 67, 387519448 }
Sun Oct 15 05:28:27 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Sun Oct 15 05:29:19 2023: Process terminated. [pid: 271209, tid:23040696874880]