%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR208+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 09:44:05 AM UTC 2026
% Result : Theorem 106.98s 16.09s
% Output : Refutation 108.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 23
% Syntax : Number of formulae : 108 ( 32 unt; 2 def)
% Number of atoms : 258 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 297 ( 147 ~; 111 |; 30 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 3 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-1 aty)
% Number of variables : 108 ( 0 sgn 94 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f116,axiom,
p__d__subclass(c__SelfConnectedObject,c__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA182) ).
fof(f171,axiom,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA251) ).
fof(f2059,axiom,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2902) ).
fof(f2092,axiom,
p__d__subclass(c__Vertebrate,c__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2942) ).
fof(f2105,axiom,
p__d__subclass(c__WarmBloodedVertebrate,c__Vertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2955) ).
fof(f2108,axiom,
p__d__subclass(c__Bird,c__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2958) ).
fof(f2170,axiom,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3024) ).
fof(f2178,axiom,
p__d__subclass(c__AnimalAnatomicalStructure,c__AnatomicalStructure),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3034) ).
fof(f2184,axiom,
p__d__subclass(c__Egg,c__AnimalAnatomicalStructure),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3040) ).
fof(f2675,axiom,
p__d__subclass(c__SexAttribute,c__BiologicalAttribute),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3674) ).
fof(f2680,axiom,
! [X0] :
( p__d__instance(X0,c__Animal)
=> ? [X1] :
( p__d__instance(X1,c__SexAttribute)
& p__attribute(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3680) ).
fof(f5614,axiom,
p__d__subclass(c__BirdEgg,c__Egg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA3664) ).
fof(f5615,axiom,
! [X0] :
( p__d__instance(X0,c__BirdEgg)
=> ? [X1,X2] :
( p__d__instance(X1,c__SexualReproduction)
& p__agent(X1,X2)
& p__d__instance(X2,c__Bird)
& p__result(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA3665) ).
fof(f6883,axiom,
! [X0,X1] :
( p__agent(X0,X1)
=> ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA30) ).
fof(f6921,axiom,
! [X0,X1] :
( p__attribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA68) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__SexualReproduction)
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__BiologicalAttribute)
& p__attribute(X1,X2) )
& p__agent(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',agentRelation0128) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__SexualReproduction)
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__BiologicalAttribute)
& p__attribute(X1,X2) )
& p__agent(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7508,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__SexualReproduction)
| ! [X2] :
( ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2) )
| ~ p__agent(X0,X1) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7509,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7510,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7509]) ).
fof(f7511,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) )
| ~ p__attribute(X0,X1) ),
inference(ennf_transformation,[],[f6921]) ).
fof(f7521,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) )
| ~ p__agent(X0,X1) ),
inference(ennf_transformation,[],[f6883]) ).
fof(f7542,plain,
! [X0] :
( ? [X1,X2] :
( p__d__instance(X1,c__SexualReproduction)
& p__agent(X1,X2)
& p__d__instance(X2,c__Bird)
& p__result(X1,X0) )
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(ennf_transformation,[],[f5615]) ).
fof(f7551,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7552,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7551]) ).
fof(f7713,plain,
! [X0] :
( ? [X1] :
( p__d__instance(X1,c__SexAttribute)
& p__attribute(X0,X1) )
| ~ p__d__instance(X0,c__Animal) ),
inference(ennf_transformation,[],[f2680]) ).
fof(f7918,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8303,plain,
! [X0] :
( ( p__d__instance(sK8(X0),c__SexualReproduction)
& p__agent(sK8(X0),sK9(X0))
& p__d__instance(sK9(X0),c__Bird)
& p__result(sK8(X0),X0) )
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0))],[f7542]) ).
fof(f8375,plain,
! [X0] :
( ( p__d__instance(sK81(X0),c__SexAttribute)
& p__attribute(X0,sK81(X0)) )
| ~ p__d__instance(X0,c__Animal) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81]),skolemize(X1,sK81(X0))],[f7713]) ).
fof(f8468,plain,
! [X0] :
( p__d__instance(sK159(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK159]),skolemize(X1,sK159(X0))],[f7918]) ).
fof(f8655,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__SexualReproduction)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__agent(X0,X1) ),
inference(cnf_transformation,[],[f7508]) ).
fof(f8656,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7510]) ).
fof(f8658,plain,
! [X0,X1] :
( ~ p__attribute(X0,X1)
| p__d__instance(X1,c__Attribute) ),
inference(cnf_transformation,[],[f7511]) ).
fof(f8673,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[],[f7521]) ).
fof(f8674,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| p__d__instance(X1,c__Agent) ),
inference(cnf_transformation,[],[f7521]) ).
fof(f8709,plain,
! [X0] :
( p__d__instance(sK9(X0),c__Bird)
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(cnf_transformation,[],[f8303]) ).
fof(f8710,plain,
! [X0] :
( p__agent(sK8(X0),sK9(X0))
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(cnf_transformation,[],[f8303]) ).
fof(f8711,plain,
! [X0] :
( p__d__instance(sK8(X0),c__SexualReproduction)
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(cnf_transformation,[],[f8303]) ).
fof(f8727,plain,
p__d__subclass(c__SexAttribute,c__BiologicalAttribute),
inference(cnf_transformation,[],[f2675]) ).
fof(f8732,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7552]) ).
fof(f8736,plain,
p__d__subclass(c__SelfConnectedObject,c__Object),
inference(cnf_transformation,[],[f116]) ).
fof(f8737,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f9006,plain,
p__d__subclass(c__Bird,c__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f2108]) ).
fof(f9007,plain,
p__d__subclass(c__BirdEgg,c__Egg),
inference(cnf_transformation,[],[f5614]) ).
fof(f9123,plain,
! [X0] :
( p__attribute(X0,sK81(X0))
| ~ p__d__instance(X0,c__Animal) ),
inference(cnf_transformation,[],[f8375]) ).
fof(f9124,plain,
! [X0] :
( p__d__instance(sK81(X0),c__SexAttribute)
| ~ p__d__instance(X0,c__Animal) ),
inference(cnf_transformation,[],[f8375]) ).
fof(f9147,plain,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
inference(cnf_transformation,[],[f2170]) ).
fof(f9149,plain,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
inference(cnf_transformation,[],[f2059]) ).
fof(f9154,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
inference(cnf_transformation,[],[f171]) ).
fof(f9538,plain,
p__d__subclass(c__Vertebrate,c__Animal),
inference(cnf_transformation,[],[f2092]) ).
fof(f9728,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f9731,plain,
! [X0] :
( p__d__instance(sK159(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f8468]) ).
fof(f10231,plain,
p__d__subclass(c__AnimalAnatomicalStructure,c__AnatomicalStructure),
inference(cnf_transformation,[],[f2178]) ).
fof(f10266,plain,
p__d__subclass(c__WarmBloodedVertebrate,c__Vertebrate),
inference(cnf_transformation,[],[f2105]) ).
fof(f10428,plain,
p__d__subclass(c__Egg,c__AnimalAnatomicalStructure),
inference(cnf_transformation,[],[f2184]) ).
fof(f10720,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__SexualReproduction)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__agent(X0,X1) ),
inference(forward_subsumption_resolution,[],[f8655,f8673]) ).
fof(f10721,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,c__SexualReproduction)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__agent(X0,X1) ),
inference(forward_subsumption_resolution,[],[f10720,f8674]) ).
fof(f10722,plain,
! [X2,X0,X1] :
( ~ p__agent(X0,X1)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__d__instance(X0,c__SexualReproduction) ),
inference(forward_subsumption_resolution,[],[f10721,f8658]) ).
fof(f10727,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__BiologicalAttribute)
| ~ p__attribute(sK9(X1),X0)
| ~ p__d__instance(sK8(X1),c__SexualReproduction)
| ~ p__d__instance(X1,c__BirdEgg) ),
inference(resolution,[],[f10722,f8710]) ).
fof(f10752,plain,
! [X0,X1] :
( ~ p__attribute(sK9(X1),X0)
| ~ p__d__instance(X0,c__BiologicalAttribute)
| ~ p__d__instance(X1,c__BirdEgg) ),
inference(forward_subsumption_resolution,[],[f10727,f8711]) ).
fof(f10943,plain,
! [X0] :
( ~ p__d__instance(sK81(sK9(X0)),c__BiologicalAttribute)
| ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__instance(sK9(X0),c__Animal) ),
inference(resolution,[],[f10752,f9123]) ).
fof(f14641,plain,
! [X0,X1] :
( ~ p__d__instance(sK81(sK9(X0)),X1)
| ~ p__d__instance(sK9(X0),c__Animal)
| ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(X1,c__BiologicalAttribute) ),
inference(resolution,[],[f10943,f8656]) ).
fof(f14642,plain,
! [X0] :
( ~ p__d__instance(sK9(X0),c__Animal)
| ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(c__SexAttribute,c__BiologicalAttribute)
| ~ p__d__instance(sK9(X0),c__Animal) ),
inference(resolution,[],[f14641,f9124]) ).
fof(f14655,plain,
! [X0] :
( ~ p__d__instance(sK9(X0),c__Animal)
| ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(c__SexAttribute,c__BiologicalAttribute) ),
inference(duplicate_literal_removal,[],[f14642]) ).
fof(f14656,plain,
! [X0] :
( ~ p__d__instance(sK9(X0),c__Animal)
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(forward_subsumption_resolution,[],[f14655,f8727]) ).
fof(f14658,plain,
! [X0,X1] :
( ~ p__d__instance(sK9(X0),X1)
| ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(X1,c__Animal) ),
inference(resolution,[],[f14656,f8656]) ).
fof(f14659,plain,
! [X0] :
( ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(c__Bird,c__Animal)
| ~ p__d__instance(X0,c__BirdEgg) ),
inference(resolution,[],[f14658,f8709]) ).
fof(f14672,plain,
! [X0] :
( ~ p__d__instance(X0,c__BirdEgg)
| ~ p__d__subclass(c__Bird,c__Animal) ),
inference(duplicate_literal_removal,[],[f14659]) ).
fof(f14718,definition,
( spl316_722
<=> ! [X0] : ~ p__d__instance(X0,c__BirdEgg) ),
introduced(definition,[new_symbols(definition,[spl316_722])],[avatar_definition]) ).
fof(f14719,plain,
( ! [X0] : ~ p__d__instance(X0,c__BirdEgg)
| ~ spl316_722 ),
inference(avatar_component_clause,[],[f14718]) ).
fof(f14735,definition,
( spl316_726
<=> p__d__subclass(c__Bird,c__Animal) ),
introduced(definition,[new_symbols(definition,[spl316_726])],[avatar_definition]) ).
fof(f14737,plain,
( ~ p__d__subclass(c__Bird,c__Animal)
| spl316_726 ),
inference(avatar_component_clause,[],[f14735]) ).
fof(f14738,plain,
( ~ spl316_726
| spl316_722 ),
inference(avatar_split_clause,[],[f14672,f14718,f14735]) ).
fof(f14739,plain,
( ! [X0] :
( ~ p__d__subclass(c__Bird,X0)
| ~ p__d__subclass(X0,c__Animal) )
| spl316_726 ),
inference(resolution,[],[f14737,f8732]) ).
fof(f14742,plain,
( ~ p__d__subclass(c__WarmBloodedVertebrate,c__Animal)
| spl316_726 ),
inference(resolution,[],[f14739,f9006]) ).
fof(f14747,plain,
( ! [X0] :
( ~ p__d__subclass(c__WarmBloodedVertebrate,X0)
| ~ p__d__subclass(X0,c__Animal) )
| spl316_726 ),
inference(resolution,[],[f14742,f8732]) ).
fof(f14750,plain,
( ~ p__d__subclass(c__Vertebrate,c__Animal)
| spl316_726 ),
inference(resolution,[],[f14747,f10266]) ).
fof(f14751,plain,
( $false
| spl316_726 ),
inference(forward_subsumption_resolution,[],[f14750,f9538]) ).
fof(f14752,plain,
spl316_726,
inference(avatar_contradiction_clause,[],[f14751]) ).
fof(f14762,plain,
( ~ p__d__subclass(c__BirdEgg,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14719,f9731]) ).
fof(f14774,plain,
( ! [X0] :
( ~ p__d__subclass(c__BirdEgg,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14762,f8732]) ).
fof(f14777,plain,
( ~ p__d__subclass(c__Egg,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14774,f9007]) ).
fof(f14778,plain,
( ! [X0] :
( ~ p__d__subclass(c__Egg,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14777,f8732]) ).
fof(f14782,plain,
( ~ p__d__subclass(c__AnimalAnatomicalStructure,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14778,f10428]) ).
fof(f14784,plain,
( ! [X0] :
( ~ p__d__subclass(c__AnimalAnatomicalStructure,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14782,f8732]) ).
fof(f14791,plain,
( ~ p__d__subclass(c__AnatomicalStructure,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14784,f10231]) ).
fof(f14792,plain,
( ! [X0] :
( ~ p__d__subclass(c__AnatomicalStructure,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14791,f8732]) ).
fof(f14795,plain,
( ~ p__d__subclass(c__OrganicObject,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14792,f9147]) ).
fof(f14796,plain,
( ! [X0] :
( ~ p__d__subclass(c__OrganicObject,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14795,f8732]) ).
fof(f14799,plain,
( ~ p__d__subclass(c__CorpuscularObject,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14796,f9149]) ).
fof(f14800,plain,
( ! [X0] :
( ~ p__d__subclass(c__CorpuscularObject,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14799,f8732]) ).
fof(f14803,plain,
( ~ p__d__subclass(c__SelfConnectedObject,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14800,f9154]) ).
fof(f14804,plain,
( ! [X0] :
( ~ p__d__subclass(c__SelfConnectedObject,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14803,f8732]) ).
fof(f14807,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14804,f8736]) ).
fof(f14808,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| ~ spl316_722 ),
inference(resolution,[],[f14807,f8732]) ).
fof(f14811,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| ~ spl316_722 ),
inference(resolution,[],[f14808,f8737]) ).
fof(f14812,plain,
( $false
| ~ spl316_722 ),
inference(forward_subsumption_resolution,[],[f14811,f9728]) ).
fof(f14813,plain,
~ spl316_722,
inference(avatar_contradiction_clause,[],[f14812]) ).
cnf(s531,plain,
( spl316_722
| ~ spl316_726 ),
inference(sat_conversion,[],[f14738]) ).
cnf(s532,plain,
spl316_726,
inference(sat_conversion,[],[f14752]) ).
cnf(s534,plain,
~ spl316_722,
inference(sat_conversion,[],[f14813]) ).
cnf(s535,plain,
$false,
inference(rat,[],[s531,s532,s534]) ).
fof(f14814,plain,
$false,
inference(avatar_sat_refutation,[],[s535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR208+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 23:47:17 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 10.75/2.37 % (1293165)Detected formulas, will run a generic FOF schedule.
% 10.75/2.37 % (1293170)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=4051171898:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.75/2.37 % (1293174)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1922265896:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.75/2.37 % (1293171)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=3636138731:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.75/2.37 % (1293173)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=315175413:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.75/2.37 % (1293172)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=4061045207:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.75/2.37 % (1293175)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1410202387:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.75/2.37 % (1293176)dis-21_1_sil=8000:lcm=predicate:random_seed=420356761:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.75/2.37 % (1293173)Refutation not found, incomplete strategy
% 10.75/2.37 % (1293173)------------------------------
% 10.75/2.37 % (1293173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.37 % (1293173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.37 % (1293173)CaDiCaL version: 2.1.3
% 10.75/2.37 % (1293173)Termination reason: Refutation not found, incomplete strategy
% 10.75/2.37 % (1293173)Time elapsed: 0.017 s
% 10.75/2.37 % (1293173)Peak memory usage: 93 MB
% 10.75/2.37 % (1293173)Instructions burned: 24 (million)
% 10.75/2.37 % (1293174)Instruction limit reached!
% 10.75/2.37 % (1293174)------------------------------
% 10.75/2.37 % (1293174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.37 % (1293174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.37 % (1293174)CaDiCaL version: 2.1.3
% 10.75/2.37 % (1293174)Termination reason: Instruction limit
% 10.75/2.37 % (1293174)Termination phase: Saturation
% 10.75/2.37 % (1293174)Time elapsed: 0.068 s
% 10.75/2.37 % (1293174)Peak memory usage: 93 MB
% 10.75/2.37 % (1293174)Instructions burned: 119 (million)
% 10.75/2.37 % (1293176)Instruction limit reached!
% 10.75/2.37 % (1293176)------------------------------
% 10.75/2.37 % (1293176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.37 % (1293176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.37 % (1293176)CaDiCaL version: 2.1.3
% 10.75/2.37 % (1293176)Termination reason: Instruction limit
% 10.75/2.37 % (1293176)Termination phase: Saturation
% 10.75/2.37 % (1293176)Time elapsed: 0.074 s
% 10.75/2.37 % (1293176)Peak memory usage: 95 MB
% 10.75/2.37 % (1293176)Instructions burned: 130 (million)
% 10.75/2.37 % (1293175)Instruction limit reached!
% 10.75/2.37 % (1293175)------------------------------
% 10.75/2.37 % (1293175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.37 % (1293175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.37 % (1293175)CaDiCaL version: 2.1.3
% 10.75/2.37 % (1293175)Termination reason: Instruction limit
% 10.75/2.37 % (1293175)Termination phase: Preprocessing 3
% 10.75/2.37 % (1293175)Time elapsed: 0.087 s
% 10.75/2.37 % (1293175)Peak memory usage: 94 MB
% 10.75/2.37 % (1293175)Instructions burned: 140 (million)
% 10.75/2.37 % (1293184)lrs+10_1_sil=8000:sp=occurrence:random_seed=2120673696:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.75/2.37 % (1293186)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4251422367:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 10.75/2.37 % (1293185)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4111534292:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 10.75/2.37 % (1293173)------------------------------
% 10.75/2.37 % (1293173)------------------------------
% 10.75/2.37 % (1293186)Refutation not found, incomplete strategy
% 10.75/2.37 % (1293186)------------------------------
% 10.75/2.37 % (1293186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293186)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293186)Termination reason: Refutation not found, incomplete strategy
% 16.86/3.15 % (1293186)Time elapsed: 0.016 s
% 16.86/3.15 % (1293186)Peak memory usage: 94 MB
% 16.86/3.15 % (1293186)Instructions burned: 20 (million)
% 16.86/3.15 % (1293185)Refutation not found, incomplete strategy
% 16.86/3.15 % (1293185)------------------------------
% 16.86/3.15 % (1293185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293185)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293185)Termination reason: Refutation not found, incomplete strategy
% 16.86/3.15 % (1293185)Time elapsed: 0.032 s
% 16.86/3.15 % (1293185)Peak memory usage: 94 MB
% 16.86/3.15 % (1293185)Instructions burned: 61 (million)
% 16.86/3.15 % (1293184)Instruction limit reached!
% 16.86/3.15 % (1293184)------------------------------
% 16.86/3.15 % (1293184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293184)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293184)Termination reason: Instruction limit
% 16.86/3.15 % (1293184)Termination phase: Saturation
% 16.86/3.15 % (1293184)Time elapsed: 0.166 s
% 16.86/3.15 % (1293184)Peak memory usage: 98 MB
% 16.86/3.15 % (1293184)Instructions burned: 285 (million)
% 16.86/3.15 % (1293190)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=1710168669:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 16.86/3.15 % (1293186)------------------------------
% 16.86/3.15 % (1293186)------------------------------
% 16.86/3.15 % (1293185)------------------------------
% 16.86/3.15 % (1293185)------------------------------
% 16.86/3.15 % (1293191)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1701075396:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 16.86/3.15 % (1293190)Instruction limit reached!
% 16.86/3.15 % (1293190)------------------------------
% 16.86/3.15 % (1293190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293190)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293190)Termination reason: Instruction limit
% 16.86/3.15 % (1293190)Termination phase: Saturation
% 16.86/3.15 % (1293190)Time elapsed: 0.139 s
% 16.86/3.15 % (1293190)Peak memory usage: 98 MB
% 16.86/3.15 % (1293190)Instructions burned: 250 (million)
% 16.86/3.15 % (1293191)Instruction limit reached!
% 16.86/3.15 % (1293191)------------------------------
% 16.86/3.15 % (1293191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293191)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293191)Termination reason: Instruction limit
% 16.86/3.15 % (1293191)Termination phase: Saturation
% 16.86/3.15 % (1293191)Time elapsed: 0.086 s
% 16.86/3.15 % (1293191)Peak memory usage: 95 MB
% 16.86/3.15 % (1293191)Instructions burned: 295 (million)
% 16.86/3.15 % (1293172)Refutation not found, incomplete strategy
% 16.86/3.15 % (1293172)------------------------------
% 16.86/3.15 % (1293172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.15 % (1293172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.15 % (1293172)CaDiCaL version: 2.1.3
% 16.86/3.15 % (1293172)Termination reason: Refutation not found, incomplete strategy
% 16.86/3.15 % (1293172)Time elapsed: 0.637 s
% 16.86/3.15 % (1293172)Peak memory usage: 136 MB
% 16.86/3.15 % (1293172)Instructions burned: 957 (million)
% 16.86/3.15 % (1293195)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1124992974:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 16.86/3.15 % (1293193)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1043469816:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 16.86/3.15 % (1293196)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=576147047:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 16.86/3.15 % (1293197)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2665650822:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 29.12/4.94 % (1293195)Instruction limit reached!
% 29.12/4.94 % (1293195)------------------------------
% 29.12/4.94 % (1293195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293195)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293195)Termination reason: Instruction limit
% 29.12/4.94 % (1293195)Termination phase: Saturation
% 29.12/4.94 % (1293195)Time elapsed: 0.060 s
% 29.12/4.94 % (1293195)Peak memory usage: 94 MB
% 29.12/4.94 % (1293195)Instructions burned: 114 (million)
% 29.12/4.94 % (1293197)Instruction limit reached!
% 29.12/4.94 % (1293197)------------------------------
% 29.12/4.94 % (1293197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293197)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293197)Termination reason: Instruction limit
% 29.12/4.94 % (1293197)Termination phase: Property scanning
% 29.12/4.94 % (1293197)Time elapsed: 0.035 s
% 29.12/4.94 % (1293197)Peak memory usage: 92 MB
% 29.12/4.94 % (1293197)Instructions burned: 119 (million)
% 29.12/4.94 % (1293196)Instruction limit reached!
% 29.12/4.94 % (1293196)------------------------------
% 29.12/4.94 % (1293196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293196)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293196)Termination reason: Instruction limit
% 29.12/4.94 % (1293196)Termination phase: Property scanning
% 29.12/4.94 % (1293196)Time elapsed: 0.079 s
% 29.12/4.94 % (1293196)Peak memory usage: 96 MB
% 29.12/4.94 % (1293196)Instructions burned: 129 (million)
% 29.12/4.94 % (1293172)------------------------------
% 29.12/4.94 % (1293172)------------------------------
% 29.12/4.94 % (1293203)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1363345610:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 29.12/4.94 % (1293202)lrs+10_1_sil=8000:sp=occurrence:random_seed=4170388213:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 29.12/4.94 % (1293203)Refutation not found, incomplete strategy
% 29.12/4.94 % (1293203)------------------------------
% 29.12/4.94 % (1293203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293203)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293203)Termination reason: Refutation not found, incomplete strategy
% 29.12/4.94 % (1293203)Time elapsed: 0.009 s
% 29.12/4.94 % (1293203)Peak memory usage: 94 MB
% 29.12/4.94 % (1293203)Instructions burned: 19 (million)
% 29.12/4.94 % (1293204)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=358732902:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 29.12/4.94 % (1293203)------------------------------
% 29.12/4.94 % (1293203)------------------------------
% 29.12/4.94 % (1293207)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3076858112:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 29.12/4.94 % (1293207)Refutation not found, incomplete strategy
% 29.12/4.94 % (1293207)------------------------------
% 29.12/4.94 % (1293207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293207)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293207)Termination reason: Refutation not found, incomplete strategy
% 29.12/4.94 % (1293207)Time elapsed: 0.020 s
% 29.12/4.94 % (1293207)Peak memory usage: 94 MB
% 29.12/4.94 % (1293207)Instructions burned: 27 (million)
% 29.12/4.94 % (1293210)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2196904284:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 29.12/4.94 % (1293207)------------------------------
% 29.12/4.94 % (1293207)------------------------------
% 29.12/4.94 % (1293210)Instruction limit reached!
% 29.12/4.94 % (1293210)------------------------------
% 29.12/4.94 % (1293210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/4.94 % (1293210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/4.94 % (1293210)CaDiCaL version: 2.1.3
% 29.12/4.94 % (1293210)Termination reason: Instruction limit
% 29.12/4.94 % (1293210)Termination phase: Saturation
% 45.24/7.15 % (1293210)Time elapsed: 0.171 s
% 45.24/7.15 % (1293210)Peak memory usage: 101 MB
% 45.24/7.15 % (1293210)Instructions burned: 593 (million)
% 45.24/7.15 % (1293202)Instruction limit reached!
% 45.24/7.15 % (1293202)------------------------------
% 45.24/7.15 % (1293202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.15 % (1293202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.15 % (1293202)CaDiCaL version: 2.1.3
% 45.24/7.15 % (1293202)Termination reason: Instruction limit
% 45.24/7.15 % (1293202)Termination phase: Saturation
% 45.24/7.15 % (1293202)Time elapsed: 0.501 s
% 45.24/7.15 % (1293202)Peak memory usage: 105 MB
% 45.24/7.15 % (1293202)Instructions burned: 908 (million)
% 45.24/7.15 % (1293213)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=684851464:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 45.24/7.15 % (1293212)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1219038488:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 45.24/7.15 % (1293213)Instruction limit reached!
% 45.24/7.15 % (1293213)------------------------------
% 45.24/7.15 % (1293213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.15 % (1293213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.15 % (1293213)CaDiCaL version: 2.1.3
% 45.24/7.15 % (1293213)Termination reason: Instruction limit
% 45.24/7.15 % (1293213)Termination phase: Preprocessing 3
% 45.24/7.15 % (1293213)Time elapsed: 0.044 s
% 45.24/7.15 % (1293213)Peak memory usage: 93 MB
% 45.24/7.15 % (1293213)Instructions burned: 125 (million)
% 45.24/7.15 % (1293214)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1478231360:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 45.24/7.15 % (1293214)Instruction limit reached!
% 45.24/7.15 % (1293214)------------------------------
% 45.24/7.15 % (1293214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.15 % (1293214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.15 % (1293214)CaDiCaL version: 2.1.3
% 45.24/7.15 % (1293214)Termination reason: Instruction limit
% 45.24/7.15 % (1293214)Termination phase: Preprocessing 2
% 45.24/7.15 % (1293214)Time elapsed: 0.073 s
% 45.24/7.15 % (1293214)Peak memory usage: 92 MB
% 45.24/7.15 % (1293214)Instructions burned: 135 (million)
% 45.24/7.15 % (1293217)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2085761567:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 45.24/7.15 % (1293217)Refutation not found, incomplete strategy
% 45.24/7.15 % (1293217)------------------------------
% 45.24/7.15 % (1293217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.15 % (1293217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.15 % (1293217)CaDiCaL version: 2.1.3
% 45.24/7.15 % (1293217)Termination reason: Refutation not found, incomplete strategy
% 45.24/7.15 % (1293217)Time elapsed: 0.011 s
% 45.24/7.15 % (1293217)Peak memory usage: 94 MB
% 45.24/7.15 % (1293217)Instructions burned: 24 (million)
% 45.24/7.15 % (1293217)------------------------------
% 45.24/7.15 % (1293217)------------------------------
% 45.24/7.15 % (1293219)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3040975779:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 45.24/7.15 % (1293222)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=735663576:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 45.24/7.15 % (1293219)Instruction limit reached!
% 45.24/7.15 % (1293219)------------------------------
% 45.24/7.15 % (1293219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.15 % (1293219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.15 % (1293219)CaDiCaL version: 2.1.3
% 45.24/7.15 % (1293219)Termination reason: Instruction limit
% 45.24/7.15 % (1293219)Termination phase: Saturation
% 45.24/7.15 % (1293219)Time elapsed: 0.251 s
% 45.24/7.15 % (1293219)Peak memory usage: 96 MB
% 45.24/7.15 % (1293219)Instructions burned: 432 (million)
% 45.24/7.15 % (1293193)Instruction limit reached!
% 45.24/7.15 % (1293193)------------------------------
% 45.24/7.15 % (1293193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293193)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293193)Termination reason: Instruction limit
% 76.74/11.75 % (1293193)Termination phase: Saturation
% 76.74/11.75 % (1293193)Time elapsed: 1.464 s
% 76.74/11.75 % (1293193)Peak memory usage: 213 MB
% 76.74/11.75 % (1293193)Instructions burned: 2351 (million)
% 76.74/11.75 % (1293224)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1097028833:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 76.74/11.75 % (1293225)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=185190039:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 76.74/11.75 % (1293224)Instruction limit reached!
% 76.74/11.75 % (1293224)------------------------------
% 76.74/11.75 % (1293224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293224)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293224)Termination reason: Instruction limit
% 76.74/11.75 % (1293224)Termination phase: Property scanning
% 76.74/11.75 % (1293224)Time elapsed: 0.087 s
% 76.74/11.75 % (1293224)Peak memory usage: 96 MB
% 76.74/11.75 % (1293224)Instructions burned: 151 (million)
% 76.74/11.75 % (1293228)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=331265092:i=667:av=off:fsr=off_2973 on theBenchmark for (2973ds/667Mi)
% 76.74/11.75 % (1293228)Instruction limit reached!
% 76.74/11.75 % (1293228)------------------------------
% 76.74/11.75 % (1293228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293228)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293228)Termination reason: Instruction limit
% 76.74/11.75 % (1293228)Termination phase: Saturation
% 76.74/11.75 % (1293228)Time elapsed: 0.356 s
% 76.74/11.75 % (1293228)Peak memory usage: 106 MB
% 76.74/11.75 % (1293228)Instructions burned: 668 (million)
% 76.74/11.75 % (1293230)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1783341302:s2a=on:i=185:s2at=1.8:fdi=4_2967 on theBenchmark for (2967ds/185Mi)
% 76.74/11.75 % (1293230)Instruction limit reached!
% 76.74/11.75 % (1293230)------------------------------
% 76.74/11.75 % (1293230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293230)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293230)Termination reason: Instruction limit
% 76.74/11.75 % (1293230)Termination phase: Property scanning
% 76.74/11.75 % (1293230)Time elapsed: 0.119 s
% 76.74/11.75 % (1293230)Peak memory usage: 97 MB
% 76.74/11.75 % (1293230)Instructions burned: 187 (million)
% 76.74/11.75 % (1293233)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3467116994:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2965 on theBenchmark for (2965ds/193Mi)
% 76.74/11.75 % (1293233)Refutation not found, incomplete strategy
% 76.74/11.75 % (1293233)------------------------------
% 76.74/11.75 % (1293233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293233)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293233)Termination reason: Refutation not found, incomplete strategy
% 76.74/11.75 % (1293233)Time elapsed: 0.041 s
% 76.74/11.75 % (1293233)Peak memory usage: 94 MB
% 76.74/11.75 % (1293233)Instructions burned: 58 (million)
% 76.74/11.75 % (1293233)------------------------------
% 76.74/11.75 % (1293233)------------------------------
% 76.74/11.75 % (1293235)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=678437379:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2960 on theBenchmark for (2960ds/4850Mi)
% 76.74/11.75 % (1293222)Instruction limit reached!
% 76.74/11.75 % (1293222)------------------------------
% 76.74/11.75 % (1293222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.74/11.75 % (1293222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.74/11.75 % (1293222)CaDiCaL version: 2.1.3
% 76.74/11.75 % (1293222)Termination reason: Instruction limit
% 98.21/14.62 % (1293222)Termination phase: Saturation
% 98.21/14.62 % (1293222)Time elapsed: 1.967 s
% 98.21/14.62 % (1293222)Peak memory usage: 241 MB
% 98.21/14.62 % (1293222)Instructions burned: 6060 (million)
% 98.21/14.62 % (1293237)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=339117235:i=12111:sd=1:ss=included_2957 on theBenchmark for (2957ds/12111Mi)
% 98.21/14.62 % (1293204)Instruction limit reached!
% 98.21/14.62 % (1293204)------------------------------
% 98.21/14.62 % (1293204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.21/14.62 % (1293204)CaDiCaL version: 2.1.3
% 98.21/14.62 % (1293204)Termination reason: Instruction limit
% 98.21/14.62 % (1293204)Termination phase: Saturation
% 98.21/14.62 % (1293204)Time elapsed: 3.345 s
% 98.21/14.62 % (1293204)Peak memory usage: 217 MB
% 98.21/14.62 % (1293204)Instructions burned: 5202 (million)
% 98.21/14.62 % (1293237)Refutation not found, incomplete strategy
% 98.21/14.62 % (1293237)------------------------------
% 98.21/14.62 % (1293237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.21/14.62 % (1293237)CaDiCaL version: 2.1.3
% 98.21/14.62 % (1293237)Termination reason: Refutation not found, incomplete strategy
% 98.21/14.62 % (1293237)Time elapsed: 0.359 s
% 98.21/14.62 % (1293237)Peak memory usage: 146 MB
% 98.21/14.62 % (1293237)Instructions burned: 988 (million)
% 98.21/14.62 % (1293239)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=854483593:i=319:kws=precedence:fsr=off_2953 on theBenchmark for (2953ds/319Mi)
% 98.21/14.62 % (1293237)------------------------------
% 98.21/14.62 % (1293237)------------------------------
% 98.21/14.62 % (1293239)Instruction limit reached!
% 98.21/14.62 % (1293239)------------------------------
% 98.21/14.62 % (1293239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.21/14.62 % (1293239)CaDiCaL version: 2.1.3
% 98.21/14.62 % (1293239)Termination reason: Instruction limit
% 98.21/14.62 % (1293239)Termination phase: Saturation
% 98.21/14.62 % (1293239)Time elapsed: 0.160 s
% 98.21/14.62 % (1293239)Peak memory usage: 100 MB
% 98.21/14.62 % (1293239)Instructions burned: 320 (million)
% 98.21/14.62 % (1293241)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1354147559:i=2064:ep=RST_2950 on theBenchmark for (2950ds/2064Mi)
% 98.21/14.62 % (1293242)dis-1011_128_sil=32000:random_seed=381042175:i=3706:ep=RST:av=off_2950 on theBenchmark for (2950ds/3706Mi)
% 98.21/14.62 % (1293241)Instruction limit reached!
% 98.21/14.62 % (1293241)------------------------------
% 98.21/14.62 % (1293241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.21/14.62 % (1293241)CaDiCaL version: 2.1.3
% 98.21/14.62 % (1293241)Termination reason: Instruction limit
% 98.21/14.62 % (1293241)Termination phase: Saturation
% 98.21/14.62 % (1293241)Time elapsed: 0.561 s
% 98.21/14.62 % (1293241)Peak memory usage: 120 MB
% 98.21/14.62 % (1293241)Instructions burned: 2068 (million)
% 98.21/14.62 % (1293245)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=669040572:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2943 on theBenchmark for (2943ds/757Mi)
% 98.21/14.62 % (1293245)Instruction limit reached!
% 98.21/14.62 % (1293245)------------------------------
% 98.21/14.62 % (1293245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.21/14.62 % (1293245)CaDiCaL version: 2.1.3
% 98.21/14.62 % (1293245)Termination reason: Instruction limit
% 98.21/14.62 % (1293245)Termination phase: Saturation
% 98.21/14.62 % (1293245)Time elapsed: 0.319 s
% 98.21/14.62 % (1293245)Peak memory usage: 101 MB
% 98.21/14.62 % (1293245)Instructions burned: 757 (million)
% 98.21/14.62 % (1293247)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4270927081:i=13913:ss=axioms:sgt=8_2939 on theBenchmark for (2939ds/13913Mi)
% 98.21/14.62 % (1293235)Instruction limit reached!
% 98.21/14.62 % (1293235)------------------------------
% 98.21/14.62 % (1293235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.21/14.62 % (1293235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293235)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293235)Termination reason: Instruction limit
% 106.98/16.09 % (1293235)Termination phase: Saturation
% 106.98/16.09 % (1293235)Time elapsed: 2.352 s
% 106.98/16.09 % (1293235)Peak memory usage: 114 MB
% 106.98/16.09 % (1293235)Instructions burned: 4850 (million)
% 106.98/16.09 % (1293249)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=806440757:i=9925:aac=none_2935 on theBenchmark for (2935ds/9925Mi)
% 106.98/16.09 % (1293242)Instruction limit reached!
% 106.98/16.09 % (1293242)------------------------------
% 106.98/16.09 % (1293242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293242)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293242)Termination reason: Instruction limit
% 106.98/16.09 % (1293242)Termination phase: Saturation
% 106.98/16.09 % (1293242)Time elapsed: 1.637 s
% 106.98/16.09 % (1293242)Peak memory usage: 102 MB
% 106.98/16.09 % (1293242)Instructions burned: 3706 (million)
% 106.98/16.09 % (1293251)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=489991215:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2932 on theBenchmark for (2932ds/2479Mi)
% 106.98/16.09 % (1293251)Instruction limit reached!
% 106.98/16.09 % (1293251)------------------------------
% 106.98/16.09 % (1293251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293251)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293251)Termination reason: Instruction limit
% 106.98/16.09 % (1293251)Termination phase: Saturation
% 106.98/16.09 % (1293251)Time elapsed: 0.969 s
% 106.98/16.09 % (1293251)Peak memory usage: 96 MB
% 106.98/16.09 % (1293251)Instructions burned: 2481 (million)
% 106.98/16.09 % (1293253)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2704304736:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2920 on theBenchmark for (2920ds/440Mi)
% 106.98/16.09 % (1293253)Instruction limit reached!
% 106.98/16.09 % (1293253)------------------------------
% 106.98/16.09 % (1293253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293253)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293253)Termination reason: Instruction limit
% 106.98/16.09 % (1293253)Termination phase: Saturation
% 106.98/16.09 % (1293253)Time elapsed: 0.211 s
% 106.98/16.09 % (1293253)Peak memory usage: 102 MB
% 106.98/16.09 % (1293253)Instructions burned: 442 (million)
% 106.98/16.09 % (1293255)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2638976877:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2916 on theBenchmark for (2916ds/11145Mi)
% 106.98/16.09 % (1293212)Instruction limit reached!
% 106.98/16.09 % (1293212)------------------------------
% 106.98/16.09 % (1293212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293212)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293212)Termination reason: Instruction limit
% 106.98/16.09 % (1293212)Termination phase: Saturation
% 106.98/16.09 % (1293212)Time elapsed: 8.511 s
% 106.98/16.09 % (1293212)Peak memory usage: 250 MB
% 106.98/16.09 % (1293212)Instructions burned: 13193 (million)
% 106.98/16.09 % (1293257)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1487074632:cts=off:i=3034:av=off:er=known:fsd=on_2896 on theBenchmark for (2896ds/3034Mi)
% 106.98/16.09 % (1293247)Instruction limit reached!
% 106.98/16.09 % (1293247)------------------------------
% 106.98/16.09 % (1293247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293247)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293247)Termination reason: Instruction limit
% 106.98/16.09 % (1293247)Termination phase: Saturation
% 106.98/16.09 % (1293247)Time elapsed: 4.553 s
% 106.98/16.09 % (1293247)Peak memory usage: 231 MB
% 106.98/16.09 % (1293247)Instructions burned: 13915 (million)
% 106.98/16.09 % (1293259)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2868066308:st=2:s2a=on:i=524:s2at=2:ss=axioms_2892 on theBenchmark for (2892ds/524Mi)
% 106.98/16.09 % (1293259)Instruction limit reached!
% 106.98/16.09 % (1293259)------------------------------
% 106.98/16.09 % (1293259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293259)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293259)Termination reason: Instruction limit
% 106.98/16.09 % (1293259)Termination phase: Saturation
% 106.98/16.09 % (1293259)Time elapsed: 0.159 s
% 106.98/16.09 % (1293259)Peak memory usage: 100 MB
% 106.98/16.09 % (1293259)Instructions burned: 524 (million)
% 106.98/16.09 % (1293261)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1385148122:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2889 on theBenchmark for (2889ds/1016Mi)
% 106.98/16.09 % (1293261)Refutation not found, incomplete strategy
% 106.98/16.09 % (1293261)------------------------------
% 106.98/16.09 % (1293261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293261)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293261)Termination reason: Refutation not found, incomplete strategy
% 106.98/16.09 % (1293261)Time elapsed: 0.010 s
% 106.98/16.09 % (1293261)Peak memory usage: 94 MB
% 106.98/16.09 % (1293261)Instructions burned: 24 (million)
% 106.98/16.09 % (1293261)------------------------------
% 106.98/16.09 % (1293261)------------------------------
% 106.98/16.09 % (1293225)Instruction limit reached!
% 106.98/16.09 % (1293225)------------------------------
% 106.98/16.09 % (1293225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293225)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293225)Termination reason: Instruction limit
% 106.98/16.09 % (1293225)Termination phase: Saturation
% 106.98/16.09 % (1293225)Time elapsed: 8.872 s
% 106.98/16.09 % (1293225)Peak memory usage: 253 MB
% 106.98/16.09 % (1293225)Instructions burned: 14155 (million)
% 106.98/16.09 % (1293263)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1998967177:i=14123:bd=preordered:ins=4_2886 on theBenchmark for (2886ds/14123Mi)
% 106.98/16.09 % (1293265)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2861980784:i=5781:kws=precedence:bd=all:rawr=on_2884 on theBenchmark for (2884ds/5781Mi)
% 106.98/16.09 % (1293249)Instruction limit reached!
% 106.98/16.09 % (1293249)------------------------------
% 106.98/16.09 % (1293249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293249)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293249)Termination reason: Instruction limit
% 106.98/16.09 % (1293249)Termination phase: Saturation
% 106.98/16.09 % (1293249)Time elapsed: 5.588 s
% 106.98/16.09 % (1293249)Peak memory usage: 264 MB
% 106.98/16.09 % (1293249)Instructions burned: 9925 (million)
% 106.98/16.09 % (1293257)Instruction limit reached!
% 106.98/16.09 % (1293257)------------------------------
% 106.98/16.09 % (1293257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293257)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293257)Termination reason: Instruction limit
% 106.98/16.09 % (1293257)Termination phase: Saturation
% 106.98/16.09 % (1293257)Time elapsed: 1.817 s
% 106.98/16.09 % (1293257)Peak memory usage: 205 MB
% 106.98/16.09 % (1293257)Instructions burned: 3035 (million)
% 106.98/16.09 % (1293267)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3495196963:i=2448:gtgl=5:bd=preordered:gtg=all_2877 on theBenchmark for (2877ds/2448Mi)
% 106.98/16.09 % (1293268)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3808115341:i=3223:kws=precedence:fgj=on:av=off_2876 on theBenchmark for (2876ds/3223Mi)
% 106.98/16.09 % (1293267)Instruction limit reached!
% 106.98/16.09 % (1293267)------------------------------
% 106.98/16.09 % (1293267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293267)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293267)Termination reason: Instruction limit
% 106.98/16.09 % (1293267)Termination phase: Saturation
% 106.98/16.09 % (1293267)Time elapsed: 1.509 s
% 106.98/16.09 % (1293267)Peak memory usage: 212 MB
% 106.98/16.09 % (1293267)Instructions burned: 2449 (million)
% 106.98/16.09 % (1293271)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2497242620:st=5.6:i=2033:sd=3:ss=axioms_2860 on theBenchmark for (2860ds/2033Mi)
% 106.98/16.09 % (1293268)Instruction limit reached!
% 106.98/16.09 % (1293268)------------------------------
% 106.98/16.09 % (1293268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293268)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293268)Termination reason: Instruction limit
% 106.98/16.09 % (1293268)Termination phase: Saturation
% 106.98/16.09 % (1293268)Time elapsed: 1.820 s
% 106.98/16.09 % (1293268)Peak memory usage: 192 MB
% 106.98/16.09 % (1293268)Instructions burned: 3224 (million)
% 106.98/16.09 % (1293273)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=925918712:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2856 on theBenchmark for (2856ds/2055Mi)
% 106.98/16.09 % (1293265)Instruction limit reached!
% 106.98/16.09 % (1293265)------------------------------
% 106.98/16.09 % (1293265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293265)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293265)Termination reason: Instruction limit
% 106.98/16.09 % (1293265)Termination phase: Saturation
% 106.98/16.09 % (1293265)Time elapsed: 3.309 s
% 106.98/16.09 % (1293265)Peak memory usage: 145 MB
% 106.98/16.09 % (1293265)Instructions burned: 5781 (million)
% 106.98/16.09 % (1293255)Instruction limit reached!
% 106.98/16.09 % (1293255)------------------------------
% 106.98/16.09 % (1293255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.98/16.09 % (1293255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.98/16.09 % (1293255)CaDiCaL version: 2.1.3
% 106.98/16.09 % (1293255)Termination reason: Instruction limit
% 106.98/16.09 % (1293255)Termination phase: Saturation
% 106.98/16.09 % (1293255)Time elapsed: 6.593 s
% 106.98/16.09 % (1293255)Peak memory usage: 159 MB
% 106.98/16.09 % (1293255)Instructions burned: 11148 (million)
% 106.98/16.09 % (1293271)First to succeed.
% 106.98/16.09 % (1293271)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1293165"
% 106.98/16.09 % (1293275)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3996251557:i=21611:sd=3:ss=axioms_2849 on theBenchmark for (2849ds/21611Mi)
% 106.98/16.09 % (1293276)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1195380299:i=4835:sd=13:ss=axioms:sgt=23_2849 on theBenchmark for (2849ds/4835Mi)
% 106.98/16.09 % (1293271)Refutation found. Thanks to Tanya!
% 106.98/16.09 % SZS status Theorem for theBenchmark
% 106.98/16.09 % SZS output start Proof for theBenchmark
% See solution above
% 108.77/16.29 % (1293271)------------------------------
% 108.77/16.29 % (1293271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.77/16.29 % (1293271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.77/16.29 % (1293271)CaDiCaL version: 2.1.3
% 108.77/16.29 % (1293271)Termination reason: Refutation
% 108.77/16.29 % (1293271)Time elapsed: 0.976 s
% 108.77/16.29 % (1293271)Peak memory usage: 146 MB
% 108.77/16.29 % (1293271)Instructions burned: 1543 (million)
% 108.77/16.29 % (1293271)------------------------------
% 108.77/16.29 % (1293271)------------------------------
% 108.77/16.29 % (1293165)Success in time 15.412 s
% 108.77/16.29 % Vampire exiting
%------------------------------------------------------------------------------