Sender: LSF System <lsfadmin@n0237.pegasus.edu>
Subject: Job 2326944: <erun#test1#BOO001-1.p> Done

Job <erun#test1#BOO001-1.p> was submitted from host <u03> by user <sschulz> in cluster <lsfcluster>.
Job was executed on host(s) <n0237.pegasus.edu>, in queue <small>, as user <sschulz> in cluster <lsfcluster>.
</nethome/sschulz> was used as the home directory.
</nethome/sschulz> was used as the working directory.
Started at Mon Dec  6 19:00:54 2010
Results reported at Mon Dec  6 19:00:55 2010

Your job looked like:

------------------------------------------------------------
# LSBATCH: User input
#!/bin/bash
#BSUB -J erun#test1#BOO001-1.p
#BSUB -o erun#test1#BOO001-1.p.out   
#BSUB -e erun#test1#BOO001-1.p.err 
#BSUB -W 0:10   
#BSUB -q small 
#BSUB -n 1      
#
# Run serial executable on 1 cpu of one node
cd ${HOME}/EPROVER/TESTRUNS_BATCH
env TPTP=${HOME}/EPROVER/TPTP_4.1.0_FLAT ${HOME}/bin/eprover -s --print-statistics --cpu-limit=300 --tptp3-format --resources-info -xAuto -tAuto BOO001-1.p
echo "### Job complete ###"

------------------------------------------------------------

Successfully completed.

Resource usage summary:

    CPU time   :      0.02 sec.
    Max Memory :         2 MB
    Max Swap   :        23 MB

    Max Processes  :         1
    Max Threads    :         1

The output (if any) follows:

# Preprocessing time       : 0.004 s
# Presaturation interreduction done

# Proof found!
# SZS status Unsatisfiable
# Parsed axioms                        : 6
# Removed by relevancy pruning         : 0
# Initial clauses                      : 6
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 6
# Processed clauses                    : 20
# ...of these trivial                  : 1
# ...subsumed                          : 0
# ...remaining for further processing  : 19
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 1
# Generated clauses                    : 84
# ...of the previous two non-trivial   : 50
# Contextual simplify-reflections      : 0
# Paramodulations                      : 84
# Factorizations                       : 0
# Equation resolutions                 : 0
# Current number of processed clauses  : 12
#    Positive orientable unit clauses  : 12
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 0
#    Non-unit-clauses                  : 0
# Current number of unprocessed clauses: 42
# ...number of literals in the above   : 42
# 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          : 62
# Indexed BW rewrite successes         : 1
# Backwards rewriting index:     7 leaves,   3.43+/-4.747 terms/leaf
# Paramod-from index:            5 leaves,   2.40+/-2.332 terms/leaf
# Paramod-into index:            7 leaves,   2.86+/-3.356 terms/leaf

# -------------------------------------------------
# User time                : 0.004 s
# System time              : 0.001 s
# Total time               : 0.005 s
# Maximum resident set size: 0 pages
### Job complete ###


PS:

Read file <erun#test1#BOO001-1.p.err> for stderr output of this job.