%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM487+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:42 PM UTC 2026
% Result : Theorem 2.04s 1.02s
% Output : CNFRefutation 2.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 32
% Syntax : Number of formulae : 127 ( 18 unt; 20 def)
% Number of atoms : 432 ( 94 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 537 ( 232 ~; 223 |; 46 &)
% ( 23 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 18 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 101 ( 97 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
=> ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
sdtlseqdt0(xp,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
xr = sdtmndt0(xn,xp),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
( sdtlseqdt0(xr,xn)
& xr != xn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
~ ( sdtlseqdt0(xr,xn)
& xr != xn ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f49,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f52,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f53,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
! [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f57,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f60,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f62,plain,
! [X0] :
( X0 = sdtpldt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f76,plain,
! [W0,W1,W2] :
( W1 = W2
| ( sdtpldt0(W1,W0) != sdtpldt0(W2,W0)
& sdtpldt0(W0,W1) != sdtpldt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f78,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f87,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f88,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ( sdtpldt0(W0,sK0_skl(W1,W0)) = W1
& aNaturalNumber0(sK0_skl(W1,W0)) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f88]) ).
fof(f92,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f93,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f94,plain,
! [W0,W1] :
( ! [W2] :
( ( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2)
| W2 = sdtmndt0(W1,W0) )
& ( ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| W2 != sdtmndt0(W1,W0) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [W0,W1] :
( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2)
| W2 = sdtmndt0(W1,W0) )
& ! [W2] :
( ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| W2 != sdtmndt0(W1,W0) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f96,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) = X1
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f99,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f100,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f103,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(f104,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f149,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(f150,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)],[f149]) ).
fof(f151,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))],[f150]) ).
fof(f152,plain,
! [X0] :
( X0 != sz00
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f164,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f165,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f166,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f169,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f171,plain,
sdtlseqdt0(xp,xn),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f172,plain,
xr = sdtmndt0(xn,xp),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f173,plain,
( ~ sdtlseqdt0(xr,xn)
| xr = xn ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f174,plain,
( ~ sdtlseqdt0(xr,xn)
| xr = xn ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f175,definition,
( sQ0_spl
<=> xr = xn ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ0_spl
| xr = xn ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,definition,
( sQ1_spl
<=> sdtlseqdt0(xr,xn) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f181,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f174,f175,f178]) ).
fof(f182,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f92]) ).
fof(f183,plain,
! [X0,X1] :
( aNaturalNumber0(sdtmndt0(X1,X0))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f96]) ).
fof(f184,plain,
! [X0,X1] :
( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f97]) ).
fof(f192,plain,
( ~ isPrime0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(destructive_equality_resolution,[status(thm)],[f152]) ).
fof(f195,plain,
( ~ sQ0_spl
| xr = sdtmndt0(xr,xp) ),
inference(forward_demodulation,[status(thm)],[f176,f172]) ).
fof(f239,definition,
! [X1] :
( sQ3_spl
<=> ~ aNaturalNumber0(X1) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f240,plain,
! [X0] :
( ~ sQ3_spl
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f239]) ).
fof(f266,plain,
( ~ sQ0_spl
| sdtlseqdt0(xp,xr) ),
inference(forward_demodulation,[status(thm)],[f176,f171]) ).
fof(f268,plain,
! [X0] :
( ~ sQ0_spl
| sdtlseqdt0(X0,xr)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f266,f104]) ).
fof(f270,definition,
( sQ5_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f272,plain,
( sQ5_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f270]) ).
fof(f273,definition,
( sQ6_spl
<=> aNaturalNumber0(xr) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f280,definition,
! [X0] :
( sQ8_spl
<=> ( sdtlseqdt0(X0,xr)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f281,plain,
! [X0] :
( ~ sQ8_spl
| sdtlseqdt0(X0,xr)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f280]) ).
fof(f283,plain,
( ~ sQ0_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f268,f280,f270,f273,f175]) ).
fof(f291,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f272,f166]) ).
fof(f292,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f291]) ).
fof(f298,definition,
( sQ11_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f300,plain,
( sQ11_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f310,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f164]) ).
fof(f311,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f310]) ).
fof(f325,definition,
( sQ14_spl
<=> sdtlseqdt0(xp,xr) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f330,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f182,f53]) ).
fof(f380,plain,
( ~ sQ8_spl
| ~ aNaturalNumber0(xp)
| sdtlseqdt0(xp,xr)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f281,f100]) ).
fof(f393,plain,
( ~ sQ8_spl
| sQ14_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f380,f270,f325,f280]) ).
fof(f468,plain,
! [X0] :
( sdtlseqdt0(X0,xn)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f171,f104]) ).
fof(f474,definition,
! [X0] :
( sQ28_spl
<=> ( sdtlseqdt0(X0,xn)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f475,plain,
! [X0] :
( ~ sQ28_spl
| sdtlseqdt0(X0,xn)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f474]) ).
fof(f477,plain,
( ~ sQ11_spl
| ~ sQ5_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f468,f474,f270,f298]) ).
fof(f490,definition,
( sQ31_spl
<=> sdtlseqdt0(xp,xn) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f520,plain,
~ isPrime0(sz00),
inference(forward_subsumption_resolution,[status(thm)],[f192,f49]) ).
fof(f527,definition,
( sQ36_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( sQ36_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f535,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f49]) ).
fof(f536,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f535]) ).
fof(f733,plain,
( ~ sQ28_spl
| ~ aNaturalNumber0(xp)
| sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f475,f100]) ).
fof(f746,plain,
( ~ sQ28_spl
| sQ31_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f733,f270,f490,f474]) ).
fof(f799,definition,
( sQ64_spl
<=> xp = sz00 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( ~ sQ64_spl
| xp = sz00 ),
inference(component_clause,[status(thm)],[f799]) ).
fof(f843,plain,
( ~ sQ64_spl
| ~ isPrime0(xp) ),
inference(backward_demodulation,[status(thm)],[f800,f520]) ).
fof(f851,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f843,f169]) ).
fof(f852,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f851]) ).
fof(f1013,plain,
( ~ sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f49,f240]) ).
fof(f1018,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1013]) ).
fof(f1278,plain,
( aNaturalNumber0(xr)
| ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f172,f183]) ).
fof(f1279,plain,
( sQ6_spl
| ~ sQ31_spl
| ~ sQ11_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1278,f270,f298,f490,f273]) ).
fof(f1397,plain,
( ~ sQ0_spl
| sdtpldt0(xp,xr) = xr
| ~ sdtlseqdt0(xp,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f195,f184]) ).
fof(f1399,definition,
( sQ112_spl
<=> sdtpldt0(xp,xr) = xr ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
( ~ sQ112_spl
| sdtpldt0(xp,xr) = xr ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1402,plain,
( ~ sQ0_spl
| sQ112_spl
| ~ sQ14_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1397,f270,f273,f325,f1399,f175]) ).
fof(f1621,plain,
( sdtpldt0(xp,xr) = xn
| ~ sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f172,f184]) ).
fof(f1623,definition,
( sQ127_spl
<=> sdtpldt0(xp,xr) = xn ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1624,plain,
( ~ sQ127_spl
| sdtpldt0(xp,xr) = xn ),
inference(component_clause,[status(thm)],[f1623]) ).
fof(f1626,plain,
( sQ127_spl
| ~ sQ31_spl
| ~ sQ11_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1621,f270,f298,f490,f1623]) ).
fof(f1694,plain,
( ~ sQ127_spl
| sdtpldt0(xr,xp) = xn
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f1624,f57]) ).
fof(f1699,plain,
! [X0] :
( ~ sQ127_spl
| X0 = xp
| sdtpldt0(X0,xr) != xn
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f1624,f78]) ).
fof(f1731,definition,
( sQ140_spl
<=> sdtpldt0(xr,xp) = xn ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1732,plain,
( ~ sQ140_spl
| sdtpldt0(xr,xp) = xn ),
inference(component_clause,[status(thm)],[f1731]) ).
fof(f1734,plain,
( ~ sQ127_spl
| sQ140_spl
| ~ sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1694,f273,f270,f1731,f1623]) ).
fof(f1742,definition,
! [X0] :
( sQ142_spl
<=> ( X0 = xp
| sdtpldt0(X0,xr) != xn
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1743,plain,
! [X0] :
( ~ sQ142_spl
| X0 = xp
| sdtpldt0(X0,xr) != xn
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f1742]) ).
fof(f1745,plain,
( ~ sQ127_spl
| ~ sQ5_spl
| sQ142_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1699,f273,f1742,f270,f1623]) ).
fof(f1772,plain,
( ~ sQ140_spl
| ~ aNaturalNumber0(xp)
| sdtlseqdt0(xr,xn)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f1732,f330]) ).
fof(f1816,plain,
( ~ sQ140_spl
| ~ sQ5_spl
| sQ1_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1772,f273,f178,f270,f1731]) ).
fof(f1817,plain,
( ~ sQ112_spl
| ~ sQ127_spl
| xn = xr ),
inference(forward_demodulation,[status(thm)],[f1624,f1400]) ).
fof(f2055,definition,
( sQ174_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2057,plain,
( sQ174_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f2055]) ).
fof(f2063,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2057,f165]) ).
fof(f2064,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f2063]) ).
fof(f2394,plain,
! [X0] :
( ~ sQ142_spl
| ~ sQ112_spl
| ~ sQ127_spl
| X0 = xp
| sdtpldt0(X0,xr) != xr
| ~ aNaturalNumber0(X0) ),
inference(forward_demodulation,[status(thm)],[f1817,f1743]) ).
fof(f2684,plain,
( ~ sQ142_spl
| ~ sQ112_spl
| ~ sQ127_spl
| sz00 = xp
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xr) ),
inference(resolution,[status(thm)],[f62,f2394]) ).
fof(f2690,plain,
( ~ sQ142_spl
| ~ sQ112_spl
| ~ sQ127_spl
| sQ64_spl
| ~ sQ36_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2684,f273,f527,f799,f1623,f1399,f1742]) ).
fof(f2692,plain,
$false,
inference(sat_refutation,[status(thm)],[f181,f283,f292,f311,f393,f477,f536,f746,f852,f1018,f1279,f1402,f1626,f1734,f1745,f1816,f2064,f2690]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM487+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/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:34:04 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 2.04/1.02 % Refutation found
% 2.04/1.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.04/1.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.59/1.04 % Elapsed time: 0.665520 seconds
% 2.59/1.04 % CPU time: 4.922857 seconds
% 2.59/1.04 % Total memory used: 135.242 MB
% 2.59/1.04 % Net memory used: 131.030 MB
%------------------------------------------------------------------------------