%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM587+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 : n017.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:29 AM UTC 2026
% Result : Theorem 110.45s 15.52s
% Output : CNFRefutation 110.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 7
% Syntax : Number of formulae : 33 ( 15 unt; 0 def)
% Number of atoms : 229 ( 43 equ)
% Maximal formula atoms : 47 ( 6 avg)
% Number of connectives : 253 ( 57 ~; 61 |; 105 &)
% ( 7 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 54 ( 0 sgn 44 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mImgRng,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ),
file('theBenchmark.p',mImgRng) ).
fof(m__3453,axiom,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(W0,xT) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
=> aElementOf0(W0,szDzozmdt0(xc)) )
& ( aElementOf0(W0,szDzozmdt0(xc))
=> ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
& aFunction0(xc) ),
file('theBenchmark.p',m__3453) ).
fof(m__4151,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( ( ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ( ( ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
=> ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ) )
& aSet0(W1) )
=> ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) ) )
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( ( ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1) ) ) )
=> aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0))) )
& ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
=> ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1) ) ) )
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('theBenchmark.p',m__4151) ).
fof(m__4237,axiom,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) = xx
& aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('theBenchmark.p',m__4237) ).
fof(m__4263,axiom,
( ? [W0] :
( sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& aElementOf0(W0,szDzozmdt0(xc)) )
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('theBenchmark.p',m__4263) ).
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_2051,negated_conjecture,
~ aElementOf0(xx,xT),
inference(clausify,[status(thm)],[m___neg]) ).
fof(nnf_83,plain,
( ? [W0] :
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,W0)
& aElementOf0(W0,szDzozmdt0(xc)) )
& ! [X3] :
( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X3
& ~ aElementOf0(X3,xQ) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) )
| ~ aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& ~ aElementOf0(X1,xQ) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) )
| ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(fof_nnf,[status(thm)],[m__4263]) ).
fof(sk_m__4263_sk,plain,
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK0)
& aElementOf0(sK0,szDzozmdt0(xc))
& ! [X3] :
( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X3
& ~ aElementOf0(X3,xQ) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) )
| ~ aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& ~ aElementOf0(X1,xQ) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) )
| ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W0,sK0)],[nnf_83]) ).
fof(sk_m__4263,plain,
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK0)
& aElementOf0(sK0,szDzozmdt0(xc))
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,xQ)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) = VAR_0
| aElementOf0(VAR_0,xQ)
| ~ aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),VAR_0)
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,xi)) )
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,xQ)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) = VAR_0
| aElementOf0(VAR_0,xQ)
| ~ aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [VAR_0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),VAR_0)
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(cnf_transformation,[status(thm)],[sk_m__4263_sk]) ).
cnf(c_2052,plain,
sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK0),
inference(split_conjunct,[status(thm)],[sk_m__4263]) ).
cnf(c_2053,plain,
aElementOf0(sK0,szDzozmdt0(xc)),
inference(split_conjunct,[status(thm)],[sk_m__4263]) ).
cnf(c_2061,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) = xx,
inference(clausify,[status(thm)],[m__4237]) ).
cnf(c_2062,plain,
aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)),
inference(clausify,[status(thm)],[m__4237]) ).
cnf(c_2066,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__4237]) ).
fof(m__4200,axiom,
aElementOf0(xi,szNzAzT0),
file('theBenchmark.p',m__4200) ).
cnf(c_2075,plain,
aElementOf0(xi,szNzAzT0),
inference(clausify,[status(thm)],[m__4200]) ).
cnf(c_2076,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,A),B) = sdtlpdtrp0(xc,sdtpldt0(B,szmzizndt0(sdtlpdtrp0(xN,A))))
| ~ aElementOf0(B,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A))),xk))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4151]) ).
cnf(c_2077,plain,
( sdtlpdtrp0(xc,sdtpldt0(B,szmzizndt0(sdtlpdtrp0(xN,A)))) = sdtlpdtrp0(sdtlpdtrp0(xC,A),B)
| ~ aElementOf0(B,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A))),xk))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(copy,[status(thm)],[c_2076]) ).
cnf(c_2419,plain,
( aElementOf0(A,xT)
| ~ aElementOf0(A,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(clausify,[status(thm)],[m__3453]) ).
cnf(c_2433,plain,
aFunction0(xc),
inference(clausify,[status(thm)],[m__3453]) ).
cnf(c_2452,plain,
( aElementOf0(sdtlpdtrp0(A,B),sdtlcdtrc0(A,szDzozmdt0(A)))
| ~ aElementOf0(B,szDzozmdt0(A))
| ~ aFunction0(A) ),
inference(clausify,[status(thm)],[mImgRng]) ).
cnf(c_19434,plain,
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)
| ~ aSet0(xQ)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolve,[status(thm)],[c_2077,c_2062]) ).
cnf(c_19435,plain,
( sdtlpdtrp0(xc,sK0) = sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)
| ~ aSet0(xQ)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_2052,c_19434]) ).
cnf(c_19436,plain,
( sdtlpdtrp0(xc,sK0) = xx
| ~ aSet0(xQ)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramod,[status(thm)],[c_2061,c_19435]) ).
cnf(c_19437,plain,
( sdtlpdtrp0(xc,sK0) = xx
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_2075,c_19436]) ).
cnf(c_7948,plain,
sdtlpdtrp0(xc,sK0) = xx,
inference(resolve,[status(thm)],[c_2066,c_19437]) ).
cnf(c_19438,plain,
( aElementOf0(sdtlpdtrp0(xc,sK0),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aFunction0(xc) ),
inference(resolve,[status(thm)],[c_2452,c_2053]) ).
cnf(c_19439,plain,
( aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aFunction0(xc) ),
inference(paramod,[status(thm)],[c_7948,c_19438]) ).
cnf(c_8094,plain,
aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc))),
inference(resolve,[status(thm)],[c_2433,c_19439]) ).
cnf(c_19440,plain,
aElementOf0(xx,xT),
inference(resolve,[status(thm)],[c_8094,c_2419]) ).
cnf(c_19433,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2051,c_19440]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM587+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.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 03:15:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 3864334 was started by sandbox on n017,
% 0.10/0.37 % Sat Sep 26 03:15:50 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.20/0.52
% 0.20/0.52 % From the command line: assign(max_seconds, 300).
% 110.45/15.52
% 110.45/15.52 % given #500 (I,wt=61): 1193 -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(277,a,112,e)].
% 110.45/15.52
% 110.45/15.52 % given #1000 (I,wt=52): 2086 -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aSubsetOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) | sbrdtbr0(B) != xk | aElementOf0(C,sdtpldt0(B,szmzizndt0(sdtlpdtrp0(xN,A)))) | -aElement0(C) | -aElementOf0(C,B) # tptp_name(m__4151). [clausify(80)].
% 110.45/15.52
% 110.45/15.52 % given #1500 (I,wt=74): 2660 -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(f26(A,B,C),xT) | -iLess0(A,xK) | -aElementOf0(E,f28(A,B,C)) | aElementOf0(E,B). [resolve(280,a,227,f)].
% 110.45/15.52
% 110.45/15.52 % given #2000 (I,wt=92): 3383 -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),szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -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(3382),flip(p)].
% 110.45/15.52
% 110.45/15.52 % given #2500 (I,wt=55): 4104 aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aSubsetOf0(sdtlcdtrc0(C,szDzozmdt0(C)),xT) | -iLess0(A,xK) | aSet0(f28(A,B,C)). [resolve(286,a,93,e)].
% 110.45/15.52
% 110.45/15.52 % given #3000 (I,wt=85): 4768 -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) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | aSet0(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(421,a,l),flip(n),merge(m)].
% 110.45/15.52
% 110.45/15.52 % given #3500 (I,wt=88): 5268 -aSubsetOf0(f23(A,B,C),B) | 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) | -aSet0(f23(A,B,C)) | -aElementOf0(f29(A,B,C,f23(A,B,C)),f28(A,B,C)) | sdtlpdtrp0(C,f23(A,B,C)) = f27(A,B,C). [factor(1474,b,m),flip(m)].
% 110.45/15.52
% 110.45/15.52 % given #4000 (I,wt=125): 5770 -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))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -aElementOf0(D,szDzozmdt0(B)) | f22(A,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,D) | -iLess0(A,xK) | aSubsetOf0(f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))). [factor(2685,h,k),flip(l)].
% 110.45/15.52
% 110.45/15.52 % given #4500 (I,wt=112): 6270 -aSet0(f23(A,szDzozmdt0(B),B)) | aElementOf0(f24(A,szDzozmdt0(B),B),f23(A,szDzozmdt0(B),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) | -aSet0(szDzozmdt0(B)) | -aElementOf0(f22(A,szDzozmdt0(B)),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | -aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -iLess0(A,xK) | -aSubsetOf0(D,f28(A,szDzozmdt0(B),B)) | sbrdtbr0(D) != A | f27(A,szDzozmdt0(B),B) = sdtlpdtrp0(B,D). [factor(3433,e,l)].
% 110.45/15.52
% 110.45/15.52 % given #5000 (I,wt=91): 6770 aElementOf0(f23(A,szDzozmdt0(B),B),szDzozmdt0(B)) | -aElementOf0(f23(A,szDzozmdt0(B),B),f23(A,szDzozmdt0(B),B)) | -aElementOf0(A,szNzAzT0) | -aSet0(szDzozmdt0(B)) | -aElementOf0(f22(A,szDzozmdt0(B)),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | aElementOf0(f26(A,szDzozmdt0(B),B),sdtlcdtrc0(B,szDzozmdt0(B))) | -iLess0(A,xK) | -aSet0(C) | -aElementOf0(f29(A,szDzozmdt0(B),B,C),f28(A,szDzozmdt0(B),B)) | sbrdtbr0(C) != A | f27(A,szDzozmdt0(B),B) = sdtlpdtrp0(B,C). [factor(4215,a,c)].
% 110.45/15.52
% 110.45/15.52 % given #5500 (I,wt=122): 7270 -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))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | sdtlpdtrp0(B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != f22(A,sdtlcdtrc0(B,szDzozmdt0(B))) | -iLess0(A,xK) | aSubsetOf0(f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))). [factor(5014,g,j)].
% 110.45/15.52
% 110.45/15.52 % given #6000 (I,wt=114): 7770 aElementOf0(f23(A,szDzozmdt0(B),B),szDzozmdt0(B)) | -aElementOf0(f23(A,szDzozmdt0(B),B),f23(A,szDzozmdt0(B),B)) | -aElementOf0(A,szNzAzT0) | -aSet0(szDzozmdt0(B)) | -aElementOf0(f22(A,szDzozmdt0(B)),szNzAzT0) | -isCountable0(szDzozmdt0(B)) | -aFunction0(B) | aElementOf0(f29(A,szDzozmdt0(B),B,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(C,szDzozmdt0(B)) | f29(A,szDzozmdt0(B),B,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,C) | -iLess0(A,xK) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(sdtlcdtrc0(B,szDzozmdt0(B))) != A | f27(A,szDzozmdt0(B),B) = sdtlpdtrp0(B,sdtlcdtrc0(B,szDzozmdt0(B))). [factor(6798,h,m),flip(j)].
% 110.45/15.52
% 110.45/15.52 % given #6500 (W,wt=14): 18970 aElement0(f9(xi,szNzAzT0)). [resolve(14158,a,2579,b),unit_del(a,2540)].
% 110.45/15.52
% 110.45/15.52 % SZS status Theorem for theBenchmark
% 110.45/15.52
% 110.45/15.52 % Proof 1 at 6.44 (+ 0.39) seconds.
% 110.45/15.52 % Length of proof is 21.
% 110.45/15.52 % Level of proof is 5.
% 110.45/15.52 % Maximum clause weight is 56.000.
% 110.45/15.52 % Given clauses 6554.
% 110.45/15.52
% 110.45/15.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------