%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM549+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:22 AM UTC 2026
% Result : Theorem 0.63s 0.50s
% Output : CNFRefutation 0.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 32 ( 13 unt; 0 def)
% Number of atoms : 74 ( 29 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 71 ( 29 ~; 24 |; 13 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-1 aty)
% Number of variables : 23 ( 0 sgn 12 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefEmp,axiom,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('theBenchmark.p',mDefEmp) ).
fof(mCardEmpty,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
file('theBenchmark.p',mCardEmpty) ).
fof(m__2202_02,axiom,
( xk != sz00
& aSet0(xT)
& aSet0(xS) ),
file('theBenchmark.p',m__2202_02) ).
fof(m__2291,axiom,
( sbrdtbr0(xQ) = xk
& isFinite0(xQ)
& aSet0(xQ) ),
file('theBenchmark.p',m__2291) ).
fof(m__,conjecture,
? [W0] :
( aElementOf0(W0,xQ)
& aElement0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( aElementOf0(W0,xQ)
& aElement0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_62,negated_conjecture,
( ~ aElementOf0(A,xQ)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_63,plain,
sbrdtbr0(xQ) = xk,
inference(clausify,[status(thm)],[m__2291]) ).
cnf(c_64,plain,
xk = sbrdtbr0(xQ),
inference(copy,[status(thm)],[c_63]) ).
cnf(c_66,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__2291]) ).
cnf(c_74,plain,
xk != sz00,
inference(clausify,[status(thm)],[m__2202_02]) ).
cnf(c_75,plain,
sbrdtbr0(xQ) != sz00,
inference(paramod,[status(thm)],[c_64,c_74]) ).
fof(mSegZero,axiom,
slbdtrb0(sz00) = slcrc0,
file('theBenchmark.p',mSegZero) ).
cnf(c_98,plain,
slbdtrb0(sz00) = slcrc0,
inference(clausify,[status(thm)],[mSegZero]) ).
cnf(c_99,plain,
slcrc0 = slbdtrb0(sz00),
inference(copy,[status(thm)],[c_98]) ).
cnf(c_132,plain,
( slcrc0 != A
| sbrdtbr0(A) = sz00
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardEmpty]) ).
cnf(c_133,plain,
( slbdtrb0(sz00) != A
| sbrdtbr0(A) = sz00
| ~ aSet0(A) ),
inference(paramod,[status(thm)],[c_99,c_132]) ).
fof(nnf_5,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| slcrc0 = W0 )
& ( ( ! [X0] : ~ aElementOf0(X0,W0)
& aSet0(W0) )
| slcrc0 != W0 ) ),
inference(fof_nnf,[status(thm)],[mDefEmp]) ).
fof(sk_mDefEmp_sk,plain,
! [W0] :
( ( aElementOf0(sK0(W0),W0)
| ~ aSet0(W0)
| slcrc0 = W0 )
& ( ( ! [X0] : ~ aElementOf0(X0,W0)
& aSet0(W0) )
| slcrc0 != W0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_5]) ).
fof(sk_mDefEmp,plain,
( ! [VAR_0] :
( aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0)
| slcrc0 = VAR_0 )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,VAR_0)
| slcrc0 != VAR_0 )
& ! [VAR_0] :
( aSet0(VAR_0)
| slcrc0 != VAR_0 ) ),
inference(cnf_transformation,[status(thm)],[sk_mDefEmp_sk]) ).
cnf(c_194,plain,
( aElementOf0(sK0(A),A)
| ~ aSet0(A)
| slcrc0 = A ),
inference(split_conjunct,[status(thm)],[sk_mDefEmp]) ).
cnf(c_195,plain,
( aElementOf0(sK0(A),A)
| ~ aSet0(A)
| slbdtrb0(sz00) = A ),
inference(paramod,[status(thm)],[c_99,c_194]) ).
cnf(c_200,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_687,plain,
( slbdtrb0(sz00) != xQ
| sbrdtbr0(xQ) = sz00 ),
inference(resolve,[status(thm)],[c_133,c_66]) ).
cnf(c_265,plain,
slbdtrb0(sz00) != xQ,
inference(resolve,[status(thm)],[c_75,c_687]) ).
cnf(c_688,plain,
( aElementOf0(sK0(xQ),xQ)
| slbdtrb0(sz00) = xQ ),
inference(resolve,[status(thm)],[c_195,c_66]) ).
cnf(c_375,plain,
aElementOf0(sK0(xQ),xQ),
inference(resolve,[status(thm)],[c_265,c_688]) ).
cnf(c_689,plain,
( aElement0(sK0(xQ))
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_375,c_200]) ).
cnf(c_674,plain,
aElement0(sK0(xQ)),
inference(resolve,[status(thm)],[c_66,c_689]) ).
cnf(c_690,negated_conjecture,
~ aElement0(sK0(xQ)),
inference(resolve,[status(thm)],[c_375,c_62]) ).
cnf(c_686,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_674,c_690]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM549+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.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 03:11:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.15/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.38 % Process 1815027 was started by sandbox2 on n013,
% 0.15/0.38 % Sat Sep 26 03:11:06 2026
% 0.15/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.39
% 0.15/0.39 % From the command line: assign(max_seconds, 300).
% 0.63/0.50
% 0.63/0.50 % SZS status Theorem for theBenchmark
% 0.63/0.50
% 0.63/0.50 % Proof 1 at 0.06 (+ 0.02) seconds.
% 0.63/0.50 % Length of proof is 23.
% 0.63/0.50 % Level of proof is 7.
% 0.63/0.50 % Maximum clause weight is 10.000.
% 0.63/0.50 % Given clauses 180.
% 0.63/0.50
% 0.63/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------