%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM423+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:29 PM UTC 2026
% Result : Theorem 0.21s 0.68s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 64 ( 16 unt; 10 def)
% Number of atoms : 196 ( 45 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 223 ( 91 ~; 88 |; 28 &)
% ( 12 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 9 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 50 ( 46 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,definition,
! [W0] :
( aInteger0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,definition,
! [W0,W1,W2] :
( ( W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
( xq != sz00
& aInteger0(xq)
& aInteger0(xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,conjecture,
sdteqdtlpzmzozddtrp0(xa,xa,xq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
~ sdteqdtlpzmzozddtrp0(xa,xa,xq),
inference(negated_conjecture,[status(cth)],[f21]) ).
fof(f26,plain,
aInteger0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f41,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f42,plain,
! [X0] :
( sdtpldt0(X0,smndt0(X0)) = sz00
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f54,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f55,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f62,plain,
! [W0] :
( ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f63,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [W0] :
( ( ! [W1] :
( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ! [W1] :
( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
! [W0] :
( ( ! [W1] :
( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ! [W1] :
( ( sdtasdt0(W1,sK0_skl(W1,W0)) = W0
& aInteger0(sK0_skl(W1,W0))
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f64]) ).
fof(f70,plain,
! [X0,X1,X2] :
( sdtasdt0(X1,X2) != X0
| ~ aInteger0(X2)
| X1 = sz00
| ~ aInteger0(X1)
| aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f71,plain,
! [W0,W1,W2] :
( ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) )
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f72,plain,
! [W0,W1,W2] :
( ( ( ~ aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))
| sdteqdtlpzmzozddtrp0(W0,W1,W2) )
& ( aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2) ) )
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X0,X1,X2)
| X2 = sz00
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f75,plain,
aInteger0(xa),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f76,plain,
aInteger0(xq),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f77,plain,
xq != sz00,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f78,plain,
~ sdteqdtlpzmzozddtrp0(xa,xa,xq),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f111,plain,
! [X0,X1] :
( ~ aDivisorOf0(xq,sdtpldt0(X0,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X0,X1,xq)
| xq = sz00
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f76,f74]) ).
fof(f121,definition,
( sQ6_spl
<=> xq = sz00 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f122,plain,
( ~ sQ6_spl
| xq = sz00 ),
inference(component_clause,[status(thm)],[f121]) ).
fof(f125,definition,
! [X0,X1] :
( sQ7_spl
<=> ( ~ aDivisorOf0(xq,sdtpldt0(X0,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X0,X1,xq)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f126,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ aDivisorOf0(xq,sdtpldt0(X0,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X0,X1,xq)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(component_clause,[status(thm)],[f125]) ).
fof(f128,plain,
( sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f111,f125,f121]) ).
fof(f143,definition,
( sQ11_spl
<=> aInteger0(xa) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f145,plain,
( sQ11_spl
| ~ aInteger0(xa) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f227,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f122,f77]) ).
fof(f228,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f227]) ).
fof(f231,definition,
( sQ22_spl
<=> aInteger0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( sQ22_spl
| ~ aInteger0(sz00) ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f234,definition,
( sQ23_spl
<=> aInteger0(xq) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( sQ23_spl
| ~ aInteger0(xq) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f341,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f236,f76]) ).
fof(f342,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f341]) ).
fof(f343,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f233,f26]) ).
fof(f344,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f343]) ).
fof(f348,plain,
sdtpldt0(xa,smndt0(xa)) = sz00,
inference(resolution,[status(thm)],[f75,f42]) ).
fof(f505,plain,
sdtasdt0(xq,sz00) = sz00,
inference(resolution,[status(thm)],[f55,f76]) ).
fof(f610,plain,
( ~ sQ7_spl
| ~ aDivisorOf0(xq,sdtpldt0(xa,smndt0(xa)))
| ~ aInteger0(xa)
| ~ aInteger0(xa) ),
inference(resolution,[status(thm)],[f126,f78]) ).
fof(f611,definition,
( sQ51_spl
<=> aDivisorOf0(xq,sdtpldt0(xa,smndt0(xa))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( sQ51_spl
| ~ aDivisorOf0(xq,sdtpldt0(xa,smndt0(xa))) ),
inference(component_clause,[status(thm)],[f611]) ).
fof(f614,plain,
( ~ sQ7_spl
| ~ sQ51_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f610,f143,f611,f125]) ).
fof(f615,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f145,f75]) ).
fof(f616,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f615]) ).
fof(f874,plain,
! [X0] :
( sQ51_spl
| sdtasdt0(xq,X0) != sdtpldt0(xa,smndt0(xa))
| ~ aInteger0(X0)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(sdtpldt0(xa,smndt0(xa))) ),
inference(resolution,[status(thm)],[f70,f613]) ).
fof(f879,definition,
( sQ67_spl
<=> aInteger0(sdtpldt0(xa,smndt0(xa))) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f881,plain,
( sQ67_spl
| ~ aInteger0(sdtpldt0(xa,smndt0(xa))) ),
inference(component_clause,[status(thm)],[f879]) ).
fof(f882,definition,
! [X0] :
( sQ68_spl
<=> ( sdtasdt0(xq,X0) != sdtpldt0(xa,smndt0(xa))
| ~ aInteger0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f883,plain,
! [X0] :
( ~ sQ68_spl
| sdtasdt0(xq,X0) != sdtpldt0(xa,smndt0(xa))
| ~ aInteger0(X0) ),
inference(component_clause,[status(thm)],[f882]) ).
fof(f885,plain,
( sQ51_spl
| sQ68_spl
| sQ6_spl
| ~ sQ23_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f874,f879,f234,f121,f882,f611]) ).
fof(f1269,plain,
( sQ67_spl
| ~ aInteger0(sz00) ),
inference(backward_demodulation,[status(thm)],[f348,f881]) ).
fof(f1274,plain,
( sQ67_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1269,f231,f879]) ).
fof(f1290,plain,
! [X0] :
( ~ sQ68_spl
| sdtasdt0(xq,X0) != sz00
| ~ aInteger0(X0) ),
inference(forward_demodulation,[status(thm)],[f348,f883]) ).
fof(f1461,plain,
( ~ sQ68_spl
| sdtasdt0(xq,sz00) != sz00 ),
inference(resolution,[status(thm)],[f1290,f26]) ).
fof(f2140,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f505,f1461]) ).
fof(f2141,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f2140]) ).
fof(f2142,plain,
$false,
inference(sat_refutation,[status(thm)],[f128,f228,f342,f344,f614,f616,f885,f1274,f2141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM423+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n009.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 02:28:12 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.21/0.68 % Refutation found
% 0.21/0.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/0.70 % Elapsed time: 0.250376 seconds
% 0.21/0.70 % CPU time: 1.656022 seconds
% 0.21/0.70 % Total memory used: 102.714 MB
% 0.21/0.70 % Net memory used: 100.971 MB
%------------------------------------------------------------------------------