%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM471+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 : n016.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:38 PM UTC 2026
% Result : Theorem 260.42s 33.49s
% Output : CNFRefutation 260.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 35
% Syntax : Number of formulae : 150 ( 24 unt; 22 def)
% Number of atoms : 570 ( 125 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 725 ( 305 ~; 334 |; 45 &)
% ( 24 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 21 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 139 ( 136 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 != sz00
=> ! [W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W1,W0) = sdtasdt0(W2,W0)
| sdtasdt0(W0,W1) = sdtasdt0(W0,W2) )
=> W1 = W2 ) ) ) ),
file('/export/starexec/sandbox/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/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(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& W1 != W2
& W0 != sz00 )
=> ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(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(f34,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xl) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
( doDivides0(xl,sdtpldt0(xm,xn))
& doDivides0(xl,xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
xl != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
xp = sdtsldt0(xm,xl),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
xq = sdtsldt0(sdtpldt0(xm,xn),xl),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,conjecture,
sdtlseqdt0(xp,xq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
~ sdtlseqdt0(xp,xq),
inference(negated_conjecture,[status(cth)],[f39]) ).
fof(f47,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f48,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f50,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f74,plain,
! [W0] :
( ! [W1,W2] :
( W1 = W2
| ( sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f75,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f82,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(f83,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)],[f82]) ).
fof(f84,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))],[f83]) ).
fof(f87,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f96,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f97,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f100,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f102,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f103,plain,
! [W0,W1] :
( ! [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) )
| ~ aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1)
| W0 = W1
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f105,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f106,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f107,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f108,plain,
! [W0,W1,W2] :
( ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ sdtlseqdt0(W1,W2)
| W1 = W2
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f110,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f112,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f128,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(f129,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)],[f128]) ).
fof(f130,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)],[f129]) ).
fof(f131,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,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)],[f130]) ).
fof(f138,plain,
aNaturalNumber0(xl),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f139,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f140,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f141,plain,
doDivides0(xl,xm),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f142,plain,
doDivides0(xl,sdtpldt0(xm,xn)),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f143,plain,
xl != sz00,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f144,plain,
xp = sdtsldt0(xm,xl),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f145,plain,
xq = sdtsldt0(sdtpldt0(xm,xn),xl),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f146,plain,
~ sdtlseqdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f147,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f87]) ).
fof(f154,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f131]) ).
fof(f155,plain,
! [X0,X1] :
( X1 = sdtasdt0(X0,sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f132]) ).
fof(f157,plain,
( sdtlseqdt0(xq,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f102,f146]) ).
fof(f158,definition,
( sQ0_spl
<=> aNaturalNumber0(xq) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f161,definition,
( sQ1_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f164,definition,
( sQ2_spl
<=> sdtlseqdt0(xq,xp) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f165,plain,
( ~ sQ2_spl
| sdtlseqdt0(xq,xp) ),
inference(component_clause,[status(thm)],[f164]) ).
fof(f167,plain,
( sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f157,f158,f161,f164]) ).
fof(f175,definition,
( sQ4_spl
<=> xp = xq ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ4_spl
| xp = xq ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f177,plain,
( sQ4_spl
| xp != xq ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f232,plain,
! [X0,X1,X2] :
( sdtpldt0(X1,X2) = sdtpldt0(X0,X2)
| ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f107,f97]) ).
fof(f233,plain,
! [X0,X1,X2] :
( ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f232,f106]) ).
fof(f263,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f147,f48]) ).
fof(f1280,plain,
! [X0,X1,X2] :
( ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f233,f48]) ).
fof(f2178,plain,
( aNaturalNumber0(xq)
| ~ doDivides0(xl,sdtpldt0(xm,xn))
| xl = sz00
| ~ aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f145,f154]) ).
fof(f2179,plain,
( aNaturalNumber0(xp)
| ~ doDivides0(xl,xm)
| xl = sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f144,f154]) ).
fof(f2180,definition,
( sQ104_spl
<=> aNaturalNumber0(xl) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f2182,plain,
( sQ104_spl
| ~ aNaturalNumber0(xl) ),
inference(component_clause,[status(thm)],[f2180]) ).
fof(f2183,definition,
( sQ105_spl
<=> aNaturalNumber0(sdtpldt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2185,plain,
( sQ105_spl
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f2183]) ).
fof(f2186,definition,
( sQ106_spl
<=> xl = sz00 ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2187,plain,
( ~ sQ106_spl
| xl = sz00 ),
inference(component_clause,[status(thm)],[f2186]) ).
fof(f2189,definition,
( sQ107_spl
<=> doDivides0(xl,sdtpldt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2191,plain,
( sQ107_spl
| ~ doDivides0(xl,sdtpldt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f2189]) ).
fof(f2192,plain,
( sQ0_spl
| ~ sQ107_spl
| sQ106_spl
| ~ sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f2178,f2180,f2183,f2186,f2189,f158]) ).
fof(f2193,definition,
( sQ108_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f2195,plain,
( sQ108_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f2193]) ).
fof(f2196,definition,
( sQ109_spl
<=> doDivides0(xl,xm) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f2198,plain,
( sQ109_spl
| ~ doDivides0(xl,xm) ),
inference(component_clause,[status(thm)],[f2196]) ).
fof(f2199,plain,
( sQ1_spl
| ~ sQ109_spl
| sQ106_spl
| ~ sQ108_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f2179,f2180,f2193,f2186,f2196,f161]) ).
fof(f2200,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2187,f143]) ).
fof(f2201,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f2200]) ).
fof(f2202,plain,
( sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2182,f138]) ).
fof(f2203,plain,
sQ104_spl,
inference(contradiction_clause,[status(thm)],[f2202]) ).
fof(f2204,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2198,f141]) ).
fof(f2205,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f2204]) ).
fof(f2228,plain,
( sQ105_spl
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f2185,f48]) ).
fof(f2229,definition,
( sQ110_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2231,plain,
( sQ110_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f2229]) ).
fof(f2232,plain,
( sQ105_spl
| ~ sQ110_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f2228,f2193,f2229,f2183]) ).
fof(f2233,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2195,f139]) ).
fof(f2234,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f2233]) ).
fof(f2235,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2191,f142]) ).
fof(f2236,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f2235]) ).
fof(f2237,plain,
( sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2231,f140]) ).
fof(f2238,plain,
sQ110_spl,
inference(contradiction_clause,[status(thm)],[f2237]) ).
fof(f2244,plain,
( ~ sQ4_spl
| ~ sdtlseqdt0(xq,xq) ),
inference(backward_demodulation,[status(thm)],[f176,f146]) ).
fof(f2272,plain,
( ~ sQ2_spl
| ~ sQ4_spl
| sdtlseqdt0(xq,xq) ),
inference(forward_demodulation,[status(thm)],[f176,f165]) ).
fof(f2303,plain,
( ~ sQ4_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2244,f2272]) ).
fof(f2304,plain,
( ~ sQ4_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f2303]) ).
fof(f2507,definition,
( sQ133_spl
<=> xm = sdtasdt0(xl,xp) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f2508,plain,
( ~ sQ133_spl
| xm = sdtasdt0(xl,xp) ),
inference(component_clause,[status(thm)],[f2507]) ).
fof(f2511,definition,
( sQ134_spl
<=> sdtpldt0(xm,xn) = sdtasdt0(xl,xq) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2512,plain,
( ~ sQ134_spl
| sdtpldt0(xm,xn) = sdtasdt0(xl,xq) ),
inference(component_clause,[status(thm)],[f2511]) ).
fof(f3047,definition,
( sQ194_spl
<=> sdtlseqdt0(xm,sdtpldt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f3048,plain,
( ~ sQ194_spl
| sdtlseqdt0(xm,sdtpldt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f3047]) ).
fof(f3049,plain,
( sQ194_spl
| ~ sdtlseqdt0(xm,sdtpldt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f3047]) ).
fof(f3069,definition,
( sQ200_spl
<=> sdtpldt0(xm,xn) = xm ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f3070,plain,
( ~ sQ200_spl
| sdtpldt0(xm,xn) = xm ),
inference(component_clause,[status(thm)],[f3069]) ).
fof(f3430,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,X2) = sdtasdt0(X0,X1)
| ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X0,X1))
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f110,f97]) ).
fof(f3435,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,X2) = sdtasdt0(X0,X1)
| ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X0,X1))
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3430,f50]) ).
fof(f3582,plain,
( ~ sQ200_spl
| xq = sdtsldt0(xm,xl) ),
inference(forward_demodulation,[status(thm)],[f3070,f145]) ).
fof(f4207,plain,
( ~ sQ200_spl
| xp = xq ),
inference(forward_demodulation,[status(thm)],[f3582,f144]) ).
fof(f4208,plain,
( ~ sQ200_spl
| sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4207,f177]) ).
fof(f4209,plain,
( ~ sQ200_spl
| sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f4208]) ).
fof(f4615,plain,
( xm = sdtasdt0(xl,xp)
| ~ doDivides0(xl,xm)
| xl = sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f144,f155]) ).
fof(f4616,plain,
( sQ133_spl
| ~ sQ109_spl
| sQ106_spl
| ~ sQ108_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f4615,f2180,f2193,f2186,f2196,f2507]) ).
fof(f4617,plain,
( sdtpldt0(xm,xn) = sdtasdt0(xl,xq)
| ~ doDivides0(xl,sdtpldt0(xm,xn))
| xl = sz00
| ~ aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f145,f155]) ).
fof(f4618,plain,
( sQ134_spl
| ~ sQ107_spl
| sQ106_spl
| ~ sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f4617,f2180,f2183,f2186,f2189,f2511]) ).
fof(f6363,plain,
! [X0,X1,X2] :
( ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1280,f48]) ).
fof(f6364,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X1)
| X1 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X0,X0)
| X0 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f6363,f105]) ).
fof(f6380,definition,
! [X0] :
( sQ495_spl
<=> ( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X0)
| X0 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition]) ).
fof(f6383,plain,
sQ495_spl,
inference(split_clause,[status(thm)],[f6364,f6380]) ).
fof(f6387,definition,
! [X2] :
( sQ497_spl
<=> ( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition]) ).
fof(f6388,plain,
! [X0] :
( ~ sQ497_spl
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f6387]) ).
fof(f6401,plain,
! [X0] :
( ~ sQ497_spl
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f6388]) ).
fof(f6447,plain,
( ~ sQ497_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f140,f6401]) ).
fof(f6456,plain,
~ sQ497_spl,
inference(contradiction_clause,[status(thm)],[f6447]) ).
fof(f7491,plain,
( ~ sQ194_spl
| sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(resolution,[status(thm)],[f3048,f97]) ).
fof(f7497,definition,
( sQ584_spl
<=> sdtlseqdt0(sdtpldt0(xm,xn),xm) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f7499,plain,
( sQ584_spl
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm) ),
inference(component_clause,[status(thm)],[f7497]) ).
fof(f7500,plain,
( ~ sQ194_spl
| sQ200_spl
| ~ sQ584_spl
| ~ sQ108_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f7491,f2183,f2193,f7497,f3069,f3047]) ).
fof(f8165,plain,
( sQ194_spl
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f3049,f263]) ).
fof(f8167,plain,
( sQ194_spl
| ~ sQ110_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f8165,f2193,f2229,f3047]) ).
fof(f8307,definition,
! [X0] :
( sQ614_spl
<=> ( sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f8308,plain,
! [X0] :
( ~ sQ614_spl
| sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f8307]) ).
fof(f8602,plain,
( sQ584_spl
| ~ sQ134_spl
| ~ sdtlseqdt0(sdtasdt0(xl,xq),xm) ),
inference(backward_demodulation,[status(thm)],[f2512,f7499]) ).
fof(f8797,plain,
! [X0] :
( ~ sQ133_spl
| sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| xl = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f2508,f110]) ).
fof(f8803,plain,
( ~ sQ133_spl
| sQ106_spl
| ~ sQ1_spl
| sQ614_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f8797,f2180,f8307,f161,f2186,f2507]) ).
fof(f10949,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,X2) = sdtasdt0(X0,X1)
| ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3435,f50]) ).
fof(f11229,plain,
! [X0,X1,X2] :
( ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f10949,f75]) ).
fof(f18763,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X0)
| X0 = X0
| X1 = sz00
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X1,X1)
| X1 = X1
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f11229,f112]) ).
fof(f18773,definition,
! [X0] :
( sQ1330_spl
<=> ( ~ sdtlseqdt0(X0,X0)
| X0 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1330_spl])],[split_symbol_definition]) ).
fof(f18776,plain,
sQ1330_spl,
inference(split_clause,[status(thm)],[f18763,f18773]) ).
fof(f36134,plain,
( sQ584_spl
| ~ sQ134_spl
| ~ sQ614_spl
| ~ sdtlseqdt0(xq,xp)
| xq = xp
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f8308,f8602]) ).
fof(f36142,plain,
( sQ584_spl
| ~ sQ134_spl
| ~ sQ614_spl
| ~ sQ2_spl
| sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f36134,f158,f175,f164,f8307,f2511,f7497]) ).
fof(f36168,plain,
$false,
inference(sat_refutation,[status(thm)],[f167,f2192,f2199,f2201,f2203,f2205,f2232,f2234,f2236,f2238,f2304,f4209,f4616,f4618,f6383,f6456,f7500,f8167,f8803,f18776,f36142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM471+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n016.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.45 % CPULimit : 300
% 0.16/0.45 % WCLimit : 300
% 0.16/0.45 % DateTime : Mon Sep 21 02:37:22 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 260.42/33.49 % Refutation found
% 260.42/33.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 260.42/33.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 112.00/33.57 % Elapsed time: 33.104429 seconds
% 112.00/33.57 % CPU time: 262.278326 seconds
% 112.00/33.57 % Total memory used: 618.299 MB
% 112.00/33.57 % Net memory used: 564.908 MB
%------------------------------------------------------------------------------