%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM503+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 : 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:46 PM UTC 2026
% Result : Theorem 57.22s 7.92s
% Output : CNFRefutation 57.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 17
% Syntax : Number of formulae : 118 ( 32 unt; 2 def)
% Number of atoms : 470 ( 181 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 570 ( 218 ~; 229 |; 105 &)
% ( 3 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 86 ( 73 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
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(f15,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 != sz00
=> ! [W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W1,W0) = sdtasdt0(W2,W0)
| sdtasdt0(W0,W1) = sdtasdt0(W0,W2) )
=> W1 = W2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& W1 != W2
& W0 != sz00 )
=> ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
~ ( sdtlseqdt0(xp,xm)
| ? [W0] :
( sdtpldt0(xp,W0) = xm
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( xk = sdtsldt0(sdtasdt0(xn,xm),xp)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& aNaturalNumber0(xk) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
~ ( xk = sz10
| xk = sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( sdtlseqdt0(xp,xk)
& ? [W0] :
( sdtpldt0(xp,W0) = xk
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,conjecture,
( ( 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/sandbox/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
~ ( ( 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) ),
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f56,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f77,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f78,plain,
! [X0] :
( sz00 = sdtasdt0(X0,sz00)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f86,plain,
! [W0] :
( ! [W1,W2] :
( W1 = W2
| ( sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f87,plain,
! [X0,X1,X2] :
( sdtasdt0(X2,X0) != sdtasdt0(X2,X1)
| ~ aNaturalNumber0(X1)
| X2 = sz00
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f110,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f111,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f114,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f120,plain,
! [W0,W1,W2] :
( ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ sdtlseqdt0(W1,W2)
| W1 = W2
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f122,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtasdt0(X2,X0),sdtasdt0(X2,X1))
| ~ aNaturalNumber0(X0)
| X2 = sz00
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f124,plain,
! [X0,X1,X2] :
( X2 = sz00
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f128,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f129,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X1,sdtasdt0(X1,X0))
| X0 = sz00 ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f156,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(f157,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)],[f156]) ).
fof(f158,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))],[f157]) ).
fof(f159,plain,
! [X0] :
( X0 != sz00
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f171,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f172,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f173,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f185,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(f186,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)],[f185]) ).
fof(f187,plain,
xp != sz00,
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f192,plain,
aNaturalNumber0(sK5_skl),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f193,plain,
sdtasdt0(xp,sK5_skl) = sdtasdt0(xn,xm),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f198,plain,
( ~ sdtlseqdt0(xp,xm)
& ! [W0] :
( sdtpldt0(xp,W0) != xm
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f199,plain,
! [X0] :
( sdtpldt0(xp,X0) != xm
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f200,plain,
~ sdtlseqdt0(xp,xm),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f201,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(f202,plain,
xn != xp,
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f205,plain,
sdtlseqdt0(xn,xp),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f210,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f211,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f213,plain,
( xk != sz10
& xk != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f214,plain,
sz00 != xk,
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f235,plain,
( sdtlseqdt0(xp,xk)
& sdtpldt0(xp,sK11_skl) = xk
& aNaturalNumber0(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(W0,sK11_skl)],[f50]) ).
fof(f236,plain,
aNaturalNumber0(sK11_skl),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f237,plain,
xk = sdtpldt0(xp,sK11_skl),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f238,plain,
sdtlseqdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f239,plain,
( ( ~ 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) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f240,definition,
( sP2_prd
<=> ( ~ sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ! [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) != sdtasdt0(xp,xm)
| ~ aNaturalNumber0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f241,plain,
( ( ~ sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
& ! [W0] :
( sdtpldt0(sdtasdt0(xp,xm),W0) != sdtasdt0(xp,xk)
| ~ aNaturalNumber0(W0) ) )
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk)
| sP2_prd
| sdtasdt0(xn,xm) = sdtasdt0(xp,xm) ),
inference(formula_renaming,[status(thm)],[f239,f240]) ).
fof(f243,plain,
( sP2_prd
| sdtasdt0(xp,xk) = sdtasdt0(xp,xm)
| ~ sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
| sdtasdt0(xp,xm) = sdtasdt0(xn,xm) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f264,plain,
( ( sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
| ? [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) = sdtasdt0(xp,xm)
& aNaturalNumber0(W0) )
| sP2_prd )
& ( ( ~ sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ! [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) != sdtasdt0(xp,xm)
| ~ aNaturalNumber0(W0) ) )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f240]) ).
fof(f265,plain,
( ( sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
| ( sdtpldt0(sdtasdt0(xn,xm),sK15_skl) = sdtasdt0(xp,xm)
& aNaturalNumber0(sK15_skl) )
| sP2_prd )
& ( ( ~ sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
& ! [W0] :
( sdtpldt0(sdtasdt0(xn,xm),W0) != sdtasdt0(xp,xm)
| ~ aNaturalNumber0(W0) ) )
| ~ sP2_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(W0,sK15_skl)],[f264]) ).
fof(f267,plain,
( ~ sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f280,plain,
( ~ isPrime0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(destructive_equality_resolution,[status(thm)],[f159]) ).
fof(f309,plain,
! [X0] :
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,xm)
| ~ sdtlseqdt0(xp,X0) ),
inference(resolution,[status(thm)],[f200,f111]) ).
fof(f310,plain,
! [X0] :
( ~ sdtlseqdt0(xp,X0)
| ~ sdtlseqdt0(X0,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f309,f173]) ).
fof(f323,plain,
( xk != xm
| ~ aNaturalNumber0(sK11_skl) ),
inference(paramodulation,[status(thm)],[f237,f199]) ).
fof(f325,plain,
xk != xm,
inference(forward_subsumption_resolution,[status(thm)],[f323,f236]) ).
fof(f347,plain,
~ isPrime0(sz00),
inference(forward_subsumption_resolution,[status(thm)],[f280,f56]) ).
fof(f359,plain,
( sP2_prd
| sdtasdt0(xp,xk) = sdtasdt0(xp,xm)
| ~ sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk) ),
inference(backward_demodulation,[status(thm)],[f211,f243]) ).
fof(f363,plain,
( ~ sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(xp,xm))
| ~ sP2_prd ),
inference(backward_demodulation,[status(thm)],[f211,f267]) ).
fof(f377,plain,
( ~ sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))
| sP2_prd
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk) ),
inference(duplicate_literals_removal,[status(thm)],[f359]) ).
fof(f428,plain,
sdtasdt0(xp,sK5_skl) = sdtasdt0(xp,xk),
inference(forward_demodulation,[status(thm)],[f211,f193]) ).
fof(f443,plain,
! [X0] :
( xm = sz00
| ~ aNaturalNumber0(xn)
| sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(X0,xm))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(xn,X0)
| X0 = xn ),
inference(paramodulation,[status(thm)],[f211,f124]) ).
fof(f453,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(X0,xm))
| ~ sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(xn)
| sz00 = xm
| X0 = xn ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f172]) ).
fof(f486,plain,
( ~ aNaturalNumber0(xk)
| xp = sz00
| ~ aNaturalNumber0(sK5_skl)
| ~ aNaturalNumber0(xp)
| sK5_skl = xk ),
inference(resolution,[status(thm)],[f87,f428]) ).
fof(f512,plain,
( xp = sz00
| xk = sK5_skl
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f173]) ).
fof(f669,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK5_skl)
| sdtlseqdt0(xp,sdtasdt0(xp,xk))
| sK5_skl = sz00 ),
inference(paramodulation,[status(thm)],[f428,f129]) ).
fof(f674,plain,
( sdtlseqdt0(xp,sdtasdt0(xp,xk))
| sK5_skl = sz00
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f192]) ).
fof(f750,plain,
( sK5_skl = xk
| sz00 = xp
| ~ aNaturalNumber0(xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f512,f192]) ).
fof(f751,plain,
( sK5_skl = xk
| sz00 = xp ),
inference(resolution,[status(thm)],[f750,f210]) ).
fof(f752,plain,
sK5_skl = xk,
inference(forward_subsumption_resolution,[status(thm)],[f751,f187]) ).
fof(f809,plain,
( sP2_prd
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk)
| ~ aNaturalNumber0(xm)
| xp = sz00
| xk = xm
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xm,xk) ),
inference(resolution,[status(thm)],[f122,f377]) ).
fof(f829,plain,
( sP2_prd
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk)
| sz00 = xp
| ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(xm,xk)
| xk = xm
| ~ aNaturalNumber0(xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f809,f173]) ).
fof(f891,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xm)
| ~ sdtlseqdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f310,f172]) ).
fof(f892,plain,
( ~ sdtlseqdt0(xk,xm)
| ~ aNaturalNumber0(xk) ),
inference(resolution,[status(thm)],[f891,f238]) ).
fof(f901,plain,
~ sdtlseqdt0(xk,xm),
inference(forward_subsumption_resolution,[status(thm)],[f892,f210]) ).
fof(f908,plain,
( ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xm)
| sdtlseqdt0(xm,xk) ),
inference(resolution,[status(thm)],[f901,f114]) ).
fof(f910,plain,
( sdtlseqdt0(xm,xk)
| ~ aNaturalNumber0(xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f908,f172]) ).
fof(f912,plain,
sdtlseqdt0(xm,xk),
inference(forward_subsumption_resolution,[status(thm)],[f910,f210]) ).
fof(f1662,plain,
( sdtlseqdt0(xp,sdtasdt0(xp,xk))
| xk = sz00
| ~ aNaturalNumber0(xp) ),
inference(forward_demodulation,[status(thm)],[f752,f674]) ).
fof(f1663,plain,
( sdtlseqdt0(xp,sdtasdt0(xp,xk))
| sz00 = xk ),
inference(forward_subsumption_resolution,[status(thm)],[f1662,f173]) ).
fof(f5234,plain,
( ~ sdtlseqdt0(xm,xk)
| sP2_prd
| ~ aNaturalNumber0(xm)
| sz00 = xp
| xm = xk
| sdtasdt0(xp,xm) = sdtasdt0(xp,xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f210]) ).
fof(f5238,plain,
( ~ aNaturalNumber0(xm)
| xp = sz00
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| xk = xm
| ~ sdtlseqdt0(xm,xk)
| sP2_prd
| ~ aNaturalNumber0(xm)
| sz00 = xp
| xm = xk ),
inference(resolution,[status(thm)],[f5234,f87]) ).
fof(f5239,plain,
( ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xm,xk)
| sP2_prd
| ~ aNaturalNumber0(xm)
| sz00 = xp
| xm = xk ),
inference(duplicate_literals_removal,[status(thm)],[f5238]) ).
fof(f5240,plain,
( ~ aNaturalNumber0(xp)
| xp = sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xk)
| sP2_prd
| ~ sdtlseqdt0(xm,xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f5239,f325]) ).
fof(f5872,plain,
( ~ aNaturalNumber0(xk)
| sP2_prd
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f5240,f912]) ).
fof(f5873,plain,
( sP2_prd
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f5872,f210]) ).
fof(f5874,plain,
( sz00 = xp
| ~ aNaturalNumber0(xp)
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f5873,f172]) ).
fof(f5875,plain,
( xp = sz00
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f5874,f173]) ).
fof(f6003,plain,
( sP2_prd
| isPrime0(sz00) ),
inference(paramodulation,[status(thm)],[f5875,f191]) ).
fof(f6026,plain,
sP2_prd,
inference(forward_subsumption_resolution,[status(thm)],[f6003,f347]) ).
fof(f6196,plain,
~ sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(xp,xm)),
inference(backward_subsumption_resolution,[status(thm)],[f363,f6026]) ).
fof(f6338,plain,
! [X0] :
( sz00 = xm
| X0 = xn
| ~ sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(X0,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f453,f171]) ).
fof(f6339,plain,
( sz00 = xm
| xp = xn
| ~ sdtlseqdt0(xn,xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f6338,f6196]) ).
fof(f6349,plain,
( xn = xp
| xm = sz00
| ~ sdtlseqdt0(xn,xp) ),
inference(forward_subsumption_resolution,[status(thm)],[f6339,f173]) ).
fof(f6508,plain,
( xm = sz00
| xp = xn ),
inference(forward_subsumption_resolution,[status(thm)],[f6349,f205]) ).
fof(f6555,plain,
( xm = sz00
| xp != xp ),
inference(paramodulation,[status(thm)],[f6508,f202]) ).
fof(f6557,plain,
xm = sz00,
inference(trivial_equality_resolution,[status(thm)],[f6555]) ).
fof(f6630,plain,
sdtasdt0(xp,xk) = sdtasdt0(xn,sz00),
inference(backward_demodulation,[status(thm)],[f6557,f211]) ).
fof(f6633,plain,
~ sdtlseqdt0(xp,sz00),
inference(backward_demodulation,[status(thm)],[f6557,f200]) ).
fof(f6666,plain,
( sz00 = sdtasdt0(xp,xk)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f6630,f78]) ).
fof(f6707,plain,
sz00 = sdtasdt0(xp,xk),
inference(forward_subsumption_resolution,[status(thm)],[f6666,f171]) ).
fof(f6839,plain,
( sdtlseqdt0(xp,sz00)
| sz00 = xk ),
inference(backward_demodulation,[status(thm)],[f6707,f1663]) ).
fof(f6882,plain,
sdtlseqdt0(xp,sz00),
inference(forward_subsumption_resolution,[status(thm)],[f6839,f214]) ).
fof(f7006,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6882,f6633]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM503+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n009.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 02:35:57 UTC 2026
% 0.15/0.44 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 57.22/7.92 % Refutation found
% 57.22/7.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.22/7.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.70/8.00 % Elapsed time: 7.549285 seconds
% 3.70/8.00 % CPU time: 59.067470 seconds
% 3.70/8.00 % Total memory used: 267.693 MB
% 3.70/8.00 % Net memory used: 250.324 MB
%------------------------------------------------------------------------------