%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM464+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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:57:25 PM UTC 2026
% Result : Theorem 0.28s 1.61s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 68)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( xm != sz00
=> sdtlseqdt0(sz10,xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(mAMDistr,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtasdt0(sdtpldt0(X2,X3),X1) = sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAMDistr) ).
fof(mMonMul,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( X1 != sz00
& X2 != X3
& sdtlseqdt0(X2,X3) )
=> ( sdtasdt0(X1,X2) != sdtasdt0(X1,X3)
& sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtasdt0(X2,X1) != sdtasdt0(X3,X1)
& sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul) ).
fof(mMonAdd,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( X1 != X2
& sdtlseqdt0(X1,X2) )
=> ! [X3] :
( aNaturalNumber0(X3)
=> ( sdtpldt0(X3,X1) != sdtpldt0(X3,X2)
& sdtlseqdt0(sdtpldt0(X3,X1),sdtpldt0(X3,X2))
& sdtpldt0(X1,X3) != sdtpldt0(X2,X3)
& sdtlseqdt0(sdtpldt0(X1,X3),sdtpldt0(X2,X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonAdd) ).
fof(mMulAsso,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulAsso) ).
fof(mAddAsso,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddAsso) ).
fof(mDefDiff,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
=> ! [X3] :
( X3 = sdtmndt0(X2,X1)
<=> ( aNaturalNumber0(X3)
& sdtpldt0(X1,X3) = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
fof(mLETran,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETran) ).
fof(mDefLE,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
<=> ? [X3] :
( aNaturalNumber0(X3)
& sdtpldt0(X1,X3) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefLE) ).
fof(mMulCanc,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( X1 != sz00
=> ! [X2,X3] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( sdtasdt0(X1,X2) = sdtasdt0(X1,X3)
| sdtasdt0(X2,X1) = sdtasdt0(X3,X1) )
=> X2 = X3 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulCanc) ).
fof(mAddCanc,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( sdtpldt0(X1,X2) = sdtpldt0(X1,X3)
| sdtpldt0(X2,X1) = sdtpldt0(X3,X1) )
=> X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddCanc) ).
fof(mLEAsym,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEAsym) ).
fof(mSortsB_02,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> aNaturalNumber0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(mSortsB,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> aNaturalNumber0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
fof(mLETotal,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
| ( X2 != X1
& sdtlseqdt0(X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETotal) ).
fof(mMulComm,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(mAddComm,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> sdtpldt0(X1,X2) = sdtpldt0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddComm) ).
fof(mZeroMul,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtasdt0(X1,X2) = sz00
=> ( X1 = sz00
| X2 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroMul) ).
fof(mZeroAdd,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtpldt0(X1,X2) = sz00
=> ( X1 = sz00
& X2 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroAdd) ).
fof(mLENTr,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( X1 = sz00
| X1 = sz10
| ( sz10 != X1
& sdtlseqdt0(sz10,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLENTr) ).
fof(mLERefl,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERefl) ).
fof(m_MulUnit,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( sdtasdt0(X1,sz10) = X1
& X1 = sdtasdt0(sz10,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulUnit) ).
fof(m_AddZero,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( sdtpldt0(X1,sz00) = X1
& X1 = sdtpldt0(sz00,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_AddZero) ).
fof(m_MulZero,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( sdtasdt0(X1,sz00) = sz00
& sz00 = sdtasdt0(sz00,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
fof(m__987,hypothesis,
( aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__987) ).
fof(mSortsC_01,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
fof(i_0_27,negated_conjecture,
~ ( xm != sz00
=> sdtlseqdt0(sz10,xm) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(i_0_28,plain,
! [X73,X74,X75] :
( ( sdtasdt0(X73,sdtpldt0(X74,X75)) = sdtpldt0(sdtasdt0(X73,X74),sdtasdt0(X73,X75))
| ~ aNaturalNumber0(X73)
| ~ aNaturalNumber0(X74)
| ~ aNaturalNumber0(X75) )
& ( sdtasdt0(sdtpldt0(X74,X75),X73) = sdtpldt0(sdtasdt0(X74,X73),sdtasdt0(X75,X73))
| ~ aNaturalNumber0(X73)
| ~ aNaturalNumber0(X74)
| ~ aNaturalNumber0(X75) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAMDistr])])]) ).
fof(i_0_29,plain,
! [X104,X105,X106] :
( ( sdtasdt0(X104,X105) != sdtasdt0(X104,X106)
| X104 = sz00
| X105 = X106
| ~ sdtlseqdt0(X105,X106)
| ~ aNaturalNumber0(X104)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106) )
& ( sdtlseqdt0(sdtasdt0(X104,X105),sdtasdt0(X104,X106))
| X104 = sz00
| X105 = X106
| ~ sdtlseqdt0(X105,X106)
| ~ aNaturalNumber0(X104)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106) )
& ( sdtasdt0(X105,X104) != sdtasdt0(X106,X104)
| X104 = sz00
| X105 = X106
| ~ sdtlseqdt0(X105,X106)
| ~ aNaturalNumber0(X104)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106) )
& ( sdtlseqdt0(sdtasdt0(X105,X104),sdtasdt0(X106,X104))
| X104 = sz00
| X105 = X106
| ~ sdtlseqdt0(X105,X106)
| ~ aNaturalNumber0(X104)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMonMul])])]) ).
fof(i_0_30,plain,
! [X101,X102,X103] :
( ( sdtpldt0(X103,X101) != sdtpldt0(X103,X102)
| ~ aNaturalNumber0(X103)
| X101 = X102
| ~ sdtlseqdt0(X101,X102)
| ~ aNaturalNumber0(X101)
| ~ aNaturalNumber0(X102) )
& ( sdtlseqdt0(sdtpldt0(X103,X101),sdtpldt0(X103,X102))
| ~ aNaturalNumber0(X103)
| X101 = X102
| ~ sdtlseqdt0(X101,X102)
| ~ aNaturalNumber0(X101)
| ~ aNaturalNumber0(X102) )
& ( sdtpldt0(X101,X103) != sdtpldt0(X102,X103)
| ~ aNaturalNumber0(X103)
| X101 = X102
| ~ sdtlseqdt0(X101,X102)
| ~ aNaturalNumber0(X101)
| ~ aNaturalNumber0(X102) )
& ( sdtlseqdt0(sdtpldt0(X101,X103),sdtpldt0(X102,X103))
| ~ aNaturalNumber0(X103)
| X101 = X102
| ~ sdtlseqdt0(X101,X102)
| ~ aNaturalNumber0(X101)
| ~ aNaturalNumber0(X102) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMonAdd])])])]) ).
fof(i_0_31,plain,
! [X68,X69,X70] :
( ~ aNaturalNumber0(X68)
| ~ aNaturalNumber0(X69)
| ~ aNaturalNumber0(X70)
| sdtasdt0(sdtasdt0(X68,X69),X70) = sdtasdt0(X68,sdtasdt0(X69,X70)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulAsso])]) ).
fof(i_0_32,plain,
! [X62,X63,X64] :
( ~ aNaturalNumber0(X62)
| ~ aNaturalNumber0(X63)
| ~ aNaturalNumber0(X64)
| sdtpldt0(sdtpldt0(X62,X63),X64) = sdtpldt0(X62,sdtpldt0(X63,X64)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddAsso])]) ).
fof(i_0_33,plain,
! [X90,X91,X92] :
( ( aNaturalNumber0(X92)
| X92 != sdtmndt0(X91,X90)
| ~ sdtlseqdt0(X90,X91)
| ~ aNaturalNumber0(X90)
| ~ aNaturalNumber0(X91) )
& ( sdtpldt0(X90,X92) = X91
| X92 != sdtmndt0(X91,X90)
| ~ sdtlseqdt0(X90,X91)
| ~ aNaturalNumber0(X90)
| ~ aNaturalNumber0(X91) )
& ( ~ aNaturalNumber0(X92)
| sdtpldt0(X90,X92) != X91
| X92 = sdtmndt0(X91,X90)
| ~ sdtlseqdt0(X90,X91)
| ~ aNaturalNumber0(X90)
| ~ aNaturalNumber0(X91) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefDiff])])])]) ).
fof(i_0_34,plain,
! [X96,X97,X98] :
( ~ aNaturalNumber0(X96)
| ~ aNaturalNumber0(X97)
| ~ aNaturalNumber0(X98)
| ~ sdtlseqdt0(X96,X97)
| ~ sdtlseqdt0(X97,X98)
| sdtlseqdt0(X96,X98) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETran])]) ).
fof(i_0_35,plain,
! [X86,X87,X89] :
( ( aNaturalNumber0(esk1_2(X86,X87))
| ~ sdtlseqdt0(X86,X87)
| ~ aNaturalNumber0(X86)
| ~ aNaturalNumber0(X87) )
& ( sdtpldt0(X86,esk1_2(X86,X87)) = X87
| ~ sdtlseqdt0(X86,X87)
| ~ aNaturalNumber0(X86)
| ~ aNaturalNumber0(X87) )
& ( ~ aNaturalNumber0(X89)
| sdtpldt0(X86,X89) != X87
| sdtlseqdt0(X86,X87)
| ~ aNaturalNumber0(X86)
| ~ aNaturalNumber0(X87) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefLE])])])])]) ).
fof(i_0_36,plain,
! [X79,X80,X81] :
( ( sdtasdt0(X79,X80) != sdtasdt0(X79,X81)
| X80 = X81
| ~ aNaturalNumber0(X80)
| ~ aNaturalNumber0(X81)
| X79 = sz00
| ~ aNaturalNumber0(X79) )
& ( sdtasdt0(X80,X79) != sdtasdt0(X81,X79)
| X80 = X81
| ~ aNaturalNumber0(X80)
| ~ aNaturalNumber0(X81)
| X79 = sz00
| ~ aNaturalNumber0(X79) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulCanc])])])]) ).
fof(i_0_37,plain,
! [X76,X77,X78] :
( ( sdtpldt0(X76,X77) != sdtpldt0(X76,X78)
| X77 = X78
| ~ aNaturalNumber0(X76)
| ~ aNaturalNumber0(X77)
| ~ aNaturalNumber0(X78) )
& ( sdtpldt0(X77,X76) != sdtpldt0(X78,X76)
| X77 = X78
| ~ aNaturalNumber0(X76)
| ~ aNaturalNumber0(X77)
| ~ aNaturalNumber0(X78) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddCanc])])]) ).
fof(i_0_38,plain,
! [X94,X95] :
( ~ aNaturalNumber0(X94)
| ~ aNaturalNumber0(X95)
| ~ sdtlseqdt0(X94,X95)
| ~ sdtlseqdt0(X95,X94)
| X94 = X95 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEAsym])]) ).
fof(i_0_39,plain,
! [X58,X59] :
( ~ aNaturalNumber0(X58)
| ~ aNaturalNumber0(X59)
| aNaturalNumber0(sdtasdt0(X58,X59)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB_02])]) ).
fof(i_0_40,plain,
! [X56,X57] :
( ~ aNaturalNumber0(X56)
| ~ aNaturalNumber0(X57)
| aNaturalNumber0(sdtpldt0(X56,X57)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB])]) ).
fof(i_0_41,plain,
! [X99,X100] :
( ( X100 != X99
| sdtlseqdt0(X99,X100)
| ~ aNaturalNumber0(X99)
| ~ aNaturalNumber0(X100) )
& ( sdtlseqdt0(X100,X99)
| sdtlseqdt0(X99,X100)
| ~ aNaturalNumber0(X99)
| ~ aNaturalNumber0(X100) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETotal])])]) ).
fof(i_0_42,plain,
! [X66,X67] :
( ~ aNaturalNumber0(X66)
| ~ aNaturalNumber0(X67)
| sdtasdt0(X66,X67) = sdtasdt0(X67,X66) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulComm])]) ).
fof(i_0_43,plain,
! [X60,X61] :
( ~ aNaturalNumber0(X60)
| ~ aNaturalNumber0(X61)
| sdtpldt0(X60,X61) = sdtpldt0(X61,X60) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddComm])]) ).
fof(i_0_44,plain,
! [X84,X85] :
( ~ aNaturalNumber0(X84)
| ~ aNaturalNumber0(X85)
| sdtasdt0(X84,X85) != sz00
| X84 = sz00
| X85 = sz00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroMul])]) ).
fof(i_0_45,plain,
! [X82,X83] :
( ( X82 = sz00
| sdtpldt0(X82,X83) != sz00
| ~ aNaturalNumber0(X82)
| ~ aNaturalNumber0(X83) )
& ( X83 = sz00
| sdtpldt0(X82,X83) != sz00
| ~ aNaturalNumber0(X82)
| ~ aNaturalNumber0(X83) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroAdd])])]) ).
fof(i_0_46,plain,
! [X107] :
( ( sz10 != X107
| X107 = sz00
| X107 = sz10
| ~ aNaturalNumber0(X107) )
& ( sdtlseqdt0(sz10,X107)
| X107 = sz00
| X107 = sz10
| ~ aNaturalNumber0(X107) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLENTr])])]) ).
fof(i_0_47,plain,
! [X93] :
( ~ aNaturalNumber0(X93)
| sdtlseqdt0(X93,X93) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLERefl])]) ).
fof(i_0_48,plain,
! [X71] :
( ( sdtasdt0(X71,sz10) = X71
| ~ aNaturalNumber0(X71) )
& ( X71 = sdtasdt0(sz10,X71)
| ~ aNaturalNumber0(X71) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_MulUnit])])]) ).
fof(i_0_49,plain,
! [X65] :
( ( sdtpldt0(X65,sz00) = X65
| ~ aNaturalNumber0(X65) )
& ( X65 = sdtpldt0(sz00,X65)
| ~ aNaturalNumber0(X65) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_AddZero])])]) ).
fof(i_0_50,plain,
! [X72] :
( ( sdtasdt0(X72,sz00) = sz00
| ~ aNaturalNumber0(X72) )
& ( sz00 = sdtasdt0(sz00,X72)
| ~ aNaturalNumber0(X72) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_MulZero])])]) ).
fof(i_0_51,negated_conjecture,
( xm != sz00
& ~ sdtlseqdt0(sz10,xm) ),
inference(fof_nnf,[status(thm)],[i_0_27]) ).
cnf(i_0_52,plain,
( sdtasdt0(sdtpldt0(X1,X2),X3) = sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_53,plain,
( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_54,plain,
( sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X3,X2))
| X2 = sz00
| X1 = X3
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_55,plain,
( sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| X1 = sz00
| X2 = X3
| ~ sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_56,plain,
( sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X2))
| X1 = X3
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_57,plain,
( sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X1,X3))
| X2 = X3
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_58,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_59,plain,
( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_60,plain,
( X2 = sz00
| X1 = X3
| sdtasdt0(X1,X2) != sdtasdt0(X3,X2)
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_61,plain,
( X1 = sz00
| X2 = X3
| sdtasdt0(X1,X2) != sdtasdt0(X1,X3)
| ~ sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_62,plain,
( X1 = X3
| sdtpldt0(X1,X2) != sdtpldt0(X3,X2)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_63,plain,
( X2 = X3
| sdtpldt0(X1,X2) != sdtpldt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_64,plain,
( X1 = sdtmndt0(X3,X2)
| ~ aNaturalNumber0(X1)
| sdtpldt0(X2,X1) != X3
| ~ sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_65,plain,
( sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_66,plain,
( sdtpldt0(X1,esk1_2(X1,X2)) = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_67,plain,
( sdtpldt0(X1,X2) = X3
| X2 != sdtmndt0(X3,X1)
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_68,plain,
( X1 = X3
| X2 = sz00
| sdtasdt0(X1,X2) != sdtasdt0(X3,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_69,plain,
( X2 = X3
| X1 = sz00
| sdtasdt0(X1,X2) != sdtasdt0(X1,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_70,plain,
( X1 = X3
| sdtpldt0(X1,X2) != sdtpldt0(X3,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_71,plain,
( X2 = X3
| sdtpldt0(X1,X2) != sdtpldt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_72,plain,
( aNaturalNumber0(esk1_2(X1,X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_73,plain,
( aNaturalNumber0(X1)
| X1 != sdtmndt0(X2,X3)
| ~ sdtlseqdt0(X3,X2)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_74,plain,
( X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_75,plain,
( sdtlseqdt0(X2,X3)
| ~ aNaturalNumber0(X1)
| sdtpldt0(X2,X1) != X3
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_76,plain,
( aNaturalNumber0(sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_77,plain,
( aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_78,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_79,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_80,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_81,plain,
( X1 = sz00
| X2 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != sz00 ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_82,plain,
( X1 = sz00
| sdtpldt0(X1,X2) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_83,plain,
( X1 = sz00
| sdtpldt0(X2,X1) != sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_84,plain,
( sdtlseqdt0(X2,X1)
| X1 != X2
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_85,plain,
( sdtlseqdt0(sz10,X1)
| X1 = sz00
| X1 = sz10
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_86,plain,
( sdtlseqdt0(X1,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_87,plain,
( sdtasdt0(X1,sz10) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_88,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_89,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_90,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_91,plain,
( sdtasdt0(X1,sz00) = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_92,plain,
( sz00 = sdtasdt0(sz00,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_93,negated_conjecture,
~ sdtlseqdt0(sz10,xm),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_94,hypothesis,
aNaturalNumber0(xn),
inference(split_conjunct,[status(thm)],[m__987]),
[final] ).
cnf(i_0_95,hypothesis,
aNaturalNumber0(xm),
inference(split_conjunct,[status(thm)],[m__987]),
[final] ).
cnf(i_0_96,plain,
aNaturalNumber0(sz10),
inference(split_conjunct,[status(thm)],[mSortsC_01]),
[final] ).
cnf(i_0_97,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[mSortsC]),
[final] ).
cnf(i_0_98,negated_conjecture,
xm != sz00,
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_99,plain,
sz10 != sz00,
inference(split_conjunct,[status(thm)],[mSortsC_01]),
[final] ).
cnf(i_0_100,axiom,
X1 = X1 ).
cnf(i_0_101,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_102,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_103,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| sdtmndt0(X1,X3) = sdtmndt0(X2,X3) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| sdtmndt0(X3,X1) = sdtmndt0(X3,X2) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_100_001,axiom,
X1 = X1 ).
cnf(i_0_101_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_102_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_103_004,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_104_005,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_105_006,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_106_007,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_107_008,axiom,
( X1 != X2
| sdtmndt0(X1,X3) = sdtmndt0(X2,X3) ) ).
cnf(i_0_108_009,axiom,
( X1 != X2
| sdtmndt0(X3,X1) = sdtmndt0(X3,X2) ) ).
cnf(i_0_109_010,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_110_011,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_111_012,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_112,plain,
( ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X2,sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(sdtpldt0(X2,X1))
| X1 = sdtmndt0(sdtpldt0(X2,X1),X2) ),
inference(equality_inference,[],[64]) ).
cnf(i_0_113,plain,
( ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X1,sdtmndt0(X2,X1)) = X2 ),
inference(equality_inference,[],[67]) ).
cnf(i_0_114,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| X1 = X1
| X2 = sz00 ),
inference(equality_inference,[],[68]) ).
cnf(i_0_115,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| X1 = X1
| X2 = sz00 ),
inference(equality_inference,[],[69]) ).
cnf(i_0_116,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X2)
| X2 = X2 ),
inference(equality_inference,[],[70]) ).
cnf(i_0_117,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X2)
| X2 = X2 ),
inference(equality_inference,[],[71]) ).
cnf(i_0_118,plain,
( ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtmndt0(X2,X1)) ),
inference(equality_inference,[],[73]) ).
cnf(i_0_119,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| sdtlseqdt0(X1,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2) ),
inference(equality_inference,[],[75]) ).
cnf(i_0_120,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X1) ),
inference(equality_inference,[],[84]) ).
cnf(i_0_121,plain,
sdtlseqdt0(xn,xn),
inference(scs_inference,[],[i_0_94,i_0_86]) ).
cnf(i_0_122,plain,
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_86]) ).
cnf(i_0_123,plain,
sdtlseqdt0(xm,sz10),
inference(scs_inference,[],[i_0_93,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78]) ).
cnf(i_0_124,plain,
( sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_125,plain,
xm = sz10,
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85]) ).
cnf(i_0_126,plain,
( X1 = sz00
| X1 = sz10
| sdtlseqdt0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_127,plain,
sdtpldt0(xn,sdtmndt0(xn,xn)) = xn,
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113]) ).
cnf(i_0_128,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X1,sdtmndt0(X2,X1)) = X2
| ~ sdtlseqdt0(X1,X2) ),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_129,plain,
aNaturalNumber0(sdtmndt0(xn,xn)),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118]) ).
cnf(i_0_130,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtmndt0(X2,X1))
| ~ sdtlseqdt0(X1,X2) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_131,plain,
sz10 = xm,
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101]) ).
cnf(i_0_132,plain,
( X1 = xn
| X1 != sdtpldt0(xn,sdtmndt0(xn,xn)) ),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101,i_0_102]) ).
cnf(i_0_133,plain,
~ sdtlseqdt0(xm,xm),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101,i_0_102,i_0_110]) ).
cnf(i_0_134,plain,
~ sdtlseqdt0(sz10,sz10),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101,i_0_102,i_0_110,i_0_111]) ).
cnf(i_0_135,plain,
( X1 != X2
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_136,plain,
( sdtpldt0(xn,xn) != sdtpldt0(xn,sdtmndt0(xn,xn))
| xn = sdtmndt0(xn,xn) ),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101,i_0_102,i_0_110,i_0_111,i_0_84,i_0_64]) ).
cnf(i_0_137,plain,
( sdtpldt0(X1,X2) != X3
| X2 = sdtmndt0(X3,X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_138,plain,
( ~ sdtlseqdt0(xm,sz00)
| sz00 != sdtpldt0(xn,xn)
| sdtpldt0(xn,xn) != sdtpldt0(xn,sdtmndt0(xn,xn))
| sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xm,sz00)) ),
inference(scs_inference,[],[i_0_93,i_0_98,i_0_94,i_0_95,i_0_96,i_0_97,i_0_86,i_0_78,i_0_85,i_0_113,i_0_118,i_0_101,i_0_102,i_0_110,i_0_111,i_0_84,i_0_64,i_0_109,i_0_119,i_0_75,i_0_67,i_0_73,i_0_112,i_0_65,i_0_55]) ).
cnf(i_0_139,plain,
sdtpldt0(xn,sdtmndt0(xn,xn)) = xn,
inference(equality_inference,[],[132]) ).
cnf(i_0_140,plain,
$false,
inference(scs_inference,[],[i_0_96,i_0_134,i_0_86]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM464+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.14/0.32 % Computer : n011.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 00:35:32 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 0.28/1.61 % Version : CSE_E---1.7
% 0.28/1.61 % Problem : theBenchmark.p
% 0.28/1.61 % SZS status Theorem for theBenchmark.p
% 0.28/1.61 % SZS output start CNFRefutation
% See solution above
% 0.39/1.72 % Total time : 1.273s
%------------------------------------------------------------------------------