% 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___212_C18_F1_AE_Q12_CS_SP_S2S
# and selection function SelectNewComplexAHP.
#
# Preprocessing time       : 0.019 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(c_0_0, conjecture, (![X1]:![X4]:![X2]:![X11]:(txtprec(X1,X4,X2)=>![X12]:![X12]:((((((comptxt(X12,X2)&txtpt(X1,X12,X2))&txtpt(X4,X12,X2))&comptxt(X11,X2))&txtpt(X1,X11,X2))&txtpt(X4,X11,X2))=>X12=X11))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', conjectureXXXVIIIb)).
fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(txtpt(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&pt(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiomLXX)).
fof(c_0_2, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', definition4)).
fof(c_0_3, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>(present(X1,X2)&present(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom7)).
fof(c_0_4, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>![X2]:(present(X4,X2)=>present(X1,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom61)).
fof(c_0_5, axiom, (![X1]:![X4]:![X2]:(txtprec(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&phtxtprec(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiomLXXII)).
fof(c_0_6, axiom, (![X15]:![X17]:![X16]:![X18]:![X2]:((txtdep(X15,X17)&txtdep(X16,X18))=>(phtxtprec(X15,X16,X2)<=>phtxtprec(X17,X18,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom64)).
fof(c_0_7, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom3)).
fof(c_0_8, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom56)).
fof(c_0_9, axiom, (![X2]:~(?[X1]:(phtxt(X1,X2)&txt(X1,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom66)).
fof(c_0_10, axiom, (![X1]:![X4]:![X2]:(phtxtprec(X1,X4,X2)=>(phtxt(X1,X2)&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56238/SOT_TKRfMZ', axiom30)).
fof(c_0_11, negated_conjecture, (~(![X1]:![X4]:![X2]:![X11]:(txtprec(X1,X4,X2)=>![X12]:((((((comptxt(X12,X2)&txtpt(X1,X12,X2))&txtpt(X4,X12,X2))&comptxt(X11,X2))&txtpt(X1,X11,X2))&txtpt(X4,X11,X2))=>X12=X11)))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_0])])).
fof(c_0_12, 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_1])])])])])])).
fof(c_0_13, negated_conjecture, ((txtprec(esk47_0,esk48_0,esk49_0)&((((((comptxt(esk51_0,esk49_0)&txtpt(esk47_0,esk51_0,esk49_0))&txtpt(esk48_0,esk51_0,esk49_0))&comptxt(esk50_0,esk49_0))&txtpt(esk47_0,esk50_0,esk49_0))&txtpt(esk48_0,esk50_0,esk49_0))&esk51_0!=esk50_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])])).
fof(c_0_14, 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_2])])])])])).
fof(c_0_15, plain, (![X5]:![X6]:![X7]:((present(X5,X7)|~ppt(X5,X6,X7))&(present(X6,X7)|~ppt(X5,X6,X7)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])).
fof(c_0_16, 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_4])])])).
cnf(c_0_17, plain, (txtdep(X1,esk36_3(X1,X2,X3))|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_12])).
cnf(c_0_18, negated_conjecture, (txtpt(esk48_0,esk51_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_13])).
cnf(c_0_19, plain, (ppt(X1,X2,X3)|present(X1,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_14])).
cnf(c_0_20, plain, (present(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_15])).
cnf(c_0_21, plain, (pt(esk36_3(X1,X2,X3),esk37_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_12])).
fof(c_0_22, 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_5])])])])])])).
cnf(c_0_23, plain, (present(X1,X2)|~present(X3,X2)|~txtdep(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_24, negated_conjecture, (txtdep(esk48_0,esk36_3(esk48_0,esk51_0,esk49_0))), inference(spm,[status(thm)],[c_0_17, c_0_18])).
cnf(c_0_25, plain, (present(X1,X2)|~pt(X1,X3,X2)), inference(csr,[status(thm)],[c_0_19, c_0_20])).
cnf(c_0_26, negated_conjecture, (pt(esk36_3(esk48_0,esk51_0,esk49_0),esk37_3(esk48_0,esk51_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_21, c_0_18])).
fof(c_0_27, 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_6])])])])])).
cnf(c_0_28, plain, (phtxtprec(esk40_3(X1,X2,X3),esk41_3(X1,X2,X3),X3)|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_29, negated_conjecture, (txtprec(esk47_0,esk48_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_13])).
fof(c_0_30, 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_7])])])])).
cnf(c_0_31, negated_conjecture, (present(esk48_0,X1)|~present(esk36_3(esk48_0,esk51_0,esk49_0),X1)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
cnf(c_0_32, negated_conjecture, (present(esk36_3(esk48_0,esk51_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_25, c_0_26])).
fof(c_0_33, 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])])])])).
cnf(c_0_34, plain, (txtdep(X2,esk41_3(X1,X2,X3))|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_35, plain, (phtxtprec(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~phtxtprec(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_27])).
cnf(c_0_36, negated_conjecture, (phtxtprec(esk40_3(esk47_0,esk48_0,esk49_0),esk41_3(esk47_0,esk48_0,esk49_0),esk49_0)), 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_22])).
cnf(c_0_38, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_30])).
cnf(c_0_39, negated_conjecture, (present(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_31, c_0_32])).
cnf(c_0_40, plain, (txt(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_33])).
cnf(c_0_41, negated_conjecture, (txtdep(esk48_0,esk41_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_34, c_0_29])).
cnf(c_0_42, negated_conjecture, (phtxtprec(X1,X2,esk49_0)|~txtdep(X1,esk40_3(esk47_0,esk48_0,esk49_0))|~txtdep(X2,esk41_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
cnf(c_0_43, negated_conjecture, (txtdep(esk47_0,esk40_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_37, c_0_29])).
fof(c_0_44, 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_45, negated_conjecture, (txt(esk48_0,esk49_0)|~txt(esk48_0,X1)), inference(spm,[status(thm)],[c_0_38, c_0_39])).
cnf(c_0_46, negated_conjecture, (txt(esk48_0,esk28_2(esk48_0,esk41_3(esk47_0,esk48_0,esk49_0)))), inference(spm,[status(thm)],[c_0_40, c_0_41])).
fof(c_0_47, 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_10])])])).
cnf(c_0_48, negated_conjecture, (phtxtprec(esk47_0,X1,esk49_0)|~txtdep(X1,esk41_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
cnf(c_0_49, plain, (~txt(X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_44])).
cnf(c_0_50, negated_conjecture, (txt(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
cnf(c_0_51, plain, (phtxt(X2,X3)|~phtxtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_47])).
cnf(c_0_52, negated_conjecture, (phtxtprec(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_48, c_0_41])).
cnf(c_0_53, negated_conjecture, (~phtxt(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_49, c_0_50])).
cnf(c_0_54, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_53]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 0.628 s
# System time              : 0.030 s
# Total time               : 0.659 s
# Maximum resident set size: 1856 pages

% END OF SYSTEM OUTPUT
% RESULT: SOT_TKRfMZ - E---1.9.1 says Theorem - CPU = 0.64 WC = 0.65 
% OUTPUT: SOT_TKRfMZ - E---1.9.1 says CNFRefutation - CPU = 0.64 WC = 0.65