%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG061+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:54 PM UTC 2026
% Result : Theorem 169.55s 34.15s
% Output : Refutation 169.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 40
% Syntax : Number of formulae : 247 ( 56 unt; 13 def)
% Number of atoms : 762 ( 121 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 938 ( 423 ~; 419 |; 65 &)
% ( 13 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 14 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 14 con; 0-2 aty)
% Number of variables : 127 ( 0 sgn 127 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(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(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMonM) ).
fof(f25,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETot) ).
fof(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/sandbox2/benchmark/theBenchmark.p',mPosMon) ).
fof(f27,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqPos) ).
fof(f28,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(sz0z00,X0)
& sdtlseqdt0(sz0z00,X1)
& sdtasdt0(X0,X0) = sdtasdt0(X1,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqrt) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScSqPos) ).
fof(f42,axiom,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0) )
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1709) ).
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(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1766) ).
fof(f46,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1783) ).
fof(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(f50,axiom,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1854) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
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(f58,axiom,
( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)
& sdtasdt0(smndt0(xS),xR) = smndt0(xN)
& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2144) ).
fof(f59,axiom,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2180) ).
fof(f60,conjecture,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f61,negated_conjecture,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(negated_conjecture,[status(cth)],[f60]) ).
fof(f67,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(flattening,[],[f61]) ).
fof(f76,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f77,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f79,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(f80,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(f81,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,[],[f80]) ).
fof(f90,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f91,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f92,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f91]) ).
fof(f97,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(f98,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,[],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f100,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f99]) ).
fof(f101,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(f102,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,[],[f101]) ).
fof(f103,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f104,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f105,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f104]) ).
fof(f119,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f122,plain,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0)
| ~ aNaturalNumber0(X0) )
& xp = sziznziztdt0(xs) ),
inference(ennf_transformation,[],[f42]) ).
fof(f123,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(f136,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f138,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f139,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f144,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(sz0z00,X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f145,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(X0,sz0z00) ),
inference(cnf_transformation,[],[f79]) ).
fof(f146,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(sz0z00,X0) = X0 ),
inference(cnf_transformation,[],[f79]) ).
fof(f147,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,sz0z00) = X0 ),
inference(cnf_transformation,[],[f79]) ).
fof(f150,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f81]) ).
fof(f158,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f90]) ).
fof(f159,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| X0 = X1
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f92]) ).
fof(f162,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,[],[f98]) ).
fof(f163,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f164,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f166,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f167,plain,
! [X0,X1] :
( sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| X0 = X1
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f179,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f188,plain,
aVector0(xp),
inference(cnf_transformation,[],[f122]) ).
fof(f192,plain,
aVector0(xq),
inference(cnf_transformation,[],[f123]) ).
fof(f194,plain,
aScalar0(xA),
inference(cnf_transformation,[],[f44]) ).
fof(f196,plain,
aScalar0(xB),
inference(cnf_transformation,[],[f45]) ).
fof(f197,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[],[f46]) ).
fof(f198,plain,
aScalar0(xC),
inference(cnf_transformation,[],[f46]) ).
fof(f199,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[],[f47]) ).
fof(f200,plain,
aScalar0(xD),
inference(cnf_transformation,[],[f47]) ).
fof(f203,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[],[f49]) ).
fof(f204,plain,
aScalar0(xF),
inference(cnf_transformation,[],[f49]) ).
fof(f205,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[],[f50]) ).
fof(f206,plain,
aScalar0(xG),
inference(cnf_transformation,[],[f50]) ).
fof(f209,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[],[f52]) ).
fof(f210,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f213,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[],[f54]) ).
fof(f214,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f215,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[],[f55]) ).
fof(f216,plain,
aScalar0(xN),
inference(cnf_transformation,[],[f55]) ).
fof(f219,plain,
sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS),
inference(cnf_transformation,[],[f58]) ).
fof(f220,plain,
smndt0(xN) = sdtasdt0(smndt0(xS),xR),
inference(cnf_transformation,[],[f58]) ).
fof(f221,plain,
sdtasdt0(xR,smndt0(xS)) = smndt0(xN),
inference(cnf_transformation,[],[f58]) ).
fof(f222,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
inference(cnf_transformation,[],[f59]) ).
fof(f223,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(cnf_transformation,[],[f67]) ).
fof(f240,definition,
( spl2_1
<=> ! [X0] : ~ aScalar0(X0) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f241,plain,
( ! [X0] : ~ aScalar0(X0)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f274,plain,
sz0z00 = sdtasdt0(sz0z00,xR),
inference(resolution,[],[f144,f210]) ).
fof(f324,plain,
( sdtlseqdt0(sz0z00,xF)
| ~ aScalar0(xA) ),
inference(superposition,[],[f166,f203]) ).
fof(f325,plain,
( sdtlseqdt0(sz0z00,xG)
| ~ aScalar0(xB) ),
inference(superposition,[],[f166,f205]) ).
fof(f326,plain,
sdtlseqdt0(sz0z00,xG),
inference(forward_subsumption_resolution,[],[f325,f196]) ).
fof(f327,plain,
sdtlseqdt0(sz0z00,xF),
inference(forward_subsumption_resolution,[],[f324,f194]) ).
fof(f328,plain,
( sdtlseqdt0(sz0z00,xC)
| ~ aVector0(xp) ),
inference(superposition,[],[f179,f197]) ).
fof(f329,plain,
( sdtlseqdt0(sz0z00,xD)
| ~ aVector0(xq) ),
inference(superposition,[],[f179,f199]) ).
fof(f330,plain,
sdtlseqdt0(sz0z00,xD),
inference(forward_subsumption_resolution,[],[f329,f192]) ).
fof(f331,plain,
sdtlseqdt0(sz0z00,xC),
inference(forward_subsumption_resolution,[],[f328,f188]) ).
fof(f350,plain,
( aScalar0(smndt0(xN))
| ~ aScalar0(xR)
| ~ aScalar0(smndt0(xS)) ),
inference(superposition,[],[f138,f221]) ).
fof(f353,plain,
( aScalar0(smndt0(xN))
| ~ aScalar0(smndt0(xS)) ),
inference(forward_subsumption_resolution,[],[f350,f210]) ).
fof(f418,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(smndt0(xS)) ),
inference(superposition,[],[f138,f219]) ).
fof(f419,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS)) ),
inference(duplicate_literal_removal,[],[f418]) ).
fof(f446,plain,
( $false
| ~ spl2_1 ),
inference(resolution,[],[f241,f136]) ).
fof(f475,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f446]) ).
fof(f513,definition,
( spl2_4
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f514,plain,
( ! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) )
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl2_1
| spl2_4 ),
inference(avatar_split_clause,[],[f150,f513,f240]) ).
fof(f547,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,xR) = sdtpldt0(xR,X0) )
| ~ spl2_4 ),
inference(resolution,[],[f514,f210]) ).
fof(f550,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,xN) = sdtpldt0(xN,X0) )
| ~ spl2_4 ),
inference(resolution,[],[f514,f216]) ).
fof(f718,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xC)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(superposition,[],[f164,f209]) ).
fof(f720,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xF)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(xF)
| ~ aScalar0(xD) ),
inference(superposition,[],[f164,f213]) ).
fof(f728,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(xF)
| ~ aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f720,f327]) ).
fof(f730,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f718,f331]) ).
fof(f734,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(xF)
| ~ aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f728,f330]) ).
fof(f736,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f730,f326]) ).
fof(f738,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f734,f204]) ).
fof(f739,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f736,f198]) ).
fof(f740,plain,
sdtlseqdt0(sz0z00,xS),
inference(forward_subsumption_resolution,[],[f738,f200]) ).
fof(f741,plain,
sdtlseqdt0(sz0z00,xR),
inference(forward_subsumption_resolution,[],[f739,f206]) ).
fof(f980,plain,
! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,smndt0(xS))
| smndt0(xS) = X0
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xS)) ),
inference(superposition,[],[f167,f219]) ).
fof(f1042,plain,
! [X0,X1] :
( sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| ~ sdtlseqdt0(smndt0(xS),X0)
| ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(xR,X1)
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(X1) ),
inference(superposition,[],[f162,f220]) ).
fof(f1049,plain,
! [X0,X1] :
( sdtlseqdt0(xR,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xC,X0)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(xG,X1)
| ~ aScalar0(xC)
| ~ aScalar0(X0)
| ~ aScalar0(xG)
| ~ aScalar0(X1) ),
inference(superposition,[],[f162,f209]) ).
fof(f1076,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| ~ sdtlseqdt0(X0,smndt0(xS))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X1,xR)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(X1)
| ~ aScalar0(xR) ),
inference(superposition,[],[f162,f220]) ).
fof(f1124,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| ~ sdtlseqdt0(X0,smndt0(xS))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X1,xR)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1076,f210]) ).
fof(f1151,plain,
! [X0,X1] :
( sdtlseqdt0(xR,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xC,X0)
| ~ sdtlseqdt0(xG,X1)
| ~ aScalar0(xC)
| ~ aScalar0(X0)
| ~ aScalar0(xG)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1049,f326]) ).
fof(f1157,plain,
! [X0,X1] :
( sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| ~ sdtlseqdt0(smndt0(xS),X0)
| ~ sdtlseqdt0(xR,X1)
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1042,f741]) ).
fof(f1214,plain,
! [X0,X1] :
( sdtlseqdt0(xR,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xC,X0)
| ~ sdtlseqdt0(xG,X1)
| ~ aScalar0(X0)
| ~ aScalar0(xG)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1151,f198]) ).
fof(f1218,plain,
! [X0,X1] :
( sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| ~ sdtlseqdt0(smndt0(xS),X0)
| ~ sdtlseqdt0(xR,X1)
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1157,f210]) ).
fof(f1245,plain,
! [X0,X1] :
( sdtlseqdt0(xR,sdtasdt0(X0,X1))
| ~ sdtlseqdt0(xC,X0)
| ~ sdtlseqdt0(xG,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1214,f206]) ).
fof(f1557,definition,
( spl2_5
<=> aScalar0(smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f1558,plain,
( aScalar0(smndt0(xS))
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1559,plain,
( ~ aScalar0(smndt0(xS))
| spl2_5 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1561,definition,
( spl2_6
<=> aScalar0(smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f1563,plain,
( aScalar0(smndt0(xN))
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f1561]) ).
fof(f1564,plain,
( ~ spl2_5
| spl2_6 ),
inference(avatar_split_clause,[],[f353,f1561,f1557]) ).
fof(f1913,definition,
( spl2_7
<=> aScalar0(sdtasdt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f1915,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f1913]) ).
fof(f1916,plain,
( ~ spl2_5
| spl2_7 ),
inference(avatar_split_clause,[],[f419,f1913,f1557]) ).
fof(f1917,plain,
( ~ aScalar0(xS)
| spl2_5 ),
inference(resolution,[],[f1559,f139]) ).
fof(f1918,plain,
( $false
| spl2_5 ),
inference(forward_subsumption_resolution,[],[f1917,f214]) ).
fof(f1919,plain,
spl2_5,
inference(avatar_contradiction_clause,[],[f1918]) ).
fof(f1924,plain,
( sz0z00 = sdtasdt0(smndt0(xS),sz0z00)
| ~ spl2_5 ),
inference(resolution,[],[f1558,f145]) ).
fof(f1964,plain,
( sdtasdt0(xS,xS) = sdtpldt0(sz0z00,sdtasdt0(xS,xS))
| ~ spl2_7 ),
inference(resolution,[],[f1915,f146]) ).
fof(f1965,plain,
( sdtasdt0(xS,xS) = sdtpldt0(sdtasdt0(xS,xS),sz0z00)
| ~ spl2_7 ),
inference(resolution,[],[f1915,f147]) ).
fof(f2738,plain,
( sdtpldt0(xS,xR) = sdtpldt0(xR,xS)
| ~ spl2_4 ),
inference(resolution,[],[f547,f214]) ).
fof(f2814,plain,
( sdtpldt0(sdtasdt0(xS,xS),xN) = sdtpldt0(xN,sdtasdt0(xS,xS))
| ~ spl2_4
| ~ spl2_7 ),
inference(resolution,[],[f550,f1915]) ).
fof(f3202,definition,
( spl2_22
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
fof(f3203,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| spl2_22 ),
inference(avatar_component_clause,[],[f3202]) ).
fof(f3204,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f3202]) ).
fof(f3425,definition,
( spl2_27
<=> sdtlseqdt0(sz0z00,smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f3427,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xS))
| spl2_27 ),
inference(avatar_component_clause,[],[f3425]) ).
fof(f9002,definition,
( spl2_37
<=> sdtlseqdt0(sz0z00,smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f9003,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| spl2_37 ),
inference(avatar_component_clause,[],[f9002]) ).
fof(f9004,plain,
( sdtlseqdt0(sz0z00,smndt0(xN))
| ~ spl2_37 ),
inference(avatar_component_clause,[],[f9002]) ).
fof(f19795,plain,
( sdtlseqdt0(xR,xR)
| ~ sdtlseqdt0(xC,xC)
| ~ sdtlseqdt0(xG,xG)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(superposition,[],[f1245,f209]) ).
fof(f19889,plain,
( sdtlseqdt0(xR,xR)
| ~ sdtlseqdt0(xG,xG)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19795,f158]) ).
fof(f19965,plain,
( sdtlseqdt0(xR,xR)
| ~ aScalar0(xC)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19889,f158]) ).
fof(f20014,plain,
( sdtlseqdt0(xR,xR)
| ~ aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19965,f198]) ).
fof(f20018,plain,
sdtlseqdt0(xR,xR),
inference(forward_subsumption_resolution,[],[f20014,f206]) ).
fof(f37285,definition,
( spl2_112
<=> ! [X0,X1] :
( sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xR,X1)
| ~ sdtlseqdt0(smndt0(xS),X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_112])],[avatar_definition]) ).
fof(f37286,plain,
( ! [X0,X1] :
( sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(xR,X1)
| ~ sdtlseqdt0(smndt0(xS),X0) )
| ~ spl2_112 ),
inference(avatar_component_clause,[],[f37285]) ).
fof(f37287,plain,
( ~ spl2_5
| spl2_112 ),
inference(avatar_split_clause,[],[f1218,f37285,f1557]) ).
fof(f37328,plain,
( sdtlseqdt0(smndt0(xN),sz0z00)
| ~ aScalar0(xR)
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(xR,xR)
| ~ sdtlseqdt0(smndt0(xS),sz0z00)
| ~ spl2_112 ),
inference(superposition,[],[f37286,f274]) ).
fof(f37589,plain,
( sdtlseqdt0(smndt0(xN),sz0z00)
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(xR,xR)
| ~ sdtlseqdt0(smndt0(xS),sz0z00)
| ~ spl2_112 ),
inference(forward_subsumption_resolution,[],[f37328,f210]) ).
fof(f37712,plain,
( sdtlseqdt0(smndt0(xN),sz0z00)
| ~ sdtlseqdt0(xR,xR)
| ~ sdtlseqdt0(smndt0(xS),sz0z00)
| ~ spl2_112 ),
inference(forward_subsumption_resolution,[],[f37589,f136]) ).
fof(f37752,plain,
( sdtlseqdt0(smndt0(xN),sz0z00)
| ~ sdtlseqdt0(smndt0(xS),sz0z00)
| ~ spl2_112 ),
inference(forward_subsumption_resolution,[],[f37712,f20018]) ).
fof(f37775,definition,
( spl2_113
<=> sdtlseqdt0(smndt0(xS),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_113])],[avatar_definition]) ).
fof(f37777,plain,
( ~ sdtlseqdt0(smndt0(xS),sz0z00)
| spl2_113 ),
inference(avatar_component_clause,[],[f37775]) ).
fof(f37779,definition,
( spl2_114
<=> sdtlseqdt0(smndt0(xN),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_114])],[avatar_definition]) ).
fof(f37781,plain,
( sdtlseqdt0(smndt0(xN),sz0z00)
| ~ spl2_114 ),
inference(avatar_component_clause,[],[f37779]) ).
fof(f37782,plain,
( ~ spl2_113
| spl2_114
| ~ spl2_112 ),
inference(avatar_split_clause,[],[f37752,f37285,f37779,f37775]) ).
fof(f37800,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| ~ aScalar0(sz0z00)
| ~ aScalar0(smndt0(xS))
| spl2_113 ),
inference(resolution,[],[f37777,f163]) ).
fof(f38625,definition,
( spl2_115
<=> ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| ~ aScalar0(X0)
| smndt0(xS) = X0
| ~ sdtlseqdt0(sz0z00,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_115])],[avatar_definition]) ).
fof(f38626,plain,
( ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| ~ aScalar0(X0)
| smndt0(xS) = X0
| ~ sdtlseqdt0(sz0z00,X0) )
| ~ spl2_115 ),
inference(avatar_component_clause,[],[f38625]) ).
fof(f38627,plain,
( ~ spl2_5
| ~ spl2_27
| spl2_115 ),
inference(avatar_split_clause,[],[f980,f38625,f3425,f1557]) ).
fof(f38638,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(smndt0(xS))
| spl2_27
| spl2_113 ),
inference(forward_subsumption_resolution,[],[f37800,f3427]) ).
fof(f38645,plain,
( ~ aScalar0(smndt0(xS))
| spl2_27
| spl2_113 ),
inference(forward_subsumption_resolution,[],[f38638,f136]) ).
fof(f38647,plain,
( $false
| ~ spl2_5
| spl2_27
| spl2_113 ),
inference(forward_subsumption_resolution,[],[f38645,f1558]) ).
fof(f38648,plain,
( ~ spl2_5
| spl2_27
| spl2_113 ),
inference(avatar_contradiction_clause,[],[f38647]) ).
fof(f39969,definition,
( spl2_117
<=> ! [X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,xR)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X0,smndt0(xS)) ) ),
introduced(definition,[new_symbols(definition,[spl2_117])],[avatar_definition]) ).
fof(f39970,plain,
( ! [X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,xR)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(X0,smndt0(xS)) )
| ~ spl2_117 ),
inference(avatar_component_clause,[],[f39969]) ).
fof(f39971,plain,
( ~ spl2_5
| spl2_117 ),
inference(avatar_split_clause,[],[f1124,f39969,f1557]) ).
fof(f40060,plain,
( sdtlseqdt0(sz0z00,smndt0(xN))
| ~ aScalar0(sz0z00)
| ~ aScalar0(smndt0(xS))
| ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| ~ spl2_117 ),
inference(superposition,[],[f39970,f1924]) ).
fof(f40532,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| sz0z00 = smndt0(xN)
| ~ aScalar0(smndt0(xN))
| ~ aScalar0(sz0z00)
| ~ spl2_114 ),
inference(resolution,[],[f37781,f159]) ).
fof(f40533,plain,
( sz0z00 = smndt0(xN)
| ~ aScalar0(smndt0(xN))
| ~ aScalar0(sz0z00)
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f40532,f9004]) ).
fof(f40540,plain,
( sz0z00 = smndt0(xN)
| ~ aScalar0(sz0z00)
| ~ spl2_6
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f40533,f1563]) ).
fof(f40545,plain,
( sz0z00 = smndt0(xN)
| ~ spl2_6
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f40540,f136]) ).
fof(f41120,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sz0z00),sdtpldt0(sz0z00,sdtasdt0(xS,xS)))
| ~ spl2_6
| ~ spl2_37
| ~ spl2_114 ),
inference(superposition,[],[f222,f40545]) ).
fof(f41121,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sz0z00),sdtpldt0(sdtasdt0(xS,xS),sz0z00))
| ~ spl2_6
| ~ spl2_37
| ~ spl2_114 ),
inference(superposition,[],[f223,f40545]) ).
fof(f41139,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sz0z00),sdtasdt0(xS,xS))
| ~ spl2_6
| ~ spl2_7
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_demodulation,[],[f41121,f1965]) ).
fof(f41140,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sz0z00),sdtasdt0(xS,xS))
| ~ spl2_6
| ~ spl2_7
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_demodulation,[],[f41120,f1964]) ).
fof(f41141,plain,
( $false
| ~ spl2_6
| ~ spl2_7
| ~ spl2_37
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f41140,f41139]) ).
fof(f41142,plain,
( ~ spl2_6
| ~ spl2_7
| ~ spl2_37
| ~ spl2_114 ),
inference(avatar_contradiction_clause,[],[f41141]) ).
fof(f41157,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(smndt0(xS))
| ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f40060,f9003]) ).
fof(f41189,plain,
( ~ aScalar0(smndt0(xS))
| ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f41157,f136]) ).
fof(f41221,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f41189,f1558]) ).
fof(f41253,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f41221,f741]) ).
fof(f41285,plain,
( ~ sdtlseqdt0(smndt0(xS),smndt0(xS))
| ~ spl2_5
| ~ spl2_22
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f41253,f3204]) ).
fof(f41924,plain,
( ~ aScalar0(sz0z00)
| spl2_22 ),
inference(resolution,[],[f3203,f158]) ).
fof(f41930,plain,
( $false
| spl2_22 ),
inference(forward_subsumption_resolution,[],[f41924,f136]) ).
fof(f41931,plain,
spl2_22,
inference(avatar_contradiction_clause,[],[f41930]) ).
fof(f51584,plain,
( ~ aScalar0(smndt0(xS))
| ~ spl2_5
| ~ spl2_22
| spl2_37
| ~ spl2_117 ),
inference(resolution,[],[f41285,f158]) ).
fof(f51590,plain,
( $false
| ~ spl2_5
| ~ spl2_22
| spl2_37
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f51584,f1558]) ).
fof(f51591,plain,
( ~ spl2_5
| ~ spl2_22
| spl2_37
| ~ spl2_117 ),
inference(avatar_contradiction_clause,[],[f51590]) ).
fof(f51627,plain,
( ~ aScalar0(xS)
| xS = smndt0(xS)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ spl2_115 ),
inference(equality_resolution,[],[f38626]) ).
fof(f51628,plain,
( xS = smndt0(xS)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f51627,f214]) ).
fof(f51632,plain,
( xS = smndt0(xS)
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f51628,f740]) ).
fof(f52192,plain,
( sdtasdt0(xR,xS) = smndt0(xN)
| ~ spl2_115 ),
inference(superposition,[],[f221,f51632]) ).
fof(f52216,plain,
( xN = smndt0(xN)
| ~ spl2_115 ),
inference(forward_demodulation,[],[f52192,f215]) ).
fof(f53894,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_115 ),
inference(superposition,[],[f222,f52216]) ).
fof(f53895,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xS),xN))
| ~ spl2_115 ),
inference(superposition,[],[f223,f52216]) ).
fof(f53920,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(forward_demodulation,[],[f53895,f2814]) ).
fof(f53921,plain,
( sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_115 ),
inference(forward_demodulation,[],[f53894,f51632]) ).
fof(f53922,plain,
( sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(forward_demodulation,[],[f53920,f51632]) ).
fof(f53923,plain,
( sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_4
| ~ spl2_115 ),
inference(forward_demodulation,[],[f53921,f2738]) ).
fof(f53924,plain,
( sdtasdt0(sdtpldt0(xS,xR),sdtpldt0(xS,xR)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(xN,sdtasdt0(xS,xS)))
| ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(forward_demodulation,[],[f53922,f2738]) ).
fof(f53925,plain,
( $false
| ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f53924,f53923]) ).
fof(f53926,plain,
( ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(avatar_contradiction_clause,[],[f53925]) ).
cnf(s15,plain,
~ spl2_1,
inference(sat_conversion,[],[f475]) ).
cnf(s16,plain,
( spl2_1
| spl2_4 ),
inference(sat_conversion,[],[f515]) ).
cnf(s17,plain,
( ~ spl2_5
| spl2_6 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s18,plain,
( ~ spl2_5
| spl2_7 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s19,plain,
spl2_5,
inference(sat_conversion,[],[f1919]) ).
cnf(s120,plain,
( ~ spl2_5
| spl2_112 ),
inference(sat_conversion,[],[f37287]) ).
cnf(s121,plain,
( ~ spl2_112
| ~ spl2_113
| spl2_114 ),
inference(sat_conversion,[],[f37782]) ).
cnf(s124,plain,
( ~ spl2_5
| ~ spl2_27
| spl2_115 ),
inference(sat_conversion,[],[f38627]) ).
cnf(s126,plain,
( ~ spl2_5
| spl2_27
| spl2_113 ),
inference(sat_conversion,[],[f38648]) ).
cnf(s129,plain,
( ~ spl2_5
| spl2_117 ),
inference(sat_conversion,[],[f39971]) ).
cnf(s130,plain,
( ~ spl2_6
| ~ spl2_7
| ~ spl2_37
| ~ spl2_114 ),
inference(sat_conversion,[],[f41142]) ).
cnf(s132,plain,
spl2_22,
inference(sat_conversion,[],[f41931]) ).
cnf(s147,plain,
( ~ spl2_5
| ~ spl2_22
| spl2_37
| ~ spl2_117 ),
inference(sat_conversion,[],[f51591]) ).
cnf(s151,plain,
( ~ spl2_4
| ~ spl2_7
| ~ spl2_115 ),
inference(sat_conversion,[],[f53926]) ).
cnf(s167,plain,
spl2_117,
inference(rat,[],[s129,s19]) ).
cnf(s169,plain,
spl2_112,
inference(rat,[],[s120,s19]) ).
cnf(s171,plain,
spl2_37,
inference(rat,[],[s147,s19,s132,s167]) ).
cnf(s172,plain,
spl2_7,
inference(rat,[],[s18,s19]) ).
cnf(s173,plain,
spl2_6,
inference(rat,[],[s17,s19]) ).
cnf(s176,plain,
~ spl2_114,
inference(rat,[],[s130,s172,s171,s173]) ).
cnf(s178,plain,
~ spl2_113,
inference(rat,[],[s121,s169,s176]) ).
cnf(s179,plain,
spl2_27,
inference(rat,[],[s126,s19,s178]) ).
cnf(s182,plain,
spl2_115,
inference(rat,[],[s124,s19,s179]) ).
cnf(s184,plain,
~ spl2_4,
inference(rat,[],[s151,s172,s182]) ).
cnf(s186,plain,
spl2_1,
inference(rat,[],[s16,s184]) ).
cnf(s187,plain,
$false,
inference(rat,[],[s15,s186]) ).
fof(f53927,plain,
$false,
inference(avatar_sat_refutation,[],[s187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG061+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n017.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 22:59:20 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.27/2.37 % (3056775)Will run a generic schedule for satisfiability detection.
% 13.27/2.37 % (3056783)dis+10_1_sil=32000:sp=arity:random_seed=2881003869:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.27/2.37 % (3056781)% WARNING: option uhcvi not known.
% 13.27/2.37 % (3056780)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2928581608_2999 on theBenchmark for (2999ds/0Mi)
% 13.27/2.37 % (3056784)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4128598865:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.27/2.37 % (3056781)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3404038850:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.27/2.37 % (3056785)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2111731604:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.27/2.37 % (3056782)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=167161455:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.27/2.37 % (3056786)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1240880091:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.27/2.37 % TRYING [1]
% 13.27/2.37 % TRYING [2]
% 13.27/2.37 % TRYING [3]
% 13.27/2.37 % (3056783)Instruction limit reached!
% 13.27/2.37 % (3056783)------------------------------
% 13.27/2.37 % (3056783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.27/2.37 % (3056783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.37 % (3056783)CaDiCaL version: 2.1.3
% 13.27/2.37 % (3056783)Termination reason: Instruction limit
% 13.27/2.37 % (3056783)Termination phase: Saturation
% 13.27/2.37 % (3056783)Time elapsed: 0.035 s
% 13.27/2.37 % (3056783)Peak memory usage: 13 MB
% 13.27/2.37 % (3056783)Instructions burned: 104 (million)
% 13.27/2.37 % TRYING [4]
% 13.27/2.37 % (3056794)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=835230512:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.27/2.37 % TRYING [1]
% 13.27/2.37 % TRYING [2]
% 13.27/2.37 % TRYING [3]
% 13.27/2.37 % TRYING [4]
% 13.27/2.37 % (3056784)Instruction limit reached!
% 13.27/2.37 % (3056784)------------------------------
% 13.27/2.37 % (3056784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.27/2.37 % (3056784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.37 % (3056784)CaDiCaL version: 2.1.3
% 13.27/2.37 % (3056784)Termination reason: Instruction limit
% 13.27/2.37 % (3056784)Termination phase: Saturation
% 13.27/2.37 % (3056784)Time elapsed: 0.068 s
% 13.27/2.37 % (3056784)Peak memory usage: 13 MB
% 13.27/2.37 % (3056784)Instructions burned: 116 (million)
% 13.27/2.37 % (3056785)Instruction limit reached!
% 13.27/2.37 % (3056785)------------------------------
% 13.27/2.37 % (3056785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.27/2.37 % (3056785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.37 % (3056785)CaDiCaL version: 2.1.3
% 13.27/2.37 % (3056785)Termination reason: Instruction limit
% 13.27/2.37 % (3056785)Termination phase: Saturation
% 13.27/2.37 % (3056785)Time elapsed: 0.069 s
% 13.27/2.37 % (3056785)Peak memory usage: 13 MB
% 13.27/2.37 % (3056785)Instructions burned: 131 (million)
% 13.27/2.37 % TRYING [5]
% 13.27/2.37 % TRYING [5]
% 13.27/2.37 % (3056796)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2659880550:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.27/2.37 % (3056797)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2143598557:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.27/2.37 % (3056786)Instruction limit reached!
% 13.27/2.37 % (3056786)------------------------------
% 13.27/2.37 % (3056786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.27/2.37 % (3056786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.37 % (3056786)CaDiCaL version: 2.1.3
% 13.27/2.37 % (3056786)Termination reason: Instruction limit
% 13.27/2.37 % (3056786)Termination phase: Saturation
% 13.27/2.37 % (3056786)Time elapsed: 0.098 s
% 13.27/2.37 % (3056786)Peak memory usage: 14 MB
% 13.27/2.37 % (3056786)Instructions burned: 159 (million)
% 13.27/2.37 % (3056800)ott-21_1_sil=16000:fs=off:random_seed=3165715960:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.27/2.37 % (3056796)Instruction limit reached!
% 13.27/2.37 % (3056796)------------------------------
% 13.27/2.37 % (3056796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056796)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056796)Termination reason: Instruction limit
% 35.98/5.56 % (3056796)Termination phase: Saturation
% 35.98/5.56 % (3056796)Time elapsed: 0.060 s
% 35.98/5.56 % (3056796)Peak memory usage: 12 MB
% 35.98/5.56 % (3056796)Instructions burned: 131 (million)
% 35.98/5.56 % (3056802)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4278372215:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 35.98/5.56 % TRYING [6]
% 35.98/5.56 % (3056794)Instruction limit reached!
% 35.98/5.56 % (3056794)------------------------------
% 35.98/5.56 % (3056794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056794)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056794)Termination reason: Instruction limit
% 35.98/5.56 % (3056794)Termination phase: Finite model building constraint generation
% 35.98/5.56 % (3056794)Time elapsed: 0.141 s
% 35.98/5.56 % (3056794)Peak memory usage: 37 MB
% 35.98/5.56 % (3056794)Instructions burned: 717 (million)
% 35.98/5.56 % (3056804)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2161292477:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.98/5.56 % TRYING [1]
% 35.98/5.56 % TRYING [2]
% 35.98/5.56 % TRYING [3]
% 35.98/5.56 % (3056800)Instruction limit reached!
% 35.98/5.56 % (3056800)------------------------------
% 35.98/5.56 % (3056800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056800)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056800)Termination reason: Instruction limit
% 35.98/5.56 % (3056800)Termination phase: Saturation
% 35.98/5.56 % (3056800)Time elapsed: 0.088 s
% 35.98/5.56 % (3056800)Peak memory usage: 13 MB
% 35.98/5.56 % (3056800)Instructions burned: 180 (million)
% 35.98/5.56 % (3056806)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3156226073:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 35.98/5.56 % TRYING [4]
% 35.98/5.56 % TRYING [6]
% 35.98/5.56 % TRYING [5]
% 35.98/5.56 % (3056804)Instruction limit reached!
% 35.98/5.56 % (3056804)------------------------------
% 35.98/5.56 % (3056804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056804)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056804)Termination reason: Instruction limit
% 35.98/5.56 % (3056804)Termination phase: Finite model building constraint generation
% 35.98/5.56 % (3056804)Time elapsed: 0.173 s
% 35.98/5.56 % (3056804)Peak memory usage: 20 MB
% 35.98/5.56 % (3056804)Instructions burned: 868 (million)
% 35.98/5.56 % (3056808)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=207697926:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 35.98/5.56 % (3056802)Instruction limit reached!
% 35.98/5.56 % (3056802)------------------------------
% 35.98/5.56 % (3056802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056802)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056802)Termination reason: Instruction limit
% 35.98/5.56 % (3056802)Termination phase: Saturation
% 35.98/5.56 % (3056802)Time elapsed: 0.284 s
% 35.98/5.56 % (3056802)Peak memory usage: 15 MB
% 35.98/5.56 % (3056802)Instructions burned: 478 (million)
% 35.98/5.56 % (3056810)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1509762695:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 35.98/5.56 % (3056797)Instruction limit reached!
% 35.98/5.56 % (3056797)------------------------------
% 35.98/5.56 % (3056797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.98/5.56 % (3056797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.56 % (3056797)CaDiCaL version: 2.1.3
% 35.98/5.56 % (3056797)Termination reason: Instruction limit
% 35.98/5.56 % (3056797)Termination phase: Saturation
% 35.98/5.56 % (3056797)Time elapsed: 0.390 s
% 35.98/5.56 % (3056797)Peak memory usage: 21 MB
% 35.98/5.56 % (3056797)Instructions burned: 684 (million)
% 35.98/5.56 % (3056812)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=996903893:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 35.98/5.56 % (3056808)Instruction limit reached!
% 62.24/9.29 % (3056808)------------------------------
% 62.24/9.29 % (3056808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056808)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056808)Termination reason: Instruction limit
% 62.24/9.29 % (3056808)Termination phase: Finite model building constraint generation
% 62.24/9.29 % (3056808)Time elapsed: 0.237 s
% 62.24/9.29 % (3056808)Peak memory usage: 107 MB
% 62.24/9.29 % (3056808)Instructions burned: 892 (million)
% 62.24/9.29 % (3056814)fmb+10_1_sil=64000:random_seed=2199312599:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 62.24/9.29 % TRYING [7]
% 62.24/9.29 % TRYING [1]
% 62.24/9.29 % TRYING [2]
% 62.24/9.29 % TRYING [3]
% 62.24/9.29 % TRYING [4]
% 62.24/9.29 % TRYING [5]
% 62.24/9.29 % (3056810)Instruction limit reached!
% 62.24/9.29 % (3056810)------------------------------
% 62.24/9.29 % (3056810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056810)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056810)Termination reason: Instruction limit
% 62.24/9.29 % (3056810)Termination phase: Saturation
% 62.24/9.29 % (3056810)Time elapsed: 0.368 s
% 62.24/9.29 % (3056810)Peak memory usage: 19 MB
% 62.24/9.29 % (3056810)Instructions burned: 693 (million)
% 62.24/9.29 % (3056806)Instruction limit reached!
% 62.24/9.29 % (3056806)------------------------------
% 62.24/9.29 % (3056806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056806)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056806)Termination reason: Instruction limit
% 62.24/9.29 % (3056806)Termination phase: Saturation
% 62.24/9.29 % (3056806)Time elapsed: 0.625 s
% 62.24/9.29 % (3056806)Peak memory usage: 28 MB
% 62.24/9.29 % (3056806)Instructions burned: 1180 (million)
% 62.24/9.29 % (3056816)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3401904754:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 62.24/9.29 % TRYING [20]
% 62.24/9.29 % (3056817)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=462951730:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 62.24/9.29 % TRYING [8]
% 62.24/9.29 % (3056812)Instruction limit reached!
% 62.24/9.29 % (3056812)------------------------------
% 62.24/9.29 % (3056812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056812)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056812)Termination reason: Instruction limit
% 62.24/9.29 % (3056812)Termination phase: Saturation
% 62.24/9.29 % (3056812)Time elapsed: 0.496 s
% 62.24/9.29 % (3056812)Peak memory usage: 21 MB
% 62.24/9.29 % (3056812)Instructions burned: 879 (million)
% 62.24/9.29 % (3056820)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1773453845:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 62.24/9.29 % (3056817)Instruction limit reached!
% 62.24/9.29 % (3056817)------------------------------
% 62.24/9.29 % (3056817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056817)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056817)Termination reason: Instruction limit
% 62.24/9.29 % (3056817)Termination phase: Finite model building constraint generation
% 62.24/9.29 % (3056817)Time elapsed: 0.305 s
% 62.24/9.29 % (3056817)Peak memory usage: 63 MB
% 62.24/9.29 % (3056817)Instructions burned: 922 (million)
% 62.24/9.29 % (3056822)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=631393953:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 62.24/9.29 % TRYING [6]
% 62.24/9.29 % TRYING [8]
% 62.24/9.29 % (3056822)Instruction limit reached!
% 62.24/9.29 % (3056822)------------------------------
% 62.24/9.29 % (3056822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.24/9.29 % (3056822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.24/9.29 % (3056822)CaDiCaL version: 2.1.3
% 62.24/9.29 % (3056822)Termination reason: Instruction limit
% 62.24/9.29 % (3056822)Termination phase: Saturation
% 62.24/9.29 % (3056822)Time elapsed: 0.679 s
% 62.24/9.29 % (3056822)Peak memory usage: 19 MB
% 62.24/9.29 % (3056822)Instructions burned: 1472 (million)
% 62.24/9.29 % (3056824)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2582851023:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 187.13/26.89 % (3056824)Cannot represent all propositional literals internally
% 187.13/26.89 % (3056824)Refutation not found, incomplete strategy
% 187.13/26.89 % (3056824)------------------------------
% 187.13/26.89 % (3056824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056824)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056824)Termination reason: Refutation not found, incomplete strategy
% 187.13/26.89 % (3056824)Time elapsed: 0.008 s
% 187.13/26.89 % (3056824)Peak memory usage: 11 MB
% 187.13/26.89 % (3056824)Instructions burned: 16 (million)
% 187.13/26.89 % (3056824)------------------------------
% 187.13/26.89 % (3056824)------------------------------
% 187.13/26.89 % (3056826)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=664666178:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 187.13/26.89 % TRYING [16]
% 187.13/26.89 % TRYING [7]
% 187.13/26.89 % (3056826)Instruction limit reached!
% 187.13/26.89 % (3056826)------------------------------
% 187.13/26.89 % (3056826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056826)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056826)Termination reason: Instruction limit
% 187.13/26.89 % (3056826)Termination phase: Finite model building constraint generation
% 187.13/26.89 % (3056826)Time elapsed: 0.763 s
% 187.13/26.89 % (3056826)Peak memory usage: 146 MB
% 187.13/26.89 % (3056826)Instructions burned: 2177 (million)
% 187.13/26.89 % (3056828)ott-2_1_sil=16000:newcnf=on:random_seed=3712551205:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 187.13/26.89 % (3056828)Instruction limit reached!
% 187.13/26.89 % (3056828)------------------------------
% 187.13/26.89 % (3056828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056828)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056828)Termination reason: Instruction limit
% 187.13/26.89 % (3056828)Termination phase: Saturation
% 187.13/26.89 % (3056828)Time elapsed: 0.447 s
% 187.13/26.89 % (3056828)Peak memory usage: 26 MB
% 187.13/26.89 % (3056828)Instructions burned: 871 (million)
% 187.13/26.89 % (3056830)ott+10_1_sil=32000:tgt=ground:random_seed=30032211:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 187.13/26.89 % (3056820)Instruction limit reached!
% 187.13/26.89 % (3056820)------------------------------
% 187.13/26.89 % (3056820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056820)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056820)Termination reason: Instruction limit
% 187.13/26.89 % (3056820)Termination phase: Saturation
% 187.13/26.89 % (3056820)Time elapsed: 2.505 s
% 187.13/26.89 % (3056820)Peak memory usage: 57 MB
% 187.13/26.89 % (3056820)Instructions burned: 5131 (million)
% 187.13/26.89 % (3056832)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1690443334:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 187.13/26.89 % TRYING [1]
% 187.13/26.89 % TRYING [2]
% 187.13/26.89 % TRYING [3]
% 187.13/26.89 % TRYING [4]
% 187.13/26.89 % TRYING [5]
% 187.13/26.89 % TRYING [6]
% 187.13/26.89 % (3056816)Instruction limit reached!
% 187.13/26.89 % (3056816)------------------------------
% 187.13/26.89 % (3056816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056816)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056816)Termination reason: Instruction limit
% 187.13/26.89 % (3056816)Termination phase: Finite model building constraint generation
% 187.13/26.89 % (3056816)Time elapsed: 3.076 s
% 187.13/26.89 % (3056816)Peak memory usage: 484 MB
% 187.13/26.89 % (3056816)Instructions burned: 9515 (million)
% 187.13/26.89 % (3056834)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3968097099:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 187.13/26.89 % TRYING [7]
% 187.13/26.89 % TRYING [9]
% 187.13/26.89 % (3056814)Instruction limit reached!
% 187.13/26.89 % (3056814)------------------------------
% 187.13/26.89 % (3056814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.13/26.89 % (3056814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.13/26.89 % (3056814)CaDiCaL version: 2.1.3
% 187.13/26.89 % (3056814)Termination reason: Instruction limit
% 187.13/26.89 % (3056814)Termination phase: Finite model building SAT solving
% 187.13/26.89 % (3056814)Time elapsed: 4.464 s
% 169.55/34.15 % (3056814)Peak memory usage: 152 MB
% 169.55/34.15 % (3056814)Instructions burned: 22068 (million)
% 169.55/34.15 % (3056836)dis+21_1_sil=32000:sas=cadical:random_seed=2659373775:i=3773:amm=off_2948 on theBenchmark for (2948ds/3773Mi)
% 169.55/34.15 % TRYING [8]
% 169.55/34.15 % (3056834)Instruction limit reached!
% 169.55/34.15 % (3056834)------------------------------
% 169.55/34.15 % (3056834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056834)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056834)Termination reason: Instruction limit
% 169.55/34.15 % (3056834)Termination phase: Saturation
% 169.55/34.15 % (3056834)Time elapsed: 1.791 s
% 169.55/34.15 % (3056834)Peak memory usage: 42 MB
% 169.55/34.15 % (3056834)Instructions burned: 3513 (million)
% 169.55/34.15 % (3056838)ott+11_1_sil=16000:gs=on:random_seed=1270496548:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2941 on theBenchmark for (2941ds/2251Mi)
% 169.55/34.15 % (3056830)Instruction limit reached!
% 169.55/34.15 % (3056830)------------------------------
% 169.55/34.15 % (3056830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056830)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056830)Termination reason: Instruction limit
% 169.55/34.15 % (3056830)Termination phase: Saturation
% 169.55/34.15 % (3056830)Time elapsed: 2.778 s
% 169.55/34.15 % (3056830)Peak memory usage: 75 MB
% 169.55/34.15 % (3056830)Instructions burned: 5115 (million)
% 169.55/34.15 % (3056840)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2833935140:fmbsr=1.6:i=67534_2939 on theBenchmark for (2939ds/67534Mi)
% 169.55/34.15 % TRYING [7]
% 169.55/34.15 % (3056836)Instruction limit reached!
% 169.55/34.15 % (3056836)------------------------------
% 169.55/34.15 % (3056836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056836)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056836)Termination reason: Instruction limit
% 169.55/34.15 % (3056836)Termination phase: Saturation
% 169.55/34.15 % (3056836)Time elapsed: 1.067 s
% 169.55/34.15 % (3056836)Peak memory usage: 45 MB
% 169.55/34.15 % (3056836)Instructions burned: 3773 (million)
% 169.55/34.15 % (3056842)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3671901955:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi)
% 169.55/34.15 % (3056838)Instruction limit reached!
% 169.55/34.15 % (3056838)------------------------------
% 169.55/34.15 % (3056838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056838)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056838)Termination reason: Instruction limit
% 169.55/34.15 % (3056838)Termination phase: Saturation
% 169.55/34.15 % (3056838)Time elapsed: 0.918 s
% 169.55/34.15 % (3056838)Peak memory usage: 17 MB
% 169.55/34.15 % (3056838)Instructions burned: 2253 (million)
% 169.55/34.15 % (3056844)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=321251669:i=29340_2932 on theBenchmark for (2932ds/29340Mi)
% 169.55/34.15 % (3056842)Instruction limit reached!
% 169.55/34.15 % (3056842)------------------------------
% 169.55/34.15 % (3056842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056842)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056842)Termination reason: Instruction limit
% 169.55/34.15 % (3056842)Termination phase: Saturation
% 169.55/34.15 % (3056842)Time elapsed: 1.087 s
% 169.55/34.15 % (3056842)Peak memory usage: 59 MB
% 169.55/34.15 % (3056842)Instructions burned: 4592 (million)
% 169.55/34.15 % (3056846)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3104500390:i=5211_2926 on theBenchmark for (2926ds/5211Mi)
% 169.55/34.15 % TRYING [9]
% 169.55/34.15 % (3056846)Instruction limit reached!
% 169.55/34.15 % (3056846)------------------------------
% 169.55/34.15 % (3056846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056846)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056846)Termination reason: Instruction limit
% 169.55/34.15 % (3056846)Termination phase: Saturation
% 169.55/34.15 % (3056846)Time elapsed: 1.522 s
% 169.55/34.15 % (3056846)Peak memory usage: 60 MB
% 169.55/34.15 % (3056846)Instructions burned: 5213 (million)
% 169.55/34.15 % (3056848)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=530893675:i=5497:nm=2_2911 on theBenchmark for (2911ds/5497Mi)
% 169.55/34.15 % TRYING [17]
% 169.55/34.15 % (3056848)Instruction limit reached!
% 169.55/34.15 % (3056848)------------------------------
% 169.55/34.15 % (3056848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056848)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056848)Termination reason: Instruction limit
% 169.55/34.15 % (3056848)Termination phase: Finite model building constraint generation
% 169.55/34.15 % (3056848)Time elapsed: 1.002 s
% 169.55/34.15 % (3056848)Peak memory usage: 309 MB
% 169.55/34.15 % (3056848)Instructions burned: 5499 (million)
% 169.55/34.15 % (3056850)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3162034740:fmbsr=2:i=46332_2900 on theBenchmark for (2900ds/46332Mi)
% 169.55/34.15 % TRYING [15]
% 169.55/34.15 % TRYING [8]
% 169.55/34.15 % (3056850)Instruction limit reached!
% 169.55/34.15 % (3056850)------------------------------
% 169.55/34.15 % (3056850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056850)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056850)Termination reason: Instruction limit
% 169.55/34.15 % (3056850)Termination phase: Finite model building constraint generation
% 169.55/34.15 % (3056850)Time elapsed: 9.211 s
% 169.55/34.15 % (3056850)Peak memory usage: 3045 MB
% 169.55/34.15 % (3056850)Instructions burned: 46334 (million)
% 169.55/34.15 % TRYING [9]
% 169.55/34.15 % (3056852)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2197058429:i=14071_2805 on theBenchmark for (2805ds/14071Mi)
% 169.55/34.15 % TRYING [12]
% 169.55/34.15 % (3056844)Instruction limit reached!
% 169.55/34.15 % (3056844)------------------------------
% 169.55/34.15 % (3056844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056844)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056844)Termination reason: Instruction limit
% 169.55/34.15 % (3056844)Termination phase: Saturation
% 169.55/34.15 % (3056844)Time elapsed: 13.776 s
% 169.55/34.15 % (3056844)Peak memory usage: 344 MB
% 169.55/34.15 % (3056844)Instructions burned: 29342 (million)
% 169.55/34.15 % (3056854)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1990561480:i=22565:add=on:rawr=on_2793 on theBenchmark for (2793ds/22565Mi)
% 169.55/34.15 % (3056852)Instruction limit reached!
% 169.55/34.15 % (3056852)------------------------------
% 169.55/34.15 % (3056852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056852)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056852)Termination reason: Instruction limit
% 169.55/34.15 % (3056852)Termination phase: Finite model building constraint generation
% 169.55/34.15 % (3056852)Time elapsed: 2.763 s
% 169.55/34.15 % (3056852)Peak memory usage: 967 MB
% 169.55/34.15 % (3056852)Instructions burned: 14075 (million)
% 169.55/34.15 % (3056856)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=661752799:i=8173:av=off_2777 on theBenchmark for (2777ds/8173Mi)
% 169.55/34.15 % (3056856)Instruction limit reached!
% 169.55/34.15 % (3056856)------------------------------
% 169.55/34.15 % (3056856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056856)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056856)Termination reason: Instruction limit
% 169.55/34.15 % (3056856)Termination phase: Saturation
% 169.55/34.15 % (3056856)Time elapsed: 1.633 s
% 169.55/34.15 % (3056856)Peak memory usage: 51 MB
% 169.55/34.15 % (3056856)Instructions burned: 8180 (million)
% 169.55/34.15 % (3056858)dis+10_16:1_sil=16000:random_seed=1114157998:i=9155:fsr=off_2760 on theBenchmark for (2760ds/9155Mi)
% 169.55/34.15 % (3056858)Instruction limit reached!
% 169.55/34.15 % (3056858)------------------------------
% 169.55/34.15 % (3056858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056858)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056858)Termination reason: Instruction limit
% 169.55/34.15 % (3056858)Termination phase: Saturation
% 169.55/34.15 % (3056858)Time elapsed: 2.541 s
% 169.55/34.15 % (3056858)Peak memory usage: 92 MB
% 169.55/34.15 % (3056858)Instructions burned: 9156 (million)
% 169.55/34.15 % (3056860)ott-3_8_sil=64000:random_seed=1021039377:i=20139:bs=on_2735 on theBenchmark for (2735ds/20139Mi)
% 169.55/34.15 % (3056832)Instruction limit reached!
% 169.55/34.15 % (3056832)------------------------------
% 169.55/34.15 % (3056832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056832)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056832)Termination reason: Instruction limit
% 169.55/34.15 % (3056832)Termination phase: Finite model building SAT solving
% 169.55/34.15 % (3056832)Time elapsed: 24.326 s
% 169.55/34.15 % (3056832)Peak memory usage: 825 MB
% 169.55/34.15 % (3056832)Instructions burned: 54282 (million)
% 169.55/34.15 % (3056862)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1476446956:fmbsr=2:i=32576_2719 on theBenchmark for (2719ds/32576Mi)
% 169.55/34.15 % TRYING [9]
% 169.55/34.15 % TRYING [10]
% 169.55/34.15 % (3056840)Instruction limit reached!
% 169.55/34.15 % (3056840)------------------------------
% 169.55/34.15 % (3056840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056840)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056840)Termination reason: Instruction limit
% 169.55/34.15 % (3056840)Termination phase: Finite model building SAT solving
% 169.55/34.15 % (3056840)Time elapsed: 26.389 s
% 169.55/34.15 % (3056840)Peak memory usage: 468 MB
% 169.55/34.15 % (3056840)Instructions burned: 67536 (million)
% 169.55/34.15 % (3056864)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2900580103:i=11404_2674 on theBenchmark for (2674ds/11404Mi)
% 169.55/34.15 % (3056860)Instruction limit reached!
% 169.55/34.15 % (3056860)------------------------------
% 169.55/34.15 % (3056860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056860)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056860)Termination reason: Instruction limit
% 169.55/34.15 % (3056860)Termination phase: Saturation
% 169.55/34.15 % (3056860)Time elapsed: 6.255 s
% 169.55/34.15 % (3056860)Peak memory usage: 206 MB
% 169.55/34.15 % (3056860)Instructions burned: 20141 (million)
% 169.55/34.15 % (3056866)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2751281010:i=14134_2672 on theBenchmark for (2672ds/14134Mi)
% 169.55/34.15 % (3056854)Instruction limit reached!
% 169.55/34.15 % (3056854)------------------------------
% 169.55/34.15 % (3056854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.15 % (3056854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.15 % (3056854)CaDiCaL version: 2.1.3
% 169.55/34.15 % (3056854)Termination reason: Instruction limit
% 169.55/34.15 % (3056854)Termination phase: Saturation
% 169.55/34.15 % (3056854)Time elapsed: 12.166 s
% 169.55/34.15 % (3056854)Peak memory usage: 191 MB
% 169.55/34.15 % (3056854)Instructions burned: 22566 (million)
% 169.55/34.15 % (3056868)dis+33_16_sil=32000:sac=on:random_seed=922095987:i=15851:nm=0_2671 on theBenchmark for (2671ds/15851Mi)
% 169.55/34.15 % (3056866) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3056775-3056866"...
% 169.55/34.15 % (3056866)...printing done.
% 169.55/34.15 % (3056866)Refutation found. Thanks to Tanya!
% 169.55/34.15 % SZS status Theorem for theBenchmark
% 169.55/34.15 % SZS output start Proof for theBenchmark
% See solution above
% 169.55/34.16 % (3056866)------------------------------
% 169.55/34.16 % (3056866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/34.16 % (3056866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/34.16 % (3056866)CaDiCaL version: 2.1.3
% 169.55/34.16 % (3056866)Termination reason: Refutation
% 169.55/34.16 % (3056866)Time elapsed: 0.793 s
% 169.55/34.16 % (3056866)Peak memory usage: 52 MB
% 169.55/34.16 % (3056866)Instructions burned: 2769 (million)
% 169.55/34.16 % (3056775)Success in time 33.73 s
% 169.55/34.16 % Vampire exiting
%------------------------------------------------------------------------------