%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM595+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 : n002.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 92.51s 17.98s
% Output : CNFRefutation 92.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 5
% Syntax : Number of formulae : 40 ( 14 unt; 0 def)
% Number of atoms : 194 ( 56 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 245 ( 91 ~; 88 |; 56 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-2 aty)
% Number of variables : 48 ( 0 sgn 34 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__4618,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ? [W1] :
( ! [W2] :
( ( ( aElementOf0(W2,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ( sbrdtbr0(W2) = xk
& ( aSubsetOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
| ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )
& aSet0(W2) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W2) = W1 )
& aElementOf0(W1,xT) ) ),
file('theBenchmark.p',m__4618) ).
fof(m__4730,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( ( aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
| ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )
& aSet0(W1) )
=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('theBenchmark.p',m__4730) ).
fof(m__4806,axiom,
( sdtlpdtrp0(xd,xi) = xx
& aElementOf0(xi,szNzAzT0) ),
file('theBenchmark.p',m__4806) ).
fof(m__4826,axiom,
( ~ ~ ? [W0] : aElementOf0(W0,xX)
& xX = slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(xi)),xk)
& ! [W0] :
( ( ( sbrdtbr0(W0) = xk
& ( aSubsetOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(xi))) )
& aSet0(W0) ) ) )
=> aElementOf0(W0,xX) )
& ( aElementOf0(W0,xX)
=> ( sbrdtbr0(W0) = xk
& aSubsetOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(xi))) )
& aSet0(W0) ) ) )
& aSet0(xX) ),
file('theBenchmark.p',m__4826) ).
fof(m__,conjecture,
aElementOf0(xx,xT),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ aElementOf0(xx,xT),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_1018,negated_conjecture,
~ aElementOf0(xx,xT),
inference(clausify,[status(thm)],[m___neg]) ).
fof(nnf_90,plain,
( ? [W0] : aElementOf0(W0,xX)
& slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(xi)),xk) = xX
& ! [X0] :
( ( aElementOf0(X0,xX)
| sbrdtbr0(X0) != xk
| ( ~ aSubsetOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& ( ? [W1] :
( ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& aElementOf0(W1,X0) )
| ~ aSet0(X0) ) ) )
& ( ( sbrdtbr0(X0) = xk
& aSubsetOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aElementOf0(X1,X0) )
& aSet0(X0) )
| ~ aElementOf0(X0,xX) ) )
& aSet0(xX) ),
inference(fof_nnf,[status(thm)],[m__4826]) ).
fof(sk_m__4826_sk,plain,
( aElementOf0(sK0,xX)
& slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(xi)),xk) = xX
& ! [X0] :
( ( aElementOf0(X0,xX)
| sbrdtbr0(X0) != xk
| ( ~ aSubsetOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& ( ( ~ aElementOf0(sK2(X0),sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& aElementOf0(sK2(X0),X0) )
| ~ aSet0(X0) ) ) )
& ( ( sbrdtbr0(X0) = xk
& aSubsetOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aElementOf0(X1,X0) )
& aSet0(X0) )
| ~ aElementOf0(X0,xX) ) )
& aSet0(xX) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK0]),skolemize(W1,sK2(X0)),skolemize(W0,sK0)],[nnf_90]) ).
fof(sk_m__4826,plain,
( aElementOf0(sK0,xX)
& slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(xi)),xk) = xX
& ! [VAR_0] :
( aElementOf0(VAR_0,xX)
| sbrdtbr0(VAR_0) != xk
| ~ aSubsetOf0(VAR_0,sdtlpdtrp0(xN,szszuzczcdt0(xi))) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xX)
| sbrdtbr0(VAR_0) != xk
| ~ aElementOf0(sK2(VAR_0),sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xX)
| sbrdtbr0(VAR_0) != xk
| aElementOf0(sK2(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( sbrdtbr0(VAR_0) = xk
| ~ aElementOf0(VAR_0,xX) )
& ! [VAR_0] :
( aSubsetOf0(VAR_0,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aElementOf0(VAR_0,xX) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aElementOf0(VAR_1,VAR_0)
| ~ aElementOf0(VAR_0,xX) )
& ! [VAR_0] :
( aSet0(VAR_0)
| ~ aElementOf0(VAR_0,xX) )
& aSet0(xX) ),
inference(cnf_transformation,[status(thm)],[sk_m__4826_sk]) ).
cnf(c_1019,plain,
aElementOf0(sK0,xX),
inference(split_conjunct,[status(thm)],[sk_m__4826]) ).
cnf(c_1024,plain,
( sbrdtbr0(A) = xk
| ~ aElementOf0(A,xX) ),
inference(split_conjunct,[status(thm)],[sk_m__4826]) ).
cnf(c_1025,plain,
( aSubsetOf0(A,sdtlpdtrp0(xN,szszuzczcdt0(xi)))
| ~ aElementOf0(A,xX) ),
inference(split_conjunct,[status(thm)],[sk_m__4826]) ).
cnf(c_1027,plain,
( aSet0(A)
| ~ aElementOf0(A,xX) ),
inference(split_conjunct,[status(thm)],[sk_m__4826]) ).
cnf(c_1029,plain,
sdtlpdtrp0(xd,xi) = xx,
inference(clausify,[status(thm)],[m__4806]) ).
cnf(c_1030,plain,
aElementOf0(xi,szNzAzT0),
inference(clausify,[status(thm)],[m__4806]) ).
cnf(c_1039,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,A),B) = sdtlpdtrp0(xd,A)
| sbrdtbr0(B) != xk
| ~ aSubsetOf0(B,sdtlpdtrp0(xN,szszuzczcdt0(A)))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4730]) ).
fof(nnf_84,plain,
! [W0] :
( ? [W1] :
( ! [W2] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W2) = W1
| ( ~ aElementOf0(W2,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& ( sbrdtbr0(W2) != xk
| ( ~ aSubsetOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ? [W3] :
( ~ aElementOf0(W3,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aElementOf0(W3,W2) ) ) ) )
| ~ aSet0(W2) )
& aElementOf0(W1,xT) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(fof_nnf,[status(thm)],[m__4618]) ).
fof(sk_m__4618_sk,plain,
! [W0] :
( ( ! [W2] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W2) = sK1(W0)
| ( ~ aElementOf0(W2,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& ( sbrdtbr0(W2) != xk
| ( ~ aSubsetOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ~ aElementOf0(sK4(W0,W2),sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aElementOf0(sK4(W0,W2),W2) ) ) )
| ~ aSet0(W2) )
& aElementOf0(sK1(W0),xT) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK4]),skolemize(W1,sK1(W0)),skolemize(W3,sK4(W0,W2))],[nnf_84]) ).
fof(sk_m__4618,plain,
( ! [VAR_0,VAR_1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,VAR_0),VAR_1) = sK1(VAR_0)
| ~ aElementOf0(VAR_1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(VAR_0)),xk))
| ~ aSet0(VAR_1)
| ~ aElementOf0(VAR_0,szNzAzT0) )
& ! [VAR_0,VAR_1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,VAR_0),VAR_1) = sK1(VAR_0)
| sbrdtbr0(VAR_1) != xk
| ~ aSubsetOf0(VAR_1,sdtlpdtrp0(xN,szszuzczcdt0(VAR_0)))
| ~ aSet0(VAR_1)
| ~ aElementOf0(VAR_0,szNzAzT0) )
& ! [VAR_0,VAR_1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,VAR_0),VAR_1) = sK1(VAR_0)
| sbrdtbr0(VAR_1) != xk
| ~ aElementOf0(sK4(VAR_0,VAR_1),sdtlpdtrp0(xN,szszuzczcdt0(VAR_0)))
| ~ aSet0(VAR_1)
| ~ aElementOf0(VAR_0,szNzAzT0) )
& ! [VAR_0,VAR_1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,VAR_0),VAR_1) = sK1(VAR_0)
| sbrdtbr0(VAR_1) != xk
| aElementOf0(sK4(VAR_0,VAR_1),VAR_1)
| ~ aSet0(VAR_1)
| ~ aElementOf0(VAR_0,szNzAzT0) )
& ! [VAR_0] :
( aElementOf0(sK1(VAR_0),xT)
| ~ aElementOf0(VAR_0,szNzAzT0) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__4618_sk]) ).
cnf(c_1051,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,A),B) = sK1(A)
| sbrdtbr0(B) != xk
| ~ aSubsetOf0(B,sdtlpdtrp0(xN,szszuzczcdt0(A)))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[sk_m__4618]) ).
cnf(c_1054,plain,
( aElementOf0(sK1(A),xT)
| ~ aElementOf0(A,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[sk_m__4618]) ).
cnf(c_7846,plain,
sbrdtbr0(sK0) = xk,
inference(resolve,[status(thm)],[c_1024,c_1019]) ).
cnf(c_7847,plain,
aSubsetOf0(sK0,sdtlpdtrp0(xN,szszuzczcdt0(xi))),
inference(resolve,[status(thm)],[c_1025,c_1019]) ).
cnf(c_7850,plain,
aSet0(sK0),
inference(resolve,[status(thm)],[c_1027,c_1019]) ).
cnf(c_7857,plain,
aElementOf0(sK1(xi),xT),
inference(resolve,[status(thm)],[c_1054,c_1030]) ).
cnf(c_8802,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sK1(xi)
| sbrdtbr0(sK0) != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolve,[status(thm)],[c_7847,c_1051]) ).
cnf(c_8803,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sK1(xi)
| xk != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_7846,c_8802]) ).
cnf(c_8804,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sK1(xi)
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(copy,[status(thm)],[c_8803]) ).
cnf(c_8805,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sK1(xi)
| ~ aSet0(sK0) ),
inference(resolve,[status(thm)],[c_1030,c_8804]) ).
cnf(c_8798,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sK1(xi),
inference(resolve,[status(thm)],[c_7850,c_8805]) ).
cnf(c_8806,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sdtlpdtrp0(xd,xi)
| sbrdtbr0(sK0) != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolve,[status(thm)],[c_7847,c_1039]) ).
cnf(c_8807,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK0) = sdtlpdtrp0(xd,xi)
| xk != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_7846,c_8806]) ).
cnf(c_8808,plain,
( sK1(xi) = sdtlpdtrp0(xd,xi)
| xk != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_8798,c_8807]) ).
cnf(c_8809,plain,
( sK1(xi) = xx
| xk != xk
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_1029,c_8808]) ).
cnf(c_8810,plain,
( sK1(xi) = xx
| ~ aSet0(sK0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(copy,[status(thm)],[c_8809]) ).
cnf(c_8811,plain,
( sK1(xi) = xx
| ~ aSet0(sK0) ),
inference(resolve,[status(thm)],[c_1030,c_8810]) ).
cnf(c_8799,plain,
sK1(xi) = xx,
inference(resolve,[status(thm)],[c_7850,c_8811]) ).
cnf(c_8812,plain,
aElementOf0(xx,xT),
inference(paramod,[status(thm)],[c_8799,c_7857]) ).
cnf(c_8801,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1018,c_8812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM595+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.11/5.38 % Computer : n002.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sat Sep 26 03:25:26 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.38 % Process 725562 was started by sandbox on n002,
% 0.11/5.38 % Sat Sep 26 03:25:26 2026
% 0.11/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/5.49
% 0.13/5.49 % From the command line: assign(max_seconds, 300).
% 92.51/17.98
% 92.51/17.98 % given #500 (I,wt=63): 1083 -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aElementOf0(f36(A,B),sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) | -isCountable0(B) | -aSet0(C) | -aElementOf0(C,slbdtsldtrb0(B,xk)) | aElementOf0(C,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A))),xk)) # tptp_name(m__4331). [clausify(82)].
% 92.51/17.98
% 92.51/17.98 % given #1000 (I,wt=61): 1642 -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(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | aElementOf0(f27(A,B,C),xT). [resolve(284,a,119,e)].
% 92.51/17.98
% 92.51/17.98 % given #1500 (I,wt=73): 2422 -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(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | isCountable0(f28(A,B,C)). [resolve(287,a,178,f)].
% 92.51/17.98
% 92.51/17.98 % given #2000 (I,wt=83): 3143 -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(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | -aElementOf0(E,slbdtsldtrb0(f28(A,B,C),A)) | f27(A,B,C) = sdtlpdtrp0(C,E). [copy(3142),flip(m)].
% 92.51/17.98
% 92.51/17.98 % given #2500 (I,wt=52): 3866 aElementOf0(f23(A,B,C),szDzozmdt0(C)) | aSubsetOf0(f23(A,B,C),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(f28(A,B,C),B). [resolve(292,a,233,f)].
% 92.51/17.98
% 92.51/17.98 % given #3000 (I,wt=86): 4554 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | aSet0(sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | -aSet0(f23(A,B,C)) | aElementOf0(f29(A,B,C,f23(A,B,C)),f23(A,B,C)) | sdtlpdtrp0(C,f23(A,B,C)) = f27(A,B,C). [factor(478,b,m),flip(m)].
% 92.51/17.98
% 92.51/17.98 % given #3500 (I,wt=117): 5056 -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(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),szDzozmdt0(B)) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | aElementOf0(f25(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)),szDzozmdt0(B)) | -iLess0(A,xK) | aElementOf0(f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),xT). [factor(1919,b,j)].
% 92.51/17.98
% 92.51/17.98 % given #4000 (I,wt=122): 5556 -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(C,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | aElementOf0(f25(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)),szDzozmdt0(B)) | -iLess0(A,xK) | aElementOf0(f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),xT). [factor(2465,b,k)].
% 92.51/17.98
% 92.51/17.98 % given #4500 (I,wt=97): 6056 -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))) | -aElementOf0(F,szDzozmdt0(C)) | sdtlpdtrp0(C,F) != E | -iLess0(A,xK) | -aElementOf0(f29(A,B,C,f23(A,B,C)),f28(A,B,C)) | sdtlpdtrp0(C,f23(A,B,C)) = f27(A,B,C). [factor(3160,a,n),flip(p),merge(o)].
% 92.51/17.98
% 92.51/17.98 % given #5000 (I,wt=84): 6556 aElementOf0(f23(A,szDzozmdt0(B),B),szDzozmdt0(B)) | -aElementOf0(f23(A,szDzozmdt0(B),B),f23(A,szDzozmdt0(B),B)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(szDzozmdt0(B),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(D,szDzozmdt0(B)) | sdtlpdtrp0(B,D) != C | -iLess0(A,xK) | -aSubsetOf0(E,f28(A,szDzozmdt0(B),B)) | sbrdtbr0(E) != A | f27(A,szDzozmdt0(B),B) = sdtlpdtrp0(B,E). [factor(3977,a,c)].
% 92.51/17.98
% 92.51/17.98 % given #5500 (I,wt=113): 7056 -aSubsetOf0(f23(A,szDzozmdt0(B),B),szDzozmdt0(B)) | sbrdtbr0(f23(A,szDzozmdt0(B),B)) != A | -aElementOf0(f25(A,szDzozmdt0(B),B,C),f23(A,szDzozmdt0(B),B)) | aElementOf0(f25(A,szDzozmdt0(B),B,C),szDzozmdt0(B)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(szDzozmdt0(B),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | -aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -iLess0(A,xK) | -aSet0(f23(A,szDzozmdt0(B),B)) | aElementOf0(f29(A,szDzozmdt0(B),B,f23(A,szDzozmdt0(B),B)),f23(A,szDzozmdt0(B),B)) | sdtlpdtrp0(B,f23(A,szDzozmdt0(B),B)) = f27(A,szDzozmdt0(B),B). [factor(4500,d,j)].
% 92.51/17.98
% 92.51/17.98 % given #6000 (I,wt=94): 7558 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f22(A,B),f23(A,B,C)) | aElementOf0(f22(A,B),B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | -isCountable0(B) | -aFunction0(C) | aElementOf0(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | -aElementOf0(f29(A,B,C,f23(A,B,C)),f28(A,B,C)) | sdtlpdtrp0(C,f23(A,B,C)) = f27(A,B,C). [factor(6226,e,h)].
% 92.51/17.98
% 92.51/17.98 % SZS status Theorem for theBenchmark
% 92.51/17.98
% 92.51/17.98 % Proof 1 at 4.16 (+ 0.19) seconds.
% 92.51/17.98 % Length of proof is 22.
% 92.51/17.98 % Level of proof is 5.
% 92.51/17.98 % Maximum clause weight is 39.000.
% 92.51/17.98 % Given clauses 6289.
% 92.51/17.98
% 92.51/17.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------