%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM463+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 3.65s 0.98s
% Output : CNFRefutation 3.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 18
% Syntax : Number of formulae : 82 ( 22 unt; 8 def)
% Number of atoms : 208 ( 72 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 215 ( 89 ~; 84 |; 25 &)
% ( 8 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 39 ( 37 !; 2 ?)
% 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(f8,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
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(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(f26,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,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(f29,negated_conjecture,
~ ( xm != sz00
=> ( sdtlseqdt0(xn,sdtasdt0(xn,xm))
| ? [W0] :
( sdtpldt0(xn,W0) = sdtasdt0(xn,xm)
& aNaturalNumber0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f33,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f34,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f44,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f45,plain,
! [X0] :
( sdtpldt0(X0,sz00) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f47,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f48,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f51,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f52,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f54,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f56,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f97,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(f101,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)],[f97]) ).
fof(f102,plain,
! [W0] :
( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f104,plain,
! [X0] :
( sdtlseqdt0(sz10,X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f106,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f107,plain,
( ~ sdtlseqdt0(xn,sdtasdt0(xn,xm))
& ! [W0] :
( sdtpldt0(xn,W0) != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(W0) )
& xm != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f108,plain,
xm != sz00,
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [X0] :
( sdtpldt0(xn,X0) != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f110,plain,
~ sdtlseqdt0(xn,sdtasdt0(xn,xm)),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f119,plain,
sdtpldt0(xn,sz00) != sdtasdt0(xn,xm),
inference(resolution,[status(thm)],[f33,f109]) ).
fof(f139,plain,
sdtpldt0(xn,sz00) = xn,
inference(resolution,[status(thm)],[f45,f106]) ).
fof(f143,plain,
xn != sdtasdt0(xn,xm),
inference(backward_demodulation,[status(thm)],[f139,f119]) ).
fof(f150,plain,
! [X0] :
( sdtasdt0(xm,X0) = sdtasdt0(X0,xm)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f48,f105]) ).
fof(f156,plain,
sdtasdt0(xn,sz10) = xn,
inference(resolution,[status(thm)],[f52,f106]) ).
fof(f160,plain,
xn = sdtasdt0(sz10,xn),
inference(resolution,[status(thm)],[f53,f106]) ).
fof(f174,plain,
sz00 = sdtasdt0(sz00,xm),
inference(resolution,[status(thm)],[f56,f105]) ).
fof(f196,definition,
( sQ0_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ0_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f210,definition,
( sQ4_spl
<=> xm = sz00 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( ~ sQ4_spl
| xm = sz00 ),
inference(component_clause,[status(thm)],[f210]) ).
fof(f224,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f211,f108]) ).
fof(f225,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f224]) ).
fof(f231,plain,
( ~ sQ0_spl
| xn != sdtasdt0(sz00,xm) ),
inference(backward_demodulation,[status(thm)],[f197,f143]) ).
fof(f259,plain,
( ~ sQ0_spl
| sz00 != sdtasdt0(sz00,xm) ),
inference(forward_demodulation,[status(thm)],[f197,f231]) ).
fof(f260,plain,
( ~ sQ0_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f174,f259]) ).
fof(f261,plain,
( ~ sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f260]) ).
fof(f262,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f261]) ).
fof(f365,definition,
( sQ22_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( sQ22_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f365]) ).
fof(f375,definition,
( sQ25_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ25_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f387,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f377,f34]) ).
fof(f388,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f387]) ).
fof(f419,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f367,f105]) ).
fof(f420,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f419]) ).
fof(f608,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X1,xn))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| xn = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f101,f106]) ).
fof(f612,definition,
! [X0,X1] :
( sQ68_spl
<=> ( sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X1,xn))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f613,plain,
! [X0,X1] :
( ~ sQ68_spl
| sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X1,xn))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( sQ0_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f608,f612,f196]) ).
fof(f638,plain,
( sdtlseqdt0(sz10,xm)
| xm = sz10
| xm = sz00 ),
inference(resolution,[status(thm)],[f104,f105]) ).
fof(f648,definition,
( sQ76_spl
<=> xm = sz10 ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ76_spl
| xm = sz10 ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,definition,
( sQ77_spl
<=> sdtlseqdt0(sz10,xm) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( ~ sQ77_spl
| sdtlseqdt0(sz10,xm) ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f654,plain,
( sQ77_spl
| sQ76_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f638,f210,f648,f651]) ).
fof(f667,plain,
( ~ sQ76_spl
| xn != sdtasdt0(xn,sz10) ),
inference(backward_demodulation,[status(thm)],[f649,f143]) ).
fof(f892,plain,
( ~ sQ76_spl
| xn != xn ),
inference(forward_demodulation,[status(thm)],[f156,f667]) ).
fof(f893,plain,
( ~ sQ76_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f892]) ).
fof(f894,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f893]) ).
fof(f2470,plain,
sdtasdt0(xm,xn) = sdtasdt0(xn,xm),
inference(resolution,[status(thm)],[f150,f106]) ).
fof(f2477,plain,
~ sdtlseqdt0(xn,sdtasdt0(xm,xn)),
inference(backward_demodulation,[status(thm)],[f2470,f110]) ).
fof(f2574,plain,
( ~ sQ77_spl
| ~ sQ68_spl
| sdtlseqdt0(sdtasdt0(sz10,xn),sdtasdt0(xm,xn))
| sz10 = xm
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f613,f652]) ).
fof(f2605,definition,
( sQ214_spl
<=> sdtlseqdt0(sdtasdt0(sz10,xn),sdtasdt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f2606,plain,
( ~ sQ214_spl
| sdtlseqdt0(sdtasdt0(sz10,xn),sdtasdt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f2605]) ).
fof(f2608,plain,
( ~ sQ77_spl
| ~ sQ68_spl
| sQ214_spl
| sQ76_spl
| ~ sQ22_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2574,f375,f365,f648,f2605,f612,f651]) ).
fof(f2614,plain,
( ~ sQ214_spl
| sdtlseqdt0(xn,sdtasdt0(xm,xn)) ),
inference(forward_demodulation,[status(thm)],[f160,f2606]) ).
fof(f2615,plain,
( ~ sQ214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2614,f2477]) ).
fof(f2616,plain,
~ sQ214_spl,
inference(contradiction_clause,[status(thm)],[f2615]) ).
fof(f2617,plain,
$false,
inference(sat_refutation,[status(thm)],[f225,f262,f388,f420,f615,f654,f894,f2608,f2616]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM463+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.40 % Computer : n019.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 21 02:32:05 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.41 % Drodi V4.1.1
% 3.65/0.98 % Refutation found
% 3.65/0.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.65/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.65/1.00 % Elapsed time: 0.580199 seconds
% 3.65/1.00 % CPU time: 4.317623 seconds
% 3.65/1.00 % Total memory used: 132.746 MB
% 3.65/1.00 % Net memory used: 127.101 MB
%------------------------------------------------------------------------------