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

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(c_0_0, axiom, (![X2]:(time(X2)=>~(nontime(X2)))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', axiomCX)).
fof(c_0_1, conjecture, (![X1]:![X2]:![X6]:(txt(X1,X2)=>(![X6]:txtpt(X6,X1,X2)=>?[X4]:(txtpt(X4,X6,X2)&![X5]:~(txtppt(X5,X4,X2)))))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', conjectureXXVI)).
fof(c_0_2, axiom, (![X1]:((obj(X1)|reg(X1))=>nontime(X1))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', axiomCIX)).
fof(c_0_3, axiom, (![X1]:![X2]:(txt(X1,X2)=>(obj(X1)&time(X2)))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', axiomCI)).
fof(c_0_4, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(obj(X1)&obj(X4)))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', axiomCII)).
fof(c_0_5, axiom, (![X1]:![X4]:![X2]:(txtpt(X1,X4,X2)<=>?[X10]:?[X7]:((txtdep(X1,X10)&txtdep(X4,X7))&pt(X10,X7,X2)))), file('/tmp/SystemOnTPTPFormReply53304/SOT_I5hUgQ', axiomLXX)).
fof(c_0_6, plain, (![X2]:(time(X2)=>~nontime(X2))), inference(fof_simplification,[status(thm)],[c_0_0])).
fof(c_0_7, negated_conjecture, (~(![X1]:![X2]:![X6]:(txt(X1,X2)=>(![X6]:txtpt(X6,X1,X2)=>?[X4]:(txtpt(X4,X6,X2)&![X5]:~txtppt(X5,X4,X2)))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_1])])).
fof(c_0_8, plain, (![X3]:(~time(X3)|~nontime(X3))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])).
fof(c_0_9, plain, (![X2]:((~obj(X2)|nontime(X2))&(~reg(X2)|nontime(X2)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])).
fof(c_0_10, plain, (![X3]:![X4]:((obj(X3)|~txt(X3,X4))&(time(X4)|~txt(X3,X4)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])).
fof(c_0_11, negated_conjecture, (![X9]:![X11]:(txt(esk17_0,esk18_0)&(txtpt(X9,esk17_0,esk18_0)&(~txtpt(X11,esk19_0,esk18_0)|txtppt(esk20_1(X11),X11,esk18_0))))), 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])])])])])).
fof(c_0_12, plain, (![X5]:![X6]:((obj(X5)|~txtdep(X5,X6))&(obj(X6)|~txtdep(X5,X6)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])).
fof(c_0_13, plain, (![X11]:![X12]:![X13]:![X16]:![X17]:![X18]:![X19]:![X20]:((((txtdep(X11,esk15_3(X11,X12,X13))|~txtpt(X11,X12,X13))&(txtdep(X12,esk16_3(X11,X12,X13))|~txtpt(X11,X12,X13)))&(pt(esk15_3(X11,X12,X13),esk16_3(X11,X12,X13),X13)|~txtpt(X11,X12,X13)))&(((~txtdep(X16,X19)|~txtdep(X17,X20))|~pt(X19,X20,X18))|txtpt(X16,X17,X18)))), 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_14, plain, (~nontime(X1)|~time(X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
cnf(c_0_15, plain, (nontime(X1)|~obj(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
cnf(c_0_16, plain, (time(X2)|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_10])).
cnf(c_0_17, negated_conjecture, (txt(esk17_0,esk18_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
cnf(c_0_18, plain, (obj(X1)|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
cnf(c_0_19, plain, (txtdep(X1,esk15_3(X1,X2,X3))|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_13])).
cnf(c_0_20, plain, (~obj(X1)|~time(X1)), inference(spm,[status(thm)],[c_0_14, c_0_15])).
cnf(c_0_21, negated_conjecture, (time(esk18_0)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
cnf(c_0_22, plain, (obj(X1)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
cnf(c_0_23, negated_conjecture, (txtpt(X1,esk17_0,esk18_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
cnf(c_0_24, negated_conjecture, (~obj(esk18_0)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
cnf(c_0_25, negated_conjecture, (obj(X1)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
cnf(c_0_26, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 0.016 s
# System time              : 0.003 s
# Total time               : 0.019 s
# Maximum resident set size: 1764 pages

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