%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NUM495+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:12:56 AM UTC 2026
% Result : Theorem 5.52s 27.44s
% Output : CNFRefutation 5.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 14
% Syntax : Number of formulae : 126 ( 52 unt; 1 def)
% Number of atoms : 335 ( 97 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 381 ( 172 ~; 181 |; 16 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 68 ( 0 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsB,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ) ).
fof(mAddComm,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ) ).
fof(mAddAsso,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ) ).
fof(mMulComm,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ).
fof(mDefDiff,definition,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( sdtlseqdt0(X0,X1)
=> ! [X2] :
( X2 = sdtmndt0(X1,X0)
<=> ( sdtpldt0(X0,X2) = X1
& aNaturalNumber0(X2) ) ) ) ) ).
fof(mIH_03,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( sdtlseqdt0(X0,X1)
& X0 != X1 )
=> iLess0(X0,X1) ) ) ).
fof(m__1837,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ) ).
fof(m__1799,hypothesis,
! [X0,X1,X2] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X1)
& aNaturalNumber0(X0) )
=> ( ( doDivides0(X2,sdtasdt0(X0,X1))
& isPrime0(X2) )
=> ( iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
=> ( doDivides0(X2,X1)
| doDivides0(X2,X0) ) ) ) ) ).
fof(m__1860,hypothesis,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ) ).
fof(m__1870,hypothesis,
sdtlseqdt0(xp,xn) ).
fof(m__1883,hypothesis,
xr = sdtmndt0(xn,xp) ).
fof(m__1913,hypothesis,
doDivides0(xp,sdtasdt0(xr,xm)) ).
fof(m__2062,hypothesis,
( sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
& sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp) ) ).
fof(m__,conjecture,
( doDivides0(xp,xm)
| doDivides0(xp,xr) ) ).
fof(negated_conjecture,negated_conjecture,
~ ( doDivides0(xp,xm)
| doDivides0(xp,xr) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(c3,plain,
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mSortsB]) ).
cnf(c5,plain,
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mAddComm]) ).
cnf(c6,plain,
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mAddAsso]) ).
cnf(c9,plain,
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mMulComm]) ).
cnf(c27,plain,
( aNaturalNumber0(X1)
| ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| X1 != sdtmndt0(X2,X0)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mDefDiff]) ).
cnf(c28,plain,
( ~ aNaturalNumber0(X1)
| sdtpldt0(X0,X2) = X1
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mDefDiff]) ).
cnf(c46,plain,
( ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X1,X0)
| iLess0(X1,X0)
| X1 = X0
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mIH_03]) ).
cnf(c70,plain,
aNaturalNumber0(xn),
inference(clausification,[status(esa)],[m__1837]) ).
cnf(c71,plain,
aNaturalNumber0(xm),
inference(clausification,[status(esa)],[m__1837]) ).
cnf(c72,plain,
aNaturalNumber0(xp),
inference(clausification,[status(esa)],[m__1837]) ).
cnf(c73,plain,
( doDivides0(X1,X2)
| ~ iLess0(sdtpldt0(sdtpldt0(X2,X0),X1),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ doDivides0(X1,sdtasdt0(X2,X0))
| doDivides0(X1,X0)
| ~ isPrime0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[m__1799]) ).
cnf(c74,plain,
isPrime0(xp),
inference(clausification,[status(esa)],[m__1860]) ).
cnf(c76,plain,
sdtlseqdt0(xp,xn),
inference(clausification,[status(esa)],[m__1870]) ).
cnf(c77,plain,
xr = sdtmndt0(xn,xp),
inference(clausification,[status(esa)],[m__1883]) ).
cnf(c80,plain,
doDivides0(xp,sdtasdt0(xr,xm)),
inference(clausification,[status(esa)],[m__1913]) ).
cnf(c81,plain,
sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp),
inference(clausification,[status(esa)],[m__2062]) ).
cnf(c82,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)),
inference(clausification,[status(esa)],[m__2062]) ).
cnf(c83,plain,
~ doDivides0(xp,xr),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c84,plain,
~ doDivides0(xp,xm),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn)
| sdtpldt0(xp,X0) = xn
| X0 != xr ),
inference(superposition,[status(thm)],[c77,c28]) ).
cnf(d1,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xp)
| sdtpldt0(xp,X0) = xn
| X0 != xr ),
inference(resolution,[status(thm)],[c70,d0]) ).
cnf(d2,plain,
( ~ sdtlseqdt0(xp,xn)
| sdtpldt0(xp,X0) = xn
| X0 != xr ),
inference(resolution,[status(thm)],[c72,d1]) ).
cnf(d3,plain,
( sdtpldt0(xp,X0) = xn
| X0 != xr ),
inference(resolution,[status(thm)],[c76,d2]) ).
cnf(d4,plain,
sdtpldt0(xp,xr) = xn,
inference(equality_resolution,[status(thm)],[d3]) ).
cnf(d5,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(xp,X0) = sdtpldt0(X0,xp) ),
inference(resolution,[status(thm)],[c5,c72]) ).
cnf(d6,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn)
| aNaturalNumber0(X0)
| X0 != xr ),
inference(superposition,[status(thm)],[c77,c27]) ).
cnf(d7,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xp)
| aNaturalNumber0(X0)
| X0 != xr ),
inference(resolution,[status(thm)],[c70,d6]) ).
cnf(d8,plain,
( ~ sdtlseqdt0(xp,xn)
| aNaturalNumber0(X0)
| X0 != xr ),
inference(resolution,[status(thm)],[c72,d7]) ).
cnf(d9,plain,
( aNaturalNumber0(X0)
| X0 != xr ),
inference(resolution,[status(thm)],[c76,d8]) ).
cnf(d10,plain,
aNaturalNumber0(xr),
inference(equality_resolution,[status(thm)],[d9]) ).
cnf(d11,plain,
sdtpldt0(xp,xr) = sdtpldt0(xr,xp),
inference(resolution,[status(thm)],[d10,d5]) ).
cnf(d12,plain,
xn = sdtpldt0(xr,xp),
inference(demodulation,[status(thm)],[d11,d4]) ).
cnf(d13,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtpldt0(sdtpldt0(X0,xp),X1) = sdtpldt0(X0,sdtpldt0(xp,X1)) ),
inference(resolution,[status(thm)],[c6,c72]) ).
cnf(d14,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xr,xp),X0) = sdtpldt0(xr,sdtpldt0(xp,X0)) ),
inference(resolution,[status(thm)],[d10,d13]) ).
cnf(d15,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(xn,X0) = sdtpldt0(xr,sdtpldt0(xp,X0)) ),
inference(demodulation,[status(thm)],[d14,d12]) ).
cnf(d16,plain,
sdtpldt0(xn,xm) = sdtpldt0(xr,sdtpldt0(xp,xm)),
inference(resolution,[status(thm)],[d15,c71]) ).
cnf(d17,plain,
sdtpldt0(xp,xm) = sdtpldt0(xm,xp),
inference(resolution,[status(thm)],[d5,c71]) ).
cnf(d18,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(xm,X0) = sdtpldt0(X0,xm) ),
inference(resolution,[status(thm)],[c5,c71]) ).
cnf(d19,plain,
sdtpldt0(xm,xr) = sdtpldt0(xr,xm),
inference(resolution,[status(thm)],[d10,d18]) ).
cnf(d20,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtpldt0(sdtpldt0(X0,xm),X1) = sdtpldt0(X0,sdtpldt0(xm,X1)) ),
inference(resolution,[status(thm)],[c6,c71]) ).
cnf(d21,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xr,xm),X0) = sdtpldt0(xr,sdtpldt0(xm,X0)) ),
inference(resolution,[status(thm)],[d10,d20]) ).
cnf(d22,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xm,xr),X0) = sdtpldt0(xr,sdtpldt0(xm,X0)) ),
inference(demodulation,[status(thm)],[d21,d19]) ).
cnf(d23,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(xr,sdtpldt0(xm,xp)),
inference(resolution,[status(thm)],[d22,c72]) ).
cnf(d24,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(xr,sdtpldt0(xp,xm)),
inference(demodulation,[status(thm)],[d23,d17]) ).
cnf(d25,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(xn,xm),
inference(demodulation,[status(thm)],[d24,d16]) ).
cnf(d26,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtpldt0(sdtpldt0(X0,xn),X1) = sdtpldt0(X0,sdtpldt0(xn,X1)) ),
inference(resolution,[status(thm)],[c6,c70]) ).
cnf(d27,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xp,xn),X0) = sdtpldt0(xp,sdtpldt0(xn,X0)) ),
inference(resolution,[status(thm)],[d26,c72]) ).
cnf(d28,plain,
sdtpldt0(sdtpldt0(xp,xn),xm) = sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(resolution,[status(thm)],[d27,c71]) ).
cnf(d29,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(xn,X0) = sdtpldt0(X0,xn) ),
inference(resolution,[status(thm)],[c5,c70]) ).
cnf(d30,plain,
sdtpldt0(xn,xp) = sdtpldt0(xp,xn),
inference(resolution,[status(thm)],[d29,c72]) ).
cnf(d31,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xn,xp),X0) = sdtpldt0(xn,sdtpldt0(xp,X0)) ),
inference(resolution,[status(thm)],[d13,c70]) ).
cnf(d32,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xp,xn),X0) = sdtpldt0(xn,sdtpldt0(xp,X0)) ),
inference(demodulation,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
sdtpldt0(sdtpldt0(xp,xn),xm) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(resolution,[status(thm)],[d32,c71]) ).
cnf(d34,plain,
sdtpldt0(xp,sdtpldt0(xn,xm)) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(demodulation,[status(thm)],[d33,d28]) ).
cnf(d35,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xn,xm),X0) = sdtpldt0(xn,sdtpldt0(xm,X0)) ),
inference(resolution,[status(thm)],[d20,c70]) ).
cnf(d36,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)),
inference(resolution,[status(thm)],[d35,c72]) ).
cnf(d37,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xn,sdtpldt0(xp,xm)),
inference(demodulation,[status(thm)],[d36,d17]) ).
cnf(d38,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(demodulation,[status(thm)],[d37,d34]) ).
cnf(d39,plain,
( iLess0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xr,xm),xp))
| sdtpldt0(sdtpldt0(xr,xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(resolution,[status(thm)],[c82,c46]) ).
cnf(d40,plain,
( iLess0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xr,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(demodulation,[status(thm)],[d39,d19]) ).
cnf(d41,plain,
( iLess0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(demodulation,[status(thm)],[d40,d19]) ).
cnf(d42,plain,
( iLess0(sdtpldt0(sdtpldt0(xm,xr),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(demodulation,[status(thm)],[d41,d19]) ).
cnf(d43,plain,
( ~ isPrime0(xp)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| doDivides0(xp,xr)
| doDivides0(xp,xm)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xm,xr),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(resolution,[status(thm)],[d42,c73]) ).
cnf(d44,plain,
( ~ isPrime0(xp)
| doDivides0(xp,xr)
| doDivides0(xp,xm)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(xn,xm) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(demodulation,[status(thm)],[d43,d25]) ).
cnf(d45,plain,
( ~ isPrime0(xp)
| doDivides0(xp,xr)
| doDivides0(xp,xm)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(demodulation,[status(thm)],[d44,d38]) ).
cnf(d46,plain,
( ~ isPrime0(xp)
| doDivides0(xp,xr)
| doDivides0(xp,xm)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xm,xr),xp))
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(demodulation,[status(thm)],[d45,d38]) ).
cnf(d47,plain,
( ~ isPrime0(xp)
| doDivides0(xp,xr)
| doDivides0(xp,xm)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(demodulation,[status(thm)],[d46,d25]) ).
cnf(d48,plain,
( ~ isPrime0(xp)
| doDivides0(xp,xm)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c83,d47]) ).
cnf(d49,plain,
( ~ isPrime0(xp)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c84,d48]) ).
cnf(d50,plain,
( ~ isPrime0(xp)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c71,d49]) ).
cnf(d51,plain,
( ~ isPrime0(xp)
| ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c72,d50]) ).
cnf(d52,plain,
( ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c74,d51]) ).
cnf(d53,plain,
( ~ doDivides0(xp,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[d10,d52]) ).
cnf(d54,plain,
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xm) = sdtasdt0(xm,X0) ),
inference(resolution,[status(thm)],[c9,c71]) ).
cnf(d55,plain,
sdtasdt0(xr,xm) = sdtasdt0(xm,xr),
inference(resolution,[status(thm)],[d10,d54]) ).
cnf(d56,plain,
doDivides0(xp,sdtasdt0(xm,xr)),
inference(demodulation,[status(thm)],[c80,d55]) ).
cnf(d57,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[d56,d53]) ).
cnf(d58,plain,
sdtpldt0(xn,xm) = sdtpldt0(xm,xn),
inference(resolution,[status(thm)],[d29,c71]) ).
cnf(d59,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xm,xp),X0) = sdtpldt0(xm,sdtpldt0(xp,X0)) ),
inference(resolution,[status(thm)],[d13,c71]) ).
cnf(d60,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xp,xm),X0) = sdtpldt0(xm,sdtpldt0(xp,X0)) ),
inference(demodulation,[status(thm)],[d59,d17]) ).
cnf(d61,plain,
sdtpldt0(sdtpldt0(xp,xm),xr) = sdtpldt0(xm,sdtpldt0(xp,xr)),
inference(resolution,[status(thm)],[d60,d10]) ).
cnf(d62,plain,
sdtpldt0(sdtpldt0(xp,xm),xr) = sdtpldt0(xm,xn),
inference(demodulation,[status(thm)],[d61,d4]) ).
cnf(d63,plain,
sdtpldt0(sdtpldt0(xp,xm),xr) = sdtpldt0(xn,xm),
inference(demodulation,[status(thm)],[d62,d58]) ).
cnf(d64,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xm))
| ~ aNaturalNumber0(xr)
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(superposition,[status(thm)],[d63,c3]) ).
cnf(d65,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xm))
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[d10,d64]) ).
cnf(d66,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[d65,c3]) ).
cnf(d67,plain,
( ~ aNaturalNumber0(xp)
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[c71,d66]) ).
cnf(d68,plain,
aNaturalNumber0(sdtpldt0(xn,xm)),
inference(resolution,[status(thm)],[c72,d67]) ).
cnf(d69,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm)))
| sdtpldt0(xn,xm) = sdtpldt0(xp,sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[d68,d57]) ).
cnf(d70,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xp,xp),X0) = sdtpldt0(xp,sdtpldt0(xp,X0)) ),
inference(resolution,[status(thm)],[d13,c72]) ).
cnf(d71,plain,
sdtpldt0(sdtpldt0(xp,xp),xr) = sdtpldt0(xp,sdtpldt0(xp,xr)),
inference(resolution,[status(thm)],[d70,d10]) ).
cnf(d72,plain,
sdtpldt0(sdtpldt0(xp,xp),xr) = sdtpldt0(xp,xn),
inference(demodulation,[status(thm)],[d71,d4]) ).
cnf(d73,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xp))
| ~ aNaturalNumber0(xr)
| aNaturalNumber0(sdtpldt0(xp,xn)) ),
inference(superposition,[status(thm)],[d72,c3]) ).
cnf(d74,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xp))
| aNaturalNumber0(sdtpldt0(xp,xn)) ),
inference(resolution,[status(thm)],[d10,d73]) ).
cnf(d75,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp)
| aNaturalNumber0(sdtpldt0(xp,xn)) ),
inference(resolution,[status(thm)],[d74,c3]) ).
cnf(d76,plain,
aNaturalNumber0(sdtpldt0(xp,xn)),
inference(resolution,[status(thm)],[c72,d75]) ).
cnf(d77,plain,
sdtpldt0(xm,sdtpldt0(xp,xn)) = sdtpldt0(sdtpldt0(xp,xn),xm),
inference(resolution,[status(thm)],[d76,d18]) ).
cnf(d78,plain,
sdtpldt0(xm,sdtpldt0(xp,xn)) = sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(demodulation,[status(thm)],[d77,d28]) ).
cnf(d79,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xm,xn),X0) = sdtpldt0(xm,sdtpldt0(xn,X0)) ),
inference(resolution,[status(thm)],[d26,c71]) ).
cnf(d80,plain,
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(xn,xm),X0) = sdtpldt0(xm,sdtpldt0(xn,X0)) ),
inference(demodulation,[status(thm)],[d79,d58]) ).
cnf(d81,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xm,sdtpldt0(xn,xp)),
inference(resolution,[status(thm)],[d80,c72]) ).
cnf(d82,plain,
sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xm,sdtpldt0(xp,xn)),
inference(demodulation,[status(thm)],[d81,d30]) ).
cnf(d83,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) != sdtpldt0(sdtpldt0(xn,xm),xp),
inference(demodulation,[status(thm)],[c81,d19]) ).
cnf(d84,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) != sdtpldt0(xm,sdtpldt0(xp,xn)),
inference(demodulation,[status(thm)],[d83,d82]) ).
cnf(d85,plain,
sdtpldt0(sdtpldt0(xm,xr),xp) != sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(demodulation,[status(thm)],[d84,d78]) ).
cnf(d86,plain,
sdtpldt0(xn,xm) != sdtpldt0(xp,sdtpldt0(xn,xm)),
inference(demodulation,[status(thm)],[d85,d25]) ).
cnf(d87,plain,
~ aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm))),
inference(resolution,[status(thm)],[d86,d69]) ).
cnf(d88,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xn))
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm))) ),
inference(superposition,[status(thm)],[d28,c3]) ).
cnf(d89,plain,
( ~ aNaturalNumber0(sdtpldt0(xp,xn))
| aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm))) ),
inference(resolution,[status(thm)],[c71,d88]) ).
cnf(d90,plain,
aNaturalNumber0(sdtpldt0(xp,sdtpldt0(xn,xm))),
inference(resolution,[status(thm)],[d76,d89]) ).
cnf(d91,plain,
$false,
inference(resolution,[status(thm)],[d90,d87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM495+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 03:00:51 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.52/27.44 % SZS status Theorem for theBenchmark.p
% 5.52/27.44 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------