%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM600+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.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 : Fri Sep 25 02:26:10 PM UTC 2026
% Result : Theorem 91.04s 22.37s
% Output : CNFRefutation 91.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 12
% Syntax : Number of formulae : 88 ( 28 unt; 2 def)
% Number of atoms : 404 ( 97 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 466 ( 184 ~; 181 |; 80 &)
% ( 10 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 3 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-3 aty)
% Number of variables : 148 ( 0 sgn 131 !; 17 ?; 23 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(f66,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aFunction0(X0) )
=> ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefPtt) ).
fof(f67,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aFunction0(X0) )
=> aSubsetOf0(sdtlbdtrb0(X0,X1),szDzozmdt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPttSet) ).
fof(f68,axiom,
! [X0] :
( aFunction0(X0)
=> ! [X1] :
( aSubsetOf0(X1,szDzozmdt0(X0))
=> ! [X2] :
( X2 = sdtlcdtrc0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& aSet0(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSImg) ).
fof(f73,axiom,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3291) ).
fof(f91,axiom,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4660) ).
fof(f92,axiom,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aElementOf0(X1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),xk))
& aSet0(X1) )
=> sdtlpdtrp0(xd,X0) = sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4730) ).
fof(f94,axiom,
( isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4854) ).
fof(f95,axiom,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4891) ).
fof(f97,conjecture,
! [X0] :
( aElementOf0(X0,xO)
=> ? [X1] :
( sdtlpdtrp0(xe,X1) = X0
& aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(X1,szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f98,negated_conjecture,
~ ! [X0] :
( aElementOf0(X0,xO)
=> ? [X1] :
( sdtlpdtrp0(xe,X1) = X0
& aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(X1,szNzAzT0) ) ),
inference(negated_conjecture,[status(cth)],[f97]) ).
fof(f106,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f194,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
inference(ennf_transformation,[],[f66]) ).
fof(f195,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
inference(flattening,[],[f194]) ).
fof(f196,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| aSubsetOf0(sdtlbdtrb0(X0,X1),szDzozmdt0(X0)) ),
inference(ennf_transformation,[],[f67]) ).
fof(f197,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| aSubsetOf0(sdtlbdtrb0(X0,X1),szDzozmdt0(X0)) ),
inference(flattening,[],[f196]) ).
fof(f198,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ! [X2] :
( X2 = sdtlcdtrc0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& aSet0(X2) ) ) ) ),
inference(ennf_transformation,[],[f68]) ).
fof(f225,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
inference(ennf_transformation,[],[f91]) ).
fof(f226,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ~ aElementOf0(X1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),xk))
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X0) = sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(ennf_transformation,[],[f92]) ).
fof(f227,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ~ aElementOf0(X1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),xk))
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X0) = sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(flattening,[],[f226]) ).
fof(f228,plain,
? [X0] :
( aElementOf0(X0,xO)
& ! [X1] :
( sdtlpdtrp0(xe,X1) != X0
| ~ aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X1,szNzAzT0) ) ),
inference(ennf_transformation,[],[f98]) ).
fof(f281,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0))
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f195]) ).
fof(f282,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0))
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(flattening,[],[f281]) ).
fof(f283,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sdtlpdtrp0(X0,X4) = X1
& aElementOf0(X4,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X4) != X1
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(rectify,[],[f282]) ).
fof(f284,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sdtlpdtrp0(X0,X4) = X1
& aElementOf0(X4,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X4) != X1
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ( ( aElementOf0(sK16(X0,X1,X2),X2)
| ( sdtlpdtrp0(X0,sK16(X0,X1,X2)) = X1
& aElementOf0(sK16(X0,X1,X2),szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(sK16(X0,X1,X2),X2)
| sdtlpdtrp0(X0,sK16(X0,X1,X2)) != X1
| ~ aElementOf0(sK16(X0,X1,X2),szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X3,sK16(X0,X1,X2))],[f283]) ).
fof(f285,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ! [X2] :
( ( sdtlcdtrc0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& ( ! [X4] :
( sdtlpdtrp0(X0,X4) != X3
| ~ aElementOf0(X4,X1) )
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& ( ~ aElementOf0(X3,X2)
| ! [X4] :
( sdtlpdtrp0(X0,X4) != X3
| ~ aElementOf0(X4,X1) ) ) )
| ~ aSet0(X2)
| X2 = sdtlcdtrc0(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f198]) ).
fof(f286,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ! [X2] :
( ( sdtlcdtrc0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& ( ! [X4] :
( sdtlpdtrp0(X0,X4) != X3
| ~ aElementOf0(X4,X1) )
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ? [X4] :
( sdtlpdtrp0(X0,X4) = X3
& aElementOf0(X4,X1) ) )
& ( ~ aElementOf0(X3,X2)
| ! [X4] :
( sdtlpdtrp0(X0,X4) != X3
| ~ aElementOf0(X4,X1) ) ) )
| ~ aSet0(X2)
| X2 = sdtlcdtrc0(X0,X1) ) ) ) ),
inference(flattening,[],[f285]) ).
fof(f287,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ! [X2] :
( ( sdtlcdtrc0(X0,X1) != X2
| ( ! [X6] :
( ( ~ aElementOf0(X6,X2)
| ? [X8] :
( sdtlpdtrp0(X0,X8) = X6
& aElementOf0(X8,X1) ) )
& ( ! [X7] :
( sdtlpdtrp0(X0,X7) != X6
| ~ aElementOf0(X7,X1) )
| aElementOf0(X6,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ? [X5] :
( sdtlpdtrp0(X0,X5) = X3
& aElementOf0(X5,X1) ) )
& ( ~ aElementOf0(X3,X2)
| ! [X4] :
( sdtlpdtrp0(X0,X4) != X3
| ~ aElementOf0(X4,X1) ) ) )
| ~ aSet0(X2)
| X2 = sdtlcdtrc0(X0,X1) ) ) ) ),
inference(rectify,[],[f286]) ).
fof(f288,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ! [X2] :
( ( sdtlcdtrc0(X0,X1) != X2
| ( ! [X6] :
( ( ~ aElementOf0(X6,X2)
| ( sdtlpdtrp0(X0,sK19(X0,X1,X6)) = X6
& aElementOf0(sK19(X0,X1,X6),X1) ) )
& ( ! [X7] :
( sdtlpdtrp0(X0,X7) != X6
| ~ aElementOf0(X7,X1) )
| aElementOf0(X6,X2) ) )
& aSet0(X2) ) )
& ( ( ( aElementOf0(sK17(X0,X1,X2),X2)
| ( sK17(X0,X1,X2) = sdtlpdtrp0(X0,sK18(X0,X1,X2))
& aElementOf0(sK18(X0,X1,X2),X1) ) )
& ( ~ aElementOf0(sK17(X0,X1,X2),X2)
| ! [X4] :
( sdtlpdtrp0(X0,X4) != sK17(X0,X1,X2)
| ~ aElementOf0(X4,X1) ) ) )
| ~ aSet0(X2)
| X2 = sdtlcdtrc0(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X3,sK17(X0,X1,X2)),skolemize(X5,sK18(X0,X1,X2)),skolemize(X8,sK19(X0,X1,X6))],[f287]) ).
fof(f297,plain,
( aElementOf0(sK28,xO)
& ! [X1] :
( sdtlpdtrp0(xe,X1) != sK28
| ~ aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X1,szNzAzT0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X0,sK28)],[f228]) ).
fof(f298,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| aElement0(X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f415,plain,
! [X2,X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| sdtlbdtrb0(X0,X1) != X2
| ~ aElementOf0(X4,X2)
| aElementOf0(X4,szDzozmdt0(X0)) ),
inference(cnf_transformation,[],[f284]) ).
fof(f421,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| aSubsetOf0(sdtlbdtrb0(X0,X1),szDzozmdt0(X0)) ),
inference(cnf_transformation,[],[f197]) ).
fof(f422,plain,
! [X2,X0,X1,X6] :
( ~ aFunction0(X0)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| sdtlcdtrc0(X0,X1) != X2
| ~ aElementOf0(X6,X2)
| sdtlpdtrp0(X0,sK19(X0,X1,X6)) = X6 ),
inference(cnf_transformation,[],[f288]) ).
fof(f423,plain,
! [X2,X0,X1,X6] :
( ~ aFunction0(X0)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| sdtlcdtrc0(X0,X1) != X2
| ~ aElementOf0(X6,X2)
| aElementOf0(sK19(X0,X1,X6),X1) ),
inference(cnf_transformation,[],[f288]) ).
fof(f442,plain,
aSet0(xT),
inference(cnf_transformation,[],[f73]) ).
fof(f481,plain,
szNzAzT0 = szDzozmdt0(xe),
inference(cnf_transformation,[],[f225]) ).
fof(f482,plain,
aFunction0(xe),
inference(cnf_transformation,[],[f225]) ).
fof(f484,plain,
szNzAzT0 = szDzozmdt0(xd),
inference(cnf_transformation,[],[f227]) ).
fof(f485,plain,
aFunction0(xd),
inference(cnf_transformation,[],[f227]) ).
fof(f488,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[],[f94]) ).
fof(f489,plain,
xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[],[f95]) ).
fof(f493,plain,
aElementOf0(sK28,xO),
inference(cnf_transformation,[],[f297]) ).
fof(f494,plain,
! [X1] :
( sdtlpdtrp0(xe,X1) != sK28
| ~ aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f520,plain,
! [X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ~ aElementOf0(X4,sdtlbdtrb0(X0,X1))
| aElementOf0(X4,szDzozmdt0(X0)) ),
inference(equality_resolution,[],[f415]) ).
fof(f525,plain,
! [X0,X1,X6] :
( ~ aFunction0(X0)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aElementOf0(X6,sdtlcdtrc0(X0,X1))
| aElementOf0(sK19(X0,X1,X6),X1) ),
inference(equality_resolution,[],[f423]) ).
fof(f526,plain,
! [X0,X1,X6] :
( ~ aFunction0(X0)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aElementOf0(X6,sdtlcdtrc0(X0,X1))
| sdtlpdtrp0(X0,sK19(X0,X1,X6)) = X6 ),
inference(equality_resolution,[],[f422]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( aElement0(X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,szDzozmdt0(X1))
| ~ aFunction0(X1)
| ~ aElement0(X2)
| ~ aElementOf0(X0,sdtlbdtrb0(X1,X2)) ),
inference(cnf_transformation,[],[f520]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(sdtlbdtrb0(X1,X0),szDzozmdt0(X1))
| ~ aFunction0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_178,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(sK19(X1,X2,X0),X2)
| ~ aFunction0(X1)
| ~ aSubsetOf0(X2,szDzozmdt0(X1))
| ~ aElementOf0(X0,sdtlcdtrc0(X1,X2)) ),
inference(cnf_transformation,[],[f525]) ).
tcf(c_179,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtlpdtrp0(X1,sK19(X1,X2,X0)) = X0 )
| ~ aFunction0(X1)
| ~ aSubsetOf0(X2,szDzozmdt0(X1))
| ~ aElementOf0(X0,sdtlcdtrc0(X1,X2)) ),
inference(cnf_transformation,[],[f526]) ).
tcf(c_192,plain,
aSet0(xT),
inference(cnf_transformation,[],[f442]) ).
tcf(c_231,plain,
aFunction0(xe),
inference(cnf_transformation,[],[f482]) ).
tcf(c_232,plain,
szDzozmdt0(xe) = szNzAzT0,
inference(cnf_transformation,[],[f481]) ).
tcf(c_234,plain,
aFunction0(xd),
inference(cnf_transformation,[],[f485]) ).
tcf(c_235,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(cnf_transformation,[],[f484]) ).
tcf(c_238,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[],[f488]) ).
tcf(c_241,plain,
sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) = xO,
inference(cnf_transformation,[],[f489]) ).
tcf(c_244,negated_conjecture,
! [X0: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ( sdtlpdtrp0(xe,X0) != sK28 ) ),
inference(cnf_transformation,[],[f494]) ).
tcf(c_245,negated_conjecture,
aElementOf0(sK28,xO),
inference(cnf_transformation,[],[f493]) ).
tcf(c_15161,definition,
iPr_def_10 = szDzizrdt0(xd),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_15162,definition,
iPr_def_11 = sdtlbdtrb0(xd,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_15163,negated_conjecture,
aElementOf0(sK28,xO),
inference(demodulation,[status(thm)],[c_245]) ).
tcf(c_15164,negated_conjecture,
! [X0: $i] :
( ~ aElementOf0(X0,iPr_def_11)
| ~ aElementOf0(X0,szNzAzT0)
| ( sdtlpdtrp0(xe,X0) != sK28 ) ),
inference(demodulation,[status(thm)],[c_244,c_15161,c_15162]) ).
tcf(c_18090,plain,
aElementOf0(iPr_def_10,xT),
inference(light_normalisation,[status(thm)],[c_238,c_15161]) ).
tcf(c_18252,plain,
( aElement0(iPr_def_10)
| ~ aSet0(xT) ),
inference(superposition,[status(thm)],[c_18090,c_49]) ).
tcf(c_18253,plain,
aElement0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_18252,c_192]) ).
tcf(c_21765,plain,
! [X0: $i] :
( aElementOf0(X0,szDzozmdt0(xd))
| ~ aFunction0(xd)
| ~ aElement0(iPr_def_10)
| ~ aElementOf0(X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_15162,c_170]) ).
tcf(c_21768,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aFunction0(xd)
| ~ aElement0(iPr_def_10)
| ~ aElementOf0(X0,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_21765,c_235]) ).
tcf(c_21769,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_11) ),
inference(forward_subsumption_resolution,[status(thm)],[c_21768,c_234,c_18253]) ).
tcf(c_21803,plain,
! [X0: $i] :
( ~ aElementOf0(X0,iPr_def_11)
| ( sdtlpdtrp0(xe,X0) != sK28 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_15164,c_21769]) ).
tcf(c_126504,negated_conjecture,
! [X0: $i] :
( ~ aElementOf0(X0,iPr_def_11)
| ( sdtlpdtrp0(xe,X0) != sK28 ) ),
inference(global_subsumption_just,[status(thm)],[c_15164,c_21803]) ).
tcf(c_126508,plain,
aElementOf0(iPr_def_10,xT),
inference(light_normalisation,[status(thm)],[c_238,c_15161]) ).
tcf(c_126664,plain,
( aElement0(iPr_def_10)
| ~ aSet0(xT) ),
inference(superposition,[status(thm)],[c_126508,c_49]) ).
tcf(c_126665,plain,
aElement0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_126664,c_192]) ).
tcf(c_126682,plain,
sdtlcdtrc0(xe,iPr_def_11) = xO,
inference(light_normalisation,[status(thm)],[c_241,c_15161,c_15162]) ).
tcf(c_127699,plain,
( aSubsetOf0(iPr_def_11,szDzozmdt0(xd))
| ~ aFunction0(xd)
| ~ aElement0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_15162,c_172]) ).
tcf(c_127706,plain,
( aSubsetOf0(iPr_def_11,szNzAzT0)
| ~ aFunction0(xd)
| ~ aElement0(iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_127699,c_235]) ).
tcf(c_127707,plain,
aSubsetOf0(iPr_def_11,szNzAzT0),
inference(forward_subsumption_resolution,[status(thm)],[c_127706,c_234,c_126665]) ).
tcf(c_137499,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xe,sK19(xe,iPr_def_11,X0)) = X0 )
| ~ aFunction0(xe)
| ~ aElementOf0(X0,xO)
| ~ aSubsetOf0(iPr_def_11,szDzozmdt0(xe)) ),
inference(superposition,[status(thm)],[c_126682,c_179]) ).
tcf(c_137508,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xe,sK19(xe,iPr_def_11,X0)) = X0 )
| ~ aFunction0(xe)
| ~ aSubsetOf0(iPr_def_11,szNzAzT0)
| ~ aElementOf0(X0,xO) ),
inference(light_normalisation,[status(thm)],[c_137499,c_232]) ).
tcf(c_137509,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xe,sK19(xe,iPr_def_11,X0)) = X0 )
| ~ aElementOf0(X0,xO) ),
inference(forward_subsumption_resolution,[status(thm)],[c_137508,c_231,c_127707]) ).
tcf(c_259694,plain,
sdtlpdtrp0(xe,sK19(xe,iPr_def_11,sK28)) = sK28,
inference(superposition,[status(thm)],[c_15163,c_137509]) ).
tcf(c_259948,plain,
~ aElementOf0(sK19(xe,iPr_def_11,sK28),iPr_def_11),
inference(superposition,[status(thm)],[c_259694,c_126504]) ).
tcf(c_259973,plain,
( ~ aFunction0(xe)
| ~ aSubsetOf0(iPr_def_11,szDzozmdt0(xe))
| ~ aElementOf0(sK28,sdtlcdtrc0(xe,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_178,c_259948]) ).
tcf(c_259974,plain,
( ~ aFunction0(xe)
| ~ aSubsetOf0(iPr_def_11,szNzAzT0)
| ~ aElementOf0(sK28,xO) ),
inference(light_normalisation,[status(thm)],[c_259973,c_232,c_126682]) ).
tcf(c_259975,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_259974,c_231,c_127707,c_15163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM600+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.20/0.67 % Computer : n015.cluster.edu
% 0.20/0.67 % Model : x86_64 x86_64
% 0.20/0.67 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.67 % Memory : 8046.5625MB
% 0.20/0.67 % OS : Linux 6.8.0-71-generic
% 0.20/0.67 % CPULimit : 300
% 0.20/0.67 % WCLimit : 300
% 0.20/0.67 % DateTime : Thu Sep 24 04:54:26 UTC 2026
% 0.20/0.67 % CPUTime :
% 0.20/0.68 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/0.74 Running first-order theorem proving
% 0.24/0.74 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.24/0.76
% 0.24/0.76 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.76
% 0.24/0.76 % Detected problem language: tptp
% 0.24/0.78 % Proving...
% 91.04/22.37 % SZS status Started for theBenchmark.p
% 91.04/22.37 % SZS status Theorem for theBenchmark.p
% 91.04/22.37
% 91.04/22.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 91.04/22.37
% 91.04/22.37 % ------ iProver source info
% 91.04/22.37
% 91.04/22.37 % git: date: 2026-07-19 20:42:38 +0200
% 91.04/22.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 91.04/22.37 % git: non_committed_changes: false
% 91.04/22.37
% 91.04/22.37 % ------ Parsing...
% 91.04/22.37 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 91.04/22.37
% 91.04/22.37 % ------ Preprocessing... sup_sim: 2 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 91.04/22.37
% 91.04/22.37 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 91.04/22.37
% 91.04/22.37 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 91.04/22.37 % ------ Proving...
% 91.04/22.37 % ------ Problem Properties
% 91.04/22.37
% 91.04/22.37 %
% 91.04/22.37 % clauses 194
% 91.04/22.37 % conjectures 2
% 91.04/22.37 % EPR 44
% 91.04/22.37 % Horn 155
% 91.04/22.37 % unary 38
% 91.04/22.37 % binary 29
% 91.04/22.37 % lits 648
% 91.04/22.37 % lits eq 105
% 91.04/22.37 % fd_pure 0
% 91.04/22.37 % fd_pseudo 0
% 91.04/22.37 % fd_cond 10
% 91.04/22.37 % fd_pseudo_cond 25
% 91.04/22.37 % AC symbols 0
% 91.04/22.37
% 91.04/22.37 % ------ Schedule dynamic 5 is on
% 91.04/22.37
% 91.04/22.37 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 91.04/22.37
% 91.04/22.37
% 91.04/22.37 % ------
% 91.04/22.37 % Current options:
% 91.04/22.37 % ------
% 91.04/22.37
% 91.04/22.37
% 91.04/22.37 %
% 91.04/22.37
% 91.04/22.37 % ------ Proving...
% 91.04/22.37 % Proof_search_loop: time out after: 3959 full_loop iterations
% 91.04/22.37
% 91.04/22.37 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 91.04/22.37
% 91.04/22.37
% 91.04/22.37 % ------
% 91.04/22.37 % Current options:
% 91.04/22.37 % ------
% 91.04/22.37
% 91.04/22.37
% 91.04/22.37 %
% 91.04/22.37
% 91.04/22.37 % ------ Proving...
% 91.04/22.37 %
% 91.04/22.37
% 91.04/22.37 % SZS status Theorem for theBenchmark.p
% 91.04/22.37
% 91.04/22.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 91.04/22.37
% 91.04/22.37
%------------------------------------------------------------------------------