( 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-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.
  Wall-clock time:  10.6175 h
  CPU utilization: 679.52 core-h )
Fri Oct 27 14:32:03 2023: Process started. [pid: 93532, tid:22976569104256]
Tasks:
1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true)
2. generateDProofRepresentativeFiles(87, 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(87, false, true).
Fri Oct 27 14:32:03 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 87, unfiltered]
0.00 ms taken to load initial representatives.
22.19 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22976508880640]
12.05 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22976506779392]
22.17 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22976504678144]
11.72 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22976502576896]
18.90 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22976500475648]
28.36 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22976498374400]
17.40 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22976496273152]
21.04 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22976494171904]
34.20 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22976492070656]
22.65 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22976489969408]
9.71 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22976487868160]
19.32 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22976485766912]
26.84 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22976483665664]
29.98 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22976481564416]
26.54 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22976479463168]
27.25 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22976477361920]
36.80 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22976475260672]
25.23 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22976473159424]
52.44 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22976471058176]
48.43 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22976468956928]
38.40 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22976466855680]
191.74 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22975055132416]
252.62 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22975189350144]
162.28 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22975187248896]
477.38 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22975185147648]
571.20 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22975183046400]
808.26 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22975180945152]
863.59 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22975178843904]
1007.27 ms (1 s 7.27 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22975176742656]
3003.11 ms (3 s 3.11 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22975174641408]
4674.72 ms (4 s 674.73 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22975172540160]
7229.01 ms (7 s 229.00 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22975170438912]
2907.75 ms (2 s 907.75 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22975168337664]
3547.90 ms (3 s 547.90 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22975166236416]
4536.91 ms (4 s 536.91 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22975164135168]
6068.38 ms (6 s 68.38 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22975162033920]
6612.49 ms (6 s 612.49 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22975159932672]
7269.71 ms (7 s 269.71 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22975157831424]
7943.80 ms (7 s 943.80 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22975155730176]
8824.14 ms (8 s 824.14 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22975153628928]
8919.28 ms (8 s 919.28 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.
12866.78 ms (12 s 866.78 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22975153628928]
23169.58 ms (23 s 169.58 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22975155730176]
23177.67 ms (23 s 177.68 ms) additional read duration.
Loaded 2 more representative collections of sizes:
83 : 22730041
85 : 38726684
81336436 representatives in total.
Fri Oct 27 14:32:41 2023: Inserted ≈ 5% of D-proof conclusions. [ 4066821 of 81336436] (ETC: Fri Oct 27 14:34:17 2023 ; 1 min 36 s 469.71 ms remaining ; 1 min 41 s 547.06 ms total)
Fri Oct 27 14:32:47 2023: Inserted ≈10% of D-proof conclusions. [ 8133643 of 81336436] (ETC: Fri Oct 27 14:34:27 2023 ; 1 min 40 s 295.08 ms remaining ; 1 min 51 s 438.98 ms total)
Fri Oct 27 14:32:52 2023: Inserted ≈15% of D-proof conclusions. [12200465 of 81336436] (ETC: Fri Oct 27 14:34:24 2023 ; 1 min 32 s 467.35 ms remaining ; 1 min 48 s 785.12 ms total)
Fri Oct 27 14:32:57 2023: Inserted ≈20% of D-proof conclusions. [16267287 of 81336436] (ETC: Fri Oct 27 14:34:24 2023 ; 1 min 26 s 333.15 ms remaining ; 1 min 47 s 916.44 ms total)
Fri Oct 27 14:33:02 2023: Inserted ≈25% of D-proof conclusions. [20334109 of 81336436] (ETC: Fri Oct 27 14:34:20 2023 ; 1 min 18 s 590.53 ms remaining ; 1 min 44 s 787.38 ms total)
Fri Oct 27 14:33:06 2023: Inserted ≈30% of D-proof conclusions. [24400930 of 81336436] (ETC: Fri Oct 27 14:34:18 2023 ; 1 min 11 s 687.49 ms remaining ; 1 min 42 s 410.69 ms total)
Fri Oct 27 14:33:11 2023: Inserted ≈35% of D-proof conclusions. [28467752 of 81336436] (ETC: Fri Oct 27 14:34:16 2023 ; 1 min  5 s  21.79 ms remaining ; 1 min 40 s  33.52 ms total)
Fri Oct 27 14:33:15 2023: Inserted ≈40% of D-proof conclusions. [32534574 of 81336436] (ETC: Fri Oct 27 14:34:14 2023 ; 58 s 972.64 ms remaining ; 1 min 38 s 287.74 ms total)
Fri Oct 27 14:33:19 2023: Inserted ≈45% of D-proof conclusions. [36601396 of 81336436] (ETC: Fri Oct 27 14:34:13 2023 ; 53 s 497.17 ms remaining ; 1 min 37 s 267.57 ms total)
Fri Oct 27 14:33:24 2023: Inserted ≈50% of D-proof conclusions. [40668218 of 81336436] (ETC: Fri Oct 27 14:34:12 2023 ; 48 s 418.05 ms remaining ; 1 min 36 s 836.10 ms total)
Fri Oct 27 14:33:29 2023: Inserted ≈55% of D-proof conclusions. [44735039 of 81336436] (ETC: Fri Oct 27 14:34:12 2023 ; 43 s 438.18 ms remaining ; 1 min 36 s 529.29 ms total)
Fri Oct 27 14:33:33 2023: Inserted ≈60% of D-proof conclusions. [48801861 of 81336436] (ETC: Fri Oct 27 14:34:12 2023 ; 38 s 569.10 ms remaining ; 1 min 36 s 422.75 ms total)
Fri Oct 27 14:33:39 2023: Inserted ≈65% of D-proof conclusions. [52868683 of 81336436] (ETC: Fri Oct 27 14:34:13 2023 ; 33 s 909.62 ms remaining ; 1 min 36 s 884.61 ms total)
Fri Oct 27 14:33:44 2023: Inserted ≈70% of D-proof conclusions. [56935505 of 81336436] (ETC: Fri Oct 27 14:34:13 2023 ; 29 s 162.91 ms remaining ; 1 min 37 s 209.69 ms total)
Fri Oct 27 14:33:49 2023: Inserted ≈75% of D-proof conclusions. [61002327 of 81336436] (ETC: Fri Oct 27 14:34:13 2023 ; 24 s 325.24 ms remaining ; 1 min 37 s 300.96 ms total)
Fri Oct 27 14:33:54 2023: Inserted ≈80% of D-proof conclusions. [65069148 of 81336436] (ETC: Fri Oct 27 14:34:13 2023 ; 19 s 500.36 ms remaining ; 1 min 37 s 501.81 ms total)
Fri Oct 27 14:33:59 2023: Inserted ≈85% of D-proof conclusions. [69135970 of 81336436] (ETC: Fri Oct 27 14:34:14 2023 ; 14 s 726.26 ms remaining ; 1 min 38 s 175.07 ms total)
Fri Oct 27 14:34:05 2023: Inserted ≈90% of D-proof conclusions. [73202792 of 81336436] (ETC: Fri Oct 27 14:34:15 2023 ; 9 s 936.32 ms remaining ; 1 min 39 s 363.19 ms total)
Fri Oct 27 14:34:11 2023: Inserted ≈95% of D-proof conclusions. [77269614 of 81336436] (ETC: Fri Oct 27 14:34:17 2023 ; 5 s  45.62 ms remaining ; 1 min 40 s 912.31 ms total)
Fri Oct 27 14:34:20 2023: Inserted 100% of D-proof conclusions. [81336436 of 81336436] (ETC: Fri Oct 27 14:34:20 2023 ; 0.00 ms remaining ; 1 min 44 s 139.16 ms total)
104139.34 ms (1 min 44 s 139.34 ms) total insertion duration.
Known iteration count loaded from 87:692467431.
Fri Oct 27 14:34:20 2023: Starting to generate D-proof representatives of length 87.
Fri Oct 27 14:49:08 2023: Iterated ≈ 2% of D-proof candidates. [ 13849348 of 692467431] (ETC: Sat Oct 28 02:54:36 2023 ; 12 h  5 min 27 s 550.37 ms remaining ; 12 h 20 min 15 s 867.69 ms total)
Fri Oct 27 15:02:32 2023: Iterated ≈ 4% of D-proof candidates. [ 27698697 of 692467431] (ETC: Sat Oct 28 02:19:14 2023 ; 11 h 16 min 42 s 292.78 ms remaining ; 11 h 44 min 54 s  54.97 ms total)
Fri Oct 27 15:15:36 2023: Iterated ≈ 6% of D-proof candidates. [ 41548045 of 692467431] (ETC: Sat Oct 28 02:02:18 2023 ; 10 h 46 min 41 s 448.41 ms remaining ; 11 h 27 min 58 s 136.55 ms total)
Fri Oct 27 15:29:24 2023: Iterated ≈ 8% of D-proof candidates. [ 55397394 of 692467431] (ETC: Sat Oct 28 02:02:49 2023 ; 10 h 33 min 24 s 225.05 ms remaining ; 11 h 28 min 28 s 940.25 ms total)
Fri Oct 27 15:42:13 2023: Iterated ≈10% of D-proof candidates. [ 69246743 of 692467431] (ETC: Sat Oct 28 01:53:10 2023 ; 10 h 10 min 57 s  57.15 ms remaining ; 11 h 18 min 50 s  63.49 ms total)
Fri Oct 27 15:55:21 2023: Iterated ≈12% of D-proof candidates. [ 83096091 of 692467431] (ETC: Sat Oct 28 01:49:26 2023 ; 9 h 54 min  5 s 693.51 ms remaining ; 11 h 15 min  6 s 469.85 ms total)
Fri Oct 27 16:08:43 2023: Iterated ≈14% of D-proof candidates. [ 96945440 of 692467431] (ETC: Sat Oct 28 01:48:31 2023 ; 9 h 39 min 47 s 648.32 ms remaining ; 11 h 14 min 10 s 753.84 ms total)
Fri Oct 27 16:21:29 2023: Iterated ≈16% of D-proof candidates. [110794788 of 692467431] (ETC: Sat Oct 28 01:44:03 2023 ; 9 h 22 min 33 s 546.90 ms remaining ; 11 h  9 min 42 s 793.87 ms total)
Fri Oct 27 16:33:43 2023: Iterated ≈18% of D-proof candidates. [124644137 of 692467431] (ETC: Sat Oct 28 01:37:35 2023 ; 9 h  3 min 51 s 974.58 ms remaining ; 11 h  3 min 15 s  90.91 ms total)
Fri Oct 27 16:46:07 2023: Iterated ≈20% of D-proof candidates. [138493486 of 692467431] (ETC: Sat Oct 28 01:33:16 2023 ; 8 h 47 min  8 s 638.66 ms remaining ; 10 h 58 min 55 s 798.31 ms total)
Fri Oct 27 16:58:25 2023: Iterated ≈22% of D-proof candidates. [152342834 of 692467431] (ETC: Sat Oct 28 01:29:15 2023 ; 8 h 30 min 50 s 284.35 ms remaining ; 10 h 54 min 55 s 236.28 ms total)
Fri Oct 27 17:10:38 2023: Iterated ≈24% of D-proof candidates. [166192183 of 692467431] (ETC: Sat Oct 28 01:25:34 2023 ; 8 h 14 min 56 s 594.20 ms remaining ; 10 h 51 min 14 s 466.01 ms total)
Fri Oct 27 17:22:46 2023: Iterated ≈26% of D-proof candidates. [180041532 of 692467431] (ETC: Sat Oct 28 01:22:11 2023 ; 7 h 59 min 24 s 521.80 ms remaining ; 10 h 47 min 50 s 975.40 ms total)
Fri Oct 27 17:35:00 2023: Iterated ≈28% of D-proof candidates. [193890880 of 692467431] (ETC: Sat Oct 28 01:19:35 2023 ; 7 h 44 min 34 s 869.49 ms remaining ; 10 h 45 min 15 s  96.47 ms total)
Fri Oct 27 17:47:11 2023: Iterated ≈30% of D-proof candidates. [207740229 of 692467431] (ETC: Sat Oct 28 01:17:11 2023 ; 7 h 29 min 59 s 635.96 ms remaining ; 10 h 42 min 50 s 908.49 ms total)
Fri Oct 27 17:59:18 2023: Iterated ≈32% of D-proof candidates. [221589577 of 692467431] (ETC: Sat Oct 28 01:14:52 2023 ; 7 h 15 min 33 s 747.79 ms remaining ; 10 h 40 min 31 s 981.98 ms total)
Fri Oct 27 18:11:26 2023: Iterated ≈34% of D-proof candidates. [235438926 of 692467431] (ETC: Sat Oct 28 01:12:53 2023 ; 7 h  1 min 27 s   8.06 ms remaining ; 10 h 38 min 33 s 648.53 ms total)
Fri Oct 27 18:23:45 2023: Iterated ≈36% of D-proof candidates. [249288275 of 692467431] (ETC: Sat Oct 28 01:11:35 2023 ; 6 h 47 min 50 s 770.97 ms remaining ; 10 h 37 min 15 s 579.63 ms total)
Fri Oct 27 18:35:53 2023: Iterated ≈38% of D-proof candidates. [263137623 of 692467431] (ETC: Sat Oct 28 01:10:00 2023 ; 6 h 34 min  6 s 899.92 ms remaining ; 10 h 35 min 40 s 161.10 ms total)
Fri Oct 27 18:48:17 2023: Iterated ≈40% of D-proof candidates. [276986972 of 692467431] (ETC: Sat Oct 28 01:09:13 2023 ; 6 h 20 min 55 s 711.36 ms remaining ; 10 h 34 min 52 s 852.23 ms total)
Fri Oct 27 19:00:27 2023: Iterated ≈42% of D-proof candidates. [290836321 of 692467431] (ETC: Sat Oct 28 01:07:57 2023 ; 6 h  7 min 29 s 860.42 ms remaining ; 10 h 33 min 37 s   0.72 ms total)
Fri Oct 27 19:12:45 2023: Iterated ≈44% of D-proof candidates. [304685669 of 692467431] (ETC: Sat Oct 28 01:07:07 2023 ; 5 h 54 min 21 s 383.57 ms remaining ; 10 h 32 min 46 s 756.31 ms total)
Fri Oct 27 19:24:55 2023: Iterated ≈46% of D-proof candidates. [318535018 of 692467431] (ETC: Sat Oct 28 01:06:02 2023 ; 5 h 41 min  7 s 216.19 ms remaining ; 10 h 31 min 42 s 252.17 ms total)
Fri Oct 27 19:37:08 2023: Iterated ≈48% of D-proof candidates. [332384366 of 692467431] (ETC: Sat Oct 28 01:05:10 2023 ; 5 h 28 min  2 s 133.49 ms remaining ; 10 h 30 min 50 s 256.63 ms total)
Fri Oct 27 19:49:16 2023: Iterated ≈50% of D-proof candidates. [346233715 of 692467431] (ETC: Sat Oct 28 01:04:13 2023 ; 5 h 14 min 56 s 560.26 ms remaining ; 10 h 29 min 53 s 120.48 ms total)
Fri Oct 27 20:01:29 2023: Iterated ≈52% of D-proof candidates. [360083064 of 692467431] (ETC: Sat Oct 28 01:03:28 2023 ; 5 h  1 min 59 s 207.35 ms remaining ; 10 h 29 min  8 s 348.63 ms total)
Fri Oct 27 20:13:30 2023: Iterated ≈54% of D-proof candidates. [373932412 of 692467431] (ETC: Sat Oct 28 01:02:26 2023 ; 4 h 48 min 55 s 616.80 ms remaining ; 10 h 28 min  6 s 123.39 ms total)
Fri Oct 27 20:25:37 2023: Iterated ≈56% of D-proof candidates. [387781761 of 692467431] (ETC: Sat Oct 28 01:01:37 2023 ; 4 h 36 min      319.26 ms remaining ; 10 h 27 min 17 s  89.19 ms total)
Fri Oct 27 20:37:40 2023: Iterated ≈58% of D-proof candidates. [401631109 of 692467431] (ETC: Sat Oct 28 01:00:47 2023 ; 4 h 23 min  6 s 655.37 ms remaining ; 10 h 26 min 27 s 274.57 ms total)
Fri Oct 27 20:49:45 2023: Iterated ≈60% of D-proof candidates. [415480458 of 692467431] (ETC: Sat Oct 28 01:00:03 2023 ; 4 h 10 min 17 s 139.23 ms remaining ; 10 h 25 min 42 s 848.00 ms total)
Fri Oct 27 21:01:47 2023: Iterated ≈62% of D-proof candidates. [429329807 of 692467431] (ETC: Sat Oct 28 00:59:16 2023 ; 3 h 57 min 28 s 414.85 ms remaining ; 10 h 24 min 55 s 828.51 ms total)
Fri Oct 27 21:13:45 2023: Iterated ≈64% of D-proof candidates. [443179155 of 692467431] (ETC: Sat Oct 28 00:58:25 2023 ; 3 h 44 min 40 s 320.36 ms remaining ; 10 h 24 min  5 s 334.21 ms total)
Fri Oct 27 21:25:53 2023: Iterated ≈66% of D-proof candidates. [457028504 of 692467431] (ETC: Sat Oct 28 00:57:53 2023 ; 3 h 32 min      594.86 ms remaining ; 10 h 23 min 33 s 514.22 ms total)
Fri Oct 27 21:38:02 2023: Iterated ≈68% of D-proof candidates. [470877853 of 692467431] (ETC: Sat Oct 28 00:57:25 2023 ; 3 h 19 min 23 s 433.47 ms remaining ; 10 h 23 min  5 s 729.59 ms total)
Fri Oct 27 21:50:15 2023: Iterated ≈70% of D-proof candidates. [484727201 of 692467431] (ETC: Sat Oct 28 00:57:05 2023 ; 3 h  6 min 49 s 460.78 ms remaining ; 10 h 22 min 44 s 869.13 ms total)
Fri Oct 27 22:02:25 2023: Iterated ≈72% of D-proof candidates. [498576550 of 692467431] (ETC: Sat Oct 28 00:56:41 2023 ; 2 h 54 min 15 s 451.32 ms remaining ; 10 h 22 min 20 s 897.50 ms total)
Fri Oct 27 22:14:35 2023: Iterated ≈74% of D-proof candidates. [512425898 of 692467431] (ETC: Sat Oct 28 00:56:17 2023 ; 2 h 41 min 42 s 478.42 ms remaining ; 10 h 21 min 57 s 224.49 ms total)
Fri Oct 27 22:26:49 2023: Iterated ≈76% of D-proof candidates. [526275247 of 692467431] (ETC: Sat Oct 28 00:56:02 2023 ; 2 h 29 min 12 s 479.85 ms remaining ; 10 h 21 min 41 s 999.27 ms total)
Fri Oct 27 22:39:08 2023: Iterated ≈78% of D-proof candidates. [540124596 of 692467431] (ETC: Sat Oct 28 00:55:52 2023 ; 2 h 16 min 44 s 267.99 ms remaining ; 10 h 21 min 32 s 127.19 ms total)
Fri Oct 27 22:51:25 2023: Iterated ≈80% of D-proof candidates. [553973944 of 692467431] (ETC: Sat Oct 28 00:55:41 2023 ; 2 h  4 min 16 s 193.74 ms remaining ; 10 h 21 min 20 s 968.50 ms total)
Fri Oct 27 23:03:44 2023: Iterated ≈82% of D-proof candidates. [567823293 of 692467431] (ETC: Sat Oct 28 00:55:33 2023 ; 1 h 51 min 49 s 163.05 ms remaining ; 10 h 21 min 13 s 127.92 ms total)
Fri Oct 27 23:16:00 2023: Iterated ≈84% of D-proof candidates. [581672642 of 692467431] (ETC: Sat Oct 28 00:55:22 2023 ; 1 h 39 min 21 s 948.13 ms remaining ; 10 h 21 min  2 s 175.80 ms total)
Fri Oct 27 23:28:21 2023: Iterated ≈86% of D-proof candidates. [595521990 of 692467431] (ETC: Sat Oct 28 00:55:17 2023 ; 1 h 26 min 55 s 965.63 ms remaining ; 10 h 20 min 56 s 897.10 ms total)
Fri Oct 27 23:40:37 2023: Iterated ≈88% of D-proof candidates. [609371339 of 692467431] (ETC: Sat Oct 28 00:55:06 2023 ; 1 h 14 min 29 s 577.31 ms remaining ; 10 h 20 min 46 s 477.43 ms total)
Fri Oct 27 23:52:55 2023: Iterated ≈90% of D-proof candidates. [623220687 of 692467431] (ETC: Sat Oct 28 00:54:59 2023 ; 1 h  2 min  3 s 887.90 ms remaining ; 10 h 20 min 38 s 878.50 ms total)
Sat Oct 28 00:05:08 2023: Iterated ≈92% of D-proof candidates. [637070036 of 692467431] (ETC: Sat Oct 28 00:54:46 2023 ; 49 min 38 s  84.20 ms remaining ; 10 h 20 min 26 s  52.17 ms total)
Sat Oct 28 00:17:22 2023: Iterated ≈94% of D-proof candidates. [650919385 of 692467431] (ETC: Sat Oct 28 00:54:35 2023 ; 37 min 12 s 926.28 ms remaining ; 10 h 20 min 15 s 437.83 ms total)
Sat Oct 28 00:29:27 2023: Iterated ≈96% of D-proof candidates. [664768733 of 692467431] (ETC: Sat Oct 28 00:54:15 2023 ; 24 min 47 s 810.91 ms remaining ; 10 h 19 min 55 s 271.70 ms total)
Sat Oct 28 00:41:40 2023: Iterated ≈98% of D-proof candidates. [678618082 of 692467431] (ETC: Sat Oct 28 00:54:04 2023 ; 12 min 23 s 683.13 ms remaining ; 10 h 19 min 44 s 155.35 ms total)
Sat Oct 28 00:53:50 2023: Iterated 100% of D-proof candidates. [692467431 of 692467431] (ETC: Sat Oct 28 00:53:50 2023 ; 0.00 ms remaining ; 10 h 19 min 29 s 812.76 ms total)
37170528.55 ms (10 h 19 min 30 s 528.55 ms) taken to collect 62716073 D-proofs of length 87. [iterated 692467431 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 }, { 87, 692467431 } }
573288.66 ms (9 min 33 s 288.66 ms) taken to filter and order new representative proofs.
Found 62716073 representative, 159168941 redundant, and 470582417 invalid condensed detachment proof strings.
lengths up to 87 ; 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), (87,62716073)} ; 62716073 new representative proofs (159168941 redundant, 470582417 invalid)
Sat Oct 28 01:05:02 2023: Starting to write 62716073 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt.
79997.29 ms (1 min 19 s 997.29 ms) taken to print and save 25607335143 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt.
Sat Oct 28 01:07:34 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 87, unfiltered]
Sat Oct 28 01:09:06 2023: Process terminated. [pid: 93532, tid:22976569104256]