( 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:     6.213888… h
  CPU utilization: 35792 core-h )
Sat May 30 21:07:34 2026: Process started. [pid: 158893, tid:23003174328128]
Sat May 30 21:07:34 2026: Process started. [pid: 415342, tid:22533898045248]
Sat May 30 21:07:34 2026: Process started. [pid: 472872, tid:22369089324864]
Sat May 30 21:07:35 2026: Process started. [pid: 297138, tid:22565077174080]
Sat May 30 21:07:35 2026: Process started. [pid: 178464, tid:22755993511744]
Sat May 30 21:07:35 2026: Process started. [pid: 4383, tid:22392360494912]
Sat May 30 21:07:35 2026: Process started. [pid: 320799, tid:23018085451584]
Sat May 30 21:07:35 2026: Process started. [pid: 185392, tid:23133192939328]
Sat May 30 21:07:35 2026: Process started. [pid: 368818, tid:22818327316288]
Sat May 30 21:07:35 2026: Process started. [pid: 362920, tid:22681984227136]
Sat May 30 21:07:35 2026: Process started. [pid: 445754, tid:23008866096960]
Sat May 30 21:07:35 2026: Process started. [pid: 6262, tid:23016957368128]
Sat May 30 21:07:35 2026: Process started. [pid: 410062, tid:23243695183680]
Sat May 30 21:07:35 2026: Process started. [pid: 380341, tid:22365778925376]
Sat May 30 21:07:35 2026: Process started. [pid: 138685, tid:22728106334016]
Sat May 30 21:07:35 2026: Process started. [pid: 309946, tid:22551748216640]
Sat May 30 21:07:35 2026: Process started. [pid: 151356, tid:22860409354048]
Sat May 30 21:07:35 2026: Process started. [pid: 472138, tid:22507963356992]
Sat May 30 21:07:35 2026: Process started. [pid: 434844, tid:22763245651776]
Sat May 30 21:07:35 2026: Process started. [pid: 441820, tid:22599646996288]
Sat May 30 21:07:35 2026: Process started. [pid: 98312, tid:22362637621056]
Sat May 30 21:07:35 2026: Process started. [pid: 465126, tid:23228046968640]
Sat May 30 21:07:35 2026: Process started. [pid: 419084, tid:22863139718976]
Sat May 30 21:07:35 2026: Process started. [pid: 59657, tid:22710106376000]
Sat May 30 21:07:35 2026: Process started. [pid: 464935, tid:23343659886400]
Sat May 30 21:07:35 2026: Process started. [pid: 410238, tid:23236086523712]
Sat May 30 21:07:35 2026: Process started. [pid: 311889, tid:22380142200640]
Sat May 30 21:07:35 2026: Process started. [pid: 271304, tid:22865431705408]
Sat May 30 21:07:35 2026: Process started. [pid: 367590, tid:23099264190272]
Sat May 30 21:07:35 2026: Process started. [pid: 235779, tid:22847903807296]
Sat May 30 21:07:35 2026: Process started. [pid: 295016, tid:22674242316096]
Sat May 30 21:07:35 2026: Process started. [pid: 269195, tid:22467098949440]
Sat May 30 21:07:35 2026: Process started. [pid: 3555, tid:23425865791296]
Sat May 30 21:07:35 2026: Process started. [pid: 456097, tid:22950172198720]
Sat May 30 21:07:35 2026: Process started. [pid: 241875, tid:22922407085888]
Sat May 30 21:07:35 2026: Process started. [pid: 125665, tid:23162042427200]
Sat May 30 21:07:35 2026: Process started. [pid: 159585, tid:22645285386048]
Sat May 30 21:07:35 2026: Process started. [pid: 101605, tid:22862458013504]
Sat May 30 21:07:35 2026: Process started. [pid: 36821, tid:23368185071424]
Sat May 30 21:07:35 2026: Process started. [pid: 390218, tid:22825715611456]
Sat May 30 21:07:35 2026: Process started. [pid: 382397, tid:23334501291840]
Sat May 30 21:07:35 2026: Process started. [pid: 249611, tid:23354579576640]
Sat May 30 21:07:35 2026: Process started. [pid: 162391, tid:23240302753600]
Sat May 30 21:07:35 2026: Process started. [pid: 96989, tid:23289549035328]
Sat May 30 21:07:35 2026: Process started. [pid: 435486, tid:22808970995520]
Sat May 30 21:07:35 2026: Process started. [pid: 240518, tid:22909452896064]
Sat May 30 21:07:35 2026: Process started. [pid: 389994, tid:23429451278144]
Sat May 30 21:07:35 2026: Process started. [pid: 441721, tid:22823318792000]
Sat May 30 21:07:35 2026: Process started. [pid: 429114, tid:22420734953280]
Sat May 30 21:07:35 2026: Process started. [pid: 341310, tid:22555395237696]
Sat May 30 21:07:35 2026: Process started. [pid: 43422, tid:23196682798912]
Sat May 30 21:07:35 2026: Process started. [pid: 348796, tid:23018142279488]
Sat May 30 21:07:35 2026: Process started. [pid: 334380, tid:22465098086208]
Sat May 30 21:07:35 2026: Process started. [pid: 446900, tid:22582188496704]
Sat May 30 21:07:35 2026: Process started. [pid: 310890, tid:22820181292864]
Sat May 30 21:07:35 2026: Process started. [pid: 113888, tid:23353369511744]
Sat May 30 21:07:35 2026: Process started. [pid: 80338, tid:23108849915712]
Sat May 30 21:07:35 2026: Process started. [pid: 285325, tid:23277666686784]
Sat May 30 21:07:35 2026: Process started. [pid: 191908, tid:22415741753152]
Sat May 30 21:07:35 2026: Process started. [pid: 451180, tid:22477414401856]
Tasks:
1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true)
2. mpi_filterDProofRepresentativeFile(83, true)

[Rank 0 ; pid: 235779 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true).
Loaded 2 custom axioms. [SHA-512/224 hash: d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9]
(1) CCC0.1.2CC2.0C3.0    -    CCCpqrCCrpCsp    -    ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0))
(2) CO0                  -    COp              -    \bot\imply0
[Rank 1 ; pid: 151356 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 2 ; pid: 451180 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 3 ; pid: 191908 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 4 ; pid: 241875 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 5 ; pid: 297138 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 6 ; pid: 435486 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 7 ; pid: 446900 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 8 ; pid: 113888 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 9 ; pid: 320799 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 10 ; pid: 368818 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 11 ; pid: 415342 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 12 ; pid: 249611 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 13 ; pid: 4383 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 14 ; pid: 419084 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 15 ; pid: 295016 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 16 ; pid: 441820 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 17 ; pid: 429114 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 18 ; pid: 348796 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 19 ; pid: 285325 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 20 ; pid: 240518 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 21 ; pid: 101605 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 22 ; pid: 472138 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 23 ; pid: 6262 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 24 ; pid: 341310 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 25 ; pid: 36821 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 26 ; pid: 3555 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 27 ; pid: 334380 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 28 ; pid: 367590 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 29 ; pid: 410238 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 30 ; pid: 465126 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 31 ; pid: 185392 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 32 ; pid: 43422 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 33 ; pid: 434844 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 34 ; pid: 390218 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 35 ; pid: 271304 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 36 ; pid: 159585 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 37 ; pid: 138685 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 38 ; pid: 410062 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 39 ; pid: 178464 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 40 ; pid: 310890 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 41 ; pid: 125665 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 42 ; pid: 158893 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 43 ; pid: 456097 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 44 ; pid: 472872 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 45 ; pid: 96989 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 46 ; pid: 464935 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 47 ; pid: 162391 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 48 ; pid: 59657 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 49 ; pid: 362920 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 50 ; pid: 445754 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 51 ; pid: 269195 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 52 ; pid: 441721 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 53 ; pid: 309946 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 54 ; pid: 382397 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 55 ; pid: 98312 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 56 ; pid: 380341 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 57 ; pid: 80338 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 58 ; pid: 389994 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 59 ; pid: 311889 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently.
[Rank 0 ; pid: 235779 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 1 ; pid: 151356 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 2 ; pid: 451180 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 3 ; pid: 191908 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 4 ; pid: 241875 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 5 ; pid: 297138 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 6 ; pid: 435486 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 7 ; pid: 446900 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 8 ; pid: 113888 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 9 ; pid: 320799 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 10 ; pid: 368818 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 11 ; pid: 415342 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 12 ; pid: 249611 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 13 ; pid: 4383 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 14 ; pid: 419084 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 15 ; pid: 295016 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 16 ; pid: 441820 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 17 ; pid: 429114 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 18 ; pid: 348796 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 19 ; pid: 285325 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 20 ; pid: 240518 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 21 ; pid: 101605 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 22 ; pid: 472138 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 23 ; pid: 6262 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 24 ; pid: 341310 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 25 ; pid: 36821 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 26 ; pid: 3555 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 27 ; pid: 334380 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 28 ; pid: 367590 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 29 ; pid: 410238 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 30 ; pid: 465126 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 31 ; pid: 185392 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 32 ; pid: 43422 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 33 ; pid: 434844 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 34 ; pid: 390218 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 35 ; pid: 271304 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 36 ; pid: 159585 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 37 ; pid: 138685 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 38 ; pid: 410062 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 39 ; pid: 178464 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 40 ; pid: 310890 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 41 ; pid: 125665 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 42 ; pid: 158893 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 43 ; pid: 456097 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 44 ; pid: 472872 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 45 ; pid: 96989 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 46 ; pid: 464935 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 47 ; pid: 162391 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 48 ; pid: 59657 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 49 ; pid: 362920 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 50 ; pid: 445754 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 51 ; pid: 269195 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 52 ; pid: 441721 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 53 ; pid: 309946 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 54 ; pid: 382397 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 55 ; pid: 98312 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 56 ; pid: 380341 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 57 ; pid: 80338 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 58 ; pid: 389994 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
[Rank 59 ; pid: 311889 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(83, true).
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 0 on "n23m0022.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 1 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 2 on "n23m0036.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 3 on "n23m0061.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 4 on "n23m0067.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 5 on "n23m0113.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 6 on "n23m0117.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 7 on "n23m0136.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 8 on "n23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 9 on "n23m0167.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 10 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 11 on "n23m0175.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 12 on "n23m0178.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 13 on "n23m0179.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 14 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 15 on "n23m0187.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 16 on "n23m0188.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 17 on "n23m0191.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 18 on "n23m0193.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 19 on "n23m0194.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 20 on "n23m0201.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 21 on "n23m0210.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 22 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 23 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 24 on "n23m0265.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 25 on "n23m0269.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 26 on "n23m0272.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 27 on "n23m0278.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 28 on "n23m0286.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 29 on "n23m0288.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 30 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 31 on "n23m0311.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 32 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 33 on "n23m0313.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 34 on "n23m0316.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 35 on "n23m0319.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 36 on "n23m0328.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 37 on "n23m0338.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 38 on "n23m0352.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 39 on "n23m0356.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 40 on "n23m0379.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 41 on "n23m0389.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 42 on "n23m0391.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 43 on "n23m0394.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 44 on "n23m0408.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 45 on "r23m0003.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 46 on "r23m0005.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 47 on "r23m0019.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 48 on "r23m0022.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 49 on "r23m0043.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 50 on "r23m0044.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 51 on "r23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 52 on "r23m0047.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 53 on "r23m0048.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 54 on "r23m0052.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 55 on "r23m0053.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 56 on "r23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 57 on "r23m0082.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 58 on "r23m0131.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sat May 30 21:07:36 2026: MPI-based D-proof representative filter started. [rank 59 on "r23m0139.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
0.00 ms taken to load initial representatives.
9.56 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs3.txt. [tid:22847355303488]
3.99 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs5.txt. [tid:22847353202240]
2.53 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs7.txt. [tid:22847351100992]
0.01 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs9.txt. [tid:22846877201984]
0.03 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs11.txt. [tid:22846875100736]
5.93 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs13.txt. [tid:22846872999488]
0.31 ms taken to read 33 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs15.txt. [tid:22846870898240]
0.36 ms taken to read 45 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs17.txt. [tid:22846868796992]
0.20 ms taken to read 69 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs19.txt. [tid:22846866695744]
11.73 ms taken to read 101 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs21.txt. [tid:22846864594496]
0.03 ms taken to read 140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs23.txt. [tid:22846862493248]
6.39 ms taken to read 205 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs25.txt. [tid:22846860392000]
7.68 ms taken to read 280 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs27.txt. [tid:22846858290752]
0.34 ms taken to read 404 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs29.txt. [tid:22846856189504]
32.40 ms taken to read 568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs31.txt. [tid:22846854088256]
7.64 ms taken to read 809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs33.txt. [tid:22846851987008]
10.63 ms taken to read 1140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs35.txt. [tid:22846849885760]
18.75 ms taken to read 1614 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs37.txt. [tid:22846847784512]
24.24 ms taken to read 2278 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs39.txt. [tid:22846845683264]
22.43 ms taken to read 3217 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs41.txt. [tid:22846843582016]
46.39 ms taken to read 4529 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs43.txt. [tid:22846841480768]
27.10 ms taken to read 6426 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs45.txt. [tid:22846839379520]
27.87 ms taken to read 9042 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs47.txt. [tid:22846837278272]
28.63 ms taken to read 12829 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs49.txt. [tid:22846835177024]
44.40 ms taken to read 18076 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs51.txt. [tid:22846833075776]
56.32 ms taken to read 25667 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs53.txt. [tid:22846830974528]
56.02 ms taken to read 36224 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs55.txt. [tid:22846828873280]
72.94 ms taken to read 51530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs57.txt. [tid:22846826772032]
82.16 ms taken to read 72889 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs59.txt. [tid:22846824670784]
186.81 ms taken to read 103901 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs61.txt. [tid:22846822569536]
152.53 ms taken to read 147416 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs63.txt. [tid:22846820468288]
207.16 ms taken to read 210360 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs65.txt. [tid:22846818367040]
282.19 ms taken to read 299183 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs67.txt. [tid:22846816265792]
323.54 ms taken to read 427694 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs69.txt. [tid:22846814164544]
906.79 ms taken to read 609264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs71.txt. [tid:22844595500608]
492.74 ms taken to read 872065 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs73.txt. [tid:22844593399360]
760.39 ms taken to read 1244628 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs75.txt. [tid:22844591298112]
1492.04 ms (1 s 492.04 ms) taken to read 1782980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs77.txt. [tid:22844589196864]
1714.43 ms (1 s 714.43 ms) taken to read 2547752 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs79.txt. [tid:22844587095616]
2730.24 ms (2 s 730.24 ms) taken to read 3653261 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81.txt. [tid:22844584994368]
2767.75 ms (2 s 767.75 ms) total read duration.
Loaded 41 representative collections of sizes:
1 : 2
3 : 1
5 : 1
7 : 3
9 : 8
11 : 15
13 : 22
15 : 33
17 : 45
19 : 69
21 : 101
23 : 140
25 : 205
27 : 280
29 : 404
31 : 568
33 : 809
35 : 1140
37 : 1614
39 : 2278
41 : 3217
43 : 4529
45 : 6426
47 : 9042
49 : 12829
51 : 18076
53 : 25667
55 : 36224
57 : 51530
59 : 72889
61 : 103901
63 : 147416
65 : 210360
67 : 299183
69 : 427694
71 : 609264
73 : 872065
75 : 1244628
77 : 1782980
79 : 2547752
81 : 3653261
12146671 representatives in total.
17850.22 ms (17 s 850.22 ms) taken to read 51074573 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22844584994368]
17856.80 ms (17 s 856.80 ms) additional read duration.
Loaded 1 more representative collection of size:
83 : 51074573
63221244 representatives in total.
Sat May 30 21:07:58 2026: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 45789639, based on entry 81:31544132 and last known pair (79:21730511, 81:31544132) with 31544132/21730511 ≈ 1.45161 and 31544132 * (31544132/21730511)^1 ≈ 45789639.44.
Sat May 30 21:08:00 2026: Inserted ≈ 5% of D-proof conclusions. [ 3161062 of 63221244] (ETC: Sat May 30 21:08:22 2026 ; 22 s 487.49 ms remaining ; 23 s 671.04 ms total)
Sat May 30 21:08:01 2026: Inserted ≈10% of D-proof conclusions. [ 6322124 of 63221244] (ETC: Sat May 30 21:08:23 2026 ; 22 s 454.76 ms remaining ; 24 s 949.73 ms total)
Sat May 30 21:08:02 2026: Inserted ≈15% of D-proof conclusions. [ 9483186 of 63221244] (ETC: Sat May 30 21:08:24 2026 ; 21 s 974.16 ms remaining ; 25 s 851.95 ms total)
Sat May 30 21:08:04 2026: Inserted ≈20% of D-proof conclusions. [12644248 of 63221244] (ETC: Sat May 30 21:08:25 2026 ; 21 s   9.39 ms remaining ; 26 s 261.74 ms total)
Sat May 30 21:08:04 2026: Inserted ≈25% of D-proof conclusions. [15805311 of 63221244] (ETC: Sat May 30 21:08:22 2026 ; 17 s 616.40 ms remaining ; 23 s 488.53 ms total)
Sat May 30 21:08:05 2026: Inserted ≈30% of D-proof conclusions. [18966373 of 63221244] (ETC: Sat May 30 21:08:20 2026 ; 15 s 261.24 ms remaining ; 21 s 801.78 ms total)
Sat May 30 21:08:06 2026: Inserted ≈35% of D-proof conclusions. [22127435 of 63221244] (ETC: Sat May 30 21:08:19 2026 ; 13 s 326.58 ms remaining ; 20 s 502.43 ms total)
Sat May 30 21:08:06 2026: Inserted ≈40% of D-proof conclusions. [25288497 of 63221244] (ETC: Sat May 30 21:08:18 2026 ; 11 s 712.23 ms remaining ; 19 s 520.38 ms total)
Sat May 30 21:08:07 2026: Inserted ≈45% of D-proof conclusions. [28449559 of 63221244] (ETC: Sat May 30 21:08:17 2026 ; 10 s 312.37 ms remaining ; 18 s 749.76 ms total)
Sat May 30 21:08:07 2026: Inserted ≈50% of D-proof conclusions. [31610622 of 63221244] (ETC: Sat May 30 21:08:17 2026 ; 9 s  77.19 ms remaining ; 18 s 154.38 ms total)
Sat May 30 21:08:08 2026: Inserted ≈55% of D-proof conclusions. [34771684 of 63221244] (ETC: Sat May 30 21:08:16 2026 ; 8 s  12.83 ms remaining ; 17 s 806.29 ms total)
Sat May 30 21:08:09 2026: Inserted ≈60% of D-proof conclusions. [37932746 of 63221244] (ETC: Sat May 30 21:08:16 2026 ; 7 s  12.55 ms remaining ; 17 s 531.37 ms total)
Sat May 30 21:08:10 2026: Inserted ≈65% of D-proof conclusions. [41093808 of 63221244] (ETC: Sat May 30 21:08:16 2026 ; 6 s  56.14 ms remaining ; 17 s 303.27 ms total)
Sat May 30 21:08:10 2026: Inserted ≈70% of D-proof conclusions. [44254870 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 5 s 136.25 ms remaining ; 17 s 120.84 ms total)
Sat May 30 21:08:11 2026: Inserted ≈75% of D-proof conclusions. [47415933 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 4 s 242.78 ms remaining ; 16 s 971.14 ms total)
Sat May 30 21:08:12 2026: Inserted ≈80% of D-proof conclusions. [50576995 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 3 s 348.67 ms remaining ; 16 s 743.37 ms total)
Sat May 30 21:08:12 2026: Inserted ≈85% of D-proof conclusions. [53738057 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 2 s 479.97 ms remaining ; 16 s 533.13 ms total)
Sat May 30 21:08:13 2026: Inserted ≈90% of D-proof conclusions. [56899119 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 1 s 634.41 ms remaining ; 16 s 344.13 ms total)
Sat May 30 21:08:14 2026: Inserted ≈95% of D-proof conclusions. [60060181 of 63221244] (ETC: Sat May 30 21:08:15 2026 ; 808.68 ms remaining ; 16 s 173.54 ms total)
Sat May 30 21:08:14 2026: Inserted 100% of D-proof conclusions. [63221244 of 63221244] (ETC: Sat May 30 21:08:14 2026 ; 0.00 ms remaining ; 15 s 991.27 ms total)
15991.47 ms (15 s 991.47 ms) total insertion duration.
Reservable workloads: { 0:[567495, 851241], 1:[1418738, 1702484], 2:[2269981, 2553727], 3:[3121224, 3404970], 4:[3972467, 4256213], 5:[4823710, 5107456], 6:[5674953, 5958699], 7:[6526196, 6809942], 8:[7377438, 7661184], 9:[8228681, 8512427], 10:[9079924, 9363670], 11:[9931167, 10214913], 12:[10782410, 11066156], 13:[11633653, 11917399], 14:[12484896, 12768642], 15:[13336139, 13619885], 16:[14187382, 14471128], 17:[15038624, 15322370], 18:[15889867, 16173613], 19:[16741110, 17024856], 20:[17592353, 17876099], 21:[18443596, 18727342], 22:[19294839, 19578585], 23:[20146082, 20429828], 24:[20997325, 21281071], 25:[21848567, 22132313], 26:[22699810, 22983556], 27:[23551053, 23834799], 28:[24402296, 24686042], 29:[25253539, 25537285], 30:[26104782, 26388528], 31:[26956025, 27239771], 32:[27807268, 28091014], 33:[28658511, 28942257], 34:[29509753, 29793499], 35:[30360996, 30644742], 36:[31212239, 31495985], 37:[32063482, 32347228], 38:[32914725, 33198471], 39:[33765968, 34049714], 40:[34617211, 34900957], 41:[35468454, 35752200], 42:[36319696, 36603442], 43:[37170939, 37454685], 44:[38022182, 38305928], 45:[38873425, 39157171], 46:[39724668, 40008414], 47:[40575911, 40859657], 48:[41427154, 41710900], 49:[42278397, 42562143], 50:[43129640, 43413386], 51:[43980882, 44264628], 52:[44832125, 45115871], 53:[45683368, 45967114], 54:[46534611, 46818357], 55:[47385854, 47669600], 56:[48237097, 48520843], 57:[49088340, 49372086], 58:[49939583, 50223329], 59:[50790826, 51074572] }
Sat May 30 21:15:53 2026: Removed ≈  2% of redundant conclusions. [  915792 of approximately 45789639] (ETC: Sun May 31 03:27:48 2026 ; 6 h 11 min 55 s 140.12 ms remaining ; 6 h 19 min 30 s 550.74 ms total)
Sat May 30 21:23:32 2026: Removed ≈  4% of redundant conclusions. [ 1831585 of approximately 45789639] (ETC: Sun May 31 03:29:16 2026 ; 6 h  5 min 43 s 879.49 ms remaining ; 6 h 20 min 58 s 207.51 ms total)
Sat May 30 21:31:10 2026: Removed ≈  6% of redundant conclusions. [ 2747378 of approximately 45789639] (ETC: Sun May 31 03:29:24 2026 ; 5 h 58 min 14 s 797.34 ms remaining ; 6 h 21 min  6 s 805.50 ms total)
Sat May 30 21:38:48 2026: Removed ≈  8% of redundant conclusions. [ 3663171 of approximately 45789639] (ETC: Sun May 31 03:29:33 2026 ; 5 h 50 min 45 s 670.28 ms remaining ; 6 h 21 min 15 s 728.50 ms total)
Sat May 30 21:46:24 2026: Removed ≈ 10% of redundant conclusions. [ 4578963 of approximately 45789639] (ETC: Sun May 31 03:29:22 2026 ; 5 h 42 min 58 s  12.10 ms remaining ; 6 h 21 min  4 s 457.39 ms total)
Sat May 30 21:54:04 2026: Removed ≈ 12% of redundant conclusions. [ 5494756 of approximately 45789639] (ETC: Sun May 31 03:29:45 2026 ; 5 h 35 min 41 s 251.26 ms remaining ; 6 h 21 min 27 s 785.14 ms total)
Sat May 30 22:01:41 2026: Removed ≈ 14% of redundant conclusions. [ 6410549 of approximately 45789639] (ETC: Sun May 31 03:29:38 2026 ; 5 h 27 min 57 s 457.75 ms remaining ; 6 h 21 min 20 s 764.56 ms total)
Sat May 30 22:09:17 2026: Removed ≈ 16% of redundant conclusions. [ 7326342 of approximately 45789639] (ETC: Sun May 31 03:29:26 2026 ; 5 h 20 min  9 s 712.33 ms remaining ; 6 h 21 min  8 s 705.02 ms total)
Sat May 30 22:16:52 2026: Removed ≈ 18% of redundant conclusions. [ 8242135 of approximately 45789639] (ETC: Sun May 31 03:29:13 2026 ; 5 h 12 min 21 s  10.79 ms remaining ; 6 h 20 min 54 s 891.20 ms total)
Sat May 30 22:24:27 2026: Removed ≈ 20% of redundant conclusions. [ 9157927 of approximately 45789639] (ETC: Sun May 31 03:29:04 2026 ; 5 h  4 min 36 s 791.07 ms remaining ; 6 h 20 min 45 s 988.34 ms total)
Sat May 30 22:32:03 2026: Removed ≈ 22% of redundant conclusions. [10073720 of approximately 45789639] (ETC: Sun May 31 03:28:59 2026 ; 4 h 56 min 55 s 941.34 ms remaining ; 6 h 20 min 40 s 950.06 ms total)
Sat May 30 22:39:38 2026: Removed ≈ 24% of redundant conclusions. [10989513 of approximately 45789639] (ETC: Sun May 31 03:28:52 2026 ; 4 h 49 min 14 s 333.24 ms remaining ; 6 h 20 min 34 s 648.76 ms total)
Sat May 30 22:47:13 2026: Removed ≈ 26% of redundant conclusions. [11905306 of approximately 45789639] (ETC: Sun May 31 03:28:45 2026 ; 4 h 41 min 32 s 158.52 ms remaining ; 6 h 20 min 27 s 241.15 ms total)
Sat May 30 22:54:47 2026: Removed ≈ 28% of redundant conclusions. [12821098 of approximately 45789639] (ETC: Sun May 31 03:28:38 2026 ; 4 h 33 min 50 s 616.81 ms remaining ; 6 h 20 min 20 s 300.49 ms total)
Sat May 30 23:02:21 2026: Removed ≈ 30% of redundant conclusions. [13736891 of approximately 45789639] (ETC: Sun May 31 03:28:28 2026 ; 4 h 26 min  7 s 554.88 ms remaining ; 6 h 20 min 10 s 792.20 ms total)
Sat May 30 23:09:51 2026: Removed ≈ 32% of redundant conclusions. [14652684 of approximately 45789639] (ETC: Sun May 31 03:28:10 2026 ; 4 h 18 min 18 s 539.00 ms remaining ; 6 h 19 min 51 s 968.76 ms total)
Sat May 30 23:17:20 2026: Removed ≈ 34% of redundant conclusions. [15568477 of approximately 45789639] (ETC: Sun May 31 03:27:51 2026 ; 4 h 10 min 30 s 196.03 ms remaining ; 6 h 19 min 33 s  24.09 ms total)
Sat May 30 23:24:48 2026: Removed ≈ 36% of redundant conclusions. [16484270 of approximately 45789639] (ETC: Sun May 31 03:27:28 2026 ; 4 h  2 min 40 s 168.15 ms remaining ; 6 h 19 min 10 s 262.71 ms total)
Sat May 30 23:32:12 2026: Removed ≈ 38% of redundant conclusions. [17400062 of approximately 45789639] (ETC: Sun May 31 03:27:00 2026 ; 3 h 54 min 47 s 864.00 ms remaining ; 6 h 18 min 42 s 360.64 ms total)
Sat May 30 23:39:35 2026: Removed ≈ 40% of redundant conclusions. [18315855 of approximately 45789639] (ETC: Sun May 31 03:26:30 2026 ; 3 h 46 min 55 s 666.97 ms remaining ; 6 h 18 min 12 s 777.78 ms total)
Sat May 30 23:46:56 2026: Removed ≈ 42% of redundant conclusions. [19231648 of approximately 45789639] (ETC: Sun May 31 03:26:00 2026 ; 3 h 39 min  4 s 399.93 ms remaining ; 6 h 17 min 42 s 758.17 ms total)
Sat May 30 23:54:12 2026: Removed ≈ 44% of redundant conclusions. [20147441 of approximately 45789639] (ETC: Sun May 31 03:25:22 2026 ; 3 h 31 min  9 s 783.86 ms remaining ; 6 h 17 min  4 s 613.89 ms total)
Sun May 31 00:01:30 2026: Removed ≈ 46% of redundant conclusions. [21063233 of approximately 45789639] (ETC: Sun May 31 03:24:51 2026 ; 3 h 23 min 20 s 255.30 ms remaining ; 6 h 16 min 33 s  64.51 ms total)
Sun May 31 00:08:46 2026: Removed ≈ 48% of redundant conclusions. [21979026 of approximately 45789639] (ETC: Sun May 31 03:24:17 2026 ; 3 h 15 min 30 s 803.21 ms remaining ; 6 h 15 min 59 s 236.25 ms total)
Sun May 31 00:16:00 2026: Removed ≈ 50% of redundant conclusions. [22894819 of approximately 45789639] (ETC: Sun May 31 03:23:41 2026 ; 3 h  7 min 41 s 909.15 ms remaining ; 6 h 15 min 23 s 817.81 ms total)
Sun May 31 00:23:11 2026: Removed ≈ 52% of redundant conclusions. [23810612 of approximately 45789639] (ETC: Sun May 31 03:23:06 2026 ; 2 h 59 min 54 s 185.27 ms remaining ; 6 h 14 min 47 s 885.70 ms total)
Sun May 31 00:30:20 2026: Removed ≈ 54% of redundant conclusions. [24726405 of approximately 45789639] (ETC: Sun May 31 03:22:27 2026 ; 2 h 52 min  6 s 842.56 ms remaining ; 6 h 14 min  9 s 657.68 ms total)
Sun May 31 00:37:27 2026: Removed ≈ 56% of redundant conclusions. [25642197 of approximately 45789639] (ETC: Sun May 31 03:21:48 2026 ; 2 h 44 min 20 s 440.20 ms remaining ; 6 h 13 min 30 s  90.42 ms total)
Sun May 31 00:44:32 2026: Removed ≈ 58% of redundant conclusions. [26557990 of approximately 45789639] (ETC: Sun May 31 03:21:08 2026 ; 2 h 36 min 35 s 403.03 ms remaining ; 6 h 12 min 50 s   6.49 ms total)
Sun May 31 00:51:36 2026: Removed ≈ 60% of redundant conclusions. [27473783 of approximately 45789639] (ETC: Sun May 31 03:20:28 2026 ; 2 h 28 min 52 s 119.15 ms remaining ; 6 h 12 min 10 s 297.39 ms total)
Sun May 31 00:58:36 2026: Removed ≈ 62% of redundant conclusions. [28389576 of approximately 45789639] (ETC: Sun May 31 03:19:46 2026 ; 2 h 21 min  9 s 470.80 ms remaining ; 6 h 11 min 28 s  80.82 ms total)
Sun May 31 01:05:34 2026: Removed ≈ 64% of redundant conclusions. [29305368 of approximately 45789639] (ETC: Sun May 31 03:19:02 2026 ; 2 h 13 min 28 s  72.92 ms remaining ; 6 h 10 min 44 s 645.71 ms total)
Sun May 31 01:12:41 2026: Removed ≈ 66% of redundant conclusions. [30221161 of approximately 45789639] (ETC: Sun May 31 03:18:35 2026 ; 2 h  5 min 53 s 841.03 ms remaining ; 6 h 10 min 17 s 178.44 ms total)
Sun May 31 01:20:25 2026: Removed ≈ 68% of redundant conclusions. [31136954 of approximately 45789639] (ETC: Sun May 31 03:19:04 2026 ; 1 h 58 min 38 s 700.06 ms remaining ; 6 h 10 min 45 s 936.90 ms total)
Sun May 31 01:27:26 2026: Removed ≈ 70% of redundant conclusions. [32052747 of approximately 45789639] (ETC: Sun May 31 03:18:30 2026 ; 1 h 51 min  3 s 701.08 ms remaining ; 6 h 10 min 12 s 336.44 ms total)
Sun May 31 01:34:15 2026: Removed ≈ 72% of redundant conclusions. [32968540 of approximately 45789639] (ETC: Sun May 31 03:17:40 2026 ; 1 h 43 min 25 s 565.48 ms remaining ; 6 h  9 min 22 s 733.71 ms total)
Sun May 31 01:41:02 2026: Removed ≈ 74% of redundant conclusions. [33884332 of approximately 45789639] (ETC: Sun May 31 03:16:51 2026 ; 1 h 35 min 49 s 528.96 ms remaining ; 6 h  8 min 33 s 571.33 ms total)
Sun May 31 01:47:48 2026: Removed ≈ 76% of redundant conclusions. [34800125 of approximately 45789639] (ETC: Sun May 31 03:16:04 2026 ; 1 h 28 min 15 s 939.87 ms remaining ; 6 h  7 min 46 s 414.84 ms total)
Sun May 31 01:54:34 2026: Removed ≈ 78% of redundant conclusions. [35715918 of approximately 45789639] (ETC: Sun May 31 03:15:19 2026 ; 1 h 20 min 44 s 726.79 ms remaining ; 6 h  7 min  1 s 484.49 ms total)
Sun May 31 02:01:20 2026: Removed ≈ 80% of redundant conclusions. [36631711 of approximately 45789639] (ETC: Sun May 31 03:14:35 2026 ; 1 h 13 min 15 s 546.95 ms remaining ; 6 h  6 min 17 s 734.27 ms total)
Sun May 31 02:08:07 2026: Removed ≈ 82% of redundant conclusions. [37547503 of approximately 45789639] (ETC: Sun May 31 03:13:55 2026 ; 1 h  5 min 48 s 803.55 ms remaining ; 6 h  5 min 37 s 794.88 ms total)
Sun May 31 02:14:50 2026: Removed ≈ 84% of redundant conclusions. [38463296 of approximately 45789639] (ETC: Sun May 31 03:13:14 2026 ; 58 min 23 s 378.19 ms remaining ; 6 h  4 min 56 s 111.45 ms total)
Sun May 31 02:21:35 2026: Removed ≈ 86% of redundant conclusions. [39379089 of approximately 45789639] (ETC: Sun May 31 03:12:35 2026 ; 51 min       50.56 ms remaining ; 6 h  4 min 17 s 502.18 ms total)
Sun May 31 02:28:29 2026: Removed ≈ 88% of redundant conclusions. [40294882 of approximately 45789639] (ETC: Sun May 31 03:12:09 2026 ; 43 min 39 s 779.41 ms remaining ; 6 h  3 min 51 s 493.85 ms total)
Sun May 31 02:35:35 2026: Removed ≈ 90% of redundant conclusions. [41210675 of approximately 45789639] (ETC: Sun May 31 03:11:57 2026 ; 36 min 21 s 906.31 ms remaining ; 6 h  3 min 39 s  62.60 ms total)
Sun May 31 02:42:18 2026: Removed ≈ 92% of redundant conclusions. [42126467 of approximately 45789639] (ETC: Sun May 31 03:11:21 2026 ; 29 min  2 s 671.03 ms remaining ; 6 h  3 min  3 s 382.68 ms total)
Sun May 31 02:49:05 2026: Removed ≈ 94% of redundant conclusions. [43042260 of approximately 45789639] (ETC: Sun May 31 03:10:50 2026 ; 21 min 45 s 168.73 ms remaining ; 6 h  2 min 32 s 806.99 ms total)
Sun May 31 02:55:58 2026: Removed ≈ 96% of redundant conclusions. [43958053 of approximately 45789639] (ETC: Sun May 31 03:10:27 2026 ; 14 min 29 s 189.75 ms remaining ; 6 h  2 min  9 s 738.65 ms total)
[Rank 3] Workload transfer approved. Starting to work on 0:[819715, 840732].
[Rank 51] Workload transfer approved. Starting to work on 6:[5927173, 5948190].
[Rank 25] Workload transfer approved. Starting to work on 11:[10183387, 10204404].
[Rank 36] Workload transfer approved. Starting to work on 16:[14439602, 14460619].
[Rank 32] Workload transfer approved. Starting to work on 23:[20398302, 20419319].
Sun May 31 03:03:07 2026: Removed ≈ 98% of redundant conclusions. [44873846 of approximately 45789639] (ETC: Sun May 31 03:10:21 2026 ; 7 min 14 s 472.75 ms remaining ; 6 h  2 min  3 s 632.16 ms total)
[Rank 27] Workload transfer approved. Starting to work on 35:[30613216, 30634233].
[Rank 39] Workload transfer approved. Starting to work on 50:[43381860, 43402877].
[Rank 33] Workload transfer approved. Starting to work on 57:[49340560, 49361577].
[Rank 19] Workload transfer approved. Starting to work on 1:[1691976, 1698981].
[Rank 38] Workload transfer approved. Starting to work on 2:[2543219, 2550224].
[Rank 21] Workload transfer approved. Starting to work on 4:[4245705, 4252710].
[Rank 52] Workload transfer approved. Starting to work on 6:[5948191, 5955196].
[Rank 18] Workload transfer approved. Starting to work on 9:[8501919, 8508924].
[Rank 43] Workload transfer approved. Starting to work on 10:[9353162, 9360167].
[Rank 7] Workload transfer approved. Starting to work on 16:[14460620, 14467625].
[Rank 22] Workload transfer approved. Starting to work on 20:[17865591, 17872596].
[Rank 8] Workload transfer approved. Starting to work on 35:[30634234, 30641239].
[Rank 26] Workload transfer approved. Starting to work on 37:[32336720, 32343725].
[Rank 19] Workload transfer approved. Starting to work on 50:[43402878, 43409883].
[Rank 47] Workload transfer approved. Starting to work on 57:[49361578, 49368583].
[Rank 14] Workload transfer approved. Starting to work on 58:[50212821, 50219826].
[Rank 49] Workload transfer approved. Starting to work on 1:[1698982, 1701317].
[Rank 38] Workload transfer approved. Starting to work on 5:[5103954, 5106289].
[Rank 12] Workload transfer approved. Starting to work on 6:[5955197, 5957532].
[Rank 15] Workload transfer approved. Starting to work on 11:[10211411, 10213746].
[Rank 3] Workload transfer approved. Starting to work on 13:[11913897, 11916232].
[Rank 46] Workload transfer approved. Starting to work on 16:[14467626, 14469961].
[Rank 21] Workload transfer approved. Starting to work on 28:[24682540, 24684875].
[Rank 52] Workload transfer approved. Starting to work on 29:[25533783, 25536118].
[Rank 17] Workload transfer approved. Starting to work on 30:[26385026, 26387361].
[Rank 51] Workload transfer approved. Starting to work on 34:[29789997, 29792332].
[Rank 13] Workload transfer approved. Starting to work on 35:[30641240, 30643575].
[Rank 25] Workload transfer approved. Starting to work on 37:[32343726, 32346061].
[Rank 49] Workload transfer approved. Starting to work on 40:[34897455, 34899790].
[Rank 0] Workload transfer approved. Starting to work on 41:[35748698, 35751033].
[Rank 15] Workload transfer approved. Starting to work on 45:[39153669, 39156004].
[Rank 18] Workload transfer approved. Starting to work on 50:[43409884, 43412219].
[Rank 12] Workload transfer approved. Starting to work on 54:[46814855, 46817190].
[Rank 38] Workload transfer approved. Starting to work on 56:[48517341, 48519676].
[Rank 3] Workload transfer approved. Starting to work on 57:[49368584, 49370919].
[Rank 24] Workload transfer approved. Starting to work on 2:[2552561, 2553727].
[Rank 46] Workload transfer approved. Starting to work on 11:[10213747, 10214913].
[Rank 42] Workload transfer approved. Starting to work on 16:[14469962, 14471128].
[Rank 1] Workload transfer approved. Starting to work on 29:[25536119, 25537285].
[Rank 21] Workload transfer approved. Starting to work on 30:[26387362, 26388528].
[Rank 2] Workload transfer approved. Starting to work on 35:[30643576, 30644742].
[Rank 28] Workload transfer approved. Starting to work on 37:[32346062, 32347228].
[Rank 5] Workload transfer approved. Starting to work on 40:[34899791, 34900957].
[Rank 34] Workload transfer approved. Starting to work on 41:[35751034, 35752200].
[Rank 30] Workload transfer approved. Starting to work on 44:[38304762, 38305928].
[Rank 23] Workload transfer approved. Starting to work on 45:[39156005, 39157171].
[Rank 9] Workload transfer approved. Starting to work on 48:[41709734, 41710900].
[Rank 10] Workload transfer approved. Starting to work on 50:[43412220, 43413386].
[Rank 31] Workload transfer approved. Starting to work on 54:[46817191, 46818357].
[Rank 52] Workload transfer approved. Starting to work on 55:[47668434, 47669600].
[Rank 17] Workload transfer approved. Starting to work on 57:[49370920, 49372086].
[Rank 55] Workload transfer approved. Starting to work on 59:[51073406, 51074572].
Sun May 31 03:10:46 2026: Removed ≈100% of redundant conclusions. [45789639 of approximately 45789639] (ETC: Sun May 31 03:10:46 2026 ; 0.00 ms remaining ; 6 h  2 min 28 s  95.46 ms total)
22275316.31 ms (6 h 11 min 15 s 316.31 ms) taken to detect 45848162 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 5226411 representative and 45848162 redundant condensed detachment proof strings.
[Copy] Removal count: { 83, 45848162 }
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 1 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 2 on "n23m0036.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 3 on "n23m0061.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 4 on "n23m0067.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 5 on "n23m0113.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 6 on "n23m0117.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 7 on "n23m0136.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 8 on "n23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 9 on "n23m0167.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 10 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 11 on "n23m0175.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 12 on "n23m0178.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 13 on "n23m0179.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 14 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 15 on "n23m0187.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 16 on "n23m0188.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 17 on "n23m0191.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 18 on "n23m0193.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 19 on "n23m0194.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 20 on "n23m0201.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 21 on "n23m0210.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 22 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 23 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 24 on "n23m0265.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 25 on "n23m0269.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 26 on "n23m0272.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 27 on "n23m0278.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 28 on "n23m0286.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 29 on "n23m0288.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 30 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 31 on "n23m0311.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 32 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 33 on "n23m0313.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 34 on "n23m0316.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 35 on "n23m0319.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 36 on "n23m0328.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 37 on "n23m0338.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 38 on "n23m0352.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 39 on "n23m0356.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 40 on "n23m0379.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 41 on "n23m0389.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 42 on "n23m0391.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 43 on "n23m0394.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 44 on "n23m0408.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 45 on "r23m0003.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 46 on "r23m0005.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 47 on "r23m0019.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 48 on "r23m0022.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 49 on "r23m0043.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 50 on "r23m0044.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 51 on "r23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 52 on "r23m0047.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 53 on "r23m0048.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 54 on "r23m0052.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 55 on "r23m0053.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 56 on "r23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 57 on "r23m0082.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 58 on "r23m0131.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:19:31 2026: MPI-based D-proof representative filter complete. [rank 59 on "r23m0139.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
1297.38 ms (1 s 297.38 ms) taken to filter and order new representative proofs.
Sun May 31 03:19:32 2026: Starting to write 5226411 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83.txt.
1841.08 ms (1 s 841.08 ms) taken to print and save 1187918763 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs83.txt.
Sun May 31 03:19:34 2026: MPI-based D-proof representative filter complete. [rank 0 on "n23m0022.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Sun May 31 03:20:23 2026: Process terminated. [pid: 249611, tid:23354579576640]
Sun May 31 03:20:23 2026: Process terminated. [pid: 138685, tid:22728106334016]
Sun May 31 03:20:23 2026: Process terminated. [pid: 310890, tid:22820181292864]
Sun May 31 03:20:23 2026: Process terminated. [pid: 465126, tid:23228046968640]
Sun May 31 03:20:23 2026: Process terminated. [pid: 464935, tid:23343659886400]
Sun May 31 03:20:23 2026: Process terminated. [pid: 390218, tid:22825715611456]
Sun May 31 03:20:23 2026: Process terminated. [pid: 382397, tid:23334501291840]
Sun May 31 03:20:23 2026: Process terminated. [pid: 451180, tid:22477414401856]
Sun May 31 03:20:23 2026: Process terminated. [pid: 435486, tid:22808970995520]
Sun May 31 03:20:23 2026: Process terminated. [pid: 311889, tid:22380142200640]
Sun May 31 03:20:23 2026: Process terminated. [pid: 419084, tid:22863139718976]
Sun May 31 03:20:23 2026: Process terminated. [pid: 3555, tid:23425865791296]
Sun May 31 03:20:23 2026: Process terminated. [pid: 441721, tid:22823318792000]
Sun May 31 03:20:23 2026: Process terminated. [pid: 159585, tid:22645285386048]
Sun May 31 03:20:23 2026: Process terminated. [pid: 472138, tid:22507963356992]
Sun May 31 03:20:23 2026: Process terminated. [pid: 368818, tid:22818327316288]
Sun May 31 03:20:23 2026: Process terminated. [pid: 36821, tid:23368185071424]
Sun May 31 03:20:23 2026: Process terminated. [pid: 334380, tid:22465098086208]
Sun May 31 03:20:23 2026: Process terminated. [pid: 6262, tid:23016957368128]
Sun May 31 03:20:23 2026: Process terminated. [pid: 271304, tid:22865431705408]
Sun May 31 03:20:23 2026: Process terminated. [pid: 4383, tid:22392360494912]
Sun May 31 03:20:23 2026: Process terminated. [pid: 320799, tid:23018085451584]
Sun May 31 03:20:23 2026: Process terminated. [pid: 295016, tid:22674242316096]
Sun May 31 03:20:23 2026: Process terminated. [pid: 445754, tid:23008866096960]
Sun May 31 03:20:23 2026: Process terminated. [pid: 43422, tid:23196682798912]
Sun May 31 03:20:23 2026: Process terminated. [pid: 362920, tid:22681984227136]
Sun May 31 03:20:23 2026: Process terminated. [pid: 456097, tid:22950172198720]
Sun May 31 03:20:23 2026: Process terminated. [pid: 80338, tid:23108849915712]
Sun May 31 03:20:23 2026: Process terminated. [pid: 410238, tid:23236086523712]
Sun May 31 03:20:23 2026: Process terminated. [pid: 415342, tid:22533898045248]
Sun May 31 03:20:23 2026: Process terminated. [pid: 98312, tid:22362637621056]
Sun May 31 03:20:23 2026: Process terminated. [pid: 389994, tid:23429451278144]
Sun May 31 03:20:23 2026: Process terminated. [pid: 59657, tid:22710106376000]
Sun May 31 03:20:23 2026: Process terminated. [pid: 348796, tid:23018142279488]
Sun May 31 03:20:23 2026: Process terminated. [pid: 191908, tid:22415741753152]
Sun May 31 03:20:23 2026: Process terminated. [pid: 158893, tid:23003174328128]
Sun May 31 03:20:23 2026: Process terminated. [pid: 446900, tid:22582188496704]
Sun May 31 03:20:23 2026: Process terminated. [pid: 241875, tid:22922407085888]
Sun May 31 03:20:23 2026: Process terminated. [pid: 151356, tid:22860409354048]
Sun May 31 03:20:23 2026: Process terminated. [pid: 113888, tid:23353369511744]
Sun May 31 03:20:23 2026: Process terminated. [pid: 472872, tid:22369089324864]
Sun May 31 03:20:23 2026: Process terminated. [pid: 434844, tid:22763245651776]
Sun May 31 03:20:23 2026: Process terminated. [pid: 185392, tid:23133192939328]
Sun May 31 03:20:23 2026: Process terminated. [pid: 380341, tid:22365778925376]
Sun May 31 03:20:23 2026: Process terminated. [pid: 367590, tid:23099264190272]
Sun May 31 03:20:23 2026: Process terminated. [pid: 235779, tid:22847903807296]
Sun May 31 03:20:23 2026: Process terminated. [pid: 178464, tid:22755993511744]
Sun May 31 03:20:23 2026: Process terminated. [pid: 429114, tid:22420734953280]
Sun May 31 03:20:23 2026: Process terminated. [pid: 96989, tid:23289549035328]
Sun May 31 03:20:23 2026: Process terminated. [pid: 297138, tid:22565077174080]
Sun May 31 03:20:23 2026: Process terminated. [pid: 125665, tid:23162042427200]
Sun May 31 03:20:24 2026: Process terminated. [pid: 309946, tid:22551748216640]
Sun May 31 03:20:24 2026: Process terminated. [pid: 162391, tid:23240302753600]
Sun May 31 03:20:24 2026: Process terminated. [pid: 269195, tid:22467098949440]
Sun May 31 03:20:24 2026: Process terminated. [pid: 441820, tid:22599646996288]
Sun May 31 03:20:24 2026: Process terminated. [pid: 240518, tid:22909452896064]
Sun May 31 03:20:24 2026: Process terminated. [pid: 341310, tid:22555395237696]
Sun May 31 03:20:24 2026: Process terminated. [pid: 285325, tid:23277666686784]
Sun May 31 03:20:24 2026: Process terminated. [pid: 410062, tid:23243695183680]
srun: First task exited 5s ago
srun: StepId=684628.0 task 21: running
srun: StepId=684628.0 tasks 0-20,22-59: exited
srun: Terminating StepId=684628.0
srun: Job step aborted: Waiting up to 92 seconds for job step to finish.
srun: error: n23m0210: task 21: Killed