% 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.021 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(c_0_0, axiom, (![X15]:![X17]:![X16]:![X18]:![X2]:((txtdep(X15,X17)&txtdep(X16,X18))=>(phtxtprec(X15,X16,X2)<=>phtxtprec(X17,X18,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom64)).
fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(txtprec(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&phtxtprec(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiomLXXII)).
fof(c_0_2, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom3)).
fof(c_0_3, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom56)).
fof(c_0_4, conjecture, (![X1]:![X4]:![X2]:(txtprec(X1,X4,X2)=>![X5]:(txtpt(X5,X4,X2)=>txtprec(X1,X5,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', conjectureXXXVII)).
fof(c_0_5, axiom, (![X1]:![X2]:![X4]:![X3]:(phtxtequiv(X1,X2,X4,X3)=>(present(X1,X2)&present(X4,X3)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom48)).
fof(c_0_6, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>phtxtequiv(X1,X2,X1,X2))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom49)).
fof(c_0_7, axiom, (![X2]:~(?[X1]:(phtxt(X1,X2)&txt(X1,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom66)).
fof(c_0_8, axiom, (![X1]:![X4]:![X2]:(phtxtprec(X1,X4,X2)=>(phtxt(X1,X2)&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply56052/SOT_yPWlLc', axiom30)).
fof(c_0_9, 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_0])])])])])).
fof(c_0_10, 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_1])])])])])])).
fof(c_0_11, 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_2])])])])).
fof(c_0_12, 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_3])])])])).
cnf(c_0_13, plain, (phtxtprec(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~phtxtprec(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_9])).
cnf(c_0_14, plain, (phtxtprec(esk40_3(X1,X2,X3),esk41_3(X1,X2,X3),X3)|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])).
cnf(c_0_15, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_11])).
cnf(c_0_16, plain, (txt(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
fof(c_0_17, negated_conjecture, (~(![X1]:![X4]:![X2]:(txtprec(X1,X4,X2)=>![X5]:(txtpt(X5,X4,X2)=>txtprec(X1,X5,X2))))), inference(assume_negation,[status(cth)],[c_0_4])).
cnf(c_0_18, 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_13, c_0_14])).
cnf(c_0_19, plain, (txtdep(X1,esk40_3(X1,X2,X3))|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])).
cnf(c_0_20, plain, (txt(X1,X2)|~txtdep(X1,X3)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
cnf(c_0_21, plain, (txtdep(X2,esk41_3(X1,X2,X3))|~txtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_10])).
fof(c_0_22, negated_conjecture, ((txtprec(esk47_0,esk48_0,esk49_0)&(txtpt(esk50_0,esk48_0,esk49_0)&~txtprec(esk47_0,esk50_0,esk49_0)))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])])).
fof(c_0_23, 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_5])])])).
fof(c_0_24, plain, (![X3]:![X4]:(~phtxt(X3,X4)|phtxtequiv(X3,X4,X3,X4))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])).
cnf(c_0_25, plain, (phtxtprec(X1,X2,X3)|~txtprec(X1,X4,X3)|~txtdep(X2,esk41_3(X1,X4,X3))), inference(spm,[status(thm)],[c_0_18, c_0_19])).
fof(c_0_26, plain, (![X3]:![X4]:(~phtxt(X4,X3)|~txt(X4,X3))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])).
cnf(c_0_27, plain, (txt(X1,X2)|~txtprec(X3,X1,X4)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
cnf(c_0_28, negated_conjecture, (txtprec(esk47_0,esk48_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_29, plain, (present(X1,X2)|~phtxtequiv(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_23])).
cnf(c_0_30, plain, (phtxtequiv(X1,X2,X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_24])).
fof(c_0_31, 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_8])])])).
cnf(c_0_32, plain, (phtxtprec(X1,X2,X3)|~txtprec(X1,X2,X3)), inference(spm,[status(thm)],[c_0_25, c_0_21])).
cnf(c_0_33, plain, (~txt(X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_26])).
cnf(c_0_34, negated_conjecture, (txt(esk48_0,X1)|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
cnf(c_0_35, plain, (present(X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
cnf(c_0_36, plain, (phtxt(X2,X3)|~phtxtprec(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_31])).
cnf(c_0_37, negated_conjecture, (phtxtprec(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_32, c_0_28])).
cnf(c_0_38, negated_conjecture, (~phtxt(esk48_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_35])).
cnf(c_0_39, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_38]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 0.268 s
# System time              : 0.014 s
# Total time               : 0.282 s
# Maximum resident set size: 1852 pages

% END OF SYSTEM OUTPUT
% RESULT: SOT_yPWlLc - E---1.9.1 says Theorem - CPU = 0.00 WC = 0.28 
% OUTPUT: SOT_yPWlLc - E---1.9.1 says CNFRefutation - CPU = 0.00 WC = 0.28