%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : LAT385+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 08:48:28 AM UTC 2026
% Result : Theorem 0.16s 5.60s
% Output : Proof 0.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(mSetSort,axiom,
! [W0] :
( aSet0(W0)
=> $true ),
file('theBenchmark.p',mSetSort) ).
fof(mElmSort,axiom,
! [W0] :
( aElement0(W0)
=> $true ),
file('theBenchmark.p',mElmSort) ).
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefEmpty,definition,
! [W0] :
( aSet0(W0)
=> ( isEmpty0(W0)
<=> ~ ? [W1] : aElementOf0(W1,W0) ) ),
file('theBenchmark.p',mDefEmpty) ).
fof(mDefSub,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('theBenchmark.p',mDefSub) ).
fof(mLessRel,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( sdtlseqdt0(W0,W1)
=> $true ) ),
file('theBenchmark.p',mLessRel) ).
fof(mARefl,axiom,
! [W0] :
( aElement0(W0)
=> sdtlseqdt0(W0,W0) ),
file('theBenchmark.p',mARefl) ).
fof(mASymm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mASymm) ).
fof(mTrans,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('theBenchmark.p',mTrans) ).
fof(mDefLB,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2] :
( aLowerBoundOfIn0(W2,W1,W0)
<=> ( ! [W3] :
( aElementOf0(W3,W1)
=> sdtlseqdt0(W2,W3) )
& aElementOf0(W2,W0) ) ) ) ),
file('theBenchmark.p',mDefLB) ).
fof(mDefUB,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2] :
( aUpperBoundOfIn0(W2,W1,W0)
<=> ( ! [W3] :
( aElementOf0(W3,W1)
=> sdtlseqdt0(W3,W2) )
& aElementOf0(W2,W0) ) ) ) ),
file('theBenchmark.p',mDefUB) ).
fof(mDefInf,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2] :
( aInfimumOfIn0(W2,W1,W0)
<=> ( ! [W3] :
( aLowerBoundOfIn0(W3,W1,W0)
=> sdtlseqdt0(W3,W2) )
& aLowerBoundOfIn0(W2,W1,W0)
& aElementOf0(W2,W0) ) ) ) ),
file('theBenchmark.p',mDefInf) ).
fof(mDefSup,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2] :
( aSupremumOfIn0(W2,W1,W0)
<=> ( ! [W3] :
( aUpperBoundOfIn0(W3,W1,W0)
=> sdtlseqdt0(W2,W3) )
& aUpperBoundOfIn0(W2,W1,W0)
& aElementOf0(W2,W0) ) ) ) ),
file('theBenchmark.p',mDefSup) ).
fof(mSupUn,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2,W3] :
( ( aSupremumOfIn0(W3,W1,W0)
& aSupremumOfIn0(W2,W1,W0) )
=> W2 = W3 ) ) ),
file('theBenchmark.p',mSupUn) ).
fof(mInfUn,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> ! [W2,W3] :
( ( aInfimumOfIn0(W3,W1,W0)
& aInfimumOfIn0(W2,W1,W0) )
=> W2 = W3 ) ) ),
file('theBenchmark.p',mInfUn) ).
fof(mDefCLat,definition,
! [W0] :
( aCompleteLattice0(W0)
<=> ( ! [W1] :
( aSubsetOf0(W1,W0)
=> ? [W2] :
( ? [W3] : aSupremumOfIn0(W3,W1,W0)
& aInfimumOfIn0(W2,W1,W0) ) )
& aSet0(W0) ) ),
file('theBenchmark.p',mDefCLat) ).
fof(mConMap,axiom,
! [W0] :
( aFunction0(W0)
=> $true ),
file('theBenchmark.p',mConMap) ).
fof(mDomSort,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('theBenchmark.p',mDomSort) ).
fof(mRanSort,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szRzazndt0(W0)) ),
file('theBenchmark.p',mRanSort) ).
fof(mDefDom,definition,
! [W0,W1] :
( ( aSet0(W1)
& aFunction0(W0) )
=> ( isOn0(W0,W1)
<=> ( szRzazndt0(W0) = W1
& szDzozmdt0(W0) = szRzazndt0(W0) ) ) ),
file('theBenchmark.p',mDefDom) ).
fof(mImgSort,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),szRzazndt0(W0)) ) ),
file('theBenchmark.p',mImgSort) ).
fof(mDefFix,definition,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aFixedPointOf0(W1,W0)
<=> ( sdtlpdtrp0(W0,W1) = W1
& aElementOf0(W1,szDzozmdt0(W0)) ) ) ),
file('theBenchmark.p',mDefFix) ).
fof(mDefMonot,definition,
! [W0] :
( aFunction0(W0)
=> ( isMonotone0(W0)
<=> ! [W1,W2] :
( ( aElementOf0(W2,szDzozmdt0(W0))
& aElementOf0(W1,szDzozmdt0(W0)) )
=> ( sdtlseqdt0(W1,W2)
=> sdtlseqdt0(sdtlpdtrp0(W0,W1),sdtlpdtrp0(W0,W2)) ) ) ) ),
file('theBenchmark.p',mDefMonot) ).
fof(m__1123,hypothesis,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( ( aElementOf0(W1,szDzozmdt0(xf))
& aElementOf0(W0,szDzozmdt0(xf)) )
=> ( sdtlseqdt0(W0,W1)
=> sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xU) )
& aSet0(W0) ) )
=> ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( ( aUpperBoundOfIn0(W3,W0,xU)
| ( ! [W4] :
( aElementOf0(W4,W0)
=> sdtlseqdt0(W4,W3) )
& aElementOf0(W3,xU) ) )
=> sdtlseqdt0(W2,W3) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W3,W2) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( ( aLowerBoundOfIn0(W2,W0,xU)
| ( ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W2,W3) )
& aElementOf0(W2,xU) ) )
=> sdtlseqdt0(W2,W1) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) ) )
& aSet0(xU) ),
file('theBenchmark.p',m__1123) ).
fof(m__1144,hypothesis,
( xS = cS1142(xf)
& ! [W0] :
( ( ( aFixedPointOf0(W0,xf)
| ( sdtlpdtrp0(xf,W0) = W0
& aElementOf0(W0,szDzozmdt0(xf)) ) )
=> aElementOf0(W0,xS) )
& ( aElementOf0(W0,xS)
=> ( aFixedPointOf0(W0,xf)
& sdtlpdtrp0(xf,W0) = W0
& aElementOf0(W0,szDzozmdt0(xf)) ) ) )
& aSet0(xS) ),
file('theBenchmark.p',m__1144) ).
fof(m__1173,hypothesis,
( aSubsetOf0(xT,xS)
& ! [W0] :
( aElementOf0(W0,xT)
=> aElementOf0(W0,xS) )
& aSet0(xT) ),
file('theBenchmark.p',m__1173) ).
fof(m__1244,hypothesis,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( ( ( ( aUpperBoundOfIn0(W0,xT,xU)
| ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) ) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
=> aElementOf0(W0,xP) )
& ( aElementOf0(W0,xP)
=> ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) ) ) )
& aSet0(xP) ),
file('theBenchmark.p',m__1244) ).
fof(m__,conjecture,
? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
file('theBenchmark.p',m__) ).
fof(f_1_1,plain,
! [W0] :
( $true
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mSetSort]) ).
fof(f_1_2,plain,
! [U_0] :
( $true
| ~ aSet0(U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_0] : ~ aSet0(U_0)
| $true ),
inference(miniscope,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( ~ aSet0(U_0)
| $true ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [W0] :
( $true
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mElmSort]) ).
fof(f_2_2,plain,
! [U_1] :
( $true
| ~ aElement0(U_1) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_1] : ~ aElement0(U_1)
| $true ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( ~ aElement0(U_1)
| $true ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mEOfElem]) ).
fof(f_3_2,plain,
! [U_3] :
( ! [U_2] :
( aElement0(U_2)
| ~ aElementOf0(U_2,U_3) )
| ~ aSet0(U_3) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( aElement0(U_2)
| ~ aElementOf0(U_2,U_3)
| ~ aSet0(U_3) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [W0] :
( ( ( isEmpty0(W0)
| ? [W1] : aElementOf0(W1,W0) )
& ( ! [W1] : ~ aElementOf0(W1,W0)
| ~ isEmpty0(W0) ) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefEmpty]) ).
fof(f_4_2,plain,
! [U_6] :
( ( ( isEmpty0(U_6)
| ? [U_5] : aElementOf0(U_5,U_6) )
& ( ! [U_4] : ~ aElementOf0(U_4,U_6)
| ~ isEmpty0(U_6) ) )
| ~ aSet0(U_6) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_6] :
( ( ( isEmpty0(U_6)
| aElementOf0(sK1(U_6),U_6) )
& ( ! [U_4] : ~ aElementOf0(U_4,U_6)
| ~ isEmpty0(U_6) ) )
| ~ aSet0(U_6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_5,sK1(U_6))],[f_4_2]) ).
cnf(f_4_4,plain,
( ~ aElementOf0(U_4,U_6)
| ~ isEmpty0(U_6)
| ~ aSet0(U_6) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( isEmpty0(U_6)
| aElementOf0(sK1(U_6),U_6)
| ~ aSet0(U_6) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [W0] :
( ! [W1] :
( ( aSubsetOf0(W1,W0)
| ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefSub]) ).
fof(f_5_2,plain,
! [U_10] :
( ! [U_9] :
( ( aSubsetOf0(U_9,U_10)
| ? [U_8] :
( ~ aElementOf0(U_8,U_10)
& aElementOf0(U_8,U_9) )
| ~ aSet0(U_9) )
& ( ( ! [U_7] :
( aElementOf0(U_7,U_10)
| ~ aElementOf0(U_7,U_9) )
& aSet0(U_9) )
| ~ aSubsetOf0(U_9,U_10) ) )
| ~ aSet0(U_10) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_10] :
( ( ! [U_12] :
( aSubsetOf0(U_12,U_10)
| ? [U_8] :
( ~ aElementOf0(U_8,U_10)
& aElementOf0(U_8,U_12) )
| ~ aSet0(U_12) )
& ! [U_11] :
( ( ! [U_7] :
( aElementOf0(U_7,U_10)
| ~ aElementOf0(U_7,U_11) )
& aSet0(U_11) )
| ~ aSubsetOf0(U_11,U_10) ) )
| ~ aSet0(U_10) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
! [U_10] :
( ( ! [U_12] :
( aSubsetOf0(U_12,U_10)
| ( ~ aElementOf0(sK2(U_10,U_12),U_10)
& aElementOf0(sK2(U_10,U_12),U_12) )
| ~ aSet0(U_12) )
& ! [U_11] :
( ( ! [U_7] :
( aElementOf0(U_7,U_10)
| ~ aElementOf0(U_7,U_11) )
& aSet0(U_11) )
| ~ aSubsetOf0(U_11,U_10) ) )
| ~ aSet0(U_10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_8,sK2(U_10,U_12))],[f_5_3]) ).
cnf(f_5_5,plain,
( aSet0(U_11)
| ~ aSubsetOf0(U_11,U_10)
| ~ aSet0(U_10) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( aElementOf0(U_7,U_10)
| ~ aElementOf0(U_7,U_11)
| ~ aSubsetOf0(U_11,U_10)
| ~ aSet0(U_10) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( aElementOf0(sK2(U_10,U_12),U_12)
| ~ aSet0(U_12)
| aSubsetOf0(U_12,U_10)
| ~ aSet0(U_10) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_8,plain,
( ~ aElementOf0(sK2(U_10,U_12),U_10)
| ~ aSet0(U_12)
| aSubsetOf0(U_12,U_10)
| ~ aSet0(U_10) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [W0,W1] :
( $true
| ~ sdtlseqdt0(W0,W1)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mLessRel]) ).
fof(f_6_2,plain,
! [U_14,U_13] :
( $true
| ~ sdtlseqdt0(U_14,U_13)
| ~ aElement0(U_13)
| ~ aElement0(U_14) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( $true
| ~ sdtlseqdt0(U_14,U_13)
| ~ aElement0(U_13)
| ~ aElement0(U_14) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mARefl]) ).
fof(f_7_2,plain,
! [U_15] :
( sdtlseqdt0(U_15,U_15)
| ~ aElement0(U_15) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( sdtlseqdt0(U_15,U_15)
| ~ aElement0(U_15) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mASymm]) ).
fof(f_8_2,plain,
! [U_17,U_16] :
( U_17 = U_16
| ~ sdtlseqdt0(U_16,U_17)
| ~ sdtlseqdt0(U_17,U_16)
| ~ aElement0(U_16)
| ~ aElement0(U_17) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( U_17 = U_16
| ~ sdtlseqdt0(U_16,U_17)
| ~ sdtlseqdt0(U_17,U_16)
| ~ aElement0(U_16)
| ~ aElement0(U_17) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mTrans]) ).
fof(f_9_2,plain,
! [U_20,U_19,U_18] :
( sdtlseqdt0(U_20,U_18)
| ~ sdtlseqdt0(U_19,U_18)
| ~ sdtlseqdt0(U_20,U_19)
| ~ aElement0(U_18)
| ~ aElement0(U_19)
| ~ aElement0(U_20) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( sdtlseqdt0(U_20,U_18)
| ~ sdtlseqdt0(U_19,U_18)
| ~ sdtlseqdt0(U_20,U_19)
| ~ aElement0(U_18)
| ~ aElement0(U_19)
| ~ aElement0(U_20) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( aLowerBoundOfIn0(W2,W1,W0)
| ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aElementOf0(W3,W1) )
| ~ aElementOf0(W2,W0) )
& ( ( ! [W3] :
( sdtlseqdt0(W2,W3)
| ~ aElementOf0(W3,W1) )
& aElementOf0(W2,W0) )
| ~ aLowerBoundOfIn0(W2,W1,W0) ) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefLB]) ).
fof(f_10_2,plain,
! [U_25] :
( ! [U_24] :
( ! [U_23] :
( ( aLowerBoundOfIn0(U_23,U_24,U_25)
| ? [U_22] :
( ~ sdtlseqdt0(U_23,U_22)
& aElementOf0(U_22,U_24) )
| ~ aElementOf0(U_23,U_25) )
& ( ( ! [U_21] :
( sdtlseqdt0(U_23,U_21)
| ~ aElementOf0(U_21,U_24) )
& aElementOf0(U_23,U_25) )
| ~ aLowerBoundOfIn0(U_23,U_24,U_25) ) )
| ~ aSubsetOf0(U_24,U_25) )
| ~ aSet0(U_25) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
! [U_25] :
( ! [U_24] :
( ( ! [U_27] :
( aLowerBoundOfIn0(U_27,U_24,U_25)
| ? [U_22] :
( ~ sdtlseqdt0(U_27,U_22)
& aElementOf0(U_22,U_24) )
| ~ aElementOf0(U_27,U_25) )
& ! [U_26] :
( ( ! [U_21] :
( sdtlseqdt0(U_26,U_21)
| ~ aElementOf0(U_21,U_24) )
& aElementOf0(U_26,U_25) )
| ~ aLowerBoundOfIn0(U_26,U_24,U_25) ) )
| ~ aSubsetOf0(U_24,U_25) )
| ~ aSet0(U_25) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
! [U_25] :
( ! [U_24] :
( ( ! [U_27] :
( aLowerBoundOfIn0(U_27,U_24,U_25)
| ( ~ sdtlseqdt0(U_27,sK3(U_25,U_24,U_27))
& aElementOf0(sK3(U_25,U_24,U_27),U_24) )
| ~ aElementOf0(U_27,U_25) )
& ! [U_26] :
( ( ! [U_21] :
( sdtlseqdt0(U_26,U_21)
| ~ aElementOf0(U_21,U_24) )
& aElementOf0(U_26,U_25) )
| ~ aLowerBoundOfIn0(U_26,U_24,U_25) ) )
| ~ aSubsetOf0(U_24,U_25) )
| ~ aSet0(U_25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_22,sK3(U_25,U_24,U_27))],[f_10_3]) ).
cnf(f_10_5,plain,
( aElementOf0(U_26,U_25)
| ~ aLowerBoundOfIn0(U_26,U_24,U_25)
| ~ aSubsetOf0(U_24,U_25)
| ~ aSet0(U_25) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_6,plain,
( sdtlseqdt0(U_26,U_21)
| ~ aElementOf0(U_21,U_24)
| ~ aLowerBoundOfIn0(U_26,U_24,U_25)
| ~ aSubsetOf0(U_24,U_25)
| ~ aSet0(U_25) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_7,plain,
( aElementOf0(sK3(U_25,U_24,U_27),U_24)
| ~ aElementOf0(U_27,U_25)
| aLowerBoundOfIn0(U_27,U_24,U_25)
| ~ aSubsetOf0(U_24,U_25)
| ~ aSet0(U_25) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_8,plain,
( ~ sdtlseqdt0(U_27,sK3(U_25,U_24,U_27))
| ~ aElementOf0(U_27,U_25)
| aLowerBoundOfIn0(U_27,U_24,U_25)
| ~ aSubsetOf0(U_24,U_25)
| ~ aSet0(U_25) ),
inference(clausify,[status(thm)],[f_10_4]) ).
fof(f_11_1,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( aUpperBoundOfIn0(W2,W1,W0)
| ? [W3] :
( ~ sdtlseqdt0(W3,W2)
& aElementOf0(W3,W1) )
| ~ aElementOf0(W2,W0) )
& ( ( ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aElementOf0(W3,W1) )
& aElementOf0(W2,W0) )
| ~ aUpperBoundOfIn0(W2,W1,W0) ) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefUB]) ).
fof(f_11_2,plain,
! [U_32] :
( ! [U_31] :
( ! [U_30] :
( ( aUpperBoundOfIn0(U_30,U_31,U_32)
| ? [U_29] :
( ~ sdtlseqdt0(U_29,U_30)
& aElementOf0(U_29,U_31) )
| ~ aElementOf0(U_30,U_32) )
& ( ( ! [U_28] :
( sdtlseqdt0(U_28,U_30)
| ~ aElementOf0(U_28,U_31) )
& aElementOf0(U_30,U_32) )
| ~ aUpperBoundOfIn0(U_30,U_31,U_32) ) )
| ~ aSubsetOf0(U_31,U_32) )
| ~ aSet0(U_32) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_32] :
( ! [U_31] :
( ( ! [U_34] :
( aUpperBoundOfIn0(U_34,U_31,U_32)
| ? [U_29] :
( ~ sdtlseqdt0(U_29,U_34)
& aElementOf0(U_29,U_31) )
| ~ aElementOf0(U_34,U_32) )
& ! [U_33] :
( ( ! [U_28] :
( sdtlseqdt0(U_28,U_33)
| ~ aElementOf0(U_28,U_31) )
& aElementOf0(U_33,U_32) )
| ~ aUpperBoundOfIn0(U_33,U_31,U_32) ) )
| ~ aSubsetOf0(U_31,U_32) )
| ~ aSet0(U_32) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
! [U_32] :
( ! [U_31] :
( ( ! [U_34] :
( aUpperBoundOfIn0(U_34,U_31,U_32)
| ( ~ sdtlseqdt0(sK4(U_32,U_31,U_34),U_34)
& aElementOf0(sK4(U_32,U_31,U_34),U_31) )
| ~ aElementOf0(U_34,U_32) )
& ! [U_33] :
( ( ! [U_28] :
( sdtlseqdt0(U_28,U_33)
| ~ aElementOf0(U_28,U_31) )
& aElementOf0(U_33,U_32) )
| ~ aUpperBoundOfIn0(U_33,U_31,U_32) ) )
| ~ aSubsetOf0(U_31,U_32) )
| ~ aSet0(U_32) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_29,sK4(U_32,U_31,U_34))],[f_11_3]) ).
cnf(f_11_5,plain,
( aElementOf0(U_33,U_32)
| ~ aUpperBoundOfIn0(U_33,U_31,U_32)
| ~ aSubsetOf0(U_31,U_32)
| ~ aSet0(U_32) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( sdtlseqdt0(U_28,U_33)
| ~ aElementOf0(U_28,U_31)
| ~ aUpperBoundOfIn0(U_33,U_31,U_32)
| ~ aSubsetOf0(U_31,U_32)
| ~ aSet0(U_32) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( aElementOf0(sK4(U_32,U_31,U_34),U_31)
| ~ aElementOf0(U_34,U_32)
| aUpperBoundOfIn0(U_34,U_31,U_32)
| ~ aSubsetOf0(U_31,U_32)
| ~ aSet0(U_32) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_8,plain,
( ~ sdtlseqdt0(sK4(U_32,U_31,U_34),U_34)
| ~ aElementOf0(U_34,U_32)
| aUpperBoundOfIn0(U_34,U_31,U_32)
| ~ aSubsetOf0(U_31,U_32)
| ~ aSet0(U_32) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( aInfimumOfIn0(W2,W1,W0)
| ? [W3] :
( ~ sdtlseqdt0(W3,W2)
& aLowerBoundOfIn0(W3,W1,W0) )
| ~ aLowerBoundOfIn0(W2,W1,W0)
| ~ aElementOf0(W2,W0) )
& ( ( ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aLowerBoundOfIn0(W3,W1,W0) )
& aLowerBoundOfIn0(W2,W1,W0)
& aElementOf0(W2,W0) )
| ~ aInfimumOfIn0(W2,W1,W0) ) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefInf]) ).
fof(f_12_2,plain,
! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ( aInfimumOfIn0(U_37,U_38,U_39)
| ? [U_36] :
( ~ sdtlseqdt0(U_36,U_37)
& aLowerBoundOfIn0(U_36,U_38,U_39) )
| ~ aLowerBoundOfIn0(U_37,U_38,U_39)
| ~ aElementOf0(U_37,U_39) )
& ( ( ! [U_35] :
( sdtlseqdt0(U_35,U_37)
| ~ aLowerBoundOfIn0(U_35,U_38,U_39) )
& aLowerBoundOfIn0(U_37,U_38,U_39)
& aElementOf0(U_37,U_39) )
| ~ aInfimumOfIn0(U_37,U_38,U_39) ) )
| ~ aSubsetOf0(U_38,U_39) )
| ~ aSet0(U_39) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_39] :
( ! [U_38] :
( ( ! [U_41] :
( aInfimumOfIn0(U_41,U_38,U_39)
| ? [U_36] :
( ~ sdtlseqdt0(U_36,U_41)
& aLowerBoundOfIn0(U_36,U_38,U_39) )
| ~ aLowerBoundOfIn0(U_41,U_38,U_39)
| ~ aElementOf0(U_41,U_39) )
& ! [U_40] :
( ( ! [U_35] :
( sdtlseqdt0(U_35,U_40)
| ~ aLowerBoundOfIn0(U_35,U_38,U_39) )
& aLowerBoundOfIn0(U_40,U_38,U_39)
& aElementOf0(U_40,U_39) )
| ~ aInfimumOfIn0(U_40,U_38,U_39) ) )
| ~ aSubsetOf0(U_38,U_39) )
| ~ aSet0(U_39) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
! [U_39] :
( ! [U_38] :
( ( ! [U_41] :
( aInfimumOfIn0(U_41,U_38,U_39)
| ( ~ sdtlseqdt0(sK5(U_39,U_38,U_41),U_41)
& aLowerBoundOfIn0(sK5(U_39,U_38,U_41),U_38,U_39) )
| ~ aLowerBoundOfIn0(U_41,U_38,U_39)
| ~ aElementOf0(U_41,U_39) )
& ! [U_40] :
( ( ! [U_35] :
( sdtlseqdt0(U_35,U_40)
| ~ aLowerBoundOfIn0(U_35,U_38,U_39) )
& aLowerBoundOfIn0(U_40,U_38,U_39)
& aElementOf0(U_40,U_39) )
| ~ aInfimumOfIn0(U_40,U_38,U_39) ) )
| ~ aSubsetOf0(U_38,U_39) )
| ~ aSet0(U_39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_36,sK5(U_39,U_38,U_41))],[f_12_3]) ).
cnf(f_12_5,plain,
( aElementOf0(U_40,U_39)
| ~ aInfimumOfIn0(U_40,U_38,U_39)
| ~ aSubsetOf0(U_38,U_39)
| ~ aSet0(U_39) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_6,plain,
( aLowerBoundOfIn0(U_40,U_38,U_39)
| ~ aInfimumOfIn0(U_40,U_38,U_39)
| ~ aSubsetOf0(U_38,U_39)
| ~ aSet0(U_39) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_7,plain,
( sdtlseqdt0(U_35,U_40)
| ~ aLowerBoundOfIn0(U_35,U_38,U_39)
| ~ aInfimumOfIn0(U_40,U_38,U_39)
| ~ aSubsetOf0(U_38,U_39)
| ~ aSet0(U_39) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_8,plain,
( aLowerBoundOfIn0(sK5(U_39,U_38,U_41),U_38,U_39)
| ~ aLowerBoundOfIn0(U_41,U_38,U_39)
| ~ aElementOf0(U_41,U_39)
| aInfimumOfIn0(U_41,U_38,U_39)
| ~ aSubsetOf0(U_38,U_39)
| ~ aSet0(U_39) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_9,plain,
( ~ sdtlseqdt0(sK5(U_39,U_38,U_41),U_41)
| ~ aLowerBoundOfIn0(U_41,U_38,U_39)
| ~ aElementOf0(U_41,U_39)
| aInfimumOfIn0(U_41,U_38,U_39)
| ~ aSubsetOf0(U_38,U_39)
| ~ aSet0(U_39) ),
inference(clausify,[status(thm)],[f_12_4]) ).
fof(f_13_1,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( aSupremumOfIn0(W2,W1,W0)
| ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aUpperBoundOfIn0(W3,W1,W0) )
| ~ aUpperBoundOfIn0(W2,W1,W0)
| ~ aElementOf0(W2,W0) )
& ( ( ! [W3] :
( sdtlseqdt0(W2,W3)
| ~ aUpperBoundOfIn0(W3,W1,W0) )
& aUpperBoundOfIn0(W2,W1,W0)
& aElementOf0(W2,W0) )
| ~ aSupremumOfIn0(W2,W1,W0) ) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mDefSup]) ).
fof(f_13_2,plain,
! [U_46] :
( ! [U_45] :
( ! [U_44] :
( ( aSupremumOfIn0(U_44,U_45,U_46)
| ? [U_43] :
( ~ sdtlseqdt0(U_44,U_43)
& aUpperBoundOfIn0(U_43,U_45,U_46) )
| ~ aUpperBoundOfIn0(U_44,U_45,U_46)
| ~ aElementOf0(U_44,U_46) )
& ( ( ! [U_42] :
( sdtlseqdt0(U_44,U_42)
| ~ aUpperBoundOfIn0(U_42,U_45,U_46) )
& aUpperBoundOfIn0(U_44,U_45,U_46)
& aElementOf0(U_44,U_46) )
| ~ aSupremumOfIn0(U_44,U_45,U_46) ) )
| ~ aSubsetOf0(U_45,U_46) )
| ~ aSet0(U_46) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_46] :
( ! [U_45] :
( ( ! [U_48] :
( aSupremumOfIn0(U_48,U_45,U_46)
| ? [U_43] :
( ~ sdtlseqdt0(U_48,U_43)
& aUpperBoundOfIn0(U_43,U_45,U_46) )
| ~ aUpperBoundOfIn0(U_48,U_45,U_46)
| ~ aElementOf0(U_48,U_46) )
& ! [U_47] :
( ( ! [U_42] :
( sdtlseqdt0(U_47,U_42)
| ~ aUpperBoundOfIn0(U_42,U_45,U_46) )
& aUpperBoundOfIn0(U_47,U_45,U_46)
& aElementOf0(U_47,U_46) )
| ~ aSupremumOfIn0(U_47,U_45,U_46) ) )
| ~ aSubsetOf0(U_45,U_46) )
| ~ aSet0(U_46) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
! [U_46] :
( ! [U_45] :
( ( ! [U_48] :
( aSupremumOfIn0(U_48,U_45,U_46)
| ( ~ sdtlseqdt0(U_48,sK6(U_46,U_45,U_48))
& aUpperBoundOfIn0(sK6(U_46,U_45,U_48),U_45,U_46) )
| ~ aUpperBoundOfIn0(U_48,U_45,U_46)
| ~ aElementOf0(U_48,U_46) )
& ! [U_47] :
( ( ! [U_42] :
( sdtlseqdt0(U_47,U_42)
| ~ aUpperBoundOfIn0(U_42,U_45,U_46) )
& aUpperBoundOfIn0(U_47,U_45,U_46)
& aElementOf0(U_47,U_46) )
| ~ aSupremumOfIn0(U_47,U_45,U_46) ) )
| ~ aSubsetOf0(U_45,U_46) )
| ~ aSet0(U_46) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_43,sK6(U_46,U_45,U_48))],[f_13_3]) ).
cnf(f_13_5,plain,
( aElementOf0(U_47,U_46)
| ~ aSupremumOfIn0(U_47,U_45,U_46)
| ~ aSubsetOf0(U_45,U_46)
| ~ aSet0(U_46) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_6,plain,
( aUpperBoundOfIn0(U_47,U_45,U_46)
| ~ aSupremumOfIn0(U_47,U_45,U_46)
| ~ aSubsetOf0(U_45,U_46)
| ~ aSet0(U_46) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_7,plain,
( sdtlseqdt0(U_47,U_42)
| ~ aUpperBoundOfIn0(U_42,U_45,U_46)
| ~ aSupremumOfIn0(U_47,U_45,U_46)
| ~ aSubsetOf0(U_45,U_46)
| ~ aSet0(U_46) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_8,plain,
( aUpperBoundOfIn0(sK6(U_46,U_45,U_48),U_45,U_46)
| ~ aUpperBoundOfIn0(U_48,U_45,U_46)
| ~ aElementOf0(U_48,U_46)
| aSupremumOfIn0(U_48,U_45,U_46)
| ~ aSubsetOf0(U_45,U_46)
| ~ aSet0(U_46) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_9,plain,
( ~ sdtlseqdt0(U_48,sK6(U_46,U_45,U_48))
| ~ aUpperBoundOfIn0(U_48,U_45,U_46)
| ~ aElementOf0(U_48,U_46)
| aSupremumOfIn0(U_48,U_45,U_46)
| ~ aSubsetOf0(U_45,U_46)
| ~ aSet0(U_46) ),
inference(clausify,[status(thm)],[f_13_4]) ).
fof(f_14_1,plain,
! [W0] :
( ! [W1] :
( ! [W2,W3] :
( W2 = W3
| ~ aSupremumOfIn0(W3,W1,W0)
| ~ aSupremumOfIn0(W2,W1,W0) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mSupUn]) ).
fof(f_14_2,plain,
! [U_52] :
( ! [U_51] :
( ! [U_50,U_49] :
( U_50 = U_49
| ~ aSupremumOfIn0(U_49,U_51,U_52)
| ~ aSupremumOfIn0(U_50,U_51,U_52) )
| ~ aSubsetOf0(U_51,U_52) )
| ~ aSet0(U_52) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( U_50 = U_49
| ~ aSupremumOfIn0(U_49,U_51,U_52)
| ~ aSupremumOfIn0(U_50,U_51,U_52)
| ~ aSubsetOf0(U_51,U_52)
| ~ aSet0(U_52) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [W0] :
( ! [W1] :
( ! [W2,W3] :
( W2 = W3
| ~ aInfimumOfIn0(W3,W1,W0)
| ~ aInfimumOfIn0(W2,W1,W0) )
| ~ aSubsetOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mInfUn]) ).
fof(f_15_2,plain,
! [U_56] :
( ! [U_55] :
( ! [U_54,U_53] :
( U_54 = U_53
| ~ aInfimumOfIn0(U_53,U_55,U_56)
| ~ aInfimumOfIn0(U_54,U_55,U_56) )
| ~ aSubsetOf0(U_55,U_56) )
| ~ aSet0(U_56) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( U_54 = U_53
| ~ aInfimumOfIn0(U_53,U_55,U_56)
| ~ aInfimumOfIn0(U_54,U_55,U_56)
| ~ aSubsetOf0(U_55,U_56)
| ~ aSet0(U_56) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [W0] :
( ( aCompleteLattice0(W0)
| ? [W1] :
( ! [W2] :
( ! [W3] : ~ aSupremumOfIn0(W3,W1,W0)
| ~ aInfimumOfIn0(W2,W1,W0) )
& aSubsetOf0(W1,W0) )
| ~ aSet0(W0) )
& ( ( ! [W1] :
( ? [W2] :
( ? [W3] : aSupremumOfIn0(W3,W1,W0)
& aInfimumOfIn0(W2,W1,W0) )
| ~ aSubsetOf0(W1,W0) )
& aSet0(W0) )
| ~ aCompleteLattice0(W0) ) ),
inference(fof_nnf,[status(thm)],[mDefCLat]) ).
fof(f_16_2,plain,
! [U_63] :
( ( aCompleteLattice0(U_63)
| ? [U_62] :
( ! [U_61] :
( ! [U_60] : ~ aSupremumOfIn0(U_60,U_62,U_63)
| ~ aInfimumOfIn0(U_61,U_62,U_63) )
& aSubsetOf0(U_62,U_63) )
| ~ aSet0(U_63) )
& ( ( ! [U_59] :
( ? [U_58] :
( ? [U_57] : aSupremumOfIn0(U_57,U_59,U_63)
& aInfimumOfIn0(U_58,U_59,U_63) )
| ~ aSubsetOf0(U_59,U_63) )
& aSet0(U_63) )
| ~ aCompleteLattice0(U_63) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_65] :
( aCompleteLattice0(U_65)
| ? [U_62] :
( ( ! [U_61] : ~ aInfimumOfIn0(U_61,U_62,U_65)
| ! [U_60] : ~ aSupremumOfIn0(U_60,U_62,U_65) )
& aSubsetOf0(U_62,U_65) )
| ~ aSet0(U_65) )
& ! [U_64] :
( ( ! [U_59] :
( ( ? [U_58] : aInfimumOfIn0(U_58,U_59,U_64)
& ? [U_57] : aSupremumOfIn0(U_57,U_59,U_64) )
| ~ aSubsetOf0(U_59,U_64) )
& aSet0(U_64) )
| ~ aCompleteLattice0(U_64) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_65] :
( aCompleteLattice0(U_65)
| ? [U_62] :
( ( ! [U_61] : ~ aInfimumOfIn0(U_61,U_62,U_65)
| ! [U_60] : ~ aSupremumOfIn0(U_60,U_62,U_65) )
& aSubsetOf0(U_62,U_65) )
| ~ aSet0(U_65) )
& ! [U_64] :
( ( ! [U_59] :
( ( ? [U_58] : aInfimumOfIn0(U_58,U_59,U_64)
& aSupremumOfIn0(sK7(U_64,U_59),U_59,U_64) )
| ~ aSubsetOf0(U_59,U_64) )
& aSet0(U_64) )
| ~ aCompleteLattice0(U_64) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_57,sK7(U_64,U_59))],[f_16_3]) ).
fof(f_16_5,plain,
( ! [U_65] :
( aCompleteLattice0(U_65)
| ? [U_62] :
( ( ! [U_61] : ~ aInfimumOfIn0(U_61,U_62,U_65)
| ! [U_60] : ~ aSupremumOfIn0(U_60,U_62,U_65) )
& aSubsetOf0(U_62,U_65) )
| ~ aSet0(U_65) )
& ! [U_64] :
( ( ! [U_59] :
( ( aInfimumOfIn0(sK8(U_64,U_59),U_59,U_64)
& aSupremumOfIn0(sK7(U_64,U_59),U_59,U_64) )
| ~ aSubsetOf0(U_59,U_64) )
& aSet0(U_64) )
| ~ aCompleteLattice0(U_64) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_58,sK8(U_64,U_59))],[f_16_4]) ).
fof(f_16_6,plain,
( ! [U_65] :
( aCompleteLattice0(U_65)
| ( ( ! [U_61] : ~ aInfimumOfIn0(U_61,sK9(U_65),U_65)
| ! [U_60] : ~ aSupremumOfIn0(U_60,sK9(U_65),U_65) )
& aSubsetOf0(sK9(U_65),U_65) )
| ~ aSet0(U_65) )
& ! [U_64] :
( ( ! [U_59] :
( ( aInfimumOfIn0(sK8(U_64,U_59),U_59,U_64)
& aSupremumOfIn0(sK7(U_64,U_59),U_59,U_64) )
| ~ aSubsetOf0(U_59,U_64) )
& aSet0(U_64) )
| ~ aCompleteLattice0(U_64) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_62,sK9(U_65))],[f_16_5]) ).
cnf(f_16_7,plain,
( aSet0(U_64)
| ~ aCompleteLattice0(U_64) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_8,plain,
( aSupremumOfIn0(sK7(U_64,U_59),U_59,U_64)
| ~ aSubsetOf0(U_59,U_64)
| ~ aCompleteLattice0(U_64) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_9,plain,
( aInfimumOfIn0(sK8(U_64,U_59),U_59,U_64)
| ~ aSubsetOf0(U_59,U_64)
| ~ aCompleteLattice0(U_64) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_10,plain,
( aSubsetOf0(sK9(U_65),U_65)
| ~ aSet0(U_65)
| aCompleteLattice0(U_65) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_11,plain,
( ~ aInfimumOfIn0(U_61,sK9(U_65),U_65)
| ~ aSupremumOfIn0(U_60,sK9(U_65),U_65)
| ~ aSet0(U_65)
| aCompleteLattice0(U_65) ),
inference(clausify,[status(thm)],[f_16_6]) ).
fof(f_17_1,plain,
! [W0] :
( $true
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mConMap]) ).
fof(f_17_2,plain,
! [U_66] :
( $true
| ~ aFunction0(U_66) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_66] : ~ aFunction0(U_66)
| $true ),
inference(miniscope,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( ~ aFunction0(U_66)
| $true ),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_1,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mDomSort]) ).
fof(f_18_2,plain,
! [U_67] :
( aSet0(szDzozmdt0(U_67))
| ~ aFunction0(U_67) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( aSet0(szDzozmdt0(U_67))
| ~ aFunction0(U_67) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [W0] :
( aSet0(szRzazndt0(W0))
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mRanSort]) ).
fof(f_19_2,plain,
! [U_68] :
( aSet0(szRzazndt0(U_68))
| ~ aFunction0(U_68) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( aSet0(szRzazndt0(U_68))
| ~ aFunction0(U_68) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [W0,W1] :
( ( ( isOn0(W0,W1)
| szRzazndt0(W0) != W1
| szDzozmdt0(W0) != szRzazndt0(W0) )
& ( ( szRzazndt0(W0) = W1
& szDzozmdt0(W0) = szRzazndt0(W0) )
| ~ isOn0(W0,W1) ) )
| ~ aSet0(W1)
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mDefDom]) ).
fof(f_20_2,plain,
! [U_70,U_69] :
( ( ( isOn0(U_70,U_69)
| szRzazndt0(U_70) != U_69
| szDzozmdt0(U_70) != szRzazndt0(U_70) )
& ( ( szRzazndt0(U_70) = U_69
& szDzozmdt0(U_70) = szRzazndt0(U_70) )
| ~ isOn0(U_70,U_69) ) )
| ~ aSet0(U_69)
| ~ aFunction0(U_70) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( szDzozmdt0(U_70) = szRzazndt0(U_70)
| ~ isOn0(U_70,U_69)
| ~ aSet0(U_69)
| ~ aFunction0(U_70) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( szRzazndt0(U_70) = U_69
| ~ isOn0(U_70,U_69)
| ~ aSet0(U_69)
| ~ aFunction0(U_70) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_5,plain,
( isOn0(U_70,U_69)
| szRzazndt0(U_70) != U_69
| szDzozmdt0(U_70) != szRzazndt0(U_70)
| ~ aSet0(U_69)
| ~ aFunction0(U_70) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [W0] :
( ! [W1] :
( aElementOf0(sdtlpdtrp0(W0,W1),szRzazndt0(W0))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mImgSort]) ).
fof(f_21_2,plain,
! [U_72] :
( ! [U_71] :
( aElementOf0(sdtlpdtrp0(U_72,U_71),szRzazndt0(U_72))
| ~ aElementOf0(U_71,szDzozmdt0(U_72)) )
| ~ aFunction0(U_72) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( aElementOf0(sdtlpdtrp0(U_72,U_71),szRzazndt0(U_72))
| ~ aElementOf0(U_71,szDzozmdt0(U_72))
| ~ aFunction0(U_72) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [W0] :
( ! [W1] :
( ( aFixedPointOf0(W1,W0)
| sdtlpdtrp0(W0,W1) != W1
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
& ( ( sdtlpdtrp0(W0,W1) = W1
& aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFixedPointOf0(W1,W0) ) )
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mDefFix]) ).
fof(f_22_2,plain,
! [U_74] :
( ! [U_73] :
( ( aFixedPointOf0(U_73,U_74)
| sdtlpdtrp0(U_74,U_73) != U_73
| ~ aElementOf0(U_73,szDzozmdt0(U_74)) )
& ( ( sdtlpdtrp0(U_74,U_73) = U_73
& aElementOf0(U_73,szDzozmdt0(U_74)) )
| ~ aFixedPointOf0(U_73,U_74) ) )
| ~ aFunction0(U_74) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
! [U_74] :
( ( ! [U_76] :
( aFixedPointOf0(U_76,U_74)
| sdtlpdtrp0(U_74,U_76) != U_76
| ~ aElementOf0(U_76,szDzozmdt0(U_74)) )
& ! [U_75] :
( ( sdtlpdtrp0(U_74,U_75) = U_75
& aElementOf0(U_75,szDzozmdt0(U_74)) )
| ~ aFixedPointOf0(U_75,U_74) ) )
| ~ aFunction0(U_74) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( aElementOf0(U_75,szDzozmdt0(U_74))
| ~ aFixedPointOf0(U_75,U_74)
| ~ aFunction0(U_74) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( sdtlpdtrp0(U_74,U_75) = U_75
| ~ aFixedPointOf0(U_75,U_74)
| ~ aFunction0(U_74) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( aFixedPointOf0(U_76,U_74)
| sdtlpdtrp0(U_74,U_76) != U_76
| ~ aElementOf0(U_76,szDzozmdt0(U_74))
| ~ aFunction0(U_74) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [W0] :
( ( ( isMonotone0(W0)
| ? [W1,W2] :
( ~ sdtlseqdt0(sdtlpdtrp0(W0,W1),sdtlpdtrp0(W0,W2))
& sdtlseqdt0(W1,W2)
& aElementOf0(W2,szDzozmdt0(W0))
& aElementOf0(W1,szDzozmdt0(W0)) ) )
& ( ! [W1,W2] :
( sdtlseqdt0(sdtlpdtrp0(W0,W1),sdtlpdtrp0(W0,W2))
| ~ sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,szDzozmdt0(W0))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ isMonotone0(W0) ) )
| ~ aFunction0(W0) ),
inference(fof_nnf,[status(thm)],[mDefMonot]) ).
fof(f_23_2,plain,
! [U_81] :
( ( ( isMonotone0(U_81)
| ? [U_80,U_79] :
( ~ sdtlseqdt0(sdtlpdtrp0(U_81,U_80),sdtlpdtrp0(U_81,U_79))
& sdtlseqdt0(U_80,U_79)
& aElementOf0(U_79,szDzozmdt0(U_81))
& aElementOf0(U_80,szDzozmdt0(U_81)) ) )
& ( ! [U_78,U_77] :
( sdtlseqdt0(sdtlpdtrp0(U_81,U_78),sdtlpdtrp0(U_81,U_77))
| ~ sdtlseqdt0(U_78,U_77)
| ~ aElementOf0(U_77,szDzozmdt0(U_81))
| ~ aElementOf0(U_78,szDzozmdt0(U_81)) )
| ~ isMonotone0(U_81) ) )
| ~ aFunction0(U_81) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
! [U_81] :
( ( ( isMonotone0(U_81)
| ? [U_79] :
( ~ sdtlseqdt0(sdtlpdtrp0(U_81,sK10(U_81)),sdtlpdtrp0(U_81,U_79))
& sdtlseqdt0(sK10(U_81),U_79)
& aElementOf0(U_79,szDzozmdt0(U_81))
& aElementOf0(sK10(U_81),szDzozmdt0(U_81)) ) )
& ( ! [U_78,U_77] :
( sdtlseqdt0(sdtlpdtrp0(U_81,U_78),sdtlpdtrp0(U_81,U_77))
| ~ sdtlseqdt0(U_78,U_77)
| ~ aElementOf0(U_77,szDzozmdt0(U_81))
| ~ aElementOf0(U_78,szDzozmdt0(U_81)) )
| ~ isMonotone0(U_81) ) )
| ~ aFunction0(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_80,sK10(U_81))],[f_23_2]) ).
fof(f_23_4,plain,
! [U_81] :
( ( ( isMonotone0(U_81)
| ( ~ sdtlseqdt0(sdtlpdtrp0(U_81,sK10(U_81)),sdtlpdtrp0(U_81,sK11(U_81)))
& sdtlseqdt0(sK10(U_81),sK11(U_81))
& aElementOf0(sK11(U_81),szDzozmdt0(U_81))
& aElementOf0(sK10(U_81),szDzozmdt0(U_81)) ) )
& ( ! [U_78,U_77] :
( sdtlseqdt0(sdtlpdtrp0(U_81,U_78),sdtlpdtrp0(U_81,U_77))
| ~ sdtlseqdt0(U_78,U_77)
| ~ aElementOf0(U_77,szDzozmdt0(U_81))
| ~ aElementOf0(U_78,szDzozmdt0(U_81)) )
| ~ isMonotone0(U_81) ) )
| ~ aFunction0(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_79,sK11(U_81))],[f_23_3]) ).
cnf(f_23_5,plain,
( sdtlseqdt0(sdtlpdtrp0(U_81,U_78),sdtlpdtrp0(U_81,U_77))
| ~ sdtlseqdt0(U_78,U_77)
| ~ aElementOf0(U_77,szDzozmdt0(U_81))
| ~ aElementOf0(U_78,szDzozmdt0(U_81))
| ~ isMonotone0(U_81)
| ~ aFunction0(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( aElementOf0(sK10(U_81),szDzozmdt0(U_81))
| isMonotone0(U_81)
| ~ aFunction0(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( aElementOf0(sK11(U_81),szDzozmdt0(U_81))
| isMonotone0(U_81)
| ~ aFunction0(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_8,plain,
( sdtlseqdt0(sK10(U_81),sK11(U_81))
| isMonotone0(U_81)
| ~ aFunction0(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_9,plain,
( ~ sdtlseqdt0(sdtlpdtrp0(U_81,sK10(U_81)),sdtlpdtrp0(U_81,sK11(U_81)))
| isMonotone0(U_81)
| ~ aFunction0(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W2,W3)
| ( ~ aUpperBoundOfIn0(W3,W0,xU)
& ( ? [W4] :
( ~ sdtlseqdt0(W4,W3)
& aElementOf0(W4,W0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aElementOf0(W3,W0) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W2,W1)
| ( ~ aLowerBoundOfIn0(W2,W0,xU)
& ( ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W2,xU) ) ) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) )
| ( ~ aSubsetOf0(W0,xU)
& ( ? [W1] :
( ~ aElementOf0(W1,xU)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& aSet0(xU) ),
inference(fof_nnf,[status(thm)],[m__1123]) ).
fof(f_24_2,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ? [U_90] :
( ? [U_89] :
( aSupremumOfIn0(U_89,U_91,xU)
& ! [U_88] :
( sdtlseqdt0(U_89,U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ? [U_87] :
( ~ sdtlseqdt0(U_87,U_88)
& aElementOf0(U_87,U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(U_89,U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,U_89)
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(U_89,xU)
& aElementOf0(U_89,xU) )
& aInfimumOfIn0(U_90,U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,U_90)
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(U_90,U_91,xU)
& ! [U_83] :
( sdtlseqdt0(U_90,U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(U_90,xU)
& aElementOf0(U_90,xU) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ? [U_82] :
( ~ aElementOf0(U_82,xU)
& aElementOf0(U_82,U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( ? [U_90] :
( aInfimumOfIn0(U_90,U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,U_90)
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(U_90,U_91,xU)
& ! [U_83] :
( sdtlseqdt0(U_90,U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(U_90,xU)
& aElementOf0(U_90,xU) )
& ? [U_89] :
( aSupremumOfIn0(U_89,U_91,xU)
& ! [U_88] :
( sdtlseqdt0(U_89,U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ? [U_87] :
( ~ sdtlseqdt0(U_87,U_88)
& aElementOf0(U_87,U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(U_89,U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,U_89)
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(U_89,xU)
& aElementOf0(U_89,xU) ) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ? [U_82] :
( ~ aElementOf0(U_82,xU)
& aElementOf0(U_82,U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( ? [U_90] :
( aInfimumOfIn0(U_90,U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,U_90)
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(U_90,U_91,xU)
& ! [U_83] :
( sdtlseqdt0(U_90,U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(U_90,xU)
& aElementOf0(U_90,xU) )
& ? [U_89] :
( aSupremumOfIn0(U_89,U_91,xU)
& ! [U_88] :
( sdtlseqdt0(U_89,U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ? [U_87] :
( ~ sdtlseqdt0(U_87,U_88)
& aElementOf0(U_87,U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(U_89,U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,U_89)
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(U_89,xU)
& aElementOf0(U_89,xU) ) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ( ~ aElementOf0(sK12(U_91),xU)
& aElementOf0(sK12(U_91),U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_82,sK12(U_91))],[f_24_3]) ).
fof(f_24_5,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( ? [U_90] :
( aInfimumOfIn0(U_90,U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,U_90)
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(U_90,U_91,xU)
& ! [U_83] :
( sdtlseqdt0(U_90,U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(U_90,xU)
& aElementOf0(U_90,xU) )
& aSupremumOfIn0(sK13(U_91),U_91,xU)
& ! [U_88] :
( sdtlseqdt0(sK13(U_91),U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ? [U_87] :
( ~ sdtlseqdt0(U_87,U_88)
& aElementOf0(U_87,U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(sK13(U_91),U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(sK13(U_91),xU)
& aElementOf0(sK13(U_91),xU) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ( ~ aElementOf0(sK12(U_91),xU)
& aElementOf0(sK12(U_91),U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_89,sK13(U_91))],[f_24_4]) ).
fof(f_24_6,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( ? [U_90] :
( aInfimumOfIn0(U_90,U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,U_90)
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(U_90,U_91,xU)
& ! [U_83] :
( sdtlseqdt0(U_90,U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(U_90,xU)
& aElementOf0(U_90,xU) )
& aSupremumOfIn0(sK13(U_91),U_91,xU)
& ! [U_88] :
( sdtlseqdt0(sK13(U_91),U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
& aElementOf0(sK14(U_91,U_88),U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(sK13(U_91),U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(sK13(U_91),xU)
& aElementOf0(sK13(U_91),xU) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ( ~ aElementOf0(sK12(U_91),xU)
& aElementOf0(sK12(U_91),U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_87,sK14(U_91,U_88))],[f_24_5]) ).
fof(f_24_7,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( aInfimumOfIn0(sK15(U_91),U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,sK15(U_91))
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ? [U_84] :
( ~ sdtlseqdt0(U_85,U_84)
& aElementOf0(U_84,U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(sK15(U_91),U_91,xU)
& ! [U_83] :
( sdtlseqdt0(sK15(U_91),U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(sK15(U_91),xU)
& aElementOf0(sK15(U_91),xU)
& aSupremumOfIn0(sK13(U_91),U_91,xU)
& ! [U_88] :
( sdtlseqdt0(sK13(U_91),U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
& aElementOf0(sK14(U_91,U_88),U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(sK13(U_91),U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(sK13(U_91),xU)
& aElementOf0(sK13(U_91),xU) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ( ~ aElementOf0(sK12(U_91),xU)
& aElementOf0(sK12(U_91),U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_90,sK15(U_91))],[f_24_6]) ).
fof(f_24_8,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [U_93,U_92] :
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [U_91] :
( ( aInfimumOfIn0(sK15(U_91),U_91,xU)
& ! [U_85] :
( sdtlseqdt0(U_85,sK15(U_91))
| ( ~ aLowerBoundOfIn0(U_85,U_91,xU)
& ( ( ~ sdtlseqdt0(U_85,sK16(U_91,U_85))
& aElementOf0(sK16(U_91,U_85),U_91) )
| ~ aElementOf0(U_85,xU) ) ) )
& aLowerBoundOfIn0(sK15(U_91),U_91,xU)
& ! [U_83] :
( sdtlseqdt0(sK15(U_91),U_83)
| ~ aElementOf0(U_83,U_91) )
& aElementOf0(sK15(U_91),xU)
& aElementOf0(sK15(U_91),xU)
& aSupremumOfIn0(sK13(U_91),U_91,xU)
& ! [U_88] :
( sdtlseqdt0(sK13(U_91),U_88)
| ( ~ aUpperBoundOfIn0(U_88,U_91,xU)
& ( ( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
& aElementOf0(sK14(U_91,U_88),U_91) )
| ~ aElementOf0(U_88,xU) ) ) )
& aUpperBoundOfIn0(sK13(U_91),U_91,xU)
& ! [U_86] :
( sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) )
& aElementOf0(sK13(U_91),xU)
& aElementOf0(sK13(U_91),xU) )
| ( ~ aSubsetOf0(U_91,xU)
& ( ( ~ aElementOf0(sK12(U_91),xU)
& aElementOf0(sK12(U_91),U_91) )
| ~ aSet0(U_91) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_84,sK16(U_91,U_85))],[f_24_7]) ).
cnf(f_24_9,plain,
aSet0(xU),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_10,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aElementOf0(sK13(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_11,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aElementOf0(sK13(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_12,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aElementOf0(sK13(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_13,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aElementOf0(sK13(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_14,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_15,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_16,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aUpperBoundOfIn0(sK13(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_17,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aUpperBoundOfIn0(sK13(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_18,plain,
( aElementOf0(sK14(U_91,U_88),U_91)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_19,plain,
( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_20,plain,
( ~ aUpperBoundOfIn0(U_88,U_91,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_21,plain,
( aElementOf0(sK14(U_91,U_88),U_91)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_22,plain,
( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_23,plain,
( ~ aUpperBoundOfIn0(U_88,U_91,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_24,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aSupremumOfIn0(sK13(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_25,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aSupremumOfIn0(sK13(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_26,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aElementOf0(sK15(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_27,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aElementOf0(sK15(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_28,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aElementOf0(sK15(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_29,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aElementOf0(sK15(U_91),xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_30,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| sdtlseqdt0(sK15(U_91),U_83)
| ~ aElementOf0(U_83,U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_31,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| sdtlseqdt0(sK15(U_91),U_83)
| ~ aElementOf0(U_83,U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_32,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aLowerBoundOfIn0(sK15(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_33,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aLowerBoundOfIn0(sK15(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_34,plain,
( aElementOf0(sK16(U_91,U_85),U_91)
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_35,plain,
( ~ sdtlseqdt0(U_85,sK16(U_91,U_85))
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_36,plain,
( ~ aLowerBoundOfIn0(U_85,U_91,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_37,plain,
( aElementOf0(sK16(U_91,U_85),U_91)
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_38,plain,
( ~ sdtlseqdt0(U_85,sK16(U_91,U_85))
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_39,plain,
( ~ aLowerBoundOfIn0(U_85,U_91,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_40,plain,
( aElementOf0(sK12(U_91),U_91)
| ~ aSet0(U_91)
| aInfimumOfIn0(sK15(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_41,plain,
( ~ aElementOf0(sK12(U_91),xU)
| ~ aSet0(U_91)
| aInfimumOfIn0(sK15(U_91),U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_42,plain,
( aElementOf0(sK13(U_91),xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_43,plain,
( aElementOf0(sK13(U_91),xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_44,plain,
( sdtlseqdt0(U_86,sK13(U_91))
| ~ aElementOf0(U_86,U_91)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_45,plain,
( aUpperBoundOfIn0(sK13(U_91),U_91,xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_46,plain,
( aElementOf0(sK14(U_91,U_88),U_91)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_47,plain,
( ~ sdtlseqdt0(sK14(U_91,U_88),U_88)
| ~ aElementOf0(U_88,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_48,plain,
( ~ aUpperBoundOfIn0(U_88,U_91,xU)
| sdtlseqdt0(sK13(U_91),U_88)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_49,plain,
( aSupremumOfIn0(sK13(U_91),U_91,xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_50,plain,
( aElementOf0(sK15(U_91),xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_51,plain,
( aElementOf0(sK15(U_91),xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_52,plain,
( sdtlseqdt0(sK15(U_91),U_83)
| ~ aElementOf0(U_83,U_91)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_53,plain,
( aLowerBoundOfIn0(sK15(U_91),U_91,xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_54,plain,
( aElementOf0(sK16(U_91,U_85),U_91)
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_55,plain,
( ~ sdtlseqdt0(U_85,sK16(U_91,U_85))
| ~ aElementOf0(U_85,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_56,plain,
( ~ aLowerBoundOfIn0(U_85,U_91,xU)
| sdtlseqdt0(U_85,sK15(U_91))
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_57,plain,
( aInfimumOfIn0(sK15(U_91),U_91,xU)
| ~ aSubsetOf0(U_91,xU) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_58,plain,
aCompleteLattice0(xU),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_59,plain,
aFunction0(xf),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_60,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,U_93),sdtlpdtrp0(xf,U_92))
| ~ sdtlseqdt0(U_93,U_92)
| ~ aElementOf0(U_92,szDzozmdt0(xf))
| ~ aElementOf0(U_93,szDzozmdt0(xf)) ),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_61,plain,
isMonotone0(xf),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_62,plain,
szDzozmdt0(xf) = szRzazndt0(xf),
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_63,plain,
szRzazndt0(xf) = xU,
inference(clausify,[status(thm)],[f_24_8]) ).
cnf(f_24_64,plain,
isOn0(xf,xU),
inference(clausify,[status(thm)],[f_24_8]) ).
fof(f_25_1,plain,
( xS = cS1142(xf)
& ! [W0] :
( ( aElementOf0(W0,xS)
| ( ~ aFixedPointOf0(W0,xf)
& ( sdtlpdtrp0(xf,W0) != W0
| ~ aElementOf0(W0,szDzozmdt0(xf)) ) ) )
& ( ( aFixedPointOf0(W0,xf)
& sdtlpdtrp0(xf,W0) = W0
& aElementOf0(W0,szDzozmdt0(xf)) )
| ~ aElementOf0(W0,xS) ) )
& aSet0(xS) ),
inference(fof_nnf,[status(thm)],[m__1144]) ).
fof(f_25_2,plain,
( xS = cS1142(xf)
& ! [U_94] :
( ( aElementOf0(U_94,xS)
| ( ~ aFixedPointOf0(U_94,xf)
& ( sdtlpdtrp0(xf,U_94) != U_94
| ~ aElementOf0(U_94,szDzozmdt0(xf)) ) ) )
& ( ( aFixedPointOf0(U_94,xf)
& sdtlpdtrp0(xf,U_94) = U_94
& aElementOf0(U_94,szDzozmdt0(xf)) )
| ~ aElementOf0(U_94,xS) ) )
& aSet0(xS) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( xS = cS1142(xf)
& ! [U_96] :
( aElementOf0(U_96,xS)
| ( ~ aFixedPointOf0(U_96,xf)
& ( sdtlpdtrp0(xf,U_96) != U_96
| ~ aElementOf0(U_96,szDzozmdt0(xf)) ) ) )
& ! [U_95] :
( ( aFixedPointOf0(U_95,xf)
& sdtlpdtrp0(xf,U_95) = U_95
& aElementOf0(U_95,szDzozmdt0(xf)) )
| ~ aElementOf0(U_95,xS) )
& aSet0(xS) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
aSet0(xS),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( aElementOf0(U_95,szDzozmdt0(xf))
| ~ aElementOf0(U_95,xS) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( sdtlpdtrp0(xf,U_95) = U_95
| ~ aElementOf0(U_95,xS) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_7,plain,
( aFixedPointOf0(U_95,xf)
| ~ aElementOf0(U_95,xS) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_8,plain,
( sdtlpdtrp0(xf,U_96) != U_96
| ~ aElementOf0(U_96,szDzozmdt0(xf))
| aElementOf0(U_96,xS) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_9,plain,
( ~ aFixedPointOf0(U_96,xf)
| aElementOf0(U_96,xS) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_10,plain,
xS = cS1142(xf),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
( aSubsetOf0(xT,xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,xT) )
& aSet0(xT) ),
inference(fof_nnf,[status(thm)],[m__1173]) ).
fof(f_26_2,plain,
( aSubsetOf0(xT,xS)
& ! [U_97] :
( aElementOf0(U_97,xS)
| ~ aElementOf0(U_97,xT) )
& aSet0(xT) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
aSet0(xT),
inference(clausify,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( aElementOf0(U_97,xS)
| ~ aElementOf0(U_97,xT) ),
inference(clausify,[status(thm)],[f_26_2]) ).
cnf(f_26_5,plain,
aSubsetOf0(xT,xS),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( ( aElementOf0(W0,xP)
| ( ~ aUpperBoundOfIn0(W0,xT,xU)
& ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aElementOf0(W1,xT) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
| ~ aElementOf0(W0,xU) )
& ( ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) ) )
& aSet0(xP) ),
inference(fof_nnf,[status(thm)],[m__1244]) ).
fof(f_27_2,plain,
( xP = cS1241(xU,xf,xT)
& ! [U_100] :
( ( aElementOf0(U_100,xP)
| ( ~ aUpperBoundOfIn0(U_100,xT,xU)
& ? [U_99] :
( ~ sdtlseqdt0(U_99,U_100)
& aElementOf0(U_99,xT) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_100),U_100)
| ~ aElementOf0(U_100,xU) )
& ( ( aUpperBoundOfIn0(U_100,xT,xU)
& ! [U_98] :
( sdtlseqdt0(U_98,U_100)
| ~ aElementOf0(U_98,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,U_100),U_100)
& aElementOf0(U_100,xU) )
| ~ aElementOf0(U_100,xP) ) )
& aSet0(xP) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( xP = cS1241(xU,xf,xT)
& ! [U_102] :
( aElementOf0(U_102,xP)
| ( ~ aUpperBoundOfIn0(U_102,xT,xU)
& ? [U_99] :
( ~ sdtlseqdt0(U_99,U_102)
& aElementOf0(U_99,xT) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_102),U_102)
| ~ aElementOf0(U_102,xU) )
& ! [U_101] :
( ( aUpperBoundOfIn0(U_101,xT,xU)
& ! [U_98] :
( sdtlseqdt0(U_98,U_101)
| ~ aElementOf0(U_98,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,U_101),U_101)
& aElementOf0(U_101,xU) )
| ~ aElementOf0(U_101,xP) )
& aSet0(xP) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( xP = cS1241(xU,xf,xT)
& ! [U_102] :
( aElementOf0(U_102,xP)
| ( ~ aUpperBoundOfIn0(U_102,xT,xU)
& ~ sdtlseqdt0(sK17(U_102),U_102)
& aElementOf0(sK17(U_102),xT) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_102),U_102)
| ~ aElementOf0(U_102,xU) )
& ! [U_101] :
( ( aUpperBoundOfIn0(U_101,xT,xU)
& ! [U_98] :
( sdtlseqdt0(U_98,U_101)
| ~ aElementOf0(U_98,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,U_101),U_101)
& aElementOf0(U_101,xU) )
| ~ aElementOf0(U_101,xP) )
& aSet0(xP) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_99,sK17(U_102))],[f_27_3]) ).
cnf(f_27_5,plain,
aSet0(xP),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_6,plain,
( aElementOf0(U_101,xU)
| ~ aElementOf0(U_101,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_7,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,U_101),U_101)
| ~ aElementOf0(U_101,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_8,plain,
( sdtlseqdt0(U_98,U_101)
| ~ aElementOf0(U_98,xT)
| ~ aElementOf0(U_101,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_9,plain,
( aUpperBoundOfIn0(U_101,xT,xU)
| ~ aElementOf0(U_101,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_10,plain,
( aElementOf0(sK17(U_102),xT)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_102),U_102)
| ~ aElementOf0(U_102,xU)
| aElementOf0(U_102,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_11,plain,
( ~ sdtlseqdt0(sK17(U_102),U_102)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_102),U_102)
| ~ aElementOf0(U_102,xU)
| aElementOf0(U_102,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_12,plain,
( ~ aUpperBoundOfIn0(U_102,xT,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,U_102),U_102)
| ~ aElementOf0(U_102,xU)
| aElementOf0(U_102,xP) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_13,plain,
xP = cS1241(xU,xf,xT),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,negated_conjecture,
~ ? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
inference(negate,[status(cth)],[m__]) ).
fof(f_28_2,negated_conjecture,
! [W0] :
( ~ aInfimumOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,xP) )
& aElementOf0(W1,xU) )
| ( ~ aLowerBoundOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W0,W1)
& aElementOf0(W1,xP) )
| ~ aElementOf0(W0,xU) ) )
| ~ aElementOf0(W0,xU) ) ),
inference(fof_nnf,[status(thm)],[f_28_1]) ).
fof(f_28_3,negated_conjecture,
! [U_106] :
( ~ aInfimumOfIn0(U_106,xP,xU)
& ( ? [U_105] :
( ~ sdtlseqdt0(U_105,U_106)
& aLowerBoundOfIn0(U_105,xP,xU)
& ! [U_104] :
( sdtlseqdt0(U_105,U_104)
| ~ aElementOf0(U_104,xP) )
& aElementOf0(U_105,xU) )
| ( ~ aLowerBoundOfIn0(U_106,xP,xU)
& ( ? [U_103] :
( ~ sdtlseqdt0(U_106,U_103)
& aElementOf0(U_103,xP) )
| ~ aElementOf0(U_106,xU) ) )
| ~ aElementOf0(U_106,xU) ) ),
inference(variable_rename,[status(thm)],[f_28_2]) ).
fof(f_28_4,negated_conjecture,
( ! [U_108] : ~ aInfimumOfIn0(U_108,xP,xU)
& ! [U_107] :
( ? [U_105] :
( ~ sdtlseqdt0(U_105,U_107)
& aLowerBoundOfIn0(U_105,xP,xU)
& ! [U_104] :
( sdtlseqdt0(U_105,U_104)
| ~ aElementOf0(U_104,xP) )
& aElementOf0(U_105,xU) )
| ( ~ aLowerBoundOfIn0(U_107,xP,xU)
& ( ? [U_103] :
( ~ sdtlseqdt0(U_107,U_103)
& aElementOf0(U_103,xP) )
| ~ aElementOf0(U_107,xU) ) )
| ~ aElementOf0(U_107,xU) ) ),
inference(miniscope,[status(thm)],[f_28_3]) ).
fof(f_28_5,negated_conjecture,
( ! [U_108] : ~ aInfimumOfIn0(U_108,xP,xU)
& ! [U_107] :
( ? [U_105] :
( ~ sdtlseqdt0(U_105,U_107)
& aLowerBoundOfIn0(U_105,xP,xU)
& ! [U_104] :
( sdtlseqdt0(U_105,U_104)
| ~ aElementOf0(U_104,xP) )
& aElementOf0(U_105,xU) )
| ( ~ aLowerBoundOfIn0(U_107,xP,xU)
& ( ( ~ sdtlseqdt0(U_107,sK18(U_107))
& aElementOf0(sK18(U_107),xP) )
| ~ aElementOf0(U_107,xU) ) )
| ~ aElementOf0(U_107,xU) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_103,sK18(U_107))],[f_28_4]) ).
fof(f_28_6,negated_conjecture,
( ! [U_108] : ~ aInfimumOfIn0(U_108,xP,xU)
& ! [U_107] :
( ( ~ sdtlseqdt0(sK19(U_107),U_107)
& aLowerBoundOfIn0(sK19(U_107),xP,xU)
& ! [U_104] :
( sdtlseqdt0(sK19(U_107),U_104)
| ~ aElementOf0(U_104,xP) )
& aElementOf0(sK19(U_107),xU) )
| ( ~ aLowerBoundOfIn0(U_107,xP,xU)
& ( ( ~ sdtlseqdt0(U_107,sK18(U_107))
& aElementOf0(sK18(U_107),xP) )
| ~ aElementOf0(U_107,xU) ) )
| ~ aElementOf0(U_107,xU) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_105,sK19(U_107))],[f_28_5]) ).
fof(f_28_7,negated_conjecture,
( ! [U_107,U_104] :
( ~ sdtlseqdt0(sK19(U_107),U_107)
| ~ sP2(U_107,U_104) )
& ! [U_107,U_104] :
( aLowerBoundOfIn0(sK19(U_107),xP,xU)
| ~ sP2(U_107,U_104) )
& ! [U_107,U_104] :
( sdtlseqdt0(sK19(U_107),U_104)
| ~ aElementOf0(U_104,xP)
| ~ sP2(U_107,U_104) )
& ! [U_107,U_104] :
( aElementOf0(sK19(U_107),xU)
| ~ sP2(U_107,U_104) )
& ! [U_107] :
( ~ sdtlseqdt0(U_107,sK18(U_107))
| ~ sP0(U_107) )
& ! [U_107] :
( aElementOf0(sK18(U_107),xP)
| ~ sP0(U_107) )
& ! [U_107] :
( ~ aLowerBoundOfIn0(U_107,xP,xU)
| ~ sP1(U_107) )
& ! [U_107] :
( sP0(U_107)
| ~ aElementOf0(U_107,xU)
| ~ sP1(U_107) )
& ! [U_108] : ~ aInfimumOfIn0(U_108,xP,xU)
& ! [U_107,U_104] :
( sP2(U_107,U_104)
| sP1(U_107)
| ~ aElementOf0(U_107,xU) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2])],[f_28_6]) ).
cnf(f_28_8,negated_conjecture,
( sP2(U_107,U_104)
| sP1(U_107)
| ~ aElementOf0(U_107,xU) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_9,negated_conjecture,
~ aInfimumOfIn0(U_108,xP,xU),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_10,negated_conjecture,
( sP0(U_107)
| ~ aElementOf0(U_107,xU)
| ~ sP1(U_107) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_11,negated_conjecture,
( ~ aLowerBoundOfIn0(U_107,xP,xU)
| ~ sP1(U_107) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_12,negated_conjecture,
( aElementOf0(sK18(U_107),xP)
| ~ sP0(U_107) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_13,negated_conjecture,
( ~ sdtlseqdt0(U_107,sK18(U_107))
| ~ sP0(U_107) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_14,negated_conjecture,
( aElementOf0(sK19(U_107),xU)
| ~ sP2(U_107,U_104) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_15,negated_conjecture,
( sdtlseqdt0(sK19(U_107),U_104)
| ~ aElementOf0(U_104,xP)
| ~ sP2(U_107,U_104) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_16,negated_conjecture,
( aLowerBoundOfIn0(sK19(U_107),xP,xU)
| ~ sP2(U_107,U_104) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_17,negated_conjecture,
( ~ sdtlseqdt0(sK19(U_107),U_107)
| ~ sP2(U_107,U_104) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_1_4_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_1_4]) ).
cnf(f_2_4_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_2_4]) ).
cnf(f_6_3_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_6_3]) ).
cnf(f_17_4_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_17_4]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( szDzozmdt0(Eq_x_0) = szDzozmdt0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( szRzazndt0(Eq_x_0) = szRzazndt0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sdtlpdtrp0(Eq_x_0,Eq_x_1) = sdtlpdtrp0(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( cS1142(Eq_x_0) = cS1142(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( cS1241(Eq_x_0,Eq_x_1,Eq_x_2) = cS1241(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK1(Eq_x_0) = sK1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2) = sK3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK4(Eq_x_0,Eq_x_1,Eq_x_2) = sK4(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK5(Eq_x_0,Eq_x_1,Eq_x_2) = sK5(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK6(Eq_x_0,Eq_x_1,Eq_x_2) = sK6(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK7(Eq_x_0,Eq_x_1) = sK7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK9(Eq_x_0) = sK9(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK10(Eq_x_0) = sK10(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK11(Eq_x_0) = sK11(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( sK12(Eq_x_0) = sK12(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sK13(Eq_x_0) = sK13(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK14(Eq_x_0,Eq_x_1) = sK14(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( sK15(Eq_x_0) = sK15(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( sK16(Eq_x_0,Eq_x_1) = sK16(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( sK17(Eq_x_0) = sK17(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( sK18(Eq_x_0) = sK18(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( sK19(Eq_x_0) = sK19(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( aSet0(Eq_y_0)
| ~ aSet0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( aElement0(Eq_y_0)
| ~ aElement0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( aElementOf0(Eq_y_0,Eq_y_1)
| ~ aElementOf0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( isEmpty0(Eq_y_0)
| ~ isEmpty0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( aSubsetOf0(Eq_y_0,Eq_y_1)
| ~ aSubsetOf0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( sdtlseqdt0(Eq_y_0,Eq_y_1)
| ~ sdtlseqdt0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( aLowerBoundOfIn0(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ aLowerBoundOfIn0(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( aUpperBoundOfIn0(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ aUpperBoundOfIn0(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( aInfimumOfIn0(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ aInfimumOfIn0(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( aSupremumOfIn0(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ aSupremumOfIn0(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( aCompleteLattice0(Eq_y_0)
| ~ aCompleteLattice0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( aFunction0(Eq_y_0)
| ~ aFunction0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( isOn0(Eq_y_0,Eq_y_1)
| ~ isOn0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( aFixedPointOf0(Eq_y_0,Eq_y_1)
| ~ aFixedPointOf0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( isMonotone0(Eq_y_0)
| ~ isMonotone0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( sP0(Eq_y_0)
| ~ sP0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( sP1(Eq_y_0)
| ~ sP1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_45,axiom,
( sP2(Eq_y_0,Eq_y_1)
| ~ sP2(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT385+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n020.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Sat Sep 19 13:52:09 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.16/5.60 % SZS status Theorem for theBenchmark
% 0.16/5.60 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------