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, 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 # 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 # Unification attempts : 111 # Unification successes : 86 # 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 # ------------------------------------------------- # User time : 0.003 s # System time : 0.003 s # Total time : 0.007 s # Maximum resident set size: 2628 pages WATCH: 0.10 CPU 0.18 WC FINAL WATCH: 0.10 CPU 0.18 WC