( This log file was generated by executing 'pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40493663 optane_low 64 COMPLETED 0:0 00:58:37 40493663.ba+ 64 COMPLETED 0:0 00:58:37 355670196K 40493663.ex+ 64 COMPLETED 0:0 00:58:37 0 By 355670196 KiB = (355670196 / 1024^2) GiB = 339.193531036376953125 GiB, it used approximately 339.19 gibibytes of memory. ) Thu Nov 2 02:21:09 2023: Process started. [pid: 28930, tid:22774479628160] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed] (1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0)) [Main] Calling countNextIterationAmount(false, true). Thu Nov 2 02:21:09 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.04 ms taken to load initial representatives. 18.60 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22774419379968] 22.89 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22774417278720] 23.82 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22774415177472] 19.43 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22774413076224] 15.12 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22774410974976] 27.27 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22774408873728] 28.40 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22774406772480] 26.37 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22774404671232] 23.84 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22774402569984] 21.50 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22774332520192] 29.21 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22774330418944] 29.84 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22774328317696] 33.38 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22774326216448] 11.76 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22774324115200] 324.62 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22774322013952] 44.82 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22774319912704] 54.96 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22774317811456] 106.01 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22774315710208] 60.75 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22774313608960] 226.85 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22774311507712] 186.41 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22774309406464] 111.01 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22774307305216] 294.76 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22774305203968] 768.52 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22774303102720] 767.52 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22774301001472] 1056.02 ms (1 s 56.02 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22774298900224] 4096.39 ms (4 s 96.39 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22774296798976] 3482.34 ms (3 s 482.34 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22774294697728] 2212.19 ms (2 s 212.19 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22774292596480] 2841.20 ms (2 s 841.20 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22774290495232] 4503.88 ms (4 s 503.88 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22774288393984] 4672.58 ms (4 s 672.58 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22774286292736] 5841.34 ms (5 s 841.34 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22774284191488] 7242.78 ms (7 s 242.78 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22774282090240] 7326.09 ms (7 s 326.10 ms) total read duration. Loaded 35 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 7 11 : 10 13 : 13 15 : 19 17 : 37 19 : 56 21 : 87 23 : 140 25 : 227 27 : 369 29 : 579 31 : 918 33 : 1499 35 : 2408 37 : 3881 39 : 6254 41 : 10109 43 : 16460 45 : 26753 47 : 43360 49 : 70709 51 : 115604 53 : 188634 55 : 308241 57 : 504870 59 : 827701 61 : 1357539 63 : 2227822 65 : 3660735 67 : 6021110 69 : 9907537 25303694 representatives in total. 35712.72 ms (35 s 712.72 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22774282090240] 58890.09 ms (58 s 890.09 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22774284191488] 79554.91 ms (1 min 19 s 554.91 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22774286292736] 107561.71 ms (1 min 47 s 561.71 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:22774288393984] 144404.17 ms (2 min 24 s 404.17 ms) taken to read 263540491 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. [tid:22774290495232] 144572.03 ms (2 min 24 s 572.03 ms) additional read duration. Loaded 5 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 77 : 143296899 79 : 263540491 580590052 representatives in total. Thu Nov 2 02:24:19 2023: Inserted ≈ 5% of D-proof conclusions. [ 29029502 of 580590052] (ETC: Thu Nov 2 02:36:11 2023 ; 11 min 52 s 468.04 ms remaining ; 12 min 29 s 966.36 ms total) Thu Nov 2 02:25:02 2023: Inserted ≈10% of D-proof conclusions. [ 58059005 of 580590052] (ETC: Thu Nov 2 02:37:12 2023 ; 12 min 9 s 953.49 ms remaining ; 13 min 31 s 59.43 ms total) Thu Nov 2 02:25:48 2023: Inserted ≈15% of D-proof conclusions. [ 87088507 of 580590052] (ETC: Thu Nov 2 02:37:49 2023 ; 12 min 977.25 ms remaining ; 14 min 8 s 208.53 ms total) Thu Nov 2 02:26:24 2023: Inserted ≈20% of D-proof conclusions. [116118010 of 580590052] (ETC: Thu Nov 2 02:37:16 2023 ; 10 min 51 s 847.79 ms remaining ; 13 min 34 s 809.74 ms total) Thu Nov 2 02:27:05 2023: Inserted ≈25% of D-proof conclusions. [145147513 of 580590052] (ETC: Thu Nov 2 02:37:18 2023 ; 10 min 12 s 748.83 ms remaining ; 13 min 36 s 998.44 ms total) Thu Nov 2 02:27:49 2023: Inserted ≈30% of D-proof conclusions. [174177015 of 580590052] (ETC: Thu Nov 2 02:37:28 2023 ; 9 min 38 s 946.02 ms remaining ; 13 min 47 s 65.74 ms total) Thu Nov 2 02:28:18 2023: Inserted ≈35% of D-proof conclusions. [203206518 of 580590052] (ETC: Thu Nov 2 02:36:53 2023 ; 8 min 34 s 884.78 ms remaining ; 13 min 12 s 130.43 ms total) Thu Nov 2 02:28:50 2023: Inserted ≈40% of D-proof conclusions. [232236020 of 580590052] (ETC: Thu Nov 2 02:36:34 2023 ; 7 min 43 s 883.95 ms remaining ; 12 min 53 s 139.91 ms total) Thu Nov 2 02:29:25 2023: Inserted ≈45% of D-proof conclusions. [261265523 of 580590052] (ETC: Thu Nov 2 02:36:26 2023 ; 7 min 619.31 ms remaining ; 12 min 44 s 762.38 ms total) Thu Nov 2 02:30:03 2023: Inserted ≈50% of D-proof conclusions. [290295026 of 580590052] (ETC: Thu Nov 2 02:36:24 2023 ; 6 min 21 s 633.13 ms remaining ; 12 min 43 s 266.26 ms total) Thu Nov 2 02:30:39 2023: Inserted ≈55% of D-proof conclusions. [319324528 of 580590052] (ETC: Thu Nov 2 02:36:20 2023 ; 5 min 41 s 719.43 ms remaining ; 12 min 39 s 376.51 ms total) Thu Nov 2 02:31:02 2023: Inserted ≈60% of D-proof conclusions. [348354031 of 580590052] (ETC: Thu Nov 2 02:35:56 2023 ; 4 min 53 s 923.33 ms remaining ; 12 min 14 s 808.32 ms total) Thu Nov 2 02:31:25 2023: Inserted ≈65% of D-proof conclusions. [377383533 of 580590052] (ETC: Thu Nov 2 02:35:35 2023 ; 4 min 10 s 26.59 ms remaining ; 11 min 54 s 361.68 ms total) Thu Nov 2 02:31:50 2023: Inserted ≈70% of D-proof conclusions. [406413036 of 580590052] (ETC: Thu Nov 2 02:35:20 2023 ; 3 min 29 s 665.72 ms remaining ; 11 min 38 s 885.74 ms total) Thu Nov 2 02:32:16 2023: Inserted ≈75% of D-proof conclusions. [435442539 of 580590052] (ETC: Thu Nov 2 02:35:07 2023 ; 2 min 51 s 558.50 ms remaining ; 11 min 26 s 233.99 ms total) Thu Nov 2 02:32:42 2023: Inserted ≈80% of D-proof conclusions. [464472041 of 580590052] (ETC: Thu Nov 2 02:34:57 2023 ; 2 min 15 s 256.89 ms remaining ; 11 min 16 s 284.46 ms total) Thu Nov 2 02:33:09 2023: Inserted ≈85% of D-proof conclusions. [493501544 of 580590052] (ETC: Thu Nov 2 02:34:50 2023 ; 1 min 40 s 283.44 ms remaining ; 11 min 8 s 556.25 ms total) Thu Nov 2 02:33:44 2023: Inserted ≈90% of D-proof conclusions. [522531046 of 580590052] (ETC: Thu Nov 2 02:34:51 2023 ; 1 min 6 s 962.76 ms remaining ; 11 min 9 s 627.62 ms total) Thu Nov 2 02:34:27 2023: Inserted ≈95% of D-proof conclusions. [551560549 of 580590052] (ETC: Thu Nov 2 02:35:01 2023 ; 34 s 5.51 ms remaining ; 11 min 20 s 110.13 ms total) Thu Nov 2 02:35:12 2023: Inserted 100% of D-proof conclusions. [580590052 of 580590052] (ETC: Thu Nov 2 02:35:12 2023 ; 0.00 ms remaining ; 11 min 30 s 939.62 ms total) 690940.87 ms (11 min 30 s 940.87 ms) total insertion duration. Thu Nov 2 02:35:12 2023: Starting to iterate D-proof candidates of length 81. 1876662.74 ms (31 min 16 s 662.74 ms) taken to iterate 3720990150 condensed detachment proof strings of length 81. [Copy] Next iteration count (unfiltered71+): { 81, 3720990150 } Thu Nov 2 03:06:40 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Thu Nov 2 03:19:21 2023: Process terminated. [pid: 28930, tid:22774479628160]