WATCH: 0.00 CPU 0.01 WC # Garbage collection reclaimed 17 unused term cells. # Garbage collection reclaimed 95 unused term cells. # Auto-Ordering is analysing problem. # Problem is type HUNSGFFSF21SM # 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 HUNSGFFSF21SM # Auto-Mode selected heuristic H_____011_C07_F1_PI_AE_Q4_CS_SP_PS_SOV # and selection function PSelectComplexExceptRRHorn. # # No equality, disabling AC handling. # # Initializing proof state # Presaturation interreduction done # Proof found! # SZS status Theorem # Parsed axioms : 1 # Removed by relevancy pruning : 0 # Initial clauses : 5 # Removed in clause preprocessing : 0 # Initial clauses in saturation : 5 # Processed clauses : 30 # ...of these trivial : 0 # ...subsumed : 0 # ...remaining for further processing : 30 # Other redundant clauses eliminated : 0 # Clauses deleted for lack of memory : 0 # Backward-subsumed : 1 # Backward-rewritten : 1 # Generated clauses : 45 # ...of the previous two non-trivial : 41 # Contextual simplify-reflections : 0 # Paramodulations : 45 # Factorizations : 0 # Equation resolutions : 0 # Current number of processed clauses : 23 # Positive orientable unit clauses : 4 # Positive unorientable unit clauses: 0 # Negative unit clauses : 2 # Non-unit-clauses : 17 # Current number of unprocessed clauses: 11 # ...number of literals in the above : 30 # Clause-clause subsumption calls (NU) : 48 # Rec. Clause-clause subsumption calls : 48 # Unit Clause-clause subsumption calls : 12 # Rewrite failures with RHS unbound : 0 # Indexed BW rewrite attempts : 14 # Indexed BW rewrite successes : 2 # Backwards rewriting index : 21 leaves, 2.67+/-2.417 terms/leaf # Paramod-from index : 3 leaves, 2.00+/-0.816 terms/leaf # Paramod-into index : 20 leaves, 2.55+/-2.479 terms/leaf # SZS output start CNFRefutation. fof(1, conjecture,~(((((![X1]:![X2]:((~(a_truth(X1))|a_truth(X2))|~(a_truth(implies(X1,X2))))&![X1]:![X2]:a_truth(implies(X1,implies(X2,X1))))&?[X3]:~(a_truth(implies(X3,X3))))&![X1]:![X2]:a_truth(implies(implies(not(X1),not(X2)),implies(X2,X1))))&![X1]:![X2]:![X4]:a_truth(implies(implies(X1,implies(X2,X4)),implies(implies(X1,X2),implies(X1,X4)))))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p', thm147)). fof(2, negated_conjecture,~(~(((((![X1]:![X2]:((~(a_truth(X1))|a_truth(X2))|~(a_truth(implies(X1,X2))))&![X1]:![X2]:a_truth(implies(X1,implies(X2,X1))))&?[X3]:~(a_truth(implies(X3,X3))))&![X1]:![X2]:a_truth(implies(implies(not(X1),not(X2)),implies(X2,X1))))&![X1]:![X2]:![X4]:a_truth(implies(implies(X1,implies(X2,X4)),implies(implies(X1,X2),implies(X1,X4))))))),inference(assume_negation,[status(cth)],[1])). fof(3, negated_conjecture,~(~(((((![X1]:![X2]:((~(a_truth(X1))|a_truth(X2))|~(a_truth(implies(X1,X2))))&![X1]:![X2]:a_truth(implies(X1,implies(X2,X1))))&?[X3]:~(a_truth(implies(X3,X3))))&![X1]:![X2]:a_truth(implies(implies(not(X1),not(X2)),implies(X2,X1))))&![X1]:![X2]:![X4]:a_truth(implies(implies(X1,implies(X2,X4)),implies(implies(X1,X2),implies(X1,X4))))))),inference(fof_simplification,[status(thm)],[2,theory(equality)])). fof(4, negated_conjecture,((((![X1]:![X2]:((~(a_truth(X1))|a_truth(X2))|~(a_truth(implies(X1,X2))))&![X1]:![X2]:a_truth(implies(X1,implies(X2,X1))))&?[X3]:~(a_truth(implies(X3,X3))))&![X1]:![X2]:a_truth(implies(implies(not(X1),not(X2)),implies(X2,X1))))&![X1]:![X2]:![X4]:a_truth(implies(implies(X1,implies(X2,X4)),implies(implies(X1,X2),implies(X1,X4))))),inference(fof_nnf,[status(thm)],[3])). fof(5, negated_conjecture,((((![X5]:![X6]:((~(a_truth(X5))|a_truth(X6))|~(a_truth(implies(X5,X6))))&![X7]:![X8]:a_truth(implies(X7,implies(X8,X7))))&?[X9]:~(a_truth(implies(X9,X9))))&![X10]:![X11]:a_truth(implies(implies(not(X10),not(X11)),implies(X11,X10))))&![X12]:![X13]:![X14]:a_truth(implies(implies(X12,implies(X13,X14)),implies(implies(X12,X13),implies(X12,X14))))),inference(variable_rename,[status(thm)],[4])). fof(6, negated_conjecture,((((![X5]:![X6]:((~(a_truth(X5))|a_truth(X6))|~(a_truth(implies(X5,X6))))&![X7]:![X8]:a_truth(implies(X7,implies(X8,X7))))&~(a_truth(implies(esk1_0,esk1_0))))&![X10]:![X11]:a_truth(implies(implies(not(X10),not(X11)),implies(X11,X10))))&![X12]:![X13]:![X14]:a_truth(implies(implies(X12,implies(X13,X14)),implies(implies(X12,X13),implies(X12,X14))))),inference(skolemize,[status(esa)],[5])). fof(7, negated_conjecture,![X5]:![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X13]:![X14]:((((((~(a_truth(X5))|a_truth(X6))|~(a_truth(implies(X5,X6))))&a_truth(implies(X7,implies(X8,X7))))&~(a_truth(implies(esk1_0,esk1_0))))&a_truth(implies(implies(not(X10),not(X11)),implies(X11,X10))))&a_truth(implies(implies(X12,implies(X13,X14)),implies(implies(X12,X13),implies(X12,X14))))),inference(shift_quantors,[status(thm)],[6])). cnf(8,negated_conjecture,(a_truth(implies(implies(X1,implies(X2,X3)),implies(implies(X1,X2),implies(X1,X3))))),inference(split_conjunct,[status(thm)],[7])). cnf(10,negated_conjecture,(~a_truth(implies(esk1_0,esk1_0))),inference(split_conjunct,[status(thm)],[7])). cnf(11,negated_conjecture,(a_truth(implies(X1,implies(X2,X1)))),inference(split_conjunct,[status(thm)],[7])). cnf(12,negated_conjecture,(a_truth(X2)|~a_truth(implies(X1,X2))|~a_truth(X1)),inference(split_conjunct,[status(thm)],[7])). cnf(15,negated_conjecture,(a_truth(implies(implies(X1,X2),implies(X1,X3)))|~a_truth(implies(X1,implies(X2,X3)))),inference(spm,[status(thm)],[12,8,theory(equality)])). cnf(32,negated_conjecture,(a_truth(implies(X1,X2))|~a_truth(implies(X1,X3))|~a_truth(implies(X1,implies(X3,X2)))),inference(spm,[status(thm)],[12,15,theory(equality)])). cnf(43,negated_conjecture,(a_truth(implies(X1,X1))|~a_truth(implies(X1,X2))),inference(spm,[status(thm)],[32,11,theory(equality)])). cnf(47,negated_conjecture,(a_truth(implies(X1,X1))),inference(spm,[status(thm)],[43,11,theory(equality)])). cnf(58,negated_conjecture,($false),inference(rw,[status(thm)],[10,47,theory(equality)])). cnf(59,negated_conjecture,($false),inference(cn,[status(thm)],[58,theory(equality)])). cnf(60,negated_conjecture,($false),59,['proof']). # SZS output end CNFRefutation WATCH: 0.00 CPU 0.10 WC FINAL WATCH: 0.00 CPU 0.10 WC