%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM529+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 : 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:52 PM UTC 2026
% Result : Theorem 0.14s 0.65s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 30
% Syntax : Number of formulae : 124 ( 28 unt; 18 def)
% Number of atoms : 374 ( 117 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 404 ( 154 ~; 159 |; 59 &)
% ( 18 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 19 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-3 aty)
% Number of variables : 58 ( 51 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,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(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> iLess0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
! [W0,W1,W2] :
( ( W2 != sz00
& W1 != sz00
& W0 != sz00
& aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W2,sdtasdt0(W1,W1)) = sdtasdt0(W0,W0)
=> ( iLess0(W0,xn)
=> ~ ( isPrime0(W2)
| ( ! [W3] :
( ( doDivides0(W3,W2)
& ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) )
& aNaturalNumber0(W3) )
=> ( W3 = W2
| W3 = sz10 ) )
& W2 != sz10 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
( doDivides0(xp,xn)
& ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( xq = sdtsldt0(xn,xp)
& xn = sdtasdt0(xp,xq)
& aNaturalNumber0(xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
( sdtlseqdt0(xm,xn)
& ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) )
& xm != xn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f57,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f67,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f74,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f76,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f83,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(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f129,plain,
! [W0,W1] :
( iLess0(W0,W1)
| ~ sdtlseqdt0(W0,W1)
| W0 = W1
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f130,plain,
! [X0,X1] :
( iLess0(X0,X1)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f171,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f172,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f173,plain,
xn != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f174,plain,
xm != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f175,plain,
xp != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f176,plain,
! [W0,W1,W2] :
( ( ~ isPrime0(W2)
& ( ? [W3] :
( W3 != W2
& W3 != sz10
& doDivides0(W3,W2)
& ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) )
& aNaturalNumber0(W3) )
| W2 = sz10 ) )
| ~ iLess0(W0,xn)
| sdtasdt0(W2,sdtasdt0(W1,W1)) != sdtasdt0(W0,W0)
| W2 = sz00
| W1 = sz00
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f177,plain,
! [W0,W1,W2] :
( ( ~ isPrime0(W2)
& ( ( sK4_skl(W2,W1,W0) != W2
& sK4_skl(W2,W1,W0) != sz10
& doDivides0(sK4_skl(W2,W1,W0),W2)
& W2 = sdtasdt0(sK4_skl(W2,W1,W0),sK5_skl(W2,W1,W0))
& aNaturalNumber0(sK5_skl(W2,W1,W0))
& aNaturalNumber0(sK4_skl(W2,W1,W0)) )
| W2 = sz10 ) )
| ~ iLess0(W0,xn)
| sdtasdt0(W2,sdtasdt0(W1,W1)) != sdtasdt0(W0,W0)
| W2 = sz00
| W1 = sz00
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(W3,sK4_skl(W2,W1,W0)),skolemize(W4,sK5_skl(W2,W1,W0))],[f176]) ).
fof(f184,plain,
! [X0,X1,X2] :
( ~ isPrime0(X2)
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f186,plain,
( isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10 ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f190,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
( doDivides0(xp,xn)
& xn = sdtasdt0(xp,sK7_skl)
& aNaturalNumber0(sK7_skl)
& doDivides0(xp,sdtasdt0(xn,xn))
& sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl)
& aNaturalNumber0(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44]) ).
fof(f192,plain,
aNaturalNumber0(sK6_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f195,plain,
aNaturalNumber0(sK7_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f196,plain,
xn = sdtasdt0(xp,sK7_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f198,plain,
aNaturalNumber0(xq),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f199,plain,
xn = sdtasdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f201,plain,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f202,plain,
( sdtlseqdt0(xm,xn)
& sdtpldt0(xm,sK8_skl) = xn
& aNaturalNumber0(sK8_skl)
& xm != xn ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W0,sK8_skl)],[f47]) ).
fof(f203,plain,
xm != xn,
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f204,plain,
aNaturalNumber0(sK8_skl),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f205,plain,
sdtpldt0(xm,sK8_skl) = xn,
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f206,plain,
sdtlseqdt0(xm,xn),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f222,definition,
( sQ0_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( sQ0_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,definition,
( sQ1_spl
<=> aNaturalNumber0(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f227,plain,
( sQ1_spl
| ~ aNaturalNumber0(sK7_skl) ),
inference(component_clause,[status(thm)],[f225]) ).
fof(f228,definition,
( sQ2_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f233,definition,
( sQ3_spl
<=> aNaturalNumber0(xq) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f235,plain,
( sQ3_spl
| ~ aNaturalNumber0(xq) ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f239,plain,
( aNaturalNumber0(xn)
| ~ aNaturalNumber0(sK8_skl)
| ~ aNaturalNumber0(xm) ),
inference(paramodulation,[status(thm)],[f205,f57]) ).
fof(f240,definition,
( sQ4_spl
<=> aNaturalNumber0(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( sQ4_spl
| ~ aNaturalNumber0(sK8_skl) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ5_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f245,plain,
( sQ5_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f251,plain,
( sQ2_spl
| ~ sQ4_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f239,f243,f240,f228]) ).
fof(f252,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f204]) ).
fof(f253,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f252]) ).
fof(f254,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f171]) ).
fof(f255,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f254]) ).
fof(f268,plain,
( xn = sdtasdt0(xq,xp)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f199,f68]) ).
fof(f272,definition,
( sQ9_spl
<=> xn = sdtasdt0(xq,xp) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f273,plain,
( ~ sQ9_spl
| xn = sdtasdt0(xq,xp) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,plain,
( sQ9_spl
| ~ sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f268,f222,f233,f272]) ).
fof(f282,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f224,f172]) ).
fof(f283,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f282]) ).
fof(f284,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f235,f198]) ).
fof(f285,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f286,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f227,f195]) ).
fof(f287,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f286]) ).
fof(f392,definition,
( sQ31_spl
<=> xm = sz00 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ31_spl
| xm = sz00 ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f513,plain,
! [X0] :
( sK7_skl = X0
| xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK7_skl)
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f196,f84]) ).
fof(f535,definition,
( sQ53_spl
<=> sK7_skl = sz00 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( ~ sQ53_spl
| sK7_skl = sz00 ),
inference(component_clause,[status(thm)],[f535]) ).
fof(f542,definition,
( sQ55_spl
<=> xq = sz00 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ55_spl
| xq = sz00 ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f544,plain,
( sQ55_spl
| xq != sz00 ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f549,definition,
( sQ57_spl
<=> xp = sz00 ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( ~ sQ57_spl
| xp = sz00 ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f556,definition,
! [X0] :
( sQ59_spl
<=> ( sK7_skl = X0
| xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f557,plain,
! [X0] :
( ~ sQ59_spl
| sK7_skl = X0
| xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f559,plain,
( sQ59_spl
| ~ sQ1_spl
| sQ57_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f513,f222,f549,f225,f556]) ).
fof(f569,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f550,f175]) ).
fof(f570,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f569]) ).
fof(f571,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f174]) ).
fof(f572,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f571]) ).
fof(f656,plain,
( ~ sQ55_spl
| xn != xq ),
inference(forward_demodulation,[status(thm)],[f543,f173]) ).
fof(f675,definition,
( sQ72_spl
<=> xn = xq ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f676,plain,
( ~ sQ72_spl
| xn = xq ),
inference(component_clause,[status(thm)],[f675]) ).
fof(f686,definition,
( sQ75_spl
<=> sK7_skl = xq ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( ~ sQ75_spl
| sK7_skl = xq ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f750,plain,
! [X0] :
( ~ sQ55_spl
| xq = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_demodulation,[status(thm)],[f543,f76]) ).
fof(f751,plain,
! [X0] :
( ~ sQ55_spl
| xq = sdtasdt0(xq,X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_demodulation,[status(thm)],[f543,f750]) ).
fof(f752,plain,
( ~ sQ9_spl
| ~ sQ55_spl
| xq = xn
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f273,f751]) ).
fof(f753,plain,
( ~ sQ9_spl
| ~ sQ55_spl
| sQ72_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f752,f222,f675,f542,f272]) ).
fof(f754,plain,
( ~ sQ72_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f676,f656]) ).
fof(f755,plain,
( ~ sQ72_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f754]) ).
fof(f781,definition,
( sQ87_spl
<=> xn = xm ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( ~ sQ87_spl
| xn = xm ),
inference(component_clause,[status(thm)],[f781]) ).
fof(f970,plain,
( ~ sQ59_spl
| sK7_skl = xq
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f557,f199]) ).
fof(f974,plain,
( ~ sQ59_spl
| sQ75_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f970,f233,f686,f556]) ).
fof(f982,plain,
( sQ55_spl
| ~ sQ75_spl
| sK7_skl != sz00 ),
inference(backward_demodulation,[status(thm)],[f687,f544]) ).
fof(f1061,plain,
( ~ sQ53_spl
| sQ55_spl
| ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f536,f982]) ).
fof(f1062,plain,
( ~ sQ53_spl
| sQ55_spl
| ~ sQ75_spl ),
inference(contradiction_clause,[status(thm)],[f1061]) ).
fof(f1452,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f203]) ).
fof(f1453,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1452]) ).
fof(f1482,plain,
( iLess0(xm,xn)
| xm = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f206,f130]) ).
fof(f1485,definition,
( sQ162_spl
<=> iLess0(xm,xn) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( sQ162_spl
| sQ87_spl
| ~ sQ2_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1482,f243,f228,f781,f1485]) ).
fof(f1591,definition,
( sQ169_spl
<=> isPrime0(xp) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( sQ169_spl
| ~ isPrime0(xp) ),
inference(component_clause,[status(thm)],[f1591]) ).
fof(f1599,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1593,f190]) ).
fof(f1600,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f1599]) ).
fof(f1788,definition,
( sQ183_spl
<=> aNaturalNumber0(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1790,plain,
( sQ183_spl
| ~ aNaturalNumber0(sK6_skl) ),
inference(component_clause,[status(thm)],[f1788]) ).
fof(f1822,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1790,f192]) ).
fof(f1823,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f1822]) ).
fof(f1953,plain,
( ~ sQ75_spl
| sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(sK7_skl,xq)) ),
inference(forward_demodulation,[status(thm)],[f687,f201]) ).
fof(f1954,plain,
( ~ sQ75_spl
| sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(sK7_skl,sK7_skl)) ),
inference(forward_demodulation,[status(thm)],[f687,f1953]) ).
fof(f1955,plain,
( ~ sQ75_spl
| ~ isPrime0(xp)
| ~ iLess0(xm,xn)
| xp = sz00
| sK7_skl = sz00
| xm = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK7_skl)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f1954,f184]) ).
fof(f1971,plain,
( ~ sQ75_spl
| ~ sQ169_spl
| ~ sQ162_spl
| sQ57_spl
| sQ53_spl
| sQ31_spl
| ~ sQ0_spl
| ~ sQ1_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1955,f243,f225,f222,f392,f535,f549,f1485,f1591,f686]) ).
fof(f2032,plain,
$false,
inference(sat_refutation,[status(thm)],[f251,f253,f255,f275,f283,f285,f287,f559,f570,f572,f753,f755,f974,f1062,f1453,f1488,f1600,f1823,f1971]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM529+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n019.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.43 % CPULimit : 300
% 0.14/0.43 % WCLimit : 300
% 0.14/0.43 % DateTime : Mon Sep 21 02:38:05 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.45 % Drodi V4.1.1
% 0.14/0.65 % Refutation found
% 0.14/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.68 % Elapsed time: 0.232932 seconds
% 0.14/0.68 % CPU time: 1.381309 seconds
% 0.14/0.68 % Total memory used: 116.820 MB
% 0.14/0.68 % Net memory used: 115.629 MB
%------------------------------------------------------------------------------