%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM523+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:25:49 PM UTC 2026
% Result : Theorem 4.30s 1.27s
% Output : CNFRefutation 4.30s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f223ERROR: Could not build tree for root c_7916ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC) ).
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f6,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(f8,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 = sdtpldt0(sz00,X0)
& sdtpldt0(X0,sz00) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_AddZero) ).
fof(f9,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 = sdtasdt0(sz10,X0)
& sdtasdt0(X0,sz10) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sz00 = sdtasdt0(sz00,X0)
& sdtasdt0(X0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulZero) ).
fof(f13,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAMDistr) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtpldt0(X1,X0) = sdtpldt0(X2,X0)
| sdtpldt0(X0,X1) = sdtpldt0(X0,X2) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddCanc) ).
fof(f15,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 != sz00
=> ! [X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1) )
=> ( ( sdtasdt0(X1,X0) = sdtasdt0(X2,X0)
| sdtasdt0(X0,X1) = sdtasdt0(X0,X2) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulCanc) ).
fof(f16,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtpldt0(X0,X1) = sz00
=> ( X1 = sz00
& X0 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroAdd) ).
fof(f17,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtasdt0(X0,X1) = sz00
=> ( X1 = sz00
| X0 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroMul) ).
fof(f18,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefLE) ).
fof(f19,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtlseqdt0(X0,X1)
=> ! [X2] :
( X2 = sdtmndt0(X1,X0)
<=> ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefDiff) ).
fof(f21,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X1,X0)
& sdtlseqdt0(X0,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEAsym) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X0,X1) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETran) ).
fof(f23,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X1,X0)
& X1 != X0 )
| sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETotal) ).
fof(f24,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X0,X1)
& X0 != X1 )
=> ! [X2] :
( aNaturalNumber0(X2)
=> ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X2,X0) != sdtpldt0(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonAdd) ).
fof(f25,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X1,X2)
& X1 != X2
& X0 != sz00 )
=> ( sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X0,X1) != sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul) ).
fof(f26,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( ( sdtlseqdt0(sz10,X0)
& sz10 != X0 )
| X0 = sz10
| X0 = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLENTr) ).
fof(f27,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( X0 != sz00
=> sdtlseqdt0(X1,sdtasdt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul2) ).
fof(f29,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X0,X1)
& X0 != X1 )
=> iLess0(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIH_03) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefDiv) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X0,X1)
& X0 != sz00 )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefQuot) ).
fof(f32,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X1,X2)
& doDivides0(X0,X1) )
=> doDivides0(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivTrans) ).
fof(f33,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X0,X2)
& doDivides0(X0,X1) )
=> doDivides0(X0,sdtpldt0(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivSum) ).
fof(f34,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X0,sdtpldt0(X1,X2))
& doDivides0(X0,X1) )
=> doDivides0(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivMin) ).
fof(f35,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( X1 != sz00
& doDivides0(X0,X1) )
=> sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivLE) ).
fof(f36,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X0,X1)
& X0 != sz00 )
=> ! [X2] :
( aNaturalNumber0(X2)
=> sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivAsso) ).
fof(f37,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( isPrime0(X0)
<=> ( ! [X1] :
( ( doDivides0(X1,X0)
& aNaturalNumber0(X1) )
=> ( X1 = X0
| X1 = sz10 ) )
& X0 != sz10
& X0 != sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefPrime) ).
fof(f38,axiom,
! [X0] :
( ( X0 != sz10
& X0 != sz00
& aNaturalNumber0(X0) )
=> ? [X1] :
( isPrime0(X1)
& doDivides0(X1,X0)
& aNaturalNumber0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPrimDiv) ).
fof(f39,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X2,sdtasdt0(X0,X1))
& isPrime0(X2) )
=> ( doDivides0(X2,X1)
| doDivides0(X2,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPDP) ).
fof(f40,axiom,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2987) ).
fof(f41,axiom,
! [X0,X1,X2] :
( ( X2 != sz00
& X1 != sz00
& X0 != sz00
& aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtasdt0(X2,sdtasdt0(X1,X1)) = sdtasdt0(X0,X0)
=> ( iLess0(X0,xn)
=> ~ isPrime0(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2963) ).
fof(f42,axiom,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3014) ).
fof(f43,axiom,
isPrime0(xp),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3025) ).
fof(f44,conjecture,
( doDivides0(xp,xn)
& doDivides0(xp,sdtasdt0(xn,xn)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f45,negated_conjecture,
~ ( doDivides0(xp,xn)
& doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f48,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f49,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(flattening,[],[f48]) ).
fof(f50,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(ennf_transformation,[],[f5]) ).
fof(f51,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(flattening,[],[f50]) ).
fof(f52,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f53,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
inference(ennf_transformation,[],[f7]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( X0 = sdtpldt0(sz00,X0)
& sdtpldt0(X0,sz00) = X0 ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f57,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f58,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(flattening,[],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(ennf_transformation,[],[f10]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(flattening,[],[f59]) ).
fof(f61,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( X0 = sdtasdt0(sz10,X0)
& sdtasdt0(X0,sz10) = X0 ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f62,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( sz00 = sdtasdt0(sz00,X0)
& sdtasdt0(X0,sz00) = sz00 ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ) ),
inference(flattening,[],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
& sdtpldt0(X0,X1) != sdtpldt0(X0,X2) )
| X1 = X2 ),
inference(ennf_transformation,[],[f14]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
& sdtpldt0(X0,X1) != sdtpldt0(X0,X2) )
| X1 = X2 ),
inference(flattening,[],[f65]) ).
fof(f67,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ! [X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ( sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtasdt0(X0,X1) != sdtasdt0(X0,X2) )
| X1 = X2 ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f68,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ! [X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ( sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtasdt0(X0,X1) != sdtasdt0(X0,X2) )
| X1 = X2 ) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtpldt0(X0,X1)
| ( X1 = sz00
& X0 = sz00 ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f70,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtpldt0(X0,X1)
| ( X1 = sz00
& X0 = sz00 ) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtasdt0(X0,X1)
| X1 = sz00
| X0 = sz00 ),
inference(ennf_transformation,[],[f17]) ).
fof(f72,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtasdt0(X0,X1)
| X1 = sz00
| X0 = sz00 ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f74,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| ! [X2] :
( X2 = sdtmndt0(X1,X0)
<=> ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f76,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| ! [X2] :
( X2 = sdtmndt0(X1,X0)
<=> ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ),
inference(flattening,[],[f75]) ).
fof(f78,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f21]) ).
fof(f79,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(X1,X0)
& X1 != X0 )
| sdtlseqdt0(X0,X1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f83,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(X1,X0)
& X1 != X0 )
| sdtlseqdt0(X0,X1) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ! [X2] :
( ~ aNaturalNumber0(X2)
| ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X2,X0) != sdtpldt0(X2,X1) ) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f85,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ! [X2] :
( ~ aNaturalNumber0(X2)
| ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X2,X0) != sdtpldt0(X2,X1) ) ) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| ( sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X0,X1) != sdtasdt0(X0,X2) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| ( sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X0,X1) != sdtasdt0(X0,X2) ) ),
inference(flattening,[],[f86]) ).
fof(f88,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(sz10,X0)
& sz10 != X0 )
| X0 = sz10
| X0 = sz00 ),
inference(ennf_transformation,[],[f26]) ).
fof(f89,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( sdtlseqdt0(sz10,X0)
& sz10 != X0 )
| X0 = sz10
| X0 = sz00 ),
inference(flattening,[],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sdtlseqdt0(X1,sdtasdt0(X1,X0)) ),
inference(ennf_transformation,[],[f27]) ).
fof(f91,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sdtlseqdt0(X1,sdtasdt0(X1,X0)) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| iLess0(X0,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f93,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| iLess0(X0,X1) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( doDivides0(X0,X1)
<=> ? [X2] :
( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f95,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( doDivides0(X0,X1)
<=> ? [X2] :
( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ),
inference(ennf_transformation,[],[f31]) ).
fof(f97,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) ) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,sdtpldt0(X1,X2)) ),
inference(ennf_transformation,[],[f33]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,sdtpldt0(X1,X2)) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(ennf_transformation,[],[f34]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(flattening,[],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X1
| ~ doDivides0(X0,X1)
| sdtlseqdt0(X0,X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f105,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X1
| ~ doDivides0(X0,X1)
| sdtlseqdt0(X0,X1) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f107,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) ) ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( isPrime0(X0)
<=> ( ! [X1] :
( ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| X1 = X0
| X1 = sz10 )
& X0 != sz10
& X0 != sz00 ) ) ),
inference(ennf_transformation,[],[f37]) ).
fof(f109,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( isPrime0(X0)
<=> ( ! [X1] :
( ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| X1 = X0
| X1 = sz10 )
& X0 != sz10
& X0 != sz00 ) ) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ? [X1] :
( isPrime0(X1)
& doDivides0(X1,X0)
& aNaturalNumber0(X1) ) ),
inference(ennf_transformation,[],[f38]) ).
fof(f111,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ? [X1] :
( isPrime0(X1)
& doDivides0(X1,X0)
& aNaturalNumber0(X1) ) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X2,sdtasdt0(X0,X1))
| ~ isPrime0(X2)
| doDivides0(X2,X1)
| doDivides0(X2,X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f113,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X2,sdtasdt0(X0,X1))
| ~ isPrime0(X2)
| doDivides0(X2,X1)
| doDivides0(X2,X0) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0,X1,X2] :
( sz00 = X2
| sz00 = X1
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| ~ iLess0(X0,xn)
| ~ isPrime0(X2) ),
inference(ennf_transformation,[],[f41]) ).
fof(f115,plain,
! [X0,X1,X2] :
( sz00 = X2
| sz00 = X1
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| ~ iLess0(X0,xn)
| ~ isPrime0(X2) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
( ~ doDivides0(xp,xn)
| ~ doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(ennf_transformation,[],[f45]) ).
fof(f117,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ sdtlseqdt0(X0,X1)
| ? [X2] :
( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) )
& ( ! [X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| sdtlseqdt0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f118,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ sdtlseqdt0(X0,X1)
| ? [X3] :
( sdtpldt0(X0,X3) = X1
& aNaturalNumber0(X3) ) )
& ( ! [X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| sdtlseqdt0(X0,X1) ) ) ),
inference(rectify,[],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ sdtlseqdt0(X0,X1)
| ( sdtpldt0(X0,sK0(X0,X1)) = X1
& aNaturalNumber0(sK0(X0,X1)) ) )
& ( ! [X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| sdtlseqdt0(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1))],[f118]) ).
fof(f120,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| ! [X2] :
( ( sdtmndt0(X1,X0) != X2
| ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) )
& ( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtmndt0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f76]) ).
fof(f121,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| ! [X2] :
( ( sdtmndt0(X1,X0) != X2
| ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) )
& ( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtmndt0(X1,X0) ) ) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ doDivides0(X0,X1)
| ? [X2] :
( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) )
& ( ! [X2] :
( sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| doDivides0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f123,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ doDivides0(X0,X1)
| ? [X3] :
( sdtasdt0(X0,X3) = X1
& aNaturalNumber0(X3) ) )
& ( ! [X2] :
( sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| doDivides0(X0,X1) ) ) ),
inference(rectify,[],[f122]) ).
fof(f124,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( ( ~ doDivides0(X0,X1)
| ( sdtasdt0(X0,sK1(X0,X1)) = X1
& aNaturalNumber0(sK1(X0,X1)) ) )
& ( ! [X2] :
( sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2) )
| doDivides0(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1))],[f123]) ).
fof(f125,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( ( sdtsldt0(X1,X0) != X2
| ( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) )
& ( sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtsldt0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f126,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ! [X2] :
( ( sdtsldt0(X1,X0) != X2
| ( X1 = sdtasdt0(X0,X2)
& aNaturalNumber0(X2) ) )
& ( sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtsldt0(X1,X0) ) ) ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ( ~ isPrime0(X0)
| ( ! [X1] :
( ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| X1 = X0
| X1 = sz10 )
& X0 != sz10
& X0 != sz00 ) )
& ( ? [X1] :
( doDivides0(X1,X0)
& aNaturalNumber0(X1)
& X0 != X1
& sz10 != X1 )
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ) ) ),
inference(nnf_transformation,[],[f109]) ).
fof(f128,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ( ~ isPrime0(X0)
| ( ! [X1] :
( ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| X1 = X0
| X1 = sz10 )
& X0 != sz10
& X0 != sz00 ) )
& ( ? [X1] :
( doDivides0(X1,X0)
& aNaturalNumber0(X1)
& X0 != X1
& sz10 != X1 )
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ) ) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ( ~ isPrime0(X0)
| ( ! [X2] :
( ~ doDivides0(X2,X0)
| ~ aNaturalNumber0(X2)
| X0 = X2
| sz10 = X2 )
& X0 != sz10
& X0 != sz00 ) )
& ( ? [X1] :
( doDivides0(X1,X0)
& aNaturalNumber0(X1)
& X0 != X1
& sz10 != X1 )
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ) ) ),
inference(rectify,[],[f128]) ).
fof(f130,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ( ~ isPrime0(X0)
| ( ! [X2] :
( ~ doDivides0(X2,X0)
| ~ aNaturalNumber0(X2)
| X0 = X2
| sz10 = X2 )
& X0 != sz10
& X0 != sz00 ) )
& ( ( doDivides0(sK2(X0),X0)
& aNaturalNumber0(sK2(X0))
& sK2(X0) != X0
& sz10 != sK2(X0) )
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X1,sK2(X0))],[f129]) ).
fof(f131,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ( isPrime0(sK3(X0))
& doDivides0(sK3(X0),X0)
& aNaturalNumber0(sK3(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X1,sK3(X0))],[f111]) ).
fof(f132,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f133,plain,
sz00 != sz10,
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f136,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f137,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
inference(cnf_transformation,[],[f55]) ).
fof(f139,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f56]) ).
fof(f140,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(cnf_transformation,[],[f56]) ).
fof(f141,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f58]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(cnf_transformation,[],[f60]) ).
fof(f143,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(sz10,X0) = X0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f144,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f145,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f146,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f62]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ),
inference(cnf_transformation,[],[f64]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f64]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f66]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f66]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f68]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f68]) ).
fof(f153,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtpldt0(X0,X1)
| sz00 = X1 ),
inference(cnf_transformation,[],[f70]) ).
fof(f154,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtpldt0(X0,X1)
| sz00 = X0 ),
inference(cnf_transformation,[],[f70]) ).
fof(f155,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0 ),
inference(cnf_transformation,[],[f72]) ).
fof(f156,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| sdtpldt0(X0,sK0(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f119]) ).
fof(f157,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| aNaturalNumber0(sK0(X0,X1)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f158,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f159,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| sdtmndt0(X1,X0) != X2
| sdtpldt0(X0,X2) = X1 ),
inference(cnf_transformation,[],[f121]) ).
fof(f160,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| sdtmndt0(X1,X0) != X2
| aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f121]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtmndt0(X1,X0) = X2 ),
inference(cnf_transformation,[],[f121]) ).
fof(f163,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f79]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(cnf_transformation,[],[f81]) ).
fof(f165,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f167,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f169,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f171,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f173,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f175,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz10,X0)
| sz10 = X0
| sz00 = X0 ),
inference(cnf_transformation,[],[f89]) ).
fof(f177,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sdtlseqdt0(X1,sdtasdt0(X1,X0)) ),
inference(cnf_transformation,[],[f91]) ).
fof(f178,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| iLess0(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f179,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sdtasdt0(X0,sK1(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f124]) ).
fof(f180,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| aNaturalNumber0(sK1(X0,X1)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f181,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f182,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtsldt0(X1,X0) != X2
| sdtasdt0(X0,X2) = X1 ),
inference(cnf_transformation,[],[f126]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtsldt0(X1,X0) != X2
| aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f126]) ).
fof(f184,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtsldt0(X1,X0) = X2 ),
inference(cnf_transformation,[],[f126]) ).
fof(f185,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f186,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,sdtpldt0(X1,X2)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f187,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f188,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X1
| ~ doDivides0(X0,X1)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f189,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f190,plain,
! [X2,X0] :
( ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| ~ doDivides0(X2,X0)
| ~ aNaturalNumber0(X2)
| X0 = X2
| sz10 = X2 ),
inference(cnf_transformation,[],[f130]) ).
fof(f191,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz10 != X0 ),
inference(cnf_transformation,[],[f130]) ).
fof(f192,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz00 != X0 ),
inference(cnf_transformation,[],[f130]) ).
fof(f193,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| doDivides0(sK2(X0),X0)
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f194,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| aNaturalNumber0(sK2(X0))
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f195,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sK2(X0) != X0
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f196,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz10 != sK2(X0)
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f197,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| isPrime0(sK3(X0)) ),
inference(cnf_transformation,[],[f131]) ).
fof(f198,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| doDivides0(sK3(X0),X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f199,plain,
! [X0] :
( sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sK3(X0)) ),
inference(cnf_transformation,[],[f131]) ).
fof(f200,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X2,sdtasdt0(X0,X1))
| ~ isPrime0(X2)
| doDivides0(X2,X1)
| doDivides0(X2,X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f201,plain,
sz00 != xp,
inference(cnf_transformation,[],[f40]) ).
fof(f202,plain,
sz00 != xm,
inference(cnf_transformation,[],[f40]) ).
fof(f203,plain,
sz00 != xn,
inference(cnf_transformation,[],[f40]) ).
fof(f204,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f40]) ).
fof(f205,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f40]) ).
fof(f206,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f40]) ).
fof(f207,plain,
! [X2,X0,X1] :
( sz00 = X2
| sz00 = X1
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| ~ iLess0(X0,xn)
| ~ isPrime0(X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f208,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[],[f42]) ).
fof(f209,plain,
isPrime0(xp),
inference(cnf_transformation,[],[f43]) ).
fof(f210,plain,
( ~ doDivides0(xp,xn)
| ~ doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(cnf_transformation,[],[f116]) ).
fof(f211,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(equality_resolution,[],[f158]) ).
fof(f212,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X2)
| sdtmndt0(sdtpldt0(X0,X2),X0) = X2 ),
inference(equality_resolution,[],[f161]) ).
fof(f213,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| aNaturalNumber0(sdtmndt0(X1,X0)) ),
inference(equality_resolution,[],[f160]) ).
fof(f214,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| sdtpldt0(X0,sdtmndt0(X1,X0)) = X1 ),
inference(equality_resolution,[],[f159]) ).
fof(f217,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f181]) ).
fof(f218,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X0,X2))
| sz00 = X0
| ~ aNaturalNumber0(X2)
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(equality_resolution,[],[f184]) ).
fof(f219,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| aNaturalNumber0(sdtsldt0(X1,X0)) ),
inference(equality_resolution,[],[f183]) ).
fof(f220,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 ),
inference(equality_resolution,[],[f182]) ).
fof(f221,plain,
( ~ aNaturalNumber0(sz00)
| ~ isPrime0(sz00) ),
inference(equality_resolution,[],[f192]) ).
fof(f222,plain,
( ~ aNaturalNumber0(sz10)
| ~ isPrime0(sz10) ),
inference(equality_resolution,[],[f191]) ).
tcf(c_49,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f132]) ).
tcf(c_50,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f134]) ).
tcf(c_51,plain,
sz00 != sz10,
inference(cnf_transformation,[],[f133]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,X1) = sdtpldt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_56,plain,
! [X0: $i] :
( ( sdtpldt0(X0,sz00) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_57,plain,
! [X0: $i] :
( ( sdtpldt0(sz00,X0) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_60,plain,
! [X0: $i] :
( ( sdtasdt0(X0,sz10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_61,plain,
! [X0: $i] :
( ( sdtasdt0(sz10,X0) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_62,plain,
! [X0: $i] :
( ( sdtasdt0(X0,sz00) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_63,plain,
! [X0: $i] :
( ( sdtasdt0(sz00,X0) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f145]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) = sdtasdt0(X0,sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) = sdtasdt0(sdtpldt0(X1,X2),X0) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X0,X1) != sdtpldt0(X0,X2) ) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X0,X1) != sdtpldt0(X2,X1) ) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2) ) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = sz00 )
| ( X0 = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtasdt0(X0,X1) != sdtasdt0(X2,X1) ) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X0,X1) != sz00 ) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( ( X1 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtpldt0(X0,X1) != sz00 ) ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( ( X1 = sz00 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ( sdtasdt0(X0,X1) != sz00 ) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sK0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,sK0(X0,X1)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( ( sdtmndt0(sdtpldt0(X0,X1),X0) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sdtmndt0(X1,X0))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_82,plain,
! [X0: $i] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
| ( X0 = X1 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
| ( X0 = X1 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(sdtasdt0(X2,X0),sdtasdt0(X2,X1))
| ( X2 = sz00 )
| ( X0 = X1 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2))
| ( X2 = sz00 )
| ( X0 = X1 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_92,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( iLess0(X0,X1)
| ( X0 = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] :
( doDivides0(X0,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sK1(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(X0,sK1(X0,X1)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtsldt0(sdtasdt0(X0,X1),X0) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ doDivides0(X0,sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( doDivides0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( doDivides0(X0,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( doDivides0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X0,sdtpldt0(X1,X2)) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ( X1 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_106,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0)
| ( sK2(X0) != sz10 ) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_107,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0)
| ( sK2(X0) != X0 ) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_108,plain,
! [X0: $i] :
( isPrime0(X0)
| aNaturalNumber0(sK2(X0))
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_109,plain,
! [X0: $i] :
( isPrime0(X0)
| doDivides0(sK2(X0),X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_110,plain,
( ~ isPrime0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_111,plain,
( ~ isPrime0(sz10)
| ~ aNaturalNumber0(sz10) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz10 )
| ( X0 = X1 )
| ~ isPrime0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_113,plain,
! [X0: $i] :
( aNaturalNumber0(sK3(X0))
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_114,plain,
! [X0: $i] :
( doDivides0(sK3(X0),X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_115,plain,
! [X0: $i] :
( isPrime0(sK3(X0))
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( doDivides0(X0,X2)
| doDivides0(X0,X1)
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X1,X2)) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_117,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f206]) ).
tcf(c_118,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f205]) ).
tcf(c_119,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f204]) ).
tcf(c_120,plain,
sz00 != xn,
inference(cnf_transformation,[],[f203]) ).
tcf(c_121,plain,
sz00 != xm,
inference(cnf_transformation,[],[f202]) ).
tcf(c_122,plain,
sz00 != xp,
inference(cnf_transformation,[],[f201]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = sz00 )
| ( X1 = sz00 )
| ( X0 = sz00 )
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ iLess0(X2,xn)
| ( sdtasdt0(X0,sdtasdt0(X1,X1)) != sdtasdt0(X2,X2) ) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_124,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[],[f208]) ).
tcf(c_125,plain,
isPrime0(xp),
inference(cnf_transformation,[],[f209]) ).
tcf(c_126,negated_conjecture,
( ~ doDivides0(xp,xn)
| ~ doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_170,plain,
~ isPrime0(sz10),
inference(global_subsumption_just,[status(thm)],[c_111,c_50,c_111]) ).
tcf(c_172,plain,
~ isPrime0(sz00),
inference(global_subsumption_just,[status(thm)],[c_110,c_49,c_110]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( doDivides0(X0,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_95,c_53,c_95]) ).
tcf(c_177,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_73,c_52,c_73]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i] :
( ( sdtmndt0(sdtpldt0(X0,X1),X0) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_76,c_52,c_76,c_177]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtsldt0(sdtasdt0(X0,X1),X0) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_98,c_53,c_98,c_174]) ).
tcf(c_1282,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X3 = X4 )
| ( X2 = sz00 )
| ( X1 = sz00 )
| ( X0 = sz00 )
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X3,X4)
| ( X4 != xn )
| ( X2 != X3 )
| ( sdtasdt0(X0,sdtasdt0(X1,X1)) != sdtasdt0(X2,X2) ) ),
inference(resolution_lifted,[status(thm)],[c_94,c_123]) ).
tcf(c_1283,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = xn )
| ( X2 = sz00 )
| ( X1 = sz00 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(xn)
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X2,xn)
| ( sdtasdt0(X0,sdtasdt0(X1,X1)) != sdtasdt0(X2,X2) ) ),
inference(unflattening,[status(thm)],[c_1282]) ).
tcf(c_1284,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = xn )
| ( X2 = sz00 )
| ( X1 = sz00 )
| ( X0 = sz00 )
| ( sdtasdt0(X0,sdtasdt0(X1,X1)) != sdtasdt0(X2,X2) )
| ~ sdtlseqdt0(X2,xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ isPrime0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1283,c_117,c_1283]) ).
tcf(c_1285,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = xn )
| ( X2 = sz00 )
| ( X1 = sz00 )
| ( X0 = sz00 )
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X2,xn)
| ( sdtasdt0(X0,sdtasdt0(X1,X1)) != sdtasdt0(X2,X2) ) ),
inference(renaming,[status(thm)],[c_1284]) ).
tcf(c_3780,definition,
iPr_def_10 = sdtasdt0(xn,xn),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_3781,negated_conjecture,
( ~ doDivides0(xp,iPr_def_10)
| ~ doDivides0(xp,xn) ),
inference(demodulation,[status(thm)],[c_126,c_3780]) ).
tcf(c_5015,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(superposition,[status(thm)],[c_49,c_56]) ).
tcf(c_5016,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(superposition,[status(thm)],[c_50,c_56]) ).
tcf(c_5017,plain,
sdtpldt0(xn,sz00) = xn,
inference(superposition,[status(thm)],[c_117,c_56]) ).
tcf(c_5018,plain,
sdtpldt0(xm,sz00) = xm,
inference(superposition,[status(thm)],[c_118,c_56]) ).
tcf(c_5019,plain,
sdtpldt0(xp,sz00) = xp,
inference(superposition,[status(thm)],[c_119,c_56]) ).
tcf(c_5025,plain,
sdtpldt0(sz00,sz10) = sz10,
inference(superposition,[status(thm)],[c_50,c_57]) ).
tcf(c_5026,plain,
sdtpldt0(sz00,xn) = xn,
inference(superposition,[status(thm)],[c_117,c_57]) ).
tcf(c_5027,plain,
sdtpldt0(sz00,xm) = xm,
inference(superposition,[status(thm)],[c_118,c_57]) ).
tcf(c_5028,plain,
sdtpldt0(sz00,xp) = xp,
inference(superposition,[status(thm)],[c_119,c_57]) ).
tcf(c_5029,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_124,c_3780]) ).
tcf(c_5034,plain,
sdtasdt0(sz00,sz10) = sz00,
inference(superposition,[status(thm)],[c_49,c_60]) ).
tcf(c_5035,plain,
sdtasdt0(sz10,sz10) = sz10,
inference(superposition,[status(thm)],[c_50,c_60]) ).
tcf(c_5036,plain,
sdtasdt0(xn,sz10) = xn,
inference(superposition,[status(thm)],[c_117,c_60]) ).
tcf(c_5037,plain,
sdtasdt0(xm,sz10) = xm,
inference(superposition,[status(thm)],[c_118,c_60]) ).
tcf(c_5038,plain,
sdtasdt0(xp,sz10) = xp,
inference(superposition,[status(thm)],[c_119,c_60]) ).
tcf(c_5043,plain,
sdtasdt0(sz10,sz00) = sz00,
inference(superposition,[status(thm)],[c_49,c_61]) ).
tcf(c_5045,plain,
sdtasdt0(sz10,xn) = xn,
inference(superposition,[status(thm)],[c_117,c_61]) ).
tcf(c_5046,plain,
sdtasdt0(sz10,xm) = xm,
inference(superposition,[status(thm)],[c_118,c_61]) ).
tcf(c_5047,plain,
sdtasdt0(sz10,xp) = xp,
inference(superposition,[status(thm)],[c_119,c_61]) ).
tcf(c_5052,plain,
sdtasdt0(sz00,sz00) = sz00,
inference(superposition,[status(thm)],[c_49,c_62]) ).
tcf(c_5054,plain,
sdtasdt0(xn,sz00) = sz00,
inference(superposition,[status(thm)],[c_117,c_62]) ).
tcf(c_5055,plain,
sdtasdt0(xm,sz00) = sz00,
inference(superposition,[status(thm)],[c_118,c_62]) ).
tcf(c_5056,plain,
sdtasdt0(xp,sz00) = sz00,
inference(superposition,[status(thm)],[c_119,c_62]) ).
tcf(c_5063,plain,
sdtasdt0(sz00,xn) = sz00,
inference(superposition,[status(thm)],[c_117,c_63]) ).
tcf(c_5064,plain,
sdtasdt0(sz00,xm) = sz00,
inference(superposition,[status(thm)],[c_118,c_63]) ).
tcf(c_5065,plain,
sdtasdt0(sz00,xp) = sz00,
inference(superposition,[status(thm)],[c_119,c_63]) ).
tcf(c_5081,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz00,sdtpldt0(X0,X1)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_63]) ).
tcf(c_5082,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtpldt0(X0,X1),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_62]) ).
tcf(c_5083,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz10,sdtpldt0(X0,X1)) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_61]) ).
tcf(c_5084,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtpldt0(X0,X1),sz10) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_60]) ).
tcf(c_5085,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sz00,sdtpldt0(X0,X1)) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_57]) ).
tcf(c_5086,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(X0,X1),sz00) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_56]) ).
tcf(c_5118,plain,
( aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_3780,c_53]) ).
tcf(c_5131,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz00,sdtasdt0(X0,X1)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_63]) ).
tcf(c_5132,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(X0,X1),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_62]) ).
tcf(c_5133,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz10,sdtasdt0(X0,X1)) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_61]) ).
tcf(c_5134,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(X0,X1),sz10) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_60]) ).
tcf(c_5135,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sz00,sdtasdt0(X0,X1)) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_57]) ).
tcf(c_5136,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtasdt0(X0,X1),sz00) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_56]) ).
tcf(c_5137,plain,
aNaturalNumber0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5118,c_117]) ).
tcf(c_5168,plain,
( doDivides0(xp,iPr_def_10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(superposition,[status(thm)],[c_5029,c_174]) ).
tcf(c_5169,plain,
( doDivides0(xn,iPr_def_10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_3780,c_174]) ).
tcf(c_5170,plain,
( doDivides0(sz00,sz00)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5052,c_174]) ).
tcf(c_5171,plain,
( doDivides0(sz10,sz00)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5043,c_174]) ).
tcf(c_5173,plain,
( doDivides0(sz10,sz10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5035,c_174]) ).
tcf(c_5174,plain,
( doDivides0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5036,c_174]) ).
tcf(c_5175,plain,
( doDivides0(xm,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5037,c_174]) ).
tcf(c_5176,plain,
( doDivides0(xp,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5038,c_174]) ).
tcf(c_5177,plain,
( doDivides0(sz10,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5045,c_174]) ).
tcf(c_5178,plain,
( doDivides0(sz10,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5046,c_174]) ).
tcf(c_5179,plain,
( doDivides0(sz10,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5047,c_174]) ).
tcf(c_5180,plain,
( doDivides0(xn,sz00)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5054,c_174]) ).
tcf(c_5181,plain,
( doDivides0(xm,sz00)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5055,c_174]) ).
tcf(c_5182,plain,
doDivides0(sz10,sz10),
inference(forward_subsumption_resolution,[status(thm)],[c_5173,c_50]) ).
tcf(c_5183,plain,
doDivides0(sz00,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5170,c_49]) ).
tcf(c_5184,plain,
doDivides0(xn,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5169,c_117]) ).
tcf(c_5185,plain,
doDivides0(xm,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5181,c_118,c_49]) ).
tcf(c_5186,plain,
doDivides0(xn,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5180,c_117,c_49]) ).
tcf(c_5187,plain,
doDivides0(sz10,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_5179,c_119,c_50]) ).
tcf(c_5188,plain,
doDivides0(sz10,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_5178,c_118,c_50]) ).
tcf(c_5189,plain,
doDivides0(sz10,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_5177,c_117,c_50]) ).
tcf(c_5190,plain,
doDivides0(xp,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_5176,c_119,c_50]) ).
tcf(c_5191,plain,
doDivides0(xm,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_5175,c_118,c_50]) ).
tcf(c_5192,plain,
doDivides0(xn,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_5174,c_117,c_50]) ).
tcf(c_5193,plain,
doDivides0(sz10,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5171,c_50,c_49]) ).
tcf(c_5194,plain,
( doDivides0(xp,iPr_def_10)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5168,c_119]) ).
tcf(c_5203,plain,
( sdtlseqdt0(sz00,sz00)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5015,c_177]) ).
tcf(c_5204,plain,
( sdtlseqdt0(sz10,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5016,c_177]) ).
tcf(c_5205,plain,
( sdtlseqdt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5017,c_177]) ).
tcf(c_5206,plain,
( sdtlseqdt0(xm,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5018,c_177]) ).
tcf(c_5207,plain,
( sdtlseqdt0(xp,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5019,c_177]) ).
tcf(c_5208,plain,
( sdtlseqdt0(sz00,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5025,c_177]) ).
tcf(c_5209,plain,
( sdtlseqdt0(sz00,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5026,c_177]) ).
tcf(c_5210,plain,
( sdtlseqdt0(sz00,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5027,c_177]) ).
tcf(c_5211,plain,
( sdtlseqdt0(sz00,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5028,c_177]) ).
tcf(c_5212,plain,
sdtlseqdt0(sz00,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5203,c_49]) ).
tcf(c_5213,plain,
sdtlseqdt0(sz00,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_5211,c_119,c_49]) ).
tcf(c_5214,plain,
sdtlseqdt0(sz00,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_5210,c_118,c_49]) ).
tcf(c_5215,plain,
sdtlseqdt0(sz00,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_5209,c_117,c_49]) ).
tcf(c_5216,plain,
sdtlseqdt0(sz00,sz10),
inference(forward_subsumption_resolution,[status(thm)],[c_5208,c_50,c_49]) ).
tcf(c_5217,plain,
sdtlseqdt0(xp,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_5207,c_119,c_49]) ).
tcf(c_5218,plain,
sdtlseqdt0(xm,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_5206,c_118,c_49]) ).
tcf(c_5219,plain,
sdtlseqdt0(xn,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_5205,c_117,c_49]) ).
tcf(c_5220,plain,
sdtlseqdt0(sz10,sz10),
inference(forward_subsumption_resolution,[status(thm)],[c_5204,c_50,c_49]) ).
tcf(c_5221,plain,
sdtasdt0(sz00,iPr_def_10) = sz00,
inference(superposition,[status(thm)],[c_5137,c_63]) ).
tcf(c_5222,plain,
sdtasdt0(iPr_def_10,sz00) = sz00,
inference(superposition,[status(thm)],[c_5137,c_62]) ).
tcf(c_5223,plain,
sdtasdt0(sz10,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_5137,c_61]) ).
tcf(c_5224,plain,
sdtasdt0(iPr_def_10,sz10) = iPr_def_10,
inference(superposition,[status(thm)],[c_5137,c_60]) ).
tcf(c_5225,plain,
sdtpldt0(sz00,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_5137,c_57]) ).
tcf(c_5226,plain,
sdtpldt0(iPr_def_10,sz00) = iPr_def_10,
inference(superposition,[status(thm)],[c_5137,c_56]) ).
tcf(c_5243,plain,
! [X0: $i] :
( ( sdtpldt0(X0,sz00) = sdtpldt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_49,c_54]) ).
tcf(c_5244,plain,
! [X0: $i] :
( ( sdtpldt0(X0,sz10) = sdtpldt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_54]) ).
tcf(c_5245,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X2,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_54]) ).
tcf(c_5246,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtasdt0(X0,X1),X2) = sdtpldt0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_54]) ).
tcf(c_5247,plain,
! [X0: $i] :
( ( sdtpldt0(X0,xn) = sdtpldt0(xn,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_54]) ).
tcf(c_5248,plain,
! [X0: $i] :
( ( sdtpldt0(X0,xm) = sdtpldt0(xm,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_54]) ).
tcf(c_5249,plain,
! [X0: $i] :
( ( sdtpldt0(X0,xp) = sdtpldt0(xp,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_54]) ).
tcf(c_5250,plain,
! [X0: $i] :
( ( sdtpldt0(X0,iPr_def_10) = sdtpldt0(iPr_def_10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_54]) ).
tcf(c_5287,plain,
! [X0: $i] :
( ( sdtasdt0(X0,sz00) = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_49,c_58]) ).
tcf(c_5288,plain,
! [X0: $i] :
( ( sdtasdt0(X0,sz10) = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_58]) ).
tcf(c_5289,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sdtpldt0(X0,X1),X2) = sdtasdt0(X2,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_58]) ).
tcf(c_5290,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_58]) ).
tcf(c_5291,plain,
! [X0: $i] :
( ( sdtasdt0(X0,xn) = sdtasdt0(xn,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_58]) ).
tcf(c_5292,plain,
! [X0: $i] :
( ( sdtasdt0(X0,xm) = sdtasdt0(xm,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_58]) ).
tcf(c_5293,plain,
! [X0: $i] :
( ( sdtasdt0(X0,xp) = sdtasdt0(xp,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_58]) ).
tcf(c_5294,plain,
! [X0: $i] :
( ( sdtasdt0(X0,iPr_def_10) = sdtasdt0(iPr_def_10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_58]) ).
tcf(c_5338,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sK0(X0,X1),X2) = sdtasdt0(X2,sK0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_58]) ).
tcf(c_5339,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sK0(X0,X1),X2) = sdtpldt0(X2,sK0(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_54]) ).
tcf(c_5340,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz00,sK0(X0,X1)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_63]) ).
tcf(c_5341,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sK0(X0,X1),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_62]) ).
tcf(c_5342,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz10,sK0(X0,X1)) = sK0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_61]) ).
tcf(c_5343,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sK0(X0,X1),sz10) = sK0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_60]) ).
tcf(c_5344,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sz00,sK0(X0,X1)) = sK0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_57]) ).
tcf(c_5345,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK0(X0,X1),sz00) = sK0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_56]) ).
tcf(c_5400,plain,
( doDivides0(xp,sz00)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5056,c_174]) ).
tcf(c_5402,plain,
doDivides0(xp,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5400,c_119,c_49]) ).
tcf(c_5415,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sdtmndt0(X1,X0),X2) = sdtasdt0(X2,sdtmndt0(X1,X0)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_58]) ).
tcf(c_5416,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sdtmndt0(X1,X0),X2) = sdtpldt0(X2,sdtmndt0(X1,X0)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_54]) ).
tcf(c_5417,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz00,sdtmndt0(X1,X0)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_63]) ).
tcf(c_5418,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtmndt0(X1,X0),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_62]) ).
tcf(c_5419,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz10,sdtmndt0(X1,X0)) = sdtmndt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_61]) ).
tcf(c_5420,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtmndt0(X1,X0),sz10) = sdtmndt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_60]) ).
tcf(c_5421,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sz00,sdtmndt0(X1,X0)) = sdtmndt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_57]) ).
tcf(c_5422,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtmndt0(X1,X0),sz00) = sdtmndt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_56]) ).
tcf(c_5489,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(sK1(X0,X1),X2) = sdtasdt0(X2,sK1(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_58]) ).
tcf(c_5490,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(sK1(X0,X1),X2) = sdtpldt0(X2,sK1(X0,X1)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_54]) ).
tcf(c_5491,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz00,sK1(X0,X1)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_63]) ).
tcf(c_5492,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sK1(X0,X1),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_62]) ).
tcf(c_5493,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sz10,sK1(X0,X1)) = sK1(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_61]) ).
tcf(c_5494,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sK1(X0,X1),sz10) = sK1(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_60]) ).
tcf(c_5495,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sz00,sK1(X0,X1)) = sK1(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_57]) ).
tcf(c_5496,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK1(X0,X1),sz00) = sK1(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_56]) ).
tcf(c_5562,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK3(X0),X1) = sdtasdt0(X1,sK3(X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_58]) ).
tcf(c_5563,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK3(X0),X1) = sdtpldt0(X1,sK3(X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_54]) ).
tcf(c_5564,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sz00,sK3(X0)) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_63]) ).
tcf(c_5565,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK3(X0),sz00) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_62]) ).
tcf(c_5566,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sz10,sK3(X0)) = sK3(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_61]) ).
tcf(c_5567,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK3(X0),sz10) = sK3(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_60]) ).
tcf(c_5568,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz00,sK3(X0)) = sK3(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_57]) ).
tcf(c_5569,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK3(X0),sz00) = sK3(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_56]) ).
tcf(c_5616,plain,
( doDivides0(iPr_def_10,sz00)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5222,c_174]) ).
tcf(c_5618,plain,
doDivides0(iPr_def_10,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_5616,c_5137,c_49]) ).
tcf(c_5619,plain,
( doDivides0(sz10,iPr_def_10)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5223,c_174]) ).
tcf(c_5621,plain,
doDivides0(sz10,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5619,c_5137,c_50]) ).
tcf(c_5622,plain,
( doDivides0(iPr_def_10,iPr_def_10)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5224,c_174]) ).
tcf(c_5624,plain,
doDivides0(iPr_def_10,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5622,c_5137,c_50]) ).
tcf(c_5637,plain,
( sdtlseqdt0(sz00,iPr_def_10)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5225,c_177]) ).
tcf(c_5639,plain,
sdtlseqdt0(sz00,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5637,c_5137,c_49]) ).
tcf(c_5640,plain,
( sdtlseqdt0(iPr_def_10,iPr_def_10)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5226,c_177]) ).
tcf(c_5642,plain,
sdtlseqdt0(iPr_def_10,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5640,c_5137,c_49]) ).
tcf(c_5651,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sz00,X0),X1) = sdtasdt0(sz00,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_49,c_59]) ).
tcf(c_5652,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sz10,X0),X1) = sdtasdt0(sz10,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_59]) ).
tcf(c_5653,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(X0,X1),X2),X3) = sdtasdt0(sdtpldt0(X0,X1),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_59]) ).
tcf(c_5654,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtasdt0(sdtasdt0(sdtasdt0(X0,X1),X2),X3) = sdtasdt0(sdtasdt0(X0,X1),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_59]) ).
tcf(c_5655,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtasdt0(sdtasdt0(sK0(X0,X1),X2),X3) = sdtasdt0(sK0(X0,X1),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_59]) ).
tcf(c_5656,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtasdt0(sdtasdt0(sdtmndt0(X1,X0),X2),X3) = sdtasdt0(sdtmndt0(X1,X0),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_59]) ).
tcf(c_5657,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtasdt0(sdtasdt0(sK1(X0,X1),X2),X3) = sdtasdt0(sK1(X0,X1),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_59]) ).
tcf(c_5658,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sdtasdt0(sK3(X0),X1),X2) = sdtasdt0(sK3(X0),sdtasdt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_59]) ).
tcf(c_5659,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(xn,X0),X1) = sdtasdt0(xn,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_59]) ).
tcf(c_5660,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(xm,X0),X1) = sdtasdt0(xm,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_59]) ).
tcf(c_5661,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(xp,X0),X1) = sdtasdt0(xp,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_59]) ).
tcf(c_5662,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(iPr_def_10,X0),X1) = sdtasdt0(iPr_def_10,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_59]) ).
tcf(c_5755,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sz00,X0),sz00) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_49,c_180]) ).
tcf(c_5756,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sz10,X0),sz10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_180]) ).
tcf(c_5757,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_180]) ).
tcf(c_5758,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(sdtpldt0(sdtasdt0(X0,X1),X2),sdtasdt0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_180]) ).
tcf(c_5759,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(sdtpldt0(sK0(X0,X1),X2),sK0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_180]) ).
tcf(c_5760,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(sdtpldt0(sdtmndt0(X1,X0),X2),sdtmndt0(X1,X0)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_180]) ).
tcf(c_5761,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(sdtpldt0(sK1(X0,X1),X2),sK1(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_180]) ).
tcf(c_5762,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtmndt0(sdtpldt0(sK3(X0),X1),sK3(X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_180]) ).
tcf(c_5763,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(xn,X0),xn) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_180]) ).
tcf(c_5764,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(xm,X0),xm) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_180]) ).
tcf(c_5765,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(xp,X0),xp) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_180]) ).
tcf(c_5766,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(iPr_def_10,X0),iPr_def_10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_180]) ).
tcf(c_5873,plain,
( sdtlseqdt0(xp,iPr_def_10)
| ( sdtasdt0(xm,xm) = sz00 )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(superposition,[status(thm)],[c_5029,c_93]) ).
tcf(c_5874,plain,
( sdtlseqdt0(xn,iPr_def_10)
| ( sz00 = xn )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_3780,c_93]) ).
tcf(c_5882,plain,
( sdtlseqdt0(sz10,xn)
| ( sz00 = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5045,c_93]) ).
tcf(c_5883,plain,
( sdtlseqdt0(sz10,xm)
| ( sz00 = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5046,c_93]) ).
tcf(c_5884,plain,
( sdtlseqdt0(sz10,xp)
| ( sz00 = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5047,c_93]) ).
tcf(c_5893,plain,
( sdtlseqdt0(sz10,iPr_def_10)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5223,c_93]) ).
tcf(c_5895,plain,
sdtlseqdt0(xn,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5874,c_120,c_117]) ).
tcf(c_5896,plain,
( sdtlseqdt0(sz10,iPr_def_10)
| ( sz00 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5893,c_5137,c_50]) ).
tcf(c_5899,plain,
sdtlseqdt0(sz10,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_5884,c_122,c_119,c_50]) ).
tcf(c_5900,plain,
sdtlseqdt0(sz10,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_5883,c_121,c_118,c_50]) ).
tcf(c_5901,plain,
sdtlseqdt0(sz10,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_5882,c_120,c_117,c_50]) ).
tcf(c_5902,plain,
( sdtlseqdt0(xp,iPr_def_10)
| ( sdtasdt0(xm,xm) = sz00 )
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5873,c_119]) ).
tcf(c_5922,plain,
( doDivides0(xp,iPr_def_10)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm)],[c_53,c_5194]) ).
tcf(c_5923,plain,
doDivides0(xp,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_5922,c_118]) ).
tcf(c_5924,plain,
~ doDivides0(xp,xn),
inference(backward_subsumption_resolution,[status(thm)],[c_3781,c_5923]) ).
tcf(c_5930,plain,
sdtpldt0(sz00,sz10) = sdtpldt0(sz10,sz00),
inference(superposition,[status(thm)],[c_50,c_5243]) ).
tcf(c_5931,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(X0,X1),sz00) = sdtpldt0(sz00,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_5243]) ).
tcf(c_5932,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtasdt0(X0,X1),sz00) = sdtpldt0(sz00,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_5243]) ).
tcf(c_5933,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK0(X0,X1),sz00) = sdtpldt0(sz00,sK0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_5243]) ).
tcf(c_5934,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtmndt0(X1,X0),sz00) = sdtpldt0(sz00,sdtmndt0(X1,X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_5243]) ).
tcf(c_5935,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK1(X0,X1),sz00) = sdtpldt0(sz00,sK1(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_5243]) ).
tcf(c_5936,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK3(X0),sz00) = sdtpldt0(sz00,sK3(X0)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_5243]) ).
tcf(c_5937,plain,
sdtpldt0(sz00,xn) = sdtpldt0(xn,sz00),
inference(superposition,[status(thm)],[c_117,c_5243]) ).
tcf(c_5938,plain,
sdtpldt0(sz00,xm) = sdtpldt0(xm,sz00),
inference(superposition,[status(thm)],[c_118,c_5243]) ).
tcf(c_5939,plain,
sdtpldt0(sz00,xp) = sdtpldt0(xp,sz00),
inference(superposition,[status(thm)],[c_119,c_5243]) ).
tcf(c_5940,plain,
sdtpldt0(sz00,iPr_def_10) = sdtpldt0(iPr_def_10,sz00),
inference(superposition,[status(thm)],[c_5137,c_5243]) ).
tcf(c_5974,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(X0,X1),sz10) = sdtpldt0(sz10,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_5244]) ).
tcf(c_5975,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtasdt0(X0,X1),sz10) = sdtpldt0(sz10,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_5244]) ).
tcf(c_5976,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK0(X0,X1),sz10) = sdtpldt0(sz10,sK0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_5244]) ).
tcf(c_5977,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtmndt0(X1,X0),sz10) = sdtpldt0(sz10,sdtmndt0(X1,X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_5244]) ).
tcf(c_5978,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sK1(X0,X1),sz10) = sdtpldt0(sz10,sK1(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_5244]) ).
tcf(c_5979,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK3(X0),sz10) = sdtpldt0(sz10,sK3(X0)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_5244]) ).
tcf(c_5980,plain,
sdtpldt0(sz10,xn) = sdtpldt0(xn,sz10),
inference(superposition,[status(thm)],[c_117,c_5244]) ).
tcf(c_5981,plain,
sdtpldt0(sz10,xm) = sdtpldt0(xm,sz10),
inference(superposition,[status(thm)],[c_118,c_5244]) ).
tcf(c_5982,plain,
sdtpldt0(sz10,xp) = sdtpldt0(xp,sz10),
inference(superposition,[status(thm)],[c_119,c_5244]) ).
tcf(c_5983,plain,
sdtpldt0(sz10,iPr_def_10) = sdtpldt0(iPr_def_10,sz10),
inference(superposition,[status(thm)],[c_5137,c_5244]) ).
tcf(c_6011,plain,
( sdtlseqdt0(xn,sdtpldt0(sz10,xn))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5980,c_177]) ).
tcf(c_6012,plain,
( aNaturalNumber0(sdtpldt0(sz10,xn))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5980,c_52]) ).
tcf(c_6013,plain,
aNaturalNumber0(sdtpldt0(sz10,xn)),
inference(forward_subsumption_resolution,[status(thm)],[c_6012,c_117,c_50]) ).
tcf(c_6014,plain,
sdtlseqdt0(xn,sdtpldt0(sz10,xn)),
inference(forward_subsumption_resolution,[status(thm)],[c_6011,c_117,c_50]) ).
tcf(c_6015,plain,
sdtpldt0(sdtpldt0(sz10,xn),sz10) = sdtpldt0(sz10,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6013,c_5244]) ).
tcf(c_6016,plain,
sdtpldt0(sdtpldt0(sz10,xn),sz00) = sdtpldt0(sz00,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6013,c_5243]) ).
tcf(c_6017,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(sz10,xn),X0),sdtpldt0(sz10,xn)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_180]) ).
tcf(c_6018,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(sz10,xn),X0),X1) = sdtasdt0(sdtpldt0(sz10,xn),sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_59]) ).
tcf(c_6019,plain,
! [X0: $i] :
( ( sdtasdt0(sdtpldt0(sz10,xn),X0) = sdtasdt0(X0,sdtpldt0(sz10,xn)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_58]) ).
tcf(c_6020,plain,
! [X0: $i] :
( ( sdtpldt0(sdtpldt0(sz10,xn),X0) = sdtpldt0(X0,sdtpldt0(sz10,xn)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_54]) ).
tcf(c_6021,plain,
sdtasdt0(sz00,sdtpldt0(sz10,xn)) = sz00,
inference(superposition,[status(thm)],[c_6013,c_63]) ).
tcf(c_6022,plain,
sdtasdt0(sdtpldt0(sz10,xn),sz00) = sz00,
inference(superposition,[status(thm)],[c_6013,c_62]) ).
tcf(c_6023,plain,
sdtasdt0(sz10,sdtpldt0(sz10,xn)) = sdtpldt0(sz10,xn),
inference(superposition,[status(thm)],[c_6013,c_61]) ).
tcf(c_6024,plain,
sdtasdt0(sdtpldt0(sz10,xn),sz10) = sdtpldt0(sz10,xn),
inference(superposition,[status(thm)],[c_6013,c_60]) ).
tcf(c_6025,plain,
sdtpldt0(sz00,sdtpldt0(sz10,xn)) = sdtpldt0(sz10,xn),
inference(superposition,[status(thm)],[c_6013,c_57]) ).
tcf(c_6026,plain,
sdtpldt0(sdtpldt0(sz10,xn),sz00) = sdtpldt0(sz10,xn),
inference(superposition,[status(thm)],[c_6013,c_56]) ).
tcf(c_6039,plain,
( sdtlseqdt0(xp,sdtpldt0(sz10,xp))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5982,c_177]) ).
tcf(c_6040,plain,
( aNaturalNumber0(sdtpldt0(sz10,xp))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5982,c_52]) ).
tcf(c_6041,plain,
aNaturalNumber0(sdtpldt0(sz10,xp)),
inference(forward_subsumption_resolution,[status(thm)],[c_6040,c_119,c_50]) ).
tcf(c_6042,plain,
sdtlseqdt0(xp,sdtpldt0(sz10,xp)),
inference(forward_subsumption_resolution,[status(thm)],[c_6039,c_119,c_50]) ).
tcf(c_6059,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK2(X0),sz10) = sdtpldt0(sz10,sK2(X0)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_5244]) ).
tcf(c_6060,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK2(X0),sz00) = sdtpldt0(sz00,sK2(X0)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_5243]) ).
tcf(c_6061,plain,
! [X0: $i,X1: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtmndt0(sdtpldt0(sK2(X0),X1),sK2(X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_180]) ).
tcf(c_6062,plain,
! [X0: $i,X1: $i,X2: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sdtasdt0(sK2(X0),X1),X2) = sdtasdt0(sK2(X0),sdtasdt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_59]) ).
tcf(c_6063,plain,
! [X0: $i,X1: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK2(X0),X1) = sdtasdt0(X1,sK2(X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_58]) ).
tcf(c_6064,plain,
! [X0: $i,X1: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK2(X0),X1) = sdtpldt0(X1,sK2(X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_54]) ).
tcf(c_6065,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sz00,sK2(X0)) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_63]) ).
tcf(c_6066,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK2(X0),sz00) = sz00 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_62]) ).
tcf(c_6067,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sz10,sK2(X0)) = sK2(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_61]) ).
tcf(c_6068,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK2(X0),sz10) = sK2(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_60]) ).
tcf(c_6069,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz00,sK2(X0)) = sK2(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_57]) ).
tcf(c_6070,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sK2(X0),sz00) = sK2(X0) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_56]) ).
tcf(c_6195,plain,
( ( sz00 = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10)
| ( sdtpldt0(sz10,xn) != sz00 ) ),
inference(superposition,[status(thm)],[c_5980,c_70]) ).
tcf(c_6196,plain,
( ( sz00 = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ( sdtpldt0(sz10,xp) != sz00 ) ),
inference(superposition,[status(thm)],[c_5982,c_70]) ).
tcf(c_6197,plain,
sdtpldt0(sz10,xp) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6196,c_122,c_119,c_50]) ).
tcf(c_6198,plain,
sdtpldt0(sz10,xn) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6195,c_120,c_117,c_50]) ).
tcf(c_6230,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,sdtasdt0(X0,X1))
| ( sdtasdt0(X0,X1) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_174,c_104]) ).
tcf(c_6231,plain,
! [X0: $i] :
( sdtlseqdt0(sK3(X0),X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3(X0)) ),
inference(superposition,[status(thm)],[c_114,c_104]) ).
tcf(c_6234,plain,
( sdtlseqdt0(xp,iPr_def_10)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_5923,c_104]) ).
tcf(c_6249,plain,
( sdtlseqdt0(xp,iPr_def_10)
| ( sz00 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6234,c_5137,c_119]) ).
tcf(c_6262,plain,
sdtpldt0(sdtpldt0(sz10,xp),sz10) = sdtpldt0(sz10,sdtpldt0(sz10,xp)),
inference(superposition,[status(thm)],[c_6041,c_5244]) ).
tcf(c_6263,plain,
sdtpldt0(sdtpldt0(sz10,xp),sz00) = sdtpldt0(sz00,sdtpldt0(sz10,xp)),
inference(superposition,[status(thm)],[c_6041,c_5243]) ).
tcf(c_6264,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(sz10,xp),X0),sdtpldt0(sz10,xp)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_180]) ).
tcf(c_6265,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(sz10,xp),X0),X1) = sdtasdt0(sdtpldt0(sz10,xp),sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_59]) ).
tcf(c_6266,plain,
! [X0: $i] :
( ( sdtasdt0(sdtpldt0(sz10,xp),X0) = sdtasdt0(X0,sdtpldt0(sz10,xp)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_58]) ).
tcf(c_6267,plain,
! [X0: $i] :
( ( sdtpldt0(sdtpldt0(sz10,xp),X0) = sdtpldt0(X0,sdtpldt0(sz10,xp)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_54]) ).
tcf(c_6268,plain,
sdtasdt0(sz00,sdtpldt0(sz10,xp)) = sz00,
inference(superposition,[status(thm)],[c_6041,c_63]) ).
tcf(c_6269,plain,
sdtasdt0(sdtpldt0(sz10,xp),sz00) = sz00,
inference(superposition,[status(thm)],[c_6041,c_62]) ).
tcf(c_6270,plain,
sdtasdt0(sz10,sdtpldt0(sz10,xp)) = sdtpldt0(sz10,xp),
inference(superposition,[status(thm)],[c_6041,c_61]) ).
tcf(c_6271,plain,
sdtasdt0(sdtpldt0(sz10,xp),sz10) = sdtpldt0(sz10,xp),
inference(superposition,[status(thm)],[c_6041,c_60]) ).
tcf(c_6272,plain,
sdtpldt0(sz00,sdtpldt0(sz10,xp)) = sdtpldt0(sz10,xp),
inference(superposition,[status(thm)],[c_6041,c_57]) ).
tcf(c_6273,plain,
sdtpldt0(sdtpldt0(sz10,xp),sz00) = sdtpldt0(sz10,xp),
inference(superposition,[status(thm)],[c_6041,c_56]) ).
tcf(c_6291,plain,
( ( sz00 = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10)
| ( sdtpldt0(sz10,xm) != sz00 ) ),
inference(superposition,[status(thm)],[c_5981,c_70]) ).
tcf(c_6292,plain,
( sdtlseqdt0(xm,sdtpldt0(sz10,xm))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5981,c_177]) ).
tcf(c_6293,plain,
( aNaturalNumber0(sdtpldt0(sz10,xm))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5981,c_52]) ).
tcf(c_6294,plain,
aNaturalNumber0(sdtpldt0(sz10,xm)),
inference(forward_subsumption_resolution,[status(thm)],[c_6293,c_118,c_50]) ).
tcf(c_6295,plain,
sdtlseqdt0(xm,sdtpldt0(sz10,xm)),
inference(forward_subsumption_resolution,[status(thm)],[c_6292,c_118,c_50]) ).
tcf(c_6296,plain,
sdtpldt0(sz10,xm) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6291,c_121,c_118,c_50]) ).
tcf(c_6297,plain,
sdtpldt0(sdtpldt0(sz10,xm),sz10) = sdtpldt0(sz10,sdtpldt0(sz10,xm)),
inference(superposition,[status(thm)],[c_6294,c_5244]) ).
tcf(c_6298,plain,
sdtpldt0(sdtpldt0(sz10,xm),sz00) = sdtpldt0(sz00,sdtpldt0(sz10,xm)),
inference(superposition,[status(thm)],[c_6294,c_5243]) ).
tcf(c_6299,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(sz10,xm),X0),sdtpldt0(sz10,xm)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_180]) ).
tcf(c_6300,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(sz10,xm),X0),X1) = sdtasdt0(sdtpldt0(sz10,xm),sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_59]) ).
tcf(c_6301,plain,
! [X0: $i] :
( ( sdtasdt0(sdtpldt0(sz10,xm),X0) = sdtasdt0(X0,sdtpldt0(sz10,xm)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_58]) ).
tcf(c_6302,plain,
! [X0: $i] :
( ( sdtpldt0(sdtpldt0(sz10,xm),X0) = sdtpldt0(X0,sdtpldt0(sz10,xm)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_54]) ).
tcf(c_6303,plain,
sdtasdt0(sz00,sdtpldt0(sz10,xm)) = sz00,
inference(superposition,[status(thm)],[c_6294,c_63]) ).
tcf(c_6304,plain,
sdtasdt0(sdtpldt0(sz10,xm),sz00) = sz00,
inference(superposition,[status(thm)],[c_6294,c_62]) ).
tcf(c_6305,plain,
sdtasdt0(sz10,sdtpldt0(sz10,xm)) = sdtpldt0(sz10,xm),
inference(superposition,[status(thm)],[c_6294,c_61]) ).
tcf(c_6306,plain,
sdtasdt0(sdtpldt0(sz10,xm),sz10) = sdtpldt0(sz10,xm),
inference(superposition,[status(thm)],[c_6294,c_60]) ).
tcf(c_6307,plain,
sdtpldt0(sz00,sdtpldt0(sz10,xm)) = sdtpldt0(sz10,xm),
inference(superposition,[status(thm)],[c_6294,c_57]) ).
tcf(c_6308,plain,
sdtpldt0(sdtpldt0(sz10,xm),sz00) = sdtpldt0(sz10,xm),
inference(superposition,[status(thm)],[c_6294,c_56]) ).
tcf(c_6335,plain,
( ( sz00 = sz10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10)
| ( sdtpldt0(iPr_def_10,sz10) != sz00 ) ),
inference(superposition,[status(thm)],[c_5983,c_70]) ).
tcf(c_6336,plain,
( sdtlseqdt0(sz10,sdtpldt0(iPr_def_10,sz10))
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5983,c_177]) ).
tcf(c_6337,plain,
( aNaturalNumber0(sdtpldt0(iPr_def_10,sz10))
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5983,c_52]) ).
tcf(c_6338,plain,
aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)),
inference(forward_subsumption_resolution,[status(thm)],[c_6337,c_5137,c_50]) ).
tcf(c_6339,plain,
sdtlseqdt0(sz10,sdtpldt0(iPr_def_10,sz10)),
inference(forward_subsumption_resolution,[status(thm)],[c_6336,c_5137,c_50]) ).
tcf(c_6340,plain,
sdtpldt0(iPr_def_10,sz10) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6335,c_51,c_5137,c_50]) ).
tcf(c_6373,plain,
sdtpldt0(sdtpldt0(iPr_def_10,sz10),sz10) = sdtpldt0(sz10,sdtpldt0(iPr_def_10,sz10)),
inference(superposition,[status(thm)],[c_6338,c_5244]) ).
tcf(c_6374,plain,
sdtpldt0(sdtpldt0(iPr_def_10,sz10),sz00) = sdtpldt0(sz00,sdtpldt0(iPr_def_10,sz10)),
inference(superposition,[status(thm)],[c_6338,c_5243]) ).
tcf(c_6375,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(iPr_def_10,sz10),X0),sdtpldt0(iPr_def_10,sz10)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_180]) ).
tcf(c_6376,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(iPr_def_10,sz10),X0),X1) = sdtasdt0(sdtpldt0(iPr_def_10,sz10),sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_59]) ).
tcf(c_6377,plain,
! [X0: $i] :
( ( sdtasdt0(sdtpldt0(iPr_def_10,sz10),X0) = sdtasdt0(X0,sdtpldt0(iPr_def_10,sz10)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_58]) ).
tcf(c_6378,plain,
! [X0: $i] :
( ( sdtpldt0(sdtpldt0(iPr_def_10,sz10),X0) = sdtpldt0(X0,sdtpldt0(iPr_def_10,sz10)) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_54]) ).
tcf(c_6379,plain,
sdtasdt0(sz00,sdtpldt0(iPr_def_10,sz10)) = sz00,
inference(superposition,[status(thm)],[c_6338,c_63]) ).
tcf(c_6380,plain,
sdtasdt0(sdtpldt0(iPr_def_10,sz10),sz00) = sz00,
inference(superposition,[status(thm)],[c_6338,c_62]) ).
tcf(c_6381,plain,
sdtasdt0(sz10,sdtpldt0(iPr_def_10,sz10)) = sdtpldt0(iPr_def_10,sz10),
inference(superposition,[status(thm)],[c_6338,c_61]) ).
tcf(c_6382,plain,
sdtasdt0(sdtpldt0(iPr_def_10,sz10),sz10) = sdtpldt0(iPr_def_10,sz10),
inference(superposition,[status(thm)],[c_6338,c_60]) ).
tcf(c_6383,plain,
sdtpldt0(sz00,sdtpldt0(iPr_def_10,sz10)) = sdtpldt0(iPr_def_10,sz10),
inference(superposition,[status(thm)],[c_6338,c_57]) ).
tcf(c_6384,plain,
sdtpldt0(sdtpldt0(iPr_def_10,sz10),sz00) = sdtpldt0(iPr_def_10,sz10),
inference(superposition,[status(thm)],[c_6338,c_56]) ).
tcf(c_6436,plain,
( ( sz00 = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn))
| ( sdtpldt0(sz10,sdtpldt0(sz10,xn)) != sz00 ) ),
inference(superposition,[status(thm)],[c_6015,c_71]) ).
tcf(c_6438,plain,
( sdtlseqdt0(sdtpldt0(sz10,xn),sdtpldt0(sz10,sdtpldt0(sz10,xn)))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6015,c_177]) ).
tcf(c_6439,plain,
( aNaturalNumber0(sdtpldt0(sz10,sdtpldt0(sz10,xn)))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6015,c_52]) ).
tcf(c_6440,plain,
aNaturalNumber0(sdtpldt0(sz10,sdtpldt0(sz10,xn))),
inference(forward_subsumption_resolution,[status(thm)],[c_6439,c_50,c_6013]) ).
tcf(c_6441,plain,
sdtlseqdt0(sdtpldt0(sz10,xn),sdtpldt0(sz10,sdtpldt0(sz10,xn))),
inference(forward_subsumption_resolution,[status(thm)],[c_6438,c_50,c_6013]) ).
tcf(c_6442,plain,
sdtpldt0(sz10,sdtpldt0(sz10,xn)) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6436,c_51,c_50,c_6013]) ).
tcf(c_6453,plain,
! [X0: $i] :
( isPrime0(X0)
| sdtlseqdt0(sK2(X0),X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK2(X0)) ),
inference(superposition,[status(thm)],[c_109,c_104]) ).
tcf(c_6468,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,sK0(X0,sdtpldt0(X0,X1))) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_177,c_75]) ).
tcf(c_6469,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X1,X0)
| ( sdtpldt0(X0,sK0(X0,X1)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_83,c_75]) ).
tcf(c_6470,plain,
! [X0: $i] :
( ( sdtpldt0(X0,sK0(X0,X0)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_82,c_75]) ).
tcf(c_6471,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ( sdtpldt0(X1,sK0(X1,X0)) = X0 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_83,c_75]) ).
tcf(c_6472,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz10,sK0(sz10,X0)) = X0 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_92,c_75]) ).
tcf(c_6473,plain,
! [X0: $i,X1: $i] :
( ( X1 = sz00 )
| ( sdtpldt0(X0,sK0(X0,sdtasdt0(X0,X1))) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_93,c_75]) ).
tcf(c_6474,plain,
( ( sdtpldt0(sz00,sK0(sz00,sz00)) = sz00 )
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5212,c_75]) ).
tcf(c_6475,plain,
( ( sdtpldt0(sz00,sK0(sz00,xn)) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5215,c_75]) ).
tcf(c_6476,plain,
( ( sdtpldt0(sz10,sK0(sz10,sz10)) = sz10 )
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5220,c_75]) ).
tcf(c_6477,plain,
( ( sdtpldt0(xn,sK0(xn,xn)) = xn )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5219,c_75]) ).
tcf(c_6478,plain,
( ( sdtpldt0(xm,sK0(xm,xm)) = xm )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm)],[c_5218,c_75]) ).
tcf(c_6479,plain,
( ( sdtpldt0(xp,sK0(xp,xp)) = xp )
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_5217,c_75]) ).
tcf(c_6480,plain,
( ( sdtpldt0(sz00,sK0(sz00,sz10)) = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5216,c_75]) ).
tcf(c_6481,plain,
( ( sdtpldt0(sz00,sK0(sz00,xm)) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5214,c_75]) ).
tcf(c_6482,plain,
( ( sdtpldt0(sz00,sK0(sz00,xp)) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5213,c_75]) ).
tcf(c_6483,plain,
( ( sdtpldt0(sz00,sK0(sz00,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5639,c_75]) ).
tcf(c_6484,plain,
( ( sdtpldt0(iPr_def_10,sK0(iPr_def_10,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_5642,c_75]) ).
tcf(c_6485,plain,
( ( sdtpldt0(sz10,sK0(sz10,xn)) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5901,c_75]) ).
tcf(c_6486,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(xp,sK0(xp,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_6249,c_75]) ).
tcf(c_6487,plain,
( ( sdtpldt0(xn,sK0(xn,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5895,c_75]) ).
tcf(c_6488,plain,
( ( sdtpldt0(sz10,sK0(sz10,xm)) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5900,c_75]) ).
tcf(c_6489,plain,
( ( sdtpldt0(sz10,sK0(sz10,xp)) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5899,c_75]) ).
tcf(c_6490,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(sz10,sK0(sz10,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5896,c_75]) ).
tcf(c_6491,plain,
( ( sdtpldt0(xn,sK0(xn,sdtpldt0(sz10,xn))) = sdtpldt0(sz10,xn) )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6014,c_75]) ).
tcf(c_6492,plain,
( ( sdtpldt0(xp,sK0(xp,sdtpldt0(sz10,xp))) = sdtpldt0(sz10,xp) )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp)) ),
inference(superposition,[status(thm)],[c_6042,c_75]) ).
tcf(c_6493,plain,
( ( sdtpldt0(xm,sK0(xm,sdtpldt0(sz10,xm))) = sdtpldt0(sz10,xm) )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm)) ),
inference(superposition,[status(thm)],[c_6295,c_75]) ).
tcf(c_6494,plain,
sdtpldt0(iPr_def_10,sK0(iPr_def_10,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6484,c_5137]) ).
tcf(c_6495,plain,
sdtpldt0(xp,sK0(xp,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6479,c_119]) ).
tcf(c_6496,plain,
sdtpldt0(xm,sK0(xm,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6478,c_118]) ).
tcf(c_6497,plain,
sdtpldt0(xn,sK0(xn,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6477,c_117]) ).
tcf(c_6498,plain,
sdtpldt0(sz10,sK0(sz10,sz10)) = sz10,
inference(forward_subsumption_resolution,[status(thm)],[c_6476,c_50]) ).
tcf(c_6499,plain,
sdtpldt0(sz00,sK0(sz00,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6474,c_49]) ).
tcf(c_6502,plain,
sdtpldt0(sz10,sK0(sz10,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6489,c_119,c_50]) ).
tcf(c_6503,plain,
sdtpldt0(sz10,sK0(sz10,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6488,c_118,c_50]) ).
tcf(c_6504,plain,
sdtpldt0(xn,sK0(xn,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6487,c_5137,c_117]) ).
tcf(c_6505,plain,
sdtpldt0(sz10,sK0(sz10,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6485,c_117,c_50]) ).
tcf(c_6506,plain,
sdtpldt0(sz00,sK0(sz00,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6483,c_5137,c_49]) ).
tcf(c_6507,plain,
sdtpldt0(sz00,sK0(sz00,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6482,c_119,c_49]) ).
tcf(c_6508,plain,
sdtpldt0(sz00,sK0(sz00,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6481,c_118,c_49]) ).
tcf(c_6509,plain,
sdtpldt0(sz00,sK0(sz00,sz10)) = sz10,
inference(forward_subsumption_resolution,[status(thm)],[c_6480,c_50,c_49]) ).
tcf(c_6510,plain,
sdtpldt0(sz00,sK0(sz00,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6475,c_117,c_49]) ).
tcf(c_6519,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(sz10,sK0(sz10,iPr_def_10)) = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6490,c_5137,c_50]) ).
tcf(c_6522,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(xp,sK0(xp,iPr_def_10)) = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6486,c_5137,c_119]) ).
tcf(c_6525,plain,
sdtpldt0(xm,sK0(xm,sdtpldt0(sz10,xm))) = sdtpldt0(sz10,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_6493,c_118,c_6294]) ).
tcf(c_6526,plain,
sdtpldt0(xp,sK0(xp,sdtpldt0(sz10,xp))) = sdtpldt0(sz10,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_6492,c_119,c_6041]) ).
tcf(c_6527,plain,
sdtpldt0(xn,sK0(xn,sdtpldt0(sz10,xn))) = sdtpldt0(sz10,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_6491,c_117,c_6013]) ).
tcf(c_6528,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz10,sK0(sz10,X0)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6472,c_50]) ).
tcf(c_6570,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,sdtmndt0(sdtpldt0(X0,X1),X0)) = sdtpldt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_177,c_78]) ).
tcf(c_6571,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X1,X0)
| ( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_83,c_78]) ).
tcf(c_6572,plain,
! [X0: $i] :
( ( sdtpldt0(X0,sdtmndt0(X0,X0)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_82,c_78]) ).
tcf(c_6573,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ( sdtpldt0(X1,sdtmndt0(X0,X1)) = X0 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_83,c_78]) ).
tcf(c_6574,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz10,sdtmndt0(X0,sz10)) = X0 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_92,c_78]) ).
tcf(c_6575,plain,
! [X0: $i,X1: $i] :
( ( X1 = sz00 )
| ( sdtpldt0(X0,sdtmndt0(sdtasdt0(X0,X1),X0)) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_93,c_78]) ).
tcf(c_6576,plain,
( ( sdtpldt0(sz00,sdtmndt0(sz00,sz00)) = sz00 )
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5212,c_78]) ).
tcf(c_6577,plain,
( ( sdtpldt0(sz00,sdtmndt0(xn,sz00)) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5215,c_78]) ).
tcf(c_6578,plain,
( ( sdtpldt0(sz10,sdtmndt0(sz10,sz10)) = sz10 )
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5220,c_78]) ).
tcf(c_6579,plain,
( ( sdtpldt0(xn,sdtmndt0(xn,xn)) = xn )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5219,c_78]) ).
tcf(c_6580,plain,
( ( sdtpldt0(xm,sdtmndt0(xm,xm)) = xm )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm)],[c_5218,c_78]) ).
tcf(c_6581,plain,
( ( sdtpldt0(xp,sdtmndt0(xp,xp)) = xp )
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_5217,c_78]) ).
tcf(c_6582,plain,
( ( sdtpldt0(sz00,sdtmndt0(sz10,sz00)) = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5216,c_78]) ).
tcf(c_6583,plain,
( ( sdtpldt0(sz00,sdtmndt0(xm,sz00)) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5214,c_78]) ).
tcf(c_6584,plain,
( ( sdtpldt0(sz00,sdtmndt0(xp,sz00)) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5213,c_78]) ).
tcf(c_6585,plain,
( ( sdtpldt0(sz00,sdtmndt0(iPr_def_10,sz00)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5639,c_78]) ).
tcf(c_6586,plain,
( ( sdtpldt0(iPr_def_10,sdtmndt0(iPr_def_10,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_5642,c_78]) ).
tcf(c_6587,plain,
( ( sdtpldt0(sz10,sdtmndt0(xn,sz10)) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5901,c_78]) ).
tcf(c_6588,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(xp,sdtmndt0(iPr_def_10,xp)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_6249,c_78]) ).
tcf(c_6589,plain,
( ( sdtpldt0(xn,sdtmndt0(iPr_def_10,xn)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5895,c_78]) ).
tcf(c_6590,plain,
( ( sdtpldt0(sz10,sdtmndt0(xm,sz10)) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5900,c_78]) ).
tcf(c_6591,plain,
( ( sdtpldt0(sz10,sdtmndt0(xp,sz10)) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5899,c_78]) ).
tcf(c_6592,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(sz10,sdtmndt0(iPr_def_10,sz10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5896,c_78]) ).
tcf(c_6593,plain,
( ( sdtpldt0(xn,sdtmndt0(sdtpldt0(sz10,xn),xn)) = sdtpldt0(sz10,xn) )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6014,c_78]) ).
tcf(c_6594,plain,
( ( sdtpldt0(xp,sdtmndt0(sdtpldt0(sz10,xp),xp)) = sdtpldt0(sz10,xp) )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp)) ),
inference(superposition,[status(thm)],[c_6042,c_78]) ).
tcf(c_6595,plain,
( ( sdtpldt0(xm,sdtmndt0(sdtpldt0(sz10,xm),xm)) = sdtpldt0(sz10,xm) )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm)) ),
inference(superposition,[status(thm)],[c_6295,c_78]) ).
tcf(c_6596,plain,
sdtpldt0(iPr_def_10,sdtmndt0(iPr_def_10,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6586,c_5137]) ).
tcf(c_6597,plain,
sdtpldt0(xp,sdtmndt0(xp,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6581,c_119]) ).
tcf(c_6598,plain,
sdtpldt0(xm,sdtmndt0(xm,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6580,c_118]) ).
tcf(c_6599,plain,
sdtpldt0(xn,sdtmndt0(xn,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6579,c_117]) ).
tcf(c_6600,plain,
sdtpldt0(sz10,sdtmndt0(sz10,sz10)) = sz10,
inference(forward_subsumption_resolution,[status(thm)],[c_6578,c_50]) ).
tcf(c_6601,plain,
sdtpldt0(sz00,sdtmndt0(sz00,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6576,c_49]) ).
tcf(c_6604,plain,
sdtpldt0(sz10,sdtmndt0(xp,sz10)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6591,c_119,c_50]) ).
tcf(c_6605,plain,
sdtpldt0(sz10,sdtmndt0(xm,sz10)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6590,c_118,c_50]) ).
tcf(c_6606,plain,
sdtpldt0(xn,sdtmndt0(iPr_def_10,xn)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6589,c_5137,c_117]) ).
tcf(c_6607,plain,
sdtpldt0(sz10,sdtmndt0(xn,sz10)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6587,c_117,c_50]) ).
tcf(c_6608,plain,
sdtpldt0(sz00,sdtmndt0(iPr_def_10,sz00)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6585,c_5137,c_49]) ).
tcf(c_6609,plain,
sdtpldt0(sz00,sdtmndt0(xp,sz00)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6584,c_119,c_49]) ).
tcf(c_6610,plain,
sdtpldt0(sz00,sdtmndt0(xm,sz00)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6583,c_118,c_49]) ).
tcf(c_6611,plain,
sdtpldt0(sz00,sdtmndt0(sz10,sz00)) = sz10,
inference(forward_subsumption_resolution,[status(thm)],[c_6582,c_50,c_49]) ).
tcf(c_6612,plain,
sdtpldt0(sz00,sdtmndt0(xn,sz00)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6577,c_117,c_49]) ).
tcf(c_6621,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(sz10,sdtmndt0(iPr_def_10,sz10)) = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6592,c_5137,c_50]) ).
tcf(c_6624,plain,
( ( sz00 = iPr_def_10 )
| ( sdtpldt0(xp,sdtmndt0(iPr_def_10,xp)) = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6588,c_5137,c_119]) ).
tcf(c_6627,plain,
sdtpldt0(xm,sdtmndt0(sdtpldt0(sz10,xm),xm)) = sdtpldt0(sz10,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_6595,c_118,c_6294]) ).
tcf(c_6628,plain,
sdtpldt0(xp,sdtmndt0(sdtpldt0(sz10,xp),xp)) = sdtpldt0(sz10,xp),
inference(forward_subsumption_resolution,[status(thm)],[c_6594,c_119,c_6041]) ).
tcf(c_6629,plain,
sdtpldt0(xn,sdtmndt0(sdtpldt0(sz10,xn),xn)) = sdtpldt0(sz10,xn),
inference(forward_subsumption_resolution,[status(thm)],[c_6593,c_117,c_6013]) ).
tcf(c_6630,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sz10,sdtmndt0(X0,sz10)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6574,c_50]) ).
tcf(c_6712,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(X0,X1) = X0 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ sdtlseqdt0(sdtpldt0(X0,X1),X0) ),
inference(superposition,[status(thm)],[c_177,c_80]) ).
tcf(c_6716,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz10) ),
inference(superposition,[status(thm)],[c_92,c_80]) ).
tcf(c_6717,plain,
! [X0: $i,X1: $i] :
( ( X1 = sz00 )
| ( sdtasdt0(X0,X1) = X0 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(sdtasdt0(X0,X1),X0) ),
inference(superposition,[status(thm)],[c_93,c_80]) ).
tcf(c_6719,plain,
( ( sz00 = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(xn,sz00) ),
inference(superposition,[status(thm)],[c_5215,c_80]) ).
tcf(c_6724,plain,
( ( sz00 = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(sz10,sz00) ),
inference(superposition,[status(thm)],[c_5216,c_80]) ).
tcf(c_6725,plain,
( ( sz00 = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(xm,sz00) ),
inference(superposition,[status(thm)],[c_5214,c_80]) ).
tcf(c_6726,plain,
( ( sz00 = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(xp,sz00) ),
inference(superposition,[status(thm)],[c_5213,c_80]) ).
tcf(c_6727,plain,
( ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(iPr_def_10,sz00) ),
inference(superposition,[status(thm)],[c_5639,c_80]) ).
tcf(c_6729,plain,
( ( sz10 = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10)
| ~ sdtlseqdt0(xn,sz10) ),
inference(superposition,[status(thm)],[c_5901,c_80]) ).
tcf(c_6730,plain,
( ( xp = iPr_def_10 )
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(iPr_def_10,xp) ),
inference(superposition,[status(thm)],[c_6249,c_80]) ).
tcf(c_6731,plain,
( ( xn = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn)
| ~ sdtlseqdt0(iPr_def_10,xn) ),
inference(superposition,[status(thm)],[c_5895,c_80]) ).
tcf(c_6732,plain,
( ( sz10 = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10)
| ~ sdtlseqdt0(xm,sz10) ),
inference(superposition,[status(thm)],[c_5900,c_80]) ).
tcf(c_6733,plain,
( ( sz10 = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ sdtlseqdt0(xp,sz10) ),
inference(superposition,[status(thm)],[c_5899,c_80]) ).
tcf(c_6734,plain,
( ( sz10 = iPr_def_10 )
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10)
| ~ sdtlseqdt0(iPr_def_10,sz10) ),
inference(superposition,[status(thm)],[c_5896,c_80]) ).
tcf(c_6735,plain,
( ( sdtpldt0(sz10,xn) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn))
| ~ sdtlseqdt0(sdtpldt0(sz10,xn),xn) ),
inference(superposition,[status(thm)],[c_6014,c_80]) ).
tcf(c_6736,plain,
( ( sdtpldt0(sz10,xp) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp))
| ~ sdtlseqdt0(sdtpldt0(sz10,xp),xp) ),
inference(superposition,[status(thm)],[c_6042,c_80]) ).
tcf(c_6737,plain,
( ( sdtpldt0(sz10,xm) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm))
| ~ sdtlseqdt0(sdtpldt0(sz10,xm),xm) ),
inference(superposition,[status(thm)],[c_6295,c_80]) ).
tcf(c_6738,plain,
( ( sz10 = xp )
| ~ sdtlseqdt0(xp,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6733,c_119,c_50]) ).
tcf(c_6741,plain,
( ( sz10 = xm )
| ~ sdtlseqdt0(xm,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6732,c_118,c_50]) ).
tcf(c_6744,plain,
( ( xn = iPr_def_10 )
| ~ sdtlseqdt0(iPr_def_10,xn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6731,c_5137,c_117]) ).
tcf(c_6747,plain,
( ( sz10 = xn )
| ~ sdtlseqdt0(xn,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6729,c_117,c_50]) ).
tcf(c_6750,plain,
( ( sz00 = iPr_def_10 )
| ~ sdtlseqdt0(iPr_def_10,sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6727,c_5137,c_49]) ).
tcf(c_6753,plain,
~ sdtlseqdt0(xp,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6726,c_122,c_119,c_49]) ).
tcf(c_6754,plain,
~ sdtlseqdt0(xm,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6725,c_121,c_118,c_49]) ).
tcf(c_6755,plain,
~ sdtlseqdt0(sz10,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6724,c_51,c_50,c_49]) ).
tcf(c_6756,plain,
~ sdtlseqdt0(xn,sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6719,c_120,c_117,c_49]) ).
tcf(c_6757,plain,
( ( sz10 = iPr_def_10 )
| ( sz00 = iPr_def_10 )
| ~ sdtlseqdt0(iPr_def_10,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6734,c_5137,c_50]) ).
tcf(c_6761,plain,
( ( xp = iPr_def_10 )
| ( sz00 = iPr_def_10 )
| ~ sdtlseqdt0(iPr_def_10,xp) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6730,c_5137,c_119]) ).
tcf(c_6765,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6716,c_50]) ).
tcf(c_6770,plain,
( ( sdtpldt0(sz10,xm) = xm )
| ~ sdtlseqdt0(sdtpldt0(sz10,xm),xm) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6737,c_118,c_6294]) ).
tcf(c_6773,plain,
( ( sdtpldt0(sz10,xp) = xp )
| ~ sdtlseqdt0(sdtpldt0(sz10,xp),xp) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6736,c_119,c_6041]) ).
tcf(c_6776,plain,
( ( sdtpldt0(sz10,xn) = xn )
| ~ sdtlseqdt0(sdtpldt0(sz10,xn),xn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6735,c_117,c_6013]) ).
tcf(c_6823,plain,
( ( sdtpldt0(iPr_def_10,sz10) = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10))
| ~ sdtlseqdt0(sdtpldt0(iPr_def_10,sz10),sz10) ),
inference(superposition,[status(thm)],[c_6339,c_80]) ).
tcf(c_6824,plain,
( ( sdtpldt0(sz10,sdtmndt0(sdtpldt0(iPr_def_10,sz10),sz10)) = sdtpldt0(iPr_def_10,sz10) )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)) ),
inference(superposition,[status(thm)],[c_6339,c_78]) ).
tcf(c_6825,plain,
( ( sdtpldt0(sz10,sK0(sz10,sdtpldt0(iPr_def_10,sz10))) = sdtpldt0(iPr_def_10,sz10) )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)) ),
inference(superposition,[status(thm)],[c_6339,c_75]) ).
tcf(c_6826,plain,
sdtpldt0(sz10,sK0(sz10,sdtpldt0(iPr_def_10,sz10))) = sdtpldt0(iPr_def_10,sz10),
inference(forward_subsumption_resolution,[status(thm)],[c_6825,c_50,c_6338]) ).
tcf(c_6827,plain,
sdtpldt0(sz10,sdtmndt0(sdtpldt0(iPr_def_10,sz10),sz10)) = sdtpldt0(iPr_def_10,sz10),
inference(forward_subsumption_resolution,[status(thm)],[c_6824,c_50,c_6338]) ).
tcf(c_6828,plain,
( ( sdtpldt0(iPr_def_10,sz10) = sz10 )
| ~ sdtlseqdt0(sdtpldt0(iPr_def_10,sz10),sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6823,c_50,c_6338]) ).
tcf(c_6831,plain,
sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sz10) = sdtpldt0(sz10,sdtpldt0(sz10,sdtpldt0(sz10,xn))),
inference(superposition,[status(thm)],[c_6440,c_5244]) ).
tcf(c_6832,plain,
sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sz00) = sdtpldt0(sz00,sdtpldt0(sz10,sdtpldt0(sz10,xn))),
inference(superposition,[status(thm)],[c_6440,c_5243]) ).
tcf(c_6833,plain,
! [X0: $i] :
( ( sdtmndt0(sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0),sdtpldt0(sz10,sdtpldt0(sz10,xn))) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_180]) ).
tcf(c_6834,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0),X1) = sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_59]) ).
tcf(c_6835,plain,
! [X0: $i] :
( ( sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0) = sdtasdt0(X0,sdtpldt0(sz10,sdtpldt0(sz10,xn))) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_58]) ).
tcf(c_6836,plain,
! [X0: $i] :
( ( sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0) = sdtpldt0(X0,sdtpldt0(sz10,sdtpldt0(sz10,xn))) )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_54]) ).
tcf(c_6837,plain,
sdtasdt0(sz00,sdtpldt0(sz10,sdtpldt0(sz10,xn))) = sz00,
inference(superposition,[status(thm)],[c_6440,c_63]) ).
tcf(c_6838,plain,
sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sz00) = sz00,
inference(superposition,[status(thm)],[c_6440,c_62]) ).
tcf(c_6839,plain,
sdtasdt0(sz10,sdtpldt0(sz10,sdtpldt0(sz10,xn))) = sdtpldt0(sz10,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6440,c_61]) ).
tcf(c_6840,plain,
sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sz10) = sdtpldt0(sz10,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6440,c_60]) ).
tcf(c_6841,plain,
sdtpldt0(sz00,sdtpldt0(sz10,sdtpldt0(sz10,xn))) = sdtpldt0(sz10,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6440,c_57]) ).
tcf(c_6842,plain,
sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sz00) = sdtpldt0(sz10,sdtpldt0(sz10,xn)),
inference(superposition,[status(thm)],[c_6440,c_56]) ).
tcf(c_6912,plain,
( doDivides0(sdtpldt0(sz10,xn),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6022,c_174]) ).
tcf(c_6915,plain,
doDivides0(sdtpldt0(sz10,xn),sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6912,c_49,c_6013]) ).
tcf(c_6935,plain,
( doDivides0(sdtpldt0(sz10,xp),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp)) ),
inference(superposition,[status(thm)],[c_6269,c_174]) ).
tcf(c_6938,plain,
doDivides0(sdtpldt0(sz10,xp),sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_6935,c_49,c_6041]) ).
tcf(c_6948,plain,
! [X0: $i,X1: $i] :
( ( sdtasdt0(X0,sK1(X0,sdtasdt0(X0,X1))) = sdtasdt0(X0,X1) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(superposition,[status(thm)],[c_174,c_97]) ).
tcf(c_6949,plain,
! [X0: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK2(X0),sK1(sK2(X0),X0)) = X0 )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK2(X0)) ),
inference(superposition,[status(thm)],[c_109,c_97]) ).
tcf(c_6950,plain,
! [X0: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtasdt0(sK3(X0),sK1(sK3(X0),X0)) = X0 )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3(X0)) ),
inference(superposition,[status(thm)],[c_114,c_97]) ).
tcf(c_6951,plain,
( ( sdtasdt0(sz00,sK1(sz00,sz00)) = sz00 )
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5183,c_97]) ).
tcf(c_6952,plain,
( ( sdtasdt0(xp,sK1(xp,sz00)) = sz00 )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5402,c_97]) ).
tcf(c_6953,plain,
( ( sdtasdt0(xp,sK1(xp,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_5923,c_97]) ).
tcf(c_6954,plain,
( ( sdtasdt0(xn,sK1(xn,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5184,c_97]) ).
tcf(c_6955,plain,
( ( sdtasdt0(sz10,sK1(sz10,sz00)) = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5193,c_97]) ).
tcf(c_6956,plain,
( ( sdtasdt0(sz10,sK1(sz10,sz10)) = sz10 )
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5182,c_97]) ).
tcf(c_6957,plain,
( ( sdtasdt0(xn,sK1(xn,xn)) = xn )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm)],[c_5192,c_97]) ).
tcf(c_6958,plain,
( ( sdtasdt0(xm,sK1(xm,xm)) = xm )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm)],[c_5191,c_97]) ).
tcf(c_6959,plain,
( ( sdtasdt0(xp,sK1(xp,xp)) = xp )
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm)],[c_5190,c_97]) ).
tcf(c_6960,plain,
( ( sdtasdt0(sz10,sK1(sz10,xn)) = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5189,c_97]) ).
tcf(c_6961,plain,
( ( sdtasdt0(sz10,sK1(sz10,xm)) = xm )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5188,c_97]) ).
tcf(c_6962,plain,
( ( sdtasdt0(sz10,sK1(sz10,xp)) = xp )
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5187,c_97]) ).
tcf(c_6963,plain,
( ( sdtasdt0(xn,sK1(xn,sz00)) = sz00 )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5186,c_97]) ).
tcf(c_6964,plain,
( ( sdtasdt0(xm,sK1(xm,sz00)) = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5185,c_97]) ).
tcf(c_6965,plain,
( ( sdtasdt0(iPr_def_10,sK1(iPr_def_10,sz00)) = sz00 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm)],[c_5618,c_97]) ).
tcf(c_6966,plain,
( ( sdtasdt0(sz10,sK1(sz10,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm)],[c_5621,c_97]) ).
tcf(c_6967,plain,
( ( sdtasdt0(iPr_def_10,sK1(iPr_def_10,iPr_def_10)) = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_5624,c_97]) ).
tcf(c_6968,plain,
( ( sdtasdt0(sdtpldt0(sz10,xn),sK1(sdtpldt0(sz10,xn),sz00)) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6915,c_97]) ).
tcf(c_6969,plain,
( ( sdtasdt0(sdtpldt0(sz10,xp),sK1(sdtpldt0(sz10,xp),sz00)) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp)) ),
inference(superposition,[status(thm)],[c_6938,c_97]) ).
tcf(c_6970,plain,
sdtasdt0(iPr_def_10,sK1(iPr_def_10,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6967,c_5137]) ).
tcf(c_6971,plain,
sdtasdt0(xp,sK1(xp,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6959,c_119]) ).
tcf(c_6972,plain,
sdtasdt0(xm,sK1(xm,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6958,c_118]) ).
tcf(c_6973,plain,
sdtasdt0(xn,sK1(xn,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6957,c_117]) ).
tcf(c_6974,plain,
sdtasdt0(sz10,sK1(sz10,sz10)) = sz10,
inference(forward_subsumption_resolution,[status(thm)],[c_6956,c_50]) ).
tcf(c_6975,plain,
sdtasdt0(sz00,sK1(sz00,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6951,c_49]) ).
tcf(c_6976,plain,
sdtasdt0(sz10,sK1(sz10,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6966,c_5137,c_50]) ).
tcf(c_6977,plain,
sdtasdt0(iPr_def_10,sK1(iPr_def_10,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6965,c_5137,c_49]) ).
tcf(c_6978,plain,
sdtasdt0(xm,sK1(xm,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6964,c_118,c_49]) ).
tcf(c_6979,plain,
sdtasdt0(xn,sK1(xn,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6963,c_117,c_49]) ).
tcf(c_6980,plain,
sdtasdt0(sz10,sK1(sz10,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[c_6962,c_119,c_50]) ).
tcf(c_6981,plain,
sdtasdt0(sz10,sK1(sz10,xm)) = xm,
inference(forward_subsumption_resolution,[status(thm)],[c_6961,c_118,c_50]) ).
tcf(c_6982,plain,
sdtasdt0(sz10,sK1(sz10,xn)) = xn,
inference(forward_subsumption_resolution,[status(thm)],[c_6960,c_117,c_50]) ).
tcf(c_6983,plain,
sdtasdt0(sz10,sK1(sz10,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6955,c_50,c_49]) ).
tcf(c_6984,plain,
sdtasdt0(xn,sK1(xn,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6954,c_5137,c_117]) ).
tcf(c_6985,plain,
sdtasdt0(xp,sK1(xp,iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6953,c_5137,c_119]) ).
tcf(c_6986,plain,
sdtasdt0(xp,sK1(xp,sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6952,c_119,c_49]) ).
tcf(c_6987,plain,
sdtasdt0(sdtpldt0(sz10,xp),sK1(sdtpldt0(sz10,xp),sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6969,c_49,c_6041]) ).
tcf(c_6988,plain,
sdtasdt0(sdtpldt0(sz10,xn),sK1(sdtpldt0(sz10,xn),sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_6968,c_49,c_6013]) ).
tcf(c_7075,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sdtsldt0(X1,X0),sz10) = sdtpldt0(sz10,sdtsldt0(X1,X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_5244]) ).
tcf(c_7076,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sdtsldt0(X1,X0),sz00) = sdtpldt0(sz00,sdtsldt0(X1,X0)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_5243]) ).
tcf(c_7077,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz00 )
| ( sdtmndt0(sdtpldt0(sdtsldt0(X1,X0),X2),sdtsldt0(X1,X0)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_180]) ).
tcf(c_7078,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sdtasdt0(sdtsldt0(X1,X0),X2),X3) = sdtasdt0(sdtsldt0(X1,X0),sdtasdt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_59]) ).
tcf(c_7079,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sdtsldt0(X1,X0),X2) = sdtasdt0(X2,sdtsldt0(X1,X0)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_58]) ).
tcf(c_7080,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sdtsldt0(X1,X0),X2) = sdtpldt0(X2,sdtsldt0(X1,X0)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_54]) ).
tcf(c_7081,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sz00,sdtsldt0(X1,X0)) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_63]) ).
tcf(c_7082,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sdtsldt0(X1,X0),sz00) = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_62]) ).
tcf(c_7083,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sz10,sdtsldt0(X1,X0)) = sdtsldt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_61]) ).
tcf(c_7084,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sdtsldt0(X1,X0),sz10) = sdtsldt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_60]) ).
tcf(c_7085,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sz00,sdtsldt0(X1,X0)) = sdtsldt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_57]) ).
tcf(c_7086,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sdtsldt0(X1,X0),sz00) = sdtsldt0(X1,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_56]) ).
tcf(c_7191,plain,
! [X0: $i] :
( ( sz00 = sz10 )
| ( sdtsldt0(sdtasdt0(sz10,X0),sz10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_187]) ).
tcf(c_7192,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtpldt0(X0,X1) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(X0,X1),X2),sdtpldt0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_187]) ).
tcf(c_7193,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtasdt0(X0,X1) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtasdt0(X0,X1),X2),sdtasdt0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_187]) ).
tcf(c_7194,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK0(X0,X1) = sz00 )
| ( sdtsldt0(sdtasdt0(sK0(X0,X1),X2),sK0(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_187]) ).
tcf(c_7195,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtmndt0(X1,X0) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtmndt0(X1,X0),X2),sdtmndt0(X1,X0)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_187]) ).
tcf(c_7196,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X0,X1) = sz00 )
| ( sdtsldt0(sdtasdt0(sK1(X0,X1),X2),sK1(X0,X1)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_187]) ).
tcf(c_7197,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz00 )
| ( sdtsldt0(X1,X0) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtsldt0(X1,X0),X2),sdtsldt0(X1,X0)) = X2 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_187]) ).
tcf(c_7198,plain,
! [X0: $i,X1: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sK2(X0) = sz00 )
| ( sdtsldt0(sdtasdt0(sK2(X0),X1),sK2(X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_187]) ).
tcf(c_7199,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sK3(X0) = sz00 )
| ( sdtsldt0(sdtasdt0(sK3(X0),X1),sK3(X0)) = X1 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_187]) ).
tcf(c_7200,plain,
! [X0: $i] :
( ( sz00 = xn )
| ( sdtsldt0(sdtasdt0(xn,X0),xn) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_187]) ).
tcf(c_7201,plain,
! [X0: $i] :
( ( sz00 = xm )
| ( sdtsldt0(sdtasdt0(xm,X0),xm) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_187]) ).
tcf(c_7202,plain,
! [X0: $i] :
( ( sz00 = xp )
| ( sdtsldt0(sdtasdt0(xp,X0),xp) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_187]) ).
tcf(c_7203,plain,
! [X0: $i] :
( ( sz00 = iPr_def_10 )
| ( sdtsldt0(sdtasdt0(iPr_def_10,X0),iPr_def_10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_187]) ).
tcf(c_7204,plain,
! [X0: $i] :
( ( sdtpldt0(sz10,xn) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xn),X0),sdtpldt0(sz10,xn)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_187]) ).
tcf(c_7205,plain,
! [X0: $i] :
( ( sdtpldt0(sz10,xp) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xp),X0),sdtpldt0(sz10,xp)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_187]) ).
tcf(c_7206,plain,
! [X0: $i] :
( ( sdtpldt0(sz10,xm) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xm),X0),sdtpldt0(sz10,xm)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_187]) ).
tcf(c_7207,plain,
! [X0: $i] :
( ( sdtpldt0(iPr_def_10,sz10) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(iPr_def_10,sz10),X0),sdtpldt0(iPr_def_10,sz10)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_187]) ).
tcf(c_7208,plain,
! [X0: $i] :
( ( sdtpldt0(sz10,sdtpldt0(sz10,xn)) = sz00 )
| ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0),sdtpldt0(sz10,sdtpldt0(sz10,xn))) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_187]) ).
tcf(c_7212,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(xp,X0),xp) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7202,c_122]) ).
tcf(c_7215,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(xm,X0),xm) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7201,c_121]) ).
tcf(c_7218,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(xn,X0),xn) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7200,c_120]) ).
tcf(c_7221,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(sz10,X0),sz10) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7191,c_51]) ).
tcf(c_7224,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(sdtpldt0(iPr_def_10,sz10),X0),sdtpldt0(iPr_def_10,sz10)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7207,c_6340]) ).
tcf(c_7227,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xm),X0),sdtpldt0(sz10,xm)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7206,c_6296]) ).
tcf(c_7230,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xp),X0),sdtpldt0(sz10,xp)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7205,c_6197]) ).
tcf(c_7233,plain,
! [X0: $i] :
( ( sdtsldt0(sdtasdt0(sdtpldt0(sz10,xn),X0),sdtpldt0(sz10,xn)) = X0 )
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7204,c_6198]) ).
tcf(c_7363,plain,
( doDivides0(sdtpldt0(sz10,xm),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm)) ),
inference(superposition,[status(thm)],[c_6304,c_174]) ).
tcf(c_7366,plain,
doDivides0(sdtpldt0(sz10,xm),sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_7363,c_49,c_6294]) ).
tcf(c_7367,plain,
( ( sdtasdt0(sdtpldt0(sz10,xm),sK1(sdtpldt0(sz10,xm),sz00)) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm)) ),
inference(superposition,[status(thm)],[c_7366,c_97]) ).
tcf(c_7369,plain,
sdtasdt0(sdtpldt0(sz10,xm),sK1(sdtpldt0(sz10,xm),sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_7367,c_49,c_6294]) ).
tcf(c_7373,plain,
( doDivides0(sdtpldt0(iPr_def_10,sz10),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)) ),
inference(superposition,[status(thm)],[c_6380,c_174]) ).
tcf(c_7376,plain,
doDivides0(sdtpldt0(iPr_def_10,sz10),sz00),
inference(forward_subsumption_resolution,[status(thm)],[c_7373,c_49,c_6338]) ).
tcf(c_7377,plain,
( ( sdtasdt0(sdtpldt0(iPr_def_10,sz10),sK1(sdtpldt0(iPr_def_10,sz10),sz00)) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)) ),
inference(superposition,[status(thm)],[c_7376,c_97]) ).
tcf(c_7379,plain,
sdtasdt0(sdtpldt0(iPr_def_10,sz10),sK1(sdtpldt0(iPr_def_10,sz10),sz00)) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[c_7377,c_49,c_6338]) ).
tcf(c_7380,plain,
( ( sK0(iPr_def_10,iPr_def_10) = sz00 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sK0(iPr_def_10,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_6494,c_71]) ).
tcf(c_7384,plain,
( ( sK0(iPr_def_10,iPr_def_10) = sz00 )
| ~ aNaturalNumber0(sK0(iPr_def_10,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7380,c_5137]) ).
tcf(c_7404,plain,
( ( sK0(sz00,sz00) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sK0(sz00,sz00)) ),
inference(superposition,[status(thm)],[c_6499,c_71]) ).
tcf(c_7408,plain,
( ( sK0(sz00,sz00) = sz00 )
| ~ aNaturalNumber0(sK0(sz00,sz00)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7404,c_49]) ).
tcf(c_7449,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ sdtlseqdt0(sdtpldt0(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_177,c_81]) ).
tcf(c_7452,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(X2,X1)
| sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_83,c_81]) ).
tcf(c_7453,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(sz10,X1)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_92,c_81]) ).
tcf(c_7454,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(X0,X2)
| ( X1 = sz00 )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(sdtasdt0(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_93,c_81]) ).
tcf(c_7456,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xn,X0) ),
inference(superposition,[status(thm)],[c_5215,c_81]) ).
tcf(c_7461,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sz10,X0) ),
inference(superposition,[status(thm)],[c_5216,c_81]) ).
tcf(c_7462,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xm,X0) ),
inference(superposition,[status(thm)],[c_5214,c_81]) ).
tcf(c_7463,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xp,X0) ),
inference(superposition,[status(thm)],[c_5213,c_81]) ).
tcf(c_7464,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5639,c_81]) ).
tcf(c_7466,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xn,X0) ),
inference(superposition,[status(thm)],[c_5901,c_81]) ).
tcf(c_7467,plain,
! [X0: $i] :
( sdtlseqdt0(xp,X0)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_6249,c_81]) ).
tcf(c_7468,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5895,c_81]) ).
tcf(c_7469,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xm,X0) ),
inference(superposition,[status(thm)],[c_5900,c_81]) ).
tcf(c_7470,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xp,X0) ),
inference(superposition,[status(thm)],[c_5899,c_81]) ).
tcf(c_7471,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5896,c_81]) ).
tcf(c_7472,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn))
| ~ sdtlseqdt0(sdtpldt0(sz10,xn),X0) ),
inference(superposition,[status(thm)],[c_6014,c_81]) ).
tcf(c_7473,plain,
! [X0: $i] :
( sdtlseqdt0(xp,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp))
| ~ sdtlseqdt0(sdtpldt0(sz10,xp),X0) ),
inference(superposition,[status(thm)],[c_6042,c_81]) ).
tcf(c_7474,plain,
! [X0: $i] :
( sdtlseqdt0(xm,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm))
| ~ sdtlseqdt0(sdtpldt0(sz10,xm),X0) ),
inference(superposition,[status(thm)],[c_6295,c_81]) ).
tcf(c_7475,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10))
| ~ sdtlseqdt0(sdtpldt0(iPr_def_10,sz10),X0) ),
inference(superposition,[status(thm)],[c_6339,c_81]) ).
tcf(c_7476,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xp,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7470,c_119,c_50]) ).
tcf(c_7480,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xm,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7469,c_118,c_50]) ).
tcf(c_7484,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7468,c_5137,c_117]) ).
tcf(c_7488,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xn,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7466,c_117,c_50]) ).
tcf(c_7492,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7464,c_5137,c_49]) ).
tcf(c_7496,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xp,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7463,c_119,c_49]) ).
tcf(c_7500,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xm,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7462,c_118,c_49]) ).
tcf(c_7504,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sz10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7461,c_50,c_49]) ).
tcf(c_7508,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xn,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7456,c_117,c_49]) ).
tcf(c_7518,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sdtpldt0(iPr_def_10,sz10),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7475,c_50,c_6338]) ).
tcf(c_7522,plain,
! [X0: $i] :
( sdtlseqdt0(xm,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sdtpldt0(sz10,xm),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7474,c_118,c_6294]) ).
tcf(c_7526,plain,
! [X0: $i] :
( sdtlseqdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sdtpldt0(sz10,xp),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7473,c_119,c_6041]) ).
tcf(c_7530,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(sdtpldt0(sz10,xn),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7472,c_117,c_6013]) ).
tcf(c_7534,plain,
! [X0: $i] :
( sdtlseqdt0(sz10,X0)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7471,c_5137,c_50]) ).
tcf(c_7539,plain,
! [X0: $i] :
( sdtlseqdt0(xp,X0)
| ( sz00 = iPr_def_10 )
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7467,c_5137,c_119]) ).
tcf(c_7550,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(sz10,X1)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7453,c_50]) ).
tcf(c_7617,plain,
! [X0: $i,X1: $i,X2: $i] :
( doDivides0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ doDivides0(sdtasdt0(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_174,c_101]) ).
tcf(c_7618,plain,
! [X0: $i,X1: $i] :
( isPrime0(X0)
| doDivides0(sK2(X0),X1)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK2(X0))
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_109,c_101]) ).
tcf(c_7619,plain,
! [X0: $i,X1: $i] :
( doDivides0(sK3(X0),X1)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3(X0))
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_114,c_101]) ).
tcf(c_7621,plain,
! [X0: $i] :
( doDivides0(xp,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(superposition,[status(thm)],[c_5402,c_101]) ).
tcf(c_7622,plain,
! [X0: $i] :
( doDivides0(xp,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5923,c_101]) ).
tcf(c_7623,plain,
! [X0: $i] :
( doDivides0(xn,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5184,c_101]) ).
tcf(c_7624,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(superposition,[status(thm)],[c_5193,c_101]) ).
tcf(c_7629,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xn,X0) ),
inference(superposition,[status(thm)],[c_5189,c_101]) ).
tcf(c_7630,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xm,X0) ),
inference(superposition,[status(thm)],[c_5188,c_101]) ).
tcf(c_7631,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,X0) ),
inference(superposition,[status(thm)],[c_5187,c_101]) ).
tcf(c_7632,plain,
! [X0: $i] :
( doDivides0(xn,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(superposition,[status(thm)],[c_5186,c_101]) ).
tcf(c_7633,plain,
! [X0: $i] :
( doDivides0(xm,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(superposition,[status(thm)],[c_5185,c_101]) ).
tcf(c_7634,plain,
! [X0: $i] :
( doDivides0(iPr_def_10,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(superposition,[status(thm)],[c_5618,c_101]) ).
tcf(c_7635,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(iPr_def_10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_5621,c_101]) ).
tcf(c_7637,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xn),X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xn)) ),
inference(superposition,[status(thm)],[c_6915,c_101]) ).
tcf(c_7638,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xp),X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xp)) ),
inference(superposition,[status(thm)],[c_6938,c_101]) ).
tcf(c_7639,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xm),X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(sz10,xm)) ),
inference(superposition,[status(thm)],[c_7366,c_101]) ).
tcf(c_7640,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(iPr_def_10,sz10),X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(iPr_def_10,sz10)) ),
inference(superposition,[status(thm)],[c_7376,c_101]) ).
tcf(c_7641,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7635,c_5137,c_50]) ).
tcf(c_7645,plain,
! [X0: $i] :
( doDivides0(iPr_def_10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7634,c_5137,c_49]) ).
tcf(c_7649,plain,
! [X0: $i] :
( doDivides0(xm,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7633,c_118,c_49]) ).
tcf(c_7653,plain,
! [X0: $i] :
( doDivides0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7632,c_117,c_49]) ).
tcf(c_7657,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7631,c_119,c_50]) ).
tcf(c_7661,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xm,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7630,c_118,c_50]) ).
tcf(c_7665,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xn,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7629,c_117,c_50]) ).
tcf(c_7669,plain,
! [X0: $i] :
( doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7624,c_50,c_49]) ).
tcf(c_7673,plain,
! [X0: $i] :
( doDivides0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7623,c_5137,c_117]) ).
tcf(c_7677,plain,
! [X0: $i] :
( doDivides0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(iPr_def_10,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7622,c_5137,c_119]) ).
tcf(c_7681,plain,
! [X0: $i] :
( doDivides0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7621,c_119,c_49]) ).
tcf(c_7685,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(iPr_def_10,sz10),X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7640,c_49,c_6338]) ).
tcf(c_7689,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xm),X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7639,c_49,c_6294]) ).
tcf(c_7693,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xp),X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7638,c_49,c_6041]) ).
tcf(c_7697,plain,
! [X0: $i] :
( doDivides0(sdtpldt0(sz10,xn),X0)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(sz00,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7637,c_49,c_6013]) ).
tcf(c_7730,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sz00,X0),X1) = sdtpldt0(sz00,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_49,c_55]) ).
tcf(c_7731,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sz10,X0),X1) = sdtpldt0(sz10,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_50,c_55]) ).
tcf(c_7732,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(X0,X1),X2),X3) = sdtpldt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_52,c_55]) ).
tcf(c_7733,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtpldt0(sdtpldt0(sdtasdt0(X0,X1),X2),X3) = sdtpldt0(sdtasdt0(X0,X1),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_53,c_55]) ).
tcf(c_7734,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtpldt0(sdtpldt0(sK0(X0,X1),X2),X3) = sdtpldt0(sK0(X0,X1),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_74,c_55]) ).
tcf(c_7735,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtpldt0(sdtpldt0(sdtmndt0(X1,X0),X2),X3) = sdtpldt0(sdtmndt0(X1,X0),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_55]) ).
tcf(c_7736,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sdtpldt0(sdtpldt0(sK1(X0,X1),X2),X3) = sdtpldt0(sK1(X0,X1),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_96,c_55]) ).
tcf(c_7737,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = sz00 )
| ( sdtpldt0(sdtpldt0(sdtsldt0(X1,X0),X2),X3) = sdtpldt0(sdtsldt0(X1,X0),sdtpldt0(X2,X3)) )
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1) ),
inference(superposition,[status(thm)],[c_99,c_55]) ).
tcf(c_7738,plain,
! [X0: $i,X1: $i,X2: $i] :
( isPrime0(X0)
| ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sdtpldt0(sK2(X0),X1),X2) = sdtpldt0(sK2(X0),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_108,c_55]) ).
tcf(c_7739,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sz10 )
| ( X0 = sz00 )
| ( sdtpldt0(sdtpldt0(sK3(X0),X1),X2) = sdtpldt0(sK3(X0),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_113,c_55]) ).
tcf(c_7740,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(xn,X0),X1) = sdtpldt0(xn,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_117,c_55]) ).
tcf(c_7741,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(xm,X0),X1) = sdtpldt0(xm,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_118,c_55]) ).
tcf(c_7742,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(xp,X0),X1) = sdtpldt0(xp,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_119,c_55]) ).
tcf(c_7743,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(iPr_def_10,X0),X1) = sdtpldt0(iPr_def_10,sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_5137,c_55]) ).
tcf(c_7744,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(sz10,xn),X0),X1) = sdtpldt0(sdtpldt0(sz10,xn),sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6013,c_55]) ).
tcf(c_7745,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(sz10,xp),X0),X1) = sdtpldt0(sdtpldt0(sz10,xp),sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6041,c_55]) ).
tcf(c_7746,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(sz10,xm),X0),X1) = sdtpldt0(sdtpldt0(sz10,xm),sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6294,c_55]) ).
tcf(c_7747,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(iPr_def_10,sz10),X0),X1) = sdtpldt0(sdtpldt0(iPr_def_10,sz10),sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6338,c_55]) ).
tcf(c_7748,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),X0),X1) = sdtpldt0(sdtpldt0(sz10,sdtpldt0(sz10,xn)),sdtpldt0(X0,X1)) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(superposition,[status(thm)],[c_6440,c_55]) ).
tcf(c_7886,plain,
( ( sz00 = xn )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sK0(xn,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_6504,c_70]) ).
tcf(c_7889,plain,
( ~ aNaturalNumber0(sK0(xn,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7886,c_120,c_117]) ).
tcf(c_7896,plain,
( ( sK0(sz00,iPr_def_10) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sK0(sz00,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_6506,c_71]) ).
tcf(c_7900,plain,
( ( sK0(sz00,iPr_def_10) = sz00 )
| ~ aNaturalNumber0(sK0(sz00,iPr_def_10))
| ( sz00 != iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7896,c_49]) ).
tcf(c_7916,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_7900,c_7896,c_7889,c_7886,c_7748,c_7747,c_7746,c_7745,c_7744,c_7743,c_7742,c_7741,c_7740,c_7739,c_7738,c_7737,c_7736,c_7735,c_7734,c_7733,c_7732,c_7731,c_7730,c_7697,c_7693,c_7689,c_7685,c_7681,c_7677,c_7673,c_7669,c_7665,c_7661,c_7657,c_7653,c_7649,c_7645,c_7641,c_7640,c_7639,c_7638,c_7637,c_7635,c_7634,c_7633,c_7632,c_7631,c_7630,c_7629,c_7624,c_7623,c_7622,c_7621,c_7619,c_7618,c_7617,c_7550,c_7539,c_7534,c_7530,c_7526,c_7522,c_7518,c_7508,c_7504,c_7500,c_7496,c_7492,c_7488,c_7484,c_7480,c_7476,c_7475,c_7474,c_7473,c_7472,c_7471,c_7470,c_7469,c_7468,c_7467,c_7466,c_7464,c_7463,c_7462,c_7461,c_7456,c_7454,c_7453,c_7452,c_7449,c_7408,c_7404,c_7384,c_7380,c_7379,c_7377,c_7376,c_7373,c_7369,c_7367,c_7366,c_7363,c_7233,c_7230,c_7227,c_7224,c_7221,c_7218,c_7215,c_7212,c_7208,c_7207,c_7206,c_7205,c_7204,c_7203,c_7202,c_7201,c_7200,c_7199,c_7198,c_7197,c_7196,c_7195,c_7194,c_7193,c_7192,c_7191,c_7086,c_7085,c_7084,c_7083,c_7082,c_7081,c_7080,c_7079,c_7078,c_7077,c_7076,c_7075,c_6988,c_6987,c_6986,c_6985,c_6984,c_6983,c_6982,c_6981,c_6980,c_6979,c_6978,c_6977,c_6976,c_6975,c_6974,c_6973,c_6972,c_6971,c_6970,c_6969,c_6968,c_6967,c_6966,c_6965,c_6964,c_6963,c_6962,c_6961,c_6960,c_6959,c_6958,c_6957,c_6956,c_6955,c_6954,c_6953,c_6952,c_6951,c_6950,c_6949,c_6948,c_6938,c_6935,c_6915,c_6912,c_6842,c_6841,c_6840,c_6839,c_6838,c_6837,c_6836,c_6835,c_6834,c_6833,c_6832,c_6831,c_6828,c_6827,c_6826,c_6825,c_6824,c_6823,c_6776,c_6773,c_6770,c_6765,c_6761,c_6757,c_6756,c_6755,c_6754,c_6753,c_6750,c_6747,c_6744,c_6741,c_6738,c_6737,c_6736,c_6735,c_6734,c_6733,c_6732,c_6731,c_6730,c_6729,c_6727,c_6726,c_6725,c_6724,c_6719,c_6717,c_6716,c_6712,c_6630,c_6629,c_6628,c_6627,c_6624,c_6621,c_6612,c_6611,c_6610,c_6609,c_6608,c_6607,c_6606,c_6605,c_6604,c_6601,c_6600,c_6599,c_6598,c_6597,c_6596,c_6595,c_6594,c_6593,c_6592,c_6591,c_6590,c_6589,c_6588,c_6587,c_6586,c_6585,c_6584,c_6583,c_6582,c_6581,c_6580,c_6579,c_6578,c_6577,c_6576,c_6575,c_6574,c_6573,c_6572,c_6571,c_6570,c_6528,c_6527,c_6526,c_6525,c_6522,c_6519,c_6510,c_6509,c_6508,c_6507,c_6506,c_6505,c_6504,c_6503,c_6502,c_6499,c_6498,c_6497,c_6496,c_6495,c_6494,c_6493,c_6492,c_6491,c_6490,c_6489,c_6488,c_6487,c_6486,c_6485,c_6484,c_6483,c_6482,c_6481,c_6480,c_6479,c_6478,c_6477,c_6476,c_6475,c_6474,c_6473,c_6472,c_6471,c_6470,c_6469,c_6468,c_6453,c_6442,c_6441,c_6440,c_6439,c_6438,c_6436,c_6384,c_6383,c_6382,c_6381,c_6380,c_6379,c_6378,c_6377,c_6376,c_6375,c_6374,c_6373,c_6340,c_6339,c_6338,c_6337,c_6336,c_6335,c_6308,c_6307,c_6306,c_6305,c_6304,c_6303,c_6302,c_6301,c_6300,c_6299,c_6298,c_6297,c_6296,c_6295,c_6294,c_6293,c_6292,c_6291,c_6273,c_6272,c_6271,c_6270,c_6269,c_6268,c_6267,c_6266,c_6265,c_6264,c_6263,c_6262,c_6249,c_6234,c_6231,c_6230,c_6198,c_6197,c_6196,c_6195,c_6070,c_6069,c_6068,c_6067,c_6066,c_6065,c_6064,c_6063,c_6062,c_6061,c_6060,c_6059,c_6042,c_6041,c_6040,c_6039,c_6026,c_6025,c_6024,c_6023,c_6022,c_6021,c_6020,c_6019,c_6018,c_6017,c_6016,c_6015,c_6014,c_6013,c_6012,c_6011,c_5983,c_5982,c_5981,c_5980,c_5979,c_5978,c_5977,c_5976,c_5975,c_5974,c_5940,c_5939,c_5938,c_5937,c_5936,c_5935,c_5934,c_5933,c_5932,c_5931,c_5930,c_5924,c_5923,c_5922,c_5902,c_5901,c_5900,c_5899,c_5896,c_5895,c_5893,c_5884,c_5883,c_5882,c_5874,c_5873,c_5766,c_5765,c_5764,c_5763,c_5762,c_5761,c_5760,c_5759,c_5758,c_5757,c_5756,c_5755,c_5662,c_5661,c_5660,c_5659,c_5658,c_5657,c_5656,c_5655,c_5654,c_5653,c_5652,c_5651,c_5642,c_5640,c_5639,c_5637,c_5624,c_5622,c_5621,c_5619,c_5618,c_5616,c_5569,c_5568,c_5567,c_5566,c_5565,c_5564,c_5563,c_5562,c_5496,c_5495,c_5494,c_5493,c_5492,c_5491,c_5490,c_5489,c_5422,c_5421,c_5420,c_5419,c_5418,c_5417,c_5416,c_5415,c_5402,c_5400,c_5345,c_5344,c_5343,c_5342,c_5341,c_5340,c_5339,c_5338,c_5294,c_5293,c_5292,c_5291,c_5290,c_5289,c_5288,c_5287,c_5250,c_5249,c_5248,c_5247,c_5246,c_5245,c_5244,c_5243,c_5226,c_5225,c_5224,c_5223,c_5222,c_5221,c_5220,c_5219,c_5218,c_5217,c_5216,c_5215,c_5214,c_5213,c_5212,c_5211,c_5210,c_5209,c_5208,c_5207,c_5206,c_5205,c_5204,c_5194,c_5193,c_5192,c_5191,c_5190,c_5189,c_5188,c_5187,c_5186,c_5185,c_5184,c_5183,c_5182,c_5181,c_5180,c_5179,c_5178,c_5177,c_5176,c_5175,c_5174,c_5173,c_5171,c_5170,c_5169,c_5168,c_5137,c_5136,c_5135,c_5134,c_5133,c_5132,c_5131,c_5118,c_5086,c_5085,c_5084,c_5083,c_5082,c_5081,c_5065,c_5064,c_5063,c_5056,c_5055,c_5054,c_5052,c_5047,c_5046,c_5045,c_5043,c_5038,c_5037,c_5036,c_5035,c_5034,c_5029,c_5028,c_5027,c_5026,c_5025,c_5019,c_5018,c_5017,c_5016,c_5015,c_3781,c_3780,c_1285,c_187,c_180,c_177,c_174,c_172,c_170,c_5203,c_125,c_124,c_122,c_121,c_120,c_119,c_118,c_117,c_116,c_115,c_114,c_113,c_112,c_109,c_108,c_107,c_106,c_105,c_104,c_103,c_102,c_101,c_100,c_99,c_97,c_96,c_93,c_92,c_91,c_89,c_87,c_85,c_83,c_81,c_80,c_82,c_78,c_77,c_75,c_74,c_72,c_71,c_70,c_69,c_68,c_67,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_54,c_53,c_52,c_51,c_50,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM523+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 04:27:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 Running first-order theorem proving
% 0.12/0.38 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 4.30/1.27 % SZS status Started for theBenchmark.p
% 4.30/1.27 % SZS status Theorem for theBenchmark.p
% 4.30/1.27
% 4.30/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.30/1.27
% 4.30/1.27 % ------ iProver source info
% 4.30/1.27
% 4.30/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 4.30/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.30/1.27 % git: non_committed_changes: false
% 4.30/1.27
% 4.30/1.27 % ------ Parsing...
% 4.30/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.30/1.27
% 4.30/1.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 4.30/1.27
% 4.30/1.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.30/1.27
% 4.30/1.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.30/1.27 % ------ Proving...
% 4.30/1.27 % ------ Problem Properties
% 4.30/1.27
% 4.30/1.27 %
% 4.30/1.27 % clauses 73
% 4.30/1.27 % conjectures 1
% 4.30/1.27 % EPR 21
% 4.30/1.27 % Horn 48
% 4.30/1.27 % unary 14
% 4.30/1.27 % binary 8
% 4.30/1.27 % lits 273
% 4.30/1.27 % lits eq 80
% 4.30/1.27 % fd_pure 0
% 4.30/1.27 % fd_pseudo 0
% 4.30/1.27 % fd_cond 16
% 4.30/1.27 % fd_pseudo_cond 10
% 4.30/1.27 % AC symbols 0
% 4.30/1.27
% 4.30/1.27 % ------ Schedule dynamic 5 is on
% 4.30/1.27
% 4.30/1.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.30/1.27
% 4.30/1.27
% 4.30/1.27 % ------
% 4.30/1.27 % Current options:
% 4.30/1.27 % ------
% 4.30/1.27
% 4.30/1.27
% 4.30/1.27 %
% 4.30/1.27
% 4.30/1.27 % ------ Proving...
% 4.30/1.27 %
% 4.30/1.27
% 4.30/1.27 % SZS status Theorem for theBenchmark.p
% 4.30/1.27
% 4.30/1.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.30/1.29
% 4.30/1.29
%------------------------------------------------------------------------------