WATCH: 0.00 CPU 0.01 WC
# Preprocessing time       : 0.333 s
# Problem is unsatisfiable (or provable), constructing proof object
# SZS status Theorem
# SZS answers Tuple [|_]
# SZS output start CNFRefutation.
fof(4108, axiom,genls(c_tptpcol_16_130924,c_tptpcol_15_130923),file('/CW/home-0/sutcliff/TPTP/Axioms/CSR002+2.ax', ax2_4328)).
fof(8006, conjecture,(genls(c_tptpcol_16_130924,c_tptpcol_15_130923)<=mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p', query172)).
fof(8007, negated_conjecture,~((genls(c_tptpcol_16_130924,c_tptpcol_15_130923)<=mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885)))),inference(assume_negation,[status(cth)],[8006])).
fof(10410, negated_conjecture,~((mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885))=>genls(c_tptpcol_16_130924,c_tptpcol_15_130923))),inference(fof_simplification,[status(thm)],[8007,theory(equality)])).
cnf(19334,plain,(genls(c_tptpcol_16_130924,c_tptpcol_15_130923)),inference(split_conjunct,[status(thm)],[4108])).
fof(27815, negated_conjecture,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885))&~(genls(c_tptpcol_16_130924,c_tptpcol_15_130923))),inference(fof_nnf,[status(thm)],[10410])).
cnf(27816,negated_conjecture,(~genls(c_tptpcol_16_130924,c_tptpcol_15_130923)),inference(split_conjunct,[status(thm)],[27815])).
cnf(28579,plain,($false),inference(sr,[status(thm)],[19334,27816,theory(equality)])).
cnf(28580,plain,($false),inference(,[status(unknown)],[28579,theory(equality)])).
cnf(28581,plain,($false),28580,['proof']).
# SZS output end CNFRefutation
# Initial clauses in saturation        : 8007
# Processed clauses                    : 3968
# ...of these trivial                  : 240
# ...subsumed                          : 167
# ...remaining for further processing  : 3560
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 16
# Generated clauses                    : 504
# ...of the previous two non-trivial   : 503
# Contextual simplify-reflections      : 0
# Paramodulations                      : 504
# Factorizations                       : 0
# Equation resolutions                 : 0
# Current number of processed clauses  : 3544
#    Positive orientable unit clauses  : 1857
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 33
#    Non-unit-clauses                  : 1654
# Current number of unprocessed clauses: 4542
# ...number of literals in the above   : 8214
# Clause-clause subsumption calls (NU) : 1334875
# Rec. Clause-clause subsumption calls : 1334794
# Unit Clause-clause subsumption calls : 2583
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 16
# Indexed BW rewrite successes         : 16
# Unification attempts                 : 3760
# Unification successes                : 3078
# Backwards rewriting index :  5904 leaves,   1.01+/-0.136 terms/leaf
# Paramod-from index        :  2805 leaves,   1.00+/-0.000 terms/leaf
# Paramod-into index        :  4751 leaves,   1.01+/-0.075 terms/leaf

# -------------------------------------------------
# User time                : 0.657 s
# System time              : 0.033 s
# Total time               : 0.690 s
# Maximum resident set size: 32328 pages

WATCH: 1.39 CPU 1.47 WC

FINAL WATCH: 1.39 CPU 1.47 WC