# Preprocessing time       : 0.029 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
thf(cmapdlsm_conj, conjecture, ![X1:$o, X4:$i > $o, X21:$i > $o, X16:$i > $o, X11:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o, X19:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X16)=(ccfv @ X14 @ cclsm)=>((X4)=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))=>((X21)=(ccfv @ X4 @ cclsm)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ X11)=>((X1=>cwcel @ X19 @ X11)=>(X1=>(ccfv @ (cco @ X18 @ X19 @ X16) @ X15)=(cco @ (ccfv @ X18 @ X15) @ (ccfv @ X19 @ X15) @ X21)))))))))))), file('mmset37610_mapdlsm.p', cmapdlsm_conj)).
thf(advhlmod_thm, axiom, ![X1:$o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>(X1=>cwcel @ X14 @ cclmod)))), file('mmset37610_mapdlsm.p', advhlmod_thm)).
thf(alsmcl_thm, axiom, ![X16:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X10:$i > $o]:((X11)=(ccfv @ X10 @ cclss)=>((X16)=(ccfv @ X10 @ cclsm)=>(((cwcel @ X10 @ cclmod&cwcel @ X13 @ X11)&cwcel @ X14 @ X11)=>cwcel @ (cco @ X13 @ X14 @ X16) @ X11))), file('mmset37610_mapdlsm.p', alsmcl_thm)).
thf(alsssssubg_thm, axiom, ![X11:$i > $o, X10:$i > $o]:((X11)=(ccfv @ X10 @ cclss)=>(cwcel @ X10 @ cclmod=>cwss @ X11 @ (ccfv @ X10 @ ccsubg))), file('mmset37610_mapdlsm.p', alsssssubg_thm)).
thf(asseldd_thm, axiom, ![X1:$o, X2:$i > $o, X3:$i > $o, X4:$i > $o]:((X1=>cwss @ X2 @ X3)=>((X1=>cwcel @ X4 @ X2)=>(X1=>cwcel @ X4 @ X3))), file('mmset37610_mapdlsm.p', asseldd_thm)).
thf(amapdcl_thm, axiom, ![X1:$o, X11:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ X11)=>(X1=>cwcel @ (ccfv @ X18 @ X15) @ (ccrn @ X15)))))))), file('mmset37610_mapdlsm.p', amapdcl_thm)).
thf(alsmub2_thm, axiom, ![X16:$i > $o, X13:$i > $o, X14:$i > $o, X17:$i > $o]:((X16)=(ccfv @ X17 @ cclsm)=>((cwcel @ X13 @ (ccfv @ X17 @ ccsubg)&cwcel @ X14 @ (ccfv @ X17 @ ccsubg))=>cwss @ X14 @ (cco @ X13 @ X14 @ X16))), file('mmset37610_mapdlsm.p', alsmub2_thm)).
thf(alsmub1_thm, axiom, ![X16:$i > $o, X13:$i > $o, X14:$i > $o, X17:$i > $o]:((X16)=(ccfv @ X17 @ cclsm)=>((cwcel @ X13 @ (ccfv @ X17 @ ccsubg)&cwcel @ X14 @ (ccfv @ X17 @ ccsubg))=>cwss @ X13 @ (cco @ X13 @ X14 @ X16))), file('mmset37610_mapdlsm.p', alsmub1_thm)).
thf(amapdcl2_thm, axiom, ![X1:$o, X4:$i > $o, X12:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X4)=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))=>((X13)=(ccfv @ X4 @ cclss)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X12 @ X11)=>(X1=>cwcel @ (ccfv @ X12 @ X15) @ X13))))))))), file('mmset37610_mapdlsm.p', amapdcl2_thm)).
thf(amapdcnvcl_thm, axiom, ![X1:$o, X11:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ (ccrn @ X15))=>(X1=>cwcel @ (ccfv @ X18 @ (cccnv @ X15)) @ X11))))))), file('mmset37610_mapdlsm.p', amapdcnvcl_thm)).
thf(amapdord_thm, axiom, ![X1:$o, X11:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o, X19:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ X11)=>((X1=>cwcel @ X19 @ X11)=>(X1=>(cwss @ (ccfv @ X18 @ X15) @ (ccfv @ X19 @ X15)<=>cwss @ X18 @ X19))))))))), file('mmset37610_mapdlsm.p', amapdord_thm)).
thf(alsmlub_thm, axiom, ![X16:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X17:$i > $o]:((X16)=(ccfv @ X17 @ cclsm)=>(((cwcel @ X11 @ (ccfv @ X17 @ ccsubg)&cwcel @ X13 @ (ccfv @ X17 @ ccsubg))&cwcel @ X14 @ (ccfv @ X17 @ ccsubg))=>((cwss @ X11 @ X14&cwss @ X13 @ X14)<=>cwss @ (cco @ X11 @ X13 @ X16) @ X14))), file('mmset37610_mapdlsm.p', alsmlub_thm)).
thf(amapdlsmcl_thm, axiom, ![X1:$o, X4:$i > $o, X16:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o, X19:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X4)=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))=>((X16)=(ccfv @ X4 @ cclsm)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ (ccrn @ X15))=>((X1=>cwcel @ X19 @ (ccrn @ X15))=>(X1=>cwcel @ (cco @ X18 @ X19 @ X16) @ (ccrn @ X15)))))))))), file('mmset37610_mapdlsm.p', amapdlsmcl_thm)).
thf(amapdcnvid2_thm, axiom, ![X1:$o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ (ccrn @ X15))=>(X1=>(ccfv @ (ccfv @ X18 @ (cccnv @ X15)) @ X15)=(X18)))))), file('mmset37610_mapdlsm.p', amapdcnvid2_thm)).
thf(alcdlmod_thm, axiom, ![X1:$o, X4:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X4)=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>(X1=>cwcel @ X4 @ cclmod)))), file('mmset37610_mapdlsm.p', alcdlmod_thm)).
thf(aeqssd_thm, axiom, ![X1:$o, X2:$i > $o, X3:$i > $o]:((X1=>cwss @ X2 @ X3)=>((X1=>cwss @ X3 @ X2)=>(X1=>(X2)=(X3)))), file('mmset37610_mapdlsm.p', aeqssd_thm)).
thf(c_0_16, negated_conjecture, ~(![X1:$o, X4:$i > $o, X21:$i > $o, X16:$i > $o, X11:$i > $o, X14:$i > $o, X8:$i > $o, X9:$i > $o, X15:$i > $o, X10:$i > $o, X18:$i > $o, X19:$i > $o]:((X8)=(ccfv @ X9 @ cclh)=>((X15)=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))=>((X14)=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))=>((X11)=(ccfv @ X14 @ cclss)=>((X16)=(ccfv @ X14 @ cclsm)=>((X4)=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))=>((X21)=(ccfv @ X4 @ cclsm)=>((X1=>(cwcel @ X9 @ cchlt&cwcel @ X10 @ X8))=>((X1=>cwcel @ X18 @ X11)=>((X1=>cwcel @ X19 @ X11)=>(X1=>(ccfv @ (cco @ X18 @ X19 @ X16) @ X15)=(cco @ (ccfv @ X18 @ X15) @ (ccfv @ X19 @ X15) @ X21))))))))))))), inference(assume_negation,[status(cth)],[cmapdlsm_conj])).
thf(c_0_17, negated_conjecture, ((epred7_0)=(ccfv @ epred8_0 @ cclh)&((epred9_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ ccmpd))&((epred6_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ ccdvh))&((epred5_0)=(ccfv @ epred6_0 @ cclss)&((epred4_0)=(ccfv @ epred6_0 @ cclsm)&((epred2_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ cclcd))&((epred3_0)=(ccfv @ epred2_0 @ cclsm)&(((cwcel @ epred8_0 @ cchlt|~epred1_0)&(cwcel @ epred10_0 @ epred7_0|~epred1_0))&((~epred1_0|cwcel @ epred11_0 @ epred5_0)&((~epred1_0|cwcel @ epred12_0 @ epred5_0)&(epred1_0&(ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)!=(cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0)))))))))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])).
thf(c_0_18, plain, ![X257:$o, X258:$i > $o, X259:$i > $o, X260:$i > $o, X261:$i > $o]:((X257|(~X257|cwcel @ X258 @ cclmod)|(X258)!=(ccfv @ X261 @ (ccfv @ X260 @ ccdvh))|(X259)!=(ccfv @ X260 @ cclh))&(~cwcel @ X260 @ cchlt|~cwcel @ X261 @ X259|(~X257|cwcel @ X258 @ cclmod)|(X258)!=(ccfv @ X261 @ (ccfv @ X260 @ ccdvh))|(X259)!=(ccfv @ X260 @ cclh))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[advhlmod_thm])])])).
thf(c_0_19, negated_conjecture, (cwcel @ epred8_0 @ cchlt|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_20, negated_conjecture, epred1_0, inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_21, plain, ![X8:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwcel @ X8 @ cclmod|~cwcel @ X2 @ cchlt|~cwcel @ X3 @ X4|(X8)!=(ccfv @ X3 @ (ccfv @ X2 @ ccdvh))|(X4)!=(ccfv @ X2 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_18])])])).
thf(c_0_22, negated_conjecture, (epred6_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ ccdvh)), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_23, negated_conjecture, (epred7_0)=(ccfv @ epred8_0 @ cclh), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_24, negated_conjecture, cwcel @ epred8_0 @ cchlt, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
thf(c_0_25, negated_conjecture, (cwcel @ epred10_0 @ epred7_0|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_26, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ cclmod|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23]), c_0_24])])).
thf(c_0_27, negated_conjecture, cwcel @ epred10_0 @ epred7_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_20])])).
thf(c_0_28, plain, ![X267:$i > $o, X268:$i > $o, X269:$i > $o, X270:$i > $o, X271:$i > $o]:((X268)!=(ccfv @ X271 @ cclss)|((X267)!=(ccfv @ X271 @ cclsm)|(~cwcel @ X271 @ cclmod|~cwcel @ X269 @ X268|~cwcel @ X270 @ X268|cwcel @ (cco @ X269 @ X270 @ X267) @ X268))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alsmcl_thm])])).
thf(c_0_29, plain, ![X190:$i > $o, X191:$i > $o]:((X190)!=(ccfv @ X191 @ cclss)|(~cwcel @ X191 @ cclmod|cwss @ X190 @ (ccfv @ X191 @ ccsubg))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alsssssubg_thm])])).
thf(c_0_30, negated_conjecture, ![X2:$i > $o]:(cwcel @ X2 @ cclmod|(X2)!=(epred6_0)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
thf(c_0_31, plain, ![X3:$i > $o, X8:$i > $o, X9:$i > $o, X4:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X8 @ X9 @ X4) @ X2|(X2)!=(ccfv @ X3 @ cclss)|(X4)!=(ccfv @ X3 @ cclsm)|~cwcel @ X3 @ cclmod|~cwcel @ X8 @ X2|~cwcel @ X9 @ X2), inference(split_conjunct,[status(thm)],[c_0_28])).
thf(c_0_32, plain, ![X178:$o, X179:$i > $o, X180:$i > $o, X181:$i > $o]:(((X178|(~X178|cwcel @ X181 @ X180)|X178)&(~cwcel @ X181 @ X179|(~X178|cwcel @ X181 @ X180)|X178))&((X178|(~X178|cwcel @ X181 @ X180)|~cwss @ X179 @ X180)&(~cwcel @ X181 @ X179|(~X178|cwcel @ X181 @ X180)|~cwss @ X179 @ X180))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asseldd_thm])])])).
thf(c_0_33, negated_conjecture, (cwcel @ epred12_0 @ epred5_0|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_34, plain, ![X2:$i > $o, X3:$i > $o]:(cwss @ X2 @ (ccfv @ X3 @ ccsubg)|(X2)!=(ccfv @ X3 @ cclss)|~cwcel @ X3 @ cclmod), inference(split_conjunct,[status(thm)],[c_0_29])).
thf(c_0_35, negated_conjecture, (epred5_0)=(ccfv @ epred6_0 @ cclss), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_36, negated_conjecture, cwcel @ epred6_0 @ cclmod, inference(er,[status(thm)],[c_0_30])).
thf(c_0_37, plain, ![X223:$o, X224:$i > $o, X225:$i > $o, X226:$i > $o, X227:$i > $o, X228:$i > $o, X229:$i > $o, X230:$i > $o]:(((X223|(~X223|cwcel @ (ccfv @ X230 @ X228) @ (ccrn @ X228))|X223|(X224)!=(ccfv @ X225 @ cclss)|(X225)!=(ccfv @ X229 @ (ccfv @ X227 @ ccdvh))|(X228)!=(ccfv @ X229 @ (ccfv @ X227 @ ccmpd))|(X226)!=(ccfv @ X227 @ cclh))&(~cwcel @ X230 @ X224|(~X223|cwcel @ (ccfv @ X230 @ X228) @ (ccrn @ X228))|X223|(X224)!=(ccfv @ X225 @ cclss)|(X225)!=(ccfv @ X229 @ (ccfv @ X227 @ ccdvh))|(X228)!=(ccfv @ X229 @ (ccfv @ X227 @ ccmpd))|(X226)!=(ccfv @ X227 @ cclh)))&((X223|(~X223|cwcel @ (ccfv @ X230 @ X228) @ (ccrn @ X228))|(~cwcel @ X227 @ cchlt|~cwcel @ X229 @ X226)|(X224)!=(ccfv @ X225 @ cclss)|(X225)!=(ccfv @ X229 @ (ccfv @ X227 @ ccdvh))|(X228)!=(ccfv @ X229 @ (ccfv @ X227 @ ccmpd))|(X226)!=(ccfv @ X227 @ cclh))&(~cwcel @ X230 @ X224|(~X223|cwcel @ (ccfv @ X230 @ X228) @ (ccrn @ X228))|(~cwcel @ X227 @ cchlt|~cwcel @ X229 @ X226)|(X224)!=(ccfv @ X225 @ cclss)|(X225)!=(ccfv @ X229 @ (ccfv @ X227 @ ccdvh))|(X228)!=(ccfv @ X229 @ (ccfv @ X227 @ ccmpd))|(X226)!=(ccfv @ X227 @ cclh)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdcl_thm])])])).
thf(c_0_38, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X8:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ (ccfv @ X4 @ cclsm)) @ X8|(X8)!=(ccfv @ X4 @ cclss)|~cwcel @ X4 @ cclmod|~cwcel @ X3 @ X8|~cwcel @ X2 @ X8), inference(er,[status(thm)],[c_0_31])).
thf(c_0_39, negated_conjecture, (epred4_0)=(ccfv @ epred6_0 @ cclsm), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_40, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ X2 @ X4|~cwcel @ X2 @ X3|~cwss @ X3 @ X4), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_32])])])).
thf(c_0_41, negated_conjecture, cwcel @ epred12_0 @ epred5_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_20])])).
thf(c_0_42, negated_conjecture, ![X2:$i > $o]:(cwss @ X2 @ (ccfv @ epred6_0 @ ccsubg)|(X2)!=(epred5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])])).
thf(c_0_43, negated_conjecture, (cwcel @ epred11_0 @ epred5_0|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_44, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ X4) @ (ccrn @ X4)|~cwcel @ X2 @ X3|~cwcel @ X8 @ cchlt|~cwcel @ X9 @ X10|(X3)!=(ccfv @ X11 @ cclss)|(X11)!=(ccfv @ X9 @ (ccfv @ X8 @ ccdvh))|(X4)!=(ccfv @ X9 @ (ccfv @ X8 @ ccmpd))|(X10)!=(ccfv @ X8 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_37])])])).
thf(c_0_45, negated_conjecture, (epred9_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ ccmpd)), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_46, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ epred4_0) @ X4|(X4)!=(epred5_0)|~cwcel @ X3 @ X4|~cwcel @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_35]), c_0_39]), c_0_36])])).
thf(c_0_47, plain, ![X248:$i > $o, X249:$i > $o, X250:$i > $o, X251:$i > $o]:((X248)!=(ccfv @ X251 @ cclsm)|(~cwcel @ X249 @ (ccfv @ X251 @ ccsubg)|~cwcel @ X250 @ (ccfv @ X251 @ ccsubg)|cwss @ X250 @ (cco @ X249 @ X250 @ X248))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alsmub2_thm])])).
thf(c_0_48, negated_conjecture, ![X2:$i > $o]:(cwcel @ epred12_0 @ X2|~cwss @ epred5_0 @ X2), inference(spm,[status(thm)],[c_0_40, c_0_41])).
thf(c_0_49, negated_conjecture, cwss @ epred5_0 @ (ccfv @ epred6_0 @ ccsubg), inference(er,[status(thm)],[c_0_42])).
thf(c_0_50, negated_conjecture, cwcel @ epred11_0 @ epred5_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_20])])).
thf(c_0_51, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X9:$i > $o, X8:$i > $o, X4:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccrn @ X3)|(X4)!=(ccfv @ X8 @ cclss)|(X8)!=(epred6_0)|(X3)!=(epred9_0)|(X9)!=(epred7_0)|~cwcel @ epred10_0 @ X9|~cwcel @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_52, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ epred12_0 @ epred4_0) @ epred5_0|~cwcel @ X2 @ epred5_0), inference(spm,[status(thm)],[c_0_46, c_0_41])).
thf(c_0_53, plain, ![X2:$i > $o, X8:$i > $o, X4:$i > $o, X3:$i > $o]:(cwss @ X8 @ (cco @ X4 @ X8 @ X2)|(X2)!=(ccfv @ X3 @ cclsm)|~cwcel @ X4 @ (ccfv @ X3 @ ccsubg)|~cwcel @ X8 @ (ccfv @ X3 @ ccsubg)), inference(split_conjunct,[status(thm)],[c_0_47])).
thf(c_0_54, negated_conjecture, cwcel @ epred12_0 @ (ccfv @ epred6_0 @ ccsubg), inference(spm,[status(thm)],[c_0_48, c_0_49])).
thf(c_0_55, negated_conjecture, ![X2:$i > $o]:(cwcel @ epred11_0 @ X2|~cwss @ epred5_0 @ X2), inference(spm,[status(thm)],[c_0_40, c_0_50])).
thf(c_0_56, plain, ![X203:$i > $o, X204:$i > $o, X205:$i > $o, X206:$i > $o]:((X203)!=(ccfv @ X206 @ cclsm)|(~cwcel @ X204 @ (ccfv @ X206 @ ccsubg)|~cwcel @ X205 @ (ccfv @ X206 @ ccsubg)|cwss @ X204 @ (cco @ X204 @ X205 @ X203))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alsmub1_thm])])).
thf(c_0_57, plain, ![X193:$o, X194:$i > $o, X195:$i > $o, X196:$i > $o, X197:$i > $o, X198:$i > $o, X199:$i > $o, X200:$i > $o, X201:$i > $o, X202:$i > $o]:(((X193|(~X193|cwcel @ (ccfv @ X195 @ X201) @ X197)|X193|(X197)!=(ccfv @ X194 @ cclss)|(X194)!=(ccfv @ X202 @ (ccfv @ X200 @ cclcd))|(X196)!=(ccfv @ X198 @ cclss)|(X198)!=(ccfv @ X202 @ (ccfv @ X200 @ ccdvh))|(X201)!=(ccfv @ X202 @ (ccfv @ X200 @ ccmpd))|(X199)!=(ccfv @ X200 @ cclh))&(~cwcel @ X195 @ X196|(~X193|cwcel @ (ccfv @ X195 @ X201) @ X197)|X193|(X197)!=(ccfv @ X194 @ cclss)|(X194)!=(ccfv @ X202 @ (ccfv @ X200 @ cclcd))|(X196)!=(ccfv @ X198 @ cclss)|(X198)!=(ccfv @ X202 @ (ccfv @ X200 @ ccdvh))|(X201)!=(ccfv @ X202 @ (ccfv @ X200 @ ccmpd))|(X199)!=(ccfv @ X200 @ cclh)))&((X193|(~X193|cwcel @ (ccfv @ X195 @ X201) @ X197)|(~cwcel @ X200 @ cchlt|~cwcel @ X202 @ X199)|(X197)!=(ccfv @ X194 @ cclss)|(X194)!=(ccfv @ X202 @ (ccfv @ X200 @ cclcd))|(X196)!=(ccfv @ X198 @ cclss)|(X198)!=(ccfv @ X202 @ (ccfv @ X200 @ ccdvh))|(X201)!=(ccfv @ X202 @ (ccfv @ X200 @ ccmpd))|(X199)!=(ccfv @ X200 @ cclh))&(~cwcel @ X195 @ X196|(~X193|cwcel @ (ccfv @ X195 @ X201) @ X197)|(~cwcel @ X200 @ cchlt|~cwcel @ X202 @ X199)|(X197)!=(ccfv @ X194 @ cclss)|(X194)!=(ccfv @ X202 @ (ccfv @ X200 @ cclcd))|(X196)!=(ccfv @ X198 @ cclss)|(X198)!=(ccfv @ X202 @ (ccfv @ X200 @ ccdvh))|(X201)!=(ccfv @ X202 @ (ccfv @ X200 @ ccmpd))|(X199)!=(ccfv @ X200 @ cclh)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdcl2_thm])])])).
thf(c_0_58, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X8:$i > $o, X4:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccrn @ X3)|(X4)!=(epred5_0)|(X3)!=(epred9_0)|(X8)!=(epred7_0)|~cwcel @ epred10_0 @ X8|~cwcel @ X2 @ X4), inference(spm,[status(thm)],[c_0_51, c_0_35])).
thf(c_0_59, plain, ![X240:$o, X241:$i > $o, X242:$i > $o, X243:$i > $o, X244:$i > $o, X245:$i > $o, X246:$i > $o, X247:$i > $o]:(((X240|(~X240|cwcel @ (ccfv @ X247 @ (cccnv @ X245)) @ X241)|X240|(X241)!=(ccfv @ X242 @ cclss)|(X242)!=(ccfv @ X246 @ (ccfv @ X244 @ ccdvh))|(X245)!=(ccfv @ X246 @ (ccfv @ X244 @ ccmpd))|(X243)!=(ccfv @ X244 @ cclh))&(~cwcel @ X247 @ (ccrn @ X245)|(~X240|cwcel @ (ccfv @ X247 @ (cccnv @ X245)) @ X241)|X240|(X241)!=(ccfv @ X242 @ cclss)|(X242)!=(ccfv @ X246 @ (ccfv @ X244 @ ccdvh))|(X245)!=(ccfv @ X246 @ (ccfv @ X244 @ ccmpd))|(X243)!=(ccfv @ X244 @ cclh)))&((X240|(~X240|cwcel @ (ccfv @ X247 @ (cccnv @ X245)) @ X241)|(~cwcel @ X244 @ cchlt|~cwcel @ X246 @ X243)|(X241)!=(ccfv @ X242 @ cclss)|(X242)!=(ccfv @ X246 @ (ccfv @ X244 @ ccdvh))|(X245)!=(ccfv @ X246 @ (ccfv @ X244 @ ccmpd))|(X243)!=(ccfv @ X244 @ cclh))&(~cwcel @ X247 @ (ccrn @ X245)|(~X240|cwcel @ (ccfv @ X247 @ (cccnv @ X245)) @ X241)|(~cwcel @ X244 @ cchlt|~cwcel @ X246 @ X243)|(X241)!=(ccfv @ X242 @ cclss)|(X242)!=(ccfv @ X246 @ (ccfv @ X244 @ ccdvh))|(X245)!=(ccfv @ X246 @ (ccfv @ X244 @ ccmpd))|(X243)!=(ccfv @ X244 @ cclh)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdcnvcl_thm])])])).
thf(c_0_60, plain, ![X231:$o, X232:$i > $o, X233:$i > $o, X234:$i > $o, X235:$i > $o, X236:$i > $o, X237:$i > $o, X238:$i > $o, X239:$i > $o]:(((((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|X231|X231|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|X231|X231|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))&((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|~cwcel @ X239 @ X232|X231|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|~cwcel @ X239 @ X232|X231|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))))&(((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|X231|~cwcel @ X238 @ X232|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|X231|~cwcel @ X238 @ X232|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))&((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|~cwcel @ X239 @ X232|~cwcel @ X238 @ X232|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|~cwcel @ X239 @ X232|~cwcel @ X238 @ X232|X231|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))))&((((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|X231|X231|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|X231|X231|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))&((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|~cwcel @ X239 @ X232|X231|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|~cwcel @ X239 @ X232|X231|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))))&(((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|X231|~cwcel @ X238 @ X232|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|X231|~cwcel @ X238 @ X232|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))&((~cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|cwss @ X238 @ X239|~X231|~cwcel @ X239 @ X232|~cwcel @ X238 @ X232|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh))&(~cwss @ X238 @ X239|cwss @ (ccfv @ X238 @ X236) @ (ccfv @ X239 @ X236)|~X231|~cwcel @ X239 @ X232|~cwcel @ X238 @ X232|(~cwcel @ X235 @ cchlt|~cwcel @ X237 @ X234)|(X236)!=(ccfv @ X237 @ (ccfv @ X235 @ ccmpd))|(X232)!=(ccfv @ X233 @ cclss)|(X233)!=(ccfv @ X237 @ (ccfv @ X235 @ ccdvh))|(X234)!=(ccfv @ X235 @ cclh)))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdord_thm])])])).
thf(c_0_61, plain, ![X262:$i > $o, X263:$i > $o, X264:$i > $o, X265:$i > $o, X266:$i > $o]:((~cwss @ X263 @ X265|~cwss @ X264 @ X265|cwss @ (cco @ X263 @ X264 @ X262) @ X265|(~cwcel @ X263 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X264 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X265 @ (ccfv @ X266 @ ccsubg))|(X262)!=(ccfv @ X266 @ cclsm))&((cwss @ X263 @ X265|~cwss @ (cco @ X263 @ X264 @ X262) @ X265|(~cwcel @ X263 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X264 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X265 @ (ccfv @ X266 @ ccsubg))|(X262)!=(ccfv @ X266 @ cclsm))&(cwss @ X264 @ X265|~cwss @ (cco @ X263 @ X264 @ X262) @ X265|(~cwcel @ X263 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X264 @ (ccfv @ X266 @ ccsubg)|~cwcel @ X265 @ (ccfv @ X266 @ ccsubg))|(X262)!=(ccfv @ X266 @ cclsm)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alsmlub_thm])])])).
thf(c_0_62, negated_conjecture, cwcel @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred5_0, inference(spm,[status(thm)],[c_0_52, c_0_50])).
thf(c_0_63, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ epred12_0 @ (cco @ X2 @ epred12_0 @ X3)|(X3)!=(epred4_0)|~cwcel @ X2 @ (ccfv @ epred6_0 @ ccsubg)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_39])).
thf(c_0_64, negated_conjecture, cwcel @ epred11_0 @ (ccfv @ epred6_0 @ ccsubg), inference(spm,[status(thm)],[c_0_55, c_0_49])).
thf(c_0_65, plain, ![X2:$i > $o, X8:$i > $o, X4:$i > $o, X3:$i > $o]:(cwss @ X4 @ (cco @ X4 @ X8 @ X2)|(X2)!=(ccfv @ X3 @ cclsm)|~cwcel @ X4 @ (ccfv @ X3 @ ccsubg)|~cwcel @ X8 @ (ccfv @ X3 @ ccsubg)), inference(split_conjunct,[status(thm)],[c_0_56])).
thf(c_0_66, plain, ![X213:$o, X214:$i > $o, X215:$i > $o, X216:$i > $o, X217:$i > $o, X218:$i > $o, X219:$i > $o, X220:$i > $o, X221:$i > $o, X222:$i > $o]:((((X213|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|X213|X213|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))&(~cwcel @ X222 @ (ccrn @ X219)|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|X213|X213|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh)))&((X213|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|~cwcel @ X221 @ (ccrn @ X219)|X213|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))&(~cwcel @ X222 @ (ccrn @ X219)|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|~cwcel @ X221 @ (ccrn @ X219)|X213|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))))&(((X213|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|X213|(~cwcel @ X218 @ cchlt|~cwcel @ X220 @ X217)|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))&(~cwcel @ X222 @ (ccrn @ X219)|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|X213|(~cwcel @ X218 @ cchlt|~cwcel @ X220 @ X217)|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh)))&((X213|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|~cwcel @ X221 @ (ccrn @ X219)|(~cwcel @ X218 @ cchlt|~cwcel @ X220 @ X217)|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))&(~cwcel @ X222 @ (ccrn @ X219)|(~X213|cwcel @ (cco @ X221 @ X222 @ X215) @ (ccrn @ X219))|~cwcel @ X221 @ (ccrn @ X219)|(~cwcel @ X218 @ cchlt|~cwcel @ X220 @ X217)|(X215)!=(ccfv @ X214 @ cclsm)|(X214)!=(ccfv @ X220 @ (ccfv @ X218 @ cclcd))|(X216)!=(ccfv @ X220 @ (ccfv @ X218 @ ccdvh))|(X219)!=(ccfv @ X220 @ (ccfv @ X218 @ ccmpd))|(X217)!=(ccfv @ X218 @ cclh))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdlsmcl_thm])])])).
thf(c_0_67, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X8:$i > $o, X13:$i > $o, X12:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o]:(cwcel @ (ccfv @ X2 @ X4) @ X8|~cwcel @ X2 @ X3|~cwcel @ X9 @ cchlt|~cwcel @ X10 @ X11|(X8)!=(ccfv @ X12 @ cclss)|(X12)!=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))|(X3)!=(ccfv @ X13 @ cclss)|(X13)!=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))|(X4)!=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))|(X11)!=(ccfv @ X9 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_57])])])).
thf(c_0_68, negated_conjecture, (epred2_0)=(ccfv @ epred10_0 @ (ccfv @ epred8_0 @ cclcd)), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_69, plain, ![X207:$o, X208:$i > $o, X209:$i > $o, X210:$i > $o, X211:$i > $o, X212:$i > $o]:(((X207|(~X207|(ccfv @ (ccfv @ X212 @ (cccnv @ X210)) @ X210)=(X212))|X207|(X210)!=(ccfv @ X211 @ (ccfv @ X209 @ ccmpd))|(X208)!=(ccfv @ X209 @ cclh))&(~cwcel @ X212 @ (ccrn @ X210)|(~X207|(ccfv @ (ccfv @ X212 @ (cccnv @ X210)) @ X210)=(X212))|X207|(X210)!=(ccfv @ X211 @ (ccfv @ X209 @ ccmpd))|(X208)!=(ccfv @ X209 @ cclh)))&((X207|(~X207|(ccfv @ (ccfv @ X212 @ (cccnv @ X210)) @ X210)=(X212))|(~cwcel @ X209 @ cchlt|~cwcel @ X211 @ X208)|(X210)!=(ccfv @ X211 @ (ccfv @ X209 @ ccmpd))|(X208)!=(ccfv @ X209 @ cclh))&(~cwcel @ X212 @ (ccrn @ X210)|(~X207|(ccfv @ (ccfv @ X212 @ (cccnv @ X210)) @ X210)=(X212))|(~cwcel @ X209 @ cchlt|~cwcel @ X211 @ X208)|(X210)!=(ccfv @ X211 @ (ccfv @ X209 @ ccmpd))|(X208)!=(ccfv @ X209 @ cclh)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amapdcnvid2_thm])])])).
thf(c_0_70, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccrn @ X3)|(X4)!=(epred5_0)|(X3)!=(epred9_0)|~cwcel @ X2 @ X4), inference(spm,[status(thm)],[c_0_58, c_0_27])).
thf(c_0_71, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ (cccnv @ X3)) @ X4|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ X8 @ cchlt|~cwcel @ X9 @ X10|(X4)!=(ccfv @ X11 @ cclss)|(X11)!=(ccfv @ X9 @ (ccfv @ X8 @ ccdvh))|(X3)!=(ccfv @ X9 @ (ccfv @ X8 @ ccmpd))|(X10)!=(ccfv @ X8 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_59])])])).
thf(c_0_72, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X8:$i > $o, X12:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o]:(cwss @ (ccfv @ X2 @ X4) @ (ccfv @ X3 @ X4)|~cwss @ X2 @ X3|~cwcel @ X3 @ X8|~cwcel @ X2 @ X8|~cwcel @ X9 @ cchlt|~cwcel @ X10 @ X11|(X4)!=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))|(X8)!=(ccfv @ X12 @ cclss)|(X12)!=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))|(X11)!=(ccfv @ X9 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_60])])])).
thf(c_0_73, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X9:$i > $o]:(cwss @ (cco @ X2 @ X4 @ X8) @ X3|~cwss @ X2 @ X3|~cwss @ X4 @ X3|~cwcel @ X2 @ (ccfv @ X9 @ ccsubg)|~cwcel @ X4 @ (ccfv @ X9 @ ccsubg)|~cwcel @ X3 @ (ccfv @ X9 @ ccsubg)|(X8)!=(ccfv @ X9 @ cclsm)), inference(split_conjunct,[status(thm)],[c_0_61])).
thf(c_0_74, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2|~cwss @ epred5_0 @ X2), inference(spm,[status(thm)],[c_0_40, c_0_62])).
thf(c_0_75, negated_conjecture, ![X2:$i > $o]:(cwss @ epred12_0 @ (cco @ epred11_0 @ epred12_0 @ X2)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_63, c_0_64])).
thf(c_0_76, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ X2 @ (cco @ X2 @ epred12_0 @ X3)|(X3)!=(epred4_0)|~cwcel @ X2 @ (ccfv @ epred6_0 @ ccsubg)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_54]), c_0_39])).
thf(c_0_77, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X13:$i > $o, X12:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o]:(cwcel @ (cco @ X4 @ X2 @ X8) @ (ccrn @ X3)|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ X4 @ (ccrn @ X3)|~cwcel @ X9 @ cchlt|~cwcel @ X10 @ X11|(X8)!=(ccfv @ X12 @ cclsm)|(X12)!=(ccfv @ X10 @ (ccfv @ X9 @ cclcd))|(X13)!=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))|(X3)!=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))|(X11)!=(ccfv @ X9 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_66])])])).
thf(c_0_78, negated_conjecture, ![X3:$i > $o, X8:$i > $o, X4:$i > $o, X2:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ X4|(X4)!=(ccfv @ X8 @ cclss)|(X9)!=(ccfv @ X10 @ cclss)|(X10)!=(epred6_0)|(X8)!=(epred2_0)|(X3)!=(epred9_0)|(X11)!=(epred7_0)|~cwcel @ epred10_0 @ X11|~cwcel @ X2 @ X9), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_22]), c_0_68]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_79, plain, ![X2:$i > $o, X3:$i > $o, X9:$i > $o, X8:$i > $o, X4:$i > $o]:((ccfv @ (ccfv @ X2 @ (cccnv @ X3)) @ X3)=(X2)|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ X4 @ cchlt|~cwcel @ X8 @ X9|(X3)!=(ccfv @ X8 @ (ccfv @ X4 @ ccmpd))|(X9)!=(ccfv @ X4 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_69])])])).
thf(c_0_80, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2) @ (ccrn @ X2)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_70, c_0_62])).
thf(c_0_81, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:(cwcel @ (ccfv @ X2 @ (cccnv @ X3)) @ X4|(X4)!=(ccfv @ (ccfv @ X8 @ (ccfv @ X9 @ ccdvh)) @ cclss)|(X3)!=(ccfv @ X8 @ (ccfv @ X9 @ ccmpd))|(X10)!=(ccfv @ X9 @ cclh)|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ X9 @ cchlt|~cwcel @ X8 @ X10), inference(er,[status(thm)],[c_0_71])).
thf(c_0_82, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X10:$i > $o, X9:$i > $o, X8:$i > $o, X4:$i > $o]:(cwss @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ X3)|(X8)!=(ccfv @ X9 @ cclss)|(X9)!=(epred6_0)|(X3)!=(epred9_0)|(X10)!=(epred7_0)|~cwcel @ epred10_0 @ X10|~cwcel @ X4 @ X8|~cwcel @ X2 @ X8|~cwss @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_83, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwss @ (cco @ X2 @ epred12_0 @ X3) @ X4|(X3)!=(epred4_0)|~cwcel @ X4 @ (ccfv @ epred6_0 @ ccsubg)|~cwcel @ X2 @ (ccfv @ epred6_0 @ ccsubg)|~cwss @ epred12_0 @ X4|~cwss @ X2 @ X4), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_54]), c_0_39])).
thf(c_0_84, negated_conjecture, cwcel @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ epred6_0 @ ccsubg), inference(spm,[status(thm)],[c_0_74, c_0_49])).
thf(c_0_85, negated_conjecture, cwss @ epred12_0 @ (cco @ epred11_0 @ epred12_0 @ epred4_0), inference(er,[status(thm)],[c_0_75])).
thf(c_0_86, negated_conjecture, ![X2:$i > $o]:(cwss @ epred11_0 @ (cco @ epred11_0 @ epred12_0 @ X2)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_76, c_0_64])).
thf(c_0_87, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ X4) @ (ccrn @ X8)|(X9)!=(ccfv @ X10 @ (ccfv @ X11 @ cclcd))|(X8)!=(ccfv @ X10 @ (ccfv @ X11 @ ccmpd))|(X12)!=(ccfv @ X11 @ cclh)|(X4)!=(ccfv @ X9 @ cclsm)|~cwcel @ X2 @ (ccrn @ X8)|~cwcel @ X3 @ (ccrn @ X8)|~cwcel @ X11 @ cchlt|~cwcel @ X10 @ X12), inference(er,[status(thm)],[c_0_77])).
thf(c_0_88, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred11_0 @ X2) @ (ccrn @ X2)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_70, c_0_50])).
thf(c_0_89, negated_conjecture, ![X3:$i > $o, X4:$i > $o, X2:$i > $o, X10:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ cclss)|(X8)!=(ccfv @ X9 @ cclss)|(X9)!=(epred6_0)|(X4)!=(epred2_0)|(X3)!=(epred9_0)|(X10)!=(epred7_0)|~cwcel @ epred10_0 @ X10|~cwcel @ X2 @ X8), inference(er,[status(thm)],[c_0_78])).
thf(c_0_90, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((ccfv @ (ccfv @ X2 @ (cccnv @ X3)) @ X3)=(X2)|(X3)!=(epred9_0)|(X4)!=(epred7_0)|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ epred10_0 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_91, negated_conjecture, cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccrn @ epred9_0), inference(er,[status(thm)],[c_0_80])).
thf(c_0_92, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ (cccnv @ X3)) @ X4|(X4)!=(epred5_0)|(X3)!=(epred9_0)|(X8)!=(epred7_0)|~cwcel @ X2 @ (ccrn @ X3)|~cwcel @ epred10_0 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_22]), c_0_35]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_93, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X9:$i > $o, X8:$i > $o, X4:$i > $o]:(cwss @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ X3)|(X8)!=(epred5_0)|(X3)!=(epred9_0)|(X9)!=(epred7_0)|~cwcel @ epred10_0 @ X9|~cwcel @ X4 @ X8|~cwcel @ X2 @ X8|~cwss @ X2 @ X4), inference(spm,[status(thm)],[c_0_82, c_0_35])).
thf(c_0_94, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ (cco @ X2 @ epred12_0 @ X3) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(X3)!=(epred4_0)|~cwss @ X2 @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|~cwcel @ X2 @ (ccfv @ epred6_0 @ ccsubg)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_84]), c_0_85])])).
thf(c_0_95, negated_conjecture, cwss @ epred11_0 @ (cco @ epred11_0 @ epred12_0 @ epred4_0), inference(er,[status(thm)],[c_0_86])).
thf(c_0_96, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ X4) @ (ccrn @ X8)|(X4)!=(ccfv @ X9 @ cclsm)|(X9)!=(epred2_0)|(X8)!=(epred9_0)|(X10)!=(epred7_0)|~cwcel @ X2 @ (ccrn @ X8)|~cwcel @ X3 @ (ccrn @ X8)|~cwcel @ epred10_0 @ X10), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_68]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_97, negated_conjecture, cwcel @ (ccfv @ epred11_0 @ epred9_0) @ (ccrn @ epred9_0), inference(er,[status(thm)],[c_0_88])).
thf(c_0_98, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred12_0 @ X2) @ (ccrn @ X2)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_70, c_0_41])).
thf(c_0_99, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ cclss)|(X8)!=(epred5_0)|(X4)!=(epred2_0)|(X3)!=(epred9_0)|(X9)!=(epred7_0)|~cwcel @ epred10_0 @ X9|~cwcel @ X2 @ X8), inference(spm,[status(thm)],[c_0_89, c_0_35])).
thf(c_0_100, plain, ![X185:$o, X186:$i > $o, X187:$i > $o, X188:$i > $o, X189:$i > $o]:((X185|(~X185|cwcel @ X186 @ cclmod)|(X186)!=(ccfv @ X189 @ (ccfv @ X188 @ cclcd))|(X187)!=(ccfv @ X188 @ cclh))&(~cwcel @ X188 @ cchlt|~cwcel @ X189 @ X187|(~X185|cwcel @ X186 @ cclmod)|(X186)!=(ccfv @ X189 @ (ccfv @ X188 @ cclcd))|(X187)!=(ccfv @ X188 @ cclh))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alcdlmod_thm])])])).
thf(c_0_101, negated_conjecture, ![X2:$i > $o]:((ccfv @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ epred9_0)=(ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_90, c_0_91])).
thf(c_0_102, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X2|(X2)!=(epred5_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(spm,[status(thm)],[c_0_92, c_0_91])).
thf(c_0_103, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X8:$i > $o, X4:$i > $o]:(cwss @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ X3)|(X8)!=(epred5_0)|(X3)!=(epred9_0)|~cwcel @ X4 @ X8|~cwcel @ X2 @ X8|~cwss @ X2 @ X4), inference(spm,[status(thm)],[c_0_93, c_0_27])).
thf(c_0_104, negated_conjecture, ![X2:$i > $o]:(cwss @ (cco @ epred11_0 @ epred12_0 @ X2) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_64])])).
thf(c_0_105, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X8:$i > $o]:(cwcel @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ X2 @ X3) @ (ccrn @ epred9_0)|(X3)!=(ccfv @ X4 @ cclsm)|(X4)!=(epred2_0)|(X8)!=(epred7_0)|~cwcel @ X2 @ (ccrn @ epred9_0)|~cwcel @ epred10_0 @ X8), inference(spm,[status(thm)],[c_0_96, c_0_97])).
thf(c_0_106, negated_conjecture, cwcel @ (ccfv @ epred12_0 @ epred9_0) @ (ccrn @ epred9_0), inference(er,[status(thm)],[c_0_98])).
thf(c_0_107, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ cclss)|(X8)!=(epred5_0)|(X4)!=(epred2_0)|(X3)!=(epred9_0)|~cwcel @ X2 @ X8), inference(spm,[status(thm)],[c_0_99, c_0_27])).
thf(c_0_108, plain, ![X8:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwcel @ X8 @ cclmod|~cwcel @ X2 @ cchlt|~cwcel @ X3 @ X4|(X8)!=(ccfv @ X3 @ (ccfv @ X2 @ cclcd))|(X4)!=(ccfv @ X2 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_100])])])).
thf(c_0_109, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X12:$i > $o, X11:$i > $o, X10:$i > $o, X9:$i > $o]:(cwss @ X2 @ X4|~cwss @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ X3)|~cwcel @ X4 @ X8|~cwcel @ X2 @ X8|~cwcel @ X9 @ cchlt|~cwcel @ X10 @ X11|(X3)!=(ccfv @ X10 @ (ccfv @ X9 @ ccmpd))|(X8)!=(ccfv @ X12 @ cclss)|(X12)!=(ccfv @ X10 @ (ccfv @ X9 @ ccdvh))|(X11)!=(ccfv @ X9 @ cclh)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_60])])])).
thf(c_0_110, negated_conjecture, (ccfv @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ epred9_0)=(ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0), inference(spm,[status(thm)],[c_0_101, c_0_27])).
thf(c_0_111, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X2|(X2)!=(epred5_0)), inference(spm,[status(thm)],[c_0_102, c_0_27])).
thf(c_0_112, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ (ccfv @ X2 @ X3) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X3)|(X3)!=(epred9_0)|~cwss @ X2 @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|~cwcel @ X2 @ epred5_0), inference(spm,[status(thm)],[c_0_103, c_0_62])).
thf(c_0_113, negated_conjecture, cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (cco @ epred11_0 @ epred12_0 @ epred4_0), inference(er,[status(thm)],[c_0_104])).
thf(c_0_114, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2) @ (ccrn @ epred9_0)|(X2)!=(ccfv @ X3 @ cclsm)|(X3)!=(epred2_0)|(X4)!=(epred7_0)|~cwcel @ epred10_0 @ X4), inference(spm,[status(thm)],[c_0_105, c_0_106])).
thf(c_0_115, negated_conjecture, (epred3_0)=(ccfv @ epred2_0 @ cclsm), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_116, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (ccfv @ epred12_0 @ X2) @ (ccfv @ X3 @ cclss)|(X3)!=(epred2_0)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_107, c_0_41])).
thf(c_0_117, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ cclmod|(X2)!=(epred2_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_68]), c_0_23]), c_0_24])])).
thf(c_0_118, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X8:$i > $o, X9:$i > $o, X4:$i > $o, X10:$i > $o]:(cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X2|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(X9)!=(ccfv @ X4 @ cclh)|(X10)!=(ccfv @ X8 @ cclss)|~cwcel @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X10|~cwss @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccfv @ X2 @ epred9_0)|~cwcel @ X4 @ cchlt|~cwcel @ X3 @ X9|~cwcel @ X2 @ X10), inference(spm,[status(thm)],[c_0_109, c_0_110])).
thf(c_0_119, negated_conjecture, cwcel @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ epred5_0, inference(er,[status(thm)],[c_0_111])).
thf(c_0_120, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2)|(X2)!=(epred9_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_113]), c_0_62])])).
thf(c_0_121, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2) @ (ccrn @ epred9_0)|(X2)!=(epred3_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(spm,[status(thm)],[c_0_114, c_0_115])).
thf(c_0_122, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred12_0 @ X2) @ (ccfv @ epred2_0 @ cclss)|(X2)!=(epred9_0)), inference(er,[status(thm)],[c_0_116])).
thf(c_0_123, negated_conjecture, ![X2:$i > $o]:(cwcel @ X2 @ cclmod|(X2)!=(epred2_0)), inference(spm,[status(thm)],[c_0_117, c_0_27])).
thf(c_0_124, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (ccfv @ epred11_0 @ X2) @ (ccfv @ X3 @ cclss)|(X3)!=(epred2_0)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_107, c_0_50])).
thf(c_0_125, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:(cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X2|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(ccfv @ X8 @ cclss)!=(epred5_0)|(X9)!=(ccfv @ X4 @ cclh)|~cwss @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccfv @ X2 @ epred9_0)|~cwcel @ X4 @ cchlt|~cwcel @ X2 @ epred5_0|~cwcel @ X3 @ X9), inference(spm,[status(thm)],[c_0_118, c_0_119])).
thf(c_0_126, negated_conjecture, cwss @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0), inference(er,[status(thm)],[c_0_120])).
thf(c_0_127, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X8:$i > $o, X9:$i > $o, X4:$i > $o, X10:$i > $o]:(cwss @ X2 @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(X9)!=(ccfv @ X4 @ cclh)|(X10)!=(ccfv @ X8 @ cclss)|~cwcel @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ X10|~cwss @ (ccfv @ X2 @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|~cwcel @ X4 @ cchlt|~cwcel @ X3 @ X9|~cwcel @ X2 @ X10), inference(spm,[status(thm)],[c_0_109, c_0_110])).
thf(c_0_128, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2) @ (ccfv @ X3 @ cclss)|(X3)!=(epred2_0)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_107, c_0_62])).
thf(c_0_129, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2) @ (ccrn @ epred9_0)|(X2)!=(epred3_0)), inference(spm,[status(thm)],[c_0_121, c_0_27])).
thf(c_0_130, negated_conjecture, cwcel @ (ccfv @ epred12_0 @ epred9_0) @ (ccfv @ epred2_0 @ cclss), inference(er,[status(thm)],[c_0_122])).
thf(c_0_131, plain, ![X2:$i > $o]:(cwss @ (ccfv @ X2 @ cclss) @ (ccfv @ X2 @ ccsubg)|~cwcel @ X2 @ cclmod), inference(er,[status(thm)],[c_0_34])).
thf(c_0_132, negated_conjecture, cwcel @ epred2_0 @ cclmod, inference(er,[status(thm)],[c_0_123])).
thf(c_0_133, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred11_0 @ X2) @ (ccfv @ epred2_0 @ cclss)|(X2)!=(epred9_0)), inference(er,[status(thm)],[c_0_124])).
thf(c_0_134, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(ccfv @ X2 @ (ccfv @ X3 @ ccmpd))!=(epred9_0)|(X4)!=(ccfv @ X2 @ (ccfv @ X3 @ ccdvh))|(ccfv @ X4 @ cclss)!=(epred5_0)|(X8)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X2 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125, c_0_126]), c_0_62])])).
thf(c_0_135, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:(cwss @ X2 @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(ccfv @ X8 @ cclss)!=(epred5_0)|(X9)!=(ccfv @ X4 @ cclh)|~cwss @ (ccfv @ X2 @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|~cwcel @ X4 @ cchlt|~cwcel @ X2 @ epred5_0|~cwcel @ X3 @ X9), inference(spm,[status(thm)],[c_0_127, c_0_119])).
thf(c_0_136, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2) @ (ccfv @ epred2_0 @ cclss)|(X2)!=(epred9_0)), inference(er,[status(thm)],[c_0_128])).
thf(c_0_137, negated_conjecture, cwcel @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (ccrn @ epred9_0), inference(er,[status(thm)],[c_0_129])).
thf(c_0_138, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred12_0 @ epred9_0) @ X2|~cwss @ (ccfv @ epred2_0 @ cclss) @ X2), inference(spm,[status(thm)],[c_0_40, c_0_130])).
thf(c_0_139, negated_conjecture, cwss @ (ccfv @ epred2_0 @ cclss) @ (ccfv @ epred2_0 @ ccsubg), inference(spm,[status(thm)],[c_0_131, c_0_132])).
thf(c_0_140, negated_conjecture, cwcel @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred2_0 @ cclss), inference(er,[status(thm)],[c_0_133])).
thf(c_0_141, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(ccfv @ X2 @ cclss)!=(epred5_0)|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_142, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ (ccfv @ X3 @ ccmpd))!=(epred9_0)|(X4)!=(ccfv @ X2 @ (ccfv @ X3 @ ccdvh))|(ccfv @ X4 @ cclss)!=(epred5_0)|(X8)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X2 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_126]), c_0_62])])).
thf(c_0_143, negated_conjecture, cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccfv @ epred2_0 @ cclss), inference(er,[status(thm)],[c_0_136])).
thf(c_0_144, negated_conjecture, ![X2:$i > $o]:((ccfv @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ epred9_0)=(cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0)|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_90, c_0_137])).
thf(c_0_145, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ X2|(X2)!=(epred5_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(spm,[status(thm)],[c_0_92, c_0_137])).
thf(c_0_146, negated_conjecture, cwcel @ (ccfv @ epred12_0 @ epred9_0) @ (ccfv @ epred2_0 @ ccsubg), inference(spm,[status(thm)],[c_0_138, c_0_139])).
thf(c_0_147, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred11_0 @ epred9_0) @ X2|~cwss @ (ccfv @ epred2_0 @ cclss) @ X2), inference(spm,[status(thm)],[c_0_40, c_0_140])).
thf(c_0_148, plain, ![X153:$o, X154:$i > $o, X155:$i > $o]:(((X153|(~X153|(X154)=(X155))|X153)&(~cwss @ X155 @ X154|(~X153|(X154)=(X155))|X153))&((X153|(~X153|(X154)=(X155))|~cwss @ X154 @ X155)&(~cwss @ X155 @ X154|(~X153|(X154)=(X155))|~cwss @ X154 @ X155))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aeqssd_thm])])])).
thf(c_0_149, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_141, c_0_35])).
thf(c_0_150, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ cclss)!=(epred5_0)|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_151, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ X2|~cwss @ (ccfv @ epred2_0 @ cclss) @ X2), inference(spm,[status(thm)],[c_0_40, c_0_143])).
thf(c_0_152, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ epred12_0 @ X2) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2)|(X2)!=(epred9_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_85]), c_0_41])])).
thf(c_0_153, negated_conjecture, (ccfv @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ epred9_0)=(cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0), inference(spm,[status(thm)],[c_0_144, c_0_27])).
thf(c_0_154, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ X2|(X2)!=(epred5_0)), inference(spm,[status(thm)],[c_0_145, c_0_27])).
thf(c_0_155, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ (ccfv @ epred12_0 @ epred9_0) @ (cco @ X2 @ (ccfv @ epred12_0 @ epred9_0) @ X3)|(X3)!=(epred3_0)|~cwcel @ X2 @ (ccfv @ epred2_0 @ ccsubg)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_146]), c_0_115])).
thf(c_0_156, negated_conjecture, cwcel @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred2_0 @ ccsubg), inference(spm,[status(thm)],[c_0_147, c_0_139])).
thf(c_0_157, plain, ![X3:$i > $o, X2:$i > $o]:((X3)=(X2)|~cwss @ X2 @ X3|~cwss @ X3 @ X2), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_148])])])).
thf(c_0_158, negated_conjecture, cwss @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0), inference(spm,[status(thm)],[c_0_149, c_0_27])).
thf(c_0_159, negated_conjecture, ![X2:$i > $o]:(cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_150, c_0_35])).
thf(c_0_160, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwss @ (cco @ X2 @ (ccfv @ epred12_0 @ epred9_0) @ X3) @ X4|(X3)!=(epred3_0)|~cwcel @ X4 @ (ccfv @ epred2_0 @ ccsubg)|~cwcel @ X2 @ (ccfv @ epred2_0 @ ccsubg)|~cwss @ (ccfv @ epred12_0 @ epred9_0) @ X4|~cwss @ X2 @ X4), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_146]), c_0_115])).
thf(c_0_161, negated_conjecture, cwcel @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (ccfv @ epred2_0 @ ccsubg), inference(spm,[status(thm)],[c_0_151, c_0_139])).
thf(c_0_162, negated_conjecture, cwss @ (ccfv @ epred12_0 @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0), inference(er,[status(thm)],[c_0_152])).
thf(c_0_163, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ epred11_0 @ X2) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ X2)|(X2)!=(epred9_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_95]), c_0_50])])).
thf(c_0_164, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X8:$i > $o, X9:$i > $o, X4:$i > $o, X10:$i > $o]:(cwss @ X2 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(X9)!=(ccfv @ X4 @ cclh)|(X10)!=(ccfv @ X8 @ cclss)|~cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ X10|~cwss @ (ccfv @ X2 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0)|~cwcel @ X4 @ cchlt|~cwcel @ X3 @ X9|~cwcel @ X2 @ X10), inference(spm,[status(thm)],[c_0_109, c_0_153])).
thf(c_0_165, negated_conjecture, cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ epred5_0, inference(er,[status(thm)],[c_0_154])).
thf(c_0_166, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ epred12_0 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2)|(X2)!=(epred3_0)), inference(spm,[status(thm)],[c_0_155, c_0_156])).
thf(c_0_167, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ X2 @ (cco @ X2 @ (ccfv @ epred12_0 @ epred9_0) @ X3)|(X3)!=(epred3_0)|~cwcel @ X2 @ (ccfv @ epred2_0 @ ccsubg)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_146]), c_0_115])).
thf(c_0_168, negated_conjecture, ((ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))=(cco @ epred11_0 @ epred12_0 @ epred4_0)|~cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))), inference(spm,[status(thm)],[c_0_157, c_0_158])).
thf(c_0_169, negated_conjecture, cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0)), inference(spm,[status(thm)],[c_0_159, c_0_27])).
thf(c_0_170, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ (cco @ X2 @ (ccfv @ epred12_0 @ epred9_0) @ X3) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|(X3)!=(epred3_0)|~cwss @ X2 @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|~cwcel @ X2 @ (ccfv @ epred2_0 @ ccsubg)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_160, c_0_161]), c_0_162])])).
thf(c_0_171, negated_conjecture, cwss @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0), inference(er,[status(thm)],[c_0_163])).
thf(c_0_172, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:(cwss @ X2 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(ccfv @ X8 @ cclss)!=(epred5_0)|(X9)!=(ccfv @ X4 @ cclh)|~cwss @ (ccfv @ X2 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0)|~cwcel @ X4 @ cchlt|~cwcel @ X2 @ epred5_0|~cwcel @ X3 @ X9), inference(spm,[status(thm)],[c_0_164, c_0_165])).
thf(c_0_173, negated_conjecture, cwss @ (ccfv @ epred12_0 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0), inference(er,[status(thm)],[c_0_166])).
thf(c_0_174, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ epred11_0 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2)|(X2)!=(epred3_0)), inference(spm,[status(thm)],[c_0_167, c_0_156])).
thf(c_0_175, negated_conjecture, (ccfv @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0) @ (cccnv @ epred9_0))=(cco @ epred11_0 @ epred12_0 @ epred4_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_168, c_0_169])])).
thf(c_0_176, negated_conjecture, ![X2:$i > $o]:(cwss @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ X2) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|(X2)!=(epred3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170, c_0_171]), c_0_156])])).
thf(c_0_177, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwss @ epred12_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ (ccfv @ X3 @ ccmpd))!=(epred9_0)|(X4)!=(ccfv @ X2 @ (ccfv @ X3 @ ccdvh))|(ccfv @ X4 @ cclss)!=(epred5_0)|(X8)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X2 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_172, c_0_173]), c_0_41])])).
thf(c_0_178, negated_conjecture, cwss @ (ccfv @ epred11_0 @ epred9_0) @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0), inference(er,[status(thm)],[c_0_174])).
thf(c_0_179, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:(cwss @ X2 @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(ccfv @ X3 @ (ccfv @ X4 @ ccmpd))!=(epred9_0)|(X8)!=(ccfv @ X3 @ (ccfv @ X4 @ ccdvh))|(ccfv @ X8 @ cclss)!=(epred5_0)|(X9)!=(ccfv @ X4 @ cclh)|~cwss @ (ccfv @ X2 @ epred9_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)|~cwcel @ X4 @ cchlt|~cwcel @ X2 @ epred5_0|~cwcel @ X3 @ X9), inference(rw,[status(thm)],[c_0_135, c_0_175])).
thf(c_0_180, negated_conjecture, cwss @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0), inference(er,[status(thm)],[c_0_176])).
thf(c_0_181, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwss @ epred12_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ cclss)!=(epred5_0)|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_182, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwss @ epred11_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ (ccfv @ X3 @ ccmpd))!=(epred9_0)|(X4)!=(ccfv @ X2 @ (ccfv @ X3 @ ccdvh))|(ccfv @ X4 @ cclss)!=(epred5_0)|(X8)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X2 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_172, c_0_178]), c_0_50])])).
thf(c_0_183, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o]:(cwss @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(ccfv @ X2 @ (ccfv @ X3 @ ccmpd))!=(epred9_0)|(X4)!=(ccfv @ X2 @ (ccfv @ X3 @ ccdvh))|(ccfv @ X4 @ cclss)!=(epred5_0)|(X8)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X2 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179, c_0_153]), c_0_180]), c_0_165])])).
thf(c_0_184, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ X2|~cwss @ epred5_0 @ X2), inference(spm,[status(thm)],[c_0_40, c_0_165])).
thf(c_0_185, negated_conjecture, ![X2:$i > $o]:(cwss @ epred12_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_181, c_0_35])).
thf(c_0_186, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwss @ epred11_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(ccfv @ X2 @ cclss)!=(epred5_0)|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_182, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_187, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwss @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(ccfv @ X2 @ cclss)!=(epred5_0)|(X2)!=(epred6_0)|(X3)!=(epred7_0)|~cwcel @ epred10_0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183, c_0_22]), c_0_45]), c_0_23]), c_0_24])])).
thf(c_0_188, negated_conjecture, cwcel @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ (ccfv @ epred6_0 @ ccsubg), inference(spm,[status(thm)],[c_0_184, c_0_49])).
thf(c_0_189, negated_conjecture, cwss @ epred12_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)), inference(spm,[status(thm)],[c_0_185, c_0_27])).
thf(c_0_190, negated_conjecture, ![X2:$i > $o]:(cwss @ epred11_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_186, c_0_35])).
thf(c_0_191, negated_conjecture, ![X2:$i > $o]:(cwss @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0)|(X2)!=(epred7_0)|~cwcel @ epred10_0 @ X2), inference(spm,[status(thm)],[c_0_187, c_0_35])).
thf(c_0_192, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwss @ (cco @ X2 @ epred12_0 @ X3) @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(X3)!=(epred4_0)|~cwss @ X2 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|~cwcel @ X2 @ (ccfv @ epred6_0 @ ccsubg)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_188]), c_0_189])])).
thf(c_0_193, negated_conjecture, cwss @ epred11_0 @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)), inference(spm,[status(thm)],[c_0_190, c_0_27])).
thf(c_0_194, negated_conjecture, cwss @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)) @ (cco @ epred11_0 @ epred12_0 @ epred4_0), inference(spm,[status(thm)],[c_0_191, c_0_27])).
thf(c_0_195, negated_conjecture, ![X2:$i > $o]:(cwss @ (cco @ epred11_0 @ epred12_0 @ X2) @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_192, c_0_193]), c_0_64])])).
thf(c_0_196, negated_conjecture, ((ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))=(cco @ epred11_0 @ epred12_0 @ epred4_0)|~cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))), inference(spm,[status(thm)],[c_0_157, c_0_194])).
thf(c_0_197, negated_conjecture, cwss @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0)), inference(er,[status(thm)],[c_0_195])).
thf(c_0_198, negated_conjecture, (ccfv @ (cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0) @ (cccnv @ epred9_0))=(cco @ epred11_0 @ epred12_0 @ epred4_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_196, c_0_197])])).
thf(c_0_199, negated_conjecture, (ccfv @ (cco @ epred11_0 @ epred12_0 @ epred4_0) @ epred9_0)!=(cco @ (ccfv @ epred11_0 @ epred9_0) @ (ccfv @ epred12_0 @ epred9_0) @ epred3_0), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_200, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_198]), c_0_199]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 201
# Proof object clause steps            : 168
# Proof object formula steps           : 33
# Proof object conjectures             : 151
# Proof object clause conjectures      : 148
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 29
# Proof object initial formulas used   : 16
# Proof object generating inferences   : 131
# Proof object simplifying inferences  : 117
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 63
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 195
# Removed in clause preprocessing      : 164
# Initial clauses in saturation        : 31
# Processed clauses                    : 11021
# ...of these trivial                  : 174
# ...subsumed                          : 2834
# ...remaining for further processing  : 8013
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 291
# Backward-rewritten                   : 2607
# Generated clauses                    : 35904
# ...of the previous two non-trivial   : 37293
# Contextual simplify-reflections      : 0
# Paramodulations                      : 31976
# Factorizations                       : 0
# NegExts                              : 0
# Equation resolutions                 : 3155
# Propositional unsat checks           : 0
#    Propositional check models        : 0
#    Propositional check unsatisfiable : 0
#    Propositional clauses             : 0
#    Propositional clauses after purity: 0
#    Propositional unsat core size     : 0
#    Propositional preprocessing time  : 0.000
#    Propositional encoding time       : 0.000
#    Propositional solver time         : 0.000
#    Success case prop preproc time    : 0.000
#    Success case prop encoding time   : 0.000
#    Success case prop solver time     : 0.000
# Current number of processed clauses  : 4881
#    Positive orientable unit clauses  : 364
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 2
#    Non-unit-clauses                  : 4515
# Current number of unprocessed clauses: 22802
# ...number of literals in the above   : 41423
# Current number of archived formulas  : 0
# Current number of archived clauses   : 3132
# Clause-clause subsumption calls (NU) : 3059111
# Rec. Clause-clause subsumption calls : 1745687
# Non-unit clause-clause subsumptions  : 3107
# Unit Clause-clause subsumption calls : 139376
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 11720
# BW rewrite match successes           : 154
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 1173612

# -------------------------------------------------
# User time                : 1.948 s
# System time              : 0.032 s
# Total time               : 1.980 s
# Maximum resident set size: 38176 pages
