%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM461+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 168.91s 22.94s
% Output : CNFRefutation 168.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 10
% Syntax : Number of formulae : 69 ( 27 unt; 0 def)
% Number of atoms : 170 ( 70 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 184 ( 83 ~; 73 |; 18 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 57 ( 0 sgn 15 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsB,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('theBenchmark.p',mSortsB) ).
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(mDefLE,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ),
file('theBenchmark.p',mDefLE) ).
fof(mDefDiff,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
=> ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ) ),
file('theBenchmark.p',mDefDiff) ).
fof(m__840,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xl) ),
file('theBenchmark.p',m__840) ).
fof(m__840_03,axiom,
( sdtlseqdt0(xl,xn)
& xl != xn ),
file('theBenchmark.p',m__840_03) ).
fof(m__,conjecture,
( sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
& sdtpldt0(xl,xm) != sdtpldt0(xn,xm)
& sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& sdtpldt0(xm,xl) != sdtpldt0(xm,xn) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
& sdtpldt0(xl,xm) != sdtpldt0(xn,xm)
& sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
& sdtpldt0(xm,xl) != sdtpldt0(xm,xn) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_29,plain,
( aNaturalNumber0(sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB]) ).
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_54,plain,
( sdtpldt0(A,C) != B
| ~ aNaturalNumber0(C)
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefLE]) ).
cnf(c_55,plain,
( aNaturalNumber0(C)
| sdtmndt0(B,A) != C
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_56,plain,
( sdtpldt0(A,C) = B
| sdtmndt0(B,A) != C
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_63,plain,
aNaturalNumber0(xl),
inference(clausify,[status(thm)],[m__840]) ).
cnf(c_64,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__840]) ).
cnf(c_65,plain,
xn != xl,
inference(clausify,[status(thm)],[m__840_03]) ).
cnf(c_66,plain,
sdtlseqdt0(xl,xn),
inference(clausify,[status(thm)],[m__840_03]) ).
fof(m__873,axiom,
aNaturalNumber0(xm),
file('theBenchmark.p',m__873) ).
cnf(c_67,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__873]) ).
cnf(c_68,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
| sdtpldt0(xn,xm) = sdtpldt0(xl,xm)
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_23412,plain,
( sdtpldt0(xl,B) = A
| sdtmndt0(A,xl) != B
| ~ sdtlseqdt0(xl,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_56,c_63]) ).
cnf(c_23413,plain,
( sdtpldt0(xl,A) = xn
| sdtmndt0(xn,xl) != A
| ~ sdtlseqdt0(xl,xn) ),
inference(resolve,[status(thm)],[c_23412,c_64]) ).
cnf(c_23414,plain,
( sdtpldt0(xl,A) = xn
| sdtmndt0(xn,xl) != A ),
inference(resolve,[status(thm)],[c_23413,c_66]) ).
cnf(c_685,plain,
sdtpldt0(xl,sdtmndt0(xn,xl)) = xn,
inference(xxres,[status(thm)],[c_23414]) ).
cnf(c_23415,plain,
( aNaturalNumber0(B)
| sdtmndt0(A,xl) != B
| ~ sdtlseqdt0(xl,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_55,c_63]) ).
cnf(c_23416,plain,
( aNaturalNumber0(A)
| sdtmndt0(xn,xl) != A
| ~ sdtlseqdt0(xl,xn) ),
inference(resolve,[status(thm)],[c_23415,c_64]) ).
cnf(c_23417,plain,
( aNaturalNumber0(A)
| sdtmndt0(xn,xl) != A ),
inference(resolve,[status(thm)],[c_23416,c_66]) ).
cnf(c_686,plain,
aNaturalNumber0(sdtmndt0(xn,xl)),
inference(xxres,[status(thm)],[c_23417]) ).
cnf(c_23418,plain,
( sdtpldt0(A,xn) = sdtpldt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_31,c_64]) ).
cnf(c_23419,plain,
sdtpldt0(xm,xn) = sdtpldt0(xn,xm),
inference(resolve,[status(thm)],[c_23418,c_67]) ).
cnf(c_941,plain,
sdtpldt0(xn,xm) = sdtpldt0(xm,xn),
inference(copy,[status(thm)],[c_23419]) ).
cnf(c_23420,plain,
( sdtpldt0(A,xl) = sdtpldt0(xl,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_31,c_63]) ).
cnf(c_23421,plain,
sdtpldt0(xm,xl) = sdtpldt0(xl,xm),
inference(resolve,[status(thm)],[c_23420,c_67]) ).
cnf(c_942,plain,
sdtpldt0(xl,xm) = sdtpldt0(xm,xl),
inference(copy,[status(thm)],[c_23421]) ).
cnf(c_23422,plain,
( aNaturalNumber0(sdtpldt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_29,c_64]) ).
cnf(c_23423,plain,
aNaturalNumber0(sdtpldt0(xn,xm)),
inference(resolve,[status(thm)],[c_23422,c_67]) ).
cnf(c_948,plain,
aNaturalNumber0(sdtpldt0(xm,xn)),
inference(paramod,[status(thm)],[c_941,c_23423]) ).
cnf(c_23424,plain,
( aNaturalNumber0(sdtpldt0(xl,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_29,c_63]) ).
cnf(c_23425,plain,
aNaturalNumber0(sdtpldt0(xl,xm)),
inference(resolve,[status(thm)],[c_23424,c_67]) ).
cnf(c_949,plain,
aNaturalNumber0(sdtpldt0(xm,xl)),
inference(paramod,[status(thm)],[c_942,c_23425]) ).
cnf(c_23426,plain,
( B = A
| sdtpldt0(B,xm) != sdtpldt0(A,xm)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_44,c_67]) ).
cnf(c_23427,plain,
( A = xn
| sdtpldt0(A,xm) != sdtpldt0(xn,xm)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_23426,c_64]) ).
cnf(c_23428,plain,
( xl = xn
| sdtpldt0(xl,xm) != sdtpldt0(xn,xm) ),
inference(resolve,[status(thm)],[c_23427,c_63]) ).
cnf(c_23429,plain,
xl != xn,
inference(copy,[status(thm)],[c_65]) ).
cnf(c_23430,plain,
sdtpldt0(xl,xm) != sdtpldt0(xn,xm),
inference(resolve,[status(thm)],[c_23428,c_23429]) ).
cnf(c_23431,plain,
sdtpldt0(xm,xl) != sdtpldt0(xn,xm),
inference(paramod,[status(thm)],[c_942,c_23430]) ).
cnf(c_23432,plain,
sdtpldt0(xm,xl) != sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_941,c_23431]) ).
cnf(c_952,plain,
sdtpldt0(xm,xn) != sdtpldt0(xm,xl),
inference(copy,[status(thm)],[c_23432]) ).
cnf(c_23433,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
| sdtpldt0(xm,xn) = sdtpldt0(xl,xm)
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_941,c_68]) ).
cnf(c_23434,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xl,xm),sdtpldt0(xn,xm))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl)
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_942,c_23433]) ).
cnf(c_23435,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xn,xm))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl)
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_942,c_23434]) ).
cnf(c_23436,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl)
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(paramod,[status(thm)],[c_941,c_23435]) ).
cnf(c_23437,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_23436]) ).
cnf(c_23438,negated_conjecture,
( ~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn))
| sdtpldt0(xm,xn) = sdtpldt0(xm,xl) ),
inference(copy,[status(thm)],[c_23437]) ).
cnf(c_1022,negated_conjecture,
~ sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn)),
inference(resolve,[status(thm)],[c_952,c_23438]) ).
cnf(c_23439,plain,
( sdtpldt0(sdtpldt0(xm,A),B) = sdtpldt0(xm,sdtpldt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_32,c_67]) ).
cnf(c_23440,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) = sdtpldt0(xm,sdtpldt0(xl,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_23439,c_63]) ).
cnf(c_23441,plain,
sdtpldt0(sdtpldt0(xm,xl),sdtmndt0(xn,xl)) = sdtpldt0(xm,sdtpldt0(xl,sdtmndt0(xn,xl))),
inference(resolve,[status(thm)],[c_23440,c_686]) ).
cnf(c_16553,plain,
sdtpldt0(sdtpldt0(xm,xl),sdtmndt0(xn,xl)) = sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_685,c_23441]) ).
cnf(c_23442,plain,
( sdtpldt0(sdtpldt0(xm,xl),B) != A
| ~ aNaturalNumber0(B)
| sdtlseqdt0(sdtpldt0(xm,xl),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_54,c_949]) ).
cnf(c_23443,plain,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(A)
| sdtlseqdt0(sdtpldt0(xm,xl),sdtpldt0(xm,xn)) ),
inference(resolve,[status(thm)],[c_23442,c_948]) ).
cnf(c_23444,negated_conjecture,
( sdtpldt0(sdtpldt0(xm,xl),A) != sdtpldt0(xm,xn)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_23443,c_1022]) ).
cnf(c_23445,negated_conjecture,
sdtpldt0(sdtpldt0(xm,xl),sdtmndt0(xn,xl)) != sdtpldt0(xm,xn),
inference(resolve,[status(thm)],[c_23444,c_686]) ).
cnf(c_23446,negated_conjecture,
sdtpldt0(xm,xn) != sdtpldt0(xm,xn),
inference(paramod,[status(thm)],[c_16553,c_23445]) ).
cnf(c_23411,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_23446]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM461+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 02:45:47 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 3820977 was started by sandbox2 on n017,
% 0.09/0.35 % Sat Sep 26 02:45:47 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.36
% 0.09/0.36 % From the command line: assign(max_seconds, 300).
% 168.91/22.94
% 168.91/22.94 % SZS status Theorem for theBenchmark
% 168.91/22.94
% 168.91/22.94 % Proof 1 at 5.57 (+ 0.81) seconds.
% 168.91/22.94 % Length of proof is 32.
% 168.91/22.94 % Level of proof is 5.
% 168.91/22.94 % Maximum clause weight is 42.000.
% 168.91/22.94 % Given clauses 276.
% 168.91/22.94
% 168.91/22.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------