( 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-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. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS%11" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ----------- 40855266 optane_low 64 COMPLETED 0:0 03:08:01 40855266.ba+ 64 COMPLETED 0:0 03:08:01 1142773416K 40855266.ex+ 64 COMPLETED 0:0 03:08:01 0 By 1142773416 KiB = (1142773416 / 1024^2) GiB = 1089.83365631103515625 GiB, it used approximately 1089.83 gibibytes of memory. ) Thu Nov 23 22:02:49 2023: Process started. [pid: 25364, tid:23067878508416] 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 Nov 23 22:02:49 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.23 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23067818260224] 0.16 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23067816158976] 0.56 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23067814057728] 0.34 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23067811956480] 0.10 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23067809855232] 0.02 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23067598255872] 0.60 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23067807753984] 0.79 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23067805652736] 0.50 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23067803551488] 0.19 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23067732473600] 1.27 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23067730372352] 0.27 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23067728271104] 110.43 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23067726169856] 0.08 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23067724068608] 0.26 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23067721967360] 0.19 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23067719866112] 5.19 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23067717764864] 4.47 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23067715663616] 4.82 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23067713562368] 5.74 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23067711461120] 10.02 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23067709359872] 13.46 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23067707258624] 18.51 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23067705157376] 21.17 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23067703056128] 54.12 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23067700954880] 83.10 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23067698853632] 532.59 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23067696752384] 587.58 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23067694651136] 1260.06 ms (1 s 260.06 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23067692549888] 4179.68 ms (4 s 179.68 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23067690448640] 5415.28 ms (5 s 415.28 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23067688347392] 8229.84 ms (8 s 229.84 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23067686246144] 3071.91 ms (3 s 71.91 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23067684144896] 4079.38 ms (4 s 79.38 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23067682043648] 4985.44 ms (4 s 985.44 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23067679942400] 6213.37 ms (6 s 213.37 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23067677841152] 7601.22 ms (7 s 601.22 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23067675739904] 8458.72 ms (8 s 458.72 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23067673638656] 9445.75 ms (9 s 445.75 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23067671537408] 10413.94 ms (10 s 413.94 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23067669436160] 10502.58 ms (10 s 502.58 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. 118692.28 ms (1 min 58 s 692.28 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23067669436160] 178464.54 ms (2 min 58 s 464.54 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:23067671537408] 256211.95 ms (4 min 16 s 211.95 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:23067673638656] 329963.28 ms (5 min 29 s 963.28 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:23067675739904] 407675.21 ms (6 min 47 s 675.21 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:23067677841152] 490783.78 ms (8 min 10 s 783.78 ms) taken to read 251856137 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. [tid:23067679942400] 606269.82 ms (10 min 6 s 269.82 ms) taken to read 406329619 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs95-unfiltered83+.txt. [tid:23067682043648] 606284.88 ms (10 min 6 s 284.88 ms) additional read duration. Loaded 7 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 89 : 101227436 91 : 157874085 93 : 251856137 95 : 406329619 1061339786 representatives in total. Thu Nov 23 22:14:38 2023: Inserted ≈ 5% of D-proof conclusions. [ 53066989 of 1061339786] (ETC: Thu Nov 23 22:43:52 2023 ; 29 min 14 s 379.60 ms remaining ; 30 min 46 s 715.37 ms total) Thu Nov 23 22:16:33 2023: Inserted ≈10% of D-proof conclusions. [ 106133978 of 1061339786] (ETC: Thu Nov 23 22:47:40 2023 ; 31 min 7 s 81.02 ms remaining ; 34 min 34 s 534.46 ms total) Thu Nov 23 22:18:28 2023: Inserted ≈15% of D-proof conclusions. [ 159200967 of 1061339786] (ETC: Thu Nov 23 22:48:55 2023 ; 30 min 26 s 931.07 ms remaining ; 35 min 49 s 330.67 ms total) Thu Nov 23 22:20:33 2023: Inserted ≈20% of D-proof conclusions. [ 212267957 of 1061339786] (ETC: Thu Nov 23 22:50:20 2023 ; 29 min 47 s 170.24 ms remaining ; 37 min 13 s 962.80 ms total) Thu Nov 23 22:23:01 2023: Inserted ≈25% of D-proof conclusions. [ 265334946 of 1061339786] (ETC: Thu Nov 23 22:52:45 2023 ; 29 min 44 s 452.97 ms remaining ; 39 min 39 s 270.62 ms total) Thu Nov 23 22:25:17 2023: Inserted ≈30% of D-proof conclusions. [ 318401935 of 1061339786] (ETC: Thu Nov 23 22:53:43 2023 ; 28 min 26 s 54.92 ms remaining ; 40 min 37 s 221.31 ms total) Thu Nov 23 22:27:41 2023: Inserted ≈35% of D-proof conclusions. [ 371468925 of 1061339786] (ETC: Thu Nov 23 22:54:45 2023 ; 27 min 4 s 767.54 ms remaining ; 41 min 39 s 642.36 ms total) Thu Nov 23 22:29:49 2023: Inserted ≈40% of D-proof conclusions. [ 424535914 of 1061339786] (ETC: Thu Nov 23 22:54:55 2023 ; 25 min 5 s 475.53 ms remaining ; 41 min 49 s 125.87 ms total) Thu Nov 23 22:31:46 2023: Inserted ≈45% of D-proof conclusions. [ 477602903 of 1061339786] (ETC: Thu Nov 23 22:54:36 2023 ; 22 min 49 s 426.53 ms remaining ; 41 min 29 s 866.42 ms total) Thu Nov 23 22:33:43 2023: Inserted ≈50% of D-proof conclusions. [ 530669893 of 1061339786] (ETC: Thu Nov 23 22:54:21 2023 ; 20 min 37 s 450.24 ms remaining ; 41 min 14 s 900.48 ms total) Thu Nov 23 22:35:52 2023: Inserted ≈55% of D-proof conclusions. [ 583736882 of 1061339786] (ETC: Thu Nov 23 22:54:29 2023 ; 18 min 37 s 546.24 ms remaining ; 41 min 23 s 436.09 ms total) Thu Nov 23 22:38:34 2023: Inserted ≈60% of D-proof conclusions. [ 636803871 of 1061339786] (ETC: Thu Nov 23 22:55:33 2023 ; 16 min 58 s 760.43 ms remaining ; 42 min 26 s 901.06 ms total) Thu Nov 23 22:40:41 2023: Inserted ≈65% of D-proof conclusions. [ 689870860 of 1061339786] (ETC: Thu Nov 23 22:55:32 2023 ; 14 min 51 s 353.20 ms remaining ; 42 min 26 s 723.42 ms total) Thu Nov 23 22:42:33 2023: Inserted ≈70% of D-proof conclusions. [ 742937850 of 1061339786] (ETC: Thu Nov 23 22:55:11 2023 ; 12 min 37 s 572.66 ms remaining ; 42 min 5 s 242.21 ms total) Thu Nov 23 22:44:33 2023: Inserted ≈75% of D-proof conclusions. [ 796004839 of 1061339786] (ETC: Thu Nov 23 22:55:03 2023 ; 10 min 29 s 241.11 ms remaining ; 41 min 56 s 964.43 ms total) Thu Nov 23 22:46:37 2023: Inserted ≈80% of D-proof conclusions. [ 849071828 of 1061339786] (ETC: Thu Nov 23 22:54:59 2023 ; 8 min 22 s 732.90 ms remaining ; 41 min 53 s 664.52 ms total) Thu Nov 23 22:48:53 2023: Inserted ≈85% of D-proof conclusions. [ 902138818 of 1061339786] (ETC: Thu Nov 23 22:55:12 2023 ; 6 min 18 s 965.62 ms remaining ; 42 min 6 s 437.46 ms total) Thu Nov 23 22:50:59 2023: Inserted ≈90% of D-proof conclusions. [ 955205807 of 1061339786] (ETC: Thu Nov 23 22:55:12 2023 ; 4 min 12 s 595.87 ms remaining ; 42 min 5 s 958.68 ms total) Thu Nov 23 22:53:15 2023: Inserted ≈95% of D-proof conclusions. [1008272796 of 1061339786] (ETC: Thu Nov 23 22:55:22 2023 ; 2 min 6 s 830.41 ms remaining ; 42 min 16 s 608.13 ms total) Thu Nov 23 22:56:29 2023: Inserted 100% of D-proof conclusions. [1061339786 of 1061339786] (ETC: Thu Nov 23 22:56:29 2023 ; 0.00 ms remaining ; 43 min 23 s 17.61 ms total) 2603018.04 ms (43 min 23 s 18.04 ms) total insertion duration. Thu Nov 23 22:56:29 2023: Starting to iterate D-proof candidates of length 97. 5322521.74 ms (1 h 28 min 42 s 521.74 ms) taken to iterate 7912094178 condensed detachment proof strings of length 97. [Copy] Next iteration count (unfiltered83+): { 97, 7912094178 } Fri Nov 24 00:25:11 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Fri Nov 24 01:09:13 2023: Process terminated. [pid: 25364, tid:23067878508416]