%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM459+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:36 PM UTC 2026
% Result : Theorem 12.00s 6.98s
% Output : CNFRefutation 12.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 11
% Syntax : Number of formulae : 132 ( 21 unt; 2 def)
% Number of atoms : 482 ( 135 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 640 ( 290 ~; 284 |; 49 &)
% ( 4 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 156 ( 147 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
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(f16,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtpldt0(W0,W1) = sz00
=> ( W1 = sz00
& W0 = sz00 ) ) ),
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(f19,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
=> ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,conjecture,
( ( sdtlseqdt0(xn,xm)
& ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) )
& sdtlseqdt0(xm,xn)
& ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
=> xm = xn ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ ( ( sdtlseqdt0(xn,xm)
& ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) )
& sdtlseqdt0(xm,xn)
& ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
=> xm = xn ),
inference(negated_conjecture,[status(cth)],[f22]) ).
fof(f27,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f34,plain,
! [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f35,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [W0,W1,W2] :
( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2))
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f37,plain,
! [X0,X1,X2] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f39,plain,
! [X0] :
( sdtpldt0(X0,sz00) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f54,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(f55,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f60,plain,
! [W0,W1] :
( ( W1 = sz00
& W0 = sz00 )
| sdtpldt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f61,plain,
! [X0,X1] :
( X0 = sz00
| sdtpldt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f65,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(f66,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)],[f65]) ).
fof(f67,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))],[f66]) ).
fof(f68,plain,
! [X0,X1] :
( aNaturalNumber0(sK0_skl(X1,X0))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( sdtpldt0(X0,sK0_skl(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f71,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f72,plain,
! [W0,W1] :
( ! [W2] :
( ( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2)
| W2 = sdtmndt0(W1,W0) )
& ( ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| W2 != sdtmndt0(W1,W0) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [W0,W1] :
( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2)
| W2 = sdtmndt0(W1,W0) )
& ! [W2] :
( ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| W2 != sdtmndt0(W1,W0) ) )
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( aNaturalNumber0(X2)
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) = X1
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f76,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f79,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f80,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f81,plain,
( xm != xn
& sdtlseqdt0(xn,xm)
& ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) )
& sdtlseqdt0(xm,xn)
& ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f82,plain,
( xm != xn
& sdtlseqdt0(xn,xm)
& sdtpldt0(xn,sK2_skl) = xm
& aNaturalNumber0(sK2_skl)
& sdtlseqdt0(xm,xn)
& sdtpldt0(xm,sK1_skl) = xn
& aNaturalNumber0(sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(W0,sK1_skl),skolemize(W0,sK2_skl)],[f81]) ).
fof(f83,plain,
aNaturalNumber0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
sdtpldt0(xm,sK1_skl) = xn,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f86,plain,
aNaturalNumber0(sK2_skl),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f87,plain,
sdtpldt0(xn,sK2_skl) = xm,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f88,plain,
sdtlseqdt0(xn,xm),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f89,plain,
xm != xn,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f93,plain,
( xn = sdtpldt0(sK1_skl,xm)
| ~ aNaturalNumber0(sK1_skl)
| ~ aNaturalNumber0(xm) ),
inference(paramodulation,[status(thm)],[f84,f35]) ).
fof(f97,plain,
( xn = sdtpldt0(sK1_skl,xm)
| ~ aNaturalNumber0(sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f93,f79]) ).
fof(f102,plain,
xn = sdtpldt0(sK1_skl,xm),
inference(forward_subsumption_resolution,[status(thm)],[f97,f83]) ).
fof(f106,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X1,X0))
| ~ aNaturalNumber0(sdtpldt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f70,f35]) ).
fof(f114,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(equality_resolution,[status(thm)],[f70]) ).
fof(f115,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X1,X0))
| ~ aNaturalNumber0(sdtpldt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f106]) ).
fof(f116,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X1,X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f115,f31]) ).
fof(f125,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f114,f31]) ).
fof(f129,plain,
( ~ aNaturalNumber0(xm)
| sdtlseqdt0(sK1_skl,xn)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f84,f116]) ).
fof(f131,plain,
( ~ aNaturalNumber0(xm)
| sdtlseqdt0(sK1_skl,xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f129,f83]) ).
fof(f135,plain,
! [X0] :
( sdtpldt0(xn,X0) = sdtpldt0(sK1_skl,sdtpldt0(xm,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f102,f37]) ).
fof(f137,plain,
! [X0] :
( sdtpldt0(xm,X0) = sdtpldt0(xn,sdtpldt0(sK2_skl,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f87,f37]) ).
fof(f147,plain,
! [X0] :
( sdtpldt0(xn,X0) = sdtpldt0(sK1_skl,sdtpldt0(xm,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f83]) ).
fof(f149,plain,
! [X0] :
( sdtpldt0(xm,X0) = sdtpldt0(xn,sdtpldt0(sK2_skl,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK2_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f80]) ).
fof(f157,plain,
! [X0] :
( xm = X0
| xn != sdtpldt0(sK1_skl,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f102,f55]) ).
fof(f166,plain,
! [X0] :
( xm = X0
| xn != sdtpldt0(sK1_skl,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f157,f83]) ).
fof(f174,plain,
sdtlseqdt0(sK1_skl,xn),
inference(forward_subsumption_resolution,[status(thm)],[f131,f79]) ).
fof(f213,plain,
! [X0] :
( xm = X0
| xn != sdtpldt0(sK1_skl,X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f166,f79]) ).
fof(f218,plain,
! [X0] :
( sdtpldt0(xm,X0) = sdtpldt0(xn,sdtpldt0(sK2_skl,X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f149,f86]) ).
fof(f336,plain,
! [X0] :
( ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| X0 = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f61,f69]) ).
fof(f343,plain,
! [X0] :
( ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| X0 = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f336]) ).
fof(f344,plain,
! [X0] :
( ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f343,f68]) ).
fof(f366,plain,
! [X0] :
( ~ sdtlseqdt0(X0,sz00)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f27]) ).
fof(f388,plain,
! [X0,X1] :
( ~ aNaturalNumber0(sdtmndt0(X1,X0))
| aNaturalNumber0(sdtpldt0(sdtmndt0(X1,X0),sz00))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f74,f39]) ).
fof(f392,plain,
! [X0,X1] :
( aNaturalNumber0(sdtmndt0(X1,X0))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(equality_resolution,[status(thm)],[f74]) ).
fof(f408,plain,
! [X0,X1] :
( ~ aNaturalNumber0(sdtmndt0(X1,X0))
| sdtpldt0(X0,sdtpldt0(sdtmndt0(X1,X0),sz00)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f75,f39]) ).
fof(f412,plain,
! [X0,X1] :
( sdtpldt0(X0,sdtmndt0(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(equality_resolution,[status(thm)],[f75]) ).
fof(f435,plain,
! [X0] :
( sdtpldt0(xn,X0) = sdtpldt0(sK1_skl,sdtpldt0(xm,X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f147,f79]) ).
fof(f803,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(X0,X1),X0))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f412,f55]) ).
fof(f818,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(X0,X1),X0))
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f803]) ).
fof(f819,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(X0,X1),X0))
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f818,f31]) ).
fof(f830,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| X2 = sdtmndt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f76,f70]) ).
fof(f833,plain,
! [X0,X1,X2,X3] :
( ~ aNaturalNumber0(X3)
| sdtlseqdt0(X2,sdtmndt0(X1,X0))
| ~ aNaturalNumber0(sdtmndt0(X1,X0))
| ~ aNaturalNumber0(X2)
| sdtpldt0(X0,sdtpldt0(X2,X3)) != X1
| ~ aNaturalNumber0(sdtpldt0(X2,X3))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f830,f70]) ).
fof(f838,plain,
! [X0,X1,X2,X3] :
( ~ aNaturalNumber0(X3)
| sdtlseqdt0(X2,sdtmndt0(X1,X0))
| ~ aNaturalNumber0(sdtmndt0(X1,X0))
| ~ aNaturalNumber0(X2)
| sdtpldt0(X0,sdtpldt0(X2,X3)) != X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f833,f31]) ).
fof(f1523,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(sdtmndt0(X1,X0),sz00))
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f392]) ).
fof(f1595,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(sK2_skl,sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(sdtpldt0(xm,X0))
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f838,f218]) ).
fof(f1637,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sK2_skl,sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(sdtpldt0(xm,X0))
| ~ aNaturalNumber0(xn) ),
inference(duplicate_literals_removal,[status(thm)],[f1595]) ).
fof(f1638,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sK2_skl,sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(sdtpldt0(xm,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1637,f80]) ).
fof(f1951,plain,
! [X0,X1] :
( sdtpldt0(X0,sdtpldt0(sdtmndt0(X1,X0),sz00)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f392]) ).
fof(f2831,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(X0,X1),X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f819,f125]) ).
fof(f2832,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f2831,f392]) ).
fof(f2849,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2832]) ).
fof(f2850,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,sdtpldt0(X0,X1))
| sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2849,f31]) ).
fof(f2891,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X0,X1),X0) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2850,f125]) ).
fof(f2911,plain,
( sdtmndt0(xn,sK1_skl) = xm
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f102,f2891]) ).
fof(f2917,plain,
( sdtmndt0(xm,xn) = sK2_skl
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f87,f2891]) ).
fof(f2931,plain,
( sdtmndt0(xn,sK1_skl) = xm
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f2911,f83]) ).
fof(f2937,plain,
( sdtmndt0(xm,xn) = sK2_skl
| ~ aNaturalNumber0(sK2_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2917,f80]) ).
fof(f2943,plain,
sdtmndt0(xn,sK1_skl) = xm,
inference(forward_subsumption_resolution,[status(thm)],[f2931,f79]) ).
fof(f2950,plain,
( sdtpldt0(sK1_skl,sdtpldt0(xm,sz00)) = xn
| ~ sdtlseqdt0(sK1_skl,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f2943,f1951]) ).
fof(f2957,plain,
( aNaturalNumber0(sdtpldt0(xm,sz00))
| ~ sdtlseqdt0(sK1_skl,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f2943,f1523]) ).
fof(f2969,plain,
( sdtpldt0(sK1_skl,sdtpldt0(xm,sz00)) = xn
| ~ sdtlseqdt0(sK1_skl,xn)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f2950,f83]) ).
fof(f2977,plain,
( aNaturalNumber0(sdtpldt0(xm,sz00))
| ~ sdtlseqdt0(sK1_skl,xn)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f2957,f83]) ).
fof(f3023,plain,
sdtmndt0(xm,xn) = sK2_skl,
inference(forward_subsumption_resolution,[status(thm)],[f2937,f86]) ).
fof(f3042,plain,
! [X0] :
( sdtpldt0(xn,X0) = xm
| X0 != sK2_skl
| ~ sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f3023,f75]) ).
fof(f3059,plain,
! [X0] :
( sdtpldt0(xn,X0) = xm
| X0 != sK2_skl
| ~ sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f3042,f80]) ).
fof(f3451,plain,
( aNaturalNumber0(sdtpldt0(xm,sz00))
| ~ sdtlseqdt0(sK1_skl,xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f2977,f80]) ).
fof(f3550,plain,
! [X0] :
( sdtpldt0(xn,X0) = xm
| X0 != sK2_skl
| ~ sdtlseqdt0(xn,xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f3059,f79]) ).
fof(f5177,plain,
( sdtpldt0(sK1_skl,sdtpldt0(xm,sz00)) = xn
| ~ sdtlseqdt0(sK1_skl,xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f2969,f80]) ).
fof(f5180,plain,
( xm = sdtpldt0(xm,sz00)
| ~ aNaturalNumber0(sdtpldt0(xm,sz00))
| ~ sdtlseqdt0(sK1_skl,xn) ),
inference(resolution,[status(thm)],[f5177,f213]) ).
fof(f5184,plain,
( xm = sdtpldt0(xm,sz00)
| ~ aNaturalNumber0(sdtpldt0(xm,sz00)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5180,f174]) ).
fof(f5185,plain,
( ~ sdtlseqdt0(sK1_skl,xn)
| xm = sdtpldt0(xm,sz00) ),
inference(resolution,[status(thm)],[f5184,f3451]) ).
fof(f5191,plain,
xm = sdtpldt0(xm,sz00),
inference(forward_subsumption_resolution,[status(thm)],[f5185,f174]) ).
fof(f5207,plain,
( sdtpldt0(xn,sz00) = sdtpldt0(sK1_skl,xm)
| ~ aNaturalNumber0(sz00) ),
inference(paramodulation,[status(thm)],[f5191,f435]) ).
fof(f5263,plain,
( sdtpldt0(xn,sz00) = xn
| ~ aNaturalNumber0(sz00) ),
inference(forward_demodulation,[status(thm)],[f102,f5207]) ).
fof(f5264,plain,
sdtpldt0(xn,sz00) = xn,
inference(forward_subsumption_resolution,[status(thm)],[f5263,f27]) ).
fof(f5740,plain,
( xn = xm
| sz00 != sK2_skl
| ~ sdtlseqdt0(xn,xm) ),
inference(paramodulation,[status(thm)],[f5264,f3550]) ).
fof(f5764,plain,
( sdtmndt0(xn,xn) = sz00
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f5264,f2891]) ).
fof(f5800,plain,
( xn = xm
| sz00 != sK2_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f5740,f88]) ).
fof(f5848,plain,
( sdtmndt0(xn,xn) = sz00
| ~ aNaturalNumber0(sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[f5764,f80]) ).
fof(f5878,plain,
sdtmndt0(xn,xn) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f5848,f27]) ).
fof(f6200,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sK2_skl,sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,X0),xn))
| ~ aNaturalNumber0(sdtpldt0(xm,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1638,f86]) ).
fof(f6205,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sdtmndt0(xn,xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,sK1_skl),xn))
| ~ aNaturalNumber0(sdtpldt0(xm,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f84,f6200]) ).
fof(f6217,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sdtmndt0(xn,xn))
| ~ aNaturalNumber0(sdtmndt0(sdtpldt0(xm,sK1_skl),xn))
| ~ aNaturalNumber0(xn) ),
inference(forward_demodulation,[status(thm)],[f84,f6205]) ).
fof(f6218,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sdtmndt0(xn,xn))
| ~ aNaturalNumber0(sdtmndt0(xn,xn))
| ~ aNaturalNumber0(xn) ),
inference(forward_demodulation,[status(thm)],[f84,f6217]) ).
fof(f6219,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sdtmndt0(xn,xn))
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xn) ),
inference(forward_demodulation,[status(thm)],[f5878,f6218]) ).
fof(f6220,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xn) ),
inference(forward_demodulation,[status(thm)],[f5878,f6219]) ).
fof(f6221,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sz00)
| ~ aNaturalNumber0(sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[f6220,f80]) ).
fof(f6261,plain,
sz00 != sK2_skl,
inference(forward_subsumption_resolution,[status(thm)],[f5800,f89]) ).
fof(f6730,plain,
( ~ aNaturalNumber0(sK1_skl)
| sdtlseqdt0(sK2_skl,sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[f6221,f27]) ).
fof(f6731,plain,
( sK2_skl = sz00
| ~ aNaturalNumber0(sK2_skl)
| ~ aNaturalNumber0(sK1_skl) ),
inference(resolution,[status(thm)],[f6730,f366]) ).
fof(f6732,plain,
( sK2_skl = sz00
| ~ aNaturalNumber0(sK2_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6731,f83]) ).
fof(f6745,plain,
sK2_skl != sK2_skl,
inference(backward_demodulation,[status(thm)],[f6811,f6261]) ).
fof(f6811,plain,
sK2_skl = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f6732,f86]) ).
fof(f6817,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f6745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM459+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n010.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 02:32:17 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 12.00/6.98 % Refutation found
% 12.00/6.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.00/6.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.00/7.03 % Elapsed time: 1.641348 seconds
% 12.00/7.03 % CPU time: 12.803786 seconds
% 12.00/7.03 % Total memory used: 221.894 MB
% 12.00/7.03 % Net memory used: 213.652 MB
%------------------------------------------------------------------------------