%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG050+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.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:07 PM UTC 2026
% Result : Theorem 0.29s 1.62s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 67)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( ( aDimensionOf0(xs) != sz00
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
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/sandbox/benchmark/theBenchmark.p',mDistr2) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',mPosMon) ).
fof(m__1516,hypothesis,
! [X1] :
( aVector0(X1)
=> ( iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
=> sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1516) ).
fof(mLETrn,axiom,
! [X1,X2,X3] :
( ( aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(X1,X3) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mMNeg) ).
fof(mLEASm,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEASm) ).
fof(mScPr,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( aDimensionOf0(X1) = aDimensionOf0(X2)
=> aScalar0(sdtasasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScPr) ).
fof(mMDNeg,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> sdtasdt0(smndt0(X1),smndt0(X2)) = sdtasdt0(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',mDefSPZ) ).
fof(mSqPos,axiom,
! [X1] :
( aScalar0(X1)
=> sdtlseqdt0(sz0z00,sdtasdt0(X1,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSqPos) ).
fof(mElmSc,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aNaturalNumber0(X2) )
=> aScalar0(sdtlbdtrb0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mElmSc) ).
fof(mMulSc,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> aScalar0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulSc) ).
fof(mSumSc,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> aScalar0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSumSc) ).
fof(mLETot,axiom,
! [X1,X2] :
( ( aScalar0(X1)
& aScalar0(X2) )
=> ( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETot) ).
fof(mSuccEqu,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( szszuzczcdt0(X1) = szszuzczcdt0(X2)
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSuccEqu) ).
fof(mIH,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> iLess0(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mScZero) ).
fof(mLERef,axiom,
! [X1] :
( aScalar0(X1)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLERef) ).
fof(mNatExtr,axiom,
! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00 )
=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = szszuzczcdt0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNatExtr) ).
fof(mNegSc,axiom,
! [X1] :
( aScalar0(X1)
=> aScalar0(smndt0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNegSc) ).
fof(mDimNat,axiom,
! [X1] :
( aVector0(X1)
=> aNaturalNumber0(aDimensionOf0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDimNat) ).
fof(mSuccNat,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( aNaturalNumber0(szszuzczcdt0(X1))
& szszuzczcdt0(X1) != sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSuccNat) ).
fof(m__1542,hypothesis,
aVector0(xs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1542) ).
fof(mSZeroSc,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSZeroSc) ).
fof(mZeroNat,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroNat) ).
fof(i_0_34,negated_conjecture,
~ ( ( aDimensionOf0(xs) != sz00
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(i_0_35,plain,
! [X92,X93,X94,X95] :
( ~ aScalar0(X92)
| ~ aScalar0(X93)
| ~ aScalar0(X94)
| ~ aScalar0(X95)
| sdtasdt0(sdtpldt0(X92,X93),sdtpldt0(X94,X95)) = sdtpldt0(sdtpldt0(sdtasdt0(X92,X94),sdtasdt0(X92,X95)),sdtpldt0(sdtasdt0(X93,X94),sdtasdt0(X93,X95))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr2])]) ).
fof(i_0_36,plain,
! [X135,X136] :
( ~ aVector0(X135)
| ~ aVector0(X136)
| aDimensionOf0(X135) != aDimensionOf0(X136)
| aDimensionOf0(X136) = sz00
| sdtasasdt0(X135,X136) = sdtpldt0(sdtasasdt0(sziznziztdt0(X135),sziznziztdt0(X136)),sdtasdt0(sdtlbdtrb0(X135,aDimensionOf0(X135)),sdtlbdtrb0(X136,aDimensionOf0(X136)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPN])]) ).
fof(i_0_37,plain,
! [X124,X125,X126,X127] :
( ( aVector0(X125)
| X125 != sziznziztdt0(X124)
| aDimensionOf0(X124) = sz00
| ~ aVector0(X124) )
& ( szszuzczcdt0(aDimensionOf0(X125)) = aDimensionOf0(X124)
| X125 != sziznziztdt0(X124)
| aDimensionOf0(X124) = sz00
| ~ aVector0(X124) )
& ( ~ aNaturalNumber0(X126)
| sdtlbdtrb0(X125,X126) = sdtlbdtrb0(X124,X126)
| X125 != sziznziztdt0(X124)
| aDimensionOf0(X124) = sz00
| ~ aVector0(X124) )
& ( aNaturalNumber0(esk2_2(X124,X127))
| ~ aVector0(X127)
| szszuzczcdt0(aDimensionOf0(X127)) != aDimensionOf0(X124)
| X127 = sziznziztdt0(X124)
| aDimensionOf0(X124) = sz00
| ~ aVector0(X124) )
& ( sdtlbdtrb0(X127,esk2_2(X124,X127)) != sdtlbdtrb0(X124,esk2_2(X124,X127))
| ~ aVector0(X127)
| szszuzczcdt0(aDimensionOf0(X127)) != aDimensionOf0(X124)
| X127 = sziznziztdt0(X124)
| aDimensionOf0(X124) = sz00
| ~ aVector0(X124) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefInit])])])])])]) ).
fof(i_0_38,plain,
! [X110,X111,X112,X113] :
( ~ aScalar0(X110)
| ~ aScalar0(X111)
| ~ aScalar0(X112)
| ~ aScalar0(X113)
| ~ sdtlseqdt0(X110,X111)
| ~ sdtlseqdt0(sz0z00,X112)
| ~ sdtlseqdt0(X112,X113)
| sdtlseqdt0(sdtasdt0(X110,X112),sdtasdt0(X111,X113)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMonM])]) ).
fof(i_0_39,plain,
! [X106,X107,X108,X109] :
( ~ aScalar0(X106)
| ~ aScalar0(X107)
| ~ aScalar0(X108)
| ~ aScalar0(X109)
| ~ sdtlseqdt0(X106,X107)
| ~ sdtlseqdt0(X108,X109)
| sdtlseqdt0(sdtpldt0(X106,X108),sdtpldt0(X107,X109)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEMon])]) ).
fof(i_0_40,plain,
! [X89,X90,X91] :
( ( sdtasdt0(X89,sdtpldt0(X90,X91)) = sdtpldt0(sdtasdt0(X89,X90),sdtasdt0(X89,X91))
| ~ aScalar0(X89)
| ~ aScalar0(X90)
| ~ aScalar0(X91) )
& ( sdtasdt0(sdtpldt0(X89,X90),X91) = sdtpldt0(sdtasdt0(X89,X91),sdtasdt0(X90,X91))
| ~ aScalar0(X89)
| ~ aScalar0(X90)
| ~ aScalar0(X91) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDistr])])]) ).
fof(i_0_41,plain,
! [X119,X120] :
( ~ aScalar0(X119)
| ~ aScalar0(X120)
| ~ sdtlseqdt0(sz0z00,X119)
| ~ sdtlseqdt0(sz0z00,X120)
| sdtasdt0(X119,X119) != sdtasdt0(X120,X120)
| X119 = X120 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqrt])]) ).
fof(i_0_42,plain,
! [X86,X87,X88] :
( ( sdtpldt0(sdtpldt0(X86,X87),X88) = sdtpldt0(X86,sdtpldt0(X87,X88))
| ~ aScalar0(X86)
| ~ aScalar0(X87)
| ~ aScalar0(X88) )
& ( sdtpldt0(X86,X87) = sdtpldt0(X87,X86)
| ~ aScalar0(X86)
| ~ aScalar0(X87)
| ~ aScalar0(X88) )
& ( sdtasdt0(sdtasdt0(X86,X87),X88) = sdtasdt0(X86,sdtasdt0(X87,X88))
| ~ aScalar0(X86)
| ~ aScalar0(X87)
| ~ aScalar0(X88) )
& ( sdtasdt0(X86,X87) = sdtasdt0(X87,X86)
| ~ aScalar0(X86)
| ~ aScalar0(X87)
| ~ aScalar0(X88) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mArith])])]) ).
fof(i_0_43,plain,
! [X116,X117] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X116,X117))
| ~ sdtlseqdt0(sz0z00,X116)
| ~ sdtlseqdt0(sz0z00,X117)
| ~ aScalar0(X116)
| ~ aScalar0(X117) )
& ( sdtlseqdt0(sz0z00,sdtasdt0(X116,X117))
| ~ sdtlseqdt0(sz0z00,X116)
| ~ sdtlseqdt0(sz0z00,X117)
| ~ aScalar0(X116)
| ~ aScalar0(X117) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mPosMon])])]) ).
fof(i_0_44,hypothesis,
! [X137] :
( ~ aVector0(X137)
| ~ iLess0(aDimensionOf0(X137),aDimensionOf0(xs))
| sdtlseqdt0(sz0z00,sdtasasdt0(X137,X137)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1516])]) ).
fof(i_0_45,plain,
! [X103,X104,X105] :
( ~ aScalar0(X103)
| ~ aScalar0(X104)
| ~ aScalar0(X105)
| ~ sdtlseqdt0(X103,X104)
| ~ sdtlseqdt0(X104,X105)
| sdtlseqdt0(X103,X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETrn])]) ).
fof(i_0_46,plain,
! [X96,X97] :
( ( sdtasdt0(X96,smndt0(X97)) = smndt0(sdtasdt0(X96,X97))
| ~ aScalar0(X96)
| ~ aScalar0(X97) )
& ( sdtasdt0(smndt0(X96),X97) = smndt0(sdtasdt0(X96,X97))
| ~ aScalar0(X96)
| ~ aScalar0(X97) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMNeg])])]) ).
fof(i_0_47,plain,
! [X101,X102] :
( ~ aScalar0(X101)
| ~ aScalar0(X102)
| ~ sdtlseqdt0(X101,X102)
| ~ sdtlseqdt0(X102,X101)
| X101 = X102 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEASm])]) ).
fof(i_0_48,plain,
! [X131,X132] :
( ~ aVector0(X131)
| ~ aVector0(X132)
| aDimensionOf0(X131) != aDimensionOf0(X132)
| aScalar0(sdtasasdt0(X131,X132)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScPr])]) ).
fof(i_0_49,plain,
! [X98,X99] :
( ~ aScalar0(X98)
| ~ aScalar0(X99)
| sdtasdt0(smndt0(X98),smndt0(X99)) = sdtasdt0(X98,X99) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMDNeg])]) ).
fof(i_0_50,plain,
! [X129,X130] :
( ~ aVector0(X129)
| ~ aVector0(X130)
| aDimensionOf0(X129) != aDimensionOf0(X130)
| aDimensionOf0(X130) = sz00
| aDimensionOf0(sziznziztdt0(X129)) = aDimensionOf0(sziznziztdt0(X130)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEqInit])]) ).
fof(i_0_51,negated_conjecture,
( ( aDimensionOf0(xs) = sz00
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )
& ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(fof_nnf,[status(thm)],[i_0_34]) ).
fof(i_0_52,plain,
! [X133,X134] :
( ~ aVector0(X133)
| ~ aVector0(X134)
| aDimensionOf0(X133) != aDimensionOf0(X134)
| aDimensionOf0(X134) != sz00
| sdtasasdt0(X133,X134) = sz0z00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSPZ])]) ).
fof(i_0_53,plain,
! [X118] :
( ~ aScalar0(X118)
| sdtlseqdt0(sz0z00,sdtasdt0(X118,X118)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSqPos])]) ).
fof(i_0_54,plain,
! [X122,X123] :
( ~ aVector0(X122)
| ~ aNaturalNumber0(X123)
| aScalar0(sdtlbdtrb0(X122,X123)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mElmSc])]) ).
fof(i_0_55,plain,
! [X82,X83] :
( ~ aScalar0(X82)
| ~ aScalar0(X83)
| aScalar0(sdtasdt0(X82,X83)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulSc])]) ).
fof(i_0_56,plain,
! [X80,X81] :
( ~ aScalar0(X80)
| ~ aScalar0(X81)
| aScalar0(sdtpldt0(X80,X81)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSumSc])]) ).
fof(i_0_57,plain,
! [X114,X115] :
( ~ aScalar0(X114)
| ~ aScalar0(X115)
| sdtlseqdt0(X114,X115)
| sdtlseqdt0(X115,X114) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETot])]) ).
fof(i_0_58,plain,
! [X77,X78] :
( ~ aNaturalNumber0(X77)
| ~ aNaturalNumber0(X78)
| szszuzczcdt0(X77) != szszuzczcdt0(X78)
| X77 = X78 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccEqu])]) ).
fof(i_0_59,plain,
! [X79] :
( ~ aNaturalNumber0(X79)
| iLess0(X79,szszuzczcdt0(X79)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIH])]) ).
fof(i_0_60,plain,
! [X85] :
( ( sdtpldt0(X85,sz0z00) = X85
| ~ aScalar0(X85) )
& ( sdtpldt0(sz0z00,X85) = X85
| ~ aScalar0(X85) )
& ( sdtasdt0(X85,sz0z00) = sz0z00
| ~ aScalar0(X85) )
& ( sdtasdt0(sz0z00,X85) = sz0z00
| ~ aScalar0(X85) )
& ( sdtpldt0(X85,smndt0(X85)) = sz0z00
| ~ aScalar0(X85) )
& ( sdtpldt0(smndt0(X85),X85) = sz0z00
| ~ aScalar0(X85) )
& ( smndt0(smndt0(X85)) = X85
| ~ aScalar0(X85) )
& ( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X85) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mScZero])])]) ).
fof(i_0_61,plain,
! [X100] :
( ~ aScalar0(X100)
| sdtlseqdt0(X100,X100) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLERef])]) ).
fof(i_0_62,plain,
! [X75] :
( ( aNaturalNumber0(esk1_1(X75))
| ~ aNaturalNumber0(X75)
| X75 = sz00 )
& ( X75 = szszuzczcdt0(esk1_1(X75))
| ~ aNaturalNumber0(X75)
| X75 = sz00 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNatExtr])])])]) ).
fof(i_0_63,plain,
! [X84] :
( ~ aScalar0(X84)
| aScalar0(smndt0(X84)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mNegSc])]) ).
fof(i_0_64,plain,
! [X121] :
( ~ aVector0(X121)
| aNaturalNumber0(aDimensionOf0(X121)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDimNat])]) ).
fof(i_0_65,plain,
! [X74] :
( ( aNaturalNumber0(szszuzczcdt0(X74))
| ~ aNaturalNumber0(X74) )
& ( szszuzczcdt0(X74) != sz00
| ~ aNaturalNumber0(X74) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSuccNat])])]) ).
cnf(i_0_66,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_35]),
[final] ).
cnf(i_0_67,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_36]),
[final] ).
cnf(i_0_68,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_37]),
[final] ).
cnf(i_0_69,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_38]),
[final] ).
cnf(i_0_70,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_39]),
[final] ).
cnf(i_0_71,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_40]),
[final] ).
cnf(i_0_72,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_40]),
[final] ).
cnf(i_0_73,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_41]),
[final] ).
cnf(i_0_74,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_75,plain,
( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_76,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_77,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_78,hypothesis,
( sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1))
| ~ aVector0(X1)
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs)) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_79,plain,
( sdtlseqdt0(X1,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_80,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_37]),
[final] ).
cnf(i_0_81,plain,
( sdtasdt0(smndt0(X1),X2) = smndt0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_82,plain,
( sdtasdt0(X1,smndt0(X2)) = smndt0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_83,plain,
( X1 = X2
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_84,plain,
( aScalar0(sdtasasdt0(X1,X2))
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_85,plain,
( sdtlbdtrb0(X2,X1) = sdtlbdtrb0(X3,X1)
| aDimensionOf0(X3) = sz00
| ~ aNaturalNumber0(X1)
| X2 != sziznziztdt0(X3)
| ~ aVector0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_86,plain,
( sdtasdt0(smndt0(X1),smndt0(X2)) = sdtasdt0(X1,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_87,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_50]),
[final] ).
cnf(i_0_88,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_89,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_90,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_91,plain,
( sdtasasdt0(X1,X2) = sz0z00
| ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2)
| aDimensionOf0(X2) != sz00 ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_92,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_93,plain,
( aScalar0(sdtlbdtrb0(X1,X2))
| ~ aVector0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_94,plain,
( aScalar0(sdtasdt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_95,plain,
( aScalar0(sdtpldt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_96,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_97,negated_conjecture,
( aDimensionOf0(xs) = sz00
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_98,plain,
( szszuzczcdt0(aDimensionOf0(X1)) = aDimensionOf0(X2)
| aDimensionOf0(X2) = sz00
| X1 != sziznziztdt0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_99,plain,
( X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| szszuzczcdt0(X1) != szszuzczcdt0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_100,plain,
( iLess0(X1,szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_101,plain,
( sdtpldt0(smndt0(X1),X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_102,plain,
( sdtpldt0(X1,smndt0(X1)) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_103,plain,
( aVector0(X1)
| aDimensionOf0(X2) = sz00
| X1 != sziznziztdt0(X2)
| ~ aVector0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_104,plain,
( sdtlseqdt0(X1,X1)
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_105,plain,
( sdtpldt0(sz0z00,X1) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_106,plain,
( sdtpldt0(X1,sz0z00) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_107,plain,
( X1 = szszuzczcdt0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_108,plain,
( sdtasdt0(sz0z00,X1) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_109,plain,
( sdtasdt0(X1,sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_110,plain,
( aNaturalNumber0(esk1_1(X1))
| X1 = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_111,plain,
( smndt0(smndt0(X1)) = X1
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_112,plain,
( aScalar0(smndt0(X1))
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_113,plain,
( aNaturalNumber0(aDimensionOf0(X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_114,plain,
( aNaturalNumber0(szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_115,plain,
( szszuzczcdt0(X1) != sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_116,plain,
( smndt0(sz0z00) = sz0z00
| ~ aScalar0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_117,hypothesis,
aVector0(xs),
inference(split_conjunct,[status(thm)],[m__1542]),
[final] ).
cnf(i_0_118,plain,
aScalar0(sz0z00),
inference(split_conjunct,[status(thm)],[mSZeroSc]),
[final] ).
cnf(i_0_119,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[mZeroNat]),
[final] ).
cnf(i_0_120,axiom,
X1 = X1 ).
cnf(i_0_121,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_122,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_123,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_124,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_125,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_126,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_127,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_128,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_129,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_130,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_131,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_132,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_133,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_134,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_135,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_136,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_137,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_138,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_139,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_140,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_141,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_120_001,axiom,
X1 = X1 ).
cnf(i_0_121_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_122_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_123_004,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_124_005,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_125_006,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_126_007,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_127_008,axiom,
( X1 != X2
| aDimensionOf0(X1) = aDimensionOf0(X2) ) ).
cnf(i_0_128_009,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_129_010,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_130_011,axiom,
( X1 != X2
| sziznziztdt0(X1) = sziznziztdt0(X2) ) ).
cnf(i_0_131_012,axiom,
( X1 != X2
| sdtlbdtrb0(X1,X3) = sdtlbdtrb0(X2,X3) ) ).
cnf(i_0_132_013,axiom,
( X1 != X2
| sdtlbdtrb0(X3,X1) = sdtlbdtrb0(X3,X2) ) ).
cnf(i_0_133_014,axiom,
( X1 != X2
| szszuzczcdt0(X1) = szszuzczcdt0(X2) ) ).
cnf(i_0_134_015,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_135_016,axiom,
( X1 != X2
| ~ aScalar0(X1)
| aScalar0(X2) ) ).
cnf(i_0_136_017,axiom,
( X1 != X2
| ~ aVector0(X1)
| aVector0(X2) ) ).
cnf(i_0_137_018,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_138_019,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_139_020,axiom,
( X1 != X2
| ~ iLess0(X1,X3)
| iLess0(X2,X3) ) ).
cnf(i_0_140_021,axiom,
( X1 != X2
| ~ iLess0(X3,X1)
| iLess0(X3,X2) ) ).
cnf(i_0_141_022,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_142,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,[],[67]) ).
cnf(i_0_143,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X1)
| X1 = X1
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X1) ),
inference(equality_inference,[],[73]) ).
cnf(i_0_144,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aScalar0(sdtasasdt0(X1,X1)) ),
inference(equality_inference,[],[84]) ).
cnf(i_0_145,plain,
( ~ aNaturalNumber0(X1)
| ~ aVector0(X2)
| sdtlbdtrb0(sziznziztdt0(X2),X1) = sdtlbdtrb0(X2,X1)
| aDimensionOf0(X2) = sz00 ),
inference(equality_inference,[],[85]) ).
cnf(i_0_146,plain,
( ~ aVector0(X1)
| ~ aVector0(X1)
| aDimensionOf0(X1) = sz00
| aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X1)) ),
inference(equality_inference,[],[87]) ).
cnf(i_0_147,plain,
( ~ aVector0(X1)
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(X1))) = aDimensionOf0(X1)
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[98]) ).
cnf(i_0_148,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| X1 = X1 ),
inference(equality_inference,[],[99]) ).
cnf(i_0_149,plain,
( ~ aVector0(X1)
| aVector0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00 ),
inference(equality_inference,[],[103]) ).
cnf(i_0_150,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
inference(scs_inference,[],[i_0_118,i_0_89]) ).
cnf(i_0_151,plain,
( ~ aScalar0(X1)
| ~ aScalar0(X2)
| sdtpldt0(X1,X2) = sdtpldt0(X2,X1) ),
inference(scs_inference,[],[i_0_118,i_0_90]) ).
cnf(i_0_152,plain,
aDimensionOf0(xs) = sz00,
inference(scs_inference,[],[i_0_88,i_0_97]) ).
cnf(i_0_153,plain,
smndt0(sz0z00) = sz0z00,
inference(scs_inference,[],[i_0_118,i_0_116]) ).
cnf(i_0_154,plain,
sdtlseqdt0(sz0z00,sz0z00),
inference(scs_inference,[],[i_0_118,i_0_104]) ).
cnf(i_0_155,plain,
( ~ aScalar0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_156,plain,
~ iLess0(aDimensionOf0(xs),aDimensionOf0(xs)),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78]) ).
cnf(i_0_157,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(X1,X1))
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_158,plain,
sz0z00 != sdtasasdt0(xs,xs),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138]) ).
cnf(i_0_159,plain,
sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(sz0z00,sz0z00)),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69]) ).
cnf(i_0_160,plain,
( ~ sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X3,X4))
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X1)
| ~ aScalar0(X4)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(X1,X4) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_161,plain,
( aScalar0(X1)
| sz0z00 != X1 ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135]) ).
cnf(i_0_162,plain,
( aVector0(X1)
| xs != X1 ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135,i_0_136]) ).
cnf(i_0_163,plain,
( X1 != sz0z00
| ~ sdtlseqdt0(X1,sdtasasdt0(xs,xs)) ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135,i_0_136,i_0_137]) ).
cnf(i_0_164,plain,
( X1 != aDimensionOf0(xs)
| ~ iLess0(X1,aDimensionOf0(xs)) ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135,i_0_136,i_0_137,i_0_139]) ).
cnf(i_0_165,plain,
( X1 != aDimensionOf0(xs)
| ~ iLess0(aDimensionOf0(xs),X1) ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135,i_0_136,i_0_137,i_0_139,i_0_140]) ).
cnf(i_0_166,plain,
( aNaturalNumber0(X1)
| sz00 != X1 ),
inference(scs_inference,[],[i_0_88,i_0_117,i_0_118,i_0_119,i_0_104,i_0_78,i_0_138,i_0_69,i_0_135,i_0_136,i_0_137,i_0_139,i_0_140,i_0_141]) ).
cnf(i_0_167,plain,
aScalar0(sz0z00),
inference(equality_inference,[],[161]) ).
cnf(i_0_168,plain,
aVector0(xs),
inference(equality_inference,[],[162]) ).
cnf(i_0_169,plain,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(equality_inference,[],[163]) ).
cnf(i_0_170,plain,
~ iLess0(aDimensionOf0(xs),aDimensionOf0(xs)),
inference(equality_inference,[],[164]) ).
cnf(i_0_171,plain,
~ iLess0(aDimensionOf0(xs),aDimensionOf0(xs)),
inference(equality_inference,[],[165]) ).
cnf(i_0_172,plain,
aNaturalNumber0(sz00),
inference(equality_inference,[],[166]) ).
cnf(i_0_173,plain,
~ sdtlseqdt0(smndt0(sz0z00),sdtasasdt0(xs,xs)),
inference(scs_inference,[],[i_0_153,i_0_163]) ).
cnf(i_0_174,plain,
sz00 = aDimensionOf0(xs),
inference(scs_inference,[],[i_0_152,i_0_153,i_0_163,i_0_121]) ).
cnf(i_0_175,plain,
~ iLess0(sz00,aDimensionOf0(xs)),
inference(scs_inference,[],[i_0_152,i_0_156,i_0_153,i_0_163,i_0_121,i_0_139]) ).
cnf(i_0_176,plain,
~ iLess0(aDimensionOf0(xs),sz00),
inference(scs_inference,[],[i_0_152,i_0_156,i_0_153,i_0_163,i_0_121,i_0_139,i_0_140]) ).
cnf(i_0_177,plain,
aNaturalNumber0(aDimensionOf0(xs)),
inference(scs_inference,[],[i_0_152,i_0_156,i_0_153,i_0_119,i_0_163,i_0_121,i_0_139,i_0_140,i_0_141]) ).
cnf(i_0_178,plain,
( X1 = sz0z00
| X1 != smndt0(sz0z00) ),
inference(scs_inference,[],[i_0_152,i_0_156,i_0_153,i_0_119,i_0_163,i_0_121,i_0_139,i_0_140,i_0_141,i_0_122]) ).
cnf(i_0_179,plain,
( aVector0(sz0z00)
| xs != smndt0(sz0z00) ),
inference(scs_inference,[],[i_0_152,i_0_156,i_0_153,i_0_119,i_0_117,i_0_163,i_0_121,i_0_139,i_0_140,i_0_141,i_0_122,i_0_136]) ).
cnf(i_0_180,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_182,plain,
smndt0(sz0z00) = sz0z00,
inference(equality_inference,[],[178]) ).
cnf(i_0_183,plain,
sz0z00 = smndt0(sz0z00),
inference(scs_inference,[],[i_0_153,i_0_121]) ).
cnf(i_0_184,plain,
~ iLess0(sz00,sz00),
inference(scs_inference,[],[i_0_174,i_0_176,i_0_153,i_0_121,i_0_139]) ).
cnf(i_0_185,plain,
aScalar0(smndt0(sz0z00)),
inference(scs_inference,[],[i_0_174,i_0_176,i_0_118,i_0_153,i_0_121,i_0_139,i_0_135]) ).
cnf(i_0_186,plain,
sdtlseqdt0(smndt0(sz0z00),smndt0(sz0z00)),
inference(scs_inference,[],[i_0_174,i_0_176,i_0_118,i_0_153,i_0_121,i_0_139,i_0_135,i_0_104]) ).
cnf(i_0_187,plain,
( ~ aScalar0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_188,plain,
smndt0(sz0z00) != sdtasasdt0(xs,xs),
inference(scs_inference,[],[i_0_173,i_0_174,i_0_176,i_0_118,i_0_153,i_0_121,i_0_139,i_0_135,i_0_104,i_0_138]) ).
cnf(i_0_189,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00) ),
inference(scs_inference,[],[i_0_88,i_0_173,i_0_174,i_0_176,i_0_118,i_0_153,i_0_121,i_0_139,i_0_135,i_0_104,i_0_138,i_0_96]) ).
cnf(i_0_190,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_191,plain,
sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00),
inference(scs_inference,[],[i_0_88,i_0_173,i_0_174,i_0_176,i_0_118,i_0_153,i_0_117,i_0_121,i_0_139,i_0_135,i_0_104,i_0_138,i_0_96,i_0_144,i_0_136,i_0_84]) ).
cnf(i_0_192,plain,
( aScalar0(sdtasasdt0(X1,X2))
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ aVector0(X1)
| ~ aVector0(X2) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_194,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sdtasasdt0(xs,xs),smndt0(sz0z00)) ),
inference(scs_inference,[],[i_0_173,i_0_185,i_0_96]) ).
cnf(i_0_195,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_196,plain,
sdtlseqdt0(sdtasasdt0(xs,xs),smndt0(sz0z00)),
inference(scs_inference,[],[i_0_173,i_0_185,i_0_117,i_0_96,i_0_144,i_0_136,i_0_84]) ).
cnf(i_0_197,plain,
( aScalar0(sdtasasdt0(X1,X2))
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ aVector0(X1)
| ~ aVector0(X2) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_199,plain,
sdtasasdt0(xs,xs) = sz0z00,
inference(scs_inference,[],[i_0_152,i_0_117,i_0_91]) ).
cnf(i_0_200,plain,
( aDimensionOf0(X1) != sz00
| sdtasasdt0(X2,X1) = sz0z00
| aDimensionOf0(X2) != aDimensionOf0(X1)
| ~ aVector0(X2)
| ~ aVector0(X1) ),
inference(rename_variables,[],[i_0_91]) ).
cnf(i_0_201,plain,
~ sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),
inference(scs_inference,[],[i_0_152,i_0_117,i_0_91,i_0_163]) ).
cnf(i_0_202,plain,
( sdtlseqdt0(X1,X2)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_203,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(sz0z00))
| xs != sdtasasdt0(xs,xs)
| sdtlseqdt0(sdtasdt0(smndt0(sz0z00),sz0z00),sdtasdt0(smndt0(sz0z00),smndt0(sz0z00))) ),
inference(scs_inference,[],[i_0_88,i_0_152,i_0_185,i_0_158,i_0_118,i_0_154,i_0_117,i_0_186,i_0_91,i_0_163,i_0_121,i_0_122,i_0_136,i_0_79,i_0_69]) ).
cnf(i_0_204,plain,
$false,
inference(scs_inference,[],[i_0_199,i_0_158,i_0_121]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : RNG050+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n028.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:49:01 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.29/1.62 % Version : CSE_E---1.7
% 0.29/1.62 % Problem : theBenchmark.p
% 0.29/1.62 % SZS status Theorem for theBenchmark.p
% 0.29/1.62 % SZS output start CNFRefutation
% See solution above
% 0.40/1.76 % Total time : 1.272s
%------------------------------------------------------------------------------