%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM624+1 : 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 : n003.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:36 AM UTC 2026
% Result : Theorem 4.06s 0.97s
% Output : CNFRefutation 4.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of formulae : 63 ( 33 unt; 0 def)
% Number of atoms : 131 ( 37 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 117 ( 49 ~; 47 |; 13 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 31 ( 0 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mDefSub,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('theBenchmark.p',mDefSub) ).
fof(mNATSet,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('theBenchmark.p',mNATSet) ).
fof(mLessASymm,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLessASymm) ).
fof(mDefMin,axiom,
! [W0] :
( ( W0 != slcrc0
& aSubsetOf0(W0,szNzAzT0) )
=> ! [W1] :
( W1 = szmzizndt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,W0) ) ) ),
file('theBenchmark.p',mDefMin) ).
fof(m__3435,axiom,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('theBenchmark.p',m__3435) ).
fof(m__5093,axiom,
( xQ != slcrc0
& aSubsetOf0(xQ,xO) ),
file('theBenchmark.p',m__5093) ).
fof(m__5365,axiom,
( aElementOf0(xx,xO)
& aElementOf0(xx,szNzAzT0) ),
file('theBenchmark.p',m__5365) ).
fof(m__5481,axiom,
( aElementOf0(xx,xQ)
& aElementOf0(xp,sdtlpdtrp0(xN,xm)) ),
file('theBenchmark.p',m__5481) ).
fof(m__5518,axiom,
( sdtlpdtrp0(xN,xm) != slcrc0
& xQ != slcrc0
& aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
& aSubsetOf0(xQ,szNzAzT0) ),
file('theBenchmark.p',m__5518) ).
fof(m__,conjecture,
xp = xx,
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
xp != xx,
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_106,plain,
( aSet0(B)
| ~ aSubsetOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSub]) ).
cnf(c_107,plain,
( aElementOf0(C,A)
| ~ aElementOf0(C,B)
| ~ aSubsetOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSub]) ).
cnf(c_138,plain,
aSet0(szNzAzT0),
inference(clausify,[status(thm)],[mNATSet]) ).
cnf(c_153,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aElementOf0(B,szNzAzT0)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mLessASymm]) ).
cnf(c_169,plain,
( sdtlseqdt0(B,C)
| ~ aElementOf0(C,A)
| szmzizndt0(A) != B
| slcrc0 = A
| ~ aSubsetOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mDefMin]) ).
cnf(c_241,plain,
aSubsetOf0(xS,szNzAzT0),
inference(clausify,[status(thm)],[m__3435]) ).
fof(m__4998,axiom,
aSubsetOf0(xO,xS),
file('theBenchmark.p',m__4998) ).
cnf(c_298,plain,
aSubsetOf0(xO,xS),
inference(clausify,[status(thm)],[m__4998]) ).
cnf(c_301,plain,
xQ != slcrc0,
inference(clausify,[status(thm)],[m__5093]) ).
fof(m__5106,axiom,
aSubsetOf0(xQ,szNzAzT0),
file('theBenchmark.p',m__5106) ).
cnf(c_302,plain,
aSubsetOf0(xQ,szNzAzT0),
inference(clausify,[status(thm)],[m__5106]) ).
fof(m__5147,axiom,
xp = szmzizndt0(xQ),
file('theBenchmark.p',m__5147) ).
cnf(c_304,plain,
xp = szmzizndt0(xQ),
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_305,plain,
szmzizndt0(xQ) = xp,
inference(copy,[status(thm)],[c_304]) ).
fof(m__5182,axiom,
aElementOf0(xp,xO),
file('theBenchmark.p',m__5182) ).
cnf(c_310,plain,
aElementOf0(xp,xO),
inference(clausify,[status(thm)],[m__5182]) ).
cnf(c_320,plain,
aElementOf0(xx,szNzAzT0),
inference(clausify,[status(thm)],[m__5365]) ).
fof(m__5401,axiom,
xx = szmzizndt0(sdtlpdtrp0(xN,xm)),
file('theBenchmark.p',m__5401) ).
cnf(c_324,plain,
xx = szmzizndt0(sdtlpdtrp0(xN,xm)),
inference(clausify,[status(thm)],[m__5401]) ).
cnf(c_325,plain,
szmzizndt0(sdtlpdtrp0(xN,xm)) = xx,
inference(copy,[status(thm)],[c_324]) ).
cnf(c_328,plain,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(clausify,[status(thm)],[m__5481]) ).
cnf(c_329,plain,
aElementOf0(xx,xQ),
inference(clausify,[status(thm)],[m__5481]) ).
cnf(c_330,plain,
aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0),
inference(clausify,[status(thm)],[m__5518]) ).
cnf(c_331,plain,
sdtlpdtrp0(xN,xm) != slcrc0,
inference(clausify,[status(thm)],[m__5518]) ).
cnf(c_332,negated_conjecture,
xx != xp,
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_333,negated_conjecture,
xp != xx,
inference(copy,[status(thm)],[c_332]) ).
cnf(c_3440,plain,
( aElementOf0(A,szNzAzT0)
| ~ aElementOf0(A,xS)
| ~ aSet0(szNzAzT0) ),
inference(resolve,[status(thm)],[c_241,c_107]) ).
cnf(c_787,plain,
( aElementOf0(A,szNzAzT0)
| ~ aElementOf0(A,xS) ),
inference(resolve,[status(thm)],[c_138,c_3440]) ).
cnf(c_3441,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolve,[status(thm)],[c_241,c_106]) ).
cnf(c_788,plain,
aSet0(xS),
inference(resolve,[status(thm)],[c_138,c_3441]) ).
cnf(c_3442,plain,
( aElementOf0(A,xS)
| ~ aElementOf0(A,xO)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_298,c_107]) ).
cnf(c_1422,plain,
( aElementOf0(A,xS)
| ~ aElementOf0(A,xO) ),
inference(resolve,[status(thm)],[c_788,c_3442]) ).
cnf(c_3443,plain,
( sdtlseqdt0(xp,A)
| ~ aElementOf0(A,xQ)
| slcrc0 = xQ
| ~ aSubsetOf0(xQ,szNzAzT0) ),
inference(resolve,[status(thm)],[c_305,c_169]) ).
cnf(c_3444,plain,
( sdtlseqdt0(xp,A)
| ~ aElementOf0(A,xQ)
| xQ = slcrc0
| ~ aSubsetOf0(xQ,szNzAzT0) ),
inference(copy,[status(thm)],[c_3443]) ).
cnf(c_3445,plain,
( sdtlseqdt0(xp,A)
| ~ aElementOf0(A,xQ)
| xQ = slcrc0 ),
inference(resolve,[status(thm)],[c_302,c_3444]) ).
cnf(c_1531,plain,
( sdtlseqdt0(xp,A)
| ~ aElementOf0(A,xQ) ),
inference(resolve,[status(thm)],[c_301,c_3445]) ).
cnf(c_3446,plain,
( sdtlseqdt0(A,xp)
| szmzizndt0(sdtlpdtrp0(xN,xm)) != A
| slcrc0 = sdtlpdtrp0(xN,xm)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(resolve,[status(thm)],[c_328,c_169]) ).
cnf(c_3447,plain,
( sdtlseqdt0(A,xp)
| xx != A
| slcrc0 = sdtlpdtrp0(xN,xm)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(paramod,[status(thm)],[c_325,c_3446]) ).
cnf(c_3448,plain,
( sdtlseqdt0(A,xp)
| xx != A
| sdtlpdtrp0(xN,xm) = slcrc0
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(copy,[status(thm)],[c_3447]) ).
cnf(c_3449,plain,
( sdtlseqdt0(A,xp)
| xx != A
| sdtlpdtrp0(xN,xm) = slcrc0 ),
inference(resolve,[status(thm)],[c_330,c_3448]) ).
cnf(c_2223,plain,
( sdtlseqdt0(A,xp)
| xx != A ),
inference(resolve,[status(thm)],[c_331,c_3449]) ).
cnf(c_3206,plain,
aElementOf0(xp,xS),
inference(resolve,[status(thm)],[c_1422,c_310]) ).
cnf(c_3228,plain,
aElementOf0(xp,szNzAzT0),
inference(resolve,[status(thm)],[c_3206,c_787]) ).
cnf(c_3406,plain,
sdtlseqdt0(xp,xx),
inference(resolve,[status(thm)],[c_1531,c_329]) ).
cnf(c_3450,plain,
( xp = xx
| ~ sdtlseqdt0(xx,xp)
| ~ aElementOf0(xp,szNzAzT0)
| ~ aElementOf0(xx,szNzAzT0) ),
inference(resolve,[status(thm)],[c_3406,c_153]) ).
cnf(c_3451,plain,
( xp = xx
| ~ sdtlseqdt0(xx,xp)
| ~ aElementOf0(xp,szNzAzT0) ),
inference(resolve,[status(thm)],[c_320,c_3450]) ).
cnf(c_3452,plain,
( xp = xx
| ~ sdtlseqdt0(xx,xp) ),
inference(resolve,[status(thm)],[c_3228,c_3451]) ).
cnf(c_3411,negated_conjecture,
~ sdtlseqdt0(xx,xp),
inference(resolve,[status(thm)],[c_333,c_3452]) ).
cnf(c_3453,plain,
xx = szmzizndt0(sdtlpdtrp0(xN,xm)),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_3454,plain,
sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),xp),
inference(resolve,[status(thm)],[c_2223,c_3453]) ).
cnf(c_3455,plain,
sdtlseqdt0(xx,xp),
inference(paramod,[status(thm)],[c_325,c_3454]) ).
cnf(c_3439,plain,
$false,
inference(resolve,[status(thm)],[c_3411,c_3455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM624+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n003.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 03:31:24 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.36 % Process 1929763 was started by sandbox on n003,
% 0.07/0.36 % Sat Sep 26 03:31:24 2026
% 0.07/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.39
% 0.07/0.39 % From the command line: assign(max_seconds, 300).
% 4.06/0.97
% 4.06/0.97 % SZS status Theorem for theBenchmark
% 4.06/0.97
% 4.06/0.97 % Proof 1 at 0.36 (+ 0.12) seconds.
% 4.06/0.97 % Length of proof is 41.
% 4.06/0.97 % Level of proof is 7.
% 4.06/0.97 % Maximum clause weight is 26.000.
% 4.06/0.97 % Given clauses 389.
% 4.06/0.97
% 4.06/0.97 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------