dProofs151_72node_3456cpu.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 72 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.9797222… h
  CPU utilization: 10297.92 core-h )
Sun Oct 22 03:22:20 2023: Process started. [pid: 111568, tid:22666438178688]
Sun Oct 22 03:22:20 2023: Process started. [pid: 87567, tid:23175184725888]
Sun Oct 22 03:22:20 2023: Process started. [pid: 220905, tid:22536795682688]
Sun Oct 22 03:22:20 2023: Process started. [pid: 90116, tid:23377883326336]
Sun Oct 22 03:22:20 2023: Process started. [pid: 2276, tid:22714815293312]
Sun Oct 22 03:22:20 2023: Process started. [pid: 85551, tid:23156554188672]
Sun Oct 22 03:22:20 2023: Process started. [pid: 246690, tid:23112434595712]
Sun Oct 22 03:22:20 2023: Process started. [pid: 9684, tid:23000170092416]
Sun Oct 22 03:22:20 2023: Process started. [pid: 117884, tid:22460849862528]
Sun Oct 22 03:22:20 2023: Process started. [pid: 142606, tid:22358009505664]
Sun Oct 22 03:22:20 2023: Process started. [pid: 54658, tid:23437029349248]
Sun Oct 22 03:22:20 2023: Process started. [pid: 277284, tid:22609131108224]
Sun Oct 22 03:22:20 2023: Process started. [pid: 126433, tid:23159523977088]
Sun Oct 22 03:22:20 2023: Process started. [pid: 163719, tid:23058043422592]
Sun Oct 22 03:22:20 2023: Process started. [pid: 13644, tid:23065108875136]
Sun Oct 22 03:22:20 2023: Process started. [pid: 104754, tid:23090265003904]
Sun Oct 22 03:22:20 2023: Process started. [pid: 264157, tid:22965684361088]
Sun Oct 22 03:22:20 2023: Process started. [pid: 201776, tid:23242533934976]
Sun Oct 22 03:22:20 2023: Process started. [pid: 165147, tid:22883564111744]
Sun Oct 22 03:22:20 2023: Process started. [pid: 12125, tid:22625873909632]
Sun Oct 22 03:22:20 2023: Process started. [pid: 146459, tid:22526437062528]
Sun Oct 22 03:22:20 2023: Process started. [pid: 163308, tid:23366341044096]
Sun Oct 22 03:22:20 2023: Process started. [pid: 132935, tid:22397695760256]
Sun Oct 22 03:22:20 2023: Process started. [pid: 45764, tid:23080435033984]
Sun Oct 22 03:22:20 2023: Process started. [pid: 178708, tid:22845083744128]
Sun Oct 22 03:22:20 2023: Process started. [pid: 156990, tid:22405251852160]
Sun Oct 22 03:22:20 2023: Process started. [pid: 218926, tid:22548426057600]
Sun Oct 22 03:22:20 2023: Process started. [pid: 240347, tid:23363014973312]
Sun Oct 22 03:22:20 2023: Process started. [pid: 113390, tid:23073680365440]
Sun Oct 22 03:22:20 2023: Process started. [pid: 19744, tid:22715342620544]
Sun Oct 22 03:22:20 2023: Process started. [pid: 198259, tid:22457326557056]
Sun Oct 22 03:22:20 2023: Process started. [pid: 216295, tid:22697053906816]
Sun Oct 22 03:22:20 2023: Process started. [pid: 137907, tid:23035522201472]
Sun Oct 22 03:22:20 2023: Process started. [pid: 148285, tid:23156946536320]
Sun Oct 22 03:22:20 2023: Process started. [pid: 193312, tid:23234177247104]
Sun Oct 22 03:22:20 2023: Process started. [pid: 112458, tid:23257082259328]
Sun Oct 22 03:22:20 2023: Process started. [pid: 174586, tid:22769505163136]
Sun Oct 22 03:22:20 2023: Process started. [pid: 237479, tid:22856952842112]
Sun Oct 22 03:22:20 2023: Process started. [pid: 128220, tid:22549788600192]
Sun Oct 22 03:22:20 2023: Process started. [pid: 40725, tid:22559237670784]
Sun Oct 22 03:22:20 2023: Process started. [pid: 102513, tid:22576520443776]
Sun Oct 22 03:22:20 2023: Process started. [pid: 48934, tid:22682949552000]
Sun Oct 22 03:22:20 2023: Process started. [pid: 152725, tid:23255849265024]
Sun Oct 22 03:22:20 2023: Process started. [pid: 237794, tid:22840307210112]
Sun Oct 22 03:22:20 2023: Process started. [pid: 143009, tid:22852241987456]
Sun Oct 22 03:22:20 2023: Process started. [pid: 190168, tid:22745488832384]
Sun Oct 22 03:22:20 2023: Process started. [pid: 247877, tid:23451583178624]
Sun Oct 22 03:22:20 2023: Process started. [pid: 45120, tid:22421764056960]
Sun Oct 22 03:22:20 2023: Process started. [pid: 26470, tid:22577631016832]
Sun Oct 22 03:22:20 2023: Process started. [pid: 73186, tid:22808259938176]
Sun Oct 22 03:22:20 2023: Process started. [pid: 231896, tid:23226914850688]
Sun Oct 22 03:22:20 2023: Process started. [pid: 261378, tid:22543215269760]
Sun Oct 22 03:22:20 2023: Process started. [pid: 24689, tid:22382670600064]
Sun Oct 22 03:22:20 2023: Process started. [pid: 118764, tid:22888055990144]
Sun Oct 22 03:22:20 2023: Process started. [pid: 87616, tid:22820666042240]
Sun Oct 22 03:22:20 2023: Process started. [pid: 226981, tid:22886894143360]
Sun Oct 22 03:22:20 2023: Process started. [pid: 235580, tid:23213391296384]
Sun Oct 22 03:22:20 2023: Process started. [pid: 202839, tid:22904331556736]
Sun Oct 22 03:22:20 2023: Process started. [pid: 65519, tid:23127824762752]
Sun Oct 22 03:22:20 2023: Process started. [pid: 266556, tid:23449134491520]
Sun Oct 22 03:22:20 2023: Process started. [pid: 218661, tid:22547623630720]
Sun Oct 22 03:22:20 2023: Process started. [pid: 147567, tid:22386044106624]
Sun Oct 22 03:22:20 2023: Process started. [pid: 105868, tid:23009840854912]
Sun Oct 22 03:22:20 2023: Process started. [pid: 230878, tid:23032448972672]
Sun Oct 22 03:22:20 2023: Process started. [pid: 101889, tid:22563794761600]
Sun Oct 22 03:22:20 2023: Process started. [pid: 62877, tid:22881977755520]
Sun Oct 22 03:22:20 2023: Process started. [pid: 114979, tid:22777186457472]
Sun Oct 22 03:22:20 2023: Process started. [pid: 57050, tid:22869321447296]
Sun Oct 22 03:22:20 2023: Process started. [pid: 232719, tid:22438374446976]
Sun Oct 22 03:22:20 2023: Process started. [pid: 134440, tid:22818485237632]
Sun Oct 22 03:22:20 2023: Process started. [pid: 53495, tid:23002419263360]
Sun Oct 22 03:22:20 2023: Process started. [pid: 69210, tid:23257575315328]
Tasks:
1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true)
2. mpi_filterDProofRepresentativeFile(151, true)

[Rank 0 ; pid: 69210 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9]
(1) C0CCN1CCN2.3C4.1CC2.4C2.1    -    CpCCNqCCNrsCtqCCrtCrq    -    0\imply((\not1\imply((\not2\imply3)\imply(4\imply1)))\imply((2\imply4)\imply(2\imply1)))
[Rank 1 ; pid: 13644 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 2 ; pid: 26470 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 3 ; pid: 142606 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 4 ; pid: 90116 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 5 ; pid: 45120 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 6 ; pid: 264157 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 7 ; pid: 54658 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 8 ; pid: 202839 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 9 ; pid: 2276 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 10 ; pid: 218661 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 11 ; pid: 24689 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 12 ; pid: 111568 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 13 ; pid: 198259 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 14 ; pid: 128220 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 15 ; pid: 174586 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 16 ; pid: 240347 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 17 ; pid: 101889 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 18 ; pid: 143009 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 19 ; pid: 126433 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 20 ; pid: 261378 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 21 ; pid: 190168 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 22 ; pid: 114979 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 23 ; pid: 201776 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 24 ; pid: 57050 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 25 ; pid: 146459 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 26 ; pid: 237479 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 27 ; pid: 230878 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 28 ; pid: 87567 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 29 ; pid: 19744 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 30 ; pid: 266556 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 31 ; pid: 104754 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 32 ; pid: 147567 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 33 ; pid: 148285 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 34 ; pid: 232719 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 35 ; pid: 156990 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 36 ; pid: 220905 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 37 ; pid: 246690 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 38 ; pid: 73186 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 39 ; pid: 12125 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 40 ; pid: 9684 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 41 ; pid: 231896 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 42 ; pid: 237794 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 43 ; pid: 235580 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 44 ; pid: 65519 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 45 ; pid: 218926 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 46 ; pid: 193312 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 47 ; pid: 247877 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 48 ; pid: 178708 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 49 ; pid: 113390 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 50 ; pid: 132935 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 51 ; pid: 48934 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 52 ; pid: 62877 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 53 ; pid: 102513 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 54 ; pid: 105868 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 55 ; pid: 40725 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 56 ; pid: 226981 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 57 ; pid: 134440 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 58 ; pid: 137907 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 59 ; pid: 277284 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 60 ; pid: 216295 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 61 ; pid: 45764 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 62 ; pid: 53495 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 63 ; pid: 152725 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 64 ; pid: 85551 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 65 ; pid: 87616 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 66 ; pid: 117884 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 67 ; pid: 163719 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 68 ; pid: 118764 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 69 ; pid: 163308 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 70 ; pid: 165147 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 71 ; pid: 112458 ; 72 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 0 ; pid: 69210 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 1 ; pid: 13644 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 2 ; pid: 26470 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 3 ; pid: 142606 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 4 ; pid: 90116 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 5 ; pid: 45120 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 6 ; pid: 264157 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 7 ; pid: 54658 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 8 ; pid: 202839 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 9 ; pid: 2276 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 10 ; pid: 218661 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 11 ; pid: 24689 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 12 ; pid: 111568 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 13 ; pid: 198259 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 14 ; pid: 128220 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 15 ; pid: 174586 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 16 ; pid: 240347 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 17 ; pid: 101889 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 18 ; pid: 143009 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 19 ; pid: 126433 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 20 ; pid: 261378 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 21 ; pid: 190168 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 22 ; pid: 114979 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 23 ; pid: 201776 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 24 ; pid: 57050 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 25 ; pid: 146459 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 26 ; pid: 237479 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 27 ; pid: 230878 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 28 ; pid: 87567 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 29 ; pid: 19744 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 30 ; pid: 266556 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 31 ; pid: 104754 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 32 ; pid: 147567 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 33 ; pid: 148285 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 34 ; pid: 232719 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 35 ; pid: 156990 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 36 ; pid: 220905 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 37 ; pid: 246690 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 38 ; pid: 73186 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 39 ; pid: 12125 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 40 ; pid: 9684 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 41 ; pid: 231896 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 42 ; pid: 237794 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 43 ; pid: 235580 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 44 ; pid: 65519 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 45 ; pid: 218926 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 46 ; pid: 193312 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 47 ; pid: 247877 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 48 ; pid: 178708 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 49 ; pid: 113390 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 50 ; pid: 132935 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 51 ; pid: 48934 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 52 ; pid: 62877 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 53 ; pid: 102513 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 54 ; pid: 105868 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 55 ; pid: 40725 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 56 ; pid: 226981 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 57 ; pid: 134440 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 58 ; pid: 137907 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 59 ; pid: 277284 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 60 ; pid: 216295 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 61 ; pid: 45764 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 62 ; pid: 53495 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 63 ; pid: 152725 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 64 ; pid: 85551 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 65 ; pid: 87616 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 66 ; pid: 117884 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 67 ; pid: 163719 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 68 ; pid: 118764 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 69 ; pid: 163308 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 70 ; pid: 165147 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
[Rank 71 ; pid: 112458 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(151, true).
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0033.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0095.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0105.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0106.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0154.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0167.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0171.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0178.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0186.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0195.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0198.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0201.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0202.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0204.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0205.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0206.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0207.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0209.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0213.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0224.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0271.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0280.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0340.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0342.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 24 on "ncm0344.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 25 on "ncm0345.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 26 on "ncm0346.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 27 on "ncm0351.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 28 on "ncm0354.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 29 on "ncm0363.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 30 on "ncm0416.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 31 on "ncm0421.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 32 on "ncm0464.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 33 on "ncm0466.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 34 on "ncm0472.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 35 on "ncm0490.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 36 on "ncm0495.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 37 on "ncm0498.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 38 on "ncm0503.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 39 on "ncm0546.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 40 on "ncm0549.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 41 on "ncm0556.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 42 on "ncm0573.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 43 on "ncm0575.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 44 on "ncm0586.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 45 on "ncm0601.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 46 on "ncm0741.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 47 on "ncm0756.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 48 on "ncm0763.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 49 on "ncm0787.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 50 on "ncm0791.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 51 on "ncm0805.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 52 on "ncm0815.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 53 on "ncm0874.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 54 on "ncm0884.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 55 on "ncm0905.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 56 on "ncm0919.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 57 on "ncm0923.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 58 on "ncm0925.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 59 on "ncm0947.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 60 on "ncm0952.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 61 on "ncm0955.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 62 on "ncm0964.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 63 on "ncm0978.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 64 on "ncm0988.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 65 on "ncm0991.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 66 on "ncm0996.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 67 on "ncm0998.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 68 on "ncm0999.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 69 on "ncm1006.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 70 on "nrm089.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 03:22:21 2023: MPI-based D-proof representative filter started. [rank 71 on "nrm094.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
0.08 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23257400157952]
0.02 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23257398056704]
0.03 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23257395955456]
0.01 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23257393854208]
0.07 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23257391752960]
2.07 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23257389651712]
0.03 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23257387550464]
0.04 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23257385449216]
0.03 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23256845252352]
0.05 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23256843151104]
0.03 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23256841049856]
0.14 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23256838948608]
0.03 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23256836847360]
0.03 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23256834746112]
0.07 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23256832644864]
0.50 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23256830543616]
1.99 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23256826341120]
1.26 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23256824239872]
0.08 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23256822138624]
0.22 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23256817936128]
0.00 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23256815834880]
3.98 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23256813733632]
2.17 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23256807429888]
0.66 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23256805328640]
4.19 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23256803227392]
1.55 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23256799024896]
289.40 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23257400157952]
381.73 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23257398056704]
610.82 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23257395955456]
656.51 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23257393854208]
705.83 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23257391752960]
977.40 ms taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23257389651712]
1070.37 ms (1 s 70.37 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23257387550464]
1999.59 ms (1 s 999.60 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23257385449216]
3013.81 ms (3 s 13.81 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23256845252352]
4150.72 ms (4 s 150.72 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23256843151104]
8897.97 ms (8 s 897.97 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23256841049856]
1017.01 ms (1 s 17.01 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23256838948608]
1379.06 ms (1 s 379.06 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23256836847360]
2726.18 ms (2 s 726.18 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23256834746112]
1097.26 ms (1 s 97.26 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23256832644864]
4501.32 ms (4 s 501.31 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23256830543616]
29.18 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23256828442368]
4344.13 ms (4 s 344.13 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23256826341120]
3472.64 ms (3 s 472.64 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23256824239872]
3526.08 ms (3 s 526.08 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23256822138624]
10.19 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23256820037376]
4992.79 ms (4 s 992.79 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23256817936128]
4465.36 ms (4 s 465.36 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23256815834880]
5261.37 ms (5 s 261.37 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23256813733632]
69.99 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23256811632384]
22.19 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23256809531136]
5493.53 ms (5 s 493.53 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23256807429888]
7075.27 ms (7 s 75.27 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23256805328640]
7803.02 ms (7 s 803.02 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23256803227392]
264.54 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23256801126144]
9035.46 ms (9 s 35.46 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23256799024896]
5.56 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23256796923648]
6.70 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23256794822400]
70.02 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23256792721152]
29.97 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23256790619904]
16.48 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23256788518656]
5.87 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23256786417408]
3.00 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23256784316160]
111.16 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23256782214912]
131.91 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23254831986432]
187.36 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23254966204160]
218.60 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23254964102912]
25.55 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23254962001664]
250.41 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23254959900416]
31.70 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23254957799168]
139.98 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23254955697920]
182.34 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23254953596672]
162.98 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23254951495424]
9133.73 ms (9 s 133.73 ms) total read duration.
Loaded 75 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 1
9 : 2
11 : 2
13 : 2
15 : 2
17 : 5
19 : 5
21 : 3
23 : 6
25 : 10
27 : 7
29 : 12
31 : 14
33 : 17
35 : 21
37 : 30
39 : 28
41 : 44
43 : 56
45 : 66
47 : 80
49 : 108
51 : 123
53 : 168
55 : 197
57 : 241
59 : 303
61 : 390
63 : 444
65 : 570
67 : 707
69 : 863
71 : 1052
73 : 1340
75 : 1586
77 : 1990
79 : 2467
81 : 3018
83 : 3679
85 : 4661
87 : 5632
89 : 6994
91 : 8637
93 : 10677
95 : 13008
97 : 16295
99 : 19833
101 : 24567
103 : 30296
105 : 37377
107 : 45724
109 : 56922
111 : 69661
113 : 85894
115 : 105871
117 : 130737
119 : 160270
121 : 198446
123 : 243740
125 : 300530
127 : 370216
129 : 456911
131 : 560926
133 : 693346
135 : 853090
137 : 1051251
139 : 1294413
141 : 1597383
143 : 1963944
145 : 2423655
147 : 2983754
149 : 3676539
19520862 representatives in total.
31225.56 ms (31 s 225.56 ms) taken to read 17299503 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151-unfiltered151+.txt. [tid:23254951495424]
31229.25 ms (31 s 229.25 ms) additional read duration.
Loaded 1 more representative collection of size:
151 : 17299503
36820365 representatives in total.
Sun Oct 22 03:23:04 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 12740796, based on entry 149:10311828 and last known pair (147:8345930, 149:10311828) with 10311828/8345930 ≈ 1.23555 and 10311828 * (10311828/8345930)^1 ≈ 12740796.62.
Sun Oct 22 03:23:06 2023: Inserted ≈ 5% of D-proof conclusions. [ 1841018 of 36820365] (ETC: Sun Oct 22 03:23:44 2023 ; 37 s 764.69 ms remaining ; 39 s 752.31 ms total)
Sun Oct 22 03:23:08 2023: Inserted ≈10% of D-proof conclusions. [ 3682036 of 36820365] (ETC: Sun Oct 22 03:23:43 2023 ; 34 s 945.89 ms remaining ; 38 s 828.76 ms total)
Sun Oct 22 03:23:09 2023: Inserted ≈15% of D-proof conclusions. [ 5523054 of 36820365] (ETC: Sun Oct 22 03:23:41 2023 ; 31 s 668.16 ms remaining ; 37 s 256.66 ms total)
Sun Oct 22 03:23:11 2023: Inserted ≈20% of D-proof conclusions. [ 7364073 of 36820365] (ETC: Sun Oct 22 03:23:40 2023 ; 28 s 907.15 ms remaining ; 36 s 133.94 ms total)
Sun Oct 22 03:23:13 2023: Inserted ≈25% of D-proof conclusions. [ 9205091 of 36820365] (ETC: Sun Oct 22 03:23:41 2023 ; 27 s 693.03 ms remaining ; 36 s 924.04 ms total)
Sun Oct 22 03:23:15 2023: Inserted ≈30% of D-proof conclusions. [11046109 of 36820365] (ETC: Sun Oct 22 03:23:42 2023 ; 27 s  16.11 ms remaining ; 38 s 594.44 ms total)
Sun Oct 22 03:23:18 2023: Inserted ≈35% of D-proof conclusions. [12887127 of 36820365] (ETC: Sun Oct 22 03:23:44 2023 ; 26 s 284.28 ms remaining ; 40 s 437.35 ms total)
Sun Oct 22 03:23:21 2023: Inserted ≈40% of D-proof conclusions. [14728146 of 36820365] (ETC: Sun Oct 22 03:23:46 2023 ; 25 s 169.08 ms remaining ; 41 s 948.46 ms total)
Sun Oct 22 03:23:23 2023: Inserted ≈45% of D-proof conclusions. [16569164 of 36820365] (ETC: Sun Oct 22 03:23:47 2023 ; 23 s 915.15 ms remaining ; 43 s 482.10 ms total)
Sun Oct 22 03:23:26 2023: Inserted ≈50% of D-proof conclusions. [18410182 of 36820365] (ETC: Sun Oct 22 03:23:49 2023 ; 22 s 594.15 ms remaining ; 45 s 188.30 ms total)
Sun Oct 22 03:23:29 2023: Inserted ≈55% of D-proof conclusions. [20251200 of 36820365] (ETC: Sun Oct 22 03:23:49 2023 ; 20 s 338.01 ms remaining ; 45 s 195.57 ms total)
Sun Oct 22 03:23:30 2023: Inserted ≈60% of D-proof conclusions. [22092219 of 36820365] (ETC: Sun Oct 22 03:23:47 2023 ; 17 s 309.23 ms remaining ; 43 s 273.07 ms total)
Sun Oct 22 03:23:31 2023: Inserted ≈65% of D-proof conclusions. [23933237 of 36820365] (ETC: Sun Oct 22 03:23:46 2023 ; 14 s 677.88 ms remaining ; 41 s 936.81 ms total)
Sun Oct 22 03:23:32 2023: Inserted ≈70% of D-proof conclusions. [25774255 of 36820365] (ETC: Sun Oct 22 03:23:45 2023 ; 12 s 213.71 ms remaining ; 40 s 712.37 ms total)
Sun Oct 22 03:23:34 2023: Inserted ≈75% of D-proof conclusions. [27615273 of 36820365] (ETC: Sun Oct 22 03:23:44 2023 ; 9 s 965.89 ms remaining ; 39 s 863.57 ms total)
Sun Oct 22 03:23:35 2023: Inserted ≈80% of D-proof conclusions. [29456292 of 36820365] (ETC: Sun Oct 22 03:23:43 2023 ; 7 s 816.84 ms remaining ; 39 s  84.21 ms total)
Sun Oct 22 03:23:37 2023: Inserted ≈85% of D-proof conclusions. [31297310 of 36820365] (ETC: Sun Oct 22 03:23:42 2023 ; 5 s 782.67 ms remaining ; 38 s 551.13 ms total)
Sun Oct 22 03:23:38 2023: Inserted ≈90% of D-proof conclusions. [33138328 of 36820365] (ETC: Sun Oct 22 03:23:42 2023 ; 3 s 792.07 ms remaining ; 37 s 920.73 ms total)
Sun Oct 22 03:23:40 2023: Inserted ≈95% of D-proof conclusions. [34979346 of 36820365] (ETC: Sun Oct 22 03:23:41 2023 ; 1 s 883.04 ms remaining ; 37 s 660.72 ms total)
Sun Oct 22 03:23:41 2023: Inserted 100% of D-proof conclusions. [36820365 of 36820365] (ETC: Sun Oct 22 03:23:41 2023 ; 0.00 ms remaining ; 37 s 367.07 ms total)
37367.23 ms (37 s 367.23 ms) total insertion duration.
Reservable workloads: { 0:[160180, 240269], 1:[400451, 480540], 2:[640722, 720811], 3:[880993, 961082], 4:[1121264, 1201353], 5:[1361535, 1441624], 6:[1601806, 1681895], 7:[1842077, 1922166], 8:[2082347, 2162436], 9:[2322618, 2402707], 10:[2562889, 2642978], 11:[2803160, 2883249], 12:[3043431, 3123520], 13:[3283702, 3363791], 14:[3523973, 3604062], 15:[3764244, 3844333], 16:[4004514, 4084603], 17:[4244785, 4324874], 18:[4485056, 4565145], 19:[4725327, 4805416], 20:[4965598, 5045687], 21:[5205869, 5285958], 22:[5446140, 5526229], 23:[5686411, 5766500], 24:[5926681, 6006770], 25:[6166952, 6247041], 26:[6407223, 6487312], 27:[6647494, 6727583], 28:[6887765, 6967854], 29:[7128036, 7208125], 30:[7368307, 7448396], 31:[7608578, 7688667], 32:[7848848, 7928937], 33:[8089119, 8169208], 34:[8329390, 8409479], 35:[8569661, 8649750], 36:[8809932, 8890021], 37:[9050203, 9130292], 38:[9290474, 9370563], 39:[9530745, 9610834], 40:[9771015, 9851104], 41:[10011286, 10091375], 42:[10251557, 10331646], 43:[10491828, 10571917], 44:[10732099, 10812188], 45:[10972370, 11052459], 46:[11212641, 11292730], 47:[11452912, 11533001], 48:[11693182, 11773271], 49:[11933453, 12013542], 50:[12173724, 12253813], 51:[12413995, 12494084], 52:[12654266, 12734355], 53:[12894537, 12974626], 54:[13134808, 13214897], 55:[13375079, 13455168], 56:[13615349, 13695438], 57:[13855620, 13935709], 58:[14095891, 14175980], 59:[14336162, 14416251], 60:[14576433, 14656522], 61:[14816704, 14896793], 62:[15056975, 15137064], 63:[15297246, 15377335], 64:[15537516, 15617605], 65:[15777787, 15857876], 66:[16018058, 16098147], 67:[16258329, 16338418], 68:[16498600, 16578689], 69:[16738871, 16818960], 70:[16979142, 17059231], 71:[17219413, 17299502] }
Sun Oct 22 03:27:26 2023: Removed ≈  2% of redundant conclusions. [  254815 of approximately 12740796] (ETC: Sun Oct 22 06:29:06 2023 ; 3 h  1 min 39 s 403.91 ms remaining ; 3 h  5 min 21 s 839.90 ms total)
Sun Oct 22 03:30:54 2023: Removed ≈  4% of redundant conclusions. [  509631 of approximately 12740796] (ETC: Sun Oct 22 06:23:05 2023 ; 2 h 52 min 10 s 385.69 ms remaining ; 2 h 59 min 20 s 817.69 ms total)
Sun Oct 22 03:34:23 2023: Removed ≈  6% of redundant conclusions. [  764447 of approximately 12740796] (ETC: Sun Oct 22 06:21:18 2023 ; 2 h 46 min 54 s 995.75 ms remaining ; 2 h 57 min 34 s 250.13 ms total)
Sun Oct 22 03:37:51 2023: Removed ≈  8% of redundant conclusions. [ 1019263 of approximately 12740796] (ETC: Sun Oct 22 06:20:19 2023 ; 2 h 42 min 27 s 372.94 ms remaining ; 2 h 56 min 34 s 969.97 ms total)
Sun Oct 22 03:41:19 2023: Removed ≈ 10% of redundant conclusions. [ 1274079 of approximately 12740796] (ETC: Sun Oct 22 06:19:38 2023 ; 2 h 38 min 18 s 873.10 ms remaining ; 2 h 55 min 54 s 302.89 ms total)
Sun Oct 22 03:44:48 2023: Removed ≈ 12% of redundant conclusions. [ 1528895 of approximately 12740796] (ETC: Sun Oct 22 06:19:18 2023 ; 2 h 34 min 30 s 569.26 ms remaining ; 2 h 55 min 34 s 737.31 ms total)
Sun Oct 22 03:48:17 2023: Removed ≈ 14% of redundant conclusions. [ 1783711 of approximately 12740796] (ETC: Sun Oct 22 06:19:06 2023 ; 2 h 30 min 49 s 460.05 ms remaining ; 2 h 55 min 22 s 627.54 ms total)
Sun Oct 22 03:51:45 2023: Removed ≈ 16% of redundant conclusions. [ 2038527 of approximately 12740796] (ETC: Sun Oct 22 06:18:51 2023 ; 2 h 27 min  5 s 730.30 ms remaining ; 2 h 55 min  6 s 821.43 ms total)
Sun Oct 22 03:55:13 2023: Removed ≈ 18% of redundant conclusions. [ 2293343 of approximately 12740796] (ETC: Sun Oct 22 06:18:41 2023 ; 2 h 23 min 27 s 685.49 ms remaining ; 2 h 54 min 57 s 177.14 ms total)
Sun Oct 22 03:58:41 2023: Removed ≈ 20% of redundant conclusions. [ 2548159 of approximately 12740796] (ETC: Sun Oct 22 06:18:32 2023 ; 2 h 19 min 50 s 868.78 ms remaining ; 2 h 54 min 48 s 585.77 ms total)
Sun Oct 22 04:02:09 2023: Removed ≈ 22% of redundant conclusions. [ 2802975 of approximately 12740796] (ETC: Sun Oct 22 06:18:21 2023 ; 2 h 16 min 12 s 337.29 ms remaining ; 2 h 54 min 37 s 355.37 ms total)
Sun Oct 22 04:05:35 2023: Removed ≈ 24% of redundant conclusions. [ 3057791 of approximately 12740796] (ETC: Sun Oct 22 06:18:07 2023 ; 2 h 12 min 32 s  84.40 ms remaining ; 2 h 54 min 23 s 268.90 ms total)
Sun Oct 22 04:09:01 2023: Removed ≈ 26% of redundant conclusions. [ 3312606 of approximately 12740796] (ETC: Sun Oct 22 06:17:55 2023 ; 2 h  8 min 54 s 281.03 ms remaining ; 2 h 54 min 11 s 730.06 ms total)
Sun Oct 22 04:12:28 2023: Removed ≈ 28% of redundant conclusions. [ 3567422 of approximately 12740796] (ETC: Sun Oct 22 06:17:47 2023 ; 2 h  5 min 19 s 334.29 ms remaining ; 2 h 54 min  3 s 518.85 ms total)
Sun Oct 22 04:15:54 2023: Removed ≈ 30% of redundant conclusions. [ 3822238 of approximately 12740796] (ETC: Sun Oct 22 06:17:37 2023 ; 2 h  1 min 42 s 984.85 ms remaining ; 2 h 53 min 52 s 834.56 ms total)
Sun Oct 22 04:19:20 2023: Removed ≈ 32% of redundant conclusions. [ 4077054 of approximately 12740796] (ETC: Sun Oct 22 06:17:29 2023 ; 1 h 58 min  9 s 150.52 ms remaining ; 2 h 53 min 45 s 220.48 ms total)
Sun Oct 22 04:22:46 2023: Removed ≈ 34% of redundant conclusions. [ 4331870 of approximately 12740796] (ETC: Sun Oct 22 06:17:21 2023 ; 1 h 54 min 35 s 597.85 ms remaining ; 2 h 53 min 37 s 571.71 ms total)
Sun Oct 22 04:26:11 2023: Removed ≈ 36% of redundant conclusions. [ 4586686 of approximately 12740796] (ETC: Sun Oct 22 06:17:12 2023 ; 1 h 51 min  1 s 361.50 ms remaining ; 2 h 53 min 28 s 376.63 ms total)
Sun Oct 22 04:29:36 2023: Removed ≈ 38% of redundant conclusions. [ 4841502 of approximately 12740796] (ETC: Sun Oct 22 06:17:03 2023 ; 1 h 47 min 27 s 720.91 ms remaining ; 2 h 53 min 19 s 549.23 ms total)
Sun Oct 22 04:33:01 2023: Removed ≈ 40% of redundant conclusions. [ 5096318 of approximately 12740796] (ETC: Sun Oct 22 06:16:56 2023 ; 1 h 43 min 55 s 467.75 ms remaining ; 2 h 53 min 12 s 445.70 ms total)
Sun Oct 22 04:36:25 2023: Removed ≈ 42% of redundant conclusions. [ 5351134 of approximately 12740796] (ETC: Sun Oct 22 06:16:48 2023 ; 1 h 40 min 23 s   2.79 ms remaining ; 2 h 53 min  4 s 487.12 ms total)
Sun Oct 22 04:39:50 2023: Removed ≈ 44% of redundant conclusions. [ 5605950 of approximately 12740796] (ETC: Sun Oct 22 06:16:41 2023 ; 1 h 36 min 51 s 154.55 ms remaining ; 2 h 52 min 57 s  61.34 ms total)
Sun Oct 22 04:43:15 2023: Removed ≈ 46% of redundant conclusions. [ 5860766 of approximately 12740796] (ETC: Sun Oct 22 06:16:36 2023 ; 1 h 33 min 20 s 911.35 ms remaining ; 2 h 52 min 52 s  57.81 ms total)
Sun Oct 22 04:46:39 2023: Removed ≈ 48% of redundant conclusions. [ 6115582 of approximately 12740796] (ETC: Sun Oct 22 06:16:28 2023 ; 1 h 29 min 49 s 621.54 ms remaining ; 2 h 52 min 44 s 656.68 ms total)
Sun Oct 22 04:50:02 2023: Removed ≈ 50% of redundant conclusions. [ 6370398 of approximately 12740796] (ETC: Sun Oct 22 06:16:21 2023 ; 1 h 26 min 18 s 649.50 ms remaining ; 2 h 52 min 37 s 299.01 ms total)
Sun Oct 22 04:53:26 2023: Removed ≈ 52% of redundant conclusions. [ 6625213 of approximately 12740796] (ETC: Sun Oct 22 06:16:15 2023 ; 1 h 22 min 48 s 617.64 ms remaining ; 2 h 52 min 31 s 285.20 ms total)
Sun Oct 22 04:56:51 2023: Removed ≈ 54% of redundant conclusions. [ 6880029 of approximately 12740796] (ETC: Sun Oct 22 06:16:11 2023 ; 1 h 19 min 19 s 599.09 ms remaining ; 2 h 52 min 26 s 953.05 ms total)
Sun Oct 22 05:00:15 2023: Removed ≈ 56% of redundant conclusions. [ 7134845 of approximately 12740796] (ETC: Sun Oct 22 06:16:05 2023 ; 1 h 15 min 50 s 297.35 ms remaining ; 2 h 52 min 21 s 583.49 ms total)
Sun Oct 22 05:03:38 2023: Removed ≈ 58% of redundant conclusions. [ 7389661 of approximately 12740796] (ETC: Sun Oct 22 06:16:00 2023 ; 1 h 12 min 21 s  39.94 ms remaining ; 2 h 52 min 15 s 808.06 ms total)
Sun Oct 22 05:07:02 2023: Removed ≈ 60% of redundant conclusions. [ 7644477 of approximately 12740796] (ETC: Sun Oct 22 06:15:54 2023 ; 1 h  8 min 52 s 103.13 ms remaining ; 2 h 52 min 10 s 256.61 ms total)
Sun Oct 22 05:10:25 2023: Removed ≈ 62% of redundant conclusions. [ 7899293 of approximately 12740796] (ETC: Sun Oct 22 06:15:48 2023 ; 1 h  5 min 23 s 188.72 ms remaining ; 2 h 52 min  4 s 179.74 ms total)
Sun Oct 22 05:13:48 2023: Removed ≈ 64% of redundant conclusions. [ 8154109 of approximately 12740796] (ETC: Sun Oct 22 06:15:42 2023 ; 1 h  1 min 54 s 689.24 ms remaining ; 2 h 51 min 58 s 580.23 ms total)
Sun Oct 22 05:17:16 2023: Removed ≈ 66% of redundant conclusions. [ 8408925 of approximately 12740796] (ETC: Sun Oct 22 06:15:45 2023 ; 58 min 29 s 218.43 ms remaining ; 2 h 52 min  1 s 229.83 ms total)
Sun Oct 22 05:20:42 2023: Removed ≈ 68% of redundant conclusions. [ 8663741 of approximately 12740796] (ETC: Sun Oct 22 06:15:45 2023 ; 55 min  2 s 720.29 ms remaining ; 2 h 52 min  1 s   0.21 ms total)
Sun Oct 22 05:24:02 2023: Removed ≈ 70% of redundant conclusions. [ 8918557 of approximately 12740796] (ETC: Sun Oct 22 06:15:36 2023 ; 51 min 33 s 745.25 ms remaining ; 2 h 51 min 52 s 483.63 ms total)
Sun Oct 22 05:27:20 2023: Removed ≈ 72% of redundant conclusions. [ 9173373 of approximately 12740796] (ETC: Sun Oct 22 06:15:24 2023 ; 48 min  4 s  65.51 ms remaining ; 2 h 51 min 40 s 233.62 ms total)
Sun Oct 22 05:30:37 2023: Removed ≈ 74% of redundant conclusions. [ 9428189 of approximately 12740796] (ETC: Sun Oct 22 06:15:12 2023 ; 44 min 34 s 882.34 ms remaining ; 2 h 51 min 28 s   8.86 ms total)
Sun Oct 22 05:33:54 2023: Removed ≈ 76% of redundant conclusions. [ 9683004 of approximately 12740796] (ETC: Sun Oct 22 06:15:01 2023 ; 41 min  6 s 498.36 ms remaining ; 2 h 51 min 17 s  73.29 ms total)
Sun Oct 22 05:37:12 2023: Removed ≈ 78% of redundant conclusions. [ 9937820 of approximately 12740796] (ETC: Sun Oct 22 06:14:50 2023 ; 37 min 38 s 674.73 ms remaining ; 2 h 51 min  6 s 700.11 ms total)
Sun Oct 22 05:40:29 2023: Removed ≈ 80% of redundant conclusions. [10192636 of approximately 12740796] (ETC: Sun Oct 22 06:14:40 2023 ; 34 min 11 s 314.15 ms remaining ; 2 h 50 min 56 s 567.53 ms total)
Sun Oct 22 05:43:47 2023: Removed ≈ 82% of redundant conclusions. [10447452 of approximately 12740796] (ETC: Sun Oct 22 06:14:31 2023 ; 30 min 44 s 561.33 ms remaining ; 2 h 50 min 47 s 559.70 ms total)
Sun Oct 22 05:47:05 2023: Removed ≈ 84% of redundant conclusions. [10702268 of approximately 12740796] (ETC: Sun Oct 22 06:14:23 2023 ; 27 min 18 s 362.96 ms remaining ; 2 h 50 min 39 s 765.31 ms total)
Sun Oct 22 05:50:23 2023: Removed ≈ 86% of redundant conclusions. [10957084 of approximately 12740796] (ETC: Sun Oct 22 06:14:16 2023 ; 23 min 52 s 477.72 ms remaining ; 2 h 50 min 31 s 980.50 ms total)
Sun Oct 22 05:53:44 2023: Removed ≈ 88% of redundant conclusions. [11211900 of approximately 12740796] (ETC: Sun Oct 22 06:14:11 2023 ; 20 min 27 s 327.09 ms remaining ; 2 h 50 min 27 s 722.51 ms total)
Sun Oct 22 05:57:05 2023: Removed ≈ 90% of redundant conclusions. [11466716 of approximately 12740796] (ETC: Sun Oct 22 06:14:07 2023 ; 17 min  2 s 368.78 ms remaining ; 2 h 50 min 23 s 684.64 ms total)
Sun Oct 22 06:00:21 2023: Removed ≈ 92% of redundant conclusions. [11721532 of approximately 12740796] (ETC: Sun Oct 22 06:13:58 2023 ; 13 min 37 s 166.00 ms remaining ; 2 h 50 min 14 s 571.76 ms total)
Sun Oct 22 06:03:38 2023: Removed ≈ 94% of redundant conclusions. [11976348 of approximately 12740796] (ETC: Sun Oct 22 06:13:50 2023 ; 10 min 12 s 386.31 ms remaining ; 2 h 50 min  6 s 435.36 ms total)
Sun Oct 22 06:06:58 2023: Removed ≈ 96% of redundant conclusions. [12231164 of approximately 12740796] (ETC: Sun Oct 22 06:13:46 2023 ; 6 min 48 s  80.96 ms remaining ; 2 h 50 min  2 s  20.90 ms total)
[Rank 18] Workload transfer approved. Starting to work on 38:[9343868, 9361665].
[Rank 17] Workload transfer approved. Starting to work on 0:[231372, 237303].
[Rank 49] Workload transfer approved. Starting to work on 4:[1192456, 1198387].
[Rank 21] Workload transfer approved. Starting to work on 16:[4075706, 4081637].
Sun Oct 22 06:10:20 2023: Removed ≈ 98% of redundant conclusions. [12485980 of approximately 12740796] (ETC: Sun Oct 22 06:13:44 2023 ; 3 min 24 s  12.19 ms remaining ; 2 h 50 min      606.28 ms total)
[Rank 70] Workload transfer approved. Starting to work on 31:[7679770, 7685701].
[Rank 61] Workload transfer approved. Starting to work on 38:[9361666, 9367597].
[Rank 30] Workload transfer approved. Starting to work on 50:[12244916, 12250847].
[Rank 27] Workload transfer approved. Starting to work on 57:[13926812, 13932743].
[Rank 48] Workload transfer approved. Starting to work on 62:[15128167, 15134098].
[Rank 25] Workload transfer approved. Starting to work on 65:[15848979, 15854910].
[Rank 20] Workload transfer approved. Starting to work on 66:[16089250, 16095181].
[Rank 53] Workload transfer approved. Starting to work on 69:[16810063, 16815994].
[Rank 26] Workload transfer approved. Starting to work on 0:[237304, 239281].
[Rank 37] Workload transfer approved. Starting to work on 1:[477575, 479552].
[Rank 63] Workload transfer approved. Starting to work on 3:[958117, 960094].
[Rank 71] Workload transfer approved. Starting to work on 9:[2399742, 2401719].
[Rank 10] Workload transfer approved. Starting to work on 11:[2880284, 2882261].
[Rank 32] Workload transfer approved. Starting to work on 12:[3120555, 3122532].
[Rank 52] Workload transfer approved. Starting to work on 16:[4081638, 4083615].
[Rank 35] Workload transfer approved. Starting to work on 22:[5523264, 5525241].
[Rank 45] Workload transfer approved. Starting to work on 36:[8887056, 8889033].
[Rank 56] Workload transfer approved. Starting to work on 39:[9607869, 9609846].
[Rank 44] Workload transfer approved. Starting to work on 40:[9848139, 9850116].
[Rank 15] Workload transfer approved. Starting to work on 41:[10088410, 10090387].
[Rank 17] Workload transfer approved. Starting to work on 42:[10328681, 10330658].
[Rank 55] Workload transfer approved. Starting to work on 43:[10568952, 10570929].
[Rank 9] Workload transfer approved. Starting to work on 46:[11289765, 11291742].
[Rank 6] Workload transfer approved. Starting to work on 58:[14173015, 14174992].
[Rank 14] Workload transfer approved. Starting to work on 59:[14413286, 14415263].
[Rank 33] Workload transfer approved. Starting to work on 60:[14653557, 14655534].
[Rank 24] Workload transfer approved. Starting to work on 64:[15614640, 15616617].
[Rank 1] Workload transfer approved. Starting to work on 65:[15854911, 15856888].
[Rank 26] Workload transfer approved. Starting to work on 68:[16575724, 16577701].
[Rank 71] Workload transfer approved. Starting to work on 69:[16815995, 16817972].
[Rank 51] Workload transfer approved. Starting to work on 0:[239282, 240269].
[Rank 23] Workload transfer approved. Starting to work on 3:[960095, 961082].
[Rank 63] Workload transfer approved. Starting to work on 11:[2882262, 2883249].
[Rank 37] Workload transfer approved. Starting to work on 16:[4083616, 4084603].
[Rank 10] Workload transfer approved. Starting to work on 22:[5525242, 5526229].
[Rank 41] Workload transfer approved. Starting to work on 28:[6966867, 6967854].
[Rank 19] Workload transfer approved. Starting to work on 38:[9369576, 9370563].
[Rank 29] Workload transfer approved. Starting to work on 39:[9609847, 9610834].
[Rank 12] Workload transfer approved. Starting to work on 42:[10330659, 10331646].
[Rank 28] Workload transfer approved. Starting to work on 43:[10570930, 10571917].
[Rank 45] Workload transfer approved. Starting to work on 46:[11291743, 11292730].
[Rank 31] Workload transfer approved. Starting to work on 50:[12252826, 12253813].
[Rank 5] Workload transfer approved. Starting to work on 54:[13213910, 13214897].
[Rank 3] Workload transfer approved. Starting to work on 57:[13934722, 13935709].
[Rank 52] Workload transfer approved. Starting to work on 59:[14415264, 14416251].
[Rank 22] Workload transfer approved. Starting to work on 60:[14655535, 14656522].
[Rank 35] Workload transfer approved. Starting to work on 64:[15616618, 15617605].
[Rank 43] Workload transfer approved. Starting to work on 65:[15856889, 15857876].
[Rank 32] Workload transfer approved. Starting to work on 67:[16337431, 16338418].
[Rank 13] Workload transfer approved. Starting to work on 68:[16577702, 16578689].
[Rank 11] Workload transfer approved. Starting to work on 69:[16817973, 16818960].
Sun Oct 22 06:13:52 2023: Removed ≈100% of redundant conclusions. [12740796 of approximately 12740796] (ETC: Sun Oct 22 06:13:52 2023 ; 0.00 ms remaining ; 2 h 50 min  8 s  77.50 ms total)
10574704.98 ms (2 h 56 min 14 s 704.98 ms) taken to detect 12772155 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 4527348 representative and 12772155 redundant condensed detachment proof strings.
[Copy] Removal count: { 151, 12772155 }
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0095.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0105.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0106.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0154.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0167.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0171.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0178.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0186.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0195.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0198.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0201.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0202.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0204.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0205.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0206.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0207.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0209.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0213.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0224.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0271.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0280.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0340.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0342.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 24 on "ncm0344.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 25 on "ncm0345.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 26 on "ncm0346.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 27 on "ncm0351.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 28 on "ncm0354.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 29 on "ncm0363.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 30 on "ncm0416.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 31 on "ncm0421.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 32 on "ncm0464.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 33 on "ncm0466.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 34 on "ncm0472.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 35 on "ncm0490.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 36 on "ncm0495.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 37 on "ncm0498.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 38 on "ncm0503.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 39 on "ncm0546.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 40 on "ncm0549.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 41 on "ncm0556.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 42 on "ncm0573.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 43 on "ncm0575.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 44 on "ncm0586.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 45 on "ncm0601.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 46 on "ncm0741.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 47 on "ncm0756.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 48 on "ncm0763.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 49 on "ncm0787.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 50 on "ncm0791.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 51 on "ncm0805.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 52 on "ncm0815.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 53 on "ncm0874.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 54 on "ncm0884.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 55 on "ncm0905.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 56 on "ncm0919.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 57 on "ncm0923.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 58 on "ncm0925.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 59 on "ncm0947.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 60 on "ncm0952.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 61 on "ncm0955.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 62 on "ncm0964.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 63 on "ncm0978.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 64 on "ncm0988.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 65 on "ncm0991.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 66 on "ncm0996.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 67 on "ncm0998.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 68 on "ncm0999.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 69 on "ncm1006.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 70 on "nrm089.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:19:56 2023: MPI-based D-proof representative filter complete. [rank 71 on "nrm094.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
6272.84 ms (6 s 272.84 ms) taken to filter and order new representative proofs.
Sun Oct 22 06:20:02 2023: Starting to write 4527348 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt.
6033.68 ms (6 s 33.68 ms) taken to print and save 2394008601 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt.
Sun Oct 22 06:20:08 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0033.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 237479, tid:22856952842112]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 62877, tid:22881977755520]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 101889, tid:22563794761600]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 266556, tid:23449134491520]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 246690, tid:23112434595712]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 13644, tid:23065108875136]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 165147, tid:22883564111744]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 104754, tid:23090265003904]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 198259, tid:22457326557056]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 111568, tid:22666438178688]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 102513, tid:22576520443776]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 65519, tid:23127824762752]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 112458, tid:23257082259328]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 48934, tid:22682949552000]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 87567, tid:23175184725888]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 114979, tid:22777186457472]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 218661, tid:22547623630720]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 45120, tid:22421764056960]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 237794, tid:22840307210112]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 201776, tid:23242533934976]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 54658, tid:23437029349248]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 230878, tid:23032448972672]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 128220, tid:22549788600192]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 240347, tid:23363014973312]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 163308, tid:23366341044096]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 147567, tid:22386044106624]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 9684, tid:23000170092416]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 264157, tid:22965684361088]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 53495, tid:23002419263360]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 163719, tid:23058043422592]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 132935, tid:22397695760256]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 156990, tid:22405251852160]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 142606, tid:22358009505664]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 190168, tid:22745488832384]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 193312, tid:23234177247104]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 26470, tid:22577631016832]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 202839, tid:22904331556736]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 220905, tid:22536795682688]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 73186, tid:22808259938176]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 226981, tid:22886894143360]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 143009, tid:22852241987456]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 218926, tid:22548426057600]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 148285, tid:23156946536320]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 40725, tid:22559237670784]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 235580, tid:23213391296384]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 90116, tid:23377883326336]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 2276, tid:22714815293312]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 69210, tid:23257575315328]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 232719, tid:22438374446976]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 126433, tid:23159523977088]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 113390, tid:23073680365440]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 57050, tid:22869321447296]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 261378, tid:22543215269760]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 12125, tid:22625873909632]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 231896, tid:23226914850688]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 85551, tid:23156554188672]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 117884, tid:22460849862528]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 105868, tid:23009840854912]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 87616, tid:22820666042240]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 277284, tid:22609131108224]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 137907, tid:23035522201472]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 152725, tid:23255849265024]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 134440, tid:22818485237632]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 247877, tid:23451583178624]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 174586, tid:22769505163136]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 118764, tid:22888055990144]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 45764, tid:23080435033984]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 216295, tid:22697053906816]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 178708, tid:22845083744128]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 19744, tid:22715342620544]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 24689, tid:22382670600064]
Sun Oct 22 06:21:07 2023: Process terminated. [pid: 146459, tid:22526437062528]