%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM528+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 : n008.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:51 PM UTC 2026
% Result : Theorem 240.13s 30.84s
% Output : CNFRefutation 240.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 47
% Syntax : Number of formulae : 178 ( 28 unt; 29 def)
% Number of atoms : 546 ( 157 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 618 ( 250 ~; 268 |; 49 &)
% ( 31 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 28 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 88 ( 87 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('/export/starexec/sandbox2/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/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(f40,hypothesis,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
isPrime0(xp),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
( doDivides0(xp,xn)
& doDivides0(xp,sdtasdt0(xn,xn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
xq = sdtsldt0(xn,xp),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
( sdtlseqdt0(xn,xm)
=> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,conjecture,
( sdtlseqdt0(xm,xn)
& xm != xn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
~ ( sdtlseqdt0(xm,xn)
& xm != xn ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f54,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f58,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f67,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f71,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f73,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f75,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f83,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(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f89,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f90,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f105,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f106,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f109,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f111,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f125,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f126,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f137,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(f138,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)],[f137]) ).
fof(f139,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)],[f138]) ).
fof(f140,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,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)],[f139]) ).
fof(f153,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(f154,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)],[f153]) ).
fof(f155,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))],[f154]) ).
fof(f157,plain,
! [X0] :
( X0 != sz10
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f170,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f171,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f172,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f173,plain,
xn != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f175,plain,
xp != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f178,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f179,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f180,plain,
doDivides0(xp,sdtasdt0(xn,xn)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f181,plain,
doDivides0(xp,xn),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f182,plain,
xq = sdtsldt0(xn,xp),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f183,plain,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f184,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(xn,xm) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f185,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(xn,xm) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f186,plain,
( ~ sdtlseqdt0(xm,xn)
| xm = xn ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f187,plain,
( ~ sdtlseqdt0(xm,xn)
| xm = xn ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f188,definition,
( sQ0_spl
<=> sdtlseqdt0(xn,xm) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f191,definition,
( sQ1_spl
<=> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ1_spl
| sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f185,f188,f191]) ).
fof(f195,definition,
( sQ2_spl
<=> xm = xn ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ2_spl
| xm = xn ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,definition,
( sQ3_spl
<=> sdtlseqdt0(xm,xn) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f200,plain,
( sQ3_spl
| ~ sdtlseqdt0(xm,xn) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f187,f195,f198]) ).
fof(f209,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f140]) ).
fof(f210,plain,
! [X0,X1] :
( X1 = sdtasdt0(X0,sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f213,plain,
( ~ isPrime0(sz10)
| ~ aNaturalNumber0(sz10) ),
inference(destructive_equality_resolution,[status(thm)],[f157]) ).
fof(f229,definition,
( sQ4_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( sQ4_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f235,definition,
( sQ6_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( sQ6_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f235]) ).
fof(f239,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f237,f170]) ).
fof(f240,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f239]) ).
fof(f279,plain,
~ isPrime0(sz10),
inference(forward_subsumption_resolution,[status(thm)],[f213,f54]) ).
fof(f298,plain,
( sQ3_spl
| sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f200,f111]) ).
fof(f300,plain,
( sQ3_spl
| sQ0_spl
| ~ sQ4_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f298,f235,f229,f188,f198]) ).
fof(f324,definition,
( sQ15_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( sQ15_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f324]) ).
fof(f337,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f326,f54]) ).
fof(f338,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f337]) ).
fof(f348,definition,
( sQ19_spl
<=> aNaturalNumber0(sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( sQ19_spl
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f359,plain,
( sQ19_spl
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f350,f59]) ).
fof(f360,plain,
( sQ19_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f359,f235,f348]) ).
fof(f447,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f231,f171]) ).
fof(f448,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f447]) ).
fof(f597,plain,
( ~ sQ1_spl
| sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(resolution,[status(thm)],[f192,f106]) ).
fof(f601,definition,
( sQ54_spl
<=> aNaturalNumber0(sdtasdt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f609,definition,
( sQ56_spl
<=> sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f612,definition,
( sQ57_spl
<=> sdtasdt0(xm,xm) = sdtasdt0(xn,xn) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ57_spl
| sdtasdt0(xm,xm) = sdtasdt0(xn,xn) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( ~ sQ1_spl
| sQ57_spl
| ~ sQ56_spl
| ~ sQ19_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f597,f601,f348,f609,f612,f191]) ).
fof(f969,definition,
( sQ95_spl
<=> sdtasdt0(xn,xn) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1165,definition,
( sQ121_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1166,plain,
( ~ sQ121_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f1165]) ).
fof(f1260,plain,
( ~ sQ121_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f1166,f173]) ).
fof(f1261,plain,
( ~ sQ121_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1260]) ).
fof(f1262,plain,
~ sQ121_spl,
inference(contradiction_clause,[status(thm)],[f1261]) ).
fof(f1659,definition,
( sQ169_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1661,plain,
( sQ169_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f1659]) ).
fof(f1662,definition,
( sQ170_spl
<=> xp = sz00 ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( ~ sQ170_spl
| xp = sz00 ),
inference(component_clause,[status(thm)],[f1662]) ).
fof(f1668,definition,
( sQ172_spl
<=> aNaturalNumber0(xq) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1882,plain,
( ~ sQ170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1663,f175]) ).
fof(f1883,plain,
~ sQ170_spl,
inference(contradiction_clause,[status(thm)],[f1882]) ).
fof(f1884,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1661,f172]) ).
fof(f1885,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f1884]) ).
fof(f2008,definition,
( sQ208_spl
<=> xq = sz00 ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f2009,plain,
( ~ sQ208_spl
| xq = sz00 ),
inference(component_clause,[status(thm)],[f2008]) ).
fof(f2209,definition,
( sQ230_spl
<=> xp = sz10 ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2210,plain,
( ~ sQ230_spl
| xp = sz10 ),
inference(component_clause,[status(thm)],[f2209]) ).
fof(f2242,plain,
( ~ sQ230_spl
| isPrime0(sz10) ),
inference(backward_demodulation,[status(thm)],[f2210,f179]) ).
fof(f2244,plain,
( ~ sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2242,f279]) ).
fof(f2245,plain,
~ sQ230_spl,
inference(contradiction_clause,[status(thm)],[f2244]) ).
fof(f2955,plain,
( xn = sdtasdt0(xp,xq)
| ~ doDivides0(xp,xn)
| xp = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f182,f210]) ).
fof(f2956,plain,
( aNaturalNumber0(xq)
| ~ doDivides0(xp,xn)
| xp = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f182,f209]) ).
fof(f2957,definition,
( sQ292_spl
<=> doDivides0(xp,xn) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f2959,plain,
( sQ292_spl
| ~ doDivides0(xp,xn) ),
inference(component_clause,[status(thm)],[f2957]) ).
fof(f2960,definition,
( sQ293_spl
<=> xn = sdtasdt0(xp,xq) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f2961,plain,
( ~ sQ293_spl
| xn = sdtasdt0(xp,xq) ),
inference(component_clause,[status(thm)],[f2960]) ).
fof(f2963,plain,
( sQ293_spl
| ~ sQ292_spl
| sQ170_spl
| ~ sQ6_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f2955,f1659,f235,f1662,f2957,f2960]) ).
fof(f2964,plain,
( sQ172_spl
| ~ sQ292_spl
| sQ170_spl
| ~ sQ6_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f2956,f1659,f235,f1662,f2957,f1668]) ).
fof(f2965,plain,
( sQ292_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2959,f181]) ).
fof(f2966,plain,
sQ292_spl,
inference(contradiction_clause,[status(thm)],[f2965]) ).
fof(f2978,plain,
( sdtasdt0(sdtasdt0(xm,xm),xp) = sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(paramodulation,[status(thm)],[f178,f68]) ).
fof(f2984,plain,
( sdtasdt0(xm,xm) = sz00
| xp = sz00
| sdtasdt0(xn,xn) != sz00
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f178,f90]) ).
fof(f2994,definition,
( sQ295_spl
<=> isPrime0(xp) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f2996,plain,
( sQ295_spl
| ~ isPrime0(xp) ),
inference(component_clause,[status(thm)],[f2994]) ).
fof(f3002,definition,
( sQ297_spl
<=> sdtasdt0(xm,xm) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f3036,definition,
( sQ306_spl
<=> doDivides0(xp,sdtasdt0(xp,sdtasdt0(xm,xm))) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f3038,plain,
( sQ306_spl
| ~ doDivides0(xp,sdtasdt0(xp,sdtasdt0(xm,xm))) ),
inference(component_clause,[status(thm)],[f3036]) ).
fof(f3047,definition,
( sQ309_spl
<=> sdtasdt0(sdtasdt0(xm,xm),xp) = sdtasdt0(xn,xn) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f3048,plain,
( ~ sQ309_spl
| sdtasdt0(sdtasdt0(xm,xm),xp) = sdtasdt0(xn,xn) ),
inference(component_clause,[status(thm)],[f3047]) ).
fof(f3050,plain,
( sQ309_spl
| ~ sQ169_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f2978,f601,f1659,f3047]) ).
fof(f3065,plain,
( sQ297_spl
| sQ170_spl
| ~ sQ95_spl
| ~ sQ54_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f2984,f1659,f601,f969,f1662,f3002]) ).
fof(f3084,plain,
( sQ295_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2996,f179]) ).
fof(f3085,plain,
sQ295_spl,
inference(contradiction_clause,[status(thm)],[f3084]) ).
fof(f3088,plain,
( sQ306_spl
| ~ doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(forward_demodulation,[status(thm)],[f178,f3038]) ).
fof(f3102,plain,
( aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f183,f59]) ).
fof(f3106,plain,
( sdtasdt0(xq,xq) = sz00
| xp = sz00
| sdtasdt0(xm,xm) != sz00
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f183,f90]) ).
fof(f3121,definition,
( sQ319_spl
<=> aNaturalNumber0(sdtasdt0(xq,xq)) ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f3123,plain,
( sQ319_spl
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) ),
inference(component_clause,[status(thm)],[f3121]) ).
fof(f3124,definition,
( sQ320_spl
<=> sdtasdt0(xq,xq) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f3125,plain,
( ~ sQ320_spl
| sdtasdt0(xq,xq) = sz00 ),
inference(component_clause,[status(thm)],[f3124]) ).
fof(f3174,plain,
( sQ54_spl
| ~ sQ319_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f3102,f1659,f3121,f601]) ).
fof(f3187,plain,
( sQ320_spl
| sQ170_spl
| ~ sQ297_spl
| ~ sQ319_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f3106,f1659,f3121,f3002,f1662,f3124]) ).
fof(f3367,plain,
( ~ sQ293_spl
| ~ sQ208_spl
| xn = sdtasdt0(xp,sz00) ),
inference(forward_demodulation,[status(thm)],[f2009,f2961]) ).
fof(f3368,plain,
( ~ sQ293_spl
| ~ sQ208_spl
| xn = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f3367,f75]) ).
fof(f3391,plain,
( ~ sQ293_spl
| ~ sQ208_spl
| sQ121_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f3368,f1659,f1165,f2008,f2960]) ).
fof(f3628,plain,
( sQ319_spl
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f3123,f59]) ).
fof(f3629,plain,
( sQ319_spl
| ~ sQ172_spl ),
inference(split_clause,[status(thm)],[f3628,f1668,f3121]) ).
fof(f4380,plain,
( ~ sQ320_spl
| xq = sz00
| xq = sz00
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f3125,f90]) ).
fof(f4408,plain,
( ~ sQ320_spl
| sQ208_spl
| ~ sQ172_spl ),
inference(split_clause,[status(thm)],[f4380,f1668,f2008,f3124]) ).
fof(f9989,plain,
( ~ sQ2_spl
| sdtasdt0(xp,sdtasdt0(xn,xm)) = sdtasdt0(xn,xn) ),
inference(forward_demodulation,[status(thm)],[f196,f178]) ).
fof(f9990,plain,
( ~ sQ2_spl
| sdtasdt0(xp,sdtasdt0(xn,xn)) = sdtasdt0(xn,xn) ),
inference(forward_demodulation,[status(thm)],[f196,f9989]) ).
fof(f10024,plain,
! [X0] :
( ~ sQ2_spl
| X0 = xp
| sdtasdt0(X0,sdtasdt0(xn,xn)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| sdtasdt0(xn,xn) = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(paramodulation,[status(thm)],[f9990,f85]) ).
fof(f10142,definition,
! [X0] :
( sQ1111_spl
<=> ( X0 = xp
| sdtasdt0(X0,sdtasdt0(xn,xn)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1111_spl])],[split_symbol_definition]) ).
fof(f10143,plain,
! [X0] :
( ~ sQ1111_spl
| X0 = xp
| sdtasdt0(X0,sdtasdt0(xn,xn)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f10142]) ).
fof(f10145,plain,
( ~ sQ2_spl
| ~ sQ169_spl
| sQ1111_spl
| sQ95_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f10024,f348,f969,f10142,f1659,f195]) ).
fof(f20639,plain,
( ~ sQ309_spl
| sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f3048,f126]) ).
fof(f20682,plain,
( ~ sQ309_spl
| sQ56_spl
| sQ170_spl
| ~ sQ54_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f20639,f1659,f601,f1662,f609,f3047]) ).
fof(f20741,plain,
( sQ306_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3088,f180]) ).
fof(f20742,plain,
sQ306_spl,
inference(contradiction_clause,[status(thm)],[f20741]) ).
fof(f23907,plain,
( ~ sQ1111_spl
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| sz10 = xp
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f10143,f73]) ).
fof(f23908,plain,
( ~ sQ1111_spl
| ~ sQ19_spl
| sQ230_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f23907,f324,f2209,f348,f10142]) ).
fof(f25779,plain,
( ~ sQ57_spl
| sdtasdt0(xp,sdtasdt0(xn,xn)) = sdtasdt0(xn,xn) ),
inference(backward_demodulation,[status(thm)],[f613,f178]) ).
fof(f26034,plain,
! [X0] :
( ~ sQ57_spl
| X0 = xp
| sdtasdt0(X0,sdtasdt0(xn,xn)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| sdtasdt0(xn,xn) = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(paramodulation,[status(thm)],[f25779,f85]) ).
fof(f26065,plain,
( ~ sQ57_spl
| ~ sQ169_spl
| sQ1111_spl
| sQ95_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f26034,f348,f969,f10142,f1659,f612]) ).
fof(f26090,plain,
$false,
inference(sat_refutation,[status(thm)],[f194,f201,f240,f300,f338,f360,f448,f615,f1262,f1883,f1885,f2245,f2963,f2964,f2966,f3050,f3065,f3085,f3174,f3187,f3391,f3629,f4408,f10145,f20682,f20742,f23908,f26065]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM528+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n008.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 02:38:39 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 240.13/30.84 % Refutation found
% 240.13/30.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 240.13/30.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.21/30.91 % Elapsed time: 30.429246 seconds
% 7.21/30.91 % CPU time: 240.707744 seconds
% 7.21/30.91 % Total memory used: 498.962 MB
% 7.21/30.91 % Net memory used: 453.401 MB
%------------------------------------------------------------------------------