( 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" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 40806186 optane_low 64 COMPLETED 0:0 00:58:02 40806186.ba+ 64 COMPLETED 0:0 00:58:02 408768632K 40806186.ex+ 64 COMPLETED 0:0 00:58:02 0 By 408768632 KiB = (408768632 / 1024^2) GiB = 389.83214569091796875 GiB, it used approximately 389.83 gibibytes of memory. ) Thu Nov 16 17:11:58 2023: Process started. [pid: 167189, tid:22742156158848] 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 16 17:11:58 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 11.91 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22742095935232] 21.39 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22742093833984] 24.72 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22742091732736] 20.42 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22742089631488] 10.13 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22742087530240] 21.30 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22741951211264] 26.56 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22742085428992] 14.48 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22742083327744] 8.89 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22742081226496] 23.51 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22742079125248] 12.73 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22742077024000] 17.55 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22742074922752] 33.52 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22742072821504] 23.62 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22742070720256] 36.40 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22742068619008] 18.05 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22742066517760] 9.84 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22742064416512] 24.75 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22742062315264] 56.92 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22742060214016] 55.41 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22742058112768] 180.93 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22742056011520] 122.51 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22741986047744] 60.44 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22741983946496] 87.80 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22741981845248] 464.00 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22741979744000] 340.62 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22741977642752] 138.03 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22741975541504] 429.16 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22741973440256] 668.71 ms taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22741971339008] 1192.27 ms (1 s 192.28 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22741969237760] 3928.48 ms (3 s 928.48 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22741967136512] 7161.74 ms (7 s 161.74 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22741965035264] 2886.98 ms (2 s 886.99 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22741962934016] 2864.48 ms (2 s 864.48 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22741960832768] 2971.00 ms (2 s 971.00 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22741958731520] 4986.35 ms (4 s 986.35 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22741956630272] 5798.11 ms (5 s 798.11 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22741954529024] 6435.94 ms (6 s 435.94 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22741949110016] 7429.37 ms (7 s 429.37 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22741947008768] 8078.17 ms (8 s 78.17 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22741944907520] 8161.19 ms (8 s 161.19 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. 49679.40 ms (49 s 679.40 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22741944907520] 76407.51 ms (1 min 16 s 407.51 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22741947008768] 107508.67 ms (1 min 47 s 508.67 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:22741949110016] 139047.54 ms (2 min 19 s 47.54 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:22741954529024] 171065.14 ms (2 min 51 s 65.14 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:22741956630272] 171102.04 ms (2 min 51 s 102.04 ms) additional read duration. Loaded 5 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 89 : 101227436 91 : 157874085 403154030 representatives in total. Thu Nov 16 17:15:31 2023: Inserted ≈ 5% of D-proof conclusions. [ 20157701 of 403154030] (ETC: Thu Nov 16 17:26:14 2023 ; 10 min 42 s 817.40 ms remaining ; 11 min 16 s 649.90 ms total) Thu Nov 16 17:16:10 2023: Inserted ≈10% of D-proof conclusions. [ 40315403 of 403154030] (ETC: Thu Nov 16 17:27:05 2023 ; 10 min 55 s 268.89 ms remaining ; 12 min 8 s 76.54 ms total) Thu Nov 16 17:16:55 2023: Inserted ≈15% of D-proof conclusions. [ 60473104 of 403154030] (ETC: Thu Nov 16 17:27:59 2023 ; 11 min 4 s 799.65 ms remaining ; 13 min 2 s 117.23 ms total) Thu Nov 16 17:17:44 2023: Inserted ≈20% of D-proof conclusions. [ 80630806 of 403154030] (ETC: Thu Nov 16 17:28:50 2023 ; 11 min 6 s 165.20 ms remaining ; 13 min 52 s 706.50 ms total) Thu Nov 16 17:18:20 2023: Inserted ≈25% of D-proof conclusions. [100788507 of 403154030] (ETC: Thu Nov 16 17:28:27 2023 ; 10 min 7 s 491.11 ms remaining ; 13 min 29 s 988.14 ms total) Thu Nov 16 17:18:59 2023: Inserted ≈30% of D-proof conclusions. [120946209 of 403154030] (ETC: Thu Nov 16 17:28:23 2023 ; 9 min 24 s 19.80 ms remaining ; 13 min 25 s 742.57 ms total) Thu Nov 16 17:19:53 2023: Inserted ≈35% of D-proof conclusions. [141103910 of 403154030] (ETC: Thu Nov 16 17:29:01 2023 ; 9 min 8 s 579.27 ms remaining ; 14 min 3 s 968.11 ms total) Thu Nov 16 17:20:24 2023: Inserted ≈40% of D-proof conclusions. [161261612 of 403154030] (ETC: Thu Nov 16 17:28:34 2023 ; 8 min 10 s 56.11 ms remaining ; 13 min 36 s 760.19 ms total) Thu Nov 16 17:20:53 2023: Inserted ≈45% of D-proof conclusions. [181419313 of 403154030] (ETC: Thu Nov 16 17:28:08 2023 ; 7 min 15 s 100.20 ms remaining ; 13 min 11 s 91.27 ms total) Thu Nov 16 17:21:35 2023: Inserted ≈50% of D-proof conclusions. [201577015 of 403154030] (ETC: Thu Nov 16 17:28:12 2023 ; 6 min 37 s 363.46 ms remaining ; 13 min 14 s 726.92 ms total) Thu Nov 16 17:22:16 2023: Inserted ≈55% of D-proof conclusions. [221734716 of 403154030] (ETC: Thu Nov 16 17:28:15 2023 ; 5 min 59 s 163.53 ms remaining ; 13 min 18 s 141.17 ms total) Thu Nov 16 17:23:18 2023: Inserted ≈60% of D-proof conclusions. [241892418 of 403154030] (ETC: Thu Nov 16 17:28:51 2023 ; 5 min 33 s 574.69 ms remaining ; 13 min 53 s 936.72 ms total) Thu Nov 16 17:23:53 2023: Inserted ≈65% of D-proof conclusions. [262050119 of 403154030] (ETC: Thu Nov 16 17:28:41 2023 ; 4 min 48 s 296.48 ms remaining ; 13 min 43 s 704.22 ms total) Thu Nov 16 17:24:25 2023: Inserted ≈70% of D-proof conclusions. [282207821 of 403154030] (ETC: Thu Nov 16 17:28:28 2023 ; 4 min 3 s 226.86 ms remaining ; 13 min 30 s 756.19 ms total) Thu Nov 16 17:24:55 2023: Inserted ≈75% of D-proof conclusions. [302365522 of 403154030] (ETC: Thu Nov 16 17:28:14 2023 ; 3 min 19 s 292.44 ms remaining ; 13 min 17 s 169.76 ms total) Thu Nov 16 17:25:26 2023: Inserted ≈80% of D-proof conclusions. [322523224 of 403154030] (ETC: Thu Nov 16 17:28:03 2023 ; 2 min 37 s 88.52 ms remaining ; 13 min 5 s 442.57 ms total) Thu Nov 16 17:26:02 2023: Inserted ≈85% of D-proof conclusions. [342680925 of 403154030] (ETC: Thu Nov 16 17:27:59 2023 ; 1 min 57 s 256.88 ms remaining ; 13 min 1 s 712.53 ms total) Thu Nov 16 17:26:40 2023: Inserted ≈90% of D-proof conclusions. [362838627 of 403154030] (ETC: Thu Nov 16 17:27:58 2023 ; 1 min 18 s 79.69 ms remaining ; 13 min 796.88 ms total) Thu Nov 16 17:27:25 2023: Inserted ≈95% of D-proof conclusions. [382996328 of 403154030] (ETC: Thu Nov 16 17:28:04 2023 ; 39 s 360.28 ms remaining ; 13 min 7 s 205.61 ms total) Thu Nov 16 17:28:08 2023: Inserted 100% of D-proof conclusions. [403154030 of 403154030] (ETC: Thu Nov 16 17:28:08 2023 ; 0.00 ms remaining ; 13 min 10 s 832.98 ms total) 790834.43 ms (13 min 10 s 834.44 ms) total insertion duration. Thu Nov 16 17:28:08 2023: Starting to iterate D-proof candidates of length 93. 1705474.92 ms (28 min 25 s 474.92 ms) taken to iterate 2979484674 condensed detachment proof strings of length 93. [Copy] Next iteration count (unfiltered83+): { 93, 2979484674 } Thu Nov 16 17:56:45 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Thu Nov 16 18:09:36 2023: Process terminated. [pid: 167189, tid:22742156158848]