-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
61.log
113 lines (112 loc) · 11.9 KB
/
61.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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
40063076 c18m_low 48 COMPLETED 0:0 00:01:58
40063076.ba+ 48 COMPLETED 0:0 00:01:58 10635352K
40063076.ex+ 48 COMPLETED 0:0 00:01:58 76K
By 10635352 KiB = (10635352 / 1024^2) GiB = 10.14266204833984375 GiB, it used approximately 10.14 gibibytes of memory. )
Sat Oct 14 12:39:09 2023: Process started. [pid: 245717, tid:23293669812096]
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 12:39:09 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
25.50 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:23293609563904]
26.17 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:23293607462656]
18.64 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:23293605361408]
10.82 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:23293603260160]
16.61 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:23293601158912]
27.44 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:23293599057664]
26.38 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:23293596956416]
11.95 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:23293594855168]
27.83 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:23293592753920]
29.54 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:23293590652672]
25.13 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:23293588551424]
31.37 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:23293586450176]
44.37 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:23293584348928]
52.79 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:23293582247680]
55.18 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:23293580146432]
58.28 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:23293578045184]
48.85 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:23293575943936]
86.18 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:23293573842688]
159.86 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:23293571741440]
327.89 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:23293569640192]
765.91 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:23293567538944]
1903.66 ms (1 s 903.66 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:23293565437696]
4812.54 ms (4 s 812.54 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:23293563336448]
427.82 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:23293561235200]
769.26 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:23293559133952]
1171.80 ms (1 s 171.80 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:23293557032704]
1660.21 ms (1 s 660.21 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:23291876079360]
2333.29 ms (2 s 333.29 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:23291873978112]
3216.50 ms (3 s 216.50 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:23291871876864]
4394.13 ms (4 s 394.13 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:23291869775616]
4830.18 ms (4 s 830.18 ms) total read duration.
Loaded 31 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
9370676 representatives in total.
Sat Oct 14 12:39:14 2023: Inserted ≈ 5% of D-proof conclusions. [ 468533 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 597.26 ms remaining ; 3 s 786.59 ms total)
Sat Oct 14 12:39:14 2023: Inserted ≈10% of D-proof conclusions. [ 937067 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 495.35 ms remaining ; 3 s 883.72 ms total)
Sat Oct 14 12:39:15 2023: Inserted ≈15% of D-proof conclusions. [1405601 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 398.96 ms remaining ; 3 s 998.78 ms total)
Sat Oct 14 12:39:15 2023: Inserted ≈20% of D-proof conclusions. [1874135 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 832.32 ms remaining ; 4 s 790.40 ms total)
Sat Oct 14 12:39:15 2023: Inserted ≈25% of D-proof conclusions. [2342669 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 634.73 ms remaining ; 4 s 846.31 ms total)
Sat Oct 14 12:39:15 2023: Inserted ≈30% of D-proof conclusions. [2811202 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 300.64 ms remaining ; 4 s 715.20 ms total)
Sat Oct 14 12:39:16 2023: Inserted ≈35% of D-proof conclusions. [3279736 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 50.37 ms remaining ; 4 s 692.87 ms total)
Sat Oct 14 12:39:16 2023: Inserted ≈40% of D-proof conclusions. [3748270 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 873.70 ms remaining ; 4 s 789.49 ms total)
Sat Oct 14 12:39:16 2023: Inserted ≈45% of D-proof conclusions. [4216804 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 722.34 ms remaining ; 4 s 949.71 ms total)
Sat Oct 14 12:39:17 2023: Inserted ≈50% of D-proof conclusions. [4685338 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 612.65 ms remaining ; 5 s 225.31 ms total)
Sat Oct 14 12:39:17 2023: Inserted ≈55% of D-proof conclusions. [5153871 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 352.83 ms remaining ; 5 s 228.51 ms total)
Sat Oct 14 12:39:17 2023: Inserted ≈60% of D-proof conclusions. [5622405 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 146.79 ms remaining ; 5 s 366.98 ms total)
Sat Oct 14 12:39:18 2023: Inserted ≈65% of D-proof conclusions. [6090939 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 921.27 ms remaining ; 5 s 489.35 ms total)
Sat Oct 14 12:39:18 2023: Inserted ≈70% of D-proof conclusions. [6559473 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 641.58 ms remaining ; 5 s 471.93 ms total)
Sat Oct 14 12:39:18 2023: Inserted ≈75% of D-proof conclusions. [7028007 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 365.27 ms remaining ; 5 s 461.07 ms total)
Sat Oct 14 12:39:18 2023: Inserted ≈80% of D-proof conclusions. [7496540 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 98.14 ms remaining ; 5 s 490.72 ms total)
Sat Oct 14 12:39:19 2023: Inserted ≈85% of D-proof conclusions. [7965074 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 827.06 ms remaining ; 5 s 513.71 ms total)
Sat Oct 14 12:39:19 2023: Inserted ≈90% of D-proof conclusions. [8433608 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 565.32 ms remaining ; 5 s 653.22 ms total)
Sat Oct 14 12:39:20 2023: Inserted ≈95% of D-proof conclusions. [8902142 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 302.70 ms remaining ; 6 s 53.95 ms total)
Sat Oct 14 12:39:20 2023: Inserted 100% of D-proof conclusions. [9370676 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 0.00 ms remaining ; 6 s 128.35 ms total)
6128.59 ms (6 s 128.59 ms) total insertion duration.
Sat Oct 14 12:39:20 2023: Starting to iterate D-proof candidates of length 63.
86461.54 ms (1 min 26 s 461.54 ms) taken to iterate 130626396 condensed detachment proof strings of length 63.
[Copy] Next iteration count (filtered): { 63, 130626396 }
Sat Oct 14 12:40:47 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Sat Oct 14 12:41:03 2023: Process terminated. [pid: 245717, tid:23293669812096]