%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM494+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Sun Sep 27 08:17:11 AM UTC 2026
% Result : Theorem 38.85s 5.58s
% Output : CNFRefutation 38.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 17
% Syntax : Number of formulae : 154 ( 64 unt; 0 def)
% Number of atoms : 336 ( 143 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 314 ( 132 ~; 137 |; 27 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 92 ( 0 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsB,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('theBenchmark.p',mSortsB) ).
fof(mAddComm,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('theBenchmark.p',mAddComm) ).
fof(mAddAsso,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('theBenchmark.p',mAddAsso) ).
fof(m_AddZero,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('theBenchmark.p',m_AddZero) ).
fof(mAddCanc,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtpldt0(W1,W0) = sdtpldt0(W2,W0)
| sdtpldt0(W0,W1) = sdtpldt0(W0,W2) )
=> W1 = W2 ) ),
file('theBenchmark.p',mAddCanc) ).
fof(mDefDiff,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
=> ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ) ),
file('theBenchmark.p',mDefDiff) ).
fof(mLEAsym,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLEAsym) ).
fof(mLETotal,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('theBenchmark.p',mLETotal) ).
fof(mMonAdd,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> ! [W2] :
( aNaturalNumber0(W2)
=> ( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W2,W0) != sdtpldt0(W2,W1) ) ) ) ),
file('theBenchmark.p',mMonAdd) ).
fof(mDefPrime,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( isPrime0(W0)
<=> ( ! [W1] :
( ( doDivides0(W1,W0)
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) ) ),
file('theBenchmark.p',mDefPrime) ).
fof(m__1837,axiom,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__1860,axiom,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ),
file('theBenchmark.p',m__1860) ).
fof(m__1894,axiom,
( sdtlseqdt0(xr,xn)
& xr != xn ),
file('theBenchmark.p',m__1894) ).
fof(m__,conjecture,
( sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
& sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
& sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_46,plain,
( sz00 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_52,plain,
isPrime0(xp),
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_53,plain,
( sz00 != xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_52,c_46]) ).
cnf(c_54,plain,
( xp != sz00
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_53]) ).
cnf(c_83,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xr,xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_85,plain,
sdtlseqdt0(xr,xn),
inference(clausify,[status(thm)],[m__1894]) ).
cnf(c_86,plain,
xr != xn,
inference(clausify,[status(thm)],[m__1894]) ).
fof(m__1883,axiom,
xr = sdtmndt0(xn,xp),
file('theBenchmark.p',m__1883) ).
cnf(c_87,plain,
xr = sdtmndt0(xn,xp),
inference(clausify,[status(thm)],[m__1883]) ).
fof(m__1870,axiom,
sdtlseqdt0(xp,xn),
file('theBenchmark.p',m__1870) ).
cnf(c_88,plain,
sdtlseqdt0(xp,xn),
inference(clausify,[status(thm)],[m__1870]) ).
cnf(c_90,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_91,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_92,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_116,plain,
( sdtlseqdt0(sdtpldt0(C,A),sdtpldt0(C,B))
| ~ aNaturalNumber0(C)
| ~ sdtlseqdt0(A,B)
| B = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMonAdd]) ).
cnf(c_118,plain,
( sdtlseqdt0(B,A)
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETotal]) ).
cnf(c_121,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_124,plain,
( sdtpldt0(A,C) = B
| sdtmndt0(B,A) != C
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_125,plain,
( aNaturalNumber0(C)
| sdtmndt0(B,A) != C
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_137,plain,
( C = B
| sdtpldt0(A,C) != sdtpldt0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddCanc]) ).
cnf(c_149,plain,
( sdtpldt0(A,sz00) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_AddZero]) ).
cnf(c_150,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_151,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddComm]) ).
cnf(c_153,plain,
( aNaturalNumber0(sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_156,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_180,plain,
sdtmndt0(xn,xp) != xn,
inference(paramod,[status(thm)],[c_87,c_86]) ).
cnf(c_181,plain,
sdtlseqdt0(sdtmndt0(xn,xp),xn),
inference(paramod,[status(thm)],[c_87,c_85]) ).
cnf(c_15027,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(paramod,[status(thm)],[c_87,c_83]) ).
cnf(c_183,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(paramod,[status(thm)],[c_87,c_15027]) ).
cnf(c_187,plain,
xp != sz00,
inference(resolve,[status(thm)],[c_90,c_54]) ).
cnf(c_15028,plain,
( sdtpldt0(xp,B) = A
| sdtmndt0(A,xp) != B
| ~ sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_124,c_90]) ).
cnf(c_15029,plain,
( sdtpldt0(xp,A) = xn
| sdtmndt0(xn,xp) != A
| ~ sdtlseqdt0(xp,xn) ),
inference(resolve,[status(thm)],[c_15028,c_92]) ).
cnf(c_15030,plain,
( sdtpldt0(xp,A) = xn
| sdtmndt0(xn,xp) != A ),
inference(resolve,[status(thm)],[c_15029,c_88]) ).
cnf(c_15031,plain,
sdtmndt0(xn,xp) = xr,
inference(copy,[status(thm)],[c_87]) ).
cnf(c_15032,plain,
sdtpldt0(xp,xr) = xn,
inference(resolve,[status(thm)],[c_15030,c_15031]) ).
cnf(c_375,plain,
sdtpldt0(xp,sdtmndt0(xn,xp)) = xn,
inference(paramod,[status(thm)],[c_87,c_15032]) ).
cnf(c_15033,plain,
( aNaturalNumber0(B)
| sdtmndt0(A,xp) != B
| ~ sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_125,c_90]) ).
cnf(c_15034,plain,
( aNaturalNumber0(A)
| sdtmndt0(xn,xp) != A
| ~ sdtlseqdt0(xp,xn) ),
inference(resolve,[status(thm)],[c_15033,c_92]) ).
cnf(c_15035,plain,
( aNaturalNumber0(A)
| sdtmndt0(xn,xp) != A ),
inference(resolve,[status(thm)],[c_15034,c_88]) ).
cnf(c_15036,plain,
sdtmndt0(xn,xp) = xr,
inference(copy,[status(thm)],[c_87]) ).
cnf(c_15037,plain,
aNaturalNumber0(xr),
inference(resolve,[status(thm)],[c_15035,c_15036]) ).
cnf(c_377,plain,
aNaturalNumber0(sdtmndt0(xn,xp)),
inference(paramod,[status(thm)],[c_87,c_15037]) ).
cnf(c_700,plain,
sdtpldt0(xm,sz00) = xm,
inference(resolve,[status(thm)],[c_149,c_91]) ).
cnf(c_15038,plain,
( sdtpldt0(sdtpldt0(xn,A),B) = sdtpldt0(xn,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_92]) ).
cnf(c_15039,plain,
( sdtpldt0(sdtpldt0(xn,xm),A) = sdtpldt0(xn,sdtpldt0(xm,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15038,c_91]) ).
cnf(c_716,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)),
inference(resolve,[status(thm)],[c_15039,c_90]) ).
cnf(c_15040,plain,
( sdtpldt0(sdtpldt0(xn,A),B) = sdtpldt0(xn,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_92]) ).
cnf(c_15041,plain,
( sdtpldt0(sdtpldt0(xn,xp),A) = sdtpldt0(xn,sdtpldt0(xp,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15040,c_90]) ).
cnf(c_718,plain,
sdtpldt0(sdtpldt0(xn,xp),xm) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(resolve,[status(thm)],[c_15041,c_91]) ).
cnf(c_15042,plain,
( sdtpldt0(sdtpldt0(xm,A),B) = sdtpldt0(xm,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_91]) ).
cnf(c_15043,plain,
( sdtpldt0(sdtpldt0(xm,xn),A) = sdtpldt0(xm,sdtpldt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15042,c_92]) ).
cnf(c_722,plain,
sdtpldt0(sdtpldt0(xm,xn),xp) = sdtpldt0(xm,sdtpldt0(xn,xp)),
inference(resolve,[status(thm)],[c_15043,c_90]) ).
cnf(c_15044,plain,
( sdtpldt0(sdtpldt0(xp,A),B) = sdtpldt0(xp,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_90]) ).
cnf(c_15045,plain,
( sdtpldt0(sdtpldt0(xp,xn),A) = sdtpldt0(xp,sdtpldt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15044,c_92]) ).
cnf(c_730,plain,
sdtpldt0(sdtpldt0(xp,xn),xm) = sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(resolve,[status(thm)],[c_15045,c_91]) ).
cnf(c_15046,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)) ),
inference(paramod,[status(thm)],[c_716,c_183]) ).
cnf(c_754,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xn,sdtpldt0(xm,xp)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)) ),
inference(paramod,[status(thm)],[c_716,c_15046]) ).
cnf(c_15047,plain,
( sdtpldt0(A,xn) = sdtpldt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_151,c_92]) ).
cnf(c_15048,plain,
sdtpldt0(xm,xn) = sdtpldt0(xn,xm),
inference(resolve,[status(thm)],[c_15047,c_91]) ).
cnf(c_781,plain,
sdtpldt0(xn,xm) = sdtpldt0(xm,xn),
inference(copy,[status(thm)],[c_15048]) ).
cnf(c_15049,plain,
( sdtpldt0(A,xn) = sdtpldt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_151,c_92]) ).
cnf(c_15050,plain,
sdtpldt0(xp,xn) = sdtpldt0(xn,xp),
inference(resolve,[status(thm)],[c_15049,c_90]) ).
cnf(c_782,plain,
sdtpldt0(xn,xp) = sdtpldt0(xp,xn),
inference(copy,[status(thm)],[c_15050]) ).
cnf(c_15051,plain,
( sdtpldt0(A,xm) = sdtpldt0(xm,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_151,c_91]) ).
cnf(c_15052,plain,
sdtpldt0(xp,xm) = sdtpldt0(xm,xp),
inference(resolve,[status(thm)],[c_15051,c_90]) ).
cnf(c_783,plain,
sdtpldt0(xm,xp) = sdtpldt0(xp,xm),
inference(copy,[status(thm)],[c_15052]) ).
cnf(c_784,plain,
sdtpldt0(sdtpldt0(xp,xn),xm) = sdtpldt0(xp,sdtpldt0(xm,xn)),
inference(paramod,[status(thm)],[c_781,c_730]) ).
cnf(c_15053,plain,
sdtpldt0(sdtpldt0(xm,xn),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)),
inference(paramod,[status(thm)],[c_781,c_716]) ).
cnf(c_15054,plain,
sdtpldt0(xm,sdtpldt0(xn,xp)) = sdtpldt0(xn,sdtpldt0(xm,xp)),
inference(paramod,[status(thm)],[c_722,c_15053]) ).
cnf(c_15055,plain,
sdtpldt0(xm,sdtpldt0(xp,xn)) = sdtpldt0(xn,sdtpldt0(xm,xp)),
inference(paramod,[status(thm)],[c_782,c_15054]) ).
cnf(c_15056,plain,
sdtpldt0(xm,sdtpldt0(xp,xn)) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(paramod,[status(thm)],[c_783,c_15055]) ).
cnf(c_786,plain,
sdtpldt0(xn,sdtpldt0(xp,xm)) = sdtpldt0(xm,sdtpldt0(xp,xn)),
inference(copy,[status(thm)],[c_15056]) ).
cnf(c_795,plain,
sdtpldt0(sdtpldt0(xm,xn),xp) = sdtpldt0(xm,sdtpldt0(xp,xn)),
inference(paramod,[status(thm)],[c_782,c_722]) ).
cnf(c_15057,plain,
sdtpldt0(sdtpldt0(xp,xn),xm) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(paramod,[status(thm)],[c_782,c_718]) ).
cnf(c_15058,plain,
sdtpldt0(xp,sdtpldt0(xm,xn)) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(paramod,[status(thm)],[c_784,c_15057]) ).
cnf(c_15059,plain,
sdtpldt0(xp,sdtpldt0(xm,xn)) = sdtpldt0(xm,sdtpldt0(xp,xn)),
inference(paramod,[status(thm)],[c_786,c_15058]) ).
cnf(c_797,plain,
sdtpldt0(xm,sdtpldt0(xp,xn)) = sdtpldt0(xp,sdtpldt0(xm,xn)),
inference(copy,[status(thm)],[c_15059]) ).
cnf(c_15060,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xn,sdtpldt0(xm,xp)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xn,sdtpldt0(xp,xm)) ),
inference(paramod,[status(thm)],[c_783,c_754]) ).
cnf(c_15061,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xn,sdtpldt0(xm,xp)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xm,sdtpldt0(xp,xn)) ),
inference(paramod,[status(thm)],[c_786,c_15060]) ).
cnf(c_15062,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xn,sdtpldt0(xm,xp)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_797,c_15061]) ).
cnf(c_15063,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xn,sdtpldt0(xp,xm)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_783,c_15062]) ).
cnf(c_15064,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xm,sdtpldt0(xp,xn)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_786,c_15063]) ).
cnf(c_826,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_797,c_15064]) ).
cnf(c_841,plain,
sdtpldt0(sdtpldt0(xm,xn),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)),
inference(paramod,[status(thm)],[c_797,c_795]) ).
cnf(c_15065,plain,
( aNaturalNumber0(sdtpldt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_153,c_92]) ).
cnf(c_15066,plain,
aNaturalNumber0(sdtpldt0(xn,xm)),
inference(resolve,[status(thm)],[c_15065,c_91]) ).
cnf(c_881,plain,
aNaturalNumber0(sdtpldt0(xm,xn)),
inference(paramod,[status(thm)],[c_781,c_15066]) ).
cnf(c_15067,plain,
( sdtpldt0(sdtpldt0(xn,A),B) = sdtpldt0(xn,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_92]) ).
cnf(c_15068,plain,
( sdtpldt0(sdtpldt0(xn,xm),A) = sdtpldt0(xn,sdtpldt0(xm,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15067,c_91]) ).
cnf(c_15069,plain,
sdtpldt0(sdtpldt0(xn,xm),sz00) = sdtpldt0(xn,sdtpldt0(xm,sz00)),
inference(resolve,[status(thm)],[c_15068,c_156]) ).
cnf(c_15070,plain,
sdtpldt0(sdtpldt0(xm,xn),sz00) = sdtpldt0(xn,sdtpldt0(xm,sz00)),
inference(paramod,[status(thm)],[c_781,c_15069]) ).
cnf(c_15071,plain,
sdtpldt0(sdtpldt0(xm,xn),sz00) = sdtpldt0(xn,xm),
inference(paramod,[status(thm)],[c_700,c_15070]) ).
cnf(c_1144,plain,
sdtpldt0(sdtpldt0(xm,xn),sz00) = sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_781,c_15071]) ).
cnf(c_15072,plain,
( sdtlseqdt0(A,xp)
| sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_118,c_90]) ).
cnf(c_1206,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(xp,sz00) ),
inference(resolve,[status(thm)],[c_15072,c_156]) ).
cnf(c_15073,plain,
( sdtmndt0(xn,xp) = xn
| ~ sdtlseqdt0(xn,sdtmndt0(xn,xp))
| ~ aNaturalNumber0(sdtmndt0(xn,xp))
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_181,c_121]) ).
cnf(c_15074,plain,
( sdtmndt0(xn,xp) = xn
| ~ sdtlseqdt0(xn,sdtmndt0(xn,xp))
| ~ aNaturalNumber0(sdtmndt0(xn,xp)) ),
inference(resolve,[status(thm)],[c_92,c_15073]) ).
cnf(c_15075,plain,
( sdtmndt0(xn,xp) = xn
| ~ sdtlseqdt0(xn,sdtmndt0(xn,xp)) ),
inference(resolve,[status(thm)],[c_377,c_15074]) ).
cnf(c_1236,plain,
~ sdtlseqdt0(xn,sdtmndt0(xn,xp)),
inference(resolve,[status(thm)],[c_180,c_15075]) ).
cnf(c_3222,plain,
sdtpldt0(sdtmndt0(xn,xp),sz00) = sdtmndt0(xn,xp),
inference(resolve,[status(thm)],[c_377,c_149]) ).
cnf(c_15076,plain,
( sdtpldt0(A,xm) = sdtpldt0(xm,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_151,c_91]) ).
cnf(c_3417,plain,
sdtpldt0(sdtmndt0(xn,xp),xm) = sdtpldt0(xm,sdtmndt0(xn,xp)),
inference(resolve,[status(thm)],[c_15076,c_377]) ).
cnf(c_15077,plain,
( sdtpldt0(A,xp) = sdtpldt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_151,c_90]) ).
cnf(c_15078,plain,
sdtpldt0(sdtmndt0(xn,xp),xp) = sdtpldt0(xp,sdtmndt0(xn,xp)),
inference(resolve,[status(thm)],[c_15077,c_377]) ).
cnf(c_3418,plain,
sdtpldt0(sdtmndt0(xn,xp),xp) = xn,
inference(paramod,[status(thm)],[c_375,c_15078]) ).
cnf(c_15079,plain,
( sdtpldt0(sdtpldt0(xm,A),B) = sdtpldt0(xm,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_91]) ).
cnf(c_15080,plain,
( sdtpldt0(sdtpldt0(xm,sdtmndt0(xn,xp)),A) = sdtpldt0(xm,sdtpldt0(sdtmndt0(xn,xp),A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15079,c_377]) ).
cnf(c_15081,plain,
sdtpldt0(sdtpldt0(xm,sdtmndt0(xn,xp)),xp) = sdtpldt0(xm,sdtpldt0(sdtmndt0(xn,xp),xp)),
inference(resolve,[status(thm)],[c_15080,c_90]) ).
cnf(c_3467,plain,
sdtpldt0(sdtpldt0(xm,sdtmndt0(xn,xp)),xp) = sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_3418,c_15081]) ).
cnf(c_15082,plain,
( sdtlseqdt0(sdtpldt0(B,xp),sdtpldt0(B,A))
| ~ aNaturalNumber0(B)
| ~ sdtlseqdt0(xp,A)
| A = xp
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_116,c_90]) ).
cnf(c_15083,plain,
( sdtlseqdt0(sdtpldt0(A,xp),sdtpldt0(A,sz00))
| ~ aNaturalNumber0(A)
| ~ sdtlseqdt0(xp,sz00)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_15082,c_156]) ).
cnf(c_15084,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(sdtpldt0(A,xp),sdtpldt0(A,sz00))
| ~ aNaturalNumber0(A)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_15083,c_1206]) ).
cnf(c_15085,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(sdtpldt0(sdtmndt0(xn,xp),xp),sdtpldt0(sdtmndt0(xn,xp),sz00))
| sz00 = xp ),
inference(resolve,[status(thm)],[c_15084,c_377]) ).
cnf(c_15086,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(xn,sdtpldt0(sdtmndt0(xn,xp),sz00))
| sz00 = xp ),
inference(paramod,[status(thm)],[c_3418,c_15085]) ).
cnf(c_15087,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(xn,sdtmndt0(xn,xp))
| sz00 = xp ),
inference(paramod,[status(thm)],[c_3222,c_15086]) ).
cnf(c_15088,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(xn,sdtmndt0(xn,xp))
| xp = sz00 ),
inference(copy,[status(thm)],[c_15087]) ).
cnf(c_15089,plain,
( sdtlseqdt0(sz00,xp)
| sdtlseqdt0(xn,sdtmndt0(xn,xp)) ),
inference(resolve,[status(thm)],[c_187,c_15088]) ).
cnf(c_3703,plain,
sdtlseqdt0(sz00,xp),
inference(resolve,[status(thm)],[c_1236,c_15089]) ).
cnf(c_15090,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(sdtpldt0(xm,sdtmndt0(xn,xp)),xp) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_3417,c_826]) ).
cnf(c_15091,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtmndt0(xn,xp),xm),xp),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(xm,xn) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_3467,c_15090]) ).
cnf(c_15092,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xm,sdtmndt0(xn,xp)),xp),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(xm,xn) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_3417,c_15091]) ).
cnf(c_15093,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(xm,xn) = sdtpldt0(xp,sdtpldt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_3467,c_15092]) ).
cnf(c_3867,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(xp,sdtpldt0(xm,xn)))
| sdtpldt0(xp,sdtpldt0(xm,xn)) = sdtpldt0(xm,xn) ),
inference(copy,[status(thm)],[c_15093]) ).
cnf(c_15094,plain,
( sdtlseqdt0(sdtpldt0(B,sz00),sdtpldt0(B,A))
| ~ aNaturalNumber0(B)
| ~ sdtlseqdt0(sz00,A)
| A = sz00
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_116,c_156]) ).
cnf(c_15095,plain,
( sdtlseqdt0(sdtpldt0(A,sz00),sdtpldt0(A,xp))
| ~ aNaturalNumber0(A)
| ~ sdtlseqdt0(sz00,xp)
| xp = sz00 ),
inference(resolve,[status(thm)],[c_15094,c_90]) ).
cnf(c_15096,plain,
( sdtlseqdt0(sdtpldt0(A,sz00),sdtpldt0(A,xp))
| ~ aNaturalNumber0(A)
| xp = sz00 ),
inference(resolve,[status(thm)],[c_15095,c_3703]) ).
cnf(c_15097,plain,
( sdtlseqdt0(sdtpldt0(sdtpldt0(xm,xn),sz00),sdtpldt0(sdtpldt0(xm,xn),xp))
| xp = sz00 ),
inference(resolve,[status(thm)],[c_15096,c_881]) ).
cnf(c_15098,plain,
( sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(sdtpldt0(xm,xn),xp))
| xp = sz00 ),
inference(paramod,[status(thm)],[c_1144,c_15097]) ).
cnf(c_15099,plain,
( sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(xp,sdtpldt0(xm,xn)))
| xp = sz00 ),
inference(paramod,[status(thm)],[c_841,c_15098]) ).
cnf(c_14815,plain,
sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(xp,sdtpldt0(xm,xn))),
inference(resolve,[status(thm)],[c_187,c_15099]) ).
cnf(c_15100,plain,
( B = A
| sdtpldt0(sdtpldt0(xm,xn),B) != sdtpldt0(sdtpldt0(xm,xn),A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_137,c_881]) ).
cnf(c_15101,plain,
( A = sz00
| sdtpldt0(sdtpldt0(xm,xn),A) != sdtpldt0(sdtpldt0(xm,xn),sz00)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_15100,c_156]) ).
cnf(c_15102,plain,
( xp = sz00
| sdtpldt0(sdtpldt0(xm,xn),xp) != sdtpldt0(sdtpldt0(xm,xn),sz00) ),
inference(resolve,[status(thm)],[c_15101,c_90]) ).
cnf(c_15103,plain,
sdtpldt0(sdtpldt0(xm,xn),xp) != sdtpldt0(sdtpldt0(xm,xn),sz00),
inference(resolve,[status(thm)],[c_15102,c_187]) ).
cnf(c_15104,plain,
sdtpldt0(xp,sdtpldt0(xm,xn)) != sdtpldt0(sdtpldt0(xm,xn),sz00),
inference(paramod,[status(thm)],[c_841,c_15103]) ).
cnf(c_14936,plain,
sdtpldt0(xp,sdtpldt0(xm,xn)) != sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_1144,c_15104]) ).
cnf(c_15105,negated_conjecture,
~ sdtlseqdt0(sdtpldt0(xm,xn),sdtpldt0(xp,sdtpldt0(xm,xn))),
inference(resolve,[status(thm)],[c_14936,c_3867]) ).
cnf(c_15026,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_14815,c_15105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM494+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 26 02:56:38 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 2647300 was started by sandbox2 on n007,
% 0.11/0.37 % Sat Sep 26 02:56:38 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 38.85/5.58
% 38.85/5.58 % SZS status Theorem for theBenchmark
% 38.85/5.58
% 38.85/5.58 % Proof 1 at 4.76 (+ 0.41) seconds.
% 38.85/5.58 % Length of proof is 71.
% 38.85/5.58 % Level of proof is 7.
% 38.85/5.58 % Maximum clause weight is 66.000.
% 38.85/5.58 % Given clauses 429.
% 38.85/5.58
% 38.85/5.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------