%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM587+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 : Thu Sep 24 01:49:40 PM UTC 2026
% Result : Theorem 3.94s 1.22s
% Output : CNFRefutation 3.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of formulae : 37 ( 16 unt; 0 def)
% Number of atoms : 856 ( 138 equ)
% Maximal formula atoms : 518 ( 23 avg)
% Number of connectives : 1240 ( 421 ~; 495 |; 260 &)
% ( 15 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 113 ( 9 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 12 con; 0-2 aty)
% Number of variables : 94 ( 0 sgn 85 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__4237,hypothesis,
( 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))))
& ! [X1] :
( aElementOf0(X1,xQ)
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( X1 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4237) ).
fof(m__4263,hypothesis,
( ? [X1] :
( sdtlpdtrp0(xc,X1) = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& aElementOf0(X1,szDzozmdt0(xc)) )
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X1 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X1 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4263) ).
fof(m__4151,hypothesis,
( ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( ! [X2] :
( ( ( ( ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) )
=> ( ( ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X3 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
=> ( aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))
| ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) ) ) ) ) ) )
& aSet0(X2) )
=> ( sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( ( X3 = szmzizndt0(sdtlpdtrp0(xN,X1))
| aElementOf0(X3,X2) )
& aElement0(X3) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) ) )
& szDzozmdt0(sdtlpdtrp0(xC,X1)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)
& ! [X2] :
( ( ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ( ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
=> aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))) )
& ( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1)))
=> ( sbrdtbr0(X2) = xk
& aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X2 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X2,sdtlpdtrp0(xN,X1))
& aElement0(X2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& aFunction0(sdtlpdtrp0(xC,X1)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4151) ).
fof(m__,conjecture,
aElementOf0(xx,xT),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(m__3453,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(X1,xT) )
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X2] :
( sdtlpdtrp0(xc,X2) = X1
& aElementOf0(X2,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [X1] :
( ( ( sbrdtbr0(X1) = xK
& ( aSubsetOf0(X1,xS)
| ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xS) )
& aSet0(X1) ) ) )
=> aElementOf0(X1,szDzozmdt0(xc)) )
& ( aElementOf0(X1,szDzozmdt0(xc))
=> ( sbrdtbr0(X1) = xK
& aSubsetOf0(X1,xS)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xS) )
& aSet0(X1) ) ) )
& aFunction0(xc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3453) ).
fof(mImgRng,axiom,
! [X1] :
( aFunction0(X1)
=> ! [X2] :
( aElementOf0(X2,szDzozmdt0(X1))
=> aElementOf0(sdtlpdtrp0(X1,X2),sdtlcdtrc0(X1,szDzozmdt0(X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mImgRng) ).
fof(m__4200,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4200) ).
fof(c_0_7,plain,
! [X1] :
( epred2_1(X1)
<=> ( ! [X2] :
( ( ( ( ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) )
=> ( ( ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X3 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
=> ( aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))
| ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) ) ) ) ) ) )
& aSet0(X2) )
=> ( sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( ( X3 = szmzizndt0(sdtlpdtrp0(xN,X1))
| aElementOf0(X3,X2) )
& aElement0(X3) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) ) )
& szDzozmdt0(sdtlpdtrp0(xC,X1)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)
& ! [X2] :
( ( ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ( ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
=> aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))) )
& ( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1)))
=> ( sbrdtbr0(X2) = xk
& aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X2 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X2,sdtlpdtrp0(xN,X1))
& aElement0(X2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& aFunction0(sdtlpdtrp0(xC,X1)) ) ),
introduced(definition) ).
fof(c_0_8,plain,
! [X1] :
( epred2_1(X1)
=> ( ! [X2] :
( ( ( ( ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) )
=> ( ( ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X3 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
=> ( aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))
| ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) ) ) ) ) ) )
& aSet0(X2) )
=> ( sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( ( X3 = szmzizndt0(sdtlpdtrp0(xN,X1))
| aElementOf0(X3,X2) )
& aElement0(X3) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) ) )
& szDzozmdt0(sdtlpdtrp0(xC,X1)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)
& ! [X2] :
( ( ( sbrdtbr0(X2) = xk
& ( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ( ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
=> aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))) )
& ( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1)))
=> ( sbrdtbr0(X2) = xk
& aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSet0(X2) ) ) )
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( X2 != szmzizndt0(sdtlpdtrp0(xN,X1))
& aElementOf0(X2,sdtlpdtrp0(xN,X1))
& aElement0(X2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& aFunction0(sdtlpdtrp0(xC,X1)) ) ),
inference(split_equiv,[status(thm)],[c_0_7]) ).
fof(c_0_9,hypothesis,
( 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))))
& ! [X1] :
( aElementOf0(X1,xQ)
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( X1 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(fof_simplification,[status(thm)],[m__4237]) ).
fof(c_0_10,plain,
! [X221,X222,X223,X224,X225,X226,X227,X229,X230,X231,X232,X234,X235,X236] :
( ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X229,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aSubsetOf0(X229,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| ~ aElementOf0(esk34_2(X221,X229),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sbrdtbr0(X229) != xk
| aElementOf0(esk34_2(X221,X229),X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(X232,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X232 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X232,sdtlpdtrp0(xN,X221))
| ~ aElement0(X232)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X231 != szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X231,sdtlpdtrp0(xN,X221))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| ~ aElementOf0(X231,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X231)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X230)
| ~ aElementOf0(X230,sdtlpdtrp0(xN,X221))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| sdtlpdtrp0(sdtlpdtrp0(xC,X221),X229) = sdtlpdtrp0(xc,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| X236 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| aElementOf0(X236,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElement0(X236)
| ~ aElementOf0(X236,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| X235 = szmzizndt0(sdtlpdtrp0(xN,X221))
| aElementOf0(X235,X229) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X235,sdtpldt0(X229,szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X235) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X234)
| ~ aElementOf0(X234,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aSet0(X229)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| szDzozmdt0(sdtlpdtrp0(xC,X221)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))),xk) )
& ( ~ epred2_1(X221)
| aElementOf0(X227,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| sbrdtbr0(X227) != xk
| ~ aSubsetOf0(X227,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| aElementOf0(X227,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| sbrdtbr0(X227) != xk
| ~ aSet0(X227)
| ~ aElementOf0(esk33_2(X221,X227),sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| aElementOf0(X227,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| sbrdtbr0(X227) != xk
| ~ aSet0(X227)
| aElementOf0(esk33_2(X221,X227),X227) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X225,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| sbrdtbr0(X225) = xk )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X225,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| aSubsetOf0(X225,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X225,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| aElementOf0(X226,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| ~ aElementOf0(X226,X225) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X225,szDzozmdt0(sdtlpdtrp0(xC,X221)))
| aSet0(X225) )
& ( ~ epred2_1(X221)
| aElementOf0(X224,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X224 = szmzizndt0(sdtlpdtrp0(xN,X221))
| ~ aElementOf0(X224,sdtlpdtrp0(xN,X221))
| ~ aElement0(X224) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X223,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| X223 != szmzizndt0(sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X223,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElementOf0(X223,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| ~ aElementOf0(X223,sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221))))
| aElement0(X223) )
& ( ~ epred2_1(X221)
| aSet0(sdtmndt0(sdtlpdtrp0(xN,X221),szmzizndt0(sdtlpdtrp0(xN,X221)))) )
& ( ~ epred2_1(X221)
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X221)),X222)
| ~ aElementOf0(X222,sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X221)),sdtlpdtrp0(xN,X221)) )
& ( ~ epred2_1(X221)
| aFunction0(sdtlpdtrp0(xC,X221)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])])])]) ).
fof(c_0_11,hypothesis,
! [X54,X55,X56] :
( 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))))
& ( aElementOf0(X56,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X56,xQ) )
& aSet0(xQ)
& ( aElementOf0(X55,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| X55 = szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X55,sdtlpdtrp0(xN,xi))
| ~ aElement0(X55) )
& ( ~ aElementOf0(X55,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| X55 != szmzizndt0(sdtlpdtrp0(xN,xi)) )
& ( ~ aElementOf0(X55,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| aElementOf0(X55,sdtlpdtrp0(xN,xi)) )
& ( ~ aElementOf0(X55,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| aElement0(X55) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X54)
| ~ aElementOf0(X54,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])]) ).
fof(c_0_12,hypothesis,
! [X57,X58,X59,X60] :
( sdtlpdtrp0(xc,esk15_0) = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& aElementOf0(esk15_0,szDzozmdt0(xc))
& ( aElementOf0(X60,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElement0(X60)
| X60 != szmzizndt0(sdtlpdtrp0(xN,xi)) )
& ( aElementOf0(X60,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElement0(X60)
| ~ aElementOf0(X60,xQ) )
& ( ~ aElementOf0(X60,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| X60 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X60,xQ) )
& ( ~ aElementOf0(X60,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| aElement0(X60) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X59)
| ~ aElementOf0(X59,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ( aElementOf0(X58,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElement0(X58)
| X58 != szmzizndt0(sdtlpdtrp0(xN,xi)) )
& ( aElementOf0(X58,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElement0(X58)
| ~ aElementOf0(X58,xQ) )
& ( ~ aElementOf0(X58,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| X58 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X58,xQ) )
& ( ~ aElementOf0(X58,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| aElement0(X58) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X57)
| ~ aElementOf0(X57,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__4263])])])])])]) ).
fof(c_0_13,hypothesis,
( ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> epred2_1(X1) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[m__4151]),c_0_7]) ).
fof(c_0_14,negated_conjecture,
~ aElementOf0(xx,xT),
inference(assume_negation,[status(cth)],[m__]) ).
fof(c_0_15,hypothesis,
! [X9,X10,X11,X13,X15,X16,X17] :
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ( aElementOf0(X17,xT)
| ~ aElementOf0(X17,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ( aElementOf0(X15,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| sdtlpdtrp0(xc,X16) != X15
| ~ aElementOf0(X16,szDzozmdt0(xc)) )
& ( ~ aElementOf0(X13,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| sdtlpdtrp0(xc,esk2_1(X13)) = X13 )
& ( ~ aElementOf0(X13,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(esk2_1(X13),szDzozmdt0(xc)) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ( aElementOf0(X11,szDzozmdt0(xc))
| sbrdtbr0(X11) != xK
| ~ aSubsetOf0(X11,xS) )
& ( aElementOf0(X11,szDzozmdt0(xc))
| sbrdtbr0(X11) != xK
| ~ aSet0(X11)
| ~ aElementOf0(esk1_1(X11),xS) )
& ( aElementOf0(X11,szDzozmdt0(xc))
| sbrdtbr0(X11) != xK
| ~ aSet0(X11)
| aElementOf0(esk1_1(X11),X11) )
& ( ~ aElementOf0(X9,szDzozmdt0(xc))
| sbrdtbr0(X9) = xK )
& ( ~ aElementOf0(X9,szDzozmdt0(xc))
| aSubsetOf0(X9,xS) )
& ( ~ aElementOf0(X9,szDzozmdt0(xc))
| aElementOf0(X10,xS)
| ~ aElementOf0(X10,X9) )
& ( ~ aElementOf0(X9,szDzozmdt0(xc))
| aSet0(X9) )
& aFunction0(xc) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[m__3453])])])])])])]) ).
fof(c_0_16,plain,
! [X103,X104] :
( aElementOf0(sdtlpdtrp0(X103,X104),sdtlcdtrc0(X103,szDzozmdt0(X103)))
| ~ aElementOf0(X104,szDzozmdt0(X103))
| ~ aFunction0(X103) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mImgRng])])])]) ).
cnf(c_0_17,plain,
( ~ epred2_1(X1)
| ~ aSet0(X2)
| sbrdtbr0(X2) != xk
| ~ aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_18,hypothesis,
aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_19,hypothesis,
sdtlpdtrp0(xc,esk15_0) = sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_20,hypothesis,
sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ) = xx,
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_21,hypothesis,
sbrdtbr0(xQ) = xk,
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_22,hypothesis,
aSet0(xQ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
fof(c_0_23,hypothesis,
! [X52] :
( ( epred2_1(X52)
| ~ aElementOf0(X52,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])]) ).
fof(c_0_24,negated_conjecture,
~ aElementOf0(xx,xT),
inference(fof_simplification,[status(thm)],[c_0_14]) ).
cnf(c_0_25,hypothesis,
( ~ aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X1,xT) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_26,plain,
( ~ aElementOf0(X2,szDzozmdt0(X1))
| ~ aFunction0(X1)
| aElementOf0(sdtlpdtrp0(X1,X2),sdtlcdtrc0(X1,szDzozmdt0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_27,hypothesis,
aFunction0(xc),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_28,hypothesis,
( ~ epred2_1(xi)
| sdtlpdtrp0(xc,esk15_0) = xx ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_19]),c_0_20]),c_0_21]),c_0_22])]) ).
cnf(c_0_29,hypothesis,
( ~ aElementOf0(X1,szNzAzT0)
| epred2_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_30,hypothesis,
aElementOf0(xi,szNzAzT0),
inference(split_conjunct,[status(thm)],[m__4200]) ).
fof(c_0_31,negated_conjecture,
~ aElementOf0(xx,xT),
inference(fof_nnf,[status(thm)],[c_0_24]) ).
cnf(c_0_32,hypothesis,
( ~ aElementOf0(X1,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X1),xT) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_27])]) ).
cnf(c_0_33,hypothesis,
sdtlpdtrp0(xc,esk15_0) = xx,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30])]) ).
cnf(c_0_34,hypothesis,
aElementOf0(esk15_0,szDzozmdt0(xc)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_35,negated_conjecture,
~ aElementOf0(xx,xT),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_36,hypothesis,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_34])]),c_0_35]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM587+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n001.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 02:47:59 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.94/1.22 % Version: 3.5.1
% 3.94/1.22 % Preprocessing class: FSLSSMSMSSSNFFN.
% 3.94/1.22 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.94/1.22 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 3.94/1.22 % Starting new_bool_3 with 300s (1) cores
% 3.94/1.22 % Starting new_bool_1 with 300s (1) cores
% 3.94/1.22 % Starting sh5l with 300s (1) cores
% 3.94/1.22 % new_bool_3 with pid 2024937 completed with status 0
% 3.94/1.22 % Result found by new_bool_3
% 3.94/1.22 % Preprocessing class: FSLSSMSMSSSNFFN.
% 3.94/1.22 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.94/1.22 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 3.94/1.22 % Starting new_bool_3 with 300s (1) cores
% 3.94/1.22 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 3.94/1.22 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 3.94/1.22 % Search class: FGHSF-SMLM32-MFFFFFNN
% 3.94/1.22 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 3.94/1.22 % Starting SubtermCWHack with 31s (1) cores
% 3.94/1.22 % SubtermCWHack with pid 2024943 completed with status 0
% 3.94/1.22 % Result found by SubtermCWHack
% 3.94/1.22 % Preprocessing class: FSLSSMSMSSSNFFN.
% 3.94/1.22 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.94/1.22 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 3.94/1.22 % Starting new_bool_3 with 300s (1) cores
% 3.94/1.22 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 3.94/1.22 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 3.94/1.22 % Search class: FGHSF-SMLM32-MFFFFFNN
% 3.94/1.22 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 3.94/1.22 % Starting SubtermCWHack with 31s (1) cores
% 3.94/1.22 % Preprocessing time : 0.049 s
% 3.94/1.22
% 3.94/1.22 % Proof found!
% 3.94/1.22 % SZS status Theorem
% 3.94/1.22 % SZS output start CNFRefutation
% See solution above
% 3.94/1.22 % Parsed axioms : 91
% 3.94/1.22 % Removed by relevancy pruning/SinE : 5
% 3.94/1.22 % Initial clauses : 4419
% 3.94/1.22 % Removed in clause preprocessing : 7
% 3.94/1.22 % Initial clauses in saturation : 4412
% 3.94/1.22 % Processed clauses : 3973
% 3.94/1.22 % ...of these trivial : 39
% 3.94/1.22 % ...subsumed : 1987
% 3.94/1.22 % ...remaining for further processing : 1947
% 3.94/1.22 % Other redundant clauses eliminated : 84
% 3.94/1.22 % Clauses deleted for lack of memory : 0
% 3.94/1.22 % Backward-subsumed : 248
% 3.94/1.22 % Backward-rewritten : 173
% 3.94/1.22 % Generated clauses : 14979
% 3.94/1.22 % ...of the previous two non-redundant : 12926
% 3.94/1.22 % ...aggressively subsumed : 0
% 3.94/1.22 % Contextual simplify-reflections : 79
% 3.94/1.22 % Paramodulations : 14895
% 3.94/1.22 % Factorizations : 0
% 3.94/1.22 % NegExts : 0
% 3.94/1.22 % Equation resolutions : 86
% 3.94/1.22 % Disequality decompositions : 0
% 3.94/1.22 % Total rewrite steps : 9192
% 3.94/1.22 % ...of those cached : 9089
% 3.94/1.22 % Propositional unsat checks : 0
% 3.94/1.22 % Propositional check models : 0
% 3.94/1.22 % Propositional check unsatisfiable : 0
% 3.94/1.22 % Propositional clauses : 0
% 3.94/1.22 % Propositional clauses after purity: 0
% 3.94/1.22 % Propositional unsat core size : 0
% 3.94/1.22 % Propositional preprocessing time : 0.000
% 3.94/1.22 % Propositional encoding time : 0.000
% 3.94/1.22 % Propositional solver time : 0.000
% 3.94/1.22 % Success case prop preproc time : 0.000
% 3.94/1.22 % Success case prop encoding time : 0.000
% 3.94/1.22 % Success case prop solver time : 0.000
% 3.94/1.22 % Current number of processed clauses : 1459
% 3.94/1.22 % Positive orientable unit clauses : 110
% 3.94/1.22 % Positive unorientable unit clauses: 0
% 3.94/1.22 % Negative unit clauses : 32
% 3.94/1.22 % Non-unit-clauses : 1317
% 3.94/1.22 % Current number of unprocessed clauses: 12408
% 3.94/1.22 % ...number of literals in the above : 94506
% 3.94/1.22 % Current number of archived formulas : 0
% 3.94/1.22 % Current number of archived clauses : 424
% 3.94/1.22 % Clause-clause subsumption calls (NU) : 407047
% 3.94/1.22 % Rec. Clause-clause subsumption calls : 127152
% 3.94/1.22 % Non-unit clause-clause subsumptions : 1807
% 3.94/1.22 % Unit Clause-clause subsumption calls : 4992
% 3.94/1.22 % Rewrite failures with RHS unbound : 0
% 3.94/1.22 % BW rewrite match attempts : 49
% 3.94/1.22 % BW rewrite match successes : 34
% 3.94/1.22 % Condensation attempts : 0
% 3.94/1.22 % Condensation successes : 0
% 3.94/1.22 % Termbank termtop insertions : 610858
% 3.94/1.22 % Search garbage collected termcells : 28242
% 3.94/1.22
% 3.94/1.22 % -------------------------------------------------
% 3.94/1.22 % User time : 0.702 s
% 3.94/1.22 % System time : 0.044 s
% 3.94/1.22 % Total time : 0.746 s
% 3.94/1.22 % Maximum resident set size: 15308 pages
% 3.94/1.22
% 3.94/1.22 % -------------------------------------------------
% 3.94/1.22 % User time : 0.705 s
% 3.94/1.22 % System time : 0.050 s
% 3.94/1.22 % Total time : 0.755 s
% 3.94/1.22 % Maximum resident set size: 4864 pages
% 3.94/1.22 % E exiting
%------------------------------------------------------------------------------