WATCH: 0.00 CPU 0.01 WC
# Garbage collection reclaimed 4982 unused term cells.
# Garbage collection reclaimed 20926 unused term cells.
# Garbage collection reclaimed 17766 unused term cells.
# Garbage collection reclaimed 15027 unused term cells.
# Garbage collection reclaimed 12490 unused term cells.
# Garbage collection reclaimed 5201 unused term cells.
# Auto-Ordering is analysing problem.
# Problem is type HHNMNSMLM31LM
# Auto-mode selected ordering type KBO6
# Auto-mode selected ordering precedence scheme <invfreq>
# Auto-mode selected weight ordering scheme <precrank20>
#
# Auto-Heuristic is analysing problem.
# Problem is type HHNMNSMLM31LM
# Auto-Mode selected heuristic H_____011_C41_F1_PI_AE_SP_SOV
# and selection function PSelectComplexExceptRRHorn.
#
# No equality, disabling AC handling.
#
# Initializing proof state
# Garbage collection reclaimed 5815 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 257 unused term cells.
# Garbage collection reclaimed 256 unused term cells.
# Garbage collection reclaimed 257 unused term cells.
# Garbage collection reclaimed 256 unused term cells.
# Garbage collection reclaimed 256 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 255 unused term cells.
# Garbage collection reclaimed 256 unused term cells.
# Proof found!
# SZS status Theorem
# Parsed axioms                        : 8006
# Removed by relevancy pruning         : 0
# Initial clauses                      : 8007
# Removed in clause preprocessing      : 0
# 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
# 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
# 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(eval_answer_literal,[status(thm)],[28579,theory(answers)])).
cnf(28581,plain,($false),28580,['proof']).
# SZS output end CNFRefutation

WATCH: 0.80 CPU 0.83 WC

FINAL WATCH: 0.80 CPU 0.83 WC