( This log file was generated by 'pmGenerator 1.2.3' (master branch), compiled by 'oneAPI DPC++/C++ Compiler 2024.2.0 (2024.2.0.20240602)'. The run was executed on 60 CLAIX-2023 MPI (small) nodes — 2-socket Intel Xeon Platinum 8468 (Sapphire Rapids) each, 48 cores each (96 cores total per node), 2.1 GHz, 3.8 GHz turbo mode, 256 GiB main memory each — running Linux, Rocky 9.6. Initialization and completion messages with rank numbers have been grouped and sorted for better readability. Wall-clock time: 5.4208333… h CPU utilization: 31224 core-h ) Wed May 27 05:58:09 2026: Process started. [pid: 252939, tid:22387064035136] Wed May 27 05:58:09 2026: Process started. [pid: 421234, tid:22945509177152] Wed May 27 05:58:09 2026: Process started. [pid: 98065, tid:22684925830976] Wed May 27 05:58:09 2026: Process started. [pid: 295697, tid:22620559423296] Wed May 27 05:58:09 2026: Process started. [pid: 239466, tid:22858953414464] Wed May 27 05:58:09 2026: Process started. [pid: 42934, tid:22399405066048] Wed May 27 05:58:09 2026: Process started. [pid: 109768, tid:22795969865536] Wed May 27 05:58:09 2026: Process started. [pid: 470584, tid:23232187516736] Wed May 27 05:58:09 2026: Process started. [pid: 211059, tid:22644595570496] Wed May 27 05:58:09 2026: Process started. [pid: 189383, tid:23183005103936] Wed May 27 05:58:09 2026: Process started. [pid: 235590, tid:23331374458688] Wed May 27 05:58:09 2026: Process started. [pid: 336196, tid:23139116201792] Wed May 27 05:58:09 2026: Process started. [pid: 159269, tid:22944517572416] Wed May 27 05:58:10 2026: Process started. [pid: 111565, tid:23325611513664] Wed May 27 05:58:10 2026: Process started. [pid: 27002, tid:22657289389888] Wed May 27 05:58:10 2026: Process started. [pid: 426832, tid:22441819875136] Wed May 27 05:58:10 2026: Process started. [pid: 220292, tid:22683767940928] Wed May 27 05:58:10 2026: Process started. [pid: 363674, tid:23181355210560] Wed May 27 05:58:10 2026: Process started. [pid: 264392, tid:22528627033920] Wed May 27 05:58:10 2026: Process started. [pid: 473626, tid:23328554141504] Wed May 27 05:58:10 2026: Process started. [pid: 354299, tid:22960185407296] Wed May 27 05:58:10 2026: Process started. [pid: 324661, tid:23103244752704] Wed May 27 05:58:10 2026: Process started. [pid: 467418, tid:23386152425280] Wed May 27 05:58:10 2026: Process started. [pid: 31894, tid:22372026296128] Wed May 27 05:58:10 2026: Process started. [pid: 142112, tid:22359552464704] Wed May 27 05:58:10 2026: Process started. [pid: 478820, tid:23007394105152] Wed May 27 05:58:10 2026: Process started. [pid: 326600, tid:23014486386496] Wed May 27 05:58:10 2026: Process started. [pid: 85677, tid:22764208592704] Wed May 27 05:58:10 2026: Process started. [pid: 292791, tid:22949524375360] Wed May 27 05:58:10 2026: Process started. [pid: 438553, tid:22839695275840] Wed May 27 05:58:10 2026: Process started. [pid: 73622, tid:23301953996608] Wed May 27 05:58:10 2026: Process started. [pid: 487098, tid:22752210638656] Wed May 27 05:58:10 2026: Process started. [pid: 190681, tid:22895047685952] Wed May 27 05:58:10 2026: Process started. [pid: 488908, tid:23433115694912] Wed May 27 05:58:10 2026: Process started. [pid: 202233, tid:23117100590912] Wed May 27 05:58:10 2026: Process started. [pid: 76311, tid:23186291349312] Wed May 27 05:58:10 2026: Process started. [pid: 74177, tid:23259459561280] Wed May 27 05:58:10 2026: Process started. [pid: 345775, tid:23044784551744] Wed May 27 05:58:10 2026: Process started. [pid: 380980, tid:22891160422208] Wed May 27 05:58:10 2026: Process started. [pid: 407040, tid:22758912759616] Wed May 27 05:58:10 2026: Process started. [pid: 188570, tid:23155983918912] Wed May 27 05:58:10 2026: Process started. [pid: 84916, tid:22513781151552] Wed May 27 05:58:10 2026: Process started. [pid: 250203, tid:23268499871552] Wed May 27 05:58:10 2026: Process started. [pid: 73933, tid:23077049411392] Wed May 27 05:58:10 2026: Process started. [pid: 105685, tid:23108085061440] Wed May 27 05:58:10 2026: Process started. [pid: 217084, tid:22869067880256] Wed May 27 05:58:10 2026: Process started. [pid: 123953, tid:22435408873280] Wed May 27 05:58:10 2026: Process started. [pid: 80595, tid:23241308354368] Wed May 27 05:58:10 2026: Process started. [pid: 60628, tid:22432405464896] Wed May 27 05:58:10 2026: Process started. [pid: 420569, tid:23021549807424] Wed May 27 05:58:10 2026: Process started. [pid: 82782, tid:22567948244800] Wed May 27 05:58:10 2026: Process started. [pid: 21560, tid:23065837856576] Wed May 27 05:58:10 2026: Process started. [pid: 441002, tid:23063100802880] Wed May 27 05:58:10 2026: Process started. [pid: 21198, tid:23140739106624] Wed May 27 05:58:10 2026: Process started. [pid: 437792, tid:23109550405440] Wed May 27 05:58:10 2026: Process started. [pid: 391958, tid:22703636006720] Wed May 27 05:58:10 2026: Process started. [pid: 350478, tid:23205581510464] Wed May 27 05:58:10 2026: Process started. [pid: 94026, tid:23173136099136] Wed May 27 05:58:10 2026: Process started. [pid: 513786, tid:22585644275520] Wed May 27 05:58:10 2026: Process started. [pid: 334834, tid:22884542756672] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true) 2. mpi_filterDProofRepresentativeFile(83, true) [Rank 0 ; pid: 350478 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Rank 1 ; pid: 295697 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 2 ; pid: 217084 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 3 ; pid: 324661 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 4 ; pid: 211059 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 5 ; pid: 478820 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 6 ; pid: 202233 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 7 ; pid: 239466 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 8 ; pid: 354299 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 9 ; pid: 31894 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 10 ; pid: 345775 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 11 ; pid: 27002 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 12 ; pid: 84916 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 13 ; pid: 470584 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 14 ; pid: 159269 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 15 ; pid: 363674 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 16 ; pid: 190681 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 17 ; pid: 488908 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 18 ; pid: 292791 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 19 ; pid: 98065 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 20 ; pid: 189383 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 21 ; pid: 42934 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 22 ; pid: 336196 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 23 ; pid: 437792 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 24 ; pid: 76311 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 25 ; pid: 426832 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 26 ; pid: 391958 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 27 ; pid: 441002 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 28 ; pid: 21560 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 29 ; pid: 80595 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 30 ; pid: 326600 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 31 ; pid: 74177 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 32 ; pid: 21198 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 33 ; pid: 73933 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 34 ; pid: 188570 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 35 ; pid: 82782 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 36 ; pid: 334834 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 37 ; pid: 60628 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 38 ; pid: 142112 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 39 ; pid: 250203 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 40 ; pid: 220292 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 41 ; pid: 94026 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 42 ; pid: 264392 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 43 ; pid: 473626 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 44 ; pid: 85677 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 45 ; pid: 380980 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 46 ; pid: 73622 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 47 ; pid: 421234 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 48 ; pid: 111565 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 49 ; pid: 487098 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 50 ; pid: 252939 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 51 ; pid: 513786 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 52 ; pid: 467418 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 53 ; pid: 438553 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 54 ; pid: 420569 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 55 ; pid: 407040 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 56 ; pid: 105685 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 57 ; pid: 123953 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 58 ; pid: 235590 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 59 ; pid: 109768 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently. [Rank 0 ; pid: 350478 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 1 ; pid: 295697 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 2 ; pid: 217084 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 3 ; pid: 324661 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 4 ; pid: 211059 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 5 ; pid: 478820 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 6 ; pid: 202233 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 7 ; pid: 239466 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 8 ; pid: 354299 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 9 ; pid: 31894 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 10 ; pid: 345775 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 11 ; pid: 27002 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 12 ; pid: 84916 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 13 ; pid: 470584 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 14 ; pid: 159269 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 15 ; pid: 363674 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 16 ; pid: 190681 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 17 ; pid: 488908 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 18 ; pid: 292791 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 19 ; pid: 98065 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 20 ; pid: 189383 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 21 ; pid: 42934 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 22 ; pid: 336196 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 23 ; pid: 437792 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 24 ; pid: 76311 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 25 ; pid: 426832 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 26 ; pid: 391958 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 27 ; pid: 441002 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 28 ; pid: 21560 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 29 ; pid: 80595 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 30 ; pid: 326600 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 31 ; pid: 74177 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 32 ; pid: 21198 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 33 ; pid: 73933 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 34 ; pid: 188570 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 35 ; pid: 82782 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 36 ; pid: 334834 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 37 ; pid: 60628 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 38 ; pid: 142112 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 39 ; pid: 250203 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 40 ; pid: 220292 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 41 ; pid: 94026 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 42 ; pid: 264392 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 43 ; pid: 473626 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 44 ; pid: 85677 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 45 ; pid: 380980 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 46 ; pid: 73622 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 47 ; pid: 421234 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 48 ; pid: 111565 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 49 ; pid: 487098 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 50 ; pid: 252939 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 51 ; pid: 513786 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 52 ; pid: 467418 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 53 ; pid: 438553 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 54 ; pid: 420569 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 55 ; pid: 407040 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 56 ; pid: 105685 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 57 ; pid: 123953 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 58 ; pid: 235590 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). [Rank 59 ; pid: 109768 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true). Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 0 on "n23m0024.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 1 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 2 on "n23m0030.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 3 on "n23m0040.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 4 on "n23m0042.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 5 on "n23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 6 on "n23m0046.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 7 on "n23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 8 on "n23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 9 on "n23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 10 on "n23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 11 on "n23m0068.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 12 on "n23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 13 on "n23m0076.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 14 on "n23m0078.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 15 on "n23m0093.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 16 on "n23m0096.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 17 on "n23m0100.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 18 on "n23m0124.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 19 on "n23m0140.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 20 on "n23m0147.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 21 on "n23m0152.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 22 on "n23m0154.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 23 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 24 on "n23m0176.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 25 on "n23m0180.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 26 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 27 on "n23m0183.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 28 on "n23m0184.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 29 on "n23m0185.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 30 on "n23m0190.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 31 on "n23m0195.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 32 on "n23m0196.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 33 on "n23m0205.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 34 on "n23m0212.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 35 on "n23m0215.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 36 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 37 on "n23m0238.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 38 on "n23m0244.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 39 on "n23m0245.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 40 on "n23m0246.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 41 on "n23m0249.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 42 on "n23m0251.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 43 on "n23m0252.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 44 on "n23m0254.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 45 on "n23m0256.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 46 on "n23m0260.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 47 on "n23m0261.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 48 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 49 on "n23m0264.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 50 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 51 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 52 on "n23m0314.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 53 on "n23m0318.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 54 on "n23m0320.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 55 on "n23m0322.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 56 on "n23m0341.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 57 on "r23m0075.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 58 on "r23m0112.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 05:58:11 2026: MPI-based D-proof representative filter started. [rank 59 on "r23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] 0.00 ms taken to load initial representatives. 2.62 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs3.txt. [tid:23205309826624] 0.02 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs5.txt. [tid:23205184001600] 8.60 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs7.txt. [tid:23205047682624] 4.09 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs9.txt. [tid:23204911363648] 27.89 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs11.txt. [tid:23205181900352] 2.87 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs13.txt. [tid:23205179799104] 1.27 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs15.txt. [tid:23205177697856] 4.45 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs17.txt. [tid:23205175596608] 1.70 ms taken to read 65 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs19.txt. [tid:23205104318016] 6.60 ms taken to read 98 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs21.txt. [tid:23205102216768] 19.68 ms taken to read 135 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs23.txt. [tid:23205100115520] 8.83 ms taken to read 197 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs25.txt. [tid:23205098014272] 3.29 ms taken to read 270 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs27.txt. [tid:23205095913024] 5.90 ms taken to read 388 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs29.txt. [tid:23205093811776] 25.68 ms taken to read 551 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs31.txt. [tid:23205091710528] 19.89 ms taken to read 783 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs33.txt. [tid:23205089609280] 9.38 ms taken to read 1106 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs35.txt. [tid:23205087508032] 10.38 ms taken to read 1563 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs37.txt. [tid:23205085406784] 18.29 ms taken to read 2211 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs39.txt. [tid:23205083305536] 25.86 ms taken to read 3116 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs41.txt. [tid:23205081204288] 10.91 ms taken to read 4400 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs43.txt. [tid:23205079103040] 11.74 ms taken to read 6223 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs45.txt. [tid:23205077001792] 14.82 ms taken to read 8774 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs47.txt. [tid:23205074900544] 29.60 ms taken to read 12413 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs49.txt. [tid:23205072799296] 21.00 ms taken to read 17529 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs51.txt. [tid:23205070698048] 83.15 ms taken to read 24829 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs53.txt. [tid:23205068596800] 145.17 ms taken to read 35088 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs55.txt. [tid:23205066495552] 48.58 ms taken to read 49805 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs57.txt. [tid:23205064394304] 71.00 ms taken to read 70539 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs59.txt. [tid:23205062293056] 119.49 ms taken to read 100323 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs61.txt. [tid:23205060191808] 142.41 ms taken to read 142420 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs63.txt. [tid:23205058090560] 216.19 ms taken to read 202794 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs65.txt. [tid:23205055989312] 205.89 ms taken to read 288534 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs67.txt. [tid:23205053888064] 295.59 ms taken to read 411654 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs69.txt. [tid:23205051786816] 505.51 ms taken to read 586547 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs71.txt. [tid:23205045581376] 736.63 ms taken to read 837981 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs73.txt. [tid:23205043480128] 771.61 ms taken to read 1196203 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs75.txt. [tid:23205041378880] 1940.14 ms (1 s 940.14 ms) taken to read 1710627 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs77.txt. [tid:23204970100288] 1714.08 ms (1 s 714.08 ms) taken to read 2444582 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs79.txt. [tid:23204967999040] 2422.00 ms (2 s 422.00 ms) taken to read 3499861 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81.txt. [tid:23204965897792] 2456.71 ms (2 s 456.71 ms) total read duration. Loaded 41 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 65 21 : 98 23 : 135 25 : 197 27 : 270 29 : 388 31 : 551 33 : 783 35 : 1106 37 : 1563 39 : 2211 41 : 3116 43 : 4400 45 : 6223 47 : 8774 49 : 12413 51 : 17529 53 : 24829 55 : 35088 57 : 49805 59 : 70539 61 : 100323 63 : 142420 65 : 202794 67 : 288534 69 : 411654 71 : 586547 73 : 837981 75 : 1196203 77 : 1710627 79 : 2444582 81 : 3499861 11661731 representatives in total. 14366.37 ms (14 s 366.37 ms) taken to read 47493930 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23204965897792] 14368.33 ms (14 s 368.33 ms) additional read duration. Loaded 1 more representative collection of size: 83 : 47493930 59155661 representatives in total. Wed May 27 05:58:30 2026: Representative collections were initialized successfully on all ranks. Estimated removal count set to 42473187, based on entry 81:29247374 and last known pair (79:20139974, 81:29247374) with 29247374/20139974 ≈ 1.45221 and 29247374 * (29247374/20139974)^1 ≈ 42473187.20. Wed May 27 05:58:32 2026: Inserted ≈ 5% of D-proof conclusions. [ 2957783 of 59155661] (ETC: Wed May 27 05:58:54 2026 ; 22 s 548.50 ms remaining ; 23 s 735.26 ms total) Wed May 27 05:58:33 2026: Inserted ≈10% of D-proof conclusions. [ 5915566 of 59155661] (ETC: Wed May 27 05:58:55 2026 ; 22 s 464.54 ms remaining ; 24 s 960.60 ms total) Wed May 27 05:58:34 2026: Inserted ≈15% of D-proof conclusions. [ 8873349 of 59155661] (ETC: Wed May 27 05:58:56 2026 ; 21 s 616.13 ms remaining ; 25 s 430.74 ms total) Wed May 27 05:58:36 2026: Inserted ≈20% of D-proof conclusions. [11831132 of 59155661] (ETC: Wed May 27 05:58:56 2026 ; 20 s 634.14 ms remaining ; 25 s 792.68 ms total) Wed May 27 05:58:36 2026: Inserted ≈25% of D-proof conclusions. [14788915 of 59155661] (ETC: Wed May 27 05:58:53 2026 ; 17 s 184.92 ms remaining ; 22 s 913.23 ms total) Wed May 27 05:58:37 2026: Inserted ≈30% of D-proof conclusions. [17746698 of 59155661] (ETC: Wed May 27 05:58:52 2026 ; 14 s 748.55 ms remaining ; 21 s 69.35 ms total) Wed May 27 05:58:37 2026: Inserted ≈35% of D-proof conclusions. [20704481 of 59155661] (ETC: Wed May 27 05:58:50 2026 ; 12 s 813.05 ms remaining ; 19 s 712.39 ms total) Wed May 27 05:58:38 2026: Inserted ≈40% of D-proof conclusions. [23662264 of 59155661] (ETC: Wed May 27 05:58:49 2026 ; 11 s 208.40 ms remaining ; 18 s 680.67 ms total) Wed May 27 05:58:39 2026: Inserted ≈45% of D-proof conclusions. [26620047 of 59155661] (ETC: Wed May 27 05:58:48 2026 ; 9 s 832.18 ms remaining ; 17 s 876.69 ms total) Wed May 27 05:58:39 2026: Inserted ≈50% of D-proof conclusions. [29577830 of 59155661] (ETC: Wed May 27 05:58:48 2026 ; 8 s 604.32 ms remaining ; 17 s 208.63 ms total) Wed May 27 05:58:40 2026: Inserted ≈55% of D-proof conclusions. [32535613 of 59155661] (ETC: Wed May 27 05:58:47 2026 ; 7 s 496.41 ms remaining ; 16 s 658.69 ms total) Wed May 27 05:58:40 2026: Inserted ≈60% of D-proof conclusions. [35493396 of 59155661] (ETC: Wed May 27 05:58:47 2026 ; 6 s 525.56 ms remaining ; 16 s 313.89 ms total) Wed May 27 05:58:41 2026: Inserted ≈65% of D-proof conclusions. [38451179 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 5 s 585.28 ms remaining ; 15 s 957.95 ms total) Wed May 27 05:58:42 2026: Inserted ≈70% of D-proof conclusions. [41408962 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 4 s 713.83 ms remaining ; 15 s 712.77 ms total) Wed May 27 05:58:42 2026: Inserted ≈75% of D-proof conclusions. [44366745 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 3 s 912.01 ms remaining ; 15 s 648.03 ms total) Wed May 27 05:58:43 2026: Inserted ≈80% of D-proof conclusions. [47324528 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 3 s 106.96 ms remaining ; 15 s 534.78 ms total) Wed May 27 05:58:44 2026: Inserted ≈85% of D-proof conclusions. [50282311 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 2 s 323.32 ms remaining ; 15 s 488.81 ms total) Wed May 27 05:58:44 2026: Inserted ≈90% of D-proof conclusions. [53240094 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 1 s 547.22 ms remaining ; 15 s 472.19 ms total) Wed May 27 05:58:45 2026: Inserted ≈95% of D-proof conclusions. [56197877 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 771.00 ms remaining ; 15 s 420.00 ms total) Wed May 27 05:58:46 2026: Inserted 100% of D-proof conclusions. [59155661 of 59155661] (ETC: Wed May 27 05:58:46 2026 ; 0.00 ms remaining ; 15 s 275.89 ms total) 15276.26 ms (15 s 276.26 ms) total insertion duration. Reservable workloads: { 0:[527710, 791564], 1:[1319276, 1583130], 2:[2110841, 2374695], 3:[2902407, 3166261], 4:[3693972, 3957826], 5:[4485538, 4749392], 6:[5277103, 5540957], 7:[6068669, 6332523], 8:[6860234, 7124088], 9:[7651800, 7915654], 10:[8443365, 8707219], 11:[9234931, 9498785], 12:[10026496, 10290350], 13:[10818062, 11081916], 14:[11609627, 11873481], 15:[12401193, 12665047], 16:[13192758, 13456612], 17:[13984324, 14248178], 18:[14775889, 15039743], 19:[15567455, 15831309], 20:[16359020, 16622874], 21:[17150586, 17414440], 22:[17942151, 18206005], 23:[18733717, 18997571], 24:[19525282, 19789136], 25:[20316848, 20580702], 26:[21108413, 21372267], 27:[21899979, 22163833], 28:[22691544, 22955398], 29:[23483110, 23746964], 30:[24274675, 24538529], 31:[25066241, 25330095], 32:[25857806, 26121660], 33:[26649372, 26913226], 34:[27440937, 27704791], 35:[28232503, 28496357], 36:[29024068, 29287922], 37:[29815634, 30079488], 38:[30607199, 30871053], 39:[31398765, 31662619], 40:[32190330, 32454184], 41:[32981896, 33245750], 42:[33773461, 34037315], 43:[34565027, 34828881], 44:[35356592, 35620446], 45:[36148158, 36412012], 46:[36939723, 37203577], 47:[37731289, 37995143], 48:[38522854, 38786708], 49:[39314420, 39578274], 50:[40105985, 40369839], 51:[40897551, 41161405], 52:[41689116, 41952970], 53:[42480682, 42744536], 54:[43272247, 43536101], 55:[44063813, 44327667], 56:[44855378, 45119232], 57:[45646944, 45910798], 58:[46438509, 46702363], 59:[47230075, 47493929] } Wed May 27 06:05:34 2026: Removed ≈ 2% of redundant conclusions. [ 849463 of approximately 42473187] (ETC: Wed May 27 11:36:30 2026 ; 5 h 30 min 55 s 939.41 ms remaining ; 5 h 37 min 41 s 162.30 ms total) Wed May 27 06:12:20 2026: Removed ≈ 4% of redundant conclusions. [ 1698927 of approximately 42473187] (ETC: Wed May 27 11:36:32 2026 ; 5 h 24 min 12 s 273.80 ms remaining ; 5 h 37 min 42 s 784.97 ms total) Wed May 27 06:19:07 2026: Removed ≈ 6% of redundant conclusions. [ 2548391 of approximately 42473187] (ETC: Wed May 27 11:37:10 2026 ; 5 h 18 min 2 s 978.08 ms remaining ; 5 h 38 min 21 s 40.40 ms total) Wed May 27 06:25:53 2026: Removed ≈ 8% of redundant conclusions. [ 3397854 of approximately 42473187] (ETC: Wed May 27 11:37:05 2026 ; 5 h 11 min 12 s 77.77 ms remaining ; 5 h 38 min 15 s 736.21 ms total) Wed May 27 06:32:38 2026: Removed ≈ 10% of redundant conclusions. [ 4247318 of approximately 42473187] (ETC: Wed May 27 11:37:00 2026 ; 5 h 4 min 21 s 900.44 ms remaining ; 5 h 38 min 11 s 0.11 ms total) Wed May 27 06:39:25 2026: Removed ≈ 12% of redundant conclusions. [ 5096782 of approximately 42473187] (ETC: Wed May 27 11:37:07 2026 ; 4 h 57 min 41 s 837.54 ms remaining ; 5 h 38 min 17 s 542.42 ms total) Wed May 27 06:46:13 2026: Removed ≈ 14% of redundant conclusions. [ 5946246 of approximately 42473187] (ETC: Wed May 27 11:37:20 2026 ; 4 h 51 min 7 s 154.12 ms remaining ; 5 h 38 min 30 s 644.23 ms total) Wed May 27 06:52:56 2026: Removed ≈ 16% of redundant conclusions. [ 6795709 of approximately 42473187] (ETC: Wed May 27 11:37:01 2026 ; 4 h 44 min 5 s 200.35 ms remaining ; 5 h 38 min 11 s 904.65 ms total) Wed May 27 06:59:42 2026: Removed ≈ 18% of redundant conclusions. [ 7645173 of approximately 42473187] (ETC: Wed May 27 11:37:01 2026 ; 4 h 37 min 19 s 286.45 ms remaining ; 5 h 38 min 11 s 812.36 ms total) Wed May 27 07:06:25 2026: Removed ≈ 20% of redundant conclusions. [ 8494637 of approximately 42473187] (ETC: Wed May 27 11:36:49 2026 ; 4 h 30 min 24 s 203.76 ms remaining ; 5 h 38 min 254.46 ms total) Wed May 27 07:13:09 2026: Removed ≈ 22% of redundant conclusions. [ 9344101 of approximately 42473187] (ETC: Wed May 27 11:36:40 2026 ; 4 h 23 min 31 s 59.01 ms remaining ; 5 h 37 min 50 s 588.38 ms total) Wed May 27 07:19:51 2026: Removed ≈ 24% of redundant conclusions. [10193564 of approximately 42473187] (ETC: Wed May 27 11:36:28 2026 ; 4 h 16 min 36 s 384.08 ms remaining ; 5 h 37 min 38 s 399.56 ms total) Wed May 27 07:26:35 2026: Removed ≈ 26% of redundant conclusions. [11043028 of approximately 42473187] (ETC: Wed May 27 11:36:22 2026 ; 4 h 9 min 47 s 34.70 ms remaining ; 5 h 37 min 32 s 749.19 ms total) Wed May 27 07:33:18 2026: Removed ≈ 28% of redundant conclusions. [11892492 of approximately 42473187] (ETC: Wed May 27 11:36:14 2026 ; 4 h 2 min 55 s 981.99 ms remaining ; 5 h 37 min 24 s 419.19 ms total) Wed May 27 07:39:59 2026: Removed ≈ 30% of redundant conclusions. [12741956 of approximately 42473187] (ETC: Wed May 27 11:36:02 2026 ; 3 h 56 min 2 s 780.77 ms remaining ; 5 h 37 min 12 s 543.88 ms total) Wed May 27 07:46:38 2026: Removed ≈ 32% of redundant conclusions. [13591419 of approximately 42473187] (ETC: Wed May 27 11:35:46 2026 ; 3 h 49 min 7 s 392.90 ms remaining ; 5 h 36 min 56 s 753.68 ms total) Wed May 27 07:53:17 2026: Removed ≈ 34% of redundant conclusions. [14440883 of approximately 42473187] (ETC: Wed May 27 11:35:28 2026 ; 3 h 42 min 11 s 344.85 ms remaining ; 5 h 36 min 39 s 6.93 ms total) Wed May 27 07:59:54 2026: Removed ≈ 36% of redundant conclusions. [15290347 of approximately 42473187] (ETC: Wed May 27 11:35:08 2026 ; 3 h 35 min 14 s 596.10 ms remaining ; 5 h 36 min 19 s 56.17 ms total) Wed May 27 08:06:29 2026: Removed ≈ 38% of redundant conclusions. [16139811 of approximately 42473187] (ETC: Wed May 27 11:34:48 2026 ; 3 h 28 min 18 s 243.84 ms remaining ; 5 h 35 min 58 s 457.77 ms total) Wed May 27 08:13:04 2026: Removed ≈ 40% of redundant conclusions. [16989274 of approximately 42473187] (ETC: Wed May 27 11:34:25 2026 ; 3 h 21 min 21 s 592.71 ms remaining ; 5 h 35 min 35 s 987.21 ms total) Wed May 27 08:19:36 2026: Removed ≈ 42% of redundant conclusions. [17838738 of approximately 42473187] (ETC: Wed May 27 11:34:01 2026 ; 3 h 14 min 24 s 734.21 ms remaining ; 5 h 35 min 11 s 610.26 ms total) Wed May 27 08:26:06 2026: Removed ≈ 44% of redundant conclusions. [18688202 of approximately 42473187] (ETC: Wed May 27 11:33:33 2026 ; 3 h 7 min 26 s 944.92 ms remaining ; 5 h 34 min 43 s 829.98 ms total) Wed May 27 08:32:33 2026: Removed ≈ 46% of redundant conclusions. [19537666 of approximately 42473187] (ETC: Wed May 27 11:33:02 2026 ; 3 h 28 s 321.50 ms remaining ; 5 h 34 min 12 s 447.20 ms total) Wed May 27 08:39:00 2026: Removed ≈ 48% of redundant conclusions. [20387129 of approximately 42473187] (ETC: Wed May 27 11:32:33 2026 ; 2 h 53 min 32 s 299.24 ms remaining ; 5 h 33 min 43 s 651.69 ms total) Wed May 27 08:45:24 2026: Removed ≈ 50% of redundant conclusions. [21236593 of approximately 42473187] (ETC: Wed May 27 11:31:59 2026 ; 2 h 46 min 34 s 748.93 ms remaining ; 5 h 33 min 9 s 497.39 ms total) Wed May 27 08:51:47 2026: Removed ≈ 52% of redundant conclusions. [22086057 of approximately 42473187] (ETC: Wed May 27 11:31:27 2026 ; 2 h 39 min 39 s 569.71 ms remaining ; 5 h 32 min 37 s 436.66 ms total) Wed May 27 08:58:08 2026: Removed ≈ 54% of redundant conclusions. [22935520 of approximately 42473187] (ETC: Wed May 27 11:30:53 2026 ; 2 h 32 min 45 s 3.21 ms remaining ; 5 h 32 min 3 s 919.03 ms total) Wed May 27 09:04:28 2026: Removed ≈ 56% of redundant conclusions. [23784984 of approximately 42473187] (ETC: Wed May 27 11:30:19 2026 ; 2 h 25 min 51 s 605.40 ms remaining ; 5 h 31 min 30 s 11.51 ms total) Wed May 27 09:10:45 2026: Removed ≈ 58% of redundant conclusions. [24634448 of approximately 42473187] (ETC: Wed May 27 11:29:44 2026 ; 2 h 18 min 58 s 944.05 ms remaining ; 5 h 30 min 54 s 628.19 ms total) Wed May 27 09:17:01 2026: Removed ≈ 60% of redundant conclusions. [25483912 of approximately 42473187] (ETC: Wed May 27 11:29:09 2026 ; 2 h 12 min 7 s 834.45 ms remaining ; 5 h 30 min 19 s 585.90 ms total) Wed May 27 09:23:15 2026: Removed ≈ 62% of redundant conclusions. [26333375 of approximately 42473187] (ETC: Wed May 27 11:28:33 2026 ; 2 h 5 min 17 s 693.96 ms remaining ; 5 h 29 min 43 s 404.01 ms total) Wed May 27 09:29:27 2026: Removed ≈ 64% of redundant conclusions. [27182839 of approximately 42473187] (ETC: Wed May 27 11:27:56 2026 ; 1 h 58 min 28 s 794.40 ms remaining ; 5 h 29 min 6 s 650.25 ms total) Wed May 27 09:35:49 2026: Removed ≈ 66% of redundant conclusions. [28032303 of approximately 42473187] (ETC: Wed May 27 11:27:36 2026 ; 1 h 51 min 47 s 10.97 ms remaining ; 5 h 28 min 46 s 502.28 ms total) Wed May 27 09:42:27 2026: Removed ≈ 68% of redundant conclusions. [28881767 of approximately 42473187] (ETC: Wed May 27 11:27:41 2026 ; 1 h 45 min 14 s 113.68 ms remaining ; 5 h 28 min 51 s 605.03 ms total) Wed May 27 09:48:33 2026: Removed ≈ 70% of redundant conclusions. [29731230 of approximately 42473187] (ETC: Wed May 27 11:27:01 2026 ; 1 h 38 min 27 s 582.51 ms remaining ; 5 h 28 min 11 s 940.33 ms total) Wed May 27 09:54:37 2026: Removed ≈ 72% of redundant conclusions. [30580694 of approximately 42473187] (ETC: Wed May 27 11:26:19 2026 ; 1 h 31 min 41 s 907.44 ms remaining ; 5 h 27 min 29 s 668.37 ms total) Wed May 27 10:00:39 2026: Removed ≈ 74% of redundant conclusions. [31430158 of approximately 42473187] (ETC: Wed May 27 11:25:37 2026 ; 1 h 24 min 57 s 962.04 ms remaining ; 5 h 26 min 47 s 545.63 ms total) Wed May 27 10:06:39 2026: Removed ≈ 76% of redundant conclusions. [32279622 of approximately 42473187] (ETC: Wed May 27 11:24:55 2026 ; 1 h 18 min 15 s 889.72 ms remaining ; 5 h 26 min 6 s 206.96 ms total) Wed May 27 10:12:40 2026: Removed ≈ 78% of redundant conclusions. [33129085 of approximately 42473187] (ETC: Wed May 27 11:24:15 2026 ; 1 h 11 min 35 s 778.35 ms remaining ; 5 h 25 min 26 s 263.42 ms total) Wed May 27 10:18:39 2026: Removed ≈ 80% of redundant conclusions. [33978549 of approximately 42473187] (ETC: Wed May 27 11:23:36 2026 ; 1 h 4 min 57 s 470.02 ms remaining ; 5 h 24 min 47 s 348.70 ms total) Wed May 27 10:24:38 2026: Removed ≈ 82% of redundant conclusions. [34828013 of approximately 42473187] (ETC: Wed May 27 11:22:59 2026 ; 58 min 20 s 925.96 ms remaining ; 5 h 24 min 9 s 587.79 ms total) Wed May 27 10:30:36 2026: Removed ≈ 84% of redundant conclusions. [35677477 of approximately 42473187] (ETC: Wed May 27 11:22:22 2026 ; 51 min 46 s 84.73 ms remaining ; 5 h 23 min 33 s 29.32 ms total) Wed May 27 10:36:34 2026: Removed ≈ 86% of redundant conclusions. [36526940 of approximately 42473187] (ETC: Wed May 27 11:21:47 2026 ; 45 min 12 s 969.24 ms remaining ; 5 h 22 min 58 s 349.02 ms total) Wed May 27 10:42:39 2026: Removed ≈ 88% of redundant conclusions. [37376404 of approximately 42473187] (ETC: Wed May 27 11:21:21 2026 ; 38 min 42 s 227.88 ms remaining ; 5 h 22 min 31 s 896.86 ms total) Wed May 27 10:48:53 2026: Removed ≈ 90% of redundant conclusions. [38225868 of approximately 42473187] (ETC: Wed May 27 11:21:06 2026 ; 32 min 13 s 725.56 ms remaining ; 5 h 22 min 17 s 254.22 ms total) Wed May 27 10:54:53 2026: Removed ≈ 92% of redundant conclusions. [39075332 of approximately 42473187] (ETC: Wed May 27 11:20:38 2026 ; 25 min 44 s 692.13 ms remaining ; 5 h 21 min 48 s 651.41 ms total) Wed May 27 11:00:50 2026: Removed ≈ 94% of redundant conclusions. [39924795 of approximately 42473187] (ETC: Wed May 27 11:20:06 2026 ; 19 min 16 s 631.41 ms remaining ; 5 h 21 min 17 s 184.24 ms total) Wed May 27 11:06:53 2026: Removed ≈ 96% of redundant conclusions. [40774259 of approximately 42473187] (ETC: Wed May 27 11:19:43 2026 ; 12 min 50 s 169.68 ms remaining ; 5 h 20 min 54 s 236.14 ms total) [Rank 27] Workload transfer approved. Starting to work on 0:[762248, 781792]. [Rank 5] Workload transfer approved. Starting to work on 3:[3136945, 3156489]. [Rank 1] Workload transfer approved. Starting to work on 15:[12635731, 12655275]. [Rank 4] Workload transfer approved. Starting to work on 22:[18176689, 18196233]. [Rank 20] Workload transfer approved. Starting to work on 28:[22926082, 22945626]. [Rank 2] Workload transfer approved. Starting to work on 29:[23717648, 23737192]. Wed May 27 11:13:09 2026: Removed ≈ 98% of redundant conclusions. [41623723 of approximately 42473187] (ETC: Wed May 27 11:19:34 2026 ; 6 min 24 s 899.82 ms remaining ; 5 h 20 min 44 s 984.96 ms total) [Rank 7] Workload transfer approved. Starting to work on 34:[27675475, 27695019]. [Rank 37] Workload transfer approved. Starting to work on 3:[3156490, 3163004]. [Rank 41] Workload transfer approved. Starting to work on 8:[7114317, 7120831]. [Rank 42] Workload transfer approved. Starting to work on 9:[7905883, 7912397]. [Rank 6] Workload transfer approved. Starting to work on 11:[9489014, 9495528]. [Rank 32] Workload transfer approved. Starting to work on 12:[10280579, 10287093]. [Rank 36] Workload transfer approved. Starting to work on 17:[14238407, 14244921]. [Rank 26] Workload transfer approved. Starting to work on 22:[18196234, 18202748]. [Rank 15] Workload transfer approved. Starting to work on 29:[23737193, 23743707]. [Rank 3] Workload transfer approved. Starting to work on 31:[25320324, 25326838]. [Rank 30] Workload transfer approved. Starting to work on 34:[27695020, 27701534]. [Rank 24] Workload transfer approved. Starting to work on 35:[28486586, 28493100]. [Rank 37] Workload transfer approved. Starting to work on 39:[31652848, 31659362]. [Rank 23] Workload transfer approved. Starting to work on 40:[32444413, 32450927]. [Rank 25] Workload transfer approved. Starting to work on 45:[36402241, 36408755]. [Rank 13] Workload transfer approved. Starting to work on 48:[38776937, 38783451]. [Rank 43] Workload transfer approved. Starting to work on 49:[39568503, 39575017]. [Rank 41] Workload transfer approved. Starting to work on 50:[40360068, 40366582]. [Rank 42] Workload transfer approved. Starting to work on 54:[43526330, 43532844]. [Rank 0] Workload transfer approved. Starting to work on 56:[45109461, 45115975]. [Rank 47] Workload transfer approved. Starting to work on 59:[47484158, 47490672]. [Rank 21] Workload transfer approved. Starting to work on 8:[7120832, 7123003]. [Rank 9] Workload transfer approved. Starting to work on 10:[8703963, 8706134]. [Rank 18] Workload transfer approved. Starting to work on 11:[9495529, 9497700]. [Rank 6] Workload transfer approved. Starting to work on 12:[10287094, 10289265]. [Rank 32] Workload transfer approved. Starting to work on 22:[18202749, 18204920]. [Rank 36] Workload transfer approved. Starting to work on 29:[23743708, 23745879]. [Rank 31] Workload transfer approved. Starting to work on 33:[26909970, 26912141]. [Rank 28] Workload transfer approved. Starting to work on 34:[27701535, 27703706]. [Rank 26] Workload transfer approved. Starting to work on 35:[28493101, 28495272]. [Rank 15] Workload transfer approved. Starting to work on 45:[36408756, 36410927]. [Rank 14] Workload transfer approved. Starting to work on 46:[37200321, 37202492]. [Rank 19] Workload transfer approved. Starting to work on 52:[41949714, 41951885]. [Rank 30] Workload transfer approved. Starting to work on 53:[42741280, 42743451]. [Rank 27] Workload transfer approved. Starting to work on 54:[43532845, 43535016]. [Rank 21] Workload transfer approved. Starting to work on 55:[44324411, 44326582]. [Rank 38] Workload transfer approved. Starting to work on 56:[45115976, 45118147]. [Rank 10] Workload transfer approved. Starting to work on 57:[45907542, 45909713]. [Rank 9] Workload transfer approved. Starting to work on 59:[47490673, 47492844]. [Rank 18] Workload transfer approved. Starting to work on 11:[9497701, 9498785]. [Rank 5] Workload transfer approved. Starting to work on 12:[10289266, 10290350]. [Rank 32] Workload transfer approved. Starting to work on 17:[14247094, 14248178]. [Rank 3] Workload transfer approved. Starting to work on 22:[18204921, 18206005]. [Rank 37] Workload transfer approved. Starting to work on 29:[23745880, 23746964]. [Rank 17] Workload transfer approved. Starting to work on 35:[28495273, 28496357]. [Rank 1] Workload transfer approved. Starting to work on 39:[31661535, 31662619]. [Rank 24] Workload transfer approved. Starting to work on 45:[36410928, 36412012]. [Rank 36] Workload transfer approved. Starting to work on 48:[38785624, 38786708]. [Rank 35] Workload transfer approved. Starting to work on 52:[41951886, 41952970]. [Rank 33] Workload transfer approved. Starting to work on 53:[42743452, 42744536]. [Rank 51] Workload transfer approved. Starting to work on 55:[44326583, 44327667]. [Rank 6] Workload transfer approved. Starting to work on 56:[45118148, 45119232]. [Rank 11] Workload transfer approved. Starting to work on 57:[45909714, 45910798]. [Rank 39] Workload transfer approved. Starting to work on 58:[46701279, 46702363]. Wed May 27 11:20:05 2026: Removed ≈100% of redundant conclusions. [42473187 of approximately 42473187] (ETC: Wed May 27 11:20:05 2026 ; 0.00 ms remaining ; 5 h 21 min 15 s 388.91 ms total) 19435197.11 ms (5 h 23 min 55 s 197.11 ms) taken to detect 42486936 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 5006994 representative and 42486936 redundant condensed detachment proof strings. [Copy] Removal count: { 83, 42486936 } Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 1 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 2 on "n23m0030.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 3 on "n23m0040.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 4 on "n23m0042.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 5 on "n23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 6 on "n23m0046.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 7 on "n23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 8 on "n23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 9 on "n23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 10 on "n23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 11 on "n23m0068.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 12 on "n23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 13 on "n23m0076.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 14 on "n23m0078.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 15 on "n23m0093.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 16 on "n23m0096.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 17 on "n23m0100.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 18 on "n23m0124.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 19 on "n23m0140.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 20 on "n23m0147.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 21 on "n23m0152.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 22 on "n23m0154.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 23 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 24 on "n23m0176.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 25 on "n23m0180.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 26 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 27 on "n23m0183.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 28 on "n23m0184.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 29 on "n23m0185.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 30 on "n23m0190.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 31 on "n23m0195.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 32 on "n23m0196.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 33 on "n23m0205.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 34 on "n23m0212.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 35 on "n23m0215.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 36 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 37 on "n23m0238.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 38 on "n23m0244.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 39 on "n23m0245.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 40 on "n23m0246.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 41 on "n23m0249.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 42 on "n23m0251.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 43 on "n23m0252.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 44 on "n23m0254.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 45 on "n23m0256.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 46 on "n23m0260.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 47 on "n23m0261.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 48 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 49 on "n23m0264.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 50 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 51 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 52 on "n23m0314.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 53 on "n23m0318.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 54 on "n23m0320.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 55 on "n23m0322.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 56 on "n23m0341.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 57 on "r23m0075.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 58 on "r23m0112.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:22:42 2026: MPI-based D-proof representative filter complete. [rank 59 on "r23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] 1043.57 ms (1 s 43.57 ms) taken to filter and order new representative proofs. Wed May 27 11:22:43 2026: Starting to write 5006994 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83.txt. 1608.01 ms (1 s 608.01 ms) taken to print and save 1147943959 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs83.txt. Wed May 27 11:22:45 2026: MPI-based D-proof representative filter complete. [rank 0 on "n23m0024.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:23:23 2026: Process terminated. [pid: 350478, tid:23205581510464] Wed May 27 11:23:23 2026: Process terminated. [pid: 488908, tid:23433115694912] Wed May 27 11:23:23 2026: Process terminated. [pid: 74177, tid:23259459561280] Wed May 27 11:23:23 2026: Process terminated. [pid: 470584, tid:23232187516736] Wed May 27 11:23:23 2026: Process terminated. [pid: 345775, tid:23044784551744] Wed May 27 11:23:23 2026: Process terminated. [pid: 354299, tid:22960185407296] Wed May 27 11:23:23 2026: Process terminated. [pid: 467418, tid:23386152425280] Wed May 27 11:23:23 2026: Process terminated. [pid: 190681, tid:22895047685952] Wed May 27 11:23:23 2026: Process terminated. [pid: 142112, tid:22359552464704] Wed May 27 11:23:23 2026: Process terminated. [pid: 189383, tid:23183005103936] Wed May 27 11:23:23 2026: Process terminated. [pid: 188570, tid:23155983918912] Wed May 27 11:23:23 2026: Process terminated. [pid: 441002, tid:23063100802880] Wed May 27 11:23:23 2026: Process terminated. [pid: 513786, tid:22585644275520] Wed May 27 11:23:23 2026: Process terminated. [pid: 105685, tid:23108085061440] Wed May 27 11:23:23 2026: Process terminated. [pid: 292791, tid:22949524375360] Wed May 27 11:23:23 2026: Process terminated. [pid: 478820, tid:23007394105152] Wed May 27 11:23:23 2026: Process terminated. [pid: 202233, tid:23117100590912] Wed May 27 11:23:23 2026: Process terminated. [pid: 111565, tid:23325611513664] Wed May 27 11:23:23 2026: Process terminated. [pid: 76311, tid:23186291349312] Wed May 27 11:23:23 2026: Process terminated. [pid: 426832, tid:22441819875136] Wed May 27 11:23:23 2026: Process terminated. [pid: 98065, tid:22684925830976] Wed May 27 11:23:23 2026: Process terminated. [pid: 421234, tid:22945509177152] Wed May 27 11:23:23 2026: Process terminated. [pid: 295697, tid:22620559423296] Wed May 27 11:23:23 2026: Process terminated. [pid: 239466, tid:22858953414464] Wed May 27 11:23:23 2026: Process terminated. [pid: 82782, tid:22567948244800] Wed May 27 11:23:23 2026: Process terminated. [pid: 391958, tid:22703636006720] Wed May 27 11:23:23 2026: Process terminated. [pid: 85677, tid:22764208592704] Wed May 27 11:23:23 2026: Process terminated. [pid: 84916, tid:22513781151552] Wed May 27 11:23:23 2026: Process terminated. [pid: 159269, tid:22944517572416] Wed May 27 11:23:23 2026: Process terminated. [pid: 336196, tid:23139116201792] Wed May 27 11:23:23 2026: Process terminated. [pid: 42934, tid:22399405066048] Wed May 27 11:23:23 2026: Process terminated. [pid: 487098, tid:22752210638656] Wed May 27 11:23:23 2026: Process terminated. [pid: 420569, tid:23021549807424] Wed May 27 11:23:23 2026: Process terminated. [pid: 109768, tid:22795969865536] Wed May 27 11:23:23 2026: Process terminated. [pid: 473626, tid:23328554141504] Wed May 27 11:23:23 2026: Process terminated. [pid: 438553, tid:22839695275840] Wed May 27 11:23:23 2026: Process terminated. [pid: 235590, tid:23331374458688] Wed May 27 11:23:23 2026: Process terminated. [pid: 80595, tid:23241308354368] Wed May 27 11:23:23 2026: Process terminated. [pid: 73933, tid:23077049411392] Wed May 27 11:23:23 2026: Process terminated. [pid: 334834, tid:22884542756672] Wed May 27 11:23:23 2026: Process terminated. [pid: 252939, tid:22387064035136] Wed May 27 11:23:23 2026: Process terminated. [pid: 250203, tid:23268499871552] Wed May 27 11:23:23 2026: Process terminated. [pid: 60628, tid:22432405464896] Wed May 27 11:23:23 2026: Process terminated. [pid: 123953, tid:22435408873280] Wed May 27 11:23:23 2026: Process terminated. [pid: 21560, tid:23065837856576] Wed May 27 11:23:23 2026: Process terminated. [pid: 211059, tid:22644595570496] Wed May 27 11:23:23 2026: Process terminated. [pid: 217084, tid:22869067880256] Wed May 27 11:23:23 2026: Process terminated. [pid: 73622, tid:23301953996608] Wed May 27 11:23:23 2026: Process terminated. [pid: 94026, tid:23173136099136] Wed May 27 11:23:23 2026: Process terminated. [pid: 437792, tid:23109550405440] Wed May 27 11:23:23 2026: Process terminated. [pid: 324661, tid:23103244752704] Wed May 27 11:23:23 2026: Process terminated. [pid: 326600, tid:23014486386496] Wed May 27 11:23:23 2026: Process terminated. [pid: 407040, tid:22758912759616] Wed May 27 11:23:23 2026: Process terminated. [pid: 21198, tid:23140739106624] Wed May 27 11:23:23 2026: Process terminated. [pid: 264392, tid:22528627033920] Wed May 27 11:23:23 2026: Process terminated. [pid: 363674, tid:23181355210560] Wed May 27 11:23:24 2026: Process terminated. [pid: 220292, tid:22683767940928] Wed May 27 11:23:24 2026: Process terminated. [pid: 27002, tid:22657289389888] Wed May 27 11:23:24 2026: Process terminated. [pid: 31894, tid:22372026296128] Wed May 27 11:23:24 2026: Process terminated. [pid: 380980, tid:22891160422208]