%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM504+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:13 AM UTC 2026
% Result : Theorem 174.12s 23.51s
% Output : CNFRefutation 174.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 9
% Syntax : Number of formulae : 119 ( 92 unt; 0 def)
% Number of atoms : 250 ( 125 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 193 ( 62 ~; 31 |; 96 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 15 con; 0-2 aty)
% Number of variables : 35 ( 0 sgn 12 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsB_02,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mSortsB_02) ).
fof(mLEAsym,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLEAsym) ).
fof(m__1837,axiom,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__1860,axiom,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10
& xp != sz00 ),
file('theBenchmark.p',m__1860) ).
fof(m__2287,axiom,
( sdtlseqdt0(xm,xp)
& ? [W0] :
( sdtpldt0(xm,W0) = xp
& aNaturalNumber0(W0) )
& xm != xp
& sdtlseqdt0(xn,xp)
& ? [W0] :
( sdtpldt0(xn,W0) = xp
& aNaturalNumber0(W0) )
& xn != xp ),
file('theBenchmark.p',m__2287) ).
fof(m__2306,axiom,
( xk = sdtsldt0(sdtasdt0(xn,xm),xp)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& aNaturalNumber0(xk) ),
file('theBenchmark.p',m__2306) ).
fof(m__2362,axiom,
( doDivides0(xr,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xr,W0)
& aNaturalNumber0(W0) )
& ? [W0] :
( sdtpldt0(xr,W0) = xk
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__2362) ).
fof(m__2389,axiom,
( sdtlseqdt0(xp,xk)
& ? [W0] :
( sdtpldt0(xp,W0) = xk
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__2389) ).
fof(m__2414,axiom,
( sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& ? [W0] :
( sdtpldt0(sdtasdt0(xp,xm),W0) = sdtasdt0(xp,xk)
& aNaturalNumber0(W0) )
& sdtasdt0(xp,xm) != sdtasdt0(xp,xk)
& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) = sdtasdt0(xp,xm)
& aNaturalNumber0(W0) )
& sdtasdt0(xn,xm) != sdtasdt0(xp,xm) ),
file('theBenchmark.p',m__2414) ).
fof(nnf_50,plain,
( sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& ? [W0] :
( sdtasdt0(xp,xk) = sdtpldt0(sdtasdt0(xp,xm),W0)
& aNaturalNumber0(W0) )
& sdtasdt0(xp,xk) != sdtasdt0(xp,xm)
& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ? [X0] :
( sdtasdt0(xp,xm) = sdtpldt0(sdtasdt0(xn,xm),X0)
& aNaturalNumber0(X0) )
& sdtasdt0(xp,xm) != sdtasdt0(xn,xm) ),
inference(fof_nnf,[status(thm)],[m__2414]) ).
fof(sk_m__2414,plain,
( sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& sdtasdt0(xp,xk) = sdtpldt0(sdtasdt0(xp,xm),sK0)
& aNaturalNumber0(sK0)
& sdtasdt0(xp,xk) != sdtasdt0(xp,xm)
& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& sdtasdt0(xp,xm) = sdtpldt0(sdtasdt0(xn,xm),sK1)
& aNaturalNumber0(sK1)
& sdtasdt0(xp,xm) != sdtasdt0(xn,xm) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(X0,sK1),skolemize(W0,sK0)],[nnf_50]) ).
cnf(c_302,plain,
sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk)),
inference(split_conjunct,[status(thm)],[sk_m__2414]) ).
cnf(c_303,plain,
sdtasdt0(xp,xk) = sdtpldt0(sdtasdt0(xp,xm),sK0),
inference(split_conjunct,[status(thm)],[sk_m__2414]) ).
cnf(c_307,plain,
sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm)),
inference(split_conjunct,[status(thm)],[sk_m__2414]) ).
cnf(c_308,plain,
sdtasdt0(xp,xm) = sdtpldt0(sdtasdt0(xn,xm),sK1),
inference(split_conjunct,[status(thm)],[sk_m__2414]) ).
cnf(c_309,plain,
sdtpldt0(sdtasdt0(xn,xm),sK1) = sdtasdt0(xp,xm),
inference(copy,[status(thm)],[c_308]) ).
cnf(c_311,plain,
sdtasdt0(xp,xm) != sdtasdt0(xn,xm),
inference(split_conjunct,[status(thm)],[sk_m__2414]) ).
cnf(c_312,plain,
sdtasdt0(xn,xm) != sdtasdt0(xp,xm),
inference(copy,[status(thm)],[c_311]) ).
fof(nnf_49,plain,
( sdtlseqdt0(xp,xk)
& ? [W0] :
( sdtpldt0(xp,W0) = xk
& aNaturalNumber0(W0) ) ),
inference(fof_nnf,[status(thm)],[m__2389]) ).
fof(sk_m__2389,plain,
( sdtlseqdt0(xp,xk)
& sdtpldt0(xp,sK2) = xk
& aNaturalNumber0(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(W0,sK2)],[nnf_49]) ).
cnf(c_314,plain,
sdtpldt0(xp,sK2) = xk,
inference(split_conjunct,[status(thm)],[sk_m__2389]) ).
cnf(c_315,plain,
xk = sdtpldt0(xp,sK2),
inference(copy,[status(thm)],[c_314]) ).
fof(nnf_48,plain,
( doDivides0(xr,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xr,W0) = sdtasdt0(xn,xm)
& aNaturalNumber0(W0) )
& ? [X0] :
( sdtpldt0(xr,X0) = xk
& aNaturalNumber0(X0) ) ),
inference(fof_nnf,[status(thm)],[m__2362]) ).
fof(sk_m__2362,plain,
( doDivides0(xr,sdtasdt0(xn,xm))
& sdtasdt0(xr,sK3) = sdtasdt0(xn,xm)
& aNaturalNumber0(sK3)
& sdtpldt0(xr,sK6) = xk
& aNaturalNumber0(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK3]),skolemize(X0,sK6),skolemize(W0,sK3)],[nnf_48]) ).
cnf(c_318,plain,
sdtasdt0(xr,sK3) = sdtasdt0(xn,xm),
inference(split_conjunct,[status(thm)],[sk_m__2362]) ).
cnf(c_341,plain,
sdtasdt0(xp,xk) = sdtasdt0(xn,xm),
inference(clausify,[status(thm)],[m__2306]) ).
cnf(c_24060,plain,
sdtasdt0(xp,sdtpldt0(xp,sK2)) = sdtasdt0(xn,xm),
inference(paramod,[status(thm)],[c_315,c_341]) ).
cnf(c_342,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,sdtpldt0(xp,sK2)),
inference(copy,[status(thm)],[c_24060]) ).
fof(nnf_43,plain,
( sdtlseqdt0(xm,xp)
& ? [W0] :
( sdtpldt0(xm,W0) = xp
& aNaturalNumber0(W0) )
& xp != xm
& sdtlseqdt0(xn,xp)
& ? [X0] :
( sdtpldt0(xn,X0) = xp
& aNaturalNumber0(X0) )
& xp != xn ),
inference(fof_nnf,[status(thm)],[m__2287]) ).
fof(sk_m__2287,plain,
( sdtlseqdt0(xm,xp)
& sdtpldt0(xm,sK4) = xp
& aNaturalNumber0(sK4)
& xp != xm
& sdtlseqdt0(xn,xp)
& sdtpldt0(xn,sK7) = xp
& aNaturalNumber0(sK7)
& xp != xn ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK4]),skolemize(X0,sK7),skolemize(W0,sK4)],[nnf_43]) ).
cnf(c_346,plain,
sdtpldt0(xm,sK4) = xp,
inference(split_conjunct,[status(thm)],[sk_m__2287]) ).
cnf(c_347,plain,
xp = sdtpldt0(xm,sK4),
inference(copy,[status(thm)],[c_346]) ).
fof(nnf_40,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xp,W0) = sdtasdt0(xn,xm)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [X0] :
( xp = X0
| sz10 = X0
| ( ~ doDivides0(X0,xp)
& ! [W1] :
( sdtasdt0(X0,W1) != xp
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(X0) )
& xp != sz10
& xp != sz00 ),
inference(fof_nnf,[status(thm)],[m__1860]) ).
fof(sk_m__1860_sk,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& sdtasdt0(xp,sK5) = sdtasdt0(xn,xm)
& aNaturalNumber0(sK5)
& isPrime0(xp)
& ! [X0] :
( xp = X0
| sz10 = X0
| ( ~ doDivides0(X0,xp)
& ! [W1] :
( sdtasdt0(X0,W1) != xp
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(X0) )
& xp != sz10
& xp != sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(W0,sK5)],[nnf_40]) ).
fof(sk_m__1860,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& sdtasdt0(xp,sK5) = sdtasdt0(xn,xm)
& aNaturalNumber0(sK5)
& isPrime0(xp)
& ! [VAR_0] :
( xp = VAR_0
| sz10 = VAR_0
| ~ doDivides0(VAR_0,xp)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( xp = VAR_0
| sz10 = VAR_0
| sdtasdt0(VAR_0,VAR_1) != xp
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& xp != sz10
& xp != sz00 ),
inference(cnf_transformation,[status(thm)],[sk_m__1860_sk]) ).
cnf(c_368,plain,
sdtasdt0(xp,sK5) = sdtasdt0(xn,xm),
inference(split_conjunct,[status(thm)],[sk_m__1860]) ).
cnf(c_24061,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtasdt0(xn,xm),
inference(paramod,[status(thm)],[c_347,c_368]) ).
cnf(c_24062,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtasdt0(xp,sdtpldt0(xp,sK2)),
inference(paramod,[status(thm)],[c_342,c_24061]) ).
cnf(c_24063,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)),
inference(paramod,[status(thm)],[c_347,c_24062]) ).
cnf(c_24064,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)),
inference(paramod,[status(thm)],[c_347,c_24063]) ).
cnf(c_369,plain,
sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)) = sdtasdt0(sdtpldt0(xm,sK4),sK5),
inference(copy,[status(thm)],[c_24064]) ).
cnf(c_595,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_596,plain,
aNaturalNumber0(sdtpldt0(xm,sK4)),
inference(paramod,[status(thm)],[c_347,c_595]) ).
cnf(c_597,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_598,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_627,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_656,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_24065,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sdtasdt0(xp,xk)),
inference(paramod,[status(thm)],[c_347,c_302]) ).
cnf(c_24066,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sdtasdt0(sdtpldt0(xm,sK4),xk)),
inference(paramod,[status(thm)],[c_347,c_24065]) ).
cnf(c_24067,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2))),
inference(paramod,[status(thm)],[c_315,c_24066]) ).
cnf(c_24068,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2))),
inference(paramod,[status(thm)],[c_347,c_24067]) ).
cnf(c_1227,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sdtasdt0(sdtpldt0(xm,sK4),sK5)),
inference(paramod,[status(thm)],[c_369,c_24068]) ).
cnf(c_24069,plain,
sdtasdt0(sdtpldt0(xm,sK4),xk) = sdtpldt0(sdtasdt0(xp,xm),sK0),
inference(paramod,[status(thm)],[c_347,c_303]) ).
cnf(c_24070,plain,
sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)) = sdtpldt0(sdtasdt0(xp,xm),sK0),
inference(paramod,[status(thm)],[c_315,c_24069]) ).
cnf(c_24071,plain,
sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)) = sdtpldt0(sdtasdt0(xp,xm),sK0),
inference(paramod,[status(thm)],[c_347,c_24070]) ).
cnf(c_24072,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtpldt0(sdtasdt0(xp,xm),sK0),
inference(paramod,[status(thm)],[c_369,c_24071]) ).
cnf(c_1229,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) = sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0),
inference(paramod,[status(thm)],[c_347,c_24072]) ).
cnf(c_24073,plain,
sdtasdt0(xr,sK3) = sdtasdt0(xp,sdtpldt0(xp,sK2)),
inference(paramod,[status(thm)],[c_342,c_318]) ).
cnf(c_24074,plain,
sdtasdt0(xr,sK3) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)),
inference(paramod,[status(thm)],[c_347,c_24073]) ).
cnf(c_24075,plain,
sdtasdt0(xr,sK3) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)),
inference(paramod,[status(thm)],[c_347,c_24074]) ).
cnf(c_24076,plain,
sdtasdt0(xr,sK3) = sdtasdt0(sdtpldt0(xm,sK4),sK5),
inference(paramod,[status(thm)],[c_369,c_24075]) ).
cnf(c_24077,plain,
sdtasdt0(xr,sK3) = sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0),
inference(paramod,[status(thm)],[c_1229,c_24076]) ).
cnf(c_1250,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0) = sdtasdt0(xr,sK3),
inference(copy,[status(thm)],[c_24077]) ).
cnf(c_24078,plain,
sdtasdt0(xp,sdtpldt0(xp,sK2)) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_342,c_312]) ).
cnf(c_24079,plain,
sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_347,c_24078]) ).
cnf(c_24080,plain,
sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_347,c_24079]) ).
cnf(c_24081,plain,
sdtasdt0(sdtpldt0(xm,sK4),sK5) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_369,c_24080]) ).
cnf(c_24082,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_1229,c_24081]) ).
cnf(c_24083,plain,
sdtasdt0(xr,sK3) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_1250,c_24082]) ).
cnf(c_24084,plain,
sdtasdt0(xr,sK3) != sdtasdt0(sdtpldt0(xm,sK4),xm),
inference(paramod,[status(thm)],[c_347,c_24083]) ).
cnf(c_1252,plain,
sdtasdt0(sdtpldt0(xm,sK4),xm) != sdtasdt0(xr,sK3),
inference(copy,[status(thm)],[c_24084]) ).
cnf(c_24085,plain,
sdtpldt0(sdtasdt0(xp,sdtpldt0(xp,sK2)),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_342,c_309]) ).
cnf(c_24086,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_347,c_24085]) ).
cnf(c_24087,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_347,c_24086]) ).
cnf(c_24088,plain,
sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),sK5),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_369,c_24087]) ).
cnf(c_24089,plain,
sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_1229,c_24088]) ).
cnf(c_24090,plain,
sdtpldt0(sdtasdt0(xr,sK3),sK1) = sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_1250,c_24089]) ).
cnf(c_24091,plain,
sdtpldt0(sdtasdt0(xr,sK3),sK1) = sdtasdt0(sdtpldt0(xm,sK4),xm),
inference(paramod,[status(thm)],[c_347,c_24090]) ).
cnf(c_1253,plain,
sdtasdt0(sdtpldt0(xm,sK4),xm) = sdtpldt0(sdtasdt0(xr,sK3),sK1),
inference(copy,[status(thm)],[c_24091]) ).
cnf(c_24092,plain,
sdtlseqdt0(sdtasdt0(xp,sdtpldt0(xp,sK2)),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_342,c_307]) ).
cnf(c_24093,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_347,c_24092]) ).
cnf(c_24094,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_347,c_24093]) ).
cnf(c_24095,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xm,sK4),sK5),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_369,c_24094]) ).
cnf(c_24096,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_1229,c_24095]) ).
cnf(c_24097,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0),sdtasdt0(xp,xm)),
inference(paramod,[status(thm)],[c_1253,c_24096]) ).
cnf(c_24098,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0),sdtasdt0(sdtpldt0(xm,sK4),xm)),
inference(paramod,[status(thm)],[c_347,c_24097]) ).
cnf(c_1254,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0),sdtpldt0(sdtasdt0(xr,sK3),sK1)),
inference(paramod,[status(thm)],[c_1253,c_24098]) ).
cnf(c_24099,plain,
sdtasdt0(xn,xm) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(xp,sK2)),
inference(paramod,[status(thm)],[c_347,c_342]) ).
cnf(c_24100,plain,
sdtasdt0(xn,xm) = sdtasdt0(sdtpldt0(xm,sK4),sdtpldt0(sdtpldt0(xm,sK4),sK2)),
inference(paramod,[status(thm)],[c_347,c_24099]) ).
cnf(c_24101,plain,
sdtasdt0(xn,xm) = sdtasdt0(sdtpldt0(xm,sK4),sK5),
inference(paramod,[status(thm)],[c_369,c_24100]) ).
cnf(c_24102,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0),
inference(paramod,[status(thm)],[c_1229,c_24101]) ).
cnf(c_24103,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0),
inference(paramod,[status(thm)],[c_1253,c_24102]) ).
cnf(c_1257,plain,
sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0) = sdtasdt0(xn,xm),
inference(copy,[status(thm)],[c_24103]) ).
cnf(c_24104,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sdtasdt0(sdtpldt0(xm,sK4),sK5)),
inference(paramod,[status(thm)],[c_1253,c_1227]) ).
cnf(c_24105,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sdtpldt0(sdtasdt0(sdtpldt0(xm,sK4),xm),sK0)),
inference(paramod,[status(thm)],[c_1229,c_24104]) ).
cnf(c_24106,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0)),
inference(paramod,[status(thm)],[c_1253,c_24105]) ).
cnf(c_2376,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sdtasdt0(xn,xm)),
inference(paramod,[status(thm)],[c_1257,c_24106]) ).
cnf(c_2380,plain,
sdtpldt0(sdtasdt0(xr,sK3),sK1) != sdtasdt0(xr,sK3),
inference(paramod,[status(thm)],[c_1253,c_1252]) ).
cnf(c_24107,plain,
sdtpldt0(sdtpldt0(sdtasdt0(xr,sK3),sK1),sK0) = sdtasdt0(xr,sK3),
inference(paramod,[status(thm)],[c_1253,c_1250]) ).
cnf(c_24108,plain,
sdtasdt0(xn,xm) = sdtasdt0(xr,sK3),
inference(paramod,[status(thm)],[c_1257,c_24107]) ).
cnf(c_2381,plain,
sdtasdt0(xr,sK3) = sdtasdt0(xn,xm),
inference(copy,[status(thm)],[c_24108]) ).
cnf(c_24109,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xn,xm),sK1),sK0),sdtpldt0(sdtasdt0(xr,sK3),sK1)),
inference(paramod,[status(thm)],[c_2381,c_1254]) ).
cnf(c_2382,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xn,xm),sK1),sK0),sdtpldt0(sdtasdt0(xn,xm),sK1)),
inference(paramod,[status(thm)],[c_2381,c_24109]) ).
cnf(c_24110,plain,
sdtpldt0(sdtasdt0(xn,xm),sK1) != sdtasdt0(xr,sK3),
inference(paramod,[status(thm)],[c_2381,c_2380]) ).
cnf(c_2878,plain,
sdtpldt0(sdtasdt0(xn,xm),sK1) != sdtasdt0(xn,xm),
inference(paramod,[status(thm)],[c_2381,c_24110]) ).
cnf(c_2879,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xn,xm),sK1),sdtasdt0(xn,xm)),
inference(paramod,[status(thm)],[c_2381,c_2376]) ).
cnf(c_2880,plain,
sdtpldt0(sdtpldt0(sdtasdt0(xn,xm),sK1),sK0) = sdtasdt0(xn,xm),
inference(paramod,[status(thm)],[c_2381,c_1257]) ).
cnf(c_2881,plain,
sdtasdt0(sdtpldt0(xm,sK4),xm) = sdtpldt0(sdtasdt0(xn,xm),sK1),
inference(paramod,[status(thm)],[c_2381,c_1253]) ).
cnf(c_2913,plain,
sdtlseqdt0(sdtasdt0(xn,xm),sdtpldt0(sdtasdt0(xn,xm),sK1)),
inference(paramod,[status(thm)],[c_2880,c_2382]) ).
cnf(c_4106,plain,
( aNaturalNumber0(sdtasdt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_656,c_598]) ).
cnf(c_4120,plain,
( aNaturalNumber0(sdtasdt0(A,xm))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_656,c_597]) ).
cnf(c_24111,plain,
( sdtpldt0(sdtasdt0(xn,xm),sK1) = sdtasdt0(xn,xm)
| ~ sdtlseqdt0(sdtasdt0(xn,xm),sdtpldt0(sdtasdt0(xn,xm),sK1))
| ~ aNaturalNumber0(sdtpldt0(sdtasdt0(xn,xm),sK1))
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_2879,c_627]) ).
cnf(c_24112,plain,
( sdtpldt0(sdtasdt0(xn,xm),sK1) = sdtasdt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(sdtasdt0(xn,xm),sK1))
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_2913,c_24111]) ).
cnf(c_7372,plain,
( ~ aNaturalNumber0(sdtpldt0(sdtasdt0(xn,xm),sK1))
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_2878,c_24112]) ).
cnf(c_16354,plain,
aNaturalNumber0(sdtasdt0(xn,xm)),
inference(resolve,[status(thm)],[c_4106,c_597]) ).
cnf(c_16383,plain,
~ aNaturalNumber0(sdtpldt0(sdtasdt0(xn,xm),sK1)),
inference(resolve,[status(thm)],[c_16354,c_7372]) ).
cnf(c_24113,plain,
aNaturalNumber0(sdtasdt0(sdtpldt0(xm,sK4),xm)),
inference(resolve,[status(thm)],[c_4120,c_596]) ).
cnf(c_24114,plain,
aNaturalNumber0(sdtpldt0(sdtasdt0(xn,xm),sK1)),
inference(paramod,[status(thm)],[c_2881,c_24113]) ).
cnf(c_24059,plain,
$false,
inference(resolve,[status(thm)],[c_16383,c_24114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM504+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.46 % Computer : n011.cluster.edu
% 0.21/0.46 % Model : x86_64 x86_64
% 0.21/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.46 % Memory : 8046.5625MB
% 0.21/0.46 % OS : Linux 6.8.0-71-generic
% 0.21/0.46 % CPULimit : 300
% 0.21/0.46 % WCLimit : 300
% 0.21/0.46 % DateTime : Sat Sep 26 03:01:29 UTC 2026
% 0.21/0.46 % CPUTime :
% 0.21/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.21/0.46 % Process 3650145 was started by sandbox on n011,
% 0.21/0.46 % Sat Sep 26 03:01:29 2026
% 0.21/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.24/0.53
% 0.24/0.53 % From the command line: assign(max_seconds, 300).
% 174.12/23.51
% 174.12/23.51 % given #500 (I,wt=52): 1081 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sdtasdt0(B,C) != sdtasdt0(A,A) | -iLess0(sdtpldt0(sdtpldt0(A,A),B),sdtpldt0(sdtpldt0(xn,xm),sdtpldt0(xm,c3))) | sdtasdt0(B,f7(A,A,B)) = A | sdtasdt0(B,f8(A,A,B)) = A | sz00 = B | sz10 = B | f3(B) != B. [factor(250,a,b),rewrite([347(12)])].
% 174.12/23.51
% 174.12/23.51 % given #1000 (I,wt=45): 1704 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sz00 = C | sz10 = C | aNaturalNumber0(f6(A,B,C)) | sdtasdt0(C,B) != sdtasdt0(A,B) | -iLess0(sdtpldt0(sdtpldt0(A,B),C),sdtpldt0(sdtpldt0(xn,xm),sdtpldt0(xm,c3))) | doDivides0(C,A) | aNaturalNumber0(f8(A,B,C)). [factor(546,b,g)].
% 174.12/23.51
% 174.12/23.51 % given #1500 (I,wt=44): 2357 -aNaturalNumber0(A) | -aNaturalNumber0(B) | sdtasdt0(A,B) != sdtasdt0(B,B) | -iLess0(sdtpldt0(sdtpldt0(A,B),B),sdtpldt0(sdtpldt0(xn,xm),sdtpldt0(xm,c3))) | aNaturalNumber0(f7(A,B,B)) | aNaturalNumber0(f8(A,B,B)) | sz00 = B | sz10 = B | f3(B) != B. [factor(1210,b,c),flip(c)].
% 174.12/23.51
% 174.12/23.51 % given #2000 (T,wt=4): 6577 aNaturalNumber0(sdtasdt0(c6,c6)). [resolve(1886,a,319,a)].
% 174.12/23.51
% 174.12/23.51 % given #2500 (F,wt=7): 14872 sdtpldt0(xr,f2(xr,xr)) != sz00. [resolve(9304,a,3485,a)].
% 174.12/23.51
% 174.12/23.51 % SZS status Theorem for theBenchmark
% 174.12/23.51
% 174.12/23.51 % Proof 1 at 20.64 (+ 2.16) seconds.
% 174.12/23.51 % Length of proof is 53.
% 174.12/23.51 % Level of proof is 14.
% 174.12/23.51 % Maximum clause weight is 15.000.
% 174.12/23.51 % Given clauses 2655.
% 174.12/23.51
% 174.12/23.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------