%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM543+2 : 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 : n011.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:45 PM UTC 2026
% Result : Theorem 175.19s 124.92s
% Output : CNFRefutation 190.19s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 196)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
? [X1] :
( aElementOf0(X1,szNzAzT0)
& ( ( aSet0(slbdtrb0(X1))
& ! [X2] :
( aElementOf0(X2,slbdtrb0(X1))
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X1) ) ) )
=> ( ! [X2] :
( aElementOf0(X2,xS)
=> aElementOf0(X2,slbdtrb0(X1)) )
| aSubsetOf0(xS,slbdtrb0(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(mCardCons,axiom,
! [X1] :
( ( aSet0(X1)
& isFinite0(X1) )
=> ! [X2] :
( aElement0(X2)
=> ( ~ aElementOf0(X2,X1)
=> sbrdtbr0(sdtpldt0(X1,X2)) = szszuzczcdt0(sbrdtbr0(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardCons) ).
fof(mDiffCons,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aSet0(X2) )
=> ( ~ aElementOf0(X1,X2)
=> sdtmndt0(sdtpldt0(X2,X1),X1) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDiffCons) ).
fof(mNoScLessZr,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ~ sdtlseqdt0(szszuzczcdt0(X1),sz00) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNoScLessZr) ).
fof(mCountNFin,axiom,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> ~ isFinite0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin) ).
fof(mDefDiff,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aElement0(X2) )
=> ! [X3] :
( X3 = sdtmndt0(X1,X2)
<=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
<=> ( aElement0(X4)
& aElementOf0(X4,X1)
& X4 != X2 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
fof(mDefCons,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aElement0(X2) )
=> ! [X3] :
( X3 = sdtpldt0(X1,X2)
<=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
<=> ( aElement0(X4)
& ( aElementOf0(X4,X1)
| X4 = X2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefCons) ).
fof(mDefSeg,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ! [X2] :
( X2 = slbdtrb0(X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSeg) ).
fof(mLessTrans,axiom,
! [X1,X2,X3] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0)
& aElementOf0(X3,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTrans) ).
fof(mDefMax,axiom,
! [X1] :
( ( aSubsetOf0(X1,szNzAzT0)
& isFinite0(X1)
& X1 != slcrc0 )
=> ! [X2] :
( X2 = szmzazxdt0(X1)
<=> ( aElementOf0(X2,X1)
& ! [X3] :
( aElementOf0(X3,X1)
=> sdtlseqdt0(X3,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefMax) ).
fof(mMinMin,axiom,
! [X1,X2] :
( ( aSubsetOf0(X1,szNzAzT0)
& aSubsetOf0(X2,szNzAzT0)
& X1 != slcrc0
& X2 != slcrc0 )
=> ( ( aElementOf0(szmzizndt0(X1),X2)
& aElementOf0(szmzizndt0(X2),X1) )
=> szmzizndt0(X1) = szmzizndt0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMinMin) ).
fof(mSegSucc,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))
<=> ( aElementOf0(X1,slbdtrb0(X2))
| X1 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegSucc) ).
fof(mDefMin,axiom,
! [X1] :
( ( aSubsetOf0(X1,szNzAzT0)
& X1 != slcrc0 )
=> ! [X2] :
( X2 = szmzizndt0(X1)
<=> ( aElementOf0(X2,X1)
& ! [X3] :
( aElementOf0(X3,X1)
=> sdtlseqdt0(X2,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefMin) ).
fof(mCardSubEx,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aElementOf0(X2,szNzAzT0) )
=> ( ( isFinite0(X1)
& sdtlseqdt0(X2,sbrdtbr0(X1)) )
=> ? [X3] :
( aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardSubEx) ).
fof(mCardDiff,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( ( isFinite0(X1)
& aElementOf0(X2,X1) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X2))) = sbrdtbr0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardDiff) ).
fof(mSuccLess,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
<=> sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccLess) ).
fof(mSegLess,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
<=> aSubsetOf0(slbdtrb0(X1),slbdtrb0(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegLess) ).
fof(mDefSub,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aSubsetOf0(X2,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(mLessASymm,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessASymm) ).
fof(mSubTrans,axiom,
! [X1,X2,X3] :
( ( aSet0(X1)
& aSet0(X2)
& aSet0(X3) )
=> ( ( aSubsetOf0(X1,X2)
& aSubsetOf0(X2,X3) )
=> aSubsetOf0(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubTrans) ).
fof(mLessTotal,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTotal) ).
fof(mConsDiff,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> sdtpldt0(sdtmndt0(X1,X2),X2) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mConsDiff) ).
fof(mCardSub,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( ( isFinite0(X1)
& aSubsetOf0(X2,X1) )
=> sdtlseqdt0(sbrdtbr0(X2),sbrdtbr0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardSub) ).
fof(mSubASymm,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ( ( aSubsetOf0(X1,X2)
& aSubsetOf0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubASymm) ).
fof(mSuccEquSucc,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( szszuzczcdt0(X1) = szszuzczcdt0(X2)
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccEquSucc) ).
fof(mCDiffSet,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( ( aSet0(X2)
& isCountable0(X2) )
=> isCountable0(sdtmndt0(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCDiffSet) ).
fof(mCConsSet,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( ( aSet0(X2)
& isCountable0(X2) )
=> isCountable0(sdtpldt0(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCConsSet) ).
fof(mFDiffSet,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( ( aSet0(X2)
& isFinite0(X2) )
=> isFinite0(sdtmndt0(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mFDiffSet) ).
fof(mFConsSet,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( ( aSet0(X2)
& isFinite0(X2) )
=> isFinite0(sdtpldt0(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mFConsSet) ).
fof(mSubFSet,axiom,
! [X1] :
( ( aSet0(X1)
& isFinite0(X1) )
=> ! [X2] :
( aSubsetOf0(X2,X1)
=> isFinite0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubFSet) ).
fof(mCardNum,axiom,
! [X1] :
( aSet0(X1)
=> ( aElementOf0(sbrdtbr0(X1),szNzAzT0)
<=> isFinite0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardNum) ).
fof(mNatExtra,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( X1 = sz00
| ? [X2] :
( aElementOf0(X2,szNzAzT0)
& X1 = szszuzczcdt0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNatExtra) ).
fof(mIH,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> iLess0(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH) ).
fof(mLessSucc,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sdtlseqdt0(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessSucc) ).
fof(mSuccNum,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
& szszuzczcdt0(X1) != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(mLessRefl,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessRefl) ).
fof(mEOfElem,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> aElement0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(mZeroLess,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sdtlseqdt0(sz00,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroLess) ).
fof(m__1986,hypothesis,
( aSet0(xS)
& ! [X1] :
( aElementOf0(X1,xS)
=> aElementOf0(X1,szNzAzT0) )
& aSubsetOf0(xS,szNzAzT0)
& isFinite0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1986) ).
fof(mSegFin,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> isFinite0(slbdtrb0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegFin) ).
fof(mDefEmp,axiom,
! [X1] :
( X1 = slcrc0
<=> ( aSet0(X1)
& ~ ? [X2] : aElementOf0(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefEmp) ).
fof(mNatNSucc,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> X1 != szszuzczcdt0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNatNSucc) ).
fof(mSubRefl,axiom,
! [X1] :
( aSet0(X1)
=> aSubsetOf0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubRefl) ).
fof(mCardS,axiom,
! [X1] :
( aSet0(X1)
=> aElement0(sbrdtbr0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardS) ).
fof(mCountNFin_01,axiom,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> X1 != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin_01) ).
fof(mCardEmpty,axiom,
! [X1] :
( aSet0(X1)
=> ( sbrdtbr0(X1) = sz00
<=> X1 = slcrc0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardEmpty) ).
fof(mZeroNum,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroNum) ).
fof(mNATSet,axiom,
( aSet0(szNzAzT0)
& isCountable0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(mEmpFin,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEmpFin) ).
fof(mSegZero,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegZero) ).
fof(i_0_50,negated_conjecture,
~ ? [X1] :
( aElementOf0(X1,szNzAzT0)
& ( ( aSet0(slbdtrb0(X1))
& ! [X2] :
( aElementOf0(X2,slbdtrb0(X1))
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X1) ) ) )
=> ( ! [X2] :
( aElementOf0(X2,xS)
=> aElementOf0(X2,slbdtrb0(X1)) )
| aSubsetOf0(xS,slbdtrb0(X1)) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(i_0_51,plain,
! [X1] :
( ( aSet0(X1)
& isFinite0(X1) )
=> ! [X2] :
( aElement0(X2)
=> ( ~ aElementOf0(X2,X1)
=> sbrdtbr0(sdtpldt0(X1,X2)) = szszuzczcdt0(sbrdtbr0(X1)) ) ) ),
inference(fof_simplification,[status(thm)],[mCardCons]) ).
fof(i_0_52,plain,
! [X1,X2] :
( ( aElement0(X1)
& aSet0(X2) )
=> ( ~ aElementOf0(X1,X2)
=> sdtmndt0(sdtpldt0(X2,X1),X1) = X2 ) ),
inference(fof_simplification,[status(thm)],[mDiffCons]) ).
fof(i_0_53,plain,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ~ sdtlseqdt0(szszuzczcdt0(X1),sz00) ),
inference(fof_simplification,[status(thm)],[mNoScLessZr]) ).
fof(i_0_54,plain,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> ~ isFinite0(X1) ),
inference(fof_simplification,[status(thm)],[mCountNFin]) ).
fof(i_0_55,plain,
! [X130,X131,X132,X133,X134,X135] :
( ( aSet0(X132)
| X132 != sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( aElement0(X133)
| ~ aElementOf0(X133,X132)
| X132 != sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( aElementOf0(X133,X130)
| ~ aElementOf0(X133,X132)
| X132 != sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( X133 != X131
| ~ aElementOf0(X133,X132)
| X132 != sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( ~ aElement0(X134)
| ~ aElementOf0(X134,X130)
| X134 = X131
| aElementOf0(X134,X132)
| X132 != sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( ~ aElementOf0(esk4_3(X130,X131,X135),X135)
| ~ aElement0(esk4_3(X130,X131,X135))
| ~ aElementOf0(esk4_3(X130,X131,X135),X130)
| esk4_3(X130,X131,X135) = X131
| ~ aSet0(X135)
| X135 = sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( aElement0(esk4_3(X130,X131,X135))
| aElementOf0(esk4_3(X130,X131,X135),X135)
| ~ aSet0(X135)
| X135 = sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( aElementOf0(esk4_3(X130,X131,X135),X130)
| aElementOf0(esk4_3(X130,X131,X135),X135)
| ~ aSet0(X135)
| X135 = sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) )
& ( esk4_3(X130,X131,X135) != X131
| aElementOf0(esk4_3(X130,X131,X135),X135)
| ~ aSet0(X135)
| X135 = sdtmndt0(X130,X131)
| ~ aSet0(X130)
| ~ aElement0(X131) ) ),
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)],[mDefDiff])])])])])]) ).
fof(i_0_56,plain,
! [X123,X124,X125,X126,X127,X128] :
( ( aSet0(X125)
| X125 != sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( aElement0(X126)
| ~ aElementOf0(X126,X125)
| X125 != sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( aElementOf0(X126,X123)
| X126 = X124
| ~ aElementOf0(X126,X125)
| X125 != sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( ~ aElementOf0(X127,X123)
| ~ aElement0(X127)
| aElementOf0(X127,X125)
| X125 != sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( X127 != X124
| ~ aElement0(X127)
| aElementOf0(X127,X125)
| X125 != sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( ~ aElementOf0(esk3_3(X123,X124,X128),X123)
| ~ aElement0(esk3_3(X123,X124,X128))
| ~ aElementOf0(esk3_3(X123,X124,X128),X128)
| ~ aSet0(X128)
| X128 = sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( esk3_3(X123,X124,X128) != X124
| ~ aElement0(esk3_3(X123,X124,X128))
| ~ aElementOf0(esk3_3(X123,X124,X128),X128)
| ~ aSet0(X128)
| X128 = sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( aElement0(esk3_3(X123,X124,X128))
| aElementOf0(esk3_3(X123,X124,X128),X128)
| ~ aSet0(X128)
| X128 = sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) )
& ( aElementOf0(esk3_3(X123,X124,X128),X123)
| esk3_3(X123,X124,X128) = X124
| aElementOf0(esk3_3(X123,X124,X128),X128)
| ~ aSet0(X128)
| X128 = sdtpldt0(X123,X124)
| ~ aSet0(X123)
| ~ aElement0(X124) ) ),
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)],[mDefCons])])])])])]) ).
fof(i_0_57,plain,
! [X193,X194,X195,X196,X197] :
( ( aSet0(X194)
| X194 != slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( aElementOf0(X195,szNzAzT0)
| ~ aElementOf0(X195,X194)
| X194 != slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(X195),X193)
| ~ aElementOf0(X195,X194)
| X194 != slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( ~ aElementOf0(X196,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X196),X193)
| aElementOf0(X196,X194)
| X194 != slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( ~ aElementOf0(esk9_2(X193,X197),X197)
| ~ aElementOf0(esk9_2(X193,X197),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk9_2(X193,X197)),X193)
| ~ aSet0(X197)
| X197 = slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( aElementOf0(esk9_2(X193,X197),szNzAzT0)
| aElementOf0(esk9_2(X193,X197),X197)
| ~ aSet0(X197)
| X197 = slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(esk9_2(X193,X197)),X193)
| aElementOf0(esk9_2(X193,X197),X197)
| ~ aSet0(X197)
| X197 = slbdtrb0(X193)
| ~ aElementOf0(X193,szNzAzT0) ) ),
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)],[mDefSeg])])])])])]) ).
fof(i_0_58,plain,
! [X163,X164,X165] :
( ~ aElementOf0(X163,szNzAzT0)
| ~ aElementOf0(X164,szNzAzT0)
| ~ aElementOf0(X165,szNzAzT0)
| ~ sdtlseqdt0(X163,X164)
| ~ sdtlseqdt0(X164,X165)
| sdtlseqdt0(X163,X165) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessTrans])]) ).
fof(i_0_59,plain,
! [X186,X187,X188,X189] :
( ( aElementOf0(X187,X186)
| X187 != szmzazxdt0(X186)
| ~ aSubsetOf0(X186,szNzAzT0)
| ~ isFinite0(X186)
| X186 = slcrc0 )
& ( ~ aElementOf0(X188,X186)
| sdtlseqdt0(X188,X187)
| X187 != szmzazxdt0(X186)
| ~ aSubsetOf0(X186,szNzAzT0)
| ~ isFinite0(X186)
| X186 = slcrc0 )
& ( aElementOf0(esk8_2(X186,X189),X186)
| ~ aElementOf0(X189,X186)
| X189 = szmzazxdt0(X186)
| ~ aSubsetOf0(X186,szNzAzT0)
| ~ isFinite0(X186)
| X186 = slcrc0 )
& ( ~ sdtlseqdt0(esk8_2(X186,X189),X189)
| ~ aElementOf0(X189,X186)
| X189 = szmzazxdt0(X186)
| ~ aSubsetOf0(X186,szNzAzT0)
| ~ isFinite0(X186)
| X186 = slcrc0 ) ),
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)],[mDefMax])])])])])]) ).
fof(i_0_60,plain,
! [X191,X192] :
( ~ aSubsetOf0(X191,szNzAzT0)
| ~ aSubsetOf0(X192,szNzAzT0)
| X191 = slcrc0
| X192 = slcrc0
| ~ aElementOf0(szmzizndt0(X191),X192)
| ~ aElementOf0(szmzizndt0(X192),X191)
| szmzizndt0(X191) = szmzizndt0(X192) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMinMin])]) ).
fof(i_0_61,plain,
! [X200,X201] :
( ( ~ aElementOf0(X200,slbdtrb0(szszuzczcdt0(X201)))
| aElementOf0(X200,slbdtrb0(X201))
| X200 = X201
| ~ aElementOf0(X200,szNzAzT0)
| ~ aElementOf0(X201,szNzAzT0) )
& ( ~ aElementOf0(X200,slbdtrb0(X201))
| aElementOf0(X200,slbdtrb0(szszuzczcdt0(X201)))
| ~ aElementOf0(X200,szNzAzT0)
| ~ aElementOf0(X201,szNzAzT0) )
& ( X200 != X201
| aElementOf0(X200,slbdtrb0(szszuzczcdt0(X201)))
| ~ aElementOf0(X200,szNzAzT0)
| ~ aElementOf0(X201,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSegSucc])])]) ).
fof(i_0_62,plain,
! [X181,X182,X183,X184] :
( ( aElementOf0(X182,X181)
| X182 != szmzizndt0(X181)
| ~ aSubsetOf0(X181,szNzAzT0)
| X181 = slcrc0 )
& ( ~ aElementOf0(X183,X181)
| sdtlseqdt0(X182,X183)
| X182 != szmzizndt0(X181)
| ~ aSubsetOf0(X181,szNzAzT0)
| X181 = slcrc0 )
& ( aElementOf0(esk7_2(X181,X184),X181)
| ~ aElementOf0(X184,X181)
| X184 = szmzizndt0(X181)
| ~ aSubsetOf0(X181,szNzAzT0)
| X181 = slcrc0 )
& ( ~ sdtlseqdt0(X184,esk7_2(X181,X184))
| ~ aElementOf0(X184,X181)
| X184 = szmzizndt0(X181)
| ~ aSubsetOf0(X181,szNzAzT0)
| X181 = slcrc0 ) ),
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)],[mDefMin])])])])])]) ).
fof(i_0_63,plain,
! [X178,X179] :
( ( aSubsetOf0(esk6_2(X178,X179),X178)
| ~ isFinite0(X178)
| ~ sdtlseqdt0(X179,sbrdtbr0(X178))
| ~ aSet0(X178)
| ~ aElementOf0(X179,szNzAzT0) )
& ( sbrdtbr0(esk6_2(X178,X179)) = X179
| ~ isFinite0(X178)
| ~ sdtlseqdt0(X179,sbrdtbr0(X178))
| ~ aSet0(X178)
| ~ aElementOf0(X179,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardSubEx])])])]) ).
fof(i_0_64,plain,
! [X174,X175] :
( ~ aSet0(X174)
| ~ isFinite0(X174)
| ~ aElementOf0(X175,X174)
| szszuzczcdt0(sbrdtbr0(sdtmndt0(X174,X175))) = sbrdtbr0(X174) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardDiff])])]) ).
fof(i_0_65,plain,
! [X157,X158] :
( ( ~ sdtlseqdt0(X157,X158)
| sdtlseqdt0(szszuzczcdt0(X157),szszuzczcdt0(X158))
| ~ aElementOf0(X157,szNzAzT0)
| ~ aElementOf0(X158,szNzAzT0) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X157),szszuzczcdt0(X158))
| sdtlseqdt0(X157,X158)
| ~ aElementOf0(X157,szNzAzT0)
| ~ aElementOf0(X158,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccLess])])]) ).
fof(i_0_66,plain,
! [X202,X203] :
( ( ~ sdtlseqdt0(X202,X203)
| aSubsetOf0(slbdtrb0(X202),slbdtrb0(X203))
| ~ aElementOf0(X202,szNzAzT0)
| ~ aElementOf0(X203,szNzAzT0) )
& ( ~ aSubsetOf0(slbdtrb0(X202),slbdtrb0(X203))
| sdtlseqdt0(X202,X203)
| ~ aElementOf0(X202,szNzAzT0)
| ~ aElementOf0(X203,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSegLess])])]) ).
fof(i_0_67,negated_conjecture,
! [X205,X206,X207] :
( ( aSet0(slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) )
& ( aElementOf0(X206,szNzAzT0)
| ~ aElementOf0(X206,slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(X206),X205)
| ~ aElementOf0(X206,slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) )
& ( ~ aElementOf0(X207,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X207),X205)
| aElementOf0(X207,slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) )
& ( aElementOf0(esk10_1(X205),xS)
| ~ aElementOf0(X205,szNzAzT0) )
& ( ~ aElementOf0(esk10_1(X205),slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) )
& ( ~ aSubsetOf0(xS,slbdtrb0(X205))
| ~ aElementOf0(X205,szNzAzT0) ) ),
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_50])])])])])]) ).
fof(i_0_68,plain,
! [X110,X111,X112,X113] :
( ( aSet0(X111)
| ~ aSubsetOf0(X111,X110)
| ~ aSet0(X110) )
& ( ~ aElementOf0(X112,X111)
| aElementOf0(X112,X110)
| ~ aSubsetOf0(X111,X110)
| ~ aSet0(X110) )
& ( aElementOf0(esk2_2(X110,X113),X113)
| ~ aSet0(X113)
| aSubsetOf0(X113,X110)
| ~ aSet0(X110) )
& ( ~ aElementOf0(esk2_2(X110,X113),X110)
| ~ aSet0(X113)
| aSubsetOf0(X113,X110)
| ~ aSet0(X110) ) ),
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)],[mDefSub])])])])])]) ).
fof(i_0_69,plain,
! [X161,X162] :
( ~ aElementOf0(X161,szNzAzT0)
| ~ aElementOf0(X162,szNzAzT0)
| ~ sdtlseqdt0(X161,X162)
| ~ sdtlseqdt0(X162,X161)
| X161 = X162 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessASymm])]) ).
fof(i_0_70,plain,
! [X120,X121,X122] :
( ~ aSet0(X120)
| ~ aSet0(X121)
| ~ aSet0(X122)
| ~ aSubsetOf0(X120,X121)
| ~ aSubsetOf0(X121,X122)
| aSubsetOf0(X120,X122) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubTrans])]) ).
fof(i_0_71,plain,
! [X172,X173] :
( ~ aSet0(X172)
| ~ isFinite0(X172)
| ~ aElement0(X173)
| aElementOf0(X173,X172)
| sbrdtbr0(sdtpldt0(X172,X173)) = szszuzczcdt0(sbrdtbr0(X172)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])]) ).
fof(i_0_72,plain,
! [X166,X167] :
( ~ aElementOf0(X166,szNzAzT0)
| ~ aElementOf0(X167,szNzAzT0)
| sdtlseqdt0(X166,X167)
| sdtlseqdt0(szszuzczcdt0(X167),X166) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessTotal])]) ).
fof(i_0_73,plain,
! [X137,X138] :
( ~ aSet0(X137)
| ~ aElementOf0(X138,X137)
| sdtpldt0(sdtmndt0(X137,X138),X138) = X137 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mConsDiff])])]) ).
fof(i_0_74,plain,
! [X139,X140] :
( ~ aElement0(X139)
| ~ aSet0(X140)
| aElementOf0(X139,X140)
| sdtmndt0(sdtpldt0(X140,X139),X139) = X140 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])]) ).
fof(i_0_75,plain,
! [X176,X177] :
( ~ aSet0(X176)
| ~ isFinite0(X176)
| ~ aSubsetOf0(X177,X176)
| sdtlseqdt0(sbrdtbr0(X177),sbrdtbr0(X176)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardSub])])]) ).
fof(i_0_76,plain,
! [X118,X119] :
( ~ aSet0(X118)
| ~ aSet0(X119)
| ~ aSubsetOf0(X118,X119)
| ~ aSubsetOf0(X119,X118)
| X118 = X119 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubASymm])]) ).
fof(i_0_77,plain,
! [X150,X151] :
( ~ aElementOf0(X150,szNzAzT0)
| ~ aElementOf0(X151,szNzAzT0)
| szszuzczcdt0(X150) != szszuzczcdt0(X151)
| X150 = X151 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccEquSucc])]) ).
fof(i_0_78,plain,
! [X143,X144] :
( ~ aElement0(X143)
| ~ aSet0(X144)
| ~ isCountable0(X144)
| isCountable0(sdtmndt0(X144,X143)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCDiffSet])])]) ).
fof(i_0_79,plain,
! [X141,X142] :
( ~ aElement0(X141)
| ~ aSet0(X142)
| ~ isCountable0(X142)
| isCountable0(sdtpldt0(X142,X141)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCConsSet])])]) ).
fof(i_0_80,plain,
! [X147,X148] :
( ~ aElement0(X147)
| ~ aSet0(X148)
| ~ isFinite0(X148)
| isFinite0(sdtmndt0(X148,X147)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mFDiffSet])])]) ).
fof(i_0_81,plain,
! [X145,X146] :
( ~ aElement0(X145)
| ~ aSet0(X146)
| ~ isFinite0(X146)
| isFinite0(sdtpldt0(X146,X145)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mFConsSet])])]) ).
fof(i_0_82,plain,
! [X156] :
( ~ aElementOf0(X156,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X156),sz00) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_53])]) ).
fof(i_0_83,plain,
! [X115,X116] :
( ~ aSet0(X115)
| ~ isFinite0(X115)
| ~ aSubsetOf0(X116,X115)
| isFinite0(X116) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubFSet])])]) ).
fof(i_0_84,plain,
! [X170] :
( ( ~ aElementOf0(sbrdtbr0(X170),szNzAzT0)
| isFinite0(X170)
| ~ aSet0(X170) )
& ( ~ isFinite0(X170)
| aElementOf0(sbrdtbr0(X170),szNzAzT0)
| ~ aSet0(X170) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardNum])])]) ).
fof(i_0_85,plain,
! [X152] :
( ( aElementOf0(esk5_1(X152),szNzAzT0)
| X152 = sz00
| ~ aElementOf0(X152,szNzAzT0) )
& ( X152 = szszuzczcdt0(esk5_1(X152))
| X152 = sz00
| ~ aElementOf0(X152,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNatExtra])])])]) ).
fof(i_0_86,plain,
! [X168] :
( ~ aElementOf0(X168,szNzAzT0)
| iLess0(X168,szszuzczcdt0(X168)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIH])]) ).
fof(i_0_87,plain,
! [X159] :
( ~ aElementOf0(X159,szNzAzT0)
| sdtlseqdt0(X159,szszuzczcdt0(X159)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessSucc])]) ).
fof(i_0_88,plain,
! [X149] :
( ( aElementOf0(szszuzczcdt0(X149),szNzAzT0)
| ~ aElementOf0(X149,szNzAzT0) )
& ( szszuzczcdt0(X149) != sz00
| ~ aElementOf0(X149,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccNum])])]) ).
fof(i_0_89,plain,
! [X160] :
( ~ aElementOf0(X160,szNzAzT0)
| sdtlseqdt0(X160,X160) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessRefl])]) ).
fof(i_0_90,plain,
! [X102,X103] :
( ~ aSet0(X102)
| ~ aElementOf0(X103,X102)
| aElement0(X103) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEOfElem])])]) ).
fof(i_0_91,plain,
! [X155] :
( ~ aElementOf0(X155,szNzAzT0)
| sdtlseqdt0(sz00,X155) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroLess])]) ).
fof(i_0_92,hypothesis,
! [X204] :
( aSet0(xS)
& ( ~ aElementOf0(X204,xS)
| aElementOf0(X204,szNzAzT0) )
& aSubsetOf0(xS,szNzAzT0)
& isFinite0(xS) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1986])])]) ).
fof(i_0_93,plain,
! [X199] :
( ~ aElementOf0(X199,szNzAzT0)
| isFinite0(slbdtrb0(X199)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSegFin])]) ).
fof(i_0_94,plain,
! [X104,X105,X106] :
( ( aSet0(X104)
| X104 != slcrc0 )
& ( ~ aElementOf0(X105,X104)
| X104 != slcrc0 )
& ( ~ aSet0(X106)
| aElementOf0(esk1_1(X106),X106)
| X106 = slcrc0 ) ),
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)],[mDefEmp])])])])])]) ).
fof(i_0_95,plain,
! [X154] :
( ~ aElementOf0(X154,szNzAzT0)
| X154 != szszuzczcdt0(X154) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNatNSucc])]) ).
fof(i_0_96,plain,
! [X117] :
( ~ aSet0(X117)
| aSubsetOf0(X117,X117) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubRefl])]) ).
fof(i_0_97,plain,
! [X108] :
( ~ aSet0(X108)
| ~ isCountable0(X108)
| ~ isFinite0(X108) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_54])]) ).
fof(i_0_98,plain,
! [X169] :
( ~ aSet0(X169)
| aElement0(sbrdtbr0(X169)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardS])]) ).
fof(i_0_99,plain,
! [X109] :
( ~ aSet0(X109)
| ~ isCountable0(X109)
| X109 != slcrc0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCountNFin_01])]) ).
fof(i_0_100,plain,
! [X171] :
( ( sbrdtbr0(X171) != sz00
| X171 = slcrc0
| ~ aSet0(X171) )
& ( X171 != slcrc0
| sbrdtbr0(X171) = sz00
| ~ aSet0(X171) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardEmpty])])]) ).
cnf(i_0_101,plain,
( esk4_3(X1,X2,X3) = X2
| X3 = sdtmndt0(X1,X2)
| ~ aElementOf0(esk4_3(X1,X2,X3),X3)
| ~ aElement0(esk4_3(X1,X2,X3))
| ~ aElementOf0(esk4_3(X1,X2,X3),X1)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_102,plain,
( X3 = sdtpldt0(X1,X2)
| ~ aElementOf0(esk3_3(X1,X2,X3),X1)
| ~ aElement0(esk3_3(X1,X2,X3))
| ~ aElementOf0(esk3_3(X1,X2,X3),X3)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_103,plain,
( X3 = sdtpldt0(X1,X2)
| esk3_3(X1,X2,X3) != X2
| ~ aElement0(esk3_3(X1,X2,X3))
| ~ aElementOf0(esk3_3(X1,X2,X3),X3)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_104,plain,
( aElementOf0(esk3_3(X1,X2,X3),X1)
| esk3_3(X1,X2,X3) = X2
| aElementOf0(esk3_3(X1,X2,X3),X3)
| X3 = sdtpldt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_105,plain,
( aElementOf0(esk4_3(X1,X2,X3),X1)
| aElementOf0(esk4_3(X1,X2,X3),X3)
| X3 = sdtmndt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_106,plain,
( X2 = slbdtrb0(X1)
| ~ aElementOf0(esk9_2(X1,X2),X2)
| ~ aElementOf0(esk9_2(X1,X2),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk9_2(X1,X2)),X1)
| ~ aSet0(X2)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_107,plain,
( aElement0(esk4_3(X1,X2,X3))
| aElementOf0(esk4_3(X1,X2,X3),X3)
| X3 = sdtmndt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_108,plain,
( aElement0(esk3_3(X1,X2,X3))
| aElementOf0(esk3_3(X1,X2,X3),X3)
| X3 = sdtpldt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_109,plain,
( aElementOf0(esk4_3(X1,X2,X3),X3)
| X3 = sdtmndt0(X1,X2)
| esk4_3(X1,X2,X3) != X2
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_110,plain,
( sdtlseqdt0(szszuzczcdt0(esk9_2(X1,X2)),X1)
| aElementOf0(esk9_2(X1,X2),X2)
| X2 = slbdtrb0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_111,plain,
( sdtlseqdt0(X1,X3)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_112,plain,
( X2 = szmzazxdt0(X1)
| X1 = slcrc0
| ~ sdtlseqdt0(esk8_2(X1,X2),X2)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ isFinite0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_113,plain,
( X1 = slcrc0
| X2 = slcrc0
| szmzizndt0(X1) = szmzizndt0(X2)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aSubsetOf0(X2,szNzAzT0)
| ~ aElementOf0(szmzizndt0(X1),X2)
| ~ aElementOf0(szmzizndt0(X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_114,plain,
( aElementOf0(X1,slbdtrb0(X2))
| X1 = X2
| ~ aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_115,plain,
( X1 = szmzizndt0(X2)
| X2 = slcrc0
| ~ sdtlseqdt0(X1,esk7_2(X2,X1))
| ~ aElementOf0(X1,X2)
| ~ aSubsetOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_116,plain,
( aElementOf0(esk9_2(X1,X2),szNzAzT0)
| aElementOf0(esk9_2(X1,X2),X2)
| X2 = slbdtrb0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_117,plain,
( aSubsetOf0(esk6_2(X1,X2),X1)
| ~ isFinite0(X1)
| ~ sdtlseqdt0(X2,sbrdtbr0(X1))
| ~ aSet0(X1)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_118,plain,
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))
| ~ aElementOf0(X1,slbdtrb0(X2))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_119,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X2))) = sbrdtbr0(X1)
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_120,plain,
( sbrdtbr0(esk6_2(X1,X2)) = X2
| ~ isFinite0(X1)
| ~ sdtlseqdt0(X2,sbrdtbr0(X1))
| ~ aSet0(X1)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_121,plain,
( aElementOf0(esk8_2(X1,X2),X1)
| X2 = szmzazxdt0(X1)
| X1 = slcrc0
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ isFinite0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_122,plain,
( sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_123,plain,
( sdtlseqdt0(X1,X2)
| ~ aSubsetOf0(slbdtrb0(X1),slbdtrb0(X2))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_124,plain,
( aElementOf0(X1,X3)
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X1),X2)
| X3 != slbdtrb0(X2)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_125,negated_conjecture,
( aElementOf0(X1,slbdtrb0(X2))
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X1),X2)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_126,plain,
( aSubsetOf0(X2,X1)
| ~ aElementOf0(esk2_2(X1,X2),X1)
| ~ aSet0(X2)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_127,plain,
( aElementOf0(esk7_2(X1,X2),X1)
| X2 = szmzizndt0(X1)
| X1 = slcrc0
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_128,plain,
( sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_129,plain,
( aSubsetOf0(slbdtrb0(X1),slbdtrb0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_130,plain,
( X1 = X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_131,plain,
( X1 = X3
| aElementOf0(X1,X4)
| ~ aElement0(X1)
| ~ aElementOf0(X1,X2)
| X4 != sdtmndt0(X2,X3)
| ~ aSet0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_132,plain,
( aElementOf0(X1,X3)
| ~ aElementOf0(X1,X2)
| ~ aElement0(X1)
| X3 != sdtpldt0(X2,X4)
| ~ aSet0(X2)
| ~ aElement0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_133,plain,
( aSubsetOf0(X1,X3)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aSet0(X3)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_134,plain,
( aElementOf0(X1,X2)
| X1 = X3
| ~ aElementOf0(X1,X4)
| X4 != sdtpldt0(X2,X3)
| ~ aSet0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_135,plain,
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))
| X1 != X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_136,plain,
( aElementOf0(X2,X1)
| sbrdtbr0(sdtpldt0(X1,X2)) = szszuzczcdt0(sbrdtbr0(X1))
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_137,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_138,plain,
( aElementOf0(X1,X2)
| ~ aElementOf0(X1,X3)
| X3 != sdtmndt0(X2,X4)
| ~ aSet0(X2)
| ~ aElement0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_139,plain,
( sdtlseqdt0(X1,X3)
| X2 = slcrc0
| ~ aElementOf0(X1,X2)
| X3 != szmzazxdt0(X2)
| ~ aSubsetOf0(X2,szNzAzT0)
| ~ isFinite0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_140,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(X1),X2)
| ~ aElementOf0(X1,slbdtrb0(X2))
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_141,plain,
( sdtlseqdt0(szszuzczcdt0(X1),X2)
| ~ aElementOf0(X1,X3)
| X3 != slbdtrb0(X2)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_142,plain,
( sdtpldt0(sdtmndt0(X1,X2),X2) = X1
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_143,plain,
( aElementOf0(X1,X2)
| sdtmndt0(sdtpldt0(X2,X1),X1) = X2
| ~ aElement0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_144,plain,
( aElementOf0(esk2_2(X1,X2),X2)
| aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_145,plain,
( sdtlseqdt0(X3,X1)
| X2 = slcrc0
| ~ aElementOf0(X1,X2)
| X3 != szmzizndt0(X2)
| ~ aSubsetOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_146,plain,
( aElementOf0(X1,X3)
| ~ aElementOf0(X1,X2)
| ~ aSubsetOf0(X2,X3)
| ~ aSet0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_147,plain,
( aElement0(X1)
| ~ aElementOf0(X1,X2)
| X2 != sdtmndt0(X3,X4)
| ~ aSet0(X3)
| ~ aElement0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_148,plain,
( aElement0(X1)
| ~ aElementOf0(X1,X2)
| X2 != sdtpldt0(X3,X4)
| ~ aSet0(X3)
| ~ aElement0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_149,negated_conjecture,
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,slbdtrb0(X2))
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_150,plain,
( X1 != X2
| ~ aElementOf0(X1,X3)
| X3 != sdtmndt0(X4,X2)
| ~ aSet0(X4)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_151,plain,
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,X2)
| X2 != slbdtrb0(X3)
| ~ aElementOf0(X3,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_152,plain,
( sdtlseqdt0(sbrdtbr0(X2),sbrdtbr0(X1))
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_153,plain,
( aElementOf0(X1,X3)
| X1 != X2
| ~ aElement0(X1)
| X3 != sdtpldt0(X4,X2)
| ~ aSet0(X4)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_154,negated_conjecture,
( ~ aElementOf0(esk10_1(X1),slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_155,plain,
( X1 = X2
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_156,plain,
( X1 = X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| szszuzczcdt0(X1) != szszuzczcdt0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_157,plain,
( isCountable0(sdtmndt0(X2,X1))
| ~ aElement0(X1)
| ~ aSet0(X2)
| ~ isCountable0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_158,plain,
( isCountable0(sdtpldt0(X2,X1))
| ~ aElement0(X1)
| ~ aSet0(X2)
| ~ isCountable0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_159,plain,
( isFinite0(sdtmndt0(X2,X1))
| ~ aElement0(X1)
| ~ aSet0(X2)
| ~ isFinite0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_160,plain,
( isFinite0(sdtpldt0(X2,X1))
| ~ aElement0(X1)
| ~ aSet0(X2)
| ~ isFinite0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_161,plain,
( aElementOf0(X1,X2)
| X2 = slcrc0
| X1 != szmzazxdt0(X2)
| ~ aSubsetOf0(X2,szNzAzT0)
| ~ isFinite0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_162,plain,
( ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X1),sz00) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_163,negated_conjecture,
( ~ aSubsetOf0(xS,slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_164,plain,
( aElementOf0(X1,X2)
| X2 = slcrc0
| X1 != szmzizndt0(X2)
| ~ aSubsetOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_165,plain,
( aSet0(X1)
| X1 != sdtmndt0(X2,X3)
| ~ aSet0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_166,plain,
( aSet0(X1)
| X1 != sdtpldt0(X2,X3)
| ~ aSet0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_167,plain,
( isFinite0(X2)
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_168,plain,
( isFinite0(X1)
| ~ aElementOf0(sbrdtbr0(X1),szNzAzT0)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_169,plain,
( aElementOf0(esk5_1(X1),szNzAzT0)
| X1 = sz00
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_170,plain,
( iLess0(X1,szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_171,plain,
( sdtlseqdt0(X1,szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_172,negated_conjecture,
( aElementOf0(esk10_1(X1),xS)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_173,plain,
( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_174,plain,
( sdtlseqdt0(X1,X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_175,plain,
( aElement0(X2)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_176,plain,
( aSet0(X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_177,plain,
( aElementOf0(sbrdtbr0(X1),szNzAzT0)
| ~ isFinite0(X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_178,plain,
( aSet0(X1)
| X1 != slbdtrb0(X2)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_179,plain,
( X1 = szszuzczcdt0(esk5_1(X1))
| X1 = sz00
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_180,plain,
( sdtlseqdt0(sz00,X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_181,hypothesis,
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,xS) ),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_182,plain,
( isFinite0(slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_183,negated_conjecture,
( aSet0(slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_184,plain,
( aElementOf0(esk1_1(X1),X1)
| X1 = slcrc0
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_185,plain,
( ~ aElementOf0(X1,szNzAzT0)
| X1 != szszuzczcdt0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_186,plain,
( szszuzczcdt0(X1) != sz00
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_187,plain,
( ~ aElementOf0(X1,X2)
| X2 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_188,plain,
( aSubsetOf0(X1,X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_189,plain,
( ~ aSet0(X1)
| ~ isCountable0(X1)
| ~ isFinite0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_190,plain,
( aElement0(sbrdtbr0(X1))
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_191,plain,
( ~ aSet0(X1)
| ~ isCountable0(X1)
| X1 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_192,plain,
( X1 = slcrc0
| sbrdtbr0(X1) != sz00
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_193,plain,
( sbrdtbr0(X1) = sz00
| X1 != slcrc0
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_194,hypothesis,
aSubsetOf0(xS,szNzAzT0),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_195,plain,
aElementOf0(sz00,szNzAzT0),
inference(split_conjunct,[status(thm)],[mZeroNum]),
[final] ).
cnf(i_0_196,plain,
( aSet0(X1)
| X1 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_197,plain,
isCountable0(szNzAzT0),
inference(split_conjunct,[status(thm)],[mNATSet]),
[final] ).
cnf(i_0_198,hypothesis,
isFinite0(xS),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_199,plain,
isFinite0(slcrc0),
inference(split_conjunct,[status(thm)],[mEmpFin]),
[final] ).
cnf(i_0_200,hypothesis,
aSet0(xS),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_201,plain,
aSet0(szNzAzT0),
inference(split_conjunct,[status(thm)],[mNATSet]),
[final] ).
cnf(i_0_202,plain,
slbdtrb0(sz00) = slcrc0,
inference(split_conjunct,[status(thm)],[mSegZero]),
[final] ).
cnf(i_0_203,axiom,
X1 = X1 ).
cnf(i_0_204,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_205,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_206,axiom,
( X1 != X2
| esk4_3(X1,X3,X4) = esk4_3(X2,X3,X4) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| esk4_3(X3,X1,X4) = esk4_3(X3,X2,X4) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| esk4_3(X3,X4,X1) = esk4_3(X3,X4,X2) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| szmzizndt0(X1) = szmzizndt0(X2) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| sbrdtbr0(X1) = sbrdtbr0(X2) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| sdtmndt0(X1,X3) = sdtmndt0(X2,X3) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| sdtmndt0(X3,X1) = sdtmndt0(X3,X2) ) ).
cnf(i_0_213,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_214,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_215,axiom,
( X1 != X2
| esk3_3(X1,X3,X4) = esk3_3(X2,X3,X4) ) ).
cnf(i_0_216,axiom,
( X1 != X2
| esk3_3(X3,X1,X4) = esk3_3(X3,X2,X4) ) ).
cnf(i_0_217,axiom,
( X1 != X2
| esk3_3(X3,X4,X1) = esk3_3(X3,X4,X2) ) ).
cnf(i_0_218,axiom,
( X1 != X2
| slbdtrb0(X1) = slbdtrb0(X2) ) ).
cnf(i_0_219,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_220,axiom,
( X1 != X2
| szmzazxdt0(X1) = szmzazxdt0(X2) ) ).
cnf(i_0_221,axiom,
( X1 != X2
| ~ aElementOf0(X1,X3)
| aElementOf0(X2,X3) ) ).
cnf(i_0_222,axiom,
( X1 != X2
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X2) ) ).
cnf(i_0_223,axiom,
( X1 != X2
| ~ aElement0(X1)
| aElement0(X2) ) ).
cnf(i_0_224,axiom,
( X1 != X2
| ~ aSet0(X1)
| aSet0(X2) ) ).
cnf(i_0_225,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| ~ aSubsetOf0(X1,X3)
| aSubsetOf0(X2,X3) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| ~ aSubsetOf0(X3,X1)
| aSubsetOf0(X3,X2) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| ~ isFinite0(X1)
| isFinite0(X2) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| ~ isCountable0(X1)
| isCountable0(X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_251,plain,
~ aElementOf0(X1,slcrc0),
inference(equality_inference,[],[187]) ).
cnf(i_0_254,plain,
aSet0(slcrc0),
inference(equality_inference,[],[196]) ).
cnf(i_0_257,plain,
~ aElementOf0(esk10_1(sz00),slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_154]) ).
cnf(i_0_259,plain,
iLess0(sz00,szszuzczcdt0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_154,i_0_170]) ).
cnf(i_0_261,plain,
sdtlseqdt0(sz00,szszuzczcdt0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_154,i_0_170,i_0_171]) ).
cnf(i_0_263,plain,
sdtlseqdt0(sz00,sz00),
inference(scs_inference,[],[i_0_195,i_0_154,i_0_170,i_0_171,i_0_174]) ).
cnf(i_0_265,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187]) ).
cnf(i_0_267,plain,
aSubsetOf0(xS,xS),
inference(scs_inference,[],[i_0_195,i_0_200,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188]) ).
cnf(i_0_269,plain,
aSet0(slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_200,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196]) ).
cnf(i_0_271,plain,
slcrc0 = slbdtrb0(sz00),
inference(scs_inference,[],[i_0_195,i_0_200,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204]) ).
cnf(i_0_272,plain,
aElement0(sz00),
inference(scs_inference,[],[i_0_195,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175]) ).
cnf(i_0_303,plain,
aSubsetOf0(szNzAzT0,szNzAzT0),
inference(scs_inference,[],[i_0_201,i_0_188]) ).
cnf(i_0_255,plain,
~ isCountable0(slcrc0),
inference(scs_inference,[],[i_0_254,i_0_252]) ).
cnf(i_0_256,plain,
sbrdtbr0(slcrc0) = sz00,
inference(scs_inference,[],[i_0_254,i_0_253]) ).
cnf(i_0_274,plain,
aElementOf0(sz00,slbdtrb0(szszuzczcdt0(sz00))),
inference(scs_inference,[],[i_0_195,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237]) ).
cnf(i_0_276,plain,
~ isFinite0(szNzAzT0),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189]) ).
cnf(i_0_278,plain,
~ isCountable0(slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191]) ).
cnf(i_0_280,plain,
xS != szNzAzT0,
inference(scs_inference,[],[i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229]) ).
cnf(i_0_281,plain,
szNzAzT0 != slbdtrb0(sz00),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230]) ).
cnf(i_0_282,plain,
~ sdtlseqdt0(szszuzczcdt0(sz00),sz00),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125]) ).
cnf(i_0_284,plain,
sdtlseqdt0(szszuzczcdt0(sz00),szszuzczcdt0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128]) ).
cnf(i_0_286,plain,
aSubsetOf0(slbdtrb0(sz00),slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129]) ).
cnf(i_0_288,plain,
aSubsetOf0(slcrc0,xS),
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144]) ).
cnf(i_0_289,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_291,plain,
~ aSubsetOf0(szNzAzT0,slcrc0),
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_199,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144,i_0_167]) ).
cnf(i_0_293,plain,
sz00 != szszuzczcdt0(sz00),
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_199,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144,i_0_167,i_0_225]) ).
cnf(i_0_294,plain,
szszuzczcdt0(sz00) != sz00,
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_199,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144,i_0_167,i_0_225,i_0_226]) ).
cnf(i_0_296,plain,
~ aSubsetOf0(szNzAzT0,slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_199,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144,i_0_167,i_0_225,i_0_226,i_0_227,i_0_228]) ).
cnf(i_0_297,plain,
szNzAzT0 != slcrc0,
inference(scs_inference,[],[i_0_251,i_0_195,i_0_197,i_0_198,i_0_199,i_0_200,i_0_201,i_0_254,i_0_202,i_0_154,i_0_170,i_0_171,i_0_174,i_0_187,i_0_188,i_0_196,i_0_204,i_0_175,i_0_237,i_0_189,i_0_191,i_0_229,i_0_230,i_0_125,i_0_128,i_0_129,i_0_144,i_0_167,i_0_225,i_0_226,i_0_227,i_0_228,i_0_205]) ).
cnf(i_0_320,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_323,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_365,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_372,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_393,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_404,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_462,plain,
aSet0(szNzAzT0),
inference(equality_inference,[],[458]) ).
cnf(i_0_463,plain,
aSubsetOf0(szNzAzT0,szNzAzT0),
inference(equality_inference,[],[459]) ).
cnf(i_0_468,plain,
aSet0(xS),
inference(equality_inference,[],[464]) ).
cnf(i_0_469,plain,
aSubsetOf0(xS,xS),
inference(equality_inference,[],[465]) ).
cnf(i_0_1097,plain,
aSubsetOf0(slbdtrb0(sz00),xS),
inference(scs_inference,[],[i_0_200,i_0_265,i_0_269,i_0_144]) ).
cnf(i_0_1098,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1558,plain,
aSubsetOf0(slbdtrb0(sz00),slcrc0),
inference(scs_inference,[],[i_0_254,i_0_265,i_0_269,i_0_144]) ).
cnf(i_0_1559,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1562,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1576,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1599,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1605,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1611,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1617,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1623,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1630,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1636,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1640,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1644,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1648,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1652,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1815,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1830,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1837,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1838,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1863,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1875,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1882,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_1885,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2013,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_2016,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2035,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2048,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2116,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2140,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2147,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2158,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2159,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2179,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2184,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2298,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2301,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2302,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2316,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2398,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2409,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2412,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2413,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2424,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2503,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2513,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2598,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2601,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2610,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2740,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2745,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2750,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2751,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2766,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2866,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2873,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_2874,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3002,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3005,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3023,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3108,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_3111,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3228,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3240,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3360,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_3525,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_3637,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_3767,plain,
~ aElementOf0(X1,slbdtrb0(sz00)),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_302,plain,
~ aSubsetOf0(szNzAzT0,slcrc0),
inference(equality_inference,[],[295]) ).
cnf(i_0_305,plain,
sz00 = sbrdtbr0(slcrc0),
inference(scs_inference,[],[i_0_201,i_0_256,i_0_188,i_0_204]) ).
cnf(i_0_306,plain,
aElementOf0(esk1_1(szNzAzT0),szNzAzT0),
inference(scs_inference,[],[i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184]) ).
cnf(i_0_308,plain,
aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0),
inference(scs_inference,[],[i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184,i_0_247]) ).
cnf(i_0_310,plain,
aElementOf0(esk1_1(szNzAzT0),slbdtrb0(szszuzczcdt0(esk1_1(szNzAzT0)))),
inference(scs_inference,[],[i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237]) ).
cnf(i_0_312,plain,
~ sdtlseqdt0(szszuzczcdt0(sz00),sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_282,i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226]) ).
cnf(i_0_313,plain,
szszuzczcdt0(sz00) != sbrdtbr0(slcrc0),
inference(scs_inference,[],[i_0_282,i_0_294,i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205]) ).
cnf(i_0_314,plain,
aElement0(sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_282,i_0_294,i_0_272,i_0_201,i_0_256,i_0_297,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223]) ).
cnf(i_0_315,plain,
slcrc0 != szNzAzT0,
inference(scs_inference,[],[i_0_282,i_0_294,i_0_272,i_0_201,i_0_256,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229]) ).
cnf(i_0_316,plain,
slbdtrb0(sz00) != szNzAzT0,
inference(scs_inference,[],[i_0_286,i_0_282,i_0_294,i_0_296,i_0_272,i_0_201,i_0_256,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227]) ).
cnf(i_0_317,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),sz00),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_294,i_0_296,i_0_272,i_0_201,i_0_256,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241]) ).
cnf(i_0_319,plain,
aSubsetOf0(slbdtrb0(sz00),szNzAzT0),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_201,i_0_269,i_0_256,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144]) ).
cnf(i_0_322,plain,
~ sdtlseqdt0(szszuzczcdt0(esk1_1(szNzAzT0)),sz00),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124]) ).
cnf(i_0_325,plain,
sdtlseqdt0(sz00,esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124,i_0_180]) ).
cnf(i_0_327,plain,
iLess0(esk1_1(szNzAzT0),szszuzczcdt0(esk1_1(szNzAzT0))),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124,i_0_180,i_0_170]) ).
cnf(i_0_329,plain,
sdtlseqdt0(esk1_1(szNzAzT0),szszuzczcdt0(esk1_1(szNzAzT0))),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124,i_0_180,i_0_170,i_0_171]) ).
cnf(i_0_331,plain,
sdtlseqdt0(esk1_1(szNzAzT0),esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124,i_0_180,i_0_170,i_0_171,i_0_174]) ).
cnf(i_0_333,plain,
~ aElementOf0(esk10_1(esk1_1(szNzAzT0)),slbdtrb0(esk1_1(szNzAzT0))),
inference(scs_inference,[],[i_0_195,i_0_286,i_0_282,i_0_265,i_0_294,i_0_296,i_0_272,i_0_251,i_0_201,i_0_269,i_0_256,i_0_271,i_0_276,i_0_297,i_0_199,i_0_188,i_0_204,i_0_184,i_0_247,i_0_237,i_0_226,i_0_205,i_0_223,i_0_229,i_0_227,i_0_241,i_0_144,i_0_124,i_0_180,i_0_170,i_0_171,i_0_174,i_0_154]) ).
cnf(i_0_1332,plain,
isFinite0(slbdtrb0(sz00)),
inference(scs_inference,[],[i_0_1097,i_0_200,i_0_198,i_0_167]) ).
cnf(i_0_1561,plain,
~ aElementOf0(szszuzczcdt0(sz00),sdtpldt0(slcrc0,sz00)),
inference(scs_inference,[],[i_0_254,i_0_294,i_0_251,i_0_265,i_0_272,i_0_269,i_0_144,i_0_236]) ).
cnf(i_0_346,plain,
sdtlseqdt0(sz00,szmzizndt0(szNzAzT0)),
inference(scs_inference,[],[i_0_308,i_0_180]) ).
cnf(i_0_348,plain,
aSubsetOf0(slcrc0,slcrc0),
inference(scs_inference,[],[i_0_308,i_0_254,i_0_180,i_0_188]) ).
cnf(i_0_350,plain,
iLess0(szmzizndt0(szNzAzT0),szszuzczcdt0(szmzizndt0(szNzAzT0))),
inference(scs_inference,[],[i_0_308,i_0_254,i_0_180,i_0_188,i_0_170]) ).
cnf(i_0_352,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),szszuzczcdt0(szmzizndt0(szNzAzT0))),
inference(scs_inference,[],[i_0_308,i_0_254,i_0_180,i_0_188,i_0_170,i_0_171]) ).
cnf(i_0_354,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),szmzizndt0(szNzAzT0)),
inference(scs_inference,[],[i_0_308,i_0_254,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174]) ).
cnf(i_0_356,plain,
~ aElementOf0(esk10_1(szmzizndt0(szNzAzT0)),slbdtrb0(szmzizndt0(szNzAzT0))),
inference(scs_inference,[],[i_0_308,i_0_254,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154]) ).
cnf(i_0_358,plain,
aElement0(esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_306,i_0_308,i_0_201,i_0_254,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175]) ).
cnf(i_0_360,plain,
aElementOf0(szmzizndt0(szNzAzT0),slbdtrb0(szszuzczcdt0(szmzizndt0(szNzAzT0)))),
inference(scs_inference,[],[i_0_306,i_0_308,i_0_201,i_0_254,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237]) ).
cnf(i_0_362,plain,
~ sdtlseqdt0(szszuzczcdt0(esk1_1(szNzAzT0)),sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_306,i_0_322,i_0_308,i_0_201,i_0_254,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226]) ).
cnf(i_0_363,plain,
szmzizndt0(szNzAzT0) != szszuzczcdt0(sz00),
inference(scs_inference,[],[i_0_282,i_0_306,i_0_322,i_0_308,i_0_317,i_0_201,i_0_254,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226,i_0_225]) ).
cnf(i_0_364,plain,
aSubsetOf0(slcrc0,szNzAzT0),
inference(scs_inference,[],[i_0_282,i_0_306,i_0_322,i_0_308,i_0_317,i_0_251,i_0_201,i_0_254,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226,i_0_225,i_0_144]) ).
cnf(i_0_367,plain,
sdtlseqdt0(szszuzczcdt0(esk1_1(szNzAzT0)),szszuzczcdt0(esk1_1(szNzAzT0))),
inference(scs_inference,[],[i_0_282,i_0_331,i_0_306,i_0_322,i_0_308,i_0_317,i_0_251,i_0_201,i_0_254,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226,i_0_225,i_0_144,i_0_128]) ).
cnf(i_0_369,plain,
aSubsetOf0(slbdtrb0(esk1_1(szNzAzT0)),slbdtrb0(esk1_1(szNzAzT0))),
inference(scs_inference,[],[i_0_282,i_0_331,i_0_306,i_0_322,i_0_308,i_0_317,i_0_251,i_0_201,i_0_254,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226,i_0_225,i_0_144,i_0_128,i_0_129]) ).
cnf(i_0_371,plain,
~ sdtlseqdt0(szszuzczcdt0(szmzizndt0(szNzAzT0)),sz00),
inference(scs_inference,[],[i_0_195,i_0_282,i_0_331,i_0_306,i_0_322,i_0_308,i_0_317,i_0_251,i_0_365,i_0_201,i_0_254,i_0_271,i_0_256,i_0_180,i_0_188,i_0_170,i_0_171,i_0_174,i_0_154,i_0_175,i_0_237,i_0_226,i_0_225,i_0_144,i_0_128,i_0_129,i_0_124]) ).
cnf(i_0_377,plain,
aElement0(szmzizndt0(szNzAzT0)),
inference(scs_inference,[],[i_0_308,i_0_201,i_0_175]) ).
cnf(i_0_379,plain,
sz00 != szszuzczcdt0(esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_322,i_0_308,i_0_263,i_0_201,i_0_175,i_0_225]) ).
cnf(i_0_391,plain,
szmzizndt0(szNzAzT0) != szszuzczcdt0(esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_322,i_0_317,i_0_225]) ).
cnf(i_0_523,plain,
aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0),
inference(equality_inference,[],[506]) ).
cnf(i_0_524,plain,
~ sdtlseqdt0(szszuzczcdt0(szmzizndt0(szNzAzT0)),sz00),
inference(equality_inference,[],[508]) ).
cnf(i_0_525,plain,
sdtlseqdt0(sz00,szmzizndt0(szNzAzT0)),
inference(equality_inference,[],[510]) ).
cnf(i_0_526,plain,
iLess0(szmzizndt0(szNzAzT0),szszuzczcdt0(szmzizndt0(szNzAzT0))),
inference(equality_inference,[],[512]) ).
cnf(i_0_527,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),szszuzczcdt0(szmzizndt0(szNzAzT0))),
inference(equality_inference,[],[514]) ).
cnf(i_0_528,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),szmzizndt0(szNzAzT0)),
inference(equality_inference,[],[516]) ).
cnf(i_0_529,plain,
~ aElementOf0(esk10_1(szmzizndt0(szNzAzT0)),slbdtrb0(szmzizndt0(szNzAzT0))),
inference(equality_inference,[],[518]) ).
cnf(i_0_550,plain,
sdtlseqdt0(szmzizndt0(szNzAzT0),esk1_1(szNzAzT0)),
inference(scs_inference,[],[i_0_306,i_0_297,i_0_303,i_0_241]) ).
cnf(i_0_1574,plain,
~ aElementOf0(szszuzczcdt0(sz00),sdtpldt0(slcrc0,sz00)),
inference(equality_inference,[],[1564]) ).
cnf(i_0_1575,plain,
~ aElementOf0(szszuzczcdt0(sz00),sdtpldt0(slcrc0,sbrdtbr0(slcrc0))),
inference(scs_inference,[],[i_0_254,i_0_251,i_0_313,i_0_314,i_0_236]) ).
cnf(i_0_1723,plain,
esk4_3(sz00,X1,X2) = esk4_3(sbrdtbr0(slcrc0),X1,X2),
inference(scs_inference,[],[i_0_305,i_0_206]) ).
cnf(i_0_1724,plain,
esk4_3(X1,sz00,X2) = esk4_3(X1,sbrdtbr0(slcrc0),X2),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207]) ).
cnf(i_0_1725,plain,
esk4_3(X1,X2,sz00) = esk4_3(X1,X2,sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208]) ).
cnf(i_0_1726,plain,
szmzizndt0(sz00) = szmzizndt0(sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209]) ).
cnf(i_0_1727,plain,
sbrdtbr0(sz00) = sbrdtbr0(sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210]) ).
cnf(i_0_1728,plain,
sdtmndt0(sz00,X1) = sdtmndt0(sbrdtbr0(slcrc0),X1),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211]) ).
cnf(i_0_1729,plain,
sdtmndt0(X1,sz00) = sdtmndt0(X1,sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212]) ).
cnf(i_0_1730,plain,
sdtpldt0(sz00,X1) = sdtpldt0(sbrdtbr0(slcrc0),X1),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213]) ).
cnf(i_0_1731,plain,
sdtpldt0(X1,sz00) = sdtpldt0(X1,sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214]) ).
cnf(i_0_1732,plain,
esk3_3(sz00,X1,X2) = esk3_3(sbrdtbr0(slcrc0),X1,X2),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215]) ).
cnf(i_0_1733,plain,
esk3_3(X1,sz00,X2) = esk3_3(X1,sbrdtbr0(slcrc0),X2),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216]) ).
cnf(i_0_1734,plain,
esk3_3(X1,X2,sz00) = esk3_3(X1,X2,sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217]) ).
cnf(i_0_1735,plain,
slbdtrb0(sz00) = slbdtrb0(sbrdtbr0(slcrc0)),
inference(scs_inference,[],[i_0_305,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218]) ).
cnf(c_0_363,plain,
( sdtlseqdt0(X1,X2)
| X3 = slcrc0
| ~ aElementOf0(X1,X3)
| X2 != szmzazxdt0(X3)
| ~ aSubsetOf0(X3,szNzAzT0)
| ~ isFinite0(X3) ),
i_0_139 ).
cnf(c_0_364,plain,
( X1 = slcrc0
| sdtlseqdt0(X2,szmzazxdt0(X1))
| ~ isFinite0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,X1) ),
inference(er,[status(thm)],[c_0_363]) ).
cnf(c_0_365,hypothesis,
aSubsetOf0(xS,szNzAzT0),
i_0_194 ).
cnf(c_0_366,hypothesis,
isFinite0(xS),
i_0_198 ).
cnf(c_0_367,plain,
( aElementOf0(X1,X2)
| X2 = slcrc0
| X1 != szmzazxdt0(X2)
| ~ aSubsetOf0(X2,szNzAzT0)
| ~ isFinite0(X2) ),
i_0_161 ).
cnf(c_0_368,hypothesis,
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,xS) ),
i_0_181 ).
cnf(c_0_369,negated_conjecture,
( aElementOf0(esk10_1(X1),xS)
| ~ aElementOf0(X1,szNzAzT0) ),
i_0_172 ).
cnf(c_0_370,hypothesis,
( xS = slcrc0
| sdtlseqdt0(X1,szmzazxdt0(xS))
| ~ aElementOf0(X1,xS) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_364,c_0_365]),c_0_366])]) ).
cnf(c_0_371,plain,
( X1 = slcrc0
| aElementOf0(szmzazxdt0(X1),X1)
| ~ isFinite0(X1)
| ~ aSubsetOf0(X1,szNzAzT0) ),
inference(er,[status(thm)],[c_0_367]) ).
cnf(c_0_372,negated_conjecture,
( ~ aElementOf0(esk10_1(X1),slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
i_0_154 ).
cnf(c_0_373,negated_conjecture,
( aElementOf0(X1,slbdtrb0(X2))
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X1),X2)
| ~ aElementOf0(X2,szNzAzT0) ),
i_0_125 ).
cnf(c_0_374,hypothesis,
( aElementOf0(esk10_1(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_368,c_0_369]) ).
cnf(c_0_375,negated_conjecture,
( xS = slcrc0
| sdtlseqdt0(esk10_1(X1),szmzazxdt0(xS))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_370,c_0_369]) ).
cnf(c_0_376,plain,
( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
i_0_173 ).
cnf(c_0_377,hypothesis,
( xS = slcrc0
| aElementOf0(szmzazxdt0(xS),xS) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_371,c_0_365]),c_0_366])]) ).
cnf(c_0_378,negated_conjecture,
( ~ sdtlseqdt0(szszuzczcdt0(esk10_1(X1)),X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_372,c_0_373]),c_0_374]) ).
cnf(c_0_379,plain,
( sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
i_0_128 ).
cnf(c_0_380,plain,
( xS = slcrc0
| sdtlseqdt0(esk10_1(szszuzczcdt0(X1)),szmzazxdt0(xS))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_375,c_0_376]) ).
cnf(c_0_381,hypothesis,
( xS = slcrc0
| aElementOf0(szmzazxdt0(xS),szNzAzT0) ),
inference(spm,[status(thm)],[c_0_368,c_0_377]) ).
cnf(c_0_382,negated_conjecture,
( ~ sdtlseqdt0(esk10_1(szszuzczcdt0(X1)),X1)
| ~ aElementOf0(esk10_1(szszuzczcdt0(X1)),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_378,c_0_379]),c_0_376]) ).
cnf(c_0_383,hypothesis,
( xS = slcrc0
| sdtlseqdt0(esk10_1(szszuzczcdt0(szmzazxdt0(xS))),szmzazxdt0(xS)) ),
inference(spm,[status(thm)],[c_0_380,c_0_381]) ).
cnf(c_0_384,negated_conjecture,
( xS = slcrc0
| ~ aElementOf0(esk10_1(szszuzczcdt0(szmzazxdt0(xS))),szNzAzT0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_382,c_0_383]),c_0_381]) ).
cnf(c_0_385,negated_conjecture,
( ~ aSubsetOf0(xS,slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
i_0_163 ).
cnf(c_0_386,plain,
slcrc0 = slbdtrb0(sz00),
i_0_271 ).
cnf(c_0_387,plain,
aElementOf0(sz00,szNzAzT0),
i_0_195 ).
cnf(c_0_388,hypothesis,
( xS = slcrc0
| ~ aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0) ),
inference(spm,[status(thm)],[c_0_384,c_0_374]) ).
cnf(c_0_389,plain,
~ aSubsetOf0(xS,slcrc0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_385,c_0_386]),c_0_387])]) ).
cnf(c_0_390,plain,
xS = slcrc0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_388,c_0_376]),c_0_381]) ).
cnf(c_0_391,plain,
aSubsetOf0(slcrc0,slcrc0),
i_0_348 ).
cnf(c_0_392,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_389,c_0_390]),c_0_391])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM543+2 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n011.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Tue May 5 00:43:02 EDT 2026
% 0.16/0.32 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 175.19/124.92 % Version : CSE_E---1.7
% 175.19/124.92 % Problem : theBenchmark.p
% 175.19/124.92 % SZS status Theorem for theBenchmark.p
% 175.19/124.92 % SZS output start CNFRefutation
% See solution above
% 190.19/139.96 % Total time : 124.556s
%------------------------------------------------------------------------------