%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM464+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 : n026.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:26 PM UTC 2026
% Result : Theorem 0.30s 1.62s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 68)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( xm != sz00
=> ( ? [X1] :
( aNaturalNumber0(X1)
& sdtpldt0(sz10,X1) = xm )
| 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
=> ( ? [X1] :
( aNaturalNumber0(X1)
& sdtpldt0(sz10,X1) = xm )
| sdtlseqdt0(sz10,xm) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(i_0_28,plain,
! [X74,X75,X76] :
( ( sdtasdt0(X74,sdtpldt0(X75,X76)) = sdtpldt0(sdtasdt0(X74,X75),sdtasdt0(X74,X76))
| ~ aNaturalNumber0(X74)
| ~ aNaturalNumber0(X75)
| ~ aNaturalNumber0(X76) )
& ( sdtasdt0(sdtpldt0(X75,X76),X74) = sdtpldt0(sdtasdt0(X75,X74),sdtasdt0(X76,X74))
| ~ aNaturalNumber0(X74)
| ~ aNaturalNumber0(X75)
| ~ aNaturalNumber0(X76) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAMDistr])])]) ).
fof(i_0_29,plain,
! [X105,X106,X107] :
( ( sdtasdt0(X105,X106) != sdtasdt0(X105,X107)
| X105 = sz00
| X106 = X107
| ~ sdtlseqdt0(X106,X107)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106)
| ~ aNaturalNumber0(X107) )
& ( sdtlseqdt0(sdtasdt0(X105,X106),sdtasdt0(X105,X107))
| X105 = sz00
| X106 = X107
| ~ sdtlseqdt0(X106,X107)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106)
| ~ aNaturalNumber0(X107) )
& ( sdtasdt0(X106,X105) != sdtasdt0(X107,X105)
| X105 = sz00
| X106 = X107
| ~ sdtlseqdt0(X106,X107)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106)
| ~ aNaturalNumber0(X107) )
& ( sdtlseqdt0(sdtasdt0(X106,X105),sdtasdt0(X107,X105))
| X105 = sz00
| X106 = X107
| ~ sdtlseqdt0(X106,X107)
| ~ aNaturalNumber0(X105)
| ~ aNaturalNumber0(X106)
| ~ aNaturalNumber0(X107) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMonMul])])]) ).
fof(i_0_30,plain,
! [X102,X103,X104] :
( ( sdtpldt0(X104,X102) != sdtpldt0(X104,X103)
| ~ aNaturalNumber0(X104)
| X102 = X103
| ~ sdtlseqdt0(X102,X103)
| ~ aNaturalNumber0(X102)
| ~ aNaturalNumber0(X103) )
& ( sdtlseqdt0(sdtpldt0(X104,X102),sdtpldt0(X104,X103))
| ~ aNaturalNumber0(X104)
| X102 = X103
| ~ sdtlseqdt0(X102,X103)
| ~ aNaturalNumber0(X102)
| ~ aNaturalNumber0(X103) )
& ( sdtpldt0(X102,X104) != sdtpldt0(X103,X104)
| ~ aNaturalNumber0(X104)
| X102 = X103
| ~ sdtlseqdt0(X102,X103)
| ~ aNaturalNumber0(X102)
| ~ aNaturalNumber0(X103) )
& ( sdtlseqdt0(sdtpldt0(X102,X104),sdtpldt0(X103,X104))
| ~ aNaturalNumber0(X104)
| X102 = X103
| ~ sdtlseqdt0(X102,X103)
| ~ aNaturalNumber0(X102)
| ~ aNaturalNumber0(X103) ) ),
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,
! [X69,X70,X71] :
( ~ aNaturalNumber0(X69)
| ~ aNaturalNumber0(X70)
| ~ aNaturalNumber0(X71)
| sdtasdt0(sdtasdt0(X69,X70),X71) = sdtasdt0(X69,sdtasdt0(X70,X71)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulAsso])]) ).
fof(i_0_32,plain,
! [X63,X64,X65] :
( ~ aNaturalNumber0(X63)
| ~ aNaturalNumber0(X64)
| ~ aNaturalNumber0(X65)
| sdtpldt0(sdtpldt0(X63,X64),X65) = sdtpldt0(X63,sdtpldt0(X64,X65)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddAsso])]) ).
fof(i_0_33,plain,
! [X91,X92,X93] :
( ( aNaturalNumber0(X93)
| X93 != sdtmndt0(X92,X91)
| ~ sdtlseqdt0(X91,X92)
| ~ aNaturalNumber0(X91)
| ~ aNaturalNumber0(X92) )
& ( sdtpldt0(X91,X93) = X92
| X93 != sdtmndt0(X92,X91)
| ~ sdtlseqdt0(X91,X92)
| ~ aNaturalNumber0(X91)
| ~ aNaturalNumber0(X92) )
& ( ~ aNaturalNumber0(X93)
| sdtpldt0(X91,X93) != X92
| X93 = sdtmndt0(X92,X91)
| ~ sdtlseqdt0(X91,X92)
| ~ aNaturalNumber0(X91)
| ~ aNaturalNumber0(X92) ) ),
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,
! [X97,X98,X99] :
( ~ aNaturalNumber0(X97)
| ~ aNaturalNumber0(X98)
| ~ aNaturalNumber0(X99)
| ~ sdtlseqdt0(X97,X98)
| ~ sdtlseqdt0(X98,X99)
| sdtlseqdt0(X97,X99) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETran])]) ).
fof(i_0_35,plain,
! [X87,X88,X90] :
( ( aNaturalNumber0(esk1_2(X87,X88))
| ~ sdtlseqdt0(X87,X88)
| ~ aNaturalNumber0(X87)
| ~ aNaturalNumber0(X88) )
& ( sdtpldt0(X87,esk1_2(X87,X88)) = X88
| ~ sdtlseqdt0(X87,X88)
| ~ aNaturalNumber0(X87)
| ~ aNaturalNumber0(X88) )
& ( ~ aNaturalNumber0(X90)
| sdtpldt0(X87,X90) != X88
| sdtlseqdt0(X87,X88)
| ~ aNaturalNumber0(X87)
| ~ aNaturalNumber0(X88) ) ),
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,
! [X80,X81,X82] :
( ( sdtasdt0(X80,X81) != sdtasdt0(X80,X82)
| X81 = X82
| ~ aNaturalNumber0(X81)
| ~ aNaturalNumber0(X82)
| X80 = sz00
| ~ aNaturalNumber0(X80) )
& ( sdtasdt0(X81,X80) != sdtasdt0(X82,X80)
| X81 = X82
| ~ aNaturalNumber0(X81)
| ~ aNaturalNumber0(X82)
| X80 = sz00
| ~ aNaturalNumber0(X80) ) ),
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,
! [X77,X78,X79] :
( ( sdtpldt0(X77,X78) != sdtpldt0(X77,X79)
| X78 = X79
| ~ aNaturalNumber0(X77)
| ~ aNaturalNumber0(X78)
| ~ aNaturalNumber0(X79) )
& ( sdtpldt0(X78,X77) != sdtpldt0(X79,X77)
| X78 = X79
| ~ aNaturalNumber0(X77)
| ~ aNaturalNumber0(X78)
| ~ aNaturalNumber0(X79) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddCanc])])]) ).
fof(i_0_38,plain,
! [X95,X96] :
( ~ aNaturalNumber0(X95)
| ~ aNaturalNumber0(X96)
| ~ sdtlseqdt0(X95,X96)
| ~ sdtlseqdt0(X96,X95)
| X95 = X96 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLEAsym])]) ).
fof(i_0_39,plain,
! [X59,X60] :
( ~ aNaturalNumber0(X59)
| ~ aNaturalNumber0(X60)
| aNaturalNumber0(sdtasdt0(X59,X60)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB_02])]) ).
fof(i_0_40,plain,
! [X57,X58] :
( ~ aNaturalNumber0(X57)
| ~ aNaturalNumber0(X58)
| aNaturalNumber0(sdtpldt0(X57,X58)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB])]) ).
fof(i_0_41,plain,
! [X100,X101] :
( ( X101 != X100
| sdtlseqdt0(X100,X101)
| ~ aNaturalNumber0(X100)
| ~ aNaturalNumber0(X101) )
& ( sdtlseqdt0(X101,X100)
| sdtlseqdt0(X100,X101)
| ~ aNaturalNumber0(X100)
| ~ aNaturalNumber0(X101) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLETotal])])]) ).
fof(i_0_42,plain,
! [X67,X68] :
( ~ aNaturalNumber0(X67)
| ~ aNaturalNumber0(X68)
| sdtasdt0(X67,X68) = sdtasdt0(X68,X67) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulComm])]) ).
fof(i_0_43,plain,
! [X61,X62] :
( ~ aNaturalNumber0(X61)
| ~ aNaturalNumber0(X62)
| sdtpldt0(X61,X62) = sdtpldt0(X62,X61) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddComm])]) ).
fof(i_0_44,plain,
! [X85,X86] :
( ~ aNaturalNumber0(X85)
| ~ aNaturalNumber0(X86)
| sdtasdt0(X85,X86) != sz00
| X85 = sz00
| X86 = sz00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroMul])]) ).
fof(i_0_45,plain,
! [X83,X84] :
( ( X83 = sz00
| sdtpldt0(X83,X84) != sz00
| ~ aNaturalNumber0(X83)
| ~ aNaturalNumber0(X84) )
& ( X84 = sz00
| sdtpldt0(X83,X84) != sz00
| ~ aNaturalNumber0(X83)
| ~ aNaturalNumber0(X84) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mZeroAdd])])]) ).
fof(i_0_46,negated_conjecture,
! [X109] :
( xm != sz00
& ( ~ aNaturalNumber0(X109)
| sdtpldt0(sz10,X109) != xm )
& ~ sdtlseqdt0(sz10,xm) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_27])])]) ).
fof(i_0_47,plain,
! [X108] :
( ( sz10 != X108
| X108 = sz00
| X108 = sz10
| ~ aNaturalNumber0(X108) )
& ( sdtlseqdt0(sz10,X108)
| X108 = sz00
| X108 = sz10
| ~ aNaturalNumber0(X108) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLENTr])])]) ).
fof(i_0_48,plain,
! [X94] :
( ~ aNaturalNumber0(X94)
| sdtlseqdt0(X94,X94) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLERefl])]) ).
fof(i_0_49,plain,
! [X72] :
( ( sdtasdt0(X72,sz10) = X72
| ~ aNaturalNumber0(X72) )
& ( X72 = sdtasdt0(sz10,X72)
| ~ aNaturalNumber0(X72) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_MulUnit])])]) ).
fof(i_0_50,plain,
! [X66] :
( ( sdtpldt0(X66,sz00) = X66
| ~ aNaturalNumber0(X66) )
& ( X66 = sdtpldt0(sz00,X66)
| ~ aNaturalNumber0(X66) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_AddZero])])]) ).
fof(i_0_51,plain,
! [X73] :
( ( sdtasdt0(X73,sz00) = sz00
| ~ aNaturalNumber0(X73) )
& ( sz00 = sdtasdt0(sz00,X73)
| ~ aNaturalNumber0(X73) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m_MulZero])])]) ).
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,negated_conjecture,
( ~ aNaturalNumber0(X1)
| sdtpldt0(sz10,X1) != xm ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_86,plain,
( sdtlseqdt0(sz10,X1)
| X1 = sz00
| X1 = sz10
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_87,plain,
( sdtlseqdt0(X1,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_88,plain,
( sdtasdt0(X1,sz10) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_89,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_90,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_91,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_92,plain,
( sdtasdt0(X1,sz00) = sz00
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_93,plain,
( sz00 = sdtasdt0(sz00,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_94,negated_conjecture,
~ sdtlseqdt0(sz10,xm),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_95,hypothesis,
aNaturalNumber0(xn),
inference(split_conjunct,[status(thm)],[m__987]),
[final] ).
cnf(i_0_96,hypothesis,
aNaturalNumber0(xm),
inference(split_conjunct,[status(thm)],[m__987]),
[final] ).
cnf(i_0_97,plain,
aNaturalNumber0(sz10),
inference(split_conjunct,[status(thm)],[mSortsC_01]),
[final] ).
cnf(i_0_98,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[mSortsC]),
[final] ).
cnf(i_0_99,negated_conjecture,
xm != sz00,
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_100,plain,
sz10 != sz00,
inference(split_conjunct,[status(thm)],[mSortsC_01]),
[final] ).
cnf(i_0_101,axiom,
X1 = X1 ).
cnf(i_0_102,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_103,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_104,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| sdtmndt0(X1,X3) = sdtmndt0(X2,X3) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| sdtmndt0(X3,X1) = sdtmndt0(X3,X2) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_101_001,axiom,
X1 = X1 ).
cnf(i_0_102_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_103_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_104_004,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_105_005,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_106_006,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_107_007,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_108_008,axiom,
( X1 != X2
| sdtmndt0(X1,X3) = sdtmndt0(X2,X3) ) ).
cnf(i_0_109_009,axiom,
( X1 != X2
| sdtmndt0(X3,X1) = sdtmndt0(X3,X2) ) ).
cnf(i_0_110_010,axiom,
( X1 != X2
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(X2) ) ).
cnf(i_0_111_011,axiom,
( X1 != X2
| ~ sdtlseqdt0(X1,X3)
| sdtlseqdt0(X2,X3) ) ).
cnf(i_0_112_012,axiom,
( X1 != X2
| ~ sdtlseqdt0(X3,X1)
| sdtlseqdt0(X3,X2) ) ).
cnf(i_0_113,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_114,plain,
( ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X1,sdtmndt0(X2,X1)) = X2 ),
inference(equality_inference,[],[67]) ).
cnf(i_0_115,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| X1 = X1
| X2 = sz00 ),
inference(equality_inference,[],[68]) ).
cnf(i_0_116,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| X1 = X1
| X2 = sz00 ),
inference(equality_inference,[],[69]) ).
cnf(i_0_117,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X2)
| X2 = X2 ),
inference(equality_inference,[],[70]) ).
cnf(i_0_118,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X2)
| X2 = X2 ),
inference(equality_inference,[],[71]) ).
cnf(i_0_119,plain,
( ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtmndt0(X2,X1)) ),
inference(equality_inference,[],[73]) ).
cnf(i_0_120,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| sdtlseqdt0(X1,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2) ),
inference(equality_inference,[],[75]) ).
cnf(i_0_121,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X1) ),
inference(equality_inference,[],[84]) ).
cnf(i_0_122,plain,
sdtlseqdt0(xn,xn),
inference(scs_inference,[],[i_0_95,i_0_87]) ).
cnf(i_0_123,plain,
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X1) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_124,plain,
sdtpldt0(xn,sdtmndt0(xn,xn)) = xn,
inference(scs_inference,[],[i_0_95,i_0_87,i_0_114]) ).
cnf(i_0_125,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X1,sdtmndt0(X2,X1)) = X2
| ~ sdtlseqdt0(X1,X2) ),
inference(rename_variables,[],[i_0_114]) ).
cnf(i_0_126,plain,
aNaturalNumber0(sdtmndt0(xn,xn)),
inference(scs_inference,[],[i_0_95,i_0_87,i_0_114,i_0_119]) ).
cnf(i_0_127,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtmndt0(X2,X1))
| ~ sdtlseqdt0(X1,X2) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_128,plain,
sdtlseqdt0(xm,sz10),
inference(scs_inference,[],[i_0_94,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78]) ).
cnf(i_0_129,plain,
( sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_130,plain,
xm = sz10,
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86]) ).
cnf(i_0_131,plain,
( X1 = sz00
| X1 = sz10
| sdtlseqdt0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(rename_variables,[],[i_0_86]) ).
cnf(i_0_132,plain,
xn = sdtpldt0(xn,sdtmndt0(xn,xn)),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102]) ).
cnf(i_0_133,plain,
aNaturalNumber0(sdtpldt0(xn,sdtmndt0(xn,xn))),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110]) ).
cnf(i_0_134,plain,
( X1 = sz10
| X1 != xm ),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103]) ).
cnf(i_0_135,plain,
~ sdtlseqdt0(xm,xm),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111]) ).
cnf(i_0_136,plain,
sz10 != xm,
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112]) ).
cnf(i_0_137,plain,
sdtlseqdt0(xn,sdtpldt0(xn,sdtmndt0(xn,xn))),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112,i_0_84]) ).
cnf(i_0_138,plain,
( X1 != X2
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X2,X1) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_139,plain,
( sdtlseqdt0(xn,sz10)
| sdtpldt0(xn,xn) != xm ),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112,i_0_84,i_0_75]) ).
cnf(i_0_140,plain,
( sdtpldt0(X1,X2) != X3
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3)
| sdtlseqdt0(X1,X3)
| ~ aNaturalNumber0(X2) ),
inference(rename_variables,[],[i_0_75]) ).
cnf(i_0_141,plain,
( sdtmndt0(xn,xn) = sdtmndt0(sdtpldt0(xn,sdtmndt0(xn,xn)),xn)
| sdtpldt0(xn,xn) != xm ),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112,i_0_84,i_0_75,i_0_113]) ).
cnf(i_0_142,plain,
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| X2 = sdtmndt0(sdtpldt0(X1,X2),X1)
| ~ sdtlseqdt0(X1,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2) ),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_143,plain,
( sdtpldt0(xn,xn) != xm
| xn = sdtmndt0(sz10,xn) ),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112,i_0_84,i_0_75,i_0_113,i_0_64]) ).
cnf(i_0_144,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_145,plain,
( ~ sdtlseqdt0(xm,sz00)
| sdtlseqdt0(sz10,sz10)
| sdtpldt0(xn,xn) != xm
| sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xm,sz00)) ),
inference(scs_inference,[],[i_0_94,i_0_99,i_0_95,i_0_96,i_0_97,i_0_98,i_0_87,i_0_114,i_0_119,i_0_78,i_0_86,i_0_102,i_0_110,i_0_103,i_0_111,i_0_112,i_0_84,i_0_75,i_0_113,i_0_64,i_0_65,i_0_55]) ).
cnf(i_0_146,plain,
xm = sz10,
inference(equality_inference,[],[134]) ).
cnf(i_0_147,plain,
$false,
inference(scs_inference,[],[i_0_96,i_0_135,i_0_87]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM464+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 : n026.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 00:36:08 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.30/1.62 % Version : CSE_E---1.7
% 0.30/1.62 % Problem : theBenchmark.p
% 0.30/1.62 % SZS status Theorem for theBenchmark.p
% 0.30/1.62 % SZS output start CNFRefutation
% See solution above
% 0.40/1.74 % Total time : 1.270s
%------------------------------------------------------------------------------