# Preprocessing time       : 0.029 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
thf(cmatinv_conj, conjecture, ![X10:$i > $o, X2:$i > $o, X22:$i > $o, X3:$i > $o, X25:$i > $o, X5:$i > $o, X28:$i > $o, X7:$i > $o, X20:$i > $o, X26:$i > $o, X14:$i > $o, X19:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X20)=(cco @ X14 @ X3 @ ccmadu)=>((X22)=(cco @ X14 @ X3 @ ccmdat)=>((X2)=(ccfv @ X10 @ ccbs)=>((X5)=(ccfv @ X10 @ ccui)=>((X19)=(ccfv @ X3 @ ccui)=>((X28)=(ccfv @ X3 @ ccinvr)=>((X7)=(ccfv @ X10 @ ccinvr)=>((X25)=(ccfv @ X10 @ ccvsca)=>(((cwcel @ X3 @ cccrg&cwcel @ X26 @ X2)&cwcel @ (ccfv @ X26 @ X22) @ X19)=>(cwcel @ X26 @ X5&(ccfv @ X26 @ X7)=(cco @ (ccfv @ (ccfv @ X26 @ X22) @ X28) @ (ccfv @ X26 @ X20) @ X25)))))))))))), file('mmset20800_matinv.p', cmatinv_conj)).
thf(amatrcl_thm, axiom, ![X10:$i > $o, X2:$i > $o, X3:$i > $o, X14:$i > $o, X8:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X2)=(ccfv @ X10 @ ccbs)=>(cwcel @ X8 @ X2=>(cwcel @ X14 @ ccfn&cwcel @ X3 @ ccvv)))), file('mmset20800_matinv.p', amatrcl_thm)).
thf(amadurid_thm, axiom, ![X10:$i > $o, X2:$i > $o, X22:$i > $o, X3:$i > $o, X25:$i > $o, X4:$i > $o, X6:$i > $o, X20:$i > $o, X26:$i > $o, X14:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X2)=(ccfv @ X10 @ ccbs)=>((X20)=(cco @ X14 @ X3 @ ccmadu)=>((X22)=(cco @ X14 @ X3 @ ccmdat)=>((X6)=(ccfv @ X10 @ ccur)=>((X4)=(ccfv @ X10 @ ccmulr)=>((X25)=(ccfv @ X10 @ ccvsca)=>((cwcel @ X26 @ X2&cwcel @ X3 @ cccrg)=>(cco @ X26 @ (ccfv @ X26 @ X20) @ X4)=(cco @ (ccfv @ X26 @ X22) @ X6 @ X25))))))))), file('mmset20800_matinv.p', amadurid_thm)).
thf(amadulid_thm, axiom, ![X10:$i > $o, X2:$i > $o, X22:$i > $o, X3:$i > $o, X25:$i > $o, X4:$i > $o, X6:$i > $o, X20:$i > $o, X26:$i > $o, X14:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X2)=(ccfv @ X10 @ ccbs)=>((X20)=(cco @ X14 @ X3 @ ccmadu)=>((X22)=(cco @ X14 @ X3 @ ccmdat)=>((X6)=(ccfv @ X10 @ ccur)=>((X4)=(ccfv @ X10 @ ccmulr)=>((X25)=(ccfv @ X10 @ ccvsca)=>((cwcel @ X26 @ X2&cwcel @ X3 @ cccrg)=>(cco @ (ccfv @ X26 @ X20) @ X26 @ X4)=(cco @ (ccfv @ X26 @ X22) @ X6 @ X25))))))))), file('mmset20800_matinv.p', amadulid_thm)).
thf(amatsca2_thm, axiom, ![X10:$i > $o, X3:$i > $o, X14:$i > $o, X19:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((cwcel @ X14 @ ccfn&cwcel @ X3 @ X19)=>(X3)=(ccfv @ X10 @ ccsca))), file('mmset20800_matinv.p', amatsca2_thm)).
thf(amatassa_thm, axiom, ![X10:$i > $o, X3:$i > $o, X14:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((cwcel @ X14 @ ccfn&cwcel @ X3 @ cccrg)=>cwcel @ X10 @ ccasa)), file('mmset20800_matinv.p', amatassa_thm)).
thf(aunitlinv_thm, axiom, ![X3:$i > $o, X4:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X8:$i > $o]:((X5)=(ccfv @ X3 @ ccui)=>((X7)=(ccfv @ X3 @ ccinvr)=>((X4)=(ccfv @ X3 @ ccmulr)=>((X6)=(ccfv @ X3 @ ccur)=>((cwcel @ X3 @ ccrg&cwcel @ X8 @ X5)=>(cco @ (ccfv @ X8 @ X7) @ X8 @ X4)=(X6)))))), file('mmset20800_matinv.p', aunitlinv_thm)).
thf(acrngring_thm, axiom, ![X3:$i > $o]:(cwcel @ X3 @ cccrg=>cwcel @ X3 @ ccrg), file('mmset20800_matinv.p', acrngring_thm)).
thf(aringinvcl_thm, axiom, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X7:$i > $o, X8:$i > $o]:((X5)=(ccfv @ X3 @ ccui)=>((X7)=(ccfv @ X3 @ ccinvr)=>((X2)=(ccfv @ X3 @ ccbs)=>((cwcel @ X3 @ ccrg&cwcel @ X8 @ X5)=>cwcel @ (ccfv @ X8 @ X7) @ X2)))), file('mmset20800_matinv.p', aringinvcl_thm)).
thf(amaduf_thm, axiom, ![X10:$i > $o, X2:$i > $o, X3:$i > $o, X20:$i > $o, X14:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X20)=(cco @ X14 @ X3 @ ccmadu)=>((X2)=(ccfv @ X10 @ ccbs)=>(cwcel @ X3 @ cccrg=>cwf @ X2 @ X2 @ X20)))), file('mmset20800_matinv.p', amaduf_thm)).
thf(aunitcl_thm, axiom, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X8:$i > $o]:((X2)=(ccfv @ X3 @ ccbs)=>((X5)=(ccfv @ X3 @ ccui)=>(cwcel @ X8 @ X5=>cwcel @ X8 @ X2))), file('mmset20800_matinv.p', aunitcl_thm)).
thf(aassaass_thm, axiom, ![X10:$i > $o, X2:$i > $o, X4:$i > $o, X24:$i > $o, X18:$i > $o, X19:$i > $o, X15:$i > $o, X8:$i > $o, X9:$i > $o]:((X19)=(ccfv @ X15 @ ccbs)=>((X18)=(ccfv @ X15 @ ccsca)=>((X2)=(ccfv @ X18 @ ccbs)=>((X4)=(ccfv @ X15 @ ccvsca)=>((X24)=(ccfv @ X15 @ ccmulr)=>((cwcel @ X15 @ ccasa&((cwcel @ X10 @ X2&cwcel @ X8 @ X19)&cwcel @ X9 @ X19))=>(cco @ (cco @ X10 @ X8 @ X4) @ X9 @ X24)=(cco @ X10 @ (cco @ X8 @ X9 @ X24) @ X4))))))), file('mmset20800_matinv.p', aassaass_thm)).
thf(almodvsass_thm, axiom, ![X27:$i > $o, X3:$i > $o, X4:$i > $o, X24:$i > $o, X18:$i > $o, X21:$i > $o, X19:$i > $o, X15:$i > $o, X8:$i > $o]:((X19)=(ccfv @ X15 @ ccbs)=>((X18)=(ccfv @ X15 @ ccsca)=>((X4)=(ccfv @ X15 @ ccvsca)=>((X21)=(ccfv @ X18 @ ccbs)=>((X24)=(ccfv @ X18 @ ccmulr)=>((cwcel @ X15 @ cclmod&((cwcel @ X27 @ X21&cwcel @ X3 @ X21)&cwcel @ X8 @ X19))=>(cco @ (cco @ X27 @ X3 @ X24) @ X8 @ X4)=(cco @ X27 @ (cco @ X3 @ X8 @ X4) @ X4))))))), file('mmset20800_matinv.p', almodvsass_thm)).
thf(almodvs1_thm, axiom, ![X4:$i > $o, X6:$i > $o, X18:$i > $o, X19:$i > $o, X15:$i > $o, X8:$i > $o]:((X19)=(ccfv @ X15 @ ccbs)=>((X18)=(ccfv @ X15 @ ccsca)=>((X4)=(ccfv @ X15 @ ccvsca)=>((X6)=(ccfv @ X18 @ ccur)=>((cwcel @ X15 @ cclmod&cwcel @ X8 @ X19)=>(cco @ X6 @ X8 @ X4)=(X8)))))), file('mmset20800_matinv.p', almodvs1_thm)).
thf(aringidcl_thm, axiom, ![X2:$i > $o, X3:$i > $o, X6:$i > $o]:((X2)=(ccfv @ X3 @ ccbs)=>((X6)=(ccfv @ X3 @ ccur)=>(cwcel @ X3 @ ccrg=>cwcel @ X6 @ X2))), file('mmset20800_matinv.p', aringidcl_thm)).
thf(aassaring_thm, axiom, ![X15:$i > $o]:(cwcel @ X15 @ ccasa=>cwcel @ X15 @ ccrg), file('mmset20800_matinv.p', aassaring_thm)).
thf(aassaassr_thm, axiom, ![X10:$i > $o, X2:$i > $o, X4:$i > $o, X24:$i > $o, X18:$i > $o, X19:$i > $o, X15:$i > $o, X8:$i > $o, X9:$i > $o]:((X19)=(ccfv @ X15 @ ccbs)=>((X18)=(ccfv @ X15 @ ccsca)=>((X2)=(ccfv @ X18 @ ccbs)=>((X4)=(ccfv @ X15 @ ccvsca)=>((X24)=(ccfv @ X15 @ ccmulr)=>((cwcel @ X15 @ ccasa&((cwcel @ X10 @ X2&cwcel @ X8 @ X19)&cwcel @ X9 @ X19))=>(cco @ X8 @ (cco @ X10 @ X9 @ X4) @ X24)=(cco @ X10 @ (cco @ X8 @ X9 @ X24) @ X4))))))), file('mmset20800_matinv.p', aassaassr_thm)).
thf(aassalmod_thm, axiom, ![X15:$i > $o]:(cwcel @ X15 @ ccasa=>cwcel @ X15 @ cclmod), file('mmset20800_matinv.p', aassalmod_thm)).
thf(ainvrvald_thm, axiom, ![X1:$o, X2:$i > $o, X3:$i > $o, X4:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X8:$i > $o, X9:$i > $o]:((X2)=(ccfv @ X3 @ ccbs)=>((X4)=(ccfv @ X3 @ ccmulr)=>((X6)=(ccfv @ X3 @ ccur)=>((X5)=(ccfv @ X3 @ ccui)=>((X7)=(ccfv @ X3 @ ccinvr)=>((X1=>cwcel @ X3 @ ccrg)=>((X1=>cwcel @ X8 @ X2)=>((X1=>cwcel @ X9 @ X2)=>((X1=>(cco @ X8 @ X9 @ X4)=(X6))=>((X1=>(cco @ X9 @ X8 @ X4)=(X6))=>(X1=>(cwcel @ X8 @ X5&(ccfv @ X8 @ X7)=(X9))))))))))))), file('mmset20800_matinv.p', ainvrvald_thm)).
thf(affvelrnd_thm, axiom, ![X1:$o, X10:$i > $o, X2:$i > $o, X17:$i > $o, X18:$i > $o]:((X1=>cwf @ X10 @ X2 @ X18)=>((X1=>cwcel @ X17 @ X10)=>(X1=>cwcel @ (ccfv @ X17 @ X18) @ X2))), file('mmset20800_matinv.p', affvelrnd_thm)).
thf(almodvscl_thm, axiom, ![X3:$i > $o, X4:$i > $o, X18:$i > $o, X21:$i > $o, X19:$i > $o, X15:$i > $o, X8:$i > $o]:((X19)=(ccfv @ X15 @ ccbs)=>((X18)=(ccfv @ X15 @ ccsca)=>((X4)=(ccfv @ X15 @ ccvsca)=>((X21)=(ccfv @ X18 @ ccbs)=>(((cwcel @ X15 @ cclmod&cwcel @ X3 @ X21)&cwcel @ X8 @ X19)=>cwcel @ (cco @ X3 @ X8 @ X4) @ X19))))), file('mmset20800_matinv.p', almodvscl_thm)).
thf(c_0_21, negated_conjecture, ~(![X10:$i > $o, X2:$i > $o, X22:$i > $o, X3:$i > $o, X25:$i > $o, X5:$i > $o, X28:$i > $o, X7:$i > $o, X20:$i > $o, X26:$i > $o, X14:$i > $o, X19:$i > $o]:((X10)=(cco @ X14 @ X3 @ ccmat)=>((X20)=(cco @ X14 @ X3 @ ccmadu)=>((X22)=(cco @ X14 @ X3 @ ccmdat)=>((X2)=(ccfv @ X10 @ ccbs)=>((X5)=(ccfv @ X10 @ ccui)=>((X19)=(ccfv @ X3 @ ccui)=>((X28)=(ccfv @ X3 @ ccinvr)=>((X7)=(ccfv @ X10 @ ccinvr)=>((X25)=(ccfv @ X10 @ ccvsca)=>(((cwcel @ X3 @ cccrg&cwcel @ X26 @ X2)&cwcel @ (ccfv @ X26 @ X22) @ X19)=>(cwcel @ X26 @ X5&(ccfv @ X26 @ X7)=(cco @ (ccfv @ (ccfv @ X26 @ X22) @ X28) @ (ccfv @ X26 @ X20) @ X25))))))))))))), inference(assume_negation,[status(cth)],[cmatinv_conj])).
thf(c_0_22, plain, ![X253:$i > $o, X254:$i > $o, X255:$i > $o, X256:$i > $o, X257:$i > $o]:((cwcel @ X256 @ ccfn|~cwcel @ X257 @ X254|(X254)!=(ccfv @ X253 @ ccbs)|(X253)!=(cco @ X256 @ X255 @ ccmat))&(cwcel @ X255 @ ccvv|~cwcel @ X257 @ X254|(X254)!=(ccfv @ X253 @ ccbs)|(X253)!=(cco @ X256 @ X255 @ ccmat))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amatrcl_thm])])])).
thf(c_0_23, negated_conjecture, ((epred1_0)=(cco @ epred11_0 @ epred4_0 @ ccmat)&((epred9_0)=(cco @ epred11_0 @ epred4_0 @ ccmadu)&((epred3_0)=(cco @ epred11_0 @ epred4_0 @ ccmdat)&((epred2_0)=(ccfv @ epred1_0 @ ccbs)&((epred6_0)=(ccfv @ epred1_0 @ ccui)&((epred12_0)=(ccfv @ epred4_0 @ ccui)&((epred7_0)=(ccfv @ epred4_0 @ ccinvr)&((epred8_0)=(ccfv @ epred1_0 @ ccinvr)&((epred5_0)=(ccfv @ epred1_0 @ ccvsca)&(((cwcel @ epred4_0 @ cccrg&cwcel @ epred10_0 @ epred2_0)&cwcel @ (ccfv @ epred10_0 @ epred3_0) @ epred12_0)&(~cwcel @ epred10_0 @ epred6_0|(ccfv @ epred10_0 @ epred8_0)!=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0)))))))))))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])).
thf(c_0_24, plain, ![X341:$i > $o, X342:$i > $o, X343:$i > $o, X344:$i > $o, X345:$i > $o, X346:$i > $o, X347:$i > $o, X348:$i > $o, X349:$i > $o, X350:$i > $o]:((X341)!=(cco @ X350 @ X344 @ ccmat)|((X342)!=(ccfv @ X341 @ ccbs)|((X348)!=(cco @ X350 @ X344 @ ccmadu)|((X343)!=(cco @ X350 @ X344 @ ccmdat)|((X347)!=(ccfv @ X341 @ ccur)|((X346)!=(ccfv @ X341 @ ccmulr)|((X345)!=(ccfv @ X341 @ ccvsca)|(~cwcel @ X349 @ X342|~cwcel @ X344 @ cccrg|(cco @ X349 @ (ccfv @ X349 @ X348) @ X346)=(cco @ (ccfv @ X349 @ X343) @ X347 @ X345))))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amadurid_thm])])).
thf(c_0_25, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o, X6:$i > $o]:(cwcel @ X2 @ ccfn|~cwcel @ X3 @ X4|(X4)!=(ccfv @ X5 @ ccbs)|(X5)!=(cco @ X2 @ X6 @ ccmat)), inference(split_conjunct,[status(thm)],[c_0_22])).
thf(c_0_26, negated_conjecture, (epred1_0)=(cco @ epred11_0 @ epred4_0 @ ccmat), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_27, plain, ![X2:$i > $o, X3:$i > $o, X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X14:$i > $o, X6:$i > $o, X5:$i > $o, X4:$i > $o]:((cco @ X14 @ (ccfv @ X14 @ X6) @ X9)=(cco @ (ccfv @ X14 @ X7) @ X8 @ X10)|(X2)!=(cco @ X3 @ X4 @ ccmat)|(X5)!=(ccfv @ X2 @ ccbs)|(X6)!=(cco @ X3 @ X4 @ ccmadu)|(X7)!=(cco @ X3 @ X4 @ ccmdat)|(X8)!=(ccfv @ X2 @ ccur)|(X9)!=(ccfv @ X2 @ ccmulr)|(X10)!=(ccfv @ X2 @ ccvsca)|~cwcel @ X14 @ X5|~cwcel @ X4 @ cccrg), inference(split_conjunct,[status(thm)],[c_0_24])).
thf(c_0_28, negated_conjecture, (epred3_0)=(cco @ epred11_0 @ epred4_0 @ ccmdat), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_29, negated_conjecture, (epred9_0)=(cco @ epred11_0 @ epred4_0 @ ccmadu), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_30, negated_conjecture, cwcel @ epred4_0 @ cccrg, inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_31, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwcel @ epred11_0 @ ccfn|(X2)!=(ccfv @ X3 @ ccbs)|(X3)!=(epred1_0)|~cwcel @ X4 @ X2), inference(spm,[status(thm)],[c_0_25, c_0_26])).
thf(c_0_32, plain, ![X407:$i > $o, X408:$i > $o, X409:$i > $o, X410:$i > $o, X411:$i > $o, X412:$i > $o, X413:$i > $o, X414:$i > $o, X415:$i > $o, X416:$i > $o]:((X407)!=(cco @ X416 @ X410 @ ccmat)|((X408)!=(ccfv @ X407 @ ccbs)|((X414)!=(cco @ X416 @ X410 @ ccmadu)|((X409)!=(cco @ X416 @ X410 @ ccmdat)|((X413)!=(ccfv @ X407 @ ccur)|((X412)!=(ccfv @ X407 @ ccmulr)|((X411)!=(ccfv @ X407 @ ccvsca)|(~cwcel @ X415 @ X408|~cwcel @ X410 @ cccrg|(cco @ (ccfv @ X415 @ X414) @ X415 @ X412)=(cco @ (ccfv @ X415 @ X409) @ X413 @ X411))))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amadulid_thm])])).
thf(c_0_33, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X6:$i > $o, X5:$i > $o, X7:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:((cco @ X2 @ (ccfv @ X2 @ X3) @ X4)=(cco @ (ccfv @ X2 @ X5) @ X6 @ X7)|(X7)!=(ccfv @ X8 @ ccvsca)|(X4)!=(ccfv @ X8 @ ccmulr)|(X6)!=(ccfv @ X8 @ ccur)|(X9)!=(ccfv @ X8 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X8)!=(epred1_0)|~cwcel @ X2 @ X9), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_29]), c_0_26]), c_0_30])])).
thf(c_0_34, plain, ![X295:$i > $o, X296:$i > $o, X297:$i > $o, X298:$i > $o]:((X295)!=(cco @ X297 @ X296 @ ccmat)|(~cwcel @ X297 @ ccfn|~cwcel @ X296 @ X298|(X296)=(ccfv @ X295 @ ccsca))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amatsca2_thm])])).
thf(c_0_35, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ epred11_0 @ ccfn|(X2)!=(epred1_0)|~cwcel @ X3 @ (ccfv @ X2 @ ccbs)), inference(er,[status(thm)],[c_0_31])).
thf(c_0_36, negated_conjecture, (epred2_0)=(ccfv @ epred1_0 @ ccbs), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_37, plain, ![X261:$i > $o, X262:$i > $o, X263:$i > $o]:((X261)!=(cco @ X263 @ X262 @ ccmat)|(~cwcel @ X263 @ ccfn|~cwcel @ X262 @ cccrg|cwcel @ X261 @ ccasa)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amatassa_thm])])).
thf(c_0_38, plain, ![X2:$i > $o, X3:$i > $o, X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X14:$i > $o, X6:$i > $o, X5:$i > $o, X4:$i > $o]:((cco @ (ccfv @ X14 @ X6) @ X14 @ X9)=(cco @ (ccfv @ X14 @ X7) @ X8 @ X10)|(X2)!=(cco @ X3 @ X4 @ ccmat)|(X5)!=(ccfv @ X2 @ ccbs)|(X6)!=(cco @ X3 @ X4 @ ccmadu)|(X7)!=(cco @ X3 @ X4 @ ccmdat)|(X8)!=(ccfv @ X2 @ ccur)|(X9)!=(ccfv @ X2 @ ccmulr)|(X10)!=(ccfv @ X2 @ ccvsca)|~cwcel @ X14 @ X5|~cwcel @ X4 @ cccrg), inference(split_conjunct,[status(thm)],[c_0_32])).
thf(c_0_39, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X4:$i > $o, X8:$i > $o]:((cco @ X2 @ (ccfv @ X2 @ X3) @ X4)=(cco @ (ccfv @ X2 @ X5) @ X6 @ (ccfv @ X7 @ ccvsca))|(X4)!=(ccfv @ X7 @ ccmulr)|(X6)!=(ccfv @ X7 @ ccur)|(X8)!=(ccfv @ X7 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X7)!=(epred1_0)|~cwcel @ X2 @ X8), inference(er,[status(thm)],[c_0_33])).
thf(c_0_40, plain, ![X361:$i > $o, X362:$i > $o, X363:$i > $o, X364:$i > $o, X365:$i > $o, X366:$i > $o]:((X363)!=(ccfv @ X361 @ ccui)|((X365)!=(ccfv @ X361 @ ccinvr)|((X362)!=(ccfv @ X361 @ ccmulr)|((X364)!=(ccfv @ X361 @ ccur)|(~cwcel @ X361 @ ccrg|~cwcel @ X366 @ X363|(cco @ (ccfv @ X366 @ X365) @ X366 @ X362)=(X364)))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aunitlinv_thm])])).
thf(c_0_41, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X5:$i > $o]:((X4)=(ccfv @ X2 @ ccsca)|(X2)!=(cco @ X3 @ X4 @ ccmat)|~cwcel @ X3 @ ccfn|~cwcel @ X4 @ X5), inference(split_conjunct,[status(thm)],[c_0_34])).
thf(c_0_42, negated_conjecture, ![X2:$i > $o]:(cwcel @ epred11_0 @ ccfn|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_35, c_0_36])).
thf(c_0_43, negated_conjecture, cwcel @ epred10_0 @ epred2_0, inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_44, plain, ![X282:$i > $o]:(~cwcel @ X282 @ cccrg|cwcel @ X282 @ ccrg), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[acrngring_thm])])).
thf(c_0_45, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ X2 @ ccasa|(X2)!=(cco @ X3 @ X4 @ ccmat)|~cwcel @ X3 @ ccfn|~cwcel @ X4 @ cccrg), inference(split_conjunct,[status(thm)],[c_0_37])).
thf(c_0_46, plain, ![X286:$i > $o, X287:$i > $o, X288:$i > $o, X289:$i > $o, X290:$i > $o]:((X288)!=(ccfv @ X287 @ ccui)|((X289)!=(ccfv @ X287 @ ccinvr)|((X286)!=(ccfv @ X287 @ ccbs)|(~cwcel @ X287 @ ccrg|~cwcel @ X290 @ X288|cwcel @ (ccfv @ X290 @ X289) @ X286)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aringinvcl_thm])])).
thf(c_0_47, plain, ![X304:$i > $o, X305:$i > $o, X306:$i > $o, X307:$i > $o, X308:$i > $o]:((X304)!=(cco @ X308 @ X306 @ ccmat)|((X307)!=(cco @ X308 @ X306 @ ccmadu)|((X305)!=(ccfv @ X304 @ ccbs)|(~cwcel @ X306 @ cccrg|cwf @ X305 @ X305 @ X307)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[amaduf_thm])])).
thf(c_0_48, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X6:$i > $o, X5:$i > $o, X7:$i > $o, X8:$i > $o, X4:$i > $o, X9:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ X4)=(cco @ (ccfv @ X2 @ X5) @ X6 @ X7)|(X7)!=(ccfv @ X8 @ ccvsca)|(X4)!=(ccfv @ X8 @ ccmulr)|(X6)!=(ccfv @ X8 @ ccur)|(X9)!=(ccfv @ X8 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X8)!=(epred1_0)|~cwcel @ X2 @ X9), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_28]), c_0_29]), c_0_26]), c_0_30])])).
thf(c_0_49, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X6:$i > $o, X5:$i > $o, X3:$i > $o, X7:$i > $o]:((cco @ X2 @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ ccmulr))=(cco @ (ccfv @ X2 @ X5) @ X6 @ (ccfv @ X4 @ ccvsca))|(X6)!=(ccfv @ X4 @ ccur)|(X7)!=(ccfv @ X4 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X4)!=(epred1_0)|~cwcel @ X2 @ X7), inference(er,[status(thm)],[c_0_39])).
thf(c_0_50, plain, ![X376:$i > $o, X377:$i > $o, X378:$i > $o, X379:$i > $o]:((X376)!=(ccfv @ X377 @ ccbs)|((X378)!=(ccfv @ X377 @ ccui)|(~cwcel @ X379 @ X378|cwcel @ X379 @ X376))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aunitcl_thm])])).
thf(c_0_51, plain, ![X3:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X4:$i > $o, X2:$i > $o]:((cco @ (ccfv @ X7 @ X4) @ X7 @ X5)=(X6)|(X2)!=(ccfv @ X3 @ ccui)|(X4)!=(ccfv @ X3 @ ccinvr)|(X5)!=(ccfv @ X3 @ ccmulr)|(X6)!=(ccfv @ X3 @ ccur)|~cwcel @ X3 @ ccrg|~cwcel @ X7 @ X2), inference(split_conjunct,[status(thm)],[c_0_40])).
thf(c_0_52, plain, ![X398:$i > $o, X399:$i > $o, X400:$i > $o, X401:$i > $o, X402:$i > $o, X403:$i > $o, X404:$i > $o, X405:$i > $o, X406:$i > $o]:((X403)!=(ccfv @ X404 @ ccbs)|((X402)!=(ccfv @ X404 @ ccsca)|((X399)!=(ccfv @ X402 @ ccbs)|((X400)!=(ccfv @ X404 @ ccvsca)|((X401)!=(ccfv @ X404 @ ccmulr)|(~cwcel @ X404 @ ccasa|(~cwcel @ X398 @ X399|~cwcel @ X405 @ X403|~cwcel @ X406 @ X403)|(cco @ (cco @ X398 @ X405 @ X400) @ X406 @ X401)=(cco @ X398 @ (cco @ X405 @ X406 @ X401) @ X400))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aassaass_thm])])).
thf(c_0_53, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((ccfv @ (cco @ X2 @ X3 @ ccmat) @ ccsca)=(X3)|~cwcel @ X2 @ ccfn|~cwcel @ X3 @ X4), inference(er,[status(thm)],[c_0_41])).
thf(c_0_54, negated_conjecture, cwcel @ epred11_0 @ ccfn, inference(spm,[status(thm)],[c_0_42, c_0_43])).
thf(c_0_55, plain, ![X2:$i > $o]:(cwcel @ X2 @ ccrg|~cwcel @ X2 @ cccrg), inference(split_conjunct,[status(thm)],[c_0_44])).
thf(c_0_56, negated_conjecture, ![X2:$i > $o]:(cwcel @ X2 @ ccasa|(X2)!=(epred1_0)|~cwcel @ epred11_0 @ ccfn), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_26]), c_0_30])])).
thf(c_0_57, plain, ![X3:$i > $o, X5:$i > $o, X6:$i > $o, X4:$i > $o, X2:$i > $o]:(cwcel @ (ccfv @ X6 @ X4) @ X5|(X2)!=(ccfv @ X3 @ ccui)|(X4)!=(ccfv @ X3 @ ccinvr)|(X5)!=(ccfv @ X3 @ ccbs)|~cwcel @ X3 @ ccrg|~cwcel @ X6 @ X2), inference(split_conjunct,[status(thm)],[c_0_46])).
thf(c_0_58, plain, ![X3:$i > $o, X2:$i > $o, X6:$i > $o, X5:$i > $o, X4:$i > $o]:(cwf @ X6 @ X6 @ X5|(X2)!=(cco @ X3 @ X4 @ ccmat)|(X5)!=(cco @ X3 @ X4 @ ccmadu)|(X6)!=(ccfv @ X2 @ ccbs)|~cwcel @ X4 @ cccrg), inference(split_conjunct,[status(thm)],[c_0_47])).
thf(c_0_59, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X4:$i > $o, X8:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ X4)=(cco @ (ccfv @ X2 @ X5) @ X6 @ (ccfv @ X7 @ ccvsca))|(X4)!=(ccfv @ X7 @ ccmulr)|(X6)!=(ccfv @ X7 @ ccur)|(X8)!=(ccfv @ X7 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X7)!=(epred1_0)|~cwcel @ X2 @ X8), inference(er,[status(thm)],[c_0_48])).
thf(c_0_60, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X5:$i > $o, X3:$i > $o, X6:$i > $o]:((cco @ X2 @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ ccmulr))=(cco @ (ccfv @ X2 @ X5) @ (ccfv @ X4 @ ccur) @ (ccfv @ X4 @ ccvsca))|(X6)!=(ccfv @ X4 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X4)!=(epred1_0)|~cwcel @ X2 @ X6), inference(er,[status(thm)],[c_0_49])).
thf(c_0_61, negated_conjecture, (epred5_0)=(ccfv @ epred1_0 @ ccvsca), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_62, plain, ![X383:$i > $o, X384:$i > $o, X385:$i > $o, X386:$i > $o, X387:$i > $o, X388:$i > $o, X389:$i > $o, X390:$i > $o, X391:$i > $o]:((X389)!=(ccfv @ X390 @ ccbs)|((X387)!=(ccfv @ X390 @ ccsca)|((X385)!=(ccfv @ X390 @ ccvsca)|((X388)!=(ccfv @ X387 @ ccbs)|((X386)!=(ccfv @ X387 @ ccmulr)|(~cwcel @ X390 @ cclmod|(~cwcel @ X383 @ X388|~cwcel @ X384 @ X388|~cwcel @ X391 @ X389)|(cco @ (cco @ X383 @ X384 @ X386) @ X391 @ X385)=(cco @ X383 @ (cco @ X384 @ X391 @ X385) @ X385))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[almodvsass_thm])])).
thf(c_0_63, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o]:(cwcel @ X5 @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccui)|~cwcel @ X5 @ X4), inference(split_conjunct,[status(thm)],[c_0_50])).
thf(c_0_64, negated_conjecture, (epred12_0)=(ccfv @ epred4_0 @ ccui), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_65, plain, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X4:$i > $o, X6:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ X4)=(ccfv @ X5 @ ccur)|(X4)!=(ccfv @ X5 @ ccmulr)|(X3)!=(ccfv @ X5 @ ccinvr)|(X6)!=(ccfv @ X5 @ ccui)|~cwcel @ X5 @ ccrg|~cwcel @ X2 @ X6), inference(er,[status(thm)],[c_0_51])).
thf(c_0_66, plain, ![X4:$i > $o, X6:$i > $o, X7:$i > $o, X5:$i > $o, X3:$i > $o, X9:$i > $o, X10:$i > $o, X8:$i > $o, X2:$i > $o]:((cco @ (cco @ X8 @ X9 @ X6) @ X10 @ X7)=(cco @ X8 @ (cco @ X9 @ X10 @ X7) @ X6)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccsca)|(X5)!=(ccfv @ X4 @ ccbs)|(X6)!=(ccfv @ X3 @ ccvsca)|(X7)!=(ccfv @ X3 @ ccmulr)|~cwcel @ X3 @ ccasa|~cwcel @ X8 @ X5|~cwcel @ X9 @ X2|~cwcel @ X10 @ X2), inference(split_conjunct,[status(thm)],[c_0_52])).
thf(c_0_67, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:((ccfv @ (cco @ epred11_0 @ X2 @ ccmat) @ ccsca)=(X2)|~cwcel @ X2 @ X3), inference(spm,[status(thm)],[c_0_53, c_0_54])).
thf(c_0_68, negated_conjecture, cwcel @ epred4_0 @ ccrg, inference(spm,[status(thm)],[c_0_55, c_0_30])).
thf(c_0_69, negated_conjecture, ![X2:$i > $o]:(cwcel @ X2 @ ccasa|(X2)!=(epred1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_54])])).
thf(c_0_70, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccfv @ X4 @ ccbs)|(X3)!=(ccfv @ X4 @ ccinvr)|(X5)!=(ccfv @ X4 @ ccui)|~cwcel @ X4 @ ccrg|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_57])).
thf(c_0_71, negated_conjecture, (epred7_0)=(ccfv @ epred4_0 @ ccinvr), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_72, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwf @ X2 @ X2 @ X3|(X2)!=(ccfv @ X4 @ ccbs)|(X3)!=(epred9_0)|(X4)!=(epred1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_29]), c_0_26]), c_0_30])])).
thf(c_0_73, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X6:$i > $o, X5:$i > $o, X3:$i > $o, X7:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ (ccfv @ X4 @ ccmulr))=(cco @ (ccfv @ X2 @ X5) @ X6 @ (ccfv @ X4 @ ccvsca))|(X6)!=(ccfv @ X4 @ ccur)|(X7)!=(ccfv @ X4 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X4)!=(epred1_0)|~cwcel @ X2 @ X7), inference(er,[status(thm)],[c_0_59])).
thf(c_0_74, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ X2 @ (ccfv @ X2 @ X3) @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ X2 @ X4) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)|(X5)!=(epred2_0)|(X4)!=(epred3_0)|(X3)!=(epred9_0)|~cwcel @ X2 @ X5), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_36]), c_0_61])).
thf(c_0_75, plain, ![X3:$i > $o, X5:$i > $o, X7:$i > $o, X6:$i > $o, X4:$i > $o, X9:$i > $o, X10:$i > $o, X8:$i > $o, X2:$i > $o]:((cco @ (cco @ X8 @ X9 @ X7) @ X10 @ X5)=(cco @ X8 @ (cco @ X9 @ X10 @ X5) @ X5)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccsca)|(X5)!=(ccfv @ X3 @ ccvsca)|(X6)!=(ccfv @ X4 @ ccbs)|(X7)!=(ccfv @ X4 @ ccmulr)|~cwcel @ X3 @ cclmod|~cwcel @ X8 @ X6|~cwcel @ X9 @ X6|~cwcel @ X10 @ X2), inference(split_conjunct,[status(thm)],[c_0_62])).
thf(c_0_76, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ X2 @ X3|(X3)!=(ccfv @ epred4_0 @ ccbs)|(X4)!=(epred12_0)|~cwcel @ X2 @ X4), inference(spm,[status(thm)],[c_0_63, c_0_64])).
thf(c_0_77, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ (ccfv @ X4 @ ccmulr))=(ccfv @ X4 @ ccur)|(X3)!=(ccfv @ X4 @ ccinvr)|(X5)!=(ccfv @ X4 @ ccui)|~cwcel @ X4 @ ccrg|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_65])).
thf(c_0_78, plain, ![X392:$i > $o, X393:$i > $o, X394:$i > $o, X395:$i > $o, X396:$i > $o, X397:$i > $o]:((X395)!=(ccfv @ X396 @ ccbs)|((X394)!=(ccfv @ X396 @ ccsca)|((X392)!=(ccfv @ X396 @ ccvsca)|((X393)!=(ccfv @ X394 @ ccur)|(~cwcel @ X396 @ cclmod|~cwcel @ X397 @ X395|(cco @ X393 @ X397 @ X392)=(X397)))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[almodvs1_thm])])).
thf(c_0_79, plain, ![X380:$i > $o, X381:$i > $o, X382:$i > $o]:((X380)!=(ccfv @ X381 @ ccbs)|((X382)!=(ccfv @ X381 @ ccur)|(~cwcel @ X381 @ ccrg|cwcel @ X382 @ X380))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aringidcl_thm])])).
thf(c_0_80, plain, ![X264:$i > $o]:(~cwcel @ X264 @ ccasa|cwcel @ X264 @ ccrg), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aassaring_thm])])).
thf(c_0_81, plain, ![X327:$i > $o, X328:$i > $o, X329:$i > $o, X330:$i > $o, X331:$i > $o, X332:$i > $o, X333:$i > $o, X334:$i > $o, X335:$i > $o]:((X332)!=(ccfv @ X333 @ ccbs)|((X331)!=(ccfv @ X333 @ ccsca)|((X328)!=(ccfv @ X331 @ ccbs)|((X329)!=(ccfv @ X333 @ ccvsca)|((X330)!=(ccfv @ X333 @ ccmulr)|(~cwcel @ X333 @ ccasa|(~cwcel @ X327 @ X328|~cwcel @ X334 @ X332|~cwcel @ X335 @ X332)|(cco @ X334 @ (cco @ X327 @ X335 @ X329) @ X330)=(cco @ X327 @ (cco @ X334 @ X335 @ X330) @ X329))))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aassaassr_thm])])).
thf(c_0_82, plain, ![X5:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o, X6:$i > $o, X9:$i > $o, X8:$i > $o, X7:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ X5 @ (ccfv @ X6 @ ccmulr))=(cco @ X2 @ (cco @ X3 @ X5 @ (ccfv @ X6 @ ccmulr)) @ X4)|(X4)!=(ccfv @ X6 @ ccvsca)|(X7)!=(ccfv @ X8 @ ccbs)|(X8)!=(ccfv @ X6 @ ccsca)|(X9)!=(ccfv @ X6 @ ccbs)|~cwcel @ X6 @ ccasa|~cwcel @ X5 @ X9|~cwcel @ X3 @ X9|~cwcel @ X2 @ X7), inference(er,[status(thm)],[c_0_66])).
thf(c_0_83, negated_conjecture, (ccfv @ epred1_0 @ ccsca)=(epred4_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_26])).
thf(c_0_84, negated_conjecture, cwcel @ epred1_0 @ ccasa, inference(er,[status(thm)],[c_0_69])).
thf(c_0_85, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (ccfv @ X2 @ X3) @ (ccfv @ epred4_0 @ ccbs)|(X3)!=(epred7_0)|(X4)!=(epred12_0)|~cwcel @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_64]), c_0_68])])).
thf(c_0_86, negated_conjecture, cwcel @ (ccfv @ epred10_0 @ epred3_0) @ epred12_0, inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_87, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwf @ X2 @ X2 @ X3|(X2)!=(epred2_0)|(X3)!=(epred9_0)), inference(spm,[status(thm)],[c_0_72, c_0_36])).
thf(c_0_88, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X5:$i > $o, X3:$i > $o, X6:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ (ccfv @ X4 @ ccmulr))=(cco @ (ccfv @ X2 @ X5) @ (ccfv @ X4 @ ccur) @ (ccfv @ X4 @ ccvsca))|(X6)!=(ccfv @ X4 @ ccbs)|(X5)!=(epred3_0)|(X3)!=(epred9_0)|(X4)!=(epred1_0)|~cwcel @ X2 @ X6), inference(er,[status(thm)],[c_0_73])).
thf(c_0_89, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ epred10_0 @ (ccfv @ epred10_0 @ X2) @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ epred10_0 @ X3) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)|(X3)!=(epred3_0)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_74, c_0_43])).
thf(c_0_90, plain, ![X2:$i > $o, X6:$i > $o, X5:$i > $o, X4:$i > $o, X3:$i > $o, X8:$i > $o, X9:$i > $o, X7:$i > $o]:((cco @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccmulr)) @ X5 @ X6)=(cco @ X2 @ (cco @ X3 @ X5 @ X6) @ X6)|(X7)!=(ccfv @ X4 @ ccbs)|(X6)!=(ccfv @ X8 @ ccvsca)|(X4)!=(ccfv @ X8 @ ccsca)|(X9)!=(ccfv @ X8 @ ccbs)|~cwcel @ X8 @ cclmod|~cwcel @ X5 @ X9|~cwcel @ X3 @ X7|~cwcel @ X2 @ X7), inference(er,[status(thm)],[c_0_75])).
thf(c_0_91, negated_conjecture, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ (ccfv @ epred4_0 @ ccbs)|(X3)!=(epred12_0)|~cwcel @ X2 @ X3), inference(er,[status(thm)],[c_0_76])).
thf(c_0_92, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ (ccfv @ epred4_0 @ ccmulr))=(ccfv @ epred4_0 @ ccur)|(X3)!=(epred7_0)|(X4)!=(epred12_0)|~cwcel @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_71]), c_0_64]), c_0_68])])).
thf(c_0_93, plain, ![X3:$i > $o, X5:$i > $o, X6:$i > $o, X7:$i > $o, X4:$i > $o, X2:$i > $o]:((cco @ X6 @ X7 @ X5)=(X7)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccsca)|(X5)!=(ccfv @ X3 @ ccvsca)|(X6)!=(ccfv @ X4 @ ccur)|~cwcel @ X3 @ cclmod|~cwcel @ X7 @ X2), inference(split_conjunct,[status(thm)],[c_0_78])).
thf(c_0_94, plain, ![X273:$i > $o]:(~cwcel @ X273 @ ccasa|cwcel @ X273 @ cclmod), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aassalmod_thm])])).
thf(c_0_95, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o]:(cwcel @ X4 @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccur)|~cwcel @ X3 @ ccrg), inference(split_conjunct,[status(thm)],[c_0_79])).
thf(c_0_96, plain, ![X2:$i > $o]:(cwcel @ X2 @ ccrg|~cwcel @ X2 @ ccasa), inference(split_conjunct,[status(thm)],[c_0_80])).
thf(c_0_97, plain, ![X4:$i > $o, X6:$i > $o, X7:$i > $o, X5:$i > $o, X3:$i > $o, X9:$i > $o, X10:$i > $o, X8:$i > $o, X2:$i > $o]:((cco @ X9 @ (cco @ X8 @ X10 @ X6) @ X7)=(cco @ X8 @ (cco @ X9 @ X10 @ X7) @ X6)|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccsca)|(X5)!=(ccfv @ X4 @ ccbs)|(X6)!=(ccfv @ X3 @ ccvsca)|(X7)!=(ccfv @ X3 @ ccmulr)|~cwcel @ X3 @ ccasa|~cwcel @ X8 @ X5|~cwcel @ X9 @ X2|~cwcel @ X10 @ X2), inference(split_conjunct,[status(thm)],[c_0_81])).
thf(c_0_98, plain, ![X229:$o, X230:$i > $o, X231:$i > $o, X232:$i > $o, X233:$i > $o, X234:$i > $o, X235:$i > $o, X236:$i > $o, X237:$i > $o]:(((((((cwcel @ X236 @ X233|~X229|X229|X229|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))&((((cwcel @ X236 @ X233|~X229|X229|X229|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))))&(((((cwcel @ X236 @ X233|~X229|X229|X229|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))&((((cwcel @ X236 @ X233|~X229|X229|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|X229|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))))&((((((cwcel @ X236 @ X233|~X229|X229|X229|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))&((((cwcel @ X236 @ X233|~X229|X229|X229|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|X229|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))))&(((((cwcel @ X236 @ X233|~X229|X229|X229|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|X229|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))&((((cwcel @ X236 @ X233|~X229|X229|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|X229|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))))&(((cwcel @ X236 @ X233|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|X229|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))&((cwcel @ X236 @ X233|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs))&((ccfv @ X236 @ X235)=(X237)|~X229|(cco @ X237 @ X236 @ X232)!=(X234)|(cco @ X236 @ X237 @ X232)!=(X234)|~cwcel @ X237 @ X230|~cwcel @ X236 @ X230|~cwcel @ X231 @ ccrg|(X235)!=(ccfv @ X231 @ ccinvr)|(X233)!=(ccfv @ X231 @ ccui)|(X234)!=(ccfv @ X231 @ ccur)|(X232)!=(ccfv @ X231 @ ccmulr)|(X230)!=(ccfv @ X231 @ ccbs)))))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ainvrvald_thm])])])).
thf(c_0_99, negated_conjecture, ![X3:$i > $o, X5:$i > $o, X4:$i > $o, X2:$i > $o, X8:$i > $o, X7:$i > $o, X6:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ X5 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ X2 @ (cco @ X3 @ X5 @ (ccfv @ epred1_0 @ ccmulr)) @ X4)|(X6)!=(ccfv @ X7 @ ccbs)|(X4)!=(epred5_0)|(X7)!=(epred4_0)|(X8)!=(epred2_0)|~cwcel @ X5 @ X8|~cwcel @ X3 @ X8|~cwcel @ X2 @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_61]), c_0_83]), c_0_36]), c_0_84])])).
thf(c_0_100, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ X2) @ (ccfv @ epred4_0 @ ccbs)|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_85, c_0_86])).
thf(c_0_101, plain, ![X299:$o, X300:$i > $o, X301:$i > $o, X302:$i > $o, X303:$i > $o]:(((X299|(~X299|cwcel @ (ccfv @ X302 @ X303) @ X301)|X299)&(~cwcel @ X302 @ X300|(~X299|cwcel @ (ccfv @ X302 @ X303) @ X301)|X299))&((X299|(~X299|cwcel @ (ccfv @ X302 @ X303) @ X301)|~cwf @ X300 @ X301 @ X303)&(~cwcel @ X302 @ X300|(~X299|cwcel @ (ccfv @ X302 @ X303) @ X301)|~cwf @ X300 @ X301 @ X303))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[affvelrnd_thm])])])).
thf(c_0_102, negated_conjecture, ![X2:$i > $o]:(cwf @ epred2_0 @ epred2_0 @ X2|(X2)!=(epred9_0)), inference(er,[status(thm)],[c_0_87])).
thf(c_0_103, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (ccfv @ X2 @ X3) @ X2 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ X2 @ X4) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)|(X5)!=(epred2_0)|(X4)!=(epred3_0)|(X3)!=(epred9_0)|~cwcel @ X2 @ X5), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_36]), c_0_61])).
thf(c_0_104, negated_conjecture, ![X2:$i > $o]:((cco @ epred10_0 @ (ccfv @ epred10_0 @ X2) @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)|(X2)!=(epred9_0)), inference(er,[status(thm)],[c_0_89])).
thf(c_0_105, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X5:$i > $o, X7:$i > $o, X6:$i > $o, X8:$i > $o]:((cco @ (cco @ X2 @ X3 @ (ccfv @ X4 @ ccmulr)) @ X5 @ X6)=(cco @ X2 @ (cco @ X3 @ X5 @ X6) @ X6)|(X6)!=(ccfv @ X7 @ ccvsca)|(X4)!=(ccfv @ X7 @ ccsca)|(X8)!=(ccfv @ X7 @ ccbs)|~cwcel @ X3 @ (ccfv @ X4 @ ccbs)|~cwcel @ X2 @ (ccfv @ X4 @ ccbs)|~cwcel @ X7 @ cclmod|~cwcel @ X5 @ X8), inference(er,[status(thm)],[c_0_90])).
thf(c_0_106, negated_conjecture, cwcel @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred4_0 @ ccbs), inference(spm,[status(thm)],[c_0_91, c_0_86])).
thf(c_0_107, negated_conjecture, ![X2:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ X2) @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred4_0 @ ccmulr))=(ccfv @ epred4_0 @ ccur)|(X2)!=(epred7_0)), inference(spm,[status(thm)],[c_0_92, c_0_86])).
thf(c_0_108, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o, X6:$i > $o]:((cco @ (ccfv @ X2 @ ccur) @ X3 @ X4)=(X3)|(X4)!=(ccfv @ X5 @ ccvsca)|(X2)!=(ccfv @ X5 @ ccsca)|(X6)!=(ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclmod|~cwcel @ X3 @ X6), inference(er,[status(thm)],[c_0_93])).
thf(c_0_109, plain, ![X2:$i > $o]:(cwcel @ X2 @ cclmod|~cwcel @ X2 @ ccasa), inference(split_conjunct,[status(thm)],[c_0_94])).
thf(c_0_110, plain, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (ccfv @ X2 @ ccur) @ X3|(X3)!=(ccfv @ X2 @ ccbs)|~cwcel @ X2 @ ccrg), inference(er,[status(thm)],[c_0_95])).
thf(c_0_111, negated_conjecture, cwcel @ epred1_0 @ ccrg, inference(spm,[status(thm)],[c_0_96, c_0_84])).
thf(c_0_112, plain, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X6:$i > $o, X5:$i > $o, X9:$i > $o, X8:$i > $o, X7:$i > $o]:((cco @ X2 @ (cco @ X3 @ X4 @ (ccfv @ X5 @ ccmulr)) @ X6)=(cco @ X3 @ (cco @ X2 @ X4 @ X6) @ (ccfv @ X5 @ ccmulr))|(X6)!=(ccfv @ X5 @ ccvsca)|(X7)!=(ccfv @ X8 @ ccbs)|(X8)!=(ccfv @ X5 @ ccsca)|(X9)!=(ccfv @ X5 @ ccbs)|~cwcel @ X5 @ ccasa|~cwcel @ X4 @ X9|~cwcel @ X3 @ X9|~cwcel @ X2 @ X7), inference(er,[status(thm)],[c_0_97])).
thf(c_0_113, plain, ![X309:$i > $o, X310:$i > $o, X311:$i > $o, X312:$i > $o, X313:$i > $o, X314:$i > $o, X315:$i > $o]:((X313)!=(ccfv @ X314 @ ccbs)|((X311)!=(ccfv @ X314 @ ccsca)|((X310)!=(ccfv @ X314 @ ccvsca)|((X312)!=(ccfv @ X311 @ ccbs)|(~cwcel @ X314 @ cclmod|~cwcel @ X309 @ X312|~cwcel @ X315 @ X313|cwcel @ (cco @ X309 @ X315 @ X310) @ X313))))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[almodvscl_thm])])).
thf(c_0_114, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X6:$i > $o, X5:$i > $o, X7:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ X2 @ X3|(cco @ X4 @ X2 @ X5)!=(X6)|(cco @ X2 @ X4 @ X5)!=(X6)|~cwcel @ X4 @ X7|~cwcel @ X2 @ X7|~cwcel @ X8 @ ccrg|(X9)!=(ccfv @ X8 @ ccinvr)|(X3)!=(ccfv @ X8 @ ccui)|(X6)!=(ccfv @ X8 @ ccur)|(X5)!=(ccfv @ X8 @ ccmulr)|(X7)!=(ccfv @ X8 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_98])])])).
thf(c_0_115, negated_conjecture, ![X2:$i > $o, X5:$i > $o, X4:$i > $o, X3:$i > $o, X6:$i > $o, X7:$i > $o]:((cco @ (cco @ X2 @ X3 @ X4) @ X5 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ X2 @ (cco @ X3 @ X5 @ (ccfv @ epred1_0 @ ccmulr)) @ X4)|(X4)!=(epred5_0)|(X6)!=(epred4_0)|(X7)!=(epred2_0)|~cwcel @ X2 @ (ccfv @ X6 @ ccbs)|~cwcel @ X5 @ X7|~cwcel @ X3 @ X7), inference(er,[status(thm)],[c_0_99])).
thf(c_0_116, negated_conjecture, cwcel @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred4_0 @ ccbs), inference(er,[status(thm)],[c_0_100])).
thf(c_0_117, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o]:(cwcel @ (ccfv @ X2 @ X4) @ X5|~cwcel @ X2 @ X3|~cwf @ X3 @ X5 @ X4), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_101])])])).
thf(c_0_118, negated_conjecture, cwf @ epred2_0 @ epred2_0 @ epred9_0, inference(er,[status(thm)],[c_0_102])).
thf(c_0_119, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (ccfv @ epred10_0 @ X2) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ epred10_0 @ X3) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)|(X3)!=(epred3_0)|(X2)!=(epred9_0)), inference(spm,[status(thm)],[c_0_103, c_0_43])).
thf(c_0_120, negated_conjecture, (cco @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)=(cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)), inference(er,[status(thm)],[c_0_104])).
thf(c_0_121, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X4:$i > $o, X6:$i > $o]:((cco @ (cco @ X2 @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred4_0 @ ccmulr)) @ X3 @ X4)=(cco @ X2 @ (cco @ (ccfv @ epred10_0 @ epred3_0) @ X3 @ X4) @ X4)|(ccfv @ X5 @ ccsca)!=(epred4_0)|(X4)!=(ccfv @ X5 @ ccvsca)|(X6)!=(ccfv @ X5 @ ccbs)|~cwcel @ X2 @ (ccfv @ epred4_0 @ ccbs)|~cwcel @ X5 @ cclmod|~cwcel @ X3 @ X6), inference(spm,[status(thm)],[c_0_105, c_0_106])).
thf(c_0_122, negated_conjecture, (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred4_0 @ ccmulr))=(ccfv @ epred4_0 @ ccur), inference(er,[status(thm)],[c_0_107])).
thf(c_0_123, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ (ccfv @ X2 @ ccur) @ X3 @ (ccfv @ X4 @ ccvsca))=(X3)|(X2)!=(ccfv @ X4 @ ccsca)|(X5)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclmod|~cwcel @ X3 @ X5), inference(er,[status(thm)],[c_0_108])).
thf(c_0_124, negated_conjecture, cwcel @ epred1_0 @ cclmod, inference(spm,[status(thm)],[c_0_109, c_0_84])).
thf(c_0_125, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ epred1_0 @ ccur) @ X2|(X2)!=(epred2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_36]), c_0_111])])).
thf(c_0_126, negated_conjecture, ![X3:$i > $o, X5:$i > $o, X4:$i > $o, X2:$i > $o, X8:$i > $o, X7:$i > $o, X6:$i > $o]:((cco @ X2 @ (cco @ X3 @ X4 @ (ccfv @ epred1_0 @ ccmulr)) @ X5)=(cco @ X3 @ (cco @ X2 @ X4 @ X5) @ (ccfv @ epred1_0 @ ccmulr))|(X6)!=(ccfv @ X7 @ ccbs)|(X5)!=(epred5_0)|(X7)!=(epred4_0)|(X8)!=(epred2_0)|~cwcel @ X4 @ X8|~cwcel @ X3 @ X8|~cwcel @ X2 @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_61]), c_0_83]), c_0_36]), c_0_84])])).
thf(c_0_127, plain, ![X3:$i > $o, X5:$i > $o, X6:$i > $o, X4:$i > $o, X8:$i > $o, X7:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X7 @ X8 @ X5) @ X2|(X2)!=(ccfv @ X3 @ ccbs)|(X4)!=(ccfv @ X3 @ ccsca)|(X5)!=(ccfv @ X3 @ ccvsca)|(X6)!=(ccfv @ X4 @ ccbs)|~cwcel @ X3 @ cclmod|~cwcel @ X7 @ X6|~cwcel @ X8 @ X2), inference(split_conjunct,[status(thm)],[c_0_113])).
thf(c_0_128, plain, ![X2:$i > $o, X3:$i > $o, X5:$i > $o, X7:$i > $o, X8:$i > $o, X6:$i > $o, X4:$i > $o]:(cwcel @ X2 @ X3|(X4)!=(ccfv @ X5 @ ccbs)|(X6)!=(ccfv @ X5 @ ccur)|(X7)!=(ccfv @ X5 @ ccmulr)|(X3)!=(ccfv @ X5 @ ccui)|(cco @ X8 @ X2 @ X7)!=(X6)|(cco @ X2 @ X8 @ X7)!=(X6)|~cwcel @ X5 @ ccrg|~cwcel @ X8 @ X4|~cwcel @ X2 @ X4), inference(er,[status(thm)],[c_0_114])).
thf(c_0_129, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ X2 @ X3) @ X4 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ X2 @ X4 @ (ccfv @ epred1_0 @ ccmulr)) @ X3)|(X3)!=(epred5_0)|(X5)!=(epred2_0)|~cwcel @ X4 @ X5|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_115, c_0_116])).
thf(c_0_130, negated_conjecture, ![X2:$i > $o]:(cwcel @ (ccfv @ X2 @ epred9_0) @ epred2_0|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_117, c_0_118])).
thf(c_0_131, negated_conjecture, ![X2:$i > $o]:((cco @ (ccfv @ epred10_0 @ X2) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr))|(X2)!=(epred9_0)), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_119]), c_0_120])).
thf(c_0_132, negated_conjecture, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X5:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ (ccfv @ epred10_0 @ epred3_0) @ X2 @ X3) @ X3)=(cco @ (ccfv @ epred4_0 @ ccur) @ X2 @ X3)|(ccfv @ X4 @ ccsca)!=(epred4_0)|(X3)!=(ccfv @ X4 @ ccvsca)|(X5)!=(ccfv @ X4 @ ccbs)|~cwcel @ X4 @ cclmod|~cwcel @ X2 @ X5), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_116]), c_0_122])).
thf(c_0_133, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((cco @ (ccfv @ X2 @ ccur) @ X3 @ epred5_0)=(X3)|(X2)!=(epred4_0)|(X4)!=(epred2_0)|~cwcel @ X3 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_83]), c_0_61]), c_0_36]), c_0_124])])).
thf(c_0_134, negated_conjecture, cwcel @ (ccfv @ epred1_0 @ ccur) @ epred2_0, inference(er,[status(thm)],[c_0_125])).
thf(c_0_135, negated_conjecture, ![X2:$i > $o, X5:$i > $o, X4:$i > $o, X3:$i > $o, X6:$i > $o, X7:$i > $o]:((cco @ X2 @ (cco @ X3 @ X4 @ (ccfv @ epred1_0 @ ccmulr)) @ X5)=(cco @ X3 @ (cco @ X2 @ X4 @ X5) @ (ccfv @ epred1_0 @ ccmulr))|(X5)!=(epred5_0)|(X6)!=(epred4_0)|(X7)!=(epred2_0)|~cwcel @ X2 @ (ccfv @ X6 @ ccbs)|~cwcel @ X4 @ X7|~cwcel @ X3 @ X7), inference(er,[status(thm)],[c_0_126])).
thf(c_0_136, plain, ![X2:$i > $o, X4:$i > $o, X3:$i > $o, X7:$i > $o, X6:$i > $o, X5:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ X4) @ X5|(X4)!=(ccfv @ X6 @ ccvsca)|(X7)!=(ccfv @ X6 @ ccsca)|(X5)!=(ccfv @ X6 @ ccbs)|~cwcel @ X2 @ (ccfv @ X7 @ ccbs)|~cwcel @ X6 @ cclmod|~cwcel @ X3 @ X5), inference(er,[status(thm)],[c_0_127])).
thf(c_0_137, plain, ![X2:$i > $o, X3:$i > $o, X4:$i > $o, X6:$i > $o, X5:$i > $o, X7:$i > $o, X9:$i > $o, X8:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(cco @ X4 @ X2 @ X5)!=(X6)|(cco @ X2 @ X4 @ X5)!=(X6)|~cwcel @ X4 @ X7|~cwcel @ X2 @ X7|~cwcel @ X8 @ ccrg|(X3)!=(ccfv @ X8 @ ccinvr)|(X9)!=(ccfv @ X8 @ ccui)|(X6)!=(ccfv @ X8 @ ccur)|(X5)!=(ccfv @ X8 @ ccmulr)|(X7)!=(ccfv @ X8 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_98])])])).
thf(c_0_138, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X7:$i > $o, X6:$i > $o, X5:$i > $o]:(cwcel @ X2 @ X3|(X4)!=(ccfv @ X5 @ ccur)|(X6)!=(ccfv @ X5 @ ccmulr)|(X3)!=(ccfv @ X5 @ ccui)|(cco @ X7 @ X2 @ X6)!=(X4)|(cco @ X2 @ X7 @ X6)!=(X4)|~cwcel @ X7 @ (ccfv @ X5 @ ccbs)|~cwcel @ X2 @ (ccfv @ X5 @ ccbs)|~cwcel @ X5 @ ccrg), inference(er,[status(thm)],[c_0_128])).
thf(c_0_139, negated_conjecture, (epred6_0)=(ccfv @ epred1_0 @ ccui), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_140, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ X2 @ X3) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ X2 @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr)) @ X3)|(X3)!=(epred5_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_129, c_0_43])).
thf(c_0_141, negated_conjecture, cwcel @ (ccfv @ epred10_0 @ epred9_0) @ epred2_0, inference(spm,[status(thm)],[c_0_130, c_0_43])).
thf(c_0_142, negated_conjecture, (cco @ (ccfv @ epred10_0 @ epred9_0) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)), inference(er,[status(thm)],[c_0_131])).
thf(c_0_143, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ (ccfv @ epred10_0 @ epred3_0) @ X2 @ X3) @ X3)=(cco @ (ccfv @ epred4_0 @ ccur) @ X2 @ X3)|(X3)!=(epred5_0)|(X4)!=(epred2_0)|~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_132, c_0_61]), c_0_83]), c_0_36]), c_0_124])])).
thf(c_0_144, negated_conjecture, ![X2:$i > $o]:((cco @ (ccfv @ X2 @ ccur) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)=(ccfv @ epred1_0 @ ccur)|(X2)!=(epred4_0)), inference(spm,[status(thm)],[c_0_133, c_0_134])).
thf(c_0_145, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X5:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ X2 @ X3 @ (ccfv @ epred1_0 @ ccmulr)) @ X4)=(cco @ X2 @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ X3 @ X4) @ (ccfv @ epred1_0 @ ccmulr))|(X4)!=(epred5_0)|(X5)!=(epred2_0)|~cwcel @ X3 @ X5|~cwcel @ X2 @ X5), inference(spm,[status(thm)],[c_0_135, c_0_116])).
thf(c_0_146, negated_conjecture, ![X3:$i > $o, X2:$i > $o, X5:$i > $o, X4:$i > $o]:(cwcel @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ X2 @ X3) @ X4|(ccfv @ X5 @ ccsca)!=(epred4_0)|(X3)!=(ccfv @ X5 @ ccvsca)|(X4)!=(ccfv @ X5 @ ccbs)|~cwcel @ X5 @ cclmod|~cwcel @ X2 @ X4), inference(spm,[status(thm)],[c_0_136, c_0_116])).
thf(c_0_147, plain, ![X3:$i > $o, X2:$i > $o, X4:$i > $o, X8:$i > $o, X7:$i > $o, X6:$i > $o, X5:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(X5)!=(ccfv @ X6 @ ccbs)|(X7)!=(ccfv @ X6 @ ccur)|(X8)!=(ccfv @ X6 @ ccmulr)|(X3)!=(ccfv @ X6 @ ccinvr)|(cco @ X4 @ X2 @ X8)!=(X7)|(cco @ X2 @ X4 @ X8)!=(X7)|~cwcel @ X6 @ ccrg|~cwcel @ X4 @ X5|~cwcel @ X2 @ X5), inference(er,[status(thm)],[c_0_137])).
thf(c_0_148, negated_conjecture, ![X3:$i > $o, X5:$i > $o, X6:$i > $o, X4:$i > $o, X2:$i > $o]:(cwcel @ X2 @ X3|(X4)!=(ccfv @ epred1_0 @ ccur)|(X5)!=(ccfv @ epred1_0 @ ccmulr)|(cco @ X6 @ X2 @ X5)!=(X4)|(cco @ X2 @ X6 @ X5)!=(X4)|(X3)!=(epred6_0)|~cwcel @ X6 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_138, c_0_36]), c_0_139]), c_0_111])])).
thf(c_0_149, negated_conjecture, ![X2:$i > $o]:((cco @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ X2) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)) @ X2)|(X2)!=(epred5_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_140, c_0_141]), c_0_142])).
thf(c_0_150, negated_conjecture, ![X2:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ (ccfv @ epred10_0 @ epred3_0) @ (ccfv @ epred1_0 @ ccur) @ X2) @ X2)=(cco @ (ccfv @ epred4_0 @ ccur) @ (ccfv @ epred1_0 @ ccur) @ X2)|(X2)!=(epred5_0)), inference(spm,[status(thm)],[c_0_143, c_0_134])).
thf(c_0_151, negated_conjecture, (cco @ (ccfv @ epred4_0 @ ccur) @ (ccfv @ epred1_0 @ ccur) @ epred5_0)=(ccfv @ epred1_0 @ ccur), inference(er,[status(thm)],[c_0_144])).
thf(c_0_152, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ X2 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)) @ X3)=(cco @ X2 @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ X3) @ (ccfv @ epred1_0 @ ccmulr))|(X3)!=(epred5_0)|~cwcel @ X2 @ epred2_0), inference(spm,[status(thm)],[c_0_145, c_0_141])).
thf(c_0_153, negated_conjecture, ![X2:$i > $o, X3:$i > $o, X4:$i > $o]:(cwcel @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ X2 @ X3) @ X4|(X3)!=(epred5_0)|(X4)!=(epred2_0)|~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_146, c_0_61]), c_0_83]), c_0_36]), c_0_124])])).
thf(c_0_154, plain, ![X4:$i > $o, X3:$i > $o, X2:$i > $o, X5:$i > $o, X7:$i > $o, X6:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(X5)!=(ccfv @ X6 @ ccur)|(X7)!=(ccfv @ X6 @ ccmulr)|(X3)!=(ccfv @ X6 @ ccinvr)|(cco @ X4 @ X2 @ X7)!=(X5)|(cco @ X2 @ X4 @ X7)!=(X5)|~cwcel @ X4 @ (ccfv @ X6 @ ccbs)|~cwcel @ X2 @ (ccfv @ X6 @ ccbs)|~cwcel @ X6 @ ccrg), inference(er,[status(thm)],[c_0_147])).
thf(c_0_155, negated_conjecture, (epred8_0)=(ccfv @ epred1_0 @ ccinvr), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_156, negated_conjecture, ![X5:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwcel @ X2 @ X3|(cco @ X4 @ X2 @ X5)!=(ccfv @ epred1_0 @ ccur)|(cco @ X2 @ X4 @ X5)!=(ccfv @ epred1_0 @ ccur)|(X5)!=(ccfv @ epred1_0 @ ccmulr)|(X3)!=(epred6_0)|~cwcel @ X4 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(er,[status(thm)],[c_0_148])).
thf(c_0_157, negated_conjecture, (cco @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)) @ epred5_0), inference(er,[status(thm)],[c_0_149])).
thf(c_0_158, negated_conjecture, (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)) @ epred5_0)=(ccfv @ epred1_0 @ ccur), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_150]), c_0_120]), c_0_151])).
thf(c_0_159, negated_conjecture, ![X2:$i > $o]:((cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (cco @ epred10_0 @ (ccfv @ epred10_0 @ epred9_0) @ (ccfv @ epred1_0 @ ccmulr)) @ X2)=(cco @ epred10_0 @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ X2) @ (ccfv @ epred1_0 @ ccmulr))|(X2)!=(epred5_0)), inference(spm,[status(thm)],[c_0_152, c_0_43])).
thf(c_0_160, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ X2) @ epred2_0|(X2)!=(epred5_0)), inference(spm,[status(thm)],[c_0_153, c_0_141])).
thf(c_0_161, negated_conjecture, ![X6:$i > $o, X5:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(X5)!=(ccfv @ epred1_0 @ ccur)|(X6)!=(ccfv @ epred1_0 @ ccmulr)|(cco @ X4 @ X2 @ X6)!=(X5)|(cco @ X2 @ X4 @ X6)!=(X5)|(X3)!=(epred8_0)|~cwcel @ X4 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_154, c_0_36]), c_0_155]), c_0_111])])).
thf(c_0_162, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:(cwcel @ X2 @ X3|(cco @ X4 @ X2 @ (ccfv @ epred1_0 @ ccmulr))!=(ccfv @ epred1_0 @ ccur)|(cco @ X2 @ X4 @ (ccfv @ epred1_0 @ ccmulr))!=(ccfv @ epred1_0 @ ccur)|(X3)!=(epred6_0)|~cwcel @ X4 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(er,[status(thm)],[c_0_156])).
thf(c_0_163, negated_conjecture, (cco @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0) @ epred10_0 @ (ccfv @ epred1_0 @ ccmulr))=(ccfv @ epred1_0 @ ccur), inference(rw,[status(thm)],[c_0_157, c_0_158])).
thf(c_0_164, negated_conjecture, (cco @ epred10_0 @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0) @ (ccfv @ epred1_0 @ ccmulr))=(ccfv @ epred1_0 @ ccur), inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_159]), c_0_158])).
thf(c_0_165, negated_conjecture, cwcel @ (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0) @ epred2_0, inference(er,[status(thm)],[c_0_160])).
thf(c_0_166, negated_conjecture, ![X5:$i > $o, X4:$i > $o, X3:$i > $o, X2:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(cco @ X4 @ X2 @ X5)!=(ccfv @ epred1_0 @ ccur)|(cco @ X2 @ X4 @ X5)!=(ccfv @ epred1_0 @ ccur)|(X5)!=(ccfv @ epred1_0 @ ccmulr)|(X3)!=(epred8_0)|~cwcel @ X4 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(er,[status(thm)],[c_0_161])).
thf(c_0_167, negated_conjecture, ![X2:$i > $o]:(cwcel @ epred10_0 @ X2|(X2)!=(epred6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_163]), c_0_164]), c_0_165]), c_0_43])])).
thf(c_0_168, negated_conjecture, ![X4:$i > $o, X3:$i > $o, X2:$i > $o]:((ccfv @ X2 @ X3)=(X4)|(cco @ X4 @ X2 @ (ccfv @ epred1_0 @ ccmulr))!=(ccfv @ epred1_0 @ ccur)|(cco @ X2 @ X4 @ (ccfv @ epred1_0 @ ccmulr))!=(ccfv @ epred1_0 @ ccur)|(X3)!=(epred8_0)|~cwcel @ X4 @ epred2_0|~cwcel @ X2 @ epred2_0), inference(er,[status(thm)],[c_0_166])).
thf(c_0_169, negated_conjecture, (~cwcel @ epred10_0 @ epred6_0|(ccfv @ epred10_0 @ epred8_0)!=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0)), inference(split_conjunct,[status(thm)],[c_0_23])).
thf(c_0_170, negated_conjecture, cwcel @ epred10_0 @ epred6_0, inference(er,[status(thm)],[c_0_167])).
thf(c_0_171, negated_conjecture, ![X2:$i > $o]:((ccfv @ epred10_0 @ X2)=(cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0)|(X2)!=(epred8_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_168, c_0_163]), c_0_164]), c_0_165]), c_0_43])])).
thf(c_0_172, negated_conjecture, (cco @ (ccfv @ (ccfv @ epred10_0 @ epred3_0) @ epred7_0) @ (ccfv @ epred10_0 @ epred9_0) @ epred5_0)!=(ccfv @ epred10_0 @ epred8_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_169, c_0_170])])).
thf(c_0_173, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_171]), c_0_172]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 174
# Proof object clause steps            : 131
# Proof object formula steps           : 43
# Proof object conjectures             : 97
# Proof object clause conjectures      : 94
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 34
# Proof object initial formulas used   : 21
# Proof object generating inferences   : 94
# Proof object simplifying inferences  : 73
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 89
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 317
# Removed in clause preprocessing      : 282
# Initial clauses in saturation        : 35
# Processed clauses                    : 14540
# ...of these trivial                  : 729
# ...subsumed                          : 759
# ...remaining for further processing  : 13052
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 21
# Backward-rewritten                   : 356
# Generated clauses                    : 69420
# ...of the previous two non-trivial   : 68976
# Contextual simplify-reflections      : 9
# Paramodulations                      : 57642
# Factorizations                       : 0
# NegExts                              : 0
# Equation resolutions                 : 3106
# 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  : 10109
#    Positive orientable unit clauses  : 1248
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 1
#    Non-unit-clauses                  : 8860
# Current number of unprocessed clauses: 54321
# ...number of literals in the above   : 247286
# Current number of archived formulas  : 0
# Current number of archived clauses   : 2943
# Clause-clause subsumption calls (NU) : 16026685
# Rec. Clause-clause subsumption calls : 2144312
# Non-unit clause-clause subsumptions  : 789
# Unit Clause-clause subsumption calls : 341284
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 721176
# BW rewrite match successes           : 54
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 4520156

# -------------------------------------------------
# User time                : 11.995 s
# System time              : 0.084 s
# Total time               : 12.079 s
# Maximum resident set size: 84432 pages
