( This log file was generated by executing 'pmGenerator -c -n -s CpCCNqCCNrsCptCCtqCrq --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40422639 optane_low 64 COMPLETED 0:0 00:22:26 40422639.ba+ 64 COMPLETED 0:0 00:22:26 199015504K 40422639.ex+ 64 COMPLETED 0:0 00:22:26 0 By 199015504 KiB = (199015504 / 1024^2) GiB = 189.7959747314453125 GiB, it used approximately 189.80 gibibytes of memory. ) Fri Oct 27 23:46:02 2023: Process started. [pid: 39742, tid:23011084609408] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314] (1) C0CCN1CCN2.3C0.4CC4.1C2.1 - CpCCNqCCNrsCptCCtqCrq - 0\imply((\not1\imply((\not2\imply3)\imply(0\imply4)))\imply((4\imply1)\imply(2\imply1))) [Main] Calling countNextIterationAmount(false, true). Fri Oct 27 23:46:02 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.00 ms taken to load initial representatives. 18.45 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:23011024385792] 21.62 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:23011022284544] 17.87 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:23011020183296] 21.13 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:23011018082048] 18.47 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:23011015980800] 16.35 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:23010879661824] 20.21 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:23011013879552] 9.78 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:23011011778304] 60.80 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:23011009677056] 914.78 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:23011007575808] 29.56 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:23011005474560] 100.90 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:23011003373312] 64.59 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:23011001272064] 256.82 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:23010999170816] 148.23 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:23010997069568] 79.80 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:23010994968320] 92.10 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:23010992867072] 104.65 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:23010990765824] 230.70 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:23010988664576] 633.43 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:23010986563328] 639.12 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:23010984462080] 3057.49 ms (3 s 57.49 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:23010982360832] 3980.31 ms (3 s 980.31 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:23010980259584] 834.39 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:23010978158336] 2532.81 ms (2 s 532.81 ms) taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:23010976057088] 3848.40 ms (3 s 848.40 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:23010973955840] 3893.38 ms (3 s 893.38 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:23010971854592] 5423.03 ms (5 s 423.04 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:23010969753344] 6065.83 ms (6 s 65.83 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:23010967652096] 7325.68 ms (7 s 325.68 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:23010965550848] 8517.07 ms (8 s 517.08 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:23010963449600] 8581.40 ms (8 s 581.40 ms) total read duration. Loaded 32 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 4 9 : 7 11 : 14 13 : 23 15 : 42 17 : 72 19 : 119 21 : 180 23 : 296 25 : 493 27 : 809 29 : 1330 31 : 2190 33 : 3606 35 : 5925 37 : 9738 39 : 15948 41 : 26109 43 : 42844 45 : 70083 47 : 115027 49 : 188519 51 : 308975 53 : 506415 55 : 830126 57 : 1360461 59 : 2229126 61 : 3652191 63 : 5983166 15353842 representatives in total. 23130.00 ms (23 s 130.00 ms) taken to read 15025264 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. [tid:23010963449600] 50309.75 ms (50 s 309.75 ms) taken to read 32295163 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs67-unfiltered65+.txt. [tid:23010965550848] 71966.31 ms (1 min 11 s 966.31 ms) taken to read 63892072 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs69-unfiltered65+.txt. [tid:23010967652096] 71989.40 ms (1 min 11 s 989.40 ms) additional read duration. Loaded 3 more representative collections of sizes: 65 : 15025264 67 : 32295163 69 : 63892072 126566341 representatives in total. Fri Oct 27 23:47:39 2023: Inserted ≈ 5% of D-proof conclusions. [ 6328317 of 126566341] (ETC: Fri Oct 27 23:52:36 2023 ; 4 min 57 s 537.78 ms remaining ; 5 min 13 s 197.66 ms total) Fri Oct 27 23:47:55 2023: Inserted ≈10% of D-proof conclusions. [ 12656634 of 126566341] (ETC: Fri Oct 27 23:52:45 2023 ; 4 min 49 s 691.16 ms remaining ; 5 min 21 s 879.07 ms total) Fri Oct 27 23:48:09 2023: Inserted ≈15% of D-proof conclusions. [ 18984951 of 126566341] (ETC: Fri Oct 27 23:52:27 2023 ; 4 min 18 s 762.60 ms remaining ; 5 min 4 s 426.59 ms total) Fri Oct 27 23:48:19 2023: Inserted ≈20% of D-proof conclusions. [ 25313268 of 126566341] (ETC: Fri Oct 27 23:52:05 2023 ; 3 min 45 s 697.30 ms remaining ; 4 min 42 s 121.62 ms total) Fri Oct 27 23:48:31 2023: Inserted ≈25% of D-proof conclusions. [ 31641585 of 126566341] (ETC: Fri Oct 27 23:51:56 2023 ; 3 min 24 s 926.01 ms remaining ; 4 min 33 s 234.68 ms total) Fri Oct 27 23:48:42 2023: Inserted ≈30% of D-proof conclusions. [ 37969902 of 126566341] (ETC: Fri Oct 27 23:51:47 2023 ; 3 min 4 s 556.94 ms remaining ; 4 min 23 s 652.76 ms total) Fri Oct 27 23:48:53 2023: Inserted ≈35% of D-proof conclusions. [ 44298219 of 126566341] (ETC: Fri Oct 27 23:51:41 2023 ; 2 min 47 s 433.70 ms remaining ; 4 min 17 s 590.30 ms total) Fri Oct 27 23:49:05 2023: Inserted ≈40% of D-proof conclusions. [ 50626536 of 126566341] (ETC: Fri Oct 27 23:51:38 2023 ; 2 min 32 s 787.56 ms remaining ; 4 min 14 s 645.94 ms total) Fri Oct 27 23:49:17 2023: Inserted ≈45% of D-proof conclusions. [ 56954853 of 126566341] (ETC: Fri Oct 27 23:51:37 2023 ; 2 min 19 s 841.81 ms remaining ; 4 min 14 s 257.83 ms total) Fri Oct 27 23:49:29 2023: Inserted ≈50% of D-proof conclusions. [ 63283170 of 126566341] (ETC: Fri Oct 27 23:51:36 2023 ; 2 min 6 s 307.23 ms remaining ; 4 min 12 s 614.45 ms total) Fri Oct 27 23:49:41 2023: Inserted ≈55% of D-proof conclusions. [ 69611487 of 126566341] (ETC: Fri Oct 27 23:51:34 2023 ; 1 min 53 s 152.72 ms remaining ; 4 min 11 s 450.48 ms total) Fri Oct 27 23:49:53 2023: Inserted ≈60% of D-proof conclusions. [ 75939804 of 126566341] (ETC: Fri Oct 27 23:51:33 2023 ; 1 min 40 s 164.33 ms remaining ; 4 min 10 s 410.83 ms total) Fri Oct 27 23:50:05 2023: Inserted ≈65% of D-proof conclusions. [ 82268121 of 126566341] (ETC: Fri Oct 27 23:51:32 2023 ; 1 min 27 s 331.56 ms remaining ; 4 min 9 s 518.75 ms total) Fri Oct 27 23:50:17 2023: Inserted ≈70% of D-proof conclusions. [ 88596438 of 126566341] (ETC: Fri Oct 27 23:51:32 2023 ; 1 min 14 s 597.97 ms remaining ; 4 min 8 s 659.89 ms total) Fri Oct 27 23:50:29 2023: Inserted ≈75% of D-proof conclusions. [ 94924755 of 126566341] (ETC: Fri Oct 27 23:51:31 2023 ; 1 min 2 s 18.92 ms remaining ; 4 min 8 s 75.68 ms total) Fri Oct 27 23:50:41 2023: Inserted ≈80% of D-proof conclusions. [101253072 of 126566341] (ETC: Fri Oct 27 23:51:30 2023 ; 49 s 462.74 ms remaining ; 4 min 7 s 313.72 ms total) Fri Oct 27 23:50:53 2023: Inserted ≈85% of D-proof conclusions. [107581389 of 126566341] (ETC: Fri Oct 27 23:51:30 2023 ; 37 s 17.15 ms remaining ; 4 min 6 s 781.01 ms total) Fri Oct 27 23:51:06 2023: Inserted ≈90% of D-proof conclusions. [113909706 of 126566341] (ETC: Fri Oct 27 23:51:31 2023 ; 24 s 833.46 ms remaining ; 4 min 8 s 334.55 ms total) Fri Oct 27 23:51:20 2023: Inserted ≈95% of D-proof conclusions. [120238023 of 126566341] (ETC: Fri Oct 27 23:51:33 2023 ; 12 s 498.37 ms remaining ; 4 min 9 s 967.42 ms total) Fri Oct 27 23:51:35 2023: Inserted 100% of D-proof conclusions. [126566341 of 126566341] (ETC: Fri Oct 27 23:51:35 2023 ; 0.00 ms remaining ; 4 min 11 s 724.56 ms total) 251726.08 ms (4 min 11 s 726.08 ms) total insertion duration. Fri Oct 27 23:51:35 2023: Starting to iterate D-proof candidates of length 71. 802272.88 ms (13 min 22 s 272.88 ms) taken to iterate 1211683171 condensed detachment proof strings of length 71. [Copy] Next iteration count (unfiltered65+): { 71, 1211683171 } Sat Oct 28 00:04:57 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Sat Oct 28 00:08:16 2023: Process terminated. [pid: 39742, tid:23011084609408]