%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM516+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 : n006.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 92.21s 17.24s
% Output : CNFRefutation 92.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 7
% Syntax : Number of formulae : 50 ( 9 unt; 1 def)
% Number of atoms : 239 ( 74 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 314 ( 125 ~; 122 |; 57 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 30 ( 26 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
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(f55,conjecture,
( ( ( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
=> ( sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ? [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),W0) = sdtpldt0(sdtpldt0(xn,xm),xp)
& aNaturalNumber0(W0) ) ) )
& ~ ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ ( ( ( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
=> ( sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| ? [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),W0) = sdtpldt0(sdtpldt0(xn,xm),xp)
& aNaturalNumber0(W0) ) ) )
& ~ ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f63,plain,
! [W0,W1] :
( aNaturalNumber0(sdtpldt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f64,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f87,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(f89,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f119,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(f123,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f175,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f176,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f177,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f254,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
& ? [W0] :
( sdtpldt0(sdtsldt0(xn,xr),W0) = xn
& aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) != xn
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f255,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)],[f254]) ).
fof(f256,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f258,plain,
sdtsldt0(xn,xr) != xn,
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f263,plain,
sdtlseqdt0(sdtsldt0(xn,xr),xn),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f270,plain,
( ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
& ! [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),W0) != sdtpldt0(sdtpldt0(xn,xm),xp)
| ~ aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f271,definition,
( sP3_prd
<=> ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f272,plain,
( ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
& ! [W0] :
( sdtpldt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),W0) != sdtpldt0(sdtpldt0(xn,xm),xp)
| ~ aNaturalNumber0(W0) )
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| sP3_prd ),
inference(formula_renaming,[status(thm)],[f270,f271]) ).
fof(f276,plain,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f303,plain,
( ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp)
| xn != sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd )
& ( ( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr)) )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f271]) ).
fof(f306,plain,
( sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f354,plain,
( ~ sP3_prd
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f89,f306]) ).
fof(f361,plain,
( ~ sP3_prd
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f354,f177]) ).
fof(f378,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xm)
| ~ sP3_prd
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) ),
inference(resolution,[status(thm)],[f361,f89]) ).
fof(f380,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xm)
| ~ sP3_prd
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f378,f64]) ).
fof(f381,plain,
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xm)
| ~ sP3_prd ),
inference(resolution,[status(thm)],[f380,f64]) ).
fof(f382,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xm)
| ~ sP3_prd ),
inference(duplicate_literals_removal,[status(thm)],[f381]) ).
fof(f383,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f176]) ).
fof(f448,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ sP3_prd ),
inference(resolution,[status(thm)],[f256,f383]) ).
fof(f449,plain,
( sdtsldt0(xn,xr) = xn
| ~ sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f448,f175]) ).
fof(f456,plain,
( sP3_prd
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(sdtpldt0(sdtsldt0(xn,xr),xm),sdtpldt0(xn,xm))
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) ),
inference(resolution,[status(thm)],[f123,f276]) ).
fof(f460,plain,
( sP3_prd
| ~ sdtlseqdt0(sdtpldt0(sdtsldt0(xn,xr),xm),sdtpldt0(xn,xm))
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f456,f177]) ).
fof(f533,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) ),
inference(resolution,[status(thm)],[f460,f123]) ).
fof(f536,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sP3_prd
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f64]) ).
fof(f550,plain,
~ sP3_prd,
inference(resolution,[status(thm)],[f258,f449]) ).
fof(f562,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(backward_subsumption_resolution,[status(thm)],[f536,f550]) ).
fof(f571,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sdtpldt0(sdtsldt0(xn,xr),xm) = sdtpldt0(xn,xm) ),
inference(forward_subsumption_resolution,[status(thm)],[f562,f64]) ).
fof(f644,plain,
( sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolution,[status(thm)],[f571,f89]) ).
fof(f646,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(duplicate_literals_removal,[status(thm)],[f644]) ).
fof(f647,plain,
( ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f256]) ).
fof(f816,plain,
( ~ aNaturalNumber0(xm)
| sdtsldt0(xn,xr) = xn
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f647,f263]) ).
fof(f820,plain,
( ~ aNaturalNumber0(xm)
| sdtsldt0(xn,xr) = xn ),
inference(forward_subsumption_resolution,[status(thm)],[f816,f175]) ).
fof(f1118,plain,
~ aNaturalNumber0(xm),
inference(resolution,[status(thm)],[f820,f258]) ).
fof(f1119,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1118,f176]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM516+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.45 % Computer : n006.cluster.edu
% 0.17/5.45 % Model : x86_64 x86_64
% 0.17/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.45 % Memory : 8046.5625MB
% 0.17/5.45 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Mon Sep 21 02:36:47 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.17/5.48 % Drodi V4.1.1
% 92.21/17.24 % Refutation found
% 92.21/17.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 92.21/17.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 41.01/17.28 % Elapsed time: 11.810289 seconds
% 41.01/17.28 % CPU time: 93.170987 seconds
% 41.01/17.28 % Total memory used: 317.235 MB
% 41.01/17.28 % Net memory used: 292.983 MB
%------------------------------------------------------------------------------