WATCH: 0.00 CPU 0.01 WC # Garbage collection reclaimed 61 unused term cells. # Garbage collection reclaimed 169 unused term cells. # Auto-Ordering is analysing problem. # Problem is type GHSFNFFSF21MS # Auto-mode selected ordering type KBO6 # Auto-mode selected ordering precedence scheme # Auto-mode selected weight ordering scheme # # Auto-Heuristic is analysing problem. # Problem is type GHSFNFFSF21MS # Auto-Mode selected heuristic G_E___107_C41_F1_PI_AE_Q4_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Initializing proof state # Scanning for AC axioms # Presaturation interreduction done # Proof found! # SZS status Theorem # Parsed axioms : 2 # Removed by relevancy pruning : 0 # Initial clauses : 7 # Removed in clause preprocessing : 0 # 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 : 22 # 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: 61 # ...number of literals in the above : 190 # Clause-clause subsumption calls (NU) : 160 # Rec. Clause-clause subsumption calls : 151 # Unit Clause-clause subsumption calls : 7 # Rewrite failures with RHS unbound : 0 # Indexed BW rewrite attempts : 1 # Indexed BW rewrite successes : 1 # 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 # 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(31,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)],[31,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(232,negated_conjecture,(esk4_2(esk2_0,X2)=X2|esk1_0!=X2),inference(ef,[status(thm)],[111,theory(equality)])). cnf(268,negated_conjecture,(X1!=esk1_0|esk3_1(esk2_0)!=esk2_0),inference(spm,[status(thm)],[27,232,theory(equality)])). cnf(275,negated_conjecture,(X1!=esk1_0|$false),inference(rw,[status(thm)],[268,99,theory(equality)])). cnf(276,negated_conjecture,(X1!=esk1_0),inference(cn,[status(thm)],[275,theory(equality)])). cnf(277,negated_conjecture,($false),inference(er,[status(thm)],[276,theory(equality)])). cnf(280,negated_conjecture,($false),277,['proof']). # SZS output end CNFRefutation WATCH: 0.01 CPU 0.14 WC FINAL WATCH: 0.01 CPU 0.14 WC