( 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: 4.9075 h CPU utilization: 235.56 core-h ) Thu Oct 26 06:30:06 2023: Process started. [pid: 178162, tid:23084471003008] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(83, 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(83, false, true). Thu Oct 26 06:30:06 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 83, unfiltered] 0.01 ms taken to load initial representatives. 20.00 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23084410754816] 11.54 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23084408653568] 16.58 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23084406552320] 19.60 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23084404451072] 17.18 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23084402349824] 16.45 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23084400248576] 14.91 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23084398147328] 11.94 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23084396046080] 22.77 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23084393944832] 33.77 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23084391843584] 61.54 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23084389742336] 12.53 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23084387641088] 32.39 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23084385539840] 20.84 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23084383438592] 23.64 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23084381337344] 12.76 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23084379236096] 25.53 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23083234621184] 27.87 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23083232519936] 71.06 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23083100403456] 52.93 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23083230418688] 46.34 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23083228317440] 55.92 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23083226216192] 75.19 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23083224114944] 66.78 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23083222013696] 128.38 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23083219912448] 173.72 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23083217811200] 321.66 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23083215709952] 530.69 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23083213608704] 1062.68 ms (1 s 62.68 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23083211507456] 2129.48 ms (2 s 129.48 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23083209406208] 4554.42 ms (4 s 554.42 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23083207304960] 9510.07 ms (9 s 510.07 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23083205203712] 755.72 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23083203102464] 1245.74 ms (1 s 245.74 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23083201001216] 1698.48 ms (1 s 698.48 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23083198899968] 2188.65 ms (2 s 188.65 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23083196798720] 2898.70 ms (2 s 898.70 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23083194697472] 3527.49 ms (3 s 527.49 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23083192596224] 4415.24 ms (4 s 415.24 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23083190494976] 5563.57 ms (5 s 563.57 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23083188393728] 9529.20 ms (9 s 529.20 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. Thu Oct 26 06:30:16 2023: Inserted ≈ 5% of D-proof conclusions. [ 993985 of 19879711] (ETC: Thu Oct 26 06:30:30 2023 ; 13 s 986.46 ms remaining ; 14 s 722.59 ms total) Thu Oct 26 06:30:17 2023: Inserted ≈10% of D-proof conclusions. [ 1987971 of 19879711] (ETC: Thu Oct 26 06:30:31 2023 ; 14 s 100.08 ms remaining ; 15 s 666.76 ms total) Thu Oct 26 06:30:18 2023: Inserted ≈15% of D-proof conclusions. [ 2981956 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 13 s 599.51 ms remaining ; 15 s 999.42 ms total) Thu Oct 26 06:30:19 2023: Inserted ≈20% of D-proof conclusions. [ 3975942 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 13 s 101.08 ms remaining ; 16 s 376.35 ms total) Thu Oct 26 06:30:20 2023: Inserted ≈25% of D-proof conclusions. [ 4969927 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 12 s 548.50 ms remaining ; 16 s 731.33 ms total) Thu Oct 26 06:30:21 2023: Inserted ≈30% of D-proof conclusions. [ 5963913 of 19879711] (ETC: Thu Oct 26 06:30:33 2023 ; 11 s 859.00 ms remaining ; 16 s 941.43 ms total) Thu Oct 26 06:30:22 2023: Inserted ≈35% of D-proof conclusions. [ 6957898 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 10 s 900.98 ms remaining ; 16 s 770.74 ms total) Thu Oct 26 06:30:22 2023: Inserted ≈40% of D-proof conclusions. [ 7951884 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 9 s 981.75 ms remaining ; 16 s 636.25 ms total) Thu Oct 26 06:30:23 2023: Inserted ≈45% of D-proof conclusions. [ 8945869 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 9 s 208.10 ms remaining ; 16 s 742.01 ms total) Thu Oct 26 06:30:24 2023: Inserted ≈50% of D-proof conclusions. [ 9939855 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 8 s 255.71 ms remaining ; 16 s 511.41 ms total) Thu Oct 26 06:30:25 2023: Inserted ≈55% of D-proof conclusions. [10933841 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 7 s 374.62 ms remaining ; 16 s 388.04 ms total) Thu Oct 26 06:30:26 2023: Inserted ≈60% of D-proof conclusions. [11927826 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 6 s 561.40 ms remaining ; 16 s 403.51 ms total) Thu Oct 26 06:30:27 2023: Inserted ≈65% of D-proof conclusions. [12921812 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 5 s 813.30 ms remaining ; 16 s 609.44 ms total) Thu Oct 26 06:30:27 2023: Inserted ≈70% of D-proof conclusions. [13915797 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 4 s 975.94 ms remaining ; 16 s 586.47 ms total) Thu Oct 26 06:30:28 2023: Inserted ≈75% of D-proof conclusions. [14909783 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 4 s 134.77 ms remaining ; 16 s 539.09 ms total) Thu Oct 26 06:30:29 2023: Inserted ≈80% of D-proof conclusions. [15903768 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 3 s 314.01 ms remaining ; 16 s 570.05 ms total) Thu Oct 26 06:30:30 2023: Inserted ≈85% of D-proof conclusions. [16897754 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 2 s 506.07 ms remaining ; 16 s 707.13 ms total) Thu Oct 26 06:30:31 2023: Inserted ≈90% of D-proof conclusions. [17891739 of 19879711] (ETC: Thu Oct 26 06:30:32 2023 ; 1 s 675.29 ms remaining ; 16 s 752.94 ms total) Thu Oct 26 06:30:32 2023: Inserted ≈95% of D-proof conclusions. [18885725 of 19879711] (ETC: Thu Oct 26 06:30:33 2023 ; 842.16 ms remaining ; 16 s 843.15 ms total) Thu Oct 26 06:30:33 2023: Inserted 100% of D-proof conclusions. [19879711 of 19879711] (ETC: Thu Oct 26 06:30:33 2023 ; 0.00 ms remaining ; 17 s 113.42 ms total) 17113.69 ms (17 s 113.69 ms) total insertion duration. Estimated iteration count set to 268384284, based on entry 81:176882404 and last known pair (79:116576814, 81:176882404) with 176882404/116576814 ≈ 1.5173 and 176882404 * (176882404/116576814)^1 ≈ 268384284.76. Thu Oct 26 06:30:33 2023: Starting to generate D-proof representatives of length 83. Thu Oct 26 06:37:45 2023: Iterated ≈ 2% of D-proof candidates. [ 5367685 of approximately 268384284] (ETC: Thu Oct 26 12:30:41 2023 ; 5 h 52 min 56 s 209.36 ms remaining ; 6 h 8 s 376.84 ms total) Thu Oct 26 06:43:24 2023: Iterated ≈ 4% of D-proof candidates. [ 10735371 of approximately 268384284] (ETC: Thu Oct 26 11:51:59 2023 ; 5 h 8 min 35 s 132.42 ms remaining ; 5 h 21 min 26 s 596.25 ms total) Thu Oct 26 06:49:14 2023: Iterated ≈ 6% of D-proof candidates. [ 16103057 of approximately 268384284] (ETC: Thu Oct 26 11:42:03 2023 ; 4 h 52 min 48 s 639.42 ms remaining ; 5 h 11 min 30 s 41.93 ms total) Thu Oct 26 06:54:49 2023: Iterated ≈ 8% of D-proof candidates. [ 21470742 of approximately 268384284] (ETC: Thu Oct 26 11:33:56 2023 ; 4 h 39 min 6 s 627.20 ms remaining ; 5 h 3 min 22 s 855.60 ms total) Thu Oct 26 07:00:35 2023: Iterated ≈ 10% of D-proof candidates. [ 26838428 of approximately 268384284] (ETC: Thu Oct 26 11:30:52 2023 ; 4 h 30 min 16 s 936.00 ms remaining ; 5 h 18 s 817.75 ms total) Thu Oct 26 07:06:13 2023: Iterated ≈ 12% of D-proof candidates. [ 32206114 of approximately 268384284] (ETC: Thu Oct 26 11:27:49 2023 ; 4 h 21 min 35 s 955.53 ms remaining ; 4 h 57 min 16 s 313.09 ms total) Thu Oct 26 07:11:48 2023: Iterated ≈ 14% of D-proof candidates. [ 37573799 of approximately 268384284] (ETC: Thu Oct 26 11:25:10 2023 ; 4 h 13 min 22 s 325.16 ms remaining ; 4 h 54 min 37 s 122.22 ms total) Thu Oct 26 07:17:24 2023: Iterated ≈ 16% of D-proof candidates. [ 42941485 of approximately 268384284] (ETC: Thu Oct 26 11:23:22 2023 ; 4 h 5 min 58 s 474.01 ms remaining ; 4 h 52 min 49 s 611.88 ms total) Thu Oct 26 07:22:45 2023: Iterated ≈ 18% of D-proof candidates. [ 48309171 of approximately 268384284] (ETC: Thu Oct 26 11:20:32 2023 ; 3 h 57 min 47 s 234.76 ms remaining ; 4 h 49 min 59 s 66.77 ms total) Thu Oct 26 07:28:37 2023: Iterated ≈ 20% of D-proof candidates. [ 53676856 of approximately 268384284] (ETC: Thu Oct 26 11:20:53 2023 ; 3 h 52 min 16 s 365.60 ms remaining ; 4 h 50 min 20 s 456.93 ms total) Thu Oct 26 07:34:15 2023: Iterated ≈ 22% of D-proof candidates. [ 59044542 of approximately 268384284] (ETC: Thu Oct 26 11:20:08 2023 ; 3 h 45 min 52 s 685.84 ms remaining ; 4 h 49 min 35 s 238.22 ms total) Thu Oct 26 07:39:51 2023: Iterated ≈ 24% of D-proof candidates. [ 64412228 of approximately 268384284] (ETC: Thu Oct 26 11:19:17 2023 ; 3 h 39 min 26 s 152.57 ms remaining ; 4 h 48 min 43 s 884.95 ms total) Thu Oct 26 07:45:41 2023: Iterated ≈ 26% of D-proof candidates. [ 69779913 of approximately 268384284] (ETC: Thu Oct 26 11:19:31 2023 ; 3 h 33 min 50 s 368.55 ms remaining ; 4 h 48 min 58 s 335.80 ms total) Thu Oct 26 07:51:20 2023: Iterated ≈ 28% of D-proof candidates. [ 75147599 of approximately 268384284] (ETC: Thu Oct 26 11:19:04 2023 ; 3 h 27 min 44 s 227.61 ms remaining ; 4 h 48 min 31 s 427.19 ms total) Thu Oct 26 07:57:11 2023: Iterated ≈ 30% of D-proof candidates. [ 80515285 of approximately 268384284] (ETC: Thu Oct 26 11:19:21 2023 ; 3 h 22 min 9 s 634.24 ms remaining ; 4 h 48 min 48 s 48.90 ms total) Thu Oct 26 08:02:58 2023: Iterated ≈ 32% of D-proof candidates. [ 85882970 of approximately 268384284] (ETC: Thu Oct 26 11:19:20 2023 ; 3 h 16 min 22 s 717.32 ms remaining ; 4 h 48 min 47 s 525.39 ms total) Thu Oct 26 08:08:41 2023: Iterated ≈ 34% of D-proof candidates. [ 91250656 of approximately 268384284] (ETC: Thu Oct 26 11:19:12 2023 ; 3 h 10 min 30 s 813.05 ms remaining ; 4 h 48 min 39 s 413.66 ms total) Thu Oct 26 08:14:28 2023: Iterated ≈ 36% of D-proof candidates. [ 96618342 of approximately 268384284] (ETC: Thu Oct 26 11:19:13 2023 ; 3 h 4 min 44 s 957.66 ms remaining ; 4 h 48 min 40 s 246.31 ms total) Thu Oct 26 08:20:17 2023: Iterated ≈ 38% of D-proof candidates. [101986027 of approximately 268384284] (ETC: Thu Oct 26 11:19:19 2023 ; 2 h 59 min 2 s 55.47 ms remaining ; 4 h 48 min 45 s 895.83 ms total) Thu Oct 26 08:26:04 2023: Iterated ≈ 40% of D-proof candidates. [107353713 of approximately 268384284] (ETC: Thu Oct 26 11:19:21 2023 ; 2 h 53 min 16 s 962.40 ms remaining ; 4 h 48 min 48 s 270.60 ms total) Thu Oct 26 08:31:53 2023: Iterated ≈ 42% of D-proof candidates. [112721399 of approximately 268384284] (ETC: Thu Oct 26 11:19:26 2023 ; 2 h 47 min 32 s 981.37 ms remaining ; 4 h 48 min 52 s 726.47 ms total) Thu Oct 26 08:37:41 2023: Iterated ≈ 44% of D-proof candidates. [118089084 of approximately 268384284] (ETC: Thu Oct 26 11:19:30 2023 ; 2 h 41 min 48 s 947.94 ms remaining ; 4 h 48 min 57 s 406.92 ms total) Thu Oct 26 08:43:31 2023: Iterated ≈ 46% of D-proof candidates. [123456770 of approximately 268384284] (ETC: Thu Oct 26 11:19:36 2023 ; 2 h 36 min 5 s 219.42 ms remaining ; 4 h 49 min 2 s 998.85 ms total) Thu Oct 26 08:49:13 2023: Iterated ≈ 48% of D-proof candidates. [128824456 of approximately 268384284] (ETC: Thu Oct 26 11:19:27 2023 ; 2 h 30 min 13 s 844.74 ms remaining ; 4 h 48 min 54 s 316.77 ms total) Thu Oct 26 08:54:53 2023: Iterated ≈ 50% of D-proof candidates. [134192142 of approximately 268384284] (ETC: Thu Oct 26 11:19:13 2023 ; 2 h 24 min 20 s 160.79 ms remaining ; 4 h 48 min 40 s 321.59 ms total) Thu Oct 26 09:00:37 2023: Iterated ≈ 52% of D-proof candidates. [139559827 of approximately 268384284] (ETC: Thu Oct 26 11:19:09 2023 ; 2 h 18 min 31 s 854.33 ms remaining ; 4 h 48 min 36 s 363.10 ms total) Thu Oct 26 09:06:21 2023: Iterated ≈ 54% of D-proof candidates. [144927513 of approximately 268384284] (ETC: Thu Oct 26 11:19:05 2023 ; 2 h 12 min 43 s 385.80 ms remaining ; 4 h 48 min 31 s 708.22 ms total) Thu Oct 26 09:11:58 2023: Iterated ≈ 56% of D-proof candidates. [150295199 of approximately 268384284] (ETC: Thu Oct 26 11:18:48 2023 ; 2 h 6 min 50 s 94.26 ms remaining ; 4 h 48 min 15 s 668.77 ms total) Thu Oct 26 09:17:39 2023: Iterated ≈ 58% of D-proof candidates. [155662884 of approximately 268384284] (ETC: Thu Oct 26 11:18:40 2023 ; 2 h 1 min 609.56 ms remaining ; 4 h 48 min 7 s 165.50 ms total) Thu Oct 26 09:23:22 2023: Iterated ≈ 60% of D-proof candidates. [161030570 of approximately 268384284] (ETC: Thu Oct 26 11:18:35 2023 ; 1 h 55 min 12 s 993.51 ms remaining ; 4 h 48 min 2 s 483.71 ms total) Thu Oct 26 09:29:03 2023: Iterated ≈ 62% of D-proof candidates. [166398256 of approximately 268384284] (ETC: Thu Oct 26 11:18:27 2023 ; 1 h 49 min 24 s 208.87 ms remaining ; 4 h 47 min 54 s 233.86 ms total) Thu Oct 26 09:34:48 2023: Iterated ≈ 64% of D-proof candidates. [171765941 of approximately 268384284] (ETC: Thu Oct 26 11:18:26 2023 ; 1 h 43 min 38 s 265.12 ms remaining ; 4 h 47 min 52 s 958.53 ms total) Thu Oct 26 09:40:27 2023: Iterated ≈ 66% of D-proof candidates. [177133627 of approximately 268384284] (ETC: Thu Oct 26 11:18:17 2023 ; 1 h 37 min 49 s 871.60 ms remaining ; 4 h 47 min 44 s 328.14 ms total) Thu Oct 26 09:46:10 2023: Iterated ≈ 68% of D-proof candidates. [182501313 of approximately 268384284] (ETC: Thu Oct 26 11:18:14 2023 ; 1 h 32 min 3 s 478.82 ms remaining ; 4 h 47 min 40 s 871.30 ms total) Thu Oct 26 09:52:00 2023: Iterated ≈ 70% of D-proof candidates. [187868998 of approximately 268384284] (ETC: Thu Oct 26 11:18:20 2023 ; 1 h 26 min 20 s 223.55 ms remaining ; 4 h 47 min 47 s 411.66 ms total) Thu Oct 26 09:57:39 2023: Iterated ≈ 72% of D-proof candidates. [193236684 of approximately 268384284] (ETC: Thu Oct 26 11:18:12 2023 ; 1 h 20 min 32 s 473.59 ms remaining ; 4 h 47 min 38 s 834.13 ms total) Thu Oct 26 10:03:24 2023: Iterated ≈ 74% of D-proof candidates. [198604370 of approximately 268384284] (ETC: Thu Oct 26 11:18:11 2023 ; 1 h 14 min 47 s 34.43 ms remaining ; 4 h 47 min 37 s 824.70 ms total) Thu Oct 26 10:09:15 2023: Iterated ≈ 76% of D-proof candidates. [203972055 of approximately 268384284] (ETC: Thu Oct 26 11:18:19 2023 ; 1 h 9 min 3 s 820.06 ms remaining ; 4 h 47 min 45 s 916.69 ms total) Thu Oct 26 10:15:06 2023: Iterated ≈ 78% of D-proof candidates. [209339741 of approximately 268384284] (ETC: Thu Oct 26 11:18:26 2023 ; 1 h 3 min 20 s 8.57 ms remaining ; 4 h 47 min 52 s 766.09 ms total) Thu Oct 26 10:20:56 2023: Iterated ≈ 80% of D-proof candidates. [214707427 of approximately 268384284] (ETC: Thu Oct 26 11:18:32 2023 ; 57 min 35 s 749.67 ms remaining ; 4 h 47 min 58 s 748.30 ms total) Thu Oct 26 10:26:42 2023: Iterated ≈ 82% of D-proof candidates. [220075112 of approximately 268384284] (ETC: Thu Oct 26 11:18:32 2023 ; 51 min 50 s 336.12 ms remaining ; 4 h 47 min 59 s 644.81 ms total) Thu Oct 26 10:32:35 2023: Iterated ≈ 84% of D-proof candidates. [225442798 of approximately 268384284] (ETC: Thu Oct 26 11:18:41 2023 ; 46 min 6 s 110.55 ms remaining ; 4 h 48 min 8 s 190.74 ms total) Thu Oct 26 10:38:26 2023: Iterated ≈ 86% of D-proof candidates. [230810484 of approximately 268384284] (ETC: Thu Oct 26 11:18:47 2023 ; 40 min 21 s 194.50 ms remaining ; 4 h 48 min 14 s 246.35 ms total) Thu Oct 26 10:44:16 2023: Iterated ≈ 88% of D-proof candidates. [236178169 of approximately 268384284] (ETC: Thu Oct 26 11:18:52 2023 ; 34 min 35 s 879.43 ms remaining ; 4 h 48 min 18 s 994.77 ms total) Thu Oct 26 10:50:04 2023: Iterated ≈ 90% of D-proof candidates. [241545855 of approximately 268384284] (ETC: Thu Oct 26 11:18:54 2023 ; 28 min 50 s 129.15 ms remaining ; 4 h 48 min 21 s 291.13 ms total) Thu Oct 26 10:55:48 2023: Iterated ≈ 92% of D-proof candidates. [246913541 of approximately 268384284] (ETC: Thu Oct 26 11:18:52 2023 ; 23 min 3 s 907.65 ms remaining ; 4 h 48 min 18 s 845.47 ms total) Thu Oct 26 11:01:33 2023: Iterated ≈ 94% of D-proof candidates. [252281226 of approximately 268384284] (ETC: Thu Oct 26 11:18:51 2023 ; 17 min 17 s 895.37 ms remaining ; 4 h 48 min 18 s 255.16 ms total) Thu Oct 26 11:07:21 2023: Iterated ≈ 96% of D-proof candidates. [257648912 of approximately 268384284] (ETC: Thu Oct 26 11:18:53 2023 ; 11 min 32 s 14.53 ms remaining ; 4 h 48 min 20 s 362.24 ms total) Thu Oct 26 11:13:00 2023: Iterated ≈ 98% of D-proof candidates. [263016598 of approximately 268384284] (ETC: Thu Oct 26 11:18:46 2023 ; 5 min 45 s 860.00 ms remaining ; 4 h 48 min 12 s 999.18 ms total) Thu Oct 26 11:18:44 2023: Iterated ≈100% of D-proof candidates. [268384284 of approximately 268384284] (ETC: Thu Oct 26 11:18:44 2023 ; 0.00 ms remaining ; 4 h 48 min 11 s 16.40 ms total) 17298847.03 ms (4 h 48 min 18 s 847.03 ms) taken to collect 22730041 D-proofs of length 83. [iterated 268514198 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 } } 147135.03 ms (2 min 27 s 135.03 ms) taken to filter and order new representative proofs. Found 22730041 representative, 66531648 redundant, and 179252509 invalid condensed detachment proof strings. lengths up to 83 ; 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)} ; 22730041 new representative proofs (66531648 redundant, 179252509 invalid) Thu Oct 26 11:22:57 2023: Starting to write 22730041 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. 35979.94 ms (35 s 979.94 ms) taken to print and save 8242569881 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. Thu Oct 26 11:23:57 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 83, unfiltered] Thu Oct 26 11:24:33 2023: Process terminated. [pid: 178162, tid:23084471003008]