% 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.017 s # Presaturation interreduction done # Proof found! # SZS status Theorem # SZS output start CNFRefutation fof(c_0_0, axiom, (![X1]:![X17]:![X18]:((txtdep(X1,X17)&txtdep(X1,X18))=>![X3]:![X13]:((present(X17,X3)&present(X18,X13))=>phtxtequiv(X17,X3,X18,X13)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom59)). fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(txtrep(X1,X4,X2)<=>?[X15]:(txtdep(X1,X15)&phrep(X15,X4,X2)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiomLXXIII)). fof(c_0_2, axiom, (![X15]:![X3]:![X16]:![X13]:![X4]:(phtxtequiv(X15,X3,X16,X13)=>(phrep(X15,X4,X3)<=>phrep(X16,X4,X13)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom55)). fof(c_0_3, axiom, (![X1]:![X2]:![X4]:![X3]:(phtxtequiv(X1,X2,X4,X3)=>(present(X1,X2)&present(X4,X3)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom48)). fof(c_0_4, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>phtxtequiv(X1,X2,X1,X2))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom49)). fof(c_0_5, axiom, (![X1]:![X4]:![X2]:(phrep(X1,X4,X2)=>phtxt(X1,X2))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom45)). fof(c_0_6, conjecture, (![X1]:![X2]:![X1]:(?[X4]:txtrep(X1,X4,X2)=>![X2]:(present(X1,X2)=>?[X4]:txtrep(X1,X4,X2)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', conjectureXLVI)). fof(c_0_7, axiom, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(phtxt(X4,X2)&txtdep(X1,X4)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom58)). fof(c_0_8, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom3)). fof(c_0_9, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply57506/SOT_3DW69P', axiom56)). fof(c_0_10, plain, (![X19]:![X20]:![X21]:![X22]:![X23]:((~txtdep(X19,X20)|~txtdep(X19,X21))|((~present(X20,X22)|~present(X21,X23))|phtxtequiv(X20,X22,X21,X23)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_0])])])). fof(c_0_11, plain, (![X16]:![X17]:![X18]:![X20]:![X21]:![X22]:![X23]:(((txtdep(X16,esk42_3(X16,X17,X18))|~txtrep(X16,X17,X18))&(phrep(esk42_3(X16,X17,X18),X17,X18)|~txtrep(X16,X17,X18)))&((~txtdep(X20,X23)|~phrep(X23,X21,X22))|txtrep(X20,X21,X22)))), 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_1])])])])])])). fof(c_0_12, plain, (![X17]:![X18]:![X19]:![X20]:![X21]:![X22]:(((~phrep(X17,X21,X18)|phrep(X19,X21,X20))|~phtxtequiv(X17,X18,X19,X20))&((~phrep(X19,X22,X20)|phrep(X17,X22,X18))|~phtxtequiv(X17,X18,X19,X20)))), 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_2])])])])])). cnf(c_0_13, plain, (phtxtequiv(X1,X2,X3,X4)|~present(X3,X4)|~present(X1,X2)|~txtdep(X5,X3)|~txtdep(X5,X1)), inference(split_conjunct,[status(thm)],[c_0_10])). cnf(c_0_14, plain, (txtdep(X1,esk42_3(X1,X2,X3))|~txtrep(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])). cnf(c_0_15, plain, (phrep(X1,X5,X2)|~phtxtequiv(X1,X2,X3,X4)|~phrep(X3,X5,X4)), inference(split_conjunct,[status(thm)],[c_0_12])). cnf(c_0_16, plain, (phtxtequiv(X1,X2,esk42_3(X3,X4,X5),X6)|~txtrep(X3,X4,X5)|~txtdep(X3,X1)|~present(esk42_3(X3,X4,X5),X6)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_13, c_0_14])). fof(c_0_17, 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_3])])])). fof(c_0_18, plain, (![X3]:![X4]:(~phtxt(X3,X4)|phtxtequiv(X3,X4,X3,X4))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])). fof(c_0_19, plain, (![X5]:![X6]:![X7]:(~phrep(X5,X6,X7)|phtxt(X5,X7))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])). cnf(c_0_20, plain, (phrep(X1,X2,X3)|~txtrep(X4,X5,X6)|~txtdep(X4,X1)|~phrep(esk42_3(X4,X5,X6),X2,X7)|~present(esk42_3(X4,X5,X6),X7)|~present(X1,X3)), inference(spm,[status(thm)],[c_0_15, c_0_16])). cnf(c_0_21, plain, (phrep(esk42_3(X1,X2,X3),X2,X3)|~txtrep(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])). cnf(c_0_22, plain, (present(X1,X2)|~phtxtequiv(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_17])). cnf(c_0_23, plain, (phtxtequiv(X1,X2,X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_18])). cnf(c_0_24, plain, (phtxt(X1,X2)|~phrep(X1,X3,X2)), inference(split_conjunct,[status(thm)],[c_0_19])). fof(c_0_25, negated_conjecture, (~(![X2]:![X1]:(?[X4]:txtrep(X1,X4,X2)=>![X2]:(present(X1,X2)=>?[X4]:txtrep(X1,X4,X2))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_6])])). cnf(c_0_26, plain, (phrep(X1,X2,X3)|~txtrep(X4,X2,X5)|~txtdep(X4,X1)|~present(esk42_3(X4,X2,X5),X5)|~present(X1,X3)), inference(spm,[status(thm)],[c_0_20, c_0_21])). cnf(c_0_27, plain, (present(X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_22, c_0_23])). cnf(c_0_28, plain, (phtxt(esk42_3(X1,X2,X3),X3)|~txtrep(X1,X2,X3)), inference(spm,[status(thm)],[c_0_24, c_0_21])). fof(c_0_29, negated_conjecture, (![X9]:(txtrep(esk48_0,esk49_0,esk47_0)&(present(esk48_0,esk50_0)&~txtrep(esk48_0,X9,esk50_0)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])])). cnf(c_0_30, plain, (phrep(X1,X2,X3)|~txtrep(X4,X2,X5)|~txtdep(X4,X1)|~present(X1,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_28])). cnf(c_0_31, negated_conjecture, (txtrep(esk48_0,esk49_0,esk47_0)), inference(split_conjunct,[status(thm)],[c_0_29])). cnf(c_0_32, plain, (txtrep(X1,X2,X3)|~phrep(X4,X2,X3)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_11])). cnf(c_0_33, negated_conjecture, (phrep(X1,esk49_0,X2)|~txtdep(esk48_0,X1)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_30, c_0_31])). fof(c_0_34, 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_7])])])])). cnf(c_0_35, negated_conjecture, (txtrep(X1,esk49_0,X2)|~txtdep(esk48_0,X3)|~txtdep(X1,X3)|~present(X3,X2)), inference(spm,[status(thm)],[c_0_32, c_0_33])). cnf(c_0_36, plain, (txtdep(X1,esk31_2(X1,X2))|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_34])). cnf(c_0_37, negated_conjecture, (txtrep(X1,esk49_0,X2)|~txtdep(esk48_0,esk31_2(X1,X3))|~txt(X1,X3)|~present(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_35, c_0_36])). fof(c_0_38, plain, (![X4]:![X5]:![X6]:(~txt(X4,X5)|(~present(X4,X6)|txt(X4,X6)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])). fof(c_0_39, 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_9])])])])). cnf(c_0_40, negated_conjecture, (txtrep(X1,esk49_0,X2)|~txtdep(esk48_0,esk31_2(X1,X3))|~txt(X1,X3)|~phtxt(esk31_2(X1,X3),X2)), inference(spm,[status(thm)],[c_0_37, c_0_27])). cnf(c_0_41, plain, (phtxt(esk31_2(X1,X2),X2)|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_34])). cnf(c_0_42, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_43, plain, (txt(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_39])). cnf(c_0_44, negated_conjecture, (txtrep(X1,esk49_0,X2)|~txtdep(esk48_0,esk31_2(X1,X2))|~txt(X1,X2)), inference(spm,[status(thm)],[c_0_40, c_0_41])). cnf(c_0_45, plain, (txt(X1,X2)|~txtdep(X1,X3)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_42, c_0_43])). cnf(c_0_46, negated_conjecture, (~txtrep(esk48_0,X1,esk50_0)), inference(split_conjunct,[status(thm)],[c_0_29])). cnf(c_0_47, negated_conjecture, (txtrep(esk48_0,esk49_0,X1)|~txt(esk48_0,X1)), inference(spm,[status(thm)],[c_0_44, c_0_36])). cnf(c_0_48, plain, (txt(X1,X2)|~txtrep(X1,X3,X4)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_45, c_0_14])). cnf(c_0_49, negated_conjecture, (~txt(esk48_0,esk50_0)), inference(spm,[status(thm)],[c_0_46, c_0_47])). cnf(c_0_50, negated_conjecture, (txt(esk48_0,X1)|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_48, c_0_31])). cnf(c_0_51, negated_conjecture, (present(esk48_0,esk50_0)), inference(split_conjunct,[status(thm)],[c_0_29])). cnf(c_0_52, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_50]), c_0_51])]), ['proof']). # SZS output end CNFRefutation # Training examples: 0 positive, 0 negative # ------------------------------------------------- # User time : 2.655 s # System time : 0.050 s # Total time : 2.705 s # Maximum resident set size: 1856 pages % END OF SYSTEM OUTPUT % RESULT: SOT_3DW69P - E---1.9.1 says Theorem - CPU = 2.67 WC = 2.70 % OUTPUT: SOT_3DW69P - E---1.9.1 says CNFRefutation - CPU = 2.67 WC = 2.70