%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG063+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:21 PM UTC 2026
% Result : Theorem 25.96s 4.60s
% Output : Refutation 27.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 33
% Syntax : Number of formulae : 205 ( 40 unt; 22 def)
% Number of atoms : 609 ( 116 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 752 ( 348 ~; 345 |; 32 &)
% ( 22 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 25 ( 23 usr; 23 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 112 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(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(f61,axiom,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2262) ).
fof(f62,conjecture,
sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN) = sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f63,negated_conjecture,
sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN) != sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f69,plain,
sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN),
inference(flattening,[],[f63]) ).
fof(f76,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,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(f82,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(f83,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,[],[f82]) ).
fof(f139,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f140,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f141,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f143,plain,
! [X0] :
( smndt0(smndt0(X0)) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f144,plain,
! [X0] :
( sz0z00 = sdtpldt0(smndt0(X0),X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f145,plain,
! [X0] :
( sz0z00 = sdtpldt0(X0,smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f148,plain,
! [X0] :
( sdtpldt0(sz0z00,X0) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f149,plain,
! [X0] :
( sdtpldt0(X0,sz0z00) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f152,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f153,plain,
! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f212,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f216,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f218,plain,
aScalar0(xN),
inference(cnf_transformation,[],[f55]) ).
fof(f221,plain,
sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS),
inference(cnf_transformation,[],[f58]) ).
fof(f226,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN)),
inference(cnf_transformation,[],[f61]) ).
fof(f227,plain,
sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN),
inference(cnf_transformation,[],[f69]) ).
fof(f231,plain,
! [X2] :
( ~ aScalar0(X2)
| sP2 ),
inference(cnf_transformation,[],[f231_D]) ).
fof(f231_D,definition,
( ! [X2] : ~ aScalar0(X2)
<=> ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[general_splitting_component_introduction]) ).
fof(f232,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sP2 ),
inference(general_splitting,[],[f152,f231_D]) ).
fof(f236,definition,
( spl4_1
<=> sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) = sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f238,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN)
| spl4_1 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,plain,
~ spl4_1,
inference(avatar_split_clause,[],[f227,f236]) ).
fof(f256,definition,
( spl4_2
<=> aScalar0(xN) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f258,plain,
( aScalar0(xN)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
spl4_2,
inference(avatar_split_clause,[],[f218,f256]) ).
fof(f264,plain,
( aScalar0(smndt0(xN))
| ~ spl4_2 ),
inference(resolution,[],[f258,f141]) ).
fof(f266,plain,
( xN = smndt0(smndt0(xN))
| ~ spl4_2 ),
inference(resolution,[],[f258,f143]) ).
fof(f267,plain,
( sz0z00 = sdtpldt0(smndt0(xN),xN)
| ~ spl4_2 ),
inference(resolution,[],[f258,f144]) ).
fof(f318,plain,
( sP2
| ~ spl4_2 ),
inference(resolution,[],[f258,f231]) ).
fof(f329,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_2 ),
inference(backward_subsumption_resolution,[],[f232,f318]) ).
fof(f335,definition,
( spl4_4
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f336,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl4_4
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f329,f256,f335]) ).
fof(f369,plain,
( ! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X1,sdtpldt0(X0,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_4 ),
inference(superposition,[],[f153,f336]) ).
fof(f375,plain,
( ! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(X1,sdtpldt0(X2,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(X1,X2)) )
| ~ spl4_4 ),
inference(superposition,[],[f153,f336]) ).
fof(f385,plain,
( ! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(X1,sdtpldt0(X2,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0)
| ~ aScalar0(sdtpldt0(X1,X2)) )
| ~ spl4_4 ),
inference(duplicate_literal_removal,[],[f375]) ).
fof(f391,plain,
( ! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X1,sdtpldt0(X0,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2) )
| ~ spl4_4 ),
inference(duplicate_literal_removal,[],[f369]) ).
fof(f414,plain,
( ! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(X1,sdtpldt0(X2,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0) )
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f385,f139]) ).
fof(f517,definition,
( spl4_8
<=> ! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X1,sdtpldt0(X0,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2) ) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f518,plain,
( ! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X1,sdtpldt0(X0,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2) )
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f519,plain,
( spl4_8
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f391,f335,f517]) ).
fof(f523,plain,
( ! [X0,X1] :
( sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz0z00,X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_8 ),
inference(superposition,[],[f518,f145]) ).
fof(f578,plain,
( ! [X0,X1] :
( sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz0z00,X1)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_8 ),
inference(duplicate_literal_removal,[],[f523]) ).
fof(f610,plain,
( ! [X0,X1] :
( sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_8 ),
inference(forward_subsumption_resolution,[],[f578,f141]) ).
fof(f621,definition,
( spl4_9
<=> aScalar0(xR) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f623,plain,
( aScalar0(xR)
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f624,plain,
spl4_9,
inference(avatar_split_clause,[],[f212,f621]) ).
fof(f686,definition,
( spl4_10
<=> ! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(X1,sdtpldt0(X2,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f687,plain,
( ! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(X1,sdtpldt0(X2,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X0) )
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f688,plain,
( spl4_10
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f414,f335,f686]) ).
fof(f860,definition,
( spl4_12
<=> sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f862,plain,
( sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f863,plain,
spl4_12,
inference(avatar_split_clause,[],[f221,f860]) ).
fof(f867,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(smndt0(xS))
| ~ spl4_12 ),
inference(superposition,[],[f140,f862]) ).
fof(f896,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS))
| ~ spl4_12 ),
inference(duplicate_literal_removal,[],[f867]) ).
fof(f898,definition,
( spl4_13
<=> aScalar0(xS) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f900,plain,
( aScalar0(xS)
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f901,plain,
spl4_13,
inference(avatar_split_clause,[],[f216,f898]) ).
fof(f906,plain,
( aScalar0(smndt0(xS))
| ~ spl4_13 ),
inference(resolution,[],[f900,f141]) ).
fof(f978,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ spl4_12
| ~ spl4_13 ),
inference(backward_subsumption_resolution,[],[f896,f906]) ).
fof(f982,definition,
( spl4_14
<=> sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f984,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN))
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f985,plain,
spl4_14,
inference(avatar_split_clause,[],[f226,f982]) ).
fof(f999,plain,
( ! [X0] :
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),X0) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sdtpldt0(smndt0(xN),X0))
| ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ aScalar0(smndt0(xN))
| ~ aScalar0(X0) )
| ~ spl4_14 ),
inference(superposition,[],[f153,f984]) ).
fof(f1016,plain,
( ! [X0] :
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),X0) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sdtpldt0(smndt0(xN),X0))
| ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ aScalar0(X0) )
| ~ spl4_2
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f999,f264]) ).
fof(f1033,definition,
( spl4_15
<=> aScalar0(sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f1034,plain,
( aScalar0(sdtasdt0(xR,xR))
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1035,plain,
( ~ aScalar0(sdtasdt0(xR,xR))
| spl4_15 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1041,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xR)
| spl4_15 ),
inference(resolution,[],[f1035,f140]) ).
fof(f1042,plain,
( ~ aScalar0(xR)
| spl4_15 ),
inference(duplicate_literal_removal,[],[f1041]) ).
fof(f1043,plain,
( $false
| ~ spl4_9
| spl4_15 ),
inference(forward_subsumption_resolution,[],[f1042,f623]) ).
fof(f1044,plain,
( ~ spl4_9
| spl4_15 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
fof(f1438,plain,
( ! [X0,X1] :
( sdtpldt0(X1,sz0z00) = sdtpldt0(smndt0(X0),sdtpldt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0))
| ~ aScalar0(X0) )
| ~ spl4_10 ),
inference(superposition,[],[f687,f145]) ).
fof(f1522,plain,
( ! [X0,X1] :
( sdtpldt0(X1,sz0z00) = sdtpldt0(smndt0(X0),sdtpldt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(smndt0(X0)) )
| ~ spl4_10 ),
inference(duplicate_literal_removal,[],[f1438]) ).
fof(f1590,plain,
( ! [X0,X1] :
( sdtpldt0(X1,sz0z00) = sdtpldt0(smndt0(X0),sdtpldt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f1522,f141]) ).
fof(f1665,definition,
( spl4_21
<=> ! [X0,X1] :
( sdtpldt0(X1,sz0z00) = sdtpldt0(smndt0(X0),sdtpldt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f1666,plain,
( ! [X0,X1] :
( sdtpldt0(X1,sz0z00) = sdtpldt0(smndt0(X0),sdtpldt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1667,plain,
( spl4_21
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f1590,f686,f1665]) ).
fof(f1677,definition,
( spl4_24
<=> ! [X0,X1] :
( sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f1678,plain,
( ! [X0,X1] :
( sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) )
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f1677]) ).
fof(f1679,plain,
( spl4_24
| ~ spl4_8 ),
inference(avatar_split_clause,[],[f610,f517,f1677]) ).
fof(f1685,plain,
( ! [X0,X1] :
( sdtpldt0(sz0z00,X0) = sdtpldt0(smndt0(X1),sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_4
| ~ spl4_24 ),
inference(superposition,[],[f1678,f336]) ).
fof(f1733,plain,
( ! [X0,X1] :
( sdtpldt0(sz0z00,X0) = sdtpldt0(smndt0(X1),sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_4
| ~ spl4_24 ),
inference(duplicate_literal_removal,[],[f1685]) ).
fof(f2352,definition,
( spl4_28
<=> aScalar0(sdtasdt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f2354,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f2352]) ).
fof(f2355,plain,
( spl4_28
| ~ spl4_12
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f978,f898,f860,f2352]) ).
fof(f2727,definition,
( spl4_30
<=> aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f2728,plain,
( aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2729,plain,
( ~ aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| spl4_30 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2735,plain,
( ~ aScalar0(sdtasdt0(xR,xR))
| ~ aScalar0(sdtasdt0(xS,xS))
| spl4_30 ),
inference(resolution,[],[f2729,f139]) ).
fof(f2740,plain,
( ~ aScalar0(sdtasdt0(xS,xS))
| ~ spl4_15
| spl4_30 ),
inference(forward_subsumption_resolution,[],[f2735,f1034]) ).
fof(f2743,plain,
( $false
| ~ spl4_15
| ~ spl4_28
| spl4_30 ),
inference(forward_subsumption_resolution,[],[f2740,f2354]) ).
fof(f2744,plain,
( ~ spl4_15
| ~ spl4_28
| spl4_30 ),
inference(avatar_contradiction_clause,[],[f2743]) ).
fof(f2752,plain,
( ! [X0] :
( aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),X0))
| ~ aScalar0(X0) )
| ~ spl4_30 ),
inference(resolution,[],[f2728,f139]) ).
fof(f2763,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sz0z00)
| ~ spl4_30 ),
inference(resolution,[],[f2728,f149]) ).
fof(f3231,plain,
( sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00) = sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ aScalar0(smndt0(xN))
| ~ spl4_14
| ~ spl4_21 ),
inference(superposition,[],[f1666,f984]) ).
fof(f3329,plain,
( sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00) = sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ aScalar0(smndt0(xN))
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f3231,f2752]) ).
fof(f3369,plain,
( sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00) = sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f3329,f264]) ).
fof(f3375,plain,
( sdtpldt0(xN,sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00)
| ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30 ),
inference(forward_demodulation,[],[f3369,f266]) ).
fof(f4831,definition,
( spl4_64
<=> aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN))) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f4832,plain,
( aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f4831]) ).
fof(f4833,plain,
( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| spl4_64 ),
inference(avatar_component_clause,[],[f4831]) ).
fof(f4839,plain,
( ~ aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| ~ aScalar0(smndt0(xN))
| spl4_64 ),
inference(resolution,[],[f4833,f139]) ).
fof(f4852,plain,
( ~ aScalar0(smndt0(xN))
| ~ spl4_30
| spl4_64 ),
inference(forward_subsumption_resolution,[],[f4839,f2728]) ).
fof(f4859,plain,
( $false
| ~ spl4_2
| ~ spl4_30
| spl4_64 ),
inference(forward_subsumption_resolution,[],[f4852,f264]) ).
fof(f4860,plain,
( ~ spl4_2
| ~ spl4_30
| spl4_64 ),
inference(avatar_contradiction_clause,[],[f4859]) ).
fof(f4875,plain,
( ! [X0] :
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),X0) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sdtpldt0(smndt0(xN),X0))
| ~ aScalar0(X0) )
| ~ spl4_2
| ~ spl4_14
| ~ spl4_64 ),
inference(backward_subsumption_resolution,[],[f1016,f4832]) ).
fof(f4893,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(sz0z00,sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ spl4_64 ),
inference(resolution,[],[f4832,f148]) ).
fof(f5103,definition,
( spl4_67
<=> sz0z00 = sdtpldt0(smndt0(xN),xN) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f5105,plain,
( sz0z00 = sdtpldt0(smndt0(xN),xN)
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f5103]) ).
fof(f5106,plain,
( spl4_67
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f267,f256,f5103]) ).
fof(f7330,definition,
( spl4_92
<=> aScalar0(smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl4_92])],[avatar_definition]) ).
fof(f7332,plain,
( aScalar0(smndt0(xN))
| ~ spl4_92 ),
inference(avatar_component_clause,[],[f7330]) ).
fof(f7333,plain,
( spl4_92
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f264,f256,f7330]) ).
fof(f10428,definition,
( spl4_107
<=> ! [X0,X1] :
( sdtpldt0(sz0z00,X0) = sdtpldt0(smndt0(X1),sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_107])],[avatar_definition]) ).
fof(f10429,plain,
( ! [X0,X1] :
( sdtpldt0(sz0z00,X0) = sdtpldt0(smndt0(X1),sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl4_107 ),
inference(avatar_component_clause,[],[f10428]) ).
fof(f10430,plain,
( spl4_107
| ~ spl4_4
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f1733,f1677,f335,f10428]) ).
fof(f10526,plain,
( sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))) = sdtpldt0(sz0z00,sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ aScalar0(smndt0(xN))
| ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ spl4_14
| ~ spl4_107 ),
inference(superposition,[],[f10429,f984]) ).
fof(f10701,plain,
( sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))) = sdtpldt0(sz0z00,sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ aScalar0(smndt0(xN))
| ~ spl4_14
| ~ spl4_30
| ~ spl4_107 ),
inference(forward_subsumption_resolution,[],[f10526,f2752]) ).
fof(f10754,plain,
( sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))) = sdtpldt0(sz0z00,sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ spl4_14
| ~ spl4_30
| ~ spl4_92
| ~ spl4_107 ),
inference(forward_subsumption_resolution,[],[f10701,f7332]) ).
fof(f10766,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(smndt0(smndt0(xN)),sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ spl4_14
| ~ spl4_30
| ~ spl4_64
| ~ spl4_92
| ~ spl4_107 ),
inference(forward_demodulation,[],[f10754,f4893]) ).
fof(f10770,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(xN,sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ spl4_2
| ~ spl4_14
| ~ spl4_30
| ~ spl4_64
| ~ spl4_92
| ~ spl4_107 ),
inference(forward_demodulation,[],[f10766,f266]) ).
fof(f12302,definition,
( spl4_129
<=> ! [X0] :
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),X0) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sdtpldt0(smndt0(xN),X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_129])],[avatar_definition]) ).
fof(f12303,plain,
( ! [X0] :
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),X0) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sdtpldt0(smndt0(xN),X0))
| ~ aScalar0(X0) )
| ~ spl4_129 ),
inference(avatar_component_clause,[],[f12302]) ).
fof(f12304,plain,
( spl4_129
| ~ spl4_2
| ~ spl4_14
| ~ spl4_64 ),
inference(avatar_split_clause,[],[f4875,f4831,f982,f256,f12302]) ).
fof(f12314,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00)
| ~ aScalar0(xN)
| ~ aScalar0(xN)
| ~ spl4_129 ),
inference(superposition,[],[f12303,f144]) ).
fof(f12400,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00)
| ~ aScalar0(xN)
| ~ spl4_129 ),
inference(duplicate_literal_removal,[],[f12314]) ).
fof(f12461,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),sz0z00)
| ~ spl4_2
| ~ spl4_129 ),
inference(forward_subsumption_resolution,[],[f12400,f258]) ).
fof(f12524,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN) = sdtpldt0(xN,sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30
| ~ spl4_129 ),
inference(forward_demodulation,[],[f12461,f3375]) ).
fof(f12552,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN)
| ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30
| ~ spl4_64
| ~ spl4_92
| ~ spl4_107
| ~ spl4_129 ),
inference(forward_demodulation,[],[f12524,f10770]) ).
fof(f14169,definition,
( spl4_138
<=> sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN) ),
introduced(definition,[new_symbols(definition,[spl4_138])],[avatar_definition]) ).
fof(f14171,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)) = sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN)
| ~ spl4_138 ),
inference(avatar_component_clause,[],[f14169]) ).
fof(f14172,plain,
( spl4_138
| ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30
| ~ spl4_64
| ~ spl4_92
| ~ spl4_107
| ~ spl4_129 ),
inference(avatar_split_clause,[],[f12552,f12302,f10428,f7330,f4831,f2727,f1665,f982,f256,f14169]) ).
fof(f14177,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),xN)
| spl4_1
| ~ spl4_138 ),
inference(superposition,[],[f238,f14171]) ).
fof(f14255,definition,
( spl4_139
<=> sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),xN) ),
introduced(definition,[new_symbols(definition,[spl4_139])],[avatar_definition]) ).
fof(f14257,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),xN)
| spl4_139 ),
inference(avatar_component_clause,[],[f14255]) ).
fof(f14258,plain,
( ~ spl4_139
| spl4_1
| ~ spl4_138 ),
inference(avatar_split_clause,[],[f14177,f14169,f236,f14255]) ).
fof(f14270,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtpldt0(smndt0(xN),xN))
| ~ aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| ~ aScalar0(smndt0(xN))
| ~ aScalar0(xN)
| spl4_139 ),
inference(superposition,[],[f14257,f153]) ).
fof(f14274,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtpldt0(smndt0(xN),xN))
| ~ aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| ~ aScalar0(xN)
| spl4_139 ),
inference(forward_subsumption_resolution,[],[f14270,f141]) ).
fof(f14286,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtpldt0(smndt0(xN),xN))
| ~ aScalar0(xN)
| ~ spl4_30
| spl4_139 ),
inference(forward_subsumption_resolution,[],[f14274,f2728]) ).
fof(f14298,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtpldt0(smndt0(xN),xN))
| ~ spl4_2
| ~ spl4_30
| spl4_139 ),
inference(forward_subsumption_resolution,[],[f14286,f258]) ).
fof(f14306,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sz0z00)
| ~ spl4_2
| ~ spl4_30
| ~ spl4_67
| spl4_139 ),
inference(forward_demodulation,[],[f14298,f5105]) ).
fof(f14308,plain,
( $false
| ~ spl4_2
| ~ spl4_30
| ~ spl4_67
| spl4_139 ),
inference(forward_subsumption_resolution,[],[f14306,f2763]) ).
fof(f14309,plain,
( ~ spl4_2
| ~ spl4_30
| ~ spl4_67
| spl4_139 ),
inference(avatar_contradiction_clause,[],[f14308]) ).
cnf(s1,plain,
~ spl4_1,
inference(sat_conversion,[],[f239]) ).
cnf(s2,plain,
spl4_2,
inference(sat_conversion,[],[f259]) ).
cnf(s4,plain,
( ~ spl4_2
| spl4_4 ),
inference(sat_conversion,[],[f337]) ).
cnf(s8,plain,
( ~ spl4_4
| spl4_8 ),
inference(sat_conversion,[],[f519]) ).
cnf(s9,plain,
spl4_9,
inference(sat_conversion,[],[f624]) ).
cnf(s10,plain,
( ~ spl4_4
| spl4_10 ),
inference(sat_conversion,[],[f688]) ).
cnf(s12,plain,
spl4_12,
inference(sat_conversion,[],[f863]) ).
cnf(s13,plain,
spl4_13,
inference(sat_conversion,[],[f901]) ).
cnf(s14,plain,
spl4_14,
inference(sat_conversion,[],[f985]) ).
cnf(s16,plain,
( ~ spl4_9
| spl4_15 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s21,plain,
( ~ spl4_10
| spl4_21 ),
inference(sat_conversion,[],[f1667]) ).
cnf(s24,plain,
( ~ spl4_8
| spl4_24 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s28,plain,
( ~ spl4_12
| ~ spl4_13
| spl4_28 ),
inference(sat_conversion,[],[f2355]) ).
cnf(s31,plain,
( ~ spl4_15
| ~ spl4_28
| spl4_30 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s71,plain,
( ~ spl4_2
| ~ spl4_30
| spl4_64 ),
inference(sat_conversion,[],[f4860]) ).
cnf(s77,plain,
( ~ spl4_2
| spl4_67 ),
inference(sat_conversion,[],[f5106]) ).
cnf(s101,plain,
( ~ spl4_2
| spl4_92 ),
inference(sat_conversion,[],[f7333]) ).
cnf(s116,plain,
( ~ spl4_4
| ~ spl4_24
| spl4_107 ),
inference(sat_conversion,[],[f10430]) ).
cnf(s138,plain,
( ~ spl4_2
| ~ spl4_14
| ~ spl4_64
| spl4_129 ),
inference(sat_conversion,[],[f12304]) ).
cnf(s147,plain,
( ~ spl4_2
| ~ spl4_14
| ~ spl4_21
| ~ spl4_30
| ~ spl4_64
| ~ spl4_92
| ~ spl4_107
| ~ spl4_129
| spl4_138 ),
inference(sat_conversion,[],[f14172]) ).
cnf(s148,plain,
( spl4_1
| ~ spl4_138
| ~ spl4_139 ),
inference(sat_conversion,[],[f14258]) ).
cnf(s149,plain,
( ~ spl4_2
| ~ spl4_30
| ~ spl4_67
| spl4_139 ),
inference(sat_conversion,[],[f14309]) ).
cnf(s160,plain,
spl4_28,
inference(rat,[],[s28,s13,s12]) ).
cnf(s169,plain,
spl4_15,
inference(rat,[],[s16,s9]) ).
cnf(s173,plain,
spl4_30,
inference(rat,[],[s31,s160,s169]) ).
cnf(s176,plain,
spl4_92,
inference(rat,[],[s101,s2]) ).
cnf(s180,plain,
spl4_67,
inference(rat,[],[s77,s2]) ).
cnf(s181,plain,
spl4_64,
inference(rat,[],[s71,s173,s2]) ).
cnf(s190,plain,
spl4_4,
inference(rat,[],[s4,s2]) ).
cnf(s193,plain,
spl4_139,
inference(rat,[],[s149,s2,s173,s180]) ).
cnf(s194,plain,
spl4_129,
inference(rat,[],[s138,s2,s14,s181]) ).
cnf(s221,plain,
spl4_10,
inference(rat,[],[s10,s190]) ).
cnf(s222,plain,
spl4_8,
inference(rat,[],[s8,s190]) ).
cnf(s236,plain,
spl4_21,
inference(rat,[],[s21,s221]) ).
cnf(s243,plain,
spl4_24,
inference(rat,[],[s24,s222]) ).
cnf(s249,plain,
spl4_107,
inference(rat,[],[s116,s190,s243]) ).
cnf(s256,plain,
spl4_138,
inference(rat,[],[s147,s236,s194,s181,s176,s2,s173,s14,s249]) ).
cnf(s258,plain,
spl4_1,
inference(rat,[],[s148,s193,s256]) ).
cnf(s261,plain,
$false,
inference(rat,[],[s1,s258]) ).
fof(f14312,plain,
$false,
inference(avatar_sat_refutation,[],[s261]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG063+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.42 % Computer : n001.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Sun Sep 27 23:10:16 UTC 2026
% 0.18/0.42 % CPUTime :
% 0.18/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.47 Running first-order theorem proving
% 0.18/0.47 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.15/4.07 % (4076439)Detected formulas, will run a generic FOF schedule.
% 23.15/4.07 % (4076450)dis-21_1_sil=8000:lcm=predicate:random_seed=1788048681:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 23.15/4.07 % (4076450)Instruction limit reached!
% 23.15/4.07 % (4076450)------------------------------
% 23.15/4.07 % (4076450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.15/4.07 % (4076450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.15/4.07 % (4076450)CaDiCaL version: 2.1.3
% 23.15/4.07 % (4076450)Termination reason: Instruction limit
% 23.15/4.07 % (4076450)Termination phase: Saturation
% 23.15/4.07 % (4076450)Time elapsed: 0.062 s
% 23.15/4.07 % (4076450)Peak memory usage: 89 MB
% 23.15/4.07 % (4076450)Instructions burned: 130 (million)
% 23.15/4.07 % (4076448)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=601954173:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 23.15/4.07 % (4076445)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3989765451:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 23.15/4.07 % (4076444)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1290296399:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 23.15/4.07 % (4076446)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2475456129:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 23.15/4.07 % (4076447)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3378965043:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 23.15/4.07 % (4076449)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3656697530:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 23.15/4.07 % (4076447)Instruction limit reached!
% 23.15/4.07 % (4076447)------------------------------
% 23.15/4.07 % (4076447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.15/4.07 % (4076447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.15/4.07 % (4076447)CaDiCaL version: 2.1.3
% 23.15/4.07 % (4076447)Termination reason: Instruction limit
% 23.15/4.07 % (4076447)Termination phase: Saturation
% 23.15/4.07 % (4076447)Time elapsed: 0.095 s
% 23.15/4.07 % (4076447)Peak memory usage: 89 MB
% 23.15/4.07 % (4076447)Instructions burned: 109 (million)
% 23.15/4.07 % (4076448)Instruction limit reached!
% 23.15/4.07 % (4076448)------------------------------
% 23.15/4.07 % (4076448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.15/4.07 % (4076448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.15/4.07 % (4076448)CaDiCaL version: 2.1.3
% 23.15/4.07 % (4076448)Termination reason: Instruction limit
% 23.15/4.07 % (4076448)Termination phase: Saturation
% 23.15/4.07 % (4076448)Time elapsed: 0.112 s
% 23.15/4.07 % (4076448)Peak memory usage: 88 MB
% 23.15/4.07 % (4076448)Instructions burned: 119 (million)
% 23.15/4.07 % (4076449)Instruction limit reached!
% 23.15/4.07 % (4076449)------------------------------
% 23.15/4.07 % (4076449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.15/4.07 % (4076449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.15/4.07 % (4076449)CaDiCaL version: 2.1.3
% 23.15/4.07 % (4076449)Termination reason: Instruction limit
% 23.15/4.07 % (4076449)Termination phase: Saturation
% 23.15/4.07 % (4076449)Time elapsed: 0.146 s
% 23.15/4.07 % (4076449)Peak memory usage: 90 MB
% 23.15/4.07 % (4076449)Instructions burned: 140 (million)
% 23.15/4.07 % (4076452)lrs+10_1_sil=8000:sp=occurrence:random_seed=2801558706:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 23.15/4.07 % (4076452)Instruction limit reached!
% 23.15/4.07 % (4076452)------------------------------
% 23.15/4.07 % (4076452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.15/4.07 % (4076452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.15/4.07 % (4076452)CaDiCaL version: 2.1.3
% 23.15/4.07 % (4076452)Termination reason: Instruction limit
% 23.15/4.07 % (4076452)Termination phase: Saturation
% 23.15/4.07 % (4076452)Time elapsed: 0.145 s
% 23.15/4.07 % (4076452)Peak memory usage: 93 MB
% 23.15/4.07 % (4076452)Instructions burned: 285 (million)
% 25.96/4.59 % (4076460)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2479715466:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 25.96/4.59 % (4076459)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2977220081:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 25.96/4.59 % (4076461)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2333528117:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 25.96/4.59 % (4076459)Instruction limit reached!
% 25.96/4.59 % (4076459)------------------------------
% 25.96/4.59 % (4076459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.59 % (4076459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.59 % (4076459)CaDiCaL version: 2.1.3
% 25.96/4.59 % (4076459)Termination reason: Instruction limit
% 25.96/4.59 % (4076459)Termination phase: Saturation
% 25.96/4.59 % (4076459)Time elapsed: 0.134 s
% 25.96/4.59 % (4076459)Peak memory usage: 91 MB
% 25.96/4.59 % (4076459)Instructions burned: 157 (million)
% 25.96/4.59 % (4076465)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2308562928:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 25.96/4.59 % (4076461)Instruction limit reached!
% 25.96/4.59 % (4076461)------------------------------
% 25.96/4.59 % (4076461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.59 % (4076461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.59 % (4076461)CaDiCaL version: 2.1.3
% 25.96/4.59 % (4076461)Termination reason: Instruction limit
% 25.96/4.59 % (4076461)Termination phase: Saturation
% 25.96/4.59 % (4076461)Time elapsed: 0.203 s
% 25.96/4.59 % (4076461)Peak memory usage: 95 MB
% 25.96/4.59 % (4076461)Instructions burned: 248 (million)
% 25.96/4.59 % (4076465)Instruction limit reached!
% 25.96/4.59 % (4076465)------------------------------
% 25.96/4.59 % (4076465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.59 % (4076465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.59 % (4076465)CaDiCaL version: 2.1.3
% 25.96/4.59 % (4076465)Termination reason: Instruction limit
% 25.96/4.59 % (4076465)Termination phase: Saturation
% 25.96/4.60 % (4076465)Time elapsed: 0.146 s
% 25.96/4.60 % (4076465)Peak memory usage: 91 MB
% 25.96/4.60 % (4076465)Instructions burned: 295 (million)
% 25.96/4.60 % (4076460)Instruction limit reached!
% 25.96/4.60 % (4076460)------------------------------
% 25.96/4.60 % (4076460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076460)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076460)Termination reason: Instruction limit
% 25.96/4.60 % (4076460)Termination phase: Saturation
% 25.96/4.60 % (4076460)Time elapsed: 0.323 s
% 25.96/4.60 % (4076460)Peak memory usage: 93 MB
% 25.96/4.60 % (4076460)Instructions burned: 325 (million)
% 25.96/4.60 % (4076470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4162034903:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 25.96/4.60 % (4076471)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=761807434:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 25.96/4.60 % (4076472)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3171415540:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 25.96/4.60 % (4076472)Instruction limit reached!
% 25.96/4.60 % (4076472)------------------------------
% 25.96/4.60 % (4076472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076472)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076472)Termination reason: Instruction limit
% 25.96/4.60 % (4076472)Termination phase: Saturation
% 25.96/4.60 % (4076472)Time elapsed: 0.058 s
% 25.96/4.60 % (4076472)Peak memory usage: 89 MB
% 25.96/4.60 % (4076472)Instructions burned: 127 (million)
% 25.96/4.60 % (4076471)Instruction limit reached!
% 25.96/4.60 % (4076471)------------------------------
% 25.96/4.60 % (4076471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076471)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076471)Termination reason: Instruction limit
% 25.96/4.60 % (4076471)Termination phase: Saturation
% 25.96/4.60 % (4076471)Time elapsed: 0.115 s
% 25.96/4.60 % (4076471)Peak memory usage: 91 MB
% 25.96/4.60 % (4076471)Instructions burned: 113 (million)
% 25.96/4.60 % (4076473)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3055042836:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 25.96/4.60 % (4076473)Instruction limit reached!
% 25.96/4.60 % (4076473)------------------------------
% 25.96/4.60 % (4076473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076473)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076473)Termination reason: Instruction limit
% 25.96/4.60 % (4076473)Termination phase: Saturation
% 25.96/4.60 % (4076473)Time elapsed: 0.102 s
% 25.96/4.60 % (4076473)Peak memory usage: 89 MB
% 25.96/4.60 % (4076473)Instructions burned: 114 (million)
% 25.96/4.60 % (4076477)lrs+10_1_sil=8000:sp=occurrence:random_seed=106904147:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 25.96/4.60 % (4076478)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2100123304:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 25.96/4.60 % (4076480)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3909367186:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 25.96/4.60 % (4076478)Instruction limit reached!
% 25.96/4.60 % (4076478)------------------------------
% 25.96/4.60 % (4076478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076478)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076478)Termination reason: Instruction limit
% 25.96/4.60 % (4076478)Termination phase: Saturation
% 25.96/4.60 % (4076478)Time elapsed: 0.409 s
% 25.96/4.60 % (4076478)Peak memory usage: 94 MB
% 25.96/4.60 % (4076478)Instructions burned: 437 (million)
% 25.96/4.60 % (4076484)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3368033878:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 25.96/4.60 % (4076484)Instruction limit reached!
% 25.96/4.60 % (4076484)------------------------------
% 25.96/4.60 % (4076484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076484)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076484)Termination reason: Instruction limit
% 25.96/4.60 % (4076484)Termination phase: Saturation
% 25.96/4.60 % (4076484)Time elapsed: 0.078 s
% 25.96/4.60 % (4076484)Peak memory usage: 91 MB
% 25.96/4.60 % (4076484)Instructions burned: 134 (million)
% 25.96/4.60 % (4076477)Instruction limit reached!
% 25.96/4.60 % (4076477)------------------------------
% 25.96/4.60 % (4076477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076477)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076477)Termination reason: Instruction limit
% 25.96/4.60 % (4076477)Termination phase: Saturation
% 25.96/4.60 % (4076477)Time elapsed: 0.794 s
% 25.96/4.60 % (4076477)Peak memory usage: 101 MB
% 25.96/4.60 % (4076477)Instructions burned: 907 (million)
% 25.96/4.60 % (4076486)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3714184519:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 25.96/4.60 % (4076487)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1048893557:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 25.96/4.60 % (4076486)Instruction limit reached!
% 25.96/4.60 % (4076486)------------------------------
% 25.96/4.60 % (4076486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076486)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076486)Termination reason: Instruction limit
% 25.96/4.60 % (4076486)Termination phase: Saturation
% 25.96/4.60 % (4076486)Time elapsed: 0.499 s
% 25.96/4.60 % (4076486)Peak memory usage: 93 MB
% 25.96/4.60 % (4076486)Instructions burned: 593 (million)
% 25.96/4.60 % (4076490)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2370277431:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 25.96/4.60 % (4076446)First to succeed.
% 25.96/4.60 % (4076446)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4076439"
% 25.96/4.60 % (4076490)Instruction limit reached!
% 25.96/4.60 % (4076490)------------------------------
% 25.96/4.60 % (4076490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076490)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076490)Termination reason: Instruction limit
% 25.96/4.60 % (4076490)Termination phase: Saturation
% 25.96/4.60 % (4076490)Time elapsed: 0.113 s
% 25.96/4.60 % (4076490)Peak memory usage: 91 MB
% 25.96/4.60 % (4076490)Instructions burned: 125 (million)
% 25.96/4.60 % (4076470)Instruction limit reached!
% 25.96/4.60 % (4076470)------------------------------
% 25.96/4.60 % (4076470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.60 % (4076470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.60 % (4076470)CaDiCaL version: 2.1.3
% 25.96/4.60 % (4076470)Termination reason: Instruction limit
% 25.96/4.60 % (4076470)Termination phase: Saturation
% 25.96/4.60 % (4076470)Time elapsed: 2.451 s
% 25.96/4.60 % (4076470)Peak memory usage: 144 MB
% 25.96/4.60 % (4076470)Instructions burned: 2351 (million)
% 25.96/4.60 % (4076492)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3701737869:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 25.96/4.60 % (4076446)Refutation found. Thanks to Tanya!
% 25.96/4.60 % SZS status Theorem for theBenchmark
% 25.96/4.60 % SZS output start Proof for theBenchmark
% See solution above
% 27.24/4.84 % (4076446)------------------------------
% 27.24/4.84 % (4076446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.24/4.84 % (4076446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.24/4.84 % (4076446)CaDiCaL version: 2.1.3
% 27.24/4.84 % (4076446)Termination reason: Refutation
% 27.24/4.84 % (4076446)Time elapsed: 3.089 s
% 27.24/4.84 % (4076446)Peak memory usage: 151 MB
% 27.24/4.84 % (4076446)Instructions burned: 3190 (million)
% 27.24/4.84 % (4076446)------------------------------
% 27.24/4.84 % (4076446)------------------------------
% 27.24/4.84 % (4076439)Success in time 3.786 s
% 27.24/4.84 % Vampire exiting
%------------------------------------------------------------------------------