%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:59:46 PM UTC 2026
% Result : Theorem 5.39s 7.09s
% Output : CNFRefutation 5.39s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f80ERROR: Could not build tree for root c_18429ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f7,axiom,
! [X0] :
( aElement0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mARefl) ).
fof(f8,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aElement0(X0) )
=> ( ( sdtlseqdt0(X1,X0)
& sdtlseqdt0(X0,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mASymm) ).
fof(f21,axiom,
! [X0] :
( aFunction0(X0)
=> ! [X1] :
( aElementOf0(X1,szDzozmdt0(X0))
=> aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mImgSort) ).
fof(f25,axiom,
( xS = cS1142(xf)
& ! [X0] :
( ( ( aFixedPointOf0(X0,xf)
| ( sdtlpdtrp0(xf,X0) = X0
& aElementOf0(X0,szDzozmdt0(xf)) ) )
=> aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
=> ( aFixedPointOf0(X0,xf)
& sdtlpdtrp0(xf,X0) = X0
& aElementOf0(X0,szDzozmdt0(xf)) ) ) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1144) ).
fof(f26,axiom,
( aSubsetOf0(xT,xS)
& ! [X0] :
( aElementOf0(X0,xT)
=> aElementOf0(X0,xS) )
& aSet0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1173) ).
fof(f27,axiom,
( xP = cS1241(xU,xf,xT)
& ! [X0] :
( ( ( ( aUpperBoundOfIn0(X0,xT,xU)
| ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) ) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) )
=> aElementOf0(X0,xP) )
& ( aElementOf0(X0,xP)
=> ( aUpperBoundOfIn0(X0,xT,xU)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) ) ) )
& aSet0(xP) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1244) ).
fof(f28,axiom,
( aInfimumOfIn0(xp,xP,xU)
& ! [X0] :
( ( aLowerBoundOfIn0(X0,xP,xU)
| ( ! [X1] :
( aElementOf0(X1,xP)
=> sdtlseqdt0(X0,X1) )
& aElementOf0(X0,xU) ) )
=> sdtlseqdt0(X0,xp) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(xp,X0) )
& aElementOf0(xp,xU)
& aElementOf0(xp,xU) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1261) ).
fof(f29,axiom,
( aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)
& ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,sdtlpdtrp0(xf,xp)) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1299) ).
fof(f30,conjecture,
( ( aSupremumOfIn0(xp,xT,xS)
| ( ! [X0] :
( ( aUpperBoundOfIn0(X0,xT,xS)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aElementOf0(X0,xS) )
=> sdtlseqdt0(xp,X0) )
& ( aUpperBoundOfIn0(xp,xT,xS)
| ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) ) ) ) )
& ( aFixedPointOf0(xp,xf)
| ( sdtlpdtrp0(xf,xp) = xp
& aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f31,negated_conjecture,
~ ( ( aSupremumOfIn0(xp,xT,xS)
| ( ! [X0] :
( ( aUpperBoundOfIn0(X0,xT,xS)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aElementOf0(X0,xS) )
=> sdtlseqdt0(xp,X0) )
& ( aUpperBoundOfIn0(xp,xT,xS)
| ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) ) ) ) )
& ( aFixedPointOf0(xp,xf)
| ( sdtlpdtrp0(xf,xp) = xp
& aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f37,plain,
( xP = cS1241(xU,xf,xT)
& ! [X0] :
( ( ( ( aUpperBoundOfIn0(X0,xT,xU)
| ! [X2] :
( aElementOf0(X2,xT)
=> sdtlseqdt0(X2,X0) ) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) )
=> aElementOf0(X0,xP) )
& ( aElementOf0(X0,xP)
=> ( aUpperBoundOfIn0(X0,xT,xU)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) ) ) )
& aSet0(xP) ),
inference(rectify,[],[f27]) ).
fof(f38,plain,
( aInfimumOfIn0(xp,xP,xU)
& ! [X1] :
( ( aLowerBoundOfIn0(X1,xP,xU)
| ( ! [X2] :
( aElementOf0(X2,xP)
=> sdtlseqdt0(X1,X2) )
& aElementOf0(X1,xU) ) )
=> sdtlseqdt0(X1,xp) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(xp,X0) )
& aElementOf0(xp,xU)
& aElementOf0(xp,xU) ),
inference(rectify,[],[f28]) ).
fof(f39,plain,
( aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,sdtlpdtrp0(xf,xp)) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) ) ),
inference(rectify,[],[f29]) ).
fof(f40,plain,
~ ( ( aSupremumOfIn0(xp,xT,xS)
| ( ! [X1] :
( ( aUpperBoundOfIn0(X1,xT,xS)
& ! [X2] :
( aElementOf0(X2,xT)
=> sdtlseqdt0(X2,X1) )
& aElementOf0(X1,xS) )
=> sdtlseqdt0(xp,X1) )
& ( aUpperBoundOfIn0(xp,xT,xS)
| ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) ) ) ) )
& ( aFixedPointOf0(xp,xf)
| ( sdtlpdtrp0(xf,xp) = xp
& aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(rectify,[],[f31]) ).
fof(f42,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f45,plain,
! [X0] :
( ~ aElement0(X0)
| sdtlseqdt0(X0,X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f46,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aElement0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f8]) ).
fof(f47,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aElement0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f46]) ).
fof(f63,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aElementOf0(X1,szDzozmdt0(X0))
| aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f69,plain,
( xS = cS1142(xf)
& ! [X0] :
( ( ( ~ aFixedPointOf0(X0,xf)
& ( sdtlpdtrp0(xf,X0) != X0
| ~ aElementOf0(X0,szDzozmdt0(xf)) ) )
| aElementOf0(X0,xS) )
& ( ~ aElementOf0(X0,xS)
| ( aFixedPointOf0(X0,xf)
& sdtlpdtrp0(xf,X0) = X0
& aElementOf0(X0,szDzozmdt0(xf)) ) ) )
& aSet0(xS) ),
inference(ennf_transformation,[],[f25]) ).
fof(f70,plain,
( aSubsetOf0(xT,xS)
& ! [X0] :
( ~ aElementOf0(X0,xT)
| aElementOf0(X0,xS) )
& aSet0(xT) ),
inference(ennf_transformation,[],[f26]) ).
fof(f71,plain,
( xP = cS1241(xU,xf,xT)
& ! [X0] :
( ( ( ~ aUpperBoundOfIn0(X0,xT,xU)
& ? [X2] :
( aElementOf0(X2,xT)
& ~ sdtlseqdt0(X2,X0) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) )
& ( ~ aElementOf0(X0,xP)
| ( aUpperBoundOfIn0(X0,xT,xU)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,X0) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) ) ) )
& aSet0(xP) ),
inference(ennf_transformation,[],[f37]) ).
fof(f72,plain,
( xP = cS1241(xU,xf,xT)
& ! [X0] :
( ( ( ~ aUpperBoundOfIn0(X0,xT,xU)
& ? [X2] :
( aElementOf0(X2,xT)
& ~ sdtlseqdt0(X2,X0) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) )
& ( ~ aElementOf0(X0,xP)
| ( aUpperBoundOfIn0(X0,xT,xU)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,X0) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) ) ) )
& aSet0(xP) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
( aInfimumOfIn0(xp,xP,xU)
& ! [X1] :
( ( ~ aLowerBoundOfIn0(X1,xP,xU)
& ( ? [X2] :
( aElementOf0(X2,xP)
& ~ sdtlseqdt0(X1,X2) )
| ~ aElementOf0(X1,xU) ) )
| sdtlseqdt0(X1,xp) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X0] :
( ~ aElementOf0(X0,xP)
| sdtlseqdt0(xp,X0) )
& aElementOf0(xp,xU)
& aElementOf0(xp,xU) ),
inference(ennf_transformation,[],[f38]) ).
fof(f74,plain,
( aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,sdtlpdtrp0(xf,xp)) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X0] :
( ~ aElementOf0(X0,xP)
| sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) ) ),
inference(ennf_transformation,[],[f39]) ).
fof(f75,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( ? [X1] :
( aUpperBoundOfIn0(X1,xT,xS)
& ! [X2] :
( ~ aElementOf0(X2,xT)
| sdtlseqdt0(X2,X1) )
& aElementOf0(X1,xS)
& ~ sdtlseqdt0(xp,X1) )
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& ? [X0] :
( aElementOf0(X0,xT)
& ~ sdtlseqdt0(X0,xp) ) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(ennf_transformation,[],[f40]) ).
fof(f76,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( ? [X1] :
( aUpperBoundOfIn0(X1,xT,xS)
& ! [X2] :
( ~ aElementOf0(X2,xT)
| sdtlseqdt0(X2,X1) )
& aElementOf0(X1,xS)
& ~ sdtlseqdt0(xp,X1) )
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& ? [X0] :
( aElementOf0(X0,xT)
& ~ sdtlseqdt0(X0,xp) ) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(flattening,[],[f75]) ).
fof(f123,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [X2,X3] :
( ~ aElementOf0(X3,szDzozmdt0(xf))
| ~ aElementOf0(X2,szDzozmdt0(xf))
| ~ sdtlseqdt0(X2,X3)
| sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [X0] :
( ( ~ aSubsetOf0(X0,xU)
& ( ? [X1] :
( aElementOf0(X1,X0)
& ~ aElementOf0(X1,xU) )
| ~ aSet0(X0) ) )
| sP2(X0) )
& aSet0(xU) ),
inference(rectify,[],[f80]) ).
fof(f124,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [X2,X3] :
( ~ aElementOf0(X3,szDzozmdt0(xf))
| ~ aElementOf0(X2,szDzozmdt0(xf))
| ~ sdtlseqdt0(X2,X3)
| sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [X0] :
( ( ~ aSubsetOf0(X0,xU)
& ( ( aElementOf0(sK18(X0),X0)
& ~ aElementOf0(sK18(X0),xU) )
| ~ aSet0(X0) ) )
| sP2(X0) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X1,sK18(X0))],[f123]) ).
fof(f125,plain,
( xP = cS1241(xU,xf,xT)
& ! [X0] :
( ( ( ~ aUpperBoundOfIn0(X0,xT,xU)
& aElementOf0(sK19(X0),xT)
& ~ sdtlseqdt0(sK19(X0),X0) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) )
& ( ~ aElementOf0(X0,xP)
| ( aUpperBoundOfIn0(X0,xT,xU)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,X0) )
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& aElementOf0(X0,xU) ) ) )
& aSet0(xP) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X2,sK19(X0))],[f72]) ).
fof(f126,plain,
( aInfimumOfIn0(xp,xP,xU)
& ! [X1] :
( ( ~ aLowerBoundOfIn0(X1,xP,xU)
& ( ( aElementOf0(sK20(X1),xP)
& ~ sdtlseqdt0(X1,sK20(X1)) )
| ~ aElementOf0(X1,xU) ) )
| sdtlseqdt0(X1,xp) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X0] :
( ~ aElementOf0(X0,xP)
| sdtlseqdt0(xp,X0) )
& aElementOf0(xp,xU)
& aElementOf0(xp,xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X2,sK20(X1))],[f73]) ).
fof(f130,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( sP3
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& aElementOf0(sK22,xT)
& ~ sdtlseqdt0(sK22,xp) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X0,sK22)],[f82]) ).
fof(f131,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| aElement0(X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f138,plain,
! [X0] :
( ~ aElement0(X0)
| sdtlseqdt0(X0,X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f139,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aElement0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f47]) ).
fof(f169,plain,
! [X0,X1] :
( ~ aFunction0(X0)
| ~ aElementOf0(X1,szDzozmdt0(X0))
| aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f197,plain,
xU = szRzazndt0(xf),
inference(cnf_transformation,[],[f124]) ).
fof(f198,plain,
szDzozmdt0(xf) = szRzazndt0(xf),
inference(cnf_transformation,[],[f124]) ).
fof(f200,plain,
! [X2,X3] :
( ~ aElementOf0(X3,szDzozmdt0(xf))
| ~ aElementOf0(X2,szDzozmdt0(xf))
| ~ sdtlseqdt0(X2,X3)
| sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f201,plain,
aFunction0(xf),
inference(cnf_transformation,[],[f124]) ).
fof(f206,plain,
aSet0(xU),
inference(cnf_transformation,[],[f124]) ).
fof(f208,plain,
! [X0] :
( ~ aFixedPointOf0(X0,xf)
| aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f69]) ).
fof(f210,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aFixedPointOf0(X0,xf) ),
inference(cnf_transformation,[],[f69]) ).
fof(f211,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| sdtlpdtrp0(xf,X0) = X0 ),
inference(cnf_transformation,[],[f69]) ).
fof(f212,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aElementOf0(X0,szDzozmdt0(xf)) ),
inference(cnf_transformation,[],[f69]) ).
fof(f216,plain,
aSet0(xT),
inference(cnf_transformation,[],[f70]) ).
fof(f218,plain,
! [X0] :
( ~ aUpperBoundOfIn0(X0,xT,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f125]) ).
fof(f219,plain,
! [X0] :
( aElementOf0(sK19(X0),xT)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f125]) ).
fof(f220,plain,
! [X0] :
( ~ sdtlseqdt0(sK19(X0),X0)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f125]) ).
fof(f227,plain,
! [X1] :
( ~ aLowerBoundOfIn0(X1,xP,xU)
| sdtlseqdt0(X1,xp) ),
inference(cnf_transformation,[],[f126]) ).
fof(f231,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| sdtlseqdt0(xp,X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f232,plain,
aElementOf0(xp,xU),
inference(cnf_transformation,[],[f126]) ).
fof(f233,plain,
aElementOf0(xp,xU),
inference(cnf_transformation,[],[f126]) ).
fof(f234,plain,
aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU),
inference(cnf_transformation,[],[f74]) ).
fof(f235,plain,
! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,sdtlpdtrp0(xf,xp)) ),
inference(cnf_transformation,[],[f74]) ).
fof(f236,plain,
aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU),
inference(cnf_transformation,[],[f74]) ).
fof(f237,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f248,plain,
( sP3
| aElementOf0(sK22,xT)
| xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f249,plain,
( sP3
| ~ sdtlseqdt0(sK22,xp)
| xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( aElement0(X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_56,plain,
! [X0: $i] :
( sdtlseqdt0(X0,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aElement0(X1)
| ~ aElement0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( aElementOf0(sdtlpdtrp0(X1,X0),szRzazndt0(X1))
| ~ aFunction0(X1)
| ~ aElementOf0(X0,szDzozmdt0(X1)) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_114,plain,
aSet0(xU),
inference(cnf_transformation,[],[f206]) ).
tcf(c_119,plain,
aFunction0(xf),
inference(cnf_transformation,[],[f201]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szDzozmdt0(xf))
| ~ aElementOf0(X0,szDzozmdt0(xf)) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_122,plain,
szDzozmdt0(xf) = szRzazndt0(xf),
inference(cnf_transformation,[],[f198]) ).
tcf(c_123,plain,
szRzazndt0(xf) = xU,
inference(cnf_transformation,[],[f197]) ).
tcf(c_126,plain,
! [X0: $i] :
( aElementOf0(X0,szDzozmdt0(xf))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_127,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xf,X0) = X0 )
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_128,plain,
! [X0: $i] :
( aFixedPointOf0(X0,xf)
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_130,plain,
! [X0: $i] :
( aElementOf0(X0,xS)
| ~ aFixedPointOf0(X0,xf) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_132,plain,
aSet0(xT),
inference(cnf_transformation,[],[f216]) ).
tcf(c_140,plain,
! [X0: $i] :
( aElementOf0(X0,xP)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(sK19(X0),X0)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_141,plain,
! [X0: $i] :
( aElementOf0(X0,xP)
| aElementOf0(sK19(X0),xT)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_142,plain,
! [X0: $i] :
( aElementOf0(X0,xP)
| ~ aElementOf0(X0,xU)
| ~ aUpperBoundOfIn0(X0,xT,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_144,plain,
aElementOf0(xp,xU),
inference(cnf_transformation,[],[f233]) ).
tcf(c_145,plain,
aElementOf0(xp,xU),
inference(cnf_transformation,[],[f232]) ).
tcf(c_146,plain,
! [X0: $i] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_150,plain,
! [X0: $i] :
( sdtlseqdt0(X0,xp)
| ~ aLowerBoundOfIn0(X0,xP,xU) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_152,plain,
! [X0: $i] :
( sdtlseqdt0(sdtlpdtrp0(xf,xp),X0)
| ~ aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_153,plain,
aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU),
inference(cnf_transformation,[],[f236]) ).
tcf(c_154,plain,
! [X0: $i] :
( sdtlseqdt0(X0,sdtlpdtrp0(xf,xp))
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_155,plain,
aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU),
inference(cnf_transformation,[],[f234]) ).
tcf(c_160,negated_conjecture,
( sP3
| ~ sdtlseqdt0(sK22,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf))
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_161,negated_conjecture,
( sP3
| aElementOf0(sK22,xT)
| ~ aElementOf0(xp,szDzozmdt0(xf))
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_295,plain,
! [X0: $i] :
( ~ aFixedPointOf0(X0,xf)
| aElementOf0(X0,szDzozmdt0(xf)) ),
inference(prop_impl_just,[status(thm)],[c_130,c_126]) ).
tcf(c_296,plain,
! [X0: $i] :
( aElementOf0(X0,szDzozmdt0(xf))
| ~ aFixedPointOf0(X0,xf) ),
inference(renaming,[status(thm)],[c_295]) ).
tcf(c_299,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xf,X0) = X0 )
| ~ aFixedPointOf0(X0,xf) ),
inference(prop_impl_just,[status(thm)],[c_130,c_127]) ).
tcf(c_1263,plain,
szDzozmdt0(xf) = xU,
inference(light_normalisation,[status(thm)],[c_122,c_123]) ).
tcf(c_1312,plain,
! [X0: $i] :
( aElementOf0(X0,xU)
| ~ aFixedPointOf0(X0,xf) ),
inference(light_normalisation,[status(thm)],[c_296,c_1263]) ).
tcf(c_1599,plain,
( sP3
| aElementOf0(sK22,xT)
| ~ aElementOf0(xp,xU)
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(light_normalisation,[status(thm)],[c_161,c_1263]) ).
tcf(c_1600,plain,
( sP3
| aElementOf0(sK22,xT)
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1599,c_144]) ).
tcf(c_1658,plain,
( sP3
| ~ sdtlseqdt0(sK22,xp)
| ~ aElementOf0(xp,xU)
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(light_normalisation,[status(thm)],[c_160,c_1263]) ).
tcf(c_1659,plain,
( sP3
| ~ sdtlseqdt0(sK22,xp)
| ( sdtlpdtrp0(xf,xp) != xp ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1658,c_144]) ).
tcf(c_1810,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1))
| ~ aElementOf0(X1,xU)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(X0,X1) ),
inference(light_normalisation,[status(thm)],[c_120,c_1263]) ).
tcf(c_2173,plain,
! [X0: $i,X1: $i] :
( aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ( X0 != xf ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_119]) ).
tcf(c_2174,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xf,X0),szRzazndt0(xf))
| ~ aElementOf0(X0,szDzozmdt0(xf)) ),
inference(unflattening,[status(thm)],[c_2173]) ).
tcf(c_5159,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xf,X0),szRzazndt0(xf))
| ~ aElementOf0(X0,szDzozmdt0(xf)) ),
inference(prop_impl_just,[status(thm)],[c_2174]) ).
tcf(c_6122,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xf,X0),xU)
| ~ aElementOf0(X0,xU) ),
inference(light_normalisation,[status(thm)],[c_5159,c_123,c_1263]) ).
tcf(c_9221,plain,
! [X0: $i] :
( aElementOf0(sdtlpdtrp0(xf,X0),xU)
| ~ aElementOf0(X0,xU) ),
inference(prop_impl_just,[status(thm)],[c_6122]) ).
tcf(c_9223,plain,
! [X0: $i] :
( ~ aFixedPointOf0(X0,xf)
| aElementOf0(X0,xU) ),
inference(prop_impl_just,[status(thm)],[c_1312]) ).
tcf(c_9224,plain,
! [X0: $i] :
( aElementOf0(X0,xU)
| ~ aFixedPointOf0(X0,xf) ),
inference(renaming,[status(thm)],[c_9223]) ).
tcf(c_9235,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xf,X0) = X0 )
| ~ aFixedPointOf0(X0,xf) ),
inference(prop_impl_just,[status(thm)],[c_299]) ).
tcf(c_13229,definition,
iPr_def_10 = sdtlpdtrp0(xf,xp),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_13231,plain,
( sP3
| ~ sdtlseqdt0(sK22,xp)
| ( iPr_def_10 != xp ) ),
inference(demodulation,[status(thm)],[c_1659]) ).
tcf(c_13232,plain,
( sP3
| aElementOf0(sK22,xT)
| ( iPr_def_10 != xp ) ),
inference(demodulation,[status(thm)],[c_1600]) ).
tcf(c_15271,plain,
aLowerBoundOfIn0(iPr_def_10,xP,xU),
inference(light_normalisation,[status(thm)],[c_153,c_13229]) ).
tcf(c_15272,plain,
aUpperBoundOfIn0(iPr_def_10,xT,xU),
inference(light_normalisation,[status(thm)],[c_155,c_13229]) ).
tcf(c_15346,plain,
sdtlseqdt0(iPr_def_10,xp),
inference(superposition,[status(thm)],[c_15271,c_150]) ).
tcf(c_15375,plain,
( aElement0(xp)
| ~ aSet0(xU) ),
inference(superposition,[status(thm)],[c_145,c_49]) ).
tcf(c_15378,plain,
aElement0(xp),
inference(forward_subsumption_resolution,[status(thm)],[c_15375,c_114]) ).
tcf(c_15479,plain,
! [X0: $i] :
( sdtlseqdt0(sdtlpdtrp0(xf,X0),iPr_def_10)
| ~ aElementOf0(xp,xU)
| ~ sdtlseqdt0(X0,xp)
| ~ aElementOf0(X0,xU) ),
inference(superposition,[status(thm)],[c_13229,c_1810]) ).
tcf(c_15480,plain,
! [X0: $i] :
( sdtlseqdt0(sdtlpdtrp0(xf,X0),iPr_def_10)
| ~ sdtlseqdt0(X0,xp)
| ~ aElementOf0(X0,xU) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15479,c_145]) ).
tcf(c_15495,plain,
! [X0: $i] :
( sdtlseqdt0(iPr_def_10,X0)
| ~ aElementOf0(X0,xP) ),
inference(light_normalisation,[status(thm)],[c_152,c_13229]) ).
tcf(c_15506,plain,
! [X0: $i] :
( sdtlseqdt0(X0,iPr_def_10)
| ~ aElementOf0(X0,xT) ),
inference(light_normalisation,[status(thm)],[c_154,c_13229]) ).
tcf(c_15598,plain,
( aElementOf0(iPr_def_10,xU)
| ~ aElementOf0(xp,xU) ),
inference(superposition,[status(thm)],[c_13229,c_9221]) ).
tcf(c_15600,plain,
aElementOf0(iPr_def_10,xU),
inference(forward_subsumption_resolution,[status(thm)],[c_15598,c_145]) ).
tcf(c_15643,plain,
( aElement0(iPr_def_10)
| ~ aSet0(xU) ),
inference(superposition,[status(thm)],[c_15600,c_49]) ).
tcf(c_15644,plain,
aElement0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_15643,c_114]) ).
tcf(c_16796,plain,
( aElementOf0(iPr_def_10,xP)
| ~ sdtlseqdt0(iPr_def_10,xp)
| ~ aElementOf0(iPr_def_10,xU)
| ~ aUpperBoundOfIn0(iPr_def_10,xT,xU) ),
inference(superposition,[status(thm)],[c_15480,c_142]) ).
tcf(c_16801,plain,
aElementOf0(iPr_def_10,xP),
inference(forward_subsumption_resolution,[status(thm)],[c_16796,c_15346,c_15600,c_15272]) ).
tcf(c_16829,plain,
sdtlseqdt0(xp,iPr_def_10),
inference(superposition,[status(thm)],[c_16801,c_146]) ).
tcf(c_16838,plain,
( ( xp = iPr_def_10 )
| ~ aElement0(iPr_def_10)
| ~ aElement0(xp)
| ~ sdtlseqdt0(iPr_def_10,xp) ),
inference(superposition,[status(thm)],[c_16829,c_57]) ).
tcf(c_16839,plain,
xp = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_16838,c_15644,c_15378,c_15346]) ).
tcf(c_16875,plain,
( sP3
| ~ sdtlseqdt0(sK22,iPr_def_10)
| ( iPr_def_10 != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_13231,c_16839]) ).
tcf(c_16876,plain,
( sP3
| aElementOf0(sK22,xT)
| ( iPr_def_10 != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_13232,c_16839]) ).
tcf(c_16892,plain,
( sP3
| aElementOf0(sK22,xT) ),
inference(equality_resolution_simp,[status(thm)],[c_16876]) ).
tcf(c_16895,plain,
( sP3
| ~ sdtlseqdt0(sK22,iPr_def_10) ),
inference(equality_resolution_simp,[status(thm)],[c_16875]) ).
tcf(c_17774,plain,
( sP3
| aElement0(sK22)
| ~ aSet0(xT) ),
inference(superposition,[status(thm)],[c_16892,c_49]) ).
tcf(c_17777,plain,
( sP3
| sdtlseqdt0(sK22,iPr_def_10) ),
inference(superposition,[status(thm)],[c_16892,c_15506]) ).
tcf(c_17783,plain,
( sP3
| aElement0(sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17774,c_132]) ).
tcf(c_17806,plain,
sP3,
inference(global_subsumption_just,[status(thm)],[c_17783,c_16895,c_17777]) ).
fof(f81,definition,
( ~ sP3
| ? [X1] :
( aUpperBoundOfIn0(X1,xT,xS)
& ! [X2] :
( ~ aElementOf0(X2,xT)
| sdtlseqdt0(X2,X1) )
& aElementOf0(X1,xS)
& ~ sdtlseqdt0(xp,X1) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f82,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( sP3
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& ? [X0] :
( aElementOf0(X0,xT)
& ~ sdtlseqdt0(X0,xp) ) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( xp != sdtlpdtrp0(xf,xp)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(definition_folding,[],[f76,f81]) ).
fof(f127,plain,
( ~ sP3
| ? [X1] :
( aUpperBoundOfIn0(X1,xT,xS)
& ! [X2] :
( ~ aElementOf0(X2,xT)
| sdtlseqdt0(X2,X1) )
& aElementOf0(X1,xS)
& ~ sdtlseqdt0(xp,X1) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f128,plain,
( ~ sP3
| ? [X0] :
( aUpperBoundOfIn0(X0,xT,xS)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,X0) )
& aElementOf0(X0,xS)
& ~ sdtlseqdt0(xp,X0) ) ),
inference(rectify,[],[f127]) ).
fof(f129,plain,
( ~ sP3
| ( aUpperBoundOfIn0(sK21,xT,xS)
& ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,sK21) )
& aElementOf0(sK21,xS)
& ~ sdtlseqdt0(xp,sK21) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X0,sK21)],[f128]) ).
fof(f239,plain,
! [X1] :
( ~ sP3
| ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,sK21) ),
inference(cnf_transformation,[],[f129]) ).
fof(f240,plain,
( ~ sP3
| aElementOf0(sK21,xS) ),
inference(cnf_transformation,[],[f129]) ).
fof(f241,plain,
( ~ sP3
| ~ sdtlseqdt0(xp,sK21) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_156,plain,
( ~ sP3
| ~ sdtlseqdt0(xp,sK21) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_157,plain,
( aElementOf0(sK21,xS)
| ~ sP3 ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_158,plain,
! [X0: $i] :
( sdtlseqdt0(X0,sK21)
| ~ sP3
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_15289,plain,
( aFixedPointOf0(sK21,xf)
| ~ sP3 ),
inference(superposition,[status(thm)],[c_157,c_128]) ).
tcf(c_15317,plain,
( aElementOf0(sK21,xU)
| ~ sP3 ),
inference(superposition,[status(thm)],[c_15289,c_9224]) ).
tcf(c_15377,plain,
( aElement0(sK21)
| ~ sP3
| ~ aSet0(xU) ),
inference(superposition,[status(thm)],[c_15317,c_49]) ).
tcf(c_15379,plain,
( aElement0(sK21)
| ~ sP3 ),
inference(forward_subsumption_resolution,[status(thm)],[c_15377,c_114]) ).
tcf(c_15640,plain,
( ( sdtlpdtrp0(xf,sK21) = sK21 )
| ~ sP3 ),
inference(superposition,[status(thm)],[c_15289,c_9235]) ).
tcf(c_16870,plain,
( ~ sP3
| ~ sdtlseqdt0(iPr_def_10,sK21) ),
inference(demodulation,[status(thm)],[c_156,c_16839]) ).
tcf(c_17812,plain,
sdtlpdtrp0(xf,sK21) = sK21,
inference(backward_subsumption_resolution,[status(thm)],[c_15640,c_17806]) ).
tcf(c_17813,plain,
aElement0(sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_15379,c_17806]) ).
tcf(c_17814,plain,
aElementOf0(sK21,xU),
inference(backward_subsumption_resolution,[status(thm)],[c_15317,c_17806]) ).
tcf(c_17817,plain,
! [X0: $i] :
( sdtlseqdt0(X0,sK21)
| ~ aElementOf0(X0,xT) ),
inference(backward_subsumption_resolution,[status(thm)],[c_158,c_17806]) ).
tcf(c_18031,plain,
( aElementOf0(sK21,xP)
| ~ sdtlseqdt0(sK21,sK21)
| ~ aElementOf0(sK21,xU)
| ~ sdtlseqdt0(sK19(sK21),sK21) ),
inference(superposition,[status(thm)],[c_17812,c_140]) ).
tcf(c_18032,plain,
( aElementOf0(sK21,xP)
| aElementOf0(sK19(sK21),xT)
| ~ sdtlseqdt0(sK21,sK21)
| ~ aElementOf0(sK21,xU) ),
inference(superposition,[status(thm)],[c_17812,c_141]) ).
tcf(c_18041,plain,
( aElementOf0(sK21,xP)
| aElementOf0(sK19(sK21),xT)
| ~ sdtlseqdt0(sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18032,c_17814]) ).
tcf(c_18045,plain,
( aElementOf0(sK21,xP)
| ~ sdtlseqdt0(sK21,sK21)
| ~ sdtlseqdt0(sK19(sK21),sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18031,c_17814]) ).
tcf(c_18212,plain,
~ sdtlseqdt0(iPr_def_10,sK21),
inference(global_subsumption_just,[status(thm)],[c_16870,c_16895,c_16870,c_17777]) ).
tcf(c_18333,plain,
( aElementOf0(sK21,xP)
| sdtlseqdt0(sK19(sK21),sK21)
| ~ sdtlseqdt0(sK21,sK21) ),
inference(superposition,[status(thm)],[c_18041,c_17817]) ).
tcf(c_18415,plain,
( aElementOf0(sK21,xP)
| ~ sdtlseqdt0(sK21,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_18333,c_18045,c_18333]) ).
tcf(c_18421,plain,
( aElementOf0(sK21,xP)
| ~ aElement0(sK21) ),
inference(superposition,[status(thm)],[c_56,c_18415]) ).
tcf(c_18422,plain,
aElementOf0(sK21,xP),
inference(forward_subsumption_resolution,[status(thm)],[c_18421,c_17813]) ).
tcf(c_18427,plain,
sdtlseqdt0(iPr_def_10,sK21),
inference(superposition,[status(thm)],[c_18422,c_15495]) ).
tcf(c_18429,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_18427,c_18212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.57 % Computer : n004.cluster.edu
% 0.11/5.57 % Model : x86_64 x86_64
% 0.11/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.57 % Memory : 8046.5625MB
% 0.11/5.57 % OS : Linux 6.8.0-71-generic
% 0.11/5.57 % CPULimit : 300
% 0.11/5.57 % WCLimit : 300
% 0.11/5.57 % DateTime : Wed Sep 23 21:31:12 UTC 2026
% 0.11/5.58 % CPUTime :
% 0.11/5.58 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.64 Running first-order theorem proving
% 0.14/5.64 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.66
% 0.14/5.66 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.66
% 0.14/5.66 % Detected problem language: tptp
% 0.14/5.68 % Proving...
% 5.39/7.09 % SZS status Started for theBenchmark.p
% 5.39/7.09 % SZS status Theorem for theBenchmark.p
% 5.39/7.09
% 5.39/7.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 5.39/7.09
% 5.39/7.09 % ------ iProver source info
% 5.39/7.09
% 5.39/7.09 % git: date: 2026-07-19 20:42:38 +0200
% 5.39/7.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 5.39/7.09 % git: non_committed_changes: false
% 5.39/7.09
% 5.39/7.09 % ------ Parsing...
% 5.39/7.09 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 5.39/7.09
% 5.39/7.09 % ------ Preprocessing... sup_sim: 8 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 9 sf_s rm: 6 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 5.39/7.09
% 5.39/7.09 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 5.39/7.09
% 5.39/7.09 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 5.39/7.09 % ------ Proving...
% 5.39/7.09 % ------ Problem Properties
% 5.39/7.09
% 5.39/7.09 %
% 5.39/7.09 % clauses 96
% 5.39/7.09 % conjectures 4
% 5.39/7.09 % EPR 47
% 5.39/7.09 % Horn 84
% 5.39/7.09 % unary 15
% 5.39/7.09 % binary 28
% 5.39/7.09 % lits 280
% 5.39/7.09 % lits eq 14
% 5.39/7.09 % fd_pure 0
% 5.39/7.09 % fd_pseudo 0
% 5.39/7.09 % fd_cond 0
% 5.39/7.09 % fd_pseudo_cond 3
% 5.39/7.09 % AC symbols 0
% 5.39/7.09
% 5.39/7.09 % ------ Schedule dynamic 5 is on
% 5.39/7.09
% 5.39/7.09 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 5.39/7.09
% 5.39/7.09
% 5.39/7.09 % ------
% 5.39/7.09 % Current options:
% 5.39/7.09 % ------
% 5.39/7.09
% 5.39/7.09
% 5.39/7.09 %
% 5.39/7.09
% 5.39/7.09 % ------ Proving...
% 5.39/7.09 %
% 5.39/7.09
% 5.39/7.09 % SZS status Theorem for theBenchmark.p
% 5.39/7.09
% 5.39/7.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 5.39/7.09
% 5.39/7.09
%------------------------------------------------------------------------------