%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM455+6 : 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 : n003.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 04:57:24 PM UTC 2026
% Result : Theorem 0.54s 1.62s
% Output : CNFRefutation 0.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM455+6 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % 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.14/0.33 % Computer : n003.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 00:34:56 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.54/1.62 % Version : CSE_E---1.7
% 0.54/1.62 % Problem : theBenchmark.p
% 0.54/1.62 % SZS status Theorem for theBenchmark.p
% 0.54/1.62 % SZS output start CNFRefutation
% 0.54/1.62 fof(m__2144, hypothesis, (((((((((aSet0(sbsmnsldt0(xS))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~(aElementOf0(X1,sbsmnsldt0(xS))))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))=>?[X2]:(((((aInteger0(X2)&X2!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2)))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))))&sdteqdtlpzmzozddtrp0(X3,X1,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))|sdteqdtlpzmzozddtrp0(X3,X1,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)))))&![X3]:(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>aElementOf0(X3,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~(aElementOf0(X1,sbsmnsldt0(xS))))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))=>?[X2]:(((((aInteger0(X2)&X2!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2)))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))))&sdteqdtlpzmzozddtrp0(X3,X1,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))|sdteqdtlpzmzozddtrp0(X3,X1,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)))))&![X3]:(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>aElementOf0(X3,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2144)).
% 0.54/1.62 fof(mComplement, axiom, ![X1]:(aSubsetOf0(X1,cS1395)=>![X2]:(X2=stldt0(X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)<=>(aInteger0(X3)&~(aElementOf0(X3,X1))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mComplement)).
% 0.54/1.62 fof(m__2171, hypothesis, ((((((((aInteger0(xp)&xp!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&![X1]:((aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=>(((aInteger0(X1)&?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(X1,sz10,xp)))&((aInteger0(X1)&(?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10)))|aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|sdteqdtlpzmzozddtrp0(X1,sz10,xp)))=>aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))&aSet0(sbsmnsldt0(xS)))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~(aElementOf0(X1,sbsmnsldt0(xS))))))&![X1]:(aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=>aElementOf0(X1,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2171)).
% 0.54/1.62 fof(m__, conjecture, ?[X1]:(((aInteger0(X1)&(?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10)))|aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|sdteqdtlpzmzozddtrp0(X1,sz10,xp)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&~(((X1=sz10|X1=smndt0(sz10))&aElementOf0(X1,cS2200)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.54/1.62 fof(m__2079, hypothesis, (((((aSet0(sbsmnsldt0(xS))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&aSet0(stldt0(sbsmnsldt0(xS))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~(aElementOf0(X1,sbsmnsldt0(xS))))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(X1=sz10|X1=smndt0(sz10))))&stldt0(sbsmnsldt0(xS))=cS2076), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2079)).
% 0.54/1.62 fof(mIntersection, axiom, ![X1, X2]:((aSubsetOf0(X1,cS1395)&aSubsetOf0(X2,cS1395))=>![X3]:(X3=sdtslmnbsdt0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>((aInteger0(X4)&aElementOf0(X4,X1))&aElementOf0(X4,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntersection)).
% 0.54/1.62 fof(mArSeq, axiom, ![X1, X2]:(((aInteger0(X1)&aInteger0(X2))&X2!=sz00)=>![X3]:(X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aInteger0(X4)&sdteqdtlpzmzozddtrp0(X4,X1,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mArSeq)).
% 0.54/1.62 fof(mUnion, axiom, ![X1, X2]:((aSubsetOf0(X1,cS1395)&aSubsetOf0(X2,cS1395))=>![X3]:(X3=sdtbsmnsldt0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aInteger0(X4)&(aElementOf0(X4,X1)|aElementOf0(X4,X2))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnion)).
% 0.54/1.62 fof(mEquModTrn, axiom, ![X1, X2, X3, X4]:(((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&X3!=sz00)&aInteger0(X4))=>((sdteqdtlpzmzozddtrp0(X1,X2,X3)&sdteqdtlpzmzozddtrp0(X2,X4,X3))=>sdteqdtlpzmzozddtrp0(X1,X4,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEquModTrn)).
% 0.54/1.62 fof(mUnionSet, axiom, ![X1]:((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aSubsetOf0(X2,cS1395)))=>![X2]:(X2=sbsmnsldt0(X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)<=>(aInteger0(X3)&?[X4]:(aElementOf0(X4,X1)&aElementOf0(X3,X4))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnionSet)).
% 0.54/1.62 fof(m__2046, hypothesis, ((aSet0(xS)&![X1]:((aElementOf0(X1,xS)=>?[X2]:(((((aInteger0(X2)&X2!=sz00)&isPrime0(X2))&aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2)))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(sz00))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(X3,sz00,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(sz00)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz00)))|sdteqdtlpzmzozddtrp0(X3,sz00,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2)))))&szAzrzSzezqlpdtcmdtrp0(sz00,X2)=X1))&(?[X2]:(((aInteger0(X2)&X2!=sz00)&isPrime0(X2))&((aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(sz00))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(X3,sz00,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(sz00)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(sz00)))|sdteqdtlpzmzozddtrp0(X3,sz00,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2)))))=>szAzrzSzezqlpdtcmdtrp0(sz00,X2)=X1))=>aElementOf0(X1,xS))))&xS=cS2043), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2046)).
% 0.54/1.62 fof(mEquModMul, axiom, ![X1, X2, X3, X4]:((((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&X3!=sz00)&aInteger0(X4))&X4!=sz00)=>(sdteqdtlpzmzozddtrp0(X1,X2,sdtasdt0(X3,X4))=>(sdteqdtlpzmzozddtrp0(X1,X2,X3)&sdteqdtlpzmzozddtrp0(X1,X2,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEquModMul)).
% 0.54/1.62 fof(mEquModSym, axiom, ![X1, X2, X3]:((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&X3!=sz00)=>(sdteqdtlpzmzozddtrp0(X1,X2,X3)=>sdteqdtlpzmzozddtrp0(X2,X1,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEquModSym)).
% 0.54/1.62 fof(mEquMod, axiom, ![X1, X2, X3]:((((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))&X3!=sz00)=>(sdteqdtlpzmzozddtrp0(X1,X2,X3)<=>aDivisorOf0(X3,sdtpldt0(X1,smndt0(X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEquMod)).
% 0.54/1.62 fof(mOpen, axiom, ![X1]:(aSubsetOf0(X1,cS1395)=>(isOpen0(X1)<=>![X2]:(aElementOf0(X2,X1)=>?[X3]:((aInteger0(X3)&X3!=sz00)&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X2,X3),X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mOpen)).
% 0.54/1.62 fof(mDistrib, axiom, ![X1, X2, X3]:(((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))=>(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X1,X2),X3)=sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDistrib)).
% 0.54/1.62 fof(m__2232, hypothesis, (((((((?[X1]:(aInteger0(X1)&sdtasdt0(xp,X1)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp))&aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&?[X1]:(aInteger0(X1)&sdtasdt0(xp,X1)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp))&aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2232)).
% 0.54/1.62 fof(mMulAsso, axiom, ![X1, X2, X3]:(((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))=>sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(sdtasdt0(X1,X2),X3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulAsso)).
% 0.54/1.62 fof(mAddAsso, axiom, ![X1, X2, X3]:(((aInteger0(X1)&aInteger0(X2))&aInteger0(X3))=>sdtpldt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtpldt0(X1,X2),X3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddAsso)).
% 0.54/1.62 fof(mSubset, axiom, ![X1]:(aSet0(X1)=>![X2]:(aSubsetOf0(X2,X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSubset)).
% 0.54/1.62 fof(mUnionClosed, axiom, ![X1, X2]:((((aSubsetOf0(X1,cS1395)&aSubsetOf0(X2,cS1395))&isClosed0(X1))&isClosed0(X2))=>isClosed0(sdtbsmnsldt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnionClosed)).
% 0.54/1.62 fof(mInterOpen, axiom, ![X1, X2]:((((aSubsetOf0(X1,cS1395)&aSubsetOf0(X2,cS1395))&isOpen0(X1))&isOpen0(X2))=>isOpen0(sdtslmnbsdt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mInterOpen)).
% 0.54/1.62 fof(mUnionSClosed, axiom, ![X1]:(((aSet0(X1)&isFinite0(X1))&![X2]:(aElementOf0(X2,X1)=>(aSubsetOf0(X2,cS1395)&isClosed0(X2))))=>isClosed0(sbsmnsldt0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnionSClosed)).
% 0.54/1.62 fof(mDivisor, axiom, ![X1]:(aInteger0(X1)=>![X2]:(aDivisorOf0(X2,X1)<=>((aInteger0(X2)&X2!=sz00)&?[X3]:(aInteger0(X3)&sdtasdt0(X2,X3)=X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDivisor)).
% 0.54/1.62 fof(mEquModRef, axiom, ![X1, X2]:(((aInteger0(X1)&aInteger0(X2))&X2!=sz00)=>sdteqdtlpzmzozddtrp0(X1,X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEquModRef)).
% 0.54/1.62 fof(mUnionOpen, axiom, ![X1]:((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>(aSubsetOf0(X2,cS1395)&isOpen0(X2))))=>isOpen0(sbsmnsldt0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mUnionOpen)).
% 0.54/1.62 fof(mArSeqClosed, axiom, ![X1, X2]:(((aInteger0(X1)&aInteger0(X2))&X2!=sz00)=>(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),cS1395)&isClosed0(szAzrzSzezqlpdtcmdtrp0(X1,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mArSeqClosed)).
% 0.54/1.62 fof(mIntMult, axiom, ![X1, X2]:((aInteger0(X1)&aInteger0(X2))=>aInteger0(sdtasdt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntMult)).
% 0.54/1.62 fof(mIntPlus, axiom, ![X1, X2]:((aInteger0(X1)&aInteger0(X2))=>aInteger0(sdtpldt0(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntPlus)).
% 0.54/1.62 fof(mPrimeDivisor, axiom, ![X1]:(aInteger0(X1)=>(?[X2]:(aDivisorOf0(X2,X1)&isPrime0(X2))<=>(X1!=sz10&X1!=smndt0(sz10)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mPrimeDivisor)).
% 0.54/1.62 fof(mMulComm, axiom, ![X1, X2]:((aInteger0(X1)&aInteger0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulComm)).
% 0.54/1.62 fof(mAddComm, axiom, ![X1, X2]:((aInteger0(X1)&aInteger0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddComm)).
% 0.54/1.62 fof(mClosed, axiom, ![X1]:(aSubsetOf0(X1,cS1395)=>(isClosed0(X1)<=>isOpen0(stldt0(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mClosed)).
% 0.54/1.62 fof(mZeroDiv, axiom, ![X1, X2]:((aInteger0(X1)&aInteger0(X2))=>(sdtasdt0(X1,X2)=sz00=>(X1=sz00|X2=sz00))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mZeroDiv)).
% 0.54/1.62 fof(mMulMinOne, axiom, ![X1]:(aInteger0(X1)=>(sdtasdt0(smndt0(sz10),X1)=smndt0(X1)&smndt0(X1)=sdtasdt0(X1,smndt0(sz10)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulMinOne)).
% 0.54/1.62 fof(mAddNeg, axiom, ![X1]:(aInteger0(X1)=>(sdtpldt0(X1,smndt0(X1))=sz00&sz00=sdtpldt0(smndt0(X1),X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddNeg)).
% 0.54/1.62 fof(mMulOne, axiom, ![X1]:(aInteger0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulOne)).
% 0.54/1.62 fof(mAddZero, axiom, ![X1]:(aInteger0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mAddZero)).
% 0.54/1.62 fof(mMulZero, axiom, ![X1]:(aInteger0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulZero)).
% 0.54/1.62 fof(mIntNeg, axiom, ![X1]:(aInteger0(X1)=>aInteger0(smndt0(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntNeg)).
% 0.54/1.62 fof(m__2286, hypothesis, (sdtpldt0(sz10,xp)!=smndt0(sz10)|sdtpldt0(sz10,smndt0(xp))!=smndt0(sz10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2286)).
% 0.54/1.62 fof(m__2258, hypothesis, (sdtpldt0(sz10,xp)!=sz10&sdtpldt0(sz10,smndt0(xp))!=sz10), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2258)).
% 0.54/1.62 fof(m__2117, hypothesis, isFinite0(xS), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2117)).
% 0.54/1.62 fof(mIntOne, axiom, aInteger0(sz10), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntOne)).
% 0.54/1.62 fof(mIntZero, axiom, aInteger0(sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntZero)).
% 0.54/1.62 fof(i_0_45, hypothesis, (((((((((aSet0(sbsmnsldt0(xS))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~aElementOf0(X1,sbsmnsldt0(xS)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))=>?[X2]:(((((aInteger0(X2)&X2!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2)))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))))&sdteqdtlpzmzozddtrp0(X3,X1,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))|sdteqdtlpzmzozddtrp0(X3,X1,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)))))&![X3]:(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>aElementOf0(X3,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~aElementOf0(X1,sbsmnsldt0(xS)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))=>?[X2]:(((((aInteger0(X2)&X2!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2)))&![X3]:((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>(((aInteger0(X3)&?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1))))&aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))))&sdteqdtlpzmzozddtrp0(X3,X1,X2)))&((aInteger0(X3)&(?[X4]:(aInteger0(X4)&sdtasdt0(X2,X4)=sdtpldt0(X3,smndt0(X1)))|aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))|sdteqdtlpzmzozddtrp0(X3,X1,X2)))=>aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)))))&![X3]:(aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))=>aElementOf0(X3,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS)))))), inference(fof_simplification,[status(thm)],[m__2144])).
% 0.54/1.62 fof(i_0_46, plain, ![X1]:(aSubsetOf0(X1,cS1395)=>![X2]:(X2=stldt0(X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)<=>(aInteger0(X3)&~aElementOf0(X3,X1)))))), inference(fof_simplification,[status(thm)],[mComplement])).
% 0.54/1.62 fof(i_0_47, hypothesis, ((((((((aInteger0(xp)&xp!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&![X1]:((aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=>(((aInteger0(X1)&?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(X1,sz10,xp)))&((aInteger0(X1)&(?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10)))|aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|sdteqdtlpzmzozddtrp0(X1,sz10,xp)))=>aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))&aSet0(sbsmnsldt0(xS)))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~aElementOf0(X1,sbsmnsldt0(xS)))))&![X1]:(aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=>aElementOf0(X1,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))), inference(fof_simplification,[status(thm)],[m__2171])).
% 0.54/1.62 fof(i_0_48, negated_conjecture, ~(?[X1]:(((aInteger0(X1)&(?[X2]:(aInteger0(X2)&sdtasdt0(xp,X2)=sdtpldt0(X1,smndt0(sz10)))|aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|sdteqdtlpzmzozddtrp0(X1,sz10,xp)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&~(((X1=sz10|X1=smndt0(sz10))&aElementOf0(X1,cS2200))))), inference(assume_negation,[status(cth)],[m__])).
% 0.54/1.62 fof(i_0_49, hypothesis, (((((aSet0(sbsmnsldt0(xS))&![X1]:(aElementOf0(X1,sbsmnsldt0(xS))<=>(aInteger0(X1)&?[X2]:(aElementOf0(X2,xS)&aElementOf0(X1,X2)))))&aSet0(stldt0(sbsmnsldt0(xS))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(X1)&~aElementOf0(X1,sbsmnsldt0(xS)))))&![X1]:(aElementOf0(X1,stldt0(sbsmnsldt0(xS)))<=>(X1=sz10|X1=smndt0(sz10))))&stldt0(sbsmnsldt0(xS))=cS2076), inference(fof_simplification,[status(thm)],[m__2079])).
% 0.54/1.62 fof(i_0_50, plain, ![X197, X198, X199, X200, X201, X202]:(((aSet0(X199)|X199!=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))&((((aInteger0(X200)|~aElementOf0(X200,X199)|X199!=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))&(aElementOf0(X200,X197)|~aElementOf0(X200,X199)|X199!=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395))))&(aElementOf0(X200,X198)|~aElementOf0(X200,X199)|X199!=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395))))&(~aInteger0(X201)|~aElementOf0(X201,X197)|~aElementOf0(X201,X198)|aElementOf0(X201,X199)|X199!=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))))&((~aElementOf0(esk5_3(X197,X198,X202),X202)|(~aInteger0(esk5_3(X197,X198,X202))|~aElementOf0(esk5_3(X197,X198,X202),X197)|~aElementOf0(esk5_3(X197,X198,X202),X198))|~aSet0(X202)|X202=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))&(((aInteger0(esk5_3(X197,X198,X202))|aElementOf0(esk5_3(X197,X198,X202),X202)|~aSet0(X202)|X202=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))&(aElementOf0(esk5_3(X197,X198,X202),X197)|aElementOf0(esk5_3(X197,X198,X202),X202)|~aSet0(X202)|X202=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395))))&(aElementOf0(esk5_3(X197,X198,X202),X198)|aElementOf0(esk5_3(X197,X198,X202),X202)|~aSet0(X202)|X202=sdtslmnbsdt0(X197,X198)|(~aSubsetOf0(X197,cS1395)|~aSubsetOf0(X198,cS1395)))))), 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)],[mIntersection])])])])])])).
% 0.54/1.62 fof(i_0_51, plain, ![X221, X222, X223, X224, X225, X226]:(((aSet0(X223)|X223!=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))&(((aInteger0(X224)|~aElementOf0(X224,X223)|X223!=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))&(sdteqdtlpzmzozddtrp0(X224,X221,X222)|~aElementOf0(X224,X223)|X223!=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00)))&(~aInteger0(X225)|~sdteqdtlpzmzozddtrp0(X225,X221,X222)|aElementOf0(X225,X223)|X223!=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))))&((~aElementOf0(esk11_3(X221,X222,X226),X226)|(~aInteger0(esk11_3(X221,X222,X226))|~sdteqdtlpzmzozddtrp0(esk11_3(X221,X222,X226),X221,X222))|~aSet0(X226)|X226=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))&((aInteger0(esk11_3(X221,X222,X226))|aElementOf0(esk11_3(X221,X222,X226),X226)|~aSet0(X226)|X226=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))&(sdteqdtlpzmzozddtrp0(esk11_3(X221,X222,X226),X221,X222)|aElementOf0(esk11_3(X221,X222,X226),X226)|~aSet0(X226)|X226=szAzrzSzezqlpdtcmdtrp0(X221,X222)|(~aInteger0(X221)|~aInteger0(X222)|X222=sz00))))), 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)],[mArSeq])])])])])])).
% 0.54/1.62 fof(i_0_52, plain, ![X190, X191, X192, X193, X194, X195]:(((aSet0(X192)|X192!=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))&(((aInteger0(X193)|~aElementOf0(X193,X192)|X192!=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))&(aElementOf0(X193,X190)|aElementOf0(X193,X191)|~aElementOf0(X193,X192)|X192!=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395))))&((~aElementOf0(X194,X190)|~aInteger0(X194)|aElementOf0(X194,X192)|X192!=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))&(~aElementOf0(X194,X191)|~aInteger0(X194)|aElementOf0(X194,X192)|X192!=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395))))))&(((~aElementOf0(esk4_3(X190,X191,X195),X190)|~aInteger0(esk4_3(X190,X191,X195))|~aElementOf0(esk4_3(X190,X191,X195),X195)|~aSet0(X195)|X195=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))&(~aElementOf0(esk4_3(X190,X191,X195),X191)|~aInteger0(esk4_3(X190,X191,X195))|~aElementOf0(esk4_3(X190,X191,X195),X195)|~aSet0(X195)|X195=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395))))&((aInteger0(esk4_3(X190,X191,X195))|aElementOf0(esk4_3(X190,X191,X195),X195)|~aSet0(X195)|X195=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))&(aElementOf0(esk4_3(X190,X191,X195),X190)|aElementOf0(esk4_3(X190,X191,X195),X191)|aElementOf0(esk4_3(X190,X191,X195),X195)|~aSet0(X195)|X195=sdtbsmnsldt0(X190,X191)|(~aSubsetOf0(X190,cS1395)|~aSubsetOf0(X191,cS1395)))))), 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)],[mUnion])])])])])])).
% 0.54/1.62 fof(i_0_53, plain, ![X174, X175, X176, X177]:(~aInteger0(X174)|~aInteger0(X175)|~aInteger0(X176)|X176=sz00|~aInteger0(X177)|(~sdteqdtlpzmzozddtrp0(X174,X175,X176)|~sdteqdtlpzmzozddtrp0(X175,X177,X176)|sdteqdtlpzmzozddtrp0(X174,X177,X176))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEquModTrn])])).
% 0.54/1.62 fof(i_0_54, plain, ![X204, X206, X207, X209, X210, X211, X213]:((((aSet0(X206)|X206!=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&(((aInteger0(X207)|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&((aElementOf0(esk7_3(X204,X206,X207),X204)|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&(aElementOf0(X207,esk7_3(X204,X206,X207))|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))))&(~aInteger0(X209)|(~aElementOf0(X210,X204)|~aElementOf0(X209,X210))|aElementOf0(X209,X206)|X206!=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))))&((~aElementOf0(esk8_2(X204,X211),X211)|(~aInteger0(esk8_2(X204,X211))|(~aElementOf0(X213,X204)|~aElementOf0(esk8_2(X204,X211),X213)))|~aSet0(X211)|X211=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&((aInteger0(esk8_2(X204,X211))|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&((aElementOf0(esk9_2(X204,X211),X204)|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))&(aElementOf0(esk8_2(X204,X211),esk9_2(X204,X211))|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(aElementOf0(esk6_1(X204),X204)|~aSet0(X204)))))))&(((aSet0(X206)|X206!=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&(((aInteger0(X207)|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&((aElementOf0(esk7_3(X204,X206,X207),X204)|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&(aElementOf0(X207,esk7_3(X204,X206,X207))|~aElementOf0(X207,X206)|X206!=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))))&(~aInteger0(X209)|(~aElementOf0(X210,X204)|~aElementOf0(X209,X210))|aElementOf0(X209,X206)|X206!=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))))&((~aElementOf0(esk8_2(X204,X211),X211)|(~aInteger0(esk8_2(X204,X211))|(~aElementOf0(X213,X204)|~aElementOf0(esk8_2(X204,X211),X213)))|~aSet0(X211)|X211=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&((aInteger0(esk8_2(X204,X211))|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&((aElementOf0(esk9_2(X204,X211),X204)|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))&(aElementOf0(esk8_2(X204,X211),esk9_2(X204,X211))|aElementOf0(esk8_2(X204,X211),X211)|~aSet0(X211)|X211=sbsmnsldt0(X204)|(~aSubsetOf0(esk6_1(X204),cS1395)|~aSet0(X204)))))))), 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)],[mUnionSet])])])])])])).
% 0.54/1.62 fof(i_0_55, hypothesis, ![X244, X246, X248, X249, X250, X251, X252, X254, X255]:((aSet0(xS)&(((((((aInteger0(esk16_1(X244))|~aElementOf0(X244,xS))&(esk16_1(X244)!=sz00|~aElementOf0(X244,xS)))&(isPrime0(esk16_1(X244))|~aElementOf0(X244,xS)))&(aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS)))&(((((aInteger0(X246)|~aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS))&((aInteger0(esk17_2(X244,X246))|~aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS))&(sdtasdt0(esk16_1(X244),esk17_2(X244,X246))=sdtpldt0(X246,smndt0(sz00))|~aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS))))&(aDivisorOf0(esk16_1(X244),sdtpldt0(X246,smndt0(sz00)))|~aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS)))&(sdteqdtlpzmzozddtrp0(X246,sz00,esk16_1(X244))|~aElementOf0(X246,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS)))&(((~aInteger0(X249)|sdtasdt0(esk16_1(X244),X249)!=sdtpldt0(X248,smndt0(sz00))|~aInteger0(X248)|aElementOf0(X248,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS))&(~aDivisorOf0(esk16_1(X244),sdtpldt0(X248,smndt0(sz00)))|~aInteger0(X248)|aElementOf0(X248,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS)))&(~sdteqdtlpzmzozddtrp0(X248,sz00,esk16_1(X244))|~aInteger0(X248)|aElementOf0(X248,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244)))|~aElementOf0(X244,xS)))))&(szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X244))=X244|~aElementOf0(X244,xS)))&(((aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS))&(((((aInteger0(X252)|~aElementOf0(X252,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS))&((aInteger0(esk18_3(X250,X251,X252))|~aElementOf0(X252,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS))&(sdtasdt0(X251,esk18_3(X250,X251,X252))=sdtpldt0(X252,smndt0(sz00))|~aElementOf0(X252,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS))))&(aDivisorOf0(X251,sdtpldt0(X252,smndt0(sz00)))|~aElementOf0(X252,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS)))&(sdteqdtlpzmzozddtrp0(X252,sz00,X251)|~aElementOf0(X252,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS)))&(((~aInteger0(X255)|sdtasdt0(X251,X255)!=sdtpldt0(X254,smndt0(sz00))|~aInteger0(X254)|aElementOf0(X254,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS))&(~aDivisorOf0(X251,sdtpldt0(X254,smndt0(sz00)))|~aInteger0(X254)|aElementOf0(X254,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS)))&(~sdteqdtlpzmzozddtrp0(X254,sz00,X251)|~aInteger0(X254)|aElementOf0(X254,szAzrzSzezqlpdtcmdtrp0(sz00,X251))|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS)))))&(szAzrzSzezqlpdtcmdtrp0(sz00,X251)!=X250|(~aInteger0(X251)|X251=sz00|~isPrime0(X251))|aElementOf0(X250,xS)))))&xS=cS2043), 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)],[m__2046])])])])])])).
% 0.54/1.62 fof(i_0_56, plain, ![X178, X179, X180, X181]:((sdteqdtlpzmzozddtrp0(X178,X179,X180)|~sdteqdtlpzmzozddtrp0(X178,X179,sdtasdt0(X180,X181))|(~aInteger0(X178)|~aInteger0(X179)|~aInteger0(X180)|X180=sz00|~aInteger0(X181)|X181=sz00))&(sdteqdtlpzmzozddtrp0(X178,X179,X181)|~sdteqdtlpzmzozddtrp0(X178,X179,sdtasdt0(X180,X181))|(~aInteger0(X178)|~aInteger0(X179)|~aInteger0(X180)|X180=sz00|~aInteger0(X181)|X181=sz00))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEquModMul])])])).
% 0.54/1.62 fof(i_0_57, hypothesis, ![X262, X264, X265, X266, X267, X269, X271, X272, X273, X274, X276, X277, X278, X279, X281, X283, X284, X285]:(((((((((aSet0(sbsmnsldt0(xS))&(((aInteger0(X262)|~aElementOf0(X262,sbsmnsldt0(xS)))&((aElementOf0(esk20_1(X262),xS)|~aElementOf0(X262,sbsmnsldt0(xS)))&(aElementOf0(X262,esk20_1(X262))|~aElementOf0(X262,sbsmnsldt0(xS)))))&(~aInteger0(X264)|(~aElementOf0(X265,xS)|~aElementOf0(X264,X265))|aElementOf0(X264,sbsmnsldt0(xS)))))&(((aInteger0(X266)|~aElementOf0(X266,stldt0(sbsmnsldt0(xS))))&(~aElementOf0(X266,sbsmnsldt0(xS))|~aElementOf0(X266,stldt0(sbsmnsldt0(xS)))))&(~aInteger0(X266)|aElementOf0(X266,sbsmnsldt0(xS))|aElementOf0(X266,stldt0(sbsmnsldt0(xS))))))&((((((aInteger0(esk21_1(X267))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))&(esk21_1(X267)!=sz00|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(aSet0(szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(((((aInteger0(X269)|~aElementOf0(X269,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))&((aInteger0(esk22_2(X267,X269))|~aElementOf0(X269,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))&(sdtasdt0(esk21_1(X267),esk22_2(X267,X269))=sdtpldt0(X269,smndt0(X267))|~aElementOf0(X269,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))))&(aDivisorOf0(esk21_1(X267),sdtpldt0(X269,smndt0(X267)))|~aElementOf0(X269,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(sdteqdtlpzmzozddtrp0(X269,X267,esk21_1(X267))|~aElementOf0(X269,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(((~aInteger0(X272)|sdtasdt0(esk21_1(X267),X272)!=sdtpldt0(X271,smndt0(X267))|~aInteger0(X271)|aElementOf0(X271,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))&(~aDivisorOf0(esk21_1(X267),sdtpldt0(X271,smndt0(X267)))|~aInteger0(X271)|aElementOf0(X271,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(~sdteqdtlpzmzozddtrp0(X271,X267,esk21_1(X267))|~aInteger0(X271)|aElementOf0(X271,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))))&(~aElementOf0(X273,szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)))|aElementOf0(X273,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS)))))&(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X267,esk21_1(X267)),stldt0(sbsmnsldt0(xS)))|~aElementOf0(X267,stldt0(sbsmnsldt0(xS))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(((aInteger0(X274)|~aElementOf0(X274,sbsmnsldt0(xS)))&((aElementOf0(esk23_1(X274),xS)|~aElementOf0(X274,sbsmnsldt0(xS)))&(aElementOf0(X274,esk23_1(X274))|~aElementOf0(X274,sbsmnsldt0(xS)))))&(~aInteger0(X276)|(~aElementOf0(X277,xS)|~aElementOf0(X276,X277))|aElementOf0(X276,sbsmnsldt0(xS)))))&(((aInteger0(X278)|~aElementOf0(X278,stldt0(sbsmnsldt0(xS))))&(~aElementOf0(X278,sbsmnsldt0(xS))|~aElementOf0(X278,stldt0(sbsmnsldt0(xS)))))&(~aInteger0(X278)|aElementOf0(X278,sbsmnsldt0(xS))|aElementOf0(X278,stldt0(sbsmnsldt0(xS))))))&((((((aInteger0(esk24_1(X279))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS))))&(esk24_1(X279)!=sz00|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(aSet0(szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(((((aInteger0(X281)|~aElementOf0(X281,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS))))&((aInteger0(esk25_2(X279,X281))|~aElementOf0(X281,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS))))&(sdtasdt0(esk24_1(X279),esk25_2(X279,X281))=sdtpldt0(X281,smndt0(X279))|~aElementOf0(X281,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS))))))&(aDivisorOf0(esk24_1(X279),sdtpldt0(X281,smndt0(X279)))|~aElementOf0(X281,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(sdteqdtlpzmzozddtrp0(X281,X279,esk24_1(X279))|~aElementOf0(X281,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(((~aInteger0(X284)|sdtasdt0(esk24_1(X279),X284)!=sdtpldt0(X283,smndt0(X279))|~aInteger0(X283)|aElementOf0(X283,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS))))&(~aDivisorOf0(esk24_1(X279),sdtpldt0(X283,smndt0(X279)))|~aInteger0(X283)|aElementOf0(X283,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(~sdteqdtlpzmzozddtrp0(X283,X279,esk24_1(X279))|~aInteger0(X283)|aElementOf0(X283,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))))&(~aElementOf0(X285,szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)))|aElementOf0(X285,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))&(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X279,esk24_1(X279)),stldt0(sbsmnsldt0(xS)))|~aElementOf0(X279,stldt0(sbsmnsldt0(xS)))))), 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)],[i_0_45])])])])])])).
% 0.54/1.62 fof(i_0_58, plain, ![X215, X216, X217, X218, X219]:(((aSet0(X216)|X216!=stldt0(X215)|~aSubsetOf0(X215,cS1395))&(((aInteger0(X217)|~aElementOf0(X217,X216)|X216!=stldt0(X215)|~aSubsetOf0(X215,cS1395))&(~aElementOf0(X217,X215)|~aElementOf0(X217,X216)|X216!=stldt0(X215)|~aSubsetOf0(X215,cS1395)))&(~aInteger0(X218)|aElementOf0(X218,X215)|aElementOf0(X218,X216)|X216!=stldt0(X215)|~aSubsetOf0(X215,cS1395))))&((~aElementOf0(esk10_2(X215,X219),X219)|(~aInteger0(esk10_2(X215,X219))|aElementOf0(esk10_2(X215,X219),X215))|~aSet0(X219)|X219=stldt0(X215)|~aSubsetOf0(X215,cS1395))&((aInteger0(esk10_2(X215,X219))|aElementOf0(esk10_2(X215,X219),X219)|~aSet0(X219)|X219=stldt0(X215)|~aSubsetOf0(X215,cS1395))&(~aElementOf0(esk10_2(X215,X219),X215)|aElementOf0(esk10_2(X215,X219),X219)|~aSet0(X219)|X219=stldt0(X215)|~aSubsetOf0(X215,cS1395))))), 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)],[i_0_46])])])])])])).
% 0.54/1.62 fof(i_0_59, plain, ![X171, X172, X173]:(~aInteger0(X171)|~aInteger0(X172)|~aInteger0(X173)|X173=sz00|(~sdteqdtlpzmzozddtrp0(X171,X172,X173)|sdteqdtlpzmzozddtrp0(X172,X171,X173))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEquModSym])])).
% 0.54/1.62 fof(i_0_60, plain, ![X166, X167, X168]:((~sdteqdtlpzmzozddtrp0(X166,X167,X168)|aDivisorOf0(X168,sdtpldt0(X166,smndt0(X167)))|(~aInteger0(X166)|~aInteger0(X167)|~aInteger0(X168)|X168=sz00))&(~aDivisorOf0(X168,sdtpldt0(X166,smndt0(X167)))|sdteqdtlpzmzozddtrp0(X166,X167,X168)|(~aInteger0(X166)|~aInteger0(X167)|~aInteger0(X168)|X168=sz00))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEquMod])])])).
% 0.54/1.62 fof(i_0_61, plain, ![X228, X229, X232]:((((aInteger0(esk12_2(X228,X229))|~aElementOf0(X229,X228)|~isOpen0(X228)|~aSubsetOf0(X228,cS1395))&(esk12_2(X228,X229)!=sz00|~aElementOf0(X229,X228)|~isOpen0(X228)|~aSubsetOf0(X228,cS1395)))&(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X229,esk12_2(X228,X229)),X228)|~aElementOf0(X229,X228)|~isOpen0(X228)|~aSubsetOf0(X228,cS1395)))&((aElementOf0(esk13_1(X228),X228)|isOpen0(X228)|~aSubsetOf0(X228,cS1395))&(~aInteger0(X232)|X232=sz00|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk13_1(X228),X232),X228)|isOpen0(X228)|~aSubsetOf0(X228,cS1395)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mOpen])])])])])).
% 0.54/1.62 fof(i_0_62, plain, ![X154, X155, X156]:((sdtasdt0(X154,sdtpldt0(X155,X156))=sdtpldt0(sdtasdt0(X154,X155),sdtasdt0(X154,X156))|(~aInteger0(X154)|~aInteger0(X155)|~aInteger0(X156)))&(sdtasdt0(sdtpldt0(X154,X155),X156)=sdtpldt0(sdtasdt0(X154,X156),sdtasdt0(X155,X156))|(~aInteger0(X154)|~aInteger0(X155)|~aInteger0(X156)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistrib])])])).
% 0.54/1.62 fof(i_0_63, hypothesis, ![X286, X288, X289, X290, X292, X293, X294, X295]:((((((((aInteger0(xp)&xp!=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(((((aInteger0(X286)|~aElementOf0(X286,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((aInteger0(esk26_1(X286))|~aElementOf0(X286,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(sdtasdt0(xp,esk26_1(X286))=sdtpldt0(X286,smndt0(sz10))|~aElementOf0(X286,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))&(aDivisorOf0(xp,sdtpldt0(X286,smndt0(sz10)))|~aElementOf0(X286,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))&(sdteqdtlpzmzozddtrp0(X286,sz10,xp)|~aElementOf0(X286,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))&(((~aInteger0(X289)|sdtasdt0(xp,X289)!=sdtpldt0(X288,smndt0(sz10))|~aInteger0(X288)|aElementOf0(X288,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(~aDivisorOf0(xp,sdtpldt0(X288,smndt0(sz10)))|~aInteger0(X288)|aElementOf0(X288,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))&(~sdteqdtlpzmzozddtrp0(X288,sz10,xp)|~aInteger0(X288)|aElementOf0(X288,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&(((aInteger0(X290)|~aElementOf0(X290,sbsmnsldt0(xS)))&((aElementOf0(esk27_1(X290),xS)|~aElementOf0(X290,sbsmnsldt0(xS)))&(aElementOf0(X290,esk27_1(X290))|~aElementOf0(X290,sbsmnsldt0(xS)))))&(~aInteger0(X292)|(~aElementOf0(X293,xS)|~aElementOf0(X292,X293))|aElementOf0(X292,sbsmnsldt0(xS)))))&(((aInteger0(X294)|~aElementOf0(X294,stldt0(sbsmnsldt0(xS))))&(~aElementOf0(X294,sbsmnsldt0(xS))|~aElementOf0(X294,stldt0(sbsmnsldt0(xS)))))&(~aInteger0(X294)|aElementOf0(X294,sbsmnsldt0(xS))|aElementOf0(X294,stldt0(sbsmnsldt0(xS))))))&(~aElementOf0(X295,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(X295,stldt0(sbsmnsldt0(xS)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))), 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)],[i_0_47])])])])])])).
% 0.54/1.62 fof(i_0_64, hypothesis, ((((((((aInteger0(esk28_0)&sdtasdt0(xp,esk28_0)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp))&aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(aInteger0(esk29_0)&sdtasdt0(xp,esk29_0)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp))&aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[m__2232])])).
% 0.54/1.62 fof(i_0_65, plain, ![X148, X149, X150]:(~aInteger0(X148)|~aInteger0(X149)|~aInteger0(X150)|sdtasdt0(X148,sdtasdt0(X149,X150))=sdtasdt0(sdtasdt0(X148,X149),X150)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulAsso])])).
% 0.54/1.62 fof(i_0_66, plain, ![X141, X142, X143]:(~aInteger0(X141)|~aInteger0(X142)|~aInteger0(X143)|sdtpldt0(X141,sdtpldt0(X142,X143))=sdtpldt0(sdtpldt0(X141,X142),X143)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddAsso])])).
% 0.54/1.62 fof(i_0_67, negated_conjecture, ![X298, X299]:(((((X298=sz10|X298=smndt0(sz10)|(~aInteger0(X299)|sdtasdt0(xp,X299)!=sdtpldt0(X298,smndt0(sz10))|~aInteger0(X298)))&(aElementOf0(X298,cS2200)|(~aInteger0(X299)|sdtasdt0(xp,X299)!=sdtpldt0(X298,smndt0(sz10))|~aInteger0(X298))))&((X298=sz10|X298=smndt0(sz10)|(~aDivisorOf0(xp,sdtpldt0(X298,smndt0(sz10)))|~aInteger0(X298)))&(aElementOf0(X298,cS2200)|(~aDivisorOf0(xp,sdtpldt0(X298,smndt0(sz10)))|~aInteger0(X298)))))&((X298=sz10|X298=smndt0(sz10)|(~sdteqdtlpzmzozddtrp0(X298,sz10,xp)|~aInteger0(X298)))&(aElementOf0(X298,cS2200)|(~sdteqdtlpzmzozddtrp0(X298,sz10,xp)|~aInteger0(X298)))))&((X298=sz10|X298=smndt0(sz10)|~aElementOf0(X298,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(aElementOf0(X298,cS2200)|~aElementOf0(X298,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])])])).
% 0.54/1.62 fof(i_0_68, plain, ![X185, X186, X187, X188]:(((aSet0(X186)|~aSubsetOf0(X186,X185)|~aSet0(X185))&(~aElementOf0(X187,X186)|aElementOf0(X187,X185)|~aSubsetOf0(X186,X185)|~aSet0(X185)))&((aElementOf0(esk3_2(X185,X188),X188)|~aSet0(X188)|aSubsetOf0(X188,X185)|~aSet0(X185))&(~aElementOf0(esk3_2(X185,X188),X185)|~aSet0(X188)|aSubsetOf0(X188,X185)|~aSet0(X185)))), 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)],[mSubset])])])])])])).
% 0.54/1.62 fof(i_0_69, plain, ![X238, X239]:(~aSubsetOf0(X238,cS1395)|~aSubsetOf0(X239,cS1395)|~isClosed0(X238)|~isClosed0(X239)|isClosed0(sdtbsmnsldt0(X238,X239))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mUnionClosed])])).
% 0.54/1.62 fof(i_0_70, plain, ![X236, X237]:(~aSubsetOf0(X236,cS1395)|~aSubsetOf0(X237,cS1395)|~isOpen0(X236)|~isOpen0(X237)|isOpen0(sdtslmnbsdt0(X236,X237))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mInterOpen])])).
% 0.54/1.62 fof(i_0_71, plain, ![X240]:((aElementOf0(esk15_1(X240),X240)|(~aSet0(X240)|~isFinite0(X240))|isClosed0(sbsmnsldt0(X240)))&(~aSubsetOf0(esk15_1(X240),cS1395)|~isClosed0(esk15_1(X240))|(~aSet0(X240)|~isFinite0(X240))|isClosed0(sbsmnsldt0(X240)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mUnionSClosed])])])])).
% 0.54/1.62 fof(i_0_72, plain, ![X161, X162, X164, X165]:((((aInteger0(X162)|~aDivisorOf0(X162,X161)|~aInteger0(X161))&(X162!=sz00|~aDivisorOf0(X162,X161)|~aInteger0(X161)))&((aInteger0(esk1_2(X161,X162))|~aDivisorOf0(X162,X161)|~aInteger0(X161))&(sdtasdt0(X162,esk1_2(X161,X162))=X161|~aDivisorOf0(X162,X161)|~aInteger0(X161))))&(~aInteger0(X164)|X164=sz00|(~aInteger0(X165)|sdtasdt0(X164,X165)!=X161)|aDivisorOf0(X164,X161)|~aInteger0(X161))), 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)],[mDivisor])])])])])])).
% 0.54/1.62 fof(i_0_73, plain, ![X169, X170]:(~aInteger0(X169)|~aInteger0(X170)|X170=sz00|sdteqdtlpzmzozddtrp0(X169,X169,X170)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEquModRef])])).
% 0.54/1.62 fof(i_0_74, hypothesis, ![X256, X258, X259, X260, X261]:(((((aSet0(sbsmnsldt0(xS))&(((aInteger0(X256)|~aElementOf0(X256,sbsmnsldt0(xS)))&((aElementOf0(esk19_1(X256),xS)|~aElementOf0(X256,sbsmnsldt0(xS)))&(aElementOf0(X256,esk19_1(X256))|~aElementOf0(X256,sbsmnsldt0(xS)))))&(~aInteger0(X258)|(~aElementOf0(X259,xS)|~aElementOf0(X258,X259))|aElementOf0(X258,sbsmnsldt0(xS)))))&aSet0(stldt0(sbsmnsldt0(xS))))&(((aInteger0(X260)|~aElementOf0(X260,stldt0(sbsmnsldt0(xS))))&(~aElementOf0(X260,sbsmnsldt0(xS))|~aElementOf0(X260,stldt0(sbsmnsldt0(xS)))))&(~aInteger0(X260)|aElementOf0(X260,sbsmnsldt0(xS))|aElementOf0(X260,stldt0(sbsmnsldt0(xS))))))&((~aElementOf0(X261,stldt0(sbsmnsldt0(xS)))|(X261=sz10|X261=smndt0(sz10)))&((X261!=sz10|aElementOf0(X261,stldt0(sbsmnsldt0(xS))))&(X261!=smndt0(sz10)|aElementOf0(X261,stldt0(sbsmnsldt0(xS)))))))&stldt0(sbsmnsldt0(xS))=cS2076), 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)],[i_0_49])])])])])])).
% 0.54/1.62 fof(i_0_75, plain, ![X234]:((aElementOf0(esk14_1(X234),X234)|~aSet0(X234)|isOpen0(sbsmnsldt0(X234)))&(~aSubsetOf0(esk14_1(X234),cS1395)|~isOpen0(esk14_1(X234))|~aSet0(X234)|isOpen0(sbsmnsldt0(X234)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mUnionOpen])])])])).
% 0.54/1.62 fof(i_0_76, plain, ![X242, X243]:((aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X242,X243),cS1395)|(~aInteger0(X242)|~aInteger0(X243)|X243=sz00))&(isClosed0(szAzrzSzezqlpdtcmdtrp0(X242,X243))|(~aInteger0(X242)|~aInteger0(X243)|X243=sz00))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mArSeqClosed])])])).
% 0.54/1.62 fof(i_0_77, plain, ![X139, X140]:(~aInteger0(X139)|~aInteger0(X140)|aInteger0(sdtasdt0(X139,X140))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIntMult])])).
% 0.54/1.62 fof(i_0_78, plain, ![X137, X138]:(~aInteger0(X137)|~aInteger0(X138)|aInteger0(sdtpldt0(X137,X138))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIntPlus])])).
% 0.54/1.62 fof(i_0_79, plain, ![X182, X183]:(((X182!=sz10|(~aDivisorOf0(X183,X182)|~isPrime0(X183))|~aInteger0(X182))&(X182!=smndt0(sz10)|(~aDivisorOf0(X183,X182)|~isPrime0(X183))|~aInteger0(X182)))&((aDivisorOf0(esk2_1(X182),X182)|(X182=sz10|X182=smndt0(sz10))|~aInteger0(X182))&(isPrime0(esk2_1(X182))|(X182=sz10|X182=smndt0(sz10))|~aInteger0(X182)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mPrimeDivisor])])])])])).
% 0.54/1.62 fof(i_0_80, plain, ![X151, X152]:(~aInteger0(X151)|~aInteger0(X152)|sdtasdt0(X151,X152)=sdtasdt0(X152,X151)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulComm])])).
% 0.54/1.62 fof(i_0_81, plain, ![X144, X145]:(~aInteger0(X144)|~aInteger0(X145)|sdtpldt0(X144,X145)=sdtpldt0(X145,X144)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddComm])])).
% 0.54/1.62 fof(i_0_82, plain, ![X233]:((~isClosed0(X233)|isOpen0(stldt0(X233))|~aSubsetOf0(X233,cS1395))&(~isOpen0(stldt0(X233))|isClosed0(X233)|~aSubsetOf0(X233,cS1395))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mClosed])])])).
% 0.54/1.62 fof(i_0_83, plain, ![X159, X160]:(~aInteger0(X159)|~aInteger0(X160)|(sdtasdt0(X159,X160)!=sz00|(X159=sz00|X160=sz00))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroDiv])])).
% 0.54/1.62 fof(i_0_84, plain, ![X158]:((sdtasdt0(smndt0(sz10),X158)=smndt0(X158)|~aInteger0(X158))&(smndt0(X158)=sdtasdt0(X158,smndt0(sz10))|~aInteger0(X158))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulMinOne])])])).
% 0.54/1.62 fof(i_0_85, plain, ![X147]:((sdtpldt0(X147,smndt0(X147))=sz00|~aInteger0(X147))&(sz00=sdtpldt0(smndt0(X147),X147)|~aInteger0(X147))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddNeg])])])).
% 0.54/1.62 fof(i_0_86, plain, ![X153]:((sdtasdt0(X153,sz10)=X153|~aInteger0(X153))&(X153=sdtasdt0(sz10,X153)|~aInteger0(X153))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulOne])])])).
% 0.54/1.62 fof(i_0_87, plain, ![X146]:((sdtpldt0(X146,sz00)=X146|~aInteger0(X146))&(X146=sdtpldt0(sz00,X146)|~aInteger0(X146))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddZero])])])).
% 0.54/1.62 fof(i_0_88, plain, ![X157]:((sdtasdt0(X157,sz00)=sz00|~aInteger0(X157))&(sz00=sdtasdt0(sz00,X157)|~aInteger0(X157))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulZero])])])).
% 0.54/1.62 fof(i_0_89, plain, ![X136]:(~aInteger0(X136)|aInteger0(smndt0(X136))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIntNeg])])).
% 0.54/1.62 cnf(i_0_90, plain, (X3=sdtslmnbsdt0(X1,X2)|~aElementOf0(esk5_3(X1,X2,X3),X3)|~aInteger0(esk5_3(X1,X2,X3))|~aElementOf0(esk5_3(X1,X2,X3),X1)|~aElementOf0(esk5_3(X1,X2,X3),X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_91, plain, (X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)|X2=sz00|~aElementOf0(esk11_3(X1,X2,X3),X3)|~aInteger0(esk11_3(X1,X2,X3))|~sdteqdtlpzmzozddtrp0(esk11_3(X1,X2,X3),X1,X2)|~aSet0(X3)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_92, plain, (X3=sdtbsmnsldt0(X1,X2)|~aElementOf0(esk4_3(X1,X2,X3),X1)|~aInteger0(esk4_3(X1,X2,X3))|~aElementOf0(esk4_3(X1,X2,X3),X3)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_93, plain, (X3=sdtbsmnsldt0(X1,X2)|~aElementOf0(esk4_3(X1,X2,X3),X2)|~aInteger0(esk4_3(X1,X2,X3))|~aElementOf0(esk4_3(X1,X2,X3),X3)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_94, plain, (aElementOf0(esk4_3(X1,X2,X3),X1)|aElementOf0(esk4_3(X1,X2,X3),X2)|aElementOf0(esk4_3(X1,X2,X3),X3)|X3=sdtbsmnsldt0(X1,X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_95, plain, (sdteqdtlpzmzozddtrp0(esk11_3(X1,X2,X3),X1,X2)|aElementOf0(esk11_3(X1,X2,X3),X3)|X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)|X2=sz00|~aSet0(X3)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_96, plain, (aElementOf0(esk5_3(X1,X2,X3),X1)|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtslmnbsdt0(X1,X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_97, plain, (aElementOf0(esk5_3(X1,X2,X3),X2)|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtslmnbsdt0(X1,X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_98, plain, (aInteger0(esk5_3(X1,X2,X3))|aElementOf0(esk5_3(X1,X2,X3),X3)|X3=sdtslmnbsdt0(X1,X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_99, plain, (aInteger0(esk4_3(X1,X2,X3))|aElementOf0(esk4_3(X1,X2,X3),X3)|X3=sdtbsmnsldt0(X1,X2)|~aSet0(X3)|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_100, plain, (aInteger0(esk11_3(X1,X2,X3))|aElementOf0(esk11_3(X1,X2,X3),X3)|X3=szAzrzSzezqlpdtcmdtrp0(X1,X2)|X2=sz00|~aSet0(X3)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_101, plain, (X3=sz00|sdteqdtlpzmzozddtrp0(X1,X4,X3)|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X4)|~sdteqdtlpzmzozddtrp0(X1,X2,X3)|~sdteqdtlpzmzozddtrp0(X2,X4,X3)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.54/1.62 cnf(i_0_102, plain, (X2=sbsmnsldt0(X1)|~aElementOf0(esk8_2(X1,X2),X2)|~aInteger0(esk8_2(X1,X2))|~aElementOf0(X3,X1)|~aElementOf0(esk8_2(X1,X2),X3)|~aSet0(X2)|~aSubsetOf0(esk6_1(X1),cS1395)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_103, plain, (X2=sbsmnsldt0(X1)|aElementOf0(esk6_1(X1),X1)|~aElementOf0(esk8_2(X1,X2),X2)|~aInteger0(esk8_2(X1,X2))|~aElementOf0(X3,X1)|~aElementOf0(esk8_2(X1,X2),X3)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_104, hypothesis, (sdtasdt0(X1,esk18_3(X2,X1,X3))=sdtpldt0(X3,smndt0(sz00))|X1=sz00|aElementOf0(X2,xS)|~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X1))|~aInteger0(X1)|~isPrime0(X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_105, plain, (sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00|X4=sz00|~sdteqdtlpzmzozddtrp0(X1,X2,sdtasdt0(X3,X4))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X4)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.54/1.62 cnf(i_0_106, plain, (sdteqdtlpzmzozddtrp0(X1,X2,X3)|X4=sz00|X3=sz00|~sdteqdtlpzmzozddtrp0(X1,X2,sdtasdt0(X4,X3))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X4)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.54/1.62 cnf(i_0_107, hypothesis, (aInteger0(esk18_3(X1,X2,X3))|X2=sz00|aElementOf0(X1,xS)|~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|~aInteger0(X2)|~isPrime0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_108, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk24_1(X2)))|~sdteqdtlpzmzozddtrp0(X1,X2,esk24_1(X2))|~aInteger0(X1)|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_109, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk21_1(X2)))|~sdteqdtlpzmzozddtrp0(X1,X2,esk21_1(X2))|~aInteger0(X1)|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_110, hypothesis, (aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|~aDivisorOf0(esk24_1(X1),sdtpldt0(X2,smndt0(X1)))|~aInteger0(X2)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_111, hypothesis, (aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|~aDivisorOf0(esk21_1(X1),sdtpldt0(X2,smndt0(X1)))|~aInteger0(X2)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_112, hypothesis, (sdtasdt0(esk24_1(X1),esk25_2(X1,X2))=sdtpldt0(X2,smndt0(X1))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_113, hypothesis, (sdtasdt0(esk21_1(X1),esk22_2(X1,X2))=sdtpldt0(X2,smndt0(X1))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_114, plain, (aElementOf0(esk7_3(X1,X2,X3),X1)|~aElementOf0(X3,X2)|X2!=sbsmnsldt0(X1)|~aSubsetOf0(esk6_1(X1),cS1395)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_115, plain, (aElementOf0(X1,esk7_3(X2,X3,X1))|~aElementOf0(X1,X3)|X3!=sbsmnsldt0(X2)|~aSubsetOf0(esk6_1(X2),cS1395)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_116, hypothesis, (sdteqdtlpzmzozddtrp0(X1,X2,esk24_1(X2))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk24_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_117, hypothesis, (sdteqdtlpzmzozddtrp0(X1,X2,esk21_1(X2))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk21_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_118, plain, (aElementOf0(esk10_2(X1,X2),X1)|X2=stldt0(X1)|~aElementOf0(esk10_2(X1,X2),X2)|~aInteger0(esk10_2(X1,X2))|~aSet0(X2)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_119, hypothesis, (aDivisorOf0(esk24_1(X1),sdtpldt0(X2,smndt0(X1)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_120, hypothesis, (aDivisorOf0(esk21_1(X1),sdtpldt0(X2,smndt0(X1)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_121, plain, (aElementOf0(esk7_3(X1,X2,X3),X1)|aElementOf0(esk6_1(X1),X1)|~aElementOf0(X3,X2)|X2!=sbsmnsldt0(X1)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_122, plain, (aElementOf0(X1,esk7_3(X2,X3,X1))|aElementOf0(esk6_1(X2),X2)|~aElementOf0(X1,X3)|X3!=sbsmnsldt0(X2)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_123, hypothesis, (aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X2,esk24_1(X2)))|~aInteger0(X1)|sdtasdt0(esk24_1(X2),X1)!=sdtpldt0(X3,smndt0(X2))|~aInteger0(X3)|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_124, hypothesis, (aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X2,esk21_1(X2)))|~aInteger0(X1)|sdtasdt0(esk21_1(X2),X1)!=sdtpldt0(X3,smndt0(X2))|~aInteger0(X3)|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_125, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X2)))|~sdteqdtlpzmzozddtrp0(X1,sz00,esk16_1(X2))|~aInteger0(X1)|~aElementOf0(X2,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_126, plain, (X3=sz00|sdteqdtlpzmzozddtrp0(X2,X1,X3)|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)|~sdteqdtlpzmzozddtrp0(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.54/1.62 cnf(i_0_127, plain, (aDivisorOf0(X3,sdtpldt0(X1,smndt0(X2)))|X3=sz00|~sdteqdtlpzmzozddtrp0(X1,X2,X3)|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.54/1.62 cnf(i_0_128, hypothesis, (sdtasdt0(esk16_1(X1),esk17_2(X1,X2))=sdtpldt0(X2,smndt0(sz00))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1)))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_129, plain, (sdteqdtlpzmzozddtrp0(X2,X3,X1)|X1=sz00|~aDivisorOf0(X1,sdtpldt0(X2,smndt0(X3)))|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.54/1.62 cnf(i_0_130, hypothesis, (aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1)))|~aDivisorOf0(esk16_1(X1),sdtpldt0(X2,smndt0(sz00)))|~aInteger0(X2)|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_131, hypothesis, (sdteqdtlpzmzozddtrp0(X1,sz00,esk16_1(X2))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X2)))|~aElementOf0(X2,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_132, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|X2=sz00|aElementOf0(X3,xS)|~sdteqdtlpzmzozddtrp0(X1,sz00,X2)|~aInteger0(X1)|~aInteger0(X2)|~isPrime0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_133, plain, (aElementOf0(esk8_2(X1,X2),esk9_2(X1,X2))|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|~aSet0(X2)|~aSubsetOf0(esk6_1(X1),cS1395)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_134, hypothesis, (aInteger0(esk25_2(X1,X2))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_135, hypothesis, (aInteger0(esk22_2(X1,X2))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_136, hypothesis, (aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk24_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_137, hypothesis, (aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk21_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_138, hypothesis, (aDivisorOf0(esk16_1(X1),sdtpldt0(X2,smndt0(sz00)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1)))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_139, plain, (aElementOf0(X1,X4)|X3=sz00|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,X2,X3)|X4!=szAzrzSzezqlpdtcmdtrp0(X2,X3)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_140, plain, (aElementOf0(esk8_2(X1,X2),esk9_2(X1,X2))|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|aElementOf0(esk6_1(X1),X1)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_141, hypothesis, (aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))|X1=sz00|aElementOf0(X3,xS)|~aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))|~aInteger0(X2)|~aInteger0(X1)|~isPrime0(X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_142, hypothesis, (aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X2)))|~aInteger0(X1)|sdtasdt0(esk16_1(X2),X1)!=sdtpldt0(X3,smndt0(sz00))|~aInteger0(X3)|~aElementOf0(X2,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_143, plain, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,esk12_2(X2,X1)),X2)|~aElementOf0(X1,X2)|~isOpen0(X2)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.54/1.62 cnf(i_0_144, hypothesis, (sdteqdtlpzmzozddtrp0(X1,sz00,X2)|X2=sz00|aElementOf0(X3,xS)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|~aInteger0(X2)|~isPrime0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_145, plain, (aElementOf0(esk10_2(X1,X2),X2)|X2=stldt0(X1)|~aElementOf0(esk10_2(X1,X2),X1)|~aSet0(X2)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_146, hypothesis, (aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))|X1=sz00|aElementOf0(X3,xS)|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))|~aInteger0(X1)|~isPrime0(X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_147, plain, (aElementOf0(X1,X4)|~aInteger0(X1)|~aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X4!=sdtslmnbsdt0(X2,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_148, plain, (aElementOf0(esk9_2(X1,X2),X1)|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|~aSet0(X2)|~aSubsetOf0(esk6_1(X1),cS1395)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_149, hypothesis, (aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|X2=sz00|aElementOf0(X4,xS)|~aInteger0(X1)|sdtasdt0(X2,X1)!=sdtpldt0(X3,smndt0(sz00))|~aInteger0(X3)|~aInteger0(X2)|~isPrime0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_150, hypothesis, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk24_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_151, hypothesis, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,esk21_1(X2)))|~aElementOf0(X2,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_152, hypothesis, (aInteger0(esk17_2(X1,X2))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1)))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_153, plain, (sdtasdt0(sdtpldt0(X1,X2),X3)=sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.54/1.62 cnf(i_0_154, plain, (sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.54/1.62 cnf(i_0_155, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|~sdteqdtlpzmzozddtrp0(X1,sz10,xp)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_156, plain, (aElementOf0(esk9_2(X1,X2),X1)|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|aElementOf0(esk6_1(X1),X1)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_157, plain, (aInteger0(esk8_2(X1,X2))|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|~aSet0(X2)|~aSubsetOf0(esk6_1(X1),cS1395)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_158, plain, (sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00|~aElementOf0(X1,X4)|X4!=szAzrzSzezqlpdtcmdtrp0(X2,X3)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_159, plain, (aElementOf0(X1,X2)|aElementOf0(X1,X3)|~aElementOf0(X1,X4)|X4!=sdtbsmnsldt0(X2,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_160, plain, (X1=sz00|isOpen0(X2)|~aInteger0(X1)|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk13_1(X2),X1),X2)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.54/1.62 cnf(i_0_161, plain, (aElementOf0(X1,X4)|~aInteger0(X1)|~aElementOf0(X2,X3)|~aElementOf0(X1,X2)|X4!=sbsmnsldt0(X3)|~aSubsetOf0(esk6_1(X3),cS1395)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_162, hypothesis, (aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_163, plain, (aInteger0(esk8_2(X1,X2))|aElementOf0(esk8_2(X1,X2),X2)|X2=sbsmnsldt0(X1)|aElementOf0(esk6_1(X1),X1)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_164, plain, (aElementOf0(X1,X3)|~aElementOf0(X1,X2)|~aInteger0(X1)|X3!=sdtbsmnsldt0(X2,X4)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X4,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_165, plain, (aElementOf0(X1,X3)|~aElementOf0(X1,X2)|~aInteger0(X1)|X3!=sdtbsmnsldt0(X4,X2)|~aSubsetOf0(X4,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_166, hypothesis, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)),stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_167, hypothesis, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)),stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_168, hypothesis, (sdteqdtlpzmzozddtrp0(X1,sz10,xp)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_169, plain, (aInteger0(esk10_2(X1,X2))|aElementOf0(esk10_2(X1,X2),X2)|X2=stldt0(X1)|~aSet0(X2)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_170, plain, (aElementOf0(X1,X4)|aElementOf0(esk6_1(X3),X3)|~aInteger0(X1)|~aElementOf0(X2,X3)|~aElementOf0(X1,X2)|X4!=sbsmnsldt0(X3)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_171, hypothesis, (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_172, hypothesis, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X2)))|~aElementOf0(X2,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_173, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X3!=sdtslmnbsdt0(X2,X4)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X4,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_174, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X3!=sdtslmnbsdt0(X4,X2)|~aSubsetOf0(X4,cS1395)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_175, plain, (sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(sdtasdt0(X1,X2),X3)|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.54/1.62 cnf(i_0_176, plain, (sdtpldt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtpldt0(X1,X2),X3)|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.54/1.62 cnf(i_0_177, negated_conjecture, (aElementOf0(X1,cS2200)|~sdteqdtlpzmzozddtrp0(X1,sz10,xp)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_178, hypothesis, (aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_179, hypothesis, (aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|~aInteger0(X1)|sdtasdt0(xp,X1)!=sdtpldt0(X2,smndt0(sz10))|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_180, negated_conjecture, (X1=sz10|X1=smndt0(sz10)|~sdteqdtlpzmzozddtrp0(X1,sz10,xp)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_181, plain, (aSubsetOf0(X2,X1)|~aElementOf0(esk3_2(X1,X2),X1)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.54/1.62 cnf(i_0_182, hypothesis, (aInteger0(X1)|X2=sz00|aElementOf0(X3,xS)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|~aInteger0(X2)|~isPrime0(X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_183, plain, (aInteger0(X1)|~aElementOf0(X1,X2)|X2!=sdtslmnbsdt0(X3,X4)|~aSubsetOf0(X3,cS1395)|~aSubsetOf0(X4,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_184, plain, (aInteger0(X1)|~aElementOf0(X1,X2)|X2!=sdtbsmnsldt0(X3,X4)|~aSubsetOf0(X3,cS1395)|~aSubsetOf0(X4,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_185, negated_conjecture, (aElementOf0(X1,cS2200)|~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_186, hypothesis, (sdtasdt0(xp,esk26_1(X1))=sdtpldt0(X1,smndt0(sz10))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_187, plain, (isClosed0(sdtbsmnsldt0(X1,X2))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)|~isClosed0(X1)|~isClosed0(X2)), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 0.54/1.62 cnf(i_0_188, plain, (isOpen0(sdtslmnbsdt0(X1,X2))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)|~isOpen0(X1)|~isOpen0(X2)), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.54/1.62 cnf(i_0_189, hypothesis, (aSet0(szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_190, hypothesis, (aSet0(szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_191, hypothesis, (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_192, negated_conjecture, (X1=sz10|X1=smndt0(sz10)|~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_193, plain, (aInteger0(esk12_2(X1,X2))|~aElementOf0(X2,X1)|~isOpen0(X1)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.54/1.62 cnf(i_0_194, hypothesis, (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_195, hypothesis, (aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_196, plain, (~aElementOf0(X1,X2)|~aElementOf0(X1,X3)|X3!=stldt0(X2)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_197, negated_conjecture, (aElementOf0(X1,cS2200)|~aInteger0(X2)|sdtasdt0(xp,X2)!=sdtpldt0(X1,smndt0(sz10))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_198, plain, (esk12_2(X1,X2)!=sz00|~aElementOf0(X2,X1)|~isOpen0(X1)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.54/1.62 cnf(i_0_199, plain, (aInteger0(X1)|~aElementOf0(X1,X2)|X2!=sbsmnsldt0(X3)|~aSubsetOf0(esk6_1(X3),cS1395)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_200, plain, (isClosed0(sbsmnsldt0(X1))|~aSubsetOf0(esk15_1(X1),cS1395)|~isClosed0(esk15_1(X1))|~aSet0(X1)|~isFinite0(X1)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.54/1.62 cnf(i_0_201, hypothesis, (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_202, plain, (sdtasdt0(X1,esk1_2(X2,X1))=X2|~aDivisorOf0(X1,X2)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.54/1.62 cnf(i_0_203, plain, (X2=sz00|sdteqdtlpzmzozddtrp0(X1,X1,X2)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.54/1.62 cnf(i_0_204, hypothesis, (~aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_205, hypothesis, (~aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_206, hypothesis, (~aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_207, hypothesis, (~aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_208, plain, (aSet0(X1)|X1!=sdtslmnbsdt0(X2,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.54/1.62 cnf(i_0_209, plain, (aSet0(X1)|X1!=sdtbsmnsldt0(X2,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.54/1.62 cnf(i_0_210, plain, (aElementOf0(esk3_2(X1,X2),X2)|aSubsetOf0(X2,X1)|~aSet0(X2)|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.54/1.62 cnf(i_0_211, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|~aInteger0(X1)|~aElementOf0(X2,xS)|~aElementOf0(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_212, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|~aInteger0(X1)|~aElementOf0(X2,xS)|~aElementOf0(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_213, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|~aInteger0(X1)|~aElementOf0(X2,xS)|~aElementOf0(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_214, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|~aInteger0(X1)|~aElementOf0(X2,xS)|~aElementOf0(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_215, plain, (aInteger0(X1)|X4=sz00|~aElementOf0(X1,X2)|X2!=szAzrzSzezqlpdtcmdtrp0(X3,X4)|~aInteger0(X3)|~aInteger0(X4)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_216, plain, (aElementOf0(X1,X3)|~aElementOf0(X1,X2)|~aSubsetOf0(X2,X3)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.54/1.62 cnf(i_0_217, negated_conjecture, (aElementOf0(X1,cS2200)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_218, negated_conjecture, (X1=sz10|X1=smndt0(sz10)|~aInteger0(X2)|sdtasdt0(xp,X2)!=sdtpldt0(X1,smndt0(sz10))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_219, plain, (aElementOf0(X1,X2)|aElementOf0(X1,X3)|~aInteger0(X1)|X3!=stldt0(X2)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_220, plain, (isOpen0(sbsmnsldt0(X1))|~aSubsetOf0(esk14_1(X1),cS1395)|~isOpen0(esk14_1(X1))|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.54/1.62 cnf(i_0_221, hypothesis, (aInteger0(esk26_1(X1))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_222, plain, (aInteger0(X1)|aElementOf0(esk6_1(X3),X3)|~aElementOf0(X1,X2)|X2!=sbsmnsldt0(X3)|~aSet0(X3)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_223, hypothesis, (aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_224, plain, (X1=sz00|aDivisorOf0(X1,X3)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X1,X2)!=X3|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.54/1.62 cnf(i_0_225, plain, (aInteger0(esk1_2(X1,X2))|~aDivisorOf0(X2,X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.54/1.62 cnf(i_0_226, hypothesis, (aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1)))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_227, negated_conjecture, (X1=sz10|X1=smndt0(sz10)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.54/1.62 cnf(i_0_228, hypothesis, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_229, hypothesis, (sdtasdt0(xp,esk29_0)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_230, hypothesis, (aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))|X1=sz00|aElementOf0(X2,xS)|~aInteger0(X1)|~isPrime0(X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_231, plain, (aInteger0(X1)|~aElementOf0(X1,X2)|X2!=stldt0(X3)|~aSubsetOf0(X3,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_232, plain, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),cS1395)|X2=sz00|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.54/1.62 cnf(i_0_233, hypothesis, (aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_234, hypothesis, (aInteger0(esk24_1(X1))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_235, hypothesis, (aInteger0(esk21_1(X1))|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_236, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_237, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_238, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_239, hypothesis, (aElementOf0(X1,sbsmnsldt0(xS))|aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_240, hypothesis, (X1=sz00|aElementOf0(X2,xS)|szAzrzSzezqlpdtcmdtrp0(sz00,X1)!=X2|~aInteger0(X1)|~isPrime0(X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_241, hypothesis, (sdtpldt0(sz10,xp)!=smndt0(sz10)|sdtpldt0(sz10,smndt0(xp))!=smndt0(sz10)), inference(split_conjunct,[status(thm)],[m__2286]), ['final']).
% 0.54/1.62 cnf(i_0_242, plain, (aSet0(X1)|X1!=sbsmnsldt0(X2)|~aSubsetOf0(esk6_1(X2),cS1395)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_243, hypothesis, (esk24_1(X1)!=sz00|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_244, hypothesis, (esk21_1(X1)!=sz00|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_245, hypothesis, (aElementOf0(X1,esk27_1(X1))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_246, hypothesis, (aElementOf0(X1,esk23_1(X1))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_247, hypothesis, (aElementOf0(X1,esk20_1(X1))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_248, hypothesis, (aElementOf0(X1,esk19_1(X1))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_249, hypothesis, (sdtasdt0(xp,esk28_0)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_250, hypothesis, (X1=sz10|X1=smndt0(sz10)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_251, hypothesis, (aElementOf0(esk27_1(X1),xS)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_252, hypothesis, (aElementOf0(esk23_1(X1),xS)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_253, hypothesis, (aElementOf0(esk20_1(X1),xS)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_254, hypothesis, (aElementOf0(esk19_1(X1),xS)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_255, hypothesis, (aInteger0(X1)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_256, hypothesis, (aInteger0(X1)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_257, hypothesis, (aInteger0(X1)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_258, hypothesis, (aInteger0(X1)|~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_259, hypothesis, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_260, plain, (isClosed0(szAzrzSzezqlpdtcmdtrp0(X1,X2))|X2=sz00|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.54/1.62 cnf(i_0_261, plain, (aElementOf0(esk15_1(X1),X1)|isClosed0(sbsmnsldt0(X1))|~aSet0(X1)|~isFinite0(X1)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.54/1.62 cnf(i_0_262, plain, (aElementOf0(esk13_1(X1),X1)|isOpen0(X1)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.54/1.62 cnf(i_0_263, plain, (aInteger0(sdtasdt0(X1,X2))|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.54/1.62 cnf(i_0_264, plain, (aInteger0(sdtpldt0(X1,X2))|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_78]), ['final']).
% 0.54/1.62 cnf(i_0_265, plain, (aSet0(X1)|X3=sz00|X1!=szAzrzSzezqlpdtcmdtrp0(X2,X3)|~aInteger0(X2)|~aInteger0(X3)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.54/1.62 cnf(i_0_266, plain, (X1!=smndt0(sz10)|~aDivisorOf0(X2,X1)|~isPrime0(X2)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.54/1.62 cnf(i_0_267, plain, (sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 0.54/1.62 cnf(i_0_268, plain, (sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aInteger0(X1)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 0.54/1.62 cnf(i_0_269, plain, (isClosed0(X1)|~isOpen0(stldt0(X1))|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 0.54/1.62 cnf(i_0_270, plain, (aSet0(X1)|aElementOf0(esk6_1(X2),X2)|X1!=sbsmnsldt0(X2)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.54/1.62 cnf(i_0_271, plain, (X1=sz00|X2=sz00|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X1,X2)!=sz00), inference(split_conjunct,[status(thm)],[i_0_83]), ['final']).
% 0.54/1.62 cnf(i_0_272, hypothesis, (szAzrzSzezqlpdtcmdtrp0(sz00,esk16_1(X1))=X1|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_273, plain, (X1!=sz10|~aDivisorOf0(X2,X1)|~isPrime0(X2)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.54/1.62 cnf(i_0_274, plain, (aElementOf0(esk14_1(X1),X1)|isOpen0(sbsmnsldt0(X1))|~aSet0(X1)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.54/1.62 cnf(i_0_275, plain, (isOpen0(stldt0(X1))|~isClosed0(X1)|~aSubsetOf0(X1,cS1395)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 0.54/1.62 cnf(i_0_276, plain, (aSet0(X1)|~aSubsetOf0(X1,X2)|~aSet0(X2)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.54/1.62 cnf(i_0_277, plain, (aInteger0(X1)|~aDivisorOf0(X1,X2)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.54/1.62 cnf(i_0_278, plain, (aSet0(X1)|X1!=stldt0(X2)|~aSubsetOf0(X2,cS1395)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.54/1.62 cnf(i_0_279, plain, (aDivisorOf0(esk2_1(X1),X1)|X1=sz10|X1=smndt0(sz10)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.54/1.62 cnf(i_0_280, hypothesis, (aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|X1!=smndt0(sz10)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_281, plain, (X1!=sz00|~aDivisorOf0(X1,X2)|~aInteger0(X2)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.54/1.62 cnf(i_0_282, hypothesis, (aInteger0(X1)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_283, hypothesis, (aInteger0(X1)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_284, hypothesis, (aInteger0(X1)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_285, hypothesis, (aInteger0(X1)|~aElementOf0(X1,sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_286, hypothesis, (isPrime0(esk16_1(X1))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_287, hypothesis, (aInteger0(esk16_1(X1))|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_288, hypothesis, (aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|X1!=sz10), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_289, plain, (sdtasdt0(smndt0(sz10),X1)=smndt0(X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_84]), ['final']).
% 0.54/1.62 cnf(i_0_290, plain, (smndt0(X1)=sdtasdt0(X1,smndt0(sz10))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_84]), ['final']).
% 0.54/1.62 cnf(i_0_291, plain, (sdtpldt0(X1,smndt0(X1))=sz00|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 0.54/1.62 cnf(i_0_292, plain, (sz00=sdtpldt0(smndt0(X1),X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 0.54/1.62 cnf(i_0_293, hypothesis, (esk16_1(X1)!=sz00|~aElementOf0(X1,xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_294, hypothesis, (sdtpldt0(sz10,smndt0(xp))!=sz10), inference(split_conjunct,[status(thm)],[m__2258]), ['final']).
% 0.54/1.62 cnf(i_0_295, hypothesis, (aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_296, plain, (isPrime0(esk2_1(X1))|X1=sz10|X1=smndt0(sz10)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.54/1.62 cnf(i_0_297, plain, (sdtasdt0(X1,sz10)=X1|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_86]), ['final']).
% 0.54/1.62 cnf(i_0_298, plain, (sdtpldt0(X1,sz00)=X1|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_87]), ['final']).
% 0.54/1.62 cnf(i_0_299, plain, (X1=sdtasdt0(sz10,X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_86]), ['final']).
% 0.54/1.62 cnf(i_0_300, plain, (X1=sdtpldt0(sz00,X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_87]), ['final']).
% 0.54/1.62 cnf(i_0_301, plain, (sdtasdt0(X1,sz00)=sz00|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_88]), ['final']).
% 0.54/1.62 cnf(i_0_302, plain, (sz00=sdtasdt0(sz00,X1)|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_88]), ['final']).
% 0.54/1.62 cnf(i_0_303, hypothesis, (sdtpldt0(sz10,xp)!=sz10), inference(split_conjunct,[status(thm)],[m__2258]), ['final']).
% 0.54/1.62 cnf(i_0_304, plain, (aInteger0(smndt0(X1))|~aInteger0(X1)), inference(split_conjunct,[status(thm)],[i_0_89]), ['final']).
% 0.54/1.62 cnf(i_0_305, hypothesis, (isOpen0(stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_306, hypothesis, (aSet0(stldt0(sbsmnsldt0(xS)))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_307, hypothesis, (isClosed0(sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_308, hypothesis, (aSet0(sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_309, hypothesis, (aSet0(sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_310, hypothesis, (aSet0(sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.54/1.62 cnf(i_0_311, hypothesis, (aSet0(sbsmnsldt0(xS))), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_312, hypothesis, (stldt0(sbsmnsldt0(xS))=cS2076), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.54/1.62 cnf(i_0_313, hypothesis, (isFinite0(xS)), inference(split_conjunct,[status(thm)],[m__2117]), ['final']).
% 0.54/1.62 cnf(i_0_314, hypothesis, (aSet0(xS)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_315, hypothesis, (aInteger0(esk29_0)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_316, hypothesis, (aInteger0(esk28_0)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.54/1.62 cnf(i_0_317, hypothesis, (aInteger0(xp)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_318, plain, (aInteger0(sz10)), inference(split_conjunct,[status(thm)],[mIntOne]), ['final']).
% 0.54/1.62 cnf(i_0_319, plain, (aInteger0(sz00)), inference(split_conjunct,[status(thm)],[mIntZero]), ['final']).
% 0.54/1.62 cnf(i_0_320, hypothesis, (xp!=sz00), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.54/1.62 cnf(i_0_321, hypothesis, (xS=cS2043), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.54/1.62 cnf(i_0_322, axiom, (X1=X1)).
% 0.54/1.62 cnf(i_0_323, axiom, (X1=X2|X2!=X1)).
% 0.54/1.62 cnf(i_0_324, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.54/1.62 cnf(i_0_325, axiom, (X1!=X2|sdtslmnbsdt0(X1,X3)=sdtslmnbsdt0(X2,X3))).
% 0.54/1.62 cnf(i_0_326, axiom, (X1!=X2|sdtslmnbsdt0(X3,X1)=sdtslmnbsdt0(X3,X2))).
% 0.54/1.62 cnf(i_0_327, axiom, (X1!=X2|sdtasdt0(X1,X3)=sdtasdt0(X2,X3))).
% 0.54/1.62 cnf(i_0_328, axiom, (X1!=X2|sdtasdt0(X3,X1)=sdtasdt0(X3,X2))).
% 0.54/1.62 cnf(i_0_329, axiom, (X1!=X2|sdtpldt0(X1,X3)=sdtpldt0(X2,X3))).
% 0.54/1.62 cnf(i_0_330, axiom, (X1!=X2|sdtpldt0(X3,X1)=sdtpldt0(X3,X2))).
% 0.54/1.62 cnf(i_0_331, axiom, (X1!=X2|smndt0(X1)=smndt0(X2))).
% 0.54/1.62 cnf(i_0_332, axiom, (X1!=X2|esk24_1(X1)=esk24_1(X2))).
% 0.54/1.62 cnf(i_0_333, axiom, (X1!=X2|stldt0(X1)=stldt0(X2))).
% 0.54/1.62 cnf(i_0_334, axiom, (X1!=X2|esk21_1(X1)=esk21_1(X2))).
% 0.54/1.62 cnf(i_0_335, axiom, (X1!=X2|esk16_1(X1)=esk16_1(X2))).
% 0.54/1.62 cnf(i_0_336, axiom, (X1!=X2|esk12_2(X1,X3)=esk12_2(X2,X3))).
% 0.54/1.62 cnf(i_0_337, axiom, (X1!=X2|esk12_2(X3,X1)=esk12_2(X3,X2))).
% 0.54/1.62 cnf(i_0_338, axiom, (X1!=X2|szAzrzSzezqlpdtcmdtrp0(X1,X3)=szAzrzSzezqlpdtcmdtrp0(X2,X3))).
% 0.54/1.62 cnf(i_0_339, axiom, (X1!=X2|szAzrzSzezqlpdtcmdtrp0(X3,X1)=szAzrzSzezqlpdtcmdtrp0(X3,X2))).
% 0.54/1.62 cnf(i_0_340, axiom, (X1!=X2|sdtbsmnsldt0(X1,X3)=sdtbsmnsldt0(X2,X3))).
% 0.54/1.62 cnf(i_0_341, axiom, (X1!=X2|sdtbsmnsldt0(X3,X1)=sdtbsmnsldt0(X3,X2))).
% 0.54/1.62 cnf(i_0_342, axiom, (X1!=X2|sbsmnsldt0(X1)=sbsmnsldt0(X2))).
% 0.54/1.62 cnf(i_0_343, axiom, (X1!=X2|~aElementOf0(X1,X3)|aElementOf0(X2,X3))).
% 0.54/1.62 cnf(i_0_344, axiom, (X1!=X2|~aElementOf0(X3,X1)|aElementOf0(X3,X2))).
% 0.54/1.62 cnf(i_0_345, axiom, (X1!=X2|~isFinite0(X1)|isFinite0(X2))).
% 0.54/1.62 cnf(i_0_346, axiom, (X1!=X2|~aInteger0(X1)|aInteger0(X2))).
% 0.54/1.62 cnf(i_0_347, axiom, (X1!=X2|~aSet0(X1)|aSet0(X2))).
% 0.54/1.62 cnf(i_0_348, axiom, (X1!=X2|~aSubsetOf0(X1,X3)|aSubsetOf0(X2,X3))).
% 0.54/1.62 cnf(i_0_349, axiom, (X1!=X2|~aSubsetOf0(X3,X1)|aSubsetOf0(X3,X2))).
% 0.54/1.62 cnf(i_0_350, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X1,X3,X4)|sdteqdtlpzmzozddtrp0(X2,X3,X4))).
% 0.54/1.62 cnf(i_0_351, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X1,X4)|sdteqdtlpzmzozddtrp0(X3,X2,X4))).
% 0.54/1.62 cnf(i_0_352, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X4,X1)|sdteqdtlpzmzozddtrp0(X3,X4,X2))).
% 0.54/1.62 cnf(i_0_353, axiom, (X1!=X2|~isPrime0(X1)|isPrime0(X2))).
% 0.54/1.62 cnf(i_0_354, axiom, (X1!=X2|~aDivisorOf0(X1,X3)|aDivisorOf0(X2,X3))).
% 0.54/1.62 cnf(i_0_355, axiom, (X1!=X2|~aDivisorOf0(X3,X1)|aDivisorOf0(X3,X2))).
% 0.54/1.62 cnf(i_0_356, axiom, (X1!=X2|~isOpen0(X1)|isOpen0(X2))).
% 0.54/1.62 cnf(i_0_357, axiom, (X1!=X2|~isClosed0(X1)|isClosed0(X2))).
% 0.84/1.96 cnf(i_0_322, axiom, (X1=X1)).
% 0.84/1.96 cnf(i_0_323, axiom, (X1=X2|X2!=X1)).
% 0.84/1.96 cnf(i_0_324, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.84/1.96 cnf(i_0_325, axiom, (X1!=X2|sdtslmnbsdt0(X1,X3)=sdtslmnbsdt0(X2,X3))).
% 0.84/1.96 cnf(i_0_326, axiom, (X1!=X2|sdtslmnbsdt0(X3,X1)=sdtslmnbsdt0(X3,X2))).
% 0.84/1.96 cnf(i_0_327, axiom, (X1!=X2|sdtasdt0(X1,X3)=sdtasdt0(X2,X3))).
% 0.84/1.96 cnf(i_0_328, axiom, (X1!=X2|sdtasdt0(X3,X1)=sdtasdt0(X3,X2))).
% 0.84/1.96 cnf(i_0_329, axiom, (X1!=X2|sdtpldt0(X1,X3)=sdtpldt0(X2,X3))).
% 0.84/1.96 cnf(i_0_330, axiom, (X1!=X2|sdtpldt0(X3,X1)=sdtpldt0(X3,X2))).
% 0.84/1.96 cnf(i_0_331, axiom, (X1!=X2|smndt0(X1)=smndt0(X2))).
% 0.84/1.96 cnf(i_0_332, axiom, (X1!=X2|esk24_1(X1)=esk24_1(X2))).
% 0.84/1.96 cnf(i_0_333, axiom, (X1!=X2|stldt0(X1)=stldt0(X2))).
% 0.84/1.96 cnf(i_0_334, axiom, (X1!=X2|esk21_1(X1)=esk21_1(X2))).
% 0.84/1.96 cnf(i_0_335, axiom, (X1!=X2|esk16_1(X1)=esk16_1(X2))).
% 0.84/1.96 cnf(i_0_336, axiom, (X1!=X2|esk12_2(X1,X3)=esk12_2(X2,X3))).
% 0.84/1.96 cnf(i_0_337, axiom, (X1!=X2|esk12_2(X3,X1)=esk12_2(X3,X2))).
% 0.84/1.96 cnf(i_0_338, axiom, (X1!=X2|szAzrzSzezqlpdtcmdtrp0(X1,X3)=szAzrzSzezqlpdtcmdtrp0(X2,X3))).
% 0.84/1.96 cnf(i_0_339, axiom, (X1!=X2|szAzrzSzezqlpdtcmdtrp0(X3,X1)=szAzrzSzezqlpdtcmdtrp0(X3,X2))).
% 0.84/1.96 cnf(i_0_340, axiom, (X1!=X2|sdtbsmnsldt0(X1,X3)=sdtbsmnsldt0(X2,X3))).
% 0.84/1.96 cnf(i_0_341, axiom, (X1!=X2|sdtbsmnsldt0(X3,X1)=sdtbsmnsldt0(X3,X2))).
% 0.84/1.96 cnf(i_0_342, axiom, (X1!=X2|sbsmnsldt0(X1)=sbsmnsldt0(X2))).
% 0.84/1.96 cnf(i_0_343, axiom, (X1!=X2|~aElementOf0(X1,X3)|aElementOf0(X2,X3))).
% 0.84/1.96 cnf(i_0_344, axiom, (X1!=X2|~aElementOf0(X3,X1)|aElementOf0(X3,X2))).
% 0.84/1.96 cnf(i_0_345, axiom, (X1!=X2|~isFinite0(X1)|isFinite0(X2))).
% 0.84/1.96 cnf(i_0_346, axiom, (X1!=X2|~aInteger0(X1)|aInteger0(X2))).
% 0.84/1.96 cnf(i_0_347, axiom, (X1!=X2|~aSet0(X1)|aSet0(X2))).
% 0.84/1.96 cnf(i_0_348, axiom, (X1!=X2|~aSubsetOf0(X1,X3)|aSubsetOf0(X2,X3))).
% 0.84/1.96 cnf(i_0_349, axiom, (X1!=X2|~aSubsetOf0(X3,X1)|aSubsetOf0(X3,X2))).
% 0.84/1.96 cnf(i_0_350, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X1,X3,X4)|sdteqdtlpzmzozddtrp0(X2,X3,X4))).
% 0.84/1.96 cnf(i_0_351, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X1,X4)|sdteqdtlpzmzozddtrp0(X3,X2,X4))).
% 0.84/1.96 cnf(i_0_352, axiom, (X1!=X2|~sdteqdtlpzmzozddtrp0(X3,X4,X1)|sdteqdtlpzmzozddtrp0(X3,X4,X2))).
% 0.84/1.96 cnf(i_0_353, axiom, (X1!=X2|~isPrime0(X1)|isPrime0(X2))).
% 0.84/1.96 cnf(i_0_354, axiom, (X1!=X2|~aDivisorOf0(X1,X3)|aDivisorOf0(X2,X3))).
% 0.84/1.96 cnf(i_0_355, axiom, (X1!=X2|~aDivisorOf0(X3,X1)|aDivisorOf0(X3,X2))).
% 0.84/1.96 cnf(i_0_356, axiom, (X1!=X2|~isOpen0(X1)|isOpen0(X2))).
% 0.84/1.96 cnf(i_0_357, axiom, (X1!=X2|~isClosed0(X1)|isClosed0(X2))).
% 0.84/1.96 cnf(i_0_358, plain, (~aElementOf0(X1,sbsmnsldt0(X2))|~aSet0(X2)|aElementOf0(esk7_3(X2,sbsmnsldt0(X2),X1),X2)|~aSubsetOf0(esk6_1(X2),cS1395)), inference(equality_inference,[],[114])).
% 0.84/1.96 cnf(i_0_359, plain, (~aElementOf0(X1,sbsmnsldt0(X2))|~aSet0(X2)|aElementOf0(X1,esk7_3(X2,sbsmnsldt0(X2),X1))|~aSubsetOf0(esk6_1(X2),cS1395)), inference(equality_inference,[],[115])).
% 0.84/1.96 cnf(i_0_360, plain, (~aElementOf0(X1,sbsmnsldt0(X2))|~aSet0(X2)|aElementOf0(esk6_1(X2),X2)|aElementOf0(esk7_3(X2,sbsmnsldt0(X2),X1),X2)), inference(equality_inference,[],[121])).
% 0.84/1.96 cnf(i_0_361, plain, (~aElementOf0(X1,sbsmnsldt0(X2))|~aSet0(X2)|aElementOf0(esk6_1(X2),X2)|aElementOf0(X1,esk7_3(X2,sbsmnsldt0(X2),X1))), inference(equality_inference,[],[122])).
% 0.84/1.96 cnf(i_0_362, plain, (~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X3)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(X2,X3))|~sdteqdtlpzmzozddtrp0(X1,X2,X3)|X3=sz00), inference(equality_inference,[],[139])).
% 0.84/1.96 cnf(i_0_363, plain, (~aInteger0(X1)|aElementOf0(X1,sdtslmnbsdt0(X2,X3))|~aElementOf0(X1,X2)|~aElementOf0(X1,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[147])).
% 0.84/1.96 cnf(i_0_364, plain, (~aInteger0(X1)|~aInteger0(X2)|sdteqdtlpzmzozddtrp0(X3,X1,X2)|~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))|X2=sz00), inference(equality_inference,[],[158])).
% 0.84/1.96 cnf(i_0_365, plain, (aElementOf0(X1,X2)|aElementOf0(X1,X3)|~aElementOf0(X1,sdtbsmnsldt0(X2,X3))|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[159])).
% 0.84/1.96 cnf(i_0_366, plain, (~aInteger0(X1)|~aElementOf0(X1,X2)|~aSet0(X3)|aElementOf0(X1,sbsmnsldt0(X3))|~aElementOf0(X2,X3)|~aSubsetOf0(esk6_1(X3),cS1395)), inference(equality_inference,[],[161])).
% 0.84/1.96 cnf(i_0_367, plain, (~aInteger0(X1)|aElementOf0(X1,sdtbsmnsldt0(X2,X3))|~aElementOf0(X1,X2)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[164])).
% 0.84/1.96 cnf(i_0_368, plain, (~aInteger0(X1)|aElementOf0(X1,sdtbsmnsldt0(X2,X3))|~aElementOf0(X1,X3)|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[165])).
% 0.84/1.96 cnf(i_0_369, plain, (~aInteger0(X1)|~aElementOf0(X1,X2)|~aSet0(X3)|aElementOf0(X1,sbsmnsldt0(X3))|~aElementOf0(X2,X3)|aElementOf0(esk6_1(X3),X3)), inference(equality_inference,[],[170])).
% 0.84/1.96 cnf(i_0_370, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,sdtslmnbsdt0(X2,X3))|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[173])).
% 0.84/1.96 cnf(i_0_371, plain, (aElementOf0(X1,X2)|~aElementOf0(X1,sdtslmnbsdt0(X3,X2))|~aSubsetOf0(X3,cS1395)|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[174])).
% 0.84/1.96 cnf(i_0_372, plain, (aInteger0(X1)|~aElementOf0(X1,sdtslmnbsdt0(X2,X3))|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[183])).
% 0.84/1.96 cnf(i_0_373, plain, (aInteger0(X1)|~aElementOf0(X1,sdtbsmnsldt0(X2,X3))|~aSubsetOf0(X2,cS1395)|~aSubsetOf0(X3,cS1395)), inference(equality_inference,[],[184])).
% 0.84/1.96 cnf(i_0_374, plain, (~aElementOf0(X1,X2)|~aElementOf0(X1,stldt0(X2))|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[196])).
% 0.84/1.96 cnf(i_0_375, plain, (~aSet0(X1)|aInteger0(X2)|~aElementOf0(X2,sbsmnsldt0(X1))|~aSubsetOf0(esk6_1(X1),cS1395)), inference(equality_inference,[],[199])).
% 0.84/1.96 cnf(i_0_376, plain, (aSet0(sdtslmnbsdt0(X1,X2))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[208])).
% 0.84/1.96 cnf(i_0_377, plain, (aSet0(sdtbsmnsldt0(X1,X2))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[209])).
% 0.84/1.96 cnf(i_0_378, plain, (~aInteger0(X1)|~aInteger0(X2)|aInteger0(X3)|~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))|X2=sz00), inference(equality_inference,[],[215])).
% 0.84/1.96 cnf(i_0_379, plain, (~aInteger0(X1)|aElementOf0(X1,X2)|aElementOf0(X1,stldt0(X2))|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[219])).
% 0.84/1.96 cnf(i_0_380, plain, (~aSet0(X1)|aInteger0(X2)|~aElementOf0(X2,sbsmnsldt0(X1))|aElementOf0(esk6_1(X1),X1)), inference(equality_inference,[],[222])).
% 0.84/1.96 cnf(i_0_381, plain, (~aInteger0(X1)|~aInteger0(sdtasdt0(X1,X2))|aDivisorOf0(X1,sdtasdt0(X1,X2))|~aInteger0(X2)|X1=sz00), inference(equality_inference,[],[224])).
% 0.84/1.96 cnf(i_0_382, plain, (aInteger0(X1)|~aElementOf0(X1,stldt0(X2))|~aSubsetOf0(X2,cS1395)), inference(equality_inference,[],[231])).
% 0.84/1.96 cnf(i_0_383, plain, (~aInteger0(X1)|~isPrime0(X1)|X1=sz00|aElementOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X1),xS)), inference(equality_inference,[],[240])).
% 0.84/1.96 cnf(i_0_384, plain, (~aSet0(X1)|aSet0(sbsmnsldt0(X1))|~aSubsetOf0(esk6_1(X1),cS1395)), inference(equality_inference,[],[242])).
% 0.84/1.96 cnf(i_0_385, plain, (~aInteger0(X1)|~aInteger0(X2)|aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))|X2=sz00), inference(equality_inference,[],[265])).
% 0.84/1.96 cnf(i_0_386, plain, (~isPrime0(X1)|~aInteger0(smndt0(sz10))|~aDivisorOf0(X1,smndt0(sz10))), inference(equality_inference,[],[266])).
% 0.84/1.96 cnf(i_0_387, plain, (~aSet0(X1)|aSet0(sbsmnsldt0(X1))|aElementOf0(esk6_1(X1),X1)), inference(equality_inference,[],[270])).
% 0.84/1.96 cnf(i_0_388, plain, (~isPrime0(X1)|~aInteger0(sz10)|~aDivisorOf0(X1,sz10)), inference(equality_inference,[],[273])).
% 0.84/1.96 cnf(i_0_389, plain, (aSet0(stldt0(X1))|~aSubsetOf0(X1,cS1395)), inference(equality_inference,[],[278])).
% 0.84/1.96 cnf(i_0_390, plain, (aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS)))), inference(equality_inference,[],[280])).
% 0.84/1.96 cnf(i_0_391, plain, (~aInteger0(X1)|~aDivisorOf0(sz00,X1)), inference(equality_inference,[],[281])).
% 0.84/1.96 cnf(i_0_392, plain, (aElementOf0(sz10,stldt0(sbsmnsldt0(xS)))), inference(equality_inference,[],[288])).
% 0.84/1.96 cnf(i_0_393, plain, (~isPrime0(X1)|~aDivisorOf0(X1,sz10)), inference(scs_inference,[],[i_0_318,i_0_388])).
% 0.84/1.96 cnf(i_0_394, plain, (aElementOf0(sdtpldt0(sz10,xp),cS2200)), inference(scs_inference,[],[i_0_233,i_0_217])).
% 0.84/1.96 cnf(i_0_395, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(X1,cS2200)), inference(rename_variables,[],[i_0_217])).
% 0.84/1.96 cnf(i_0_396, plain, (aInteger0(sdtpldt0(sz10,xp))), inference(scs_inference,[],[i_0_233,i_0_217,i_0_228])).
% 0.84/1.96 cnf(i_0_397, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aInteger0(X1)), inference(rename_variables,[],[i_0_228])).
% 0.84/1.96 cnf(i_0_398, plain, (aInteger0(esk24_1(sz10))), inference(scs_inference,[],[i_0_392,i_0_233,i_0_217,i_0_228,i_0_234])).
% 0.84/1.96 cnf(i_0_399, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aInteger0(esk24_1(X1))), inference(rename_variables,[],[i_0_234])).
% 0.84/1.96 cnf(i_0_400, plain, (aInteger0(esk21_1(sz10))), inference(scs_inference,[],[i_0_392,i_0_233,i_0_217,i_0_228,i_0_234,i_0_235])).
% 0.84/1.96 cnf(i_0_401, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aInteger0(esk21_1(X1))), inference(rename_variables,[],[i_0_235])).
% 0.84/1.96 cnf(i_0_402, plain, (aInteger0(smndt0(sz10))), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258])).
% 0.84/1.96 cnf(i_0_403, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aInteger0(X1)), inference(rename_variables,[],[i_0_258])).
% 0.84/1.96 cnf(i_0_404, plain, (cS2043=xS), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323])).
% 0.84/1.96 cnf(i_0_405, plain, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,esk24_1(sz10)),stldt0(sbsmnsldt0(xS)))), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166])).
% 0.84/1.96 cnf(i_0_406, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)),stldt0(sbsmnsldt0(xS)))), inference(rename_variables,[],[i_0_166])).
% 0.84/1.96 cnf(i_0_407, plain, (aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,esk21_1(sz10)),stldt0(sbsmnsldt0(xS)))), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167])).
% 0.84/1.96 cnf(i_0_408, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)),stldt0(sbsmnsldt0(xS)))), inference(rename_variables,[],[i_0_167])).
% 0.84/1.96 cnf(i_0_409, plain, (~aElementOf0(sz10,sbsmnsldt0(xS))), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207])).
% 0.84/1.96 cnf(i_0_410, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(rename_variables,[],[i_0_207])).
% 0.84/1.96 cnf(i_0_411, plain, (esk24_1(sz10)!=sz00), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243])).
% 0.84/1.96 cnf(i_0_412, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|esk24_1(X1)!=sz00), inference(rename_variables,[],[i_0_243])).
% 0.84/1.96 cnf(i_0_413, plain, (esk21_1(sz10)!=sz00), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244])).
% 0.84/1.96 cnf(i_0_414, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|esk21_1(X1)!=sz00), inference(rename_variables,[],[i_0_244])).
% 0.84/1.96 cnf(i_0_415, plain, (stldt0(sbsmnsldt0(xS))!=sbsmnsldt0(xS)), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344])).
% 0.84/1.96 cnf(i_0_416, plain, (isFinite0(cS2043)), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_313,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345])).
% 0.84/1.96 cnf(i_0_417, plain, (aSet0(cS2043)), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_313,i_0_314,i_0_321,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347])).
% 0.84/1.96 cnf(i_0_418, plain, (isOpen0(cS2076)), inference(scs_inference,[],[i_0_392,i_0_390,i_0_233,i_0_313,i_0_314,i_0_321,i_0_312,i_0_305,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356])).
% 0.84/1.96 cnf(i_0_419, plain, (sdtpldt0(sz10,xp)=smndt0(sz10)), inference(scs_inference,[],[i_0_392,i_0_303,i_0_390,i_0_233,i_0_313,i_0_314,i_0_321,i_0_191,i_0_312,i_0_305,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192])).
% 0.84/1.96 cnf(i_0_420, plain, (~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|X1=smndt0(sz10)|X1=sz10|~aInteger0(X1)), inference(rename_variables,[],[i_0_192])).
% 0.84/1.96 cnf(i_0_421, plain, (sdteqdtlpzmzozddtrp0(esk29_0,esk29_0,xp)), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_303,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_191,i_0_312,i_0_305,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203])).
% 0.84/1.96 cnf(i_0_422, plain, (X1=sz00|~aInteger0(X2)|~aInteger0(X1)|sdteqdtlpzmzozddtrp0(X2,X2,X1)), inference(rename_variables,[],[i_0_203])).
% 0.84/1.96 cnf(i_0_423, plain, (~aElementOf0(stldt0(sbsmnsldt0(xS)),xS)), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_191,i_0_312,i_0_305,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214])).
% 0.84/1.96 cnf(i_0_424, plain, (aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X2,xS)|~aInteger0(X1)|~aElementOf0(X1,X2)), inference(rename_variables,[],[i_0_214])).
% 0.84/1.96 cnf(i_0_425, plain, (aElementOf0(sdtpldt0(sz10,xp),stldt0(sbsmnsldt0(xS)))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216])).
% 0.84/1.96 cnf(i_0_426, plain, (~aSubsetOf0(X1,X2)|~aSet0(X2)|aElementOf0(X3,X2)|~aElementOf0(X3,X1)), inference(rename_variables,[],[i_0_216])).
% 0.84/1.96 cnf(i_0_427, plain, (aSet0(szAzrzSzezqlpdtcmdtrp0(esk29_0,xp))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385])).
% 0.84/1.96 cnf(i_0_428, plain, (X1=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(X2,X1))|~aInteger0(X2)|~aInteger0(X1)), inference(rename_variables,[],[i_0_385])).
% 0.84/1.96 cnf(i_0_429, plain, (~aInteger0(sdtpldt0(sz10,smndt0(xp)))|aElementOf0(sdtpldt0(sz10,smndt0(xp)),cS2200)), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177])).
% 0.84/1.96 cnf(i_0_430, plain, (~sdteqdtlpzmzozddtrp0(X1,sz10,xp)|aElementOf0(X1,cS2200)|~aInteger0(X1)), inference(rename_variables,[],[i_0_177])).
% 0.84/1.96 cnf(i_0_431, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,esk24_1(sz10)))|aInteger0(esk25_2(sz10,X1))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177,i_0_134])).
% 0.84/1.96 cnf(i_0_432, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|aInteger0(esk25_2(X1,X2))), inference(rename_variables,[],[i_0_134])).
% 0.84/1.96 cnf(i_0_433, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,esk21_1(sz10)))|aInteger0(esk22_2(sz10,X1))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177,i_0_134,i_0_135])).
% 0.84/1.96 cnf(i_0_434, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|aInteger0(esk22_2(X1,X2))), inference(rename_variables,[],[i_0_135])).
% 0.84/1.96 cnf(i_0_435, plain, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,esk24_1(sz10)))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177,i_0_134,i_0_135,i_0_150])).
% 0.84/1.96 cnf(i_0_436, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|aInteger0(X2)), inference(rename_variables,[],[i_0_150])).
% 0.84/1.96 cnf(i_0_437, plain, (aInteger0(X1)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,esk21_1(sz10)))), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177,i_0_134,i_0_135,i_0_150,i_0_151])).
% 0.84/1.96 cnf(i_0_438, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk21_1(X1)))|aInteger0(X2)), inference(rename_variables,[],[i_0_151])).
% 0.84/1.96 cnf(i_0_439, plain, (aInteger0(X1)|~aDivisorOf0(X1,esk29_0)), inference(scs_inference,[],[i_0_392,i_0_315,i_0_317,i_0_318,i_0_303,i_0_194,i_0_390,i_0_233,i_0_313,i_0_314,i_0_320,i_0_321,i_0_259,i_0_191,i_0_312,i_0_305,i_0_306,i_0_217,i_0_228,i_0_234,i_0_235,i_0_258,i_0_323,i_0_166,i_0_167,i_0_207,i_0_243,i_0_244,i_0_344,i_0_345,i_0_347,i_0_356,i_0_192,i_0_203,i_0_214,i_0_216,i_0_385,i_0_177,i_0_134,i_0_135,i_0_150,i_0_151,i_0_277])).
% 0.84/1.96 cnf(i_0_440, plain, (~aInteger0(X1)|aInteger0(X2)|~aDivisorOf0(X2,X1)), inference(rename_variables,[],[i_0_277])).
% 0.84/1.96 cnf(i_0_441, plain, (~aInteger0(X1)|~aInteger0(X2)|~isPrime0(X2)|~sdteqdtlpzmzozddtrp0(X1,sz00,X2)|X2=sz00|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))), inference(scs_inference,[],[i_0_423,i_0_132])).
% 0.84/1.96 cnf(i_0_442, plain, (~aInteger0(X1)|~aInteger0(X2)|~isPrime0(X2)|X2=sz00|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|~aDivisorOf0(X2,sdtpldt0(X1,smndt0(sz00)))), inference(scs_inference,[],[i_0_423,i_0_141])).
% 0.84/1.96 cnf(i_0_443, plain, (~aInteger0(X1)|~isPrime0(X1)|sdteqdtlpzmzozddtrp0(X2,sz00,X1)|X1=sz00|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))), inference(scs_inference,[],[i_0_423,i_0_144])).
% 0.84/1.96 cnf(i_0_444, plain, (~aInteger0(X1)|~isPrime0(X1)|X1=sz00|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))|aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))), inference(scs_inference,[],[i_0_423,i_0_146])).
% 0.84/1.96 cnf(i_0_445, plain, (~aInteger0(X1)|~aInteger0(X2)|~isPrime0(X2)|~aInteger0(X3)|X2=sz00|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X2))|sdtasdt0(X2,X3)!=sdtpldt0(X1,smndt0(sz00))), inference(scs_inference,[],[i_0_423,i_0_149])).
% 0.84/1.96 cnf(i_0_446, plain, (~aInteger0(X1)|~isPrime0(X1)|aInteger0(X2)|X1=sz00|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))), inference(scs_inference,[],[i_0_423,i_0_182])).
% 0.84/1.96 cnf(i_0_447, plain, (~aInteger0(X1)|~isPrime0(X1)|X1=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))), inference(scs_inference,[],[i_0_423,i_0_230])).
% 0.84/1.96 cnf(i_0_448, plain, (sdtpldt0(sz10,smndt0(xp))!=smndt0(sz10)), inference(scs_inference,[],[i_0_419,i_0_241])).
% 0.84/1.96 cnf(i_0_449, plain, (aElementOf0(sdtpldt0(sz10,smndt0(xp)),cS2200)), inference(scs_inference,[],[i_0_223,i_0_217])).
% 0.84/1.96 cnf(i_0_450, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(X1,cS2200)), inference(rename_variables,[],[i_0_217])).
% 0.84/1.96 cnf(i_0_451, plain, (aInteger0(esk24_1(sdtpldt0(sz10,xp)))), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234])).
% 0.84/1.96 cnf(i_0_452, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aInteger0(esk24_1(X1))), inference(rename_variables,[],[i_0_234])).
% 0.84/1.96 cnf(i_0_453, plain, (aInteger0(esk21_1(sdtpldt0(sz10,xp)))), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234,i_0_235])).
% 0.84/1.96 cnf(i_0_454, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|aInteger0(esk21_1(X1))), inference(rename_variables,[],[i_0_235])).
% 0.84/1.96 cnf(i_0_455, plain, (~aElementOf0(sdtpldt0(sz10,xp),sbsmnsldt0(xS))), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207])).
% 0.84/1.96 cnf(i_0_456, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X1,sbsmnsldt0(xS))), inference(rename_variables,[],[i_0_207])).
% 0.84/1.96 cnf(i_0_457, plain, (esk24_1(sdtpldt0(sz10,xp))!=sz00), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243])).
% 0.84/1.96 cnf(i_0_458, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|esk24_1(X1)!=sz00), inference(rename_variables,[],[i_0_243])).
% 0.84/1.96 cnf(i_0_459, plain, (esk21_1(sdtpldt0(sz10,xp))!=sz00), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244])).
% 0.84/1.96 cnf(i_0_460, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|esk21_1(X1)!=sz00), inference(rename_variables,[],[i_0_244])).
% 0.84/1.96 cnf(i_0_461, plain, (aInteger0(sdtpldt0(sz10,smndt0(xp)))), inference(scs_inference,[],[i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228])).
% 0.84/1.96 cnf(i_0_462, plain, (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aInteger0(X1)), inference(rename_variables,[],[i_0_228])).
% 0.84/1.96 cnf(i_0_463, plain, (smndt0(sz10)=sdtpldt0(sz10,xp)), inference(scs_inference,[],[i_0_419,i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323])).
% 0.84/1.96 cnf(i_0_464, plain, (~aElementOf0(smndt0(sz10),sbsmnsldt0(xS))), inference(scs_inference,[],[i_0_419,i_0_425,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343])).
% 0.84/1.96 cnf(i_0_465, plain, (aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,esk24_1(sz10)))), inference(scs_inference,[],[i_0_419,i_0_425,i_0_306,i_0_405,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276])).
% 0.84/1.96 cnf(i_0_466, plain, (~aSet0(X1)|aSet0(X2)|~aSubsetOf0(X2,X1)), inference(rename_variables,[],[i_0_276])).
% 0.84/1.96 cnf(i_0_467, plain, (~aElementOf0(stldt0(sbsmnsldt0(xS)),cS2043)), inference(scs_inference,[],[i_0_419,i_0_425,i_0_423,i_0_404,i_0_306,i_0_405,i_0_223,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344])).
% 0.84/1.96 cnf(i_0_468, plain, (aSet0(cS2076)), inference(scs_inference,[],[i_0_419,i_0_425,i_0_423,i_0_404,i_0_306,i_0_405,i_0_223,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347])).
% 0.84/1.96 cnf(i_0_469, plain, (sdtpldt0(sz10,smndt0(xp))=smndt0(sz10)), inference(scs_inference,[],[i_0_171,i_0_419,i_0_425,i_0_423,i_0_404,i_0_294,i_0_306,i_0_405,i_0_223,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192])).
% 0.84/1.96 cnf(i_0_470, plain, (~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))|X1=smndt0(sz10)|X1=sz10|~aInteger0(X1)), inference(rename_variables,[],[i_0_192])).
% 0.84/1.96 cnf(i_0_471, plain, (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sdtpldt0(sz10,xp),xp)), inference(scs_inference,[],[i_0_171,i_0_419,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_320,i_0_306,i_0_405,i_0_223,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203])).
% 0.84/1.96 cnf(i_0_472, plain, (X1=sz00|~aInteger0(X2)|~aInteger0(X1)|sdteqdtlpzmzozddtrp0(X2,X2,X1)), inference(rename_variables,[],[i_0_203])).
% 0.84/1.96 cnf(i_0_473, plain, (~aElementOf0(cS2200,xS)), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_320,i_0_306,i_0_405,i_0_223,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214])).
% 0.84/1.96 cnf(i_0_474, plain, (aElementOf0(X1,sbsmnsldt0(xS))|~aElementOf0(X2,xS)|~aInteger0(X1)|~aElementOf0(X1,X2)), inference(rename_variables,[],[i_0_214])).
% 0.84/1.96 cnf(i_0_475, plain, (aSet0(szAzrzSzezqlpdtcmdtrp0(sdtpldt0(sz10,xp),xp))), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_320,i_0_306,i_0_405,i_0_223,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385])).
% 0.84/1.96 cnf(i_0_476, plain, (X1=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(X2,X1))|~aInteger0(X2)|~aInteger0(X1)), inference(rename_variables,[],[i_0_385])).
% 0.84/1.96 cnf(i_0_477, plain, (aElementOf0(sdtpldt0(sz10,smndt0(xp)),stldt0(sbsmnsldt0(xS)))), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_320,i_0_306,i_0_405,i_0_223,i_0_259,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385,i_0_216])).
% 0.84/1.96 cnf(i_0_478, plain, (~aSubsetOf0(X1,X2)|~aSet0(X2)|aElementOf0(X3,X2)|~aElementOf0(X3,X1)), inference(rename_variables,[],[i_0_216])).
% 0.84/1.96 cnf(i_0_479, plain, (aElementOf0(esk29_0,szAzrzSzezqlpdtcmdtrp0(esk29_0,xp))), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_421,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_315,i_0_320,i_0_306,i_0_405,i_0_223,i_0_259,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385,i_0_216,i_0_362])).
% 0.84/1.96 cnf(i_0_480, plain, (X1=sz00|aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X3,X1))|~sdteqdtlpzmzozddtrp0(X2,X3,X1)|~aInteger0(X2)|~aInteger0(X3)|~aInteger0(X1)), inference(rename_variables,[],[i_0_362])).
% 0.84/1.96 cnf(i_0_481, plain, (X1=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))|X1!=sdtasdt0(xp,esk28_0)), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_421,i_0_396,i_0_425,i_0_423,i_0_404,i_0_294,i_0_317,i_0_315,i_0_320,i_0_249,i_0_306,i_0_405,i_0_223,i_0_259,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385,i_0_216,i_0_362,i_0_324])).
% 0.84/1.96 cnf(i_0_482, plain, (aInteger0(sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))|esk24_1(sz10)!=sdtasdt0(xp,esk28_0)), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_421,i_0_396,i_0_425,i_0_398,i_0_423,i_0_404,i_0_294,i_0_317,i_0_315,i_0_320,i_0_249,i_0_306,i_0_405,i_0_223,i_0_259,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385,i_0_216,i_0_362,i_0_324,i_0_346])).
% 0.84/1.96 cnf(i_0_483, plain, (~aElementOf0(X1,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,esk24_1(X1)))|sdtasdt0(esk24_1(X1),esk25_2(X1,X2))=sdtpldt0(X2,smndt0(X1))), inference(rename_variables,[],[i_0_112])).
% 0.84/1.96 cnf(i_0_484, plain, (esk24_1(sz10)!=sdtasdt0(xp,esk28_0)|sdteqdtlpzmzozddtrp0(X1,sdtpldt0(sz10,xp),esk21_1(sdtpldt0(sz10,xp)))|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sdtpldt0(sz10,xp),esk21_1(sdtpldt0(sz10,xp))))), inference(scs_inference,[],[i_0_171,i_0_394,i_0_419,i_0_421,i_0_396,i_0_425,i_0_398,i_0_423,i_0_404,i_0_294,i_0_317,i_0_315,i_0_320,i_0_249,i_0_306,i_0_405,i_0_223,i_0_307,i_0_259,i_0_312,i_0_217,i_0_234,i_0_235,i_0_207,i_0_243,i_0_244,i_0_228,i_0_323,i_0_343,i_0_276,i_0_344,i_0_347,i_0_192,i_0_203,i_0_214,i_0_385,i_0_216,i_0_362,i_0_324,i_0_346,i_0_117])).
% 0.84/1.96 cnf(i_0_485, plain, (sdtasdt0(xp,esk28_0)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))), inference(equality_inference,[],[481])).
% 0.84/1.96 cnf(i_0_486,plain, ($false), inference(scs_inference,[],[i_0+469, i_0_448]), ['proof']).
% 0.84/1.96 % SZS output end CNFRefutation
% 0.84/1.96 % Total time : 1.272s
%------------------------------------------------------------------------------