%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM616+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:16:00 PM UTC 2026
% Result : Theorem 13.50s 2.86s
% Output : Refutation 14.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 50
% Syntax : Number of formulae : 316 ( 59 unt; 25 def)
% Number of atoms : 1001 ( 129 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1188 ( 503 ~; 515 |; 115 &)
% ( 37 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 22 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 13 con; 0-3 aty)
% Number of variables : 226 ( 0 sgn 211 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f5,axiom,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ~ ? [X1] : aElementOf0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefEmp) ).
fof(f6,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEmpFin) ).
fof(f8,axiom,
! [X0] :
( ( aSet0(X0)
& isCountable0(X0) )
=> ~ isFinite0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin) ).
fof(f9,axiom,
! [X0] :
( ( aSet0(X0)
& isCountable0(X0) )
=> X0 != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin_01) ).
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(f16,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElement0(X1) )
=> ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
fof(f23,axiom,
( aSet0(szNzAzT0)
& isCountable0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f37,axiom,
! [X0,X1] :
( ( aElementOf0(X0,szNzAzT0)
& aElementOf0(X1,szNzAzT0) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(szszuzczcdt0(X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTotal) ).
fof(f47,axiom,
! [X0] :
( ( aSubsetOf0(X0,szNzAzT0)
& X0 != slcrc0 )
=> ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( aElementOf0(X2,X0)
=> sdtlseqdt0(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefMin) ).
fof(f49,axiom,
! [X0,X1] :
( ( aSubsetOf0(X0,szNzAzT0)
& aSubsetOf0(X1,szNzAzT0)
& X0 != slcrc0
& X1 != slcrc0 )
=> ( ( aElementOf0(szmzizndt0(X0),X1)
& aElementOf0(szmzizndt0(X1),X0) )
=> szmzizndt0(X0) = szmzizndt0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMinMin) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3671) ).
fof(f83,axiom,
! [X0,X1] :
( ( aElementOf0(X0,szNzAzT0)
& aElementOf0(X1,szNzAzT0) )
=> ( sdtlseqdt0(X1,X0)
=> aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3754) ).
fof(f91,axiom,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4660) ).
fof(f96,axiom,
( aSet0(xO)
& isCountable0(xO) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4908) ).
fof(f97,axiom,
! [X0] :
( aElementOf0(X0,xO)
=> ? [X1] :
( aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X1) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4982) ).
fof(f100,axiom,
( aSubsetOf0(xQ,xO)
& xQ != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5093) ).
fof(f101,axiom,
aSubsetOf0(xQ,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5106) ).
fof(f103,axiom,
xp = szmzizndt0(xQ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5147) ).
fof(f104,axiom,
( aSet0(xP)
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5164) ).
fof(f107,axiom,
aSubsetOf0(xP,xQ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5195) ).
fof(f108,axiom,
aSubsetOf0(xP,xO),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5208) ).
fof(f111,axiom,
( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(xn,szNzAzT0)
& sdtlpdtrp0(xe,xn) = xp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5309) ).
fof(f113,conjecture,
aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f114,negated_conjecture,
~ aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(negated_conjecture,[status(cth)],[f113]) ).
fof(f122,plain,
~ aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(flattening,[],[f114]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f124,plain,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f125,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f126,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0] :
( X0 != slcrc0
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f128,plain,
! [X0] :
( X0 != slcrc0
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0] :
( ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) ) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f139,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f140,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f139]) ).
fof(f152,plain,
! [X0] :
( ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f168,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f169,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f168]) ).
fof(f182,plain,
! [X0] :
( ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(ennf_transformation,[],[f47]) ).
fof(f183,plain,
! [X0] :
( ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(flattening,[],[f182]) ).
fof(f186,plain,
! [X0,X1] :
( szmzizndt0(X0) = szmzizndt0(X1)
| ~ aElementOf0(szmzizndt0(X0),X1)
| ~ aElementOf0(szmzizndt0(X1),X0)
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,szNzAzT0)
| slcrc0 = X0
| slcrc0 = X1 ),
inference(ennf_transformation,[],[f49]) ).
fof(f187,plain,
! [X0,X1] :
( szmzizndt0(X0) = szmzizndt0(X1)
| ~ aElementOf0(szmzizndt0(X0),X1)
| ~ aElementOf0(szmzizndt0(X1),X0)
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,szNzAzT0)
| slcrc0 = X0
| slcrc0 = X1 ),
inference(flattening,[],[f186]) ).
fof(f226,plain,
! [X0] :
( ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f227,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f228,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f227]) ).
fof(f242,plain,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f245,plain,
! [X0] :
( ? [X1] :
( aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X1) = X0 )
| ~ aElementOf0(X0,xO) ),
inference(ennf_transformation,[],[f97]) ).
fof(f249,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f250,definition,
! [X1,X0] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> sP2(X2,X0,X1) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f251,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f140,f250,f249]) ).
fof(f252,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(nnf_transformation,[],[f124]) ).
fof(f253,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(flattening,[],[f252]) ).
fof(f254,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(rectify,[],[f253]) ).
fof(f255,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| aElementOf0(sK4(X0),X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f254]) ).
fof(f256,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(nnf_transformation,[],[f129]) ).
fof(f257,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(flattening,[],[f256]) ).
fof(f258,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X3] :
( aElementOf0(X3,X0)
| ~ aElementOf0(X3,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(rectify,[],[f257]) ).
fof(f259,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ( ~ aElementOf0(sK5(X0,X1),X0)
& aElementOf0(sK5(X0,X1),X1) ) )
& ( ( aSet0(X1)
& ! [X3] :
( aElementOf0(X3,X0)
| ~ aElementOf0(X3,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f258]) ).
fof(f266,plain,
! [X1,X0] :
( ! [X2] :
( ( X2 = sdtmndt0(X0,X1)
| ~ sP2(X2,X0,X1) )
& ( sP2(X2,X0,X1)
| sdtmndt0(X0,X1) != X2 ) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f250]) ).
fof(f267,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtmndt0(X1,X0) = X2
| ~ sP2(X2,X1,X0) )
& ( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2 ) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f266]) ).
fof(f268,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f249]) ).
fof(f269,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(flattening,[],[f268]) ).
fof(f270,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X1)
| X2 = X3
| ~ aElementOf0(X3,X0) )
& ( ( aElement0(X3)
& aElementOf0(X3,X1)
& X2 != X3 )
| aElementOf0(X3,X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(rectify,[],[f269]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ( ( ~ aElement0(sK7(X0,X1,X2))
| ~ aElementOf0(sK7(X0,X1,X2),X1)
| sK7(X0,X1,X2) = X2
| ~ aElementOf0(sK7(X0,X1,X2),X0) )
& ( ( aElement0(sK7(X0,X1,X2))
& aElementOf0(sK7(X0,X1,X2),X1)
& sK7(X0,X1,X2) != X2 )
| aElementOf0(sK7(X0,X1,X2),X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f270]) ).
fof(f277,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(nnf_transformation,[],[f183]) ).
fof(f278,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(flattening,[],[f277]) ).
fof(f279,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X3] :
( sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(rectify,[],[f278]) ).
fof(f280,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ( ~ sdtlseqdt0(X1,sK10(X0,X1))
& aElementOf0(sK10(X0,X1),X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X3] :
( sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f279]) ).
fof(f314,plain,
! [X0] :
( ( aElementOf0(sK28(X0),szNzAzT0)
& aElementOf0(sK28(X0),sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,sK28(X0)) = X0 )
| ~ aElementOf0(X0,xO) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X1,sK28(X0))],[f245]) ).
fof(f315,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f317,plain,
! [X0] :
( aSet0(X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f255]) ).
fof(f319,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[],[f6]) ).
fof(f320,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f321,plain,
! [X0] :
( slcrc0 != X0
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f322,plain,
! [X3,X0,X1] :
( ~ aSubsetOf0(X1,X0)
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f323,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f324,plain,
! [X0,X1] :
( aElementOf0(sK5(X0,X1),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f325,plain,
! [X0,X1] :
( ~ aElementOf0(sK5(X0,X1),X0)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f342,plain,
! [X2,X0,X1] :
( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f267]) ).
fof(f344,plain,
! [X2,X0,X1,X4] :
( X2 != X4
| ~ aElementOf0(X4,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f271]) ).
fof(f353,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f251]) ).
fof(f361,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f364,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f377,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f390,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| szmzizndt0(X0) != X1
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(cnf_transformation,[],[f280]) ).
fof(f397,plain,
! [X0,X1] :
( ~ aElementOf0(szmzizndt0(X1),X0)
| ~ aElementOf0(szmzizndt0(X0),X1)
| szmzizndt0(X0) = szmzizndt0(X1)
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,szNzAzT0)
| slcrc0 = X0
| slcrc0 = X1 ),
inference(cnf_transformation,[],[f187]) ).
fof(f479,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f480,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f481,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f497,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = sdtlpdtrp0(xe,X0) ),
inference(cnf_transformation,[],[f242]) ).
fof(f509,plain,
aSet0(xO),
inference(cnf_transformation,[],[f96]) ).
fof(f510,plain,
! [X0] :
( ~ aElementOf0(X0,xO)
| sdtlpdtrp0(xe,sK28(X0)) = X0 ),
inference(cnf_transformation,[],[f314]) ).
fof(f512,plain,
! [X0] :
( aElementOf0(sK28(X0),szNzAzT0)
| ~ aElementOf0(X0,xO) ),
inference(cnf_transformation,[],[f314]) ).
fof(f515,plain,
slcrc0 != xQ,
inference(cnf_transformation,[],[f100]) ).
fof(f517,plain,
aSubsetOf0(xQ,szNzAzT0),
inference(cnf_transformation,[],[f101]) ).
fof(f519,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[],[f103]) ).
fof(f520,plain,
xP = sdtmndt0(xQ,szmzizndt0(xQ)),
inference(cnf_transformation,[],[f104]) ).
fof(f521,plain,
aSet0(xP),
inference(cnf_transformation,[],[f104]) ).
fof(f524,plain,
aSubsetOf0(xP,xQ),
inference(cnf_transformation,[],[f107]) ).
fof(f525,plain,
aSubsetOf0(xP,xO),
inference(cnf_transformation,[],[f108]) ).
fof(f528,plain,
xp = sdtlpdtrp0(xe,xn),
inference(cnf_transformation,[],[f111]) ).
fof(f529,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f111]) ).
fof(f532,plain,
~ aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(cnf_transformation,[],[f122]) ).
fof(f533,plain,
aSet0(slcrc0),
inference(equality_resolution,[],[f317]) ).
fof(f535,plain,
( ~ aSet0(slcrc0)
| ~ isCountable0(slcrc0) ),
inference(equality_resolution,[],[f321]) ).
fof(f538,plain,
! [X0,X1] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(equality_resolution,[],[f342]) ).
fof(f539,plain,
! [X0,X1,X4] :
( ~ sP2(X0,X1,X4)
| ~ aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f344]) ).
fof(f541,plain,
! [X0] :
( aElementOf0(szmzizndt0(X0),X0)
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(equality_resolution,[],[f390]) ).
fof(f570,definition,
sF29 = szszuzczcdt0(xn),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f571,plain,
szszuzczcdt0(xn) = sF29,
inference(reorient_equations,[],[f570]) ).
fof(f572,definition,
sF30 = sdtlpdtrp0(xN,sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f573,plain,
sdtlpdtrp0(xN,sF29) = sF30,
inference(reorient_equations,[],[f572]) ).
fof(f574,plain,
~ aSubsetOf0(xP,sF30),
inference(definition_folding,[],[f532,f573,f571]) ).
fof(f579,definition,
( spl31_1
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[spl31_1])],[avatar_definition]) ).
fof(f588,definition,
( spl31_3
<=> isCountable0(slcrc0) ),
introduced(definition,[new_symbols(definition,[spl31_3])],[avatar_definition]) ).
fof(f590,plain,
( ~ isCountable0(slcrc0)
| spl31_3 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( ~ spl31_3
| ~ spl31_1 ),
inference(avatar_split_clause,[],[f535,f579,f588]) ).
fof(f592,plain,
spl31_1,
inference(avatar_split_clause,[],[f533,f579]) ).
fof(f596,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sF30)
| ~ sdtlseqdt0(sF29,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sF29,szNzAzT0) ),
inference(superposition,[],[f481,f573]) ).
fof(f598,definition,
( spl31_4
<=> aElementOf0(sF29,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl31_4])],[avatar_definition]) ).
fof(f599,plain,
( aElementOf0(sF29,szNzAzT0)
| ~ spl31_4 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( ~ aElementOf0(sF29,szNzAzT0)
| spl31_4 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f602,definition,
( spl31_5
<=> ! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sF30)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(sF29,X0) ) ),
introduced(definition,[new_symbols(definition,[spl31_5])],[avatar_definition]) ).
fof(f603,plain,
( ! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sF30)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(sF29,X0) )
| ~ spl31_5 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f604,plain,
( ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f596,f602,f598]) ).
fof(f612,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(sdtlpdtrp0(xN,X0))
| ~ aSet0(szNzAzT0) ),
inference(resolution,[],[f480,f323]) ).
fof(f614,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f612,f361]) ).
fof(f615,plain,
! [X2,X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,X1))
| aElementOf0(X0,sdtlpdtrp0(xN,X2))
| ~ aSet0(sdtlpdtrp0(xN,X2))
| ~ sdtlseqdt0(X2,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(resolution,[],[f322,f481]) ).
fof(f617,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xQ)
| ~ aSet0(xQ) ),
inference(resolution,[],[f322,f524]) ).
fof(f618,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xO)
| ~ aSet0(xO) ),
inference(resolution,[],[f322,f525]) ).
fof(f619,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xO) ),
inference(forward_subsumption_resolution,[],[f618,f509]) ).
fof(f621,definition,
( spl31_7
<=> aSet0(xQ) ),
introduced(definition,[new_symbols(definition,[spl31_7])],[avatar_definition]) ).
fof(f622,plain,
( aSet0(xQ)
| ~ spl31_7 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( ~ aSet0(xQ)
| spl31_7 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl31_8
<=> ! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xQ) ) ),
introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition]) ).
fof(f626,plain,
( ! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,xQ) )
| ~ spl31_8 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f627,plain,
( ~ spl31_7
| spl31_8 ),
inference(avatar_split_clause,[],[f617,f625,f621]) ).
fof(f629,plain,
! [X2,X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,X1))
| aElementOf0(X0,sdtlpdtrp0(xN,X2))
| ~ sdtlseqdt0(X2,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f615,f614]) ).
fof(f633,plain,
! [X0] :
( aElementOf0(sK5(X0,xP),xO)
| ~ aSet0(xP)
| aSubsetOf0(xP,X0)
| ~ aSet0(X0) ),
inference(resolution,[],[f619,f324]) ).
fof(f634,plain,
! [X0] :
( aElementOf0(sK5(X0,xP),xO)
| aSubsetOf0(xP,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[],[f633,f521]) ).
fof(f635,plain,
! [X0] :
( ~ aElementOf0(X0,xQ)
| aElementOf0(X0,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[],[f517,f322]) ).
fof(f636,plain,
( aSet0(xQ)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[],[f517,f323]) ).
fof(f637,plain,
( ~ aSet0(szNzAzT0)
| spl31_7 ),
inference(forward_subsumption_resolution,[],[f636,f623]) ).
fof(f638,plain,
! [X0] :
( ~ aElementOf0(X0,xQ)
| aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f635,f361]) ).
fof(f639,plain,
( $false
| spl31_7 ),
inference(forward_subsumption_resolution,[],[f637,f361]) ).
fof(f640,plain,
spl31_7,
inference(avatar_contradiction_clause,[],[f639]) ).
fof(f641,plain,
( ! [X0] :
( aElementOf0(sK5(X0,xP),xQ)
| ~ aSet0(xP)
| aSubsetOf0(xP,X0)
| ~ aSet0(X0) )
| ~ spl31_8 ),
inference(resolution,[],[f626,f324]) ).
fof(f642,plain,
( ! [X0] :
( aElementOf0(sK5(X0,xP),xQ)
| aSubsetOf0(xP,X0)
| ~ aSet0(X0) )
| ~ spl31_8 ),
inference(forward_subsumption_resolution,[],[f641,f521]) ).
fof(f643,plain,
( aSet0(sF30)
| ~ aElementOf0(sF29,szNzAzT0) ),
inference(superposition,[],[f614,f573]) ).
fof(f662,plain,
sdtlpdtrp0(xe,xn) = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(resolution,[],[f497,f529]) ).
fof(f667,plain,
xp = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(forward_demodulation,[],[f662,f528]) ).
fof(f714,plain,
! [X0] :
( aSubsetOf0(xP,X0)
| sK5(X0,xP) = sdtlpdtrp0(xe,sK28(sK5(X0,xP)))
| ~ aSet0(X0) ),
inference(resolution,[],[f510,f634]) ).
fof(f717,plain,
( sK5(sF30,xP) = sdtlpdtrp0(xe,sK28(sK5(sF30,xP)))
| ~ aSet0(sF30) ),
inference(resolution,[],[f714,f574]) ).
fof(f726,definition,
( spl31_9
<=> aSet0(sF30) ),
introduced(definition,[new_symbols(definition,[spl31_9])],[avatar_definition]) ).
fof(f727,plain,
( aSet0(sF30)
| ~ spl31_9 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f728,plain,
( ~ aSet0(sF30)
| spl31_9 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f730,definition,
( spl31_10
<=> sK5(sF30,xP) = sdtlpdtrp0(xe,sK28(sK5(sF30,xP))) ),
introduced(definition,[new_symbols(definition,[spl31_10])],[avatar_definition]) ).
fof(f732,plain,
( sK5(sF30,xP) = sdtlpdtrp0(xe,sK28(sK5(sF30,xP)))
| ~ spl31_10 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f733,plain,
( ~ spl31_9
| spl31_10 ),
inference(avatar_split_clause,[],[f717,f730,f726]) ).
fof(f751,definition,
( spl31_12
<=> sP3(xp,xQ) ),
introduced(definition,[new_symbols(definition,[spl31_12])],[avatar_definition]) ).
fof(f752,plain,
( sP3(xp,xQ)
| ~ spl31_12 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f753,plain,
( ~ sP3(xp,xQ)
| spl31_12 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f759,plain,
( ~ aSubsetOf0(xQ,szNzAzT0)
| slcrc0 = xQ
| aElementOf0(szmzizndt0(xQ),szNzAzT0) ),
inference(resolution,[],[f541,f638]) ).
fof(f762,plain,
( aElementOf0(xp,sdtlpdtrp0(xN,xn))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| slcrc0 = sdtlpdtrp0(xN,xn) ),
inference(superposition,[],[f541,f667]) ).
fof(f764,definition,
( spl31_13
<=> slcrc0 = sdtlpdtrp0(xN,xn) ),
introduced(definition,[new_symbols(definition,[spl31_13])],[avatar_definition]) ).
fof(f766,plain,
( slcrc0 = sdtlpdtrp0(xN,xn)
| ~ spl31_13 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f768,definition,
( spl31_14
<=> aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl31_14])],[avatar_definition]) ).
fof(f770,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| spl31_14 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f772,definition,
( spl31_15
<=> aElementOf0(xp,sdtlpdtrp0(xN,xn)) ),
introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition]) ).
fof(f774,plain,
( aElementOf0(xp,sdtlpdtrp0(xN,xn))
| ~ spl31_15 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f775,plain,
( spl31_13
| ~ spl31_14
| spl31_15 ),
inference(avatar_split_clause,[],[f762,f772,f768,f764]) ).
fof(f778,plain,
( slcrc0 = xQ
| aElementOf0(szmzizndt0(xQ),szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f759,f517]) ).
fof(f819,plain,
aElementOf0(szmzizndt0(xQ),szNzAzT0),
inference(forward_subsumption_resolution,[],[f778,f515]) ).
fof(f820,plain,
aElementOf0(xp,szNzAzT0),
inference(forward_demodulation,[],[f819,f519]) ).
fof(f821,plain,
( ~ aElementOf0(xn,szNzAzT0)
| spl31_14 ),
inference(resolution,[],[f770,f480]) ).
fof(f822,plain,
( $false
| spl31_14 ),
inference(forward_subsumption_resolution,[],[f821,f529]) ).
fof(f823,plain,
spl31_14,
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f826,plain,
( isCountable0(slcrc0)
| ~ aElementOf0(xn,szNzAzT0)
| ~ spl31_13 ),
inference(superposition,[],[f479,f766]) ).
fof(f833,plain,
( ~ aElementOf0(xn,szNzAzT0)
| spl31_3
| ~ spl31_13 ),
inference(forward_subsumption_resolution,[],[f826,f590]) ).
fof(f834,plain,
( $false
| spl31_3
| ~ spl31_13 ),
inference(forward_subsumption_resolution,[],[f833,f529]) ).
fof(f835,plain,
( spl31_3
| ~ spl31_13 ),
inference(avatar_contradiction_clause,[],[f834]) ).
fof(f879,plain,
( aElementOf0(sF29,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(superposition,[],[f364,f571]) ).
fof(f880,plain,
( ~ aElementOf0(xn,szNzAzT0)
| spl31_4 ),
inference(forward_subsumption_resolution,[],[f879,f600]) ).
fof(f881,plain,
( $false
| spl31_4 ),
inference(forward_subsumption_resolution,[],[f880,f529]) ).
fof(f882,plain,
spl31_4,
inference(avatar_contradiction_clause,[],[f881]) ).
fof(f884,plain,
( ~ aElementOf0(sF29,szNzAzT0)
| spl31_9 ),
inference(forward_subsumption_resolution,[],[f643,f728]) ).
fof(f886,plain,
( $false
| ~ spl31_4
| spl31_9 ),
inference(forward_subsumption_resolution,[],[f884,f599]) ).
fof(f887,plain,
( ~ spl31_4
| spl31_9 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f897,plain,
( ! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(sF29,X0)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,sF30)
| ~ aSet0(sF30) )
| ~ spl31_5 ),
inference(resolution,[],[f603,f322]) ).
fof(f903,plain,
( ! [X0,X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(sF29,X0)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X1,sF30) )
| ~ spl31_5
| ~ spl31_9 ),
inference(forward_subsumption_resolution,[],[f897,f727]) ).
fof(f1052,plain,
( aElement0(xp)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[],[f315,f820]) ).
fof(f1073,plain,
aElement0(xp),
inference(forward_subsumption_resolution,[],[f1052,f361]) ).
fof(f1122,plain,
( ~ aSet0(xQ)
| ~ aElement0(xp)
| spl31_12 ),
inference(resolution,[],[f353,f753]) ).
fof(f1123,plain,
( ~ aElement0(xp)
| ~ spl31_7
| spl31_12 ),
inference(forward_subsumption_resolution,[],[f1122,f622]) ).
fof(f1124,plain,
( $false
| ~ spl31_7
| spl31_12 ),
inference(forward_subsumption_resolution,[],[f1123,f1073]) ).
fof(f1125,plain,
( ~ spl31_7
| spl31_12 ),
inference(avatar_contradiction_clause,[],[f1124]) ).
fof(f1419,plain,
( ! [X0] :
( aElementOf0(xp,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xn)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) )
| ~ spl31_15 ),
inference(resolution,[],[f629,f774]) ).
fof(f1426,plain,
( ! [X0] :
( aElementOf0(xp,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xn)
| ~ aElementOf0(X0,szNzAzT0) )
| ~ spl31_15 ),
inference(forward_subsumption_resolution,[],[f1419,f529]) ).
fof(f1436,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f539,f538]) ).
fof(f1437,plain,
( ~ aElementOf0(szmzizndt0(xQ),xP)
| ~ sP3(szmzizndt0(xQ),xQ) ),
inference(superposition,[],[f1436,f520]) ).
fof(f1519,plain,
! [X0] :
( sdtlseqdt0(sF29,X0)
| sdtlseqdt0(X0,xn)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(superposition,[],[f377,f571]) ).
fof(f1522,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(X0,xn)
| sdtlseqdt0(sF29,X0) ),
inference(forward_subsumption_resolution,[],[f1519,f529]) ).
fof(f1589,plain,
! [X0] :
( ~ aElementOf0(xp,X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| szmzizndt0(X0) = xp
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(xQ,szNzAzT0)
| slcrc0 = X0
| slcrc0 = xQ ),
inference(superposition,[],[f397,f519]) ).
fof(f1592,plain,
! [X0] :
( ~ aElementOf0(xp,X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| szmzizndt0(X0) = xp
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0
| slcrc0 = xQ ),
inference(forward_subsumption_resolution,[],[f1589,f517]) ).
fof(f1595,plain,
! [X0] :
( ~ aElementOf0(szmzizndt0(X0),xQ)
| ~ aElementOf0(xp,X0)
| szmzizndt0(X0) = xp
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(forward_subsumption_resolution,[],[f1592,f515]) ).
fof(f1957,plain,
( ~ aElementOf0(xp,xP)
| ~ sP3(szmzizndt0(xQ),xQ) ),
inference(forward_demodulation,[],[f1437,f519]) ).
fof(f1987,plain,
( ~ sP3(xp,xQ)
| ~ aElementOf0(xp,xP) ),
inference(forward_demodulation,[],[f1957,f519]) ).
fof(f1990,plain,
( ~ aElementOf0(xp,xP)
| ~ spl31_12 ),
inference(forward_subsumption_resolution,[],[f1987,f752]) ).
fof(f3569,plain,
! [X0] :
( ~ aSet0(sdtlpdtrp0(xN,X0))
| ~ isFinite0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f320,f479]) ).
fof(f3576,plain,
! [X0] :
( ~ isFinite0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f3569,f614]) ).
fof(f13511,definition,
( spl31_753
<=> aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl31_753])],[avatar_definition]) ).
fof(f13512,plain,
( aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| ~ spl31_753 ),
inference(avatar_component_clause,[],[f13511]) ).
fof(f13513,plain,
( ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| spl31_753 ),
inference(avatar_component_clause,[],[f13511]) ).
fof(f13641,plain,
( ~ aElementOf0(sK5(sF30,xP),xO)
| spl31_753 ),
inference(resolution,[],[f13513,f512]) ).
fof(f13674,plain,
( aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| spl31_753 ),
inference(resolution,[],[f13641,f634]) ).
fof(f13677,plain,
( ~ aSet0(sF30)
| spl31_753 ),
inference(forward_subsumption_resolution,[],[f13674,f574]) ).
fof(f13679,plain,
( $false
| ~ spl31_9
| spl31_753 ),
inference(forward_subsumption_resolution,[],[f13677,f727]) ).
fof(f13680,plain,
( ~ spl31_9
| spl31_753 ),
inference(avatar_contradiction_clause,[],[f13679]) ).
fof(f13684,plain,
( sdtlseqdt0(sK28(sK5(sF30,xP)),xn)
| sdtlseqdt0(sF29,sK28(sK5(sF30,xP)))
| ~ spl31_753 ),
inference(resolution,[],[f13512,f1522]) ).
fof(f13685,plain,
( sdtlpdtrp0(xe,sK28(sK5(sF30,xP))) = szmzizndt0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| ~ spl31_753 ),
inference(resolution,[],[f13512,f497]) ).
fof(f13691,plain,
( sK5(sF30,xP) = szmzizndt0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| ~ spl31_10
| ~ spl31_753 ),
inference(forward_demodulation,[],[f13685,f732]) ).
fof(f13703,definition,
( spl31_764
<=> sdtlseqdt0(sF29,sK28(sK5(sF30,xP))) ),
introduced(definition,[new_symbols(definition,[spl31_764])],[avatar_definition]) ).
fof(f13704,plain,
( ~ sdtlseqdt0(sF29,sK28(sK5(sF30,xP)))
| spl31_764 ),
inference(avatar_component_clause,[],[f13703]) ).
fof(f13705,plain,
( sdtlseqdt0(sF29,sK28(sK5(sF30,xP)))
| ~ spl31_764 ),
inference(avatar_component_clause,[],[f13703]) ).
fof(f13746,plain,
( aElementOf0(sK5(sF30,xP),sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| ~ aSubsetOf0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))),szNzAzT0)
| slcrc0 = sdtlpdtrp0(xN,sK28(sK5(sF30,xP)))
| ~ spl31_10
| ~ spl31_753 ),
inference(superposition,[],[f541,f13691]) ).
fof(f13747,plain,
( ~ aElementOf0(sK5(sF30,xP),xQ)
| ~ aElementOf0(xp,sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| xp = sK5(sF30,xP)
| ~ aSubsetOf0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))),szNzAzT0)
| slcrc0 = sdtlpdtrp0(xN,sK28(sK5(sF30,xP)))
| ~ spl31_10
| ~ spl31_753 ),
inference(superposition,[],[f1595,f13691]) ).
fof(f13755,definition,
( spl31_768
<=> xp = sK5(sF30,xP) ),
introduced(definition,[new_symbols(definition,[spl31_768])],[avatar_definition]) ).
fof(f13757,plain,
( xp = sK5(sF30,xP)
| ~ spl31_768 ),
inference(avatar_component_clause,[],[f13755]) ).
fof(f13759,definition,
( spl31_769
<=> aSubsetOf0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl31_769])],[avatar_definition]) ).
fof(f13761,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,sK28(sK5(sF30,xP))),szNzAzT0)
| spl31_769 ),
inference(avatar_component_clause,[],[f13759]) ).
fof(f13763,definition,
( spl31_770
<=> slcrc0 = sdtlpdtrp0(xN,sK28(sK5(sF30,xP))) ),
introduced(definition,[new_symbols(definition,[spl31_770])],[avatar_definition]) ).
fof(f13765,plain,
( slcrc0 = sdtlpdtrp0(xN,sK28(sK5(sF30,xP)))
| ~ spl31_770 ),
inference(avatar_component_clause,[],[f13763]) ).
fof(f13767,definition,
( spl31_771
<=> aElementOf0(xp,sdtlpdtrp0(xN,sK28(sK5(sF30,xP)))) ),
introduced(definition,[new_symbols(definition,[spl31_771])],[avatar_definition]) ).
fof(f13769,plain,
( ~ aElementOf0(xp,sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| spl31_771 ),
inference(avatar_component_clause,[],[f13767]) ).
fof(f13771,definition,
( spl31_772
<=> aElementOf0(sK5(sF30,xP),sF30) ),
introduced(definition,[new_symbols(definition,[spl31_772])],[avatar_definition]) ).
fof(f13772,plain,
( aElementOf0(sK5(sF30,xP),sF30)
| ~ spl31_772 ),
inference(avatar_component_clause,[],[f13771]) ).
fof(f13777,definition,
( spl31_773
<=> aElementOf0(sK5(sF30,xP),xQ) ),
introduced(definition,[new_symbols(definition,[spl31_773])],[avatar_definition]) ).
fof(f13779,plain,
( ~ aElementOf0(sK5(sF30,xP),xQ)
| spl31_773 ),
inference(avatar_component_clause,[],[f13777]) ).
fof(f13780,plain,
( spl31_770
| ~ spl31_769
| spl31_768
| ~ spl31_771
| ~ spl31_773
| ~ spl31_10
| ~ spl31_753 ),
inference(avatar_split_clause,[],[f13747,f13511,f730,f13777,f13767,f13755,f13759,f13763]) ).
fof(f13782,definition,
( spl31_774
<=> aElementOf0(sK5(sF30,xP),sdtlpdtrp0(xN,sK28(sK5(sF30,xP)))) ),
introduced(definition,[new_symbols(definition,[spl31_774])],[avatar_definition]) ).
fof(f13784,plain,
( aElementOf0(sK5(sF30,xP),sdtlpdtrp0(xN,sK28(sK5(sF30,xP))))
| ~ spl31_774 ),
inference(avatar_component_clause,[],[f13782]) ).
fof(f13785,plain,
( spl31_770
| ~ spl31_769
| spl31_774
| ~ spl31_10
| ~ spl31_753 ),
inference(avatar_split_clause,[],[f13746,f13511,f730,f13782,f13759,f13763]) ).
fof(f13924,plain,
( ~ isFinite0(slcrc0)
| ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| ~ spl31_770 ),
inference(superposition,[],[f3576,f13765]) ).
fof(f13937,plain,
( ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| ~ spl31_770 ),
inference(forward_subsumption_resolution,[],[f13924,f319]) ).
fof(f13962,plain,
( $false
| ~ spl31_753
| ~ spl31_770 ),
inference(forward_subsumption_resolution,[],[f13937,f13512]) ).
fof(f13963,plain,
( ~ spl31_753
| ~ spl31_770 ),
inference(avatar_contradiction_clause,[],[f13962]) ).
fof(f14052,plain,
( ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| spl31_769 ),
inference(resolution,[],[f13761,f480]) ).
fof(f14055,plain,
( $false
| ~ spl31_753
| spl31_769 ),
inference(forward_subsumption_resolution,[],[f14052,f13512]) ).
fof(f14056,plain,
( ~ spl31_753
| spl31_769 ),
inference(avatar_contradiction_clause,[],[f14055]) ).
fof(f14068,plain,
( ~ sdtlseqdt0(sF29,sK28(sK5(sF30,xP)))
| ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| aElementOf0(sK5(sF30,xP),sF30)
| ~ spl31_5
| ~ spl31_9
| ~ spl31_774 ),
inference(resolution,[],[f13784,f903]) ).
fof(f14086,plain,
( ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| aElementOf0(sK5(sF30,xP),sF30)
| ~ spl31_5
| ~ spl31_9
| ~ spl31_764
| ~ spl31_774 ),
inference(forward_subsumption_resolution,[],[f14068,f13705]) ).
fof(f14087,plain,
( aElementOf0(sK5(sF30,xP),sF30)
| ~ spl31_5
| ~ spl31_9
| ~ spl31_753
| ~ spl31_764
| ~ spl31_774 ),
inference(forward_subsumption_resolution,[],[f14086,f13512]) ).
fof(f14088,plain,
( spl31_772
| ~ spl31_5
| ~ spl31_9
| ~ spl31_753
| ~ spl31_764
| ~ spl31_774 ),
inference(avatar_split_clause,[],[f14087,f13782,f13703,f13511,f726,f602,f13771]) ).
fof(f14112,plain,
( ~ sdtlseqdt0(sK28(sK5(sF30,xP)),xn)
| ~ aElementOf0(sK28(sK5(sF30,xP)),szNzAzT0)
| ~ spl31_15
| spl31_771 ),
inference(resolution,[],[f13769,f1426]) ).
fof(f14114,plain,
( ~ sdtlseqdt0(sK28(sK5(sF30,xP)),xn)
| ~ spl31_15
| ~ spl31_753
| spl31_771 ),
inference(forward_subsumption_resolution,[],[f14112,f13512]) ).
fof(f14128,plain,
( aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_8
| spl31_773 ),
inference(resolution,[],[f13779,f642]) ).
fof(f14130,plain,
( ~ aSet0(sF30)
| ~ spl31_8
| spl31_773 ),
inference(forward_subsumption_resolution,[],[f14128,f574]) ).
fof(f14131,plain,
( $false
| ~ spl31_8
| ~ spl31_9
| spl31_773 ),
inference(forward_subsumption_resolution,[],[f14130,f727]) ).
fof(f14132,plain,
( ~ spl31_8
| ~ spl31_9
| spl31_773 ),
inference(avatar_contradiction_clause,[],[f14131]) ).
fof(f14220,plain,
( aElementOf0(xp,xP)
| ~ aSet0(xP)
| aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_768 ),
inference(superposition,[],[f324,f13757]) ).
fof(f14221,plain,
( ~ aSet0(xP)
| aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_12
| ~ spl31_768 ),
inference(forward_subsumption_resolution,[],[f14220,f1990]) ).
fof(f14228,plain,
( aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_12
| ~ spl31_768 ),
inference(forward_subsumption_resolution,[],[f14221,f521]) ).
fof(f14230,plain,
( ~ aSet0(sF30)
| ~ spl31_12
| ~ spl31_768 ),
inference(forward_subsumption_resolution,[],[f14228,f574]) ).
fof(f14231,plain,
( $false
| ~ spl31_9
| ~ spl31_12
| ~ spl31_768 ),
inference(forward_subsumption_resolution,[],[f14230,f727]) ).
fof(f14232,plain,
( ~ spl31_9
| ~ spl31_12
| ~ spl31_768 ),
inference(avatar_contradiction_clause,[],[f14231]) ).
fof(f14251,plain,
( ~ aSet0(xP)
| aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_772 ),
inference(resolution,[],[f13772,f325]) ).
fof(f14262,plain,
( aSubsetOf0(xP,sF30)
| ~ aSet0(sF30)
| ~ spl31_772 ),
inference(forward_subsumption_resolution,[],[f14251,f521]) ).
fof(f14263,plain,
( ~ aSet0(sF30)
| ~ spl31_772 ),
inference(forward_subsumption_resolution,[],[f14262,f574]) ).
fof(f14264,plain,
( $false
| ~ spl31_9
| ~ spl31_772 ),
inference(forward_subsumption_resolution,[],[f14263,f727]) ).
fof(f14265,plain,
( ~ spl31_9
| ~ spl31_772 ),
inference(avatar_contradiction_clause,[],[f14264]) ).
fof(f14306,plain,
( sdtlseqdt0(sK28(sK5(sF30,xP)),xn)
| ~ spl31_753
| spl31_764 ),
inference(forward_subsumption_resolution,[],[f13684,f13704]) ).
fof(f14311,plain,
( $false
| ~ spl31_15
| ~ spl31_753
| spl31_764
| spl31_771 ),
inference(forward_subsumption_resolution,[],[f14306,f14114]) ).
fof(f14312,plain,
( ~ spl31_15
| ~ spl31_753
| spl31_764
| spl31_771 ),
inference(avatar_contradiction_clause,[],[f14311]) ).
cnf(s2,plain,
( ~ spl31_1
| ~ spl31_3 ),
inference(sat_conversion,[],[f591]) ).
cnf(s3,plain,
spl31_1,
inference(sat_conversion,[],[f592]) ).
cnf(s4,plain,
( ~ spl31_4
| spl31_5 ),
inference(sat_conversion,[],[f604]) ).
cnf(s6,plain,
( ~ spl31_7
| spl31_8 ),
inference(sat_conversion,[],[f627]) ).
cnf(s7,plain,
spl31_7,
inference(sat_conversion,[],[f640]) ).
cnf(s8,plain,
( ~ spl31_9
| spl31_10 ),
inference(sat_conversion,[],[f733]) ).
cnf(s10,plain,
( spl31_13
| ~ spl31_14
| spl31_15 ),
inference(sat_conversion,[],[f775]) ).
cnf(s15,plain,
spl31_14,
inference(sat_conversion,[],[f823]) ).
cnf(s16,plain,
( spl31_3
| ~ spl31_13 ),
inference(sat_conversion,[],[f835]) ).
cnf(s17,plain,
spl31_4,
inference(sat_conversion,[],[f882]) ).
cnf(s18,plain,
( ~ spl31_4
| spl31_9 ),
inference(sat_conversion,[],[f887]) ).
cnf(s31,plain,
( ~ spl31_7
| spl31_12 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s915,plain,
( ~ spl31_9
| spl31_753 ),
inference(sat_conversion,[],[f13680]) ).
cnf(s920,plain,
( ~ spl31_10
| ~ spl31_753
| spl31_768
| ~ spl31_769
| spl31_770
| ~ spl31_771
| ~ spl31_773 ),
inference(sat_conversion,[],[f13780]) ).
cnf(s921,plain,
( ~ spl31_10
| ~ spl31_753
| ~ spl31_769
| spl31_770
| spl31_774 ),
inference(sat_conversion,[],[f13785]) ).
cnf(s935,plain,
( ~ spl31_753
| ~ spl31_770 ),
inference(sat_conversion,[],[f13963]) ).
cnf(s950,plain,
( ~ spl31_753
| spl31_769 ),
inference(sat_conversion,[],[f14056]) ).
cnf(s954,plain,
( ~ spl31_5
| ~ spl31_9
| ~ spl31_753
| ~ spl31_764
| spl31_772
| ~ spl31_774 ),
inference(sat_conversion,[],[f14088]) ).
cnf(s958,plain,
( ~ spl31_8
| ~ spl31_9
| spl31_773 ),
inference(sat_conversion,[],[f14132]) ).
cnf(s961,plain,
( ~ spl31_9
| ~ spl31_12
| ~ spl31_768 ),
inference(sat_conversion,[],[f14232]) ).
cnf(s969,plain,
( ~ spl31_9
| ~ spl31_772 ),
inference(sat_conversion,[],[f14265]) ).
cnf(s976,plain,
( ~ spl31_15
| ~ spl31_753
| spl31_764
| spl31_771 ),
inference(sat_conversion,[],[f14312]) ).
cnf(s1002,plain,
spl31_9,
inference(rat,[],[s18,s17]) ).
cnf(s1003,plain,
~ spl31_772,
inference(rat,[],[s969,s1002]) ).
cnf(s1004,plain,
spl31_753,
inference(rat,[],[s915,s1002]) ).
cnf(s1007,plain,
spl31_769,
inference(rat,[],[s950,s1004]) ).
cnf(s1008,plain,
~ spl31_770,
inference(rat,[],[s935,s1004]) ).
cnf(s1023,plain,
( spl31_13
| spl31_15 ),
inference(rat,[],[s10,s15]) ).
cnf(s1024,plain,
spl31_10,
inference(rat,[],[s8,s1002]) ).
cnf(s1027,plain,
spl31_774,
inference(rat,[],[s921,s1004,s1008,s1007,s1024]) ).
cnf(s1031,plain,
spl31_12,
inference(rat,[],[s31,s7]) ).
cnf(s1033,plain,
~ spl31_768,
inference(rat,[],[s961,s1002,s1031]) ).
cnf(s1038,plain,
spl31_8,
inference(rat,[],[s6,s7]) ).
cnf(s1039,plain,
spl31_773,
inference(rat,[],[s958,s1002,s1038]) ).
cnf(s1043,plain,
~ spl31_771,
inference(rat,[],[s920,s1033,s1024,s1008,s1007,s1004,s1039]) ).
cnf(s1054,plain,
spl31_5,
inference(rat,[],[s4,s17]) ).
cnf(s1055,plain,
~ spl31_764,
inference(rat,[],[s954,s1027,s1003,s1004,s1002,s1054]) ).
cnf(s1057,plain,
~ spl31_15,
inference(rat,[],[s976,s1043,s1004,s1055]) ).
cnf(s1058,plain,
spl31_13,
inference(rat,[],[s1023,s1057]) ).
cnf(s1059,plain,
spl31_3,
inference(rat,[],[s16,s1058]) ).
cnf(s1060,plain,
$false,
inference(rat,[],[s2,s1059,s3]) ).
fof(f14341,plain,
$false,
inference(avatar_sat_refutation,[],[s1060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM616+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 20:46:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.04/2.43 % (1294381)Detected formulas, will run a generic FOF schedule.
% 11.04/2.43 % (1294390)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2810783845:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.04/2.43 % (1294387)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4175620292:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.04/2.43 % (1294390)Instruction limit reached!
% 11.04/2.43 % (1294390)------------------------------
% 11.04/2.43 % (1294390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.43 % (1294390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.43 % (1294390)CaDiCaL version: 2.1.3
% 11.04/2.43 % (1294390)Termination reason: Instruction limit
% 11.04/2.43 % (1294390)Termination phase: Saturation
% 11.04/2.43 % (1294390)Time elapsed: 0.042 s
% 11.04/2.43 % (1294390)Peak memory usage: 89 MB
% 11.04/2.43 % (1294390)Instructions burned: 122 (million)
% 11.04/2.43 % (1294388)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=474716164:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.04/2.43 % (1294386)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1346130720:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.04/2.43 % (1294391)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2434496720:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.04/2.43 % (1294392)dis-21_1_sil=8000:lcm=predicate:random_seed=3154161377:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.04/2.43 % (1294389)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1453065814:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.04/2.43 % (1294389)Instruction limit reached!
% 11.04/2.43 % (1294389)------------------------------
% 11.04/2.43 % (1294389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.43 % (1294389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.43 % (1294389)CaDiCaL version: 2.1.3
% 11.04/2.43 % (1294389)Termination reason: Instruction limit
% 11.04/2.43 % (1294389)Termination phase: Saturation
% 11.04/2.43 % (1294389)Time elapsed: 0.067 s
% 11.04/2.43 % (1294389)Peak memory usage: 90 MB
% 11.04/2.43 % (1294389)Instructions burned: 110 (million)
% 11.04/2.43 % (1294392)Instruction limit reached!
% 11.04/2.43 % (1294392)------------------------------
% 11.04/2.43 % (1294392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.43 % (1294392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.43 % (1294392)CaDiCaL version: 2.1.3
% 11.04/2.43 % (1294392)Termination reason: Instruction limit
% 11.04/2.43 % (1294392)Termination phase: Saturation
% 11.04/2.43 % (1294392)Time elapsed: 0.075 s
% 11.04/2.43 % (1294392)Peak memory usage: 91 MB
% 11.04/2.43 % (1294392)Instructions burned: 130 (million)
% 11.04/2.43 % (1294398)lrs+10_1_sil=8000:sp=occurrence:random_seed=3018465296:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.04/2.43 % (1294391)Instruction limit reached!
% 11.04/2.43 % (1294391)------------------------------
% 11.04/2.43 % (1294391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.43 % (1294391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.43 % (1294391)CaDiCaL version: 2.1.3
% 11.04/2.43 % (1294391)Termination reason: Instruction limit
% 11.04/2.43 % (1294391)Termination phase: Saturation
% 11.04/2.43 % (1294391)Time elapsed: 0.107 s
% 11.04/2.43 % (1294391)Peak memory usage: 90 MB
% 11.04/2.43 % (1294391)Instructions burned: 139 (million)
% 11.04/2.43 % (1294398)Instruction limit reached!
% 11.04/2.43 % (1294398)------------------------------
% 11.04/2.43 % (1294398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.43 % (1294398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.43 % (1294398)CaDiCaL version: 2.1.3
% 11.04/2.43 % (1294398)Termination reason: Instruction limit
% 11.04/2.43 % (1294398)Termination phase: Saturation
% 11.04/2.43 % (1294398)Time elapsed: 0.101 s
% 11.04/2.43 % (1294398)Peak memory usage: 92 MB
% 11.04/2.43 % (1294398)Instructions burned: 286 (million)
% 13.50/2.86 % (1294401)lrs+10_1_sil=32000:urr=on:br=off:random_seed=374949564:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.50/2.86 % (1294401)Refutation not found, incomplete strategy
% 13.50/2.86 % (1294401)------------------------------
% 13.50/2.86 % (1294401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294401)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294401)Termination reason: Refutation not found, incomplete strategy
% 13.50/2.86 % (1294401)Time elapsed: 0.003 s
% 13.50/2.86 % (1294401)Peak memory usage: 89 MB
% 13.50/2.86 % (1294401)Instructions burned: 3 (million)
% 13.50/2.86 % (1294403)lrs+1011_1_sil=32000:sp=occurrence:random_seed=80923865:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.50/2.86 % (1294404)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=405939156:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.50/2.86 % (1294405)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3945289609:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 13.50/2.86 % (1294405)Instruction limit reached!
% 13.50/2.86 % (1294405)------------------------------
% 13.50/2.86 % (1294405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294405)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294405)Termination reason: Instruction limit
% 13.50/2.86 % (1294405)Termination phase: Saturation
% 13.50/2.86 % (1294405)Time elapsed: 0.099 s
% 13.50/2.86 % (1294405)Peak memory usage: 90 MB
% 13.50/2.86 % (1294405)Instructions burned: 296 (million)
% 13.50/2.86 % (1294404)Instruction limit reached!
% 13.50/2.86 % (1294404)------------------------------
% 13.50/2.86 % (1294404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294404)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294404)Termination reason: Instruction limit
% 13.50/2.86 % (1294404)Termination phase: Saturation
% 13.50/2.86 % (1294404)Time elapsed: 0.145 s
% 13.50/2.86 % (1294404)Peak memory usage: 92 MB
% 13.50/2.86 % (1294404)Instructions burned: 248 (million)
% 13.50/2.86 % (1294401)------------------------------
% 13.50/2.86 % (1294401)------------------------------
% 13.50/2.86 % (1294403)Instruction limit reached!
% 13.50/2.86 % (1294403)------------------------------
% 13.50/2.86 % (1294403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294403)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294403)Termination reason: Instruction limit
% 13.50/2.86 % (1294403)Termination phase: Saturation
% 13.50/2.86 % (1294403)Time elapsed: 0.228 s
% 13.50/2.86 % (1294403)Peak memory usage: 92 MB
% 13.50/2.86 % (1294403)Instructions burned: 325 (million)
% 13.50/2.86 % (1294410)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=108162528:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 13.50/2.86 % (1294411)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3467505323:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 13.50/2.86 % (1294412)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3091485266:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 13.50/2.86 % (1294411)Instruction limit reached!
% 13.50/2.86 % (1294411)------------------------------
% 13.50/2.86 % (1294411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294411)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294411)Termination reason: Instruction limit
% 13.50/2.86 % (1294411)Termination phase: Saturation
% 13.50/2.86 % (1294411)Time elapsed: 0.076 s
% 13.50/2.86 % (1294411)Peak memory usage: 91 MB
% 13.50/2.86 % (1294411)Instructions burned: 114 (million)
% 13.50/2.86 % (1294413)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1596458265:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 13.50/2.86 % (1294412)Instruction limit reached!
% 13.50/2.86 % (1294412)------------------------------
% 13.50/2.86 % (1294412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294412)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294412)Termination reason: Instruction limit
% 13.50/2.86 % (1294412)Termination phase: Saturation
% 13.50/2.86 % (1294412)Time elapsed: 0.068 s
% 13.50/2.86 % (1294412)Peak memory usage: 89 MB
% 13.50/2.86 % (1294412)Instructions burned: 127 (million)
% 13.50/2.86 % (1294413)Instruction limit reached!
% 13.50/2.86 % (1294413)------------------------------
% 13.50/2.86 % (1294413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294413)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294413)Termination reason: Instruction limit
% 13.50/2.86 % (1294413)Termination phase: Saturation
% 13.50/2.86 % (1294413)Time elapsed: 0.074 s
% 13.50/2.86 % (1294413)Peak memory usage: 89 MB
% 13.50/2.86 % (1294413)Instructions burned: 115 (million)
% 13.50/2.86 % (1294418)lrs+10_1_sil=8000:sp=occurrence:random_seed=1790701752:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 13.50/2.86 % (1294419)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1448127941:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 13.50/2.86 % (1294420)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=226120656:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 13.50/2.86 % (1294419)Instruction limit reached!
% 13.50/2.86 % (1294419)------------------------------
% 13.50/2.86 % (1294419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294419)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294419)Termination reason: Instruction limit
% 13.50/2.86 % (1294419)Termination phase: Saturation
% 13.50/2.86 % (1294419)Time elapsed: 0.271 s
% 13.50/2.86 % (1294419)Peak memory usage: 92 MB
% 13.50/2.86 % (1294419)Instructions burned: 437 (million)
% 13.50/2.86 % (1294424)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2028972736:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 13.50/2.86 % (1294424)Instruction limit reached!
% 13.50/2.86 % (1294424)------------------------------
% 13.50/2.86 % (1294424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294424)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294424)Termination reason: Instruction limit
% 13.50/2.86 % (1294424)Termination phase: Saturation
% 13.50/2.86 % (1294424)Time elapsed: 0.078 s
% 13.50/2.86 % (1294424)Peak memory usage: 91 MB
% 13.50/2.86 % (1294424)Instructions burned: 135 (million)
% 13.50/2.86 % (1294418)Instruction limit reached!
% 13.50/2.86 % (1294418)------------------------------
% 13.50/2.86 % (1294418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294418)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294418)Termination reason: Instruction limit
% 13.50/2.86 % (1294418)Termination phase: Saturation
% 13.50/2.86 % (1294418)Time elapsed: 0.546 s
% 13.50/2.86 % (1294418)Peak memory usage: 99 MB
% 13.50/2.86 % (1294418)Instructions burned: 907 (million)
% 13.50/2.86 % (1294410)Instruction limit reached!
% 13.50/2.86 % (1294410)------------------------------
% 13.50/2.86 % (1294410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294410)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294410)Termination reason: Instruction limit
% 13.50/2.86 % (1294410)Termination phase: Saturation
% 13.50/2.86 % (1294410)Time elapsed: 0.888 s
% 13.50/2.86 % (1294410)Peak memory usage: 142 MB
% 13.50/2.86 % (1294410)Instructions burned: 2351 (million)
% 13.50/2.86 % (1294426)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1768167587:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 13.50/2.86 % (1294427)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1053375507:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 13.50/2.86 % (1294428)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3679103157:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 13.50/2.86 % (1294428)Instruction limit reached!
% 13.50/2.86 % (1294428)------------------------------
% 13.50/2.86 % (1294428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294428)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294428)Termination reason: Instruction limit
% 13.50/2.86 % (1294428)Termination phase: Saturation
% 13.50/2.86 % (1294428)Time elapsed: 0.047 s
% 13.50/2.86 % (1294428)Peak memory usage: 91 MB
% 13.50/2.86 % (1294428)Instructions burned: 126 (million)
% 13.50/2.86 % (1294432)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2233268497:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 13.50/2.86 % (1294386)First to succeed.
% 13.50/2.86 % (1294386)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1294381"
% 13.50/2.86 % (1294432)Instruction limit reached!
% 13.50/2.86 % (1294432)------------------------------
% 13.50/2.86 % (1294432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294432)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294432)Termination reason: Instruction limit
% 13.50/2.86 % (1294432)Termination phase: Saturation
% 13.50/2.86 % (1294432)Time elapsed: 0.046 s
% 13.50/2.86 % (1294432)Peak memory usage: 91 MB
% 13.50/2.86 % (1294432)Instructions burned: 135 (million)
% 13.50/2.86 % (1294426)Instruction limit reached!
% 13.50/2.86 % (1294426)------------------------------
% 13.50/2.86 % (1294426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294426)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294426)Termination reason: Instruction limit
% 13.50/2.86 % (1294426)Termination phase: Saturation
% 13.50/2.86 % (1294426)Time elapsed: 0.278 s
% 13.50/2.86 % (1294426)Peak memory usage: 91 MB
% 13.50/2.86 % (1294426)Instructions burned: 592 (million)
% 13.50/2.86 % (1294434)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1532684818:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 13.50/2.86 % (1294434)Instruction limit reached!
% 13.50/2.86 % (1294434)------------------------------
% 13.50/2.86 % (1294434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.86 % (1294434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.86 % (1294434)CaDiCaL version: 2.1.3
% 13.50/2.86 % (1294434)Termination reason: Instruction limit
% 13.50/2.86 % (1294434)Termination phase: Saturation
% 13.50/2.86 % (1294434)Time elapsed: 0.052 s
% 13.50/2.86 % (1294434)Peak memory usage: 91 MB
% 13.50/2.86 % (1294434)Instructions burned: 141 (million)
% 13.50/2.86 % (1294435)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1613592076:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 13.50/2.86 % (1294437)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3806042792:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 13.50/2.86 % (1294386)Refutation found. Thanks to Tanya!
% 13.50/2.86 % SZS status Theorem for theBenchmark
% 13.50/2.86 % SZS output start Proof for theBenchmark
% See solution above
% 14.77/2.95 % (1294386)------------------------------
% 14.77/2.95 % (1294386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.77/2.95 % (1294386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.77/2.95 % (1294386)CaDiCaL version: 2.1.3
% 14.77/2.95 % (1294386)Termination reason: Refutation
% 14.77/2.95 % (1294386)Time elapsed: 1.610 s
% 14.77/2.95 % (1294386)Peak memory usage: 144 MB
% 14.77/2.95 % (1294386)Instructions burned: 2395 (million)
% 14.77/2.95 % (1294386)------------------------------
% 14.77/2.95 % (1294386)------------------------------
% 14.77/2.95 % (1294381)Success in time 2.02 s
% 14.77/2.95 % Vampire exiting
%------------------------------------------------------------------------------