%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM605+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 : 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:32 AM UTC 2026
% Result : Theorem 31.70s 5.22s
% Output : CNFRefutation 31.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 16 ( 9 unt; 0 def)
% Number of atoms : 29 ( 17 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 24 ( 11 ~; 4 |; 6 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 5 ( 0 sgn 2 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mCardEmpty,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
file('theBenchmark.p',mCardEmpty) ).
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__,conjecture,
~ ( xQ = slcrc0
& ~ ? [W0] : aElementOf0(W0,xQ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ~ ( xQ = slcrc0
& ~ ? [W0] : aElementOf0(W0,xQ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_1437,negated_conjecture,
xQ = slcrc0,
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_1442,plain,
sbrdtbr0(xQ) = xK,
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_1443,plain,
sbrdtbr0(slcrc0) = xK,
inference(paramod,[status(thm)],[c_1437,c_1442]) ).
cnf(c_1447,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_1448,plain,
aSet0(slcrc0),
inference(paramod,[status(thm)],[c_1437,c_1447]) ).
fof(m__3520,axiom,
xK != sz00,
file('theBenchmark.p',m__3520) ).
cnf(c_1651,plain,
xK != sz00,
inference(clausify,[status(thm)],[m__3520]) ).
cnf(c_1954,plain,
( slcrc0 != A
| sbrdtbr0(A) = sz00
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardEmpty]) ).
cnf(c_8654,plain,
( slcrc0 != slcrc0
| sbrdtbr0(slcrc0) = sz00 ),
inference(resolve,[status(thm)],[c_1954,c_1448]) ).
cnf(c_8655,plain,
( slcrc0 != slcrc0
| xK = sz00 ),
inference(paramod,[status(thm)],[c_1443,c_8654]) ).
cnf(c_8656,plain,
xK = sz00,
inference(copy,[status(thm)],[c_8655]) ).
cnf(c_8653,plain,
$false,
inference(resolve,[status(thm)],[c_1651,c_8656]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM605+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.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Sat Sep 26 03:25:43 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.37 % Process 3678598 was started by sandbox on n011,
% 0.13/0.37 % Sat Sep 26 03:25:43 2026
% 0.13/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.33/0.62
% 0.33/0.62 % From the command line: assign(max_seconds, 300).
% 31.70/5.22
% 31.70/5.22 % given #500 (I,wt=40): 1385 szDzozmdt0(A) != slbdtsldtrb0(B,C) | -aElementOf0(C,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(A) | aElementOf0(D,sdtlcdtrc0(A,szDzozmdt0(A))) | -aElementOf0(E,szDzozmdt0(A)) | sdtlpdtrp0(A,E) != D | -iLess0(C,xK) | aElementOf0(f27(C,B,A),xT). [resolve(95,a,131,e)].
% 31.70/5.22
% 31.70/5.22 % given #1000 (I,wt=13): 1937 -aElementOf0(A,szNzAzT0) | slbdtrb0(A) != B | -aElementOf0(C,B) | aElementOf0(C,szNzAzT0) # tptp_name(mDefSeg). [clausify(48)].
% 31.70/5.22
% 31.70/5.22 % SZS status Theorem for theBenchmark
% 31.70/5.22
% 31.70/5.22 % Proof 1 at 4.38 (+ 0.15) seconds.
% 31.70/5.22 % Length of proof is 11.
% 31.70/5.22 % Level of proof is 3.
% 31.70/5.22 % Maximum clause weight is 9.000.
% 31.70/5.22 % Given clauses 1016.
% 31.70/5.22
% 31.70/5.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------