%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM528+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:52 PM UTC 2026
% Result : Theorem 65.40s 8.86s
% Output : CNFRefutation 60.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 19
% Syntax : Number of formulae : 127 ( 32 unt; 1 def)
% Number of atoms : 413 ( 160 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 469 ( 183 ~; 206 |; 62 &)
% ( 1 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 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 : 89 ( 79 !; 10 ?)
% 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(f10,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ),
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(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(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
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(f40,hypothesis,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
( doDivides0(xp,xn)
& ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( xq = sdtsldt0(xn,xp)
& xn = sdtasdt0(xp,xq)
& aNaturalNumber0(xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
( ( sdtlseqdt0(xn,xm)
| ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) ) )
=> ( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xn),W0) = sdtasdt0(xm,xm)
& aNaturalNumber0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,conjecture,
( ( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
& xm != xn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
~ ( ( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
& xm != xn ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f54,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f58,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f67,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [W0,W1,W2] :
( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f70,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f73,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f83,plain,
! [W0] :
( ! [W1,W2] :
( W1 = W2
| ( sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f89,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f90,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f105,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f106,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f109,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f111,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f125,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f126,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f170,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f171,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f172,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f174,plain,
xm != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f175,plain,
xp != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f185,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f186,plain,
( isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10 ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f187,plain,
xp != sz10,
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
( doDivides0(xp,xn)
& xn = sdtasdt0(xp,sK7_skl)
& aNaturalNumber0(sK7_skl)
& doDivides0(xp,sdtasdt0(xn,xn))
& sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl)
& aNaturalNumber0(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44]) ).
fof(f192,plain,
aNaturalNumber0(sK6_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f198,plain,
aNaturalNumber0(xq),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f199,plain,
xn = sdtasdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f201,plain,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f202,plain,
( ( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xn),W0) = sdtasdt0(xm,xm)
& aNaturalNumber0(W0) ) )
| ( ~ sdtlseqdt0(xn,xm)
& ! [W0] :
( sdtpldt0(xn,W0) != xm
| ~ aNaturalNumber0(W0) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f203,definition,
( sP0_prd
<=> ( ~ sdtlseqdt0(xn,xm)
& ! [W0] :
( sdtpldt0(xn,W0) != xm
| ~ aNaturalNumber0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f204,plain,
( ( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xn),W0) = sdtasdt0(xm,xm)
& aNaturalNumber0(W0) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f202,f203]) ).
fof(f205,plain,
( ( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
& sdtpldt0(sdtasdt0(xn,xn),sK8_skl) = sdtasdt0(xm,xm)
& aNaturalNumber0(sK8_skl) )
| sP0_prd ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W0,sK8_skl)],[f204]) ).
fof(f208,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f209,plain,
( ( ~ sdtlseqdt0(xm,xn)
& ! [W0] :
( sdtpldt0(xm,W0) != xn
| ~ aNaturalNumber0(W0) ) )
| xm = xn ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f211,plain,
( ~ sdtlseqdt0(xm,xn)
| xm = xn ),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f212,plain,
( ( sdtlseqdt0(xn,xm)
| ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) )
| sP0_prd )
& ( ( ~ sdtlseqdt0(xn,xm)
& ! [W0] :
( sdtpldt0(xn,W0) != xm
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f203]) ).
fof(f213,plain,
( ( sdtlseqdt0(xn,xm)
| ( sdtpldt0(xn,sK9_skl) = xm
& aNaturalNumber0(sK9_skl) )
| sP0_prd )
& ( ( ~ sdtlseqdt0(xn,xm)
& ! [W0] :
( sdtpldt0(xn,W0) != xm
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W0,sK9_skl)],[f212]) ).
fof(f215,plain,
( ~ sdtlseqdt0(xn,xm)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f230,plain,
( xm = xn
| sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f111,f211]) ).
fof(f231,plain,
( xm = xn
| sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f230,f170]) ).
fof(f232,plain,
( xm = xn
| sdtlseqdt0(xn,xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f231,f171]) ).
fof(f264,plain,
( xm = xn
| ~ sP0_prd ),
inference(resolution,[status(thm)],[f215,f232]) ).
fof(f265,plain,
( sdtlseqdt0(xm,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm)
| ~ sP0_prd ),
inference(resolution,[status(thm)],[f215,f111]) ).
fof(f266,plain,
( sdtlseqdt0(xm,xn)
| ~ aNaturalNumber0(xn)
| ~ sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f171]) ).
fof(f273,plain,
( sdtlseqdt0(xm,xn)
| ~ sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f170]) ).
fof(f402,plain,
( aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK6_skl)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f193,f59]) ).
fof(f409,plain,
( aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f402,f172]) ).
fof(f418,plain,
aNaturalNumber0(sdtasdt0(xn,xn)),
inference(forward_subsumption_resolution,[status(thm)],[f409,f192]) ).
fof(f459,plain,
! [X0] :
( sK6_skl = X0
| sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK6_skl)
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f193,f84]) ).
fof(f468,plain,
! [X0] :
( sK6_skl = X0
| sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK6_skl)
| xp = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f459,f172]) ).
fof(f899,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sdtasdt0(xm,xm)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| sdtasdt0(xm,xm) = sz00
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(paramodulation,[status(thm)],[f185,f85]) ).
fof(f915,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sdtasdt0(xm,xm)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0)
| sdtasdt0(xm,xm) = sz00
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f899,f172]) ).
fof(f927,plain,
( sdtasdt0(sdtasdt0(xp,xq),xq) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f201,f70]) ).
fof(f942,plain,
( sdtasdt0(xn,xq) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xp) ),
inference(forward_demodulation,[status(thm)],[f199,f927]) ).
fof(f943,plain,
( sdtasdt0(xn,xq) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xp) ),
inference(duplicate_literals_removal,[status(thm)],[f942]) ).
fof(f944,plain,
( sdtasdt0(xn,xq) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(xq) ),
inference(forward_subsumption_resolution,[status(thm)],[f943,f172]) ).
fof(f962,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sP0_prd ),
inference(resolution,[status(thm)],[f208,f106]) ).
fof(f966,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f962,f418]) ).
fof(f1011,plain,
sdtasdt0(xp,sdtasdt0(xn,xq)) = sdtasdt0(xn,xn),
inference(backward_demodulation,[status(thm)],[f1012,f185]) ).
fof(f1012,plain,
sdtasdt0(xn,xq) = sdtasdt0(xm,xm),
inference(forward_subsumption_resolution,[status(thm)],[f944,f198]) ).
fof(f1013,plain,
( xm = sz00
| xm = sz00
| sdtasdt0(xn,xq) != sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm) ),
inference(paramodulation,[status(thm)],[f1012,f90]) ).
fof(f1021,plain,
( aNaturalNumber0(sdtasdt0(xn,xq))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm) ),
inference(paramodulation,[status(thm)],[f1012,f59]) ).
fof(f1025,plain,
( xm = sz00
| sdtasdt0(xn,xq) != sz00
| ~ aNaturalNumber0(xm) ),
inference(duplicate_literals_removal,[status(thm)],[f1013]) ).
fof(f1026,plain,
( xm = sz00
| sdtasdt0(xn,xq) != sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f1025,f171]) ).
fof(f1041,plain,
( aNaturalNumber0(sdtasdt0(xn,xq))
| ~ aNaturalNumber0(xm) ),
inference(duplicate_literals_removal,[status(thm)],[f1021]) ).
fof(f1042,plain,
aNaturalNumber0(sdtasdt0(xn,xq)),
inference(forward_subsumption_resolution,[status(thm)],[f1041,f171]) ).
fof(f1049,plain,
sdtasdt0(xn,xq) != sz00,
inference(forward_subsumption_resolution,[status(thm)],[f1026,f174]) ).
fof(f1360,plain,
( sdtasdt0(sdtasdt0(xn,xq),xp) = sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xq)) ),
inference(paramodulation,[status(thm)],[f1011,f68]) ).
fof(f1377,plain,
( sdtasdt0(sdtasdt0(xn,xq),xp) = sdtasdt0(xn,xn)
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[status(thm)],[f1360,f1042]) ).
fof(f2462,plain,
sdtasdt0(sdtasdt0(xn,xq),xp) = sdtasdt0(xn,xn),
inference(forward_subsumption_resolution,[status(thm)],[f1377,f172]) ).
fof(f5666,plain,
! [X0] :
( sK6_skl = X0
| sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f175]) ).
fof(f5670,plain,
( sK6_skl = sdtasdt0(xn,xq)
| ~ aNaturalNumber0(sdtasdt0(xn,xq))
| ~ aNaturalNumber0(sK6_skl) ),
inference(resolution,[status(thm)],[f5666,f1011]) ).
fof(f5679,plain,
( sK6_skl = sdtasdt0(xn,xq)
| ~ aNaturalNumber0(sdtasdt0(xn,xq)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5670,f192]) ).
fof(f6231,plain,
sdtasdt0(sK6_skl,xp) = sdtasdt0(xn,xn),
inference(backward_demodulation,[status(thm)],[f6243,f2462]) ).
fof(f6240,plain,
sK6_skl != sz00,
inference(backward_demodulation,[status(thm)],[f6243,f1049]) ).
fof(f6242,plain,
sK6_skl = sdtasdt0(xm,xm),
inference(backward_demodulation,[status(thm)],[f6243,f1012]) ).
fof(f6243,plain,
sK6_skl = sdtasdt0(xn,xq),
inference(forward_subsumption_resolution,[status(thm)],[f5679,f1042]) ).
fof(f6490,plain,
( sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sK6_skl)
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f6231,f126]) ).
fof(f6520,plain,
( sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6490,f172]) ).
fof(f7119,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sdtasdt0(xm,xm)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0)
| sdtasdt0(xm,xm) = sz00
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_demodulation,[status(thm)],[f6242,f915]) ).
fof(f7120,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sdtasdt0(xm,xm)) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0)
| sK6_skl = sz00
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_demodulation,[status(thm)],[f6242,f7119]) ).
fof(f7121,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sK6_skl) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0)
| sK6_skl = sz00
| ~ aNaturalNumber0(sK6_skl) ),
inference(forward_demodulation,[status(thm)],[f6242,f7120]) ).
fof(f7122,plain,
! [X0] :
( X0 = xp
| sdtasdt0(X0,sK6_skl) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(X0)
| sK6_skl = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f7121,f192]) ).
fof(f7918,plain,
( sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| xp = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f6520,f192]) ).
fof(f11007,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK6_skl)
| sP0_prd ),
inference(forward_demodulation,[status(thm)],[f6242,f966]) ).
fof(f11008,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK6_skl)
| sP0_prd ),
inference(forward_demodulation,[status(thm)],[f6242,f11007]) ).
fof(f11009,plain,
( sK6_skl = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK6_skl)
| sP0_prd ),
inference(forward_demodulation,[status(thm)],[f6242,f11008]) ).
fof(f11010,plain,
( sK6_skl = sdtasdt0(xn,xn)
| ~ sdtlseqdt0(sK6_skl,sdtasdt0(xn,xn))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f11009,f192]) ).
fof(f11011,plain,
( xp = sz00
| sK6_skl = sdtasdt0(xn,xn)
| sP0_prd ),
inference(resolution,[status(thm)],[f11010,f7918]) ).
fof(f11016,plain,
( sK6_skl = sdtasdt0(xn,xn)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f11011,f175]) ).
fof(f11026,plain,
! [X0] :
( sP0_prd
| X0 = xp
| sdtasdt0(X0,sK6_skl) != sK6_skl
| ~ aNaturalNumber0(X0)
| sK6_skl = sz00 ),
inference(paramodulation,[status(thm)],[f11016,f7122]) ).
fof(f11080,plain,
! [X0] :
( sP0_prd
| X0 = xp
| sdtasdt0(X0,sK6_skl) != sK6_skl
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11026,f6240]) ).
fof(f11349,plain,
( ~ aNaturalNumber0(sK6_skl)
| sP0_prd
| sz10 = xp
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f11080,f73]) ).
fof(f11351,plain,
( ~ aNaturalNumber0(sK6_skl)
| sP0_prd
| sz10 = xp ),
inference(forward_subsumption_resolution,[status(thm)],[f11349,f54]) ).
fof(f11352,plain,
( ~ aNaturalNumber0(sK6_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f11351,f187]) ).
fof(f11353,plain,
sP0_prd,
inference(resolution,[status(thm)],[f11352,f192]) ).
fof(f11373,plain,
sdtlseqdt0(xm,xn),
inference(backward_subsumption_resolution,[status(thm)],[f273,f11353]) ).
fof(f11374,plain,
xm = xn,
inference(backward_subsumption_resolution,[status(thm)],[f264,f11353]) ).
fof(f11375,plain,
~ sdtlseqdt0(xn,xm),
inference(backward_subsumption_resolution,[status(thm)],[f215,f11353]) ).
fof(f11540,plain,
sdtlseqdt0(xn,xn),
inference(forward_demodulation,[status(thm)],[f11374,f11373]) ).
fof(f11547,plain,
~ sdtlseqdt0(xn,xn),
inference(forward_demodulation,[status(thm)],[f11374,f11375]) ).
fof(f11548,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11547,f11540]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n009.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 02:37:57 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.42 % Drodi V4.1.1
% 65.40/8.86 % Refutation found
% 65.40/8.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 65.40/8.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 60.56/8.91 % Elapsed time: 8.501962 seconds
% 60.56/8.91 % CPU time: 66.711411 seconds
% 60.56/8.91 % Total memory used: 261.656 MB
% 60.56/8.91 % Net memory used: 244.687 MB
%------------------------------------------------------------------------------