%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG074+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 : n018.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.32s 5.62s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 94)
% 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(m__1726,hypothesis,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(xq,X1) = sdtlbdtrb0(xt,X1) )
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1726) ).
fof(m__1709,hypothesis,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(xp,X1) = sdtlbdtrb0(xs,X1) )
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1709) ).
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__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,
! [X96,X97,X98,X99] :
( ~ aScalar0(X96)
| ~ aScalar0(X97)
| ~ aScalar0(X98)
| ~ aScalar0(X99)
| sdtasdt0(sdtpldt0(X96,X97),sdtpldt0(X98,X99)) = sdtpldt0(sdtpldt0(sdtasdt0(X96,X98),sdtasdt0(X96,X99)),sdtpldt0(sdtasdt0(X97,X98),sdtasdt0(X97,X99))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr2])]) ).
fof(i_0_60,hypothesis,
! [X142,X143] :
( ~ aVector0(X142)
| ~ aVector0(X143)
| aDimensionOf0(X142) != aDimensionOf0(X143)
| ~ iLess0(aDimensionOf0(X142),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X142,X143),sdtasasdt0(X142,X143)),sdtasdt0(sdtasasdt0(X142,X142),sdtasasdt0(X143,X143))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1652])]) ).
fof(i_0_61,plain,
! [X139,X140] :
( ~ aVector0(X139)
| ~ aVector0(X140)
| aDimensionOf0(X139) != aDimensionOf0(X140)
| aDimensionOf0(X140) = sz00
| sdtasasdt0(X139,X140) = sdtpldt0(sdtasasdt0(sziznziztdt0(X139),sziznziztdt0(X140)),sdtasdt0(sdtlbdtrb0(X139,aDimensionOf0(X139)),sdtlbdtrb0(X140,aDimensionOf0(X140)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPN])]) ).
fof(i_0_62,plain,
! [X128,X129,X130,X131] :
( ( aVector0(X129)
| X129 != sziznziztdt0(X128)
| aDimensionOf0(X128) = sz00
| ~ aVector0(X128) )
& ( szszuzczcdt0(aDimensionOf0(X129)) = aDimensionOf0(X128)
| X129 != sziznziztdt0(X128)
| aDimensionOf0(X128) = sz00
| ~ aVector0(X128) )
& ( ~ aNaturalNumber0(X130)
| sdtlbdtrb0(X129,X130) = sdtlbdtrb0(X128,X130)
| X129 != sziznziztdt0(X128)
| aDimensionOf0(X128) = sz00
| ~ aVector0(X128) )
& ( aNaturalNumber0(esk2_2(X128,X131))
| ~ aVector0(X131)
| szszuzczcdt0(aDimensionOf0(X131)) != aDimensionOf0(X128)
| X131 = sziznziztdt0(X128)
| aDimensionOf0(X128) = sz00
| ~ aVector0(X128) )
& ( sdtlbdtrb0(X131,esk2_2(X128,X131)) != sdtlbdtrb0(X128,esk2_2(X128,X131))
| ~ aVector0(X131)
| szszuzczcdt0(aDimensionOf0(X131)) != aDimensionOf0(X128)
| X131 = sziznziztdt0(X128)
| aDimensionOf0(X128) = sz00
| ~ aVector0(X128) ) ),
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,
! [X114,X115,X116,X117] :
( ~ aScalar0(X114)
| ~ aScalar0(X115)
| ~ aScalar0(X116)
| ~ aScalar0(X117)
| ~ sdtlseqdt0(X114,X115)
| ~ sdtlseqdt0(sz0z00,X116)
| ~ sdtlseqdt0(X116,X117)
| sdtlseqdt0(sdtasdt0(X114,X116),sdtasdt0(X115,X117)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMonM])]) ).
fof(i_0_64,plain,
! [X110,X111,X112,X113] :
( ~ aScalar0(X110)
| ~ aScalar0(X111)
| ~ aScalar0(X112)
| ~ aScalar0(X113)
| ~ sdtlseqdt0(X110,X111)
| ~ sdtlseqdt0(X112,X113)
| sdtlseqdt0(sdtpldt0(X110,X112),sdtpldt0(X111,X113)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMon])]) ).
fof(i_0_65,plain,
! [X93,X94,X95] :
( ( sdtasdt0(X93,sdtpldt0(X94,X95)) = sdtpldt0(sdtasdt0(X93,X94),sdtasdt0(X93,X95))
| ~ aScalar0(X93)
| ~ aScalar0(X94)
| ~ aScalar0(X95) )
& ( sdtasdt0(sdtpldt0(X93,X94),X95) = sdtpldt0(sdtasdt0(X93,X95),sdtasdt0(X94,X95))
| ~ aScalar0(X93)
| ~ aScalar0(X94)
| ~ aScalar0(X95) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr])])]) ).
fof(i_0_66,plain,
! [X123,X124] :
( ~ aScalar0(X123)
| ~ aScalar0(X124)
| ~ sdtlseqdt0(sz0z00,X123)
| ~ sdtlseqdt0(sz0z00,X124)
| sdtasdt0(X123,X123) != sdtasdt0(X124,X124)
| X123 = X124 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqrt])]) ).
fof(i_0_67,plain,
! [X90,X91,X92] :
( ( sdtpldt0(sdtpldt0(X90,X91),X92) = sdtpldt0(X90,sdtpldt0(X91,X92))
| ~ aScalar0(X90)
| ~ aScalar0(X91)
| ~ aScalar0(X92) )
& ( sdtpldt0(X90,X91) = sdtpldt0(X91,X90)
| ~ aScalar0(X90)
| ~ aScalar0(X91)
| ~ aScalar0(X92) )
& ( sdtasdt0(sdtasdt0(X90,X91),X92) = sdtasdt0(X90,sdtasdt0(X91,X92))
| ~ aScalar0(X90)
| ~ aScalar0(X91)
| ~ aScalar0(X92) )
& ( sdtasdt0(X90,X91) = sdtasdt0(X91,X90)
| ~ aScalar0(X90)
| ~ aScalar0(X91)
| ~ aScalar0(X92) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mArith])])]) ).
fof(i_0_68,plain,
! [X120,X121] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X120,X121))
| ~ sdtlseqdt0(sz0z00,X120)
| ~ sdtlseqdt0(sz0z00,X121)
| ~ aScalar0(X120)
| ~ aScalar0(X121) )
& ( sdtlseqdt0(sz0z00,sdtasdt0(X120,X121))
| ~ sdtlseqdt0(sz0z00,X120)
| ~ sdtlseqdt0(sz0z00,X121)
| ~ aScalar0(X120)
| ~ aScalar0(X121) ) ),
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,
! [X107,X108,X109] :
( ~ aScalar0(X107)
| ~ aScalar0(X108)
| ~ aScalar0(X109)
| ~ sdtlseqdt0(X107,X108)
| ~ sdtlseqdt0(X108,X109)
| sdtlseqdt0(X107,X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETrn])]) ).
fof(i_0_71,plain,
! [X100,X101] :
( ( sdtasdt0(X100,smndt0(X101)) = smndt0(sdtasdt0(X100,X101))
| ~ aScalar0(X100)
| ~ aScalar0(X101) )
& ( sdtasdt0(smndt0(X100),X101) = smndt0(sdtasdt0(X100,X101))
| ~ aScalar0(X100)
| ~ aScalar0(X101) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMNeg])])]) ).
fof(i_0_72,plain,
! [X105,X106] :
( ~ aScalar0(X105)
| ~ aScalar0(X106)
| ~ sdtlseqdt0(X105,X106)
| ~ sdtlseqdt0(X106,X105)
| X105 = X106 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEASm])]) ).
fof(i_0_73,plain,
! [X135,X136] :
( ~ aVector0(X135)
| ~ aVector0(X136)
| aDimensionOf0(X135) != aDimensionOf0(X136)
| aScalar0(sdtasasdt0(X135,X136)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScPr])]) ).
fof(i_0_74,plain,
! [X102,X103] :
( ~ aScalar0(X102)
| ~ aScalar0(X103)
| sdtasdt0(smndt0(X102),smndt0(X103)) = sdtasdt0(X102,X103) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMDNeg])]) ).
fof(i_0_75,plain,
! [X133,X134] :
( ~ aVector0(X133)
| ~ aVector0(X134)
| aDimensionOf0(X133) != aDimensionOf0(X134)
| aDimensionOf0(X134) = sz00
| aDimensionOf0(sziznziztdt0(X133)) = aDimensionOf0(sziznziztdt0(X134)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEqInit])]) ).
fof(i_0_76,plain,
! [X137,X138] :
( ~ aVector0(X137)
| ~ aVector0(X138)
| aDimensionOf0(X137) != aDimensionOf0(X138)
| aDimensionOf0(X138) != sz00
| sdtasasdt0(X137,X138) = sz0z00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPZ])]) ).
fof(i_0_77,plain,
! [X141] :
( ~ aVector0(X141)
| sdtlseqdt0(sz0z00,sdtasasdt0(X141,X141)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScSqPos])]) ).
fof(i_0_78,plain,
! [X122] :
( ~ aScalar0(X122)
| sdtlseqdt0(sz0z00,sdtasdt0(X122,X122)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqPos])]) ).
fof(i_0_79,plain,
! [X126,X127] :
( ~ aVector0(X126)
| ~ aNaturalNumber0(X127)
| aScalar0(sdtlbdtrb0(X126,X127)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mElmSc])]) ).
fof(i_0_80,plain,
! [X86,X87] :
( ~ aScalar0(X86)
| ~ aScalar0(X87)
| aScalar0(sdtasdt0(X86,X87)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulSc])]) ).
fof(i_0_81,plain,
! [X84,X85] :
( ~ aScalar0(X84)
| ~ aScalar0(X85)
| aScalar0(sdtpldt0(X84,X85)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSumSc])]) ).
fof(i_0_82,plain,
! [X118,X119] :
( ~ aScalar0(X118)
| ~ aScalar0(X119)
| sdtlseqdt0(X118,X119)
| sdtlseqdt0(X119,X118) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETot])]) ).
fof(i_0_83,hypothesis,
! [X145] :
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ( ~ aNaturalNumber0(X145)
| sdtlbdtrb0(xq,X145) = sdtlbdtrb0(xt,X145) )
& xq = sziznziztdt0(xt) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1726])])]) ).
fof(i_0_84,hypothesis,
! [X144] :
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ( ~ aNaturalNumber0(X144)
| sdtlbdtrb0(xp,X144) = sdtlbdtrb0(xs,X144) )
& xp = sziznziztdt0(xs) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1709])])]) ).
fof(i_0_85,plain,
! [X81,X82] :
( ~ aNaturalNumber0(X81)
| ~ aNaturalNumber0(X82)
| szszuzczcdt0(X81) != szszuzczcdt0(X82)
| X81 = X82 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccEqu])]) ).
fof(i_0_86,plain,
! [X83] :
( ~ aNaturalNumber0(X83)
| iLess0(X83,szszuzczcdt0(X83)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIH])]) ).
fof(i_0_87,plain,
! [X89] :
( ( sdtpldt0(X89,sz0z00) = X89
| ~ aScalar0(X89) )
& ( sdtpldt0(sz0z00,X89) = X89
| ~ aScalar0(X89) )
& ( sdtasdt0(X89,sz0z00) = sz0z00
| ~ aScalar0(X89) )
& ( sdtasdt0(sz0z00,X89) = sz0z00
| ~ aScalar0(X89) )
& ( sdtpldt0(X89,smndt0(X89)) = sz0z00
| ~ aScalar0(X89) )
& ( sdtpldt0(smndt0(X89),X89) = sz0z00
| ~ aScalar0(X89) )
& ( smndt0(smndt0(X89)) = X89
| ~ aScalar0(X89) )
& ( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X89) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScZero])])]) ).
fof(i_0_88,plain,
! [X104] :
( ~ aScalar0(X104)
| sdtlseqdt0(X104,X104) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLERef])]) ).
fof(i_0_89,plain,
! [X79] :
( ( aNaturalNumber0(esk1_1(X79))
| ~ aNaturalNumber0(X79)
| X79 = sz00 )
& ( X79 = szszuzczcdt0(esk1_1(X79))
| ~ aNaturalNumber0(X79)
| X79 = sz00 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNatExtr])])])]) ).
fof(i_0_90,plain,
! [X88] :
( ~ aScalar0(X88)
| aScalar0(smndt0(X88)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNegSc])]) ).
fof(i_0_91,plain,
! [X125] :
( ~ aVector0(X125)
| aNaturalNumber0(aDimensionOf0(X125)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDimNat])]) ).
fof(i_0_92,plain,
! [X78] :
( ( aNaturalNumber0(szszuzczcdt0(X78))
| ~ aNaturalNumber0(X78) )
& ( szszuzczcdt0(X78) != sz00
| ~ aNaturalNumber0(X78) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccNat])])]) ).
cnf(i_0_93,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_94,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_95,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_96,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_97,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_98,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_99,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_100,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_101,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_102,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_103,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_104,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_105,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_106,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_107,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_108,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_109,hypothesis,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_110,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_111,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_112,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_113,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_114,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_115,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_116,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_117,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_118,hypothesis,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(split_conjunct,[status(thm)],[m__1967]),
[final] ).
cnf(i_0_119,hypothesis,
sdtlseqdt0(sdtpldt0(xR,xS),sdtpldt0(xP,xP)),
inference(split_conjunct,[status(thm)],[m__2610]),
[final] ).
cnf(i_0_120,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_121,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_122,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_123,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_124,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_125,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_126,plain,
( aScalar0(sdtlbdtrb0(X1,X2))
| ~ aVector0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_127,plain,
( aScalar0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_128,plain,
( aScalar0(sdtpldt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_129,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_130,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_131,hypothesis,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(split_conjunct,[status(thm)],[m__2004]),
[final] ).
cnf(i_0_132,hypothesis,
sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)),
inference(split_conjunct,[status(thm)],[m__2628]),
[final] ).
cnf(i_0_133,hypothesis,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(split_conjunct,[status(thm)],[m__2628]),
[final] ).
cnf(i_0_134,hypothesis,
( sdtlbdtrb0(xq,X1) = sdtlbdtrb0(xt,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_135,hypothesis,
( sdtlbdtrb0(xp,X1) = sdtlbdtrb0(xs,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_136,plain,
( X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| szszuzczcdt0(X1) != szszuzczcdt0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_137,plain,
( iLess0(X1,szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_138,plain,
( sdtpldt0(smndt0(X1),X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_139,plain,
( sdtpldt0(X1,smndt0(X1)) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_140,plain,
( aVector0(X1)
| aDimensionOf0(X2) = sz00
| X1 != sziznziztdt0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_141,hypothesis,
sdtpldt0(xR,xS) = sdtpldt0(xP,xP),
inference(split_conjunct,[status(thm)],[m__2679]),
[final] ).
cnf(i_0_142,plain,
( sdtlseqdt0(X1,X1)
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_143,plain,
( sdtpldt0(sz0z00,X1) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_144,plain,
( sdtpldt0(X1,sz0z00) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_145,plain,
( X1 = szszuzczcdt0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_146,plain,
( sdtasdt0(sz0z00,X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_147,plain,
( sdtasdt0(X1,sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_148,plain,
( aNaturalNumber0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_149,plain,
( smndt0(smndt0(X1)) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_150,plain,
( aScalar0(smndt0(X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_151,plain,
( aNaturalNumber0(aDimensionOf0(X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_152,plain,
( aNaturalNumber0(szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_153,hypothesis,
xB = sdtlbdtrb0(xt,aDimensionOf0(xt)),
inference(split_conjunct,[status(thm)],[m__1766]),
[final] ).
cnf(i_0_154,hypothesis,
xA = sdtlbdtrb0(xs,aDimensionOf0(xs)),
inference(split_conjunct,[status(thm)],[m__1746]),
[final] ).
cnf(i_0_155,plain,
( szszuzczcdt0(X1) != sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_156,hypothesis,
xN = sdtasdt0(xR,xS),
inference(split_conjunct,[status(thm)],[m__1949]),
[final] ).
cnf(i_0_157,hypothesis,
xS = sdtasdt0(xF,xD),
inference(split_conjunct,[status(thm)],[m__1930]),
[final] ).
cnf(i_0_158,hypothesis,
xP = sdtasdt0(xE,xH),
inference(split_conjunct,[status(thm)],[m__1911]),
[final] ).
cnf(i_0_159,hypothesis,
xR = sdtasdt0(xC,xG),
inference(split_conjunct,[status(thm)],[m__1892]),
[final] ).
cnf(i_0_160,hypothesis,
xH = sdtasdt0(xA,xB),
inference(split_conjunct,[status(thm)],[m__1873]),
[final] ).
cnf(i_0_161,hypothesis,
xG = sdtasdt0(xB,xB),
inference(split_conjunct,[status(thm)],[m__1854]),
[final] ).
cnf(i_0_162,hypothesis,
xF = sdtasdt0(xA,xA),
inference(split_conjunct,[status(thm)],[m__1837]),
[final] ).
cnf(i_0_163,hypothesis,
xE = sdtasasdt0(xp,xq),
inference(split_conjunct,[status(thm)],[m__1820]),
[final] ).
cnf(i_0_164,hypothesis,
xD = sdtasasdt0(xq,xq),
inference(split_conjunct,[status(thm)],[m__1800]),
[final] ).
cnf(i_0_165,hypothesis,
xC = sdtasasdt0(xp,xp),
inference(split_conjunct,[status(thm)],[m__1783]),
[final] ).
cnf(i_0_166,plain,
( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_167,hypothesis,
szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_168,hypothesis,
szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_169,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[m__1678_01]),
[final] ).
cnf(i_0_170,hypothesis,
aDimensionOf0(xs) != sz00,
inference(split_conjunct,[status(thm)],[m__1692]),
[final] ).
cnf(i_0_171,hypothesis,
aVector0(xq),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_172,hypothesis,
aVector0(xp),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_173,hypothesis,
aVector0(xt),
inference(split_conjunct,[status(thm)],[m__1678]),
[final] ).
cnf(i_0_174,hypothesis,
aVector0(xs),
inference(split_conjunct,[status(thm)],[m__1678]),
[final] ).
cnf(i_0_175,hypothesis,
aScalar0(xN),
inference(split_conjunct,[status(thm)],[m__1949]),
[final] ).
cnf(i_0_176,hypothesis,
aScalar0(xS),
inference(split_conjunct,[status(thm)],[m__1930]),
[final] ).
cnf(i_0_177,hypothesis,
aScalar0(xP),
inference(split_conjunct,[status(thm)],[m__1911]),
[final] ).
cnf(i_0_178,hypothesis,
aScalar0(xR),
inference(split_conjunct,[status(thm)],[m__1892]),
[final] ).
cnf(i_0_179,hypothesis,
aScalar0(xH),
inference(split_conjunct,[status(thm)],[m__1873]),
[final] ).
cnf(i_0_180,hypothesis,
aScalar0(xG),
inference(split_conjunct,[status(thm)],[m__1854]),
[final] ).
cnf(i_0_181,hypothesis,
aScalar0(xF),
inference(split_conjunct,[status(thm)],[m__1837]),
[final] ).
cnf(i_0_182,hypothesis,
aScalar0(xE),
inference(split_conjunct,[status(thm)],[m__1820]),
[final] ).
cnf(i_0_183,hypothesis,
aScalar0(xD),
inference(split_conjunct,[status(thm)],[m__1800]),
[final] ).
cnf(i_0_184,hypothesis,
aScalar0(xC),
inference(split_conjunct,[status(thm)],[m__1783]),
[final] ).
cnf(i_0_185,hypothesis,
aScalar0(xB),
inference(split_conjunct,[status(thm)],[m__1766]),
[final] ).
cnf(i_0_186,hypothesis,
aScalar0(xA),
inference(split_conjunct,[status(thm)],[m__1746]),
[final] ).
cnf(i_0_187,plain,
aScalar0(sz0z00),
inference(split_conjunct,[status(thm)],[mSZeroSc]),
[final] ).
cnf(i_0_188,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[mZeroNat]),
[final] ).
cnf(i_0_189,hypothesis,
xq = sziznziztdt0(xt),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_190,hypothesis,
xp = sziznziztdt0(xs),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_191,axiom,
X1 = X1 ).
cnf(i_0_192,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_193,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_194,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_191_001,axiom,
X1 = X1 ).
cnf(i_0_192_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_193_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_194_004,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_195_005,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_196_006,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_197_007,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_198_008,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_199_009,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_200_010,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_201_011,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_202_012,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_203_013,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_204_014,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_205_015,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_206_016,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_207_017,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_208_018,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_209_019,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_210_020,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_211_021,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_212_022,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_213,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,[],[94]) ).
cnf(i_0_214,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,[],[95]) ).
cnf(i_0_215,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X1)
| X1 = X1
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X1) ),
inference(equality_inference,[],[104]) ).
cnf(i_0_216,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aScalar0(sdtasasdt0(X1,X1)) ),
inference(equality_inference,[],[115]) ).
cnf(i_0_217,plain,
( ~ aNaturalNumber0(X1)
| ~ aVector0(X2)
| sdtlbdtrb0(sziznziztdt0(X2),X1) = sdtlbdtrb0(X2,X1)
| aDimensionOf0(X2) = sz00 ),
inference(equality_inference,[],[116]) ).
cnf(i_0_218,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aDimensionOf0(X1) = sz00
| aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X1)) ),
inference(equality_inference,[],[120]) ).
cnf(i_0_219,plain,
( ~ aVector0(X1)
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(X1))) = aDimensionOf0(X1)
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[130]) ).
cnf(i_0_220,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| X1 = X1 ),
inference(equality_inference,[],[136]) ).
cnf(i_0_221,plain,
( ~ aVector0(X1)
| aVector0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[140]) ).
cnf(i_0_222,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
inference(scs_inference,[],[i_0_175,i_0_121]) ).
cnf(i_0_223,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtpldt0(X1,X2) = sdtpldt0(X2,X1) ),
inference(scs_inference,[],[i_0_175,i_0_122]) ).
cnf(i_0_224,plain,
smndt0(sz0z00) = sz0z00,
inference(scs_inference,[],[i_0_175,i_0_166]) ).
cnf(i_0_225,plain,
sdtlseqdt0(xN,xN),
inference(scs_inference,[],[i_0_175,i_0_142]) ).
cnf(i_0_226,plain,
( ~ aScalar0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_227,plain,
sdtpldt0(xP,xP) = sdtpldt0(xR,xS),
inference(scs_inference,[],[i_0_141,i_0_175,i_0_142,i_0_192]) ).
cnf(i_0_228,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(scs_inference,[],[i_0_141,i_0_174,i_0_175,i_0_170,i_0_142,i_0_192,i_0_219]) ).
cnf(i_0_229,plain,
( aDimensionOf0(X1) = sz00
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(X1))) = aDimensionOf0(X1)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_219]) ).
cnf(i_0_230,plain,
aVector0(sziznziztdt0(xs)),
inference(scs_inference,[],[i_0_141,i_0_174,i_0_175,i_0_170,i_0_142,i_0_192,i_0_219,i_0_221]) ).
cnf(i_0_231,plain,
( aDimensionOf0(X1) = sz00
| aVector0(sziznziztdt0(X1))
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_221]) ).
cnf(i_0_232,plain,
szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xt),
inference(scs_inference,[],[i_0_141,i_0_174,i_0_175,i_0_169,i_0_170,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193]) ).
cnf(i_0_233,plain,
aScalar0(sdtasdt0(xR,xS)),
inference(scs_inference,[],[i_0_141,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206]) ).
cnf(i_0_234,plain,
~ sdtlseqdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207]) ).
cnf(i_0_235,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208]) ).
cnf(i_0_236,plain,
aVector0(sziznziztdt0(xt)),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_189,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209]) ).
cnf(i_0_237,plain,
~ aScalar0(sdtpldt0(xR,xS)),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_189,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129]) ).
cnf(i_0_238,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_239,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_169,i_0_156,i_0_170,i_0_189,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129,i_0_214]) ).
cnf(i_0_240,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_214]) ).
cnf(i_0_241,plain,
sdtlbdtrb0(sziznziztdt0(xs),sz00) = sdtlbdtrb0(xs,sz00),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_188,i_0_169,i_0_156,i_0_170,i_0_189,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129,i_0_214,i_0_217]) ).
cnf(i_0_242,plain,
( aDimensionOf0(X1) = sz00
| sdtlbdtrb0(sziznziztdt0(X1),X2) = sdtlbdtrb0(X1,X2)
| ~ aNaturalNumber0(X2)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_217]) ).
cnf(i_0_243,plain,
sdtlbdtrb0(xp,sz00) = sdtlbdtrb0(xs,sz00),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_188,i_0_169,i_0_156,i_0_170,i_0_189,i_0_190,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129,i_0_214,i_0_217,i_0_116]) ).
cnf(i_0_244,plain,
( aDimensionOf0(X1) = sz00
| X2 != sziznziztdt0(X1)
| sdtlbdtrb0(X2,X3) = sdtlbdtrb0(X1,X3)
| ~ aNaturalNumber0(X3)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_245,plain,
~ sdtlseqdt0(xP,xP),
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_177,i_0_188,i_0_169,i_0_156,i_0_170,i_0_189,i_0_190,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129,i_0_214,i_0_217,i_0_116,i_0_101]) ).
cnf(i_0_246,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_101]) ).
cnf(i_0_247,plain,
$false,
inference(scs_inference,[],[i_0_141,i_0_109,i_0_171,i_0_174,i_0_175,i_0_176,i_0_177,i_0_178,i_0_188,i_0_169,i_0_156,i_0_170,i_0_189,i_0_190,i_0_168,i_0_142,i_0_192,i_0_219,i_0_221,i_0_193,i_0_206,i_0_207,i_0_208,i_0_209,i_0_129,i_0_214,i_0_217,i_0_116,i_0_101,i_0_128]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : RNG074+2 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n018.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 01:58:47 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.32/5.62 % Version : CSE_E---1.7
% 0.32/5.62 % Problem : theBenchmark.p
% 0.32/5.62 % SZS status Theorem for theBenchmark.p
% 0.32/5.62 % SZS output start CNFRefutation
% See solution above
% 0.42/5.77 % Total time : 5.281s
%------------------------------------------------------------------------------