%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR092+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:45:09 AM UTC 2026
% Result : Theorem 53.46s 13.72s
% Output : Refutation 53.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 21
% Syntax : Number of formulae : 140 ( 33 unt; 4 def)
% Number of atoms : 381 ( 4 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 467 ( 226 ~; 222 |; 8 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 5 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 86 ( 0 sgn 84 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f97,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__parent(X0,X1)
=> s__ancestor(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_97) ).
fof(f125,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__son(X0,X1)
=> s__parent(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_125) ).
fof(f5906,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5980) ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5997) ).
fof(f5956,axiom,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6030) ).
fof(f5972,axiom,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6046) ).
fof(f5999,axiom,
s__subclass(s__Primate,s__Mammal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6073) ).
fof(f6009,axiom,
s__subclass(s__Hominid,s__Primate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6083) ).
fof(f6012,axiom,
s__subclass(s__Human,s__Hominid),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6086) ).
fof(f6017,axiom,
s__subclass(s__Man,s__Human),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6091) ).
fof(f6021,axiom,
s__subclass(s__Woman,s__Human),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6095) ).
fof(f7218,axiom,
s__instance(s__Man22_1,s__Man),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f7219,axiom,
s__instance(s__Ancestor22_1,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f7220,axiom,
s__son(s__Man22_1,s__Ancestor22_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f7221,conjecture,
? [X0] :
( s__ancestor(s__Man22_1,X0)
& X0 = s__Ancestor22_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7222,negated_conjecture,
~ ? [X0] :
( s__ancestor(s__Man22_1,X0)
& X0 = s__Ancestor22_1 ),
inference(negated_conjecture,[status(cth)],[f7221]) ).
fof(f7316,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f7317,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f7318,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f7317]) ).
fof(f7434,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f97]) ).
fof(f7435,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f7434]) ).
fof(f7484,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__son(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f125]) ).
fof(f7485,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__son(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f7484]) ).
fof(f12410,plain,
! [X0] :
( ~ s__ancestor(s__Man22_1,X0)
| s__Ancestor22_1 != X0 ),
inference(ennf_transformation,[],[f7222]) ).
fof(f14336,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7316]) ).
fof(f14337,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7316]) ).
fof(f14338,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f7318]) ).
fof(f14407,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f7435]) ).
fof(f14432,plain,
! [X0,X1] :
( ~ s__son(X0,X1)
| s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f7485]) ).
fof(f21033,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[],[f5906]) ).
fof(f21055,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f5923]) ).
fof(f21088,plain,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f5956]) ).
fof(f21106,plain,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f5972]) ).
fof(f21133,plain,
s__subclass(s__Primate,s__Mammal),
inference(cnf_transformation,[],[f5999]) ).
fof(f21143,plain,
s__subclass(s__Hominid,s__Primate),
inference(cnf_transformation,[],[f6009]) ).
fof(f21146,plain,
s__subclass(s__Human,s__Hominid),
inference(cnf_transformation,[],[f6012]) ).
fof(f21151,plain,
s__subclass(s__Man,s__Human),
inference(cnf_transformation,[],[f6017]) ).
fof(f21155,plain,
s__subclass(s__Woman,s__Human),
inference(cnf_transformation,[],[f6021]) ).
fof(f22558,plain,
s__instance(s__Man22_1,s__Man),
inference(cnf_transformation,[],[f7218]) ).
fof(f22559,plain,
s__instance(s__Ancestor22_1,s__Human),
inference(cnf_transformation,[],[f7219]) ).
fof(f22560,plain,
s__son(s__Man22_1,s__Ancestor22_1),
inference(cnf_transformation,[],[f7220]) ).
fof(f22561,plain,
! [X0] :
( ~ s__ancestor(s__Man22_1,X0)
| s__Ancestor22_1 != X0 ),
inference(cnf_transformation,[],[f12410]) ).
fof(f22923,plain,
~ s__ancestor(s__Man22_1,s__Ancestor22_1),
inference(equality_resolution,[],[f22561]) ).
fof(f26760,definition,
( spl504_168
<=> s__instance(s__Human,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_168])],[avatar_definition]) ).
fof(f26761,plain,
( s__instance(s__Human,s__SetOrClass)
| ~ spl504_168 ),
inference(avatar_component_clause,[],[f26760]) ).
fof(f26762,plain,
( ~ s__instance(s__Human,s__SetOrClass)
| spl504_168 ),
inference(avatar_component_clause,[],[f26760]) ).
fof(f26768,plain,
( ! [X0] : ~ s__subclass(X0,s__Human)
| spl504_168 ),
inference(resolution,[],[f26762,f14336]) ).
fof(f26776,plain,
( $false
| spl504_168 ),
inference(resolution,[],[f26768,f21155]) ).
fof(f26779,plain,
spl504_168,
inference(avatar_contradiction_clause,[],[f26776]) ).
fof(f32175,plain,
( ~ s__parent(s__Man22_1,s__Ancestor22_1)
| ~ s__instance(s__Ancestor22_1,s__Organism)
| ~ s__instance(s__Man22_1,s__Organism) ),
inference(resolution,[],[f14407,f22923]) ).
fof(f32179,definition,
( spl504_239
<=> s__instance(s__Man22_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl504_239])],[avatar_definition]) ).
fof(f32180,plain,
( s__instance(s__Man22_1,s__Organism)
| ~ spl504_239 ),
inference(avatar_component_clause,[],[f32179]) ).
fof(f32181,plain,
( ~ s__instance(s__Man22_1,s__Organism)
| spl504_239 ),
inference(avatar_component_clause,[],[f32179]) ).
fof(f32183,definition,
( spl504_240
<=> s__instance(s__Ancestor22_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl504_240])],[avatar_definition]) ).
fof(f32184,plain,
( s__instance(s__Ancestor22_1,s__Organism)
| ~ spl504_240 ),
inference(avatar_component_clause,[],[f32183]) ).
fof(f32185,plain,
( ~ s__instance(s__Ancestor22_1,s__Organism)
| spl504_240 ),
inference(avatar_component_clause,[],[f32183]) ).
fof(f32187,definition,
( spl504_241
<=> s__parent(s__Man22_1,s__Ancestor22_1) ),
introduced(definition,[new_symbols(definition,[spl504_241])],[avatar_definition]) ).
fof(f32189,plain,
( ~ s__parent(s__Man22_1,s__Ancestor22_1)
| spl504_241 ),
inference(avatar_component_clause,[],[f32187]) ).
fof(f32190,plain,
( ~ spl504_239
| ~ spl504_240
| ~ spl504_241 ),
inference(avatar_split_clause,[],[f32175,f32187,f32183,f32179]) ).
fof(f32244,plain,
( s__parent(s__Man22_1,s__Ancestor22_1)
| ~ s__instance(s__Ancestor22_1,s__Organism)
| ~ s__instance(s__Man22_1,s__Organism) ),
inference(resolution,[],[f14432,f22560]) ).
fof(f73599,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f14338,f32181]) ).
fof(f73625,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f73599,f14336]) ).
fof(f73841,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f73625,f14337]) ).
fof(f74049,plain,
( ~ s__instance(s__Man22_1,s__Animal)
| spl504_239 ),
inference(resolution,[],[f73841,f21033]) ).
fof(f74054,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f74049,f14338]) ).
fof(f74055,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f74054,f14336]) ).
fof(f74056,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f74055,f14337]) ).
fof(f75872,plain,
( ~ s__instance(s__Man22_1,s__Vertebrate)
| spl504_239 ),
inference(resolution,[],[f74056,f21055]) ).
fof(f75879,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f75872,f14338]) ).
fof(f75880,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f75879,f14336]) ).
fof(f75881,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f75880,f14337]) ).
fof(f75968,plain,
( ~ s__instance(s__Man22_1,s__WarmBloodedVertebrate)
| spl504_239 ),
inference(resolution,[],[f75881,f21088]) ).
fof(f75986,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f75968,f14338]) ).
fof(f75987,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f75986,f14336]) ).
fof(f75988,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f75987,f14337]) ).
fof(f76074,plain,
( ~ s__instance(s__Man22_1,s__Mammal)
| spl504_239 ),
inference(resolution,[],[f75988,f21106]) ).
fof(f76092,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f76074,f14338]) ).
fof(f76093,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76092,f14336]) ).
fof(f76094,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76093,f14337]) ).
fof(f76259,plain,
( ~ s__instance(s__Man22_1,s__Primate)
| spl504_239 ),
inference(resolution,[],[f76094,f21133]) ).
fof(f76291,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f76259,f14338]) ).
fof(f76292,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76291,f14336]) ).
fof(f76293,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76292,f14337]) ).
fof(f76620,plain,
( ~ s__instance(s__Man22_1,s__Hominid)
| spl504_239 ),
inference(resolution,[],[f76293,f21143]) ).
fof(f76647,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f76620,f14338]) ).
fof(f76648,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76647,f14336]) ).
fof(f76649,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0) )
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f76648,f14337]) ).
fof(f80432,plain,
( ~ s__instance(s__Man22_1,s__Human)
| spl504_239 ),
inference(resolution,[],[f76649,f21146]) ).
fof(f80519,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Human,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_239 ),
inference(resolution,[],[f80432,f14338]) ).
fof(f80520,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_168
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f80519,f26761]) ).
fof(f80521,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0) )
| ~ spl504_168
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f80520,f14337]) ).
fof(f80560,plain,
( ~ s__instance(s__Man22_1,s__Man)
| ~ spl504_168
| spl504_239 ),
inference(resolution,[],[f80521,f21151]) ).
fof(f80561,plain,
( $false
| ~ spl504_168
| spl504_239 ),
inference(forward_subsumption_resolution,[],[f80560,f22558]) ).
fof(f80562,plain,
( ~ spl504_168
| spl504_239 ),
inference(avatar_contradiction_clause,[],[f80561]) ).
fof(f80575,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f32185,f14338]) ).
fof(f80576,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80575,f14336]) ).
fof(f80577,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80576,f14337]) ).
fof(f80640,plain,
( ~ s__instance(s__Ancestor22_1,s__Animal)
| spl504_240 ),
inference(resolution,[],[f80577,f21033]) ).
fof(f80645,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f80640,f14338]) ).
fof(f80646,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80645,f14336]) ).
fof(f80647,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80646,f14337]) ).
fof(f80681,plain,
( ~ s__instance(s__Ancestor22_1,s__Vertebrate)
| spl504_240 ),
inference(resolution,[],[f80647,f21055]) ).
fof(f80689,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f80681,f14338]) ).
fof(f80690,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80689,f14336]) ).
fof(f80691,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80690,f14337]) ).
fof(f80750,plain,
( ~ s__instance(s__Ancestor22_1,s__WarmBloodedVertebrate)
| spl504_240 ),
inference(resolution,[],[f80691,f21088]) ).
fof(f80754,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f80750,f14338]) ).
fof(f80755,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80754,f14336]) ).
fof(f80756,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80755,f14337]) ).
fof(f80871,plain,
( ~ s__instance(s__Ancestor22_1,s__Mammal)
| spl504_240 ),
inference(resolution,[],[f80756,f21106]) ).
fof(f80890,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f80871,f14338]) ).
fof(f80891,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80890,f14336]) ).
fof(f80892,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f80891,f14337]) ).
fof(f81032,plain,
( ~ s__instance(s__Ancestor22_1,s__Primate)
| spl504_240 ),
inference(resolution,[],[f80892,f21133]) ).
fof(f81069,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f81032,f14338]) ).
fof(f81070,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f81069,f14336]) ).
fof(f81071,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f81070,f14337]) ).
fof(f81109,plain,
( ~ s__instance(s__Ancestor22_1,s__Hominid)
| spl504_240 ),
inference(resolution,[],[f81071,f21143]) ).
fof(f81129,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(resolution,[],[f81109,f14338]) ).
fof(f81130,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f81129,f14336]) ).
fof(f81131,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f81130,f14337]) ).
fof(f81178,plain,
( ~ s__instance(s__Ancestor22_1,s__Human)
| spl504_240 ),
inference(resolution,[],[f81131,f21146]) ).
fof(f81179,plain,
( $false
| spl504_240 ),
inference(forward_subsumption_resolution,[],[f81178,f22559]) ).
fof(f81180,plain,
spl504_240,
inference(avatar_contradiction_clause,[],[f81179]) ).
fof(f81181,plain,
( ~ s__instance(s__Ancestor22_1,s__Organism)
| ~ s__instance(s__Man22_1,s__Organism)
| spl504_241 ),
inference(forward_subsumption_resolution,[],[f32244,f32189]) ).
fof(f81182,plain,
( ~ s__instance(s__Man22_1,s__Organism)
| ~ spl504_240
| spl504_241 ),
inference(forward_subsumption_resolution,[],[f81181,f32184]) ).
fof(f81183,plain,
( $false
| ~ spl504_239
| ~ spl504_240
| spl504_241 ),
inference(forward_subsumption_resolution,[],[f81182,f32180]) ).
fof(f81184,plain,
( ~ spl504_239
| ~ spl504_240
| spl504_241 ),
inference(avatar_contradiction_clause,[],[f81183]) ).
cnf(s205,plain,
spl504_168,
inference(sat_conversion,[],[f26779]) ).
cnf(s984,plain,
( ~ spl504_239
| ~ spl504_240
| ~ spl504_241 ),
inference(sat_conversion,[],[f32190]) ).
cnf(s3914,plain,
( ~ spl504_168
| spl504_239 ),
inference(sat_conversion,[],[f80562]) ).
cnf(s3920,plain,
spl504_240,
inference(sat_conversion,[],[f81180]) ).
cnf(s3921,plain,
( ~ spl504_239
| ~ spl504_240
| spl504_241 ),
inference(sat_conversion,[],[f81184]) ).
cnf(s3959,plain,
( ~ spl504_239
| ~ spl504_241 ),
inference(rat,[],[s984,s3920]) ).
cnf(s3980,plain,
spl504_239,
inference(rat,[],[s3914,s205]) ).
cnf(s3981,plain,
spl504_241,
inference(rat,[],[s3921,s3920,s3980]) ).
cnf(s3983,plain,
$false,
inference(rat,[],[s3959,s3981,s3980]) ).
fof(f81185,plain,
$false,
inference(avatar_sat_refutation,[],[s3983]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR092+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.18 % Computer : n015.cluster.edu
% 0.13/0.18 % Model : x86_64 x86_64
% 0.13/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.18 % Memory : 8046.5625MB
% 0.13/0.18 % OS : Linux 6.8.0-71-generic
% 0.13/0.18 % CPULimit : 300
% 0.13/0.18 % WCLimit : 300
% 0.13/0.18 % DateTime : Mon Sep 28 22:45:02 UTC 2026
% 0.13/0.19 % CPUTime :
% 0.13/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.22 Running first-order model finding
% 0.13/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.06/1.99 % (3114575)Will run a generic schedule for satisfiability detection.
% 9.06/1.99 % (3114583)dis+10_1_sil=32000:sp=arity:random_seed=2727203342:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 9.06/1.99 % (3114581)% WARNING: option uhcvi not known.
% 9.06/1.99 % (3114581)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2397704146:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 9.06/1.99 % (3114580)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1323041312_2997 on theBenchmark for (2997ds/0Mi)
% 9.06/1.99 % (3114582)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3632708009:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 9.06/1.99 % (3114584)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=465447729:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 9.06/1.99 % (3114586)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=884121078:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 9.06/1.99 % (3114585)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1482289700:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 9.06/1.99 % (3114583)Instruction limit reached!
% 9.06/1.99 % (3114583)------------------------------
% 9.06/1.99 % (3114583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/1.99 % (3114583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/1.99 % (3114583)CaDiCaL version: 2.1.3
% 9.06/1.99 % (3114583)Termination reason: Instruction limit
% 9.06/1.99 % (3114583)Termination phase: Property scanning
% 9.06/1.99 % (3114583)Time elapsed: 0.036 s
% 9.06/1.99 % (3114583)Peak memory usage: 24 MB
% 9.06/1.99 % (3114583)Instructions burned: 105 (million)
% 9.06/1.99 % (3114594)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=876016670:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 9.06/1.99 % (3114584)Instruction limit reached!
% 9.06/1.99 % (3114584)------------------------------
% 9.06/1.99 % (3114584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/1.99 % (3114584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/1.99 % (3114584)CaDiCaL version: 2.1.3
% 9.06/1.99 % (3114584)Termination reason: Instruction limit
% 9.06/1.99 % (3114584)Termination phase: Property scanning
% 9.06/1.99 % (3114584)Time elapsed: 0.071 s
% 9.06/1.99 % (3114584)Peak memory usage: 26 MB
% 9.06/1.99 % (3114584)Instructions burned: 116 (million)
% 9.06/1.99 % (3114586)Instruction limit reached!
% 9.06/1.99 % (3114586)------------------------------
% 9.06/1.99 % (3114586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/1.99 % (3114586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/1.99 % (3114586)CaDiCaL version: 2.1.3
% 9.06/1.99 % (3114586)Termination reason: Instruction limit
% 9.06/1.99 % (3114586)Termination phase: Equality resolution with deletion
% 9.06/1.99 % (3114586)Time elapsed: 0.090 s
% 9.06/1.99 % (3114586)Peak memory usage: 25 MB
% 9.06/1.99 % (3114586)Instructions burned: 161 (million)
% 9.06/1.99 % (3114596)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3716094514:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 9.06/1.99 % (3114598)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3348352338:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 9.06/1.99 % (3114585)Instruction limit reached!
% 9.06/1.99 % (3114585)------------------------------
% 9.06/1.99 % (3114585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/1.99 % (3114585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/1.99 % (3114585)CaDiCaL version: 2.1.3
% 9.06/1.99 % (3114585)Termination reason: Instruction limit
% 9.06/1.99 % (3114585)Termination phase: Property scanning
% 9.06/1.99 % (3114585)Time elapsed: 0.136 s
% 9.06/1.99 % (3114585)Peak memory usage: 24 MB
% 9.06/1.99 % (3114585)Instructions burned: 131 (million)
% 9.06/1.99 % (3114596)Instruction limit reached!
% 9.06/1.99 % (3114596)------------------------------
% 9.06/1.99 % (3114596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/1.99 % (3114596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/1.99 % (3114596)CaDiCaL version: 2.1.3
% 9.06/1.99 % (3114596)Termination reason: Instruction limit
% 9.06/1.99 % (3114596)Termination phase: Property scanning
% 22.44/3.65 % (3114596)Time elapsed: 0.078 s
% 22.44/3.65 % (3114596)Peak memory usage: 24 MB
% 22.44/3.65 % (3114596)Instructions burned: 132 (million)
% 22.44/3.65 % (3114601)ott-21_1_sil=16000:fs=off:random_seed=2423857179:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 22.44/3.65 % (3114603)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=63956003:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 22.44/3.65 % (3114594)Instruction limit reached!
% 22.44/3.65 % (3114594)------------------------------
% 22.44/3.65 % (3114594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % (3114594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/3.65 % (3114594)CaDiCaL version: 2.1.3
% 22.44/3.65 % (3114594)Termination reason: Instruction limit
% 22.44/3.65 % (3114594)Termination phase: Finite model building preprocessing
% 22.44/3.65 % (3114594)Time elapsed: 0.188 s
% 22.44/3.65 % (3114594)Peak memory usage: 36 MB
% 22.44/3.65 % (3114594)Instructions burned: 715 (million)
% 22.44/3.65 % (3114605)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=930845798:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 22.44/3.65 % (3114601)Instruction limit reached!
% 22.44/3.65 % (3114601)------------------------------
% 22.44/3.65 % (3114601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % (3114601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/3.65 % (3114601)CaDiCaL version: 2.1.3
% 22.44/3.65 % (3114601)Termination reason: Instruction limit
% 22.44/3.65 % (3114601)Termination phase: Property scanning
% 22.44/3.65 % (3114601)Time elapsed: 0.131 s
% 22.44/3.65 % (3114601)Peak memory usage: 25 MB
% 22.44/3.65 % (3114601)Instructions burned: 181 (million)
% 22.44/3.65 % (3114607)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1658576016:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 22.44/3.65 % (3114603)Instruction limit reached!
% 22.44/3.65 % (3114603)------------------------------
% 22.44/3.65 % (3114603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % (3114603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/3.65 % (3114603)CaDiCaL version: 2.1.3
% 22.44/3.65 % (3114603)Termination reason: Instruction limit
% 22.44/3.65 % (3114603)Termination phase: Saturation
% 22.44/3.65 % (3114603)Time elapsed: 0.260 s
% 22.44/3.65 % (3114603)Peak memory usage: 30 MB
% 22.44/3.65 % (3114603)Instructions burned: 477 (million)
% 22.44/3.65 % (3114616)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3167518032:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 22.44/3.65 % (3114605)Instruction limit reached!
% 22.44/3.65 % (3114605)------------------------------
% 22.44/3.65 % (3114605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % (3114605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/3.65 % (3114605)CaDiCaL version: 2.1.3
% 22.44/3.65 % (3114605)Termination reason: Instruction limit
% 22.44/3.65 % (3114605)Termination phase: Finite model building preprocessing
% 22.44/3.65 % (3114605)Time elapsed: 0.266 s
% 22.44/3.65 % (3114605)Peak memory usage: 39 MB
% 22.44/3.65 % (3114605)Instructions burned: 866 (million)
% 22.44/3.65 % (3114598)Instruction limit reached!
% 22.44/3.65 % (3114598)------------------------------
% 22.44/3.65 % (3114598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % (3114598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/3.65 % (3114598)CaDiCaL version: 2.1.3
% 22.44/3.65 % (3114598)Termination reason: Instruction limit
% 22.44/3.65 % (3114598)Termination phase: Saturation
% 22.44/3.65 % (3114598)Time elapsed: 0.403 s
% 22.44/3.65 % (3114598)Peak memory usage: 32 MB
% 22.44/3.65 % (3114598)Instructions burned: 684 (million)
% 22.44/3.65 % (3114618)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3320912808:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 22.44/3.65 % (3114619)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3784882834:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 22.44/3.65 % (3114616)Instruction limit reached!
% 22.44/3.65 % (3114616)------------------------------
% 22.44/3.65 % (3114616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.44/3.65 % Detected minimum model sizes of [51]
% 38.82/5.91 % (3114616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % Detected maximum model sizes of [max]
% 38.82/5.91 % (3114580)Cannot represent all propositional literals internally
% 38.82/5.91 % (3114580)Refutation not found, incomplete strategy
% 38.82/5.91 % (3114580)------------------------------
% 38.82/5.91 % (3114580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.82/5.91 % (3114616)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114616)Termination reason: Instruction limit
% 38.82/5.91 % (3114616)Termination phase: Finite model building preprocessing
% 38.82/5.91 % (3114580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % (3114616)Time elapsed: 0.428 s
% 38.82/5.91 % (3114580)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114616)Peak memory usage: 40 MB
% 38.82/5.91 % (3114616)Instructions burned: 890 (million)
% 38.82/5.91 % (3114580)Termination reason: Refutation not found, incomplete strategy
% 38.82/5.91 % (3114580)Time elapsed: 0.911 s
% 38.82/5.91 % (3114580)Peak memory usage: 49 MB
% 38.82/5.91 % (3114580)Instructions burned: 1473 (million)
% 38.82/5.91 % (3114580)------------------------------
% 38.82/5.91 % (3114580)------------------------------
% 38.82/5.91 % (3114632)fmb+10_1_sil=64000:random_seed=499017240:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 38.82/5.91 % (3114633)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3512770750:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 38.82/5.91 % (3114618)Instruction limit reached!
% 38.82/5.91 % (3114618)------------------------------
% 38.82/5.91 % (3114618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.82/5.91 % (3114618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % (3114618)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114618)Termination reason: Instruction limit
% 38.82/5.91 % (3114618)Termination phase: Saturation
% 38.82/5.91 % (3114618)Time elapsed: 0.541 s
% 38.82/5.91 % (3114618)Peak memory usage: 35 MB
% 38.82/5.91 % (3114618)Instructions burned: 692 (million)
% 38.82/5.91 % (3114640)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3627267037:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 38.82/5.91 % (3114619)Instruction limit reached!
% 38.82/5.91 % (3114619)------------------------------
% 38.82/5.91 % (3114619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.82/5.91 % (3114619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % (3114619)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114619)Termination reason: Instruction limit
% 38.82/5.91 % (3114619)Termination phase: Saturation
% 38.82/5.91 % (3114619)Time elapsed: 0.745 s
% 38.82/5.91 % (3114619)Peak memory usage: 37 MB
% 38.82/5.91 % (3114619)Instructions burned: 879 (million)
% 38.82/5.91 % (3114607)Instruction limit reached!
% 38.82/5.91 % (3114607)------------------------------
% 38.82/5.91 % (3114607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.82/5.91 % (3114607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % (3114607)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114607)Termination reason: Instruction limit
% 38.82/5.91 % (3114607)Termination phase: Saturation
% 38.82/5.91 % (3114607)Time elapsed: 0.970 s
% 38.82/5.91 % (3114607)Peak memory usage: 36 MB
% 38.82/5.91 % (3114607)Instructions burned: 1179 (million)
% 38.82/5.91 % (3114644)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1997064464:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 38.82/5.91 % (3114645)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1918902258:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 38.82/5.91 % Detected minimum model sizes of [51]
% 38.82/5.91 % Detected maximum model sizes of [max]
% 38.82/5.91 % (3114632)Cannot represent all propositional literals internally
% 38.82/5.91 % (3114632)Refutation not found, incomplete strategy
% 38.82/5.91 % (3114632)------------------------------
% 38.82/5.91 % (3114632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.82/5.91 % (3114632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.82/5.91 % (3114632)CaDiCaL version: 2.1.3
% 38.82/5.91 % (3114632)Termination reason: Refutation not found, incomplete strategy
% 38.82/5.91 % (3114632)Time elapsed: 0.566 s
% 38.82/5.91 % (3114632)Peak memory usage: 43 MB
% 38.82/5.91 % (3114632)Instructions burned: 1181 (million)
% 38.82/5.91 % (3114632)------------------------------
% 38.82/5.91 % (3114632)------------------------------
% 38.82/5.91 % (3114651)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3869803060:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 48.42/7.25 % (3114640)Instruction limit reached!
% 48.42/7.25 % (3114640)------------------------------
% 48.42/7.25 % (3114640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.42/7.25 % (3114640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.42/7.25 % (3114640)CaDiCaL version: 2.1.3
% 48.42/7.25 % (3114640)Termination reason: Instruction limit
% 48.42/7.25 % (3114640)Termination phase: Finite model building preprocessing
% 48.42/7.25 % (3114640)Time elapsed: 0.635 s
% 48.42/7.25 % (3114640)Peak memory usage: 39 MB
% 48.42/7.25 % (3114640)Instructions burned: 920 (million)
% 48.42/7.25 % (3114656)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1304093654:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 48.42/7.25 % Detected minimum model sizes of [51]
% 48.42/7.25 % Detected maximum model sizes of [max]
% 48.42/7.25 % (3114633)Cannot represent all propositional literals internally
% 48.42/7.25 % (3114633)Refutation not found, incomplete strategy
% 48.42/7.25 % (3114633)------------------------------
% 48.42/7.25 % (3114633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.42/7.25 % (3114633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.42/7.25 % (3114633)CaDiCaL version: 2.1.3
% 48.42/7.25 % (3114633)Termination reason: Refutation not found, incomplete strategy
% 48.42/7.25 % (3114633)Time elapsed: 0.944 s
% 48.42/7.25 % (3114633)Peak memory usage: 44 MB
% 48.42/7.25 % (3114633)Instructions burned: 1256 (million)
% 48.42/7.25 % (3114633)------------------------------
% 48.42/7.25 % (3114633)------------------------------
% 48.42/7.25 % (3114661)ott-2_1_sil=16000:newcnf=on:random_seed=2801539073:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi)
% 48.42/7.25 % Detected minimum model sizes of [51]
% 48.42/7.25 % Detected maximum model sizes of [max]
% 48.42/7.25 % (3114651)Cannot represent all propositional literals internally
% 48.42/7.25 % (3114651)Refutation not found, incomplete strategy
% 48.42/7.25 % (3114651)------------------------------
% 48.42/7.25 % (3114651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.42/7.25 % (3114651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.42/7.25 % (3114651)CaDiCaL version: 2.1.3
% 48.42/7.25 % (3114651)Termination reason: Refutation not found, incomplete strategy
% 48.42/7.25 % (3114651)Time elapsed: 0.686 s
% 48.42/7.25 % (3114651)Peak memory usage: 48 MB
% 48.42/7.25 % (3114651)Instructions burned: 1456 (million)
% 48.42/7.25 % (3114651)------------------------------
% 48.42/7.25 % (3114651)------------------------------
% 48.42/7.25 % (3114668)ott+10_1_sil=32000:tgt=ground:random_seed=1671586719:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi)
% 48.42/7.25 % (3114645)Instruction limit reached!
% 48.42/7.25 % (3114645)------------------------------
% 48.42/7.25 % (3114645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.42/7.25 % (3114645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.42/7.25 % (3114645)CaDiCaL version: 2.1.3
% 48.42/7.25 % (3114645)Termination reason: Instruction limit
% 48.42/7.25 % (3114645)Termination phase: Saturation
% 48.42/7.25 % (3114645)Time elapsed: 1.137 s
% 48.42/7.25 % (3114645)Peak memory usage: 43 MB
% 48.42/7.25 % (3114645)Instructions burned: 1473 (million)
% 48.42/7.25 % (3114672)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=744242660:i=54282_2972 on theBenchmark for (2972ds/54282Mi)
% 48.42/7.25 % (3114661)Instruction limit reached!
% 48.42/7.25 % (3114661)------------------------------
% 48.42/7.25 % (3114661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.42/7.25 % (3114661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.42/7.25 % (3114661)CaDiCaL version: 2.1.3
% 48.42/7.25 % (3114661)Termination reason: Instruction limit
% 48.42/7.25 % (3114661)Termination phase: Saturation
% 48.42/7.25 % (3114661)Time elapsed: 0.796 s
% 48.42/7.25 % (3114661)Peak memory usage: 38 MB
% 48.42/7.25 % (3114661)Instructions burned: 869 (million)
% 48.42/7.25 % (3114677)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=369230943:i=3512:aac=none_2970 on theBenchmark for (2970ds/3512Mi)
% 48.42/7.25 % Detected minimum model sizes of [51]
% 48.42/7.25 % Detected maximum model sizes of [max]
% 48.42/7.25 % (3114672)Cannot represent all propositional literals internally
% 48.42/7.25 % (3114672)Refutation not found, incomplete strategy
% 48.42/7.25 % (3114672)------------------------------
% 92.45/13.41 % (3114672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114672)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114672)Termination reason: Refutation not found, incomplete strategy
% 92.45/13.41 % (3114672)Time elapsed: 0.701 s
% 92.45/13.41 % (3114672)Peak memory usage: 48 MB
% 92.45/13.41 % (3114672)Instructions burned: 1465 (million)
% 92.45/13.41 % (3114672)------------------------------
% 92.45/13.41 % (3114672)------------------------------
% 92.45/13.41 % (3114682)dis+21_1_sil=32000:sas=cadical:random_seed=1544449722:i=3773:amm=off_2965 on theBenchmark for (2965ds/3773Mi)
% 92.45/13.41 % (3114656)Instruction limit reached!
% 92.45/13.41 % (3114656)------------------------------
% 92.45/13.41 % (3114656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114656)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114656)Termination reason: Instruction limit
% 92.45/13.41 % (3114656)Termination phase: Finite model building preprocessing
% 92.45/13.41 % (3114656)Time elapsed: 1.785 s
% 92.45/13.41 % (3114656)Peak memory usage: 62 MB
% 92.45/13.41 % (3114656)Instructions burned: 2174 (million)
% 92.45/13.41 % (3114687)ott+11_1_sil=16000:gs=on:random_seed=2559781761:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2961 on theBenchmark for (2961ds/2251Mi)
% 92.45/13.41 % (3114682)Instruction limit reached!
% 92.45/13.41 % (3114682)------------------------------
% 92.45/13.41 % (3114682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114682)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114682)Termination reason: Instruction limit
% 92.45/13.41 % (3114682)Termination phase: Saturation
% 92.45/13.41 % (3114682)Time elapsed: 1.681 s
% 92.45/13.41 % (3114682)Peak memory usage: 58 MB
% 92.45/13.41 % (3114682)Instructions burned: 3774 (million)
% 92.45/13.41 % (3114700)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=12927972:fmbsr=1.6:i=67534_2948 on theBenchmark for (2948ds/67534Mi)
% 92.45/13.41 % (3114677)Instruction limit reached!
% 92.45/13.41 % (3114677)------------------------------
% 92.45/13.41 % (3114677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114677)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114677)Termination reason: Instruction limit
% 92.45/13.41 % (3114677)Termination phase: Saturation
% 92.45/13.41 % (3114677)Time elapsed: 2.418 s
% 92.45/13.41 % (3114677)Peak memory usage: 60 MB
% 92.45/13.41 % (3114677)Instructions burned: 3514 (million)
% 92.45/13.41 % (3114707)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3759840057:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2945 on theBenchmark for (2945ds/4591Mi)
% 92.45/13.41 % Detected minimum model sizes of [51]
% 92.45/13.41 % Detected maximum model sizes of [max]
% 92.45/13.41 % (3114700)Cannot represent all propositional literals internally
% 92.45/13.41 % (3114700)Refutation not found, incomplete strategy
% 92.45/13.41 % (3114700)------------------------------
% 92.45/13.41 % (3114700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114700)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114700)Termination reason: Refutation not found, incomplete strategy
% 92.45/13.41 % (3114700)Time elapsed: 0.359 s
% 92.45/13.41 % (3114700)Peak memory usage: 45 MB
% 92.45/13.41 % (3114700)Instructions burned: 1418 (million)
% 92.45/13.41 % (3114700)------------------------------
% 92.45/13.41 % (3114700)------------------------------
% 92.45/13.41 % (3114726)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3490732631:i=29340_2944 on theBenchmark for (2944ds/29340Mi)
% 92.45/13.41 % (3114687)Instruction limit reached!
% 92.45/13.41 % (3114687)------------------------------
% 92.45/13.41 % (3114687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.45/13.41 % (3114687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.45/13.41 % (3114687)CaDiCaL version: 2.1.3
% 92.45/13.41 % (3114687)Termination reason: Instruction limit
% 92.45/13.41 % (3114687)Termination phase: Saturation
% 92.45/13.41 % (3114687)Time elapsed: 1.830 s
% 92.45/13.41 % (3114687)Peak memory usage: 75 MB
% 53.46/13.72 % (3114687)Instructions burned: 2252 (million)
% 53.46/13.72 % (3114644)Instruction limit reached!
% 53.46/13.72 % (3114644)------------------------------
% 53.46/13.72 % (3114644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114644)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114644)Termination reason: Instruction limit
% 53.46/13.72 % (3114644)Termination phase: Saturation
% 53.46/13.72 % (3114644)Time elapsed: 4.127 s
% 53.46/13.72 % (3114644)Peak memory usage: 57 MB
% 53.46/13.72 % (3114644)Instructions burned: 5132 (million)
% 53.46/13.72 % (3114746)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1638898275:i=5211_2943 on theBenchmark for (2943ds/5211Mi)
% 53.46/13.72 % (3114747)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2399695657:i=5497:nm=2_2943 on theBenchmark for (2943ds/5497Mi)
% 53.46/13.72 % (3114668)Instruction limit reached!
% 53.46/13.72 % (3114668)------------------------------
% 53.46/13.72 % (3114668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114668)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114668)Termination reason: Instruction limit
% 53.46/13.72 % (3114668)Termination phase: Saturation
% 53.46/13.72 % (3114668)Time elapsed: 3.480 s
% 53.46/13.72 % (3114668)Peak memory usage: 63 MB
% 53.46/13.72 % (3114668)Instructions burned: 5117 (million)
% 53.46/13.72 % (3114767)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3715153489:fmbsr=2:i=46332_2940 on theBenchmark for (2940ds/46332Mi)
% 53.46/13.72 % Detected minimum model sizes of [51]
% 53.46/13.72 % Detected maximum model sizes of [max]
% 53.46/13.72 % (3114747)Cannot represent all propositional literals internally
% 53.46/13.72 % (3114747)Refutation not found, incomplete strategy
% 53.46/13.72 % (3114747)------------------------------
% 53.46/13.72 % (3114747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114747)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114747)Termination reason: Refutation not found, incomplete strategy
% 53.46/13.72 % (3114747)Time elapsed: 0.635 s
% 53.46/13.72 % (3114747)Peak memory usage: 45 MB
% 53.46/13.72 % (3114747)Instructions burned: 1327 (million)
% 53.46/13.72 % (3114747)------------------------------
% 53.46/13.72 % (3114747)------------------------------
% 53.46/13.72 % (3114818)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3722190275:i=14071_2936 on theBenchmark for (2936ds/14071Mi)
% 53.46/13.72 % Detected minimum model sizes of [51]
% 53.46/13.72 % Detected maximum model sizes of [max]
% 53.46/13.72 % (3114767)Cannot represent all propositional literals internally
% 53.46/13.72 % (3114767)Refutation not found, incomplete strategy
% 53.46/13.72 % (3114767)------------------------------
% 53.46/13.72 % (3114767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114767)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114767)Termination reason: Refutation not found, incomplete strategy
% 53.46/13.72 % (3114767)Time elapsed: 0.639 s
% 53.46/13.72 % (3114767)Peak memory usage: 45 MB
% 53.46/13.72 % (3114767)Instructions burned: 1417 (million)
% 53.46/13.72 % (3114767)------------------------------
% 53.46/13.72 % (3114767)------------------------------
% 53.46/13.72 % (3114825)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3780938845:i=22565:add=on:rawr=on_2933 on theBenchmark for (2933ds/22565Mi)
% 53.46/13.72 % Detected minimum model sizes of [51]
% 53.46/13.72 % Detected maximum model sizes of [max]
% 53.46/13.72 % (3114818)Cannot represent all propositional literals internally
% 53.46/13.72 % (3114818)Refutation not found, incomplete strategy
% 53.46/13.72 % (3114818)------------------------------
% 53.46/13.72 % (3114818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114818)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114818)Termination reason: Refutation not found, incomplete strategy
% 53.46/13.72 % (3114818)Time elapsed: 0.598 s
% 53.46/13.72 % (3114818)Peak memory usage: 46 MB
% 53.46/13.72 % (3114818)Instructions burned: 1286 (million)
% 53.46/13.72 % (3114818)------------------------------
% 53.46/13.72 % (3114818)------------------------------
% 53.46/13.72 % (3114869)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2253199879:i=8173:av=off_2930 on theBenchmark for (2930ds/8173Mi)
% 53.46/13.72 % (3114746)Instruction limit reached!
% 53.46/13.72 % (3114746)------------------------------
% 53.46/13.72 % (3114746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114746)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114746)Termination reason: Instruction limit
% 53.46/13.72 % (3114746)Termination phase: Saturation
% 53.46/13.72 % (3114746)Time elapsed: 1.977 s
% 53.46/13.72 % (3114746)Peak memory usage: 47 MB
% 53.46/13.72 % (3114746)Instructions burned: 5213 (million)
% 53.46/13.72 % (3114871)dis+10_16:1_sil=16000:random_seed=3188654885:i=9155:fsr=off_2923 on theBenchmark for (2923ds/9155Mi)
% 53.46/13.72 % (3114707)Instruction limit reached!
% 53.46/13.72 % (3114707)------------------------------
% 53.46/13.72 % (3114707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114707)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114707)Termination reason: Instruction limit
% 53.46/13.72 % (3114707)Termination phase: Saturation
% 53.46/13.72 % (3114707)Time elapsed: 2.587 s
% 53.46/13.72 % (3114707)Peak memory usage: 97 MB
% 53.46/13.72 % (3114707)Instructions burned: 4592 (million)
% 53.46/13.72 % (3114873)ott-3_8_sil=64000:random_seed=1721350707:i=20139:bs=on_2919 on theBenchmark for (2919ds/20139Mi)
% 53.46/13.72 % (3114869)Instruction limit reached!
% 53.46/13.72 % (3114869)------------------------------
% 53.46/13.72 % (3114869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114869)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114869)Termination reason: Instruction limit
% 53.46/13.72 % (3114869)Termination phase: Saturation
% 53.46/13.72 % (3114869)Time elapsed: 4.305 s
% 53.46/13.72 % (3114869)Peak memory usage: 110 MB
% 53.46/13.72 % (3114869)Instructions burned: 8174 (million)
% 53.46/13.72 % (3114875)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1326392919:fmbsr=2:i=32576_2886 on theBenchmark for (2886ds/32576Mi)
% 53.46/13.72 % (3114871)Instruction limit reached!
% 53.46/13.72 % (3114871)------------------------------
% 53.46/13.72 % (3114871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114871)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114871)Termination reason: Instruction limit
% 53.46/13.72 % (3114871)Termination phase: Saturation
% 53.46/13.72 % (3114871)Time elapsed: 4.011 s
% 53.46/13.72 % (3114871)Peak memory usage: 92 MB
% 53.46/13.72 % (3114871)Instructions burned: 9156 (million)
% 53.46/13.72 % (3114877)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1274725066:i=11404_2882 on theBenchmark for (2882ds/11404Mi)
% 53.46/13.72 % Detected minimum model sizes of [51]
% 53.46/13.72 % Detected maximum model sizes of [max]
% 53.46/13.72 % (3114875)Cannot represent all propositional literals internally
% 53.46/13.72 % (3114875)Refutation not found, incomplete strategy
% 53.46/13.72 % (3114875)------------------------------
% 53.46/13.72 % (3114875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114875)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114875)Termination reason: Refutation not found, incomplete strategy
% 53.46/13.72 % (3114875)Time elapsed: 0.709 s
% 53.46/13.72 % (3114875)Peak memory usage: 48 MB
% 53.46/13.72 % (3114875)Instructions burned: 1456 (million)
% 53.46/13.72 % (3114875)------------------------------
% 53.46/13.72 % (3114875)------------------------------
% 53.46/13.72 % (3114879)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3292720153:i=14134_2879 on theBenchmark for (2879ds/14134Mi)
% 53.46/13.72 % (3114726)Instruction limit reached!
% 53.46/13.72 % (3114726)------------------------------
% 53.46/13.72 % (3114726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.72 % (3114726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.72 % (3114726)CaDiCaL version: 2.1.3
% 53.46/13.72 % (3114726)Termination reason: Instruction limit
% 53.46/13.72 % (3114726)Termination phase: Saturation
% 53.46/13.72 % (3114726)Time elapsed: 7.619 s
% 53.46/13.72 % (3114726)Peak memory usage: 78 MB
% 53.46/13.72 % (3114726)Instructions burned: 29342 (million)
% 53.46/13.72 % (3114907)dis+33_16_sil=32000:sac=on:random_seed=1760415063:i=15851:nm=0_2868 on theBenchmark for (2868ds/15851Mi)
% 53.46/13.72 % (3114879) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3114575-3114879"...
% 53.46/13.72 % (3114879)...printing done.
% 53.46/13.72 % (3114879)Refutation found. Thanks to Tanya!
% 53.46/13.72 % SZS status Theorem for theBenchmark
% 53.46/13.72 % SZS output start Proof for theBenchmark
% See solution above
% 53.46/13.73 % (3114879)------------------------------
% 53.46/13.73 % (3114879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.46/13.73 % (3114879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/13.73 % (3114879)CaDiCaL version: 2.1.3
% 53.46/13.73 % (3114879)Termination reason: Refutation
% 53.46/13.73 % (3114879)Time elapsed: 1.273 s
% 53.46/13.73 % (3114879)Peak memory usage: 47 MB
% 53.46/13.73 % (3114879)Instructions burned: 2379 (million)
% 53.46/13.73 % (3114575)Success in time 13.496 s
% 53.46/13.73 % Vampire exiting
%------------------------------------------------------------------------------