( This log file was generated by '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.
  Wall-clock time:   8.6463888… h
  CPU utilization: 415.02666… core-h )
Thu Oct 26 11:40:13 2023: Process started. [pid: 164202, tid:23012151359360]
Tasks:
1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true)
2. generateDProofRepresentativeFiles(85, 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 generateDProofRepresentativeFiles(85, false, true).
Thu Oct 26 11:40:13 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 85, unfiltered]
0.02 ms taken to load initial representatives.
16.76 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23012091111168]
13.14 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23012089009920]
16.34 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23012086908672]
28.71 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23012084807424]
13.04 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23012082706176]
22.44 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23012080604928]
17.79 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23012078503680]
21.94 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23012076402432]
30.40 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23012074301184]
6.94 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23012072199936]
28.57 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23012070098688]
13.78 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23012067997440]
31.50 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23012065896192]
10.48 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23012063794944]
26.61 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23012061693696]
22.28 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23012059592448]
36.64 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23012057491200]
28.75 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23012055389952]
41.94 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23012053288704]
47.19 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23012051187456]
40.41 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23012049086208]
49.98 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23012046984960]
85.49 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23012044883712]
82.17 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23012042782464]
114.23 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23012040681216]
130.93 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23012038579968]
299.62 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23012036478720]
506.39 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23012034377472]
1036.35 ms (1 s 36.35 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23011830789888]
2124.15 ms (2 s 124.15 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23011828688640]
4736.42 ms (4 s 736.42 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23011826587392]
9352.83 ms (9 s 352.83 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23011824486144]
796.36 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23011822384896]
1075.58 ms (1 s 75.58 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23011820283648]
1623.67 ms (1 s 623.67 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23011818182400]
1958.65 ms (1 s 958.65 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23011816081152]
2415.47 ms (2 s 415.48 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23011813979904]
3225.47 ms (3 s 225.47 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23011811878656]
4159.25 ms (4 s 159.25 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23011809777408]
5261.39 ms (5 s 261.39 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23011807676160]
9372.94 ms (9 s 372.94 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.
14157.81 ms (14 s 157.81 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23011807676160]
14159.44 ms (14 s 159.44 ms) additional read duration.
Loaded 1 more representative collection of size:
83 : 22730041
42609752 representatives in total.
Thu Oct 26 11:40:38 2023: Inserted ≈ 5% of D-proof conclusions. [ 2130487 of 42609752] (ETC: Thu Oct 26 11:41:05 2023 ; 27 s 376.27 ms remaining ; 28 s 817.13 ms total)
Thu Oct 26 11:40:39 2023: Inserted ≈10% of D-proof conclusions. [ 4260975 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 26 s 506.59 ms remaining ; 29 s 451.76 ms total)
Thu Oct 26 11:40:41 2023: Inserted ≈15% of D-proof conclusions. [ 6391462 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 25 s 995.76 ms remaining ; 30 s 583.25 ms total)
Thu Oct 26 11:40:43 2023: Inserted ≈20% of D-proof conclusions. [ 8521950 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 24 s 908.07 ms remaining ; 31 s 135.09 ms total)
Thu Oct 26 11:40:44 2023: Inserted ≈25% of D-proof conclusions. [10652438 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 22 s 942.70 ms remaining ; 30 s 590.26 ms total)
Thu Oct 26 11:40:46 2023: Inserted ≈30% of D-proof conclusions. [12782925 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 21 s 553.17 ms remaining ; 30 s 790.24 ms total)
Thu Oct 26 11:40:47 2023: Inserted ≈35% of D-proof conclusions. [14913413 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 20 s 252.47 ms remaining ; 31 s 157.65 ms total)
Thu Oct 26 11:40:49 2023: Inserted ≈40% of D-proof conclusions. [17043900 of 42609752] (ETC: Thu Oct 26 11:41:08 2023 ; 18 s 819.12 ms remaining ; 31 s 365.20 ms total)
Thu Oct 26 11:40:51 2023: Inserted ≈45% of D-proof conclusions. [19174388 of 42609752] (ETC: Thu Oct 26 11:41:08 2023 ; 17 s 371.77 ms remaining ; 31 s 585.03 ms total)
Thu Oct 26 11:40:52 2023: Inserted ≈50% of D-proof conclusions. [21304876 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 15 s 539.65 ms remaining ; 31 s  79.31 ms total)
Thu Oct 26 11:40:53 2023: Inserted ≈55% of D-proof conclusions. [23435363 of 42609752] (ETC: Thu Oct 26 11:41:07 2023 ; 13 s 779.08 ms remaining ; 30 s 620.18 ms total)
Thu Oct 26 11:40:54 2023: Inserted ≈60% of D-proof conclusions. [25565851 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 12 s  67.87 ms remaining ; 30 s 169.68 ms total)
Thu Oct 26 11:40:56 2023: Inserted ≈65% of D-proof conclusions. [27696338 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 10 s 519.99 ms remaining ; 30 s  57.13 ms total)
Thu Oct 26 11:40:57 2023: Inserted ≈70% of D-proof conclusions. [29826826 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 8 s 947.82 ms remaining ; 29 s 826.07 ms total)
Thu Oct 26 11:40:58 2023: Inserted ≈75% of D-proof conclusions. [31957314 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 7 s 370.53 ms remaining ; 29 s 482.14 ms total)
Thu Oct 26 11:41:00 2023: Inserted ≈80% of D-proof conclusions. [34087801 of 42609752] (ETC: Thu Oct 26 11:41:06 2023 ; 5 s 853.20 ms remaining ; 29 s 266.01 ms total)
Thu Oct 26 11:41:01 2023: Inserted ≈85% of D-proof conclusions. [36218289 of 42609752] (ETC: Thu Oct 26 11:41:05 2023 ; 4 s 331.66 ms remaining ; 28 s 877.76 ms total)
Thu Oct 26 11:41:02 2023: Inserted ≈90% of D-proof conclusions. [38348776 of 42609752] (ETC: Thu Oct 26 11:41:05 2023 ; 2 s 858.49 ms remaining ; 28 s 584.93 ms total)
Thu Oct 26 11:41:03 2023: Inserted ≈95% of D-proof conclusions. [40479264 of 42609752] (ETC: Thu Oct 26 11:41:05 2023 ; 1 s 428.79 ms remaining ; 28 s 575.74 ms total)
Thu Oct 26 11:41:05 2023: Inserted 100% of D-proof conclusions. [42609752 of 42609752] (ETC: Thu Oct 26 11:41:05 2023 ; 0.00 ms remaining ; 28 s 581.87 ms total)
28582.09 ms (28 s 582.09 ms) total insertion duration.
Known iteration count loaded from 85:433296910.
Thu Oct 26 11:41:05 2023: Starting to generate D-proof representatives of length 85.
Thu Oct 26 11:54:36 2023: Iterated ≈ 2% of D-proof candidates. [  8665938 of 433296910] (ETC: Thu Oct 26 22:57:15 2023 ; 11 h  2 min 38 s 912.13 ms remaining ; 11 h 16 min 10 s 318.49 ms total)
Thu Oct 26 12:05:39 2023: Iterated ≈ 4% of D-proof candidates. [ 17331876 of 433296910] (ETC: Thu Oct 26 21:55:16 2023 ; 9 h 49 min 37 s  78.55 ms remaining ; 10 h 14 min 11 s 123.45 ms total)
Thu Oct 26 12:16:29 2023: Iterated ≈ 6% of D-proof candidates. [ 25997814 of 433296910] (ETC: Thu Oct 26 21:31:06 2023 ; 9 h 14 min 37 s 495.51 ms remaining ; 9 h 50 min  1 s 590.92 ms total)
Thu Oct 26 12:27:27 2023: Iterated ≈ 8% of D-proof candidates. [ 34663752 of 433296910] (ETC: Thu Oct 26 21:20:46 2023 ; 8 h 53 min 18 s 945.78 ms remaining ; 9 h 39 min 41 s 462.74 ms total)
Thu Oct 26 12:38:05 2023: Iterated ≈10% of D-proof candidates. [ 43329691 of 433296910] (ETC: Thu Oct 26 21:11:10 2023 ; 8 h 33 min  5 s  15.52 ms remaining ; 9 h 30 min  5 s 572.80 ms total)
Thu Oct 26 12:48:59 2023: Iterated ≈12% of D-proof candidates. [ 51995629 of 433296910] (ETC: Thu Oct 26 21:06:53 2023 ; 8 h 17 min 54 s 244.79 ms remaining ; 9 h 25 min 48 s   5.43 ms total)
Thu Oct 26 12:59:16 2023: Iterated ≈14% of D-proof candidates. [ 60661567 of 433296910] (ETC: Thu Oct 26 20:59:32 2023 ; 8 h        16 s 225.45 ms remaining ; 9 h 18 min 27 s 238.86 ms total)
Thu Oct 26 13:10:04 2023: Iterated ≈16% of D-proof candidates. [ 69327505 of 433296910] (ETC: Thu Oct 26 20:57:15 2023 ; 7 h 47 min 10 s 520.77 ms remaining ; 9 h 16 min  9 s 667.53 ms total)
Thu Oct 26 13:20:01 2023: Iterated ≈18% of D-proof candidates. [ 77993443 of 433296910] (ETC: Thu Oct 26 20:50:42 2023 ; 7 h 30 min 41 s 469.95 ms remaining ; 9 h  9 min 37 s 402.30 ms total)
Thu Oct 26 13:30:22 2023: Iterated ≈20% of D-proof candidates. [ 86659382 of 433296910] (ETC: Thu Oct 26 20:47:28 2023 ; 7 h 17 min  6 s 605.31 ms remaining ; 9 h  6 min 23 s 256.63 ms total)
Thu Oct 26 13:40:02 2023: Iterated ≈22% of D-proof candidates. [ 95325320 of 433296910] (ETC: Thu Oct 26 20:41:48 2023 ; 7 h  1 min 45 s 968.98 ms remaining ; 9 h        43 s 549.96 ms total)
Thu Oct 26 13:50:11 2023: Iterated ≈24% of D-proof candidates. [103991258 of 433296910] (ETC: Thu Oct 26 20:38:58 2023 ; 6 h 48 min 47 s 446.74 ms remaining ; 8 h 57 min 52 s 956.20 ms total)
Thu Oct 26 14:00:19 2023: Iterated ≈26% of D-proof candidates. [112657196 of 433296910] (ETC: Thu Oct 26 20:36:38 2023 ; 6 h 36 min 18 s 477.74 ms remaining ; 8 h 55 min 33 s  77.97 ms total)
Thu Oct 26 14:09:56 2023: Iterated ≈28% of D-proof candidates. [121323134 of 433296910] (ETC: Thu Oct 26 20:32:43 2023 ; 6 h 22 min 47 s   0.55 ms remaining ; 8 h 51 min 38 s 611.79 ms total)
Thu Oct 26 14:20:12 2023: Iterated ≈30% of D-proof candidates. [129989072 of 433296910] (ETC: Thu Oct 26 20:31:28 2023 ; 6 h 11 min 16 s 157.45 ms remaining ; 8 h 50 min 23 s  81.97 ms total)
Thu Oct 26 14:29:50 2023: Iterated ≈32% of D-proof candidates. [138655011 of 433296910] (ETC: Thu Oct 26 20:28:25 2023 ; 5 h 58 min 35 s 394.53 ms remaining ; 8 h 47 min 20 s 286.05 ms total)
Thu Oct 26 14:39:59 2023: Iterated ≈34% of D-proof candidates. [147320949 of 433296910] (ETC: Thu Oct 26 20:27:16 2023 ; 5 h 47 min 17 s  74.80 ms remaining ; 8 h 46 min 11 s 325.41 ms total)
Thu Oct 26 14:49:52 2023: Iterated ≈36% of D-proof candidates. [155986887 of 433296910] (ETC: Thu Oct 26 20:25:28 2023 ; 5 h 35 min 36 s 307.20 ms remaining ; 8 h 44 min 22 s 979.93 ms total)
Thu Oct 26 14:59:56 2023: Iterated ≈38% of D-proof candidates. [164652825 of 433296910] (ETC: Thu Oct 26 20:24:21 2023 ; 5 h 24 min 25 s 854.92 ms remaining ; 8 h 43 min 16 s 540.11 ms total)
Thu Oct 26 15:09:59 2023: Iterated ≈40% of D-proof candidates. [173318764 of 433296910] (ETC: Thu Oct 26 20:23:21 2023 ; 5 h 13 min 21 s 889.61 ms remaining ; 8 h 42 min 16 s 482.68 ms total)
Thu Oct 26 15:20:05 2023: Iterated ≈42% of D-proof candidates. [181984702 of 433296910] (ETC: Thu Oct 26 20:22:32 2023 ; 5 h  2 min 26 s 568.83 ms remaining ; 8 h 41 min 27 s 187.61 ms total)
Thu Oct 26 15:30:08 2023: Iterated ≈44% of D-proof candidates. [190650640 of 433296910] (ETC: Thu Oct 26 20:21:39 2023 ; 4 h 51 min 30 s 967.75 ms remaining ; 8 h 40 min 33 s 870.93 ms total)
Thu Oct 26 15:40:08 2023: Iterated ≈46% of D-proof candidates. [199316578 of 433296910] (ETC: Thu Oct 26 20:20:45 2023 ; 4 h 40 min 37 s 371.24 ms remaining ; 8 h 39 min 40 s 317.02 ms total)
Thu Oct 26 15:50:10 2023: Iterated ≈48% of D-proof candidates. [207982516 of 433296910] (ETC: Thu Oct 26 20:20:01 2023 ; 4 h 29 min 50 s 893.52 ms remaining ; 8 h 38 min 56 s 333.59 ms total)
Thu Oct 26 16:00:01 2023: Iterated ≈50% of D-proof candidates. [216648454 of 433296910] (ETC: Thu Oct 26 20:18:57 2023 ; 4 h 18 min 56 s 140.78 ms remaining ; 8 h 37 min 52 s 281.42 ms total)
Thu Oct 26 16:09:50 2023: Iterated ≈52% of D-proof candidates. [225314393 of 433296910] (ETC: Thu Oct 26 20:17:55 2023 ; 4 h  8 min  5 s   5.26 ms remaining ; 8 h 36 min 50 s 427.59 ms total)
Thu Oct 26 16:19:46 2023: Iterated ≈54% of D-proof candidates. [233980331 of 433296910] (ETC: Thu Oct 26 20:17:10 2023 ; 3 h 57 min 24 s   4.45 ms remaining ; 8 h 36 min  5 s 227.00 ms total)
Thu Oct 26 16:29:39 2023: Iterated ≈56% of D-proof candidates. [242646269 of 433296910] (ETC: Thu Oct 26 20:16:24 2023 ; 3 h 46 min 44 s 232.31 ms remaining ; 8 h 35 min 18 s 709.70 ms total)
Thu Oct 26 16:39:27 2023: Iterated ≈58% of D-proof candidates. [251312207 of 433296910] (ETC: Thu Oct 26 20:15:30 2023 ; 3 h 36 min  3 s 267.08 ms remaining ; 8 h 34 min 24 s 921.48 ms total)
Thu Oct 26 16:49:03 2023: Iterated ≈60% of D-proof candidates. [259978145 of 433296910] (ETC: Thu Oct 26 20:14:22 2023 ; 3 h 25 min 19 s  35.63 ms remaining ; 8 h 33 min 17 s 588.91 ms total)
Thu Oct 26 16:59:02 2023: Iterated ≈62% of D-proof candidates. [268644084 of 433296910] (ETC: Thu Oct 26 20:13:54 2023 ; 3 h 14 min 52 s 335.61 ms remaining ; 8 h 32 min 49 s 304.20 ms total)
Thu Oct 26 17:08:56 2023: Iterated ≈64% of D-proof candidates. [277310022 of 433296910] (ETC: Thu Oct 26 20:13:21 2023 ; 3 h  4 min 24 s 869.60 ms remaining ; 8 h 32 min 15 s 748.82 ms total)
Thu Oct 26 17:18:38 2023: Iterated ≈66% of D-proof candidates. [285975960 of 433296910] (ETC: Thu Oct 26 20:12:31 2023 ; 2 h 53 min 53 s 365.12 ms remaining ; 8 h 31 min 26 s 367.88 ms total)
Thu Oct 26 17:28:30 2023: Iterated ≈68% of D-proof candidates. [294641898 of 433296910] (ETC: Thu Oct 26 20:11:59 2023 ; 2 h 43 min 29 s 422.37 ms remaining ; 8 h 30 min 54 s 444.74 ms total)
Thu Oct 26 17:38:25 2023: Iterated ≈70% of D-proof candidates. [303307837 of 433296910] (ETC: Thu Oct 26 20:11:34 2023 ; 2 h 33 min  8 s 608.47 ms remaining ; 8 h 30 min 28 s 694.89 ms total)
Thu Oct 26 17:48:24 2023: Iterated ≈72% of D-proof candidates. [311973775 of 433296910] (ETC: Thu Oct 26 20:11:15 2023 ; 2 h 22 min 50 s 936.11 ms remaining ; 8 h 30 min 10 s 486.06 ms total)
Thu Oct 26 17:58:22 2023: Iterated ≈74% of D-proof candidates. [320639713 of 433296910] (ETC: Thu Oct 26 20:10:55 2023 ; 2 h 12 min 33 s 428.60 ms remaining ; 8 h 29 min 50 s 109.91 ms total)
Thu Oct 26 18:08:15 2023: Iterated ≈76% of D-proof candidates. [329305651 of 433296910] (ETC: Thu Oct 26 20:10:31 2023 ; 2 h  2 min 15 s 914.14 ms remaining ; 8 h 29 min 26 s 308.75 ms total)
Thu Oct 26 18:18:17 2023: Iterated ≈78% of D-proof candidates. [337971589 of 433296910] (ETC: Thu Oct 26 20:10:19 2023 ; 1 h 52 min  1 s 966.79 ms remaining ; 8 h 29 min 14 s 394.26 ms total)
Thu Oct 26 18:28:21 2023: Iterated ≈80% of D-proof candidates. [346637528 of 433296910] (ETC: Thu Oct 26 20:10:10 2023 ; 1 h 41 min 48 s 929.80 ms remaining ; 8 h 29 min  4 s 648.98 ms total)
Thu Oct 26 18:38:27 2023: Iterated ≈82% of D-proof candidates. [355303466 of 433296910] (ETC: Thu Oct 26 20:10:04 2023 ; 1 h 31 min 37 s  89.12 ms remaining ; 8 h 28 min 59 s 383.94 ms total)
Thu Oct 26 18:48:38 2023: Iterated ≈84% of D-proof candidates. [363969404 of 433296910] (ETC: Thu Oct 26 20:10:04 2023 ; 1 h 21 min 26 s 264.50 ms remaining ; 8 h 28 min 59 s 152.94 ms total)
Thu Oct 26 18:58:46 2023: Iterated ≈86% of D-proof candidates. [372635342 of 433296910] (ETC: Thu Oct 26 20:10:01 2023 ; 1 h 11 min 15 s 107.50 ms remaining ; 8 h 28 min 56 s 481.87 ms total)
Thu Oct 26 19:08:50 2023: Iterated ≈88% of D-proof candidates. [381301280 of 433296910] (ETC: Thu Oct 26 20:09:54 2023 ; 1 h  1 min  3 s 441.64 ms remaining ; 8 h 28 min 48 s 679.87 ms total)
Thu Oct 26 19:18:56 2023: Iterated ≈90% of D-proof candidates. [389967218 of 433296910] (ETC: Thu Oct 26 20:09:49 2023 ; 50 min 52 s 384.67 ms remaining ; 8 h 28 min 43 s 846.03 ms total)
Thu Oct 26 19:28:59 2023: Iterated ≈92% of D-proof candidates. [398633157 of 433296910] (ETC: Thu Oct 26 20:09:41 2023 ; 40 min 41 s 260.75 ms remaining ; 8 h 28 min 35 s 759.21 ms total)
Thu Oct 26 19:39:00 2023: Iterated ≈94% of D-proof candidates. [407299095 of 433296910] (ETC: Thu Oct 26 20:09:30 2023 ; 30 min 30 s 329.02 ms remaining ; 8 h 28 min 25 s 483.25 ms total)
Thu Oct 26 19:48:57 2023: Iterated ≈96% of D-proof candidates. [415965033 of 433296910] (ETC: Thu Oct 26 20:09:17 2023 ; 20 min 19 s 680.93 ms remaining ; 8 h 28 min 12 s  22.17 ms total)
Thu Oct 26 19:58:48 2023: Iterated ≈98% of D-proof candidates. [424630971 of 433296910] (ETC: Thu Oct 26 20:08:57 2023 ; 10 min  9 s 449.35 ms remaining ; 8 h 27 min 52 s 464.92 ms total)
Thu Oct 26 20:08:43 2023: Iterated 100% of D-proof candidates. [433296909 of 433296910] (ETC: Thu Oct 26 20:08:43 2023 ; 0.07 ms remaining ; 8 h 27 min 37 s 971.55 ms total)
30458415.32 ms (8 h 27 min 38 s 415.32 ms) taken to collect 38726684 D-proofs of length 85. [iterated 433296910 condensed detachment proof strings]
[Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 10 }, { 11, 22 }, { 13, 38 }, { 15, 71 }, { 17, 118 }, { 19, 202 }, { 21, 334 }, { 23, 569 }, { 25, 950 }, { 27, 1592 }, { 29, 2608 }, { 31, 4241 }, { 33, 6762 }, { 35, 10683 }, { 37, 16666 }, { 39, 25862 }, { 41, 39912 }, { 43, 61603 }, { 45, 94986 }, { 47, 146305 }, { 49, 224682 }, { 51, 343672 }, { 53, 523454 }, { 55, 794596 }, { 57, 1203760 }, { 59, 1822563 }, { 61, 2759474 }, { 63, 4180702 }, { 65, 6335388 }, { 67, 9603788 }, { 69, 14556142 }, { 71, 22063703 }, { 73, 33439008 }, { 75, 50690848 }, { 77, 76854816 }, { 79, 116576814 }, { 81, 176882404 }, { 83, 268514198 }, { 85, 433296910 } }
341975.85 ms (5 min 41 s 975.85 ms) taken to filter and order new representative proofs.
Found 38726684 representative, 101622050 redundant, and 292948176 invalid condensed detachment proof strings.
lengths up to 85 ; amounts per length: {(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), (83,22730041), (85,38726684)} ; 38726684 new representative proofs (101622050 redundant, 292948176 invalid)
Thu Oct 26 20:15:22 2023: Starting to write 38726684 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt.
61333.20 ms (1 min 1 s 333.20 ms) taken to print and save 14942566211 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt.
Thu Oct 26 20:17:27 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 85, unfiltered]
Thu Oct 26 20:19:00 2023: Process terminated. [pid: 164202, tid:23012151359360]