%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM518+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 01:40:49 PM UTC 2026
% Result : Theorem 8.02s 1.46s
% Output : CNFRefutation 8.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 35
% Syntax : Number of formulae : 135 ( 26 unt; 21 def)
% Number of atoms : 403 ( 85 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 451 ( 183 ~; 190 |; 44 &)
% ( 23 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 20 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 63 ( 62 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,W1)
& W0 != sz00 )
=> ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( W1 != sz00
& doDivides0(W0,W1) )
=> sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,definition,
! [W0] :
( aNaturalNumber0(W0)
=> ( isPrime0(W0)
<=> ( ! [W1] :
( ( doDivides0(W1,W0)
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
~ sdtlseqdt0(xp,xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
( sdtlseqdt0(xm,xp)
& xm != xp
& sdtlseqdt0(xn,xp)
& xn != xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
( isPrime0(xr)
& doDivides0(xr,xk)
& aNaturalNumber0(xr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
doDivides0(xr,xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
& sdtsldt0(xn,xr) != xn ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
( doDivides0(xp,xm)
| doDivides0(xp,sdtsldt0(xn,xr)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
( doDivides0(xp,xm)
| doDivides0(xp,xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ ( doDivides0(xp,xm)
| doDivides0(xp,xn) ),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f61,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f82,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f83,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f113,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f114,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f116,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f145,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f146,plain,
! [W0,W1] :
( ! [W2] :
( ( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2)
| W2 = sdtsldt0(W1,W0) )
& ( ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| W2 != sdtsldt0(W1,W0) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
! [W0,W1] :
( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2)
| W2 = sdtsldt0(W1,W0) )
& ! [W2] :
( ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| W2 != sdtsldt0(W1,W0) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2] :
( X1 = sdtasdt0(X0,X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f157,plain,
! [W0,W1] :
( sdtlseqdt0(W0,W1)
| W1 = sz00
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f158,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| X1 = sz00
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f161,plain,
! [W0] :
( ( isPrime0(W0)
<=> ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 ) )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f162,plain,
! [W0] :
( ( ( ? [W1] :
( W1 != W0
& W1 != sz10
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| W0 = sz10
| W0 = sz00
| isPrime0(W0) )
& ( ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
! [W0] :
( ( ( ( sK2_skl(W0) != W0
& sK2_skl(W0) != sz10
& doDivides0(sK2_skl(W0),W0)
& aNaturalNumber0(sK2_skl(W0)) )
| W0 = sz10
| W0 = sz00
| isPrime0(W0) )
& ( ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f162]) ).
fof(f164,plain,
! [X0] :
( X0 != sz00
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f176,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f177,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f178,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f182,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f183,plain,
~ sdtlseqdt0(xp,xn),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f186,plain,
sdtlseqdt0(xn,xp),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f195,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f197,plain,
isPrime0(xr),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f203,plain,
doDivides0(xr,xn),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f205,plain,
sdtlseqdt0(sdtsldt0(xn,xr),xn),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f207,plain,
( doDivides0(xp,xm)
| doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f208,plain,
( ~ doDivides0(xp,xm)
& ~ doDivides0(xp,xn) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f209,plain,
~ doDivides0(xp,xn),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f210,plain,
~ doDivides0(xp,xm),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ0_spl
<=> doDivides0(xr,xn) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f213,plain,
( sQ0_spl
| ~ doDivides0(xr,xn) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f218,definition,
( sQ2_spl
<=> doDivides0(xp,sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( ~ sQ2_spl
| doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(component_clause,[status(thm)],[f218]) ).
fof(f221,definition,
( sQ3_spl
<=> doDivides0(xp,xm) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( ~ sQ3_spl
| doDivides0(xp,xm) ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f224,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f207,f218,f221]) ).
fof(f232,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f148]) ).
fof(f233,plain,
! [X0,X1] :
( X1 = sdtasdt0(X0,sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f149]) ).
fof(f235,plain,
( ~ isPrime0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(destructive_equality_resolution,[status(thm)],[f164]) ).
fof(f241,definition,
( sQ4_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( sQ4_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f241]) ).
fof(f254,definition,
( sQ8_spl
<=> aNaturalNumber0(xr) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( sQ8_spl
| ~ aNaturalNumber0(xr) ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f261,definition,
( sQ10_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( sQ10_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f264,definition,
( sQ11_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( ~ sQ11_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f264]) ).
fof(f288,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f256,f195]) ).
fof(f289,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f288]) ).
fof(f290,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f243,f178]) ).
fof(f291,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f290]) ).
fof(f316,definition,
( sQ20_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f318,plain,
( sQ20_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f316]) ).
fof(f327,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f318,f177]) ).
fof(f328,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f327]) ).
fof(f336,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f176]) ).
fof(f337,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f336]) ).
fof(f346,definition,
( sQ23_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( sQ23_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f346]) ).
fof(f409,definition,
( sQ27_spl
<=> sdtasdt0(xn,xm) = xn ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f410,plain,
( ~ sQ27_spl
| sdtasdt0(xn,xm) = xn ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f411,plain,
( sQ27_spl
| sdtasdt0(xn,xm) != xn ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f442,plain,
( ~ sQ27_spl
| doDivides0(xp,xn) ),
inference(backward_demodulation,[status(thm)],[f410,f182]) ).
fof(f494,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f209]) ).
fof(f495,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f494]) ).
fof(f689,definition,
( sQ65_spl
<=> isPrime0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ65_spl
| ~ isPrime0(sz00) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( ~ sQ65_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f235,f346,f689]) ).
fof(f707,plain,
( ~ sQ2_spl
| sdtlseqdt0(xp,sdtsldt0(xn,xr))
| sdtsldt0(xn,xr) = sz00
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f158,f219]) ).
fof(f710,definition,
( sQ67_spl
<=> aNaturalNumber0(sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( sQ67_spl
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(component_clause,[status(thm)],[f710]) ).
fof(f713,definition,
( sQ68_spl
<=> sdtsldt0(xn,xr) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( ~ sQ68_spl
| sdtsldt0(xn,xr) = sz00 ),
inference(component_clause,[status(thm)],[f713]) ).
fof(f716,definition,
( sQ69_spl
<=> sdtlseqdt0(xp,sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( ~ sQ69_spl
| sdtlseqdt0(xp,sdtsldt0(xn,xr)) ),
inference(component_clause,[status(thm)],[f716]) ).
fof(f719,plain,
( ~ sQ2_spl
| sQ69_spl
| sQ68_spl
| ~ sQ67_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f707,f241,f710,f713,f716,f218]) ).
fof(f722,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f222,f210]) ).
fof(f723,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f738,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f61,f348]) ).
fof(f739,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f738]) ).
fof(f893,plain,
! [X0] :
( ~ sQ11_spl
| sz00 = sdtasdt0(xn,X0)
| ~ aNaturalNumber0(X0) ),
inference(backward_demodulation,[status(thm)],[f265,f84]) ).
fof(f903,plain,
! [X0] :
( ~ sQ11_spl
| xn = sdtasdt0(xn,X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_demodulation,[status(thm)],[f265,f893]) ).
fof(f1062,plain,
( sQ27_spl
| ~ sQ11_spl
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f903,f411]) ).
fof(f1063,plain,
( sQ27_spl
| ~ sQ11_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1062,f316,f264,f409]) ).
fof(f1109,plain,
! [X0] :
( sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f116,f186]) ).
fof(f1117,definition,
! [X0] :
( sQ100_spl
<=> ( sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1118,plain,
! [X0] :
( ~ sQ100_spl
| sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f1117]) ).
fof(f1120,plain,
( ~ sQ4_spl
| ~ sQ10_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1109,f1117,f261,f241]) ).
fof(f1260,definition,
( sQ113_spl
<=> sz00 = xr ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1261,plain,
( ~ sQ113_spl
| sz00 = xr ),
inference(component_clause,[status(thm)],[f1260]) ).
fof(f1266,plain,
( sQ65_spl
| ~ sQ113_spl
| ~ isPrime0(xr) ),
inference(backward_demodulation,[status(thm)],[f1261,f691]) ).
fof(f1271,plain,
( sQ65_spl
| ~ sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1266,f197]) ).
fof(f1272,plain,
( sQ65_spl
| ~ sQ113_spl ),
inference(contradiction_clause,[status(thm)],[f1271]) ).
fof(f1772,plain,
( sQ67_spl
| ~ doDivides0(xr,xn)
| xr = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(resolution,[status(thm)],[f712,f232]) ).
fof(f1773,plain,
( sQ67_spl
| ~ sQ0_spl
| sQ113_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1772,f254,f261,f1260,f211,f710]) ).
fof(f1774,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f213,f203]) ).
fof(f1775,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1774]) ).
fof(f1846,plain,
( ~ sQ69_spl
| sdtsldt0(xn,xr) = xp
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolution,[status(thm)],[f717,f114]) ).
fof(f1847,definition,
( sQ167_spl
<=> xp = sdtsldt0(xn,xr) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1848,plain,
( ~ sQ167_spl
| xp = sdtsldt0(xn,xr) ),
inference(component_clause,[status(thm)],[f1847]) ).
fof(f1858,definition,
( sQ170_spl
<=> sdtlseqdt0(sdtsldt0(xn,xr),xp) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1861,plain,
( ~ sQ69_spl
| sQ167_spl
| ~ sQ170_spl
| ~ sQ4_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1846,f710,f241,f1858,f1847,f716]) ).
fof(f3963,plain,
( ~ sQ68_spl
| xn = sdtasdt0(xr,sz00)
| ~ doDivides0(xr,xn)
| xr = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f714,f233]) ).
fof(f3966,definition,
( sQ307_spl
<=> xn = sdtasdt0(xr,sz00) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f3967,plain,
( ~ sQ307_spl
| xn = sdtasdt0(xr,sz00) ),
inference(component_clause,[status(thm)],[f3966]) ).
fof(f3969,plain,
( ~ sQ68_spl
| sQ307_spl
| ~ sQ0_spl
| sQ113_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3963,f254,f261,f1260,f211,f3966,f713]) ).
fof(f4002,plain,
( ~ sQ307_spl
| xn = sz00
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f3967,f83]) ).
fof(f4018,plain,
( ~ sQ307_spl
| sQ11_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4002,f254,f264,f3966]) ).
fof(f7054,plain,
( ~ sQ100_spl
| sdtlseqdt0(sdtsldt0(xn,xr),xp)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolution,[status(thm)],[f1118,f205]) ).
fof(f7073,plain,
( ~ sQ100_spl
| sQ170_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f7054,f710,f1858,f1117]) ).
fof(f7531,plain,
( ~ sQ167_spl
| sdtlseqdt0(xp,xn) ),
inference(backward_demodulation,[status(thm)],[f1848,f205]) ).
fof(f7537,plain,
( ~ sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7531,f183]) ).
fof(f7538,plain,
~ sQ167_spl,
inference(contradiction_clause,[status(thm)],[f7537]) ).
fof(f7539,plain,
$false,
inference(sat_refutation,[status(thm)],[f224,f289,f291,f328,f337,f495,f692,f719,f723,f739,f1063,f1120,f1272,f1773,f1775,f1861,f3969,f4018,f7073,f7538]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM518+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:36:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 8.02/1.46 % Refutation found
% 8.02/1.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.02/1.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.02/1.48 % Elapsed time: 1.110402 seconds
% 8.02/1.48 % CPU time: 8.427939 seconds
% 8.02/1.48 % Total memory used: 159.195 MB
% 8.02/1.48 % Net memory used: 152.564 MB
%------------------------------------------------------------------------------