%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG074+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:05:14 PM UTC 2026
% Result : Theorem 0.31s 5.62s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 92)
% Comments :
%------------------------------------------------------------------------------
fof(mDistr2,axiom,
! [X1,X2,X3,X4] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3)
& aScalar0(X4) )
=> sdtasdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X4)) = sdtpldt0(sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X1,X4)),sdtpldt0(sdtasdt0(X2,X3),sdtasdt0(X2,X4))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDistr2) ).
fof(m__1652,hypothesis,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( aDimensionOf0(X1) = aDimensionOf0(X2)
=> ( iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X2),sdtasasdt0(X1,X2)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X2,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1652) ).
fof(mDefSPN,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( ( aDimensionOf0(X1) = aDimensionOf0(X2)
& aDimensionOf0(X2) != sz00 )
=> sdtasasdt0(X1,X2) = sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X2)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X2,aDimensionOf0(X2)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSPN) ).
fof(mDefInit,axiom,
! [X1] :
( aVector0(X1)
=> ( aDimensionOf0(X1) != sz00
=> ! [X2] :
( X2 = sziznziztdt0(X1)
<=> ( aVector0(X2)
& szszuzczcdt0(aDimensionOf0(X2)) = aDimensionOf0(X1)
& ! [X3] :
( aNaturalNumber0(X3)
=> sdtlbdtrb0(X2,X3) = sdtlbdtrb0(X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefInit) ).
fof(mLEMonM,axiom,
! [X1,X2,X3,X4] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3)
& aScalar0(X4) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(sz0z00,X3)
& sdtlseqdt0(X3,X4) )
=> sdtlseqdt0(sdtasdt0(X1,X3),sdtasdt0(X2,X4)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMonM) ).
fof(mLEMon,axiom,
! [X1,X2,X3,X4] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3)
& aScalar0(X4) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X3,X4) )
=> sdtlseqdt0(sdtpldt0(X1,X3),sdtpldt0(X2,X4)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMon) ).
fof(mDistr,axiom,
! [X1,X2,X3] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(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',mDistr) ).
fof(mSqrt,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(sz0z00,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtasdt0(X1,X1) = sdtasdt0(X2,X2) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqrt) ).
fof(mArith,axiom,
! [X1,X2,X3] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
& sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
& sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
& sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(mPosMon,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(sz0z00,X1)
& sdtlseqdt0(sz0z00,X2) )
=> ( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
& sdtlseqdt0(sz0z00,sdtasdt0(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mPosMon) ).
fof(m__2590,hypothesis,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2590) ).
fof(mLETrn,axiom,
! [X1,X2,X3] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETrn) ).
fof(mMNeg,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( sdtasdt0(X1,smndt0(X2)) = smndt0(sdtasdt0(X1,X2))
& sdtasdt0(smndt0(X1),X2) = smndt0(sdtasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMNeg) ).
fof(mLEASm,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
fof(mScPr,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( aDimensionOf0(X1) = aDimensionOf0(X2)
=> aScalar0(sdtasasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScPr) ).
fof(mMDNeg,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> sdtasdt0(smndt0(X1),smndt0(X2)) = sdtasdt0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMDNeg) ).
fof(mEqInit,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( ( aDimensionOf0(X1) = aDimensionOf0(X2)
& aDimensionOf0(X2) != sz00 )
=> aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEqInit) ).
fof(mDefSPZ,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( ( aDimensionOf0(X1) = aDimensionOf0(X2)
& aDimensionOf0(X2) = sz00 )
=> sdtasasdt0(X1,X2) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSPZ) ).
fof(mScSqPos,axiom,
! [X1] :
( aVector0(X1)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScSqPos) ).
fof(mSqPos,axiom,
! [X1] :
( aScalar0(X1)
=> sdtlseqdt0(sz0z00,sdtasdt0(X1,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqPos) ).
fof(mElmSc,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aNaturalNumber0(X2) )
=> aScalar0(sdtlbdtrb0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mElmSc) ).
fof(mMulSc,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> aScalar0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(mSumSc,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> aScalar0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
fof(mLETot,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETot) ).
fof(mSuccEqu,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( szszuzczcdt0(X1) = szszuzczcdt0(X2)
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccEqu) ).
fof(mIH,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> iLess0(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH) ).
fof(mScZero,axiom,
! [X1] :
( aScalar0(X1)
=> ( sdtpldt0(X1,sz0z00) = X1
& sdtpldt0(sz0z00,X1) = X1
& sdtasdt0(X1,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X1) = sz0z00
& sdtpldt0(X1,smndt0(X1)) = sz0z00
& sdtpldt0(smndt0(X1),X1) = sz0z00
& smndt0(smndt0(X1)) = X1
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(mLERef,axiom,
! [X1] :
( aScalar0(X1)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERef) ).
fof(mNatExtr,axiom,
! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00 )
=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = szszuzczcdt0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNatExtr) ).
fof(mNegSc,axiom,
! [X1] :
( aScalar0(X1)
=> aScalar0(smndt0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(mDimNat,axiom,
! [X1] :
( aVector0(X1)
=> aNaturalNumber0(aDimensionOf0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDimNat) ).
fof(mSuccNat,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( aNaturalNumber0(szszuzczcdt0(X1))
& szszuzczcdt0(X1) != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNat) ).
fof(m__2405,hypothesis,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2405) ).
fof(m__2654,hypothesis,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2654) ).
fof(m__2104,hypothesis,
sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2104) ).
fof(m__1967,hypothesis,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1967) ).
fof(m__2610,hypothesis,
sdtlseqdt0(sdtpldt0(xR,xS),sdtpldt0(xP,xP)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2610) ).
fof(m__2004,hypothesis,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2004) ).
fof(m__2628,hypothesis,
( sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
& sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2628) ).
fof(m__2679,hypothesis,
sdtpldt0(xR,xS) = sdtpldt0(xP,xP),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2679) ).
fof(m__1766,hypothesis,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1766) ).
fof(m__1746,hypothesis,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1746) ).
fof(m__1949,hypothesis,
( aScalar0(xN)
& xN = sdtasdt0(xR,xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1949) ).
fof(m__1930,hypothesis,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
fof(m__1911,hypothesis,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
fof(m__1892,hypothesis,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
fof(m__1873,hypothesis,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1873) ).
fof(m__1854,hypothesis,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1854) ).
fof(m__1837,hypothesis,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(m__1820,hypothesis,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1820) ).
fof(m__1800,hypothesis,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1800) ).
fof(m__1783,hypothesis,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1783) ).
fof(m__1678_01,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1678_01) ).
fof(m__1692,hypothesis,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1692) ).
fof(m__1726,hypothesis,
( aVector0(xq)
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1726) ).
fof(m__1709,hypothesis,
( aVector0(xp)
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1709) ).
fof(m__1678,hypothesis,
( aVector0(xs)
& aVector0(xt) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1678) ).
fof(mSZeroSc,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
fof(mZeroNat,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroNat) ).
fof(i_0_59,plain,
! [X94,X95,X96,X97] :
( ~ aScalar0(X94)
| ~ aScalar0(X95)
| ~ aScalar0(X96)
| ~ aScalar0(X97)
| sdtasdt0(sdtpldt0(X94,X95),sdtpldt0(X96,X97)) = sdtpldt0(sdtpldt0(sdtasdt0(X94,X96),sdtasdt0(X94,X97)),sdtpldt0(sdtasdt0(X95,X96),sdtasdt0(X95,X97))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr2])]) ).
fof(i_0_60,hypothesis,
! [X140,X141] :
( ~ aVector0(X140)
| ~ aVector0(X141)
| aDimensionOf0(X140) != aDimensionOf0(X141)
| ~ iLess0(aDimensionOf0(X140),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X140,X141),sdtasasdt0(X140,X141)),sdtasdt0(sdtasasdt0(X140,X140),sdtasasdt0(X141,X141))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1652])]) ).
fof(i_0_61,plain,
! [X137,X138] :
( ~ aVector0(X137)
| ~ aVector0(X138)
| aDimensionOf0(X137) != aDimensionOf0(X138)
| aDimensionOf0(X138) = sz00
| sdtasasdt0(X137,X138) = sdtpldt0(sdtasasdt0(sziznziztdt0(X137),sziznziztdt0(X138)),sdtasdt0(sdtlbdtrb0(X137,aDimensionOf0(X137)),sdtlbdtrb0(X138,aDimensionOf0(X138)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPN])]) ).
fof(i_0_62,plain,
! [X126,X127,X128,X129] :
( ( aVector0(X127)
| X127 != sziznziztdt0(X126)
| aDimensionOf0(X126) = sz00
| ~ aVector0(X126) )
& ( szszuzczcdt0(aDimensionOf0(X127)) = aDimensionOf0(X126)
| X127 != sziznziztdt0(X126)
| aDimensionOf0(X126) = sz00
| ~ aVector0(X126) )
& ( ~ aNaturalNumber0(X128)
| sdtlbdtrb0(X127,X128) = sdtlbdtrb0(X126,X128)
| X127 != sziznziztdt0(X126)
| aDimensionOf0(X126) = sz00
| ~ aVector0(X126) )
& ( aNaturalNumber0(esk2_2(X126,X129))
| ~ aVector0(X129)
| szszuzczcdt0(aDimensionOf0(X129)) != aDimensionOf0(X126)
| X129 = sziznziztdt0(X126)
| aDimensionOf0(X126) = sz00
| ~ aVector0(X126) )
& ( sdtlbdtrb0(X129,esk2_2(X126,X129)) != sdtlbdtrb0(X126,esk2_2(X126,X129))
| ~ aVector0(X129)
| szszuzczcdt0(aDimensionOf0(X129)) != aDimensionOf0(X126)
| X129 = sziznziztdt0(X126)
| aDimensionOf0(X126) = sz00
| ~ aVector0(X126) ) ),
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)],[mDefInit])])])])])]) ).
fof(i_0_63,plain,
! [X112,X113,X114,X115] :
( ~ aScalar0(X112)
| ~ aScalar0(X113)
| ~ aScalar0(X114)
| ~ aScalar0(X115)
| ~ sdtlseqdt0(X112,X113)
| ~ sdtlseqdt0(sz0z00,X114)
| ~ sdtlseqdt0(X114,X115)
| sdtlseqdt0(sdtasdt0(X112,X114),sdtasdt0(X113,X115)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMonM])]) ).
fof(i_0_64,plain,
! [X108,X109,X110,X111] :
( ~ aScalar0(X108)
| ~ aScalar0(X109)
| ~ aScalar0(X110)
| ~ aScalar0(X111)
| ~ sdtlseqdt0(X108,X109)
| ~ sdtlseqdt0(X110,X111)
| sdtlseqdt0(sdtpldt0(X108,X110),sdtpldt0(X109,X111)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMon])]) ).
fof(i_0_65,plain,
! [X91,X92,X93] :
( ( sdtasdt0(X91,sdtpldt0(X92,X93)) = sdtpldt0(sdtasdt0(X91,X92),sdtasdt0(X91,X93))
| ~ aScalar0(X91)
| ~ aScalar0(X92)
| ~ aScalar0(X93) )
& ( sdtasdt0(sdtpldt0(X91,X92),X93) = sdtpldt0(sdtasdt0(X91,X93),sdtasdt0(X92,X93))
| ~ aScalar0(X91)
| ~ aScalar0(X92)
| ~ aScalar0(X93) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr])])]) ).
fof(i_0_66,plain,
! [X121,X122] :
( ~ aScalar0(X121)
| ~ aScalar0(X122)
| ~ sdtlseqdt0(sz0z00,X121)
| ~ sdtlseqdt0(sz0z00,X122)
| sdtasdt0(X121,X121) != sdtasdt0(X122,X122)
| X121 = X122 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqrt])]) ).
fof(i_0_67,plain,
! [X88,X89,X90] :
( ( sdtpldt0(sdtpldt0(X88,X89),X90) = sdtpldt0(X88,sdtpldt0(X89,X90))
| ~ aScalar0(X88)
| ~ aScalar0(X89)
| ~ aScalar0(X90) )
& ( sdtpldt0(X88,X89) = sdtpldt0(X89,X88)
| ~ aScalar0(X88)
| ~ aScalar0(X89)
| ~ aScalar0(X90) )
& ( sdtasdt0(sdtasdt0(X88,X89),X90) = sdtasdt0(X88,sdtasdt0(X89,X90))
| ~ aScalar0(X88)
| ~ aScalar0(X89)
| ~ aScalar0(X90) )
& ( sdtasdt0(X88,X89) = sdtasdt0(X89,X88)
| ~ aScalar0(X88)
| ~ aScalar0(X89)
| ~ aScalar0(X90) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mArith])])]) ).
fof(i_0_68,plain,
! [X118,X119] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X118,X119))
| ~ sdtlseqdt0(sz0z00,X118)
| ~ sdtlseqdt0(sz0z00,X119)
| ~ aScalar0(X118)
| ~ aScalar0(X119) )
& ( sdtlseqdt0(sz0z00,sdtasdt0(X118,X119))
| ~ sdtlseqdt0(sz0z00,X118)
| ~ sdtlseqdt0(sz0z00,X119)
| ~ aScalar0(X118)
| ~ aScalar0(X119) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mPosMon])])]) ).
fof(i_0_69,hypothesis,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(fof_simplification,[status(thm)],[m__2590]) ).
fof(i_0_70,plain,
! [X105,X106,X107] :
( ~ aScalar0(X105)
| ~ aScalar0(X106)
| ~ aScalar0(X107)
| ~ sdtlseqdt0(X105,X106)
| ~ sdtlseqdt0(X106,X107)
| sdtlseqdt0(X105,X107) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETrn])]) ).
fof(i_0_71,plain,
! [X98,X99] :
( ( sdtasdt0(X98,smndt0(X99)) = smndt0(sdtasdt0(X98,X99))
| ~ aScalar0(X98)
| ~ aScalar0(X99) )
& ( sdtasdt0(smndt0(X98),X99) = smndt0(sdtasdt0(X98,X99))
| ~ aScalar0(X98)
| ~ aScalar0(X99) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMNeg])])]) ).
fof(i_0_72,plain,
! [X103,X104] :
( ~ aScalar0(X103)
| ~ aScalar0(X104)
| ~ sdtlseqdt0(X103,X104)
| ~ sdtlseqdt0(X104,X103)
| X103 = X104 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEASm])]) ).
fof(i_0_73,plain,
! [X133,X134] :
( ~ aVector0(X133)
| ~ aVector0(X134)
| aDimensionOf0(X133) != aDimensionOf0(X134)
| aScalar0(sdtasasdt0(X133,X134)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScPr])]) ).
fof(i_0_74,plain,
! [X100,X101] :
( ~ aScalar0(X100)
| ~ aScalar0(X101)
| sdtasdt0(smndt0(X100),smndt0(X101)) = sdtasdt0(X100,X101) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMDNeg])]) ).
fof(i_0_75,plain,
! [X131,X132] :
( ~ aVector0(X131)
| ~ aVector0(X132)
| aDimensionOf0(X131) != aDimensionOf0(X132)
| aDimensionOf0(X132) = sz00
| aDimensionOf0(sziznziztdt0(X131)) = aDimensionOf0(sziznziztdt0(X132)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEqInit])]) ).
fof(i_0_76,plain,
! [X135,X136] :
( ~ aVector0(X135)
| ~ aVector0(X136)
| aDimensionOf0(X135) != aDimensionOf0(X136)
| aDimensionOf0(X136) != sz00
| sdtasasdt0(X135,X136) = sz0z00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPZ])]) ).
fof(i_0_77,plain,
! [X139] :
( ~ aVector0(X139)
| sdtlseqdt0(sz0z00,sdtasasdt0(X139,X139)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScSqPos])]) ).
fof(i_0_78,plain,
! [X120] :
( ~ aScalar0(X120)
| sdtlseqdt0(sz0z00,sdtasdt0(X120,X120)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqPos])]) ).
fof(i_0_79,plain,
! [X124,X125] :
( ~ aVector0(X124)
| ~ aNaturalNumber0(X125)
| aScalar0(sdtlbdtrb0(X124,X125)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mElmSc])]) ).
fof(i_0_80,plain,
! [X84,X85] :
( ~ aScalar0(X84)
| ~ aScalar0(X85)
| aScalar0(sdtasdt0(X84,X85)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulSc])]) ).
fof(i_0_81,plain,
! [X82,X83] :
( ~ aScalar0(X82)
| ~ aScalar0(X83)
| aScalar0(sdtpldt0(X82,X83)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSumSc])]) ).
fof(i_0_82,plain,
! [X116,X117] :
( ~ aScalar0(X116)
| ~ aScalar0(X117)
| sdtlseqdt0(X116,X117)
| sdtlseqdt0(X117,X116) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETot])]) ).
fof(i_0_83,plain,
! [X79,X80] :
( ~ aNaturalNumber0(X79)
| ~ aNaturalNumber0(X80)
| szszuzczcdt0(X79) != szszuzczcdt0(X80)
| X79 = X80 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccEqu])]) ).
fof(i_0_84,plain,
! [X81] :
( ~ aNaturalNumber0(X81)
| iLess0(X81,szszuzczcdt0(X81)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIH])]) ).
fof(i_0_85,plain,
! [X87] :
( ( sdtpldt0(X87,sz0z00) = X87
| ~ aScalar0(X87) )
& ( sdtpldt0(sz0z00,X87) = X87
| ~ aScalar0(X87) )
& ( sdtasdt0(X87,sz0z00) = sz0z00
| ~ aScalar0(X87) )
& ( sdtasdt0(sz0z00,X87) = sz0z00
| ~ aScalar0(X87) )
& ( sdtpldt0(X87,smndt0(X87)) = sz0z00
| ~ aScalar0(X87) )
& ( sdtpldt0(smndt0(X87),X87) = sz0z00
| ~ aScalar0(X87) )
& ( smndt0(smndt0(X87)) = X87
| ~ aScalar0(X87) )
& ( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X87) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScZero])])]) ).
fof(i_0_86,plain,
! [X102] :
( ~ aScalar0(X102)
| sdtlseqdt0(X102,X102) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLERef])]) ).
fof(i_0_87,plain,
! [X77] :
( ( aNaturalNumber0(esk1_1(X77))
| ~ aNaturalNumber0(X77)
| X77 = sz00 )
& ( X77 = szszuzczcdt0(esk1_1(X77))
| ~ aNaturalNumber0(X77)
| X77 = sz00 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNatExtr])])])]) ).
fof(i_0_88,plain,
! [X86] :
( ~ aScalar0(X86)
| aScalar0(smndt0(X86)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNegSc])]) ).
fof(i_0_89,plain,
! [X123] :
( ~ aVector0(X123)
| aNaturalNumber0(aDimensionOf0(X123)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDimNat])]) ).
fof(i_0_90,plain,
! [X76] :
( ( aNaturalNumber0(szszuzczcdt0(X76))
| ~ aNaturalNumber0(X76) )
& ( szszuzczcdt0(X76) != sz00
| ~ aNaturalNumber0(X76) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccNat])])]) ).
cnf(i_0_91,plain,
( sdtasdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X4)) = sdtpldt0(sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X1,X4)),sdtpldt0(sdtasdt0(X2,X3),sdtasdt0(X2,X4)))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_92,hypothesis,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X2),sdtasasdt0(X1,X2)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X2,X2)))
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs)) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_93,plain,
( aDimensionOf0(X2) = sz00
| sdtasasdt0(X1,X2) = sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X2)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X2,aDimensionOf0(X2))))
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_94,hypothesis,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(split_conjunct,[status(thm)],[m__2405]),
[final] ).
cnf(i_0_95,hypothesis,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
inference(split_conjunct,[status(thm)],[m__2654]),
[final] ).
cnf(i_0_96,hypothesis,
sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))),
inference(split_conjunct,[status(thm)],[m__2104]),
[final] ).
cnf(i_0_97,plain,
( X1 = sziznziztdt0(X2)
| aDimensionOf0(X2) = sz00
| sdtlbdtrb0(X1,esk2_2(X2,X1)) != sdtlbdtrb0(X2,esk2_2(X2,X1))
| ~ aVector0(X1)
| szszuzczcdt0(aDimensionOf0(X1)) != aDimensionOf0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_98,plain,
( sdtlseqdt0(sdtasdt0(X1,X3),sdtasdt0(X2,X4))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X4)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(sz0z00,X3)
| ~ sdtlseqdt0(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_99,plain,
( sdtlseqdt0(sdtpldt0(X1,X3),sdtpldt0(X2,X4))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X4)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_100,plain,
( sdtasdt0(sdtpldt0(X1,X2),X3) = sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_101,plain,
( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_102,plain,
( X1 = X2
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| sdtasdt0(X1,X1) != sdtasdt0(X2,X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_103,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_104,plain,
( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_105,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_106,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_107,hypothesis,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_108,plain,
( sdtlseqdt0(X1,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_109,plain,
( aNaturalNumber0(esk2_2(X1,X2))
| X2 = sziznziztdt0(X1)
| aDimensionOf0(X1) = sz00
| ~ aVector0(X2)
| szszuzczcdt0(aDimensionOf0(X2)) != aDimensionOf0(X1)
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_110,plain,
( sdtasdt0(smndt0(X1),X2) = smndt0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_111,plain,
( sdtasdt0(X1,smndt0(X2)) = smndt0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_112,plain,
( X1 = X2
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_113,plain,
( aScalar0(sdtasasdt0(X1,X2))
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_114,plain,
( sdtlbdtrb0(X2,X1) = sdtlbdtrb0(X3,X1)
| aDimensionOf0(X3) = sz00
| ~ aNaturalNumber0(X1)
| X2 != sziznziztdt0(X3)
| ~ aVector0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_115,plain,
( sdtasdt0(smndt0(X1),smndt0(X2)) = sdtasdt0(X1,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_116,hypothesis,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(split_conjunct,[status(thm)],[m__1967]),
[final] ).
cnf(i_0_117,hypothesis,
sdtlseqdt0(sdtpldt0(xR,xS),sdtpldt0(xP,xP)),
inference(split_conjunct,[status(thm)],[m__2610]),
[final] ).
cnf(i_0_118,plain,
( aDimensionOf0(X2) = sz00
| aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X2))
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_119,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_120,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_121,plain,
( sdtasasdt0(X1,X2) = sz0z00
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2)
| aDimensionOf0(X2) != sz00 ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_122,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_123,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_124,plain,
( aScalar0(sdtlbdtrb0(X1,X2))
| ~ aVector0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_125,plain,
( aScalar0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_126,plain,
( aScalar0(sdtpldt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_127,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_128,plain,
( szszuzczcdt0(aDimensionOf0(X1)) = aDimensionOf0(X2)
| aDimensionOf0(X2) = sz00
| X1 != sziznziztdt0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_129,hypothesis,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(split_conjunct,[status(thm)],[m__2004]),
[final] ).
cnf(i_0_130,hypothesis,
sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)),
inference(split_conjunct,[status(thm)],[m__2628]),
[final] ).
cnf(i_0_131,hypothesis,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(split_conjunct,[status(thm)],[m__2628]),
[final] ).
cnf(i_0_132,plain,
( X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| szszuzczcdt0(X1) != szszuzczcdt0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_133,plain,
( iLess0(X1,szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_134,plain,
( sdtpldt0(smndt0(X1),X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_135,plain,
( sdtpldt0(X1,smndt0(X1)) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_136,plain,
( aVector0(X1)
| aDimensionOf0(X2) = sz00
| X1 != sziznziztdt0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_137,hypothesis,
sdtpldt0(xR,xS) = sdtpldt0(xP,xP),
inference(split_conjunct,[status(thm)],[m__2679]),
[final] ).
cnf(i_0_138,plain,
( sdtlseqdt0(X1,X1)
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_139,plain,
( sdtpldt0(sz0z00,X1) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_140,plain,
( sdtpldt0(X1,sz0z00) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_141,plain,
( X1 = szszuzczcdt0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_142,plain,
( sdtasdt0(sz0z00,X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_143,plain,
( sdtasdt0(X1,sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_144,plain,
( aNaturalNumber0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_145,plain,
( smndt0(smndt0(X1)) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_146,plain,
( aScalar0(smndt0(X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_147,plain,
( aNaturalNumber0(aDimensionOf0(X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_148,plain,
( aNaturalNumber0(szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_149,hypothesis,
xB = sdtlbdtrb0(xt,aDimensionOf0(xt)),
inference(split_conjunct,[status(thm)],[m__1766]),
[final] ).
cnf(i_0_150,hypothesis,
xA = sdtlbdtrb0(xs,aDimensionOf0(xs)),
inference(split_conjunct,[status(thm)],[m__1746]),
[final] ).
cnf(i_0_151,plain,
( szszuzczcdt0(X1) != sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_152,hypothesis,
xN = sdtasdt0(xR,xS),
inference(split_conjunct,[status(thm)],[m__1949]),
[final] ).
cnf(i_0_153,hypothesis,
xS = sdtasdt0(xF,xD),
inference(split_conjunct,[status(thm)],[m__1930]),
[final] ).
cnf(i_0_154,hypothesis,
xP = sdtasdt0(xE,xH),
inference(split_conjunct,[status(thm)],[m__1911]),
[final] ).
cnf(i_0_155,hypothesis,
xR = sdtasdt0(xC,xG),
inference(split_conjunct,[status(thm)],[m__1892]),
[final] ).
cnf(i_0_156,hypothesis,
xH = sdtasdt0(xA,xB),
inference(split_conjunct,[status(thm)],[m__1873]),
[final] ).
cnf(i_0_157,hypothesis,
xG = sdtasdt0(xB,xB),
inference(split_conjunct,[status(thm)],[m__1854]),
[final] ).
cnf(i_0_158,hypothesis,
xF = sdtasdt0(xA,xA),
inference(split_conjunct,[status(thm)],[m__1837]),
[final] ).
cnf(i_0_159,hypothesis,
xE = sdtasasdt0(xp,xq),
inference(split_conjunct,[status(thm)],[m__1820]),
[final] ).
cnf(i_0_160,hypothesis,
xD = sdtasasdt0(xq,xq),
inference(split_conjunct,[status(thm)],[m__1800]),
[final] ).
cnf(i_0_161,hypothesis,
xC = sdtasasdt0(xp,xp),
inference(split_conjunct,[status(thm)],[m__1783]),
[final] ).
cnf(i_0_162,plain,
( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_163,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[m__1678_01]),
[final] ).
cnf(i_0_164,hypothesis,
aDimensionOf0(xs) != sz00,
inference(split_conjunct,[status(thm)],[m__1692]),
[final] ).
cnf(i_0_165,hypothesis,
aVector0(xq),
inference(split_conjunct,[status(thm)],[m__1726]),
[final] ).
cnf(i_0_166,hypothesis,
aVector0(xp),
inference(split_conjunct,[status(thm)],[m__1709]),
[final] ).
cnf(i_0_167,hypothesis,
aVector0(xt),
inference(split_conjunct,[status(thm)],[m__1678]),
[final] ).
cnf(i_0_168,hypothesis,
aVector0(xs),
inference(split_conjunct,[status(thm)],[m__1678]),
[final] ).
cnf(i_0_169,hypothesis,
aScalar0(xN),
inference(split_conjunct,[status(thm)],[m__1949]),
[final] ).
cnf(i_0_170,hypothesis,
aScalar0(xS),
inference(split_conjunct,[status(thm)],[m__1930]),
[final] ).
cnf(i_0_171,hypothesis,
aScalar0(xP),
inference(split_conjunct,[status(thm)],[m__1911]),
[final] ).
cnf(i_0_172,hypothesis,
aScalar0(xR),
inference(split_conjunct,[status(thm)],[m__1892]),
[final] ).
cnf(i_0_173,hypothesis,
aScalar0(xH),
inference(split_conjunct,[status(thm)],[m__1873]),
[final] ).
cnf(i_0_174,hypothesis,
aScalar0(xG),
inference(split_conjunct,[status(thm)],[m__1854]),
[final] ).
cnf(i_0_175,hypothesis,
aScalar0(xF),
inference(split_conjunct,[status(thm)],[m__1837]),
[final] ).
cnf(i_0_176,hypothesis,
aScalar0(xE),
inference(split_conjunct,[status(thm)],[m__1820]),
[final] ).
cnf(i_0_177,hypothesis,
aScalar0(xD),
inference(split_conjunct,[status(thm)],[m__1800]),
[final] ).
cnf(i_0_178,hypothesis,
aScalar0(xC),
inference(split_conjunct,[status(thm)],[m__1783]),
[final] ).
cnf(i_0_179,hypothesis,
aScalar0(xB),
inference(split_conjunct,[status(thm)],[m__1766]),
[final] ).
cnf(i_0_180,hypothesis,
aScalar0(xA),
inference(split_conjunct,[status(thm)],[m__1746]),
[final] ).
cnf(i_0_181,plain,
aScalar0(sz0z00),
inference(split_conjunct,[status(thm)],[mSZeroSc]),
[final] ).
cnf(i_0_182,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[mZeroNat]),
[final] ).
cnf(i_0_183,hypothesis,
xq = sziznziztdt0(xt),
inference(split_conjunct,[status(thm)],[m__1726]),
[final] ).
cnf(i_0_184,hypothesis,
xp = sziznziztdt0(xs),
inference(split_conjunct,[status(thm)],[m__1709]),
[final] ).
cnf(i_0_185,axiom,
X1 = X1 ).
cnf(i_0_186,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_187,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_188,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_185_001,axiom,
X1 = X1 ).
cnf(i_0_186_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_187_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_188_004,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_189_005,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_190_006,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_191_007,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_192_008,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_193_009,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_194_010,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_195_011,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_196_012,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_197_013,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_198_014,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_199_015,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_200_016,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_201_017,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_202_018,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_203_019,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_204_020,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_205_021,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_206_022,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_207,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X1,X1)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X1,X1))) ),
inference(equality_inference,[],[92]) ).
cnf(i_0_208,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aDimensionOf0(X1) = sz00
| sdtasasdt0(X1,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X1,aDimensionOf0(X1)))) ),
inference(equality_inference,[],[93]) ).
cnf(i_0_209,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X1)
| X1 = X1
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X1) ),
inference(equality_inference,[],[102]) ).
cnf(i_0_210,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aScalar0(sdtasasdt0(X1,X1)) ),
inference(equality_inference,[],[113]) ).
cnf(i_0_211,plain,
( ~ aNaturalNumber0(X1)
| ~ aVector0(X2)
| sdtlbdtrb0(sziznziztdt0(X2),X1) = sdtlbdtrb0(X2,X1)
| aDimensionOf0(X2) = sz00 ),
inference(equality_inference,[],[114]) ).
cnf(i_0_212,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aDimensionOf0(X1) = sz00
| aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X1)) ),
inference(equality_inference,[],[118]) ).
cnf(i_0_213,plain,
( ~ aVector0(X1)
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(X1))) = aDimensionOf0(X1)
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[128]) ).
cnf(i_0_214,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| X1 = X1 ),
inference(equality_inference,[],[132]) ).
cnf(i_0_215,plain,
( ~ aVector0(X1)
| aVector0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[136]) ).
cnf(i_0_216,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
inference(scs_inference,[],[i_0_169,i_0_119]) ).
cnf(i_0_217,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtpldt0(X1,X2) = sdtpldt0(X2,X1) ),
inference(scs_inference,[],[i_0_169,i_0_120]) ).
cnf(i_0_218,plain,
smndt0(sz0z00) = sz0z00,
inference(scs_inference,[],[i_0_169,i_0_162]) ).
cnf(i_0_219,plain,
sdtlseqdt0(xN,xN),
inference(scs_inference,[],[i_0_169,i_0_138]) ).
cnf(i_0_220,plain,
( ~ aScalar0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_138]) ).
cnf(i_0_221,plain,
sdtpldt0(xP,xP) = sdtpldt0(xR,xS),
inference(scs_inference,[],[i_0_137,i_0_169,i_0_138,i_0_186]) ).
cnf(i_0_222,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(scs_inference,[],[i_0_137,i_0_168,i_0_169,i_0_164,i_0_138,i_0_186,i_0_213]) ).
cnf(i_0_223,plain,
( aDimensionOf0(X1) = sz00
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(X1))) = aDimensionOf0(X1)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_213]) ).
cnf(i_0_224,plain,
aVector0(sziznziztdt0(xs)),
inference(scs_inference,[],[i_0_137,i_0_168,i_0_169,i_0_164,i_0_138,i_0_186,i_0_213,i_0_215]) ).
cnf(i_0_225,plain,
( aDimensionOf0(X1) = sz00
| aVector0(sziznziztdt0(X1))
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_215]) ).
cnf(i_0_226,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xt),
inference(scs_inference,[],[i_0_137,i_0_168,i_0_169,i_0_163,i_0_164,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187]) ).
cnf(i_0_227,plain,
aScalar0(sdtasdt0(xR,xS)),
inference(scs_inference,[],[i_0_137,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200]) ).
cnf(i_0_228,plain,
~ sdtlseqdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201]) ).
cnf(i_0_229,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202]) ).
cnf(i_0_230,plain,
aVector0(sziznziztdt0(xt)),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_183,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203]) ).
cnf(i_0_231,plain,
~ aScalar0(sdtpldt0(xR,xS)),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_183,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127]) ).
cnf(i_0_232,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_127]) ).
cnf(i_0_233,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_163,i_0_152,i_0_164,i_0_183,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127,i_0_208]) ).
cnf(i_0_234,plain,
( aDimensionOf0(X1) = sz00
| sdtasasdt0(X1,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| ~ aVector0(X1)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_208]) ).
cnf(i_0_235,plain,
sdtlbdtrb0(sziznziztdt0(xs),sz00) = sdtlbdtrb0(xs,sz00),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_182,i_0_163,i_0_152,i_0_164,i_0_183,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127,i_0_208,i_0_211]) ).
cnf(i_0_236,plain,
( aDimensionOf0(X1) = sz00
| sdtlbdtrb0(sziznziztdt0(X1),X2) = sdtlbdtrb0(X1,X2)
| ~ aNaturalNumber0(X2)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_211]) ).
cnf(i_0_237,plain,
sdtlbdtrb0(xp,sz00) = sdtlbdtrb0(xs,sz00),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_182,i_0_163,i_0_152,i_0_164,i_0_183,i_0_184,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127,i_0_208,i_0_211,i_0_114]) ).
cnf(i_0_238,plain,
( aDimensionOf0(X1) = sz00
| X2 != sziznziztdt0(X1)
| sdtlbdtrb0(X2,X3) = sdtlbdtrb0(X1,X3)
| ~ aNaturalNumber0(X3)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_114]) ).
cnf(i_0_239,plain,
~ sdtlseqdt0(xP,xP),
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_171,i_0_182,i_0_163,i_0_152,i_0_164,i_0_183,i_0_184,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127,i_0_208,i_0_211,i_0_114,i_0_99]) ).
cnf(i_0_240,plain,
( sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X4))
| ~ aScalar0(X1)
| ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X4)
| ~ sdtlseqdt0(X1,X3)
| ~ sdtlseqdt0(X2,X4) ),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_241,plain,
$false,
inference(scs_inference,[],[i_0_137,i_0_107,i_0_165,i_0_168,i_0_169,i_0_170,i_0_171,i_0_172,i_0_182,i_0_163,i_0_152,i_0_164,i_0_183,i_0_184,i_0_138,i_0_186,i_0_213,i_0_215,i_0_187,i_0_200,i_0_201,i_0_202,i_0_203,i_0_127,i_0_208,i_0_211,i_0_114,i_0_99,i_0_126]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : RNG074+1 : 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.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 01:48:54 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.31/5.62 % Version : CSE_E---1.7
% 0.31/5.62 % Problem : theBenchmark.p
% 0.31/5.62 % SZS status Theorem for theBenchmark.p
% 0.31/5.62 % SZS output start CNFRefutation
% See solution above
% 0.40/5.77 % Total time : 5.282s
%------------------------------------------------------------------------------