( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40833947 optane_low 64 COMPLETED 0:0 01:54:06 40833947.ba+ 64 COMPLETED 0:0 01:54:06 682020752K 40833947.ex+ 64 COMPLETED 0:0 01:54:06 16K By 682020752 KiB = (682020752 / 1024^2) GiB = 650.4256744384765625 GiB, it used approximately 650.43 gibibytes of memory. ) Sun Nov 19 12:23:44 2023: Process started. [pid: 268874, tid:23185404274560] 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). Sun Nov 19 12:23:44 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 25.17 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23185344050944] 6.42 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23185341949696] 12.27 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23185339848448] 15.26 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23185337747200] 10.41 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23185335645952] 12.35 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23185240094464] 18.26 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23185333544704] 14.56 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23185331443456] 16.32 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23185329342208] 20.17 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23185327240960] 19.20 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23185325139712] 26.32 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23185323038464] 23.37 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23185320937216] 25.90 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23185318835968] 27.45 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23185316734720] 34.75 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23185314633472] 24.24 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23185312532224] 30.16 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23185310430976] 37.50 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23185237993216] 162.49 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23185235891968] 163.33 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23185233790720] 317.18 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23185231689472] 66.28 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23185229588224] 177.69 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23185227486976] 407.33 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23185225385728] 427.59 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23185223284480] 920.47 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23185221183232] 996.29 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23185219081984] 1085.75 ms (1 s 85.75 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23185216980736] 2202.84 ms (2 s 202.84 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23185214879488] 5703.49 ms (5 s 703.49 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23185212778240] 7891.77 ms (7 s 891.77 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23185210676992] 2933.77 ms (2 s 933.77 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23185208575744] 3581.71 ms (3 s 581.71 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23185206474496] 1470.16 ms (1 s 470.16 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23185204373248] 5288.32 ms (5 s 288.32 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23185202272000] 6563.95 ms (6 s 563.95 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23185200170752] 7533.69 ms (7 s 533.69 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23185198069504] 8106.81 ms (8 s 106.81 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23185195968256] 9299.42 ms (9 s 299.42 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23185193867008] 9625.33 ms (9 s 625.33 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. 105434.31 ms (1 min 45 s 434.31 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23185193867008] 139190.20 ms (2 min 19 s 190.20 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:23185195968256] 180632.82 ms (3 min 632.82 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:23185198069504] 228088.82 ms (3 min 48 s 88.82 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:23185200170752] 276829.56 ms (4 min 36 s 829.56 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:23185202272000] 331035.76 ms (5 min 31 s 35.76 ms) taken to read 251856137 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. [tid:23185204373248] 331190.76 ms (5 min 31 s 190.76 ms) additional read duration. Loaded 6 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 89 : 101227436 91 : 157874085 93 : 251856137 655010167 representatives in total. Sun Nov 19 12:30:33 2023: Inserted ≈ 5% of D-proof conclusions. [ 32750508 of 655010167] (ETC: Sun Nov 19 12:52:10 2023 ; 21 min 36 s 459.79 ms remaining ; 22 min 44 s 694.51 ms total) Sun Nov 19 12:31:58 2023: Inserted ≈10% of D-proof conclusions. [ 65501016 of 655010167] (ETC: Sun Nov 19 12:54:58 2023 ; 22 min 59 s 660.40 ms remaining ; 25 min 32 s 956.00 ms total) Sun Nov 19 12:33:28 2023: Inserted ≈15% of D-proof conclusions. [ 98251525 of 655010167] (ETC: Sun Nov 19 12:56:26 2023 ; 22 min 57 s 728.23 ms remaining ; 27 min 856.74 ms total) Sun Nov 19 12:34:47 2023: Inserted ≈20% of D-proof conclusions. [131002033 of 655010167] (ETC: Sun Nov 19 12:56:14 2023 ; 21 min 27 s 153.37 ms remaining ; 26 min 48 s 941.71 ms total) Sun Nov 19 12:35:57 2023: Inserted ≈25% of D-proof conclusions. [163752541 of 655010167] (ETC: Sun Nov 19 12:55:35 2023 ; 19 min 37 s 683.22 ms remaining ; 26 min 10 s 244.30 ms total) Sun Nov 19 12:37:13 2023: Inserted ≈30% of D-proof conclusions. [196503050 of 655010167] (ETC: Sun Nov 19 12:55:26 2023 ; 18 min 12 s 568.40 ms remaining ; 26 min 812.00 ms total) Sun Nov 19 12:38:31 2023: Inserted ≈35% of D-proof conclusions. [229253558 of 655010167] (ETC: Sun Nov 19 12:55:26 2023 ; 16 min 54 s 987.06 ms remaining ; 26 min 1 s 518.55 ms total) Sun Nov 19 12:39:42 2023: Inserted ≈40% of D-proof conclusions. [262004066 of 655010167] (ETC: Sun Nov 19 12:55:09 2023 ; 15 min 26 s 284.36 ms remaining ; 25 min 43 s 807.26 ms total) Sun Nov 19 12:40:51 2023: Inserted ≈45% of D-proof conclusions. [294754575 of 655010167] (ETC: Sun Nov 19 12:54:50 2023 ; 13 min 58 s 805.33 ms remaining ; 25 min 25 s 100.59 ms total) Sun Nov 19 12:42:16 2023: Inserted ≈50% of D-proof conclusions. [327505083 of 655010167] (ETC: Sun Nov 19 12:55:07 2023 ; 12 min 51 s 197.74 ms remaining ; 25 min 42 s 395.48 ms total) Sun Nov 19 12:43:52 2023: Inserted ≈55% of D-proof conclusions. [360255591 of 655010167] (ETC: Sun Nov 19 12:55:42 2023 ; 11 min 49 s 585.24 ms remaining ; 26 min 16 s 856.08 ms total) Sun Nov 19 12:45:29 2023: Inserted ≈60% of D-proof conclusions. [393006100 of 655010167] (ETC: Sun Nov 19 12:56:12 2023 ; 10 min 42 s 964.82 ms remaining ; 26 min 47 s 412.06 ms total) Sun Nov 19 12:46:39 2023: Inserted ≈65% of D-proof conclusions. [425756608 of 655010167] (ETC: Sun Nov 19 12:55:56 2023 ; 9 min 16 s 806.16 ms remaining ; 26 min 30 s 874.74 ms total) Sun Nov 19 12:47:33 2023: Inserted ≈70% of D-proof conclusions. [458507116 of 655010167] (ETC: Sun Nov 19 12:55:19 2023 ; 7 min 46 s 189.32 ms remaining ; 25 min 53 s 964.41 ms total) Sun Nov 19 12:48:31 2023: Inserted ≈75% of D-proof conclusions. [491257625 of 655010167] (ETC: Sun Nov 19 12:54:53 2023 ; 6 min 21 s 946.85 ms remaining ; 25 min 27 s 787.40 ms total) Sun Nov 19 12:49:34 2023: Inserted ≈80% of D-proof conclusions. [524008133 of 655010167] (ETC: Sun Nov 19 12:54:36 2023 ; 5 min 2 s 281.67 ms remaining ; 25 min 11 s 408.35 ms total) Sun Nov 19 12:50:45 2023: Inserted ≈85% of D-proof conclusions. [556758641 of 655010167] (ETC: Sun Nov 19 12:54:31 2023 ; 3 min 45 s 978.09 ms remaining ; 25 min 6 s 520.56 ms total) Sun Nov 19 12:51:57 2023: Inserted ≈90% of D-proof conclusions. [589509150 of 655010167] (ETC: Sun Nov 19 12:54:27 2023 ; 2 min 30 s 196.79 ms remaining ; 25 min 1 s 967.86 ms total) Sun Nov 19 12:53:23 2023: Inserted ≈95% of D-proof conclusions. [622259658 of 655010167] (ETC: Sun Nov 19 12:54:38 2023 ; 1 min 15 s 675.33 ms remaining ; 25 min 13 s 506.55 ms total) Sun Nov 19 12:55:23 2023: Inserted 100% of D-proof conclusions. [655010167 of 655010167] (ETC: Sun Nov 19 12:55:23 2023 ; 0.00 ms remaining ; 25 min 57 s 934.45 ms total) 1557936.15 ms (25 min 57 s 936.15 ms) total insertion duration. Sun Nov 19 12:55:23 2023: Starting to iterate D-proof candidates of length 95. 3422205.13 ms (57 min 2 s 205.13 ms) taken to iterate 4844444054 condensed detachment proof strings of length 95. [Copy] Next iteration count (unfiltered83+): { 95, 4844444054 } Sun Nov 19 13:52:25 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Sun Nov 19 14:17:01 2023: Process terminated. [pid: 268874, tid:23185404274560]