%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 : Tue Sep 29 11:48:46 AM UTC 2026
% Result : Theorem 1.00s 0.80s
% Output : Refutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 36
% Syntax : Number of formulae : 282 ( 46 unt; 26 def)
% Number of atoms : 1113 ( 63 equ)
% Maximal formula atoms : 37 ( 3 avg)
% Number of connectives : 1283 ( 452 ~; 452 |; 303 &)
% ( 20 <=>; 56 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 22 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 10 con; 0-3 aty)
% Number of variables : 201 ( 0 sgn 166 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(f7,axiom,
! [X0] :
( aElement0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mARefl) ).
fof(f8,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mASymm) ).
fof(f21,axiom,
! [X0] :
( aFunction0(X0)
=> ! [X1] :
( aElementOf0(X1,szDzozmdt0(X0))
=> aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mImgSort) ).
fof(f24,axiom,
( aSet0(xU)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xU) ) )
| aSubsetOf0(X0,xU) )
=> ? [X1] :
( aElementOf0(X1,xU)
& aElementOf0(X1,xU)
& ! [X2] :
( aElementOf0(X2,X0)
=> sdtlseqdt0(X1,X2) )
& aLowerBoundOfIn0(X1,X0,xU)
& ! [X2] :
( ( ( aElementOf0(X2,xU)
& ! [X3] :
( aElementOf0(X3,X0)
=> sdtlseqdt0(X2,X3) ) )
| aLowerBoundOfIn0(X2,X0,xU) )
=> sdtlseqdt0(X2,X1) )
& aInfimumOfIn0(X1,X0,xU)
& ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( aElementOf0(X3,X0)
=> sdtlseqdt0(X3,X2) )
& aUpperBoundOfIn0(X2,X0,xU)
& ! [X3] :
( ( ( aElementOf0(X3,xU)
& ! [X4] :
( aElementOf0(X4,X0)
=> sdtlseqdt0(X4,X3) ) )
| aUpperBoundOfIn0(X3,X0,xU) )
=> sdtlseqdt0(X2,X3) )
& aSupremumOfIn0(X2,X0,xU) ) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X0,X1] :
( ( aElementOf0(X0,szDzozmdt0(xf))
& aElementOf0(X1,szDzozmdt0(xf)) )
=> ( sdtlseqdt0(X0,X1)
=> sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1)) ) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1123) ).
fof(f25,axiom,
( aSet0(xS)
& ! [X0] :
( ( aElementOf0(X0,xS)
=> ( aElementOf0(X0,szDzozmdt0(xf))
& sdtlpdtrp0(xf,X0) = X0
& aFixedPointOf0(X0,xf) ) )
& ( ( ( aElementOf0(X0,szDzozmdt0(xf))
& sdtlpdtrp0(xf,X0) = X0 )
| aFixedPointOf0(X0,xf) )
=> aElementOf0(X0,xS) ) )
& xS = cS1142(xf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1144) ).
fof(f27,axiom,
( aSet0(xP)
& ! [X0] :
( ( aElementOf0(X0,xP)
=> ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aUpperBoundOfIn0(X0,xT,xU) ) )
& ( ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ( ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
| aUpperBoundOfIn0(X0,xT,xU) ) )
=> aElementOf0(X0,xP) ) )
& xP = cS1241(xU,xf,xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1244) ).
fof(f28,axiom,
( aElementOf0(xp,xU)
& aElementOf0(xp,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(xp,X0) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X0] :
( ( ( aElementOf0(X0,xU)
& ! [X1] :
( aElementOf0(X1,xP)
=> sdtlseqdt0(X0,X1) ) )
| aLowerBoundOfIn0(X0,xP,xU) )
=> sdtlseqdt0(X0,xp) )
& aInfimumOfIn0(xp,xP,xU) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1261) ).
fof(f29,axiom,
( ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,sdtlpdtrp0(xf,xp)) )
& aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1299) ).
fof(f30,conjecture,
( ( ( aElementOf0(xp,szDzozmdt0(xf))
& sdtlpdtrp0(xf,xp) = xp )
| aFixedPointOf0(xp,xf) )
& ( ( ( ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) )
| aUpperBoundOfIn0(xp,xT,xS) )
& ! [X0] :
( ( aElementOf0(X0,xS)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aUpperBoundOfIn0(X0,xT,xS) )
=> sdtlseqdt0(xp,X0) ) )
| aSupremumOfIn0(xp,xT,xS) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f31,negated_conjecture,
~ ( ( ( aElementOf0(xp,szDzozmdt0(xf))
& sdtlpdtrp0(xf,xp) = xp )
| aFixedPointOf0(xp,xf) )
& ( ( ( ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) )
| aUpperBoundOfIn0(xp,xT,xS) )
& ! [X0] :
( ( aElementOf0(X0,xS)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aUpperBoundOfIn0(X0,xT,xS) )
=> sdtlseqdt0(xp,X0) ) )
| aSupremumOfIn0(xp,xT,xS) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f36,plain,
( aSet0(xU)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xU) ) )
| aSubsetOf0(X0,xU) )
=> ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( aElementOf0(X3,X0)
=> sdtlseqdt0(X2,X3) )
& aLowerBoundOfIn0(X2,X0,xU)
& ! [X4] :
( ( ( aElementOf0(X4,xU)
& ! [X5] :
( aElementOf0(X5,X0)
=> sdtlseqdt0(X4,X5) ) )
| aLowerBoundOfIn0(X4,X0,xU) )
=> sdtlseqdt0(X4,X2) )
& aInfimumOfIn0(X2,X0,xU)
& ? [X6] :
( aElementOf0(X6,xU)
& aElementOf0(X6,xU)
& ! [X7] :
( aElementOf0(X7,X0)
=> sdtlseqdt0(X7,X6) )
& aUpperBoundOfIn0(X6,X0,xU)
& ! [X8] :
( ( ( aElementOf0(X8,xU)
& ! [X9] :
( aElementOf0(X9,X0)
=> sdtlseqdt0(X9,X8) ) )
| aUpperBoundOfIn0(X8,X0,xU) )
=> sdtlseqdt0(X6,X8) )
& aSupremumOfIn0(X6,X0,xU) ) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X10,X11] :
( ( aElementOf0(X10,szDzozmdt0(xf))
& aElementOf0(X11,szDzozmdt0(xf)) )
=> ( sdtlseqdt0(X10,X11)
=> sdtlseqdt0(sdtlpdtrp0(xf,X10),sdtlpdtrp0(xf,X11)) ) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(rectify,[],[f24]) ).
fof(f37,plain,
( aSet0(xP)
& ! [X0] :
( ( aElementOf0(X0,xP)
=> ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,X0) )
& aUpperBoundOfIn0(X0,xT,xU) ) )
& ( ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ( ! [X2] :
( aElementOf0(X2,xT)
=> sdtlseqdt0(X2,X0) )
| aUpperBoundOfIn0(X0,xT,xU) ) )
=> aElementOf0(X0,xP) ) )
& xP = cS1241(xU,xf,xT) ),
inference(rectify,[],[f27]) ).
fof(f38,plain,
( aElementOf0(xp,xU)
& aElementOf0(xp,xU)
& ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(xp,X0) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X1] :
( ( ( aElementOf0(X1,xU)
& ! [X2] :
( aElementOf0(X2,xP)
=> sdtlseqdt0(X1,X2) ) )
| aLowerBoundOfIn0(X1,xP,xU) )
=> sdtlseqdt0(X1,xp) )
& aInfimumOfIn0(xp,xP,xU) ),
inference(rectify,[],[f28]) ).
fof(f39,plain,
( ! [X0] :
( aElementOf0(X0,xP)
=> sdtlseqdt0(sdtlpdtrp0(xf,xp),X0) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X1] :
( aElementOf0(X1,xT)
=> sdtlseqdt0(X1,sdtlpdtrp0(xf,xp)) )
& aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU) ),
inference(rectify,[],[f29]) ).
fof(f40,plain,
~ ( ( ( aElementOf0(xp,szDzozmdt0(xf))
& sdtlpdtrp0(xf,xp) = xp )
| aFixedPointOf0(xp,xf) )
& ( ( ( ! [X0] :
( aElementOf0(X0,xT)
=> sdtlseqdt0(X0,xp) )
| aUpperBoundOfIn0(xp,xT,xS) )
& ! [X1] :
( ( aElementOf0(X1,xS)
& ! [X2] :
( aElementOf0(X2,xT)
=> sdtlseqdt0(X2,X1) )
& aUpperBoundOfIn0(X1,xT,xS) )
=> sdtlseqdt0(xp,X1) ) )
| aSupremumOfIn0(xp,xT,xS) ) ),
inference(rectify,[],[f31]) ).
fof(f42,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f45,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f46,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f47,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f46]) ).
fof(f63,plain,
! [X0] :
( ! [X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0))
| ~ aElementOf0(X1,szDzozmdt0(X0)) )
| ~ aFunction0(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f67,plain,
( aSet0(xU)
& ! [X0] :
( ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( sdtlseqdt0(X2,X3)
| ~ aElementOf0(X3,X0) )
& aLowerBoundOfIn0(X2,X0,xU)
& ! [X4] :
( sdtlseqdt0(X4,X2)
| ( ( ~ aElementOf0(X4,xU)
| ? [X5] :
( ~ sdtlseqdt0(X4,X5)
& aElementOf0(X5,X0) ) )
& ~ aLowerBoundOfIn0(X4,X0,xU) ) )
& aInfimumOfIn0(X2,X0,xU)
& ? [X6] :
( aElementOf0(X6,xU)
& aElementOf0(X6,xU)
& ! [X7] :
( sdtlseqdt0(X7,X6)
| ~ aElementOf0(X7,X0) )
& aUpperBoundOfIn0(X6,X0,xU)
& ! [X8] :
( sdtlseqdt0(X6,X8)
| ( ( ~ aElementOf0(X8,xU)
| ? [X9] :
( ~ sdtlseqdt0(X9,X8)
& aElementOf0(X9,X0) ) )
& ~ aUpperBoundOfIn0(X8,X0,xU) ) )
& aSupremumOfIn0(X6,X0,xU) ) )
| ( ( ~ aSet0(X0)
| ? [X1] :
( ~ aElementOf0(X1,xU)
& aElementOf0(X1,X0) ) )
& ~ aSubsetOf0(X0,xU) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X10,X11] :
( sdtlseqdt0(sdtlpdtrp0(xf,X10),sdtlpdtrp0(xf,X11))
| ~ sdtlseqdt0(X10,X11)
| ~ aElementOf0(X10,szDzozmdt0(xf))
| ~ aElementOf0(X11,szDzozmdt0(xf)) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(ennf_transformation,[],[f36]) ).
fof(f68,plain,
( aSet0(xU)
& ! [X0] :
( ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( sdtlseqdt0(X2,X3)
| ~ aElementOf0(X3,X0) )
& aLowerBoundOfIn0(X2,X0,xU)
& ! [X4] :
( sdtlseqdt0(X4,X2)
| ( ( ~ aElementOf0(X4,xU)
| ? [X5] :
( ~ sdtlseqdt0(X4,X5)
& aElementOf0(X5,X0) ) )
& ~ aLowerBoundOfIn0(X4,X0,xU) ) )
& aInfimumOfIn0(X2,X0,xU)
& ? [X6] :
( aElementOf0(X6,xU)
& aElementOf0(X6,xU)
& ! [X7] :
( sdtlseqdt0(X7,X6)
| ~ aElementOf0(X7,X0) )
& aUpperBoundOfIn0(X6,X0,xU)
& ! [X8] :
( sdtlseqdt0(X6,X8)
| ( ( ~ aElementOf0(X8,xU)
| ? [X9] :
( ~ sdtlseqdt0(X9,X8)
& aElementOf0(X9,X0) ) )
& ~ aUpperBoundOfIn0(X8,X0,xU) ) )
& aSupremumOfIn0(X6,X0,xU) ) )
| ( ( ~ aSet0(X0)
| ? [X1] :
( ~ aElementOf0(X1,xU)
& aElementOf0(X1,X0) ) )
& ~ aSubsetOf0(X0,xU) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X10,X11] :
( sdtlseqdt0(sdtlpdtrp0(xf,X10),sdtlpdtrp0(xf,X11))
| ~ sdtlseqdt0(X10,X11)
| ~ aElementOf0(X10,szDzozmdt0(xf))
| ~ aElementOf0(X11,szDzozmdt0(xf)) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
( aSet0(xS)
& ! [X0] :
( ( ( aElementOf0(X0,szDzozmdt0(xf))
& sdtlpdtrp0(xf,X0) = X0
& aFixedPointOf0(X0,xf) )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ( ( ~ aElementOf0(X0,szDzozmdt0(xf))
| sdtlpdtrp0(xf,X0) != X0 )
& ~ aFixedPointOf0(X0,xf) ) ) )
& xS = cS1142(xf) ),
inference(ennf_transformation,[],[f25]) ).
fof(f71,plain,
( aSet0(xP)
& ! [X0] :
( ( ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ! [X1] :
( sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(X0,xT,xU) )
| ~ aElementOf0(X0,xP) )
& ( aElementOf0(X0,xP)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ( ? [X2] :
( ~ sdtlseqdt0(X2,X0)
& aElementOf0(X2,xT) )
& ~ aUpperBoundOfIn0(X0,xT,xU) ) ) )
& xP = cS1241(xU,xf,xT) ),
inference(ennf_transformation,[],[f37]) ).
fof(f72,plain,
( aSet0(xP)
& ! [X0] :
( ( ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ! [X1] :
( sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(X0,xT,xU) )
| ~ aElementOf0(X0,xP) )
& ( aElementOf0(X0,xP)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ( ? [X2] :
( ~ sdtlseqdt0(X2,X0)
& aElementOf0(X2,xT) )
& ~ aUpperBoundOfIn0(X0,xT,xU) ) ) )
& xP = cS1241(xU,xf,xT) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
( aElementOf0(xp,xU)
& aElementOf0(xp,xU)
& ! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xP) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X1] :
( sdtlseqdt0(X1,xp)
| ( ( ~ aElementOf0(X1,xU)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,xP) ) )
& ~ aLowerBoundOfIn0(X1,xP,xU) ) )
& aInfimumOfIn0(xp,xP,xU) ),
inference(ennf_transformation,[],[f38]) ).
fof(f74,plain,
( ! [X0] :
( sdtlseqdt0(sdtlpdtrp0(xf,xp),X0)
| ~ aElementOf0(X0,xP) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [X1] :
( sdtlseqdt0(X1,sdtlpdtrp0(xf,xp))
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU) ),
inference(ennf_transformation,[],[f39]) ).
fof(f75,plain,
( ( ( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp) )
& ~ aFixedPointOf0(xp,xf) )
| ( ( ( ? [X0] :
( ~ sdtlseqdt0(X0,xp)
& aElementOf0(X0,xT) )
& ~ aUpperBoundOfIn0(xp,xT,xS) )
| ? [X1] :
( ~ sdtlseqdt0(xp,X1)
& aElementOf0(X1,xS)
& ! [X2] :
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X2,xT) )
& aUpperBoundOfIn0(X1,xT,xS) ) )
& ~ aSupremumOfIn0(xp,xT,xS) ) ),
inference(ennf_transformation,[],[f40]) ).
fof(f76,plain,
( ( ( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp) )
& ~ aFixedPointOf0(xp,xf) )
| ( ( ( ? [X0] :
( ~ sdtlseqdt0(X0,xp)
& aElementOf0(X0,xT) )
& ~ aUpperBoundOfIn0(xp,xT,xS) )
| ? [X1] :
( ~ sdtlseqdt0(xp,X1)
& aElementOf0(X1,xS)
& ! [X2] :
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X2,xT) )
& aUpperBoundOfIn0(X1,xT,xS) ) )
& ~ aSupremumOfIn0(xp,xT,xS) ) ),
inference(flattening,[],[f75]) ).
fof(f77,definition,
! [X0] :
( ? [X6] :
( aElementOf0(X6,xU)
& aElementOf0(X6,xU)
& ! [X7] :
( sdtlseqdt0(X7,X6)
| ~ aElementOf0(X7,X0) )
& aUpperBoundOfIn0(X6,X0,xU)
& ! [X8] :
( sdtlseqdt0(X6,X8)
| ( ( ~ aElementOf0(X8,xU)
| ? [X9] :
( ~ sdtlseqdt0(X9,X8)
& aElementOf0(X9,X0) ) )
& ~ aUpperBoundOfIn0(X8,X0,xU) ) )
& aSupremumOfIn0(X6,X0,xU) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f78,definition,
! [X2,X0] :
( ! [X4] :
( sdtlseqdt0(X4,X2)
| ( ( ~ aElementOf0(X4,xU)
| ? [X5] :
( ~ sdtlseqdt0(X4,X5)
& aElementOf0(X5,X0) ) )
& ~ aLowerBoundOfIn0(X4,X0,xU) ) )
| ~ sP1(X2,X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f79,definition,
! [X0] :
( ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( sdtlseqdt0(X2,X3)
| ~ aElementOf0(X3,X0) )
& aLowerBoundOfIn0(X2,X0,xU)
& sP1(X2,X0)
& aInfimumOfIn0(X2,X0,xU)
& sP0(X0) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f80,plain,
( aSet0(xU)
& ! [X0] :
( sP2(X0)
| ( ( ~ aSet0(X0)
| ? [X1] :
( ~ aElementOf0(X1,xU)
& aElementOf0(X1,X0) ) )
& ~ aSubsetOf0(X0,xU) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X10,X11] :
( sdtlseqdt0(sdtlpdtrp0(xf,X10),sdtlpdtrp0(xf,X11))
| ~ sdtlseqdt0(X10,X11)
| ~ aElementOf0(X10,szDzozmdt0(xf))
| ~ aElementOf0(X11,szDzozmdt0(xf)) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(definition_folding,[],[f68,f79,f78,f77]) ).
fof(f81,definition,
( ? [X1] :
( ~ sdtlseqdt0(xp,X1)
& aElementOf0(X1,xS)
& ! [X2] :
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X2,xT) )
& aUpperBoundOfIn0(X1,xT,xS) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f82,plain,
( ( ( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp) )
& ~ aFixedPointOf0(xp,xf) )
| ( ( ( ? [X0] :
( ~ sdtlseqdt0(X0,xp)
& aElementOf0(X0,xT) )
& ~ aUpperBoundOfIn0(xp,xT,xS) )
| sP3 )
& ~ aSupremumOfIn0(xp,xT,xS) ) ),
inference(definition_folding,[],[f76,f81]) ).
fof(f114,plain,
! [X0] :
( ? [X2] :
( aElementOf0(X2,xU)
& aElementOf0(X2,xU)
& ! [X3] :
( sdtlseqdt0(X2,X3)
| ~ aElementOf0(X3,X0) )
& aLowerBoundOfIn0(X2,X0,xU)
& sP1(X2,X0)
& aInfimumOfIn0(X2,X0,xU)
& sP0(X0) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f79]) ).
fof(f115,plain,
! [X0] :
( ? [X1] :
( aElementOf0(X1,xU)
& aElementOf0(X1,xU)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) )
& aLowerBoundOfIn0(X1,X0,xU)
& sP1(X1,X0)
& aInfimumOfIn0(X1,X0,xU)
& sP0(X0) )
| ~ sP2(X0) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ( aElementOf0(sK14(X0),xU)
& aElementOf0(sK14(X0),xU)
& ! [X2] :
( sdtlseqdt0(sK14(X0),X2)
| ~ aElementOf0(X2,X0) )
& aLowerBoundOfIn0(sK14(X0),X0,xU)
& sP1(sK14(X0),X0)
& aInfimumOfIn0(sK14(X0),X0,xU)
& sP0(X0) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X1,sK14(X0))],[f115]) ).
fof(f117,plain,
! [X2,X0] :
( ! [X4] :
( sdtlseqdt0(X4,X2)
| ( ( ~ aElementOf0(X4,xU)
| ? [X5] :
( ~ sdtlseqdt0(X4,X5)
& aElementOf0(X5,X0) ) )
& ~ aLowerBoundOfIn0(X4,X0,xU) ) )
| ~ sP1(X2,X0) ),
inference(nnf_transformation,[],[f78]) ).
fof(f118,plain,
! [X0,X1] :
( ! [X2] :
( sdtlseqdt0(X2,X0)
| ( ( ~ aElementOf0(X2,xU)
| ? [X3] :
( ~ sdtlseqdt0(X2,X3)
& aElementOf0(X3,X1) ) )
& ~ aLowerBoundOfIn0(X2,X1,xU) ) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( ! [X2] :
( sdtlseqdt0(X2,X0)
| ( ( ~ aElementOf0(X2,xU)
| ( ~ sdtlseqdt0(X2,sK15(X1,X2))
& aElementOf0(sK15(X1,X2),X1) ) )
& ~ aLowerBoundOfIn0(X2,X1,xU) ) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X3,sK15(X1,X2))],[f118]) ).
fof(f123,plain,
( aSet0(xU)
& ! [X0] :
( sP2(X0)
| ( ( ~ aSet0(X0)
| ? [X1] :
( ~ aElementOf0(X1,xU)
& aElementOf0(X1,X0) ) )
& ~ aSubsetOf0(X0,xU) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X2,X3] :
( sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3))
| ~ sdtlseqdt0(X2,X3)
| ~ aElementOf0(X2,szDzozmdt0(xf))
| ~ aElementOf0(X3,szDzozmdt0(xf)) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(rectify,[],[f80]) ).
fof(f124,plain,
( aSet0(xU)
& ! [X0] :
( sP2(X0)
| ( ( ~ aSet0(X0)
| ( ~ aElementOf0(sK18(X0),xU)
& aElementOf0(sK18(X0),X0) ) )
& ~ aSubsetOf0(X0,xU) ) )
& aCompleteLattice0(xU)
& aFunction0(xf)
& ! [X2,X3] :
( sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3))
| ~ sdtlseqdt0(X2,X3)
| ~ aElementOf0(X2,szDzozmdt0(xf))
| ~ aElementOf0(X3,szDzozmdt0(xf)) )
& isMonotone0(xf)
& szDzozmdt0(xf) = szRzazndt0(xf)
& szRzazndt0(xf) = xU
& isOn0(xf,xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X1,sK18(X0))],[f123]) ).
fof(f125,plain,
( aSet0(xP)
& ! [X0] :
( ( ( aElementOf0(X0,xU)
& sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
& ! [X1] :
( sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(X0,xT,xU) )
| ~ aElementOf0(X0,xP) )
& ( aElementOf0(X0,xP)
| ~ aElementOf0(X0,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ( ~ sdtlseqdt0(sK19(X0),X0)
& aElementOf0(sK19(X0),xT)
& ~ aUpperBoundOfIn0(X0,xT,xU) ) ) )
& xP = cS1241(xU,xf,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X2,sK19(X0))],[f72]) ).
fof(f126,plain,
( aElementOf0(xp,xU)
& aElementOf0(xp,xU)
& ! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xP) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [X1] :
( sdtlseqdt0(X1,xp)
| ( ( ~ aElementOf0(X1,xU)
| ( ~ sdtlseqdt0(X1,sK20(X1))
& aElementOf0(sK20(X1),xP) ) )
& ~ aLowerBoundOfIn0(X1,xP,xU) ) )
& aInfimumOfIn0(xp,xP,xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X2,sK20(X1))],[f73]) ).
fof(f127,plain,
( ? [X1] :
( ~ sdtlseqdt0(xp,X1)
& aElementOf0(X1,xS)
& ! [X2] :
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X2,xT) )
& aUpperBoundOfIn0(X1,xT,xS) )
| ~ sP3 ),
inference(nnf_transformation,[],[f81]) ).
fof(f128,plain,
( ? [X0] :
( ~ sdtlseqdt0(xp,X0)
& aElementOf0(X0,xS)
& ! [X1] :
( sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(X0,xT,xS) )
| ~ sP3 ),
inference(rectify,[],[f127]) ).
fof(f129,plain,
( ( ~ sdtlseqdt0(xp,sK21)
& aElementOf0(sK21,xS)
& ! [X1] :
( sdtlseqdt0(X1,sK21)
| ~ aElementOf0(X1,xT) )
& aUpperBoundOfIn0(sK21,xT,xS) )
| ~ sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X0,sK21)],[f128]) ).
fof(f130,plain,
( ( ( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp) )
& ~ aFixedPointOf0(xp,xf) )
| ( ( ( ~ sdtlseqdt0(sK22,xp)
& aElementOf0(sK22,xT)
& ~ aUpperBoundOfIn0(xp,xT,xS) )
| sP3 )
& ~ aSupremumOfIn0(xp,xT,xS) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X0,sK22)],[f82]) ).
fof(f131,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f138,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f139,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f169,plain,
! [X0,X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f180,plain,
! [X0] :
( sP1(sK14(X0),X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f181,plain,
! [X0] :
( aLowerBoundOfIn0(sK14(X0),X0,xU)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f182,plain,
! [X2,X0] :
( ~ aElementOf0(X2,X0)
| sdtlseqdt0(sK14(X0),X2)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f183,plain,
! [X0] :
( aElementOf0(sK14(X0),xU)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f185,plain,
! [X2,X0,X1] :
( ~ aLowerBoundOfIn0(X2,X1,xU)
| sdtlseqdt0(X2,X0)
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
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))
| ~ sdtlseqdt0(X2,X3)
| ~ aElementOf0(X2,szDzozmdt0(xf))
| sdtlseqdt0(sdtlpdtrp0(xf,X2),sdtlpdtrp0(xf,X3)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f201,plain,
aFunction0(xf),
inference(cnf_transformation,[],[f124]) ).
fof(f204,plain,
! [X0] :
( aElementOf0(sK18(X0),X0)
| ~ aSet0(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f205,plain,
! [X0] :
( ~ aElementOf0(sK18(X0),xU)
| ~ aSet0(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f206,plain,
aSet0(xU),
inference(cnf_transformation,[],[f124]) ).
fof(f207,plain,
xS = cS1142(xf),
inference(cnf_transformation,[],[f69]) ).
fof(f211,plain,
! [X0] :
( sdtlpdtrp0(xf,X0) = X0
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f69]) ).
fof(f212,plain,
! [X0] :
( aElementOf0(X0,szDzozmdt0(xf))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f69]) ).
fof(f213,plain,
aSet0(xS),
inference(cnf_transformation,[],[f69]) ).
fof(f218,plain,
! [X0] :
( ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP)
| ~ aUpperBoundOfIn0(X0,xT,xU) ),
inference(cnf_transformation,[],[f125]) ).
fof(f219,plain,
! [X0] :
( ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP)
| aElementOf0(sK19(X0),xT) ),
inference(cnf_transformation,[],[f125]) ).
fof(f220,plain,
! [X0] :
( ~ sdtlseqdt0(sdtlpdtrp0(xf,X0),X0)
| ~ aElementOf0(X0,xU)
| aElementOf0(X0,xP)
| ~ sdtlseqdt0(sK19(X0),X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f224,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xU) ),
inference(cnf_transformation,[],[f125]) ).
fof(f225,plain,
aSet0(xP),
inference(cnf_transformation,[],[f125]) ).
fof(f227,plain,
! [X1] :
( ~ aLowerBoundOfIn0(X1,xP,xU)
| sdtlseqdt0(X1,xp) ),
inference(cnf_transformation,[],[f126]) ).
fof(f230,plain,
aLowerBoundOfIn0(xp,xP,xU),
inference(cnf_transformation,[],[f126]) ).
fof(f232,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(f239,plain,
! [X1] :
( sdtlseqdt0(X1,sK21)
| ~ aElementOf0(X1,xT)
| ~ sP3 ),
inference(cnf_transformation,[],[f129]) ).
fof(f240,plain,
( aElementOf0(sK21,xS)
| ~ sP3 ),
inference(cnf_transformation,[],[f129]) ).
fof(f241,plain,
( ~ sdtlseqdt0(xp,sK21)
| ~ sP3 ),
inference(cnf_transformation,[],[f129]) ).
fof(f248,plain,
( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp)
| aElementOf0(sK22,xT)
| sP3 ),
inference(cnf_transformation,[],[f130]) ).
fof(f249,plain,
( ~ aElementOf0(xp,szDzozmdt0(xf))
| xp != sdtlpdtrp0(xf,xp)
| ~ sdtlseqdt0(sK22,xp)
| sP3 ),
inference(cnf_transformation,[],[f130]) ).
fof(f251,definition,
sF23 = szDzozmdt0(xf),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f252,plain,
szDzozmdt0(xf) = sF23,
inference(reorient_equations,[],[f251]) ).
fof(f253,definition,
sF24 = sdtlpdtrp0(xf,xp),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f254,plain,
sdtlpdtrp0(xf,xp) = sF24,
inference(reorient_equations,[],[f253]) ).
fof(f255,plain,
( ~ aElementOf0(xp,sF23)
| xp != sF24
| ~ sdtlseqdt0(sK22,xp)
| sP3 ),
inference(definition_folding,[],[f249,f254,f252]) ).
fof(f256,plain,
( ~ aElementOf0(xp,sF23)
| xp != sF24
| aElementOf0(sK22,xT)
| sP3 ),
inference(definition_folding,[],[f248,f254,f252]) ).
fof(f269,definition,
( spl25_3
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition]) ).
fof(f278,definition,
( spl25_5
<=> aElementOf0(sK22,xT) ),
introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition]) ).
fof(f280,plain,
( aElementOf0(sK22,xT)
| ~ spl25_5 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f283,definition,
( spl25_6
<=> sdtlseqdt0(sK22,xp) ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
fof(f285,plain,
( ~ sdtlseqdt0(sK22,xp)
| spl25_6 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f288,definition,
( spl25_7
<=> xp = sF24 ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
fof(f289,plain,
( xp = sF24
| ~ spl25_7 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f290,plain,
( xp != sF24
| spl25_7 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl25_8
<=> aElementOf0(xp,sF23) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f294,plain,
( ~ aElementOf0(xp,sF23)
| spl25_8 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f297,plain,
( spl25_3
| spl25_5
| ~ spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f256,f292,f288,f278,f269]) ).
fof(f298,plain,
( spl25_3
| ~ spl25_6
| ~ spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f255,f292,f288,f283,f269]) ).
fof(f305,definition,
( spl25_10
<=> ! [X1] :
( sdtlseqdt0(X1,sK21)
| ~ aElementOf0(X1,xT) ) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f306,plain,
( ! [X1] :
( ~ aElementOf0(X1,xT)
| sdtlseqdt0(X1,sK21) )
| ~ spl25_10 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f307,plain,
( ~ spl25_3
| spl25_10 ),
inference(avatar_split_clause,[],[f239,f305,f269]) ).
fof(f309,definition,
( spl25_11
<=> aElementOf0(sK21,xS) ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
fof(f311,plain,
( aElementOf0(sK21,xS)
| ~ spl25_11 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( ~ spl25_3
| spl25_11 ),
inference(avatar_split_clause,[],[f240,f309,f269]) ).
fof(f314,definition,
( spl25_12
<=> sdtlseqdt0(xp,sK21) ),
introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition]) ).
fof(f316,plain,
( ~ sdtlseqdt0(xp,sK21)
| spl25_12 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f317,plain,
( ~ spl25_3
| ~ spl25_12 ),
inference(avatar_split_clause,[],[f241,f314,f269]) ).
fof(f321,plain,
! [X0] :
( ~ aElementOf0(X0,cS1142(xf))
| sdtlpdtrp0(xf,X0) = X0 ),
inference(forward_demodulation,[],[f211,f207]) ).
fof(f322,plain,
! [X0] :
( ~ aElementOf0(X0,cS1142(xf))
| aElementOf0(X0,szDzozmdt0(xf)) ),
inference(forward_demodulation,[],[f212,f207]) ).
fof(f323,plain,
aSet0(cS1142(xf)),
inference(forward_demodulation,[],[f213,f207]) ).
fof(f324,plain,
xU = szDzozmdt0(xf),
inference(forward_demodulation,[],[f198,f197]) ).
fof(f326,plain,
! [X0] :
( ~ aElementOf0(X0,cS1142(xf))
| aElementOf0(X0,sF23) ),
inference(forward_demodulation,[],[f322,f252]) ).
fof(f330,plain,
xU = sF23,
inference(superposition,[],[f324,f252]) ).
fof(f331,plain,
( ~ aElementOf0(xp,xU)
| spl25_8 ),
inference(superposition,[],[f294,f330]) ).
fof(f332,plain,
( $false
| spl25_8 ),
inference(forward_subsumption_resolution,[],[f331,f232]) ).
fof(f333,plain,
spl25_8,
inference(avatar_contradiction_clause,[],[f332]) ).
fof(f340,plain,
aUpperBoundOfIn0(sF24,xT,xU),
inference(superposition,[],[f234,f254]) ).
fof(f341,plain,
aLowerBoundOfIn0(sF24,xP,xU),
inference(superposition,[],[f236,f254]) ).
fof(f344,plain,
sdtlseqdt0(sF24,xp),
inference(resolution,[],[f227,f341]) ).
fof(f349,plain,
( aElement0(xp)
| ~ aSet0(xU) ),
inference(resolution,[],[f131,f232]) ).
fof(f350,plain,
! [X0] :
( aElement0(sK14(X0))
| ~ aSet0(xU)
| ~ sP2(X0) ),
inference(resolution,[],[f131,f183]) ).
fof(f355,plain,
! [X0] :
( ~ sP2(X0)
| aElement0(sK14(X0)) ),
inference(forward_subsumption_resolution,[],[f350,f206]) ).
fof(f356,plain,
aElement0(xp),
inference(forward_subsumption_resolution,[],[f349,f206]) ).
fof(f388,plain,
( ~ sP2(xP)
| sdtlseqdt0(sK14(xP),xp) ),
inference(resolution,[],[f181,f227]) ).
fof(f390,definition,
( spl25_18
<=> sdtlseqdt0(sK14(xP),xp) ),
introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition]) ).
fof(f392,plain,
( sdtlseqdt0(sK14(xP),xp)
| ~ spl25_18 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f394,definition,
( spl25_19
<=> sP2(xP) ),
introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition]) ).
fof(f395,plain,
( sP2(xP)
| ~ spl25_19 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f396,plain,
( ~ sP2(xP)
| spl25_19 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( spl25_18
| ~ spl25_19 ),
inference(avatar_split_clause,[],[f388,f394,f390]) ).
fof(f404,plain,
( ~ aSet0(xP)
| sP2(xP)
| aElementOf0(sK18(xP),xU) ),
inference(resolution,[],[f204,f224]) ).
fof(f407,plain,
( sP2(xP)
| aElementOf0(sK18(xP),xU) ),
inference(forward_subsumption_resolution,[],[f404,f225]) ).
fof(f412,plain,
( aElementOf0(sK18(xP),xU)
| spl25_19 ),
inference(forward_subsumption_resolution,[],[f407,f396]) ).
fof(f562,plain,
( ~ aSet0(xP)
| sP2(xP)
| spl25_19 ),
inference(resolution,[],[f412,f205]) ).
fof(f568,plain,
( sP2(xP)
| spl25_19 ),
inference(forward_subsumption_resolution,[],[f562,f225]) ).
fof(f569,plain,
( $false
| spl25_19 ),
inference(forward_subsumption_resolution,[],[f568,f396]) ).
fof(f570,plain,
spl25_19,
inference(avatar_contradiction_clause,[],[f569]) ).
fof(f584,plain,
( aElement0(sK14(xP))
| ~ spl25_19 ),
inference(resolution,[],[f395,f355]) ).
fof(f601,plain,
! [X0] :
( ~ sP1(X0,xP)
| sdtlseqdt0(xp,X0) ),
inference(resolution,[],[f185,f230]) ).
fof(f675,definition,
( spl25_34
<=> aElementOf0(sF24,xU) ),
introduced(definition,[new_symbols(definition,[spl25_34])],[avatar_definition]) ).
fof(f677,plain,
( aElementOf0(sF24,xU)
| ~ spl25_34 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f719,plain,
( aElementOf0(sF24,szRzazndt0(xf))
| ~ aElementOf0(xp,szDzozmdt0(xf))
| ~ aFunction0(xf) ),
inference(superposition,[],[f169,f254]) ).
fof(f722,plain,
( aElementOf0(sF24,szRzazndt0(xf))
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(forward_subsumption_resolution,[],[f719,f201]) ).
fof(f726,plain,
( aElementOf0(sF24,xU)
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(forward_demodulation,[],[f722,f197]) ).
fof(f728,plain,
( ~ aElementOf0(xp,sF23)
| aElementOf0(sF24,xU) ),
inference(forward_demodulation,[],[f726,f252]) ).
fof(f729,plain,
( ~ aElementOf0(xp,xU)
| aElementOf0(sF24,xU) ),
inference(forward_demodulation,[],[f728,f330]) ).
fof(f730,plain,
aElementOf0(sF24,xU),
inference(forward_subsumption_resolution,[],[f729,f232]) ).
fof(f731,plain,
spl25_34,
inference(avatar_split_clause,[],[f730,f675]) ).
fof(f735,plain,
( aElement0(sF24)
| ~ aSet0(xU)
| ~ spl25_34 ),
inference(resolution,[],[f677,f131]) ).
fof(f736,plain,
( aElement0(sF24)
| ~ spl25_34 ),
inference(forward_subsumption_resolution,[],[f735,f206]) ).
fof(f743,plain,
( ~ sdtlseqdt0(xp,sK14(xP))
| xp = sK14(xP)
| ~ aElement0(xp)
| ~ aElement0(sK14(xP))
| ~ spl25_18 ),
inference(resolution,[],[f139,f392]) ).
fof(f746,plain,
( ~ sdtlseqdt0(xp,sF24)
| xp = sF24
| ~ aElement0(xp)
| ~ aElement0(sF24) ),
inference(resolution,[],[f139,f344]) ).
fof(f749,plain,
( ~ sdtlseqdt0(xp,sF24)
| ~ aElement0(xp)
| ~ aElement0(sF24)
| spl25_7 ),
inference(forward_subsumption_resolution,[],[f746,f290]) ).
fof(f752,plain,
( ~ sdtlseqdt0(xp,sK14(xP))
| xp = sK14(xP)
| ~ aElement0(sK14(xP))
| ~ spl25_18 ),
inference(forward_subsumption_resolution,[],[f743,f356]) ).
fof(f755,plain,
( ~ sdtlseqdt0(xp,sF24)
| ~ aElement0(sF24)
| spl25_7 ),
inference(forward_subsumption_resolution,[],[f749,f356]) ).
fof(f758,plain,
( ~ sdtlseqdt0(xp,sK14(xP))
| xp = sK14(xP)
| ~ spl25_18
| ~ spl25_19 ),
inference(forward_subsumption_resolution,[],[f752,f584]) ).
fof(f761,plain,
( ~ sdtlseqdt0(xp,sF24)
| spl25_7
| ~ spl25_34 ),
inference(forward_subsumption_resolution,[],[f755,f736]) ).
fof(f781,definition,
( spl25_40
<=> xp = sK14(xP) ),
introduced(definition,[new_symbols(definition,[spl25_40])],[avatar_definition]) ).
fof(f783,plain,
( xp = sK14(xP)
| ~ spl25_40 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f785,definition,
( spl25_41
<=> sdtlseqdt0(xp,sK14(xP)) ),
introduced(definition,[new_symbols(definition,[spl25_41])],[avatar_definition]) ).
fof(f787,plain,
( ~ sdtlseqdt0(xp,sK14(xP))
| spl25_41 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f788,plain,
( spl25_40
| ~ spl25_41
| ~ spl25_18
| ~ spl25_19 ),
inference(avatar_split_clause,[],[f758,f394,f390,f785,f781]) ).
fof(f1087,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,xU)
| ~ aElementOf0(X1,xU)
| sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)) ),
inference(superposition,[],[f200,f324]) ).
fof(f1246,plain,
( sdtlseqdt0(xp,sK14(xP))
| ~ sP2(xP) ),
inference(resolution,[],[f601,f180]) ).
fof(f1247,plain,
( ~ sP2(xP)
| spl25_41 ),
inference(forward_subsumption_resolution,[],[f1246,f787]) ).
fof(f1248,plain,
( $false
| ~ spl25_19
| spl25_41 ),
inference(forward_subsumption_resolution,[],[f1247,f395]) ).
fof(f1249,plain,
( ~ spl25_19
| spl25_41 ),
inference(avatar_contradiction_clause,[],[f1248]) ).
fof(f1255,plain,
( aElementOf0(sK14(xP),xU)
| ~ spl25_40 ),
inference(superposition,[],[f232,f783]) ).
fof(f1258,plain,
( sF24 = sdtlpdtrp0(xf,sK14(xP))
| ~ spl25_40 ),
inference(superposition,[],[f254,f783]) ).
fof(f1261,plain,
( sdtlseqdt0(sF24,sK14(xP))
| ~ spl25_40 ),
inference(superposition,[],[f344,f783]) ).
fof(f1267,plain,
( ~ sdtlseqdt0(sK14(xP),sF24)
| spl25_7
| ~ spl25_34
| ~ spl25_40 ),
inference(superposition,[],[f761,f783]) ).
fof(f4434,plain,
( ~ aElementOf0(sK14(xP),xU)
| ~ aElementOf0(sF24,xU)
| sdtlseqdt0(sdtlpdtrp0(xf,sF24),sdtlpdtrp0(xf,sK14(xP)))
| ~ spl25_40 ),
inference(resolution,[],[f1087,f1261]) ).
fof(f4443,plain,
( ~ aElementOf0(sF24,xU)
| sdtlseqdt0(sdtlpdtrp0(xf,sF24),sdtlpdtrp0(xf,sK14(xP)))
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f4434,f1255]) ).
fof(f4514,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,sF24),sdtlpdtrp0(xf,sK14(xP)))
| ~ spl25_34
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f4443,f677]) ).
fof(f4593,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,sF24),sF24)
| ~ spl25_34
| ~ spl25_40 ),
inference(forward_demodulation,[],[f4514,f1258]) ).
fof(f5906,plain,
( ~ aElementOf0(sF24,xU)
| aElementOf0(sF24,xP)
| ~ aUpperBoundOfIn0(sF24,xT,xU)
| ~ spl25_34
| ~ spl25_40 ),
inference(resolution,[],[f4593,f218]) ).
fof(f5913,plain,
( aElementOf0(sF24,xP)
| ~ aUpperBoundOfIn0(sF24,xT,xU)
| ~ spl25_34
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f5906,f677]) ).
fof(f5934,plain,
( aElementOf0(sF24,xP)
| ~ spl25_34
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f5913,f340]) ).
fof(f5940,definition,
( spl25_351
<=> aElementOf0(sF24,xP) ),
introduced(definition,[new_symbols(definition,[spl25_351])],[avatar_definition]) ).
fof(f5942,plain,
( aElementOf0(sF24,xP)
| ~ spl25_351 ),
inference(avatar_component_clause,[],[f5940]) ).
fof(f5949,plain,
( spl25_351
| ~ spl25_34
| ~ spl25_40 ),
inference(avatar_split_clause,[],[f5934,f781,f675,f5940]) ).
fof(f5968,plain,
( sdtlseqdt0(sK14(xP),sF24)
| ~ sP2(xP)
| ~ spl25_351 ),
inference(resolution,[],[f5942,f182]) ).
fof(f5971,plain,
( ~ sP2(xP)
| spl25_7
| ~ spl25_34
| ~ spl25_40
| ~ spl25_351 ),
inference(forward_subsumption_resolution,[],[f5968,f1267]) ).
fof(f5976,plain,
( $false
| spl25_7
| ~ spl25_19
| ~ spl25_34
| ~ spl25_40
| ~ spl25_351 ),
inference(forward_subsumption_resolution,[],[f5971,f395]) ).
fof(f5977,plain,
( spl25_7
| ~ spl25_19
| ~ spl25_34
| ~ spl25_40
| ~ spl25_351 ),
inference(avatar_contradiction_clause,[],[f5976]) ).
fof(f5981,plain,
( sF24 = sK14(xP)
| ~ spl25_7
| ~ spl25_40 ),
inference(forward_demodulation,[],[f289,f783]) ).
fof(f5983,plain,
( aElementOf0(sK21,cS1142(xf))
| ~ spl25_11 ),
inference(forward_demodulation,[],[f311,f207]) ).
fof(f5984,plain,
( ~ sdtlseqdt0(sK14(xP),sK21)
| spl25_12
| ~ spl25_40 ),
inference(forward_demodulation,[],[f316,f783]) ).
fof(f6091,plain,
( aElementOf0(sK21,sF23)
| ~ spl25_11 ),
inference(resolution,[],[f5983,f326]) ).
fof(f6096,plain,
( aElement0(sK21)
| ~ aSet0(cS1142(xf))
| ~ spl25_11 ),
inference(resolution,[],[f5983,f131]) ).
fof(f6097,plain,
( aElement0(sK21)
| ~ spl25_11 ),
inference(forward_subsumption_resolution,[],[f6096,f323]) ).
fof(f6100,plain,
( aElementOf0(sK21,xU)
| ~ spl25_11 ),
inference(forward_demodulation,[],[f6091,f330]) ).
fof(f6385,plain,
( ~ sdtlseqdt0(sK22,sK14(xP))
| spl25_6
| ~ spl25_40 ),
inference(forward_demodulation,[],[f285,f783]) ).
fof(f6397,plain,
( sdtlseqdt0(sK22,sdtlpdtrp0(xf,xp))
| ~ spl25_5 ),
inference(resolution,[],[f280,f235]) ).
fof(f6407,plain,
( sdtlseqdt0(sK22,sF24)
| ~ spl25_5 ),
inference(forward_demodulation,[],[f6397,f254]) ).
fof(f6668,definition,
( spl25_408
<=> aElementOf0(sK21,xU) ),
introduced(definition,[new_symbols(definition,[spl25_408])],[avatar_definition]) ).
fof(f6669,plain,
( aElementOf0(sK21,xU)
| ~ spl25_408 ),
inference(avatar_component_clause,[],[f6668]) ).
fof(f6670,plain,
( ~ aElementOf0(sK21,xU)
| spl25_408 ),
inference(avatar_component_clause,[],[f6668]) ).
fof(f6673,definition,
( spl25_409
<=> aElement0(sK21) ),
introduced(definition,[new_symbols(definition,[spl25_409])],[avatar_definition]) ).
fof(f6674,plain,
( aElement0(sK21)
| ~ spl25_409 ),
inference(avatar_component_clause,[],[f6673]) ).
fof(f6675,plain,
( ~ aElement0(sK21)
| spl25_409 ),
inference(avatar_component_clause,[],[f6673]) ).
fof(f6707,plain,
( sdtlseqdt0(sK22,sK14(xP))
| ~ spl25_5
| ~ spl25_7
| ~ spl25_40 ),
inference(superposition,[],[f6407,f5981]) ).
fof(f6708,plain,
( $false
| ~ spl25_5
| spl25_6
| ~ spl25_7
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f6707,f6385]) ).
fof(f6709,plain,
( ~ spl25_5
| spl25_6
| ~ spl25_7
| ~ spl25_40 ),
inference(avatar_contradiction_clause,[],[f6708]) ).
fof(f6737,plain,
( aElementOf0(sK21,cS1142(xf))
| ~ spl25_11 ),
inference(forward_demodulation,[],[f311,f207]) ).
fof(f6740,plain,
( $false
| ~ spl25_11
| spl25_408 ),
inference(forward_subsumption_resolution,[],[f6100,f6670]) ).
fof(f6741,plain,
( ~ spl25_11
| spl25_408 ),
inference(avatar_contradiction_clause,[],[f6740]) ).
fof(f6743,plain,
( $false
| ~ spl25_11
| spl25_409 ),
inference(forward_subsumption_resolution,[],[f6097,f6675]) ).
fof(f6744,plain,
( ~ spl25_11
| spl25_409 ),
inference(avatar_contradiction_clause,[],[f6743]) ).
fof(f6809,plain,
( sK21 = sdtlpdtrp0(xf,sK21)
| ~ spl25_11 ),
inference(resolution,[],[f6737,f321]) ).
fof(f7059,plain,
( ~ sdtlseqdt0(sK21,sK21)
| ~ aElementOf0(sK21,xU)
| aElementOf0(sK21,xP)
| ~ sdtlseqdt0(sK19(sK21),sK21)
| ~ spl25_11 ),
inference(superposition,[],[f220,f6809]) ).
fof(f7060,plain,
( ~ sdtlseqdt0(sK21,sK21)
| ~ aElementOf0(sK21,xU)
| aElementOf0(sK21,xP)
| aElementOf0(sK19(sK21),xT)
| ~ spl25_11 ),
inference(superposition,[],[f219,f6809]) ).
fof(f7069,plain,
( ~ sdtlseqdt0(sK21,sK21)
| aElementOf0(sK21,xP)
| aElementOf0(sK19(sK21),xT)
| ~ spl25_11
| ~ spl25_408 ),
inference(forward_subsumption_resolution,[],[f7060,f6669]) ).
fof(f7070,plain,
( ~ sdtlseqdt0(sK21,sK21)
| aElementOf0(sK21,xP)
| ~ sdtlseqdt0(sK19(sK21),sK21)
| ~ spl25_11
| ~ spl25_408 ),
inference(forward_subsumption_resolution,[],[f7059,f6669]) ).
fof(f7077,definition,
( spl25_435
<=> aElementOf0(sK21,xP) ),
introduced(definition,[new_symbols(definition,[spl25_435])],[avatar_definition]) ).
fof(f7079,plain,
( aElementOf0(sK21,xP)
| ~ spl25_435 ),
inference(avatar_component_clause,[],[f7077]) ).
fof(f7081,definition,
( spl25_436
<=> sdtlseqdt0(sK21,sK21) ),
introduced(definition,[new_symbols(definition,[spl25_436])],[avatar_definition]) ).
fof(f7083,plain,
( ~ sdtlseqdt0(sK21,sK21)
| spl25_436 ),
inference(avatar_component_clause,[],[f7081]) ).
fof(f7086,definition,
( spl25_437
<=> aElementOf0(sK19(sK21),xT) ),
introduced(definition,[new_symbols(definition,[spl25_437])],[avatar_definition]) ).
fof(f7088,plain,
( aElementOf0(sK19(sK21),xT)
| ~ spl25_437 ),
inference(avatar_component_clause,[],[f7086]) ).
fof(f7089,plain,
( spl25_437
| spl25_435
| ~ spl25_436
| ~ spl25_11
| ~ spl25_408 ),
inference(avatar_split_clause,[],[f7069,f6668,f309,f7081,f7077,f7086]) ).
fof(f7091,definition,
( spl25_438
<=> sdtlseqdt0(sK19(sK21),sK21) ),
introduced(definition,[new_symbols(definition,[spl25_438])],[avatar_definition]) ).
fof(f7093,plain,
( ~ sdtlseqdt0(sK19(sK21),sK21)
| spl25_438 ),
inference(avatar_component_clause,[],[f7091]) ).
fof(f7094,plain,
( ~ spl25_438
| spl25_435
| ~ spl25_436
| ~ spl25_11
| ~ spl25_408 ),
inference(avatar_split_clause,[],[f7070,f6668,f309,f7081,f7077,f7091]) ).
fof(f7095,plain,
( ~ aElement0(sK21)
| spl25_436 ),
inference(resolution,[],[f7083,f138]) ).
fof(f7096,plain,
( $false
| ~ spl25_409
| spl25_436 ),
inference(forward_subsumption_resolution,[],[f7095,f6674]) ).
fof(f7097,plain,
( ~ spl25_409
| spl25_436 ),
inference(avatar_contradiction_clause,[],[f7096]) ).
fof(f7323,plain,
( sdtlseqdt0(sK19(sK21),sK21)
| ~ spl25_10
| ~ spl25_437 ),
inference(resolution,[],[f7088,f306]) ).
fof(f7336,plain,
( $false
| ~ spl25_10
| ~ spl25_437
| spl25_438 ),
inference(forward_subsumption_resolution,[],[f7323,f7093]) ).
fof(f7337,plain,
( ~ spl25_10
| ~ spl25_437
| spl25_438 ),
inference(avatar_contradiction_clause,[],[f7336]) ).
fof(f7342,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,xp),sK21)
| ~ spl25_435 ),
inference(resolution,[],[f7079,f237]) ).
fof(f7357,plain,
( sdtlseqdt0(sF24,sK21)
| ~ spl25_435 ),
inference(forward_demodulation,[],[f7342,f254]) ).
fof(f7364,plain,
( sdtlseqdt0(sK14(xP),sK21)
| ~ spl25_7
| ~ spl25_40
| ~ spl25_435 ),
inference(forward_demodulation,[],[f7357,f5981]) ).
fof(f7367,plain,
( $false
| ~ spl25_7
| spl25_12
| ~ spl25_40
| ~ spl25_435 ),
inference(forward_subsumption_resolution,[],[f7364,f5984]) ).
fof(f7368,plain,
( ~ spl25_7
| spl25_12
| ~ spl25_40
| ~ spl25_435 ),
inference(avatar_contradiction_clause,[],[f7367]) ).
cnf(s7,plain,
( spl25_3
| spl25_5
| ~ spl25_7
| ~ spl25_8 ),
inference(sat_conversion,[],[f297]) ).
cnf(s8,plain,
( spl25_3
| ~ spl25_6
| ~ spl25_7
| ~ spl25_8 ),
inference(sat_conversion,[],[f298]) ).
cnf(s10,plain,
( ~ spl25_3
| spl25_10 ),
inference(sat_conversion,[],[f307]) ).
cnf(s11,plain,
( ~ spl25_3
| spl25_11 ),
inference(sat_conversion,[],[f312]) ).
cnf(s12,plain,
( ~ spl25_3
| ~ spl25_12 ),
inference(sat_conversion,[],[f317]) ).
cnf(s13,plain,
spl25_8,
inference(sat_conversion,[],[f333]) ).
cnf(s18,plain,
( spl25_18
| ~ spl25_19 ),
inference(sat_conversion,[],[f397]) ).
cnf(s28,plain,
spl25_19,
inference(sat_conversion,[],[f570]) ).
cnf(s33,plain,
spl25_34,
inference(sat_conversion,[],[f731]) ).
cnf(s36,plain,
( ~ spl25_18
| ~ spl25_19
| spl25_40
| ~ spl25_41 ),
inference(sat_conversion,[],[f788]) ).
cnf(s51,plain,
( ~ spl25_19
| spl25_41 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s283,plain,
( ~ spl25_34
| ~ spl25_40
| spl25_351 ),
inference(sat_conversion,[],[f5949]) ).
cnf(s285,plain,
( spl25_7
| ~ spl25_19
| ~ spl25_34
| ~ spl25_40
| ~ spl25_351 ),
inference(sat_conversion,[],[f5977]) ).
cnf(s357,plain,
( ~ spl25_5
| spl25_6
| ~ spl25_7
| ~ spl25_40 ),
inference(sat_conversion,[],[f6709]) ).
cnf(s361,plain,
( ~ spl25_11
| spl25_408 ),
inference(sat_conversion,[],[f6741]) ).
cnf(s363,plain,
( ~ spl25_11
| spl25_409 ),
inference(sat_conversion,[],[f6744]) ).
cnf(s386,plain,
( ~ spl25_11
| ~ spl25_408
| spl25_435
| ~ spl25_436
| spl25_437 ),
inference(sat_conversion,[],[f7089]) ).
cnf(s387,plain,
( ~ spl25_11
| ~ spl25_408
| spl25_435
| ~ spl25_436
| ~ spl25_438 ),
inference(sat_conversion,[],[f7094]) ).
cnf(s388,plain,
( ~ spl25_409
| spl25_436 ),
inference(sat_conversion,[],[f7097]) ).
cnf(s407,plain,
( ~ spl25_10
| ~ spl25_437
| spl25_438 ),
inference(sat_conversion,[],[f7337]) ).
cnf(s412,plain,
( ~ spl25_7
| spl25_12
| ~ spl25_40
| ~ spl25_435 ),
inference(sat_conversion,[],[f7368]) ).
cnf(s467,plain,
spl25_41,
inference(rat,[],[s51,s28]) ).
cnf(s468,plain,
spl25_18,
inference(rat,[],[s18,s28]) ).
cnf(s469,plain,
spl25_40,
inference(rat,[],[s36,s467,s28,s468]) ).
cnf(s470,plain,
spl25_351,
inference(rat,[],[s283,s33,s469]) ).
cnf(s477,plain,
spl25_7,
inference(rat,[],[s285,s470,s28,s33,s469]) ).
cnf(s482,plain,
( spl25_3
| ~ spl25_6 ),
inference(rat,[],[s8,s13,s477]) ).
cnf(s483,plain,
( spl25_3
| spl25_5 ),
inference(rat,[],[s7,s13,s477]) ).
cnf(s486,plain,
spl25_3,
inference(rat,[],[s357,s483,s482,s477,s469]) ).
cnf(s487,plain,
~ spl25_12,
inference(rat,[],[s12,s486]) ).
cnf(s488,plain,
spl25_11,
inference(rat,[],[s11,s486]) ).
cnf(s489,plain,
spl25_10,
inference(rat,[],[s10,s486]) ).
cnf(s491,plain,
~ spl25_435,
inference(rat,[],[s412,s477,s469,s487]) ).
cnf(s492,plain,
spl25_409,
inference(rat,[],[s363,s488]) ).
cnf(s493,plain,
spl25_408,
inference(rat,[],[s361,s488]) ).
cnf(s494,plain,
spl25_436,
inference(rat,[],[s388,s492]) ).
cnf(s496,plain,
spl25_437,
inference(rat,[],[s386,s493,s488,s491,s494]) ).
cnf(s497,plain,
~ spl25_438,
inference(rat,[],[s387,s493,s488,s491,s494]) ).
cnf(s498,plain,
$false,
inference(rat,[],[s407,s489,s497,s496]) ).
fof(f7369,plain,
$false,
inference(avatar_sat_refutation,[],[s498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 15:16:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.39 Running first-order model finding
% 0.08/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.00/0.80 % (3654423)Will run a generic schedule for satisfiability detection.
% 1.00/0.80 % (3654431)dis+10_1_sil=32000:sp=arity:random_seed=440376156:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.00/0.80 % (3654428)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3881272884_2999 on theBenchmark for (2999ds/0Mi)
% 1.00/0.80 % (3654430)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4092265409:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.00/0.80 % (3654432)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3571370385:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.00/0.80 % (3654433)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1312819568:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.00/0.80 % (3654429)% WARNING: option uhcvi not known.
% 1.00/0.80 % (3654434)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1610678784:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.00/0.80 % (3654429)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3186988347:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.00/0.80 % TRYING [1]
% 1.00/0.80 % TRYING [2]
% 1.00/0.80 % TRYING [3]
% 1.00/0.80 % TRYING [4]
% 1.00/0.80 % (3654431)Instruction limit reached!
% 1.00/0.80 % (3654431)------------------------------
% 1.00/0.80 % (3654431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654431)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654431)Termination reason: Instruction limit
% 1.00/0.80 % (3654431)Termination phase: Saturation
% 1.00/0.80 % (3654431)Time elapsed: 0.042 s
% 1.00/0.80 % (3654431)Peak memory usage: 13 MB
% 1.00/0.80 % (3654431)Instructions burned: 104 (million)
% 1.00/0.80 % TRYING [5]
% 1.00/0.80 % (3654442)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2922891968:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.00/0.80 % TRYING [1]
% 1.00/0.80 % TRYING [2]
% 1.00/0.80 % TRYING [3]
% 1.00/0.80 % TRYING [6]
% 1.00/0.80 % TRYING [4]
% 1.00/0.80 % (3654432)Instruction limit reached!
% 1.00/0.80 % (3654432)------------------------------
% 1.00/0.80 % (3654432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654432)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654432)Termination reason: Instruction limit
% 1.00/0.80 % (3654432)Termination phase: Saturation
% 1.00/0.80 % (3654432)Time elapsed: 0.077 s
% 1.00/0.80 % (3654432)Peak memory usage: 13 MB
% 1.00/0.80 % (3654432)Instructions burned: 117 (million)
% 1.00/0.80 % (3654433)Instruction limit reached!
% 1.00/0.80 % (3654433)------------------------------
% 1.00/0.80 % (3654433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654433)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654433)Termination reason: Instruction limit
% 1.00/0.80 % (3654433)Termination phase: Saturation
% 1.00/0.80 % (3654433)Time elapsed: 0.087 s
% 1.00/0.80 % (3654433)Peak memory usage: 13 MB
% 1.00/0.80 % (3654433)Instructions burned: 132 (million)
% 1.00/0.80 % (3654444)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1898502046:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.00/0.80 % (3654445)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1971403546:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.00/0.80 % (3654434)Instruction limit reached!
% 1.00/0.80 % (3654434)------------------------------
% 1.00/0.80 % (3654434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654434)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654434)Termination reason: Instruction limit
% 1.00/0.80 % (3654434)Termination phase: Saturation
% 1.00/0.80 % (3654434)Time elapsed: 0.109 s
% 1.00/0.80 % (3654434)Peak memory usage: 14 MB
% 1.00/0.80 % (3654434)Instructions burned: 160 (million)
% 1.00/0.80 % TRYING [7]
% 1.00/0.80 % (3654448)ott-21_1_sil=16000:fs=off:random_seed=4208754676:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.00/0.80 % TRYING [5]
% 1.00/0.80 % (3654444)Instruction limit reached!
% 1.00/0.80 % (3654444)------------------------------
% 1.00/0.80 % (3654444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654444)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654444)Termination reason: Instruction limit
% 1.00/0.80 % (3654444)Termination phase: Saturation
% 1.00/0.80 % (3654444)Time elapsed: 0.089 s
% 1.00/0.80 % (3654444)Peak memory usage: 14 MB
% 1.00/0.80 % (3654444)Instructions burned: 132 (million)
% 1.00/0.80 % (3654450)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1829377053:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.00/0.80 % TRYING [8]
% 1.00/0.80 % (3654448)Instruction limit reached!
% 1.00/0.80 % (3654448)------------------------------
% 1.00/0.80 % (3654448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654448)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654448)Termination reason: Instruction limit
% 1.00/0.80 % (3654448)Termination phase: Saturation
% 1.00/0.80 % (3654448)Time elapsed: 0.103 s
% 1.00/0.80 % (3654448)Peak memory usage: 13 MB
% 1.00/0.80 % (3654448)Instructions burned: 182 (million)
% 1.00/0.80 % (3654452)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=605099994:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.00/0.80 % TRYING [1]
% 1.00/0.80 % TRYING [2]
% 1.00/0.80 % (3654442)Instruction limit reached!
% 1.00/0.80 % (3654442)------------------------------
% 1.00/0.80 % (3654442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.80 % (3654442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.80 % (3654442)CaDiCaL version: 2.1.3
% 1.00/0.80 % (3654442)Termination reason: Instruction limit
% 1.00/0.80 % (3654442)Termination phase: Finite model building SAT solving
% 1.00/0.80 % (3654442)Time elapsed: 0.216 s
% 1.00/0.80 % (3654442)Peak memory usage: 21 MB
% 1.00/0.80 % (3654442)Instructions burned: 715 (million)
% 1.00/0.80 % TRYING [3]
% 1.00/0.80 % (3654454)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3403771017:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 1.00/0.80 % TRYING [4]
% 1.00/0.80 % TRYING [5]
% 1.00/0.80 % (3654454) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3654423-3654454"...
% 1.00/0.80 % (3654454)...printing done.
% 1.00/0.80 % (3654454)Refutation found. Thanks to Tanya!
% 1.00/0.80 % SZS status Theorem for theBenchmark
% 1.00/0.80 % SZS output start Proof for theBenchmark
% See solution above
% 1.00/0.81 % (3654454)------------------------------
% 1.00/0.81 % (3654454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.81 % (3654454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.81 % (3654454)CaDiCaL version: 2.1.3
% 1.00/0.81 % (3654454)Termination reason: Refutation
% 1.00/0.81 % (3654454)Time elapsed: 0.080 s
% 1.00/0.81 % (3654454)Peak memory usage: 16 MB
% 1.00/0.81 % (3654454)Instructions burned: 226 (million)
% 1.00/0.81 % (3654423)Success in time 0.399 s
% 1.00/0.81 % Vampire exiting
%------------------------------------------------------------------------------