%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM483+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 : n019.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:41 PM UTC 2026
% Result : Theorem 11.89s 1.96s
% Output : CNFRefutation 11.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 12
% Syntax : Number of formulae : 93 ( 15 unt; 2 def)
% Number of atoms : 499 ( 170 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 605 ( 199 ~; 283 |; 105 &)
% ( 3 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 134 ( 111 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> iLess0(W0,W1) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W1,W2)
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( W1 != sz00
& doDivides0(W0,W1) )
=> sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
aNaturalNumber0(xk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ( iLess0(W0,xk)
=> ? [W1] :
( isPrime0(W1)
& ! [W2] :
( ( ( doDivides0(W2,W1)
| ? [W3] :
( W1 = sdtasdt0(W2,W3)
& aNaturalNumber0(W3) ) )
& aNaturalNumber0(W2) )
=> ( W2 = W1
| W2 = sz10 ) )
& W1 != sz10
& W1 != sz00
& doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
( xk != sz10
& xk != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
~ ( isPrime0(xk)
| ! [W0] :
( ( doDivides0(W0,xk)
& ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) )
& aNaturalNumber0(W0) )
=> ( W0 = xk
| W0 = sz10 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,conjecture,
? [W0] :
( ( isPrime0(W0)
| ( ! [W1] :
( ( doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) )
& ( doDivides0(W0,xk)
| ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
~ ? [W0] :
( ( isPrime0(W0)
| ( ! [W1] :
( ( doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) )
& ( doDivides0(W0,xk)
| ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f52,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f53,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f68,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f70,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f123,plain,
! [W0,W1] :
( iLess0(W0,W1)
| ~ sdtlseqdt0(W0,W1)
| W0 = W1
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f124,plain,
! [X0,X1] :
( iLess0(X0,X1)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,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(f126,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)],[f125]) ).
fof(f127,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))],[f126]) ).
fof(f130,plain,
! [X0,X1,X2] :
( X1 != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f137,plain,
! [W0,W1,W2] :
( doDivides0(W0,W2)
| ~ doDivides0(W1,W2)
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f138,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f143,plain,
! [W0,W1] :
( sdtlseqdt0(W0,W1)
| W1 = sz00
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f144,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| X1 = sz00
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f157,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f158,plain,
! [W0] :
( ? [W1] :
( isPrime0(W1)
& ! [W2] :
( W2 = W1
| W2 = sz10
| ( ~ doDivides0(W2,W1)
& ! [W3] :
( W1 != sdtasdt0(W2,W3)
| ~ aNaturalNumber0(W3) ) )
| ~ aNaturalNumber0(W2) )
& W1 != sz10
& W1 != sz00
& doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) )
| ~ iLess0(W0,xk)
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f159,plain,
! [W0] :
( ( isPrime0(sK3_skl(W0))
& ! [W2] :
( W2 = sK3_skl(W0)
| W2 = sz10
| ( ~ doDivides0(W2,sK3_skl(W0))
& ! [W3] :
( sK3_skl(W0) != sdtasdt0(W2,W3)
| ~ aNaturalNumber0(W3) ) )
| ~ aNaturalNumber0(W2) )
& sK3_skl(W0) != sz10
& sK3_skl(W0) != sz00
& doDivides0(sK3_skl(W0),W0)
& W0 = sdtasdt0(sK3_skl(W0),sK4_skl(W0))
& aNaturalNumber0(sK4_skl(W0))
& aNaturalNumber0(sK3_skl(W0)) )
| ~ iLess0(W0,xk)
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(W1,sK3_skl(W0)),skolemize(W2,sK4_skl(W0))],[f158]) ).
fof(f160,plain,
! [X0] :
( aNaturalNumber0(sK3_skl(X0))
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f163,plain,
! [X0] :
( doDivides0(sK3_skl(X0),X0)
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f168,plain,
! [X0] :
( isPrime0(sK3_skl(X0))
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f169,plain,
xk != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f171,plain,
( ~ isPrime0(xk)
& ? [W0] :
( W0 != xk
& W0 != sz10
& doDivides0(W0,xk)
& ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) )
& aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f172,plain,
( ~ isPrime0(xk)
& sK5_skl != xk
& sK5_skl != sz10
& doDivides0(sK5_skl,xk)
& xk = sdtasdt0(sK5_skl,sK6_skl)
& aNaturalNumber0(sK6_skl)
& aNaturalNumber0(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(W0,sK5_skl),skolemize(W1,sK6_skl)],[f171]) ).
fof(f173,plain,
aNaturalNumber0(sK5_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
aNaturalNumber0(sK6_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f175,plain,
xk = sdtasdt0(sK5_skl,sK6_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f176,plain,
doDivides0(sK5_skl,xk),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f177,plain,
sK5_skl != sz10,
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f178,plain,
sK5_skl != xk,
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f180,plain,
! [W0] :
( ( ~ isPrime0(W0)
& ( ? [W1] :
( W1 != W0
& W1 != sz10
& doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) )
| W0 = sz10
| W0 = sz00 ) )
| ( ~ doDivides0(W0,xk)
& ! [W1] :
( xk != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f181,definition,
! [W0] :
( sP0_prd(W0)
<=> ( ~ doDivides0(W0,xk)
& ! [W1] :
( xk != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f182,plain,
! [W0] :
( ( ~ isPrime0(W0)
& ( ? [W1] :
( W1 != W0
& W1 != sz10
& doDivides0(W1,W0)
& ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) )
& aNaturalNumber0(W1) )
| W0 = sz10
| W0 = sz00 ) )
| sP0_prd(W0)
| ~ aNaturalNumber0(W0) ),
inference(formula_renaming,[status(thm)],[f180,f181]) ).
fof(f183,plain,
! [W0] :
( ( ~ isPrime0(W0)
& ( ( sK7_skl(W0) != W0
& sK7_skl(W0) != sz10
& doDivides0(sK7_skl(W0),W0)
& W0 = sdtasdt0(sK7_skl(W0),sK8_skl(W0))
& aNaturalNumber0(sK8_skl(W0))
& aNaturalNumber0(sK7_skl(W0)) )
| W0 = sz10
| W0 = sz00 ) )
| sP0_prd(W0)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W1,sK7_skl(W0)),skolemize(W2,sK8_skl(W0))],[f182]) ).
fof(f190,plain,
! [X0] :
( ~ isPrime0(X0)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f191,plain,
! [W0] :
( ( doDivides0(W0,xk)
| ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) )
| sP0_prd(W0) )
& ( ( ~ doDivides0(W0,xk)
& ! [W1] :
( xk != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ sP0_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f181]) ).
fof(f192,plain,
( ! [W0] :
( doDivides0(W0,xk)
| ? [W1] :
( xk = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) )
| sP0_prd(W0) )
& ! [W0] :
( ( ~ doDivides0(W0,xk)
& ! [W1] :
( xk != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ sP0_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
( ! [W0] :
( doDivides0(W0,xk)
| ( xk = sdtasdt0(W0,sK9_skl(W0))
& aNaturalNumber0(sK9_skl(W0)) )
| sP0_prd(W0) )
& ! [W0] :
( ( ~ doDivides0(W0,xk)
& ! [W1] :
( xk != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ sP0_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W1,sK9_skl(W0))],[f192]) ).
fof(f195,plain,
! [X0] :
( ~ doDivides0(X0,xk)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f196,plain,
! [X0] :
( doDivides0(X0,xk)
| aNaturalNumber0(sK9_skl(X0))
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
! [X0] :
( doDivides0(X0,xk)
| xk = sdtasdt0(X0,sK9_skl(X0))
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f206,plain,
! [X0,X2] :
( ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f130]) ).
fof(f207,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| doDivides0(X0,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f206,f53]) ).
fof(f341,plain,
! [X0] :
( doDivides0(X0,xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(sK9_skl(X0))
| doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f197,f207]) ).
fof(f346,plain,
! [X0] :
( sP0_prd(X0)
| ~ aNaturalNumber0(sK9_skl(X0))
| doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f341]) ).
fof(f347,plain,
! [X0] :
( sP0_prd(X0)
| doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f196]) ).
fof(f373,plain,
! [X0] :
( sdtlseqdt0(X0,xk)
| xk = sz00
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(X0)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f347,f144]) ).
fof(f375,plain,
! [X0] :
( sdtlseqdt0(X0,xk)
| xk = sz00
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f373]) ).
fof(f376,plain,
! [X0] :
( sdtlseqdt0(X0,xk)
| xk = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f157]) ).
fof(f377,plain,
! [X0] :
( iLess0(X0,xk)
| X0 = xk
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(X0)
| xk = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f376,f124]) ).
fof(f378,plain,
! [X0] :
( iLess0(X0,xk)
| X0 = xk
| ~ aNaturalNumber0(xk)
| xk = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f377]) ).
fof(f379,plain,
! [X0] :
( iLess0(X0,xk)
| X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f378,f169]) ).
fof(f422,plain,
! [X0] :
( aNaturalNumber0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0)
| X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f379,f160]) ).
fof(f423,plain,
! [X0] :
( isPrime0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0)
| X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f379,f168]) ).
fof(f426,plain,
! [X0] :
( aNaturalNumber0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f422]) ).
fof(f427,plain,
! [X0] :
( aNaturalNumber0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f157]) ).
fof(f428,plain,
! [X0] :
( isPrime0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f423]) ).
fof(f429,plain,
! [X0] :
( isPrime0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f428,f157]) ).
fof(f440,plain,
! [X0] :
( sP0_prd(sK3_skl(X0))
| ~ aNaturalNumber0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f429,f190]) ).
fof(f441,plain,
! [X0] :
( sP0_prd(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| X0 = xk
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f427]) ).
fof(f546,plain,
! [X0,X1] :
( sP0_prd(X1)
| ~ aNaturalNumber0(X1)
| doDivides0(X0,xk)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f138,f347]) ).
fof(f557,plain,
! [X0,X1] :
( sP0_prd(X1)
| doDivides0(X0,xk)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f546]) ).
fof(f558,plain,
! [X0,X1] :
( sP0_prd(X1)
| doDivides0(X0,xk)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f157]) ).
fof(f565,plain,
~ sP0_prd(sK5_skl),
inference(resolution,[status(thm)],[f176,f195]) ).
fof(f589,plain,
! [X0] :
( ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0)
| sP0_prd(X0)
| doDivides0(sK3_skl(X0),xk)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3_skl(X0)) ),
inference(resolution,[status(thm)],[f558,f163]) ).
fof(f595,plain,
! [X0] :
( ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| doDivides0(sK3_skl(X0),xk)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3_skl(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f589]) ).
fof(f596,plain,
! [X0] :
( ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| doDivides0(sK3_skl(X0),xk)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f595,f160]) ).
fof(f827,plain,
! [X0] :
( ~ sP0_prd(sK3_skl(X0))
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f596,f195]) ).
fof(f835,plain,
! [X0] :
( X0 = sz10
| X0 = sz00
| X0 = xk
| sP0_prd(X0)
| ~ aNaturalNumber0(X0)
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f827,f441]) ).
fof(f837,plain,
! [X0] :
( X0 = xk
| ~ iLess0(X0,xk)
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f835]) ).
fof(f843,plain,
! [X0] :
( X0 = xk
| ~ aNaturalNumber0(xk)
| sP0_prd(X0)
| ~ aNaturalNumber0(X0)
| X0 = xk
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f837,f379]) ).
fof(f852,plain,
! [X0] :
( ~ aNaturalNumber0(xk)
| X0 = xk
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f843]) ).
fof(f853,plain,
! [X0] :
( X0 = xk
| X0 = sz10
| X0 = sz00
| sP0_prd(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f852,f157]) ).
fof(f866,plain,
( sK5_skl = xk
| sK5_skl = sz10
| sK5_skl = sz00
| sP0_prd(sK5_skl) ),
inference(resolution,[status(thm)],[f853,f173]) ).
fof(f885,plain,
( sK5_skl = xk
| sK5_skl = sz10
| sK5_skl = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f866,f565]) ).
fof(f888,plain,
( sK5_skl = xk
| sK5_skl = sz00 ),
inference(resolution,[status(thm)],[f885,f177]) ).
fof(f908,plain,
xk = sdtasdt0(sz00,sK6_skl),
inference(backward_demodulation,[status(thm)],[f909,f175]) ).
fof(f909,plain,
sK5_skl = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f888,f178]) ).
fof(f1096,plain,
( sz00 = xk
| ~ aNaturalNumber0(sK6_skl) ),
inference(paramodulation,[status(thm)],[f908,f70]) ).
fof(f1280,plain,
sz00 != sz00,
inference(backward_demodulation,[status(thm)],[f1281,f169]) ).
fof(f1281,plain,
sz00 = xk,
inference(forward_subsumption_resolution,[status(thm)],[f1096,f174]) ).
fof(f1587,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f1280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM483+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:34:04 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 11.89/1.96 % Refutation found
% 11.89/1.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.89/1.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.21/2.01 % Elapsed time: 1.636942 seconds
% 7.21/2.01 % CPU time: 12.482284 seconds
% 7.21/2.01 % Total memory used: 167.805 MB
% 7.21/2.01 % Net memory used: 160.277 MB
%------------------------------------------------------------------------------