%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG066+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:22 PM UTC 2026
% Result : Theorem 15.64s 3.07s
% Output : Refutation 16.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 46
% Syntax : Number of formulae : 311 ( 53 unt; 22 def)
% Number of atoms : 1056 ( 99 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1408 ( 663 ~; 648 |; 58 &)
% ( 22 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 23 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 15 con; 0-2 aty)
% Number of variables : 211 ( 0 sgn 211 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f10,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDistr2) ).
fof(f17,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMNeg) ).
fof(f20,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERef) ).
fof(f21,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMon) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMonM) ).
fof(f27,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqPos) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScSqPos) ).
fof(f43,axiom,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0) )
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1726) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1746) ).
fof(f47,axiom,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1800) ).
fof(f49,axiom,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
fof(f53,axiom,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
fof(f54,axiom,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
fof(f55,axiom,
( aScalar0(xN)
& xN = sdtasdt0(xR,xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1949) ).
fof(f57,axiom,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2004) ).
fof(f59,conjecture,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f60,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f61,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(flattening,[],[f60]) ).
fof(f70,plain,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0)
| ~ aNaturalNumber0(X0) )
& xq = sziznziztdt0(xt) ),
inference(ennf_transformation,[],[f43]) ).
fof(f71,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f88,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f93,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(f94,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,[],[f93]) ).
fof(f95,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(f96,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,[],[f95]) ).
fof(f99,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f100,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f102,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f103,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f102]) ).
fof(f109,plain,
! [X0,X1,X2,X3] :
( sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(flattening,[],[f109]) ).
fof(f113,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(f114,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,[],[f113]) ).
fof(f115,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(f116,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f117,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f116]) ).
fof(f120,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(f121,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,[],[f120]) ).
fof(f122,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f140,plain,
aVector0(xq),
inference(cnf_transformation,[],[f70]) ).
fof(f142,plain,
aScalar0(xA),
inference(cnf_transformation,[],[f44]) ).
fof(f147,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[],[f47]) ).
fof(f148,plain,
aScalar0(xD),
inference(cnf_transformation,[],[f47]) ).
fof(f152,plain,
aScalar0(xF),
inference(cnf_transformation,[],[f49]) ).
fof(f158,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f160,plain,
aScalar0(xP),
inference(cnf_transformation,[],[f53]) ).
fof(f161,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[],[f54]) ).
fof(f162,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f163,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[],[f55]) ).
fof(f164,plain,
aScalar0(xN),
inference(cnf_transformation,[],[f55]) ).
fof(f166,plain,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(cnf_transformation,[],[f57]) ).
fof(f168,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(cnf_transformation,[],[f61]) ).
fof(f169,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f183,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f88]) ).
fof(f187,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,[],[f94]) ).
fof(f188,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,[],[f96]) ).
fof(f190,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f191,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f192,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f199,plain,
! [X2,X3,X0,X1] :
( sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(cnf_transformation,[],[f110]) ).
fof(f202,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f206,plain,
! [X0] :
( sz0z00 = smndt0(sz0z00)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f209,plain,
! [X0] :
( sz0z00 = sdtpldt0(X0,smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f211,plain,
! [X0] :
( sz0z00 = sdtasdt0(X0,sz0z00)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f213,plain,
! [X0] :
( sdtpldt0(X0,sz0z00) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f214,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f215,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f217,plain,
! [X0,X1] :
( smndt0(sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f121]) ).
fof(f219,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f224,definition,
( spl2_1
<=> ! [X0] : ~ aScalar0(X0) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f225,plain,
( ! [X0] : ~ aScalar0(X0)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f227,definition,
( spl2_2
<=> sz0z00 = smndt0(sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f229,plain,
( sz0z00 = smndt0(sz0z00)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f230,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f206,f227,f224]) ).
fof(f232,definition,
( spl2_3
<=> ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f233,plain,
( ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( spl2_1
| spl2_3 ),
inference(avatar_split_clause,[],[f202,f232,f224]) ).
fof(f242,definition,
( spl2_5
<=> aScalar0(sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f243,plain,
( aScalar0(sdtpldt0(xR,xS))
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| spl2_5 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f258,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| spl2_5 ),
inference(resolution,[],[f214,f244]) ).
fof(f260,plain,
( ~ aScalar0(xS)
| spl2_5 ),
inference(forward_subsumption_resolution,[],[f258,f158]) ).
fof(f261,plain,
( $false
| spl2_5 ),
inference(forward_subsumption_resolution,[],[f260,f162]) ).
fof(f262,plain,
spl2_5,
inference(avatar_contradiction_clause,[],[f261]) ).
fof(f279,plain,
( ! [X2,X3,X0,X1] :
( sdtasdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X0)) = sdtpldt0(sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X0,X1)),sdtpldt0(sdtasdt0(X2,X3),sdtasdt0(X2,X0)))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl2_3 ),
inference(superposition,[],[f199,f233]) ).
fof(f282,plain,
( ! [X2,X3,X0,X1] :
( sdtasdt0(sdtpldt0(X1,X2),sdtpldt0(X3,X0)) = sdtpldt0(sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X0,X1)),sdtpldt0(sdtasdt0(X2,X3),sdtasdt0(X2,X0)))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3)
| ~ aScalar0(X0) )
| ~ spl2_3 ),
inference(duplicate_literal_removal,[],[f279]) ).
fof(f683,definition,
( spl2_14
<=> sdtlseqdt0(sz0z00,xS) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f684,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f685,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| spl2_14 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f866,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,smndt0(X2))
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(smndt0(X2))
| ~ aScalar0(X2) ),
inference(superposition,[],[f188,f209]) ).
fof(f867,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X2)
| ~ aScalar0(X0) ),
inference(superposition,[],[f188,f209]) ).
fof(f870,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X2) ),
inference(duplicate_literal_removal,[],[f867]) ).
fof(f871,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,smndt0(X2))
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(smndt0(X2)) ),
inference(duplicate_literal_removal,[],[f866]) ).
fof(f872,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(smndt0(X0),X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f870,f219]) ).
fof(f873,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,smndt0(X2))
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f871,f219]) ).
fof(f1016,plain,
( smndt0(xS) = sdtasdt0(smndt0(xF),xD)
| ~ aScalar0(xF)
| ~ aScalar0(xD) ),
inference(superposition,[],[f217,f161]) ).
fof(f1025,plain,
( smndt0(xS) = sdtasdt0(smndt0(xF),xD)
| ~ aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f1016,f152]) ).
fof(f1043,plain,
smndt0(xS) = sdtasdt0(smndt0(xF),xD),
inference(forward_subsumption_resolution,[],[f1025,f148]) ).
fof(f1058,definition,
( spl2_35
<=> sdtlseqdt0(sz0z00,xD) ),
introduced(definition,[new_symbols(definition,[spl2_35])],[avatar_definition]) ).
fof(f1059,plain,
( sdtlseqdt0(sz0z00,xD)
| ~ spl2_35 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1060,plain,
( ~ sdtlseqdt0(sz0z00,xD)
| spl2_35 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1168,definition,
( spl2_37
<=> aScalar0(smndt0(xF)) ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f1169,plain,
( aScalar0(smndt0(xF))
| ~ spl2_37 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1170,plain,
( ~ aScalar0(smndt0(xF))
| spl2_37 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1704,definition,
( spl2_86
<=> sdtlseqdt0(sz0z00,smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f1705,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| ~ spl2_86 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1706,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xS))
| spl2_86 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1931,plain,
( $false
| ~ spl2_1 ),
inference(resolution,[],[f225,f142]) ).
fof(f1940,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f1931]) ).
fof(f2220,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2)
| ~ aScalar0(X0) ),
inference(superposition,[],[f187,f211]) ).
fof(f2221,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) ),
inference(superposition,[],[f187,f211]) ).
fof(f2269,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00) ),
inference(duplicate_literal_removal,[],[f2221]) ).
fof(f2270,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) ),
inference(duplicate_literal_removal,[],[f2220]) ).
fof(f2300,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| ~ sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X1,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f2269,f215]) ).
fof(f2301,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f2270,f191]) ).
fof(f2317,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X1,X2))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(forward_subsumption_resolution,[],[f2301,f215]) ).
fof(f2326,plain,
! [X0] :
( sdtlseqdt0(sz0z00,smndt0(xS))
| ~ sdtlseqdt0(X0,smndt0(xF))
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xF))
| ~ aScalar0(xD) ),
inference(superposition,[],[f2317,f1043]) ).
fof(f2334,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(X0,xF)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(X0)
| ~ aScalar0(xF)
| ~ aScalar0(xD) ),
inference(superposition,[],[f2317,f161]) ).
fof(f2336,plain,
! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,xR)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) ),
inference(superposition,[],[f2317,f163]) ).
fof(f2351,definition,
( spl2_105
<=> ! [X1] :
( ~ sdtlseqdt0(X1,xR)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_105])],[avatar_definition]) ).
fof(f2352,plain,
( ! [X1] :
( ~ sdtlseqdt0(X1,xR)
| ~ aScalar0(X1) )
| ~ spl2_105 ),
inference(avatar_component_clause,[],[f2351]) ).
fof(f2358,definition,
( spl2_107
<=> ! [X1] :
( ~ sdtlseqdt0(X1,xF)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_107])],[avatar_definition]) ).
fof(f2359,plain,
( ! [X1] :
( ~ sdtlseqdt0(X1,xF)
| ~ aScalar0(X1) )
| ~ spl2_107 ),
inference(avatar_component_clause,[],[f2358]) ).
fof(f2381,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xR)
| ~ spl2_105 ),
inference(resolution,[],[f2352,f191]) ).
fof(f2382,plain,
( ~ aScalar0(xR)
| ~ spl2_105 ),
inference(duplicate_literal_removal,[],[f2381]) ).
fof(f2385,plain,
( $false
| ~ spl2_105 ),
inference(forward_subsumption_resolution,[],[f2382,f158]) ).
fof(f2386,plain,
~ spl2_105,
inference(avatar_contradiction_clause,[],[f2385]) ).
fof(f2390,plain,
( ~ aScalar0(xF)
| ~ aScalar0(xF)
| ~ spl2_107 ),
inference(resolution,[],[f2359,f191]) ).
fof(f2391,plain,
( ~ aScalar0(xF)
| ~ spl2_107 ),
inference(duplicate_literal_removal,[],[f2390]) ).
fof(f2394,plain,
( $false
| ~ spl2_107 ),
inference(forward_subsumption_resolution,[],[f2391,f152]) ).
fof(f2395,plain,
~ spl2_107,
inference(avatar_contradiction_clause,[],[f2394]) ).
fof(f2433,plain,
! [X0] :
( sdtlseqdt0(xN,sz0z00)
| ~ sdtlseqdt0(xR,X0)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(xR)
| ~ aScalar0(X0)
| ~ aScalar0(xS) ),
inference(superposition,[],[f2300,f163]) ).
fof(f2450,definition,
( spl2_113
<=> ! [X1] :
( ~ sdtlseqdt0(xR,X1)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_113])],[avatar_definition]) ).
fof(f2451,plain,
( ! [X1] :
( ~ sdtlseqdt0(xR,X1)
| ~ aScalar0(X1) )
| ~ spl2_113 ),
inference(avatar_component_clause,[],[f2450]) ).
fof(f2480,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xR)
| ~ spl2_113 ),
inference(resolution,[],[f2451,f191]) ).
fof(f2481,plain,
( ~ aScalar0(xR)
| ~ spl2_113 ),
inference(duplicate_literal_removal,[],[f2480]) ).
fof(f2484,plain,
( $false
| ~ spl2_113 ),
inference(forward_subsumption_resolution,[],[f2481,f158]) ).
fof(f2485,plain,
~ spl2_113,
inference(avatar_contradiction_clause,[],[f2484]) ).
fof(f2591,definition,
( spl2_130
<=> sdtlseqdt0(sz0z00,xN) ),
introduced(definition,[new_symbols(definition,[spl2_130])],[avatar_definition]) ).
fof(f2593,plain,
( sdtlseqdt0(sz0z00,xN)
| ~ spl2_130 ),
inference(avatar_component_clause,[],[f2591]) ).
fof(f2659,plain,
( ~ aScalar0(xF)
| spl2_37 ),
inference(resolution,[],[f219,f1170]) ).
fof(f2671,plain,
( $false
| spl2_37 ),
inference(forward_subsumption_resolution,[],[f2659,f152]) ).
fof(f2672,plain,
spl2_37,
inference(avatar_contradiction_clause,[],[f2671]) ).
fof(f3012,plain,
! [X0,X1] :
( sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0) ),
inference(superposition,[],[f873,f213]) ).
fof(f3018,plain,
! [X0,X1] :
( sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00) ),
inference(duplicate_literal_removal,[],[f3012]) ).
fof(f3032,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,smndt0(X1))
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f3018,f215]) ).
fof(f3101,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(xS) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f2336,f684]) ).
fof(f3111,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f3101,f158]) ).
fof(f3120,plain,
( ! [X0] :
( sdtlseqdt0(sz0z00,xN)
| ~ sdtlseqdt0(X0,xR)
| ~ aScalar0(X0) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f3111,f162]) ).
fof(f3127,plain,
( spl2_105
| spl2_130
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f3120,f683,f2591,f2351]) ).
fof(f3397,definition,
( spl2_181
<=> sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ),
introduced(definition,[new_symbols(definition,[spl2_181])],[avatar_definition]) ).
fof(f3398,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| ~ spl2_181 ),
inference(avatar_component_clause,[],[f3397]) ).
fof(f3399,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| spl2_181 ),
inference(avatar_component_clause,[],[f3397]) ).
fof(f3405,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| spl2_181 ),
inference(resolution,[],[f3399,f183]) ).
fof(f3416,plain,
( $false
| ~ spl2_5
| spl2_181 ),
inference(forward_subsumption_resolution,[],[f3405,f243]) ).
fof(f3417,plain,
( ~ spl2_5
| spl2_181 ),
inference(avatar_contradiction_clause,[],[f3416]) ).
fof(f3612,definition,
( spl2_186
<=> ! [X1] :
( ~ sdtlseqdt0(X1,smndt0(xF))
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_186])],[avatar_definition]) ).
fof(f3613,plain,
( ! [X1] :
( ~ sdtlseqdt0(X1,smndt0(xF))
| ~ aScalar0(X1) )
| ~ spl2_186 ),
inference(avatar_component_clause,[],[f3612]) ).
fof(f3690,plain,
( ~ aScalar0(smndt0(xF))
| ~ aScalar0(smndt0(xF))
| ~ spl2_186 ),
inference(resolution,[],[f3613,f191]) ).
fof(f3692,plain,
( ~ aScalar0(smndt0(xF))
| ~ spl2_186 ),
inference(duplicate_literal_removal,[],[f3690]) ).
fof(f3696,plain,
( $false
| ~ spl2_37
| ~ spl2_186 ),
inference(forward_subsumption_resolution,[],[f3692,f1169]) ).
fof(f3697,plain,
( ~ spl2_37
| ~ spl2_186 ),
inference(avatar_contradiction_clause,[],[f3696]) ).
fof(f4216,definition,
( spl2_218
<=> sdtlseqdt0(xN,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_218])],[avatar_definition]) ).
fof(f4218,plain,
( sdtlseqdt0(xN,sz0z00)
| ~ spl2_218 ),
inference(avatar_component_clause,[],[f4216]) ).
fof(f5114,definition,
( spl2_280
<=> aScalar0(sdtpldt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_280])],[avatar_definition]) ).
fof(f5115,plain,
( aScalar0(sdtpldt0(xS,xS))
| ~ spl2_280 ),
inference(avatar_component_clause,[],[f5114]) ).
fof(f5116,plain,
( ~ aScalar0(sdtpldt0(xS,xS))
| spl2_280 ),
inference(avatar_component_clause,[],[f5114]) ).
fof(f5163,definition,
( spl2_291
<=> sdtlseqdt0(sz0z00,sdtpldt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_291])],[avatar_definition]) ).
fof(f5164,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xS,xS))
| ~ spl2_291 ),
inference(avatar_component_clause,[],[f5163]) ).
fof(f5165,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xS,xS))
| spl2_291 ),
inference(avatar_component_clause,[],[f5163]) ).
fof(f5168,definition,
( spl2_292
<=> sdtlseqdt0(sdtpldt0(xS,xS),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_292])],[avatar_definition]) ).
fof(f5169,plain,
( sdtlseqdt0(sdtpldt0(xS,xS),sz0z00)
| ~ spl2_292 ),
inference(avatar_component_clause,[],[f5168]) ).
fof(f5170,plain,
( ~ sdtlseqdt0(sdtpldt0(xS,xS),sz0z00)
| spl2_292 ),
inference(avatar_component_clause,[],[f5168]) ).
fof(f5270,plain,
( ~ aScalar0(xS)
| ~ aScalar0(xS)
| spl2_280 ),
inference(resolution,[],[f5116,f214]) ).
fof(f5271,plain,
( ~ aScalar0(xS)
| spl2_280 ),
inference(duplicate_literal_removal,[],[f5270]) ).
fof(f5272,plain,
( $false
| spl2_280 ),
inference(forward_subsumption_resolution,[],[f5271,f162]) ).
fof(f5273,plain,
spl2_280,
inference(avatar_contradiction_clause,[],[f5272]) ).
fof(f5301,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xS)
| ~ sdtlseqdt0(smndt0(X0),xS)
| ~ aScalar0(X0)
| ~ aScalar0(xS)
| ~ aScalar0(xS) )
| spl2_291 ),
inference(resolution,[],[f5165,f872]) ).
fof(f5304,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xS)
| ~ sdtlseqdt0(smndt0(X0),xS)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| spl2_291 ),
inference(duplicate_literal_removal,[],[f5301]) ).
fof(f5307,plain,
( ! [X0] :
( ~ sdtlseqdt0(smndt0(X0),xS)
| ~ sdtlseqdt0(X0,xS)
| ~ aScalar0(X0) )
| spl2_291 ),
inference(forward_subsumption_resolution,[],[f5304,f162]) ).
fof(f5316,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(sz0z00)
| ~ spl2_2
| spl2_291 ),
inference(superposition,[],[f5307,f229]) ).
fof(f5317,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(sz0z00)
| ~ spl2_2
| spl2_291 ),
inference(duplicate_literal_removal,[],[f5316]) ).
fof(f5318,plain,
( ~ aScalar0(sz0z00)
| ~ spl2_2
| ~ spl2_14
| spl2_291 ),
inference(forward_subsumption_resolution,[],[f5317,f684]) ).
fof(f5323,plain,
( $false
| ~ spl2_2
| ~ spl2_14
| spl2_291 ),
inference(forward_subsumption_resolution,[],[f5318,f215]) ).
fof(f5324,plain,
( ~ spl2_2
| ~ spl2_14
| spl2_291 ),
inference(avatar_contradiction_clause,[],[f5323]) ).
fof(f5327,plain,
( ! [X0] :
( ~ sdtlseqdt0(xS,X0)
| ~ sdtlseqdt0(xS,smndt0(X0))
| ~ aScalar0(xS)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| spl2_292 ),
inference(resolution,[],[f5170,f873]) ).
fof(f5330,plain,
( ! [X0] :
( ~ sdtlseqdt0(xS,X0)
| ~ sdtlseqdt0(xS,smndt0(X0))
| ~ aScalar0(xS)
| ~ aScalar0(X0) )
| spl2_292 ),
inference(duplicate_literal_removal,[],[f5327]) ).
fof(f5332,plain,
( ! [X0] :
( ~ sdtlseqdt0(xS,smndt0(X0))
| ~ sdtlseqdt0(xS,X0)
| ~ aScalar0(X0) )
| spl2_292 ),
inference(forward_subsumption_resolution,[],[f5330,f162]) ).
fof(f5339,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(sz0z00)
| ~ spl2_2
| spl2_292 ),
inference(superposition,[],[f5332,f229]) ).
fof(f5340,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(sz0z00)
| ~ spl2_2
| spl2_292 ),
inference(duplicate_literal_removal,[],[f5339]) ).
fof(f5774,plain,
( sdtlseqdt0(sz0z00,xD)
| ~ aVector0(xq) ),
inference(superposition,[],[f169,f147]) ).
fof(f5781,plain,
( ~ aVector0(xq)
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f5774,f1060]) ).
fof(f5791,plain,
( $false
| spl2_35 ),
inference(forward_subsumption_resolution,[],[f5781,f140]) ).
fof(f5792,plain,
spl2_35,
inference(avatar_contradiction_clause,[],[f5791]) ).
fof(f5801,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xF))
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xF))
| ~ aScalar0(xD) )
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f2326,f1706]) ).
fof(f5806,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xF))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xF))
| ~ aScalar0(xD) )
| ~ spl2_35
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f5801,f1059]) ).
fof(f5811,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xF))
| ~ aScalar0(X0)
| ~ aScalar0(xD) )
| ~ spl2_35
| ~ spl2_37
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f5806,f1169]) ).
fof(f5813,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,smndt0(xF))
| ~ aScalar0(X0) )
| ~ spl2_35
| ~ spl2_37
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f5811,f148]) ).
fof(f5815,plain,
( spl2_186
| ~ spl2_35
| ~ spl2_37
| spl2_86 ),
inference(avatar_split_clause,[],[f5813,f1704,f1168,f1058,f3612]) ).
fof(f5822,plain,
( ! [X0] :
( sdtlseqdt0(xN,sz0z00)
| ~ sdtlseqdt0(xR,X0)
| ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(xR)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f2433,f684]) ).
fof(f5827,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| ~ spl2_2
| spl2_292 ),
inference(forward_subsumption_resolution,[],[f5340,f215]) ).
fof(f5830,plain,
( ! [X0] :
( sdtlseqdt0(xN,sz0z00)
| ~ sdtlseqdt0(xR,X0)
| ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f5822,f158]) ).
fof(f5833,definition,
( spl2_325
<=> sdtlseqdt0(xS,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_325])],[avatar_definition]) ).
fof(f5834,plain,
( sdtlseqdt0(xS,sz0z00)
| ~ spl2_325 ),
inference(avatar_component_clause,[],[f5833]) ).
fof(f5835,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| spl2_325 ),
inference(avatar_component_clause,[],[f5833]) ).
fof(f5839,plain,
( ~ spl2_325
| ~ spl2_2
| spl2_292 ),
inference(avatar_split_clause,[],[f5827,f5168,f227,f5833]) ).
fof(f5842,plain,
( ! [X0] :
( sdtlseqdt0(xN,sz0z00)
| ~ sdtlseqdt0(xR,X0)
| ~ sdtlseqdt0(xS,sz0z00)
| ~ aScalar0(X0) )
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f5830,f162]) ).
fof(f5846,plain,
( ~ spl2_325
| spl2_113
| spl2_218
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f5842,f683,f4216,f2450,f5833]) ).
fof(f6041,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xS)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(xS) )
| ~ spl2_86 ),
inference(resolution,[],[f1705,f3032]) ).
fof(f6043,plain,
( ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| ~ sdtlseqdt0(X0,xS)
| ~ aScalar0(X0) )
| ~ spl2_86 ),
inference(forward_subsumption_resolution,[],[f6041,f162]) ).
fof(f7267,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xS,xS))
| sz0z00 = sdtpldt0(xS,xS)
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtpldt0(xS,xS))
| ~ spl2_292 ),
inference(resolution,[],[f190,f5169]) ).
fof(f7282,plain,
( ~ sdtlseqdt0(xN,sdtasdt0(xP,xP))
| xN = sdtasdt0(xP,xP)
| ~ aScalar0(xN)
| ~ aScalar0(sdtasdt0(xP,xP)) ),
inference(resolution,[],[f190,f166]) ).
fof(f7289,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| sz0z00 = xS
| ~ aScalar0(sz0z00)
| ~ aScalar0(xS)
| ~ spl2_325 ),
inference(resolution,[],[f190,f5834]) ).
fof(f7295,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| sz0z00 = xN
| ~ aScalar0(sz0z00)
| ~ aScalar0(xN)
| ~ spl2_218 ),
inference(resolution,[],[f190,f4218]) ).
fof(f7310,plain,
( sz0z00 = xN
| ~ aScalar0(sz0z00)
| ~ aScalar0(xN)
| ~ spl2_130
| ~ spl2_218 ),
inference(forward_subsumption_resolution,[],[f7295,f2593]) ).
fof(f7313,plain,
( sz0z00 = xS
| ~ aScalar0(sz0z00)
| ~ aScalar0(xS)
| ~ spl2_14
| ~ spl2_325 ),
inference(forward_subsumption_resolution,[],[f7289,f684]) ).
fof(f7315,plain,
( ~ sdtlseqdt0(xN,sdtasdt0(xP,xP))
| xN = sdtasdt0(xP,xP)
| ~ aScalar0(sdtasdt0(xP,xP)) ),
inference(forward_subsumption_resolution,[],[f7282,f164]) ).
fof(f7371,plain,
( sz0z00 = sdtpldt0(xS,xS)
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtpldt0(xS,xS))
| ~ spl2_291
| ~ spl2_292 ),
inference(forward_subsumption_resolution,[],[f7267,f5164]) ).
fof(f7417,plain,
( sz0z00 = xN
| ~ aScalar0(xN)
| ~ spl2_130
| ~ spl2_218 ),
inference(forward_subsumption_resolution,[],[f7310,f215]) ).
fof(f7420,plain,
( sz0z00 = xS
| ~ aScalar0(xS)
| ~ spl2_14
| ~ spl2_325 ),
inference(forward_subsumption_resolution,[],[f7313,f215]) ).
fof(f7423,definition,
( spl2_377
<=> aScalar0(sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_377])],[avatar_definition]) ).
fof(f7425,plain,
( ~ aScalar0(sdtasdt0(xP,xP))
| spl2_377 ),
inference(avatar_component_clause,[],[f7423]) ).
fof(f7427,definition,
( spl2_378
<=> xN = sdtasdt0(xP,xP) ),
introduced(definition,[new_symbols(definition,[spl2_378])],[avatar_definition]) ).
fof(f7429,plain,
( xN = sdtasdt0(xP,xP)
| ~ spl2_378 ),
inference(avatar_component_clause,[],[f7427]) ).
fof(f7431,definition,
( spl2_379
<=> sdtlseqdt0(xN,sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_379])],[avatar_definition]) ).
fof(f7433,plain,
( ~ sdtlseqdt0(xN,sdtasdt0(xP,xP))
| spl2_379 ),
inference(avatar_component_clause,[],[f7431]) ).
fof(f7434,plain,
( ~ spl2_377
| spl2_378
| ~ spl2_379 ),
inference(avatar_split_clause,[],[f7315,f7431,f7427,f7423]) ).
fof(f7443,plain,
( sz0z00 = sdtpldt0(xS,xS)
| ~ aScalar0(sdtpldt0(xS,xS))
| ~ spl2_291
| ~ spl2_292 ),
inference(forward_subsumption_resolution,[],[f7371,f215]) ).
fof(f7516,plain,
( sz0z00 = xN
| ~ spl2_130
| ~ spl2_218 ),
inference(forward_subsumption_resolution,[],[f7417,f164]) ).
fof(f7517,plain,
( sz0z00 = xS
| ~ spl2_14
| ~ spl2_325 ),
inference(forward_subsumption_resolution,[],[f7420,f162]) ).
fof(f7534,plain,
( sz0z00 = sdtpldt0(xS,xS)
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292 ),
inference(forward_subsumption_resolution,[],[f7443,f5115]) ).
fof(f7553,plain,
( sz0z00 = sdtpldt0(sz0z00,sz0z00)
| ~ spl2_14
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325 ),
inference(forward_demodulation,[],[f7534,f7517]) ).
fof(f7564,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xP,xP))
| ~ spl2_130
| ~ spl2_218
| spl2_379 ),
inference(forward_demodulation,[],[f7433,f7516]) ).
fof(f7592,plain,
( ~ sdtlseqdt0(xS,xS)
| ~ aScalar0(xS)
| ~ spl2_86
| spl2_325 ),
inference(resolution,[],[f5835,f6043]) ).
fof(f7596,plain,
( ~ aScalar0(xS)
| ~ spl2_86
| spl2_325 ),
inference(forward_subsumption_resolution,[],[f7592,f191]) ).
fof(f7598,plain,
( $false
| ~ spl2_86
| spl2_325 ),
inference(forward_subsumption_resolution,[],[f7596,f162]) ).
fof(f7599,plain,
( ~ spl2_86
| spl2_325 ),
inference(avatar_contradiction_clause,[],[f7598]) ).
fof(f7711,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,sz0z00),sdtpldt0(xR,sz0z00)))
| ~ spl2_14
| ~ spl2_325 ),
inference(superposition,[],[f168,f7517]) ).
fof(f7743,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xR,sz0z00),sdtpldt0(xR,sz0z00)))
| ~ spl2_14
| ~ spl2_181
| ~ spl2_325 ),
inference(superposition,[],[f3398,f7517]) ).
fof(f8263,plain,
( ~ aScalar0(xP)
| ~ spl2_130
| ~ spl2_218
| spl2_379 ),
inference(resolution,[],[f7564,f183]) ).
fof(f8280,plain,
( $false
| ~ spl2_130
| ~ spl2_218
| spl2_379 ),
inference(forward_subsumption_resolution,[],[f8263,f160]) ).
fof(f8281,plain,
( ~ spl2_130
| ~ spl2_218
| spl2_379 ),
inference(avatar_contradiction_clause,[],[f8280]) ).
fof(f8302,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| spl2_377 ),
inference(resolution,[],[f7425,f192]) ).
fof(f8303,plain,
( ~ aScalar0(xP)
| spl2_377 ),
inference(duplicate_literal_removal,[],[f8302]) ).
fof(f8304,plain,
( $false
| spl2_377 ),
inference(forward_subsumption_resolution,[],[f8303,f160]) ).
fof(f8305,plain,
spl2_377,
inference(avatar_contradiction_clause,[],[f8304]) ).
fof(f8306,plain,
( sz0z00 = sdtasdt0(xP,xP)
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(forward_demodulation,[],[f7429,f7516]) ).
fof(f11719,plain,
( ! [X0,X1] :
( sdtasdt0(sdtpldt0(X0,xP),sdtpldt0(X1,xP)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xP,X0)),sdtpldt0(sdtasdt0(xP,X1),sz0z00))
| ~ aScalar0(X0)
| ~ aScalar0(xP)
| ~ aScalar0(X1)
| ~ aScalar0(xP) )
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(superposition,[],[f282,f8306]) ).
fof(f11758,plain,
( ! [X0,X1] :
( sdtasdt0(sdtpldt0(X0,xP),sdtpldt0(X1,xP)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xP,X0)),sdtpldt0(sdtasdt0(xP,X1),sz0z00))
| ~ aScalar0(X0)
| ~ aScalar0(xP)
| ~ aScalar0(X1) )
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(duplicate_literal_removal,[],[f11719]) ).
fof(f11799,plain,
( ! [X0,X1] :
( sdtasdt0(sdtpldt0(X0,xP),sdtpldt0(X1,xP)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(xP,X0)),sdtpldt0(sdtasdt0(xP,X1),sz0z00))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(forward_subsumption_resolution,[],[f11758,f160]) ).
fof(f12069,plain,
( sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtpldt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sz0z00,sz0z00))
| ~ aScalar0(xP)
| ~ aScalar0(xP)
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(superposition,[],[f11799,f8306]) ).
fof(f12120,plain,
( sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtpldt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sz0z00,sz0z00))
| ~ aScalar0(xP)
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(duplicate_literal_removal,[],[f12069]) ).
fof(f12147,plain,
( sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtpldt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sz0z00,sz0z00))
| ~ spl2_3
| ~ spl2_130
| ~ spl2_218
| ~ spl2_378 ),
inference(forward_subsumption_resolution,[],[f12120,f160]) ).
fof(f12175,plain,
( sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtpldt0(sz0z00,sz0z00)
| ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(forward_demodulation,[],[f12147,f7553]) ).
fof(f12197,plain,
( sz0z00 = sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))
| ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(forward_demodulation,[],[f12175,f7553]) ).
fof(f14337,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtpldt0(xR,sz0z00),sdtpldt0(xR,sz0z00)))
| ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(forward_demodulation,[],[f7711,f12197]) ).
fof(f14347,plain,
( $false
| ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_181
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(forward_subsumption_resolution,[],[f14337,f7743]) ).
fof(f14348,plain,
( ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_181
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(avatar_contradiction_clause,[],[f14347]) ).
fof(f14355,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xF)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(X0)
| ~ aScalar0(xF)
| ~ aScalar0(xD) )
| spl2_14 ),
inference(forward_subsumption_resolution,[],[f2334,f685]) ).
fof(f14696,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xF)
| ~ aScalar0(X0)
| ~ aScalar0(xF)
| ~ aScalar0(xD) )
| spl2_14
| ~ spl2_35 ),
inference(forward_subsumption_resolution,[],[f14355,f1059]) ).
fof(f14895,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xF)
| ~ aScalar0(X0)
| ~ aScalar0(xD) )
| spl2_14
| ~ spl2_35 ),
inference(forward_subsumption_resolution,[],[f14696,f152]) ).
fof(f15021,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xF)
| ~ aScalar0(X0) )
| spl2_14
| ~ spl2_35 ),
inference(forward_subsumption_resolution,[],[f14895,f148]) ).
fof(f15086,plain,
( spl2_107
| spl2_14
| ~ spl2_35 ),
inference(avatar_split_clause,[],[f15021,f1058,f683,f2358]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f230]) ).
cnf(s2,plain,
( spl2_1
| spl2_3 ),
inference(sat_conversion,[],[f234]) ).
cnf(s5,plain,
spl2_5,
inference(sat_conversion,[],[f262]) ).
cnf(s94,plain,
~ spl2_1,
inference(sat_conversion,[],[f1940]) ).
cnf(s123,plain,
~ spl2_105,
inference(sat_conversion,[],[f2386]) ).
cnf(s124,plain,
~ spl2_107,
inference(sat_conversion,[],[f2395]) ).
cnf(s131,plain,
~ spl2_113,
inference(sat_conversion,[],[f2485]) ).
cnf(s145,plain,
spl2_37,
inference(sat_conversion,[],[f2672]) ).
cnf(s162,plain,
( ~ spl2_14
| spl2_105
| spl2_130 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s186,plain,
( ~ spl2_5
| spl2_181 ),
inference(sat_conversion,[],[f3417]) ).
cnf(s202,plain,
( ~ spl2_37
| ~ spl2_186 ),
inference(sat_conversion,[],[f3697]) ).
cnf(s313,plain,
spl2_280,
inference(sat_conversion,[],[f5273]) ).
cnf(s318,plain,
( ~ spl2_2
| ~ spl2_14
| spl2_291 ),
inference(sat_conversion,[],[f5324]) ).
cnf(s327,plain,
spl2_35,
inference(sat_conversion,[],[f5792]) ).
cnf(s329,plain,
( ~ spl2_35
| ~ spl2_37
| spl2_86
| spl2_186 ),
inference(sat_conversion,[],[f5815]) ).
cnf(s333,plain,
( ~ spl2_2
| spl2_292
| ~ spl2_325 ),
inference(sat_conversion,[],[f5839]) ).
cnf(s334,plain,
( ~ spl2_14
| spl2_113
| spl2_218
| ~ spl2_325 ),
inference(sat_conversion,[],[f5846]) ).
cnf(s371,plain,
( ~ spl2_377
| spl2_378
| ~ spl2_379 ),
inference(sat_conversion,[],[f7434]) ).
cnf(s386,plain,
( ~ spl2_86
| spl2_325 ),
inference(sat_conversion,[],[f7599]) ).
cnf(s413,plain,
( ~ spl2_130
| ~ spl2_218
| spl2_379 ),
inference(sat_conversion,[],[f8281]) ).
cnf(s420,plain,
spl2_377,
inference(sat_conversion,[],[f8305]) ).
cnf(s535,plain,
( ~ spl2_3
| ~ spl2_14
| ~ spl2_130
| ~ spl2_181
| ~ spl2_218
| ~ spl2_280
| ~ spl2_291
| ~ spl2_292
| ~ spl2_325
| ~ spl2_378 ),
inference(sat_conversion,[],[f14348]) ).
cnf(s543,plain,
( spl2_14
| ~ spl2_35
| spl2_107 ),
inference(sat_conversion,[],[f15086]) ).
cnf(s582,plain,
( spl2_378
| ~ spl2_379 ),
inference(rat,[],[s371,s420]) ).
cnf(s626,plain,
~ spl2_186,
inference(rat,[],[s202,s145]) ).
cnf(s628,plain,
spl2_86,
inference(rat,[],[s329,s145,s327,s626]) ).
cnf(s629,plain,
spl2_325,
inference(rat,[],[s386,s628]) ).
cnf(s645,plain,
spl2_14,
inference(rat,[],[s543,s327,s124]) ).
cnf(s648,plain,
spl2_218,
inference(rat,[],[s334,s629,s131,s645]) ).
cnf(s667,plain,
spl2_130,
inference(rat,[],[s162,s645,s123]) ).
cnf(s670,plain,
spl2_379,
inference(rat,[],[s413,s648,s667]) ).
cnf(s674,plain,
spl2_378,
inference(rat,[],[s582,s670]) ).
cnf(s789,plain,
spl2_181,
inference(rat,[],[s186,s5]) ).
cnf(s801,plain,
spl2_3,
inference(rat,[],[s2,s94]) ).
cnf(s809,plain,
spl2_2,
inference(rat,[],[s1,s94]) ).
cnf(s823,plain,
spl2_292,
inference(rat,[],[s333,s629,s809]) ).
cnf(s824,plain,
spl2_291,
inference(rat,[],[s318,s645,s809]) ).
cnf(s829,plain,
$false,
inference(rat,[],[s535,s674,s629,s801,s789,s313,s648,s667,s645,s823,s824]) ).
fof(f15207,plain,
$false,
inference(avatar_sat_refutation,[],[s829]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG066+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n008.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 23:08:25 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.00/2.90 % (1715581)Detected formulas, will run a generic FOF schedule.
% 14.00/2.90 % (1715589)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3791594854:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.00/2.90 % (1715589)Instruction limit reached!
% 14.00/2.90 % (1715589)------------------------------
% 14.00/2.90 % (1715589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.90 % (1715589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.90 % (1715589)CaDiCaL version: 2.1.3
% 14.00/2.90 % (1715589)Termination reason: Instruction limit
% 14.00/2.90 % (1715589)Termination phase: Saturation
% 14.00/2.90 % (1715589)Time elapsed: 0.035 s
% 14.00/2.90 % (1715589)Peak memory usage: 89 MB
% 14.00/2.90 % (1715589)Instructions burned: 110 (million)
% 14.00/2.90 % (1715586)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=2531222092:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.00/2.90 % (1715587)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=3713424232:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.00/2.90 % (1715590)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2049402454:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.00/2.90 % (1715588)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=3912770988:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.00/2.90 % (1715591)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2771555829:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.00/2.90 % (1715592)dis-21_1_sil=8000:lcm=predicate:random_seed=3540268319: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)
% 14.00/2.90 % (1715590)Instruction limit reached!
% 14.00/2.90 % (1715590)------------------------------
% 14.00/2.90 % (1715590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.90 % (1715590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.90 % (1715590)CaDiCaL version: 2.1.3
% 14.00/2.90 % (1715590)Termination reason: Instruction limit
% 14.00/2.90 % (1715590)Termination phase: Saturation
% 14.00/2.90 % (1715590)Time elapsed: 0.064 s
% 14.00/2.90 % (1715590)Peak memory usage: 88 MB
% 14.00/2.90 % (1715590)Instructions burned: 119 (million)
% 14.00/2.90 % (1715592)Instruction limit reached!
% 14.00/2.90 % (1715592)------------------------------
% 14.00/2.90 % (1715592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.90 % (1715592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.90 % (1715592)CaDiCaL version: 2.1.3
% 14.00/2.90 % (1715592)Termination reason: Instruction limit
% 14.00/2.90 % (1715592)Termination phase: Saturation
% 14.00/2.90 % (1715592)Time elapsed: 0.066 s
% 14.00/2.90 % (1715592)Peak memory usage: 89 MB
% 14.00/2.90 % (1715592)Instructions burned: 129 (million)
% 14.00/2.90 % (1715591)Instruction limit reached!
% 14.00/2.90 % (1715591)------------------------------
% 14.00/2.90 % (1715591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.90 % (1715591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.90 % (1715591)CaDiCaL version: 2.1.3
% 14.00/2.90 % (1715591)Termination reason: Instruction limit
% 14.00/2.90 % (1715591)Termination phase: Saturation
% 14.00/2.90 % (1715591)Time elapsed: 0.092 s
% 14.00/2.90 % (1715591)Peak memory usage: 90 MB
% 14.00/2.90 % (1715591)Instructions burned: 140 (million)
% 14.00/2.90 % (1715594)lrs+10_1_sil=8000:sp=occurrence:random_seed=700509918:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 14.00/2.90 % (1715594)Instruction limit reached!
% 14.00/2.90 % (1715594)------------------------------
% 14.00/2.90 % (1715594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.90 % (1715601)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1533115658:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 14.00/2.90 % (1715594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.90 % (1715594)CaDiCaL version: 2.1.3
% 14.00/2.90 % (1715594)Termination reason: Instruction limit
% 14.00/2.90 % (1715594)Termination phase: Saturation
% 15.64/3.07 % (1715594)Time elapsed: 0.095 s
% 15.64/3.07 % (1715594)Peak memory usage: 92 MB
% 15.64/3.07 % (1715594)Instructions burned: 287 (million)
% 15.64/3.07 % (1715602)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3429096673:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.64/3.07 % (1715603)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=168713074:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 15.64/3.07 % (1715601)Instruction limit reached!
% 15.64/3.07 % (1715601)------------------------------
% 15.64/3.07 % (1715601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715601)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715601)Termination reason: Instruction limit
% 15.64/3.07 % (1715601)Termination phase: Saturation
% 15.64/3.07 % (1715601)Time elapsed: 0.073 s
% 15.64/3.07 % (1715601)Peak memory usage: 91 MB
% 15.64/3.07 % (1715601)Instructions burned: 158 (million)
% 15.64/3.07 % (1715606)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=302100437:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 15.64/3.07 % (1715603)Instruction limit reached!
% 15.64/3.07 % (1715603)------------------------------
% 15.64/3.07 % (1715603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715603)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715603)Termination reason: Instruction limit
% 15.64/3.07 % (1715603)Termination phase: Saturation
% 15.64/3.07 % (1715603)Time elapsed: 0.112 s
% 15.64/3.07 % (1715603)Peak memory usage: 94 MB
% 15.64/3.07 % (1715603)Instructions burned: 250 (million)
% 15.64/3.07 % (1715606)Instruction limit reached!
% 15.64/3.07 % (1715606)------------------------------
% 15.64/3.07 % (1715606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715606)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715606)Termination reason: Instruction limit
% 15.64/3.07 % (1715606)Termination phase: Saturation
% 15.64/3.07 % (1715606)Time elapsed: 0.091 s
% 15.64/3.07 % (1715606)Peak memory usage: 90 MB
% 15.64/3.07 % (1715606)Instructions burned: 297 (million)
% 15.64/3.07 % (1715602)Instruction limit reached!
% 15.64/3.07 % (1715602)------------------------------
% 15.64/3.07 % (1715602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715602)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715602)Termination reason: Instruction limit
% 15.64/3.07 % (1715602)Termination phase: Saturation
% 15.64/3.07 % (1715602)Time elapsed: 0.187 s
% 15.64/3.07 % (1715602)Peak memory usage: 93 MB
% 15.64/3.07 % (1715602)Instructions burned: 325 (million)
% 15.64/3.07 % (1715609)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=215384312:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.64/3.07 % (1715611)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=141029296:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 15.64/3.07 % (1715613)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4252163691:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 15.64/3.07 % (1715613)Refutation not found, incomplete strategy
% 15.64/3.07 % (1715613)------------------------------
% 15.64/3.07 % (1715613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715613)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715613)Termination reason: Refutation not found, incomplete strategy
% 15.64/3.07 % (1715613)Time elapsed: 0.002 s
% 15.64/3.07 % (1715613)Peak memory usage: 88 MB
% 15.64/3.07 % (1715613)Instructions burned: 3 (million)
% 15.64/3.07 % (1715612)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3034277588:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 15.64/3.07 % (1715611)Instruction limit reached!
% 15.64/3.07 % (1715611)------------------------------
% 15.64/3.07 % (1715611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715611)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715611)Termination reason: Instruction limit
% 15.64/3.07 % (1715611)Termination phase: Saturation
% 15.64/3.07 % (1715611)Time elapsed: 0.075 s
% 15.64/3.07 % (1715611)Peak memory usage: 91 MB
% 15.64/3.07 % (1715611)Instructions burned: 114 (million)
% 15.64/3.07 % (1715612)Instruction limit reached!
% 15.64/3.07 % (1715612)------------------------------
% 15.64/3.07 % (1715612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715612)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715612)Termination reason: Instruction limit
% 15.64/3.07 % (1715612)Termination phase: Saturation
% 15.64/3.07 % (1715612)Time elapsed: 0.066 s
% 15.64/3.07 % (1715612)Peak memory usage: 89 MB
% 15.64/3.07 % (1715612)Instructions burned: 128 (million)
% 15.64/3.07 % (1715613)------------------------------
% 15.64/3.07 % (1715613)------------------------------
% 15.64/3.07 % (1715618)lrs+10_1_sil=8000:sp=occurrence:random_seed=2713444917:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 15.64/3.07 % (1715619)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2794158888:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 15.64/3.07 % (1715620)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3338867065:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 15.64/3.07 % (1715619)Instruction limit reached!
% 15.64/3.07 % (1715619)------------------------------
% 15.64/3.07 % (1715619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715619)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715619)Termination reason: Instruction limit
% 15.64/3.07 % (1715619)Termination phase: Saturation
% 15.64/3.07 % (1715619)Time elapsed: 0.246 s
% 15.64/3.07 % (1715619)Peak memory usage: 94 MB
% 15.64/3.07 % (1715619)Instructions burned: 438 (million)
% 15.64/3.07 % (1715624)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2472132016:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 15.64/3.07 % (1715618)Instruction limit reached!
% 15.64/3.07 % (1715618)------------------------------
% 15.64/3.07 % (1715618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715618)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715618)Termination reason: Instruction limit
% 15.64/3.07 % (1715618)Termination phase: Saturation
% 15.64/3.07 % (1715618)Time elapsed: 0.502 s
% 15.64/3.07 % (1715618)Peak memory usage: 103 MB
% 15.64/3.07 % (1715618)Instructions burned: 908 (million)
% 15.64/3.07 % (1715624)Instruction limit reached!
% 15.64/3.07 % (1715624)------------------------------
% 15.64/3.07 % (1715624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715624)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715624)Termination reason: Instruction limit
% 15.64/3.07 % (1715624)Termination phase: Saturation
% 15.64/3.07 % (1715624)Time elapsed: 0.059 s
% 15.64/3.07 % (1715624)Peak memory usage: 91 MB
% 15.64/3.07 % (1715624)Instructions burned: 134 (million)
% 15.64/3.07 % (1715626)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1324475081:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 15.64/3.07 % (1715627)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1525616356:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 15.64/3.07 % (1715626)Instruction limit reached!
% 15.64/3.07 % (1715626)------------------------------
% 15.64/3.07 % (1715626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715626)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715626)Termination reason: Instruction limit
% 15.64/3.07 % (1715626)Termination phase: Saturation
% 15.64/3.07 % (1715626)Time elapsed: 0.294 s
% 15.64/3.07 % (1715626)Peak memory usage: 92 MB
% 15.64/3.07 % (1715626)Instructions burned: 593 (million)
% 15.64/3.07 % (1715620)First to succeed.
% 15.64/3.07 % (1715620)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1715581"
% 15.64/3.07 % (1715609)Instruction limit reached!
% 15.64/3.07 % (1715609)------------------------------
% 15.64/3.07 % (1715609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715609)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715609)Termination reason: Instruction limit
% 15.64/3.07 % (1715609)Termination phase: Saturation
% 15.64/3.07 % (1715609)Time elapsed: 1.415 s
% 15.64/3.07 % (1715609)Peak memory usage: 144 MB
% 15.64/3.07 % (1715609)Instructions burned: 2351 (million)
% 15.64/3.07 % (1715630)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=1491915953:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 15.64/3.07 % (1715630)Instruction limit reached!
% 15.64/3.07 % (1715630)------------------------------
% 15.64/3.07 % (1715630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.07 % (1715630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.07 % (1715630)CaDiCaL version: 2.1.3
% 15.64/3.07 % (1715630)Termination reason: Instruction limit
% 15.64/3.07 % (1715630)Termination phase: Saturation
% 15.64/3.07 % (1715630)Time elapsed: 0.068 s
% 15.64/3.07 % (1715630)Peak memory usage: 90 MB
% 15.64/3.07 % (1715630)Instructions burned: 126 (million)
% 15.64/3.07 % (1715620)Refutation found. Thanks to Tanya!
% 15.64/3.07 % SZS status Theorem for theBenchmark
% 15.64/3.07 % SZS output start Proof for theBenchmark
% See solution above
% 16.09/3.27 % (1715620)------------------------------
% 16.09/3.27 % (1715620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.09/3.27 % (1715620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/3.27 % (1715620)CaDiCaL version: 2.1.3
% 16.09/3.27 % (1715620)Termination reason: Refutation
% 16.09/3.27 % (1715620)Time elapsed: 1.055 s
% 16.09/3.27 % (1715620)Peak memory usage: 151 MB
% 16.09/3.27 % (1715620)Instructions burned: 3166 (million)
% 16.09/3.27 % (1715620)------------------------------
% 16.09/3.27 % (1715620)------------------------------
% 16.09/3.27 % (1715581)Success in time 2.197 s
% 16.09/3.27 % Vampire exiting
%------------------------------------------------------------------------------