%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG054+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 : n014.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:35:18 PM UTC 2026
% Result : Theorem 17.99s 3.82s
% Output : Refutation 20.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 51
% Syntax : Number of formulae : 361 ( 57 unt; 26 def)
% Number of atoms : 1218 ( 86 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1639 ( 782 ~; 758 |; 56 &)
% ( 26 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 27 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 17 con; 0-2 aty)
% Number of variables : 261 ( 0 sgn 261 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(f17,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMNeg) ).
fof(f18,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMDNeg) ).
fof(f20,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERef) ).
fof(f21,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETrn) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMon) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMonM) ).
fof(f25,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETot) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScSqPos) ).
fof(f42,axiom,
( aVector0(xp)
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1709) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1746) ).
fof(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1766) ).
fof(f46,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1783) ).
fof(f48,axiom,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1820) ).
fof(f51,axiom,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1873) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
fof(f53,axiom,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
fof(f54,axiom,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
fof(f55,axiom,
( aScalar0(xN)
& xN = sdtasdt0(xR,xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1949) ).
fof(f57,conjecture,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f58,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f59,plain,
~ sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(flattening,[],[f58]) ).
fof(f67,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f87,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f88,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f87]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(flattening,[],[f89]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(ennf_transformation,[],[f23]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(flattening,[],[f91]) ).
fof(f93,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f94,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f96,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f98,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f99,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f98]) ).
fof(f103,plain,
! [X0] :
( ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 )
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f108]) ).
fof(f114,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f115,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0,X1] :
( ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) )
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f117,plain,
! [X0,X1] :
( ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) )
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f116]) ).
fof(f118,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f130,plain,
aVector0(xp),
inference(cnf_transformation,[],[f42]) ).
fof(f134,plain,
aScalar0(xA),
inference(cnf_transformation,[],[f44]) ).
fof(f136,plain,
aScalar0(xB),
inference(cnf_transformation,[],[f45]) ).
fof(f137,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[],[f46]) ).
fof(f138,plain,
aScalar0(xC),
inference(cnf_transformation,[],[f46]) ).
fof(f142,plain,
aScalar0(xE),
inference(cnf_transformation,[],[f48]) ).
fof(f147,plain,
xH = sdtasdt0(xA,xB),
inference(cnf_transformation,[],[f51]) ).
fof(f148,plain,
aScalar0(xH),
inference(cnf_transformation,[],[f51]) ).
fof(f150,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f151,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[],[f53]) ).
fof(f152,plain,
aScalar0(xP),
inference(cnf_transformation,[],[f53]) ).
fof(f154,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f155,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[],[f55]) ).
fof(f156,plain,
aScalar0(xN),
inference(cnf_transformation,[],[f55]) ).
fof(f158,plain,
~ sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(cnf_transformation,[],[f59]) ).
fof(f159,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f176,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f177,plain,
! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(cnf_transformation,[],[f92]) ).
fof(f179,plain,
! [X2,X0,X1] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f94]) ).
fof(f180,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f181,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f182,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f189,plain,
! [X0] :
( smndt0(smndt0(X0)) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f190,plain,
! [X0] :
( sz0z00 = sdtpldt0(smndt0(X0),X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f193,plain,
! [X0] :
( sz0z00 = sdtasdt0(X0,sz0z00)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f195,plain,
! [X0] :
( sdtpldt0(X0,sz0z00) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f196,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f200,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f206,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(smndt0(X0),smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f207,plain,
! [X0,X1] :
( smndt0(sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f208,plain,
! [X0,X1] :
( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f209,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f214,definition,
( spl2_1
<=> ! [X2] : ~ aScalar0(X2) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f215,plain,
( ! [X2] : ~ aScalar0(X2)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f217,definition,
( spl2_2
<=> ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f218,plain,
( ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f219,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f200,f217,f214]) ).
fof(f237,definition,
( spl2_5
<=> sdtlseqdt0(sz0z00,xS) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f238,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| spl2_5 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f259,definition,
( spl2_7
<=> aScalar0(sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f260,plain,
( aScalar0(sdtasdt0(xP,xP))
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f261,plain,
( ~ aScalar0(sdtasdt0(xP,xP))
| spl2_7 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f267,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| spl2_7 ),
inference(resolution,[],[f261,f182]) ).
fof(f268,plain,
( ~ aScalar0(xP)
| spl2_7 ),
inference(duplicate_literal_removal,[],[f267]) ).
fof(f269,plain,
( $false
| spl2_7 ),
inference(forward_subsumption_resolution,[],[f268,f152]) ).
fof(f270,plain,
spl2_7,
inference(avatar_contradiction_clause,[],[f269]) ).
fof(f279,definition,
( spl2_9
<=> sdtlseqdt0(sz0z00,xH) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f280,plain,
( sdtlseqdt0(sz0z00,xH)
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f281,plain,
( ~ sdtlseqdt0(sz0z00,xH)
| spl2_9 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f286,plain,
! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xP,xP),X0)
| ~ sdtlseqdt0(X0,xN)
| ~ aScalar0(sdtasdt0(xP,xP))
| ~ aScalar0(X0)
| ~ aScalar0(xN) ),
inference(resolution,[],[f179,f158]) ).
fof(f287,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xP,xP),X0)
| ~ sdtlseqdt0(X0,xN)
| ~ aScalar0(X0)
| ~ aScalar0(xN) )
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f286,f260]) ).
fof(f288,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xP,xP),X0)
| ~ sdtlseqdt0(X0,xN)
| ~ aScalar0(X0) )
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f287,f156]) ).
fof(f289,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ aScalar0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xP,X0)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xP,X1)
| ~ aScalar0(xP)
| ~ aScalar0(X0)
| ~ aScalar0(xP)
| ~ aScalar0(X1) )
| ~ spl2_7 ),
inference(resolution,[],[f288,f177]) ).
fof(f296,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ aScalar0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xP,X0)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xP,X1)
| ~ aScalar0(xP)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_7 ),
inference(duplicate_literal_removal,[],[f289]) ).
fof(f299,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ aScalar0(sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xP,X0)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xP,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f296,f152]) ).
fof(f300,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ sdtlseqdt0(xP,X0)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xP,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f299,f182]) ).
fof(f302,definition,
( spl2_11
<=> sdtlseqdt0(sz0z00,xP) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f303,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f304,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| spl2_11 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl2_12
<=> ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,X1)
| ~ sdtlseqdt0(xP,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f307,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,X1)
| ~ sdtlseqdt0(xP,X0) )
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f308,plain,
( ~ spl2_11
| spl2_12
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f300,f259,f306,f302]) ).
fof(f312,plain,
( sdtasdt0(xE,smndt0(xH)) = smndt0(xP)
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(superposition,[],[f208,f151]) ).
fof(f315,plain,
( sdtasdt0(xE,smndt0(xH)) = smndt0(xP)
| ~ aScalar0(xH) ),
inference(forward_subsumption_resolution,[],[f312,f142]) ).
fof(f317,plain,
sdtasdt0(xE,smndt0(xH)) = smndt0(xP),
inference(forward_subsumption_resolution,[],[f315,f148]) ).
fof(f325,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = smndt0(sdtasdt0(X0,smndt0(X1)))
| ~ aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(superposition,[],[f189,f208]) ).
fof(f326,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = smndt0(sdtasdt0(X0,smndt0(X1)))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f325,f182]) ).
fof(f370,plain,
( smndt0(xP) = sdtasdt0(smndt0(xE),xH)
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(superposition,[],[f207,f151]) ).
fof(f382,plain,
( smndt0(xP) = sdtasdt0(smndt0(xE),xH)
| ~ aScalar0(xH) ),
inference(forward_subsumption_resolution,[],[f370,f142]) ).
fof(f385,plain,
smndt0(xP) = sdtasdt0(smndt0(xE),xH),
inference(forward_subsumption_resolution,[],[f382,f148]) ).
fof(f386,plain,
( smndt0(xP) = sdtasdt0(xH,smndt0(xE))
| ~ aScalar0(smndt0(xE))
| ~ aScalar0(xH)
| ~ spl2_2 ),
inference(superposition,[],[f385,f218]) ).
fof(f390,plain,
( aScalar0(smndt0(xP))
| ~ aScalar0(smndt0(xE))
| ~ aScalar0(xH) ),
inference(superposition,[],[f182,f385]) ).
fof(f401,plain,
( aScalar0(smndt0(xP))
| ~ aScalar0(smndt0(xE)) ),
inference(forward_subsumption_resolution,[],[f390,f148]) ).
fof(f404,plain,
( smndt0(xP) = sdtasdt0(xH,smndt0(xE))
| ~ aScalar0(smndt0(xE))
| ~ spl2_2 ),
inference(forward_subsumption_resolution,[],[f386,f148]) ).
fof(f406,definition,
( spl2_13
<=> aScalar0(smndt0(xE)) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f407,plain,
( aScalar0(smndt0(xE))
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f408,plain,
( ~ aScalar0(smndt0(xE))
| spl2_13 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f410,definition,
( spl2_14
<=> smndt0(xP) = sdtasdt0(xH,smndt0(xE)) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f412,plain,
( smndt0(xP) = sdtasdt0(xH,smndt0(xE))
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f430,definition,
( spl2_18
<=> aScalar0(smndt0(xP)) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f432,plain,
( aScalar0(smndt0(xP))
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f433,plain,
( ~ spl2_13
| spl2_18 ),
inference(avatar_split_clause,[],[f401,f430,f406]) ).
fof(f439,plain,
( ~ spl2_13
| spl2_14
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f404,f217,f410,f406]) ).
fof(f476,definition,
( spl2_20
<=> aScalar0(smndt0(xR)) ),
introduced(definition,[new_symbols(definition,[spl2_20])],[avatar_definition]) ).
fof(f477,plain,
( aScalar0(smndt0(xR))
| ~ spl2_20 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f478,plain,
( ~ aScalar0(smndt0(xR))
| spl2_20 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f568,plain,
( ~ aScalar0(xE)
| spl2_13 ),
inference(resolution,[],[f209,f408]) ).
fof(f569,plain,
( ~ aScalar0(xR)
| spl2_20 ),
inference(resolution,[],[f209,f478]) ).
fof(f575,plain,
( $false
| spl2_20 ),
inference(forward_subsumption_resolution,[],[f569,f150]) ).
fof(f576,plain,
spl2_20,
inference(avatar_contradiction_clause,[],[f575]) ).
fof(f577,plain,
( $false
| spl2_13 ),
inference(forward_subsumption_resolution,[],[f568,f142]) ).
fof(f578,plain,
spl2_13,
inference(avatar_contradiction_clause,[],[f577]) ).
fof(f665,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,smndt0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X2) ),
inference(superposition,[],[f178,f190]) ).
fof(f666,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X1)
| ~ sdtlseqdt0(X0,X2)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X0) ),
inference(superposition,[],[f178,f190]) ).
fof(f671,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X1)
| ~ sdtlseqdt0(X0,X2)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2) ),
inference(duplicate_literal_removal,[],[f666]) ).
fof(f672,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,smndt0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(duplicate_literal_removal,[],[f665]) ).
fof(f676,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X1)
| ~ sdtlseqdt0(X0,X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f671,f209]) ).
fof(f677,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,smndt0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f672,f209]) ).
fof(f683,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2)
| ~ aScalar0(X0) ),
inference(superposition,[],[f177,f193]) ).
fof(f706,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) ),
inference(duplicate_literal_removal,[],[f683]) ).
fof(f717,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f706,f181]) ).
fof(f723,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f717,f196]) ).
fof(f726,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_2 ),
inference(superposition,[],[f723,f218]) ).
fof(f731,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(superposition,[],[f723,f206]) ).
fof(f732,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(X0,xE)
| ~ sdtlseqdt0(sz0z00,xH)
| ~ aScalar0(X0)
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(superposition,[],[f723,f151]) ).
fof(f734,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,xR)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) ),
inference(superposition,[],[f723,f155]) ).
fof(f737,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl2_2 ),
inference(duplicate_literal_removal,[],[f726]) ).
fof(f740,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f731,f209]) ).
fof(f743,definition,
( spl2_27
<=> ! [X1] :
( ~ sdtlseqdt0(X1,xE)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f744,plain,
( ! [X1] :
( ~ sdtlseqdt0(X1,xE)
| ~ aScalar0(X1) )
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f749,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f740,f209]) ).
fof(f752,plain,
( ~ aScalar0(xE)
| ~ aScalar0(xE)
| ~ spl2_27 ),
inference(resolution,[],[f744,f181]) ).
fof(f753,plain,
( ~ aScalar0(xE)
| ~ spl2_27 ),
inference(duplicate_literal_removal,[],[f752]) ).
fof(f756,plain,
( $false
| ~ spl2_27 ),
inference(forward_subsumption_resolution,[],[f753,f142]) ).
fof(f757,plain,
~ spl2_27,
inference(avatar_contradiction_clause,[],[f756]) ).
fof(f801,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X1))
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(smndt0(X1))
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_2 ),
inference(superposition,[],[f737,f206]) ).
fof(f812,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X1))
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_2 ),
inference(forward_subsumption_resolution,[],[f801,f209]) ).
fof(f826,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X1))
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_2 ),
inference(forward_subsumption_resolution,[],[f812,f209]) ).
fof(f837,definition,
( spl2_35
<=> sdtlseqdt0(sz0z00,xN) ),
introduced(definition,[new_symbols(definition,[spl2_35])],[avatar_definition]) ).
fof(f838,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| spl2_35 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f839,plain,
( sdtlseqdt0(sz0z00,xN)
| ~ spl2_35 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f859,definition,
( spl2_40
<=> sdtlseqdt0(sz0z00,smndt0(xP)) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f860,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xP))
| spl2_40 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f861,plain,
( sdtlseqdt0(sz0z00,smndt0(xP))
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f1056,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,smndt0(xR))
| ~ sdtlseqdt0(sz0z00,smndt0(xS))
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) ),
inference(superposition,[],[f749,f155]) ).
fof(f1061,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,smndt0(xR))
| ~ sdtlseqdt0(sz0z00,smndt0(xS))
| ~ aScalar0(X0)
| ~ aScalar0(xS) ),
inference(forward_subsumption_resolution,[],[f1056,f150]) ).
fof(f1068,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,smndt0(xR))
| ~ sdtlseqdt0(sz0z00,smndt0(xS))
| ~ aScalar0(X0) ),
inference(forward_subsumption_resolution,[],[f1061,f154]) ).
fof(f1070,definition,
( spl2_47
<=> ! [X1] :
( ~ sdtlseqdt0(X1,smndt0(xE))
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_47])],[avatar_definition]) ).
fof(f1071,plain,
( ! [X1] :
( ~ sdtlseqdt0(X1,smndt0(xE))
| ~ aScalar0(X1) )
| ~ spl2_47 ),
inference(avatar_component_clause,[],[f1070]) ).
fof(f1081,definition,
( spl2_49
<=> sdtlseqdt0(sz0z00,smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f1083,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xS))
| spl2_49 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl2_50
<=> ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xR))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_50])],[avatar_definition]) ).
fof(f1086,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xR))
| ~ aScalar0(X0) )
| ~ spl2_50 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1087,plain,
( ~ spl2_49
| spl2_50
| spl2_35 ),
inference(avatar_split_clause,[],[f1068,f837,f1085,f1081]) ).
fof(f1104,plain,
( ~ aScalar0(smndt0(xE))
| ~ aScalar0(smndt0(xE))
| ~ spl2_47 ),
inference(resolution,[],[f1071,f181]) ).
fof(f1105,plain,
( ~ aScalar0(smndt0(xE))
| ~ spl2_47 ),
inference(duplicate_literal_removal,[],[f1104]) ).
fof(f1108,plain,
( $false
| ~ spl2_13
| ~ spl2_47 ),
inference(forward_subsumption_resolution,[],[f1105,f407]) ).
fof(f1109,plain,
( ~ spl2_13
| ~ spl2_47 ),
inference(avatar_contradiction_clause,[],[f1108]) ).
fof(f1142,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0) ),
inference(superposition,[],[f676,f195]) ).
fof(f1143,plain,
! [X0,X1] :
( sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(X0,smndt0(X1))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(superposition,[],[f677,f195]) ).
fof(f1145,plain,
! [X0,X1] :
( sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(X0,smndt0(X1))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X1) ),
inference(duplicate_literal_removal,[],[f1143]) ).
fof(f1146,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00) ),
inference(duplicate_literal_removal,[],[f1142]) ).
fof(f1154,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,smndt0(X1))
| sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1145,f196]) ).
fof(f1155,plain,
! [X0,X1] :
( ~ sdtlseqdt0(smndt0(X1),X0)
| sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1146,f196]) ).
fof(f1160,plain,
! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0)) ),
inference(resolution,[],[f1155,f181]) ).
fof(f1165,plain,
! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(duplicate_literal_removal,[],[f1160]) ).
fof(f1171,plain,
! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0) ),
inference(forward_subsumption_resolution,[],[f1165,f209]) ).
fof(f1437,plain,
( sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(xS)
| ~ aScalar0(sz0z00)
| spl2_5 ),
inference(resolution,[],[f239,f176]) ).
fof(f1438,plain,
( sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(sz0z00)
| spl2_5 ),
inference(forward_subsumption_resolution,[],[f1437,f154]) ).
fof(f1440,plain,
( sdtlseqdt0(xS,sz0z00)
| spl2_5 ),
inference(forward_subsumption_resolution,[],[f1438,f196]) ).
fof(f1595,plain,
( sdtlseqdt0(sz0z00,xC)
| ~ aVector0(xp) ),
inference(superposition,[],[f159,f137]) ).
fof(f1600,plain,
sdtlseqdt0(sz0z00,xC),
inference(forward_subsumption_resolution,[],[f1595,f130]) ).
fof(f1848,plain,
( $false
| ~ spl2_1 ),
inference(resolution,[],[f215,f196]) ).
fof(f1884,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f1848]) ).
fof(f1899,plain,
! [X0] :
( sdtlseqdt0(smndt0(X0),sz0z00)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0)) ),
inference(resolution,[],[f1154,f181]) ).
fof(f1910,plain,
! [X0] :
( sdtlseqdt0(smndt0(X0),sz0z00)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(duplicate_literal_removal,[],[f1899]) ).
fof(f1919,plain,
! [X0] :
( sdtlseqdt0(smndt0(X0),sz0z00)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) ),
inference(forward_subsumption_resolution,[],[f1910,f209]) ).
fof(f2325,definition,
( spl2_93
<=> ! [X2] :
( ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f2326,plain,
( ! [X2] :
( ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X2) )
| ~ spl2_93 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2381,plain,
( ~ aScalar0(xC)
| ~ spl2_93 ),
inference(resolution,[],[f2326,f1600]) ).
fof(f2398,plain,
( $false
| ~ spl2_93 ),
inference(forward_subsumption_resolution,[],[f2381,f138]) ).
fof(f2399,plain,
~ spl2_93,
inference(avatar_contradiction_clause,[],[f2398]) ).
fof(f2591,plain,
( ~ sdtlseqdt0(xP,sz0z00)
| sz0z00 = xP
| ~ aScalar0(xP)
| ~ aScalar0(sz0z00)
| ~ spl2_11 ),
inference(resolution,[],[f303,f180]) ).
fof(f2597,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,xN)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,sz0z00)
| ~ sdtlseqdt0(xP,X0)
| ~ aScalar0(X0) )
| ~ spl2_12 ),
inference(superposition,[],[f307,f193]) ).
fof(f2814,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(xS)
| spl2_49 ),
inference(resolution,[],[f1083,f1171]) ).
fof(f2819,plain,
( ~ aScalar0(xS)
| spl2_5
| spl2_49 ),
inference(forward_subsumption_resolution,[],[f2814,f1440]) ).
fof(f2822,plain,
( $false
| spl2_5
| spl2_49 ),
inference(forward_subsumption_resolution,[],[f2819,f154]) ).
fof(f2823,plain,
( spl2_5
| spl2_49 ),
inference(avatar_contradiction_clause,[],[f2822]) ).
fof(f2846,plain,
( ~ aScalar0(smndt0(xR))
| ~ aScalar0(smndt0(xR))
| ~ spl2_50 ),
inference(resolution,[],[f1086,f181]) ).
fof(f2849,plain,
( ~ aScalar0(smndt0(xR))
| ~ spl2_50 ),
inference(duplicate_literal_removal,[],[f2846]) ).
fof(f2853,plain,
( $false
| ~ spl2_20
| ~ spl2_50 ),
inference(forward_subsumption_resolution,[],[f2849,f477]) ).
fof(f2854,plain,
( ~ spl2_20
| ~ spl2_50 ),
inference(avatar_contradiction_clause,[],[f2853]) ).
fof(f3085,plain,
( sdtasdt0(xE,xH) = smndt0(smndt0(xP))
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(superposition,[],[f326,f317]) ).
fof(f3115,plain,
( sdtasdt0(xE,xH) = smndt0(smndt0(xP))
| ~ aScalar0(xH) ),
inference(forward_subsumption_resolution,[],[f3085,f142]) ).
fof(f3151,plain,
sdtasdt0(xE,xH) = smndt0(smndt0(xP)),
inference(forward_subsumption_resolution,[],[f3115,f148]) ).
fof(f3157,plain,
xP = smndt0(smndt0(xP)),
inference(forward_demodulation,[],[f3151,f151]) ).
fof(f3171,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ sdtlseqdt0(sz0z00,smndt0(xP))
| ~ aScalar0(smndt0(xP)) ),
inference(superposition,[],[f1919,f3157]) ).
fof(f3449,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(xP))
| ~ sdtlseqdt0(X0,smndt0(xE))
| ~ sdtlseqdt0(sz0z00,xH)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xE))
| ~ aScalar0(xH) )
| ~ spl2_2
| ~ spl2_14 ),
inference(superposition,[],[f737,f412]) ).
fof(f3833,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xH)
| ~ sdtlseqdt0(X0,xA)
| ~ sdtlseqdt0(sz0z00,xB)
| ~ aScalar0(X0)
| ~ aScalar0(xA)
| ~ aScalar0(xB) ),
inference(superposition,[],[f723,f147]) ).
fof(f3834,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,xH)
| ~ sdtlseqdt0(X0,xB)
| ~ sdtlseqdt0(sz0z00,xA)
| ~ aScalar0(X0)
| ~ aScalar0(xB)
| ~ aScalar0(xA) )
| ~ spl2_2 ),
inference(superposition,[],[f737,f147]) ).
fof(f3837,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,xH)
| ~ sdtlseqdt0(X0,smndt0(xB))
| ~ sdtlseqdt0(sz0z00,smndt0(xA))
| ~ aScalar0(X0)
| ~ aScalar0(xA)
| ~ aScalar0(xB) )
| ~ spl2_2 ),
inference(superposition,[],[f826,f147]) ).
fof(f3844,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ sdtlseqdt0(sz0z00,smndt0(xA))
| ~ aScalar0(X0)
| ~ aScalar0(xA)
| ~ aScalar0(xB) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3837,f281]) ).
fof(f3846,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xB)
| ~ sdtlseqdt0(sz0z00,xA)
| ~ aScalar0(X0)
| ~ aScalar0(xB)
| ~ aScalar0(xA) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3834,f281]) ).
fof(f3847,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xA)
| ~ sdtlseqdt0(sz0z00,xB)
| ~ aScalar0(X0)
| ~ aScalar0(xA)
| ~ aScalar0(xB) )
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3833,f281]) ).
fof(f3861,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ sdtlseqdt0(sz0z00,smndt0(xA))
| ~ aScalar0(X0)
| ~ aScalar0(xB) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3844,f134]) ).
fof(f3863,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xB)
| ~ sdtlseqdt0(sz0z00,xA)
| ~ aScalar0(X0)
| ~ aScalar0(xA) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3846,f136]) ).
fof(f3864,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xA)
| ~ sdtlseqdt0(sz0z00,xB)
| ~ aScalar0(X0)
| ~ aScalar0(xB) )
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3847,f134]) ).
fof(f3878,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ sdtlseqdt0(sz0z00,smndt0(xA))
| ~ aScalar0(X0) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3861,f136]) ).
fof(f3880,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xB)
| ~ sdtlseqdt0(sz0z00,xA)
| ~ aScalar0(X0) )
| ~ spl2_2
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3863,f134]) ).
fof(f3881,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xA)
| ~ sdtlseqdt0(sz0z00,xB)
| ~ aScalar0(X0) )
| spl2_9 ),
inference(forward_subsumption_resolution,[],[f3864,f136]) ).
fof(f3884,definition,
( spl2_134
<=> sdtlseqdt0(sz0z00,xB) ),
introduced(definition,[new_symbols(definition,[spl2_134])],[avatar_definition]) ).
fof(f3886,plain,
( ~ sdtlseqdt0(sz0z00,xB)
| spl2_134 ),
inference(avatar_component_clause,[],[f3884]) ).
fof(f3894,definition,
( spl2_136
<=> sdtlseqdt0(sz0z00,smndt0(xA)) ),
introduced(definition,[new_symbols(definition,[spl2_136])],[avatar_definition]) ).
fof(f3895,plain,
( sdtlseqdt0(sz0z00,smndt0(xA))
| ~ spl2_136 ),
inference(avatar_component_clause,[],[f3894]) ).
fof(f3896,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xA))
| spl2_136 ),
inference(avatar_component_clause,[],[f3894]) ).
fof(f3898,definition,
( spl2_137
<=> ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_137])],[avatar_definition]) ).
fof(f3899,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ aScalar0(X0) )
| ~ spl2_137 ),
inference(avatar_component_clause,[],[f3898]) ).
fof(f3910,definition,
( spl2_140
<=> sdtlseqdt0(sz0z00,xA) ),
introduced(definition,[new_symbols(definition,[spl2_140])],[avatar_definition]) ).
fof(f3912,plain,
( ~ sdtlseqdt0(sz0z00,xA)
| spl2_140 ),
inference(avatar_component_clause,[],[f3910]) ).
fof(f3914,definition,
( spl2_141
<=> ! [X0] :
( ~ sdtlseqdt0(X0,xB)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_141])],[avatar_definition]) ).
fof(f3915,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xB)
| ~ aScalar0(X0) )
| ~ spl2_141 ),
inference(avatar_component_clause,[],[f3914]) ).
fof(f3916,plain,
( ~ spl2_140
| spl2_141
| ~ spl2_2
| spl2_9 ),
inference(avatar_split_clause,[],[f3880,f279,f217,f3914,f3910]) ).
fof(f3918,definition,
( spl2_142
<=> ! [X0] :
( ~ sdtlseqdt0(X0,xA)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_142])],[avatar_definition]) ).
fof(f3919,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xA)
| ~ aScalar0(X0) )
| ~ spl2_142 ),
inference(avatar_component_clause,[],[f3918]) ).
fof(f3920,plain,
( ~ spl2_134
| spl2_142
| spl2_9 ),
inference(avatar_split_clause,[],[f3881,f279,f3918,f3884]) ).
fof(f3943,plain,
( sdtlseqdt0(xA,sz0z00)
| ~ aScalar0(xA)
| ~ aScalar0(sz0z00)
| spl2_140 ),
inference(resolution,[],[f3912,f176]) ).
fof(f3944,plain,
( sdtlseqdt0(xA,sz0z00)
| ~ aScalar0(sz0z00)
| spl2_140 ),
inference(forward_subsumption_resolution,[],[f3943,f134]) ).
fof(f3947,plain,
( sdtlseqdt0(xA,sz0z00)
| spl2_140 ),
inference(forward_subsumption_resolution,[],[f3944,f196]) ).
fof(f3958,plain,
( sdtlseqdt0(xB,sz0z00)
| ~ aScalar0(xB)
| ~ aScalar0(sz0z00)
| spl2_134 ),
inference(resolution,[],[f3886,f176]) ).
fof(f3959,plain,
( sdtlseqdt0(xB,sz0z00)
| ~ aScalar0(sz0z00)
| spl2_134 ),
inference(forward_subsumption_resolution,[],[f3958,f136]) ).
fof(f3962,plain,
( sdtlseqdt0(xB,sz0z00)
| spl2_134 ),
inference(forward_subsumption_resolution,[],[f3959,f196]) ).
fof(f3965,plain,
( ~ sdtlseqdt0(xA,sz0z00)
| ~ aScalar0(xA)
| spl2_136 ),
inference(resolution,[],[f3896,f1171]) ).
fof(f3972,plain,
( ~ aScalar0(xA)
| spl2_136
| spl2_140 ),
inference(forward_subsumption_resolution,[],[f3965,f3947]) ).
fof(f3986,plain,
( $false
| spl2_136
| spl2_140 ),
inference(forward_subsumption_resolution,[],[f3972,f134]) ).
fof(f3987,plain,
( spl2_136
| spl2_140 ),
inference(avatar_contradiction_clause,[],[f3986]) ).
fof(f3998,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xE))
| ~ sdtlseqdt0(sz0z00,xH)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xE))
| ~ aScalar0(xH) )
| ~ spl2_2
| ~ spl2_14
| spl2_40 ),
inference(forward_subsumption_resolution,[],[f3449,f860]) ).
fof(f4012,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xE))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xE))
| ~ aScalar0(xH) )
| ~ spl2_2
| ~ spl2_9
| ~ spl2_14
| spl2_40 ),
inference(forward_subsumption_resolution,[],[f3998,f280]) ).
fof(f4026,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xE))
| ~ aScalar0(X0)
| ~ aScalar0(xH) )
| ~ spl2_2
| ~ spl2_9
| ~ spl2_13
| ~ spl2_14
| spl2_40 ),
inference(forward_subsumption_resolution,[],[f4012,f407]) ).
fof(f4038,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xE))
| ~ aScalar0(X0) )
| ~ spl2_2
| ~ spl2_9
| ~ spl2_13
| ~ spl2_14
| spl2_40 ),
inference(forward_subsumption_resolution,[],[f4026,f148]) ).
fof(f4051,plain,
( spl2_47
| ~ spl2_2
| ~ spl2_9
| ~ spl2_13
| ~ spl2_14
| spl2_40 ),
inference(avatar_split_clause,[],[f4038,f859,f410,f406,f279,f217,f1070]) ).
fof(f4054,plain,
( ~ sdtlseqdt0(xP,sz0z00)
| sz0z00 = xP
| ~ aScalar0(sz0z00)
| ~ spl2_11 ),
inference(forward_subsumption_resolution,[],[f2591,f152]) ).
fof(f4063,definition,
( spl2_152
<=> sdtlseqdt0(xP,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_152])],[avatar_definition]) ).
fof(f4064,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ spl2_152 ),
inference(avatar_component_clause,[],[f4063]) ).
fof(f4079,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ aScalar0(smndt0(xP))
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f3171,f861]) ).
fof(f4097,plain,
( ~ sdtlseqdt0(xP,sz0z00)
| sz0z00 = xP
| ~ spl2_11 ),
inference(forward_subsumption_resolution,[],[f4054,f196]) ).
fof(f4114,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ spl2_18
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f4079,f432]) ).
fof(f4143,definition,
( spl2_159
<=> sz0z00 = xP ),
introduced(definition,[new_symbols(definition,[spl2_159])],[avatar_definition]) ).
fof(f4145,plain,
( sz0z00 = xP
| ~ spl2_159 ),
inference(avatar_component_clause,[],[f4143]) ).
fof(f4146,plain,
( spl2_159
| ~ spl2_152
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f4097,f302,f4063,f4143]) ).
fof(f4156,plain,
( spl2_152
| ~ spl2_18
| ~ spl2_40 ),
inference(avatar_split_clause,[],[f4114,f859,f430,f4063]) ).
fof(f4211,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xE)
| ~ sdtlseqdt0(sz0z00,xH)
| ~ aScalar0(X0)
| ~ aScalar0(xE)
| ~ aScalar0(xH) )
| spl2_11 ),
inference(forward_subsumption_resolution,[],[f732,f304]) ).
fof(f4216,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xE)
| ~ aScalar0(X0)
| ~ aScalar0(xE)
| ~ aScalar0(xH) )
| ~ spl2_9
| spl2_11 ),
inference(forward_subsumption_resolution,[],[f4211,f280]) ).
fof(f4219,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xE)
| ~ aScalar0(X0)
| ~ aScalar0(xH) )
| ~ spl2_9
| spl2_11 ),
inference(forward_subsumption_resolution,[],[f4216,f142]) ).
fof(f4222,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xE)
| ~ aScalar0(X0) )
| ~ spl2_9
| spl2_11 ),
inference(forward_subsumption_resolution,[],[f4219,f148]) ).
fof(f4224,plain,
( spl2_27
| ~ spl2_9
| spl2_11 ),
inference(avatar_split_clause,[],[f4222,f302,f279,f743]) ).
fof(f4227,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xB))
| ~ aScalar0(X0) )
| ~ spl2_2
| spl2_9
| ~ spl2_136 ),
inference(forward_subsumption_resolution,[],[f3878,f3895]) ).
fof(f4320,plain,
( ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(xB,sz0z00)
| ~ aScalar0(xB)
| ~ spl2_137 ),
inference(resolution,[],[f3899,f1171]) ).
fof(f4327,plain,
( ~ sdtlseqdt0(xB,sz0z00)
| ~ aScalar0(xB)
| ~ spl2_137 ),
inference(forward_subsumption_resolution,[],[f4320,f196]) ).
fof(f4328,plain,
( ~ aScalar0(xB)
| spl2_134
| ~ spl2_137 ),
inference(forward_subsumption_resolution,[],[f4327,f3962]) ).
fof(f4329,plain,
( $false
| spl2_134
| ~ spl2_137 ),
inference(forward_subsumption_resolution,[],[f4328,f136]) ).
fof(f4330,plain,
( spl2_134
| ~ spl2_137 ),
inference(avatar_contradiction_clause,[],[f4329]) ).
fof(f4334,plain,
( ~ aScalar0(xB)
| ~ aScalar0(xB)
| ~ spl2_141 ),
inference(resolution,[],[f3915,f181]) ).
fof(f4337,plain,
( ~ aScalar0(xB)
| ~ spl2_141 ),
inference(duplicate_literal_removal,[],[f4334]) ).
fof(f4340,plain,
( $false
| ~ spl2_141 ),
inference(forward_subsumption_resolution,[],[f4337,f136]) ).
fof(f4341,plain,
~ spl2_141,
inference(avatar_contradiction_clause,[],[f4340]) ).
fof(f4344,plain,
( spl2_137
| ~ spl2_2
| spl2_9
| ~ spl2_136 ),
inference(avatar_split_clause,[],[f4227,f3894,f279,f217,f3898]) ).
fof(f4349,plain,
( ~ aScalar0(xA)
| ~ aScalar0(xA)
| ~ spl2_142 ),
inference(resolution,[],[f3919,f181]) ).
fof(f4352,plain,
( ~ aScalar0(xA)
| ~ spl2_142 ),
inference(duplicate_literal_removal,[],[f4349]) ).
fof(f4356,plain,
( $false
| ~ spl2_142 ),
inference(forward_subsumption_resolution,[],[f4352,f134]) ).
fof(f4357,plain,
~ spl2_142,
inference(avatar_contradiction_clause,[],[f4356]) ).
fof(f4361,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,xN)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,sz0z00)
| ~ sdtlseqdt0(xP,X0) )
| ~ spl2_12 ),
inference(duplicate_literal_removal,[],[f2597]) ).
fof(f4373,plain,
( ! [X0] :
( ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,sz0z00)
| ~ sdtlseqdt0(xP,X0) )
| ~ spl2_12
| ~ spl2_35 ),
inference(forward_subsumption_resolution,[],[f4361,f839]) ).
fof(f4409,plain,
( ! [X0] :
( ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,sz0z00)
| ~ sdtlseqdt0(xP,X0) )
| ~ spl2_12
| ~ spl2_35 ),
inference(forward_subsumption_resolution,[],[f4373,f196]) ).
fof(f4432,plain,
( ! [X0] :
( ~ aScalar0(X0)
| ~ sdtlseqdt0(xP,X0) )
| ~ spl2_12
| ~ spl2_35
| ~ spl2_152 ),
inference(forward_subsumption_resolution,[],[f4409,f4064]) ).
fof(f4449,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) )
| ~ spl2_12
| ~ spl2_35
| ~ spl2_152
| ~ spl2_159 ),
inference(forward_demodulation,[],[f4432,f4145]) ).
fof(f4465,plain,
( spl2_93
| ~ spl2_12
| ~ spl2_35
| ~ spl2_152
| ~ spl2_159 ),
inference(avatar_split_clause,[],[f4449,f4143,f4063,f837,f306,f2325]) ).
fof(f4488,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xR)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) )
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f734,f838]) ).
fof(f4510,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) )
| ~ spl2_5
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f4488,f238]) ).
fof(f4528,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| ~ spl2_5
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f4510,f150]) ).
fof(f4558,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0) )
| ~ spl2_5
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f4528,f154]) ).
fof(f4605,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xR)
| ~ spl2_5
| spl2_35 ),
inference(resolution,[],[f4558,f181]) ).
fof(f4608,plain,
( ~ aScalar0(xR)
| ~ spl2_5
| spl2_35 ),
inference(duplicate_literal_removal,[],[f4605]) ).
fof(f4611,plain,
( $false
| ~ spl2_5
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f4608,f150]) ).
fof(f4612,plain,
( ~ spl2_5
| spl2_35 ),
inference(avatar_contradiction_clause,[],[f4611]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f219]) ).
cnf(s6,plain,
spl2_7,
inference(sat_conversion,[],[f270]) ).
cnf(s8,plain,
( ~ spl2_7
| ~ spl2_11
| spl2_12 ),
inference(sat_conversion,[],[f308]) ).
cnf(s14,plain,
( ~ spl2_13
| spl2_18 ),
inference(sat_conversion,[],[f433]) ).
cnf(s17,plain,
( ~ spl2_2
| ~ spl2_13
| spl2_14 ),
inference(sat_conversion,[],[f439]) ).
cnf(s27,plain,
spl2_20,
inference(sat_conversion,[],[f576]) ).
cnf(s28,plain,
spl2_13,
inference(sat_conversion,[],[f578]) ).
cnf(s30,plain,
~ spl2_27,
inference(sat_conversion,[],[f757]) ).
cnf(s43,plain,
( spl2_35
| ~ spl2_49
| spl2_50 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s47,plain,
( ~ spl2_13
| ~ spl2_47 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s86,plain,
~ spl2_1,
inference(sat_conversion,[],[f1884]) ).
cnf(s118,plain,
~ spl2_93,
inference(sat_conversion,[],[f2399]) ).
cnf(s135,plain,
( spl2_5
| spl2_49 ),
inference(sat_conversion,[],[f2823]) ).
cnf(s137,plain,
( ~ spl2_20
| ~ spl2_50 ),
inference(sat_conversion,[],[f2854]) ).
cnf(s164,plain,
( ~ spl2_2
| spl2_9
| ~ spl2_140
| spl2_141 ),
inference(sat_conversion,[],[f3916]) ).
cnf(s165,plain,
( spl2_9
| ~ spl2_134
| spl2_142 ),
inference(sat_conversion,[],[f3920]) ).
cnf(s171,plain,
( spl2_136
| spl2_140 ),
inference(sat_conversion,[],[f3987]) ).
cnf(s174,plain,
( ~ spl2_2
| ~ spl2_9
| ~ spl2_13
| ~ spl2_14
| spl2_40
| spl2_47 ),
inference(sat_conversion,[],[f4051]) ).
cnf(s185,plain,
( ~ spl2_11
| ~ spl2_152
| spl2_159 ),
inference(sat_conversion,[],[f4146]) ).
cnf(s189,plain,
( ~ spl2_18
| ~ spl2_40
| spl2_152 ),
inference(sat_conversion,[],[f4156]) ).
cnf(s209,plain,
( ~ spl2_9
| spl2_11
| spl2_27 ),
inference(sat_conversion,[],[f4224]) ).
cnf(s212,plain,
( spl2_134
| ~ spl2_137 ),
inference(sat_conversion,[],[f4330]) ).
cnf(s213,plain,
~ spl2_141,
inference(sat_conversion,[],[f4341]) ).
cnf(s214,plain,
( ~ spl2_2
| spl2_9
| ~ spl2_136
| spl2_137 ),
inference(sat_conversion,[],[f4344]) ).
cnf(s215,plain,
~ spl2_142,
inference(sat_conversion,[],[f4357]) ).
cnf(s222,plain,
( ~ spl2_12
| ~ spl2_35
| spl2_93
| ~ spl2_152
| ~ spl2_159 ),
inference(sat_conversion,[],[f4465]) ).
cnf(s244,plain,
( ~ spl2_5
| spl2_35 ),
inference(sat_conversion,[],[f4612]) ).
cnf(s245,plain,
( spl2_9
| ~ spl2_134 ),
inference(rat,[],[s165,s215]) ).
cnf(s246,plain,
( ~ spl2_2
| spl2_9
| ~ spl2_140 ),
inference(rat,[],[s164,s213]) ).
cnf(s278,plain,
~ spl2_47,
inference(rat,[],[s47,s28]) ).
cnf(s280,plain,
~ spl2_50,
inference(rat,[],[s137,s27]) ).
cnf(s290,plain,
( ~ spl2_2
| spl2_14 ),
inference(rat,[],[s17,s28]) ).
cnf(s293,plain,
spl2_18,
inference(rat,[],[s14,s28]) ).
cnf(s303,plain,
spl2_2,
inference(rat,[],[s1,s86]) ).
cnf(s305,plain,
spl2_14,
inference(rat,[],[s290,s303]) ).
cnf(s306,plain,
spl2_9,
inference(rat,[],[s214,s171,s212,s246,s245,s303]) ).
cnf(s307,plain,
spl2_11,
inference(rat,[],[s209,s30,s306]) ).
cnf(s308,plain,
spl2_40,
inference(rat,[],[s174,s278,s305,s303,s28,s306]) ).
cnf(s311,plain,
spl2_12,
inference(rat,[],[s8,s6,s307]) ).
cnf(s312,plain,
spl2_152,
inference(rat,[],[s189,s293,s308]) ).
cnf(s315,plain,
spl2_159,
inference(rat,[],[s185,s307,s312]) ).
cnf(s317,plain,
~ spl2_35,
inference(rat,[],[s222,s311,s312,s118,s315]) ).
cnf(s319,plain,
~ spl2_5,
inference(rat,[],[s244,s317]) ).
cnf(s323,plain,
~ spl2_49,
inference(rat,[],[s43,s280,s317]) ).
cnf(s324,plain,
$false,
inference(rat,[],[s135,s323,s319]) ).
fof(f4614,plain,
$false,
inference(avatar_sat_refutation,[],[s324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG054+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.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 23:02:31 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.42 Running first-order theorem proving
% 0.14/0.42 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
% 17.65/3.50 % (1275266)Detected formulas, will run a generic FOF schedule.
% 17.65/3.50 % (1275294)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=2758681668:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 17.65/3.50 % (1275293)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=2237197832:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 17.65/3.50 % (1275296)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2223196742:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 17.65/3.50 % (1275298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2928126526:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 17.65/3.50 % (1275299)dis-21_1_sil=8000:lcm=predicate:random_seed=3212956671: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)
% 17.65/3.50 % (1275297)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=844989953:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 17.65/3.50 % (1275295)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=3302071195:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 17.65/3.50 % (1275296)Instruction limit reached!
% 17.65/3.50 % (1275296)------------------------------
% 17.65/3.50 % (1275296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/3.50 % (1275296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/3.50 % (1275296)CaDiCaL version: 2.1.3
% 17.65/3.50 % (1275296)Termination reason: Instruction limit
% 17.65/3.50 % (1275296)Termination phase: Saturation
% 17.65/3.50 % (1275296)Time elapsed: 0.078 s
% 17.65/3.50 % (1275296)Peak memory usage: 89 MB
% 17.65/3.50 % (1275296)Instructions burned: 109 (million)
% 17.65/3.50 % (1275297)Instruction limit reached!
% 17.65/3.50 % (1275297)------------------------------
% 17.65/3.50 % (1275297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/3.50 % (1275297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/3.50 % (1275297)CaDiCaL version: 2.1.3
% 17.65/3.50 % (1275297)Termination reason: Instruction limit
% 17.65/3.50 % (1275297)Termination phase: Saturation
% 17.65/3.50 % (1275297)Time elapsed: 0.104 s
% 17.65/3.50 % (1275297)Peak memory usage: 88 MB
% 17.65/3.50 % (1275297)Instructions burned: 119 (million)
% 17.65/3.50 % (1275299)Instruction limit reached!
% 17.65/3.50 % (1275299)------------------------------
% 17.65/3.50 % (1275299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/3.50 % (1275299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/3.50 % (1275299)CaDiCaL version: 2.1.3
% 17.65/3.50 % (1275299)Termination reason: Instruction limit
% 17.65/3.50 % (1275299)Termination phase: Saturation
% 17.65/3.50 % (1275299)Time elapsed: 0.112 s
% 17.65/3.50 % (1275299)Peak memory usage: 89 MB
% 17.65/3.50 % (1275299)Instructions burned: 130 (million)
% 17.65/3.50 % (1275298)Instruction limit reached!
% 17.65/3.50 % (1275298)------------------------------
% 17.65/3.50 % (1275298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/3.50 % (1275298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/3.50 % (1275298)CaDiCaL version: 2.1.3
% 17.65/3.50 % (1275298)Termination reason: Instruction limit
% 17.65/3.50 % (1275298)Termination phase: Saturation
% 17.65/3.50 % (1275298)Time elapsed: 0.146 s
% 17.65/3.50 % (1275298)Peak memory usage: 90 MB
% 17.65/3.50 % (1275298)Instructions burned: 140 (million)
% 17.65/3.50 % (1275312)lrs+10_1_sil=8000:sp=occurrence:random_seed=3868324205:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 17.65/3.50 % (1275314)lrs+10_1_sil=32000:urr=on:br=off:random_seed=870380558:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 17.65/3.50 % (1275315)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1181114859:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 17.65/3.50 % (1275316)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=2882440426:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 17.65/3.50 % (1275314)Instruction limit reached!
% 17.99/3.82 % (1275314)------------------------------
% 17.99/3.82 % (1275314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275314)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275314)Termination reason: Instruction limit
% 17.99/3.82 % (1275314)Termination phase: Saturation
% 17.99/3.82 % (1275314)Time elapsed: 0.132 s
% 17.99/3.82 % (1275314)Peak memory usage: 90 MB
% 17.99/3.82 % (1275314)Instructions burned: 157 (million)
% 17.99/3.82 % (1275312)Instruction limit reached!
% 17.99/3.82 % (1275312)------------------------------
% 17.99/3.82 % (1275312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275312)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275312)Termination reason: Instruction limit
% 17.99/3.82 % (1275312)Termination phase: Saturation
% 17.99/3.82 % (1275312)Time elapsed: 0.285 s
% 17.99/3.82 % (1275312)Peak memory usage: 93 MB
% 17.99/3.82 % (1275312)Instructions burned: 285 (million)
% 17.99/3.82 % (1275316)Instruction limit reached!
% 17.99/3.82 % (1275316)------------------------------
% 17.99/3.82 % (1275316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275316)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275316)Termination reason: Instruction limit
% 17.99/3.82 % (1275316)Termination phase: Saturation
% 17.99/3.82 % (1275316)Time elapsed: 0.211 s
% 17.99/3.82 % (1275316)Peak memory usage: 95 MB
% 17.99/3.82 % (1275316)Instructions burned: 248 (million)
% 17.99/3.82 % (1275323)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3980035384:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 17.99/3.82 % (1275315)Instruction limit reached!
% 17.99/3.82 % (1275315)------------------------------
% 17.99/3.82 % (1275315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275315)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275315)Termination reason: Instruction limit
% 17.99/3.82 % (1275315)Termination phase: Saturation
% 17.99/3.82 % (1275315)Time elapsed: 0.328 s
% 17.99/3.82 % (1275315)Peak memory usage: 94 MB
% 17.99/3.82 % (1275315)Instructions burned: 327 (million)
% 17.99/3.82 % (1275324)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=730354849:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 17.99/3.82 % (1275323)Instruction limit reached!
% 17.99/3.82 % (1275323)------------------------------
% 17.99/3.82 % (1275323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275323)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275323)Termination reason: Instruction limit
% 17.99/3.82 % (1275323)Termination phase: Saturation
% 17.99/3.82 % (1275323)Time elapsed: 0.157 s
% 17.99/3.82 % (1275323)Peak memory usage: 91 MB
% 17.99/3.82 % (1275323)Instructions burned: 295 (million)
% 17.99/3.82 % (1275326)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2829667182:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 17.99/3.82 % (1275326)Instruction limit reached!
% 17.99/3.82 % (1275326)------------------------------
% 17.99/3.82 % (1275326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275326)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275326)Termination reason: Instruction limit
% 17.99/3.82 % (1275326)Termination phase: Saturation
% 17.99/3.82 % (1275326)Time elapsed: 0.118 s
% 17.99/3.82 % (1275326)Peak memory usage: 91 MB
% 17.99/3.82 % (1275326)Instructions burned: 113 (million)
% 17.99/3.82 % (1275328)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1159026443:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.99/3.82 % (1275330)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=765432100:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 17.99/3.82 % (1275328)Instruction limit reached!
% 17.99/3.82 % (1275328)------------------------------
% 17.99/3.82 % (1275328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275328)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275328)Termination reason: Instruction limit
% 17.99/3.82 % (1275328)Termination phase: Saturation
% 17.99/3.82 % (1275328)Time elapsed: 0.071 s
% 17.99/3.82 % (1275328)Peak memory usage: 89 MB
% 17.99/3.82 % (1275328)Instructions burned: 128 (million)
% 17.99/3.82 % (1275330)Instruction limit reached!
% 17.99/3.82 % (1275330)------------------------------
% 17.99/3.82 % (1275330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275330)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275330)Termination reason: Instruction limit
% 17.99/3.82 % (1275330)Termination phase: Saturation
% 17.99/3.82 % (1275330)Time elapsed: 0.116 s
% 17.99/3.82 % (1275330)Peak memory usage: 89 MB
% 17.99/3.82 % (1275330)Instructions burned: 115 (million)
% 17.99/3.82 % (1275334)lrs+10_1_sil=8000:sp=occurrence:random_seed=2389114628:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 17.99/3.82 % (1275337)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=379097025:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 17.99/3.82 % (1275339)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2661122095:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 17.99/3.82 % (1275337)Instruction limit reached!
% 17.99/3.82 % (1275337)------------------------------
% 17.99/3.82 % (1275337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275337)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275337)Termination reason: Instruction limit
% 17.99/3.82 % (1275337)Termination phase: Saturation
% 17.99/3.82 % (1275337)Time elapsed: 0.391 s
% 17.99/3.82 % (1275337)Peak memory usage: 95 MB
% 17.99/3.82 % (1275337)Instructions burned: 437 (million)
% 17.99/3.82 % (1275345)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3054305017:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 17.99/3.82 % (1275345)Instruction limit reached!
% 17.99/3.82 % (1275345)------------------------------
% 17.99/3.82 % (1275345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275345)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275345)Termination reason: Instruction limit
% 17.99/3.82 % (1275345)Termination phase: Saturation
% 17.99/3.82 % (1275345)Time elapsed: 0.059 s
% 17.99/3.82 % (1275345)Peak memory usage: 91 MB
% 17.99/3.82 % (1275345)Instructions burned: 134 (million)
% 17.99/3.82 % (1275334)Instruction limit reached!
% 17.99/3.82 % (1275334)------------------------------
% 17.99/3.82 % (1275334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275334)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275334)Termination reason: Instruction limit
% 17.99/3.82 % (1275334)Termination phase: Saturation
% 17.99/3.82 % (1275334)Time elapsed: 0.672 s
% 17.99/3.82 % (1275334)Peak memory usage: 103 MB
% 17.99/3.82 % (1275334)Instructions burned: 909 (million)
% 17.99/3.82 % (1275348)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=100835262:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 17.99/3.82 % (1275349)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=401786699:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 17.99/3.82 % (1275348)Instruction limit reached!
% 17.99/3.82 % (1275348)------------------------------
% 17.99/3.82 % (1275348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275348)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275348)Termination reason: Instruction limit
% 17.99/3.82 % (1275348)Termination phase: Saturation
% 17.99/3.82 % (1275348)Time elapsed: 0.252 s
% 17.99/3.82 % (1275348)Peak memory usage: 90 MB
% 17.99/3.82 % (1275348)Instructions burned: 594 (million)
% 17.99/3.82 % (1275446)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=1049699219:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 17.99/3.82 % (1275339)First to succeed.
% 17.99/3.82 % (1275339)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1275266"
% 17.99/3.82 % (1275446)Instruction limit reached!
% 17.99/3.82 % (1275446)------------------------------
% 17.99/3.82 % (1275446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275446)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275446)Termination reason: Instruction limit
% 17.99/3.82 % (1275446)Termination phase: Saturation
% 17.99/3.82 % (1275446)Time elapsed: 0.065 s
% 17.99/3.82 % (1275446)Peak memory usage: 91 MB
% 17.99/3.82 % (1275446)Instructions burned: 125 (million)
% 17.99/3.82 % (1275479)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=676876362:i=134:gtgl=5:slsql=off:gtg=exists_sym_2974 on theBenchmark for (2974ds/134Mi)
% 17.99/3.82 % (1275324)Instruction limit reached!
% 17.99/3.82 % (1275324)------------------------------
% 17.99/3.82 % (1275324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275324)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275324)Termination reason: Instruction limit
% 17.99/3.82 % (1275324)Termination phase: Saturation
% 17.99/3.82 % (1275324)Time elapsed: 1.778 s
% 17.99/3.82 % (1275324)Peak memory usage: 143 MB
% 17.99/3.82 % (1275324)Instructions burned: 2350 (million)
% 17.99/3.82 % (1275479)Instruction limit reached!
% 17.99/3.82 % (1275479)------------------------------
% 17.99/3.82 % (1275479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.82 % (1275479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.82 % (1275479)CaDiCaL version: 2.1.3
% 17.99/3.82 % (1275479)Termination reason: Instruction limit
% 17.99/3.82 % (1275479)Termination phase: Saturation
% 17.99/3.82 % (1275479)Time elapsed: 0.070 s
% 17.99/3.82 % (1275479)Peak memory usage: 91 MB
% 17.99/3.82 % (1275479)Instructions burned: 136 (million)
% 17.99/3.82 % (1275339)Refutation found. Thanks to Tanya!
% 17.99/3.82 % SZS status Theorem for theBenchmark
% 17.99/3.82 % SZS output start Proof for theBenchmark
% See solution above
% 20.62/4.02 % (1275339)------------------------------
% 20.62/4.02 % (1275339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/4.02 % (1275339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/4.02 % (1275339)CaDiCaL version: 2.1.3
% 20.62/4.02 % (1275339)Termination reason: Refutation
% 20.62/4.02 % (1275339)Time elapsed: 1.040 s
% 20.62/4.02 % (1275339)Peak memory usage: 135 MB
% 20.62/4.02 % (1275339)Instructions burned: 1451 (million)
% 20.62/4.02 % (1275339)------------------------------
% 20.62/4.02 % (1275339)------------------------------
% 20.62/4.02 % (1275266)Success in time 2.831 s
% 20.62/4.02 % Vampire exiting
%------------------------------------------------------------------------------