# Preprocessing time       : 0.032 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
thf(csibfinima_conj, conjecture, ![X1:$o, X12:$i > $o, X9:$i > $o, X15:$i > $o, X11:$i > $o, X22:$i > $o, X16:$i > $o, X17:$i > $o, X7:$i > $o, X14:$i > $o, X18:$i > $o, X21:$i > $o, X23:$i > $o, X19:$i > $o]:((X12)=(ccfv @ X18 @ ccbs)=>((X17)=(ccfv @ X18 @ cctopn)=>((X9)=(ccfv @ X17 @ ccsigagen)=>((X19)=(ccfv @ X18 @ cc0g)=>((X15)=(ccfv @ X18 @ ccvsca)=>((X16)=(ccfv @ (ccfv @ X18 @ ccsca) @ ccrrh)=>((X1=>cwcel @ X18 @ X14)=>((X1=>cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas)))=>((X1=>cwcel @ X11 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>((X1=>cwcel @ X22 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>((X1=>cwcel @ X18 @ cctps)=>((X1=>cwcel @ X17 @ cct1)=>((((X1&cwcel @ X21 @ (ccrn @ X11))&cwcel @ X23 @ (ccrn @ X22))&((X21)!=(X19)|(X23)!=(X19)))=>cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ X11) @ (ccsn @ X21)) @ (ccima @ (cccnv @ X22) @ (ccsn @ X23))) @ X7) @ (cco @ ccc0 @ ccpnf @ ccico)))))))))))))), file('mmset30834_sibfinima.p', csibfinima_conj)).
thf(asibff_thm, axiom, ![X1:$o, X12:$i > $o, X9:$i > $o, X15:$i > $o, X11:$i > $o, X16:$i > $o, X17:$i > $o, X7:$i > $o, X14:$i > $o, X18:$i > $o, X19:$i > $o]:((X12)=(ccfv @ X18 @ ccbs)=>((X17)=(ccfv @ X18 @ cctopn)=>((X9)=(ccfv @ X17 @ ccsigagen)=>((X19)=(ccfv @ X18 @ cc0g)=>((X15)=(ccfv @ X18 @ ccvsca)=>((X16)=(ccfv @ (ccfv @ X18 @ ccsca) @ ccrrh)=>((X1=>cwcel @ X18 @ X14)=>((X1=>cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas)))=>((X1=>cwcel @ X11 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>(X1=>cwf @ (ccuni @ (ccdm @ X7)) @ (ccuni @ X17) @ X11)))))))))), file('mmset30834_sibfinima.p', asibff_thm)).
thf(asibfmbl_thm, axiom, ![X1:$o, X12:$i > $o, X9:$i > $o, X15:$i > $o, X11:$i > $o, X16:$i > $o, X17:$i > $o, X7:$i > $o, X14:$i > $o, X18:$i > $o, X19:$i > $o]:((X12)=(ccfv @ X18 @ ccbs)=>((X17)=(ccfv @ X18 @ cctopn)=>((X9)=(ccfv @ X17 @ ccsigagen)=>((X19)=(ccfv @ X18 @ cc0g)=>((X15)=(ccfv @ X18 @ ccvsca)=>((X16)=(ccfv @ (ccfv @ X18 @ ccsca) @ ccrrh)=>((X1=>cwcel @ X18 @ X14)=>((X1=>cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas)))=>((X1=>cwcel @ X11 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>(X1=>cwcel @ X11 @ (cco @ (ccdm @ X7) @ X9 @ ccmbfm))))))))))), file('mmset30834_sibfinima.p', asibfmbl_thm)).
thf(at1sncld_thm, axiom, ![X8:$i > $o, X17:$i > $o, X21:$i > $o]:((X21)=(ccuni @ X17)=>((cwcel @ X17 @ cct1&cwcel @ X8 @ X21)=>cwcel @ (ccsn @ X8) @ (ccfv @ X17 @ cccld))), file('mmset30834_sibfinima.p', at1sncld_thm)).
thf(asseldd_thm, axiom, ![X1:$o, X8:$i > $o, X12:$i > $o, X13:$i > $o]:((X1=>cwss @ X8 @ X12)=>((X1=>cwcel @ X13 @ X8)=>(X1=>cwcel @ X13 @ X12))), file('mmset30834_sibfinima.p', asseldd_thm)).
thf(afrn_thm, axiom, ![X8:$i > $o, X12:$i > $o, X11:$i > $o]:(cwf @ X8 @ X12 @ X11=>cwss @ (ccrn @ X11) @ X12), file('mmset30834_sibfinima.p', afrn_thm)).
thf(atpstop_thm, axiom, ![X17:$i > $o, X20:$i > $o]:((X17)=(ccfv @ X20 @ cctopn)=>(cwcel @ X20 @ cctps=>cwcel @ X17 @ cctop)), file('mmset30834_sibfinima.p', atpstop_thm)).
thf(asibfima_thm, axiom, ![X1:$o, X8:$i > $o, X12:$i > $o, X9:$i > $o, X15:$i > $o, X11:$i > $o, X16:$i > $o, X17:$i > $o, X7:$i > $o, X14:$i > $o, X18:$i > $o, X19:$i > $o]:((X12)=(ccfv @ X18 @ ccbs)=>((X17)=(ccfv @ X18 @ cctopn)=>((X9)=(ccfv @ X17 @ ccsigagen)=>((X19)=(ccfv @ X18 @ cc0g)=>((X15)=(ccfv @ X18 @ ccvsca)=>((X16)=(ccfv @ (ccfv @ X18 @ ccsca) @ ccrrh)=>((X1=>cwcel @ X18 @ X14)=>((X1=>cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas)))=>((X1=>cwcel @ X11 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>((X1&cwcel @ X8 @ (ccdif @ (ccrn @ X11) @ (ccsn @ X19)))=>cwcel @ (ccfv @ (ccima @ (cccnv @ X11) @ (ccsn @ X8)) @ X7) @ (cco @ ccc0 @ ccpnf @ ccico))))))))))), file('mmset30834_sibfinima.p', asibfima_thm)).
thf(aeldifsn_thm, axiom, ![X8:$i > $o, X12:$i > $o, X13:$i > $o]:(cwcel @ X8 @ (ccdif @ X12 @ (ccsn @ X13))<=>(cwcel @ X8 @ X12&(X8)!=(X13))), file('mmset30834_sibfinima.p', aeldifsn_thm)).
thf(admmeas_thm, axiom, ![X7:$i > $o]:(cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas))=>cwcel @ (ccdm @ X7) @ (ccuni @ (ccrn @ ccsiga))), file('mmset30834_sibfinima.p', admmeas_thm)).
thf(ambfmcnvima_thm, axiom, ![X1:$o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o]:((X1=>cwcel @ X9 @ (ccuni @ (ccrn @ ccsiga)))=>((X1=>cwcel @ X10 @ (ccuni @ (ccrn @ ccsiga)))=>((X1=>cwcel @ X11 @ (cco @ X9 @ X10 @ ccmbfm))=>((X1=>cwcel @ X8 @ X10)=>(X1=>cwcel @ (ccima @ (cccnv @ X11) @ X8) @ X9))))), file('mmset30834_sibfinima.p', ambfmcnvima_thm)).
thf(asgsiga_thm, axiom, ![X1:$o, X8:$i > $o, X14:$i > $o]:((X1=>cwcel @ X8 @ X14)=>(X1=>cwcel @ (ccfv @ X8 @ ccsigagen) @ (ccuni @ (ccrn @ ccsiga)))), file('mmset30834_sibfinima.p', asgsiga_thm)).
thf(acldssbrsiga_thm, axiom, ![X17:$i > $o]:(cwcel @ X17 @ cctop=>cwss @ (ccfv @ X17 @ cccld) @ (ccfv @ X17 @ ccsigagen)), file('mmset30834_sibfinima.p', acldssbrsiga_thm)).
thf(ameasbasedom_thm, axiom, ![X7:$i > $o]:(cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas))<=>cwcel @ X7 @ (ccfv @ (ccdm @ X7) @ ccmeas)), file('mmset30834_sibfinima.p', ameasbasedom_thm)).
thf(ainelsiga_thm, axiom, ![X8:$i > $o, X12:$i > $o, X9:$i > $o]:(((cwcel @ X9 @ (ccuni @ (ccrn @ ccsiga))&cwcel @ X8 @ X9)&cwcel @ X12 @ X9)=>cwcel @ (ccin @ X8 @ X12) @ X9), file('mmset30834_sibfinima.p', ainelsiga_thm)).
thf(ameasssd_thm, axiom, ![X1:$o, X8:$i > $o, X12:$i > $o, X9:$i > $o, X7:$i > $o]:((X1=>cwcel @ X7 @ (ccfv @ X9 @ ccmeas))=>((X1=>cwcel @ X8 @ X9)=>((X1=>cwcel @ X12 @ X9)=>((X1=>cwss @ X8 @ X12)=>(X1=>cwbr @ (ccfv @ X8 @ X7) @ (ccfv @ X12 @ X7) @ ccle))))), file('mmset30834_sibfinima.p', ameasssd_thm)).
thf(ameasvxrge0_thm, axiom, ![X8:$i > $o, X9:$i > $o, X7:$i > $o]:((cwcel @ X7 @ (ccfv @ X9 @ ccmeas)&cwcel @ X8 @ X9)=>cwcel @ (ccfv @ X8 @ X7) @ (cco @ ccc0 @ ccpnf @ ccicc)), file('mmset30834_sibfinima.p', ameasvxrge0_thm)).
thf(ainss1_thm, axiom, ![X8:$i > $o, X12:$i > $o]:cwss @ (ccin @ X8 @ X12) @ X8, file('mmset30834_sibfinima.p', ainss1_thm)).
thf(aelxrge0_thm, axiom, ![X8:$i > $o]:(cwcel @ X8 @ (cco @ ccc0 @ ccpnf @ ccicc)<=>(cwcel @ X8 @ ccxr&cwbr @ ccc0 @ X8 @ ccle)), file('mmset30834_sibfinima.p', aelxrge0_thm)).
thf(axrlelttrd_thm, axiom, ![X1:$o, X8:$i > $o, X12:$i > $o, X13:$i > $o]:((X1=>cwcel @ X8 @ ccxr)=>((X1=>cwcel @ X12 @ ccxr)=>((X1=>cwcel @ X13 @ ccxr)=>((X1=>cwbr @ X8 @ X12 @ ccle)=>((X1=>cwbr @ X12 @ X13 @ cclt)=>(X1=>cwbr @ X8 @ X13 @ cclt)))))), file('mmset30834_sibfinima.p', axrlelttrd_thm)).
thf(aelico2_thm, axiom, ![X8:$i > $o, X12:$i > $o, X13:$i > $o]:((cwcel @ X8 @ ccr&cwcel @ X12 @ ccxr)=>(cwcel @ X13 @ (cco @ X8 @ X12 @ ccico)<=>((cwcel @ X13 @ ccr&cwbr @ X8 @ X13 @ ccle)&cwbr @ X13 @ X12 @ cclt))), file('mmset30834_sibfinima.p', aelico2_thm)).
thf(a_0re_thm, axiom, cwcel @ ccc0 @ ccr, file('mmset30834_sibfinima.p', a_0re_thm)).
thf(apnfxr_thm, axiom, cwcel @ ccpnf @ ccxr, file('mmset30834_sibfinima.p', apnfxr_thm)).
thf(axrre3_thm, axiom, ![X8:$i > $o, X12:$i > $o]:(((cwcel @ X8 @ ccxr&cwcel @ X12 @ ccr)&(cwbr @ X12 @ X8 @ ccle&cwbr @ X8 @ ccpnf @ cclt))=>cwcel @ X8 @ ccr), file('mmset30834_sibfinima.p', axrre3_thm)).
thf(ainss2_thm, axiom, ![X8:$i > $o, X12:$i > $o]:cwss @ (ccin @ X8 @ X12) @ X12, file('mmset30834_sibfinima.p', ainss2_thm)).
thf(c_0_25, negated_conjecture, ~(![X1:$o, X12:$i > $o, X9:$i > $o, X15:$i > $o, X11:$i > $o, X22:$i > $o, X16:$i > $o, X17:$i > $o, X7:$i > $o, X14:$i > $o, X18:$i > $o, X21:$i > $o, X23:$i > $o, X19:$i > $o]:((X12)=(ccfv @ X18 @ ccbs)=>((X17)=(ccfv @ X18 @ cctopn)=>((X9)=(ccfv @ X17 @ ccsigagen)=>((X19)=(ccfv @ X18 @ cc0g)=>((X15)=(ccfv @ X18 @ ccvsca)=>((X16)=(ccfv @ (ccfv @ X18 @ ccsca) @ ccrrh)=>((X1=>cwcel @ X18 @ X14)=>((X1=>cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas)))=>((X1=>cwcel @ X11 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>((X1=>cwcel @ X22 @ (ccdm @ (cco @ X18 @ X7 @ ccsitg)))=>((X1=>cwcel @ X18 @ cctps)=>((X1=>cwcel @ X17 @ cct1)=>((((X1&cwcel @ X21 @ (ccrn @ X11))&cwcel @ X23 @ (ccrn @ X22))&((X21)!=(X19)|(X23)!=(X19)))=>cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ X11) @ (ccsn @ X21)) @ (ccima @ (cccnv @ X22) @ (ccsn @ X23))) @ X7) @ (cco @ ccc0 @ ccpnf @ ccico))))))))))))))), inference(assume_negation,[status(cth)],[csibfinima_conj])).
thf(c_0_26, negated_conjecture, ((epred2_0)=(ccfv @ epred11_0 @ ccbs)&((epred8_0)=(ccfv @ epred11_0 @ cctopn)&((epred3_0)=(ccfv @ epred8_0 @ ccsigagen)&((epred14_0)=(ccfv @ epred11_0 @ cc0g)&((epred4_0)=(ccfv @ epred11_0 @ ccvsca)&((epred7_0)=(ccfv @ (ccfv @ epred11_0 @ ccsca) @ ccrrh)&((~epred1_0|cwcel @ epred11_0 @ epred10_0)&((~epred1_0|cwcel @ epred9_0 @ (ccuni @ (ccrn @ ccmeas)))&((~epred1_0|cwcel @ epred5_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg)))&((~epred1_0|cwcel @ epred6_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg)))&((~epred1_0|cwcel @ epred11_0 @ cctps)&((~epred1_0|cwcel @ epred8_0 @ cct1)&((((epred1_0&cwcel @ epred12_0 @ (ccrn @ epred5_0))&cwcel @ epred13_0 @ (ccrn @ epred6_0))&((epred12_0)!=(epred14_0)|(epred13_0)!=(epred14_0)))&~cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)))))))))))))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])).
thf(c_0_27, plain, ![X277:$o, X278:$i > $o, X279:$i > $o, X280:$i > $o, X281:$i > $o, X282:$i > $o, X283:$i > $o, X284:$i > $o, X285:$i > $o, X286:$i > $o, X287:$i > $o]:((((X277|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|X277|X277|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))&(~cwcel @ X281 @ (ccdm @ (cco @ X286 @ X284 @ ccsitg))|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|X277|X277|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs)))&((X277|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|~cwcel @ X284 @ (ccuni @ (ccrn @ ccmeas))|X277|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))&(~cwcel @ X281 @ (ccdm @ (cco @ X286 @ X284 @ ccsitg))|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|~cwcel @ X284 @ (ccuni @ (ccrn @ ccmeas))|X277|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))))&(((X277|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|X277|~cwcel @ X286 @ X285|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))&(~cwcel @ X281 @ (ccdm @ (cco @ X286 @ X284 @ ccsitg))|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|X277|~cwcel @ X286 @ X285|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs)))&((X277|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|~cwcel @ X284 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X286 @ X285|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))&(~cwcel @ X281 @ (ccdm @ (cco @ X286 @ X284 @ ccsitg))|(~X277|cwf @ (ccuni @ (ccdm @ X284)) @ (ccuni @ X283) @ X281)|~cwcel @ X284 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X286 @ X285|(X282)!=(ccfv @ (ccfv @ X286 @ ccsca) @ ccrrh)|(X280)!=(ccfv @ X286 @ ccvsca)|(X287)!=(ccfv @ X286 @ cc0g)|(X279)!=(ccfv @ X283 @ ccsigagen)|(X283)!=(ccfv @ X286 @ cctopn)|(X278)!=(ccfv @ X286 @ ccbs))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asibff_thm])])])).
thf(c_0_28, negated_conjecture, (cwcel @ epred6_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_29, negated_conjecture, epred1_0, inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_30, negated_conjecture, (cwcel @ epred9_0 @ (ccuni @ (ccrn @ ccmeas))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_31, negated_conjecture, (cwcel @ epred5_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_32, plain, ![X7:$i > $o, X9:$i > $o, X12:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X10:$i > $o, X16:$i > $o, X15:$i > $o, X8:$i > $o]:(cwf @ (ccuni @ (ccdm @ X9)) @ (ccuni @ X10) @ X7|~cwcel @ X7 @ (ccdm @ (cco @ X8 @ X9 @ ccsitg))|~cwcel @ X9 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X8 @ X11|(X12)!=(ccfv @ (ccfv @ X8 @ ccsca) @ ccrrh)|(X13)!=(ccfv @ X8 @ ccvsca)|(X14)!=(ccfv @ X8 @ cc0g)|(X15)!=(ccfv @ X10 @ ccsigagen)|(X10)!=(ccfv @ X8 @ cctopn)|(X16)!=(ccfv @ X8 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_27])])])).
thf(c_0_33, negated_conjecture, cwcel @ epred6_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
thf(c_0_34, negated_conjecture, (epred7_0)=(ccfv @ (ccfv @ epred11_0 @ ccsca) @ ccrrh), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_35, negated_conjecture, (epred2_0)=(ccfv @ epred11_0 @ ccbs), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_36, negated_conjecture, (epred14_0)=(ccfv @ epred11_0 @ cc0g), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_37, negated_conjecture, (epred4_0)=(ccfv @ epred11_0 @ ccvsca), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_38, negated_conjecture, (epred8_0)=(ccfv @ epred11_0 @ cctopn), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_39, negated_conjecture, cwcel @ epred9_0 @ (ccuni @ (ccrn @ ccmeas)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_29])])).
thf(c_0_40, negated_conjecture, cwcel @ epred5_0 @ (ccdm @ (cco @ epred11_0 @ epred9_0 @ ccsitg)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_29])])).
thf(c_0_41, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(ccfv @ X7 @ ccsigagen)|(X9)!=(epred7_0)|(X10)!=(epred2_0)|(X11)!=(epred14_0)|(X12)!=(epred4_0)|(X7)!=(epred8_0)|~cwcel @ epred11_0 @ X13), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_34]), c_0_35]), c_0_36]), c_0_37]), c_0_38]), c_0_39])])).
thf(c_0_42, negated_conjecture, (cwcel @ epred11_0 @ epred10_0|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_43, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(ccfv @ X7 @ ccsigagen)|(X9)!=(epred7_0)|(X10)!=(epred2_0)|(X11)!=(epred14_0)|(X12)!=(epred4_0)|(X7)!=(epred8_0)|~cwcel @ epred11_0 @ X13), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_40]), c_0_34]), c_0_35]), c_0_36]), c_0_37]), c_0_38]), c_0_39])])).
thf(c_0_44, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|(X7)!=(epred8_0)|~cwcel @ epred11_0 @ X12), inference(er,[status(thm)],[c_0_41])).
thf(c_0_45, negated_conjecture, cwcel @ epred11_0 @ epred10_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_29])])).
thf(c_0_46, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|(X7)!=(epred8_0)|~cwcel @ epred11_0 @ X12), inference(er,[status(thm)],[c_0_43])).
thf(c_0_47, plain, ![X251:$o, X252:$i > $o, X253:$i > $o, X254:$i > $o, X255:$i > $o, X256:$i > $o, X257:$i > $o, X258:$i > $o, X259:$i > $o, X260:$i > $o, X261:$i > $o]:((((X251|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|X251|X251|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))&(~cwcel @ X255 @ (ccdm @ (cco @ X260 @ X258 @ ccsitg))|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|X251|X251|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs)))&((X251|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|~cwcel @ X258 @ (ccuni @ (ccrn @ ccmeas))|X251|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))&(~cwcel @ X255 @ (ccdm @ (cco @ X260 @ X258 @ ccsitg))|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|~cwcel @ X258 @ (ccuni @ (ccrn @ ccmeas))|X251|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))))&(((X251|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|X251|~cwcel @ X260 @ X259|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))&(~cwcel @ X255 @ (ccdm @ (cco @ X260 @ X258 @ ccsitg))|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|X251|~cwcel @ X260 @ X259|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs)))&((X251|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|~cwcel @ X258 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X260 @ X259|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))&(~cwcel @ X255 @ (ccdm @ (cco @ X260 @ X258 @ ccsitg))|(~X251|cwcel @ X255 @ (cco @ (ccdm @ X258) @ X253 @ ccmbfm))|~cwcel @ X258 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X260 @ X259|(X256)!=(ccfv @ (ccfv @ X260 @ ccsca) @ ccrrh)|(X254)!=(ccfv @ X260 @ ccvsca)|(X261)!=(ccfv @ X260 @ cc0g)|(X253)!=(ccfv @ X257 @ ccsigagen)|(X257)!=(ccfv @ X260 @ cctopn)|(X252)!=(ccfv @ X260 @ ccbs))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asibfmbl_thm])])])).
thf(c_0_48, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|(X7)!=(epred8_0)), inference(spm,[status(thm)],[c_0_44, c_0_45])).
thf(c_0_49, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|(X7)!=(epred8_0)), inference(spm,[status(thm)],[c_0_46, c_0_45])).
thf(c_0_50, plain, ![X7:$i > $o, X9:$i > $o, X11:$i > $o, X13:$i > $o, X12:$i > $o, X10:$i > $o, X14:$i > $o, X16:$i > $o, X15:$i > $o, X8:$i > $o]:(cwcel @ X7 @ (cco @ (ccdm @ X9) @ X10 @ ccmbfm)|~cwcel @ X7 @ (ccdm @ (cco @ X8 @ X9 @ ccsitg))|~cwcel @ X9 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X8 @ X11|(X12)!=(ccfv @ (ccfv @ X8 @ ccsca) @ ccrrh)|(X13)!=(ccfv @ X8 @ ccvsca)|(X14)!=(ccfv @ X8 @ cc0g)|(X10)!=(ccfv @ X15 @ ccsigagen)|(X15)!=(ccfv @ X8 @ cctopn)|(X16)!=(ccfv @ X8 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_47])])])).
thf(c_0_51, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(epred2_0)|(X9)!=(epred14_0)|(X10)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_48])).
thf(c_0_52, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(epred2_0)|(X9)!=(epred14_0)|(X10)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_49])).
thf(c_0_53, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(ccfv @ X8 @ ccsigagen)|(X9)!=(epred7_0)|(X10)!=(epred2_0)|(X8)!=(epred8_0)|(X11)!=(epred14_0)|(X12)!=(epred4_0)|~cwcel @ epred11_0 @ X13), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_33]), c_0_34]), c_0_35]), c_0_38]), c_0_36]), c_0_37]), c_0_39])])).
thf(c_0_54, negated_conjecture, (epred3_0)=(ccfv @ epred8_0 @ ccsigagen), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_55, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(epred14_0)|(X9)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_51])).
thf(c_0_56, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(ccfv @ X8 @ ccsigagen)|(X9)!=(epred7_0)|(X10)!=(epred2_0)|(X8)!=(epred8_0)|(X11)!=(epred14_0)|(X12)!=(epred4_0)|~cwcel @ epred11_0 @ X13), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_40]), c_0_34]), c_0_35]), c_0_38]), c_0_36]), c_0_37]), c_0_39])])).
thf(c_0_57, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(epred14_0)|(X9)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_52])).
thf(c_0_58, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(epred3_0)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|~cwcel @ epred11_0 @ X12), inference(spm,[status(thm)],[c_0_53, c_0_54])).
thf(c_0_59, negated_conjecture, ![X8:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X8)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_55])).
thf(c_0_60, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(epred3_0)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)|~cwcel @ epred11_0 @ X12), inference(spm,[status(thm)],[c_0_56, c_0_54])).
thf(c_0_61, negated_conjecture, ![X8:$i > $o, X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X8)!=(epred4_0)|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_57])).
thf(c_0_62, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(epred3_0)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)), inference(spm,[status(thm)],[c_0_58, c_0_45])).
thf(c_0_63, plain, ![X294:$i > $o, X295:$i > $o, X296:$i > $o]:((X296)!=(ccuni @ X295)|(~cwcel @ X295 @ cct1|~cwcel @ X294 @ X296|cwcel @ (ccsn @ X294) @ (ccfv @ X295 @ cccld))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[at1sncld_thm])])).
thf(c_0_64, negated_conjecture, (cwcel @ epred8_0 @ cct1|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_65, plain, ![X262:$o, X263:$i > $o, X264:$i > $o, X265:$i > $o]:(((X262|(~X262|cwcel @ X265 @ X264)|X262)&(~cwcel @ X265 @ X263|(~X262|cwcel @ X265 @ X264)|X262))&((X262|(~X262|cwcel @ X265 @ X264)|~cwss @ X263 @ X264)&(~cwcel @ X265 @ X263|(~X262|cwcel @ X265 @ X264)|~cwss @ X263 @ X264))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asseldd_thm])])])).
thf(c_0_66, plain, ![X288:$i > $o, X289:$i > $o, X290:$i > $o]:(~cwf @ X288 @ X289 @ X290|cwss @ (ccrn @ X290) @ X289), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[afrn_thm])])).
thf(c_0_67, negated_conjecture, ![X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred6_0|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_59])).
thf(c_0_68, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o, X11:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ X7 @ ccmbfm)|(X7)!=(epred3_0)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred14_0)|(X11)!=(epred4_0)), inference(spm,[status(thm)],[c_0_60, c_0_45])).
thf(c_0_69, negated_conjecture, ![X7:$i > $o]:(cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ X7) @ epred5_0|(X7)!=(epred8_0)), inference(er,[status(thm)],[c_0_61])).
thf(c_0_70, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred7_0)|(X8)!=(epred2_0)|(X9)!=(epred14_0)|(X10)!=(epred4_0)), inference(er,[status(thm)],[c_0_62])).
thf(c_0_71, plain, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:(cwcel @ (ccsn @ X9) @ (ccfv @ X8 @ cccld)|(X7)!=(ccuni @ X8)|~cwcel @ X8 @ cct1|~cwcel @ X9 @ X7), inference(split_conjunct,[status(thm)],[c_0_63])).
thf(c_0_72, negated_conjecture, cwcel @ epred8_0 @ cct1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_29])])).
thf(c_0_73, plain, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwcel @ X7 @ X9|~cwcel @ X7 @ X8|~cwss @ X8 @ X9), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_65])])])).
thf(c_0_74, negated_conjecture, cwcel @ epred13_0 @ (ccrn @ epred6_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_75, plain, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwss @ (ccrn @ X9) @ X8|~cwf @ X7 @ X8 @ X9), inference(split_conjunct,[status(thm)],[c_0_66])).
thf(c_0_76, negated_conjecture, cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ epred8_0) @ epred6_0, inference(er,[status(thm)],[c_0_67])).
thf(c_0_77, plain, ![X274:$i > $o, X275:$i > $o]:((X274)!=(ccfv @ X275 @ cctopn)|(~cwcel @ X275 @ cctps|cwcel @ X274 @ cctop)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[atpstop_thm])])).
thf(c_0_78, negated_conjecture, (cwcel @ epred11_0 @ cctps|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_79, plain, ![X344:$o, X345:$i > $o, X346:$i > $o, X347:$i > $o, X348:$i > $o, X349:$i > $o, X350:$i > $o, X351:$i > $o, X352:$i > $o, X353:$i > $o, X354:$i > $o, X355:$i > $o]:((((X344|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|X344|X344|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))&(~cwcel @ X349 @ (ccdm @ (cco @ X354 @ X352 @ ccsitg))|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|X344|X344|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs)))&((X344|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|~cwcel @ X352 @ (ccuni @ (ccrn @ ccmeas))|X344|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))&(~cwcel @ X349 @ (ccdm @ (cco @ X354 @ X352 @ ccsitg))|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|~cwcel @ X352 @ (ccuni @ (ccrn @ ccmeas))|X344|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))))&(((X344|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|X344|~cwcel @ X354 @ X353|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))&(~cwcel @ X349 @ (ccdm @ (cco @ X354 @ X352 @ ccsitg))|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|X344|~cwcel @ X354 @ X353|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs)))&((X344|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|~cwcel @ X352 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X354 @ X353|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))&(~cwcel @ X349 @ (ccdm @ (cco @ X354 @ X352 @ ccsitg))|(~X344|~cwcel @ X345 @ (ccdif @ (ccrn @ X349) @ (ccsn @ X355))|cwcel @ (ccfv @ (ccima @ (cccnv @ X349) @ (ccsn @ X345)) @ X352) @ (cco @ ccc0 @ ccpnf @ ccico))|~cwcel @ X352 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X354 @ X353|(X350)!=(ccfv @ (ccfv @ X354 @ ccsca) @ ccrrh)|(X348)!=(ccfv @ X354 @ ccvsca)|(X355)!=(ccfv @ X354 @ cc0g)|(X347)!=(ccfv @ X351 @ ccsigagen)|(X351)!=(ccfv @ X354 @ cctopn)|(X346)!=(ccfv @ X354 @ ccbs))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asibfima_thm])])])).
thf(c_0_80, plain, ![X341:$i > $o, X342:$i > $o, X343:$i > $o]:(((cwcel @ X341 @ X342|~cwcel @ X341 @ (ccdif @ X342 @ (ccsn @ X343)))&((X341)!=(X343)|~cwcel @ X341 @ (ccdif @ X342 @ (ccsn @ X343))))&(~cwcel @ X341 @ X342|(X341)=(X343)|cwcel @ X341 @ (ccdif @ X342 @ (ccsn @ X343)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aeldifsn_thm])])])).
thf(c_0_81, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred7_0)|(X8)!=(epred2_0)|(X9)!=(epred14_0)|(X10)!=(epred4_0)), inference(er,[status(thm)],[c_0_68])).
thf(c_0_82, negated_conjecture, cwcel @ epred12_0 @ (ccrn @ epred5_0), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_83, negated_conjecture, cwf @ (ccuni @ (ccdm @ epred9_0)) @ (ccuni @ epred8_0) @ epred5_0, inference(er,[status(thm)],[c_0_69])).
thf(c_0_84, plain, ![X238:$i > $o]:(~cwcel @ X238 @ (ccuni @ (ccrn @ ccmeas))|cwcel @ (ccdm @ X238) @ (ccuni @ (ccrn @ ccsiga))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[admmeas_thm])])).
thf(c_0_85, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred2_0)|(X8)!=(epred14_0)|(X9)!=(epred4_0)), inference(er,[status(thm)],[c_0_70])).
thf(c_0_86, negated_conjecture, ![X7:$i > $o, X8:$i > $o]:(cwcel @ (ccsn @ X7) @ (ccfv @ epred8_0 @ cccld)|(X8)!=(ccuni @ epred8_0)|~cwcel @ X7 @ X8), inference(spm,[status(thm)],[c_0_71, c_0_72])).
thf(c_0_87, negated_conjecture, ![X7:$i > $o]:(cwcel @ epred13_0 @ X7|~cwss @ (ccrn @ epred6_0) @ X7), inference(spm,[status(thm)],[c_0_73, c_0_74])).
thf(c_0_88, negated_conjecture, cwss @ (ccrn @ epred6_0) @ (ccuni @ epred8_0), inference(spm,[status(thm)],[c_0_75, c_0_76])).
thf(c_0_89, plain, ![X7:$i > $o, X8:$i > $o]:(cwcel @ X7 @ cctop|(X7)!=(ccfv @ X8 @ cctopn)|~cwcel @ X8 @ cctps), inference(split_conjunct,[status(thm)],[c_0_77])).
thf(c_0_90, negated_conjecture, cwcel @ epred11_0 @ cctps, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_29])])).
thf(c_0_91, plain, ![X7:$i > $o, X10:$i > $o, X9:$i > $o, X12:$i > $o, X13:$i > $o, X14:$i > $o, X11:$i > $o, X15:$i > $o, X17:$i > $o, X16:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ (ccima @ (cccnv @ X7) @ (ccsn @ X10)) @ X9) @ (cco @ ccc0 @ ccpnf @ ccico)|~cwcel @ X7 @ (ccdm @ (cco @ X8 @ X9 @ ccsitg))|~cwcel @ X10 @ (ccdif @ (ccrn @ X7) @ (ccsn @ X11))|~cwcel @ X9 @ (ccuni @ (ccrn @ ccmeas))|~cwcel @ X8 @ X12|(X13)!=(ccfv @ (ccfv @ X8 @ ccsca) @ ccrrh)|(X14)!=(ccfv @ X8 @ ccvsca)|(X11)!=(ccfv @ X8 @ cc0g)|(X15)!=(ccfv @ X16 @ ccsigagen)|(X16)!=(ccfv @ X8 @ cctopn)|(X17)!=(ccfv @ X8 @ ccbs)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_79])])])).
thf(c_0_92, plain, ![X7:$i > $o, X9:$i > $o, X8:$i > $o]:((X7)=(X9)|cwcel @ X7 @ (ccdif @ X8 @ (ccsn @ X9))|~cwcel @ X7 @ X8), inference(split_conjunct,[status(thm)],[c_0_80])).
thf(c_0_93, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred2_0)|(X8)!=(epred14_0)|(X9)!=(epred4_0)), inference(er,[status(thm)],[c_0_81])).
thf(c_0_94, negated_conjecture, ![X7:$i > $o]:(cwcel @ epred12_0 @ X7|~cwss @ (ccrn @ epred5_0) @ X7), inference(spm,[status(thm)],[c_0_73, c_0_82])).
thf(c_0_95, negated_conjecture, cwss @ (ccrn @ epred5_0) @ (ccuni @ epred8_0), inference(spm,[status(thm)],[c_0_75, c_0_83])).
thf(c_0_96, plain, ![X239:$o, X240:$i > $o, X241:$i > $o, X242:$i > $o, X243:$i > $o]:(((((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|X239|X239)&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|X239|X239))&((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|X239|X239)&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|X239|X239)))&(((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|X239)&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|X239))&((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|X239)&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|X239))))&((((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|X239|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga)))&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|X239|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga))))&((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|X239|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga)))&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|X239|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga)))))&(((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga)))&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|X239|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga))))&((X239|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga)))&(~cwcel @ X240 @ X242|(~X239|cwcel @ (ccima @ (cccnv @ X243) @ X240) @ X241)|~cwcel @ X243 @ (cco @ X241 @ X242 @ ccmbfm)|~cwcel @ X242 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X241 @ (ccuni @ (ccrn @ ccsiga))))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ambfmcnvima_thm])])])).
thf(c_0_97, plain, ![X7:$i > $o]:(cwcel @ (ccdm @ X7) @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas))), inference(split_conjunct,[status(thm)],[c_0_84])).
thf(c_0_98, negated_conjecture, ![X7:$i > $o, X8:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred14_0)|(X8)!=(epred4_0)), inference(er,[status(thm)],[c_0_85])).
thf(c_0_99, plain, ![X248:$o, X249:$i > $o, X250:$i > $o]:((X248|(~X248|cwcel @ (ccfv @ X249 @ ccsigagen) @ (ccuni @ (ccrn @ ccsiga))))&(~cwcel @ X249 @ X250|(~X248|cwcel @ (ccfv @ X249 @ ccsigagen) @ (ccuni @ (ccrn @ ccsiga))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[asgsiga_thm])])])).
thf(c_0_100, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccsn @ X7) @ (ccfv @ epred8_0 @ cccld)|~cwcel @ X7 @ (ccuni @ epred8_0)), inference(er,[status(thm)],[c_0_86])).
thf(c_0_101, negated_conjecture, cwcel @ epred13_0 @ (ccuni @ epred8_0), inference(spm,[status(thm)],[c_0_87, c_0_88])).
thf(c_0_102, plain, ![X276:$i > $o]:(~cwcel @ X276 @ cctop|cwss @ (ccfv @ X276 @ cccld) @ (ccfv @ X276 @ ccsigagen)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[acldssbrsiga_thm])])).
thf(c_0_103, negated_conjecture, ![X7:$i > $o]:(cwcel @ X7 @ cctop|(X7)!=(epred8_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_38]), c_0_90])])).
thf(c_0_104, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o, X12:$i > $o, X13:$i > $o, X14:$i > $o]:(cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ X7)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(ccfv @ X9 @ ccsigagen)|(X10)!=(epred7_0)|(X11)!=(epred2_0)|(X9)!=(epred8_0)|(X12)!=(epred4_0)|(X13)!=(epred14_0)|~cwcel @ X7 @ (ccdif @ (ccrn @ epred5_0) @ (ccsn @ X13))|~cwcel @ epred11_0 @ X14), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_40]), c_0_34]), c_0_35]), c_0_38]), c_0_37]), c_0_36]), c_0_39])])).
thf(c_0_105, negated_conjecture, ![X7:$i > $o]:((epred12_0)=(X7)|cwcel @ epred12_0 @ (ccdif @ (ccrn @ epred5_0) @ (ccsn @ X7))), inference(spm,[status(thm)],[c_0_92, c_0_82])).
thf(c_0_106, negated_conjecture, ![X7:$i > $o, X8:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred14_0)|(X8)!=(epred4_0)), inference(er,[status(thm)],[c_0_93])).
thf(c_0_107, negated_conjecture, cwcel @ epred12_0 @ (ccuni @ epred8_0), inference(spm,[status(thm)],[c_0_94, c_0_95])).
thf(c_0_108, plain, ![X7:$i > $o, X8:$i > $o, X9:$i > $o, X10:$i > $o]:(cwcel @ (ccima @ (cccnv @ X9) @ X7) @ X10|~cwcel @ X7 @ X8|~cwcel @ X9 @ (cco @ X10 @ X8 @ ccmbfm)|~cwcel @ X8 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X10 @ (ccuni @ (ccrn @ ccsiga))), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_96])])])).
thf(c_0_109, negated_conjecture, cwcel @ (ccdm @ epred9_0) @ (ccuni @ (ccrn @ ccsiga)), inference(spm,[status(thm)],[c_0_97, c_0_39])).
thf(c_0_110, negated_conjecture, ![X7:$i > $o]:(cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred4_0)), inference(er,[status(thm)],[c_0_98])).
thf(c_0_111, plain, ![X7:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X7 @ ccsigagen) @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X7 @ X8), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_99])])])).
thf(c_0_112, negated_conjecture, cwcel @ (ccsn @ epred13_0) @ (ccfv @ epred8_0 @ cccld), inference(spm,[status(thm)],[c_0_100, c_0_101])).
thf(c_0_113, plain, ![X7:$i > $o]:(cwss @ (ccfv @ X7 @ cccld) @ (ccfv @ X7 @ ccsigagen)|~cwcel @ X7 @ cctop), inference(split_conjunct,[status(thm)],[c_0_102])).
thf(c_0_114, negated_conjecture, cwcel @ epred8_0 @ cctop, inference(er,[status(thm)],[c_0_103])).
thf(c_0_115, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(ccfv @ X9 @ ccsigagen)|(X10)!=(epred7_0)|(X11)!=(epred2_0)|(X9)!=(epred8_0)|(X12)!=(epred4_0)|(X7)!=(epred14_0)|~cwcel @ epred11_0 @ X13), inference(spm,[status(thm)],[c_0_104, c_0_105])).
thf(c_0_116, plain, ![X232:$i > $o]:((~cwcel @ X232 @ (ccuni @ (ccrn @ ccmeas))|cwcel @ X232 @ (ccfv @ (ccdm @ X232) @ ccmeas))&(~cwcel @ X232 @ (ccfv @ (ccdm @ X232) @ ccmeas)|cwcel @ X232 @ (ccuni @ (ccrn @ ccmeas)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ameasbasedom_thm])])).
thf(c_0_117, negated_conjecture, ![X7:$i > $o]:(cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm)|(X7)!=(epred4_0)), inference(er,[status(thm)],[c_0_106])).
thf(c_0_118, negated_conjecture, cwcel @ (ccsn @ epred12_0) @ (ccfv @ epred8_0 @ cccld), inference(spm,[status(thm)],[c_0_100, c_0_107])).
thf(c_0_119, plain, ![X301:$i > $o, X302:$i > $o, X303:$i > $o]:(~cwcel @ X303 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X301 @ X303|~cwcel @ X302 @ X303|cwcel @ (ccin @ X301 @ X302) @ X303), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ainelsiga_thm])])).
thf(c_0_120, negated_conjecture, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwcel @ (ccima @ (cccnv @ X7) @ X8) @ (ccdm @ epred9_0)|~cwcel @ X7 @ (cco @ (ccdm @ epred9_0) @ X9 @ ccmbfm)|~cwcel @ X9 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X8 @ X9), inference(spm,[status(thm)],[c_0_108, c_0_109])).
thf(c_0_121, negated_conjecture, cwcel @ epred6_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm), inference(er,[status(thm)],[c_0_110])).
thf(c_0_122, negated_conjecture, cwcel @ epred3_0 @ (ccuni @ (ccrn @ ccsiga)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_72]), c_0_54])).
thf(c_0_123, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccsn @ epred13_0) @ X7|~cwss @ (ccfv @ epred8_0 @ cccld) @ X7), inference(spm,[status(thm)],[c_0_73, c_0_112])).
thf(c_0_124, negated_conjecture, cwss @ (ccfv @ epred8_0 @ cccld) @ epred3_0, inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_114]), c_0_54])).
thf(c_0_125, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred8_0)|(X11)!=(epred4_0)|(X7)!=(epred14_0)|~cwcel @ epred11_0 @ X12), inference(er,[status(thm)],[c_0_115])).
thf(c_0_126, plain, ![X324:$o, X325:$i > $o, X326:$i > $o, X327:$i > $o, X328:$i > $o]:(((((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|X324|X324)&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|X324|X324))&((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|X324|X324)&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|X324|X324)))&(((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|~cwcel @ X325 @ X327|X324)&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|~cwcel @ X325 @ X327|X324))&((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|~cwcel @ X325 @ X327|X324)&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|~cwcel @ X325 @ X327|X324))))&((((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|X324|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas))&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|X324|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas)))&((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|X324|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas))&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|X324|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas))))&(((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|~cwcel @ X325 @ X327|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas))&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|X324|~cwcel @ X325 @ X327|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas)))&((X324|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|~cwcel @ X325 @ X327|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas))&(~cwss @ X325 @ X326|(~X324|cwbr @ (ccfv @ X325 @ X328) @ (ccfv @ X326 @ X328) @ ccle)|~cwcel @ X326 @ X327|~cwcel @ X325 @ X327|~cwcel @ X328 @ (ccfv @ X327 @ ccmeas)))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ameasssd_thm])])])).
thf(c_0_127, plain, ![X7:$i > $o]:(cwcel @ X7 @ (ccfv @ (ccdm @ X7) @ ccmeas)|~cwcel @ X7 @ (ccuni @ (ccrn @ ccmeas))), inference(split_conjunct,[status(thm)],[c_0_116])).
thf(c_0_128, negated_conjecture, cwcel @ epred5_0 @ (cco @ (ccdm @ epred9_0) @ epred3_0 @ ccmbfm), inference(er,[status(thm)],[c_0_117])).
thf(c_0_129, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccsn @ epred12_0) @ X7|~cwss @ (ccfv @ epred8_0 @ cccld) @ X7), inference(spm,[status(thm)],[c_0_73, c_0_118])).
thf(c_0_130, plain, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:(cwcel @ (ccin @ X8 @ X9) @ X7|~cwcel @ X7 @ (ccuni @ (ccrn @ ccsiga))|~cwcel @ X8 @ X7|~cwcel @ X9 @ X7), inference(split_conjunct,[status(thm)],[c_0_119])).
thf(c_0_131, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccima @ (cccnv @ epred6_0) @ X7) @ (ccdm @ epred9_0)|~cwcel @ X7 @ epred3_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_121]), c_0_122])])).
thf(c_0_132, negated_conjecture, cwcel @ (ccsn @ epred13_0) @ epred3_0, inference(spm,[status(thm)],[c_0_123, c_0_124])).
thf(c_0_133, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred8_0)|(X11)!=(epred4_0)|(X7)!=(epred14_0)), inference(spm,[status(thm)],[c_0_125, c_0_45])).
thf(c_0_134, plain, ![X8:$i > $o, X7:$i > $o, X9:$i > $o, X10:$i > $o]:(cwbr @ (ccfv @ X7 @ X9) @ (ccfv @ X8 @ X9) @ ccle|~cwss @ X7 @ X8|~cwcel @ X8 @ X10|~cwcel @ X7 @ X10|~cwcel @ X9 @ (ccfv @ X10 @ ccmeas)), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_126])])])).
thf(c_0_135, negated_conjecture, cwcel @ epred9_0 @ (ccfv @ (ccdm @ epred9_0) @ ccmeas), inference(spm,[status(thm)],[c_0_127, c_0_39])).
thf(c_0_136, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccima @ (cccnv @ epred5_0) @ X7) @ (ccdm @ epred9_0)|~cwcel @ X7 @ epred3_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_128]), c_0_122])])).
thf(c_0_137, negated_conjecture, cwcel @ (ccsn @ epred12_0) @ epred3_0, inference(spm,[status(thm)],[c_0_129, c_0_124])).
thf(c_0_138, plain, ![X304:$i > $o, X305:$i > $o, X306:$i > $o]:(~cwcel @ X306 @ (ccfv @ X305 @ ccmeas)|~cwcel @ X304 @ X305|cwcel @ (ccfv @ X304 @ X306) @ (cco @ ccc0 @ ccpnf @ ccicc)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ameasvxrge0_thm])])).
thf(c_0_139, negated_conjecture, ![X8:$i > $o, X7:$i > $o]:(cwcel @ (ccin @ X7 @ X8) @ (ccdm @ epred9_0)|~cwcel @ X8 @ (ccdm @ epred9_0)|~cwcel @ X7 @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_130, c_0_109])).
thf(c_0_140, negated_conjecture, cwcel @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ (ccdm @ epred9_0), inference(spm,[status(thm)],[c_0_131, c_0_132])).
thf(c_0_141, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred2_0)|(X9)!=(epred8_0)|(X10)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_133])).
thf(c_0_142, negated_conjecture, ![X7:$i > $o, X8:$i > $o]:(cwbr @ (ccfv @ X7 @ epred9_0) @ (ccfv @ X8 @ epred9_0) @ ccle|~cwcel @ X8 @ (ccdm @ epred9_0)|~cwcel @ X7 @ (ccdm @ epred9_0)|~cwss @ X7 @ X8), inference(spm,[status(thm)],[c_0_134, c_0_135])).
thf(c_0_143, negated_conjecture, cwcel @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccdm @ epred9_0), inference(spm,[status(thm)],[c_0_136, c_0_137])).
thf(c_0_144, plain, ![X329:$i > $o, X330:$i > $o]:cwss @ (ccin @ X329 @ X330) @ X329, inference(variable_rename,[status(thm)],[ainss1_thm])).
thf(c_0_145, plain, ![X7:$i > $o, X9:$i > $o, X8:$i > $o]:(cwcel @ (ccfv @ X9 @ X7) @ (cco @ ccc0 @ ccpnf @ ccicc)|~cwcel @ X7 @ (ccfv @ X8 @ ccmeas)|~cwcel @ X9 @ X8), inference(split_conjunct,[status(thm)],[c_0_138])).
thf(c_0_146, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccin @ X7 @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ (ccdm @ epred9_0)|~cwcel @ X7 @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_139, c_0_140])).
thf(c_0_147, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred8_0)|(X9)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_141])).
thf(c_0_148, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ X7 @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ ccle|~cwss @ X7 @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0))|~cwcel @ X7 @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_142, c_0_143])).
thf(c_0_149, plain, ![X8:$i > $o, X7:$i > $o]:cwss @ (ccin @ X7 @ X8) @ X7, inference(split_conjunct,[status(thm)],[c_0_144])).
thf(c_0_150, plain, ![X310:$i > $o]:(((cwcel @ X310 @ ccxr|~cwcel @ X310 @ (cco @ ccc0 @ ccpnf @ ccicc))&(cwbr @ ccc0 @ X310 @ ccle|~cwcel @ X310 @ (cco @ ccc0 @ ccpnf @ ccicc)))&(~cwcel @ X310 @ ccxr|~cwbr @ ccc0 @ X310 @ ccle|cwcel @ X310 @ (cco @ ccc0 @ ccpnf @ ccicc))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aelxrge0_thm])])])).
thf(c_0_151, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccfv @ X7 @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccicc)|~cwcel @ X7 @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_145, c_0_135])).
thf(c_0_152, negated_conjecture, cwcel @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ (ccdm @ epred9_0), inference(spm,[status(thm)],[c_0_146, c_0_143])).
thf(c_0_153, negated_conjecture, ![X8:$i > $o, X7:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_147])).
thf(c_0_154, plain, ![X320:$o, X321:$i > $o, X322:$i > $o, X323:$i > $o]:((((((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|X320|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|X320|X320))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|X320|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|X320|X320)))&(((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|X320|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|X320|X320))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|X320|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|X320|X320))))&((((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|~cwcel @ X322 @ ccxr|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|~cwcel @ X322 @ ccxr|X320))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|~cwcel @ X322 @ ccxr|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|~cwcel @ X322 @ ccxr|X320)))&(((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|X320))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|X320)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|X320)))))&(((((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|X320|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|X320|~cwcel @ X321 @ ccxr))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|X320|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|X320|~cwcel @ X321 @ ccxr)))&(((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|X320|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|X320|~cwcel @ X321 @ ccxr))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|X320|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|X320|~cwcel @ X321 @ ccxr))))&((((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|X320|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|X320|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)))&(((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|X320|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr))&((X320|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)&(~cwbr @ X322 @ X323 @ cclt|(~X320|cwbr @ X321 @ X323 @ cclt)|~cwbr @ X321 @ X322 @ ccle|~cwcel @ X323 @ ccxr|~cwcel @ X322 @ ccxr|~cwcel @ X321 @ ccxr)))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axrlelttrd_thm])])])).
thf(c_0_155, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ X7) @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ ccle|~cwcel @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ X7) @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_148, c_0_149])).
thf(c_0_156, plain, ![X7:$i > $o]:(cwcel @ X7 @ ccxr|~cwcel @ X7 @ (cco @ ccc0 @ ccpnf @ ccicc)), inference(split_conjunct,[status(thm)],[c_0_150])).
thf(c_0_157, negated_conjecture, cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccicc), inference(spm,[status(thm)],[c_0_151, c_0_152])).
thf(c_0_158, negated_conjecture, cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccicc), inference(spm,[status(thm)],[c_0_151, c_0_143])).
thf(c_0_159, plain, ![X363:$i > $o, X364:$i > $o, X365:$i > $o]:((((cwcel @ X365 @ ccr|~cwcel @ X365 @ (cco @ X363 @ X364 @ ccico)|(~cwcel @ X363 @ ccr|~cwcel @ X364 @ ccxr))&(cwbr @ X363 @ X365 @ ccle|~cwcel @ X365 @ (cco @ X363 @ X364 @ ccico)|(~cwcel @ X363 @ ccr|~cwcel @ X364 @ ccxr)))&(cwbr @ X365 @ X364 @ cclt|~cwcel @ X365 @ (cco @ X363 @ X364 @ ccico)|(~cwcel @ X363 @ ccr|~cwcel @ X364 @ ccxr)))&(~cwcel @ X365 @ ccr|~cwbr @ X363 @ X365 @ ccle|~cwbr @ X365 @ X364 @ cclt|cwcel @ X365 @ (cco @ X363 @ X364 @ ccico)|(~cwcel @ X363 @ ccr|~cwcel @ X364 @ ccxr))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aelico2_thm])])])).
thf(c_0_160, negated_conjecture, ![X7:$i > $o]:((epred12_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_153])).
thf(c_0_161, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o, X12:$i > $o, X13:$i > $o, X14:$i > $o]:(cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ X7)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(ccfv @ X9 @ ccsigagen)|(X10)!=(epred7_0)|(X11)!=(epred2_0)|(X9)!=(epred8_0)|(X12)!=(epred4_0)|(X13)!=(epred14_0)|~cwcel @ X7 @ (ccdif @ (ccrn @ epred6_0) @ (ccsn @ X13))|~cwcel @ epred11_0 @ X14), 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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_33]), c_0_34]), c_0_35]), c_0_38]), c_0_37]), c_0_36]), c_0_39])])).
thf(c_0_162, negated_conjecture, ![X7:$i > $o]:((epred13_0)=(X7)|cwcel @ epred13_0 @ (ccdif @ (ccrn @ epred6_0) @ (ccsn @ X7))), inference(spm,[status(thm)],[c_0_92, c_0_74])).
thf(c_0_163, plain, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwbr @ X9 @ X8 @ cclt|~cwbr @ X7 @ X8 @ cclt|~cwbr @ X9 @ X7 @ ccle|~cwcel @ X8 @ ccxr|~cwcel @ X7 @ ccxr|~cwcel @ X9 @ ccxr), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_154])])])).
thf(c_0_164, negated_conjecture, cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_155, c_0_152])).
thf(c_0_165, negated_conjecture, cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_156, c_0_157])).
thf(c_0_166, negated_conjecture, cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_156, c_0_158])).
thf(c_0_167, plain, ![X7:$i > $o, X9:$i > $o, X8:$i > $o]:(cwbr @ X7 @ X8 @ cclt|~cwcel @ X7 @ (cco @ X9 @ X8 @ ccico)|~cwcel @ X9 @ ccr|~cwcel @ X8 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_159])).
thf(c_0_168, negated_conjecture, ((epred12_0)=(epred14_0)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)), inference(er,[status(thm)],[c_0_160])).
thf(c_0_169, plain, cwcel @ ccc0 @ ccr, inference(split_conjunct,[status(thm)],[a_0re_thm])).
thf(c_0_170, plain, cwcel @ ccpnf @ ccxr, inference(split_conjunct,[status(thm)],[apnfxr_thm])).
thf(c_0_171, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o, X11:$i > $o, X12:$i > $o, X13:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(ccfv @ X9 @ ccsigagen)|(X10)!=(epred7_0)|(X11)!=(epred2_0)|(X9)!=(epred8_0)|(X12)!=(epred4_0)|(X7)!=(epred14_0)|~cwcel @ epred11_0 @ X13), inference(spm,[status(thm)],[c_0_161, c_0_162])).
thf(c_0_172, plain, ![X368:$i > $o, X369:$i > $o]:(~cwcel @ X368 @ ccxr|~cwcel @ X369 @ ccr|(~cwbr @ X369 @ X368 @ ccle|~cwbr @ X368 @ ccpnf @ cclt)|cwcel @ X368 @ ccr), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axrre3_thm])])).
thf(c_0_173, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwbr @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ X7 @ cclt|~cwcel @ X7 @ ccxr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163, c_0_164]), c_0_165]), c_0_166])])).
thf(c_0_174, negated_conjecture, ((epred12_0)=(epred14_0)|cwbr @ (ccfv @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ epred9_0) @ ccpnf @ cclt), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167, c_0_168]), c_0_169]), c_0_170])])).
thf(c_0_175, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o, X10:$i > $o, X11:$i > $o, X12:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred8_0)|(X11)!=(epred4_0)|(X7)!=(epred14_0)|~cwcel @ epred11_0 @ X12), inference(er,[status(thm)],[c_0_171])).
thf(c_0_176, plain, ![X7:$i > $o]:(cwbr @ ccc0 @ X7 @ ccle|~cwcel @ X7 @ (cco @ ccc0 @ ccpnf @ ccicc)), inference(split_conjunct,[status(thm)],[c_0_150])).
thf(c_0_177, plain, ![X8:$i > $o, X7:$i > $o]:(cwcel @ X7 @ ccr|~cwcel @ X7 @ ccxr|~cwcel @ X8 @ ccr|~cwbr @ X8 @ X7 @ ccle|~cwbr @ X7 @ ccpnf @ cclt), inference(split_conjunct,[status(thm)],[c_0_172])).
thf(c_0_178, negated_conjecture, ((epred12_0)=(epred14_0)|cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccpnf @ cclt), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173, c_0_174]), c_0_170])])).
thf(c_0_179, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X11:$i > $o, X10:$i > $o, X7:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred7_0)|(X9)!=(epred2_0)|(X10)!=(epred8_0)|(X11)!=(epred4_0)|(X7)!=(epred14_0)), inference(spm,[status(thm)],[c_0_175, c_0_45])).
thf(c_0_180, plain, ![X7:$i > $o, X8:$i > $o, X9:$i > $o]:(cwcel @ X7 @ (cco @ X8 @ X9 @ ccico)|~cwcel @ X7 @ ccr|~cwbr @ X8 @ X7 @ ccle|~cwbr @ X7 @ X9 @ cclt|~cwcel @ X8 @ ccr|~cwcel @ X9 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_159])).
thf(c_0_181, negated_conjecture, cwbr @ ccc0 @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_176, c_0_157])).
thf(c_0_182, negated_conjecture, ![X7:$i > $o]:((epred12_0)=(epred14_0)|cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr|~cwbr @ X7 @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccle|~cwcel @ X7 @ ccr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177, c_0_178]), c_0_165])])).
thf(c_0_183, negated_conjecture, ![X8:$i > $o, X10:$i > $o, X9:$i > $o, X7:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred2_0)|(X9)!=(epred8_0)|(X10)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_179])).
thf(c_0_184, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ X7 @ ccico)|~cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr|~cwcel @ X7 @ ccxr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180, c_0_181]), c_0_169])])).
thf(c_0_185, negated_conjecture, ((epred12_0)=(epred14_0)|cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_182, c_0_181]), c_0_169])])).
thf(c_0_186, negated_conjecture, ![X9:$i > $o, X8:$i > $o, X7:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred8_0)|(X9)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_183])).
thf(c_0_187, plain, ![X366:$i > $o, X367:$i > $o]:cwss @ (ccin @ X366 @ X367) @ X367, inference(variable_rename,[status(thm)],[ainss2_thm])).
thf(c_0_188, negated_conjecture, ![X7:$i > $o]:((epred12_0)=(epred14_0)|cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ X7 @ ccico)|~cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwcel @ X7 @ ccxr), inference(spm,[status(thm)],[c_0_184, c_0_185])).
thf(c_0_189, negated_conjecture, ~cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred12_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_190, negated_conjecture, ![X8:$i > $o, X7:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X8)!=(epred4_0)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_186])).
thf(c_0_191, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ X7 @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccle|~cwss @ X7 @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))|~cwcel @ X7 @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_142, c_0_140])).
thf(c_0_192, plain, ![X7:$i > $o, X8:$i > $o]:cwss @ (ccin @ X7 @ X8) @ X8, inference(split_conjunct,[status(thm)],[c_0_187])).
thf(c_0_193, negated_conjecture, (epred12_0)=(epred14_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188, c_0_178]), c_0_170])]), c_0_189])).
thf(c_0_194, negated_conjecture, ![X7:$i > $o]:((epred13_0)=(X7)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)|(X7)!=(epred14_0)), inference(er,[status(thm)],[c_0_190])).
thf(c_0_195, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ (ccin @ X7 @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccle|~cwcel @ (ccin @ X7 @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ (ccdm @ epred9_0)), inference(spm,[status(thm)],[c_0_191, c_0_192])).
thf(c_0_196, negated_conjecture, cwcel @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ (ccdm @ epred9_0), inference(rw,[status(thm)],[c_0_152, c_0_193])).
thf(c_0_197, negated_conjecture, cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccicc), inference(spm,[status(thm)],[c_0_151, c_0_140])).
thf(c_0_198, negated_conjecture, ((epred13_0)=(epred14_0)|cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico)), inference(er,[status(thm)],[c_0_194])).
thf(c_0_199, negated_conjecture, ((epred12_0)!=(epred14_0)|(epred13_0)!=(epred14_0)), inference(split_conjunct,[status(thm)],[c_0_26])).
thf(c_0_200, negated_conjecture, cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_195, c_0_196])).
thf(c_0_201, negated_conjecture, cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccxr, inference(rw,[status(thm)],[c_0_165, c_0_193])).
thf(c_0_202, negated_conjecture, cwcel @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_156, c_0_197])).
thf(c_0_203, negated_conjecture, ((epred13_0)=(epred14_0)|cwbr @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccpnf @ cclt), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167, c_0_198]), c_0_169]), c_0_170])])).
thf(c_0_204, negated_conjecture, (epred13_0)!=(epred14_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_199, c_0_193])])).
thf(c_0_205, negated_conjecture, ![X7:$i > $o]:(cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwbr @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ X7 @ cclt|~cwcel @ X7 @ ccxr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163, c_0_200]), c_0_201]), c_0_202])])).
thf(c_0_206, negated_conjecture, cwbr @ (ccfv @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0)) @ epred9_0) @ ccpnf @ cclt, inference(sr,[status(thm)],[c_0_203, c_0_204])).
thf(c_0_207, negated_conjecture, cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccpnf @ cclt, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205, c_0_206]), c_0_170])])).
thf(c_0_208, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr|~cwbr @ X7 @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccle|~cwcel @ X7 @ ccr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177, c_0_207]), c_0_201])])).
thf(c_0_209, negated_conjecture, cwbr @ ccc0 @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccle, inference(rw,[status(thm)],[c_0_181, c_0_193])).
thf(c_0_210, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ X7 @ ccico)|~cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr|~cwcel @ X7 @ ccxr), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_184, c_0_193]), c_0_193]), c_0_193])).
thf(c_0_211, negated_conjecture, cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ ccr, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_208, c_0_209]), c_0_169])])).
thf(c_0_212, negated_conjecture, ![X7:$i > $o]:(cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ X7 @ ccico)|~cwbr @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ X7 @ cclt|~cwcel @ X7 @ ccxr), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210, c_0_211])])).
thf(c_0_213, negated_conjecture, ~cwcel @ (ccfv @ (ccin @ (ccima @ (cccnv @ epred5_0) @ (ccsn @ epred14_0)) @ (ccima @ (cccnv @ epred6_0) @ (ccsn @ epred13_0))) @ epred9_0) @ (cco @ ccc0 @ ccpnf @ ccico), inference(rw,[status(thm)],[c_0_189, c_0_193])).
thf(c_0_214, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_212, c_0_207]), c_0_170])]), c_0_213]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 215
# Proof object clause steps            : 166
# Proof object formula steps           : 49
# Proof object conjectures             : 143
# Proof object clause conjectures      : 140
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 43
# Proof object initial formulas used   : 25
# Proof object generating inferences   : 109
# Proof object simplifying inferences  : 114
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 106
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 417
# Removed in clause preprocessing      : 368
# Initial clauses in saturation        : 49
# Processed clauses                    : 12006
# ...of these trivial                  : 130
# ...subsumed                          : 2474
# ...remaining for further processing  : 9402
# Other redundant clauses eliminated   : 1
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 62
# Backward-rewritten                   : 668
# Generated clauses                    : 120143
# ...of the previous two non-trivial   : 120312
# Contextual simplify-reflections      : 0
# Paramodulations                      : 112637
# Factorizations                       : 0
# NegExts                              : 0
# Equation resolutions                 : 49
# 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  : 6281
#    Positive orientable unit clauses  : 764
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 3
#    Non-unit-clauses                  : 5514
# Current number of unprocessed clauses: 105215
# ...number of literals in the above   : 110413
# Current number of archived formulas  : 0
# Current number of archived clauses   : 3120
# Clause-clause subsumption calls (NU) : 6657494
# Rec. Clause-clause subsumption calls : 1083793
# Non-unit clause-clause subsumptions  : 2534
# Unit Clause-clause subsumption calls : 177692
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 25459
# BW rewrite match successes           : 15
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 4256811

# -------------------------------------------------
# User time                : 4.107 s
# System time              : 0.084 s
# Total time               : 4.191 s
# Maximum resident set size: 102704 pages
