% 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
# AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S0YP
# and selection function SelectMaxLComplexAvoidPosPred.
#
# Preprocessing time       : 0.019 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(c_0_0, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>![X2]:(present(X4,X2)=>present(X1,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom61)).
fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)<=>?[X10]:?[X7]:((txtdep(X1,X10)&txtdep(X4,X7))&ppt(X10,X7,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom68)).
fof(c_0_2, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>(present(X1,X2)&present(X4,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom7)).
fof(c_0_3, conjecture, (![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)=>?[X5]:(txtppt(X5,X4,X2)&~(?[X6]:(txtppt(X5,X6,X2)&txtppt(X6,X4,X2)))))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', conjectureXXV)).
fof(c_0_4, axiom, (![X10]:![X7]:![X11]:![X8]:![X2]:((txtdep(X10,X7)&txtdep(X11,X8))=>(ppt(X10,X11,X2)<=>ppt(X7,X8,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom63)).
fof(c_0_5, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom3)).
fof(c_0_6, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom56)).
fof(c_0_7, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X3]:(present(X1,X3)=>phtxt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom2)).
fof(c_0_8, axiom, (![X1]:![X2]:![X5]:((txt(X1,X2)&ppt(X5,X1,X2))=>txt(X5,X2))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom65)).
fof(c_0_9, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>?[X4]:(txt(X4,X2)&txtdep(X4,X1)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom57a)).
fof(c_0_10, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X7]:![X8]:((((txt(X7,X2)&txtdep(X7,X1))&txt(X8,X2))&txtdep(X8,X1))=>X7=X8))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom57b)).
fof(c_0_11, axiom, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(phtxt(X4,X2)&txtdep(X1,X4)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom58)).
fof(c_0_12, axiom, (![X1]:![X4]:![X2]:(phppt(X1,X4,X2)=>?[X5]:(phppt(X5,X4,X2)&~(?[X6]:(phppt(X5,X6,X2)&phppt(X6,X4,X2)))))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', axiom26)).
fof(c_0_13, axiom, (![X1]:![X4]:![X2]:(phppt(X1,X4,X2)<=>((ppt(X1,X4,X2)&phtxt(X1,X2))&phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply53189/SOT_PHbuKH', definition17)).
fof(c_0_14, 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_0])])])).
fof(c_0_15, plain, (![X11]:![X12]:![X13]:![X16]:![X17]:![X18]:![X19]:![X20]:((((txtdep(X11,esk13_3(X11,X12,X13))|~txtppt(X11,X12,X13))&(txtdep(X12,esk14_3(X11,X12,X13))|~txtppt(X11,X12,X13)))&(ppt(esk13_3(X11,X12,X13),esk14_3(X11,X12,X13),X13)|~txtppt(X11,X12,X13)))&(((~txtdep(X16,X19)|~txtdep(X17,X20))|~ppt(X19,X20,X18))|txtppt(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_1])])])])])])).
fof(c_0_16, 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_2])])])).
cnf(c_0_17, plain, (present(X1,X2)|~present(X3,X2)|~txtdep(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_14])).
cnf(c_0_18, plain, (txtdep(X2,esk14_3(X1,X2,X3))|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_15])).
cnf(c_0_19, plain, (present(X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_20, plain, (ppt(esk13_3(X1,X2,X3),esk14_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_15])).
fof(c_0_21, negated_conjecture, (~(![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)=>?[X5]:(txtppt(X5,X4,X2)&~(?[X6]:(txtppt(X5,X6,X2)&txtppt(X6,X4,X2))))))), inference(assume_negation,[status(cth)],[c_0_3])).
fof(c_0_22, plain, (![X12]:![X13]:![X14]:![X15]:![X16]:![X17]:(((~ppt(X12,X14,X16)|ppt(X13,X15,X16))|(~txtdep(X12,X13)|~txtdep(X14,X15)))&((~ppt(X13,X15,X17)|ppt(X12,X14,X17))|(~txtdep(X12,X13)|~txtdep(X14,X15))))), 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_23, plain, (present(X1,X2)|~txtppt(X3,X1,X4)|~present(esk14_3(X3,X1,X4),X2)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
cnf(c_0_24, plain, (present(esk14_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_19, c_0_20])).
fof(c_0_25, negated_conjecture, (![X10]:(txtppt(esk17_0,esk18_0,esk19_0)&((txtppt(X10,esk20_1(X10),esk19_0)|~txtppt(X10,esk18_0,esk19_0))&(txtppt(esk20_1(X10),esk18_0,esk19_0)|~txtppt(X10,esk18_0,esk19_0))))), 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_21])])])])])).
cnf(c_0_26, plain, (ppt(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_22])).
fof(c_0_27, 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_5])])])])).
cnf(c_0_28, plain, (present(X1,X2)|~txtppt(X3,X1,X2)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
cnf(c_0_29, negated_conjecture, (txtppt(X1,esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_30, plain, (ppt(X1,X2,X3)|~txtppt(X4,X5,X3)|~txtdep(X1,esk13_3(X4,X5,X3))|~txtdep(X2,esk14_3(X4,X5,X3))), inference(spm,[status(thm)],[c_0_26, c_0_20])).
cnf(c_0_31, plain, (txtdep(X1,esk13_3(X1,X2,X3))|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_15])).
cnf(c_0_32, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_27])).
cnf(c_0_33, negated_conjecture, (present(esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
fof(c_0_34, plain, (![X5]:![X6]:((txt(X5,esk7_2(X5,X6))|~txtdep(X5,X6))&(phtxt(X6,esk8_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_6])])])])).
cnf(c_0_35, plain, (ppt(X1,X2,X3)|~txtppt(X1,X4,X3)|~txtdep(X2,esk14_3(X1,X4,X3))), inference(spm,[status(thm)],[c_0_30, c_0_31])).
cnf(c_0_36, negated_conjecture, (txtppt(esk17_0,esk18_0,esk19_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_37, negated_conjecture, (txt(esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~txt(esk20_1(X1),X2)), inference(spm,[status(thm)],[c_0_32, c_0_33])).
cnf(c_0_38, plain, (txt(X1,esk7_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_34])).
cnf(c_0_39, plain, (ppt(X1,X2,X3)|~txtppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_35, c_0_18])).
cnf(c_0_40, negated_conjecture, (present(esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_28, c_0_36])).
cnf(c_0_41, negated_conjecture, (txt(esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~txtdep(esk20_1(X1),X2)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
cnf(c_0_42, plain, (txtppt(X1,X2,X3)|~ppt(X4,X5,X3)|~txtdep(X2,X5)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_15])).
fof(c_0_43, plain, (![X4]:![X5]:![X6]:(~phtxt(X4,X5)|(~present(X4,X6)|phtxt(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_44, plain, (present(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_45, plain, (ppt(X4,X2,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X3,X1,X5)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_46, negated_conjecture, (ppt(esk17_0,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_39, c_0_36])).
cnf(c_0_47, negated_conjecture, (txt(esk18_0,esk19_0)|~txt(esk18_0,X1)), inference(spm,[status(thm)],[c_0_32, c_0_40])).
fof(c_0_48, plain, (![X6]:![X7]:![X8]:((~txt(X6,X7)|~ppt(X8,X6,X7))|txt(X8,X7))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])).
cnf(c_0_49, negated_conjecture, (txt(esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~txtppt(X2,esk20_1(X1),X3)), inference(spm,[status(thm)],[c_0_41, c_0_18])).
cnf(c_0_50, plain, (txtppt(X1,X2,X3)|~txtppt(X4,X5,X3)|~txtdep(X2,esk14_3(X4,X5,X3))|~txtdep(X1,esk13_3(X4,X5,X3))), inference(spm,[status(thm)],[c_0_42, c_0_20])).
fof(c_0_51, plain, (![X5]:![X6]:((txt(esk9_2(X5,X6),X6)|~phtxt(X5,X6))&(txtdep(esk9_2(X5,X6),X5)|~phtxt(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_52, plain, (phtxt(X1,X2)|~present(X1,X2)|~phtxt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_43])).
cnf(c_0_53, plain, (present(esk13_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_44, c_0_20])).
fof(c_0_54, plain, (![X9]:![X10]:![X11]:![X12]:(~phtxt(X9,X10)|((((~txt(X11,X10)|~txtdep(X11,X9))|~txt(X12,X10))|~txtdep(X12,X9))|X11=X12))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])).
cnf(c_0_55, negated_conjecture, (ppt(X1,X2,esk19_0)|~txtdep(esk17_0,X1)|~txtdep(esk18_0,X2)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
fof(c_0_56, plain, (![X5]:![X6]:((phtxt(esk10_2(X5,X6),X6)|~txt(X5,X6))&(txtdep(X5,esk10_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_11])])])])).
cnf(c_0_57, negated_conjecture, (txt(esk18_0,esk19_0)|~txtdep(esk18_0,X1)), inference(spm,[status(thm)],[c_0_47, c_0_38])).
cnf(c_0_58, plain, (txt(X1,X2)|~ppt(X1,X3,X2)|~txt(X3,X2)), inference(split_conjunct,[status(thm)],[c_0_48])).
cnf(c_0_59, negated_conjecture, (ppt(X1,esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_39, c_0_29])).
cnf(c_0_60, negated_conjecture, (txt(esk20_1(X1),esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_49, c_0_29])).
cnf(c_0_61, plain, (txtppt(X1,X2,X3)|~txtppt(X4,X2,X3)|~txtdep(X1,esk13_3(X4,X2,X3))), inference(spm,[status(thm)],[c_0_50, c_0_18])).
cnf(c_0_62, plain, (txtdep(esk9_2(X1,X2),X1)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_51])).
cnf(c_0_63, plain, (phtxt(esk13_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)|~phtxt(esk13_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_52, c_0_53])).
cnf(c_0_64, plain, (phtxt(X2,esk8_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_34])).
cnf(c_0_65, plain, (phtxt(esk14_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)|~phtxt(esk14_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_52, c_0_24])).
cnf(c_0_66, plain, (X1=X2|~txtdep(X2,X3)|~txt(X2,X4)|~txtdep(X1,X3)|~txt(X1,X4)|~phtxt(X3,X4)), inference(split_conjunct,[status(thm)],[c_0_54])).
cnf(c_0_67, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk17_0,X1)|~txtdep(esk18_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_55])).
cnf(c_0_68, plain, (txtdep(X1,esk10_2(X1,X2))|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_56])).
cnf(c_0_69, negated_conjecture, (txt(esk18_0,esk19_0)|~txtppt(X1,esk18_0,X2)), inference(spm,[status(thm)],[c_0_57, c_0_18])).
cnf(c_0_70, negated_conjecture, (txt(X1,esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60])).
cnf(c_0_71, plain, (txtppt(esk9_2(esk13_3(X1,X2,X3),X4),X2,X3)|~txtppt(X1,X2,X3)|~phtxt(esk13_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_61, c_0_62])).
cnf(c_0_72, plain, (phtxt(esk13_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)|~txtdep(X4,esk13_3(X1,X2,X3))), inference(spm,[status(thm)],[c_0_63, c_0_64])).
cnf(c_0_73, plain, (ppt(X1,esk9_2(esk14_3(X1,X2,X3),X4),X3)|~txtppt(X1,X2,X3)|~phtxt(esk14_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_35, c_0_62])).
cnf(c_0_74, plain, (phtxt(esk14_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)|~txtdep(X4,esk14_3(X1,X2,X3))), inference(spm,[status(thm)],[c_0_65, c_0_64])).
cnf(c_0_75, plain, (X1=esk9_2(X2,X3)|~txtdep(X1,X2)|~txt(esk9_2(X2,X3),X4)|~txt(X1,X4)|~phtxt(X2,X4)|~phtxt(X2,X3)), inference(spm,[status(thm)],[c_0_66, c_0_62])).
cnf(c_0_76, plain, (txt(esk9_2(X1,X2),X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_51])).
cnf(c_0_77, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk17_0,X1)|~txt(esk18_0,X2)), inference(spm,[status(thm)],[c_0_67, c_0_68])).
cnf(c_0_78, negated_conjecture, (txt(esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_69, c_0_36])).
cnf(c_0_79, negated_conjecture, (txt(esk9_2(esk13_3(X1,esk18_0,esk19_0),X2),esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~phtxt(esk13_3(X1,esk18_0,esk19_0),X2)), inference(spm,[status(thm)],[c_0_70, c_0_71])).
cnf(c_0_80, plain, (phtxt(esk13_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_72, c_0_31])).
cnf(c_0_81, plain, (txt(X1,X2)|~txtppt(X1,X3,X2)|~txt(esk9_2(esk14_3(X1,X3,X2),X4),X2)|~phtxt(esk14_3(X1,X3,X2),X4)), inference(spm,[status(thm)],[c_0_58, c_0_73])).
cnf(c_0_82, plain, (phtxt(esk14_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_74, c_0_18])).
cnf(c_0_83, plain, (X1=esk9_2(X2,X3)|~txtdep(X1,X2)|~txt(X1,X3)|~phtxt(X2,X3)), inference(spm,[status(thm)],[c_0_75, c_0_76])).
cnf(c_0_84, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk17_0,X1)), inference(spm,[status(thm)],[c_0_77, c_0_78])).
cnf(c_0_85, negated_conjecture, (X1=esk9_2(esk13_3(X2,esk18_0,esk19_0),X3)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X1,esk13_3(X2,esk18_0,esk19_0))|~txt(X1,esk19_0)|~phtxt(esk13_3(X2,esk18_0,esk19_0),X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_79]), c_0_80])).
cnf(c_0_86, plain, (txt(X1,X2)|~txtppt(X1,X3,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_76]), c_0_82])).
cnf(c_0_87, plain, (esk9_2(X1,X2)=esk9_2(X1,X3)|~txt(esk9_2(X1,X2),X3)|~phtxt(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_83, c_0_62])).
cnf(c_0_88, negated_conjecture, (phtxt(X1,esk19_0)|~txtdep(esk17_0,X1)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_52, c_0_84])).
cnf(c_0_89, plain, (present(X1,X2)|~txtppt(X1,X3,X4)|~present(esk13_3(X1,X3,X4),X2)), inference(spm,[status(thm)],[c_0_17, c_0_31])).
cnf(c_0_90, negated_conjecture, (esk9_2(esk13_3(X1,esk18_0,esk19_0),X2)=X1|~txtppt(X1,esk18_0,esk19_0)|~phtxt(esk13_3(X1,esk18_0,esk19_0),X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_31]), c_0_86])).
cnf(c_0_91, negated_conjecture, (esk9_2(esk13_3(X1,esk18_0,esk19_0),X2)=esk9_2(esk13_3(X1,esk18_0,esk19_0),esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~phtxt(esk13_3(X1,esk18_0,esk19_0),X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_79]), c_0_80])).
cnf(c_0_92, negated_conjecture, (phtxt(esk13_3(esk17_0,X1,X2),esk19_0)|~txtppt(esk17_0,X1,X2)|~phtxt(esk13_3(esk17_0,X1,X2),X3)), inference(spm,[status(thm)],[c_0_88, c_0_31])).
cnf(c_0_93, plain, (present(X1,X2)|~txtppt(X1,X3,X2)), inference(spm,[status(thm)],[c_0_89, c_0_53])).
cnf(c_0_94, negated_conjecture, (esk9_2(esk13_3(X1,esk18_0,esk19_0),esk19_0)=X1|~txtppt(X1,esk18_0,esk19_0)|~phtxt(esk13_3(X1,esk18_0,esk19_0),X2)), inference(spm,[status(thm)],[c_0_90, c_0_91])).
cnf(c_0_95, negated_conjecture, (phtxt(esk13_3(esk17_0,X1,X2),esk19_0)|~txtppt(esk17_0,X1,X2)), inference(spm,[status(thm)],[c_0_92, c_0_80])).
cnf(c_0_96, negated_conjecture, (present(esk17_0,esk19_0)), inference(spm,[status(thm)],[c_0_93, c_0_36])).
cnf(c_0_97, negated_conjecture, (esk9_2(esk13_3(esk17_0,esk18_0,esk19_0),esk19_0)=esk17_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_36])])).
cnf(c_0_98, negated_conjecture, (txt(esk17_0,esk19_0)|~txt(esk17_0,X1)), inference(spm,[status(thm)],[c_0_32, c_0_96])).
fof(c_0_99, plain, (![X7]:![X8]:![X9]:![X11]:((phppt(esk4_3(X7,X8,X9),X8,X9)|~phppt(X7,X8,X9))&((~phppt(esk4_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_12])])])])])).
fof(c_0_100, 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_13])])])])])).
cnf(c_0_101, plain, (ppt(X1,X2,X3)|~txtppt(X4,X5,X3)|~txtdep(esk9_2(esk14_3(X4,X5,X3),X6),X2)|~txtdep(X4,X1)|~phtxt(esk14_3(X4,X5,X3),X6)), inference(spm,[status(thm)],[c_0_45, c_0_73])).
cnf(c_0_102, negated_conjecture, (esk9_2(esk13_3(esk17_0,esk18_0,esk19_0),X1)=esk17_0|~phtxt(esk13_3(esk17_0,esk18_0,esk19_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_97]), c_0_36])])).
cnf(c_0_103, negated_conjecture, (txt(esk17_0,esk19_0)|~txtdep(esk17_0,X1)), inference(spm,[status(thm)],[c_0_98, c_0_38])).
cnf(c_0_104, plain, (~phppt(X1,X2,X3)|~phppt(X4,X2,X3)|~phppt(esk4_3(X1,X2,X3),X4,X3)), inference(split_conjunct,[status(thm)],[c_0_99])).
cnf(c_0_105, plain, (phppt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_100])).
cnf(c_0_106, plain, (phtxt(X1,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_100])).
cnf(c_0_107, plain, (ppt(X1,esk14_3(X2,X3,X4),X4)|~txtppt(X2,X3,X4)|~txtdep(X2,X1)|~phtxt(esk14_3(X2,X3,X4),X5)), inference(spm,[status(thm)],[c_0_101, c_0_62])).
cnf(c_0_108, plain, (phppt(esk4_3(X1,X2,X3),X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_99])).
cnf(c_0_109, negated_conjecture, (txtppt(esk20_1(X1),esk18_0,esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_110, negated_conjecture, (ppt(X1,X2,esk19_0)|~txtppt(X3,esk18_0,esk19_0)|~txtdep(esk20_1(X3),X2)|~txtdep(X3,X1)), inference(spm,[status(thm)],[c_0_45, c_0_59])).
cnf(c_0_111, negated_conjecture, (txtdep(esk17_0,esk13_3(esk17_0,esk18_0,esk19_0))|~phtxt(esk13_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_62, c_0_102])).
cnf(c_0_112, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk17_0,X2)|~txtdep(esk18_0,X1)), inference(spm,[status(thm)],[c_0_19, c_0_55])).
cnf(c_0_113, negated_conjecture, (txt(esk17_0,esk19_0)|~txtppt(esk17_0,X1,X2)), inference(spm,[status(thm)],[c_0_103, c_0_31])).
cnf(c_0_114, plain, (~phppt(X1,X2,X3)|~phppt(X4,X2,X3)|~ppt(esk4_3(X4,X2,X3),X1,X3)|~phtxt(esk4_3(X4,X2,X3),X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_105]), c_0_106])).
cnf(c_0_115, plain, (ppt(X1,esk14_3(X2,X3,X4),X4)|~txtppt(X2,X3,X4)|~txtdep(X2,X1)), inference(spm,[status(thm)],[c_0_107, c_0_82])).
cnf(c_0_116, plain, (phtxt(esk4_3(X1,X2,X3),X3)|~phppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_106, c_0_108])).
cnf(c_0_117, negated_conjecture, (ppt(esk20_1(X1),esk18_0,esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_39, c_0_109])).
cnf(c_0_118, negated_conjecture, (ppt(X1,esk10_2(esk20_1(X2),X3),esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X2,X1)|~txt(esk20_1(X2),X3)), inference(spm,[status(thm)],[c_0_110, c_0_68])).
cnf(c_0_119, plain, (present(esk9_2(X1,X2),X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_17, c_0_62])).
cnf(c_0_120, negated_conjecture, (txtdep(esk17_0,esk13_3(esk17_0,esk18_0,esk19_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_95]), c_0_36])])).
cnf(c_0_121, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk18_0,X1)|~txt(esk17_0,X2)), inference(spm,[status(thm)],[c_0_112, c_0_68])).
cnf(c_0_122, negated_conjecture, (txt(esk17_0,esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_29]), c_0_36])])).
cnf(c_0_123, plain, (~txtppt(X1,X2,X3)|~txtdep(X1,esk4_3(X4,X5,X3))|~phppt(esk14_3(X1,X2,X3),X5,X3)|~phppt(X4,X5,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_114, c_0_115]), c_0_116])).
cnf(c_0_124, plain, (phtxt(X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_100])).
cnf(c_0_125, negated_conjecture, (ppt(X1,X2,esk19_0)|~txtppt(X3,esk18_0,esk19_0)|~txtdep(esk20_1(X3),X1)|~txtdep(esk18_0,X2)), inference(spm,[status(thm)],[c_0_45, c_0_117])).
cnf(c_0_126, negated_conjecture, (txtppt(X1,X2,esk19_0)|~txtppt(X3,esk18_0,esk19_0)|~txtdep(X2,esk10_2(esk20_1(X3),X4))|~txtdep(X1,X5)|~txtdep(X3,X5)|~txt(esk20_1(X3),X4)), inference(spm,[status(thm)],[c_0_42, c_0_118])).
cnf(c_0_127, plain, (txt(esk9_2(X1,X2),X3)|~txt(esk9_2(X1,X2),X4)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_32, c_0_119])).
cnf(c_0_128, negated_conjecture, (ppt(esk17_0,X1,esk19_0)|~txtdep(X1,esk14_3(esk17_0,esk18_0,esk19_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_120]), c_0_36])])).
cnf(c_0_129, negated_conjecture, (present(X1,esk19_0)|~txtdep(esk18_0,X1)), inference(spm,[status(thm)],[c_0_121, c_0_122])).
cnf(c_0_130, plain, (~txtppt(X1,X2,X3)|~txtdep(X1,esk4_3(X4,X5,X3))|~phppt(X4,X5,X3)|~ppt(esk14_3(X1,X2,X3),X5,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_105]), c_0_82]), c_0_124])).
cnf(c_0_131, negated_conjecture, (ppt(esk14_3(X1,esk20_1(X2),X3),X4,esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtppt(X1,esk20_1(X2),X3)|~txtdep(esk18_0,X4)), inference(spm,[status(thm)],[c_0_125, c_0_18])).
cnf(c_0_132, negated_conjecture, (txtppt(X1,esk20_1(X2),esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X1,X3)|~txtdep(X2,X3)|~txt(esk20_1(X2),X4)), inference(spm,[status(thm)],[c_0_126, c_0_68])).
cnf(c_0_133, plain, (ppt(X1,X2,X3)|~phppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_100])).
cnf(c_0_134, plain, (txt(esk9_2(X1,X2),X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_127, c_0_76])).
cnf(c_0_135, negated_conjecture, (ppt(esk17_0,esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_128, c_0_62])).
cnf(c_0_136, negated_conjecture, (phtxt(X1,esk19_0)|~txtdep(esk18_0,X1)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_52, c_0_129])).
cnf(c_0_137, negated_conjecture, (~txtppt(X1,esk20_1(X2),esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X1,esk4_3(X3,X4,esk19_0))|~txtdep(esk18_0,X4)|~phppt(X3,X4,esk19_0)), inference(spm,[status(thm)],[c_0_130, c_0_131])).
cnf(c_0_138, negated_conjecture, (txtppt(X1,esk20_1(X2),esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X1,X3)|~txtdep(X2,X3)), inference(spm,[status(thm)],[c_0_132, c_0_60])).
cnf(c_0_139, plain, (ppt(esk4_3(X1,X2,X3),X2,X3)|~phppt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_133, c_0_108])).
cnf(c_0_140, plain, (esk9_2(X1,X2)=esk9_2(X1,X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_134]), c_0_52])).
cnf(c_0_141, negated_conjecture, (ppt(X1,X2,esk19_0)|~txtdep(esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X3),X2)|~txtdep(esk17_0,X1)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X3)), inference(spm,[status(thm)],[c_0_45, c_0_135])).
cnf(c_0_142, negated_conjecture, (phtxt(esk14_3(X1,esk18_0,X2),esk19_0)|~txtppt(X1,esk18_0,X2)|~phtxt(esk14_3(X1,esk18_0,X2),X3)), inference(spm,[status(thm)],[c_0_136, c_0_18])).
cnf(c_0_143, negated_conjecture, (~txtppt(esk9_2(esk4_3(X1,X2,esk19_0),X3),esk20_1(X4),esk19_0)|~txtppt(X4,esk18_0,esk19_0)|~txtdep(esk18_0,X2)|~phppt(X1,X2,esk19_0)|~phtxt(esk4_3(X1,X2,esk19_0),X3)), inference(spm,[status(thm)],[c_0_137, c_0_62])).
cnf(c_0_144, negated_conjecture, (txtppt(esk9_2(X1,X2),esk20_1(X3),esk19_0)|~txtppt(X3,esk18_0,esk19_0)|~txtdep(X3,X1)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_138, c_0_62])).
cnf(c_0_145, plain, (txtppt(X1,X2,X3)|~txtdep(X1,esk4_3(X4,X5,X3))|~txtdep(X2,X5)|~phppt(X4,X5,X3)), inference(spm,[status(thm)],[c_0_42, c_0_139])).
cnf(c_0_146, negated_conjecture, (present(X1,esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X2,X1)|~txt(esk20_1(X2),X3)), inference(spm,[status(thm)],[c_0_44, c_0_118])).
cnf(c_0_147, plain, (txtdep(esk9_2(X1,X2),X1)|~present(X1,X2)|~phtxt(X1,X3)), inference(spm,[status(thm)],[c_0_62, c_0_140])).
cnf(c_0_148, negated_conjecture, (present(esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_19, c_0_135])).
cnf(c_0_149, negated_conjecture, (ppt(X1,esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~txtdep(esk17_0,X1)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X2)), inference(spm,[status(thm)],[c_0_141, c_0_62])).
cnf(c_0_150, negated_conjecture, (phtxt(esk14_3(X1,esk18_0,X2),esk19_0)|~txtppt(X1,esk18_0,X2)), inference(spm,[status(thm)],[c_0_142, c_0_82])).
cnf(c_0_151, negated_conjecture, (~txtdep(X1,esk4_3(X2,X3,esk19_0))|~txtdep(esk18_0,X3)|~phppt(X2,X3,esk19_0)|~phtxt(esk4_3(X2,X3,esk19_0),X4)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_143, c_0_144]), c_0_145])).
cnf(c_0_152, negated_conjecture, (txtppt(esk9_2(esk13_3(X1,esk18_0,esk19_0),esk19_0),esk18_0,esk19_0)|~txtppt(X1,esk18_0,esk19_0)|~phtxt(esk13_3(X1,esk18_0,esk19_0),X2)), inference(spm,[status(thm)],[c_0_71, c_0_91])).
cnf(c_0_153, negated_conjecture, (present(X1,esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(X2,X1)), inference(spm,[status(thm)],[c_0_146, c_0_60])).
cnf(c_0_154, plain, (txtdep(esk9_2(X1,X2),X1)|~txtdep(X3,X1)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_147, c_0_64])).
cnf(c_0_155, plain, (X1=X2|~txtppt(X3,X2,X4)|~txtdep(X1,esk14_3(X3,X2,X4))|~txt(X2,X5)|~txt(X1,X5)|~phtxt(esk14_3(X3,X2,X4),X5)), inference(spm,[status(thm)],[c_0_66, c_0_18])).
cnf(c_0_156, negated_conjecture, (txt(esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1),esk19_0)|~txt(esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1),X2)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_32, c_0_148])).
cnf(c_0_157, negated_conjecture, (ppt(X1,esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~txtdep(esk17_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_150]), c_0_36])])).
cnf(c_0_158, negated_conjecture, (~txtdep(esk18_0,X1)|~phppt(X2,X1,esk19_0)|~phtxt(esk4_3(X2,X1,esk19_0),X3)|~phtxt(esk4_3(X2,X1,esk19_0),X4)), inference(spm,[status(thm)],[c_0_151, c_0_62])).
cnf(c_0_159, negated_conjecture, (txtppt(esk9_2(esk13_3(X1,esk18_0,esk19_0),esk19_0),esk18_0,esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_152, c_0_80])).
cnf(c_0_160, negated_conjecture, (present(X1,esk19_0)|~txtppt(X2,esk18_0,esk19_0)|~txtdep(esk9_2(esk13_3(X2,esk18_0,esk19_0),X3),X1)|~phtxt(esk13_3(X2,esk18_0,esk19_0),X3)), inference(spm,[status(thm)],[c_0_153, c_0_71])).
cnf(c_0_161, negated_conjecture, (txtdep(esk9_2(esk13_3(esk17_0,esk18_0,esk19_0),X1),esk13_3(esk17_0,esk18_0,esk19_0))|~present(esk13_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_154, c_0_120])).
cnf(c_0_162, negated_conjecture, (phtxt(esk13_3(esk17_0,esk18_0,esk19_0),esk19_0)|~phtxt(esk13_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_88, c_0_120])).
cnf(c_0_163, plain, (esk9_2(esk14_3(X1,X2,X3),X4)=X2|~txtppt(X1,X2,X3)|~txt(esk9_2(esk14_3(X1,X2,X3),X4),X5)|~txt(X2,X5)|~phtxt(esk14_3(X1,X2,X3),X5)|~phtxt(esk14_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_155, c_0_62])).
cnf(c_0_164, negated_conjecture, (txt(esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_156, c_0_76])).
cnf(c_0_165, negated_conjecture, (present(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~txtdep(esk17_0,X1)), inference(spm,[status(thm)],[c_0_19, c_0_157])).
cnf(c_0_166, negated_conjecture, (~txtdep(esk18_0,X1)|~phppt(X2,X1,esk19_0)|~phtxt(esk4_3(X2,X1,esk19_0),X3)), inference(spm,[status(thm)],[c_0_158, c_0_116])).
cnf(c_0_167, negated_conjecture, (ppt(esk9_2(esk13_3(X1,esk18_0,esk19_0),esk19_0),esk18_0,esk19_0)|~txtppt(X1,esk18_0,esk19_0)), inference(spm,[status(thm)],[c_0_39, c_0_159])).
cnf(c_0_168, negated_conjecture, (present(esk13_3(esk17_0,esk18_0,esk19_0),esk19_0)|~present(esk13_3(esk17_0,esk18_0,esk19_0),X1)|~phtxt(esk13_3(esk17_0,esk18_0,esk19_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_160, c_0_161]), c_0_36])])).
cnf(c_0_169, negated_conjecture, (phtxt(esk13_3(esk17_0,esk18_0,esk19_0),esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_95]), c_0_36])])).
cnf(c_0_170, negated_conjecture, (esk9_2(esk14_3(esk17_0,esk18_0,esk19_0),X1)=esk18_0|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163, c_0_164]), c_0_36]), c_0_78])])).
cnf(c_0_171, negated_conjecture, (present(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)), inference(spm,[status(thm)],[c_0_165, c_0_120])).
cnf(c_0_172, negated_conjecture, (~txtdep(esk18_0,X1)|~phppt(X2,X1,esk19_0)), inference(spm,[status(thm)],[c_0_166, c_0_116])).
cnf(c_0_173, negated_conjecture, (ppt(X1,X2,esk19_0)|~txtppt(X3,esk18_0,esk19_0)|~txtdep(esk9_2(esk13_3(X3,esk18_0,esk19_0),esk19_0),X1)|~txtdep(esk18_0,X2)), inference(spm,[status(thm)],[c_0_45, c_0_167])).
cnf(c_0_174, negated_conjecture, (present(esk13_3(esk17_0,esk18_0,esk19_0),esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_168, c_0_84]), c_0_169]), c_0_120])])).
cnf(c_0_175, negated_conjecture, (txtdep(esk18_0,esk14_3(esk17_0,esk18_0,esk19_0))|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_62, c_0_170])).
cnf(c_0_176, negated_conjecture, (phtxt(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),X1)), inference(spm,[status(thm)],[c_0_52, c_0_171])).
cnf(c_0_177, negated_conjecture, (~txtdep(esk18_0,X1)|~ppt(X2,X1,esk19_0)|~phtxt(X1,esk19_0)|~phtxt(X2,esk19_0)), inference(spm,[status(thm)],[c_0_172, c_0_105])).
cnf(c_0_178, negated_conjecture, (ppt(esk13_3(esk17_0,esk18_0,esk19_0),X1,esk19_0)|~txtdep(esk18_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173, c_0_161]), c_0_36]), c_0_174])])).
cnf(c_0_179, negated_conjecture, (txtdep(esk18_0,esk14_3(esk17_0,esk18_0,esk19_0))|~phtxt(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_175, c_0_150]), c_0_36])])).
cnf(c_0_180, negated_conjecture, (phtxt(esk14_3(esk17_0,esk18_0,esk19_0),esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176, c_0_150]), c_0_36])])).
cnf(c_0_181, negated_conjecture, (~txtdep(esk18_0,X1)|~phtxt(X1,esk19_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177, c_0_178]), c_0_169])])).
cnf(c_0_182, negated_conjecture, (txtdep(esk18_0,esk14_3(esk17_0,esk18_0,esk19_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_179, c_0_180])])).
cnf(c_0_183, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_181, c_0_182]), c_0_180])]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 34.002 s
# System time              : 0.237 s
# Total time               : 34.238 s
# Maximum resident set size: 1764 pages

% END OF SYSTEM OUTPUT
% RESULT: SOT_PHbuKH - E---1.9.1 says Theorem - CPU = 34.13 WC = 34.20 
% OUTPUT: SOT_PHbuKH - E---1.9.1 says CNFRefutation - CPU = 34.13 WC = 34.21