%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM518+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 : n001.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:49 PM UTC 2026
% Result : Theorem 35.26s 5.01s
% Output : CNFRefutation 11.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 53
% Syntax : Number of formulae : 214 ( 54 unt; 35 def)
% Number of atoms : 618 ( 140 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 632 ( 228 ~; 201 |; 158 &)
% ( 36 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 35 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 19 con; 0-2 aty)
% Number of variables : 94 ( 67 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(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(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/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,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(f50,hypothesis,
( sdtlseqdt0(xk,xp)
& ? [W0] :
( sdtpldt0(xk,W0) = xp
& aNaturalNumber0(W0) )
& xk != xp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
( doDivides0(xr,xn)
& ? [W0] :
( xn = sdtasdt0(xr,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
& ? [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) = xn
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr))
& ~ ( ( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
=> sdtsldt0(xn,xr) = xn ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
( doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))
& ? [W0] :
( sdtasdt0(sdtsldt0(xn,xr),xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
( ( doDivides0(xp,xm)
& ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) )
| ( doDivides0(xp,sdtsldt0(xn,xr))
& ? [W0] :
( sdtsldt0(xn,xr) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
( 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(f57,negated_conjecture,
~ ( 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)],[f56]) ).
fof(f62,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f63,plain,
sz10 != sz00,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f66,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f75,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f76,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f79,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f80,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f139,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(f140,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)],[f139]) ).
fof(f141,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))],[f140]) ).
fof(f144,plain,
! [X0,X1,X2] :
( X1 != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f151,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(f152,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f176,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f177,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f178,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f190,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(f191,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)],[f190]) ).
fof(f197,plain,
aNaturalNumber0(sK5_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f206,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(f207,plain,
xn != xp,
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f208,plain,
aNaturalNumber0(sK6_skl),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f211,plain,
xm != xp,
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f212,plain,
aNaturalNumber0(sK7_skl),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f215,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f218,plain,
( xk != sz10
& xk != sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f219,plain,
xk != sz00,
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
xk != sz10,
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f223,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(f224,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)],[f223]) ).
fof(f225,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
aNaturalNumber0(sK8_skl),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f229,plain,
xr != sz00,
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f234,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(f235,plain,
aNaturalNumber0(sK9_skl),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f237,plain,
aNaturalNumber0(sK10_skl),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f240,plain,
( sdtlseqdt0(xk,xp)
& sdtpldt0(xk,sK11_skl) = xp
& aNaturalNumber0(sK11_skl)
& xk != xp ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(W0,sK11_skl)],[f50]) ).
fof(f241,plain,
xk != xp,
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
aNaturalNumber0(sK11_skl),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f251,plain,
( doDivides0(xr,xn)
& xn = sdtasdt0(xr,sK13_skl)
& aNaturalNumber0(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(W0,sK13_skl)],[f52]) ).
fof(f252,plain,
aNaturalNumber0(sK13_skl),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f254,plain,
doDivides0(xr,xn),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f255,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)],[f53]) ).
fof(f256,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
& sdtpldt0(sdtsldt0(xn,xr),sK14_skl) = xn
& aNaturalNumber0(sK14_skl)
& 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(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(W0,sK14_skl)],[f255]) ).
fof(f258,plain,
xn = sdtasdt0(xr,sdtsldt0(xn,xr)),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f259,plain,
sdtsldt0(xn,xr) != xn,
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f262,plain,
aNaturalNumber0(sK14_skl),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f265,plain,
( doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))
& sdtasdt0(sdtsldt0(xn,xr),xm) = sdtasdt0(xp,sK15_skl)
& aNaturalNumber0(sK15_skl)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(W0,sK15_skl)],[f54]) ).
fof(f268,plain,
aNaturalNumber0(sK15_skl),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f271,definition,
( sP3_prd
<=> ( doDivides0(xp,sdtsldt0(xn,xr))
& ? [W0] :
( sdtsldt0(xn,xr) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f272,plain,
( ( doDivides0(xp,xm)
& ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) )
| sP3_prd ),
inference(formula_renaming,[status(thm)],[f55,f271]) ).
fof(f273,plain,
( ( doDivides0(xp,xm)
& xm = sdtasdt0(xp,sK16_skl)
& aNaturalNumber0(sK16_skl) )
| sP3_prd ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(W0,sK16_skl)],[f272]) ).
fof(f276,plain,
( doDivides0(xp,xm)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f277,plain,
( ~ doDivides0(xp,xm)
& ! [W0] :
( xm != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
& ~ doDivides0(xp,xn)
& ! [W0] :
( xn != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f279,plain,
~ doDivides0(xp,xn),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f281,plain,
~ doDivides0(xp,xm),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f308,plain,
( ( ~ doDivides0(xp,sdtsldt0(xn,xr))
| ! [W0] :
( sdtsldt0(xn,xr) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
| xn != sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd )
& ( ( doDivides0(xp,sdtsldt0(xn,xr))
& ? [W0] :
( sdtsldt0(xn,xr) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f271]) ).
fof(f309,plain,
( ( ~ doDivides0(xp,sdtsldt0(xn,xr))
| ! [W0] :
( sdtsldt0(xn,xr) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) )
| xn != sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd )
& ( ( doDivides0(xp,sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) = sdtasdt0(xp,sK21_skl)
& aNaturalNumber0(sK21_skl)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W0,sK21_skl)],[f308]) ).
fof(f310,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f314,plain,
( doDivides0(xp,sdtsldt0(xn,xr))
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f331,definition,
( sQ4_spl
<=> sP3_prd ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f342,definition,
( sQ7_spl
<=> doDivides0(xp,xm) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f345,plain,
( sQ7_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f276,f331,f342]) ).
fof(f362,definition,
( sQ12_spl
<=> aNaturalNumber0(sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ12_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f310,f331,f362]) ).
fof(f378,definition,
( sQ16_spl
<=> doDivides0(xp,sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( ~ sQ16_spl
| doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f381,plain,
( sQ16_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f314,f331,f378]) ).
fof(f389,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| doDivides0(X0,sdtasdt0(X1,X0))
| ~ aNaturalNumber0(sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f144,f76]) ).
fof(f395,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| doDivides0(X0,sdtasdt0(X1,X0))
| ~ aNaturalNumber0(sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f389]) ).
fof(f396,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| doDivides0(X0,sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f67]) ).
fof(f405,plain,
! [X0] :
( ~ doDivides0(X0,xm)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f152,f281]) ).
fof(f406,plain,
! [X0] :
( ~ doDivides0(X0,xn)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f152,f279]) ).
fof(f409,definition,
( sQ18_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( sQ18_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f412,definition,
! [X0] :
( sQ19_spl
<=> ( ~ doDivides0(X0,xm)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f413,plain,
! [X0] :
( ~ sQ19_spl
| ~ doDivides0(X0,xm)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ20_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ20_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,plain,
( ~ sQ20_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f405,f409,f412,f415]) ).
fof(f419,definition,
! [X0] :
( sQ21_spl
<=> ( ~ doDivides0(X0,xn)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f420,plain,
! [X0] :
( ~ sQ21_spl
| ~ doDivides0(X0,xn)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f419]) ).
fof(f422,definition,
( sQ22_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( sQ22_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,plain,
( ~ sQ22_spl
| sQ21_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f406,f409,f419,f422]) ).
fof(f427,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f178]) ).
fof(f428,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f427]) ).
fof(f439,plain,
! [X0] :
( ~ aNaturalNumber0(sz10)
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f80,f144]) ).
fof(f441,definition,
! [X0] :
( sQ23_spl
<=> ( doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f442,plain,
! [X0] :
( ~ sQ23_spl
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f444,definition,
( sQ24_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( sQ24_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f447,plain,
( ~ sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f439,f441,f444]) ).
fof(f448,plain,
! [X0] :
( ~ sQ23_spl
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f442]) ).
fof(f456,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f62]) ).
fof(f457,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f456]) ).
fof(f487,definition,
( sQ31_spl
<=> aNaturalNumber0(xr) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( sQ31_spl
| ~ aNaturalNumber0(xr) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f491,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f424,f176]) ).
fof(f492,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f491]) ).
fof(f531,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f417,f177]) ).
fof(f532,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f531]) ).
fof(f593,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f225]) ).
fof(f594,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f593]) ).
fof(f671,plain,
( ~ sQ23_spl
| ~ sQ19_spl
| ~ aNaturalNumber0(xp)
| ~ doDivides0(xp,xm)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f413,f448]) ).
fof(f675,plain,
( ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ7_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f671,f409,f342,f412,f441]) ).
fof(f726,definition,
( sQ60_spl
<=> xp = xm ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( ~ sQ60_spl
| xp = xm ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f859,definition,
( sQ78_spl
<=> xp = xn ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( ~ sQ78_spl
| xp = xn ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f1256,definition,
( sQ134_spl
<=> aNaturalNumber0(xk) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
( sQ134_spl
| ~ aNaturalNumber0(xk) ),
inference(component_clause,[status(thm)],[f1256]) ).
fof(f1268,plain,
( sQ134_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1258,f215]) ).
fof(f1269,plain,
sQ134_spl,
inference(contradiction_clause,[status(thm)],[f1268]) ).
fof(f1416,definition,
( sQ160_spl
<=> xp = xk ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1417,plain,
( ~ sQ160_spl
| xp = xk ),
inference(component_clause,[status(thm)],[f1416]) ).
fof(f1658,definition,
( sQ193_spl
<=> aNaturalNumber0(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1660,plain,
( sQ193_spl
| ~ aNaturalNumber0(sK6_skl) ),
inference(component_clause,[status(thm)],[f1658]) ).
fof(f1730,plain,
( sQ193_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1660,f208]) ).
fof(f1731,plain,
sQ193_spl,
inference(contradiction_clause,[status(thm)],[f1730]) ).
fof(f1750,definition,
( sQ211_spl
<=> aNaturalNumber0(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f1752,plain,
( sQ211_spl
| ~ aNaturalNumber0(sK7_skl) ),
inference(component_clause,[status(thm)],[f1750]) ).
fof(f1819,plain,
( sQ211_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1752,f212]) ).
fof(f1820,plain,
sQ211_spl,
inference(contradiction_clause,[status(thm)],[f1819]) ).
fof(f2062,definition,
( sQ260_spl
<=> aNaturalNumber0(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f2064,plain,
( sQ260_spl
| ~ aNaturalNumber0(sK8_skl) ),
inference(component_clause,[status(thm)],[f2062]) ).
fof(f2105,definition,
( sQ272_spl
<=> xr = sz00 ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f2106,plain,
( ~ sQ272_spl
| xr = sz00 ),
inference(component_clause,[status(thm)],[f2105]) ).
fof(f2146,definition,
( sQ282_spl
<=> xk = sz00 ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f2147,plain,
( ~ sQ282_spl
| xk = sz00 ),
inference(component_clause,[status(thm)],[f2146]) ).
fof(f2160,plain,
( sQ260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2064,f226]) ).
fof(f2161,plain,
sQ260_spl,
inference(contradiction_clause,[status(thm)],[f2160]) ).
fof(f2162,plain,
( ~ sQ272_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2106,f229]) ).
fof(f2163,plain,
~ sQ272_spl,
inference(contradiction_clause,[status(thm)],[f2162]) ).
fof(f2264,plain,
( ~ sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2147,f219]) ).
fof(f2265,plain,
~ sQ282_spl,
inference(contradiction_clause,[status(thm)],[f2264]) ).
fof(f2335,definition,
( sQ307_spl
<=> xk = sz10 ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f2336,plain,
( ~ sQ307_spl
| xk = sz10 ),
inference(component_clause,[status(thm)],[f2335]) ).
fof(f2609,definition,
( sQ339_spl
<=> sz00 = sz10 ),
introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition]) ).
fof(f2610,plain,
( ~ sQ339_spl
| sz00 = sz10 ),
inference(component_clause,[status(thm)],[f2609]) ).
fof(f2643,plain,
( ~ sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2336,f220]) ).
fof(f2644,plain,
~ sQ307_spl,
inference(contradiction_clause,[status(thm)],[f2643]) ).
fof(f2673,plain,
( ~ sQ339_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2610,f63]) ).
fof(f2674,plain,
~ sQ339_spl,
inference(contradiction_clause,[status(thm)],[f2673]) ).
fof(f3196,definition,
( sQ413_spl
<=> aNaturalNumber0(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition]) ).
fof(f3198,plain,
( sQ413_spl
| ~ aNaturalNumber0(sK5_skl) ),
inference(component_clause,[status(thm)],[f3196]) ).
fof(f3324,plain,
( sQ413_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3198,f197]) ).
fof(f3325,plain,
sQ413_spl,
inference(contradiction_clause,[status(thm)],[f3324]) ).
fof(f3609,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f860,f207]) ).
fof(f3610,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f3609]) ).
fof(f3783,definition,
( sQ502_spl
<=> aNaturalNumber0(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f3785,plain,
( sQ502_spl
| ~ aNaturalNumber0(sK9_skl) ),
inference(component_clause,[status(thm)],[f3783]) ).
fof(f3875,plain,
( sQ502_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3785,f235]) ).
fof(f3876,plain,
sQ502_spl,
inference(contradiction_clause,[status(thm)],[f3875]) ).
fof(f3909,definition,
( sQ526_spl
<=> aNaturalNumber0(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition]) ).
fof(f3911,plain,
( sQ526_spl
| ~ aNaturalNumber0(sK10_skl) ),
inference(component_clause,[status(thm)],[f3909]) ).
fof(f3924,definition,
( sQ530_spl
<=> xr = xp ),
introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition]) ).
fof(f3925,plain,
( ~ sQ530_spl
| xr = xp ),
inference(component_clause,[status(thm)],[f3924]) ).
fof(f4025,plain,
( sQ526_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3911,f237]) ).
fof(f4026,plain,
sQ526_spl,
inference(contradiction_clause,[status(thm)],[f4025]) ).
fof(f4062,definition,
( sQ555_spl
<=> aNaturalNumber0(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition]) ).
fof(f4064,plain,
( sQ555_spl
| ~ aNaturalNumber0(sK11_skl) ),
inference(component_clause,[status(thm)],[f4062]) ).
fof(f4154,plain,
( sQ555_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4064,f242]) ).
fof(f4155,plain,
sQ555_spl,
inference(contradiction_clause,[status(thm)],[f4154]) ).
fof(f4358,definition,
( sQ603_spl
<=> aNaturalNumber0(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition]) ).
fof(f4360,plain,
( sQ603_spl
| ~ aNaturalNumber0(sK13_skl) ),
inference(component_clause,[status(thm)],[f4358]) ).
fof(f4464,plain,
( sQ603_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4360,f252]) ).
fof(f4465,plain,
sQ603_spl,
inference(contradiction_clause,[status(thm)],[f4464]) ).
fof(f4494,plain,
( ~ aNaturalNumber0(xr)
| doDivides0(sdtsldt0(xn,xr),xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(paramodulation,[status(thm)],[f258,f396]) ).
fof(f4567,definition,
( sQ644_spl
<=> doDivides0(sdtsldt0(xn,xr),xn) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f4570,plain,
( ~ sQ31_spl
| sQ644_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f4494,f362,f4567,f487]) ).
fof(f4616,plain,
( ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f241]) ).
fof(f4617,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f4616]) ).
fof(f4618,plain,
( ~ sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f727,f211]) ).
fof(f4619,plain,
~ sQ60_spl,
inference(contradiction_clause,[status(thm)],[f4618]) ).
fof(f4648,plain,
( ~ sQ530_spl
| doDivides0(xp,xn) ),
inference(backward_demodulation,[status(thm)],[f3925,f254]) ).
fof(f4657,plain,
( ~ sQ530_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4648,f279]) ).
fof(f4658,plain,
~ sQ530_spl,
inference(contradiction_clause,[status(thm)],[f4657]) ).
fof(f4772,definition,
( sQ655_spl
<=> aNaturalNumber0(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition]) ).
fof(f4774,plain,
( sQ655_spl
| ~ aNaturalNumber0(sK14_skl) ),
inference(component_clause,[status(thm)],[f4772]) ).
fof(f4840,plain,
( sQ655_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4774,f262]) ).
fof(f4841,plain,
sQ655_spl,
inference(contradiction_clause,[status(thm)],[f4840]) ).
fof(f4851,definition,
( sQ674_spl
<=> xn = sdtsldt0(xn,xr) ),
introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition]) ).
fof(f4852,plain,
( ~ sQ674_spl
| xn = sdtsldt0(xn,xr) ),
inference(component_clause,[status(thm)],[f4851]) ).
fof(f4855,plain,
( ~ sQ674_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4852,f259]) ).
fof(f4856,plain,
~ sQ674_spl,
inference(contradiction_clause,[status(thm)],[f4855]) ).
fof(f4971,definition,
( sQ681_spl
<=> aNaturalNumber0(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition]) ).
fof(f4973,plain,
( sQ681_spl
| ~ aNaturalNumber0(sK15_skl) ),
inference(component_clause,[status(thm)],[f4971]) ).
fof(f5111,plain,
( sQ681_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4973,f268]) ).
fof(f5112,plain,
sQ681_spl,
inference(contradiction_clause,[status(thm)],[f5111]) ).
fof(f9449,plain,
( ~ sQ16_spl
| ~ sQ21_spl
| ~ doDivides0(sdtsldt0(xn,xr),xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolution,[status(thm)],[f420,f379]) ).
fof(f9469,plain,
( ~ sQ16_spl
| ~ sQ21_spl
| ~ sQ644_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f9449,f362,f4567,f419,f378]) ).
fof(f9489,plain,
$false,
inference(sat_refutation,[status(thm)],[f345,f365,f381,f418,f425,f428,f447,f457,f492,f532,f594,f675,f1269,f1731,f1820,f2161,f2163,f2265,f2644,f2674,f3325,f3610,f3876,f4026,f4155,f4465,f4570,f4617,f4619,f4658,f4841,f4856,f5112,f9469]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM518+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n001.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 02:42:13 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 35.26/5.01 % Refutation found
% 35.26/5.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 35.26/5.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.63/5.07 % Elapsed time: 4.622068 seconds
% 11.63/5.07 % CPU time: 36.121171 seconds
% 11.63/5.07 % Total memory used: 218.494 MB
% 11.63/5.07 % Net memory used: 206.321 MB
%------------------------------------------------------------------------------