%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM521+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:50 PM UTC 2026
% Result : Theorem 0.14s 0.41s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 19
% Syntax : Number of formulae : 71 ( 12 unt; 11 def)
% Number of atoms : 201 ( 44 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 226 ( 96 ~; 83 |; 34 &)
% ( 11 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 12 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 34 ( 25 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
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(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
~ ( sdtlseqdt0(xp,xn)
| ? [W0] :
( sdtpldt0(xp,W0) = xn
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
~ ( sdtlseqdt0(xp,xm)
| ? [W0] :
( sdtpldt0(xp,W0) = xm
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
~ ( ( sdtlseqdt0(xm,xp)
| ? [W0] :
( sdtpldt0(xm,W0) = xp
& aNaturalNumber0(W0) ) )
& xm != xp
& ( sdtlseqdt0(xn,xp)
| ? [W0] :
( sdtpldt0(xn,W0) = xp
& aNaturalNumber0(W0) ) )
& xn != xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
( doDivides0(xp,xm)
| ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ ( doDivides0(xp,xm)
| ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f51,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f68,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f69,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f106,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f108,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f165,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f166,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f167,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f189,plain,
( ~ sdtlseqdt0(xp,xn)
& ! [W0] :
( sdtpldt0(xp,W0) != xn
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f191,plain,
~ sdtlseqdt0(xp,xn),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f192,plain,
( ~ sdtlseqdt0(xp,xm)
& ! [W0] :
( sdtpldt0(xp,W0) != xm
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f194,plain,
~ sdtlseqdt0(xp,xm),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f195,plain,
( ( ~ sdtlseqdt0(xm,xp)
& ! [W0] :
( sdtpldt0(xm,W0) != xp
| ~ aNaturalNumber0(W0) ) )
| xm = xp
| ( ~ sdtlseqdt0(xn,xp)
& ! [W0] :
( sdtpldt0(xn,W0) != xp
| ~ aNaturalNumber0(W0) ) )
| xn = xp ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f196,definition,
( sP2_prd
<=> ( ~ sdtlseqdt0(xn,xp)
& ! [W0] :
( sdtpldt0(xn,W0) != xp
| ~ aNaturalNumber0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f197,plain,
( ( ~ sdtlseqdt0(xm,xp)
& ! [W0] :
( sdtpldt0(xm,W0) != xp
| ~ aNaturalNumber0(W0) ) )
| xm = xp
| sP2_prd
| xn = xp ),
inference(formula_renaming,[status(thm)],[f195,f196]) ).
fof(f199,plain,
( ~ sdtlseqdt0(xm,xp)
| xm = xp
| sP2_prd
| xn = xp ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f200,plain,
( ~ doDivides0(xp,xm)
& ! [W0] :
( xm != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
& ~ doDivides0(xp,xn)
& ! [W0] :
( xn != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f201,plain,
! [X0] :
( xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [X0] :
( xm != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f225,plain,
( ( sdtlseqdt0(xn,xp)
| ? [W0] :
( sdtpldt0(xn,W0) = xp
& aNaturalNumber0(W0) )
| sP2_prd )
& ( ( ~ sdtlseqdt0(xn,xp)
& ! [W0] :
( sdtpldt0(xn,W0) != xp
| ~ aNaturalNumber0(W0) ) )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f196]) ).
fof(f226,plain,
( ( sdtlseqdt0(xn,xp)
| ( sdtpldt0(xn,sK9_skl) = xp
& aNaturalNumber0(sK9_skl) )
| sP2_prd )
& ( ( ~ sdtlseqdt0(xn,xp)
& ! [W0] :
( sdtpldt0(xn,W0) != xp
| ~ aNaturalNumber0(W0) ) )
| ~ sP2_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W0,sK9_skl)],[f225]) ).
fof(f228,plain,
( ~ sdtlseqdt0(xn,xp)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f231,definition,
( sQ0_spl
<=> xn = xp ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f232,plain,
( ~ sQ0_spl
| xn = xp ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f234,definition,
( sQ1_spl
<=> sP2_prd ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f237,definition,
( sQ2_spl
<=> xm = xp ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f238,plain,
( ~ sQ2_spl
| xm = xp ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f244,definition,
( sQ4_spl
<=> sdtlseqdt0(xm,xp) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( ~ sQ4_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f199,f231,f234,f237,f244]) ).
fof(f252,definition,
( sQ6_spl
<=> sdtlseqdt0(xn,xp) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f255,plain,
( ~ sQ6_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f228,f234,f252]) ).
fof(f281,definition,
( sQ9_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f283,plain,
( sQ9_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f298,plain,
! [X0] :
( ~ sQ2_spl
| xp != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(backward_demodulation,[status(thm)],[f238,f203]) ).
fof(f303,plain,
! [X0] :
( ~ sQ0_spl
| xp != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(backward_demodulation,[status(thm)],[f232,f201]) ).
fof(f320,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f283,f167]) ).
fof(f321,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f320]) ).
fof(f362,definition,
( sQ22_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( sQ22_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f362]) ).
fof(f368,definition,
( sQ24_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( sQ24_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f394,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f166]) ).
fof(f395,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f394]) ).
fof(f396,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f165]) ).
fof(f397,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f396]) ).
fof(f656,definition,
! [X0] :
( sQ69_spl
<=> ~ aNaturalNumber0(X0) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f657,plain,
! [X0] :
( ~ sQ69_spl
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f656]) ).
fof(f689,definition,
( sQ72_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ72_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f735,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f691,f51]) ).
fof(f736,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f735]) ).
fof(f824,plain,
( ~ sQ69_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f165,f657]) ).
fof(f831,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f824]) ).
fof(f1266,plain,
( sdtlseqdt0(xn,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f108,f191]) ).
fof(f1267,plain,
( sdtlseqdt0(xm,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f108,f194]) ).
fof(f1285,plain,
( sQ6_spl
| ~ sQ9_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1266,f368,f281,f252]) ).
fof(f1286,plain,
( sQ4_spl
| ~ sQ9_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1267,f362,f281,f244]) ).
fof(f1319,plain,
( ~ sQ0_spl
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f303,f69]) ).
fof(f1321,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1319,f689,f281,f231]) ).
fof(f1323,plain,
( ~ sQ2_spl
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f298,f69]) ).
fof(f1325,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1323,f689,f281,f237]) ).
fof(f1327,plain,
$false,
inference(sat_refutation,[status(thm)],[f247,f255,f321,f395,f397,f736,f831,f1285,f1286,f1321,f1325]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM521+3 : 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.35 % Computer : n006.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 02:37:12 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.42 % Elapsed time: 0.067361 seconds
% 0.14/0.42 % CPU time: 0.258100 seconds
% 0.14/0.42 % Total memory used: 108.304 MB
% 0.14/0.42 % Net memory used: 107.927 MB
%------------------------------------------------------------------------------