%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM507+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 : n007.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:47 PM UTC 2026
% Result : Theorem 0.09s 0.44s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 13
% Syntax : Number of formulae : 78 ( 13 unt; 1 def)
% Number of atoms : 336 ( 90 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 440 ( 182 ~; 171 |; 72 &)
% ( 2 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 83 ( 72 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtpldt0(W1,W0) = sdtpldt0(W2,W0)
| sdtpldt0(W0,W1) = sdtpldt0(W0,W2) )
=> W1 = W2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
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(f24,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> ! [W2] :
( aNaturalNumber0(W2)
=> ( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W2,W0) != sdtpldt0(W2,W1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
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(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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( sdtlseqdt0(xk,xp)
& ? [W0] :
( sdtpldt0(xk,W0) = xp
& aNaturalNumber0(W0) )
& xk != xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,conjecture,
( ( sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| ? [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(xn,xm),xr),W0) = sdtpldt0(sdtpldt0(xn,xm),xp)
& aNaturalNumber0(W0) ) )
& sdtpldt0(sdtpldt0(xn,xm),xr) != sdtpldt0(sdtpldt0(xn,xm),xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
~ ( ( sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| ? [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(xn,xm),xr),W0) = sdtpldt0(sdtpldt0(xn,xm),xp)
& aNaturalNumber0(W0) ) )
& sdtpldt0(sdtpldt0(xn,xm),xr) != sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f59,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f83,plain,
! [W0,W1,W2] :
( W1 = W2
| ( sdtpldt0(W1,W0) != sdtpldt0(W2,W0)
& sdtpldt0(W0,W1) != sdtpldt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f94,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f95,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ( sdtpldt0(W0,sK0_skl(W1,W0)) = W1
& aNaturalNumber0(sK0_skl(W1,W0)) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f95]) ).
fof(f99,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f106,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f107,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f109,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
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] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f115,plain,
! [W0,W1] :
( ! [W2] :
( ( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W2,W0) != sdtpldt0(W2,W1) )
| ~ aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1)
| W0 = W1
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f117,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
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(f210,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f218,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(f219,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)],[f218]) ).
fof(f220,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f229,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(f230,plain,
aNaturalNumber0(sK9_skl),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
sdtpldt0(xr,sK9_skl) = xk,
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f235,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(f236,plain,
xk != xp,
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f239,plain,
sdtlseqdt0(xk,xp),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f240,plain,
( ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
& ! [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(xn,xm),xr),W0) != sdtpldt0(sdtpldt0(xn,xm),xp)
| ~ aNaturalNumber0(W0) ) )
| sdtpldt0(sdtpldt0(xn,xm),xr) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f242,plain,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xn,xm),xr) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f263,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f99]) ).
fof(f293,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f60]) ).
fof(f318,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xn,xm),xr) = sdtpldt0(sdtpldt0(xn,xm),xp)
| ~ sdtlseqdt0(X0,sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),X0)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xr)) ),
inference(resolution,[status(thm)],[f111,f242]) ).
fof(f370,plain,
( ~ aNaturalNumber0(sK9_skl)
| sdtlseqdt0(xr,xk)
| ~ aNaturalNumber0(xr) ),
inference(paramodulation,[status(thm)],[f231,f293]) ).
fof(f377,plain,
( ~ aNaturalNumber0(sK9_skl)
| sdtlseqdt0(xr,xk) ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f220]) ).
fof(f389,plain,
! [X0] :
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(X0,sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),X0)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xr)) ),
inference(resolution,[status(thm)],[f318,f84]) ).
fof(f391,plain,
! [X0] :
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(X0,sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),X0)
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f60]) ).
fof(f393,plain,
! [X0] :
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(X0,sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f391,f60]) ).
fof(f398,plain,
( ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xr))
| xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xr)) ),
inference(resolution,[status(thm)],[f393,f107]) ).
fof(f405,plain,
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| ~ aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xr)) ),
inference(duplicate_literals_removal,[status(thm)],[f398]) ).
fof(f406,plain,
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp)) ),
inference(forward_subsumption_resolution,[status(thm)],[f405,f60]) ).
fof(f411,plain,
sdtlseqdt0(xr,xk),
inference(forward_subsumption_resolution,[status(thm)],[f377,f230]) ).
fof(f413,plain,
( xk = xr
| ~ sdtlseqdt0(xk,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk) ),
inference(resolution,[status(thm)],[f411,f109]) ).
fof(f415,plain,
( xk = xr
| ~ sdtlseqdt0(xk,xr)
| ~ aNaturalNumber0(xr) ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f210]) ).
fof(f420,plain,
( xk = xr
| ~ sdtlseqdt0(xk,xr) ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f220]) ).
fof(f535,plain,
( xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp)) ),
inference(forward_subsumption_resolution,[status(thm)],[f406,f220]) ).
fof(f536,plain,
( ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(xr,xp)
| xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(resolution,[status(thm)],[f535,f117]) ).
fof(f539,plain,
( ~ sdtlseqdt0(xr,xp)
| ~ aNaturalNumber0(xr)
| xr = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(duplicate_literals_removal,[status(thm)],[f536]) ).
fof(f540,plain,
( ~ sdtlseqdt0(xr,xp)
| ~ aNaturalNumber0(xr)
| xr = xp
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f173]) ).
fof(f543,plain,
( ~ sdtlseqdt0(xr,xp)
| xr = xp
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f540,f220]) ).
fof(f544,plain,
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn)
| ~ sdtlseqdt0(xr,xp)
| xr = xp ),
inference(resolution,[status(thm)],[f543,f60]) ).
fof(f545,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(xr,xp)
| xr = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f544,f171]) ).
fof(f546,plain,
( ~ sdtlseqdt0(xr,xp)
| xr = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f172]) ).
fof(f547,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(xr,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| xr = xp ),
inference(resolution,[status(thm)],[f546,f111]) ).
fof(f549,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(xr,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| xr = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f547,f220]) ).
fof(f723,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(xr,X0)
| ~ aNaturalNumber0(X0)
| xr = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f549,f173]) ).
fof(f724,plain,
( ~ sdtlseqdt0(xk,xp)
| ~ aNaturalNumber0(xk)
| xr = xp ),
inference(resolution,[status(thm)],[f723,f411]) ).
fof(f730,plain,
( ~ sdtlseqdt0(xk,xp)
| xr = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f210]) ).
fof(f746,plain,
( xk = xp
| ~ sdtlseqdt0(xk,xr) ),
inference(backward_demodulation,[status(thm)],[f763,f420]) ).
fof(f763,plain,
xr = xp,
inference(forward_subsumption_resolution,[status(thm)],[f730,f239]) ).
fof(f764,plain,
( xk = xp
| ~ sdtlseqdt0(xk,xp) ),
inference(forward_demodulation,[status(thm)],[f763,f746]) ).
fof(f765,plain,
xk = xp,
inference(forward_subsumption_resolution,[status(thm)],[f764,f239]) ).
fof(f794,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f765,f236]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM507+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:33:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.44 % Refutation found
% 0.09/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.46 % Elapsed time: 0.095865 seconds
% 0.09/0.46 % CPU time: 0.448734 seconds
% 0.09/0.46 % Total memory used: 112.665 MB
% 0.09/0.46 % Net memory used: 111.866 MB
%------------------------------------------------------------------------------