WATCH: 0.00 CPU 0.01 WC
# Preprocessing time       : 0.007 s
# Problem is unsatisfiable (or provable), constructing proof object
# SZS status Theorem
# SZS output start CNFRefutation.
fof(1, axiom,?[X1]:?[X2]:![X3]:![X4]:((X4=X2&X1=X3)<=>big_f(X3,X4)),file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p', pel52_1)).
fof(2, conjecture,?[X2]:![X4]:(?[X1]:![X3]:(X3=X1<=>big_f(X3,X4))<=>X4=X2),file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p', pel52)).
fof(3, negated_conjecture,~(?[X2]:![X4]:(?[X1]:![X3]:(X3=X1<=>big_f(X3,X4))<=>X4=X2)),inference(assume_negation,[status(cth)],[2])).
fof(4, plain,?[X1]:?[X2]:![X3]:![X4]:(((~(X4=X2)|~(X1=X3))|big_f(X3,X4))&(~(big_f(X3,X4))|(X4=X2&X1=X3))),inference(fof_nnf,[status(thm)],[1])).
fof(5, plain,?[X5]:?[X6]:![X7]:![X8]:(((~(X8=X6)|~(X5=X7))|big_f(X7,X8))&(~(big_f(X7,X8))|(X8=X6&X5=X7))),inference(variable_rename,[status(thm)],[4])).
fof(6, plain,![X7]:![X8]:(((~(X8=esk2_0)|~(esk1_0=X7))|big_f(X7,X8))&(~(big_f(X7,X8))|(X8=esk2_0&esk1_0=X7))),inference(skolemize,[status(esa)],[5])).
fof(7, plain,![X7]:![X8]:(((~(X8=esk2_0)|~(esk1_0=X7))|big_f(X7,X8))&((X8=esk2_0|~(big_f(X7,X8)))&(esk1_0=X7|~(big_f(X7,X8))))),inference(distribute,[status(thm)],[6])).
cnf(8,plain,(esk1_0=X1|~big_f(X1,X2)),inference(split_conjunct,[status(thm)],[7])).
cnf(9,plain,(X2=esk2_0|~big_f(X1,X2)),inference(split_conjunct,[status(thm)],[7])).
cnf(10,plain,(big_f(X1,X2)|esk1_0!=X1|X2!=esk2_0),inference(split_conjunct,[status(thm)],[7])).
fof(11, negated_conjecture,![X2]:?[X4]:((![X1]:?[X3]:((~(X3=X1)|~(big_f(X3,X4)))&(X3=X1|big_f(X3,X4)))|~(X4=X2))&(?[X1]:![X3]:((~(X3=X1)|big_f(X3,X4))&(~(big_f(X3,X4))|X3=X1))|X4=X2)),inference(fof_nnf,[status(thm)],[3])).
fof(12, negated_conjecture,![X5]:?[X6]:((![X7]:?[X8]:((~(X8=X7)|~(big_f(X8,X6)))&(X8=X7|big_f(X8,X6)))|~(X6=X5))&(?[X9]:![X10]:((~(X10=X9)|big_f(X10,X6))&(~(big_f(X10,X6))|X10=X9))|X6=X5)),inference(variable_rename,[status(thm)],[11])).
fof(13, negated_conjecture,![X5]:((![X7]:((~(esk4_2(X5,X7)=X7)|~(big_f(esk4_2(X5,X7),esk3_1(X5))))&(esk4_2(X5,X7)=X7|big_f(esk4_2(X5,X7),esk3_1(X5))))|~(esk3_1(X5)=X5))&(![X10]:((~(X10=esk5_1(X5))|big_f(X10,esk3_1(X5)))&(~(big_f(X10,esk3_1(X5)))|X10=esk5_1(X5)))|esk3_1(X5)=X5)),inference(skolemize,[status(esa)],[12])).
fof(14, negated_conjecture,![X5]:![X7]:![X10]:((((~(esk4_2(X5,X7)=X7)|~(big_f(esk4_2(X5,X7),esk3_1(X5))))&(esk4_2(X5,X7)=X7|big_f(esk4_2(X5,X7),esk3_1(X5))))|~(esk3_1(X5)=X5))&(((~(X10=esk5_1(X5))|big_f(X10,esk3_1(X5)))&(~(big_f(X10,esk3_1(X5)))|X10=esk5_1(X5)))|esk3_1(X5)=X5)),inference(shift_quantors,[status(thm)],[13])).
fof(15, negated_conjecture,![X5]:![X7]:![X10]:((((~(esk4_2(X5,X7)=X7)|~(big_f(esk4_2(X5,X7),esk3_1(X5))))|~(esk3_1(X5)=X5))&((esk4_2(X5,X7)=X7|big_f(esk4_2(X5,X7),esk3_1(X5)))|~(esk3_1(X5)=X5)))&(((~(X10=esk5_1(X5))|big_f(X10,esk3_1(X5)))|esk3_1(X5)=X5)&((~(big_f(X10,esk3_1(X5)))|X10=esk5_1(X5))|esk3_1(X5)=X5))),inference(distribute,[status(thm)],[14])).
cnf(17,negated_conjecture,(esk3_1(X1)=X1|big_f(X2,esk3_1(X1))|X2!=esk5_1(X1)),inference(split_conjunct,[status(thm)],[15])).
cnf(18,negated_conjecture,(big_f(esk4_2(X1,X2),esk3_1(X1))|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1),inference(split_conjunct,[status(thm)],[15])).
cnf(19,negated_conjecture,(esk3_1(X1)!=X1|~big_f(esk4_2(X1,X2),esk3_1(X1))|esk4_2(X1,X2)!=X2),inference(split_conjunct,[status(thm)],[15])).
cnf(22,negated_conjecture,(esk3_1(X1)=X1|big_f(esk5_1(X1),esk3_1(X1))),inference(er,[status(thm)],[17,theory(equality)])).
cnf(24,negated_conjecture,(esk1_0=esk4_2(X1,X2)|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1),inference(spm,[status(thm)],[8,18,theory(equality)])).
cnf(25,negated_conjecture,(esk2_0=esk3_1(X1)|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1),inference(spm,[status(thm)],[9,18,theory(equality)])).
cnf(27,negated_conjecture,(esk4_2(X1,X2)!=X2|esk3_1(X1)!=X1|esk1_0!=esk4_2(X1,X2)|esk2_0!=esk3_1(X1)),inference(spm,[status(thm)],[19,10,theory(equality)])).
cnf(29,negated_conjecture,(esk1_0=esk5_1(X1)|esk3_1(X1)=X1),inference(spm,[status(thm)],[8,22,theory(equality)])).
cnf(30,negated_conjecture,(esk2_0=esk3_1(X1)|esk3_1(X1)=X1),inference(spm,[status(thm)],[9,22,theory(equality)])).
cnf(32,negated_conjecture,(esk3_1(X1)=X1|big_f(esk1_0,esk3_1(X1))),inference(spm,[status(thm)],[22,29,theory(equality)])).
cnf(33,negated_conjecture,(esk3_1(X2)=X2|esk2_0!=X2),inference(ef,[status(thm)],[30,theory(equality)])).
cnf(46,negated_conjecture,(esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),X1)|esk2_0!=X1),inference(spm,[status(thm)],[19,33,theory(equality)])).
cnf(54,negated_conjecture,(esk2_0=X1|big_f(esk1_0,esk2_0)|esk3_1(X1)=X1),inference(spm,[status(thm)],[32,30,theory(equality)])).
cnf(60,negated_conjecture,(esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),X1)),inference(csr,[status(thm)],[46,9])).
cnf(70,negated_conjecture,(esk3_1(X1)=X1|big_f(esk1_0,esk2_0)),inference(csr,[status(thm)],[54,33])).
cnf(75,negated_conjecture,(esk3_1(X1)=esk2_0|esk4_2(X1,X2)=X2),inference(csr,[status(thm)],[25,30])).
cnf(78,negated_conjecture,(esk3_1(X1)=esk2_0|~big_f(X2,X1)),inference(spm,[status(thm)],[60,75,theory(equality)])).
cnf(84,negated_conjecture,(esk3_1(esk2_0)=esk2_0|esk3_1(X1)=X1),inference(spm,[status(thm)],[78,70,theory(equality)])).
cnf(99,negated_conjecture,(esk3_1(esk2_0)=esk2_0),inference(ef,[status(thm)],[84,theory(equality)])).
cnf(111,negated_conjecture,(esk4_2(esk2_0,X1)=esk1_0|esk4_2(esk2_0,X1)=X1),inference(spm,[status(thm)],[24,99,theory(equality)])).
cnf(225,negated_conjecture,(esk4_2(esk2_0,X2)=X2|esk1_0!=X2),inference(ef,[status(thm)],[111,theory(equality)])).
cnf(269,negated_conjecture,(X1!=esk1_0|esk3_1(esk2_0)!=esk2_0),inference(spm,[status(thm)],[27,225,theory(equality)])).
cnf(276,negated_conjecture,(X1!=esk1_0|$false),inference(rw,[status(thm)],[269,99,theory(equality)])).
cnf(277,negated_conjecture,(X1!=esk1_0),inference(cn,[status(thm)],[276,theory(equality)])).
cnf(278,negated_conjecture,($false),inference(er,[status(thm)],[277,theory(equality)])).
cnf(281,negated_conjecture,($false),278,['proof']).
# SZS output end CNFRefutation
# Initial clauses in saturation        : 7
# Processed clauses                    : 74
# ...of these trivial                  : 0
# ...subsumed                          : 25
# ...remaining for further processing  : 49
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 5
# Backward-rewritten                   : 0
# Generated clauses                    : 192
# ...of the previous two non-trivial   : 143
# Contextual simplify-reflections      : 23
# Paramodulations                      : 180
# Factorizations                       : 6
# Equation resolutions                 : 4
# Current number of processed clauses  : 35
#    Positive orientable unit clauses  : 1
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 1
#    Non-unit-clauses                  : 33
# Current number of unprocessed clauses: 60
# ...number of literals in the above   : 186
# Clause-clause subsumption calls (NU) : 165
# Rec. Clause-clause subsumption calls : 155
# Unit Clause-clause subsumption calls : 7
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 1
# Indexed BW rewrite successes         : 1
# Unification attempts                 : 166
# Unification successes                : 122
# Backwards rewriting index :    21 leaves,   1.05+/-0.213 terms/leaf
# Paramod-from index        :    14 leaves,   1.00+/-0.000 terms/leaf
# Paramod-into index        :    20 leaves,   1.05+/-0.218 terms/leaf

# -------------------------------------------------
# User time                : 0.010 s
# System time              : 0.000 s
# Total time               : 0.010 s
# Maximum resident set size: 2664 pages

WATCH: 0.10 CPU 0.54 WC

FINAL WATCH: 0.10 CPU 0.54 WC