%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM611+3 : 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 : n009.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:34 AM UTC 2026
% Result : Theorem 138.26s 19.24s
% Output : CNFRefutation 138.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 51 ( 21 unt; 0 def)
% Number of atoms : 119 ( 38 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 110 ( 42 ~; 39 |; 16 &)
% ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 25 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSubFSet,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('theBenchmark.p',mSubFSet) ).
fof(mSuccEquSucc,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)
=> W0 = W1 ) ),
file('theBenchmark.p',mSuccEquSucc) ).
fof(mCardNum,axiom,
! [W0] :
( aSet0(W0)
=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) ) ),
file('theBenchmark.p',mCardNum) ).
fof(mCardDiff,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aElementOf0(W1,W0)
& isFinite0(W0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ),
file('theBenchmark.p',mCardDiff) ).
fof(m__3533,axiom,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('theBenchmark.p',m__3533) ).
fof(m__5078,axiom,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,xO) )
& aSet0(xQ) ),
file('theBenchmark.p',m__5078) ).
fof(m__5147,axiom,
( xp = szmzizndt0(xQ)
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(xp,W0) )
& aElementOf0(xp,xQ) ),
file('theBenchmark.p',m__5147) ).
fof(m__5164,axiom,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(szmzizndt0(xQ),W0) )
& aSet0(xP) ),
file('theBenchmark.p',m__5164) ).
fof(m__5195,axiom,
( aSubsetOf0(xP,xQ)
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xQ) ) ),
file('theBenchmark.p',m__5195) ).
fof(m__,conjecture,
sbrdtbr0(xP) = xk,
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
sbrdtbr0(xP) != xk,
inference(assume_negation,[status(cth)],[m__]) ).
fof(m__3418,axiom,
aElementOf0(xK,szNzAzT0),
file('theBenchmark.p',m__3418) ).
cnf(c_519,plain,
aElementOf0(xK,szNzAzT0),
inference(clausify,[status(thm)],[m__3418]) ).
cnf(c_595,plain,
( sbrdtbr0(A) = szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B)))
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardDiff]) ).
cnf(c_596,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B))) = sbrdtbr0(A)
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(copy,[status(thm)],[c_595]) ).
cnf(c_600,plain,
( ~ isFinite0(A)
| aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_601,plain,
( isFinite0(A)
| ~ aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_616,plain,
( B = A
| szszuzczcdt0(B) != szszuzczcdt0(A)
| ~ aElementOf0(B,szNzAzT0)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mSuccEquSucc]) ).
cnf(c_649,plain,
( isFinite0(B)
| ~ aSubsetOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mSubFSet]) ).
cnf(c_667,plain,
aElementOf0(xk,szNzAzT0),
inference(clausify,[status(thm)],[m__3533]) ).
cnf(c_668,plain,
szszuzczcdt0(xk) = xK,
inference(clausify,[status(thm)],[m__3533]) ).
cnf(c_975,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_978,plain,
sbrdtbr0(xQ) = xK,
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_987,plain,
aElementOf0(xp,xQ),
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_989,plain,
szmzizndt0(xQ) = xp,
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_990,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_998,plain,
sdtmndt0(xQ,szmzizndt0(xQ)) = xP,
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_999,plain,
sdtmndt0(xQ,xp) = xP,
inference(paramod,[status(thm)],[c_989,c_998]) ).
cnf(c_1002,plain,
aSubsetOf0(xP,xQ),
inference(clausify,[status(thm)],[m__5195]) ).
cnf(c_1005,negated_conjecture,
sbrdtbr0(xP) != xk,
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_22908,plain,
( xk = A
| szszuzczcdt0(xk) != szszuzczcdt0(A)
| ~ aElementOf0(A,szNzAzT0) ),
inference(resolve,[status(thm)],[c_667,c_616]) ).
cnf(c_22909,plain,
( xk = A
| xK != szszuzczcdt0(A)
| ~ aElementOf0(A,szNzAzT0) ),
inference(paramod,[status(thm)],[c_668,c_22908]) ).
cnf(c_5437,plain,
( xk = A
| szszuzczcdt0(A) != xK
| ~ aElementOf0(A,szNzAzT0) ),
inference(copy,[status(thm)],[c_22909]) ).
cnf(c_22910,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_978,c_601]) ).
cnf(c_22911,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolve,[status(thm)],[c_975,c_22910]) ).
cnf(c_6097,plain,
isFinite0(xQ),
inference(resolve,[status(thm)],[c_519,c_22911]) ).
cnf(c_22912,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp))) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_987,c_596]) ).
cnf(c_22913,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_999,c_22912]) ).
cnf(c_22914,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_978,c_22913]) ).
cnf(c_22915,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_975,c_22914]) ).
cnf(c_6236,plain,
szszuzczcdt0(sbrdtbr0(xP)) = xK,
inference(resolve,[status(thm)],[c_6097,c_22915]) ).
cnf(c_22916,plain,
( isFinite0(xP)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_1002,c_649]) ).
cnf(c_22917,plain,
( isFinite0(xP)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_975,c_22916]) ).
cnf(c_6295,plain,
isFinite0(xP),
inference(resolve,[status(thm)],[c_6097,c_22917]) ).
cnf(c_22918,plain,
( aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ aSet0(xP) ),
inference(resolve,[status(thm)],[c_6295,c_600]) ).
cnf(c_6552,plain,
aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(resolve,[status(thm)],[c_990,c_22918]) ).
cnf(c_22919,plain,
( xk = sbrdtbr0(xP)
| szszuzczcdt0(sbrdtbr0(xP)) != xK ),
inference(resolve,[status(thm)],[c_5437,c_6552]) ).
cnf(c_22920,plain,
( xk = sbrdtbr0(xP)
| xK != xK ),
inference(paramod,[status(thm)],[c_6236,c_22919]) ).
cnf(c_22921,plain,
( sbrdtbr0(xP) = xk
| xK != xK ),
inference(copy,[status(thm)],[c_22920]) ).
cnf(c_22922,plain,
sbrdtbr0(xP) = xk,
inference(copy,[status(thm)],[c_22921]) ).
cnf(c_22907,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1005,c_22922]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM611+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.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 03:26:44 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 3267979 was started by sandbox on n009,
% 0.12/0.36 % Sat Sep 26 03:26:44 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.30/0.61
% 0.30/0.61 % From the command line: assign(max_seconds, 300).
% 138.26/19.24
% 138.26/19.24 % given #500 (I,wt=17): 911 -aElementOf0(A,szNzAzT0) | -aElementOf0(B,f39(A)) | aElementOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) # tptp_name(m__4411). [clausify(83)].
% 138.26/19.24
% 138.26/19.24 % given #1000 (I,wt=65): 1618 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(E,sdtlcdtrc0(C,szDzozmdt0(C))) | aElementOf0(f25(A,B,C,E),szDzozmdt0(C)) | -iLess0(A,xK) | -aElementOf0(F,slbdtsldtrb0(f28(A,B,C),A)) | f27(A,B,C) = sdtlpdtrp0(C,F). [copy(1617),flip(m)].
% 138.26/19.24
% 138.26/19.24 % given #1500 (I,wt=61): 2453 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(E,sdtlcdtrc0(C,szDzozmdt0(C))) | sdtlpdtrp0(C,f25(A,B,C,E)) = E | -iLess0(A,xK) | aSubsetOf0(f28(A,B,C),B). [resolve(298,a,145,e)].
% 138.26/19.24
% 138.26/19.24 % given #2000 (I,wt=77): 3175 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | aSubsetOf0(f23(A,B,C),B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | sdtlpdtrp0(C,f25(A,B,C,D)) = D | -iLess0(A,xK) | -aSubsetOf0(E,f28(A,B,C)) | sbrdtbr0(E) != A | f27(A,B,C) = sdtlpdtrp0(C,E). [copy(3174),flip(o)].
% 138.26/19.24
% 138.26/19.24 % given #2500 (I,wt=72): 3694 -aSet0(f23(A,szDzozmdt0(B),B)) | -aElementOf0(f24(A,szDzozmdt0(B),B),szDzozmdt0(B)) | sbrdtbr0(f23(A,szDzozmdt0(B),B)) != A | -aElementOf0(f23(A,szDzozmdt0(B),B),szDzozmdt0(B)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(szDzozmdt0(B),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | -aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | aElementOf0(f25(A,szDzozmdt0(B),B,C),szDzozmdt0(B)) | -iLess0(A,xK) | -aElementOf0(f25(A,szDzozmdt0(B),B,C),f28(A,szDzozmdt0(B),B)). [factor(1921,j,m)].
% 138.26/19.24
% 138.26/19.24 % given #3000 (I,wt=104): 4204 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(C,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -aElementOf0(D,szDzozmdt0(B)) | sdtlpdtrp0(B,D) != C | -iLess0(A,xK) | -aSubsetOf0(E,f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | sbrdtbr0(E) != A | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,E). [factor(2525,e,k)].
% 138.26/19.24
% 138.26/19.24 % given #3500 (I,wt=67): 4715 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | aSubsetOf0(f23(A,B,C),B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | -aElementOf0(E,szDzozmdt0(C)) | sdtlpdtrp0(C,E) != D | -iLess0(A,xK) | -aElementOf0(f22(A,B),f28(A,B,C)). [factor(3169,g,o)].
% 138.26/19.24
% 138.26/19.24 % given #4000 (I,wt=129): 5221 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | aElementOf0(f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(C,szDzozmdt0(B)) | f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,C) | -iLess0(A,xK) | sbrdtbr0(sdtlcdtrc0(B,szDzozmdt0(B))) != A | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,sdtlcdtrc0(B,szDzozmdt0(B))). [factor(5064,j,n),flip(l)].
% 138.26/19.24
% 138.26/19.24 % given #4500 (A,wt=11): 5328 -aElementOf0(A,szNzAzT0) | slbdtrb0(A) != szNzAzT0 | sdtlseqdt0(szszuzczcdt0(sz00),A). [resolve(619,a,580,c)].
% 138.26/19.24
% 138.26/19.24 % given #5000 (T,wt=4): 20909 aElement0(szszuzczcdt0(szszuzczcdt0(c1))). [resolve(13871,a,660,b),unit_del(a,621)].
% 138.26/19.24
% 138.26/19.24 % SZS status Theorem for theBenchmark
% 138.26/19.24
% 138.26/19.24 % Proof 1 at 17.37 (+ 0.93) seconds.
% 138.26/19.24 % Length of proof is 34.
% 138.26/19.24 % Level of proof is 5.
% 138.26/19.24 % Maximum clause weight is 15.000.
% 138.26/19.24 % Given clauses 5130.
% 138.26/19.24
% 138.26/19.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------