% SZS start RequiredInformation % Congratulations - you have become a registered power user of SystemOnTPTP, at IP address 89.186.28.63. % Please consider donating to the TPTP project - see www.tptp.org for details. % When you donate this message will disappear. % If you do not donate a random delay might be added to your processing time. % SZS end RequiredInformation % START OF SYSTEM OUTPUT # Version: 1.9.1pre011 # No SInE strategy applied # Trying AutoSched0 for 121 seconds # AutoSched0-Mode selected heuristic G_E___107_C36_F1_PI_AE_Q4_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Preprocessing time : 0.016 s # Presaturation interreduction done # Proof found! # SZS status Theorem # SZS output start CNFRefutation fof(c_0_0, conjecture, (![X1]:![X3]:![X4]:![X11]:((phtxt(X1,X3)&phtxt(X4,X11))=>(X1=X4<=>![X8]:![X2]:(occ(X1,X8,X2)<=>occ(X4,X8,X2))))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', conjecture44)). fof(c_0_1, axiom, (![X7]:![X8]:![X2]:(occ(X7,X8,X2)=>(present(X7,X2)&present(X8,X2)))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', axiom13)). fof(c_0_2, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>?[X8]:occ(X1,X8,X2))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', axiom28)). fof(c_0_3, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', definition4)). fof(c_0_4, axiom, (![X1]:![X4]:![X2]:(phpt(X1,X4,X2)<=>((pt(X1,X4,X2)&phtxt(X1,X2))&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', definition18)). fof(c_0_5, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X3]:(present(X1,X3)=>phtxt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', axiom2)). fof(c_0_6, axiom, (![X1]:![X8]:![X2]:![X4]:((occ(X1,X8,X2)&occ(X4,X8,X2))=>((phtxt(X1,X2)&phtxt(X4,X2))=>X1=X4))), file('/tmp/SystemOnTPTPFormReply60308/SOT_KJVp6v', axiom29)). fof(c_0_7, negated_conjecture, (~(![X1]:![X3]:![X4]:![X11]:((phtxt(X1,X3)&phtxt(X4,X11))=>(X1=X4<=>![X8]:![X2]:(occ(X1,X8,X2)<=>occ(X4,X8,X2)))))), inference(assume_negation,[status(cth)],[c_0_0])). fof(c_0_8, plain, (![X9]:![X10]:![X11]:((present(X9,X11)|~occ(X9,X10,X11))&(present(X10,X11)|~occ(X9,X10,X11)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])). fof(c_0_9, negated_conjecture, (![X18]:![X19]:![X20]:![X21]:((phtxt(esk17_0,esk18_0)&phtxt(esk19_0,esk20_0))&((((~occ(esk17_0,esk21_0,esk22_0)|~occ(esk19_0,esk21_0,esk22_0))|esk17_0!=esk19_0)&((occ(esk17_0,esk21_0,esk22_0)|occ(esk19_0,esk21_0,esk22_0))|esk17_0!=esk19_0))&(((~occ(esk17_0,X18,X19)|occ(esk19_0,X18,X19))|esk17_0=esk19_0)&((~occ(esk19_0,X20,X21)|occ(esk17_0,X20,X21))|esk17_0=esk19_0))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])])])). cnf(c_0_10, plain, (present(X1,X3)|~occ(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_8])). cnf(c_0_11, negated_conjecture, (esk17_0=esk19_0|occ(esk17_0,X1,X2)|~occ(esk19_0,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_9])). fof(c_0_12, plain, (![X9]:![X10]:(~phtxt(X9,X10)|occ(X9,esk16_2(X9,X10),X10))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])). fof(c_0_13, plain, (![X5]:![X6]:![X7]:![X8]:![X9]:![X10]:(((((X5=X6|ppt(X5,X6,X7))|~pt(X5,X6,X7))&((present(X5,X7)|ppt(X5,X6,X7))|~pt(X5,X6,X7)))&((present(X6,X7)|ppt(X5,X6,X7))|~pt(X5,X6,X7)))&((~ppt(X8,X9,X10)|pt(X8,X9,X10))&(((X8!=X9|~present(X8,X10))|~present(X9,X10))|pt(X8,X9,X10))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])). cnf(c_0_14, negated_conjecture, (esk17_0=esk19_0|present(esk17_0,X1)|~occ(esk19_0,X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_11])). cnf(c_0_15, plain, (occ(X1,esk16_2(X1,X2),X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])). cnf(c_0_16, plain, (pt(X1,X2,X3)|~present(X2,X3)|~present(X1,X3)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_13])). cnf(c_0_17, negated_conjecture, (esk17_0=esk19_0|present(esk17_0,X1)|~phtxt(esk19_0,X1)), inference(spm,[status(thm)],[c_0_14, c_0_15])). cnf(c_0_18, negated_conjecture, (phtxt(esk19_0,esk20_0)), inference(split_conjunct,[status(thm)],[c_0_9])). fof(c_0_19, plain, (![X5]:![X6]:![X7]:![X8]:![X9]:![X10]:((((pt(X5,X6,X7)|~phpt(X5,X6,X7))&(phtxt(X5,X7)|~phpt(X5,X6,X7)))&(phtxt(X6,X7)|~phpt(X5,X6,X7)))&(((~pt(X8,X9,X10)|~phtxt(X8,X10))|~phtxt(X9,X10))|phpt(X8,X9,X10)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])). cnf(c_0_20, plain, (pt(X1,X1,X2)|~present(X1,X2)), inference(er,[status(thm)],[c_0_16])). cnf(c_0_21, negated_conjecture, (esk17_0=esk19_0|present(esk17_0,esk20_0)), inference(spm,[status(thm)],[c_0_17, c_0_18])). fof(c_0_22, plain, (![X4]:![X5]:![X6]:(~phtxt(X4,X5)|(~present(X4,X6)|phtxt(X4,X6)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])). fof(c_0_23, plain, (![X9]:![X10]:![X11]:![X12]:((~occ(X9,X10,X11)|~occ(X12,X10,X11))|((~phtxt(X9,X11)|~phtxt(X12,X11))|X9=X12))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])). cnf(c_0_24, plain, (phpt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_19])). cnf(c_0_25, negated_conjecture, (esk17_0=esk19_0|pt(esk17_0,esk17_0,esk20_0)), inference(spm,[status(thm)],[c_0_20, c_0_21])). cnf(c_0_26, plain, (phtxt(X1,X2)|~present(X1,X2)|~phtxt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_22])). cnf(c_0_27, negated_conjecture, (phtxt(esk17_0,esk18_0)), inference(split_conjunct,[status(thm)],[c_0_9])). cnf(c_0_28, plain, (X1=X2|~phtxt(X2,X3)|~phtxt(X1,X3)|~occ(X2,X4,X3)|~occ(X1,X4,X3)), inference(split_conjunct,[status(thm)],[c_0_23])). cnf(c_0_29, negated_conjecture, (esk17_0=esk19_0|occ(esk19_0,X1,X2)|~occ(esk17_0,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_9])). cnf(c_0_30, negated_conjecture, (esk17_0=esk19_0|phpt(esk17_0,esk17_0,esk20_0)|~phtxt(esk17_0,esk20_0)), inference(spm,[status(thm)],[c_0_24, c_0_25])). cnf(c_0_31, negated_conjecture, (phtxt(esk17_0,X1)|~present(esk17_0,X1)), inference(spm,[status(thm)],[c_0_26, c_0_27])). cnf(c_0_32, plain, (X1=X2|~occ(X1,esk16_2(X2,X3),X3)|~phtxt(X2,X3)|~phtxt(X1,X3)), inference(spm,[status(thm)],[c_0_28, c_0_15])). cnf(c_0_33, negated_conjecture, (esk17_0=esk19_0|occ(esk19_0,esk16_2(esk17_0,X1),X1)|~phtxt(esk17_0,X1)), inference(spm,[status(thm)],[c_0_29, c_0_15])). cnf(c_0_34, plain, (phtxt(X2,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_19])). cnf(c_0_35, negated_conjecture, (esk17_0=esk19_0|phpt(esk17_0,esk17_0,esk20_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_21])). cnf(c_0_36, negated_conjecture, (esk17_0=esk19_0|~phtxt(esk17_0,X1)|~phtxt(esk19_0,X1)), inference(spm,[status(thm)],[c_0_32, c_0_33])). cnf(c_0_37, negated_conjecture, (esk17_0=esk19_0|phtxt(esk17_0,esk20_0)), inference(spm,[status(thm)],[c_0_34, c_0_35])). cnf(c_0_38, negated_conjecture, (occ(esk19_0,esk21_0,esk22_0)|occ(esk17_0,esk21_0,esk22_0)|esk17_0!=esk19_0), inference(split_conjunct,[status(thm)],[c_0_9])). cnf(c_0_39, negated_conjecture, (esk17_0=esk19_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_18])])). cnf(c_0_40, negated_conjecture, (esk17_0!=esk19_0|~occ(esk19_0,esk21_0,esk22_0)|~occ(esk17_0,esk21_0,esk22_0)), inference(split_conjunct,[status(thm)],[c_0_9])). cnf(c_0_41, negated_conjecture, (occ(esk19_0,esk21_0,esk22_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39]), c_0_39])])). cnf(c_0_42, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_39]), c_0_39])]), c_0_41])]), ['proof']). # SZS output end CNFRefutation # Training examples: 0 positive, 0 negative # ------------------------------------------------- # User time : 0.036 s # System time : 0.006 s # Total time : 0.041 s # Maximum resident set size: 1768 pages % END OF SYSTEM OUTPUT % RESULT: SOT_KJVp6v - E---1.9.1 says Theorem - CPU = 0.00 WC = 0.04 % OUTPUT: SOT_KJVp6v - E---1.9.1 says CNFRefutation - CPU = 0.00 WC = 0.04