%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM548+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 : n011.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:21 AM UTC 2026
% Result : Theorem 2.05s 0.67s
% Output : CNFRefutation 2.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 7
% Syntax : Number of formulae : 30 ( 13 unt; 0 def)
% Number of atoms : 72 ( 10 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 74 ( 32 ~; 28 |; 6 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 26 ( 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(mCardNum,axiom,
! [W0] :
( aSet0(W0)
=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) ) ),
file('theBenchmark.p',mCardNum) ).
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__2202_02,axiom,
( xk != sz00
& aSet0(xT)
& aSet0(xS) ),
file('theBenchmark.p',m__2202_02) ).
fof(m__,conjecture,
isFinite0(xQ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ isFinite0(xQ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_61,negated_conjecture,
~ isFinite0(xQ),
inference(clausify,[status(thm)],[m___neg]) ).
fof(m__2270,axiom,
aElementOf0(xQ,slbdtsldtrb0(xS,xk)),
file('theBenchmark.p',m__2270) ).
cnf(c_62,plain,
aElementOf0(xQ,slbdtsldtrb0(xS,xk)),
inference(clausify,[status(thm)],[m__2270]) ).
cnf(c_68,plain,
aSet0(xS),
inference(clausify,[status(thm)],[m__2202_02]) ).
fof(m__2202,axiom,
aElementOf0(xk,szNzAzT0),
file('theBenchmark.p',m__2202) ).
cnf(c_69,plain,
aElementOf0(xk,szNzAzT0),
inference(clausify,[status(thm)],[m__2202]) ).
cnf(c_77,plain,
( sbrdtbr0(D) = B
| ~ aElementOf0(D,C)
| slbdtsldtrb0(A,B) != C
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSel]) ).
cnf(c_78,plain,
( aSubsetOf0(D,A)
| ~ aElementOf0(D,C)
| slbdtsldtrb0(A,B) != C
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSel]) ).
cnf(c_127,plain,
( isFinite0(A)
| ~ aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_178,plain,
( aSet0(B)
| ~ aSubsetOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSub]) ).
cnf(c_241,plain,
( sbrdtbr0(C) = B
| ~ aElementOf0(C,slbdtsldtrb0(A,B))
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_77]) ).
cnf(c_250,plain,
( aSubsetOf0(C,A)
| ~ aElementOf0(C,slbdtsldtrb0(A,B))
| ~ aElementOf0(B,szNzAzT0)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_78]) ).
cnf(c_638,plain,
( aSet0(A)
| ~ aSubsetOf0(A,xS) ),
inference(resolve,[status(thm)],[c_178,c_68]) ).
cnf(c_2240,plain,
( sbrdtbr0(xQ) = xk
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_241,c_62]) ).
cnf(c_2241,plain,
( sbrdtbr0(xQ) = xk
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolve,[status(thm)],[c_68,c_2240]) ).
cnf(c_2040,plain,
sbrdtbr0(xQ) = xk,
inference(resolve,[status(thm)],[c_69,c_2241]) ).
cnf(c_2242,plain,
( isFinite0(xQ)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_2040,c_127]) ).
cnf(c_2243,plain,
( isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_69,c_2242]) ).
cnf(c_2072,negated_conjecture,
~ aSet0(xQ),
inference(resolve,[status(thm)],[c_61,c_2243]) ).
cnf(c_2244,plain,
( aSubsetOf0(xQ,xS)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_250,c_62]) ).
cnf(c_2245,plain,
( aSubsetOf0(xQ,xS)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolve,[status(thm)],[c_68,c_2244]) ).
cnf(c_2221,plain,
aSubsetOf0(xQ,xS),
inference(resolve,[status(thm)],[c_69,c_2245]) ).
cnf(c_2246,plain,
aSet0(xQ),
inference(resolve,[status(thm)],[c_2221,c_638]) ).
cnf(c_2239,plain,
$false,
inference(resolve,[status(thm)],[c_2072,c_2246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM548+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.07/0.36 % Computer : n011.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:11:14 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 3658579 was started by sandbox2 on n011,
% 0.07/0.37 % Sat Sep 26 03:11:14 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).
% 2.05/0.67
% 2.05/0.67 % SZS status Theorem for theBenchmark
% 2.05/0.67
% 2.05/0.67 % Proof 1 at 0.20 (+ 0.07) seconds.
% 2.05/0.67 % Length of proof is 20.
% 2.05/0.67 % Level of proof is 5.
% 2.05/0.67 % Maximum clause weight is 21.000.
% 2.05/0.67 % Given clauses 326.
% 2.05/0.67
% 2.05/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------