# Preprocessing time       : 0.031 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
thf(ccdleme30a_conj, conjecture, ![X2:$i > $o, X3:$i > $o, X13:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X15:$i > $o, X14:$i > $o, X16:$i > $o, X17:$i > $o, X24:$i]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>((X15)=(ccfv @ X11 @ ccmee)=>((X2)=(ccfv @ X11 @ ccatm)=>((X13)=(ccfv @ X11 @ cclh)=>((((cwcel @ X11 @ cchlt&cwcel @ X14 @ X13)&((cwcel @ (ccv @ X24) @ X2&(cwcel @ X16 @ X3&~(cwbr @ X16 @ X14 @ X21)))&cwcel @ X17 @ X3))&((cco @ (ccv @ X24) @ (cco @ X16 @ X14 @ X15) @ X18)=(X16)&cwbr @ X16 @ X17 @ X21))=>(cco @ (ccv @ X24) @ (cco @ X17 @ X14 @ X15) @ X18)=(X17)))))))), file('mmset36315_cdleme30a.p', ccdleme30a_conj)).
thf(alhpbase_thm, axiom, ![X3:$i > $o, X13:$i > $o, X11:$i > $o, X14:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X13)=(ccfv @ X11 @ cclh)=>(cwcel @ X14 @ X13=>cwcel @ X14 @ X3))), file('mmset36315_cdleme30a.p', alhpbase_thm)).
thf(ahllat_thm, axiom, ![X11:$i > $o]:(cwcel @ X11 @ cchlt=>cwcel @ X11 @ cclat), file('mmset36315_cdleme30a.p', ahllat_thm)).
thf(alatmcl_thm, axiom, ![X3:$i > $o, X11:$i > $o, X15:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X15)=(ccfv @ X11 @ ccmee)=>(((cwcel @ X11 @ cclat&cwcel @ X16 @ X3)&cwcel @ X17 @ X3)=>cwcel @ (cco @ X16 @ X17 @ X15) @ X3))), file('mmset36315_cdleme30a.p', alatmcl_thm)).
thf(aatbase_thm, axiom, ![X2:$i > $o, X3:$i > $o, X12:$i > $o, X11:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X2)=(ccfv @ X11 @ ccatm)=>(cwcel @ X12 @ X2=>cwcel @ X12 @ X3))), file('mmset36315_cdleme30a.p', aatbase_thm)).
thf(alatlej1_thm, axiom, ![X3:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>(((cwcel @ X11 @ cclat&cwcel @ X16 @ X3)&cwcel @ X17 @ X3)=>cwbr @ X16 @ (cco @ X16 @ X17 @ X18) @ X21)))), file('mmset36315_cdleme30a.p', alatlej1_thm)).
thf(alatleeqj2_thm, axiom, ![X3:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>(((cwcel @ X11 @ cclat&cwcel @ X16 @ X3)&cwcel @ X17 @ X3)=>(cwbr @ X16 @ X17 @ X21<=>(cco @ X17 @ X16 @ X18)=(X17)))))), file('mmset36315_cdleme30a.p', alatleeqj2_thm)).
thf(alatleeqj1_thm, axiom, ![X3:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>(((cwcel @ X11 @ cclat&cwcel @ X16 @ X3)&cwcel @ X17 @ X3)=>(cwbr @ X16 @ X17 @ X21<=>(cco @ X16 @ X17 @ X18)=(X17)))))), file('mmset36315_cdleme30a.p', alatleeqj1_thm)).
thf(alhpj1_thm, axiom, ![X3:$i > $o, X23:$i > $o, X13:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X14:$i > $o, X16:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>((X23)=(ccfv @ X11 @ ccp1)=>((X13)=(ccfv @ X11 @ cclh)=>(((cwcel @ X11 @ cchlt&cwcel @ X14 @ X13)&(cwcel @ X16 @ X3&~(cwbr @ X16 @ X14 @ X21)))=>(cco @ X14 @ X16 @ X18)=(X23))))))), file('mmset36315_cdleme30a.p', alhpj1_thm)).
thf(alatjass_thm, axiom, ![X3:$i > $o, X18:$i > $o, X11:$i > $o, X16:$i > $o, X17:$i > $o, X19:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X18)=(ccfv @ X11 @ ccjn)=>((cwcel @ X11 @ cclat&((cwcel @ X16 @ X3&cwcel @ X17 @ X3)&cwcel @ X19 @ X3))=>(cco @ (cco @ X16 @ X17 @ X18) @ X19 @ X18)=(cco @ X16 @ (cco @ X17 @ X19 @ X18) @ X18)))), file('mmset36315_cdleme30a.p', alatjass_thm)).
thf(alatjcl_thm, axiom, ![X3:$i > $o, X18:$i > $o, X11:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X18)=(ccfv @ X11 @ ccjn)=>(((cwcel @ X11 @ cclat&cwcel @ X16 @ X3)&cwcel @ X17 @ X3)=>cwcel @ (cco @ X16 @ X17 @ X18) @ X3))), file('mmset36315_cdleme30a.p', alatjcl_thm)).
thf(alhpmod2i2_thm, axiom, ![X3:$i > $o, X13:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X15:$i > $o, X14:$i > $o, X16:$i > $o, X17:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>((X15)=(ccfv @ X11 @ ccmee)=>((X13)=(ccfv @ X11 @ cclh)=>((((cwcel @ X11 @ cchlt&cwcel @ X14 @ X13)&(cwcel @ X16 @ X3&cwcel @ X17 @ X3))&cwbr @ X17 @ X16 @ X21)=>(cco @ (cco @ X16 @ X14 @ X15) @ X17 @ X18)=(cco @ X16 @ (cco @ X14 @ X17 @ X18) @ X15))))))), file('mmset36315_cdleme30a.p', alhpmod2i2_thm)).
thf(aolm11_thm, axiom, ![X3:$i > $o, X23:$i > $o, X11:$i > $o, X15:$i > $o, X16:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X15)=(ccfv @ X11 @ ccmee)=>((X23)=(ccfv @ X11 @ ccp1)=>((cwcel @ X11 @ ccol&cwcel @ X16 @ X3)=>(cco @ X16 @ X23 @ X15)=(X16))))), file('mmset36315_cdleme30a.p', aolm11_thm)).
thf(ahlol_thm, axiom, ![X11:$i > $o]:(cwcel @ X11 @ cchlt=>cwcel @ X11 @ ccol), file('mmset36315_cdleme30a.p', ahlol_thm)).
thf(alattrd_thm, axiom, ![X1:$o, X3:$i > $o, X11:$i > $o, X21:$i > $o, X16:$i > $o, X17:$i > $o, X19:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X1=>cwcel @ X11 @ cclat)=>((X1=>cwcel @ X16 @ X3)=>((X1=>cwcel @ X17 @ X3)=>((X1=>cwcel @ X19 @ X3)=>((X1=>cwbr @ X16 @ X17 @ X21)=>((X1=>cwbr @ X17 @ X19 @ X21)=>(X1=>cwbr @ X16 @ X19 @ X21))))))))), file('mmset36315_cdleme30a.p', alattrd_thm)).
thf(alatmlem1_thm, axiom, ![X3:$i > $o, X11:$i > $o, X21:$i > $o, X15:$i > $o, X16:$i > $o, X17:$i > $o, X19:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X15)=(ccfv @ X11 @ ccmee)=>((cwcel @ X11 @ cclat&((cwcel @ X16 @ X3&cwcel @ X17 @ X3)&cwcel @ X19 @ X3))=>(cwbr @ X16 @ X17 @ X21=>cwbr @ (cco @ X16 @ X19 @ X15) @ (cco @ X17 @ X19 @ X15) @ X21))))), file('mmset36315_cdleme30a.p', alatmlem1_thm)).
thf(c_0_16, negated_conjecture, ~(![X2:$i > $o, X3:$i > $o, X13:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X15:$i > $o, X14:$i > $o, X16:$i > $o, X17:$i > $o, X24:$i]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>((X15)=(ccfv @ X11 @ ccmee)=>((X2)=(ccfv @ X11 @ ccatm)=>((X13)=(ccfv @ X11 @ cclh)=>((((cwcel @ X11 @ cchlt&cwcel @ X14 @ X13)&((cwcel @ (ccv @ X24) @ X2&(cwcel @ X16 @ X3&~cwbr @ X16 @ X14 @ X21))&cwcel @ X17 @ X3))&((cco @ (ccv @ X24) @ (cco @ X16 @ X14 @ X15) @ X18)=(X16)&cwbr @ X16 @ X17 @ X21))=>(cco @ (ccv @ X24) @ (cco @ X17 @ X14 @ X15) @ X18)=(X17))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[ccdleme30a_conj])])).
thf(c_0_17, plain, ![X265:$i > $o, X266:$i > $o, X267:$i > $o, X268:$i > $o]:((X265)!=(ccfv @ X267 @ ccbs)|((X266)!=(ccfv @ X267 @ cclh)|(~cwcel @ X268 @ X266|cwcel @ X268 @ X265))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alhpbase_thm])])).
thf(c_0_18, negated_conjecture, ((epred2_0)=(ccfv @ epred5_0 @ ccbs)&((epred6_0)=(ccfv @ epred5_0 @ ccple)&((epred4_0)=(ccfv @ epred5_0 @ ccjn)&((epred7_0)=(ccfv @ epred5_0 @ ccmee)&((epred1_0)=(ccfv @ epred5_0 @ ccatm)&((epred3_0)=(ccfv @ epred5_0 @ cclh)&((((cwcel @ epred5_0 @ cchlt&cwcel @ epred8_0 @ epred3_0)&((cwcel @ (ccv @ esk1_0) @ epred1_0&(cwcel @ epred9_0 @ epred2_0&~cwbr @ epred9_0 @ epred8_0 @ epred6_0))&cwcel @ epred10_0 @ epred2_0))&((cco @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred4_0)=(epred9_0)&cwbr @ epred9_0 @ epred10_0 @ epred6_0))&(cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0)!=(epred10_0)))))))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])).
thf(c_0_19, plain, ![X241:$i > $o]:(~cwcel @ X241 @ cchlt|cwcel @ X241 @ cclat), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ahllat_thm])])).
thf(c_0_20, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o]:(cwcel @ X5 @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ cclh)|~cwcel @ X5 @ X4), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_21, negated_conjecture, (epred3_0)=(ccfv @ epred5_0 @ cclh), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_22, negated_conjecture, (epred2_0)=(ccfv @ epred5_0 @ ccbs), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_23, plain, ![X269:$i > $o, X270:$i > $o, X271:$i > $o, X272:$i > $o, X273:$i > $o]:((X269)!=(ccfv @ X270 @ ccbs)|((X271)!=(ccfv @ X270 @ ccmee)|(~cwcel @ X270 @ cclat|~cwcel @ X272 @ X269|~cwcel @ X273 @ X269|cwcel @ (cco @ X272 @ X273 @ X271) @ X269))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatmcl_thm])])).
thf(c_0_24, plain, ![X2:$i > $o]:(cwcel @ X2 @ cclat|~cwcel @ X2 @ cchlt), inference(split_conjunct,[status(thm)],[c_0_19])).
thf(c_0_25, negated_conjecture, cwcel @ epred5_0 @ cchlt, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_26, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ X2 @ X3|(X4)!=(epred3_0)|(X3)!=(epred2_0)|~cwcel @ X2 @ X4), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])).
thf(c_0_27, negated_conjecture, cwcel @ epred8_0 @ epred3_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_28, plain, ![X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X5 @ X11 @ X4) @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccmee)|~cwcel @ X3 @ cclat|~cwcel @ X5 @ X2|~cwcel @ X11 @ X2), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_29, negated_conjecture, (epred7_0)=(ccfv @ epred5_0 @ ccmee), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_30, negated_conjecture, cwcel @ epred5_0 @ cclat, inference(spm,[status(thm)],[c_0_24, c_0_25])).
thf(c_0_31, negated_conjecture, ![X2:$i > $o]:(cwcel @ epred8_0 @ X2|(X2)!=(epred2_0)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
thf(c_0_32, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ X4) @ X5|(X4)!=(epred7_0)|(X5)!=(epred2_0)|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_22]), c_0_30])])).
thf(c_0_33, negated_conjecture, cwcel @ epred8_0 @ epred2_0, inference(er,[status(thm)],[c_0_31])).
thf(c_0_34, plain, ![X247:$i > $o, X248:$i > $o, X249:$i > $o, X250:$i > $o]:((X248)!=(ccfv @ X250 @ ccbs)|((X247)!=(ccfv @ X250 @ ccatm)|(~cwcel @ X249 @ X247|cwcel @ X249 @ X248))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aatbase_thm])])).
thf(c_0_35, plain, ![X398:$i > $o, X399:$i > $o, X400:$i > $o, X401:$i > $o, X402:$i > $o, X403:$i > $o]:((X398)!=(ccfv @ X400 @ ccbs)|((X401)!=(ccfv @ X400 @ ccple)|((X399)!=(ccfv @ X400 @ ccjn)|(~cwcel @ X400 @ cclat|~cwcel @ X402 @ X398|~cwcel @ X403 @ X398|cwbr @ X402 @ (cco @ X402 @ X403 @ X399) @ X401)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatlej1_thm])])).
thf(c_0_36, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X2 @ epred8_0 @ X3) @ epred2_0|(X3)!=(epred7_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_32, c_0_33])).
thf(c_0_37, negated_conjecture, cwcel @ epred9_0 @ epred2_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_38, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o]:(cwcel @ X5 @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccatm)|~cwcel @ X5 @ X4), inference(split_conjunct,[status(thm)],[c_0_34])).
thf(c_0_39, negated_conjecture, (epred1_0)=(ccfv @ epred5_0 @ ccatm), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_40, plain, ![X12:$i > $o, X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o, X2:$i > $o]:(cwbr @ X11 @ (cco @ X11 @ X12 @ X5) @ X4|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccple)|(X5)!=(ccfv @ X3 @ ccjn)|~cwcel @ X3 @ cclat|~cwcel @ X11 @ X2|~cwcel @ X12 @ X2), inference(split_conjunct,[status(thm)],[c_0_35])).
thf(c_0_41, negated_conjecture, (epred4_0)=(ccfv @ epred5_0 @ ccjn), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_42, negated_conjecture, (epred6_0)=(ccfv @ epred5_0 @ ccple), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_43, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ epred9_0 @ epred8_0 @ X2) @ epred2_0|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
thf(c_0_44, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ X2 @ X3|(X4)!=(epred1_0)|(X3)!=(epred2_0)|~cwcel @ X2 @ X4), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_22])).
thf(c_0_45, negated_conjecture, cwcel @ (ccv @ esk1_0) @ epred1_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_46, plain, ![X324:$i > $o, X325:$i > $o, X326:$i > $o, X327:$i > $o, X328:$i > $o, X329:$i > $o]:((~cwbr @ X328 @ X329 @ X327|(cco @ X329 @ X328 @ X325)=(X329)|(~cwcel @ X326 @ cclat|~cwcel @ X328 @ X324|~cwcel @ X329 @ X324)|(X325)!=(ccfv @ X326 @ ccjn)|(X327)!=(ccfv @ X326 @ ccple)|(X324)!=(ccfv @ X326 @ ccbs))&((cco @ X329 @ X328 @ X325)!=(X329)|cwbr @ X328 @ X329 @ X327|(~cwcel @ X326 @ cclat|~cwcel @ X328 @ X324|~cwcel @ X329 @ X324)|(X325)!=(ccfv @ X326 @ ccjn)|(X327)!=(ccfv @ X326 @ ccple)|(X324)!=(ccfv @ X326 @ ccbs))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatleeqj2_thm])])])).
thf(c_0_47, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X5:$i > $o, X11:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ X3 @ X4) @ X5|(X4)!=(epred4_0)|(X5)!=(epred6_0)|(X11)!=(epred2_0)|~cwcel @ X3 @ X11|~cwcel @ X2 @ X11), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42]), c_0_22]), c_0_30])])).
thf(c_0_48, negated_conjecture, cwcel @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred2_0, inference(er,[status(thm)],[c_0_43])).
thf(c_0_49, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccv @ esk1_0) @ X2|(X2)!=(epred2_0)), inference(spm,[status(thm)],[c_0_44, c_0_45])).
thf(c_0_50, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X12:$i > $o, X5:$i > $o, X11:$i > $o]:((cco @ X3 @ X2 @ X5)=(X3)|~cwbr @ X2 @ X3 @ X4|~cwcel @ X11 @ cclat|~cwcel @ X2 @ X12|~cwcel @ X3 @ X12|(X5)!=(ccfv @ X11 @ ccjn)|(X4)!=(ccfv @ X11 @ ccple)|(X12)!=(ccfv @ X11 @ ccbs)), inference(split_conjunct,[status(thm)],[c_0_46])).
thf(c_0_51, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X3) @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_47, c_0_48])).
thf(c_0_52, negated_conjecture, cwcel @ (ccv @ esk1_0) @ epred2_0, inference(er,[status(thm)],[c_0_49])).
thf(c_0_53, plain, ![X2:$i > $o, X4:$i > $o, X5:$i > $o, X3:$i > $o, X11:$i > $o]:((cco @ X2 @ X3 @ X4)=(X2)|(X4)!=(ccfv @ X5 @ ccjn)|(X11)!=(ccfv @ X5 @ ccple)|~cwcel @ X2 @ (ccfv @ X5 @ ccbs)|~cwcel @ X3 @ (ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclat|~cwbr @ X3 @ X2 @ X11), inference(er,[status(thm)],[c_0_50])).
thf(c_0_54, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_51, c_0_52])).
thf(c_0_55, negated_conjecture, (cco @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred4_0)=(epred9_0), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_56, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ (ccv @ esk1_0) @ X3) @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_47, c_0_52])).
thf(c_0_57, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ X2 @ X3 @ X4)=(X2)|(X4)!=(epred4_0)|(X5)!=(epred6_0)|~cwcel @ X2 @ epred2_0|~cwcel @ X3 @ epred2_0|~cwbr @ X3 @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_22]), c_0_41]), c_0_42]), c_0_30])])).
thf(c_0_58, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ epred9_0 @ X2|(X2)!=(epred6_0)), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_54]), c_0_55])).
thf(c_0_59, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ epred9_0 @ (cco @ epred9_0 @ (ccv @ esk1_0) @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_56, c_0_37])).
thf(c_0_60, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ epred9_0 @ X2 @ X3)=(epred9_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ epred9_0 @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_57, c_0_37])).
thf(c_0_61, negated_conjecture, cwbr @ (ccv @ esk1_0) @ epred9_0 @ epred6_0, inference(er,[status(thm)],[c_0_58])).
thf(c_0_62, plain, ![X404:$i > $o, X405:$i > $o, X406:$i > $o, X407:$i > $o, X408:$i > $o, X409:$i > $o]:((~cwbr @ X408 @ X409 @ X407|(cco @ X408 @ X409 @ X405)=(X409)|(~cwcel @ X406 @ cclat|~cwcel @ X408 @ X404|~cwcel @ X409 @ X404)|(X405)!=(ccfv @ X406 @ ccjn)|(X407)!=(ccfv @ X406 @ ccple)|(X404)!=(ccfv @ X406 @ ccbs))&((cco @ X408 @ X409 @ X405)!=(X409)|cwbr @ X408 @ X409 @ X407|(~cwcel @ X406 @ cclat|~cwcel @ X408 @ X404|~cwcel @ X409 @ X404)|(X405)!=(ccfv @ X406 @ ccjn)|(X407)!=(ccfv @ X406 @ ccple)|(X404)!=(ccfv @ X406 @ ccbs))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatleeqj1_thm])])])).
thf(c_0_63, plain, ![X3:$i > $o, X23:$i > $o, X13:$i > $o, X18:$i > $o, X11:$i > $o, X21:$i > $o, X14:$i > $o, X16:$i > $o]:((X3)=(ccfv @ X11 @ ccbs)=>((X21)=(ccfv @ X11 @ ccple)=>((X18)=(ccfv @ X11 @ ccjn)=>((X23)=(ccfv @ X11 @ ccp1)=>((X13)=(ccfv @ X11 @ cclh)=>(((cwcel @ X11 @ cchlt&cwcel @ X14 @ X13)&(cwcel @ X16 @ X3&~cwbr @ X16 @ X14 @ X21))=>(cco @ X14 @ X16 @ X18)=(X23))))))), inference(fof_simplification,[status(thm)],[alhpj1_thm])).
thf(c_0_64, plain, ![X280:$i > $o, X281:$i > $o, X282:$i > $o, X283:$i > $o, X284:$i > $o, X285:$i > $o]:((X280)!=(ccfv @ X282 @ ccbs)|((X281)!=(ccfv @ X282 @ ccjn)|(~cwcel @ X282 @ cclat|(~cwcel @ X283 @ X280|~cwcel @ X284 @ X280|~cwcel @ X285 @ X280)|(cco @ (cco @ X283 @ X284 @ X281) @ X285 @ X281)=(cco @ X283 @ (cco @ X284 @ X285 @ X281) @ X281)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatjass_thm])])).
thf(c_0_65, negated_conjecture, ![X2:$i > $o]:(cwbr @ epred9_0 @ (cco @ epred9_0 @ (ccv @ esk1_0) @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_59])).
thf(c_0_66, negated_conjecture, ![X2:$i > $o]:((cco @ epred9_0 @ (ccv @ esk1_0) @ X2)=(epred9_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_52])])).
thf(c_0_67, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X12:$i > $o, X5:$i > $o, X11:$i > $o]:((cco @ X2 @ X3 @ X5)=(X3)|~cwbr @ X2 @ X3 @ X4|~cwcel @ X11 @ cclat|~cwcel @ X2 @ X12|~cwcel @ X3 @ X12|(X5)!=(ccfv @ X11 @ ccjn)|(X4)!=(ccfv @ X11 @ ccple)|(X12)!=(ccfv @ X11 @ ccbs)), inference(split_conjunct,[status(thm)],[c_0_62])).
thf(c_0_68, plain, ![X371:$i > $o, X372:$i > $o, X373:$i > $o, X374:$i > $o, X375:$i > $o, X376:$i > $o, X377:$i > $o, X378:$i > $o]:((X371)!=(ccfv @ X375 @ ccbs)|((X376)!=(ccfv @ X375 @ ccple)|((X374)!=(ccfv @ X375 @ ccjn)|((X372)!=(ccfv @ X375 @ ccp1)|((X373)!=(ccfv @ X375 @ cclh)|(~cwcel @ X375 @ cchlt|~cwcel @ X377 @ X373|(~cwcel @ X378 @ X371|cwbr @ X378 @ X377 @ X376)|(cco @ X377 @ X378 @ X374)=(X372))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_63])])).
thf(c_0_69, plain, ![X12:$i > $o, X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o, X2:$i > $o]:((cco @ (cco @ X5 @ X11 @ X4) @ X12 @ X4)=(cco @ X5 @ (cco @ X11 @ X12 @ X4) @ X4)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccjn)|~cwcel @ X3 @ cclat|~cwcel @ X5 @ X2|~cwcel @ X11 @ X2|~cwcel @ X12 @ X2), inference(split_conjunct,[status(thm)],[c_0_64])).
thf(c_0_70, negated_conjecture, cwbr @ epred9_0 @ (cco @ epred9_0 @ (ccv @ esk1_0) @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_65])).
thf(c_0_71, negated_conjecture, (cco @ epred9_0 @ (ccv @ esk1_0) @ epred4_0)=(epred9_0), inference(er,[status(thm)],[c_0_66])).
thf(c_0_72, plain, ![X319:$i > $o, X320:$i > $o, X321:$i > $o, X322:$i > $o, X323:$i > $o]:((X319)!=(ccfv @ X321 @ ccbs)|((X320)!=(ccfv @ X321 @ ccjn)|(~cwcel @ X321 @ cclat|~cwcel @ X322 @ X319|~cwcel @ X323 @ X319|cwcel @ (cco @ X322 @ X323 @ X320) @ X319))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatjcl_thm])])).
thf(c_0_73, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o, X11:$i > $o]:((cco @ X2 @ X3 @ X4)=(X3)|(X4)!=(ccfv @ X5 @ ccjn)|(X11)!=(ccfv @ X5 @ ccple)|~cwcel @ X3 @ (ccfv @ X5 @ ccbs)|~cwcel @ X2 @ (ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclat|~cwbr @ X2 @ X3 @ X11), inference(er,[status(thm)],[c_0_67])).
thf(c_0_74, plain, ![X12:$i > $o, X3:$i > $o, X5:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X4:$i > $o, X2:$i > $o]:(cwbr @ X14 @ X13 @ X4|(cco @ X13 @ X14 @ X5)=(X11)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccple)|(X5)!=(ccfv @ X3 @ ccjn)|(X11)!=(ccfv @ X3 @ ccp1)|(X12)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X13 @ X12|~cwcel @ X14 @ X2), inference(split_conjunct,[status(thm)],[c_0_68])).
thf(c_0_75, plain, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X5:$i > $o, X11:$i > $o]:((cco @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccjn)) @ X5 @ (ccfv @ X4 @ ccjn))=(cco @ X2 @ (cco @ X3 @ X5 @ (ccfv @ X4 @ ccjn)) @ (ccfv @ X4 @ ccjn))|(X11)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclat|~cwcel @ X5 @ X11|~cwcel @ X3 @ X11|~cwcel @ X2 @ X11), inference(er,[status(thm)],[c_0_69])).
thf(c_0_76, negated_conjecture, cwbr @ epred9_0 @ epred9_0 @ epred6_0, inference(rw,[status(thm)],[c_0_70, c_0_71])).
thf(c_0_77, plain, ![X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X5 @ X11 @ X4) @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccjn)|~cwcel @ X3 @ cclat|~cwcel @ X5 @ X2|~cwcel @ X11 @ X2), inference(split_conjunct,[status(thm)],[c_0_72])).
thf(c_0_78, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ epred8_0 @ X3) @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_47, c_0_33])).
thf(c_0_79, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X5:$i > $o, X11:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ X5 @ X4)=(cco @ X2 @ (cco @ X3 @ X5 @ X4) @ X4)|(X4)!=(epred4_0)|(X11)!=(epred2_0)|~cwcel @ X5 @ X11|~cwcel @ X3 @ X11|~cwcel @ X2 @ X11), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_41]), c_0_22]), c_0_30])])).
thf(c_0_80, negated_conjecture, cwcel @ epred10_0 @ epred2_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_81, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ X2 @ X3 @ X4)=(X3)|(X4)!=(epred4_0)|(X5)!=(epred6_0)|~cwcel @ X3 @ epred2_0|~cwcel @ X2 @ epred2_0|~cwbr @ X2 @ X3 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_22]), c_0_41]), c_0_42]), c_0_30])])).
thf(c_0_82, plain, ![X12:$i > $o, X2:$i > $o, X4:$i > $o, X3:$i > $o, X11:$i > $o, X5:$i > $o, X13:$i > $o]:((cco @ X2 @ X3 @ X4)=(X5)|cwbr @ X3 @ X2 @ X11|(X5)!=(ccfv @ X12 @ ccp1)|(X4)!=(ccfv @ X12 @ ccjn)|(X11)!=(ccfv @ X12 @ ccple)|(X13)!=(ccfv @ X12 @ ccbs)|~cwcel @ X2 @ (ccfv @ X12 @ cclh)|~cwcel @ X12 @ cchlt|~cwcel @ X3 @ X13), inference(er,[status(thm)],[c_0_74])).
thf(c_0_83, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ (cco @ X2 @ X3 @ epred4_0) @ X4 @ epred4_0)=(cco @ X2 @ (cco @ X3 @ X4 @ epred4_0) @ epred4_0)|(X5)!=(epred2_0)|~cwcel @ X4 @ X5|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_22]), c_0_41]), c_0_41]), c_0_41]), c_0_41]), c_0_30])])).
thf(c_0_84, negated_conjecture, ![X2:$i > $o]:((cco @ epred9_0 @ epred9_0 @ X2)=(epred9_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_76]), c_0_37])])).
thf(c_0_85, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ X4) @ X5|(X4)!=(epred4_0)|(X5)!=(epred2_0)|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_41]), c_0_22]), c_0_30])])).
thf(c_0_86, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ epred9_0 @ (cco @ epred9_0 @ epred8_0 @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_78, c_0_37])).
thf(c_0_87, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ epred10_0 @ X4)=(cco @ X2 @ (cco @ X3 @ epred10_0 @ X4) @ X4)|(X4)!=(epred4_0)|~cwcel @ X3 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_79, c_0_80])).
thf(c_0_88, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ epred10_0 @ X3)=(epred10_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ epred10_0 @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_80])).
thf(c_0_89, negated_conjecture, cwbr @ epred9_0 @ epred10_0 @ epred6_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_90, negated_conjecture, ![X4:$i > $o, X11:$i > $o, X5:$i > $o, X3:$i > $o, X2:$i > $o, X12:$i > $o]:((cco @ X2 @ X3 @ X4)=(X5)|cwbr @ X3 @ X2 @ X11|(X5)!=(ccfv @ epred5_0 @ ccp1)|(X4)!=(epred4_0)|(X11)!=(epred6_0)|(X12)!=(epred2_0)|~cwcel @ X2 @ epred3_0|~cwcel @ X3 @ X12), 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_82, c_0_21]), c_0_41]), c_0_42]), c_0_22]), c_0_25])])).
thf(c_0_91, plain, ![X3:$i > $o, X4:$i > $o, X2:$i > $o, X12:$i > $o, X5:$i > $o, X11:$i > $o]:(cwbr @ X3 @ X2 @ X5|(cco @ X2 @ X3 @ X4)!=(X2)|~cwcel @ X11 @ cclat|~cwcel @ X3 @ X12|~cwcel @ X2 @ X12|(X4)!=(ccfv @ X11 @ ccjn)|(X5)!=(ccfv @ X11 @ ccple)|(X12)!=(ccfv @ X11 @ ccbs)), inference(split_conjunct,[status(thm)],[c_0_46])).
thf(c_0_92, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ X3 @ epred4_0) @ epred9_0 @ epred4_0)=(cco @ X2 @ (cco @ X3 @ epred9_0 @ epred4_0) @ epred4_0)|~cwcel @ X3 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_83, c_0_37])).
thf(c_0_93, negated_conjecture, (cco @ epred9_0 @ epred9_0 @ epred4_0)=(epred9_0), inference(er,[status(thm)],[c_0_84])).
thf(c_0_94, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X2 @ epred9_0 @ X3) @ epred2_0|(X3)!=(epred4_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_85, c_0_37])).
thf(c_0_95, negated_conjecture, ![X2:$i > $o]:(cwbr @ epred9_0 @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_86])).
thf(c_0_96, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X2 @ epred8_0 @ X3) @ epred2_0|(X3)!=(epred4_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_85, c_0_33])).
thf(c_0_97, plain, ![X349:$i > $o, X350:$i > $o, X351:$i > $o, X352:$i > $o, X353:$i > $o, X354:$i > $o, X355:$i > $o, X356:$i > $o, X357:$i > $o]:((X349)!=(ccfv @ X352 @ ccbs)|((X353)!=(ccfv @ X352 @ ccple)|((X351)!=(ccfv @ X352 @ ccjn)|((X354)!=(ccfv @ X352 @ ccmee)|((X350)!=(ccfv @ X352 @ cclh)|(~cwcel @ X352 @ cchlt|~cwcel @ X355 @ X350|(~cwcel @ X356 @ X349|~cwcel @ X357 @ X349)|~cwbr @ X357 @ X356 @ X353|(cco @ (cco @ X356 @ X355 @ X354) @ X357 @ X351)=(cco @ X356 @ (cco @ X355 @ X357 @ X351) @ X354))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alhpmod2i2_thm])])).
thf(c_0_98, plain, ![X381:$i > $o, X382:$i > $o, X383:$i > $o, X384:$i > $o, X385:$i > $o]:((X381)!=(ccfv @ X383 @ ccbs)|((X384)!=(ccfv @ X383 @ ccmee)|((X382)!=(ccfv @ X383 @ ccp1)|(~cwcel @ X383 @ ccol|~cwcel @ X385 @ X381|(cco @ X385 @ X382 @ X384)=(X385))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aolm11_thm])])).
thf(c_0_99, plain, ![X380:$i > $o]:(~cwcel @ X380 @ cchlt|cwcel @ X380 @ ccol), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ahlol_thm])])).
thf(c_0_100, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ epred10_0 @ X3) @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_47, c_0_80])).
thf(c_0_101, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ epred9_0 @ X3) @ epred10_0 @ X3)=(cco @ X2 @ (cco @ epred9_0 @ epred10_0 @ X3) @ X3)|(X3)!=(epred4_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_87, c_0_37])).
thf(c_0_102, negated_conjecture, ![X2:$i > $o]:((cco @ epred9_0 @ epred10_0 @ X2)=(epred10_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_89]), c_0_37])])).
thf(c_0_103, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ epred9_0 @ X3)=(epred9_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ epred9_0 @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_37])).
thf(c_0_104, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o, X11:$i > $o]:((cco @ X2 @ X3 @ X4)=(ccfv @ epred5_0 @ ccp1)|cwbr @ X3 @ X2 @ X5|(X4)!=(epred4_0)|(X5)!=(epred6_0)|(X11)!=(epred2_0)|~cwcel @ X2 @ epred3_0|~cwcel @ X3 @ X11), inference(er,[status(thm)],[c_0_90])).
thf(c_0_105, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X11:$i > $o, X5:$i > $o]:(cwbr @ X2 @ X3 @ X4|(X4)!=(ccfv @ X5 @ ccple)|(X11)!=(ccfv @ X5 @ ccjn)|(cco @ X3 @ X2 @ X11)!=(X3)|~cwcel @ X2 @ (ccfv @ X5 @ ccbs)|~cwcel @ X3 @ (ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclat), inference(er,[status(thm)],[c_0_91])).
thf(c_0_106, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ X2 @ epred9_0 @ epred4_0) @ epred9_0 @ epred4_0)=(cco @ X2 @ epred9_0 @ epred4_0)|~cwcel @ X2 @ epred2_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_37]), c_0_93])).
thf(c_0_107, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ epred8_0 @ epred9_0 @ X2) @ epred2_0|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_94, c_0_33])).
thf(c_0_108, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X11:$i > $o, X5:$i > $o]:((cco @ X2 @ X3 @ X4)=(X2)|(X5)!=(epred2_0)|(X4)!=(epred4_0)|(X11)!=(epred6_0)|~cwbr @ X3 @ X2 @ X11|~cwcel @ X2 @ X5|~cwcel @ X3 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_22]), c_0_41]), c_0_42]), c_0_30])])).
thf(c_0_109, negated_conjecture, cwbr @ epred9_0 @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_95])).
thf(c_0_110, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ epred9_0 @ epred8_0 @ X2) @ epred2_0|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_96, c_0_37])).
thf(c_0_111, plain, ![X12:$i > $o, X3:$i > $o, X2:$i > $o, X5:$i > $o, X11:$i > $o, X13:$i > $o, X15:$i > $o, X14:$i > $o, X4:$i > $o]:((cco @ (cco @ X14 @ X13 @ X11) @ X15 @ X5)=(cco @ X14 @ (cco @ X13 @ X15 @ X5) @ X11)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccple)|(X5)!=(ccfv @ X3 @ ccjn)|(X11)!=(ccfv @ X3 @ ccmee)|(X12)!=(ccfv @ X3 @ cclh)|~cwcel @ X3 @ cchlt|~cwcel @ X13 @ X12|~cwcel @ X14 @ X2|~cwcel @ X15 @ X2|~cwbr @ X15 @ X14 @ X4), inference(split_conjunct,[status(thm)],[c_0_97])).
thf(c_0_112, plain, ![X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o, X2:$i > $o]:((cco @ X11 @ X5 @ X4)=(X11)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccmee)|(X5)!=(ccfv @ X3 @ ccp1)|~cwcel @ X3 @ ccol|~cwcel @ X11 @ X2), inference(split_conjunct,[status(thm)],[c_0_98])).
thf(c_0_113, plain, ![X2:$i > $o]:(cwcel @ X2 @ ccol|~cwcel @ X2 @ cchlt), inference(split_conjunct,[status(thm)],[c_0_99])).
thf(c_0_114, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ epred10_0 @ epred8_0 @ X2) @ epred2_0|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_36, c_0_80])).
thf(c_0_115, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred10_0 @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_100, c_0_52])).
thf(c_0_116, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ epred9_0 @ X2) @ epred10_0 @ X2)=(cco @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred10_0 @ X2) @ X2)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_101, c_0_52])).
thf(c_0_117, negated_conjecture, (cco @ epred9_0 @ epred10_0 @ epred4_0)=(epred10_0), inference(er,[status(thm)],[c_0_102])).
thf(c_0_118, negated_conjecture, ![X2:$i > $o]:((cco @ (ccv @ esk1_0) @ epred9_0 @ X2)=(epred9_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_61]), c_0_52])])).
thf(c_0_119, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ epred8_0 @ X2 @ X3)=(ccfv @ epred5_0 @ ccp1)|cwbr @ X2 @ epred8_0 @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|(X5)!=(epred2_0)|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_104, c_0_27])).
thf(c_0_120, negated_conjecture, ![X2:$i > $o, X5:$i > $o, X4:$i > $o, X3:$i > $o]:(cwbr @ X2 @ X3 @ X4|(cco @ X3 @ X2 @ X5)!=(X3)|(X4)!=(epred6_0)|(X5)!=(epred4_0)|~cwcel @ X2 @ epred2_0|~cwcel @ X3 @ epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_22]), c_0_42]), c_0_41]), c_0_30])])).
thf(c_0_121, negated_conjecture, (cco @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred9_0 @ epred4_0)=(cco @ epred8_0 @ epred9_0 @ epred4_0), inference(spm,[status(thm)],[c_0_106, c_0_33])).
thf(c_0_122, negated_conjecture, cwcel @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred2_0, inference(er,[status(thm)],[c_0_107])).
thf(c_0_123, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ epred9_0 @ X4)=(cco @ X2 @ (cco @ X3 @ epred9_0 @ X4) @ X4)|(X4)!=(epred4_0)|~cwcel @ X3 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_79, c_0_37])).
thf(c_0_124, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred9_0 @ X2)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|(X3)!=(epred2_0)|(X2)!=(epred4_0)|~cwcel @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ X3|~cwcel @ epred9_0 @ X3), inference(spm,[status(thm)],[c_0_108, c_0_109])).
thf(c_0_125, negated_conjecture, cwcel @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred2_0, inference(er,[status(thm)],[c_0_110])).
thf(c_0_126, negated_conjecture, ![X11:$i > $o, X5:$i > $o, X4:$i > $o, X14:$i > $o, X13:$i > $o, X3:$i > $o, X2:$i > $o, X12:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ X5 @ X11)=(cco @ X2 @ (cco @ X3 @ X5 @ X11) @ X4)|(X12)!=(epred3_0)|(X4)!=(epred7_0)|(X11)!=(epred4_0)|(X13)!=(epred6_0)|(X14)!=(epred2_0)|~cwbr @ X5 @ X2 @ X13|~cwcel @ X5 @ X14|~cwcel @ X2 @ X14|~cwcel @ X3 @ X12), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_21]), c_0_29]), c_0_41]), c_0_42]), c_0_22]), c_0_25])])).
thf(c_0_127, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ X2 @ (ccfv @ X3 @ ccp1) @ X4)=(X2)|(X4)!=(ccfv @ X3 @ ccmee)|(X5)!=(ccfv @ X3 @ ccbs)|~cwcel @ X3 @ ccol|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_112])).
thf(c_0_128, negated_conjecture, cwcel @ epred5_0 @ ccol, inference(spm,[status(thm)],[c_0_113, c_0_25])).
thf(c_0_129, negated_conjecture, cwcel @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred2_0, inference(er,[status(thm)],[c_0_114])).
thf(c_0_130, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred10_0 @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_115])).
thf(c_0_131, negated_conjecture, (cco @ (cco @ (ccv @ esk1_0) @ epred9_0 @ epred4_0) @ epred10_0 @ epred4_0)=(cco @ (ccv @ esk1_0) @ epred10_0 @ epred4_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_116]), c_0_117])).
thf(c_0_132, negated_conjecture, (cco @ (ccv @ esk1_0) @ epred9_0 @ epred4_0)=(epred9_0), inference(er,[status(thm)],[c_0_118])).
thf(c_0_133, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ epred8_0 @ epred9_0 @ X2)=(ccfv @ epred5_0 @ ccp1)|cwbr @ epred9_0 @ epred8_0 @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_119, c_0_37])).
thf(c_0_134, negated_conjecture, ![X2:$i > $o]:(cwbr @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_121]), c_0_37]), c_0_122])])).
thf(c_0_135, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ epred8_0 @ X3) @ epred9_0 @ X3)=(cco @ X2 @ (cco @ epred8_0 @ epred9_0 @ X3) @ X3)|(X3)!=(epred4_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_123, c_0_33])).
thf(c_0_136, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred9_0 @ X2)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_125]), c_0_37])])).
thf(c_0_137, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X11:$i > $o, X5:$i > $o]:((cco @ (cco @ epred9_0 @ X2 @ X3) @ epred9_0 @ X4)=(cco @ epred9_0 @ (cco @ X2 @ epred9_0 @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|(X11)!=(epred2_0)|~cwcel @ epred9_0 @ X11|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_126, c_0_76])).
thf(c_0_138, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((cco @ X2 @ (ccfv @ epred5_0 @ ccp1) @ X3)=(X2)|(X3)!=(epred7_0)|(X4)!=(epred2_0)|~cwcel @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_29]), c_0_22]), c_0_128])])).
thf(c_0_139, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X3) @ X4|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_47, c_0_129])).
thf(c_0_140, negated_conjecture, cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred10_0 @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_130])).
thf(c_0_141, negated_conjecture, (cco @ (ccv @ esk1_0) @ epred10_0 @ epred4_0)=(epred10_0), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_132]), c_0_117])).
thf(c_0_142, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ epred8_0 @ (ccv @ esk1_0) @ X2)=(ccfv @ epred5_0 @ ccp1)|cwbr @ (ccv @ esk1_0) @ epred8_0 @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_119, c_0_52])).
thf(c_0_143, negated_conjecture, ![X2:$i > $o]:((ccfv @ epred5_0 @ ccp1)=(cco @ epred8_0 @ epred9_0 @ epred4_0)|cwbr @ epred9_0 @ epred8_0 @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_133])).
thf(c_0_144, negated_conjecture, ~cwbr @ epred9_0 @ epred8_0 @ epred6_0, inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_145, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ X3)=(cco @ epred8_0 @ epred9_0 @ epred4_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_122])).
thf(c_0_146, negated_conjecture, cwbr @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_134])).
thf(c_0_147, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ X2) @ epred9_0 @ X2)=(cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ X2) @ X2)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_135, c_0_37])).
thf(c_0_148, negated_conjecture, (cco @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred9_0 @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0), inference(er,[status(thm)],[c_0_136])).
thf(c_0_149, plain, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X4:$i > $o, X11:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccjn)) @ X5|(X5)!=(ccfv @ X4 @ ccple)|(X11)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclat|~cwcel @ X3 @ X11|~cwcel @ X2 @ X11), inference(er,[status(thm)],[c_0_40])).
thf(c_0_150, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (cco @ epred9_0 @ X2 @ X3) @ epred9_0 @ X4)=(cco @ epred9_0 @ (cco @ X2 @ epred9_0 @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_137, c_0_37])).
thf(c_0_151, negated_conjecture, ![X2:$i > $o]:((cco @ epred9_0 @ (ccfv @ epred5_0 @ ccp1) @ X2)=(epred9_0)|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_138, c_0_37])).
thf(c_0_152, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_139, c_0_52])).
thf(c_0_153, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccjn)) @ X5|(X5)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclat|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_77])).
thf(c_0_154, negated_conjecture, cwbr @ (ccv @ esk1_0) @ epred10_0 @ epred6_0, inference(rw,[status(thm)],[c_0_140, c_0_141])).
thf(c_0_155, negated_conjecture, ![X2:$i > $o]:((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(ccfv @ epred5_0 @ ccp1)|cwbr @ (ccv @ esk1_0) @ epred8_0 @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_142])).
thf(c_0_156, negated_conjecture, (ccfv @ epred5_0 @ ccp1)=(cco @ epred8_0 @ epred9_0 @ epred4_0), inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_143]), c_0_144])).
thf(c_0_157, negated_conjecture, ![X2:$i > $o]:((cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ X2)=(cco @ epred8_0 @ epred9_0 @ epred4_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145, c_0_146]), c_0_37])])).
thf(c_0_158, negated_conjecture, (cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_147]), c_0_148])).
thf(c_0_159, plain, ![X386:$o, X387:$i > $o, X388:$i > $o, X389:$i > $o, X390:$i > $o, X391:$i > $o, X392:$i > $o]:(((((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))&((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))))&(((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))&((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|X386|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))))&((((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))&((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|X386|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))))&(((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|X386|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))&((((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|X386|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))))&(((X386|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|X386|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))&((X386|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs))&(~cwbr @ X391 @ X392 @ X389|(~X386|cwbr @ X390 @ X392 @ X389)|~cwbr @ X390 @ X391 @ X389|~cwcel @ X392 @ X387|~cwcel @ X391 @ X387|~cwcel @ X390 @ X387|~cwcel @ X388 @ cclat|(X389)!=(ccfv @ X388 @ ccple)|(X387)!=(ccfv @ X388 @ ccbs)))))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alattrd_thm])])])).
thf(c_0_160, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ X3 @ epred4_0) @ X4|(X4)!=(epred6_0)|(X5)!=(epred2_0)|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_42]), c_0_41]), c_0_22]), c_0_30])])).
thf(c_0_161, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ X2) @ epred9_0 @ X3)=(cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ X3) @ X2)|(X2)!=(epred7_0)|(X3)!=(epred4_0)), inference(spm,[status(thm)],[c_0_150, c_0_27])).
thf(c_0_162, negated_conjecture, (cco @ epred9_0 @ (ccfv @ epred5_0 @ ccp1) @ epred7_0)=(epred9_0), inference(er,[status(thm)],[c_0_151])).
thf(c_0_163, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_152])).
thf(c_0_164, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ epred4_0) @ X4|(X4)!=(epred2_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_153, c_0_22]), c_0_41]), c_0_30])])).
thf(c_0_165, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X11:$i > $o, X5:$i > $o]:((cco @ (cco @ epred10_0 @ X2 @ X3) @ (ccv @ esk1_0) @ X4)=(cco @ epred10_0 @ (cco @ X2 @ (ccv @ esk1_0) @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|(X11)!=(epred2_0)|~cwcel @ epred10_0 @ X11|~cwcel @ X2 @ X5), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_154]), c_0_49])).
thf(c_0_166, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ (ccv @ esk1_0) @ epred8_0 @ X2) @ epred2_0|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_96, c_0_52])).
thf(c_0_167, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred8_0 @ X2) @ X3|(X2)!=(epred4_0)|(X3)!=(epred6_0)), inference(spm,[status(thm)],[c_0_78, c_0_52])).
thf(c_0_168, negated_conjecture, ![X2:$i > $o]:((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred8_0 @ epred9_0 @ epred4_0)|cwbr @ (ccv @ esk1_0) @ epred8_0 @ X2|(X2)!=(epred6_0)), inference(rw,[status(thm)],[c_0_155, c_0_156])).
thf(c_0_169, negated_conjecture, (cco @ epred8_0 @ epred9_0 @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_157]), c_0_158])).
thf(c_0_170, plain, ![X3:$i > $o, X4:$i > $o, X5:$i > $o, X11:$i > $o, X2:$i > $o, X12:$i > $o]:(cwbr @ X5 @ X3 @ X4|~cwbr @ X2 @ X3 @ X4|~cwbr @ X5 @ X2 @ X4|~cwcel @ X3 @ X11|~cwcel @ X2 @ X11|~cwcel @ X5 @ X11|~cwcel @ X12 @ cclat|(X4)!=(ccfv @ X12 @ ccple)|(X11)!=(ccfv @ X12 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_159])])])).
thf(c_0_171, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ (cco @ X2 @ epred9_0 @ epred4_0) @ X3|(X3)!=(epred6_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_160, c_0_37])).
thf(c_0_172, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred9_0 @ X2)=(cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ X2) @ epred7_0)|(X2)!=(epred4_0)), inference(er,[status(thm)],[c_0_161])).
thf(c_0_173, negated_conjecture, (cco @ epred9_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred7_0)=(epred9_0), inference(rw,[status(thm)],[c_0_162, c_0_156])).
thf(c_0_174, negated_conjecture, cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_163])).
thf(c_0_175, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_164, c_0_129])).
thf(c_0_176, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (cco @ epred10_0 @ X2 @ X3) @ (ccv @ esk1_0) @ X4)=(cco @ epred10_0 @ (cco @ X2 @ (ccv @ esk1_0) @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_165, c_0_80])).
thf(c_0_177, negated_conjecture, cwcel @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ epred2_0, inference(er,[status(thm)],[c_0_166])).
thf(c_0_178, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(er,[status(thm)],[c_0_167])).
thf(c_0_179, negated_conjecture, ![X2:$i > $o]:((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|cwbr @ (ccv @ esk1_0) @ epred8_0 @ X2|(X2)!=(epred6_0)), inference(rw,[status(thm)],[c_0_168, c_0_169])).
thf(c_0_180, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X11:$i > $o, X4:$i > $o]:(cwbr @ X2 @ X3 @ X4|(X4)!=(ccfv @ X5 @ ccple)|~cwcel @ X2 @ (ccfv @ X5 @ ccbs)|~cwcel @ X3 @ (ccfv @ X5 @ ccbs)|~cwcel @ X11 @ (ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclat|~cwbr @ X2 @ X11 @ X4|~cwbr @ X11 @ X3 @ X4), inference(er,[status(thm)],[c_0_170])).
thf(c_0_181, negated_conjecture, ![X2:$i > $o]:(cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred9_0 @ epred4_0) @ X2|(X2)!=(epred6_0)), inference(spm,[status(thm)],[c_0_171, c_0_48])).
thf(c_0_182, negated_conjecture, (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred9_0 @ epred4_0)=(epred9_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_172]), c_0_173])).
thf(c_0_183, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X11:$i > $o, X5:$i > $o]:((cco @ (cco @ epred9_0 @ X2 @ X3) @ (ccv @ esk1_0) @ X4)=(cco @ epred9_0 @ (cco @ X2 @ (ccv @ esk1_0) @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|(X11)!=(epred2_0)|~cwcel @ epred9_0 @ X11|~cwcel @ X2 @ X5), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_61]), c_0_49])).
thf(c_0_184, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ (ccv @ esk1_0) @ X4)=(cco @ X2 @ (cco @ X3 @ (ccv @ esk1_0) @ X4) @ X4)|(X4)!=(epred4_0)|~cwcel @ X3 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_79, c_0_52])).
thf(c_0_185, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ (ccv @ esk1_0) @ X2)=(cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0)|(X3)!=(epred2_0)|(X2)!=(epred4_0)|~cwcel @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ X3), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_174]), c_0_49])).
thf(c_0_186, negated_conjecture, cwcel @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ epred2_0, inference(spm,[status(thm)],[c_0_175, c_0_52])).
thf(c_0_187, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ X2) @ (ccv @ esk1_0) @ X3)=(cco @ epred10_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ X3) @ X2)|(X2)!=(epred7_0)|(X3)!=(epred4_0)), inference(spm,[status(thm)],[c_0_176, c_0_27])).
thf(c_0_188, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ X2 @ X3)=(cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_57, c_0_177])).
thf(c_0_189, negated_conjecture, cwbr @ (ccv @ esk1_0) @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ epred6_0, inference(er,[status(thm)],[c_0_178])).
thf(c_0_190, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ epred8_0 @ X3)=(epred8_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ epred8_0 @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_33])).
thf(c_0_191, negated_conjecture, ((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|cwbr @ (ccv @ esk1_0) @ epred8_0 @ epred6_0), inference(er,[status(thm)],[c_0_179])).
thf(c_0_192, negated_conjecture, ![X2:$i > $o]:((cco @ epred10_0 @ (ccfv @ epred5_0 @ ccp1) @ X2)=(epred10_0)|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_138, c_0_80])).
thf(c_0_193, plain, ![X305:$i > $o, X306:$i > $o, X307:$i > $o, X308:$i > $o, X309:$i > $o, X310:$i > $o, X311:$i > $o]:((X305)!=(ccfv @ X306 @ ccbs)|((X307)!=(ccfv @ X306 @ ccple)|((X308)!=(ccfv @ X306 @ ccmee)|(~cwcel @ X306 @ cclat|(~cwcel @ X309 @ X305|~cwcel @ X310 @ X305|~cwcel @ X311 @ X305)|(~cwbr @ X309 @ X310 @ X307|cwbr @ (cco @ X309 @ X311 @ X308) @ (cco @ X310 @ X311 @ X308) @ X307))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[alatmlem1_thm])])).
thf(c_0_194, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o]:(cwbr @ X2 @ X3 @ X4|(X4)!=(epred6_0)|~cwcel @ X2 @ epred2_0|~cwcel @ X3 @ epred2_0|~cwcel @ X5 @ epred2_0|~cwbr @ X2 @ X5 @ X4|~cwbr @ X5 @ X3 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180, c_0_22]), c_0_42]), c_0_30])])).
thf(c_0_195, negated_conjecture, ![X2:$i > $o]:(cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred9_0 @ X2|(X2)!=(epred6_0)), inference(rw,[status(thm)],[c_0_181, c_0_182])).
thf(c_0_196, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (cco @ epred9_0 @ X2 @ X3) @ (ccv @ esk1_0) @ X4)=(cco @ epred9_0 @ (cco @ X2 @ (ccv @ esk1_0) @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_183, c_0_37])).
thf(c_0_197, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (cco @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X3) @ (ccv @ esk1_0) @ X3)=(cco @ X2 @ (cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ X3) @ X3)|(X3)!=(epred4_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_184, c_0_129])).
thf(c_0_198, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ (ccv @ esk1_0) @ X2)=(cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_185, c_0_186])).
thf(c_0_199, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ X2)=(cco @ epred10_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ X2) @ epred7_0)|(X2)!=(epred4_0)), inference(er,[status(thm)],[c_0_187])).
thf(c_0_200, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ (ccv @ esk1_0) @ X2)=(cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188, c_0_189]), c_0_52])])).
thf(c_0_201, negated_conjecture, ![X2:$i > $o]:((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|(cco @ (ccv @ esk1_0) @ epred8_0 @ X2)=(epred8_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190, c_0_191]), c_0_52])])).
thf(c_0_202, negated_conjecture, (cco @ epred10_0 @ (ccfv @ epred5_0 @ ccp1) @ epred7_0)=(epred10_0), inference(er,[status(thm)],[c_0_192])).
thf(c_0_203, plain, ![X3:$i > $o, X2:$i > $o, X12:$i > $o, X5:$i > $o, X13:$i > $o, X11:$i > $o, X4:$i > $o]:(cwbr @ (cco @ X11 @ X13 @ X5) @ (cco @ X12 @ X13 @ X5) @ X4|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccple)|(X5)!=(ccfv @ X3 @ ccmee)|~cwcel @ X3 @ cclat|~cwcel @ X11 @ X2|~cwcel @ X12 @ X2|~cwcel @ X13 @ X2|~cwbr @ X11 @ X12 @ X4), inference(split_conjunct,[status(thm)],[c_0_193])).
thf(c_0_204, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o]:(cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2 @ X3|(X3)!=(epred6_0)|~cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X4 @ X3|~cwcel @ X2 @ epred2_0|~cwcel @ X4 @ epred2_0|~cwbr @ X4 @ X2 @ X3), inference(spm,[status(thm)],[c_0_194, c_0_48])).
thf(c_0_205, negated_conjecture, cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred9_0 @ epred6_0, inference(er,[status(thm)],[c_0_195])).
thf(c_0_206, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ X2) @ (ccv @ esk1_0) @ X3)=(cco @ epred9_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ X3) @ X2)|(X2)!=(epred7_0)|(X3)!=(epred4_0)), inference(spm,[status(thm)],[c_0_196, c_0_27])).
thf(c_0_207, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2) @ (ccv @ esk1_0) @ X2)=(cco @ (ccv @ esk1_0) @ (cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ X2) @ X2)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_197, c_0_52])).
thf(c_0_208, negated_conjecture, (cco @ (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0) @ (ccv @ esk1_0) @ epred4_0)=(cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0), inference(er,[status(thm)],[c_0_198])).
thf(c_0_209, negated_conjecture, (cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred10_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0) @ epred7_0), inference(er,[status(thm)],[c_0_199])).
thf(c_0_210, negated_conjecture, (cco @ (cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0) @ (ccv @ esk1_0) @ epred4_0)=(cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0), inference(er,[status(thm)],[c_0_200])).
thf(c_0_211, negated_conjecture, ((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|(cco @ (ccv @ esk1_0) @ epred8_0 @ epred4_0)=(epred8_0)), inference(er,[status(thm)],[c_0_201])).
thf(c_0_212, negated_conjecture, (cco @ epred10_0 @ (cco @ epred8_0 @ epred9_0 @ epred4_0) @ epred7_0)=(epred10_0), inference(rw,[status(thm)],[c_0_202, c_0_156])).
thf(c_0_213, plain, ![X4:$i > $o, X3:$i > $o, X11:$i > $o, X5:$i > $o, X2:$i > $o, X12:$i > $o]:(cwbr @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccmee)) @ (cco @ X5 @ X3 @ (ccfv @ X4 @ ccmee)) @ X11|(X11)!=(ccfv @ X4 @ ccple)|(X12)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclat|~cwbr @ X2 @ X5 @ X11|~cwcel @ X3 @ X12|~cwcel @ X5 @ X12|~cwcel @ X2 @ X12), inference(er,[status(thm)],[c_0_203])).
thf(c_0_214, negated_conjecture, ![X2:$i > $o]:(cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2 @ epred6_0|~cwbr @ epred9_0 @ X2 @ epred6_0|~cwcel @ X2 @ epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_204, c_0_205]), c_0_37])])).
thf(c_0_215, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ X2)=(cco @ epred9_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ X2) @ epred7_0)|(X2)!=(epred4_0)), inference(er,[status(thm)],[c_0_206])).
thf(c_0_216, negated_conjecture, (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0) @ epred7_0) @ epred4_0)=(cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_207]), c_0_208]), c_0_209])).
thf(c_0_217, negated_conjecture, ((cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ epred8_0 @ epred4_0)|(cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(epred8_0)), inference(spm,[status(thm)],[c_0_210, c_0_211])).
thf(c_0_218, negated_conjecture, (cco @ epred10_0 @ (cco @ epred9_0 @ epred8_0 @ epred4_0) @ epred7_0)=(epred10_0), inference(rw,[status(thm)],[c_0_212, c_0_169])).
thf(c_0_219, negated_conjecture, (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0)!=(epred10_0), inference(split_conjunct,[status(thm)],[c_0_18])).
thf(c_0_220, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X4:$i > $o, X11:$i > $o]:(cwbr @ (cco @ X2 @ X3 @ epred7_0) @ (cco @ X4 @ X3 @ epred7_0) @ X5|(X5)!=(epred6_0)|(X11)!=(epred2_0)|~cwbr @ X2 @ X4 @ X5|~cwcel @ X3 @ X11|~cwcel @ X4 @ X11|~cwcel @ X2 @ X11), 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_213, c_0_42]), c_0_29]), c_0_29]), c_0_22]), c_0_30])])).
thf(c_0_221, negated_conjecture, cwbr @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred10_0 @ epred6_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_214, c_0_89]), c_0_80])])).
thf(c_0_222, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccmee)) @ X5|(X5)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclat|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_28])).
thf(c_0_223, negated_conjecture, (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ (ccv @ esk1_0) @ epred4_0)=(cco @ epred9_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0) @ epred7_0), inference(er,[status(thm)],[c_0_215])).
thf(c_0_224, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2|(cco @ epred10_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0) @ epred7_0)!=(cco @ epred10_0 @ epred8_0 @ epred7_0)|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_209]), c_0_52]), c_0_129])])).
thf(c_0_225, negated_conjecture, (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0)=(epred8_0), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_216, c_0_217]), c_0_218]), c_0_141]), c_0_219])).
thf(c_0_226, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwbr @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2 @ epred7_0) @ (cco @ epred10_0 @ X2 @ epred7_0) @ epred6_0|(X3)!=(epred2_0)|~cwcel @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X3|~cwcel @ epred10_0 @ X3|~cwcel @ X2 @ X3), inference(spm,[status(thm)],[c_0_220, c_0_221])).
thf(c_0_227, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ epred7_0) @ X4|(X4)!=(epred2_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_222, c_0_22]), c_0_29]), c_0_30])])).
thf(c_0_228, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2|(cco @ epred9_0 @ (cco @ epred8_0 @ (ccv @ esk1_0) @ epred4_0) @ epred7_0)!=(cco @ epred9_0 @ epred8_0 @ epred7_0)|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_223]), c_0_52]), c_0_48])])).
thf(c_0_229, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X11:$i > $o, X5:$i > $o]:((cco @ (cco @ epred10_0 @ X2 @ X3) @ epred9_0 @ X4)=(cco @ epred10_0 @ (cco @ X2 @ epred9_0 @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|(X11)!=(epred2_0)|~cwcel @ epred9_0 @ X11|~cwcel @ epred10_0 @ X11|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_126, c_0_89])).
thf(c_0_230, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_224, c_0_225])])).
thf(c_0_231, negated_conjecture, ![X2:$i > $o]:(cwbr @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2 @ epred7_0) @ (cco @ epred10_0 @ X2 @ epred7_0) @ epred6_0|~cwcel @ X2 @ epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_226, c_0_48]), c_0_80])])).
thf(c_0_232, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ epred8_0 @ epred7_0) @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_227, c_0_33])).
thf(c_0_233, negated_conjecture, ![X2:$i > $o]:(cwbr @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_228, c_0_225])])).
thf(c_0_234, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (cco @ epred10_0 @ X2 @ X3) @ epred9_0 @ X4)=(cco @ epred10_0 @ (cco @ X2 @ epred9_0 @ X4) @ X3)|(X5)!=(epred3_0)|(X3)!=(epred7_0)|(X4)!=(epred4_0)|~cwcel @ X2 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_229, c_0_37]), c_0_80])])).
thf(c_0_235, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X3)=(cco @ epred10_0 @ epred8_0 @ epred7_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_129])).
thf(c_0_236, negated_conjecture, cwbr @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred6_0, inference(er,[status(thm)],[c_0_230])).
thf(c_0_237, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2 @ X3)=(cco @ epred10_0 @ epred8_0 @ epred7_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_57, c_0_129])).
thf(c_0_238, negated_conjecture, cwbr @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred8_0 @ epred7_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred6_0, inference(spm,[status(thm)],[c_0_231, c_0_33])).
thf(c_0_239, negated_conjecture, cwcel @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred8_0 @ epred7_0) @ epred2_0, inference(spm,[status(thm)],[c_0_232, c_0_48])).
thf(c_0_240, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((cco @ X2 @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X3)=(cco @ epred9_0 @ epred8_0 @ epred7_0)|(X3)!=(epred4_0)|(X4)!=(epred6_0)|~cwbr @ X2 @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X4|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_81, c_0_48])).
thf(c_0_241, negated_conjecture, cwbr @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred6_0, inference(er,[status(thm)],[c_0_233])).
thf(c_0_242, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ X2) @ epred9_0 @ X3)=(cco @ epred10_0 @ (cco @ epred8_0 @ epred9_0 @ X3) @ X2)|(X2)!=(epred7_0)|(X3)!=(epred4_0)), inference(spm,[status(thm)],[c_0_234, c_0_27])).
thf(c_0_243, negated_conjecture, ![X2:$i > $o]:((cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ X2)=(cco @ epred10_0 @ epred8_0 @ epred7_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_235, c_0_236]), c_0_52])])).
thf(c_0_244, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred8_0 @ epred7_0) @ X2)=(cco @ epred10_0 @ epred8_0 @ epred7_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_237, c_0_238]), c_0_239])])).
thf(c_0_245, negated_conjecture, ![X2:$i > $o]:((cco @ (ccv @ esk1_0) @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ X2)=(cco @ epred9_0 @ epred8_0 @ epred7_0)|(X2)!=(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_240, c_0_241]), c_0_52])])).
thf(c_0_246, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred9_0 @ X2)=(cco @ epred10_0 @ (cco @ epred8_0 @ epred9_0 @ X2) @ epred7_0)|(X2)!=(epred4_0)), inference(er,[status(thm)],[c_0_242])).
thf(c_0_247, negated_conjecture, (cco @ (ccv @ esk1_0) @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred4_0)=(cco @ epred10_0 @ epred8_0 @ epred7_0), inference(er,[status(thm)],[c_0_243])).
thf(c_0_248, negated_conjecture, (cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ (cco @ (cco @ epred9_0 @ epred8_0 @ epred7_0) @ epred8_0 @ epred7_0) @ epred4_0)=(cco @ epred10_0 @ epred8_0 @ epred7_0), inference(er,[status(thm)],[c_0_244])).
thf(c_0_249, negated_conjecture, (cco @ epred9_0 @ epred8_0 @ epred7_0)=(epred9_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_245]), c_0_55])).
thf(c_0_250, negated_conjecture, (cco @ (cco @ epred10_0 @ epred8_0 @ epred7_0) @ epred9_0 @ epred4_0)=(epred10_0), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_246]), c_0_212])).
thf(c_0_251, negated_conjecture, (cco @ epred10_0 @ epred8_0 @ epred7_0)!=(epred10_0), inference(rw,[status(thm)],[c_0_219, c_0_247])).
thf(c_0_252, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_248, c_0_249]), c_0_249]), c_0_250]), c_0_251]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 253
# Proof object clause steps            : 219
# Proof object formula steps           : 34
# Proof object conjectures             : 195
# Proof object clause conjectures      : 192
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 31
# Proof object initial formulas used   : 16
# Proof object generating inferences   : 175
# Proof object simplifying inferences  : 145
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 67
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 383
# Removed in clause preprocessing      : 350
# Initial clauses in saturation        : 33
# Processed clauses                    : 24880
# ...of these trivial                  : 785
# ...subsumed                          : 7823
# ...remaining for further processing  : 16272
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 51074
# Backward-subsumed                    : 229
# Backward-rewritten                   : 6314
# Generated clauses                    : 392232
# ...of the previous two non-trivial   : 395220
# Contextual simplify-reflections      : 293
# Paramodulations                      : 380078
# Factorizations                       : 2
# NegExts                              : 0
# Equation resolutions                 : 6933
# 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  : 8324
#    Positive orientable unit clauses  : 534
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 2
#    Non-unit-clauses                  : 7788
# Current number of unprocessed clauses: 75471
# ...number of literals in the above   : 163182
# Current number of archived formulas  : 0
# Current number of archived clauses   : 7948
# Clause-clause subsumption calls (NU) : 16298675
# Rec. Clause-clause subsumption calls : 9244933
# Non-unit clause-clause subsumptions  : 8335
# Unit Clause-clause subsumption calls : 589818
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 165345
# BW rewrite match successes           : 103
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 10779673

# -------------------------------------------------
# User time                : 12.255 s
# System time              : 0.076 s
# Total time               : 12.331 s
# Maximum resident set size: 140448 pages
