%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM510+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 : 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:48 PM UTC 2026
% Result : Theorem 0.14s 10.80s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 15
% Syntax : Number of formulae : 94 ( 30 unt; 1 def)
% Number of atoms : 294 ( 144 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 304 ( 104 ~; 112 |; 73 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 52 ( 44 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
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(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(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(f17,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
~ ( sdtlseqdt0(xp,xn)
| ? [W0] :
( sdtpldt0(xp,W0) = xn
& aNaturalNumber0(W0) ) ),
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,hypothesis,
~ ( xk = sz10
| xk = sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
( isPrime0(xr)
& ! [W0] :
( ( ( doDivides0(W0,xr)
| ? [W1] :
( xr = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xr
| W0 = sz10 ) )
& xr != sz10
& xr != sz00
& doDivides0(xr,xk)
& ? [W0] :
( xk = sdtasdt0(xr,W0)
& aNaturalNumber0(W0) )
& aNaturalNumber0(xr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
( doDivides0(xr,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xr,W0)
& aNaturalNumber0(W0) )
& ? [W0] :
( sdtpldt0(xr,W0) = xk
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
=> ( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ? [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) = xn
& aNaturalNumber0(W0) ) ) )
& ~ ( sdtsldt0(xn,xr) = xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
=> ( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ? [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) = xn
& aNaturalNumber0(W0) ) ) )
& ~ ( sdtsldt0(xn,xr) = xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f59,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f72,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f73,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f76,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f77,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f81,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f88,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(f89,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)],[f88]) ).
fof(f94,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f95,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f130,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f131,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f173,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f174,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f175,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f197,plain,
( ~ sdtlseqdt0(xp,xn)
& ! [W0] :
( sdtpldt0(xp,W0) != xn
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f199,plain,
~ sdtlseqdt0(xp,xn),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f212,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f213,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f215,plain,
( xk != sz10
& xk != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f216,plain,
xk != sz00,
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f220,plain,
( isPrime0(xr)
& ! [W0] :
( W0 = xr
| W0 = sz10
| ( ~ doDivides0(W0,xr)
& ! [W1] :
( xr != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xr != sz10
& xr != sz00
& doDivides0(xr,xk)
& ? [W0] :
( xk = sdtasdt0(xr,W0)
& aNaturalNumber0(W0) )
& aNaturalNumber0(xr) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f221,plain,
( isPrime0(xr)
& ! [W0] :
( W0 = xr
| W0 = sz10
| ( ~ doDivides0(W0,xr)
& ! [W1] :
( xr != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xr != sz10
& xr != sz00
& doDivides0(xr,xk)
& xk = sdtasdt0(xr,sK8_skl)
& aNaturalNumber0(sK8_skl)
& aNaturalNumber0(xr) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W0,sK8_skl)],[f220]) ).
fof(f222,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f226,plain,
xr != sz00,
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f227,plain,
xr != sz10,
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f231,plain,
( doDivides0(xr,sdtasdt0(xn,xm))
& sdtasdt0(xn,xm) = sdtasdt0(xr,sK10_skl)
& aNaturalNumber0(sK10_skl)
& sdtpldt0(xr,sK9_skl) = xk
& aNaturalNumber0(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(W0,sK9_skl),skolemize(W0,sK10_skl)],[f49]) ).
fof(f234,plain,
aNaturalNumber0(sK10_skl),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f235,plain,
sdtasdt0(xn,xm) = sdtasdt0(xr,sK10_skl),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f252,plain,
( ( ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
& ! [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) != xn
| ~ aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ( sdtsldt0(xn,xr) = xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f253,definition,
( sP3_prd
<=> ( sdtsldt0(xn,xr) = xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f254,plain,
( ( ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
& ! [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) != xn
| ~ aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| sP3_prd ),
inference(formula_renaming,[status(thm)],[f252,f253]) ).
fof(f255,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f256,plain,
( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f258,plain,
( ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f285,plain,
( ( sdtsldt0(xn,xr) != xn
| xn != sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd )
& ( ( sdtsldt0(xn,xr) = xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f253]) ).
fof(f286,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f287,plain,
( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f288,plain,
( sdtsldt0(xn,xr) = xn
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f306,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(forward_subsumption_resolution,[status(thm)],[f286,f255]) ).
fof(f308,plain,
xn = sdtasdt0(xr,sdtsldt0(xn,xr)),
inference(forward_subsumption_resolution,[status(thm)],[f287,f256]) ).
fof(f311,plain,
( sdtasdt0(sdtsldt0(xn,xr),xr) = xn
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(paramodulation,[status(thm)],[f308,f73]) ).
fof(f313,plain,
( sdtasdt0(sdtsldt0(xn,xr),xr) = xn
| ~ aNaturalNumber0(xr) ),
inference(forward_subsumption_resolution,[status(thm)],[f311,f306]) ).
fof(f318,plain,
sdtasdt0(sdtsldt0(xn,xr),xr) = xn,
inference(forward_subsumption_resolution,[status(thm)],[f313,f222]) ).
fof(f340,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| xr = sz00
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f318,f131]) ).
fof(f345,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| xr = sz00
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(forward_subsumption_resolution,[status(thm)],[f340,f222]) ).
fof(f452,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| xr = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f345,f306]) ).
fof(f453,plain,
( sP3_prd
| xr = sz00 ),
inference(resolution,[status(thm)],[f452,f258]) ).
fof(f456,plain,
sP3_prd,
inference(forward_subsumption_resolution,[status(thm)],[f453,f226]) ).
fof(f458,plain,
sdtsldt0(xn,xr) = xn,
inference(backward_subsumption_resolution,[status(thm)],[f288,f456]) ).
fof(f462,plain,
sdtasdt0(xn,xr) = xn,
inference(backward_demodulation,[status(thm)],[f458,f318]) ).
fof(f463,plain,
xn = sdtasdt0(xr,xn),
inference(backward_demodulation,[status(thm)],[f458,f308]) ).
fof(f628,plain,
! [X0] :
( xr = X0
| xn != sdtasdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| xn = sz00
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f462,f89]) ).
fof(f645,plain,
! [X0] :
( xr = X0
| xn != sdtasdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| xn = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f173]) ).
fof(f858,plain,
( sdtlseqdt0(xp,sdtasdt0(xn,xm))
| xk = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xk) ),
inference(paramodulation,[status(thm)],[f213,f131]) ).
fof(f870,plain,
( sdtlseqdt0(xp,sdtasdt0(xn,xm))
| xk = sz00
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[status(thm)],[f858,f212]) ).
fof(f939,plain,
! [X0] :
( xr = X0
| xn != sdtasdt0(xn,X0)
| ~ aNaturalNumber0(X0)
| xn = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f645,f222]) ).
fof(f943,plain,
( ~ aNaturalNumber0(xn)
| xr = sz10
| ~ aNaturalNumber0(sz10)
| xn = sz00 ),
inference(resolution,[status(thm)],[f939,f77]) ).
fof(f947,plain,
( ~ aNaturalNumber0(xn)
| xr = sz10
| xn = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f943,f59]) ).
fof(f948,plain,
( ~ aNaturalNumber0(xn)
| xn = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f227]) ).
fof(f949,plain,
xn = sz00,
inference(resolution,[status(thm)],[f948,f173]) ).
fof(f953,plain,
sdtasdt0(sz00,xm) = sdtasdt0(xr,sK10_skl),
inference(backward_demodulation,[status(thm)],[f949,f235]) ).
fof(f972,plain,
xn = sdtasdt0(xr,sz00),
inference(backward_demodulation,[status(thm)],[f949,f463]) ).
fof(f978,plain,
~ sdtlseqdt0(xp,sz00),
inference(backward_demodulation,[status(thm)],[f949,f199]) ).
fof(f988,plain,
sz00 = sdtasdt0(xr,sz00),
inference(forward_demodulation,[status(thm)],[f949,f972]) ).
fof(f1002,plain,
( sK10_skl = sz00
| xr = sz00
| sdtasdt0(sz00,xm) != sz00
| ~ aNaturalNumber0(sK10_skl)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f953,f95]) ).
fof(f1015,plain,
( sK10_skl = sz00
| xr = sz00
| sdtasdt0(sz00,xm) != sz00
| ~ aNaturalNumber0(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1002,f222]) ).
fof(f1851,plain,
( sdtlseqdt0(xp,sdtasdt0(sz00,xm))
| xk = sz00
| ~ aNaturalNumber0(xp) ),
inference(forward_demodulation,[status(thm)],[f949,f870]) ).
fof(f1852,plain,
( sdtlseqdt0(xp,sdtasdt0(sz00,xm))
| xk = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f1851,f175]) ).
fof(f2045,plain,
( sK10_skl = sz00
| xr = sz00
| sdtasdt0(sz00,xm) != sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f1015,f234]) ).
fof(f2046,plain,
( ~ aNaturalNumber0(xm)
| sK10_skl = sz00
| xr = sz00 ),
inference(resolution,[status(thm)],[f2045,f81]) ).
fof(f2047,plain,
( ~ aNaturalNumber0(xm)
| sK10_skl = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f2046,f226]) ).
fof(f2050,plain,
sdtasdt0(sz00,xm) = sdtasdt0(xr,sz00),
inference(backward_demodulation,[status(thm)],[f2052,f953]) ).
fof(f2052,plain,
sK10_skl = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f2047,f174]) ).
fof(f2053,plain,
sdtasdt0(sz00,xm) = sz00,
inference(forward_demodulation,[status(thm)],[f988,f2050]) ).
fof(f2054,plain,
( sdtlseqdt0(xp,sz00)
| xk = sz00 ),
inference(backward_demodulation,[status(thm)],[f2053,f1852]) ).
fof(f2090,plain,
sdtlseqdt0(xp,sz00),
inference(forward_subsumption_resolution,[status(thm)],[f2054,f216]) ).
fof(f2151,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2090,f978]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM510+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/10.38 % Computer : n009.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Mon Sep 21 02:36:24 UTC 2026
% 0.11/10.38 % CPUTime :
% 0.14/10.40 % Drodi V4.1.1
% 0.14/10.80 % Refutation found
% 0.14/10.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/10.83 % Elapsed time: 0.428626 seconds
% 0.14/10.83 % CPU time: 3.121049 seconds
% 0.14/10.83 % Total memory used: 139.705 MB
% 0.14/10.83 % Net memory used: 136.211 MB
%------------------------------------------------------------------------------