%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM590+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 : n005.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:30 AM UTC 2026
% Result : Theorem 47.98s 7.76s
% Output : CNFRefutation 47.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 16 ( 7 unt; 0 def)
% Number of atoms : 42 ( 3 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 37 ( 11 ~; 6 |; 14 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 10 ( 0 sgn 6 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__3671,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ),
file('theBenchmark.p',m__3671) ).
fof(m__4448_02,axiom,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [W0] :
( aElementOf0(W0,xY)
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(xY)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('theBenchmark.p',m__4448_02) ).
fof(m__,conjecture,
( aSubsetOf0(xY,szNzAzT0)
| ! [W0] :
( aElementOf0(W0,xY)
=> aElementOf0(W0,szNzAzT0) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( aSubsetOf0(xY,szNzAzT0)
| ! [W0] :
( aElementOf0(W0,xY)
=> aElementOf0(W0,szNzAzT0) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_690,plain,
( aElementOf0(B,szNzAzT0)
| ~ aElementOf0(B,sdtlpdtrp0(xN,A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__3671]) ).
fof(m__4448,axiom,
aElementOf0(xi,szNzAzT0),
file('theBenchmark.p',m__4448) ).
cnf(c_884,plain,
aElementOf0(xi,szNzAzT0),
inference(clausify,[status(thm)],[m__4448]) ).
cnf(c_889,plain,
( aElementOf0(A,sdtlpdtrp0(xN,xi))
| ~ aElementOf0(A,xY) ),
inference(clausify,[status(thm)],[m__4448_02]) ).
fof(nnf_84,plain,
( ~ aSubsetOf0(xY,szNzAzT0)
& ? [W0] :
( ~ aElementOf0(W0,szNzAzT0)
& aElementOf0(W0,xY) ) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg,plain,
( ~ aSubsetOf0(xY,szNzAzT0)
& ~ aElementOf0(sK0,szNzAzT0)
& aElementOf0(sK0,xY) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W0,sK0)],[nnf_84]) ).
cnf(c_894,negated_conjecture,
aElementOf0(sK0,xY),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_895,negated_conjecture,
~ aElementOf0(sK0,szNzAzT0),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_7168,plain,
aElementOf0(sK0,sdtlpdtrp0(xN,xi)),
inference(resolve,[status(thm)],[c_894,c_889]) ).
cnf(c_13258,plain,
( aElementOf0(sK0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolve,[status(thm)],[c_7168,c_690]) ).
cnf(c_13259,plain,
aElementOf0(sK0,szNzAzT0),
inference(resolve,[status(thm)],[c_884,c_13258]) ).
cnf(c_13257,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_895,c_13259]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM590+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n005.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sat Sep 26 03:21:46 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.43 % Process 1088339 was started by sandbox on n005,
% 0.17/0.43 % Sat Sep 26 03:21:46 2026
% 0.17/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.48/0.77
% 0.48/0.77 % From the command line: assign(max_seconds, 300).
% 47.98/7.76
% 47.98/7.76 % given #500 (I,wt=23): 885 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) # tptp_name(m__4448_02). [clausify(83)].
% 47.98/7.76
% 47.98/7.76 % given #1000 (I,wt=84): 1660 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | aSet0(f23(A,B,C)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | aElementOf0(f25(A,B,C,D),szDzozmdt0(C)) | -iLess0(A,xK) | -aSet0(E) | -aElementOf0(f29(A,B,C,E),f28(A,B,C)) | sbrdtbr0(E) != A | f27(A,B,C) = sdtlpdtrp0(C,E). [copy(1659),flip(n)].
% 47.98/7.76
% 47.98/7.76 % given #1500 (I,wt=79): 2437 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aElementOf0(f22(A,B),szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(E,sdtlcdtrc0(C,szDzozmdt0(C))) | sdtlpdtrp0(C,f25(A,B,C,E)) = E | -iLess0(A,xK) | aSet0(f28(A,B,C)). [resolve(280,a,192,f)].
% 47.98/7.76
% 47.98/7.76 % given #2000 (I,wt=94): 3161 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(E,sdtlcdtrc0(C,szDzozmdt0(C))) | sdtlpdtrp0(C,f25(A,B,C,E)) = E | -iLess0(A,xK) | -aSet0(F) | aElementOf0(f29(A,B,C,F),F) | sbrdtbr0(F) != A | f27(A,B,C) = sdtlpdtrp0(C,F). [copy(3160),flip(p)].
% 47.98/7.76
% 47.98/7.76 % given #2500 (I,wt=79): 3811 slbdtsldtrb0(sdtlcdtrc0(A,szDzozmdt0(A)),B) != szDzozmdt0(A) | -aElementOf0(B,szNzAzT0) | -aSet0(sdtlcdtrc0(A,szDzozmdt0(A))) | -aElementOf0(f22(B,sdtlcdtrc0(A,szDzozmdt0(A))),szNzAzT0) | -isCountable0(sdtlcdtrc0(A,szDzozmdt0(A))) | -aFunction0(A) | aElementOf0(C,sdtlcdtrc0(A,szDzozmdt0(A))) | -aElementOf0(D,szDzozmdt0(A)) | sdtlpdtrp0(A,D) != C | -iLess0(B,xK) | -aElementOf0(C,f28(B,sdtlcdtrc0(A,szDzozmdt0(A)),A)). [factor(1037,g,l),flip(a)].
% 47.98/7.76
% 47.98/7.76 % given #3000 (I,wt=91): 4318 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | aSubsetOf0(f23(A,B,C),B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | -aElementOf0(E,szDzozmdt0(C)) | sdtlpdtrp0(C,E) != D | -iLess0(A,xK) | aElementOf0(f29(A,B,C,f23(A,B,C)),f23(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(2056,a,m),merge(n)].
% 47.98/7.76
% 47.98/7.76 % given #3500 (I,wt=96): 4836 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(E,sdtlcdtrc0(C,szDzozmdt0(C))) | sdtlpdtrp0(C,f25(A,B,C,E)) = E | -iLess0(A,xK) | -aElementOf0(f29(A,B,C,B),f28(A,B,C)) | sbrdtbr0(B) != A | f27(A,B,C) = sdtlpdtrp0(C,B). [factor(2522,g,n)].
% 47.98/7.76
% 47.98/7.76 % given #4000 (I,wt=88): 5354 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -iLess0(A,xK) | -aSubsetOf0(f23(A,B,C),f28(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(3300,c,n)].
% 47.98/7.76
% 47.98/7.76 % given #4500 (I,wt=150): 5866 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(f26(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(f26(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -iLess0(A,xK) | -aElementOf0(f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)),f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)). [factor(4758,e,k)].
% 47.98/7.76
% 47.98/7.76 % given #5000 (T,wt=14): 6579 aFunction0(sdtlpdtrp0(xC,xK)). [resolve(803,a,505,a)].
% 47.98/7.76
% 47.98/7.76 % SZS status Theorem for theBenchmark
% 47.98/7.76
% 47.98/7.76 % Proof 1 at 6.53 (+ 0.33) seconds.
% 47.98/7.76 % Length of proof is 10.
% 47.98/7.76 % Level of proof is 3.
% 47.98/7.76 % Maximum clause weight is 21.000.
% 47.98/7.76 % Given clauses 5081.
% 47.98/7.76
% 47.98/7.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------