%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG125+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:05:26 PM UTC 2026
% Result : Theorem 0.32s 5.62s
% Output : CNFRefutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : RNG125+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n009.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 01:52:11 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 0.32/5.62 % Version : CSE_E---1.7
% 0.32/5.62 % Problem : theBenchmark.p
% 0.32/5.62 % SZS status Theorem for theBenchmark.p
% 0.32/5.62 % SZS output start CNFRefutation
% 0.32/5.62 fof(m__2273, hypothesis, ((aElementOf0(xu,xI)&xu!=sz00)&![X1]:((aElementOf0(X1,xI)&X1!=sz00)=>~(iLess0(sbrdtbr0(X1),sbrdtbr0(xu))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2273)).
% 0.32/5.62 fof(mDefSSum, axiom, ![X1, X2]:((aSet0(X1)&aSet0(X2))=>![X3]:(X3=sdtpldt1(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>?[X5, X6]:((aElementOf0(X5,X1)&aElementOf0(X6,X2))&sdtpldt0(X5,X6)=X4))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefSSum)).
% 0.32/5.62 fof(mChineseRemainder, axiom, ![X1, X2]:((aIdeal0(X1)&aIdeal0(X2))=>(![X3]:(aElement0(X3)=>aElementOf0(X3,sdtpldt1(X1,X2)))=>![X3, X4]:((aElement0(X3)&aElement0(X4))=>?[X5]:((aElement0(X5)&sdteqdtlpzmzozddtrp0(X5,X3,X1))&sdteqdtlpzmzozddtrp0(X5,X4,X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mChineseRemainder)).
% 0.32/5.62 fof(mDefSInt, axiom, ![X1, X2]:((aSet0(X1)&aSet0(X2))=>![X3]:(X3=sdtasasdt0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aElementOf0(X4,X1)&aElementOf0(X4,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefSInt)).
% 0.32/5.62 fof(mDefGCD, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>![X3]:(aGcdOfAnd0(X3,X1,X2)<=>((aDivisorOf0(X3,X1)&aDivisorOf0(X3,X2))&![X4]:((aDivisorOf0(X4,X1)&aDivisorOf0(X4,X2))=>doDivides0(X4,X3))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefGCD)).
% 0.32/5.62 fof(mDefIdeal, axiom, ![X1]:(aIdeal0(X1)<=>(aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>(![X3]:(aElementOf0(X3,X1)=>aElementOf0(sdtpldt0(X2,X3),X1))&![X3]:(aElement0(X3)=>aElementOf0(sdtasdt0(X3,X2),X1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefIdeal)).
% 0.32/5.62 fof(mDefMod, axiom, ![X1, X2, X3]:(((aElement0(X1)&aElement0(X2))&aIdeal0(X3))=>(sdteqdtlpzmzozddtrp0(X1,X2,X3)<=>aElementOf0(sdtpldt0(X1,smndt0(X2)),X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefMod)).
% 0.32/5.62 fof(mDefPrIdeal, axiom, ![X1]:(aElement0(X1)=>![X2]:(X2=slsdtgt0(X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)<=>?[X4]:(aElement0(X4)&sdtasdt0(X1,X4)=X3))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefPrIdeal)).
% 0.32/5.62 fof(mSetEq, axiom, ![X1, X2]:((aSet0(X1)&aSet0(X2))=>((![X3]:(aElementOf0(X3,X1)=>aElementOf0(X3,X2))&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,X1)))=>X1=X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSetEq)).
% 0.32/5.62 fof(mDivision, axiom, ![X1, X2]:(((aElement0(X1)&aElement0(X2))&X2!=sz00)=>?[X3, X4]:(((aElement0(X3)&aElement0(X4))&X1=sdtpldt0(sdtasdt0(X3,X2),X4))&(X4!=sz00=>iLess0(sbrdtbr0(X4),sbrdtbr0(X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDivision)).
% 0.32/5.62 fof(mAMDistr, axiom, ![X1, X2, X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X2,X3),X1)=sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAMDistr)).
% 0.32/5.62 fof(mDefRel, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>(misRelativelyPrime0(X1,X2)<=>aGcdOfAnd0(sz10,X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefRel)).
% 0.32/5.62 fof(mMulAsso, axiom, ![X1, X2, X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulAsso)).
% 0.32/5.62 fof(mAddAsso, axiom, ![X1, X2, X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>sdtpldt0(sdtpldt0(X1,X2),X3)=sdtpldt0(X1,sdtpldt0(X2,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddAsso)).
% 0.32/5.62 fof(mDefDiv, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aElement0(X3)&sdtasdt0(X1,X3)=X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefDiv)).
% 0.32/5.62 fof(m__2416, hypothesis, ?[X1, X2]:((aElement0(X1)&aElement0(X2))&xu=sdtpldt0(sdtasdt0(xa,X1),sdtasdt0(xb,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2416)).
% 0.32/5.62 fof(mDefDvs, axiom, ![X1]:(aElement0(X1)=>![X2]:(aDivisorOf0(X2,X1)<=>(aElement0(X2)&doDivides0(X2,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefDvs)).
% 0.32/5.62 fof(m__2228, hypothesis, ?[X1]:(aElementOf0(X1,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))&X1!=sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2228)).
% 0.32/5.62 fof(mIdeInt, axiom, ![X1, X2]:((aIdeal0(X1)&aIdeal0(X2))=>aIdeal0(sdtasasdt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIdeInt)).
% 0.32/5.62 fof(mIdeSum, axiom, ![X1, X2]:((aIdeal0(X1)&aIdeal0(X2))=>aIdeal0(sdtpldt1(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIdeSum)).
% 0.32/5.62 fof(mSortsB_02, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>aElement0(sdtasdt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsB_02)).
% 0.32/5.62 fof(mSortsB, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>aElement0(sdtpldt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsB)).
% 0.32/5.62 fof(mMulComm, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulComm)).
% 0.32/5.62 fof(mAddComm, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddComm)).
% 0.32/5.62 fof(mCancel, axiom, ![X1, X2]:((aElement0(X1)&aElement0(X2))=>(sdtasdt0(X1,X2)=sz00=>(X1=sz00|X2=sz00))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mCancel)).
% 0.32/5.62 fof(m__2383, hypothesis, ~((aDivisorOf0(xu,xa)&aDivisorOf0(xu,xb))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2383)).
% 0.32/5.62 fof(mEOfElem, axiom, ![X1]:(aSet0(X1)=>![X2]:(aElementOf0(X2,X1)=>aElement0(X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEOfElem)).
% 0.32/5.62 fof(mMulMnOne, axiom, ![X1]:(aElement0(X1)=>(sdtasdt0(smndt0(sz10),X1)=smndt0(X1)&smndt0(X1)=sdtasdt0(X1,smndt0(sz10)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulMnOne)).
% 0.32/5.62 fof(mAddInvr, axiom, ![X1]:(aElement0(X1)=>(sdtpldt0(X1,smndt0(X1))=sz00&sz00=sdtpldt0(smndt0(X1),X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddInvr)).
% 0.32/5.62 fof(mMulUnit, axiom, ![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulUnit)).
% 0.32/5.62 fof(mAddZero, axiom, ![X1]:(aElement0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddZero)).
% 0.32/5.62 fof(mMulZero, axiom, ![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulZero)).
% 0.32/5.62 fof(mEucSort, axiom, ![X1]:((aElement0(X1)&X1!=sz00)=>aNaturalNumber0(sbrdtbr0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEucSort)).
% 0.32/5.62 fof(mPrIdeal, axiom, ![X1]:(aElement0(X1)=>aIdeal0(slsdtgt0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mPrIdeal)).
% 0.32/5.62 fof(mSortsU, axiom, ![X1]:(aElement0(X1)=>aElement0(smndt0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsU)).
% 0.32/5.62 fof(m__2612, hypothesis, ~(~(doDivides0(xu,xb))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2612)).
% 0.32/5.62 fof(m__2479, hypothesis, ~(~(doDivides0(xu,xa))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2479)).
% 0.32/5.62 fof(m__2129, hypothesis, aGcdOfAnd0(xc,xa,xb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2129)).
% 0.32/5.62 fof(m__2174, hypothesis, (aIdeal0(xI)&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2174)).
% 0.32/5.62 fof(m__2203, hypothesis, (((aElementOf0(sz00,slsdtgt0(xa))&aElementOf0(xa,slsdtgt0(xa)))&aElementOf0(sz00,slsdtgt0(xb)))&aElementOf0(xb,slsdtgt0(xb))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2203)).
% 0.32/5.62 fof(m__2091, hypothesis, (aElement0(xa)&aElement0(xb)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2091)).
% 0.32/5.62 fof(mSortsC_01, axiom, aElement0(sz10), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsC_01)).
% 0.32/5.62 fof(mSortsC, axiom, aElement0(sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsC)).
% 0.32/5.62 fof(m__2110, hypothesis, (xa!=sz00|xb!=sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2110)).
% 0.32/5.62 fof(mUnNeZr, axiom, sz10!=sz00, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnNeZr)).
% 0.32/5.62 fof(i_0_45, hypothesis, ((aElementOf0(xu,xI)&xu!=sz00)&![X1]:((aElementOf0(X1,xI)&X1!=sz00)=>~iLess0(sbrdtbr0(X1),sbrdtbr0(xu)))), inference(fof_simplification,[status(thm)],[m__2273])).
% 0.32/5.62 fof(i_0_46, plain, ![X126, X127, X128, X129, X132, X133, X134, X135, X137, X138]:(((aSet0(X128)|X128!=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))&((((aElementOf0(esk3_4(X126,X127,X128,X129),X126)|~aElementOf0(X129,X128)|X128!=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))&(aElementOf0(esk4_4(X126,X127,X128,X129),X127)|~aElementOf0(X129,X128)|X128!=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127))))&(sdtpldt0(esk3_4(X126,X127,X128,X129),esk4_4(X126,X127,X128,X129))=X129|~aElementOf0(X129,X128)|X128!=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127))))&(~aElementOf0(X133,X126)|~aElementOf0(X134,X127)|sdtpldt0(X133,X134)!=X132|aElementOf0(X132,X128)|X128!=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))))&((~aElementOf0(esk5_3(X126,X127,X135),X135)|(~aElementOf0(X137,X126)|~aElementOf0(X138,X127)|sdtpldt0(X137,X138)!=esk5_3(X126,X127,X135))|~aSet0(X135)|X135=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))&(((aElementOf0(esk6_3(X126,X127,X135),X126)|aElementOf0(esk5_3(X126,X127,X135),X135)|~aSet0(X135)|X135=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))&(aElementOf0(esk7_3(X126,X127,X135),X127)|aElementOf0(esk5_3(X126,X127,X135),X135)|~aSet0(X135)|X135=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127))))&(sdtpldt0(esk6_3(X126,X127,X135),esk7_3(X126,X127,X135))=esk5_3(X126,X127,X135)|aElementOf0(esk5_3(X126,X127,X135),X135)|~aSet0(X135)|X135=sdtpldt1(X126,X127)|(~aSet0(X126)|~aSet0(X127)))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSSum])])])])])])).
% 0.32/5.62 fof(i_0_47, plain, ![X163, X164, X166, X167]:((((aElement0(esk13_4(X163,X164,X166,X167))|(~aElement0(X166)|~aElement0(X167))|aElement0(esk12_2(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164)))&(sdteqdtlpzmzozddtrp0(esk13_4(X163,X164,X166,X167),X166,X163)|(~aElement0(X166)|~aElement0(X167))|aElement0(esk12_2(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164))))&(sdteqdtlpzmzozddtrp0(esk13_4(X163,X164,X166,X167),X167,X164)|(~aElement0(X166)|~aElement0(X167))|aElement0(esk12_2(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164))))&(((aElement0(esk13_4(X163,X164,X166,X167))|(~aElement0(X166)|~aElement0(X167))|~aElementOf0(esk12_2(X163,X164),sdtpldt1(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164)))&(sdteqdtlpzmzozddtrp0(esk13_4(X163,X164,X166,X167),X166,X163)|(~aElement0(X166)|~aElement0(X167))|~aElementOf0(esk12_2(X163,X164),sdtpldt1(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164))))&(sdteqdtlpzmzozddtrp0(esk13_4(X163,X164,X166,X167),X167,X164)|(~aElement0(X166)|~aElement0(X167))|~aElementOf0(esk12_2(X163,X164),sdtpldt1(X163,X164))|(~aIdeal0(X163)|~aIdeal0(X164))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mChineseRemainder])])])])])).
% 0.32/5.62 fof(i_0_48, plain, ![X141, X142, X143, X144, X145, X146]:(((aSet0(X143)|X143!=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))&(((aElementOf0(X144,X141)|~aElementOf0(X144,X143)|X143!=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))&(aElementOf0(X144,X142)|~aElementOf0(X144,X143)|X143!=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142))))&(~aElementOf0(X145,X141)|~aElementOf0(X145,X142)|aElementOf0(X145,X143)|X143!=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))))&((~aElementOf0(esk8_3(X141,X142,X146),X146)|(~aElementOf0(esk8_3(X141,X142,X146),X141)|~aElementOf0(esk8_3(X141,X142,X146),X142))|~aSet0(X146)|X146=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))&((aElementOf0(esk8_3(X141,X142,X146),X141)|aElementOf0(esk8_3(X141,X142,X146),X146)|~aSet0(X146)|X146=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))&(aElementOf0(esk8_3(X141,X142,X146),X142)|aElementOf0(esk8_3(X141,X142,X146),X146)|~aSet0(X146)|X146=sdtasasdt0(X141,X142)|(~aSet0(X141)|~aSet0(X142)))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSInt])])])])])])).
% 0.32/5.62 fof(i_0_49, plain, ![X180, X181, X182, X183, X184]:((((aDivisorOf0(X182,X180)|~aGcdOfAnd0(X182,X180,X181)|(~aElement0(X180)|~aElement0(X181)))&(aDivisorOf0(X182,X181)|~aGcdOfAnd0(X182,X180,X181)|(~aElement0(X180)|~aElement0(X181))))&(~aDivisorOf0(X183,X180)|~aDivisorOf0(X183,X181)|doDivides0(X183,X182)|~aGcdOfAnd0(X182,X180,X181)|(~aElement0(X180)|~aElement0(X181))))&(((aDivisorOf0(esk17_3(X180,X181,X184),X180)|(~aDivisorOf0(X184,X180)|~aDivisorOf0(X184,X181))|aGcdOfAnd0(X184,X180,X181)|(~aElement0(X180)|~aElement0(X181)))&(aDivisorOf0(esk17_3(X180,X181,X184),X181)|(~aDivisorOf0(X184,X180)|~aDivisorOf0(X184,X181))|aGcdOfAnd0(X184,X180,X181)|(~aElement0(X180)|~aElement0(X181))))&(~doDivides0(esk17_3(X180,X181,X184),X184)|(~aDivisorOf0(X184,X180)|~aDivisorOf0(X184,X181))|aGcdOfAnd0(X184,X180,X181)|(~aElement0(X180)|~aElement0(X181))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefGCD])])])])])])).
% 0.32/5.62 fof(i_0_50, plain, ![X148, X149, X150, X151, X152]:(((aSet0(X148)|~aIdeal0(X148))&((~aElementOf0(X150,X148)|aElementOf0(sdtpldt0(X149,X150),X148)|~aElementOf0(X149,X148)|~aIdeal0(X148))&(~aElement0(X151)|aElementOf0(sdtasdt0(X151,X149),X148)|~aElementOf0(X149,X148)|~aIdeal0(X148))))&((aElementOf0(esk9_1(X152),X152)|~aSet0(X152)|aIdeal0(X152))&(((aElement0(esk11_1(X152))|aElementOf0(esk10_1(X152),X152)|~aSet0(X152)|aIdeal0(X152))&(~aElementOf0(sdtasdt0(esk11_1(X152),esk9_1(X152)),X152)|aElementOf0(esk10_1(X152),X152)|~aSet0(X152)|aIdeal0(X152)))&((aElement0(esk11_1(X152))|~aElementOf0(sdtpldt0(esk9_1(X152),esk10_1(X152)),X152)|~aSet0(X152)|aIdeal0(X152))&(~aElementOf0(sdtasdt0(esk11_1(X152),esk9_1(X152)),X152)|~aElementOf0(sdtpldt0(esk9_1(X152),esk10_1(X152)),X152)|~aSet0(X152)|aIdeal0(X152)))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefIdeal])])])])])])).
% 0.32/5.62 fof(i_0_51, plain, ![X160, X161, X162]:((~sdteqdtlpzmzozddtrp0(X160,X161,X162)|aElementOf0(sdtpldt0(X160,smndt0(X161)),X162)|(~aElement0(X160)|~aElement0(X161)|~aIdeal0(X162)))&(~aElementOf0(sdtpldt0(X160,smndt0(X161)),X162)|sdteqdtlpzmzozddtrp0(X160,X161,X162)|(~aElement0(X160)|~aElement0(X161)|~aIdeal0(X162)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefMod])])])).
% 0.32/5.62 fof(i_0_52, plain, ![X188, X189, X190, X192, X193, X194, X196]:(((aSet0(X189)|X189!=slsdtgt0(X188)|~aElement0(X188))&(((aElement0(esk18_3(X188,X189,X190))|~aElementOf0(X190,X189)|X189!=slsdtgt0(X188)|~aElement0(X188))&(sdtasdt0(X188,esk18_3(X188,X189,X190))=X190|~aElementOf0(X190,X189)|X189!=slsdtgt0(X188)|~aElement0(X188)))&(~aElement0(X193)|sdtasdt0(X188,X193)!=X192|aElementOf0(X192,X189)|X189!=slsdtgt0(X188)|~aElement0(X188))))&((~aElementOf0(esk19_2(X188,X194),X194)|(~aElement0(X196)|sdtasdt0(X188,X196)!=esk19_2(X188,X194))|~aSet0(X194)|X194=slsdtgt0(X188)|~aElement0(X188))&((aElement0(esk20_2(X188,X194))|aElementOf0(esk19_2(X188,X194),X194)|~aSet0(X194)|X194=slsdtgt0(X188)|~aElement0(X188))&(sdtasdt0(X188,esk20_2(X188,X194))=esk19_2(X188,X194)|aElementOf0(esk19_2(X188,X194),X194)|~aSet0(X194)|X194=slsdtgt0(X188)|~aElement0(X188))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefPrIdeal])])])])])])).
% 0.32/5.62 fof(i_0_53, plain, ![X122, X123]:(((aElementOf0(esk2_2(X122,X123),X123)|aElementOf0(esk1_2(X122,X123),X122)|X122=X123|(~aSet0(X122)|~aSet0(X123)))&(~aElementOf0(esk2_2(X122,X123),X122)|aElementOf0(esk1_2(X122,X123),X122)|X122=X123|(~aSet0(X122)|~aSet0(X123))))&((aElementOf0(esk2_2(X122,X123),X123)|~aElementOf0(esk1_2(X122,X123),X123)|X122=X123|(~aSet0(X122)|~aSet0(X123)))&(~aElementOf0(esk2_2(X122,X123),X122)|~aElementOf0(esk1_2(X122,X123),X123)|X122=X123|(~aSet0(X122)|~aSet0(X123))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSetEq])])])])).
% 0.32/5.62 fof(i_0_54, plain, ![X170, X171]:((((aElement0(esk14_2(X170,X171))|(~aElement0(X170)|~aElement0(X171)|X171=sz00))&(aElement0(esk15_2(X170,X171))|(~aElement0(X170)|~aElement0(X171)|X171=sz00)))&(X170=sdtpldt0(sdtasdt0(esk14_2(X170,X171),X171),esk15_2(X170,X171))|(~aElement0(X170)|~aElement0(X171)|X171=sz00)))&(esk15_2(X170,X171)=sz00|iLess0(sbrdtbr0(esk15_2(X170,X171)),sbrdtbr0(X171))|(~aElement0(X170)|~aElement0(X171)|X171=sz00))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDivision])])])])).
% 0.32/5.62 fof(i_0_55, plain, ![X113, X114, X115]:((sdtasdt0(X113,sdtpldt0(X114,X115))=sdtpldt0(sdtasdt0(X113,X114),sdtasdt0(X113,X115))|(~aElement0(X113)|~aElement0(X114)|~aElement0(X115)))&(sdtasdt0(sdtpldt0(X114,X115),X113)=sdtpldt0(sdtasdt0(X114,X113),sdtasdt0(X115,X113))|(~aElement0(X113)|~aElement0(X114)|~aElement0(X115)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAMDistr])])])).
% 0.32/5.62 fof(i_0_56, plain, ![X186, X187]:((~misRelativelyPrime0(X186,X187)|aGcdOfAnd0(sz10,X186,X187)|(~aElement0(X186)|~aElement0(X187)))&(~aGcdOfAnd0(sz10,X186,X187)|misRelativelyPrime0(X186,X187)|(~aElement0(X186)|~aElement0(X187)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefRel])])])).
% 0.32/5.62 fof(i_0_57, plain, ![X109, X110, X111]:(~aElement0(X109)|~aElement0(X110)|~aElement0(X111)|sdtasdt0(sdtasdt0(X109,X110),X111)=sdtasdt0(X109,sdtasdt0(X110,X111))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulAsso])])).
% 0.32/5.62 fof(i_0_58, plain, ![X102, X103, X104]:(~aElement0(X102)|~aElement0(X103)|~aElement0(X104)|sdtpldt0(sdtpldt0(X102,X103),X104)=sdtpldt0(X102,sdtpldt0(X103,X104))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddAsso])])).
% 0.32/5.62 fof(i_0_59, plain, ![X174, X175, X177]:(((aElement0(esk16_2(X174,X175))|~doDivides0(X174,X175)|(~aElement0(X174)|~aElement0(X175)))&(sdtasdt0(X174,esk16_2(X174,X175))=X175|~doDivides0(X174,X175)|(~aElement0(X174)|~aElement0(X175))))&(~aElement0(X177)|sdtasdt0(X174,X177)!=X175|doDivides0(X174,X175)|(~aElement0(X174)|~aElement0(X175)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefDiv])])])])])).
% 0.32/5.62 fof(i_0_60, hypothesis, ![X200]:((aElementOf0(xu,xI)&xu!=sz00)&(~aElementOf0(X200,xI)|X200=sz00|~iLess0(sbrdtbr0(X200),sbrdtbr0(xu)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_45])])])).
% 0.32/5.62 fof(i_0_61, hypothesis, ((aElement0(esk22_0)&aElement0(esk23_0))&xu=sdtpldt0(sdtasdt0(xa,esk22_0),sdtasdt0(xb,esk23_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[m__2416])])).
% 0.32/5.62 fof(i_0_62, plain, ![X178, X179]:(((aElement0(X179)|~aDivisorOf0(X179,X178)|~aElement0(X178))&(doDivides0(X179,X178)|~aDivisorOf0(X179,X178)|~aElement0(X178)))&(~aElement0(X179)|~doDivides0(X179,X178)|aDivisorOf0(X179,X178)|~aElement0(X178))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefDvs])])])])).
% 0.32/5.62 fof(i_0_63, hypothesis, (aElementOf0(esk21_0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))&esk21_0!=sz00), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[m__2228])])).
% 0.32/5.62 fof(i_0_64, plain, ![X158, X159]:(~aIdeal0(X158)|~aIdeal0(X159)|aIdeal0(sdtasasdt0(X158,X159))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIdeInt])])).
% 0.32/5.62 fof(i_0_65, plain, ![X156, X157]:(~aIdeal0(X156)|~aIdeal0(X157)|aIdeal0(sdtpldt1(X156,X157))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIdeSum])])).
% 0.32/5.62 fof(i_0_66, plain, ![X98, X99]:(~aElement0(X98)|~aElement0(X99)|aElement0(sdtasdt0(X98,X99))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB_02])])).
% 0.32/5.62 fof(i_0_67, plain, ![X96, X97]:(~aElement0(X96)|~aElement0(X97)|aElement0(sdtpldt0(X96,X97))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB])])).
% 0.32/5.62 fof(i_0_68, plain, ![X107, X108]:(~aElement0(X107)|~aElement0(X108)|sdtasdt0(X107,X108)=sdtasdt0(X108,X107)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulComm])])).
% 0.32/5.62 fof(i_0_69, plain, ![X100, X101]:(~aElement0(X100)|~aElement0(X101)|sdtpldt0(X100,X101)=sdtpldt0(X101,X100)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddComm])])).
% 0.32/5.62 fof(i_0_70, plain, ![X118, X119]:(~aElement0(X118)|~aElement0(X119)|(sdtasdt0(X118,X119)!=sz00|(X118=sz00|X119=sz00))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCancel])])).
% 0.32/5.62 fof(i_0_71, hypothesis, (~aDivisorOf0(xu,xa)|~aDivisorOf0(xu,xb)), inference(fof_nnf,[status(thm)],[m__2383])).
% 0.32/5.62 fof(i_0_72, plain, ![X120, X121]:(~aSet0(X120)|(~aElementOf0(X121,X120)|aElement0(X121))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEOfElem])])])).
% 0.32/5.62 fof(i_0_73, plain, ![X116]:((sdtasdt0(smndt0(sz10),X116)=smndt0(X116)|~aElement0(X116))&(smndt0(X116)=sdtasdt0(X116,smndt0(sz10))|~aElement0(X116))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulMnOne])])])).
% 0.32/5.62 fof(i_0_74, plain, ![X106]:((sdtpldt0(X106,smndt0(X106))=sz00|~aElement0(X106))&(sz00=sdtpldt0(smndt0(X106),X106)|~aElement0(X106))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddInvr])])])).
% 0.32/5.62 fof(i_0_75, plain, ![X112]:((sdtasdt0(X112,sz10)=X112|~aElement0(X112))&(X112=sdtasdt0(sz10,X112)|~aElement0(X112))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulUnit])])])).
% 0.32/5.62 fof(i_0_76, plain, ![X105]:((sdtpldt0(X105,sz00)=X105|~aElement0(X105))&(X105=sdtpldt0(sz00,X105)|~aElement0(X105))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddZero])])])).
% 0.32/5.62 fof(i_0_77, plain, ![X117]:((sdtasdt0(X117,sz00)=sz00|~aElement0(X117))&(sz00=sdtasdt0(sz00,X117)|~aElement0(X117))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulZero])])])).
% 0.32/5.62 fof(i_0_78, plain, ![X169]:(~aElement0(X169)|X169=sz00|aNaturalNumber0(sbrdtbr0(X169))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEucSort])])).
% 0.32/5.62 fof(i_0_79, plain, ![X198]:(~aElement0(X198)|aIdeal0(slsdtgt0(X198))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mPrIdeal])])).
% 0.32/5.62 fof(i_0_80, plain, ![X95]:(~aElement0(X95)|aElement0(smndt0(X95))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsU])])).
% 0.32/5.62 fof(i_0_81, hypothesis, doDivides0(xu,xb), inference(fof_simplification,[status(thm)],[m__2612])).
% 0.32/5.62 fof(i_0_82, hypothesis, doDivides0(xu,xa), inference(fof_simplification,[status(thm)],[m__2479])).
% 0.32/5.62 cnf(i_0_83, plain, (sdtpldt0(esk3_4(X1,X2,X3,X4),esk4_4(X1,X2,X3,X4))=X4|~aElementOf0(X4,X3)|X3!=sdtpldt1(X1,X2)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_84, plain, (sdteqdtlpzmzozddtrp0(esk13_4(X1,X2,X3,X4),X3,X1)|~aElement0(X3)|~aElement0(X4)|~aElementOf0(esk12_2(X1,X2),sdtpldt1(X1,X2))|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_85, plain, (sdteqdtlpzmzozddtrp0(esk13_4(X1,X2,X3,X4),X4,X2)|~aElement0(X3)|~aElement0(X4)|~aElementOf0(esk12_2(X1,X2),sdtpldt1(X1,X2))|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_86, plain, (aElement0(esk13_4(X1,X2,X3,X4))|~aElement0(X3)|~aElement0(X4)|~aElementOf0(esk12_2(X1,X2),sdtpldt1(X1,X2))|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_87, plain, (X3=sdtasasdt0(X1,X2)|~aElementOf0(esk8_3(X1,X2,X3),X3)|~aElementOf0(esk8_3(X1,X2,X3),X1)|~aElementOf0(esk8_3(X1,X2,X3),X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_88, plain, (sdteqdtlpzmzozddtrp0(esk13_4(X1,X2,X3,X4),X3,X1)|aElement0(esk12_2(X1,X2))|~aElement0(X3)|~aElement0(X4)|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_89, plain, (sdteqdtlpzmzozddtrp0(esk13_4(X1,X2,X3,X4),X4,X2)|aElement0(esk12_2(X1,X2))|~aElement0(X3)|~aElement0(X4)|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_90, plain, (aElementOf0(esk4_4(X1,X2,X3,X4),X2)|~aElementOf0(X4,X3)|X3!=sdtpldt1(X1,X2)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_91, plain, (aElementOf0(esk3_4(X1,X2,X3,X4),X1)|~aElementOf0(X4,X3)|X3!=sdtpldt1(X1,X2)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_92, plain, (aElement0(esk13_4(X1,X2,X3,X4))|aElement0(esk12_2(X1,X2))|~aElement0(X3)|~aElement0(X4)|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.32/5.62 cnf(i_0_93, plain, (sdtpldt0(esk6_3(X1,X2,X3),esk7_3(X1,X2,X3))=esk5_3(X1,X2,X3)|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtpldt1(X1,X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_94, plain, (X3=sdtpldt1(X1,X2)|~aElementOf0(esk5_3(X1,X2,X3),X3)|~aElementOf0(X4,X1)|~aElementOf0(X5,X2)|sdtpldt0(X4,X5)!=esk5_3(X1,X2,X3)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_95, plain, (aGcdOfAnd0(X3,X1,X2)|~doDivides0(esk17_3(X1,X2,X3),X3)|~aDivisorOf0(X3,X1)|~aDivisorOf0(X3,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_96, plain, (aElementOf0(esk8_3(X1,X2,X3),X1)|aElementOf0(esk8_3(X1,X2,X3),X3)|X3=sdtasasdt0(X1,X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_97, plain, (aElementOf0(esk8_3(X1,X2,X3),X2)|aElementOf0(esk8_3(X1,X2,X3),X3)|X3=sdtasasdt0(X1,X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_98, plain, (aElementOf0(esk7_3(X1,X2,X3),X2)|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtpldt1(X1,X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_99, plain, (aElementOf0(esk6_3(X1,X2,X3),X1)|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtpldt1(X1,X2)|~aSet0(X3)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_100, plain, (aDivisorOf0(esk17_3(X1,X2,X3),X1)|aGcdOfAnd0(X3,X1,X2)|~aDivisorOf0(X3,X1)|~aDivisorOf0(X3,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_101, plain, (aDivisorOf0(esk17_3(X1,X2,X3),X2)|aGcdOfAnd0(X3,X1,X2)|~aDivisorOf0(X3,X1)|~aDivisorOf0(X3,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_102, plain, (aIdeal0(X1)|~aElementOf0(sdtasdt0(esk11_1(X1),esk9_1(X1)),X1)|~aElementOf0(sdtpldt0(esk9_1(X1),esk10_1(X1)),X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_103, plain, (doDivides0(X1,X4)|~aDivisorOf0(X1,X2)|~aDivisorOf0(X1,X3)|~aGcdOfAnd0(X4,X2,X3)|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_104, plain, (aElementOf0(sdtpldt0(X1,smndt0(X2)),X3)|~sdteqdtlpzmzozddtrp0(X1,X2,X3)|~aElement0(X1)|~aElement0(X2)|~aIdeal0(X3)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.32/5.62 cnf(i_0_105, plain, (sdtasdt0(X1,esk18_3(X1,X2,X3))=X3|~aElementOf0(X3,X2)|X2!=slsdtgt0(X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_106, plain, (sdteqdtlpzmzozddtrp0(X1,X2,X3)|~aElementOf0(sdtpldt0(X1,smndt0(X2)),X3)|~aElement0(X1)|~aElement0(X2)|~aIdeal0(X3)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.32/5.62 cnf(i_0_107, plain, (aElement0(esk18_3(X1,X2,X3))|~aElementOf0(X3,X2)|X2!=slsdtgt0(X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_108, plain, (X1=X2|~aElementOf0(esk2_2(X1,X2),X1)|~aElementOf0(esk1_2(X1,X2),X2)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.32/5.62 cnf(i_0_109, plain, (X1=sdtpldt0(sdtasdt0(esk14_2(X1,X2),X2),esk15_2(X1,X2))|X2=sz00|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.32/5.62 cnf(i_0_110, plain, (X2=slsdtgt0(X1)|~aElementOf0(esk19_2(X1,X2),X2)|~aElement0(X3)|sdtasdt0(X1,X3)!=esk19_2(X1,X2)|~aSet0(X2)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_111, plain, (aElementOf0(esk10_1(X1),X1)|aIdeal0(X1)|~aElementOf0(sdtasdt0(esk11_1(X1),esk9_1(X1)),X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_112, plain, (sdtasdt0(sdtpldt0(X1,X2),X3)=sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))|~aElement0(X3)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.32/5.62 cnf(i_0_113, plain, (sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.32/5.62 cnf(i_0_114, plain, (aElement0(esk11_1(X1))|aIdeal0(X1)|~aElementOf0(sdtpldt0(esk9_1(X1),esk10_1(X1)),X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_115, plain, (aElementOf0(X5,X6)|~aElementOf0(X1,X2)|~aElementOf0(X3,X4)|sdtpldt0(X1,X3)!=X5|X6!=sdtpldt1(X2,X4)|~aSet0(X2)|~aSet0(X4)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_116, plain, (aElementOf0(esk2_2(X1,X2),X2)|X1=X2|~aElementOf0(esk1_2(X1,X2),X2)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.32/5.62 cnf(i_0_117, plain, (aElementOf0(esk1_2(X1,X2),X1)|X1=X2|~aElementOf0(esk2_2(X1,X2),X1)|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.32/5.62 cnf(i_0_118, plain, (aDivisorOf0(X1,X2)|~aGcdOfAnd0(X1,X2,X3)|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_119, plain, (aDivisorOf0(X1,X2)|~aGcdOfAnd0(X1,X3,X2)|~aElement0(X3)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.32/5.62 cnf(i_0_120, plain, (sdtasdt0(X1,esk20_2(X1,X2))=esk19_2(X1,X2)|aElementOf0(esk19_2(X1,X2),X2)|X2=slsdtgt0(X1)|~aSet0(X2)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_121, plain, (misRelativelyPrime0(X1,X2)|~aGcdOfAnd0(sz10,X1,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.32/5.62 cnf(i_0_122, plain, (esk15_2(X1,X2)=sz00|iLess0(sbrdtbr0(esk15_2(X1,X2)),sbrdtbr0(X2))|X2=sz00|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.32/5.62 cnf(i_0_123, plain, (sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.32/5.62 cnf(i_0_124, plain, (sdtpldt0(sdtpldt0(X1,X2),X3)=sdtpldt0(X1,sdtpldt0(X2,X3))|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.32/5.62 cnf(i_0_125, plain, (aElementOf0(X1,X4)|~aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X4!=sdtasasdt0(X2,X3)|~aSet0(X2)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_126, plain, (aElementOf0(esk2_2(X1,X2),X2)|aElementOf0(esk1_2(X1,X2),X1)|X1=X2|~aSet0(X1)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.32/5.62 cnf(i_0_127, plain, (aElementOf0(sdtpldt0(X3,X1),X2)|~aElementOf0(X1,X2)|~aElementOf0(X3,X2)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_128, plain, (aElement0(esk20_2(X1,X2))|aElementOf0(esk19_2(X1,X2),X2)|X2=slsdtgt0(X1)|~aSet0(X2)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_129, plain, (aGcdOfAnd0(sz10,X1,X2)|~misRelativelyPrime0(X1,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.32/5.62 cnf(i_0_130, plain, (sdtasdt0(X1,esk16_2(X1,X2))=X2|~doDivides0(X1,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.32/5.62 cnf(i_0_131, plain, (aElementOf0(sdtasdt0(X1,X2),X3)|~aElement0(X1)|~aElementOf0(X2,X3)|~aIdeal0(X3)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_132, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X3!=sdtasasdt0(X2,X4)|~aSet0(X2)|~aSet0(X4)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_133, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X3!=sdtasasdt0(X4,X2)|~aSet0(X4)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_134, plain, (aElement0(esk16_2(X1,X2))|~doDivides0(X1,X2)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.32/5.62 cnf(i_0_135, plain, (aElementOf0(X3,X4)|~aElement0(X1)|sdtasdt0(X2,X1)!=X3|X4!=slsdtgt0(X2)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_136, plain, (doDivides0(X2,X3)|~aElement0(X1)|sdtasdt0(X2,X1)!=X3|~aElement0(X2)|~aElement0(X3)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.32/5.62 cnf(i_0_137, hypothesis, (X1=sz00|~aElementOf0(X1,xI)|~iLess0(sbrdtbr0(X1),sbrdtbr0(xu))), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.32/5.62 cnf(i_0_138, hypothesis, (xu=sdtpldt0(sdtasdt0(xa,esk22_0),sdtasdt0(xb,esk23_0))), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.32/5.62 cnf(i_0_139, plain, (aDivisorOf0(X1,X2)|~aElement0(X1)|~doDivides0(X1,X2)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.32/5.62 cnf(i_0_140, hypothesis, (aElementOf0(esk21_0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.32/5.62 cnf(i_0_141, hypothesis, (aGcdOfAnd0(xc,xa,xb)), inference(split_conjunct,[status(thm)],[m__2129]), ['final']).
% 0.32/5.62 cnf(i_0_142, plain, (aElement0(esk15_2(X1,X2))|X2=sz00|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.32/5.62 cnf(i_0_143, plain, (aElement0(esk14_2(X1,X2))|X2=sz00|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.32/5.62 cnf(i_0_144, plain, (aIdeal0(sdtasasdt0(X1,X2))|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.32/5.62 cnf(i_0_145, plain, (aIdeal0(sdtpldt1(X1,X2))|~aIdeal0(X1)|~aIdeal0(X2)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.32/5.62 cnf(i_0_146, plain, (aElement0(sdtasdt0(X1,X2))|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.32/5.62 cnf(i_0_147, plain, (aElement0(sdtpldt0(X1,X2))|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.32/5.62 cnf(i_0_148, plain, (doDivides0(X1,X2)|~aDivisorOf0(X1,X2)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.32/5.62 cnf(i_0_149, plain, (aElement0(esk11_1(X1))|aElementOf0(esk10_1(X1),X1)|aIdeal0(X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_150, plain, (aSet0(X1)|X1!=sdtasasdt0(X2,X3)|~aSet0(X2)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.32/5.62 cnf(i_0_151, plain, (aSet0(X1)|X1!=sdtpldt1(X2,X3)|~aSet0(X2)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.32/5.62 cnf(i_0_152, plain, (sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.32/5.62 cnf(i_0_153, plain, (sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aElement0(X1)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 0.32/5.62 cnf(i_0_154, plain, (X1=sz00|X2=sz00|~aElement0(X1)|~aElement0(X2)|sdtasdt0(X1,X2)!=sz00), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.32/5.62 cnf(i_0_155, hypothesis, (~aDivisorOf0(xu,xa)|~aDivisorOf0(xu,xb)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.32/5.62 cnf(i_0_156, plain, (aElement0(X1)|~aDivisorOf0(X1,X2)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.32/5.62 cnf(i_0_157, plain, (aElement0(X2)|~aSet0(X1)|~aElementOf0(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.32/5.62 cnf(i_0_158, plain, (aElementOf0(esk9_1(X1),X1)|aIdeal0(X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_159, plain, (sdtasdt0(smndt0(sz10),X1)=smndt0(X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.32/5.62 cnf(i_0_160, plain, (smndt0(X1)=sdtasdt0(X1,smndt0(sz10))|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.32/5.62 cnf(i_0_161, plain, (sdtpldt0(X1,smndt0(X1))=sz00|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.32/5.62 cnf(i_0_162, plain, (sz00=sdtpldt0(smndt0(X1),X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.32/5.62 cnf(i_0_163, plain, (sdtasdt0(X1,sz10)=X1|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.32/5.62 cnf(i_0_164, plain, (sdtpldt0(X1,sz00)=X1|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.32/5.62 cnf(i_0_165, plain, (X1=sdtasdt0(sz10,X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.32/5.62 cnf(i_0_166, plain, (X1=sdtpldt0(sz00,X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.32/5.62 cnf(i_0_167, hypothesis, (xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))), inference(split_conjunct,[status(thm)],[m__2174]), ['final']).
% 0.32/5.62 cnf(i_0_168, plain, (aSet0(X1)|X1!=slsdtgt0(X2)|~aElement0(X2)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.32/5.62 cnf(i_0_169, plain, (sdtasdt0(X1,sz00)=sz00|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.32/5.62 cnf(i_0_170, plain, (sz00=sdtasdt0(sz00,X1)|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.32/5.62 cnf(i_0_171, plain, (X1=sz00|aNaturalNumber0(sbrdtbr0(X1))|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_78]), ['final']).
% 0.32/5.62 cnf(i_0_172, plain, (aIdeal0(slsdtgt0(X1))|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.32/5.62 cnf(i_0_173, plain, (aElement0(smndt0(X1))|~aElement0(X1)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 0.32/5.62 cnf(i_0_174, hypothesis, (aElementOf0(xb,slsdtgt0(xb))), inference(split_conjunct,[status(thm)],[m__2203]), ['final']).
% 0.32/5.62 cnf(i_0_175, hypothesis, (aElementOf0(xa,slsdtgt0(xa))), inference(split_conjunct,[status(thm)],[m__2203]), ['final']).
% 0.32/5.62 cnf(i_0_176, hypothesis, (aElementOf0(sz00,slsdtgt0(xb))), inference(split_conjunct,[status(thm)],[m__2203]), ['final']).
% 0.32/5.62 cnf(i_0_177, hypothesis, (aElementOf0(sz00,slsdtgt0(xa))), inference(split_conjunct,[status(thm)],[m__2203]), ['final']).
% 0.32/5.62 cnf(i_0_178, plain, (aSet0(X1)|~aIdeal0(X1)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.32/5.62 cnf(i_0_179, hypothesis, (doDivides0(xu,xb)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 0.32/5.62 cnf(i_0_180, hypothesis, (doDivides0(xu,xa)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 0.32/5.62 cnf(i_0_181, hypothesis, (aElementOf0(xu,xI)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.32/5.62 cnf(i_0_182, hypothesis, (aIdeal0(xI)), inference(split_conjunct,[status(thm)],[m__2174]), ['final']).
% 0.32/5.62 cnf(i_0_183, hypothesis, (aElement0(esk23_0)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.32/5.62 cnf(i_0_184, hypothesis, (aElement0(esk22_0)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.32/5.62 cnf(i_0_185, hypothesis, (aElement0(xb)), inference(split_conjunct,[status(thm)],[m__2091]), ['final']).
% 0.32/5.62 cnf(i_0_186, hypothesis, (aElement0(xa)), inference(split_conjunct,[status(thm)],[m__2091]), ['final']).
% 0.32/5.62 cnf(i_0_187, plain, (aElement0(sz10)), inference(split_conjunct,[status(thm)],[mSortsC_01]), ['final']).
% 0.32/5.62 cnf(i_0_188, plain, (aElement0(sz00)), inference(split_conjunct,[status(thm)],[mSortsC]), ['final']).
% 0.32/5.62 cnf(i_0_189, hypothesis, (xa!=sz00|xb!=sz00), inference(split_conjunct,[status(thm)],[m__2110]), ['final']).
% 0.32/5.62 cnf(i_0_190, hypothesis, (esk21_0!=sz00), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.32/5.62 cnf(i_0_191, hypothesis, (xu!=sz00), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.32/5.62 cnf(i_0_192, plain, (sz10!=sz00), inference(split_conjunct,[status(thm)],[mUnNeZr]), ['final']).
% 0.32/5.62 cnf(i_0_193, axiom, (X1=X1)).
% 0.32/5.62 cnf(i_0_194, axiom, (X1=X2|X2!=X1)).
% 0.32/5.62 cnf(i_0_195, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.32/5.62 cnf(i_0_196, axiom, (X1!=X2|sdtpldt0(X1,X3)=sdtpldt0(X2,X3))).
% 0.32/5.62 cnf(i_0_197, axiom, (X1!=X2|sdtpldt0(X3,X1)=sdtpldt0(X3,X2))).
% 0.32/5.62 cnf(i_0_198, axiom, (X1!=X2|esk5_3(X1,X3,X4)=esk5_3(X2,X3,X4))).
% 0.32/5.62 cnf(i_0_199, axiom, (X1!=X2|esk5_3(X3,X1,X4)=esk5_3(X3,X2,X4))).
% 0.32/5.62 cnf(i_0_200, axiom, (X1!=X2|esk5_3(X3,X4,X1)=esk5_3(X3,X4,X2))).
% 0.32/5.62 cnf(i_0_201, axiom, (X1!=X2|sdtasdt0(X1,X3)=sdtasdt0(X2,X3))).
% 0.32/5.62 cnf(i_0_202, axiom, (X1!=X2|sdtasdt0(X3,X1)=sdtasdt0(X3,X2))).
% 0.32/5.62 cnf(i_0_203, axiom, (X1!=X2|smndt0(X1)=smndt0(X2))).
% 0.32/5.62 cnf(i_0_204, axiom, (X1!=X2|slsdtgt0(X1)=slsdtgt0(X2))).
% 0.32/5.62 cnf(i_0_205, axiom, (X1!=X2|esk15_2(X1,X3)=esk15_2(X2,X3))).
% 0.32/5.62 cnf(i_0_206, axiom, (X1!=X2|esk15_2(X3,X1)=esk15_2(X3,X2))).
% 0.32/5.62 cnf(i_0_207, axiom, (X1!=X2|esk19_2(X1,X3)=esk19_2(X2,X3))).
% 0.32/5.62 cnf(i_0_208, axiom, (X1!=X2|esk19_2(X3,X1)=esk19_2(X3,X2))).
% 0.32/5.63 cnf(i_0_209, axiom, (X1!=X2|sdtpldt1(X1,X3)=sdtpldt1(X2,X3))).
% 0.32/5.63 cnf(i_0_210, axiom, (X1!=X2|sdtpldt1(X3,X1)=sdtpldt1(X3,X2))).
% 0.32/5.63 cnf(i_0_211, axiom, (X1!=X2|sdtasasdt0(X1,X3)=sdtasasdt0(X2,X3))).
% 0.32/5.63 cnf(i_0_212, axiom, (X1!=X2|sdtasasdt0(X3,X1)=sdtasasdt0(X3,X2))).
% 0.32/5.63 cnf(i_0_213, axiom, (X1!=X2|~aElementOf0(X1,X3)|aElementOf0(X2,X3))).
% 0.32/5.63 cnf(i_0_214, axiom, (X1!=X2|~aElementOf0(X3,X1)|aElementOf0(X3,X2))).
% 0.32/5.63 cnf(i_0_215, axiom, (X1!=X2|~iLess0(X1,X3)|iLess0(X2,X3))).
% 0.32/5.63 cnf(i_0_216, axiom, (X1!=X2|~iLess0(X3,X1)|iLess0(X3,X2))).
% 0.32/5.63 cnf(i_0_217, axiom, (X1!=X2|~aNaturalNumber0(X1)|aNaturalNumber0(X2))).
% 0.32/5.63 cnf(i_0_218, axiom, (X1!=X2|~aSet0(X1)|aSet0(X2))).
% 0.32/5.63 cnf(i_0_219, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X1,X3,X4)|sdteqdtlpzmzozddtrp0(X2,X3,X4))).
% 0.32/5.63 cnf(i_0_220, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X1,X4)|sdteqdtlpzmzozddtrp0(X3,X2,X4))).
% 0.32/5.63 cnf(i_0_221, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X4,X1)|sdteqdtlpzmzozddtrp0(X3,X4,X2))).
% 0.32/5.63 cnf(i_0_222, axiom, (X1!=X2|~aElement0(X1)|aElement0(X2))).
% 0.32/5.63 cnf(i_0_223, axiom, (X1!=X2|~aIdeal0(X1)|aIdeal0(X2))).
% 0.32/5.63 cnf(i_0_224, axiom, (X1!=X2|~aGcdOfAnd0(X1,X3,X4)|aGcdOfAnd0(X2,X3,X4))).
% 0.32/5.63 cnf(i_0_225, axiom, (X1!=X2|~aGcdOfAnd0(X3,X1,X4)|aGcdOfAnd0(X3,X2,X4))).
% 0.32/5.63 cnf(i_0_226, axiom, (X1!=X2|~aGcdOfAnd0(X3,X4,X1)|aGcdOfAnd0(X3,X4,X2))).
% 0.32/5.63 cnf(i_0_227, axiom, (X1!=X2|~doDivides0(X1,X3)|doDivides0(X2,X3))).
% 0.32/5.63 cnf(i_0_228, axiom, (X1!=X2|~doDivides0(X3,X1)|doDivides0(X3,X2))).
% 0.32/5.63 cnf(i_0_229, axiom, (X1!=X2|~aDivisorOf0(X1,X3)|aDivisorOf0(X2,X3))).
% 0.32/5.63 cnf(i_0_230, axiom, (X1!=X2|~aDivisorOf0(X3,X1)|aDivisorOf0(X3,X2))).
% 0.32/5.63 cnf(i_0_231, axiom, (X1!=X2|~misRelativelyPrime0(X1,X3)|misRelativelyPrime0(X2,X3))).
% 0.32/5.63 cnf(i_0_232, axiom, (X1!=X2|~misRelativelyPrime0(X3,X1)|misRelativelyPrime0(X3,X2))).
% 0.40/5.80 cnf(i_0_193, axiom, (X1=X1)).
% 0.40/5.80 cnf(i_0_194, axiom, (X1=X2|X2!=X1)).
% 0.40/5.80 cnf(i_0_195, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.40/5.80 cnf(i_0_196, axiom, (X1!=X2|sdtpldt0(X1,X3)=sdtpldt0(X2,X3))).
% 0.40/5.80 cnf(i_0_197, axiom, (X1!=X2|sdtpldt0(X3,X1)=sdtpldt0(X3,X2))).
% 0.40/5.80 cnf(i_0_198, axiom, (X1!=X2|esk5_3(X1,X3,X4)=esk5_3(X2,X3,X4))).
% 0.40/5.80 cnf(i_0_199, axiom, (X1!=X2|esk5_3(X3,X1,X4)=esk5_3(X3,X2,X4))).
% 0.40/5.80 cnf(i_0_200, axiom, (X1!=X2|esk5_3(X3,X4,X1)=esk5_3(X3,X4,X2))).
% 0.40/5.80 cnf(i_0_201, axiom, (X1!=X2|sdtasdt0(X1,X3)=sdtasdt0(X2,X3))).
% 0.40/5.80 cnf(i_0_202, axiom, (X1!=X2|sdtasdt0(X3,X1)=sdtasdt0(X3,X2))).
% 0.40/5.80 cnf(i_0_203, axiom, (X1!=X2|smndt0(X1)=smndt0(X2))).
% 0.40/5.80 cnf(i_0_204, axiom, (X1!=X2|slsdtgt0(X1)=slsdtgt0(X2))).
% 0.40/5.80 cnf(i_0_205, axiom, (X1!=X2|esk15_2(X1,X3)=esk15_2(X2,X3))).
% 0.40/5.80 cnf(i_0_206, axiom, (X1!=X2|esk15_2(X3,X1)=esk15_2(X3,X2))).
% 0.40/5.80 cnf(i_0_207, axiom, (X1!=X2|esk19_2(X1,X3)=esk19_2(X2,X3))).
% 0.40/5.80 cnf(i_0_208, axiom, (X1!=X2|esk19_2(X3,X1)=esk19_2(X3,X2))).
% 0.40/5.80 cnf(i_0_209, axiom, (X1!=X2|sdtpldt1(X1,X3)=sdtpldt1(X2,X3))).
% 0.40/5.80 cnf(i_0_210, axiom, (X1!=X2|sdtpldt1(X3,X1)=sdtpldt1(X3,X2))).
% 0.40/5.80 cnf(i_0_211, axiom, (X1!=X2|sdtasasdt0(X1,X3)=sdtasasdt0(X2,X3))).
% 0.40/5.80 cnf(i_0_212, axiom, (X1!=X2|sdtasasdt0(X3,X1)=sdtasasdt0(X3,X2))).
% 0.40/5.80 cnf(i_0_213, axiom, (X1!=X2|~aElementOf0(X1,X3)|aElementOf0(X2,X3))).
% 0.40/5.80 cnf(i_0_214, axiom, (X1!=X2|~aElementOf0(X3,X1)|aElementOf0(X3,X2))).
% 0.40/5.80 cnf(i_0_215, axiom, (X1!=X2|~iLess0(X1,X3)|iLess0(X2,X3))).
% 0.51/5.80 cnf(i_0_216, axiom, (X1!=X2|~iLess0(X3,X1)|iLess0(X3,X2))).
% 0.51/5.80 cnf(i_0_217, axiom, (X1!=X2|~aNaturalNumber0(X1)|aNaturalNumber0(X2))).
% 0.51/5.80 cnf(i_0_218, axiom, (X1!=X2|~aSet0(X1)|aSet0(X2))).
% 0.51/5.80 cnf(i_0_219, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X1,X3,X4)|sdteqdtlpzmzozddtrp0(X2,X3,X4))).
% 0.51/5.80 cnf(i_0_220, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X1,X4)|sdteqdtlpzmzozddtrp0(X3,X2,X4))).
% 0.51/5.80 cnf(i_0_221, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X4,X1)|sdteqdtlpzmzozddtrp0(X3,X4,X2))).
% 0.51/5.80 cnf(i_0_222, axiom, (X1!=X2|~aElement0(X1)|aElement0(X2))).
% 0.51/5.80 cnf(i_0_223, axiom, (X1!=X2|~aIdeal0(X1)|aIdeal0(X2))).
% 0.51/5.80 cnf(i_0_224, axiom, (X1!=X2|~aGcdOfAnd0(X1,X3,X4)|aGcdOfAnd0(X2,X3,X4))).
% 0.51/5.80 cnf(i_0_225, axiom, (X1!=X2|~aGcdOfAnd0(X3,X1,X4)|aGcdOfAnd0(X3,X2,X4))).
% 0.51/5.80 cnf(i_0_226, axiom, (X1!=X2|~aGcdOfAnd0(X3,X4,X1)|aGcdOfAnd0(X3,X4,X2))).
% 0.51/5.80 cnf(i_0_227, axiom, (X1!=X2|~doDivides0(X1,X3)|doDivides0(X2,X3))).
% 0.51/5.80 cnf(i_0_228, axiom, (X1!=X2|~doDivides0(X3,X1)|doDivides0(X3,X2))).
% 0.51/5.80 cnf(i_0_229, axiom, (X1!=X2|~aDivisorOf0(X1,X3)|aDivisorOf0(X2,X3))).
% 0.51/5.80 cnf(i_0_230, axiom, (X1!=X2|~aDivisorOf0(X3,X1)|aDivisorOf0(X3,X2))).
% 0.51/5.80 cnf(i_0_231, axiom, (X1!=X2|~misRelativelyPrime0(X1,X3)|misRelativelyPrime0(X2,X3))).
% 0.51/5.80 cnf(i_0_232, axiom, (X1!=X2|~misRelativelyPrime0(X3,X1)|misRelativelyPrime0(X3,X2))).
% 0.51/5.80 cnf(i_0_233, plain, (~aElementOf0(X1,sdtpldt1(X2,X3))|~aSet0(X2)|~aSet0(X3)|sdtpldt0(esk3_4(X2,X3,sdtpldt1(X2,X3),X1),esk4_4(X2,X3,sdtpldt1(X2,X3),X1))=X1), inference(equality_inference,[],[83])).
% 0.51/5.80 cnf(i_0_234, plain, (~aElementOf0(X1,sdtpldt1(X2,X3))|~aSet0(X2)|~aSet0(X3)|aElementOf0(esk4_4(X2,X3,sdtpldt1(X2,X3),X1),X3)), inference(equality_inference,[],[90])).
% 0.51/5.80 cnf(i_0_235, plain, (~aElementOf0(X1,sdtpldt1(X2,X3))|~aSet0(X2)|~aSet0(X3)|aElementOf0(esk3_4(X2,X3,sdtpldt1(X2,X3),X1),X2)), inference(equality_inference,[],[91])).
% 0.51/5.80 cnf(i_0_236, plain, (~aElementOf0(X1,slsdtgt0(X2))|~aElement0(X2)|sdtasdt0(X2,esk18_3(X2,slsdtgt0(X2),X1))=X1), inference(equality_inference,[],[105])).
% 0.51/5.80 cnf(i_0_237, plain, (~aElementOf0(X1,slsdtgt0(X2))|~aElement0(X2)|aElement0(esk18_3(X2,slsdtgt0(X2),X1))), inference(equality_inference,[],[107])).
% 0.51/5.80 cnf(i_0_238, plain, (~aSet0(X1)|~aSet0(X2)|aElementOf0(X3,sdtasasdt0(X1,X2))|~aElementOf0(X3,X1)|~aElementOf0(X3,X2)), inference(equality_inference,[],[125])).
% 0.51/5.80 cnf(i_0_239, plain, (~aSet0(X1)|~aSet0(X2)|aElementOf0(X3,X1)|~aElementOf0(X3,sdtasasdt0(X1,X2))), inference(equality_inference,[],[132])).
% 0.51/5.80 cnf(i_0_240, plain, (~aSet0(X1)|~aSet0(X2)|aElementOf0(X3,X2)|~aElementOf0(X3,sdtasasdt0(X1,X2))), inference(equality_inference,[],[133])).
% 0.51/5.80 cnf(i_0_241, plain, (~aElement0(X1)|~aElement0(sdtasdt0(X1,X2))|doDivides0(X1,sdtasdt0(X1,X2))|~aElement0(X2)), inference(equality_inference,[],[136])).
% 0.51/5.80 cnf(i_0_242, plain, (~aSet0(X1)|~aSet0(X2)|aSet0(sdtasasdt0(X1,X2))), inference(equality_inference,[],[150])).
% 0.51/5.80 cnf(i_0_243, plain, (~aSet0(X1)|~aSet0(X2)|aSet0(sdtpldt1(X1,X2))), inference(equality_inference,[],[151])).
% 0.51/5.80 cnf(i_0_244, plain, (~aElement0(X1)|aSet0(slsdtgt0(X1))), inference(equality_inference,[],[168])).
% 0.51/5.80 cnf(i_0_245, plain, (aSet0(xI)), inference(scs_inference,[],[i_0_182,i_0_178])).
% 0.51/5.80 cnf(i_0_246, plain, (~aIdeal0(X1)|aSet0(X1)), inference(rename_variables,[],[i_0_178])).
% 0.51/5.80 cnf(i_0_247, plain, (sdtpldt0(sdtasdt0(xa,esk22_0),sdtasdt0(xb,esk23_0))=xu), inference(scs_inference,[],[i_0_138,i_0_182,i_0_178,i_0_194])).
% 0.51/5.80 cnf(i_0_248, plain, (aElement0(xu)), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_178,i_0_194,i_0_157])).
% 0.51/5.80 cnf(i_0_249, plain, (~aElementOf0(X1,X2)|aElement0(X1)|~aSet0(X2)), inference(rename_variables,[],[i_0_157])).
% 0.51/5.80 cnf(i_0_250, plain, (sdtasdt0(xb,esk18_3(xb,slsdtgt0(xb),xb))=xb), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_185,i_0_174,i_0_178,i_0_194,i_0_157,i_0_236])).
% 0.51/5.80 cnf(i_0_251, plain, (~aElement0(X1)|sdtasdt0(X1,esk18_3(X1,slsdtgt0(X1),X2))=X2|~aElementOf0(X2,slsdtgt0(X1))), inference(rename_variables,[],[i_0_236])).
% 0.51/5.80 cnf(i_0_252, plain, (aElement0(esk18_3(xb,slsdtgt0(xb),xb))), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_185,i_0_174,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237])).
% 0.51/5.80 cnf(i_0_253, plain, (~aElement0(X1)|aElement0(esk18_3(X1,slsdtgt0(X1),X2))|~aElementOf0(X2,slsdtgt0(X1))), inference(rename_variables,[],[i_0_237])).
% 0.51/5.80 cnf(i_0_254, plain, (aSet0(sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218])).
% 0.51/5.80 cnf(i_0_255, plain, (aElement0(sdtpldt0(sdtasdt0(xa,esk22_0),sdtasdt0(xb,esk23_0)))), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222])).
% 0.51/5.80 cnf(i_0_256, plain, (aIdeal0(sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))), inference(scs_inference,[],[i_0_138,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223])).
% 0.51/5.80 cnf(i_0_257, plain, (aDivisorOf0(xu,xb)), inference(scs_inference,[],[i_0_138,i_0_179,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223,i_0_139])).
% 0.51/5.80 cnf(i_0_258, plain, (~aElement0(X1)|~doDivides0(X1,X2)|~aElement0(X2)|aDivisorOf0(X1,X2)), inference(rename_variables,[],[i_0_139])).
% 0.51/5.80 cnf(i_0_259, plain, (doDivides0(xb,xb)), inference(scs_inference,[],[i_0_138,i_0_179,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223,i_0_139,i_0_136])).
% 0.51/5.80 cnf(i_0_260, plain, (sdtasdt0(X1,X2)!=X3|~aElement0(X1)|~aElement0(X3)|doDivides0(X1,X3)|~aElement0(X2)), inference(rename_variables,[],[i_0_136])).
% 0.51/5.80 cnf(i_0_261, plain, (aElementOf0(xu,sdtasasdt0(xI,xI))), inference(scs_inference,[],[i_0_138,i_0_179,i_0_181,i_0_182,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223,i_0_139,i_0_136,i_0_238])).
% 0.51/5.80 cnf(i_0_262, plain, (~aElementOf0(X1,X2)|~aElementOf0(X1,X3)|~aSet0(X2)|aElementOf0(X1,sdtasasdt0(X2,X3))|~aSet0(X3)), inference(rename_variables,[],[i_0_238])).
% 0.51/5.80 cnf(i_0_263, plain, (aElement0(X1)|~aDivisorOf0(X1,esk23_0)), inference(scs_inference,[],[i_0_138,i_0_179,i_0_181,i_0_182,i_0_183,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223,i_0_139,i_0_136,i_0_238,i_0_156])).
% 0.51/5.80 cnf(i_0_264, plain, (~aElement0(X1)|aElement0(X2)|~aDivisorOf0(X2,X1)), inference(rename_variables,[],[i_0_156])).
% 0.51/5.80 cnf(i_0_265, plain, (doDivides0(esk23_0,sdtasdt0(esk23_0,esk23_0))|~aDivisorOf0(sdtasdt0(esk23_0,esk23_0),esk23_0)), inference(scs_inference,[],[i_0_138,i_0_179,i_0_181,i_0_182,i_0_183,i_0_185,i_0_174,i_0_167,i_0_178,i_0_194,i_0_157,i_0_236,i_0_237,i_0_218,i_0_222,i_0_223,i_0_139,i_0_136,i_0_238,i_0_156,i_0_241])).
% 0.51/5.80 cnf(i_0_266, plain, (~aElement0(X1)|doDivides0(X2,sdtasdt0(X2,X1))|~aElement0(X2)|~aElement0(sdtasdt0(X2,X1))), inference(rename_variables,[],[i_0_241])).
% 0.51/5.80 cnf(i_0_268, plain, (~aDivisorOf0(xu,xa)), inference(scs_inference,[],[i_0_257,i_0_155])).
% 0.51/5.80 cnf(i_0_269, plain, (xb=sdtasdt0(xb,esk18_3(xb,slsdtgt0(xb),xb))), inference(scs_inference,[],[i_0_250,i_0_194])).
% 0.51/5.80 cnf(i_0_270, plain, (aElement0(esk21_0)), inference(scs_inference,[],[i_0_254,i_0_250,i_0_140,i_0_194,i_0_157])).
% 0.51/5.80 cnf(i_0_271, plain, (~aElementOf0(X1,X2)|aElement0(X1)|~aSet0(X2)), inference(rename_variables,[],[i_0_157])).
% 0.51/5.80 cnf(i_0_272, plain, (sdtasdt0(xa,esk18_3(xa,slsdtgt0(xa),xa))=xa), inference(scs_inference,[],[i_0_254,i_0_250,i_0_186,i_0_175,i_0_140,i_0_194,i_0_157,i_0_236])).
% 0.51/5.80 cnf(i_0_273, plain, (~aElement0(X1)|sdtasdt0(X1,esk18_3(X1,slsdtgt0(X1),X2))=X2|~aElementOf0(X2,slsdtgt0(X1))), inference(rename_variables,[],[i_0_236])).
% 0.51/5.80 cnf(i_0_274, plain, (aElement0(esk18_3(xa,slsdtgt0(xa),xa))), inference(scs_inference,[],[i_0_254,i_0_250,i_0_186,i_0_175,i_0_140,i_0_194,i_0_157,i_0_236,i_0_237])).
% 0.51/5.80 cnf(i_0_275, plain, (~aElement0(X1)|aElement0(esk18_3(X1,slsdtgt0(X1),X2))|~aElementOf0(X2,slsdtgt0(X1))), inference(rename_variables,[],[i_0_237])).
% 0.51/5.80 cnf(i_0_276, plain, (aElement0(sdtasdt0(xb,esk18_3(xb,slsdtgt0(xb),xb)))), inference(scs_inference,[],[i_0_254,i_0_250,i_0_186,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222])).
% 0.51/5.80 cnf(i_0_277, plain, (aDivisorOf0(xu,xa)), inference(scs_inference,[],[i_0_254,i_0_250,i_0_180,i_0_186,i_0_248,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139])).
% 0.51/5.80 cnf(i_0_278, plain, (~aElement0(X1)|~doDivides0(X1,X2)|~aElement0(X2)|aDivisorOf0(X1,X2)), inference(rename_variables,[],[i_0_139])).
% 0.51/5.80 cnf(i_0_279, plain, (doDivides0(xa,xa)), inference(scs_inference,[],[i_0_254,i_0_250,i_0_180,i_0_186,i_0_248,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139,i_0_136])).
% 0.51/5.80 cnf(i_0_280, plain, (sdtasdt0(X1,X2)!=X3|~aElement0(X1)|~aElement0(X3)|doDivides0(X1,X3)|~aElement0(X2)), inference(rename_variables,[],[i_0_136])).
% 0.51/5.80 cnf(i_0_281, plain, (doDivides0(xu,xc)), inference(scs_inference,[],[i_0_254,i_0_250,i_0_141,i_0_180,i_0_186,i_0_248,i_0_257,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139,i_0_136,i_0_103])).
% 0.51/5.80 cnf(i_0_282, plain, (~aGcdOfAnd0(X1,X2,X3)|~aElement0(X2)|~aElement0(X3)|doDivides0(X4,X1)|~aDivisorOf0(X4,X2)|~aDivisorOf0(X4,X3)), inference(rename_variables,[],[i_0_103])).
% 0.51/5.80 cnf(i_0_283, plain, (aElement0(X1)|~aDivisorOf0(X1,esk18_3(xb,slsdtgt0(xb),xb))), inference(scs_inference,[],[i_0_254,i_0_252,i_0_250,i_0_141,i_0_180,i_0_186,i_0_248,i_0_257,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139,i_0_136,i_0_103,i_0_156])).
% 0.51/5.80 cnf(i_0_284, plain, (~aElement0(X1)|aElement0(X2)|~aDivisorOf0(X2,X1)), inference(rename_variables,[],[i_0_156])).
% 0.51/5.80 cnf(i_0_285, plain, (doDivides0(esk22_0,sdtasdt0(esk22_0,esk22_0))|~aDivisorOf0(sdtasdt0(esk22_0,esk22_0),esk18_3(xb,slsdtgt0(xb),xb))), inference(scs_inference,[],[i_0_254,i_0_252,i_0_250,i_0_141,i_0_180,i_0_184,i_0_186,i_0_248,i_0_257,i_0_175,i_0_140,i_0_185,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139,i_0_136,i_0_103,i_0_156,i_0_241])).
% 0.51/5.80 cnf(i_0_286, plain, (~aElement0(X1)|doDivides0(X2,sdtasdt0(X2,X1))|~aElement0(X2)|~aElement0(sdtasdt0(X2,X1))), inference(rename_variables,[],[i_0_241])).
% 0.51/5.80 cnf(i_0_287, plain, (~aDivisorOf0(sdtasdt0(esk22_0,esk22_0),esk18_3(xb,slsdtgt0(xb),xb))|aDivisorOf0(X1,esk18_3(xb,slsdtgt0(xb),xb))|~aGcdOfAnd0(X1,esk18_3(xb,slsdtgt0(xb),xb),esk18_3(xb,slsdtgt0(xb),xb))|sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))!=xI), inference(scs_inference,[],[i_0_254,i_0_256,i_0_252,i_0_250,i_0_261,i_0_141,i_0_180,i_0_184,i_0_186,i_0_245,i_0_248,i_0_257,i_0_175,i_0_140,i_0_185,i_0_167,i_0_194,i_0_157,i_0_236,i_0_237,i_0_222,i_0_139,i_0_136,i_0_103,i_0_156,i_0_241,i_0_195,i_0_218,i_0_223,i_0_239,i_0_240,i_0_119])).
% 0.51/5.80 cnf(i_0_288,plain, ($false), inference(scs_inference,[],[i_0+268, i_0_277]), ['proof']).
% 0.51/5.80 % SZS output end CNFRefutation
% 0.51/5.80 % Total time : 5.284s
%------------------------------------------------------------------------------