%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM461+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 08:17:04 AM UTC 2026
% Result : Theorem 248.42s 33.31s
% Output : CNFRefutation 248.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 7
% Syntax : Number of formulae : 77 ( 32 unt; 0 def)
% Number of atoms : 224 ( 135 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 260 ( 113 ~; 118 |; 25 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 72 ( 0 sgn 8 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mAddComm,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('theBenchmark.p',mAddComm) ).
fof(mAddAsso,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('theBenchmark.p',mAddAsso) ).
fof(mAddCanc,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('theBenchmark.p',mAddCanc) ).
fof(m__840,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xl) ),
file('theBenchmark.p',m__840) ).
fof(m__840_03,axiom,
( sdtlseqdt0(xl,xn)
& ? [W0] :
( sdtpldt0(xl,W0) = xn
& aNaturalNumber0(W0) )
& xl != xn ),
file('theBenchmark.p',m__840_03) ).
fof(m__,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('theBenchmark.p',m__) ).
fof(m___neg,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(assume_negation,[status(cth)],[m__]) ).
cnf(c_31,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddComm]) ).
cnf(c_32,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_44,plain,
( C = B
| sdtpldt0(C,A) != sdtpldt0(B,A)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mAddCanc]) ).
cnf(c_63,plain,
aNaturalNumber0(xl),
inference(clausify,[status(thm)],[m__840]) ).
cnf(c_64,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__840]) ).
fof(nnf_24,plain,
( sdtlseqdt0(xl,xn)
& ? [W0] :
( sdtpldt0(xl,W0) = xn
& aNaturalNumber0(W0) )
& xn != xl ),
inference(fof_nnf,[status(thm)],[m__840_03]) ).
fof(sk_m__840_03,plain,
( sdtlseqdt0(xl,xn)
& sdtpldt0(xl,sK0) = xn
& aNaturalNumber0(sK0)
& xn != xl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W0,sK0)],[nnf_24]) ).
cnf(c_65,plain,
xn != xl,
inference(split_conjunct,[status(thm)],[sk_m__840_03]) ).
cnf(c_66,plain,
aNaturalNumber0(sK0),
inference(split_conjunct,[status(thm)],[sk_m__840_03]) ).
cnf(c_67,plain,
sdtpldt0(xl,sK0) = xn,
inference(split_conjunct,[status(thm)],[sk_m__840_03]) ).
cnf(c_68,plain,
xn = sdtpldt0(xl,sK0),
inference(copy,[status(thm)],[c_67]) ).
fof(m__873,axiom,
aNaturalNumber0(xm),
file('theBenchmark.p',m__873) ).
cnf(c_71,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__873]) ).
cnf(c_72,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,xm),B) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(B)
| sdtpldt0(xn,xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_2499,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,xm),B) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(B)
| sdtpldt0(xn,xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_68,c_72]) ).
cnf(c_2500,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,xm),B) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(B)
| sdtpldt0(xn,xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_68,c_2499]) ).
cnf(c_2501,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,xm),B) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(B)
| sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_68,c_2500]) ).
cnf(c_2502,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,xm),B) != sdtpldt0(sdtpldt0(xl,sK0),xm)
| ~ aNaturalNumber0(B)
| sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_68,c_2501]) ).
cnf(c_73,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_2502]) ).
cnf(c_115,plain,
sdtpldt0(xl,sK0) != xl,
inference(paramod,[status(thm)],[c_68,c_65]) ).
cnf(c_116,plain,
aNaturalNumber0(sdtpldt0(xl,sK0)),
inference(paramod,[status(thm)],[c_68,c_64]) ).
cnf(c_2503,plain,
( sdtpldt0(A,xl) = sdtpldt0(xl,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_31,c_63]) ).
cnf(c_625,plain,
sdtpldt0(sK0,xl) = sdtpldt0(xl,sK0),
inference(resolve,[status(thm)],[c_2503,c_66]) ).
cnf(c_2504,plain,
( sdtpldt0(sdtpldt0(sK0,A),B) = sdtpldt0(sK0,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_32,c_66]) ).
cnf(c_2505,plain,
( sdtpldt0(sdtpldt0(sK0,xl),A) = sdtpldt0(sK0,sdtpldt0(xl,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_2504,c_63]) ).
cnf(c_2506,plain,
sdtpldt0(sdtpldt0(sK0,xl),xm) = sdtpldt0(sK0,sdtpldt0(xl,xm)),
inference(resolve,[status(thm)],[c_2505,c_71]) ).
cnf(c_903,plain,
sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(sK0,sdtpldt0(xl,xm)),
inference(paramod,[status(thm)],[c_625,c_2506]) ).
cnf(c_2507,plain,
( sdtpldt0(sdtpldt0(sK0,A),B) = sdtpldt0(sK0,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_32,c_66]) ).
cnf(c_2508,plain,
( sdtpldt0(sdtpldt0(sK0,xm),A) = sdtpldt0(sK0,sdtpldt0(xm,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_2507,c_71]) ).
cnf(c_922,plain,
sdtpldt0(sdtpldt0(sK0,xm),xl) = sdtpldt0(sK0,sdtpldt0(xm,xl)),
inference(resolve,[status(thm)],[c_2508,c_63]) ).
cnf(c_2509,plain,
( sdtpldt0(sdtpldt0(xm,A),B) = sdtpldt0(xm,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_32,c_71]) ).
cnf(c_2510,plain,
( sdtpldt0(sdtpldt0(xm,sK0),A) = sdtpldt0(xm,sdtpldt0(sK0,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_2509,c_66]) ).
cnf(c_2511,plain,
sdtpldt0(sdtpldt0(xm,sK0),xl) = sdtpldt0(xm,sdtpldt0(sK0,xl)),
inference(resolve,[status(thm)],[c_2510,c_63]) ).
cnf(c_937,plain,
sdtpldt0(sdtpldt0(xm,sK0),xl) = sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(paramod,[status(thm)],[c_625,c_2511]) ).
cnf(c_2512,plain,
( sdtpldt0(sdtpldt0(xm,A),B) = sdtpldt0(xm,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_32,c_71]) ).
cnf(c_2513,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) = sdtpldt0(xm,sdtpldt0(xl,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_2512,c_63]) ).
cnf(c_940,plain,
sdtpldt0(sdtpldt0(xm,xl),sK0) = sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(resolve,[status(thm)],[c_2513,c_66]) ).
cnf(c_2514,plain,
( sdtpldt0(A,sK0) = sdtpldt0(sK0,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_31,c_66]) ).
cnf(c_2515,plain,
sdtpldt0(xm,sK0) = sdtpldt0(sK0,xm),
inference(resolve,[status(thm)],[c_2514,c_71]) ).
cnf(c_948,plain,
sdtpldt0(sK0,xm) = sdtpldt0(xm,sK0),
inference(copy,[status(thm)],[c_2515]) ).
cnf(c_2516,plain,
( sdtpldt0(A,xl) = sdtpldt0(xl,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_31,c_63]) ).
cnf(c_2517,plain,
sdtpldt0(xm,xl) = sdtpldt0(xl,xm),
inference(resolve,[status(thm)],[c_2516,c_71]) ).
cnf(c_949,plain,
sdtpldt0(xl,xm) = sdtpldt0(xm,xl),
inference(copy,[status(thm)],[c_2517]) ).
cnf(c_2518,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xl,xm)) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_903,c_73]) ).
cnf(c_2519,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xl,xm)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_949,c_2518]) ).
cnf(c_2520,negated_conjecture,
( sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_949,c_2519]) ).
cnf(c_2521,negated_conjecture,
( sdtpldt0(sK0,sdtpldt0(xl,xm)) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_903,c_2520]) ).
cnf(c_2522,negated_conjecture,
( sdtpldt0(sK0,sdtpldt0(xm,xl)) != sdtpldt0(sdtpldt0(xl,xm),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_949,c_2521]) ).
cnf(c_2523,negated_conjecture,
( sdtpldt0(sK0,sdtpldt0(xm,xl)) != sdtpldt0(sdtpldt0(xm,xl),B)
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_949,c_2522]) ).
cnf(c_1023,negated_conjecture,
( sdtpldt0(sdtpldt0(xm,xl),B) != sdtpldt0(sK0,sdtpldt0(xm,xl))
| ~ aNaturalNumber0(B)
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_2523]) ).
cnf(c_1024,plain,
sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(sK0,sdtpldt0(xm,xl)),
inference(paramod,[status(thm)],[c_949,c_903]) ).
cnf(c_2524,plain,
sdtpldt0(sdtpldt0(xm,sK0),xl) = sdtpldt0(sK0,sdtpldt0(xm,xl)),
inference(paramod,[status(thm)],[c_948,c_922]) ).
cnf(c_2525,plain,
sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(sK0,sdtpldt0(xm,xl)),
inference(paramod,[status(thm)],[c_937,c_2524]) ).
cnf(c_1027,plain,
sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(copy,[status(thm)],[c_2525]) ).
cnf(c_2526,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(sK0,sdtpldt0(xm,xl))
| sdtpldt0(sK0,sdtpldt0(xm,xl)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(factor,[status(thm)],[c_1023]) ).
cnf(c_2527,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(sK0,sdtpldt0(xm,xl))
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_1027,c_2526]) ).
cnf(c_2528,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl)
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_1027,c_2527]) ).
cnf(c_2529,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_2528]) ).
cnf(c_1051,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A)
| sdtpldt0(xm,sdtpldt0(xl,sK0)) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_2529]) ).
cnf(c_1053,plain,
sdtpldt0(sdtpldt0(xl,sK0),xm) = sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(paramod,[status(thm)],[c_1027,c_1024]) ).
cnf(c_2530,plain,
( B = A
| sdtpldt0(B,xm) != sdtpldt0(A,xm)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_44,c_71]) ).
cnf(c_2531,plain,
( A = xl
| sdtpldt0(A,xm) != sdtpldt0(xl,xm)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_2530,c_63]) ).
cnf(c_2532,plain,
( sdtpldt0(xl,sK0) = xl
| sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(xl,xm) ),
inference(resolve,[status(thm)],[c_2531,c_116]) ).
cnf(c_2533,plain,
sdtpldt0(sdtpldt0(xl,sK0),xm) != sdtpldt0(xl,xm),
inference(resolve,[status(thm)],[c_2532,c_115]) ).
cnf(c_2534,plain,
sdtpldt0(xm,sdtpldt0(xl,sK0)) != sdtpldt0(xl,xm),
inference(paramod,[status(thm)],[c_1053,c_2533]) ).
cnf(c_1541,plain,
sdtpldt0(xm,sdtpldt0(xl,sK0)) != sdtpldt0(xm,xl),
inference(paramod,[status(thm)],[c_949,c_2534]) ).
cnf(c_1615,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,sdtpldt0(xl,sK0))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_1541,c_1051]) ).
cnf(c_2535,plain,
sdtpldt0(sdtpldt0(xm,xl),sK0) != sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(resolve,[status(thm)],[c_1615,c_66]) ).
cnf(c_2536,plain,
sdtpldt0(xm,sdtpldt0(xl,sK0)) != sdtpldt0(xm,sdtpldt0(xl,sK0)),
inference(paramod,[status(thm)],[c_940,c_2535]) ).
cnf(c_2498,plain,
$false,
inference(copy,[status(thm)],[c_2536]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM461+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 02:53:42 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2953583 was started by sandbox on n015,
% 0.13/0.36 % Sat Sep 26 02:53:42 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 248.42/33.31
% 248.42/33.31 % SZS status Theorem for theBenchmark
% 248.42/33.31
% 248.42/33.31 % Proof 1 at 0.68 (+ 0.11) seconds.
% 248.42/33.31 % Length of proof is 35.
% 248.42/33.31 % Level of proof is 8.
% 248.42/33.31 % Maximum clause weight is 89.000.
% 248.42/33.31 % Given clauses 230.
% 248.42/33.31
% 248.42/33.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------