91-83.log

( This log file was generated by executing 'pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp --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-OPTANE MPI node
  — 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
  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 
   ------------ ---------- ---------- ---------- -------- ---------- ---------- 
   40806186     optane_low         64  COMPLETED      0:0   00:58:02            
   40806186.ba+                    64  COMPLETED      0:0   00:58:02 408768632K 
   40806186.ex+                    64  COMPLETED      0:0   00:58:02          0 
  By 408768632 KiB = (408768632 / 1024^2) GiB = 389.83214569091796875 GiB, it used approximately 389.83 gibibytes of memory. )
Thu Nov 16 17:11:58 2023: Process started. [pid: 167189, tid:22742156158848]
Tasks:
1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true)
2. countNextIterationAmount(false, true)

[Main] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69]
(1) CCC0.1CCCN2N3.2.4CC4.0C3.0    -    CCCpqCCCNrNsrtCCtpCsp    -    ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0))
[Main] Calling countNextIterationAmount(false, true).
Thu Nov 16 17:11:58 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
11.91 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22742095935232]
21.39 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22742093833984]
24.72 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22742091732736]
20.42 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22742089631488]
10.13 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22742087530240]
21.30 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22741951211264]
26.56 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22742085428992]
14.48 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22742083327744]
8.89 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22742081226496]
23.51 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22742079125248]
12.73 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22742077024000]
17.55 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22742074922752]
33.52 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22742072821504]
23.62 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22742070720256]
36.40 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22742068619008]
18.05 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22742066517760]
9.84 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22742064416512]
24.75 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22742062315264]
56.92 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22742060214016]
55.41 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22742058112768]
180.93 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22742056011520]
122.51 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22741986047744]
60.44 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22741983946496]
87.80 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22741981845248]
464.00 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22741979744000]
340.62 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22741977642752]
138.03 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22741975541504]
429.16 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22741973440256]
668.71 ms taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22741971339008]
1192.27 ms (1 s 192.28 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22741969237760]
3928.48 ms (3 s 928.48 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22741967136512]
7161.74 ms (7 s 161.74 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22741965035264]
2886.98 ms (2 s 886.99 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22741962934016]
2864.48 ms (2 s 864.48 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22741960832768]
2971.00 ms (2 s 971.00 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22741958731520]
4986.35 ms (4 s 986.35 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22741956630272]
5798.11 ms (5 s 798.11 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22741954529024]
6435.94 ms (6 s 435.94 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22741949110016]
7429.37 ms (7 s 429.37 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22741947008768]
8078.17 ms (8 s 78.17 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22741944907520]
8161.19 ms (8 s 161.19 ms) total read duration.
Loaded 41 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 3
9 : 6
11 : 7
13 : 12
15 : 15
17 : 23
19 : 36
21 : 61
23 : 99
25 : 152
27 : 214
29 : 299
31 : 400
33 : 560
35 : 797
37 : 1162
39 : 1706
41 : 2502
43 : 3673
45 : 5333
47 : 7756
49 : 11285
51 : 16457
53 : 24156
55 : 35569
57 : 52769
59 : 78319
61 : 116867
63 : 174207
65 : 260535
67 : 389264
69 : 582969
71 : 872258
73 : 1307863
75 : 1959086
77 : 2940441
79 : 4409199
81 : 6623647
19879711 representatives in total.
49679.40 ms (49 s 679.40 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22741944907520]
76407.51 ms (1 min 16 s 407.51 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22741947008768]
107508.67 ms (1 min 47 s 508.67 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:22741949110016]
139047.54 ms (2 min 19 s 47.54 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:22741954529024]
171065.14 ms (2 min 51 s 65.14 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:22741956630272]
171102.04 ms (2 min 51 s 102.04 ms) additional read duration.
Loaded 5 more representative collections of sizes:
83 : 22730041
85 : 38726684
87 : 62716073
89 : 101227436
91 : 157874085
403154030 representatives in total.
Thu Nov 16 17:15:31 2023: Inserted ≈ 5% of D-proof conclusions. [ 20157701 of 403154030] (ETC: Thu Nov 16 17:26:14 2023 ; 10 min 42 s 817.40 ms remaining ; 11 min 16 s 649.90 ms total)
Thu Nov 16 17:16:10 2023: Inserted ≈10% of D-proof conclusions. [ 40315403 of 403154030] (ETC: Thu Nov 16 17:27:05 2023 ; 10 min 55 s 268.89 ms remaining ; 12 min  8 s  76.54 ms total)
Thu Nov 16 17:16:55 2023: Inserted ≈15% of D-proof conclusions. [ 60473104 of 403154030] (ETC: Thu Nov 16 17:27:59 2023 ; 11 min  4 s 799.65 ms remaining ; 13 min  2 s 117.23 ms total)
Thu Nov 16 17:17:44 2023: Inserted ≈20% of D-proof conclusions. [ 80630806 of 403154030] (ETC: Thu Nov 16 17:28:50 2023 ; 11 min  6 s 165.20 ms remaining ; 13 min 52 s 706.50 ms total)
Thu Nov 16 17:18:20 2023: Inserted ≈25% of D-proof conclusions. [100788507 of 403154030] (ETC: Thu Nov 16 17:28:27 2023 ; 10 min  7 s 491.11 ms remaining ; 13 min 29 s 988.14 ms total)
Thu Nov 16 17:18:59 2023: Inserted ≈30% of D-proof conclusions. [120946209 of 403154030] (ETC: Thu Nov 16 17:28:23 2023 ; 9 min 24 s  19.80 ms remaining ; 13 min 25 s 742.57 ms total)
Thu Nov 16 17:19:53 2023: Inserted ≈35% of D-proof conclusions. [141103910 of 403154030] (ETC: Thu Nov 16 17:29:01 2023 ; 9 min  8 s 579.27 ms remaining ; 14 min  3 s 968.11 ms total)
Thu Nov 16 17:20:24 2023: Inserted ≈40% of D-proof conclusions. [161261612 of 403154030] (ETC: Thu Nov 16 17:28:34 2023 ; 8 min 10 s  56.11 ms remaining ; 13 min 36 s 760.19 ms total)
Thu Nov 16 17:20:53 2023: Inserted ≈45% of D-proof conclusions. [181419313 of 403154030] (ETC: Thu Nov 16 17:28:08 2023 ; 7 min 15 s 100.20 ms remaining ; 13 min 11 s  91.27 ms total)
Thu Nov 16 17:21:35 2023: Inserted ≈50% of D-proof conclusions. [201577015 of 403154030] (ETC: Thu Nov 16 17:28:12 2023 ; 6 min 37 s 363.46 ms remaining ; 13 min 14 s 726.92 ms total)
Thu Nov 16 17:22:16 2023: Inserted ≈55% of D-proof conclusions. [221734716 of 403154030] (ETC: Thu Nov 16 17:28:15 2023 ; 5 min 59 s 163.53 ms remaining ; 13 min 18 s 141.17 ms total)
Thu Nov 16 17:23:18 2023: Inserted ≈60% of D-proof conclusions. [241892418 of 403154030] (ETC: Thu Nov 16 17:28:51 2023 ; 5 min 33 s 574.69 ms remaining ; 13 min 53 s 936.72 ms total)
Thu Nov 16 17:23:53 2023: Inserted ≈65% of D-proof conclusions. [262050119 of 403154030] (ETC: Thu Nov 16 17:28:41 2023 ; 4 min 48 s 296.48 ms remaining ; 13 min 43 s 704.22 ms total)
Thu Nov 16 17:24:25 2023: Inserted ≈70% of D-proof conclusions. [282207821 of 403154030] (ETC: Thu Nov 16 17:28:28 2023 ; 4 min  3 s 226.86 ms remaining ; 13 min 30 s 756.19 ms total)
Thu Nov 16 17:24:55 2023: Inserted ≈75% of D-proof conclusions. [302365522 of 403154030] (ETC: Thu Nov 16 17:28:14 2023 ; 3 min 19 s 292.44 ms remaining ; 13 min 17 s 169.76 ms total)
Thu Nov 16 17:25:26 2023: Inserted ≈80% of D-proof conclusions. [322523224 of 403154030] (ETC: Thu Nov 16 17:28:03 2023 ; 2 min 37 s  88.52 ms remaining ; 13 min  5 s 442.57 ms total)
Thu Nov 16 17:26:02 2023: Inserted ≈85% of D-proof conclusions. [342680925 of 403154030] (ETC: Thu Nov 16 17:27:59 2023 ; 1 min 57 s 256.88 ms remaining ; 13 min  1 s 712.53 ms total)
Thu Nov 16 17:26:40 2023: Inserted ≈90% of D-proof conclusions. [362838627 of 403154030] (ETC: Thu Nov 16 17:27:58 2023 ; 1 min 18 s  79.69 ms remaining ; 13 min      796.88 ms total)
Thu Nov 16 17:27:25 2023: Inserted ≈95% of D-proof conclusions. [382996328 of 403154030] (ETC: Thu Nov 16 17:28:04 2023 ; 39 s 360.28 ms remaining ; 13 min  7 s 205.61 ms total)
Thu Nov 16 17:28:08 2023: Inserted 100% of D-proof conclusions. [403154030 of 403154030] (ETC: Thu Nov 16 17:28:08 2023 ; 0.00 ms remaining ; 13 min 10 s 832.98 ms total)
790834.43 ms (13 min 10 s 834.44 ms) total insertion duration.
Thu Nov 16 17:28:08 2023: Starting to iterate D-proof candidates of length 93.
1705474.92 ms (28 min 25 s 474.92 ms) taken to iterate 2979484674 condensed detachment proof strings of length 93.
[Copy] Next iteration count (unfiltered83+): { 93, 2979484674 }
Thu Nov 16 17:56:45 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Thu Nov 16 18:09:36 2023: Process terminated. [pid: 167189, tid:22742156158848]