%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG097+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 : n012.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:19 PM UTC 2026
% Result : Theorem 259.18s 154.20s
% Output : CNFRefutation 265.98s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_149)
% Comments :
%------------------------------------------------------------------------------
fof(mDefSSum,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ! [X3] :
( X3 = sdtpldt1(X1,X2)
<=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
<=> ? [X5,X6] :
( aElementOf0(X5,X1)
& aElementOf0(X6,X2)
& sdtpldt0(X5,X6) = X4 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSSum) ).
fof(mDefSInt,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ! [X3] :
( X3 = sdtasasdt0(X1,X2)
<=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
<=> ( aElementOf0(X4,X1)
& aElementOf0(X4,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSInt) ).
fof(mDefIdeal,axiom,
! [X1] :
( aIdeal0(X1)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> ( ! [X3] :
( aElementOf0(X3,X1)
=> aElementOf0(sdtpldt0(X2,X3),X1) )
& ! [X3] :
( aElement0(X3)
=> aElementOf0(sdtasdt0(X3,X2),X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefIdeal) ).
fof(mDefMod,axiom,
! [X1,X2,X3] :
( ( aElement0(X1)
& aElement0(X2)
& aIdeal0(X3) )
=> ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
<=> aElementOf0(sdtpldt0(X1,smndt0(X2)),X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefMod) ).
fof(m__,conjecture,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(mSetEq,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ( ( ! [X3] :
( aElementOf0(X3,X1)
=> aElementOf0(X3,X2) )
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) ) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSetEq) ).
fof(mAMDistr,axiom,
! [X1,X2,X3] :
( ( aElement0(X1)
& aElement0(X2)
& aElement0(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/sandbox/benchmark/theBenchmark.p',mAMDistr) ).
fof(mMulAsso,axiom,
! [X1,X2,X3] :
( ( aElement0(X1)
& aElement0(X2)
& aElement0(X3) )
=> sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
fof(mAddAsso,axiom,
! [X1,X2,X3] :
( ( aElement0(X1)
& aElement0(X2)
& aElement0(X3) )
=> sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(mIdeInt,axiom,
! [X1,X2] :
( ( aIdeal0(X1)
& aIdeal0(X2) )
=> aIdeal0(sdtasasdt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIdeInt) ).
fof(mIdeSum,axiom,
! [X1,X2] :
( ( aIdeal0(X1)
& aIdeal0(X2) )
=> aIdeal0(sdtpldt1(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIdeSum) ).
fof(mSortsB_02,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> aElement0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(mSortsB,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> aElement0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
fof(mMulComm,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(mAddComm,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> sdtpldt0(X1,X2) = sdtpldt0(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(m__1205_03,hypothesis,
! [X1] :
( aElement0(X1)
=> aElementOf0(X1,sdtpldt1(xI,xJ)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1205_03) ).
fof(mCancel,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> ( sdtasdt0(X1,X2) = sz00
=> ( X1 = sz00
| X2 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCancel) ).
fof(mEOfElem,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> aElement0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(mMulMnOne,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
& smndt0(X1) = sdtasdt0(X1,smndt0(sz10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulMnOne) ).
fof(mAddInvr,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtpldt0(X1,smndt0(X1)) = sz00
& sz00 = sdtpldt0(smndt0(X1),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddInvr) ).
fof(mMulUnit,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtasdt0(X1,sz10) = X1
& X1 = sdtasdt0(sz10,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulUnit) ).
fof(mAddZero,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtpldt0(X1,sz00) = X1
& X1 = sdtpldt0(sz00,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(mMulZero,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtasdt0(X1,sz00) = sz00
& sz00 = sdtasdt0(sz00,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulZero) ).
fof(mSortsU,axiom,
! [X1] :
( aElement0(X1)
=> aElement0(smndt0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsU) ).
fof(m__1374,hypothesis,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1374) ).
fof(m__1319,hypothesis,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1319) ).
fof(m__1294,hypothesis,
( aElementOf0(xa,xI)
& aElementOf0(xb,xJ)
& sdtpldt0(xa,xb) = sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1294) ).
fof(m__1205,hypothesis,
( aIdeal0(xI)
& aIdeal0(xJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1205) ).
fof(m__1217,hypothesis,
( aElement0(xx)
& aElement0(xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1217) ).
fof(mSortsC_01,axiom,
aElement0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(mSortsC,axiom,
aElement0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC) ).
fof(mUnNeZr,axiom,
sz10 != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mUnNeZr) ).
fof(i_0_32,plain,
! [X93,X94,X95,X96,X99,X100,X101,X102,X104,X105] :
( ( aSet0(X95)
| X95 != sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( aElementOf0(esk3_4(X93,X94,X95,X96),X93)
| ~ aElementOf0(X96,X95)
| X95 != sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( aElementOf0(esk4_4(X93,X94,X95,X96),X94)
| ~ aElementOf0(X96,X95)
| X95 != sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( sdtpldt0(esk3_4(X93,X94,X95,X96),esk4_4(X93,X94,X95,X96)) = X96
| ~ aElementOf0(X96,X95)
| X95 != sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( ~ aElementOf0(X100,X93)
| ~ aElementOf0(X101,X94)
| sdtpldt0(X100,X101) != X99
| aElementOf0(X99,X95)
| X95 != sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( ~ aElementOf0(esk5_3(X93,X94,X102),X102)
| ~ aElementOf0(X104,X93)
| ~ aElementOf0(X105,X94)
| sdtpldt0(X104,X105) != esk5_3(X93,X94,X102)
| ~ aSet0(X102)
| X102 = sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( aElementOf0(esk6_3(X93,X94,X102),X93)
| aElementOf0(esk5_3(X93,X94,X102),X102)
| ~ aSet0(X102)
| X102 = sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( aElementOf0(esk7_3(X93,X94,X102),X94)
| aElementOf0(esk5_3(X93,X94,X102),X102)
| ~ aSet0(X102)
| X102 = sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) )
& ( sdtpldt0(esk6_3(X93,X94,X102),esk7_3(X93,X94,X102)) = esk5_3(X93,X94,X102)
| aElementOf0(esk5_3(X93,X94,X102),X102)
| ~ aSet0(X102)
| X102 = sdtpldt1(X93,X94)
| ~ aSet0(X93)
| ~ aSet0(X94) ) ),
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)],[mDefSSum])])])])])]) ).
fof(i_0_33,plain,
! [X108,X109,X110,X111,X112,X113] :
( ( aSet0(X110)
| X110 != sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( aElementOf0(X111,X108)
| ~ aElementOf0(X111,X110)
| X110 != sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( aElementOf0(X111,X109)
| ~ aElementOf0(X111,X110)
| X110 != sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( ~ aElementOf0(X112,X108)
| ~ aElementOf0(X112,X109)
| aElementOf0(X112,X110)
| X110 != sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( ~ aElementOf0(esk8_3(X108,X109,X113),X113)
| ~ aElementOf0(esk8_3(X108,X109,X113),X108)
| ~ aElementOf0(esk8_3(X108,X109,X113),X109)
| ~ aSet0(X113)
| X113 = sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( aElementOf0(esk8_3(X108,X109,X113),X108)
| aElementOf0(esk8_3(X108,X109,X113),X113)
| ~ aSet0(X113)
| X113 = sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) )
& ( aElementOf0(esk8_3(X108,X109,X113),X109)
| aElementOf0(esk8_3(X108,X109,X113),X113)
| ~ aSet0(X113)
| X113 = sdtasasdt0(X108,X109)
| ~ aSet0(X108)
| ~ aSet0(X109) ) ),
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)],[mDefSInt])])])])])]) ).
fof(i_0_34,plain,
! [X115,X116,X117,X118,X119] :
( ( aSet0(X115)
| ~ aIdeal0(X115) )
& ( ~ aElementOf0(X117,X115)
| aElementOf0(sdtpldt0(X116,X117),X115)
| ~ aElementOf0(X116,X115)
| ~ aIdeal0(X115) )
& ( ~ aElement0(X118)
| aElementOf0(sdtasdt0(X118,X116),X115)
| ~ aElementOf0(X116,X115)
| ~ aIdeal0(X115) )
& ( aElementOf0(esk9_1(X119),X119)
| ~ aSet0(X119)
| aIdeal0(X119) )
& ( aElement0(esk11_1(X119))
| aElementOf0(esk10_1(X119),X119)
| ~ aSet0(X119)
| aIdeal0(X119) )
& ( ~ aElementOf0(sdtasdt0(esk11_1(X119),esk9_1(X119)),X119)
| aElementOf0(esk10_1(X119),X119)
| ~ aSet0(X119)
| aIdeal0(X119) )
& ( aElement0(esk11_1(X119))
| ~ aElementOf0(sdtpldt0(esk9_1(X119),esk10_1(X119)),X119)
| ~ aSet0(X119)
| aIdeal0(X119) )
& ( ~ aElementOf0(sdtasdt0(esk11_1(X119),esk9_1(X119)),X119)
| ~ aElementOf0(sdtpldt0(esk9_1(X119),esk10_1(X119)),X119)
| ~ aSet0(X119)
| aIdeal0(X119) ) ),
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)],[mDefIdeal])])])])])]) ).
fof(i_0_35,plain,
! [X127,X128,X129] :
( ( ~ sdteqdtlpzmzozddtrp0(X127,X128,X129)
| aElementOf0(sdtpldt0(X127,smndt0(X128)),X129)
| ~ aElement0(X127)
| ~ aElement0(X128)
| ~ aIdeal0(X129) )
& ( ~ aElementOf0(sdtpldt0(X127,smndt0(X128)),X129)
| sdteqdtlpzmzozddtrp0(X127,X128,X129)
| ~ aElement0(X127)
| ~ aElement0(X128)
| ~ aIdeal0(X129) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefMod])])]) ).
fof(i_0_36,negated_conjecture,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[m__])]) ).
fof(i_0_37,plain,
! [X89,X90] :
( ( aElementOf0(esk2_2(X89,X90),X90)
| aElementOf0(esk1_2(X89,X90),X89)
| X89 = X90
| ~ aSet0(X89)
| ~ aSet0(X90) )
& ( ~ aElementOf0(esk2_2(X89,X90),X89)
| aElementOf0(esk1_2(X89,X90),X89)
| X89 = X90
| ~ aSet0(X89)
| ~ aSet0(X90) )
& ( aElementOf0(esk2_2(X89,X90),X90)
| ~ aElementOf0(esk1_2(X89,X90),X90)
| X89 = X90
| ~ aSet0(X89)
| ~ aSet0(X90) )
& ( ~ aElementOf0(esk2_2(X89,X90),X89)
| ~ aElementOf0(esk1_2(X89,X90),X90)
| X89 = X90
| ~ aSet0(X89)
| ~ aSet0(X90) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSetEq])])])]) ).
fof(i_0_38,plain,
! [X80,X81,X82] :
( ( sdtasdt0(X80,sdtpldt0(X81,X82)) = sdtpldt0(sdtasdt0(X80,X81),sdtasdt0(X80,X82))
| ~ aElement0(X80)
| ~ aElement0(X81)
| ~ aElement0(X82) )
& ( sdtasdt0(sdtpldt0(X81,X82),X80) = sdtpldt0(sdtasdt0(X81,X80),sdtasdt0(X82,X80))
| ~ aElement0(X80)
| ~ aElement0(X81)
| ~ aElement0(X82) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAMDistr])])]) ).
fof(i_0_39,plain,
! [X76,X77,X78] :
( ~ aElement0(X76)
| ~ aElement0(X77)
| ~ aElement0(X78)
| sdtasdt0(sdtasdt0(X76,X77),X78) = sdtasdt0(X76,sdtasdt0(X77,X78)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulAsso])]) ).
fof(i_0_40,plain,
! [X69,X70,X71] :
( ~ aElement0(X69)
| ~ aElement0(X70)
| ~ aElement0(X71)
| sdtpldt0(sdtpldt0(X69,X70),X71) = sdtpldt0(X69,sdtpldt0(X70,X71)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddAsso])]) ).
fof(i_0_41,plain,
! [X125,X126] :
( ~ aIdeal0(X125)
| ~ aIdeal0(X126)
| aIdeal0(sdtasasdt0(X125,X126)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIdeInt])]) ).
fof(i_0_42,plain,
! [X123,X124] :
( ~ aIdeal0(X123)
| ~ aIdeal0(X124)
| aIdeal0(sdtpldt1(X123,X124)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mIdeSum])]) ).
fof(i_0_43,plain,
! [X65,X66] :
( ~ aElement0(X65)
| ~ aElement0(X66)
| aElement0(sdtasdt0(X65,X66)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB_02])]) ).
fof(i_0_44,plain,
! [X63,X64] :
( ~ aElement0(X63)
| ~ aElement0(X64)
| aElement0(sdtpldt0(X63,X64)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsB])]) ).
fof(i_0_45,plain,
! [X74,X75] :
( ~ aElement0(X74)
| ~ aElement0(X75)
| sdtasdt0(X74,X75) = sdtasdt0(X75,X74) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulComm])]) ).
fof(i_0_46,plain,
! [X67,X68] :
( ~ aElement0(X67)
| ~ aElement0(X68)
| sdtpldt0(X67,X68) = sdtpldt0(X68,X67) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddComm])]) ).
fof(i_0_47,hypothesis,
! [X130] :
( ~ aElement0(X130)
| aElementOf0(X130,sdtpldt1(xI,xJ)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__1205_03])]) ).
fof(i_0_48,plain,
! [X85,X86] :
( ~ aElement0(X85)
| ~ aElement0(X86)
| sdtasdt0(X85,X86) != sz00
| X85 = sz00
| X86 = sz00 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCancel])]) ).
fof(i_0_49,plain,
! [X87,X88] :
( ~ aSet0(X87)
| ~ aElementOf0(X88,X87)
| aElement0(X88) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEOfElem])])]) ).
fof(i_0_50,plain,
! [X83] :
( ( sdtasdt0(smndt0(sz10),X83) = smndt0(X83)
| ~ aElement0(X83) )
& ( smndt0(X83) = sdtasdt0(X83,smndt0(sz10))
| ~ aElement0(X83) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulMnOne])])]) ).
fof(i_0_51,plain,
! [X73] :
( ( sdtpldt0(X73,smndt0(X73)) = sz00
| ~ aElement0(X73) )
& ( sz00 = sdtpldt0(smndt0(X73),X73)
| ~ aElement0(X73) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddInvr])])]) ).
fof(i_0_52,plain,
! [X79] :
( ( sdtasdt0(X79,sz10) = X79
| ~ aElement0(X79) )
& ( X79 = sdtasdt0(sz10,X79)
| ~ aElement0(X79) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulUnit])])]) ).
fof(i_0_53,plain,
! [X72] :
( ( sdtpldt0(X72,sz00) = X72
| ~ aElement0(X72) )
& ( X72 = sdtpldt0(sz00,X72)
| ~ aElement0(X72) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddZero])])]) ).
fof(i_0_54,plain,
! [X84] :
( ( sdtasdt0(X84,sz00) = sz00
| ~ aElement0(X84) )
& ( sz00 = sdtasdt0(sz00,X84)
| ~ aElement0(X84) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mMulZero])])]) ).
fof(i_0_55,plain,
! [X62] :
( ~ aElement0(X62)
| aElement0(smndt0(X62)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSortsU])]) ).
cnf(i_0_56,plain,
( sdtpldt0(esk3_4(X1,X2,X3,X4),esk4_4(X1,X2,X3,X4)) = X4
| ~ aElementOf0(X4,X3)
| X3 != sdtpldt1(X1,X2)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_57,plain,
( X3 = sdtasasdt0(X1,X2)
| ~ aElementOf0(esk8_3(X1,X2,X3),X3)
| ~ aElementOf0(esk8_3(X1,X2,X3),X1)
| ~ aElementOf0(esk8_3(X1,X2,X3),X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_58,plain,
( aElementOf0(esk4_4(X1,X2,X3,X4),X2)
| ~ aElementOf0(X4,X3)
| X3 != sdtpldt1(X1,X2)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_59,plain,
( aElementOf0(esk3_4(X1,X2,X3,X4),X1)
| ~ aElementOf0(X4,X3)
| X3 != sdtpldt1(X1,X2)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_60,plain,
( sdtpldt0(esk6_3(X1,X2,X3),esk7_3(X1,X2,X3)) = esk5_3(X1,X2,X3)
| aElementOf0(esk5_3(X1,X2,X3),X3)
| X3 = sdtpldt1(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_61,plain,
( X3 = sdtpldt1(X1,X2)
| ~ aElementOf0(esk5_3(X1,X2,X3),X3)
| ~ aElementOf0(X4,X1)
| ~ aElementOf0(X5,X2)
| sdtpldt0(X4,X5) != esk5_3(X1,X2,X3)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_62,plain,
( aElementOf0(esk8_3(X1,X2,X3),X1)
| aElementOf0(esk8_3(X1,X2,X3),X3)
| X3 = sdtasasdt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_63,plain,
( aElementOf0(esk8_3(X1,X2,X3),X2)
| aElementOf0(esk8_3(X1,X2,X3),X3)
| X3 = sdtasasdt0(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_64,plain,
( aElementOf0(esk7_3(X1,X2,X3),X2)
| aElementOf0(esk5_3(X1,X2,X3),X3)
| X3 = sdtpldt1(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_65,plain,
( aElementOf0(esk6_3(X1,X2,X3),X1)
| aElementOf0(esk5_3(X1,X2,X3),X3)
| X3 = sdtpldt1(X1,X2)
| ~ aSet0(X3)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_66,plain,
( aIdeal0(X1)
| ~ aElementOf0(sdtasdt0(esk11_1(X1),esk9_1(X1)),X1)
| ~ aElementOf0(sdtpldt0(esk9_1(X1),esk10_1(X1)),X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_67,plain,
( aElementOf0(sdtpldt0(X1,smndt0(X2)),X3)
| ~ sdteqdtlpzmzozddtrp0(X1,X2,X3)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aIdeal0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_68,plain,
( sdteqdtlpzmzozddtrp0(X1,X2,X3)
| ~ aElementOf0(sdtpldt0(X1,smndt0(X2)),X3)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aIdeal0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_69,negated_conjecture,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_70,plain,
( X1 = X2
| ~ aElementOf0(esk2_2(X1,X2),X1)
| ~ aElementOf0(esk1_2(X1,X2),X2)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_71,plain,
( aElementOf0(esk10_1(X1),X1)
| aIdeal0(X1)
| ~ aElementOf0(sdtasdt0(esk11_1(X1),esk9_1(X1)),X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_72,plain,
( sdtasdt0(sdtpldt0(X1,X2),X3) = sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))
| ~ aElement0(X3)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_73,plain,
( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_74,plain,
( aElement0(esk11_1(X1))
| aIdeal0(X1)
| ~ aElementOf0(sdtpldt0(esk9_1(X1),esk10_1(X1)),X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_75,plain,
( aElementOf0(X5,X6)
| ~ aElementOf0(X1,X2)
| ~ aElementOf0(X3,X4)
| sdtpldt0(X1,X3) != X5
| X6 != sdtpldt1(X2,X4)
| ~ aSet0(X2)
| ~ aSet0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_76,hypothesis,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
inference(split_conjunct,[status(thm)],[m__1374]),
[final] ).
cnf(i_0_77,plain,
( aElementOf0(esk2_2(X1,X2),X2)
| X1 = X2
| ~ aElementOf0(esk1_2(X1,X2),X2)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_78,plain,
( aElementOf0(esk1_2(X1,X2),X1)
| X1 = X2
| ~ aElementOf0(esk2_2(X1,X2),X1)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_79,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_80,plain,
( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_81,plain,
( aElementOf0(X1,X4)
| ~ aElementOf0(X1,X2)
| ~ aElementOf0(X1,X3)
| X4 != sdtasasdt0(X2,X3)
| ~ aSet0(X2)
| ~ aSet0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_82,plain,
( aElementOf0(esk2_2(X1,X2),X2)
| aElementOf0(esk1_2(X1,X2),X1)
| X1 = X2
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_83,plain,
( aElementOf0(sdtpldt0(X3,X1),X2)
| ~ aElementOf0(X1,X2)
| ~ aElementOf0(X3,X2)
| ~ aIdeal0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_84,plain,
( aElementOf0(sdtasdt0(X1,X2),X3)
| ~ aElement0(X1)
| ~ aElementOf0(X2,X3)
| ~ aIdeal0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_85,plain,
( aElementOf0(X1,X2)
| ~ aElementOf0(X1,X3)
| X3 != sdtasasdt0(X2,X4)
| ~ aSet0(X2)
| ~ aSet0(X4) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_86,plain,
( aElementOf0(X1,X2)
| ~ aElementOf0(X1,X3)
| X3 != sdtasasdt0(X4,X2)
| ~ aSet0(X4)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_87,hypothesis,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(split_conjunct,[status(thm)],[m__1319]),
[final] ).
cnf(i_0_88,plain,
( aIdeal0(sdtasasdt0(X1,X2))
| ~ aIdeal0(X1)
| ~ aIdeal0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_89,plain,
( aIdeal0(sdtpldt1(X1,X2))
| ~ aIdeal0(X1)
| ~ aIdeal0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_90,plain,
( aElement0(sdtasdt0(X1,X2))
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_91,plain,
( aElement0(sdtpldt0(X1,X2))
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_92,plain,
( aElement0(esk11_1(X1))
| aElementOf0(esk10_1(X1),X1)
| aIdeal0(X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_93,plain,
( aSet0(X1)
| X1 != sdtasasdt0(X2,X3)
| ~ aSet0(X2)
| ~ aSet0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_94,plain,
( aSet0(X1)
| X1 != sdtpldt1(X2,X3)
| ~ aSet0(X2)
| ~ aSet0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_95,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_96,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_97,hypothesis,
( aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_98,plain,
( X1 = sz00
| X2 = sz00
| ~ aElement0(X1)
| ~ aElement0(X2)
| sdtasdt0(X1,X2) != sz00 ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_99,plain,
( aElement0(X2)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_100,plain,
( aElementOf0(esk9_1(X1),X1)
| aIdeal0(X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_101,plain,
( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_102,plain,
( smndt0(X1) = sdtasdt0(X1,smndt0(sz10))
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_103,plain,
( sdtpldt0(X1,smndt0(X1)) = sz00
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_104,plain,
( sz00 = sdtpldt0(smndt0(X1),X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_105,plain,
( sdtasdt0(X1,sz10) = X1
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_106,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_107,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_108,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_109,plain,
( sdtasdt0(X1,sz00) = sz00
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_110,plain,
( sz00 = sdtasdt0(sz00,X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_111,plain,
( aElement0(smndt0(X1))
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_112,plain,
( aSet0(X1)
| ~ aIdeal0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_113,hypothesis,
aElementOf0(xb,xJ),
inference(split_conjunct,[status(thm)],[m__1294]),
[final] ).
cnf(i_0_114,hypothesis,
aElementOf0(xa,xI),
inference(split_conjunct,[status(thm)],[m__1294]),
[final] ).
cnf(i_0_115,hypothesis,
sdtpldt0(xa,xb) = sz10,
inference(split_conjunct,[status(thm)],[m__1294]),
[final] ).
cnf(i_0_116,hypothesis,
aIdeal0(xJ),
inference(split_conjunct,[status(thm)],[m__1205]),
[final] ).
cnf(i_0_117,hypothesis,
aIdeal0(xI),
inference(split_conjunct,[status(thm)],[m__1205]),
[final] ).
cnf(i_0_118,hypothesis,
aElement0(xy),
inference(split_conjunct,[status(thm)],[m__1217]),
[final] ).
cnf(i_0_119,hypothesis,
aElement0(xx),
inference(split_conjunct,[status(thm)],[m__1217]),
[final] ).
cnf(i_0_120,plain,
aElement0(sz10),
inference(split_conjunct,[status(thm)],[mSortsC_01]),
[final] ).
cnf(i_0_121,plain,
aElement0(sz00),
inference(split_conjunct,[status(thm)],[mSortsC]),
[final] ).
cnf(i_0_122,plain,
sz10 != sz00,
inference(split_conjunct,[status(thm)],[mUnNeZr]),
[final] ).
cnf(i_0_123,axiom,
X1 = X1 ).
cnf(i_0_124,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_125,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_126,axiom,
( X1 != X2
| sdtpldt0(X1,X3) = sdtpldt0(X2,X3) ) ).
cnf(i_0_127,axiom,
( X1 != X2
| sdtpldt0(X3,X1) = sdtpldt0(X3,X2) ) ).
cnf(i_0_128,axiom,
( X1 != X2
| sdtasdt0(X1,X3) = sdtasdt0(X2,X3) ) ).
cnf(i_0_129,axiom,
( X1 != X2
| sdtasdt0(X3,X1) = sdtasdt0(X3,X2) ) ).
cnf(i_0_130,axiom,
( X1 != X2
| smndt0(X1) = smndt0(X2) ) ).
cnf(i_0_131,axiom,
( X1 != X2
| sdtpldt1(X1,X3) = sdtpldt1(X2,X3) ) ).
cnf(i_0_132,axiom,
( X1 != X2
| sdtpldt1(X3,X1) = sdtpldt1(X3,X2) ) ).
cnf(i_0_133,axiom,
( X1 != X2
| sdtasasdt0(X1,X3) = sdtasasdt0(X2,X3) ) ).
cnf(i_0_134,axiom,
( X1 != X2
| sdtasasdt0(X3,X1) = sdtasasdt0(X3,X2) ) ).
cnf(i_0_135,axiom,
( X1 != X2
| esk5_3(X1,X3,X4) = esk5_3(X2,X3,X4) ) ).
cnf(i_0_136,axiom,
( X1 != X2
| esk5_3(X3,X1,X4) = esk5_3(X3,X2,X4) ) ).
cnf(i_0_137,axiom,
( X1 != X2
| esk5_3(X3,X4,X1) = esk5_3(X3,X4,X2) ) ).
cnf(i_0_138,axiom,
( X1 != X2
| ~ aElementOf0(X1,X3)
| aElementOf0(X2,X3) ) ).
cnf(i_0_139,axiom,
( X1 != X2
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X2) ) ).
cnf(i_0_140,axiom,
( X1 != X2
| ~ aSet0(X1)
| aSet0(X2) ) ).
cnf(i_0_141,axiom,
( X1 != X2
| ~ aIdeal0(X1)
| aIdeal0(X2) ) ).
cnf(i_0_142,axiom,
( X1 != X2
| ~ sdteqdtlpzmzozddtrp0(X1,X3,X4)
| sdteqdtlpzmzozddtrp0(X2,X3,X4) ) ).
cnf(i_0_143,axiom,
( X1 != X2
| ~ sdteqdtlpzmzozddtrp0(X3,X1,X4)
| sdteqdtlpzmzozddtrp0(X3,X2,X4) ) ).
cnf(i_0_144,axiom,
( X1 != X2
| ~ sdteqdtlpzmzozddtrp0(X3,X4,X1)
| sdteqdtlpzmzozddtrp0(X3,X4,X2) ) ).
cnf(i_0_145,axiom,
( X1 != X2
| ~ aElement0(X1)
| aElement0(X2) ) ).
cnf(i_0_154,plain,
aSet0(xJ),
inference(scs_inference,[],[i_0_116,i_0_112]) ).
cnf(i_0_156,plain,
sz10 = sdtpldt0(xa,xb),
inference(scs_inference,[],[i_0_116,i_0_115,i_0_112,i_0_124]) ).
cnf(i_0_157,plain,
xa != sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),
inference(scs_inference,[],[i_0_69,i_0_114,i_0_116,i_0_115,i_0_112,i_0_124,i_0_138]) ).
cnf(i_0_158,plain,
aElement0(xb),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99]) ).
cnf(i_0_160,plain,
aElement0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_120,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99,i_0_145]) ).
cnf(i_0_161,plain,
~ aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_117,i_0_119,i_0_120,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99,i_0_145,i_0_84]) ).
cnf(i_0_177,plain,
aSet0(xI),
inference(scs_inference,[],[i_0_117,i_0_112]) ).
cnf(i_0_179,plain,
sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))) = sdtpldt0(xw,smndt0(xx)),
inference(scs_inference,[],[i_0_76,i_0_117,i_0_112,i_0_124]) ).
cnf(i_0_180,plain,
aElement0(xa),
inference(scs_inference,[],[i_0_76,i_0_114,i_0_117,i_0_112,i_0_124,i_0_99]) ).
cnf(i_0_190,plain,
sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)) = xw,
inference(scs_inference,[],[i_0_87,i_0_124]) ).
cnf(i_0_163,plain,
aElementOf0(xb,sdtasasdt0(xJ,xJ)),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_117,i_0_119,i_0_120,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99,i_0_145,i_0_84,i_0_149]) ).
cnf(i_0_165,plain,
~ sdteqdtlpzmzozddtrp0(xb,sz10,xI),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_117,i_0_119,i_0_120,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99,i_0_145,i_0_84,i_0_149,i_0_67]) ).
cnf(i_0_168,plain,
~ sdteqdtlpzmzozddtrp0(xb,sdtpldt0(xa,xb),xI),
inference(scs_inference,[],[i_0_69,i_0_113,i_0_114,i_0_116,i_0_117,i_0_119,i_0_120,i_0_115,i_0_112,i_0_124,i_0_138,i_0_99,i_0_145,i_0_84,i_0_149,i_0_67,i_0_139,i_0_143]) ).
cnf(i_0_182,plain,
xa != sdtpldt0(xb,smndt0(sz10)),
inference(scs_inference,[],[i_0_161,i_0_76,i_0_114,i_0_117,i_0_112,i_0_124,i_0_99,i_0_138]) ).
cnf(i_0_183,plain,
aElementOf0(xa,sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_161,i_0_76,i_0_114,i_0_117,i_0_112,i_0_124,i_0_99,i_0_138,i_0_149]) ).
cnf(i_0_200,plain,
aElement0(xy),
inference(equality_inference,[],[196]) ).
cnf(i_0_220,plain,
aElement0(sz00),
inference(equality_inference,[],[216]) ).
cnf(i_0_225,plain,
aIdeal0(xJ),
inference(equality_inference,[],[221]) ).
cnf(i_0_226,plain,
aSet0(xJ),
inference(equality_inference,[],[222]) ).
cnf(i_0_237,plain,
aIdeal0(xI),
inference(equality_inference,[],[227]) ).
cnf(i_0_243,plain,
aElement0(xx),
inference(equality_inference,[],[239]) ).
cnf(i_0_3736,plain,
sdtpldt0(sz10,X1) = sdtpldt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_156,i_0_126]) ).
cnf(i_0_3737,plain,
sdtpldt0(X1,sz10) = sdtpldt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127]) ).
cnf(i_0_3738,plain,
sdtasdt0(sz10,X1) = sdtasdt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128]) ).
cnf(i_0_3739,plain,
sdtasdt0(X1,sz10) = sdtasdt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129]) ).
cnf(i_0_3740,plain,
smndt0(sz10) = smndt0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130]) ).
cnf(i_0_3741,plain,
sdtpldt1(sz10,X1) = sdtpldt1(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131]) ).
cnf(i_0_3742,plain,
sdtpldt1(X1,sz10) = sdtpldt1(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132]) ).
cnf(i_0_3743,plain,
sdtasasdt0(sz10,X1) = sdtasasdt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133]) ).
cnf(i_0_3744,plain,
sdtasasdt0(X1,sz10) = sdtasasdt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134]) ).
cnf(i_0_3745,plain,
esk5_3(sz10,X1,X2) = esk5_3(sdtpldt0(xa,xb),X1,X2),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135]) ).
cnf(i_0_3746,plain,
esk5_3(X1,sz10,X2) = esk5_3(X1,sdtpldt0(xa,xb),X2),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136]) ).
cnf(i_0_3747,plain,
esk5_3(X1,X2,sz10) = esk5_3(X1,X2,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137]) ).
cnf(i_0_3748,plain,
aElement0(smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111]) ).
cnf(i_0_3750,plain,
sdtasdt0(sdtpldt0(xa,xb),sz10) = sdtpldt0(xa,xb),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105]) ).
cnf(i_0_3752,plain,
sdtpldt0(sdtpldt0(xa,xb),sz00) = sdtpldt0(xa,xb),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106]) ).
cnf(i_0_3754,plain,
sdtpldt0(xa,xb) = sdtasdt0(sz10,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107]) ).
cnf(i_0_3756,plain,
sdtpldt0(xa,xb) = sdtpldt0(sz00,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108]) ).
cnf(i_0_3758,plain,
sdtasdt0(sdtpldt0(xa,xb),sz00) = sz00,
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109]) ).
cnf(i_0_3760,plain,
sz00 = sdtasdt0(sz00,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110]) ).
cnf(i_0_3762,plain,
sdtpldt0(sdtpldt0(xa,xb),smndt0(sdtpldt0(xa,xb))) = sz00,
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103]) ).
cnf(i_0_3764,plain,
sz00 = sdtpldt0(smndt0(sdtpldt0(xa,xb)),sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104]) ).
cnf(i_0_3766,plain,
sdtasdt0(smndt0(sz10),sdtpldt0(xa,xb)) = smndt0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101]) ).
cnf(i_0_3768,plain,
smndt0(sdtpldt0(xa,xb)) = sdtasdt0(sdtpldt0(xa,xb),smndt0(sz10)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102]) ).
cnf(i_0_3770,plain,
aElementOf0(sdtpldt0(xa,xb),sdtpldt1(xI,xJ)),
inference(scs_inference,[],[i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97]) ).
cnf(i_0_3772,plain,
sz00 != sz10,
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124]) ).
cnf(i_0_3773,plain,
aIdeal0(sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88]) ).
cnf(i_0_3775,plain,
aIdeal0(sdtpldt1(xI,xI)),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89]) ).
cnf(i_0_3777,plain,
aSet0(sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152]) ).
cnf(i_0_3779,plain,
aSet0(sdtpldt1(xI,xI)),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153]) ).
cnf(i_0_3781,plain,
aElement0(sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90]) ).
cnf(i_0_3783,plain,
aElement0(sdtpldt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91]) ).
cnf(i_0_3785,plain,
sdtpldt0(xa,xb) != sz00,
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125]) ).
cnf(i_0_3786,plain,
aElementOf0(sz10,sdtpldt1(xI,xJ)),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_177,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138]) ).
cnf(i_0_176,plain,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
inference(equality_inference,[],[167]) ).
cnf(i_0_189,plain,
~ aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI),
inference(equality_inference,[],[185]) ).
cnf(i_0_195,plain,
aSet0(xI),
inference(equality_inference,[],[191]) ).
cnf(i_0_210,plain,
aElement0(xa),
inference(equality_inference,[],[206]) ).
cnf(i_0_238,plain,
aElement0(xb),
inference(equality_inference,[],[228]) ).
cnf(i_0_3787,plain,
~ sdteqdtlpzmzozddtrp0(xb,sdtasdt0(sdtpldt0(xa,xb),sz10),xI),
inference(scs_inference,[],[i_0_122,i_0_160,i_0_156,i_0_117,i_0_168,i_0_177,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143]) ).
cnf(i_0_3796,plain,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_117,i_0_168,i_0_177,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150]) ).
cnf(i_0_3798,plain,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),sdtasasdt0(xJ,xI)),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151]) ).
cnf(i_0_3800,plain,
aElementOf0(sdtasdt0(sdtpldt0(xa,xb),xa),sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84]) ).
cnf(i_0_3802,plain,
aElementOf0(sdtpldt0(xa,xa),sdtasasdt0(xI,xI)),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84,i_0_83]) ).
cnf(i_0_3804,plain,
aElementOf0(esk4_4(xI,xJ,sdtpldt1(xI,xJ),sdtpldt0(xa,xb)),xJ),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84,i_0_83,i_0_147]) ).
cnf(i_0_3806,plain,
aElementOf0(esk3_4(xI,xJ,sdtpldt1(xI,xJ),sdtpldt0(xa,xb)),xI),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84,i_0_83,i_0_147,i_0_148]) ).
cnf(i_0_3810,plain,
sdtasdt0(sz10,sz10) != sz00,
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_120,i_0_117,i_0_168,i_0_177,i_0_154,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84,i_0_83,i_0_147,i_0_148,i_0_146,i_0_98]) ).
cnf(i_0_3812,plain,
aElementOf0(xa,sdtasasdt0(xI,sdtasasdt0(xI,xI))),
inference(scs_inference,[],[i_0_69,i_0_122,i_0_160,i_0_156,i_0_183,i_0_120,i_0_117,i_0_168,i_0_177,i_0_154,i_0_114,i_0_115,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125,i_0_138,i_0_143,i_0_79,i_0_80,i_0_72,i_0_73,i_0_150,i_0_151,i_0_84,i_0_83,i_0_147,i_0_148,i_0_146,i_0_98,i_0_149]) ).
cnf(i_0_3821,plain,
aElement0(smndt0(smndt0(sdtpldt0(xa,xb)))),
inference(scs_inference,[],[i_0_3748,i_0_111]) ).
cnf(i_0_3823,plain,
sdtasdt0(smndt0(sdtpldt0(xa,xb)),sz10) = smndt0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105]) ).
cnf(i_0_3825,plain,
sdtpldt0(smndt0(sdtpldt0(xa,xb)),sz00) = smndt0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106]) ).
cnf(i_0_3827,plain,
smndt0(sdtpldt0(xa,xb)) = sdtasdt0(sz10,smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107]) ).
cnf(i_0_3829,plain,
smndt0(sdtpldt0(xa,xb)) = sdtpldt0(sz00,smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108]) ).
cnf(i_0_3831,plain,
sdtasdt0(smndt0(sdtpldt0(xa,xb)),sz00) = sz00,
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109]) ).
cnf(i_0_3833,plain,
sz00 = sdtasdt0(sz00,smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110]) ).
cnf(i_0_3835,plain,
sdtpldt0(smndt0(sdtpldt0(xa,xb)),smndt0(smndt0(sdtpldt0(xa,xb)))) = sz00,
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103]) ).
cnf(i_0_3837,plain,
sz00 = sdtpldt0(smndt0(smndt0(sdtpldt0(xa,xb))),smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104]) ).
cnf(i_0_3839,plain,
sdtasdt0(smndt0(sz10),smndt0(sdtpldt0(xa,xb))) = smndt0(smndt0(sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101]) ).
cnf(i_0_3841,plain,
smndt0(smndt0(sdtpldt0(xa,xb))) = sdtasdt0(smndt0(sdtpldt0(xa,xb)),smndt0(sz10)),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102]) ).
cnf(i_0_3843,plain,
aElementOf0(smndt0(sdtpldt0(xa,xb)),sdtpldt1(xI,xJ)),
inference(scs_inference,[],[i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97]) ).
cnf(i_0_3845,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xa,xb),sz10),X1) = sdtpldt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126]) ).
cnf(i_0_3846,plain,
sdtpldt0(X1,sdtasdt0(sdtpldt0(xa,xb),sz10)) = sdtpldt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127]) ).
cnf(i_0_3847,plain,
sdtasdt0(sdtasdt0(sdtpldt0(xa,xb),sz10),X1) = sdtasdt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128]) ).
cnf(i_0_3848,plain,
sdtasdt0(X1,sdtasdt0(sdtpldt0(xa,xb),sz10)) = sdtasdt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129]) ).
cnf(i_0_3849,plain,
smndt0(sdtasdt0(sdtpldt0(xa,xb),sz10)) = smndt0(sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130]) ).
cnf(i_0_3850,plain,
sdtpldt1(sdtasdt0(sdtpldt0(xa,xb),sz10),X1) = sdtpldt1(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131]) ).
cnf(i_0_3851,plain,
sdtpldt1(X1,sdtasdt0(sdtpldt0(xa,xb),sz10)) = sdtpldt1(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132]) ).
cnf(i_0_3852,plain,
sdtasasdt0(sdtasdt0(sdtpldt0(xa,xb),sz10),X1) = sdtasasdt0(sdtpldt0(xa,xb),X1),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133]) ).
cnf(i_0_3853,plain,
sdtasasdt0(X1,sdtasdt0(sdtpldt0(xa,xb),sz10)) = sdtasasdt0(X1,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134]) ).
cnf(i_0_3854,plain,
esk5_3(sdtasdt0(sdtpldt0(xa,xb),sz10),X1,X2) = esk5_3(sdtpldt0(xa,xb),X1,X2),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135]) ).
cnf(i_0_3855,plain,
esk5_3(X1,sdtasdt0(sdtpldt0(xa,xb),sz10),X2) = esk5_3(X1,sdtpldt0(xa,xb),X2),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136]) ).
cnf(i_0_3856,plain,
esk5_3(X1,X2,sdtasdt0(sdtpldt0(xa,xb),sz10)) = esk5_3(X1,X2,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137]) ).
cnf(i_0_3857,plain,
sz00 != sdtpldt0(xa,xb),
inference(scs_inference,[],[i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124]) ).
cnf(i_0_3858,plain,
aIdeal0(sdtasasdt0(sdtasasdt0(xI,xI),sdtasasdt0(xI,xI))),
inference(scs_inference,[],[i_0_3773,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88]) ).
cnf(i_0_3860,plain,
aIdeal0(sdtpldt1(sdtasasdt0(xI,xI),sdtasasdt0(xI,xI))),
inference(scs_inference,[],[i_0_3773,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89]) ).
cnf(i_0_3862,plain,
aSet0(sdtasasdt0(sdtasasdt0(xI,xI),sdtasasdt0(xI,xI))),
inference(scs_inference,[],[i_0_3773,i_0_3777,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89,i_0_152]) ).
cnf(i_0_3864,plain,
aSet0(sdtpldt1(sdtasasdt0(xI,xI),sdtasasdt0(xI,xI))),
inference(scs_inference,[],[i_0_3773,i_0_3777,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153]) ).
cnf(i_0_3866,plain,
aElement0(sdtasdt0(smndt0(sdtpldt0(xa,xb)),smndt0(sdtpldt0(xa,xb)))),
inference(scs_inference,[],[i_0_3773,i_0_3777,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90]) ).
cnf(i_0_3868,plain,
aElement0(sdtpldt0(smndt0(sdtpldt0(xa,xb)),smndt0(sdtpldt0(xa,xb)))),
inference(scs_inference,[],[i_0_3773,i_0_3777,i_0_3785,i_0_3750,i_0_3748,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91]) ).
cnf(i_0_3870,plain,
sdtasdt0(sdtpldt0(xa,xb),sz10) = sdtasdt0(sz10,sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3773,i_0_3777,i_0_3785,i_0_3750,i_0_3748,i_0_3754,i_0_111,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_103,i_0_104,i_0_101,i_0_102,i_0_97,i_0_126,i_0_127,i_0_128,i_0_129,i_0_130,i_0_131,i_0_132,i_0_133,i_0_134,i_0_135,i_0_136,i_0_137,i_0_124,i_0_88,i_0_89,i_0_152,i_0_153,i_0_90,i_0_91,i_0_125]) ).
cnf(i_0_3907,plain,
aElement0(smndt0(sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)))),
inference(scs_inference,[],[i_0_3781,i_0_111]) ).
cnf(i_0_3909,plain,
sdtasdt0(sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)),sz10) = sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3781,i_0_111,i_0_105]) ).
cnf(i_0_3911,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)),sz00) = sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)),
inference(scs_inference,[],[i_0_3781,i_0_111,i_0_105,i_0_106]) ).
cnf(i_0_3913,plain,
sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb)) = sdtasdt0(sz10,sdtasdt0(sdtpldt0(xa,xb),sdtpldt0(xa,xb))),
inference(scs_inference,[],[i_0_3781,i_0_111,i_0_105,i_0_106,i_0_107]) ).
cnf(c_0_3872,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
i_0_95 ).
cnf(c_0_3873,plain,
aElement0(xb),
i_0_158 ).
cnf(c_0_3874,plain,
aElement0(smndt0(smndt0(sdtpldt0(xa,xb)))),
i_0_3821 ).
cnf(c_0_3875,plain,
sz10 = sdtpldt0(xa,xb),
i_0_156 ).
cnf(c_0_3876,plain,
aElement0(smndt0(sdtpldt0(xa,xb))),
i_0_3748 ).
cnf(c_0_3877,plain,
( sdtasdt0(X1,xb) = sdtasdt0(xb,X1)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3872,c_0_3873]) ).
cnf(c_0_3878,plain,
aElement0(smndt0(smndt0(sz10))),
inference(rw,[status(thm)],[c_0_3874,c_0_3875]) ).
cnf(c_0_3879,plain,
aElement0(smndt0(sz10)),
inference(rw,[status(thm)],[c_0_3876,c_0_3875]) ).
cnf(c_0_3880,hypothesis,
aElement0(xx),
i_0_119 ).
cnf(c_0_3881,plain,
( aElement0(sdtasdt0(X1,X2))
| ~ aElement0(X1)
| ~ aElement0(X2) ),
i_0_90 ).
cnf(c_0_3882,plain,
sdtasdt0(smndt0(smndt0(sz10)),xb) = sdtasdt0(xb,smndt0(smndt0(sz10))),
inference(spm,[status(thm)],[c_0_3877,c_0_3878]) ).
cnf(c_0_3883,plain,
smndt0(smndt0(sdtpldt0(xa,xb))) = sdtasdt0(smndt0(sdtpldt0(xa,xb)),smndt0(sz10)),
i_0_3841 ).
cnf(c_0_3884,plain,
( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
| ~ aElement0(X1) ),
i_0_101 ).
cnf(c_0_3885,plain,
sdtasdt0(smndt0(sz10),xb) = sdtasdt0(xb,smndt0(sz10)),
inference(spm,[status(thm)],[c_0_3877,c_0_3879]) ).
cnf(c_0_3886,hypothesis,
( sdtasdt0(X1,xx) = sdtasdt0(xx,X1)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3872,c_0_3880]) ).
cnf(c_0_3887,plain,
aElement0(sdtasdt0(xb,smndt0(smndt0(sz10)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3881,c_0_3882]),c_0_3873]),c_0_3878])]) ).
cnf(c_0_3888,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
i_0_79 ).
cnf(c_0_3889,plain,
sdtasdt0(smndt0(sz10),smndt0(sz10)) = smndt0(smndt0(sz10)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3883,c_0_3875]),c_0_3875]) ).
cnf(c_0_3890,plain,
sdtasdt0(xb,smndt0(sz10)) = smndt0(xb),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3884,c_0_3885]),c_0_3873])]) ).
cnf(c_0_3891,plain,
sdtasdt0(smndt0(sz10),xx) = sdtasdt0(xx,smndt0(sz10)),
inference(spm,[status(thm)],[c_0_3886,c_0_3879]) ).
cnf(c_0_3892,hypothesis,
sdtasdt0(sdtasdt0(xb,smndt0(smndt0(sz10))),xx) = sdtasdt0(xx,sdtasdt0(xb,smndt0(smndt0(sz10)))),
inference(spm,[status(thm)],[c_0_3886,c_0_3887]) ).
cnf(c_0_3893,plain,
sdtasdt0(smndt0(smndt0(sz10)),xx) = sdtasdt0(xx,smndt0(smndt0(sz10))),
inference(spm,[status(thm)],[c_0_3886,c_0_3878]) ).
cnf(c_0_3894,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(smndt0(sz10),X1)) = sdtasdt0(smndt0(smndt0(sz10)),X1)
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3888,c_0_3889]),c_0_3879])]) ).
cnf(c_0_3895,plain,
sdtasdt0(smndt0(sz10),xb) = smndt0(xb),
inference(rw,[status(thm)],[c_0_3885,c_0_3890]) ).
cnf(c_0_3896,plain,
sdtasdt0(xx,smndt0(sz10)) = smndt0(xx),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3884,c_0_3891]),c_0_3880])]) ).
cnf(c_0_3897,plain,
sdtasdt0(xx,sdtasdt0(xb,smndt0(smndt0(sz10)))) = sdtasdt0(xb,sdtasdt0(xx,smndt0(smndt0(sz10)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3888,c_0_3892]),c_0_3893]),c_0_3880]),c_0_3878]),c_0_3873])]) ).
cnf(c_0_3898,plain,
sdtasdt0(smndt0(sz10),smndt0(xb)) = sdtasdt0(xb,smndt0(smndt0(sz10))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3894,c_0_3895]),c_0_3882]),c_0_3873])]) ).
cnf(c_0_3899,plain,
aElement0(smndt0(xb)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3881,c_0_3890]),c_0_3879]),c_0_3873])]) ).
cnf(c_0_3900,plain,
sdtasdt0(smndt0(sz10),xx) = smndt0(xx),
inference(rw,[status(thm)],[c_0_3891,c_0_3896]) ).
cnf(c_0_3901,hypothesis,
sdtasdt0(sdtasdt0(xb,smndt0(smndt0(sz10))),xx) = sdtasdt0(xb,sdtasdt0(xx,smndt0(smndt0(sz10)))),
inference(rw,[status(thm)],[c_0_3892,c_0_3897]) ).
cnf(c_0_3902,plain,
sdtasdt0(xb,smndt0(smndt0(sz10))) = smndt0(smndt0(xb)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3884,c_0_3898]),c_0_3899])]) ).
cnf(c_0_3903,plain,
aElement0(sdtasdt0(xx,smndt0(smndt0(sz10)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3881,c_0_3893]),c_0_3880]),c_0_3878])]) ).
cnf(c_0_3904,plain,
sdtasdt0(smndt0(sz10),smndt0(xx)) = sdtasdt0(xx,smndt0(smndt0(sz10))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3894,c_0_3900]),c_0_3893]),c_0_3880])]) ).
cnf(c_0_3905,plain,
aElement0(smndt0(xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3881,c_0_3896]),c_0_3879]),c_0_3880])]) ).
cnf(c_0_3906,hypothesis,
sdtasdt0(xb,sdtasdt0(xx,smndt0(smndt0(sz10)))) = sdtasdt0(smndt0(smndt0(xb)),xx),
inference(rw,[status(thm)],[c_0_3901,c_0_3902]) ).
cnf(c_0_3907,plain,
sdtasdt0(sdtasdt0(xx,smndt0(smndt0(sz10))),xb) = sdtasdt0(xb,sdtasdt0(xx,smndt0(smndt0(sz10)))),
inference(spm,[status(thm)],[c_0_3877,c_0_3903]) ).
cnf(c_0_3908,plain,
sdtasdt0(xx,smndt0(smndt0(sz10))) = smndt0(smndt0(xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3884,c_0_3904]),c_0_3905])]) ).
cnf(c_0_3909,plain,
sdtasdt0(smndt0(smndt0(xb)),xx) = sdtasdt0(xx,smndt0(smndt0(xb))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3897,c_0_3902]),c_0_3906]) ).
cnf(c_0_3910,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
i_0_96 ).
cnf(c_0_3911,plain,
sdtasdt0(smndt0(smndt0(xx)),xb) = sdtasdt0(xx,smndt0(smndt0(xb))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3907,c_0_3906]),c_0_3908]),c_0_3909]) ).
cnf(c_0_3912,hypothesis,
sdtasdt0(xx,smndt0(smndt0(xb))) = sdtasdt0(xb,smndt0(smndt0(xx))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3906,c_0_3909]),c_0_3908]) ).
cnf(c_0_3913,plain,
( sdtpldt0(sdtpldt0(X1,X2),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
i_0_80 ).
cnf(c_0_3914,plain,
sdtpldt0(sdtpldt0(xa,xb),smndt0(sdtpldt0(xa,xb))) = sz00,
i_0_3762 ).
cnf(c_0_3915,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aElement0(X1) ),
i_0_108 ).
cnf(c_0_3916,plain,
sdtpldt0(smndt0(sdtpldt0(xa,xb)),smndt0(smndt0(sdtpldt0(xa,xb)))) = sz00,
i_0_3835 ).
cnf(c_0_3917,plain,
sdtpldt0(sdtpldt0(xa,xb),sz00) = sdtpldt0(xa,xb),
i_0_3752 ).
cnf(c_0_3918,plain,
( sdtpldt0(X1,xb) = sdtpldt0(xb,X1)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3910,c_0_3873]) ).
cnf(c_0_3919,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(X1,X2)) = sdtasdt0(smndt0(X1),X2)
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3888,c_0_3884]),c_0_3879])]) ).
cnf(c_0_3920,plain,
sdtasdt0(smndt0(xx),xb) = sdtasdt0(xb,smndt0(xx)),
inference(spm,[status(thm)],[c_0_3877,c_0_3905]) ).
cnf(c_0_3921,plain,
sdtasdt0(smndt0(smndt0(xx)),xb) = sdtasdt0(xb,smndt0(smndt0(xx))),
inference(rw,[status(thm)],[c_0_3911,c_0_3912]) ).
cnf(c_0_3922,plain,
( sdtpldt0(sdtpldt0(X1,X2),smndt0(smndt0(sz10))) = sdtpldt0(X1,sdtpldt0(X2,smndt0(smndt0(sz10))))
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3913,c_0_3878]) ).
cnf(c_0_3923,plain,
sdtpldt0(sz10,smndt0(sz10)) = sz00,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3914,c_0_3875]),c_0_3875]) ).
cnf(c_0_3924,plain,
sdtpldt0(sz00,smndt0(smndt0(sz10))) = smndt0(smndt0(sz10)),
inference(spm,[status(thm)],[c_0_3915,c_0_3878]) ).
cnf(c_0_3925,plain,
sdtpldt0(smndt0(sz10),smndt0(smndt0(sz10))) = sz00,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3916,c_0_3875]),c_0_3875]) ).
cnf(c_0_3926,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3917,c_0_3875]),c_0_3875]) ).
cnf(c_0_3927,plain,
aElement0(sz10),
i_0_120 ).
cnf(c_0_3928,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aElement0(X1) ),
i_0_107 ).
cnf(c_0_3929,plain,
( aElement0(sdtpldt0(X1,X2))
| ~ aElement0(X1)
| ~ aElement0(X2) ),
i_0_91 ).
cnf(c_0_3930,plain,
sdtpldt0(smndt0(sz10),xb) = sdtpldt0(xb,smndt0(sz10)),
inference(spm,[status(thm)],[c_0_3918,c_0_3879]) ).
cnf(c_0_3931,plain,
( aElement0(smndt0(X1))
| ~ aElement0(X1) ),
i_0_111 ).
cnf(c_0_3932,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xb,smndt0(xx))) = sdtasdt0(xb,smndt0(smndt0(xx))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3919,c_0_3920]),c_0_3921]),c_0_3873]),c_0_3905])]) ).
cnf(c_0_3933,plain,
sdtasdt0(smndt0(smndt0(sz10)),xx) = smndt0(smndt0(xx)),
inference(rw,[status(thm)],[c_0_3893,c_0_3908]) ).
cnf(c_0_3934,plain,
smndt0(smndt0(sz10)) = sz10,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3922,c_0_3923]),c_0_3924]),c_0_3925]),c_0_3926]),c_0_3879]),c_0_3927])]) ).
cnf(c_0_3935,hypothesis,
sdtasdt0(sz10,xx) = xx,
inference(spm,[status(thm)],[c_0_3928,c_0_3880]) ).
cnf(c_0_3936,plain,
aElement0(sdtpldt0(xb,smndt0(sz10))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3929,c_0_3930]),c_0_3873]),c_0_3879])]) ).
cnf(c_0_3937,plain,
( sdtasdt0(sdtpldt0(X1,X2),X3) = sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))
| ~ aElement0(X3)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
i_0_72 ).
cnf(c_0_3938,plain,
( sdtasdt0(sz10,smndt0(X1)) = smndt0(X1)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3928,c_0_3931]) ).
cnf(c_0_3939,plain,
sdtasdt0(smndt0(xb),smndt0(xx)) = sdtasdt0(xb,smndt0(smndt0(xx))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3919,c_0_3932]),c_0_3905]),c_0_3873])]) ).
cnf(c_0_3940,plain,
smndt0(smndt0(xx)) = xx,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3933,c_0_3934]),c_0_3935]) ).
cnf(c_0_3941,plain,
( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
i_0_73 ).
cnf(c_0_3942,hypothesis,
sdtasdt0(xx,xb) = sdtasdt0(xb,xx),
inference(spm,[status(thm)],[c_0_3877,c_0_3880]) ).
cnf(c_0_3943,hypothesis,
sdtasdt0(sdtpldt0(xb,smndt0(sz10)),xx) = sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),
inference(spm,[status(thm)],[c_0_3886,c_0_3936]) ).
cnf(c_0_3944,plain,
( sdtpldt0(sdtasdt0(X1,X2),smndt0(X2)) = sdtasdt0(sdtpldt0(X1,smndt0(sz10)),X2)
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3937,c_0_3884]),c_0_3879])]) ).
cnf(c_0_3945,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X2,smndt0(X1))) = sdtasdt0(sdtpldt0(sz10,X2),smndt0(X1))
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3937,c_0_3938]),c_0_3927])]),c_0_3931]) ).
cnf(c_0_3946,plain,
sdtasdt0(smndt0(xb),smndt0(xx)) = sdtasdt0(xb,xx),
inference(rw,[status(thm)],[c_0_3939,c_0_3940]) ).
cnf(c_0_3947,plain,
( sdtpldt0(sdtasdt0(xx,X1),sdtasdt0(xb,xx)) = sdtasdt0(xx,sdtpldt0(X1,xb))
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3941,c_0_3942]),c_0_3873]),c_0_3880])]) ).
cnf(c_0_3948,plain,
( smndt0(X1) = sdtasdt0(X1,smndt0(sz10))
| ~ aElement0(X1) ),
i_0_102 ).
cnf(c_0_3949,hypothesis,
sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))) = sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3943,c_0_3944]),c_0_3880]),c_0_3873])]) ).
cnf(c_0_3950,plain,
( sz00 = sdtpldt0(smndt0(X1),X1)
| ~ aElement0(X1) ),
i_0_104 ).
cnf(c_0_3951,plain,
sdtpldt0(smndt0(xb),xb) = sdtpldt0(xb,smndt0(xb)),
inference(spm,[status(thm)],[c_0_3918,c_0_3899]) ).
cnf(c_0_3952,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aElement0(X1) ),
i_0_106 ).
cnf(c_0_3953,plain,
aElement0(xa),
i_0_180 ).
cnf(c_0_3954,plain,
sdtasdt0(sdtpldt0(sz10,smndt0(xb)),smndt0(xx)) = sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3945,c_0_3946]),c_0_3899]),c_0_3880])]) ).
cnf(c_0_3955,plain,
sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)) = sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3947,c_0_3948]),c_0_3930]),c_0_3949]),c_0_3879]),c_0_3880])]) ).
cnf(c_0_3956,plain,
( sdtpldt0(sdtpldt0(X1,X2),smndt0(xb)) = sdtpldt0(X1,sdtpldt0(X2,smndt0(xb)))
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3913,c_0_3899]) ).
cnf(c_0_3957,plain,
sdtpldt0(xb,smndt0(xb)) = sz00,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3950,c_0_3951]),c_0_3873])]) ).
cnf(c_0_3958,plain,
sdtpldt0(xa,sz00) = xa,
inference(spm,[status(thm)],[c_0_3952,c_0_3953]) ).
cnf(c_0_3959,plain,
( aElementOf0(sdtasdt0(X1,X2),X3)
| ~ aElement0(X1)
| ~ aElementOf0(X2,X3)
| ~ aIdeal0(X3) ),
i_0_84 ).
cnf(c_0_3960,hypothesis,
aElementOf0(xa,xI),
i_0_114 ).
cnf(c_0_3961,hypothesis,
aIdeal0(xI),
i_0_117 ).
cnf(c_0_3962,plain,
( sdtasdt0(X1,xa) = sdtasdt0(xa,X1)
| ~ aElement0(X1) ),
inference(spm,[status(thm)],[c_0_3872,c_0_3953]) ).
cnf(c_0_3963,negated_conjecture,
~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
i_0_69 ).
cnf(c_0_3964,plain,
( sdtpldt0(sdtasdt0(X1,X2),smndt0(X1)) = sdtasdt0(X1,sdtpldt0(X2,smndt0(sz10)))
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3941,c_0_3948]),c_0_3879])]) ).
cnf(c_0_3965,plain,
sdtasdt0(sdtpldt0(sz10,smndt0(xb)),smndt0(xx)) = sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)),
inference(rw,[status(thm)],[c_0_3954,c_0_3955]) ).
cnf(c_0_3966,plain,
sdtpldt0(sz10,smndt0(xb)) = xa,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3956,c_0_3875]),c_0_3957]),c_0_3958]),c_0_3873]),c_0_3953])]) ).
cnf(c_0_3967,hypothesis,
( aElementOf0(sdtasdt0(X1,xa),xI)
| ~ aElement0(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3959,c_0_3960]),c_0_3961])]) ).
cnf(c_0_3968,plain,
sdtasdt0(smndt0(xx),xa) = sdtasdt0(xa,smndt0(xx)),
inference(spm,[status(thm)],[c_0_3962,c_0_3905]) ).
cnf(c_0_3969,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)),xI),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3963,c_0_3964]),c_0_3942]),c_0_3873]),c_0_3880])]) ).
cnf(c_0_3970,plain,
sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)) = sdtasdt0(xa,smndt0(xx)),
inference(rw,[status(thm)],[c_0_3965,c_0_3966]) ).
cnf(c_0_3971,hypothesis,
aElementOf0(sdtasdt0(xa,smndt0(xx)),xI),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3967,c_0_3968]),c_0_3905])]) ).
cnf(c_0_3972,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3969,c_0_3970]),c_0_3971])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : RNG097+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.06 % 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.06/0.24 % Computer : n012.cluster.edu
% 0.06/0.24 % Model : x86_64 x86_64
% 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.24 % Memory : 8042.1875MB
% 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.24 % CPULimit : 300
% 0.06/0.24 % WCLimit : 300
% 0.06/0.24 % DateTime : Tue May 5 01:52:01 EDT 2026
% 0.06/0.24 % CPUTime :
% 0.06/0.25 % start to proof: theBenchmark
% 259.18/154.20 % Version : CSE_E---1.7
% 259.18/154.20 % Problem : theBenchmark.p
% 259.18/154.20 % SZS status Theorem for theBenchmark.p
% 259.18/154.20 % SZS output start CNFRefutation
% See solution above
% 265.98/161.08 % Total time : 150.331s
%------------------------------------------------------------------------------