( 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: 103.4275 h CPU utilization: 6619.36 core-h ) Sun Nov 19 14:35:08 2023: Process started. [pid: 30862, tid:22849731037056] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(95, 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(95, false, true). Sun Nov 19 14:35:09 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 95, unfiltered] 0.03 ms taken to load initial representatives. 5.46 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22849670788864] 7.70 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22849668687616] 18.46 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22849666586368] 20.24 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22849664485120] 14.97 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22849662383872] 17.75 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22849660282624] 21.36 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22849658181376] 3.46 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22849656080128] 7.18 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22849653978880] 13.86 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22849651877632] 23.29 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22849649776384] 17.46 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22849647675136] 18.48 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22849645573888] 26.11 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22849643472640] 30.33 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22849641371392] 25.71 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22849639270144] 20.56 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22849637168896] 20.52 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22849635067648] 51.71 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22849632966400] 35.84 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22849630865152] 98.13 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22848689141504] 34.66 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22848687040256] 333.80 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22848684939008] 159.23 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22848682837760] 683.25 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22848680736512] 86.62 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22848678635264] 846.30 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22848676534016] 823.91 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22848674432768] 1155.36 ms (1 s 155.35 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22848672331520] 2573.88 ms (2 s 573.88 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22848670230272] 4978.23 ms (4 s 978.23 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22848668129024] 7285.16 ms (7 s 285.16 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22848666027776] 3306.24 ms (3 s 306.24 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22848663926528] 3197.45 ms (3 s 197.45 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22848661825280] 3326.21 ms (3 s 326.21 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22848659724032] 4652.49 ms (4 s 652.49 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22848657622784] 6135.75 ms (6 s 135.75 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22848655521536] 6589.53 ms (6 s 589.53 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22848653420288] 7276.82 ms (7 s 276.82 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22848651319040] 7829.00 ms (7 s 829.00 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22848649217792] 7926.01 ms (7 s 926.01 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. 81573.00 ms (1 min 21 s 573.00 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22848649217792] 128762.81 ms (2 min 8 s 762.81 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22848651319040] 165377.58 ms (2 min 45 s 377.58 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:22848653420288] 212120.91 ms (3 min 32 s 120.91 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:22848655521536] 270146.02 ms (4 min 30 s 146.02 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:22848657622784] 321331.78 ms (5 min 21 s 331.78 ms) taken to read 251856137 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. [tid:22848659724032] 321348.37 ms (5 min 21 s 348.37 ms) additional read duration. Loaded 6 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 89 : 101227436 91 : 157874085 93 : 251856137 655010167 representatives in total. Sun Nov 19 14:41:27 2023: Inserted ≈ 5% of D-proof conclusions. [ 32750508 of 655010167] (ETC: Sun Nov 19 14:57:09 2023 ; 15 min 41 s 223.09 ms remaining ; 16 min 30 s 761.15 ms total) Sun Nov 19 14:42:28 2023: Inserted ≈10% of D-proof conclusions. [ 65501016 of 655010167] (ETC: Sun Nov 19 14:58:57 2023 ; 16 min 28 s 990.25 ms remaining ; 18 min 18 s 878.05 ms total) Sun Nov 19 14:43:34 2023: Inserted ≈15% of D-proof conclusions. [ 98251525 of 655010167] (ETC: Sun Nov 19 15:00:12 2023 ; 16 min 38 s 360.02 ms remaining ; 19 min 34 s 541.20 ms total) Sun Nov 19 14:44:43 2023: Inserted ≈20% of D-proof conclusions. [131002033 of 655010167] (ETC: Sun Nov 19 15:01:05 2023 ; 16 min 21 s 526.74 ms remaining ; 20 min 26 s 908.42 ms total) Sun Nov 19 14:46:03 2023: Inserted ≈25% of D-proof conclusions. [163752541 of 655010167] (ETC: Sun Nov 19 15:02:17 2023 ; 16 min 13 s 975.28 ms remaining ; 21 min 38 s 633.70 ms total) Sun Nov 19 14:47:28 2023: Inserted ≈30% of D-proof conclusions. [196503050 of 655010167] (ETC: Sun Nov 19 15:03:26 2023 ; 15 min 57 s 571.89 ms remaining ; 22 min 47 s 959.85 ms total) Sun Nov 19 14:48:52 2023: Inserted ≈35% of D-proof conclusions. [229253558 of 655010167] (ETC: Sun Nov 19 15:04:08 2023 ; 15 min 16 s 725.44 ms remaining ; 23 min 30 s 346.83 ms total) Sun Nov 19 14:50:02 2023: Inserted ≈40% of D-proof conclusions. [262004066 of 655010167] (ETC: Sun Nov 19 15:04:08 2023 ; 14 min 5 s 818.61 ms remaining ; 23 min 29 s 697.68 ms total) Sun Nov 19 14:51:20 2023: Inserted ≈45% of D-proof conclusions. [294754575 of 655010167] (ETC: Sun Nov 19 15:04:25 2023 ; 13 min 4 s 869.90 ms remaining ; 23 min 47 s 36.17 ms total) Sun Nov 19 14:52:50 2023: Inserted ≈50% of D-proof conclusions. [327505083 of 655010167] (ETC: Sun Nov 19 15:05:03 2023 ; 12 min 12 s 422.21 ms remaining ; 24 min 24 s 844.41 ms total) Sun Nov 19 14:54:25 2023: Inserted ≈55% of D-proof conclusions. [360255591 of 655010167] (ETC: Sun Nov 19 15:05:42 2023 ; 11 min 16 s 748.56 ms remaining ; 25 min 3 s 885.68 ms total) Sun Nov 19 14:56:03 2023: Inserted ≈60% of D-proof conclusions. [393006100 of 655010167] (ETC: Sun Nov 19 15:06:19 2023 ; 10 min 16 s 434.46 ms remaining ; 25 min 41 s 86.16 ms total) Sun Nov 19 14:57:30 2023: Inserted ≈65% of D-proof conclusions. [425756608 of 655010167] (ETC: Sun Nov 19 15:06:35 2023 ; 9 min 5 s 48.29 ms remaining ; 25 min 57 s 280.81 ms total) Sun Nov 19 14:58:43 2023: Inserted ≈70% of D-proof conclusions. [458507116 of 655010167] (ETC: Sun Nov 19 15:06:28 2023 ; 7 min 44 s 983.50 ms remaining ; 25 min 49 s 944.99 ms total) Sun Nov 19 15:00:04 2023: Inserted ≈75% of D-proof conclusions. [491257625 of 655010167] (ETC: Sun Nov 19 15:06:32 2023 ; 6 min 28 s 613.45 ms remaining ; 25 min 54 s 453.80 ms total) Sun Nov 19 15:01:24 2023: Inserted ≈80% of D-proof conclusions. [524008133 of 655010167] (ETC: Sun Nov 19 15:06:35 2023 ; 5 min 11 s 441.75 ms remaining ; 25 min 57 s 208.72 ms total) Sun Nov 19 15:02:39 2023: Inserted ≈85% of D-proof conclusions. [556758641 of 655010167] (ETC: Sun Nov 19 15:06:33 2023 ; 3 min 53 s 187.81 ms remaining ; 25 min 54 s 585.38 ms total) Sun Nov 19 15:03:42 2023: Inserted ≈90% of D-proof conclusions. [589509150 of 655010167] (ETC: Sun Nov 19 15:06:15 2023 ; 2 min 33 s 753.81 ms remaining ; 25 min 37 s 538.09 ms total) Sun Nov 19 15:04:42 2023: Inserted ≈95% of D-proof conclusions. [622259658 of 655010167] (ETC: Sun Nov 19 15:05:58 2023 ; 1 min 15 s 981.51 ms remaining ; 25 min 19 s 630.28 ms total) Sun Nov 19 15:05:35 2023: Inserted 100% of D-proof conclusions. [655010167 of 655010167] (ETC: Sun Nov 19 15:05:35 2023 ; 0.00 ms remaining ; 24 min 56 s 905.38 ms total) 1496906.70 ms (24 min 56 s 906.70 ms) total insertion duration. Known iteration count loaded from 95:4844444054. Sun Nov 19 15:05:35 2023: Starting to generate D-proof representatives of length 95. Sun Nov 19 18:37:33 2023: Iterated ≈ 2% of D-proof candidates. [ 96888881 of 4844444054] (ETC: Sun Nov 26 23:44:19 2023 ; 7 d 5 h 6 min 46 s 21.30 ms remaining ; 7 d 8 h 38 min 44 s 511.53 ms total) Sun Nov 19 21:10:23 2023: Iterated ≈ 4% of D-proof candidates. [ 193777762 of 4844444054] (ETC: Sat Nov 25 23:05:46 2023 ; 6 d 1 h 55 min 23 s 143.70 ms remaining ; 6 d 8 h 11 s 608.00 ms total) Mon Nov 20 00:11:21 2023: Iterated ≈ 6% of D-proof candidates. [ 290666643 of 4844444054] (ETC: Sat Nov 25 22:41:49 2023 ; 5 d 22 h 30 min 27 s 501.53 ms remaining ; 6 d 7 h 36 min 13 s 937.77 ms total) Mon Nov 20 02:50:13 2023: Iterated ≈ 8% of D-proof candidates. [ 387555524 of 4844444054] (ETC: Sat Nov 25 17:53:29 2023 ; 5 d 15 h 3 min 16 s 520.97 ms remaining ; 6 d 2 h 47 min 54 s 479.27 ms total) Mon Nov 20 05:08:17 2023: Iterated ≈10% of D-proof candidates. [ 484444405 of 4844444054] (ETC: Sat Nov 25 11:32:32 2023 ; 5 d 6 h 24 min 15 s 770.63 ms remaining ; 5 d 20 h 26 min 57 s 522.88 ms total) Mon Nov 20 08:22:03 2023: Iterated ≈12% of D-proof candidates. [ 581333286 of 4844444054] (ETC: Sat Nov 25 15:02:49 2023 ; 5 d 6 h 40 min 46 s 435.90 ms remaining ; 5 d 23 h 57 min 14 s 586.19 ms total) Mon Nov 20 11:03:46 2023: Iterated ≈14% of D-proof candidates. [ 678222167 of 4844444054] (ETC: Sat Nov 25 13:44:05 2023 ; 5 d 2 h 40 min 19 s 50.27 ms remaining ; 5 d 22 h 38 min 30 s 523.50 ms total) Mon Nov 20 13:35:41 2023: Iterated ≈16% of D-proof candidates. [ 775111048 of 4844444054] (ETC: Sat Nov 25 11:43:45 2023 ; 4 d 22 h 8 min 3 s 376.79 ms remaining ; 5 d 20 h 38 min 9 s 734.20 ms total) Mon Nov 20 16:15:33 2023: Iterated ≈18% of D-proof candidates. [ 871999929 of 4844444054] (ETC: Sat Nov 25 10:54:17 2023 ; 4 d 18 h 38 min 43 s 946.04 ms remaining ; 5 d 19 h 48 min 41 s 885.32 ms total) Mon Nov 20 19:00:28 2023: Iterated ≈20% of D-proof candidates. [ 968888810 of 4844444054] (ETC: Sat Nov 25 10:40:03 2023 ; 4 d 15 h 39 min 34 s 425.58 ms remaining ; 5 d 19 h 34 min 28 s 31.87 ms total) Mon Nov 20 21:53:43 2023: Iterated ≈22% of D-proof candidates. [1065777691 of 4844444054] (ETC: Sat Nov 25 11:06:13 2023 ; 4 d 13 h 12 min 29 s 613.98 ms remaining ; 5 d 20 h 37 s 966.52 ms total) Tue Nov 21 00:15:53 2023: Iterated ≈24% of D-proof candidates. [1162666572 of 4844444054] (ETC: Sat Nov 25 09:18:32 2023 ; 4 d 9 h 2 min 38 s 647.98 ms remaining ; 5 d 18 h 12 min 57 s 168.27 ms total) Tue Nov 21 02:34:59 2023: Iterated ≈26% of D-proof candidates. [1259555454 of 4844444054] (ETC: Sat Nov 25 07:35:35 2023 ; 4 d 5 h 35 s 747.42 ms remaining ; 5 d 16 h 29 min 59 s 658.67 ms total) Tue Nov 21 05:12:23 2023: Iterated ≈28% of D-proof candidates. [1356444335 of 4844444054] (ETC: Sat Nov 25 07:12:43 2023 ; 4 d 2 h 20 s 399.83 ms remaining ; 5 d 16 h 7 min 8 s 333.08 ms total) Tue Nov 21 07:50:54 2023: Iterated ≈30% of D-proof candidates. [1453333216 of 4844444054] (ETC: Sat Nov 25 06:56:40 2023 ; 3 d 23 h 5 min 45 s 393.86 ms remaining ; 5 d 15 h 51 min 4 s 848.34 ms total) Tue Nov 21 10:05:58 2023: Iterated ≈32% of D-proof candidates. [1550222097 of 4844444054] (ETC: Sat Nov 25 05:29:16 2023 ; 3 d 19 h 23 min 18 s 502.14 ms remaining ; 5 d 14 h 23 min 41 s 326.64 ms total) Tue Nov 21 12:10:02 2023: Iterated ≈34% of D-proof candidates. [1647110978 of 4844444054] (ETC: Sat Nov 25 03:39:50 2023 ; 3 d 15 h 29 min 48 s 463.90 ms remaining ; 5 d 12 h 34 min 15 s 248.28 ms total) Tue Nov 21 14:08:49 2023: Iterated ≈36% of D-proof candidates. [1743999859 of 4844444054] (ETC: Sat Nov 25 01:47:53 2023 ; 3 d 11 h 39 min 4 s 391.93 ms remaining ; 5 d 10 h 42 min 18 s 112.33 ms total) Tue Nov 21 16:23:08 2023: Iterated ≈38% of D-proof candidates. [1840888740 of 4844444054] (ETC: Sat Nov 25 00:48:37 2023 ; 3 d 8 h 25 min 29 s 94.99 ms remaining ; 5 d 9 h 43 min 2 s 411.19 ms total) Tue Nov 21 18:30:05 2023: Iterated ≈40% of D-proof candidates. [1937777621 of 4844444054] (ETC: Fri Nov 24 23:36:50 2023 ; 3 d 5 h 6 min 44 s 807.11 ms remaining ; 5 d 8 h 31 min 14 s 678.42 ms total) Tue Nov 21 20:14:14 2023: Iterated ≈42% of D-proof candidates. [2034666502 of 4844444054] (ETC: Fri Nov 24 21:37:36 2023 ; 3 d 1 h 23 min 22 s 32.91 ms remaining ; 5 d 6 h 32 min 746.28 ms total) Tue Nov 21 21:58:45 2023: Iterated ≈44% of D-proof candidates. [2131555383 of 4844444054] (ETC: Fri Nov 24 19:50:04 2023 ; 2 d 21 h 51 min 18 s 461.02 ms remaining ; 5 d 4 h 44 min 28 s 680.27 ms total) Tue Nov 21 23:59:35 2023: Iterated ≈46% of D-proof candidates. [2228444264 of 4844444054] (ETC: Fri Nov 24 18:47:18 2023 ; 2 d 18 h 47 min 43 s 909.31 ms remaining ; 5 d 3 h 41 min 43 s 535.62 ms total) Wed Nov 22 02:07:48 2023: Iterated ≈48% of D-proof candidates. [2325333145 of 4844444054] (ETC: Fri Nov 24 18:05:13 2023 ; 2 d 15 h 57 min 24 s 422.86 ms remaining ; 5 d 2 h 59 min 37 s 736.11 ms total) Wed Nov 22 04:01:30 2023: Iterated ≈50% of D-proof candidates. [2422222027 of 4844444054] (ETC: Fri Nov 24 16:57:25 2023 ; 2 d 12 h 55 min 55 s 13.29 ms remaining ; 5 d 1 h 51 min 50 s 26.59 ms total) Wed Nov 22 05:43:02 2023: Iterated ≈52% of D-proof candidates. [2519110908 of 4844444054] (ETC: Fri Nov 24 15:31:26 2023 ; 2 d 9 h 48 min 24 s 692.44 ms remaining ; 5 d 25 min 51 s 442.58 ms total) Wed Nov 22 07:23:32 2023: Iterated ≈54% of D-proof candidates. [2615999789 of 4844444054] (ETC: Fri Nov 24 14:09:56 2023 ; 2 d 6 h 46 min 24 s 10.82 ms remaining ; 4 d 23 h 4 min 20 s 893.06 ms total) Wed Nov 22 09:06:34 2023: Iterated ≈56% of D-proof candidates. [2712888670 of 4844444054] (ETC: Fri Nov 24 12:58:47 2023 ; 2 d 3 h 52 min 12 s 445.74 ms remaining ; 4 d 21 h 53 min 11 s 922.08 ms total) Wed Nov 22 10:47:12 2023: Iterated ≈58% of D-proof candidates. [2809777551 of 4844444054] (ETC: Fri Nov 24 11:48:22 2023 ; 2 d 1 h 1 min 10 s 411.84 ms remaining ; 4 d 20 h 42 min 47 s 647.17 ms total) Wed Nov 22 12:24:21 2023: Iterated ≈60% of D-proof candidates. [2906666432 of 4844444054] (ETC: Fri Nov 24 10:36:52 2023 ; 1 d 22 h 12 min 30 s 996.29 ms remaining ; 4 d 19 h 31 min 17 s 490.64 ms total) Wed Nov 22 13:58:25 2023: Iterated ≈62% of D-proof candidates. [3003555313 of 4844444054] (ETC: Fri Nov 24 09:25:00 2023 ; 1 d 19 h 26 min 34 s 593.02 ms remaining ; 4 d 18 h 19 min 24 s 718.38 ms total) Wed Nov 22 15:30:53 2023: Iterated ≈64% of D-proof candidates. [3100444194 of 4844444054] (ETC: Fri Nov 24 08:15:07 2023 ; 1 d 16 h 44 min 13 s 967.00 ms remaining ; 4 d 17 h 9 min 32 s 130.41 ms total) Wed Nov 22 17:02:09 2023: Iterated ≈66% of D-proof candidates. [3197333075 of 4844444054] (ETC: Fri Nov 24 07:07:39 2023 ; 1 d 14 h 5 min 30 s 180.35 ms remaining ; 4 d 16 h 2 min 4 s 59.71 ms total) Wed Nov 22 18:33:15 2023: Iterated ≈68% of D-proof candidates. [3294221956 of 4844444054] (ETC: Fri Nov 24 06:03:55 2023 ; 1 d 11 h 30 min 40 s 3.03 ms remaining ; 4 d 14 h 58 min 20 s 9.28 ms total) Wed Nov 22 20:04:20 2023: Iterated ≈70% of D-proof candidates. [3391110837 of 4844444054] (ETC: Fri Nov 24 05:03:48 2023 ; 1 d 8 h 59 min 28 s 78.06 ms remaining ; 4 d 13 h 58 min 13 s 593.33 ms total) Wed Nov 22 21:35:14 2023: Iterated ≈72% of D-proof candidates. [3487999718 of 4844444054] (ETC: Fri Nov 24 04:06:46 2023 ; 1 d 6 h 31 min 31 s 944.40 ms remaining ; 4 d 13 h 1 min 11 s 229.75 ms total) Wed Nov 22 23:06:40 2023: Iterated ≈74% of D-proof candidates. [3584888599 of 4844444054] (ETC: Fri Nov 24 03:13:32 2023 ; 1 d 4 h 6 min 51 s 962.61 ms remaining ; 4 d 12 h 7 min 56 s 778.98 ms total) Thu Nov 23 00:37:54 2023: Iterated ≈76% of D-proof candidates. [3681777481 of 4844444054] (ETC: Fri Nov 24 02:22:51 2023 ; 1 d 1 h 44 min 56 s 591.78 ms remaining ; 4 d 11 h 17 min 15 s 799.06 ms total) Thu Nov 23 02:09:52 2023: Iterated ≈78% of D-proof candidates. [3778666362 of 4844444054] (ETC: Fri Nov 24 01:35:41 2023 ; 23 h 25 min 49 s 447.91 ms remaining ; 4 d 10 h 30 min 6 s 581.35 ms total) Thu Nov 23 03:41:54 2023: Iterated ≈80% of D-proof candidates. [3875555243 of 4844444054] (ETC: Fri Nov 24 00:50:59 2023 ; 21 h 9 min 4 s 887.59 ms remaining ; 4 d 9 h 45 min 24 s 437.86 ms total) Thu Nov 23 05:14:11 2023: Iterated ≈82% of D-proof candidates. [3972444124 of 4844444054] (ETC: Fri Nov 24 00:08:45 2023 ; 18 h 54 min 34 s 300.20 ms remaining ; 4 d 9 h 3 min 10 s 556.53 ms total) Thu Nov 23 06:46:45 2023: Iterated ≈84% of D-proof candidates. [4069333005 of 4844444054] (ETC: Thu Nov 23 23:28:53 2023 ; 16 h 42 min 7 s 699.92 ms remaining ; 4 d 8 h 23 min 18 s 124.30 ms total) Thu Nov 23 08:19:09 2023: Iterated ≈86% of D-proof candidates. [4166221886 of 4844444054] (ETC: Thu Nov 23 22:50:40 2023 ; 14 h 31 min 30 s 690.33 ms remaining ; 4 d 7 h 45 min 4 s 930.65 ms total) Thu Nov 23 09:51:47 2023: Iterated ≈88% of D-proof candidates. [4263110767 of 4844444054] (ETC: Thu Nov 23 22:14:27 2023 ; 12 h 22 min 39 s 866.00 ms remaining ; 4 d 7 h 8 min 52 s 216.30 ms total) Thu Nov 23 11:24:26 2023: Iterated ≈90% of D-proof candidates. [4359999648 of 4844444054] (ETC: Thu Nov 23 21:39:49 2023 ; 10 h 15 min 25 s 371.87 ms remaining ; 4 d 6 h 34 min 13 s 718.26 ms total) Thu Nov 23 12:56:28 2023: Iterated ≈92% of D-proof candidates. [4456888529 of 4844444054] (ETC: Thu Nov 23 21:06:06 2023 ; 8 h 9 min 38 s 521.57 ms remaining ; 4 d 6 h 31 s 518.94 ms total) Thu Nov 23 14:28:26 2023: Iterated ≈94% of D-proof candidates. [4553777410 of 4844444054] (ETC: Thu Nov 23 20:33:43 2023 ; 6 h 5 min 17 s 314.93 ms remaining ; 4 d 5 h 28 min 8 s 581.27 ms total) Thu Nov 23 16:00:19 2023: Iterated ≈96% of D-proof candidates. [4650666291 of 4844444054] (ETC: Thu Nov 23 20:02:35 2023 ; 4 h 2 min 16 s 819.16 ms remaining ; 4 d 4 h 57 min 477.43 ms total) Thu Nov 23 17:32:09 2023: Iterated ≈98% of D-proof candidates. [4747555172 of 4844444054] (ETC: Thu Nov 23 19:32:42 2023 ; 2 h 32 s 542.28 ms remaining ; 4 d 4 h 27 min 7 s 110.65 ms total) Thu Nov 23 19:03:23 2023: Iterated 100% of D-proof candidates. [4844444054 of 4844444054] (ETC: Thu Nov 23 19:03:23 2023 ; 0.00 ms remaining ; 4 d 3 h 57 min 47 s 813.48 ms total) 359873135.17 ms (4 d 3 h 57 min 53 s 135.17 ms) taken to collect 406329619 D-proofs of length 95. [iterated 4844444054 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 }, { 89, 1120159490 }, { 91, 1817170079 }, { 93, 2979484674 }, { 95, 4844444054 } } 6190040.95 ms (1 h 43 min 10 s 40.95 ms) taken to filter and order new representative proofs. Found 406329619 representative, 1183738603 redundant, and 3254375832 invalid condensed detachment proof strings. lengths up to 95 ; 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), (89,101227436), (91,157874085), (93,251856137), (95,406329619)} ; 406329619 new representative proofs (1183738603 redundant, 3254375832 invalid) Thu Nov 23 21:13:06 2023: Starting to write 406329619 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs95-unfiltered83+.txt. 879949.16 ms (14 min 39 s 949.16 ms) taken to print and save 193064036043 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs95-unfiltered83+.txt. Thu Nov 23 21:38:05 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 95, unfiltered] Thu Nov 23 22:00:47 2023: Process terminated. [pid: 30862, tid:22849731037056]