%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG075+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:24 PM UTC 2026
% Result : Theorem 72.32s 16.62s
% Output : Refutation 112.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 78
% Syntax : Number of formulae : 438 ( 82 unt; 47 def)
% Number of atoms : 1476 ( 112 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1964 ( 926 ~; 904 |; 64 &)
% ( 47 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 48 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 14 con; 0-2 aty)
% Number of variables : 323 ( 0 sgn 323 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f10,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSumSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',mMNeg) ).
fof(f18,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMDNeg) ).
fof(f20,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLERef) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',mLEMonM) ).
fof(f25,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETot) ).
fof(f26,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(sz0z00,X0)
& sdtlseqdt0(sz0z00,X1) )
=> ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPosMon) ).
fof(f27,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSqPos) ).
fof(f34,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( aDimensionOf0(X0) = aDimensionOf0(X1)
=> aScalar0(sdtasasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScPr) ).
fof(f36,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( ( aDimensionOf0(X0) = aDimensionOf0(X1)
& aDimensionOf0(X1) != sz00 )
=> sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSPN) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScSqPos) ).
fof(f38,axiom,
( aVector0(xs)
& aVector0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678) ).
fof(f41,axiom,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1692) ).
fof(f42,axiom,
( aVector0(xp)
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1709) ).
fof(f43,axiom,
( aVector0(xq)
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1726) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1746) ).
fof(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1766) ).
fof(f46,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1783) ).
fof(f47,axiom,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1800) ).
fof(f48,axiom,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1820) ).
fof(f49,axiom,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1837) ).
fof(f50,axiom,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1854) ).
fof(f51,axiom,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1873) ).
fof(f58,conjecture,
sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f59,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f65,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(flattening,[],[f59]) ).
fof(f72,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f73,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f75,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f77,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(f78,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(f79,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,[],[f78]) ).
fof(f84,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(f85,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,[],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f87,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f86]) ).
fof(f88,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f91,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f92,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f91]) ).
fof(f93,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(f94,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,[],[f93]) ).
fof(f95,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(f96,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,[],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f98,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) )
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f100,plain,
! [X0,X1] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) )
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f111,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f112,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f111]) ).
fof(f115,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f36]) ).
fof(f116,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f132,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f133,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f134,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f135,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f137,plain,
! [X0] :
( smndt0(smndt0(X0)) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f138,plain,
! [X0] :
( sz0z00 = sdtpldt0(smndt0(X0),X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f140,plain,
! [X0] :
( sz0z00 = sdtasdt0(sz0z00,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f142,plain,
! [X0] :
( sdtpldt0(sz0z00,X0) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f143,plain,
! [X0] :
( sdtpldt0(X0,sz0z00) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f144,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f79]) ).
fof(f146,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f79]) ).
fof(f152,plain,
! [X0,X1] :
( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(smndt0(X0),smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f154,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f88]) ).
fof(f156,plain,
! [X2,X0,X1] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f92]) ).
fof(f157,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,[],[f94]) ).
fof(f158,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,[],[f96]) ).
fof(f159,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f160,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f161,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f162,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f172,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f174,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(cnf_transformation,[],[f116]) ).
fof(f175,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f177,plain,
aVector0(xs),
inference(cnf_transformation,[],[f38]) ).
fof(f180,plain,
sz00 != aDimensionOf0(xs),
inference(cnf_transformation,[],[f41]) ).
fof(f181,plain,
xp = sziznziztdt0(xs),
inference(cnf_transformation,[],[f42]) ).
fof(f184,plain,
aVector0(xq),
inference(cnf_transformation,[],[f43]) ).
fof(f185,plain,
xA = sdtlbdtrb0(xs,aDimensionOf0(xs)),
inference(cnf_transformation,[],[f44]) ).
fof(f188,plain,
aScalar0(xB),
inference(cnf_transformation,[],[f45]) ).
fof(f189,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[],[f46]) ).
fof(f190,plain,
aScalar0(xC),
inference(cnf_transformation,[],[f46]) ).
fof(f191,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[],[f47]) ).
fof(f192,plain,
aScalar0(xD),
inference(cnf_transformation,[],[f47]) ).
fof(f194,plain,
aScalar0(xE),
inference(cnf_transformation,[],[f48]) ).
fof(f195,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[],[f49]) ).
fof(f197,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[],[f50]) ).
fof(f198,plain,
aScalar0(xG),
inference(cnf_transformation,[],[f50]) ).
fof(f200,plain,
aScalar0(xH),
inference(cnf_transformation,[],[f51]) ).
fof(f211,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(cnf_transformation,[],[f65]) ).
fof(f215,plain,
! [X2] :
( ~ aScalar0(X2)
| sP2 ),
inference(cnf_transformation,[],[f215_D]) ).
fof(f215_D,definition,
( ! [X2] : ~ aScalar0(X2)
<=> ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[general_splitting_component_introduction]) ).
fof(f216,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sP2 ),
inference(general_splitting,[],[f146,f215_D]) ).
fof(f217,plain,
! [X2] :
( ~ aScalar0(X2)
| sP3 ),
inference(cnf_transformation,[],[f217_D]) ).
fof(f217_D,definition,
( ! [X2] : ~ aScalar0(X2)
<=> ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[general_splitting_component_introduction]) ).
fof(f218,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sP3 ),
inference(general_splitting,[],[f144,f217_D]) ).
fof(f220,definition,
( spl4_1
<=> sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f222,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| spl4_1 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
~ spl4_1,
inference(avatar_split_clause,[],[f211,f220]) ).
fof(f227,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(X0,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ aScalar0(X0)
| ~ aScalar0(sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) )
| spl4_1 ),
inference(resolution,[],[f222,f156]) ).
fof(f390,definition,
( spl4_5
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f392,plain,
( aScalar0(xC)
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,plain,
spl4_5,
inference(avatar_split_clause,[],[f190,f390]) ).
fof(f452,plain,
( sP2
| ~ spl4_5 ),
inference(resolution,[],[f392,f215]) ).
fof(f455,plain,
( sP3
| ~ spl4_5 ),
inference(resolution,[],[f392,f217]) ).
fof(f460,plain,
( ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_5 ),
inference(backward_subsumption_resolution,[],[f218,f455]) ).
fof(f463,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_5 ),
inference(backward_subsumption_resolution,[],[f216,f452]) ).
fof(f465,definition,
( spl4_6
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f467,plain,
( aScalar0(xD)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f468,plain,
spl4_6,
inference(avatar_split_clause,[],[f192,f465]) ).
fof(f534,definition,
( spl4_8
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f536,plain,
( aScalar0(xE)
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,plain,
spl4_8,
inference(avatar_split_clause,[],[f194,f534]) ).
fof(f664,definition,
( spl4_10
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f666,plain,
( aScalar0(xG)
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
spl4_10,
inference(avatar_split_clause,[],[f198,f664]) ).
fof(f729,definition,
( spl4_11
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f731,plain,
( aScalar0(xH)
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f732,plain,
spl4_11,
inference(avatar_split_clause,[],[f200,f729]) ).
fof(f798,definition,
( spl4_13
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f799,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f800,plain,
( spl4_13
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f463,f390,f798]) ).
fof(f832,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtpldt0(X2,X3),sdtpldt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X3,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X3)
| ~ aScalar0(X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_13 ),
inference(superposition,[],[f157,f799]) ).
fof(f848,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtpldt0(X2,X3),sdtpldt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X3,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X3)
| ~ aScalar0(X0) )
| ~ spl4_13 ),
inference(duplicate_literal_removal,[],[f832]) ).
fof(f898,definition,
( spl4_14
<=> ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f899,plain,
( ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f900,plain,
( spl4_14
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f460,f390,f898]) ).
fof(f944,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X2,X3))
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X0,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_14 ),
inference(superposition,[],[f158,f899]) ).
fof(f958,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X2,X3))
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X0,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X3) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f944]) ).
fof(f1958,definition,
( spl4_25
<=> aScalar0(xB) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f1960,plain,
( aScalar0(xB)
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f1958]) ).
fof(f1961,plain,
spl4_25,
inference(avatar_split_clause,[],[f188,f1958]) ).
fof(f2017,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(xB,xB))
| ~ spl4_25 ),
inference(resolution,[],[f1960,f162]) ).
fof(f2024,plain,
( sdtlseqdt0(sz0z00,xG)
| ~ spl4_25 ),
inference(forward_demodulation,[],[f2017,f197]) ).
fof(f2433,definition,
( spl4_30
<=> sdtlseqdt0(sz0z00,xG) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f2435,plain,
( sdtlseqdt0(sz0z00,xG)
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f2433]) ).
fof(f2436,plain,
( spl4_30
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f2024,f1958,f2433]) ).
fof(f2998,definition,
( spl4_36
<=> ! [X0,X3,X2,X1] :
( sdtlseqdt0(sdtpldt0(X2,X3),sdtpldt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X3,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X3)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_36])],[avatar_definition]) ).
fof(f2999,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtpldt0(X2,X3),sdtpldt0(X0,X1))
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X3,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X3)
| ~ aScalar0(X0) )
| ~ spl4_36 ),
inference(avatar_component_clause,[],[f2998]) ).
fof(f3000,plain,
( spl4_36
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f848,f798,f2998]) ).
fof(f3011,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(X0,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_36 ),
inference(superposition,[],[f2999,f143]) ).
fof(f3025,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_36 ),
inference(superposition,[],[f2999,f138]) ).
fof(f3058,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_36 ),
inference(duplicate_literal_removal,[],[f3025]) ).
fof(f3064,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(X0,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X1) )
| ~ spl4_36 ),
inference(duplicate_literal_removal,[],[f3011]) ).
fof(f3079,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_36 ),
inference(forward_subsumption_resolution,[],[f3058,f135]) ).
fof(f3090,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(X0,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1) )
| ~ spl4_36 ),
inference(forward_subsumption_resolution,[],[f3064,f132]) ).
fof(f3120,definition,
( spl4_37
<=> ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f3121,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_37 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f3122,plain,
( spl4_37
| ~ spl4_36 ),
inference(avatar_split_clause,[],[f3079,f2998,f3120]) ).
fof(f3147,plain,
( ! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0) )
| ~ spl4_37 ),
inference(superposition,[],[f3121,f142]) ).
fof(f3165,plain,
( ! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00) )
| ~ spl4_37 ),
inference(duplicate_literal_removal,[],[f3147]) ).
fof(f3181,plain,
( ! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_37 ),
inference(forward_subsumption_resolution,[],[f3165,f132]) ).
fof(f3711,definition,
( spl4_46
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f3713,plain,
( aVector0(xs)
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f3711]) ).
fof(f3714,plain,
spl4_46,
inference(avatar_split_clause,[],[f177,f3711]) ).
fof(f3728,plain,
( ! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| sz00 = aDimensionOf0(xs)
| ~ aVector0(X0) )
| ~ spl4_46 ),
inference(resolution,[],[f3713,f174]) ).
fof(f3736,plain,
( ! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) )
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f3728,f180]) ).
fof(f3745,plain,
( ! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) )
| ~ spl4_46 ),
inference(forward_demodulation,[],[f3736,f185]) ).
fof(f3750,plain,
( ! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) )
| ~ spl4_46 ),
inference(forward_demodulation,[],[f3745,f181]) ).
fof(f3752,definition,
( spl4_47
<=> ! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f3753,plain,
( ! [X0] :
( aDimensionOf0(X0) != aDimensionOf0(xs)
| sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xp),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xA))
| ~ aVector0(X0) )
| ~ spl4_47 ),
inference(avatar_component_clause,[],[f3752]) ).
fof(f3754,plain,
( spl4_47
| ~ spl4_46 ),
inference(avatar_split_clause,[],[f3750,f3711,f3752]) ).
fof(f4304,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))
| ~ aVector0(xs)
| ~ spl4_47 ),
inference(equality_resolution,[],[f3753]) ).
fof(f4312,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xA))
| ~ spl4_46
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f4304,f3713]) ).
fof(f4321,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),sdtasdt0(xA,xA))
| ~ spl4_46
| ~ spl4_47 ),
inference(forward_demodulation,[],[f4312,f185]) ).
fof(f4329,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xp),xF)
| ~ spl4_46
| ~ spl4_47 ),
inference(forward_demodulation,[],[f4321,f195]) ).
fof(f4331,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(xp,xp),xF)
| ~ spl4_46
| ~ spl4_47 ),
inference(forward_demodulation,[],[f4329,f181]) ).
fof(f4332,plain,
( sdtpldt0(xC,xF) = sdtasasdt0(xs,xs)
| ~ spl4_46
| ~ spl4_47 ),
inference(forward_demodulation,[],[f4331,f189]) ).
fof(f4334,definition,
( spl4_53
<=> sdtpldt0(xC,xF) = sdtasasdt0(xs,xs) ),
introduced(definition,[new_symbols(definition,[spl4_53])],[avatar_definition]) ).
fof(f4336,plain,
( sdtpldt0(xC,xF) = sdtasasdt0(xs,xs)
| ~ spl4_53 ),
inference(avatar_component_clause,[],[f4334]) ).
fof(f4337,plain,
( spl4_53
| ~ spl4_46
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f4332,f3752,f3711,f4334]) ).
fof(f4340,plain,
( aScalar0(sdtpldt0(xC,xF))
| aDimensionOf0(xs) != aDimensionOf0(xs)
| ~ aVector0(xs)
| ~ aVector0(xs)
| ~ spl4_53 ),
inference(superposition,[],[f172,f4336]) ).
fof(f4341,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xC,xF))
| ~ aVector0(xs)
| ~ spl4_53 ),
inference(superposition,[],[f175,f4336]) ).
fof(f4342,plain,
( aScalar0(sdtpldt0(xC,xF))
| aDimensionOf0(xs) != aDimensionOf0(xs)
| ~ aVector0(xs)
| ~ spl4_53 ),
inference(duplicate_literal_removal,[],[f4340]) ).
fof(f4343,plain,
( aScalar0(sdtpldt0(xC,xF))
| ~ aVector0(xs)
| ~ spl4_53 ),
inference(trivial_inequality_removal,[],[f4342]) ).
fof(f4348,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xC,xF))
| ~ spl4_46
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f4341,f3713]) ).
fof(f4349,plain,
( aScalar0(sdtpldt0(xC,xF))
| ~ spl4_46
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f4343,f3713]) ).
fof(f4352,definition,
( spl4_54
<=> aScalar0(sdtpldt0(xC,xF)) ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f4354,plain,
( aScalar0(sdtpldt0(xC,xF))
| ~ spl4_54 ),
inference(avatar_component_clause,[],[f4352]) ).
fof(f4355,plain,
( spl4_54
| ~ spl4_46
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f4349,f4334,f3711,f4352]) ).
fof(f4453,definition,
( spl4_56
<=> sdtlseqdt0(sz0z00,sdtpldt0(xC,xF)) ),
introduced(definition,[new_symbols(definition,[spl4_56])],[avatar_definition]) ).
fof(f4455,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xC,xF))
| ~ spl4_56 ),
inference(avatar_component_clause,[],[f4453]) ).
fof(f4456,plain,
( spl4_56
| ~ spl4_46
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f4348,f4334,f3711,f4453]) ).
fof(f11091,definition,
( spl4_88
<=> aVector0(xq) ),
introduced(definition,[new_symbols(definition,[spl4_88])],[avatar_definition]) ).
fof(f11093,plain,
( aVector0(xq)
| ~ spl4_88 ),
inference(avatar_component_clause,[],[f11091]) ).
fof(f11094,plain,
spl4_88,
inference(avatar_split_clause,[],[f184,f11091]) ).
fof(f11109,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(xq,xq))
| ~ spl4_88 ),
inference(resolution,[],[f11093,f175]) ).
fof(f11113,plain,
( sdtlseqdt0(sz0z00,xD)
| ~ spl4_88 ),
inference(forward_demodulation,[],[f11109,f191]) ).
fof(f11131,definition,
( spl4_89
<=> sdtlseqdt0(sz0z00,xD) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f11133,plain,
( sdtlseqdt0(sz0z00,xD)
| ~ spl4_89 ),
inference(avatar_component_clause,[],[f11131]) ).
fof(f11134,plain,
( spl4_89
| ~ spl4_88 ),
inference(avatar_split_clause,[],[f11113,f11091,f11131]) ).
fof(f12329,definition,
( spl4_100
<=> ! [X0,X3,X2,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X2,X3))
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X0,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X3) ) ),
introduced(definition,[new_symbols(definition,[spl4_100])],[avatar_definition]) ).
fof(f12330,plain,
( ! [X2,X3,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X2,X3))
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X0,X3)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X3) )
| ~ spl4_100 ),
inference(avatar_component_clause,[],[f12329]) ).
fof(f12331,plain,
( spl4_100
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f958,f898,f12329]) ).
fof(f12356,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) )
| ~ spl4_100 ),
inference(superposition,[],[f12330,f140]) ).
fof(f12453,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) )
| ~ spl4_100 ),
inference(duplicate_literal_removal,[],[f12356]) ).
fof(f12505,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) )
| ~ spl4_100 ),
inference(forward_subsumption_resolution,[],[f12453,f154]) ).
fof(f12534,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) )
| ~ spl4_100 ),
inference(forward_subsumption_resolution,[],[f12505,f132]) ).
fof(f12546,definition,
( spl4_101
<=> ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ) ),
introduced(definition,[new_symbols(definition,[spl4_101])],[avatar_definition]) ).
fof(f12547,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) )
| ~ spl4_101 ),
inference(avatar_component_clause,[],[f12546]) ).
fof(f12548,plain,
( spl4_101
| ~ spl4_100 ),
inference(avatar_split_clause,[],[f12534,f12329,f12546]) ).
fof(f12591,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) )
| ~ spl4_101 ),
inference(superposition,[],[f12547,f153]) ).
fof(f12630,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) )
| ~ spl4_101 ),
inference(forward_subsumption_resolution,[],[f12591,f135]) ).
fof(f12664,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_101 ),
inference(forward_subsumption_resolution,[],[f12630,f135]) ).
fof(f12875,definition,
( spl4_103
<=> aScalar0(sdtpldt0(xD,xG)) ),
introduced(definition,[new_symbols(definition,[spl4_103])],[avatar_definition]) ).
fof(f12876,plain,
( aScalar0(sdtpldt0(xD,xG))
| ~ spl4_103 ),
inference(avatar_component_clause,[],[f12875]) ).
fof(f12877,plain,
( ~ aScalar0(sdtpldt0(xD,xG))
| spl4_103 ),
inference(avatar_component_clause,[],[f12875]) ).
fof(f12879,definition,
( spl4_104
<=> aScalar0(sdtpldt0(xE,xH)) ),
introduced(definition,[new_symbols(definition,[spl4_104])],[avatar_definition]) ).
fof(f12880,plain,
( aScalar0(sdtpldt0(xE,xH))
| ~ spl4_104 ),
inference(avatar_component_clause,[],[f12879]) ).
fof(f12881,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| spl4_104 ),
inference(avatar_component_clause,[],[f12879]) ).
fof(f12887,definition,
( spl4_106
<=> sdtlseqdt0(sz0z00,sdtpldt0(xE,xH)) ),
introduced(definition,[new_symbols(definition,[spl4_106])],[avatar_definition]) ).
fof(f12888,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xE,xH))
| ~ spl4_106 ),
inference(avatar_component_clause,[],[f12887]) ).
fof(f12889,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xE,xH))
| spl4_106 ),
inference(avatar_component_clause,[],[f12887]) ).
fof(f12895,plain,
( ~ aScalar0(xD)
| ~ aScalar0(xG)
| spl4_103 ),
inference(resolution,[],[f12877,f133]) ).
fof(f12896,plain,
( ~ aScalar0(xG)
| ~ spl4_6
| spl4_103 ),
inference(forward_subsumption_resolution,[],[f12895,f467]) ).
fof(f12897,plain,
( $false
| ~ spl4_6
| ~ spl4_10
| spl4_103 ),
inference(forward_subsumption_resolution,[],[f12896,f666]) ).
fof(f12898,plain,
( ~ spl4_6
| ~ spl4_10
| spl4_103 ),
inference(avatar_contradiction_clause,[],[f12897]) ).
fof(f12899,plain,
( ~ aScalar0(xE)
| ~ aScalar0(xH)
| spl4_104 ),
inference(resolution,[],[f12881,f133]) ).
fof(f12900,plain,
( ~ aScalar0(xH)
| ~ spl4_8
| spl4_104 ),
inference(forward_subsumption_resolution,[],[f12899,f536]) ).
fof(f12901,plain,
( $false
| ~ spl4_8
| ~ spl4_11
| spl4_104 ),
inference(forward_subsumption_resolution,[],[f12900,f731]) ).
fof(f12902,plain,
( ~ spl4_8
| ~ spl4_11
| spl4_104 ),
inference(avatar_contradiction_clause,[],[f12901]) ).
fof(f12907,plain,
( aScalar0(smndt0(sdtpldt0(xE,xH)))
| ~ spl4_104 ),
inference(resolution,[],[f12880,f135]) ).
fof(f12909,plain,
( sdtpldt0(xE,xH) = smndt0(smndt0(sdtpldt0(xE,xH)))
| ~ spl4_104 ),
inference(resolution,[],[f12880,f137]) ).
fof(f25704,definition,
( spl4_188
<=> ! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_188])],[avatar_definition]) ).
fof(f25705,plain,
( ! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_188 ),
inference(avatar_component_clause,[],[f25704]) ).
fof(f25706,plain,
spl4_188,
inference(avatar_split_clause,[],[f133,f25704]) ).
fof(f25763,definition,
( spl4_189
<=> ! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_189])],[avatar_definition]) ).
fof(f25764,plain,
( ! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_189 ),
inference(avatar_component_clause,[],[f25763]) ).
fof(f25765,plain,
spl4_189,
inference(avatar_split_clause,[],[f134,f25763]) ).
fof(f26498,definition,
( spl4_190
<=> aScalar0(sz0z00) ),
introduced(definition,[new_symbols(definition,[spl4_190])],[avatar_definition]) ).
fof(f26500,plain,
( aScalar0(sz0z00)
| ~ spl4_190 ),
inference(avatar_component_clause,[],[f26498]) ).
fof(f26501,plain,
spl4_190,
inference(avatar_split_clause,[],[f132,f26498]) ).
fof(f30616,plain,
( sdtlseqdt0(sdtpldt0(xE,xH),sz0z00)
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtpldt0(xE,xH))
| spl4_106 ),
inference(resolution,[],[f12889,f159]) ).
fof(f30619,plain,
( sdtlseqdt0(sdtpldt0(xE,xH),sz0z00)
| ~ aScalar0(sdtpldt0(xE,xH))
| spl4_106
| ~ spl4_190 ),
inference(forward_subsumption_resolution,[],[f30616,f26500]) ).
fof(f30625,plain,
( sdtlseqdt0(sdtpldt0(xE,xH),sz0z00)
| ~ spl4_104
| spl4_106
| ~ spl4_190 ),
inference(forward_subsumption_resolution,[],[f30619,f12880]) ).
fof(f31543,definition,
( spl4_239
<=> ! [X2,X0,X1] :
( sdtlseqdt0(X0,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_239])],[avatar_definition]) ).
fof(f31544,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(X0,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1) )
| ~ spl4_239 ),
inference(avatar_component_clause,[],[f31543]) ).
fof(f31545,plain,
( spl4_239
| ~ spl4_36 ),
inference(avatar_split_clause,[],[f3090,f2998,f31543]) ).
fof(f32914,definition,
( spl4_248
<=> sdtlseqdt0(sdtpldt0(xE,xH),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl4_248])],[avatar_definition]) ).
fof(f32916,plain,
( sdtlseqdt0(sdtpldt0(xE,xH),sz0z00)
| ~ spl4_248 ),
inference(avatar_component_clause,[],[f32914]) ).
fof(f32917,plain,
( spl4_248
| ~ spl4_104
| spl4_106
| ~ spl4_190 ),
inference(avatar_split_clause,[],[f30625,f26498,f12887,f12879,f32914]) ).
fof(f55138,definition,
( spl4_384
<=> ! [X0,X1] :
( sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(smndt0(X1),X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_384])],[avatar_definition]) ).
fof(f55139,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(smndt0(X1),X0)
| sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_384 ),
inference(avatar_component_clause,[],[f55138]) ).
fof(f55140,plain,
( spl4_384
| ~ spl4_37 ),
inference(avatar_split_clause,[],[f3181,f3120,f55138]) ).
fof(f55141,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0)) )
| ~ spl4_384 ),
inference(resolution,[],[f55139,f154]) ).
fof(f55156,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0) )
| ~ spl4_384 ),
inference(duplicate_literal_removal,[],[f55141]) ).
fof(f55166,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0) )
| ~ spl4_384 ),
inference(forward_subsumption_resolution,[],[f55156,f135]) ).
fof(f55170,definition,
( spl4_385
<=> ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_385])],[avatar_definition]) ).
fof(f55171,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,smndt0(X0))
| ~ sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0) )
| ~ spl4_385 ),
inference(avatar_component_clause,[],[f55170]) ).
fof(f55172,plain,
( spl4_385
| ~ spl4_384 ),
inference(avatar_split_clause,[],[f55166,f55138,f55170]) ).
fof(f55342,definition,
( spl4_393
<=> ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_393])],[avatar_definition]) ).
fof(f55343,plain,
( ! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(X2,smndt0(X0))
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_393 ),
inference(avatar_component_clause,[],[f55342]) ).
fof(f55344,plain,
( spl4_393
| ~ spl4_101 ),
inference(avatar_split_clause,[],[f12664,f12546,f55342]) ).
fof(f58138,definition,
( spl4_403
<=> ! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_403])],[avatar_definition]) ).
fof(f58139,plain,
( ! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) )
| ~ spl4_403 ),
inference(avatar_component_clause,[],[f58138]) ).
fof(f58140,plain,
spl4_403,
inference(avatar_split_clause,[],[f135,f58138]) ).
fof(f61434,definition,
( spl4_420
<=> sdtlseqdt0(sz0z00,sdtpldt0(xD,xG)) ),
introduced(definition,[new_symbols(definition,[spl4_420])],[avatar_definition]) ).
fof(f61435,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xD,xG))
| ~ spl4_420 ),
inference(avatar_component_clause,[],[f61434]) ).
fof(f61436,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xD,xG))
| spl4_420 ),
inference(avatar_component_clause,[],[f61434]) ).
fof(f61624,plain,
( ~ sdtlseqdt0(sz0z00,xD)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ aScalar0(xD)
| ~ aScalar0(xG)
| spl4_420 ),
inference(resolution,[],[f61436,f161]) ).
fof(f61635,plain,
( ~ sdtlseqdt0(sz0z00,xG)
| ~ aScalar0(xD)
| ~ aScalar0(xG)
| ~ spl4_89
| spl4_420 ),
inference(forward_subsumption_resolution,[],[f61624,f11133]) ).
fof(f61645,plain,
( ~ aScalar0(xD)
| ~ aScalar0(xG)
| ~ spl4_30
| ~ spl4_89
| spl4_420 ),
inference(forward_subsumption_resolution,[],[f61635,f2435]) ).
fof(f61654,plain,
( ~ aScalar0(xG)
| ~ spl4_6
| ~ spl4_30
| ~ spl4_89
| spl4_420 ),
inference(forward_subsumption_resolution,[],[f61645,f467]) ).
fof(f61657,plain,
( $false
| ~ spl4_6
| ~ spl4_10
| ~ spl4_30
| ~ spl4_89
| spl4_420 ),
inference(forward_subsumption_resolution,[],[f61654,f666]) ).
fof(f61658,plain,
( ~ spl4_6
| ~ spl4_10
| ~ spl4_30
| ~ spl4_89
| spl4_420 ),
inference(avatar_contradiction_clause,[],[f61657]) ).
fof(f61844,definition,
( spl4_423
<=> sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH))) ),
introduced(definition,[new_symbols(definition,[spl4_423])],[avatar_definition]) ).
fof(f61845,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH)))
| ~ spl4_423 ),
inference(avatar_component_clause,[],[f61844]) ).
fof(f61846,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH)))
| spl4_423 ),
inference(avatar_component_clause,[],[f61844]) ).
fof(f108612,definition,
( spl4_582
<=> aScalar0(sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
introduced(definition,[new_symbols(definition,[spl4_582])],[avatar_definition]) ).
fof(f108613,plain,
( aScalar0(sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ spl4_582 ),
inference(avatar_component_clause,[],[f108612]) ).
fof(f108614,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| spl4_582 ),
inference(avatar_component_clause,[],[f108612]) ).
fof(f108616,definition,
( spl4_583
<=> aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH))) ),
introduced(definition,[new_symbols(definition,[spl4_583])],[avatar_definition]) ).
fof(f108617,plain,
( aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ spl4_583 ),
inference(avatar_component_clause,[],[f108616]) ).
fof(f108618,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| spl4_583 ),
inference(avatar_component_clause,[],[f108616]) ).
fof(f108627,plain,
( ~ aScalar0(sdtpldt0(xC,xF))
| ~ aScalar0(sdtpldt0(xD,xG))
| ~ spl4_189
| spl4_582 ),
inference(resolution,[],[f108614,f25764]) ).
fof(f108628,plain,
( ~ aScalar0(sdtpldt0(xD,xG))
| ~ spl4_54
| ~ spl4_189
| spl4_582 ),
inference(forward_subsumption_resolution,[],[f108627,f4354]) ).
fof(f108633,plain,
( $false
| ~ spl4_54
| ~ spl4_103
| ~ spl4_189
| spl4_582 ),
inference(forward_subsumption_resolution,[],[f108628,f12876]) ).
fof(f108634,plain,
( ~ spl4_54
| ~ spl4_103
| ~ spl4_189
| spl4_582 ),
inference(avatar_contradiction_clause,[],[f108633]) ).
fof(f108642,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(X0,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ aScalar0(X0) )
| spl4_1
| ~ spl4_582 ),
inference(backward_subsumption_resolution,[],[f227,f108613]) ).
fof(f108647,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_189
| spl4_583 ),
inference(resolution,[],[f108618,f25764]) ).
fof(f108648,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_189
| spl4_583 ),
inference(duplicate_literal_removal,[],[f108647]) ).
fof(f108649,plain,
( $false
| ~ spl4_104
| ~ spl4_189
| spl4_583 ),
inference(forward_subsumption_resolution,[],[f108648,f12880]) ).
fof(f108650,plain,
( ~ spl4_104
| ~ spl4_189
| spl4_583 ),
inference(avatar_contradiction_clause,[],[f108649]) ).
fof(f108676,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(X0,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(X0) )
| spl4_1
| ~ spl4_582
| ~ spl4_583 ),
inference(forward_subsumption_resolution,[],[f108642,f108617]) ).
fof(f108820,definition,
( spl4_586
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(X0,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_586])],[avatar_definition]) ).
fof(f108821,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(X0,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(X0) )
| ~ spl4_586 ),
inference(avatar_component_clause,[],[f108820]) ).
fof(f108822,plain,
( spl4_586
| spl4_1
| ~ spl4_582
| ~ spl4_583 ),
inference(avatar_split_clause,[],[f108676,f108616,f108612,f220,f108820]) ).
fof(f108844,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ aScalar0(sdtpldt0(X0,X1))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_239
| ~ spl4_586 ),
inference(resolution,[],[f108821,f31544]) ).
fof(f108867,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_188
| ~ spl4_239
| ~ spl4_586 ),
inference(forward_subsumption_resolution,[],[f108844,f25705]) ).
fof(f108873,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_188
| ~ spl4_239
| ~ spl4_583
| ~ spl4_586 ),
inference(forward_subsumption_resolution,[],[f108867,f108617]) ).
fof(f135109,definition,
( spl4_667
<=> ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_667])],[avatar_definition]) ).
fof(f135110,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_667 ),
inference(avatar_component_clause,[],[f135109]) ).
fof(f135111,plain,
( spl4_667
| ~ spl4_188
| ~ spl4_239
| ~ spl4_583
| ~ spl4_586 ),
inference(avatar_split_clause,[],[f108873,f108820,f108616,f31543,f25704,f135109]) ).
fof(f135215,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0) )
| ~ spl4_667 ),
inference(superposition,[],[f135110,f138]) ).
fof(f135250,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0)) )
| ~ spl4_667 ),
inference(duplicate_literal_removal,[],[f135215]) ).
fof(f135314,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ sdtlseqdt0(sz0z00,smndt0(X0))
| ~ aScalar0(X0) )
| ~ spl4_403
| ~ spl4_667 ),
inference(forward_subsumption_resolution,[],[f135250,f58139]) ).
fof(f135482,definition,
( spl4_668
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,smndt0(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl4_668])],[avatar_definition]) ).
fof(f135483,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),X0)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,smndt0(X0)) )
| ~ spl4_668 ),
inference(avatar_component_clause,[],[f135482]) ).
fof(f135485,definition,
( spl4_669
<=> sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
introduced(definition,[new_symbols(definition,[spl4_669])],[avatar_definition]) ).
fof(f135487,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)))
| spl4_669 ),
inference(avatar_component_clause,[],[f135485]) ).
fof(f135488,plain,
( spl4_668
| ~ spl4_669
| ~ spl4_403
| ~ spl4_667 ),
inference(avatar_split_clause,[],[f135314,f135109,f58138,f135485,f135482]) ).
fof(f135493,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xC,xF))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xD,xG))
| ~ aScalar0(sdtpldt0(xC,xF))
| ~ aScalar0(sdtpldt0(xD,xG))
| spl4_669 ),
inference(resolution,[],[f135487,f160]) ).
fof(f135500,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xD,xG))
| ~ aScalar0(sdtpldt0(xC,xF))
| ~ aScalar0(sdtpldt0(xD,xG))
| ~ spl4_56
| spl4_669 ),
inference(forward_subsumption_resolution,[],[f135493,f4455]) ).
fof(f135508,plain,
( ~ aScalar0(sdtpldt0(xC,xF))
| ~ aScalar0(sdtpldt0(xD,xG))
| ~ spl4_56
| ~ spl4_420
| spl4_669 ),
inference(forward_subsumption_resolution,[],[f135500,f61435]) ).
fof(f135514,plain,
( ~ aScalar0(sdtpldt0(xD,xG))
| ~ spl4_54
| ~ spl4_56
| ~ spl4_420
| spl4_669 ),
inference(forward_subsumption_resolution,[],[f135508,f4354]) ).
fof(f135517,plain,
( $false
| ~ spl4_54
| ~ spl4_56
| ~ spl4_103
| ~ spl4_420
| spl4_669 ),
inference(forward_subsumption_resolution,[],[f135514,f12876]) ).
fof(f135518,plain,
( ~ spl4_54
| ~ spl4_56
| ~ spl4_103
| ~ spl4_420
| spl4_669 ),
inference(avatar_contradiction_clause,[],[f135517]) ).
fof(f135594,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ sdtlseqdt0(sz0z00,smndt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH))))
| ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ spl4_668 ),
inference(resolution,[],[f135483,f154]) ).
fof(f135604,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))
| ~ sdtlseqdt0(sz0z00,smndt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH))))
| ~ spl4_668 ),
inference(duplicate_literal_removal,[],[f135594]) ).
fof(f135626,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH))))
| ~ spl4_583
| ~ spl4_668 ),
inference(forward_subsumption_resolution,[],[f135604,f108617]) ).
fof(f135644,definition,
( spl4_670
<=> sdtlseqdt0(sz0z00,smndt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)))) ),
introduced(definition,[new_symbols(definition,[spl4_670])],[avatar_definition]) ).
fof(f135646,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH))))
| spl4_670 ),
inference(avatar_component_clause,[],[f135644]) ).
fof(f135647,plain,
( ~ spl4_670
| ~ spl4_583
| ~ spl4_668 ),
inference(avatar_split_clause,[],[f135626,f135482,f108616,f135644]) ).
fof(f135655,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xE,xH),smndt0(sdtpldt0(xE,xH))))
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ aScalar0(sdtpldt0(xE,xH))
| spl4_670 ),
inference(superposition,[],[f135646,f152]) ).
fof(f135656,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xE,xH),smndt0(sdtpldt0(xE,xH))))
| ~ aScalar0(sdtpldt0(xE,xH))
| spl4_670 ),
inference(duplicate_literal_removal,[],[f135655]) ).
fof(f135660,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xE,xH),smndt0(sdtpldt0(xE,xH))))
| ~ spl4_104
| spl4_670 ),
inference(forward_subsumption_resolution,[],[f135656,f12880]) ).
fof(f135669,definition,
( spl4_671
<=> sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xE,xH),smndt0(sdtpldt0(xE,xH)))) ),
introduced(definition,[new_symbols(definition,[spl4_671])],[avatar_definition]) ).
fof(f135671,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xE,xH),smndt0(sdtpldt0(xE,xH))))
| spl4_671 ),
inference(avatar_component_clause,[],[f135669]) ).
fof(f135672,plain,
( ~ spl4_671
| ~ spl4_104
| spl4_670 ),
inference(avatar_split_clause,[],[f135660,f135644,f12879,f135669]) ).
fof(f135674,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ sdtlseqdt0(sz0z00,smndt0(smndt0(sdtpldt0(xE,xH))))
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ aScalar0(smndt0(sdtpldt0(xE,xH))) )
| ~ spl4_393
| spl4_671 ),
inference(resolution,[],[f135671,f55343]) ).
fof(f135676,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ aScalar0(smndt0(sdtpldt0(xE,xH))) )
| ~ spl4_101
| spl4_671 ),
inference(resolution,[],[f135671,f12547]) ).
fof(f135684,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(xE,xH)) )
| ~ spl4_101
| ~ spl4_403
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135676,f58139]) ).
fof(f135685,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ sdtlseqdt0(sz0z00,smndt0(smndt0(sdtpldt0(xE,xH))))
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(xE,xH)) )
| ~ spl4_393
| ~ spl4_403
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135674,f58139]) ).
fof(f135687,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ sdtlseqdt0(sz0z00,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0) )
| ~ spl4_101
| ~ spl4_104
| ~ spl4_403
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135684,f12880]) ).
fof(f135688,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ sdtlseqdt0(sz0z00,smndt0(smndt0(sdtpldt0(xE,xH))))
| ~ aScalar0(X0) )
| ~ spl4_104
| ~ spl4_393
| ~ spl4_403
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135685,f12880]) ).
fof(f135689,plain,
( ! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xE,xH))
| ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0) )
| ~ spl4_104
| ~ spl4_393
| ~ spl4_403
| spl4_671 ),
inference(forward_demodulation,[],[f135688,f12909]) ).
fof(f135691,plain,
( ~ sdtlseqdt0(sdtpldt0(xE,xH),sz0z00)
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_385
| spl4_423 ),
inference(resolution,[],[f61846,f55171]) ).
fof(f135698,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_248
| ~ spl4_385
| spl4_423 ),
inference(forward_subsumption_resolution,[],[f135691,f32916]) ).
fof(f135702,plain,
( $false
| ~ spl4_104
| ~ spl4_248
| ~ spl4_385
| spl4_423 ),
inference(forward_subsumption_resolution,[],[f135698,f12880]) ).
fof(f135703,plain,
( ~ spl4_104
| ~ spl4_248
| ~ spl4_385
| spl4_423 ),
inference(avatar_contradiction_clause,[],[f135702]) ).
fof(f135728,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ aScalar0(X0) )
| ~ spl4_101
| ~ spl4_104
| ~ spl4_403
| ~ spl4_423
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135687,f61845]) ).
fof(f135774,definition,
( spl4_672
<=> ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_672])],[avatar_definition]) ).
fof(f135775,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(xE,xH))
| ~ aScalar0(X0) )
| ~ spl4_672 ),
inference(avatar_component_clause,[],[f135774]) ).
fof(f135776,plain,
( spl4_672
| ~ spl4_101
| ~ spl4_104
| ~ spl4_403
| ~ spl4_423
| spl4_671 ),
inference(avatar_split_clause,[],[f135728,f135669,f61844,f58138,f12879,f12546,f135774]) ).
fof(f135779,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_672 ),
inference(resolution,[],[f135775,f154]) ).
fof(f135799,plain,
( ~ aScalar0(sdtpldt0(xE,xH))
| ~ spl4_672 ),
inference(duplicate_literal_removal,[],[f135779]) ).
fof(f135811,plain,
( $false
| ~ spl4_104
| ~ spl4_672 ),
inference(forward_subsumption_resolution,[],[f135799,f12880]) ).
fof(f135812,plain,
( ~ spl4_104
| ~ spl4_672 ),
inference(avatar_contradiction_clause,[],[f135811]) ).
fof(f136064,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0) )
| ~ spl4_104
| ~ spl4_106
| ~ spl4_393
| ~ spl4_403
| spl4_671 ),
inference(forward_subsumption_resolution,[],[f135689,f12888]) ).
fof(f136613,definition,
( spl4_675
<=> ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_675])],[avatar_definition]) ).
fof(f136614,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(X0) )
| ~ spl4_675 ),
inference(avatar_component_clause,[],[f136613]) ).
fof(f136615,plain,
( spl4_675
| ~ spl4_104
| ~ spl4_106
| ~ spl4_393
| ~ spl4_403
| spl4_671 ),
inference(avatar_split_clause,[],[f136064,f135669,f58138,f55342,f12887,f12879,f136613]) ).
fof(f136616,plain,
( ~ aScalar0(smndt0(sdtpldt0(xE,xH)))
| ~ aScalar0(smndt0(sdtpldt0(xE,xH)))
| ~ spl4_675 ),
inference(resolution,[],[f136614,f154]) ).
fof(f136628,plain,
( ~ aScalar0(smndt0(sdtpldt0(xE,xH)))
| ~ spl4_675 ),
inference(duplicate_literal_removal,[],[f136616]) ).
fof(f136632,plain,
( $false
| ~ spl4_104
| ~ spl4_675 ),
inference(forward_subsumption_resolution,[],[f136628,f12907]) ).
fof(f136633,plain,
( ~ spl4_104
| ~ spl4_675 ),
inference(avatar_contradiction_clause,[],[f136632]) ).
cnf(s1,plain,
~ spl4_1,
inference(sat_conversion,[],[f223]) ).
cnf(s5,plain,
spl4_5,
inference(sat_conversion,[],[f393]) ).
cnf(s6,plain,
spl4_6,
inference(sat_conversion,[],[f468]) ).
cnf(s8,plain,
spl4_8,
inference(sat_conversion,[],[f537]) ).
cnf(s10,plain,
spl4_10,
inference(sat_conversion,[],[f667]) ).
cnf(s11,plain,
spl4_11,
inference(sat_conversion,[],[f732]) ).
cnf(s13,plain,
( ~ spl4_5
| spl4_13 ),
inference(sat_conversion,[],[f800]) ).
cnf(s14,plain,
( ~ spl4_5
| spl4_14 ),
inference(sat_conversion,[],[f900]) ).
cnf(s25,plain,
spl4_25,
inference(sat_conversion,[],[f1961]) ).
cnf(s30,plain,
( ~ spl4_25
| spl4_30 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s36,plain,
( ~ spl4_13
| spl4_36 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s37,plain,
( ~ spl4_36
| spl4_37 ),
inference(sat_conversion,[],[f3122]) ).
cnf(s46,plain,
spl4_46,
inference(sat_conversion,[],[f3714]) ).
cnf(s47,plain,
( ~ spl4_46
| spl4_47 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s53,plain,
( ~ spl4_46
| ~ spl4_47
| spl4_53 ),
inference(sat_conversion,[],[f4337]) ).
cnf(s54,plain,
( ~ spl4_46
| ~ spl4_53
| spl4_54 ),
inference(sat_conversion,[],[f4355]) ).
cnf(s56,plain,
( ~ spl4_46
| ~ spl4_53
| spl4_56 ),
inference(sat_conversion,[],[f4456]) ).
cnf(s88,plain,
spl4_88,
inference(sat_conversion,[],[f11094]) ).
cnf(s89,plain,
( ~ spl4_88
| spl4_89 ),
inference(sat_conversion,[],[f11134]) ).
cnf(s99,plain,
( ~ spl4_14
| spl4_100 ),
inference(sat_conversion,[],[f12331]) ).
cnf(s100,plain,
( ~ spl4_100
| spl4_101 ),
inference(sat_conversion,[],[f12548]) ).
cnf(s103,plain,
( ~ spl4_6
| ~ spl4_10
| spl4_103 ),
inference(sat_conversion,[],[f12898]) ).
cnf(s104,plain,
( ~ spl4_8
| ~ spl4_11
| spl4_104 ),
inference(sat_conversion,[],[f12902]) ).
cnf(s222,plain,
spl4_188,
inference(sat_conversion,[],[f25706]) ).
cnf(s223,plain,
spl4_189,
inference(sat_conversion,[],[f25765]) ).
cnf(s224,plain,
spl4_190,
inference(sat_conversion,[],[f26501]) ).
cnf(s272,plain,
( ~ spl4_36
| spl4_239 ),
inference(sat_conversion,[],[f31545]) ).
cnf(s281,plain,
( ~ spl4_104
| spl4_106
| ~ spl4_190
| spl4_248 ),
inference(sat_conversion,[],[f32917]) ).
cnf(s427,plain,
( ~ spl4_37
| spl4_384 ),
inference(sat_conversion,[],[f55140]) ).
cnf(s428,plain,
( ~ spl4_384
| spl4_385 ),
inference(sat_conversion,[],[f55172]) ).
cnf(s436,plain,
( ~ spl4_101
| spl4_393 ),
inference(sat_conversion,[],[f55344]) ).
cnf(s446,plain,
spl4_403,
inference(sat_conversion,[],[f58140]) ).
cnf(s467,plain,
( ~ spl4_6
| ~ spl4_10
| ~ spl4_30
| ~ spl4_89
| spl4_420 ),
inference(sat_conversion,[],[f61658]) ).
cnf(s837,plain,
( ~ spl4_54
| ~ spl4_103
| ~ spl4_189
| spl4_582 ),
inference(sat_conversion,[],[f108634]) ).
cnf(s840,plain,
( ~ spl4_104
| ~ spl4_189
| spl4_583 ),
inference(sat_conversion,[],[f108650]) ).
cnf(s847,plain,
( spl4_1
| ~ spl4_582
| ~ spl4_583
| spl4_586 ),
inference(sat_conversion,[],[f108822]) ).
cnf(s990,plain,
( ~ spl4_188
| ~ spl4_239
| ~ spl4_583
| ~ spl4_586
| spl4_667 ),
inference(sat_conversion,[],[f135111]) ).
cnf(s991,plain,
( ~ spl4_403
| ~ spl4_667
| spl4_668
| ~ spl4_669 ),
inference(sat_conversion,[],[f135488]) ).
cnf(s993,plain,
( ~ spl4_54
| ~ spl4_56
| ~ spl4_103
| ~ spl4_420
| spl4_669 ),
inference(sat_conversion,[],[f135518]) ).
cnf(s994,plain,
( ~ spl4_583
| ~ spl4_668
| ~ spl4_670 ),
inference(sat_conversion,[],[f135647]) ).
cnf(s995,plain,
( ~ spl4_104
| spl4_670
| ~ spl4_671 ),
inference(sat_conversion,[],[f135672]) ).
cnf(s997,plain,
( ~ spl4_104
| ~ spl4_248
| ~ spl4_385
| spl4_423 ),
inference(sat_conversion,[],[f135703]) ).
cnf(s998,plain,
( ~ spl4_101
| ~ spl4_104
| ~ spl4_403
| ~ spl4_423
| spl4_671
| spl4_672 ),
inference(sat_conversion,[],[f135776]) ).
cnf(s1000,plain,
( ~ spl4_104
| ~ spl4_672 ),
inference(sat_conversion,[],[f135812]) ).
cnf(s1008,plain,
( ~ spl4_104
| ~ spl4_106
| ~ spl4_393
| ~ spl4_403
| spl4_671
| spl4_675 ),
inference(sat_conversion,[],[f136615]) ).
cnf(s1009,plain,
( ~ spl4_104
| ~ spl4_675 ),
inference(sat_conversion,[],[f136633]) ).
cnf(s1023,plain,
spl4_89,
inference(rat,[],[s89,s88]) ).
cnf(s1043,plain,
spl4_47,
inference(rat,[],[s47,s46]) ).
cnf(s1047,plain,
spl4_53,
inference(rat,[],[s53,s46,s1043]) ).
cnf(s1051,plain,
spl4_56,
inference(rat,[],[s56,s46,s1047]) ).
cnf(s1052,plain,
spl4_54,
inference(rat,[],[s54,s46,s1047]) ).
cnf(s1074,plain,
spl4_30,
inference(rat,[],[s30,s25]) ).
cnf(s1180,plain,
spl4_104,
inference(rat,[],[s104,s11,s8]) ).
cnf(s1182,plain,
~ spl4_675,
inference(rat,[],[s1009,s1180]) ).
cnf(s1183,plain,
~ spl4_672,
inference(rat,[],[s1000,s1180]) ).
cnf(s1186,plain,
spl4_583,
inference(rat,[],[s840,s223,s1180]) ).
cnf(s1222,plain,
spl4_420,
inference(rat,[],[s467,s10,s1023,s1074,s6]) ).
cnf(s1244,plain,
spl4_103,
inference(rat,[],[s103,s10,s6]) ).
cnf(s1249,plain,
spl4_582,
inference(rat,[],[s837,s1052,s223,s1244]) ).
cnf(s1274,plain,
spl4_669,
inference(rat,[],[s993,s1222,s1052,s1051,s1244]) ).
cnf(s1311,plain,
spl4_14,
inference(rat,[],[s14,s5]) ).
cnf(s1312,plain,
spl4_13,
inference(rat,[],[s13,s5]) ).
cnf(s1324,plain,
spl4_100,
inference(rat,[],[s99,s1311]) ).
cnf(s1347,plain,
spl4_36,
inference(rat,[],[s36,s1312]) ).
cnf(s1358,plain,
spl4_101,
inference(rat,[],[s100,s1324]) ).
cnf(s1400,plain,
spl4_239,
inference(rat,[],[s272,s1347]) ).
cnf(s1408,plain,
spl4_37,
inference(rat,[],[s37,s1347]) ).
cnf(s1430,plain,
spl4_393,
inference(rat,[],[s436,s1358]) ).
cnf(s1458,plain,
spl4_384,
inference(rat,[],[s427,s1408]) ).
cnf(s1489,plain,
spl4_385,
inference(rat,[],[s428,s1458]) ).
cnf(s1547,plain,
spl4_586,
inference(rat,[],[s847,s1249,s1186,s1]) ).
cnf(s1549,plain,
spl4_667,
inference(rat,[],[s990,s1400,s1186,s222,s1547]) ).
cnf(s1551,plain,
spl4_668,
inference(rat,[],[s991,s1274,s446,s1549]) ).
cnf(s1552,plain,
~ spl4_670,
inference(rat,[],[s994,s1186,s1551]) ).
cnf(s1554,plain,
~ spl4_671,
inference(rat,[],[s995,s1180,s1552]) ).
cnf(s1555,plain,
~ spl4_423,
inference(rat,[],[s998,s1183,s1358,s1180,s446,s1554]) ).
cnf(s1556,plain,
~ spl4_106,
inference(rat,[],[s1008,s1182,s1430,s446,s1180,s1554]) ).
cnf(s1557,plain,
~ spl4_248,
inference(rat,[],[s997,s1489,s1180,s1555]) ).
cnf(s1562,plain,
$false,
inference(rat,[],[s281,s1180,s224,s1557,s1556]) ).
fof(f136635,plain,
$false,
inference(avatar_sat_refutation,[],[s1562]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG075+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:09:40 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.56/2.85 % (3437195)Detected formulas, will run a generic FOF schedule.
% 13.56/2.85 % (3437202)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=2012607634:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.56/2.85 % (3437205)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=70729841:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.56/2.85 % (3437201)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=2614657218:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.56/2.85 % (3437206)dis-21_1_sil=8000:lcm=predicate:random_seed=2679622194: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)
% 13.56/2.85 % (3437200)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=2453368267:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.56/2.85 % (3437203)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3689141703:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.56/2.85 % (3437204)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=126007696:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.56/2.85 % (3437206)Instruction limit reached!
% 13.56/2.85 % (3437206)------------------------------
% 13.56/2.85 % (3437206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3437206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3437206)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3437206)Termination reason: Instruction limit
% 13.56/2.85 % (3437206)Termination phase: Saturation
% 13.56/2.85 % (3437206)Time elapsed: 0.058 s
% 13.56/2.85 % (3437206)Peak memory usage: 89 MB
% 13.56/2.85 % (3437206)Instructions burned: 130 (million)
% 13.56/2.85 % (3437203)Instruction limit reached!
% 13.56/2.85 % (3437203)------------------------------
% 13.56/2.85 % (3437203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3437203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3437203)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3437203)Termination reason: Instruction limit
% 13.56/2.85 % (3437203)Termination phase: Saturation
% 13.56/2.85 % (3437203)Time elapsed: 0.059 s
% 13.56/2.85 % (3437203)Peak memory usage: 89 MB
% 13.56/2.85 % (3437203)Instructions burned: 110 (million)
% 13.56/2.85 % (3437204)Instruction limit reached!
% 13.56/2.85 % (3437204)------------------------------
% 13.56/2.85 % (3437204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3437204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3437204)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3437204)Termination reason: Instruction limit
% 13.56/2.85 % (3437204)Termination phase: Saturation
% 13.56/2.85 % (3437204)Time elapsed: 0.070 s
% 13.56/2.85 % (3437204)Peak memory usage: 88 MB
% 13.56/2.85 % (3437204)Instructions burned: 120 (million)
% 13.56/2.85 % (3437205)Instruction limit reached!
% 13.56/2.85 % (3437205)------------------------------
% 13.56/2.85 % (3437205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3437205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3437205)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3437205)Termination reason: Instruction limit
% 13.56/2.85 % (3437205)Termination phase: Saturation
% 13.56/2.85 % (3437205)Time elapsed: 0.091 s
% 13.56/2.85 % (3437205)Peak memory usage: 90 MB
% 13.56/2.85 % (3437205)Instructions burned: 140 (million)
% 13.56/2.85 % (3437214)lrs+10_1_sil=8000:sp=occurrence:random_seed=3632036109:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.56/2.85 % (3437215)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1008406419:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.56/2.85 % (3437216)lrs+1011_1_sil=32000:sp=occurrence:random_seed=501710134:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.56/2.85 % (3437217)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=2566163554:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.56/2.85 % (3437215)Instruction limit reached!
% 19.87/3.76 % (3437215)------------------------------
% 19.87/3.76 % (3437215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437215)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437215)Termination reason: Instruction limit
% 19.87/3.76 % (3437215)Termination phase: Saturation
% 19.87/3.76 % (3437215)Time elapsed: 0.071 s
% 19.87/3.76 % (3437215)Peak memory usage: 91 MB
% 19.87/3.76 % (3437215)Instructions burned: 157 (million)
% 19.87/3.76 % (3437217)Instruction limit reached!
% 19.87/3.76 % (3437217)------------------------------
% 19.87/3.76 % (3437217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437217)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437217)Termination reason: Instruction limit
% 19.87/3.76 % (3437217)Termination phase: Saturation
% 19.87/3.76 % (3437217)Time elapsed: 0.118 s
% 19.87/3.76 % (3437217)Peak memory usage: 98 MB
% 19.87/3.76 % (3437217)Instructions burned: 249 (million)
% 19.87/3.76 % (3437214)Instruction limit reached!
% 19.87/3.76 % (3437214)------------------------------
% 19.87/3.76 % (3437214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437214)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437214)Termination reason: Instruction limit
% 19.87/3.76 % (3437214)Termination phase: Saturation
% 19.87/3.76 % (3437214)Time elapsed: 0.173 s
% 19.87/3.76 % (3437214)Peak memory usage: 93 MB
% 19.87/3.76 % (3437214)Instructions burned: 285 (million)
% 19.87/3.76 % (3437216)Instruction limit reached!
% 19.87/3.76 % (3437216)------------------------------
% 19.87/3.76 % (3437216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437216)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437216)Termination reason: Instruction limit
% 19.87/3.76 % (3437216)Termination phase: Saturation
% 19.87/3.76 % (3437216)Time elapsed: 0.190 s
% 19.87/3.76 % (3437216)Peak memory usage: 93 MB
% 19.87/3.76 % (3437216)Instructions burned: 326 (million)
% 19.87/3.76 % (3437222)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4248888623:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.87/3.76 % (3437223)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1057057278:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 19.87/3.76 % (3437224)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1682018330:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.87/3.76 % (3437225)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2422461155:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.87/3.76 % (3437224)Instruction limit reached!
% 19.87/3.76 % (3437224)------------------------------
% 19.87/3.76 % (3437224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437224)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437224)Termination reason: Instruction limit
% 19.87/3.76 % (3437224)Termination phase: Saturation
% 19.87/3.76 % (3437224)Time elapsed: 0.072 s
% 19.87/3.76 % (3437224)Peak memory usage: 91 MB
% 19.87/3.76 % (3437224)Instructions burned: 114 (million)
% 19.87/3.76 % (3437222)Instruction limit reached!
% 19.87/3.76 % (3437222)------------------------------
% 19.87/3.76 % (3437222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437222)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437222)Termination reason: Instruction limit
% 19.87/3.76 % (3437222)Termination phase: Saturation
% 19.87/3.76 % (3437222)Time elapsed: 0.173 s
% 19.87/3.76 % (3437222)Peak memory usage: 90 MB
% 19.87/3.76 % (3437222)Instructions burned: 295 (million)
% 19.87/3.76 % (3437225)Instruction limit reached!
% 19.87/3.76 % (3437225)------------------------------
% 19.87/3.76 % (3437225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.76 % (3437225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.76 % (3437225)CaDiCaL version: 2.1.3
% 19.87/3.76 % (3437225)Termination reason: Instruction limit
% 19.87/3.76 % (3437225)Termination phase: Saturation
% 44.21/7.07 % (3437225)Time elapsed: 0.065 s
% 44.21/7.07 % (3437225)Peak memory usage: 89 MB
% 44.21/7.07 % (3437225)Instructions burned: 128 (million)
% 44.21/7.07 % (3437231)lrs+10_1_sil=8000:sp=occurrence:random_seed=3141250064:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 44.21/7.07 % (3437230)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=990532695:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 44.21/7.07 % (3437232)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=312614149:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 44.21/7.07 % (3437230)Instruction limit reached!
% 44.21/7.07 % (3437230)------------------------------
% 44.21/7.07 % (3437230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/7.07 % (3437230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/7.07 % (3437230)CaDiCaL version: 2.1.3
% 44.21/7.07 % (3437230)Termination reason: Instruction limit
% 44.21/7.07 % (3437230)Termination phase: Saturation
% 44.21/7.07 % (3437230)Time elapsed: 0.063 s
% 44.21/7.07 % (3437230)Peak memory usage: 89 MB
% 44.21/7.07 % (3437230)Instructions burned: 115 (million)
% 44.21/7.07 % (3437236)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3042098243:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 44.21/7.07 % (3437232)Instruction limit reached!
% 44.21/7.07 % (3437232)------------------------------
% 44.21/7.07 % (3437232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/7.07 % (3437232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/7.07 % (3437232)CaDiCaL version: 2.1.3
% 44.21/7.07 % (3437232)Termination reason: Instruction limit
% 44.21/7.07 % (3437232)Termination phase: Saturation
% 44.21/7.07 % (3437232)Time elapsed: 0.244 s
% 44.21/7.07 % (3437232)Peak memory usage: 95 MB
% 44.21/7.07 % (3437232)Instructions burned: 439 (million)
% 44.21/7.07 % (3437238)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=281154498:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 44.21/7.07 % (3437238)Instruction limit reached!
% 44.21/7.07 % (3437238)------------------------------
% 44.21/7.07 % (3437238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/7.07 % (3437238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/7.07 % (3437238)CaDiCaL version: 2.1.3
% 44.21/7.07 % (3437238)Termination reason: Instruction limit
% 44.21/7.07 % (3437238)Termination phase: Saturation
% 44.21/7.07 % (3437238)Time elapsed: 0.059 s
% 44.21/7.07 % (3437238)Peak memory usage: 91 MB
% 44.21/7.07 % (3437238)Instructions burned: 136 (million)
% 44.21/7.07 % (3437231)Instruction limit reached!
% 44.21/7.07 % (3437231)------------------------------
% 44.21/7.07 % (3437231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/7.07 % (3437231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/7.07 % (3437231)CaDiCaL version: 2.1.3
% 44.21/7.07 % (3437231)Termination reason: Instruction limit
% 44.21/7.07 % (3437231)Termination phase: Saturation
% 44.21/7.07 % (3437231)Time elapsed: 0.496 s
% 44.21/7.07 % (3437231)Peak memory usage: 102 MB
% 44.21/7.07 % (3437231)Instructions burned: 908 (million)
% 44.21/7.07 % (3437240)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=478196973:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 44.21/7.07 % (3437241)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2004611328:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 44.21/7.07 % (3437240)Instruction limit reached!
% 44.21/7.07 % (3437240)------------------------------
% 44.21/7.07 % (3437240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/7.07 % (3437240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/7.07 % (3437240)CaDiCaL version: 2.1.3
% 44.21/7.07 % (3437240)Termination reason: Instruction limit
% 44.21/7.07 % (3437240)Termination phase: Saturation
% 44.21/7.07 % (3437240)Time elapsed: 0.282 s
% 44.21/7.07 % (3437240)Peak memory usage: 91 MB
% 44.21/7.07 % (3437240)Instructions burned: 593 (million)
% 44.21/7.07 % (3437244)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=4062014640:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 69.85/10.71 % (3437244)Instruction limit reached!
% 69.85/10.71 % (3437244)------------------------------
% 69.85/10.71 % (3437244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437244)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437244)Termination reason: Instruction limit
% 69.85/10.71 % (3437244)Termination phase: Saturation
% 69.85/10.71 % (3437244)Time elapsed: 0.065 s
% 69.85/10.71 % (3437244)Peak memory usage: 91 MB
% 69.85/10.71 % (3437244)Instructions burned: 127 (million)
% 69.85/10.71 % (3437223)Instruction limit reached!
% 69.85/10.71 % (3437223)------------------------------
% 69.85/10.71 % (3437223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437223)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437223)Termination reason: Instruction limit
% 69.85/10.71 % (3437223)Termination phase: Saturation
% 69.85/10.71 % (3437223)Time elapsed: 1.403 s
% 69.85/10.71 % (3437223)Peak memory usage: 144 MB
% 69.85/10.71 % (3437223)Instructions burned: 2350 (million)
% 69.85/10.71 % (3437246)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1452036258:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 69.85/10.71 % (3437247)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2277195195:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 69.85/10.71 % (3437246)Instruction limit reached!
% 69.85/10.71 % (3437246)------------------------------
% 69.85/10.71 % (3437246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437246)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437246)Termination reason: Instruction limit
% 69.85/10.71 % (3437246)Termination phase: Saturation
% 69.85/10.71 % (3437246)Time elapsed: 0.070 s
% 69.85/10.71 % (3437246)Peak memory usage: 91 MB
% 69.85/10.71 % (3437246)Instructions burned: 136 (million)
% 69.85/10.71 % (3437247)Instruction limit reached!
% 69.85/10.71 % (3437247)------------------------------
% 69.85/10.71 % (3437247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437247)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437247)Termination reason: Instruction limit
% 69.85/10.71 % (3437247)Termination phase: Saturation
% 69.85/10.71 % (3437247)Time elapsed: 0.071 s
% 69.85/10.71 % (3437247)Peak memory usage: 91 MB
% 69.85/10.71 % (3437247)Instructions burned: 142 (million)
% 69.85/10.71 % (3437250)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2146508922:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 69.85/10.71 % (3437251)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=1178542347:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 69.85/10.71 % (3437250)Instruction limit reached!
% 69.85/10.71 % (3437250)------------------------------
% 69.85/10.71 % (3437250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437250)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437250)Termination reason: Instruction limit
% 69.85/10.71 % (3437250)Termination phase: Saturation
% 69.85/10.71 % (3437250)Time elapsed: 0.231 s
% 69.85/10.71 % (3437250)Peak memory usage: 97 MB
% 69.85/10.71 % (3437250)Instructions burned: 431 (million)
% 69.85/10.71 % (3437254)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1588719757:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 69.85/10.71 % (3437254)Instruction limit reached!
% 69.85/10.71 % (3437254)------------------------------
% 69.85/10.71 % (3437254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.85/10.71 % (3437254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.85/10.71 % (3437254)CaDiCaL version: 2.1.3
% 69.85/10.71 % (3437254)Termination reason: Instruction limit
% 69.85/10.71 % (3437254)Termination phase: Saturation
% 69.85/10.71 % (3437254)Time elapsed: 0.075 s
% 69.85/10.71 % (3437254)Peak memory usage: 92 MB
% 93.88/14.04 % (3437254)Instructions burned: 151 (million)
% 93.88/14.04 % (3437256)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2777730712:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 93.88/14.04 % (3437236)Instruction limit reached!
% 93.88/14.04 % (3437236)------------------------------
% 93.88/14.04 % (3437236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437236)CaDiCaL version: 2.1.3
% 93.88/14.04 % (3437236)Termination reason: Instruction limit
% 93.88/14.04 % (3437236)Termination phase: Saturation
% 93.88/14.04 % (3437236)Time elapsed: 3.210 s
% 93.88/14.04 % (3437236)Peak memory usage: 169 MB
% 93.88/14.04 % (3437236)Instructions burned: 5204 (million)
% 93.88/14.04 % (3437258)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4233612112:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi)
% 93.88/14.04 % (3437258)Instruction limit reached!
% 93.88/14.04 % (3437258)------------------------------
% 93.88/14.04 % (3437258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437258)CaDiCaL version: 2.1.3
% 93.88/14.04 % (3437258)Termination reason: Instruction limit
% 93.88/14.04 % (3437258)Termination phase: Saturation
% 93.88/14.04 % (3437258)Time elapsed: 0.219 s
% 93.88/14.04 % (3437258)Peak memory usage: 93 MB
% 93.88/14.04 % (3437258)Instructions burned: 668 (million)
% 93.88/14.04 % (3437260)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1999132183:s2a=on:i=185:s2at=1.8:fdi=4_2952 on theBenchmark for (2952ds/185Mi)
% 93.88/14.04 % (3437260)Instruction limit reached!
% 93.88/14.04 % (3437260)------------------------------
% 93.88/14.04 % (3437260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437260)CaDiCaL version: 2.1.3
% 93.88/14.04 % (3437260)Termination reason: Instruction limit
% 93.88/14.04 % (3437260)Termination phase: Saturation
% 93.88/14.04 % (3437260)Time elapsed: 0.089 s
% 93.88/14.04 % (3437260)Peak memory usage: 92 MB
% 93.88/14.04 % (3437260)Instructions burned: 187 (million)
% 93.88/14.04 % (3437262)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1195610407:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2949 on theBenchmark for (2949ds/193Mi)
% 93.88/14.04 % (3437262)Instruction limit reached!
% 93.88/14.04 % (3437262)------------------------------
% 93.88/14.04 % (3437262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437262)CaDiCaL version: 2.1.3
% 93.88/14.04 % (3437262)Termination reason: Instruction limit
% 93.88/14.04 % (3437262)Termination phase: Saturation
% 93.88/14.04 % (3437262)Time elapsed: 0.109 s
% 93.88/14.04 % (3437262)Peak memory usage: 90 MB
% 93.88/14.04 % (3437262)Instructions burned: 196 (million)
% 93.88/14.04 % (3437264)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1948394093:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 93.88/14.04 % (3437241)Instruction limit reached!
% 93.88/14.04 % (3437241)------------------------------
% 93.88/14.04 % (3437241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437241)CaDiCaL version: 2.1.3
% 93.88/14.04 % (3437241)Termination reason: Instruction limit
% 93.88/14.04 % (3437241)Termination phase: Saturation
% 93.88/14.04 % (3437241)Time elapsed: 4.170 s
% 93.88/14.04 % (3437241)Peak memory usage: 259 MB
% 93.88/14.04 % (3437241)Instructions burned: 13196 (million)
% 93.88/14.04 % (3437266)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2349820636:i=12111:sd=1:ss=included_2942 on theBenchmark for (2942ds/12111Mi)
% 93.88/14.04 % (3437251)Instruction limit reached!
% 93.88/14.04 % (3437251)------------------------------
% 93.88/14.04 % (3437251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.88/14.04 % (3437251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.88/14.04 % (3437251)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437251)Termination reason: Instruction limit
% 72.32/16.62 % (3437251)Termination phase: Saturation
% 72.32/16.62 % (3437251)Time elapsed: 3.754 s
% 72.32/16.62 % (3437251)Peak memory usage: 161 MB
% 72.32/16.62 % (3437251)Instructions burned: 6061 (million)
% 72.32/16.62 % (3437268)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=339437018:i=319:kws=precedence:fsr=off_2937 on theBenchmark for (2937ds/319Mi)
% 72.32/16.62 % (3437268)Instruction limit reached!
% 72.32/16.62 % (3437268)------------------------------
% 72.32/16.62 % (3437268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437268)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437268)Termination reason: Instruction limit
% 72.32/16.62 % (3437268)Termination phase: Saturation
% 72.32/16.62 % (3437268)Time elapsed: 0.172 s
% 72.32/16.62 % (3437268)Peak memory usage: 94 MB
% 72.32/16.62 % (3437268)Instructions burned: 320 (million)
% 72.32/16.62 % (3437270)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1368006608:i=2064:ep=RST_2934 on theBenchmark for (2934ds/2064Mi)
% 72.32/16.62 % (3437270)Instruction limit reached!
% 72.32/16.62 % (3437270)------------------------------
% 72.32/16.62 % (3437270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437270)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437270)Termination reason: Instruction limit
% 72.32/16.62 % (3437270)Termination phase: Saturation
% 72.32/16.62 % (3437270)Time elapsed: 0.991 s
% 72.32/16.62 % (3437270)Peak memory usage: 111 MB
% 72.32/16.62 % (3437270)Instructions burned: 2065 (million)
% 72.32/16.62 % (3437272)dis-1011_128_sil=32000:random_seed=2793006923:i=3706:ep=RST:av=off_2922 on theBenchmark for (2922ds/3706Mi)
% 72.32/16.62 % (3437264)Instruction limit reached!
% 72.32/16.62 % (3437264)------------------------------
% 72.32/16.62 % (3437264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437264)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437264)Termination reason: Instruction limit
% 72.32/16.62 % (3437264)Termination phase: Saturation
% 72.32/16.62 % (3437264)Time elapsed: 2.500 s
% 72.32/16.62 % (3437264)Peak memory usage: 99 MB
% 72.32/16.62 % (3437264)Instructions burned: 4851 (million)
% 72.32/16.62 % (3437274)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3923785913:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2920 on theBenchmark for (2920ds/757Mi)
% 72.32/16.62 % (3437274)Instruction limit reached!
% 72.32/16.62 % (3437274)------------------------------
% 72.32/16.62 % (3437274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437274)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437274)Termination reason: Instruction limit
% 72.32/16.62 % (3437274)Termination phase: Saturation
% 72.32/16.62 % (3437274)Time elapsed: 0.602 s
% 72.32/16.62 % (3437274)Peak memory usage: 94 MB
% 72.32/16.62 % (3437274)Instructions burned: 757 (million)
% 72.32/16.62 % (3437276)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1582172547:i=13913:ss=axioms:sgt=8_2912 on theBenchmark for (2912ds/13913Mi)
% 72.32/16.62 % (3437266)Instruction limit reached!
% 72.32/16.62 % (3437266)------------------------------
% 72.32/16.62 % (3437266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437266)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437266)Termination reason: Instruction limit
% 72.32/16.62 % (3437266)Termination phase: Saturation
% 72.32/16.62 % (3437266)Time elapsed: 3.511 s
% 72.32/16.62 % (3437266)Peak memory usage: 319 MB
% 72.32/16.62 % (3437266)Instructions burned: 12112 (million)
% 72.32/16.62 % (3437278)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3017585805:i=9925:aac=none_2905 on theBenchmark for (2905ds/9925Mi)
% 72.32/16.62 % (3437272)Instruction limit reached!
% 72.32/16.62 % (3437272)------------------------------
% 72.32/16.62 % (3437272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437272)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437272)Termination reason: Instruction limit
% 72.32/16.62 % (3437272)Termination phase: Saturation
% 72.32/16.62 % (3437272)Time elapsed: 1.994 s
% 72.32/16.62 % (3437272)Peak memory usage: 99 MB
% 72.32/16.62 % (3437272)Instructions burned: 3707 (million)
% 72.32/16.62 % (3437280)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3513373954:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2901 on theBenchmark for (2901ds/2479Mi)
% 72.32/16.62 % (3437256)Instruction limit reached!
% 72.32/16.62 % (3437256)------------------------------
% 72.32/16.62 % (3437256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437256)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437256)Termination reason: Instruction limit
% 72.32/16.62 % (3437256)Termination phase: Saturation
% 72.32/16.62 % (3437256)Time elapsed: 7.453 s
% 72.32/16.62 % (3437256)Peak memory usage: 262 MB
% 72.32/16.62 % (3437256)Instructions burned: 14156 (million)
% 72.32/16.62 % (3437282)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1906396696:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2894 on theBenchmark for (2894ds/440Mi)
% 72.32/16.62 % (3437282)Instruction limit reached!
% 72.32/16.62 % (3437282)------------------------------
% 72.32/16.62 % (3437282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437282)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437282)Termination reason: Instruction limit
% 72.32/16.62 % (3437282)Termination phase: Saturation
% 72.32/16.62 % (3437282)Time elapsed: 0.251 s
% 72.32/16.62 % (3437282)Peak memory usage: 93 MB
% 72.32/16.62 % (3437282)Instructions burned: 441 (million)
% 72.32/16.62 % (3437284)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2440093762:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2890 on theBenchmark for (2890ds/11145Mi)
% 72.32/16.62 % (3437280)Instruction limit reached!
% 72.32/16.62 % (3437280)------------------------------
% 72.32/16.62 % (3437280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437280)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437280)Termination reason: Instruction limit
% 72.32/16.62 % (3437280)Termination phase: Saturation
% 72.32/16.62 % (3437280)Time elapsed: 1.400 s
% 72.32/16.62 % (3437280)Peak memory usage: 108 MB
% 72.32/16.62 % (3437280)Instructions burned: 2480 (million)
% 72.32/16.62 % (3437286)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2432015075:cts=off:i=3034:av=off:er=known:fsd=on_2885 on theBenchmark for (2885ds/3034Mi)
% 72.32/16.62 % (3437278)Instruction limit reached!
% 72.32/16.62 % (3437278)------------------------------
% 72.32/16.62 % (3437278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437278)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437278)Termination reason: Instruction limit
% 72.32/16.62 % (3437278)Termination phase: Saturation
% 72.32/16.62 % (3437278)Time elapsed: 3.017 s
% 72.32/16.62 % (3437278)Peak memory usage: 219 MB
% 72.32/16.62 % (3437278)Instructions burned: 9928 (million)
% 72.32/16.62 % (3437288)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=656765443:st=2:s2a=on:i=524:s2at=2:ss=axioms_2874 on theBenchmark for (2874ds/524Mi)
% 72.32/16.62 % (3437288)Instruction limit reached!
% 72.32/16.62 % (3437288)------------------------------
% 72.32/16.62 % (3437288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437288)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437288)Termination reason: Instruction limit
% 72.32/16.62 % (3437288)Termination phase: Saturation
% 72.32/16.62 % (3437288)Time elapsed: 0.126 s
% 72.32/16.62 % (3437288)Peak memory usage: 100 MB
% 72.32/16.62 % (3437288)Instructions burned: 526 (million)
% 72.32/16.62 % (3437290)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=553825903:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2871 on theBenchmark for (2871ds/1016Mi)
% 72.32/16.62 % (3437286)Instruction limit reached!
% 72.32/16.62 % (3437286)------------------------------
% 72.32/16.62 % (3437286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437286)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437286)Termination reason: Instruction limit
% 72.32/16.62 % (3437286)Termination phase: Saturation
% 72.32/16.62 % (3437286)Time elapsed: 1.585 s
% 72.32/16.62 % (3437286)Peak memory usage: 150 MB
% 72.32/16.62 % (3437286)Instructions burned: 3035 (million)
% 72.32/16.62 % (3437290)Instruction limit reached!
% 72.32/16.62 % (3437290)------------------------------
% 72.32/16.62 % (3437290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437290)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437290)Termination reason: Instruction limit
% 72.32/16.62 % (3437290)Termination phase: Saturation
% 72.32/16.62 % (3437290)Time elapsed: 0.302 s
% 72.32/16.62 % (3437290)Peak memory usage: 134 MB
% 72.32/16.62 % (3437290)Instructions burned: 1017 (million)
% 72.32/16.62 % (3437292)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3802638685:i=14123:bd=preordered:ins=4_2868 on theBenchmark for (2868ds/14123Mi)
% 72.32/16.62 % (3437293)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3402587129:i=5781:kws=precedence:bd=all:rawr=on_2867 on theBenchmark for (2867ds/5781Mi)
% 72.32/16.62 % (3437293)Instruction limit reached!
% 72.32/16.62 % (3437293)------------------------------
% 72.32/16.62 % (3437293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.32/16.62 % (3437293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.32/16.62 % (3437293)CaDiCaL version: 2.1.3
% 72.32/16.62 % (3437293)Termination reason: Instruction limit
% 72.32/16.62 % (3437293)Termination phase: Saturation
% 72.32/16.62 % (3437293)Time elapsed: 1.805 s
% 72.32/16.62 % (3437293)Peak memory usage: 142 MB
% 72.32/16.62 % (3437293)Instructions burned: 5781 (million)
% 72.32/16.62 % (3437296)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=29972726:i=2448:gtgl=5:bd=preordered:gtg=all_2847 on theBenchmark for (2847ds/2448Mi)
% 72.32/16.62 % (3437202)First to succeed.
% 72.32/16.62 % (3437202)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3437195"
% 72.32/16.62 % (3437202)Refutation found. Thanks to Tanya!
% 72.32/16.62 % SZS status Theorem for theBenchmark
% 72.32/16.62 % SZS output start Proof for theBenchmark
% See solution above
% 112.16/16.72 % (3437202)------------------------------
% 112.16/16.72 % (3437202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.72 % (3437202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.72 % (3437202)CaDiCaL version: 2.1.3
% 112.16/16.72 % (3437202)Termination reason: Refutation
% 112.16/16.72 % (3437202)Time elapsed: 15.301 s
% 112.16/16.72 % (3437202)Peak memory usage: 321 MB
% 112.16/16.72 % (3437202)Instructions burned: 27659 (million)
% 112.16/16.72 % (3437202)------------------------------
% 112.16/16.72 % (3437202)------------------------------
% 112.16/16.72 % (3437195)Success in time 15.762 s
% 112.16/16.72 % Vampire exiting
%------------------------------------------------------------------------------