( 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 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40063076 c18m_low 48 COMPLETED 0:0 00:01:58 40063076.ba+ 48 COMPLETED 0:0 00:01:58 10635352K 40063076.ex+ 48 COMPLETED 0:0 00:01:58 76K By 10635352 KiB = (10635352 / 1024^2) GiB = 10.14266204833984375 GiB, it used approximately 10.14 gibibytes of memory. ) Sat Oct 14 12:39:09 2023: Process started. [pid: 245717, tid:23293669812096] 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). Sat Oct 14 12:39:09 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 25.50 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:23293609563904] 26.17 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:23293607462656] 18.64 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:23293605361408] 10.82 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:23293603260160] 16.61 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:23293601158912] 27.44 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:23293599057664] 26.38 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:23293596956416] 11.95 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:23293594855168] 27.83 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:23293592753920] 29.54 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:23293590652672] 25.13 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:23293588551424] 31.37 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:23293586450176] 44.37 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:23293584348928] 52.79 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:23293582247680] 55.18 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:23293580146432] 58.28 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:23293578045184] 48.85 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:23293575943936] 86.18 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:23293573842688] 159.86 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:23293571741440] 327.89 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:23293569640192] 765.91 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:23293567538944] 1903.66 ms (1 s 903.66 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:23293565437696] 4812.54 ms (4 s 812.54 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:23293563336448] 427.82 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:23293561235200] 769.26 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:23293559133952] 1171.80 ms (1 s 171.80 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:23293557032704] 1660.21 ms (1 s 660.21 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:23291876079360] 2333.29 ms (2 s 333.29 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:23291873978112] 3216.50 ms (3 s 216.50 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:23291871876864] 4394.13 ms (4 s 394.13 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:23291869775616] 4830.18 ms (4 s 830.18 ms) total read duration. Loaded 31 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 9370676 representatives in total. Sat Oct 14 12:39:14 2023: Inserted ≈ 5% of D-proof conclusions. [ 468533 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 597.26 ms remaining ; 3 s 786.59 ms total) Sat Oct 14 12:39:14 2023: Inserted ≈10% of D-proof conclusions. [ 937067 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 495.35 ms remaining ; 3 s 883.72 ms total) Sat Oct 14 12:39:15 2023: Inserted ≈15% of D-proof conclusions. [1405601 of 9370676] (ETC: Sat Oct 14 12:39:18 2023 ; 3 s 398.96 ms remaining ; 3 s 998.78 ms total) Sat Oct 14 12:39:15 2023: Inserted ≈20% of D-proof conclusions. [1874135 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 832.32 ms remaining ; 4 s 790.40 ms total) Sat Oct 14 12:39:15 2023: Inserted ≈25% of D-proof conclusions. [2342669 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 634.73 ms remaining ; 4 s 846.31 ms total) Sat Oct 14 12:39:15 2023: Inserted ≈30% of D-proof conclusions. [2811202 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 300.64 ms remaining ; 4 s 715.20 ms total) Sat Oct 14 12:39:16 2023: Inserted ≈35% of D-proof conclusions. [3279736 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 3 s 50.37 ms remaining ; 4 s 692.87 ms total) Sat Oct 14 12:39:16 2023: Inserted ≈40% of D-proof conclusions. [3748270 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 873.70 ms remaining ; 4 s 789.49 ms total) Sat Oct 14 12:39:16 2023: Inserted ≈45% of D-proof conclusions. [4216804 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 722.34 ms remaining ; 4 s 949.71 ms total) Sat Oct 14 12:39:17 2023: Inserted ≈50% of D-proof conclusions. [4685338 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 612.65 ms remaining ; 5 s 225.31 ms total) Sat Oct 14 12:39:17 2023: Inserted ≈55% of D-proof conclusions. [5153871 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 352.83 ms remaining ; 5 s 228.51 ms total) Sat Oct 14 12:39:17 2023: Inserted ≈60% of D-proof conclusions. [5622405 of 9370676] (ETC: Sat Oct 14 12:39:19 2023 ; 2 s 146.79 ms remaining ; 5 s 366.98 ms total) Sat Oct 14 12:39:18 2023: Inserted ≈65% of D-proof conclusions. [6090939 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 921.27 ms remaining ; 5 s 489.35 ms total) Sat Oct 14 12:39:18 2023: Inserted ≈70% of D-proof conclusions. [6559473 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 641.58 ms remaining ; 5 s 471.93 ms total) Sat Oct 14 12:39:18 2023: Inserted ≈75% of D-proof conclusions. [7028007 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 365.27 ms remaining ; 5 s 461.07 ms total) Sat Oct 14 12:39:18 2023: Inserted ≈80% of D-proof conclusions. [7496540 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 1 s 98.14 ms remaining ; 5 s 490.72 ms total) Sat Oct 14 12:39:19 2023: Inserted ≈85% of D-proof conclusions. [7965074 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 827.06 ms remaining ; 5 s 513.71 ms total) Sat Oct 14 12:39:19 2023: Inserted ≈90% of D-proof conclusions. [8433608 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 565.32 ms remaining ; 5 s 653.22 ms total) Sat Oct 14 12:39:20 2023: Inserted ≈95% of D-proof conclusions. [8902142 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 302.70 ms remaining ; 6 s 53.95 ms total) Sat Oct 14 12:39:20 2023: Inserted 100% of D-proof conclusions. [9370676 of 9370676] (ETC: Sat Oct 14 12:39:20 2023 ; 0.00 ms remaining ; 6 s 128.35 ms total) 6128.59 ms (6 s 128.59 ms) total insertion duration. Sat Oct 14 12:39:20 2023: Starting to iterate D-proof candidates of length 63. 86461.54 ms (1 min 26 s 461.54 ms) taken to iterate 130626396 condensed detachment proof strings of length 63. [Copy] Next iteration count (filtered): { 63, 130626396 } Sat Oct 14 12:40:47 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sat Oct 14 12:41:03 2023: Process terminated. [pid: 245717, tid:23293669812096]