( This log file was generated by executing 'pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39734329 c18m 48 COMPLETED 0:0 00:18:00 39734329.ba+ 48 COMPLETED 0:0 00:18:00 101941908K 39734329.ex+ 48 COMPLETED 0:0 00:18:00 76K By 101941908 KiB = (101941908 / 1024^2) GiB = 97.219379425048828125 GiB, it used approximately 97.22 gibibytes of memory. ) Thu Oct 5 08:33:24 2023: Process started. [pid: 167857, tid:22845139355520] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed] (1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0)) [Main] Calling countNextIterationAmount(false, true). Thu Oct 5 08:33:24 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 7.67 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22845079107328] 25.87 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22845077006080] 21.23 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22845074904832] 18.19 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22845072803584] 4.91 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22845070702336] 16.33 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22845068601088] 8.12 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22844662609664] 22.96 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22844528391936] 15.41 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22844660508416] 19.87 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22844658407168] 21.79 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22844656305920] 12.75 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22844654204672] 24.93 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22844652103424] 8.53 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22844650002176] 23.05 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22844647900928] 92.36 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22844645799680] 39.32 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22844643698432] 51.89 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22844641597184] 56.14 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22844639495936] 75.74 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22844637394688] 73.61 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22844635293440] 96.61 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22844633192192] 176.30 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22844631090944] 369.87 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22844628989696] 825.63 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22844626888448] 2093.06 ms (2 s 93.06 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22844624787200] 5098.63 ms (5 s 98.63 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22844622685952] 539.08 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22844620584704] 863.96 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22844618483456] 1384.24 ms (1 s 384.24 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22844616382208] 2085.85 ms (2 s 85.85 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22844614280960] 2659.45 ms (2 s 659.45 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22844612179712] 3724.82 ms (3 s 724.82 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22844610078464] 5321.18 ms (5 s 321.18 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22844607977216] 5342.41 ms (5 s 342.41 ms) total read duration. Loaded 35 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 7 11 : 10 13 : 13 15 : 19 17 : 37 19 : 56 21 : 87 23 : 140 25 : 227 27 : 369 29 : 579 31 : 918 33 : 1499 35 : 2408 37 : 3881 39 : 6254 41 : 10109 43 : 16460 45 : 26753 47 : 43360 49 : 70709 51 : 115604 53 : 188634 55 : 308241 57 : 504870 59 : 827701 61 : 1357539 63 : 2227822 65 : 3660735 67 : 6021110 69 : 9907537 25303694 representatives in total. 14436.70 ms (14 s 436.70 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22844607977216] 26545.86 ms (26 s 545.86 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22844610078464] 41716.56 ms (41 s 716.56 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22844612179712] 41719.96 ms (41 s 719.96 ms) additional read duration. Loaded 3 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 173752662 representatives in total. Thu Oct 5 08:34:18 2023: Inserted ≈ 5% of D-proof conclusions. [ 8687633 of 173752662] (ETC: Thu Oct 5 08:36:16 2023 ; 1 min 58 s 651.70 ms remaining ; 2 min 4 s 896.52 ms total) Thu Oct 5 08:34:23 2023: Inserted ≈10% of D-proof conclusions. [ 17375266 of 173752662] (ETC: Thu Oct 5 08:36:03 2023 ; 1 min 40 s 325.21 ms remaining ; 1 min 51 s 472.45 ms total) Thu Oct 5 08:34:27 2023: Inserted ≈15% of D-proof conclusions. [ 26062899 of 173752662] (ETC: Thu Oct 5 08:35:56 2023 ; 1 min 28 s 506.80 ms remaining ; 1 min 44 s 125.65 ms total) Thu Oct 5 08:34:31 2023: Inserted ≈20% of D-proof conclusions. [ 34750532 of 173752662] (ETC: Thu Oct 5 08:35:51 2023 ; 1 min 19 s 406.47 ms remaining ; 1 min 39 s 258.09 ms total) Thu Oct 5 08:34:35 2023: Inserted ≈25% of D-proof conclusions. [ 43438165 of 173752662] (ETC: Thu Oct 5 08:35:47 2023 ; 1 min 11 s 903.85 ms remaining ; 1 min 35 s 871.80 ms total) Thu Oct 5 08:34:39 2023: Inserted ≈30% of D-proof conclusions. [ 52125798 of 173752662] (ETC: Thu Oct 5 08:35:44 2023 ; 1 min 4 s 926.21 ms remaining ; 1 min 32 s 751.73 ms total) Thu Oct 5 08:34:43 2023: Inserted ≈35% of D-proof conclusions. [ 60813431 of 173752662] (ETC: Thu Oct 5 08:35:41 2023 ; 58 s 538.01 ms remaining ; 1 min 30 s 58.48 ms total) Thu Oct 5 08:34:47 2023: Inserted ≈40% of D-proof conclusions. [ 69501064 of 173752662] (ETC: Thu Oct 5 08:35:40 2023 ; 53 s 432.52 ms remaining ; 1 min 29 s 54.21 ms total) Thu Oct 5 08:34:52 2023: Inserted ≈45% of D-proof conclusions. [ 78188697 of 173752662] (ETC: Thu Oct 5 08:35:41 2023 ; 49 s 231.70 ms remaining ; 1 min 29 s 512.18 ms total) Thu Oct 5 08:34:55 2023: Inserted ≈50% of D-proof conclusions. [ 86876331 of 173752662] (ETC: Thu Oct 5 08:35:39 2023 ; 44 s 5.88 ms remaining ; 1 min 28 s 11.76 ms total) Thu Oct 5 08:34:59 2023: Inserted ≈55% of D-proof conclusions. [ 95563964 of 173752662] (ETC: Thu Oct 5 08:35:38 2023 ; 38 s 845.52 ms remaining ; 1 min 26 s 323.39 ms total) Thu Oct 5 08:35:02 2023: Inserted ≈60% of D-proof conclusions. [104251597 of 173752662] (ETC: Thu Oct 5 08:35:35 2023 ; 33 s 530.56 ms remaining ; 1 min 23 s 826.40 ms total) Thu Oct 5 08:35:05 2023: Inserted ≈65% of D-proof conclusions. [112939230 of 173752662] (ETC: Thu Oct 5 08:35:34 2023 ; 29 s 10.69 ms remaining ; 1 min 22 s 887.69 ms total) Thu Oct 5 08:35:08 2023: Inserted ≈70% of D-proof conclusions. [121626863 of 173752662] (ETC: Thu Oct 5 08:35:33 2023 ; 24 s 338.55 ms remaining ; 1 min 21 s 128.50 ms total) Thu Oct 5 08:35:11 2023: Inserted ≈75% of D-proof conclusions. [130314496 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 19 s 912.03 ms remaining ; 1 min 19 s 648.13 ms total) Thu Oct 5 08:35:15 2023: Inserted ≈80% of D-proof conclusions. [139002129 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 15 s 953.09 ms remaining ; 1 min 19 s 765.45 ms total) Thu Oct 5 08:35:19 2023: Inserted ≈85% of D-proof conclusions. [147689762 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 11 s 879.35 ms remaining ; 1 min 19 s 195.69 ms total) Thu Oct 5 08:35:23 2023: Inserted ≈90% of D-proof conclusions. [156377395 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 7 s 898.41 ms remaining ; 1 min 18 s 984.09 ms total) Thu Oct 5 08:35:26 2023: Inserted ≈95% of D-proof conclusions. [165065028 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 3 s 936.21 ms remaining ; 1 min 18 s 724.13 ms total) Thu Oct 5 08:35:30 2023: Inserted 100% of D-proof conclusions. [173752662 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 0.00 ms remaining ; 1 min 18 s 493.92 ms total) 78495.09 ms (1 min 18 s 495.09 ms) total insertion duration. Thu Oct 5 08:35:30 2023: Starting to iterate D-proof candidates of length 77. 769711.36 ms (12 min 49 s 711.36 ms) taken to iterate 1198182438 condensed detachment proof strings of length 77. [Copy] Next iteration count (unfiltered71+): { 77, 1198182438 } Thu Oct 5 08:48:20 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Thu Oct 5 08:51:14 2023: Process terminated. [pid: 167857, tid:22845139355520]