%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM612+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 : n019.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 4.72s 1.08s
% Output : CNFRefutation 4.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 14
% Syntax : Number of formulae : 58 ( 24 unt; 0 def)
% Number of atoms : 123 ( 30 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 115 ( 50 ~; 42 |; 11 &)
% ( 4 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 29 ( 0 sgn 12 !; 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(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(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__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,
( aElementOf0(sbrdtbr0(xP),szNzAzT0)
& szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( aElementOf0(sbrdtbr0(xP),szNzAzT0)
& szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ) ),
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_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_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_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,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| sbrdtbr0(xQ) != szszuzczcdt0(sbrdtbr0(xP)) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_308,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| szszuzczcdt0(sbrdtbr0(xP)) != sbrdtbr0(xQ) ),
inference(copy,[status(thm)],[c_307]) ).
cnf(c_487,plain,
( sbrdtbr0(C) = B
| ~ aElementOf0(C,slbdtsldtrb0(A,B))
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_191]) ).
cnf(c_9063,plain,
( aSet0(xQ)
| ~ aSet0(xO) ),
inference(resolve,[status(thm)],[c_294,c_101]) ).
cnf(c_1445,plain,
aSet0(xQ),
inference(resolve,[status(thm)],[c_286,c_9063]) ).
cnf(c_1547,plain,
( ~ isFinite0(xP)
| aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(resolve,[status(thm)],[c_300,c_154]) ).
cnf(c_9064,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp))) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_303,c_159]) ).
cnf(c_9065,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_302,c_9064]) ).
cnf(c_1631,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_1445,c_9065]) ).
cnf(c_9066,plain,
( isFinite0(xP)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_305,c_105]) ).
cnf(c_1682,plain,
( isFinite0(xP)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_1445,c_9066]) ).
cnf(c_2077,plain,
( isFinite0(xQ)
| ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0) ),
inference(resolve,[status(thm)],[c_1445,c_153]) ).
cnf(c_9067,plain,
( sbrdtbr0(xQ) = xK
| ~ aElementOf0(xK,szNzAzT0)
| ~ aSet0(xO) ),
inference(resolve,[status(thm)],[c_487,c_293]) ).
cnf(c_9068,plain,
( sbrdtbr0(xQ) = xK
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolve,[status(thm)],[c_286,c_9067]) ).
cnf(c_9014,plain,
sbrdtbr0(xQ) = xK,
inference(resolve,[status(thm)],[c_235,c_9068]) ).
cnf(c_9069,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(paramod,[status(thm)],[c_9014,c_2077]) ).
cnf(c_9022,plain,
isFinite0(xQ),
inference(resolve,[status(thm)],[c_235,c_9069]) ).
cnf(c_9070,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ) ),
inference(paramod,[status(thm)],[c_9014,c_1631]) ).
cnf(c_9029,plain,
szszuzczcdt0(sbrdtbr0(xP)) = xK,
inference(resolve,[status(thm)],[c_9022,c_9070]) ).
cnf(c_9071,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| xK != sbrdtbr0(xQ) ),
inference(paramod,[status(thm)],[c_9029,c_308]) ).
cnf(c_9072,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| xK != xK ),
inference(paramod,[status(thm)],[c_9014,c_9071]) ).
cnf(c_9034,negated_conjecture,
~ aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(copy,[status(thm)],[c_9072]) ).
cnf(c_9050,plain,
isFinite0(xP),
inference(resolve,[status(thm)],[c_9022,c_1682]) ).
cnf(c_9073,negated_conjecture,
~ isFinite0(xP),
inference(resolve,[status(thm)],[c_9034,c_1547]) ).
cnf(c_9062,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_9050,c_9073]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM612+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n019.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % 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 03:27:03 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 292463 was started by sandbox2 on n019,
% 0.12/0.36 % Sat Sep 26 03:27:03 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 4.72/1.08
% 4.72/1.08 % given #500 (T,wt=11): 3824 -aSubsetOf0(xS,xQ) | aSubsetOf0(xO,xQ). [resolve(1402,a,1445,a)].
% 4.72/1.08
% 4.72/1.08 % SZS status Theorem for theBenchmark
% 4.72/1.08
% 4.72/1.08 % Proof 1 at 0.51 (+ 0.14) seconds.
% 4.72/1.08 % Length of proof is 41.
% 4.72/1.08 % Level of proof is 7.
% 4.72/1.08 % Maximum clause weight is 35.000.
% 4.72/1.08 % Given clauses 765.
% 4.72/1.08
% 4.72/1.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------