%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM498+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 : 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:45 PM UTC 2026
% Result : Theorem 0.18s 0.52s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 8
% Syntax : Number of formulae : 55 ( 12 unt; 0 def)
% Number of atoms : 191 ( 116 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 198 ( 62 ~; 76 |; 53 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 33 ( 24 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
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(f17,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| 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))
& ? [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(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/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(f46,conjecture,
( ( xk = sz10
| xk = sz00 )
=> ( doDivides0(xp,xm)
| ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ( ( xk = sz10
| xk = sz00 )
=> ( 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)],[f46]) ).
fof(f69,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f70,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f73,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f87,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f88,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f166,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f167,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f168,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f180,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(f181,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)],[f180]) ).
fof(f184,plain,
! [X0,X1] :
( X0 = xp
| X0 = sz10
| xp != sdtasdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f196,plain,
( sdtlseqdt0(xm,xp)
& sdtpldt0(xm,sK7_skl) = xp
& aNaturalNumber0(sK7_skl)
& xm != xp
& sdtlseqdt0(xn,xp)
& sdtpldt0(xn,sK6_skl) = xp
& aNaturalNumber0(sK6_skl)
& xn != xp ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44]) ).
fof(f197,plain,
xn != xp,
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f205,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f206,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f208,plain,
( ~ doDivides0(xp,xm)
& ! [W0] :
( xm != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
& ~ doDivides0(xp,xn)
& ! [W0] :
( xn != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
& ( xk = sz10
| xk = sz00 ) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f209,plain,
( xk = sz10
| xk = sz00 ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f210,plain,
! [X0] :
( xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f212,plain,
! [X0] :
( xm != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f265,plain,
( xk = sz00
| sdtasdt0(xn,xm) = sdtasdt0(xp,sz10) ),
inference(paramodulation,[status(thm)],[f209,f206]) ).
fof(f266,plain,
( xm != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(xk) ),
inference(paramodulation,[status(thm)],[f206,f212]) ).
fof(f267,plain,
( xn != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(xk) ),
inference(paramodulation,[status(thm)],[f206,f210]) ).
fof(f269,plain,
xm != sdtasdt0(xn,xm),
inference(forward_subsumption_resolution,[status(thm)],[f266,f205]) ).
fof(f270,plain,
xn != sdtasdt0(xn,xm),
inference(forward_subsumption_resolution,[status(thm)],[f267,f205]) ).
fof(f283,plain,
( xk = sz00
| sdtasdt0(xn,xm) = xp
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f265,f70]) ).
fof(f287,plain,
( xk = sz00
| sdtasdt0(xn,xm) = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f283,f168]) ).
fof(f478,plain,
( xk = sz00
| xn = xp
| xn = sz10
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f184,f287]) ).
fof(f487,plain,
( xk = sz00
| xn = xp
| xn = sz10
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f166]) ).
fof(f589,plain,
( xk = sz00
| xn = xp
| xn = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f167]) ).
fof(f590,plain,
( xk = sz00
| xn = sz10 ),
inference(resolution,[status(thm)],[f589,f197]) ).
fof(f647,plain,
( xn = sz10
| sdtasdt0(xn,xm) = sdtasdt0(xp,sz00) ),
inference(paramodulation,[status(thm)],[f590,f206]) ).
fof(f705,plain,
( xn = sz10
| sdtasdt0(xn,xm) = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f647,f73]) ).
fof(f721,plain,
( xn = sz10
| sdtasdt0(xn,xm) = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f168]) ).
fof(f731,plain,
( xm = sz00
| xn = sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn)
| xn = sz10 ),
inference(resolution,[status(thm)],[f721,f88]) ).
fof(f739,plain,
( xn = sz10
| xn != sz00 ),
inference(paramodulation,[status(thm)],[f721,f270]) ).
fof(f740,plain,
( xn = sz10
| xm != sz00 ),
inference(paramodulation,[status(thm)],[f721,f269]) ).
fof(f755,plain,
( xm = sz00
| xn = sz00
| ~ aNaturalNumber0(xm)
| xn = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f166]) ).
fof(f816,plain,
( xm = sz00
| xn = sz00
| xn = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f167]) ).
fof(f817,plain,
( xn = sz10
| xn = sz00
| xn = sz10 ),
inference(resolution,[status(thm)],[f816,f740]) ).
fof(f836,plain,
( xn = sz00
| xn = sz10 ),
inference(duplicate_literals_removal,[status(thm)],[f817]) ).
fof(f837,plain,
xn = sz10,
inference(forward_subsumption_resolution,[status(thm)],[f836,f739]) ).
fof(f877,plain,
xm != sdtasdt0(sz10,xm),
inference(backward_demodulation,[status(thm)],[f837,f269]) ).
fof(f895,plain,
~ aNaturalNumber0(xm),
inference(resolution,[status(thm)],[f877,f71]) ).
fof(f896,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f895,f167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM498+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n004.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 02:34:49 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.18/0.52 % Refutation found
% 0.18/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.18/0.56 % Elapsed time: 0.203295 seconds
% 0.18/0.56 % CPU time: 1.265200 seconds
% 0.18/0.56 % Total memory used: 116.467 MB
% 0.18/0.56 % Net memory used: 115.450 MB
%------------------------------------------------------------------------------