( 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:     2.696111… h
  CPU utilization: 15529.6 core-h )
Mon May 25 20:54:41 2026: Process started. [pid: 372717, tid:23453741684544]
Mon May 25 20:54:41 2026: Process started. [pid: 39821, tid:23385999095616]
Mon May 25 20:54:41 2026: Process started. [pid: 322533, tid:23143535040320]
Mon May 25 20:54:41 2026: Process started. [pid: 67188, tid:23324194113344]
Mon May 25 20:54:41 2026: Process started. [pid: 283948, tid:22688989734720]
Mon May 25 20:54:41 2026: Process started. [pid: 518610, tid:23422816601920]
Mon May 25 20:54:41 2026: Process started. [pid: 460859, tid:22574477944640]
Mon May 25 20:54:41 2026: Process started. [pid: 375497, tid:22956122691392]
Mon May 25 20:54:41 2026: Process started. [pid: 340662, tid:23070401922880]
Mon May 25 20:54:41 2026: Process started. [pid: 161425, tid:22440770766656]
Mon May 25 20:54:42 2026: Process started. [pid: 61060, tid:22431195334464]
Mon May 25 20:54:42 2026: Process started. [pid: 94413, tid:22759996147520]
Mon May 25 20:54:42 2026: Process started. [pid: 55200, tid:23075115525952]
Mon May 25 20:54:42 2026: Process started. [pid: 133775, tid:23316327855936]
Mon May 25 20:54:42 2026: Process started. [pid: 358581, tid:22684290385728]
Mon May 25 20:54:42 2026: Process started. [pid: 336418, tid:22651077191488]
Mon May 25 20:54:42 2026: Process started. [pid: 129898, tid:23380639000384]
Mon May 25 20:54:42 2026: Process started. [pid: 83401, tid:22464947054400]
Mon May 25 20:54:42 2026: Process started. [pid: 25356, tid:22833542047552]
Mon May 25 20:54:42 2026: Process started. [pid: 442408, tid:23405289076544]
Mon May 25 20:54:42 2026: Process started. [pid: 297975, tid:22644580443968]
Mon May 25 20:54:42 2026: Process started. [pid: 173217, tid:22370950539072]
Mon May 25 20:54:42 2026: Process started. [pid: 115703, tid:23404261353280]
Mon May 25 20:54:42 2026: Process started. [pid: 514404, tid:22441746474816]
Mon May 25 20:54:42 2026: Process started. [pid: 243825, tid:23155956434752]
Mon May 25 20:54:42 2026: Process started. [pid: 425414, tid:22565365000000]
Mon May 25 20:54:42 2026: Process started. [pid: 216173, tid:23225495660352]
Mon May 25 20:54:42 2026: Process started. [pid: 325173, tid:22581571450688]
Mon May 25 20:54:42 2026: Process started. [pid: 111414, tid:23378627954496]
Mon May 25 20:54:42 2026: Process started. [pid: 93902, tid:22658761324352]
Mon May 25 20:54:42 2026: Process started. [pid: 478469, tid:22901412648768]
Mon May 25 20:54:42 2026: Process started. [pid: 419217, tid:23158069966656]
Mon May 25 20:54:42 2026: Process started. [pid: 366591, tid:23287147882304]
Mon May 25 20:54:42 2026: Process started. [pid: 513427, tid:22658757551936]
Mon May 25 20:54:42 2026: Process started. [pid: 18463, tid:23339677034304]
Mon May 25 20:54:42 2026: Process started. [pid: 497673, tid:22769969538880]
Mon May 25 20:54:42 2026: Process started. [pid: 67779, tid:22383466014528]
Mon May 25 20:54:42 2026: Process started. [pid: 200906, tid:22889763923776]
Mon May 25 20:54:42 2026: Process started. [pid: 126409, tid:23225349146432]
Mon May 25 20:54:42 2026: Process started. [pid: 9867, tid:23018638059328]
Mon May 25 20:54:42 2026: Process started. [pid: 479052, tid:23433203853120]
Mon May 25 20:54:42 2026: Process started. [pid: 458645, tid:22451160233792]
Mon May 25 20:54:42 2026: Process started. [pid: 51705, tid:22482542163776]
Mon May 25 20:54:42 2026: Process started. [pid: 467612, tid:23369280456512]
Mon May 25 20:54:42 2026: Process started. [pid: 374491, tid:23191698212672]
Mon May 25 20:54:42 2026: Process started. [pid: 161162, tid:22502989281088]
Mon May 25 20:54:42 2026: Process started. [pid: 380067, tid:22680538347328]
Mon May 25 20:54:42 2026: Process started. [pid: 82642, tid:22507514943296]
Mon May 25 20:54:42 2026: Process started. [pid: 218132, tid:22514229622592]
Mon May 25 20:54:42 2026: Process started. [pid: 44474, tid:22839143622464]
Mon May 25 20:54:42 2026: Process started. [pid: 436128, tid:22826284123968]
Mon May 25 20:54:42 2026: Process started. [pid: 222058, tid:23375360149312]
Mon May 25 20:54:42 2026: Process started. [pid: 274765, tid:22438300563264]
Mon May 25 20:54:42 2026: Process started. [pid: 261319, tid:23171622348608]
Mon May 25 20:54:42 2026: Process started. [pid: 315562, tid:22372034897728]
Mon May 25 20:54:42 2026: Process started. [pid: 167377, tid:22931563050816]
Mon May 25 20:54:42 2026: Process started. [pid: 239331, tid:22774772193088]
Mon May 25 20:54:42 2026: Process started. [pid: 518034, tid:23422632130368]
Mon May 25 20:54:42 2026: Process started. [pid: 248607, tid:22618467972928]
Mon May 25 20:54:42 2026: Process started. [pid: 412226, tid:22369879308096]
Tasks:
1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true)
2. mpi_filterDProofRepresentativeFile(81, true)

[Rank 0 ; pid: 412226 ; 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: 375497 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 2 ; pid: 55200 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 3 ; pid: 380067 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 4 ; pid: 67188 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 5 ; pid: 93902 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 6 ; pid: 83401 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 7 ; pid: 248607 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 8 ; pid: 460859 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 9 ; pid: 436128 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 10 ; pid: 283948 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 11 ; pid: 372717 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 12 ; pid: 216173 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 13 ; pid: 218132 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 14 ; pid: 366591 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 15 ; pid: 479052 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 16 ; pid: 39821 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 17 ; pid: 126409 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 18 ; pid: 374491 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 19 ; pid: 51705 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 20 ; pid: 513427 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 21 ; pid: 467612 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 22 ; pid: 325173 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 23 ; pid: 129898 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 24 ; pid: 94413 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 25 ; pid: 419217 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 26 ; pid: 25356 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 27 ; pid: 322533 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 28 ; pid: 133775 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 29 ; pid: 161425 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 30 ; pid: 18463 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 31 ; pid: 9867 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 32 ; pid: 458645 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 33 ; pid: 425414 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 34 ; pid: 61060 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 35 ; pid: 514404 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 36 ; pid: 358581 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 37 ; pid: 222058 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 38 ; pid: 173217 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 39 ; pid: 497673 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 40 ; pid: 44474 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 41 ; pid: 340662 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 42 ; pid: 518610 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 43 ; pid: 274765 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 44 ; pid: 161162 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 45 ; pid: 315562 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 46 ; pid: 67779 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 47 ; pid: 200906 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 48 ; pid: 442408 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 49 ; pid: 297975 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 50 ; pid: 336418 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 51 ; pid: 243825 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 52 ; pid: 111414 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 53 ; pid: 478469 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 54 ; pid: 167377 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 55 ; pid: 82642 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 56 ; pid: 115703 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 57 ; pid: 518034 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 58 ; pid: 261319 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 59 ; pid: 239331 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true), silently.
[Rank 0 ; pid: 412226 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 1 ; pid: 375497 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 2 ; pid: 55200 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 3 ; pid: 380067 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 4 ; pid: 67188 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 5 ; pid: 93902 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 6 ; pid: 83401 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 7 ; pid: 248607 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 8 ; pid: 460859 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 9 ; pid: 436128 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 10 ; pid: 283948 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 11 ; pid: 372717 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 12 ; pid: 216173 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 13 ; pid: 218132 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 14 ; pid: 366591 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 15 ; pid: 479052 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 16 ; pid: 39821 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 17 ; pid: 126409 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 18 ; pid: 374491 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 19 ; pid: 51705 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 20 ; pid: 513427 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 21 ; pid: 467612 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 22 ; pid: 325173 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 23 ; pid: 129898 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 24 ; pid: 94413 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 25 ; pid: 419217 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 26 ; pid: 25356 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 27 ; pid: 322533 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 28 ; pid: 133775 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 29 ; pid: 161425 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 30 ; pid: 18463 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 31 ; pid: 9867 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 32 ; pid: 458645 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 33 ; pid: 425414 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 34 ; pid: 61060 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 35 ; pid: 514404 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 36 ; pid: 358581 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 37 ; pid: 222058 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 38 ; pid: 173217 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 39 ; pid: 497673 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 40 ; pid: 44474 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 41 ; pid: 340662 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 42 ; pid: 518610 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 43 ; pid: 274765 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 44 ; pid: 161162 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 45 ; pid: 315562 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 46 ; pid: 67779 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 47 ; pid: 200906 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 48 ; pid: 442408 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 49 ; pid: 297975 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 50 ; pid: 336418 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 51 ; pid: 243825 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 52 ; pid: 111414 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 53 ; pid: 478469 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 54 ; pid: 167377 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 55 ; pid: 82642 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 56 ; pid: 115703 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 57 ; pid: 518034 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 58 ; pid: 261319 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
[Rank 59 ; pid: 239331 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true).
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 0 on "n23m0095.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 1 on "n23m0097.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 2 on "n23m0101.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 3 on "n23m0114.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 4 on "n23m0121.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 5 on "n23m0125.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 6 on "n23m0134.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 7 on "n23m0135.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 8 on "n23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 9 on "n23m0144.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 10 on "n23m0166.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 11 on "n23m0168.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 12 on "n23m0175.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 13 on "n23m0199.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 14 on "n23m0211.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 15 on "n23m0292.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 16 on "n23m0295.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 17 on "n23m0300.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 18 on "n23m0302.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 19 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 20 on "n23m0308.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 21 on "n23m0311.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 22 on "n23m0313.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 23 on "n23m0317.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 24 on "n23m0321.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 25 on "n23m0323.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 26 on "n23m0324.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 27 on "n23m0327.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 28 on "n23m0328.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 29 on "n23m0331.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 30 on "n23m0335.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 31 on "n23m0338.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 32 on "n23m0340.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 33 on "n23m0352.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 34 on "n23m0353.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 35 on "n23m0354.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 36 on "n23m0355.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 37 on "r23m0043.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 38 on "r23m0044.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 39 on "r23m0048.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 40 on "r23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 41 on "r23m0051.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 42 on "r23m0053.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 43 on "r23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 44 on "r23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 45 on "r23m0057.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 46 on "r23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 47 on "r23m0059.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 48 on "r23m0060.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 49 on "r23m0061.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 50 on "r23m0063.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 51 on "r23m0064.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 52 on "r23m0069.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 53 on "r23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 54 on "r23m0072.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 55 on "r23m0074.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 56 on "r23m0080.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 57 on "r23m0083.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 58 on "r23m0088.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 20:54:43 2026: MPI-based D-proof representative filter started. [rank 59 on "r23m0094.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
0.00 ms taken to load initial representatives.
0.01 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs3.txt. [tid:22369607337536]
0.00 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs5.txt. [tid:22369605236288]
3.06 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs7.txt. [tid:22369603135040]
0.03 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs9.txt. [tid:22369208882752]
2.75 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs11.txt. [tid:22369397634624]
0.05 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs13.txt. [tid:22369477318208]
0.06 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs15.txt. [tid:22369475216960]
2.00 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs17.txt. [tid:22369473115712]
2.21 ms taken to read 65 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs19.txt. [tid:22369471014464]
5.04 ms taken to read 98 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs21.txt. [tid:22369468913216]
0.36 ms taken to read 135 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs23.txt. [tid:22369395533376]
7.43 ms taken to read 197 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs25.txt. [tid:22369393432128]
11.55 ms taken to read 270 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs27.txt. [tid:22369391330880]
2.83 ms taken to read 388 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs29.txt. [tid:22369389229632]
4.44 ms taken to read 551 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs31.txt. [tid:22369387128384]
1.31 ms taken to read 783 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs33.txt. [tid:22369385027136]
4.26 ms taken to read 1106 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs35.txt. [tid:22369382925888]
5.28 ms taken to read 1563 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs37.txt. [tid:22369380824640]
8.72 ms taken to read 2211 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs39.txt. [tid:22369378723392]
20.51 ms taken to read 3116 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs41.txt. [tid:22369376622144]
16.05 ms taken to read 4400 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs43.txt. [tid:22369374520896]
3.43 ms taken to read 6223 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs45.txt. [tid:22369372419648]
7.69 ms taken to read 8774 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs47.txt. [tid:22369370318400]
34.18 ms taken to read 12413 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs49.txt. [tid:22369368217152]
22.22 ms taken to read 17529 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs51.txt. [tid:22369366115904]
32.82 ms taken to read 24829 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs53.txt. [tid:22369364014656]
42.39 ms taken to read 35088 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs55.txt. [tid:22369361913408]
96.33 ms taken to read 49805 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs57.txt. [tid:22369359812160]
61.86 ms taken to read 70539 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs59.txt. [tid:22369357710912]
117.30 ms taken to read 100323 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs61.txt. [tid:22369355609664]
133.48 ms taken to read 142420 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs63.txt. [tid:22369353508416]
166.91 ms taken to read 202794 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs65.txt. [tid:22369351407168]
228.27 ms taken to read 288534 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs67.txt. [tid:22369349305920]
285.09 ms taken to read 411654 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs69.txt. [tid:22369347204672]
451.51 ms taken to read 586547 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs71.txt. [tid:22369345103424]
677.90 ms taken to read 837981 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs73.txt. [tid:22369343002176]
1859.19 ms (1 s 859.19 ms) taken to read 1196203 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs75.txt. [tid:22369340900928]
2008.22 ms (2 s 8.22 ms) taken to read 1710627 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs77.txt. [tid:22369338799680]
1898.48 ms (1 s 898.48 ms) taken to read 2444582 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs79.txt. [tid:22369336698432]
2047.81 ms (2 s 47.81 ms) total read duration.
Loaded 40 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
8161870 representatives in total.
10573.29 ms (10 s 573.29 ms) taken to read 32747235 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81-unfiltered81+.txt. [tid:22369336698432]
10574.79 ms (10 s 574.79 ms) additional read duration.
Loaded 1 more representative collection of size:
81 : 32747235
40909105 representatives in total.
Mon May 25 20:54:57 2026: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 29282280, based on entry 79:20139974 and last known pair (77:13852014, 79:20139974) with 20139974/13852014 ≈ 1.45394 and 20139974 * (20139974/13852014)^1 ≈ 29282280.02.
Mon May 25 20:54:58 2026: Inserted ≈ 5% of D-proof conclusions. [ 2045455 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 8 s 860.71 ms remaining ; 9 s 327.06 ms total)
Mon May 25 20:54:59 2026: Inserted ≈10% of D-proof conclusions. [ 4090910 of 40909105] (ETC: Mon May 25 20:55:09 2026 ; 10 s 417.26 ms remaining ; 11 s 574.73 ms total)
Mon May 25 20:54:59 2026: Inserted ≈15% of D-proof conclusions. [ 6136365 of 40909105] (ETC: Mon May 25 20:55:11 2026 ; 11 s 357.01 ms remaining ; 13 s 361.19 ms total)
Mon May 25 20:55:00 2026: Inserted ≈20% of D-proof conclusions. [ 8181821 of 40909105] (ETC: Mon May 25 20:55:12 2026 ; 11 s 452.31 ms remaining ; 14 s 315.39 ms total)
Mon May 25 20:55:01 2026: Inserted ≈25% of D-proof conclusions. [10227276 of 40909105] (ETC: Mon May 25 20:55:11 2026 ; 10 s   8.97 ms remaining ; 13 s 345.29 ms total)
Mon May 25 20:55:01 2026: Inserted ≈30% of D-proof conclusions. [12272731 of 40909105] (ETC: Mon May 25 20:55:10 2026 ; 8 s 878.25 ms remaining ; 12 s 683.21 ms total)
Mon May 25 20:55:02 2026: Inserted ≈35% of D-proof conclusions. [14318186 of 40909105] (ETC: Mon May 25 20:55:10 2026 ; 7 s 978.27 ms remaining ; 12 s 274.26 ms total)
Mon May 25 20:55:02 2026: Inserted ≈40% of D-proof conclusions. [16363642 of 40909105] (ETC: Mon May 25 20:55:09 2026 ; 7 s 147.19 ms remaining ; 11 s 911.98 ms total)
Mon May 25 20:55:03 2026: Inserted ≈45% of D-proof conclusions. [18409097 of 40909105] (ETC: Mon May 25 20:55:09 2026 ; 6 s 373.24 ms remaining ; 11 s 587.71 ms total)
Mon May 25 20:55:03 2026: Inserted ≈50% of D-proof conclusions. [20454552 of 40909105] (ETC: Mon May 25 20:55:09 2026 ; 5 s 677.12 ms remaining ; 11 s 354.24 ms total)
Mon May 25 20:55:03 2026: Inserted ≈55% of D-proof conclusions. [22500007 of 40909105] (ETC: Mon May 25 20:55:08 2026 ; 5 s  14.46 ms remaining ; 11 s 143.25 ms total)
Mon May 25 20:55:04 2026: Inserted ≈60% of D-proof conclusions. [24545463 of 40909105] (ETC: Mon May 25 20:55:08 2026 ; 4 s 366.12 ms remaining ; 10 s 915.31 ms total)
Mon May 25 20:55:04 2026: Inserted ≈65% of D-proof conclusions. [26590918 of 40909105] (ETC: Mon May 25 20:55:08 2026 ; 3 s 757.74 ms remaining ; 10 s 736.39 ms total)
Mon May 25 20:55:05 2026: Inserted ≈70% of D-proof conclusions. [28636373 of 40909105] (ETC: Mon May 25 20:55:08 2026 ; 3 s 154.39 ms remaining ; 10 s 514.64 ms total)
Mon May 25 20:55:05 2026: Inserted ≈75% of D-proof conclusions. [30681828 of 40909105] (ETC: Mon May 25 20:55:08 2026 ; 2 s 577.20 ms remaining ; 10 s 308.81 ms total)
Mon May 25 20:55:05 2026: Inserted ≈80% of D-proof conclusions. [32727284 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 2 s  29.59 ms remaining ; 10 s 147.94 ms total)
Mon May 25 20:55:06 2026: Inserted ≈85% of D-proof conclusions. [34772739 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 1 s 508.44 ms remaining ; 10 s  56.25 ms total)
Mon May 25 20:55:06 2026: Inserted ≈90% of D-proof conclusions. [36818194 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 994.50 ms remaining ; 9 s 944.97 ms total)
Mon May 25 20:55:07 2026: Inserted ≈95% of D-proof conclusions. [38863649 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 492.45 ms remaining ; 9 s 849.08 ms total)
Mon May 25 20:55:07 2026: Inserted 100% of D-proof conclusions. [40909105 of 40909105] (ETC: Mon May 25 20:55:07 2026 ; 0.00 ms remaining ; 9 s 802.12 ms total)
9802.51 ms (9 s 802.51 ms) total insertion duration.
Reservable workloads: { 0:[363858, 545786], 1:[909645, 1091573], 2:[1455432, 1637360], 3:[2001220, 2183148], 4:[2547007, 2728935], 5:[3092794, 3274722], 6:[3638581, 3820509], 7:[4184369, 4366297], 8:[4730156, 4912084], 9:[5275943, 5457871], 10:[5821730, 6003658], 11:[6367518, 6549446], 12:[6913305, 7095233], 13:[7459092, 7641020], 14:[8004879, 8186807], 15:[8550667, 8732595], 16:[9096454, 9278382], 17:[9642241, 9824169], 18:[10188028, 10369956], 19:[10733816, 10915744], 20:[11279603, 11461531], 21:[11825390, 12007318], 22:[12371177, 12553105], 23:[12916965, 13098893], 24:[13462752, 13644680], 25:[14008539, 14190467], 26:[14554326, 14736254], 27:[15100114, 15282042], 28:[15645901, 15827829], 29:[16191688, 16373616], 30:[16737475, 16919403], 31:[17283263, 17465191], 32:[17829050, 18010978], 33:[18374837, 18556765], 34:[18920624, 19102552], 35:[19466412, 19648340], 36:[20012199, 20194127], 37:[20557986, 20739914], 38:[21103773, 21285701], 39:[21649561, 21831489], 40:[22195348, 22377276], 41:[22741135, 22923063], 42:[23286922, 23468850], 43:[23832710, 24014638], 44:[24378497, 24560425], 45:[24924284, 25106212], 46:[25470071, 25651999], 47:[26015859, 26197787], 48:[26561646, 26743574], 49:[27107433, 27289361], 50:[27653220, 27835148], 51:[28199008, 28380936], 52:[28744795, 28926723], 53:[29290582, 29472510], 54:[29836369, 30018297], 55:[30382157, 30564085], 56:[30927944, 31109872], 57:[31473731, 31655659], 58:[32019518, 32201446], 59:[32565306, 32747234] }
Mon May 25 20:58:18 2026: Removed ≈  2% of redundant conclusions. [  585645 of approximately 29282280] (ETC: Mon May 25 23:32:13 2026 ; 2 h 33 min 54 s 890.74 ms remaining ; 2 h 37 min  3 s 357.70 ms total)
Mon May 25 21:01:27 2026: Removed ≈  4% of redundant conclusions. [ 1171291 of approximately 29282280] (ETC: Mon May 25 23:32:41 2026 ; 2 h 31 min 14 s 118.34 ms remaining ; 2 h 37 min 32 s 206.54 ms total)
Mon May 25 21:04:37 2026: Removed ≈  6% of redundant conclusions. [ 1756936 of approximately 29282280] (ETC: Mon May 25 23:32:55 2026 ; 2 h 28 min 17 s 544.28 ms remaining ; 2 h 37 min 45 s 472.36 ms total)
Mon May 25 21:07:48 2026: Removed ≈  8% of redundant conclusions. [ 2342582 of approximately 29282280] (ETC: Mon May 25 23:33:17 2026 ; 2 h 25 min 29 s   7.46 ms remaining ; 2 h 38 min  8 s  51.45 ms total)
Mon May 25 21:10:59 2026: Removed ≈ 10% of redundant conclusions. [ 2928228 of approximately 29282280] (ETC: Mon May 25 23:33:22 2026 ; 2 h 22 min 23 s 805.18 ms remaining ; 2 h 38 min 13 s 116.87 ms total)
Mon May 25 21:14:10 2026: Removed ≈ 12% of redundant conclusions. [ 3513873 of approximately 29282280] (ETC: Mon May 25 23:33:35 2026 ; 2 h 19 min 25 s 461.90 ms remaining ; 2 h 38 min 26 s 206.48 ms total)
Mon May 25 21:17:20 2026: Removed ≈ 14% of redundant conclusions. [ 4099519 of approximately 29282280] (ETC: Mon May 25 23:33:36 2026 ; 2 h 16 min 15 s 671.80 ms remaining ; 2 h 38 min 26 s 595.04 ms total)
Mon May 25 21:20:30 2026: Removed ≈ 16% of redundant conclusions. [ 4685164 of approximately 29282280] (ETC: Mon May 25 23:33:34 2026 ; 2 h 13 min  3 s 652.34 ms remaining ; 2 h 38 min 24 s 347.71 ms total)
Mon May 25 21:23:39 2026: Removed ≈ 18% of redundant conclusions. [ 5270810 of approximately 29282280] (ETC: Mon May 25 23:33:28 2026 ; 2 h  9 min 49 s 311.88 ms remaining ; 2 h 38 min 19 s 160.68 ms total)
Mon May 25 21:26:49 2026: Removed ≈ 20% of redundant conclusions. [ 5856456 of approximately 29282280] (ETC: Mon May 25 23:33:30 2026 ; 2 h  6 min 40 s 703.14 ms remaining ; 2 h 38 min 20 s 878.92 ms total)
Mon May 25 21:30:00 2026: Removed ≈ 22% of redundant conclusions. [ 6442101 of approximately 29282280] (ETC: Mon May 25 23:33:35 2026 ; 2 h  3 min 34 s 423.14 ms remaining ; 2 h 38 min 25 s 670.44 ms total)
Mon May 25 21:33:11 2026: Removed ≈ 24% of redundant conclusions. [ 7027747 of approximately 29282280] (ETC: Mon May 25 23:33:38 2026 ; 2 h        26 s 350.81 ms remaining ; 2 h 38 min 28 s 356.24 ms total)
Mon May 25 21:36:22 2026: Removed ≈ 26% of redundant conclusions. [ 7613392 of approximately 29282280] (ETC: Mon May 25 23:33:40 2026 ; 1 h 57 min 17 s 878.35 ms remaining ; 2 h 38 min 30 s 646.07 ms total)
Mon May 25 21:39:33 2026: Removed ≈ 28% of redundant conclusions. [ 8199038 of approximately 29282280] (ETC: Mon May 25 23:33:44 2026 ; 1 h 54 min 10 s 602.24 ms remaining ; 2 h 38 min 34 s 725.15 ms total)
Mon May 25 21:42:44 2026: Removed ≈ 30% of redundant conclusions. [ 8784684 of approximately 29282280] (ETC: Mon May 25 23:33:46 2026 ; 1 h 51 min  1 s 661.37 ms remaining ; 2 h 38 min 36 s 659.11 ms total)
Mon May 25 21:45:55 2026: Removed ≈ 32% of redundant conclusions. [ 9370329 of approximately 29282280] (ETC: Mon May 25 23:33:48 2026 ; 1 h 47 min 52 s 876.99 ms remaining ; 2 h 38 min 38 s 936.47 ms total)
Mon May 25 21:49:07 2026: Removed ≈ 34% of redundant conclusions. [ 9955975 of approximately 29282280] (ETC: Mon May 25 23:33:52 2026 ; 1 h 44 min 45 s  58.97 ms remaining ; 2 h 38 min 42 s 816.53 ms total)
Mon May 25 21:52:17 2026: Removed ≈ 36% of redundant conclusions. [10541620 of approximately 29282280] (ETC: Mon May 25 23:33:51 2026 ; 1 h 41 min 33 s 852.90 ms remaining ; 2 h 38 min 41 s 644.75 ms total)
Mon May 25 21:55:29 2026: Removed ≈ 38% of redundant conclusions. [11127266 of approximately 29282280] (ETC: Mon May 25 23:33:54 2026 ; 1 h 38 min 25 s 533.16 ms remaining ; 2 h 38 min 45 s  53.27 ms total)
Mon May 25 21:58:40 2026: Removed ≈ 40% of redundant conclusions. [11712912 of approximately 29282280] (ETC: Mon May 25 23:33:55 2026 ; 1 h 35 min 15 s 541.61 ms remaining ; 2 h 38 min 45 s 902.69 ms total)
Mon May 25 22:01:50 2026: Removed ≈ 42% of redundant conclusions. [12298557 of approximately 29282280] (ETC: Mon May 25 23:33:54 2026 ; 1 h 32 min  4 s 316.34 ms remaining ; 2 h 38 min 44 s 683.01 ms total)
Mon May 25 22:05:01 2026: Removed ≈ 44% of redundant conclusions. [12884203 of approximately 29282280] (ETC: Mon May 25 23:33:55 2026 ; 1 h 28 min 54 s 378.22 ms remaining ; 2 h 38 min 45 s 675.27 ms total)
Mon May 25 22:08:12 2026: Removed ≈ 46% of redundant conclusions. [13469848 of approximately 29282280] (ETC: Mon May 25 23:33:56 2026 ; 1 h 25 min 44 s 648.47 ms remaining ; 2 h 38 min 47 s 126.32 ms total)
Mon May 25 22:11:23 2026: Removed ≈ 48% of redundant conclusions. [14055494 of approximately 29282280] (ETC: Mon May 25 23:33:58 2026 ; 1 h 22 min 35 s  30.19 ms remaining ; 2 h 38 min 48 s 903.96 ms total)
Mon May 25 22:14:35 2026: Removed ≈ 50% of redundant conclusions. [14641140 of approximately 29282280] (ETC: Mon May 25 23:34:00 2026 ; 1 h 19 min 25 s 454.92 ms remaining ; 2 h 38 min 50 s 909.83 ms total)
Mon May 25 22:17:46 2026: Removed ≈ 52% of redundant conclusions. [15226785 of approximately 29282280] (ETC: Mon May 25 23:34:01 2026 ; 1 h 16 min 15 s 371.19 ms remaining ; 2 h 38 min 52 s  22.90 ms total)
Mon May 25 22:20:57 2026: Removed ≈ 54% of redundant conclusions. [15812431 of approximately 29282280] (ETC: Mon May 25 23:34:03 2026 ; 1 h 13 min  5 s 551.72 ms remaining ; 2 h 38 min 53 s 807.95 ms total)
Mon May 25 22:24:09 2026: Removed ≈ 56% of redundant conclusions. [16398076 of approximately 29282280] (ETC: Mon May 25 23:34:04 2026 ; 1 h  9 min 55 s 402.66 ms remaining ; 2 h 38 min 55 s   5.46 ms total)
Mon May 25 22:27:19 2026: Removed ≈ 58% of redundant conclusions. [16983722 of approximately 29282280] (ETC: Mon May 25 23:34:04 2026 ; 1 h  6 min 44 s 571.89 ms remaining ; 2 h 38 min 54 s 694.67 ms total)
Mon May 25 22:30:30 2026: Removed ≈ 60% of redundant conclusions. [17569368 of approximately 29282280] (ETC: Mon May 25 23:34:05 2026 ; 1 h  3 min 34 s 171.49 ms remaining ; 2 h 38 min 55 s 428.73 ms total)
Mon May 25 22:33:41 2026: Removed ≈ 62% of redundant conclusions. [18155013 of approximately 29282280] (ETC: Mon May 25 23:34:04 2026 ; 1 h        23 s  51.93 ms remaining ; 2 h 38 min 54 s 346.67 ms total)
Mon May 25 22:36:52 2026: Removed ≈ 64% of redundant conclusions. [18740659 of approximately 29282280] (ETC: Mon May 25 23:34:05 2026 ; 57 min 12 s 902.67 ms remaining ; 2 h 38 min 55 s 840.57 ms total)
Mon May 25 22:40:04 2026: Removed ≈ 66% of redundant conclusions. [19326304 of approximately 29282280] (ETC: Mon May 25 23:34:07 2026 ; 54 min  2 s 843.50 ms remaining ; 2 h 38 min 57 s 774.24 ms total)
Mon May 25 22:43:55 2026: Removed ≈ 68% of redundant conclusions. [19911950 of approximately 29282280] (ETC: Mon May 25 23:35:06 2026 ; 51 min 10 s 821.69 ms remaining ; 2 h 39 min 56 s 317.38 ms total)
Mon May 25 22:47:04 2026: Removed ≈ 70% of redundant conclusions. [20497596 of approximately 29282280] (ETC: Mon May 25 23:35:01 2026 ; 47 min 57 s 612.78 ms remaining ; 2 h 39 min 52 s  42.62 ms total)
Mon May 25 22:50:12 2026: Removed ≈ 72% of redundant conclusions. [21083241 of approximately 29282280] (ETC: Mon May 25 23:34:57 2026 ; 44 min 44 s 596.57 ms remaining ; 2 h 39 min 47 s 844.21 ms total)
Mon May 25 22:53:21 2026: Removed ≈ 74% of redundant conclusions. [21668887 of approximately 29282280] (ETC: Mon May 25 23:34:53 2026 ; 41 min 31 s 839.45 ms remaining ; 2 h 39 min 43 s 997.64 ms total)
Mon May 25 22:56:29 2026: Removed ≈ 76% of redundant conclusions. [22254532 of approximately 29282280] (ETC: Mon May 25 23:34:48 2026 ; 38 min 18 s 982.23 ms remaining ; 2 h 39 min 39 s  91.51 ms total)
Mon May 25 22:59:37 2026: Removed ≈ 78% of redundant conclusions. [22840178 of approximately 29282280] (ETC: Mon May 25 23:34:43 2026 ; 35 min  6 s 173.87 ms remaining ; 2 h 39 min 33 s 516.99 ms total)
Mon May 25 23:02:44 2026: Removed ≈ 80% of redundant conclusions. [23425824 of approximately 29282280] (ETC: Mon May 25 23:34:38 2026 ; 31 min 53 s 714.28 ms remaining ; 2 h 39 min 28 s 571.41 ms total)
Mon May 25 23:05:52 2026: Removed ≈ 82% of redundant conclusions. [24011469 of approximately 29282280] (ETC: Mon May 25 23:34:33 2026 ; 28 min 41 s 526.46 ms remaining ; 2 h 39 min 24 s  34.80 ms total)
Mon May 25 23:08:59 2026: Removed ≈ 84% of redundant conclusions. [24597115 of approximately 29282280] (ETC: Mon May 25 23:34:29 2026 ; 25 min 29 s 505.31 ms remaining ; 2 h 39 min 19 s 407.77 ms total)
Mon May 25 23:12:07 2026: Removed ≈ 86% of redundant conclusions. [25182760 of approximately 29282280] (ETC: Mon May 25 23:34:25 2026 ; 22 min 17 s 770.45 ms remaining ; 2 h 39 min 15 s 501.37 ms total)
Mon May 25 23:15:15 2026: Removed ≈ 88% of redundant conclusions. [25768406 of approximately 29282280] (ETC: Mon May 25 23:34:21 2026 ; 19 min  6 s 213.29 ms remaining ; 2 h 39 min 11 s 776.34 ms total)
Mon May 25 23:18:46 2026: Removed ≈ 90% of redundant conclusions. [26354052 of approximately 29282280] (ETC: Mon May 25 23:34:43 2026 ; 15 min 57 s 404.34 ms remaining ; 2 h 39 min 34 s  43.40 ms total)
Mon May 25 23:21:52 2026: Removed ≈ 92% of redundant conclusions. [26939697 of approximately 29282280] (ETC: Mon May 25 23:34:38 2026 ; 12 min 45 s 495.24 ms remaining ; 2 h 39 min 28 s 688.04 ms total)
Mon May 25 23:24:58 2026: Removed ≈ 94% of redundant conclusions. [27525343 of approximately 29282280] (ETC: Mon May 25 23:34:32 2026 ; 9 min 33 s 743.22 ms remaining ; 2 h 39 min 22 s 385.87 ms total)
Mon May 25 23:28:07 2026: Removed ≈ 96% of redundant conclusions. [28110988 of approximately 29282280] (ETC: Mon May 25 23:34:30 2026 ; 6 min 22 s 415.63 ms remaining ; 2 h 39 min 20 s 384.15 ms total)
[Rank 55] Workload transfer approved. Starting to work on 1:[1071360, 1084835].
[Rank 42] Workload transfer approved. Starting to work on 3:[2162935, 2176410].
[Rank 25] Workload transfer approved. Starting to work on 10:[5983445, 5996920].
[Rank 0] Workload transfer approved. Starting to work on 37:[20719701, 20733176].
Mon May 25 23:31:30 2026: Removed ≈ 98% of redundant conclusions. [28696634 of approximately 29282280] (ETC: Mon May 25 23:34:41 2026 ; 3 min 11 s 444.37 ms remaining ; 2 h 39 min 32 s 212.07 ms total)
[Rank 55] Workload transfer approved. Starting to work on 2:[1630623, 1635114].
[Rank 1] Workload transfer approved. Starting to work on 8:[4905347, 4909838].
[Rank 5] Workload transfer approved. Starting to work on 15:[8725858, 8730349].
[Rank 42] Workload transfer approved. Starting to work on 18:[10363219, 10367710].
[Rank 10] Workload transfer approved. Starting to work on 21:[12000581, 12005072].
[Rank 3] Workload transfer approved. Starting to work on 34:[19095815, 19100306].
[Rank 55] Workload transfer approved. Starting to work on 39:[21824752, 21829243].
[Rank 38] Workload transfer approved. Starting to work on 41:[22916326, 22920817].
[Rank 6] Workload transfer approved. Starting to work on 45:[25099475, 25103966].
[Rank 25] Workload transfer approved. Starting to work on 58:[32194709, 32199200].
[Rank 0] Workload transfer approved. Starting to work on 13:[7638775, 7640272].
[Rank 37] Workload transfer approved. Starting to work on 15:[8730350, 8731847].
[Rank 14] Workload transfer approved. Starting to work on 16:[9276137, 9277634].
[Rank 40] Workload transfer approved. Starting to work on 17:[9821924, 9823421].
[Rank 8] Workload transfer approved. Starting to work on 22:[12550860, 12552357].
[Rank 18] Workload transfer approved. Starting to work on 23:[13096648, 13098145].
[Rank 59] Workload transfer approved. Starting to work on 24:[13642435, 13643932].
[Rank 1] Workload transfer approved. Starting to work on 28:[15825584, 15827081].
[Rank 5] Workload transfer approved. Starting to work on 29:[16371371, 16372868].
[Rank 12] Workload transfer approved. Starting to work on 33:[18554520, 18556017].
[Rank 2] Workload transfer approved. Starting to work on 35:[19646095, 19647592].
[Rank 49] Workload transfer approved. Starting to work on 36:[20191882, 20193379].
[Rank 13] Workload transfer approved. Starting to work on 41:[22920818, 22922315].
[Rank 11] Workload transfer approved. Starting to work on 43:[24012393, 24013890].
[Rank 0] Workload transfer approved. Starting to work on 44:[24558180, 24559677].
[Rank 27] Workload transfer approved. Starting to work on 45:[25103967, 25105464].
[Rank 9] Workload transfer approved. Starting to work on 46:[25649754, 25651251].
[Rank 42] Workload transfer approved. Starting to work on 47:[26195542, 26197039].
[Rank 7] Workload transfer approved. Starting to work on 48:[26741329, 26742826].
[Rank 24] Workload transfer approved. Starting to work on 50:[27832903, 27834400].
[Rank 56] Workload transfer approved. Starting to work on 51:[28378691, 28380188].
[Rank 14] Workload transfer approved. Starting to work on 52:[28924478, 28925975].
[Rank 4] Workload transfer approved. Starting to work on 57:[31653414, 31654911].
[Rank 40] Workload transfer approved. Starting to work on 23:[13098146, 13098893].
[Rank 32] Workload transfer approved. Starting to work on 29:[16372869, 16373616].
[Rank 29] Workload transfer approved. Starting to work on 31:[17464444, 17465191].
[Rank 59] Workload transfer approved. Starting to work on 33:[18556018, 18556765].
[Rank 34] Workload transfer approved. Starting to work on 39:[21830742, 21831489].
[Rank 35] Workload transfer approved. Starting to work on 41:[22922316, 22923063].
[Rank 22] Workload transfer approved. Starting to work on 44:[24559678, 24560425].
[Rank 5] Workload transfer approved. Starting to work on 46:[25651252, 25651999].
[Rank 12] Workload transfer approved. Starting to work on 47:[26197040, 26197787].
[Rank 37] Workload transfer approved. Starting to work on 50:[27834401, 27835148].
[Rank 17] Workload transfer approved. Starting to work on 51:[28380189, 28380936].
[Rank 33] Workload transfer approved. Starting to work on 52:[28925976, 28926723].
[Rank 20] Workload transfer approved. Starting to work on 53:[29471763, 29472510].
[Rank 8] Workload transfer approved. Starting to work on 57:[31654912, 31655659].
[Rank 18] Workload transfer approved. Starting to work on 58:[32200699, 32201446].
9642661.62 ms (2 h 40 min 42 s 661.62 ms) taken to detect 29247374 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 3499861 representative and 29247374 redundant condensed detachment proof strings.
[Copy] Removal count: { 81, 29247374 }
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 1 on "n23m0097.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 2 on "n23m0101.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 3 on "n23m0114.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 4 on "n23m0121.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 5 on "n23m0125.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 6 on "n23m0134.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 7 on "n23m0135.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 8 on "n23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 9 on "n23m0144.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 10 on "n23m0166.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 11 on "n23m0168.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 12 on "n23m0175.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 13 on "n23m0199.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 14 on "n23m0211.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 15 on "n23m0292.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 16 on "n23m0295.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 17 on "n23m0300.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 18 on "n23m0302.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 19 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 20 on "n23m0308.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 21 on "n23m0311.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 22 on "n23m0313.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 23 on "n23m0317.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 24 on "n23m0321.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 25 on "n23m0323.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 26 on "n23m0324.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 27 on "n23m0327.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 28 on "n23m0328.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 29 on "n23m0331.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 30 on "n23m0335.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 31 on "n23m0338.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 32 on "n23m0340.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 33 on "n23m0352.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 34 on "n23m0353.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 35 on "n23m0354.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 36 on "n23m0355.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 37 on "r23m0043.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 38 on "r23m0044.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 39 on "r23m0048.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 40 on "r23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 41 on "r23m0051.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 42 on "r23m0053.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 43 on "r23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 44 on "r23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 45 on "r23m0057.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 46 on "r23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 47 on "r23m0059.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 48 on "r23m0060.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 49 on "r23m0061.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 50 on "r23m0063.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 51 on "r23m0064.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 52 on "r23m0069.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 53 on "r23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 54 on "r23m0072.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 55 on "r23m0074.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 56 on "r23m0080.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 57 on "r23m0083.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 58 on "r23m0088.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:35:51 2026: MPI-based D-proof representative filter complete. [rank 59 on "r23m0094.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
919.56 ms taken to filter and order new representative proofs.
Mon May 25 23:35:52 2026: Starting to write 3499861 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81.txt.
988.89 ms taken to print and save 782466043 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/dProofs-withConclusions/dProofs81.txt.
Mon May 25 23:35:53 2026: MPI-based D-proof representative filter complete. [rank 0 on "n23m0095.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts]
Mon May 25 23:36:26 2026: Process terminated. [pid: 161425, tid:22440770766656]
Mon May 25 23:36:26 2026: Process terminated. [pid: 126409, tid:23225349146432]
Mon May 25 23:36:26 2026: Process terminated. [pid: 297975, tid:22644580443968]
Mon May 25 23:36:26 2026: Process terminated. [pid: 83401, tid:22464947054400]
Mon May 25 23:36:26 2026: Process terminated. [pid: 173217, tid:22370950539072]
Mon May 25 23:36:26 2026: Process terminated. [pid: 25356, tid:22833542047552]
Mon May 25 23:36:26 2026: Process terminated. [pid: 39821, tid:23385999095616]
Mon May 25 23:36:26 2026: Process terminated. [pid: 366591, tid:23287147882304]
Mon May 25 23:36:26 2026: Process terminated. [pid: 94413, tid:22759996147520]
Mon May 25 23:36:26 2026: Process terminated. [pid: 518610, tid:23422816601920]
Mon May 25 23:36:26 2026: Process terminated. [pid: 55200, tid:23075115525952]
Mon May 25 23:36:26 2026: Process terminated. [pid: 460859, tid:22574477944640]
Mon May 25 23:36:26 2026: Process terminated. [pid: 18463, tid:23339677034304]
Mon May 25 23:36:26 2026: Process terminated. [pid: 115703, tid:23404261353280]
Mon May 25 23:36:26 2026: Process terminated. [pid: 111414, tid:23378627954496]
Mon May 25 23:36:26 2026: Process terminated. [pid: 261319, tid:23171622348608]
Mon May 25 23:36:26 2026: Process terminated. [pid: 167377, tid:22931563050816]
Mon May 25 23:36:26 2026: Process terminated. [pid: 322533, tid:23143535040320]
Mon May 25 23:36:26 2026: Process terminated. [pid: 218132, tid:22514229622592]
Mon May 25 23:36:26 2026: Process terminated. [pid: 51705, tid:22482542163776]
Mon May 25 23:36:26 2026: Process terminated. [pid: 274765, tid:22438300563264]
Mon May 25 23:36:26 2026: Process terminated. [pid: 82642, tid:22507514943296]
Mon May 25 23:36:26 2026: Process terminated. [pid: 239331, tid:22774772193088]
Mon May 25 23:36:26 2026: Process terminated. [pid: 518034, tid:23422632130368]
Mon May 25 23:36:26 2026: Process terminated. [pid: 336418, tid:22651077191488]
Mon May 25 23:36:26 2026: Process terminated. [pid: 513427, tid:22658757551936]
Mon May 25 23:36:26 2026: Process terminated. [pid: 458645, tid:22451160233792]
Mon May 25 23:36:26 2026: Process terminated. [pid: 61060, tid:22431195334464]
Mon May 25 23:36:26 2026: Process terminated. [pid: 200906, tid:22889763923776]
Mon May 25 23:36:26 2026: Process terminated. [pid: 380067, tid:22680538347328]
Mon May 25 23:36:26 2026: Process terminated. [pid: 372717, tid:23453741684544]
Mon May 25 23:36:26 2026: Process terminated. [pid: 467612, tid:23369280456512]
Mon May 25 23:36:26 2026: Process terminated. [pid: 442408, tid:23405289076544]
Mon May 25 23:36:26 2026: Process terminated. [pid: 248607, tid:22618467972928]
Mon May 25 23:36:26 2026: Process terminated. [pid: 44474, tid:22839143622464]
Mon May 25 23:36:26 2026: Process terminated. [pid: 67188, tid:23324194113344]
Mon May 25 23:36:26 2026: Process terminated. [pid: 374491, tid:23191698212672]
Mon May 25 23:36:26 2026: Process terminated. [pid: 222058, tid:23375360149312]
Mon May 25 23:36:26 2026: Process terminated. [pid: 412226, tid:22369879308096]
Mon May 25 23:36:26 2026: Process terminated. [pid: 358581, tid:22684290385728]
Mon May 25 23:36:26 2026: Process terminated. [pid: 340662, tid:23070401922880]
Mon May 25 23:36:26 2026: Process terminated. [pid: 514404, tid:22441746474816]
Mon May 25 23:36:26 2026: Process terminated. [pid: 9867, tid:23018638059328]
Mon May 25 23:36:26 2026: Process terminated. [pid: 375497, tid:22956122691392]
Mon May 25 23:36:26 2026: Process terminated. [pid: 67779, tid:22383466014528]
Mon May 25 23:36:26 2026: Process terminated. [pid: 497673, tid:22769969538880]
Mon May 25 23:36:26 2026: Process terminated. [pid: 325173, tid:22581571450688]
Mon May 25 23:36:26 2026: Process terminated. [pid: 436128, tid:22826284123968]
Mon May 25 23:36:26 2026: Process terminated. [pid: 161162, tid:22502989281088]
Mon May 25 23:36:26 2026: Process terminated. [pid: 283948, tid:22688989734720]
Mon May 25 23:36:26 2026: Process terminated. [pid: 315562, tid:22372034897728]
Mon May 25 23:36:26 2026: Process terminated. [pid: 419217, tid:23158069966656]
Mon May 25 23:36:26 2026: Process terminated. [pid: 479052, tid:23433203853120]
Mon May 25 23:36:26 2026: Process terminated. [pid: 243825, tid:23155956434752]
Mon May 25 23:36:26 2026: Process terminated. [pid: 129898, tid:23380639000384]
Mon May 25 23:36:26 2026: Process terminated. [pid: 133775, tid:23316327855936]
Mon May 25 23:36:27 2026: Process terminated. [pid: 425414, tid:22565365000000]
Mon May 25 23:36:27 2026: Process terminated. [pid: 93902, tid:22658761324352]
Mon May 25 23:36:27 2026: Process terminated. [pid: 478469, tid:22901412648768]
Mon May 25 23:36:27 2026: Process terminated. [pid: 216173, tid:23225495660352]