%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM465+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:37 PM UTC 2026
% Result : Theorem 4.11s 1.45s
% Output : CNFRefutation 4.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 30
% Syntax : Number of formulae : 127 ( 11 unt; 19 def)
% Number of atoms : 400 ( 95 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 474 ( 201 ~; 197 |; 42 &)
% ( 21 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 18 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 88 ( 81 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
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(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
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(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
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(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
( xm != sz00
=> ( sdtlseqdt0(sz10,xm)
& ? [W0] :
( sdtpldt0(sz10,W0) = xm
& aNaturalNumber0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,conjecture,
( xm != sz00
=> ( sdtlseqdt0(xn,sdtasdt0(xn,xm))
| ? [W0] :
( sdtpldt0(xn,W0) = sdtasdt0(xn,xm)
& aNaturalNumber0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ ( xm != sz00
=> ( sdtlseqdt0(xn,sdtasdt0(xn,xm))
| ? [W0] :
( sdtpldt0(xn,W0) = sdtasdt0(xn,xm)
& aNaturalNumber0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f34,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f35,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f37,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f38,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f40,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f45,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f47,plain,
! [X0] :
( X0 = sdtpldt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f52,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f53,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f72,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(f73,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)],[f72]) ).
fof(f74,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))],[f73]) ).
fof(f77,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,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(f79,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)],[f78]) ).
fof(f80,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)],[f79]) ).
fof(f82,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) = X1
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f85,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f98,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(f100,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)],[f98]) ).
fof(f107,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f108,plain,
( ( sdtlseqdt0(sz10,xm)
& ? [W0] :
( sdtpldt0(sz10,W0) = xm
& aNaturalNumber0(W0) ) )
| xm = sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f109,plain,
( ( sdtlseqdt0(sz10,xm)
& sdtpldt0(sz10,sK1_skl) = xm
& aNaturalNumber0(sK1_skl) )
| xm = sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W0,sK1_skl)],[f108]) ).
fof(f110,plain,
( aNaturalNumber0(sK1_skl)
| xm = sz00 ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( sdtpldt0(sz10,sK1_skl) = xm
| xm = sz00 ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f113,plain,
( ~ sdtlseqdt0(xn,sdtasdt0(xn,xm))
& ! [W0] :
( sdtpldt0(xn,W0) != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(W0) )
& xm != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f114,plain,
xm != sz00,
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0] :
( sdtpldt0(xn,X0) != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f116,plain,
~ sdtlseqdt0(xn,sdtasdt0(xn,xm)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f117,definition,
( sQ0_spl
<=> xm = sz00 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f118,plain,
( ~ sQ0_spl
| xm = sz00 ),
inference(component_clause,[status(thm)],[f117]) ).
fof(f120,definition,
( sQ1_spl
<=> aNaturalNumber0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f123,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f110,f117,f120]) ).
fof(f124,definition,
( sQ2_spl
<=> sdtpldt0(sz10,sK1_skl) = xm ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f125,plain,
( ~ sQ2_spl
| sdtpldt0(sz10,sK1_skl) = xm ),
inference(component_clause,[status(thm)],[f124]) ).
fof(f127,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f111,f117,f124]) ).
fof(f128,definition,
( sQ3_spl
<=> sdtlseqdt0(sz10,xm) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f129,plain,
( ~ sQ3_spl
| sdtlseqdt0(sz10,xm) ),
inference(component_clause,[status(thm)],[f128]) ).
fof(f132,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f77]) ).
fof(f134,plain,
! [X0,X1] :
( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f82]) ).
fof(f135,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| X1 = sdtmndt0(sdtpldt0(X0,X1),X0)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f83]) ).
fof(f138,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f118,f114]) ).
fof(f139,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f138]) ).
fof(f144,definition,
( sQ5_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f146,plain,
( sQ5_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f144]) ).
fof(f153,definition,
( sQ7_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f155,plain,
( sQ7_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f161,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f155,f34]) ).
fof(f162,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f161]) ).
fof(f166,plain,
( ~ sQ2_spl
| aNaturalNumber0(xm)
| ~ aNaturalNumber0(sK1_skl)
| ~ aNaturalNumber0(sz10) ),
inference(paramodulation,[status(thm)],[f125,f38]) ).
fof(f167,definition,
( sQ9_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( sQ9_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f167]) ).
fof(f182,definition,
( sQ13_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( ~ sQ2_spl
| sQ13_spl
| ~ sQ1_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f166,f167,f120,f182,f124]) ).
fof(f186,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f169,f35]) ).
fof(f187,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f186]) ).
fof(f273,definition,
( sQ24_spl
<=> xm = sz10 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( ~ sQ24_spl
| xm = sz10 ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f287,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f146,f107]) ).
fof(f288,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f287]) ).
fof(f341,definition,
( sQ34_spl
<=> xn = sdtasdt0(xn,xm) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( ~ sQ34_spl
| xn = sdtasdt0(xn,xm) ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f343,plain,
( sQ34_spl
| xn != sdtasdt0(xn,xm) ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f345,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f132,f38]) ).
fof(f361,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| X1 = sdtmndt0(sdtpldt0(X0,X1),X0)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f38]) ).
fof(f366,definition,
( sQ37_spl
<=> sK1_skl = sdtmndt0(xm,sz10) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( ~ sQ37_spl
| sK1_skl = sdtmndt0(xm,sz10) ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f394,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| X1 = sdtmndt0(sdtpldt0(X0,X1),X0)
| ~ aNaturalNumber0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f361,f345]) ).
fof(f397,plain,
( ~ sQ2_spl
| ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sz10,xm)
| ~ aNaturalNumber0(sz10) ),
inference(paramodulation,[status(thm)],[f125,f345]) ).
fof(f402,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ3_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f397,f167,f128,f120,f124]) ).
fof(f422,plain,
( ~ sQ37_spl
| ~ sQ24_spl
| sK1_skl = sdtmndt0(sz10,sz10) ),
inference(backward_demodulation,[status(thm)],[f274,f367]) ).
fof(f430,plain,
( ~ sQ3_spl
| ~ sQ24_spl
| sdtlseqdt0(sz10,sz10) ),
inference(backward_demodulation,[status(thm)],[f274,f129]) ).
fof(f439,definition,
( sQ43_spl
<=> sdtlseqdt0(sz10,sz10) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( sQ43_spl
| ~ sdtlseqdt0(sz10,sz10) ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f446,plain,
( sQ43_spl
| ~ sQ3_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f441,f430]) ).
fof(f447,plain,
( sQ43_spl
| ~ sQ3_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f446]) ).
fof(f466,plain,
( ~ sQ37_spl
| ~ sQ24_spl
| sdtpldt0(sz10,sK1_skl) = sz10
| ~ sdtlseqdt0(sz10,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz10) ),
inference(paramodulation,[status(thm)],[f422,f134]) ).
fof(f468,definition,
( sQ47_spl
<=> sdtpldt0(sz10,sK1_skl) = sz10 ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ47_spl
| sdtpldt0(sz10,sK1_skl) = sz10 ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( ~ sQ37_spl
| ~ sQ24_spl
| sQ47_spl
| ~ sQ43_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f466,f167,f439,f468,f273,f366]) ).
fof(f529,definition,
( sQ59_spl
<=> xn = sdtasdt0(xn,sz10) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( ~ sQ59_spl
| xn = sdtasdt0(xn,sz10) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f531,plain,
( sQ59_spl
| xn != sdtasdt0(xn,sz10) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f574,definition,
( sQ66_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f575,plain,
( ~ sQ66_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f720,plain,
! [X0] :
( ~ sQ66_spl
| sdtpldt0(xn,X0) != sdtasdt0(sz00,xm)
| ~ aNaturalNumber0(X0) ),
inference(backward_demodulation,[status(thm)],[f575,f115]) ).
fof(f726,plain,
! [X0] :
( ~ sQ66_spl
| sdtpldt0(sz00,X0) != sdtasdt0(sz00,xm)
| ~ aNaturalNumber0(X0) ),
inference(forward_demodulation,[status(thm)],[f575,f720]) ).
fof(f730,definition,
( sQ80_spl
<=> aNaturalNumber0(sdtasdt0(sz00,xm)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( sQ80_spl
| ~ aNaturalNumber0(sdtasdt0(sz00,xm)) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f744,plain,
( ~ sQ47_spl
| ~ sQ2_spl
| xm = sz10 ),
inference(forward_demodulation,[status(thm)],[f125,f469]) ).
fof(f902,plain,
( sQ80_spl
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz00) ),
inference(resolution,[status(thm)],[f732,f40]) ).
fof(f903,plain,
( sQ80_spl
| ~ sQ13_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f902,f153,f182,f730]) ).
fof(f904,plain,
( ~ sQ34_spl
| ~ sdtlseqdt0(xn,xn) ),
inference(backward_demodulation,[status(thm)],[f342,f116]) ).
fof(f1078,plain,
( ~ sQ2_spl
| ~ aNaturalNumber0(sK1_skl)
| sK1_skl = sdtmndt0(xm,sz10)
| ~ aNaturalNumber0(sz10) ),
inference(paramodulation,[status(thm)],[f125,f394]) ).
fof(f1093,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1078,f167,f366,f120,f124]) ).
fof(f1210,plain,
( ~ sQ34_spl
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f904,f85]) ).
fof(f1215,plain,
( ~ sQ34_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1210,f144,f341]) ).
fof(f1218,plain,
( ~ sQ66_spl
| ~ aNaturalNumber0(sdtasdt0(sz00,xm))
| ~ aNaturalNumber0(sdtasdt0(sz00,xm)) ),
inference(resolution,[status(thm)],[f726,f47]) ).
fof(f1230,plain,
( ~ sQ66_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f1218,f730,f574]) ).
fof(f1403,plain,
! [X0] :
( ~ sQ59_spl
| sdtlseqdt0(xn,sdtasdt0(xn,X0))
| ~ sdtlseqdt0(sz10,X0)
| sz10 = X0
| xn = sz00
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f530,f100]) ).
fof(f1428,definition,
! [X0] :
( sQ153_spl
<=> ( sdtlseqdt0(xn,sdtasdt0(xn,X0))
| ~ sdtlseqdt0(sz10,X0)
| sz10 = X0
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ153_spl
| sdtlseqdt0(xn,sdtasdt0(xn,X0))
| ~ sdtlseqdt0(sz10,X0)
| sz10 = X0
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,plain,
( ~ sQ59_spl
| sQ66_spl
| sQ153_spl
| ~ sQ9_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1403,f144,f167,f1428,f574,f529]) ).
fof(f3113,plain,
( ~ sQ153_spl
| ~ sdtlseqdt0(sz10,xm)
| sz10 = xm
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f1429,f116]) ).
fof(f3121,plain,
( ~ sQ153_spl
| ~ sQ3_spl
| sQ24_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f3113,f182,f273,f128,f1428]) ).
fof(f3183,plain,
( sQ59_spl
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f531,f53]) ).
fof(f3184,plain,
( sQ59_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f3183,f144,f529]) ).
fof(f3198,plain,
( sQ34_spl
| ~ sQ47_spl
| ~ sQ2_spl
| xn != sdtasdt0(xn,sz10) ),
inference(backward_demodulation,[status(thm)],[f744,f343]) ).
fof(f3219,plain,
( sQ34_spl
| ~ sQ47_spl
| ~ sQ2_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f3198,f529,f124,f468,f341]) ).
fof(f3220,plain,
$false,
inference(sat_refutation,[status(thm)],[f123,f127,f139,f162,f185,f187,f288,f402,f447,f471,f903,f1093,f1215,f1230,f1431,f3121,f3184,f3219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM465+2 : 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.48 % Computer : n019.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 02:32:36 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 4.11/1.45 % Refutation found
% 4.11/1.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.11/1.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.11/1.49 % Elapsed time: 0.993644 seconds
% 4.11/1.49 % CPU time: 7.369374 seconds
% 4.11/1.49 % Total memory used: 134.473 MB
% 4.11/1.49 % Net memory used: 129.123 MB
%------------------------------------------------------------------------------