%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM514+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 : n004.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:48 PM UTC 2026
% Result : Theorem 0.14s 10.55s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 22
% Syntax : Number of formulae : 92 ( 28 unt; 14 def)
% Number of atoms : 271 ( 61 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 295 ( 116 ~; 118 |; 38 &)
% ( 17 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 12 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 54 ( 50 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
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(f30,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
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(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
( isPrime0(xr)
& doDivides0(xr,xk)
& aNaturalNumber0(xr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
sdtasdt0(xp,sdtsldt0(xk,xr)) = sdtasdt0(sdtsldt0(xn,xr),xm),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f61,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f66,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f139,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(f140,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)],[f139]) ).
fof(f141,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))],[f140]) ).
fof(f144,plain,
! [X0,X1,X2] :
( X1 != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f145,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(f146,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)],[f145]) ).
fof(f147,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)],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f161,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(f162,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)],[f161]) ).
fof(f163,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))],[f162]) ).
fof(f164,plain,
! [X0] :
( X0 != sz00
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f176,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f177,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f178,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f181,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f182,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f189,plain,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f195,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f196,plain,
doDivides0(xr,xk),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f197,plain,
isPrime0(xr),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f208,plain,
sdtasdt0(xp,sdtsldt0(xk,xr)) = sdtasdt0(sdtsldt0(xn,xr),xm),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f209,plain,
~ doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f225,plain,
! [X0,X2] :
( ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f144]) ).
fof(f226,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| doDivides0(X0,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f67]) ).
fof(f227,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f148]) ).
fof(f231,plain,
( ~ isPrime0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(destructive_equality_resolution,[status(thm)],[f164]) ).
fof(f232,plain,
~ isPrime0(sz00),
inference(forward_subsumption_resolution,[status(thm)],[f231,f61]) ).
fof(f236,plain,
~ doDivides0(xp,sdtasdt0(xp,sdtsldt0(xk,xr))),
inference(forward_demodulation,[status(thm)],[f208,f209]) ).
fof(f237,plain,
( ~ aNaturalNumber0(sdtsldt0(xk,xr))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f226,f236]) ).
fof(f238,definition,
( sQ2_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f240,plain,
( sQ2_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f238]) ).
fof(f241,definition,
( sQ3_spl
<=> aNaturalNumber0(sdtsldt0(xk,xr)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( sQ3_spl
| ~ aNaturalNumber0(sdtsldt0(xk,xr)) ),
inference(component_clause,[status(thm)],[f241]) ).
fof(f244,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f237,f238,f241]) ).
fof(f245,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f240,f178]) ).
fof(f246,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f245]) ).
fof(f251,definition,
( sQ4_spl
<=> aNaturalNumber0(sdtasdt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( sQ4_spl
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f261,definition,
( sQ7_spl
<=> aNaturalNumber0(xr) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( sQ7_spl
| ~ aNaturalNumber0(xr) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f268,definition,
( sQ9_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f270,plain,
( sQ9_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f280,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f195]) ).
fof(f281,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f280]) ).
fof(f290,plain,
( sQ4_spl
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f253,f67]) ).
fof(f291,definition,
( sQ12_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ12_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,plain,
( sQ4_spl
| ~ sQ12_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f290,f268,f291,f251]) ).
fof(f295,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f270,f176]) ).
fof(f296,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f295]) ).
fof(f314,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f177]) ).
fof(f315,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f314]) ).
fof(f348,plain,
( sQ3_spl
| ~ doDivides0(xr,xk)
| xr = sz00
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xr) ),
inference(resolution,[status(thm)],[f227,f243]) ).
fof(f349,definition,
( sQ16_spl
<=> aNaturalNumber0(xk) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f352,definition,
( sQ17_spl
<=> xr = sz00 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( ~ sQ17_spl
| xr = sz00 ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,definition,
( sQ18_spl
<=> doDivides0(xr,xk) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ18_spl
| ~ doDivides0(xr,xk) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,plain,
( sQ3_spl
| ~ sQ18_spl
| sQ17_spl
| ~ sQ16_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f348,f261,f349,f352,f355,f241]) ).
fof(f359,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f196]) ).
fof(f360,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( ~ sQ17_spl
| isPrime0(sz00) ),
inference(backward_demodulation,[status(thm)],[f353,f197]) ).
fof(f377,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f362,f232]) ).
fof(f378,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f377]) ).
fof(f523,definition,
( sQ40_spl
<=> xp = sz00 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f524,plain,
( ~ sQ40_spl
| xp = sz00 ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f546,plain,
( ~ sQ40_spl
| isPrime0(sz00) ),
inference(backward_demodulation,[status(thm)],[f524,f181]) ).
fof(f553,plain,
( ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f232]) ).
fof(f554,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f553]) ).
fof(f612,plain,
( aNaturalNumber0(xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f189,f227]) ).
fof(f620,definition,
( sQ51_spl
<=> doDivides0(xp,sdtasdt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( sQ51_spl
| ~ doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(component_clause,[status(thm)],[f620]) ).
fof(f627,plain,
( sQ16_spl
| ~ sQ51_spl
| sQ40_spl
| ~ sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f612,f238,f251,f523,f620,f349]) ).
fof(f628,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f622,f182]) ).
fof(f629,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f628]) ).
fof(f630,plain,
$false,
inference(sat_refutation,[status(thm)],[f244,f246,f281,f294,f296,f315,f358,f360,f378,f554,f627,f629]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM514+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n004.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Mon Sep 21 02:37:15 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.14/10.40 % Drodi V4.1.1
% 0.14/10.55 % Refutation found
% 0.14/10.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/10.57 % Elapsed time: 0.177316 seconds
% 0.14/10.57 % CPU time: 1.163963 seconds
% 0.14/10.57 % Total memory used: 121.284 MB
% 0.14/10.57 % Net memory used: 119.764 MB
%------------------------------------------------------------------------------