%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM611+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 : 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 : Sun Sep 27 08:17:33 AM UTC 2026
% Result : Theorem 27.25s 4.40s
% Output : CNFRefutation 27.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 20
% Syntax : Number of formulae : 91 ( 38 unt; 0 def)
% Number of atoms : 206 ( 50 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 196 ( 81 ~; 79 |; 15 &)
% ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-2 aty)
% Number of variables : 55 ( 0 sgn 21 !; 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(mSubFSet,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('theBenchmark.p',mSubFSet) ).
fof(mNatNSucc,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> W0 != szszuzczcdt0(W0) ),
file('theBenchmark.p',mNatNSucc) ).
fof(mLessSucc,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(W0,szszuzczcdt0(W0)) ),
file('theBenchmark.p',mLessSucc) ).
fof(mLessASymm,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLessASymm) ).
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(mDefSeg,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) ) ),
file('theBenchmark.p',mDefSeg) ).
fof(mSegSucc,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))
<=> ( W0 = W1
| aElementOf0(W0,slbdtrb0(W1)) ) ) ),
file('theBenchmark.p',mSegSucc) ).
fof(mDefSel,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aSet0(W0) )
=> ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
file('theBenchmark.p',mDefSel) ).
fof(m__3533,axiom,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('theBenchmark.p',m__3533) ).
fof(m__4891,axiom,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('theBenchmark.p',m__4891) ).
fof(m__5093,axiom,
( xQ != slcrc0
& aSubsetOf0(xQ,xO) ),
file('theBenchmark.p',m__5093) ).
fof(m__5164,axiom,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& aSet0(xP) ),
file('theBenchmark.p',m__5164) ).
fof(m__,conjecture,
sbrdtbr0(xP) = xk,
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
sbrdtbr0(xP) != xk,
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_101,plain,
( aSet0(B)
| ~ aSubsetOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSub]) ).
cnf(c_105,plain,
( isFinite0(B)
| ~ aSubsetOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mSubFSet]) ).
cnf(c_141,plain,
( szszuzczcdt0(A) != A
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mNatNSucc]) ).
cnf(c_146,plain,
( sdtlseqdt0(A,szszuzczcdt0(A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mLessSucc]) ).
cnf(c_148,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aElementOf0(B,szNzAzT0)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mLessASymm]) ).
cnf(c_153,plain,
( isFinite0(A)
| ~ aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_154,plain,
( ~ isFinite0(A)
| aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_158,plain,
( sbrdtbr0(A) = szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B)))
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardDiff]) ).
cnf(c_159,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B))) = sbrdtbr0(A)
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(copy,[status(thm)],[c_158]) ).
cnf(c_174,plain,
( sdtlseqdt0(szszuzczcdt0(C),A)
| ~ aElementOf0(C,B)
| slbdtrb0(A) != B
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mDefSeg]) ).
cnf(c_181,plain,
( B = A
| aElementOf0(A,slbdtrb0(B))
| ~ aElementOf0(A,slbdtrb0(szszuzczcdt0(B)))
| ~ aElementOf0(B,szNzAzT0)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mSegSucc]) ).
cnf(c_183,plain,
( B != A
| aElementOf0(A,slbdtrb0(szszuzczcdt0(B)))
| ~ aElementOf0(B,szNzAzT0)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[mSegSucc]) ).
cnf(c_191,plain,
( sbrdtbr0(D) = B
| ~ aElementOf0(D,C)
| slbdtsldtrb0(A,B) != C
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSel]) ).
fof(m__3418,axiom,
aElementOf0(xK,szNzAzT0),
file('theBenchmark.p',m__3418) ).
cnf(c_235,plain,
aElementOf0(xK,szNzAzT0),
inference(clausify,[status(thm)],[m__3418]) ).
cnf(c_248,plain,
aElementOf0(xk,szNzAzT0),
inference(clausify,[status(thm)],[m__3533]) ).
cnf(c_249,plain,
szszuzczcdt0(xk) = xK,
inference(clausify,[status(thm)],[m__3533]) ).
cnf(c_286,plain,
aSet0(xO),
inference(clausify,[status(thm)],[m__4891]) ).
fof(m__5078,axiom,
aElementOf0(xQ,slbdtsldtrb0(xO,xK)),
file('theBenchmark.p',m__5078) ).
cnf(c_293,plain,
aElementOf0(xQ,slbdtsldtrb0(xO,xK)),
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_294,plain,
aSubsetOf0(xQ,xO),
inference(clausify,[status(thm)],[m__5093]) ).
fof(m__5147,axiom,
xp = szmzizndt0(xQ),
file('theBenchmark.p',m__5147) ).
cnf(c_298,plain,
xp = szmzizndt0(xQ),
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_299,plain,
szmzizndt0(xQ) = xp,
inference(copy,[status(thm)],[c_298]) ).
cnf(c_300,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_301,plain,
sdtmndt0(xQ,szmzizndt0(xQ)) = xP,
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_302,plain,
sdtmndt0(xQ,xp) = xP,
inference(paramod,[status(thm)],[c_299,c_301]) ).
fof(m__5173,axiom,
aElementOf0(xp,xQ),
file('theBenchmark.p',m__5173) ).
cnf(c_303,plain,
aElementOf0(xp,xQ),
inference(clausify,[status(thm)],[m__5173]) ).
fof(m__5195,axiom,
aSubsetOf0(xP,xQ),
file('theBenchmark.p',m__5195) ).
cnf(c_305,plain,
aSubsetOf0(xP,xQ),
inference(clausify,[status(thm)],[m__5195]) ).
cnf(c_307,negated_conjecture,
sbrdtbr0(xP) != xk,
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_29584,plain,
( A != A
| aElementOf0(A,slbdtrb0(szszuzczcdt0(A)))
| ~ aElementOf0(A,szNzAzT0) ),
inference(factor,[status(thm)],[c_183]) ).
cnf(c_324,plain,
( aElementOf0(A,slbdtrb0(szszuzczcdt0(A)))
| ~ aElementOf0(A,szNzAzT0) ),
inference(copy,[status(thm)],[c_29584]) ).
cnf(c_452,plain,
( sdtlseqdt0(szszuzczcdt0(B),A)
| ~ aElementOf0(B,slbdtrb0(A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(xxres,[status(thm)],[c_174]) ).
cnf(c_480,plain,
( sbrdtbr0(C) = B
| ~ aElementOf0(C,slbdtsldtrb0(A,B))
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_191]) ).
cnf(c_29585,plain,
( xk = A
| aElementOf0(A,slbdtrb0(xk))
| ~ aElementOf0(A,slbdtrb0(szszuzczcdt0(xk)))
| ~ aElementOf0(A,szNzAzT0) ),
inference(resolve,[status(thm)],[c_248,c_181]) ).
cnf(c_844,plain,
( xk = A
| aElementOf0(A,slbdtrb0(xk))
| ~ aElementOf0(A,slbdtrb0(xK))
| ~ aElementOf0(A,szNzAzT0) ),
inference(paramod,[status(thm)],[c_249,c_29585]) ).
cnf(c_29586,plain,
sdtlseqdt0(xk,szszuzczcdt0(xk)),
inference(resolve,[status(thm)],[c_248,c_146]) ).
cnf(c_869,plain,
sdtlseqdt0(xk,xK),
inference(paramod,[status(thm)],[c_249,c_29586]) ).
cnf(c_29587,plain,
szszuzczcdt0(xk) != xk,
inference(resolve,[status(thm)],[c_248,c_141]) ).
cnf(c_29588,plain,
xK != xk,
inference(paramod,[status(thm)],[c_249,c_29587]) ).
cnf(c_876,plain,
xk != xK,
inference(copy,[status(thm)],[c_29588]) ).
cnf(c_29589,plain,
( aSet0(xQ)
| ~ aSet0(xO) ),
inference(resolve,[status(thm)],[c_294,c_101]) ).
cnf(c_1280,plain,
aSet0(xQ),
inference(resolve,[status(thm)],[c_286,c_29589]) ).
cnf(c_1369,plain,
( ~ isFinite0(xP)
| aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(resolve,[status(thm)],[c_300,c_154]) ).
cnf(c_29590,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp))) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_303,c_159]) ).
cnf(c_29591,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_302,c_29590]) ).
cnf(c_1445,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_1280,c_29591]) ).
cnf(c_29592,plain,
( isFinite0(xP)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_305,c_105]) ).
cnf(c_1495,plain,
( isFinite0(xP)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_1280,c_29592]) ).
cnf(c_1869,plain,
( isFinite0(xQ)
| ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0) ),
inference(resolve,[status(thm)],[c_1280,c_153]) ).
cnf(c_29593,plain,
( xk = xK
| ~ sdtlseqdt0(xK,xk)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolve,[status(thm)],[c_869,c_148]) ).
cnf(c_29594,plain,
( xk = xK
| ~ sdtlseqdt0(xK,xk)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolve,[status(thm)],[c_235,c_29593]) ).
cnf(c_29595,plain,
( xk = xK
| ~ sdtlseqdt0(xK,xk) ),
inference(resolve,[status(thm)],[c_248,c_29594]) ).
cnf(c_2095,plain,
~ sdtlseqdt0(xK,xk),
inference(resolve,[status(thm)],[c_876,c_29595]) ).
cnf(c_29596,plain,
( sbrdtbr0(xQ) = xK
| ~ aElementOf0(xK,szNzAzT0)
| ~ aSet0(xO) ),
inference(resolve,[status(thm)],[c_480,c_293]) ).
cnf(c_29597,plain,
( sbrdtbr0(xQ) = xK
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolve,[status(thm)],[c_286,c_29596]) ).
cnf(c_11040,plain,
sbrdtbr0(xQ) = xK,
inference(resolve,[status(thm)],[c_235,c_29597]) ).
cnf(c_29598,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(paramod,[status(thm)],[c_11040,c_1869]) ).
cnf(c_11047,plain,
isFinite0(xQ),
inference(resolve,[status(thm)],[c_235,c_29598]) ).
cnf(c_29599,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ) ),
inference(paramod,[status(thm)],[c_11040,c_1445]) ).
cnf(c_11054,plain,
szszuzczcdt0(sbrdtbr0(xP)) = xK,
inference(resolve,[status(thm)],[c_11047,c_29599]) ).
cnf(c_11074,plain,
isFinite0(xP),
inference(resolve,[status(thm)],[c_11047,c_1495]) ).
cnf(c_11101,plain,
aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(resolve,[status(thm)],[c_11074,c_1369]) ).
cnf(c_29600,plain,
aElementOf0(sbrdtbr0(xP),slbdtrb0(szszuzczcdt0(sbrdtbr0(xP)))),
inference(resolve,[status(thm)],[c_11101,c_324]) ).
cnf(c_11991,plain,
aElementOf0(sbrdtbr0(xP),slbdtrb0(xK)),
inference(paramod,[status(thm)],[c_11054,c_29600]) ).
cnf(c_29601,plain,
( xk = sbrdtbr0(xP)
| aElementOf0(sbrdtbr0(xP),slbdtrb0(xk))
| ~ aElementOf0(sbrdtbr0(xP),slbdtrb0(xK)) ),
inference(resolve,[status(thm)],[c_844,c_11101]) ).
cnf(c_29602,plain,
( sbrdtbr0(xP) = xk
| aElementOf0(sbrdtbr0(xP),slbdtrb0(xk))
| ~ aElementOf0(sbrdtbr0(xP),slbdtrb0(xK)) ),
inference(copy,[status(thm)],[c_29601]) ).
cnf(c_29603,plain,
( sbrdtbr0(xP) = xk
| aElementOf0(sbrdtbr0(xP),slbdtrb0(xk)) ),
inference(resolve,[status(thm)],[c_11991,c_29602]) ).
cnf(c_29523,negated_conjecture,
aElementOf0(sbrdtbr0(xP),slbdtrb0(xk)),
inference(resolve,[status(thm)],[c_307,c_29603]) ).
cnf(c_29604,plain,
( sdtlseqdt0(szszuzczcdt0(sbrdtbr0(xP)),xk)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolve,[status(thm)],[c_29523,c_452]) ).
cnf(c_29605,plain,
( sdtlseqdt0(xK,xk)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramod,[status(thm)],[c_11054,c_29604]) ).
cnf(c_29606,plain,
sdtlseqdt0(xK,xk),
inference(resolve,[status(thm)],[c_248,c_29605]) ).
cnf(c_29583,plain,
$false,
inference(resolve,[status(thm)],[c_2095,c_29606]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM611+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.07/0.36 % Computer : n013.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Sat Sep 26 03:26:06 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.37 % Process 1834775 was started by sandbox2 on n013,
% 0.07/0.37 % Sat Sep 26 03:26:06 2026
% 0.07/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.07/0.38
% 0.07/0.38 % From the command line: assign(max_seconds, 300).
% 27.25/4.40
% 27.25/4.40 % given #500 (T,wt=8): 1469 aElementOf0(f25(xp),szNzAzT0). [resolve(304,a,289,a)].
% 27.25/4.40
% 27.25/4.40 % given #1000 (A,wt=12): 511 -aFunction0(A) | -aElement0(B) | aSet0(sdtlbdtrb0(A,B)). [xx_res(205,c)].
% 27.25/4.40
% 27.25/4.40 % given #1500 (F,wt=9): 18645 sdtmndt0(xS,xK) != slcrc0. [back_unit_del(13781),unit_del(a,18628)].
% 27.25/4.40
% 27.25/4.40 % given #2000 (W,wt=9): 25414 aSubsetOf0(slcrc0,slbdtsldtrb0(szNzAzT0,xk)). [resolve(24899,a,1615,a)].
% 27.25/4.40
% 27.25/4.40 % SZS status Theorem for theBenchmark
% 27.25/4.40
% 27.25/4.40 % Proof 1 at 2.81 (+ 1.11) seconds.
% 27.25/4.40 % Length of proof is 62.
% 27.25/4.40 % Level of proof is 9.
% 27.25/4.40 % Maximum clause weight is 24.000.
% 27.25/4.40 % Given clauses 2415.
% 27.25/4.40
% 27.25/4.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------