%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG049+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 : n012.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:52 PM UTC 2026
% Result : Theorem 7.42s 1.62s
% Output : Refutation 7.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 33
% Syntax : Number of formulae : 243 ( 33 unt; 17 def)
% Number of atoms : 851 ( 124 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1069 ( 461 ~; 526 |; 47 &)
% ( 17 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 18 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 182 ( 0 sgn 182 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(f17,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMNeg) ).
fof(f18,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMDNeg) ).
fof(f20,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERef) ).
fof(f21,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMon) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEMonM) ).
fof(f25,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETot) ).
fof(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(f34,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( aDimensionOf0(X0) = aDimensionOf0(X1)
=> aScalar0(sdtasasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScPr) ).
fof(f37,axiom,
aVector0(xs),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1542) ).
fof(f42,conjecture,
sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f43,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f46,plain,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(flattening,[],[f43]) ).
fof(f59,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f60,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f59]) ).
fof(f61,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f62,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(f63,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(f64,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,[],[f63]) ).
fof(f69,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(f70,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,[],[f69]) ).
fof(f71,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f72,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f71]) ).
fof(f75,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f76,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f77,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f76]) ).
fof(f80,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(f81,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,[],[f80]) ).
fof(f82,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(f83,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,[],[f82]) ).
fof(f84,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f85,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f84]) ).
fof(f89,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(f90,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f89]) ).
fof(f99,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f100,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f99]) ).
fof(f116,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f118,plain,
! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| aScalar0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f60]) ).
fof(f119,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f120,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = smndt0(sz0z00) ),
inference(cnf_transformation,[],[f62]) ).
fof(f121,plain,
! [X0] :
( ~ aScalar0(X0)
| smndt0(smndt0(X0)) = X0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f122,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtpldt0(smndt0(X0),X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f123,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtpldt0(X0,smndt0(X0)) ),
inference(cnf_transformation,[],[f62]) ).
fof(f124,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(sz0z00,X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f125,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(X0,sz0z00) ),
inference(cnf_transformation,[],[f62]) ).
fof(f126,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(sz0z00,X0) = X0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f127,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,sz0z00) = X0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f128,plain,
! [X2,X0,X1] :
( ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f135,plain,
! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| smndt0(sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1) ),
inference(cnf_transformation,[],[f70]) ).
fof(f136,plain,
! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f137,plain,
! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtasdt0(X0,X1) = sdtasdt0(smndt0(X0),smndt0(X1)) ),
inference(cnf_transformation,[],[f72]) ).
fof(f138,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtlseqdt0(X0,X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f139,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ),
inference(cnf_transformation,[],[f83]) ).
fof(f143,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f147,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f90]) ).
fof(f156,plain,
! [X0,X1] :
( ~ aVector0(X1)
| ~ aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| aScalar0(sdtasasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f100]) ).
fof(f159,plain,
aVector0(xs),
inference(cnf_transformation,[],[f37]) ).
fof(f175,plain,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(cnf_transformation,[],[f46]) ).
fof(f186,plain,
! [X0] :
( ~ sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f187,plain,
! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f189,plain,
! [X2,X3,X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtlseqdt0(X2,X3)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X3) ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f190,plain,
! [X2,X3,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtlseqdt0(X2,X3)
| sdtlseqdt0(sz0z00,X2)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X3) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f191,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X1) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f195,plain,
! [X0,X1] :
( sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f204,plain,
! [X0,X1] :
( aDimensionOf0(X0) != aDimensionOf0(X1)
| aVector0(X0)
| aVector0(X1)
| aScalar0(sdtasasdt0(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f207,plain,
~ aVector0(xs),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f218,plain,
sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f220,definition,
( spl2_1
<=> ! [X0,X1] :
( ~ aScalar0(X1)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f221,plain,
( ! [X0,X1] :
( ~ aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1) )
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,definition,
( spl2_2
<=> ! [X2] : ~ aScalar0(X2) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f224,plain,
( ! [X2] : ~ aScalar0(X2)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f128,f223,f220]) ).
fof(f231,definition,
( spl2_4
<=> sz0z00 = smndt0(sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f233,plain,
( sz0z00 = smndt0(sz0z00)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
( spl2_4
| spl2_2 ),
inference(avatar_split_clause,[],[f120,f223,f231]) ).
fof(f235,plain,
( $false
| ~ spl2_2 ),
inference(backward_subsumption_resolution,[],[f116,f224]) ).
fof(f236,plain,
~ spl2_2,
inference(avatar_contradiction_clause,[],[f235]) ).
fof(f258,plain,
sz0z00 = sdtasdt0(sz0z00,sz0z00),
inference(resolution,[],[f124,f116]) ).
fof(f259,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(sz0z00,smndt0(X0)) ),
inference(resolution,[],[f124,f119]) ).
fof(f298,plain,
( ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs)) ),
inference(resolution,[],[f191,f218]) ).
fof(f299,plain,
( ~ sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs)) ),
inference(forward_subsumption_resolution,[],[f298,f116]) ).
fof(f301,definition,
( spl2_8
<=> aScalar0(sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f302,plain,
( aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| spl2_8 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl2_9
<=> sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f307,plain,
( ~ sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00)
| spl2_9 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( ~ spl2_8
| ~ spl2_9 ),
inference(avatar_split_clause,[],[f299,f305,f301]) ).
fof(f310,plain,
( ! [X0,X1] :
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtasdt0(smndt0(X0),X1) = sdtasdt0(X1,smndt0(X0)) )
| ~ spl2_1 ),
inference(resolution,[],[f221,f119]) ).
fof(f327,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| smndt0(sdtasdt0(smndt0(X1),X0)) = sdtasdt0(smndt0(smndt0(X1)),X0)
| ~ aScalar0(X0) ),
inference(resolution,[],[f135,f119]) ).
fof(f340,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(sz0z00,X0)
| sz0z00 = X0 ),
inference(resolution,[],[f187,f116]) ).
fof(f355,plain,
! [X0] :
( aVector0(X0)
| aVector0(X0)
| aScalar0(sdtasasdt0(X0,X0)) ),
inference(equality_resolution,[],[f204]) ).
fof(f356,plain,
! [X0] :
( aScalar0(sdtasasdt0(X0,X0))
| aVector0(X0) ),
inference(duplicate_literal_removal,[],[f355]) ).
fof(f436,plain,
! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,sz0z00)
| sz0z00 = X0 ),
inference(superposition,[],[f195,f258]) ).
fof(f441,plain,
! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| ~ aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,sz0z00)
| sz0z00 = X0 ),
inference(forward_subsumption_resolution,[],[f436,f116]) ).
fof(f443,definition,
( spl2_17
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f444,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| spl2_17 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl2_18
<=> ! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| sz0z00 = X0
| sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f448,plain,
( ! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| sz0z00 = X0
| sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) )
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl2_17
| spl2_18 ),
inference(avatar_split_clause,[],[f441,f447,f443]) ).
fof(f459,plain,
( ~ aScalar0(sz0z00)
| ~ spl2_17 ),
inference(resolution,[],[f445,f186]) ).
fof(f465,plain,
( $false
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f459,f116]) ).
fof(f466,plain,
~ spl2_17,
inference(avatar_contradiction_clause,[],[f465]) ).
fof(f491,plain,
( aVector0(xs)
| spl2_8 ),
inference(resolution,[],[f356,f303]) ).
fof(f514,plain,
( $false
| spl2_8 ),
inference(forward_subsumption_resolution,[],[f491,f207]) ).
fof(f515,plain,
spl2_8,
inference(avatar_contradiction_clause,[],[f514]) ).
fof(f522,plain,
( ! [X0] :
( ~ aScalar0(X0)
| aScalar0(sdtasdt0(sdtasasdt0(xs,xs),X0)) )
| ~ spl2_8 ),
inference(resolution,[],[f302,f118]) ).
fof(f523,plain,
( sdtasasdt0(xs,xs) = smndt0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f302,f121]) ).
fof(f524,plain,
( sz0z00 = sdtpldt0(smndt0(sdtasasdt0(xs,xs)),sdtasasdt0(xs,xs))
| ~ spl2_8 ),
inference(resolution,[],[f302,f122]) ).
fof(f525,plain,
( sz0z00 = sdtpldt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f302,f123]) ).
fof(f527,plain,
( sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),sz0z00)
| ~ spl2_8 ),
inference(resolution,[],[f302,f125]) ).
fof(f528,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sz0z00,sdtasasdt0(xs,xs))
| ~ spl2_8 ),
inference(resolution,[],[f302,f126]) ).
fof(f529,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(xs,xs),sz0z00)
| ~ spl2_8 ),
inference(resolution,[],[f302,f127]) ).
fof(f536,plain,
( ! [X0] :
( ~ aScalar0(X0)
| smndt0(sdtasdt0(sdtasasdt0(xs,xs),X0)) = sdtasdt0(sdtasasdt0(xs,xs),smndt0(X0)) )
| ~ spl2_8 ),
inference(resolution,[],[f302,f136]) ).
fof(f537,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtasdt0(sdtasasdt0(xs,xs),X0) = sdtasdt0(smndt0(sdtasasdt0(xs,xs)),smndt0(X0)) )
| ~ spl2_8 ),
inference(resolution,[],[f302,f137]) ).
fof(f581,plain,
( sz0z00 = sdtasdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f259,f302]) ).
fof(f635,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sdtasasdt0(xs,xs),X0)
| ~ aScalar0(X1) )
| ~ spl2_8 ),
inference(superposition,[],[f190,f527]) ).
fof(f637,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sdtasasdt0(xs,xs),X0)
| ~ aScalar0(X1) )
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f635,f116]) ).
fof(f639,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sdtasasdt0(xs,xs),X0)
| ~ aScalar0(X1) )
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f637,f302]) ).
fof(f641,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sdtasasdt0(xs,xs),X0)
| ~ aScalar0(X1) )
| ~ spl2_8
| spl2_17 ),
inference(forward_subsumption_resolution,[],[f639,f444]) ).
fof(f762,plain,
( aScalar0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f522,f302]) ).
fof(f868,plain,
! [X0] :
( sdtlseqdt0(smndt0(X0),sz0z00)
| sdtlseqdt0(sz0z00,smndt0(X0))
| sz0z00 = smndt0(X0)
| ~ aScalar0(X0) ),
inference(resolution,[],[f340,f119]) ).
fof(f874,definition,
( spl2_24
<=> sz0z00 = sdtpldt0(sdtasasdt0(xs,xs),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f876,plain,
( sz0z00 = sdtpldt0(sdtasasdt0(xs,xs),sz0z00)
| ~ spl2_24 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f944,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| ~ aScalar0(X1)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| sdtlseqdt0(X1,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs))) )
| ~ spl2_8 ),
inference(superposition,[],[f190,f581]) ).
fof(f948,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtlseqdt0(X1,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs))) )
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f944,f116]) ).
fof(f950,definition,
( spl2_32
<=> sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs))) ),
introduced(definition,[new_symbols(definition,[spl2_32])],[avatar_definition]) ).
fof(f951,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| spl2_32 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f952,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_32 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f954,definition,
( spl2_33
<=> aScalar0(smndt0(sdtasasdt0(xs,xs))) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f955,plain,
( aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f956,plain,
( ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| spl2_33 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f962,definition,
( spl2_35
<=> ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X1,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_35])],[avatar_definition]) ).
fof(f963,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),sz0z00)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X1,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl2_35 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f964,plain,
( ~ spl2_33
| spl2_35
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f948,f301,f962,f954]) ).
fof(f976,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| spl2_33 ),
inference(resolution,[],[f956,f119]) ).
fof(f977,plain,
( $false
| ~ spl2_8
| spl2_33 ),
inference(forward_subsumption_resolution,[],[f976,f302]) ).
fof(f978,plain,
( ~ spl2_8
| spl2_33 ),
inference(avatar_contradiction_clause,[],[f977]) ).
fof(f1032,definition,
( spl2_36
<=> sz0z00 = smndt0(sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[spl2_36])],[avatar_definition]) ).
fof(f1033,plain,
( sz0z00 != smndt0(sdtasasdt0(xs,xs))
| spl2_36 ),
inference(avatar_component_clause,[],[f1032]) ).
fof(f1034,plain,
( sz0z00 = smndt0(sdtasasdt0(xs,xs))
| ~ spl2_36 ),
inference(avatar_component_clause,[],[f1032]) ).
fof(f1036,definition,
( spl2_37
<=> sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f1047,plain,
( ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_32 ),
inference(resolution,[],[f952,f191]) ).
fof(f1048,plain,
( ~ sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_32 ),
inference(forward_subsumption_resolution,[],[f1047,f116]) ).
fof(f1050,plain,
( ~ sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ spl2_32
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f1048,f955]) ).
fof(f1052,plain,
( ~ spl2_37
| ~ spl2_32
| ~ spl2_33 ),
inference(avatar_split_clause,[],[f1050,f954,f950,f1036]) ).
fof(f1157,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtasdt0(smndt0(sdtasasdt0(xs,xs)),X0) = sdtasdt0(X0,smndt0(sdtasasdt0(xs,xs))) )
| ~ spl2_1
| ~ spl2_8 ),
inference(resolution,[],[f310,f302]) ).
fof(f1230,plain,
( ! [X0] :
( smndt0(sdtasdt0(smndt0(sdtasasdt0(xs,xs)),X0)) = sdtasdt0(smndt0(smndt0(sdtasasdt0(xs,xs))),X0)
| ~ aScalar0(X0) )
| ~ spl2_8 ),
inference(resolution,[],[f327,f302]) ).
fof(f1527,definition,
( spl2_50
<=> sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[spl2_50])],[avatar_definition]) ).
fof(f1528,plain,
( sz0z00 != sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| spl2_50 ),
inference(avatar_component_clause,[],[f1527]) ).
fof(f2049,plain,
( sz0z00 = sdtasasdt0(xs,xs)
| ~ spl2_8
| ~ spl2_24 ),
inference(forward_demodulation,[],[f529,f876]) ).
fof(f2050,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl2_8
| ~ spl2_24 ),
inference(superposition,[],[f218,f2049]) ).
fof(f2090,plain,
( $false
| ~ spl2_8
| spl2_17
| ~ spl2_24 ),
inference(forward_subsumption_resolution,[],[f2050,f444]) ).
fof(f2091,plain,
( ~ spl2_8
| spl2_17
| ~ spl2_24 ),
inference(avatar_contradiction_clause,[],[f2090]) ).
fof(f2141,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sdtasasdt0(xs,xs),X1)
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),X0)
| ~ aScalar0(X1) )
| ~ spl2_8 ),
inference(superposition,[],[f189,f524]) ).
fof(f2143,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sdtasasdt0(xs,xs),X1)
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),X0)
| ~ aScalar0(X1) )
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f2141,f302]) ).
fof(f2145,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| sdtlseqdt0(sdtasasdt0(xs,xs),X1)
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),X0)
| ~ aScalar0(X1) )
| ~ spl2_8
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f2143,f955]) ).
fof(f2254,plain,
( sz0z00 = sdtpldt0(sdtasasdt0(xs,xs),sz0z00)
| ~ spl2_8
| ~ spl2_36 ),
inference(superposition,[],[f525,f1034]) ).
fof(f2269,plain,
( spl2_24
| ~ spl2_8
| ~ spl2_36 ),
inference(avatar_split_clause,[],[f2254,f1032,f301,f874]) ).
fof(f2512,plain,
( sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))) = smndt0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f536,f302]) ).
fof(f2539,plain,
( sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) = sdtasdt0(smndt0(sdtasasdt0(xs,xs)),smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f537,f302]) ).
fof(f2617,plain,
( sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))) = sdtasdt0(smndt0(sdtasasdt0(xs,xs)),sdtasasdt0(xs,xs))
| ~ spl2_1
| ~ spl2_8 ),
inference(resolution,[],[f1157,f302]) ).
fof(f2741,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtasdt0(sdtasasdt0(xs,xs),X0) = smndt0(sdtasdt0(smndt0(sdtasasdt0(xs,xs)),X0)) )
| ~ spl2_8 ),
inference(forward_demodulation,[],[f1230,f523]) ).
fof(f2756,plain,
( sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) = smndt0(sdtasdt0(smndt0(sdtasasdt0(xs,xs)),sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(resolution,[],[f2741,f302]) ).
fof(f6524,definition,
( spl2_190
<=> sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))) ),
introduced(definition,[new_symbols(definition,[spl2_190])],[avatar_definition]) ).
fof(f6526,plain,
( sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_190 ),
inference(avatar_component_clause,[],[f6524]) ).
fof(f6528,definition,
( spl2_191
<=> sdtlseqdt0(sz0z00,sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs)))) ),
introduced(definition,[new_symbols(definition,[spl2_191])],[avatar_definition]) ).
fof(f6530,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))))
| ~ spl2_191 ),
inference(avatar_component_clause,[],[f6528]) ).
fof(f6532,definition,
( spl2_192
<=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_192])],[avatar_definition]) ).
fof(f6534,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))),sz0z00)
| ~ spl2_192 ),
inference(avatar_component_clause,[],[f6532]) ).
fof(f43719,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))),sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))))
| sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(superposition,[],[f868,f2512]) ).
fof(f43721,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))),sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))))
| sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f43719,f762]) ).
fof(f43722,plain,
( spl2_190
| spl2_191
| spl2_192
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f43721,f301,f6532,f6528,f6524]) ).
fof(f43939,plain,
( sz0z00 != sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| sz0z00 = smndt0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| ~ spl2_18 ),
inference(superposition,[],[f448,f2539]) ).
fof(f43960,plain,
( sz0z00 != sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| ~ spl2_18
| spl2_36 ),
inference(forward_subsumption_resolution,[],[f43939,f1033]) ).
fof(f43967,plain,
( sz0z00 != sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| ~ spl2_18
| spl2_32
| spl2_36 ),
inference(forward_subsumption_resolution,[],[f43960,f951]) ).
fof(f43970,plain,
( sz0z00 != sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ spl2_8
| ~ spl2_18
| spl2_32
| ~ spl2_33
| spl2_36 ),
inference(forward_subsumption_resolution,[],[f43967,f955]) ).
fof(f43972,plain,
( ~ spl2_50
| ~ spl2_8
| ~ spl2_18
| spl2_32
| ~ spl2_33
| spl2_36 ),
inference(avatar_split_clause,[],[f43970,f1032,f954,f950,f447,f301,f1527]) ).
fof(f45848,plain,
( sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) = smndt0(sdtasdt0(sdtasasdt0(xs,xs),smndt0(sdtasasdt0(xs,xs))))
| ~ spl2_1
| ~ spl2_8 ),
inference(forward_demodulation,[],[f2756,f2617]) ).
fof(f46537,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| spl2_17
| ~ spl2_191 ),
inference(resolution,[],[f6530,f641]) ).
fof(f46543,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| spl2_17
| ~ spl2_191 ),
inference(forward_subsumption_resolution,[],[f46537,f302]) ).
fof(f46546,plain,
( sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_191 ),
inference(forward_subsumption_resolution,[],[f46543,f951]) ).
fof(f46549,plain,
( sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_33
| ~ spl2_191 ),
inference(forward_subsumption_resolution,[],[f46546,f955]) ).
fof(f46551,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_33
| ~ spl2_191 ),
inference(resolution,[],[f46549,f186]) ).
fof(f46557,plain,
( $false
| ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_33
| ~ spl2_191 ),
inference(forward_subsumption_resolution,[],[f46551,f302]) ).
fof(f46558,plain,
( ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_33
| ~ spl2_191 ),
inference(avatar_contradiction_clause,[],[f46557]) ).
fof(f62517,plain,
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))
| ~ aScalar0(sz0z00)
| sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8
| ~ spl2_33 ),
inference(superposition,[],[f2145,f528]) ).
fof(f65799,plain,
( sdtlseqdt0(sdtasasdt0(xs,xs),sz0z00)
| sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_35
| ~ spl2_192 ),
inference(resolution,[],[f963,f6534]) ).
fof(f65826,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| spl2_9
| ~ spl2_35
| ~ spl2_192 ),
inference(forward_subsumption_resolution,[],[f65799,f307]) ).
fof(f66009,plain,
( smndt0(sz0z00) = sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ spl2_1
| ~ spl2_8
| ~ spl2_190 ),
inference(superposition,[],[f45848,f6526]) ).
fof(f66028,plain,
( sz0z00 = sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| ~ spl2_1
| ~ spl2_4
| ~ spl2_8
| ~ spl2_190 ),
inference(forward_demodulation,[],[f66009,f233]) ).
fof(f66031,plain,
( $false
| ~ spl2_1
| ~ spl2_4
| ~ spl2_8
| spl2_50
| ~ spl2_190 ),
inference(forward_subsumption_resolution,[],[f66028,f1528]) ).
fof(f66032,plain,
( ~ spl2_1
| ~ spl2_4
| ~ spl2_8
| spl2_50
| ~ spl2_190 ),
inference(avatar_contradiction_clause,[],[f66031]) ).
fof(f66048,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| spl2_9
| ~ spl2_35
| ~ spl2_192 ),
inference(forward_subsumption_resolution,[],[f65826,f186]) ).
fof(f66053,plain,
( ~ aScalar0(sz0z00)
| sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f62517,f218]) ).
fof(f66097,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ aScalar0(smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| spl2_9
| ~ spl2_35
| ~ spl2_192 ),
inference(forward_subsumption_resolution,[],[f66048,f302]) ).
fof(f66102,plain,
( sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))
| sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f66053,f116]) ).
fof(f66125,plain,
( sdtlseqdt0(sz0z00,smndt0(sdtasasdt0(xs,xs)))
| ~ spl2_8
| spl2_9
| ~ spl2_33
| ~ spl2_35
| ~ spl2_192 ),
inference(forward_subsumption_resolution,[],[f66097,f955]) ).
fof(f66130,plain,
( sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl2_8
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f66102,f186]) ).
fof(f66146,plain,
( spl2_32
| ~ spl2_8
| spl2_9
| ~ spl2_33
| ~ spl2_35
| ~ spl2_192 ),
inference(avatar_split_clause,[],[f66125,f6532,f962,f954,f305,f301,f950]) ).
fof(f66149,plain,
( sdtlseqdt0(smndt0(sdtasasdt0(xs,xs)),sz0z00)
| ~ spl2_8
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f66130,f302]) ).
fof(f66158,plain,
( spl2_37
| ~ spl2_8
| ~ spl2_33 ),
inference(avatar_split_clause,[],[f66149,f954,f301,f1036]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f225]) ).
cnf(s3,plain,
( spl2_2
| spl2_4 ),
inference(sat_conversion,[],[f234]) ).
cnf(s4,plain,
~ spl2_2,
inference(sat_conversion,[],[f236]) ).
cnf(s7,plain,
( ~ spl2_8
| ~ spl2_9 ),
inference(sat_conversion,[],[f308]) ).
cnf(s20,plain,
( spl2_17
| spl2_18 ),
inference(sat_conversion,[],[f450]) ).
cnf(s21,plain,
~ spl2_17,
inference(sat_conversion,[],[f466]) ).
cnf(s22,plain,
spl2_8,
inference(sat_conversion,[],[f515]) ).
cnf(s32,plain,
( ~ spl2_8
| ~ spl2_33
| spl2_35 ),
inference(sat_conversion,[],[f964]) ).
cnf(s33,plain,
( ~ spl2_8
| spl2_33 ),
inference(sat_conversion,[],[f978]) ).
cnf(s35,plain,
( ~ spl2_32
| ~ spl2_33
| ~ spl2_37 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s61,plain,
( ~ spl2_8
| spl2_17
| ~ spl2_24 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s67,plain,
( ~ spl2_8
| spl2_24
| ~ spl2_36 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s457,plain,
( ~ spl2_8
| spl2_190
| spl2_191
| spl2_192 ),
inference(sat_conversion,[],[f43722]) ).
cnf(s461,plain,
( ~ spl2_8
| ~ spl2_18
| spl2_32
| ~ spl2_33
| spl2_36
| ~ spl2_50 ),
inference(sat_conversion,[],[f43972]) ).
cnf(s511,plain,
( ~ spl2_8
| spl2_17
| spl2_32
| ~ spl2_33
| ~ spl2_191 ),
inference(sat_conversion,[],[f46558]) ).
cnf(s867,plain,
( ~ spl2_1
| ~ spl2_4
| ~ spl2_8
| spl2_50
| ~ spl2_190 ),
inference(sat_conversion,[],[f66032]) ).
cnf(s906,plain,
( ~ spl2_8
| spl2_9
| spl2_32
| ~ spl2_33
| ~ spl2_35
| ~ spl2_192 ),
inference(sat_conversion,[],[f66146]) ).
cnf(s918,plain,
( ~ spl2_8
| ~ spl2_33
| spl2_37 ),
inference(sat_conversion,[],[f66158]) ).
cnf(s928,plain,
spl2_33,
inference(rat,[],[s33,s22]) ).
cnf(s930,plain,
spl2_37,
inference(rat,[],[s918,s22,s928]) ).
cnf(s932,plain,
~ spl2_32,
inference(rat,[],[s35,s930,s928]) ).
cnf(s933,plain,
spl2_35,
inference(rat,[],[s32,s22,s928]) ).
cnf(s944,plain,
~ spl2_191,
inference(rat,[],[s511,s932,s928,s22,s21]) ).
cnf(s945,plain,
~ spl2_24,
inference(rat,[],[s61,s22,s21]) ).
cnf(s948,plain,
~ spl2_36,
inference(rat,[],[s67,s22,s945]) ).
cnf(s951,plain,
spl2_18,
inference(rat,[],[s20,s21]) ).
cnf(s952,plain,
~ spl2_50,
inference(rat,[],[s461,s948,s932,s928,s22,s951]) ).
cnf(s956,plain,
~ spl2_9,
inference(rat,[],[s7,s22]) ).
cnf(s957,plain,
~ spl2_192,
inference(rat,[],[s906,s932,s933,s928,s22,s956]) ).
cnf(s959,plain,
spl2_190,
inference(rat,[],[s457,s944,s22,s957]) ).
cnf(s966,plain,
spl2_4,
inference(rat,[],[s3,s4]) ).
cnf(s967,plain,
~ spl2_1,
inference(rat,[],[s867,s959,s952,s22,s966]) ).
cnf(s969,plain,
$false,
inference(rat,[],[s1,s4,s967]) ).
fof(f66160,plain,
$false,
inference(avatar_sat_refutation,[],[s969]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : RNG049+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 23:02:34 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.33 Running first-order model finding
% 0.08/0.33 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
% 7.42/1.62 % (2861483)Will run a generic schedule for satisfiability detection.
% 7.42/1.62 % (2861489)% WARNING: option uhcvi not known.
% 7.42/1.62 % (2861493)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3558191585:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.42/1.62 % (2861491)dis+10_1_sil=32000:sp=arity:random_seed=4156218975:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.42/1.62 % (2861492)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1525302543:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.42/1.62 % (2861488)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2917508131_2999 on theBenchmark for (2999ds/0Mi)
% 7.42/1.62 % (2861490)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2169096076:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.42/1.62 % (2861489)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1392053059:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.42/1.62 % TRYING [1]
% 7.42/1.62 % TRYING [2]
% 7.42/1.62 % TRYING [3]
% 7.42/1.62 % (2861494)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1309536138:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.42/1.62 % TRYING [4]
% 7.42/1.62 % (2861491)Instruction limit reached!
% 7.42/1.62 % (2861491)------------------------------
% 7.42/1.62 % (2861491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861491)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861491)Termination reason: Instruction limit
% 7.42/1.62 % (2861491)Termination phase: Saturation
% 7.42/1.62 % (2861491)Time elapsed: 0.035 s
% 7.42/1.62 % (2861491)Peak memory usage: 12 MB
% 7.42/1.62 % (2861491)Instructions burned: 104 (million)
% 7.42/1.62 % (2861492)Instruction limit reached!
% 7.42/1.62 % (2861492)------------------------------
% 7.42/1.62 % (2861492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861492)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861492)Termination reason: Instruction limit
% 7.42/1.62 % (2861492)Termination phase: Saturation
% 7.42/1.62 % (2861492)Time elapsed: 0.037 s
% 7.42/1.62 % (2861492)Peak memory usage: 13 MB
% 7.42/1.62 % (2861492)Instructions burned: 117 (million)
% 7.42/1.62 % TRYING [5]
% 7.42/1.62 % (2861493)Instruction limit reached!
% 7.42/1.62 % (2861493)------------------------------
% 7.42/1.62 % (2861493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861493)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861493)Termination reason: Instruction limit
% 7.42/1.62 % (2861493)Termination phase: Saturation
% 7.42/1.62 % (2861493)Time elapsed: 0.042 s
% 7.42/1.62 % (2861493)Peak memory usage: 13 MB
% 7.42/1.62 % (2861493)Instructions burned: 134 (million)
% 7.42/1.62 % (2861502)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3274049997:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.42/1.62 % (2861503)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2907208726:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.42/1.62 % TRYING [1]
% 7.42/1.62 % TRYING [2]
% 7.42/1.62 % TRYING [3]
% 7.42/1.62 % (2861504)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=2707691210:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.42/1.62 % TRYING [4]
% 7.42/1.62 % (2861494)Instruction limit reached!
% 7.42/1.62 % (2861494)------------------------------
% 7.42/1.62 % (2861494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861494)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861494)Termination reason: Instruction limit
% 7.42/1.62 % (2861494)Termination phase: Saturation
% 7.42/1.62 % (2861494)Time elapsed: 0.055 s
% 7.42/1.62 % (2861494)Peak memory usage: 12 MB
% 7.42/1.62 % (2861494)Instructions burned: 163 (million)
% 7.42/1.62 % (2861508)ott-21_1_sil=16000:fs=off:random_seed=3831116523:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.42/1.62 % (2861503)Instruction limit reached!
% 7.42/1.62 % (2861503)------------------------------
% 7.42/1.62 % (2861503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861503)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861503)Termination reason: Instruction limit
% 7.42/1.62 % (2861503)Termination phase: Saturation
% 7.42/1.62 % (2861503)Time elapsed: 0.035 s
% 7.42/1.62 % (2861503)Peak memory usage: 12 MB
% 7.42/1.62 % (2861503)Instructions burned: 135 (million)
% 7.42/1.62 % TRYING [5]
% 7.42/1.62 % (2861509)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1019519760:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.42/1.62 % TRYING [6]
% 7.42/1.62 % (2861508)Instruction limit reached!
% 7.42/1.62 % (2861508)------------------------------
% 7.42/1.62 % (2861508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861508)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861508)Termination reason: Instruction limit
% 7.42/1.62 % (2861508)Termination phase: Saturation
% 7.42/1.62 % (2861508)Time elapsed: 0.066 s
% 7.42/1.62 % (2861508)Peak memory usage: 13 MB
% 7.42/1.62 % (2861508)Instructions burned: 180 (million)
% 7.42/1.62 % (2861512)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2152697432:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.42/1.62 % TRYING [1]
% 7.42/1.62 % TRYING [2]
% 7.42/1.62 % TRYING [6]
% 7.42/1.62 % TRYING [3]
% 7.42/1.62 % (2861502)Instruction limit reached!
% 7.42/1.62 % (2861502)------------------------------
% 7.42/1.62 % (2861502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861502)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861502)Termination reason: Instruction limit
% 7.42/1.62 % (2861502)Termination phase: Finite model building constraint generation
% 7.42/1.62 % (2861502)Time elapsed: 0.153 s
% 7.42/1.62 % (2861502)Peak memory usage: 35 MB
% 7.42/1.62 % (2861502)Instructions burned: 717 (million)
% 7.42/1.62 % (2861522)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1459286319:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.42/1.62 % TRYING [4]
% 7.42/1.62 % (2861504)Instruction limit reached!
% 7.42/1.62 % (2861504)------------------------------
% 7.42/1.62 % (2861504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861504)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861504)Termination reason: Instruction limit
% 7.42/1.62 % (2861504)Termination phase: Saturation
% 7.42/1.62 % (2861504)Time elapsed: 0.235 s
% 7.42/1.62 % (2861504)Peak memory usage: 18 MB
% 7.42/1.62 % (2861504)Instructions burned: 685 (million)
% 7.42/1.62 % (2861509)Instruction limit reached!
% 7.42/1.62 % (2861509)------------------------------
% 7.42/1.62 % (2861509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861509)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861509)Termination reason: Instruction limit
% 7.42/1.62 % (2861509)Termination phase: Saturation
% 7.42/1.62 % (2861509)Time elapsed: 0.199 s
% 7.42/1.62 % (2861509)Peak memory usage: 14 MB
% 7.42/1.62 % (2861509)Instructions burned: 478 (million)
% 7.42/1.62 % (2861531)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=661511904:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 7.42/1.62 % (2861532)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=1716061697:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 7.42/1.62 % TRYING [5]
% 7.42/1.62 % (2861512)Instruction limit reached!
% 7.42/1.62 % (2861512)------------------------------
% 7.42/1.62 % (2861512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861512)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861512)Termination reason: Instruction limit
% 7.42/1.62 % (2861512)Termination phase: Finite model building constraint generation
% 7.42/1.62 % (2861512)Time elapsed: 0.263 s
% 7.42/1.62 % (2861512)Peak memory usage: 21 MB
% 7.42/1.62 % (2861512)Instructions burned: 868 (million)
% 7.42/1.62 % (2861536)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=522461073:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 7.42/1.62 % TRYING [7]
% 7.42/1.62 % (2861532)Instruction limit reached!
% 7.42/1.62 % (2861532)------------------------------
% 7.42/1.62 % (2861532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861532)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861532)Termination reason: Instruction limit
% 7.42/1.62 % (2861532)Termination phase: Saturation
% 7.42/1.62 % (2861532)Time elapsed: 0.304 s
% 7.42/1.62 % (2861532)Peak memory usage: 20 MB
% 7.42/1.62 % (2861532)Instructions burned: 692 (million)
% 7.42/1.62 % (2861540)fmb+10_1_sil=64000:random_seed=4088560943:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 7.42/1.62 % TRYING [1]
% 7.42/1.62 % TRYING [2]
% 7.42/1.62 % TRYING [3]
% 7.42/1.62 % (2861531)Instruction limit reached!
% 7.42/1.62 % (2861531)------------------------------
% 7.42/1.62 % (2861531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861531)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861531)Termination reason: Instruction limit
% 7.42/1.62 % (2861531)Termination phase: Finite model building constraint generation
% 7.42/1.62 % (2861531)Time elapsed: 0.349 s
% 7.42/1.62 % (2861531)Peak memory usage: 108 MB
% 7.42/1.62 % (2861531)Instructions burned: 894 (million)
% 7.42/1.62 % TRYING [4]
% 7.42/1.62 % (2861542)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1620679569:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 7.42/1.62 % TRYING [20]
% 7.42/1.62 % (2861522)Instruction limit reached!
% 7.42/1.62 % (2861522)------------------------------
% 7.42/1.62 % (2861522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861522)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861522)Termination reason: Instruction limit
% 7.42/1.62 % (2861522)Termination phase: Saturation
% 7.42/1.62 % (2861522)Time elapsed: 0.479 s
% 7.42/1.62 % (2861522)Peak memory usage: 27 MB
% 7.42/1.62 % (2861522)Instructions burned: 1180 (million)
% 7.42/1.62 % (2861544)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4198886798:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 7.42/1.62 % TRYING [8]
% 7.42/1.62 % TRYING [5]
% 7.42/1.62 % (2861536)Instruction limit reached!
% 7.42/1.62 % (2861536)------------------------------
% 7.42/1.62 % (2861536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861536)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861536)Termination reason: Instruction limit
% 7.42/1.62 % (2861536)Termination phase: Saturation
% 7.42/1.62 % (2861536)Time elapsed: 0.366 s
% 7.42/1.62 % (2861536)Peak memory usage: 20 MB
% 7.42/1.62 % (2861536)Instructions burned: 879 (million)
% 7.42/1.62 % (2861547)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4213018048:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 7.42/1.62 % (2861544)Instruction limit reached!
% 7.42/1.62 % (2861544)------------------------------
% 7.42/1.62 % (2861544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861544)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861544)Termination reason: Instruction limit
% 7.42/1.62 % (2861544)Termination phase: Finite model building constraint generation
% 7.42/1.62 % (2861544)Time elapsed: 0.168 s
% 7.42/1.62 % (2861544)Peak memory usage: 63 MB
% 7.42/1.62 % (2861544)Instructions burned: 924 (million)
% 7.42/1.62 % (2861585)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3156063712:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 7.42/1.62 % TRYING [8]
% 7.42/1.62 % TRYING [6]
% 7.42/1.62 % (2861489) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2861483-2861489"...
% 7.42/1.62 % (2861489)...printing done.
% 7.42/1.62 % (2861489)Refutation found. Thanks to Tanya!
% 7.42/1.62 % SZS status Theorem for theBenchmark
% 7.42/1.62 % SZS output start Proof for theBenchmark
% See solution above
% 7.42/1.62 % (2861489)------------------------------
% 7.42/1.62 % (2861489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.62 % (2861489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.62 % (2861489)CaDiCaL version: 2.1.3
% 7.42/1.62 % (2861489)Termination reason: Refutation
% 7.42/1.62 % (2861489)Time elapsed: 1.234 s
% 7.42/1.62 % (2861489)Peak memory usage: 43 MB
% 7.42/1.62 % (2861489)Instructions burned: 3766 (million)
% 7.42/1.62 % (2861483)Success in time 1.288 s
% 7.42/1.62 % Vampire exiting
%------------------------------------------------------------------------------