# Preprocessing time       : 0.029 s

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
thf(cisxmet2d_conj, conjecture, ![X1:$o, X2:$i > $o, X3:$i > $o]:((X1=>cwcel @ X3 @ ccvv)=>((X1=>cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2)=>(![X4:$i, X5:$i]:((X1&(cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3))=>cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ ccle)=>(![X4:$i, X5:$i]:((X1&(cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3))=>(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ ccc0 @ ccle<=>(ccv @ X4)=(ccv @ X5)))=>(![X4:$i, X5:$i, X6:$i]:(((X1&((cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3)&cwcel @ (ccv @ X6) @ X3))&(cwcel @ (cco @ (ccv @ X6) @ (ccv @ X4) @ X2) @ ccr&cwcel @ (cco @ (ccv @ X6) @ (ccv @ X5) @ X2) @ ccr))=>cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ (cco @ (cco @ (ccv @ X6) @ (ccv @ X4) @ X2) @ (cco @ (ccv @ X6) @ (ccv @ X5) @ X2) @ ccaddc) @ ccle)=>(X1=>cwcel @ X2 @ (ccfv @ X3 @ ccxmt))))))), file('mmset22449_isxmet2d.p', cisxmet2d_conj)).
thf(aisxmetd_thm, axiom, ![X1:$o, X2:$i > $o, X3:$i > $o]:((X1=>cwcel @ X3 @ ccvv)=>((X1=>cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2)=>(![X4:$i, X5:$i]:((X1&(cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3))=>((cco @ (ccv @ X4) @ (ccv @ X5) @ X2)=(ccc0)<=>(ccv @ X4)=(ccv @ X5)))=>(![X4:$i, X5:$i, X6:$i]:((X1&((cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3)&cwcel @ (ccv @ X6) @ X3))=>cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ (cco @ (cco @ (ccv @ X6) @ (ccv @ X4) @ X2) @ (cco @ (ccv @ X6) @ (ccv @ X5) @ X2) @ ccxad) @ ccle)=>(X1=>cwcel @ X2 @ (ccfv @ X3 @ ccxmt)))))), file('mmset22449_isxmet2d.p', aisxmetd_thm)).
thf(axrletri3_thm, axiom, ![X11:$i > $o, X12:$i > $o]:((cwcel @ X11 @ ccxr&cwcel @ X12 @ ccxr)=>((X11)=(X12)<=>(cwbr @ X11 @ X12 @ ccle&cwbr @ X12 @ X11 @ ccle))), file('mmset22449_isxmet2d.p', axrletri3_thm)).
thf(afovrnda_thm, axiom, ![X1:$o, X11:$i > $o, X12:$i > $o, X13:$i > $o, X14:$i > $o, X15:$i > $o, X16:$i > $o]:((X1=>cwf @ (ccxp @ X14 @ X15) @ X13 @ X16)=>((X1&(cwcel @ X11 @ X14&cwcel @ X12 @ X15))=>cwcel @ (cco @ X11 @ X12 @ X16) @ X13)), file('mmset22449_isxmet2d.p', afovrnda_thm)).
thf(a_0xr_thm, axiom, cwcel @ ccc0 @ ccxr, file('mmset22449_isxmet2d.p', a_0xr_thm)).
thf(age0nemnf_thm, axiom, ![X11:$i > $o]:((cwcel @ X11 @ ccxr&cwbr @ ccc0 @ X11 @ ccle)=>(X11)!=(ccmnf)), file('mmset22449_isxmet2d.p', age0nemnf_thm)).
thf(aelxr_thm, axiom, ![X11:$i > $o]:(cwcel @ X11 @ ccxr<=>(cwcel @ X11 @ ccr|(X11)=(ccpnf)|(X11)=(ccmnf))), file('mmset22449_isxmet2d.p', aelxr_thm)).
thf(arexadd_thm, axiom, ![X11:$i > $o, X12:$i > $o]:((cwcel @ X11 @ ccr&cwcel @ X12 @ ccr)=>(cco @ X11 @ X12 @ ccxad)=(cco @ X11 @ X12 @ ccaddc)), file('mmset22449_isxmet2d.p', arexadd_thm)).
thf(axaddpnf1_thm, axiom, ![X11:$i > $o]:((cwcel @ X11 @ ccxr&(X11)!=(ccmnf))=>(cco @ X11 @ ccpnf @ ccxad)=(ccpnf)), file('mmset22449_isxmet2d.p', axaddpnf1_thm)).
thf(apnfge_thm, axiom, ![X11:$i > $o]:(cwcel @ X11 @ ccxr=>cwbr @ X11 @ ccpnf @ ccle), file('mmset22449_isxmet2d.p', apnfge_thm)).
thf(axaddpnf2_thm, axiom, ![X11:$i > $o]:((cwcel @ X11 @ ccxr&(X11)!=(ccmnf))=>(cco @ ccpnf @ X11 @ ccxad)=(ccpnf)), file('mmset22449_isxmet2d.p', axaddpnf2_thm)).
thf(c_0_11, negated_conjecture, ~(![X1:$o, X2:$i > $o, X3:$i > $o]:((X1=>cwcel @ X3 @ ccvv)=>((X1=>cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2)=>(![X4:$i, X5:$i]:((X1&(cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3))=>cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ ccle)=>(![X4:$i, X5:$i]:((X1&(cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3))=>(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ ccc0 @ ccle<=>(ccv @ X4)=(ccv @ X5)))=>(![X4:$i, X5:$i, X6:$i]:(((X1&((cwcel @ (ccv @ X4) @ X3&cwcel @ (ccv @ X5) @ X3)&cwcel @ (ccv @ X6) @ X3))&(cwcel @ (cco @ (ccv @ X6) @ (ccv @ X4) @ X2) @ ccr&cwcel @ (cco @ (ccv @ X6) @ (ccv @ X5) @ X2) @ ccr))=>cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ X2) @ (cco @ (cco @ (ccv @ X6) @ (ccv @ X4) @ X2) @ (cco @ (ccv @ X6) @ (ccv @ X5) @ X2) @ ccaddc) @ ccle)=>(X1=>cwcel @ X2 @ (ccfv @ X3 @ ccxmt)))))))), inference(assume_negation,[status(cth)],[cisxmet2d_conj])).
thf(c_0_12, negated_conjecture, ![X331:$i, X332:$i, X333:$i, X334:$i, X335:$i, X336:$i, X337:$i]:((~epred8_0|cwcel @ epred10_0 @ ccvv)&((~epred8_0|cwf @ (ccxp @ epred10_0 @ epred10_0) @ ccxr @ epred9_0)&((~epred8_0|(~cwcel @ (ccv @ X331) @ epred10_0|~cwcel @ (ccv @ X332) @ epred10_0)|cwbr @ ccc0 @ (cco @ (ccv @ X331) @ (ccv @ X332) @ epred9_0) @ ccle)&(((~cwbr @ (cco @ (ccv @ X333) @ (ccv @ X334) @ epred9_0) @ ccc0 @ ccle|(ccv @ X333)=(ccv @ X334)|(~epred8_0|(~cwcel @ (ccv @ X333) @ epred10_0|~cwcel @ (ccv @ X334) @ epred10_0)))&((ccv @ X333)!=(ccv @ X334)|cwbr @ (cco @ (ccv @ X333) @ (ccv @ X334) @ epred9_0) @ ccc0 @ ccle|(~epred8_0|(~cwcel @ (ccv @ X333) @ epred10_0|~cwcel @ (ccv @ X334) @ epred10_0))))&((~epred8_0|(~cwcel @ (ccv @ X335) @ epred10_0|~cwcel @ (ccv @ X336) @ epred10_0|~cwcel @ (ccv @ X337) @ epred10_0)|(~cwcel @ (cco @ (ccv @ X337) @ (ccv @ X335) @ epred9_0) @ ccr|~cwcel @ (cco @ (ccv @ X337) @ (ccv @ X336) @ epred9_0) @ ccr)|cwbr @ (cco @ (ccv @ X335) @ (ccv @ X336) @ epred9_0) @ (cco @ (cco @ (ccv @ X337) @ (ccv @ X335) @ epred9_0) @ (cco @ (ccv @ X337) @ (ccv @ X336) @ epred9_0) @ ccaddc) @ ccle)&(epred8_0&~cwcel @ epred9_0 @ (ccfv @ epred10_0 @ ccxmt))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])])])).
thf(c_0_13, plain, ![X181:$o, X182:$i > $o, X183:$i > $o]:(((((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|X181))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|X181))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|X181))))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|X181))))&(((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|X181)))))&((((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|X181|~cwcel @ X183 @ ccvv))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|X181|~cwcel @ X183 @ ccvv))))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|X181|~cwcel @ X183 @ ccvv))))&(((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|X181|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|cwcel @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X183|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))))&((((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)!=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))!=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(((X181|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(((cwcel @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)&(cwcel @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv))&(cwcel @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ X183|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))&(~cwbr @ (cco @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk3_3 @ X181 @ X182 @ X183)) @ X182) @ (cco @ (ccv @ (esk5_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk4_3 @ X181 @ X182 @ X183)) @ X182) @ ccxad) @ ccle|(~X181|cwcel @ X182 @ (ccfv @ X183 @ ccxmt))|((cco @ (ccv @ (esk1_3 @ X181 @ X182 @ X183)) @ (ccv @ (esk2_3 @ X181 @ X182 @ X183)) @ X182)=(ccc0)|(ccv @ (esk1_3 @ X181 @ X182 @ X183))=(ccv @ (esk2_3 @ X181 @ X182 @ X183)))|~cwf @ (ccxp @ X183 @ X183) @ ccxr @ X182|~cwcel @ X183 @ ccvv)))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aisxmetd_thm])])])])).
thf(c_0_14, negated_conjecture, (cwf @ (ccxp @ epred10_0 @ epred10_0) @ ccxr @ epred9_0|~epred8_0), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_15, negated_conjecture, epred8_0, inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_16, negated_conjecture, (cwcel @ epred10_0 @ ccvv|~epred8_0), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_17, plain, ![X205:$i > $o, X206:$i > $o]:(((cwbr @ X205 @ X206 @ ccle|(X205)!=(X206)|(~cwcel @ X205 @ ccxr|~cwcel @ X206 @ ccxr))&(cwbr @ X206 @ X205 @ ccle|(X205)!=(X206)|(~cwcel @ X205 @ ccxr|~cwcel @ X206 @ ccxr)))&(~cwbr @ X205 @ X206 @ ccle|~cwbr @ X206 @ X205 @ ccle|(X205)=(X206)|(~cwcel @ X205 @ ccxr|~cwcel @ X206 @ ccxr))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axrletri3_thm])])])).
thf(c_0_18, plain, ![X198:$o, X199:$i > $o, X200:$i > $o, X201:$i > $o, X202:$i > $o, X203:$i > $o, X204:$i > $o]:((X198|(~X198|(~cwcel @ X199 @ X202|~cwcel @ X200 @ X203)|cwcel @ (cco @ X199 @ X200 @ X204) @ X201))&(~cwf @ (ccxp @ X202 @ X203) @ X201 @ X204|(~X198|(~cwcel @ X199 @ X202|~cwcel @ X200 @ X203)|cwcel @ (cco @ X199 @ X200 @ X204) @ X201))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[afovrnda_thm])])])).
thf(c_0_19, negated_conjecture, ![X4:$i, X5:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccle|~epred8_0|~cwcel @ (ccv @ X4) @ epred10_0|~cwcel @ (ccv @ X5) @ epred10_0), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_20, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_21, negated_conjecture, cwf @ (ccxp @ epred10_0 @ epred10_0) @ ccxr @ epred9_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
thf(c_0_22, negated_conjecture, cwcel @ epred10_0 @ ccvv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_15])])).
thf(c_0_23, negated_conjecture, ~cwcel @ epred9_0 @ (ccfv @ epred10_0 @ ccxmt), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_24, plain, ![X3:$i > $o, X2:$i > $o]:(cwbr @ X2 @ X3 @ ccle|(X3)!=(X2)|~cwcel @ X3 @ ccxr|~cwcel @ X2 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_25, plain, ![X2:$i > $o, X11:$i > $o, X13:$i > $o, X14:$i > $o, X12:$i > $o, X3:$i > $o]:(cwcel @ (cco @ X13 @ X14 @ X12) @ X11|~cwf @ (ccxp @ X2 @ X3) @ X11 @ X12|~cwcel @ X13 @ X2|~cwcel @ X14 @ X3), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_18])])])).
thf(c_0_26, negated_conjecture, ![X5:$i, X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccle|~cwcel @ (ccv @ X5) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_15])])).
thf(c_0_27, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_28, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_29, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_30, negated_conjecture, ![X4:$i, X5:$i]:((ccv @ X4)=(ccv @ X5)|~cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccc0 @ ccle|~epred8_0|~cwcel @ (ccv @ X4) @ epred10_0|~cwcel @ (ccv @ X5) @ epred10_0), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_31, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_32, plain, ![X2:$i > $o]:(cwbr @ X2 @ X2 @ ccle|~cwcel @ X2 @ ccxr), inference(er,[status(thm)],[c_0_24])).
thf(c_0_33, plain, cwcel @ ccc0 @ ccxr, inference(split_conjunct,[status(thm)],[a_0xr_thm])).
thf(c_0_34, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_35, negated_conjecture, ![X3:$i > $o, X2:$i > $o]:(cwcel @ (cco @ X2 @ X3 @ epred9_0) @ ccxr|~cwcel @ X3 @ epred10_0|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_25, c_0_21])).
thf(c_0_36, plain, ![X318:$i > $o]:(~cwcel @ X318 @ ccxr|~cwbr @ ccc0 @ X318 @ ccle|(X318)!=(ccmnf)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[age0nemnf_thm])])).
thf(c_0_37, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_27])).
thf(c_0_38, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_39, plain, ![X322:$i > $o]:((~cwcel @ X322 @ ccxr|(cwcel @ X322 @ ccr|(X322)=(ccpnf)|(X322)=(ccmnf)))&(((~cwcel @ X322 @ ccr|cwcel @ X322 @ ccxr)&((X322)!=(ccpnf)|cwcel @ X322 @ ccxr))&((X322)!=(ccmnf)|cwcel @ X322 @ ccxr))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[aelxr_thm])])])).
thf(c_0_40, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_41, negated_conjecture, ![X5:$i, X4:$i]:((ccv @ X4)=(ccv @ X5)|~cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccc0 @ ccle|~cwcel @ (ccv @ X5) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_15])])).
thf(c_0_42, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_43, plain, cwbr @ ccc0 @ ccc0 @ ccle, inference(spm,[status(thm)],[c_0_32, c_0_33])).
thf(c_0_44, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_45, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_46, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_47, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_48, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X3|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_49, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_27])).
thf(c_0_50, plain, ![X2:$i > $o]:(~cwcel @ X2 @ ccxr|~cwbr @ ccc0 @ X2 @ ccle|(X2)!=(ccmnf)), inference(split_conjunct,[status(thm)],[c_0_36])).
thf(c_0_51, negated_conjecture, (cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_37, c_0_38])).
thf(c_0_52, plain, ![X2:$i > $o]:(cwcel @ X2 @ ccxr|(X2)!=(ccmnf)), inference(split_conjunct,[status(thm)],[c_0_39])).
thf(c_0_53, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_40])).
thf(c_0_54, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])]), c_0_27]), c_0_44])).
thf(c_0_55, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_56, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_57, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_58, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|cwcel @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_59, negated_conjecture, ![X4:$i, X6:$i, X5:$i]:(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ (cco @ (cco @ (ccv @ X6) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ X6) @ (ccv @ X5) @ epred9_0) @ ccaddc) @ ccle|~epred8_0|~cwcel @ (ccv @ X4) @ epred10_0|~cwcel @ (ccv @ X5) @ epred10_0|~cwcel @ (ccv @ X6) @ epred10_0|~cwcel @ (cco @ (ccv @ X6) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (cco @ (ccv @ X6) @ (ccv @ X5) @ epred9_0) @ ccr), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_60, plain, ![X2:$i > $o]:(cwcel @ X2 @ ccr|(X2)=(ccpnf)|(X2)=(ccmnf)|~cwcel @ X2 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_39])).
thf(c_0_61, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_49, c_0_38])).
thf(c_0_62, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_52])).
thf(c_0_63, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_40])).
thf(c_0_64, negated_conjecture, (cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_53, c_0_38])).
thf(c_0_65, plain, ![X227:$i > $o, X228:$i > $o]:(~cwcel @ X227 @ ccr|~cwcel @ X228 @ ccr|(cco @ X227 @ X228 @ ccxad)=(cco @ X227 @ X228 @ ccaddc)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arexadd_thm])])).
thf(c_0_66, negated_conjecture, ![X4:$i]:((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_54])).
thf(c_0_67, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_55]), c_0_43])]), c_0_38]), c_0_56])).
thf(c_0_68, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_57]), c_0_43])]), c_0_40]), c_0_58])).
thf(c_0_69, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_44])).
thf(c_0_70, negated_conjecture, ![X6:$i, X5:$i, X4:$i]:(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ (cco @ (cco @ (ccv @ X6) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ X6) @ (ccv @ X5) @ epred9_0) @ ccaddc) @ ccle|~cwcel @ (cco @ (ccv @ X6) @ (ccv @ X5) @ epred9_0) @ ccr|~cwcel @ (cco @ (ccv @ X6) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (ccv @ X6) @ epred10_0|~cwcel @ (ccv @ X5) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_15])])).
thf(c_0_71, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_62])).
thf(c_0_72, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_63, c_0_38])).
thf(c_0_73, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_64]), c_0_52])).
thf(c_0_74, plain, ![X2:$i > $o, X3:$i > $o]:((cco @ X2 @ X3 @ ccxad)=(cco @ X2 @ X3 @ ccaddc)|~cwcel @ X2 @ ccr|~cwcel @ X3 @ ccr), inference(split_conjunct,[status(thm)],[c_0_65])).
thf(c_0_75, negated_conjecture, ![X2:$i > $o]:((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ X2 @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_54])).
thf(c_0_76, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle), inference(spm,[status(thm)],[c_0_66, c_0_67])).
thf(c_0_77, negated_conjecture, ![X4:$i]:((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_68])).
thf(c_0_78, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_44])).
thf(c_0_79, negated_conjecture, (cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_69, c_0_56])).
thf(c_0_80, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_58])).
thf(c_0_81, negated_conjecture, ![X4:$i]:((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (ccv @ X4) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_27]), c_0_38])).
thf(c_0_82, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_72]), c_0_73])).
thf(c_0_83, negated_conjecture, ![X2:$i > $o]:((cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ ccr), inference(spm,[status(thm)],[c_0_74, c_0_71])).
thf(c_0_84, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr), inference(spm,[status(thm)],[c_0_75, c_0_67])).
thf(c_0_85, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_76]), c_0_52])).
thf(c_0_86, negated_conjecture, ![X2:$i > $o]:((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ X2 @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_68])).
thf(c_0_87, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle), inference(spm,[status(thm)],[c_0_77, c_0_67])).
thf(c_0_88, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_78, c_0_56])).
thf(c_0_89, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_79]), c_0_52])).
thf(c_0_90, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_58])).
thf(c_0_91, negated_conjecture, (cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_80, c_0_56])).
thf(c_0_92, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_82]), c_0_40])).
thf(c_0_93, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_83, c_0_82])).
thf(c_0_94, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_84]), c_0_85])).
thf(c_0_95, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr), inference(spm,[status(thm)],[c_0_86, c_0_67])).
thf(c_0_96, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_87]), c_0_52])).
thf(c_0_97, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_88]), c_0_89])).
thf(c_0_98, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_90, c_0_56])).
thf(c_0_99, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_91]), c_0_52])).
thf(c_0_100, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ X3|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ ccxad) @ ccle|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_101, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_92, c_0_93])).
thf(c_0_102, plain, ![X296:$i > $o]:(~cwcel @ X296 @ ccxr|(X296)=(ccmnf)|(cco @ X296 @ ccpnf @ ccxad)=(ccpnf)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axaddpnf1_thm])])).
thf(c_0_103, plain, ![X241:$i > $o]:(~cwcel @ X241 @ ccxr|cwbr @ X241 @ ccpnf @ ccle), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apnfge_thm])])).
thf(c_0_104, negated_conjecture, ![X4:$i]:((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|~cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (ccv @ X4) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_94]), c_0_54]), c_0_67])).
thf(c_0_105, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_95]), c_0_96])).
thf(c_0_106, negated_conjecture, ![X2:$i > $o]:((cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|~cwcel @ X2 @ ccr), inference(spm,[status(thm)],[c_0_74, c_0_94])).
thf(c_0_107, negated_conjecture, ![X4:$i]:((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (ccv @ X4) @ epred10_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_97]), c_0_44]), c_0_56])).
thf(c_0_108, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_98]), c_0_99])).
thf(c_0_109, negated_conjecture, ![X2:$i > $o]:((cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwcel @ X2 @ ccr), inference(spm,[status(thm)],[c_0_74, c_0_97])).
thf(c_0_110, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_101]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_111, plain, ![X2:$i > $o]:((X2)=(ccmnf)|(cco @ X2 @ ccpnf @ ccxad)=(ccpnf)|~cwcel @ X2 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_102])).
thf(c_0_112, plain, ![X2:$i > $o]:(cwbr @ X2 @ ccpnf @ ccle|~cwcel @ X2 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_103])).
thf(c_0_113, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_49, c_0_40])).
thf(c_0_114, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_105]), c_0_68])).
thf(c_0_115, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(spm,[status(thm)],[c_0_106, c_0_105])).
thf(c_0_116, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_108]), c_0_58])).
thf(c_0_117, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_109, c_0_108])).
thf(c_0_118, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_110]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_119, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_72]), c_0_73])).
thf(c_0_120, negated_conjecture, (cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccle|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_112, c_0_113])).
thf(c_0_121, plain, ![X327:$i > $o]:(~cwcel @ X327 @ ccxr|(X327)=(ccmnf)|(cco @ ccpnf @ X327 @ ccxad)=(ccpnf)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axaddpnf2_thm])])).
thf(c_0_122, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ ccxad) @ ccle|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_123, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle), inference(spm,[status(thm)],[c_0_114, c_0_115])).
thf(c_0_124, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|cwcel @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X3|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ ccxad) @ ccle|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_125, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_116, c_0_117])).
thf(c_0_126, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_119]), c_0_120])).
thf(c_0_127, plain, ![X2:$i > $o]:((X2)=(ccmnf)|(cco @ ccpnf @ X2 @ ccxad)=(ccpnf)|~cwcel @ X2 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_121])).
thf(c_0_128, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_123]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_129, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwcel @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr), inference(spm,[status(thm)],[c_0_75, c_0_68])).
thf(c_0_130, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_125]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_131, negated_conjecture, (cwcel @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_78, c_0_58])).
thf(c_0_132, negated_conjecture, (cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_126]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_133, negated_conjecture, ((cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)=(ccpnf)|cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_61]), c_0_62])).
thf(c_0_134, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_128]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_135, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_95]), c_0_96])).
thf(c_0_136, negated_conjecture, ((ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccle), inference(spm,[status(thm)],[c_0_112, c_0_129])).
thf(c_0_137, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_130]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_138, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_98]), c_0_99])).
thf(c_0_139, negated_conjecture, (cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccle|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(spm,[status(thm)],[c_0_112, c_0_131])).
thf(c_0_140, negated_conjecture, cwcel @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_133]), c_0_120])).
thf(c_0_141, negated_conjecture, ![X4:$i, X5:$i]:(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccc0 @ ccle|(ccv @ X4)!=(ccv @ X5)|~epred8_0|~cwcel @ (ccv @ X4) @ epred10_0|~cwcel @ (ccv @ X5) @ epred10_0), inference(split_conjunct,[status(thm)],[c_0_12])).
thf(c_0_142, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_134, c_0_135]), c_0_136])).
thf(c_0_143, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_137, c_0_138]), c_0_139])).
thf(c_0_144, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_140])).
thf(c_0_145, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_140])).
thf(c_0_146, negated_conjecture, ![X5:$i, X4:$i]:(cwbr @ (cco @ (ccv @ X4) @ (ccv @ X5) @ epred9_0) @ ccc0 @ ccle|(ccv @ X4)!=(ccv @ X5)|~cwcel @ (ccv @ X5) @ epred10_0|~cwcel @ (ccv @ X4) @ epred10_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_15])])).
thf(c_0_147, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_142]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_148, negated_conjecture, ((cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)=(ccpnf)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_84]), c_0_85])).
thf(c_0_149, negated_conjecture, (cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_143]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_150, negated_conjecture, ((cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)=(ccpnf)|cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_88]), c_0_89])).
thf(c_0_151, plain, ![X2:$i > $o, X3:$i > $o]:((X2)=(X3)|~cwbr @ X2 @ X3 @ ccle|~cwbr @ X3 @ X2 @ ccle|~cwcel @ X2 @ ccxr|~cwcel @ X3 @ ccxr), inference(split_conjunct,[status(thm)],[c_0_17])).
thf(c_0_152, negated_conjecture, cwbr @ ccc0 @ (cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_144, c_0_140])).
thf(c_0_153, negated_conjecture, cwcel @ (cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_145, c_0_140])).
thf(c_0_154, negated_conjecture, ![X4:$i]:(cwbr @ (cco @ (ccv @ X4) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccc0 @ ccle|(ccv @ X4)!=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_146, c_0_140])).
thf(c_0_155, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|(ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_147, c_0_148]), c_0_136])).
thf(c_0_156, negated_conjecture, cwcel @ (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_150]), c_0_139])).
thf(c_0_157, negated_conjecture, ((cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0)|~cwbr @ (cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccc0 @ ccle), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_151, c_0_152]), c_0_33]), c_0_153])])).
thf(c_0_158, negated_conjecture, cwbr @ (cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccc0 @ ccle, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_154]), c_0_140])])).
thf(c_0_159, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)!=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))!=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_160, negated_conjecture, (ccv @ (esk2_3 @ $true @ epred9_0 @ epred10_0))=(ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_155]), c_0_43]), c_0_156]), c_0_140])])).
thf(c_0_161, negated_conjecture, (cco @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk1_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccc0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_158])])).
thf(c_0_162, negated_conjecture, cwcel @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_160]), c_0_161]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_163, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)!=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))!=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_164, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X3|cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)!=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))!=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_165, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_162])).
thf(c_0_166, negated_conjecture, cwcel @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163, c_0_160]), c_0_161]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_167, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_162])).
thf(c_0_168, negated_conjecture, cwcel @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred10_0, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164, c_0_160]), c_0_161]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_169, negated_conjecture, cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_165, c_0_166])).
thf(c_0_170, negated_conjecture, cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_167, c_0_166])).
thf(c_0_171, negated_conjecture, ![X4:$i]:(cwbr @ ccc0 @ (cco @ (ccv @ X4) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle|~cwcel @ (ccv @ X4) @ epred10_0), inference(spm,[status(thm)],[c_0_26, c_0_168])).
thf(c_0_172, negated_conjecture, ![X2:$i > $o]:(cwcel @ (cco @ X2 @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr|~cwcel @ X2 @ epred10_0), inference(spm,[status(thm)],[c_0_35, c_0_168])).
thf(c_0_173, negated_conjecture, (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_169]), c_0_170])])).
thf(c_0_174, negated_conjecture, cwbr @ ccc0 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccle, inference(spm,[status(thm)],[c_0_171, c_0_166])).
thf(c_0_175, negated_conjecture, cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_172, c_0_166])).
thf(c_0_176, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_170]), c_0_173])).
thf(c_0_177, negated_conjecture, (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)!=(ccmnf), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_174]), c_0_175])])).
thf(c_0_178, negated_conjecture, ![X4:$i]:((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ X4) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle|~cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ X4) @ epred9_0) @ ccr|~cwcel @ (ccv @ X4) @ epred10_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_176]), c_0_166]), c_0_162])])).
thf(c_0_179, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwcel @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccr), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_175]), c_0_177])).
thf(c_0_180, negated_conjecture, ![X2:$i > $o]:((cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ X2 @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|~cwcel @ X2 @ ccr), inference(spm,[status(thm)],[c_0_74, c_0_176])).
thf(c_0_181, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc) @ ccle), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_178, c_0_179]), c_0_168])])).
thf(c_0_182, negated_conjecture, ((cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccaddc)=(cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)), inference(spm,[status(thm)],[c_0_180, c_0_179])).
thf(c_0_183, plain, ![X2:$i > $o, X3:$i > $o]:(cwcel @ X2 @ (ccfv @ X3 @ ccxmt)|~cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk3_3 @ $true @ X2 @ X3)) @ X2) @ (cco @ (ccv @ (esk5_3 @ $true @ X2 @ X3)) @ (ccv @ (esk4_3 @ $true @ X2 @ X3)) @ X2) @ ccxad) @ ccle|(cco @ (ccv @ (esk1_3 @ $true @ X2 @ X3)) @ (ccv @ (esk2_3 @ $true @ X2 @ X3)) @ X2)!=(ccc0)|(ccv @ (esk1_3 @ $true @ X2 @ X3))!=(ccv @ (esk2_3 @ $true @ X2 @ X3))|~cwf @ (ccxp @ X3 @ X3) @ ccxr @ X2|~cwcel @ X3 @ ccvv), inference(eliminate_boolean_vars,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_13])])])).
thf(c_0_184, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad) @ ccle), inference(spm,[status(thm)],[c_0_181, c_0_182])).
thf(c_0_185, negated_conjecture, cwcel @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxr, inference(spm,[status(thm)],[c_0_167, c_0_168])).
thf(c_0_186, negated_conjecture, ((cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)|(cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183, c_0_184]), c_0_160]), c_0_161]), c_0_160]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_187, negated_conjecture, (cco @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccxad)=(ccpnf), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_175]), c_0_177])).
thf(c_0_188, negated_conjecture, cwbr @ (cco @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccpnf @ ccle, inference(spm,[status(thm)],[c_0_112, c_0_185])).
thf(c_0_189, negated_conjecture, (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk3_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0)=(ccpnf), inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183, c_0_186]), c_0_160]), c_0_161]), c_0_160]), c_0_187]), c_0_188]), c_0_21]), c_0_22])]), c_0_23])).
thf(c_0_190, negated_conjecture, (cco @ ccpnf @ (cco @ (ccv @ (esk5_3 @ $true @ epred9_0 @ epred10_0)) @ (ccv @ (esk4_3 @ $true @ epred9_0 @ epred10_0)) @ epred9_0) @ ccxad)=(ccpnf), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_170]), c_0_173])).
thf(c_0_191, negated_conjecture, ($false), inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183, c_0_189]), c_0_160]), c_0_161]), c_0_160]), c_0_190]), c_0_188]), c_0_21]), c_0_22])]), c_0_23]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 192
# Proof object clause steps            : 170
# Proof object formula steps           : 22
# Proof object conjectures             : 144
# Proof object clause conjectures      : 141
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 35
# Proof object initial formulas used   : 11
# Proof object generating inferences   : 127
# Proof object simplifying inferences  : 202
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 71
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 441
# Removed in clause preprocessing      : 380
# Initial clauses in saturation        : 61
# Processed clauses                    : 54974
# ...of these trivial                  : 5389
# ...subsumed                          : 19961
# ...remaining for further processing  : 29624
# Other redundant clauses eliminated   : 2
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 3206
# Backward-rewritten                   : 7591
# Generated clauses                    : 73615
# ...of the previous two non-trivial   : 68028
# Contextual simplify-reflections      : 1149
# Paramodulations                      : 39842
# Factorizations                       : 0
# NegExts                              : 0
# Equation resolutions                 : 18
# 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  : 9621
#    Positive orientable unit clauses  : 3758
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 15
#    Non-unit-clauses                  : 5848
# Current number of unprocessed clauses: 5866
# ...number of literals in the above   : 18501
# Current number of archived formulas  : 0
# Current number of archived clauses   : 20001
# Clause-clause subsumption calls (NU) : 53954616
# Rec. Clause-clause subsumption calls : 5760022
# Non-unit clause-clause subsumptions  : 24200
# Unit Clause-clause subsumption calls : 2948011
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 443881
# BW rewrite match successes           : 90
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 4198908

# -------------------------------------------------
# User time                : 27.471 s
# System time              : 0.080 s
# Total time               : 27.551 s
# Maximum resident set size: 71656 pages
