%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM587+3 : 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 : n010.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:08 PM UTC 2026
% Result : Theorem 92.52s 14.37s
% Output : CNFRefutation 92.52s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f245ERROR: Could not build tree for root c_80212ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSub) ).
fof(f12,axiom,
! [X0] :
( aSet0(X0)
=> aSubsetOf0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSubRefl) ).
fof(f13,axiom,
! [X0,X1] :
( ( aSet0(X1)
& aSet0(X0) )
=> ( ( aSubsetOf0(X1,X0)
& aSubsetOf0(X0,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSubASymm) ).
fof(f73,axiom,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3291) ).
fof(f76,axiom,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(X0,xT) )
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X1] :
( sdtlpdtrp0(xc,X1) = X0
& aElementOf0(X1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( ( sbrdtbr0(X0) = xK
& ( aSubsetOf0(X0,xS)
| ( ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
=> aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
=> ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3453) ).
fof(f87,axiom,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4200) ).
fof(f89,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))))
& ! [X0] :
( aElementOf0(X0,xQ)
=> aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( X0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(X0,sdtlpdtrp0(xN,xi))
& aElement0(X0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4237) ).
fof(f90,axiom,
( ? [X0] :
( sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& aElementOf0(X0,szDzozmdt0(xc)) )
& ! [X0] :
( aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ) )
& aElement0(X0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ) )
& aElement0(X0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4263) ).
fof(f91,conjecture,
aElementOf0(xx,xT),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f92,negated_conjecture,
~ aElementOf0(xx,xT),
inference(negated_conjecture,[status(cth)],[f91]) ).
fof(f100,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X5] :
( aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(X5,xT) )
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( sdtlpdtrp0(xc,X4) = X3
& aElementOf0(X4,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( ( sbrdtbr0(X0) = xK
& ( aSubsetOf0(X0,xS)
| ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(X2,xS) )
& aSet0(X0) ) ) )
=> aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
=> ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(rectify,[],[f76]) ).
fof(f106,plain,
( 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))))
& ! [X2] :
( aElementOf0(X2,xQ)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(rectify,[],[f89]) ).
fof(f107,plain,
( ? [X4] :
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,X4)
& aElementOf0(X4,szDzozmdt0(xc)) )
& ! [X3] :
( aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(rectify,[],[f90]) ).
fof(f108,plain,
~ aElementOf0(xx,xT),
inference(flattening,[],[f92]) ).
fof(f115,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f118,plain,
! [X0] :
( ~ aSet0(X0)
| aSubsetOf0(X0,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f119,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f13]) ).
fof(f120,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f119]) ).
fof(f209,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X5] :
( ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X5,xT) )
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( sdtlpdtrp0(xc,X4) = X3
& aElementOf0(X4,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( sbrdtbr0(X0) != xK
| ( ~ aSubsetOf0(X0,xS)
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ aElementOf0(X2,xS) )
| ~ aSet0(X0) ) )
| aElementOf0(X0,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X0,szDzozmdt0(xc))
| ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( ~ aElementOf0(X1,X0)
| aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(ennf_transformation,[],[f100]) ).
fof(f210,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X5] :
( ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X5,xT) )
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( sdtlpdtrp0(xc,X4) = X3
& aElementOf0(X4,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( sbrdtbr0(X0) != xK
| ( ~ aSubsetOf0(X0,xS)
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ aElementOf0(X2,xS) )
| ~ aSet0(X0) ) )
| aElementOf0(X0,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X0,szDzozmdt0(xc))
| ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( ~ aElementOf0(X1,X0)
| aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(flattening,[],[f209]) ).
fof(f224,plain,
( 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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(ennf_transformation,[],[f106]) ).
fof(f225,plain,
( ? [X4] :
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,X4)
& aElementOf0(X4,szDzozmdt0(xc)) )
& ! [X3] :
( aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(ennf_transformation,[],[f107]) ).
fof(f254,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f255,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(flattening,[],[f254]) ).
fof(f256,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(rectify,[],[f255]) ).
fof(f257,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ( aElementOf0(sK19(X0,X1),X1)
& ~ aElementOf0(sK19(X0,X1),X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X2,sK19(X0,X1))],[f256]) ).
fof(f309,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X5] :
( ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X5,xT) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ? [X4] :
( sdtlpdtrp0(xc,X4) = X3
& aElementOf0(X4,szDzozmdt0(xc)) ) )
& ( ! [X4] :
( sdtlpdtrp0(xc,X4) != X3
| ~ aElementOf0(X4,szDzozmdt0(xc)) )
| aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( sbrdtbr0(X0) != xK
| ( ~ aSubsetOf0(X0,xS)
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ aElementOf0(X2,xS) )
| ~ aSet0(X0) ) )
| aElementOf0(X0,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X0,szDzozmdt0(xc))
| ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( ~ aElementOf0(X1,X0)
| aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(nnf_transformation,[],[f210]) ).
fof(f310,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X6] :
( ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X6,xT) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ? [X5] :
( sdtlpdtrp0(xc,X5) = X3
& aElementOf0(X5,szDzozmdt0(xc)) ) )
& ( ! [X4] :
( sdtlpdtrp0(xc,X4) != X3
| ~ aElementOf0(X4,szDzozmdt0(xc)) )
| aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( sbrdtbr0(X0) != xK
| ( ~ aSubsetOf0(X0,xS)
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ aElementOf0(X2,xS) )
| ~ aSet0(X0) ) )
| aElementOf0(X0,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X0,szDzozmdt0(xc))
| ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( ~ aElementOf0(X1,X0)
| aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(rectify,[],[f309]) ).
fof(f311,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X6] :
( ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X6,xT) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ( sdtlpdtrp0(xc,sK38(X3)) = X3
& aElementOf0(sK38(X3),szDzozmdt0(xc)) ) )
& ( ! [X4] :
( sdtlpdtrp0(xc,X4) != X3
| ~ aElementOf0(X4,szDzozmdt0(xc)) )
| aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X0] :
( ( sbrdtbr0(X0) != xK
| ( ~ aSubsetOf0(X0,xS)
& ( ( aElementOf0(sK37(X0),X0)
& ~ aElementOf0(sK37(X0),xS) )
| ~ aSet0(X0) ) )
| aElementOf0(X0,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X0,szDzozmdt0(xc))
| ( sbrdtbr0(X0) = xK
& aSubsetOf0(X0,xS)
& ! [X1] :
( ~ aElementOf0(X1,X0)
| aElementOf0(X1,xS) )
& aSet0(X0) ) ) )
& aFunction0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37,sK38]),skolemize(X2,sK37(X0)),skolemize(X5,sK38(X3))],[f310]) ).
fof(f349,plain,
! [X0] :
( ~ sP15(X0)
| ! [X6] :
( sP14(X0,X6)
| ~ aSet0(X6)
| ( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X11] :
( ( ~ aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X11
| aElementOf0(X11,X6) )
& aElement0(X11) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X11
& ~ aElementOf0(X11,X6) )
| ~ aElement0(X11)
| aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& ! [X10] :
( ~ aElementOf0(X10,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) ),
inference(nnf_transformation,[],[f246]) ).
fof(f350,plain,
! [X0] :
( ~ sP15(X0)
| ! [X6] :
( sP14(X0,X6)
| ~ aSet0(X6)
| ( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X11] :
( ( ~ aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X11
| aElementOf0(X11,X6) )
& aElement0(X11) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X11
& ~ aElementOf0(X11,X6) )
| ~ aElement0(X11)
| aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& ! [X10] :
( ~ aElementOf0(X10,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) ),
inference(flattening,[],[f349]) ).
fof(f351,plain,
! [X0] :
( ~ sP15(X0)
| ! [X1] :
( sP14(X0,X1)
| ~ aSet0(X1)
| ( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| aElementOf0(X3,X1) )
& aElement0(X3) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& ~ aElementOf0(X3,X1) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) ),
inference(rectify,[],[f350]) ).
fof(f352,plain,
! [X0,X6] :
( ~ sP14(X0,X6)
| ( ! [X7] :
( ~ aElementOf0(X7,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X7) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& sP13(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X6,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& ( xk != sbrdtbr0(X6)
| ( ~ aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ? [X9] :
( aElementOf0(X9,X6)
& ~ aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ) ),
inference(nnf_transformation,[],[f245]) ).
fof(f353,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| ( ! [X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& sP13(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ) ),
inference(rectify,[],[f352]) ).
fof(f354,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| ( ! [X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& sP13(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(sK51(X0,X1),X1)
& ~ aElementOf0(sK51(X0,X1),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X2,sK51(X0,X1))],[f353]) ).
fof(f359,plain,
( 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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(nnf_transformation,[],[f224]) ).
fof(f360,plain,
( 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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(flattening,[],[f359]) ).
fof(f361,plain,
( ? [X4] :
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,X4)
& aElementOf0(X4,szDzozmdt0(xc)) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) ) )
& ( ( 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] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& ( ( 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] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(nnf_transformation,[],[f225]) ).
fof(f362,plain,
( ? [X4] :
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,X4)
& aElementOf0(X4,szDzozmdt0(xc)) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) ) )
& ( ( 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] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& ( ( 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] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(flattening,[],[f361]) ).
fof(f363,plain,
( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK53)
& aElementOf0(sK53,szDzozmdt0(xc))
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X3
| aElementOf0(X3,xQ) )
& aElement0(X3) ) )
& ( ( 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] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& ( ( 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] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X4,sK53)],[f362]) ).
fof(f372,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| aSet0(X1) ),
inference(cnf_transformation,[],[f257]) ).
fof(f376,plain,
! [X0] :
( ~ aSet0(X0)
| aSubsetOf0(X0,X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f377,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f120]) ).
fof(f508,plain,
aSet0(xT),
inference(cnf_transformation,[],[f73]) ).
fof(f515,plain,
! [X6] :
( ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X6,xT) ),
inference(cnf_transformation,[],[f311]) ).
fof(f518,plain,
! [X3,X4] :
( sdtlpdtrp0(xc,X4) != X3
| ~ aElementOf0(X4,szDzozmdt0(xc))
| aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(cnf_transformation,[],[f311]) ).
fof(f628,plain,
! [X0,X1] :
( ~ sP15(X0)
| sP14(X0,X1)
| ~ aSet0(X1)
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f351]) ).
fof(f639,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ),
inference(cnf_transformation,[],[f354]) ).
fof(f647,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sP15(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f657,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f87]) ).
fof(f661,plain,
xx = sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ),
inference(cnf_transformation,[],[f360]) ).
fof(f662,plain,
aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)),
inference(cnf_transformation,[],[f360]) ).
fof(f666,plain,
aSet0(xQ),
inference(cnf_transformation,[],[f360]) ).
fof(f674,plain,
sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK53),
inference(cnf_transformation,[],[f363]) ).
fof(f675,plain,
aElementOf0(sK53,szDzozmdt0(xc)),
inference(cnf_transformation,[],[f363]) ).
fof(f690,plain,
~ aElementOf0(xx,xT),
inference(cnf_transformation,[],[f108]) ).
fof(f728,plain,
! [X4] :
( ~ aElementOf0(X4,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X4),sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(equality_resolution,[],[f518]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( aSet0(X0)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_61,plain,
! [X0: $i] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_192,plain,
aSet0(xT),
inference(cnf_transformation,[],[f508]) ).
tcf(c_209,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xc,X0),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(cnf_transformation,[],[f728]) ).
tcf(c_212,plain,
! [X0: $i] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(cnf_transformation,[],[f515]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i] :
( sP14(X1,X0)
| ( sdtlpdtrp0(xc,sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,X1)))) = sdtlpdtrp0(sdtlpdtrp0(xC,X1),X0) )
| ~ sP15(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f628]) ).
tcf(c_323,plain,
! [X0: $i,X1: $i] :
( ~ sP14(X1,X0)
| ~ aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)) ),
inference(cnf_transformation,[],[f639]) ).
tcf(c_341,plain,
! [X0: $i] :
( sP15(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f647]) ).
tcf(c_342,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f657]) ).
tcf(c_353,plain,
aSet0(xQ),
inference(cnf_transformation,[],[f666]) ).
tcf(c_357,plain,
aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)),
inference(cnf_transformation,[],[f662]) ).
tcf(c_358,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) = xx,
inference(cnf_transformation,[],[f661]) ).
tcf(c_373,plain,
aElementOf0(sK53,szDzozmdt0(xc)),
inference(cnf_transformation,[],[f675]) ).
tcf(c_374,plain,
sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(xc,sK53),
inference(cnf_transformation,[],[f674]) ).
tcf(c_375,negated_conjecture,
~ aElementOf0(xx,xT),
inference(cnf_transformation,[],[f690]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_62,c_58,c_62]) ).
tcf(c_642,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(renaming,[status(thm)],[c_641]) ).
tcf(c_721,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_723,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( aElementOf0(X0,X2)
| ~ aElementOf0(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_816,plain,
( aElementOf0(sdtlpdtrp0(xc,sK53),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(sK53,szDzozmdt0(xc)) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_852,plain,
( sP15(xi)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_1803,plain,
( aSubsetOf0(xT,xT)
| ~ aSet0(xT) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_2785,plain,
( aElementOf0(sdtlpdtrp0(xc,sK53),xT)
| ~ aElementOf0(sdtlpdtrp0(xc,sK53),sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(instantiation,[status(thm)],[c_212]) ).
tcf(c_4578,plain,
( ( xT = xT )
| ~ aSet0(xT)
| ~ aSubsetOf0(xT,xT) ),
inference(instantiation,[status(thm)],[c_642]) ).
tcf(c_35703,plain,
xx = xx,
inference(instantiation,[status(thm)],[c_721]) ).
tcf(c_36185,plain,
! [X0: $i,X1: $i] :
( aElementOf0(xx,xT)
| ~ aElementOf0(X1,X0)
| ( xx != X1 )
| ( xT != X0 ) ),
inference(instantiation,[status(thm)],[c_725]) ).
tcf(c_36569,plain,
! [X0: $i,X1: $i] :
( ( xx = X0 )
| ( xx != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_38708,plain,
! [X0: $i] :
( ( xx = X0 )
| ( xx != xx )
| ( X0 != xx ) ),
inference(instantiation,[status(thm)],[c_36569]) ).
tcf(c_40913,plain,
( ( xx = sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) )
| ( xx != xx )
| ( sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) != xx ) ),
inference(instantiation,[status(thm)],[c_38708]) ).
tcf(c_43502,plain,
! [X0: $i] :
( ( xx = X0 )
| ( xx != sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) )
| ( X0 != sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) ) ),
inference(instantiation,[status(thm)],[c_36569]) ).
tcf(c_47035,plain,
( ( xx = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ( xx != sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) )
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) ) ),
inference(instantiation,[status(thm)],[c_43502]) ).
tcf(c_47036,plain,
( sP14(xi,xQ)
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) )
| ~ sP15(xi)
| ~ aSet0(xQ) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_51318,plain,
( ~ sP14(xi,xQ)
| ~ aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ),
inference(instantiation,[status(thm)],[c_323]) ).
tcf(c_55331,plain,
! [X0: $i] :
( aElementOf0(xx,xT)
| ~ aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),X0)
| ( xx != sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ( xT != X0 ) ),
inference(instantiation,[status(thm)],[c_36185]) ).
tcf(c_67889,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),X1)
| ~ aElementOf0(X0,X2)
| ( X1 != X2 )
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != X0 ) ),
inference(instantiation,[status(thm)],[c_725]) ).
tcf(c_68273,plain,
! [X0: $i,X1: $i] :
( aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),X0)
| ~ aElementOf0(sdtlpdtrp0(xc,sK53),X1)
| ( X0 != X1 )
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != sdtlpdtrp0(xc,sK53) ) ),
inference(instantiation,[status(thm)],[c_67889]) ).
tcf(c_72121,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),X0)
| ~ aElementOf0(sdtlpdtrp0(xc,sK53),xT)
| ( X0 != xT )
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != sdtlpdtrp0(xc,sK53) ) ),
inference(instantiation,[status(thm)],[c_68273]) ).
tcf(c_72243,plain,
( aElementOf0(xx,xT)
| ~ aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),xT)
| ( xx != sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ( xT != xT ) ),
inference(instantiation,[status(thm)],[c_55331]) ).
tcf(c_80211,plain,
( aElementOf0(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),xT)
| ~ aElementOf0(sdtlpdtrp0(xc,sK53),xT)
| ( xT != xT )
| ( sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != sdtlpdtrp0(xc,sK53) ) ),
inference(instantiation,[status(thm)],[c_72121]) ).
tcf(c_80212,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_80211,c_72243,c_51318,c_47036,c_47035,c_40913,c_35703,c_4578,c_2785,c_1803,c_852,c_816,c_374,c_357,c_358,c_373,c_375,c_342,c_192,c_353]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM587+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 04:46:57 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.38 Running first-order theorem proving
% 0.09/0.38 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.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 92.52/14.37 % SZS status Started for theBenchmark.p
% 92.52/14.37 % SZS status Theorem for theBenchmark.p
% 92.52/14.37
% 92.52/14.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 92.52/14.37
% 92.52/14.37 % ------ iProver source info
% 92.52/14.37
% 92.52/14.37 % git: date: 2026-07-19 20:42:38 +0200
% 92.52/14.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 92.52/14.37 % git: non_committed_changes: false
% 92.52/14.37
% 92.52/14.37 % ------ Parsing...
% 92.52/14.37 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 92.52/14.37
% 92.52/14.37 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 1 0s sf_e %
% 92.52/14.37
% 92.52/14.37 % ------ Preprocessing...%
% 92.52/14.37
% 92.52/14.37 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 92.52/14.37 % ------ Proving...
% 92.52/14.37 % ------ Problem Properties
% 92.52/14.37
% 92.52/14.37 %
% 92.52/14.37 % clauses 312
% 92.52/14.37 % conjectures 1
% 92.52/14.37 % EPR 57
% 92.52/14.37 % Horn 241
% 92.52/14.37 % unary 43
% 92.52/14.37 % binary 76
% 92.52/14.37 % lits 1006
% 92.52/14.37 % lits eq 127
% 92.52/14.37 % fd_pure 0
% 92.52/14.37 % fd_pseudo 0
% 92.52/14.37 % fd_cond 12
% 92.52/14.37 % fd_pseudo_cond 39
% 92.52/14.37 % AC symbols 0
% 92.52/14.37
% 92.52/14.37 % ------ Input Options Time Limit: Unbounded
% 92.52/14.37
% 92.52/14.37
% 92.52/14.37 % ------
% 92.52/14.37 % Current options:
% 92.52/14.37 % ------
% 92.52/14.37
% 92.52/14.37
% 92.52/14.37 %
% 92.52/14.37
% 92.52/14.37 % ------ Proving...
% 92.52/14.37 %
% 92.52/14.37
% 92.52/14.37 % SZS status Theorem for theBenchmark.p
% 92.52/14.37
% 92.52/14.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 92.52/14.38
% 92.52/14.38
%------------------------------------------------------------------------------