%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM504+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:46 PM UTC 2026
% Result : Theorem 0.99s 0.55s
% Output : CNFRefutation 0.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 16
% Syntax : Number of formulae : 70 ( 21 unt; 9 def)
% Number of atoms : 212 ( 50 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 224 ( 82 ~; 75 |; 51 &)
% ( 10 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 9 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 48 ( 40 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
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))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10
& xp != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( xk = sdtsldt0(sdtasdt0(xn,xm),xp)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& aNaturalNumber0(xk) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
( sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& ? [W0] :
( sdtpldt0(sdtasdt0(xp,xm),W0) = sdtasdt0(xp,xk)
& aNaturalNumber0(W0) )
& sdtasdt0(xp,xm) != sdtasdt0(xp,xk)
& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) = sdtasdt0(xp,xm)
& aNaturalNumber0(W0) )
& sdtasdt0(xn,xm) != sdtasdt0(xp,xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f61,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f63,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f95,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(f96,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)],[f95]) ).
fof(f97,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))],[f96]) ).
fof(f100,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f109,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f110,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f174,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f186,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10
& xp != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f187,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK5_skl)
& aNaturalNumber0(sK5_skl)
& isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10
& xp != sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W0,sK5_skl)],[f186]) ).
fof(f194,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,sK5_skl),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f211,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f212,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f240,plain,
( sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& sdtpldt0(sdtasdt0(xp,xm),sK13_skl) = sdtasdt0(xp,xk)
& aNaturalNumber0(sK13_skl)
& sdtasdt0(xp,xm) != sdtasdt0(xp,xk)
& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& sdtpldt0(sdtasdt0(xn,xm),sK12_skl) = sdtasdt0(xp,xm)
& aNaturalNumber0(sK12_skl)
& sdtasdt0(xn,xm) != sdtasdt0(xp,xm) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(W0,sK12_skl),skolemize(W0,sK13_skl)],[f51]) ).
fof(f241,plain,
sdtasdt0(xn,xm) != sdtasdt0(xp,xm),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
aNaturalNumber0(sK12_skl),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f243,plain,
sdtpldt0(sdtasdt0(xn,xm),sK12_skl) = sdtasdt0(xp,xm),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f244,plain,
sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm)),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f246,plain,
aNaturalNumber0(sK13_skl),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f247,plain,
sdtpldt0(sdtasdt0(xp,xm),sK13_skl) = sdtasdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f269,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f100]) ).
fof(f820,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f61]) ).
fof(f1439,definition,
( sQ95_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1441,plain,
( sQ95_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f1439]) ).
fof(f1454,plain,
( sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1441,f174]) ).
fof(f1455,plain,
sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1454]) ).
fof(f1624,definition,
( sQ128_spl
<=> aNaturalNumber0(xk) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1626,plain,
( sQ128_spl
| ~ aNaturalNumber0(xk) ),
inference(component_clause,[status(thm)],[f1624]) ).
fof(f1682,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f211]) ).
fof(f1683,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f1682]) ).
fof(f1981,definition,
( sQ189_spl
<=> aNaturalNumber0(sdtasdt0(xp,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2068,plain,
sdtasdt0(xp,sK5_skl) = sdtasdt0(xp,xk),
inference(forward_demodulation,[status(thm)],[f194,f212]) ).
fof(f2070,plain,
( aNaturalNumber0(sdtasdt0(xp,sK5_skl))
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f2068,f63]) ).
fof(f2075,plain,
( sQ189_spl
| ~ sQ128_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f2070,f1439,f1624,f1981]) ).
fof(f2266,plain,
sdtasdt0(xp,sK5_skl) != sdtasdt0(xp,xm),
inference(forward_demodulation,[status(thm)],[f194,f241]) ).
fof(f2267,plain,
sdtpldt0(sdtasdt0(xp,sK5_skl),sK12_skl) = sdtasdt0(xp,xm),
inference(forward_demodulation,[status(thm)],[f194,f243]) ).
fof(f2272,plain,
( aNaturalNumber0(sdtasdt0(xp,xm))
| ~ aNaturalNumber0(sK12_skl)
| ~ aNaturalNumber0(sdtasdt0(xp,sK5_skl)) ),
inference(paramodulation,[status(thm)],[f2267,f61]) ).
fof(f2279,definition,
( sQ233_spl
<=> aNaturalNumber0(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2281,plain,
( sQ233_spl
| ~ aNaturalNumber0(sK12_skl) ),
inference(component_clause,[status(thm)],[f2279]) ).
fof(f2289,definition,
( sQ235_spl
<=> aNaturalNumber0(sdtasdt0(xp,xm)) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f2292,plain,
( sQ235_spl
| ~ sQ233_spl
| ~ sQ189_spl ),
inference(split_clause,[status(thm)],[f2272,f1981,f2279,f2289]) ).
fof(f2293,plain,
( sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2281,f242]) ).
fof(f2294,plain,
sQ233_spl,
inference(contradiction_clause,[status(thm)],[f2293]) ).
fof(f2296,plain,
sdtlseqdt0(sdtasdt0(xp,sK5_skl),sdtasdt0(xp,xm)),
inference(forward_demodulation,[status(thm)],[f194,f244]) ).
fof(f2300,plain,
( sdtasdt0(xp,xm) = sdtasdt0(xp,sK5_skl)
| ~ sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,sK5_skl))
| ~ aNaturalNumber0(sdtasdt0(xp,sK5_skl))
| ~ aNaturalNumber0(sdtasdt0(xp,xm)) ),
inference(resolution,[status(thm)],[f2296,f110]) ).
fof(f2305,definition,
( sQ236_spl
<=> sdtasdt0(xp,sK5_skl) = sdtasdt0(xp,xm) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2306,plain,
( ~ sQ236_spl
| sdtasdt0(xp,sK5_skl) = sdtasdt0(xp,xm) ),
inference(component_clause,[status(thm)],[f2305]) ).
fof(f2320,definition,
( sQ240_spl
<=> sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f2323,plain,
( sQ236_spl
| ~ sQ240_spl
| ~ sQ189_spl
| ~ sQ235_spl ),
inference(split_clause,[status(thm)],[f2300,f2289,f1981,f2320,f2305]) ).
fof(f2340,plain,
( ~ sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2306,f2266]) ).
fof(f2341,plain,
~ sQ236_spl,
inference(contradiction_clause,[status(thm)],[f2340]) ).
fof(f2343,plain,
sdtpldt0(sdtasdt0(xp,xm),sK13_skl) = sdtasdt0(xp,sK5_skl),
inference(forward_demodulation,[status(thm)],[f2068,f247]) ).
fof(f2345,plain,
( ~ aNaturalNumber0(sK13_skl)
| sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,sK5_skl))
| ~ aNaturalNumber0(sdtasdt0(xp,xm)) ),
inference(paramodulation,[status(thm)],[f2343,f820]) ).
fof(f2352,definition,
( sQ246_spl
<=> aNaturalNumber0(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f2354,plain,
( sQ246_spl
| ~ aNaturalNumber0(sK13_skl) ),
inference(component_clause,[status(thm)],[f2352]) ).
fof(f2356,plain,
( ~ sQ246_spl
| sQ240_spl
| ~ sQ235_spl ),
inference(split_clause,[status(thm)],[f2345,f2289,f2320,f2352]) ).
fof(f2363,plain,
( sQ246_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2354,f246]) ).
fof(f2364,plain,
sQ246_spl,
inference(contradiction_clause,[status(thm)],[f2363]) ).
fof(f2365,plain,
$false,
inference(sat_refutation,[status(thm)],[f1455,f1683,f2075,f2292,f2294,f2323,f2341,f2356,f2364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM504+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n007.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:33:51 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.99/0.55 % Refutation found
% 0.99/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.99/0.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.99/0.59 % Elapsed time: 0.216100 seconds
% 0.99/0.59 % CPU time: 1.440646 seconds
% 0.99/0.59 % Total memory used: 126.143 MB
% 0.99/0.59 % Net memory used: 124.304 MB
%------------------------------------------------------------------------------