### Running: erun#X----_auto_300#AGT002+2.p
# Preprocessing time       : 0.025 s

# Proof found!
# SZS status Theorem
# Parsed axioms                        : 923
# Removed by relevancy pruning         : 0
# Initial clauses                      : 996
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 996
# Processed clauses                    : 2
# ...of these trivial                  : 0
# ...subsumed                          : 0
# ...remaining for further processing  : 2
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 0
# Generated clauses                    : 0
# ...of the previous two non-trivial   : 0
# Contextual simplify-reflections      : 0
# Paramodulations                      : 0
# Factorizations                       : 0
# Equation resolutions                 : 0
# Current number of processed clauses  : 1
#    Positive orientable unit clauses  : 0
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 1
#    Non-unit-clauses                  : 0
# Current number of unprocessed clauses: 994
# ...number of literals in the above   : 1166
# Clause-clause subsumption calls (NU) : 0
# Rec. Clause-clause subsumption calls : 0
# Unit Clause-clause subsumption calls : 0
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 0
# Indexed BW rewrite successes         : 0
# Unification attempts                 : 1
# Unification successes                : 0
# Backwards rewriting index:     6 leaves,   1.00+/-0.000 terms/leaf
# Paramod-from index:            0 leaves,   0.00+/-0.000 terms/leaf
# Paramod-into index:            5 leaves,   1.00+/-0.000 terms/leaf

# -------------------------------------------------
# User time                : 0.019 s
# System time              : 0.005 s
# Total time               : 0.025 s
# Maximum resident set size: 3334144 pages
### Running: erun#X----_auto_300#AGT003+1.p
# Preprocessing time       : 0.018 s

# Proof found!
# SZS status Theorem
# Parsed axioms                        : 556
# Removed by relevancy pruning         : 0
# Initial clauses                      : 629
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 629
# Processed clauses                    : 5964
# ...of these trivial                  : 211
# ...subsumed                          : 3
# ...remaining for further processing  : 5750
# Other redundant clauses eliminated   : 2
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 3
# Generated clauses                    : 55047
# ...of the previous two non-trivial   : 54629
# Contextual simplify-reflections      : 0
# Paramodulations                      : 55043
# Factorizations                       : 2
# Equation resolutions                 : 2
# Current number of processed clauses  : 5745
#    Positive orientable unit clauses  : 2994
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 2201
#    Non-unit-clauses                  : 550
# Current number of unprocessed clauses: 49294
# ...number of literals in the above   : 81222
# Clause-clause subsumption calls (NU) : 114114
# Rec. Clause-clause subsumption calls : 113946
# Unit Clause-clause subsumption calls : 2327358
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 293
# Indexed BW rewrite successes         : 3
# Unification attempts                 : 67782
# Unification successes                : 62244
# Backwards rewriting index:  5867 leaves,   1.13+/-2.469 terms/leaf
# Paramod-from index:         2896 leaves,   1.04+/-0.376 terms/leaf
# Paramod-into index:         5575 leaves,   1.08+/-1.799 terms/leaf

# -------------------------------------------------
# User time                : 1.116 s
# System time              : 0.045 s
# Total time               : 1.161 s
# Maximum resident set size: 47443968 pages
### Running: erun#X----_auto_300#AGT003+2.p
# Preprocessing time       : 0.022 s

# Proof found!
# SZS status Theorem
# Parsed axioms                        : 923
# Removed by relevancy pruning         : 0
# Initial clauses                      : 996
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 996
# Processed clauses                    : 1018
# ...of these trivial                  : 37
# ...subsumed                          : 3
# ...remaining for further processing  : 978
# Other redundant clauses eliminated   : 2
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 0
# Generated clauses                    : 1394
# ...of the previous two non-trivial   : 717
# Contextual simplify-reflections      : 0
# Paramodulations                      : 1390
# Factorizations                       : 2
# Equation resolutions                 : 2
# Current number of processed clauses  : 976
#    Positive orientable unit clauses  : 819
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 47
#    Non-unit-clauses                  : 110
# Current number of unprocessed clauses: 695
# ...number of literals in the above   : 1731
# Clause-clause subsumption calls (NU) : 387
# Rec. Clause-clause subsumption calls : 266
# Unit Clause-clause subsumption calls : 672
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 347
# Indexed BW rewrite successes         : 0
# Unification attempts                 : 3216
# Unification successes                : 2221
# Backwards rewriting index:  1121 leaves,   1.48+/-4.012 terms/leaf
# Paramod-from index:          644 leaves,   1.28+/-0.764 terms/leaf
# Paramod-into index:         1109 leaves,   1.44+/-4.011 terms/leaf

# -------------------------------------------------
# User time                : 0.049 s
# System time              : 0.008 s
# Total time               : 0.057 s
# Maximum resident set size: 7323648 pages
### Job complete ###