( This log file was generated by executing 'pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp --iterate -u' (pmGenerator 1.2, master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'. The run was executed on a CLAIX-2018 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. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 40363276 c18m_low 48 COMPLETED 0:0 00:09:44 40363276.ba+ 48 COMPLETED 0:0 00:09:44 72518108K 40363276.ex+ 48 COMPLETED 0:0 00:09:44 84K By 72518108 KiB = (72518108 / 1024^2) GiB = 69.158657073974609375 GiB, it used approximately 69.16 gibibytes of memory. ) Thu Oct 26 20:19:13 2023: Process started. [pid: 162285, tid:22754652997504] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69] (1) CCC0.1CCCN2N3.2.4CC4.0C3.0 - CCCpqCCCNrNsrtCCtpCsp - ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0)) [Main] Calling countNextIterationAmount(false, true). Thu Oct 26 20:19:13 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 15.55 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22754592749312] 16.21 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22754590648064] 15.88 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22754588546816] 10.91 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22754586445568] 18.33 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22754584344320] 20.99 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22754582243072] 19.30 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22754580141824] 13.94 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22754578040576] 5.87 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22754575939328] 12.00 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22754573838080] 13.96 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22754571736832] 20.11 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22754569635584] 21.45 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22754567534336] 27.25 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22754565433088] 28.42 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22754563331840] 28.85 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22754561230592] 33.13 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22754559129344] 25.39 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22754557028096] 81.94 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22754554926848] 35.61 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22754552825600] 50.63 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22754550724352] 30.26 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22754548623104] 76.16 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22754546521856] 61.94 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22754544420608] 98.31 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22754542319360] 137.91 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22754540218112] 278.90 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22754538116864] 533.39 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22752723465984] 1026.22 ms (1 s 26.22 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22752721364736] 2012.54 ms (2 s 12.54 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22752719263488] 3930.27 ms (3 s 930.27 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22752717162240] 9951.58 ms (9 s 951.58 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22752715060992] 849.36 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22752712959744] 1297.54 ms (1 s 297.54 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22752710858496] 1712.08 ms (1 s 712.08 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22752708757248] 2359.65 ms (2 s 359.65 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22752706656000] 3029.67 ms (3 s 29.67 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22752704554752] 3832.62 ms (3 s 832.62 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22752702453504] 4817.03 ms (4 s 817.03 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22752700352256] 6014.21 ms (6 s 14.21 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22752698251008] 9976.28 ms (9 s 976.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. 17511.86 ms (17 s 511.86 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22752698251008] 32793.87 ms (32 s 793.87 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22752700352256] 32809.88 ms (32 s 809.88 ms) additional read duration. Loaded 2 more representative collections of sizes: 83 : 22730041 85 : 38726684 81336436 representatives in total. Thu Oct 26 20:19:58 2023: Inserted ≈ 5% of D-proof conclusions. [ 4066821 of 81336436] (ETC: Thu Oct 26 20:20:55 2023 ; 56 s 143.57 ms remaining ; 59 s 98.49 ms total) Thu Oct 26 20:20:02 2023: Inserted ≈10% of D-proof conclusions. [ 8133643 of 81336436] (ETC: Thu Oct 26 20:20:56 2023 ; 54 s 785.15 ms remaining ; 1 min 872.39 ms total) Thu Oct 26 20:20:05 2023: Inserted ≈15% of D-proof conclusions. [12200465 of 81336436] (ETC: Thu Oct 26 20:20:57 2023 ; 52 s 607.47 ms remaining ; 1 min 1 s 891.13 ms total) Thu Oct 26 20:20:08 2023: Inserted ≈20% of D-proof conclusions. [16267287 of 81336436] (ETC: Thu Oct 26 20:20:58 2023 ; 49 s 945.71 ms remaining ; 1 min 2 s 432.13 ms total) Thu Oct 26 20:20:11 2023: Inserted ≈25% of D-proof conclusions. [20334109 of 81336436] (ETC: Thu Oct 26 20:20:58 2023 ; 47 s 147.07 ms remaining ; 1 min 2 s 862.76 ms total) Thu Oct 26 20:20:14 2023: Inserted ≈30% of D-proof conclusions. [24400930 of 81336436] (ETC: Thu Oct 26 20:20:55 2023 ; 41 s 981.14 ms remaining ; 59 s 973.05 ms total) Thu Oct 26 20:20:16 2023: Inserted ≈35% of D-proof conclusions. [28467752 of 81336436] (ETC: Thu Oct 26 20:20:54 2023 ; 37 s 778.88 ms remaining ; 58 s 121.36 ms total) Thu Oct 26 20:20:18 2023: Inserted ≈40% of D-proof conclusions. [32534574 of 81336436] (ETC: Thu Oct 26 20:20:52 2023 ; 34 s 73.20 ms remaining ; 56 s 788.68 ms total) Thu Oct 26 20:20:21 2023: Inserted ≈45% of D-proof conclusions. [36601396 of 81336436] (ETC: Thu Oct 26 20:20:53 2023 ; 31 s 589.00 ms remaining ; 57 s 434.54 ms total) Thu Oct 26 20:20:25 2023: Inserted ≈50% of D-proof conclusions. [40668218 of 81336436] (ETC: Thu Oct 26 20:20:54 2023 ; 29 s 396.88 ms remaining ; 58 s 793.76 ms total) Thu Oct 26 20:20:28 2023: Inserted ≈55% of D-proof conclusions. [44735039 of 81336436] (ETC: Thu Oct 26 20:20:55 2023 ; 26 s 600.65 ms remaining ; 59 s 112.56 ms total) Thu Oct 26 20:20:30 2023: Inserted ≈60% of D-proof conclusions. [48801861 of 81336436] (ETC: Thu Oct 26 20:20:53 2023 ; 23 s 169.05 ms remaining ; 57 s 922.63 ms total) Thu Oct 26 20:20:33 2023: Inserted ≈65% of D-proof conclusions. [52868683 of 81336436] (ETC: Thu Oct 26 20:20:53 2023 ; 20 s 104.73 ms remaining ; 57 s 442.10 ms total) Thu Oct 26 20:20:36 2023: Inserted ≈70% of D-proof conclusions. [56935505 of 81336436] (ETC: Thu Oct 26 20:20:53 2023 ; 17 s 205.79 ms remaining ; 57 s 352.63 ms total) Thu Oct 26 20:20:38 2023: Inserted ≈75% of D-proof conclusions. [61002327 of 81336436] (ETC: Thu Oct 26 20:20:53 2023 ; 14 s 273.19 ms remaining ; 57 s 92.74 ms total) Thu Oct 26 20:20:41 2023: Inserted ≈80% of D-proof conclusions. [65069148 of 81336436] (ETC: Thu Oct 26 20:20:52 2023 ; 11 s 373.33 ms remaining ; 56 s 866.64 ms total) Thu Oct 26 20:20:44 2023: Inserted ≈85% of D-proof conclusions. [69135970 of 81336436] (ETC: Thu Oct 26 20:20:52 2023 ; 8 s 494.90 ms remaining ; 56 s 632.66 ms total) Thu Oct 26 20:20:46 2023: Inserted ≈90% of D-proof conclusions. [73202792 of 81336436] (ETC: Thu Oct 26 20:20:52 2023 ; 5 s 634.57 ms remaining ; 56 s 345.69 ms total) Thu Oct 26 20:20:49 2023: Inserted ≈95% of D-proof conclusions. [77269614 of 81336436] (ETC: Thu Oct 26 20:20:51 2023 ; 2 s 795.97 ms remaining ; 55 s 919.34 ms total) Thu Oct 26 20:20:51 2023: Inserted 100% of D-proof conclusions. [81336436 of 81336436] (ETC: Thu Oct 26 20:20:51 2023 ; 0.00 ms remaining ; 55 s 694.69 ms total) 55695.19 ms (55 s 695.20 ms) total insertion duration. Thu Oct 26 20:20:51 2023: Starting to iterate D-proof candidates of length 87. 366317.89 ms (6 min 6 s 317.89 ms) taken to iterate 692467431 condensed detachment proof strings of length 87. [Copy] Next iteration count (unfiltered83+): { 87, 692467431 } Thu Oct 26 20:26:58 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Thu Oct 26 20:28:48 2023: Process terminated. [pid: 162285, tid:22754652997504]