( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40411591 c18m_low 48 COMPLETED 0:0 00:17:34 40411591.ba+ 48 COMPLETED 0:0 00:17:34 134783968K 40411591.ex+ 48 COMPLETED 0:0 00:17:34 0 By 134783968 KiB = (134783968 / 1024^2) GiB = 128.540008544921875 GiB, it used approximately 128.54 gibibytes of memory. ) Sat Oct 28 01:09:19 2023: Process started. [pid: 244699, tid:22491510421376] 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). Sat Oct 28 01:09:19 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.03 ms taken to load initial representatives. 6.43 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22491450173184] 12.10 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22491448071936] 18.83 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22491445970688] 16.68 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22491443869440] 10.31 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22491441768192] 23.73 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22491439666944] 3.19 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22491437565696] 12.30 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22491435464448] 20.70 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22491433363200] 18.85 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22491431261952] 11.90 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22491429160704] 11.88 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22491427059456] 30.40 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22491424958208] 14.64 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22491422856960] 4.40 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22491420755712] 12.20 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22491418654464] 25.36 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22491416553216] 28.22 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22491414451968] 39.43 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22491412350720] 52.13 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22491410249472] 35.08 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22491408148224] 61.24 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22491406046976] 83.33 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22491403945728] 66.39 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22489858045696] 95.29 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22489721726720] 164.39 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22489855944448] 249.79 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22489853843200] 514.56 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22489851741952] 1037.96 ms (1 s 37.96 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22489849640704] 2214.54 ms (2 s 214.54 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22489847539456] 4995.33 ms (4 s 995.33 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22489845438208] 10143.93 ms (10 s 143.93 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22489843336960] 771.86 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22489841235712] 1116.08 ms (1 s 116.08 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22489839134464] 1579.15 ms (1 s 579.15 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22489837033216] 2137.30 ms (2 s 137.30 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22489834931968] 2887.45 ms (2 s 887.45 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22489832830720] 3717.17 ms (3 s 717.17 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22489830729472] 4778.47 ms (4 s 778.47 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22489828628224] 6194.24 ms (6 s 194.24 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22489826526976] 10187.97 ms (10 s 187.97 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. 22691.41 ms (22 s 691.41 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22489826526976] 46543.01 ms (46 s 543.01 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22489828628224] 66628.29 ms (1 min 6 s 628.29 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:22489830729472] 66661.83 ms (1 min 6 s 661.83 ms) additional read duration. Loaded 3 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 144052509 representatives in total. Sat Oct 28 01:10:44 2023: Inserted ≈ 5% of D-proof conclusions. [ 7202625 of 144052509] (ETC: Sat Oct 28 01:13:04 2023 ; 2 min 19 s 931.70 ms remaining ; 2 min 27 s 296.53 ms total) Sat Oct 28 01:10:51 2023: Inserted ≈10% of D-proof conclusions. [ 14405250 of 144052509] (ETC: Sat Oct 28 01:13:03 2023 ; 2 min 11 s 804.29 ms remaining ; 2 min 26 s 449.21 ms total) Sat Oct 28 01:10:57 2023: Inserted ≈15% of D-proof conclusions. [ 21607876 of 144052509] (ETC: Sat Oct 28 01:12:54 2023 ; 1 min 57 s 485.32 ms remaining ; 2 min 18 s 218.03 ms total) Sat Oct 28 01:11:04 2023: Inserted ≈20% of D-proof conclusions. [ 28810501 of 144052509] (ETC: Sat Oct 28 01:12:54 2023 ; 1 min 50 s 269.30 ms remaining ; 2 min 17 s 836.62 ms total) Sat Oct 28 01:11:11 2023: Inserted ≈25% of D-proof conclusions. [ 36013127 of 144052509] (ETC: Sat Oct 28 01:12:56 2023 ; 1 min 44 s 650.11 ms remaining ; 2 min 19 s 533.48 ms total) Sat Oct 28 01:11:19 2023: Inserted ≈30% of D-proof conclusions. [ 43215752 of 144052509] (ETC: Sat Oct 28 01:12:58 2023 ; 1 min 39 s 48.32 ms remaining ; 2 min 21 s 497.61 ms total) Sat Oct 28 01:11:25 2023: Inserted ≈35% of D-proof conclusions. [ 50418378 of 144052509] (ETC: Sat Oct 28 01:12:55 2023 ; 1 min 29 s 948.34 ms remaining ; 2 min 18 s 382.06 ms total) Sat Oct 28 01:11:32 2023: Inserted ≈40% of D-proof conclusions. [ 57621003 of 144052509] (ETC: Sat Oct 28 01:12:55 2023 ; 1 min 23 s 371.60 ms remaining ; 2 min 18 s 952.67 ms total) Sat Oct 28 01:11:39 2023: Inserted ≈45% of D-proof conclusions. [ 64823629 of 144052509] (ETC: Sat Oct 28 01:12:56 2023 ; 1 min 17 s 54.56 ms remaining ; 2 min 20 s 99.20 ms total) Sat Oct 28 01:11:46 2023: Inserted ≈50% of D-proof conclusions. [ 72026254 of 144052509] (ETC: Sat Oct 28 01:12:56 2023 ; 1 min 9 s 990.48 ms remaining ; 2 min 19 s 980.95 ms total) Sat Oct 28 01:11:53 2023: Inserted ≈55% of D-proof conclusions. [ 79228879 of 144052509] (ETC: Sat Oct 28 01:12:56 2023 ; 1 min 2 s 841.63 ms remaining ; 2 min 19 s 648.06 ms total) Sat Oct 28 01:11:59 2023: Inserted ≈60% of D-proof conclusions. [ 86431505 of 144052509] (ETC: Sat Oct 28 01:12:55 2023 ; 55 s 353.79 ms remaining ; 2 min 18 s 384.47 ms total) Sat Oct 28 01:12:04 2023: Inserted ≈65% of D-proof conclusions. [ 93634130 of 144052509] (ETC: Sat Oct 28 01:12:52 2023 ; 47 s 359.61 ms remaining ; 2 min 15 s 313.16 ms total) Sat Oct 28 01:12:10 2023: Inserted ≈70% of D-proof conclusions. [100836756 of 144052509] (ETC: Sat Oct 28 01:12:50 2023 ; 40 s 247.68 ms remaining ; 2 min 14 s 158.94 ms total) Sat Oct 28 01:12:17 2023: Inserted ≈75% of D-proof conclusions. [108039381 of 144052509] (ETC: Sat Oct 28 01:12:50 2023 ; 33 s 562.39 ms remaining ; 2 min 14 s 249.57 ms total) Sat Oct 28 01:12:25 2023: Inserted ≈80% of D-proof conclusions. [115242007 of 144052509] (ETC: Sat Oct 28 01:12:52 2023 ; 27 s 239.29 ms remaining ; 2 min 16 s 196.44 ms total) Sat Oct 28 01:12:33 2023: Inserted ≈85% of D-proof conclusions. [122444632 of 144052509] (ETC: Sat Oct 28 01:12:54 2023 ; 20 s 629.95 ms remaining ; 2 min 17 s 533.01 ms total) Sat Oct 28 01:12:40 2023: Inserted ≈90% of D-proof conclusions. [129647258 of 144052509] (ETC: Sat Oct 28 01:12:54 2023 ; 13 s 761.01 ms remaining ; 2 min 17 s 610.13 ms total) Sat Oct 28 01:12:46 2023: Inserted ≈95% of D-proof conclusions. [136849883 of 144052509] (ETC: Sat Oct 28 01:12:53 2023 ; 6 s 840.50 ms remaining ; 2 min 16 s 809.91 ms total) Sat Oct 28 01:12:54 2023: Inserted 100% of D-proof conclusions. [144052509 of 144052509] (ETC: Sat Oct 28 01:12:54 2023 ; 0.00 ms remaining ; 2 min 17 s 428.74 ms total) 137449.21 ms (2 min 17 s 449.21 ms) total insertion duration. Sat Oct 28 01:12:54 2023: Starting to iterate D-proof candidates of length 89. 652504.88 ms (10 min 52 s 504.88 ms) taken to iterate 1120159490 condensed detachment proof strings of length 89. [Copy] Next iteration count (unfiltered83+): { 89, 1120159490 } Sat Oct 28 01:23:46 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sat Oct 28 01:26:40 2023: Process terminated. [pid: 244699, tid:22491510421376]