%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM477+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 : n026.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:40 PM UTC 2026
% Result : Theorem 16.91s 2.57s
% Output : CNFRefutation 16.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 35
% Syntax : Number of formulae : 155 ( 24 unt; 22 def)
% Number of atoms : 455 ( 103 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 504 ( 204 ~; 221 |; 41 &)
% ( 24 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 21 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 96 ( 93 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
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(f16,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtpldt0(W0,W1) = sz00
=> ( W1 = sz00
& W0 = sz00 ) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> sdtlseqdt0(W0,W0) ),
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(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(f26,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
( xn != sz00
& doDivides0(xm,xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,conjecture,
sdtlseqdt0(xm,xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
~ sdtlseqdt0(xm,xn),
inference(negated_conjecture,[status(cth)],[f37]) ).
fof(f43,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f45,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f46,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f56,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f57,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f60,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f61,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f64,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f75,plain,
! [W0,W1] :
( ( W1 = sz00
& W0 = sz00 )
| sdtpldt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f76,plain,
! [X0,X1] :
( X0 = sz00
| sdtpldt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f86,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(f87,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)],[f86]) ).
fof(f88,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)],[f87]) ).
fof(f89,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) = X1
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f92,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f93,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f98,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f100,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f106,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(f108,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)],[f106]) ).
fof(f111,plain,
! [W0] :
( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f113,plain,
! [X0] :
( sdtlseqdt0(sz10,X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f120,plain,
! [W0,W1] :
( ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f121,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f120]) ).
fof(f122,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ( W1 = sdtasdt0(W0,sK1_skl(W1,W0))
& aNaturalNumber0(sK1_skl(W1,W0)) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( aNaturalNumber0(sK1_skl(X1,X0))
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [X0,X1] :
( X1 = sdtasdt0(X0,sK1_skl(X1,X0))
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f138,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f139,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f140,plain,
doDivides0(xm,xn),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f141,plain,
xn != sz00,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f142,plain,
~ sdtlseqdt0(xm,xn),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f145,plain,
! [X0,X1] :
( aNaturalNumber0(sdtmndt0(X1,X0))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f89]) ).
fof(f146,plain,
! [X0,X1] :
( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f90]) ).
fof(f159,plain,
sdtlseqdt0(xn,xn),
inference(resolution,[status(thm)],[f139,f93]) ).
fof(f161,plain,
! [X0] :
( sdtlseqdt0(X0,xn)
| sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f100,f139]) ).
fof(f171,plain,
! [X0] :
( aNaturalNumber0(sdtpldt0(xn,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f46,f139]) ).
fof(f172,plain,
! [X0] :
( aNaturalNumber0(sdtpldt0(xm,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f46,f138]) ).
fof(f202,definition,
( sQ0_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f204,plain,
( sQ0_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f220,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f204,f138]) ).
fof(f221,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f220]) ).
fof(f231,definition,
( sQ6_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( sQ6_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f253,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f233,f139]) ).
fof(f254,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f253]) ).
fof(f268,plain,
( sdtlseqdt0(xm,xn)
| sdtlseqdt0(xn,xm) ),
inference(resolution,[status(thm)],[f161,f138]) ).
fof(f284,definition,
( sQ16_spl
<=> sdtlseqdt0(xn,xm) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( ~ sQ16_spl
| sdtlseqdt0(xn,xm) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,definition,
( sQ17_spl
<=> sdtlseqdt0(xm,xn) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ17_spl
| sdtlseqdt0(xm,xn) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f289,plain,
( sQ17_spl
| ~ sdtlseqdt0(xm,xn) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f268,f284,f287]) ).
fof(f315,definition,
( sQ22_spl
<=> xn = xm ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f316,plain,
( ~ sQ22_spl
| xn = xm ),
inference(component_clause,[status(thm)],[f315]) ).
fof(f317,plain,
( sQ22_spl
| xn != xm ),
inference(component_clause,[status(thm)],[f315]) ).
fof(f331,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f142]) ).
fof(f332,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f331]) ).
fof(f353,plain,
( sQ17_spl
| ~ sQ22_spl
| ~ sdtlseqdt0(xn,xn) ),
inference(forward_demodulation,[status(thm)],[f316,f289]) ).
fof(f354,plain,
( sQ17_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f159]) ).
fof(f355,plain,
( sQ17_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f354]) ).
fof(f374,plain,
! [X0] :
( sdtasdt0(X0,xm) = sdtasdt0(xm,X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f57,f138]) ).
fof(f391,plain,
sdtasdt0(xm,sz10) = xm,
inference(resolution,[status(thm)],[f61,f138]) ).
fof(f396,plain,
xm = sdtasdt0(sz10,xm),
inference(resolution,[status(thm)],[f62,f138]) ).
fof(f400,plain,
sdtasdt0(xm,sz00) = sz00,
inference(resolution,[status(thm)],[f64,f138]) ).
fof(f486,definition,
( sQ35_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( sQ35_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f505,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f43]) ).
fof(f506,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f505]) ).
fof(f733,plain,
aNaturalNumber0(sdtpldt0(xm,xm)),
inference(resolution,[status(thm)],[f172,f138]) ).
fof(f741,plain,
aNaturalNumber0(sdtpldt0(xn,xn)),
inference(resolution,[status(thm)],[f171,f139]) ).
fof(f742,plain,
aNaturalNumber0(sdtpldt0(xn,xm)),
inference(resolution,[status(thm)],[f171,f138]) ).
fof(f870,definition,
( sQ52_spl
<=> xm = sz00 ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f996,plain,
( xn = sdtasdt0(xm,sK1_skl(xn,xm))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f124,f140]) ).
fof(f997,definition,
( sQ54_spl
<=> xn = sdtasdt0(xm,sK1_skl(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f998,plain,
( ~ sQ54_spl
| xn = sdtasdt0(xm,sK1_skl(xn,xm)) ),
inference(component_clause,[status(thm)],[f997]) ).
fof(f1000,plain,
( sQ54_spl
| ~ sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f996,f202,f231,f997]) ).
fof(f1001,plain,
( aNaturalNumber0(sK1_skl(xn,xm))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f123,f140]) ).
fof(f1002,definition,
( sQ55_spl
<=> aNaturalNumber0(sK1_skl(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( ~ sQ55_spl
| aNaturalNumber0(sK1_skl(xn,xm)) ),
inference(component_clause,[status(thm)],[f1002]) ).
fof(f1005,plain,
( sQ55_spl
| ~ sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1001,f202,f231,f1002]) ).
fof(f1134,plain,
( ~ sQ16_spl
| sdtpldt0(xn,sdtmndt0(xm,xn)) = xm
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f146,f285]) ).
fof(f1144,definition,
( sQ62_spl
<=> sdtpldt0(xn,sdtmndt0(xm,xn)) = xm ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1145,plain,
( ~ sQ62_spl
| sdtpldt0(xn,sdtmndt0(xm,xn)) = xm ),
inference(component_clause,[status(thm)],[f1144]) ).
fof(f1147,plain,
( ~ sQ16_spl
| sQ62_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1134,f231,f202,f1144,f284]) ).
fof(f1154,plain,
( ~ sQ16_spl
| aNaturalNumber0(sdtmndt0(xm,xn))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f145,f285]) ).
fof(f1164,definition,
( sQ66_spl
<=> aNaturalNumber0(sdtmndt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1167,plain,
( ~ sQ16_spl
| sQ66_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1154,f231,f202,f1164,f284]) ).
fof(f1407,definition,
( sQ95_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1408,plain,
( ~ sQ95_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f1407]) ).
fof(f1428,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1408,f141]) ).
fof(f1429,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1428]) ).
fof(f1605,plain,
( ~ sQ62_spl
| xn = sz00
| xm != sz00
| ~ aNaturalNumber0(sdtmndt0(xm,xn))
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f1145,f76]) ).
fof(f1620,plain,
( ~ sQ62_spl
| sQ95_spl
| ~ sQ52_spl
| ~ sQ66_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1605,f231,f1164,f870,f1407,f1144]) ).
fof(f1685,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| xm = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f108,f138]) ).
fof(f1698,definition,
! [X0,X1] :
( sQ126_spl
<=> ( sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
! [X0,X1] :
( ~ sQ126_spl
| sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f1698]) ).
fof(f1701,plain,
( sQ52_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1685,f1698,f870]) ).
fof(f1966,definition,
( sQ148_spl
<=> aNaturalNumber0(sdtpldt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( sQ148_spl
| ~ aNaturalNumber0(sdtpldt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f1966]) ).
fof(f2001,plain,
( sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1968,f741]) ).
fof(f2002,plain,
sQ148_spl,
inference(contradiction_clause,[status(thm)],[f2001]) ).
fof(f2359,definition,
( sQ186_spl
<=> aNaturalNumber0(sdtpldt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2361,plain,
( sQ186_spl
| ~ aNaturalNumber0(sdtpldt0(xm,xm)) ),
inference(component_clause,[status(thm)],[f2359]) ).
fof(f2389,plain,
( sQ186_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2361,f733]) ).
fof(f2390,plain,
sQ186_spl,
inference(contradiction_clause,[status(thm)],[f2389]) ).
fof(f3064,definition,
( sQ209_spl
<=> sK1_skl(xn,xm) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f3065,plain,
( ~ sQ209_spl
| sK1_skl(xn,xm) = sz00 ),
inference(component_clause,[status(thm)],[f3064]) ).
fof(f3078,plain,
( ~ sQ54_spl
| ~ sQ209_spl
| xn = sdtasdt0(xm,sz00) ),
inference(backward_demodulation,[status(thm)],[f3065,f998]) ).
fof(f3081,plain,
( ~ sQ54_spl
| ~ sQ209_spl
| xn = sz00 ),
inference(forward_demodulation,[status(thm)],[f400,f3078]) ).
fof(f3082,plain,
( ~ sQ54_spl
| ~ sQ209_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3081,f141]) ).
fof(f3083,plain,
( ~ sQ54_spl
| ~ sQ209_spl ),
inference(contradiction_clause,[status(thm)],[f3082]) ).
fof(f3477,definition,
( sQ253_spl
<=> aNaturalNumber0(sdtpldt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f3479,plain,
( sQ253_spl
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(component_clause,[status(thm)],[f3477]) ).
fof(f3512,plain,
( sQ253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3479,f742]) ).
fof(f3513,plain,
sQ253_spl,
inference(contradiction_clause,[status(thm)],[f3512]) ).
fof(f3986,plain,
( ~ sQ55_spl
| sdtlseqdt0(sz10,sK1_skl(xn,xm))
| sK1_skl(xn,xm) = sz10
| sK1_skl(xn,xm) = sz00 ),
inference(resolution,[status(thm)],[f1003,f113]) ).
fof(f4024,plain,
( ~ sQ55_spl
| sdtasdt0(sK1_skl(xn,xm),xm) = sdtasdt0(xm,sK1_skl(xn,xm)) ),
inference(resolution,[status(thm)],[f1003,f374]) ).
fof(f4077,definition,
( sQ283_spl
<=> sdtlseqdt0(sz10,sK1_skl(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f4078,plain,
( ~ sQ283_spl
| sdtlseqdt0(sz10,sK1_skl(xn,xm)) ),
inference(component_clause,[status(thm)],[f4077]) ).
fof(f4087,definition,
( sQ285_spl
<=> sK1_skl(xn,xm) = sz10 ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f4088,plain,
( ~ sQ285_spl
| sK1_skl(xn,xm) = sz10 ),
inference(component_clause,[status(thm)],[f4087]) ).
fof(f4090,plain,
( ~ sQ55_spl
| sQ283_spl
| sQ285_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f3986,f3064,f4087,f4077,f1002]) ).
fof(f4140,plain,
( ~ sQ55_spl
| ~ sQ54_spl
| sdtasdt0(sK1_skl(xn,xm),xm) = xn ),
inference(forward_demodulation,[status(thm)],[f998,f4024]) ).
fof(f4705,plain,
( ~ sQ126_spl
| ~ sQ283_spl
| sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK1_skl(xn,xm)))
| sz10 = sK1_skl(xn,xm)
| ~ aNaturalNumber0(sK1_skl(xn,xm))
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f4078,f1699]) ).
fof(f4727,definition,
( sQ317_spl
<=> sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK1_skl(xn,xm))) ),
introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition]) ).
fof(f4728,plain,
( ~ sQ317_spl
| sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK1_skl(xn,xm))) ),
inference(component_clause,[status(thm)],[f4727]) ).
fof(f4730,plain,
( ~ sQ126_spl
| ~ sQ283_spl
| sQ317_spl
| sQ285_spl
| ~ sQ55_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f4705,f486,f1002,f4087,f4727,f4077,f1698]) ).
fof(f4790,plain,
( ~ sQ55_spl
| ~ sQ54_spl
| ~ sQ285_spl
| sdtasdt0(sz10,xm) = xn ),
inference(backward_demodulation,[status(thm)],[f4088,f4140]) ).
fof(f4914,plain,
( ~ sQ55_spl
| ~ sQ54_spl
| ~ sQ285_spl
| xm = xn ),
inference(forward_demodulation,[status(thm)],[f396,f4790]) ).
fof(f4915,plain,
( ~ sQ55_spl
| ~ sQ54_spl
| ~ sQ285_spl
| sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4914,f317]) ).
fof(f4916,plain,
( ~ sQ55_spl
| ~ sQ54_spl
| ~ sQ285_spl
| sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f4915]) ).
fof(f4918,plain,
( ~ sQ317_spl
| sdtlseqdt0(xm,sdtasdt0(xm,sK1_skl(xn,xm))) ),
inference(forward_demodulation,[status(thm)],[f391,f4728]) ).
fof(f4923,plain,
( ~ sQ317_spl
| ~ sQ54_spl
| sdtlseqdt0(xm,xn) ),
inference(backward_demodulation,[status(thm)],[f998,f4918]) ).
fof(f4925,plain,
( ~ sQ317_spl
| ~ sQ54_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f4923,f287,f997,f4727]) ).
fof(f4926,plain,
$false,
inference(sat_refutation,[status(thm)],[f221,f254,f290,f332,f355,f506,f1000,f1005,f1147,f1167,f1429,f1620,f1701,f2002,f2390,f3083,f3513,f4090,f4730,f4916,f4925]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM477+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:36:22 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 16.91/2.57 % Refutation found
% 16.91/2.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.91/2.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.29/2.61 % Elapsed time: 2.233884 seconds
% 2.29/2.61 % CPU time: 17.364891 seconds
% 2.29/2.61 % Total memory used: 226.072 MB
% 2.29/2.61 % Net memory used: 210.192 MB
%------------------------------------------------------------------------------