Sender: LSF System <lsfadmin@n0237.pegasus.edu>
Subject: Job 2326943: <erun#test1#ALG154+1.p> Done

Job <erun#test1#ALG154+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:01:02 2010

Your job looked like:

------------------------------------------------------------
# LSBATCH: User input
#!/bin/bash
#BSUB -J erun#test1#ALG154+1.p
#BSUB -o erun#test1#ALG154+1.p.out   
#BSUB -e erun#test1#ALG154+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 ALG154+1.p
echo "### Job complete ###"

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

Successfully completed.

Resource usage summary:

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

    Max Processes  :         1
    Max Threads    :         1

The output (if any) follows:

# Preprocessing time       : 0.043 s

# Proof found!
# SZS status Unsatisfiable
# Parsed axioms                        : 29
# Removed by relevancy pruning         : 0
# Initial clauses                      : 1602
# Removed in clause preprocessing      : 252
# Initial clauses in saturation        : 1350
# Processed clauses                    : 41517
# ...of these trivial                  : 173
# ...subsumed                          : 32879
# ...remaining for further processing  : 8465
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 5414
# Backward-rewritten                   : 2483
# Generated clauses                    : 262376
# ...of the previous two non-trivial   : 258808
# Contextual simplify-reflections      : 73862
# Paramodulations                      : 260907
# Factorizations                       : 1169
# Equation resolutions                 : 0
# Current number of processed clauses  : 268
#    Positive orientable unit clauses  : 28
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 50
#    Non-unit-clauses                  : 190
# Current number of unprocessed clauses: 759
# ...number of literals in the above   : 4363
# Clause-clause subsumption calls (NU) : 1601468
# Rec. Clause-clause subsumption calls : 185346
# Unit Clause-clause subsumption calls : 3483
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 24
# Indexed BW rewrite successes         : 24
# Backwards rewriting index:    51 leaves,   1.00+/-0.000 terms/leaf
# Paramod-from index:           37 leaves,   1.00+/-0.000 terms/leaf
# Paramod-into index:           46 leaves,   1.00+/-0.000 terms/leaf

# -------------------------------------------------
# User time                : 7.332 s
# System time              : 0.041 s
# Total time               : 7.373 s
# Maximum resident set size: 0 pages
### Job complete ###


PS:

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