-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
63.log
115 lines (114 loc) · 12.2 KB
/
63.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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
40063108 c18m_low 48 COMPLETED 0:0 00:03:00
40063108.ba+ 48 COMPLETED 0:0 00:03:00 17785628K
40063108.ex+ 48 COMPLETED 0:0 00:03:00 4K
By 17785628 KiB = (17785628 / 1024^2) GiB = 16.961696624755859375 GiB, it used approximately 16.96 gibibytes of memory. )
Sat Oct 14 20:25:28 2023: Process started. [pid: 63458, tid:22781115144064]
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).
Sat Oct 14 20:25:28 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.02 ms taken to load initial representatives.
0.43 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:22781054895872]
0.04 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:22781052794624]
0.05 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:22781050693376]
0.07 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:22781048592128]
0.05 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:22781046490880]
0.13 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:22780707862272]
0.10 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:22780571543296]
0.05 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:22780705761024]
3.64 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:22780703659776]
0.07 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:22780701558528]
0.06 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:22780699457280]
3.57 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:22780697356032]
4.22 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:22780695254784]
2.09 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:22780693153536]
3.88 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:22780691052288]
42.21 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:22780688951040]
20.37 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:22780686849792]
50.95 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:22780684748544]
163.76 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:22780682647296]
293.10 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:22780680546048]
770.65 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:22780678444800]
2136.34 ms (2 s 136.34 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:22780676343552]
4560.99 ms (4 s 560.99 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:22780674242304]
431.47 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:22780672141056]
795.15 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:22780670039808]
1279.54 ms (1 s 279.54 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:22780667938560]
1872.36 ms (1 s 872.37 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:22780665837312]
2799.26 ms (2 s 799.26 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:22780663736064]
3891.25 ms (3 s 891.25 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:22780661634816]
5295.52 ms (5 s 295.52 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:22780659533568]
7269.53 ms (7 s 269.53 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:22780657432320]
7287.09 ms (7 s 287.10 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.
Sat Oct 14 20:25:36 2023: Inserted ≈ 5% of D-proof conclusions. [ 767692 of 15353842] (ETC: Sat Oct 14 20:25:43 2023 ; 6 s 830.98 ms remaining ; 7 s 190.50 ms total)
Sat Oct 14 20:25:36 2023: Inserted ≈10% of D-proof conclusions. [ 1535384 of 15353842] (ETC: Sat Oct 14 20:25:43 2023 ; 6 s 945.53 ms remaining ; 7 s 717.26 ms total)
Sat Oct 14 20:25:37 2023: Inserted ≈15% of D-proof conclusions. [ 2303076 of 15353842] (ETC: Sat Oct 14 20:25:43 2023 ; 6 s 794.91 ms remaining ; 7 s 994.01 ms total)
Sat Oct 14 20:25:37 2023: Inserted ≈20% of D-proof conclusions. [ 3070768 of 15353842] (ETC: Sat Oct 14 20:25:44 2023 ; 6 s 656.74 ms remaining ; 8 s 320.93 ms total)
Sat Oct 14 20:25:38 2023: Inserted ≈25% of D-proof conclusions. [ 3838460 of 15353842] (ETC: Sat Oct 14 20:25:44 2023 ; 6 s 793.36 ms remaining ; 9 s 57.81 ms total)
Sat Oct 14 20:25:38 2023: Inserted ≈30% of D-proof conclusions. [ 4606152 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 6 s 707.53 ms remaining ; 9 s 582.18 ms total)
Sat Oct 14 20:25:39 2023: Inserted ≈35% of D-proof conclusions. [ 5373844 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 6 s 322.13 ms remaining ; 9 s 726.35 ms total)
Sat Oct 14 20:25:39 2023: Inserted ≈40% of D-proof conclusions. [ 6141536 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 5 s 881.15 ms remaining ; 9 s 801.92 ms total)
Sat Oct 14 20:25:40 2023: Inserted ≈45% of D-proof conclusions. [ 6909228 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 5 s 293.25 ms remaining ; 9 s 624.09 ms total)
Sat Oct 14 20:25:40 2023: Inserted ≈50% of D-proof conclusions. [ 7676921 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 4 s 773.86 ms remaining ; 9 s 547.73 ms total)
Sat Oct 14 20:25:41 2023: Inserted ≈55% of D-proof conclusions. [ 8444613 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 4 s 377.84 ms remaining ; 9 s 728.53 ms total)
Sat Oct 14 20:25:41 2023: Inserted ≈60% of D-proof conclusions. [ 9212305 of 15353842] (ETC: Sat Oct 14 20:25:45 2023 ; 4 s 22.95 ms remaining ; 10 s 57.37 ms total)
Sat Oct 14 20:25:42 2023: Inserted ≈65% of D-proof conclusions. [ 9979997 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 3 s 588.72 ms remaining ; 10 s 253.49 ms total)
Sat Oct 14 20:25:42 2023: Inserted ≈70% of D-proof conclusions. [10747689 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 3 s 63.30 ms remaining ; 10 s 210.99 ms total)
Sat Oct 14 20:25:43 2023: Inserted ≈75% of D-proof conclusions. [11515381 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 2 s 570.45 ms remaining ; 10 s 281.78 ms total)
Sat Oct 14 20:25:44 2023: Inserted ≈80% of D-proof conclusions. [12283073 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 2 s 77.53 ms remaining ; 10 s 387.65 ms total)
Sat Oct 14 20:25:44 2023: Inserted ≈85% of D-proof conclusions. [13050765 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 1 s 573.32 ms remaining ; 10 s 488.80 ms total)
Sat Oct 14 20:25:45 2023: Inserted ≈90% of D-proof conclusions. [13818457 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 1 s 56.67 ms remaining ; 10 s 566.74 ms total)
Sat Oct 14 20:25:46 2023: Inserted ≈95% of D-proof conclusions. [14586149 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 537.05 ms remaining ; 10 s 740.93 ms total)
Sat Oct 14 20:25:46 2023: Inserted 100% of D-proof conclusions. [15353842 of 15353842] (ETC: Sat Oct 14 20:25:46 2023 ; 0.00 ms remaining ; 10 s 875.01 ms total)
10875.18 ms (10 s 875.18 ms) total insertion duration.
Sat Oct 14 20:25:46 2023: Starting to iterate D-proof candidates of length 65.
134211.26 ms (2 min 14 s 211.26 ms) taken to iterate 222080338 condensed detachment proof strings of length 65.
[Copy] Next iteration count (filtered): { 65, 222080338 }
Sat Oct 14 20:28:00 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Sat Oct 14 20:28:23 2023: Process terminated. [pid: 63458, tid:22781115144064]