% 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___107_B42_F1_PI_AE_Q4_CS_SP_PS_S0Y
# and selection function SelectMaxLComplexAvoidPosPred.
#
# Preprocessing time       : 0.022 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(c_0_0, conjecture, (![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)<=>((ppt(X1,X4,X2)&txt(X1,X2))&txt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', conjectureXVII)).
fof(c_0_1, axiom, (![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)<=>?[X15]:?[X17]:((txtdep(X1,X15)&txtdep(X4,X17))&ppt(X15,X17,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom68)).
fof(c_0_2, axiom, (![X15]:![X17]:![X16]:![X18]:![X2]:((txtdep(X15,X17)&txtdep(X16,X18))=>(ppt(X15,X16,X2)<=>ppt(X17,X18,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom63)).
fof(c_0_3, axiom, (![X1]:![X2]:(txt(X1,X2)=>?[X4]:(phtxt(X4,X2)&txtdep(X1,X4)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom58)).
fof(c_0_4, axiom, (![X1]:![X2]:(txt(X1,X2)=>![X3]:(present(X1,X3)=>txt(X1,X3)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom3)).
fof(c_0_5, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>(?[X2]:txt(X1,X2)&?[X2]:phtxt(X4,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom56)).
fof(c_0_6, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>(present(X1,X2)&present(X4,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom7)).
fof(c_0_7, axiom, (![X1]:![X4]:(txtdep(X1,X4)=>![X2]:(present(X4,X2)=>present(X1,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom61)).
fof(c_0_8, axiom, (![X1]:![X2]:![X4]:![X3]:(phtxtequiv(X1,X2,X4,X3)=>(present(X1,X2)&present(X4,X3)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom48)).
fof(c_0_9, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>phtxtequiv(X1,X2,X1,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom49)).
fof(c_0_10, axiom, (![X1]:![X17]:![X18]:((txtdep(X1,X17)&txtdep(X1,X18))=>![X3]:![X13]:((present(X17,X3)&present(X18,X13))=>phtxtequiv(X17,X3,X18,X13)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom59)).
fof(c_0_11, axiom, (![X7]:![X8]:![X2]:(occ(X7,X8,X2)=>((nontime(X7)®(X8))&time(X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiomCIV)).
fof(c_0_12, axiom, (![X1]:![X2]:(phtxt(X1,X2)=>?[X8]:occ(X1,X8,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom28)).
fof(c_0_13, axiom, (![X1]:![X4]:![X2]:(pt(X1,X4,X2)<=>(ppt(X1,X4,X2)|((X1=X4&present(X1,X2))&present(X4,X2))))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', definition4)).
fof(c_0_14, axiom, (![X1]:![X2]:![X5]:((txt(X1,X2)&ppt(X5,X1,X2))=>txt(X5,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom65)).
fof(c_0_15, axiom, (![X1]:?[X2]:(nontime(X1)=>present(X1,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom1)).
fof(c_0_16, axiom, (![X17]:![X3]:![X18]:![X13]:(phtxtequiv(X17,X3,X18,X13)=>![X5]:(txtdep(X5,X17)<=>txtdep(X5,X18)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom62)).
fof(c_0_17, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>((nontime(X1)&nontime(X4))&time(X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiomCV)).
fof(c_0_18, axiom, (![X1]:![X2]:(present(X1,X2)=>(nontime(X1)&time(X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiomCIII)).
fof(c_0_19, axiom, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>~(phtxtequiv(X1,X2,X4,X2)))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom52)).
fof(c_0_20, axiom, (![X1]:![X2]:~(ppt(X1,X1,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom8)).
fof(c_0_21, axiom, (![X1]:![X2]:![X4]:![X3]:(phtxtequiv(X1,X2,X4,X3)=>phtxtequiv(X4,X3,X1,X2))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom50)).
fof(c_0_22, axiom, (![X1]:![X3]:![X4]:![X13]:![X5]:![X14]:((phtxtequiv(X1,X3,X4,X13)&phtxtequiv(X4,X13,X5,X14))=>phtxtequiv(X1,X3,X5,X14))), file('/tmp/SystemOnTPTPFormReply36531/SOT_7mLMQO', axiom51)).
fof(c_0_23, negated_conjecture, (~(![X1]:![X4]:![X2]:(txtppt(X1,X4,X2)<=>((ppt(X1,X4,X2)&txt(X1,X2))&txt(X4,X2))))), inference(assume_negation,[status(cth)],[c_0_0])).
fof(c_0_24, plain, (![X18]:![X19]:![X20]:![X23]:![X24]:![X25]:![X26]:![X27]:((((txtdep(X18,esk34_3(X18,X19,X20))|~txtppt(X18,X19,X20))&(txtdep(X19,esk35_3(X18,X19,X20))|~txtppt(X18,X19,X20)))&(ppt(esk34_3(X18,X19,X20),esk35_3(X18,X19,X20),X20)|~txtppt(X18,X19,X20)))&(((~txtdep(X23,X26)|~txtdep(X24,X27))|~ppt(X26,X27,X25))|txtppt(X23,X24,X25)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])])])])).
fof(c_0_25, negated_conjecture, (((~txtppt(esk47_0,esk48_0,esk49_0)|((~ppt(esk47_0,esk48_0,esk49_0)|~txt(esk47_0,esk49_0))|~txt(esk48_0,esk49_0)))&(((ppt(esk47_0,esk48_0,esk49_0)|txtppt(esk47_0,esk48_0,esk49_0))&(txt(esk47_0,esk49_0)|txtppt(esk47_0,esk48_0,esk49_0)))&(txt(esk48_0,esk49_0)|txtppt(esk47_0,esk48_0,esk49_0))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])])])])).
fof(c_0_26, plain, (![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:(((~ppt(X19,X21,X23)|ppt(X20,X22,X23))|(~txtdep(X19,X20)|~txtdep(X21,X22)))&((~ppt(X20,X22,X24)|ppt(X19,X21,X24))|(~txtdep(X19,X20)|~txtdep(X21,X22))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])).
cnf(c_0_27, plain, (ppt(esk34_3(X1,X2,X3),esk35_3(X1,X2,X3),X3)|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_24])).
cnf(c_0_28, negated_conjecture, (txtppt(esk47_0,esk48_0,esk49_0)|ppt(esk47_0,esk48_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
fof(c_0_29, plain, (![X5]:![X6]:((phtxt(esk31_2(X5,X6),X6)|~txt(X5,X6))&(txtdep(X5,esk31_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_3])])])])).
cnf(c_0_30, plain, (txtdep(X1,esk34_3(X1,X2,X3))|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_24])).
cnf(c_0_31, negated_conjecture, (txtppt(esk47_0,esk48_0,esk49_0)|txt(esk48_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_32, plain, (ppt(X3,X1,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X4,X2,X5)), inference(split_conjunct,[status(thm)],[c_0_26])).
cnf(c_0_33, negated_conjecture, (ppt(esk34_3(esk47_0,esk48_0,esk49_0),esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|ppt(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
cnf(c_0_34, plain, (phtxt(esk31_2(X1,X2),X2)|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_29])).
cnf(c_0_35, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|txt(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
cnf(c_0_36, plain, (txtdep(X2,esk35_3(X1,X2,X3))|~txtppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_24])).
cnf(c_0_37, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|ppt(X1,X2,esk49_0)|~txtdep(X1,esk34_3(esk47_0,esk48_0,esk49_0))|~txtdep(X2,esk35_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
cnf(c_0_38, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
cnf(c_0_39, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|txt(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_36, c_0_31])).
cnf(c_0_40, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|ppt(esk47_0,X1,esk49_0)|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)|~txtdep(X1,esk35_3(esk47_0,esk48_0,esk49_0))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
cnf(c_0_41, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_34, c_0_39])).
fof(c_0_42, 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_4])])])])).
fof(c_0_43, plain, (![X5]:![X6]:((txt(X5,esk28_2(X5,X6))|~txtdep(X5,X6))&(phtxt(X6,esk29_2(X5,X6))|~txtdep(X5,X6)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])).
cnf(c_0_44, plain, (ppt(X4,X2,X5)|~txtdep(X1,X2)|~txtdep(X3,X4)|~ppt(X3,X1,X5)), inference(split_conjunct,[status(thm)],[c_0_26])).
cnf(c_0_45, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_40, c_0_41])).
cnf(c_0_46, plain, (txt(X1,X2)|~present(X1,X2)|~txt(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_42])).
cnf(c_0_47, plain, (txt(X1,esk28_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_43])).
fof(c_0_48, 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_6])])])).
cnf(c_0_49, negated_conjecture, (ppt(X1,X2,esk49_0)|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_45])).
cnf(c_0_50, plain, (txt(X1,X2)|~txtdep(X1,X3)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
fof(c_0_51, 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_7])])])).
cnf(c_0_52, plain, (present(X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_48])).
cnf(c_0_53, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|ppt(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_36, c_0_28])).
cnf(c_0_54, negated_conjecture, (ppt(esk34_3(esk47_0,esk48_0,esk49_0),X1,esk49_0)|phtxt(esk31_2(esk48_0,esk49_0),esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_49, c_0_38])).
cnf(c_0_55, plain, (txtdep(X1,esk31_2(X1,X2))|~txt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_29])).
cnf(c_0_56, negated_conjecture, (txt(esk48_0,X1)|~present(esk48_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_39]), c_0_50])).
cnf(c_0_57, plain, (present(X1,X2)|~present(X3,X2)|~txtdep(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_51])).
cnf(c_0_58, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|present(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_52, c_0_53])).
cnf(c_0_59, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_52, c_0_33])).
fof(c_0_60, plain, (![X5]:![X6]:![X7]:![X8]:((present(X5,X6)|~phtxtequiv(X5,X6,X7,X8))&(present(X7,X8)|~phtxtequiv(X5,X6,X7,X8)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])).
fof(c_0_61, plain, (![X3]:![X4]:(~phtxt(X3,X4)|phtxtequiv(X3,X4,X3,X4))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])).
fof(c_0_62, plain, (![X19]:![X20]:![X21]:![X22]:![X23]:((~txtdep(X19,X20)|~txtdep(X19,X21))|((~present(X20,X22)|~present(X21,X23))|phtxtequiv(X20,X22,X21,X23)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])).
cnf(c_0_63, negated_conjecture, (phtxt(esk31_2(esk48_0,esk49_0),esk49_0)|present(X1,esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_52, c_0_54])).
cnf(c_0_64, negated_conjecture, (txtdep(esk48_0,esk31_2(esk48_0,X1))|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_55, c_0_56])).
cnf(c_0_65, negated_conjecture, (present(esk48_0,esk49_0)|present(esk48_0,X1)|~present(esk35_3(esk47_0,esk48_0,esk49_0),X1)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
cnf(c_0_66, negated_conjecture, (present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|present(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_52, c_0_59])).
cnf(c_0_67, plain, (present(X3,X4)|~phtxtequiv(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_60])).
cnf(c_0_68, plain, (phtxtequiv(X1,X2,X1,X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_61])).
fof(c_0_69, plain, (![X9]:![X10]:![X11]:(((nontime(X9)|~occ(X9,X10,X11))&(reg(X10)|~occ(X9,X10,X11)))&(time(X11)|~occ(X9,X10,X11)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).
fof(c_0_70, plain, (![X9]:![X10]:(~phtxt(X9,X10)|occ(X9,esk17_2(X9,X10),X10))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])).
cnf(c_0_71, plain, (phtxtequiv(X1,X2,X3,X4)|~present(X3,X4)|~present(X1,X2)|~txtdep(X5,X3)|~txtdep(X5,X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
cnf(c_0_72, negated_conjecture, (phtxt(esk31_2(esk48_0,esk49_0),esk49_0)|present(esk31_2(esk48_0,X1),esk49_0)|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_63, c_0_64])).
cnf(c_0_73, negated_conjecture, (present(esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_65, c_0_66])).
cnf(c_0_74, plain, (present(X1,X2)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_67, c_0_68])).
cnf(c_0_75, plain, (nontime(X1)|~occ(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_69])).
cnf(c_0_76, plain, (occ(X1,esk17_2(X1,X2),X2)|~phtxt(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_70])).
fof(c_0_77, 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_13])])])])])).
fof(c_0_78, 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_14])])).
cnf(c_0_79, negated_conjecture, (phtxtequiv(X1,X2,esk31_2(esk48_0,X3),X4)|~txtdep(esk48_0,X1)|~present(esk31_2(esk48_0,X3),X4)|~present(esk48_0,X3)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_71, c_0_64])).
cnf(c_0_80, negated_conjecture, (present(esk31_2(esk48_0,esk49_0),esk49_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_74])).
fof(c_0_81, plain, (![X3]:(~nontime(X3)|present(X3,esk1_1(X3)))), 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_82, plain, (nontime(X1)|~phtxt(X1,X2)), inference(spm,[status(thm)],[c_0_75, c_0_76])).
cnf(c_0_83, plain, (phtxt(X2,esk29_2(X1,X2))|~txtdep(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_43])).
cnf(c_0_84, plain, (pt(X1,X2,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_77])).
cnf(c_0_85, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|ppt(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_30, c_0_28])).
cnf(c_0_86, plain, (txt(X1,X2)|~ppt(X1,X3,X2)|~txt(X3,X2)), inference(split_conjunct,[status(thm)],[c_0_78])).
cnf(c_0_87, negated_conjecture, (txtppt(esk47_0,esk48_0,esk49_0)|txt(esk47_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
fof(c_0_88, plain, (![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:(((~txtdep(X23,X19)|txtdep(X23,X21))|~phtxtequiv(X19,X20,X21,X22))&((~txtdep(X24,X21)|txtdep(X24,X19))|~phtxtequiv(X19,X20,X21,X22)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])])).
cnf(c_0_89, negated_conjecture, (phtxtequiv(X1,X2,esk31_2(esk48_0,esk49_0),esk49_0)|~txtdep(esk48_0,X1)|~present(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_80]), c_0_73])])).
cnf(c_0_90, plain, (present(X1,esk1_1(X1))|~nontime(X1)), inference(split_conjunct,[status(thm)],[c_0_81])).
cnf(c_0_91, plain, (nontime(X1)|~txtdep(X2,X1)), inference(spm,[status(thm)],[c_0_82, c_0_83])).
fof(c_0_92, plain, (![X5]:![X6]:![X7]:(((nontime(X5)|~ppt(X5,X6,X7))&(nontime(X6)|~ppt(X5,X6,X7)))&(time(X7)|~ppt(X5,X6,X7)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])])).
cnf(c_0_93, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|pt(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_84, c_0_85])).
cnf(c_0_94, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|txt(esk47_0,esk49_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_85]), c_0_35])).
cnf(c_0_95, plain, (present(X1,X3)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_48])).
cnf(c_0_96, negated_conjecture, (ppt(esk34_3(esk47_0,esk48_0,esk49_0),esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|txt(esk47_0,esk49_0)), inference(spm,[status(thm)],[c_0_27, c_0_87])).
cnf(c_0_97, plain, (txtdep(X5,X3)|~phtxtequiv(X1,X2,X3,X4)|~txtdep(X5,X1)), inference(split_conjunct,[status(thm)],[c_0_88])).
cnf(c_0_98, negated_conjecture, (phtxtequiv(X1,esk1_1(X1),esk31_2(esk48_0,esk49_0),esk49_0)|~txtdep(esk48_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_90]), c_0_91])).
cnf(c_0_99, plain, (nontime(X2)|~ppt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_92])).
fof(c_0_100, plain, (![X3]:![X4]:((nontime(X3)|~present(X3,X4))&(time(X4)|~present(X3,X4)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])).
cnf(c_0_101, plain, (ppt(X1,X2,X3)|X1=X2|~pt(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_77])).
cnf(c_0_102, negated_conjecture, (ppt(esk47_0,X1,esk49_0)|pt(esk47_0,esk48_0,esk49_0)|~txtdep(X1,esk35_3(esk47_0,esk48_0,esk49_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_93]), c_0_84])).
cnf(c_0_103, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|pt(esk47_0,esk48_0,esk49_0)), inference(spm,[status(thm)],[c_0_84, c_0_53])).
cnf(c_0_104, negated_conjecture, (txt(esk47_0,esk49_0)|present(esk47_0,X1)|~present(esk34_3(esk47_0,esk48_0,esk49_0),X1)), inference(spm,[status(thm)],[c_0_57, c_0_94])).
cnf(c_0_105, negated_conjecture, (txt(esk47_0,esk49_0)|present(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_95, c_0_96])).
cnf(c_0_106, negated_conjecture, (txt(esk47_0,X1)|~present(esk47_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_94]), c_0_46])).
cnf(c_0_107, negated_conjecture, (txtdep(X1,esk31_2(esk48_0,esk49_0))|~txtdep(esk48_0,X2)|~txtdep(X1,X2)), inference(spm,[status(thm)],[c_0_97, c_0_98])).
cnf(c_0_108, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|nontime(esk48_0)), inference(spm,[status(thm)],[c_0_99, c_0_53])).
cnf(c_0_109, plain, (nontime(X1)|~present(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_100])).
cnf(c_0_110, plain, (X1=X2|ppt(X3,X4,X5)|~txtdep(X1,X3)|~txtdep(X2,X4)|~pt(X1,X2,X5)), inference(spm,[status(thm)],[c_0_44, c_0_101])).
cnf(c_0_111, negated_conjecture, (pt(esk47_0,esk48_0,esk49_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_103]), c_0_84])).
cnf(c_0_112, negated_conjecture, (txt(esk47_0,esk49_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_105]), c_0_106])).
cnf(c_0_113, negated_conjecture, (txtdep(X1,esk31_2(esk48_0,esk49_0))|~txtdep(X1,esk31_2(esk48_0,X2))|~present(esk48_0,X2)), inference(spm,[status(thm)],[c_0_107, c_0_64])).
cnf(c_0_114, negated_conjecture, (nontime(esk48_0)|~present(esk35_3(esk47_0,esk48_0,esk49_0),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_108]), c_0_109])).
cnf(c_0_115, negated_conjecture, (present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|nontime(esk48_0)), inference(spm,[status(thm)],[c_0_99, c_0_59])).
cnf(c_0_116, negated_conjecture, (esk48_0=esk47_0|ppt(X1,X2,esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_110, c_0_111])).
cnf(c_0_117, negated_conjecture, (txtdep(esk47_0,esk31_2(esk47_0,esk49_0))), inference(spm,[status(thm)],[c_0_55, c_0_112])).
cnf(c_0_118, negated_conjecture, (txtdep(esk48_0,esk31_2(esk48_0,esk49_0))|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_113, c_0_64])).
cnf(c_0_119, negated_conjecture, (nontime(esk48_0)), inference(spm,[status(thm)],[c_0_114, c_0_115])).
cnf(c_0_120, negated_conjecture, (esk48_0=esk47_0|ppt(esk31_2(esk47_0,esk49_0),X1,esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_116, c_0_117])).
cnf(c_0_121, negated_conjecture, (txtdep(esk48_0,esk31_2(esk48_0,esk49_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_90]), c_0_119])])).
cnf(c_0_122, negated_conjecture, (esk48_0=esk47_0|ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,X1),esk49_0)|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_120, c_0_64])).
cnf(c_0_123, negated_conjecture, (~txt(esk48_0,esk49_0)|~txt(esk47_0,esk49_0)|~ppt(esk47_0,esk48_0,esk49_0)|~txtppt(esk47_0,esk48_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
cnf(c_0_124, plain, (txtppt(X1,X2,X3)|~ppt(X4,X5,X3)|~txtdep(X2,X5)|~txtdep(X1,X4)), inference(split_conjunct,[status(thm)],[c_0_24])).
cnf(c_0_125, negated_conjecture, (esk48_0=esk47_0|ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_120, c_0_121])).
cnf(c_0_126, negated_conjecture, (esk48_0=esk47_0|present(esk31_2(esk47_0,esk49_0),esk49_0)|~present(esk48_0,X1)), inference(spm,[status(thm)],[c_0_95, c_0_122])).
cnf(c_0_127, negated_conjecture, (present(esk47_0,X1)|~present(esk31_2(esk47_0,esk49_0),X1)), inference(spm,[status(thm)],[c_0_57, c_0_117])).
cnf(c_0_128, negated_conjecture, (~txtppt(esk47_0,esk48_0,esk49_0)|~ppt(esk47_0,esk48_0,esk49_0)|~txt(esk48_0,esk49_0)), inference(csr,[status(thm)],[c_0_123, c_0_86])).
cnf(c_0_129, negated_conjecture, (esk48_0=esk47_0|txtppt(X1,X2,esk49_0)|~txtdep(X2,esk31_2(esk48_0,esk49_0))|~txtdep(X1,esk31_2(esk47_0,esk49_0))), inference(spm,[status(thm)],[c_0_124, c_0_125])).
fof(c_0_130, plain, (![X1]:![X4]:![X2]:(ppt(X1,X4,X2)=>~phtxtequiv(X1,X2,X4,X2))), inference(fof_simplification,[status(thm)],[c_0_19])).
cnf(c_0_131, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|ppt(X1,X2,esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_53])).
cnf(c_0_132, negated_conjecture, (txtdep(esk47_0,esk31_2(esk47_0,X1))|~present(esk47_0,X1)), inference(spm,[status(thm)],[c_0_55, c_0_106])).
cnf(c_0_133, negated_conjecture, (esk48_0=esk47_0|present(esk31_2(esk47_0,esk49_0),esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_90]), c_0_119])])).
cnf(c_0_134, negated_conjecture, (present(esk47_0,X1)|~phtxt(esk31_2(esk47_0,esk49_0),X1)), inference(spm,[status(thm)],[c_0_127, c_0_74])).
cnf(c_0_135, negated_conjecture, (phtxt(esk31_2(esk47_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_34, c_0_112])).
cnf(c_0_136, negated_conjecture, (ppt(X1,X2,esk49_0)|present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_59])).
cnf(c_0_137, negated_conjecture, (esk48_0=esk47_0|~ppt(esk47_0,esk48_0,esk49_0)|~txt(esk48_0,esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_121]), c_0_117])])).
fof(c_0_138, plain, (![X1]:![X2]:~ppt(X1,X1,X2)), inference(fof_simplification,[status(thm)],[c_0_20])).
fof(c_0_139, plain, (![X5]:![X6]:![X7]:(~ppt(X5,X6,X7)|~phtxtequiv(X5,X7,X6,X7))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_130])])).
cnf(c_0_140, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|ppt(esk31_2(esk47_0,esk49_0),X1,esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_131, c_0_117])).
cnf(c_0_141, negated_conjecture, (phtxtequiv(X1,X2,esk31_2(esk47_0,X3),X4)|~txtdep(esk47_0,X1)|~present(esk31_2(esk47_0,X3),X4)|~present(esk47_0,X3)|~present(X1,X2)), inference(spm,[status(thm)],[c_0_71, c_0_132])).
cnf(c_0_142, negated_conjecture, (present(esk31_2(esk47_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_80, c_0_133])).
cnf(c_0_143, negated_conjecture, (present(esk47_0,esk49_0)), inference(spm,[status(thm)],[c_0_134, c_0_135])).
cnf(c_0_144, negated_conjecture, (ppt(esk31_2(esk47_0,esk49_0),X1,esk49_0)|present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_136, c_0_117])).
cnf(c_0_145, negated_conjecture, (esk48_0=esk47_0|~ppt(esk47_0,esk48_0,esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137, c_0_56]), c_0_73])])).
fof(c_0_146, plain, (![X3]:![X4]:~ppt(X3,X3,X4)), inference(variable_rename,[status(thm)],[c_0_138])).
cnf(c_0_147, plain, (~phtxtequiv(X1,X2,X3,X2)|~ppt(X1,X3,X2)), inference(split_conjunct,[status(thm)],[c_0_139])).
cnf(c_0_148, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_140, c_0_121])).
cnf(c_0_149, negated_conjecture, (phtxtequiv(X1,X2,esk31_2(esk47_0,esk49_0),esk49_0)|~txtdep(esk47_0,X1)|~present(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_141, c_0_142]), c_0_143])])).
cnf(c_0_150, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|present(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_95, c_0_33])).
cnf(c_0_151, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|ppt(X1,X2,esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_85])).
cnf(c_0_152, negated_conjecture, (ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,esk49_0),esk49_0)|present(esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_144, c_0_121])).
cnf(c_0_153, negated_conjecture, (esk48_0=esk47_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145, c_0_101]), c_0_111])])).
cnf(c_0_154, plain, (~ppt(X1,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_146])).
cnf(c_0_155, negated_conjecture, (txtdep(esk48_0,esk35_3(esk47_0,esk48_0,esk49_0))|~phtxtequiv(esk31_2(esk47_0,esk49_0),esk49_0,esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_147, c_0_148])).
cnf(c_0_156, negated_conjecture, (phtxtequiv(esk31_2(esk47_0,esk49_0),esk49_0,esk31_2(esk47_0,esk49_0),esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_142]), c_0_117])])).
cnf(c_0_157, negated_conjecture, (ppt(X1,X2,esk49_0)|present(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0)|~txtdep(esk47_0,X1)|~txtdep(esk48_0,X2)), inference(spm,[status(thm)],[c_0_44, c_0_150])).
cnf(c_0_158, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|ppt(esk31_2(esk47_0,esk49_0),X1,esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_151, c_0_117])).
fof(c_0_159, plain, (![X5]:![X6]:![X7]:![X8]:(~phtxtequiv(X5,X6,X7,X8)|phtxtequiv(X7,X8,X5,X6))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])).
cnf(c_0_160, negated_conjecture, (present(esk35_3(esk47_0,esk47_0,esk49_0),esk49_0)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_152, c_0_153]), c_0_153]), c_0_154])).
cnf(c_0_161, negated_conjecture, (txtdep(esk47_0,esk35_3(esk47_0,esk47_0,esk49_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_155, c_0_153]), c_0_153]), c_0_153]), c_0_156])])).
cnf(c_0_162, negated_conjecture, (ppt(esk31_2(esk47_0,esk49_0),X1,esk49_0)|present(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0)|~txtdep(esk48_0,X1)), inference(spm,[status(thm)],[c_0_157, c_0_117])).
cnf(c_0_163, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_158, c_0_121])).
fof(c_0_164, plain, (![X15]:![X16]:![X17]:![X18]:![X19]:![X20]:((~phtxtequiv(X15,X16,X17,X18)|~phtxtequiv(X17,X18,X19,X20))|phtxtequiv(X15,X16,X19,X20))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])).
cnf(c_0_165, plain, (phtxtequiv(X1,X2,X3,X4)|~phtxtequiv(X3,X4,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_159])).
cnf(c_0_166, negated_conjecture, (phtxtequiv(esk35_3(esk47_0,esk47_0,esk49_0),esk49_0,esk31_2(esk47_0,esk49_0),esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_160]), c_0_161])])).
cnf(c_0_167, negated_conjecture, (ppt(esk31_2(esk47_0,esk49_0),esk31_2(esk48_0,esk49_0),esk49_0)|present(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_162, c_0_121])).
cnf(c_0_168, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk48_0,esk49_0))|~phtxtequiv(esk31_2(esk47_0,esk49_0),esk49_0,esk31_2(esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_147, c_0_163])).
cnf(c_0_169, negated_conjecture, (ppt(esk47_0,esk48_0,esk49_0)|~phtxtequiv(esk34_3(esk47_0,esk48_0,esk49_0),esk49_0,esk35_3(esk47_0,esk48_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_147, c_0_33])).
cnf(c_0_170, plain, (phtxtequiv(X1,X2,X3,X4)|~phtxtequiv(X5,X6,X3,X4)|~phtxtequiv(X1,X2,X5,X6)), inference(split_conjunct,[status(thm)],[c_0_164])).
cnf(c_0_171, negated_conjecture, (phtxtequiv(esk31_2(esk47_0,esk49_0),esk49_0,esk35_3(esk47_0,esk47_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_165, c_0_166])).
cnf(c_0_172, negated_conjecture, (present(esk34_3(esk47_0,esk47_0,esk49_0),esk49_0)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_153]), c_0_153]), c_0_154])).
cnf(c_0_173, negated_conjecture, (txtdep(esk47_0,esk34_3(esk47_0,esk47_0,esk49_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_168, c_0_153]), c_0_153]), c_0_156])])).
cnf(c_0_174, negated_conjecture, (~phtxtequiv(esk34_3(esk47_0,esk47_0,esk49_0),esk49_0,esk35_3(esk47_0,esk47_0,esk49_0),esk49_0)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_169, c_0_153]), c_0_153]), c_0_153]), c_0_154])).
cnf(c_0_175, negated_conjecture, (phtxtequiv(X1,X2,esk35_3(esk47_0,esk47_0,esk49_0),esk49_0)|~phtxtequiv(X1,X2,esk31_2(esk47_0,esk49_0),esk49_0)), inference(spm,[status(thm)],[c_0_170, c_0_171])).
cnf(c_0_176, negated_conjecture, (phtxtequiv(esk34_3(esk47_0,esk47_0,esk49_0),esk49_0,esk31_2(esk47_0,esk49_0),esk49_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_172]), c_0_173])])).
cnf(c_0_177, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_174, c_0_175]), c_0_176])]), ['proof']).
# SZS output end CNFRefutation
# Training examples: 0 positive, 0 negative

# -------------------------------------------------
# User time                : 2.892 s
# System time              : 0.065 s
# Total time               : 2.957 s
# Maximum resident set size: 1852 pages

% END OF SYSTEM OUTPUT
% RESULT: SOT_7mLMQO - E---1.9.1 says Theorem - CPU = 2.92 WC = 2.95 
% OUTPUT: SOT_7mLMQO - E---1.9.1 says CNFRefutation - CPU = 2.92 WC = 2.95