%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM461+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 50.74s 11.87s
% Output : CNFRefutation 50.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 8
% Syntax : Number of formulae : 52 ( 17 unt; 1 def)
% Number of atoms : 168 ( 76 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 201 ( 85 ~; 78 |; 33 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 52 ( 46 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('/export/starexec/sandbox2/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/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,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xl) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
( sdtlseqdt0(xl,xn)
& ? [W0] :
( sdtpldt0(xl,W0) = xn
& aNaturalNumber0(W0) )
& xl != xn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
aNaturalNumber0(xm),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,conjecture,
( ( sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
| ? [W0] :
( sdtpldt0(sdtpldt0(xl,xm),W0) = sdtpldt0(xn,xm)
& aNaturalNumber0(W0) ) )
& sdtpldt0(xl,xm) != sdtpldt0(xn,xm)
& ( sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| ? [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) = sdtpldt0(xm,xn)
& aNaturalNumber0(W0) ) )
& sdtpldt0(xm,xl) != sdtpldt0(xm,xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
~ ( ( sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
| ? [W0] :
( sdtpldt0(sdtpldt0(xl,xm),W0) = sdtpldt0(xn,xm)
& aNaturalNumber0(W0) ) )
& sdtpldt0(xl,xm) != sdtpldt0(xn,xm)
& ( sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| ? [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) = sdtpldt0(xm,xn)
& aNaturalNumber0(W0) ) )
& sdtpldt0(xm,xl) != sdtpldt0(xm,xn) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f39,plain,
! [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f40,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,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(f42,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)],[f41]) ).
fof(f59,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(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f91,plain,
aNaturalNumber0(xl),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f92,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f93,plain,
( sdtlseqdt0(xl,xn)
& sdtpldt0(xl,sK1_skl) = xn
& aNaturalNumber0(sK1_skl)
& xl != xn ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W0,sK1_skl)],[f25]) ).
fof(f94,plain,
xl != xn,
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
aNaturalNumber0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
sdtpldt0(xl,sK1_skl) = xn,
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f98,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f99,plain,
( ( ~ sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
& ! [W0] :
( sdtpldt0(sdtpldt0(xl,xm),W0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(W0) ) )
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm)
| ( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& ! [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(W0) ) )
| sdtpldt0(xm,xl) = sdtpldt0(xm,xn) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f100,definition,
( sP0_prd
<=> ( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& ! [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f101,plain,
( ( ~ sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
& ! [W0] :
( sdtpldt0(sdtpldt0(xl,xm),W0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(W0) ) )
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm)
| sP0_prd
| sdtpldt0(xm,xl) = sdtpldt0(xm,xn) ),
inference(formula_renaming,[status(thm)],[f99,f100]) ).
fof(f102,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm)
| sP0_prd
| sdtpldt0(xm,xl) = sdtpldt0(xm,xn) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f104,plain,
( ( sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| ? [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) = sdtpldt0(xm,xn)
& aNaturalNumber0(W0) )
| sP0_prd )
& ( ( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& ! [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f100]) ).
fof(f105,plain,
( ( sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| ( sdtpldt0(sdtpldt0(xm,xl),sK2_skl) = sdtpldt0(xm,xn)
& aNaturalNumber0(sK2_skl) )
| sP0_prd )
& ( ( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& ! [W0] :
( sdtpldt0(sdtpldt0(xm,xl),W0) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W0,sK2_skl)],[f104]) ).
fof(f106,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xm,xl),X0) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f117,plain,
! [X0] :
( sdtpldt0(X0,xm) = sdtpldt0(xm,X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f40,f98]) ).
fof(f162,plain,
! [X0,X1] :
( xn = X1
| sdtpldt0(X0,xn) != sdtpldt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f60,f92]) ).
fof(f197,plain,
! [X0] :
( sdtpldt0(sdtpldt0(X0,xl),sK1_skl) = sdtpldt0(X0,xn)
| ~ aNaturalNumber0(sK1_skl)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f96,f42]) ).
fof(f200,plain,
! [X0] :
( sdtpldt0(sdtpldt0(X0,xl),sK1_skl) = sdtpldt0(X0,xn)
| ~ aNaturalNumber0(sK1_skl)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f197,f91]) ).
fof(f516,plain,
sdtpldt0(xn,xm) = sdtpldt0(xm,xn),
inference(resolution,[status(thm)],[f117,f92]) ).
fof(f517,plain,
sdtpldt0(xl,xm) = sdtpldt0(xm,xl),
inference(resolution,[status(thm)],[f117,f91]) ).
fof(f878,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm)
| sP0_prd
| sdtpldt0(xm,xl) = sdtpldt0(xn,xm) ),
inference(backward_demodulation,[status(thm)],[f516,f102]) ).
fof(f879,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xm,xl),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| ~ sP0_prd ),
inference(backward_demodulation,[status(thm)],[f516,f106]) ).
fof(f931,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm)
| sP0_prd
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm) ),
inference(forward_demodulation,[status(thm)],[f517,f878]) ).
fof(f932,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| sP0_prd
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm) ),
inference(duplicate_literals_removal,[status(thm)],[f931]) ).
fof(f933,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm) ),
inference(backward_subsumption_resolution,[status(thm)],[f932,f934]) ).
fof(f934,plain,
! [X0] :
( sdtpldt0(sdtpldt0(xl,xm),X0) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X0)
| ~ sP0_prd ),
inference(forward_demodulation,[status(thm)],[f517,f879]) ).
fof(f953,plain,
( sdtpldt0(sdtpldt0(xl,xm),sK1_skl) != sdtpldt0(xn,xm)
| sdtpldt0(xl,xm) = sdtpldt0(xn,xm) ),
inference(resolution,[status(thm)],[f933,f95]) ).
fof(f1039,plain,
! [X0] :
( xn = xl
| sdtpldt0(X0,xn) != sdtpldt0(X0,xl)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f162,f91]) ).
fof(f1040,plain,
! [X0] :
( sdtpldt0(X0,xn) != sdtpldt0(X0,xl)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1039,f94]) ).
fof(f1336,plain,
! [X0] :
( sdtpldt0(sdtpldt0(X0,xl),sK1_skl) = sdtpldt0(X0,xn)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f200,f95]) ).
fof(f1342,plain,
sdtpldt0(sdtpldt0(xm,xl),sK1_skl) = sdtpldt0(xm,xn),
inference(resolution,[status(thm)],[f1336,f98]) ).
fof(f1348,plain,
sdtpldt0(sdtpldt0(xl,xm),sK1_skl) = sdtpldt0(xm,xn),
inference(forward_demodulation,[status(thm)],[f517,f1342]) ).
fof(f1349,plain,
sdtpldt0(sdtpldt0(xl,xm),sK1_skl) = sdtpldt0(xn,xm),
inference(forward_demodulation,[status(thm)],[f516,f1348]) ).
fof(f1709,plain,
sdtpldt0(xm,xn) != sdtpldt0(xm,xl),
inference(resolution,[status(thm)],[f1040,f98]) ).
fof(f1715,plain,
sdtpldt0(xn,xm) != sdtpldt0(xm,xl),
inference(forward_demodulation,[status(thm)],[f516,f1709]) ).
fof(f1716,plain,
sdtpldt0(xn,xm) != sdtpldt0(xl,xm),
inference(forward_demodulation,[status(thm)],[f517,f1715]) ).
fof(f1753,plain,
sdtpldt0(sdtpldt0(xl,xm),sK1_skl) != sdtpldt0(xn,xm),
inference(backward_subsumption_resolution,[status(thm)],[f953,f1716]) ).
fof(f11945,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1349,f1753]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM461+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n013.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % 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:31:43 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 50.74/11.87 % Refutation found
% 50.74/11.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.74/11.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.97/11.92 % Elapsed time: 6.531521 seconds
% 4.97/11.92 % CPU time: 51.580672 seconds
% 4.97/11.92 % Total memory used: 335.207 MB
% 4.97/11.92 % Net memory used: 315.121 MB
%------------------------------------------------------------------------------