dProofs137_48node_2304cpu.log

( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'.
  The run was executed on 48 CLAIX-2018 MPI nodes
  — 2-socket Intel Xeon Platinum 8160 (Skylake) each, 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory each —
  running Linux, Rocky 8.8. Initialization and completion messages with rank numbers have been grouped and sorted for better readability.
  Wall-clock time:    2.9113888… h
  CPU utilization: 6707.84 core-h )
Sun Oct  1 11:56:29 2023: Process started. [pid: 162953, tid:22883746346880]
Sun Oct  1 11:56:29 2023: Process started. [pid: 228572, tid:22686815242112]
Sun Oct  1 11:56:29 2023: Process started. [pid: 103566, tid:23389857654656]
Sun Oct  1 11:56:29 2023: Process started. [pid: 260994, tid:22660369487744]
Sun Oct  1 11:56:29 2023: Process started. [pid: 6028, tid:22658019436416]
Sun Oct  1 11:56:29 2023: Process started. [pid: 102522, tid:22668398028672]
Sun Oct  1 11:56:29 2023: Process started. [pid: 256496, tid:22371252995968]
Sun Oct  1 11:56:29 2023: Process started. [pid: 210847, tid:23437190748032]
Sun Oct  1 11:56:29 2023: Process started. [pid: 16572, tid:22824990521216]
Sun Oct  1 11:56:29 2023: Process started. [pid: 200307, tid:23243528345472]
Sun Oct  1 11:56:29 2023: Process started. [pid: 223862, tid:23274358183808]
Sun Oct  1 11:56:29 2023: Process started. [pid: 206927, tid:22740393527168]
Sun Oct  1 11:56:29 2023: Process started. [pid: 257248, tid:23410566924160]
Sun Oct  1 11:56:29 2023: Process started. [pid: 270316, tid:22476426356608]
Sun Oct  1 11:56:29 2023: Process started. [pid: 267968, tid:22708276672384]
Sun Oct  1 11:56:29 2023: Process started. [pid: 227619, tid:22953816307584]
Sun Oct  1 11:56:29 2023: Process started. [pid: 63926, tid:22827390928768]
Sun Oct  1 11:56:29 2023: Process started. [pid: 249424, tid:22711862007680]
Sun Oct  1 11:56:29 2023: Process started. [pid: 223225, tid:22924446844800]
Sun Oct  1 11:56:29 2023: Process started. [pid: 72713, tid:22934036006784]
Sun Oct  1 11:56:30 2023: Process started. [pid: 224635, tid:23107796805504]
Sun Oct  1 11:56:30 2023: Process started. [pid: 275006, tid:23253744117632]
Sun Oct  1 11:56:30 2023: Process started. [pid: 250254, tid:22942087788416]
Sun Oct  1 11:56:30 2023: Process started. [pid: 1438, tid:23001885915008]
Sun Oct  1 11:56:30 2023: Process started. [pid: 219016, tid:23385297700736]
Sun Oct  1 11:56:30 2023: Process started. [pid: 274763, tid:23206316066688]
Sun Oct  1 11:56:30 2023: Process started. [pid: 276962, tid:22756119312256]
Sun Oct  1 11:56:30 2023: Process started. [pid: 235377, tid:23380255713152]
Sun Oct  1 11:56:30 2023: Process started. [pid: 255142, tid:22772861208448]
Sun Oct  1 11:56:30 2023: Process started. [pid: 22859, tid:22540687116160]
Sun Oct  1 11:56:30 2023: Process started. [pid: 195651, tid:23293449389952]
Sun Oct  1 11:56:30 2023: Process started. [pid: 224584, tid:23427456882560]
Sun Oct  1 11:56:30 2023: Process started. [pid: 230129, tid:22850536327040]
Sun Oct  1 11:56:30 2023: Process started. [pid: 92970, tid:23432791201664]
Sun Oct  1 11:56:30 2023: Process started. [pid: 41545, tid:23371999139712]
Sun Oct  1 11:56:30 2023: Process started. [pid: 149358, tid:23335155562368]
Sun Oct  1 11:56:30 2023: Process started. [pid: 158176, tid:22629302286208]
Sun Oct  1 11:56:30 2023: Process started. [pid: 145846, tid:22898531383168]
Sun Oct  1 11:56:30 2023: Process started. [pid: 242375, tid:22453605508992]
Sun Oct  1 11:56:30 2023: Process started. [pid: 206445, tid:23262505375616]
Sun Oct  1 11:56:30 2023: Process started. [pid: 174746, tid:22384182241152]
Sun Oct  1 11:56:30 2023: Process started. [pid: 95570, tid:22513916409728]
Sun Oct  1 11:56:30 2023: Process started. [pid: 139173, tid:23399086483328]
Sun Oct  1 11:56:30 2023: Process started. [pid: 240930, tid:22703855765376]
Sun Oct  1 11:56:30 2023: Process started. [pid: 157248, tid:22497801869184]
Sun Oct  1 11:56:30 2023: Process started. [pid: 194382, tid:23420537935744]
Sun Oct  1 11:56:30 2023: Process started. [pid: 163122, tid:22902969030528]
Sun Oct  1 11:56:30 2023: Process started. [pid: 118291, tid:23254672766848]
Tasks:
1. resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true)
2. mpi_filterDProofRepresentativeFile(137, true)

[Rank 0 ; pid: 118291 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c]
(1) CC0CCN0.1.2C3CCN4C2.4C0.4    -    CCpCCNpqrCsCCNtCrtCpt    -    (0\imply((\not0\imply1)\imply2))\imply(3\imply((\not4\imply(2\imply4))\imply(0\imply4)))
[Rank 1 ; pid: 240930 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 2 ; pid: 149358 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 3 ; pid: 92970 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 4 ; pid: 1438 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 5 ; pid: 139173 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 6 ; pid: 163122 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 7 ; pid: 22859 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 8 ; pid: 158176 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 9 ; pid: 223225 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 10 ; pid: 250254 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 11 ; pid: 276962 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 12 ; pid: 145846 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 13 ; pid: 227619 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 14 ; pid: 219016 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 15 ; pid: 224584 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 16 ; pid: 275006 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 17 ; pid: 102522 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 18 ; pid: 16572 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 19 ; pid: 174746 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 20 ; pid: 257248 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 21 ; pid: 95570 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 22 ; pid: 72713 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 23 ; pid: 195651 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 24 ; pid: 210847 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 25 ; pid: 200307 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 26 ; pid: 194382 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 27 ; pid: 256496 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 28 ; pid: 242375 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 29 ; pid: 228572 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 30 ; pid: 206927 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 31 ; pid: 235377 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 32 ; pid: 41545 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 33 ; pid: 255142 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 34 ; pid: 223862 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 35 ; pid: 224635 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 36 ; pid: 270316 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 37 ; pid: 260994 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 38 ; pid: 274763 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 39 ; pid: 230129 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 40 ; pid: 162953 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 41 ; pid: 249424 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 42 ; pid: 267968 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 43 ; pid: 6028 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 44 ; pid: 206445 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 45 ; pid: 157248 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 46 ; pid: 103566 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 47 ; pid: 63926 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently.
[Rank 0 ; pid: 118291 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 1 ; pid: 240930 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 2 ; pid: 149358 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 3 ; pid: 92970 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 4 ; pid: 1438 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 5 ; pid: 139173 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 6 ; pid: 163122 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 7 ; pid: 22859 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 8 ; pid: 158176 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 9 ; pid: 223225 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 10 ; pid: 250254 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 11 ; pid: 276962 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 12 ; pid: 145846 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 13 ; pid: 227619 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 14 ; pid: 219016 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 15 ; pid: 224584 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 16 ; pid: 275006 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 17 ; pid: 102522 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 18 ; pid: 16572 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 19 ; pid: 174746 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 20 ; pid: 257248 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 21 ; pid: 95570 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 22 ; pid: 72713 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 23 ; pid: 195651 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 24 ; pid: 210847 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 25 ; pid: 200307 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 26 ; pid: 194382 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 27 ; pid: 256496 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 28 ; pid: 242375 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 29 ; pid: 228572 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 30 ; pid: 206927 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 31 ; pid: 235377 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 32 ; pid: 41545 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 33 ; pid: 255142 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 34 ; pid: 223862 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 35 ; pid: 224635 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 36 ; pid: 270316 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 37 ; pid: 260994 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 38 ; pid: 274763 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 39 ; pid: 230129 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 40 ; pid: 162953 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 41 ; pid: 249424 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 42 ; pid: 267968 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 43 ; pid: 6028 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 44 ; pid: 206445 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 45 ; pid: 157248 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 46 ; pid: 103566 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
[Rank 47 ; pid: 63926 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true).
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0597.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0604.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0608.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0612.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 4 on "nrm081.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 5 on "nrm082.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 6 on "nrm084.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 7 on "nrm085.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 8 on "nrm088.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 9 on "nrm089.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 10 on "nrm091.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 11 on "nrm092.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 12 on "nrm095.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 13 on "nrm096.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 14 on "nrm097.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 15 on "nrm098.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 16 on "nrm099.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 17 on "nrm100.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 18 on "nrm101.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 19 on "nrm102.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 20 on "nrm103.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 21 on "nrm104.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 22 on "nrm105.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 23 on "nrm107.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 24 on "nrm109.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 25 on "nrm110.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 26 on "nrm111.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 27 on "nrm113.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 28 on "nrm115.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 29 on "nrm116.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 30 on "nrm117.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 31 on "nrm118.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 32 on "nrm120.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 33 on "nrm121.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 34 on "nrm123.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 35 on "nrm124.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 36 on "nrm125.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 37 on "nrm126.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 38 on "nrm128.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 39 on "nrm130.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 40 on "nrm132.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 41 on "nrm133.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 42 on "nrm135.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 43 on "nrm138.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 44 on "nrm139.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 45 on "nrm142.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 46 on "nrm143.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 47 on "nrm144.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
0.05 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23254489204480]
3.32 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23254497609472]
4.39 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23254470293248]
0.26 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23254466090752]
1.45 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23254468192000]
2.05 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23254485001984]
0.16 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23254472394496]
1.07 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23254474495744]
0.70 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23254463989504]
0.72 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23254480799488]
0.30 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23254455584512]
0.31 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23254461888256]
0.53 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23254495508224]
0.53 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23254493406976]
0.39 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23254482900736]
0.20 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23254445078272]
2.78 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23254453483264]
2.84 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23254487103232]
0.03 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23254451382016]
482.34 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23254497609472]
1781.04 ms (1 s 781.04 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23254495508224]
2405.00 ms (2 s 405.00 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23254493406976]
3.67 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23254491305728]
446.43 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23254489204480]
4279.90 ms (4 s 279.90 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23254487103232]
3697.05 ms (3 s 697.05 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23254485001984]
3004.60 ms (3 s 4.60 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23254482900736]
713.88 ms taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23254480799488]
0.04 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23254478698240]
21.37 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23254476596992]
7029.36 ms (7 s 29.36 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23254474495744]
4344.45 ms (4 s 344.45 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23254472394496]
1591.38 ms (1 s 591.38 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23254470293248]
2279.08 ms (2 s 279.08 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23254468192000]
1550.48 ms (1 s 550.48 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23254466090752]
1639.28 ms (1 s 639.28 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23254463989504]
1961.78 ms (1 s 961.78 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23254461888256]
9.38 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23254459787008]
21.99 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23254457685760]
911.18 ms taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23254455584512]
3692.93 ms (3 s 692.93 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23254453483264]
4341.32 ms (4 s 341.32 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23254451382016]
1.59 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23254449280768]
12.52 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23254447179520]
3188.89 ms (3 s 188.89 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23254445078272]
6.35 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23254442977024]
2.89 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23254440875776]
16.87 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23254438774528]
173.42 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23254436673280]
9.94 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23254434572032]
6.27 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23254432470784]
10.37 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23252348958464]
29.36 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23252214740736]
24.23 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23252346857216]
30.20 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23252344755968]
32.97 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23252342654720]
26.06 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23252340553472]
31.27 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23252338452224]
41.91 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23252336350976]
42.78 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23252334249728]
67.61 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23252332148480]
76.68 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23252330047232]
206.22 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23252327945984]
76.99 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23252325844736]
102.00 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23252323743488]
296.71 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23252321642240]
214.56 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23252319540992]
7087.01 ms (7 s 87.01 ms) total read duration.
Loaded 68 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 2
9 : 1
11 : 0
13 : 1
15 : 2
17 : 3
19 : 4
21 : 5
23 : 5
25 : 5
27 : 6
29 : 7
31 : 15
33 : 20
35 : 25
37 : 30
39 : 37
41 : 42
43 : 51
45 : 63
47 : 85
49 : 122
51 : 162
53 : 206
55 : 251
57 : 292
59 : 339
61 : 444
63 : 598
65 : 781
67 : 1016
69 : 1303
71 : 1593
73 : 1922
75 : 2359
77 : 2986
79 : 3875
81 : 5006
83 : 6466
85 : 8184
87 : 10182
89 : 12488
91 : 15534
93 : 19614
95 : 25087
97 : 32452
99 : 41840
101 : 53343
103 : 67105
105 : 84222
107 : 105925
109 : 134564
111 : 172053
113 : 221055
115 : 283569
117 : 361751
119 : 458509
121 : 579502
123 : 734352
125 : 935212
127 : 1197027
129 : 1534565
131 : 1965596
133 : 2509883
135 : 3196594
14790342 representatives in total.
5733.95 ms (5 s 733.95 ms) taken to read 10430172 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137-unfiltered137+.txt. [tid:23252319540992]
5735.24 ms (5 s 735.24 ms) additional read duration.
Loaded 1 more representative collection of size:
137 : 10430172
25220514 representatives in total.
Sun Oct  1 11:56:46 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 6392697, based on entry 135:5001838 and last known pair (133:3913588, 135:5001838) with 5001838/3913588 ≈ 1.27807 and 5001838 * (5001838/3913588)^1 ≈ 6392697.28.
Sun Oct  1 11:56:47 2023: Inserted ≈ 5% of D-proof conclusions. [ 1261025 of 25220514] (ETC: Sun Oct  1 11:57:05 2023 ; 18 s 355.32 ms remaining ; 19 s 321.39 ms total)
Sun Oct  1 11:56:48 2023: Inserted ≈10% of D-proof conclusions. [ 2522051 of 25220514] (ETC: Sun Oct  1 11:57:05 2023 ; 17 s 503.37 ms remaining ; 19 s 448.19 ms total)
Sun Oct  1 11:56:48 2023: Inserted ≈15% of D-proof conclusions. [ 3783077 of 25220514] (ETC: Sun Oct  1 11:57:04 2023 ; 15 s 982.49 ms remaining ; 18 s 802.93 ms total)
Sun Oct  1 11:56:49 2023: Inserted ≈20% of D-proof conclusions. [ 5044102 of 25220514] (ETC: Sun Oct  1 11:57:03 2023 ; 14 s 233.13 ms remaining ; 17 s 791.41 ms total)
Sun Oct  1 11:56:50 2023: Inserted ≈25% of D-proof conclusions. [ 6305128 of 25220514] (ETC: Sun Oct  1 11:57:03 2023 ; 12 s 810.90 ms remaining ; 17 s  81.20 ms total)
Sun Oct  1 11:56:51 2023: Inserted ≈30% of D-proof conclusions. [ 7566154 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 11 s 672.13 ms remaining ; 16 s 674.47 ms total)
Sun Oct  1 11:56:51 2023: Inserted ≈35% of D-proof conclusions. [ 8827179 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 10 s 811.32 ms remaining ; 16 s 632.80 ms total)
Sun Oct  1 11:56:52 2023: Inserted ≈40% of D-proof conclusions. [10088205 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 9 s 696.71 ms remaining ; 16 s 161.18 ms total)
Sun Oct  1 11:56:53 2023: Inserted ≈45% of D-proof conclusions. [11349231 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 8 s 735.49 ms remaining ; 15 s 882.71 ms total)
Sun Oct  1 11:56:53 2023: Inserted ≈50% of D-proof conclusions. [12610257 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 7 s 844.84 ms remaining ; 15 s 689.68 ms total)
Sun Oct  1 11:56:54 2023: Inserted ≈55% of D-proof conclusions. [13871282 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 7 s 102.96 ms remaining ; 15 s 784.36 ms total)
Sun Oct  1 11:56:55 2023: Inserted ≈60% of D-proof conclusions. [15132308 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 6 s 269.61 ms remaining ; 15 s 674.02 ms total)
Sun Oct  1 11:56:56 2023: Inserted ≈65% of D-proof conclusions. [16393334 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 5 s 482.55 ms remaining ; 15 s 664.44 ms total)
Sun Oct  1 11:56:57 2023: Inserted ≈70% of D-proof conclusions. [17654359 of 25220514] (ETC: Sun Oct  1 11:57:01 2023 ; 4 s 740.02 ms remaining ; 15 s 800.08 ms total)
Sun Oct  1 11:56:58 2023: Inserted ≈75% of D-proof conclusions. [18915385 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 4 s   4.48 ms remaining ; 16 s  17.93 ms total)
Sun Oct  1 11:56:59 2023: Inserted ≈80% of D-proof conclusions. [20176411 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 3 s 239.52 ms remaining ; 16 s 197.61 ms total)
Sun Oct  1 11:57:00 2023: Inserted ≈85% of D-proof conclusions. [21437436 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 2 s 460.52 ms remaining ; 16 s 403.45 ms total)
Sun Oct  1 11:57:00 2023: Inserted ≈90% of D-proof conclusions. [22698462 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 1 s 654.04 ms remaining ; 16 s 540.43 ms total)
Sun Oct  1 11:57:01 2023: Inserted ≈95% of D-proof conclusions. [23959488 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 832.72 ms remaining ; 16 s 654.42 ms total)
Sun Oct  1 11:57:02 2023: Inserted 100% of D-proof conclusions. [25220514 of 25220514] (ETC: Sun Oct  1 11:57:02 2023 ; 0.00 ms remaining ; 16 s 749.51 ms total)
16749.60 ms (16 s 749.60 ms) total insertion duration.
Reservable workloads: { 0:[144864, 217294], 1:[362159, 434589], 2:[579454, 651884], 3:[796749, 869180], 4:[1014045, 1086475], 5:[1231340, 1303770], 6:[1448635, 1521065], 7:[1665930, 1738361], 8:[1883226, 1955656], 9:[2100521, 2172951], 10:[2317816, 2390246], 11:[2535111, 2607542], 12:[2752407, 2824837], 13:[2969702, 3042132], 14:[3186997, 3259427], 15:[3404292, 3476723], 16:[3621588, 3694018], 17:[3838883, 3911313], 18:[4056178, 4128608], 19:[4273473, 4345904], 20:[4490769, 4563199], 21:[4708064, 4780494], 22:[4925359, 4997789], 23:[5142654, 5215085], 24:[5359950, 5432380], 25:[5577245, 5649675], 26:[5794540, 5866970], 27:[6011835, 6084266], 28:[6229131, 6301561], 29:[6446426, 6518856], 30:[6663721, 6736151], 31:[6881016, 6953447], 32:[7098312, 7170742], 33:[7315607, 7388037], 34:[7532902, 7605332], 35:[7750197, 7822628], 36:[7967493, 8039923], 37:[8184788, 8257218], 38:[8402083, 8474513], 39:[8619378, 8691809], 40:[8836674, 8909104], 41:[9053969, 9126399], 42:[9271264, 9343694], 43:[9488559, 9560990], 44:[9705855, 9778285], 45:[9923150, 9995580], 46:[10140445, 10212875], 47:[10357740, 10430171] }
Sun Oct  1 12:00:40 2023: Removed ≈  2% of redundant conclusions. [ 127853 of approximately 6392697] (ETC: Sun Oct  1 14:57:47 2023 ; 2 h 57 min  6 s 839.72 ms remaining ; 3 h        43 s 712.37 ms total)
Sun Oct  1 12:04:17 2023: Removed ≈  4% of redundant conclusions. [ 255707 of approximately 6392697] (ETC: Sun Oct  1 14:57:39 2023 ; 2 h 53 min 22 s 637.49 ms remaining ; 3 h        36 s  79.17 ms total)
Sun Oct  1 12:07:51 2023: Removed ≈  6% of redundant conclusions. [ 383561 of approximately 6392697] (ETC: Sun Oct  1 14:57:02 2023 ; 2 h 49 min 11 s  33.27 ms remaining ; 2 h 59 min 58 s 970.09 ms total)
Sun Oct  1 12:11:27 2023: Removed ≈  8% of redundant conclusions. [ 511415 of approximately 6392697] (ETC: Sun Oct  1 14:56:57 2023 ; 2 h 45 min 29 s 928.03 ms remaining ; 2 h 59 min 53 s 398.64 ms total)
Sun Oct  1 12:14:59 2023: Removed ≈ 10% of redundant conclusions. [ 639269 of approximately 6392697] (ETC: Sun Oct  1 14:56:22 2023 ; 2 h 41 min 22 s 871.00 ms remaining ; 2 h 59 min 18 s 744.25 ms total)
Sun Oct  1 12:18:31 2023: Removed ≈ 12% of redundant conclusions. [ 767123 of approximately 6392697] (ETC: Sun Oct  1 14:55:55 2023 ; 2 h 37 min 24 s  54.69 ms remaining ; 2 h 58 min 51 s 879.10 ms total)
Sun Oct  1 12:22:04 2023: Removed ≈ 14% of redundant conclusions. [ 894977 of approximately 6392697] (ETC: Sun Oct  1 14:55:42 2023 ; 2 h 33 min 38 s 413.96 ms remaining ; 2 h 58 min 39 s  84.87 ms total)
Sun Oct  1 12:25:34 2023: Removed ≈ 16% of redundant conclusions. [1022831 of approximately 6392697] (ETC: Sun Oct  1 14:55:18 2023 ; 2 h 29 min 43 s 712.05 ms remaining ; 2 h 58 min 14 s 894.26 ms total)
Sun Oct  1 12:29:07 2023: Removed ≈ 18% of redundant conclusions. [1150685 of approximately 6392697] (ETC: Sun Oct  1 14:55:13 2023 ; 2 h 26 min  6 s   5.32 ms remaining ; 2 h 58 min 10 s 249.45 ms total)
Sun Oct  1 12:32:37 2023: Removed ≈ 20% of redundant conclusions. [1278539 of approximately 6392697] (ETC: Sun Oct  1 14:54:50 2023 ; 2 h 22 min 13 s 699.41 ms remaining ; 2 h 57 min 47 s 123.43 ms total)
Sun Oct  1 12:36:05 2023: Removed ≈ 22% of redundant conclusions. [1406393 of approximately 6392697] (ETC: Sun Oct  1 14:54:26 2023 ; 2 h 18 min 21 s 641.87 ms remaining ; 2 h 57 min 23 s 129.88 ms total)
Sun Oct  1 12:39:34 2023: Removed ≈ 24% of redundant conclusions. [1534247 of approximately 6392697] (ETC: Sun Oct  1 14:54:11 2023 ; 2 h 14 min 37 s 113.11 ms remaining ; 2 h 57 min  7 s 779.80 ms total)
Sun Oct  1 12:43:02 2023: Removed ≈ 26% of redundant conclusions. [1662101 of approximately 6392697] (ETC: Sun Oct  1 14:53:54 2023 ; 2 h 10 min 52 s  72.81 ms remaining ; 2 h 56 min 50 s 908.71 ms total)
Sun Oct  1 12:46:30 2023: Removed ≈ 28% of redundant conclusions. [1789955 of approximately 6392697] (ETC: Sun Oct  1 14:53:39 2023 ; 2 h  7 min  8 s 978.22 ms remaining ; 2 h 56 min 35 s 802.72 ms total)
Sun Oct  1 12:49:57 2023: Removed ≈ 30% of redundant conclusions. [1917809 of approximately 6392697] (ETC: Sun Oct  1 14:53:24 2023 ; 2 h  3 min 26 s 421.32 ms remaining ; 2 h 56 min 20 s 601.65 ms total)
Sun Oct  1 12:53:23 2023: Removed ≈ 32% of redundant conclusions. [2045663 of approximately 6392697] (ETC: Sun Oct  1 14:53:04 2023 ; 1 h 59 min 41 s 590.37 ms remaining ; 2 h 56 min  1 s 162.21 ms total)
Sun Oct  1 12:56:47 2023: Removed ≈ 34% of redundant conclusions. [2173516 of approximately 6392697] (ETC: Sun Oct  1 14:52:43 2023 ; 1 h 55 min 56 s  23.31 ms remaining ; 2 h 55 min 39 s 426.80 ms total)
Sun Oct  1 13:00:12 2023: Removed ≈ 36% of redundant conclusions. [2301370 of approximately 6392697] (ETC: Sun Oct  1 14:52:28 2023 ; 1 h 52 min 15 s 740.69 ms remaining ; 2 h 55 min 24 s 592.47 ms total)
Sun Oct  1 13:03:37 2023: Removed ≈ 38% of redundant conclusions. [2429224 of approximately 6392697] (ETC: Sun Oct  1 14:52:12 2023 ; 1 h 48 min 35 s 664.49 ms remaining ; 2 h 55 min  9 s 134.00 ms total)
Sun Oct  1 13:06:59 2023: Removed ≈ 40% of redundant conclusions. [2557078 of approximately 6392697] (ETC: Sun Oct  1 14:51:53 2023 ; 1 h 44 min 53 s 944.78 ms remaining ; 2 h 54 min 49 s 905.77 ms total)
Sun Oct  1 13:10:21 2023: Removed ≈ 42% of redundant conclusions. [2684932 of approximately 6392697] (ETC: Sun Oct  1 14:51:34 2023 ; 1 h 41 min 13 s 176.86 ms remaining ; 2 h 54 min 30 s 992.50 ms total)
Sun Oct  1 13:13:44 2023: Removed ≈ 44% of redundant conclusions. [2812786 of approximately 6392697] (ETC: Sun Oct  1 14:51:19 2023 ; 1 h 37 min 35 s 398.81 ms remaining ; 2 h 54 min 16 s  67.33 ms total)
Sun Oct  1 13:17:06 2023: Removed ≈ 46% of redundant conclusions. [2940640 of approximately 6392697] (ETC: Sun Oct  1 14:51:04 2023 ; 1 h 33 min 57 s 864.79 ms remaining ; 2 h 54 min      488.47 ms total)
Sun Oct  1 13:20:28 2023: Removed ≈ 48% of redundant conclusions. [3068494 of approximately 6392697] (ETC: Sun Oct  1 14:50:50 2023 ; 1 h 30 min 21 s 981.31 ms remaining ; 2 h 53 min 46 s 885.38 ms total)
Sun Oct  1 13:23:51 2023: Removed ≈ 50% of redundant conclusions. [3196348 of approximately 6392697] (ETC: Sun Oct  1 14:50:38 2023 ; 1 h 26 min 47 s 572.10 ms remaining ; 2 h 53 min 35 s 142.58 ms total)
Sun Oct  1 13:27:14 2023: Removed ≈ 52% of redundant conclusions. [3324202 of approximately 6392697] (ETC: Sun Oct  1 14:50:29 2023 ; 1 h 23 min 14 s 587.87 ms remaining ; 2 h 53 min 25 s 389.90 ms total)
Sun Oct  1 13:30:38 2023: Removed ≈ 54% of redundant conclusions. [3452056 of approximately 6392697] (ETC: Sun Oct  1 14:50:21 2023 ; 1 h 19 min 42 s 942.90 ms remaining ; 2 h 53 min 17 s 700.61 ms total)
Sun Oct  1 13:34:01 2023: Removed ≈ 56% of redundant conclusions. [3579910 of approximately 6392697] (ETC: Sun Oct  1 14:50:12 2023 ; 1 h 16 min 11 s  69.32 ms remaining ; 2 h 53 min  8 s 792.73 ms total)
Sun Oct  1 13:37:24 2023: Removed ≈ 58% of redundant conclusions. [3707764 of approximately 6392697] (ETC: Sun Oct  1 14:50:03 2023 ; 1 h 12 min 39 s 574.01 ms remaining ; 2 h 52 min 59 s 937.11 ms total)
Sun Oct  1 13:40:46 2023: Removed ≈ 60% of redundant conclusions. [3835618 of approximately 6392697] (ETC: Sun Oct  1 14:49:54 2023 ; 1 h  9 min  8 s 379.66 ms remaining ; 2 h 52 min 50 s 948.34 ms total)
Sun Oct  1 13:44:10 2023: Removed ≈ 62% of redundant conclusions. [3963472 of approximately 6392697] (ETC: Sun Oct  1 14:49:49 2023 ; 1 h  5 min 39 s 106.45 ms remaining ; 2 h 52 min 46 s  69.01 ms total)
Sun Oct  1 13:47:33 2023: Removed ≈ 64% of redundant conclusions. [4091326 of approximately 6392697] (ETC: Sun Oct  1 14:49:43 2023 ; 1 h  2 min  9 s 373.51 ms remaining ; 2 h 52 min 39 s 370.50 ms total)
Sun Oct  1 13:51:01 2023: Removed ≈ 66% of redundant conclusions. [4219180 of approximately 6392697] (ETC: Sun Oct  1 14:49:43 2023 ; 58 min 42 s 315.61 ms remaining ; 2 h 52 min 39 s 751.70 ms total)
Sun Oct  1 13:54:28 2023: Removed ≈ 68% of redundant conclusions. [4347033 of approximately 6392697] (ETC: Sun Oct  1 14:49:43 2023 ; 55 min 15 s 206.46 ms remaining ; 2 h 52 min 40 s  15.32 ms total)
Sun Oct  1 13:57:49 2023: Removed ≈ 70% of redundant conclusions. [4474887 of approximately 6392697] (ETC: Sun Oct  1 14:49:34 2023 ; 51 min 45 s 157.53 ms remaining ; 2 h 52 min 30 s 520.25 ms total)
Sun Oct  1 14:01:08 2023: Removed ≈ 72% of redundant conclusions. [4602741 of approximately 6392697] (ETC: Sun Oct  1 14:49:23 2023 ; 48 min 15 s 141.20 ms remaining ; 2 h 52 min 19 s 785.14 ms total)
Sun Oct  1 14:04:26 2023: Removed ≈ 74% of redundant conclusions. [4730595 of approximately 6392697] (ETC: Sun Oct  1 14:49:12 2023 ; 44 min 45 s 359.39 ms remaining ; 2 h 52 min  8 s 300.51 ms total)
Sun Oct  1 14:07:48 2023: Removed ≈ 76% of redundant conclusions. [4858449 of approximately 6392697] (ETC: Sun Oct  1 14:49:06 2023 ; 41 min 17 s 375.32 ms remaining ; 2 h 52 min  2 s 392.31 ms total)
Sun Oct  1 14:11:08 2023: Removed ≈ 78% of redundant conclusions. [4986303 of approximately 6392697] (ETC: Sun Oct  1 14:48:58 2023 ; 37 min 49 s 155.28 ms remaining ; 2 h 51 min 54 s 337.33 ms total)
Sun Oct  1 14:14:28 2023: Removed ≈ 80% of redundant conclusions. [5114157 of approximately 6392697] (ETC: Sun Oct  1 14:48:49 2023 ; 34 min 21 s 124.64 ms remaining ; 2 h 51 min 45 s 618.36 ms total)
Sun Oct  1 14:17:48 2023: Removed ≈ 82% of redundant conclusions. [5242011 of approximately 6392697] (ETC: Sun Oct  1 14:48:42 2023 ; 30 min 53 s 786.12 ms remaining ; 2 h 51 min 38 s 806.96 ms total)
Sun Oct  1 14:21:09 2023: Removed ≈ 84% of redundant conclusions. [5369865 of approximately 6392697] (ETC: Sun Oct  1 14:48:36 2023 ; 27 min 26 s 830.82 ms remaining ; 2 h 51 min 32 s 687.79 ms total)
Sun Oct  1 14:24:31 2023: Removed ≈ 86% of redundant conclusions. [5497719 of approximately 6392697] (ETC: Sun Oct  1 14:48:32 2023 ; 24 min      365.86 ms remaining ; 2 h 51 min 28 s 322.71 ms total)
Sun Oct  1 14:27:53 2023: Removed ≈ 88% of redundant conclusions. [5625573 of approximately 6392697] (ETC: Sun Oct  1 14:48:27 2023 ; 20 min 34 s  97.12 ms remaining ; 2 h 51 min 24 s 137.82 ms total)
Sun Oct  1 14:31:17 2023: Removed ≈ 90% of redundant conclusions. [5753427 of approximately 6392697] (ETC: Sun Oct  1 14:48:25 2023 ; 17 min  8 s 223.32 ms remaining ; 2 h 51 min 22 s 228.41 ms total)
Sun Oct  1 14:34:35 2023: Removed ≈ 92% of redundant conclusions. [5881281 of approximately 6392697] (ETC: Sun Oct  1 14:48:17 2023 ; 13 min 41 s 909.24 ms remaining ; 2 h 51 min 13 s 860.69 ms total)
Sun Oct  1 14:37:57 2023: Removed ≈ 94% of redundant conclusions. [6009135 of approximately 6392697] (ETC: Sun Oct  1 14:48:13 2023 ; 10 min 16 s 201.63 ms remaining ; 2 h 51 min 10 s  22.30 ms total)
Sun Oct  1 14:41:21 2023: Removed ≈ 96% of redundant conclusions. [6136989 of approximately 6392697] (ETC: Sun Oct  1 14:48:12 2023 ; 6 min 50 s 737.93 ms remaining ; 2 h 51 min  8 s 443.37 ms total)
[Rank 8] Workload transfer approved. Starting to work on 43:[9552943, 9558308].
[Rank 1] Workload transfer approved. Starting to work on 47:[10422124, 10427489].
[Rank 13] Workload transfer approved. Starting to work on 0:[209248, 214612].
[Rank 42] Workload transfer approved. Starting to work on 2:[643838, 649202].
[Rank 18] Workload transfer approved. Starting to work on 5:[1295724, 1301088].
[Rank 41] Workload transfer approved. Starting to work on 36:[8031877, 8037241].
Sun Oct  1 14:44:50 2023: Removed ≈ 98% of redundant conclusions. [6264843 of approximately 6392697] (ETC: Sun Oct  1 14:48:16 2023 ; 3 min 25 s 446.99 ms remaining ; 2 h 51 min 12 s 344.65 ms total)
[Rank 38] Workload transfer approved. Starting to work on 46:[10204829, 10210193].
[Rank 45] Workload transfer approved. Starting to work on 2:[649203, 650990].
[Rank 26] Workload transfer approved. Starting to work on 3:[866499, 868286].
[Rank 12] Workload transfer approved. Starting to work on 4:[1083794, 1085581].
[Rank 27] Workload transfer approved. Starting to work on 5:[1301089, 1302876].
[Rank 37] Workload transfer approved. Starting to work on 6:[1518384, 1520171].
[Rank 0] Workload transfer approved. Starting to work on 7:[1735680, 1737467].
[Rank 24] Workload transfer approved. Starting to work on 14:[3256746, 3258533].
[Rank 44] Workload transfer approved. Starting to work on 23:[5212404, 5214191].
[Rank 43] Workload transfer approved. Starting to work on 25:[5646994, 5648781].
[Rank 21] Workload transfer approved. Starting to work on 28:[6298880, 6300667].
[Rank 29] Workload transfer approved. Starting to work on 39:[8689128, 8690915].
[Rank 4] Workload transfer approved. Starting to work on 46:[10210194, 10211981].
[Rank 9] Workload transfer approved. Starting to work on 47:[10427490, 10429277].
[Rank 19] Workload transfer approved. Starting to work on 2:[650991, 651884].
[Rank 45] Workload transfer approved. Starting to work on 6:[1520172, 1521065].
[Rank 12] Workload transfer approved. Starting to work on 7:[1737468, 1738361].
[Rank 5] Workload transfer approved. Starting to work on 10:[2389353, 2390246].
[Rank 26] Workload transfer approved. Starting to work on 14:[3258534, 3259427].
[Rank 7] Workload transfer approved. Starting to work on 15:[3475830, 3476723].
[Rank 10] Workload transfer approved. Starting to work on 17:[3910420, 3911313].
[Rank 36] Workload transfer approved. Starting to work on 20:[4562306, 4563199].
[Rank 22] Workload transfer approved. Starting to work on 23:[5214192, 5215085].
[Rank 16] Workload transfer approved. Starting to work on 25:[5648782, 5649675].
[Rank 3] Workload transfer approved. Starting to work on 28:[6300668, 6301561].
[Rank 11] Workload transfer approved. Starting to work on 30:[6735258, 6736151].
[Rank 23] Workload transfer approved. Starting to work on 31:[6952554, 6953447].
[Rank 27] Workload transfer approved. Starting to work on 32:[7169849, 7170742].
[Rank 8] Workload transfer approved. Starting to work on 33:[7387144, 7388037].
[Rank 15] Workload transfer approved. Starting to work on 35:[7821735, 7822628].
[Rank 25] Workload transfer approved. Starting to work on 46:[10211982, 10212875].
[Rank 40] Workload transfer approved. Starting to work on 47:[10429278, 10430171].
10414029.15 ms (2 h 53 min 34 s 29.15 ms) taken to detect 6364145 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 4066027 representative and 6364145 redundant condensed detachment proof strings.
[Copy] Removal count: { 137, 6364145 }
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0604.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0608.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0612.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 4 on "nrm081.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 5 on "nrm082.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 6 on "nrm084.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 7 on "nrm085.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 8 on "nrm088.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 9 on "nrm089.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 10 on "nrm091.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 11 on "nrm092.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 12 on "nrm095.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 13 on "nrm096.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 14 on "nrm097.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 15 on "nrm098.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 16 on "nrm099.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 17 on "nrm100.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 18 on "nrm101.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 19 on "nrm102.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 20 on "nrm103.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 21 on "nrm104.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 22 on "nrm105.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 23 on "nrm107.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 24 on "nrm109.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 25 on "nrm110.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 26 on "nrm111.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 27 on "nrm113.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 28 on "nrm115.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 29 on "nrm116.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 30 on "nrm117.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 31 on "nrm118.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 32 on "nrm120.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 33 on "nrm121.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 34 on "nrm123.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 35 on "nrm124.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 36 on "nrm125.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 37 on "nrm126.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 38 on "nrm128.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 39 on "nrm130.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 40 on "nrm132.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 41 on "nrm133.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 42 on "nrm135.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 43 on "nrm138.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 44 on "nrm139.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 45 on "nrm142.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 46 on "nrm143.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 47 on "nrm144.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
1838.09 ms (1 s 838.09 ms) taken to filter and order new representative proofs.
Sun Oct  1 14:50:38 2023: Starting to write 4066027 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt.
3005.54 ms (3 s 5.54 ms) taken to print and save 1235762264 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt.
Sun Oct  1 14:50:41 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0597.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 206445, tid:23262505375616]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 223225, tid:22924446844800]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 260994, tid:22660369487744]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 219016, tid:23385297700736]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 149358, tid:23335155562368]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 210847, tid:23437190748032]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 145846, tid:22898531383168]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 41545, tid:23371999139712]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 174746, tid:22384182241152]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 139173, tid:23399086483328]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 72713, tid:22934036006784]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 228572, tid:22686815242112]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 227619, tid:22953816307584]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 274763, tid:23206316066688]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 275006, tid:23253744117632]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 63926, tid:22827390928768]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 256496, tid:22371252995968]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 200307, tid:23243528345472]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 1438, tid:23001885915008]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 276962, tid:22756119312256]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 235377, tid:23380255713152]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 223862, tid:23274358183808]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 163122, tid:22902969030528]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 157248, tid:22497801869184]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 224584, tid:23427456882560]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 242375, tid:22453605508992]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 224635, tid:23107796805504]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 257248, tid:23410566924160]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 270316, tid:22476426356608]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 162953, tid:22883746346880]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 118291, tid:23254672766848]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 6028, tid:22658019436416]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 16572, tid:22824990521216]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 255142, tid:22772861208448]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 102522, tid:22668398028672]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 95570, tid:22513916409728]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 249424, tid:22711862007680]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 230129, tid:22850536327040]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 206927, tid:22740393527168]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 195651, tid:23293449389952]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 267968, tid:22708276672384]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 250254, tid:22942087788416]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 158176, tid:22629302286208]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 194382, tid:23420537935744]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 22859, tid:22540687116160]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 92970, tid:23432791201664]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 240930, tid:22703855765376]
Sun Oct  1 14:51:10 2023: Process terminated. [pid: 103566, tid:23389857654656]