% 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 % 10 wall clock seconds gone, waiting for system output % 20 wall clock seconds gone, waiting for system output % 30 wall clock seconds gone, waiting for system output % 40 wall clock seconds gone, waiting for system output % 50 wall clock seconds gone, waiting for system output % 60 wall clock seconds gone, waiting for system output % 70 wall clock seconds gone, waiting for system output % 80 wall clock seconds gone, waiting for system output % 90 wall clock seconds gone, waiting for system output % 100 wall clock seconds gone, waiting for system output % 110 wall clock seconds gone, waiting for system output % 120 wall clock seconds gone, waiting for system output # AutoSched0-Mode selected heuristic G_E___107_C36_F1_PI_AE_Q4_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Preprocessing time : 0.024 s # Presaturation interreduction done # No success with AutoSched0 # Trying AutoSched1 for 58 seconds % 130 wall clock seconds gone, waiting for system output % 140 wall clock seconds gone, waiting for system output % 150 wall clock seconds gone, waiting for system output % 160 wall clock seconds gone, waiting for system output % 170 wall clock seconds gone, waiting for system output # AutoSched1-Mode selected heuristic G_E___208_C18_F1_AE_CS_SP_PS_S3S # and selection function SelectNewComplexAHPExceptUniqMaxHorn. # # Preprocessing time : 0.018 s # Presaturation interreduction done # No success with AutoSched1 # Trying AutoSched2 for 19 seconds % 180 wall clock seconds gone, waiting for system output % 190 wall clock seconds gone, waiting for system output # AutoSched2-Mode selected heuristic G_E___208_B07_F1_SE_CS_SP_PS_S2q # and selection function SelectCQArNTNp. # # Preprocessing time : 0.021 s # Presaturation interreduction done # No success with AutoSched2 # Trying AutoSched3 for 14 seconds % 200 wall clock seconds gone, waiting for system output % 210 wall clock seconds gone, waiting for system output # AutoSched3-Mode selected heuristic G_E___300_C18_F1_SE_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Preprocessing time : 0.022 s # Presaturation interreduction done # No success with AutoSched3 # Trying AutoSched4 for 10 seconds # AutoSched4-Mode selected heuristic G_E___060_C18_F1_PI_SE_CS_SP_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Preprocessing time : 0.019 s # Proof found! # SZS status Theorem # SZS output start CNFRefutation fof(c_0_0, axiom, (![X1]:![X4]:![X2]:(phpt(X1,X4,X2)<=>((pt(X1,X4,X2)&phtxt(X1,X2))&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', definition18)). fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', definition4)). fof(c_0_2, axiom, (![X7]:![X8]:![X2]:(occ(X7,X8,X2)=>(present(X7,X2)&present(X8,X2)))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', axiom13)). fof(c_0_3, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>?[X8]:occ(X1,X8,X2))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', axiom28)). fof(c_0_4, axiom, (![X1]:![X4]:![X2]:(phppt(X1,X4,X2)<=>((ppt(X1,X4,X2)&phtxt(X1,X2))&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', definition17)). fof(c_0_5, axiom, (![X1]:![X4]:![X2]:(phoverlap(X1,X4,X2)<=>?[X5]:(phpt(X5,X1,X2)&phpt(X5,X4,X2)))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', definition19)). fof(c_0_6, axiom, (![X1]:![X2]:![X4]:((phtxt(X1,X2)&phtxt(X4,X2))=>(~(phpt(X1,X4,X2))=>?[X5]:(phpt(X5,X1,X2)&~(phoverlap(X5,X4,X2)))))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', axiom23)). fof(c_0_7, conjecture, (![X1]:![X2]:![X4]:![X1]:![X4]:(?[X5]:(phppt(X5,X1,X2)|phppt(X5,X4,X2))=>(X1=X4<=>![X5]:![X2]:(phppt(X5,X1,X2)<=>phppt(X5,X4,X2))))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', conjecture43)). fof(c_0_8, axiom, (![X1]:![X4]:![X2]:(phppt(X1,X4,X2)=>?[X5]:(phppt(X5,X4,X2)&~(?[X6]:(phppt(X5,X6,X2)&phppt(X6,X4,X2)))))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', axiom26)). fof(c_0_9, axiom, (![X1]:![X2]:~(ppt(X1,X1,X2))), file('/tmp/SystemOnTPTPFormReply60149/SOT_I9kVU9', axiom8)). fof(c_0_10, 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_0])])])])])). fof(c_0_11, 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_1])])])])])). fof(c_0_12, 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_2])])])). fof(c_0_13, 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_3])])])). cnf(c_0_14, plain, (phpt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])). cnf(c_0_15, plain, (pt(X1,X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])). fof(c_0_16, plain, (![X5]:![X6]:![X7]:![X8]:![X9]:![X10]:((((ppt(X5,X6,X7)|~phppt(X5,X6,X7))&(phtxt(X5,X7)|~phppt(X5,X6,X7)))&(phtxt(X6,X7)|~phppt(X5,X6,X7)))&(((~ppt(X8,X9,X10)|~phtxt(X8,X10))|~phtxt(X9,X10))|phppt(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_17, plain, (pt(X1,X2,X3)|~present(X2,X3)|~present(X1,X3)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_11])). cnf(c_0_18, plain, (present(X1,X3)|~occ(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_12])). cnf(c_0_19, plain, (occ(X1,esk16_2(X1,X2),X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])). fof(c_0_20, plain, (![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X13]:(((phpt(esk8_3(X6,X7,X8),X6,X8)|~phoverlap(X6,X7,X8))&(phpt(esk8_3(X6,X7,X8),X7,X8)|~phoverlap(X6,X7,X8)))&((~phpt(X13,X10,X12)|~phpt(X13,X11,X12))|phoverlap(X10,X11,X12)))), 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_5])])])])])])). cnf(c_0_21, plain, (phpt(X1,X2,X3)|~ppt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)), inference(spm,[status(thm)],[c_0_14, c_0_15])). cnf(c_0_22, plain, (ppt(X1,X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])). cnf(c_0_23, plain, (phtxt(X1,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])). cnf(c_0_24, plain, (phtxt(X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])). cnf(c_0_25, plain, (pt(X1,X1,X2)|~present(X1,X2)), inference(er,[status(thm)],[c_0_17])). cnf(c_0_26, plain, (present(X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_18, c_0_19])). fof(c_0_27, plain, (![X1]:![X2]:![X4]:((phtxt(X1,X2)&phtxt(X4,X2))=>(~phpt(X1,X4,X2)=>?[X5]:(phpt(X5,X1,X2)&~phoverlap(X5,X4,X2))))), inference(fof_simplification,[status(thm)],[c_0_6])). cnf(c_0_28, plain, (phoverlap(X1,X2,X3)|~phpt(X4,X2,X3)|~phpt(X4,X1,X3)), inference(split_conjunct,[status(thm)],[c_0_20])). cnf(c_0_29, plain, (phpt(X1,X2,X3)|~phppt(X1,X2,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23]), c_0_24])). cnf(c_0_30, plain, (pt(X1,X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_25, c_0_26])). fof(c_0_31, negated_conjecture, (~(![X2]:![X1]:![X4]:(?[X5]:(phppt(X5,X1,X2)|phppt(X5,X4,X2))=>(X1=X4<=>![X5]:![X2]:(phppt(X5,X1,X2)<=>phppt(X5,X4,X2)))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_7])])). fof(c_0_32, plain, (![X6]:![X7]:![X8]:(((phpt(esk10_3(X6,X7,X8),X6,X7)|phpt(X6,X8,X7))|(~phtxt(X6,X7)|~phtxt(X8,X7)))&((~phoverlap(esk10_3(X6,X7,X8),X8,X7)|phpt(X6,X8,X7))|(~phtxt(X6,X7)|~phtxt(X8,X7))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])])). cnf(c_0_33, plain, (phoverlap(X1,X2,X3)|~phpt(X4,X1,X3)|~phppt(X4,X2,X3)), inference(spm,[status(thm)],[c_0_28, c_0_29])). cnf(c_0_34, plain, (phpt(X1,X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_14, c_0_30])). cnf(c_0_35, plain, (ppt(X1,X2,X3)|X1=X2|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])). cnf(c_0_36, plain, (pt(X1,X2,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])). fof(c_0_37, plain, (![X7]:![X8]:![X9]:![X11]:((phppt(esk13_3(X7,X8,X9),X8,X9)|~phppt(X7,X8,X9))&((~phppt(esk13_3(X7,X8,X9),X11,X9)|~phppt(X11,X8,X9))|~phppt(X7,X8,X9)))), 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_8])])])])])). fof(c_0_38, negated_conjecture, (![X13]:![X14]:![X15]:![X16]:((phppt(esk20_0,esk18_0,esk17_0)|phppt(esk21_0,esk19_0,esk17_0))&((((~phppt(esk22_0,esk18_0,esk23_0)|~phppt(esk22_0,esk19_0,esk23_0))|esk18_0!=esk19_0)&((phppt(esk22_0,esk18_0,esk23_0)|phppt(esk22_0,esk19_0,esk23_0))|esk18_0!=esk19_0))&(((~phppt(X13,esk18_0,X14)|phppt(X13,esk19_0,X14))|esk18_0=esk19_0)&((~phppt(X15,esk19_0,X16)|phppt(X15,esk18_0,X16))|esk18_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_31])])])])])])). cnf(c_0_39, plain, (phpt(X3,X1,X2)|~phtxt(X1,X2)|~phtxt(X3,X2)|~phoverlap(esk10_3(X3,X2,X1),X1,X2)), inference(split_conjunct,[status(thm)],[c_0_32])). cnf(c_0_40, plain, (phoverlap(X1,X2,X3)|~phppt(X1,X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_23])). cnf(c_0_41, plain, (phppt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])). cnf(c_0_42, plain, (X1=X2|ppt(X1,X2,X3)|~phpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_35, c_0_36])). cnf(c_0_43, plain, (phtxt(X1,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])). cnf(c_0_44, plain, (phtxt(X2,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])). cnf(c_0_45, plain, (phoverlap(X1,X2,X3)|~phppt(X4,X2,X3)|~phppt(X4,X1,X3)), inference(spm,[status(thm)],[c_0_33, c_0_29])). cnf(c_0_46, plain, (phppt(esk13_3(X1,X2,X3),X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_37])). cnf(c_0_47, negated_conjecture, (esk18_0=esk19_0|phppt(X1,esk18_0,X2)|~phppt(X1,esk19_0,X2)), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_48, plain, (phpt(X1,X2,X3)|~phppt(esk10_3(X1,X3,X2),X2,X3)|~phtxt(X1,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_24])). cnf(c_0_49, negated_conjecture, (esk18_0=esk19_0|phppt(X1,esk19_0,X2)|~phppt(X1,esk18_0,X2)), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_50, plain, (X1=X2|phppt(X1,X2,X3)|~phpt(X1,X2,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43]), c_0_44])). cnf(c_0_51, plain, (phpt(X3,X1,X2)|phpt(esk10_3(X3,X2,X1),X3,X2)|~phtxt(X1,X2)|~phtxt(X3,X2)), inference(split_conjunct,[status(thm)],[c_0_32])). cnf(c_0_52, plain, (phoverlap(X1,X2,X3)|~phppt(esk13_3(X4,X2,X3),X1,X3)|~phppt(X4,X2,X3)), inference(spm,[status(thm)],[c_0_45, c_0_46])). cnf(c_0_53, negated_conjecture, (esk19_0=esk18_0|phppt(esk13_3(X1,esk19_0,X2),esk18_0,X2)|~phppt(X1,esk19_0,X2)), inference(spm,[status(thm)],[c_0_47, c_0_46])). cnf(c_0_54, negated_conjecture, (esk19_0=esk18_0|phpt(X1,esk19_0,X2)|~phppt(esk10_3(X1,X2,esk19_0),esk18_0,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_48, c_0_49])). cnf(c_0_55, plain, (esk10_3(X1,X2,X3)=X1|phpt(X1,X3,X2)|phppt(esk10_3(X1,X2,X3),X1,X2)|~phtxt(X1,X2)|~phtxt(X3,X2)), inference(spm,[status(thm)],[c_0_50, c_0_51])). cnf(c_0_56, plain, (phpt(esk8_3(X1,X2,X3),X2,X3)|~phoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_20])). cnf(c_0_57, plain, (phpt(esk8_3(X1,X2,X3),X1,X3)|~phoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_20])). cnf(c_0_58, negated_conjecture, (esk19_0=esk18_0|phoverlap(esk18_0,esk19_0,X1)|~phppt(X2,esk19_0,X1)), inference(spm,[status(thm)],[c_0_52, c_0_53])). cnf(c_0_59, negated_conjecture, (esk10_3(esk18_0,X1,esk19_0)=esk18_0|esk19_0=esk18_0|phpt(esk18_0,esk19_0,X1)|~phtxt(esk18_0,X1)|~phtxt(esk19_0,X1)), inference(spm,[status(thm)],[c_0_54, c_0_55])). cnf(c_0_60, plain, (phtxt(X1,X2)|~phoverlap(X3,X1,X2)), inference(spm,[status(thm)],[c_0_44, c_0_56])). cnf(c_0_61, plain, (phtxt(X1,X2)|~phoverlap(X1,X3,X2)), inference(spm,[status(thm)],[c_0_44, c_0_57])). cnf(c_0_62, negated_conjecture, (phppt(esk21_0,esk19_0,esk17_0)|phppt(esk20_0,esk18_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_63, negated_conjecture, (esk19_0=esk18_0|phoverlap(esk18_0,esk19_0,X1)|~phppt(X2,esk18_0,X1)), inference(spm,[status(thm)],[c_0_58, c_0_49])). fof(c_0_64, plain, (![X1]:![X2]:~ppt(X1,X1,X2)), inference(fof_simplification,[status(thm)],[c_0_9])). cnf(c_0_65, negated_conjecture, (esk19_0=esk18_0|phpt(esk18_0,esk19_0,X1)|~phoverlap(esk18_0,esk19_0,X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_59]), c_0_60]), c_0_61])). cnf(c_0_66, negated_conjecture, (esk19_0=esk18_0|phoverlap(esk18_0,esk19_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_62]), c_0_63])). fof(c_0_67, plain, (![X3]:![X4]:~ppt(X3,X3,X4)), inference(variable_rename,[status(thm)],[c_0_64])). cnf(c_0_68, negated_conjecture, (esk19_0=esk18_0|phpt(esk18_0,esk19_0,esk17_0)), inference(spm,[status(thm)],[c_0_65, c_0_66])). cnf(c_0_69, plain, (~ppt(X1,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_67])). cnf(c_0_70, negated_conjecture, (esk19_0=esk18_0|phppt(esk18_0,esk19_0,esk17_0)), inference(spm,[status(thm)],[c_0_50, c_0_68])). cnf(c_0_71, plain, (~phppt(X1,X1,X2)), inference(spm,[status(thm)],[c_0_69, c_0_22])). cnf(c_0_72, negated_conjecture, (esk18_0!=esk19_0|~phppt(esk22_0,esk19_0,esk23_0)|~phppt(esk22_0,esk18_0,esk23_0)), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_73, negated_conjecture, (esk19_0=esk18_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_70]), c_0_71])). cnf(c_0_74, negated_conjecture, (phppt(esk22_0,esk19_0,esk23_0)|phppt(esk22_0,esk18_0,esk23_0)|esk18_0!=esk19_0), inference(split_conjunct,[status(thm)],[c_0_38])). cnf(c_0_75, negated_conjecture, (~phppt(esk22_0,esk18_0,esk23_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73]), c_0_73])])). cnf(c_0_76, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_73]), c_0_73])]), c_0_75]), ['proof']). # SZS output end CNFRefutation # Training examples: 0 positive, 0 negative # ------------------------------------------------- # User time : 214.478 s # System time : 1.568 s # Total time : 216.046 s # Maximum resident set size: 1768 pages % END OF SYSTEM OUTPUT % RESULT: SOT_I9kVU9 - E---1.9.1 says Theorem - CPU = 216.01 WC = 216.10 % OUTPUT: SOT_I9kVU9 - E---1.9.1 says CNFRefutation - CPU = 216.01 WC = 216.10