% 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.014 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
# AutoSched1-Mode selected heuristic G_E___208_C18_F1_AE_CS_SP_PS_S3S
# and selection function SelectNewComplexAHPExceptUniqMaxHorn.
#
# Preprocessing time       : 0.021 s
# Presaturation interreduction done

# 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/SystemOnTPTPFormReply48493/SOT_T54nMk', definition18)).
fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(phoverlap(X1,X4,X2)<=>?[X5]:(phpt(X5,X1,X2)&phpt(X5,X4,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', definition19)).
fof(c_0_2, conjecture, (![X1]:![X4]:![X2]:(txtoverlap(X1,X4,X2)<=>?[X5]:(txtpt(X5,X1,X2)&txtpt(X5,X4,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', conjectureXIX)).
fof(c_0_3, axiom, (![X1]:![X4]:![X2]:(txtpt(X1,X4,X2)<=>?[X8]:?[X6]:((txtdep(X1,X8)&txtdep(X4,X6))&pt(X8,X6,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiomLXX)).
fof(c_0_4, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>?[X4]:(txt(X4,X2)&txtdep(X4,X1)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom57a)).
fof(c_0_5, axiom, (![X1]:![X4]:![X2]:(txtoverlap(X1,X4,X2)<=>?[X8]:?[X6]:((txtdep(X1,X8)&txtdep(X4,X6))&phoverlap(X8,X6,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiomLXXI)).
fof(c_0_6, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', definition4)).
fof(c_0_7, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>(present(X1,X2)&present(X4,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom7)).
fof(c_0_8, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>![X2]:(present(X4,X2)=>present(X1,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom61)).
fof(c_0_9, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom3)).
fof(c_0_10, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X6]:![X7]:((((txt(X6,X2)&txtdep(X6,X1))&txt(X7,X2))&txtdep(X7,X1))=>X6=X7))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom57b)).
fof(c_0_11, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom56)).
fof(c_0_12, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>![X3]:(present(X1,X3)=>phtxt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom2)).
fof(c_0_13, axiom, (![X8]:![X6]:![X9]:![X7]:![X2]:((txtdep(X8,X6)&txtdep(X9,X7))=>(ppt(X8,X9,X2)<=>ppt(X6,X7,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom63)).
fof(c_0_14, axiom, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(phtxt(X4,X2)&txtdep(X1,X4)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', axiom58)).
fof(c_0_15, axiom, (![X1]:![X4]:![X2]:(overlap(X1,X4,X2)<=>?[X5]:(pt(X5,X1,X2)&pt(X5,X4,X2)))), file('/tmp/SystemOnTPTPFormReply48493/SOT_T54nMk', definition5)).
fof(c_0_16, 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_17, plain, (![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X13]:(((phpt(esk2_3(X6,X7,X8),X6,X8)|~phoverlap(X6,X7,X8))&(phpt(esk2_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_1])])])])])])).
fof(c_0_18, negated_conjecture, (~(![X1]:![X4]:![X2]:(txtoverlap(X1,X4,X2)<=>?[X5]:(txtpt(X5,X1,X2)&txtpt(X5,X4,X2))))), inference(assume_negation,[status(cth)],[c_0_2])).
fof(c_0_19, plain, (![X9]:![X10]:![X11]:![X14]:![X15]:![X16]:![X17]:![X18]:((((txtdep(X9,esk11_3(X9,X10,X11))|~txtpt(X9,X10,X11))&(txtdep(X10,esk12_3(X9,X10,X11))|~txtpt(X9,X10,X11)))&(pt(esk11_3(X9,X10,X11),esk12_3(X9,X10,X11),X11)|~txtpt(X9,X10,X11)))&(((~txtdep(X14,X17)|~txtdep(X15,X18))|~pt(X17,X18,X16))|txtpt(X14,X15,X16)))), 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_3])])])])])])).
cnf(c_0_20, plain, (pt(X1,X2,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_21, plain, (phpt(esk2_3(X1,X2,X3),X2,X3)|~phoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_17])).
fof(c_0_22, negated_conjecture, (![X9]:((~txtoverlap(esk15_0,esk16_0,esk17_0)|(~txtpt(X9,esk15_0,esk17_0)|~txtpt(X9,esk16_0,esk17_0)))&((txtpt(esk18_0,esk15_0,esk17_0)|txtoverlap(esk15_0,esk16_0,esk17_0))&(txtpt(esk18_0,esk16_0,esk17_0)|txtoverlap(esk15_0,esk16_0,esk17_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_18])])])])])).
cnf(c_0_23, plain, (txtpt(X1,X2,X3)|~pt(X4,X5,X3)|~txtdep(X2,X5)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_19])).
cnf(c_0_24, plain, (pt(esk2_3(X1,X2,X3),X2,X3)|~phoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
fof(c_0_25, plain, (![X5]:![X6]:((txt(esk5_2(X5,X6),X6)|~phtxt(X5,X6))&(txtdep(esk5_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_4])])])])).
cnf(c_0_26, plain, (phpt(esk2_3(X1,X2,X3),X1,X3)|~phoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_17])).
cnf(c_0_27, negated_conjecture, (~txtpt(X1,esk16_0,esk17_0)|~txtpt(X1,esk15_0,esk17_0)|~txtoverlap(esk15_0,esk16_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_28, negated_conjecture, (txtoverlap(esk15_0,esk16_0,esk17_0)|txtpt(esk18_0,esk15_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_29, plain, (txtpt(X1,X2,X3)|~txtdep(X1,esk2_3(X4,X5,X3))|~txtdep(X2,X5)|~phoverlap(X4,X5,X3)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
cnf(c_0_30, plain, (txtdep(esk5_2(X1,X2),X1)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_31, plain, (pt(esk2_3(X1,X2,X3),X1,X3)|~phoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_20, c_0_26])).
cnf(c_0_32, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtpt(X1,esk15_0,esk17_0)|~txtpt(X1,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
cnf(c_0_33, plain, (txtpt(esk5_2(esk2_3(X1,X2,X3),X4),X5,X3)|~txtdep(X5,X2)|~phoverlap(X1,X2,X3)|~phtxt(esk2_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
cnf(c_0_34, plain, (txtpt(X1,X2,X3)|~txtdep(X1,esk2_3(X4,X5,X3))|~txtdep(X2,X4)|~phoverlap(X4,X5,X3)), inference(spm,[status(thm)],[c_0_23, c_0_31])).
cnf(c_0_35, plain, (phoverlap(X1,X2,X3)|~phpt(X4,X2,X3)|~phpt(X4,X1,X3)), inference(split_conjunct,[status(thm)],[c_0_17])).
cnf(c_0_36, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtpt(esk5_2(esk2_3(X1,X2,esk17_0),X3),esk16_0,esk17_0)|~txtdep(esk15_0,X2)|~phoverlap(X1,X2,esk17_0)|~phtxt(esk2_3(X1,X2,esk17_0),X3)), inference(spm,[status(thm)],[c_0_32, c_0_33])).
cnf(c_0_37, plain, (txtpt(esk5_2(esk2_3(X1,X2,X3),X4),X5,X3)|~txtdep(X5,X1)|~phoverlap(X1,X2,X3)|~phtxt(esk2_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_34, c_0_30])).
cnf(c_0_38, plain, (phtxt(X1,X3)|~phpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_39, plain, (phoverlap(X1,X2,X3)|~phoverlap(X2,X4,X3)|~phpt(esk2_3(X2,X4,X3),X1,X3)), inference(spm,[status(thm)],[c_0_35, c_0_26])).
fof(c_0_40, plain, (![X9]:![X10]:![X11]:![X14]:![X15]:![X16]:![X17]:![X18]:((((txtdep(X9,esk13_3(X9,X10,X11))|~txtoverlap(X9,X10,X11))&(txtdep(X10,esk14_3(X9,X10,X11))|~txtoverlap(X9,X10,X11)))&(phoverlap(esk13_3(X9,X10,X11),esk14_3(X9,X10,X11),X11)|~txtoverlap(X9,X10,X11)))&(((~txtdep(X14,X17)|~txtdep(X15,X18))|~phoverlap(X17,X18,X16))|txtoverlap(X14,X15,X16)))), 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])])])])])])).
fof(c_0_41, 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_6])])])])])).
fof(c_0_42, 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_7])])])).
cnf(c_0_43, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)|~phoverlap(X2,X1,esk17_0)|~phtxt(esk2_3(X2,X1,esk17_0),X3)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
cnf(c_0_44, plain, (phtxt(esk2_3(X1,X2,X3),X3)|~phoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_38, c_0_21])).
cnf(c_0_45, plain, (phoverlap(X1,X2,X3)|~phoverlap(X2,X1,X3)), inference(spm,[status(thm)],[c_0_39, c_0_21])).
cnf(c_0_46, plain, (phoverlap(esk13_3(X1,X2,X3),esk14_3(X1,X2,X3),X3)|~txtoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_40])).
cnf(c_0_47, plain, (ppt(X1,X2,X3)|present(X2,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_41])).
cnf(c_0_48, plain, (present(X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_42])).
fof(c_0_49, 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_8])])])).
cnf(c_0_50, plain, (ppt(X1,X2,X3)|present(X1,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_41])).
cnf(c_0_51, plain, (present(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_42])).
cnf(c_0_52, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)|~phoverlap(X2,X1,esk17_0)), inference(spm,[status(thm)],[c_0_43, c_0_44])).
cnf(c_0_53, plain, (phoverlap(esk14_3(X1,X2,X3),esk13_3(X1,X2,X3),X3)|~txtoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
cnf(c_0_54, plain, (present(X1,X2)|~pt(X3,X1,X2)), inference(csr,[status(thm)],[c_0_47, c_0_48])).
cnf(c_0_55, plain, (present(X1,X2)|~present(X3,X2)|~txtdep(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_49])).
cnf(c_0_56, plain, (txtdep(X1,esk11_3(X1,X2,X3))|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_19])).
cnf(c_0_57, plain, (present(X1,X2)|~pt(X1,X3,X2)), inference(csr,[status(thm)],[c_0_50, c_0_51])).
cnf(c_0_58, plain, (pt(esk11_3(X1,X2,X3),esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_19])).
cnf(c_0_59, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtoverlap(X1,X2,esk17_0)|~txtdep(esk15_0,esk13_3(X1,X2,esk17_0))|~txtdep(esk16_0,esk14_3(X1,X2,esk17_0))), inference(spm,[status(thm)],[c_0_52, c_0_53])).
cnf(c_0_60, plain, (txtdep(X2,esk14_3(X1,X2,X3))|~txtoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_40])).
cnf(c_0_61, plain, (txtdep(X1,esk13_3(X1,X2,X3))|~txtoverlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_40])).
cnf(c_0_62, plain, (present(X1,X2)|~phoverlap(X1,X3,X2)), inference(spm,[status(thm)],[c_0_54, c_0_31])).
cnf(c_0_63, plain, (txtdep(X2,esk12_3(X1,X2,X3))|~txtpt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_19])).
cnf(c_0_64, plain, (present(X1,X2)|~txtpt(X1,X3,X4)|~present(esk11_3(X1,X3,X4),X2)), inference(spm,[status(thm)],[c_0_55, c_0_56])).
cnf(c_0_65, plain, (present(esk11_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
cnf(c_0_66, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|~txtoverlap(X1,esk16_0,esk17_0)|~txtdep(esk15_0,esk13_3(X1,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_59, c_0_60])).
cnf(c_0_67, plain, (present(X1,X2)|~txtoverlap(X1,X3,X4)|~present(esk13_3(X1,X3,X4),X2)), inference(spm,[status(thm)],[c_0_55, c_0_61])).
cnf(c_0_68, plain, (present(esk13_3(X1,X2,X3),X3)|~txtoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_62, c_0_46])).
cnf(c_0_69, plain, (present(X1,X2)|~txtpt(X3,X1,X4)|~present(esk12_3(X3,X1,X4),X2)), inference(spm,[status(thm)],[c_0_55, c_0_63])).
cnf(c_0_70, plain, (present(esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_54, c_0_58])).
fof(c_0_71, 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_9])])])])).
cnf(c_0_72, plain, (present(X1,X2)|~txtpt(X1,X3,X2)), inference(spm,[status(thm)],[c_0_64, c_0_65])).
cnf(c_0_73, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_61]), c_0_28])).
cnf(c_0_74, plain, (ppt(X1,X2,X3)|X1=X2|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_41])).
cnf(c_0_75, plain, (present(X1,X2)|~txtoverlap(X1,X3,X2)), inference(spm,[status(thm)],[c_0_67, c_0_68])).
cnf(c_0_76, plain, (present(X1,X2)|~txtpt(X3,X1,X2)), inference(spm,[status(thm)],[c_0_69, c_0_70])).
fof(c_0_77, plain, (![X8]:![X9]:![X10]:![X11]:(~phtxt(X8,X9)|((((~txt(X10,X9)|~txtdep(X10,X8))|~txt(X11,X9))|~txtdep(X11,X8))|X10=X11))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])).
cnf(c_0_78, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_71])).
cnf(c_0_79, negated_conjecture, (present(esk18_0,esk17_0)), inference(spm,[status(thm)],[c_0_72, c_0_73])).
fof(c_0_80, plain, (![X5]:![X6]:((txt(X5,esk3_2(X5,X6))|~txtdep(X5,X6))&(phtxt(X6,esk4_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_11])])])])).
cnf(c_0_81, plain, (esk11_3(X1,X2,X3)=esk12_3(X1,X2,X3)|ppt(esk11_3(X1,X2,X3),esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_74, c_0_58])).
cnf(c_0_82, negated_conjecture, (present(esk15_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_28]), c_0_76])).
cnf(c_0_83, 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_77])).
cnf(c_0_84, plain, (present(esk5_2(X1,X2),X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_55, c_0_30])).
cnf(c_0_85, negated_conjecture, (txt(esk18_0,esk17_0)|~txt(esk18_0,X1)), inference(spm,[status(thm)],[c_0_78, c_0_79])).
cnf(c_0_86, plain, (txt(X1,esk3_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_80])).
fof(c_0_87, 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_12])])])])).
cnf(c_0_88, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|ppt(esk11_3(esk18_0,esk15_0,esk17_0),esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_81, c_0_73])).
cnf(c_0_89, negated_conjecture, (txt(esk15_0,esk17_0)|~txt(esk15_0,X1)), inference(spm,[status(thm)],[c_0_78, c_0_82])).
cnf(c_0_90, plain, (X1=X2|~txtpt(X2,X3,X4)|~txtdep(X1,esk11_3(X2,X3,X4))|~txt(X2,X5)|~txt(X1,X5)|~phtxt(esk11_3(X2,X3,X4),X5)), inference(spm,[status(thm)],[c_0_83, c_0_56])).
cnf(c_0_91, plain, (txt(esk5_2(X1,X2),X3)|~txt(esk5_2(X1,X2),X4)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_78, c_0_84])).
cnf(c_0_92, plain, (txt(esk5_2(X1,X2),X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_93, negated_conjecture, (txt(esk18_0,esk17_0)|~txtdep(esk18_0,X1)), inference(spm,[status(thm)],[c_0_85, c_0_86])).
cnf(c_0_94, plain, (phtxt(X1,X2)|~present(X1,X2)|~phtxt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_87])).
cnf(c_0_95, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|present(esk11_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_51, c_0_88])).
cnf(c_0_96, negated_conjecture, (txt(esk15_0,esk17_0)|~txtdep(esk15_0,X1)), inference(spm,[status(thm)],[c_0_89, c_0_86])).
cnf(c_0_97, plain, (esk5_2(esk11_3(X1,X2,X3),X4)=X1|~txtpt(X1,X2,X3)|~txt(esk5_2(esk11_3(X1,X2,X3),X4),X5)|~txt(X1,X5)|~phtxt(esk11_3(X1,X2,X3),X5)|~phtxt(esk11_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_90, c_0_30])).
cnf(c_0_98, plain, (txt(esk5_2(X1,X2),X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_91, c_0_92])).
cnf(c_0_99, negated_conjecture, (txt(esk18_0,esk17_0)|~txtpt(esk18_0,X1,X2)), inference(spm,[status(thm)],[c_0_93, c_0_56])).
cnf(c_0_100, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk11_3(esk18_0,esk15_0,esk17_0),esk17_0)|~phtxt(esk11_3(esk18_0,esk15_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_95])).
cnf(c_0_101, plain, (phtxt(X2,esk4_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_80])).
cnf(c_0_102, plain, (X1=X2|~txtpt(X3,X2,X4)|~txtdep(X1,esk12_3(X3,X2,X4))|~txt(X2,X5)|~txt(X1,X5)|~phtxt(esk12_3(X3,X2,X4),X5)), inference(spm,[status(thm)],[c_0_83, c_0_63])).
cnf(c_0_103, negated_conjecture, (txt(esk15_0,esk17_0)|~txtoverlap(esk15_0,X1,X2)), inference(spm,[status(thm)],[c_0_96, c_0_61])).
cnf(c_0_104, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|present(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_48, c_0_88])).
cnf(c_0_105, plain, (esk5_2(esk11_3(X1,X2,X3),X4)=X1|~txtpt(X1,X2,X3)|~txt(X1,X5)|~present(esk11_3(X1,X2,X3),X5)|~phtxt(esk11_3(X1,X2,X3),X4)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_98]), c_0_94])).
cnf(c_0_106, negated_conjecture, (txt(esk18_0,esk17_0)), inference(spm,[status(thm)],[c_0_99, c_0_73])).
cnf(c_0_107, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk11_3(esk18_0,esk15_0,esk17_0),esk17_0)|~txtdep(X1,esk11_3(esk18_0,esk15_0,esk17_0))), inference(spm,[status(thm)],[c_0_100, c_0_101])).
cnf(c_0_108, plain, (esk5_2(esk12_3(X1,X2,X3),X4)=X2|~txtpt(X1,X2,X3)|~txt(esk5_2(esk12_3(X1,X2,X3),X4),X5)|~txt(X2,X5)|~phtxt(esk12_3(X1,X2,X3),X5)|~phtxt(esk12_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_102, c_0_30])).
cnf(c_0_109, negated_conjecture, (txt(esk15_0,esk17_0)|~txtpt(X1,esk15_0,X2)), inference(spm,[status(thm)],[c_0_96, c_0_63])).
cnf(c_0_110, negated_conjecture, (txtpt(esk18_0,esk15_0,esk17_0)|txt(esk15_0,esk17_0)), inference(spm,[status(thm)],[c_0_103, c_0_28])).
cnf(c_0_111, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)|~phtxt(esk12_3(esk18_0,esk15_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_104])).
fof(c_0_112, plain, (![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:(((~ppt(X10,X12,X14)|ppt(X11,X13,X14))|(~txtdep(X10,X11)|~txtdep(X12,X13)))&((~ppt(X11,X13,X15)|ppt(X10,X12,X15))|(~txtdep(X10,X11)|~txtdep(X12,X13))))), 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_113, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|esk5_2(esk11_3(esk18_0,esk15_0,esk17_0),X1)=esk18_0|~phtxt(esk11_3(esk18_0,esk15_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_95]), c_0_73]), c_0_106])])).
cnf(c_0_114, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk11_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_56]), c_0_73])])).
cnf(c_0_115, plain, (esk5_2(esk12_3(X1,X2,X3),X4)=X2|~txtpt(X1,X2,X3)|~txt(X2,X5)|~present(esk12_3(X1,X2,X3),X5)|~phtxt(esk12_3(X1,X2,X3),X4)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_98]), c_0_94])).
cnf(c_0_116, negated_conjecture, (txt(esk15_0,esk17_0)), inference(spm,[status(thm)],[c_0_109, c_0_110])).
cnf(c_0_117, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)|~txtdep(X1,esk12_3(esk18_0,esk15_0,esk17_0))), inference(spm,[status(thm)],[c_0_111, c_0_101])).
cnf(c_0_118, plain, (ppt(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_112])).
cnf(c_0_119, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|esk5_2(esk11_3(esk18_0,esk15_0,esk17_0),esk17_0)=esk18_0), inference(spm,[status(thm)],[c_0_113, c_0_114])).
cnf(c_0_120, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|esk5_2(esk12_3(esk18_0,esk15_0,esk17_0),X1)=esk15_0|~phtxt(esk12_3(esk18_0,esk15_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_104]), c_0_73]), c_0_116])])).
cnf(c_0_121, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|phtxt(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_63]), c_0_73])])).
cnf(c_0_122, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|ppt(X1,X2,esk17_0)|~txtdep(X1,esk11_3(esk18_0,esk15_0,esk17_0))|~txtdep(X2,esk12_3(esk18_0,esk15_0,esk17_0))), inference(spm,[status(thm)],[c_0_118, c_0_88])).
cnf(c_0_123, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|txtdep(esk18_0,esk11_3(esk18_0,esk15_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_119]), c_0_114])).
cnf(c_0_124, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|esk5_2(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)=esk15_0), inference(spm,[status(thm)],[c_0_120, c_0_121])).
cnf(c_0_125, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|ppt(esk18_0,X1,esk17_0)|~txtdep(X1,esk12_3(esk18_0,esk15_0,esk17_0))), inference(spm,[status(thm)],[c_0_122, c_0_123])).
cnf(c_0_126, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|txtdep(esk15_0,esk12_3(esk18_0,esk15_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_124]), c_0_121])).
cnf(c_0_127, plain, (phtxt(esk11_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)|~phtxt(esk11_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_94, c_0_65])).
cnf(c_0_128, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|ppt(esk18_0,esk15_0,esk17_0)), inference(spm,[status(thm)],[c_0_125, c_0_126])).
cnf(c_0_129, plain, (phtxt(esk11_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)|~txtdep(X4,esk11_3(X1,X2,X3))), inference(spm,[status(thm)],[c_0_127, c_0_101])).
cnf(c_0_130, negated_conjecture, (txtdep(esk18_0,esk12_3(esk18_0,esk15_0,esk17_0))|ppt(esk18_0,esk15_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_128]), c_0_73])])).
cnf(c_0_131, plain, (phtxt(esk11_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_129, c_0_56])).
cnf(c_0_132, negated_conjecture, (esk18_0=esk15_0|ppt(esk18_0,esk15_0,esk17_0)|~txt(esk15_0,X1)|~txt(esk18_0,X1)|~phtxt(esk12_3(esk18_0,esk15_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_130]), c_0_73])])).
cnf(c_0_133, negated_conjecture, (ppt(esk18_0,esk15_0,esk17_0)|phtxt(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131, c_0_128]), c_0_73])])).
cnf(c_0_134, plain, (ppt(X4,X2,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X3,X1,X5)), inference(split_conjunct,[status(thm)],[c_0_112])).
cnf(c_0_135, negated_conjecture, (esk18_0=esk15_0|ppt(esk18_0,esk15_0,esk17_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_116]), c_0_106])]), c_0_133])).
fof(c_0_136, plain, (![X5]:![X6]:((phtxt(esk6_2(X5,X6),X6)|~txt(X5,X6))&(txtdep(X5,esk6_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_14])])])])).
cnf(c_0_137, negated_conjecture, (esk18_0=esk15_0|ppt(X1,X2,esk17_0)|~txtdep(esk18_0,X1)|~txtdep(esk15_0,X2)), inference(spm,[status(thm)],[c_0_134, c_0_135])).
cnf(c_0_138, plain, (txtdep(X1,esk6_2(X1,X2))|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_136])).
cnf(c_0_139, negated_conjecture, (esk18_0=esk15_0|ppt(esk6_2(esk18_0,X1),X2,esk17_0)|~txtdep(esk15_0,X2)|~txt(esk18_0,X1)), inference(spm,[status(thm)],[c_0_137, c_0_138])).
cnf(c_0_140, negated_conjecture, (esk18_0=esk15_0|ppt(esk6_2(esk18_0,X1),esk6_2(esk15_0,X2),esk17_0)|~txt(esk18_0,X1)|~txt(esk15_0,X2)), inference(spm,[status(thm)],[c_0_139, c_0_138])).
cnf(c_0_141, negated_conjecture, (esk18_0=esk15_0|ppt(esk6_2(esk18_0,esk17_0),esk6_2(esk15_0,X1),esk17_0)|~txt(esk15_0,X1)), inference(spm,[status(thm)],[c_0_140, c_0_106])).
cnf(c_0_142, negated_conjecture, (txtoverlap(esk15_0,esk16_0,esk17_0)|txtpt(esk18_0,esk16_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
cnf(c_0_143, plain, (X1=X2|~txtdep(X1,esk6_2(X2,X3))|~txt(X2,X4)|~txt(X1,X4)|~txt(X2,X3)|~phtxt(esk6_2(X2,X3),X4)), inference(spm,[status(thm)],[c_0_83, c_0_138])).
cnf(c_0_144, negated_conjecture, (esk18_0=esk15_0|ppt(esk6_2(esk18_0,esk17_0),esk6_2(esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_141, c_0_116])).
cnf(c_0_145, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtpt(X1,esk15_0,esk17_0)|~txtpt(X1,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_27, c_0_142])).
cnf(c_0_146, plain, (esk5_2(esk6_2(X1,X2),X3)=X1|~txt(esk5_2(esk6_2(X1,X2),X3),X4)|~txt(X1,X4)|~txt(X1,X2)|~phtxt(esk6_2(X1,X2),X4)|~phtxt(esk6_2(X1,X2),X3)), inference(spm,[status(thm)],[c_0_143, c_0_30])).
cnf(c_0_147, negated_conjecture, (esk18_0=esk15_0|present(esk6_2(esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_48, c_0_144])).
cnf(c_0_148, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtpt(esk5_2(esk2_3(X1,X2,esk17_0),X3),esk16_0,esk17_0)|~txtdep(esk15_0,X2)|~phoverlap(X1,X2,esk17_0)|~phtxt(esk2_3(X1,X2,esk17_0),X3)), inference(spm,[status(thm)],[c_0_145, c_0_33])).
cnf(c_0_149, plain, (esk5_2(esk6_2(X1,X2),X3)=X1|~txt(X1,X4)|~txt(X1,X2)|~present(esk6_2(X1,X2),X4)|~phtxt(esk6_2(X1,X2),X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_146, c_0_98]), c_0_94])).
cnf(c_0_150, negated_conjecture, (esk18_0=esk15_0|phtxt(esk6_2(esk15_0,esk17_0),esk17_0)|~phtxt(esk6_2(esk15_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_147])).
cnf(c_0_151, plain, (phtxt(esk6_2(X1,X2),X2)|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_136])).
cnf(c_0_152, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)|~phoverlap(X2,X1,esk17_0)|~phtxt(esk2_3(X2,X1,esk17_0),X3)), inference(spm,[status(thm)],[c_0_148, c_0_37])).
cnf(c_0_153, plain, (present(X1,X2)|~phoverlap(X3,X1,X2)), inference(spm,[status(thm)],[c_0_54, c_0_24])).
cnf(c_0_154, negated_conjecture, (esk5_2(esk6_2(esk15_0,esk17_0),X1)=esk15_0|esk18_0=esk15_0|~phtxt(esk6_2(esk15_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_147]), c_0_116])])).
cnf(c_0_155, negated_conjecture, (esk18_0=esk15_0|phtxt(esk6_2(esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_151]), c_0_116])])).
cnf(c_0_156, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)|~phoverlap(X2,X1,esk17_0)), inference(spm,[status(thm)],[c_0_152, c_0_44])).
cnf(c_0_157, plain, (present(X1,X2)|~txtoverlap(X3,X1,X4)|~present(esk14_3(X3,X1,X4),X2)), inference(spm,[status(thm)],[c_0_55, c_0_60])).
cnf(c_0_158, plain, (present(esk14_3(X1,X2,X3),X3)|~txtoverlap(X1,X2,X3)), inference(spm,[status(thm)],[c_0_153, c_0_46])).
cnf(c_0_159, negated_conjecture, (esk5_2(esk6_2(esk15_0,esk17_0),esk17_0)=esk15_0|esk18_0=esk15_0), inference(spm,[status(thm)],[c_0_154, c_0_155])).
cnf(c_0_160, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtoverlap(X1,X2,esk17_0)|~txtdep(esk15_0,esk13_3(X1,X2,esk17_0))|~txtdep(esk16_0,esk14_3(X1,X2,esk17_0))), inference(spm,[status(thm)],[c_0_156, c_0_53])).
cnf(c_0_161, plain, (present(X1,X2)|~txtoverlap(X3,X1,X2)), inference(spm,[status(thm)],[c_0_157, c_0_158])).
fof(c_0_162, plain, (![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X13]:(((pt(esk1_3(X6,X7,X8),X6,X8)|~overlap(X6,X7,X8))&(pt(esk1_3(X6,X7,X8),X7,X8)|~overlap(X6,X7,X8)))&((~pt(X13,X10,X12)|~pt(X13,X11,X12))|overlap(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_15])])])])])])).
cnf(c_0_163, negated_conjecture, (esk18_0=esk15_0|ppt(esk11_3(esk18_0,X1,X2),X3,esk17_0)|~txtpt(esk18_0,X1,X2)|~txtdep(esk15_0,X3)), inference(spm,[status(thm)],[c_0_137, c_0_56])).
cnf(c_0_164, negated_conjecture, (esk18_0=esk15_0|txtdep(esk15_0,esk6_2(esk15_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_159]), c_0_155])).
cnf(c_0_165, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|~txtoverlap(X1,esk16_0,esk17_0)|~txtdep(esk15_0,esk13_3(X1,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_160, c_0_60])).
cnf(c_0_166, negated_conjecture, (present(esk16_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_161, c_0_142]), c_0_76])).
cnf(c_0_167, plain, (overlap(X1,X2,X3)|~pt(X4,X2,X3)|~pt(X4,X1,X3)), inference(split_conjunct,[status(thm)],[c_0_162])).
cnf(c_0_168, plain, (pt(X1,X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_41])).
cnf(c_0_169, negated_conjecture, (esk18_0=esk15_0|ppt(esk11_3(esk18_0,X1,X2),esk6_2(esk15_0,esk17_0),esk17_0)|~txtpt(esk18_0,X1,X2)), inference(spm,[status(thm)],[c_0_163, c_0_164])).
cnf(c_0_170, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_165, c_0_61]), c_0_142])).
cnf(c_0_171, negated_conjecture, (txt(esk16_0,esk17_0)|~txt(esk16_0,X1)), inference(spm,[status(thm)],[c_0_78, c_0_166])).
cnf(c_0_172, plain, (overlap(X1,X2,X3)|~ppt(X4,X2,X3)|~pt(X4,X1,X3)), inference(spm,[status(thm)],[c_0_167, c_0_168])).
cnf(c_0_173, negated_conjecture, (esk18_0=esk15_0|ppt(esk11_3(esk18_0,esk16_0,esk17_0),esk6_2(esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_169, c_0_170])).
cnf(c_0_174, negated_conjecture, (txt(esk16_0,esk17_0)|~txtdep(esk16_0,X1)), inference(spm,[status(thm)],[c_0_171, c_0_86])).
cnf(c_0_175, plain, (pt(esk1_3(X1,X2,X3),X1,X3)|~overlap(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_162])).
cnf(c_0_176, negated_conjecture, (esk18_0=esk15_0|overlap(X1,esk6_2(esk15_0,esk17_0),esk17_0)|~pt(esk11_3(esk18_0,esk16_0,esk17_0),X1,esk17_0)), inference(spm,[status(thm)],[c_0_172, c_0_173])).
cnf(c_0_177, negated_conjecture, (txt(esk16_0,esk17_0)|~txtoverlap(X1,esk16_0,X2)), inference(spm,[status(thm)],[c_0_174, c_0_60])).
cnf(c_0_178, plain, (present(X1,X2)|~overlap(X1,X3,X2)), inference(spm,[status(thm)],[c_0_54, c_0_175])).
cnf(c_0_179, negated_conjecture, (esk18_0=esk15_0|overlap(esk12_3(esk18_0,esk16_0,esk17_0),esk6_2(esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176, c_0_58]), c_0_170])])).
cnf(c_0_180, plain, (phtxt(esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)|~phtxt(esk12_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_94, c_0_70])).
cnf(c_0_181, plain, (phpt(X1,X2,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_16])).
cnf(c_0_182, negated_conjecture, (txt(esk16_0,esk17_0)|~txtpt(X1,esk16_0,X2)), inference(spm,[status(thm)],[c_0_174, c_0_63])).
cnf(c_0_183, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|txt(esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_177, c_0_142])).
cnf(c_0_184, negated_conjecture, (esk18_0=esk15_0|present(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_178, c_0_179])).
cnf(c_0_185, plain, (phtxt(esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)|~txtdep(X4,esk12_3(X1,X2,X3))), inference(spm,[status(thm)],[c_0_180, c_0_101])).
cnf(c_0_186, plain, (phoverlap(X1,X2,X3)|~phpt(X4,X1,X3)|~pt(X4,X2,X3)|~phtxt(X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_181]), c_0_38])).
cnf(c_0_187, negated_conjecture, (txt(esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_182, c_0_183])).
cnf(c_0_188, negated_conjecture, (esk18_0=esk15_0|phtxt(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)|~phtxt(esk12_3(esk18_0,esk16_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_184])).
cnf(c_0_189, plain, (phtxt(esk12_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(spm,[status(thm)],[c_0_185, c_0_63])).
cnf(c_0_190, plain, (phoverlap(X1,X2,X3)|~pt(X4,X2,X3)|~pt(X4,X1,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)|~phtxt(X4,X3)), inference(spm,[status(thm)],[c_0_186, c_0_181])).
cnf(c_0_191, negated_conjecture, (esk5_2(esk12_3(esk18_0,esk16_0,esk17_0),X1)=esk16_0|esk18_0=esk15_0|~phtxt(esk12_3(esk18_0,esk16_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_184]), c_0_170]), c_0_187])])).
cnf(c_0_192, negated_conjecture, (esk18_0=esk15_0|phtxt(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188, c_0_189]), c_0_170])])).
cnf(c_0_193, plain, (txtoverlap(X1,X2,X3)|~phoverlap(X4,X5,X3)|~txtdep(X2,X5)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_40])).
cnf(c_0_194, plain, (phoverlap(X1,esk12_3(X2,X3,X4),X4)|~txtpt(X2,X3,X4)|~pt(esk11_3(X2,X3,X4),X1,X4)|~phtxt(X1,X4)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_190, c_0_58]), c_0_131]), c_0_189])).
cnf(c_0_195, negated_conjecture, (esk5_2(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)=esk16_0|esk18_0=esk15_0), inference(spm,[status(thm)],[c_0_191, c_0_192])).
cnf(c_0_196, plain, (txtoverlap(X1,X2,X3)|~txtpt(X4,X5,X3)|~txtdep(X2,esk12_3(X4,X5,X3))|~txtdep(X1,X6)|~pt(esk11_3(X4,X5,X3),X6,X3)|~phtxt(X6,X3)), inference(spm,[status(thm)],[c_0_193, c_0_194])).
cnf(c_0_197, negated_conjecture, (esk18_0=esk15_0|txtdep(esk16_0,esk12_3(esk18_0,esk16_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_195]), c_0_192])).
cnf(c_0_198, negated_conjecture, (esk18_0=esk15_0|txtoverlap(X1,esk16_0,esk17_0)|~txtdep(X1,X2)|~pt(esk11_3(esk18_0,esk16_0,esk17_0),X2,esk17_0)|~phtxt(X2,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196, c_0_197]), c_0_170])])).
cnf(c_0_199, negated_conjecture, (esk18_0=esk15_0|txtoverlap(X1,esk16_0,esk17_0)|~txtdep(X1,esk6_2(esk15_0,esk17_0))|~pt(esk11_3(esk18_0,esk16_0,esk17_0),esk6_2(esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_198, c_0_155])).
cnf(c_0_200, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|ppt(esk11_3(esk18_0,esk16_0,esk17_0),esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_81, c_0_170])).
cnf(c_0_201, negated_conjecture, (esk18_0=esk15_0|txtoverlap(X1,esk16_0,esk17_0)|~txtdep(X1,esk6_2(esk15_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_199, c_0_168]), c_0_173])).
cnf(c_0_202, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|present(esk11_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_51, c_0_200])).
cnf(c_0_203, negated_conjecture, (esk18_0=esk15_0|txtoverlap(esk15_0,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_201, c_0_164])).
cnf(c_0_204, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|phtxt(esk11_3(esk18_0,esk16_0,esk17_0),esk17_0)|~phtxt(esk11_3(esk18_0,esk16_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_202])).
cnf(c_0_205, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|present(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_48, c_0_200])).
cnf(c_0_206, negated_conjecture, (esk18_0=esk15_0|~txtpt(X1,esk15_0,esk17_0)|~txtpt(X1,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_27, c_0_203])).
cnf(c_0_207, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|esk5_2(esk11_3(esk18_0,esk16_0,esk17_0),X1)=esk18_0|~phtxt(esk11_3(esk18_0,esk16_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_202]), c_0_170]), c_0_106])])).
cnf(c_0_208, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|phtxt(esk11_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_204, c_0_131]), c_0_170])])).
cnf(c_0_209, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|phtxt(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)|~phtxt(esk12_3(esk18_0,esk16_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_205])).
cnf(c_0_210, plain, (pt(X1,X2,X3)|~present(X2,X3)|~present(X1,X3)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_41])).
cnf(c_0_211, negated_conjecture, (esk18_0=esk15_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_206, c_0_170]), c_0_73])])).
cnf(c_0_212, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|esk5_2(esk11_3(esk18_0,esk16_0,esk17_0),esk17_0)=esk18_0), inference(spm,[status(thm)],[c_0_207, c_0_208])).
cnf(c_0_213, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|esk5_2(esk12_3(esk18_0,esk16_0,esk17_0),X1)=esk16_0|~phtxt(esk12_3(esk18_0,esk16_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_205]), c_0_170]), c_0_187])])).
cnf(c_0_214, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|phtxt(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_209, c_0_189]), c_0_170])])).
cnf(c_0_215, plain, (phoverlap(X1,X2,X3)|~phoverlap(X4,X2,X3)|~phpt(esk2_3(X4,X2,X3),X1,X3)), inference(spm,[status(thm)],[c_0_35, c_0_21])).
cnf(c_0_216, plain, (pt(X1,X1,X2)|~present(X1,X2)), inference(er,[status(thm)],[c_0_210])).
cnf(c_0_217, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|ppt(esk11_3(esk15_0,esk16_0,esk17_0),esk12_3(esk15_0,esk16_0,esk17_0),esk17_0)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_200, c_0_211]), c_0_211]), c_0_211]), c_0_211])).
cnf(c_0_218, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|txtdep(esk18_0,esk11_3(esk18_0,esk16_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_212]), c_0_208])).
cnf(c_0_219, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|esk5_2(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)=esk16_0), inference(spm,[status(thm)],[c_0_213, c_0_214])).
cnf(c_0_220, plain, (phoverlap(X1,X1,X2)|~phoverlap(X3,X1,X2)), inference(spm,[status(thm)],[c_0_215, c_0_21])).
cnf(c_0_221, plain, (phoverlap(X1,X2,X3)|~pt(X2,X1,X3)|~phtxt(X2,X3)|~phtxt(X1,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_190, c_0_216]), c_0_57])).
cnf(c_0_222, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|ppt(X1,X2,esk17_0)|~txtdep(X1,esk11_3(esk15_0,esk16_0,esk17_0))|~txtdep(X2,esk12_3(esk15_0,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_118, c_0_217])).
cnf(c_0_223, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|txtdep(esk15_0,esk11_3(esk15_0,esk16_0,esk17_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_218, c_0_211]), c_0_211]), c_0_211]), c_0_211])).
cnf(c_0_224, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|txtdep(esk16_0,esk12_3(esk18_0,esk16_0,esk17_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_219]), c_0_214])).
cnf(c_0_225, plain, (phoverlap(X1,X1,X2)|~pt(X1,X3,X2)|~phtxt(X1,X2)|~phtxt(X3,X2)), inference(spm,[status(thm)],[c_0_220, c_0_221])).
cnf(c_0_226, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|ppt(esk15_0,X1,esk17_0)|~txtdep(X1,esk12_3(esk15_0,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_222, c_0_223])).
cnf(c_0_227, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|txtdep(esk16_0,esk12_3(esk15_0,esk16_0,esk17_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_224, c_0_211]), c_0_211]), c_0_211])).
cnf(c_0_228, plain, (phoverlap(esk11_3(X1,X2,X3),esk11_3(X1,X2,X3),X3)|~txtpt(X1,X2,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_225, c_0_58]), c_0_189]), c_0_131])).
cnf(c_0_229, negated_conjecture, (esk11_3(esk15_0,esk16_0,esk17_0)=esk12_3(esk15_0,esk16_0,esk17_0)|ppt(esk15_0,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_226, c_0_227])).
cnf(c_0_230, negated_conjecture, (txtpt(esk15_0,esk16_0,esk17_0)), inference(rw,[status(thm)],[c_0_170, c_0_211])).
cnf(c_0_231, negated_conjecture, (phoverlap(esk12_3(esk15_0,esk16_0,esk17_0),esk12_3(esk15_0,esk16_0,esk17_0),esk17_0)|ppt(esk15_0,esk16_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_228, c_0_229]), c_0_230])])).
cnf(c_0_232, plain, (txtpt(X1,X2,X3)|~txtdep(X2,X4)|~txtdep(X1,X4)|~present(X4,X3)), inference(spm,[status(thm)],[c_0_23, c_0_216])).
cnf(c_0_233, plain, (txtoverlap(X1,X2,X3)|~txtoverlap(X4,X5,X3)|~txtdep(X2,esk13_3(X4,X5,X3))|~txtdep(X1,esk14_3(X4,X5,X3))), inference(spm,[status(thm)],[c_0_193, c_0_53])).
cnf(c_0_234, negated_conjecture, (txtoverlap(X1,X2,esk17_0)|ppt(esk15_0,esk16_0,esk17_0)|~txtdep(X2,esk12_3(esk15_0,esk16_0,esk17_0))|~txtdep(X1,esk12_3(esk15_0,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_193, c_0_231])).
cnf(c_0_235, negated_conjecture, (txtdep(esk15_0,esk12_3(esk15_0,esk16_0,esk17_0))|ppt(esk15_0,esk16_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_229]), c_0_230])])).
cnf(c_0_236, plain, (txtpt(X1,X2,X3)|~txtpt(X4,X2,X5)|~txtdep(X1,esk12_3(X4,X2,X5))|~present(esk12_3(X4,X2,X5),X3)), inference(spm,[status(thm)],[c_0_232, c_0_63])).
cnf(c_0_237, plain, (txtoverlap(X1,X2,X3)|~txtoverlap(X2,X4,X3)|~txtdep(X1,esk14_3(X2,X4,X3))), inference(spm,[status(thm)],[c_0_233, c_0_61])).
cnf(c_0_238, negated_conjecture, (txtoverlap(X1,esk15_0,esk17_0)|ppt(esk15_0,esk16_0,esk17_0)|~txtdep(X1,esk12_3(esk15_0,esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_234, c_0_235])).
cnf(c_0_239, plain, (txtpt(X1,X1,X2)|~txtpt(X3,X1,X4)|~present(esk12_3(X3,X1,X4),X2)), inference(spm,[status(thm)],[c_0_236, c_0_63])).
cnf(c_0_240, plain, (txtoverlap(X1,X2,X3)|~txtoverlap(X2,X1,X3)), inference(spm,[status(thm)],[c_0_237, c_0_60])).
cnf(c_0_241, negated_conjecture, (txtoverlap(esk16_0,esk15_0,esk17_0)|ppt(esk15_0,esk16_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_238, c_0_63]), c_0_230])])).
cnf(c_0_242, negated_conjecture, (esk11_3(esk18_0,esk15_0,esk17_0)=esk12_3(esk18_0,esk15_0,esk17_0)|txtpt(esk15_0,esk15_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_239, c_0_104]), c_0_73])])).
cnf(c_0_243, plain, (txtpt(X1,X2,X3)|~txtoverlap(X4,X2,X5)|~txtdep(X1,esk14_3(X4,X2,X5))|~present(esk14_3(X4,X2,X5),X3)), inference(spm,[status(thm)],[c_0_232, c_0_60])).
cnf(c_0_244, negated_conjecture, (txtoverlap(esk15_0,esk16_0,esk17_0)|ppt(esk15_0,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_240, c_0_241])).
cnf(c_0_245, negated_conjecture, (txtpt(esk15_0,esk15_0,esk17_0)|present(esk12_3(esk18_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_242]), c_0_73])])).
cnf(c_0_246, plain, (txtpt(X1,X1,X2)|~txtoverlap(X3,X1,X4)|~present(esk14_3(X3,X1,X4),X2)), inference(spm,[status(thm)],[c_0_243, c_0_60])).
cnf(c_0_247, negated_conjecture, (ppt(esk15_0,esk16_0,esk17_0)|~txtpt(X1,esk15_0,esk17_0)|~txtpt(X1,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_27, c_0_244])).
cnf(c_0_248, negated_conjecture, (txtpt(esk15_0,esk15_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_239, c_0_245]), c_0_73])])).
cnf(c_0_249, plain, (txtpt(X1,X1,X2)|~txtoverlap(X3,X1,X2)), inference(spm,[status(thm)],[c_0_246, c_0_158])).
cnf(c_0_250, negated_conjecture, (ppt(esk15_0,esk16_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_247, c_0_230]), c_0_248])])).
cnf(c_0_251, negated_conjecture, (txtpt(esk18_0,esk16_0,esk17_0)|txtpt(esk16_0,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_249, c_0_142])).
cnf(c_0_252, negated_conjecture, (ppt(X1,X2,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)), inference(spm,[status(thm)],[c_0_134, c_0_250])).
cnf(c_0_253, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|txtpt(esk16_0,esk16_0,esk17_0)|ppt(esk11_3(esk18_0,esk16_0,esk17_0),esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_81, c_0_251])).
cnf(c_0_254, negated_conjecture, (present(X1,esk17_0)|~txtdep(esk15_0,X1)|~txtdep(esk16_0,X2)), inference(spm,[status(thm)],[c_0_51, c_0_252])).
cnf(c_0_255, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|txtpt(esk16_0,esk16_0,esk17_0)|present(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_48, c_0_253])).
cnf(c_0_256, plain, (X1=esk5_2(X2,X3)|~txtdep(X1,X2)|~txt(esk5_2(X2,X3),X4)|~txt(X1,X4)|~phtxt(X2,X4)|~phtxt(X2,X3)), inference(spm,[status(thm)],[c_0_83, c_0_30])).
cnf(c_0_257, negated_conjecture, (present(esk12_3(X1,esk15_0,X2),esk17_0)|~txtpt(X1,esk15_0,X2)|~txtdep(esk16_0,X3)), inference(spm,[status(thm)],[c_0_254, c_0_63])).
cnf(c_0_258, negated_conjecture, (esk11_3(esk18_0,esk16_0,esk17_0)=esk12_3(esk18_0,esk16_0,esk17_0)|txtpt(esk16_0,esk16_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_239, c_0_255]), c_0_251])).
cnf(c_0_259, plain, (X1=esk5_2(X2,X3)|~txtdep(X1,X2)|~txt(X1,X3)|~phtxt(X2,X3)), inference(spm,[status(thm)],[c_0_256, c_0_92])).
cnf(c_0_260, negated_conjecture, (present(esk12_3(X1,esk15_0,X2),esk17_0)|~txtpt(X1,esk15_0,X2)|~txtpt(X3,esk16_0,X4)), inference(spm,[status(thm)],[c_0_257, c_0_63])).
cnf(c_0_261, negated_conjecture, (txtpt(esk16_0,esk16_0,esk17_0)|present(esk12_3(esk18_0,esk16_0,esk17_0),esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_258]), c_0_251])).
cnf(c_0_262, plain, (esk5_2(X1,X2)=esk5_2(X1,X3)|~txt(esk5_2(X1,X2),X3)|~phtxt(X1,X3)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_259, c_0_30])).
cnf(c_0_263, negated_conjecture, (present(esk12_3(esk15_0,esk15_0,esk17_0),esk17_0)|~txtpt(X1,esk16_0,X2)), inference(spm,[status(thm)],[c_0_260, c_0_248])).
cnf(c_0_264, negated_conjecture, (txtpt(esk16_0,esk16_0,esk17_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_239, c_0_261]), c_0_251])).
cnf(c_0_265, negated_conjecture, (present(X1,esk17_0)|~txtdep(esk15_0,X2)|~txtdep(esk16_0,X1)), inference(spm,[status(thm)],[c_0_48, c_0_252])).
cnf(c_0_266, plain, (esk5_2(X1,X2)=esk5_2(X1,X3)|~present(X1,X3)|~phtxt(X1,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_262, c_0_98]), c_0_94])).
cnf(c_0_267, negated_conjecture, (present(esk12_3(esk15_0,esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_263, c_0_264])).
cnf(c_0_268, negated_conjecture, (present(X1,esk17_0)|~txtpt(X2,esk15_0,X3)|~txtdep(esk16_0,X1)), inference(spm,[status(thm)],[c_0_265, c_0_63])).
cnf(c_0_269, negated_conjecture, (present(esk11_3(esk15_0,X1,X2),esk17_0)|~txtpt(esk15_0,X1,X2)|~txtdep(esk16_0,X3)), inference(spm,[status(thm)],[c_0_254, c_0_56])).
cnf(c_0_270, plain, (txtdep(esk5_2(X1,X2),X1)|~present(X1,X2)|~phtxt(X1,X3)), inference(spm,[status(thm)],[c_0_30, c_0_266])).
cnf(c_0_271, negated_conjecture, (phtxt(esk12_3(esk15_0,esk15_0,esk17_0),esk17_0)|~phtxt(esk12_3(esk15_0,esk15_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_267])).
cnf(c_0_272, negated_conjecture, (present(esk6_2(esk16_0,X1),esk17_0)|~txtpt(X2,esk15_0,X3)|~txt(esk16_0,X1)), inference(spm,[status(thm)],[c_0_268, c_0_138])).
cnf(c_0_273, negated_conjecture, (present(esk11_3(esk15_0,X1,X2),esk17_0)|~txtpt(esk15_0,X1,X2)|~txtpt(X3,esk16_0,X4)), inference(spm,[status(thm)],[c_0_269, c_0_63])).
cnf(c_0_274, plain, (txtdep(esk5_2(esk12_3(X1,X2,X3),X3),esk12_3(X1,X2,X3))|~txtpt(X1,X2,X3)|~phtxt(esk12_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_270, c_0_70])).
cnf(c_0_275, negated_conjecture, (phtxt(esk12_3(esk15_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_271, c_0_189]), c_0_248])])).
cnf(c_0_276, negated_conjecture, (present(esk6_2(esk16_0,esk17_0),esk17_0)|~txtpt(X1,esk15_0,X2)), inference(spm,[status(thm)],[c_0_272, c_0_187])).
cnf(c_0_277, negated_conjecture, (present(esk11_3(esk15_0,esk15_0,esk17_0),esk17_0)|~txtpt(X1,esk16_0,X2)), inference(spm,[status(thm)],[c_0_273, c_0_248])).
cnf(c_0_278, negated_conjecture, (txtdep(esk5_2(esk12_3(esk15_0,esk15_0,esk17_0),esk17_0),esk12_3(esk15_0,esk15_0,esk17_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_274, c_0_275]), c_0_248])])).
cnf(c_0_279, plain, (esk5_2(esk12_3(X1,X2,X3),X4)=X2|~txtpt(X1,X2,X3)|~txt(X2,X4)|~phtxt(esk12_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_259, c_0_63])).
cnf(c_0_280, negated_conjecture, (present(esk6_2(esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_276, c_0_248])).
cnf(c_0_281, negated_conjecture, (present(esk11_3(esk15_0,esk15_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_277, c_0_264])).
cnf(c_0_282, negated_conjecture, (txtdep(esk15_0,esk12_3(esk15_0,esk15_0,esk17_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_278, c_0_279]), c_0_248]), c_0_116]), c_0_275])])).
cnf(c_0_283, negated_conjecture, (phtxt(esk6_2(esk16_0,esk17_0),esk17_0)|~phtxt(esk6_2(esk16_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_280])).
cnf(c_0_284, negated_conjecture, (phtxt(esk11_3(esk15_0,esk15_0,esk17_0),esk17_0)|~phtxt(esk11_3(esk15_0,esk15_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_94, c_0_281])).
cnf(c_0_285, negated_conjecture, (txtoverlap(X1,esk15_0,esk17_0)|~txtdep(X1,X2)|~pt(esk11_3(esk15_0,esk15_0,esk17_0),X2,esk17_0)|~phtxt(X2,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196, c_0_282]), c_0_248])])).
cnf(c_0_286, negated_conjecture, (phtxt(esk6_2(esk16_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_283, c_0_151]), c_0_187])])).
cnf(c_0_287, plain, (txtdep(esk5_2(esk11_3(X1,X2,X3),X3),esk11_3(X1,X2,X3))|~txtpt(X1,X2,X3)|~phtxt(esk11_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_270, c_0_65])).
cnf(c_0_288, negated_conjecture, (phtxt(esk11_3(esk15_0,esk15_0,esk17_0),esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_284, c_0_131]), c_0_248])])).
cnf(c_0_289, negated_conjecture, (esk5_2(esk6_2(esk16_0,esk17_0),X1)=esk16_0|~phtxt(esk6_2(esk16_0,esk17_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_280]), c_0_187])])).
cnf(c_0_290, negated_conjecture, (txtoverlap(X1,esk15_0,esk17_0)|~txtdep(X1,esk6_2(esk16_0,esk17_0))|~pt(esk11_3(esk15_0,esk15_0,esk17_0),esk6_2(esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_285, c_0_286])).
cnf(c_0_291, negated_conjecture, (txtdep(esk5_2(esk11_3(esk15_0,esk15_0,esk17_0),esk17_0),esk11_3(esk15_0,esk15_0,esk17_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_287, c_0_288]), c_0_248])])).
cnf(c_0_292, plain, (esk5_2(esk11_3(X1,X2,X3),X4)=X1|~txtpt(X1,X2,X3)|~txt(X1,X4)|~phtxt(esk11_3(X1,X2,X3),X4)), inference(spm,[status(thm)],[c_0_259, c_0_56])).
cnf(c_0_293, negated_conjecture, (txtdep(esk16_0,esk6_2(esk16_0,esk17_0))|~phtxt(esk6_2(esk16_0,esk17_0),X1)), inference(spm,[status(thm)],[c_0_30, c_0_289])).
cnf(c_0_294, negated_conjecture, (txtoverlap(X1,esk15_0,esk17_0)|~txtdep(X1,esk6_2(esk16_0,esk17_0))|~ppt(esk11_3(esk15_0,esk15_0,esk17_0),esk6_2(esk16_0,esk17_0),esk17_0)), inference(spm,[status(thm)],[c_0_290, c_0_168])).
cnf(c_0_295, negated_conjecture, (txtdep(esk15_0,esk11_3(esk15_0,esk15_0,esk17_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_291, c_0_292]), c_0_248]), c_0_116]), c_0_288])])).
cnf(c_0_296, negated_conjecture, (txtdep(esk16_0,esk6_2(esk16_0,esk17_0))), inference(spm,[status(thm)],[c_0_293, c_0_286])).
cnf(c_0_297, negated_conjecture, (txtoverlap(X1,esk15_0,esk17_0)|~txtdep(X1,esk6_2(esk16_0,esk17_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_294, c_0_252]), c_0_295]), c_0_296])])).
cnf(c_0_298, negated_conjecture, (txtoverlap(esk16_0,esk15_0,esk17_0)), inference(spm,[status(thm)],[c_0_297, c_0_296])).
cnf(c_0_299, negated_conjecture, (txtoverlap(esk15_0,esk16_0,esk17_0)), inference(spm,[status(thm)],[c_0_240, c_0_298])).
cnf(c_0_300, negated_conjecture, (~txtpt(X1,esk15_0,esk17_0)|~txtpt(X1,esk16_0,esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_299])])).
cnf(c_0_301, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_300, c_0_230]), c_0_248])]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 148.769 s
# System time              : 0.281 s
# Total time               : 149.050 s
# Maximum resident set size: 1752 pages

% END OF SYSTEM OUTPUT
% RESULT: SOT_T54nMk - E---1.9.1 says Theorem - CPU = 148.99 WC = 149.02 
% OUTPUT: SOT_T54nMk - E---1.9.1 says CNFRefutation - CPU = 148.99 WC = 149.02