% 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___208_C18_F1_SE_CS_SP_PS_S0YP # and selection function SelectMaxLComplexAvoidPosPred. # # Preprocessing time : 0.028 s # Presaturation interreduction done # Proof found! # SZS status Theorem # SZS output start CNFRefutation fof(c_0_0, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>![X2]:(present(X4,X2)=>present(X1,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom61)). fof(c_0_1, axiom, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(phtxt(X4,X2)&txtdep(X1,X4)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom58)). fof(c_0_2, axiom, (![X1]:![X2]:![X4]:![X3]:(phtxtequiv(X1,X2,X4,X3)=>(present(X1,X2)&present(X4,X3)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom48)). fof(c_0_3, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>phtxtequiv(X1,X2,X1,X2))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom49)). fof(c_0_4, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', definition4)). fof(c_0_5, axiom, (![X15]:![X17]:![X16]:![X18]:![X2]:((txtdep(X15,X17)&txtdep(X16,X18))=>(phtxtprec(X15,X16,X2)<=>phtxtprec(X17,X18,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom64)). fof(c_0_6, axiom, (![X1]:![X4]:![X2]:(txtprec(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&phtxtprec(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiomLXXII)). fof(c_0_7, axiom, (![X1]:![X4]:![X2]:(txtpt(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&pt(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiomLXX)). fof(c_0_8, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom56)). fof(c_0_9, axiom, (![X2]:~(?[X1]:(phtxt(X1,X2)&txt(X1,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom66)). fof(c_0_10, conjecture, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(txtpt(X4,X1,X2)&![X5]:(txtpt(X5,X1,X2)=>~(txtprec(X4,X5,X2)))))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', conjectureXL)). fof(c_0_11, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X3]:(present(X1,X3)=>phtxt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom2)). fof(c_0_12, axiom, (![X1]:![X4]:![X2]:(phtxtprec(X1,X4,X2)=>(phtxt(X1,X2)&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56621/SOT_srRpCZ', axiom30)). fof(c_0_13, plain, (![X5]:![X6]:![X7]:(~txtdep(X5,X6)|(~present(X6,X7)|present(X5,X7)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_0])])])). fof(c_0_14, plain, (![X5]:![X6]:((phtxt(esk31_2(X5,X6),X6)|~txt(X5,X6))&(txtdep(X5,esk31_2(X5,X6))|~txt(X5,X6)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])])). fof(c_0_15, plain, (![X5]:![X6]:![X7]:![X8]:((present(X5,X6)|~phtxtequiv(X5,X6,X7,X8))&(present(X7,X8)|~phtxtequiv(X5,X6,X7,X8)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])). fof(c_0_16, plain, (![X3]:![X4]:(~phtxt(X3,X4)|phtxtequiv(X3,X4,X3,X4))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])). cnf(c_0_17, plain, (present(X1,X2)|~present(X3,X2)|~txtdep(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_13])). cnf(c_0_18, plain, (txtdep(X1,esk31_2(X1,X2))|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_14])). cnf(c_0_19, plain, (present(X1,X2)|~phtxtequiv(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_15])). cnf(c_0_20, plain, (phtxtequiv(X1,X2,X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_16])). fof(c_0_21, 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_4])])])])])). fof(c_0_22, plain, (![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:(((~phtxtprec(X19,X21,X23)|phtxtprec(X20,X22,X23))|(~txtdep(X19,X20)|~txtdep(X21,X22)))&((~phtxtprec(X20,X22,X24)|phtxtprec(X19,X21,X24))|(~txtdep(X19,X20)|~txtdep(X21,X22))))), 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_5])])])])])). fof(c_0_23, plain, (![X18]:![X19]:![X20]:![X23]:![X24]:![X25]:![X26]:![X27]:((((txtdep(X18,esk40_3(X18,X19,X20))|~txtprec(X18,X19,X20))&(txtdep(X19,esk41_3(X18,X19,X20))|~txtprec(X18,X19,X20)))&(phtxtprec(esk40_3(X18,X19,X20),esk41_3(X18,X19,X20),X20)|~txtprec(X18,X19,X20)))&(((~txtdep(X23,X26)|~txtdep(X24,X27))|~phtxtprec(X26,X27,X25))|txtprec(X23,X24,X25)))), 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_6])])])])])])). cnf(c_0_24, plain, (present(X1,X2)|~txt(X1,X3)|~present(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_17, c_0_18])). cnf(c_0_25, plain, (present(X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_19, c_0_20])). fof(c_0_26, plain, (![X18]:![X19]:![X20]:![X23]:![X24]:![X25]:![X26]:![X27]:((((txtdep(X18,esk36_3(X18,X19,X20))|~txtpt(X18,X19,X20))&(txtdep(X19,esk37_3(X18,X19,X20))|~txtpt(X18,X19,X20)))&(pt(esk36_3(X18,X19,X20),esk37_3(X18,X19,X20),X20)|~txtpt(X18,X19,X20)))&(((~txtdep(X23,X26)|~txtdep(X24,X27))|~pt(X26,X27,X25))|txtpt(X23,X24,X25)))), 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_27, plain, (pt(X1,X2,X3)|~present(X2,X3)|~present(X1,X3)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_21])). cnf(c_0_28, plain, (phtxtprec(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~phtxtprec(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_22])). cnf(c_0_29, plain, (phtxtprec(esk40_3(X1,X2,X3),esk41_3(X1,X2,X3),X3)|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_23])). cnf(c_0_30, plain, (present(X1,X2)|~txt(X1,X3)|~phtxt(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_24, c_0_25])). cnf(c_0_31, plain, (phtxt(esk31_2(X1,X2),X2)|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_14])). fof(c_0_32, plain, (![X5]:![X6]:((txt(X5,esk28_2(X5,X6))|~txtdep(X5,X6))&(phtxt(X6,esk29_2(X5,X6))|~txtdep(X5,X6)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])). fof(c_0_33, plain, (![X3]:![X4]:(~phtxt(X4,X3)|~txt(X4,X3))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])). cnf(c_0_34, plain, (txtpt(X1,X2,X3)|~pt(X4,X5,X3)|~txtdep(X2,X5)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_26])). cnf(c_0_35, plain, (pt(X1,X1,X2)|~present(X1,X2)), inference(er,[status(thm)],[c_0_27])). cnf(c_0_36, plain, (phtxtprec(X1,X2,X3)|~txtprec(X4,X5,X3)|~txtdep(X1,esk40_3(X4,X5,X3))|~txtdep(X2,esk41_3(X4,X5,X3))), inference(spm,[status(thm)],[c_0_28, c_0_29])). cnf(c_0_37, plain, (txtdep(X1,esk40_3(X1,X2,X3))|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_23])). fof(c_0_38, negated_conjecture, (~(![X1]:![X2]:(txt(X1,X2)=>?[X4]:(txtpt(X4,X1,X2)&![X5]:(txtpt(X5,X1,X2)=>~txtprec(X4,X5,X2)))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_10])])). fof(c_0_39, 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_11])])])])). cnf(c_0_40, plain, (present(X1,X2)|~txt(X1,X2)), inference(spm,[status(thm)],[c_0_30, c_0_31])). cnf(c_0_41, plain, (txt(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_32])). cnf(c_0_42, plain, (~txt(X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_33])). cnf(c_0_43, plain, (txtpt(X1,X2,X3)|~txtdep(X2,X4)|~txtdep(X1,X4)|~present(X4,X3)), inference(spm,[status(thm)],[c_0_34, c_0_35])). cnf(c_0_44, plain, (phtxtprec(X1,X2,X3)|~txtprec(X1,X4,X3)|~txtdep(X2,esk41_3(X1,X4,X3))), inference(spm,[status(thm)],[c_0_36, c_0_37])). cnf(c_0_45, plain, (txtdep(X2,esk41_3(X1,X2,X3))|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_23])). fof(c_0_46, negated_conjecture, (![X8]:(txt(esk47_0,esk48_0)&((txtpt(esk49_1(X8),esk47_0,esk48_0)|~txtpt(X8,esk47_0,esk48_0))&(txtprec(X8,esk49_1(X8),esk48_0)|~txtpt(X8,esk47_0,esk48_0))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_38])])])])])). cnf(c_0_47, plain, (phtxt(X1,X2)|~present(X1,X2)|~phtxt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_39])). cnf(c_0_48, plain, (present(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(spm,[status(thm)],[c_0_40, c_0_41])). cnf(c_0_49, plain, (~txtdep(X1,X2)|~phtxt(X1,esk28_2(X1,X2))), inference(spm,[status(thm)],[c_0_42, c_0_41])). cnf(c_0_50, plain, (txtpt(X1,X2,X3)|~txtdep(X1,esk31_2(X2,X4))|~txt(X2,X4)|~present(esk31_2(X2,X4),X3)), inference(spm,[status(thm)],[c_0_43, c_0_18])). fof(c_0_51, plain, (![X5]:![X6]:![X7]:((phtxt(X5,X7)|~phtxtprec(X5,X6,X7))&(phtxt(X6,X7)|~phtxtprec(X5,X6,X7)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])). cnf(c_0_52, plain, (phtxtprec(X1,X2,X3)|~txtprec(X1,X2,X3)), inference(spm,[status(thm)],[c_0_44, c_0_45])). cnf(c_0_53, negated_conjecture, (txtprec(X1,esk49_1(X1),esk48_0)|~txtpt(X1,esk47_0,esk48_0)), inference(split_conjunct,[status(thm)],[c_0_46])). cnf(c_0_54, plain, (~txtdep(X1,X2)|~phtxt(X1,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_49])). cnf(c_0_55, plain, (txtdep(X1,esk36_3(X1,X2,X3))|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_26])). cnf(c_0_56, plain, (txtpt(X1,X1,X2)|~txt(X1,X3)|~present(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_50, c_0_18])). cnf(c_0_57, plain, (phtxt(X1,X3)|~phtxtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_51])). cnf(c_0_58, negated_conjecture, (phtxtprec(X1,esk49_1(X1),esk48_0)|~txtpt(X1,esk47_0,esk48_0)), inference(spm,[status(thm)],[c_0_52, c_0_53])). cnf(c_0_59, plain, (~txtpt(X1,X2,X3)|~phtxt(X1,X4)), inference(spm,[status(thm)],[c_0_54, c_0_55])). cnf(c_0_60, plain, (txtpt(X1,X1,X2)|~txt(X1,X3)|~phtxt(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_56, c_0_25])). cnf(c_0_61, negated_conjecture, (~txtpt(X1,esk47_0,esk48_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_58]), c_0_59])). cnf(c_0_62, plain, (txtpt(X1,X1,X2)|~txt(X1,X2)), inference(spm,[status(thm)],[c_0_60, c_0_31])). cnf(c_0_63, negated_conjecture, (txt(esk47_0,esk48_0)), inference(split_conjunct,[status(thm)],[c_0_46])). cnf(c_0_64, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63])]), ['proof']). # SZS output end CNFRefutation # Training examples: 0 positive, 0 negative # ------------------------------------------------- # User time : 0.467 s # System time : 0.026 s # Total time : 0.493 s # Maximum resident set size: 1856 pages % END OF SYSTEM OUTPUT % RESULT: SOT_srRpCZ - E---1.9.1 says Theorem - CPU = 0.00 WC = 0.49 % OUTPUT: SOT_srRpCZ - E---1.9.1 says CNFRefutation - CPU = 0.00 WC = 0.49